# Theory PrimeFactorsList

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

theory PrimeFactorsList = IntFactorization:

```(*  Title:      PrimeFactorsList.thy
Author:     David Gray and Jeremy Avigad
*)

header {* Primes and multiplicity *}

theory PrimeFactorsList = IntFactorization:;

(********************************************)
(* Some initial sorting stuff for lists     *)
(* which will later be quite useful         *)
(********************************************)

consts
zinsert      :: "int => int list => int list"
zsort        :: "int list => int list";

primrec
"zinsert x []      = [x]"
"zinsert x (h # t) = (if (x <= h) then (x # (h#t))
else (h # (zinsert x t)))";
primrec
"zsort []      = []"
"zsort (h # t) = (zinsert h (zsort t))";

(* the actual stuff  *)

consts
pfactors     :: "int => int list"
numoccurs    :: "'a => 'a list => nat"
multiplicity :: "int => int => nat";

primrec
"numoccurs x []      = 0"
"numoccurs x (h # t) = (if (x = h) then 1 + (numoccurs x t)
else (numoccurs x t))";
defs
pfactors_def:     "pfactors n ==
(if (1 < n) then
(THE l. (zprimel l & znondec l & zprod l = n))
else [])"
multiplicity_def: "multiplicity p n == (numoccurs p (pfactors n))";

subsection {* Show that zinsert and zsort play well with others *}

lemma znondec_zinsert [rule_format]: "znondec (l) --> znondec (zinsert a (l))";
apply (induct l, force);
apply (case_tac list, auto);
done;

lemma znondec_zsort: "znondec (zsort l)";
by (induct l, auto simp add: znondec_zinsert);

lemma zprimel_zinsert [rule_format]: "zprimel l --> a : zprime --> zprimel (zinsert a (l))";
by (induct l, auto simp add: zprimel_def);

lemma zprimel_zsort [rule_format]: "zprimel l --> zprimel (zsort l)";
apply (induct l, force, clarify);
apply (frule zprimel_distrib2);
apply (drule zprimel_distrib1, clarify);
done;

lemma zprod_zinsert: "(a * zprod l) = (zprod (zinsert a l))";
by (induct l, auto);

lemma zprod_zsort: "zprod l = zprod (zsort l)";
by (induct l, auto simp add: zprod_zinsert);

lemma numoccurs_zinsert1: "numoccurs a l + 1 = numoccurs a (zinsert a l)";
by (induct l, auto);

lemma numoccurs_zinsert2: "a ~= p ==> numoccurs p l = numoccurs p (zinsert a l)";
by (induct l, auto);

lemma numoccurs_zsort: "numoccurs p l = numoccurs p (zsort l)";
apply (induct l, auto simp add: numoccurs_zinsert2);
apply (insert numoccurs_zinsert1, auto);
done;

lemma length_zinsert: "length l + 1 = length (zinsert a l)";
by (induct l, auto);

lemma length_zsort: "length l = length (zsort l)";
by (insert length_zinsert, induct l, auto);

subsection {* Some more intial properties for zprime and zprod *}

lemma zprimel_cons: "(zprimel lista & zprimel listb) = zprimel (lista @ listb)";

lemma aux1 [rule_format]: "zprod lista * zprod list = zprod (lista @ list) -->
zprod lista * (a * zprod list) = zprod (lista @ a # list)";
by (induct lista, auto);

lemma zprod_cons: "zprod lista * zprod listb = zprod (lista @ listb)";
by (induct listb, auto simp add: aux1);

lemma zprod_zprime_prop [rule_format]: "p:zprime ==> zprimel l --> p dvd (zprod l) --> p mem l";
proof (induct l, auto);
assume "p :zprime" and "p dvd 1";
thus "False";
apply (drule zdvd_bounds, auto);
done;
next;
fix a and list;
assume "zprimel (a # list)" and "~ zprimel list"
thus "p mem list" by (simp add: zprimel_def);
next;
fix a and list;
assume p1:"p:zprime" and " zprimel (a # list)" and "p dvd a * zprod list" and "~ p dvd zprod list";
with zprime_zdvd_zmult_better have p2:"p dvd a" by auto;
have p3: "a: zprime" by (insert prems, auto simp add: zprimel_def);
have "p = a";
apply (insert p1 p2 p3);
apply (rule_tac zprimes_eq, auto);
done;
moreover assume "a ~= p";
ultimately show "p mem list" by auto;
qed;

subsection {* Basic properties of numoccurs *}

lemma not_mem_numoccurs_eq_0 [rule_format]: "~(a mem list) --> numoccurs a list = 0";
by (induct list, auto);

lemma mem_numoccurs_gr_0 [rule_format]: "a mem list --> 0 < numoccurs a list";
by (induct list, auto);

lemma zprimel_not_zprime_numoccrs_eq_0 [rule_format]: "zprimel l --> p ~: zprime --> numoccurs p l = 0";
by (induct l, auto simp add: zprimel_def);

lemma aux2 [rule_format]: "numoccurs a (l1 @ list) = numoccurs a l1 + numoccurs a list
--> numoccurs a (l1 @ aa # list) = numoccurs a l1 + numoccurs a (aa # list)";
by (induct l1, auto);

lemma numoccurs_concat_zplus: "numoccurs a (l1 @ l2) = numoccurs a l1 + numoccurs a l2";
by (induct l2, auto simp add: aux2);

subsection {* More Properties for numoccurs *}

lemma aux3: "(ALL p. numoccurs p (a # l1) <= numoccurs p (a # l2)) =
(ALL p. numoccurs p l1 <= numoccurs p l2)";
by (auto);

lemma aux4 [rule_format]: "znondec (b # aa # list) --> znondec (b # list)";
by (case_tac list, auto);

lemma znondec_l_numoccurs [rule_format]: "a < b --> znondec (b # list) --> numoccurs a (b # list) = 0";
apply (induct list, force, clarify);
apply (frule aux4);
apply (drule mp, auto);
done;

lemma aux5: "[| znondec (b # lista); a < b;
ALL p. numoccurs p (b # lista) <= numoccurs p (a # listb);
ALL l1. znondec l1 & (ALL p. numoccurs p l1 <= numoccurs p listb) --> zprod l1 dvd zprod listb |]
==> zprod (b # lista) dvd zprod listb";
apply (drule_tac x = "b # lista" in spec);
apply (erule mp);
apply (rule conjI, force);
apply (rule allI);
apply (drule_tac x = p in spec);
apply (case_tac "p = a");
apply (drule znondec_l_numoccurs, auto);
done;

lemma aux6 [rule_format]: "znondec l2 -->
(ALL l1. (znondec l1 & (ALL p. (numoccurs p l1 <= numoccurs p l2))) -->
zprod l1 dvd zprod l2)";
apply (induct l2, clarify);
apply (case_tac l1, force, clarify);
apply (drule_tac x = a in spec, force, clarify);
apply (frule znondec_distrib);
apply (drule mp, force);
apply (case_tac l1, force, clarify);
apply (case_tac "aa = a", clarify);
apply (drule_tac x = "lista" in spec);
apply (drule znondec_distrib)+;
apply (clarsimp simp only: aux3, clarsimp);
apply (subgoal_tac "a dvd a");
apply (case_tac "a < aa");
apply (frule_tac a = a and b = aa and lista = lista and listb = list in aux5);
apply (force)+;
apply (subgoal_tac "aa < a");
apply (frule znondec_l_numoccurs, force);
apply (drule_tac x = aa in spec);
apply (force)+;
done;

lemma znondec_imp_zprod_zdvd: "[| znondec lista; znondec listb;
ALL p. numoccurs p lista <= numoccurs p listb |] ==>
zprod lista dvd zprod listb";

lemma zpower_numoccurs_zdvd_zprod: "p^(numoccurs p l) dvd zprod l";
by (induct l, auto simp add: dvd_def);

lemma aux7: "ALL k. p ^ k dvd zprod l --> zprimel l --> p:zprime --> k <= (numoccurs p l)";
apply (induct l, auto); defer;
apply (case_tac k, auto);defer;defer;
proof-;
fix k;
assume "p : zprime";
then have p1: "1 < p" by (auto simp add: zprime_def);
then have "0 <= p ^ k";
by (induct k, auto simp add: zero_le_mult_iff);
moreover assume "p^k dvd 1";
ultimately have "p ^ k = 1";
by (auto simp: ge_0_zdvd_1);
then show "k = 0";
apply (induct k);
apply (insert p1);
done;
next;
fix list; fix nat;
assume IH: "ALL k. p ^ k dvd zprod list --> zprimel list --> k <= numoccurs p list" and
p1: "p * p ^ nat dvd p * zprod list" and
p2: "zprimel (p # list)" and p3: "p : zprime";
have "p ^ nat dvd zprod list";
proof-;
from p3 have "p ~= 0" by (auto simp add: zprime_def);
with p1 show "p ^ nat dvd zprod list";
by (rule_tac a = p in ne_0_zdvd_prop, auto);
qed;
moreover from p2 have "zprimel list";
ultimately show "nat <= numoccurs p list";
next;
fix a; fix list; fix k;
assume IH: "ALL k. p ^ k dvd zprod list --> zprimel list --> k <= numoccurs p list" and
p1: "p ~= a" and p2: "p ^ k dvd a * zprod list" and
p3: "zprimel (a # list)" and p4: "p : zprime";
from p3 have "a:zprime" by (auto simp add: zprimel_def);
with p1 p4 have "~ p dvd a";
apply (drule_tac x = a in allE, force);
apply (drule_tac x = p in allE, auto);
done;
moreover note p4 p2;
ultimately have "p ^ k dvd zprod list";
apply (rule_tac p = p in zprime_zdvd_zpower);
done;
moreover from p3 have "zprimel list"
ultimately show "k <= numoccurs p list";
qed;

lemma zpower_zdvd_zprod_impl_numoccurs [rule_format]: "p ^ k dvd zprod l --> zprimel l --> p:zprime --> k <= (numoccurs p l)";

subsection {* A Few Useful Lemmas *}

lemma zprimel_zprod_eq_1_impl_empty [rule_format]: "zprimel l --> zprod l = 1 --> l = []";
apply (induct l);
apply (auto simp add: zprimel_def zprime_def pos_zmult_eq_1_iff);
done;

lemma zprimel_zprod_gr_1_impl_not_empty [rule_format]: "zprimel l --> 1 < zprod l --> l ~= []";
apply (induct l);
apply (auto simp add: zprimel_def zprime_def pos_zmult_eq_1_iff);
done;

subsection {* Basic Properties about pfactors (from Unique Factorization) *}

lemma pfactors_simp_prop: "[|zprimel l; znondec l; zprod l = n |] ==> pfactors n = l";
apply (rule the1_equality);
apply (frule zprodl_zprimel_gr_0);
apply (case_tac "zprod l = 1");
apply (auto simp add: zprimel_zprod_eq_1_impl_empty [THEN sym]);
done;

lemma pfactors_fundamental_prop: "1 < n ==> zprimel (pfactors n) & znondec (pfactors n) &
zprod (pfactors n) = n";
apply (rule theI', drule unique_zprime_factorization);
apply (auto);
done;

lemma pfactors_zprimel: "zprimel (pfactors n)";
apply (case_tac "1 < n");
apply (auto simp add: zprimel_def pfactors_def);
done;

lemma pfactors_znondec: "znondec(pfactors n)";
apply (case_tac "1 < n");
done;

lemma pfactors_zprod: "1 <= n ==> zprod (pfactors n) = n";
apply (case_tac "1 < n");
done;

lemma pfactors_le_1: "n <= 1 ==> pfactors n = []";

lemma pfactors_gr_1: "1 < n ==> pfactors n ~= []";
proof-;
assume "1 < n";
also have "n = zprod( pfactors n)";
by (insert prems, auto simp add: pfactors_zprod);
finally have "1 < zprod( pfactors n)" .;
moreover have "zprimel (pfactors n)";
ultimately show ?thesis;
qed;

lemmas pfactors_ac = pfactors_le_1 pfactors_gr_1 pfactors_zprimel
pfactors_znondec pfactors_zprod;

subsection {* More Properties About pfactors *}

lemma pfactors_zprime: "p:zprime ==> pfactors p = [p]";
apply (rule the1_equality);
apply (drule unique_zprime_factorization);
apply (auto simp add: zprime_def zprimel_def);
done;

lemma length_pfactors_zprime: "p:zprime ==> length (pfactors p) = 1";

lemma zprod_zdvd [rule_format]: "x mem list --> x dvd (zprod list)";
by (induct list, auto simp add: dvd_def);

lemma mem_pfactors_imp_zdvd: "[| 1 <= n; p mem (pfactors n) |] ==> p dvd n";
proof-;
assume "1 <= n" and "p mem (pfactors n)";
then have "p dvd (zprod (pfactors n))";
also have "zprod (pfactors n) = n"
by (insert prems, auto simp add: pfactors_ac);
finally show ?thesis;.;
qed;

lemma zdvd_imp_mem_pfactors: "[| 1 <= n; p:zprime; p dvd n |] ==> p mem (pfactors n)";
proof-;
assume "1 <= n" and "p dvd n";
then have "p dvd zprod (pfactors n)";
moreover have "zprimel (pfactors n)";
by (insert prems, auto simp add: pfactors_zprimel);
moreover assume "p:zprime";
ultimately show "p mem (pfactors n)";
qed;

lemma pfactors_zsort_cons: "[| 1 <= a; 1 <= b |] ==> pfactors (a * b) = zsort((pfactors a) @ (pfactors b))";
apply (rule pfactors_simp_prop);
proof-;
have "zprimel (pfactors a)" and "zprimel (pfactors b)";
then have "zprimel (pfactors a @ pfactors b)";
by (insert zprimel_cons, auto);
thus "zprimel (zsort (pfactors a @ pfactors b))";
next;
show "znondec (zsort (pfactors a @ pfactors b))";
next;
assume "1 <= a" and "1 <= b";
have "zprod (zsort (pfactors a @ pfactors b)) = zprod (pfactors a @ pfactors b)";
by (auto simp add: zprod_zsort [THEN sym]);
also have "... = zprod (pfactors a) * zprod (pfactors b)";
by (auto simp add: zprod_cons [THEN sym]);
also have "zprod (pfactors a) = a";
by (insert prems, auto simp add: pfactors_ac);
also have "zprod (pfactors b) = b";
by (insert prems, auto simp add: pfactors_ac);
finally show "zprod (zsort (pfactors a @ pfactors b)) = a * b" by auto;
qed;

lemma pfactors_zmult_length: "[| 1 <= a; 1 <= b |] ==>
length (pfactors (a * b)) = length(pfactors a) + length(pfactors b)";
proof-;
assume "1 <= a" and "1 <= b";
then have "length(pfactors (a * b)) = length(zsort((pfactors a) @ (pfactors b)))";
also have "... = length(pfactors a @ pfactors b)";
by (insert length_zsort [of "pfactors a @ pfactors b"], auto);
also have "... = length (pfactors a) + length (pfactors b)";
by (auto);
finally show ?thesis by auto;
qed;

lemma pfactors_zprime_zmult_length: "[| 1 <= d; p:zprime|] ==>
length (pfactors (d * p)) = length(pfactors d) + 1";
proof-;
assume "1 <= d";
assume "p : zprime" then have "1 <= p" by (auto simp add: zprime_def);
then have "length (pfactors (d * p)) = length(pfactors d) + length(pfactors p)";
by (auto simp add: prems pfactors_zmult_length);
also have "length (pfactors p) = 1";
by (insert prems, auto simp add: pfactors_zprime);
finally show ?thesis by auto;
qed;

subsection {* Properties for Multiplicity *}

lemma multiplicity_base: "p :zprime ==> multiplicity p p = 1";
by (auto simp add: multiplicity_def pfactors_zprime);

lemma multiplicity_zmult_distrib: "[| 1 <= a; 1 <= b |] ==>
multiplicity p (a * b) = multiplicity p a + multiplicity p b";
proof-;
assume "1 <= a" and "1 <= b";
then have "pfactors (a * b) = zsort((pfactors a) @ (pfactors b))";
then have "numoccurs p (pfactors (a * b)) = numoccurs p (zsort((pfactors a) @ (pfactors b)))";
by (auto);
also have "... = numoccurs p ((pfactors a) @ (pfactors b))";
by (auto simp add: numoccurs_zsort [THEN sym]);
also have "... = numoccurs p (pfactors a) + numoccurs p (pfactors b)";
finally show "numoccurs p (pfactors (a * b)) = numoccurs p (pfactors a) + numoccurs p (pfactors b)"
by auto;
qed;

lemma multiplicity_zpower_prop: "p:zprime ==> multiplicity p (p^k) = k";
apply (induct k, simp add: multiplicity_def pfactors_def);
proof (auto);
fix n;
assume "multiplicity p (p ^ n) = n";
assume "p:zprime" then have p1: "1 <= p" by (auto simp add: zprime_def);
then have "1 <= p ^ n" by (auto simp add: ge_1_imp_zpower_ge_1);
then have "multiplicity p (p * p ^ n) = multiplicity p p + multiplicity p (p ^ n)";
by (insert p1 multiplicity_zmult_distrib, auto);
also have "multiplicity p p = 1";
by (insert prems multiplicity_base, auto);
also have "multiplicity p (p ^ n) = n" by (auto simp add: prems);
finally show "multiplicity p (p * p ^ n) = Suc n" by auto;
qed;

lemma multiplicity_zdvd: "p ^ (multiplicity p n) dvd n";
proof (case_tac "1 < n");
assume "1 < n";
have "p^(numoccurs p (pfactors n)) dvd zprod (pfactors n)";
by ( auto simp add:  zpower_numoccurs_zdvd_zprod);
also have "zprod (pfactors n) = n";
by (insert prems, auto simp add: pfactors_ac);
also have "numoccurs p (pfactors n) = multiplicity p n";
finally show ?thesis .;
next;
assume "~(1 < n)";
then have p1: "n <= 1" by auto;
have "p ^ 0 dvd n" by auto;
also have "0 = multiplicity p n";
by (insert p1, auto simp add: multiplicity_def pfactors_def);
finally show ?thesis .;
qed;

lemma not_zprime_multiplicity_eq_0: "[| p ~: zprime |] ==> multiplicity p n = 0";
apply (insert pfactors_zprimel [of n]);
apply (auto simp add: multiplicity_def zprimel_not_zprime_numoccrs_eq_0);
done;

lemma aux8: "k <= multiplicity p n ==> p ^ k dvd n";
proof-;
assume "k <= multiplicity p n";
then have "p ^ k dvd p ^ multiplicity p n";
moreover from  multiplicity_zdvd have "p ^ multiplicity p n dvd n"
by auto;
ultimately show ?thesis by (auto simp add: dvd_def);
qed;

lemma aux9: "[| 0 < n; p:zprime; p ^ k dvd n |]==> k <= multiplicity p n";
apply (case_tac "1 < n");
apply (rule zpower_zdvd_zprod_impl_numoccurs);
apply (subgoal_tac "n <= 1", auto);
apply (case_tac "n = 1", auto);
proof-;
assume "p:zprime"
then have p1: "1 < p" by (auto simp add: zprime_def);
then have "0 <= p ^ k";
by (induct k, auto simp add: zero_le_mult_iff);
moreover assume "p^k dvd 1";
ultimately have "p ^ k = 1";
by (auto simp: ge_0_zdvd_1);
then show "k = 0";
apply (induct k, insert p1);
done;
qed;

lemma multiplicity_zpower_zdvd: "[| 0 < n; p:zprime |] ==> (k <= multiplicity p n) = (p ^ k dvd n)";

lemma zdvd_zprime_imp_multiplicity_ge_1: "[| 0 < n; p dvd n; p:zprime |] ==> 1 <= multiplicity p n";
by (insert multiplicity_zpower_zdvd [of n p 1], auto);

lemma multiplicity_eq_1_imp_zdvd: "[| multiplicity p n = 1 |] ==> p dvd n";
apply (case_tac "0 < n");
proof-;
assume "multiplicity p n = 1";
then have "multiplicity p n ~= 0" by auto;
then have p1: "p : zprime";
by (insert not_zprime_multiplicity_eq_0 [of p n], auto);
moreover assume "0 < n";
moreover have "1 <= multiplicity p n" by (insert prems, auto);
ultimately have "(p ^ 1 dvd n)";
by (insert multiplicity_zpower_zdvd [of n p 1], auto);
thus ?thesis by auto;
next;
assume "multiplicity p n = 1" and "~ 0 < n";
thus ?thesis by (simp add: multiplicity_def pfactors_def);
qed;

lemma zdvd_imp_multiplicity_le: "[| 0 < n; m dvd n |] ==> ALL p. (multiplicity p m <= multiplicity p n)";
proof (clarify, case_tac "p : zprime");
fix p;
assume "m dvd n";
then have "p ^ (multiplicity p m) dvd m";
then have "p ^ (multiplicity p m) dvd n";
by (insert prems zdvd_trans [of "p ^ (multiplicity p m)" m n], auto);
moreover assume "p : zprime" and "0 < n";
ultimately show "(multiplicity p m <= multiplicity p n)";
by (insert multiplicity_zpower_zdvd [of n p "multiplicity p m"], auto);
next;
fix p;
assume "p ~: zprime";
thus "multiplicity p m <= multiplicity p n";
qed;

lemma multiplicity_le_imp_zdvd: "[| 0 < m; 0 < n;
ALL p. (multiplicity p m <= multiplicity p n) |] ==>
m dvd n";
proof-;
assume "0 < m" and "0 < n";
assume "ALL p. (multiplicity p m <= multiplicity p n)";
then have "ALL p. (numoccurs p (pfactors m) <= numoccurs p (pfactors n))"
moreover have "znondec (pfactors m)" by (auto simp add: pfactors_ac);
moreover have "znondec (pfactors n)" by (auto simp add: pfactors_ac);
moreover note znondec_imp_zprod_zdvd;
ultimately have "zprod (pfactors m) dvd zprod (pfactors n)" by auto;
also have "zprod (pfactors m) = m" by (insert prems, auto simp add: pfactors_ac);
also have "zprod (pfactors n) = n" by (insert prems, auto simp add: pfactors_ac);
finally show ?thesis .;
qed;

(* A useful lemma *)

lemma p_neq_q_impl_nzdvd: "[| p ~= q; p:zprime; q:zprime |] ==> ~(p dvd q)";
assume "1 < p" and "p dvd q" and "ALL m. 0 <= m & m dvd q --> m = 1 | m = q";
then have "p = q" by (drule_tac x = p in allE, auto);
moreover assume "p ~= q";
ultimately show False by auto;
qed;

(* Another useful lemma *)

lemma multiplicity_p_1_eq_0: "multiplicity p 1 = 0";
by (auto simp add: multiplicity_def pfactors_def);

(* This should replace zdvd_zprime_imp_multiplicity_ge_1  in PrimeFactorsList *)

lemma zdvd_zprime_multiplicity_ge_1: "[| 0 < n; p:zprime |] ==> (p dvd n) = (1 <= multiplicity p n)";
by (insert multiplicity_zpower_zdvd [of n p 1], auto);

(* Now follow J's notes -- more or less... *)

lemma finite_prime_divisors: "0 < n ==> finite {p. p:zprime & p dvd n}";
proof-;
assume "0 < n";
then have "{p. p:zprime & p dvd n} <= {0..n}";
apply (frule zdvd_bounds, auto);
done;
moreover have "finite {0..n}" by auto;
ultimately show ?thesis by (auto simp add: finite_subset);
qed;

lemma zdvd_imp_m_eq_n: "[| (0::int) < m; 0 < n; m dvd n; n dvd m |] ==> m = n";
proof-;
fix k and ka;
assume "0 < m" and "0 < m * k";
then have "0 < k" by (elim zero_less_mult_pos);
moreover assume "k * ka = 1";
ultimately show "k = 1" by (auto simp add: pos_zmult_eq_1_iff);
qed;

lemma multiplicity_imp_m_eq_n: "[| (0::int) < m; 0 < n;
ALL p. (multiplicity p m) = (multiplicity p n) |] ==> m = n";
proof-;
assume "ALL p. multiplicity p m = multiplicity p n"
then have "ALL p. multiplicity p m <= multiplicity p n" and
"ALL p. multiplicity p n <= multiplicity p m" by auto;
moreover assume "0 < m" and "0 < n";
ultimately have "m dvd n" and "n dvd m" by (auto simp add: multiplicity_le_imp_zdvd);
with prems show "m = n" by (auto simp add: zdvd_imp_m_eq_n);
qed;

lemma aux2: "finite F ==> ALL a:F. 0 < a ==> (0::int) < setprod (%q. q ^ g q x) (F::int set)";
by (induct F rule: finite_induct, auto simp add: mult_pos zero_less_power);

lemma aux3: "[| finite A; 0 < p; ALL a:A. 0 < a |] ==>
multiplicity p (setprod (%q. q ^ (g q x)) A) =
setsum (%q. multiplicity p (q ^ (g q x))) A";
apply (induct A rule: finite_induct, auto simp add: multiplicity_p_1_eq_0);
proof-;
fix F and xa;
assume "finite (F::int set)" and "ALL x:F. 0 < x" and "(0::int) < xa";
then have "0 < xa ^ (g xa x)" by (auto simp add: zero_less_power);
moreover have "0 < setprod (%q. q ^ g q x) F";
by (insert prems, auto simp add: aux2);
ultimately have "1 <= xa ^ (g xa x)" and "1 <= setprod (%q. q ^ g q x) F" by auto;
then have "multiplicity p (xa ^ g xa x * setprod (%q. q ^ g q x) F) =
multiplicity p (xa ^ g xa x) + multiplicity p (setprod (%q. q ^ g q x) F)";
by (rule multiplicity_zmult_distrib);
also assume "multiplicity p (setprod (%q. q ^ g q x) F) = (∑q:F. multiplicity p (q ^ g q x))";
finally show "multiplicity p (xa ^ g xa x * setprod (%q. q ^ g q x) F) =
multiplicity p (xa ^ g xa x) + (∑q:F. multiplicity p (q ^ g q x))" .;
qed;

lemma multiplicity_zpower_zmult: "0 < x ==> (multiplicity p (x ^ n)) = n * (multiplicity p x)";
apply (induct n, auto simp add: multiplicity_p_1_eq_0);
proof-;
fix n;
assume "0 < x";
then have "0 < x ^ n" by (induct n, auto simp add: mult_pos);
then have "multiplicity p (x * x ^ n) = (multiplicity p x) + (multiplicity p (x^n))";
by (insert prems, auto simp add: multiplicity_zmult_distrib);
also assume "multiplicity p (x ^ n) = n * multiplicity p x";
finally show "multiplicity p (x * x ^ n) = multiplicity p x + n * multiplicity p x".;
qed;

lemma p_neq_q_multiplicity_eq_0: "[| q ~= p; p:zprime; q:zprime |] ==> multiplicity p q = 0";
proof-;
assume "q ~= p" and "p : zprime" and "q : zprime";
then have "~(p dvd q)" by (auto simp add: p_neq_q_impl_nzdvd);
moreover have "0 < q" by (insert prems, auto simp add: zprime_def);
ultimately have "~(1 <= multiplicity p q)";
by (auto simp add: prems zdvd_zprime_multiplicity_ge_1);
thus ?thesis by auto;
qed;

lemma p_neq_q_multiplicity_zpower_eq_0: "[| q ~= p; p:zprime; q:zprime |] ==> multiplicity p (q ^ n) = 0";
proof-;
assume "q ~= p" and "p:zprime" and "q:zprime";
then have "0 < q" by (auto simp add: zprime_def);
then have "(multiplicity p (q ^ n)) = n * (multiplicity p q)"
also have "multiplicity p q = 0" by (insert prems, auto simp add: p_neq_q_multiplicity_eq_0);
finally show ?thesis by auto;
qed;

lemma finite_A_setsum_eq_0: "finite A ==> ALL x:A. f x = 0 ==> setsum f A = (0::int)";
by (induct A rule: finite_induct, auto);

lemma multiplicity_setprod_eq_0: "[| finite A; ALL p:A. (p:zprime); p ~: A; p:zprime |] ==>
multiplicity p (setprod (%q. q ^ (g q x)) A) = 0";
proof-;
assume "finite A" and "ALL p:A. p : zprime" and "p ~:A" and "p:zprime";
moreover have "0 < p" and "ALL p:A. 0 < p" by (insert prems, auto simp add: zprime_def);
ultimately have "multiplicity p (setprod (%q. q ^ (g q x)) A) =
setsum (%q. multiplicity p (q ^ (g q x))) A";
also have "... = 0";
apply (insert prems, auto simp add: finite_A_setsum_eq_0);
apply (rule p_neq_q_multiplicity_zpower_eq_0, auto);
done;
finally show ?thesis .;
qed;

lemma multiplicity_zdvd_setprod_eq_n: "[| (0::int) < n; q:zprime; q dvd n |] ==>
multiplicity q (setprod (%p. p^(multiplicity p n)) {p. p: zprime & p dvd n}) =
multiplicity q n";
proof-;
assume "0 < n" and "q:zprime" and "q dvd n";
have p1: "finite {p. p: zprime & p dvd n & q ~= p}";
apply (insert finite_prime_divisors [of n] prems);
apply (subgoal_tac "{p. p: zprime & p dvd n & q ~= p} <= {p. p:zprime & p dvd n}");
done;
have "{p. p:zprime & p dvd n} = insert q {p . p:zprime & p dvd n & q ~= p}";
by (insert prems, auto);
then have "multiplicity q (setprod (%p. p^(multiplicity p n)) {p. p: zprime & p dvd n}) =
multiplicity q (setprod (%p. p^(multiplicity p n)) (insert q {p. p: zprime & p dvd n & q ~= p}))";
by auto;
also have "(setprod (%p. p^(multiplicity p n)) (insert q {p. p: zprime & p dvd n & q ~= p})) =
(%p. p^(multiplicity p n)) q * setprod (%p. p^(multiplicity p n)) {p. p: zprime & p dvd n & q ~= p}";
proof-;
note p1;
moreover have "q ~: {p. p: zprime & p dvd n & q ~= p}" by auto;
ultimately show ?thesis by (auto simp add: setprod_insert);
qed;
finally have "multiplicity q (setprod (%p. p ^ multiplicity p n) {p. p : zprime & p dvd n}) =
multiplicity q (q ^ multiplicity q n *
setprod (%p. p ^ multiplicity p n) {p. p : zprime & p dvd n & q ~= p})" .;
also have "... = (multiplicity q (q^(multiplicity q n))) +
(multiplicity q (setprod (%p. p^(multiplicity p n)) {p. p: zprime & p dvd n & q ~= p}))";
proof-;
have p2: "ALL p:{p. p : zprime & p dvd n & q ~= p}. 0 < p"; by (auto simp add: zprime_def);
have "0 < q" by (insert prems, auto simp add: zprime_def);
then have "0 < q ^ multiplicity q n" by (auto simp add: zero_less_power);
moreover have "0 < setprod (%p. p ^ multiplicity p n) {p. p : zprime & p dvd n & q ~= p}";
apply (insert p1 p2 prems);
apply (induct "{p. p : zprime & p dvd n & q ~= p}" rule: finite_induct);
apply (auto simp add: mult_pos zero_less_power);
done;
ultimately show ?thesis by (auto simp add: multiplicity_zmult_distrib);
qed;
also have "(multiplicity q (setprod (%p. p^(multiplicity p n)) {p. p: zprime & p dvd n & q ~= p})) = 0";
proof-;
note p1;
moreover have "ALL p:{p. p : zprime & p dvd n & q ~= p}. (p:zprime)" by auto;
moreover have "q ~: {p. p : zprime & p dvd n & q ~= p}" by auto;
moreover have "q:zprime" by (insert prems, auto);
ultimately show ?thesis by (rule   multiplicity_setprod_eq_0);
qed;
also have "(multiplicity q (q^(multiplicity q n))) = multiplicity q n";
by (insert prems, auto simp add: multiplicity_zpower_prop);
finally show ?thesis by auto;
qed;

lemma multiplicity_nzdvd_setprod_eq_n: "[| 0 < n; q: zprime; ~(q dvd n) |] ==>
multiplicity q (setprod (%p. p ^ (multiplicity p n)) {p. p:zprime & p dvd n}) =
multiplicity q n";
proof-;
assume "0 < n" and "q: zprime" and "~(q dvd n)";
then have "multiplicity q n = 0" by (insert zdvd_zprime_multiplicity_ge_1, auto);
moreover have "multiplicity q (setprod (%p. p ^ (multiplicity p n)) {p. p:zprime & p dvd n}) = 0";
proof-;
have "finite {p. p:zprime & p dvd n}" by (insert prems, auto simp add: finite_prime_divisors);
moreover have "ALL p:{p. p:zprime & p dvd n}. p:zprime" by (auto);
moreover have "q ~: {p. p:zprime & p dvd n}" by (auto simp add: prems);
moreover note prems;
ultimately show ?thesis;
apply (rule_tac  multiplicity_setprod_eq_0);
apply (force)+;
done;
qed;
ultimately show ?thesis by auto;
qed;

lemma multiplicity_setprod_eq_n: "[| 0 < n; q: zprime |] ==>
multiplicity q (setprod (%p. p ^ (multiplicity p n)) {p. p:zprime & p dvd n}) =
multiplicity q n";
apply (case_tac "q dvd n");
apply (auto simp add: multiplicity_nzdvd_setprod_eq_n multiplicity_zdvd_setprod_eq_n);
done;

theorem n_eq_setprod_multiplicity: "0 < n ==> n = setprod (%p. p ^(multiplicity p n)) {p. p:zprime & p dvd n}";
apply (rule multiplicity_imp_m_eq_n, auto);
apply (rule aux2, auto simp add: finite_prime_divisors);
apply (case_tac "p : zprime");
apply (auto simp add: multiplicity_setprod_eq_n [THEN sym] not_zprime_multiplicity_eq_0);
done;

end;
```

