src/HOL/GCD.thy
 changeset 30240 5b25fee0362c parent 29700 22faf21db3df child 30242 aea5d7fa7ef5
```     1.1 --- a/src/HOL/GCD.thy	Wed Mar 04 10:43:39 2009 +0100
1.2 +++ b/src/HOL/GCD.thy	Wed Mar 04 10:45:52 2009 +0100
1.3 @@ -60,9 +60,12 @@
1.4  lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd m n = gcd n (m mod n)"
1.5    by simp
1.6
1.7 -lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = 1"
1.8 +lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = Suc 0"
1.9    by simp
1.10
1.11 +lemma nat_gcd_1_right [simp, algebra]: "gcd m 1 = 1"
1.12 +  unfolding One_nat_def by (rule gcd_1)
1.13 +
1.14  declare gcd.simps [simp del]
1.15
1.16  text {*
1.17 @@ -116,9 +119,12 @@
1.18    apply (blast intro: dvd_trans)
1.19    done
1.20
1.21 -lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = 1"
1.22 +lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = Suc 0"
1.24
1.25 +lemma nat_gcd_1_left [simp, algebra]: "gcd 1 m = 1"
1.26 +  unfolding One_nat_def by (rule gcd_1_left)
1.27 +
1.28  text {*
1.29    \medskip Multiplication laws
1.30  *}
1.31 @@ -156,7 +162,6 @@
1.35 -  apply (blast intro: dvd_mult)
1.36    done
1.37
1.38
1.39 @@ -404,7 +409,7 @@
1.40    {fix x y assume H: "a * x - b * y = d \<or> b * x - a * y = d"
1.41      have dv: "?g dvd a*x" "?g dvd b * y" "?g dvd b*x" "?g dvd a * y"
1.42        using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
1.43 -    from dvd_diff[OF dv(1,2)] dvd_diff[OF dv(3,4)] H
1.44 +    from nat_dvd_diff[OF dv(1,2)] nat_dvd_diff[OF dv(3,4)] H
1.45      have ?rhs by auto}
1.46    ultimately show ?thesis by blast
1.47  qed
1.48 @@ -597,8 +602,8 @@
1.49    from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
1.50    then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
1.51    then show ?thesis
1.52 -    apply (subst zdvd_abs1 [symmetric])
1.53 -    apply (subst zdvd_abs2 [symmetric])
1.54 +    apply (subst abs_dvd_iff [symmetric])
1.55 +    apply (subst dvd_abs_iff [symmetric])
1.56      apply (unfold dvd_def)
1.57      apply (rule_tac x = "int h'" in exI, simp)
1.58      done
1.59 @@ -614,11 +619,11 @@
1.60    let ?m' = "nat \<bar>m\<bar>"
1.61    let ?n' = "nat \<bar>n\<bar>"
1.62    from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
1.63 -    unfolding zdvd_int by (simp_all only: int_nat_abs zdvd_abs1 zdvd_abs2)
1.64 +    unfolding zdvd_int by (simp_all only: int_nat_abs abs_dvd_iff dvd_abs_iff)
1.65    from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd zgcd m n"
1.66      unfolding zgcd_def by (simp only: zdvd_int)
1.67    then have "\<bar>k\<bar> dvd zgcd m n" by (simp only: int_nat_abs)
1.68 -  then show "k dvd zgcd m n" by (simp add: zdvd_abs1)
1.69 +  then show "k dvd zgcd m n" by simp
1.70  qed
1.71
1.72  lemma div_zgcd_relprime:
1.73 @@ -721,7 +726,7 @@
1.74    assumes "k dvd i" shows "k dvd (zlcm i j)"
1.75  proof -
1.76    have "nat(abs k) dvd nat(abs i)" using `k dvd i`
1.77 -    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric] zdvd_abs1)