src/HOL/GCD.thy
changeset 62429 25271ff79171
parent 62353 7f927120b5a2
child 63025 92680537201f
     1.1 --- a/src/HOL/GCD.thy	Fri Feb 26 18:33:01 2016 +0100
     1.2 +++ b/src/HOL/GCD.thy	Fri Feb 26 22:15:09 2016 +0100
     1.3 @@ -395,10 +395,549 @@
     1.4  lemma mult_lcm_right:
     1.5    "lcm a b * c = lcm (a * c) (b * c) * unit_factor c"
     1.6    using mult_lcm_left [of c a b] by (simp add: ac_simps)
     1.7 +
     1.8 +lemma gcdI:
     1.9 +  assumes "c dvd a" and "c dvd b" and greatest: "\<And>d. d dvd a \<Longrightarrow> d dvd b \<Longrightarrow> d dvd c"
    1.10 +    and "normalize c = c"
    1.11 +  shows "c = gcd a b"
    1.12 +  by (rule associated_eqI) (auto simp: assms intro: gcd_greatest)
    1.13 +
    1.14 +lemma gcd_unique: "d dvd a \<and> d dvd b \<and> 
    1.15 +    normalize d = d \<and>
    1.16 +    (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
    1.17 +  by rule (auto intro: gcdI simp: gcd_greatest)
    1.18 +
    1.19 +lemma gcd_dvd_prod: "gcd a b dvd k * b"
    1.20 +  using mult_dvd_mono [of 1] by auto
    1.21 +
    1.22 +lemma gcd_proj2_if_dvd: "b dvd a \<Longrightarrow> gcd a b = normalize b"
    1.23 +  by (rule gcdI [symmetric]) simp_all
    1.24 +
    1.25 +lemma gcd_proj1_if_dvd: "a dvd b \<Longrightarrow> gcd a b = normalize a"
    1.26 +  by (rule gcdI [symmetric]) simp_all
    1.27 +
    1.28 +lemma gcd_proj1_iff: "gcd m n = normalize m \<longleftrightarrow> m dvd n"
    1.29 +proof
    1.30 +  assume A: "gcd m n = normalize m"
    1.31 +  show "m dvd n"
    1.32 +  proof (cases "m = 0")
    1.33 +    assume [simp]: "m \<noteq> 0"
    1.34 +    from A have B: "m = gcd m n * unit_factor m"
    1.35 +      by (simp add: unit_eq_div2)
    1.36 +    show ?thesis by (subst B, simp add: mult_unit_dvd_iff)
    1.37 +  qed (insert A, simp)
    1.38 +next
    1.39 +  assume "m dvd n"
    1.40 +  then show "gcd m n = normalize m" by (rule gcd_proj1_if_dvd)
    1.41 +qed
    1.42    
    1.43 +lemma gcd_proj2_iff: "gcd m n = normalize n \<longleftrightarrow> n dvd m"
    1.44 +  using gcd_proj1_iff [of n m] by (simp add: ac_simps)
    1.45 +
    1.46 +lemma gcd_mult_distrib': "normalize c * gcd a b = gcd (c * a) (c * b)"
    1.47 +  by (rule gcdI) (auto simp: normalize_mult gcd_greatest mult_dvd_mono gcd_mult_left[symmetric])
    1.48 +
    1.49 +lemma gcd_mult_distrib:
    1.50 +  "k * gcd a b = gcd (k * a) (k * b) * unit_factor k"
    1.51 +proof-
    1.52 +  have "normalize k * gcd a b = gcd (k * a) (k * b)"
    1.53 +    by (simp add: gcd_mult_distrib')
    1.54 +  then have "normalize k * gcd a b * unit_factor k = gcd (k * a) (k * b) * unit_factor k"
    1.55 +    by simp
    1.56 +  then have "normalize k * unit_factor k * gcd a b  = gcd (k * a) (k * b) * unit_factor k"
    1.57 +    by (simp only: ac_simps)
    1.58 +  then show ?thesis
    1.59 +    by simp
    1.60 +qed
    1.61 +
    1.62 +lemma lcm_mult_unit1:
    1.63 +  "is_unit a \<Longrightarrow> lcm (b * a) c = lcm b c"
    1.64 +  by (rule associated_eqI) (simp_all add: mult_unit_dvd_iff dvd_lcmI1)
    1.65 +
    1.66 +lemma lcm_mult_unit2:
    1.67 +  "is_unit a \<Longrightarrow> lcm b (c * a) = lcm b c"
    1.68 +  using lcm_mult_unit1 [of a c b] by (simp add: ac_simps)
    1.69 +
    1.70 +lemma lcm_div_unit1:
    1.71 +  "is_unit a \<Longrightarrow> lcm (b div a) c = lcm b c"
    1.72 +  by (erule is_unitE [of _ b]) (simp add: lcm_mult_unit1) 
    1.73 +
    1.74 +lemma lcm_div_unit2:
    1.75 +  "is_unit a \<Longrightarrow> lcm b (c div a) = lcm b c"
    1.76 +  by (erule is_unitE [of _ c]) (simp add: lcm_mult_unit2)
    1.77 +
    1.78 +lemma normalize_lcm_left [simp]:
    1.79 +  "lcm (normalize a) b = lcm a b"
    1.80 +proof (cases "a = 0")
    1.81 +  case True then show ?thesis
    1.82 +    by simp
    1.83 +next
    1.84 +  case False then have "is_unit (unit_factor a)"
    1.85 +    by simp
    1.86 +  moreover have "normalize a = a div unit_factor a"
    1.87 +    by simp
    1.88 +  ultimately show ?thesis
    1.89 +    by (simp only: lcm_div_unit1)
    1.90 +qed
    1.91 +
    1.92 +lemma normalize_lcm_right [simp]:
    1.93 +  "lcm a (normalize b) = lcm a b"
    1.94 +  using normalize_lcm_left [of b a] by (simp add: ac_simps)
    1.95 +
    1.96 +lemma gcd_mult_unit1: "is_unit a \<Longrightarrow> gcd (b * a) c = gcd b c"
    1.97 +  apply (rule gcdI)
    1.98 +  apply simp_all
    1.99 +  apply (rule dvd_trans, rule gcd_dvd1, simp add: unit_simps)
   1.100 +  done
   1.101 +
   1.102 +lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c"
   1.103 +  by (subst gcd.commute, subst gcd_mult_unit1, assumption, rule gcd.commute)
   1.104 +
   1.105 +lemma gcd_div_unit1: "is_unit a \<Longrightarrow> gcd (b div a) c = gcd b c"
   1.106 +  by (erule is_unitE [of _ b]) (simp add: gcd_mult_unit1)
   1.107 +
   1.108 +lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c"
   1.109 +  by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2)
   1.110 +
   1.111 +lemma normalize_gcd_left [simp]:
   1.112 +  "gcd (normalize a) b = gcd a b"
   1.113 +proof (cases "a = 0")
   1.114 +  case True then show ?thesis
   1.115 +    by simp
   1.116 +next
   1.117 +  case False then have "is_unit (unit_factor a)"
   1.118 +    by simp
   1.119 +  moreover have "normalize a = a div unit_factor a"
   1.120 +    by simp
   1.121 +  ultimately show ?thesis
   1.122 +    by (simp only: gcd_div_unit1)
   1.123 +qed
   1.124 +
   1.125 +lemma normalize_gcd_right [simp]:
   1.126 +  "gcd a (normalize b) = gcd a b"
   1.127 +  using normalize_gcd_left [of b a] by (simp add: ac_simps)
   1.128 +
   1.129 +lemma comp_fun_idem_gcd: "comp_fun_idem gcd"
   1.130 +  by standard (simp_all add: fun_eq_iff ac_simps)
   1.131 +
   1.132 +lemma comp_fun_idem_lcm: "comp_fun_idem lcm"
   1.133 +  by standard (simp_all add: fun_eq_iff ac_simps)
   1.134 +
   1.135 +lemma gcd_dvd_antisym:
   1.136 +  "gcd a b dvd gcd c d \<Longrightarrow> gcd c d dvd gcd a b \<Longrightarrow> gcd a b = gcd c d"
   1.137 +proof (rule gcdI)
   1.138 +  assume A: "gcd a b dvd gcd c d" and B: "gcd c d dvd gcd a b"
   1.139 +  have "gcd c d dvd c" by simp
   1.140 +  with A show "gcd a b dvd c" by (rule dvd_trans)
   1.141 +  have "gcd c d dvd d" by simp
   1.142 +  with A show "gcd a b dvd d" by (rule dvd_trans)
   1.143 +  show "normalize (gcd a b) = gcd a b"
   1.144 +    by simp
   1.145 +  fix l assume "l dvd c" and "l dvd d"
   1.146 +  hence "l dvd gcd c d" by (rule gcd_greatest)
   1.147 +  from this and B show "l dvd gcd a b" by (rule dvd_trans)
   1.148 +qed
   1.149 +
   1.150 +lemma coprime_dvd_mult:
   1.151 +  assumes "coprime a b" and "a dvd c * b"
   1.152 +  shows "a dvd c"
   1.153 +proof (cases "c = 0")
   1.154 +  case True then show ?thesis by simp
   1.155 +next
   1.156 +  case False
   1.157 +  then have unit: "is_unit (unit_factor c)" by simp
   1.158 +  from \<open>coprime a b\<close> mult_gcd_left [of c a b]
   1.159 +  have "gcd (c * a) (c * b) * unit_factor c = c"
   1.160 +    by (simp add: ac_simps)
   1.161 +  moreover from \<open>a dvd c * b\<close> have "a dvd gcd (c * a) (c * b) * unit_factor c"
   1.162 +    by (simp add: dvd_mult_unit_iff unit)
   1.163 +  ultimately show ?thesis by simp
   1.164 +qed
   1.165 +
   1.166 +lemma coprime_dvd_mult_iff:
   1.167 +  assumes "coprime a c"
   1.168 +  shows "a dvd b * c \<longleftrightarrow> a dvd b"
   1.169 +  using assms by (auto intro: coprime_dvd_mult)
   1.170 +
   1.171 +lemma gcd_mult_cancel:
   1.172 +  "coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b"
   1.173 +  apply (rule associated_eqI)
   1.174 +  apply (rule gcd_greatest)
   1.175 +  apply (rule_tac b = c in coprime_dvd_mult)
   1.176 +  apply (simp add: gcd.assoc)
   1.177 +  apply (simp_all add: ac_simps)
   1.178 +  done
   1.179 +
   1.180 +lemma coprime_crossproduct:
   1.181 +  fixes a b c d
   1.182 +  assumes "coprime a d" and "coprime b c"
   1.183 +  shows "normalize a * normalize c = normalize b * normalize d
   1.184 +    \<longleftrightarrow> normalize a = normalize b \<and> normalize c = normalize d" (is "?lhs \<longleftrightarrow> ?rhs")
   1.185 +proof
   1.186 +  assume ?rhs then show ?lhs by simp
   1.187 +next
   1.188 +  assume ?lhs
   1.189 +  from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
   1.190 +    by (auto intro: dvdI dest: sym)
   1.191 +  with \<open>coprime a d\<close> have "a dvd b"
   1.192 +    by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
   1.193 +  from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c"
   1.194 +    by (auto intro: dvdI dest: sym)
   1.195 +  with \<open>coprime b c\<close> have "b dvd a"
   1.196 +    by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
   1.197 +  from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b"
   1.198 +    by (auto intro: dvdI dest: sym simp add: mult.commute)
   1.199 +  with \<open>coprime b c\<close> have "c dvd d"
   1.200 +    by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
   1.201 +  from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a"
   1.202 +    by (auto intro: dvdI dest: sym simp add: mult.commute)
   1.203 +  with \<open>coprime a d\<close> have "d dvd c"
   1.204 +    by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
   1.205 +  from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b"
   1.206 +    by (rule associatedI)
   1.207 +  moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d"
   1.208 +    by (rule associatedI)
   1.209 +  ultimately show ?rhs ..
   1.210 +qed
   1.211 +
   1.212 +lemma gcd_add1 [simp]: "gcd (m + n) n = gcd m n"
   1.213 +  by (rule gcdI [symmetric]) (simp_all add: dvd_add_left_iff)
   1.214 +
   1.215 +lemma gcd_add2 [simp]: "gcd m (m + n) = gcd m n"
   1.216 +  using gcd_add1 [of n m] by (simp add: ac_simps)
   1.217 +
   1.218 +lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
   1.219 +  by (rule gcdI [symmetric]) (simp_all add: dvd_add_right_iff)
   1.220 +
   1.221 +lemma coprimeI: "(\<And>l. \<lbrakk>l dvd a; l dvd b\<rbrakk> \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd a b = 1"
   1.222 +  by (rule sym, rule gcdI, simp_all)
   1.223 +
   1.224 +lemma coprime: "gcd a b = 1 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)"
   1.225 +  by (auto intro: coprimeI gcd_greatest dvd_gcdD1 dvd_gcdD2)
   1.226 +
   1.227 +lemma div_gcd_coprime:
   1.228 +  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
   1.229 +  shows "coprime (a div gcd a b) (b div gcd a b)"
   1.230 +proof -
   1.231 +  let ?g = "gcd a b"
   1.232 +  let ?a' = "a div ?g"
   1.233 +  let ?b' = "b div ?g"
   1.234 +  let ?g' = "gcd ?a' ?b'"
   1.235 +  have dvdg: "?g dvd a" "?g dvd b" by simp_all
   1.236 +  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
   1.237 +  from dvdg dvdg' obtain ka kb ka' kb' where
   1.238 +      kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
   1.239 +    unfolding dvd_def by blast
   1.240 +  from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
   1.241 +    by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
   1.242 +  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   1.243 +    by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
   1.244 +      dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   1.245 +  have "?g \<noteq> 0" using nz by simp
   1.246 +  moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   1.247 +  thm dvd_mult_cancel_left
   1.248 +  ultimately show ?thesis using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
   1.249 +qed
   1.250 +
   1.251 +
   1.252 +lemma divides_mult:
   1.253 +  assumes "a dvd c" and nr: "b dvd c" and "coprime a b"
   1.254 +  shows "a * b dvd c"
   1.255 +proof-
   1.256 +  from \<open>b dvd c\<close> obtain b' where"c = b * b'" ..
   1.257 +  with \<open>a dvd c\<close> have "a dvd b' * b"
   1.258 +    by (simp add: ac_simps)
   1.259 +  with \<open>coprime a b\<close> have "a dvd b'"
   1.260 +    by (simp add: coprime_dvd_mult_iff)
   1.261 +  then obtain a' where "b' = a * a'" ..
   1.262 +  with \<open>c = b * b'\<close> have "c = (a * b) * a'"
   1.263 +    by (simp add: ac_simps)
   1.264 +  then show ?thesis ..
   1.265 +qed
   1.266 +
   1.267 +lemma coprime_lmult:
   1.268 +  assumes dab: "gcd d (a * b) = 1" 
   1.269 +  shows "gcd d a = 1"
   1.270 +proof (rule coprimeI)
   1.271 +  fix l assume "l dvd d" and "l dvd a"
   1.272 +  hence "l dvd a * b" by simp
   1.273 +  with \<open>l dvd d\<close> and dab show "l dvd 1" by (auto intro: gcd_greatest)
   1.274 +qed
   1.275 +
   1.276 +lemma coprime_rmult:
   1.277 +  assumes dab: "gcd d (a * b) = 1"
   1.278 +  shows "gcd d b = 1"
   1.279 +proof (rule coprimeI)
   1.280 +  fix l assume "l dvd d" and "l dvd b"
   1.281 +  hence "l dvd a * b" by simp
   1.282 +  with \<open>l dvd d\<close> and dab show "l dvd 1" by (auto intro: gcd_greatest)
   1.283 +qed
   1.284 +
   1.285 +lemma coprime_mult:
   1.286 +  assumes da: "coprime d a" and db: "coprime d b"
   1.287 +  shows "coprime d (a * b)"
   1.288 +  apply (subst gcd.commute)
   1.289 +  using da apply (subst gcd_mult_cancel)
   1.290 +  apply (subst gcd.commute, assumption)
   1.291 +  apply (subst gcd.commute, rule db)
   1.292 +  done
   1.293 +
   1.294 +lemma coprime_mul_eq: "gcd d (a * b) = 1 \<longleftrightarrow> gcd d a = 1 \<and> gcd d b = 1"
   1.295 +  using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b] by blast
   1.296 +
   1.297 +lemma gcd_coprime:
   1.298 +  assumes c: "gcd a b \<noteq> 0" and a: "a = a' * gcd a b" and b: "b = b' * gcd a b"
   1.299 +  shows "gcd a' b' = 1"
   1.300 +proof -
   1.301 +  from c have "a \<noteq> 0 \<or> b \<noteq> 0" by simp
   1.302 +  with div_gcd_coprime have "gcd (a div gcd a b) (b div gcd a b) = 1" .
   1.303 +  also from assms have "a div gcd a b = a'" using dvd_div_eq_mult local.gcd_dvd1 by blast
   1.304 +  also from assms have "b div gcd a b = b'" using dvd_div_eq_mult local.gcd_dvd1 by blast
   1.305 +  finally show ?thesis .
   1.306 +qed
   1.307 +
   1.308 +lemma coprime_power:
   1.309 +  assumes "0 < n"
   1.310 +  shows "gcd a (b ^ n) = 1 \<longleftrightarrow> gcd a b = 1"
   1.311 +using assms proof (induct n)
   1.312 +  case (Suc n) then show ?case
   1.313 +    by (cases n) (simp_all add: coprime_mul_eq)
   1.314 +qed simp
   1.315 +
   1.316 +lemma gcd_coprime_exists:
   1.317 +  assumes nz: "gcd a b \<noteq> 0"
   1.318 +  shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> gcd a' b' = 1"
   1.319 +  apply (rule_tac x = "a div gcd a b" in exI)
   1.320 +  apply (rule_tac x = "b div gcd a b" in exI)
   1.321 +  apply (insert nz, auto intro: div_gcd_coprime)
   1.322 +  done
   1.323 +
   1.324 +lemma coprime_exp:
   1.325 +  "gcd d a = 1 \<Longrightarrow> gcd d (a^n) = 1"
   1.326 +  by (induct n, simp_all add: coprime_mult)
   1.327 +
   1.328 +lemma coprime_exp_left:
   1.329 +  assumes "coprime a b"
   1.330 +  shows "coprime (a ^ n) b"
   1.331 +  using assms by (induct n) (simp_all add: gcd_mult_cancel)
   1.332 +
   1.333 +lemma coprime_exp2:
   1.334 +  assumes "coprime a b"
   1.335 +  shows "coprime (a ^ n) (b ^ m)"
   1.336 +proof (rule coprime_exp_left)
   1.337 +  from assms show "coprime a (b ^ m)"
   1.338 +    by (induct m) (simp_all add: gcd_mult_cancel gcd.commute [of a])
   1.339 +qed
   1.340 +
   1.341 +lemma gcd_exp:
   1.342 +  "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
   1.343 +proof (cases "a = 0 \<and> b = 0")
   1.344 +  case True
   1.345 +  then show ?thesis by (cases n) simp_all
   1.346 +next
   1.347 +  case False
   1.348 +  then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
   1.349 +    using coprime_exp2[OF div_gcd_coprime[of a b], of n n, symmetric] by simp
   1.350 +  then have "gcd a b ^ n = gcd a b ^ n * ..." by simp
   1.351 +  also note gcd_mult_distrib
   1.352 +  also have "unit_factor (gcd a b ^ n) = 1"
   1.353 +    using False by (auto simp add: unit_factor_power unit_factor_gcd)
   1.354 +  also have "(gcd a b)^n * (a div gcd a b)^n = a^n"
   1.355 +    by (subst ac_simps, subst div_power, simp, rule dvd_div_mult_self, rule dvd_power_same, simp)
   1.356 +  also have "(gcd a b)^n * (b div gcd a b)^n = b^n"
   1.357 +    by (subst ac_simps, subst div_power, simp, rule dvd_div_mult_self, rule dvd_power_same, simp)
   1.358 +  finally show ?thesis by simp
   1.359 +qed
   1.360 +
   1.361 +lemma coprime_common_divisor: 
   1.362 +  "gcd a b = 1 \<Longrightarrow> a dvd a \<Longrightarrow> a dvd b \<Longrightarrow> is_unit a"
   1.363 +  apply (subgoal_tac "a dvd gcd a b")
   1.364 +  apply simp
   1.365 +  apply (erule (1) gcd_greatest)
   1.366 +  done
   1.367 +
   1.368 +lemma division_decomp: 
   1.369 +  assumes dc: "a dvd b * c"
   1.370 +  shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
   1.371 +proof (cases "gcd a b = 0")
   1.372 +  assume "gcd a b = 0"
   1.373 +  hence "a = 0 \<and> b = 0" by simp
   1.374 +  hence "a = 0 * c \<and> 0 dvd b \<and> c dvd c" by simp
   1.375 +  then show ?thesis by blast
   1.376 +next
   1.377 +  let ?d = "gcd a b"
   1.378 +  assume "?d \<noteq> 0"
   1.379 +  from gcd_coprime_exists[OF this]
   1.380 +    obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
   1.381 +    by blast
   1.382 +  from ab'(1) have "a' dvd a" unfolding dvd_def by blast
   1.383 +  with dc have "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
   1.384 +  from dc ab'(1,2) have "a'*?d dvd (b'*?d) * c" by simp
   1.385 +  hence "?d * a' dvd ?d * (b' * c)" by (simp add: mult_ac)
   1.386 +  with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c" by simp
   1.387 +  with coprime_dvd_mult[OF ab'(3)] 
   1.388 +    have "a' dvd c" by (subst (asm) ac_simps, blast)
   1.389 +  with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c" by (simp add: mult_ac)
   1.390 +  then show ?thesis by blast
   1.391 +qed
   1.392 +
   1.393 +lemma pow_divs_pow:
   1.394 +  assumes ab: "a ^ n dvd b ^ n" and n: "n \<noteq> 0"
   1.395 +  shows "a dvd b"
   1.396 +proof (cases "gcd a b = 0")
   1.397 +  assume "gcd a b = 0"
   1.398 +  then show ?thesis by simp
   1.399 +next
   1.400 +  let ?d = "gcd a b"
   1.401 +  assume "?d \<noteq> 0"
   1.402 +  from n obtain m where m: "n = Suc m" by (cases n, simp_all)
   1.403 +  from \<open>?d \<noteq> 0\<close> have zn: "?d ^ n \<noteq> 0" by (rule power_not_zero)
   1.404 +  from gcd_coprime_exists[OF \<open>?d \<noteq> 0\<close>]
   1.405 +    obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
   1.406 +    by blast
   1.407 +  from ab have "(a' * ?d) ^ n dvd (b' * ?d) ^ n"
   1.408 +    by (simp add: ab'(1,2)[symmetric])
   1.409 +  hence "?d^n * a'^n dvd ?d^n * b'^n"
   1.410 +    by (simp only: power_mult_distrib ac_simps)
   1.411 +  with zn have "a'^n dvd b'^n" by simp
   1.412 +  hence "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m)
   1.413 +  hence "a' dvd b'^m * b'" by (simp add: m ac_simps)
   1.414 +  with coprime_dvd_mult[OF coprime_exp[OF ab'(3), of m]]
   1.415 +    have "a' dvd b'" by (subst (asm) ac_simps, blast)
   1.416 +  hence "a'*?d dvd b'*?d" by (rule mult_dvd_mono, simp)
   1.417 +  with ab'(1,2) show ?thesis by simp
   1.418 +qed
   1.419 +
   1.420 +lemma pow_divs_eq [simp]:
   1.421 +  "n \<noteq> 0 \<Longrightarrow> a ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
   1.422 +  by (auto intro: pow_divs_pow dvd_power_same)
   1.423 +
   1.424 +lemma coprime_plus_one [simp]: "gcd (n + 1) n = 1"
   1.425 +  by (subst add_commute, simp)
   1.426 +
   1.427 +lemma setprod_coprime [rule_format]:
   1.428 +  "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
   1.429 +  apply (cases "finite A")
   1.430 +  apply (induct set: finite)
   1.431 +  apply (auto simp add: gcd_mult_cancel)
   1.432 +  done
   1.433 +  
   1.434 +lemma listprod_coprime:
   1.435 +  "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (listprod xs) y" 
   1.436 +  by (induction xs) (simp_all add: gcd_mult_cancel)
   1.437 +
   1.438 +lemma coprime_divisors: 
   1.439 +  assumes "d dvd a" "e dvd b" "gcd a b = 1"
   1.440 +  shows "gcd d e = 1" 
   1.441 +proof -
   1.442 +  from assms obtain k l where "a = d * k" "b = e * l"
   1.443 +    unfolding dvd_def by blast
   1.444 +  with assms have "gcd (d * k) (e * l) = 1" by simp
   1.445 +  hence "gcd (d * k) e = 1" by (rule coprime_lmult)
   1.446 +  also have "gcd (d * k) e = gcd e (d * k)" by (simp add: ac_simps)
   1.447 +  finally have "gcd e d = 1" by (rule coprime_lmult)
   1.448 +  then show ?thesis by (simp add: ac_simps)
   1.449 +qed
   1.450 +
   1.451 +lemma lcm_gcd_prod:
   1.452 +  "lcm a b * gcd a b = normalize (a * b)"
   1.453 +  by (simp add: lcm_gcd)
   1.454 +
   1.455 +declare unit_factor_lcm [simp]
   1.456 +
   1.457 +lemma lcmI:
   1.458 +  assumes "a dvd c" and "b dvd c" and "\<And>d. a dvd d \<Longrightarrow> b dvd d \<Longrightarrow> c dvd d"
   1.459 +    and "normalize c = c"
   1.460 +  shows "c = lcm a b"
   1.461 +  by (rule associated_eqI) (auto simp: assms intro: lcm_least)
   1.462 +
   1.463 +lemma gcd_dvd_lcm [simp]:
   1.464 +  "gcd a b dvd lcm a b"
   1.465 +  using gcd_dvd2 by (rule dvd_lcmI2)
   1.466 +
   1.467 +lemmas lcm_0 = lcm_0_right
   1.468 +
   1.469 +lemma lcm_unique:
   1.470 +  "a dvd d \<and> b dvd d \<and> 
   1.471 +  normalize d = d \<and>
   1.472 +  (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
   1.473 +  by rule (auto intro: lcmI simp: lcm_least lcm_eq_0_iff)
   1.474 +
   1.475 +lemma lcm_coprime:
   1.476 +  "gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)"
   1.477 +  by (subst lcm_gcd) simp
   1.478 +
   1.479 +lemma lcm_proj1_if_dvd: 
   1.480 +  "b dvd a \<Longrightarrow> lcm a b = normalize a"
   1.481 +  by (cases "a = 0") (simp, rule sym, rule lcmI, simp_all)
   1.482 +
   1.483 +lemma lcm_proj2_if_dvd: 
   1.484 +  "a dvd b \<Longrightarrow> lcm a b = normalize b"
   1.485 +  using lcm_proj1_if_dvd [of a b] by (simp add: ac_simps)
   1.486 +
   1.487 +lemma lcm_proj1_iff:
   1.488 +  "lcm m n = normalize m \<longleftrightarrow> n dvd m"
   1.489 +proof
   1.490 +  assume A: "lcm m n = normalize m"
   1.491 +  show "n dvd m"
   1.492 +  proof (cases "m = 0")
   1.493 +    assume [simp]: "m \<noteq> 0"
   1.494 +    from A have B: "m = lcm m n * unit_factor m"
   1.495 +      by (simp add: unit_eq_div2)
   1.496 +    show ?thesis by (subst B, simp)
   1.497 +  qed simp
   1.498 +next
   1.499 +  assume "n dvd m"
   1.500 +  then show "lcm m n = normalize m" by (rule lcm_proj1_if_dvd)
   1.501 +qed
   1.502 +
   1.503 +lemma lcm_proj2_iff:
   1.504 +  "lcm m n = normalize n \<longleftrightarrow> m dvd n"
   1.505 +  using lcm_proj1_iff [of n m] by (simp add: ac_simps)
   1.506 +
   1.507  end
   1.508  
   1.509  class ring_gcd = comm_ring_1 + semiring_gcd
   1.510 +begin
   1.511 +
   1.512 +lemma coprime_minus_one: "coprime (n - 1) n"
   1.513 +  using coprime_plus_one[of "n - 1"] by (simp add: gcd.commute)
   1.514 +
   1.515 +lemma gcd_neg1 [simp]:
   1.516 +  "gcd (-a) b = gcd a b"
   1.517 +  by (rule sym, rule gcdI, simp_all add: gcd_greatest)
   1.518 +
   1.519 +lemma gcd_neg2 [simp]:
   1.520 +  "gcd a (-b) = gcd a b"
   1.521 +  by (rule sym, rule gcdI, simp_all add: gcd_greatest)
   1.522 +
   1.523 +lemma gcd_neg_numeral_1 [simp]:
   1.524 +  "gcd (- numeral n) a = gcd (numeral n) a"
   1.525 +  by (fact gcd_neg1)
   1.526 +
   1.527 +lemma gcd_neg_numeral_2 [simp]:
   1.528 +  "gcd a (- numeral n) = gcd a (numeral n)"
   1.529 +  by (fact gcd_neg2)
   1.530 +
   1.531 +lemma gcd_diff1: "gcd (m - n) n = gcd m n"
   1.532 +  by (subst diff_conv_add_uminus, subst gcd_neg2[symmetric],  subst gcd_add1, simp)
   1.533 +
   1.534 +lemma gcd_diff2: "gcd (n - m) n = gcd m n"
   1.535 +  by (subst gcd_neg1[symmetric], simp only: minus_diff_eq gcd_diff1)
   1.536 +
   1.537 +lemma lcm_neg1 [simp]: "lcm (-a) b = lcm a b"
   1.538 +  by (rule sym, rule lcmI, simp_all add: lcm_least lcm_eq_0_iff)
   1.539 +
   1.540 +lemma lcm_neg2 [simp]: "lcm a (-b) = lcm a b"
   1.541 +  by (rule sym, rule lcmI, simp_all add: lcm_least lcm_eq_0_iff)
   1.542 +
   1.543 +lemma lcm_neg_numeral_1 [simp]: "lcm (- numeral n) a = lcm (numeral n) a"
   1.544 +  by (fact lcm_neg1)
   1.545 +
   1.546 +lemma lcm_neg_numeral_2 [simp]: "lcm a (- numeral n) = lcm a (numeral n)"
   1.547 +  by (fact lcm_neg2)
   1.548 +
   1.549 +end
   1.550  
   1.551  class semiring_Gcd = semiring_gcd + Gcd +
   1.552    assumes Gcd_dvd: "a \<in> A \<Longrightarrow> Gcd A dvd a"
   1.553 @@ -471,6 +1010,27 @@
   1.554      by (rule associated_eqI) (simp_all add: lcm_eq_0_iff)
   1.555  qed
   1.556  
   1.557 +lemma LcmI:
   1.558 +  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.559 +    and "normalize b = b" shows "b = Lcm A"
   1.560 +  by (rule associated_eqI) (auto simp: assms dvd_Lcm intro: Lcm_least)
   1.561 +
   1.562 +lemma Lcm_subset:
   1.563 +  "A \<subseteq> B \<Longrightarrow> Lcm A dvd Lcm B"
   1.564 +  by (blast intro: Lcm_least dvd_Lcm)
   1.565 +
   1.566 +lemma Lcm_Un:
   1.567 +  "Lcm (A \<union> B) = lcm (Lcm A) (Lcm B)"
   1.568 +  apply (rule lcmI)
   1.569 +  apply (blast intro: Lcm_subset)
   1.570 +  apply (blast intro: Lcm_subset)
   1.571 +  apply (intro Lcm_least ballI, elim UnE)
   1.572 +  apply (rule dvd_trans, erule dvd_Lcm, assumption)
   1.573 +  apply (rule dvd_trans, erule dvd_Lcm, assumption)
   1.574 +  apply simp
   1.575 +  done
   1.576 +  
   1.577 +
   1.578  lemma Gcd_0_iff [simp]:
   1.579    "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}" (is "?P \<longleftrightarrow> ?Q")
   1.580  proof
   1.581 @@ -518,20 +1078,6 @@
   1.582      by simp
   1.583  qed
   1.584  
   1.585 -lemma unit_factor_Gcd:
   1.586 -  "unit_factor (Gcd A) = (if \<forall>a\<in>A. a = 0 then 0 else 1)"
   1.587 -proof (cases "Gcd A = 0")
   1.588 -  case True then show ?thesis by auto
   1.589 -next
   1.590 -  case False
   1.591 -  from unit_factor_mult_normalize
   1.592 -  have "unit_factor (Gcd A) * normalize (Gcd A) = Gcd A" .
   1.593 -  then have "unit_factor (Gcd A) * Gcd A = Gcd A" by simp
   1.594 -  then have "unit_factor (Gcd A) * Gcd A div Gcd A = Gcd A div Gcd A" by simp
   1.595 -  with False have "unit_factor (Gcd A) = 1" by simp
   1.596 -  with False show ?thesis by auto
   1.597 -qed
   1.598 -
   1.599  lemma unit_factor_Lcm:
   1.600    "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
   1.601  proof (cases "Lcm A = 0")
   1.602 @@ -544,6 +1090,18 @@
   1.603      by simp
   1.604  qed
   1.605  
   1.606 +lemma unit_factor_Gcd: "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
   1.607 +proof -
   1.608 +  show "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
   1.609 +    by (simp add: Gcd_Lcm unit_factor_Lcm)
   1.610 +qed
   1.611 +
   1.612 +lemma GcdI:
   1.613 +  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.614 +    and "normalize b = b"
   1.615 +  shows "b = Gcd A"
   1.616 +  by (rule associated_eqI) (auto simp: assms Gcd_dvd intro: Gcd_greatest)
   1.617 +
   1.618  lemma Gcd_eq_1_I:
   1.619    assumes "is_unit a" and "a \<in> A"
   1.620    shows "Gcd A = 1"
   1.621 @@ -585,13 +1143,26 @@
   1.622        (auto simp add: lcm_eq_0_iff)
   1.623  qed
   1.624  
   1.625 -lemma Gcd_set [code_unfold]:
   1.626 -  "Gcd (set as) = foldr gcd as 0"
   1.627 -  by (induct as) simp_all
   1.628 +lemma Gcd_finite:
   1.629 +  assumes "finite A"
   1.630 +  shows "Gcd A = Finite_Set.fold gcd 0 A"
   1.631 +  by (induct rule: finite.induct[OF \<open>finite A\<close>])
   1.632 +     (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd])
   1.633 +
   1.634 +lemma Gcd_set [code_unfold]: "Gcd (set as) = foldl gcd 0 as"
   1.635 +  by (simp add: Gcd_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd] 
   1.636 +                foldl_conv_fold gcd.commute)
   1.637 +
   1.638 +lemma Lcm_finite:
   1.639 +  assumes "finite A"
   1.640 +  shows "Lcm A = Finite_Set.fold lcm 1 A"
   1.641 +  by (induct rule: finite.induct[OF \<open>finite A\<close>])
   1.642 +     (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm])
   1.643  
   1.644  lemma Lcm_set [code_unfold]:
   1.645 -  "Lcm (set as) = foldr lcm as 1"
   1.646 -  by (induct as) simp_all
   1.647 +  "Lcm (set as) = foldl lcm 1 as"
   1.648 +  by (simp add: Lcm_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm] 
   1.649 +                foldl_conv_fold lcm.commute)
   1.650  
   1.651  lemma Gcd_image_normalize [simp]:
   1.652    "Gcd (normalize ` A) = Gcd A"
   1.653 @@ -624,6 +1195,76 @@
   1.654    shows "Lcm A = a"
   1.655    using assms by (blast intro: associated_eqI Lcm_least dvd_Lcm normalize_Lcm)
   1.656  
   1.657 +
   1.658 +lemma Lcm_no_units:
   1.659 +  "Lcm A = Lcm (A - {a. is_unit a})"
   1.660 +proof -
   1.661 +  have "(A - {a. is_unit a}) \<union> {a\<in>A. is_unit a} = A" by blast
   1.662 +  hence "Lcm A = lcm (Lcm (A - {a. is_unit a})) (Lcm {a\<in>A. is_unit a})"
   1.663 +    by (simp add: Lcm_Un [symmetric])
   1.664 +  also have "Lcm {a\<in>A. is_unit a} = 1" by (simp add: Lcm_1_iff)
   1.665 +  finally show ?thesis by simp
   1.666 +qed
   1.667 +
   1.668 +lemma Lcm_0_iff': "Lcm A = 0 \<longleftrightarrow> \<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))"
   1.669 +  by (metis Lcm_least dvd_0_left dvd_Lcm)
   1.670 +
   1.671 +lemma Lcm_no_multiple: "(\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not>a dvd m)) \<Longrightarrow> Lcm A = 0"
   1.672 +  by (auto simp: Lcm_0_iff')
   1.673 +
   1.674 +lemma Lcm_singleton [simp]:
   1.675 +  "Lcm {a} = normalize a"
   1.676 +  by simp
   1.677 +
   1.678 +lemma Lcm_2 [simp]:
   1.679 +  "Lcm {a,b} = lcm a b"
   1.680 +  by simp
   1.681 +
   1.682 +lemma Lcm_coprime:
   1.683 +  assumes "finite A" and "A \<noteq> {}" 
   1.684 +  assumes "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1"
   1.685 +  shows "Lcm A = normalize (\<Prod>A)"
   1.686 +using assms proof (induct rule: finite_ne_induct)
   1.687 +  case (insert a A)
   1.688 +  have "Lcm (insert a A) = lcm a (Lcm A)" by simp
   1.689 +  also from insert have "Lcm A = normalize (\<Prod>A)" by blast
   1.690 +  also have "lcm a \<dots> = lcm a (\<Prod>A)" by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
   1.691 +  also from insert have "gcd a (\<Prod>A) = 1" by (subst gcd.commute, intro setprod_coprime) auto
   1.692 +  with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
   1.693 +    by (simp add: lcm_coprime)
   1.694 +  finally show ?case .
   1.695 +qed simp
   1.696 +      
   1.697 +lemma Lcm_coprime':
   1.698 +  "card A \<noteq> 0 \<Longrightarrow> (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1)
   1.699 +    \<Longrightarrow> Lcm A = normalize (\<Prod>A)"
   1.700 +  by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
   1.701 +
   1.702 +lemma Gcd_1:
   1.703 +  "1 \<in> A \<Longrightarrow> Gcd A = 1"
   1.704 +  by (auto intro!: Gcd_eq_1_I)
   1.705 +
   1.706 +lemma Gcd_singleton [simp]: "Gcd {a} = normalize a"
   1.707 +  by simp
   1.708 +
   1.709 +lemma Gcd_2 [simp]: "Gcd {a,b} = gcd a b"
   1.710 +  by simp
   1.711 +
   1.712 +
   1.713 +definition pairwise_coprime where
   1.714 +  "pairwise_coprime A = (\<forall>x y. x \<in> A \<and> y \<in> A \<and> x \<noteq> y \<longrightarrow> coprime x y)"
   1.715 +
   1.716 +lemma pairwise_coprimeI [intro?]:
   1.717 +  "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y) \<Longrightarrow> pairwise_coprime A"
   1.718 +  by (simp add: pairwise_coprime_def)
   1.719 +
   1.720 +lemma pairwise_coprimeD:
   1.721 +  "pairwise_coprime A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y"
   1.722 +  by (simp add: pairwise_coprime_def)
   1.723 +
   1.724 +lemma pairwise_coprime_subset: "pairwise_coprime A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> pairwise_coprime B"
   1.725 +  by (force simp: pairwise_coprime_def)
   1.726 +
   1.727  end
   1.728  
   1.729  subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
   1.730 @@ -895,73 +1536,6 @@
   1.731    apply auto
   1.732  done
   1.733  
   1.734 -context semiring_gcd
   1.735 -begin
   1.736 -
   1.737 -lemma coprime_dvd_mult:
   1.738 -  assumes "coprime a b" and "a dvd c * b"
   1.739 -  shows "a dvd c"
   1.740 -proof (cases "c = 0")
   1.741 -  case True then show ?thesis by simp
   1.742 -next
   1.743 -  case False
   1.744 -  then have unit: "is_unit (unit_factor c)" by simp
   1.745 -  from \<open>coprime a b\<close> mult_gcd_left [of c a b]
   1.746 -  have "gcd (c * a) (c * b) * unit_factor c = c"
   1.747 -    by (simp add: ac_simps)
   1.748 -  moreover from \<open>a dvd c * b\<close> have "a dvd gcd (c * a) (c * b) * unit_factor c"
   1.749 -    by (simp add: dvd_mult_unit_iff unit)
   1.750 -  ultimately show ?thesis by simp
   1.751 -qed
   1.752 -
   1.753 -lemma coprime_dvd_mult_iff:
   1.754 -  assumes "coprime a c"
   1.755 -  shows "a dvd b * c \<longleftrightarrow> a dvd b"
   1.756 -  using assms by (auto intro: coprime_dvd_mult)
   1.757 -
   1.758 -lemma gcd_mult_cancel:
   1.759 -  "coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b"
   1.760 -  apply (rule associated_eqI)
   1.761 -  apply (rule gcd_greatest)
   1.762 -  apply (rule_tac b = c in coprime_dvd_mult)
   1.763 -  apply (simp add: gcd.assoc)
   1.764 -  apply (simp_all add: ac_simps)
   1.765 -  done
   1.766 -
   1.767 -lemma coprime_crossproduct:
   1.768 -  fixes a b c d
   1.769 -  assumes "coprime a d" and "coprime b c"
   1.770 -  shows "normalize a * normalize c = normalize b * normalize d
   1.771 -    \<longleftrightarrow> normalize a = normalize b \<and> normalize c = normalize d" (is "?lhs \<longleftrightarrow> ?rhs")
   1.772 -proof
   1.773 -  assume ?rhs then show ?lhs by simp
   1.774 -next
   1.775 -  assume ?lhs
   1.776 -  from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
   1.777 -    by (auto intro: dvdI dest: sym)
   1.778 -  with \<open>coprime a d\<close> have "a dvd b"
   1.779 -    by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
   1.780 -  from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c"
   1.781 -    by (auto intro: dvdI dest: sym)
   1.782 -  with \<open>coprime b c\<close> have "b dvd a"
   1.783 -    by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
   1.784 -  from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b"
   1.785 -    by (auto intro: dvdI dest: sym simp add: mult.commute)
   1.786 -  with \<open>coprime b c\<close> have "c dvd d"
   1.787 -    by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
   1.788 -  from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a"
   1.789 -    by (auto intro: dvdI dest: sym simp add: mult.commute)
   1.790 -  with \<open>coprime a d\<close> have "d dvd c"
   1.791 -    by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
   1.792 -  from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b"
   1.793 -    by (rule associatedI)
   1.794 -  moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d"
   1.795 -    by (rule associatedI)
   1.796 -  ultimately show ?rhs ..
   1.797 -qed
   1.798 -
   1.799 -end
   1.800 -
   1.801  lemma coprime_crossproduct_nat:
   1.802    fixes a b c d :: nat
   1.803    assumes "coprime a d" and "coprime b c"
   1.804 @@ -976,21 +1550,10 @@
   1.805  
   1.806  text \<open>\medskip Addition laws\<close>
   1.807  
   1.808 -lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n"
   1.809 -  apply (case_tac "n = 0")
   1.810 -  apply (simp_all add: gcd_non_0_nat)
   1.811 -  done
   1.812 -
   1.813 -lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n"
   1.814 -  apply (subst (1 2) gcd.commute)
   1.815 -  apply (subst add.commute)
   1.816 -  apply simp
   1.817 -  done
   1.818 -
   1.819  (* to do: add the other variations? *)
   1.820  
   1.821  lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
   1.822 -  by (subst gcd_add1_nat [symmetric]) auto
   1.823 +  by (subst gcd_add1 [symmetric]) auto
   1.824  
   1.825  lemma gcd_diff2_nat: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
   1.826    apply (subst gcd.commute)
   1.827 @@ -1022,25 +1585,9 @@
   1.828    apply auto
   1.829  done
   1.830  
   1.831 -lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n"
   1.832 -by (metis gcd_red_int mod_add_self1 add.commute)
   1.833 -
   1.834 -lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n"
   1.835 -by (metis gcd_add1_int gcd.commute add.commute)
   1.836 -
   1.837 -lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n"
   1.838 -by (metis mod_mult_self3 gcd.commute gcd_red_nat)
   1.839 -
   1.840 -lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n"
   1.841 -by (metis gcd.commute gcd_red_int mod_mult_self1 add.commute)
   1.842 -
   1.843 -
   1.844  (* to do: differences, and all variations of addition rules
   1.845      as simplification rules for nat and int *)
   1.846  
   1.847 -lemma gcd_dvd_prod_nat: "gcd (m::nat) n dvd k * n"
   1.848 -  using mult_dvd_mono [of 1] by auto
   1.849 -
   1.850  (* to do: add the three variations of these, and for ints? *)
   1.851  
   1.852  lemma finite_divisors_nat [simp]: -- \<open>FIXME move\<close>
   1.853 @@ -1104,49 +1651,6 @@
   1.854  
   1.855  subsection \<open>Coprimality\<close>
   1.856  
   1.857 -context semiring_gcd
   1.858 -begin
   1.859 -
   1.860 -lemma div_gcd_coprime:
   1.861 -  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
   1.862 -  shows "coprime (a div gcd a b) (b div gcd a b)"
   1.863 -proof -
   1.864 -  let ?g = "gcd a b"
   1.865 -  let ?a' = "a div ?g"
   1.866 -  let ?b' = "b div ?g"
   1.867 -  let ?g' = "gcd ?a' ?b'"
   1.868 -  have dvdg: "?g dvd a" "?g dvd b" by simp_all
   1.869 -  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
   1.870 -  from dvdg dvdg' obtain ka kb ka' kb' where
   1.871 -      kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
   1.872 -    unfolding dvd_def by blast
   1.873 -  from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
   1.874 -    by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
   1.875 -  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   1.876 -    by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
   1.877 -      dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   1.878 -  have "?g \<noteq> 0" using nz by simp
   1.879 -  moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   1.880 -  thm dvd_mult_cancel_left
   1.881 -  ultimately show ?thesis using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
   1.882 -qed
   1.883 -
   1.884 -lemma coprime:
   1.885 -  "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)" (is "?P \<longleftrightarrow> ?Q")
   1.886 -proof
   1.887 -  assume ?P then show ?Q by auto
   1.888 -next
   1.889 -  assume ?Q
   1.890 -  then have "is_unit (gcd a b) \<longleftrightarrow> gcd a b dvd a \<and> gcd a b dvd b"
   1.891 -    by blast
   1.892 -  then have "is_unit (gcd a b)"
   1.893 -    by simp
   1.894 -  then show ?P
   1.895 -    by simp
   1.896 -qed
   1.897 -
   1.898 -end
   1.899 -
   1.900  lemma coprime_nat:
   1.901    "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   1.902    using coprime [of a b] by simp
   1.903 @@ -1165,337 +1669,15 @@
   1.904    using abs_dvd_iff abs_ge_zero apply blast
   1.905    done
   1.906  
   1.907 -lemma gcd_coprime_nat:
   1.908 -  assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and
   1.909 -    b: "b = b' * gcd a b"
   1.910 -  shows    "coprime a' b'"
   1.911 -
   1.912 -  apply (subgoal_tac "a' = a div gcd a b")
   1.913 -  apply (erule ssubst)
   1.914 -  apply (subgoal_tac "b' = b div gcd a b")
   1.915 -  apply (erule ssubst)
   1.916 -  apply (rule div_gcd_coprime)
   1.917 -  using z apply force
   1.918 -  apply (subst (1) b)
   1.919 -  using z apply force
   1.920 -  apply (subst (1) a)
   1.921 -  using z apply force
   1.922 -  done
   1.923 -
   1.924 -lemma gcd_coprime_int:
   1.925 -  assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
   1.926 -    b: "b = b' * gcd a b"
   1.927 -  shows    "coprime a' b'"
   1.928 -  apply (subgoal_tac "a' = a div gcd a b")
   1.929 -  apply (erule ssubst)
   1.930 -  apply (subgoal_tac "b' = b div gcd a b")
   1.931 -  apply (erule ssubst)
   1.932 -  apply (rule div_gcd_coprime)
   1.933 -  using z apply force
   1.934 -  apply (subst (1) b)
   1.935 -  using z apply force
   1.936 -  apply (subst (1) a)
   1.937 -  using z apply force
   1.938 -  done
   1.939 -
   1.940 -context semiring_gcd
   1.941 -begin
   1.942 -
   1.943 -lemma coprime_mult:
   1.944 -  assumes da: "coprime d a" and db: "coprime d b"
   1.945 -  shows "coprime d (a * b)"
   1.946 -  apply (subst gcd.commute)
   1.947 -  using da apply (subst gcd_mult_cancel)
   1.948 -  apply (subst gcd.commute, assumption)
   1.949 -  apply (subst gcd.commute, rule db)
   1.950 -  done
   1.951 -
   1.952 -end
   1.953 -
   1.954 -lemma coprime_lmult_nat:
   1.955 -  assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
   1.956 -proof -
   1.957 -  have "gcd d a dvd gcd d (a * b)"
   1.958 -    by (rule gcd_greatest, auto)
   1.959 -  with dab show ?thesis
   1.960 -    by auto
   1.961 -qed
   1.962 -
   1.963 -lemma coprime_lmult_int:
   1.964 -  assumes "coprime (d::int) (a * b)" shows "coprime d a"
   1.965 -proof -
   1.966 -  have "gcd d a dvd gcd d (a * b)"
   1.967 -    by (rule gcd_greatest, auto)
   1.968 -  with assms show ?thesis
   1.969 -    by auto
   1.970 -qed
   1.971 -
   1.972 -lemma coprime_rmult_nat:
   1.973 -  assumes "coprime (d::nat) (a * b)" shows "coprime d b"
   1.974 -proof -
   1.975 -  have "gcd d b dvd gcd d (a * b)"
   1.976 -    by (rule gcd_greatest, auto intro: dvd_mult)
   1.977 -  with assms show ?thesis
   1.978 -    by auto
   1.979 -qed
   1.980 -
   1.981 -lemma coprime_rmult_int:
   1.982 -  assumes dab: "coprime (d::int) (a * b)" shows "coprime d b"
   1.983 -proof -
   1.984 -  have "gcd d b dvd gcd d (a * b)"
   1.985 -    by (rule gcd_greatest, auto intro: dvd_mult)
   1.986 -  with dab show ?thesis
   1.987 -    by auto
   1.988 -qed
   1.989 -
   1.990 -lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \<longleftrightarrow>
   1.991 -    coprime d a \<and>  coprime d b"
   1.992 -  using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b]
   1.993 -    coprime_mult [of d a b]
   1.994 -  by blast
   1.995 -
   1.996 -lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \<longleftrightarrow>
   1.997 -    coprime d a \<and>  coprime d b"
   1.998 -  using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b]
   1.999 -    coprime_mult [of d a b]
  1.1000 -  by blast
  1.1001 -
  1.1002 -lemma coprime_power_int:
  1.1003 -  assumes "0 < n" shows "coprime (a :: int) (b ^ n) \<longleftrightarrow> coprime a b"
  1.1004 -  using assms
  1.1005 -proof (induct n)
  1.1006 -  case (Suc n) then show ?case
  1.1007 -    by (cases n) (simp_all add: coprime_mul_eq_int)
  1.1008 -qed simp
  1.1009 -
  1.1010 -lemma gcd_coprime_exists_nat:
  1.1011 -    assumes nz: "gcd (a::nat) b \<noteq> 0"
  1.1012 -    shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
  1.1013 -  apply (rule_tac x = "a div gcd a b" in exI)
  1.1014 -  apply (rule_tac x = "b div gcd a b" in exI)
  1.1015 -  using nz apply (auto simp add: div_gcd_coprime dvd_div_mult)
  1.1016 -done
  1.1017 -
  1.1018 -lemma gcd_coprime_exists_int:
  1.1019 -    assumes nz: "gcd (a::int) b \<noteq> 0"
  1.1020 -    shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
  1.1021 -  apply (rule_tac x = "a div gcd a b" in exI)
  1.1022 -  apply (rule_tac x = "b div gcd a b" in exI)
  1.1023 -  using nz apply (auto simp add: div_gcd_coprime)
  1.1024 -done
  1.1025 -
  1.1026 -lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
  1.1027 -  by (induct n) (simp_all add: coprime_mult)
  1.1028 -
  1.1029 -lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
  1.1030 -  by (induct n) (simp_all add: coprime_mult)
  1.1031 -
  1.1032 -context semiring_gcd
  1.1033 -begin
  1.1034 -
  1.1035 -lemma coprime_exp_left:
  1.1036 -  assumes "coprime a b"
  1.1037 -  shows "coprime (a ^ n) b"
  1.1038 -  using assms by (induct n) (simp_all add: gcd_mult_cancel)
  1.1039 -
  1.1040 -lemma coprime_exp2:
  1.1041 -  assumes "coprime a b"
  1.1042 -  shows "coprime (a ^ n) (b ^ m)"
  1.1043 -proof (rule coprime_exp_left)
  1.1044 -  from assms show "coprime a (b ^ m)"
  1.1045 -    by (induct m) (simp_all add: gcd_mult_cancel gcd.commute [of a])
  1.1046 -qed
  1.1047 -
  1.1048 -end
  1.1049 -
  1.1050 -lemma gcd_exp_nat:
  1.1051 -  "gcd ((a :: nat) ^ n) (b ^ n) = gcd a b ^ n"
  1.1052 -proof (cases "a = 0 \<and> b = 0")
  1.1053 -  case True then show ?thesis by (cases "n > 0") (simp_all add: zero_power)
  1.1054 -next
  1.1055 -  case False
  1.1056 -  then have "coprime (a div gcd a b) (b div gcd a b)"
  1.1057 -    by (auto simp: div_gcd_coprime)
  1.1058 -  then have "coprime ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
  1.1059 -    by (simp add: coprime_exp2)
  1.1060 -  then have "gcd ((a div gcd a b)^n * (gcd a b)^n)
  1.1061 -      ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
  1.1062 -    by (metis gcd_mult_distrib_nat mult.commute mult.right_neutral)
  1.1063 -  also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
  1.1064 -    by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib)
  1.1065 -  also have "(b div gcd a b)^n * (gcd a b)^n = b^n"
  1.1066 -    by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib)
  1.1067 -  finally show ?thesis .
  1.1068 -qed
  1.1069 -
  1.1070 -lemma gcd_exp_int: "gcd ((a::int)^n) (b^n) = (gcd a b)^n"
  1.1071 -  apply (subst (1 2) gcd_abs_int)
  1.1072 -  apply (subst (1 2) power_abs)
  1.1073 -  apply (rule gcd_exp_nat [where n = n, transferred])
  1.1074 -  apply auto
  1.1075 -done
  1.1076 -
  1.1077 -lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c"
  1.1078 -  shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
  1.1079 -proof-
  1.1080 -  let ?g = "gcd a b"
  1.1081 -  {assume "?g = 0" with dc have ?thesis by auto}
  1.1082 -  moreover
  1.1083 -  {assume z: "?g \<noteq> 0"
  1.1084 -    from gcd_coprime_exists_nat[OF z]
  1.1085 -    obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
  1.1086 -      by blast
  1.1087 -    have thb: "?g dvd b" by auto
  1.1088 -    from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
  1.1089 -    with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
  1.1090 -    from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
  1.1091 -    hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc)
  1.1092 -    with z have th_1: "a' dvd b' * c" by auto
  1.1093 -    from coprime_dvd_mult [OF ab'(3)] th_1
  1.1094 -    have thc: "a' dvd c" by (subst (asm) mult.commute, blast)
  1.1095 -    from ab' have "a = ?g*a'" by algebra
  1.1096 -    with thb thc have ?thesis by blast }
  1.1097 -  ultimately show ?thesis by blast
  1.1098 -qed
  1.1099 -
  1.1100 -lemma division_decomp_int: assumes dc: "(a::int) dvd b * c"
  1.1101 -  shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
  1.1102 -proof-
  1.1103 -  let ?g = "gcd a b"
  1.1104 -  {assume "?g = 0" with dc have ?thesis by auto}
  1.1105 -  moreover
  1.1106 -  {assume z: "?g \<noteq> 0"
  1.1107 -    from gcd_coprime_exists_int[OF z]
  1.1108 -    obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
  1.1109 -      by blast
  1.1110 -    have thb: "?g dvd b" by auto
  1.1111 -    from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
  1.1112 -    with dc have th0: "a' dvd b*c"
  1.1113 -      using dvd_trans[of a' a "b*c"] by simp
  1.1114 -    from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
  1.1115 -    hence "?g*a' dvd ?g * (b' * c)" by (simp add: ac_simps)
  1.1116 -    with z have th_1: "a' dvd b' * c" by auto
  1.1117 -    from coprime_dvd_mult [OF ab'(3)] th_1
  1.1118 -    have thc: "a' dvd c" by (subst (asm) mult.commute, blast)
  1.1119 -    from ab' have "a = ?g*a'" by algebra
  1.1120 -    with thb thc have ?thesis by blast }
  1.1121 -  ultimately show ?thesis by blast
  1.1122 -qed
  1.1123 -
  1.1124 -lemma pow_divides_pow_nat:
  1.1125 -  assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0"
  1.1126 -  shows "a dvd b"
  1.1127 -proof-
  1.1128 -  let ?g = "gcd a b"
  1.1129 -  from n obtain m where m: "n = Suc m" by (cases n, simp_all)
  1.1130 -  {assume "?g = 0" with ab n have ?thesis by auto }
  1.1131 -  moreover
  1.1132 -  {assume z: "?g \<noteq> 0"
  1.1133 -    hence zn: "?g ^ n \<noteq> 0" using n by simp
  1.1134 -    from gcd_coprime_exists_nat[OF z]
  1.1135 -    obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
  1.1136 -      by blast
  1.1137 -    from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
  1.1138 -      by (simp add: ab'(1,2)[symmetric])
  1.1139 -    hence "?g^n*a'^n dvd ?g^n *b'^n"
  1.1140 -      by (simp only: power_mult_distrib mult.commute)
  1.1141 -    then have th0: "a'^n dvd b'^n"
  1.1142 -      using zn by auto
  1.1143 -    have "a' dvd a'^n" by (simp add: m)
  1.1144 -    with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
  1.1145 -    hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)
  1.1146 -    from coprime_dvd_mult [OF coprime_exp_nat [OF ab'(3), of m]] th1
  1.1147 -    have "a' dvd b'" by (subst (asm) mult.commute, blast)
  1.1148 -    hence "a'*?g dvd b'*?g" by simp
  1.1149 -    with ab'(1,2)  have ?thesis by simp }
  1.1150 -  ultimately show ?thesis by blast
  1.1151 -qed
  1.1152 -
  1.1153 -lemma pow_divides_pow_int:
  1.1154 -  assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0"
  1.1155 -  shows "a dvd b"
  1.1156 -proof-
  1.1157 -  let ?g = "gcd a b"
  1.1158 -  from n obtain m where m: "n = Suc m" by (cases n, simp_all)
  1.1159 -  {assume "?g = 0" with ab n have ?thesis by auto }
  1.1160 -  moreover
  1.1161 -  {assume z: "?g \<noteq> 0"
  1.1162 -    hence zn: "?g ^ n \<noteq> 0" using n by simp
  1.1163 -    from gcd_coprime_exists_int[OF z]
  1.1164 -    obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
  1.1165 -      by blast
  1.1166 -    from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
  1.1167 -      by (simp add: ab'(1,2)[symmetric])
  1.1168 -    hence "?g^n*a'^n dvd ?g^n *b'^n"
  1.1169 -      by (simp only: power_mult_distrib mult.commute)
  1.1170 -    with zn z n have th0:"a'^n dvd b'^n" by auto
  1.1171 -    have "a' dvd a'^n" by (simp add: m)
  1.1172 -    with th0 have "a' dvd b'^n"
  1.1173 -      using dvd_trans[of a' "a'^n" "b'^n"] by simp
  1.1174 -    hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)
  1.1175 -    from coprime_dvd_mult [OF coprime_exp_int [OF ab'(3), of m]] th1
  1.1176 -    have "a' dvd b'" by (subst (asm) mult.commute, blast)
  1.1177 -    hence "a'*?g dvd b'*?g" by simp
  1.1178 -    with ab'(1,2)  have ?thesis by simp }
  1.1179 -  ultimately show ?thesis by blast
  1.1180 -qed
  1.1181 -
  1.1182  lemma pow_divides_eq_nat [simp]:
  1.1183    "n > 0 \<Longrightarrow> (a::nat) ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
  1.1184 -  by (auto intro: pow_divides_pow_nat dvd_power_same)
  1.1185 -
  1.1186 -lemma pow_divides_eq_int [simp]:
  1.1187 -  "n ~= 0 \<Longrightarrow> (a::int) ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
  1.1188 -  by (auto intro: pow_divides_pow_int dvd_power_same)
  1.1189 -
  1.1190 -context semiring_gcd
  1.1191 -begin
  1.1192 -
  1.1193 -lemma divides_mult:
  1.1194 -  assumes "a dvd c" and nr: "b dvd c" and "coprime a b"
  1.1195 -  shows "a * b dvd c"
  1.1196 -proof-
  1.1197 -  from \<open>b dvd c\<close> obtain b' where"c = b * b'" ..
  1.1198 -  with \<open>a dvd c\<close> have "a dvd b' * b"
  1.1199 -    by (simp add: ac_simps)
  1.1200 -  with \<open>coprime a b\<close> have "a dvd b'"
  1.1201 -    by (simp add: coprime_dvd_mult_iff)
  1.1202 -  then obtain a' where "b' = a * a'" ..
  1.1203 -  with \<open>c = b * b'\<close> have "c = (a * b) * a'"
  1.1204 -    by (simp add: ac_simps)
  1.1205 -  then show ?thesis ..
  1.1206 -qed
  1.1207 -
  1.1208 -end
  1.1209 -
  1.1210 -lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
  1.1211 -  by (simp add: gcd.commute del: One_nat_def)
  1.1212 +  using pow_divs_eq[of n] by simp
  1.1213  
  1.1214  lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
  1.1215 -  using coprime_plus_one_nat by simp
  1.1216 -
  1.1217 -lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"
  1.1218 -  by (simp add: gcd.commute)
  1.1219 +  using coprime_plus_one[of n] by simp
  1.1220  
  1.1221  lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
  1.1222 -  using coprime_plus_one_nat [of "n - 1"]
  1.1223 -    gcd.commute [of "n - 1" n] by auto
  1.1224 -
  1.1225 -lemma coprime_minus_one_int: "coprime ((n::int) - 1) n"
  1.1226 -  using coprime_plus_one_int [of "n - 1"]
  1.1227 -    gcd.commute [of "n - 1" n] by auto
  1.1228 -
  1.1229 -lemma setprod_coprime_nat:
  1.1230 -  fixes x :: nat
  1.1231 -  shows "(\<And>i. i \<in> A \<Longrightarrow> coprime (f i) x) \<Longrightarrow> coprime (\<Prod>i\<in>A. f i) x"
  1.1232 -  by (induct A rule: infinite_finite_induct)
  1.1233 -    (auto simp add: gcd_mult_cancel One_nat_def [symmetric] simp del: One_nat_def)
  1.1234 -
  1.1235 -lemma setprod_coprime_int:
  1.1236 -  fixes x :: int
  1.1237 -  shows "(\<And>i. i \<in> A \<Longrightarrow> coprime (f i) x) \<Longrightarrow> coprime (\<Prod>i\<in>A. f i) x"
  1.1238 -  by (induct A rule: infinite_finite_induct)
  1.1239 -    (auto simp add: gcd_mult_cancel)
  1.1240 +  using coprime_Suc_nat [of "n - 1"] gcd.commute [of "n - 1" n] by auto
  1.1241  
  1.1242  lemma coprime_common_divisor_nat: 
  1.1243    "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
  1.1244 @@ -1505,15 +1687,11 @@
  1.1245    "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
  1.1246    using gcd_greatest_iff [of x a b] by auto
  1.1247  
  1.1248 -lemma coprime_divisors_nat:
  1.1249 -    "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> coprime d e"
  1.1250 -  by (meson coprime_int dvd_trans gcd_dvd1 gcd_dvd2 gcd_ge_0_int)
  1.1251 -
  1.1252  lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
  1.1253 -by (metis coprime_lmult_nat gcd_1_nat gcd.commute gcd_red_nat)
  1.1254 +by (metis coprime_lmult gcd_1_nat gcd.commute gcd_red_nat)
  1.1255  
  1.1256  lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
  1.1257 -by (metis coprime_lmult_int gcd_1_int gcd.commute gcd_red_int)
  1.1258 +by (metis coprime_lmult gcd_1_int gcd.commute gcd_red_int)
  1.1259  
  1.1260  
  1.1261  subsection \<open>Bezout's theorem\<close>
  1.1262 @@ -1763,7 +1941,7 @@
  1.1263  
  1.1264  lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
  1.1265    unfolding lcm_nat_def
  1.1266 -  by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat])
  1.1267 +  by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod])
  1.1268  
  1.1269  lemma prod_gcd_lcm_int: "\<bar>m::int\<bar> * \<bar>n\<bar> = gcd m n * lcm m n"
  1.1270    unfolding lcm_int_def gcd_int_def
  1.1271 @@ -1828,14 +2006,6 @@
  1.1272  lemma lcm_proj2_iff_int [simp]: "lcm m n = \<bar>n::int\<bar> \<longleftrightarrow> m dvd n"
  1.1273  by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
  1.1274  
  1.1275 -lemma (in semiring_gcd) comp_fun_idem_gcd:
  1.1276 -  "comp_fun_idem gcd"
  1.1277 -  by standard (simp_all add: fun_eq_iff ac_simps)
  1.1278 -
  1.1279 -lemma (in semiring_gcd) comp_fun_idem_lcm:
  1.1280 -  "comp_fun_idem lcm"
  1.1281 -  by standard (simp_all add: fun_eq_iff ac_simps)
  1.1282 -
  1.1283  lemma lcm_1_iff_nat [simp]:
  1.1284    "lcm (m::nat) n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
  1.1285    using lcm_eq_1_iff [of m n] by simp
  1.1286 @@ -2069,21 +2239,11 @@
  1.1287  
  1.1288  text \<open>Some code equations\<close>
  1.1289  
  1.1290 -lemma Lcm_set_nat [code, code_unfold]:
  1.1291 -  "Lcm (set ns) = fold lcm ns (1::nat)"
  1.1292 -  using Lcm_set [of ns] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric])
  1.1293 -
  1.1294 -lemma Gcd_set_nat [code]:
  1.1295 -  "Gcd (set ns) = fold gcd ns (0::nat)"
  1.1296 -  using Gcd_set [of ns] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric])
  1.1297 +lemmas Lcm_set_nat [code, code_unfold] = Lcm_set[where ?'a = nat]
  1.1298 +lemmas Gcd_set_nat [code] = Gcd_set[where ?'a = nat]
  1.1299 +lemmas Lcm_set_int [code, code_unfold] = Lcm_set[where ?'a = int]
  1.1300 +lemmas Gcd_set_int [code] = Gcd_set[where ?'a = int]
  1.1301  
  1.1302 -lemma Lcm_set_int [code, code_unfold]:
  1.1303 -  "Lcm (set xs) = fold lcm xs (1::int)"
  1.1304 -  using Lcm_set [of xs] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric])
  1.1305 -
  1.1306 -lemma Gcd_set_int [code]:
  1.1307 -  "Gcd (set xs) = fold gcd xs (0::int)"
  1.1308 -  using Gcd_set [of xs] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric])
  1.1309  
  1.1310  text \<open>Fact aliasses\<close>
  1.1311