### Show that zinsert and zsort play well with others

lemma znondec_zinsert:

`  znondec l ==> znondec (zinsert a l)`

lemma znondec_zsort:

`  znondec (zsort l)`

lemma zprimel_zinsert:

`  [| zprimel l; a ∈ zprime |] ==> zprimel (zinsert a l)`

lemma zprimel_zsort:

`  zprimel l ==> zprimel (zsort l)`

lemma zprod_zinsert:

`  a * zprod l = zprod (zinsert a l)`

lemma zprod_zsort:

`  zprod l = zprod (zsort l)`

lemma numoccurs_zinsert1:

`  numoccurs a l + 1 = numoccurs a (zinsert a l)`

lemma numoccurs_zinsert2:

`  a ≠ p ==> numoccurs p l = numoccurs p (zinsert a l)`

lemma numoccurs_zsort:

`  numoccurs p l = numoccurs p (zsort l)`

lemma length_zinsert:

`  length l + 1 = length (zinsert a l)`

lemma length_zsort:

`  length l = length (zsort l)`

### Some more intial properties for zprime and zprod

lemma zprimel_cons:

`  (zprimel lista ∧ zprimel listb) = zprimel (lista @ listb)`

lemma aux1:

```  zprod lista * zprod list = zprod (lista @ list)
==> zprod lista * (a * zprod list) = zprod (lista @ a # list)```

