src/HOL/Number_Theory/Euclidean_Algorithm.thy
 changeset 62429 25271ff79171 parent 62428 4d5fbec92bb1 child 62442 26e4be6a680f
```     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Feb 26 18:33:01 2016 +0100
1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Feb 26 22:15:09 2016 +0100
1.3 @@ -3,7 +3,7 @@
1.4  section \<open>Abstract euclidean algorithm\<close>
1.5
1.6  theory Euclidean_Algorithm
1.7 -imports Main "~~/src/HOL/GCD" "~~/src/HOL/Library/Polynomial"
1.8 +imports "~~/src/HOL/GCD" "~~/src/HOL/Library/Polynomial"
1.9  begin
1.10
1.11  text \<open>
1.12 @@ -309,56 +309,14 @@
1.13  subclass semiring_Gcd
1.14    by standard (auto simp: Gcd_Gcd_eucl Lcm_Lcm_eucl Gcd_eucl_def intro: Lcm_eucl_least)
1.15
1.16 -
1.17  lemma gcd_non_0:
1.18    "b \<noteq> 0 \<Longrightarrow> gcd a b = gcd b (a mod b)"
1.19    unfolding gcd_gcd_eucl by (fact gcd_eucl_non_0)
1.20
1.21  lemmas gcd_0 = gcd_0_right
1.22  lemmas dvd_gcd_iff = gcd_greatest_iff
1.23 -
1.24  lemmas gcd_greatest_iff = dvd_gcd_iff
1.25
1.26 -lemma gcdI:
1.27 -  assumes "c dvd a" and "c dvd b" and greatest: "\<And>d. d dvd a \<Longrightarrow> d dvd b \<Longrightarrow> d dvd c"
1.28 -    and "normalize c = c"
1.29 -  shows "c = gcd a b"
1.30 -  by (rule associated_eqI) (auto simp: assms intro: gcd_greatest)
1.31 -
1.32 -lemma gcd_unique: "d dvd a \<and> d dvd b \<and>
1.33 -    normalize d = d \<and>
1.34 -    (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
1.35 -  by rule (auto intro: gcdI simp: gcd_greatest)
1.36 -
1.37 -lemma gcd_dvd_prod: "gcd a b dvd k * b"
1.38 -  using mult_dvd_mono [of 1] by auto
1.39 -
1.40 -lemma gcd_proj2_if_dvd:
1.41 -  "b dvd a \<Longrightarrow> gcd a b = normalize b"
1.42 -  by (cases "b = 0", simp_all add: dvd_eq_mod_eq_0 gcd_non_0)
1.43 -
1.44 -lemma gcd_proj1_if_dvd:
1.45 -  "a dvd b \<Longrightarrow> gcd a b = normalize a"
1.46 -  by (subst gcd.commute, simp add: gcd_proj2_if_dvd)
1.47 -
1.48 -lemma gcd_proj1_iff: "gcd m n = normalize m \<longleftrightarrow> m dvd n"
1.49 -proof
1.50 -  assume A: "gcd m n = normalize m"
1.51 -  show "m dvd n"
1.52 -  proof (cases "m = 0")
1.53 -    assume [simp]: "m \<noteq> 0"
1.54 -    from A have B: "m = gcd m n * unit_factor m"
1.55 -      by (simp add: unit_eq_div2)
1.56 -    show ?thesis by (subst B, simp add: mult_unit_dvd_iff)
1.57 -  qed (insert A, simp)
1.58 -next
1.59 -  assume "m dvd n"
1.60 -  then show "gcd m n = normalize m" by (rule gcd_proj1_if_dvd)
1.61 -qed
1.62 -
1.63 -lemma gcd_proj2_iff: "gcd m n = normalize n \<longleftrightarrow> n dvd m"
1.64 -  using gcd_proj1_iff [of n m] by (simp add: ac_simps)
1.65 -
1.66  lemma gcd_mod1 [simp]:
1.67    "gcd (a mod b) b = gcd a b"
1.68    by (rule gcdI, metis dvd_mod_iff gcd_dvd1 gcd_dvd2, simp_all add: gcd_greatest dvd_mod_iff)
1.69 @@ -367,39 +325,6 @@
1.70    "gcd a (b mod a) = gcd a b"
1.71    by (rule gcdI, simp, metis dvd_mod_iff gcd_dvd1 gcd_dvd2, simp_all add: gcd_greatest dvd_mod_iff)
1.72
1.73 -lemma gcd_mult_distrib':
1.74 -  "normalize c * gcd a b = gcd (c * a) (c * b)"
1.75 -proof (cases "c = 0")
1.76 -  case True then show ?thesis by simp_all
1.77 -next
1.78 -  case False then have [simp]: "is_unit (unit_factor c)" by simp
1.79 -  show ?thesis
1.80 -  proof (induct a b rule: gcd_eucl_induct)
1.81 -    case (zero a) show ?case
1.82 -    proof (cases "a = 0")
1.83 -      case True then show ?thesis by simp
1.84 -    next
1.85 -      case False
1.86 -      then show ?thesis by (simp add: normalize_mult)
1.87 -    qed
1.88 -    case (mod a b)
1.89 -    then show ?case by (simp add: mult_mod_right gcd.commute)
1.90 -  qed
1.91 -qed
1.92 -
1.93 -lemma gcd_mult_distrib:
1.94 -  "k * gcd a b = gcd (k * a) (k * b) * unit_factor k"
1.95 -proof-
1.96 -  have "normalize k * gcd a b = gcd (k * a) (k * b)"
1.97 -    by (simp add: gcd_mult_distrib')
1.98 -  then have "normalize k * gcd a b * unit_factor k = gcd (k * a) (k * b) * unit_factor k"
1.99 -    by simp
1.100 -  then have "normalize k * unit_factor k * gcd a b  = gcd (k * a) (k * b) * unit_factor k"
1.101 -    by (simp only: ac_simps)
1.102 -  then show ?thesis
1.103 -    by simp
1.104 -qed
1.105 -
1.106  lemma euclidean_size_gcd_le1 [simp]:
1.107    assumes "a \<noteq> 0"
1.108    shows "euclidean_size (gcd a b) \<le> euclidean_size a"
1.109 @@ -431,408 +356,13 @@
1.110    shows "euclidean_size (gcd a b) < euclidean_size b"
1.111    using assms by (subst gcd.commute, rule euclidean_size_gcd_less1)
1.112
1.113 -lemma gcd_mult_unit1: "is_unit a \<Longrightarrow> gcd (b * a) c = gcd b c"
1.114 -  apply (rule gcdI)
1.115 -  apply simp_all
1.116 -  apply (rule dvd_trans, rule gcd_dvd1, simp add: unit_simps)
1.117 -  done
1.118 -
1.119 -lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c"
1.120 -  by (subst gcd.commute, subst gcd_mult_unit1, assumption, rule gcd.commute)
1.121 -
1.122 -lemma gcd_div_unit1: "is_unit a \<Longrightarrow> gcd (b div a) c = gcd b c"
1.123 -  by (erule is_unitE [of _ b]) (simp add: gcd_mult_unit1)
1.124 -
1.125 -lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c"
1.126 -  by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2)
1.127 -
1.128 -lemma normalize_gcd_left [simp]:
1.129 -  "gcd (normalize a) b = gcd a b"
1.130 -proof (cases "a = 0")
1.131 -  case True then show ?thesis
1.132 -    by simp
1.133 -next
1.134 -  case False then have "is_unit (unit_factor a)"
1.135 -    by simp
1.136 -  moreover have "normalize a = a div unit_factor a"
1.137 -    by simp
1.138 -  ultimately show ?thesis
1.139 -    by (simp only: gcd_div_unit1)
1.140 -qed
1.141 -
1.142 -lemma normalize_gcd_right [simp]:
1.143 -  "gcd a (normalize b) = gcd a b"
1.144 -  using normalize_gcd_left [of b a] by (simp add: ac_simps)
1.145 -
1.146 -lemma gcd_idem: "gcd a a = normalize a"
1.147 -  by (cases "a = 0") (simp, rule sym, rule gcdI, simp_all)
1.148 -
1.149 -lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b"
1.150 -  apply (rule gcdI)
1.151 -  apply (simp add: ac_simps)
1.152 -  apply (rule gcd_dvd2)
1.153 -  apply (rule gcd_greatest, erule (1) gcd_greatest, assumption)
1.154 -  apply simp
1.155 -  done
1.156 -
1.157 -lemma gcd_left_idem: "gcd a (gcd a b) = gcd a b"
1.158 -  apply (rule gcdI)
1.159 -  apply simp
1.160 -  apply (rule dvd_trans, rule gcd_dvd2, rule gcd_dvd2)
1.161 -  apply (rule gcd_greatest, assumption, erule gcd_greatest, assumption)
1.162 -  apply simp
1.163 -  done
1.164 -
1.165 -lemma comp_fun_idem_gcd: "comp_fun_idem gcd"
1.166 -proof
1.167 -  fix a b show "gcd a \<circ> gcd b = gcd b \<circ> gcd a"
1.168 -    by (simp add: fun_eq_iff ac_simps)
1.169 -next
1.170 -  fix a show "gcd a \<circ> gcd a = gcd a"
1.171 -    by (simp add: fun_eq_iff gcd_left_idem)
1.172 -qed
1.173 -
1.174 -lemma gcd_dvd_antisym:
1.175 -  "gcd a b dvd gcd c d \<Longrightarrow> gcd c d dvd gcd a b \<Longrightarrow> gcd a b = gcd c d"
1.176 -proof (rule gcdI)
1.177 -  assume A: "gcd a b dvd gcd c d" and B: "gcd c d dvd gcd a b"
1.178 -  have "gcd c d dvd c" by simp
1.179 -  with A show "gcd a b dvd c" by (rule dvd_trans)
1.180 -  have "gcd c d dvd d" by simp
1.181 -  with A show "gcd a b dvd d" by (rule dvd_trans)
1.182 -  show "normalize (gcd a b) = gcd a b"
1.183 -    by simp
1.184 -  fix l assume "l dvd c" and "l dvd d"
1.185 -  hence "l dvd gcd c d" by (rule gcd_greatest)
1.186 -  from this and B show "l dvd gcd a b" by (rule dvd_trans)
1.187 -qed
1.188 -
1.189 -lemma coprime_crossproduct:
1.190 -  assumes [simp]: "gcd a d = 1" "gcd b c = 1"
1.191 -  shows "normalize (a * c) = normalize (b * d) \<longleftrightarrow> normalize a  = normalize b \<and> normalize c = normalize d"
1.192 -    (is "?lhs \<longleftrightarrow> ?rhs")
1.193 -proof
1.194 -  assume ?rhs
1.195 -  then have "a dvd b" "b dvd a" "c dvd d" "d dvd c" by (simp_all add: associated_iff_dvd)
1.196 -  then have "a * c dvd b * d" "b * d dvd a * c" by (fast intro: mult_dvd_mono)+
1.197 -  then show ?lhs by (simp add: associated_iff_dvd)
1.198 -next
1.199 -  assume ?lhs
1.200 -  then have dvd: "a * c dvd b * d" "b * d dvd a * c" by (simp_all add: associated_iff_dvd)
1.201 -  then have "a dvd b * d" by (metis dvd_mult_left)
1.202 -  hence "a dvd b" by (simp add: coprime_dvd_mult_iff)
1.203 -  moreover from dvd have "b dvd a * c" by (metis dvd_mult_left)
1.204 -  hence "b dvd a" by (simp add: coprime_dvd_mult_iff)
1.205 -  moreover from dvd have "c dvd d * b"
1.206 -    by (auto dest: dvd_mult_right simp add: ac_simps)
1.207 -  hence "c dvd d" by (simp add: coprime_dvd_mult_iff gcd.commute)
1.208 -  moreover from dvd have "d dvd c * a"
1.209 -    by (auto dest: dvd_mult_right simp add: ac_simps)
1.210 -  hence "d dvd c" by (simp add: coprime_dvd_mult_iff gcd.commute)
1.211 -  ultimately show ?rhs by (simp add: associated_iff_dvd)
1.212 -qed
1.213 -
1.215 -  "gcd (m + n) n = gcd m n"
1.216 -  by (cases "n = 0", simp_all add: gcd_non_0)
1.217 -
1.219 -  "gcd m (m + n) = gcd m n"
1.221 -
1.223 -  "gcd m (k * m + n) = gcd m n"
1.224 -proof -
1.225 -  have "gcd m ((k * m + n) mod m) = gcd m (k * m + n)"
1.226 -    by (fact gcd_mod2)
1.227 -  then show ?thesis by simp
1.228 -qed
1.229 -
1.230 -lemma coprimeI: "(\<And>l. \<lbrakk>l dvd a; l dvd b\<rbrakk> \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd a b = 1"
1.231 -  by (rule sym, rule gcdI, simp_all)
1.232 -
1.233 -lemma coprime: "gcd a b = 1 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)"
1.234 -  by (auto intro: coprimeI gcd_greatest dvd_gcdD1 dvd_gcdD2)
1.235 -
1.236 -lemma div_gcd_coprime:
1.237 -  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
1.238 -  defines [simp]: "d \<equiv> gcd a b"
1.239 -  defines [simp]: "a' \<equiv> a div d" and [simp]: "b' \<equiv> b div d"
1.240 -  shows "gcd a' b' = 1"
1.241 -proof (rule coprimeI)
1.242 -  fix l assume "l dvd a'" "l dvd b'"
1.243 -  then obtain s t where "a' = l * s" "b' = l * t" unfolding dvd_def by blast
1.244 -  moreover have "a = a' * d" "b = b' * d" by simp_all
1.245 -  ultimately have "a = (l * d) * s" "b = (l * d) * t"
1.246 -    by (simp_all only: ac_simps)
1.247 -  hence "l*d dvd a" and "l*d dvd b" by (simp_all only: dvd_triv_left)
1.248 -  hence "l*d dvd d" by (simp add: gcd_greatest)
1.249 -  then obtain u where "d = l * d * u" ..
1.250 -  then have "d * (l * u) = d" by (simp add: ac_simps)
1.251 -  moreover from nz have "d \<noteq> 0" by simp
1.252 -  with div_mult_self1_is_id have "d * (l * u) div d = l * u" .
1.253 -  ultimately have "1 = l * u"
1.254 -    using \<open>d \<noteq> 0\<close> by simp
1.255 -  then show "l dvd 1" ..
1.256 -qed
1.257 -
1.258 -lemma coprime_lmult:
1.259 -  assumes dab: "gcd d (a * b) = 1"
1.260 -  shows "gcd d a = 1"
1.261 -proof (rule coprimeI)
1.262 -  fix l assume "l dvd d" and "l dvd a"
1.263 -  hence "l dvd a * b" by simp
1.264 -  with \<open>l dvd d\<close> and dab show "l dvd 1" by (auto intro: gcd_greatest)
1.265 -qed
1.266 -
1.267 -lemma coprime_rmult:
1.268 -  assumes dab: "gcd d (a * b) = 1"
1.269 -  shows "gcd d b = 1"
1.270 -proof (rule coprimeI)
1.271 -  fix l assume "l dvd d" and "l dvd b"
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_mul_eq: "gcd d (a * b) = 1 \<longleftrightarrow> gcd d a = 1 \<and> gcd d b = 1"
1.277 -  using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b] by blast
1.278 -
1.279 -lemma gcd_coprime:
1.280 -  assumes c: "gcd a b \<noteq> 0" and a: "a = a' * gcd a b" and b: "b = b' * gcd a b"
1.281 -  shows "gcd a' b' = 1"
1.282 -proof -
1.283 -  from c have "a \<noteq> 0 \<or> b \<noteq> 0" by simp
1.284 -  with div_gcd_coprime have "gcd (a div gcd a b) (b div gcd a b) = 1" .
1.285 -  also from assms have "a div gcd a b = a'" by (metis div_mult_self2_is_id)+
1.286 -  also from assms have "b div gcd a b = b'" by (metis div_mult_self2_is_id)+
1.287 -  finally show ?thesis .
1.288 -qed
1.289 -
1.290 -lemma coprime_power:
1.291 -  assumes "0 < n"
1.292 -  shows "gcd a (b ^ n) = 1 \<longleftrightarrow> gcd a b = 1"
1.293 -using assms proof (induct n)
1.294 -  case (Suc n) then show ?case
1.295 -    by (cases n) (simp_all add: coprime_mul_eq)
1.296 -qed simp
1.297 -
1.298 -lemma gcd_coprime_exists:
1.299 -  assumes nz: "gcd a b \<noteq> 0"
1.300 -  shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> gcd a' b' = 1"
1.301 -  apply (rule_tac x = "a div gcd a b" in exI)
1.302 -  apply (rule_tac x = "b div gcd a b" in exI)
1.303 -  apply (insert nz, auto intro: div_gcd_coprime)
1.304 -  done
1.305 -
1.306 -lemma coprime_exp:
1.307 -  "gcd d a = 1 \<Longrightarrow> gcd d (a^n) = 1"
1.308 -  by (induct n, simp_all add: coprime_mult)
1.309 -
1.310 -lemma gcd_exp:
1.311 -  "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
1.312 -proof (cases "a = 0 \<and> b = 0")
1.313 -  case True
1.314 -  then show ?thesis by (cases n) simp_all
1.315 -next
1.316 -  case False
1.317 -  then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
1.318 -    using coprime_exp2[OF div_gcd_coprime[of a b], of n n, symmetric] by simp
1.319 -  then have "gcd a b ^ n = gcd a b ^ n * ..." by simp
1.320 -  also note gcd_mult_distrib
1.321 -  also have "unit_factor (gcd a b ^ n) = 1"
1.322 -    using False by (auto simp add: unit_factor_power unit_factor_gcd)
1.323 -  also have "(gcd a b)^n * (a div gcd a b)^n = a^n"
1.324 -    by (subst ac_simps, subst div_power, simp, rule dvd_div_mult_self, rule dvd_power_same, simp)
1.325 -  also have "(gcd a b)^n * (b div gcd a b)^n = b^n"
1.326 -    by (subst ac_simps, subst div_power, simp, rule dvd_div_mult_self, rule dvd_power_same, simp)
1.327 -  finally show ?thesis by simp
1.328 -qed
1.329 -
1.330 -lemma coprime_common_divisor:
1.331 -  "gcd a b = 1 \<Longrightarrow> a dvd a \<Longrightarrow> a dvd b \<Longrightarrow> is_unit a"
1.332 -  apply (subgoal_tac "a dvd gcd a b")
1.333 -  apply simp
1.334 -  apply (erule (1) gcd_greatest)
1.335 -  done
1.336 -
1.337 -lemma division_decomp:
1.338 -  assumes dc: "a dvd b * c"
1.339 -  shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
1.340 -proof (cases "gcd a b = 0")
1.341 -  assume "gcd a b = 0"
1.342 -  hence "a = 0 \<and> b = 0" by simp
1.343 -  hence "a = 0 * c \<and> 0 dvd b \<and> c dvd c" by simp
1.344 -  then show ?thesis by blast
1.345 -next
1.346 -  let ?d = "gcd a b"
1.347 -  assume "?d \<noteq> 0"
1.348 -  from gcd_coprime_exists[OF this]
1.349 -    obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
1.350 -    by blast
1.351 -  from ab'(1) have "a' dvd a" unfolding dvd_def by blast
1.352 -  with dc have "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
1.353 -  from dc ab'(1,2) have "a'*?d dvd (b'*?d) * c" by simp
1.354 -  hence "?d * a' dvd ?d * (b' * c)" by (simp add: mult_ac)
1.355 -  with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c" by simp
1.356 -  with coprime_dvd_mult[OF ab'(3)]
1.357 -    have "a' dvd c" by (subst (asm) ac_simps, blast)
1.358 -  with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c" by (simp add: mult_ac)
1.359 -  then show ?thesis by blast
1.360 -qed
1.361 -
1.362 -lemma pow_divs_pow:
1.363 -  assumes ab: "a ^ n dvd b ^ n" and n: "n \<noteq> 0"
1.364 -  shows "a dvd b"
1.365 -proof (cases "gcd a b = 0")
1.366 -  assume "gcd a b = 0"
1.367 -  then show ?thesis by simp
1.368 -next
1.369 -  let ?d = "gcd a b"
1.370 -  assume "?d \<noteq> 0"
1.371 -  from n obtain m where m: "n = Suc m" by (cases n, simp_all)
1.372 -  from \<open>?d \<noteq> 0\<close> have zn: "?d ^ n \<noteq> 0" by (rule power_not_zero)
1.373 -  from gcd_coprime_exists[OF \<open>?d \<noteq> 0\<close>]
1.374 -    obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
1.375 -    by blast
1.376 -  from ab have "(a' * ?d) ^ n dvd (b' * ?d) ^ n"
1.377 -    by (simp add: ab'(1,2)[symmetric])
1.378 -  hence "?d^n * a'^n dvd ?d^n * b'^n"
1.379 -    by (simp only: power_mult_distrib ac_simps)
1.380 -  with zn have "a'^n dvd b'^n" by simp
1.381 -  hence "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m)
1.382 -  hence "a' dvd b'^m * b'" by (simp add: m ac_simps)
1.383 -  with coprime_dvd_mult[OF coprime_exp[OF ab'(3), of m]]
1.384 -    have "a' dvd b'" by (subst (asm) ac_simps, blast)
1.385 -  hence "a'*?d dvd b'*?d" by (rule mult_dvd_mono, simp)
1.386 -  with ab'(1,2) show ?thesis by simp
1.387 -qed
1.388 -
1.389 -lemma pow_divs_eq [simp]:
1.390 -  "n \<noteq> 0 \<Longrightarrow> a ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
1.391 -  by (auto intro: pow_divs_pow dvd_power_same)
1.392 -
1.393 -lemmas divs_mult = divides_mult
1.394 -
1.395 -lemma coprime_plus_one [simp]: "gcd (n + 1) n = 1"
1.396 -  by (subst add_commute, simp)
1.397 -
1.398 -lemma setprod_coprime [rule_format]:
1.399 -  "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
1.400 -  apply (cases "finite A")
1.401 -  apply (induct set: finite)
1.402 -  apply (auto simp add: gcd_mult_cancel)
1.403 -  done
1.404 -
1.405 -lemma listprod_coprime:
1.406 -  "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (listprod xs) y"
1.407 -  by (induction xs) (simp_all add: gcd_mult_cancel)
1.408 -
1.409 -lemma coprime_divisors:
1.410 -  assumes "d dvd a" "e dvd b" "gcd a b = 1"
1.411 -  shows "gcd d e = 1"
1.412 -proof -
1.413 -  from assms obtain k l where "a = d * k" "b = e * l"
1.414 -    unfolding dvd_def by blast
1.415 -  with assms have "gcd (d * k) (e * l) = 1" by simp
1.416 -  hence "gcd (d * k) e = 1" by (rule coprime_lmult)
1.417 -  also have "gcd (d * k) e = gcd e (d * k)" by (simp add: ac_simps)
1.418 -  finally have "gcd e d = 1" by (rule coprime_lmult)
1.419 -  then show ?thesis by (simp add: ac_simps)
1.420 -qed
1.421 -
1.422 -lemma invertible_coprime:
1.423 -  assumes "a * b mod m = 1"
1.424 -  shows "coprime a m"
1.425 -proof -
1.426 -  from assms have "coprime m (a * b mod m)"
1.427 -    by simp
1.428 -  then have "coprime m (a * b)"
1.429 -    by simp
1.430 -  then have "coprime m a"
1.431 -    by (rule coprime_lmult)
1.432 -  then show ?thesis
1.433 -    by (simp add: ac_simps)
1.434 -qed
1.435 -
1.436 -lemma lcm_gcd_prod:
1.437 -  "lcm a b * gcd a b = normalize (a * b)"
1.438 -  by (simp add: lcm_gcd)
1.439 -
1.440 -lemma lcm_zero:
1.441 -  "lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
1.442 -  by (fact lcm_eq_0_iff)
1.443 -
1.444 -lemmas lcm_0_iff = lcm_zero
1.445 -
1.446 -lemma gcd_lcm:
1.447 -  assumes "lcm a b \<noteq> 0"
1.448 -  shows "gcd a b = normalize (a * b) div lcm a b"
1.449 -proof -
1.450 -  have "lcm a b * gcd a b = normalize (a * b)"
1.451 -    by (fact lcm_gcd_prod)
1.452 -  with assms show ?thesis
1.453 -    by (metis nonzero_mult_divide_cancel_left)
1.454 -qed
1.455 -
1.456 -declare unit_factor_lcm [simp]
1.457 -
1.458 -lemma lcmI:
1.459 -  assumes "a dvd c" and "b dvd c" and "\<And>d. a dvd d \<Longrightarrow> b dvd d \<Longrightarrow> c dvd d"
1.460 -    and "normalize c = c"
1.461 -  shows "c = lcm a b"
1.462 -  by (rule associated_eqI) (auto simp: assms intro: lcm_least)
1.463 -
1.464 -lemma gcd_dvd_lcm [simp]:
1.465 -  "gcd a b dvd lcm a b"
1.466 -  using gcd_dvd2 by (rule dvd_lcmI2)
1.467 -
1.468 -lemmas lcm_0 = lcm_0_right
1.469 -
1.470 -lemma lcm_unique:
1.471 -  "a dvd d \<and> b dvd d \<and>
1.472 -  normalize d = d \<and>
1.473 -  (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
1.474 -  by rule (auto intro: lcmI simp: lcm_least lcm_zero)
1.475 -
1.476 -lemma lcm_coprime:
1.477 -  "gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)"
1.478 -  by (subst lcm_gcd) simp
1.479 -
1.480 -lemma lcm_proj1_if_dvd:
1.481 -  "b dvd a \<Longrightarrow> lcm a b = normalize a"
1.482 -  by (cases "a = 0") (simp, rule sym, rule lcmI, simp_all)
1.483 -
1.484 -lemma lcm_proj2_if_dvd:
1.485 -  "a dvd b \<Longrightarrow> lcm a b = normalize b"
1.486 -  using lcm_proj1_if_dvd [of a b] by (simp add: ac_simps)
1.487 -
1.488 -lemma lcm_proj1_iff:
1.489 -  "lcm m n = normalize m \<longleftrightarrow> n dvd m"
1.490 -proof
1.491 -  assume A: "lcm m n = normalize m"
1.492 -  show "n dvd m"
1.493 -  proof (cases "m = 0")
1.494 -    assume [simp]: "m \<noteq> 0"
1.495 -    from A have B: "m = lcm m n * unit_factor m"
1.496 -      by (simp add: unit_eq_div2)
1.497 -    show ?thesis by (subst B, simp)
1.498 -  qed simp
1.499 -next
1.500 -  assume "n dvd m"
1.501 -  then show "lcm m n = normalize m" by (rule lcm_proj1_if_dvd)
1.502 -qed
1.503 -
1.504 -lemma lcm_proj2_iff:
1.505 -  "lcm m n = normalize n \<longleftrightarrow> m dvd n"
1.506 -  using lcm_proj1_iff [of n m] by (simp add: ac_simps)
1.507 -
1.508  lemma euclidean_size_lcm_le1:
1.509    assumes "a \<noteq> 0" and "b \<noteq> 0"
1.510    shows "euclidean_size a \<le> euclidean_size (lcm a b)"
1.511  proof -
1.512    have "a dvd lcm a b" by (rule dvd_lcm1)
1.513    then obtain c where A: "lcm a b = a * c" ..
1.514 -  with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "c \<noteq> 0" by (auto simp: lcm_zero)
1.515 +  with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "c \<noteq> 0" by (auto simp: lcm_eq_0_iff)
1.516    then show ?thesis by (subst A, intro size_mult_mono)
1.517  qed
1.518
1.519 @@ -849,7 +379,7 @@
1.520    with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "euclidean_size (lcm a b) = euclidean_size a"
1.521      by (intro le_antisym, simp, intro euclidean_size_lcm_le1)
1.522    with assms have "lcm a b dvd a"
1.523 -    by (rule_tac dvd_euclidean_size_eq_imp_dvd) (auto simp: lcm_zero)
1.524 +    by (rule_tac dvd_euclidean_size_eq_imp_dvd) (auto simp: lcm_eq_0_iff)
1.525    hence "b dvd a" by (rule lcm_dvdD2)
1.526    with \<open>\<not>b dvd a\<close> show False by contradiction
1.527  qed
1.528 @@ -859,197 +389,14 @@
1.529    shows "euclidean_size b < euclidean_size (lcm a b)"
1.530    using assms euclidean_size_lcm_less1 [of a b] by (simp add: ac_simps)
1.531
1.532 -lemma lcm_mult_unit1:
1.533 -  "is_unit a \<Longrightarrow> lcm (b * a) c = lcm b c"
1.534 -  by (rule associated_eqI) (simp_all add: mult_unit_dvd_iff dvd_lcmI1)
1.535 -
1.536 -lemma lcm_mult_unit2:
1.537 -  "is_unit a \<Longrightarrow> lcm b (c * a) = lcm b c"
1.538 -  using lcm_mult_unit1 [of a c b] by (simp add: ac_simps)
1.539 -
1.540 -lemma lcm_div_unit1:
1.541 -  "is_unit a \<Longrightarrow> lcm (b div a) c = lcm b c"
1.542 -  by (erule is_unitE [of _ b]) (simp add: lcm_mult_unit1)
1.543 -
1.544 -lemma lcm_div_unit2:
1.545 -  "is_unit a \<Longrightarrow> lcm b (c div a) = lcm b c"
1.546 -  by (erule is_unitE [of _ c]) (simp add: lcm_mult_unit2)
1.547 -
1.548 -lemma normalize_lcm_left [simp]:
1.549 -  "lcm (normalize a) b = lcm a b"
1.550 -proof (cases "a = 0")
1.551 -  case True then show ?thesis
1.552 -    by simp
1.553 -next
1.554 -  case False then have "is_unit (unit_factor a)"
1.555 -    by simp
1.556 -  moreover have "normalize a = a div unit_factor a"
1.557 -    by simp
1.558 -  ultimately show ?thesis
1.559 -    by (simp only: lcm_div_unit1)
1.560 -qed
1.561 -
1.562 -lemma normalize_lcm_right [simp]:
1.563 -  "lcm a (normalize b) = lcm a b"
1.564 -  using normalize_lcm_left [of b a] by (simp add: ac_simps)
1.565 -
1.566 -lemma LcmI:
1.567 -  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.568 -    and "normalize b = b" shows "b = Lcm A"
1.569 -  by (rule associated_eqI) (auto simp: assms dvd_Lcm intro: Lcm_least)
1.570 -
1.571 -lemma Lcm_subset:
1.572 -  "A \<subseteq> B \<Longrightarrow> Lcm A dvd Lcm B"
1.573 -  by (blast intro: Lcm_least dvd_Lcm)
1.574 -
1.575 -lemma Lcm_Un:
1.576 -  "Lcm (A \<union> B) = lcm (Lcm A) (Lcm B)"
1.577 -  apply (rule lcmI)
1.578 -  apply (blast intro: Lcm_subset)
1.579 -  apply (blast intro: Lcm_subset)
1.580 -  apply (intro Lcm_least ballI, elim UnE)
1.581 -  apply (rule dvd_trans, erule dvd_Lcm, assumption)
1.582 -  apply (rule dvd_trans, erule dvd_Lcm, assumption)
1.583 -  apply simp
1.584 -  done
1.585 -
1.586 -lemma Lcm_no_units:
1.587 -  "Lcm A = Lcm (A - {a. is_unit a})"
1.588 -proof -
1.589 -  have "(A - {a. is_unit a}) \<union> {a\<in>A. is_unit a} = A" by blast
1.590 -  hence "Lcm A = lcm (Lcm (A - {a. is_unit a})) (Lcm {a\<in>A. is_unit a})"
1.591 -    by (simp add: Lcm_Un [symmetric])
1.592 -  also have "Lcm {a\<in>A. is_unit a} = 1" by (simp add: Lcm_1_iff)
1.593 -  finally show ?thesis by simp
1.594 -qed
1.595 -
1.596 -lemma Lcm_0_iff':
1.597 -  "Lcm A = 0 \<longleftrightarrow> \<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))"
1.598 -proof
1.599 -  assume "Lcm A = 0"
1.600 -  show "\<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))"
1.601 -  proof
1.602 -    assume ex: "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l)"
1.603 -    then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l\<^sub>0)" by blast
1.604 -    def n \<equiv> "LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
1.605 -    def l \<equiv> "SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
1.606 -    have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
1.607 -      apply (subst n_def)
1.608 -      apply (rule LeastI[of _ "euclidean_size l\<^sub>0"])
1.609 -      apply (rule exI[of _ l\<^sub>0])
1.610 -      apply (simp add: l\<^sub>0_props)
1.611 -      done
1.612 -    from someI_ex[OF this] have "l \<noteq> 0" unfolding l_def by simp_all
1.613 -    hence "normalize l \<noteq> 0" by simp
1.614 -    also from ex have "normalize l = Lcm A"
1.615 -       by (simp only: Lcm_Lcm_eucl Lcm_eucl_def n_def l_def if_True Let_def)
1.616 -    finally show False using \<open>Lcm A = 0\<close> by contradiction
1.617 -  qed
1.618 -qed (simp only: Lcm_Lcm_eucl Lcm_eucl_def if_False)
1.619 -
1.620 -lemma Lcm_no_multiple:
1.621 -  "(\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not>a dvd m)) \<Longrightarrow> Lcm A = 0"
1.622 -proof -
1.623 -  assume "\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not>a dvd m)"
1.624 -  hence "\<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))" by blast
1.625 -  then show "Lcm A = 0" by (simp only: Lcm_Lcm_eucl Lcm_eucl_def if_False)
1.626 -qed
1.627 -
1.628 -lemma Lcm_finite:
1.629 -  assumes "finite A"
1.630 -  shows "Lcm A = Finite_Set.fold lcm 1 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_lcm])
1.633 -
1.634 -lemma Lcm_set:
1.635 -  "Lcm (set xs) = foldl lcm 1 xs"
1.636 -  using comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm] Lcm_finite
1.637 -  by (simp add: foldl_conv_fold lcm.commute)
1.638 -
1.639  lemma Lcm_eucl_set [code]:
1.640    "Lcm_eucl (set xs) = foldl lcm_eucl 1 xs"
1.641    by (simp add: Lcm_Lcm_eucl [symmetric] lcm_lcm_eucl Lcm_set)
1.642
1.643 -lemma Lcm_singleton [simp]:
1.644 -  "Lcm {a} = normalize a"
1.645 -  by simp
1.646 -
1.647 -lemma Lcm_2 [simp]:
1.648 -  "Lcm {a,b} = lcm a b"
1.649 -  by simp
1.650 -
1.651 -lemma Lcm_coprime:
1.652 -  assumes "finite A" and "A \<noteq> {}"
1.653 -  assumes "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1"
1.654 -  shows "Lcm A = normalize (\<Prod>A)"
1.655 -using assms proof (induct rule: finite_ne_induct)
1.656 -  case (insert a A)
1.657 -  have "Lcm (insert a A) = lcm a (Lcm A)" by simp
1.658 -  also from insert have "Lcm A = normalize (\<Prod>A)" by blast
1.659 -  also have "lcm a \<dots> = lcm a (\<Prod>A)" by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
1.660 -  also from insert have "gcd a (\<Prod>A) = 1" by (subst gcd.commute, intro setprod_coprime) auto
1.661 -  with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
1.662 -    by (simp add: lcm_coprime)
1.663 -  finally show ?case .
1.664 -qed simp
1.665 -
1.666 -lemma Lcm_coprime':
1.667 -  "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.668 -    \<Longrightarrow> Lcm A = normalize (\<Prod>A)"
1.669 -  by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
1.670 -
1.671 -lemma unit_factor_Gcd [simp]: "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
1.672 -proof -
1.673 -  show "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
1.674 -    by (simp add: Gcd_Lcm unit_factor_Lcm)
1.675 -qed
1.676 -
1.677 -lemma GcdI:
1.678 -  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.679 -    and "normalize b = b"
1.680 -  shows "b = Gcd A"
1.681 -  by (rule associated_eqI) (auto simp: assms Gcd_dvd intro: Gcd_greatest)
1.682 -
1.683 -lemma Gcd_1:
1.684 -  "1 \<in> A \<Longrightarrow> Gcd A = 1"
1.685 -  by (auto intro!: Gcd_eq_1_I)
1.686 -
1.687 -lemma Gcd_finite:
1.688 -  assumes "finite A"
1.689 -  shows "Gcd A = Finite_Set.fold gcd 0 A"
1.690 -  by (induct rule: finite.induct[OF \<open>finite A\<close>])
1.691 -    (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd])
1.692 -
1.693 -lemma Gcd_set:
1.694 -  "Gcd (set xs) = foldl gcd 0 xs"
1.695 -  using comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd] Gcd_finite
1.696 -  by (simp add: foldl_conv_fold gcd.commute)
1.697 -
1.698  lemma Gcd_eucl_set [code]:
1.699    "Gcd_eucl (set xs) = foldl gcd_eucl 0 xs"
1.700    by (simp add: Gcd_Gcd_eucl [symmetric] gcd_gcd_eucl Gcd_set)
1.701
1.702 -lemma Gcd_singleton [simp]: "Gcd {a} = normalize a"
1.703 -  by simp
1.704 -
1.705 -lemma Gcd_2 [simp]: "Gcd {a,b} = gcd a b"
1.706 -  by simp
1.707 -
1.708 -
1.709 -definition pairwise_coprime where
1.710 -  "pairwise_coprime A = (\<forall>x y. x \<in> A \<and> y \<in> A \<and> x \<noteq> y \<longrightarrow> coprime x y)"
1.711 -
1.712 -lemma pairwise_coprimeI [intro?]:
1.713 -  "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y) \<Longrightarrow> pairwise_coprime A"
1.714 -  by (simp add: pairwise_coprime_def)
1.715 -
1.716 -lemma pairwise_coprimeD:
1.717 -  "pairwise_coprime A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y"
1.718 -  by (simp add: pairwise_coprime_def)
1.719 -
1.720 -lemma pairwise_coprime_subset: "pairwise_coprime A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> pairwise_coprime B"
1.721 -  by (force simp: pairwise_coprime_def)
1.722 -
1.723  end
1.724
1.725  text \<open>
1.726 @@ -1084,48 +431,6 @@
1.727  lemma bezout: "\<exists>s t. s * a + t * b = gcd a b"
1.728    using euclid_ext'_correct by blast
1.729
1.730 -lemma gcd_neg1 [simp]:
1.731 -  "gcd (-a) b = gcd a b"
1.732 -  by (rule sym, rule gcdI, simp_all add: gcd_greatest)
1.733 -
1.734 -lemma gcd_neg2 [simp]:
1.735 -  "gcd a (-b) = gcd a b"
1.736 -  by (rule sym, rule gcdI, simp_all add: gcd_greatest)
1.737 -
1.738 -lemma gcd_neg_numeral_1 [simp]:
1.739 -  "gcd (- numeral n) a = gcd (numeral n) a"
1.740 -  by (fact gcd_neg1)
1.741 -
1.742 -lemma gcd_neg_numeral_2 [simp]:
1.743 -  "gcd a (- numeral n) = gcd a (numeral n)"
1.744 -  by (fact gcd_neg2)
1.745 -
1.746 -lemma gcd_diff1: "gcd (m - n) n = gcd m n"
1.748 -
1.749 -lemma gcd_diff2: "gcd (n - m) n = gcd m n"
1.750 -  by (subst gcd_neg1[symmetric], simp only: minus_diff_eq gcd_diff1)
1.751 -
1.752 -lemma coprime_minus_one [simp]: "gcd (n - 1) n = 1"
1.753 -proof -
1.754 -  have "gcd (n - 1) n = gcd n (n - 1)" by (fact gcd.commute)
1.755 -  also have "\<dots> = gcd ((n - 1) + 1) (n - 1)" by simp
1.756 -  also have "\<dots> = 1" by (rule coprime_plus_one)
1.757 -  finally show ?thesis .
1.758 -qed
1.759 -
1.760 -lemma lcm_neg1 [simp]: "lcm (-a) b = lcm a b"
1.761 -  by (rule sym, rule lcmI, simp_all add: lcm_least lcm_zero)
1.762 -
1.763 -lemma lcm_neg2 [simp]: "lcm a (-b) = lcm a b"
1.764 -  by (rule sym, rule lcmI, simp_all add: lcm_least lcm_zero)
1.765 -
1.766 -lemma lcm_neg_numeral_1 [simp]: "lcm (- numeral n) a = lcm (numeral n) a"
1.767 -  by (fact lcm_neg1)
1.768 -
1.769 -lemma lcm_neg_numeral_2 [simp]: "lcm a (- numeral n) = lcm a (numeral n)"
1.770 -  by (fact lcm_neg2)
1.771 -
1.772  end
1.773
1.774
```