src/HOL/NumberTheory/IntPrimes.thy
changeset 13788 fd03c4ab89d4
parent 13630 a013a9dd370f
child 13833 f8dcb1d9ea68
     1.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Mon Jan 27 10:39:31 2003 +0100
     1.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Tue Jan 28 07:39:29 2003 +0100
     1.3 @@ -31,7 +31,6 @@
     1.4    "xzgcda (m, n, r', r, s', s, t', t) =
     1.5      (if r \<le> 0 then (r', s', t')
     1.6       else xzgcda (m, n, r, r' mod r, s, s' - (r' div r) * s, t, t' - (r' div r) * t))"
     1.7 -  (hints simp: pos_mod_bound)
     1.8  
     1.9  constdefs
    1.10    zgcd :: "int * int => int"
    1.11 @@ -263,11 +262,10 @@
    1.12  
    1.13  lemma zgcd_non_0: "0 < n ==> zgcd (m, n) = zgcd (n, m mod n)"
    1.14    apply (frule_tac b = n and a = m in pos_mod_sign)
    1.15 -  apply (simp add: zgcd_def zabs_def nat_mod_distrib)
    1.16 +  apply (simp add: zgcd_def zabs_def nat_mod_distrib del:pos_mod_sign)
    1.17    apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
    1.18    apply (frule_tac a = m in pos_mod_bound)
    1.19 -  apply (simp add: nat_diff_distrib gcd_diff2 nat_le_eq_zle)
    1.20 -  apply (simp add: gcd_non_0 nat_mod_distrib [symmetric])
    1.21 +  apply (simp add: nat_diff_distrib gcd_diff2 nat_le_eq_zle del:pos_mod_bound)
    1.22    done
    1.23  
    1.24  lemma zgcd_eq: "zgcd (m, n) = zgcd (n, m mod n)"
    1.25 @@ -598,7 +596,7 @@
    1.26          simp add: zcong_sym)
    1.27    apply (unfold zcong_def dvd_def)
    1.28    apply (rule_tac x = "a mod m" in exI)
    1.29 -  apply (auto simp add: pos_mod_sign pos_mod_bound)
    1.30 +  apply (auto)
    1.31    apply (rule_tac x = "-(a div m)" in exI)
    1.32    apply (simp add:zdiff_eq_eq eq_zdiff_eq zadd_commute)
    1.33    done
    1.34 @@ -633,7 +631,7 @@
    1.35     apply (rule_tac m = m in zcong_zless_imp_eq)
    1.36         prefer 5
    1.37         apply (subst zcong_zmod [symmetric])
    1.38 -       apply (simp_all add: pos_mod_bound pos_mod_sign)
    1.39 +       apply (simp_all)
    1.40    apply (unfold zcong_def dvd_def)
    1.41    apply (rule_tac x = "a div m - b div m" in exI)
    1.42    apply (rule_tac m1 = m in zcong_zmod_aux [THEN trans])
    1.43 @@ -659,7 +657,7 @@
    1.44    apply (subst zcong_zmod_eq)
    1.45     apply arith
    1.46    apply (frule neg_mod_bound [of _ a], frule neg_mod_bound [of _ b]) 
    1.47 -  apply (simp add: zmod_zminus2_eq_if)
    1.48 +  apply (simp add: zmod_zminus2_eq_if del: neg_mod_bound)
    1.49    done
    1.50  
    1.51  subsection {* Modulo *}
    1.52 @@ -809,7 +807,7 @@
    1.53      apply auto
    1.54    apply (rule_tac x = "x * b mod n" in exI)
    1.55    apply safe
    1.56 -    apply (simp_all (no_asm_simp) add: pos_mod_bound pos_mod_sign)
    1.57 +    apply (simp_all (no_asm_simp))
    1.58    apply (subst zcong_zmod)
    1.59    apply (subst zmod_zmult1_eq [symmetric])
    1.60    apply (subst zcong_zmod [symmetric])