# HG changeset patch
# User nipkow
# Date 1043735969 -3600
# Node ID fd03c4ab89d4e504abb8e8b2e9199536464d2417
# Parent  139c3bd8f7b2f32854ac80bc773285e615de249d
pos/neg_mod_sign/bound are now simp rules.

diff -r 139c3bd8f7b2 -r fd03c4ab89d4 src/HOL/Integ/IntDiv.thy
--- a/src/HOL/Integ/IntDiv.thy	Mon Jan 27 10:39:31 2003 +0100
+++ b/src/HOL/Integ/IntDiv.thy	Tue Jan 28 07:39:29 2003 +0100
@@ -235,16 +235,16 @@
 apply (auto simp add: quorem_def mod_def)
 done
 
-lemmas pos_mod_sign  = pos_mod_conj [THEN conjunct1, standard]
-   and pos_mod_bound = pos_mod_conj [THEN conjunct2, standard]
+lemmas pos_mod_sign[simp]  = pos_mod_conj [THEN conjunct1, standard]
+   and pos_mod_bound[simp] = pos_mod_conj [THEN conjunct2, standard]
 
 lemma neg_mod_conj : "b < (0::int) ==> a mod b <= 0 & b < a mod b"
 apply (cut_tac a = a and b = b in divAlg_correct)
 apply (auto simp add: quorem_def div_def mod_def)
 done
 
-lemmas neg_mod_sign  = neg_mod_conj [THEN conjunct1, standard]
-   and neg_mod_bound = neg_mod_conj [THEN conjunct2, standard]
+lemmas neg_mod_sign[simp]  = neg_mod_conj [THEN conjunct1, standard]
+   and neg_mod_bound[simp] = neg_mod_conj [THEN conjunct2, standard]
 
 
 
@@ -252,8 +252,7 @@
 
 lemma quorem_div_mod: "b ~= 0 ==> quorem ((a, b), (a div b, a mod b))"
 apply (cut_tac a = a and b = b in zmod_zdiv_equality)
-apply (force simp add: quorem_def linorder_neq_iff pos_mod_sign pos_mod_bound
-                       neg_mod_sign neg_mod_bound)
+apply (force simp add: quorem_def linorder_neq_iff)
 done
 
 lemma quorem_div: "[| quorem((a,b),(q,r));  b ~= 0 |] ==> a div b = q"
@@ -459,15 +458,17 @@
 
 lemma zmod_1 [simp]: "a mod (1::int) = 0"
 apply (cut_tac a = a and b = 1 in pos_mod_sign)
-apply (cut_tac [2] a = a and b = 1 in pos_mod_bound, auto)
-done 
+apply (cut_tac [2] a = a and b = 1 in pos_mod_bound)
+apply (auto simp del:pos_mod_bound pos_mod_sign)
+done
 
 lemma zdiv_1 [simp]: "a div (1::int) = a"
 by (cut_tac a = a and b = 1 in zmod_zdiv_equality, auto)
 
 lemma zmod_minus1_right [simp]: "a mod (-1::int) = 0"
 apply (cut_tac a = a and b = "-1" in neg_mod_sign)
-apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound, auto)
+apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound)
+apply (auto simp del: neg_mod_sign neg_mod_bound)
 done
 
 lemma zdiv_minus1_right [simp]: "a div (-1::int) = -a"
@@ -493,7 +494,7 @@
 apply (rule unique_quotient_lemma)
 apply (erule subst)
 apply (erule subst)
-apply (simp_all add: pos_mod_sign pos_mod_bound)
+apply (simp_all)
 done
 
 lemma zdiv_mono1_neg: "[| a <= a';  (b::int) < 0 |] ==> a' div b <= a div b"
@@ -502,7 +503,7 @@
 apply (rule unique_quotient_lemma_neg)
 apply (erule subst)
 apply (erule subst)
-apply (simp_all add: neg_mod_sign neg_mod_bound)
+apply (simp_all)
 done
 
 
@@ -538,7 +539,7 @@
 apply (rule zdiv_mono2_lemma)
 apply (erule subst)
 apply (erule subst)
-apply (simp_all add: pos_mod_sign pos_mod_bound)
+apply (simp_all)
 done
 
 lemma q_neg_lemma:
@@ -569,7 +570,7 @@
 apply (rule zdiv_mono2_neg_lemma)
 apply (erule subst)
 apply (erule subst)
-apply (simp_all add: pos_mod_sign pos_mod_bound)
+apply (simp_all)
 done
 
 
@@ -580,8 +581,7 @@
 lemma zmult1_lemma:
      "[| quorem((b,c),(q,r));  c ~= 0 |]  
       ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
-by (force simp add: split_ifs quorem_def linorder_neq_iff zadd_zmult_distrib2
-                    pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound)
+by (force simp add: split_ifs quorem_def linorder_neq_iff zadd_zmult_distrib2)
 
 lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
 apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
@@ -636,8 +636,7 @@
 lemma zadd1_lemma:
      "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  c ~= 0 |]  
       ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
