# HG changeset patch # User paulson # Date 1124211191 -7200 # Node ID 5b57f995a17944ac96d339d00492c0bcefd81cc9 # Parent fb0a80aef0becc7551647c57f96b379594476801 more simprules now have names diff -r fb0a80aef0be -r 5b57f995a179 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Tue Aug 16 15:36:28 2005 +0200 +++ b/src/HOL/Divides.thy Tue Aug 16 18:53:11 2005 +0200 @@ -460,7 +460,7 @@ done (* Similar for "less than" *) -lemma div_less_dividend [rule_format, simp]: +lemma div_less_dividend [rule_format]: "!!n::nat. 1 0 < m --> m div n < m" apply (induct_tac m rule: nat_less_induct) apply (rename_tac "m") @@ -475,6 +475,8 @@ apply (simp_all) done +declare div_less_dividend [simp] + text{*A fact for the mutilated chess board*} lemma mod_Suc: "Suc(m) mod n = (if Suc(m mod n) = n then 0 else Suc(m mod n))" apply (case_tac "n=0", simp) diff -r fb0a80aef0be -r 5b57f995a179 src/HOL/Finite_Set.thy --- a/src/HOL/Finite_Set.thy Tue Aug 16 15:36:28 2005 +0200 +++ b/src/HOL/Finite_Set.thy Tue Aug 16 18:53:11 2005 +0200 @@ -2256,14 +2256,17 @@ text{* Now we instantiate the recursion equations and declare them simplification rules: *} -(* Making Min (resp. Max) a defined parameter of a locale suitably - extending ACIf could make the following interpretations more automatic. *) +(* Making Min or Max a defined parameter of a locale, suitably + extending ACIf, could make the following interpretations more automatic. *) -declare - fold1_singleton_def[OF Min_def, simp] - min.fold1_insert_idem_def[OF Min_def, simp] - fold1_singleton_def[OF Max_def, simp] - max.fold1_insert_idem_def[OF Max_def, simp] +lemmas Min_singleton = fold1_singleton_def [OF Min_def] +lemmas Max_singleton = fold1_singleton_def [OF Max_def] +lemmas Min_insert = min.fold1_insert_idem_def [OF Min_def] +lemmas Max_insert = max.fold1_insert_idem_def [OF Max_def] + +declare Min_singleton [simp] Max_singleton [simp] +declare Min_insert [simp] Max_insert [simp] + text{* Now we instantiate some @{text fold1} properties: *} diff -r fb0a80aef0be -r 5b57f995a179 src/HOL/Integ/IntArith.thy --- a/src/HOL/Integ/IntArith.thy Tue Aug 16 15:36:28 2005 +0200 +++ b/src/HOL/Integ/IntArith.thy Tue Aug 16 18:53:11 2005 +0200 @@ -182,7 +182,9 @@ text{*This simplifies expressions of the form @{term "int n = z"} where z is an integer literal.*} -declare int_eq_iff [of _ "number_of v", standard, simp] +lemmas int_eq_iff_number_of = int_eq_iff [of _ "number_of v", standard] +declare int_eq_iff_number_of [simp] + lemma split_nat [arith_split]: "P(nat(i::int)) = ((\n. i = int n \ P n) & (i < 0 \ P 0))" diff -r fb0a80aef0be -r 5b57f995a179 src/HOL/Integ/IntDef.thy --- a/src/HOL/Integ/IntDef.thy Tue Aug 16 15:36:28 2005 +0200 +++ b/src/HOL/Integ/IntDef.thy Tue Aug 16 18:53:11 2005 +0200 @@ -658,16 +658,20 @@ done text{*Special cases where either operand is zero*} -declare of_int_le_iff [of 0, simplified, simp] -declare of_int_le_iff [of _ 0, simplified, simp] +lemmas of_int_0_le_iff = of_int_le_iff [of 0, simplified] +lemmas of_int_le_0_iff = of_int_le_iff [of _ 0, simplified] +declare of_int_0_le_iff [simp] +declare of_int_le_0_iff [simp] lemma of_int_less_iff [simp]: "(of_int w < (of_int z::'a::ordered_idom)) = (w < z)" by (simp add: linorder_not_le [symmetric]) text{*Special cases where either operand is zero*} -declare of_int_less_iff [of 0, simplified, simp] -declare of_int_less_iff [of _ 0, simplified, simp] +lemmas of_int_0_less_iff = of_int_less_iff [of 0, simplified] +lemmas of_int_less_0_iff = of_int_less_iff [of _ 0, simplified] +declare of_int_0_less_iff [simp] +declare of_int_less_0_iff [simp] text{*The ordering on the @{text comm_ring_1} is necessary. See @{text of_nat_eq_iff} above.*} @@ -676,8 +680,10 @@ by (simp add: order_eq_iff) text{*Special cases where either operand is zero*} -declare of_int_eq_iff [of 0, simplified, simp] -declare of_int_eq_iff [of _ 0, simplified, simp] +lemmas of_int_0_eq_iff = of_int_eq_iff [of 0, simplified] +lemmas of_int_eq_0_iff = of_int_eq_iff [of _ 0, simplified] +declare of_int_0_eq_iff [simp] +declare of_int_eq_0_iff [simp] lemma of_int_eq_id [simp]: "of_int = (id :: int => int)" proof @@ -756,11 +762,6 @@ (* int (Suc n) = 1 + int n *) declare int_Suc [simp] -text{*Simplification of @{term "x-y < 0"}, etc.*} -declare less_iff_diff_less_0 [symmetric, simp] -declare eq_iff_diff_eq_0 [symmetric, simp] -declare le_iff_diff_le_0 [symmetric, simp] - subsection{*More Properties of @{term setsum} and @{term setprod}*} diff -r fb0a80aef0be -r 5b57f995a179 src/HOL/Integ/IntDiv.thy --- a/src/HOL/Integ/IntDiv.thy Tue Aug 16 15:36:28 2005 +0200 +++ b/src/HOL/Integ/IntDiv.thy Tue Aug 16 18:53:11 2005 +0200 @@ -456,18 +456,48 @@ text {*Simplify expresions in which div and mod combine numerical constants*} -declare div_pos_pos [of "number_of v" "number_of w", standard, simp] -declare div_neg_pos [of "number_of v" "number_of w", standard, simp] -declare div_pos_neg [of "number_of v" "number_of w", standard, simp] -declare div_neg_neg [of "number_of v" "number_of w", standard, simp] +lemmas div_pos_pos_number_of = + div_pos_pos [of "number_of v" "number_of w", standard] +declare div_pos_pos_number_of [simp] + +lemmas div_neg_pos_number_of = + div_neg_pos [of "number_of v" "number_of w", standard] +declare div_neg_pos_number_of [simp] + +lemmas div_pos_neg_number_of = + div_pos_neg [of "number_of v" "number_of w", standard] +declare div_pos_neg_number_of [simp] + +lemmas div_neg_neg_number_of = + div_neg_neg [of "number_of v" "number_of w", standard] +declare div_neg_neg_number_of [simp] + + +lemmas mod_pos_pos_number_of = + mod_pos_pos [of "number_of v" "number_of w", standard] +declare mod_pos_pos_number_of [simp] -declare mod_pos_pos [of "number_of v" "number_of w", standard, simp] -declare mod_neg_pos [of "number_of v" "number_of w", standard, simp] -declare mod_pos_neg [of "number_of v" "number_of w", standard, simp] -declare mod_neg_neg [of "number_of v" "number_of w", standard, simp] +lemmas mod_neg_pos_number_of = + mod_neg_pos [of "number_of v" "number_of w", standard] +declare mod_neg_pos_number_of [simp] + +lemmas mod_pos_neg_number_of = + mod_pos_neg [of "number_of v" "number_of w", standard] +declare mod_pos_neg_number_of [simp] -declare posDivAlg_eqn [of "number_of v" "number_of w", standard, simp] -declare negDivAlg_eqn [of "number_of v" "number_of w", standard, simp] +lemmas mod_neg_neg_number_of = + mod_neg_neg [of "number_of v" "number_of w", standard] +declare mod_neg_neg_number_of [simp] + + +lemmas posDivAlg_eqn_number_of = + posDivAlg_eqn [of "number_of v" "number_of w", standard] +declare posDivAlg_eqn_number_of [simp] + +lemmas negDivAlg_eqn_number_of = + negDivAlg_eqn [of "number_of v" "number_of w", standard] +declare negDivAlg_eqn_number_of [simp] + text{*Special-case simplification *} @@ -493,13 +523,31 @@ (** The last remaining special cases for constant arithmetic: 1 div z and 1 mod z **) -declare div_pos_pos [OF int_0_less_1, of "number_of w", standard, simp] -declare div_pos_neg [OF int_0_less_1, of "number_of w", standard, simp] -declare mod_pos_pos [OF int_0_less_1, of "number_of w", standard, simp] -declare mod_pos_neg [OF int_0_less_1, of "number_of w", standard, simp] +lemmas div_pos_pos_1_number_of = + div_pos_pos [OF int_0_less_1, of "number_of w", standard] +declare div_pos_pos_1_number_of [simp] + +lemmas div_pos_neg_1_number_of = + div_pos_neg [OF int_0_less_1, of "number_of w", standard] +declare div_pos_neg_1_number_of [simp] + +lemmas mod_pos_pos_1_number_of = + mod_pos_pos [OF int_0_less_1, of "number_of w", standard] +declare mod_pos_pos_1_number_of [simp] -declare posDivAlg_eqn [of concl: 1 "number_of w", standard, simp] -declare negDivAlg_eqn [of concl: 1 "number_of w", standard, simp] +lemmas mod_pos_neg_1_number_of = + mod_pos_neg [OF int_0_less_1, of "number_of w", standard] +declare mod_pos_neg_1_number_of [simp] + + +lemmas posDivAlg_eqn_1_number_of = + posDivAlg_eqn [of concl: 1 "number_of w", standard] +declare posDivAlg_eqn_1_number_of [simp] + +lemmas negDivAlg_eqn_1_number_of = + negDivAlg_eqn [of concl: 1 "number_of w", standard] +declare negDivAlg_eqn_1_number_of [simp] + subsection{*Monotonicity in the First Argument (Dividend)*} diff -r fb0a80aef0be -r 5b57f995a179 src/HOL/Integ/NatBin.thy --- a/src/HOL/Integ/NatBin.thy Tue Aug 16 15:36:28 2005 +0200 +++ b/src/HOL/Integ/NatBin.thy Tue Aug 16 18:53:11 2005 +0200 @@ -284,7 +284,10 @@ done text{*Squares of literal numerals will be evaluated.*} -declare power2_eq_square [of "number_of w", standard, simp] +lemmas power2_eq_square_number_of = + power2_eq_square [of "number_of w", standard] +declare power2_eq_square_number_of [simp] + lemma zero_le_power2: "0 \ (a\::'a::{ordered_idom,recpower})" by (simp add: power2_eq_square zero_le_square) @@ -543,7 +546,9 @@ split add: split_if cong: imp_cong) -declare power_nat_number_of [of _ "number_of w", standard, simp] +lemmas power_nat_number_of_number_of = power_nat_number_of [of _ "number_of w", standard] +declare power_nat_number_of_number_of [simp] + text{*For the integers*} @@ -569,8 +574,14 @@ apply (auto simp add: nat_add_distrib nat_mult_distrib power_even_eq power2_eq_square neg_nat) done -declare zpower_number_of_even [of "number_of v", standard, simp] -declare zpower_number_of_odd [of "number_of v", standard, simp] +lemmas zpower_number_of_even_number_of = + zpower_number_of_even [of "number_of v", standard] +declare zpower_number_of_even_number_of [simp] + +lemmas zpower_number_of_odd_number_of = + zpower_number_of_odd [of "number_of v", standard] +declare zpower_number_of_odd_number_of [simp] + diff -r fb0a80aef0be -r 5b57f995a179 src/HOL/Integ/NatSimprocs.thy --- a/src/HOL/Integ/NatSimprocs.thy Tue Aug 16 15:36:28 2005 +0200 +++ b/src/HOL/Integ/NatSimprocs.thy Tue Aug 16 18:53:11 2005 +0200 @@ -151,8 +151,14 @@ lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n" by (simp add: Suc3_eq_add_3) -declare Suc_div_eq_add3_div [of _ "number_of v", standard, simp] -declare Suc_mod_eq_add3_mod [of _ "number_of v", standard, simp] +lemmas Suc_div_eq_add3_div_number_of = + Suc_div_eq_add3_div [of _ "number_of v", standard] +declare Suc_div_eq_add3_div_number_of [simp] + +lemmas Suc_mod_eq_add3_mod_number_of = + Suc_mod_eq_add3_mod [of _ "number_of v", standard] +declare Suc_mod_eq_add3_mod_number_of [simp] + subsection{*Special Simplification for Constants*} @@ -162,17 +168,39 @@ @{term number_of}*} text{*These distributive laws move literals inside sums and differences.*} -declare left_distrib [of _ _ "number_of v", standard, simp] -declare right_distrib [of "number_of v", standard, simp] +lemmas left_distrib_number_of = left_distrib [of _ _ "number_of v", standard] +declare left_distrib_number_of [simp] + +lemmas right_distrib_number_of = right_distrib [of "number_of v", standard] +declare right_distrib_number_of [simp] + -declare left_diff_distrib [of _ _ "number_of v", standard, simp] -declare right_diff_distrib [of "number_of v", standard, simp] +lemmas left_diff_distrib_number_of = + left_diff_distrib [of _ _ "number_of v", standard] +declare left_diff_distrib_number_of [simp] + +lemmas right_diff_distrib_number_of = + right_diff_distrib [of "number_of v", standard] +declare right_diff_distrib_number_of [simp] + text{*These are actually for fields, like real: but where else to put them?*} -declare zero_less_divide_iff [of "number_of w", standard, simp] -declare divide_less_0_iff [of "number_of w", standard, simp] -declare zero_le_divide_iff [of "number_of w", standard, simp] -declare divide_le_0_iff [of "number_of w", standard, simp] +lemmas zero_less_divide_iff_number_of = + zero_less_divide_iff [of "number_of w", standard] +declare zero_less_divide_iff_number_of [simp] + +lemmas divide_less_0_iff_number_of = + divide_less_0_iff [of "number_of w", standard] +declare divide_less_0_iff_number_of [simp] + +lemmas zero_le_divide_iff_number_of = + zero_le_divide_iff [of "number_of w", standard] +declare zero_le_divide_iff_number_of [simp] + +lemmas divide_le_0_iff_number_of = + divide_le_0_iff [of "number_of w", standard] +declare divide_le_0_iff_number_of [simp] + (**** IF times_divide_eq_right and times_divide_eq_left are removed as simprules, @@ -185,51 +213,119 @@ lemma times_recip_eq_left [simp]: "(1/c) * a = a / (c::'a::field)" by (simp add: times_divide_eq) -declare times_divide_eq_right [of "number_of w", standard, simp] -declare times_divide_eq_right [of _ _ "number_of w", standard, simp] -declare times_divide_eq_left [of _ "number_of w", standard, simp] -declare times_divide_eq_left [of _ _ "number_of w", standard, simp] +lemmas times_divide_eq_right_number_of = + times_divide_eq_right [of "number_of w", standard] +declare times_divide_eq_right_number_of [simp] + +lemmas times_divide_eq_right_number_of = + times_divide_eq_right [of _ _ "number_of w", standard] +declare times_divide_eq_right_number_of [simp] + +lemmas times_divide_eq_left_number_of = + times_divide_eq_left [of _ "number_of w", standard] +declare times_divide_eq_left_number_of [simp] + +lemmas times_divide_eq_left_number_of = + times_divide_eq_left [of _ _ "number_of w", standard] +declare times_divide_eq_left_number_of [simp] + ****) text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks strange, but then other simprocs simplify the quotient.*} -declare inverse_eq_divide [of "number_of w", standard, simp] +lemmas inverse_eq_divide_number_of = + inverse_eq_divide [of "number_of w", standard] +declare inverse_eq_divide_number_of [simp] + text{*These laws simplify inequalities, moving unary minus from a term into the literal.*} -declare less_minus_iff [of "number_of v", standard, simp] -declare le_minus_iff [of "number_of v", standard, simp] -declare equation_minus_iff [of "number_of v", standard, simp] +lemmas less_minus_iff_number_of = + less_minus_iff [of "number_of v", standard] +declare less_minus_iff_number_of [simp] + +lemmas le_minus_iff_number_of = + le_minus_iff [of "number_of v", standard] +declare le_minus_iff_number_of [simp] + +lemmas equation_minus_iff_number_of = + equation_minus_iff [of "number_of v", standard] +declare equation_minus_iff_number_of [simp] + -declare minus_less_iff [of _ "number_of v", standard, simp] -declare minus_le_iff [of _ "number_of v", standard, simp] -declare minus_equation_iff [of _ "number_of v", standard, simp] +lemmas minus_less_iff_number_of = + minus_less_iff [of _ "number_of v", standard] +declare minus_less_iff_number_of [simp] + +lemmas minus_le_iff_number_of = + minus_le_iff [of _ "number_of v", standard] +declare minus_le_iff_number_of [simp] + +lemmas minus_equation_iff_number_of = + minus_equation_iff [of _ "number_of v", standard] +declare minus_equation_iff_number_of [simp] + text{*These simplify inequalities where one side is the constant 1.*} -declare less_minus_iff [of 1, simplified, simp] -declare le_minus_iff [of 1, simplified, simp] -declare equation_minus_iff [of 1, simplified, simp] +lemmas less_minus_iff_1 = less_minus_iff [of 1, simplified] +declare less_minus_iff_1 [simp] + +lemmas le_minus_iff_1 = le_minus_iff [of 1, simplified] +declare le_minus_iff_1 [simp] + +lemmas equation_minus_iff_1 = equation_minus_iff [of 1, simplified] +declare equation_minus_iff_1 [simp] -declare minus_less_iff [of _ 1, simplified, simp] -declare minus_le_iff [of _ 1, simplified, simp] -declare minus_equation_iff [of _ 1, simplified, simp] +lemmas minus_less_iff_1 = minus_less_iff [of _ 1, simplified] +declare minus_less_iff_1 [simp] + +lemmas minus_le_iff_1 = minus_le_iff [of _ 1, simplified] +declare minus_le_iff_1 [simp] + +lemmas minus_equation_iff_1 = minus_equation_iff [of _ 1, simplified] +declare minus_equation_iff_1 [simp] + text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\"}) *} -declare mult_less_cancel_left [of "number_of v", standard, simp] -declare mult_less_cancel_right [of _ "number_of v", standard, simp] -declare mult_le_cancel_left [of "number_of v", standard, simp] -declare mult_le_cancel_right [of _ "number_of v", standard, simp] +lemmas mult_less_cancel_left_number_of = + mult_less_cancel_left [of "number_of v", standard] +declare mult_less_cancel_left_number_of [simp] + +lemmas mult_less_cancel_right_number_of = + mult_less_cancel_right [of _ "number_of v", standard] +declare mult_less_cancel_right_number_of [simp] + +lemmas mult_le_cancel_left_number_of = + mult_le_cancel_left [of "number_of v", standard] +declare mult_le_cancel_left_number_of [simp] + +lemmas mult_le_cancel_right_number_of = + mult_le_cancel_right [of _ "number_of v", standard] +declare mult_le_cancel_right_number_of [simp] + text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\"} and @{text "="}) *} -declare le_divide_eq [of _ _ "number_of w", standard, simp] -declare divide_le_eq [of _ "number_of w", standard, simp] -declare less_divide_eq [of _ _ "number_of w", standard, simp] -declare divide_less_eq [of _ "number_of w", standard, simp] -declare eq_divide_eq [of _ _ "number_of w", standard, simp] -declare divide_eq_eq [of _ "number_of w", standard, simp] +lemmas le_divide_eq_number_of = le_divide_eq [of _ _ "number_of w", standard] +declare le_divide_eq_number_of [simp] + +lemmas divide_le_eq_number_of = divide_le_eq [of _ "number_of w", standard] +declare divide_le_eq_number_of [simp] + +lemmas less_divide_eq_number_of = less_divide_eq [of _ _ "number_of w", standard] +declare less_divide_eq_number_of [simp] + +lemmas divide_less_eq_number_of = divide_less_eq [of _ "number_of w", standard] +declare divide_less_eq_number_of [simp] + +lemmas eq_divide_eq_number_of = eq_divide_eq [of _ _ "number_of w", standard] +declare eq_divide_eq_number_of [simp] + +lemmas divide_eq_eq_number_of = divide_eq_eq [of _ "number_of w", standard] +declare divide_eq_eq_number_of [simp] + subsection{*Optional Simplification Rules Involving Constants*} diff -r fb0a80aef0be -r 5b57f995a179 src/HOL/Integ/Parity.thy --- a/src/HOL/Integ/Parity.thy Tue Aug 16 15:36:28 2005 +0200 +++ b/src/HOL/Integ/Parity.thy Tue Aug 16 18:53:11 2005 +0200 @@ -367,14 +367,35 @@ (* Simplify, when the exponent is a numeral *) -declare power_0_left [of "number_of w", standard, simp] -declare zero_le_power_eq [of _ "number_of w", standard, simp] -declare zero_less_power_eq [of _ "number_of w", standard, simp] -declare power_le_zero_eq [of _ "number_of w", standard, simp] -declare power_less_zero_eq [of _ "number_of w", standard, simp] -declare zero_less_power_nat_eq [of _ "number_of w", standard, simp] -declare power_eq_0_iff [of _ "number_of w", standard, simp] -declare power_even_abs [of "number_of w" _, standard, simp] +lemmas power_0_left_number_of = power_0_left [of "number_of w", standard] +declare power_0_left_number_of [simp] + +lemmas zero_le_power_eq_number_of = + zero_le_power_eq [of _ "number_of w", standard] +declare zero_le_power_eq_number_of [simp] + +lemmas zero_less_power_eq_number_of = + zero_less_power_eq [of _ "number_of w", standard] +declare zero_less_power_eq_number_of [simp] + +lemmas power_le_zero_eq_number_of = + power_le_zero_eq [of _ "number_of w", standard] +declare power_le_zero_eq_number_of [simp] + +lemmas power_less_zero_eq_number_of = + power_less_zero_eq [of _ "number_of w", standard] +declare power_less_zero_eq_number_of [simp] + +lemmas zero_less_power_nat_eq_number_of = + zero_less_power_nat_eq [of _ "number_of w", standard] +declare zero_less_power_nat_eq_number_of [simp] + +lemmas power_eq_0_iff_number_of = power_eq_0_iff [of _ "number_of w", standard] +declare power_eq_0_iff_number_of [simp] + +lemmas power_even_abs_number_of = power_even_abs [of "number_of w" _, standard] +declare power_even_abs_number_of [simp] + subsection {* An Equivalence for @{term "0 \ a^n"} *} diff -r fb0a80aef0be -r 5b57f995a179 src/HOL/NatArith.thy --- a/src/HOL/NatArith.thy Tue Aug 16 15:36:28 2005 +0200 +++ b/src/HOL/NatArith.thy Tue Aug 16 18:53:11 2005 +0200 @@ -123,9 +123,9 @@ i - j - k = i - (j + k), k \ j ==> j - k + i = j + i - k, k \ j ==> i + (j - k) = i + j - k *) -declare diff_diff_left [simp] - diff_add_assoc [symmetric, simp] - diff_add_assoc2[symmetric, simp] +lemmas add_diff_assoc = diff_add_assoc [symmetric] +lemmas add_diff_assoc2 = diff_add_assoc2[symmetric] +declare diff_diff_left [simp] add_diff_assoc [simp] add_diff_assoc2[simp] text{*At present we prove no analogue of @{text not_less_Least} or @{text Least_Suc}, since there appears to be no need.*} @@ -206,16 +206,20 @@ by (blast intro: of_nat_less_imp_less less_imp_of_nat_less) text{*Special cases where either operand is zero*} -declare of_nat_less_iff [of 0, simplified, simp] -declare of_nat_less_iff [of _ 0, simplified, simp] +lemmas of_nat_0_less_iff = of_nat_less_iff [of 0, simplified] +lemmas of_nat_less_0_iff = of_nat_less_iff [of _ 0, simplified] +declare of_nat_0_less_iff [simp] +declare of_nat_less_0_iff [simp] lemma of_nat_le_iff [simp]: "(of_nat m \ (of_nat n::'a::ordered_semidom)) = (m \ n)" by (simp add: linorder_not_less [symmetric]) text{*Special cases where either operand is zero*} -declare of_nat_le_iff [of 0, simplified, simp] -declare of_nat_le_iff [of _ 0, simplified, simp] +lemmas of_nat_0_le_iff = of_nat_le_iff [of 0, simplified] +lemmas of_nat_le_0_iff = of_nat_le_iff [of _ 0, simplified] +declare of_nat_0_le_iff [simp] +declare of_nat_le_0_iff [simp] text{*The ordering on the @{text comm_semiring_1_cancel} is necessary to exclude the possibility of a finite field, which indeed wraps back to @@ -225,8 +229,10 @@ by (simp add: order_eq_iff) text{*Special cases where either operand is zero*} -declare of_nat_eq_iff [of 0, simplified, simp] -declare of_nat_eq_iff [of _ 0, simplified, simp] +lemmas of_nat_0_eq_iff = of_nat_eq_iff [of 0, simplified] +lemmas of_nat_eq_0_iff = of_nat_eq_iff [of _ 0, simplified] +declare of_nat_0_eq_iff [simp] +declare of_nat_eq_0_iff [simp] lemma of_nat_diff [simp]: "n \ m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::comm_ring_1)" diff -r fb0a80aef0be -r 5b57f995a179 src/HOL/OrderedGroup.thy --- a/src/HOL/OrderedGroup.thy Tue Aug 16 15:36:28 2005 +0200 +++ b/src/HOL/OrderedGroup.thy Tue Aug 16 18:53:11 2005 +0200 @@ -1021,6 +1021,15 @@ show ?thesis by (rule le_add_right_mono[OF 2 3]) qed +text{*Simplification of @{term "x-y < 0"}, etc.*} +lemmas diff_less_0_iff_less = less_iff_diff_less_0 [symmetric] +lemmas diff_eq_0_iff_eq = eq_iff_diff_eq_0 [symmetric] +lemmas diff_le_0_iff_le = le_iff_diff_le_0 [symmetric] +declare diff_less_0_iff_less [simp] +declare diff_eq_0_iff_eq [simp] +declare diff_le_0_iff_le [simp] + + ML {* val add_zero_left = thm"add_0"; val add_zero_right = thm"add_0_right"; diff -r fb0a80aef0be -r 5b57f995a179 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Tue Aug 16 15:36:28 2005 +0200 +++ b/src/HOL/Product_Type.thy Tue Aug 16 18:53:11 2005 +0200 @@ -269,7 +269,8 @@ -- {* Do not add as rewrite rule: invalidates some proofs in IMP *} by (cases p) simp -declare surjective_pairing [symmetric, simp] +lemmas pair_collapse = surjective_pairing [symmetric] +declare pair_collapse [simp] lemma surj_pair [simp]: "EX x y. z = (x, y)" apply (rule exI) diff -r fb0a80aef0be -r 5b57f995a179 src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Tue Aug 16 15:36:28 2005 +0200 +++ b/src/HOL/Ring_and_Field.thy Tue Aug 16 18:53:11 2005 +0200 @@ -429,7 +429,8 @@ text{*All three types of comparision involving 0 and 1 are covered.*} -declare zero_neq_one [THEN not_sym, simp] +lemmas one_neq_zero = zero_neq_one [THEN not_sym] +declare one_neq_zero [simp] lemma zero_le_one [simp]: "(0::'a::ordered_semidom) \ 1" by (rule zero_less_one [THEN order_less_imp_le]) @@ -1046,12 +1047,14 @@ text{*The effect is to extract signs from divisions*} -declare minus_divide_left [symmetric, simp] -declare minus_divide_right [symmetric, simp] +lemmas divide_minus_left = minus_divide_left [symmetric] +lemmas divide_minus_right = minus_divide_right [symmetric] +declare divide_minus_left [simp] divide_minus_right [simp] text{*Also, extract signs from products*} -declare minus_mult_left [symmetric, simp] -declare minus_mult_right [symmetric, simp] +lemmas mult_minus_left = minus_mult_left [symmetric] +lemmas mult_minus_right = minus_mult_right [symmetric] +declare mult_minus_left [simp] mult_minus_right [simp] lemma minus_divide_divide [simp]: "(-a)/(-b) = a / (b::'a::{field,division_by_zero})" @@ -1553,10 +1556,15 @@ done text{*Simplify expressions such as @{text "0 < 1/x"} to @{text "0 < x"}*} -declare zero_less_divide_iff [of "1", simp] -declare divide_less_0_iff [of "1", simp] -declare zero_le_divide_iff [of "1", simp] -declare divide_le_0_iff [of "1", simp] +lemmas zero_less_divide_1_iff = zero_less_divide_iff [of "1"] +lemmas divide_less_0_1_iff = divide_less_0_iff [of "1"] +lemmas zero_le_divide_1_iff = zero_le_divide_iff [of "1"] +lemmas divide_le_0_1_iff = divide_le_0_iff [of "1"] + +declare zero_less_divide_1_iff [simp] +declare divide_less_0_1_iff [simp] +declare zero_le_divide_1_iff [simp] +declare divide_le_0_1_iff [simp] subsection {* Ordering Rules for Division *} diff -r fb0a80aef0be -r 5b57f995a179 src/HOL/Set.thy --- a/src/HOL/Set.thy Tue Aug 16 15:36:28 2005 +0200 +++ b/src/HOL/Set.thy Tue Aug 16 18:53:11 2005 +0200 @@ -303,8 +303,8 @@ text {* Isomorphisms between predicates and sets. *} axioms - mem_Collect_eq [iff]: "(a : {x. P(x)}) = P(a)" - Collect_mem_eq [simp]: "{x. x:A} = A" + mem_Collect_eq: "(a : {x. P(x)}) = P(a)" + Collect_mem_eq: "{x. x:A} = A" defs Ball_def: "Ball A P == ALL x. x:A --> P(x)" @@ -334,6 +334,8 @@ subsubsection {* Relating predicates and sets *} +declare mem_Collect_eq [iff] Collect_mem_eq [simp] + lemma CollectI: "P(a) ==> a : {x. P(x)}" by simp