added noatps
authornipkow
Sun, 08 Feb 2009 11:59:26 +0100
changeset 29833 409138c4de12
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
--- a/src/HOL/Integration.thy	Sat Feb 07 10:56:44 2009 +0100
+++ b/src/HOL/Integration.thy	Sun Feb 08 11:59:26 2009 +0100
@@ -558,7 +558,7 @@
 apply (frule partition_eq_bound)
 apply (drule_tac [2] partition_gt, auto)
 apply (metis linear not_less partition_rhs partition_rhs2)
-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))
+apply (metis lemma_additivity1 order_less_trans partition_eq_bound partition_lb partition_rhs)
 done
 
 lemma lemma_additivity4_psize_eq:
--- a/src/HOL/OrderedGroup.thy	Sat Feb 07 10:56:44 2009 +0100
+++ b/src/HOL/OrderedGroup.thy	Sun Feb 08 11:59:26 2009 +0100
@@ -598,12 +598,12 @@
 by (simp add: algebra_simps)
 
 text{*Legacy - use @{text algebra_simps} *}
-lemmas group_simps = algebra_simps
+lemmas group_simps[noatp] = algebra_simps
 
 end
 
 text{*Legacy - use @{text algebra_simps} *}
-lemmas group_simps = algebra_simps
+lemmas group_simps[noatp] = algebra_simps
 
 class ordered_ab_semigroup_add =
   linorder + pordered_ab_semigroup_add
@@ -1310,9 +1310,9 @@
   add_less_le_mono add_le_less_mono add_strict_mono)
 
 text{*Simplification of @{term "x-y < 0"}, etc.*}
-lemmas diff_less_0_iff_less [simp] = less_iff_diff_less_0 [symmetric]
+lemmas diff_less_0_iff_less [simp, noatp] = less_iff_diff_less_0 [symmetric]
 lemmas diff_eq_0_iff_eq [simp, noatp] = eq_iff_diff_eq_0 [symmetric]
