src/HOL/GCD.thy

   by simp
 
 lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd m n = gcd n (m mod n)"
   by simp
 
-lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = 1"
+lemma gcd_1 [simp, algebra]: "gcd m (Suc 0) = Suc 0"
   by simp
+
+lemma nat_gcd_1_right [simp, algebra]: "gcd m 1 = 1"
+  unfolding One_nat_def by (rule gcd_1)
 
 declare gcd.simps [simp del]
 
 text {*
   \medskip @{term "gcd m n"} divides @{text m} and @{text n}.  The

    apply (rule is_gcd)
   apply (simp add: is_gcd_def)
   apply (blast intro: dvd_trans)
   done
 
-lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = 1"
+lemma gcd_1_left [simp, algebra]: "gcd (Suc 0) m = Suc 0"
   by (simp add: gcd_commute)
+
+lemma nat_gcd_1_left [simp, algebra]: "gcd 1 m = 1"
+  unfolding One_nat_def by (rule gcd_1_left)
 
 text {*
   \medskip Multiplication laws
 *}
 

    apply (rule gcd_greatest)
     apply (rule_tac n = k in relprime_dvd_mult)
      apply (simp add: gcd_assoc)
      apply (simp add: gcd_commute)
     apply (simp_all add: mult_commute)
-  apply (blast intro: dvd_mult)
   done
 
 
 text {* \medskip Addition laws *}
 

     hence ?lhs by blast}
   moreover
   {fix x y assume H: "a * x - b * y = d \<or> b * x - a * y = d"
     have dv: "?g dvd a*x" "?g dvd b * y" "?g dvd b*x" "?g dvd a * y"
       using dvd_mult2[OF gcd_dvd1[of a b]] dvd_mult2[OF gcd_dvd2[of a b]] by simp_all
-    from dvd_diff[OF dv(1,2)] dvd_diff[OF dv(3,4)] H
+    from nat_dvd_diff[OF dv(1,2)] nat_dvd_diff[OF dv(3,4)] H
     have ?rhs by auto}
   ultimately show ?thesis by blast
 qed
 
 lemma gcd_bezout_sum: assumes H:"a * x + b * y = d" shows "gcd a b dvd d"

   from relprime_dvd_mult [OF g th] obtain h' where h': "nat \<bar>k\<bar> = nat \<bar>i\<bar> * h'"
     unfolding dvd_def by blast
   from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
   then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
   then show ?thesis
-    apply (subst zdvd_abs1 [symmetric])
-    apply (subst zdvd_abs2 [symmetric])
+    apply (subst abs_dvd_iff [symmetric])
+    apply (subst dvd_abs_iff [symmetric])
     apply (unfold dvd_def)
     apply (rule_tac x = "int h'" in exI, simp)
     done
 qed
 

 proof -
   let ?k' = "nat \<bar>k\<bar>"
   let ?m' = "nat \<bar>m\<bar>"
   let ?n' = "nat \<bar>n\<bar>"
   from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
-    unfolding zdvd_int by (simp_all only: int_nat_abs zdvd_abs1 zdvd_abs2)
+    unfolding zdvd_int by (simp_all only: int_nat_abs abs_dvd_iff dvd_abs_iff)
   from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd zgcd m n"
     unfolding zgcd_def by (simp only: zdvd_int)
   then have "\<bar>k\<bar> dvd zgcd m n" by (simp only: int_nat_abs)
-  then show "k dvd zgcd m n" by (simp add: zdvd_abs1)
+  then show "k dvd zgcd m n" by simp
 qed
 
 lemma div_zgcd_relprime:
   assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
   shows "zgcd (a div (zgcd a b)) (b div (zgcd a b)) = 1"

 
 lemma dvd_imp_dvd_zlcm1:
   assumes "k dvd i" shows "k dvd (zlcm i j)"
 proof -
   have "nat(abs k) dvd nat(abs i)" using `k dvd i`
-    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric] zdvd_abs1)
+    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
   thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
 qed
 
 lemma dvd_imp_dvd_zlcm2:
   assumes "k dvd j" shows "k dvd (zlcm i j)"
 proof -
   have "nat(abs k) dvd nat(abs j)" using `k dvd j`
-    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric] zdvd_abs1)
+    by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric])
   thus ?thesis by(simp add:zlcm_def dvd_int_iff)(blast intro: dvd_trans)
 qed
 
 
 lemma zdvd_self_abs1: "(d::int) dvd (abs d)"