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