lemma zprod_cons:

`  zprod lista * zprod listb = zprod (lista @ listb)`

lemma zprod_zprime_prop:

`  [| p ∈ zprime; zprimel l; p dvd zprod l |] ==> p mem l`

### Basic properties of numoccurs

lemma not_mem_numoccurs_eq_0:

`  ¬ a mem list ==> numoccurs a list = 0`

lemma mem_numoccurs_gr_0:

`  a mem list ==> 0 < numoccurs a list`

lemma zprimel_not_zprime_numoccrs_eq_0:

`  [| zprimel l; p ∉ zprime |] ==> numoccurs p l = 0`

lemma aux2:

```  numoccurs a (l1 @ list) = numoccurs a l1 + numoccurs a list
==> numoccurs a (l1 @ aa # list) = numoccurs a l1 + numoccurs a (aa # list)```

lemma numoccurs_concat_zplus:

`  numoccurs a (l1 @ l2) = numoccurs a l1 + numoccurs a l2`

### More Properties for numoccurs

lemma aux3:

```  (∀p. numoccurs p (a # l1) ≤ numoccurs p (a # l2)) =
(∀p. numoccurs p l1 ≤ numoccurs p l2)```

lemma aux4:

`  znondec (b # aa # list) ==> znondec (b # list)`