-by (force simp add: split_ifs quorem_def linorder_neq_iff zadd_zmult_distrib2
-                    pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound)
+by (force simp add: split_ifs quorem_def linorder_neq_iff zadd_zmult_distrib2)
 
 (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
 lemma zdiv_zadd1_eq:
@@ -653,15 +652,12 @@
 
 lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)"
 apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
-apply (auto simp add: linorder_neq_iff pos_mod_sign pos_mod_bound
-            div_pos_pos_trivial neg_mod_sign neg_mod_bound div_neg_neg_trivial)
+apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
 done
 
 lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)"
 apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
-apply (force simp add: linorder_neq_iff pos_mod_sign pos_mod_bound
-                       mod_pos_pos_trivial neg_mod_sign neg_mod_bound 
-                       mod_neg_neg_trivial)
+apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
 done
 
 lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c"
@@ -714,13 +710,13 @@
 lemma zmult2_lemma_aux2: "[| (0::int) < c;   b < r;  r <= 0 |] ==> b * (q mod c) + r <= 0"
 apply (subgoal_tac "b * (q mod c) <= 0")
  apply arith
-apply (simp add: zmult_le_0_iff pos_mod_sign)
+apply (simp add: zmult_le_0_iff)
 done
 
 lemma zmult2_lemma_aux3: "[| (0::int) < c;  0 <= r;  r < b |] ==> 0 <= b * (q mod c) + r"
 apply (subgoal_tac "0 <= b * (q mod c) ")
 apply arith
-apply (simp add: int_0_le_mult_iff pos_mod_sign)
+apply (simp add: int_0_le_mult_iff)
 done
 
 lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 <= r; r < b |] ==> b * (q mod c) + r < b * c"
@@ -811,7 +807,7 @@
 txt{*converse direction*}
 apply (drule_tac x = "n div k" in spec) 
 apply (drule_tac x = "n mod k" in spec) 
-apply (simp add: pos_mod_bound pos_mod_sign) 
+apply (simp)
 done
 
 lemma split_neg_lemma:
@@ -826,7 +822,7 @@
 txt{*converse direction*}
 apply (drule_tac x = "n div k" in spec) 
 apply (drule_tac x = "n mod k" in spec) 
-apply (simp add: neg_mod_bound neg_mod_sign) 
+apply (simp)
 done
 
 lemma split_zdiv:
@@ -879,7 +875,7 @@
 apply (subst div_pos_pos_trivial)
 apply (auto simp add: mod_pos_pos_trivial)
 apply (subgoal_tac "0 <= b mod a", arith)
-apply (simp add: pos_mod_sign)
+apply (simp)
 done
 
 
@@ -929,7 +925,7 @@
 apply (rule mod_pos_pos_trivial)
 apply (auto simp add: mod_pos_pos_trivial)
 apply (subgoal_tac "0 <= b mod a", arith)
-apply (simp add: pos_mod_sign)
+apply (simp)
 done
 
 
diff -r 139c3bd8f7b2 -r fd03c4ab89d4 src/HOL/NumberTheory/IntPrimes.thy
--- 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 @@
         simp add: zcong_sym)
   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)
   apply (simp add:zdiff_eq_eq eq_zdiff_eq zadd_commute)
   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]) 
-  apply (simp add: zmod_zminus2_eq_if)
+  apply (simp add: zmod_zminus2_eq_if del: neg_mod_bound)
   done
 
 subsection {* Modulo *}
@@ -809,7 +807,7 @@
     apply auto
   apply (rule_tac x = "x * b mod n" in exI)
   apply safe
-    apply (simp_all (no_asm_simp) add: pos_mod_bound pos_mod_sign)
+    apply (simp_all (no_asm_simp))
   apply (subst zcong_zmod)
   apply (subst zmod_zmult1_eq [symmetric])
   apply (subst zcong_zmod [symmetric])
diff -r 139c3bd8f7b2 -r fd03c4ab89d4 src/HOL/NumberTheory/WilsonRuss.thy
--- a/src/HOL/NumberTheory/WilsonRuss.thy	Mon Jan 27 10:39:31 2003 +0100
+++ b/src/HOL/NumberTheory/WilsonRuss.thy	Tue Jan 28 07:39:29 2003 +0100
@@ -124,7 +124,7 @@
        apply (rule_tac [5] inv_not_1)
          apply auto
   apply (unfold inv_def zprime_def)
-  apply (simp add: pos_mod_sign)
+  apply (simp)
   done
 
 lemma inv_less_p_minus_1:
@@ -134,7 +134,7 @@
    apply (simp add: inv_not_p_minus_1)
   apply auto
   apply (unfold inv_def zprime_def)
-  apply (simp add: pos_mod_bound)
+  apply (simp)
   done
 
 lemma inv_inv_aux: "5 \<le> p ==>
@@ -170,7 +170,7 @@
          apply (rule_tac [4] zcong_zpower_zmult)
          apply (erule_tac [4] Little_Fermat)
          apply (rule_tac [4] zdvd_not_zless)
-          apply (simp_all add: pos_mod_bound pos_mod_sign)
+          apply (simp_all)
   done