# HG changeset patch # User haftmann # Date 1483561709 -3600 # Node ID 340db65fd2c1d87ea110392e3a54f7fd7832a7c6 # Parent ae0bbc8e45ad9b9733f8972acb7cb0dfff5ed933 reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings diff -r ae0bbc8e45ad -r 340db65fd2c1 NEWS --- a/NEWS Wed Jan 04 21:28:29 2017 +0100 +++ b/NEWS Wed Jan 04 21:28:29 2017 +0100 @@ -28,6 +28,15 @@ unique_euclidean_(semi)ring; instantiation requires provision of a euclidean size. +* Reworking of theory Euclidean_Algorithm in session HOL-Number_Theory: + - Euclidean induction is available as rule eucl_induct; + - Constants Euclidean_Algorithm.gcd, Euclidean_Algorithm.lcm, + Euclidean_Algorithm.Gcd and Euclidean_Algorithm.Lcm allow + easy instantiation of euclidean (semi)rings as GCD (semi)rings. + - Coefficients obtained by extended euclidean algorithm are + available as "bezout_coefficients". +INCOMPATIBILITY. + * Swapped orientation of congruence rules mod_add_left_eq, mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq, mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq, diff -r ae0bbc8e45ad -r 340db65fd2c1 src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy --- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Wed Jan 04 21:28:29 2017 +0100 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Wed Jan 04 21:28:29 2017 +0100 @@ -20,64 +20,31 @@ in fold Code.del_eqns consts thy end \ \ \drop technical stuff from \Quickcheck_Narrowing\ which is tailored towards Haskell\ -(* - The following code equations have to be deleted because they use - lists to implement sets in the code generetor. -*) - -lemma [code, code del]: - "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" .. - -lemma [code, code del]: - "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" .. - -lemma [code, code del]: - "pred_of_set = pred_of_set" .. - -lemma [code, code del]: - "Wellfounded.acc = Wellfounded.acc" .. - -lemma [code, code del]: - "Cardinality.card' = Cardinality.card'" .. - -lemma [code, code del]: - "Cardinality.finite' = Cardinality.finite'" .. - -lemma [code, code del]: - "Cardinality.subset' = Cardinality.subset'" .. - -lemma [code, code del]: - "Cardinality.eq_set = Cardinality.eq_set" .. +text \ + The following code equations have to be deleted because they use + lists to implement sets in the code generetor. +\ -lemma [code, code del]: - "(Gcd :: nat set \ nat) = Gcd" .. - -lemma [code, code del]: - "(Lcm :: nat set \ nat) = Lcm" .. - -lemma [code, code del]: - "(Gcd :: int set \ int) = Gcd" .. - -lemma [code, code del]: - "(Lcm :: int set \ int) = Lcm" .. - -lemma [code, code del]: - "(Gcd :: _ poly set \ _) = Gcd" .. - -lemma [code, code del]: - "(Lcm :: _ poly set \ _) = Lcm" .. - -lemma [code, code del]: - "Gcd_eucl = Gcd_eucl" .. - -lemma [code, code del]: - "Lcm_eucl = Lcm_eucl" .. - -lemma [code, code del]: - "permutations_of_set = permutations_of_set" .. - -lemma [code, code del]: - "permutations_of_multiset = permutations_of_multiset" .. +declare [[code drop: + Sup_pred_inst.Sup_pred + Inf_pred_inst.Inf_pred + pred_of_set + Wellfounded.acc + Cardinality.card' + Cardinality.finite' + Cardinality.subset' + Cardinality.eq_set + "Gcd :: nat set \ nat" + "Lcm :: nat set \ nat" + "Gcd :: int set \ int" + "Lcm :: int set \ int" + "Gcd :: _ poly set \ _" + "Lcm :: _ poly set \ _" + Euclidean_Algorithm.Gcd + Euclidean_Algorithm.Lcm + permutations_of_set + permutations_of_multiset +]] (* If the code generation ends with an exception with the following message: diff -r ae0bbc8e45ad -r 340db65fd2c1 src/HOL/Library/Field_as_Ring.thy --- a/src/HOL/Library/Field_as_Ring.thy Wed Jan 04 21:28:29 2017 +0100 +++ b/src/HOL/Library/Field_as_Ring.thy Wed Jan 04 21:28:29 2017 +0100 @@ -43,13 +43,13 @@ begin definition gcd_real :: "real \ real \ real" where - "gcd_real = gcd_eucl" + "gcd_real = Euclidean_Algorithm.gcd" definition lcm_real :: "real \ real \ real" where - "lcm_real = lcm_eucl" + "lcm_real = Euclidean_Algorithm.lcm" definition Gcd_real :: "real set \ real" where - "Gcd_real = Gcd_eucl" + "Gcd_real = Euclidean_Algorithm.Gcd" definition Lcm_real :: "real set \ real" where - "Lcm_real = Lcm_eucl" + "Lcm_real = Euclidean_Algorithm.Lcm" instance by standard (simp_all add: gcd_real_def lcm_real_def Gcd_real_def Lcm_real_def) @@ -74,13 +74,13 @@ begin definition gcd_rat :: "rat \ rat \ rat" where - "gcd_rat = gcd_eucl" + "gcd_rat = Euclidean_Algorithm.gcd" definition lcm_rat :: "rat \ rat \ rat" where - "lcm_rat = lcm_eucl" + "lcm_rat = Euclidean_Algorithm.lcm" definition Gcd_rat :: "rat set \ rat" where - "Gcd_rat = Gcd_eucl" + "Gcd_rat = Euclidean_Algorithm.Gcd" definition Lcm_rat :: "rat set \ rat" where - "Lcm_rat = Lcm_eucl" + "Lcm_rat = Euclidean_Algorithm.Lcm" instance by standard (simp_all add: gcd_rat_def lcm_rat_def Gcd_rat_def Lcm_rat_def) @@ -105,13 +105,13 @@ begin definition gcd_complex :: "complex \ complex \ complex" where - "gcd_complex = gcd_eucl" + "gcd_complex = Euclidean_Algorithm.gcd" definition lcm_complex :: "complex \ complex \ complex" where - "lcm_complex = lcm_eucl" + "lcm_complex = Euclidean_Algorithm.lcm" definition Gcd_complex :: "complex set \ complex" where - "Gcd_complex = Gcd_eucl" + "Gcd_complex = Euclidean_Algorithm.Gcd" definition Lcm_complex :: "complex set \ complex" where - "Lcm_complex = Lcm_eucl" + "Lcm_complex = Euclidean_Algorithm.Lcm" instance by standard (simp_all add: gcd_complex_def lcm_complex_def Gcd_complex_def Lcm_complex_def) diff -r ae0bbc8e45ad -r 340db65fd2c1 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Wed Jan 04 21:28:29 2017 +0100 +++ b/src/HOL/Library/Formal_Power_Series.thy Wed Jan 04 21:28:29 2017 +0100 @@ -1421,10 +1421,10 @@ instantiation fps :: (field) euclidean_ring_gcd begin -definition fps_gcd_def: "(gcd :: 'a fps \ _) = gcd_eucl" -definition fps_lcm_def: "(lcm :: 'a fps \ _) = lcm_eucl" -definition fps_Gcd_def: "(Gcd :: 'a fps set \ _) = Gcd_eucl" -definition fps_Lcm_def: "(Lcm :: 'a fps set \ _) = Lcm_eucl" +definition fps_gcd_def: "(gcd :: 'a fps \ _) = Euclidean_Algorithm.gcd" +definition fps_lcm_def: "(lcm :: 'a fps \ _) = Euclidean_Algorithm.lcm" +definition fps_Gcd_def: "(Gcd :: 'a fps set \ _) = Euclidean_Algorithm.Gcd" +definition fps_Lcm_def: "(Lcm :: 'a fps set \ _) = Euclidean_Algorithm.Lcm" instance by standard (simp_all add: fps_gcd_def fps_lcm_def fps_Gcd_def fps_Lcm_def) end diff -r ae0bbc8e45ad -r 340db65fd2c1 src/HOL/Library/Polynomial_Factorial.thy --- a/src/HOL/Library/Polynomial_Factorial.thy Wed Jan 04 21:28:29 2017 +0100 +++ b/src/HOL/Library/Polynomial_Factorial.thy Wed Jan 04 21:28:29 2017 +0100 @@ -1040,7 +1040,8 @@ end instance poly :: ("{field,factorial_ring_gcd}") euclidean_ring_gcd - by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def eucl_eq_factorial) + by (rule euclidean_ring_gcd_class.intro, rule factorial_euclidean_semiring_gcdI) + standard subsection \Polynomial GCD\ diff -r ae0bbc8e45ad -r 340db65fd2c1 src/HOL/Number_Theory/Euclidean_Algorithm.thy --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Jan 04 21:28:29 2017 +0100 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy Wed Jan 04 21:28:29 2017 +0100 @@ -9,24 +9,28 @@ "~~/src/HOL/Number_Theory/Factorial_Ring" begin +subsection \Generic construction of the (simple) euclidean algorithm\ + context euclidean_semiring begin -function gcd_eucl :: "'a \ 'a \ 'a" -where - "gcd_eucl a b = (if b = 0 then normalize a else gcd_eucl b (a mod b))" +context +begin + +qualified function gcd :: "'a \ 'a \ 'a" + where "gcd a b = (if b = 0 then normalize a else gcd b (a mod b))" by pat_completeness simp termination by (relation "measure (euclidean_size \ snd)") (simp_all add: mod_size_less) -declare gcd_eucl.simps [simp del] +declare gcd.simps [simp del] -lemma gcd_eucl_induct [case_names zero mod]: +lemma eucl_induct [case_names zero mod]: assumes H1: "\b. P b 0" and H2: "\a b. b \ 0 \ P b (a mod b) \ P a b" shows "P a b" -proof (induct a b rule: gcd_eucl.induct) - case ("1" a b) +proof (induct a b rule: gcd.induct) + case (1 a b) show ?case proof (cases "b = 0") case True then show "P a b" by simp (rule H1) @@ -38,425 +42,305 @@ by (blast intro: H2) qed qed - -definition lcm_eucl :: "'a \ 'a \ 'a" -where - "lcm_eucl a b = normalize (a * b) div gcd_eucl a b" + +qualified lemma gcd_0: + "gcd a 0 = normalize a" + by (simp add: gcd.simps [of a 0]) + +qualified lemma gcd_mod: + "a \ 0 \ gcd a (b mod a) = gcd b a" + by (simp add: gcd.simps [of b 0] gcd.simps [of b a]) -definition Lcm_eucl :: "'a set \ 'a" \ \ - Somewhat complicated definition of Lcm that has the advantage of working - for infinite sets as well\ -where - "Lcm_eucl A = (if \l. l \ 0 \ (\a\A. a dvd l) then +qualified definition lcm :: "'a \ 'a \ 'a" + where "lcm a b = normalize (a * b) div gcd a b" + +qualified definition Lcm :: "'a set \ 'a" \ + \Somewhat complicated definition of Lcm that has the advantage of working + for infinite sets as well\ + where + [code del]: "Lcm A = (if \l. l \ 0 \ (\a\A. a dvd l) then let l = SOME l. l \ 0 \ (\a\A. a dvd l) \ euclidean_size l = (LEAST n. \l. l \ 0 \ (\a\A. a dvd l) \ euclidean_size l = n) in normalize l else 0)" -definition Gcd_eucl :: "'a set \ 'a" -where - "Gcd_eucl A = Lcm_eucl {d. \a\A. d dvd a}" - -declare Lcm_eucl_def Gcd_eucl_def [code del] +qualified definition Gcd :: "'a set \ 'a" + where [code del]: "Gcd A = Lcm {d. \a\A. d dvd a}" -lemma gcd_eucl_0: - "gcd_eucl a 0 = normalize a" - by (simp add: gcd_eucl.simps [of a 0]) - -lemma gcd_eucl_0_left: - "gcd_eucl 0 a = normalize a" - by (simp_all add: gcd_eucl_0 gcd_eucl.simps [of 0 a]) +end -lemma gcd_eucl_non_0: - "b \ 0 \ gcd_eucl a b = gcd_eucl b (a mod b)" - by (simp add: gcd_eucl.simps [of a b] gcd_eucl.simps [of b 0]) - -lemma gcd_eucl_dvd1 [iff]: "gcd_eucl a b dvd a" - and gcd_eucl_dvd2 [iff]: "gcd_eucl a b dvd b" - by (induct a b rule: gcd_eucl_induct) - (simp_all add: gcd_eucl_0 gcd_eucl_non_0 dvd_mod_iff) - -lemma normalize_gcd_eucl [simp]: - "normalize (gcd_eucl a b) = gcd_eucl a b" - by (induct a b rule: gcd_eucl_induct) (simp_all add: gcd_eucl_0 gcd_eucl_non_0) - -lemma gcd_eucl_greatest: - fixes k a b :: 'a - shows "k dvd a \ k dvd b \ k dvd gcd_eucl a b" -proof (induct a b rule: gcd_eucl_induct) - case (zero a) from zero(1) show ?case by (rule dvd_trans) (simp add: gcd_eucl_0) +lemma semiring_gcd: + "class.semiring_gcd one zero times gcd lcm + divide plus minus normalize unit_factor" +proof + show "gcd a b dvd a" + and "gcd a b dvd b" for a b + by (induct a b rule: eucl_induct) + (simp_all add: local.gcd_0 local.gcd_mod dvd_mod_iff) next - case (mod a b) - then show ?case - by (simp add: gcd_eucl_non_0 dvd_mod_iff) -qed - -lemma gcd_euclI: - fixes gcd :: "'a \ 'a \ 'a" - assumes "d dvd a" "d dvd b" "normalize d = d" - "\k. k dvd a \ k dvd b \ k dvd d" - shows "gcd_eucl a b = d" - by (rule associated_eqI) (simp_all add: gcd_eucl_greatest assms) - -lemma eq_gcd_euclI: - fixes gcd :: "'a \ 'a \ 'a" - assumes "\a b. gcd a b dvd a" "\a b. gcd a b dvd b" "\a b. normalize (gcd a b) = gcd a b" - "\a b k. k dvd a \ k dvd b \ k dvd gcd a b" - shows "gcd = gcd_eucl" - by (intro ext, rule associated_eqI) (simp_all add: gcd_eucl_greatest assms) - -lemma gcd_eucl_zero [simp]: - "gcd_eucl a b = 0 \ a = 0 \ b = 0" - by (metis dvd_0_left dvd_refl gcd_eucl_dvd1 gcd_eucl_dvd2 gcd_eucl_greatest)+ - - -lemma dvd_Lcm_eucl [simp]: "a \ A \ a dvd Lcm_eucl A" - and Lcm_eucl_least: "(\a. a \ A \ a dvd b) \ Lcm_eucl A dvd b" - and unit_factor_Lcm_eucl [simp]: - "unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)" -proof - - have "(\a\A. a dvd Lcm_eucl A) \ (\l'. (\a\A. a dvd l') \ Lcm_eucl A dvd l') \ - unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)" (is ?thesis) - proof (cases "\l. l \ 0 \ (\a\A. a dvd l)") - case False - hence "Lcm_eucl A = 0" by (auto simp: Lcm_eucl_def) - with False show ?thesis by auto + show "c dvd a \ c dvd b \ c dvd gcd a b" for a b c + proof (induct a b rule: eucl_induct) + case (zero a) from \c dvd a\ show ?case + by (rule dvd_trans) (simp add: local.gcd_0) next - case True - then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \ 0 \ (\a\A. a dvd l\<^sub>0)" by blast - define n where "n = (LEAST n. \l. l \ 0 \ (\a\A. a dvd l) \ euclidean_size l = n)" - define l where "l = (SOME l. l \ 0 \ (\a\A. a dvd l) \ euclidean_size l = n)" - have "\l. l \ 0 \ (\a\A. a dvd l) \ euclidean_size l = n" - apply (subst n_def) - apply (rule LeastI[of _ "euclidean_size l\<^sub>0"]) - apply (rule exI[of _ l\<^sub>0]) - apply (simp add: l\<^sub>0_props) - done - from someI_ex[OF this] have "l \ 0" and "\a\A. a dvd l" and "euclidean_size l = n" - unfolding l_def by simp_all - { - fix l' assume "\a\A. a dvd l'" - with \\a\A. a dvd l\ have "\a\A. a dvd gcd_eucl l l'" by (auto intro: gcd_eucl_greatest) - moreover from \l \ 0\ have "gcd_eucl l l' \ 0" by simp - ultimately have "\b. b \ 0 \ (\a\A. a dvd b) \ - euclidean_size b = euclidean_size (gcd_eucl l l')" - by (intro exI[of _ "gcd_eucl l l'"], auto) - hence "euclidean_size (gcd_eucl l l') \ n" by (subst n_def) (rule Least_le) - moreover have "euclidean_size (gcd_eucl l l') \ n" - proof - - have "gcd_eucl l l' dvd l" by simp - then obtain a where "l = gcd_eucl l l' * a" unfolding dvd_def by blast - with \l \ 0\ have "a \ 0" by auto - hence "euclidean_size (gcd_eucl l l') \ euclidean_size (gcd_eucl l l' * a)" - by (rule size_mult_mono) - also have "gcd_eucl l l' * a = l" using \l = gcd_eucl l l' * a\ .. - also note \euclidean_size l = n\ - finally show "euclidean_size (gcd_eucl l l') \ n" . - qed - ultimately have *: "euclidean_size l = euclidean_size (gcd_eucl l l')" - by (intro le_antisym, simp_all add: \euclidean_size l = n\) - from \l \ 0\ have "l dvd gcd_eucl l l'" - by (rule dvd_euclidean_size_eq_imp_dvd) (auto simp add: *) - hence "l dvd l'" by (rule dvd_trans[OF _ gcd_eucl_dvd2]) - } - - with \(\a\A. a dvd l)\ and unit_factor_is_unit[OF \l \ 0\] and \l \ 0\ - have "(\a\A. a dvd normalize l) \ - (\l'. (\a\A. a dvd l') \ normalize l dvd l') \ - unit_factor (normalize l) = - (if normalize l = 0 then 0 else 1)" - by (auto simp: unit_simps) - also from True have "normalize l = Lcm_eucl A" - by (simp add: Lcm_eucl_def Let_def n_def l_def) - finally show ?thesis . + case (mod a b) + then show ?case + by (simp add: local.gcd_mod dvd_mod_iff) qed - note A = this - - {fix a assume "a \ A" then show "a dvd Lcm_eucl A" using A by blast} - {fix b assume "\a. a \ A \ a dvd b" then show "Lcm_eucl A dvd b" using A by blast} - from A show "unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)" by blast -qed - -lemma normalize_Lcm_eucl [simp]: - "normalize (Lcm_eucl A) = Lcm_eucl A" -proof (cases "Lcm_eucl A = 0") - case True then show ?thesis by simp next - case False - have "unit_factor (Lcm_eucl A) * normalize (Lcm_eucl A) = Lcm_eucl A" - by (fact unit_factor_mult_normalize) - with False show ?thesis by simp -qed - -lemma eq_Lcm_euclI: - fixes lcm :: "'a set \ 'a" - assumes "\A a. a \ A \ a dvd lcm A" and "\A c. (\a. a \ A \ a dvd c) \ lcm A dvd c" - "\A. normalize (lcm A) = lcm A" shows "lcm = Lcm_eucl" - by (intro ext, rule associated_eqI) (auto simp: assms intro: Lcm_eucl_least) - -lemma Gcd_eucl_dvd: "a \ A \ Gcd_eucl A dvd a" - unfolding Gcd_eucl_def by (auto intro: Lcm_eucl_least) - -lemma Gcd_eucl_greatest: "(\x. x \ A \ d dvd x) \ d dvd Gcd_eucl A" - unfolding Gcd_eucl_def by auto - -lemma normalize_Gcd_eucl [simp]: "normalize (Gcd_eucl A) = Gcd_eucl A" - by (simp add: Gcd_eucl_def) - -lemma Lcm_euclI: - assumes "\x. x \ A \ x dvd d" "\d'. (\x. x \ A \ x dvd d') \ d dvd d'" "normalize d = d" - shows "Lcm_eucl A = d" -proof - - have "normalize (Lcm_eucl A) = normalize d" - by (intro associatedI) (auto intro: dvd_Lcm_eucl Lcm_eucl_least assms) - thus ?thesis by (simp add: assms) + show "normalize (gcd a b) = gcd a b" for a b + by (induct a b rule: eucl_induct) + (simp_all add: local.gcd_0 local.gcd_mod) +next + show "lcm a b = normalize (a * b) div gcd a b" for a b + by (fact local.lcm_def) qed -lemma Gcd_euclI: - assumes "\x. x \ A \ d dvd x" "\d'. (\x. x \ A \ d' dvd x) \ d' dvd d" "normalize d = d" - shows "Gcd_eucl A = d" -proof - - have "normalize (Gcd_eucl A) = normalize d" - by (intro associatedI) (auto intro: Gcd_eucl_dvd Gcd_eucl_greatest assms) - thus ?thesis by (simp add: assms) -qed +interpretation semiring_gcd one zero times gcd lcm + divide plus minus normalize unit_factor + by (fact semiring_gcd) -lemmas lcm_gcd_eucl_facts = - gcd_eucl_dvd1 gcd_eucl_dvd2 gcd_eucl_greatest normalize_gcd_eucl lcm_eucl_def - Gcd_eucl_def Gcd_eucl_dvd Gcd_eucl_greatest normalize_Gcd_eucl - dvd_Lcm_eucl Lcm_eucl_least normalize_Lcm_eucl - -lemma normalized_factors_product: - "{p. p dvd a * b \ normalize p = p} = - (\(x,y). x * y) ` ({p. p dvd a \ normalize p = p} \ {p. p dvd b \ normalize p = p})" -proof safe - fix p assume p: "p dvd a * b" "normalize p = p" - interpret semiring_gcd 1 0 "op *" gcd_eucl lcm_eucl "op div" "op +" "op -" normalize unit_factor - by standard (rule lcm_gcd_eucl_facts; assumption)+ - from dvd_productE[OF p(1)] guess x y . note xy = this - define x' y' where "x' = normalize x" and "y' = normalize y" - have "p = x' * y'" - by (subst p(2) [symmetric]) (simp add: xy x'_def y'_def normalize_mult) - moreover from xy have "normalize x' = x'" "normalize y' = y'" "x' dvd a" "y' dvd b" - by (simp_all add: x'_def y'_def) - ultimately show "p \ (\(x, y). x * y) ` - ({p. p dvd a \ normalize p = p} \ {p. p dvd b \ normalize p = p})" - by blast -qed (auto simp: normalize_mult mult_dvd_mono) - - -subclass factorial_semiring -proof (standard, rule factorial_semiring_altI_aux) - fix x assume "x \ 0" - thus "finite {p. p dvd x \ normalize p = p}" - proof (induction "euclidean_size x" arbitrary: x rule: less_induct) - case (less x) - show ?case - proof (cases "\y. y dvd x \ \x dvd y \ \is_unit y") +lemma semiring_Gcd: + "class.semiring_Gcd one zero times gcd lcm Gcd Lcm + divide plus minus normalize unit_factor" +proof - + show ?thesis + proof + have "(\a\A. a dvd Lcm A) \ (\b. (\a\A. a dvd b) \ Lcm A dvd b)" for A + proof (cases "\l. l \ 0 \ (\a\A. a dvd l)") case False - have "{p. p dvd x \ normalize p = p} \ {1, normalize x}" - proof - fix p assume p: "p \ {p. p dvd x \ normalize p = p}" - with False have "is_unit p \ x dvd p" by blast - thus "p \ {1, normalize x}" - proof (elim disjE) - assume "is_unit p" - hence "normalize p = 1" by (simp add: is_unit_normalize) - with p show ?thesis by simp - next - assume "x dvd p" - with p have "normalize p = normalize x" by (intro associatedI) simp_all - with p show ?thesis by simp - qed - qed - moreover have "finite \" by simp - ultimately show ?thesis by (rule finite_subset) - + then have "Lcm A = 0" + by (auto simp add: local.Lcm_def) + with False show ?thesis + by auto next case True - then obtain y where y: "y dvd x" "\x dvd y" "\is_unit y" by blast - define z where "z = x div y" - let ?fctrs = "\x. {p. p dvd x \ normalize p = p}" - from y have x: "x = y * z" by (simp add: z_def) - with less.prems have "y \ 0" "z \ 0" by auto - from x y have "\is_unit z" by (auto simp: mult_unit_dvd_iff) - have "?fctrs x = (\(p,p'). p * p') ` (?fctrs y \ ?fctrs z)" - by (subst x) (rule normalized_factors_product) - also have "\y * z dvd y * 1" "\y * z dvd 1 * z" - by (subst dvd_times_left_cancel_iff dvd_times_right_cancel_iff; fact)+ - hence "finite ((\(p,p'). p * p') ` (?fctrs y \ ?fctrs z))" - by (intro finite_imageI finite_cartesian_product less dvd_proper_imp_size_less) - (auto simp: x) + then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \ 0" "\a\A. a dvd l\<^sub>0" by blast + define n where "n = (LEAST n. \l. l \ 0 \ (\a\A. a dvd l) \ euclidean_size l = n)" + define l where "l = (SOME l. l \ 0 \ (\a\A. a dvd l) \ euclidean_size l = n)" + have "\l. l \ 0 \ (\a\A. a dvd l) \ euclidean_size l = n" + apply (subst n_def) + apply (rule LeastI [of _ "euclidean_size l\<^sub>0"]) + apply (rule exI [of _ l\<^sub>0]) + apply (simp add: l\<^sub>0_props) + done + from someI_ex [OF this] have "l \ 0" and "\a\A. a dvd l" + and "euclidean_size l = n" + unfolding l_def by simp_all + { + fix l' assume "\a\A. a dvd l'" + with \\a\A. a dvd l\ have "\a\A. a dvd gcd l l'" + by (auto intro: gcd_greatest) + moreover from \l \ 0\ have "gcd l l' \ 0" + by simp + ultimately have "\b. b \ 0 \ (\a\A. a dvd b) \ + euclidean_size b = euclidean_size (gcd l l')" + by (intro exI [of _ "gcd l l'"], auto) + then have "euclidean_size (gcd l l') \ n" + by (subst n_def) (rule Least_le) + moreover have "euclidean_size (gcd l l') \ n" + proof - + have "gcd l l' dvd l" + by simp + then obtain a where "l = gcd l l' * a" .. + with \l \ 0\ have "a \ 0" + by auto + hence "euclidean_size (gcd l l') \ euclidean_size (gcd l l' * a)" + by (rule size_mult_mono) + also have "gcd l l' * a = l" using \l = gcd l l' * a\ .. + also note \euclidean_size l = n\ + finally show "euclidean_size (gcd l l') \ n" . + qed + ultimately have *: "euclidean_size l = euclidean_size (gcd l l')" + by (intro le_antisym, simp_all add: \euclidean_size l = n\) + from \l \ 0\ have "l dvd gcd l l'" + by (rule dvd_euclidean_size_eq_imp_dvd) (auto simp add: *) + hence "l dvd l'" by (rule dvd_trans [OF _ gcd_dvd2]) + } + with \\a\A. a dvd l\ and \l \ 0\ + have "(\a\A. a dvd normalize l) \ + (\l'. (\a\A. a dvd l') \ normalize l dvd l')" + by auto + also from True have "normalize l = Lcm A" + by (simp add: local.Lcm_def Let_def n_def l_def) finally show ?thesis . qed - qed -next - interpret semiring_gcd 1 0 "op *" gcd_eucl lcm_eucl "op div" "op +" "op -" normalize unit_factor - by standard (rule lcm_gcd_eucl_facts; assumption)+ - fix p assume p: "irreducible p" - thus "prime_elem p" by (rule irreducible_imp_prime_elem_gcd) -qed - -lemma gcd_eucl_eq_gcd_factorial: "gcd_eucl = gcd_factorial" - by (intro ext gcd_euclI gcd_lcm_factorial) - -lemma lcm_eucl_eq_lcm_factorial: "lcm_eucl = lcm_factorial" - by (intro ext) (simp add: lcm_eucl_def lcm_factorial_gcd_factorial gcd_eucl_eq_gcd_factorial) - -lemma Gcd_eucl_eq_Gcd_factorial: "Gcd_eucl = Gcd_factorial" - by (intro ext Gcd_euclI gcd_lcm_factorial) - -lemma Lcm_eucl_eq_Lcm_factorial: "Lcm_eucl = Lcm_factorial" - by (intro ext Lcm_euclI gcd_lcm_factorial) - -lemmas eucl_eq_factorial = - gcd_eucl_eq_gcd_factorial lcm_eucl_eq_lcm_factorial - Gcd_eucl_eq_Gcd_factorial Lcm_eucl_eq_Lcm_factorial - -end - -context euclidean_ring -begin - -function euclid_ext_aux :: "'a \ _" where - "euclid_ext_aux r' r s' s t' t = ( - if r = 0 then let c = 1 div unit_factor r' in (s' * c, t' * c, normalize r') - else let q = r' div r - in euclid_ext_aux r (r' mod r) s (s' - q * s) t (t' - q * t))" -by auto -termination by (relation "measure (\(_,b,_,_,_,_). euclidean_size b)") (simp_all add: mod_size_less) - -declare euclid_ext_aux.simps [simp del] - -lemma euclid_ext_aux_correct: - assumes "gcd_eucl r' r = gcd_eucl a b" - assumes "s' * a + t' * b = r'" - assumes "s * a + t * b = r" - shows "case euclid_ext_aux r' r s' s t' t of (x,y,c) \ - x * a + y * b = c \ c = gcd_eucl a b" (is "?P (euclid_ext_aux r' r s' s t' t)") -using assms -proof (induction r' r s' s t' t rule: euclid_ext_aux.induct) - case (1 r' r s' s t' t) - show ?case - proof (cases "r = 0") - case True - hence "euclid_ext_aux r' r s' s t' t = - (s' div unit_factor r', t' div unit_factor r', normalize r')" - by (subst euclid_ext_aux.simps) (simp add: Let_def) - also have "?P \" - proof safe - have "s' div unit_factor r' * a + t' div unit_factor r' * b = - (s' * a + t' * b) div unit_factor r'" - by (cases "r' = 0") (simp_all add: unit_div_commute) - also have "s' * a + t' * b = r'" by fact - also have "\ div unit_factor r' = normalize r'" by simp - finally show "s' div unit_factor r' * a + t' div unit_factor r' * b = normalize r'" . - next - from "1.prems" True show "normalize r' = gcd_eucl a b" by (simp add: gcd_eucl_0) - qed - finally show ?thesis . - next - case False - hence "euclid_ext_aux r' r s' s t' t = - euclid_ext_aux r (r' mod r) s (s' - r' div r * s) t (t' - r' div r * t)" - by (subst euclid_ext_aux.simps) (simp add: Let_def) - also from "1.prems" False have "?P \" - proof (intro "1.IH") - have "(s' - r' div r * s) * a + (t' - r' div r * t) * b = - (s' * a + t' * b) - r' div r * (s * a + t * b)" by (simp add: algebra_simps) - also have "s' * a + t' * b = r'" by fact - also have "s * a + t * b = r" by fact - also have "r' - r' div r * r = r' mod r" using div_mult_mod_eq [of r' r] - by (simp add: algebra_simps) - finally show "(s' - r' div r * s) * a + (t' - r' div r * t) * b = r' mod r" . - qed (auto simp: gcd_eucl_non_0 algebra_simps minus_mod_eq_div_mult [symmetric]) - finally show ?thesis . + then show dvd_Lcm: "a \ A \ a dvd Lcm A" + and Lcm_least: "(\a. a \ A \ a dvd b) \ Lcm A dvd b" for A and a b + by auto + show "a \ A \ Gcd A dvd a" for A and a + by (auto simp add: local.Gcd_def intro: Lcm_least) + show "(\a. a \ A \ b dvd a) \ b dvd Gcd A" for A and b + by (auto simp add: local.Gcd_def intro: dvd_Lcm) + show [simp]: "normalize (Lcm A) = Lcm A" for A + by (simp add: local.Lcm_def) + show "normalize (Gcd A) = Gcd A" for A + by (simp add: local.Gcd_def) qed qed -definition euclid_ext where - "euclid_ext a b = euclid_ext_aux a b 1 0 0 1" - -lemma euclid_ext_0: - "euclid_ext a 0 = (1 div unit_factor a, 0, normalize a)" - by (simp add: euclid_ext_def euclid_ext_aux.simps) - -lemma euclid_ext_left_0: - "euclid_ext 0 a = (0, 1 div unit_factor a, normalize a)" - by (simp add: euclid_ext_def euclid_ext_aux.simps) - -lemma euclid_ext_correct': - "case euclid_ext a b of (x,y,c) \ x * a + y * b = c \ c = gcd_eucl a b" - unfolding euclid_ext_def by (rule euclid_ext_aux_correct) simp_all +interpretation semiring_Gcd one zero times gcd lcm Gcd Lcm + divide plus minus normalize unit_factor + by (fact semiring_Gcd) -lemma euclid_ext_gcd_eucl: - "(case euclid_ext a b of (x,y,c) \ c) = gcd_eucl a b" - using euclid_ext_correct'[of a b] by (simp add: case_prod_unfold) - -definition euclid_ext' where - "euclid_ext' a b = (case euclid_ext a b of (x, y, _) \ (x, y))" +subclass factorial_semiring +proof - + show "class.factorial_semiring divide plus minus zero times one + normalize unit_factor" + proof (standard, rule factorial_semiring_altI_aux) -- \