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.214 -lemma gcd_add1 [simp]:
   1.215 -  "gcd (m + n) n = gcd m n"
   1.216 -  by (cases "n = 0", simp_all add: gcd_non_0)
   1.217 -
   1.218 -lemma gcd_add2 [simp]:
   1.219 -  "gcd m (m + n) = gcd m n"
   1.220 -  using gcd_add1 [of n m] by (simp add: ac_simps)
   1.221 -
   1.222 -lemma gcd_add_mult:
   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.747 -  by (subst diff_conv_add_uminus, subst gcd_neg2[symmetric],  subst gcd_add1, simp)
   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