# Theory IntFactorization

Up to index of Isabelle/HOL/HOL-Complex/NumberTheory

theory IntFactorization = Factorization + NatIntLib:

```(*  Title:      IntFactorization.thy
Author:     David Gray
*)

header {* Unique factorization for integers *}

theory IntFactorization = Factorization + NatIntLib:;

(********************************************************************)
(* the following 5 lemmas set up the zprime, prime set equivalence  *)
(* but gr_1_prop is also used for other things in this file...      *)
(* should move all these to IntPrimes (or Int2, though IntPrimes    *)
(* would be better)?                                                *)
(********************************************************************)

lemma gr_1_prop: "(1 < p) = (1 < nat p)";
by (auto simp add: zless_nat_eq_int_zless);

lemma int_nat_dvd_prop: "(m dvd p) = (int m dvd int p)";
apply (auto simp add: dvd_def);
apply (rule_tac x = "int k" in exI);
apply (auto simp add: zmult_int);
apply (rule_tac x = "nat k" in exI);
proof-;
fix k;
assume "int p = int m * k";
then have "nat (int p) = nat(int m * k)";
by (auto);
then have "p = nat(int m * k)";
by (auto);
also have "... = nat(int m) * nat k";
apply (insert nat_mult_distrib [of "int m" k]);
apply (auto);
done;
finally have "p = nat (int m) * nat k".;
thus "p = m * nat k"; by auto;
qed;

lemma nat_int_dvd_prop: "[| 0 < m; m dvd p |] ==> (nat m dvd nat p)";
by (auto simp add: int_nat_dvd_prop);

lemma nat_prime_prop: "(p: zprime) = ((nat p): prime)";
proof;
assume "p : zprime";
then have p:"0 <= p" by (auto simp add: zprime_def);
from prems show "(nat p):prime";
apply (auto simp add: prems zprime_def prime_def gr_1_prop);
apply (drule_tac x = "int m" in allE, auto);
proof-;
fix m;
assume "m dvd nat p" and "~ int m dvd p";
then have "(int m) dvd int (nat p)";
by (insert int_nat_dvd_prop [of m "nat p"] prems, auto);
also have "int (nat p) = p"; by (auto simp add: p);
finally have "int m dvd p".;
with prems have "False"; by auto;
thus "m = Suc 0"; by auto;
qed;
next;
assume "nat p : prime";
thus "p : zprime";
apply (auto simp add: prime_def zprime_def gr_1_prop);
apply (drule_tac x = "nat m" in allE);
apply (auto);
proof-;
fix m;
assume "Suc 0 < nat p" and "0 <= m" and
"m dvd p" and "~ nat m dvd nat p";
then have p: "1 < p"; by (auto simp add: gr_1_prop);
from prems have "~(int (nat m) dvd int (nat p))";
by (auto simp add: int_nat_dvd_prop);
also have "int (nat m) = m" by (auto simp add: prems);
also have "int (nat p) = p" by (insert p, auto);
finally have "~(m dvd p)" .;
with prems have "False" by auto;
thus "m = 1"; by auto;
next;
fix m;
assume "nat m = Suc 0" and p:"0 <= m";
then have "int (nat m) = int (Suc 0)" by auto;
also have "int (nat m) = m" by (auto simp add: p);
also have "int (Suc 0) = 1" by auto;
finally show "m = 1" .;
next;
fix m;
assume "Suc 0 < nat p" and p1:"0 <= m" and
"m ~= p" and "nat m = nat p";
then have p2: "1 < p"; by (auto simp add: gr_1_prop);
from prems have "int (nat m) = int (nat p)";
by auto;
also have "int (nat m) = m" by (auto simp add: p1);
also have "int (nat p) = p" by (insert p2, auto);
finally have "m = p" .;
with prems have "False" by auto;
thus "m = 1" by auto;
qed;
qed;

lemma int_prime_prop: "(int p : zprime) = (p : prime)";
by (auto simp add: nat_prime_prop);

(****************************)
(* Now for the real stuff!! *)
(****************************)

consts
intl     :: "nat list => int list"
natl     :: "int list => nat list"
zprimel  :: "int list => bool"
znondec  :: "int list => bool"
zprod    :: "int list => int";

primrec
"natl []       = []"
"natl (x # xs) = (nat x) # (natl xs)";

primrec
"intl []       = []"
"intl (x # xs) = (int x) # (intl xs)";

defs
zprimel_def: "zprimel xs == set xs ⊆ zprime";

primrec
"znondec [] = True"
"znondec (x # xs) = (case xs of [] => True | y # ys => x <= y ∧ znondec xs)";

primrec
"zprod [] = 1"
"zprod (x # xs) = x * zprod xs";

subsection {* Properties about intl and natl *}

lemma intl_natl_prime [rule_format]: "zprimel x --> intl (natl x) = x";
by (induct_tac x, auto simp add: zprimel_def zprime_def);

lemma intl_natl_prop [rule_format]: "x = y --> intl x = intl y";
by (induct x, auto);

subsection {* Properties about zprimel *}

lemma zprimel_distrib1: "zprimel (h # t) ==> (h : zprime)";
by (auto simp add: zprime_def zprimel_def);

lemma zprimel_distrib2: "zprimel (h # t) ==> zprimel t";
by (auto simp add: zprime_def zprimel_def);

lemma aux [rule_format]: "zprimel (a # list) --> zprimel y --> nat a # natl list = natl y -->
a # list ~= y  --> natl list = natl y";
apply (induct y, force);
apply (clarify, auto);
proof-;
fix aa and lista;
assume "zprimel (a # list)" and "zprimel (aa # lista)" and "nat a = nat aa";
then have "0 <= a" and "0 <= aa";
by (auto simp add: zprimel_def zprime_def);
thus "a = aa" by (auto simp add: nat_pos_prop prems);
next;
fix aa and lista;
assume "zprimel (a # list)" and "zprimel (aa # lista)" and "natl list = natl lista";
then have "intl (natl list) = intl (natl lista)";
by (rule_tac x = "natl list" in intl_natl_prop, auto);
also have "intl (natl list) = list";
proof-;
from prems have "zprimel (a # list)"; by auto;
then have "zprimel list" by (rule zprimel_distrib2);
thus "intl (natl list) = list" by (rule intl_natl_prime);
qed;
also have "intl (natl lista) = lista";
proof-;
from prems have "zprimel (aa # lista)"; by auto;
then have "zprimel lista" by (rule zprimel_distrib2);
thus "intl (natl lista) = lista" by (rule intl_natl_prime);
qed;
finally show "list = lista" .;
qed;

lemma zprimel_natl_prop: "[| zprimel x; zprimel y; natl x = natl y |] ==> x = y";
proof-;
assume "zprimel x" and "zprimel y" and "natl x = natl y";
have "zprimel x & zprimel y & natl x = natl y --> x = y";
apply (induct x, induct y, auto);
apply (simp add: zprimel_def);
apply (rule aux, auto);
done;
with prems show "x = y" by auto;
qed;

lemma zprimel_conversion: "primel l = zprimel (intl l)";
apply (induct l);
apply (auto simp add: primel_def zprimel_def int_prime_prop);
done;

subsection {* Properties about zprod *}

lemma zprod_pos: "0 <= zprod(intl l)";
apply (induct l, auto);
proof-;
fix a and list;
assume "0 <= zprod (intl list)";
moreover have "0 <= int a" by auto;
ultimately show "0 <= int a * zprod (intl list)";
by (auto simp add: zero_le_mult_iff);
qed;

lemma zprod_conversion: "prod l = nat (zprod(intl l))";
apply (induct l);
apply (auto);
proof-;
fix a and list;
have "a * nat (zprod (intl list)) =  nat (int a) * nat (zprod (intl list))";
by (auto);
also have "... = nat (int a * zprod (intl list))";
by (auto simp add: nat_mult_distrib);
finally show "a * nat (zprod (intl list)) = nat (int a * zprod (intl list))".;
qed;

lemma zprodl_zprimel_pos [rule_format]: "zprimel pl --> 0 <= zprod (pl)";
apply (induct pl);
apply (auto simp add: zprimel_def zprime_def);
apply (auto simp add: zero_le_mult_iff);
done;

lemma zprodl_zprimel_gr_0 [rule_format]: "zprimel pl --> 0 < zprod (pl)";
apply (induct pl);
apply (auto simp add: zprimel_def zprime_def);
apply (auto simp add: zero_less_mult_iff);
done;

subsection {* Properties about znondec *}

lemma znondec_conversion: "nondec l = znondec (intl l)";
apply (induct l, auto);
apply (case_tac list, auto simp add: neq_Nil_conv);
apply (case_tac list, auto simp add: neq_Nil_conv);
apply (case_tac list, auto simp add: neq_Nil_conv);
apply (case_tac list, auto simp add: neq_Nil_conv);
done;

lemma znondec_distrib [rule_format]: "znondec(a # list) --> znondec(list)";
by (induct list, auto);

subsection {* Uniqueness *}

lemma temp: "(1::int) < p ==> ~(p dvd 1)";
apply (auto);
proof-;
assume "1 < p" and "p dvd 1";
moreover from prems have "0 < p" by auto;
ultimately have "nat p dvd nat 1";
by (rule_tac m = p in nat_int_dvd_prop, auto);
with dvd_1_iff_1 have "nat p = nat 1" by auto;
then have "int (nat p) = int (nat 1)" by auto;
with prems show "False" by (auto);
qed;

lemma zprime_zdvd_zmult_list [rule_format]:
"p : zprime ==> (p dvd zprod xs) --> (EX m. m : set xs & p dvd m)";
apply (induct xs);
apply (simp add: zprime_def);defer;
apply (clarsimp);
apply (drule_tac p = p and m = a in zprime_zdvd_zmult_better);
apply (force, force);
proof (clarify);
assume "1 < p" and "p dvd 1";
moreover from prems have "0 < p" by auto;
ultimately have "nat p dvd nat 1";
by (rule_tac m = p in nat_int_dvd_prop, auto);
with dvd_1_iff_1 have "nat p = nat 1" by auto;
then have "int (nat p) = int (nat 1)" by auto;
with prems show "False" by (auto);
qed;

lemma zprimes_eq: "[| p : zprime; q : zprime; p dvd q |] ==> p = q";
apply (auto simp add: zprime_def);
apply (drule_tac x = q in allE, auto);
apply (drule_tac x = p in allE, auto);
done;

lemma zprime_zdvd_eq: "[| zprimel (x # xs); zprimel ys; m : set ys; x dvd m |] ==> x = m";
apply (rule zprimes_eq);
apply (auto simp add: zprimel_distrib1);
apply (auto simp add: zprimel_def);
done;

lemma zfactor_unique: "[| zprimel (intl x); zprimel (intl y);
znondec (intl x); znondec (intl y);
zprod (intl x) = zprod (intl y) |] ==> x = y";
proof-;
assume "zprimel (intl x)" and "zprimel (intl y)" and
"znondec (intl x)" and "znondec (intl y)" and
"zprod (intl x) = zprod (intl y)";
then have "nat (zprod (intl y)) = nat (zprod (intl x))" by auto;
then have "primel x & primel y & prod x = prod y";
by (auto simp add: zprimel_conversion zprod_conversion);
with factor_unique have "x <~~> y" by auto;
moreover from prems have "nondec x" and "nondec y"
by (auto simp add: znondec_conversion);
moreover note perm_nondec_unique;
ultimately show "x = y" by auto;
qed;

subsection {* Unique Factorization into Prime Integers *}

lemma aux1: "1 < n ==> EX! l. zprimel (intl l) & znondec (intl l) & zprod (intl l) = n";
proof (auto);
assume "1 < n";
then have "Suc 0 < nat n" by (auto simp add: gr_1_prop);
with unique_prime_factorization have "EX! l. primel l & nondec l & prod l = nat n";
by (auto);
then have "EX l. primel l & nondec l & prod l = nat  n" by auto;
then show "EX l. zprimel (intl l) & znondec (intl l) & zprod (intl l) = n";
apply (auto simp add: zprimel_conversion zprod_conversion znondec_conversion);
apply (rule_tac x = l in exI, auto);
apply (insert prems, rule nat_pos_prop, auto simp add: zprod_pos);
done;
next;
fix l and y;
assume "zprimel (intl l)" and "zprimel (intl y)" and
"znondec (intl l)" and "znondec (intl y)" and
"zprod (intl y) = zprod (intl l)";
with zfactor_unique show "l = y"; by auto;
qed;

theorem unique_zprime_factorization: "1 < n ==> EX! l. zprimel l & znondec l & zprod l = n";
proof-;
assume "1 < n";
with aux1 have "EX! l. zprimel (intl l) & znondec (intl l) & zprod (intl l) = n";
by auto;
then show "EX! l. zprimel l & znondec l & zprod l = n";
apply (auto);
apply (rule_tac x = la and y = y in zprimel_natl_prop);
apply (auto);
apply (rule_tac x = "natl la" in zfactor_unique);
proof-;
fix la;
assume "zprimel la";
with intl_natl_prime have "intl (natl la) = la" by auto;
then show "zprimel (intl (natl la))" by auto;
next;
fix y;
assume "zprimel y";
with intl_natl_prime have "intl (natl y) = y" by auto;
then show "zprimel (intl (natl y))" by auto;
next;
fix la;
assume "zprimel la" and "znondec la";
with intl_natl_prime have "intl (natl la) = la" by auto;
then show "znondec (intl (natl la))" by auto;
next;
fix y;
assume "zprimel y" and "znondec y";
with intl_natl_prime have "intl (natl y) = y" by auto;
then show "znondec (intl (natl y))" by auto;
next;
fix l and la and y;
assume "zprimel la" and "zprimel y";
assume "zprod la = zprod (intl l)" and "zprod y = zprod (intl l)";
then have "zprod la = zprod y" by auto;
also have "la = intl (natl la)";
by (auto simp add: prems intl_natl_prime);
also have "y = intl (natl y)";
by (auto simp add: prems intl_natl_prime);
finally show "zprod (intl (natl la)) = zprod (intl (natl y))".;
qed;
qed;

end;
```

