--- a/src/HOL/Datatype.thy Sun Nov 20 21:07:06 2011 +0100
+++ b/src/HOL/Datatype.thy Sun Nov 20 21:07:10 2011 +0100
@@ -131,7 +131,7 @@
lemma Push_neq_K0: "Push (Inr (Suc k)) f = (%z. Inr 0) ==> P"
by (auto simp add: Push_def fun_eq_iff split: nat.split_asm)
-lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1, standard]
+lemmas Abs_Node_inj = Abs_Node_inject [THEN [2] rev_iffD1]
(*** Introduction rules for Node ***)
@@ -155,7 +155,7 @@
dest!: Abs_Node_inj
elim!: apfst_convE sym [THEN Push_neq_K0])
-lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym, standard]
+lemmas Atom_not_Scons [iff] = Scons_not_Atom [THEN not_sym]
(*** Injectiveness ***)
@@ -166,7 +166,7 @@
apply (simp add: Atom_def)
apply (blast intro!: inj_onI Node_K0_I dest!: Abs_Node_inj)
done
-lemmas Atom_inject = inj_Atom [THEN injD, standard]
+lemmas Atom_inject = inj_Atom [THEN injD]
lemma Atom_Atom_eq [iff]: "(Atom(a)=Atom(b)) = (a=b)"
by (blast dest!: Atom_inject)
@@ -177,7 +177,7 @@
apply (erule Atom_inject [THEN Inl_inject])
done
-lemmas Leaf_inject [dest!] = inj_Leaf [THEN injD, standard]
+lemmas Leaf_inject [dest!] = inj_Leaf [THEN injD]
lemma inj_Numb: "inj(Numb)"
apply (simp add: Numb_def o_def)
@@ -185,7 +185,7 @@
apply (erule Atom_inject [THEN Inr_inject])
done
-lemmas Numb_inject [dest!] = inj_Numb [THEN injD, standard]
+lemmas Numb_inject [dest!] = inj_Numb [THEN injD]
(** Injectiveness of Push_Node **)
@@ -235,14 +235,14 @@
lemma Scons_not_Leaf [iff]: "Scons M N \<noteq> Leaf(a)"
unfolding Leaf_def o_def by (rule Scons_not_Atom)
-lemmas Leaf_not_Scons [iff] = Scons_not_Leaf [THEN not_sym, standard]
+lemmas Leaf_not_Scons [iff] = Scons_not_Leaf [THEN not_sym]
(** Scons vs Numb **)
lemma Scons_not_Numb [iff]: "Scons M N \<noteq> Numb(k)"
unfolding Numb_def o_def by (rule Scons_not_Atom)
-lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym, standard]
+lemmas Numb_not_Scons [iff] = Scons_not_Numb [THEN not_sym]
(** Leaf vs Numb **)
@@ -250,7 +250,7 @@
lemma Leaf_not_Numb [iff]: "Leaf(a) \<noteq> Numb(k)"
by (simp add: Leaf_def Numb_def)
-lemmas Numb_not_Leaf [iff] = Leaf_not_Numb [THEN not_sym, standard]
+lemmas Numb_not_Leaf [iff] = Leaf_not_Numb [THEN not_sym]
(*** ndepth -- the depth of a node ***)
@@ -357,7 +357,7 @@
lemma In0_not_In1 [iff]: "In0(M) \<noteq> In1(N)"
unfolding In0_def In1_def One_nat_def by auto
-lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym, standard]
+lemmas In1_not_In0 [iff] = In0_not_In1 [THEN not_sym]
lemma In0_inject: "In0(M) = In0(N) ==> M=N"
by (simp add: In0_def)
@@ -503,7 +503,7 @@
lemma dprod_Sigma: "(dprod (A <*> B) (C <*> D)) <= (uprod A C) <*> (uprod B D)"
by blast
-lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma, standard]
+lemmas dprod_subset_Sigma = subset_trans [OF dprod_mono dprod_Sigma]
(*Dependent version*)
lemma dprod_subset_Sigma2:
@@ -514,7 +514,7 @@
lemma dsum_Sigma: "(dsum (A <*> B) (C <*> D)) <= (usum A C) <*> (usum B D)"
by blast
-lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma, standard]
+lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma]
text {* hides popular names *}
--- a/src/HOL/Divides.thy Sun Nov 20 21:07:06 2011 +0100
+++ b/src/HOL/Divides.thy Sun Nov 20 21:07:10 2011 +0100
@@ -1142,13 +1142,8 @@
lemma Suc_mod_eq_add3_mod: "(Suc (Suc (Suc m))) mod n = (3+m) mod n"
by (simp add: Suc3_eq_add_3)
-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]
+lemmas Suc_div_eq_add3_div_number_of [simp] = Suc_div_eq_add3_div [of _ "number_of v"] for v
+lemmas Suc_mod_eq_add3_mod_number_of [simp] = Suc_mod_eq_add3_mod [of _ "number_of v"] for v
lemma Suc_times_mod_eq: "1<k ==> Suc (k * m) mod k = 1"
@@ -1156,7 +1151,7 @@
apply (simp_all add: mod_Suc)
done
-declare Suc_times_mod_eq [of "number_of w", standard, simp]
+declare Suc_times_mod_eq [of "number_of w", simp] for w
lemma [simp]: "n div k \<le> (Suc n) div k"
by (simp add: div_le_mono)
@@ -1450,17 +1445,16 @@
apply (auto simp add: divmod_int_rel_def mod_int_def)
done
-lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1, standard]
- and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2, standard]
+lemmas pos_mod_sign [simp] = pos_mod_conj [THEN conjunct1]
+ and pos_mod_bound [simp] = pos_mod_conj [THEN conjunct2]
lemma neg_mod_conj : "b < (0::int) ==> a mod b \<le> 0 & b < a mod b"
apply (cut_tac a = a and b = b in divmod_int_correct)
apply (auto simp add: divmod_int_rel_def div_int_def mod_int_def)
done
-lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1, standard]
- and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2, standard]
-
+lemmas neg_mod_sign [simp] = neg_mod_conj [THEN conjunct1]
+ and neg_mod_bound [simp] = neg_mod_conj [THEN conjunct2]
subsubsection{*General Properties of div and mod*}
@@ -1728,11 +1722,8 @@
simproc_setup binary_int_mod ("number_of m mod number_of n :: int") =
{* K (divmod_proc @{thm int_mod_pos_eq} @{thm int_mod_neg_eq}) *}
-lemmas posDivAlg_eqn_number_of [simp] =
- posDivAlg_eqn [of "number_of v" "number_of w", standard]
-
-lemmas negDivAlg_eqn_number_of [simp] =
- negDivAlg_eqn [of "number_of v" "number_of w", standard]
+lemmas posDivAlg_eqn_number_of [simp] = posDivAlg_eqn [of "number_of v" "number_of w"] for v w
+lemmas negDivAlg_eqn_number_of [simp] = negDivAlg_eqn [of "number_of v" "number_of w"] for v w
text{*Special-case simplification *}
@@ -1749,25 +1740,12 @@
(** The last remaining special cases for constant arithmetic:
1 div z and 1 mod z **)
-lemmas div_pos_pos_1_number_of [simp] =
- div_pos_pos [OF zero_less_one, of "number_of w", standard]
-
-lemmas div_pos_neg_1_number_of [simp] =
- div_pos_neg [OF zero_less_one, of "number_of w", standard]
-
-lemmas mod_pos_pos_1_number_of [simp] =
- mod_pos_pos [OF zero_less_one, of "number_of w", standard]
-
-lemmas mod_pos_neg_1_number_of [simp] =
- mod_pos_neg [OF zero_less_one, of "number_of w", standard]
-
-
-lemmas posDivAlg_eqn_1_number_of [simp] =
- posDivAlg_eqn [of concl: 1 "number_of w", standard]
-
-lemmas negDivAlg_eqn_1_number_of [simp] =
- negDivAlg_eqn [of concl: 1 "number_of w", standard]
-
+lemmas div_pos_pos_1_number_of [simp] = div_pos_pos [OF zero_less_one, of "number_of w"] for w
+lemmas div_pos_neg_1_number_of [simp] = div_pos_neg [OF zero_less_one, of "number_of w"] for w
+lemmas mod_pos_pos_1_number_of [simp] = mod_pos_pos [OF zero_less_one, of "number_of w"] for w
+lemmas mod_pos_neg_1_number_of [simp] = mod_pos_neg [OF zero_less_one, of "number_of w"] for w
+lemmas posDivAlg_eqn_1_number_of [simp] = posDivAlg_eqn [of concl: 1 "number_of w"] for w
+lemmas negDivAlg_eqn_1_number_of [simp] = negDivAlg_eqn [of concl: 1 "number_of w"] for w
subsubsection{*Monotonicity in the First Argument (Dividend)*}
@@ -2069,8 +2047,8 @@
text {* Enable (lin)arith to deal with @{const div} and @{const mod}
when these are applied to some constant that is of the form
@{term "number_of k"}: *}
-declare split_zdiv [of _ _ "number_of k", standard, arith_split]
-declare split_zmod [of _ _ "number_of k", standard, arith_split]
+declare split_zdiv [of _ _ "number_of k", arith_split] for k
+declare split_zmod [of _ _ "number_of k", arith_split] for k
subsubsection{*Speeding up the Division Algorithm with Shifting*}
@@ -2257,7 +2235,7 @@
subsubsection {* The Divides Relation *}
lemmas zdvd_iff_zmod_eq_0_number_of [simp] =
- dvd_eq_mod_eq_0 [of "number_of x::int" "number_of y::int", standard]
+ dvd_eq_mod_eq_0 [of "number_of x" "number_of y"] for x y :: int
lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n"
by (rule dvd_mod) (* TODO: remove *)
@@ -2456,10 +2434,8 @@
else nat (1 mod number_of v'))"
by (simp del: nat_numeral_1_eq_1 add: numeral_1_eq_Suc_0 [symmetric])
-lemmas dvd_eq_mod_eq_0_number_of =
- dvd_eq_mod_eq_0 [of "number_of x" "number_of y", standard]
-
-declare dvd_eq_mod_eq_0_number_of [simp]
+lemmas dvd_eq_mod_eq_0_number_of [simp] =
+ dvd_eq_mod_eq_0 [of "number_of x" "number_of y"] for x y
subsubsection {* Nitpick *}
--- a/src/HOL/HOL.thy Sun Nov 20 21:07:06 2011 +0100
+++ b/src/HOL/HOL.thy Sun Nov 20 21:07:10 2011 +0100
@@ -494,7 +494,7 @@
apply assumption
done
-lemmas ccontr = FalseE [THEN classical, standard]
+lemmas ccontr = FalseE [THEN classical]
(*notE with premises exchanged; it discharges ~R so that it can be used to
make elimination rules*)
@@ -1445,8 +1445,8 @@
lemmas induct_atomize' = induct_forall_eq induct_implies_eq induct_conj_eq
lemmas induct_atomize = induct_atomize' induct_equal_eq
-lemmas induct_rulify' [symmetric, standard] = induct_atomize'
-lemmas induct_rulify [symmetric, standard] = induct_atomize
+lemmas induct_rulify' [symmetric] = induct_atomize'
+lemmas induct_rulify [symmetric] = induct_atomize
lemmas induct_rulify_fallback =
induct_forall_def induct_implies_def induct_equal_def induct_conj_def
induct_true_def induct_false_def
--- a/src/HOL/Hilbert_Choice.thy Sun Nov 20 21:07:06 2011 +0100
+++ b/src/HOL/Hilbert_Choice.thy Sun Nov 20 21:07:10 2011 +0100
@@ -554,7 +554,7 @@
apply (erule ex_has_least_nat)
done
-lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1, standard]
+lemmas LeastM_natI = LeastM_nat_lemma [THEN conjunct1]
lemma LeastM_nat_le: "P x ==> m (LeastM m P) <= (m x::nat)"
by (rule LeastM_nat_lemma [THEN conjunct2, THEN spec, THEN mp], assumption, assumption)
@@ -620,7 +620,7 @@
apply (erule ex_has_greatest_nat, assumption)
done
-lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1, standard]
+lemmas GreatestM_natI = GreatestM_nat_lemma [THEN conjunct1]
lemma GreatestM_nat_le:
"P x ==> \<forall>y. P y --> m y < b
--- a/src/HOL/Int.thy Sun Nov 20 21:07:06 2011 +0100
+++ b/src/HOL/Int.thy Sun Nov 20 21:07:10 2011 +0100
@@ -273,10 +273,11 @@
done
lemmas int_distrib =
- left_distrib [of "z1::int" "z2" "w", standard]
- right_distrib [of "w::int" "z1" "z2", standard]
- left_diff_distrib [of "z1::int" "z2" "w", standard]
- right_diff_distrib [of "w::int" "z1" "z2", standard]
+ left_distrib [of z1 z2 w]
+ right_distrib [of w z1 z2]
+ left_diff_distrib [of z1 z2 w]
+ right_diff_distrib [of w z1 z2]
+ for z1 z2 w :: int
subsection {* Embedding of the Integers into any @{text ring_1}: @{text of_int}*}
@@ -637,12 +638,9 @@
definition pred :: "int \<Rightarrow> int" where
"pred k = k - 1"
-lemmas
- max_number_of [simp] = max_def
- [of "number_of u" "number_of v", standard]
-and
- min_number_of [simp] = min_def
- [of "number_of u" "number_of v", standard]
+lemmas max_number_of [simp] = max_def [of "number_of u" "number_of v"]
+ and min_number_of [simp] = min_def [of "number_of u" "number_of v"]
+ for u v
-- {* unfolding @{text minx} and @{text max} on numerals *}
lemmas numeral_simps =
@@ -1178,8 +1176,7 @@
text {* Reduces @{term "a\<le>b"} to @{term "~ (b<a)"} for ALL numerals. *}
lemmas le_number_of_eq_not_less =
- linorder_not_less [of "number_of w" "number_of v", symmetric,
- standard]
+ linorder_not_less [of "number_of w" "number_of v", symmetric] for w v
text {* Absolute value (@{term abs}) *}
@@ -1199,12 +1196,12 @@
subsubsection {* Simplification of arithmetic operations on integer constants. *}
-lemmas arith_extra_simps [standard, simp] =
+lemmas arith_extra_simps [simp] =
number_of_add [symmetric]
number_of_minus [symmetric]
numeral_m1_eq_minus_1 [symmetric]
number_of_mult [symmetric]
- diff_number_of_eq abs_number_of
+ diff_number_of_eq abs_number_of
text {*
For making a minimal simpset, one must include these default simprules.
@@ -1465,34 +1462,34 @@
lemmas add_special =
one_add_one_is_two
- binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl, standard]
- binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1, standard]
+ binop_eq [of "op +", OF add_number_of_eq numeral_1_eq_1 refl]
+ binop_eq [of "op +", OF add_number_of_eq refl numeral_1_eq_1]
text{*Allow 1 on either or both sides (1-1 already simplifies to 0)*}
lemmas diff_special =
- binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl, standard]
- binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1, standard]
+ binop_eq [of "op -", OF diff_number_of_eq numeral_1_eq_1 refl]
+ binop_eq [of "op -", OF diff_number_of_eq refl numeral_1_eq_1]
text{*Allow 0 or 1 on either side with a binary numeral on the other*}
lemmas eq_special =
- binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl, standard]
- binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl, standard]
- binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0, standard]
- binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1, standard]
+ binop_eq [of "op =", OF eq_number_of_eq numeral_0_eq_0 refl]
+ binop_eq [of "op =", OF eq_number_of_eq numeral_1_eq_1 refl]
+ binop_eq [of "op =", OF eq_number_of_eq refl numeral_0_eq_0]
+ binop_eq [of "op =", OF eq_number_of_eq refl numeral_1_eq_1]
text{*Allow 0 or 1 on either side with a binary numeral on the other*}
lemmas less_special =
- binop_eq [of "op <", OF less_number_of numeral_0_eq_0 refl, standard]
- binop_eq [of "op <", OF less_number_of numeral_1_eq_1 refl, standard]
- binop_eq [of "op <", OF less_number_of refl numeral_0_eq_0, standard]
- binop_eq [of "op <", OF less_number_of refl numeral_1_eq_1, standard]
+ binop_eq [of "op <", OF less_number_of numeral_0_eq_0 refl]
+ binop_eq [of "op <", OF less_number_of numeral_1_eq_1 refl]
+ binop_eq [of "op <", OF less_number_of refl numeral_0_eq_0]
+ binop_eq [of "op <", OF less_number_of refl numeral_1_eq_1]
text{*Allow 0 or 1 on either side with a binary numeral on the other*}
lemmas le_special =
- binop_eq [of "op \<le>", OF le_number_of numeral_0_eq_0 refl, standard]
- binop_eq [of "op \<le>", OF le_number_of numeral_1_eq_1 refl, standard]
- binop_eq [of "op \<le>", OF le_number_of refl numeral_0_eq_0, standard]
- binop_eq [of "op \<le>", OF le_number_of refl numeral_1_eq_1, standard]
+ binop_eq [of "op \<le>", OF le_number_of numeral_0_eq_0 refl]
+ binop_eq [of "op \<le>", OF le_number_of numeral_1_eq_1 refl]
+ binop_eq [of "op \<le>", OF le_number_of refl numeral_0_eq_0]
+ binop_eq [of "op \<le>", OF le_number_of refl numeral_1_eq_1]
lemmas arith_special[simp] =
add_special diff_special eq_special less_special le_special
@@ -1609,7 +1606,7 @@
text{*This simplifies expressions of the form @{term "int n = z"} where
z is an integer literal.*}
-lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v", standard]
+lemmas int_eq_iff_number_of [simp] = int_eq_iff [of _ "number_of v"] for v
lemma split_nat [arith_split]:
"P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
@@ -1895,60 +1892,33 @@
text{*These distributive laws move literals inside sums and differences.*}
-lemmas left_distrib_number_of [simp] =
- left_distrib [of _ _ "number_of v", standard]
-
-lemmas right_distrib_number_of [simp] =
- right_distrib [of "number_of v", standard]
-
-lemmas left_diff_distrib_number_of [simp] =
- left_diff_distrib [of _ _ "number_of v", standard]
-
-lemmas right_diff_distrib_number_of [simp] =
- right_diff_distrib [of "number_of v", standard]
+lemmas left_distrib_number_of [simp] = left_distrib [of _ _ "number_of v"] for v
+lemmas right_distrib_number_of [simp] = right_distrib [of "number_of v"] for v
+lemmas left_diff_distrib_number_of [simp] = left_diff_distrib [of _ _ "number_of v"] for v
+lemmas right_diff_distrib_number_of [simp] = right_diff_distrib [of "number_of v"] for v
text{*These are actually for fields, like real: but where else to put them?*}
-lemmas zero_less_divide_iff_number_of [simp, no_atp] =
- zero_less_divide_iff [of "number_of w", standard]
-
-lemmas divide_less_0_iff_number_of [simp, no_atp] =
- divide_less_0_iff [of "number_of w", standard]
-
-lemmas zero_le_divide_iff_number_of [simp, no_atp] =
- zero_le_divide_iff [of "number_of w", standard]
-
-lemmas divide_le_0_iff_number_of [simp, no_atp] =
- divide_le_0_iff [of "number_of w", standard]
+lemmas zero_less_divide_iff_number_of [simp, no_atp] = zero_less_divide_iff [of "number_of w"] for w
+lemmas divide_less_0_iff_number_of [simp, no_atp] = divide_less_0_iff [of "number_of w"] for w
+lemmas zero_le_divide_iff_number_of [simp, no_atp] = zero_le_divide_iff [of "number_of w"] for w
+lemmas divide_le_0_iff_number_of [simp, no_atp] = divide_le_0_iff [of "number_of w"] for w
text {*Replaces @{text "inverse #nn"} by @{text "1/#nn"}. It looks
strange, but then other simprocs simplify the quotient.*}
-lemmas inverse_eq_divide_number_of [simp] =
- inverse_eq_divide [of "number_of w", standard]
+lemmas inverse_eq_divide_number_of [simp] = inverse_eq_divide [of "number_of w"] for w
text {*These laws simplify inequalities, moving unary minus from a term
into the literal.*}
-lemmas less_minus_iff_number_of [simp, no_atp] =
- less_minus_iff [of "number_of v", standard]
-
-lemmas le_minus_iff_number_of [simp, no_atp] =
- le_minus_iff [of "number_of v", standard]
-
-lemmas equation_minus_iff_number_of [simp, no_atp] =
- equation_minus_iff [of "number_of v", standard]
-
-lemmas minus_less_iff_number_of [simp, no_atp] =
- minus_less_iff [of _ "number_of v", standard]
-
-lemmas minus_le_iff_number_of [simp, no_atp] =
- minus_le_iff [of _ "number_of v", standard]
-
-lemmas minus_equation_iff_number_of [simp, no_atp] =
- minus_equation_iff [of _ "number_of v", standard]
-
+lemmas less_minus_iff_number_of [simp, no_atp] = less_minus_iff [of "number_of v"] for v
+lemmas le_minus_iff_number_of [simp, no_atp] = le_minus_iff [of "number_of v"] for v
+lemmas equation_minus_iff_number_of [simp, no_atp] = equation_minus_iff [of "number_of v"] for v
+lemmas minus_less_iff_number_of [simp, no_atp] = minus_less_iff [of _ "number_of v"] for v
+lemmas minus_le_iff_number_of [simp, no_atp] = minus_le_iff [of _ "number_of v"] for v
+lemmas minus_equation_iff_number_of [simp, no_atp] = minus_equation_iff [of _ "number_of v"] for v
text{*To Simplify Inequalities Where One Side is the Constant 1*}
@@ -1985,39 +1955,32 @@
text {*Cancellation of constant factors in comparisons (@{text "<"} and @{text "\<le>"}) *}
-lemmas mult_less_cancel_left_number_of [simp, no_atp] =
- mult_less_cancel_left [of "number_of v", standard]
-
-lemmas mult_less_cancel_right_number_of [simp, no_atp] =
- mult_less_cancel_right [of _ "number_of v", standard]
-
-lemmas mult_le_cancel_left_number_of [simp, no_atp] =
- mult_le_cancel_left [of "number_of v", standard]
-
-lemmas mult_le_cancel_right_number_of [simp, no_atp] =
- mult_le_cancel_right [of _ "number_of v", standard]
+lemmas mult_less_cancel_left_number_of [simp, no_atp] = mult_less_cancel_left [of "number_of v"] for v
+lemmas mult_less_cancel_right_number_of [simp, no_atp] = mult_less_cancel_right [of _ "number_of v"] for v
+lemmas mult_le_cancel_left_number_of [simp, no_atp] = mult_le_cancel_left [of "number_of v"] for v
+lemmas mult_le_cancel_right_number_of [simp, no_atp] = mult_le_cancel_right [of _ "number_of v"] for v
text {*Multiplying out constant divisors in comparisons (@{text "<"}, @{text "\<le>"} and @{text "="}) *}
-lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w", standard]
-lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w", standard]
-lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w", standard]
-lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w", standard]
-lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w", standard]
-lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w", standard]
+lemmas le_divide_eq_number_of1 [simp] = le_divide_eq [of _ _ "number_of w"] for w
+lemmas divide_le_eq_number_of1 [simp] = divide_le_eq [of _ "number_of w"] for w
+lemmas less_divide_eq_number_of1 [simp] = less_divide_eq [of _ _ "number_of w"] for w
+lemmas divide_less_eq_number_of1 [simp] = divide_less_eq [of _ "number_of w"] for w
+lemmas eq_divide_eq_number_of1 [simp] = eq_divide_eq [of _ _ "number_of w"] for w
+lemmas divide_eq_eq_number_of1 [simp] = divide_eq_eq [of _ "number_of w"] for w
subsubsection{*Optional Simplification Rules Involving Constants*}
text{*Simplify quotients that are compared with a literal constant.*}
-lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w", standard]
-lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w", standard]
-lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w", standard]
-lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w", standard]
-lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w", standard]
-lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w", standard]
+lemmas le_divide_eq_number_of = le_divide_eq [of "number_of w"] for w
+lemmas divide_le_eq_number_of = divide_le_eq [of _ _ "number_of w"] for w
+lemmas less_divide_eq_number_of = less_divide_eq [of "number_of w"] for w
+lemmas divide_less_eq_number_of = divide_less_eq [of _ _ "number_of w"] for w
+lemmas eq_divide_eq_number_of = eq_divide_eq [of "number_of w"] for w
+lemmas divide_eq_eq_number_of = divide_eq_eq [of _ _ "number_of w"] for w
text{*Not good as automatic simprules because they cause case splits.*}
@@ -2040,7 +2003,7 @@
"(0 < r/2) = (0 < (r::'a::{linordered_field_inverse_zero,number_ring}))"
by auto
-lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2, standard]
+lemmas half_gt_zero [simp] = half_gt_zero_iff [THEN iffD2]
lemma divide_Numeral1:
"(x::'a::{field, number_ring}) / Numeral1 = x"
@@ -2359,16 +2322,16 @@
lemmas zadd_int = of_nat_add [where 'a=int, symmetric]
lemmas int_mult = of_nat_mult [where 'a=int]
lemmas zmult_int = of_nat_mult [where 'a=int, symmetric]
-lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n", standard]
+lemmas int_eq_0_conv = of_nat_eq_0_iff [where 'a=int and m="n"] for n
lemmas zless_int = of_nat_less_iff [where 'a=int]
-lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k", standard]
+lemmas int_less_0_conv = of_nat_less_0_iff [where 'a=int and m="k"] for k
lemmas zero_less_int_conv = of_nat_0_less_iff [where 'a=int]
lemmas zero_zle_int = of_nat_0_le_iff [where 'a=int]
-lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n", standard]
+lemmas int_le_0_conv = of_nat_le_0_iff [where 'a=int and m="n"] for n
lemmas int_0 = of_nat_0 [where 'a=int]
lemmas int_1 = of_nat_1 [where 'a=int]
lemmas int_Suc = of_nat_Suc [where 'a=int]
-lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m", standard]
+lemmas abs_int_eq = abs_of_nat [where 'a=int and n="m"] for m
lemmas of_int_int_eq = of_int_of_nat_eq [where 'a=int]
lemmas zdiff_int = of_nat_diff [where 'a=int, symmetric]
--- a/src/HOL/List.thy Sun Nov 20 21:07:06 2011 +0100
+++ b/src/HOL/List.thy Sun Nov 20 21:07:10 2011 +0100
@@ -2564,7 +2564,7 @@
-- {* simp does not terminate! *}
by (induct j) auto
-lemmas upt_rec_number_of[simp] = upt_rec[of "number_of m" "number_of n", standard]
+lemmas upt_rec_number_of[simp] = upt_rec[of "number_of m" "number_of n"] for m n
lemma upt_conv_Nil [simp]: "j <= i ==> [i..<j] = []"
by (subst upt_rec) simp
@@ -2679,9 +2679,9 @@
lemma nth_Cons': "(x # xs)!n = (if n = 0 then x else xs!(n - 1))"
by (cases n) simp_all
-lemmas take_Cons_number_of = take_Cons'[of "number_of v",standard]
-lemmas drop_Cons_number_of = drop_Cons'[of "number_of v",standard]
-lemmas nth_Cons_number_of = nth_Cons'[of _ _ "number_of v",standard]
+lemmas take_Cons_number_of = take_Cons'[of "number_of v"] for v
+lemmas drop_Cons_number_of = drop_Cons'[of "number_of v"] for v
+lemmas nth_Cons_number_of = nth_Cons'[of _ _ "number_of v"] for v
declare take_Cons_number_of [simp]
drop_Cons_number_of [simp]
@@ -2700,8 +2700,7 @@
declare upto.simps[code, simp del]
-lemmas upto_rec_number_of[simp] =
- upto.simps[of "number_of m" "number_of n", standard]
+lemmas upto_rec_number_of[simp] = upto.simps[of "number_of m" "number_of n"] for m n
lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
by(simp add: upto.simps)
--- a/src/HOL/Nat_Numeral.thy Sun Nov 20 21:07:06 2011 +0100
+++ b/src/HOL/Nat_Numeral.thy Sun Nov 20 21:07:10 2011 +0100
@@ -510,7 +510,7 @@
text{*Squares of literal numerals will be evaluated.*}
lemmas power2_eq_square_number_of [simp] =
- power2_eq_square [of "number_of w", standard]
+ power2_eq_square [of "number_of w"] for w
text{*Simprules for comparisons where common factors can be cancelled.*}
@@ -529,7 +529,7 @@
(*Expresses a natural number constant as the Suc of another one.
NOT suitable for rewriting because n recurs in the condition.*)
-lemmas expand_Suc = Suc_pred' [of "number_of v", standard]
+lemmas expand_Suc = Suc_pred' [of "number_of v"] for v
subsubsection{*Arith *}
@@ -684,7 +684,7 @@
split add: split_if cong: imp_cong)
-lemmas power_nat_number_of_number_of = power_nat_number_of [of _ "number_of w", standard]
+lemmas power_nat_number_of_number_of = power_nat_number_of [of _ "number_of w"] for w
declare power_nat_number_of_number_of [simp]
@@ -711,10 +711,10 @@
lemmas zpower_number_of_odd = power_number_of_odd [where 'a=int]
lemmas power_number_of_even_number_of [simp] =
- power_number_of_even [of "number_of v", standard]
+ power_number_of_even [of "number_of v"] for v
lemmas power_number_of_odd_number_of [simp] =
- power_number_of_odd [of "number_of v", standard]
+ power_number_of_odd [of "number_of v"] for v
lemma nat_number_of_Pls: "Numeral0 = (0::nat)"
by (simp add: nat_number_of_def)
--- a/src/HOL/Numeral_Simprocs.thy Sun Nov 20 21:07:06 2011 +0100
+++ b/src/HOL/Numeral_Simprocs.thy Sun Nov 20 21:07:10 2011 +0100
@@ -14,8 +14,8 @@
("Tools/nat_numeral_simprocs.ML")
begin
-declare split_div [of _ _ "number_of k", standard, arith_split]
-declare split_mod [of _ _ "number_of k", standard, arith_split]
+declare split_div [of _ _ "number_of k", arith_split] for k
+declare split_mod [of _ _ "number_of k", arith_split] for k
text {* For @{text combine_numerals} *}
--- a/src/HOL/Parity.thy Sun Nov 20 21:07:06 2011 +0100
+++ b/src/HOL/Parity.thy Sun Nov 20 21:07:10 2011 +0100
@@ -45,9 +45,9 @@
lemma odd_1_nat [simp]: "odd (1::nat)" by presburger
-declare even_def[of "number_of v", standard, simp]
+declare even_def[of "number_of v", simp] for v
-declare even_nat_def[of "number_of v", standard, simp]
+declare even_nat_def[of "number_of v", simp] for v
subsection {* Even and odd are mutually exclusive *}
@@ -347,27 +347,27 @@
text {* Simplify, when the exponent is a numeral *}
-lemmas power_0_left_number_of = power_0_left [of "number_of w", standard]
+lemmas power_0_left_number_of = power_0_left [of "number_of w"] for w
declare power_0_left_number_of [simp]
lemmas zero_le_power_eq_number_of [simp] =
- zero_le_power_eq [of _ "number_of w", standard]
+ zero_le_power_eq [of _ "number_of w"] for w
lemmas zero_less_power_eq_number_of [simp] =
- zero_less_power_eq [of _ "number_of w", standard]
+ zero_less_power_eq [of _ "number_of w"] for w
lemmas power_le_zero_eq_number_of [simp] =
- power_le_zero_eq [of _ "number_of w", standard]
+ power_le_zero_eq [of _ "number_of w"] for w
lemmas power_less_zero_eq_number_of [simp] =
- power_less_zero_eq [of _ "number_of w", standard]
+ power_less_zero_eq [of _ "number_of w"] for w
lemmas zero_less_power_nat_eq_number_of [simp] =
- zero_less_power_nat_eq [of _ "number_of w", standard]
+ zero_less_power_nat_eq [of _ "number_of w"] for w
-lemmas power_eq_0_iff_number_of [simp] = power_eq_0_iff [of _ "number_of w", standard]
+lemmas power_eq_0_iff_number_of [simp] = power_eq_0_iff [of _ "number_of w"] for w
-lemmas power_even_abs_number_of [simp] = power_even_abs [of "number_of w" _, standard]
+lemmas power_even_abs_number_of [simp] = power_even_abs [of "number_of w" _] for w
subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *}
--- a/src/HOL/Product_Type.thy Sun Nov 20 21:07:06 2011 +0100
+++ b/src/HOL/Product_Type.thy Sun Nov 20 21:07:10 2011 +0100
@@ -625,7 +625,7 @@
Setup of internal @{text split_rule}.
*}
-lemmas prod_caseI = prod.cases [THEN iffD2, standard]
+lemmas prod_caseI = prod.cases [THEN iffD2]
lemma prod_caseI2: "!!p. [| !!a b. p = (a, b) ==> c a b |] ==> prod_case c p"
by (fact splitI2)
--- a/src/HOL/Set.thy Sun Nov 20 21:07:06 2011 +0100
+++ b/src/HOL/Set.thy Sun Nov 20 21:07:10 2011 +0100
@@ -1107,7 +1107,7 @@
lemma insert_not_empty [simp]: "insert a A \<noteq> {}"
by blast
-lemmas empty_not_insert = insert_not_empty [symmetric, standard]
+lemmas empty_not_insert = insert_not_empty [symmetric]
declare empty_not_insert [simp]
lemma insert_absorb: "a \<in> A ==> insert a A = A"
--- a/src/HOL/Transitive_Closure.thy Sun Nov 20 21:07:06 2011 +0100
+++ b/src/HOL/Transitive_Closure.thy Sun Nov 20 21:07:10 2011 +0100
@@ -139,7 +139,7 @@
qed
qed
-lemmas rtrancl_trans = trans_rtrancl [THEN transD, standard]
+lemmas rtrancl_trans = trans_rtrancl [THEN transD]
lemma rtranclp_trans:
assumes xy: "r^** x y"
@@ -429,7 +429,7 @@
qed
qed
-lemmas trancl_trans = trans_trancl [THEN transD, standard]
+lemmas trancl_trans = trans_trancl [THEN transD]
lemma tranclp_trans:
assumes xy: "r^++ x y"