src/HOL/GCD.thy
changeset 30042 31039ee583fa
parent 29700 22faf21db3df
child 30082 43c5b7bfc791
     1.1 --- a/src/HOL/GCD.thy	Sat Feb 21 09:58:45 2009 +0100
     1.2 +++ b/src/HOL/GCD.thy	Sat Feb 21 20:52:30 2009 +0100
     1.3 @@ -156,7 +156,6 @@
     1.4       apply (simp add: gcd_assoc)
     1.5       apply (simp add: gcd_commute)
     1.6      apply (simp_all add: mult_commute)
     1.7 -  apply (blast intro: dvd_mult)
     1.8    done
     1.9  
    1.10  
    1.11 @@ -404,7 +403,7 @@
    1.12    {fix x y assume H: "a * x - b * y = d \<or> b * x - a * y = d"
    1.13      have dv: "?g dvd a*x" "?g dvd b * y" "?g dvd b*x" "?g dvd a * y"
    1.14        using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
    1.15 -    from dvd_diff[OF dv(1,2)] dvd_diff[OF dv(3,4)] H
    1.16 +    from nat_dvd_diff[OF dv(1,2)] nat_dvd_diff[OF dv(3,4)] H
    1.17      have ?rhs by auto}
    1.18    ultimately show ?thesis by blast
    1.19  qed
    1.20 @@ -597,8 +596,8 @@
    1.21    from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
    1.22    then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
    1.23    then show ?thesis
    1.24 -    apply (subst zdvd_abs1 [symmetric])
    1.25 -    apply (subst zdvd_abs2 [symmetric])
    1.26 +    apply (subst abs_dvd_iff [symmetric])
    1.27 +    apply (subst dvd_abs_iff [symmetric])
    1.28      apply (unfold dvd_def)
    1.29      apply (rule_tac x = "int h'" in exI, simp)
    1.30      done
    1.31 @@ -614,11 +613,11 @@
    1.32    let ?m' = "nat \<bar>m\<bar>"
    1.33    let ?n' = "nat \<bar>n\<bar>"
    1.34    from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
    1.35 -    unfolding zdvd_int by (simp_all only: int_nat_abs zdvd_abs1 zdvd_abs2)
    1.36 +    unfolding zdvd_int by (simp_all only: int_nat_abs abs_dvd_iff dvd_abs_iff)
    1.37    from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd zgcd m n"
    1.38      unfolding zgcd_def by (simp only: zdvd_int)
    1.39    then have "\<bar>k\<bar> dvd zgcd m n" by (simp only: int_nat_abs)
    1.40 -  then show "k dvd zgcd m n" by (simp add: zdvd_abs1)
    1.41 +  then show "k dvd zgcd m n" by simp
    1.42  qed
    1.43  
    1.44  lemma div_zgcd_relprime:
    1.45 @@ -721,7 +720,7 @@
    1.46    assumes "k dvd i" shows "k dvd (zlcm i j)"
    1.47  proof -
    1.48    have "nat(abs k) dvd nat(abs i)" using `k dvd i`
    1.49 -    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric] zdvd_abs1)
    1.50 +    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
    1.51    thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
    1.52  qed
    1.53  
    1.54 @@ -729,7 +728,7 @@
    1.55    assumes "k dvd j" shows "k dvd (zlcm i j)"
    1.56  proof -
    1.57    have "nat(abs k) dvd nat(abs j)" using `k dvd j`
    1.58 -    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric] zdvd_abs1)
    1.59 +    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
    1.60    thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
    1.61  qed
    1.62