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