src/HOL/NumberTheory/IntPrimes.thy
 changeset 13788 fd03c4ab89d4 parent 13630 a013a9dd370f child 13833 f8dcb1d9ea68
```--- a/src/HOL/NumberTheory/IntPrimes.thy	Mon Jan 27 10:39:31 2003 +0100
+++ b/src/HOL/NumberTheory/IntPrimes.thy	Tue Jan 28 07:39:29 2003 +0100
@@ -31,7 +31,6 @@
"xzgcda (m, n, r', r, s', s, t', t) =
(if r \<le> 0 then (r', s', t')
else xzgcda (m, n, r, r' mod r, s, s' - (r' div r) * s, t, t' - (r' div r) * t))"
-  (hints simp: pos_mod_bound)

constdefs
zgcd :: "int * int => int"
@@ -263,11 +262,10 @@

lemma zgcd_non_0: "0 < n ==> zgcd (m, n) = zgcd (n, m mod n)"
apply (frule_tac b = n and a = m in pos_mod_sign)
-  apply (simp add: zgcd_def zabs_def nat_mod_distrib)
+  apply (simp add: zgcd_def zabs_def nat_mod_distrib del:pos_mod_sign)
apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
apply (frule_tac a = m in pos_mod_bound)
-  apply (simp add: nat_diff_distrib gcd_diff2 nat_le_eq_zle)
-  apply (simp add: gcd_non_0 nat_mod_distrib [symmetric])
+  apply (simp add: nat_diff_distrib gcd_diff2 nat_le_eq_zle del:pos_mod_bound)
done

lemma zgcd_eq: "zgcd (m, n) = zgcd (n, m mod n)"
@@ -598,7 +596,7 @@
apply (unfold zcong_def dvd_def)
apply (rule_tac x = "a mod m" in exI)
-  apply (auto simp add: pos_mod_sign pos_mod_bound)
+  apply (auto)
apply (rule_tac x = "-(a div m)" in exI)
done
@@ -633,7 +631,7 @@
apply (rule_tac m = m in zcong_zless_imp_eq)
prefer 5
apply (subst zcong_zmod [symmetric])
-       apply (simp_all add: pos_mod_bound pos_mod_sign)
+       apply (simp_all)
apply (unfold zcong_def dvd_def)
apply (rule_tac x = "a div m - b div m" in exI)
apply (rule_tac m1 = m in zcong_zmod_aux [THEN trans])
@@ -659,7 +657,7 @@
apply (subst zcong_zmod_eq)
apply arith
apply (frule neg_mod_bound [of _ a], frule neg_mod_bound [of _ b])