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.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)