src/HOL/Number_Theory/Euclidean_Algorithm.thy
 changeset 59009 348561aa3869 parent 58953 2e19b392d9e3 child 59010 ec2b4270a502
```     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Nov 17 14:55:32 2014 +0100
1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Nov 17 14:55:33 2014 +0100
1.3 @@ -6,33 +6,6 @@
1.4  imports Complex_Main
1.5  begin
1.6
1.7 -lemma finite_int_set_iff_bounded_le:
1.8 -  "finite (N::int set) = (\<exists>m\<ge>0. \<forall>n\<in>N. abs n \<le> m)"
1.9 -proof
1.10 -  assume "finite (N::int set)"
1.11 -  hence "finite (nat ` abs ` N)" by (intro finite_imageI)
1.12 -  hence "\<exists>m. \<forall>n\<in>nat`abs`N. n \<le> m" by (simp add: finite_nat_set_iff_bounded_le)
1.13 -  then obtain m :: nat where "\<forall>n\<in>N. nat (abs n) \<le> nat (int m)" by auto
1.14 -  then show "\<exists>m\<ge>0. \<forall>n\<in>N. abs n \<le> m" by (intro exI[of _ "int m"]) (auto simp: nat_le_eq_zle)
1.15 -next
1.16 -  assume "\<exists>m\<ge>0. \<forall>n\<in>N. abs n \<le> m"
1.17 -  then obtain m where "m \<ge> 0" and "\<forall>n\<in>N. abs n \<le> m" by blast
1.18 -  hence "\<forall>n\<in>N. nat (abs n) \<le> nat m" by (auto simp: nat_le_eq_zle)
1.19 -  hence "\<forall>n\<in>nat`abs`N. n \<le> nat m" by (auto simp: nat_le_eq_zle)
1.20 -  hence A: "finite ((nat \<circ> abs)`N)" unfolding o_def
1.21 -      by (subst finite_nat_set_iff_bounded_le) blast
1.22 -  {
1.23 -    assume "\<not>finite N"
1.24 -    from pigeonhole_infinite[OF this A] obtain x
1.25 -       where "x \<in> N" and B: "~finite {a\<in>N. nat (abs a) = nat (abs x)}"
1.26 -       unfolding o_def by blast
1.27 -    have "{a\<in>N. nat (abs a) = nat (abs x)} \<subseteq> {x, -x}" by auto
1.28 -    hence "finite {a\<in>N. nat (abs a) = nat (abs x)}" by (rule finite_subset) simp
1.29 -    with B have False by contradiction
1.30 -  }
1.31 -  then show "finite N" by blast
1.32 -qed
1.33 -
1.34  context semiring_div
1.35  begin
1.36
1.37 @@ -46,32 +19,6 @@
1.38    finally show "setprod f A = f x * setprod f (A - {x})" .
1.39  qed
1.40
1.41 -lemma dvd_mult_cancel_left:
1.42 -  assumes "a \<noteq> 0" and "a * b dvd a * c"
1.43 -  shows "b dvd c"
1.44 -proof-
1.45 -  from assms(2) obtain k where "a * c = a * b * k" unfolding dvd_def by blast
1.46 -  hence "c * a = b * k * a" by (simp add: ac_simps)
1.47 -  hence "c * (a div a) = b * k * (a div a)" by (simp add: div_mult_swap)
1.48 -  also from `a \<noteq> 0` have "a div a = 1" by simp
1.49 -  finally show ?thesis by simp
1.50 -qed
1.51 -
1.52 -lemma dvd_mult_cancel_right:
1.53 -  "a \<noteq> 0 \<Longrightarrow> b * a dvd c * a \<Longrightarrow> b dvd c"
1.54 -  by (subst (asm) (1 2) ac_simps, rule dvd_mult_cancel_left)
1.55 -
1.56 -lemma nonzero_pow_nonzero:
1.57 -  "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
1.58 -  by (induct n) (simp_all add: no_zero_divisors)
1.59 -
1.60 -lemma zero_pow_zero: "n \<noteq> 0 \<Longrightarrow> 0 ^ n = 0"
1.61 -  by (cases n, simp_all)
1.62 -
1.63 -lemma pow_zero_iff:
1.64 -  "n \<noteq> 0 \<Longrightarrow> a^n = 0 \<longleftrightarrow> a = 0"
1.65 -  using nonzero_pow_nonzero zero_pow_zero by auto
1.66 -
1.67  end
1.68
1.69  context semiring_div
1.70 @@ -260,9 +207,9 @@
1.71      hence [simp]: "x dvd y" "y dvd x" using `associated x y`
1.72          unfolding associated_def by simp_all
1.73      hence "1 = x div y * (y div x)"
1.74 -      by (simp add: div_mult_swap dvd_div_mult_self)
1.75 +      by (simp add: div_mult_swap)
1.76      hence "is_unit (x div y)" unfolding is_unit_def by (rule dvdI)
1.77 -    moreover have "x = (x div y) * y" by (simp add: dvd_div_mult_self)
1.78 +    moreover have "x = (x div y) * y" by simp
1.79      ultimately show ?thesis by blast
1.80    qed
1.81  next
1.82 @@ -364,7 +311,7 @@
1.83    have "?nf (x div ?nf x) * ?nf (?nf x) = ?nf (x div ?nf x * ?nf x)"
1.85    also have "x div ?nf x * ?nf x = x" using `x \<noteq> 0`
1.86 -    by (simp add: dvd_div_mult_self)
1.87 +    by simp
1.88    also have "?nf (?nf x) = ?nf x" using `x \<noteq> 0`
1.89      normalisation_factor_is_unit normalisation_factor_unit by simp
1.90    finally show ?thesis using `x \<noteq> 0` and `?nf x \<noteq> 0`
1.91 @@ -653,7 +600,7 @@
1.92    also have "... = k * gcd x y div ?nf k"
1.93      by (metis dvd_div_mult dvd_eq_mod_eq_0 mod_0 normalisation_factor_dvd)
1.94    finally show ?thesis
1.95 -    by (simp add: ac_simps dvd_mult_div_cancel)
1.96 +    by simp
1.97  qed
1.98
1.99  lemma euclidean_size_gcd_le1 [simp]:
1.100 @@ -711,7 +658,7 @@
1.102    apply (rule gcd_dvd2)
1.103    apply (rule gcd_greatest, erule (1) gcd_greatest, assumption)
1.104 -  apply (simp add: gcd_zero)
1.105 +  apply simp
1.106    done
1.107
1.108  lemma gcd_left_idem: "gcd p (gcd p q) = gcd p q"
1.109 @@ -719,7 +666,7 @@
1.110    apply simp
1.111    apply (rule dvd_trans, rule gcd_dvd2, rule gcd_dvd2)
1.112    apply (rule gcd_greatest, assumption, erule gcd_greatest, assumption)
1.113 -  apply (simp add: gcd_zero)
1.114 +  apply simp
1.115    done
1.116
1.117  lemma comp_fun_idem_gcd: "comp_fun_idem gcd"
1.118 @@ -754,7 +701,7 @@
1.119    have "gcd c d dvd d" by simp
1.120    with A show "gcd a b dvd d" by (rule dvd_trans)
1.121    show "normalisation_factor (gcd a b) = (if gcd a b = 0 then 0 else 1)"
1.122 -    by (simp add: gcd_zero)
1.123 +    by simp
1.124    fix l assume "l dvd c" and "l dvd d"
1.125    hence "l dvd gcd c d" by (rule gcd_greatest)
1.126    from this and B show "l dvd gcd a b" by (rule dvd_trans)
1.127 @@ -786,10 +733,10 @@
1.128    moreover from `?lhs` have "b dvd a * c" unfolding associated_def by (metis dvd_mult_left)
1.129    hence "b dvd a" by (simp add: coprime_dvd_mult_iff)
1.130    moreover from `?lhs` have "c dvd d * b"
1.131 -    unfolding associated_def by (metis dvd_mult_right ac_simps)
1.132 +    unfolding associated_def by (auto dest: dvd_mult_right simp add: ac_simps)
1.133    hence "c dvd d" by (simp add: coprime_dvd_mult_iff gcd.commute)
1.134    moreover from `?lhs` have "d dvd c * a"
1.135 -    unfolding associated_def by (metis dvd_mult_right ac_simps)
1.136 +    unfolding associated_def by (auto dest: dvd_mult_right simp add: ac_simps)
1.137    hence "d dvd c" by (simp add: coprime_dvd_mult_iff gcd.commute)
1.138    ultimately show ?rhs unfolding associated_def by simp
1.139  qed
1.140 @@ -819,17 +766,18 @@
1.141  proof (rule coprimeI)
1.142    fix l assume "l dvd a'" "l dvd b'"
1.143    then obtain s t where "a' = l * s" "b' = l * t" unfolding dvd_def by blast
1.144 -  moreover have "a = a' * d" "b = b' * d" by (simp_all add: dvd_div_mult_self)
1.145 +  moreover have "a = a' * d" "b = b' * d" by simp_all
1.146    ultimately have "a = (l * d) * s" "b = (l * d) * t"
1.147 -    by (metis ac_simps)+
1.148 +    by (simp_all only: ac_simps)
1.149    hence "l*d dvd a" and "l*d dvd b" by (simp_all only: dvd_triv_left)
1.150    hence "l*d dvd d" by (simp add: gcd_greatest)
1.151 -  then obtain u where "u * l * d = d" unfolding dvd_def
1.152 -    by (metis ac_simps mult_assoc)
1.153 -  moreover from nz have "d \<noteq> 0" by (simp add: gcd_zero)
1.154 -  ultimately have "u * l = 1"
1.155 -    by (metis div_mult_self1_is_id div_self ac_simps)
1.156 -  then show "l dvd 1" by force
1.157 +  then obtain u where "d = l * d * u" ..
1.158 +  then have "d * (l * u) = d" by (simp add: ac_simps)
1.159 +  moreover from nz have "d \<noteq> 0" by simp
1.160 +  with div_mult_self1_is_id have "d * (l * u) div d = l * u" .
1.161 +  ultimately have "1 = l * u"
1.162 +    using `d \<noteq> 0` by simp
1.163 +  then show "l dvd 1" ..
1.164  qed
1.165
1.166  lemma coprime_mult:
1.167 @@ -866,7 +814,7 @@
1.168    assumes z: "gcd a b \<noteq> 0" and a: "a = a' * gcd a b" and b: "b = b' * gcd a b"
1.169    shows "gcd a' b' = 1"
1.170  proof -
1.171 -  from z have "a \<noteq> 0 \<or> b \<noteq> 0" by (simp add: gcd_zero)
1.172 +  from z have "a \<noteq> 0 \<or> b \<noteq> 0" by simp
1.173    with div_gcd_coprime have "gcd (a div gcd a b) (b div gcd a b) = 1" .
1.174    also from assms have "a div gcd a b = a'" by (metis div_mult_self2_is_id)+
1.175    also from assms have "b div gcd a b = b'" by (metis div_mult_self2_is_id)+
1.176 @@ -886,7 +834,7 @@
1.177    shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> gcd a' b' = 1"
1.178    apply (rule_tac x = "a div gcd a b" in exI)
1.179    apply (rule_tac x = "b div gcd a b" in exI)
1.180 -  apply (insert nz, auto simp add: dvd_div_mult gcd_0_left  gcd_zero intro: div_gcd_coprime)
1.181 +  apply (insert nz, auto intro: div_gcd_coprime)
1.182    done
1.183
1.184  lemma coprime_exp:
1.185 @@ -934,7 +882,7 @@
1.186    shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
1.187  proof (cases "gcd a b = 0")
1.188    assume "gcd a b = 0"
1.189 -  hence "a = 0 \<and> b = 0" by (simp add: gcd_zero)
1.190 +  hence "a = 0 \<and> b = 0" by simp
1.191    hence "a = 0 * c \<and> 0 dvd b \<and> c dvd c" by simp
1.192    then show ?thesis by blast
1.193  next
1.194 @@ -947,7 +895,7 @@
1.195    with dc have "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
1.196    from dc ab'(1,2) have "a'*?d dvd (b'*?d) * c" by simp
1.197    hence "?d * a' dvd ?d * (b' * c)" by (simp add: mult_ac)
1.198 -  with `?d \<noteq> 0` have "a' dvd b' * c" by (rule dvd_mult_cancel_left)
1.199 +  with `?d \<noteq> 0` have "a' dvd b' * c" by simp
1.200    with coprime_dvd_mult[OF ab'(3)]
1.201      have "a' dvd c" by (subst (asm) ac_simps, blast)
1.202    with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c" by (simp add: mult_ac)
1.203 @@ -959,12 +907,12 @@
1.204    shows "a dvd b"
1.205  proof (cases "gcd a b = 0")
1.206    assume "gcd a b = 0"
1.207 -  then show ?thesis by (simp add: gcd_zero)
1.208 +  then show ?thesis by simp
1.209  next
1.210    let ?d = "gcd a b"
1.211    assume "?d \<noteq> 0"
1.212    from n obtain m where m: "n = Suc m" by (cases n, simp_all)
1.213 -  from `?d \<noteq> 0` have zn: "?d ^ n \<noteq> 0" by (rule nonzero_pow_nonzero)
1.214 +  from `?d \<noteq> 0` have zn: "?d ^ n \<noteq> 0" by (rule power_not_zero)
1.215    from gcd_coprime_exists[OF `?d \<noteq> 0`]
1.216      obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
1.217      by blast
1.218 @@ -972,7 +920,7 @@
1.220    hence "?d^n * a'^n dvd ?d^n * b'^n"
1.221      by (simp only: power_mult_distrib ac_simps)
1.222 -  with zn have "a'^n dvd b'^n" by (rule dvd_mult_cancel_left)
1.223 +  with zn have "a'^n dvd b'^n" by simp
1.224    hence "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m)
1.225    hence "a' dvd b'^m * b'" by (simp add: m ac_simps)
1.226    with coprime_dvd_mult[OF coprime_exp[OF ab'(3), of m]]
1.227 @@ -1022,8 +970,18 @@
1.228  qed
1.229
1.230  lemma invertible_coprime:
1.231 -  "x * y mod m = 1 \<Longrightarrow> gcd x m = 1"
1.232 -  by (metis coprime_lmult gcd_1 ac_simps gcd_red)
1.233 +  assumes "x * y mod m = 1"
1.234 +  shows "coprime x m"
1.235 +proof -
1.236 +  from assms have "coprime m (x * y mod m)"
1.237 +    by simp
1.238 +  then have "coprime m (x * y)"
1.239 +    by simp
1.240 +  then have "coprime m x"
1.241 +    by (rule coprime_lmult)
1.242 +  then show ?thesis
1.243 +    by (simp add: ac_simps)
1.244 +qed
1.245
1.246  lemma lcm_gcd:
1.247    "lcm a b = a * b div (gcd a b * normalisation_factor (a*b))"
1.248 @@ -1108,7 +1066,7 @@
1.249    {
1.250      assume "a \<noteq> 0" "b \<noteq> 0"
1.251      hence "a * b div ?nf (a * b) \<noteq> 0" by (simp add: no_zero_divisors)
1.252 -    moreover from `a \<noteq> 0` and `b \<noteq> 0` have "gcd a b \<noteq> 0" by (simp add: gcd_zero)
1.253 +    moreover from `a \<noteq> 0` and `b \<noteq> 0` have "gcd a b \<noteq> 0" by simp
1.254      ultimately have "lcm a b \<noteq> 0" using lcm_gcd_prod[of a b] by (intro notI, simp)
1.255    } moreover {
1.256      assume "a = 0 \<or> b = 0"
1.257 @@ -1123,7 +1081,7 @@
1.258    assumes "lcm a b \<noteq> 0"
1.259    shows "gcd a b = a * b div (lcm a b * normalisation_factor (a * b))"
1.260  proof-
1.261 -  from assms have "gcd a b \<noteq> 0" by (simp add: gcd_zero lcm_zero)
1.262 +  from assms have "gcd a b \<noteq> 0" by (simp add: lcm_zero)
1.263    let ?c = "normalisation_factor (a*b)"
1.264    from `lcm a b \<noteq> 0` have "?c \<noteq> 0" by (intro notI, simp add: lcm_zero no_zero_divisors)
1.265    hence "is_unit ?c" by simp
1.266 @@ -1383,7 +1341,7 @@
1.267      {
1.268        fix l' assume "\<forall>x\<in>A. x dvd l'"
1.269        with `\<forall>x\<in>A. x dvd l` have "\<forall>x\<in>A. x dvd gcd l l'" by (auto intro: gcd_greatest)
1.270 -      moreover from `l \<noteq> 0` have "gcd l l' \<noteq> 0" by (simp add: gcd_zero)
1.271 +      moreover from `l \<noteq> 0` have "gcd l l' \<noteq> 0" by simp
1.272        ultimately have "\<exists>b. b \<noteq> 0 \<and> (\<forall>x\<in>A. x dvd b) \<and> euclidean_size b = euclidean_size (gcd l l')"
1.273          by (intro exI[of _ "gcd l l'"], auto)
1.274        hence "euclidean_size (gcd l l') \<ge> n" by (subst n_def) (rule Least_le)
1.275 @@ -1585,7 +1543,7 @@
1.276    then show "g' dvd Gcd A" by (simp add: Gcd_Lcm)
1.277  next
1.278    show "normalisation_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
1.279 -    by (simp add: Gcd_Lcm normalisation_factor_Lcm)
1.280 +    by (simp add: Gcd_Lcm)
1.281  qed
1.282
1.283  lemma GcdI:
1.284 @@ -1619,7 +1577,7 @@
1.285    fix l assume "l dvd a" and "l dvd Gcd A"
1.286    hence "\<forall>x\<in>A. l dvd x" by (blast intro: dvd_trans Gcd_dvd)
1.287    with `l dvd a` show "l dvd Gcd (insert a A)" by (force intro: Gcd_dvd)
1.288 -qed (auto intro: Gcd_dvd dvd_Gcd simp: normalisation_factor_Gcd)
1.289 +qed auto
1.290
1.291  lemma Gcd_finite:
1.292    assumes "finite A"
1.293 @@ -1653,11 +1611,11 @@
1.294
1.295  lemma gcd_neg1 [simp]:
1.296    "gcd (-x) y = gcd x y"
1.297 -  by (rule sym, rule gcdI, simp_all add: gcd_greatest gcd_zero)
1.298 +  by (rule sym, rule gcdI, simp_all add: gcd_greatest)
1.299
1.300  lemma gcd_neg2 [simp]:
1.301    "gcd x (-y) = gcd x y"
1.302 -  by (rule sym, rule gcdI, simp_all add: gcd_greatest gcd_zero)
1.303 +  by (rule sym, rule gcdI, simp_all add: gcd_greatest)
1.304
1.305  lemma gcd_neg_numeral_1 [simp]:
1.306    "gcd (- numeral n) x = gcd (numeral n) x"
```