src/HOL/GCD.thy
changeset 67051 e7e54a0b9197
parent 66936 cf8d8fc23891
child 67118 ccab07d1196c
     1.1 --- a/src/HOL/GCD.thy	Sat Nov 11 18:33:35 2017 +0000
     1.2 +++ b/src/HOL/GCD.thy	Sat Nov 11 18:41:08 2017 +0000
     1.3 @@ -142,12 +142,6 @@
     1.4  class gcd = zero + one + dvd +
     1.5    fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
     1.6      and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
     1.7 -begin
     1.8 -
     1.9 -abbreviation coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.10 -  where "coprime x y \<equiv> gcd x y = 1"
    1.11 -
    1.12 -end
    1.13  
    1.14  class Gcd = gcd +
    1.15    fixes Gcd :: "'a set \<Rightarrow> 'a"
    1.16 @@ -243,7 +237,8 @@
    1.17      by simp
    1.18  qed
    1.19  
    1.20 -lemma is_unit_gcd [simp]: "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
    1.21 +lemma is_unit_gcd_iff [simp]:
    1.22 +  "is_unit (gcd a b) \<longleftrightarrow> gcd a b = 1"
    1.23    by (cases "a = 0 \<and> b = 0") (auto simp add: unit_factor_gcd dest: is_unit_unit_factor)
    1.24  
    1.25  sublocale gcd: abel_semigroup gcd
    1.26 @@ -279,7 +274,7 @@
    1.27    show "gcd (normalize a) b = gcd a b" for a b
    1.28      using gcd_dvd1 [of "normalize a" b]
    1.29      by (auto intro: associated_eqI)
    1.30 -  show "coprime 1 a" for a
    1.31 +  show "gcd 1 a = 1" for a
    1.32      by (rule associated_eqI) simp_all
    1.33  qed simp_all
    1.34  
    1.35 @@ -292,12 +287,6 @@
    1.36  lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b"
    1.37    by (fact gcd.right_idem)
    1.38  
    1.39 -lemma coprime_1_left: "coprime 1 a"
    1.40 -  by (fact gcd.bottom_left_bottom)
    1.41 -
    1.42 -lemma coprime_1_right: "coprime a 1"
    1.43 -  by (fact gcd.bottom_right_bottom)
    1.44 -
    1.45  lemma gcd_mult_left: "gcd (c * a) (c * b) = normalize c * gcd a b"
    1.46  proof (cases "c = 0")
    1.47    case True
    1.48 @@ -634,70 +623,6 @@
    1.49      by (rule dvd_trans)
    1.50  qed
    1.51  
    1.52 -lemma coprime_dvd_mult:
    1.53 -  assumes "coprime a b" and "a dvd c * b"
    1.54 -  shows "a dvd c"
    1.55 -proof (cases "c = 0")
    1.56 -  case True
    1.57 -  then show ?thesis by simp
    1.58 -next
    1.59 -  case False
    1.60 -  then have unit: "is_unit (unit_factor c)"
    1.61 -    by simp
    1.62 -  from \<open>coprime a b\<close> mult_gcd_left [of c a b]
    1.63 -  have "gcd (c * a) (c * b) * unit_factor c = c"
    1.64 -    by (simp add: ac_simps)
    1.65 -  moreover from \<open>a dvd c * b\<close> have "a dvd gcd (c * a) (c * b) * unit_factor c"
    1.66 -    by (simp add: dvd_mult_unit_iff unit)
    1.67 -  ultimately show ?thesis
    1.68 -    by simp
    1.69 -qed
    1.70 -
    1.71 -lemma coprime_dvd_mult_iff: "coprime a c \<Longrightarrow> a dvd b * c \<longleftrightarrow> a dvd b"
    1.72 -  by (auto intro: coprime_dvd_mult)
    1.73 -
    1.74 -lemma gcd_mult_cancel: "coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b"
    1.75 -  apply (rule associated_eqI)
    1.76 -     apply (rule gcd_greatest)
    1.77 -      apply (rule_tac b = c in coprime_dvd_mult)
    1.78 -       apply (simp add: gcd.assoc)
    1.79 -       apply (simp_all add: ac_simps)
    1.80 -  done
    1.81 -
    1.82 -lemma coprime_crossproduct:
    1.83 -  fixes a b c d :: 'a
    1.84 -  assumes "coprime a d" and "coprime b c"
    1.85 -  shows "normalize a * normalize c = normalize b * normalize d \<longleftrightarrow>
    1.86 -    normalize a = normalize b \<and> normalize c = normalize d"
    1.87 -    (is "?lhs \<longleftrightarrow> ?rhs")
    1.88 -proof
    1.89 -  assume ?rhs
    1.90 -  then show ?lhs by simp
    1.91 -next
    1.92 -  assume ?lhs
    1.93 -  from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
    1.94 -    by (auto intro: dvdI dest: sym)
    1.95 -  with \<open>coprime a d\<close> have "a dvd b"
    1.96 -    by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
    1.97 -  from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c"
    1.98 -    by (auto intro: dvdI dest: sym)
    1.99 -  with \<open>coprime b c\<close> have "b dvd a"
   1.100 -    by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
   1.101 -  from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b"
   1.102 -    by (auto intro: dvdI dest: sym simp add: mult.commute)
   1.103 -  with \<open>coprime b c\<close> have "c dvd d"
   1.104 -    by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
   1.105 -  from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a"
   1.106 -    by (auto intro: dvdI dest: sym simp add: mult.commute)
   1.107 -  with \<open>coprime a d\<close> have "d dvd c"
   1.108 -    by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
   1.109 -  from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b"
   1.110 -    by (rule associatedI)
   1.111 -  moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d"
   1.112 -    by (rule associatedI)
   1.113 -  ultimately show ?rhs ..
   1.114 -qed
   1.115 -
   1.116  lemma gcd_add1 [simp]: "gcd (m + n) n = gcd m n"
   1.117    by (rule gcdI [symmetric]) (simp_all add: dvd_add_left_iff)
   1.118  
   1.119 @@ -707,285 +632,6 @@
   1.120  lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
   1.121    by (rule gcdI [symmetric]) (simp_all add: dvd_add_right_iff)
   1.122  
   1.123 -lemma coprimeI: "(\<And>l. l dvd a \<Longrightarrow> l dvd b \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd a b = 1"
   1.124 -  by (rule sym, rule gcdI) simp_all
   1.125 -
   1.126 -lemma coprime: "gcd a b = 1 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)"
   1.127 -  by (auto intro: coprimeI gcd_greatest dvd_gcdD1 dvd_gcdD2)
   1.128 -
   1.129 -lemma div_gcd_coprime:
   1.130 -  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
   1.131 -  shows "coprime (a div gcd a b) (b div gcd a b)"
   1.132 -proof -
   1.133 -  let ?g = "gcd a b"
   1.134 -  let ?a' = "a div ?g"
   1.135 -  let ?b' = "b div ?g"
   1.136 -  let ?g' = "gcd ?a' ?b'"
   1.137 -  have dvdg: "?g dvd a" "?g dvd b"
   1.138 -    by simp_all
   1.139 -  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'"
   1.140 -    by simp_all
   1.141 -  from dvdg dvdg' obtain ka kb ka' kb' where
   1.142 -    kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
   1.143 -    unfolding dvd_def by blast
   1.144 -  from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
   1.145 -    by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
   1.146 -  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   1.147 -    by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   1.148 -  have "?g \<noteq> 0"
   1.149 -    using nz by simp
   1.150 -  moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   1.151 -  ultimately show ?thesis
   1.152 -    using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
   1.153 -qed
   1.154 -
   1.155 -lemma divides_mult:
   1.156 -  assumes "a dvd c" and nr: "b dvd c" and "coprime a b"
   1.157 -  shows "a * b dvd c"
   1.158 -proof -
   1.159 -  from \<open>b dvd c\<close> obtain b' where"c = b * b'" ..
   1.160 -  with \<open>a dvd c\<close> have "a dvd b' * b"
   1.161 -    by (simp add: ac_simps)
   1.162 -  with \<open>coprime a b\<close> have "a dvd b'"
   1.163 -    by (simp add: coprime_dvd_mult_iff)
   1.164 -  then obtain a' where "b' = a * a'" ..
   1.165 -  with \<open>c = b * b'\<close> have "c = (a * b) * a'"
   1.166 -    by (simp add: ac_simps)
   1.167 -  then show ?thesis ..
   1.168 -qed
   1.169 -
   1.170 -lemma coprime_lmult:
   1.171 -  assumes dab: "gcd d (a * b) = 1"
   1.172 -  shows "gcd d a = 1"
   1.173 -proof (rule coprimeI)
   1.174 -  fix l
   1.175 -  assume "l dvd d" and "l dvd a"
   1.176 -  then have "l dvd a * b"
   1.177 -    by simp
   1.178 -  with \<open>l dvd d\<close> and dab show "l dvd 1"
   1.179 -    by (auto intro: gcd_greatest)
   1.180 -qed
   1.181 -
   1.182 -lemma coprime_rmult:
   1.183 -  assumes dab: "gcd d (a * b) = 1"
   1.184 -  shows "gcd d b = 1"
   1.185 -proof (rule coprimeI)
   1.186 -  fix l
   1.187 -  assume "l dvd d" and "l dvd b"
   1.188 -  then have "l dvd a * b"
   1.189 -    by simp
   1.190 -  with \<open>l dvd d\<close> and dab show "l dvd 1"
   1.191 -    by (auto intro: gcd_greatest)
   1.192 -qed
   1.193 -
   1.194 -lemma coprime_mult:
   1.195 -  assumes "coprime d a"
   1.196 -    and "coprime d b"
   1.197 -  shows "coprime d (a * b)"
   1.198 -  apply (subst gcd.commute)
   1.199 -  using assms(1) apply (subst gcd_mult_cancel)
   1.200 -   apply (subst gcd.commute)
   1.201 -   apply assumption
   1.202 -  apply (subst gcd.commute)
   1.203 -  apply (rule assms(2))
   1.204 -  done
   1.205 -
   1.206 -lemma coprime_mul_eq: "gcd d (a * b) = 1 \<longleftrightarrow> gcd d a = 1 \<and> gcd d b = 1"
   1.207 -  using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b]
   1.208 -  by blast
   1.209 -
   1.210 -lemma coprime_mul_eq':
   1.211 -  "coprime (a * b) d \<longleftrightarrow> coprime a d \<and> coprime b d"
   1.212 -  using coprime_mul_eq [of d a b] by (simp add: gcd.commute)
   1.213 -
   1.214 -lemma gcd_coprime:
   1.215 -  assumes c: "gcd a b \<noteq> 0"
   1.216 -    and a: "a = a' * gcd a b"
   1.217 -    and b: "b = b' * gcd a b"
   1.218 -  shows "gcd a' b' = 1"
   1.219 -proof -
   1.220 -  from c have "a \<noteq> 0 \<or> b \<noteq> 0"
   1.221 -    by simp
   1.222 -  with div_gcd_coprime have "gcd (a div gcd a b) (b div gcd a b) = 1" .
   1.223 -  also from assms have "a div gcd a b = a'"
   1.224 -    using dvd_div_eq_mult local.gcd_dvd1 by blast
   1.225 -  also from assms have "b div gcd a b = b'"
   1.226 -    using dvd_div_eq_mult local.gcd_dvd1 by blast
   1.227 -  finally show ?thesis .
   1.228 -qed
   1.229 -
   1.230 -lemma coprime_power:
   1.231 -  assumes "0 < n"
   1.232 -  shows "gcd a (b ^ n) = 1 \<longleftrightarrow> gcd a b = 1"
   1.233 -  using assms
   1.234 -proof (induct n)
   1.235 -  case 0
   1.236 -  then show ?case by simp
   1.237 -next
   1.238 -  case (Suc n)
   1.239 -  then show ?case
   1.240 -    by (cases n) (simp_all add: coprime_mul_eq)
   1.241 -qed
   1.242 -
   1.243 -lemma gcd_coprime_exists:
   1.244 -  assumes "gcd a b \<noteq> 0"
   1.245 -  shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> gcd a' b' = 1"
   1.246 -  apply (rule_tac x = "a div gcd a b" in exI)
   1.247 -  apply (rule_tac x = "b div gcd a b" in exI)
   1.248 -  using assms
   1.249 -  apply (auto intro: div_gcd_coprime)
   1.250 -  done
   1.251 -
   1.252 -lemma coprime_exp: "gcd d a = 1 \<Longrightarrow> gcd d (a^n) = 1"
   1.253 -  by (induct n) (simp_all add: coprime_mult)
   1.254 -
   1.255 -lemma coprime_exp_left: "coprime a b \<Longrightarrow> coprime (a ^ n) b"
   1.256 -  by (induct n) (simp_all add: gcd_mult_cancel)
   1.257 -
   1.258 -lemma coprime_exp2:
   1.259 -  assumes "coprime a b"
   1.260 -  shows "coprime (a ^ n) (b ^ m)"
   1.261 -proof (rule coprime_exp_left)
   1.262 -  from assms show "coprime a (b ^ m)"
   1.263 -    by (induct m) (simp_all add: gcd_mult_cancel gcd.commute [of a])
   1.264 -qed
   1.265 -
   1.266 -lemma gcd_exp: "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
   1.267 -proof (cases "a = 0 \<and> b = 0")
   1.268 -  case True
   1.269 -  then show ?thesis
   1.270 -    by (cases n) simp_all
   1.271 -next
   1.272 -  case False
   1.273 -  then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
   1.274 -    using coprime_exp2[OF div_gcd_coprime[of a b], of n n, symmetric] by simp
   1.275 -  then have "gcd a b ^ n = gcd a b ^ n * \<dots>"
   1.276 -    by simp
   1.277 -  also note gcd_mult_distrib
   1.278 -  also have "unit_factor (gcd a b ^ n) = 1"
   1.279 -    using False by (auto simp add: unit_factor_power unit_factor_gcd)
   1.280 -  also have "(gcd a b)^n * (a div gcd a b)^n = a^n"
   1.281 -    apply (subst ac_simps)
   1.282 -    apply (subst div_power)
   1.283 -     apply simp
   1.284 -    apply (rule dvd_div_mult_self)
   1.285 -    apply (rule dvd_power_same)
   1.286 -    apply simp
   1.287 -    done
   1.288 -  also have "(gcd a b)^n * (b div gcd a b)^n = b^n"
   1.289 -    apply (subst ac_simps)
   1.290 -    apply (subst div_power)
   1.291 -     apply simp
   1.292 -    apply (rule dvd_div_mult_self)
   1.293 -    apply (rule dvd_power_same)
   1.294 -    apply simp
   1.295 -    done
   1.296 -  finally show ?thesis by simp
   1.297 -qed
   1.298 -
   1.299 -lemma coprime_common_divisor: "gcd a b = 1 \<Longrightarrow> a dvd a \<Longrightarrow> a dvd b \<Longrightarrow> is_unit a"
   1.300 -  apply (subgoal_tac "a dvd gcd a b")
   1.301 -   apply simp
   1.302 -  apply (erule (1) gcd_greatest)
   1.303 -  done
   1.304 -
   1.305 -lemma division_decomp:
   1.306 -  assumes "a dvd b * c"
   1.307 -  shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   1.308 -proof (cases "gcd a b = 0")
   1.309 -  case True
   1.310 -  then have "a = 0 \<and> b = 0"
   1.311 -    by simp
   1.312 -  then have "a = 0 * c \<and> 0 dvd b \<and> c dvd c"
   1.313 -    by simp
   1.314 -  then show ?thesis by blast
   1.315 -next
   1.316 -  case False
   1.317 -  let ?d = "gcd a b"
   1.318 -  from gcd_coprime_exists [OF False]
   1.319 -    obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
   1.320 -    by blast
   1.321 -  from ab'(1) have "a' dvd a"
   1.322 -    unfolding dvd_def by blast
   1.323 -  with assms have "a' dvd b * c"
   1.324 -    using dvd_trans [of a' a "b * c"] by simp
   1.325 -  from assms ab'(1,2) have "a' * ?d dvd (b' * ?d) * c"
   1.326 -    by simp
   1.327 -  then have "?d * a' dvd ?d * (b' * c)"
   1.328 -    by (simp add: mult_ac)
   1.329 -  with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c"
   1.330 -    by simp
   1.331 -  with coprime_dvd_mult[OF ab'(3)] have "a' dvd c"
   1.332 -    by (subst (asm) ac_simps) blast
   1.333 -  with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c"
   1.334 -    by (simp add: mult_ac)
   1.335 -  then show ?thesis by blast
   1.336 -qed
   1.337 -
   1.338 -lemma pow_divs_pow:
   1.339 -  assumes ab: "a ^ n dvd b ^ n" and n: "n \<noteq> 0"
   1.340 -  shows "a dvd b"
   1.341 -proof (cases "gcd a b = 0")
   1.342 -  case True
   1.343 -  then show ?thesis by simp
   1.344 -next
   1.345 -  case False
   1.346 -  let ?d = "gcd a b"
   1.347 -  from n obtain m where m: "n = Suc m"
   1.348 -    by (cases n) simp_all
   1.349 -  from False have zn: "?d ^ n \<noteq> 0"
   1.350 -    by (rule power_not_zero)
   1.351 -  from gcd_coprime_exists [OF False]
   1.352 -  obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
   1.353 -    by blast
   1.354 -  from ab have "(a' * ?d) ^ n dvd (b' * ?d) ^ n"
   1.355 -    by (simp add: ab'(1,2)[symmetric])
   1.356 -  then have "?d^n * a'^n dvd ?d^n * b'^n"
   1.357 -    by (simp only: power_mult_distrib ac_simps)
   1.358 -  with zn have "a'^n dvd b'^n"
   1.359 -    by simp
   1.360 -  then have "a' dvd b'^n"
   1.361 -    using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m)
   1.362 -  then have "a' dvd b'^m * b'"
   1.363 -    by (simp add: m ac_simps)
   1.364 -  with coprime_dvd_mult[OF coprime_exp[OF ab'(3), of m]]
   1.365 -  have "a' dvd b'" by (subst (asm) ac_simps) blast
   1.366 -  then have "a' * ?d dvd b' * ?d"
   1.367 -    by (rule mult_dvd_mono) simp
   1.368 -  with ab'(1,2) show ?thesis
   1.369 -    by simp
   1.370 -qed
   1.371 -
   1.372 -lemma pow_divs_eq [simp]: "n \<noteq> 0 \<Longrightarrow> a ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
   1.373 -  by (auto intro: pow_divs_pow dvd_power_same)
   1.374 -
   1.375 -lemma coprime_plus_one [simp]: "gcd (n + 1) n = 1"
   1.376 -  by (subst add_commute) simp
   1.377 -
   1.378 -lemma prod_coprime [rule_format]: "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
   1.379 -  by (induct A rule: infinite_finite_induct) (auto simp add: gcd_mult_cancel)
   1.380 -
   1.381 -lemma prod_list_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (prod_list xs) y"
   1.382 -  by (induct xs) (simp_all add: gcd_mult_cancel)
   1.383 -
   1.384 -lemma coprime_divisors:
   1.385 -  assumes "d dvd a" "e dvd b" "gcd a b = 1"
   1.386 -  shows "gcd d e = 1"
   1.387 -proof -
   1.388 -  from assms obtain k l where "a = d * k" "b = e * l"
   1.389 -    unfolding dvd_def by blast
   1.390 -  with assms have "gcd (d * k) (e * l) = 1"
   1.391 -    by simp
   1.392 -  then have "gcd (d * k) e = 1"
   1.393 -    by (rule coprime_lmult)
   1.394 -  also have "gcd (d * k) e = gcd e (d * k)"
   1.395 -    by (simp add: ac_simps)
   1.396 -  finally have "gcd e d = 1"
   1.397 -    by (rule coprime_lmult)
   1.398 -  then show ?thesis
   1.399 -    by (simp add: ac_simps)
   1.400 -qed
   1.401 -
   1.402  lemma lcm_gcd_prod: "lcm a b * gcd a b = normalize (a * b)"
   1.403    by (simp add: lcm_gcd)
   1.404  
   1.405 @@ -1006,9 +652,6 @@
   1.406    "a dvd d \<and> b dvd d \<and> normalize d = d \<and> (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
   1.407    by rule (auto intro: lcmI simp: lcm_least lcm_eq_0_iff)
   1.408  
   1.409 -lemma lcm_coprime: "gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)"
   1.410 -  by (subst lcm_gcd) simp
   1.411 -
   1.412  lemma lcm_proj1_if_dvd: "b dvd a \<Longrightarrow> lcm a b = normalize a"
   1.413    apply (cases "a = 0")
   1.414     apply simp
   1.415 @@ -1058,7 +701,7 @@
   1.416  qed
   1.417  
   1.418  lemma dvd_productE:
   1.419 -  assumes "p dvd (a * b)"
   1.420 +  assumes "p dvd a * b"
   1.421    obtains x y where "p = x * y" "x dvd a" "y dvd b"
   1.422  proof (cases "a = 0")
   1.423    case True
   1.424 @@ -1076,32 +719,11 @@
   1.425    ultimately show ?thesis by (rule that)
   1.426  qed
   1.427  
   1.428 -lemma coprime_crossproduct':
   1.429 -  fixes a b c d
   1.430 -  assumes "b \<noteq> 0"
   1.431 -  assumes unit_factors: "unit_factor b = unit_factor d"
   1.432 -  assumes coprime: "coprime a b" "coprime c d"
   1.433 -  shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
   1.434 -proof safe
   1.435 -  assume eq: "a * d = b * c"
   1.436 -  hence "normalize a * normalize d = normalize c * normalize b"
   1.437 -    by (simp only: normalize_mult [symmetric] mult_ac)
   1.438 -  with coprime have "normalize b = normalize d"
   1.439 -    by (subst (asm) coprime_crossproduct) simp_all
   1.440 -  from this and unit_factors show "b = d"
   1.441 -    by (rule normalize_unit_factor_eqI)
   1.442 -  from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
   1.443 -  with \<open>b \<noteq> 0\<close> \<open>b = d\<close> show "a = c" by simp
   1.444 -qed (simp_all add: mult_ac)
   1.445 -
   1.446  end
   1.447  
   1.448  class ring_gcd = comm_ring_1 + semiring_gcd
   1.449  begin
   1.450  
   1.451 -lemma coprime_minus_one: "coprime (n - 1) n"
   1.452 -  using coprime_plus_one[of "n - 1"] by (simp add: gcd.commute)
   1.453 -
   1.454  lemma gcd_neg1 [simp]: "gcd (-a) b = gcd a b"
   1.455    by (rule sym, rule gcdI) (simp_all add: gcd_greatest)
   1.456  
   1.457 @@ -1471,36 +1093,6 @@
   1.458  lemma Lcm_2 [simp]: "Lcm {a, b} = lcm a b"
   1.459    by simp
   1.460  
   1.461 -lemma Lcm_coprime:
   1.462 -  assumes "finite A"
   1.463 -    and "A \<noteq> {}"
   1.464 -    and "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1"
   1.465 -  shows "Lcm A = normalize (\<Prod>A)"
   1.466 -  using assms
   1.467 -proof (induct rule: finite_ne_induct)
   1.468 -  case singleton
   1.469 -  then show ?case by simp
   1.470 -next
   1.471 -  case (insert a A)
   1.472 -  have "Lcm (insert a A) = lcm a (Lcm A)"
   1.473 -    by simp
   1.474 -  also from insert have "Lcm A = normalize (\<Prod>A)"
   1.475 -    by blast
   1.476 -  also have "lcm a \<dots> = lcm a (\<Prod>A)"
   1.477 -    by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
   1.478 -  also from insert have "gcd a (\<Prod>A) = 1"
   1.479 -    by (subst gcd.commute, intro prod_coprime) auto
   1.480 -  with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
   1.481 -    by (simp add: lcm_coprime)
   1.482 -  finally show ?case .
   1.483 -qed
   1.484 -
   1.485 -lemma Lcm_coprime':
   1.486 -  "card A \<noteq> 0 \<Longrightarrow>
   1.487 -    (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1) \<Longrightarrow>
   1.488 -    Lcm A = normalize (\<Prod>A)"
   1.489 -  by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
   1.490 -
   1.491  lemma Gcd_1: "1 \<in> A \<Longrightarrow> Gcd A = 1"
   1.492    by (auto intro!: Gcd_eq_1_I)
   1.493  
   1.494 @@ -1677,6 +1269,465 @@
   1.495  
   1.496  end
   1.497  
   1.498 +
   1.499 +subsection \<open>Coprimality\<close>
   1.500 +
   1.501 +context semiring_gcd
   1.502 +begin
   1.503 +
   1.504 +lemma coprime_imp_gcd_eq_1 [simp]:
   1.505 +  "gcd a b = 1" if "coprime a b"
   1.506 +proof -
   1.507 +  define t r s where "t = gcd a b" and "r = a div t" and "s = b div t"
   1.508 +  then have "a = t * r" and "b = t * s"
   1.509 +    by simp_all
   1.510 +  with that have "coprime (t * r) (t * s)"
   1.511 +    by simp
   1.512 +  then show ?thesis
   1.513 +    by (simp add: t_def)
   1.514 +qed
   1.515 +
   1.516 +lemma gcd_eq_1_imp_coprime:
   1.517 +  "coprime a b" if "gcd a b = 1"
   1.518 +proof (rule coprimeI)
   1.519 +  fix c
   1.520 +  assume "c dvd a" and "c dvd b"
   1.521 +  then have "c dvd gcd a b"
   1.522 +    by (rule gcd_greatest)
   1.523 +  with that show "is_unit c"
   1.524 +    by simp
   1.525 +qed
   1.526 +
   1.527 +lemma coprime_iff_gcd_eq_1 [presburger, code]:
   1.528 +  "coprime a b \<longleftrightarrow> gcd a b = 1"
   1.529 +  by rule (simp_all add: gcd_eq_1_imp_coprime)
   1.530 +
   1.531 +lemma is_unit_gcd [simp]:
   1.532 +  "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
   1.533 +  by (simp add: coprime_iff_gcd_eq_1)
   1.534 +
   1.535 +lemma coprime_add_one_left [simp]: "coprime (a + 1) a"
   1.536 +  by (simp add: gcd_eq_1_imp_coprime ac_simps)
   1.537 +
   1.538 +lemma coprime_add_one_right [simp]: "coprime a (a + 1)"
   1.539 +  using coprime_add_one_left [of a] by (simp add: ac_simps)
   1.540 +
   1.541 +lemma coprime_mult_left_iff [simp]:
   1.542 +  "coprime (a * b) c \<longleftrightarrow> coprime a c \<and> coprime b c"
   1.543 +proof
   1.544 +  assume "coprime (a * b) c"
   1.545 +  with coprime_common_divisor [of "a * b" c]
   1.546 +  have *: "is_unit d" if "d dvd a * b" and "d dvd c" for d
   1.547 +    using that by blast
   1.548 +  have "coprime a c"
   1.549 +    by (rule coprimeI, rule *) simp_all
   1.550 +  moreover have "coprime b c"
   1.551 +    by (rule coprimeI, rule *) simp_all
   1.552 +  ultimately show "coprime a c \<and> coprime b c" ..
   1.553 +next
   1.554 +  assume "coprime a c \<and> coprime b c"
   1.555 +  then have "coprime a c" "coprime b c"
   1.556 +    by simp_all
   1.557 +  show "coprime (a * b) c"
   1.558 +  proof (rule coprimeI)
   1.559 +    fix d
   1.560 +    assume "d dvd a * b"
   1.561 +    then obtain r s where d: "d = r * s" "r dvd a" "s dvd b"
   1.562 +      by (rule dvd_productE)
   1.563 +    assume "d dvd c"
   1.564 +    with d have "r * s dvd c"
   1.565 +      by simp
   1.566 +    then have "r dvd c" "s dvd c"
   1.567 +      by (auto intro: dvd_mult_left dvd_mult_right)
   1.568 +    from \<open>coprime a c\<close> \<open>r dvd a\<close> \<open>r dvd c\<close>
   1.569 +    have "is_unit r"
   1.570 +      by (rule coprime_common_divisor)
   1.571 +    moreover from \<open>coprime b c\<close> \<open>s dvd b\<close> \<open>s dvd c\<close>
   1.572 +    have "is_unit s"
   1.573 +      by (rule coprime_common_divisor)
   1.574 +    ultimately show "is_unit d"
   1.575 +      by (simp add: d is_unit_mult_iff)
   1.576 +  qed
   1.577 +qed
   1.578 +
   1.579 +lemma coprime_mult_right_iff [simp]:
   1.580 +  "coprime c (a * b) \<longleftrightarrow> coprime c a \<and> coprime c b"
   1.581 +  using coprime_mult_left_iff [of a b c] by (simp add: ac_simps)
   1.582 +
   1.583 +lemma coprime_power_left_iff [simp]:
   1.584 +  "coprime (a ^ n) b \<longleftrightarrow> coprime a b \<or> n = 0"
   1.585 +proof (cases "n = 0")
   1.586 +  case True
   1.587 +  then show ?thesis
   1.588 +    by simp
   1.589 +next
   1.590 +  case False
   1.591 +  then have "n > 0"
   1.592 +    by simp
   1.593 +  then show ?thesis
   1.594 +    by (induction n rule: nat_induct_non_zero) simp_all
   1.595 +qed
   1.596 +
   1.597 +lemma coprime_power_right_iff [simp]:
   1.598 +  "coprime a (b ^ n) \<longleftrightarrow> coprime a b \<or> n = 0"
   1.599 +  using coprime_power_left_iff [of b n a] by (simp add: ac_simps)
   1.600 +
   1.601 +lemma prod_coprime_left:
   1.602 +  "coprime (\<Prod>i\<in>A. f i) a" if "\<And>i. i \<in> A \<Longrightarrow> coprime (f i) a"
   1.603 +  using that by (induct A rule: infinite_finite_induct) simp_all
   1.604 +
   1.605 +lemma prod_coprime_right:
   1.606 +  "coprime a (\<Prod>i\<in>A. f i)" if "\<And>i. i \<in> A \<Longrightarrow> coprime a (f i)"
   1.607 +  using that prod_coprime_left [of A f a] by (simp add: ac_simps)
   1.608 +
   1.609 +lemma prod_list_coprime_left:
   1.610 +  "coprime (prod_list xs) a" if "\<And>x. x \<in> set xs \<Longrightarrow> coprime x a"
   1.611 +  using that by (induct xs) simp_all
   1.612 +
   1.613 +lemma prod_list_coprime_right:
   1.614 +  "coprime a (prod_list xs)" if "\<And>x. x \<in> set xs \<Longrightarrow> coprime a x"
   1.615 +  using that prod_list_coprime_left [of xs a] by (simp add: ac_simps)
   1.616 +
   1.617 +lemma coprime_dvd_mult_left_iff:
   1.618 +  "a dvd b * c \<longleftrightarrow> a dvd b" if "coprime a c"
   1.619 +proof
   1.620 +  assume "a dvd b"
   1.621 +  then show "a dvd b * c"
   1.622 +    by simp
   1.623 +next
   1.624 +  assume "a dvd b * c"
   1.625 +  show "a dvd b"
   1.626 +  proof (cases "b = 0")
   1.627 +    case True
   1.628 +    then show ?thesis
   1.629 +      by simp
   1.630 +  next
   1.631 +    case False
   1.632 +    then have unit: "is_unit (unit_factor b)"
   1.633 +      by simp
   1.634 +    from \<open>coprime a c\<close> mult_gcd_left [of b a c]
   1.635 +    have "gcd (b * a) (b * c) * unit_factor b = b"
   1.636 +      by (simp add: ac_simps)
   1.637 +    moreover from \<open>a dvd b * c\<close>
   1.638 +    have "a dvd gcd (b * a) (b * c) * unit_factor b"
   1.639 +      by (simp add: dvd_mult_unit_iff unit)
   1.640 +    ultimately show ?thesis
   1.641 +      by simp
   1.642 +  qed
   1.643 +qed
   1.644 +
   1.645 +lemma coprime_dvd_mult_right_iff:
   1.646 +  "a dvd c * b \<longleftrightarrow> a dvd b" if "coprime a c"
   1.647 +  using that coprime_dvd_mult_left_iff [of a c b] by (simp add: ac_simps)
   1.648 +
   1.649 +lemma divides_mult:
   1.650 +  "a * b dvd c" if "a dvd c" and "b dvd c" and "coprime a b"
   1.651 +proof -
   1.652 +  from \<open>b dvd c\<close> obtain b' where "c = b * b'" ..
   1.653 +  with \<open>a dvd c\<close> have "a dvd b' * b"
   1.654 +    by (simp add: ac_simps)
   1.655 +  with \<open>coprime a b\<close> have "a dvd b'"
   1.656 +    by (simp add: coprime_dvd_mult_left_iff)
   1.657 +  then obtain a' where "b' = a * a'" ..
   1.658 +  with \<open>c = b * b'\<close> have "c = (a * b) * a'"
   1.659 +    by (simp add: ac_simps)
   1.660 +  then show ?thesis ..
   1.661 +qed
   1.662 +
   1.663 +lemma div_gcd_coprime:
   1.664 +  assumes "a \<noteq> 0 \<or> b \<noteq> 0"
   1.665 +  shows "coprime (a div gcd a b) (b div gcd a b)"
   1.666 +proof -
   1.667 +  let ?g = "gcd a b"
   1.668 +  let ?a' = "a div ?g"
   1.669 +  let ?b' = "b div ?g"
   1.670 +  let ?g' = "gcd ?a' ?b'"
   1.671 +  have dvdg: "?g dvd a" "?g dvd b"
   1.672 +    by simp_all
   1.673 +  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'"
   1.674 +    by simp_all
   1.675 +  from dvdg dvdg' obtain ka kb ka' kb' where
   1.676 +    kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
   1.677 +    unfolding dvd_def by blast
   1.678 +  from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
   1.679 +    by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
   1.680 +  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   1.681 +    by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   1.682 +  have "?g \<noteq> 0"
   1.683 +    using assms by simp
   1.684 +  moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   1.685 +  ultimately show ?thesis
   1.686 +    using dvd_times_left_cancel_iff [of "gcd a b" _ 1]
   1.687 +    by simp (simp only: coprime_iff_gcd_eq_1)
   1.688 +qed
   1.689 +
   1.690 +lemma gcd_coprime:
   1.691 +  assumes c: "gcd a b \<noteq> 0"
   1.692 +    and a: "a = a' * gcd a b"
   1.693 +    and b: "b = b' * gcd a b"
   1.694 +  shows "coprime a' b'"
   1.695 +proof -
   1.696 +  from c have "a \<noteq> 0 \<or> b \<noteq> 0"
   1.697 +    by simp
   1.698 +  with div_gcd_coprime have "coprime (a div gcd a b) (b div gcd a b)" .
   1.699 +  also from assms have "a div gcd a b = a'"
   1.700 +    using dvd_div_eq_mult local.gcd_dvd1 by blast
   1.701 +  also from assms have "b div gcd a b = b'"
   1.702 +    using dvd_div_eq_mult local.gcd_dvd1 by blast
   1.703 +  finally show ?thesis .
   1.704 +qed
   1.705 +
   1.706 +lemma gcd_coprime_exists:
   1.707 +  assumes "gcd a b \<noteq> 0"
   1.708 +  shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   1.709 +  apply (rule_tac x = "a div gcd a b" in exI)
   1.710 +  apply (rule_tac x = "b div gcd a b" in exI)
   1.711 +  using assms
   1.712 +  apply (auto intro: div_gcd_coprime)
   1.713 +  done
   1.714 +
   1.715 +lemma pow_divides_pow_iff [simp]:
   1.716 +  "a ^ n dvd b ^ n \<longleftrightarrow> a dvd b" if "n > 0"
   1.717 +proof (cases "gcd a b = 0")
   1.718 +  case True
   1.719 +  then show ?thesis
   1.720 +    by simp
   1.721 +next
   1.722 +  case False
   1.723 +  show ?thesis
   1.724 +  proof
   1.725 +    let ?d = "gcd a b"
   1.726 +    from \<open>n > 0\<close> obtain m where m: "n = Suc m"
   1.727 +      by (cases n) simp_all
   1.728 +    from False have zn: "?d ^ n \<noteq> 0"
   1.729 +      by (rule power_not_zero)
   1.730 +    from gcd_coprime_exists [OF False]
   1.731 +    obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "coprime a' b'"
   1.732 +      by blast
   1.733 +    assume "a ^ n dvd b ^ n"
   1.734 +    then have "(a' * ?d) ^ n dvd (b' * ?d) ^ n"
   1.735 +      by (simp add: ab'(1,2)[symmetric])
   1.736 +    then have "?d^n * a'^n dvd ?d^n * b'^n"
   1.737 +      by (simp only: power_mult_distrib ac_simps)
   1.738 +    with zn have "a' ^ n dvd b' ^ n"
   1.739 +      by simp
   1.740 +    then have "a' dvd b' ^ n"
   1.741 +      using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m)
   1.742 +    then have "a' dvd b' ^ m * b'"
   1.743 +      by (simp add: m ac_simps)
   1.744 +    moreover have "coprime a' (b' ^ n)"
   1.745 +      using \<open>coprime a' b'\<close> by simp
   1.746 +    then have "a' dvd b'"
   1.747 +      using \<open>a' dvd b' ^ n\<close> coprime_dvd_mult_left_iff dvd_mult by blast
   1.748 +    then have "a' * ?d dvd b' * ?d"
   1.749 +      by (rule mult_dvd_mono) simp
   1.750 +    with ab'(1,2) show "a dvd b"
   1.751 +      by simp
   1.752 +  next
   1.753 +    assume "a dvd b"
   1.754 +    with \<open>n > 0\<close> show "a ^ n dvd b ^ n"
   1.755 +      by (induction rule: nat_induct_non_zero)
   1.756 +        (simp_all add: mult_dvd_mono)
   1.757 +  qed
   1.758 +qed
   1.759 +
   1.760 +lemma coprime_crossproduct:
   1.761 +  fixes a b c d :: 'a
   1.762 +  assumes "coprime a d" and "coprime b c"
   1.763 +  shows "normalize a * normalize c = normalize b * normalize d \<longleftrightarrow>
   1.764 +    normalize a = normalize b \<and> normalize c = normalize d"
   1.765 +    (is "?lhs \<longleftrightarrow> ?rhs")
   1.766 +proof
   1.767 +  assume ?rhs
   1.768 +  then show ?lhs by simp
   1.769 +next
   1.770 +  assume ?lhs
   1.771 +  from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
   1.772 +    by (auto intro: dvdI dest: sym)
   1.773 +  with \<open>coprime a d\<close> have "a dvd b"
   1.774 +    by (simp add: coprime_dvd_mult_left_iff normalize_mult [symmetric])
   1.775 +  from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c"
   1.776 +    by (auto intro: dvdI dest: sym)
   1.777 +  with \<open>coprime b c\<close> have "b dvd a"
   1.778 +    by (simp add: coprime_dvd_mult_left_iff normalize_mult [symmetric])
   1.779 +  from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b"
   1.780 +    by (auto intro: dvdI dest: sym simp add: mult.commute)
   1.781 +  with \<open>coprime b c\<close> have "c dvd d"
   1.782 +    by (simp add: coprime_dvd_mult_left_iff coprime_commute normalize_mult [symmetric])
   1.783 +  from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a"
   1.784 +    by (auto intro: dvdI dest: sym simp add: mult.commute)
   1.785 +  with \<open>coprime a d\<close> have "d dvd c"
   1.786 +    by (simp add: coprime_dvd_mult_left_iff coprime_commute normalize_mult [symmetric])
   1.787 +  from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b"
   1.788 +    by (rule associatedI)
   1.789 +  moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d"
   1.790 +    by (rule associatedI)
   1.791 +  ultimately show ?rhs ..
   1.792 +qed
   1.793 +
   1.794 +lemma coprime_crossproduct':
   1.795 +  fixes a b c d
   1.796 +  assumes "b \<noteq> 0"
   1.797 +  assumes unit_factors: "unit_factor b = unit_factor d"
   1.798 +  assumes coprime: "coprime a b" "coprime c d"
   1.799 +  shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
   1.800 +proof safe
   1.801 +  assume eq: "a * d = b * c"
   1.802 +  hence "normalize a * normalize d = normalize c * normalize b"
   1.803 +    by (simp only: normalize_mult [symmetric] mult_ac)
   1.804 +  with coprime have "normalize b = normalize d"
   1.805 +    by (subst (asm) coprime_crossproduct) simp_all
   1.806 +  from this and unit_factors show "b = d"
   1.807 +    by (rule normalize_unit_factor_eqI)
   1.808 +  from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
   1.809 +  with \<open>b \<noteq> 0\<close> \<open>b = d\<close> show "a = c" by simp
   1.810 +qed (simp_all add: mult_ac)
   1.811 +
   1.812 +lemma gcd_mult_left_left_cancel:
   1.813 +  "gcd (c * a) b = gcd a b" if "coprime b c"
   1.814 +proof -
   1.815 +  have "coprime (gcd b (a * c)) c"
   1.816 +    by (rule coprimeI) (auto intro: that coprime_common_divisor)
   1.817 +  then have "gcd b (a * c) dvd a"
   1.818 +    using coprime_dvd_mult_left_iff [of "gcd b (a * c)" c a]
   1.819 +    by simp
   1.820 +  then show ?thesis
   1.821 +    by (auto intro: associated_eqI simp add: ac_simps)
   1.822 +qed
   1.823 +
   1.824 +lemma gcd_mult_left_right_cancel:
   1.825 +  "gcd (a * c) b = gcd a b" if "coprime b c"
   1.826 +  using that gcd_mult_left_left_cancel [of b c a]
   1.827 +  by (simp add: ac_simps)
   1.828 +
   1.829 +lemma gcd_mult_right_left_cancel:
   1.830 +  "gcd a (c * b) = gcd a b" if "coprime a c"
   1.831 +  using that gcd_mult_left_left_cancel [of a c b]
   1.832 +  by (simp add: ac_simps)
   1.833 +
   1.834 +lemma gcd_mult_right_right_cancel:
   1.835 +  "gcd a (b * c) = gcd a b" if "coprime a c"
   1.836 +  using that gcd_mult_right_left_cancel [of a c b]
   1.837 +  by (simp add: ac_simps)
   1.838 +
   1.839 +lemma gcd_exp [simp]:
   1.840 +  "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
   1.841 +proof (cases "a = 0 \<and> b = 0 \<or> n = 0")
   1.842 +  case True
   1.843 +  then show ?thesis
   1.844 +    by (cases n) simp_all
   1.845 +next
   1.846 +  case False
   1.847 +  then have "coprime (a div gcd a b) (b div gcd a b)" and "n > 0"
   1.848 +    by (auto intro: div_gcd_coprime)
   1.849 +  then have "coprime ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
   1.850 +    by simp
   1.851 +  then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
   1.852 +    by simp
   1.853 +  then have "gcd a b ^ n = gcd a b ^ n * \<dots>"
   1.854 +    by simp
   1.855 +  also note gcd_mult_distrib
   1.856 +  also have "unit_factor (gcd a b ^ n) = 1"
   1.857 +    using False by (auto simp add: unit_factor_power unit_factor_gcd)
   1.858 +  also have "(gcd a b) ^ n * (a div gcd a b) ^ n = a ^ n"
   1.859 +    by (simp add: ac_simps div_power dvd_power_same)
   1.860 +  also have "(gcd a b) ^ n * (b div gcd a b) ^ n = b ^ n"
   1.861 +    by (simp add: ac_simps div_power dvd_power_same)
   1.862 +  finally show ?thesis by simp
   1.863 +qed
   1.864 +
   1.865 +lemma division_decomp:
   1.866 +  assumes "a dvd b * c"
   1.867 +  shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   1.868 +proof (cases "gcd a b = 0")
   1.869 +  case True
   1.870 +  then have "a = 0 \<and> b = 0"
   1.871 +    by simp
   1.872 +  then have "a = 0 * c \<and> 0 dvd b \<and> c dvd c"
   1.873 +    by simp
   1.874 +  then show ?thesis by blast
   1.875 +next
   1.876 +  case False
   1.877 +  let ?d = "gcd a b"
   1.878 +  from gcd_coprime_exists [OF False]
   1.879 +    obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "coprime a' b'"
   1.880 +    by blast
   1.881 +  from ab'(1) have "a' dvd a" ..
   1.882 +  with assms have "a' dvd b * c"
   1.883 +    using dvd_trans [of a' a "b * c"] by simp
   1.884 +  from assms ab'(1,2) have "a' * ?d dvd (b' * ?d) * c"
   1.885 +    by simp
   1.886 +  then have "?d * a' dvd ?d * (b' * c)"
   1.887 +    by (simp add: mult_ac)
   1.888 +  with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c"
   1.889 +    by simp
   1.890 +  then have "a' dvd c"
   1.891 +    using \<open>coprime a' b'\<close> by (simp add: coprime_dvd_mult_right_iff)
   1.892 +  with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c"
   1.893 +    by (simp add: ac_simps)
   1.894 +  then show ?thesis by blast
   1.895 +qed
   1.896 +
   1.897 +lemma lcm_coprime: "coprime a b \<Longrightarrow> lcm a b = normalize (a * b)"
   1.898 +  by (subst lcm_gcd) simp
   1.899 +
   1.900 +end
   1.901 +
   1.902 +context ring_gcd
   1.903 +begin
   1.904 +
   1.905 +lemma coprime_minus_left_iff [simp]:
   1.906 +  "coprime (- a) b \<longleftrightarrow> coprime a b"
   1.907 +  by (rule; rule coprimeI) (auto intro: coprime_common_divisor)
   1.908 +
   1.909 +lemma coprime_minus_right_iff [simp]:
   1.910 +  "coprime a (- b) \<longleftrightarrow> coprime a b"
   1.911 +  using coprime_minus_left_iff [of b a] by (simp add: ac_simps)
   1.912 +
   1.913 +lemma coprime_diff_one_left [simp]: "coprime (a - 1) a"
   1.914 +  using coprime_add_one_right [of "a - 1"] by simp
   1.915 +
   1.916 +lemma coprime_doff_one_right [simp]: "coprime a (a - 1)"
   1.917 +  using coprime_diff_one_left [of a] by (simp add: ac_simps)
   1.918 +
   1.919 +end
   1.920 +
   1.921 +context semiring_Gcd
   1.922 +begin
   1.923 +
   1.924 +lemma Lcm_coprime:
   1.925 +  assumes "finite A"
   1.926 +    and "A \<noteq> {}"
   1.927 +    and "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> coprime a b"
   1.928 +  shows "Lcm A = normalize (\<Prod>A)"
   1.929 +  using assms
   1.930 +proof (induct rule: finite_ne_induct)
   1.931 +  case singleton
   1.932 +  then show ?case by simp
   1.933 +next
   1.934 +  case (insert a A)
   1.935 +  have "Lcm (insert a A) = lcm a (Lcm A)"
   1.936 +    by simp
   1.937 +  also from insert have "Lcm A = normalize (\<Prod>A)"
   1.938 +    by blast
   1.939 +  also have "lcm a \<dots> = lcm a (\<Prod>A)"
   1.940 +    by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
   1.941 +  also from insert have "coprime a (\<Prod>A)"
   1.942 +    by (subst coprime_commute, intro prod_coprime_left) auto
   1.943 +  with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
   1.944 +    by (simp add: lcm_coprime)
   1.945 +  finally show ?case .
   1.946 +qed
   1.947 +
   1.948 +lemma Lcm_coprime':
   1.949 +  "card A \<noteq> 0 \<Longrightarrow>
   1.950 +    (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> coprime a b) \<Longrightarrow>
   1.951 +    Lcm A = normalize (\<Prod>A)"
   1.952 +  by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
   1.953 +
   1.954 +end
   1.955 +
   1.956 +
   1.957  subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
   1.958  
   1.959  instantiation nat :: gcd
   1.960 @@ -1716,9 +1767,6 @@
   1.961     apply simp_all
   1.962    done
   1.963  
   1.964 -
   1.965 -text \<open>Specific to \<open>int\<close>.\<close>
   1.966 -
   1.967  lemma gcd_eq_int_iff: "gcd k l = int n \<longleftrightarrow> gcd (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
   1.968    by (simp add: gcd_int_def)
   1.969  
   1.970 @@ -1949,19 +1997,6 @@
   1.971    for k m n :: int
   1.972    by (simp add: gcd_int_def abs_mult nat_mult_distrib gcd_mult_distrib_nat [symmetric])
   1.973  
   1.974 -lemma coprime_crossproduct_nat:
   1.975 -  fixes a b c d :: nat
   1.976 -  assumes "coprime a d" and "coprime b c"
   1.977 -  shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d"
   1.978 -  using assms coprime_crossproduct [of a d b c] by simp
   1.979 -
   1.980 -lemma coprime_crossproduct_int:
   1.981 -  fixes a b c d :: int
   1.982 -  assumes "coprime a d" and "coprime b c"
   1.983 -  shows "\<bar>a\<bar> * \<bar>c\<bar> = \<bar>b\<bar> * \<bar>d\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>b\<bar> \<and> \<bar>c\<bar> = \<bar>d\<bar>"
   1.984 -  using assms coprime_crossproduct [of a d b c] by simp
   1.985 -
   1.986 -
   1.987  text \<open>\medskip Addition laws.\<close>
   1.988  
   1.989  (* TODO: add the other variations? *)
   1.990 @@ -2064,53 +2099,33 @@
   1.991    for k l :: int
   1.992    by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
   1.993  
   1.994 -
   1.995 -subsection \<open>Coprimality\<close>
   1.996 -
   1.997 -lemma coprime_nat: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   1.998 -  for a b :: nat
   1.999 -  using coprime [of a b] by simp
  1.1000 -
  1.1001 -lemma coprime_Suc_0_nat: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
  1.1002 -  for a b :: nat
  1.1003 -  using coprime_nat by simp
  1.1004 -
  1.1005 -lemma coprime_int: "coprime a b \<longleftrightarrow> (\<forall>d. d \<ge> 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
  1.1006 -  for a b :: int
  1.1007 -  using gcd_unique_int [of 1 a b]
  1.1008 -  apply clarsimp
  1.1009 -  apply (erule subst)
  1.1010 -  apply (rule iffI)
  1.1011 -   apply force
  1.1012 -  using abs_dvd_iff abs_ge_zero apply blast
  1.1013 -  done
  1.1014 -
  1.1015 -lemma pow_divides_eq_nat [simp]: "n > 0 \<Longrightarrow> a^n dvd b^n \<longleftrightarrow> a dvd b"
  1.1016 -  for a b n :: nat
  1.1017 -  using pow_divs_eq[of n] by simp
  1.1018 -
  1.1019 -lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
  1.1020 -  using coprime_plus_one[of n] by simp
  1.1021 -
  1.1022 -lemma coprime_minus_one_nat: "n \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
  1.1023 -  for n :: nat
  1.1024 -  using coprime_Suc_nat [of "n - 1"] gcd.commute [of "n - 1" n] by auto
  1.1025 -
  1.1026 -lemma coprime_common_divisor_nat: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
  1.1027 -  for a b :: nat
  1.1028 -  by (metis gcd_greatest_iff nat_dvd_1_iff_1)
  1.1029 -
  1.1030 -lemma coprime_common_divisor_int: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
  1.1031 -  for a b :: int
  1.1032 -  using gcd_greatest_iff [of x a b] by auto
  1.1033 -
  1.1034 -lemma invertible_coprime_nat: "x * y mod m = 1 \<Longrightarrow> coprime x m"
  1.1035 -  for m x y :: nat
  1.1036 -  by (metis coprime_lmult gcd_1_nat gcd.commute gcd_red_nat)
  1.1037 -
  1.1038 -lemma invertible_coprime_int: "x * y mod m = 1 \<Longrightarrow> coprime x m"
  1.1039 -  for m x y :: int
  1.1040 -  by (metis coprime_lmult gcd_1_int gcd.commute gcd_red_int)
  1.1041 +lemma coprime_Suc_left_nat [simp]:
  1.1042 +  "coprime (Suc n) n"
  1.1043 +  using coprime_add_one_left [of n] by simp
  1.1044 +
  1.1045 +lemma coprime_Suc_right_nat [simp]:
  1.1046 +  "coprime n (Suc n)"
  1.1047 +  using coprime_Suc_left_nat [of n] by (simp add: ac_simps)
  1.1048 +
  1.1049 +lemma coprime_diff_one_left_nat [simp]:
  1.1050 +  "coprime (n - 1) n" if "n > 0" for n :: nat
  1.1051 +  using that coprime_Suc_right_nat [of "n - 1"] by simp
  1.1052 +
  1.1053 +lemma coprime_diff_one_right_nat [simp]:
  1.1054 +  "coprime n (n - 1)" if "n > 0" for n :: nat
  1.1055 +  using that coprime_diff_one_left_nat [of n] by (simp add: ac_simps)
  1.1056 +
  1.1057 +lemma coprime_crossproduct_nat:
  1.1058 +  fixes a b c d :: nat
  1.1059 +  assumes "coprime a d" and "coprime b c"
  1.1060 +  shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d"
  1.1061 +  using assms coprime_crossproduct [of a d b c] by simp
  1.1062 +
  1.1063 +lemma coprime_crossproduct_int:
  1.1064 +  fixes a b c d :: int
  1.1065 +  assumes "coprime a d" and "coprime b c"
  1.1066 +  shows "\<bar>a\<bar> * \<bar>c\<bar> = \<bar>b\<bar> * \<bar>d\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>b\<bar> \<and> \<bar>c\<bar> = \<bar>d\<bar>"
  1.1067 +  using assms coprime_crossproduct [of a d b c] by simp
  1.1068  
  1.1069  
  1.1070  subsection \<open>Bezout's theorem\<close>
  1.1071 @@ -2742,14 +2757,6 @@
  1.1072    for i m n :: int
  1.1073    by (fact dvd_lcmI2)
  1.1074  
  1.1075 -lemma coprime_exp2_nat [intro]: "coprime a b \<Longrightarrow> coprime (a^n) (b^m)"
  1.1076 -  for a b :: nat
  1.1077 -  by (fact coprime_exp2)
  1.1078 -
  1.1079 -lemma coprime_exp2_int [intro]: "coprime a b \<Longrightarrow> coprime (a^n) (b^m)"
  1.1080 -  for a b :: int
  1.1081 -  by (fact coprime_exp2)
  1.1082 -
  1.1083  lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
  1.1084  lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
  1.1085  lemmas Gcd_greatest_nat [simp] = Gcd_greatest [where ?'a = nat]