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