Theory Radical

(*  Title:      Radical.thy
    Author:     David Gray
*)

header {* The radical function *}

theory Radical = PrimeFactorsList:;

consts
  pdivisors  :: "int => int list"
  rad        :: "int => int"
  squarefree :: "int => bool"
  subplist   :: "int list => int list => bool";


(* Should 0 and 1 be squarefree?? *)

defs
  pdivisors_def:   "pdivisors n  == remdups(pfactors n)"
  rad_def:         "rad n        == zprod(pdivisors n)"
  squarefree_def:  "squarefree n ==
                     (if (n <= 1) then True
                      else (distinct (pfactors n)))";

subsection {* Some Initial Properties Involving distinct *}

lemma distinct_numoccurs_le_1: "distinct list = (ALL p. (numoccurs p list) <= 1)";
proof-;
  have "distinct list --> (ALL p. (numoccurs p list) <= 1)";
    by (induct list, auto simp add: not_mem_numoccurs_eq_0 set_mem_eq);
  moreover have  "~(distinct list) --> ~(ALL p. (numoccurs p list <= 1)) ";
    apply (induct list);
    apply (auto simp add: mem_numoccurs_gr_0 set_mem_eq);
    apply (rule_tac x = p in exI, auto);
  done;
  ultimately show ?thesis by auto;
qed;

subsection {* Some Initial Properties Involving remdups *}

lemma zprimel_remdups_prop [rule_format]: "zprimel l --> zprimel (remdups l)";
  by (auto simp add: zprimel_def);

lemma aux [rule_format]: "znondec (remdups list) --> znondec (a # list) --> znondec (remdups (a # list))";
  apply (induct_tac list, auto);
  apply (case_tac list, auto);
done;

lemma znondec_remdups_prop [rule_format]: "znondec l --> znondec (remdups l)";
  apply (induct_tac l, force, clarify);
  apply (subgoal_tac "znondec(remdups list)");
  apply (drule aux, force, force);
  apply (drule znondec_distrib, force);
done;

lemma not_empty_remdups: "(l ~= []) = (remdups(l) ~= [])";
  by (induct l, auto);

lemma zprimel_zprod_ge_1 [rule_format]: "zprimel pl --> 1 <= zprod (remdups (pl))";
  apply (induct pl, auto simp add: zprimel_def zprime_def);
proof-;
  fix a and list;
  assume "1 < (a::int)" and "1 <= zprod (remdups list)";
  then have b: "1 <= a" by auto;
  from b have c: "0 <= a"; by arith;
  have "1 * 1 <= a * zprod (remdups list)";
    apply (rule mult_mono);
    by (auto simp add: prems b c);
  thus "1 <= a * zprod (remdups list)" by auto;
qed;

lemma pfactors_zprod_ge_1: "1 <= zprod (remdups (pfactors n))";
  apply (rule_tac zprimel_zprod_ge_1);
  apply (auto simp add: pfactors_ac);
done;

lemma zprimel_zprod_le [rule_format]: "zprimel pl --> zprod (remdups (pl)) <= zprod (pl)";
proof (induct pl, auto);
  fix a and list;
  assume "~ zprimel list" and "a : set list" and "zprimel (a # list)";
  thus "zprod (remdups list) <= a * zprod list" by (auto simp add: zprimel_def);
next;
  fix a and list;
  assume "~ zprimel list" and "a ~: set list" and "zprimel (a # list)";
  thus "a * zprod (remdups list) <= a * zprod list" by (auto simp add: zprimel_def);
next;
  fix a and list;
  assume "zprod (remdups list) <= zprod list" and "zprimel (a # list)";
  then have "zprod (remdups list) * 1 <= zprod list * a"
    apply (intro mult_mono);
    apply (auto simp add: zprimel_def zprime_def zprodl_zprimel_pos);
  done;
  also have "zprod (remdups list) * 1 = zprod (remdups list)" by auto;
  also have "zprod list * a = a * zprod list" by auto;
  finally show "zprod (remdups list) <= a * zprod list".;
next;
  fix a and list;
  assume "zprod (remdups list) <= zprod list" and "a ~: set list" and "zprimel (a # list)";
  thus "a * zprod (remdups list) <= a * zprod list"
    by (auto simp add: zprimel_def zprime_def mult_left_mono);
qed;

lemma pfactors_zprod_le: "zprod (remdups (pfactors n)) <= zprod (pfactors n)";
  apply (rule_tac zprimel_zprod_le);
  apply (auto simp add: pfactors_ac);
done;

lemma numoccurs_remdups: "ALL p. numoccurs p (remdups list) <= numoccurs p list";
  apply (induct list, auto);
  apply (drule_tac x = a in spec, auto);
done;

subsection {* Properties about pdivisors *}

lemma pdivisors_zprimel: "zprimel (pdivisors n)";
  apply (insert pfactors_zprimel [of n]);
  apply (drule zprimel_remdups_prop);
  apply (auto simp add: pdivisors_def);
