reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
authorhaftmann
Wed Jan 04 21:28:29 2017 +0100 (2017-01-04)
changeset 64786340db65fd2c1
parent 64785 ae0bbc8e45ad
child 64787 067cacdd1117
reworked to provide auxiliary operations Euclidean_Algorithm.* to instantiate gcd etc. for euclidean rings
NEWS
src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
src/HOL/Library/Field_as_Ring.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Library/Polynomial_Factorial.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
     1.1 --- a/NEWS	Wed Jan 04 21:28:29 2017 +0100
     1.2 +++ b/NEWS	Wed Jan 04 21:28:29 2017 +0100
     1.3 @@ -28,6 +28,15 @@
     1.4  unique_euclidean_(semi)ring; instantiation requires
     1.5  provision of a euclidean size.
     1.6  
     1.7 +* Reworking of theory Euclidean_Algorithm in session HOL-Number_Theory:
     1.8 +  - Euclidean induction is available as rule eucl_induct;
     1.9 +  - Constants Euclidean_Algorithm.gcd, Euclidean_Algorithm.lcm,
    1.10 +    Euclidean_Algorithm.Gcd and Euclidean_Algorithm.Lcm allow
    1.11 +    easy instantiation of euclidean (semi)rings as GCD (semi)rings.
    1.12 +  - Coefficients obtained by extended euclidean algorithm are
    1.13 +    available as "bezout_coefficients".
    1.14 +INCOMPATIBILITY.
    1.15 +
    1.16  * Swapped orientation of congruence rules mod_add_left_eq,
    1.17  mod_add_right_eq, mod_add_eq, mod_mult_left_eq, mod_mult_right_eq,
    1.18  mod_mult_eq, mod_minus_eq, mod_diff_left_eq, mod_diff_right_eq,
     2.1 --- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Wed Jan 04 21:28:29 2017 +0100
     2.2 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Wed Jan 04 21:28:29 2017 +0100
     2.3 @@ -20,64 +20,31 @@
     2.4  in fold Code.del_eqns consts thy end
     2.5  \<close> \<comment> \<open>drop technical stuff from \<open>Quickcheck_Narrowing\<close> which is tailored towards Haskell\<close>
     2.6  
     2.7 -(* 
     2.8 -   The following code equations have to be deleted because they use 
     2.9 -   lists to implement sets in the code generetor. 
    2.10 -*)
    2.11 -
    2.12 -lemma [code, code del]:
    2.13 -  "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" ..
    2.14 -
    2.15 -lemma [code, code del]:
    2.16 -  "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" ..
    2.17 -
    2.18 -lemma [code, code del]:
    2.19 -  "pred_of_set = pred_of_set" ..
    2.20 -
    2.21 -lemma [code, code del]:
    2.22 -  "Wellfounded.acc = Wellfounded.acc" ..
    2.23 -
    2.24 -lemma [code, code del]:
    2.25 -  "Cardinality.card' = Cardinality.card'" ..
    2.26 -
    2.27 -lemma [code, code del]:
    2.28 -  "Cardinality.finite' = Cardinality.finite'" ..
    2.29 -
    2.30 -lemma [code, code del]:
    2.31 -  "Cardinality.subset' = Cardinality.subset'" ..
    2.32 -
    2.33 -lemma [code, code del]:
    2.34 -  "Cardinality.eq_set = Cardinality.eq_set" ..
    2.35 +text \<open>
    2.36 +  The following code equations have to be deleted because they use 
    2.37 +  lists to implement sets in the code generetor. 
    2.38 +\<close>
    2.39  
    2.40 -lemma [code, code del]:
    2.41 -  "(Gcd :: nat set \<Rightarrow> nat) = Gcd" ..
    2.42 -
    2.43 -lemma [code, code del]:
    2.44 -  "(Lcm :: nat set \<Rightarrow> nat) = Lcm" ..
    2.45 -
    2.46 -lemma [code, code del]:
    2.47 -  "(Gcd :: int set \<Rightarrow> int) = Gcd" ..
    2.48 -
    2.49 -lemma [code, code del]:
    2.50 -  "(Lcm :: int set \<Rightarrow> int) = Lcm" ..
    2.51 -
    2.52 -lemma [code, code del]:
    2.53 -  "(Gcd :: _ poly set \<Rightarrow> _) = Gcd" ..
    2.54 -
    2.55 -lemma [code, code del]:
    2.56 -  "(Lcm :: _ poly set \<Rightarrow> _) = Lcm" ..
    2.57 -
    2.58 -lemma [code, code del]:
    2.59 -  "Gcd_eucl = Gcd_eucl" ..
    2.60 -
    2.61 -lemma [code, code del]:
    2.62 -  "Lcm_eucl = Lcm_eucl" ..
    2.63 -
    2.64 -lemma [code, code del]:
    2.65 -  "permutations_of_set = permutations_of_set" ..
    2.66 -
    2.67 -lemma [code, code del]:
    2.68 -  "permutations_of_multiset = permutations_of_multiset" ..
    2.69 +declare [[code drop:
    2.70 +  Sup_pred_inst.Sup_pred
    2.71 +  Inf_pred_inst.Inf_pred
    2.72 +  pred_of_set
    2.73 +  Wellfounded.acc
    2.74 +  Cardinality.card'
    2.75 +  Cardinality.finite'
    2.76 +  Cardinality.subset'
    2.77 +  Cardinality.eq_set
    2.78 +  "Gcd :: nat set \<Rightarrow> nat"
    2.79 +  "Lcm :: nat set \<Rightarrow> nat"
    2.80 +  "Gcd :: int set \<Rightarrow> int"
    2.81 +  "Lcm :: int set \<Rightarrow> int"
    2.82 +  "Gcd :: _ poly set \<Rightarrow> _"
    2.83 +  "Lcm :: _ poly set \<Rightarrow> _"
    2.84 +  Euclidean_Algorithm.Gcd
    2.85 +  Euclidean_Algorithm.Lcm
    2.86 +  permutations_of_set
    2.87 +  permutations_of_multiset
    2.88 +]]
    2.89  
    2.90  (*
    2.91    If the code generation ends with an exception with the following message:
     3.1 --- a/src/HOL/Library/Field_as_Ring.thy	Wed Jan 04 21:28:29 2017 +0100
     3.2 +++ b/src/HOL/Library/Field_as_Ring.thy	Wed Jan 04 21:28:29 2017 +0100
     3.3 @@ -43,13 +43,13 @@
     3.4  begin
     3.5  
     3.6  definition gcd_real :: "real \<Rightarrow> real \<Rightarrow> real" where
     3.7 -  "gcd_real = gcd_eucl"
     3.8 +  "gcd_real = Euclidean_Algorithm.gcd"
     3.9  definition lcm_real :: "real \<Rightarrow> real \<Rightarrow> real" where
    3.10 -  "lcm_real = lcm_eucl"
    3.11 +  "lcm_real = Euclidean_Algorithm.lcm"
    3.12  definition Gcd_real :: "real set \<Rightarrow> real" where
    3.13 - "Gcd_real = Gcd_eucl"
    3.14 + "Gcd_real = Euclidean_Algorithm.Gcd"
    3.15  definition Lcm_real :: "real set \<Rightarrow> real" where
    3.16 - "Lcm_real = Lcm_eucl"
    3.17 + "Lcm_real = Euclidean_Algorithm.Lcm"
    3.18  
    3.19  instance by standard (simp_all add: gcd_real_def lcm_real_def Gcd_real_def Lcm_real_def)
    3.20  
    3.21 @@ -74,13 +74,13 @@
    3.22  begin
    3.23  
    3.24  definition gcd_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
    3.25 -  "gcd_rat = gcd_eucl"
    3.26 +  "gcd_rat = Euclidean_Algorithm.gcd"
    3.27  definition lcm_rat :: "rat \<Rightarrow> rat \<Rightarrow> rat" where
    3.28 -  "lcm_rat = lcm_eucl"
    3.29 +  "lcm_rat = Euclidean_Algorithm.lcm"
    3.30  definition Gcd_rat :: "rat set \<Rightarrow> rat" where
    3.31 - "Gcd_rat = Gcd_eucl"
    3.32 + "Gcd_rat = Euclidean_Algorithm.Gcd"
    3.33  definition Lcm_rat :: "rat set \<Rightarrow> rat" where
    3.34 - "Lcm_rat = Lcm_eucl"
    3.35 + "Lcm_rat = Euclidean_Algorithm.Lcm"
    3.36  
    3.37  instance by standard (simp_all add: gcd_rat_def lcm_rat_def Gcd_rat_def Lcm_rat_def)
    3.38  
    3.39 @@ -105,13 +105,13 @@
    3.40  begin
    3.41  
    3.42  definition gcd_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
    3.43 -  "gcd_complex = gcd_eucl"
    3.44 +  "gcd_complex = Euclidean_Algorithm.gcd"
    3.45  definition lcm_complex :: "complex \<Rightarrow> complex \<Rightarrow> complex" where
    3.46 -  "lcm_complex = lcm_eucl"
    3.47 +  "lcm_complex = Euclidean_Algorithm.lcm"
    3.48  definition Gcd_complex :: "complex set \<Rightarrow> complex" where
    3.49 - "Gcd_complex = Gcd_eucl"
    3.50 + "Gcd_complex = Euclidean_Algorithm.Gcd"
    3.51  definition Lcm_complex :: "complex set \<Rightarrow> complex" where
    3.52 - "Lcm_complex = Lcm_eucl"
    3.53 + "Lcm_complex = Euclidean_Algorithm.Lcm"
    3.54  
    3.55  instance by standard (simp_all add: gcd_complex_def lcm_complex_def Gcd_complex_def Lcm_complex_def)
    3.56  
     4.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Wed Jan 04 21:28:29 2017 +0100
     4.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Jan 04 21:28:29 2017 +0100
     4.3 @@ -1421,10 +1421,10 @@
     4.4  
     4.5  instantiation fps :: (field) euclidean_ring_gcd
     4.6  begin
     4.7 -definition fps_gcd_def: "(gcd :: 'a fps \<Rightarrow> _) = gcd_eucl"
     4.8 -definition fps_lcm_def: "(lcm :: 'a fps \<Rightarrow> _) = lcm_eucl"
     4.9 -definition fps_Gcd_def: "(Gcd :: 'a fps set \<Rightarrow> _) = Gcd_eucl"
    4.10 -definition fps_Lcm_def: "(Lcm :: 'a fps set \<Rightarrow> _) = Lcm_eucl"
    4.11 +definition fps_gcd_def: "(gcd :: 'a fps \<Rightarrow> _) = Euclidean_Algorithm.gcd"
    4.12 +definition fps_lcm_def: "(lcm :: 'a fps \<Rightarrow> _) = Euclidean_Algorithm.lcm"
    4.13 +definition fps_Gcd_def: "(Gcd :: 'a fps set \<Rightarrow> _) = Euclidean_Algorithm.Gcd"
    4.14 +definition fps_Lcm_def: "(Lcm :: 'a fps set \<Rightarrow> _) = Euclidean_Algorithm.Lcm"
    4.15  instance by standard (simp_all add: fps_gcd_def fps_lcm_def fps_Gcd_def fps_Lcm_def)
    4.16  end
    4.17  
     5.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Wed Jan 04 21:28:29 2017 +0100
     5.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Wed Jan 04 21:28:29 2017 +0100
     5.3 @@ -1040,7 +1040,8 @@
     5.4  end
     5.5  
     5.6  instance poly :: ("{field,factorial_ring_gcd}") euclidean_ring_gcd
     5.7 -  by standard (simp_all add: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def eucl_eq_factorial)
     5.8 +  by (rule euclidean_ring_gcd_class.intro, rule factorial_euclidean_semiring_gcdI)
     5.9 +    standard
    5.10  
    5.11    
    5.12  subsection \<open>Polynomial GCD\<close>
     6.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jan 04 21:28:29 2017 +0100
     6.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jan 04 21:28:29 2017 +0100
     6.3 @@ -9,24 +9,28 @@
     6.4      "~~/src/HOL/Number_Theory/Factorial_Ring"
     6.5  begin
     6.6  
     6.7 +subsection \<open>Generic construction of the (simple) euclidean algorithm\<close>
     6.8 +  
     6.9  context euclidean_semiring
    6.10  begin
    6.11  
    6.12 -function gcd_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    6.13 -where
    6.14 -  "gcd_eucl a b = (if b = 0 then normalize a else gcd_eucl b (a mod b))"
    6.15 +context
    6.16 +begin
    6.17 +
    6.18 +qualified function gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    6.19 +  where "gcd a b = (if b = 0 then normalize a else gcd b (a mod b))"
    6.20    by pat_completeness simp
    6.21  termination
    6.22    by (relation "measure (euclidean_size \<circ> snd)") (simp_all add: mod_size_less)
    6.23  
    6.24 -declare gcd_eucl.simps [simp del]
    6.25 +declare gcd.simps [simp del]
    6.26  
    6.27 -lemma gcd_eucl_induct [case_names zero mod]:
    6.28 +lemma eucl_induct [case_names zero mod]:
    6.29    assumes H1: "\<And>b. P b 0"
    6.30    and H2: "\<And>a b. b \<noteq> 0 \<Longrightarrow> P b (a mod b) \<Longrightarrow> P a b"
    6.31    shows "P a b"
    6.32 -proof (induct a b rule: gcd_eucl.induct)
    6.33 -  case ("1" a b)
    6.34 +proof (induct a b rule: gcd.induct)
    6.35 +  case (1 a b)
    6.36    show ?case
    6.37    proof (cases "b = 0")
    6.38      case True then show "P a b" by simp (rule H1)
    6.39 @@ -38,425 +42,305 @@
    6.40        by (blast intro: H2)
    6.41    qed
    6.42  qed
    6.43 -
    6.44 -definition lcm_eucl :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    6.45 -where
    6.46 -  "lcm_eucl a b = normalize (a * b) div gcd_eucl a b"
    6.47 +  
    6.48 +qualified lemma gcd_0:
    6.49 +  "gcd a 0 = normalize a"
    6.50 +  by (simp add: gcd.simps [of a 0])
    6.51 +  
    6.52 +qualified lemma gcd_mod:
    6.53 +  "a \<noteq> 0 \<Longrightarrow> gcd a (b mod a) = gcd b a"
    6.54 +  by (simp add: gcd.simps [of b 0] gcd.simps [of b a])
    6.55  
    6.56 -definition Lcm_eucl :: "'a set \<Rightarrow> 'a" \<comment> \<open>
    6.57 -  Somewhat complicated definition of Lcm that has the advantage of working
    6.58 -  for infinite sets as well\<close>
    6.59 -where
    6.60 -  "Lcm_eucl A = (if \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) then
    6.61 +qualified definition lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    6.62 +  where "lcm a b = normalize (a * b) div gcd a b"
    6.63 +
    6.64 +qualified definition Lcm :: "'a set \<Rightarrow> 'a" \<comment>
    6.65 +    \<open>Somewhat complicated definition of Lcm that has the advantage of working
    6.66 +    for infinite sets as well\<close>
    6.67 +  where
    6.68 +  [code del]: "Lcm A = (if \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) then
    6.69       let l = SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l =
    6.70         (LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n)
    6.71         in normalize l 
    6.72        else 0)"
    6.73  
    6.74 -definition Gcd_eucl :: "'a set \<Rightarrow> 'a"
    6.75 -where
    6.76 -  "Gcd_eucl A = Lcm_eucl {d. \<forall>a\<in>A. d dvd a}"
    6.77 -
    6.78 -declare Lcm_eucl_def Gcd_eucl_def [code del]
    6.79 +qualified definition Gcd :: "'a set \<Rightarrow> 'a"
    6.80 +  where [code del]: "Gcd A = Lcm {d. \<forall>a\<in>A. d dvd a}"
    6.81  
    6.82 -lemma gcd_eucl_0:
    6.83 -  "gcd_eucl a 0 = normalize a"
    6.84 -  by (simp add: gcd_eucl.simps [of a 0])
    6.85 -
    6.86 -lemma gcd_eucl_0_left:
    6.87 -  "gcd_eucl 0 a = normalize a"
    6.88 -  by (simp_all add: gcd_eucl_0 gcd_eucl.simps [of 0 a])
    6.89 +end    
    6.90  
    6.91 -lemma gcd_eucl_non_0:
    6.92 -  "b \<noteq> 0 \<Longrightarrow> gcd_eucl a b = gcd_eucl b (a mod b)"
    6.93 -  by (simp add: gcd_eucl.simps [of a b] gcd_eucl.simps [of b 0])
    6.94 -
    6.95 -lemma gcd_eucl_dvd1 [iff]: "gcd_eucl a b dvd a"
    6.96 -  and gcd_eucl_dvd2 [iff]: "gcd_eucl a b dvd b"
    6.97 -  by (induct a b rule: gcd_eucl_induct)
    6.98 -     (simp_all add: gcd_eucl_0 gcd_eucl_non_0 dvd_mod_iff)
    6.99 -
   6.100 -lemma normalize_gcd_eucl [simp]:
   6.101 -  "normalize (gcd_eucl a b) = gcd_eucl a b"
   6.102 -  by (induct a b rule: gcd_eucl_induct) (simp_all add: gcd_eucl_0 gcd_eucl_non_0)
   6.103 -     
   6.104 -lemma gcd_eucl_greatest:
   6.105 -  fixes k a b :: 'a
   6.106 -  shows "k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd gcd_eucl a b"
   6.107 -proof (induct a b rule: gcd_eucl_induct)
   6.108 -  case (zero a) from zero(1) show ?case by (rule dvd_trans) (simp add: gcd_eucl_0)
   6.109 +lemma semiring_gcd:
   6.110 +  "class.semiring_gcd one zero times gcd lcm
   6.111 +    divide plus minus normalize unit_factor"
   6.112 +proof
   6.113 +  show "gcd a b dvd a"
   6.114 +    and "gcd a b dvd b" for a b
   6.115 +    by (induct a b rule: eucl_induct)
   6.116 +      (simp_all add: local.gcd_0 local.gcd_mod dvd_mod_iff)
   6.117  next
   6.118 -  case (mod a b)
   6.119 -  then show ?case
   6.120 -    by (simp add: gcd_eucl_non_0 dvd_mod_iff)
   6.121 -qed
   6.122 -
   6.123 -lemma gcd_euclI:
   6.124 -  fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   6.125 -  assumes "d dvd a" "d dvd b" "normalize d = d"
   6.126 -          "\<And>k. k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd d"
   6.127 -  shows   "gcd_eucl a b = d"
   6.128 -  by (rule associated_eqI) (simp_all add: gcd_eucl_greatest assms)
   6.129 -
   6.130 -lemma eq_gcd_euclI:
   6.131 -  fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   6.132 -  assumes "\<And>a b. gcd a b dvd a" "\<And>a b. gcd a b dvd b" "\<And>a b. normalize (gcd a b) = gcd a b"
   6.133 -          "\<And>a b k. k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd gcd a b"
   6.134 -  shows   "gcd = gcd_eucl"
   6.135 -  by (intro ext, rule associated_eqI) (simp_all add: gcd_eucl_greatest assms)
   6.136 -
   6.137 -lemma gcd_eucl_zero [simp]:
   6.138 -  "gcd_eucl a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
   6.139 -  by (metis dvd_0_left dvd_refl gcd_eucl_dvd1 gcd_eucl_dvd2 gcd_eucl_greatest)+
   6.140 -
   6.141 -  
   6.142 -lemma dvd_Lcm_eucl [simp]: "a \<in> A \<Longrightarrow> a dvd Lcm_eucl A"
   6.143 -  and Lcm_eucl_least: "(\<And>a. a \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> Lcm_eucl A dvd b"
   6.144 -  and unit_factor_Lcm_eucl [simp]: 
   6.145 -          "unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)"
   6.146 -proof -
   6.147 -  have "(\<forall>a\<in>A. a dvd Lcm_eucl A) \<and> (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> Lcm_eucl A dvd l') \<and>
   6.148 -    unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)" (is ?thesis)
   6.149 -  proof (cases "\<exists>l. l \<noteq>  0 \<and> (\<forall>a\<in>A. a dvd l)")
   6.150 -    case False
   6.151 -    hence "Lcm_eucl A = 0" by (auto simp: Lcm_eucl_def)
   6.152 -    with False show ?thesis by auto
   6.153 +  show "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b" for a b c
   6.154 +  proof (induct a b rule: eucl_induct)
   6.155 +    case (zero a) from \<open>c dvd a\<close> show ?case
   6.156 +      by (rule dvd_trans) (simp add: local.gcd_0)
   6.157    next
   6.158 -    case True
   6.159 -    then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l\<^sub>0)" by blast
   6.160 -    define n where "n = (LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n)"
   6.161 -    define l where "l = (SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n)"
   6.162 -    have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
   6.163 -      apply (subst n_def)
   6.164 -      apply (rule LeastI[of _ "euclidean_size l\<^sub>0"])
   6.165 -      apply (rule exI[of _ l\<^sub>0])
   6.166 -      apply (simp add: l\<^sub>0_props)
   6.167 -      done
   6.168 -    from someI_ex[OF this] have "l \<noteq> 0" and "\<forall>a\<in>A. a dvd l" and "euclidean_size l = n" 
   6.169 -      unfolding l_def by simp_all
   6.170 -    {
   6.171 -      fix l' assume "\<forall>a\<in>A. a dvd l'"
   6.172 -      with \<open>\<forall>a\<in>A. a dvd l\<close> have "\<forall>a\<in>A. a dvd gcd_eucl l l'" by (auto intro: gcd_eucl_greatest)
   6.173 -      moreover from \<open>l \<noteq> 0\<close> have "gcd_eucl l l' \<noteq> 0" by simp
   6.174 -      ultimately have "\<exists>b. b \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd b) \<and> 
   6.175 -                          euclidean_size b = euclidean_size (gcd_eucl l l')"
   6.176 -        by (intro exI[of _ "gcd_eucl l l'"], auto)
   6.177 -      hence "euclidean_size (gcd_eucl l l') \<ge> n" by (subst n_def) (rule Least_le)
   6.178 -      moreover have "euclidean_size (gcd_eucl l l') \<le> n"
   6.179 -      proof -
   6.180 -        have "gcd_eucl l l' dvd l" by simp
   6.181 -        then obtain a where "l = gcd_eucl l l' * a" unfolding dvd_def by blast
   6.182 -        with \<open>l \<noteq> 0\<close> have "a \<noteq> 0" by auto
   6.183 -        hence "euclidean_size (gcd_eucl l l') \<le> euclidean_size (gcd_eucl l l' * a)"
   6.184 -          by (rule size_mult_mono)
   6.185 -        also have "gcd_eucl l l' * a = l" using \<open>l = gcd_eucl l l' * a\<close> ..
   6.186 -        also note \<open>euclidean_size l = n\<close>
   6.187 -        finally show "euclidean_size (gcd_eucl l l') \<le> n" .
   6.188 -      qed
   6.189 -      ultimately have *: "euclidean_size l = euclidean_size (gcd_eucl l l')" 
   6.190 -        by (intro le_antisym, simp_all add: \<open>euclidean_size l = n\<close>)
   6.191 -      from \<open>l \<noteq> 0\<close> have "l dvd gcd_eucl l l'"
   6.192 -        by (rule dvd_euclidean_size_eq_imp_dvd) (auto simp add: *)
   6.193 -      hence "l dvd l'" by (rule dvd_trans[OF _ gcd_eucl_dvd2])
   6.194 -    }
   6.195 -
   6.196 -    with \<open>(\<forall>a\<in>A. a dvd l)\<close> and unit_factor_is_unit[OF \<open>l \<noteq> 0\<close>] and \<open>l \<noteq> 0\<close>
   6.197 -      have "(\<forall>a\<in>A. a dvd normalize l) \<and> 
   6.198 -        (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> normalize l dvd l') \<and>
   6.199 -        unit_factor (normalize l) = 
   6.200 -        (if normalize l = 0 then 0 else 1)"
   6.201 -      by (auto simp: unit_simps)
   6.202 -    also from True have "normalize l = Lcm_eucl A"
   6.203 -      by (simp add: Lcm_eucl_def Let_def n_def l_def)
   6.204 -    finally show ?thesis .
   6.205 +    case (mod a b)
   6.206 +    then show ?case
   6.207 +      by (simp add: local.gcd_mod dvd_mod_iff)
   6.208    qed
   6.209 -  note A = this
   6.210 -
   6.211 -  {fix a assume "a \<in> A" then show "a dvd Lcm_eucl A" using A by blast}
   6.212 -  {fix b assume "\<And>a. a \<in> A \<Longrightarrow> a dvd b" then show "Lcm_eucl A dvd b" using A by blast}
   6.213 -  from A show "unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)" by blast
   6.214 -qed
   6.215 -
   6.216 -lemma normalize_Lcm_eucl [simp]:
   6.217 -  "normalize (Lcm_eucl A) = Lcm_eucl A"
   6.218 -proof (cases "Lcm_eucl A = 0")
   6.219 -  case True then show ?thesis by simp
   6.220  next
   6.221 -  case False
   6.222 -  have "unit_factor (Lcm_eucl A) * normalize (Lcm_eucl A) = Lcm_eucl A"
   6.223 -    by (fact unit_factor_mult_normalize)
   6.224 -  with False show ?thesis by simp
   6.225 -qed
   6.226 -
   6.227 -lemma eq_Lcm_euclI:
   6.228 -  fixes lcm :: "'a set \<Rightarrow> 'a"
   6.229 -  assumes "\<And>A a. a \<in> A \<Longrightarrow> a dvd lcm A" and "\<And>A c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> lcm A dvd c"
   6.230 -          "\<And>A. normalize (lcm A) = lcm A" shows "lcm = Lcm_eucl"
   6.231 -  by (intro ext, rule associated_eqI) (auto simp: assms intro: Lcm_eucl_least)  
   6.232 -
   6.233 -lemma Gcd_eucl_dvd: "a \<in> A \<Longrightarrow> Gcd_eucl A dvd a"
   6.234 -  unfolding Gcd_eucl_def by (auto intro: Lcm_eucl_least)
   6.235 -
   6.236 -lemma Gcd_eucl_greatest: "(\<And>x. x \<in> A \<Longrightarrow> d dvd x) \<Longrightarrow> d dvd Gcd_eucl A"
   6.237 -  unfolding Gcd_eucl_def by auto
   6.238 -
   6.239 -lemma normalize_Gcd_eucl [simp]: "normalize (Gcd_eucl A) = Gcd_eucl A"
   6.240 -  by (simp add: Gcd_eucl_def)
   6.241 -
   6.242 -lemma Lcm_euclI:
   6.243 -  assumes "\<And>x. x \<in> A \<Longrightarrow> x dvd d" "\<And>d'. (\<And>x. x \<in> A \<Longrightarrow> x dvd d') \<Longrightarrow> d dvd d'" "normalize d = d"
   6.244 -  shows   "Lcm_eucl A = d"
   6.245 -proof -
   6.246 -  have "normalize (Lcm_eucl A) = normalize d"
   6.247 -    by (intro associatedI) (auto intro: dvd_Lcm_eucl Lcm_eucl_least assms)
   6.248 -  thus ?thesis by (simp add: assms)
   6.249 +  show "normalize (gcd a b) = gcd a b" for a b
   6.250 +    by (induct a b rule: eucl_induct)
   6.251 +      (simp_all add: local.gcd_0 local.gcd_mod)
   6.252 +next
   6.253 +  show "lcm a b = normalize (a * b) div gcd a b" for a b
   6.254 +    by (fact local.lcm_def)
   6.255  qed
   6.256  
   6.257 -lemma Gcd_euclI:
   6.258 -  assumes "\<And>x. x \<in> A \<Longrightarrow> d dvd x" "\<And>d'. (\<And>x. x \<in> A \<Longrightarrow> d' dvd x) \<Longrightarrow> d' dvd d" "normalize d = d"
   6.259 -  shows   "Gcd_eucl A = d"
   6.260 -proof -
   6.261 -  have "normalize (Gcd_eucl A) = normalize d"
   6.262 -    by (intro associatedI) (auto intro: Gcd_eucl_dvd Gcd_eucl_greatest assms)
   6.263 -  thus ?thesis by (simp add: assms)
   6.264 -qed
   6.265 +interpretation semiring_gcd one zero times gcd lcm
   6.266 +  divide plus minus normalize unit_factor
   6.267 +  by (fact semiring_gcd)
   6.268    
   6.269 -lemmas lcm_gcd_eucl_facts = 
   6.270 -  gcd_eucl_dvd1 gcd_eucl_dvd2 gcd_eucl_greatest normalize_gcd_eucl lcm_eucl_def
   6.271 -  Gcd_eucl_def Gcd_eucl_dvd Gcd_eucl_greatest normalize_Gcd_eucl
   6.272 -  dvd_Lcm_eucl Lcm_eucl_least normalize_Lcm_eucl
   6.273 -
   6.274 -lemma normalized_factors_product:
   6.275 -  "{p. p dvd a * b \<and> normalize p = p} = 
   6.276 -     (\<lambda>(x,y). x * y) ` ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})"
   6.277 -proof safe
   6.278 -  fix p assume p: "p dvd a * b" "normalize p = p"
   6.279 -  interpret semiring_gcd 1 0 "op *" gcd_eucl lcm_eucl "op div" "op +" "op -" normalize unit_factor
   6.280 -    by standard (rule lcm_gcd_eucl_facts; assumption)+
   6.281 -  from dvd_productE[OF p(1)] guess x y . note xy = this
   6.282 -  define x' y' where "x' = normalize x" and "y' = normalize y"
   6.283 -  have "p = x' * y'"
   6.284 -    by (subst p(2) [symmetric]) (simp add: xy x'_def y'_def normalize_mult)
   6.285 -  moreover from xy have "normalize x' = x'" "normalize y' = y'" "x' dvd a" "y' dvd b" 
   6.286 -    by (simp_all add: x'_def y'_def)
   6.287 -  ultimately show "p \<in> (\<lambda>(x, y). x * y) ` 
   6.288 -                     ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})"
   6.289 -    by blast
   6.290 -qed (auto simp: normalize_mult mult_dvd_mono)
   6.291 -
   6.292 -
   6.293 -subclass factorial_semiring
   6.294 -proof (standard, rule factorial_semiring_altI_aux)
   6.295 -  fix x assume "x \<noteq> 0"
   6.296 -  thus "finite {p. p dvd x \<and> normalize p = p}"
   6.297 -  proof (induction "euclidean_size x" arbitrary: x rule: less_induct)
   6.298 -    case (less x)
   6.299 -    show ?case
   6.300 -    proof (cases "\<exists>y. y dvd x \<and> \<not>x dvd y \<and> \<not>is_unit y")
   6.301 +lemma semiring_Gcd:
   6.302 +  "class.semiring_Gcd one zero times gcd lcm Gcd Lcm
   6.303 +    divide plus minus normalize unit_factor"
   6.304 +proof -
   6.305 +  show ?thesis
   6.306 +  proof
   6.307 +    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
   6.308 +    proof (cases "\<exists>l. l \<noteq>  0 \<and> (\<forall>a\<in>A. a dvd l)")
   6.309        case False
   6.310 -      have "{p. p dvd x \<and> normalize p = p} \<subseteq> {1, normalize x}"
   6.311 -      proof
   6.312 -        fix p assume p: "p \<in> {p. p dvd x \<and> normalize p = p}"
   6.313 -        with False have "is_unit p \<or> x dvd p" by blast
   6.314 -        thus "p \<in> {1, normalize x}"
   6.315 -        proof (elim disjE)
   6.316 -          assume "is_unit p"
   6.317 -          hence "normalize p = 1" by (simp add: is_unit_normalize)
   6.318 -          with p show ?thesis by simp
   6.319 -        next
   6.320 -          assume "x dvd p"
   6.321 -          with p have "normalize p = normalize x" by (intro associatedI) simp_all
   6.322 -          with p show ?thesis by simp
   6.323 -        qed
   6.324 -      qed
   6.325 -      moreover have "finite \<dots>" by simp
   6.326 -      ultimately show ?thesis by (rule finite_subset)
   6.327 -      
   6.328 +      then have "Lcm A = 0"
   6.329 +        by (auto simp add: local.Lcm_def)
   6.330 +      with False show ?thesis
   6.331 +        by auto
   6.332      next
   6.333        case True
   6.334 -      then obtain y where y: "y dvd x" "\<not>x dvd y" "\<not>is_unit y" by blast
   6.335 -      define z where "z = x div y"
   6.336 -      let ?fctrs = "\<lambda>x. {p. p dvd x \<and> normalize p = p}"
   6.337 -      from y have x: "x = y * z" by (simp add: z_def)
   6.338 -      with less.prems have "y \<noteq> 0" "z \<noteq> 0" by auto
   6.339 -      from x y have "\<not>is_unit z" by (auto simp: mult_unit_dvd_iff)
   6.340 -      have "?fctrs x = (\<lambda>(p,p'). p * p') ` (?fctrs y \<times> ?fctrs z)"
   6.341 -        by (subst x) (rule normalized_factors_product)
   6.342 -      also have "\<not>y * z dvd y * 1" "\<not>y * z dvd 1 * z"
   6.343 -        by (subst dvd_times_left_cancel_iff dvd_times_right_cancel_iff; fact)+
   6.344 -      hence "finite ((\<lambda>(p,p'). p * p') ` (?fctrs y \<times> ?fctrs z))"
   6.345 -        by (intro finite_imageI finite_cartesian_product less dvd_proper_imp_size_less)
   6.346 -           (auto simp: x)
   6.347 +      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
   6.348 +      define n where "n = (LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n)"
   6.349 +      define l where "l = (SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n)"
   6.350 +      have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
   6.351 +        apply (subst n_def)
   6.352 +        apply (rule LeastI [of _ "euclidean_size l\<^sub>0"])
   6.353 +        apply (rule exI [of _ l\<^sub>0])
   6.354 +        apply (simp add: l\<^sub>0_props)
   6.355 +        done
   6.356 +      from someI_ex [OF this] have "l \<noteq> 0" and "\<forall>a\<in>A. a dvd l"
   6.357 +        and "euclidean_size l = n" 
   6.358 +        unfolding l_def by simp_all
   6.359 +      {
   6.360 +        fix l' assume "\<forall>a\<in>A. a dvd l'"
   6.361 +        with \<open>\<forall>a\<in>A. a dvd l\<close> have "\<forall>a\<in>A. a dvd gcd l l'"
   6.362 +          by (auto intro: gcd_greatest)
   6.363 +        moreover from \<open>l \<noteq> 0\<close> have "gcd l l' \<noteq> 0"
   6.364 +          by simp
   6.365 +        ultimately have "\<exists>b. b \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd b) \<and> 
   6.366 +          euclidean_size b = euclidean_size (gcd l l')"
   6.367 +          by (intro exI [of _ "gcd l l'"], auto)
   6.368 +        then have "euclidean_size (gcd l l') \<ge> n"
   6.369 +          by (subst n_def) (rule Least_le)
   6.370 +        moreover have "euclidean_size (gcd l l') \<le> n"
   6.371 +        proof -
   6.372 +          have "gcd l l' dvd l"
   6.373 +            by simp
   6.374 +          then obtain a where "l = gcd l l' * a" ..
   6.375 +          with \<open>l \<noteq> 0\<close> have "a \<noteq> 0"
   6.376 +            by auto
   6.377 +          hence "euclidean_size (gcd l l') \<le> euclidean_size (gcd l l' * a)"
   6.378 +            by (rule size_mult_mono)
   6.379 +          also have "gcd l l' * a = l" using \<open>l = gcd l l' * a\<close> ..
   6.380 +          also note \<open>euclidean_size l = n\<close>
   6.381 +          finally show "euclidean_size (gcd l l') \<le> n" .
   6.382 +        qed
   6.383 +        ultimately have *: "euclidean_size l = euclidean_size (gcd l l')" 
   6.384 +          by (intro le_antisym, simp_all add: \<open>euclidean_size l = n\<close>)
   6.385 +        from \<open>l \<noteq> 0\<close> have "l dvd gcd l l'"
   6.386 +          by (rule dvd_euclidean_size_eq_imp_dvd) (auto simp add: *)
   6.387 +        hence "l dvd l'" by (rule dvd_trans [OF _ gcd_dvd2])
   6.388 +      }
   6.389 +      with \<open>\<forall>a\<in>A. a dvd l\<close> and \<open>l \<noteq> 0\<close>
   6.390 +        have "(\<forall>a\<in>A. a dvd normalize l) \<and> 
   6.391 +          (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> normalize l dvd l')"
   6.392 +        by auto
   6.393 +      also from True have "normalize l = Lcm A"
   6.394 +        by (simp add: local.Lcm_def Let_def n_def l_def)
   6.395        finally show ?thesis .
   6.396      qed
   6.397 -  qed
   6.398 -next
   6.399 -  interpret semiring_gcd 1 0 "op *" gcd_eucl lcm_eucl "op div" "op +" "op -" normalize unit_factor
   6.400 -    by standard (rule lcm_gcd_eucl_facts; assumption)+
   6.401 -  fix p assume p: "irreducible p"
   6.402 -  thus "prime_elem p" by (rule irreducible_imp_prime_elem_gcd)
   6.403 -qed
   6.404 -
   6.405 -lemma gcd_eucl_eq_gcd_factorial: "gcd_eucl = gcd_factorial"
   6.406 -  by (intro ext gcd_euclI gcd_lcm_factorial)
   6.407 -
   6.408 -lemma lcm_eucl_eq_lcm_factorial: "lcm_eucl = lcm_factorial"
   6.409 -  by (intro ext) (simp add: lcm_eucl_def lcm_factorial_gcd_factorial gcd_eucl_eq_gcd_factorial)
   6.410 -
   6.411 -lemma Gcd_eucl_eq_Gcd_factorial: "Gcd_eucl = Gcd_factorial"
   6.412 -  by (intro ext Gcd_euclI gcd_lcm_factorial)
   6.413 -
   6.414 -lemma Lcm_eucl_eq_Lcm_factorial: "Lcm_eucl = Lcm_factorial"
   6.415 -  by (intro ext Lcm_euclI gcd_lcm_factorial)
   6.416 -
   6.417 -lemmas eucl_eq_factorial = 
   6.418 -  gcd_eucl_eq_gcd_factorial lcm_eucl_eq_lcm_factorial 
   6.419 -  Gcd_eucl_eq_Gcd_factorial Lcm_eucl_eq_Lcm_factorial
   6.420 -  
   6.421 -end
   6.422 -
   6.423 -context euclidean_ring
   6.424 -begin
   6.425 -
   6.426 -function euclid_ext_aux :: "'a \<Rightarrow> _" where
   6.427 -  "euclid_ext_aux r' r s' s t' t = (
   6.428 -     if r = 0 then let c = 1 div unit_factor r' in (s' * c, t' * c, normalize r')
   6.429 -     else let q = r' div r
   6.430 -          in  euclid_ext_aux r (r' mod r) s (s' - q * s) t (t' - q * t))"
   6.431 -by auto
   6.432 -termination by (relation "measure (\<lambda>(_,b,_,_,_,_). euclidean_size b)") (simp_all add: mod_size_less)
   6.433 -
   6.434 -declare euclid_ext_aux.simps [simp del]
   6.435 -
   6.436 -lemma euclid_ext_aux_correct:
   6.437 -  assumes "gcd_eucl r' r = gcd_eucl a b"
   6.438 -  assumes "s' * a + t' * b = r'"
   6.439 -  assumes "s * a + t * b = r"
   6.440 -  shows   "case euclid_ext_aux r' r s' s t' t of (x,y,c) \<Rightarrow>
   6.441 -             x * a + y * b = c \<and> c = gcd_eucl a b" (is "?P (euclid_ext_aux r' r s' s t' t)")
   6.442 -using assms
   6.443 -proof (induction r' r s' s t' t rule: euclid_ext_aux.induct)
   6.444 -  case (1 r' r s' s t' t)
   6.445 -  show ?case
   6.446 -  proof (cases "r = 0")
   6.447 -    case True
   6.448 -    hence "euclid_ext_aux r' r s' s t' t = 
   6.449 -             (s' div unit_factor r', t' div unit_factor r', normalize r')"
   6.450 -      by (subst euclid_ext_aux.simps) (simp add: Let_def)
   6.451 -    also have "?P \<dots>"
   6.452 -    proof safe
   6.453 -      have "s' div unit_factor r' * a + t' div unit_factor r' * b = 
   6.454 -                (s' * a + t' * b) div unit_factor r'"
   6.455 -        by (cases "r' = 0") (simp_all add: unit_div_commute)
   6.456 -      also have "s' * a + t' * b = r'" by fact
   6.457 -      also have "\<dots> div unit_factor r' = normalize r'" by simp
   6.458 -      finally show "s' div unit_factor r' * a + t' div unit_factor r' * b = normalize r'" .
   6.459 -    next
   6.460 -      from "1.prems" True show "normalize r' = gcd_eucl a b" by (simp add: gcd_eucl_0)
   6.461 -    qed
   6.462 -    finally show ?thesis .
   6.463 -  next
   6.464 -    case False
   6.465 -    hence "euclid_ext_aux r' r s' s t' t = 
   6.466 -             euclid_ext_aux r (r' mod r) s (s' - r' div r * s) t (t' - r' div r * t)"
   6.467 -      by (subst euclid_ext_aux.simps) (simp add: Let_def)
   6.468 -    also from "1.prems" False have "?P \<dots>"
   6.469 -    proof (intro "1.IH")
   6.470 -      have "(s' - r' div r * s) * a + (t' - r' div r * t) * b =
   6.471 -              (s' * a + t' * b) - r' div r * (s * a + t * b)" by (simp add: algebra_simps)
   6.472 -      also have "s' * a + t' * b = r'" by fact
   6.473 -      also have "s * a + t * b = r" by fact
   6.474 -      also have "r' - r' div r * r = r' mod r" using div_mult_mod_eq [of r' r]
   6.475 -        by (simp add: algebra_simps)
   6.476 -      finally show "(s' - r' div r * s) * a + (t' - r' div r * t) * b = r' mod r" .
   6.477 -    qed (auto simp: gcd_eucl_non_0 algebra_simps minus_mod_eq_div_mult [symmetric])
   6.478 -    finally show ?thesis .
   6.479 +    then show dvd_Lcm: "a \<in> A \<Longrightarrow> a dvd Lcm A"
   6.480 +      and Lcm_least: "(\<And>a. a \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> Lcm A dvd b" for A and a b
   6.481 +      by auto
   6.482 +    show "a \<in> A \<Longrightarrow> Gcd A dvd a" for A and a
   6.483 +      by (auto simp add: local.Gcd_def intro: Lcm_least)
   6.484 +    show "(\<And>a. a \<in> A \<Longrightarrow> b dvd a) \<Longrightarrow> b dvd Gcd A" for A and b
   6.485 +      by (auto simp add: local.Gcd_def intro: dvd_Lcm)
   6.486 +    show [simp]: "normalize (Lcm A) = Lcm A" for A
   6.487 +      by (simp add: local.Lcm_def)
   6.488 +    show "normalize (Gcd A) = Gcd A" for A
   6.489 +      by (simp add: local.Gcd_def)
   6.490    qed
   6.491  qed
   6.492  
   6.493 -definition euclid_ext where
   6.494 -  "euclid_ext a b = euclid_ext_aux a b 1 0 0 1"
   6.495 -
   6.496 -lemma euclid_ext_0: 
   6.497 -  "euclid_ext a 0 = (1 div unit_factor a, 0, normalize a)"
   6.498 -  by (simp add: euclid_ext_def euclid_ext_aux.simps)
   6.499 -
   6.500 -lemma euclid_ext_left_0: 
   6.501 -  "euclid_ext 0 a = (0, 1 div unit_factor a, normalize a)"
   6.502 -  by (simp add: euclid_ext_def euclid_ext_aux.simps)
   6.503 -
   6.504 -lemma euclid_ext_correct':
   6.505 -  "case euclid_ext a b of (x,y,c) \<Rightarrow> x * a + y * b = c \<and> c = gcd_eucl a b"
   6.506 -  unfolding euclid_ext_def by (rule euclid_ext_aux_correct) simp_all
   6.507 +interpretation semiring_Gcd one zero times gcd lcm Gcd Lcm
   6.508 +    divide plus minus normalize unit_factor
   6.509 +  by (fact semiring_Gcd)
   6.510  
   6.511 -lemma euclid_ext_gcd_eucl:
   6.512 -  "(case euclid_ext a b of (x,y,c) \<Rightarrow> c) = gcd_eucl a b"
   6.513 -  using euclid_ext_correct'[of a b] by (simp add: case_prod_unfold)
   6.514 -
   6.515 -definition euclid_ext' where
   6.516 -  "euclid_ext' a b = (case euclid_ext a b of (x, y, _) \<Rightarrow> (x, y))"
   6.517 +subclass factorial_semiring
   6.518 +proof -
   6.519 +  show "class.factorial_semiring divide plus minus zero times one
   6.520 +     normalize unit_factor"
   6.521 +  proof (standard, rule factorial_semiring_altI_aux) -- \<open>FIXME rule\<close>
   6.522 +    fix x assume "x \<noteq> 0"
   6.523 +    thus "finite {p. p dvd x \<and> normalize p = p}"
   6.524 +    proof (induction "euclidean_size x" arbitrary: x rule: less_induct)
   6.525 +      case (less x)
   6.526 +      show ?case
   6.527 +      proof (cases "\<exists>y. y dvd x \<and> \<not>x dvd y \<and> \<not>is_unit y")
   6.528 +        case False
   6.529 +        have "{p. p dvd x \<and> normalize p = p} \<subseteq> {1, normalize x}"
   6.530 +        proof
   6.531 +          fix p assume p: "p \<in> {p. p dvd x \<and> normalize p = p}"
   6.532 +          with False have "is_unit p \<or> x dvd p" by blast
   6.533 +          thus "p \<in> {1, normalize x}"
   6.534 +          proof (elim disjE)
   6.535 +            assume "is_unit p"
   6.536 +            hence "normalize p = 1" by (simp add: is_unit_normalize)
   6.537 +            with p show ?thesis by simp
   6.538 +          next
   6.539 +            assume "x dvd p"
   6.540 +            with p have "normalize p = normalize x" by (intro associatedI) simp_all
   6.541 +            with p show ?thesis by simp
   6.542 +          qed
   6.543 +        qed
   6.544 +        moreover have "finite \<dots>" by simp
   6.545 +        ultimately show ?thesis by (rule finite_subset)
   6.546 +      next
   6.547 +        case True
   6.548 +        then obtain y where y: "y dvd x" "\<not>x dvd y" "\<not>is_unit y" by blast
   6.549 +        define z where "z = x div y"
   6.550 +        let ?fctrs = "\<lambda>x. {p. p dvd x \<and> normalize p = p}"
   6.551 +        from y have x: "x = y * z" by (simp add: z_def)
   6.552 +        with less.prems have "y \<noteq> 0" "z \<noteq> 0" by auto
   6.553 +        have normalized_factors_product:
   6.554 +          "{p. p dvd a * b \<and> normalize p = p} = 
   6.555 +             (\<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
   6.556 +        proof safe
   6.557 +          fix p assume p: "p dvd a * b" "normalize p = p"
   6.558 +          from dvd_productE[OF p(1)] guess x y . note xy = this
   6.559 +          define x' y' where "x' = normalize x" and "y' = normalize y"
   6.560 +          have "p = x' * y'"
   6.561 +            by (subst p(2) [symmetric]) (simp add: xy x'_def y'_def normalize_mult)
   6.562 +          moreover from xy have "normalize x' = x'" "normalize y' = y'" "x' dvd a" "y' dvd b" 
   6.563 +            by (simp_all add: x'_def y'_def)
   6.564 +          ultimately show "p \<in> (\<lambda>(x, y). x * y) ` 
   6.565 +            ({p. p dvd a \<and> normalize p = p} \<times> {p. p dvd b \<and> normalize p = p})"
   6.566 +            by blast
   6.567 +        qed (auto simp: normalize_mult mult_dvd_mono)
   6.568 +        from x y have "\<not>is_unit z" by (auto simp: mult_unit_dvd_iff)
   6.569 +        have "?fctrs x = (\<lambda>(p,p'). p * p') ` (?fctrs y \<times> ?fctrs z)"
   6.570 +          by (subst x) (rule normalized_factors_product)
   6.571 +        also have "\<not>y * z dvd y * 1" "\<not>y * z dvd 1 * z"
   6.572 +          by (subst dvd_times_left_cancel_iff dvd_times_right_cancel_iff; fact)+
   6.573 +        hence "finite ((\<lambda>(p,p'). p * p') ` (?fctrs y \<times> ?fctrs z))"
   6.574 +          by (intro finite_imageI finite_cartesian_product less dvd_proper_imp_size_less)
   6.575 +             (auto simp: x)
   6.576 +        finally show ?thesis .
   6.577 +      qed
   6.578 +    qed
   6.579 +  next
   6.580 +    fix p
   6.581 +    assume "irreducible p"
   6.582 +    then show "prime_elem p"
   6.583 +      by (rule irreducible_imp_prime_elem_gcd)
   6.584 +  qed
   6.585 +qed
   6.586  
   6.587 -lemma euclid_ext'_correct':
   6.588 -  "case euclid_ext' a b of (x,y) \<Rightarrow> x * a + y * b = gcd_eucl a b"
   6.589 -  using euclid_ext_correct'[of a b] by (simp add: case_prod_unfold euclid_ext'_def)
   6.590 +lemma Gcd_eucl_set [code]:
   6.591 +  "Gcd (set xs) = foldl gcd 0 xs"
   6.592 +  by (fact local.Gcd_set)
   6.593  
   6.594 -lemma euclid_ext'_0: "euclid_ext' a 0 = (1 div unit_factor a, 0)" 
   6.595 -  by (simp add: euclid_ext'_def euclid_ext_0)
   6.596 -
   6.597 -lemma euclid_ext'_left_0: "euclid_ext' 0 a = (0, 1 div unit_factor a)" 
   6.598 -  by (simp add: euclid_ext'_def euclid_ext_left_0)
   6.599 -
   6.600 +lemma Lcm_eucl_set [code]:
   6.601 +  "Lcm (set xs) = foldl lcm 1 xs"
   6.602 +  by (fact local.Lcm_set)
   6.603 + 
   6.604  end
   6.605  
   6.606 +hide_const (open) gcd lcm Gcd Lcm
   6.607 +
   6.608 +lemma prime_elem_int_abs_iff [simp]:
   6.609 +  fixes p :: int
   6.610 +  shows "prime_elem \<bar>p\<bar> \<longleftrightarrow> prime_elem p"
   6.611 +  using prime_elem_normalize_iff [of p] by simp
   6.612 +  
   6.613 +lemma prime_elem_int_minus_iff [simp]:
   6.614 +  fixes p :: int
   6.615 +  shows "prime_elem (- p) \<longleftrightarrow> prime_elem p"
   6.616 +  using prime_elem_normalize_iff [of "- p"] by simp
   6.617 +
   6.618 +lemma prime_int_iff:
   6.619 +  fixes p :: int
   6.620 +  shows "prime p \<longleftrightarrow> p > 0 \<and> prime_elem p"
   6.621 +  by (auto simp add: prime_def dest: prime_elem_not_zeroI)
   6.622 +  
   6.623 +  
   6.624 +subsection \<open>The (simple) euclidean algorithm as gcd computation\<close>
   6.625 +  
   6.626  class euclidean_semiring_gcd = euclidean_semiring + gcd + Gcd +
   6.627 -  assumes gcd_gcd_eucl: "gcd = gcd_eucl" and lcm_lcm_eucl: "lcm = lcm_eucl"
   6.628 -  assumes Gcd_Gcd_eucl: "Gcd = Gcd_eucl" and Lcm_Lcm_eucl: "Lcm = Lcm_eucl"
   6.629 +  assumes gcd_eucl: "Euclidean_Algorithm.gcd = GCD.gcd"
   6.630 +    and lcm_eucl: "Euclidean_Algorithm.lcm = GCD.lcm"
   6.631 +  assumes Gcd_eucl: "Euclidean_Algorithm.Gcd = GCD.Gcd"
   6.632 +    and Lcm_eucl: "Euclidean_Algorithm.Lcm = GCD.Lcm"
   6.633  begin
   6.634  
   6.635  subclass semiring_gcd
   6.636 -  by standard (simp_all add: gcd_gcd_eucl gcd_eucl_greatest lcm_lcm_eucl lcm_eucl_def)
   6.637 +  unfolding gcd_eucl [symmetric] lcm_eucl [symmetric]
   6.638 +  by (fact semiring_gcd)
   6.639  
   6.640  subclass semiring_Gcd
   6.641 -  by standard (auto simp: Gcd_Gcd_eucl Lcm_Lcm_eucl Gcd_eucl_def intro: Lcm_eucl_least)
   6.642 +  unfolding  gcd_eucl [symmetric] lcm_eucl [symmetric]
   6.643 +    Gcd_eucl [symmetric] Lcm_eucl [symmetric]
   6.644 +  by (fact semiring_Gcd)
   6.645  
   6.646  subclass factorial_semiring_gcd
   6.647  proof
   6.648 -  fix a b
   6.649 -  show "gcd a b = gcd_factorial a b"
   6.650 -    by (rule sym, rule gcdI) (rule gcd_lcm_factorial; assumption)+
   6.651 -  thus "lcm a b = lcm_factorial a b"
   6.652 +  show "gcd a b = gcd_factorial a b" for a b
   6.653 +    apply (rule sym)
   6.654 +    apply (rule gcdI)
   6.655 +       apply (fact gcd_lcm_factorial)+
   6.656 +    done
   6.657 +  then show "lcm a b = lcm_factorial a b" for a b
   6.658      by (simp add: lcm_factorial_gcd_factorial lcm_gcd)
   6.659 -next
   6.660 -  fix A 
   6.661 -  show "Gcd A = Gcd_factorial A"
   6.662 -    by (rule sym, rule GcdI) (rule gcd_lcm_factorial; assumption)+
   6.663 -  show "Lcm A = Lcm_factorial A"
   6.664 -    by (rule sym, rule LcmI) (rule gcd_lcm_factorial; assumption)+
   6.665 +  show "Gcd A = Gcd_factorial A" for A
   6.666 +    apply (rule sym)
   6.667 +    apply (rule GcdI)
   6.668 +       apply (fact gcd_lcm_factorial)+
   6.669 +    done
   6.670 +  show "Lcm A = Lcm_factorial A" for A
   6.671 +    apply (rule sym)
   6.672 +    apply (rule LcmI)
   6.673 +       apply (fact gcd_lcm_factorial)+
   6.674 +    done
   6.675  qed
   6.676  
   6.677 -lemma gcd_non_0:
   6.678 -  "b \<noteq> 0 \<Longrightarrow> gcd a b = gcd b (a mod b)"
   6.679 -  unfolding gcd_gcd_eucl by (fact gcd_eucl_non_0)
   6.680 -
   6.681 -lemmas gcd_0 = gcd_0_right
   6.682 -lemmas dvd_gcd_iff = gcd_greatest_iff
   6.683 -lemmas gcd_greatest_iff = dvd_gcd_iff
   6.684 +lemma gcd_mod_right [simp]:
   6.685 +  "a \<noteq> 0 \<Longrightarrow> gcd a (b mod a) = gcd a b"
   6.686 +  unfolding gcd.commute [of a b]
   6.687 +  by (simp add: gcd_eucl [symmetric] local.gcd_mod)
   6.688  
   6.689 -lemma gcd_mod1 [simp]:
   6.690 -  "gcd (a mod b) b = gcd a b"
   6.691 -  by (rule gcdI, metis dvd_mod_iff gcd_dvd1 gcd_dvd2, simp_all add: gcd_greatest dvd_mod_iff)
   6.692 +lemma gcd_mod_left [simp]:
   6.693 +  "b \<noteq> 0 \<Longrightarrow> gcd (a mod b) b = gcd a b"
   6.694 +  by (drule gcd_mod_right [of _ a]) (simp add: gcd.commute)
   6.695  
   6.696 -lemma gcd_mod2 [simp]:
   6.697 -  "gcd a (b mod a) = gcd a b"
   6.698 -  by (rule gcdI, simp, metis dvd_mod_iff gcd_dvd1 gcd_dvd2, simp_all add: gcd_greatest dvd_mod_iff)
   6.699 -         
   6.700  lemma euclidean_size_gcd_le1 [simp]:
   6.701    assumes "a \<noteq> 0"
   6.702    shows "euclidean_size (gcd a b) \<le> euclidean_size a"
   6.703  proof -
   6.704 -   have "gcd a b dvd a" by (rule gcd_dvd1)
   6.705 -   then obtain c where A: "a = gcd a b * c" unfolding dvd_def by blast
   6.706 -   with \<open>a \<noteq> 0\<close> show ?thesis by (subst (2) A, intro size_mult_mono) auto
   6.707 +  from gcd_dvd1 obtain c where A: "a = gcd a b * c" ..
   6.708 +  with assms have "c \<noteq> 0"
   6.709 +    by auto
   6.710 +  moreover from this
   6.711 +  have "euclidean_size (gcd a b) \<le> euclidean_size (gcd a b * c)"
   6.712 +    by (rule size_mult_mono)
   6.713 +  with A show ?thesis
   6.714 +    by simp
   6.715  qed
   6.716  
   6.717  lemma euclidean_size_gcd_le2 [simp]:
   6.718 @@ -464,7 +348,7 @@
   6.719    by (subst gcd.commute, rule euclidean_size_gcd_le1)
   6.720  
   6.721  lemma euclidean_size_gcd_less1:
   6.722 -  assumes "a \<noteq> 0" and "\<not>a dvd b"
   6.723 +  assumes "a \<noteq> 0" and "\<not> a dvd b"
   6.724    shows "euclidean_size (gcd a b) < euclidean_size a"
   6.725  proof (rule ccontr)
   6.726    assume "\<not>euclidean_size (gcd a b) < euclidean_size a"
   6.727 @@ -473,11 +357,11 @@
   6.728    have "a dvd gcd a b"
   6.729      by (rule dvd_euclidean_size_eq_imp_dvd) (simp_all add: assms A)
   6.730    hence "a dvd b" using dvd_gcdD2 by blast
   6.731 -  with \<open>\<not>a dvd b\<close> show False by contradiction
   6.732 +  with \<open>\<not> a dvd b\<close> show False by contradiction
   6.733  qed
   6.734  
   6.735  lemma euclidean_size_gcd_less2:
   6.736 -  assumes "b \<noteq> 0" and "\<not>b dvd a"
   6.737 +  assumes "b \<noteq> 0" and "\<not> b dvd a"
   6.738    shows "euclidean_size (gcd a b) < euclidean_size b"
   6.739    using assms by (subst gcd.commute, rule euclidean_size_gcd_less1)
   6.740  
   6.741 @@ -496,7 +380,7 @@
   6.742    using euclidean_size_lcm_le1 [of b a] by (simp add: ac_simps)
   6.743  
   6.744  lemma euclidean_size_lcm_less1:
   6.745 -  assumes "b \<noteq> 0" and "\<not>b dvd a"
   6.746 +  assumes "b \<noteq> 0" and "\<not> b dvd a"
   6.747    shows "euclidean_size a < euclidean_size (lcm a b)"
   6.748  proof (rule ccontr)
   6.749    from assms have "a \<noteq> 0" by auto
   6.750 @@ -510,26 +394,49 @@
   6.751  qed
   6.752  
   6.753  lemma euclidean_size_lcm_less2:
   6.754 -  assumes "a \<noteq> 0" and "\<not>a dvd b"
   6.755 +  assumes "a \<noteq> 0" and "\<not> a dvd b"
   6.756    shows "euclidean_size b < euclidean_size (lcm a b)"
   6.757    using assms euclidean_size_lcm_less1 [of a b] by (simp add: ac_simps)
   6.758  
   6.759 -lemma Lcm_eucl_set [code]:
   6.760 -  "Lcm_eucl (set xs) = foldl lcm_eucl 1 xs"
   6.761 -  by (simp add: Lcm_Lcm_eucl [symmetric] lcm_lcm_eucl Lcm_set)
   6.762 -
   6.763 -lemma Gcd_eucl_set [code]:
   6.764 -  "Gcd_eucl (set xs) = foldl gcd_eucl 0 xs"
   6.765 -  by (simp add: Gcd_Gcd_eucl [symmetric] gcd_gcd_eucl Gcd_set)
   6.766 -
   6.767  end
   6.768  
   6.769 +lemma factorial_euclidean_semiring_gcdI:
   6.770 +  "OFCLASS('a::{factorial_semiring_gcd, euclidean_semiring}, euclidean_semiring_gcd_class)"
   6.771 +proof
   6.772 +  interpret semiring_Gcd 1 0 times
   6.773 +    Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm
   6.774 +    Euclidean_Algorithm.Gcd Euclidean_Algorithm.Lcm
   6.775 +    divide plus minus normalize unit_factor
   6.776 +    rewrites "dvd.dvd op * = Rings.dvd"
   6.777 +    by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   6.778 +  show [simp]: "Euclidean_Algorithm.gcd = (gcd :: 'a \<Rightarrow> _)"
   6.779 +  proof (rule ext)+
   6.780 +    fix a b :: 'a
   6.781 +    show "Euclidean_Algorithm.gcd a b = gcd a b"
   6.782 +    proof (induct a b rule: eucl_induct)
   6.783 +      case zero
   6.784 +      then show ?case
   6.785 +        by simp
   6.786 +    next
   6.787 +      case (mod a b)
   6.788 +      moreover have "gcd b (a mod b) = gcd b a"
   6.789 +        using GCD.gcd_add_mult [of b "a div b" "a mod b", symmetric]
   6.790 +          by (simp add: div_mult_mod_eq)
   6.791 +      ultimately show ?case
   6.792 +        by (simp add: Euclidean_Algorithm.gcd_mod ac_simps)
   6.793 +    qed
   6.794 +  qed
   6.795 +  show [simp]: "Euclidean_Algorithm.Lcm = (Lcm :: 'a set \<Rightarrow> _)"
   6.796 +    by (auto intro!: Lcm_eqI GCD.dvd_Lcm GCD.Lcm_least)
   6.797 +  show "Euclidean_Algorithm.lcm = (lcm :: 'a \<Rightarrow> _)"
   6.798 +    by (simp add: fun_eq_iff Euclidean_Algorithm.lcm_def semiring_gcd_class.lcm_gcd)
   6.799 +  show "Euclidean_Algorithm.Gcd = (Gcd :: 'a set \<Rightarrow> _)"
   6.800 +    by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm)
   6.801 +qed
   6.802  
   6.803 -text \<open>
   6.804 -  A Euclidean ring is a Euclidean semiring with additive inverses. It provides a 
   6.805 -  few more lemmas; in particular, Bezout's lemma holds for any Euclidean ring.
   6.806 -\<close>
   6.807  
   6.808 +subsection \<open>The extended euclidean algorithm\<close>
   6.809 +  
   6.810  class euclidean_ring_gcd = euclidean_semiring_gcd + idom
   6.811  begin
   6.812  
   6.813 @@ -537,26 +444,109 @@
   6.814  subclass ring_gcd ..
   6.815  subclass factorial_ring_gcd ..
   6.816  
   6.817 -lemma euclid_ext_gcd [simp]:
   6.818 -  "(case euclid_ext a b of (_, _ , t) \<Rightarrow> t) = gcd a b"
   6.819 -  using euclid_ext_correct'[of a b] by (simp add: case_prod_unfold Let_def gcd_gcd_eucl)
   6.820 -
   6.821 -lemma euclid_ext_gcd' [simp]:
   6.822 -  "euclid_ext a b = (r, s, t) \<Longrightarrow> t = gcd a b"
   6.823 -  by (insert euclid_ext_gcd[of a b], drule (1) subst, simp)
   6.824 +function euclid_ext_aux :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a \<times> 'a) \<times> 'a"
   6.825 +  where "euclid_ext_aux s' s t' t r' r = (
   6.826 +     if r = 0 then let c = 1 div unit_factor r' in ((s' * c, t' * c), normalize r')
   6.827 +     else let q = r' div r
   6.828 +          in euclid_ext_aux s (s' - q * s) t (t' - q * t) r (r' mod r))"
   6.829 +  by auto
   6.830 +termination
   6.831 +  by (relation "measure (\<lambda>(_, _, _, _, _, b). euclidean_size b)")
   6.832 +    (simp_all add: mod_size_less)
   6.833  
   6.834 -lemma euclid_ext_correct:
   6.835 -  "case euclid_ext a b of (x,y,c) \<Rightarrow> x * a + y * b = c \<and> c = gcd a b"
   6.836 -  using euclid_ext_correct'[of a b]
   6.837 -  by (simp add: gcd_gcd_eucl case_prod_unfold)
   6.838 -  
   6.839 -lemma euclid_ext'_correct:
   6.840 -  "fst (euclid_ext' a b) * a + snd (euclid_ext' a b) * b = gcd a b"
   6.841 -  using euclid_ext_correct'[of a b]
   6.842 -  by (simp add: gcd_gcd_eucl case_prod_unfold euclid_ext'_def)
   6.843 +abbreviation (input) euclid_ext :: "'a \<Rightarrow> 'a \<Rightarrow> ('a \<times> 'a) \<times> 'a"
   6.844 +  where "euclid_ext \<equiv> euclid_ext_aux 1 0 0 1"
   6.845 +    
   6.846 +lemma
   6.847 +  assumes "gcd r' r = gcd a b"
   6.848 +  assumes "s' * a + t' * b = r'"
   6.849 +  assumes "s * a + t * b = r"
   6.850 +  assumes "euclid_ext_aux s' s t' t r' r = ((x, y), c)"
   6.851 +  shows euclid_ext_aux_eq_gcd: "c = gcd a b"
   6.852 +    and euclid_ext_aux_bezout: "x * a + y * b = gcd a b"
   6.853 +proof -
   6.854 +  have "case euclid_ext_aux s' s t' t r' r of ((x, y), c) \<Rightarrow> 
   6.855 +    x * a + y * b = c \<and> c = gcd a b" (is "?P (euclid_ext_aux s' s t' t r' r)")
   6.856 +    using assms(1-3)
   6.857 +  proof (induction s' s t' t r' r rule: euclid_ext_aux.induct)
   6.858 +    case (1 s' s t' t r' r)
   6.859 +    show ?case
   6.860 +    proof (cases "r = 0")
   6.861 +      case True
   6.862 +      hence "euclid_ext_aux s' s t' t r' r = 
   6.863 +               ((s' div unit_factor r', t' div unit_factor r'), normalize r')"
   6.864 +        by (subst euclid_ext_aux.simps) (simp add: Let_def)
   6.865 +      also have "?P \<dots>"
   6.866 +      proof safe
   6.867 +        have "s' div unit_factor r' * a + t' div unit_factor r' * b = 
   6.868 +                (s' * a + t' * b) div unit_factor r'"
   6.869 +          by (cases "r' = 0") (simp_all add: unit_div_commute)
   6.870 +        also have "s' * a + t' * b = r'" by fact
   6.871 +        also have "\<dots> div unit_factor r' = normalize r'" by simp
   6.872 +        finally show "s' div unit_factor r' * a + t' div unit_factor r' * b = normalize r'" .
   6.873 +      next
   6.874 +        from "1.prems" True show "normalize r' = gcd a b"
   6.875 +          by simp
   6.876 +      qed
   6.877 +      finally show ?thesis .
   6.878 +    next
   6.879 +      case False
   6.880 +      hence "euclid_ext_aux s' s t' t r' r = 
   6.881 +             euclid_ext_aux s (s' - r' div r * s) t (t' - r' div r * t) r (r' mod r)"
   6.882 +        by (subst euclid_ext_aux.simps) (simp add: Let_def)
   6.883 +      also from "1.prems" False have "?P \<dots>"
   6.884 +      proof (intro "1.IH")
   6.885 +        have "(s' - r' div r * s) * a + (t' - r' div r * t) * b =
   6.886 +              (s' * a + t' * b) - r' div r * (s * a + t * b)" by (simp add: algebra_simps)
   6.887 +        also have "s' * a + t' * b = r'" by fact
   6.888 +        also have "s * a + t * b = r" by fact
   6.889 +        also have "r' - r' div r * r = r' mod r" using div_mult_mod_eq [of r' r]
   6.890 +          by (simp add: algebra_simps)
   6.891 +        finally show "(s' - r' div r * s) * a + (t' - r' div r * t) * b = r' mod r" .
   6.892 +      qed (auto simp: gcd_mod_right algebra_simps minus_mod_eq_div_mult [symmetric] gcd.commute)
   6.893 +      finally show ?thesis .
   6.894 +    qed
   6.895 +  qed
   6.896 +  with assms(4) show "c = gcd a b" "x * a + y * b = gcd a b"
   6.897 +    by simp_all
   6.898 +qed
   6.899  
   6.900 -lemma bezout: "\<exists>s t. s * a + t * b = gcd a b"
   6.901 -  using euclid_ext'_correct by blast
   6.902 +declare euclid_ext_aux.simps [simp del]
   6.903 +
   6.904 +definition bezout_coefficients :: "'a \<Rightarrow> 'a \<Rightarrow> 'a \<times> 'a"
   6.905 +  where [code]: "bezout_coefficients a b = fst (euclid_ext a b)"
   6.906 +
   6.907 +lemma bezout_coefficients_0: 
   6.908 +  "bezout_coefficients a 0 = (1 div unit_factor a, 0)"
   6.909 +  by (simp add: bezout_coefficients_def euclid_ext_aux.simps)
   6.910 +
   6.911 +lemma bezout_coefficients_left_0: 
   6.912 +  "bezout_coefficients 0 a = (0, 1 div unit_factor a)"
   6.913 +  by (simp add: bezout_coefficients_def euclid_ext_aux.simps)
   6.914 +
   6.915 +lemma bezout_coefficients:
   6.916 +  assumes "bezout_coefficients a b = (x, y)"
   6.917 +  shows "x * a + y * b = gcd a b"
   6.918 +  using assms by (simp add: bezout_coefficients_def
   6.919 +    euclid_ext_aux_bezout [of a b a b 1 0 0 1 x y] prod_eq_iff)
   6.920 +
   6.921 +lemma bezout_coefficients_fst_snd:
   6.922 +  "fst (bezout_coefficients a b) * a + snd (bezout_coefficients a b) * b = gcd a b"
   6.923 +  by (rule bezout_coefficients) simp
   6.924 +
   6.925 +lemma euclid_ext_eq [simp]:
   6.926 +  "euclid_ext a b = (bezout_coefficients a b, gcd a b)" (is "?p = ?q")
   6.927 +proof
   6.928 +  show "fst ?p = fst ?q"
   6.929 +    by (simp add: bezout_coefficients_def)
   6.930 +  have "snd (euclid_ext_aux 1 0 0 1 a b) = gcd a b"
   6.931 +    by (rule euclid_ext_aux_eq_gcd [of a b a b 1 0 0 1])
   6.932 +      (simp_all add: prod_eq_iff)
   6.933 +  then show "snd ?p = snd ?q"
   6.934 +    by simp
   6.935 +qed
   6.936 +
   6.937 +declare euclid_ext_eq [symmetric, code_unfold]
   6.938  
   6.939  end
   6.940  
   6.941 @@ -565,19 +555,78 @@
   6.942  
   6.943  instance nat :: euclidean_semiring_gcd
   6.944  proof
   6.945 -  show [simp]: "gcd = (gcd_eucl :: nat \<Rightarrow> _)" "Lcm = (Lcm_eucl :: nat set \<Rightarrow> _)"
   6.946 -    by (simp_all add: eq_gcd_euclI eq_Lcm_euclI)
   6.947 -  show "lcm = (lcm_eucl :: nat \<Rightarrow> _)" "Gcd = (Gcd_eucl :: nat set \<Rightarrow> _)"
   6.948 -    by (intro ext, simp add: lcm_eucl_def lcm_nat_def Gcd_nat_def Gcd_eucl_def)+
   6.949 +  interpret semiring_Gcd 1 0 times
   6.950 +    "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
   6.951 +    "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
   6.952 +    divide plus minus normalize unit_factor
   6.953 +    rewrites "dvd.dvd op * = Rings.dvd"
   6.954 +    by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   6.955 +  show [simp]: "(Euclidean_Algorithm.gcd :: nat \<Rightarrow> _) = gcd"
   6.956 +  proof (rule ext)+
   6.957 +    fix m n :: nat
   6.958 +    show "Euclidean_Algorithm.gcd m n = gcd m n"
   6.959 +    proof (induct m n rule: eucl_induct)
   6.960 +      case zero
   6.961 +      then show ?case
   6.962 +        by simp
   6.963 +    next
   6.964 +      case (mod m n)
   6.965 +      then have "gcd n (m mod n) = gcd n m"
   6.966 +        using gcd_nat.simps [of m n] by (simp add: ac_simps)
   6.967 +      with mod show ?case
   6.968 +        by (simp add: Euclidean_Algorithm.gcd_mod ac_simps)
   6.969 +    qed
   6.970 +  qed
   6.971 +  show [simp]: "(Euclidean_Algorithm.Lcm :: nat set \<Rightarrow> _) = Lcm"
   6.972 +    by (auto intro!: ext Lcm_eqI)
   6.973 +  show "(Euclidean_Algorithm.lcm :: nat \<Rightarrow> _) = lcm"
   6.974 +    by (simp add: fun_eq_iff Euclidean_Algorithm.lcm_def semiring_gcd_class.lcm_gcd)
   6.975 +  show "(Euclidean_Algorithm.Gcd :: nat set \<Rightarrow> _) = Gcd"
   6.976 +    by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm)
   6.977  qed
   6.978  
   6.979  instance int :: euclidean_ring_gcd
   6.980  proof
   6.981 -  show [simp]: "gcd = (gcd_eucl :: int \<Rightarrow> _)" "Lcm = (Lcm_eucl :: int set \<Rightarrow> _)"
   6.982 -    by (simp_all add: eq_gcd_euclI eq_Lcm_euclI)
   6.983 -  show "lcm = (lcm_eucl :: int \<Rightarrow> _)" "Gcd = (Gcd_eucl :: int set \<Rightarrow> _)"
   6.984 -    by (intro ext, simp add: lcm_eucl_def lcm_altdef_int 
   6.985 -          semiring_Gcd_class.Gcd_Lcm Gcd_eucl_def abs_mult)+
   6.986 +  interpret semiring_Gcd 1 0 times
   6.987 +    "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
   6.988 +    "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
   6.989 +    divide plus minus normalize unit_factor
   6.990 +    rewrites "dvd.dvd op * = Rings.dvd"
   6.991 +    by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   6.992 +  show [simp]: "(Euclidean_Algorithm.gcd :: int \<Rightarrow> _) = gcd"
   6.993 +  proof (rule ext)+
   6.994 +    fix k l :: int
   6.995 +    show "Euclidean_Algorithm.gcd k l = gcd k l"
   6.996 +    proof (induct k l rule: eucl_induct)
   6.997 +      case zero
   6.998 +      then show ?case
   6.999 +        by simp
  6.1000 +    next
  6.1001 +      case (mod k l)
  6.1002 +      have "gcd l (k mod l) = gcd l k"
  6.1003 +      proof (cases l "0::int" rule: linorder_cases)
  6.1004 +        case less
  6.1005 +        then show ?thesis
  6.1006 +          using gcd_non_0_int [of "- l" "- k"] by (simp add: ac_simps)
  6.1007 +      next
  6.1008 +        case equal
  6.1009 +        with mod show ?thesis
  6.1010 +          by simp
  6.1011 +      next
  6.1012 +        case greater
  6.1013 +        then show ?thesis
  6.1014 +          using gcd_non_0_int [of l k] by (simp add: ac_simps)
  6.1015 +      qed
  6.1016 +      with mod show ?case
  6.1017 +        by (simp add: Euclidean_Algorithm.gcd_mod ac_simps)
  6.1018 +    qed
  6.1019 +  qed
  6.1020 +  show [simp]: "(Euclidean_Algorithm.Lcm :: int set \<Rightarrow> _) = Lcm"
  6.1021 +    by (auto intro!: ext Lcm_eqI)
  6.1022 +  show "(Euclidean_Algorithm.lcm :: int \<Rightarrow> _) = lcm"
  6.1023 +    by (simp add: fun_eq_iff Euclidean_Algorithm.lcm_def semiring_gcd_class.lcm_gcd)
  6.1024 +  show "(Euclidean_Algorithm.Gcd :: int set \<Rightarrow> _) = Gcd"
  6.1025 +    by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm)
  6.1026  qed
  6.1027  
  6.1028  end