Theory PrimeFactorsList

(*  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);
  apply (auto simp add: zprimel_zinsert);
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)";
  by (auto simp add: zprimel_def);

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 (auto simp add: zprime_def); 
     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 (simp add: zdvd_zmult_mono, force);
  apply (case_tac "a < aa");
  apply (frule_tac a = a and b = aa and lista = lista and listb = list in aux5);
  apply (force)+;
  apply (simp add: zdvd_zmult);
  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";
  by (auto simp add: aux6);

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);
    apply (auto simp add:zmult_eq_1_iff);
  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";
    by (auto simp add: zprimel_def);
  ultimately show "nat <= numoccurs p list";
    by (auto simp add: IH);
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 (auto simp add: zprime_def);
    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);
    apply (auto simp add: zmult_ac);
  done;
  moreover from p3 have "zprimel list"
    by (auto simp add: zprimel_def);
  ultimately show "k <= numoccurs p list";
    by (auto simp add: IH);
qed;

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

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 (simp add: pfactors_def, auto);
  apply (rule the1_equality);
  apply (auto simp add: unique_zprime_factorization);
  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 (simp add: pfactors_def);
  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: pfactors_fundamental_prop);   
  apply (auto simp add: zprimel_def pfactors_def);
done;

lemma pfactors_znondec: "znondec(pfactors n)";
  apply (case_tac "1 < n");
  apply (auto simp add: pfactors_fundamental_prop);
  apply (auto simp add: pfactors_def);
done;

lemma pfactors_zprod: "1 <= n ==> zprod (pfactors n) = n";
  apply (case_tac "1 < n");
  apply (auto simp add: pfactors_fundamental_prop);
  apply (auto simp add: pfactors_def);
done;

lemma pfactors_le_1: "n <= 1 ==> pfactors n = []";
  by (auto simp add: pfactors_def);

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)";
    by( auto simp add: pfactors_zprimel);
  ultimately show ?thesis;
    by (auto simp add:zprimel_zprod_gr_1_impl_not_empty);
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 (auto simp add: pfactors_def);
  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";
  by (auto simp add: pfactors_zprime);

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))";
    by (auto simp add: zprod_zdvd);
  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)";
    by (auto simp add: pfactors_ac);
  moreover have "zprimel (pfactors n)";
    by (insert prems, auto simp add: pfactors_zprimel);
   moreover assume "p:zprime";
  ultimately show "p mem (pfactors n)";
    by (auto simp add: zprod_zprime_prop);
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)";
    by (auto simp add: pfactors_ac);
  then have "zprimel (pfactors a @ pfactors b)";
    by (insert zprimel_cons, auto);
  thus "zprimel (zsort (pfactors a @ pfactors b))";
    by (auto simp add: zprimel_zsort);
next;
  show "znondec (zsort (pfactors a @ pfactors b))";
    by (auto simp add: znondec_zsort);
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)))";
    by (auto simp add: pfactors_zsort_cons);
  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";
  apply (auto simp add: multiplicity_def);
proof-;
  assume "1 <= a" and "1 <= b";
  then have "pfactors (a * b) = zsort((pfactors a) @ (pfactors b))";
    by (auto simp add: pfactors_zsort_cons);
  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)";
    by (auto simp add: numoccurs_concat_zplus);
  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";
    by (auto simp add: multiplicity_def);
  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";
    by (auto simp add: le_imp_zpower_zdvd);
  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 (auto simp add: multiplicity_def);
  apply (case_tac "1 < n");
  apply (rule zpower_zdvd_zprod_impl_numoccurs);
  apply (auto simp add: pfactors_ac);
  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);
    apply (auto simp add:zmult_eq_1_iff);
  done;
qed;

lemma multiplicity_zpower_zdvd: "[| 0 < n; p:zprime |] ==> (k <= multiplicity p n) = (p ^ k dvd n)";
  by (auto simp add: aux8, simp add: aux9);

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";
    by (auto simp add: multiplicity_zdvd);
  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";
     by (auto simp add: not_zprime_multiplicity_eq_0);
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))"
    by (auto simp add: multiplicity_def);
  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)";
proof (auto simp add: zprime_def);
  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 (auto simp add: zprime_def);
    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";
  apply (auto simp add: dvd_def);
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)"
    by (auto simp add: multiplicity_zpower_zmult);
  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";
    by (auto simp add: aux3);
  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}");
      apply (auto simp add: finite_subset);
  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 (force simp add: zprime_def);
  apply (case_tac "p : zprime");
  apply (auto simp add: multiplicity_setprod_eq_n [THEN sym] not_zprime_multiplicity_eq_0);
done;

end;