Theory IntFactorization

(*  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;