# HG changeset patch # User wenzelm # Date 1185053100 -7200 # Node ID 1a4167d761ac251efd7b8e246219700b1f4a190d # Parent 8babfcaaf12945fa27ed8fabce38e81ac8b41bca tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.); diff -r 8babfcaaf129 -r 1a4167d761ac src/CCL/Type.thy --- 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 @@ "[| : lfp(%x. EQgen(x) Un R Un EQ); : lfp(%x. EQgen(x) Un R Un EQ) |] ==> : 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 : EQgen(R) using rews and *) (* then reduce this to a goal : 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 *} diff -r 8babfcaaf129 -r 1a4167d761ac src/CCL/ex/Flag.thy --- 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)"); *} diff -r 8babfcaaf129 -r 1a4167d761ac src/CCL/ex/Stream.thy --- 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= & (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 diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/Algebra/abstract/Ideal2.thy --- 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) diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/Algebra/abstract/Ring2.thy --- 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 diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/Auth/Public.thy --- 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 diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/Auth/Recur.thy --- 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 diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/Auth/Shared.thy --- 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 \ 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 diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/Auth/Smartcard/ShoupRubin.thy --- 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 - diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/Auth/Smartcard/ShoupRubinBella.thy --- 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" diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/Auth/Smartcard/Smartcard.thy --- 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 \ 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 \ 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 diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/Bali/AxCompl.thy --- 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) diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/Bali/AxSem.thy --- 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)|\(ts::'a triple set) \ \A. A' \ A \ G,A|\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) diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/HoareParallel/Gar_Coll.thy --- 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) diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/HoareParallel/Mul_Gar_Coll.thy --- 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) *}) diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/HoareParallel/OG_Examples.thy --- 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 @@ .{ \kb ! 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 @@ .{\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) diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/HoareParallel/OG_Tactics.thy --- 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 diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/IMPP/Hoare.thy --- 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) diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/MicroJava/J/Example.thy --- 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\Class Base))\ Expr(e::=NewC Ext);; Expr({Base}LAcc e..foo({?pTs'}[Lit Null]))\" 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] diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/MicroJava/J/JTypeSafe.thy --- 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) diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/NanoJava/AxSem.thy --- 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' |\ C \ (\A. A' \ A \ A |\ C )) \ (A' \\<^sub>e {P} e {Q} \ (\A. A' \ A \ A \\<^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) diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/Nominal/nominal_atoms.ML --- 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 ... *) 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 *) 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_ 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 / show that *) (* every is an instance of pt_; the proof for *) @@ -466,14 +468,14 @@ (******** fs_ 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 is an instance of fs_ *) (* uses the theorem at__inst *) @@ -528,18 +530,18 @@ (******** cp__ 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 is an instance of cp__ *) (* for every /-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 *) diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/NumberTheory/Chinese.thy --- 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) diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/NumberTheory/WilsonBij.thy --- 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) diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/NumberTheory/WilsonRuss.thy --- 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 \ wset (a - 1, p)") apply (rule_tac [5] wset_inv_mem_mem) apply (simp_all add: wset_fin) diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/ROOT.ML --- 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*) diff -r 8babfcaaf129 -r 1a4167d761ac src/HOL/Tools/meson.ML --- 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 **) diff -r 8babfcaaf129 -r 1a4167d761ac src/HOLCF/Tools/domain/domain_theorems.ML --- 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 diff -r 8babfcaaf129 -r 1a4167d761ac src/ZF/ROOT.ML --- 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*) diff -r 8babfcaaf129 -r 1a4167d761ac src/ZF/UNITY/Constrains.thy --- 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 diff -r 8babfcaaf129 -r 1a4167d761ac src/ZF/UNITY/SubstAx.thy --- 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