src/HOL/Computational_Algebra/Squarefree.thy
 author wenzelm Wed Nov 01 20:46:23 2017 +0100 (22 months ago) changeset 66983 df83b66f1d94 parent 66276 acc3b7dd0b21 child 67051 e7e54a0b9197 permissions -rw-r--r--
proper merge (amending fb46c031c841);
 eberlm@66276 ` 1` ```(* ``` eberlm@66276 ` 2` ``` File: HOL/Computational_Algebra/Squarefree.thy ``` eberlm@66276 ` 3` ``` Author: Manuel Eberl ``` eberlm@66276 ` 4` eberlm@66276 ` 5` ``` Squarefreeness and decomposition of ring elements into square part and squarefree part ``` eberlm@66276 ` 6` ```*) ``` eberlm@66276 ` 7` ```section \Squarefreeness\ ``` eberlm@66276 ` 8` ```theory Squarefree ``` eberlm@66276 ` 9` ```imports Primes ``` eberlm@66276 ` 10` ```begin ``` eberlm@66276 ` 11` ``` ``` eberlm@66276 ` 12` ```(* TODO: Generalise to n-th powers *) ``` eberlm@66276 ` 13` eberlm@66276 ` 14` ```definition squarefree :: "'a :: comm_monoid_mult \ bool" where ``` eberlm@66276 ` 15` ``` "squarefree n \ (\x. x ^ 2 dvd n \ x dvd 1)" ``` eberlm@66276 ` 16` ``` ``` eberlm@66276 ` 17` ```lemma squarefreeI: "(\x. x ^ 2 dvd n \ x dvd 1) \ squarefree n" ``` eberlm@66276 ` 18` ``` by (auto simp: squarefree_def) ``` eberlm@66276 ` 19` eberlm@66276 ` 20` ```lemma squarefreeD: "squarefree n \ x ^ 2 dvd n \ x dvd 1" ``` eberlm@66276 ` 21` ``` by (auto simp: squarefree_def) ``` eberlm@66276 ` 22` eberlm@66276 ` 23` ```lemma not_squarefreeI: "x ^ 2 dvd n \ \x dvd 1 \ \squarefree n" ``` eberlm@66276 ` 24` ``` by (auto simp: squarefree_def) ``` eberlm@66276 ` 25` eberlm@66276 ` 26` ```lemma not_squarefreeE [case_names square_dvd]: ``` eberlm@66276 ` 27` ``` "\squarefree n \ (\x. x ^ 2 dvd n \ \x dvd 1 \ P) \ P" ``` eberlm@66276 ` 28` ``` by (auto simp: squarefree_def) ``` eberlm@66276 ` 29` eberlm@66276 ` 30` ```lemma not_squarefree_0 [simp]: "\squarefree (0 :: 'a :: comm_semiring_1)" ``` eberlm@66276 ` 31` ``` by (rule not_squarefreeI[of 0]) auto ``` eberlm@66276 ` 32` eberlm@66276 ` 33` ```lemma squarefree_factorial_semiring: ``` eberlm@66276 ` 34` ``` assumes "n \ 0" ``` eberlm@66276 ` 35` ``` shows "squarefree (n :: 'a :: factorial_semiring) \ (\p. prime p \ \p ^ 2 dvd n)" ``` eberlm@66276 ` 36` ``` unfolding squarefree_def ``` eberlm@66276 ` 37` ```proof safe ``` eberlm@66276 ` 38` ``` assume *: "\p. prime p \ \p ^ 2 dvd n" ``` eberlm@66276 ` 39` ``` fix x :: 'a assume x: "x ^ 2 dvd n" ``` eberlm@66276 ` 40` ``` { ``` eberlm@66276 ` 41` ``` assume "\is_unit x" ``` eberlm@66276 ` 42` ``` moreover from assms and x have "x \ 0" by auto ``` eberlm@66276 ` 43` ``` ultimately obtain p where "p dvd x" "prime p" ``` eberlm@66276 ` 44` ``` using prime_divisor_exists by blast ``` eberlm@66276 ` 45` ``` with * have "\p ^ 2 dvd n" by blast ``` eberlm@66276 ` 46` ``` moreover from \p dvd x\ have "p ^ 2 dvd x ^ 2" by (rule dvd_power_same) ``` eberlm@66276 ` 47` ``` ultimately have "\x ^ 2 dvd n" by (blast dest: dvd_trans) ``` eberlm@66276 ` 48` ``` with x have False by contradiction ``` eberlm@66276 ` 49` ``` } ``` eberlm@66276 ` 50` ``` thus "is_unit x" by blast ``` eberlm@66276 ` 51` ```qed auto ``` eberlm@66276 ` 52` eberlm@66276 ` 53` ```lemma squarefree_factorial_semiring': ``` eberlm@66276 ` 54` ``` assumes "n \ 0" ``` eberlm@66276 ` 55` ``` shows "squarefree (n :: 'a :: factorial_semiring) \ ``` eberlm@66276 ` 56` ``` (\p\prime_factors n. multiplicity p n = 1)" ``` eberlm@66276 ` 57` ```proof (subst squarefree_factorial_semiring [OF assms], safe) ``` eberlm@66276 ` 58` ``` fix p assume "\p\#prime_factorization n. multiplicity p n = 1" "prime p" "p^2 dvd n" ``` eberlm@66276 ` 59` ``` with assms show False ``` eberlm@66276 ` 60` ``` by (cases "p dvd n") ``` eberlm@66276 ` 61` ``` (auto simp: prime_factors_dvd power_dvd_iff_le_multiplicity not_dvd_imp_multiplicity_0) ``` eberlm@66276 ` 62` ```qed (auto intro!: multiplicity_eqI simp: power2_eq_square [symmetric]) ``` eberlm@66276 ` 63` eberlm@66276 ` 64` ```lemma squarefree_factorial_semiring'': ``` eberlm@66276 ` 65` ``` assumes "n \ 0" ``` eberlm@66276 ` 66` ``` shows "squarefree (n :: 'a :: factorial_semiring) \ ``` eberlm@66276 ` 67` ``` (\p. prime p \ multiplicity p n \ 1)" ``` eberlm@66276 ` 68` ``` by (subst squarefree_factorial_semiring'[OF assms]) (auto simp: prime_factors_multiplicity) ``` eberlm@66276 ` 69` eberlm@66276 ` 70` ```lemma squarefree_unit [simp]: "is_unit n \ squarefree n" ``` eberlm@66276 ` 71` ```proof (rule squarefreeI) ``` eberlm@66276 ` 72` ``` fix x assume "x^2 dvd n" "n dvd 1" ``` eberlm@66276 ` 73` ``` hence "is_unit (x^2)" by (rule dvd_unit_imp_unit) ``` eberlm@66276 ` 74` ``` thus "is_unit x" by (simp add: is_unit_power_iff) ``` eberlm@66276 ` 75` ```qed ``` eberlm@66276 ` 76` eberlm@66276 ` 77` ```lemma squarefree_1 [simp]: "squarefree (1 :: 'a :: algebraic_semidom)" ``` eberlm@66276 ` 78` ``` by simp ``` eberlm@66276 ` 79` eberlm@66276 ` 80` ```lemma squarefree_minus [simp]: "squarefree (-n :: 'a :: comm_ring_1) \ squarefree n" ``` eberlm@66276 ` 81` ``` by (simp add: squarefree_def) ``` eberlm@66276 ` 82` eberlm@66276 ` 83` ```lemma squarefree_mono: "a dvd b \ squarefree b \ squarefree a" ``` eberlm@66276 ` 84` ``` by (auto simp: squarefree_def intro: dvd_trans) ``` eberlm@66276 ` 85` eberlm@66276 ` 86` ```lemma squarefree_multD: ``` eberlm@66276 ` 87` ``` assumes "squarefree (a * b)" ``` eberlm@66276 ` 88` ``` shows "squarefree a" "squarefree b" ``` eberlm@66276 ` 89` ``` by (rule squarefree_mono[OF _ assms], simp)+ ``` eberlm@66276 ` 90` ``` ``` eberlm@66276 ` 91` ```lemma squarefree_prime_elem: ``` eberlm@66276 ` 92` ``` assumes "prime_elem (p :: 'a :: factorial_semiring)" ``` eberlm@66276 ` 93` ``` shows "squarefree p" ``` eberlm@66276 ` 94` ```proof - ``` eberlm@66276 ` 95` ``` from assms have "p \ 0" by auto ``` eberlm@66276 ` 96` ``` show ?thesis ``` eberlm@66276 ` 97` ``` proof (subst squarefree_factorial_semiring [OF \p \ 0\]; safe) ``` eberlm@66276 ` 98` ``` fix q assume *: "prime q" "q^2 dvd p" ``` eberlm@66276 ` 99` ``` with assms have "multiplicity q p \ 2" by (intro multiplicity_geI) auto ``` eberlm@66276 ` 100` ``` thus False using assms \prime q\ prime_multiplicity_other[of q "normalize p"] ``` eberlm@66276 ` 101` ``` by (cases "q = normalize p") simp_all ``` eberlm@66276 ` 102` ``` qed ``` eberlm@66276 ` 103` ```qed ``` eberlm@66276 ` 104` eberlm@66276 ` 105` ```lemma squarefree_prime: ``` eberlm@66276 ` 106` ``` assumes "prime (p :: 'a :: factorial_semiring)" ``` eberlm@66276 ` 107` ``` shows "squarefree p" ``` eberlm@66276 ` 108` ``` using assms by (intro squarefree_prime_elem) auto ``` eberlm@66276 ` 109` eberlm@66276 ` 110` ```lemma squarefree_mult_coprime: ``` eberlm@66276 ` 111` ``` fixes a b :: "'a :: factorial_semiring_gcd" ``` eberlm@66276 ` 112` ``` assumes "coprime a b" "squarefree a" "squarefree b" ``` eberlm@66276 ` 113` ``` shows "squarefree (a * b)" ``` eberlm@66276 ` 114` ```proof - ``` eberlm@66276 ` 115` ``` from assms have nz: "a * b \ 0" by auto ``` eberlm@66276 ` 116` ``` show ?thesis unfolding squarefree_factorial_semiring'[OF nz] ``` eberlm@66276 ` 117` ``` proof ``` eberlm@66276 ` 118` ``` fix p assume p: "p \ prime_factors (a * b)" ``` eberlm@66276 ` 119` ``` { ``` eberlm@66276 ` 120` ``` assume "p dvd a \ p dvd b" ``` eberlm@66276 ` 121` ``` hence "p dvd gcd a b" by simp ``` eberlm@66276 ` 122` ``` also have "gcd a b = 1" by fact ``` eberlm@66276 ` 123` ``` finally have False using nz using p by (auto simp: prime_factors_dvd) ``` eberlm@66276 ` 124` ``` } ``` eberlm@66276 ` 125` ``` hence "\(p dvd a \ p dvd b)" by blast ``` eberlm@66276 ` 126` ``` moreover from p have "p dvd a \ p dvd b" using nz ``` eberlm@66276 ` 127` ``` by (auto simp: prime_factors_dvd prime_dvd_mult_iff) ``` eberlm@66276 ` 128` ``` ultimately show "multiplicity p (a * b) = 1" using nz p assms(2,3) ``` eberlm@66276 ` 129` ``` by (auto simp: prime_elem_multiplicity_mult_distrib prime_factors_multiplicity ``` eberlm@66276 ` 130` ``` not_dvd_imp_multiplicity_0 squarefree_factorial_semiring') ``` eberlm@66276 ` 131` ``` qed ``` eberlm@66276 ` 132` ```qed ``` eberlm@66276 ` 133` eberlm@66276 ` 134` ```lemma squarefree_prod_coprime: ``` eberlm@66276 ` 135` ``` fixes f :: "'a \ 'b :: factorial_semiring_gcd" ``` eberlm@66276 ` 136` ``` assumes "\a b. a \ A \ b \ A \ a \ b \ coprime (f a) (f b)" ``` eberlm@66276 ` 137` ``` assumes "\a. a \ A \ squarefree (f a)" ``` eberlm@66276 ` 138` ``` shows "squarefree (prod f A)" ``` eberlm@66276 ` 139` ``` using assms ``` eberlm@66276 ` 140` ``` by (induction A rule: infinite_finite_induct) ``` eberlm@66276 ` 141` ``` (auto intro!: squarefree_mult_coprime prod_coprime') ``` eberlm@66276 ` 142` eberlm@66276 ` 143` ```lemma squarefree_powerD: "m > 0 \ squarefree (n ^ m) \ squarefree n" ``` eberlm@66276 ` 144` ``` by (cases m) (auto dest: squarefree_multD) ``` eberlm@66276 ` 145` eberlm@66276 ` 146` ```lemma squarefree_power_iff: ``` eberlm@66276 ` 147` ``` "squarefree (n ^ m) \ m = 0 \ is_unit n \ (squarefree n \ m = 1)" ``` eberlm@66276 ` 148` ```proof safe ``` eberlm@66276 ` 149` ``` assume "squarefree (n ^ m)" "m > 0" "\is_unit n" ``` eberlm@66276 ` 150` ``` show "m = 1" ``` eberlm@66276 ` 151` ``` proof (rule ccontr) ``` eberlm@66276 ` 152` ``` assume "m \ 1" ``` eberlm@66276 ` 153` ``` with \m > 0\ have "n ^ 2 dvd n ^ m" by (intro le_imp_power_dvd) auto ``` eberlm@66276 ` 154` ``` from this and \\is_unit n\ have "\squarefree (n ^ m)" by (rule not_squarefreeI) ``` eberlm@66276 ` 155` ``` with \squarefree (n ^ m)\ show False by contradiction ``` eberlm@66276 ` 156` ``` qed ``` eberlm@66276 ` 157` ```qed (auto simp: is_unit_power_iff dest: squarefree_powerD) ``` eberlm@66276 ` 158` eberlm@66276 ` 159` ```definition squarefree_nat :: "nat \ bool" where ``` eberlm@66276 ` 160` ``` [code_abbrev]: "squarefree_nat = squarefree" ``` eberlm@66276 ` 161` ``` ``` eberlm@66276 ` 162` ```lemma squarefree_nat_code_naive [code]: ``` eberlm@66276 ` 163` ``` "squarefree_nat n \ n \ 0 \ (\k\{2..n}. \k ^ 2 dvd n)" ``` eberlm@66276 ` 164` ```proof safe ``` eberlm@66276 ` 165` ``` assume *: "\k\{2..n}. \ k\<^sup>2 dvd n" and n: "n > 0" ``` eberlm@66276 ` 166` ``` show "squarefree_nat n" unfolding squarefree_nat_def ``` eberlm@66276 ` 167` ``` proof (rule squarefreeI) ``` eberlm@66276 ` 168` ``` fix k assume k: "k ^ 2 dvd n" ``` eberlm@66276 ` 169` ``` have "k dvd n" by (rule dvd_trans[OF _ k]) auto ``` eberlm@66276 ` 170` ``` with n have "k \ n" by (intro dvd_imp_le) ``` eberlm@66276 ` 171` ``` with bspec[OF *, of k] k have "\k > 1" by (intro notI) auto ``` eberlm@66276 ` 172` ``` moreover from k and n have "k \ 0" by (intro notI) auto ``` eberlm@66276 ` 173` ``` ultimately have "k = 1" by presburger ``` eberlm@66276 ` 174` ``` thus "is_unit k" by simp ``` eberlm@66276 ` 175` ``` qed ``` eberlm@66276 ` 176` ```qed (auto simp: squarefree_nat_def squarefree_def intro!: Nat.gr0I) ``` eberlm@66276 ` 177` eberlm@66276 ` 178` eberlm@66276 ` 179` eberlm@66276 ` 180` ```definition square_part :: "'a :: factorial_semiring \ 'a" where ``` eberlm@66276 ` 181` ``` "square_part n = (if n = 0 then 0 else ``` eberlm@66276 ` 182` ``` normalize (\p\prime_factors n. p ^ (multiplicity p n div 2)))" ``` eberlm@66276 ` 183` ``` ``` eberlm@66276 ` 184` ```lemma square_part_nonzero: ``` eberlm@66276 ` 185` ``` "n \ 0 \ square_part n = normalize (\p\prime_factors n. p ^ (multiplicity p n div 2))" ``` eberlm@66276 ` 186` ``` by (simp add: square_part_def) ``` eberlm@66276 ` 187` ``` ``` eberlm@66276 ` 188` ```lemma square_part_0 [simp]: "square_part 0 = 0" ``` eberlm@66276 ` 189` ``` by (simp add: square_part_def) ``` eberlm@66276 ` 190` eberlm@66276 ` 191` ```lemma square_part_unit [simp]: "is_unit x \ square_part x = 1" ``` eberlm@66276 ` 192` ``` by (auto simp: square_part_def prime_factorization_unit) ``` eberlm@66276 ` 193` eberlm@66276 ` 194` ```lemma square_part_1 [simp]: "square_part 1 = 1" ``` eberlm@66276 ` 195` ``` by simp ``` eberlm@66276 ` 196` ``` ``` eberlm@66276 ` 197` ```lemma square_part_0_iff [simp]: "square_part n = 0 \ n = 0" ``` eberlm@66276 ` 198` ``` by (simp add: square_part_def) ``` eberlm@66276 ` 199` eberlm@66276 ` 200` ```lemma normalize_uminus [simp]: ``` eberlm@66276 ` 201` ``` "normalize (-x :: 'a :: {normalization_semidom, comm_ring_1}) = normalize x" ``` eberlm@66276 ` 202` ``` by (rule associatedI) auto ``` eberlm@66276 ` 203` eberlm@66276 ` 204` ```lemma multiplicity_uminus_right [simp]: ``` eberlm@66276 ` 205` ``` "multiplicity (x :: 'a :: {factorial_semiring, comm_ring_1}) (-y) = multiplicity x y" ``` eberlm@66276 ` 206` ```proof - ``` eberlm@66276 ` 207` ``` have "multiplicity x (-y) = multiplicity x (normalize (-y))" ``` eberlm@66276 ` 208` ``` by (rule multiplicity_normalize_right [symmetric]) ``` eberlm@66276 ` 209` ``` also have "\ = multiplicity x y" by simp ``` eberlm@66276 ` 210` ``` finally show ?thesis . ``` eberlm@66276 ` 211` ```qed ``` eberlm@66276 ` 212` eberlm@66276 ` 213` ```lemma multiplicity_uminus_left [simp]: ``` eberlm@66276 ` 214` ``` "multiplicity (-x :: 'a :: {factorial_semiring, comm_ring_1}) y = multiplicity x y" ``` eberlm@66276 ` 215` ```proof - ``` eberlm@66276 ` 216` ``` have "multiplicity (-x) y = multiplicity (normalize (-x)) y" ``` eberlm@66276 ` 217` ``` by (rule multiplicity_normalize_left [symmetric]) ``` eberlm@66276 ` 218` ``` also have "\ = multiplicity x y" by simp ``` eberlm@66276 ` 219` ``` finally show ?thesis . ``` eberlm@66276 ` 220` ```qed ``` eberlm@66276 ` 221` eberlm@66276 ` 222` ```lemma prime_factorization_uminus [simp]: ``` eberlm@66276 ` 223` ``` "prime_factorization (-x :: 'a :: {factorial_semiring, comm_ring_1}) = prime_factorization x" ``` eberlm@66276 ` 224` ``` by (rule prime_factorization_cong) simp_all ``` eberlm@66276 ` 225` eberlm@66276 ` 226` ```lemma square_part_uminus [simp]: ``` eberlm@66276 ` 227` ``` "square_part (-x :: 'a :: {factorial_semiring, comm_ring_1}) = square_part x" ``` eberlm@66276 ` 228` ``` by (simp add: square_part_def) ``` eberlm@66276 ` 229` ``` ``` eberlm@66276 ` 230` ```lemma prime_multiplicity_square_part: ``` eberlm@66276 ` 231` ``` assumes "prime p" ``` eberlm@66276 ` 232` ``` shows "multiplicity p (square_part n) = multiplicity p n div 2" ``` eberlm@66276 ` 233` ```proof (cases "n = 0") ``` eberlm@66276 ` 234` ``` case False ``` eberlm@66276 ` 235` ``` thus ?thesis unfolding square_part_nonzero[OF False] multiplicity_normalize_right ``` eberlm@66276 ` 236` ``` using finite_prime_divisors[of n] assms ``` eberlm@66276 ` 237` ``` by (subst multiplicity_prod_prime_powers) ``` eberlm@66276 ` 238` ``` (auto simp: not_dvd_imp_multiplicity_0 prime_factors_dvd multiplicity_prod_prime_powers) ``` eberlm@66276 ` 239` ```qed auto ``` eberlm@66276 ` 240` eberlm@66276 ` 241` ```lemma square_part_square_dvd [simp, intro]: "square_part n ^ 2 dvd n" ``` eberlm@66276 ` 242` ```proof (cases "n = 0") ``` eberlm@66276 ` 243` ``` case False ``` eberlm@66276 ` 244` ``` thus ?thesis ``` eberlm@66276 ` 245` ``` by (intro multiplicity_le_imp_dvd) ``` eberlm@66276 ` 246` ``` (auto simp: prime_multiplicity_square_part prime_elem_multiplicity_power_distrib) ``` eberlm@66276 ` 247` ```qed auto ``` eberlm@66276 ` 248` ``` ``` eberlm@66276 ` 249` ```lemma prime_multiplicity_le_imp_dvd: ``` eberlm@66276 ` 250` ``` assumes "x \ 0" "y \ 0" ``` eberlm@66276 ` 251` ``` shows "x dvd y \ (\p. prime p \ multiplicity p x \ multiplicity p y)" ``` eberlm@66276 ` 252` ``` using assms by (auto intro: multiplicity_le_imp_dvd dvd_imp_multiplicity_le) ``` eberlm@66276 ` 253` eberlm@66276 ` 254` ```lemma dvd_square_part_iff: "x dvd square_part n \ x ^ 2 dvd n" ``` eberlm@66276 ` 255` ```proof (cases "x = 0"; cases "n = 0") ``` eberlm@66276 ` 256` ``` assume nz: "x \ 0" "n \ 0" ``` eberlm@66276 ` 257` ``` thus ?thesis ``` eberlm@66276 ` 258` ``` by (subst (1 2) prime_multiplicity_le_imp_dvd) ``` eberlm@66276 ` 259` ``` (auto simp: prime_multiplicity_square_part prime_elem_multiplicity_power_distrib) ``` eberlm@66276 ` 260` ```qed auto ``` eberlm@66276 ` 261` eberlm@66276 ` 262` eberlm@66276 ` 263` ```definition squarefree_part :: "'a :: factorial_semiring \ 'a" where ``` eberlm@66276 ` 264` ``` "squarefree_part n = (if n = 0 then 1 else n div square_part n ^ 2)" ``` eberlm@66276 ` 265` eberlm@66276 ` 266` ```lemma squarefree_part_0 [simp]: "squarefree_part 0 = 1" ``` eberlm@66276 ` 267` ``` by (simp add: squarefree_part_def) ``` eberlm@66276 ` 268` eberlm@66276 ` 269` ```lemma squarefree_part_unit [simp]: "is_unit n \ squarefree_part n = n" ``` eberlm@66276 ` 270` ``` by (auto simp add: squarefree_part_def) ``` eberlm@66276 ` 271` ``` ``` eberlm@66276 ` 272` ```lemma squarefree_part_1 [simp]: "squarefree_part 1 = 1" ``` eberlm@66276 ` 273` ``` by simp ``` eberlm@66276 ` 274` ``` ``` eberlm@66276 ` 275` ```lemma squarefree_decompose: "n = squarefree_part n * square_part n ^ 2" ``` eberlm@66276 ` 276` ``` by (simp add: squarefree_part_def) ``` eberlm@66276 ` 277` eberlm@66276 ` 278` ```lemma squarefree_part_uminus [simp]: ``` eberlm@66276 ` 279` ``` assumes "x \ 0" ``` eberlm@66276 ` 280` ``` shows "squarefree_part (-x :: 'a :: {factorial_semiring, comm_ring_1}) = -squarefree_part x" ``` eberlm@66276 ` 281` ```proof - ``` eberlm@66276 ` 282` ``` have "-(squarefree_part x * square_part x ^ 2) = -x" ``` eberlm@66276 ` 283` ``` by (subst squarefree_decompose [symmetric]) auto ``` eberlm@66276 ` 284` ``` also have "\ = squarefree_part (-x) * square_part (-x) ^ 2" by (rule squarefree_decompose) ``` eberlm@66276 ` 285` ``` finally have "(- squarefree_part x) * square_part x ^ 2 = ``` eberlm@66276 ` 286` ``` squarefree_part (-x) * square_part x ^ 2" by simp ``` eberlm@66276 ` 287` ``` thus ?thesis using assms by (subst (asm) mult_right_cancel) auto ``` eberlm@66276 ` 288` ```qed ``` eberlm@66276 ` 289` eberlm@66276 ` 290` ```lemma squarefree_part_nonzero [simp]: "squarefree_part n \ 0" ``` eberlm@66276 ` 291` ``` using squarefree_decompose[of n] by (cases "n \ 0") auto ``` eberlm@66276 ` 292` eberlm@66276 ` 293` ```lemma prime_multiplicity_squarefree_part: ``` eberlm@66276 ` 294` ``` assumes "prime p" ``` eberlm@66276 ` 295` ``` shows "multiplicity p (squarefree_part n) = multiplicity p n mod 2" ``` eberlm@66276 ` 296` ```proof (cases "n = 0") ``` eberlm@66276 ` 297` ``` case False ``` eberlm@66276 ` 298` ``` hence n: "n \ 0" by auto ``` eberlm@66276 ` 299` ``` have "multiplicity p n mod 2 + 2 * (multiplicity p n div 2) = multiplicity p n" by simp ``` eberlm@66276 ` 300` ``` also have "\ = multiplicity p (squarefree_part n * square_part n ^ 2)" ``` eberlm@66276 ` 301` ``` by (subst squarefree_decompose[of n]) simp ``` eberlm@66276 ` 302` ``` also from assms n have "\ = multiplicity p (squarefree_part n) + 2 * (multiplicity p n div 2)" ``` eberlm@66276 ` 303` ``` by (subst prime_elem_multiplicity_mult_distrib) ``` eberlm@66276 ` 304` ``` (auto simp: prime_elem_multiplicity_power_distrib prime_multiplicity_square_part) ``` eberlm@66276 ` 305` ``` finally show ?thesis by (subst (asm) add_right_cancel) simp ``` eberlm@66276 ` 306` ```qed auto ``` eberlm@66276 ` 307` ``` ``` eberlm@66276 ` 308` ```lemma prime_multiplicity_squarefree_part_le_Suc_0 [intro]: ``` eberlm@66276 ` 309` ``` assumes "prime p" ``` eberlm@66276 ` 310` ``` shows "multiplicity p (squarefree_part n) \ Suc 0" ``` eberlm@66276 ` 311` ``` by (simp add: assms prime_multiplicity_squarefree_part) ``` eberlm@66276 ` 312` eberlm@66276 ` 313` ```lemma squarefree_squarefree_part [simp, intro]: "squarefree (squarefree_part n)" ``` eberlm@66276 ` 314` ``` by (subst squarefree_factorial_semiring'') ``` eberlm@66276 ` 315` ``` (auto simp: prime_multiplicity_squarefree_part_le_Suc_0) ``` eberlm@66276 ` 316` ``` ``` eberlm@66276 ` 317` ```lemma squarefree_decomposition_unique: ``` eberlm@66276 ` 318` ``` assumes "square_part m = square_part n" ``` eberlm@66276 ` 319` ``` assumes "squarefree_part m = squarefree_part n" ``` eberlm@66276 ` 320` ``` shows "m = n" ``` eberlm@66276 ` 321` ``` by (subst (1 2) squarefree_decompose) (simp_all add: assms) ``` eberlm@66276 ` 322` ``` ``` eberlm@66276 ` 323` ```lemma normalize_square_part [simp]: "normalize (square_part x) = square_part x" ``` eberlm@66276 ` 324` ``` by (simp add: square_part_def) ``` eberlm@66276 ` 325` eberlm@66276 ` 326` ```lemma square_part_even_power': "square_part (x ^ (2 * n)) = normalize (x ^ n)" ``` eberlm@66276 ` 327` ```proof (cases "x = 0") ``` eberlm@66276 ` 328` ``` case False ``` eberlm@66276 ` 329` ``` have "normalize (square_part (x ^ (2 * n))) = normalize (x ^ n)" using False ``` eberlm@66276 ` 330` ``` by (intro multiplicity_eq_imp_eq) ``` eberlm@66276 ` 331` ``` (auto simp: prime_multiplicity_square_part prime_elem_multiplicity_power_distrib) ``` eberlm@66276 ` 332` ``` thus ?thesis by simp ``` eberlm@66276 ` 333` ```qed (auto simp: power_0_left) ``` eberlm@66276 ` 334` eberlm@66276 ` 335` ```lemma square_part_even_power: "even n \ square_part (x ^ n) = normalize (x ^ (n div 2))" ``` eberlm@66276 ` 336` ``` by (subst square_part_even_power' [symmetric]) auto ``` eberlm@66276 ` 337` eberlm@66276 ` 338` ```lemma square_part_odd_power': "square_part (x ^ (Suc (2 * n))) = normalize (x ^ n * square_part x)" ``` eberlm@66276 ` 339` ```proof (cases "x = 0") ``` eberlm@66276 ` 340` ``` case False ``` eberlm@66276 ` 341` ``` have "normalize (square_part (x ^ (Suc (2 * n)))) = normalize (square_part x * x ^ n)" ``` eberlm@66276 ` 342` ``` proof (rule multiplicity_eq_imp_eq, goal_cases) ``` eberlm@66276 ` 343` ``` case (3 p) ``` eberlm@66276 ` 344` ``` hence "multiplicity p (square_part (x ^ Suc (2 * n))) = ``` eberlm@66276 ` 345` ``` (2 * (n * multiplicity p x) + multiplicity p x) div 2" ``` eberlm@66276 ` 346` ``` by (subst prime_multiplicity_square_part) ``` eberlm@66276 ` 347` ``` (auto simp: False prime_elem_multiplicity_power_distrib algebra_simps simp del: power_Suc) ``` eberlm@66276 ` 348` ``` also from 3 False have "\ = multiplicity p (square_part x * x ^ n)" ``` eberlm@66276 ` 349` ``` by (subst div_mult_self4) (auto simp: prime_multiplicity_square_part ``` eberlm@66276 ` 350` ``` prime_elem_multiplicity_mult_distrib prime_elem_multiplicity_power_distrib) ``` eberlm@66276 ` 351` ``` finally show ?case . ``` eberlm@66276 ` 352` ``` qed (insert False, auto) ``` eberlm@66276 ` 353` ``` thus ?thesis by (simp add: mult_ac) ``` eberlm@66276 ` 354` ```qed auto ``` eberlm@66276 ` 355` eberlm@66276 ` 356` ```lemma square_part_odd_power: ``` eberlm@66276 ` 357` ``` "odd n \ square_part (x ^ n) = normalize (x ^ (n div 2) * square_part x)" ``` eberlm@66276 ` 358` ``` by (subst square_part_odd_power' [symmetric]) auto ``` eberlm@66276 ` 359` eberlm@66276 ` 360` `end`