lemma gr_1_prop:

`  (1 < p) = (1 < nat p)`

lemma int_nat_dvd_prop:

`  (m dvd p) = (int m dvd int p)`

lemma nat_int_dvd_prop:

`  [| 0 < m; m dvd p |] ==> nat m dvd nat p`

lemma nat_prime_prop:

`  (p ∈ zprime) = (nat p ∈ prime)`

lemma int_prime_prop:

`  (int p ∈ zprime) = (p ∈ prime)`

### Properties about intl and natl

lemma intl_natl_prime:

`  zprimel x ==> intl (natl x) = x`

lemma intl_natl_prop:

`  x = y ==> intl x = intl y`

### Properties about zprimel

lemma zprimel_distrib1:

`  zprimel (h # t) ==> h ∈ zprime`

lemma zprimel_distrib2:

`  zprimel (h # t) ==> zprimel t`

lemma aux:

```  [| zprimel (a # list); zprimel y; nat a # natl list = natl y; a # list ≠ y |]
==> natl list = natl y```

lemma zprimel_natl_prop:

`  [| zprimel x; zprimel y; natl x = natl y |] ==> x = y`

lemma zprimel_conversion:

`  primel l = zprimel (intl l)`

### Properties about zprod

lemma zprod_pos:

`  0 ≤ zprod (intl l)`

