--- 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<n ==> 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)
--- 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: *}
--- 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)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
--- 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}*}
--- 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)*}
--- 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 \<le> (a\<twosuperior>::'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]
+
--- 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 "\<le>"}) *}
-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 "\<le>"} 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*}
--- 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 \<le> a^n"} *}
--- 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 \<le> j ==> j - k + i = j + i - k,
k \<le> 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 \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> 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 \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::comm_ring_1)"
--- 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";
--- 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)
--- 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) \<le> 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 *}
--- 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