pos/neg_mod_sign/bound are now simp rules.
authornipkow
Tue Jan 28 07:39:29 2003 +0100 (2003-01-28)
changeset 13788fd03c4ab89d4
parent 13787 139c3bd8f7b2
child 13789 d37f66755f47
pos/neg_mod_sign/bound are now simp rules.
src/HOL/Integ/IntDiv.thy
src/HOL/NumberTheory/IntPrimes.thy
src/HOL/NumberTheory/WilsonRuss.thy
     1.1 --- a/src/HOL/Integ/IntDiv.thy	Mon Jan 27 10:39:31 2003 +0100
     1.2 +++ b/src/HOL/Integ/IntDiv.thy	Tue Jan 28 07:39:29 2003 +0100
     1.3 @@ -235,16 +235,16 @@
     1.4  apply (auto simp add: quorem_def mod_def)
     1.5  done
     1.6  
     1.7 -lemmas pos_mod_sign  = pos_mod_conj [THEN conjunct1, standard]
     1.8 -   and pos_mod_bound = pos_mod_conj [THEN conjunct2, standard]
     1.9 +lemmas pos_mod_sign[simp]  = pos_mod_conj [THEN conjunct1, standard]
    1.10 +   and pos_mod_bound[simp] = pos_mod_conj [THEN conjunct2, standard]
    1.11  
    1.12  lemma neg_mod_conj : "b < (0::int) ==> a mod b <= 0 & b < a mod b"
    1.13  apply (cut_tac a = a and b = b in divAlg_correct)
    1.14  apply (auto simp add: quorem_def div_def mod_def)
    1.15  done
    1.16  
    1.17 -lemmas neg_mod_sign  = neg_mod_conj [THEN conjunct1, standard]
    1.18 -   and neg_mod_bound = neg_mod_conj [THEN conjunct2, standard]
    1.19 +lemmas neg_mod_sign[simp]  = neg_mod_conj [THEN conjunct1, standard]
    1.20 +   and neg_mod_bound[simp] = neg_mod_conj [THEN conjunct2, standard]
    1.21  
    1.22  
    1.23  
    1.24 @@ -252,8 +252,7 @@
    1.25  
    1.26  lemma quorem_div_mod: "b ~= 0 ==> quorem ((a, b), (a div b, a mod b))"
    1.27  apply (cut_tac a = a and b = b in zmod_zdiv_equality)
    1.28 -apply (force simp add: quorem_def linorder_neq_iff pos_mod_sign pos_mod_bound
    1.29 -                       neg_mod_sign neg_mod_bound)
    1.30 +apply (force simp add: quorem_def linorder_neq_iff)
    1.31  done
    1.32  
    1.33  lemma quorem_div: "[| quorem((a,b),(q,r));  b ~= 0 |] ==> a div b = q"
    1.34 @@ -459,15 +458,17 @@
    1.35  
    1.36  lemma zmod_1 [simp]: "a mod (1::int) = 0"
    1.37  apply (cut_tac a = a and b = 1 in pos_mod_sign)
    1.38 -apply (cut_tac [2] a = a and b = 1 in pos_mod_bound, auto)
    1.39 -done 
    1.40 +apply (cut_tac [2] a = a and b = 1 in pos_mod_bound)
    1.41 +apply (auto simp del:pos_mod_bound pos_mod_sign)
    1.42 +done
    1.43  
    1.44  lemma zdiv_1 [simp]: "a div (1::int) = a"
    1.45  by (cut_tac a = a and b = 1 in zmod_zdiv_equality, auto)
    1.46  
    1.47  lemma zmod_minus1_right [simp]: "a mod (-1::int) = 0"
    1.48  apply (cut_tac a = a and b = "-1" in neg_mod_sign)
    1.49 -apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound, auto)
    1.50 +apply (cut_tac [2] a = a and b = "-1" in neg_mod_bound)
    1.51 +apply (auto simp del: neg_mod_sign neg_mod_bound)
    1.52  done
    1.53  
    1.54  lemma zdiv_minus1_right [simp]: "a div (-1::int) = -a"
    1.55 @@ -493,7 +494,7 @@
    1.56  apply (rule unique_quotient_lemma)
    1.57  apply (erule subst)
    1.58  apply (erule subst)
    1.59 -apply (simp_all add: pos_mod_sign pos_mod_bound)
    1.60 +apply (simp_all)
    1.61  done
    1.62  
    1.63  lemma zdiv_mono1_neg: "[| a <= a';  (b::int) < 0 |] ==> a' div b <= a div b"
    1.64 @@ -502,7 +503,7 @@
    1.65  apply (rule unique_quotient_lemma_neg)
    1.66  apply (erule subst)
    1.67  apply (erule subst)
    1.68 -apply (simp_all add: neg_mod_sign neg_mod_bound)
    1.69 +apply (simp_all)
    1.70  done
    1.71  
    1.72  
    1.73 @@ -538,7 +539,7 @@
    1.74  apply (rule zdiv_mono2_lemma)
    1.75  apply (erule subst)
    1.76  apply (erule subst)
    1.77 -apply (simp_all add: pos_mod_sign pos_mod_bound)
    1.78 +apply (simp_all)
    1.79  done
    1.80  
    1.81  lemma q_neg_lemma:
    1.82 @@ -569,7 +570,7 @@
    1.83  apply (rule zdiv_mono2_neg_lemma)
    1.84  apply (erule subst)
    1.85  apply (erule subst)
    1.86 -apply (simp_all add: pos_mod_sign pos_mod_bound)
    1.87 +apply (simp_all)
    1.88  done
    1.89  
    1.90  
    1.91 @@ -580,8 +581,7 @@
    1.92  lemma zmult1_lemma:
    1.93       "[| quorem((b,c),(q,r));  c ~= 0 |]  
    1.94        ==> quorem ((a*b, c), (a*q + a*r div c, a*r mod c))"
    1.95 -by (force simp add: split_ifs quorem_def linorder_neq_iff zadd_zmult_distrib2
    1.96 -                    pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound)
    1.97 +by (force simp add: split_ifs quorem_def linorder_neq_iff zadd_zmult_distrib2)
    1.98  
    1.99  lemma zdiv_zmult1_eq: "(a*b) div c = a*(b div c) + a*(b mod c) div (c::int)"
   1.100  apply (case_tac "c = 0", simp add: DIVISION_BY_ZERO)
   1.101 @@ -636,8 +636,7 @@
   1.102  lemma zadd1_lemma:
   1.103       "[| quorem((a,c),(aq,ar));  quorem((b,c),(bq,br));  c ~= 0 |]  
   1.104        ==> quorem ((a+b, c), (aq + bq + (ar+br) div c, (ar+br) mod c))"
   1.105 -by (force simp add: split_ifs quorem_def linorder_neq_iff zadd_zmult_distrib2
   1.106 -                    pos_mod_sign pos_mod_bound neg_mod_sign neg_mod_bound)
   1.107 +by (force simp add: split_ifs quorem_def linorder_neq_iff zadd_zmult_distrib2)
   1.108  
   1.109  (*NOT suitable for rewriting: the RHS has an instance of the LHS*)
   1.110  lemma zdiv_zadd1_eq:
   1.111 @@ -653,15 +652,12 @@
   1.112  
   1.113  lemma mod_div_trivial [simp]: "(a mod b) div b = (0::int)"
   1.114  apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
   1.115 -apply (auto simp add: linorder_neq_iff pos_mod_sign pos_mod_bound
   1.116 -            div_pos_pos_trivial neg_mod_sign neg_mod_bound div_neg_neg_trivial)
   1.117 +apply (auto simp add: linorder_neq_iff div_pos_pos_trivial div_neg_neg_trivial)
   1.118  done
   1.119  
   1.120  lemma mod_mod_trivial [simp]: "(a mod b) mod b = a mod (b::int)"
   1.121  apply (case_tac "b = 0", simp add: DIVISION_BY_ZERO)
   1.122 -apply (force simp add: linorder_neq_iff pos_mod_sign pos_mod_bound
   1.123 -                       mod_pos_pos_trivial neg_mod_sign neg_mod_bound 
   1.124 -                       mod_neg_neg_trivial)
   1.125 +apply (force simp add: linorder_neq_iff mod_pos_pos_trivial mod_neg_neg_trivial)
   1.126  done
   1.127  
   1.128  lemma zmod_zadd_left_eq: "(a+b) mod (c::int) = ((a mod c) + b) mod c"
   1.129 @@ -714,13 +710,13 @@
   1.130  lemma zmult2_lemma_aux2: "[| (0::int) < c;   b < r;  r <= 0 |] ==> b * (q mod c) + r <= 0"
   1.131  apply (subgoal_tac "b * (q mod c) <= 0")
   1.132   apply arith
   1.133 -apply (simp add: zmult_le_0_iff pos_mod_sign)
   1.134 +apply (simp add: zmult_le_0_iff)
   1.135  done
   1.136  
   1.137  lemma zmult2_lemma_aux3: "[| (0::int) < c;  0 <= r;  r < b |] ==> 0 <= b * (q mod c) + r"
   1.138  apply (subgoal_tac "0 <= b * (q mod c) ")
   1.139  apply arith
   1.140 -apply (simp add: int_0_le_mult_iff pos_mod_sign)
   1.141 +apply (simp add: int_0_le_mult_iff)
   1.142  done
   1.143  
   1.144  lemma zmult2_lemma_aux4: "[| (0::int) < c; 0 <= r; r < b |] ==> b * (q mod c) + r < b * c"
   1.145 @@ -811,7 +807,7 @@
   1.146  txt{*converse direction*}
   1.147  apply (drule_tac x = "n div k" in spec) 
   1.148  apply (drule_tac x = "n mod k" in spec) 
   1.149 -apply (simp add: pos_mod_bound pos_mod_sign) 
   1.150 +apply (simp)
   1.151  done
   1.152  
   1.153  lemma split_neg_lemma:
   1.154 @@ -826,7 +822,7 @@
   1.155  txt{*converse direction*}
   1.156  apply (drule_tac x = "n div k" in spec) 
   1.157  apply (drule_tac x = "n mod k" in spec) 
   1.158 -apply (simp add: neg_mod_bound neg_mod_sign) 
   1.159 +apply (simp)
   1.160  done
   1.161  
   1.162  lemma split_zdiv:
   1.163 @@ -879,7 +875,7 @@
   1.164  apply (subst div_pos_pos_trivial)
   1.165  apply (auto simp add: mod_pos_pos_trivial)
   1.166  apply (subgoal_tac "0 <= b mod a", arith)
   1.167 -apply (simp add: pos_mod_sign)
   1.168 +apply (simp)
   1.169  done
   1.170  
   1.171  
   1.172 @@ -929,7 +925,7 @@
   1.173  apply (rule mod_pos_pos_trivial)
   1.174  apply (auto simp add: mod_pos_pos_trivial)
   1.175  apply (subgoal_tac "0 <= b mod a", arith)
   1.176 -apply (simp add: pos_mod_sign)
   1.177 +apply (simp)
   1.178  done
   1.179  
   1.180  
     2.1 --- a/src/HOL/NumberTheory/IntPrimes.thy	Mon Jan 27 10:39:31 2003 +0100
     2.2 +++ b/src/HOL/NumberTheory/IntPrimes.thy	Tue Jan 28 07:39:29 2003 +0100
     2.3 @@ -31,7 +31,6 @@
     2.4    "xzgcda (m, n, r', r, s', s, t', t) =
     2.5      (if r \<le> 0 then (r', s', t')
     2.6       else xzgcda (m, n, r, r' mod r, s, s' - (r' div r) * s, t, t' - (r' div r) * t))"
     2.7 -  (hints simp: pos_mod_bound)
     2.8  
     2.9  constdefs
    2.10    zgcd :: "int * int => int"
    2.11 @@ -263,11 +262,10 @@
    2.12  
    2.13  lemma zgcd_non_0: "0 < n ==> zgcd (m, n) = zgcd (n, m mod n)"
    2.14    apply (frule_tac b = n and a = m in pos_mod_sign)
    2.15 -  apply (simp add: zgcd_def zabs_def nat_mod_distrib)
    2.16 +  apply (simp add: zgcd_def zabs_def nat_mod_distrib del:pos_mod_sign)
    2.17    apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if)
    2.18    apply (frule_tac a = m in pos_mod_bound)
    2.19 -  apply (simp add: nat_diff_distrib gcd_diff2 nat_le_eq_zle)
    2.20 -  apply (simp add: gcd_non_0 nat_mod_distrib [symmetric])
    2.21 +  apply (simp add: nat_diff_distrib gcd_diff2 nat_le_eq_zle del:pos_mod_bound)
    2.22    done
    2.23  
    2.24  lemma zgcd_eq: "zgcd (m, n) = zgcd (n, m mod n)"
    2.25 @@ -598,7 +596,7 @@
    2.26          simp add: zcong_sym)
    2.27    apply (unfold zcong_def dvd_def)
    2.28    apply (rule_tac x = "a mod m" in exI)
    2.29 -  apply (auto simp add: pos_mod_sign pos_mod_bound)
    2.30 +  apply (auto)
    2.31    apply (rule_tac x = "-(a div m)" in exI)
    2.32    apply (simp add:zdiff_eq_eq eq_zdiff_eq zadd_commute)
    2.33    done
    2.34 @@ -633,7 +631,7 @@
    2.35     apply (rule_tac m = m in zcong_zless_imp_eq)
    2.36         prefer 5
    2.37         apply (subst zcong_zmod [symmetric])
    2.38 -       apply (simp_all add: pos_mod_bound pos_mod_sign)
    2.39 +       apply (simp_all)
    2.40    apply (unfold zcong_def dvd_def)
    2.41    apply (rule_tac x = "a div m - b div m" in exI)
    2.42    apply (rule_tac m1 = m in zcong_zmod_aux [THEN trans])
    2.43 @@ -659,7 +657,7 @@
    2.44    apply (subst zcong_zmod_eq)
    2.45     apply arith
    2.46    apply (frule neg_mod_bound [of _ a], frule neg_mod_bound [of _ b]) 
    2.47 -  apply (simp add: zmod_zminus2_eq_if)
    2.48 +  apply (simp add: zmod_zminus2_eq_if del: neg_mod_bound)
    2.49    done
    2.50  
    2.51  subsection {* Modulo *}
    2.52 @@ -809,7 +807,7 @@
    2.53      apply auto
    2.54    apply (rule_tac x = "x * b mod n" in exI)
    2.55    apply safe
    2.56 -    apply (simp_all (no_asm_simp) add: pos_mod_bound pos_mod_sign)
    2.57 +    apply (simp_all (no_asm_simp))
    2.58    apply (subst zcong_zmod)
    2.59    apply (subst zmod_zmult1_eq [symmetric])
    2.60    apply (subst zcong_zmod [symmetric])
     3.1 --- a/src/HOL/NumberTheory/WilsonRuss.thy	Mon Jan 27 10:39:31 2003 +0100
     3.2 +++ b/src/HOL/NumberTheory/WilsonRuss.thy	Tue Jan 28 07:39:29 2003 +0100
     3.3 @@ -124,7 +124,7 @@
     3.4         apply (rule_tac [5] inv_not_1)
     3.5           apply auto
     3.6    apply (unfold inv_def zprime_def)
     3.7 -  apply (simp add: pos_mod_sign)
     3.8 +  apply (simp)
     3.9    done
    3.10  
    3.11  lemma inv_less_p_minus_1:
    3.12 @@ -134,7 +134,7 @@
    3.13     apply (simp add: inv_not_p_minus_1)
    3.14    apply auto
    3.15    apply (unfold inv_def zprime_def)
    3.16 -  apply (simp add: pos_mod_bound)
    3.17 +  apply (simp)
    3.18    done
    3.19  
    3.20  lemma inv_inv_aux: "5 \<le> p ==>
    3.21 @@ -170,7 +170,7 @@
    3.22           apply (rule_tac [4] zcong_zpower_zmult)
    3.23           apply (erule_tac [4] Little_Fermat)
    3.24           apply (rule_tac [4] zdvd_not_zless)
    3.25 -          apply (simp_all add: pos_mod_bound pos_mod_sign)
    3.26 +          apply (simp_all)
    3.27    done
    3.28  
    3.29