lemma zprod_conversion:

`  prod l = nat (zprod (intl l))`

lemma zprodl_zprimel_pos:

`  zprimel pl ==> 0 ≤ zprod pl`

lemma zprodl_zprimel_gr_0:

`  zprimel pl ==> 0 < zprod pl`

### Properties about znondec

lemma znondec_conversion:

`  nondec l = znondec (intl l)`

lemma znondec_distrib:

`  znondec (a # list) ==> znondec list`

### Uniqueness

lemma temp:

`  1 < p ==> ¬ p dvd 1`

lemma zprime_zdvd_zmult_list:

`  [| p ∈ zprime; p dvd zprod xs |] ==> ∃m. m ∈ set xs ∧ p dvd m`

lemma zprimes_eq:

`  [| p ∈ zprime; q ∈ zprime; p dvd q |] ==> p = q`

lemma zprime_zdvd_eq:

`  [| zprimel (x # xs); zprimel ys; m ∈ set ys; x dvd m |] ==> x = m`

lemma zfactor_unique:

```  [| zprimel (intl x); zprimel (intl y); znondec (intl x); znondec (intl y);
zprod (intl x) = zprod (intl y) |]
==> x = y```

### Unique Factorization into Prime Integers

lemma aux1:

`  1 < n ==> ∃!l. zprimel (intl l) ∧ znondec (intl l) ∧ zprod (intl l) = n`

theorem unique_zprime_factorization:

`  1 < n ==> ∃!l. zprimel l ∧ znondec l ∧ zprod l = n`