done;

lemma pdivisors_znondec: "znondec (pdivisors n)";
  apply (insert pfactors_znondec [of n]);
  apply (drule znondec_remdups_prop);
  apply (auto simp add: pdivisors_def);
done;

lemma pdivisors_le_1: "n <= 1 ==> pdivisors n = []";
  by (auto simp add: pdivisors_def pfactors_def);

lemma pdivisors_gr_1: "1 < n ==> pdivisors n ~= []";
  apply (drule pfactors_gr_1);
  apply (auto simp add: pdivisors_def); 
  apply (auto simp add: not_empty_remdups);
done;

lemmas pdivisors_ac = pdivisors_le_1 pdivisors_gr_1 
                      pdivisors_znondec pdivisors_zprimel;

subsection {* Properties about rad *}

lemma le_1_rad_prop: "n <= 1 ==> rad (n) = 1";
  by (auto simp add: rad_def pfactors_def pdivisors_def);

lemma rad_max: "1 < n ==> rad n <= n";
proof-;
  assume "1 < n";
  note pfactors_zprod_le;
  also have "zprod (remdups (pfactors n)) = rad n";
    by (auto simp add: rad_def pdivisors_def);
  also have "zprod (pfactors n) = n";
    by (insert prems, auto simp add: pfactors_ac);
  finally show ?thesis .;
qed;

lemma rad_min_gre_1:"1 <= n ==> 1 <= rad n";
proof-;
  assume "1 <= n";
  note pfactors_zprod_ge_1;
  also have "zprod (remdups (pfactors n)) = rad n";
    by (auto simp add: rad_def pdivisors_def);
  finally show "1 <= rad n" by auto;
qed;

lemma rad_min_gr_1:"1 < n ==> 1 < rad n";
proof-;
  assume "1 < n";
  then have "1 <= rad n" by (auto simp add: rad_min_gre_1);
  moreover have "1 ~= rad n";
  proof;
    assume "1 = rad n";
    then have "zprod( pdivisors n) = 1";
      by (auto simp add: rad_def);
    moreover have "zprimel (pdivisors n)";
      by (auto simp add: pdivisors_ac);
    ultimately have "pdivisors n = []";
      by (auto simp add: zprimel_zprod_eq_1_impl_empty);
    moreover have "pdivisors n ~= []";
      by (insert prems, auto simp add: pdivisors_ac);
    ultimately show "False" by auto;
  qed;
  ultimately show ?thesis by auto;
qed;

lemma rad_prime: "p:zprime ==> rad (p) = p";
  by (auto simp add: rad_def pfactors_zprime pdivisors_def);

lemma pfactors_rad_eq_pdivisors: "pfactors (rad n) = pdivisors n";
  by (rule pfactors_simp_prop, auto simp add: pdivisors_ac rad_def);

lemma mem_pfactors_mem_pdivisors: "p mem (pfactors n) = p mem (pdivisors n)";
  by (auto simp add: pdivisors_def set_mem_eq);

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

lemma mem_pfactors_zdvd_rad: "[| 1 <= n; p mem (pfactors n) |] ==> p dvd (rad n)";
proof-;
  assume "1 <= n" and "p mem (pfactors n)";
  then have "p dvd (zprod(remdups(pfactors n)))";
    by (auto simp add: zprod_remdups_dvd);
  also have "zprod (remdups (pfactors n)) = rad n" 
    by (auto simp add: rad_def pdivisors_def);
  finally show ?thesis .;
qed;

lemma mem_pdivisors_dvd_rad: "[| 1 <= n; p mem (pdivisors n) |] ==> p dvd rad(n)";
proof-;
  assume "1 <= n" and "p mem (pdivisors n)";
  then have "p dvd (zprod (pdivisors n))";
    by (auto simp add: zprod_zdvd);
  also have "zprod (pdivisors n) = rad n";
    by (auto simp add: prems rad_def);
  finally show ?thesis;.;
qed;

lemma dvd_rad_mem_pdivisors: "[| 1 <= n; p:zprime; p dvd rad(n) |] ==> 
                              p mem (pdivisors n)";
proof-;
  assume "1 <= n" and "p dvd rad(n)";
  then have "p dvd zprod (pdivisors n)";
    by (auto simp add: rad_def);
  moreover note pdivisors_ac;
  moreover assume "p:zprime";
  ultimately show "p mem (pdivisors n)";
    by (auto simp add: zprod_zprime_prop );
qed;

lemma zprime_zdvd_rad: "[| p:zprime; 1 <= n |] ==> (p dvd n) = (p dvd rad (n))";
proof;
  assume "p:zprime" and "1 <= n" and "p dvd n";
  then have "p mem (pfactors n)" by (auto simp add: zdvd_imp_mem_pfactors);
  thus "p dvd rad (n)" by (auto simp add: prems mem_pfactors_zdvd_rad);
