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.23    by (simp add: gcd_commute)
    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.32       apply (simp add: gcd_assoc)
    1.33       apply (simp add: gcd_commute)
    1.34      apply (simp_all add: mult_commute)
    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)
    1.78 +    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
    1.79    thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
    1.80  qed
    1.81  
    1.82 @@ -729,7 +734,7 @@
    1.83    assumes "k dvd j" shows "k dvd (zlcm i j)"
    1.84  proof -
    1.85    have "nat(abs k) dvd nat(abs j)" using `k dvd j`
    1.86 -    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric] zdvd_abs1)
    1.87 +    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
    1.88    thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
    1.89  qed
    1.90