lemma znondec_l_numoccurs:

`  [| a < b; znondec (b # list) |] ==> numoccurs a (b # list) = 0`

lemma aux5:

```  [| znondec (b # lista); a < b;
∀p. numoccurs p (b # lista) ≤ numoccurs p (a # listb);
∀l1. znondec l1 ∧ (∀p. numoccurs p l1 ≤ numoccurs p listb) -->
zprod l1 dvd zprod listb |]
==> zprod (b # lista) dvd zprod listb```

lemma aux6:

```  [| znondec l2; znondec l1 ∧ (∀p. numoccurs p l1 ≤ numoccurs p l2) |]
==> zprod l1 dvd zprod l2```

lemma znondec_imp_zprod_zdvd:

```  [| znondec lista; znondec listb; ∀p. numoccurs p lista ≤ numoccurs p listb |]
==> zprod lista dvd zprod listb```

lemma zpower_numoccurs_zdvd_zprod:

`  p ^ numoccurs p l dvd zprod l`

lemma aux7:

`  ∀k. p ^ k dvd zprod l --> zprimel l --> p ∈ zprime --> k ≤ numoccurs p l`

lemma zpower_zdvd_zprod_impl_numoccurs:

`  [| p ^ k dvd zprod l; zprimel l; p ∈ zprime |] ==> k ≤ numoccurs p l`

