added noatps
authornipkow
Sun Feb 08 11:59:26 2009 +0100 (2009-02-08)
changeset 29833409138c4de12
parent 29832 b4919260eaec
child 29834 3237cfd177f3
child 29849 a2baf1b221be
child 29867 0abd89253a0f
added noatps
src/HOL/Integration.thy
src/HOL/OrderedGroup.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/Integration.thy	Sat Feb 07 10:56:44 2009 +0100
     1.2 +++ b/src/HOL/Integration.thy	Sun Feb 08 11:59:26 2009 +0100
     1.3 @@ -558,7 +558,7 @@
     1.4  apply (frule partition_eq_bound)
     1.5  apply (drule_tac [2] partition_gt, auto)
     1.6  apply (metis linear not_less partition_rhs partition_rhs2)
     1.7 -apply (metis add_diff_inverse diff_is_0_eq le0 le_diff_conv nat_add_commute partition partition_eq_bound partition_rhs real_less_def termination_basic_simps(5))
     1.8 +apply (metis lemma_additivity1 order_less_trans partition_eq_bound partition_lb partition_rhs)
     1.9  done
    1.10  
    1.11  lemma lemma_additivity4_psize_eq:
     2.1 --- a/src/HOL/OrderedGroup.thy	Sat Feb 07 10:56:44 2009 +0100
     2.2 +++ b/src/HOL/OrderedGroup.thy	Sun Feb 08 11:59:26 2009 +0100
     2.3 @@ -598,12 +598,12 @@
     2.4  by (simp add: algebra_simps)
     2.5  
     2.6  text{*Legacy - use @{text algebra_simps} *}
     2.7 -lemmas group_simps = algebra_simps
     2.8 +lemmas group_simps[noatp] = algebra_simps
     2.9  
    2.10  end
    2.11  
    2.12  text{*Legacy - use @{text algebra_simps} *}
    2.13 -lemmas group_simps = algebra_simps
    2.14 +lemmas group_simps[noatp] = algebra_simps
    2.15  
    2.16  class ordered_ab_semigroup_add =
    2.17    linorder + pordered_ab_semigroup_add
    2.18 @@ -1310,9 +1310,9 @@
    2.19    add_less_le_mono add_le_less_mono add_strict_mono)
    2.20  
    2.21  text{*Simplification of @{term "x-y < 0"}, etc.*}
    2.22 -lemmas diff_less_0_iff_less [simp] = less_iff_diff_less_0 [symmetric]
    2.23 +lemmas diff_less_0_iff_less [simp, noatp] = less_iff_diff_less_0 [symmetric]
    2.24  lemmas diff_eq_0_iff_eq [simp, noatp] = eq_iff_diff_eq_0 [symmetric]
    2.25 -lemmas diff_le_0_iff_le [simp] = le_iff_diff_le_0 [symmetric]
    2.26 +lemmas diff_le_0_iff_le [simp, noatp] = le_iff_diff_le_0 [symmetric]
    2.27  
    2.28  ML {*
    2.29  structure ab_group_add_cancel = Abel_Cancel
     3.1 --- a/src/HOL/Ring_and_Field.thy	Sat Feb 07 10:56:44 2009 +0100
     3.2 +++ b/src/HOL/Ring_and_Field.thy	Sun Feb 08 11:59:26 2009 +0100
     3.3 @@ -232,8 +232,8 @@
     3.4  by (rule equals_zero_I) (simp add: right_distrib [symmetric]) 
     3.5  
     3.6  text{*Extract signs from products*}
     3.7 -lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
     3.8 -lemmas mult_minus_right [simp] = minus_mult_right [symmetric]
     3.9 +lemmas mult_minus_left [simp, noatp] = minus_mult_left [symmetric]
    3.10 +lemmas mult_minus_right [simp,noatp] = minus_mult_right [symmetric]
    3.11  
    3.12  lemma minus_mult_minus [simp]: "- a * - b = a * b"
    3.13  by simp
    3.14 @@ -247,11 +247,11 @@
    3.15  lemma left_diff_distrib[algebra_simps]: "(a - b) * c = a * c - b * c"
    3.16  by (simp add: left_distrib diff_minus)
    3.17  
    3.18 -lemmas ring_distribs =
    3.19 +lemmas ring_distribs[noatp] =
    3.20    right_distrib left_distrib left_diff_distrib right_diff_distrib
    3.21  
    3.22  text{*Legacy - use @{text algebra_simps} *}
    3.23 -lemmas ring_simps = algebra_simps
    3.24 +lemmas ring_simps[noatp] = algebra_simps
    3.25  
    3.26  lemma eq_add_iff1:
    3.27    "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
    3.28 @@ -263,7 +263,7 @@
    3.29  
    3.30  end
    3.31  
    3.32 -lemmas ring_distribs =
    3.33 +lemmas ring_distribs[noatp] =
    3.34    right_distrib left_distrib left_diff_distrib right_diff_distrib
    3.35  
    3.36  class comm_ring = comm_semiring + ab_group_add
    3.37 @@ -751,7 +751,7 @@
    3.38  subclass pordered_ab_group_add ..
    3.39  
    3.40  text{*Legacy - use @{text algebra_simps} *}
    3.41 -lemmas ring_simps = algebra_simps
    3.42 +lemmas ring_simps[noatp] = algebra_simps
    3.43  
    3.44  lemma less_add_iff1:
    3.45    "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
    3.46 @@ -960,7 +960,7 @@
    3.47  end
    3.48  
    3.49  text{*Legacy - use @{text algebra_simps} *}
    3.50 -lemmas ring_simps = algebra_simps
    3.51 +lemmas ring_simps[noatp] = algebra_simps
    3.52  
    3.53  
    3.54  class pordered_comm_ring = comm_ring + pordered_comm_semiring
    3.55 @@ -1107,7 +1107,7 @@
    3.56  
    3.57  text {* Simprules for comparisons where common factors can be cancelled. *}
    3.58  
    3.59 -lemmas mult_compare_simps =
    3.60 +lemmas mult_compare_simps[noatp] =
    3.61      mult_le_cancel_right mult_le_cancel_left
    3.62      mult_le_cancel_right1 mult_le_cancel_right2
    3.63      mult_le_cancel_left1 mult_le_cancel_left2
    3.64 @@ -1219,7 +1219,7 @@
    3.65  lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)"
    3.66  by (simp add: divide_inverse mult_ac)
    3.67  
    3.68 -lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
    3.69 +lemmas times_divide_eq[noatp] = times_divide_eq_right times_divide_eq_left
    3.70  
    3.71  lemma divide_divide_eq_right [simp,noatp]:
    3.72    "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
    3.73 @@ -1297,8 +1297,8 @@
    3.74  
    3.75  
    3.76  text{*The effect is to extract signs from divisions*}
    3.77 -lemmas divide_minus_left = minus_divide_left [symmetric]
    3.78 -lemmas divide_minus_right = minus_divide_right [symmetric]
    3.79 +lemmas divide_minus_left[noatp] = minus_divide_left [symmetric]
    3.80 +lemmas divide_minus_right[noatp] = minus_divide_right [symmetric]
    3.81  declare divide_minus_left [simp]   divide_minus_right [simp]
    3.82  
    3.83  lemma minus_divide_divide [simp]:
    3.84 @@ -1359,7 +1359,7 @@
    3.85  by (subst eq_divide_eq, simp)
    3.86  
    3.87  
    3.88 -lemmas field_eq_simps = algebra_simps
    3.89 +lemmas field_eq_simps[noatp] = algebra_simps
    3.90    (* pull / out*)
    3.91    add_divide_eq_iff divide_add_eq_iff
    3.92    diff_divide_eq_iff divide_diff_eq_iff
    3.93 @@ -1720,7 +1720,7 @@
    3.94  (for inequations). Can be too aggressive and is therefore separate from the
    3.95  more benign @{text algebra_simps}. *}
    3.96  
    3.97 -lemmas field_simps = field_eq_simps
    3.98 +lemmas field_simps[noatp] = field_eq_simps
    3.99    (* multiply ineqn *)
   3.100    pos_divide_less_eq neg_divide_less_eq
   3.101    pos_less_divide_eq neg_less_divide_eq
   3.102 @@ -1732,7 +1732,7 @@
   3.103  sign_simps} to @{text field_simps} because the former can lead to case
   3.104  explosions. *}
   3.105  
   3.106 -lemmas sign_simps = group_simps
   3.107 +lemmas sign_simps[noatp] = group_simps
   3.108    zero_less_mult_iff  mult_less_0_iff
   3.109  
   3.110  (* Only works once linear arithmetic is installed:
   3.111 @@ -1856,9 +1856,9 @@
   3.112  lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]
   3.113  lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
   3.114  
   3.115 -declare zero_less_divide_1_iff [simp]
   3.116 +declare zero_less_divide_1_iff [simp,noatp]
   3.117  declare divide_less_0_1_iff [simp,noatp]
   3.118 -declare zero_le_divide_1_iff [simp]
   3.119 +declare zero_le_divide_1_iff [simp,noatp]
   3.120  declare divide_le_0_1_iff [simp,noatp]
   3.121  
   3.122  
   3.123 @@ -2234,7 +2234,7 @@
   3.124    thus ?thesis by (simp add: ac cpos mult_strict_mono) 
   3.125  qed
   3.126  
   3.127 -lemmas eq_minus_self_iff = equal_neg_zero
   3.128 +lemmas eq_minus_self_iff[noatp] = equal_neg_zero
   3.129  
   3.130  lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_idom))"
   3.131    unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..