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