### A Few Useful Lemmas

lemma zprimel_zprod_eq_1_impl_empty:

`  [| zprimel l; zprod l = 1 |] ==> l = []`

lemma zprimel_zprod_gr_1_impl_not_empty:

`  [| zprimel l; 1 < zprod l |] ==> l ≠ []`

### Basic Properties about pfactors (from Unique Factorization)

lemma pfactors_simp_prop:

`  [| zprimel l; znondec l; zprod l = n |] ==> pfactors n = l`

lemma pfactors_fundamental_prop:

`  1 < n ==> zprimel (pfactors n) ∧ znondec (pfactors n) ∧ zprod (pfactors n) = n`

lemma pfactors_zprimel:

`  zprimel (pfactors n)`

lemma pfactors_znondec:

`  znondec (pfactors n)`

lemma pfactors_zprod:

`  1 ≤ n ==> zprod (pfactors n) = n`

lemma pfactors_le_1:

`  n ≤ 1 ==> pfactors n = []`

lemma pfactors_gr_1:

`  1 < n ==> pfactors n ≠ []`

lemmas pfactors_ac:

`  n ≤ 1 ==> pfactors n = []`
`  1 < n ==> pfactors n ≠ []`
`  zprimel (pfactors n)`
`  znondec (pfactors n)`
`  1 ≤ n ==> zprod (pfactors n) = n`

