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