|
1 (* Title: HOL/Number_Theory/Euclidean_Algorithm.thy |
|
2 Author: Manuel Eberl, TU Muenchen |
|
3 *) |
|
4 |
|
5 section \<open>Abstract euclidean algorithm in euclidean (semi)rings\<close> |
|
6 |
|
7 theory Euclidean_Algorithm |
|
8 imports Factorial_Ring |
|
9 begin |
|
10 |
|
11 subsection \<open>Generic construction of the (simple) euclidean algorithm\<close> |
|
12 |
|
13 context euclidean_semiring |
|
14 begin |
|
15 |
|
16 context |
|
17 begin |
|
18 |
|
19 qualified function gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
20 where "gcd a b = (if b = 0 then normalize a else gcd b (a mod b))" |
|
21 by pat_completeness simp |
|
22 termination |
|
23 by (relation "measure (euclidean_size \<circ> snd)") (simp_all add: mod_size_less) |
|
24 |
|
25 declare gcd.simps [simp del] |
|
26 |
|
27 lemma eucl_induct [case_names zero mod]: |
|
28 assumes H1: "\<And>b. P b 0" |
|
29 and H2: "\<And>a b. b \<noteq> 0 \<Longrightarrow> P b (a mod b) \<Longrightarrow> P a b" |
|
30 shows "P a b" |
|
31 proof (induct a b rule: gcd.induct) |
|
32 case (1 a b) |
|
33 show ?case |
|
34 proof (cases "b = 0") |
|
35 case True then show "P a b" by simp (rule H1) |
|
36 next |
|
37 case False |
|
38 then have "P b (a mod b)" |
|
39 by (rule "1.hyps") |
|
40 with \<open>b \<noteq> 0\<close> show "P a b" |
|
41 by (blast intro: H2) |
|
42 qed |
|
43 qed |
|
44 |
|
45 qualified lemma gcd_0: |
|
46 "gcd a 0 = normalize a" |
|
47 by (simp add: gcd.simps [of a 0]) |
|
48 |
|
49 qualified lemma gcd_mod: |
|
50 "a \<noteq> 0 \<Longrightarrow> gcd a (b mod a) = gcd b a" |
|
51 by (simp add: gcd.simps [of b 0] gcd.simps [of b a]) |
|
52 |
|
53 qualified definition lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
|
54 where "lcm a b = normalize (a * b) div gcd a b" |
|
55 |
|
56 qualified definition Lcm :: "'a set \<Rightarrow> 'a" \<comment> |
|
57 \<open>Somewhat complicated definition of Lcm that has the advantage of working |
|
58 for infinite sets as well\<close> |
|
59 where |
|
60 [code del]: "Lcm A = (if \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) then |
|
61 let l = SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = |
|
62 (LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n) |
|
63 in normalize l |
|
64 else 0)" |
|
65 |
|
66 qualified definition Gcd :: "'a set \<Rightarrow> 'a" |
|
67 where [code del]: "Gcd A = Lcm {d. \<forall>a\<in>A. d dvd a}" |
|
68 |
|
69 end |
|
70 |
|
71 lemma semiring_gcd: |
|
72 "class.semiring_gcd one zero times gcd lcm |
|
73 divide plus minus unit_factor normalize" |
|
74 proof |
|
75 show "gcd a b dvd a" |
|
76 and "gcd a b dvd b" for a b |
|
77 by (induct a b rule: eucl_induct) |
|
78 (simp_all add: local.gcd_0 local.gcd_mod dvd_mod_iff) |
|
79 next |
|
80 show "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b" for a b c |
|
81 proof (induct a b rule: eucl_induct) |
|
82 case (zero a) from \<open>c dvd a\<close> show ?case |
|
83 by (rule dvd_trans) (simp add: local.gcd_0) |
|
84 next |
|
85 case (mod a b) |
|
86 then show ?case |
|
87 by (simp add: local.gcd_mod dvd_mod_iff) |
|
88 qed |
|
89 next |
|
90 show "normalize (gcd a b) = gcd a b" for a b |
|
91 by (induct a b rule: eucl_induct) |
|
92 (simp_all add: local.gcd_0 local.gcd_mod) |
|
93 next |
|
94 show "lcm a b = normalize (a * b) div gcd a b" for a b |
|
95 by (fact local.lcm_def) |
|
96 qed |
|
97 |
|
98 interpretation semiring_gcd one zero times gcd lcm |
|
99 divide plus minus unit_factor normalize |
|
100 by (fact semiring_gcd) |
|
101 |
|
102 lemma semiring_Gcd: |
|
103 "class.semiring_Gcd one zero times gcd lcm Gcd Lcm |
|
104 divide plus minus unit_factor normalize" |
|
105 proof - |
|
106 show ?thesis |
|
107 proof |
|
108 have "(\<forall>a\<in>A. a dvd Lcm A) \<and> (\<forall>b. (\<forall>a\<in>A. a dvd b) \<longrightarrow> Lcm A dvd b)" for A |
|
109 proof (cases "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l)") |
|
110 case False |
|
111 then have "Lcm A = 0" |
|
112 by (auto simp add: local.Lcm_def) |
|
113 with False show ?thesis |
|
114 by auto |
|
115 next |
|
116 case True |
|
117 then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \<noteq> 0" "\<forall>a\<in>A. a dvd l\<^sub>0" by blast |
|
118 define n where "n = (LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n)" |
|
119 define l where "l = (SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n)" |
|
120 have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n" |
|
121 apply (subst n_def) |
|
122 apply (rule LeastI [of _ "euclidean_size l\<^sub>0"]) |
|
123 apply (rule exI [of _ l\<^sub>0]) |
|
124 apply (simp add: l\<^sub>0_props) |
|
125 done |
|
126 from someI_ex [OF this] have "l \<noteq> 0" and "\<forall>a\<in>A. a dvd l" |
|
127 and "euclidean_size l = n" |
|
128 unfolding l_def by simp_all |
|
129 { |
|
130 fix l' assume "\<forall>a\<in>A. a dvd l'" |
|
131 with \<open>\<forall>a\<in>A. a dvd l\<close> have "\<forall>a\<in>A. a dvd gcd l l'" |
|
132 by (auto intro: gcd_greatest) |
|
133 moreover from \<open>l \<noteq> 0\<close> have "gcd l l' \<noteq> 0" |
|
134 by simp |
|
135 ultimately have "\<exists>b. b \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd b) \<and> |
|
136 euclidean_size b = euclidean_size (gcd l l')" |
|
137 by (intro exI [of _ "gcd l l'"], auto) |
|
138 then have "euclidean_size (gcd l l') \<ge> n" |
|
139 by (subst n_def) (rule Least_le) |
|
140 moreover have "euclidean_size (gcd l l') \<le> n" |
|
141 proof - |
|
142 have "gcd l l' dvd l" |
|
143 by simp |
|
144 then obtain a where "l = gcd l l' * a" .. |
|
145 with \<open>l \<noteq> 0\<close> have "a \<noteq> 0" |
|
146 by auto |
|
147 hence "euclidean_size (gcd l l') \<le> euclidean_size (gcd l l' * a)" |
|
148 by (rule size_mult_mono) |
|
149 also have "gcd l l' * a = l" using \<open>l = gcd l l' * a\<close> .. |
|
150 also note \<open>euclidean_size l = n\<close> |
|
151 finally show "euclidean_size (gcd l l') \<le> n" . |
|
152 qed |
|
153 ultimately have *: "euclidean_size l = euclidean_size (gcd l l')" |
|
154 by (intro le_antisym, simp_all add: \<open>euclidean_size l = n\<close>) |
|
155 from \<open>l \<noteq> 0\<close> have "l dvd gcd l l'" |
|
156 by (rule dvd_euclidean_size_eq_imp_dvd) (auto simp add: *) |
|
157 hence "l dvd l'" by (rule dvd_trans [OF _ gcd_dvd2]) |
|
158 } |
|
159 with \<open>\<forall>a\<in>A. a dvd l\<close> and \<open>l \<noteq> 0\<close> |
|
160 have "(\<forall>a\<in>A. a dvd normalize l) \<and> |
|
161 (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> normalize l dvd l')" |
|
162 by auto |
|
163 also from True have "normalize l = Lcm A" |
|
164 by (simp add: local.Lcm_def Let_def n_def l_def) |
|
165 finally show ?thesis . |
|
166 qed |
|
167 then show dvd_Lcm: "a \<in> A \<Longrightarrow> a dvd Lcm A" |
|
168 and Lcm_least: "(\<And>a. a \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> Lcm A dvd b" for A and a b |
|
169 by auto |
|
170 show "a \<in> A \<Longrightarrow> Gcd A dvd a" for A and a |
|
171 by (auto simp add: local.Gcd_def intro: Lcm_least) |
|
172 show "(\<And>a. a \<in> A \<Longrightarrow> b dvd a) \<Longrightarrow> b dvd Gcd A" for A and b |
|
173 by (auto simp add: local.Gcd_def intro: dvd_Lcm) |
|
174 show [simp]: "normalize (Lcm A) = Lcm A" for A |
|
175 by (simp add: local.Lcm_def) |
|
176 show "normalize (Gcd A) = Gcd A" for A |
|
177 by (simp add: local.Gcd_def) |
|
178 qed |
|
179 qed |
|
180 |
|
181 interpretation semiring_Gcd one zero times gcd lcm Gcd Lcm |
|
182 divide plus minus unit_factor normalize |
|
183 by (fact semiring_Gcd) |
|
184 |
|
185 subclass factorial_semiring |
|
186 proof - |
|
187 show "class.factorial_semiring divide plus minus zero times one |
|
188 unit_factor normalize" |
|
189 proof (standard, rule factorial_semiring_altI_aux) \<comment> \<open>FIXME rule\<close> |
|
190 fix x assume "x \<noteq> 0" |
|
191 thus "finite {p. p dvd x \<and> normalize p = p}" |
|
192 proof (induction "euclidean_size x" arbitrary: x rule: less_induct) |
|
193 case (less x) |
|
194 show ?case |
|
195 proof (cases "\<exists>y. y dvd x \<and> \<not>x dvd y \<and> \<not>is_unit y") |
|
196 case False |
|
197 have "{p. p dvd x \<and> normalize p = p} \<subseteq> {1, normalize x}" |
|
198 proof |
|
199 fix p assume p: "p \<in> {p. p dvd x \<and> normalize p = p}" |
|
200 with False have "is_unit p \<or> x dvd p" by blast |
|
201 thus "p \<in> {1, normalize x}" |
|
202 proof (elim disjE) |
|
203 assume "is_unit p" |
|
204 hence "normalize p = 1" by (simp add: is_unit_normalize) |
|
205 with p show ?thesis by simp |
|
206 next |
|
207 assume "x dvd p" |
|
208 with p have "normalize p = normalize x" by (intro associatedI) simp_all |
|
209 with p show ?thesis by simp |
|
210 qed |
|
211 qed |
|
212 moreover have "finite \<dots>" by simp |
|
213 ultimately show ?thesis by (rule finite_subset) |
|
214 next |
|
215 case True |
|
216 then obtain y where y: "y dvd x" "\<not>x dvd y" "\<not>is_unit y" by blast |
|
217 define z where "z = x div y" |
|
218 let ?fctrs = "\<lambda>x. {p. p dvd x \<and> normalize p = p}" |
|
219 from y have x: "x = y * z" by (simp add: z_def) |
|
220 with less.prems have "y \<noteq> 0" "z \<noteq> 0" by auto |
|
221 have normalized_factors_product: |
|
222 "{p. p dvd a * b \<and> normalize p = p} = |
|
223 (\<lambda>(x,y). x * y) ` ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})" for a b |
|
224 proof safe |
|
225 fix p assume p: "p dvd a * b" "normalize p = p" |
|
226 from dvd_productE[OF p(1)] guess x y . note xy = this |
|
227 define x' y' where "x' = normalize x" and "y' = normalize y" |
|
228 have "p = x' * y'" |
|
229 by (subst p(2) [symmetric]) (simp add: xy x'_def y'_def normalize_mult) |
|
230 moreover from xy have "normalize x' = x'" "normalize y' = y'" "x' dvd a" "y' dvd b" |
|
231 by (simp_all add: x'_def y'_def) |
|
232 ultimately show "p \<in> (\<lambda>(x, y). x * y) ` |
|
233 ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})" |
|
234 by blast |
|
235 qed (auto simp: normalize_mult mult_dvd_mono) |
|
236 from x y have "\<not>is_unit z" by (auto simp: mult_unit_dvd_iff) |
|
237 have "?fctrs x = (\<lambda>(p,p'). p * p') ` (?fctrs y \<times> ?fctrs z)" |
|
238 by (subst x) (rule normalized_factors_product) |
|
239 also have "\<not>y * z dvd y * 1" "\<not>y * z dvd 1 * z" |
|
240 by (subst dvd_times_left_cancel_iff dvd_times_right_cancel_iff; fact)+ |
|
241 hence "finite ((\<lambda>(p,p'). p * p') ` (?fctrs y \<times> ?fctrs z))" |
|
242 by (intro finite_imageI finite_cartesian_product less dvd_proper_imp_size_less) |
|
243 (auto simp: x) |
|
244 finally show ?thesis . |
|
245 qed |
|
246 qed |
|
247 next |
|
248 fix p |
|
249 assume "irreducible p" |
|
250 then show "prime_elem p" |
|
251 by (rule irreducible_imp_prime_elem_gcd) |
|
252 qed |
|
253 qed |
|
254 |
|
255 lemma Gcd_eucl_set [code]: |
|
256 "Gcd (set xs) = fold gcd xs 0" |
|
257 by (fact Gcd_set_eq_fold) |
|
258 |
|
259 lemma Lcm_eucl_set [code]: |
|
260 "Lcm (set xs) = fold lcm xs 1" |
|
261 by (fact Lcm_set_eq_fold) |
|
262 |
|
263 end |
|
264 |
|
265 hide_const (open) gcd lcm Gcd Lcm |
|
266 |
|
267 lemma prime_elem_int_abs_iff [simp]: |
|
268 fixes p :: int |
|
269 shows "prime_elem \<bar>p\<bar> \<longleftrightarrow> prime_elem p" |
|
270 using prime_elem_normalize_iff [of p] by simp |
|
271 |
|
272 lemma prime_elem_int_minus_iff [simp]: |
|
273 fixes p :: int |
|
274 shows "prime_elem (- p) \<longleftrightarrow> prime_elem p" |
|
275 using prime_elem_normalize_iff [of "- p"] by simp |
|
276 |
|
277 lemma prime_int_iff: |
|
278 fixes p :: int |
|
279 shows "prime p \<longleftrightarrow> p > 0 \<and> prime_elem p" |
|
280 by (auto simp add: prime_def dest: prime_elem_not_zeroI) |
|
281 |
|
282 |
|
283 subsection \<open>The (simple) euclidean algorithm as gcd computation\<close> |
|
284 |
|
285 class euclidean_semiring_gcd = euclidean_semiring + gcd + Gcd + |
|
286 assumes gcd_eucl: "Euclidean_Algorithm.gcd = GCD.gcd" |
|
287 and lcm_eucl: "Euclidean_Algorithm.lcm = GCD.lcm" |
|
288 assumes Gcd_eucl: "Euclidean_Algorithm.Gcd = GCD.Gcd" |
|
289 and Lcm_eucl: "Euclidean_Algorithm.Lcm = GCD.Lcm" |
|
290 begin |
|
291 |
|
292 subclass semiring_gcd |
|
293 unfolding gcd_eucl [symmetric] lcm_eucl [symmetric] |
|
294 by (fact semiring_gcd) |
|
295 |
|
296 subclass semiring_Gcd |
|
297 unfolding gcd_eucl [symmetric] lcm_eucl [symmetric] |
|
298 Gcd_eucl [symmetric] Lcm_eucl [symmetric] |
|
299 by (fact semiring_Gcd) |
|
300 |
|
301 subclass factorial_semiring_gcd |
|
302 proof |
|
303 show "gcd a b = gcd_factorial a b" for a b |
|
304 apply (rule sym) |
|
305 apply (rule gcdI) |
|
306 apply (fact gcd_lcm_factorial)+ |
|
307 done |
|
308 then show "lcm a b = lcm_factorial a b" for a b |
|
309 by (simp add: lcm_factorial_gcd_factorial lcm_gcd) |
|
310 show "Gcd A = Gcd_factorial A" for A |
|
311 apply (rule sym) |
|
312 apply (rule GcdI) |
|
313 apply (fact gcd_lcm_factorial)+ |
|
314 done |
|
315 show "Lcm A = Lcm_factorial A" for A |
|
316 apply (rule sym) |
|
317 apply (rule LcmI) |
|
318 apply (fact gcd_lcm_factorial)+ |
|
319 done |
|
320 qed |
|
321 |
|
322 lemma gcd_mod_right [simp]: |
|
323 "a \<noteq> 0 \<Longrightarrow> gcd a (b mod a) = gcd a b" |
|
324 unfolding gcd.commute [of a b] |
|
325 by (simp add: gcd_eucl [symmetric] local.gcd_mod) |
|
326 |
|
327 lemma gcd_mod_left [simp]: |
|
328 "b \<noteq> 0 \<Longrightarrow> gcd (a mod b) b = gcd a b" |
|
329 by (drule gcd_mod_right [of _ a]) (simp add: gcd.commute) |
|
330 |
|
331 lemma euclidean_size_gcd_le1 [simp]: |
|
332 assumes "a \<noteq> 0" |
|
333 shows "euclidean_size (gcd a b) \<le> euclidean_size a" |
|
334 proof - |
|
335 from gcd_dvd1 obtain c where A: "a = gcd a b * c" .. |
|
336 with assms have "c \<noteq> 0" |
|
337 by auto |
|
338 moreover from this |
|
339 have "euclidean_size (gcd a b) \<le> euclidean_size (gcd a b * c)" |
|
340 by (rule size_mult_mono) |
|
341 with A show ?thesis |
|
342 by simp |
|
343 qed |
|
344 |
|
345 lemma euclidean_size_gcd_le2 [simp]: |
|
346 "b \<noteq> 0 \<Longrightarrow> euclidean_size (gcd a b) \<le> euclidean_size b" |
|
347 by (subst gcd.commute, rule euclidean_size_gcd_le1) |
|
348 |
|
349 lemma euclidean_size_gcd_less1: |
|
350 assumes "a \<noteq> 0" and "\<not> a dvd b" |
|
351 shows "euclidean_size (gcd a b) < euclidean_size a" |
|
352 proof (rule ccontr) |
|
353 assume "\<not>euclidean_size (gcd a b) < euclidean_size a" |
|
354 with \<open>a \<noteq> 0\<close> have A: "euclidean_size (gcd a b) = euclidean_size a" |
|
355 by (intro le_antisym, simp_all) |
|
356 have "a dvd gcd a b" |
|
357 by (rule dvd_euclidean_size_eq_imp_dvd) (simp_all add: assms A) |
|
358 hence "a dvd b" using dvd_gcdD2 by blast |
|
359 with \<open>\<not> a dvd b\<close> show False by contradiction |
|
360 qed |
|
361 |
|
362 lemma euclidean_size_gcd_less2: |
|
363 assumes "b \<noteq> 0" and "\<not> b dvd a" |
|
364 shows "euclidean_size (gcd a b) < euclidean_size b" |
|
365 using assms by (subst gcd.commute, rule euclidean_size_gcd_less1) |
|
366 |
|
367 lemma euclidean_size_lcm_le1: |
|
368 assumes "a \<noteq> 0" and "b \<noteq> 0" |
|
369 shows "euclidean_size a \<le> euclidean_size (lcm a b)" |
|
370 proof - |
|
371 have "a dvd lcm a b" by (rule dvd_lcm1) |
|
372 then obtain c where A: "lcm a b = a * c" .. |
|
373 with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "c \<noteq> 0" by (auto simp: lcm_eq_0_iff) |
|
374 then show ?thesis by (subst A, intro size_mult_mono) |
|
375 qed |
|
376 |
|
377 lemma euclidean_size_lcm_le2: |
|
378 "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> euclidean_size b \<le> euclidean_size (lcm a b)" |
|
379 using euclidean_size_lcm_le1 [of b a] by (simp add: ac_simps) |
|
380 |
|
381 lemma euclidean_size_lcm_less1: |
|
382 assumes "b \<noteq> 0" and "\<not> b dvd a" |
|
383 shows "euclidean_size a < euclidean_size (lcm a b)" |
|
384 proof (rule ccontr) |
|
385 from assms have "a \<noteq> 0" by auto |
|
386 assume "\<not>euclidean_size a < euclidean_size (lcm a b)" |
|
387 with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "euclidean_size (lcm a b) = euclidean_size a" |
|
388 by (intro le_antisym, simp, intro euclidean_size_lcm_le1) |
|
389 with assms have "lcm a b dvd a" |
|
390 by (rule_tac dvd_euclidean_size_eq_imp_dvd) (auto simp: lcm_eq_0_iff) |
|
391 hence "b dvd a" by (rule lcm_dvdD2) |
|
392 with \<open>\<not>b dvd a\<close> show False by contradiction |
|
393 qed |
|
394 |
|
395 lemma euclidean_size_lcm_less2: |
|
396 assumes "a \<noteq> 0" and "\<not> a dvd b" |
|
397 shows "euclidean_size b < euclidean_size (lcm a b)" |
|
398 using assms euclidean_size_lcm_less1 [of a b] by (simp add: ac_simps) |
|
399 |
|
400 end |
|
401 |
|
402 lemma factorial_euclidean_semiring_gcdI: |
|
403 "OFCLASS('a::{factorial_semiring_gcd, euclidean_semiring}, euclidean_semiring_gcd_class)" |
|
404 proof |
|
405 interpret semiring_Gcd 1 0 times |
|
406 Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm |
|
407 Euclidean_Algorithm.Gcd Euclidean_Algorithm.Lcm |
|
408 divide plus minus unit_factor normalize |
|
409 rewrites "dvd.dvd op * = Rings.dvd" |
|
410 by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff) |
|
411 show [simp]: "Euclidean_Algorithm.gcd = (gcd :: 'a \<Rightarrow> _)" |
|
412 proof (rule ext)+ |
|
413 fix a b :: 'a |
|
414 show "Euclidean_Algorithm.gcd a b = gcd a b" |
|
415 proof (induct a b rule: eucl_induct) |
|
416 case zero |
|
417 then show ?case |
|
418 by simp |
|
419 next |
|
420 case (mod a b) |
|
421 moreover have "gcd b (a mod b) = gcd b a" |
|
422 using GCD.gcd_add_mult [of b "a div b" "a mod b", symmetric] |
|
423 by (simp add: div_mult_mod_eq) |
|
424 ultimately show ?case |
|
425 by (simp add: Euclidean_Algorithm.gcd_mod ac_simps) |
|
426 qed |
|
427 qed |
|
428 show [simp]: "Euclidean_Algorithm.Lcm = (Lcm :: 'a set \<Rightarrow> _)" |
|
429 by (auto intro!: Lcm_eqI GCD.dvd_Lcm GCD.Lcm_least) |
|
430 show "Euclidean_Algorithm.lcm = (lcm :: 'a \<Rightarrow> _)" |
|
431 by (simp add: fun_eq_iff Euclidean_Algorithm.lcm_def semiring_gcd_class.lcm_gcd) |
|
432 show "Euclidean_Algorithm.Gcd = (Gcd :: 'a set \<Rightarrow> _)" |
|
433 by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm) |
|
434 qed |
|
435 |
|
436 |
|
437 subsection \<open>The extended euclidean algorithm\<close> |
|
438 |
|
439 class euclidean_ring_gcd = euclidean_semiring_gcd + idom |
|
440 begin |
|
441 |
|
442 subclass euclidean_ring .. |
|
443 subclass ring_gcd .. |
|
444 subclass factorial_ring_gcd .. |
|
445 |
|
446 function euclid_ext_aux :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a \<times> 'a) \<times> 'a" |
|
447 where "euclid_ext_aux s' s t' t r' r = ( |
|
448 if r = 0 then let c = 1 div unit_factor r' in ((s' * c, t' * c), normalize r') |
|
449 else let q = r' div r |
|
450 in euclid_ext_aux s (s' - q * s) t (t' - q * t) r (r' mod r))" |
|
451 by auto |
|
452 termination |
|
453 by (relation "measure (\<lambda>(_, _, _, _, _, b). euclidean_size b)") |
|
454 (simp_all add: mod_size_less) |
|
455 |
|
456 abbreviation (input) euclid_ext :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<times> 'a) \<times> 'a" |
|
457 where "euclid_ext \<equiv> euclid_ext_aux 1 0 0 1" |
|
458 |
|
459 lemma |
|
460 assumes "gcd r' r = gcd a b" |
|
461 assumes "s' * a + t' * b = r'" |
|
462 assumes "s * a + t * b = r" |
|
463 assumes "euclid_ext_aux s' s t' t r' r = ((x, y), c)" |
|
464 shows euclid_ext_aux_eq_gcd: "c = gcd a b" |
|
465 and euclid_ext_aux_bezout: "x * a + y * b = gcd a b" |
|
466 proof - |
|
467 have "case euclid_ext_aux s' s t' t r' r of ((x, y), c) \<Rightarrow> |
|
468 x * a + y * b = c \<and> c = gcd a b" (is "?P (euclid_ext_aux s' s t' t r' r)") |
|
469 using assms(1-3) |
|
470 proof (induction s' s t' t r' r rule: euclid_ext_aux.induct) |
|
471 case (1 s' s t' t r' r) |
|
472 show ?case |
|
473 proof (cases "r = 0") |
|
474 case True |
|
475 hence "euclid_ext_aux s' s t' t r' r = |
|
476 ((s' div unit_factor r', t' div unit_factor r'), normalize r')" |
|
477 by (subst euclid_ext_aux.simps) (simp add: Let_def) |
|
478 also have "?P \<dots>" |
|
479 proof safe |
|
480 have "s' div unit_factor r' * a + t' div unit_factor r' * b = |
|
481 (s' * a + t' * b) div unit_factor r'" |
|
482 by (cases "r' = 0") (simp_all add: unit_div_commute) |
|
483 also have "s' * a + t' * b = r'" by fact |
|
484 also have "\<dots> div unit_factor r' = normalize r'" by simp |
|
485 finally show "s' div unit_factor r' * a + t' div unit_factor r' * b = normalize r'" . |
|
486 next |
|
487 from "1.prems" True show "normalize r' = gcd a b" |
|
488 by simp |
|
489 qed |
|
490 finally show ?thesis . |
|
491 next |
|
492 case False |
|
493 hence "euclid_ext_aux s' s t' t r' r = |
|
494 euclid_ext_aux s (s' - r' div r * s) t (t' - r' div r * t) r (r' mod r)" |
|
495 by (subst euclid_ext_aux.simps) (simp add: Let_def) |
|
496 also from "1.prems" False have "?P \<dots>" |
|
497 proof (intro "1.IH") |
|
498 have "(s' - r' div r * s) * a + (t' - r' div r * t) * b = |
|
499 (s' * a + t' * b) - r' div r * (s * a + t * b)" by (simp add: algebra_simps) |
|
500 also have "s' * a + t' * b = r'" by fact |
|
501 also have "s * a + t * b = r" by fact |
|
502 also have "r' - r' div r * r = r' mod r" using div_mult_mod_eq [of r' r] |
|
503 by (simp add: algebra_simps) |
|
504 finally show "(s' - r' div r * s) * a + (t' - r' div r * t) * b = r' mod r" . |
|
505 qed (auto simp: gcd_mod_right algebra_simps minus_mod_eq_div_mult [symmetric] gcd.commute) |
|
506 finally show ?thesis . |
|
507 qed |
|
508 qed |
|
509 with assms(4) show "c = gcd a b" "x * a + y * b = gcd a b" |
|
510 by simp_all |
|
511 qed |
|
512 |
|
513 declare euclid_ext_aux.simps [simp del] |
|
514 |
|
515 definition bezout_coefficients :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a" |
|
516 where [code]: "bezout_coefficients a b = fst (euclid_ext a b)" |
|
517 |
|
518 lemma bezout_coefficients_0: |
|
519 "bezout_coefficients a 0 = (1 div unit_factor a, 0)" |
|
520 by (simp add: bezout_coefficients_def euclid_ext_aux.simps) |
|
521 |
|
522 lemma bezout_coefficients_left_0: |
|
523 "bezout_coefficients 0 a = (0, 1 div unit_factor a)" |
|
524 by (simp add: bezout_coefficients_def euclid_ext_aux.simps) |
|
525 |
|
526 lemma bezout_coefficients: |
|
527 assumes "bezout_coefficients a b = (x, y)" |
|
528 shows "x * a + y * b = gcd a b" |
|
529 using assms by (simp add: bezout_coefficients_def |
|
530 euclid_ext_aux_bezout [of a b a b 1 0 0 1 x y] prod_eq_iff) |
|
531 |
|
532 lemma bezout_coefficients_fst_snd: |
|
533 "fst (bezout_coefficients a b) * a + snd (bezout_coefficients a b) * b = gcd a b" |
|
534 by (rule bezout_coefficients) simp |
|
535 |
|
536 lemma euclid_ext_eq [simp]: |
|
537 "euclid_ext a b = (bezout_coefficients a b, gcd a b)" (is "?p = ?q") |
|
538 proof |
|
539 show "fst ?p = fst ?q" |
|
540 by (simp add: bezout_coefficients_def) |
|
541 have "snd (euclid_ext_aux 1 0 0 1 a b) = gcd a b" |
|
542 by (rule euclid_ext_aux_eq_gcd [of a b a b 1 0 0 1]) |
|
543 (simp_all add: prod_eq_iff) |
|
544 then show "snd ?p = snd ?q" |
|
545 by simp |
|
546 qed |
|
547 |
|
548 declare euclid_ext_eq [symmetric, code_unfold] |
|
549 |
|
550 end |
|
551 |
|
552 |
|
553 subsection \<open>Typical instances\<close> |
|
554 |
|
555 instance nat :: euclidean_semiring_gcd |
|
556 proof |
|
557 interpret semiring_Gcd 1 0 times |
|
558 "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm" |
|
559 "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm" |
|
560 divide plus minus unit_factor normalize |
|
561 rewrites "dvd.dvd op * = Rings.dvd" |
|
562 by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff) |
|
563 show [simp]: "(Euclidean_Algorithm.gcd :: nat \<Rightarrow> _) = gcd" |
|
564 proof (rule ext)+ |
|
565 fix m n :: nat |
|
566 show "Euclidean_Algorithm.gcd m n = gcd m n" |
|
567 proof (induct m n rule: eucl_induct) |
|
568 case zero |
|
569 then show ?case |
|
570 by simp |
|
571 next |
|
572 case (mod m n) |
|
573 then have "gcd n (m mod n) = gcd n m" |
|
574 using gcd_nat.simps [of m n] by (simp add: ac_simps) |
|
575 with mod show ?case |
|
576 by (simp add: Euclidean_Algorithm.gcd_mod ac_simps) |
|
577 qed |
|
578 qed |
|
579 show [simp]: "(Euclidean_Algorithm.Lcm :: nat set \<Rightarrow> _) = Lcm" |
|
580 by (auto intro!: ext Lcm_eqI) |
|
581 show "(Euclidean_Algorithm.lcm :: nat \<Rightarrow> _) = lcm" |
|
582 by (simp add: fun_eq_iff Euclidean_Algorithm.lcm_def semiring_gcd_class.lcm_gcd) |
|
583 show "(Euclidean_Algorithm.Gcd :: nat set \<Rightarrow> _) = Gcd" |
|
584 by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm) |
|
585 qed |
|
586 |
|
587 instance int :: euclidean_ring_gcd |
|
588 proof |
|
589 interpret semiring_Gcd 1 0 times |
|
590 "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm" |
|
591 "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm" |
|
592 divide plus minus unit_factor normalize |
|
593 rewrites "dvd.dvd op * = Rings.dvd" |
|
594 by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff) |
|
595 show [simp]: "(Euclidean_Algorithm.gcd :: int \<Rightarrow> _) = gcd" |
|
596 proof (rule ext)+ |
|
597 fix k l :: int |
|
598 show "Euclidean_Algorithm.gcd k l = gcd k l" |
|
599 proof (induct k l rule: eucl_induct) |
|
600 case zero |
|
601 then show ?case |
|
602 by simp |
|
603 next |
|
604 case (mod k l) |
|
605 have "gcd l (k mod l) = gcd l k" |
|
606 proof (cases l "0::int" rule: linorder_cases) |
|
607 case less |
|
608 then show ?thesis |
|
609 using gcd_non_0_int [of "- l" "- k"] by (simp add: ac_simps) |
|
610 next |
|
611 case equal |
|
612 with mod show ?thesis |
|
613 by simp |
|
614 next |
|
615 case greater |
|
616 then show ?thesis |
|
617 using gcd_non_0_int [of l k] by (simp add: ac_simps) |
|
618 qed |
|
619 with mod show ?case |
|
620 by (simp add: Euclidean_Algorithm.gcd_mod ac_simps) |
|
621 qed |
|
622 qed |
|
623 show [simp]: "(Euclidean_Algorithm.Lcm :: int set \<Rightarrow> _) = Lcm" |
|
624 by (auto intro!: ext Lcm_eqI) |
|
625 show "(Euclidean_Algorithm.lcm :: int \<Rightarrow> _) = lcm" |
|
626 by (simp add: fun_eq_iff Euclidean_Algorithm.lcm_def semiring_gcd_class.lcm_gcd) |
|
627 show "(Euclidean_Algorithm.Gcd :: int set \<Rightarrow> _) = Gcd" |
|
628 by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm) |
|
629 qed |
|
630 |
|
631 end |