lemma pfactors_zprime:

`  p ∈ zprime ==> pfactors p = [p]`

lemma length_pfactors_zprime:

`  p ∈ zprime ==> length (pfactors p) = 1`

lemma zprod_zdvd:

`  x mem list ==> x dvd zprod list`

lemma mem_pfactors_imp_zdvd:

`  [| 1 ≤ n; p mem pfactors n |] ==> p dvd n`

lemma zdvd_imp_mem_pfactors:

`  [| 1 ≤ n; p ∈ zprime; p dvd n |] ==> p mem pfactors n`

lemma pfactors_zsort_cons:

`  [| 1 ≤ a; 1 ≤ b |] ==> pfactors (a * b) = zsort (pfactors a @ pfactors b)`

lemma pfactors_zmult_length:

```  [| 1 ≤ a; 1 ≤ b |]
==> length (pfactors (a * b)) = length (pfactors a) + length (pfactors b)```

lemma pfactors_zprime_zmult_length:

`  [| 1 ≤ d; p ∈ zprime |] ==> length (pfactors (d * p)) = length (pfactors d) + 1`

### Properties for Multiplicity

lemma multiplicity_base:

`  p ∈ zprime ==> multiplicity p p = 1`

lemma multiplicity_zmult_distrib:

```  [| 1 ≤ a; 1 ≤ b |]
==> multiplicity p (a * b) = multiplicity p a + multiplicity p b```

