--- a/src/HOL/Auth/Event.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Auth/Event.thy Sun Nov 20 21:05:23 2011 +0100
@@ -93,7 +93,7 @@
(*Simplifying
parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs).
This version won't loop with the simplifier.*)
-lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
+lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs"] for A evs
lemma knows_Spy_Says [simp]:
"knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
@@ -138,10 +138,10 @@
text{*Elimination rules: derive contradictions from old Says events containing
items known to be fresh*}
lemmas Says_imp_parts_knows_Spy =
- Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard]
+ Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl]
lemmas knows_Spy_partsEs =
- Says_imp_parts_knows_Spy parts.Body [THEN revcut_rl, standard]
+ Says_imp_parts_knows_Spy parts.Body [THEN revcut_rl]
lemmas Says_imp_analz_Spy = Says_imp_knows_Spy [THEN analz.Inj]
@@ -278,7 +278,7 @@
intro: analz_subset_parts [THEN subsetD] parts_mono [THEN [2] rev_subsetD])
-lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)", standard]
+lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)"] for Y evs
ML
{*
@@ -294,7 +294,7 @@
subsubsection{*Useful for case analysis on whether a hash is a spoof or not*}
-lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))", standard]
+lemmas syan_impI = impI [where P = "Y \<notin> synth (analz (knows Spy evs))"] for Y evs
ML
{*
--- a/src/HOL/Auth/Message.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Auth/Message.thy Sun Nov 20 21:05:23 2011 +0100
@@ -166,7 +166,7 @@
lemma parts_increasing: "H \<subseteq> parts(H)"
by blast
-lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
+lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD]
lemma parts_empty [simp]: "parts{} = {}"
apply safe
@@ -358,9 +358,9 @@
apply (erule analz.induct, blast+)
done
-lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
+lemmas analz_into_parts = analz_subset_parts [THEN subsetD]
-lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
+lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]
lemma parts_analz [simp]: "parts (analz H) = parts H"
@@ -371,7 +371,7 @@
apply (erule analz.induct, auto)
done
-lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
+lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD]
subsubsection{*General equational properties *}
@@ -790,21 +790,23 @@
text{*Rewrites to push in Key and Crypt messages, so that other messages can
be pulled out using the @{text analz_insert} rules*}
-lemmas pushKeys [standard] =
+lemmas pushKeys =
insert_commute [of "Key K" "Agent C"]
insert_commute [of "Key K" "Nonce N"]
insert_commute [of "Key K" "Number N"]
insert_commute [of "Key K" "Hash X"]
insert_commute [of "Key K" "MPair X Y"]
insert_commute [of "Key K" "Crypt X K'"]
+ for K C N X Y K'
-lemmas pushCrypts [standard] =
+lemmas pushCrypts =
insert_commute [of "Crypt X K" "Agent C"]
insert_commute [of "Crypt X K" "Agent C"]
insert_commute [of "Crypt X K" "Nonce N"]
insert_commute [of "Crypt X K" "Number N"]
insert_commute [of "Crypt X K" "Hash X'"]
insert_commute [of "Crypt X K" "MPair X' Y"]
+ for X K C N X' Y
text{*Cannot be added with @{text "[simp]"} -- messages should not always be
re-ordered. *}
--- a/src/HOL/Auth/OtwayRees.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Auth/OtwayRees.thy Sun Nov 20 21:05:23 2011 +0100
@@ -121,7 +121,7 @@
We can replace them by rewriting with parts_insert2 and proving using
dest: parts_cut, but the proofs become more difficult.*)
lemmas OR2_parts_knows_Spy =
- OR2_analz_knows_Spy [THEN analz_into_parts, standard]
+ OR2_analz_knows_Spy [THEN analz_into_parts]
(*There could be OR4_parts_knows_Spy and Oops_parts_knows_Spy, but for
some reason proofs work without them!*)
--- a/src/HOL/Auth/OtwayReesBella.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Auth/OtwayReesBella.thy Sun Nov 20 21:05:23 2011 +0100
@@ -122,7 +122,7 @@
by blast
lemmas OR2_parts_knows_Spy =
- OR2_analz_knows_Spy [THEN analz_into_parts, standard]
+ OR2_analz_knows_Spy [THEN analz_into_parts]
ML
{*
--- a/src/HOL/Auth/OtwayRees_Bad.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Auth/OtwayRees_Bad.thy Sun Nov 20 21:05:23 2011 +0100
@@ -128,7 +128,7 @@
text{*Forwarding lemma: see comments in OtwayRees.thy*}
lemmas OR2_parts_knows_Spy =
- OR2_analz_knows_Spy [THEN analz_into_parts, standard]
+ OR2_analz_knows_Spy [THEN analz_into_parts]
text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that
--- a/src/HOL/Auth/Smartcard/EventSC.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Auth/Smartcard/EventSC.thy Sun Nov 20 21:05:23 2011 +0100
@@ -118,7 +118,7 @@
(*Simplifying
parts(insert X (knows Spy evs)) = parts{X} \<union> parts(knows Spy evs).
This version won't loop with the simplifier.*)
-lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
+lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs"] for A evs
lemma knows_Spy_Says [simp]:
"knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
@@ -237,8 +237,8 @@
text{*Elimination rules: derive contradictions from old Says events containing
items known to be fresh*}
lemmas knows_Spy_partsEs =
- Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard]
- parts.Body [THEN revcut_rl, standard]
+ Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl]
+ parts.Body [THEN revcut_rl]
--- a/src/HOL/Auth/Yahalom.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Auth/Yahalom.thy Sun Nov 20 21:05:23 2011 +0100
@@ -121,7 +121,7 @@
by blast
lemmas YM4_parts_knows_Spy =
- YM4_analz_knows_Spy [THEN analz_into_parts, standard]
+ YM4_analz_knows_Spy [THEN analz_into_parts]
text{*For Oops*}
lemma YM4_Key_parts_knows_Spy:
--- a/src/HOL/Auth/Yahalom2.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Auth/Yahalom2.thy Sun Nov 20 21:05:23 2011 +0100
@@ -116,7 +116,7 @@
by blast
lemmas YM4_parts_knows_Spy =
- YM4_analz_knows_Spy [THEN analz_into_parts, standard]
+ YM4_analz_knows_Spy [THEN analz_into_parts]
(** Theorems of the form X \<notin> parts (knows Spy evs) imply that NOBODY
--- a/src/HOL/Auth/Yahalom_Bad.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Auth/Yahalom_Bad.thy Sun Nov 20 21:05:23 2011 +0100
@@ -103,7 +103,7 @@
by blast
lemmas YM4_parts_knows_Spy =
- YM4_analz_knows_Spy [THEN analz_into_parts, standard]
+ YM4_analz_knows_Spy [THEN analz_into_parts]
text{*Theorems of the form @{term "X \<notin> parts (knows Spy evs)"} imply
--- a/src/HOL/Bali/AxCompl.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Bali/AxCompl.thy Sun Nov 20 21:05:23 2011 +0100
@@ -30,7 +30,7 @@
done
lemmas finite_nyinitcls [simp] =
- finite_is_class [THEN nyinitcls_subset_class [THEN finite_subset], standard]
+ finite_is_class [THEN nyinitcls_subset_class [THEN finite_subset]]
lemma card_nyinitcls_bound: "card (nyinitcls G s) \<le> card {C. is_class G C}"
apply (rule nyinitcls_subset_class [THEN finite_is_class [THEN card_mono]])
--- a/src/HOL/Bali/AxSem.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Bali/AxSem.thy Sun Nov 20 21:05:23 2011 +0100
@@ -1016,7 +1016,7 @@
apply (rule ax_derivs.Skip)
apply fast
done
-lemmas ax_SkipI = ax_Skip [THEN conseq1, standard]
+lemmas ax_SkipI = ax_Skip [THEN conseq1]
section "derived rules for methd call"
--- a/src/HOL/Bali/Decl.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Bali/Decl.thy Sun Nov 20 21:05:23 2011 +0100
@@ -613,8 +613,8 @@
apply auto
done
-lemmas subint1_acyclic = subint1_irrefl_lemma2 [THEN acyclicI, standard]
-lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI, standard]
+lemmas subint1_acyclic = subint1_irrefl_lemma2 [THEN acyclicI]
+lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI]
lemma wf_subint1: "ws_prog G \<Longrightarrow> wf ((subint1 G)\<inverse>)"
--- a/src/HOL/Bali/Table.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Bali/Table.thy Sun Nov 20 21:05:23 2011 +0100
@@ -222,7 +222,7 @@
apply auto
done
-lemmas table_of_map2_SomeI = inj_Pair_const2 [THEN map_of_mapk_SomeI, standard]
+lemmas table_of_map2_SomeI = inj_Pair_const2 [THEN map_of_mapk_SomeI]
lemma table_of_map_SomeI [rule_format (no_asm)]: "table_of t k = Some x \<longrightarrow>
table_of (map (\<lambda>(k,x). (k, f x)) t) k = Some (f x)"
--- a/src/HOL/Bali/TypeRel.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Bali/TypeRel.thy Sun Nov 20 21:05:23 2011 +0100
@@ -60,7 +60,7 @@
(* direct subinterface in Decl.thy, cf. 9.1.3 *)
(* direct subclass in Decl.thy, cf. 8.1.3 *)
-lemmas subcls_direct = subcls1I [THEN r_into_rtrancl, standard]
+lemmas subcls_direct = subcls1I [THEN r_into_rtrancl]
lemma subcls_direct1:
"\<lbrakk>class G C = Some c; C \<noteq> Object;D=super c\<rbrakk> \<Longrightarrow> G\<turnstile>C\<preceq>\<^sub>C D"
@@ -554,9 +554,9 @@
done
lemmas subint_antisym =
- subint1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard]
+ subint1_acyclic [THEN acyclic_impl_antisym_rtrancl]
lemmas subcls_antisym =
- subcls1_acyclic [THEN acyclic_impl_antisym_rtrancl, standard]
+ subcls1_acyclic [THEN acyclic_impl_antisym_rtrancl]
lemma widen_antisym: "\<lbrakk>G\<turnstile>S\<preceq>T; G\<turnstile>T\<preceq>S; ws_prog G\<rbrakk> \<Longrightarrow> S=T"
by (fast elim: widen_antisym_lemma subint_antisym [THEN antisymD]
--- a/src/HOL/Bali/WellForm.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Bali/WellForm.thy Sun Nov 20 21:05:23 2011 +0100
@@ -739,7 +739,7 @@
proof -
assume asm: "wf_prog G" "is_iface G I" "im \<in> imethds G I sig"
- note iface_rec_induct' = iface_rec.induct[of "(%x y z. P x y)", standard]
+ note iface_rec_induct' = iface_rec.induct[of "(%x y z. P x y)", standard] (* FIXME !? *)
have "wf_prog G \<longrightarrow>
(\<forall> i im. iface G I = Some i \<longrightarrow> im \<in> imethds G I sig
\<longrightarrow> \<not>is_static im \<and> accmodi im = Public)" (is "?P G I")
@@ -1355,7 +1355,7 @@
qed
qed
-lemmas class_rec_induct' = class_rec.induct[of "%x y z w. P x y", standard]
+lemmas class_rec_induct' = class_rec.induct [of "%x y z w. P x y"] for P
lemma declclass_widen[rule_format]:
"wf_prog G
--- a/src/HOL/Decision_Procs/Polynomial_List.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Decision_Procs/Polynomial_List.thy Sun Nov 20 21:05:23 2011 +0100
@@ -281,7 +281,7 @@
apply (drule_tac x = m in spec)
apply (auto simp add:field_simps)
done
-lemmas poly_roots_index_lemma1 = conjI [THEN poly_roots_index_lemma0, standard]
+lemmas poly_roots_index_lemma1 = conjI [THEN poly_roots_index_lemma0]
lemma poly_roots_index_length0: "poly p (x::'a::idom) \<noteq> poly [] x ==>
\<exists>i. \<forall>x. (poly p x = 0) --> (\<exists>n. n \<le> length p & x = i n)"
@@ -322,7 +322,7 @@
apply (clarsimp simp add: field_simps)
done
-lemmas poly_roots_index_lemma2 = conjI [THEN poly_roots_index_lemma, standard]
+lemmas poly_roots_index_lemma2 = conjI [THEN poly_roots_index_lemma]
lemma poly_roots_index_length: "poly p (x::'a::idom) \<noteq> poly [] x ==>
\<exists>i. \<forall>x. (poly p x = 0) --> x \<in> set i"
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy Sun Nov 20 21:05:23 2011 +0100
@@ -24,7 +24,7 @@
elements of the chain.
*}
lemmas [dest?] = chainD
-lemmas chainE2 [elim?] = chainD2 [elim_format, standard]
+lemmas chainE2 [elim?] = chainD2 [elim_format]
lemma some_H'h't:
assumes M: "M = norm_pres_extensions E p F f"
--- a/src/HOL/IMP/Comp_Rev.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/IMP/Comp_Rev.thy Sun Nov 20 21:05:23 2011 +0100
@@ -363,7 +363,7 @@
qed
lemmas exec_n_drop_Cons =
- exec_n_drop_left [where P="[instr]", simplified, standard]
+ exec_n_drop_left [where P="[instr]", simplified] for instr
definition
"closed P \<longleftrightarrow> exits P \<subseteq> {isize P}"
--- a/src/HOL/IMPP/Hoare.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/IMPP/Hoare.thy Sun Nov 20 21:05:23 2011 +0100
@@ -460,7 +460,7 @@
done
(* requires Body+empty+insert / BodyN, com_det *)
-lemmas hoare_complete = MGF' [THEN MGF_complete, standard]
+lemmas hoare_complete = MGF' [THEN MGF_complete]
subsection "unused derived rules"
--- a/src/HOL/Induct/PropLog.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Induct/PropLog.thy Sun Nov 20 21:05:23 2011 +0100
@@ -111,7 +111,7 @@
lemmas thms_falseE = weaken_right [THEN thms.DN [THEN thms.MP]]
-lemmas thms_notE = thms.MP [THEN thms_falseE, standard]
+lemmas thms_notE = thms.MP [THEN thms_falseE]
subsubsection {* Soundness of the rules wrt truth-table semantics *}
--- a/src/HOL/Induct/SList.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Induct/SList.thy Sun Nov 20 21:05:23 2011 +0100
@@ -191,7 +191,7 @@
by (simp add: NIL_def CONS_def)
lemmas NIL_not_CONS [iff] = CONS_not_NIL [THEN not_sym]
-lemmas CONS_neq_NIL = CONS_not_NIL [THEN notE, standard]
+lemmas CONS_neq_NIL = CONS_not_NIL [THEN notE]
lemmas NIL_neq_CONS = sym [THEN CONS_neq_NIL]
lemma Cons_not_Nil [iff]: "x # xs ~= Nil"
@@ -200,8 +200,9 @@
apply (simp_all add: list.intros rangeI Rep_List [unfolded List_def])
done
-lemmas Nil_not_Cons [iff] = Cons_not_Nil [THEN not_sym, standard]
-lemmas Cons_neq_Nil = Cons_not_Nil [THEN notE, standard]
+lemmas Nil_not_Cons = Cons_not_Nil [THEN not_sym]
+declare Nil_not_Cons [iff]
+lemmas Cons_neq_Nil = Cons_not_Nil [THEN notE]
lemmas Nil_neq_Cons = sym [THEN Cons_neq_Nil]
(** Injectiveness of CONS and Cons **)
@@ -220,7 +221,7 @@
apply (auto simp add: Rep_List_inject)
done
-lemmas Cons_inject2 = Cons_Cons_eq [THEN iffD1, THEN conjE, standard]
+lemmas Cons_inject2 = Cons_Cons_eq [THEN iffD1, THEN conjE]
lemma CONS_D: "CONS M N: list(A) ==> M: A & N: list(A)"
by (induct L == "CONS M N" set: list) auto
@@ -264,8 +265,7 @@
by (simp add: List_rec_def)
lemmas List_rec_unfold =
- def_wfrec [OF List_rec_unfold_lemma wf_pred_sexp [THEN wf_trancl],
- standard]
+ def_wfrec [OF List_rec_unfold_lemma wf_pred_sexp [THEN wf_trancl]]
(** pred_sexp lemmas **)
--- a/src/HOL/Library/AList.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Library/AList.thy Sun Nov 20 21:05:23 2011 +0100
@@ -467,7 +467,7 @@
(map_of n k = Some x \<or> map_of n k = None \<and> map_of m k = Some x)"
by (simp add: merge_conv' map_add_Some_iff)
-lemmas merge_SomeD [dest!] = merge_Some_iff [THEN iffD1, standard]
+lemmas merge_SomeD [dest!] = merge_Some_iff [THEN iffD1]
lemma merge_find_right[simp]: "map_of n k = Some v \<Longrightarrow> map_of (merge m n) k = Some v"
by (simp add: merge_conv')
--- a/src/HOL/Library/Polynomial.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Library/Polynomial.thy Sun Nov 20 21:05:23 2011 +0100
@@ -928,11 +928,9 @@
lemma pdivmod_rel_by_0_iff: "pdivmod_rel x 0 q r \<longleftrightarrow> q = 0 \<and> r = x"
by (auto dest: pdivmod_rel_unique intro: pdivmod_rel_by_0)
-lemmas pdivmod_rel_unique_div =
- pdivmod_rel_unique [THEN conjunct1, standard]
+lemmas pdivmod_rel_unique_div = pdivmod_rel_unique [THEN conjunct1]
-lemmas pdivmod_rel_unique_mod =
- pdivmod_rel_unique [THEN conjunct2, standard]
+lemmas pdivmod_rel_unique_mod = pdivmod_rel_unique [THEN conjunct2]
instantiation poly :: (field) ring_div
begin
--- a/src/HOL/Metis_Examples/Message.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Metis_Examples/Message.thy Sun Nov 20 21:05:23 2011 +0100
@@ -164,7 +164,7 @@
lemma parts_increasing: "H \<subseteq> parts(H)"
by blast
-lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
+lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD]
lemma parts_empty [simp]: "parts{} = {}"
apply safe
@@ -353,9 +353,9 @@
apply (erule analz.induct, blast+)
done
-lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
+lemmas analz_into_parts = analz_subset_parts [THEN subsetD]
-lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
+lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]
lemma parts_analz [simp]: "parts (analz H) = parts H"
apply (rule equalityI)
@@ -369,7 +369,7 @@
apply (erule analz.induct, auto)
done
-lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
+lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD]
subsubsection{*General equational properties *}
--- a/src/HOL/MicroJava/BV/JType.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/MicroJava/BV/JType.thy Sun Nov 20 21:05:23 2011 +0100
@@ -142,7 +142,7 @@
apply (case_tac t)
apply simp
apply simp
-apply (insert rtrancl_r_diff_Id [symmetric, standard, of "subcls1 G"])
+apply (insert rtrancl_r_diff_Id [symmetric, of "subcls1 G"])
apply simp
apply (erule rtrancl.cases)
apply blast
--- a/src/HOL/MicroJava/J/Example.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/MicroJava/J/Example.thy Sun Nov 20 21:05:23 2011 +0100
@@ -202,7 +202,7 @@
apply (simp (no_asm) add: ObjectC_def BaseC_def ExtC_def NullPointerC_def ClassCastC_def OutOfMemoryC_def)
done
-lemmas subcls_direct = subcls1I [THEN r_into_rtrancl [where r="subcls1 G"], standard]
+lemmas subcls_direct = subcls1I [THEN r_into_rtrancl [where r="subcls1 G"]] for G
lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext\<preceq>C Base"
apply (rule subcls_direct)
--- a/src/HOL/Multivariate_Analysis/Derivative.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Derivative.thy Sun Nov 20 21:05:23 2011 +0100
@@ -141,22 +141,22 @@
done
lemmas scaleR_right_has_derivative =
- bounded_linear.has_derivative [OF bounded_linear_scaleR_right, standard]
+ bounded_linear.has_derivative [OF bounded_linear_scaleR_right]
lemmas scaleR_left_has_derivative =
- bounded_linear.has_derivative [OF bounded_linear_scaleR_left, standard]
+ bounded_linear.has_derivative [OF bounded_linear_scaleR_left]
lemmas inner_right_has_derivative =
- bounded_linear.has_derivative [OF bounded_linear_inner_right, standard]
+ bounded_linear.has_derivative [OF bounded_linear_inner_right]
lemmas inner_left_has_derivative =
- bounded_linear.has_derivative [OF bounded_linear_inner_left, standard]
+ bounded_linear.has_derivative [OF bounded_linear_inner_left]
lemmas mult_right_has_derivative =
- bounded_linear.has_derivative [OF bounded_linear_mult_right, standard]
+ bounded_linear.has_derivative [OF bounded_linear_mult_right]
lemmas mult_left_has_derivative =
- bounded_linear.has_derivative [OF bounded_linear_mult_left, standard]
+ bounded_linear.has_derivative [OF bounded_linear_mult_left]
lemmas euclidean_component_has_derivative =
bounded_linear.has_derivative [OF bounded_linear_euclidean_component]
--- a/src/HOL/NSA/Examples/NSPrimes.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/NSA/Examples/NSPrimes.thy Sun Nov 20 21:05:23 2011 +0100
@@ -39,7 +39,7 @@
apply (force intro!: dvd_mult)
done
-lemmas dvd_by_all2 = dvd_by_all [THEN spec, standard]
+lemmas dvd_by_all2 = dvd_by_all [THEN spec]
lemma hypnat_of_nat_le_zero_iff: "(hypnat_of_nat n <= 0) = (n = 0)"
by (transfer, simp)
@@ -50,7 +50,7 @@
lemma hdvd_by_all: "\<forall>M. \<exists>N. 0 < N & (\<forall>m. 0 < m & (m::hypnat) <= M --> m dvd N)"
by (transfer, rule dvd_by_all)
-lemmas hdvd_by_all2 = hdvd_by_all [THEN spec, standard]
+lemmas hdvd_by_all2 = hdvd_by_all [THEN spec]
(* Goldblatt: Exercise 5.11(2) - p. 57 *)
lemma hypnat_dvd_all_hypnat_of_nat:
--- a/src/HOL/NSA/HyperDef.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/NSA/HyperDef.thy Sun Nov 20 21:05:23 2011 +0100
@@ -422,7 +422,7 @@
lemma power_hypreal_of_real_number_of:
"(number_of v :: hypreal) ^ n = hypreal_of_real ((number_of v) ^ n)"
by simp
-declare power_hypreal_of_real_number_of [of _ "number_of w", standard, simp]
+declare power_hypreal_of_real_number_of [of _ "number_of w", simp] for w
(*
lemma hrealpow_HFinite:
fixes x :: "'a::{real_normed_algebra,power} star"
--- a/src/HOL/NSA/StarDef.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/NSA/StarDef.thy Sun Nov 20 21:05:23 2011 +0100
@@ -683,18 +683,18 @@
text{*As above, for numerals*}
lemmas star_of_number_less =
- star_of_less [of "number_of w", standard, simplified star_of_number_of]
+ star_of_less [of "number_of w", simplified star_of_number_of] for w
lemmas star_of_number_le =
- star_of_le [of "number_of w", standard, simplified star_of_number_of]
+ star_of_le [of "number_of w", simplified star_of_number_of] for w
lemmas star_of_number_eq =
- star_of_eq [of "number_of w", standard, simplified star_of_number_of]
+ star_of_eq [of "number_of w", simplified star_of_number_of] for w
lemmas star_of_less_number =
- star_of_less [of _ "number_of w", standard, simplified star_of_number_of]
+ star_of_less [of _ "number_of w", simplified star_of_number_of] for w
lemmas star_of_le_number =
- star_of_le [of _ "number_of w", standard, simplified star_of_number_of]
+ star_of_le [of _ "number_of w", simplified star_of_number_of] for w
lemmas star_of_eq_number =
- star_of_eq [of _ "number_of w", standard, simplified star_of_number_of]
+ star_of_eq [of _ "number_of w", simplified star_of_number_of] for w
lemmas star_of_simps [simp] =
star_of_add star_of_diff star_of_minus
--- a/src/HOL/NanoJava/AxSem.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/NanoJava/AxSem.thy Sun Nov 20 21:05:23 2011 +0100
@@ -196,6 +196,6 @@
apply (auto del: image_eqI intro: rev_image_eqI)
done
-lemmas Impl1 = AxSem.Impl [of _ _ _ "{Cm}", simplified, standard]
+lemmas Impl1 = AxSem.Impl [of _ _ _ "{Cm}", simplified] for Cm
end
--- a/src/HOL/NanoJava/TypeRel.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/NanoJava/TypeRel.thy Sun Nov 20 21:05:23 2011 +0100
@@ -86,7 +86,7 @@
apply auto
done
-lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI, standard]
+lemmas subcls1_acyclic = subcls1_irrefl_lemma2 [THEN acyclicI]
lemma wf_subcls1: "ws_prog \<Longrightarrow> wf (subcls1\<inverse>)"
by (auto intro: finite_acyclic_wf_converse finite_subcls1 subcls1_acyclic)
--- a/src/HOL/Number_Theory/Primes.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Number_Theory/Primes.thy Sun Nov 20 21:05:23 2011 +0100
@@ -206,7 +206,7 @@
"prime (p::nat) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..<p]. \<not> n dvd p)"
by (auto simp add: prime_nat_code)
-lemmas prime_nat_simp_number_of [simp] = prime_nat_simp [of "number_of m", standard]
+lemmas prime_nat_simp_number_of [simp] = prime_nat_simp [of "number_of m"] for m
lemma prime_int_code [code]:
"prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
@@ -222,7 +222,7 @@
lemma prime_int_simp: "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> set [2..p - 1]. ~ n dvd p)"
by (auto simp add: prime_int_code)
-lemmas prime_int_simp_number_of [simp] = prime_int_simp [of "number_of m", standard]
+lemmas prime_int_simp_number_of [simp] = prime_int_simp [of "number_of m"] for m
lemma two_is_prime_nat [simp]: "prime (2::nat)"
by simp
--- a/src/HOL/Old_Number_Theory/EulerFermat.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Old_Number_Theory/EulerFermat.thy Sun Nov 20 21:05:23 2011 +0100
@@ -196,10 +196,8 @@
apply (rule aux_some, simp_all)
done
-lemmas RRset2norRR_correct1 =
- RRset2norRR_correct [THEN conjunct1, standard]
-lemmas RRset2norRR_correct2 =
- RRset2norRR_correct [THEN conjunct2, standard]
+lemmas RRset2norRR_correct1 = RRset2norRR_correct [THEN conjunct1]
+lemmas RRset2norRR_correct2 = RRset2norRR_correct [THEN conjunct2]
lemma RsetR_fin: "A \<in> RsetR m ==> finite A"
by (induct set: RsetR) auto
--- a/src/HOL/Old_Number_Theory/WilsonBij.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Old_Number_Theory/WilsonBij.thy Sun Nov 20 21:05:23 2011 +0100
@@ -41,9 +41,9 @@
apply auto
done
-lemmas inv_ge = inv_correct [THEN conjunct1, standard]
-lemmas inv_less = inv_correct [THEN conjunct2, THEN conjunct1, standard]
-lemmas inv_is_inv = inv_correct [THEN conjunct2, THEN conjunct2, standard]
+lemmas inv_ge = inv_correct [THEN conjunct1]
+lemmas inv_less = inv_correct [THEN conjunct2, THEN conjunct1]
+lemmas inv_is_inv = inv_correct [THEN conjunct2, THEN conjunct2]
lemma inv_not_0:
"zprime p ==> 1 < a ==> a < p - 1 ==> inv p a \<noteq> 0"
--- a/src/HOL/Proofs/Lambda/NormalForm.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Proofs/Lambda/NormalForm.thy Sun Nov 20 21:05:23 2011 +0100
@@ -132,10 +132,10 @@
apply (drule listall_conj2)
apply (drule_tac i=i and j=j in subst_terms_NF)
apply assumption
- apply (rule_tac m=x and n=j in nat_eq_dec [THEN disjE, standard])
+ apply (rule_tac m1=x and n1=j in nat_eq_dec [THEN disjE])
apply simp
apply (erule NF.App)
- apply (rule_tac m=j and n=x in nat_le_dec [THEN disjE, standard])
+ apply (rule_tac m1=j and n1=x in nat_le_dec [THEN disjE])
apply simp
apply (iprover intro: NF.App)
apply simp
@@ -173,7 +173,7 @@
apply (drule listall_conj2)
apply (drule_tac i=i in lift_terms_NF)
apply assumption
- apply (rule_tac m=x and n=i in nat_le_dec [THEN disjE, standard])
+ apply (rule_tac m1=x and n1=i in nat_le_dec [THEN disjE])
apply simp
apply (rule NF.App)
apply assumption
--- a/src/HOL/Quotient_Examples/FSet.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy Sun Nov 20 21:05:23 2011 +0100
@@ -649,8 +649,8 @@
subsection {* union_fset *}
lemmas [simp] =
- sup_bot_left[where 'a="'a fset", standard]
- sup_bot_right[where 'a="'a fset", standard]
+ sup_bot_left[where 'a="'a fset"]
+ sup_bot_right[where 'a="'a fset"]
lemma union_insert_fset [simp]:
shows "insert_fset x S |\<union>| T = insert_fset x (S |\<union>| T)"
--- a/src/HOL/Quotient_Examples/Quotient_Int.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/Quotient_Examples/Quotient_Int.thy Sun Nov 20 21:05:23 2011 +0100
@@ -263,11 +263,12 @@
qed
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]
- minus_add_distrib[of "z1::int" "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]
+ minus_add_distrib[of z1 z2]
+ for z1 z2 w :: int
lemma int_induct_raw:
assumes a: "P (0::nat, 0)"
--- a/src/HOL/SET_Protocol/Event_SET.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/SET_Protocol/Event_SET.thy Sun Nov 20 21:05:23 2011 +0100
@@ -82,7 +82,7 @@
(** Simplifying parts (insert X (knows Spy evs))
= parts {X} Un parts (knows Spy evs) -- since general case loops*)
-lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs", standard]
+lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs"] for A evs
lemma knows_Spy_Says [simp]:
"knows Spy (Says A B X # evs) = insert X (knows Spy evs)"
@@ -126,8 +126,8 @@
(*Use with addSEs to derive contradictions from old Says events containing
items known to be fresh*)
lemmas knows_Spy_partsEs =
- Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl, standard]
- parts.Body [THEN revcut_rl, standard]
+ Says_imp_knows_Spy [THEN parts.Inj, THEN revcut_rl]
+ parts.Body [THEN revcut_rl]
subsection{*The Function @{term used}*}
@@ -177,7 +177,7 @@
knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD]
knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD]
-lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)", standard]
+lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)"] for Y evs
ML
{*
--- a/src/HOL/SET_Protocol/Message_SET.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy Sun Nov 20 21:05:23 2011 +0100
@@ -210,7 +210,7 @@
lemma parts_increasing: "H \<subseteq> parts(H)"
by blast
-lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD, standard]
+lemmas parts_insertI = subset_insertI [THEN parts_mono, THEN subsetD]
lemma parts_empty [simp]: "parts{} = {}"
apply safe
@@ -424,9 +424,9 @@
apply (erule analz.induct, blast+)
done
-lemmas analz_into_parts = analz_subset_parts [THEN subsetD, standard]
+lemmas analz_into_parts = analz_subset_parts [THEN subsetD]
-lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD, standard]
+lemmas not_parts_not_analz = analz_subset_parts [THEN contra_subsetD]
lemma parts_analz [simp]: "parts (analz H) = parts H"
@@ -440,7 +440,7 @@
apply (erule analz.induct, auto)
done
-lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD, standard]
+lemmas analz_insertI = subset_insertI [THEN analz_mono, THEN [2] rev_subsetD]
subsubsection{*General equational properties*}
@@ -811,7 +811,7 @@
text{*Rewrites to push in Key and Crypt messages, so that other messages can
be pulled out using the @{text analz_insert} rules*}
-lemmas pushKeys [standard] =
+lemmas pushKeys =
insert_commute [of "Key K" "Agent C"]
insert_commute [of "Key K" "Nonce N"]
insert_commute [of "Key K" "Number N"]
@@ -819,14 +819,16 @@
insert_commute [of "Key K" "Hash X"]
insert_commute [of "Key K" "MPair X Y"]
insert_commute [of "Key K" "Crypt X K'"]
+ for K C N PAN X Y K'
-lemmas pushCrypts [standard] =
+lemmas pushCrypts =
insert_commute [of "Crypt X K" "Agent C"]
insert_commute [of "Crypt X K" "Nonce N"]
insert_commute [of "Crypt X K" "Number N"]
insert_commute [of "Crypt X K" "Pan PAN"]
insert_commute [of "Crypt X K" "Hash X'"]
insert_commute [of "Crypt X K" "MPair X' Y"]
+ for X K C N PAN X' Y
text{*Cannot be added with @{text "[simp]"} -- messages should not always be
re-ordered.*}
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Sun Nov 20 21:05:23 2011 +0100
@@ -819,7 +819,7 @@
apply force
done
(* turn into (unsafe, looping!) introduction rule *)
-lemmas unchanged_safeI = impI [THEN unchanged_safe [action_use], standard]
+lemmas unchanged_safeI = impI [THEN unchanged_safe [action_use]]
lemma S1safe: "|- $S1 rmhist p & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p)
--> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
--- a/src/HOL/TLA/TLA.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/TLA/TLA.thy Sun Nov 20 21:05:23 2011 +0100
@@ -149,7 +149,7 @@
section "Simple temporal logic"
(* []~F == []~Init F *)
-lemmas boxNotInit = boxInit [of "LIFT ~F", unfolded Init_simps, standard]
+lemmas boxNotInit = boxInit [of "LIFT ~F", unfolded Init_simps] for F
lemma dmdInit: "TEMP <>F == TEMP <> Init F"
apply (unfold dmd_def)
@@ -157,15 +157,15 @@
apply (simp (no_asm) add: Init_simps)
done
-lemmas dmdNotInit = dmdInit [of "LIFT ~F", unfolded Init_simps, standard]
+lemmas dmdNotInit = dmdInit [of "LIFT ~F", unfolded Init_simps] for F
(* boxInit and dmdInit cannot be used as rewrites, because they loop.
Non-looping instances for state predicates and actions are occasionally useful.
*)
-lemmas boxInit_stp = boxInit [where 'a = state, standard]
-lemmas boxInit_act = boxInit [where 'a = "state * state", standard]
-lemmas dmdInit_stp = dmdInit [where 'a = state, standard]
-lemmas dmdInit_act = dmdInit [where 'a = "state * state", standard]
+lemmas boxInit_stp = boxInit [where 'a = state]
+lemmas boxInit_act = boxInit [where 'a = "state * state"]
+lemmas dmdInit_stp = dmdInit [where 'a = state]
+lemmas dmdInit_act = dmdInit [where 'a = "state * state"]
(* The symmetric equations can be used to get rid of Init *)
lemmas boxInitD = boxInit [symmetric]
@@ -208,14 +208,14 @@
[| (sigma |= []F); (sigma |= [][]F) ==> PROP W |] ==> PROP W
*)
lemmas dup_boxE = STL3 [temp_unlift, THEN iffD2, elim_format]
-lemmas dup_boxD = STL3 [temp_unlift, THEN iffD1, standard]
+lemmas dup_boxD = STL3 [temp_unlift, THEN iffD1]
(* dual versions for <> *)
lemma DmdDmd: "|- (<><>F) = (<>F)"
by (auto simp add: dmd_def [try_rewrite] STL3 [try_rewrite])
lemmas dup_dmdE = DmdDmd [temp_unlift, THEN iffD2, elim_format]
-lemmas dup_dmdD = DmdDmd [temp_unlift, THEN iffD1, standard]
+lemmas dup_dmdD = DmdDmd [temp_unlift, THEN iffD1]
(* ------------------------ STL4 ------------------------------------------- *)
@@ -266,7 +266,7 @@
done
(* rewrite rule to split conjunctions under boxes *)
-lemmas split_box_conj = STL5 [temp_unlift, symmetric, standard]
+lemmas split_box_conj = STL5 [temp_unlift, symmetric]
(* the corresponding elimination rule allows to combine boxes in the hypotheses
@@ -283,9 +283,9 @@
(* Instances of box_conjE for state predicates, actions, and temporals
in case the general rule is "too polymorphic".
*)
-lemmas box_conjE_temp = box_conjE [where 'a = behavior, standard]
-lemmas box_conjE_stp = box_conjE [where 'a = state, standard]
-lemmas box_conjE_act = box_conjE [where 'a = "state * state", standard]
+lemmas box_conjE_temp = box_conjE [where 'a = behavior]
+lemmas box_conjE_stp = box_conjE [where 'a = state]
+lemmas box_conjE_act = box_conjE [where 'a = "state * state"]
(* Define a tactic that tries to merge all boxes in an antecedent. The definition is
a bit kludgy in order to simulate "double elim-resolution".
@@ -318,7 +318,7 @@
(* rewrite rule to push universal quantification through box:
(sigma |= [](! x. F x)) = (! x. (sigma |= []F x))
*)
-lemmas all_box = allT [temp_unlift, symmetric, standard]
+lemmas all_box = allT [temp_unlift, symmetric]
lemma DmdOr: "|- (<>(F | G)) = (<>F | <>G)"
apply (auto simp add: dmd_def split_box_conj [try_rewrite])
@@ -328,7 +328,7 @@
lemma exT: "|- (EX x. <>(F x)) = (<>(EX x. F x))"
by (auto simp: dmd_def Not_Rex [try_rewrite] all_box [try_rewrite])
-lemmas ex_dmd = exT [temp_unlift, symmetric, standard]
+lemmas ex_dmd = exT [temp_unlift, symmetric]
lemma STL4Edup: "!!sigma. [| sigma |= []A; sigma |= []F; |- F & []A --> G |] ==> sigma |= []G"
apply (erule dup_boxE)
@@ -526,7 +526,7 @@
apply (fastforce elim!: TLA2E [temp_use])
done
-lemmas PrimeDmd = InitDmd_gen [temp_use, THEN DmdPrime [temp_use], standard]
+lemmas PrimeDmd = InitDmd_gen [temp_use, THEN DmdPrime [temp_use]]
(* ------------------------ INV1, stable --------------------------------------- *)
section "stable, invariant"
@@ -541,8 +541,8 @@
lemma box_stp_act: "|- ([]$P) = ([]P)"
by (simp add: boxInit_act Init_simps)
-lemmas box_stp_actI = box_stp_act [temp_use, THEN iffD2, standard]
-lemmas box_stp_actD = box_stp_act [temp_use, THEN iffD1, standard]
+lemmas box_stp_actI = box_stp_act [temp_use, THEN iffD2]
+lemmas box_stp_actD = box_stp_act [temp_use, THEN iffD1]
lemmas more_temp_simps3 = box_stp_act [temp_rewrite] more_temp_simps2
@@ -710,7 +710,7 @@
done
(* |- F & (F ~> G) --> <>G *)
-lemmas leadsto_init_temp = leadsto_init [where 'a = behavior, unfolded Init_simps, standard]
+lemmas leadsto_init_temp = leadsto_init [where 'a = behavior, unfolded Init_simps]
lemma streett_leadsto: "|- ([]<>Init F --> []<>G) = (<>(F ~> G))"
apply (unfold leadsto_def)
@@ -776,8 +776,8 @@
elim!: STL4E_gen [temp_use] simp: Init_simps)
done
-lemmas ImplLeadsto = ImplLeadsto_gen [where 'a = behavior and 'b = behavior,
- unfolded Init_simps, standard]
+lemmas ImplLeadsto =
+ ImplLeadsto_gen [where 'a = behavior and 'b = behavior, unfolded Init_simps]
lemma ImplLeadsto_simple: "!!F G. |- F --> G ==> |- F ~> G"
by (auto simp: Init_def intro!: ImplLeadsto_gen [temp_use] necT [temp_use])
@@ -1065,7 +1065,7 @@
(* "wf r ==> |- <>[][ (v`, $v) : #r ]_v --> <>[][#False]_v" *)
lemmas wf_not_dmd_box_decrease =
- wf_not_box_decrease [THEN DmdImpl, unfolded more_temp_simps, standard]
+ wf_not_box_decrease [THEN DmdImpl, unfolded more_temp_simps]
(* If there are infinitely many steps where v decreases, then there
have to be infinitely many non-stuttering steps where v doesn't decrease.
--- a/src/HOL/UNITY/Comp/Alloc.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy Sun Nov 20 21:05:23 2011 +0100
@@ -791,7 +791,7 @@
done
lemmas rename_guarantees_sysOfAlloc_I =
- bij_sysOfAlloc [THEN rename_rename_guarantees_eq, THEN iffD2, standard]
+ bij_sysOfAlloc [THEN rename_rename_guarantees_eq, THEN iffD2]
(*Lifting Alloc_Increasing up to the level of systemState*)
@@ -867,7 +867,7 @@
text{*safety (1), step 2*}
(* i < Nclients ==> System : Increasing (sub i o allocRel) *)
-lemmas System_Increasing_allocRel = System_Follows_rel [THEN Follows_Increasing1, standard]
+lemmas System_Increasing_allocRel = System_Follows_rel [THEN Follows_Increasing1]
(*Lifting Alloc_safety up to the level of systemState.
Simplifying with o_def gets rid of the translations but it unfortunately
@@ -921,7 +921,7 @@
text{*progress (2), step 2; see also @{text System_Increasing_allocRel}*}
(* i < Nclients ==> System : Increasing (sub i o allocAsk) *)
-lemmas System_Increasing_allocAsk = System_Follows_ask [THEN Follows_Increasing1, standard]
+lemmas System_Increasing_allocAsk = System_Follows_ask [THEN Follows_Increasing1]
text{*progress (2), step 3: lifting @{text Client_Bounded} to systemState*}
lemma rename_Client_Bounded: "i : I
@@ -955,7 +955,7 @@
text{*progress (2), step 6*}
(* i < Nclients ==> System : Increasing (giv o sub i o client) *)
-lemmas System_Increasing_giv = System_Follows_allocGiv [THEN Follows_Increasing1, standard]
+lemmas System_Increasing_giv = System_Follows_allocGiv [THEN Follows_Increasing1]
lemma rename_Client_Progress: "i: I
--- a/src/HOL/UNITY/Constrains.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/UNITY/Constrains.thy Sun Nov 20 21:05:23 2011 +0100
@@ -86,8 +86,7 @@
(*F \<in> B co B' ==> F \<in> (reachable F \<inter> B) co (reachable F \<inter> B')*)
lemmas constrains_reachable_Int =
- subset_refl [THEN stable_reachable [unfolded stable_def],
- THEN constrains_Int, standard]
+ subset_refl [THEN stable_reachable [unfolded stable_def], THEN constrains_Int]
(*Resembles the previous definition of Constrains*)
lemma Constrains_eq_constrains:
@@ -263,8 +262,7 @@
apply (blast intro: stable_imp_Stable)
done
-lemmas Increasing_constant =
- increasing_constant [THEN increasing_imp_Increasing, standard, iff]
+lemmas Increasing_constant = increasing_constant [THEN increasing_imp_Increasing, iff]
subsection{*The Elimination Theorem*}
@@ -294,8 +292,8 @@
lemma AlwaysD: "F \<in> Always A ==> Init F \<subseteq> A & F \<in> Stable A"
by (simp add: Always_def)
-lemmas AlwaysE = AlwaysD [THEN conjE, standard]
-lemmas Always_imp_Stable = AlwaysD [THEN conjunct2, standard]
+lemmas AlwaysE = AlwaysD [THEN conjE]
+lemmas Always_imp_Stable = AlwaysD [THEN conjunct2]
(*The set of all reachable states is Always*)
@@ -312,8 +310,7 @@
apply (blast intro: constrains_imp_Constrains)
done
-lemmas Always_reachable =
- invariant_reachable [THEN invariant_imp_Always, standard]
+lemmas Always_reachable = invariant_reachable [THEN invariant_imp_Always]
lemma Always_eq_invariant_reachable:
"Always A = {F. F \<in> invariant (reachable F \<inter> A)}"
@@ -355,10 +352,10 @@
Constrains_eq_constrains Int_assoc [symmetric])
(* [| F \<in> Always INV; F \<in> (INV \<inter> A) Co A' |] ==> F \<in> A Co A' *)
-lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1, standard]
+lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1]
(* [| F \<in> Always INV; F \<in> A Co A' |] ==> F \<in> A Co (INV \<inter> A') *)
-lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2, standard]
+lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2]
(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
lemma Always_Constrains_weaken:
@@ -390,7 +387,7 @@
(*Delete the nearest invariance assumption (which will be the second one
used by Always_Int_I) *)
-lemmas Always_thin = thin_rl [of "F \<in> Always A", standard]
+lemmas Always_thin = thin_rl [of "F \<in> Always A"]
subsection{*Totalize*}
--- a/src/HOL/UNITY/ELT.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/UNITY/ELT.thy Sun Nov 20 21:05:23 2011 +0100
@@ -418,7 +418,7 @@
apply (blast intro: subset_imp_leadsETo)
done
-lemmas empty_LeadsETo = empty_subsetI [THEN subset_imp_LeadsETo, standard]
+lemmas empty_LeadsETo = empty_subsetI [THEN subset_imp_LeadsETo]
lemma LeadsETo_weaken_R [rule_format]:
"[| F : A LeadsTo[CC] A'; A' <= B' |] ==> F : A LeadsTo[CC] B'"
--- a/src/HOL/UNITY/Rename.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/UNITY/Rename.thy Sun Nov 20 21:05:23 2011 +0100
@@ -140,7 +140,7 @@
lemma bij_rename: "bij h ==> bij (rename h)"
apply (simp (no_asm_simp) add: rename_def bij_extend)
done
-lemmas surj_rename = bij_rename [THEN bij_is_surj, standard]
+lemmas surj_rename = bij_rename [THEN bij_is_surj]
lemma inj_rename_imp_inj: "inj (rename h) ==> inj h"
apply (unfold inj_on_def, auto)
--- a/src/HOL/UNITY/Simple/Reachability.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/UNITY/Simple/Reachability.thy Sun Nov 20 21:05:23 2011 +0100
@@ -69,8 +69,8 @@
MA7: "[|v \<in> V;w \<in> V|] ==> F \<in> UNIV LeadsTo nmsg_eq 0 (v,w)"
-lemmas E_imp_in_V_L = Graph2 [THEN conjunct1, standard]
-lemmas E_imp_in_V_R = Graph2 [THEN conjunct2, standard]
+lemmas E_imp_in_V_L = Graph2 [THEN conjunct1]
+lemmas E_imp_in_V_R = Graph2 [THEN conjunct2]
lemma lemma2:
"(v,w) \<in> E ==> F \<in> reachable v LeadsTo nmsg_eq 0 (v,w) \<inter> reachable v"
--- a/src/HOL/UNITY/SubstAx.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/UNITY/SubstAx.thy Sun Nov 20 21:05:23 2011 +0100
@@ -42,10 +42,10 @@
Int_assoc [symmetric])
(* [| F \<in> Always C; F \<in> (C \<inter> A) LeadsTo A' |] ==> F \<in> A LeadsTo A' *)
-lemmas Always_LeadsToI = Always_LeadsTo_pre [THEN iffD1, standard]
+lemmas Always_LeadsToI = Always_LeadsTo_pre [THEN iffD1]
(* [| F \<in> Always INV; F \<in> A LeadsTo A' |] ==> F \<in> A LeadsTo (INV \<inter> A') *)
-lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2, standard]
+lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2]
subsection{*Introduction rules: Basis, Trans, Union*}
@@ -104,7 +104,7 @@
apply (blast intro: subset_imp_leadsTo)
done
-lemmas empty_LeadsTo = empty_subsetI [THEN subset_imp_LeadsTo, standard, simp]
+lemmas empty_LeadsTo = empty_subsetI [THEN subset_imp_LeadsTo, simp]
lemma LeadsTo_weaken_R:
"[| F \<in> A LeadsTo A'; A' \<subseteq> B' |] ==> F \<in> A LeadsTo B'"
--- a/src/HOL/UNITY/UNITY.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/UNITY/UNITY.thy Sun Nov 20 21:05:23 2011 +0100
@@ -274,7 +274,7 @@
by (unfold stable_def constrains_def, blast)
(*[| F \<in> stable C; F \<in> (C \<inter> A) co A |] ==> F \<in> stable (C \<inter> A) *)
-lemmas stable_constrains_stable = stable_constrains_Int[THEN stableI, standard]
+lemmas stable_constrains_stable = stable_constrains_Int[THEN stableI]
subsubsection{*invariant*}
--- a/src/HOL/UNITY/Union.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/UNITY/Union.thy Sun Nov 20 21:05:23 2011 +0100
@@ -332,7 +332,7 @@
lemma ok_commute: "(F ok G) = (G ok F)"
by (auto simp add: ok_def)
-lemmas ok_sym = ok_commute [THEN iffD1, standard]
+lemmas ok_sym = ok_commute [THEN iffD1]
lemma ok_iff_OK:
"OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F\<squnion>G) ok H)"
--- a/src/HOL/UNITY/WFair.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/UNITY/WFair.thy Sun Nov 20 21:05:23 2011 +0100
@@ -235,13 +235,13 @@
lemma subset_imp_ensures: "A \<subseteq> B ==> F \<in> A ensures B"
by (unfold ensures_def constrains_def transient_def, blast)
-lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis, standard]
+lemmas subset_imp_leadsTo = subset_imp_ensures [THEN leadsTo_Basis]
-lemmas leadsTo_refl = subset_refl [THEN subset_imp_leadsTo, standard]
+lemmas leadsTo_refl = subset_refl [THEN subset_imp_leadsTo]
-lemmas empty_leadsTo = empty_subsetI [THEN subset_imp_leadsTo, standard, simp]
+lemmas empty_leadsTo = empty_subsetI [THEN subset_imp_leadsTo, simp]
-lemmas leadsTo_UNIV = subset_UNIV [THEN subset_imp_leadsTo, standard, simp]
+lemmas leadsTo_UNIV = subset_UNIV [THEN subset_imp_leadsTo, simp]
--- a/src/HOL/ex/Gauge_Integration.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/ex/Gauge_Integration.thy Sun Nov 20 21:05:23 2011 +0100
@@ -45,7 +45,7 @@
\<Longrightarrow> fine \<delta> (a, c) ((a, x, b) # D)"
lemmas fine_induct [induct set: fine] =
- fine.induct [of "\<delta>" "(a,b)" "D" "split P", unfolded split_conv, standard]
+ fine.induct [of "\<delta>" "(a,b)" "D" "split P", unfolded split_conv] for \<delta> a b D P
lemma fine_single:
"\<lbrakk>a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk> \<Longrightarrow> fine \<delta> (a, b) [(a, x, b)]"
--- a/src/HOL/ex/Tree23.thy Sun Nov 20 20:59:30 2011 +0100
+++ b/src/HOL/ex/Tree23.thy Sun Nov 20 21:05:23 2011 +0100
@@ -330,12 +330,13 @@
"dfull n (Some (p, (False, t'))) \<longleftrightarrow> full (Suc n) t'"
lemmas dfull_case_intros =
- ord.exhaust [where y=y and P="dfull a (ord_case b c d y)", standard]
- option.exhaust [where y=y and P="dfull a (option_case b c y)", standard]
- prod.exhaust [where y=y and P="dfull a (prod_case b y)", standard]
- bool.exhaust [where y=y and P="dfull a (bool_case b c y)", standard]
- tree23.exhaust [where y=y and P="dfull a (Some (b, tree23_case c d e y))", standard]
- tree23.exhaust [where y=y and P="full a (tree23_case b c d y)", standard]
+ ord.exhaust [where y=y and P="dfull a (ord_case b c d y)"]
+ option.exhaust [where y=y and P="dfull a (option_case b c y)"]
+ prod.exhaust [where y=y and P="dfull a (prod_case b y)"]
+ bool.exhaust [where y=y and P="dfull a (bool_case b c y)"]
+ tree23.exhaust [where y=y and P="dfull a (Some (b, tree23_case c d e y))"]
+ tree23.exhaust [where y=y and P="full a (tree23_case b c d y)"]
+ for a b c d e y
lemma dfull_del: "full (Suc n) t \<Longrightarrow> dfull n (del k t)"
proof -