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]
```