lemma multiplicity_zpower_prop:

`  p ∈ zprime ==> multiplicity p (p ^ k) = k`

lemma multiplicity_zdvd:

`  p ^ multiplicity p n dvd n`

lemma not_zprime_multiplicity_eq_0:

`  p ∉ zprime ==> multiplicity p n = 0`

lemma aux8:

`  k ≤ multiplicity p n ==> p ^ k dvd n`

lemma aux9:

`  [| 0 < n; p ∈ zprime; p ^ k dvd n |] ==> k ≤ multiplicity p n`

lemma multiplicity_zpower_zdvd:

`  [| 0 < n; p ∈ zprime |] ==> (k ≤ multiplicity p n) = (p ^ k dvd n)`

lemma zdvd_zprime_imp_multiplicity_ge_1:

`  [| 0 < n; p dvd n; p ∈ zprime |] ==> 1 ≤ multiplicity p n`

lemma multiplicity_eq_1_imp_zdvd:

`  multiplicity p n = 1 ==> p dvd n`

lemma zdvd_imp_multiplicity_le:

`  [| 0 < n; m dvd n |] ==> ∀p. multiplicity p m ≤ multiplicity p n`

lemma multiplicity_le_imp_zdvd:

`  [| 0 < m; 0 < n; ∀p. multiplicity p m ≤ multiplicity p n |] ==> m dvd n`