next;
  assume "p:zprime" and "1 <= n" and "p dvd rad n";
  then have "p mem pdivisors n";
    by (auto simp add: dvd_rad_mem_pdivisors);
  then have "p mem pfactors n";
    by (auto simp add: mem_pfactors_mem_pdivisors);
  thus "p dvd n";
    by (insert prems, auto simp add: mem_pfactors_imp_zdvd);
qed;

lemma rad_squarefree: "1 <= n ==> squarefree (rad (n))";
  by (auto simp add: squarefree_def pfactors_rad_eq_pdivisors pdivisors_def);

lemma rad_multiplicity_le: "ALL p. multiplicity p (rad n) <= multiplicity p n";
  by (auto simp add: multiplicity_def pfactors_rad_eq_pdivisors 
                     pdivisors_def numoccurs_remdups);

lemma rad_zdvd: "1 <= n ==> rad (n) dvd n";
proof-;
  assume "1 <= n";
  have "ALL p. multiplicity p (rad n) <= multiplicity p n";
    by (auto simp add: rad_multiplicity_le);
  moreover have "1 <= rad n";
    by (auto simp add: prems rad_min_gre_1);
  moreover note multiplicity_le_imp_zdvd;
  ultimately show ?thesis by (insert prems, auto);
qed;

subsection {* Properties about squarefree *}

lemma squarefree_prop: "squarefree(n) = (ALL p. (multiplicity p n) <= 1)";
  apply (simp add: squarefree_def multiplicity_def);
  apply (auto simp add: distinct_numoccurs_le_1);
  apply (auto simp add: pfactors_def);
done;

lemma squarefree_zdvd_imp_zdvd_rad: "[| 1 <= m; 1 <= n; m dvd n; squarefree m |] ==> m dvd rad(n)";
proof-;
  assume "1 <= m" and "1 <= n";
  then have p1: "1 <= rad n" by (auto simp add: rad_min_gre_1);
  assume "m dvd n" and "squarefree m";
  then have "ALL p. (multiplicity p m <= multiplicity p (rad n))";
    apply (auto simp add: squarefree_prop);
    apply (drule_tac x = p in spec);
    apply (case_tac "multiplicity p m = 0", auto);
    apply (subgoal_tac "multiplicity p m = 1", auto);
  proof-;
    fix p;
    assume "m dvd n";
    assume "multiplicity p m = Suc 0";
    then have "multiplicity p m = 1" by auto;
    then have "p dvd m" by (auto simp add: multiplicity_eq_1_imp_zdvd);
    then have "p dvd n" by (insert prems zdvd_trans [of p m n], auto);
    moreover have p2: "p : zprime";
      by (insert prems not_zprime_multiplicity_eq_0 [of p m], auto);
    ultimately have "p dvd rad(n)";
      by (insert prems zprime_zdvd_rad [of p n], auto);
    then have "1 <= multiplicity p (rad n)";
      by (insert prems p1 p2 zdvd_zprime_imp_multiplicity_ge_1 [of "rad n" p], auto);
    thus "Suc 0 <= multiplicity p (rad n)" by auto;
  qed;
  thus ?thesis by (insert prems p1, auto simp add: multiplicity_le_imp_zdvd);
qed;

lemma squarefree_zdvd_impl_squarefree: "[| 0 < n; squarefree n; m dvd n |] ==> squarefree m";
proof-;
  assume "squarefree n" and "0 < n" and "m dvd n";
  then have "ALL p. (multiplicity p n) <= 1" by (auto simp add: squarefree_prop);
  moreover have "ALL p. (multiplicity p m <= multiplicity p n)";
    by (insert prems, auto simp add:  zdvd_imp_multiplicity_le);
  ultimately have "ALL p. (multiplicity p m <= 1)"
    apply (clarify);
    apply (drule_tac x = p in spec)+;
    apply (arith);
  done;
  thus "squarefree m" by (auto simp add: squarefree_prop);
qed;

lemma squarefree_distrib1: "[| 0 < x; 0 < y; squarefree(x * y) |] ==>
                            squarefree (x)";
proof-;
  assume "0 < x" and "0 < y"; 
  then have "0 < x * y" by (auto simp add: mult_pos);
  moreover have "x dvd x * y" by auto;
  moreover assume "squarefree(x * y)";
  ultimately show ?thesis;
    by (insert prems squarefree_zdvd_impl_squarefree [of "x*y" x], auto);
qed;

lemma squarefree_distrib2: "[| 0 < x; 0 < y; squarefree(x * y) |] ==>
                            squarefree (y)";
proof-;
  assume "0 < x" and "0 < y"; 
  then have "0 < x * y" by (auto simp add: mult_pos);
  moreover have "y dvd x * y" by auto;
  moreover assume "squarefree(x * y)";
  ultimately show ?thesis;
    by (insert prems squarefree_zdvd_impl_squarefree [of "x*y" y], auto);
qed;
   
end;