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.84      by (simp add: normalisation_factor_mult)
    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.101    apply (simp add: ac_simps)
   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.219      by (simp add: ab'(1,2)[symmetric])
   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"