src/HOL/Number_Theory/Euclidean_Algorithm.thy
changeset 62422 4aa35fd6c152
parent 62353 7f927120b5a2
child 62425 d0936b500bf5
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Feb 25 13:58:48 2016 +0000
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Feb 25 16:44:53 2016 +0100
     1.3 @@ -19,6 +19,7 @@
     1.4  \<close> 
     1.5  class euclidean_semiring = semiring_div + normalization_semidom + 
     1.6    fixes euclidean_size :: "'a \<Rightarrow> nat"
     1.7 +  assumes size_0 [simp]: "euclidean_size 0 = 0"
     1.8    assumes mod_size_less: 
     1.9      "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
    1.10    assumes size_mult_mono:
    1.11 @@ -110,6 +111,122 @@
    1.12    "b \<noteq> 0 \<Longrightarrow> gcd_eucl a b = gcd_eucl b (a mod b)"
    1.13    by (simp add: gcd_eucl.simps [of a b] gcd_eucl.simps [of b 0])
    1.14  
    1.15 +lemma gcd_eucl_dvd1 [iff]: "gcd_eucl a b dvd a"
    1.16 +  and gcd_eucl_dvd2 [iff]: "gcd_eucl a b dvd b"
    1.17 +  by (induct a b rule: gcd_eucl_induct)
    1.18 +     (simp_all add: gcd_eucl_0 gcd_eucl_non_0 dvd_mod_iff)
    1.19 +
    1.20 +lemma normalize_gcd_eucl [simp]:
    1.21 +  "normalize (gcd_eucl a b) = gcd_eucl a b"
    1.22 +  by (induct a b rule: gcd_eucl_induct) (simp_all add: gcd_eucl_0 gcd_eucl_non_0)
    1.23 +     
    1.24 +lemma gcd_eucl_greatest:
    1.25 +  fixes k a b :: 'a
    1.26 +  shows "k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd gcd_eucl a b"
    1.27 +proof (induct a b rule: gcd_eucl_induct)
    1.28 +  case (zero a) from zero(1) show ?case by (rule dvd_trans) (simp add: gcd_eucl_0)
    1.29 +next
    1.30 +  case (mod a b)
    1.31 +  then show ?case
    1.32 +    by (simp add: gcd_eucl_non_0 dvd_mod_iff)
    1.33 +qed
    1.34 +
    1.35 +lemma eq_gcd_euclI:
    1.36 +  fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.37 +  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"
    1.38 +          "\<And>a b k. k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd gcd a b"
    1.39 +  shows   "gcd = gcd_eucl"
    1.40 +  by (intro ext, rule associated_eqI) (simp_all add: gcd_eucl_greatest assms)
    1.41 +
    1.42 +lemma gcd_eucl_zero [simp]:
    1.43 +  "gcd_eucl a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
    1.44 +  by (metis dvd_0_left dvd_refl gcd_eucl_dvd1 gcd_eucl_dvd2 gcd_eucl_greatest)+
    1.45 +
    1.46 +  
    1.47 +lemma dvd_Lcm_eucl [simp]: "a \<in> A \<Longrightarrow> a dvd Lcm_eucl A"
    1.48 +  and Lcm_eucl_least: "(\<And>a. a \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> Lcm_eucl A dvd b"
    1.49 +  and unit_factor_Lcm_eucl [simp]: 
    1.50 +          "unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)"
    1.51 +proof -
    1.52 +  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>
    1.53 +    unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)" (is ?thesis)
    1.54 +  proof (cases "\<exists>l. l \<noteq>  0 \<and> (\<forall>a\<in>A. a dvd l)")
    1.55 +    case False
    1.56 +    hence "Lcm_eucl A = 0" by (auto simp: Lcm_eucl_def)
    1.57 +    with False show ?thesis by auto
    1.58 +  next
    1.59 +    case True
    1.60 +    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
    1.61 +    def n \<equiv> "LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
    1.62 +    def l \<equiv> "SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
    1.63 +    have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
    1.64 +      apply (subst n_def)
    1.65 +      apply (rule LeastI[of _ "euclidean_size l\<^sub>0"])
    1.66 +      apply (rule exI[of _ l\<^sub>0])
    1.67 +      apply (simp add: l\<^sub>0_props)
    1.68 +      done
    1.69 +    from someI_ex[OF this] have "l \<noteq> 0" and "\<forall>a\<in>A. a dvd l" and "euclidean_size l = n" 
    1.70 +      unfolding l_def by simp_all
    1.71 +    {
    1.72 +      fix l' assume "\<forall>a\<in>A. a dvd l'"
    1.73 +      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)
    1.74 +      moreover from \<open>l \<noteq> 0\<close> have "gcd_eucl l l' \<noteq> 0" by simp
    1.75 +      ultimately have "\<exists>b. b \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd b) \<and> 
    1.76 +                          euclidean_size b = euclidean_size (gcd_eucl l l')"
    1.77 +        by (intro exI[of _ "gcd_eucl l l'"], auto)
    1.78 +      hence "euclidean_size (gcd_eucl l l') \<ge> n" by (subst n_def) (rule Least_le)
    1.79 +      moreover have "euclidean_size (gcd_eucl l l') \<le> n"
    1.80 +      proof -
    1.81 +        have "gcd_eucl l l' dvd l" by simp
    1.82 +        then obtain a where "l = gcd_eucl l l' * a" unfolding dvd_def by blast
    1.83 +        with \<open>l \<noteq> 0\<close> have "a \<noteq> 0" by auto
    1.84 +        hence "euclidean_size (gcd_eucl l l') \<le> euclidean_size (gcd_eucl l l' * a)"
    1.85 +          by (rule size_mult_mono)
    1.86 +        also have "gcd_eucl l l' * a = l" using \<open>l = gcd_eucl l l' * a\<close> ..
    1.87 +        also note \<open>euclidean_size l = n\<close>
    1.88 +        finally show "euclidean_size (gcd_eucl l l') \<le> n" .
    1.89 +      qed
    1.90 +      ultimately have *: "euclidean_size l = euclidean_size (gcd_eucl l l')" 
    1.91 +        by (intro le_antisym, simp_all add: \<open>euclidean_size l = n\<close>)
    1.92 +      from \<open>l \<noteq> 0\<close> have "l dvd gcd_eucl l l'"
    1.93 +        by (rule dvd_euclidean_size_eq_imp_dvd) (auto simp add: *)
    1.94 +      hence "l dvd l'" by (rule dvd_trans[OF _ gcd_eucl_dvd2])
    1.95 +    }
    1.96 +
    1.97 +    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>
    1.98 +      have "(\<forall>a\<in>A. a dvd normalize l) \<and> 
    1.99 +        (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> normalize l dvd l') \<and>
   1.100 +        unit_factor (normalize l) = 
   1.101 +        (if normalize l = 0 then 0 else 1)"
   1.102 +      by (auto simp: unit_simps)
   1.103 +    also from True have "normalize l = Lcm_eucl A"
   1.104 +      by (simp add: Lcm_eucl_def Let_def n_def l_def)
   1.105 +    finally show ?thesis .
   1.106 +  qed
   1.107 +  note A = this
   1.108 +
   1.109 +  {fix a assume "a \<in> A" then show "a dvd Lcm_eucl A" using A by blast}
   1.110 +  {fix b assume "\<And>a. a \<in> A \<Longrightarrow> a dvd b" then show "Lcm_eucl A dvd b" using A by blast}
   1.111 +  from A show "unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)" by blast
   1.112 +qed
   1.113 +  
   1.114 +lemma normalize_Lcm_eucl [simp]:
   1.115 +  "normalize (Lcm_eucl A) = Lcm_eucl A"
   1.116 +proof (cases "Lcm_eucl A = 0")
   1.117 +  case True then show ?thesis by simp
   1.118 +next
   1.119 +  case False
   1.120 +  have "unit_factor (Lcm_eucl A) * normalize (Lcm_eucl A) = Lcm_eucl A"
   1.121 +    by (fact unit_factor_mult_normalize)
   1.122 +  with False show ?thesis by simp
   1.123 +qed
   1.124 +
   1.125 +lemma eq_Lcm_euclI:
   1.126 +  fixes lcm :: "'a set \<Rightarrow> 'a"
   1.127 +  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"
   1.128 +          "\<And>A. normalize (lcm A) = lcm A" shows "lcm = Lcm_eucl"
   1.129 +  by (intro ext, rule associated_eqI) (auto simp: assms intro: Lcm_eucl_least)  
   1.130 +
   1.131  end
   1.132  
   1.133  class euclidean_ring = euclidean_semiring + idom
   1.134 @@ -184,86 +301,28 @@
   1.135    assumes Gcd_Gcd_eucl: "Gcd = Gcd_eucl" and Lcm_Lcm_eucl: "Lcm = Lcm_eucl"
   1.136  begin
   1.137  
   1.138 -lemma gcd_0_left:
   1.139 -  "gcd 0 a = normalize a"
   1.140 -  unfolding gcd_gcd_eucl by (fact gcd_eucl_0_left)
   1.141 +subclass semiring_gcd
   1.142 +  by standard (simp_all add: gcd_gcd_eucl gcd_eucl_greatest lcm_lcm_eucl lcm_eucl_def)
   1.143  
   1.144 -lemma gcd_0:
   1.145 -  "gcd a 0 = normalize a"
   1.146 -  unfolding gcd_gcd_eucl by (fact gcd_eucl_0)
   1.147 +subclass semiring_Gcd
   1.148 +  by standard (auto simp: Gcd_Gcd_eucl Lcm_Lcm_eucl Gcd_eucl_def intro: Lcm_eucl_least)
   1.149 +  
   1.150  
   1.151  lemma gcd_non_0:
   1.152    "b \<noteq> 0 \<Longrightarrow> gcd a b = gcd b (a mod b)"
   1.153    unfolding gcd_gcd_eucl by (fact gcd_eucl_non_0)
   1.154  
   1.155 -lemma gcd_dvd1 [iff]: "gcd a b dvd a"
   1.156 -  and gcd_dvd2 [iff]: "gcd a b dvd b"
   1.157 -  by (induct a b rule: gcd_eucl_induct)
   1.158 -    (simp_all add: gcd_0 gcd_non_0 dvd_mod_iff)
   1.159 -    
   1.160 -lemma dvd_gcd_D1: "k dvd gcd m n \<Longrightarrow> k dvd m"
   1.161 -  by (rule dvd_trans, assumption, rule gcd_dvd1)
   1.162 -
   1.163 -lemma dvd_gcd_D2: "k dvd gcd m n \<Longrightarrow> k dvd n"
   1.164 -  by (rule dvd_trans, assumption, rule gcd_dvd2)
   1.165 -
   1.166 -lemma gcd_greatest:
   1.167 -  fixes k a b :: 'a
   1.168 -  shows "k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd gcd a b"
   1.169 -proof (induct a b rule: gcd_eucl_induct)
   1.170 -  case (zero a) from zero(1) show ?case by (rule dvd_trans) (simp add: gcd_0)
   1.171 -next
   1.172 -  case (mod a b)
   1.173 -  then show ?case
   1.174 -    by (simp add: gcd_non_0 dvd_mod_iff)
   1.175 -qed
   1.176 -
   1.177 -lemma dvd_gcd_iff:
   1.178 -  "k dvd gcd a b \<longleftrightarrow> k dvd a \<and> k dvd b"
   1.179 -  by (blast intro!: gcd_greatest intro: dvd_trans)
   1.180 +lemmas gcd_0 = gcd_0_right
   1.181 +lemmas dvd_gcd_iff = gcd_greatest_iff
   1.182  
   1.183  lemmas gcd_greatest_iff = dvd_gcd_iff
   1.184  
   1.185 -lemma gcd_zero [simp]:
   1.186 -  "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
   1.187 -  by (metis dvd_0_left dvd_refl gcd_dvd1 gcd_dvd2 gcd_greatest)+
   1.188 -
   1.189 -lemma normalize_gcd [simp]:
   1.190 -  "normalize (gcd a b) = gcd a b"
   1.191 -  by (induct a b rule: gcd_eucl_induct) (simp_all add: gcd_0 gcd_non_0)
   1.192 -
   1.193  lemma gcdI:
   1.194    assumes "c dvd a" and "c dvd b" and greatest: "\<And>d. d dvd a \<Longrightarrow> d dvd b \<Longrightarrow> d dvd c"
   1.195      and "normalize c = c"
   1.196    shows "c = gcd a b"
   1.197    by (rule associated_eqI) (auto simp: assms intro: gcd_greatest)
   1.198  
   1.199 -sublocale gcd: abel_semigroup gcd
   1.200 -proof
   1.201 -  fix a b c 
   1.202 -  show "gcd (gcd a b) c = gcd a (gcd b c)"
   1.203 -  proof (rule gcdI)
   1.204 -    have "gcd (gcd a b) c dvd gcd a b" "gcd a b dvd a" by simp_all
   1.205 -    then show "gcd (gcd a b) c dvd a" by (rule dvd_trans)
   1.206 -    have "gcd (gcd a b) c dvd gcd a b" "gcd a b dvd b" by simp_all
   1.207 -    hence "gcd (gcd a b) c dvd b" by (rule dvd_trans)
   1.208 -    moreover have "gcd (gcd a b) c dvd c" by simp
   1.209 -    ultimately show "gcd (gcd a b) c dvd gcd b c"
   1.210 -      by (rule gcd_greatest)
   1.211 -    show "normalize (gcd (gcd a b) c) = gcd (gcd a b) c"
   1.212 -      by auto
   1.213 -    fix l assume "l dvd a" and "l dvd gcd b c"
   1.214 -    with dvd_trans [OF _ gcd_dvd1] and dvd_trans [OF _ gcd_dvd2]
   1.215 -      have "l dvd b" and "l dvd c" by blast+
   1.216 -    with \<open>l dvd a\<close> show "l dvd gcd (gcd a b) c"
   1.217 -      by (intro gcd_greatest)
   1.218 -  qed
   1.219 -next
   1.220 -  fix a b
   1.221 -  show "gcd a b = gcd b a"
   1.222 -    by (rule gcdI) (simp_all add: gcd_greatest)
   1.223 -qed
   1.224 -
   1.225  lemma gcd_unique: "d dvd a \<and> d dvd b \<and> 
   1.226      normalize d = d \<and>
   1.227      (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   1.228 @@ -272,15 +331,9 @@
   1.229  lemma gcd_dvd_prod: "gcd a b dvd k * b"
   1.230    using mult_dvd_mono [of 1] by auto
   1.231  
   1.232 -lemma gcd_1_left [simp]: "gcd 1 a = 1"
   1.233 -  by (rule sym, rule gcdI, simp_all)
   1.234 -
   1.235 -lemma gcd_1 [simp]: "gcd a 1 = 1"
   1.236 -  by (rule sym, rule gcdI, simp_all)
   1.237 -
   1.238  lemma gcd_proj2_if_dvd: 
   1.239    "b dvd a \<Longrightarrow> gcd a b = normalize b"
   1.240 -  by (cases "b = 0", simp_all add: dvd_eq_mod_eq_0 gcd_non_0 gcd_0)
   1.241 +  by (cases "b = 0", simp_all add: dvd_eq_mod_eq_0 gcd_non_0)
   1.242  
   1.243  lemma gcd_proj1_if_dvd: 
   1.244    "a dvd b \<Longrightarrow> gcd a b = normalize a"
   1.245 @@ -315,17 +368,17 @@
   1.246  lemma gcd_mult_distrib': 
   1.247    "normalize c * gcd a b = gcd (c * a) (c * b)"
   1.248  proof (cases "c = 0")
   1.249 -  case True then show ?thesis by (simp_all add: gcd_0)
   1.250 +  case True then show ?thesis by simp_all
   1.251  next
   1.252    case False then have [simp]: "is_unit (unit_factor c)" by simp
   1.253    show ?thesis
   1.254    proof (induct a b rule: gcd_eucl_induct)
   1.255      case (zero a) show ?case
   1.256      proof (cases "a = 0")
   1.257 -      case True then show ?thesis by (simp add: gcd_0)
   1.258 +      case True then show ?thesis by simp
   1.259      next
   1.260        case False
   1.261 -      then show ?thesis by (simp add: gcd_0 normalize_mult)
   1.262 +      then show ?thesis by (simp add: normalize_mult)
   1.263      qed
   1.264      case (mod a b)
   1.265      then show ?case by (simp add: mult_mod_right gcd.commute)
   1.266 @@ -363,10 +416,11 @@
   1.267    shows "euclidean_size (gcd a b) < euclidean_size a"
   1.268  proof (rule ccontr)
   1.269    assume "\<not>euclidean_size (gcd a b) < euclidean_size a"
   1.270 -  with \<open>a \<noteq> 0\<close> have "euclidean_size (gcd a b) = euclidean_size a"
   1.271 +  with \<open>a \<noteq> 0\<close> have A: "euclidean_size (gcd a b) = euclidean_size a"
   1.272      by (intro le_antisym, simp_all)
   1.273 -  with assms have "a dvd gcd a b" by (auto intro: dvd_euclidean_size_eq_imp_dvd)
   1.274 -  hence "a dvd b" using dvd_gcd_D2 by blast
   1.275 +  have "a dvd gcd a b"
   1.276 +    by (rule dvd_euclidean_size_eq_imp_dvd) (simp_all add: assms A)
   1.277 +  hence "a dvd b" using dvd_gcdD2 by blast
   1.278    with \<open>\<not>a dvd b\<close> show False by contradiction
   1.279  qed
   1.280  
   1.281 @@ -379,7 +433,6 @@
   1.282    apply (rule gcdI)
   1.283    apply simp_all
   1.284    apply (rule dvd_trans, rule gcd_dvd1, simp add: unit_simps)
   1.285 -  apply (rule gcd_greatest, simp add: unit_simps, assumption)
   1.286    done
   1.287  
   1.288  lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c"
   1.289 @@ -410,7 +463,7 @@
   1.290    using normalize_gcd_left [of b a] by (simp add: ac_simps)
   1.291  
   1.292  lemma gcd_idem: "gcd a a = normalize a"
   1.293 -  by (cases "a = 0") (simp add: gcd_0_left, rule sym, rule gcdI, simp_all)
   1.294 +  by (cases "a = 0") (simp, rule sym, rule gcdI, simp_all)
   1.295  
   1.296  lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b"
   1.297    apply (rule gcdI)
   1.298 @@ -437,20 +490,6 @@
   1.299      by (simp add: fun_eq_iff gcd_left_idem)
   1.300  qed
   1.301  
   1.302 -lemma coprime_dvd_mult:
   1.303 -  assumes "gcd c b = 1" and "c dvd a * b"
   1.304 -  shows "c dvd a"
   1.305 -proof -
   1.306 -  let ?nf = "unit_factor"
   1.307 -  from assms gcd_mult_distrib [of a c b] 
   1.308 -    have A: "a = gcd (a * c) (a * b) * ?nf a" by simp
   1.309 -  from \<open>c dvd a * b\<close> show ?thesis by (subst A, simp_all add: gcd_greatest)
   1.310 -qed
   1.311 -
   1.312 -lemma coprime_dvd_mult_iff:
   1.313 -  "gcd c b = 1 \<Longrightarrow> (c dvd a * b) = (c dvd a)"
   1.314 -  by (rule, rule coprime_dvd_mult, simp_all)
   1.315 -
   1.316  lemma gcd_dvd_antisym:
   1.317    "gcd a b dvd gcd c d \<Longrightarrow> gcd c d dvd gcd a b \<Longrightarrow> gcd a b = gcd c d"
   1.318  proof (rule gcdI)
   1.319 @@ -466,20 +505,6 @@
   1.320    from this and B show "l dvd gcd a b" by (rule dvd_trans)
   1.321  qed
   1.322  
   1.323 -lemma gcd_mult_cancel:
   1.324 -  assumes "gcd k n = 1"
   1.325 -  shows "gcd (k * m) n = gcd m n"
   1.326 -proof (rule gcd_dvd_antisym)
   1.327 -  have "gcd (gcd (k * m) n) k = gcd (gcd k n) (k * m)" by (simp add: ac_simps)
   1.328 -  also note \<open>gcd k n = 1\<close>
   1.329 -  finally have "gcd (gcd (k * m) n) k = 1" by simp
   1.330 -  hence "gcd (k * m) n dvd m" by (rule coprime_dvd_mult, simp add: ac_simps)
   1.331 -  moreover have "gcd (k * m) n dvd n" by simp
   1.332 -  ultimately show "gcd (k * m) n dvd gcd m n" by (rule gcd_greatest)
   1.333 -  have "gcd m n dvd (k * m)" and "gcd m n dvd n" by simp_all
   1.334 -  then show "gcd m n dvd gcd (k * m) n" by (rule gcd_greatest)
   1.335 -qed
   1.336 -
   1.337  lemma coprime_crossproduct:
   1.338    assumes [simp]: "gcd a d = 1" "gcd b c = 1"
   1.339    shows "normalize (a * c) = normalize (b * d) \<longleftrightarrow> normalize a  = normalize b \<and> normalize c = normalize d"
   1.340 @@ -525,7 +550,7 @@
   1.341    by (rule sym, rule gcdI, simp_all)
   1.342  
   1.343  lemma coprime: "gcd a b = 1 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)"
   1.344 -  by (auto intro: coprimeI gcd_greatest dvd_gcd_D1 dvd_gcd_D2)
   1.345 +  by (auto intro: coprimeI gcd_greatest dvd_gcdD1 dvd_gcdD2)
   1.346  
   1.347  lemma div_gcd_coprime:
   1.348    assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
   1.349 @@ -549,15 +574,6 @@
   1.350    then show "l dvd 1" ..
   1.351  qed
   1.352  
   1.353 -lemma coprime_mult: 
   1.354 -  assumes da: "gcd d a = 1" and db: "gcd d b = 1"
   1.355 -  shows "gcd d (a * b) = 1"
   1.356 -  apply (subst gcd.commute)
   1.357 -  using da apply (subst gcd_mult_cancel)
   1.358 -  apply (subst gcd.commute, assumption)
   1.359 -  apply (subst gcd.commute, rule db)
   1.360 -  done
   1.361 -
   1.362  lemma coprime_lmult:
   1.363    assumes dab: "gcd d (a * b) = 1" 
   1.364    shows "gcd d a = 1"
   1.365 @@ -610,25 +626,6 @@
   1.366    "gcd d a = 1 \<Longrightarrow> gcd d (a^n) = 1"
   1.367    by (induct n, simp_all add: coprime_mult)
   1.368  
   1.369 -lemma coprime_exp2 [intro]:
   1.370 -  "gcd a b = 1 \<Longrightarrow> gcd (a^n) (b^m) = 1"
   1.371 -  apply (rule coprime_exp)
   1.372 -  apply (subst gcd.commute)
   1.373 -  apply (rule coprime_exp)
   1.374 -  apply (subst gcd.commute)
   1.375 -  apply assumption
   1.376 -  done
   1.377 -
   1.378 -lemma lcm_gcd:
   1.379 -  "lcm a b = normalize (a * b) div gcd a b"
   1.380 -  by (simp add: lcm_lcm_eucl gcd_gcd_eucl lcm_eucl_def)
   1.381 -
   1.382 -subclass semiring_gcd
   1.383 -  apply standard
   1.384 -  using gcd_right_idem
   1.385 -  apply (simp_all add: lcm_gcd gcd_greatest_iff gcd_proj1_if_dvd)
   1.386 -  done
   1.387 -
   1.388  lemma gcd_exp:
   1.389    "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
   1.390  proof (cases "a = 0 \<and> b = 0")
   1.391 @@ -637,7 +634,7 @@
   1.392  next
   1.393    case False
   1.394    then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
   1.395 -    using div_gcd_coprime by (subst sym) (auto simp: div_gcd_coprime)
   1.396 +    using coprime_exp2[OF div_gcd_coprime[of a b], of n n, symmetric] by simp
   1.397    then have "gcd a b ^ n = gcd a b ^ n * ..." by simp
   1.398    also note gcd_mult_distrib
   1.399    also have "unit_factor (gcd a b ^ n) = 1"
   1.400 @@ -712,18 +709,7 @@
   1.401    "n \<noteq> 0 \<Longrightarrow> a ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
   1.402    by (auto intro: pow_divs_pow dvd_power_same)
   1.403  
   1.404 -lemma divs_mult:
   1.405 -  assumes mr: "m dvd r" and nr: "n dvd r" and mn: "gcd m n = 1"
   1.406 -  shows "m * n dvd r"
   1.407 -proof -
   1.408 -  from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   1.409 -    unfolding dvd_def by blast
   1.410 -  from mr n' have "m dvd n'*n" by (simp add: ac_simps)
   1.411 -  hence "m dvd n'" using coprime_dvd_mult_iff[OF mn] by simp
   1.412 -  then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   1.413 -  with n' have "r = m * n * k" by (simp add: mult_ac)
   1.414 -  then show ?thesis unfolding dvd_def by blast
   1.415 -qed
   1.416 +lemmas divs_mult = divides_mult
   1.417  
   1.418  lemma coprime_plus_one [simp]: "gcd (n + 1) n = 1"
   1.419    by (subst add_commute, simp)
   1.420 @@ -734,6 +720,10 @@
   1.421    apply (induct set: finite)
   1.422    apply (auto simp add: gcd_mult_cancel)
   1.423    done
   1.424 +  
   1.425 +lemma listprod_coprime:
   1.426 +  "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (listprod xs) y" 
   1.427 +  by (induction xs) (simp_all add: gcd_mult_cancel)
   1.428  
   1.429  lemma coprime_divisors: 
   1.430    assumes "d dvd a" "e dvd b" "gcd a b = 1"
   1.431 @@ -790,39 +780,11 @@
   1.432    shows "c = lcm a b"
   1.433    by (rule associated_eqI) (auto simp: assms intro: lcm_least)
   1.434  
   1.435 -sublocale lcm: abel_semigroup lcm ..
   1.436 -
   1.437 -lemma dvd_lcm_D1:
   1.438 -  "lcm m n dvd k \<Longrightarrow> m dvd k"
   1.439 -  by (rule dvd_trans, rule dvd_lcm1, assumption)
   1.440 -
   1.441 -lemma dvd_lcm_D2:
   1.442 -  "lcm m n dvd k \<Longrightarrow> n dvd k"
   1.443 -  by (rule dvd_trans, rule dvd_lcm2, assumption)
   1.444 -
   1.445  lemma gcd_dvd_lcm [simp]:
   1.446    "gcd a b dvd lcm a b"
   1.447    using gcd_dvd2 by (rule dvd_lcmI2)
   1.448  
   1.449 -lemma lcm_1_iff:
   1.450 -  "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b"
   1.451 -proof
   1.452 -  assume "lcm a b = 1"
   1.453 -  then show "is_unit a \<and> is_unit b" by auto
   1.454 -next
   1.455 -  assume "is_unit a \<and> is_unit b"
   1.456 -  hence "a dvd 1" and "b dvd 1" by simp_all
   1.457 -  hence "is_unit (lcm a b)" by (rule lcm_least)
   1.458 -  hence "lcm a b = unit_factor (lcm a b)"
   1.459 -    by (blast intro: sym is_unit_unit_factor)
   1.460 -  also have "\<dots> = 1" using \<open>is_unit a \<and> is_unit b\<close>
   1.461 -    by auto
   1.462 -  finally show "lcm a b = 1" .
   1.463 -qed
   1.464 -
   1.465 -lemma lcm_0:
   1.466 -  "lcm a 0 = 0"
   1.467 -  by (fact lcm_0_right)
   1.468 +lemmas lcm_0 = lcm_0_right
   1.469  
   1.470  lemma lcm_unique:
   1.471    "a dvd d \<and> b dvd d \<and> 
   1.472 @@ -886,7 +848,7 @@
   1.473      by (intro le_antisym, simp, intro euclidean_size_lcm_le1)
   1.474    with assms have "lcm a b dvd a" 
   1.475      by (rule_tac dvd_euclidean_size_eq_imp_dvd) (auto simp: lcm_zero)
   1.476 -  hence "b dvd a" by (rule dvd_lcm_D2)
   1.477 +  hence "b dvd a" by (rule lcm_dvdD2)
   1.478    with \<open>\<not>b dvd a\<close> show False by contradiction
   1.479  qed
   1.480  
   1.481 @@ -929,104 +891,10 @@
   1.482    "lcm a (normalize b) = lcm a b"
   1.483    using normalize_lcm_left [of b a] by (simp add: ac_simps)
   1.484  
   1.485 -lemma lcm_left_idem:
   1.486 -  "lcm a (lcm a b) = lcm a b"
   1.487 -  by (rule associated_eqI) simp_all
   1.488 -
   1.489 -lemma lcm_right_idem:
   1.490 -  "lcm (lcm a b) b = lcm a b"
   1.491 -  by (rule associated_eqI) simp_all
   1.492 -
   1.493 -lemma comp_fun_idem_lcm: "comp_fun_idem lcm"
   1.494 -proof
   1.495 -  fix a b show "lcm a \<circ> lcm b = lcm b \<circ> lcm a"
   1.496 -    by (simp add: fun_eq_iff ac_simps)
   1.497 -next
   1.498 -  fix a show "lcm a \<circ> lcm a = lcm a" unfolding o_def
   1.499 -    by (intro ext, simp add: lcm_left_idem)
   1.500 -qed
   1.501 -
   1.502 -lemma dvd_Lcm [simp]: "a \<in> A \<Longrightarrow> a dvd Lcm A"
   1.503 -  and Lcm_least: "(\<And>a. a \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> Lcm A dvd b"
   1.504 -  and unit_factor_Lcm [simp]: 
   1.505 -          "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
   1.506 -proof -
   1.507 -  have "(\<forall>a\<in>A. a dvd Lcm A) \<and> (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> Lcm A dvd l') \<and>
   1.508 -    unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" (is ?thesis)
   1.509 -  proof (cases "\<exists>l. l \<noteq>  0 \<and> (\<forall>a\<in>A. a dvd l)")
   1.510 -    case False
   1.511 -    hence "Lcm A = 0" by (auto simp: Lcm_Lcm_eucl Lcm_eucl_def)
   1.512 -    with False show ?thesis by auto
   1.513 -  next
   1.514 -    case True
   1.515 -    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
   1.516 -    def n \<equiv> "LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
   1.517 -    def l \<equiv> "SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
   1.518 -    have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
   1.519 -      apply (subst n_def)
   1.520 -      apply (rule LeastI[of _ "euclidean_size l\<^sub>0"])
   1.521 -      apply (rule exI[of _ l\<^sub>0])
   1.522 -      apply (simp add: l\<^sub>0_props)
   1.523 -      done
   1.524 -    from someI_ex[OF this] have "l \<noteq> 0" and "\<forall>a\<in>A. a dvd l" and "euclidean_size l = n" 
   1.525 -      unfolding l_def by simp_all
   1.526 -    {
   1.527 -      fix l' assume "\<forall>a\<in>A. a dvd l'"
   1.528 -      with \<open>\<forall>a\<in>A. a dvd l\<close> have "\<forall>a\<in>A. a dvd gcd l l'" by (auto intro: gcd_greatest)
   1.529 -      moreover from \<open>l \<noteq> 0\<close> have "gcd l l' \<noteq> 0" by simp
   1.530 -      ultimately have "\<exists>b. b \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd b) \<and> euclidean_size b = euclidean_size (gcd l l')"
   1.531 -        by (intro exI[of _ "gcd l l'"], auto)
   1.532 -      hence "euclidean_size (gcd l l') \<ge> n" by (subst n_def) (rule Least_le)
   1.533 -      moreover have "euclidean_size (gcd l l') \<le> n"
   1.534 -      proof -
   1.535 -        have "gcd l l' dvd l" by simp
   1.536 -        then obtain a where "l = gcd l l' * a" unfolding dvd_def by blast
   1.537 -        with \<open>l \<noteq> 0\<close> have "a \<noteq> 0" by auto
   1.538 -        hence "euclidean_size (gcd l l') \<le> euclidean_size (gcd l l' * a)"
   1.539 -          by (rule size_mult_mono)
   1.540 -        also have "gcd l l' * a = l" using \<open>l = gcd l l' * a\<close> ..
   1.541 -        also note \<open>euclidean_size l = n\<close>
   1.542 -        finally show "euclidean_size (gcd l l') \<le> n" .
   1.543 -      qed
   1.544 -      ultimately have *: "euclidean_size l = euclidean_size (gcd l l')" 
   1.545 -        by (intro le_antisym, simp_all add: \<open>euclidean_size l = n\<close>)
   1.546 -      from \<open>l \<noteq> 0\<close> have "l dvd gcd l l'"
   1.547 -        by (rule dvd_euclidean_size_eq_imp_dvd) (auto simp add: *)
   1.548 -      hence "l dvd l'" by (blast dest: dvd_gcd_D2)
   1.549 -    }
   1.550 -
   1.551 -    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>
   1.552 -      have "(\<forall>a\<in>A. a dvd normalize l) \<and> 
   1.553 -        (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> normalize l dvd l') \<and>
   1.554 -        unit_factor (normalize l) = 
   1.555 -        (if normalize l = 0 then 0 else 1)"
   1.556 -      by (auto simp: unit_simps)
   1.557 -    also from True have "normalize l = Lcm A"
   1.558 -      by (simp add: Lcm_Lcm_eucl Lcm_eucl_def Let_def n_def l_def)
   1.559 -    finally show ?thesis .
   1.560 -  qed
   1.561 -  note A = this
   1.562 -
   1.563 -  {fix a assume "a \<in> A" then show "a dvd Lcm A" using A by blast}
   1.564 -  {fix b assume "\<And>a. a \<in> A \<Longrightarrow> a dvd b" then show "Lcm A dvd b" using A by blast}
   1.565 -  from A show "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" by blast
   1.566 -qed
   1.567 -
   1.568 -lemma normalize_Lcm [simp]:
   1.569 -  "normalize (Lcm A) = Lcm A"
   1.570 -proof (cases "Lcm A = 0")
   1.571 -  case True then show ?thesis by simp
   1.572 -next
   1.573 -  case False
   1.574 -  have "unit_factor (Lcm A) * normalize (Lcm A) = Lcm A"
   1.575 -    by (fact unit_factor_mult_normalize)
   1.576 -  with False show ?thesis by simp
   1.577 -qed
   1.578 -
   1.579  lemma LcmI:
   1.580    assumes "\<And>a. a \<in> A \<Longrightarrow> a dvd b" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> b dvd c"
   1.581      and "normalize b = b" shows "b = Lcm A"
   1.582 -  by (rule associated_eqI) (auto simp: assms intro: Lcm_least)
   1.583 +  by (rule associated_eqI) (auto simp: assms dvd_Lcm intro: Lcm_least)
   1.584  
   1.585  lemma Lcm_subset:
   1.586    "A \<subseteq> B \<Longrightarrow> Lcm A dvd Lcm B"
   1.587 @@ -1043,13 +911,6 @@
   1.588    apply simp
   1.589    done
   1.590  
   1.591 -lemma Lcm_1_iff:
   1.592 -  "Lcm A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a)"
   1.593 -proof
   1.594 -  assume "Lcm A = 1"
   1.595 -  then show "\<forall>a\<in>A. is_unit a" by auto
   1.596 -qed (rule LcmI [symmetric], auto)
   1.597 -
   1.598  lemma Lcm_no_units:
   1.599    "Lcm A = Lcm (A - {a. is_unit a})"
   1.600  proof -
   1.601 @@ -1060,14 +921,6 @@
   1.602    finally show ?thesis by simp
   1.603  qed
   1.604  
   1.605 -lemma Lcm_empty [simp]:
   1.606 -  "Lcm {} = 1"
   1.607 -  by (simp add: Lcm_1_iff)
   1.608 -
   1.609 -lemma Lcm_eq_0_I [simp]:
   1.610 -  "0 \<in> A \<Longrightarrow> Lcm A = 0"
   1.611 -  by (drule dvd_Lcm) simp
   1.612 -
   1.613  lemma Lcm_0_iff':
   1.614    "Lcm A = 0 \<longleftrightarrow> \<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))"
   1.615  proof
   1.616 @@ -1092,27 +945,6 @@
   1.617    qed
   1.618  qed (simp only: Lcm_Lcm_eucl Lcm_eucl_def if_False)
   1.619  
   1.620 -lemma Lcm_0_iff [simp]:
   1.621 -  "finite A \<Longrightarrow> Lcm A = 0 \<longleftrightarrow> 0 \<in> A"
   1.622 -proof -
   1.623 -  assume "finite A"
   1.624 -  have "0 \<in> A \<Longrightarrow> Lcm A = 0"  by (intro dvd_0_left dvd_Lcm)
   1.625 -  moreover {
   1.626 -    assume "0 \<notin> A"
   1.627 -    hence "\<Prod>A \<noteq> 0" 
   1.628 -      apply (induct rule: finite_induct[OF \<open>finite A\<close>]) 
   1.629 -      apply simp
   1.630 -      apply (subst setprod.insert, assumption, assumption)
   1.631 -      apply (rule no_zero_divisors)
   1.632 -      apply blast+
   1.633 -      done
   1.634 -    moreover from \<open>finite A\<close> have "\<forall>a\<in>A. a dvd \<Prod>A" by blast
   1.635 -    ultimately have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l)" by blast
   1.636 -    with Lcm_0_iff' have "Lcm A \<noteq> 0" by simp
   1.637 -  }
   1.638 -  ultimately show "Lcm A = 0 \<longleftrightarrow> 0 \<in> A" by blast
   1.639 -qed
   1.640 -
   1.641  lemma Lcm_no_multiple:
   1.642    "(\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not>a dvd m)) \<Longrightarrow> Lcm A = 0"
   1.643  proof -
   1.644 @@ -1121,14 +953,6 @@
   1.645    then show "Lcm A = 0" by (simp only: Lcm_Lcm_eucl Lcm_eucl_def if_False)
   1.646  qed
   1.647  
   1.648 -lemma Lcm_insert [simp]:
   1.649 -  "Lcm (insert a A) = lcm a (Lcm A)"
   1.650 -proof (rule lcmI)
   1.651 -  fix l assume "a dvd l" and "Lcm A dvd l"
   1.652 -  then have "\<forall>a\<in>A. a dvd l" by (auto intro: dvd_trans [of _ "Lcm A" l])
   1.653 -  with \<open>a dvd l\<close> show "Lcm (insert a A) dvd l" by (force intro: Lcm_least)
   1.654 -qed (auto intro: Lcm_least dvd_Lcm)
   1.655 - 
   1.656  lemma Lcm_finite:
   1.657    assumes "finite A"
   1.658    shows "Lcm A = Finite_Set.fold lcm 1 A"
   1.659 @@ -1167,50 +991,17 @@
   1.660      \<Longrightarrow> Lcm A = normalize (\<Prod>A)"
   1.661    by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
   1.662  
   1.663 -lemma Gcd_Lcm:
   1.664 -  "Gcd A = Lcm {d. \<forall>a\<in>A. d dvd a}"
   1.665 -  by (simp add: Gcd_Gcd_eucl Lcm_Lcm_eucl Gcd_eucl_def)
   1.666 -
   1.667 -lemma Gcd_dvd [simp]: "a \<in> A \<Longrightarrow> Gcd A dvd a"
   1.668 -  and Gcd_greatest: "(\<And>a. a \<in> A \<Longrightarrow> b dvd a) \<Longrightarrow> b dvd Gcd A"
   1.669 -  and unit_factor_Gcd [simp]: 
   1.670 -    "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
   1.671 +lemma unit_factor_Gcd [simp]: "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
   1.672  proof -
   1.673 -  fix a assume "a \<in> A"
   1.674 -  hence "Lcm {d. \<forall>a\<in>A. d dvd a} dvd a" by (intro Lcm_least) blast
   1.675 -  then show "Gcd A dvd a" by (simp add: Gcd_Lcm)
   1.676 -next
   1.677 -  fix g' assume "\<And>a. a \<in> A \<Longrightarrow> g' dvd a"
   1.678 -  hence "g' dvd Lcm {d. \<forall>a\<in>A. d dvd a}" by (intro dvd_Lcm) blast
   1.679 -  then show "g' dvd Gcd A" by (simp add: Gcd_Lcm)
   1.680 -next
   1.681    show "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
   1.682 -    by (simp add: Gcd_Lcm)
   1.683 +    by (simp add: Gcd_Lcm unit_factor_Lcm)
   1.684  qed
   1.685  
   1.686 -lemma normalize_Gcd [simp]:
   1.687 -  "normalize (Gcd A) = Gcd A"
   1.688 -proof (cases "Gcd A = 0")
   1.689 -  case True then show ?thesis by simp
   1.690 -next
   1.691 -  case False
   1.692 -  have "unit_factor (Gcd A) * normalize (Gcd A) = Gcd A"
   1.693 -    by (fact unit_factor_mult_normalize)
   1.694 -  with False show ?thesis by simp
   1.695 -qed
   1.696 -
   1.697 -subclass semiring_Gcd
   1.698 -  by standard (auto intro: Gcd_greatest Lcm_least)
   1.699 -
   1.700  lemma GcdI:
   1.701    assumes "\<And>a. a \<in> A \<Longrightarrow> b dvd a" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> c dvd a) \<Longrightarrow> c dvd b"
   1.702      and "normalize b = b"
   1.703    shows "b = Gcd A"
   1.704 -  by (rule associated_eqI) (auto simp: assms intro: Gcd_greatest)
   1.705 -
   1.706 -lemma Lcm_Gcd:
   1.707 -  "Lcm A = Gcd {m. \<forall>a\<in>A. a dvd m}"
   1.708 -  by (rule LcmI[symmetric]) (auto intro: Gcd_greatest Gcd_greatest)
   1.709 +  by (rule associated_eqI) (auto simp: assms Gcd_dvd intro: Gcd_greatest)
   1.710  
   1.711  lemma Gcd_1:
   1.712    "1 \<in> A \<Longrightarrow> Gcd A = 1"
   1.713 @@ -1232,6 +1023,21 @@
   1.714  lemma Gcd_2 [simp]: "Gcd {a,b} = gcd a b"
   1.715    by simp
   1.716  
   1.717 +
   1.718 +definition pairwise_coprime where
   1.719 +  "pairwise_coprime A = (\<forall>x y. x \<in> A \<and> y \<in> A \<and> x \<noteq> y \<longrightarrow> coprime x y)"
   1.720 +
   1.721 +lemma pairwise_coprimeI [intro?]:
   1.722 +  "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y) \<Longrightarrow> pairwise_coprime A"
   1.723 +  by (simp add: pairwise_coprime_def)
   1.724 +
   1.725 +lemma pairwise_coprimeD:
   1.726 +  "pairwise_coprime A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y"
   1.727 +  by (simp add: pairwise_coprime_def)
   1.728 +
   1.729 +lemma pairwise_coprime_subset: "pairwise_coprime A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> pairwise_coprime B"
   1.730 +  by (force simp: pairwise_coprime_def)
   1.731 +
   1.732  end
   1.733  
   1.734  text \<open>
   1.735 @@ -1243,7 +1049,6 @@
   1.736  begin
   1.737  
   1.738  subclass euclidean_ring ..
   1.739 -
   1.740  subclass ring_gcd ..
   1.741  
   1.742  lemma euclid_ext_gcd [simp]:
   1.743 @@ -1325,6 +1130,7 @@
   1.744  
   1.745  end
   1.746  
   1.747 +
   1.748  instantiation int :: euclidean_ring
   1.749  begin
   1.750  
   1.751 @@ -1336,22 +1142,19 @@
   1.752  
   1.753  end
   1.754  
   1.755 +
   1.756  instantiation poly :: (field) euclidean_ring
   1.757  begin
   1.758  
   1.759  definition euclidean_size_poly :: "'a poly \<Rightarrow> nat"
   1.760 -  where "euclidean_size p = (if p = 0 then 0 else Suc (degree p))"
   1.761 -
   1.762 -lemma euclidenan_size_poly_minus_one_degree [simp]:
   1.763 -  "euclidean_size p - 1 = degree p"
   1.764 -  by (simp add: euclidean_size_poly_def)
   1.765 +  where "euclidean_size p = (if p = 0 then 0 else 2 ^ degree p)"
   1.766  
   1.767  lemma euclidean_size_poly_0 [simp]:
   1.768    "euclidean_size (0::'a poly) = 0"
   1.769    by (simp add: euclidean_size_poly_def)
   1.770  
   1.771  lemma euclidean_size_poly_not_0 [simp]:
   1.772 -  "p \<noteq> 0 \<Longrightarrow> euclidean_size p = Suc (degree p)"
   1.773 +  "p \<noteq> 0 \<Longrightarrow> euclidean_size p = 2 ^ degree p"
   1.774    by (simp add: euclidean_size_poly_def)
   1.775  
   1.776  instance
   1.777 @@ -1369,23 +1172,45 @@
   1.778      by (rule degree_mult_right_le)
   1.779    with \<open>q \<noteq> 0\<close> show "euclidean_size p \<le> euclidean_size (p * q)"
   1.780      by (cases "p = 0") simp_all
   1.781 -qed
   1.782 +qed simp
   1.783  
   1.784  end
   1.785  
   1.786 -(*instance nat :: euclidean_semiring_gcd
   1.787 -proof (standard, auto intro!: ext)
   1.788 -  fix m n :: nat
   1.789 -  show *: "gcd m n = gcd_eucl m n"
   1.790 -  proof (induct m n rule: gcd_eucl_induct)
   1.791 -    case zero then show ?case by (simp add: gcd_eucl_0)
   1.792 -  next
   1.793 -    case (mod m n)
   1.794 -    with gcd_eucl_non_0 [of n m, symmetric]
   1.795 -    show ?case by (simp add: gcd_non_0_nat)
   1.796 -  qed
   1.797 -  show "lcm m n = lcm_eucl m n"
   1.798 -    by (simp add: lcm_eucl_def lcm_gcd * [symmetric] lcm_nat_def)
   1.799 -qed*)
   1.800 +
   1.801 +instance nat :: euclidean_semiring_gcd
   1.802 +proof
   1.803 +  show [simp]: "gcd = (gcd_eucl :: nat \<Rightarrow> _)" "Lcm = (Lcm_eucl :: nat set \<Rightarrow> _)"
   1.804 +    by (simp_all add: eq_gcd_euclI eq_Lcm_euclI)
   1.805 +  show "lcm = (lcm_eucl :: nat \<Rightarrow> _)" "Gcd = (Gcd_eucl :: nat set \<Rightarrow> _)"
   1.806 +    by (intro ext, simp add: lcm_eucl_def lcm_nat_def Gcd_nat_def Gcd_eucl_def)+
   1.807 +qed
   1.808 +
   1.809 +instance int :: euclidean_ring_gcd
   1.810 +proof
   1.811 +  show [simp]: "gcd = (gcd_eucl :: int \<Rightarrow> _)" "Lcm = (Lcm_eucl :: int set \<Rightarrow> _)"
   1.812 +    by (simp_all add: eq_gcd_euclI eq_Lcm_euclI)
   1.813 +  show "lcm = (lcm_eucl :: int \<Rightarrow> _)" "Gcd = (Gcd_eucl :: int set \<Rightarrow> _)"
   1.814 +    by (intro ext, simp add: lcm_eucl_def lcm_altdef_int 
   1.815 +          semiring_Gcd_class.Gcd_Lcm Gcd_eucl_def abs_mult)+
   1.816 +qed
   1.817 +
   1.818 +
   1.819 +instantiation poly :: (field) euclidean_ring_gcd
   1.820 +begin
   1.821 +
   1.822 +definition gcd_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
   1.823 +  "gcd_poly = gcd_eucl"
   1.824 +  
   1.825 +definition lcm_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
   1.826 +  "lcm_poly = lcm_eucl"
   1.827 +  
   1.828 +definition Gcd_poly :: "'a poly set \<Rightarrow> 'a poly" where
   1.829 +  "Gcd_poly = Gcd_eucl"
   1.830 +  
   1.831 +definition Lcm_poly :: "'a poly set \<Rightarrow> 'a poly" where
   1.832 +  "Lcm_poly = Lcm_eucl"
   1.833 +
   1.834 +instance by standard (simp_all only: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def)
   1.835 +end
   1.836  
   1.837  end