tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
--- a/src/CCL/Type.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/CCL/Type.thy Sat Jul 21 23:25:00 2007 +0200
@@ -130,15 +130,15 @@
val bexE = thm "bexE"
in
- fun mk_ncanT_tac thy defs top_crls crls s = prove_goalw thy defs s
+ fun mk_ncanT_tac ctxt defs top_crls crls s = prove_goalw (ProofContext.theory_of ctxt) defs s
(fn major::prems => [(resolve_tac ([major] RL top_crls) 1),
(REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))),
- (ALLGOALS (asm_simp_tac (simpset ()))),
+ (ALLGOALS (asm_simp_tac (local_simpset_of ctxt))),
(ALLGOALS (ares_tac (prems RL [lemma]) ORELSE'
etac bspec )),
- (safe_tac (claset () addSIs prems))])
+ (safe_tac (local_claset_of ctxt addSIs prems))])
- val ncanT_tac = mk_ncanT_tac (the_context ()) [] case_rls case_rls
+ val ncanT_tac = mk_ncanT_tac @{context} [] case_rls case_rls
end
*}
@@ -275,7 +275,7 @@
lemmas icanTs = zeroT succT nilT consT
ML {*
-val incanT_tac = mk_ncanT_tac (the_context ()) [] (thms "icase_rls") (thms "case_rls");
+val incanT_tac = mk_ncanT_tac @{context} [] (thms "icase_rls") (thms "case_rls");
bind_thm ("ncaseT", incanT_tac
"[| n:Nat; n=zero ==> b:C(zero); !!x.[| x:Nat; n=succ(x) |] ==> c(x):C(succ(x)) |] ==> ncase(n,b,c) : C(n)");
@@ -469,18 +469,18 @@
"[| <h,h'> : lfp(%x. EQgen(x) Un R Un EQ); <t,t'> : lfp(%x. EQgen(x) Un R Un EQ) |] ==> <h$t,h'$t'> : EQgen(lfp(%x. EQgen(x) Un R Un EQ))"];
fun EQgen_raw_tac i =
- (REPEAT (resolve_tac (EQgenIs @ [thm "EQ_refl" RS (thm "EQgen_mono" RS ci3_AI)] @
- (EQgenIs RL [thm "EQgen_mono" RS ci3_AgenI]) @ [thm "EQgen_mono" RS ci3_RI]) i))
+ (REPEAT (resolve_tac (EQgenIs @ [@{thm EQ_refl} RS (@{thm EQgen_mono} RS ci3_AI)] @
+ (EQgenIs RL [@{thm EQgen_mono} RS ci3_AgenI]) @ [@{thm EQgen_mono} RS ci3_RI]) i))
(* Goals of the form R <= EQgen(R) - rewrite elements <a,b> : EQgen(R) using rews and *)
(* then reduce this to a goal <a',b'> : R (hopefully?) *)
(* rews are rewrite rules that would cause looping in the simpifier *)
-fun EQgen_tac simp_set rews i =
+fun EQgen_tac ctxt rews i =
SELECT_GOAL
- (TRY (CLASET safe_tac) THEN
- resolve_tac ((rews@[refl]) RL ((rews@[refl]) RL [thm "ssubst_pair"])) i THEN
- ALLGOALS (simp_tac simp_set) THEN
+ (TRY (safe_tac (local_claset_of ctxt)) THEN
+ resolve_tac ((rews@[refl]) RL ((rews@[refl]) RL [@{thm ssubst_pair}])) i THEN
+ ALLGOALS (simp_tac (local_simpset_of ctxt)) THEN
ALLGOALS EQgen_raw_tac) i
*}
--- a/src/CCL/ex/Flag.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/CCL/ex/Flag.thy Sat Jul 21 23:25:00 2007 +0200
@@ -56,7 +56,7 @@
unfolding ColourXH by blast+
ML {*
-bind_thm ("ccaseT", mk_ncanT_tac (the_context ())
+bind_thm ("ccaseT", mk_ncanT_tac @{context}
(thms "flag_defs") (thms "case_rls") (thms "case_rls")
"[| c:Colour; c=red ==> r : C(red); c=white ==> w : C(white); c=blue ==> b : C(blue) |] ==> ccase(c,r,w,b) : C(c)");
*}
--- a/src/CCL/ex/Stream.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/CCL/ex/Stream.thy Sat Jul 21 23:25:00 2007 +0200
@@ -37,7 +37,7 @@
apply (blast intro: 1)
apply safe
apply (drule ListsXH [THEN iffD1])
- apply (tactic "EQgen_tac (simpset ()) [] 1")
+ apply (tactic "EQgen_tac @{context} [] 1")
apply fastsimp
done
@@ -51,7 +51,7 @@
apply (blast intro: 1)
apply safe
apply (drule ListsXH [THEN iffD1])
- apply (tactic "EQgen_tac (simpset ()) [] 1")
+ apply (tactic "EQgen_tac @{context} [] 1")
apply blast
done
@@ -67,9 +67,9 @@
apply (blast intro: prems)
apply safe
apply (drule ListsXH [THEN iffD1])
- apply (tactic "EQgen_tac (simpset ()) [] 1")
+ apply (tactic "EQgen_tac @{context} [] 1")
apply (drule ListsXH [THEN iffD1])
- apply (tactic "EQgen_tac (simpset ()) [] 1")
+ apply (tactic "EQgen_tac @{context} [] 1")
apply blast
done
@@ -86,11 +86,11 @@
apply (blast intro: prems)
apply safe
apply (drule ListsXH [THEN iffD1])
- apply (tactic "EQgen_tac (simpset ()) [] 1")
+ apply (tactic "EQgen_tac @{context} [] 1")
prefer 2
apply blast
apply (tactic {* DEPTH_SOLVE (etac (XH_to_E (thm "ListsXH")) 1
- THEN EQgen_tac (simpset ()) [] 1) *})
+ THEN EQgen_tac @{context} [] 1) *})
done
@@ -104,7 +104,7 @@
apply (blast intro: prems)
apply safe
apply (drule IListsXH [THEN iffD1])
- apply (tactic "EQgen_tac (simpset ()) [] 1")
+ apply (tactic "EQgen_tac @{context} [] 1")
apply blast
done
@@ -136,7 +136,7 @@
apply (tactic {* eq_coinduct3_tac
"{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1 (f,f^n`a) & y=map (f) ^n`iter2 (f,a))}" 1*})
apply (fast intro!: napplyBzero [symmetric] napplyBzero [symmetric, THEN arg_cong])
- apply (tactic {* EQgen_tac (simpset ()) [thm "iter1B", thm "iter2Blemma"] 1 *})
+ apply (tactic {* EQgen_tac @{context} [thm "iter1B", thm "iter2Blemma"] 1 *})
apply (subst napply_f, assumption)
apply (rule_tac f1 = f in napplyBsucc [THEN subst])
apply blast
--- a/src/HOL/Algebra/abstract/Ideal2.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/Algebra/abstract/Ideal2.thy Sat Jul 21 23:25:00 2007 +0200
@@ -275,7 +275,7 @@
apply (unfold prime_def)
apply (rule conjI)
apply (rule_tac [2] conjI)
- apply (tactic "Clarify_tac 3")
+ apply (tactic "clarify_tac @{claset} 3")
apply (drule_tac [3] I = "ideal_of {a, b}" and x = "1" in irred_imp_max_ideal)
apply (auto intro: ideal_of_is_ideal pid_ax simp add: irred_def not_dvd_psubideal pid_ax)
apply (simp add: ideal_of_2_structure)
--- a/src/HOL/Algebra/abstract/Ring2.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy Sat Jul 21 23:25:00 2007 +0200
@@ -495,7 +495,7 @@
(* fields are integral domains *)
lemma field_integral: "!! a::'a::field. a * b = 0 ==> a = 0 | b = 0"
- apply (tactic "Step_tac 1")
+ apply (tactic "step_tac @{claset} 1")
apply (rule_tac a = " (a*b) * inverse b" in box_equals)
apply (rule_tac [3] refl)
prefer 2
--- a/src/HOL/Auth/Public.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/Auth/Public.thy Sat Jul 21 23:25:00 2007 +0200
@@ -425,31 +425,31 @@
ML
{*
-val Nonce_supply = thm "Nonce_supply";
-
-(*Tactic for possibility theorems (Isar interface)*)
-fun gen_possibility_tac ss state = state |>
+(*Tactic for possibility theorems*)
+fun possibility_tac ctxt =
REPEAT (*omit used_Says so that Nonces start from different traces!*)
- (ALLGOALS (simp_tac (ss delsimps [used_Says]))
+ (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says]))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
- resolve_tac [refl, conjI, Nonce_supply]))
-
-(*Tactic for possibility theorems (ML script version)*)
-fun possibility_tac state = gen_possibility_tac (simpset()) state
+ resolve_tac [refl, conjI, @{thm Nonce_supply}]))
(*For harder protocols (such as Recur) where we have to set up some
nonces and keys initially*)
-fun basic_possibility_tac st = st |>
+fun basic_possibility_tac ctxt =
REPEAT
- (ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver))
+ (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
THEN
REPEAT_FIRST (resolve_tac [refl, conjI]))
*}
method_setup possibility = {*
Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (gen_possibility_tac (local_simpset_of ctxt))) *}
+ Method.SIMPLE_METHOD (possibility_tac ctxt)) *}
+ "for proving possibility theorems"
+
+method_setup basic_possibility = {*
+ Method.ctxt_args (fn ctxt =>
+ Method.SIMPLE_METHOD (basic_possibility_tac ctxt)) *}
"for proving possibility theorems"
end
--- a/src/HOL/Auth/Recur.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/Auth/Recur.thy Sat Jul 21 23:25:00 2007 +0200
@@ -163,7 +163,7 @@
[OF _ _ respond.One
[THEN respond.Cons, THEN respond.Cons]],
THEN recur.RA4, THEN recur.RA4])
-apply (tactic "basic_possibility_tac")
+apply basic_possibility
apply (tactic "DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1)")
done
--- a/src/HOL/Auth/Shared.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/Auth/Shared.thy Sat Jul 21 23:25:00 2007 +0200
@@ -195,22 +195,19 @@
{*
(*Omitting used_Says makes the tactic much faster: it leaves expressions
such as Nonce ?N \<notin> used evs that match Nonce_supply*)
-fun gen_possibility_tac ss state = state |>
+fun possibility_tac ctxt =
(REPEAT
- (ALLGOALS (simp_tac (ss delsimps [used_Says, used_Notes, used_Gets]
+ (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says, used_Notes, used_Gets]
setSolver safe_solver))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac [refl, conjI, Nonce_supply])))
-(*Tactic for possibility theorems (ML script version)*)
-fun possibility_tac state = gen_possibility_tac (simpset()) state
-
(*For harder protocols (such as Recur) where we have to set up some
nonces and keys initially*)
-fun basic_possibility_tac st = st |>
+fun basic_possibility_tac ctxt =
REPEAT
- (ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver))
+ (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
THEN
REPEAT_FIRST (resolve_tac [refl, conjI]))
*}
@@ -273,10 +270,15 @@
method_setup possibility = {*
Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (gen_possibility_tac (local_simpset_of ctxt))) *}
+ Method.SIMPLE_METHOD (possibility_tac ctxt)) *}
+ "for proving possibility theorems"
+
+method_setup basic_possibility = {*
+ Method.ctxt_args (fn ctxt =>
+ Method.SIMPLE_METHOD (basic_possibility_tac ctxt)) *}
"for proving possibility theorems"
lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
-by (induct e, auto simp: knows_Cons)
+by (induct e) (auto simp: knows_Cons)
end
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Sat Jul 21 23:25:00 2007 +0200
@@ -756,13 +756,13 @@
(*SR11*) forward_tac [Outpts_A_Card_form_10] 21 THEN
eresolve_tac [exE] 22 THEN eresolve_tac [exE] 22
-val parts_prepare_tac =
+fun parts_prepare_tac ctxt =
prepare_tac THEN
(*SR9*) dresolve_tac [Gets_imp_knows_Spy_parts_Snd] 18 THEN
(*SR9*) dresolve_tac [Gets_imp_knows_Spy_parts_Snd] 19 THEN
(*Oops1*) dresolve_tac [Outpts_B_Card_form_7] 25 THEN
(*Oops2*) dresolve_tac [Outpts_A_Card_form_10] 27 THEN
- (*Base*) Force_tac 1
+ (*Base*) (force_tac (local_clasimpset_of ctxt)) 1
val analz_prepare_tac =
prepare_tac THEN
@@ -777,7 +777,7 @@
"to launch a few simple facts that'll help the simplifier"
method_setup parts_prepare = {*
- Method.no_args (Method.SIMPLE_METHOD parts_prepare_tac) *}
+ Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (parts_prepare_tac ctxt)) *}
"additional facts to reason about parts"
method_setup analz_prepare = {*
@@ -1386,10 +1386,4 @@
apply auto
done
-
-
-
-
-
end
-
--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Sat Jul 21 23:25:00 2007 +0200
@@ -758,22 +758,22 @@
val Gets_imp_knows_Spy_parts_Snd = thm "Gets_imp_knows_Spy_parts_Snd"
val Gets_imp_knows_Spy_analz_Snd = thm "Gets_imp_knows_Spy_analz_Snd"
-val prepare_tac =
+fun prepare_tac ctxt =
(*SR_U8*) forward_tac [Outpts_B_Card_form_7] 14 THEN
- (*SR_U8*) Clarify_tac 15 THEN
+ (*SR_U8*) clarify_tac (local_claset_of ctxt) 15 THEN
(*SR_U9*) forward_tac [Outpts_A_Card_form_4] 16 THEN
(*SR_U11*) forward_tac [Outpts_A_Card_form_10] 21
-val parts_prepare_tac =
- prepare_tac THEN
+fun parts_prepare_tac ctxt =
+ prepare_tac ctxt THEN
(*SR_U9*) dresolve_tac [Gets_imp_knows_Spy_parts_Snd] 18 THEN
(*SR_U9*) dresolve_tac [Gets_imp_knows_Spy_parts_Snd] 19 THEN
(*Oops1*) dresolve_tac [Outpts_B_Card_form_7] 25 THEN
(*Oops2*) dresolve_tac [Outpts_A_Card_form_10] 27 THEN
- (*Base*) Force_tac 1
+ (*Base*) (force_tac (local_clasimpset_of ctxt)) 1
-val analz_prepare_tac =
- prepare_tac THEN
+fun analz_prepare_tac ctxt =
+ prepare_tac ctxt THEN
dtac (Gets_imp_knows_Spy_analz_Snd) 18 THEN
(*SR_U9*) dtac (Gets_imp_knows_Spy_analz_Snd) 19 THEN
REPEAT_FIRST (eresolve_tac [asm_rl, conjE] ORELSE' hyp_subst_tac)
@@ -781,15 +781,15 @@
*}
method_setup prepare = {*
- Method.no_args (Method.SIMPLE_METHOD prepare_tac) *}
+ Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (prepare_tac ctxt)) *}
"to launch a few simple facts that'll help the simplifier"
method_setup parts_prepare = {*
- Method.no_args (Method.SIMPLE_METHOD parts_prepare_tac) *}
+ Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (parts_prepare_tac ctxt)) *}
"additional facts to reason about parts"
method_setup analz_prepare = {*
- Method.no_args (Method.SIMPLE_METHOD analz_prepare_tac) *}
+ Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (analz_prepare_tac ctxt)) *}
"additional facts to reason about analz"
--- a/src/HOL/Auth/Smartcard/Smartcard.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy Sat Jul 21 23:25:00 2007 +0200
@@ -359,23 +359,20 @@
{*
(*Omitting used_Says makes the tactic much faster: it leaves expressions
such as Nonce ?N \<notin> used evs that match Nonce_supply*)
-fun gen_possibility_tac ss state = state |>
+fun possibility_tac ctxt =
(REPEAT
- (ALLGOALS (simp_tac (ss delsimps [used_Says, used_Notes, used_Gets,
+ (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says, used_Notes, used_Gets,
used_Inputs, used_C_Gets, used_Outpts, used_A_Gets]
setSolver safe_solver))
THEN
REPEAT_FIRST (eq_assume_tac ORELSE'
resolve_tac [refl, conjI, Nonce_supply])))
-(*Tactic for possibility theorems (ML script version)*)
-fun possibility_tac state = gen_possibility_tac (simpset()) state
-
(*For harder protocols (such as Recur) where we have to set up some
nonces and keys initially*)
-fun basic_possibility_tac st = st |>
+fun basic_possibility_tac ctxt =
REPEAT
- (ALLGOALS (asm_simp_tac (simpset() setSolver safe_solver))
+ (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
THEN
REPEAT_FIRST (resolve_tac [refl, conjI]))
*}
@@ -426,8 +423,8 @@
val analz_image_freshK_lemma = thm "analz_image_freshK_lemma";
val analz_image_freshK_ss =
- simpset() delsimps [image_insert, image_Un]
- delsimps [imp_disjL] (*reduces blow-up*)
+ @{simpset} delsimps [image_insert, image_Un]
+ delsimps [@{thm imp_disjL}] (*reduces blow-up*)
addsimps thms "analz_image_freshK_simps"
*}
@@ -450,11 +447,16 @@
method_setup possibility = {*
Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD (gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
+ Method.SIMPLE_METHOD (possibility_tac ctxt)) *}
+ "for proving possibility theorems"
+
+method_setup basic_possibility = {*
+ Method.ctxt_args (fn ctxt =>
+ Method.SIMPLE_METHOD (basic_possibility_tac ctxt)) *}
"for proving possibility theorems"
lemma knows_subset_knows_Cons: "knows A evs \<subseteq> knows A (e # evs)"
-by (induct e, auto simp: knows_Cons)
+by (induct e) (auto simp: knows_Cons)
(*Needed for actual protocols that will follow*)
declare shrK_disj_crdK[THEN not_sym, iff]
@@ -466,8 +468,4 @@
declare legalUse_def [iff] illegalUse_def [iff]
-
-
-
-
end
--- a/src/HOL/Bali/AxCompl.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/Bali/AxCompl.thy Sat Jul 21 23:25:00 2007 +0200
@@ -1404,7 +1404,7 @@
using finU uA
apply -
apply (induct_tac "n")
-apply (tactic "ALLGOALS Clarsimp_tac")
+apply (tactic "ALLGOALS (clarsimp_tac @{clasimpset})")
apply (tactic {* dtac (permute_prems 0 1 (thm "card_seteq")) 1 *})
apply simp
apply (erule finite_imageI)
--- a/src/HOL/Bali/AxSem.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/Bali/AxSem.thy Sat Jul 21 23:25:00 2007 +0200
@@ -670,7 +670,7 @@
lemma ax_thin [rule_format (no_asm)]:
"G,(A'::'a triple set)|\<turnstile>(ts::'a triple set) \<Longrightarrow> \<forall>A. A' \<subseteq> A \<longrightarrow> G,A|\<turnstile>ts"
apply (erule ax_derivs.induct)
-apply (tactic "ALLGOALS(EVERY'[Clarify_tac,REPEAT o smp_tac 1])")
+apply (tactic "ALLGOALS(EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1])")
apply (rule ax_derivs.empty)
apply (erule (1) ax_derivs.insert)
apply (fast intro: ax_derivs.asm)
@@ -712,7 +712,7 @@
apply (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *))
(*37 subgoals*)
apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros"))
- THEN_ALL_NEW Fast_tac) *})
+ THEN_ALL_NEW fast_tac @{claset}) *})
(*1 subgoal*)
apply (clarsimp simp add: subset_mtriples_iff)
apply (rule ax_derivs.Methd)
--- a/src/HOL/HoareParallel/Gar_Coll.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/HoareParallel/Gar_Coll.thy Sat Jul 21 23:25:00 2007 +0200
@@ -792,7 +792,7 @@
--{* 32 subgoals left *}
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
--{* 20 subgoals left *}
-apply(tactic{* TRYALL Clarify_tac *})
+apply(tactic{* TRYALL (clarify_tac @{claset}) *})
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
apply(tactic {* TRYALL (etac disjE) *})
apply simp_all
@@ -812,7 +812,7 @@
apply(tactic {* TRYALL (interfree_aux_tac) *})
--{* 64 subgoals left *}
apply(simp_all add:nth_list_update Invariants Append_to_free0)+
-apply(tactic{* TRYALL Clarify_tac *})
+apply(tactic{* TRYALL (clarify_tac @{claset}) *})
--{* 4 subgoals left *}
apply force
apply(simp add:Append_to_free2)
--- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy Sat Jul 21 23:25:00 2007 +0200
@@ -133,7 +133,7 @@
apply(simp_all add:mul_mutator_interfree)
apply(simp_all add: mul_mutator_defs)
apply(tactic {* TRYALL (interfree_aux_tac) *})
-apply(tactic {* ALLGOALS Clarify_tac *})
+apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
apply (simp_all add:nth_list_update)
done
@@ -1135,7 +1135,7 @@
interfree_aux (Some(Mul_Append n),{}, Some(Mul_Redirect_Edge j n))"
apply (unfold mul_modules)
apply interfree_aux
-apply(tactic {* ALLGOALS Clarify_tac *})
+apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
apply(simp_all add:Graph6 Append_to_free0 Append_to_free1 mul_collector_defs mul_mutator_defs Mul_AppendInv_def)
apply(erule_tac x=j in allE, force dest:Graph3)+
done
@@ -1144,7 +1144,7 @@
interfree_aux (Some(Mul_Redirect_Edge j n),{},Some(Mul_Append n))"
apply (unfold mul_modules)
apply interfree_aux
-apply(tactic {* ALLGOALS Clarify_tac *})
+apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
apply(simp_all add:mul_collector_defs Append_to_free0 Mul_AppendInv_def mul_mutator_defs nth_list_update)
done
@@ -1152,7 +1152,7 @@
interfree_aux (Some(Mul_Append n),{}, Some(Mul_Color_Target j n))"
apply (unfold mul_modules)
apply interfree_aux
-apply(tactic {* ALLGOALS Clarify_tac *})
+apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
apply(simp_all add:mul_mutator_defs mul_collector_defs Mul_AppendInv_def Graph7 Graph8 Append_to_free0 Append_to_free1
Graph12 nth_list_update)
done
@@ -1161,7 +1161,7 @@
interfree_aux (Some(Mul_Color_Target j n),{}, Some(Mul_Append n))"
apply (unfold mul_modules)
apply interfree_aux
-apply(tactic {* ALLGOALS Clarify_tac *})
+apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
apply(simp_all add: mul_mutator_defs nth_list_update)
apply(simp add:Mul_AppendInv_def Append_to_free0)
done
@@ -1190,7 +1190,7 @@
--{* 24 subgoals left *}
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
--{* 14 subgoals left *}
-apply(tactic {* TRYALL Clarify_tac *})
+apply(tactic {* TRYALL (clarify_tac @{claset}) *})
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
apply(tactic {* TRYALL (rtac conjI) *})
apply(tactic {* TRYALL (rtac impI) *})
--- a/src/HOL/HoareParallel/OG_Examples.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/HoareParallel/OG_Examples.thy Sat Jul 21 23:25:00 2007 +0200
@@ -171,10 +171,10 @@
--{* 35 vc *}
apply simp_all
--{* 21 vc *}
-apply(tactic {* ALLGOALS Clarify_tac *})
+apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
--{* 11 vc *}
apply simp_all
-apply(tactic {* ALLGOALS Clarify_tac *})
+apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
--{* 10 subgoals left *}
apply(erule less_SucE)
apply simp
@@ -431,17 +431,17 @@
.{ \<forall>k<length a. (a ! k)=(\<acute>b ! k)}."
apply oghoare
--{* 138 vc *}
-apply(tactic {* ALLGOALS Clarify_tac *})
+apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
--{* 112 subgoals left *}
apply(simp_all (no_asm))
apply(tactic {*ALLGOALS (conjI_Tac (K all_tac)) *})
--{* 930 subgoals left *}
-apply(tactic {* ALLGOALS Clarify_tac *})
+apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
apply(simp_all (asm_lr) only:length_0_conv [THEN sym])
--{* 44 subgoals left *}
apply (simp_all (asm_lr) del:length_0_conv add: nth_list_update mod_less_divisor mod_lemma)
--{* 32 subgoals left *}
-apply(tactic {* ALLGOALS Clarify_tac *})
+apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
apply(tactic {* TRYALL simple_arith_tac *})
--{* 9 subgoals left *}
@@ -538,7 +538,7 @@
.{\<acute>x=n}."
apply oghoare
apply (simp_all cong del: strong_setsum_cong)
-apply (tactic {* ALLGOALS Clarify_tac *})
+apply (tactic {* ALLGOALS (clarify_tac @{claset}) *})
apply (simp_all cong del: strong_setsum_cong)
apply(erule (1) Example2_lemma2)
apply(erule (1) Example2_lemma2)
--- a/src/HOL/HoareParallel/OG_Tactics.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/HoareParallel/OG_Tactics.thy Sat Jul 21 23:25:00 2007 +0200
@@ -320,119 +320,119 @@
ML {*
- fun WlpTac i = (rtac (thm "SeqRule") i) THEN (HoareRuleTac false (i+1))
+ fun WlpTac i = (rtac (@{thm SeqRule}) i) THEN (HoareRuleTac false (i+1))
and HoareRuleTac precond i st = st |>
( (WlpTac i THEN HoareRuleTac precond i)
ORELSE
- (FIRST[rtac (thm "SkipRule") i,
- rtac (thm "BasicRule") i,
- EVERY[rtac (thm "ParallelConseqRule") i,
+ (FIRST[rtac (@{thm SkipRule}) i,
+ rtac (@{thm BasicRule}) i,
+ EVERY[rtac (@{thm ParallelConseqRule}) i,
ParallelConseq (i+2),
ParallelTac (i+1),
ParallelConseq i],
- EVERY[rtac (thm "CondRule") i,
+ EVERY[rtac (@{thm CondRule}) i,
HoareRuleTac false (i+2),
HoareRuleTac false (i+1)],
- EVERY[rtac (thm "WhileRule") i,
+ EVERY[rtac (@{thm WhileRule}) i,
HoareRuleTac true (i+1)],
K all_tac i ]
- THEN (if precond then (K all_tac i) else (rtac (thm "subset_refl") i))))
+ THEN (if precond then (K all_tac i) else (rtac (@{thm subset_refl}) i))))
-and AnnWlpTac i = (rtac (thm "AnnSeq") i) THEN (AnnHoareRuleTac (i+1))
+and AnnWlpTac i = (rtac (@{thm AnnSeq}) i) THEN (AnnHoareRuleTac (i+1))
and AnnHoareRuleTac i st = st |>
( (AnnWlpTac i THEN AnnHoareRuleTac i )
ORELSE
- (FIRST[(rtac (thm "AnnskipRule") i),
- EVERY[rtac (thm "AnnatomRule") i,
+ (FIRST[(rtac (@{thm AnnskipRule}) i),
+ EVERY[rtac (@{thm AnnatomRule}) i,
HoareRuleTac true (i+1)],
- (rtac (thm "AnnwaitRule") i),
- rtac (thm "AnnBasic") i,
- EVERY[rtac (thm "AnnCond1") i,
+ (rtac (@{thm AnnwaitRule}) i),
+ rtac (@{thm AnnBasic}) i,
+ EVERY[rtac (@{thm AnnCond1}) i,
AnnHoareRuleTac (i+3),
AnnHoareRuleTac (i+1)],
- EVERY[rtac (thm "AnnCond2") i,
+ EVERY[rtac (@{thm AnnCond2}) i,
AnnHoareRuleTac (i+1)],
- EVERY[rtac (thm "AnnWhile") i,
+ EVERY[rtac (@{thm AnnWhile}) i,
AnnHoareRuleTac (i+2)],
- EVERY[rtac (thm "AnnAwait") i,
+ EVERY[rtac (@{thm AnnAwait}) i,
HoareRuleTac true (i+1)],
K all_tac i]))
-and ParallelTac i = EVERY[rtac (thm "ParallelRule") i,
+and ParallelTac i = EVERY[rtac (@{thm ParallelRule}) i,
interfree_Tac (i+1),
MapAnn_Tac i]
and MapAnn_Tac i st = st |>
- (FIRST[rtac (thm "MapAnnEmpty") i,
- EVERY[rtac (thm "MapAnnList") i,
+ (FIRST[rtac (@{thm MapAnnEmpty}) i,
+ EVERY[rtac (@{thm MapAnnList}) i,
MapAnn_Tac (i+1),
AnnHoareRuleTac i],
- EVERY[rtac (thm "MapAnnMap") i,
- rtac (thm "allI") i,rtac (thm "impI") i,
+ EVERY[rtac (@{thm MapAnnMap}) i,
+ rtac (@{thm allI}) i,rtac (@{thm impI}) i,
AnnHoareRuleTac i]])
and interfree_swap_Tac i st = st |>
- (FIRST[rtac (thm "interfree_swap_Empty") i,
- EVERY[rtac (thm "interfree_swap_List") i,
+ (FIRST[rtac (@{thm interfree_swap_Empty}) i,
+ EVERY[rtac (@{thm interfree_swap_List}) i,
interfree_swap_Tac (i+2),
interfree_aux_Tac (i+1),
interfree_aux_Tac i ],
- EVERY[rtac (thm "interfree_swap_Map") i,
- rtac (thm "allI") i,rtac (thm "impI") i,
+ EVERY[rtac (@{thm interfree_swap_Map}) i,
+ rtac (@{thm allI}) i,rtac (@{thm impI}) i,
conjI_Tac (interfree_aux_Tac) i]])
and interfree_Tac i st = st |>
- (FIRST[rtac (thm "interfree_Empty") i,
- EVERY[rtac (thm "interfree_List") i,
+ (FIRST[rtac (@{thm interfree_Empty}) i,
+ EVERY[rtac (@{thm interfree_List}) i,
interfree_Tac (i+1),
interfree_swap_Tac i],
- EVERY[rtac (thm "interfree_Map") i,
- rtac (thm "allI") i,rtac (thm "allI") i,rtac (thm "impI") i,
+ EVERY[rtac (@{thm interfree_Map}) i,
+ rtac (@{thm allI}) i,rtac (@{thm allI}) i,rtac (@{thm impI}) i,
interfree_aux_Tac i ]])
and interfree_aux_Tac i = (before_interfree_simp_tac i ) THEN
- (FIRST[rtac (thm "interfree_aux_rule1") i,
+ (FIRST[rtac (@{thm interfree_aux_rule1}) i,
dest_assertions_Tac i])
and dest_assertions_Tac i st = st |>
- (FIRST[EVERY[rtac (thm "AnnBasic_assertions") i,
+ (FIRST[EVERY[rtac (@{thm AnnBasic_assertions}) i,
dest_atomics_Tac (i+1),
dest_atomics_Tac i],
- EVERY[rtac (thm "AnnSeq_assertions") i,
+ EVERY[rtac (@{thm AnnSeq_assertions}) i,
dest_assertions_Tac (i+1),
dest_assertions_Tac i],
- EVERY[rtac (thm "AnnCond1_assertions") i,
+ EVERY[rtac (@{thm AnnCond1_assertions}) i,
dest_assertions_Tac (i+2),
dest_assertions_Tac (i+1),
dest_atomics_Tac i],
- EVERY[rtac (thm "AnnCond2_assertions") i,
+ EVERY[rtac (@{thm AnnCond2_assertions}) i,
dest_assertions_Tac (i+1),
dest_atomics_Tac i],
- EVERY[rtac (thm "AnnWhile_assertions") i,
+ EVERY[rtac (@{thm AnnWhile_assertions}) i,
dest_assertions_Tac (i+2),
dest_atomics_Tac (i+1),
dest_atomics_Tac i],
- EVERY[rtac (thm "AnnAwait_assertions") i,
+ EVERY[rtac (@{thm AnnAwait_assertions}) i,
dest_atomics_Tac (i+1),
dest_atomics_Tac i],
dest_atomics_Tac i])
and dest_atomics_Tac i st = st |>
- (FIRST[EVERY[rtac (thm "AnnBasic_atomics") i,
+ (FIRST[EVERY[rtac (@{thm AnnBasic_atomics}) i,
HoareRuleTac true i],
- EVERY[rtac (thm "AnnSeq_atomics") i,
+ EVERY[rtac (@{thm AnnSeq_atomics}) i,
dest_atomics_Tac (i+1),
dest_atomics_Tac i],
- EVERY[rtac (thm "AnnCond1_atomics") i,
+ EVERY[rtac (@{thm AnnCond1_atomics}) i,
dest_atomics_Tac (i+1),
dest_atomics_Tac i],
- EVERY[rtac (thm "AnnCond2_atomics") i,
+ EVERY[rtac (@{thm AnnCond2_atomics}) i,
dest_atomics_Tac i],
- EVERY[rtac (thm "AnnWhile_atomics") i,
+ EVERY[rtac (@{thm AnnWhile_atomics}) i,
dest_atomics_Tac i],
- EVERY[rtac (thm "Annatom_atomics") i,
+ EVERY[rtac (@{thm Annatom_atomics}) i,
HoareRuleTac true i],
- EVERY[rtac (thm "AnnAwait_atomics") i,
+ EVERY[rtac (@{thm AnnAwait_atomics}) i,
HoareRuleTac true i],
K all_tac i])
*}
@@ -441,8 +441,8 @@
text {* The final tactic is given the name @{text oghoare}: *}
ML {*
-fun oghoare_tac i thm = SUBGOAL (fn (term, _) =>
- (HoareRuleTac true i)) i thm
+val oghoare_tac = SUBGOAL (fn (_, i) =>
+ (HoareRuleTac true i))
*}
text {* Notice that the tactic for parallel programs @{text
@@ -453,11 +453,11 @@
verification conditions for annotated sequential programs and to
generate verification conditions out of interference freedom tests: *}
-ML {* fun annhoare_tac i thm = SUBGOAL (fn (term, _) =>
- (AnnHoareRuleTac i)) i thm
+ML {* val annhoare_tac = SUBGOAL (fn (_, i) =>
+ (AnnHoareRuleTac i))
-fun interfree_aux_tac i thm = SUBGOAL (fn (term, _) =>
- (interfree_aux_Tac i)) i thm
+val interfree_aux_tac = SUBGOAL (fn (_, i) =>
+ (interfree_aux_Tac i))
*}
text {* The so defined ML tactics are then ``exported'' to be used in
--- a/src/HOL/IMPP/Hoare.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/IMPP/Hoare.thy Sat Jul 21 23:25:00 2007 +0200
@@ -206,7 +206,7 @@
*)
lemma thin [rule_format]: "G'||-ts ==> !G. G' <= G --> G||-ts"
apply (erule hoare_derivs.induct)
-apply (tactic {* ALLGOALS (EVERY'[Clarify_tac, REPEAT o smp_tac 1]) *})
+apply (tactic {* ALLGOALS (EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1]) *})
apply (rule hoare_derivs.empty)
apply (erule (1) hoare_derivs.insert)
apply (fast intro: hoare_derivs.asm)
--- a/src/HOL/MicroJava/J/Example.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/MicroJava/J/Example.thy Sat Jul 21 23:25:00 2007 +0200
@@ -373,7 +373,7 @@
apply (auto simp add: appl_methds_foo_Base)
done
-ML {* fun t thm = resolve_tac (thms "ty_expr_ty_exprs_wt_stmt.intros") 1 thm *}
+ML {* val t = resolve_tac @{thms ty_expr_ty_exprs_wt_stmt.intros} 1 *}
lemma wt_test: "(tprg, empty(e\<mapsto>Class Base))\<turnstile>
Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\<surd>"
apply (tactic t) -- ";;"
@@ -399,7 +399,7 @@
apply (rule max_spec_foo_Base)
done
-ML {* fun e t = resolve_tac (thm "NewCI"::thms "eval_evals_exec.intros") 1 t *}
+ML {* val e = resolve_tac (@{thm NewCI} :: @{thms eval_evals_exec.intros}) 1 *}
declare split_if [split del]
declare init_vars_def [simp] c_hupd_def [simp] cast_ok_def [simp]
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/MicroJava/J/JTypeSafe.thy Sat Jul 21 23:25:00 2007 +0200
@@ -206,7 +206,7 @@
apply( simp_all)
apply( tactic "ALLGOALS strip_tac")
apply( tactic {* ALLGOALS (eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"]
- THEN_ALL_NEW Full_simp_tac) *})
+ THEN_ALL_NEW (full_simp_tac (simpset_of @{theory Conform}))) *})
apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
-- "Level 7"
@@ -246,10 +246,11 @@
-- "for FAss"
apply( tactic {* EVERY'[eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"]
- THEN_ALL_NEW Full_simp_tac, REPEAT o (etac conjE), hyp_subst_tac] 3*})
+ THEN_ALL_NEW (full_simp_tac @{simpset}), REPEAT o (etac conjE), hyp_subst_tac] 3*})
-- "for if"
-apply( tactic {* (case_tac "the_Bool v" THEN_ALL_NEW Asm_full_simp_tac) 7*})
+apply( tactic {* (case_tac "the_Bool v" THEN_ALL_NEW
+ (asm_full_simp_tac @{simpset})) 7*})
apply (tactic "forward_hyp_tac")
@@ -281,7 +282,7 @@
-- "7 LAss"
apply (fold fun_upd_def)
apply( tactic {* (eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"]
- THEN_ALL_NEW Full_simp_tac) 1 *})
+ THEN_ALL_NEW (full_simp_tac @{simpset})) 1 *})
apply (intro strip)
apply (case_tac E)
apply (simp)
--- a/src/HOL/NanoJava/AxSem.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/NanoJava/AxSem.thy Sat Jul 21 23:25:00 2007 +0200
@@ -153,7 +153,7 @@
"(A' |\<turnstile> C \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A |\<turnstile> C )) \<and>
(A' \<turnstile>\<^sub>e {P} e {Q} \<longrightarrow> (\<forall>A. A' \<subseteq> A \<longrightarrow> A \<turnstile>\<^sub>e {P} e {Q}))"
apply (rule hoare_ehoare.induct)
-apply (tactic "ALLGOALS(EVERY'[Clarify_tac, REPEAT o smp_tac 1])")
+apply (tactic "ALLGOALS(EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1])")
apply (blast intro: hoare_ehoare.Skip)
apply (blast intro: hoare_ehoare.Comp)
apply (blast intro: hoare_ehoare.Cond)
--- a/src/HOL/Nominal/nominal_atoms.ML Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Sat Jul 21 23:25:00 2007 +0200
@@ -18,8 +18,8 @@
structure NominalAtoms : NOMINAL_ATOMS =
struct
-val finite_emptyI = thm "finite.emptyI";
-val Collect_const = thm "Collect_const";
+val finite_emptyI = @{thm "finite.emptyI"};
+val Collect_const = @{thm "Collect_const"};
(* theory data *)
@@ -60,6 +60,8 @@
(* atom_decl <ak1> ... <akn> *)
fun create_nom_typedecls ak_names thy =
let
+ val cla_s = claset_of thy;
+
(* declares a type-decl for every atom-kind: *)
(* that is typedecl <ak> *)
val thy1 = TypedefPackage.add_typedecls (map (fn x => (x,[],NoSyn)) ak_names) thy;
@@ -184,7 +186,7 @@
val name = "at_"^ak_name^ "_inst";
val statement = HOLogic.mk_Trueprop (cat $ at_type);
- val proof = fn _ => auto_tac (claset(),simp_s);
+ val proof = fn _ => auto_tac (cla_s,simp_s);
in
((name, Goal.prove_global thy5 [] [] statement proof), [])
@@ -246,7 +248,7 @@
val name = "pt_"^ak_name^ "_inst";
val statement = HOLogic.mk_Trueprop (cpt $ pt_type $ at_type);
- val proof = fn _ => auto_tac (claset(),simp_s);
+ val proof = fn _ => auto_tac (cla_s,simp_s);
in
((name, Goal.prove_global thy7 [] [] statement proof), [])
end) ak_names_types);
@@ -291,7 +293,7 @@
val name = "fs_"^ak_name^ "_inst";
val statement = HOLogic.mk_Trueprop (cfs $ fs_type $ at_type);
- val proof = fn _ => auto_tac (claset(),simp_s);
+ val proof = fn _ => auto_tac (cla_s,simp_s);
in
((name, Goal.prove_global thy11 [] [] statement proof), [])
end) ak_names_types);
@@ -342,7 +344,7 @@
val name = "cp_"^ak_name^ "_"^ak_name'^"_inst";
val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type');
- val proof = fn _ => EVERY [auto_tac (claset(),simp_s), rtac cp1 1];
+ val proof = fn _ => EVERY [auto_tac (cla_s,simp_s), rtac cp1 1];
in
PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy'
end)
@@ -373,7 +375,7 @@
val name = "dj_"^ak_name^"_"^ak_name';
val statement = HOLogic.mk_Trueprop (cdj $ at_type $ at_type');
- val proof = fn _ => auto_tac (claset(),simp_s);
+ val proof = fn _ => auto_tac (cla_s,simp_s);
in
PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy'
end
@@ -384,18 +386,18 @@
(******** pt_<ak> class instances ********)
(*=========================================*)
(* some abbreviations for theorems *)
- val pt1 = thm "pt1";
- val pt2 = thm "pt2";
- val pt3 = thm "pt3";
- val at_pt_inst = thm "at_pt_inst";
- val pt_set_inst = thm "pt_set_inst";
- val pt_unit_inst = thm "pt_unit_inst";
- val pt_prod_inst = thm "pt_prod_inst";
- val pt_nprod_inst = thm "pt_nprod_inst";
- val pt_list_inst = thm "pt_list_inst";
- val pt_optn_inst = thm "pt_option_inst";
- val pt_noptn_inst = thm "pt_noption_inst";
- val pt_fun_inst = thm "pt_fun_inst";
+ val pt1 = @{thm "pt1"};
+ val pt2 = @{thm "pt2"};
+ val pt3 = @{thm "pt3"};
+ val at_pt_inst = @{thm "at_pt_inst"};
+ val pt_set_inst = @{thm "pt_set_inst"};
+ val pt_unit_inst = @{thm "pt_unit_inst"};
+ val pt_prod_inst = @{thm "pt_prod_inst"};
+ val pt_nprod_inst = @{thm "pt_nprod_inst"};
+ val pt_list_inst = @{thm "pt_list_inst"};
+ val pt_optn_inst = @{thm "pt_option_inst"};
+ val pt_noptn_inst = @{thm "pt_noption_inst"};
+ val pt_fun_inst = @{thm "pt_fun_inst"};
(* for all atom-kind combinations <ak>/<ak'> show that *)
(* every <ak> is an instance of pt_<ak'>; the proof for *)
@@ -466,14 +468,14 @@
(******** fs_<ak> class instances ********)
(*=========================================*)
(* abbreviations for some lemmas *)
- val fs1 = thm "fs1";
- val fs_at_inst = thm "fs_at_inst";
- val fs_unit_inst = thm "fs_unit_inst";
- val fs_prod_inst = thm "fs_prod_inst";
- val fs_nprod_inst = thm "fs_nprod_inst";
- val fs_list_inst = thm "fs_list_inst";
- val fs_option_inst = thm "fs_option_inst";
- val dj_supp = thm "dj_supp"
+ val fs1 = @{thm "fs1"};
+ val fs_at_inst = @{thm "fs_at_inst"};
+ val fs_unit_inst = @{thm "fs_unit_inst"};
+ val fs_prod_inst = @{thm "fs_prod_inst"};
+ val fs_nprod_inst = @{thm "fs_nprod_inst"};
+ val fs_list_inst = @{thm "fs_list_inst"};
+ val fs_option_inst = @{thm "fs_option_inst"};
+ val dj_supp = @{thm "dj_supp"};
(* shows that <ak> is an instance of fs_<ak> *)
(* uses the theorem at_<ak>_inst *)
@@ -528,18 +530,18 @@
(******** cp_<ak>_<ai> class instances ********)
(*==============================================*)
(* abbreviations for some lemmas *)
- val cp1 = thm "cp1";
- val cp_unit_inst = thm "cp_unit_inst";
- val cp_bool_inst = thm "cp_bool_inst";
- val cp_prod_inst = thm "cp_prod_inst";
- val cp_list_inst = thm "cp_list_inst";
- val cp_fun_inst = thm "cp_fun_inst";
- val cp_option_inst = thm "cp_option_inst";
- val cp_noption_inst = thm "cp_noption_inst";
- val cp_set_inst = thm "cp_set_inst";
- val pt_perm_compose = thm "pt_perm_compose";
+ val cp1 = @{thm "cp1"};
+ val cp_unit_inst = @{thm "cp_unit_inst"};
+ val cp_bool_inst = @{thm "cp_bool_inst"};
+ val cp_prod_inst = @{thm "cp_prod_inst"};
+ val cp_list_inst = @{thm "cp_list_inst"};
+ val cp_fun_inst = @{thm "cp_fun_inst"};
+ val cp_option_inst = @{thm "cp_option_inst"};
+ val cp_noption_inst = @{thm "cp_noption_inst"};
+ val cp_set_inst = @{thm "cp_set_inst"};
+ val pt_perm_compose = @{thm "pt_perm_compose"};
- val dj_pp_forget = thm "dj_perm_perm_forget";
+ val dj_pp_forget = @{thm "dj_perm_perm_forget"};
(* shows that <aj> is an instance of cp_<ak>_<ai> *)
(* for every <ak>/<ai>-combination *)
@@ -630,7 +632,7 @@
fold (fn ak_name => fn thy =>
let
val qu_class = Sign.full_name thy ("fs_"^ak_name);
- val supp_def = thm "Nominal.supp_def";
+ val supp_def = @{thm "Nominal.supp_def"};
val simp_s = HOL_ss addsimps [supp_def,Collect_const,finite_emptyI,defn];
val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
in
@@ -641,7 +643,7 @@
fold (fn ak_name' => (fold (fn ak_name => fn thy =>
let
val qu_class = Sign.full_name thy ("cp_"^ak_name^"_"^ak_name');
- val supp_def = thm "Nominal.supp_def";
+ val supp_def = @{thm "Nominal.supp_def"};
val simp_s = HOL_ss addsimps [defn];
val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
in
@@ -650,70 +652,70 @@
in
thy26
- |> discrete_pt_inst "nat" (thm "perm_nat_def")
- |> discrete_fs_inst "nat" (thm "perm_nat_def")
- |> discrete_cp_inst "nat" (thm "perm_nat_def")
- |> discrete_pt_inst "bool" (thm "perm_bool")
- |> discrete_fs_inst "bool" (thm "perm_bool")
- |> discrete_cp_inst "bool" (thm "perm_bool")
- |> discrete_pt_inst "IntDef.int" (thm "perm_int_def")
- |> discrete_fs_inst "IntDef.int" (thm "perm_int_def")
- |> discrete_cp_inst "IntDef.int" (thm "perm_int_def")
- |> discrete_pt_inst "List.char" (thm "perm_char_def")
- |> discrete_fs_inst "List.char" (thm "perm_char_def")
- |> discrete_cp_inst "List.char" (thm "perm_char_def")
+ |> discrete_pt_inst "nat" @{thm "perm_nat_def"}
+ |> discrete_fs_inst "nat" @{thm "perm_nat_def"}
+ |> discrete_cp_inst "nat" @{thm "perm_nat_def"}
+ |> discrete_pt_inst "bool" @{thm "perm_bool"}
+ |> discrete_fs_inst "bool" @{thm "perm_bool"}
+ |> discrete_cp_inst "bool" @{thm "perm_bool"}
+ |> discrete_pt_inst "IntDef.int" @{thm "perm_int_def"}
+ |> discrete_fs_inst "IntDef.int" @{thm "perm_int_def"}
+ |> discrete_cp_inst "IntDef.int" @{thm "perm_int_def"}
+ |> discrete_pt_inst "List.char" @{thm "perm_char_def"}
+ |> discrete_fs_inst "List.char" @{thm "perm_char_def"}
+ |> discrete_cp_inst "List.char" @{thm "perm_char_def"}
end;
(* abbreviations for some lemmas *)
(*===============================*)
- val abs_fun_pi = thm "Nominal.abs_fun_pi";
- val abs_fun_pi_ineq = thm "Nominal.abs_fun_pi_ineq";
- val abs_fun_eq = thm "Nominal.abs_fun_eq";
- val abs_fun_eq' = thm "Nominal.abs_fun_eq'";
- val abs_fun_fresh = thm "Nominal.abs_fun_fresh";
- val abs_fun_fresh' = thm "Nominal.abs_fun_fresh'";
- val dj_perm_forget = thm "Nominal.dj_perm_forget";
- val dj_pp_forget = thm "Nominal.dj_perm_perm_forget";
- val fresh_iff = thm "Nominal.fresh_abs_fun_iff";
- val fresh_iff_ineq = thm "Nominal.fresh_abs_fun_iff_ineq";
- val abs_fun_supp = thm "Nominal.abs_fun_supp";
- val abs_fun_supp_ineq = thm "Nominal.abs_fun_supp_ineq";
- val pt_swap_bij = thm "Nominal.pt_swap_bij";
- val pt_swap_bij' = thm "Nominal.pt_swap_bij'";
- val pt_fresh_fresh = thm "Nominal.pt_fresh_fresh";
- val pt_bij = thm "Nominal.pt_bij";
- val pt_perm_compose = thm "Nominal.pt_perm_compose";
- val pt_perm_compose' = thm "Nominal.pt_perm_compose'";
- val perm_app = thm "Nominal.pt_fun_app_eq";
- val at_fresh = thm "Nominal.at_fresh";
- val at_fresh_ineq = thm "Nominal.at_fresh_ineq";
- val at_calc = thms "Nominal.at_calc";
- val at_swap_simps = thms "Nominal.at_swap_simps";
- val at_supp = thm "Nominal.at_supp";
- val dj_supp = thm "Nominal.dj_supp";
- val fresh_left_ineq = thm "Nominal.pt_fresh_left_ineq";
- val fresh_left = thm "Nominal.pt_fresh_left";
- val fresh_right_ineq = thm "Nominal.pt_fresh_right_ineq";
- val fresh_right = thm "Nominal.pt_fresh_right";
- val fresh_bij_ineq = thm "Nominal.pt_fresh_bij_ineq";
- val fresh_bij = thm "Nominal.pt_fresh_bij";
- val fresh_eqvt = thm "Nominal.pt_fresh_eqvt";
- val fresh_eqvt_ineq = thm "Nominal.pt_fresh_eqvt_ineq";
- val set_diff_eqvt = thm "Nominal.pt_set_diff_eqvt";
- val in_eqvt = thm "Nominal.pt_in_eqvt";
- val eq_eqvt = thm "Nominal.pt_eq_eqvt";
- val all_eqvt = thm "Nominal.pt_all_eqvt";
- val ex_eqvt = thm "Nominal.pt_ex_eqvt";
- val pt_pi_rev = thm "Nominal.pt_pi_rev";
- val pt_rev_pi = thm "Nominal.pt_rev_pi";
- val at_exists_fresh = thm "Nominal.at_exists_fresh";
- val at_exists_fresh' = thm "Nominal.at_exists_fresh'";
- val fresh_perm_app_ineq = thm "Nominal.pt_fresh_perm_app_ineq";
- val fresh_perm_app = thm "Nominal.pt_fresh_perm_app";
- val fresh_aux = thm "Nominal.pt_fresh_aux";
- val pt_perm_supp_ineq = thm "Nominal.pt_perm_supp_ineq";
- val pt_perm_supp = thm "Nominal.pt_perm_supp";
+ val abs_fun_pi = @{thm "Nominal.abs_fun_pi"};
+ val abs_fun_pi_ineq = @{thm "Nominal.abs_fun_pi_ineq"};
+ val abs_fun_eq = @{thm "Nominal.abs_fun_eq"};
+ val abs_fun_eq' = @{thm "Nominal.abs_fun_eq'"};
+ val abs_fun_fresh = @{thm "Nominal.abs_fun_fresh"};
+ val abs_fun_fresh' = @{thm "Nominal.abs_fun_fresh'"};
+ val dj_perm_forget = @{thm "Nominal.dj_perm_forget"};
+ val dj_pp_forget = @{thm "Nominal.dj_perm_perm_forget"};
+ val fresh_iff = @{thm "Nominal.fresh_abs_fun_iff"};
+ val fresh_iff_ineq = @{thm "Nominal.fresh_abs_fun_iff_ineq"};
+ val abs_fun_supp = @{thm "Nominal.abs_fun_supp"};
+ val abs_fun_supp_ineq = @{thm "Nominal.abs_fun_supp_ineq"};
+ val pt_swap_bij = @{thm "Nominal.pt_swap_bij"};
+ val pt_swap_bij' = @{thm "Nominal.pt_swap_bij'"};
+ val pt_fresh_fresh = @{thm "Nominal.pt_fresh_fresh"};
+ val pt_bij = @{thm "Nominal.pt_bij"};
+ val pt_perm_compose = @{thm "Nominal.pt_perm_compose"};
+ val pt_perm_compose' = @{thm "Nominal.pt_perm_compose'"};
+ val perm_app = @{thm "Nominal.pt_fun_app_eq"};
+ val at_fresh = @{thm "Nominal.at_fresh"};
+ val at_fresh_ineq = @{thm "Nominal.at_fresh_ineq"};
+ val at_calc = @{thms "Nominal.at_calc"};
+ val at_swap_simps = @{thms "Nominal.at_swap_simps"};
+ val at_supp = @{thm "Nominal.at_supp"};
+ val dj_supp = @{thm "Nominal.dj_supp"};
+ val fresh_left_ineq = @{thm "Nominal.pt_fresh_left_ineq"};
+ val fresh_left = @{thm "Nominal.pt_fresh_left"};
+ val fresh_right_ineq = @{thm "Nominal.pt_fresh_right_ineq"};
+ val fresh_right = @{thm "Nominal.pt_fresh_right"};
+ val fresh_bij_ineq = @{thm "Nominal.pt_fresh_bij_ineq"};
+ val fresh_bij = @{thm "Nominal.pt_fresh_bij"};
+ val fresh_eqvt = @{thm "Nominal.pt_fresh_eqvt"};
+ val fresh_eqvt_ineq = @{thm "Nominal.pt_fresh_eqvt_ineq"};
+ val set_diff_eqvt = @{thm "Nominal.pt_set_diff_eqvt"};
+ val in_eqvt = @{thm "Nominal.pt_in_eqvt"};
+ val eq_eqvt = @{thm "Nominal.pt_eq_eqvt"};
+ val all_eqvt = @{thm "Nominal.pt_all_eqvt"};
+ val ex_eqvt = @{thm "Nominal.pt_ex_eqvt"};
+ val pt_pi_rev = @{thm "Nominal.pt_pi_rev"};
+ val pt_rev_pi = @{thm "Nominal.pt_rev_pi"};
+ val at_exists_fresh = @{thm "Nominal.at_exists_fresh"};
+ val at_exists_fresh' = @{thm "Nominal.at_exists_fresh'"};
+ val fresh_perm_app_ineq = @{thm "Nominal.pt_fresh_perm_app_ineq"};
+ val fresh_perm_app = @{thm "Nominal.pt_fresh_perm_app"};
+ val fresh_aux = @{thm "Nominal.pt_fresh_aux"};
+ val pt_perm_supp_ineq = @{thm "Nominal.pt_perm_supp_ineq"};
+ val pt_perm_supp = @{thm "Nominal.pt_perm_supp"};
(* Now we collect and instantiate some lemmas w.r.t. all atom *)
(* types; this allows for example to use abs_perm (which is a *)
--- a/src/HOL/NumberTheory/Chinese.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/NumberTheory/Chinese.thy Sat Jul 21 23:25:00 2007 +0200
@@ -246,7 +246,7 @@
prefer 7
apply (simp add: zmult_ac)
apply (unfold xilin_sol_def)
- apply (tactic {* Asm_simp_tac 7 *})
+ apply (tactic {* asm_simp_tac @{simpset} 7 *})
apply (rule_tac [7] ex1_implies_ex [THEN someI_ex])
apply (rule_tac [7] unique_xi_sol)
apply (rule_tac [4] funprod_zdvd)
--- a/src/HOL/NumberTheory/WilsonBij.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/NumberTheory/WilsonBij.thy Sat Jul 21 23:25:00 2007 +0200
@@ -150,7 +150,7 @@
apply (rule_tac [7] zcong_trans)
apply (tactic {* stac (thm "zcong_sym") 8 *})
apply (erule_tac [7] inv_is_inv)
- apply (tactic "Asm_simp_tac 9")
+ apply (tactic "asm_simp_tac @{simpset} 9")
apply (erule_tac [9] inv_is_inv)
apply (rule_tac [6] zless_zprime_imp_zrelprime)
apply (rule_tac [8] inv_less)
--- a/src/HOL/NumberTheory/WilsonRuss.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/NumberTheory/WilsonRuss.thy Sat Jul 21 23:25:00 2007 +0200
@@ -270,7 +270,7 @@
apply (simp add: zmult_assoc)
apply (rule_tac [5] zcong_zmult)
apply (rule_tac [5] inv_is_inv)
- apply (tactic "Clarify_tac 4")
+ apply (tactic "clarify_tac @{claset} 4")
apply (subgoal_tac [4] "a \<in> wset (a - 1, p)")
apply (rule_tac [5] wset_inv_mem_mem)
apply (simp_all add: wset_fin)
--- a/src/HOL/ROOT.ML Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/ROOT.ML Sat Jul 21 23:25:00 2007 +0200
@@ -7,5 +7,3 @@
use_thy "Main";
path_add "~~/src/HOL/Library";
-
-Goal "True"; (*leave subgoal package empty*)
--- a/src/HOL/Tools/meson.ML Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOL/Tools/meson.ML Sat Jul 21 23:25:00 2007 +0200
@@ -575,7 +575,7 @@
(*First, breaks the goal into independent units*)
val safe_best_meson_tac =
- SELECT_GOAL (TRY Safe_tac THEN
+ SELECT_GOAL (TRY (CLASET safe_tac) THEN
TRYALL (best_meson_tac size_of_subgoals));
(** Depth-first search version **)
--- a/src/HOLCF/Tools/domain/domain_theorems.ML Sat Jul 21 17:40:40 2007 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML Sat Jul 21 23:25:00 2007 +0200
@@ -195,7 +195,7 @@
val conj = foldr1 mk_conj (eqn :: map (defined o %:) (nonlazy args));
in Library.foldr mk_ex (vns, conj) end;
- val conj_assoc = thm "conj_assoc";
+ val conj_assoc = @{thm conj_assoc};
val exh = foldr1 mk_disj ((%:x_name === UU) :: map one_con cons);
val thm1 = instantiate' [SOME (cons2ctyp cons)] [] exh_start;
val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1;
@@ -333,7 +333,7 @@
end;
local
- val rev_contrapos = thm "rev_contrapos";
+ val rev_contrapos = @{thm rev_contrapos};
fun con_strict (con, args) =
let
fun one_strict vn =
@@ -441,7 +441,7 @@
end;
val sel_rews = sel_stricts @ sel_defins @ sel_apps;
-val rev_contrapos = thm "rev_contrapos";
+val rev_contrapos = @{thm rev_contrapos};
val distincts_le =
let
--- a/src/ZF/ROOT.ML Sat Jul 21 17:40:40 2007 +0200
+++ b/src/ZF/ROOT.ML Sat Jul 21 23:25:00 2007 +0200
@@ -12,5 +12,3 @@
writeln banner;
use_thy "Main_ZFC";
-
-Goal "True"; (*leave subgoal package empty*)
--- a/src/ZF/UNITY/Constrains.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/ZF/UNITY/Constrains.thy Sat Jul 21 23:25:00 2007 +0200
@@ -537,7 +537,8 @@
(*proves "co" properties when the program is specified*)
-fun gen_constrains_tac(cs,ss) i =
+fun constrains_tac ctxt =
+ let val css as (cs, ss) = local_clasimpset_of ctxt in
SELECT_GOAL
(EVERY [REPEAT (Always_Int_tac 1),
REPEAT (etac Always_ConstrainsI 1
@@ -547,27 +548,30 @@
rtac constrainsI 1,
(* Three subgoals *)
rewrite_goal_tac [st_set_def] 3,
- REPEAT (Force_tac 2),
+ REPEAT (force_tac css 2),
full_simp_tac (ss addsimps !program_defs_ref) 1,
ALLGOALS (clarify_tac cs),
REPEAT (FIRSTGOAL (etac disjE)),
- ALLGOALS Clarify_tac,
+ ALLGOALS (clarify_tac cs),
REPEAT (FIRSTGOAL (etac disjE)),
ALLGOALS (clarify_tac cs),
ALLGOALS (asm_full_simp_tac ss),
- ALLGOALS (clarify_tac cs)]) i;
-
-fun constrains_tac st = gen_constrains_tac (claset(), simpset()) st;
+ ALLGOALS (clarify_tac cs)])
+ end;
(*For proving invariants*)
-fun always_tac i =
- rtac AlwaysI i THEN Force_tac i THEN constrains_tac i;
+fun always_tac ctxt i =
+ rtac AlwaysI i THEN force_tac (local_clasimpset_of ctxt) i THEN constrains_tac ctxt i;
*}
method_setup safety = {*
Method.ctxt_args (fn ctxt =>
- Method.SIMPLE_METHOD' (gen_constrains_tac (local_clasimpset_of ctxt))) *}
+ Method.SIMPLE_METHOD' (constrains_tac ctxt)) *}
"for proving safety properties"
+method_setup always = {*
+ Method.ctxt_args (fn ctxt =>
+ Method.SIMPLE_METHOD' (always_tac ctxt)) *}
+ "for proving invariants"
end
--- a/src/ZF/UNITY/SubstAx.thy Sat Jul 21 17:40:40 2007 +0200
+++ b/src/ZF/UNITY/SubstAx.thy Sat Jul 21 23:25:00 2007 +0200
@@ -403,7 +403,8 @@
(*proves "ensures/leadsTo" properties when the program is specified*)
-fun gen_ensures_tac(cs,ss) sact =
+fun ensures_tac ctxt sact =
+ let val css as (cs, ss) = local_clasimpset_of ctxt in
SELECT_GOAL
(EVERY [REPEAT (Always_Int_tac 1),
etac Always_LeadsTo_Basis 1
@@ -416,26 +417,22 @@
(*simplify the command's domain*)
simp_tac (ss addsimps [domain_def]) 3,
(* proving the domain part *)
- clarify_tac cs 3, dtac Cla.swap 3, force_tac (cs,ss) 4,
- rtac ReplaceI 3, force_tac (cs,ss) 3, force_tac (cs,ss) 4,
+ clarify_tac cs 3, dtac Cla.swap 3, force_tac css 4,
+ rtac ReplaceI 3, force_tac css 3, force_tac css 4,
asm_full_simp_tac ss 3, rtac conjI 3, simp_tac ss 4,
REPEAT (rtac state_update_type 3),
- gen_constrains_tac (cs,ss) 1,
+ constrains_tac ctxt 1,
ALLGOALS (clarify_tac cs),
ALLGOALS (asm_full_simp_tac (ss addsimps [st_set_def])),
ALLGOALS (clarify_tac cs),
- ALLGOALS (asm_lr_simp_tac ss)]);
-
-fun ensures_tac sact = gen_ensures_tac (claset(), simpset()) sact;
+ ALLGOALS (asm_lr_simp_tac ss)])
+ end;
*}
-
method_setup ensures_tac = {*
fn args => fn ctxt =>
- Method.goal_args' (Scan.lift Args.name)
- (gen_ensures_tac (local_clasimpset_of ctxt))
+ Method.goal_args' (Scan.lift Args.name) (ensures_tac ctxt)
args ctxt *}
"for proving progress properties"
-
end