lemma p_neq_q_impl_nzdvd:

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

lemma multiplicity_p_1_eq_0:

`  multiplicity p 1 = 0`

lemma zdvd_zprime_multiplicity_ge_1:

`  [| 0 < n; p ∈ zprime |] ==> (p dvd n) = (1 ≤ multiplicity p n)`

lemma finite_prime_divisors:

`  0 < n ==> finite {p. p ∈ zprime ∧ p dvd n}`

lemma zdvd_imp_m_eq_n:

`  [| 0 < m; 0 < n; m dvd n; n dvd m |] ==> m = n`

lemma multiplicity_imp_m_eq_n:

`  [| 0 < m; 0 < n; ∀p. multiplicity p m = multiplicity p n |] ==> m = n`

lemma aux2:

`  [| finite F; ∀a∈F. 0 < a |] ==> 0 < (∏q∈F. q ^ g q x)`

lemma aux3:

```  [| finite A; 0 < p; ∀a∈A. 0 < a |]
==> multiplicity p (∏q∈A. q ^ g q x) = (∑q∈A. multiplicity p (q ^ g q x))```

lemma multiplicity_zpower_zmult:

`  0 < x ==> multiplicity p (x ^ n) = n * multiplicity p x`

lemma p_neq_q_multiplicity_eq_0:

`  [| q ≠ p; p ∈ zprime; q ∈ zprime |] ==> multiplicity p q = 0`

lemma p_neq_q_multiplicity_zpower_eq_0:

`  [| q ≠ p; p ∈ zprime; q ∈ zprime |] ==> multiplicity p (q ^ n) = 0`

lemma finite_A_setsum_eq_0:

`  [| finite A; ∀x∈A. f x = 0 |] ==> setsum f A = 0`

lemma multiplicity_setprod_eq_0:

```  [| finite A; ∀p∈A. p ∈ zprime; p ∉ A; p ∈ zprime |]
==> multiplicity p (∏q∈A. q ^ g q x) = 0```

lemma multiplicity_zdvd_setprod_eq_n:

```  [| 0 < n; q ∈ zprime; q dvd n |]
==> multiplicity q (∏p∈{p. p ∈ zprime ∧ p dvd n}. p ^ multiplicity p n) =
multiplicity q n```

lemma multiplicity_nzdvd_setprod_eq_n:

```  [| 0 < n; q ∈ zprime; ¬ q dvd n |]
==> multiplicity q (∏p∈{p. p ∈ zprime ∧ p dvd n}. p ^ multiplicity p n) =
multiplicity q n```

lemma multiplicity_setprod_eq_n:

```  [| 0 < n; q ∈ zprime |]
==> multiplicity q (∏p∈{p. p ∈ zprime ∧ p dvd n}. p ^ multiplicity p n) =
multiplicity q n```

theorem n_eq_setprod_multiplicity:

`  0 < n ==> n = (∏p∈{p. p ∈ zprime ∧ p dvd n}. p ^ multiplicity p n)`