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

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

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

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

defs
pdivisors_def:   "pdivisors n  == remdups(pfactors 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)";

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);
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);
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);
done;

lemma pdivisors_znondec: "znondec (pdivisors n)";
apply (insert pfactors_znondec [of n]);
apply (drule znondec_remdups_prop);
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);
done;

lemmas pdivisors_ac = pdivisors_le_1 pdivisors_gr_1
pdivisors_znondec pdivisors_zprimel;

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

proof-;
assume "1 <= n";
note pfactors_zprod_ge_1;
also have "zprod (remdups (pfactors n)) = rad n";
finally show "1 <= rad n" by auto;
qed;

proof-;
assume "1 < n";
moreover have "1 ~= rad n";
proof;
then have "zprod( pdivisors n) = 1";
moreover have "zprimel (pdivisors n)";
ultimately have "pdivisors n = []";
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 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)))";
also have "zprod (remdups (pfactors n)) = rad n"
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))";
also have "zprod (pdivisors n) = rad n";
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)";
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);
next;
assume "p:zprime" and "1 <= n" and "p dvd rad n";
then have "p mem pdivisors n";
then have "p mem pfactors n";
thus "p dvd n";
by (insert prems, auto simp add: mem_pfactors_imp_zdvd);
qed;

lemma rad_multiplicity_le: "ALL p. multiplicity p (rad n) <= multiplicity p n";
pdivisors_def numoccurs_remdups);

proof-;
assume "1 <= n";
have "ALL p. multiplicity p (rad n) <= multiplicity p n";
moreover have "1 <= rad n";
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)";
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";
assume "m dvd n" and "squarefree m";
then have "ALL p. (multiplicity p m <= multiplicity p (rad n))";
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);
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;

```

### Some Initial Properties Involving distinct

lemma distinct_numoccurs_le_1:

`  distinct list = (∀p. numoccurs p list ≤ 1)`

### Some Initial Properties Involving remdups

lemma zprimel_remdups_prop:

`  zprimel l ==> zprimel (remdups l)`

lemma aux:

```  [| znondec (remdups list); znondec (a # list) |]
==> znondec (remdups (a # list))```

lemma znondec_remdups_prop:

`  znondec l ==> znondec (remdups l)`

lemma not_empty_remdups:

`  (l ≠ []) = (remdups l ≠ [])`

lemma zprimel_zprod_ge_1:

`  zprimel pl ==> 1 ≤ zprod (remdups pl)`

lemma pfactors_zprod_ge_1:

`  1 ≤ zprod (remdups (pfactors n))`

lemma zprimel_zprod_le:

`  zprimel pl ==> zprod (remdups pl) ≤ zprod pl`

lemma pfactors_zprod_le:

`  zprod (remdups (pfactors n)) ≤ zprod (pfactors n)`

lemma numoccurs_remdups:

`  ∀p. numoccurs p (remdups list) ≤ numoccurs p list`

lemma pdivisors_zprimel:

`  zprimel (pdivisors n)`

lemma pdivisors_znondec:

`  znondec (pdivisors n)`

lemma pdivisors_le_1:

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

lemma pdivisors_gr_1:

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

lemmas pdivisors_ac:

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

`  n ≤ 1 ==> rad n = 1`

`  1 < n ==> rad n ≤ n`

`  1 ≤ n ==> 1 ≤ rad n`

`  1 < n ==> 1 < rad n`

`  p ∈ zprime ==> rad p = p`

`  pfactors (rad n) = pdivisors n`

lemma mem_pfactors_mem_pdivisors:

`  p mem pfactors n = p mem pdivisors n`

lemma zprod_remdups_dvd:

`  x mem list ==> x dvd zprod (remdups list)`

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

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

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

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

`  1 ≤ n ==> squarefree (rad n)`

`  ∀p. multiplicity p (rad n) ≤ multiplicity p n`

`  1 ≤ n ==> rad n dvd n`

lemma squarefree_prop:

`  squarefree n = (∀p. multiplicity p n ≤ 1)`

`  [| 1 ≤ m; 1 ≤ n; m dvd n; squarefree m |] ==> m dvd rad n`

lemma squarefree_zdvd_impl_squarefree:

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

lemma squarefree_distrib1:

`  [| 0 < x; 0 < y; squarefree (x * y) |] ==> squarefree x`

lemma squarefree_distrib2:

`  [| 0 < x; 0 < y; squarefree (x * y) |] ==> squarefree y`