src/HOL/Computational_Algebra/Euclidean_Algorithm.thy
 changeset 65417 fc41a5650fb1 parent 65398 a14fa655b48c child 65435 378175f44328
```     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Thu Apr 06 21:37:13 2017 +0200
1.3 @@ -0,0 +1,631 @@
1.4 +(*  Title:      HOL/Number_Theory/Euclidean_Algorithm.thy
1.5 +    Author:     Manuel Eberl, TU Muenchen
1.6 +*)
1.7 +
1.8 +section \<open>Abstract euclidean algorithm in euclidean (semi)rings\<close>
1.9 +
1.10 +theory Euclidean_Algorithm
1.11 +  imports Factorial_Ring
1.12 +begin
1.13 +
1.14 +subsection \<open>Generic construction of the (simple) euclidean algorithm\<close>
1.15 +
1.16 +context euclidean_semiring
1.17 +begin
1.18 +
1.19 +context
1.20 +begin
1.21 +
1.22 +qualified function gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.23 +  where "gcd a b = (if b = 0 then normalize a else gcd b (a mod b))"
1.24 +  by pat_completeness simp
1.25 +termination
1.26 +  by (relation "measure (euclidean_size \<circ> snd)") (simp_all add: mod_size_less)
1.27 +
1.28 +declare gcd.simps [simp del]
1.29 +
1.30 +lemma eucl_induct [case_names zero mod]:
1.31 +  assumes H1: "\<And>b. P b 0"
1.32 +  and H2: "\<And>a b. b \<noteq> 0 \<Longrightarrow> P b (a mod b) \<Longrightarrow> P a b"
1.33 +  shows "P a b"
1.34 +proof (induct a b rule: gcd.induct)
1.35 +  case (1 a b)
1.36 +  show ?case
1.37 +  proof (cases "b = 0")
1.38 +    case True then show "P a b" by simp (rule H1)
1.39 +  next
1.40 +    case False
1.41 +    then have "P b (a mod b)"
1.42 +      by (rule "1.hyps")
1.43 +    with \<open>b \<noteq> 0\<close> show "P a b"
1.44 +      by (blast intro: H2)
1.45 +  qed
1.46 +qed
1.47 +
1.48 +qualified lemma gcd_0:
1.49 +  "gcd a 0 = normalize a"
1.50 +  by (simp add: gcd.simps [of a 0])
1.51 +
1.52 +qualified lemma gcd_mod:
1.53 +  "a \<noteq> 0 \<Longrightarrow> gcd a (b mod a) = gcd b a"
1.54 +  by (simp add: gcd.simps [of b 0] gcd.simps [of b a])
1.55 +
1.56 +qualified definition lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.57 +  where "lcm a b = normalize (a * b) div gcd a b"
1.58 +
1.59 +qualified definition Lcm :: "'a set \<Rightarrow> 'a" \<comment>
1.60 +    \<open>Somewhat complicated definition of Lcm that has the advantage of working
1.61 +    for infinite sets as well\<close>
1.62 +  where
1.63 +  [code del]: "Lcm A = (if \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) then
1.64 +     let l = SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l =
1.65 +       (LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n)
1.66 +       in normalize l
1.67 +      else 0)"
1.68 +
1.69 +qualified definition Gcd :: "'a set \<Rightarrow> 'a"
1.70 +  where [code del]: "Gcd A = Lcm {d. \<forall>a\<in>A. d dvd a}"
1.71 +
1.72 +end
1.73 +
1.74 +lemma semiring_gcd:
1.75 +  "class.semiring_gcd one zero times gcd lcm
1.76 +    divide plus minus unit_factor normalize"
1.77 +proof
1.78 +  show "gcd a b dvd a"
1.79 +    and "gcd a b dvd b" for a b
1.80 +    by (induct a b rule: eucl_induct)
1.81 +      (simp_all add: local.gcd_0 local.gcd_mod dvd_mod_iff)
1.82 +next
1.83 +  show "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b" for a b c
1.84 +  proof (induct a b rule: eucl_induct)
1.85 +    case (zero a) from \<open>c dvd a\<close> show ?case
1.86 +      by (rule dvd_trans) (simp add: local.gcd_0)
1.87 +  next
1.88 +    case (mod a b)
1.89 +    then show ?case
1.90 +      by (simp add: local.gcd_mod dvd_mod_iff)
1.91 +  qed
1.92 +next
1.93 +  show "normalize (gcd a b) = gcd a b" for a b
1.94 +    by (induct a b rule: eucl_induct)
1.95 +      (simp_all add: local.gcd_0 local.gcd_mod)
1.96 +next
1.97 +  show "lcm a b = normalize (a * b) div gcd a b" for a b
1.98 +    by (fact local.lcm_def)
1.99 +qed
1.100 +
1.101 +interpretation semiring_gcd one zero times gcd lcm
1.102 +  divide plus minus unit_factor normalize
1.103 +  by (fact semiring_gcd)
1.104 +
1.105 +lemma semiring_Gcd:
1.106 +  "class.semiring_Gcd one zero times gcd lcm Gcd Lcm
1.107 +    divide plus minus unit_factor normalize"
1.108 +proof -
1.109 +  show ?thesis
1.110 +  proof
1.111 +    have "(\<forall>a\<in>A. a dvd Lcm A) \<and> (\<forall>b. (\<forall>a\<in>A. a dvd b) \<longrightarrow> Lcm A dvd b)" for A
1.112 +    proof (cases "\<exists>l. l \<noteq>  0 \<and> (\<forall>a\<in>A. a dvd l)")
1.113 +      case False
1.114 +      then have "Lcm A = 0"
1.115 +        by (auto simp add: local.Lcm_def)
1.116 +      with False show ?thesis
1.117 +        by auto
1.118 +    next
1.119 +      case True
1.120 +      then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \<noteq> 0" "\<forall>a\<in>A. a dvd l\<^sub>0" by blast
1.121 +      define n where "n = (LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n)"
1.122 +      define l where "l = (SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n)"
1.123 +      have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
1.124 +        apply (subst n_def)
1.125 +        apply (rule LeastI [of _ "euclidean_size l\<^sub>0"])
1.126 +        apply (rule exI [of _ l\<^sub>0])
1.127 +        apply (simp add: l\<^sub>0_props)
1.128 +        done
1.129 +      from someI_ex [OF this] have "l \<noteq> 0" and "\<forall>a\<in>A. a dvd l"
1.130 +        and "euclidean_size l = n"
1.131 +        unfolding l_def by simp_all
1.132 +      {
1.133 +        fix l' assume "\<forall>a\<in>A. a dvd l'"
1.134 +        with \<open>\<forall>a\<in>A. a dvd l\<close> have "\<forall>a\<in>A. a dvd gcd l l'"
1.135 +          by (auto intro: gcd_greatest)
1.136 +        moreover from \<open>l \<noteq> 0\<close> have "gcd l l' \<noteq> 0"
1.137 +          by simp
1.138 +        ultimately have "\<exists>b. b \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd b) \<and>
1.139 +          euclidean_size b = euclidean_size (gcd l l')"
1.140 +          by (intro exI [of _ "gcd l l'"], auto)
1.141 +        then have "euclidean_size (gcd l l') \<ge> n"
1.142 +          by (subst n_def) (rule Least_le)
1.143 +        moreover have "euclidean_size (gcd l l') \<le> n"
1.144 +        proof -
1.145 +          have "gcd l l' dvd l"
1.146 +            by simp
1.147 +          then obtain a where "l = gcd l l' * a" ..
1.148 +          with \<open>l \<noteq> 0\<close> have "a \<noteq> 0"
1.149 +            by auto
1.150 +          hence "euclidean_size (gcd l l') \<le> euclidean_size (gcd l l' * a)"
1.151 +            by (rule size_mult_mono)
1.152 +          also have "gcd l l' * a = l" using \<open>l = gcd l l' * a\<close> ..
1.153 +          also note \<open>euclidean_size l = n\<close>
1.154 +          finally show "euclidean_size (gcd l l') \<le> n" .
1.155 +        qed
1.156 +        ultimately have *: "euclidean_size l = euclidean_size (gcd l l')"
1.157 +          by (intro le_antisym, simp_all add: \<open>euclidean_size l = n\<close>)
1.158 +        from \<open>l \<noteq> 0\<close> have "l dvd gcd l l'"
1.159 +          by (rule dvd_euclidean_size_eq_imp_dvd) (auto simp add: *)
1.160 +        hence "l dvd l'" by (rule dvd_trans [OF _ gcd_dvd2])
1.161 +      }
1.162 +      with \<open>\<forall>a\<in>A. a dvd l\<close> and \<open>l \<noteq> 0\<close>
1.163 +        have "(\<forall>a\<in>A. a dvd normalize l) \<and>
1.164 +          (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> normalize l dvd l')"
1.165 +        by auto
1.166 +      also from True have "normalize l = Lcm A"
1.167 +        by (simp add: local.Lcm_def Let_def n_def l_def)
1.168 +      finally show ?thesis .
1.169 +    qed
1.170 +    then show dvd_Lcm: "a \<in> A \<Longrightarrow> a dvd Lcm A"
1.171 +      and Lcm_least: "(\<And>a. a \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> Lcm A dvd b" for A and a b
1.172 +      by auto
1.173 +    show "a \<in> A \<Longrightarrow> Gcd A dvd a" for A and a
1.174 +      by (auto simp add: local.Gcd_def intro: Lcm_least)
1.175 +    show "(\<And>a. a \<in> A \<Longrightarrow> b dvd a) \<Longrightarrow> b dvd Gcd A" for A and b
1.176 +      by (auto simp add: local.Gcd_def intro: dvd_Lcm)
1.177 +    show [simp]: "normalize (Lcm A) = Lcm A" for A
1.178 +      by (simp add: local.Lcm_def)
1.179 +    show "normalize (Gcd A) = Gcd A" for A
1.180 +      by (simp add: local.Gcd_def)
1.181 +  qed
1.182 +qed
1.183 +
1.184 +interpretation semiring_Gcd one zero times gcd lcm Gcd Lcm
1.185 +    divide plus minus unit_factor normalize
1.186 +  by (fact semiring_Gcd)
1.187 +
1.188 +subclass factorial_semiring
1.189 +proof -
1.190 +  show "class.factorial_semiring divide plus minus zero times one
1.191 +     unit_factor normalize"
1.192 +  proof (standard, rule factorial_semiring_altI_aux) \<comment> \<open>FIXME rule\<close>
1.193 +    fix x assume "x \<noteq> 0"
1.194 +    thus "finite {p. p dvd x \<and> normalize p = p}"
1.195 +    proof (induction "euclidean_size x" arbitrary: x rule: less_induct)
1.196 +      case (less x)
1.197 +      show ?case
1.198 +      proof (cases "\<exists>y. y dvd x \<and> \<not>x dvd y \<and> \<not>is_unit y")
1.199 +        case False
1.200 +        have "{p. p dvd x \<and> normalize p = p} \<subseteq> {1, normalize x}"
1.201 +        proof
1.202 +          fix p assume p: "p \<in> {p. p dvd x \<and> normalize p = p}"
1.203 +          with False have "is_unit p \<or> x dvd p" by blast
1.204 +          thus "p \<in> {1, normalize x}"
1.205 +          proof (elim disjE)
1.206 +            assume "is_unit p"
1.207 +            hence "normalize p = 1" by (simp add: is_unit_normalize)
1.208 +            with p show ?thesis by simp
1.209 +          next
1.210 +            assume "x dvd p"
1.211 +            with p have "normalize p = normalize x" by (intro associatedI) simp_all
1.212 +            with p show ?thesis by simp
1.213 +          qed
1.214 +        qed
1.215 +        moreover have "finite \<dots>" by simp
1.216 +        ultimately show ?thesis by (rule finite_subset)
1.217 +      next
1.218 +        case True
1.219 +        then obtain y where y: "y dvd x" "\<not>x dvd y" "\<not>is_unit y" by blast
1.220 +        define z where "z = x div y"
1.221 +        let ?fctrs = "\<lambda>x. {p. p dvd x \<and> normalize p = p}"
1.222 +        from y have x: "x = y * z" by (simp add: z_def)
1.223 +        with less.prems have "y \<noteq> 0" "z \<noteq> 0" by auto
1.224 +        have normalized_factors_product:
1.225 +          "{p. p dvd a * b \<and> normalize p = p} =
1.226 +             (\<lambda>(x,y). x * y) ` ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})" for a b
1.227 +        proof safe
1.228 +          fix p assume p: "p dvd a * b" "normalize p = p"
1.229 +          from dvd_productE[OF p(1)] guess x y . note xy = this
1.230 +          define x' y' where "x' = normalize x" and "y' = normalize y"
1.231 +          have "p = x' * y'"
1.232 +            by (subst p(2) [symmetric]) (simp add: xy x'_def y'_def normalize_mult)
1.233 +          moreover from xy have "normalize x' = x'" "normalize y' = y'" "x' dvd a" "y' dvd b"
1.234 +            by (simp_all add: x'_def y'_def)
1.235 +          ultimately show "p \<in> (\<lambda>(x, y). x * y) `
1.236 +            ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})"
1.237 +            by blast
1.238 +        qed (auto simp: normalize_mult mult_dvd_mono)
1.239 +        from x y have "\<not>is_unit z" by (auto simp: mult_unit_dvd_iff)
1.240 +        have "?fctrs x = (\<lambda>(p,p'). p * p') ` (?fctrs y \<times> ?fctrs z)"
1.241 +          by (subst x) (rule normalized_factors_product)
1.242 +        also have "\<not>y * z dvd y * 1" "\<not>y * z dvd 1 * z"
1.243 +          by (subst dvd_times_left_cancel_iff dvd_times_right_cancel_iff; fact)+
1.244 +        hence "finite ((\<lambda>(p,p'). p * p') ` (?fctrs y \<times> ?fctrs z))"
1.245 +          by (intro finite_imageI finite_cartesian_product less dvd_proper_imp_size_less)
1.246 +             (auto simp: x)
1.247 +        finally show ?thesis .
1.248 +      qed
1.249 +    qed
1.250 +  next
1.251 +    fix p
1.252 +    assume "irreducible p"
1.253 +    then show "prime_elem p"
1.254 +      by (rule irreducible_imp_prime_elem_gcd)
1.255 +  qed
1.256 +qed
1.257 +
1.258 +lemma Gcd_eucl_set [code]:
1.259 +  "Gcd (set xs) = fold gcd xs 0"
1.260 +  by (fact Gcd_set_eq_fold)
1.261 +
1.262 +lemma Lcm_eucl_set [code]:
1.263 +  "Lcm (set xs) = fold lcm xs 1"
1.264 +  by (fact Lcm_set_eq_fold)
1.265 +
1.266 +end
1.267 +
1.268 +hide_const (open) gcd lcm Gcd Lcm
1.269 +
1.270 +lemma prime_elem_int_abs_iff [simp]:
1.271 +  fixes p :: int
1.272 +  shows "prime_elem \<bar>p\<bar> \<longleftrightarrow> prime_elem p"
1.273 +  using prime_elem_normalize_iff [of p] by simp
1.274 +
1.275 +lemma prime_elem_int_minus_iff [simp]:
1.276 +  fixes p :: int
1.277 +  shows "prime_elem (- p) \<longleftrightarrow> prime_elem p"
1.278 +  using prime_elem_normalize_iff [of "- p"] by simp
1.279 +
1.280 +lemma prime_int_iff:
1.281 +  fixes p :: int
1.282 +  shows "prime p \<longleftrightarrow> p > 0 \<and> prime_elem p"
1.283 +  by (auto simp add: prime_def dest: prime_elem_not_zeroI)
1.284 +
1.285 +
1.286 +subsection \<open>The (simple) euclidean algorithm as gcd computation\<close>
1.287 +
1.288 +class euclidean_semiring_gcd = euclidean_semiring + gcd + Gcd +
1.289 +  assumes gcd_eucl: "Euclidean_Algorithm.gcd = GCD.gcd"
1.290 +    and lcm_eucl: "Euclidean_Algorithm.lcm = GCD.lcm"
1.291 +  assumes Gcd_eucl: "Euclidean_Algorithm.Gcd = GCD.Gcd"
1.292 +    and Lcm_eucl: "Euclidean_Algorithm.Lcm = GCD.Lcm"
1.293 +begin
1.294 +
1.295 +subclass semiring_gcd
1.296 +  unfolding gcd_eucl [symmetric] lcm_eucl [symmetric]
1.297 +  by (fact semiring_gcd)
1.298 +
1.299 +subclass semiring_Gcd
1.300 +  unfolding  gcd_eucl [symmetric] lcm_eucl [symmetric]
1.301 +    Gcd_eucl [symmetric] Lcm_eucl [symmetric]
1.302 +  by (fact semiring_Gcd)
1.303 +
1.304 +subclass factorial_semiring_gcd
1.305 +proof
1.306 +  show "gcd a b = gcd_factorial a b" for a b
1.307 +    apply (rule sym)
1.308 +    apply (rule gcdI)
1.309 +       apply (fact gcd_lcm_factorial)+
1.310 +    done
1.311 +  then show "lcm a b = lcm_factorial a b" for a b
1.312 +    by (simp add: lcm_factorial_gcd_factorial lcm_gcd)
1.313 +  show "Gcd A = Gcd_factorial A" for A
1.314 +    apply (rule sym)
1.315 +    apply (rule GcdI)
1.316 +       apply (fact gcd_lcm_factorial)+
1.317 +    done
1.318 +  show "Lcm A = Lcm_factorial A" for A
1.319 +    apply (rule sym)
1.320 +    apply (rule LcmI)
1.321 +       apply (fact gcd_lcm_factorial)+
1.322 +    done
1.323 +qed
1.324 +
1.325 +lemma gcd_mod_right [simp]:
1.326 +  "a \<noteq> 0 \<Longrightarrow> gcd a (b mod a) = gcd a b"
1.327 +  unfolding gcd.commute [of a b]
1.328 +  by (simp add: gcd_eucl [symmetric] local.gcd_mod)
1.329 +
1.330 +lemma gcd_mod_left [simp]:
1.331 +  "b \<noteq> 0 \<Longrightarrow> gcd (a mod b) b = gcd a b"
1.332 +  by (drule gcd_mod_right [of _ a]) (simp add: gcd.commute)
1.333 +
1.334 +lemma euclidean_size_gcd_le1 [simp]:
1.335 +  assumes "a \<noteq> 0"
1.336 +  shows "euclidean_size (gcd a b) \<le> euclidean_size a"
1.337 +proof -
1.338 +  from gcd_dvd1 obtain c where A: "a = gcd a b * c" ..
1.339 +  with assms have "c \<noteq> 0"
1.340 +    by auto
1.341 +  moreover from this
1.342 +  have "euclidean_size (gcd a b) \<le> euclidean_size (gcd a b * c)"
1.343 +    by (rule size_mult_mono)
1.344 +  with A show ?thesis
1.345 +    by simp
1.346 +qed
1.347 +
1.348 +lemma euclidean_size_gcd_le2 [simp]:
1.349 +  "b \<noteq> 0 \<Longrightarrow> euclidean_size (gcd a b) \<le> euclidean_size b"
1.350 +  by (subst gcd.commute, rule euclidean_size_gcd_le1)
1.351 +
1.352 +lemma euclidean_size_gcd_less1:
1.353 +  assumes "a \<noteq> 0" and "\<not> a dvd b"
1.354 +  shows "euclidean_size (gcd a b) < euclidean_size a"
1.355 +proof (rule ccontr)
1.356 +  assume "\<not>euclidean_size (gcd a b) < euclidean_size a"
1.357 +  with \<open>a \<noteq> 0\<close> have A: "euclidean_size (gcd a b) = euclidean_size a"
1.358 +    by (intro le_antisym, simp_all)
1.359 +  have "a dvd gcd a b"
1.360 +    by (rule dvd_euclidean_size_eq_imp_dvd) (simp_all add: assms A)
1.361 +  hence "a dvd b" using dvd_gcdD2 by blast
1.362 +  with \<open>\<not> a dvd b\<close> show False by contradiction
1.363 +qed
1.364 +
1.365 +lemma euclidean_size_gcd_less2:
1.366 +  assumes "b \<noteq> 0" and "\<not> b dvd a"
1.367 +  shows "euclidean_size (gcd a b) < euclidean_size b"
1.368 +  using assms by (subst gcd.commute, rule euclidean_size_gcd_less1)
1.369 +
1.370 +lemma euclidean_size_lcm_le1:
1.371 +  assumes "a \<noteq> 0" and "b \<noteq> 0"
1.372 +  shows "euclidean_size a \<le> euclidean_size (lcm a b)"
1.373 +proof -
1.374 +  have "a dvd lcm a b" by (rule dvd_lcm1)
1.375 +  then obtain c where A: "lcm a b = a * c" ..
1.376 +  with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "c \<noteq> 0" by (auto simp: lcm_eq_0_iff)
1.377 +  then show ?thesis by (subst A, intro size_mult_mono)
1.378 +qed
1.379 +
1.380 +lemma euclidean_size_lcm_le2:
1.381 +  "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> euclidean_size b \<le> euclidean_size (lcm a b)"
1.382 +  using euclidean_size_lcm_le1 [of b a] by (simp add: ac_simps)
1.383 +
1.384 +lemma euclidean_size_lcm_less1:
1.385 +  assumes "b \<noteq> 0" and "\<not> b dvd a"
1.386 +  shows "euclidean_size a < euclidean_size (lcm a b)"
1.387 +proof (rule ccontr)
1.388 +  from assms have "a \<noteq> 0" by auto
1.389 +  assume "\<not>euclidean_size a < euclidean_size (lcm a b)"
1.390 +  with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "euclidean_size (lcm a b) = euclidean_size a"
1.391 +    by (intro le_antisym, simp, intro euclidean_size_lcm_le1)
1.392 +  with assms have "lcm a b dvd a"
1.393 +    by (rule_tac dvd_euclidean_size_eq_imp_dvd) (auto simp: lcm_eq_0_iff)
1.394 +  hence "b dvd a" by (rule lcm_dvdD2)
1.395 +  with \<open>\<not>b dvd a\<close> show False by contradiction
1.396 +qed
1.397 +
1.398 +lemma euclidean_size_lcm_less2:
1.399 +  assumes "a \<noteq> 0" and "\<not> a dvd b"
1.400 +  shows "euclidean_size b < euclidean_size (lcm a b)"
1.401 +  using assms euclidean_size_lcm_less1 [of a b] by (simp add: ac_simps)
1.402 +
1.403 +end
1.404 +
1.405 +lemma factorial_euclidean_semiring_gcdI:
1.406 +  "OFCLASS('a::{factorial_semiring_gcd, euclidean_semiring}, euclidean_semiring_gcd_class)"
1.407 +proof
1.408 +  interpret semiring_Gcd 1 0 times
1.409 +    Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm
1.410 +    Euclidean_Algorithm.Gcd Euclidean_Algorithm.Lcm
1.411 +    divide plus minus unit_factor normalize
1.412 +    rewrites "dvd.dvd op * = Rings.dvd"
1.413 +    by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
1.414 +  show [simp]: "Euclidean_Algorithm.gcd = (gcd :: 'a \<Rightarrow> _)"
1.415 +  proof (rule ext)+
1.416 +    fix a b :: 'a
1.417 +    show "Euclidean_Algorithm.gcd a b = gcd a b"
1.418 +    proof (induct a b rule: eucl_induct)
1.419 +      case zero
1.420 +      then show ?case
1.421 +        by simp
1.422 +    next
1.423 +      case (mod a b)
1.424 +      moreover have "gcd b (a mod b) = gcd b a"
1.425 +        using GCD.gcd_add_mult [of b "a div b" "a mod b", symmetric]
1.426 +          by (simp add: div_mult_mod_eq)
1.427 +      ultimately show ?case
1.428 +        by (simp add: Euclidean_Algorithm.gcd_mod ac_simps)
1.429 +    qed
1.430 +  qed
1.431 +  show [simp]: "Euclidean_Algorithm.Lcm = (Lcm :: 'a set \<Rightarrow> _)"
1.432 +    by (auto intro!: Lcm_eqI GCD.dvd_Lcm GCD.Lcm_least)
1.433 +  show "Euclidean_Algorithm.lcm = (lcm :: 'a \<Rightarrow> _)"
1.434 +    by (simp add: fun_eq_iff Euclidean_Algorithm.lcm_def semiring_gcd_class.lcm_gcd)
1.435 +  show "Euclidean_Algorithm.Gcd = (Gcd :: 'a set \<Rightarrow> _)"
1.436 +    by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm)
1.437 +qed
1.438 +
1.439 +
1.440 +subsection \<open>The extended euclidean algorithm\<close>
1.441 +
1.442 +class euclidean_ring_gcd = euclidean_semiring_gcd + idom
1.443 +begin
1.444 +
1.445 +subclass euclidean_ring ..
1.446 +subclass ring_gcd ..
1.447 +subclass factorial_ring_gcd ..
1.448 +
1.449 +function euclid_ext_aux :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a \<times> 'a) \<times> 'a"
1.450 +  where "euclid_ext_aux s' s t' t r' r = (
1.451 +     if r = 0 then let c = 1 div unit_factor r' in ((s' * c, t' * c), normalize r')
1.452 +     else let q = r' div r
1.453 +          in euclid_ext_aux s (s' - q * s) t (t' - q * t) r (r' mod r))"
1.454 +  by auto
1.455 +termination
1.456 +  by (relation "measure (\<lambda>(_, _, _, _, _, b). euclidean_size b)")
1.457 +    (simp_all add: mod_size_less)
1.458 +
1.459 +abbreviation (input) euclid_ext :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<times> 'a) \<times> 'a"
1.460 +  where "euclid_ext \<equiv> euclid_ext_aux 1 0 0 1"
1.461 +
1.462 +lemma
1.463 +  assumes "gcd r' r = gcd a b"
1.464 +  assumes "s' * a + t' * b = r'"
1.465 +  assumes "s * a + t * b = r"
1.466 +  assumes "euclid_ext_aux s' s t' t r' r = ((x, y), c)"
1.467 +  shows euclid_ext_aux_eq_gcd: "c = gcd a b"
1.468 +    and euclid_ext_aux_bezout: "x * a + y * b = gcd a b"
1.469 +proof -
1.470 +  have "case euclid_ext_aux s' s t' t r' r of ((x, y), c) \<Rightarrow>
1.471 +    x * a + y * b = c \<and> c = gcd a b" (is "?P (euclid_ext_aux s' s t' t r' r)")
1.472 +    using assms(1-3)
1.473 +  proof (induction s' s t' t r' r rule: euclid_ext_aux.induct)
1.474 +    case (1 s' s t' t r' r)
1.475 +    show ?case
1.476 +    proof (cases "r = 0")
1.477 +      case True
1.478 +      hence "euclid_ext_aux s' s t' t r' r =
1.479 +               ((s' div unit_factor r', t' div unit_factor r'), normalize r')"
1.480 +        by (subst euclid_ext_aux.simps) (simp add: Let_def)
1.481 +      also have "?P \<dots>"
1.482 +      proof safe
1.483 +        have "s' div unit_factor r' * a + t' div unit_factor r' * b =
1.484 +                (s' * a + t' * b) div unit_factor r'"
1.485 +          by (cases "r' = 0") (simp_all add: unit_div_commute)
1.486 +        also have "s' * a + t' * b = r'" by fact
1.487 +        also have "\<dots> div unit_factor r' = normalize r'" by simp
1.488 +        finally show "s' div unit_factor r' * a + t' div unit_factor r' * b = normalize r'" .
1.489 +      next
1.490 +        from "1.prems" True show "normalize r' = gcd a b"
1.491 +          by simp
1.492 +      qed
1.493 +      finally show ?thesis .
1.494 +    next
1.495 +      case False
1.496 +      hence "euclid_ext_aux s' s t' t r' r =
1.497 +             euclid_ext_aux s (s' - r' div r * s) t (t' - r' div r * t) r (r' mod r)"
1.498 +        by (subst euclid_ext_aux.simps) (simp add: Let_def)
1.499 +      also from "1.prems" False have "?P \<dots>"
1.500 +      proof (intro "1.IH")
1.501 +        have "(s' - r' div r * s) * a + (t' - r' div r * t) * b =
1.502 +              (s' * a + t' * b) - r' div r * (s * a + t * b)" by (simp add: algebra_simps)
1.503 +        also have "s' * a + t' * b = r'" by fact
1.504 +        also have "s * a + t * b = r" by fact
1.505 +        also have "r' - r' div r * r = r' mod r" using div_mult_mod_eq [of r' r]
1.506 +          by (simp add: algebra_simps)
1.507 +        finally show "(s' - r' div r * s) * a + (t' - r' div r * t) * b = r' mod r" .
1.508 +      qed (auto simp: gcd_mod_right algebra_simps minus_mod_eq_div_mult [symmetric] gcd.commute)
1.509 +      finally show ?thesis .
1.510 +    qed
1.511 +  qed
1.512 +  with assms(4) show "c = gcd a b" "x * a + y * b = gcd a b"
1.513 +    by simp_all
1.514 +qed
1.515 +
1.516 +declare euclid_ext_aux.simps [simp del]
1.517 +
1.518 +definition bezout_coefficients :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a"
1.519 +  where [code]: "bezout_coefficients a b = fst (euclid_ext a b)"
1.520 +
1.521 +lemma bezout_coefficients_0:
1.522 +  "bezout_coefficients a 0 = (1 div unit_factor a, 0)"
1.523 +  by (simp add: bezout_coefficients_def euclid_ext_aux.simps)
1.524 +
1.525 +lemma bezout_coefficients_left_0:
1.526 +  "bezout_coefficients 0 a = (0, 1 div unit_factor a)"
1.527 +  by (simp add: bezout_coefficients_def euclid_ext_aux.simps)
1.528 +
1.529 +lemma bezout_coefficients:
1.530 +  assumes "bezout_coefficients a b = (x, y)"
1.531 +  shows "x * a + y * b = gcd a b"
1.532 +  using assms by (simp add: bezout_coefficients_def
1.533 +    euclid_ext_aux_bezout [of a b a b 1 0 0 1 x y] prod_eq_iff)
1.534 +
1.535 +lemma bezout_coefficients_fst_snd:
1.536 +  "fst (bezout_coefficients a b) * a + snd (bezout_coefficients a b) * b = gcd a b"
1.537 +  by (rule bezout_coefficients) simp
1.538 +
1.539 +lemma euclid_ext_eq [simp]:
1.540 +  "euclid_ext a b = (bezout_coefficients a b, gcd a b)" (is "?p = ?q")
1.541 +proof
1.542 +  show "fst ?p = fst ?q"
1.543 +    by (simp add: bezout_coefficients_def)
1.544 +  have "snd (euclid_ext_aux 1 0 0 1 a b) = gcd a b"
1.545 +    by (rule euclid_ext_aux_eq_gcd [of a b a b 1 0 0 1])
1.546 +      (simp_all add: prod_eq_iff)
1.547 +  then show "snd ?p = snd ?q"
1.548 +    by simp
1.549 +qed
1.550 +
1.551 +declare euclid_ext_eq [symmetric, code_unfold]
1.552 +
1.553 +end
1.554 +
1.555 +
1.556 +subsection \<open>Typical instances\<close>
1.557 +
1.558 +instance nat :: euclidean_semiring_gcd
1.559 +proof
1.560 +  interpret semiring_Gcd 1 0 times
1.561 +    "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
1.562 +    "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
1.563 +    divide plus minus unit_factor normalize
1.564 +    rewrites "dvd.dvd op * = Rings.dvd"
1.565 +    by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
1.566 +  show [simp]: "(Euclidean_Algorithm.gcd :: nat \<Rightarrow> _) = gcd"
1.567 +  proof (rule ext)+
1.568 +    fix m n :: nat
1.569 +    show "Euclidean_Algorithm.gcd m n = gcd m n"
1.570 +    proof (induct m n rule: eucl_induct)
1.571 +      case zero
1.572 +      then show ?case
1.573 +        by simp
1.574 +    next
1.575 +      case (mod m n)
1.576 +      then have "gcd n (m mod n) = gcd n m"
1.577 +        using gcd_nat.simps [of m n] by (simp add: ac_simps)
1.578 +      with mod show ?case
1.579 +        by (simp add: Euclidean_Algorithm.gcd_mod ac_simps)
1.580 +    qed
1.581 +  qed
1.582 +  show [simp]: "(Euclidean_Algorithm.Lcm :: nat set \<Rightarrow> _) = Lcm"
1.583 +    by (auto intro!: ext Lcm_eqI)
1.584 +  show "(Euclidean_Algorithm.lcm :: nat \<Rightarrow> _) = lcm"
1.585 +    by (simp add: fun_eq_iff Euclidean_Algorithm.lcm_def semiring_gcd_class.lcm_gcd)
1.586 +  show "(Euclidean_Algorithm.Gcd :: nat set \<Rightarrow> _) = Gcd"
1.587 +    by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm)
1.588 +qed
1.589 +
1.590 +instance int :: euclidean_ring_gcd
1.591 +proof
1.592 +  interpret semiring_Gcd 1 0 times
1.593 +    "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
1.594 +    "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
1.595 +    divide plus minus unit_factor normalize
1.596 +    rewrites "dvd.dvd op * = Rings.dvd"
1.597 +    by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
1.598 +  show [simp]: "(Euclidean_Algorithm.gcd :: int \<Rightarrow> _) = gcd"
1.599 +  proof (rule ext)+
1.600 +    fix k l :: int
1.601 +    show "Euclidean_Algorithm.gcd k l = gcd k l"
1.602 +    proof (induct k l rule: eucl_induct)
1.603 +      case zero
1.604 +      then show ?case
1.605 +        by simp
1.606 +    next
1.607 +      case (mod k l)
1.608 +      have "gcd l (k mod l) = gcd l k"
1.609 +      proof (cases l "0::int" rule: linorder_cases)
1.610 +        case less
1.611 +        then show ?thesis
1.612 +          using gcd_non_0_int [of "- l" "- k"] by (simp add: ac_simps)
1.613 +      next
1.614 +        case equal
1.615 +        with mod show ?thesis
1.616 +          by simp
1.617 +      next
1.618 +        case greater
1.619 +        then show ?thesis
1.620 +          using gcd_non_0_int [of l k] by (simp add: ac_simps)
1.621 +      qed
1.622 +      with mod show ?case
1.623 +        by (simp add: Euclidean_Algorithm.gcd_mod ac_simps)
1.624 +    qed
1.625 +  qed
1.626 +  show [simp]: "(Euclidean_Algorithm.Lcm :: int set \<Rightarrow> _) = Lcm"
1.627 +    by (auto intro!: ext Lcm_eqI)
1.628 +  show "(Euclidean_Algorithm.lcm :: int \<Rightarrow> _) = lcm"
1.629 +    by (simp add: fun_eq_iff Euclidean_Algorithm.lcm_def semiring_gcd_class.lcm_gcd)
1.630 +  show "(Euclidean_Algorithm.Gcd :: int set \<Rightarrow> _) = Gcd"
1.631 +    by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm)
1.632 +qed
1.633 +
1.634 +end
```