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