-lemmas diff_le_0_iff_le [simp] = le_iff_diff_le_0 [symmetric]
+lemmas diff_le_0_iff_le [simp, noatp] = le_iff_diff_le_0 [symmetric]
 
 ML {*
 structure ab_group_add_cancel = Abel_Cancel
--- a/src/HOL/Ring_and_Field.thy	Sat Feb 07 10:56:44 2009 +0100
+++ b/src/HOL/Ring_and_Field.thy	Sun Feb 08 11:59:26 2009 +0100
@@ -232,8 +232,8 @@
 by (rule equals_zero_I) (simp add: right_distrib [symmetric]) 
 
 text{*Extract signs from products*}
-lemmas mult_minus_left [simp] = minus_mult_left [symmetric]
-lemmas mult_minus_right [simp] = minus_mult_right [symmetric]
+lemmas mult_minus_left [simp, noatp] = minus_mult_left [symmetric]
+lemmas mult_minus_right [simp,noatp] = minus_mult_right [symmetric]
 
 lemma minus_mult_minus [simp]: "- a * - b = a * b"
 by simp
@@ -247,11 +247,11 @@
 lemma left_diff_distrib[algebra_simps]: "(a - b) * c = a * c - b * c"
 by (simp add: left_distrib diff_minus)
 
-lemmas ring_distribs =
+lemmas ring_distribs[noatp] =
   right_distrib left_distrib left_diff_distrib right_diff_distrib
 
 text{*Legacy - use @{text algebra_simps} *}
-lemmas ring_simps = algebra_simps
+lemmas ring_simps[noatp] = algebra_simps
 
 lemma eq_add_iff1:
   "a * e + c = b * e + d \<longleftrightarrow> (a - b) * e + c = d"
@@ -263,7 +263,7 @@
 
 end
 
-lemmas ring_distribs =
+lemmas ring_distribs[noatp] =
   right_distrib left_distrib left_diff_distrib right_diff_distrib
 
 class comm_ring = comm_semiring + ab_group_add
@@ -751,7 +751,7 @@
 subclass pordered_ab_group_add ..
 
 text{*Legacy - use @{text algebra_simps} *}
-lemmas ring_simps = algebra_simps
+lemmas ring_simps[noatp] = algebra_simps
 
 lemma less_add_iff1:
   "a * e + c < b * e + d \<longleftrightarrow> (a - b) * e + c < d"
@@ -960,7 +960,7 @@
 end
 
 text{*Legacy - use @{text algebra_simps} *}
-lemmas ring_simps = algebra_simps
+lemmas ring_simps[noatp] = algebra_simps
 
 
 class pordered_comm_ring = comm_ring + pordered_comm_semiring
@@ -1107,7 +1107,7 @@
 
 text {* Simprules for comparisons where common factors can be cancelled. *}
 
-lemmas mult_compare_simps =
+lemmas mult_compare_simps[noatp] =
     mult_le_cancel_right mult_le_cancel_left
     mult_le_cancel_right1 mult_le_cancel_right2
     mult_le_cancel_left1 mult_le_cancel_left2
@@ -1219,7 +1219,7 @@
 lemma times_divide_eq_left: "(b/c) * a = (b*a) / (c::'a::field)"
 by (simp add: divide_inverse mult_ac)
 
-lemmas times_divide_eq = times_divide_eq_right times_divide_eq_left
+lemmas times_divide_eq[noatp] = times_divide_eq_right times_divide_eq_left
 
 lemma divide_divide_eq_right [simp,noatp]:
   "a / (b/c) = (a*c) / (b::'a::{field,division_by_zero})"
@@ -1297,8 +1297,8 @@
 
 
 text{*The effect is to extract signs from divisions*}
-lemmas divide_minus_left = minus_divide_left [symmetric]
-lemmas divide_minus_right = minus_divide_right [symmetric]
+lemmas divide_minus_left[noatp] = minus_divide_left [symmetric]
+lemmas divide_minus_right[noatp] = minus_divide_right [symmetric]
 declare divide_minus_left [simp]   divide_minus_right [simp]
 
 lemma minus_divide_divide [simp]:
@@ -1359,7 +1359,7 @@
 by (subst eq_divide_eq, simp)
 
 
-lemmas field_eq_simps = algebra_simps
+lemmas field_eq_simps[noatp] = algebra_simps
   (* pull / out*)
   add_divide_eq_iff divide_add_eq_iff
   diff_divide_eq_iff divide_diff_eq_iff
@@ -1720,7 +1720,7 @@
 (for inequations). Can be too aggressive and is therefore separate from the
 more benign @{text algebra_simps}. *}
 
-lemmas field_simps = field_eq_simps
+lemmas field_simps[noatp] = field_eq_simps
   (* multiply ineqn *)
   pos_divide_less_eq neg_divide_less_eq
   pos_less_divide_eq neg_less_divide_eq
@@ -1732,7 +1732,7 @@
 sign_simps} to @{text field_simps} because the former can lead to case
 explosions. *}
 
-lemmas sign_simps = group_simps
+lemmas sign_simps[noatp] = group_simps
   zero_less_mult_iff  mult_less_0_iff
 
 (* Only works once linear arithmetic is installed:
@@ -1856,9 +1856,9 @@
 lemmas zero_le_divide_1_iff = zero_le_divide_iff [of 1, simplified]
 lemmas divide_le_0_1_iff = divide_le_0_iff [of 1, simplified]
 
-declare zero_less_divide_1_iff [simp]
+declare zero_less_divide_1_iff [simp,noatp]
 declare divide_less_0_1_iff [simp,noatp]
-declare zero_le_divide_1_iff [simp]
+declare zero_le_divide_1_iff [simp,noatp]
 declare divide_le_0_1_iff [simp,noatp]
 
 
@@ -2234,7 +2234,7 @@
   thus ?thesis by (simp add: ac cpos mult_strict_mono) 
 qed
 
-lemmas eq_minus_self_iff = equal_neg_zero
+lemmas eq_minus_self_iff[noatp] = equal_neg_zero
 
 lemma less_minus_self_iff: "(a < -a) = (a < (0::'a::ordered_idom))"
   unfolding order_less_le less_eq_neg_nonpos equal_neg_zero ..