# HG changeset patch # User nipkow # Date 1234090766 -3600 # Node ID 409138c4de1208a6324214c2b0bc2fd723772da6 # Parent b4919260eaecb3edd681a14b8489d4e6accd8e5c added noatps diff -r b4919260eaec -r 409138c4de12 src/HOL/Integration.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: diff -r b4919260eaec -r 409138c4de12 src/HOL/OrderedGroup.thy --- 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 diff -r b4919260eaec -r 409138c4de12 src/HOL/Ring_and_Field.thy --- 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 \ (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 \ (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 ..