# HG changeset patch # User wenzelm # Date 1437245696 -7200 # Node ID 02924903a6fd21f514b94a79a515e3aa883eb67e # Parent 80ca4a065a48d732d7e783806af4f741b62ab527 prefer tactics with explicit context; diff -r 80ca4a065a48 -r 02924903a6fd src/CCL/CCL.thy --- a/src/CCL/CCL.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/CCL/CCL.thy Sat Jul 18 20:54:56 2015 +0200 @@ -268,7 +268,7 @@ let fun mk_raw_dstnct_thm rls s = Goal.prove_global @{theory} [] [] (Syntax.read_prop_global @{theory} s) - (fn {context = ctxt, ...} => rtac @{thm notI} 1 THEN eresolve_tac ctxt rls 1) + (fn {context = ctxt, ...} => resolve_tac ctxt @{thms notI} 1 THEN eresolve_tac ctxt rls 1) in map (mk_raw_dstnct_thm caseB_lemmas) (mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end diff -r 80ca4a065a48 -r 02924903a6fd src/CCL/Type.thy --- a/src/CCL/Type.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/CCL/Type.thy Sat Jul 18 20:54:56 2015 +0200 @@ -398,7 +398,7 @@ ML {* fun genIs_tac ctxt genXH gen_mono = - rtac (genXH RS @{thm iffD2}) THEN' + resolve_tac ctxt [genXH RS @{thm iffD2}] THEN' simp_tac ctxt THEN' TRY o fast_tac (ctxt addIs [genXH RS @{thm iffD2}, gen_mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}]) @@ -436,7 +436,7 @@ ML {* fun POgen_tac ctxt (rla, rlb) i = SELECT_GOAL (safe_tac ctxt) i THEN - rtac (rlb RS (rla RS @{thm ssubst_pair})) i THEN + resolve_tac ctxt [rlb RS (rla RS @{thm ssubst_pair})] i THEN (REPEAT (resolve_tac ctxt (@{thms POgenIs} @ [@{thm PO_refl} RS (@{thm POgen_mono} RS @{thm ci3_AI})] @ (@{thms POgenIs} RL [@{thm POgen_mono} RS @{thm ci3_AgenI}]) @ diff -r 80ca4a065a48 -r 02924903a6fd src/CCL/Wfd.thy --- a/src/CCL/Wfd.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/CCL/Wfd.thy Sat Jul 18 20:54:56 2015 +0200 @@ -448,7 +448,7 @@ in fun rcall_tac ctxt i = - let fun tac ps rl i = Rule_Insts.res_inst_tac ctxt ps [] rl i THEN atac i + let fun tac ps rl i = Rule_Insts.res_inst_tac ctxt ps [] rl i THEN assume_tac ctxt i in IHinst tac @{thms rcallTs} i end THEN eresolve_tac ctxt @{thms rcall_lemmas} i @@ -468,7 +468,7 @@ (*** Clean up Correctness Condictions ***) fun clean_ccs_tac ctxt = - let fun tac ps rl i = Rule_Insts.eres_inst_tac ctxt ps [] rl i THEN atac i in + let fun tac ps rl i = Rule_Insts.eres_inst_tac ctxt ps [] rl i THEN assume_tac ctxt i in TRY (REPEAT_FIRST (IHinst tac @{thms hyprcallTs} ORELSE' eresolve_tac ctxt ([asm_rl, @{thm SubtypeE}] @ @{thms rmIHs}) ORELSE' hyp_subst_tac ctxt)) @@ -525,7 +525,7 @@ apply (rule 1 [THEN canonical]) apply (tactic {* REPEAT (DEPTH_SOLVE_1 (resolve_tac @{context} (@{thms assms} @ @{thms eval_rls}) 1 ORELSE - etac @{thm substitute} 1)) *}) + eresolve_tac @{context} @{thms substitute} 1)) *}) done lemma fixV: "f(fix(f)) ---> c \ fix(f) ---> c" diff -r 80ca4a065a48 -r 02924903a6fd src/CCL/ex/Stream.thy --- a/src/CCL/ex/Stream.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/CCL/ex/Stream.thy Sat Jul 18 20:54:56 2015 +0200 @@ -82,7 +82,7 @@ apply EQgen prefer 2 apply blast - apply (tactic {* DEPTH_SOLVE (etac (XH_to_E @{thm ListsXH}) 1 + apply (tactic {* DEPTH_SOLVE (eresolve_tac @{context} [XH_to_E @{thm ListsXH}] 1 THEN EQgen_tac @{context} [] 1) *}) done diff -r 80ca4a065a48 -r 02924903a6fd src/CTT/CTT.thy --- a/src/CTT/CTT.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/CTT/CTT.thy Sat Jul 18 20:54:56 2015 +0200 @@ -421,25 +421,25 @@ The (rtac EqE i) lets them apply to equality judgements. **) fun NE_tac ctxt sp i = - TRY (rtac @{thm EqE} i) THEN + TRY (resolve_tac ctxt @{thms EqE} i) THEN Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] [] @{thm NE} i fun SumE_tac ctxt sp i = - TRY (rtac @{thm EqE} i) THEN + TRY (resolve_tac ctxt @{thms EqE} i) THEN Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] [] @{thm SumE} i fun PlusE_tac ctxt sp i = - TRY (rtac @{thm EqE} i) THEN + TRY (resolve_tac ctxt @{thms EqE} i) THEN Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), sp)] [] @{thm PlusE} i (** Predicate logic reasoning, WITH THINNING!! Procedures adapted from NJ. **) (*Finds f:Prod(A,B) and a:A in the assumptions, concludes there is z:B(a) *) fun add_mp_tac ctxt i = - rtac @{thm subst_prodE} i THEN assume_tac ctxt i THEN assume_tac ctxt i + resolve_tac ctxt @{thms subst_prodE} i THEN assume_tac ctxt i THEN assume_tac ctxt i (*Finds P-->Q and P in the assumptions, replaces implication by Q *) -fun mp_tac ctxt i = etac @{thm subst_prodE} i THEN assume_tac ctxt i +fun mp_tac ctxt i = eresolve_tac ctxt @{thms subst_prodE} i THEN assume_tac ctxt i (*"safe" when regarded as predicate calculus rules*) val safe_brls = sort (make_ord lessb) diff -r 80ca4a065a48 -r 02924903a6fd src/Doc/Codegen/Evaluation.thy --- a/src/Doc/Codegen/Evaluation.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/Doc/Codegen/Evaluation.thy Sat Jul 18 20:54:56 2015 +0200 @@ -232,7 +232,7 @@ ML_prf (*>*) \val thm = Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \ x < z"}\ (*<*) -by (tactic \ALLGOALS (rtac thm)\) +by (tactic \ALLGOALS (resolve_tac @{context} [thm])\) (*>*) text \ diff -r 80ca4a065a48 -r 02924903a6fd src/Doc/Implementation/Isar.thy --- a/src/Doc/Implementation/Isar.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/Doc/Implementation/Isar.thy Sat Jul 18 20:54:56 2015 +0200 @@ -365,7 +365,7 @@ assume a: A and b: B have "A \ B" - apply (tactic \rtac @{thm conjI} 1\) + apply (tactic \resolve_tac @{context} @{thms conjI} 1\) using a apply (tactic \resolve_tac @{context} facts 1\) using b apply (tactic \resolve_tac @{context} facts 1\) done @@ -374,7 +374,7 @@ using a and b ML_val \@{Isar.goal}\ apply (tactic \Method.insert_tac facts 1\) - apply (tactic \(rtac @{thm conjI} THEN_ALL_NEW atac) 1\) + apply (tactic \(resolve_tac @{context} @{thms conjI} THEN_ALL_NEW assume_tac @{context}) 1\) done end diff -r 80ca4a065a48 -r 02924903a6fd src/Doc/Implementation/Proof.thy --- a/src/Doc/Implementation/Proof.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/Doc/Implementation/Proof.thy Sat Jul 18 20:54:56 2015 +0200 @@ -492,7 +492,7 @@ ML_prf %"ML" \val ctxt0 = @{context}; val (([(_, x)], [B]), ctxt1) = ctxt0 - |> Obtain.result (fn _ => etac @{thm exE} 1) [@{thm ex}];\ + |> Obtain.result (fn _ => eresolve_tac ctxt0 @{thms exE} 1) [@{thm ex}];\ ML_prf %"ML" \singleton (Proof_Context.export ctxt1 ctxt0) @{thm refl};\ ML_prf %"ML" diff -r 80ca4a065a48 -r 02924903a6fd src/Doc/Tutorial/Protocol/Event.thy --- a/src/Doc/Tutorial/Protocol/Event.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/Doc/Tutorial/Protocol/Event.thy Sat Jul 18 20:54:56 2015 +0200 @@ -261,7 +261,7 @@ ML {* fun analz_mono_contra_tac ctxt = - rtac @{thm analz_impI} THEN' + resolve_tac ctxt @{thms analz_impI} THEN' REPEAT1 o (dresolve_tac ctxt @{thms analz_mono_contra}) THEN' mp_tac ctxt *} @@ -331,7 +331,7 @@ fun synth_analz_mono_contra_tac ctxt = - rtac @{thm syan_impI} THEN' + resolve_tac ctxt @{thms syan_impI} THEN' REPEAT1 o (dresolve_tac ctxt [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}, diff -r 80ca4a065a48 -r 02924903a6fd src/FOLP/FOLP.thy --- a/src/FOLP/FOLP.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/FOLP/FOLP.thy Sat Jul 18 20:54:56 2015 +0200 @@ -56,7 +56,7 @@ and r2: "!!y. y:Q ==> g(y):R" shows "?p : R" apply (rule excluded_middle [THEN disjE]) - apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE + apply (tactic {* DEPTH_SOLVE (assume_tac @{context} 1 ORELSE resolve_tac @{context} [@{thm r1}, @{thm r2}, @{thm major} RS @{thm mp}] 1) *}) done @@ -80,8 +80,9 @@ apply (insert major) apply (unfold iff_def) apply (rule conjE) - apply (tactic {* DEPTH_SOLVE_1 (etac @{thm impCE} 1 ORELSE - eresolve_tac @{context} [@{thm notE}, @{thm impE}] 1 THEN atac 1 ORELSE atac 1 ORELSE + apply (tactic {* DEPTH_SOLVE_1 (eresolve_tac @{context} @{thms impCE} 1 ORELSE + eresolve_tac @{context} [@{thm notE}, @{thm impE}] 1 THEN assume_tac @{context} 1 ORELSE + assume_tac @{context} 1 ORELSE resolve_tac @{context} [@{thm r1}, @{thm r2}] 1) *})+ done @@ -107,7 +108,7 @@ val mp = @{thm mp} val not_elim = @{thm notE} val swap = @{thm swap} - val hyp_subst_tacs = [hyp_subst_tac] + fun hyp_subst_tacs ctxt = [hyp_subst_tac ctxt] ); open Cla; diff -r 80ca4a065a48 -r 02924903a6fd src/FOLP/IFOLP.thy --- a/src/FOLP/IFOLP.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/FOLP/IFOLP.thy Sat Jul 18 20:54:56 2015 +0200 @@ -504,19 +504,19 @@ schematic_lemma pred1_cong: "p:a=a' ==> ?p:P(a) <-> P(a')" apply (rule iffI) apply (tactic {* - DEPTH_SOLVE (atac 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1) *}) + DEPTH_SOLVE (assume_tac @{context} 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1) *}) done schematic_lemma pred2_cong: "[| p:a=a'; q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')" apply (rule iffI) apply (tactic {* - DEPTH_SOLVE (atac 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1) *}) + DEPTH_SOLVE (assume_tac @{context} 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1) *}) done schematic_lemma pred3_cong: "[| p:a=a'; q:b=b'; r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')" apply (rule iffI) apply (tactic {* - DEPTH_SOLVE (atac 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1) *}) + DEPTH_SOLVE (assume_tac @{context} 1 ORELSE eresolve_tac @{context} [@{thm subst}, @{thm ssubst}] 1) *}) done lemmas pred_congs = pred1_cong pred2_cong pred3_cong @@ -543,7 +543,7 @@ assumes major: "p:(P|Q)-->S" and minor: "!!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R" shows "?p:R" - apply (tactic {* DEPTH_SOLVE (atac 1 ORELSE + apply (tactic {* DEPTH_SOLVE (assume_tac @{context} 1 ORELSE resolve_tac @{context} [@{thm disjI1}, @{thm disjI2}, @{thm impI}, @{thm major} RS @{thm mp}, @{thm minor}] 1) *}) done diff -r 80ca4a065a48 -r 02924903a6fd src/FOLP/classical.ML --- a/src/FOLP/classical.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/FOLP/classical.ML Sat Jul 18 20:54:56 2015 +0200 @@ -22,7 +22,7 @@ val not_elim: thm (* [| ~P; P |] ==> R *) val swap: thm (* ~P ==> (~Q ==> P) ==> Q *) val sizef : thm -> int (* size function for BEST_FIRST *) - val hyp_subst_tacs: (int -> tactic) list + val hyp_subst_tacs: Proof.context -> (int -> tactic) list end; (*Higher precedence than := facilitates use of references*) @@ -70,7 +70,7 @@ val imp_elim = make_elim mp; (*Solve goal that assumes both P and ~P. *) -fun contr_tac ctxt = etac not_elim THEN' assume_tac ctxt; +fun contr_tac ctxt = eresolve_tac ctxt [not_elim] THEN' assume_tac ctxt; (*Finds P-->Q and P in the assumptions, replaces implication by Q *) fun mp_tac ctxt i = eresolve_tac ctxt ([not_elim,imp_elim]) i THEN assume_tac ctxt i; @@ -84,7 +84,7 @@ (*Uses introduction rules in the normal way, or on negated assumptions, trying rules in order. *) fun swap_res_tac ctxt rls = - let fun tacf rl = rtac rl ORELSE' etac (rl RSN (2,swap)) + let fun tacf rl = resolve_tac ctxt [rl] ORELSE' eresolve_tac ctxt [rl RSN (2, swap)] in assume_tac ctxt ORELSE' contr_tac ctxt ORELSE' FIRST' (map tacf rls) end; @@ -152,7 +152,7 @@ FIRST' [uniq_assume_tac ctxt, uniq_mp_tac ctxt, biresolve_tac ctxt safe0_brls, - FIRST' hyp_subst_tacs, + FIRST' (hyp_subst_tacs ctxt), biresolve_tac ctxt safep_brls] ; (*Repeatedly attack subgoals using safe inferences*) diff -r 80ca4a065a48 -r 02924903a6fd src/FOLP/hypsubst.ML --- a/src/FOLP/hypsubst.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/FOLP/hypsubst.ML Sat Jul 18 20:54:56 2015 +0200 @@ -19,8 +19,8 @@ signature HYPSUBST = sig - val bound_hyp_subst_tac : int -> tactic - val hyp_subst_tac : int -> tactic + val bound_hyp_subst_tac : Proof.context -> int -> tactic + val hyp_subst_tac : Proof.context -> int -> tactic (*exported purely for debugging purposes*) val eq_var : bool -> term -> int * thm val inspect_pair : bool -> term * term -> thm @@ -68,16 +68,16 @@ (*Select a suitable equality assumption and substitute throughout the subgoal Replaces only Bound variables if bnd is true*) -fun gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) => +fun gen_hyp_subst_tac bnd ctxt = SUBGOAL(fn (Bi,i) => let val n = length(Logic.strip_assums_hyp Bi) - 1 val (k,symopt) = eq_var bnd Bi in DETERM - (EVERY [REPEAT_DETERM_N k (etac rev_mp i), - etac revcut_rl i, - REPEAT_DETERM_N (n-k) (etac rev_mp i), - etac (symopt RS subst) i, - REPEAT_DETERM_N n (rtac imp_intr i)]) + (EVERY [REPEAT_DETERM_N k (eresolve_tac ctxt [rev_mp] i), + eresolve_tac ctxt [revcut_rl] i, + REPEAT_DETERM_N (n-k) (eresolve_tac ctxt [rev_mp] i), + eresolve_tac ctxt [symopt RS subst] i, + REPEAT_DETERM_N n (resolve_tac ctxt [imp_intr] i)]) end handle THM _ => no_tac | EQ_VAR => no_tac); diff -r 80ca4a065a48 -r 02924903a6fd src/FOLP/intprover.ML --- a/src/FOLP/intprover.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/FOLP/intprover.ML Sat Jul 18 20:54:56 2015 +0200 @@ -55,7 +55,7 @@ fun safe_step_tac ctxt = FIRST' [uniq_assume_tac ctxt, int_uniq_mp_tac ctxt, biresolve_tac ctxt safe0_brls, - hyp_subst_tac, + hyp_subst_tac ctxt, biresolve_tac ctxt safep_brls] ; (*Repeatedly attack subgoals using safe inferences*) diff -r 80ca4a065a48 -r 02924903a6fd src/FOLP/simp.ML --- a/src/FOLP/simp.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/FOLP/simp.ML Sat Jul 18 20:54:56 2015 +0200 @@ -39,7 +39,7 @@ val setauto : simpset * (int -> tactic) -> simpset val ASM_SIMP_CASE_TAC : Proof.context -> simpset -> int -> tactic val ASM_SIMP_TAC : Proof.context -> simpset -> int -> tactic - val CASE_TAC : simpset -> int -> tactic + val CASE_TAC : Proof.context -> simpset -> int -> tactic val SIMP_CASE2_TAC : Proof.context -> simpset -> int -> tactic val SIMP_THM : Proof.context -> simpset -> thm -> thm val SIMP_TAC : Proof.context -> simpset -> int -> tactic @@ -228,7 +228,7 @@ in Variable.tradeT (K (map (add_norms o mk_trans) o maps mk_rew_rules)) ctxt [thm] end in normed end; -fun NORM norm_lhs_tac = EVERY'[rtac red2 , norm_lhs_tac, refl_tac]; +fun NORM ctxt norm_lhs_tac = EVERY' [resolve_tac ctxt [red2], norm_lhs_tac, refl_tac]; val trans_norms = map mk_trans normE_thms; @@ -331,9 +331,9 @@ | find_if(_) = false; in find_if(tm,0) end; -fun IF1_TAC cong_tac i = +fun IF1_TAC ctxt cong_tac i = let fun seq_try (ifth::ifths,ifc::ifcs) thm = - (COND (if_rewritable ifc i) (DETERM(rtac ifth i)) + (COND (if_rewritable ifc i) (DETERM(resolve_tac ctxt [ifth] i)) (seq_try(ifths,ifcs))) thm | seq_try([],_) thm = no_tac thm and try_rew thm = (seq_try(case_rews,case_consts) ORELSE one_subt) thm @@ -346,9 +346,9 @@ in (cong_tac THEN loop) thm end in COND (may_match(case_consts,i)) try_rew no_tac end; -fun CASE_TAC (SS{cong_net,...}) i = +fun CASE_TAC ctxt (SS{cong_net,...}) i = let val cong_tac = net_tac cong_net i -in NORM (IF1_TAC cong_tac) i end; +in NORM ctxt (IF1_TAC ctxt cong_tac) i end; (* Rewriting Automaton *) @@ -441,7 +441,7 @@ thm', anet, ats, (ss,thm,anet,ats,seq',more)::cs) end | NONE => if more - then rew((lhs_net_tac anet i THEN atac i) thm, + then rew((lhs_net_tac anet i THEN assume_tac ctxt i) thm, thm,ss,anet,ats,cs,false) else (ss,thm,anet,ats,cs); @@ -457,7 +457,7 @@ end; fun if_exp(thm,ss,anet,ats,cs) = - case Seq.pull (IF1_TAC (cong_tac i) i thm) of + case Seq.pull (IF1_TAC ctxt (cong_tac i) i thm) of SOME(thm',_) => (SIMP_LHS::IF::ss,thm',anet,ats,cs) | NONE => (ss,thm,anet,ats,cs); diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Auth/Event.thy --- a/src/HOL/Auth/Event.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Auth/Event.thy Sat Jul 18 20:54:56 2015 +0200 @@ -271,7 +271,7 @@ ML {* fun analz_mono_contra_tac ctxt = - rtac @{thm analz_impI} THEN' + resolve_tac ctxt @{thms analz_impI} THEN' REPEAT1 o (dresolve_tac ctxt @{thms analz_mono_contra}) THEN' (mp_tac ctxt) *} @@ -287,7 +287,7 @@ ML {* fun synth_analz_mono_contra_tac ctxt = - rtac @{thm syan_impI} THEN' + resolve_tac ctxt @{thms syan_impI} THEN' REPEAT1 o (dresolve_tac ctxt [@{thm knows_Spy_subset_knows_Spy_Says} RS @{thm synth_analz_mono} RS @{thm contra_subsetD}, diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Auth/OtwayReesBella.thy --- a/src/HOL/Auth/OtwayReesBella.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Auth/OtwayReesBella.thy Sat Jul 18 20:54:56 2015 +0200 @@ -250,7 +250,7 @@ Scan.succeed (fn ctxt => (SIMPLE_METHOD (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]), - REPEAT_FIRST (rtac @{thm analz_image_freshCryptK_lemma}), + REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshCryptK_lemma}), ALLGOALS (asm_simp_tac (put_simpset OtwayReesBella.analz_image_freshK_ss ctxt))]))) *} "for proving useful rewrite rule" diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Auth/Public.thy --- a/src/HOL/Auth/Public.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Auth/Public.thy Sat Jul 18 20:54:56 2015 +0200 @@ -434,7 +434,7 @@ Scan.succeed (fn ctxt => (SIMPLE_METHOD (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]), - REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}), + REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}), ALLGOALS (asm_simp_tac (put_simpset Public.analz_image_freshK_ss ctxt))]))) *} "for proving the Session Key Compromise theorem" diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Auth/Shared.thy --- a/src/HOL/Auth/Shared.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Auth/Shared.thy Sat Jul 18 20:54:56 2015 +0200 @@ -238,7 +238,7 @@ Scan.succeed (fn ctxt => (SIMPLE_METHOD (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]), - REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}), + REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}), ALLGOALS (asm_simp_tac (put_simpset Shared.analz_image_freshK_ss ctxt))]))) *} "for proving the Session Key Compromise theorem" diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Auth/Smartcard/ShoupRubin.thy --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Sat Jul 18 20:54:56 2015 +0200 @@ -753,8 +753,8 @@ fun analz_prepare_tac ctxt = prepare_tac ctxt THEN - dtac @{thm Gets_imp_knows_Spy_analz_Snd} 18 THEN - (*SR9*) dtac @{thm Gets_imp_knows_Spy_analz_Snd} 19 THEN + dresolve_tac ctxt @{thms Gets_imp_knows_Spy_analz_Snd} 18 THEN + (*SR9*) dresolve_tac ctxt @{thms Gets_imp_knows_Spy_analz_Snd} 19 THEN REPEAT_FIRST (eresolve_tac ctxt [asm_rl, conjE] ORELSE' hyp_subst_tac ctxt) end @@ -818,7 +818,7 @@ (SIMPLE_METHOD (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]), - REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}), + REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}), ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt addsimps [@{thm knows_Spy_Inputs_secureM_sr_Spy}, @{thm knows_Spy_Outpts_secureM_sr_Spy}, diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Auth/Smartcard/ShoupRubinBella.thy --- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Sat Jul 18 20:54:56 2015 +0200 @@ -762,8 +762,8 @@ fun analz_prepare_tac ctxt = prepare_tac ctxt THEN - dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 18 THEN - (*SR_U9*) dtac (@{thm Gets_imp_knows_Spy_analz_Snd}) 19 THEN + dresolve_tac ctxt @{thms Gets_imp_knows_Spy_analz_Snd} 18 THEN + (*SR_U9*) dresolve_tac ctxt @{thms Gets_imp_knows_Spy_analz_Snd} 19 THEN REPEAT_FIRST (eresolve_tac ctxt [asm_rl, conjE] ORELSE' hyp_subst_tac ctxt) end @@ -827,7 +827,7 @@ Scan.succeed (fn ctxt => (SIMPLE_METHOD (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]), - REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}), + REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}), ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt addsimps [@{thm knows_Spy_Inputs_secureM_srb_Spy}, @{thm knows_Spy_Outpts_secureM_srb_Spy}, diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Auth/Smartcard/Smartcard.thy --- a/src/HOL/Auth/Smartcard/Smartcard.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy Sat Jul 18 20:54:56 2015 +0200 @@ -404,7 +404,7 @@ Scan.succeed (fn ctxt => (SIMPLE_METHOD (EVERY [REPEAT_FIRST (resolve_tac ctxt [allI, ballI, impI]), - REPEAT_FIRST (rtac @{thm analz_image_freshK_lemma}), + REPEAT_FIRST (resolve_tac ctxt @{thms analz_image_freshK_lemma}), ALLGOALS (asm_simp_tac (put_simpset Smartcard.analz_image_freshK_ss ctxt))]))) *} "for proving the Session Key Compromise theorem" diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Bali/AxCompl.thy --- a/src/HOL/Bali/AxCompl.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Bali/AxCompl.thy Sat Jul 18 20:54:56 2015 +0200 @@ -1370,7 +1370,7 @@ apply - apply (induct_tac "n") apply (tactic "ALLGOALS (clarsimp_tac @{context})") -apply (tactic {* dtac (Thm.permute_prems 0 1 @{thm card_seteq}) 1 *}) +apply (tactic {* dresolve_tac @{context} [Thm.permute_prems 0 1 @{thm card_seteq}] 1 *}) apply simp apply (erule finite_imageI) apply (simp add: MGF_asm ax_derivs_asm) diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Bali/AxExample.thy --- a/src/HOL/Bali/AxExample.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Bali/AxExample.thy Sat Jul 18 20:54:56 2015 +0200 @@ -47,7 +47,7 @@ | NONE => Seq.empty); fun ax_tac ctxt = - REPEAT o rtac allI THEN' + REPEAT o resolve_tac ctxt [allI] THEN' resolve_tac ctxt @{thms ax_Skip ax_StatRef ax_MethdN ax_Alloc ax_Alloc_Arr ax_SXAlloc_Normal ax_derivs.intros(8-)}; *} diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Bali/AxSem.thy --- a/src/HOL/Bali/AxSem.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Bali/AxSem.thy Sat Jul 18 20:54:56 2015 +0200 @@ -692,8 +692,9 @@ apply (erule ax_derivs.induct) (*42 subgoals*) apply (tactic "ALLGOALS (strip_tac @{context})") -apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac @{thm subset_singletonD}, - etac disjE, fast_tac (@{context} addSIs @{thms ax_derivs.empty})]))*}) +apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dresolve_tac @{context} @{thms subset_singletonD}, + eresolve_tac @{context} [disjE], + fast_tac (@{context} addSIs @{thms ax_derivs.empty})]))*}) apply (tactic "TRYALL (hyp_subst_tac @{context})") apply (simp, rule ax_derivs.empty) apply (drule subset_insertD) diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Bali/Evaln.thy --- a/src/HOL/Bali/Evaln.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Bali/Evaln.thy Sat Jul 18 20:54:56 2015 +0200 @@ -448,9 +448,10 @@ lemma evaln_nonstrict [rule_format (no_asm), elim]: "G\s \t\\n\ (w, s') \ \m. n\m \ G\s \t\\m\ (w, s')" apply (erule evaln.induct) -apply (tactic {* ALLGOALS (EVERY' [strip_tac @{context}, TRY o etac @{thm Suc_le_D_lemma}, +apply (tactic {* ALLGOALS (EVERY' [strip_tac @{context}, + TRY o eresolve_tac @{context} @{thms Suc_le_D_lemma}, REPEAT o smp_tac @{context} 1, - resolve_tac @{context} @{thms evaln.intros} THEN_ALL_NEW TRY o atac]) *}) + resolve_tac @{context} @{thms evaln.intros} THEN_ALL_NEW TRY o assume_tac @{context}]) *}) (* 3 subgoals *) apply (auto split del: split_if) done diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Bali/TypeRel.thy --- a/src/HOL/Bali/TypeRel.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Bali/TypeRel.thy Sat Jul 18 20:54:56 2015 +0200 @@ -535,7 +535,7 @@ apply safe apply (rule widen.int_obj) prefer 6 apply (drule implmt_is_class) apply simp -apply (tactic "ALLGOALS (etac thin_rl)") +apply (erule_tac [!] thin_rl) prefer 6 apply simp apply (rule_tac [9] widen.arr_obj) apply (rotate_tac [9] -1) diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Datatype_Examples/Stream_Processor.thy --- a/src/HOL/Datatype_Examples/Stream_Processor.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Datatype_Examples/Stream_Processor.thy Sat Jul 18 20:54:56 2015 +0200 @@ -128,16 +128,27 @@ "rel_sp\<^sub>\ R1 R2 (map_sp\<^sub>\ f1 f2 sp) (map_sp\<^sub>\ g1 g2 sp') = rel_sp\<^sub>\ (BNF_Def.vimage2p f1 g1 R1) (BNF_Def.vimage2p f2 g2 R2) sp sp'" by (tactic {* - let val ks = 1 upto 2; + let + val ks = 1 upto 2; + val ctxt = @{context}; in - BNF_Tactics.unfold_thms_tac @{context} + BNF_Tactics.unfold_thms_tac ctxt @{thms sp\<^sub>\.rel_compp sp\<^sub>\.rel_conversep sp\<^sub>\.rel_Grp vimage2p_Grp} THEN - HEADGOAL (EVERY' [rtac iffI, rtac @{thm relcomppI}, rtac @{thm GrpI}, rtac refl, rtac CollectI, - BNF_Util.CONJ_WRAP' (K (rtac @{thm subset_UNIV})) ks, rtac @{thm relcomppI}, atac, - rtac @{thm conversepI}, rtac @{thm GrpI}, rtac refl, rtac CollectI, - BNF_Util.CONJ_WRAP' (K (rtac @{thm subset_UNIV})) ks, - REPEAT_DETERM o eresolve_tac @{context} @{thms relcomppE conversepE GrpE}, - hyp_subst_tac @{context}, atac]) + HEADGOAL (EVERY' [resolve_tac ctxt [iffI], + resolve_tac ctxt @{thms relcomppI}, + resolve_tac ctxt @{thms GrpI}, + resolve_tac ctxt [refl], + resolve_tac ctxt [CollectI], + BNF_Util.CONJ_WRAP' (K (resolve_tac ctxt @{thms subset_UNIV})) ks, + resolve_tac ctxt @{thms relcomppI}, assume_tac ctxt, + resolve_tac ctxt @{thms conversepI}, + resolve_tac ctxt @{thms GrpI}, + resolve_tac ctxt [refl], + resolve_tac ctxt [CollectI], + BNF_Util.CONJ_WRAP' (K (resolve_tac ctxt @{thms subset_UNIV})) ks, + REPEAT_DETERM o eresolve_tac ctxt @{thms relcomppE conversepE GrpE}, + hyp_subst_tac ctxt, + assume_tac ctxt]) end *}) diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy Sat Jul 18 20:54:56 2015 +0200 @@ -4102,7 +4102,7 @@ THEN' CSUBGOAL (fn (g, i) => let val th = frpar_oracle (ctxt, alternative, T, ps, g); - in rtac (th RS iffD2) i end); + in resolve_tac ctxt [th RS iffD2] i end); fun method alternative = let diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Decision_Procs/approximation.ML --- a/src/HOL/Decision_Procs/approximation.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Decision_Procs/approximation.ML Sat Jul 18 20:54:56 2015 +0200 @@ -12,7 +12,7 @@ structure Approximation: APPROXIMATION = struct -fun reorder_bounds_tac prems i = +fun reorder_bounds_tac ctxt prems i = let fun variable_of_bound (Const (@{const_name Trueprop}, _) $ (Const (@{const_name Set.member}, _) $ @@ -35,8 +35,8 @@ |> Graph.strong_conn |> map the_single |> rev |> map_filter (AList.lookup (op =) variable_bounds) - fun prepend_prem th tac - = tac THEN rtac (th RSN (2, @{thm mp})) i + fun prepend_prem th tac = + tac THEN resolve_tac ctxt [th RSN (2, @{thm mp})] i in fold prepend_prem order all_tac end @@ -49,9 +49,10 @@ |> Thm.prop_of |> Logic.dest_equals |> snd; (* Should be in HOL.thy ? *) -fun gen_eval_tac conv ctxt = CONVERSION - (Object_Logic.judgment_conv ctxt (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)) - THEN' rtac TrueI +fun gen_eval_tac conv ctxt = + CONVERSION + (Object_Logic.judgment_conv ctxt (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)) + THEN' resolve_tac ctxt [TrueI] val form_equations = @{thms interpret_form_equations}; @@ -78,10 +79,10 @@ |> HOLogic.mk_list @{typ nat} |> Thm.cterm_of ctxt in - (rtac (Thm.instantiate ([], [((("n", 0), @{typ nat}), n), + (resolve_tac ctxt [Thm.instantiate ([], [((("n", 0), @{typ nat}), n), ((("prec", 0), @{typ nat}), p), ((("ss", 0), @{typ "nat list"}), s)]) - @{thm "approx_form"}) i + @{thm approx_form}] i THEN simp_tac (put_simpset (simpset_of @{context}) ctxt) i) st end @@ -95,10 +96,10 @@ val s = vs |> map lookup_splitting |> hd |> Thm.cterm_of ctxt in - rtac (Thm.instantiate ([], [((("s", 0), @{typ nat}), s), + resolve_tac ctxt [Thm.instantiate ([], [((("s", 0), @{typ nat}), s), ((("t", 0), @{typ nat}), t), ((("prec", 0), @{typ nat}), p)]) - @{thm "approx_tse_form"}) i st + @{thm approx_tse_form}] i st end end @@ -190,8 +191,10 @@ |> the |> Thm.prems_of |> hd fun prepare_form ctxt term = apply_tactic ctxt term ( - REPEAT (FIRST' [etac @{thm intervalE}, etac @{thm meta_eqE}, rtac @{thm impI}] 1) - THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems 1) ctxt 1 + REPEAT (FIRST' [eresolve_tac ctxt @{thms intervalE}, + eresolve_tac ctxt @{thms meta_eqE}, + resolve_tac ctxt @{thms impI}] 1) + THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => reorder_bounds_tac ctxt' prems 1) ctxt 1 THEN DETERM (TRY (filter_prems_tac ctxt (K false) 1))) fun reify_form ctxt term = apply_tactic ctxt term @@ -249,10 +252,10 @@ >> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t))); fun approximation_tac prec splitting taylor ctxt i = - REPEAT (FIRST' [etac @{thm intervalE}, - etac @{thm meta_eqE}, - rtac @{thm impI}] i) - THEN Subgoal.FOCUS (fn {prems, ...} => reorder_bounds_tac prems i) ctxt i + REPEAT (FIRST' [eresolve_tac ctxt @{thms intervalE}, + eresolve_tac ctxt @{thms meta_eqE}, + resolve_tac ctxt @{thms impI}] i) + THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => reorder_bounds_tac ctxt' prems i) ctxt i THEN DETERM (TRY (filter_prems_tac ctxt (K false) i)) THEN DETERM (Reification.tac ctxt form_equations NONE i) THEN rewrite_interpret_form_tac ctxt prec splitting taylor i diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Decision_Procs/cooper_tac.ML --- a/src/HOL/Decision_Procs/cooper_tac.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Decision_Procs/cooper_tac.ML Sat Jul 18 20:54:56 2015 +0200 @@ -88,9 +88,9 @@ val pth = linzqe_oracle (ctxt, Envir.eta_long [] t1) in ((pth RS iffD2) RS pre_thm, - assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)) + assm_tac (i + 1) THEN (if q then I else TRY) (resolve_tac ctxt [TrueI] i)) end | _ => (pre_thm, assm_tac i)) - in rtac (mp_step nh (spec_step np th)) i THEN tac end); + in resolve_tac ctxt [mp_step nh (spec_step np th)] i THEN tac end); end diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Decision_Procs/ferrack_tac.ML --- a/src/HOL/Decision_Procs/ferrack_tac.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML Sat Jul 18 20:54:56 2015 +0200 @@ -67,9 +67,9 @@ let val pth = linr_oracle (ctxt, Envir.eta_long [] t1) in ((pth RS iffD2) RS pre_thm, - assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)) + assm_tac (i + 1) THEN (if q then I else TRY) (resolve_tac ctxt [TrueI] i)) end | _ => (pre_thm, assm_tac i) - in rtac ((mp_step nh o spec_step np) th) i THEN tac end); + in resolve_tac ctxt [(mp_step nh o spec_step np) th] i THEN tac end); end diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Decision_Procs/mir_tac.ML Sat Jul 18 20:54:56 2015 +0200 @@ -116,9 +116,9 @@ val pth = mirfr_oracle (ctxt, Envir.eta_long [] t1) in ((pth RS iffD2) RS pre_thm, - assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)) + assm_tac (i + 1) THEN (if q then I else TRY) (resolve_tac ctxt [TrueI] i)) end | _ => (pre_thm, assm_tac i) - in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end); + in resolve_tac ctxt [((mp_step nh) o (spec_step np)) th] i THEN tac end); end diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy --- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy Sat Jul 18 20:54:56 2015 +0200 @@ -477,7 +477,7 @@ apply (rule_tac x = "schA" in spec) apply (rule_tac x = "schB" in spec) apply (rule_tac x = "tr" in spec) -apply (tactic "thin_tac' 5 1") +apply (tactic "thin_tac' @{context} 5 1") apply (rule nat_less_induct) apply (rule allI)+ apply (rename_tac tr schB schA) @@ -487,7 +487,7 @@ apply (case_tac "Forall (%x. x:act B & x~:act A) tr") apply (rule seq_take_lemma [THEN iffD2, THEN spec]) -apply (tactic "thin_tac' 5 1") +apply (tactic "thin_tac' @{context} 5 1") apply (case_tac "Finite tr") @@ -697,7 +697,7 @@ apply (rule_tac x = "schA" in spec) apply (rule_tac x = "schB" in spec) apply (rule_tac x = "tr" in spec) -apply (tactic "thin_tac' 5 1") +apply (tactic "thin_tac' @{context} 5 1") apply (rule nat_less_induct) apply (rule allI)+ apply (rename_tac tr schB schA) @@ -707,7 +707,7 @@ apply (case_tac "Forall (%x. x:act A & x~:act B) tr") apply (rule seq_take_lemma [THEN iffD2, THEN spec]) -apply (tactic "thin_tac' 5 1") +apply (tactic "thin_tac' @{context} 5 1") apply (case_tac "Finite tr") diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/HOLCF/IOA/meta_theory/Sequence.thy --- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Sat Jul 18 20:54:56 2015 +0200 @@ -1098,7 +1098,7 @@ THEN simp_tac (ctxt addsimps rws) i; fun Seq_Finite_induct_tac ctxt i = - etac @{thm Seq_Finite_ind} i + eresolve_tac ctxt @{thms Seq_Finite_ind} i THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt i))); fun pair_tac ctxt s = diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy --- a/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy Sat Jul 18 20:54:56 2015 +0200 @@ -48,9 +48,9 @@ ML {* -fun thin_tac' j = +fun thin_tac' ctxt j = rotate_tac (j - 1) THEN' - etac thin_rl THEN' + eresolve_tac ctxt [thin_rl] THEN' rotate_tac (~ (j - 1)) *} @@ -180,7 +180,7 @@ apply (intro strip) apply (rule mp) prefer 2 apply (assumption) -apply (tactic "thin_tac' 1 1") +apply (tactic "thin_tac' @{context} 1 1") apply (rule_tac x = "s" in spec) apply (rule nat_less_induct) apply (intro strip) diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/HOLCF/Lift.thy --- a/src/HOL/HOLCF/Lift.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/HOLCF/Lift.thy Sat Jul 18 20:54:56 2015 +0200 @@ -46,7 +46,7 @@ method_setup defined = {* Scan.succeed (fn ctxt => SIMPLE_METHOD' - (etac @{thm lift_definedE} THEN' asm_simp_tac ctxt)) + (eresolve_tac ctxt @{thms lift_definedE} THEN' asm_simp_tac ctxt)) *} lemma DefE: "Def x = \ \ R" diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sat Jul 18 20:54:56 2015 +0200 @@ -142,7 +142,8 @@ val cs = ContProc.cont_thms lam val betas = map (fn c => mk_meta_eq (c RS @{thm beta_cfun})) cs in - prove thy (def_thm::betas) goal (K [rtac reflexive_thm 1]) + prove thy (def_thm::betas) goal + (fn {context = ctxt, ...} => [resolve_tac ctxt [reflexive_thm] 1]) end end @@ -228,9 +229,9 @@ val goal = mk_trp (foldr1 mk_disj (mk_undef y :: map one_con spec')) (* first rules replace "y = bottom \/ P" with "rep$y = bottom \/ P" *) fun tacs ctxt = [ - rtac (iso_locale RS @{thm iso.casedist_rule}) 1, + resolve_tac ctxt [iso_locale RS @{thm iso.casedist_rule}] 1, rewrite_goals_tac ctxt [mk_meta_eq (iso_locale RS @{thm iso.iso_swap})], - rtac thm3 1] + resolve_tac ctxt [thm3] 1] in val nchotomy = prove thy con_betas goal (tacs o #context) val exhaust = @@ -245,8 +246,8 @@ val rules = @{thms compact_sinl compact_sinr compact_spair compact_up compact_ONE} fun tacs ctxt = - [rtac (iso_locale RS @{thm iso.compact_abs}) 1, - REPEAT (resolve_tac ctxt rules 1 ORELSE atac 1)] + [resolve_tac ctxt [iso_locale RS @{thm iso.compact_abs}] 1, + REPEAT (resolve_tac ctxt rules 1 ORELSE assume_tac ctxt 1)] fun con_compact (con, args) = let val vs = vars_of args @@ -709,7 +710,10 @@ local fun dis_strict dis = let val goal = mk_trp (mk_strict dis) - in prove thy dis_defs goal (K [rtac (hd case_rews) 1]) end + in + prove thy dis_defs goal + (fn {context = ctxt, ...} => [resolve_tac ctxt [hd case_rews] 1]) + end in val dis_stricts = map dis_strict dis_consts end @@ -739,9 +743,9 @@ val x = Free ("x", lhsT) val simps = dis_apps @ @{thms dist_eq_tr} fun tacs ctxt = - [rtac @{thm iffI} 1, + [resolve_tac ctxt @{thms iffI} 1, asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps dis_stricts) 2, - rtac exhaust 1, atac 1, + resolve_tac ctxt [exhaust] 1, assume_tac ctxt 1, ALLGOALS (asm_full_simp_tac (put_simpset simple_ss ctxt addsimps simps))] val goal = mk_trp (mk_eq (mk_undef (dis ` x), mk_undef x)) in prove thy [] goal (tacs o #context) end diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/HOLCF/Tools/Domain/domain_induction.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML Sat Jul 18 20:54:56 2015 +0200 @@ -161,11 +161,11 @@ val rules = prems @ con_rews @ @{thms simp_thms} val simplify = asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules) fun arg_tac (lazy, _) = - rtac (if lazy then allI else case_UU_allI) 1 + resolve_tac ctxt [if lazy then allI else case_UU_allI] 1 fun tacs ctxt = rewrite_goals_tac ctxt @{thms atomize_all atomize_imp} :: map arg_tac args @ - [REPEAT (rtac impI 1), ALLGOALS simplify] + [REPEAT (resolve_tac ctxt [impI] 1), ALLGOALS simplify] in Goal.prove ctxt [] [] subgoal (EVERY o tacs o #context) end @@ -181,7 +181,7 @@ TRY (safe_tac (put_claset HOL_cs ctxt))] fun con_tac _ = asm_simp_tac (put_simpset take_ss ctxt) 1 THEN - (resolve_tac ctxt prems' THEN_ALL_NEW etac spec) 1 + (resolve_tac ctxt prems' THEN_ALL_NEW eresolve_tac ctxt [spec]) 1 fun cases_tacs (cons, exhaust) = Rule_Insts.res_inst_tac ctxt [((("y", 0), Position.none), "x")] [] exhaust 1 :: asm_simp_tac (put_simpset take_ss ctxt addsimps prems) 1 :: @@ -201,9 +201,9 @@ fun tacf {prems, context = ctxt} = let fun finite_tac (take_induct, fin_ind) = - rtac take_induct 1 THEN + resolve_tac ctxt [take_induct] 1 THEN (if is_finite then all_tac else resolve_tac ctxt prems 1) THEN - (rtac fin_ind THEN_ALL_NEW solve_tac ctxt prems) 1 + (resolve_tac ctxt [fin_ind] THEN_ALL_NEW solve_tac ctxt prems) 1 val fin_inds = Project_Rule.projections ctxt finite_ind in TRY (safe_tac (put_claset HOL_cs ctxt)) THEN @@ -326,10 +326,10 @@ val prems' = Project_Rule.projections ctxt prem' val dests = map (fn th => th RS spec RS spec RS mp) prems' fun one_tac (dest, rews) = - dtac dest 1 THEN safe_tac (put_claset HOL_cs ctxt) THEN + dresolve_tac ctxt [dest] 1 THEN safe_tac (put_claset HOL_cs ctxt) THEN ALLGOALS (asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps rews)) in - rtac @{thm nat.induct} 1 THEN + resolve_tac ctxt @{thms nat.induct} 1 THEN simp_tac (put_simpset HOL_ss ctxt addsimps rules) 1 THEN safe_tac (put_claset HOL_cs ctxt) THEN EVERY (map one_tac (dests ~~ take_rews)) @@ -350,7 +350,7 @@ let val rule = hd prems RS coind_lemma in - rtac take_lemma 1 THEN + resolve_tac ctxt [take_lemma] 1 THEN asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps (rule :: prems)) 1 end in diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Jul 18 20:54:56 2015 +0200 @@ -310,12 +310,12 @@ Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} => EVERY [rewrite_goals_tac ctxt map_apply_thms, - rtac (map_cont_thm RS @{thm cont_fix_ind}) 1, + resolve_tac ctxt [map_cont_thm RS @{thm cont_fix_ind}] 1, REPEAT (resolve_tac ctxt adm_rules 1), simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1, simp_tac (put_simpset HOL_basic_ss ctxt addsimps tuple_rules) 1, - REPEAT (etac @{thm conjE} 1), - REPEAT (resolve_tac ctxt (deflation_rules @ prems) 1 ORELSE atac 1)]) + REPEAT (eresolve_tac ctxt @{thms conjE} 1), + REPEAT (resolve_tac ctxt (deflation_rules @ prems) 1 ORELSE assume_tac ctxt 1)]) end fun conjuncts [] _ = [] | conjuncts (n::[]) thm = [(n, thm)] @@ -623,14 +623,13 @@ Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} => EVERY [rewrite_goals_tac ctxt (defl_apply_thms @ map_apply_thms), - rtac (@{thm cont_parallel_fix_ind} - OF [defl_cont_thm, map_cont_thm]) 1, + resolve_tac ctxt [@{thm cont_parallel_fix_ind} OF [defl_cont_thm, map_cont_thm]] 1, REPEAT (resolve_tac ctxt adm_rules 1), simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1, simp_tac (put_simpset HOL_basic_ss ctxt addsimps tuple_rules) 1, simp_tac (put_simpset HOL_basic_ss ctxt addsimps map_ID_simps) 1, - REPEAT (etac @{thm conjE} 1), - REPEAT (resolve_tac ctxt (isodefl_rules @ prems) 1 ORELSE atac 1)]) + REPEAT (eresolve_tac ctxt @{thms conjE} 1), + REPEAT (resolve_tac ctxt (isodefl_rules @ prems) 1 ORELSE assume_tac ctxt 1)]) end val isodefl_binds = map (Binding.prefix_name "isodefl_") dbinds fun conjuncts [] _ = [] @@ -655,9 +654,9 @@ val lhs = list_ccomb (map_const, map mk_ID (filter is_cpo Ts)) val goal = mk_eqs (lhs, mk_ID lhsT) fun tac ctxt = EVERY - [rtac @{thm isodefl_DEFL_imp_ID} 1, + [resolve_tac ctxt @{thms isodefl_DEFL_imp_ID} 1, stac ctxt DEFL_thm 1, - rtac isodefl_thm 1, + resolve_tac ctxt [isodefl_thm] 1, REPEAT (resolve_tac ctxt @{thms isodefl_ID_DEFL isodefl_LIFTDEFL} 1)] in Goal.prove_global thy [] [] goal (tac o #context) @@ -700,8 +699,8 @@ EVERY [simp_tac (put_simpset HOL_basic_ss ctxt addsimps start_rules) 1, simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms fix_def2}) 1, - rtac @{thm lub_eq} 1, - rtac @{thm nat.induct} 1, + resolve_tac ctxt @{thms lub_eq} 1, + resolve_tac ctxt @{thms nat.induct} 1, simp_tac (put_simpset HOL_basic_ss ctxt addsimps rules0) 1, asm_full_simp_tac (put_simpset beta_ss ctxt addsimps rules1) 1] in @@ -713,12 +712,13 @@ let val n = Free ("n", natT) val goal = mk_eqs (mk_lub (lambda n (take_const $ n)), mk_ID lhsT) - val tac = + fun tac ctxt = EVERY - [rtac @{thm trans} 1, rtac map_ID_thm 2, + [resolve_tac ctxt @{thms trans} 1, + resolve_tac ctxt [map_ID_thm] 2, cut_tac lub_take_lemma 1, - REPEAT (etac @{thm Pair_inject} 1), atac 1] - val lub_take_thm = Goal.prove_global thy [] [] goal (K tac) + REPEAT (eresolve_tac ctxt @{thms Pair_inject} 1), assume_tac ctxt 1] + val lub_take_thm = Goal.prove_global thy [] [] goal (tac o #context) in add_qualified_thm "lub_take" (dbind, lub_take_thm) thy end diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML Sat Jul 18 20:54:56 2015 +0200 @@ -320,12 +320,12 @@ in Goal.prove_global thy [] [] goal (fn {context = ctxt, ...} => EVERY - [rtac @{thm nat.induct} 1, + [resolve_tac ctxt @{thms nat.induct} 1, simp_tac (put_simpset HOL_basic_ss ctxt addsimps bottom_rules) 1, asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps take_Suc_thms) 1, - REPEAT (etac @{thm conjE} 1 + REPEAT (eresolve_tac ctxt @{thms conjE} 1 ORELSE resolve_tac ctxt deflation_rules 1 - ORELSE atac 1)]) + ORELSE assume_tac ctxt 1)]) end fun conjuncts [] _ = [] | conjuncts (n::[]) thm = [(n, thm)] @@ -444,7 +444,7 @@ take_Suc_thms @ decisive_abs_rep_thms @ @{thms decisive_ID decisive_ssum_map decisive_sprod_map} fun tac ctxt = EVERY [ - rtac @{thm nat.induct} 1, + resolve_tac ctxt @{thms nat.induct} 1, simp_tac (put_simpset HOL_ss ctxt addsimps rules0) 1, asm_simp_tac (put_simpset HOL_ss ctxt addsimps rules1) 1] in Goal.prove_global thy [] [] goal (tac o #context) end @@ -461,7 +461,7 @@ fun tac ctxt = EVERY [ rewrite_goals_tac ctxt finite_defs, - rtac @{thm lub_ID_finite} 1, + resolve_tac ctxt @{thms lub_ID_finite} 1, resolve_tac ctxt chain_take_thms 1, resolve_tac ctxt lub_take_thms 1, resolve_tac ctxt decisive_thms 1] diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/HOLCF/Tools/cont_proc.ML --- a/src/HOL/HOLCF/Tools/cont_proc.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/HOLCF/Tools/cont_proc.ML Sat Jul 18 20:54:56 2015 +0200 @@ -102,7 +102,7 @@ fun new_cont_tac f' i = case all_cont_thms f' of [] => no_tac - | (c::_) => rtac c i + | (c::_) => resolve_tac ctxt [c] i fun cont_tac_of_term (Const (@{const_name cont}, _) $ f) = let diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/HOLCF/Tools/cpodef.ML --- a/src/HOL/HOLCF/Tools/cpodef.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/HOLCF/Tools/cpodef.ML Sat Jul 18 20:54:56 2015 +0200 @@ -73,8 +73,8 @@ val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible] val (full_tname, Ts) = dest_Type newT val lhs_sorts = map (snd o dest_TFree) Ts - val tac = rtac (@{thm typedef_cpo} OF cpo_thms) 1 - val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) (K tac) thy + fun tac ctxt = resolve_tac ctxt [@{thm typedef_cpo} OF cpo_thms] 1 + val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) tac thy (* transfer thms so that they will know about the new cpo instance *) val cpo_thms' = map (Thm.transfer thy) cpo_thms fun make thm = Drule.zero_var_indexes (thm OF cpo_thms') @@ -112,8 +112,8 @@ val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, bottom_mem] val (full_tname, Ts) = dest_Type newT val lhs_sorts = map (snd o dest_TFree) Ts - val tac = rtac (@{thm typedef_pcpo} OF pcpo_thms) 1 - val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) (K tac) thy + fun tac ctxt = resolve_tac ctxt [@{thm typedef_pcpo} OF pcpo_thms] 1 + val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) tac thy val pcpo_thms' = map (Thm.transfer thy) pcpo_thms fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms') val Rep_strict = make @{thm typedef_Rep_strict} @@ -182,7 +182,7 @@ val below_def = singleton (Proof_Context.export lthy ctxt_thy) below_ldef val thy = lthy |> Class.prove_instantiation_exit - (K (rtac (@{thm typedef_po} OF [type_definition, below_def]) 1)) + (fn ctxt => resolve_tac ctxt [@{thm typedef_po} OF [type_definition, below_def]] 1) in ((info, below_def), thy) end fun prepare_cpodef @@ -205,7 +205,7 @@ fun cpodef_result nonempty admissible thy = let val ((info as (_, {type_definition, ...}), below_def), thy) = thy - |> add_podef typ set opt_morphs (fn _ => rtac nonempty 1) + |> add_podef typ set opt_morphs (fn ctxt => resolve_tac ctxt [nonempty] 1) val (cpo_info, thy) = thy |> prove_cpo name newT morphs type_definition below_def admissible in @@ -237,7 +237,7 @@ fun pcpodef_result bottom_mem admissible thy = let - fun tac _ = rtac exI 1 THEN rtac bottom_mem 1 + fun tac ctxt = resolve_tac ctxt [exI] 1 THEN resolve_tac ctxt [bottom_mem] 1 val ((info as (_, {type_definition, ...}), below_def), thy) = thy |> add_podef typ set opt_morphs tac val (cpo_info, thy) = thy diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/HOLCF/Tools/domaindef.ML --- a/src/HOL/HOLCF/Tools/domaindef.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/HOLCF/Tools/domaindef.ML Sat Jul 18 20:54:56 2015 +0200 @@ -108,8 +108,8 @@ val set = @{term "defl_set :: udom defl => udom set"} $ defl (*pcpodef*) - fun tac1 _ = rtac @{thm defl_set_bottom} 1 - fun tac2 _ = rtac @{thm adm_defl_set} 1 + fun tac1 ctxt = resolve_tac ctxt @{thms defl_set_bottom} 1 + fun tac2 ctxt = resolve_tac ctxt @{thms adm_defl_set} 1 val ((info, cpo_info, pcpo_info), thy) = thy |> Cpodef.add_pcpodef typ set (SOME morphs) (tac1, tac2) @@ -165,7 +165,7 @@ liftemb_def, liftprj_def, liftdefl_def] val thy = lthy |> Class.prove_instantiation_instance - (K (rtac (@{thm typedef_domain_class} OF typedef_thms) 1)) + (fn ctxt => resolve_tac ctxt [@{thm typedef_domain_class} OF typedef_thms] 1) |> Local_Theory.exit_global (*other theorems*) diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/HOLCF/Tools/fixrec.ML --- a/src/HOL/HOLCF/Tools/fixrec.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/HOLCF/Tools/fixrec.ML Sat Jul 18 20:54:56 2015 +0200 @@ -301,7 +301,7 @@ val unfold_thm = the (Symtab.lookup tab c) val rule = unfold_thm RS @{thm ssubst_lhs} in - CHANGED (rtac rule i THEN eta_tac i THEN asm_simp_tac ctxt i) + CHANGED (resolve_tac ctxt [rule] i THEN eta_tac i THEN asm_simp_tac ctxt i) end in SUBGOAL (fn ti => the_default no_tac (try tac ti)) @@ -311,7 +311,7 @@ fun make_simps ctxt (unfold_thm, eqns : (Attrib.binding * term) list) = let val rule = unfold_thm RS @{thm ssubst_lhs} - val tac = rtac rule 1 THEN eta_tac 1 THEN asm_simp_tac ctxt 1 + val tac = resolve_tac ctxt [rule] 1 THEN eta_tac 1 THEN asm_simp_tac ctxt 1 fun prove_term t = Goal.prove ctxt [] [] t (K tac) fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t) in diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Hoare/hoare_tac.ML --- a/src/HOL/Hoare/hoare_tac.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Hoare/hoare_tac.ML Sat Jul 18 20:54:56 2015 +0200 @@ -132,9 +132,9 @@ fun set_to_pred_tac ctxt var_names = SUBGOAL (fn (_, i) => before_set2pred_simp_tac ctxt i THEN_MAYBE EVERY [ - rtac subsetI i, - rtac CollectI i, - dtac CollectD i, + resolve_tac ctxt [subsetI] i, + resolve_tac ctxt [CollectI] i, + dresolve_tac ctxt [CollectD] i, TRY (split_all_tac ctxt i) THEN_MAYBE (rename_tac var_names i THEN full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm split_conv}]) i)]); @@ -148,7 +148,8 @@ (*******************************************************************************) fun max_simp_tac ctxt var_names tac = - FIRST' [rtac subset_refl, set_to_pred_tac ctxt var_names THEN_MAYBE' tac]; + FIRST' [resolve_tac ctxt [subset_refl], + set_to_pred_tac ctxt var_names THEN_MAYBE' tac]; fun basic_simp_tac ctxt var_names tac = simp_tac @@ -163,26 +164,28 @@ let val var_names = map (fst o dest_Free) vars; fun wlp_tac i = - rtac @{thm SeqRule} i THEN rule_tac false (i + 1) + resolve_tac ctxt @{thms SeqRule} i THEN rule_tac false (i + 1) and rule_tac pre_cond i st = st |> (*abstraction over st prevents looping*) ((wlp_tac i THEN rule_tac pre_cond i) ORELSE (FIRST [ - rtac @{thm SkipRule} i, - rtac @{thm AbortRule} i, + resolve_tac ctxt @{thms SkipRule} i, + resolve_tac ctxt @{thms AbortRule} i, EVERY [ - rtac @{thm BasicRule} i, - rtac Mlem i, + resolve_tac ctxt @{thms BasicRule} i, + resolve_tac ctxt [Mlem] i, split_simp_tac ctxt i], EVERY [ - rtac @{thm CondRule} i, + resolve_tac ctxt @{thms CondRule} i, rule_tac false (i + 2), rule_tac false (i + 1)], EVERY [ - rtac @{thm WhileRule} i, + resolve_tac ctxt @{thms WhileRule} i, basic_simp_tac ctxt var_names tac (i + 2), rule_tac true (i + 1)]] - THEN (if pre_cond then basic_simp_tac ctxt var_names tac i else rtac subset_refl i))); + THEN ( + if pre_cond then basic_simp_tac ctxt var_names tac i + else resolve_tac ctxt [subset_refl] i))); in rule_tac end; diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Hoare_Parallel/Gar_Coll.thy --- a/src/HOL/Hoare_Parallel/Gar_Coll.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy Sat Jul 18 20:54:56 2015 +0200 @@ -775,11 +775,21 @@ --\20 subgoals left\ apply(tactic\TRYALL (clarify_tac @{context})\) apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) -apply(tactic \TRYALL (etac disjE)\) +apply(tactic \TRYALL (eresolve_tac @{context} [disjE])\) apply simp_all -apply(tactic \TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac @{context}])\) -apply(tactic \TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{context}])\) -apply(tactic \TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}])\) +apply(tactic \TRYALL(EVERY'[resolve_tac @{context} [disjI2], + resolve_tac @{context} [subset_trans], + eresolve_tac @{context} @{thms Graph3}, + force_tac @{context}, + assume_tac @{context}])\) +apply(tactic \TRYALL(EVERY'[resolve_tac @{context} [disjI2], + eresolve_tac @{context} [subset_trans], + resolve_tac @{context} @{thms Graph9}, + force_tac @{context}])\) +apply(tactic \TRYALL(EVERY'[resolve_tac @{context} [disjI1], + eresolve_tac @{context} @{thms psubset_subset_trans}, + resolve_tac @{context} @{thms Graph9}, + force_tac @{context}])\) done subsubsection \Interference freedom Mutator-Collector\ diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy --- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Sat Jul 18 20:54:56 2015 +0200 @@ -1178,40 +1178,62 @@ --\14 subgoals left\ apply(tactic \TRYALL (clarify_tac @{context})\) apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) -apply(tactic \TRYALL (rtac conjI)\) -apply(tactic \TRYALL (rtac impI)\) -apply(tactic \TRYALL (etac disjE)\) -apply(tactic \TRYALL (etac conjE)\) -apply(tactic \TRYALL (etac disjE)\) -apply(tactic \TRYALL (etac disjE)\) +apply(tactic \TRYALL (resolve_tac @{context} [conjI])\) +apply(tactic \TRYALL (resolve_tac @{context} [impI])\) +apply(tactic \TRYALL (eresolve_tac @{context} [disjE])\) +apply(tactic \TRYALL (eresolve_tac @{context} [conjE])\) +apply(tactic \TRYALL (eresolve_tac @{context} [disjE])\) +apply(tactic \TRYALL (eresolve_tac @{context} [disjE])\) --\72 subgoals left\ apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12) --\35 subgoals left\ -apply(tactic \TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac @{context}])\) +apply(tactic \TRYALL(EVERY'[resolve_tac @{context} [disjI1], + resolve_tac @{context} [subset_trans], + eresolve_tac @{context} @{thms Graph3}, + force_tac @{context}, + assume_tac @{context}])\) --\28 subgoals left\ -apply(tactic \TRYALL (etac conjE)\) -apply(tactic \TRYALL (etac disjE)\) +apply(tactic \TRYALL (eresolve_tac @{context} [conjE])\) +apply(tactic \TRYALL (eresolve_tac @{context} [disjE])\) --\34 subgoals left\ apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) apply(rule disjI2,rule disjI1,erule le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update) apply(case_tac [!] "M x!(T (Muts x ! j))=Black") apply(simp_all add:Graph10) --\47 subgoals left\ -apply(tactic \TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{context}])\) +apply(tactic \TRYALL(EVERY'[REPEAT o resolve_tac @{context} [disjI2], + eresolve_tac @{context} @{thms subset_psubset_trans}, + eresolve_tac @{context} @{thms Graph11}, + force_tac @{context}])\) --\41 subgoals left\ -apply(tactic \TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans}, - force_tac (@{context} addsimps - [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])])\) +apply(tactic \TRYALL(EVERY'[resolve_tac @{context} [disjI2], + resolve_tac @{context} [disjI1], + eresolve_tac @{context} @{thms le_trans}, + force_tac (@{context} addsimps @{thms Queue_def less_Suc_eq_le le_length_filter_update})])\) --\35 subgoals left\ -apply(tactic \TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}])\) +apply(tactic \TRYALL(EVERY'[resolve_tac @{context} [disjI2], + resolve_tac @{context} [disjI1], + eresolve_tac @{context} @{thms psubset_subset_trans}, + resolve_tac @{context} @{thms Graph9}, + force_tac @{context}])\) --\31 subgoals left\ -apply(tactic \TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}])\) +apply(tactic \TRYALL(EVERY'[resolve_tac @{context} [disjI2], + resolve_tac @{context} [disjI1], + eresolve_tac @{context} @{thms subset_psubset_trans}, + eresolve_tac @{context} @{thms Graph11}, + force_tac @{context}])\) --\29 subgoals left\ -apply(tactic \TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}])\) +apply(tactic \TRYALL(EVERY'[REPEAT o resolve_tac @{context} [disjI2], + eresolve_tac @{context} @{thms subset_psubset_trans}, + eresolve_tac @{context} @{thms subset_psubset_trans}, + eresolve_tac @{context} @{thms Graph11}, + force_tac @{context}])\) --\25 subgoals left\ -apply(tactic \TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans}, - force_tac (@{context} addsimps - [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])])\) +apply(tactic \TRYALL(EVERY'[resolve_tac @{context} [disjI2], + resolve_tac @{context} [disjI2], + resolve_tac @{context} [disjI1], + eresolve_tac @{context} @{thms le_trans}, + force_tac (@{context} addsimps @{thms Queue_def less_Suc_eq_le le_length_filter_update})])\) --\10 subgoals left\ apply(rule disjI2,rule disjI2,rule conjI,erule less_le_trans,force simp add:Queue_def less_Suc_eq_le le_length_filter_update, rule disjI1, rule less_imp_le, erule less_le_trans, force simp add:Queue_def less_Suc_eq_le le_length_filter_update)+ done diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Hoare_Parallel/OG_Examples.thy --- a/src/HOL/Hoare_Parallel/OG_Examples.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Sat Jul 18 20:54:56 2015 +0200 @@ -434,7 +434,7 @@ --\112 subgoals left\ apply(simp_all (no_asm)) --\43 subgoals left\ -apply(tactic \ALLGOALS (conjI_Tac (K all_tac))\) +apply(tactic \ALLGOALS (conjI_Tac @{context} (K all_tac))\) --\419 subgoals left\ apply(tactic \ALLGOALS (clarify_tac @{context})\) --\99 subgoals left\ diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Hoare_Parallel/OG_Tactics.thy --- a/src/HOL/Hoare_Parallel/OG_Tactics.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Hoare_Parallel/OG_Tactics.thy Sat Jul 18 20:54:56 2015 +0200 @@ -291,9 +291,9 @@ @{text n} subgoals, one for each conjunct:\ ML \ -fun conjI_Tac tac i st = st |> - ( (EVERY [rtac conjI i, - conjI_Tac tac (i+1), +fun conjI_Tac ctxt tac i st = st |> + ( (EVERY [resolve_tac ctxt [conjI] i, + conjI_Tac ctxt tac (i+1), tac i]) ORELSE (tac i) ) \ @@ -326,119 +326,123 @@ ML \ -fun WlpTac ctxt i = (rtac (@{thm SeqRule}) i) THEN (HoareRuleTac ctxt false (i+1)) +fun WlpTac ctxt i = resolve_tac ctxt @{thms SeqRule} i THEN HoareRuleTac ctxt false (i + 1) and HoareRuleTac ctxt precond i st = st |> ( (WlpTac ctxt i THEN HoareRuleTac ctxt precond i) ORELSE - (FIRST[rtac (@{thm SkipRule}) i, - rtac (@{thm BasicRule}) i, - EVERY[rtac (@{thm ParallelConseqRule}) i, + (FIRST[resolve_tac ctxt @{thms SkipRule} i, + resolve_tac ctxt @{thms BasicRule} i, + EVERY[resolve_tac ctxt @{thms ParallelConseqRule} i, ParallelConseq ctxt (i+2), ParallelTac ctxt (i+1), ParallelConseq ctxt i], - EVERY[rtac (@{thm CondRule}) i, + EVERY[resolve_tac ctxt @{thms CondRule} i, HoareRuleTac ctxt false (i+2), HoareRuleTac ctxt false (i+1)], - EVERY[rtac (@{thm WhileRule}) i, + EVERY[resolve_tac ctxt @{thms WhileRule} i, HoareRuleTac ctxt 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 resolve_tac ctxt @{thms subset_refl} i))) -and AnnWlpTac ctxt i = (rtac (@{thm AnnSeq}) i) THEN (AnnHoareRuleTac ctxt (i+1)) +and AnnWlpTac ctxt i = resolve_tac ctxt @{thms AnnSeq} i THEN AnnHoareRuleTac ctxt (i + 1) and AnnHoareRuleTac ctxt i st = st |> ( (AnnWlpTac ctxt i THEN AnnHoareRuleTac ctxt i ) ORELSE - (FIRST[(rtac (@{thm AnnskipRule}) i), - EVERY[rtac (@{thm AnnatomRule}) i, + (FIRST[(resolve_tac ctxt @{thms AnnskipRule} i), + EVERY[resolve_tac ctxt @{thms AnnatomRule} i, HoareRuleTac ctxt true (i+1)], - (rtac (@{thm AnnwaitRule}) i), - rtac (@{thm AnnBasic}) i, - EVERY[rtac (@{thm AnnCond1}) i, + (resolve_tac ctxt @{thms AnnwaitRule} i), + resolve_tac ctxt @{thms AnnBasic} i, + EVERY[resolve_tac ctxt @{thms AnnCond1} i, AnnHoareRuleTac ctxt (i+3), AnnHoareRuleTac ctxt (i+1)], - EVERY[rtac (@{thm AnnCond2}) i, + EVERY[resolve_tac ctxt @{thms AnnCond2} i, AnnHoareRuleTac ctxt (i+1)], - EVERY[rtac (@{thm AnnWhile}) i, + EVERY[resolve_tac ctxt @{thms AnnWhile} i, AnnHoareRuleTac ctxt (i+2)], - EVERY[rtac (@{thm AnnAwait}) i, + EVERY[resolve_tac ctxt @{thms AnnAwait} i, HoareRuleTac ctxt true (i+1)], K all_tac i])) -and ParallelTac ctxt i = EVERY[rtac (@{thm ParallelRule}) i, +and ParallelTac ctxt i = EVERY[resolve_tac ctxt @{thms ParallelRule} i, interfree_Tac ctxt (i+1), MapAnn_Tac ctxt i] and MapAnn_Tac ctxt i st = st |> - (FIRST[rtac (@{thm MapAnnEmpty}) i, - EVERY[rtac (@{thm MapAnnList}) i, + (FIRST[resolve_tac ctxt @{thms MapAnnEmpty} i, + EVERY[resolve_tac ctxt @{thms MapAnnList} i, MapAnn_Tac ctxt (i+1), AnnHoareRuleTac ctxt i], - EVERY[rtac (@{thm MapAnnMap}) i, - rtac (@{thm allI}) i, rtac (@{thm impI}) i, + EVERY[resolve_tac ctxt @{thms MapAnnMap} i, + resolve_tac ctxt @{thms allI} i, + resolve_tac ctxt @{thms impI} i, AnnHoareRuleTac ctxt i]]) and interfree_swap_Tac ctxt i st = st |> - (FIRST[rtac (@{thm interfree_swap_Empty}) i, - EVERY[rtac (@{thm interfree_swap_List}) i, + (FIRST[resolve_tac ctxt @{thms interfree_swap_Empty} i, + EVERY[resolve_tac ctxt @{thms interfree_swap_List} i, interfree_swap_Tac ctxt (i+2), interfree_aux_Tac ctxt (i+1), interfree_aux_Tac ctxt i ], - EVERY[rtac (@{thm interfree_swap_Map}) i, - rtac (@{thm allI}) i,rtac (@{thm impI}) i, - conjI_Tac (interfree_aux_Tac ctxt) i]]) + EVERY[resolve_tac ctxt @{thms interfree_swap_Map} i, + resolve_tac ctxt @{thms allI} i, + resolve_tac ctxt @{thms impI} i, + conjI_Tac ctxt (interfree_aux_Tac ctxt) i]]) and interfree_Tac ctxt i st = st |> - (FIRST[rtac (@{thm interfree_Empty}) i, - EVERY[rtac (@{thm interfree_List}) i, + (FIRST[resolve_tac ctxt @{thms interfree_Empty} i, + EVERY[resolve_tac ctxt @{thms interfree_List} i, interfree_Tac ctxt (i+1), interfree_swap_Tac ctxt i], - EVERY[rtac (@{thm interfree_Map}) i, - rtac (@{thm allI}) i,rtac (@{thm allI}) i,rtac (@{thm impI}) i, + EVERY[resolve_tac ctxt @{thms interfree_Map} i, + resolve_tac ctxt @{thms allI} i, + resolve_tac ctxt @{thms allI} i, + resolve_tac ctxt @{thms impI} i, interfree_aux_Tac ctxt i ]]) and interfree_aux_Tac ctxt i = (before_interfree_simp_tac ctxt i ) THEN - (FIRST[rtac (@{thm interfree_aux_rule1}) i, + (FIRST[resolve_tac ctxt @{thms interfree_aux_rule1} i, dest_assertions_Tac ctxt i]) and dest_assertions_Tac ctxt i st = st |> - (FIRST[EVERY[rtac (@{thm AnnBasic_assertions}) i, + (FIRST[EVERY[resolve_tac ctxt @{thms AnnBasic_assertions} i, dest_atomics_Tac ctxt (i+1), dest_atomics_Tac ctxt i], - EVERY[rtac (@{thm AnnSeq_assertions}) i, + EVERY[resolve_tac ctxt @{thms AnnSeq_assertions} i, dest_assertions_Tac ctxt (i+1), dest_assertions_Tac ctxt i], - EVERY[rtac (@{thm AnnCond1_assertions}) i, + EVERY[resolve_tac ctxt @{thms AnnCond1_assertions} i, dest_assertions_Tac ctxt (i+2), dest_assertions_Tac ctxt (i+1), dest_atomics_Tac ctxt i], - EVERY[rtac (@{thm AnnCond2_assertions}) i, + EVERY[resolve_tac ctxt @{thms AnnCond2_assertions} i, dest_assertions_Tac ctxt (i+1), dest_atomics_Tac ctxt i], - EVERY[rtac (@{thm AnnWhile_assertions}) i, + EVERY[resolve_tac ctxt @{thms AnnWhile_assertions} i, dest_assertions_Tac ctxt (i+2), dest_atomics_Tac ctxt (i+1), dest_atomics_Tac ctxt i], - EVERY[rtac (@{thm AnnAwait_assertions}) i, + EVERY[resolve_tac ctxt @{thms AnnAwait_assertions} i, dest_atomics_Tac ctxt (i+1), dest_atomics_Tac ctxt i], dest_atomics_Tac ctxt i]) and dest_atomics_Tac ctxt i st = st |> - (FIRST[EVERY[rtac (@{thm AnnBasic_atomics}) i, + (FIRST[EVERY[resolve_tac ctxt @{thms AnnBasic_atomics} i, HoareRuleTac ctxt true i], - EVERY[rtac (@{thm AnnSeq_atomics}) i, + EVERY[resolve_tac ctxt @{thms AnnSeq_atomics} i, dest_atomics_Tac ctxt (i+1), dest_atomics_Tac ctxt i], - EVERY[rtac (@{thm AnnCond1_atomics}) i, + EVERY[resolve_tac ctxt @{thms AnnCond1_atomics} i, dest_atomics_Tac ctxt (i+1), dest_atomics_Tac ctxt i], - EVERY[rtac (@{thm AnnCond2_atomics}) i, + EVERY[resolve_tac ctxt @{thms AnnCond2_atomics} i, dest_atomics_Tac ctxt i], - EVERY[rtac (@{thm AnnWhile_atomics}) i, + EVERY[resolve_tac ctxt @{thms AnnWhile_atomics} i, dest_atomics_Tac ctxt i], - EVERY[rtac (@{thm Annatom_atomics}) i, + EVERY[resolve_tac ctxt @{thms Annatom_atomics} i, HoareRuleTac ctxt true i], - EVERY[rtac (@{thm AnnAwait_atomics}) i, + EVERY[resolve_tac ctxt @{thms AnnAwait_atomics} i, HoareRuleTac ctxt true i], K all_tac i]) \ @@ -482,18 +486,18 @@ text \Tactics useful for dealing with the generated verification conditions:\ method_setup conjI_tac = \ - Scan.succeed (K (SIMPLE_METHOD' (conjI_Tac (K all_tac))))\ + Scan.succeed (fn ctxt => SIMPLE_METHOD' (conjI_Tac ctxt (K all_tac)))\ "verification condition generator for interference freedom tests" ML \ -fun disjE_Tac tac i st = st |> - ( (EVERY [etac disjE i, - disjE_Tac tac (i+1), +fun disjE_Tac ctxt tac i st = st |> + ( (EVERY [eresolve_tac ctxt [disjE] i, + disjE_Tac ctxt tac (i+1), tac i]) ORELSE (tac i) ) \ method_setup disjE_tac = \ - Scan.succeed (K (SIMPLE_METHOD' (disjE_Tac (K all_tac))))\ + Scan.succeed (fn ctxt => SIMPLE_METHOD' (disjE_Tac ctxt (K all_tac)))\ "verification condition generator for interference freedom tests" end diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/IMPP/Com.thy --- a/src/HOL/IMPP/Com.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/IMPP/Com.thy Sat Jul 18 20:54:56 2015 +0200 @@ -83,7 +83,10 @@ "WT_bodies = (!(pn,b):set bodies. WT b)" -ML {* val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl] *} +ML {* + fun make_imp_tac ctxt = + EVERY' [resolve_tac ctxt [mp], fn i => assume_tac ctxt (i + 1), eresolve_tac ctxt [thin_rl]] +*} lemma finite_dom_body: "finite (dom body)" apply (unfold body_def) diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/IMPP/Hoare.thy --- a/src/HOL/IMPP/Hoare.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/IMPP/Hoare.thy Sat Jul 18 20:54:56 2015 +0200 @@ -278,7 +278,7 @@ lemma hoare_sound: "G||-ts ==> G||=ts" apply (erule hoare_derivs.induct) -apply (tactic {* TRYALL (eresolve_tac @{context} [@{thm Loop_sound_lemma}, @{thm Body_sound_lemma}] THEN_ALL_NEW atac) *}) +apply (tactic {* TRYALL (eresolve_tac @{context} [@{thm Loop_sound_lemma}, @{thm Body_sound_lemma}] THEN_ALL_NEW assume_tac @{context}) *}) apply (unfold hoare_valids_def) apply blast apply blast @@ -351,7 +351,8 @@ rule_tac [3] P1 = "%Z' s. s= (Z[Loc loc::=fun Z])" in hoare_derivs.Local [THEN conseq1], erule_tac [3] conseq12) apply (erule_tac [5] hoare_derivs.Comp, erule_tac [5] conseq12) -apply (tactic {* (rtac @{thm hoare_derivs.If} THEN_ALL_NEW etac @{thm conseq12}) 6 *}) +apply (tactic {* (resolve_tac @{context} @{thms hoare_derivs.If} THEN_ALL_NEW + eresolve_tac @{context} @{thms conseq12}) 6 *}) apply (rule_tac [8] hoare_derivs.Loop [THEN conseq2], erule_tac [8] conseq12) apply auto done @@ -435,7 +436,7 @@ apply (frule finite_subset) apply (rule finite_dom_body [THEN finite_imageI]) apply (rotate_tac 2) -apply (tactic "make_imp_tac 1") +apply (tactic "make_imp_tac @{context} 1") apply (erule finite_induct) apply (clarsimp intro!: hoare_derivs.empty) apply (clarsimp intro!: hoare_derivs.insert simp del: range_composition) diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/IMPP/Natural.thy --- a/src/HOL/IMPP/Natural.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/IMPP/Natural.thy Sat Jul 18 20:54:56 2015 +0200 @@ -111,7 +111,9 @@ lemma evaln_evalc: " -n-> t ==> -c-> t" apply (erule evaln.induct) -apply (tactic {* ALLGOALS (resolve_tac @{context} @{thms evalc.intros} THEN_ALL_NEW atac) *}) +apply (tactic {* + ALLGOALS (resolve_tac @{context} @{thms evalc.intros} THEN_ALL_NEW assume_tac @{context}) +*}) done lemma Suc_le_D_lemma: "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'" @@ -137,11 +139,12 @@ lemma evalc_evaln: " -c-> t ==> ? n. -n-> t" apply (erule evalc.induct) -apply (tactic {* ALLGOALS (REPEAT o etac exE) *}) -apply (tactic {* TRYALL (EVERY' [dtac @{thm evaln_max2}, assume_tac @{context}, +apply (tactic {* ALLGOALS (REPEAT o eresolve_tac @{context} [exE]) *}) +apply (tactic {* TRYALL (EVERY' [dresolve_tac @{context} @{thms evaln_max2}, assume_tac @{context}, REPEAT o eresolve_tac @{context} [exE, conjE]]) *}) apply (tactic - {* ALLGOALS (rtac exI THEN' resolve_tac @{context} @{thms evaln.intros} THEN_ALL_NEW atac) *}) + {* ALLGOALS (resolve_tac @{context} [exI] THEN' + resolve_tac @{context} @{thms evaln.intros} THEN_ALL_NEW assume_tac @{context}) *}) done lemma eval_eq: " -c-> t = (? n. -n-> t)" diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/IOA/Solve.thy --- a/src/HOL/IOA/Solve.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/IOA/Solve.thy Sat Jul 18 20:54:56 2015 +0200 @@ -145,7 +145,7 @@ apply force apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: split_if) apply (tactic {* - REPEAT((resolve_tac @{context} [conjI, impI] 1 ORELSE etac conjE 1) THEN + REPEAT((resolve_tac @{context} [conjI, impI] 1 ORELSE eresolve_tac @{context} [conjE] 1) THEN asm_full_simp_tac(@{context} addsimps [@{thm comp1_reachable}, @{thm comp2_reachable}]) 1) *}) done diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Import/import_rule.ML --- a/src/HOL/Import/import_rule.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Import/import_rule.ML Sat Jul 18 20:54:56 2015 +0200 @@ -220,7 +220,7 @@ val tnames = sort_strings (map fst tfrees) val ((_, typedef_info), thy') = Typedef.add_typedef_global false (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c - (SOME (Binding.name rep_name, Binding.name abs_name)) (fn _ => rtac th2 1) thy + (SOME (Binding.name rep_name, Binding.name abs_name)) (fn ctxt => resolve_tac ctxt [th2] 1) thy val aty = #abs_type (#1 typedef_info) val th = freezeT thy' (#type_definition (#2 typedef_info)) val (th_s, _) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th)) diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Metis_Examples/Type_Encodings.thy --- a/src/HOL/Metis_Examples/Type_Encodings.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy Sat Jul 18 20:54:56 2015 +0200 @@ -54,7 +54,7 @@ fun tac [] st = all_tac st | tac (type_enc :: type_encs) st = st (* |> tap (fn _ => tracing (@{make_string} type_enc)) *) - |> ((if null type_encs then all_tac else rtac @{thm fork} 1) + |> ((if null type_encs then all_tac else resolve_tac ctxt @{thms fork} 1) THEN Metis_Tactic.metis_tac [type_enc] ATP_Problem_Generate.combsN ctxt ths 1 THEN COND (has_fewer_prems 2) all_tac no_tac diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/MicroJava/J/JTypeSafe.thy --- a/src/HOL/MicroJava/J/JTypeSafe.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy Sat Jul 18 20:54:56 2015 +0200 @@ -178,8 +178,9 @@ ML{* fun forward_hyp_tac ctxt = - ALLGOALS (TRY o (EVERY' [dtac spec, mp_tac ctxt, - (mp_tac ctxt ORELSE' (dtac spec THEN' mp_tac ctxt)), REPEAT o (etac conjE)])) + ALLGOALS (TRY o (EVERY' [dresolve_tac ctxt [spec], mp_tac ctxt, + (mp_tac ctxt ORELSE' (dresolve_tac ctxt [spec] THEN' mp_tac ctxt)), + REPEAT o (eresolve_tac ctxt [conjE])])) *} @@ -202,7 +203,7 @@ apply( tactic "ALLGOALS (REPEAT o resolve_tac @{context} [impI, allI])") apply( tactic {* ALLGOALS (eresolve_tac @{context} [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}] THEN_ALL_NEW (full_simp_tac (put_simpset (simpset_of @{theory_context Conform}) @{context}))) *}) -apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac @{context}])") +apply(tactic "ALLGOALS (EVERY' [REPEAT o (eresolve_tac @{context} [conjE]), REPEAT o hyp_subst_tac @{context}])") -- "Level 7" -- "15 NewC" @@ -241,7 +242,7 @@ -- "for FAss" apply( tactic {* EVERY'[eresolve_tac @{context} [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}] - THEN_ALL_NEW (full_simp_tac @{context}), REPEAT o (etac conjE), hyp_subst_tac @{context}] 3*}) + THEN_ALL_NEW (full_simp_tac @{context}), REPEAT o (eresolve_tac @{context} [conjE]), hyp_subst_tac @{context}] 3*}) -- "for if" apply( tactic {* (Induct_Tacs.case_tac @{context} "the_Bool v" [] NONE THEN_ALL_NEW diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Sat Jul 18 20:54:56 2015 +0200 @@ -127,8 +127,8 @@ @{thm vec_lambda_beta}, @{thm vector_scalar_mult_def}]) fun vector_arith_tac ctxt ths = simp_tac (put_simpset ss1 ctxt) - THEN' (fn i => rtac @{thm Cartesian_Euclidean_Space.setsum_cong_aux} i - ORELSE rtac @{thm setsum.neutral} i + THEN' (fn i => resolve_tac ctxt @{thms Cartesian_Euclidean_Space.setsum_cong_aux} i + ORELSE resolve_tac ctxt @{thms setsum.neutral} i ORELSE simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm vec_eq_iff}]) i) (* THEN' TRY o clarify_tac HOL_cs THEN' (TRY o rtac @{thm iffI}) *) THEN' asm_full_simp_tac (put_simpset ss2 ctxt addsimps ths) diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Multivariate_Analysis/normarith.ML --- a/src/HOL/Multivariate_Analysis/normarith.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/normarith.ML Sat Jul 18 20:54:56 2015 +0200 @@ -401,6 +401,6 @@ fun norm_arith_tac ctxt = clarify_tac (put_claset HOL_cs ctxt) THEN' Object_Logic.full_atomize_tac ctxt THEN' - CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i); + CSUBGOAL ( fn (p,i) => resolve_tac ctxt [norm_arith ctxt (Thm.dest_arg p )] i); end; diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Nominal/nominal_atoms.ML Sat Jul 18 20:54:56 2015 +0200 @@ -117,10 +117,10 @@ val simp1 = @{thm inj_on_def} :: injects; fun proof1 ctxt = EVERY [simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp1) 1, - rtac @{thm ballI} 1, - rtac @{thm ballI} 1, - rtac @{thm impI} 1, - atac 1] + resolve_tac ctxt @{thms ballI} 1, + resolve_tac ctxt @{thms ballI} 1, + resolve_tac ctxt @{thms impI} 1, + assume_tac ctxt 1] val (inj_thm,thy2) = add_thms_string [((ak^"_inj",Goal.prove_global thy1 [] [] stmnt1 (proof1 o #context)), [])] thy1 @@ -133,8 +133,8 @@ val proof2 = fn {prems, context = ctxt} => Induct_Tacs.case_tac ctxt "y" [] NONE 1 THEN asm_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp1) 1 THEN - rtac @{thm exI} 1 THEN - rtac @{thm refl} 1 + resolve_tac ctxt @{thms exI} 1 THEN + resolve_tac ctxt @{thms refl} 1 (* third statement *) val (inject_thm,thy3) = @@ -149,9 +149,9 @@ val simp3 = [@{thm UNIV_def}] fun proof3 ctxt = EVERY [cut_facts_tac inj_thm 1, - dtac @{thm range_inj_infinite} 1, - asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp2) 1, - simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp3) 1] + dresolve_tac ctxt @{thms range_inj_infinite} 1, + asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp2) 1, + simp_tac (put_simpset HOL_basic_ss ctxt addsimps simp3) 1] val (inf_thm,thy4) = add_thms_string [((ak^"_infinite",Goal.prove_global thy3 [] [] stmnt3 (proof3 o #context)), [])] thy3 @@ -437,7 +437,10 @@ fun proof ctxt = simp_tac (put_simpset HOL_basic_ss ctxt addsimps maps (Global_Theory.get_thms thy') ["cp_def"]) 1 - THEN EVERY [rtac allI 1, rtac allI 1, rtac allI 1, rtac cp1 1]; + THEN EVERY [resolve_tac ctxt [allI] 1, + resolve_tac ctxt [allI] 1, + resolve_tac ctxt [allI] 1, + resolve_tac ctxt [cp1] 1]; in yield_singleton add_thms_string ((name, Goal.prove_global thy' [] [] statement (proof o #context)), []) thy' @@ -504,10 +507,10 @@ val at_inst = Global_Theory.get_thm thy' ("at_" ^ ak_name' ^ "_inst"); fun proof1 ctxt = EVERY [Class.intro_classes_tac ctxt [], - rtac ((at_inst RS at_pt_inst) RS pt1) 1, - rtac ((at_inst RS at_pt_inst) RS pt2) 1, - rtac ((at_inst RS at_pt_inst) RS pt3) 1, - atac 1]; + resolve_tac ctxt [(at_inst RS at_pt_inst) RS pt1] 1, + resolve_tac ctxt [(at_inst RS at_pt_inst) RS pt2] 1, + resolve_tac ctxt [(at_inst RS at_pt_inst) RS pt3] 1, + assume_tac ctxt 1]; fun proof2 ctxt = Class.intro_classes_tac ctxt [] THEN REPEAT (asm_simp_tac @@ -537,7 +540,10 @@ fun pt_proof thm ctxt = EVERY [Class.intro_classes_tac ctxt [], - rtac (thm RS pt1) 1, rtac (thm RS pt2) 1, rtac (thm RS pt3) 1, atac 1]; + resolve_tac ctxt [thm RS pt1] 1, + resolve_tac ctxt [thm RS pt2] 1, + resolve_tac ctxt [thm RS pt3] 1, + assume_tac ctxt 1]; val pt_thm_fun = at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst)); val pt_thm_set = pt_inst RS pt_set_inst; @@ -581,9 +587,10 @@ fun proof ctxt = (if ak_name = ak_name' then - let val at_thm = Global_Theory.get_thm thy' ("at_"^ak_name^"_inst"); - in EVERY [Class.intro_classes_tac ctxt [], - rtac ((at_thm RS fs_at_inst) RS fs1) 1] end + let val at_thm = Global_Theory.get_thm thy' ("at_"^ak_name^"_inst") in + EVERY [Class.intro_classes_tac ctxt [], + resolve_tac ctxt [(at_thm RS fs_at_inst) RS fs1] 1] + end else let val dj_inst = Global_Theory.get_thm thy' ("dj_"^ak_name'^"_"^ak_name); val simp_s = @@ -605,7 +612,8 @@ let val cls_name = Sign.full_bname thy ("fs_"^ak_name); val fs_inst = Global_Theory.get_thm thy ("fs_"^ak_name^"_inst"); - fun fs_proof thm ctxt = EVERY [Class.intro_classes_tac ctxt [], rtac (thm RS fs1) 1]; + fun fs_proof thm ctxt = + EVERY [Class.intro_classes_tac ctxt [], resolve_tac ctxt [thm RS fs1] 1]; val fs_thm_unit = fs_unit_inst; val fs_thm_prod = fs_inst RS (fs_inst RS fs_prod_inst); @@ -652,7 +660,7 @@ val at_inst = Global_Theory.get_thm thy'' ("at_"^ak_name''^"_inst"); in EVERY [Class.intro_classes_tac ctxt [], - rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1] + resolve_tac ctxt [at_inst RS (pt_inst RS pt_perm_compose)] 1] end) else (let @@ -686,7 +694,8 @@ val pt_inst = Global_Theory.get_thm thy' ("pt_"^ak_name^"_inst"); val at_inst = Global_Theory.get_thm thy' ("at_"^ak_name^"_inst"); - fun cp_proof thm ctxt = EVERY [Class.intro_classes_tac ctxt [], rtac (thm RS cp1) 1]; + fun cp_proof thm ctxt = + EVERY [Class.intro_classes_tac ctxt [], resolve_tac ctxt [thm RS cp1] 1]; val cp_thm_unit = cp_unit_inst; val cp_thm_prod = cp_inst RS (cp_inst RS cp_prod_inst); diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Sat Jul 18 20:54:56 2015 +0200 @@ -586,7 +586,9 @@ (name, map (fn (v, _) => (v, dummyS)) tvs, mx) (* FIXME keep constraints!? *) (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $ Const (cname, U --> HOLogic.boolT)) NONE - (fn ctxt => rtac exI 1 THEN rtac CollectI 1 THEN + (fn ctxt => + resolve_tac ctxt [exI] 1 THEN + resolve_tac ctxt [CollectI] 1 THEN QUIET_BREADTH_FIRST (has_fewer_prems 1) (resolve_tac ctxt rep_intrs 1)) thy |> (fn ((_, r), thy) => let @@ -663,8 +665,8 @@ (if atom1 = atom2 then [] else [Rep RS perm_closed2 RS Abs_inverse]))) 1, cong_tac ctxt 1, - rtac refl 1, - rtac cp1' 1]) thy) + resolve_tac ctxt [refl] 1, + resolve_tac ctxt [cp1'] 1]) thy) (Abs_inverse_thms ~~ Rep_thms ~~ perm_defs ~~ new_type_names ~~ tyvars ~~ perm_closed_thms1 ~~ perm_closed_thms2) thy end; @@ -812,7 +814,7 @@ in Goal.prove_global_future thy8 [] [] eqn (fn {context = ctxt, ...} => EVERY [resolve_tac ctxt inj_thms 1, rewrite_goals_tac ctxt rewrites, - rtac refl 3, + resolve_tac ctxt [refl] 3, resolve_tac ctxt rep_intrs 2, REPEAT (resolve_tac ctxt Rep_thms 1)]) end; @@ -1046,11 +1048,12 @@ (HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj indrule_lemma_prems), HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj indrule_lemma_concls))) (fn {context = ctxt, ...} => EVERY - [REPEAT (etac conjE 1), + [REPEAT (eresolve_tac ctxt [conjE] 1), REPEAT (EVERY - [TRY (rtac conjI 1), + [TRY (resolve_tac ctxt [conjI] 1), full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps Rep_inverse_thms) 1, - etac mp 1, resolve_tac ctxt Rep_thms 1])]); + eresolve_tac ctxt [mp] 1, + resolve_tac ctxt Rep_thms 1])]); val Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of indrule_lemma))); val frees = if length Ps = 1 then [Free ("P", snd (dest_Var (hd Ps)))] else @@ -1064,7 +1067,7 @@ val dt_induct = Goal.prove_global_future thy8 [] (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop) (fn {prems, context = ctxt} => EVERY - [rtac indrule_lemma' 1, + [resolve_tac ctxt [indrule_lemma'] 1, (Old_Datatype_Aux.ind_tac ctxt rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1, EVERY (map (fn (prem, r) => (EVERY @@ -1262,9 +1265,9 @@ fin_set_supp @ ths)) 1]); val (([(_, cx)], ths), ctxt') = Obtain.result (fn ctxt' => EVERY - [etac exE 1, + [eresolve_tac ctxt' [exE] 1, full_simp_tac (put_simpset HOL_ss ctxt' addsimps (fresh_prod :: fresh_atm)) 1, - REPEAT (etac conjE 1)]) + REPEAT (eresolve_tac ctxt' [conjE] 1)]) [ex] ctxt in (freshs1 @ [Thm.term_of cx], freshs2 @ ths, ctxt') end; @@ -1320,7 +1323,7 @@ EVERY (Old_Datatype_Aux.ind_tac context1 dt_induct tnames 1 :: maps (fn ((_, (_, _, constrs)), (_, constrs')) => map (fn ((cname, cargs), is) => - REPEAT (rtac allI 1) THEN + REPEAT (resolve_tac context1 [allI] 1) THEN SUBPROOF (fn {prems = iprems, params, concl, context = context2, ...} => let @@ -1354,14 +1357,15 @@ list_comb (cnstr, maps (fn ((bs, t), cs) => cs @ [fold_rev (mk_perm []) (map perm_of_pair (bs ~~ cs)) t]) (xs'' ~~ freshs1'))))) - (fn _ => EVERY + (fn {context = ctxt, ...} => EVERY (simp_tac (put_simpset HOL_ss context3 addsimps flat inject_thms) 1 :: - REPEAT (FIRSTGOAL (rtac conjI)) :: + REPEAT (FIRSTGOAL (resolve_tac ctxt [conjI])) :: maps (fn ((bs, t), cs) => if null bs then [] - else rtac sym 1 :: maps (fn (b, c) => - [rtac trans 1, rtac sym 1, - rtac (fresh_fresh_inst thy9 b c) 1, + else resolve_tac ctxt [sym] 1 :: maps (fn (b, c) => + [resolve_tac ctxt [trans] 1, + resolve_tac ctxt [sym] 1, + resolve_tac ctxt [fresh_fresh_inst thy9 b c] 1, simp_tac ind_ss1' 1, simp_tac ind_ss2 1, simp_tac ind_ss3' 1]) (bs ~~ cs)) @@ -1385,8 +1389,8 @@ EVERY [cut_facts_tac [th] 1, REPEAT (eresolve_tac context [conjE, @{thm allE_Nil}] 1), - REPEAT (etac allE 1), - REPEAT (TRY (rtac conjI 1) THEN asm_full_simp_tac ind_ss5 1)] + REPEAT (eresolve_tac context [allE] 1), + REPEAT (TRY (resolve_tac context [conjI] 1) THEN asm_full_simp_tac ind_ss5 1)] end); val induct_aux' = Thm.instantiate ([], @@ -1404,10 +1408,10 @@ (map (augment_sort thy9 fs_cp_sort) ind_prems) (augment_sort thy9 fs_cp_sort ind_concl) (fn {prems, context = ctxt} => EVERY - [rtac induct_aux' 1, + [resolve_tac ctxt [induct_aux'] 1, REPEAT (resolve_tac ctxt fs_atoms 1), REPEAT ((resolve_tac ctxt prems THEN_ALL_NEW - (etac @{thm meta_spec} ORELSE' + (eresolve_tac ctxt @{thms meta_spec} ORELSE' full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [fresh_def]))) 1)]) val (_, thy10) = thy9 |> @@ -1551,7 +1555,8 @@ (Goal.prove_global_future thy11 [] [] (augment_sort thy1 pt_cp_sort (HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map HOLogic.mk_imp ps)))) - (fn {context = ctxt, ...} => rtac rec_induct 1 THEN REPEAT + (fn {context = ctxt, ...} => + resolve_tac ctxt [rec_induct] 1 THEN REPEAT (simp_tac (put_simpset HOL_basic_ss ctxt addsimps flat perm_simps' addsimprocs [NominalPermeq.perm_simproc_app]) 1 THEN @@ -1561,9 +1566,10 @@ Goal.prove_global_future thy11 [] [] (augment_sort thy1 pt_cp_sort (Logic.mk_implies (HOLogic.mk_Trueprop Q, HOLogic.mk_Trueprop P))) - (fn {context = ctxt, ...} => dtac (Thm.instantiate ([], + (fn {context = ctxt, ...} => + dresolve_tac ctxt [Thm.instantiate ([], [((("pi", 0), permT), - Thm.global_cterm_of thy11 (Const (@{const_name rev}, permT --> permT) $ pi))]) th) 1 THEN + Thm.global_cterm_of thy11 (Const (@{const_name rev}, permT --> permT) $ pi))]) th] 1 THEN NominalPermeq.perm_simp_tac (put_simpset HOL_ss ctxt) 1)) (ps ~~ ths) in (ths, ths') end) dt_atomTs); @@ -1594,7 +1600,7 @@ end) (recTs ~~ rec_result_Ts ~~ rec_sets ~~ (1 upto length recTs)))))) (fn {prems = fins, context = ctxt} => - (rtac rec_induct THEN_ALL_NEW cut_facts_tac fins) 1 THEN REPEAT + (resolve_tac ctxt [rec_induct] THEN_ALL_NEW cut_facts_tac fins) 1 THEN REPEAT (NominalPermeq.finite_guess_tac (put_simpset HOL_ss ctxt addsimps [fs_name]) 1)))) end) dt_atomTs; @@ -1640,25 +1646,25 @@ val _ $ (_ $ (_ $ S $ _)) $ _ = Thm.prop_of supports_fresh; val tuple = foldr1 HOLogic.mk_prod (x :: rec_fns') in EVERY - [rtac (Drule.cterm_instantiate + [resolve_tac context [Drule.cterm_instantiate [(Thm.global_cterm_of thy11 S, Thm.global_cterm_of thy11 (Const (@{const_name Nominal.supp}, fastype_of tuple --> HOLogic.mk_setT aT) $ tuple))] - supports_fresh) 1, + supports_fresh] 1, simp_tac (put_simpset HOL_basic_ss context addsimps [supports_def, Thm.symmetric fresh_def, fresh_prod]) 1, REPEAT_DETERM (resolve_tac context [allI, impI] 1), - REPEAT_DETERM (etac conjE 1), - rtac unique 1, - SUBPROOF (fn {prems = prems', params = [(_, a), (_, b)], ...} => EVERY - [cut_facts_tac [rec_prem] 1, - rtac (Thm.instantiate ([], + REPEAT_DETERM (eresolve_tac context [conjE] 1), + resolve_tac context [unique] 1, + SUBPROOF (fn {context = ctxt, prems = prems', params = [(_, a), (_, b)], ...} => + EVERY [cut_facts_tac [rec_prem] 1, + resolve_tac ctxt [Thm.instantiate ([], [((("pi", 0), mk_permT aT), Thm.global_cterm_of thy11 - (perm_of_pair (Thm.term_of a, Thm.term_of b)))]) eqvt_th) 1, + (perm_of_pair (Thm.term_of a, Thm.term_of b)))]) eqvt_th] 1, asm_simp_tac (put_simpset HOL_ss context addsimps (prems' @ perm_swap @ perm_fresh_fresh)) 1]) context 1, - rtac rec_prem 1, + resolve_tac context [rec_prem] 1, simp_tac (put_simpset HOL_ss context addsimps (fs_name :: supp_prod :: finite_Un :: finite_prems)) 1, simp_tac (put_simpset HOL_ss context addsimps (Thm.symmetric fresh_def :: @@ -1705,10 +1711,10 @@ resolve_tac ctxt exists_fresh' 1, asm_simp_tac (put_simpset HOL_ss ctxt addsimps (supp_prod :: finite_Un :: fs_atoms)) 1]); val (([(_, cx)], ths), ctxt') = Obtain.result - (fn _ => EVERY - [etac exE 1, - full_simp_tac (put_simpset HOL_ss ctxt addsimps (fresh_prod :: fresh_atm)) 1, - REPEAT (etac conjE 1)]) + (fn ctxt' => EVERY + [eresolve_tac ctxt' [exE] 1, + full_simp_tac (put_simpset HOL_ss ctxt' addsimps (fresh_prod :: fresh_atm)) 1, + REPEAT (eresolve_tac ctxt [conjE] 1)]) [ex] ctxt in (freshs1 @ [Thm.term_of cx], freshs2 @ ths, ctxt') end; @@ -1740,13 +1746,13 @@ (rec_unique_frees'' ~~ rec_unique_frees' ~~ rec_sets ~~ rec_preds))))) (fn {context = ctxt, ...} => - rtac rec_induct 1 THEN + resolve_tac ctxt [rec_induct] 1 THEN REPEAT ((resolve_tac ctxt P_ind_ths THEN_ALL_NEW assume_tac ctxt) 1)))); val rec_fin_supp_thms' = map (fn (ths, (T, fin_ths)) => (T, map (curry op MRS fin_ths) ths)) (rec_fin_supp_thms ~~ finite_thss); in EVERY - ([rtac induct_aux_rec 1] @ + ([resolve_tac context [induct_aux_rec] 1] @ maps (fn ((_, finite_ths), finite_th) => [cut_facts_tac (finite_th :: finite_ths) 1, asm_simp_tac (put_simpset HOL_ss context addsimps [supp_prod, finite_Un]) 1]) @@ -1754,10 +1760,10 @@ maps (fn ((_, idxss), elim) => maps (fn idxs => [full_simp_tac (put_simpset HOL_ss context addsimps [Thm.symmetric fresh_def, supp_prod, Un_iff]) 1, REPEAT_DETERM (eresolve_tac context @{thms conjE ex1E} 1), - rtac @{thm ex1I} 1, - (resolve_tac context rec_intrs THEN_ALL_NEW atac) 1, + resolve_tac context @{thms ex1I} 1, + (resolve_tac context rec_intrs THEN_ALL_NEW assume_tac context) 1, rotate_tac ~1 1, - ((DETERM o etac elim) THEN_ALL_NEW full_simp_tac + ((DETERM o eresolve_tac context [elim]) THEN_ALL_NEW full_simp_tac (put_simpset HOL_ss context addsimps flat distinct_thms)) 1] @ (if null idxs then [] else [hyp_subst_tac context 1, SUBPROOF (fn {asms, concl, prems = prems', params, context = context', ...} => @@ -1825,10 +1831,10 @@ val pi1_pi2_eq = Goal.prove context'' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (fold_rev (mk_perm []) pi1 lhs, fold_rev (mk_perm []) pi2 rhs))) - (fn _ => EVERY + (fn {context = ctxt, ...} => EVERY [cut_facts_tac constr_fresh_thms 1, asm_simp_tac (put_simpset HOL_basic_ss context'' addsimps perm_fresh_fresh) 1, - rtac prem 1]); + resolve_tac ctxt [prem] 1]); (** pi1 o ts = pi2 o us **) val _ = warning "step 4: pi1 o ts = pi2 o us"; @@ -1866,21 +1872,21 @@ val k = find_index (equal s) rec_set_names; val pi = rpi1 @ pi2; fun mk_pi z = fold_rev (mk_perm []) pi z; - fun eqvt_tac p = + fun eqvt_tac ctxt p = let val U as Type (_, [Type (_, [T, _])]) = fastype_of p; val l = find_index (equal T) dt_atomTs; val th = nth (nth rec_equiv_thms' l) k; val th' = Thm.instantiate ([], [((("pi", 0), U), Thm.global_cterm_of thy11 p)]) th; - in rtac th' 1 end; + in resolve_tac ctxt [th'] 1 end; val th' = Goal.prove context'' [] [] (HOLogic.mk_Trueprop (S $ mk_pi x $ mk_pi y)) - (fn _ => EVERY - (map eqvt_tac pi @ + (fn {context = ctxt, ...} => EVERY + (map (eqvt_tac ctxt) pi @ [simp_tac (put_simpset HOL_ss context'' addsimps (fresh_prems' @ freshs2' @ perm_swap @ perm_fresh_fresh)) 1, - rtac th 1])) + resolve_tac ctxt [th] 1])) in Simplifier.simplify (put_simpset HOL_basic_ss context'' addsimps rpi1_pi2_eqs) th' @@ -1924,12 +1930,13 @@ in Goal.prove context'' [] [] (HOLogic.mk_Trueprop (fresh_const aT T $ a $ y)) - (fn _ => EVERY - (rtac (nth (nth rec_fresh_thms l) k) 1 :: - map (fn th => rtac th 1) + (fn {context = ctxt, ...} => EVERY + (resolve_tac ctxt [nth (nth rec_fresh_thms l) k] 1 :: + map (fn th => resolve_tac ctxt [th] 1) (snd (nth finite_thss l)) @ - [rtac rec_prem 1, rtac ih 1, - REPEAT_DETERM (resolve_tac context fresh_prems 1)])) + [resolve_tac ctxt [rec_prem] 1, + resolve_tac ctxt [ih] 1, + REPEAT_DETERM (resolve_tac ctxt fresh_prems 1)])) end) atoms end) (rec_prems1 ~~ ihs); @@ -1954,8 +1961,9 @@ (HOLogic.mk_Trueprop (fresh_const aT rT $ fold_rev (mk_perm []) (rpi2 @ pi1) a $ fold_rev (mk_perm []) (rpi2 @ pi1) rhs')) - (fn _ => simp_tac (put_simpset HOL_ss context'' addsimps fresh_bij) 1 THEN - rtac th 1) + (fn {context = ctxt, ...} => + simp_tac (put_simpset HOL_ss context'' addsimps fresh_bij) 1 THEN + resolve_tac ctxt [th] 1) in Goal.prove context'' [] [] (HOLogic.mk_Trueprop (fresh_const aT rT $ b $ lhs')) @@ -2048,14 +2056,14 @@ val prems' = flat finite_premss @ finite_ctxt_prems @ rec_prems @ rec_prems' @ map (subst_atomic ps) prems; fun solve ctxt rules prems = resolve_tac ctxt rules THEN_ALL_NEW - (resolve_tac ctxt prems THEN_ALL_NEW atac) + (resolve_tac ctxt prems THEN_ALL_NEW assume_tac ctxt) in Goal.prove_global_future thy12 [] (map (augment_sort thy12 fs_cp_sort) prems') (augment_sort thy12 fs_cp_sort concl') (fn {context = ctxt, prems} => EVERY [rewrite_goals_tac ctxt reccomb_defs, - rtac @{thm the1_equality} 1, + resolve_tac ctxt @{thms the1_equality} 1, solve ctxt rec_unique_thms prems 1, resolve_tac ctxt rec_intrs 1, REPEAT (solve ctxt (prems @ rec_total_thms) prems 1)]) diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Sat Jul 18 20:54:56 2015 +0200 @@ -79,8 +79,8 @@ in fn st => (cut_inst_tac_term' ctxt [(x,s)] exists_fresh' 1 THEN - rtac fs_name_thm 1 THEN - etac exE 1) st + resolve_tac ctxt [fs_name_thm] 1 THEN + eresolve_tac ctxt [exE] 1) st handle List.Empty => all_tac st (* if we collected no variables then we do nothing *) end) 1; @@ -163,8 +163,8 @@ (* The tactics which solve the subgoals generated by the conditionnal rewrite rule. *) val post_rewrite_tacs = - [rtac pt_name_inst, - rtac at_name_inst, + [resolve_tac ctxt [pt_name_inst], + resolve_tac ctxt [at_name_inst], TRY o SOLVED' (NominalPermeq.finite_guess_tac simp_ctxt), inst_fresh vars params THEN' (TRY o SOLVED' (NominalPermeq.fresh_guess_tac simp_ctxt)) THEN' diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Nominal/nominal_induct.ML --- a/src/HOL/Nominal/nominal_induct.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Nominal/nominal_induct.ML Sat Jul 18 20:54:56 2015 +0200 @@ -121,7 +121,7 @@ (finish_rule (Induct.internalize ctxt more_consumes rule)) i st' |> Seq.maps (fn rule' => CASES (rule_cases ctxt rule' cases) - (rtac (rename_params_rule false [] rule') i THEN + (resolve_tac ctxt [rename_params_rule false [] rule'] i THEN PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))) THEN_ALL_NEW_CASES ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac ctxt) diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Sat Jul 18 20:54:56 2015 +0200 @@ -104,8 +104,8 @@ | inst_conj_all _ _ _ _ _ = NONE; fun inst_conj_all_tac ctxt k = EVERY - [TRY (EVERY [etac conjE 1, rtac conjI 1, atac 1]), - REPEAT_DETERM_N k (etac allE 1), + [TRY (EVERY [eresolve_tac ctxt [conjE] 1, resolve_tac ctxt [conjI] 1, assume_tac ctxt 1]), + REPEAT_DETERM_N k (eresolve_tac ctxt [allE] 1), simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm id_apply}]) 1]; fun map_term f t u = (case f t u of @@ -129,9 +129,9 @@ val prop = Thm.prop_of th; fun prove t = Goal.prove ctxt [] [] t (fn _ => - EVERY [cut_facts_tac [th] 1, etac rev_mp 1, + EVERY [cut_facts_tac [th] 1, eresolve_tac ctxt [rev_mp] 1, REPEAT_DETERM (FIRSTGOAL (resolve_tac ctxt monos)), - REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]) + REPEAT_DETERM (resolve_tac ctxt [impI] 1 THEN (assume_tac ctxt 1 ORELSE tac))]) in Option.map prove (map_term f prop (the_default prop opt)) end; val eta_contract_cterm = Thm.dest_arg o Thm.cprop_of o Thm.eta_conversion; @@ -300,19 +300,20 @@ resolve_tac ctxt fs_atoms 1]); val (([(_, cx)], ths), ctxt') = Obtain.result (fn ctxt' => EVERY - [etac exE 1, + [eresolve_tac ctxt' [exE] 1, full_simp_tac (put_simpset HOL_ss ctxt' addsimps (fresh_prod :: fresh_atm)) 1, full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]) 1, - REPEAT (etac conjE 1)]) + REPEAT (eresolve_tac ctxt [conjE] 1)]) [ex] ctxt in (freshs1 @ [Thm.term_of cx], freshs2 @ ths, ctxt') end; fun mk_ind_proof ctxt' thss = Goal.prove ctxt' [] prems' concl' (fn {prems = ihyps, context = ctxt} => let val th = Goal.prove ctxt [] [] concl (fn {context, ...} => - rtac raw_induct 1 THEN + resolve_tac context [raw_induct] 1 THEN EVERY (maps (fn ((((_, bvars, oprems, _), vc_compat_ths), ihyp), (vs, ihypt)) => - [REPEAT (rtac allI 1), simp_tac (put_simpset eqvt_ss context) 1, + [REPEAT (resolve_tac context [allI] 1), + simp_tac (put_simpset eqvt_ss context) 1, SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} => let val (params', (pis, z)) = @@ -354,7 +355,7 @@ if null (preds_of ps t) then (SOME th, mk_pi th) else (map_thm ctxt' (split_conj (K o I) names) - (etac conjunct1 1) monos NONE th, + (eresolve_tac ctxt' [conjunct1] 1) monos NONE th, mk_pi (the (map_thm ctxt' (inst_conj_all names ps (rev pis'')) (inst_conj_all_tac ctxt' (length pis'')) monos (SOME t) th)))) (gprems ~~ oprems)) |>> map_filter I; @@ -370,7 +371,7 @@ (bop (fold_rev (NominalDatatype.mk_perm []) pis lhs) (fold_rev (NominalDatatype.mk_perm []) pis rhs))) (fn _ => simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps - (fresh_bij @ perm_bij)) 1 THEN rtac th' 1) + (fresh_bij @ perm_bij)) 1 THEN resolve_tac ctxt' [th'] 1) in Simplifier.simplify (put_simpset eqvt_ss ctxt'' addsimps fresh_atm) th'' end) vc_compat_ths; val vc_compat_ths'' = NominalDatatype.mk_not_sym vc_compat_ths'; @@ -382,7 +383,8 @@ val th = Goal.prove ctxt'' [] [] (HOLogic.mk_Trueprop (list_comb (P $ hd ts, map (fold (NominalDatatype.mk_perm []) pis') (tl ts)))) - (fn _ => EVERY ([simp_tac (put_simpset eqvt_ss ctxt'') 1, rtac ihyp' 1, + (fn _ => EVERY ([simp_tac (put_simpset eqvt_ss ctxt'') 1, + resolve_tac ctxt'' [ihyp'] 1, REPEAT_DETERM_N (Thm.nprems_of ihyp - length gprems) (simp_tac swap_simps_simpset 1), REPEAT_DETERM_N (length gprems) @@ -398,9 +400,10 @@ in resolve_tac ctxt' final' 1 end) context 1]) (prems ~~ thss ~~ ihyps ~~ prems''))) in - cut_facts_tac [th] 1 THEN REPEAT (etac conjE 1) THEN + cut_facts_tac [th] 1 THEN REPEAT (eresolve_tac ctxt [conjE] 1) THEN REPEAT (REPEAT (resolve_tac ctxt [conjI, impI] 1) THEN - etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN + eresolve_tac ctxt [impE] 1 THEN assume_tac ctxt 1 THEN + REPEAT (eresolve_tac ctxt @{thms allE_Nil} 1) THEN asm_full_simp_tac ctxt 1) end) |> singleton (Proof_Context.export ctxt' ctxt); @@ -466,11 +469,11 @@ prems') = (name, Goal.prove ctxt' [] (prem :: prems') concl (fn {prems = hyp :: hyps, context = ctxt1} => - EVERY (rtac (hyp RS elim) 1 :: + EVERY (resolve_tac ctxt1 [hyp RS elim] 1 :: map (fn (((_, vc_compat_ths), case_hyp), (_, qs, is, _)) => SUBPROOF (fn {prems = case_hyps, params, context = ctxt2, concl, ...} => if null qs then - rtac (first_order_mrs case_hyps case_hyp) 1 + resolve_tac ctxt2 [first_order_mrs case_hyps case_hyp] 1 else let val params' = map (Thm.term_of o #2 o nth (rev params)) is; @@ -518,8 +521,8 @@ (Drule.strip_imp_concl (hd (cprems_of case_hyp))), obj); val th = Goal.prove ctxt3 [] [] (Thm.term_of concl) (fn {context = ctxt4, ...} => - rtac (Thm.instantiate inst case_hyp) 1 THEN - SUBPROOF (fn {prems = fresh_hyps, ...} => + resolve_tac ctxt4 [Thm.instantiate inst case_hyp] 1 THEN + SUBPROOF (fn {context = ctxt5, prems = fresh_hyps, ...} => let val fresh_hyps' = NominalDatatype.mk_not_sym fresh_hyps; val case_simpset = cases_eqvt_simpset addsimps freshs2' @ @@ -532,8 +535,8 @@ val case_hyps' = hyps1' @ hyps2' in simp_tac case_simpset 1 THEN - REPEAT_DETERM (TRY (rtac conjI 1) THEN - resolve_tac ctxt4 case_hyps' 1) + REPEAT_DETERM (TRY (resolve_tac ctxt5 [conjI] 1) THEN + resolve_tac ctxt5 case_hyps' 1) end) ctxt4 1) val final = Proof_Context.export ctxt3 ctxt2 [th] in resolve_tac ctxt2 final 1 end) ctxt1 1) @@ -629,13 +632,13 @@ val res = SUBPROOF (fn {context = ctxt'', prems, params, ...} => let val prems' = map (fn th => the_default th (map_thm ctxt'' - (split_conj (K I) names) (etac conjunct2 1) monos NONE th)) prems; + (split_conj (K I) names) (eresolve_tac ctxt'' [conjunct2] 1) monos NONE th)) prems; val prems'' = map (fn th => Simplifier.simplify eqvt_simpset (mk_perm_bool (Thm.global_cterm_of thy pi) th)) prems'; val intr' = Drule.cterm_instantiate (map (Thm.global_cterm_of thy) vs ~~ map (Thm.global_cterm_of thy o NominalDatatype.mk_perm [] pi o Thm.term_of o #2) params) intr - in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac ctxt'' prems'')) 1 + in (resolve_tac ctxt'' [intr'] THEN_ALL_NEW (TRY o resolve_tac ctxt'' prems'')) 1 end) ctxt' 1 st in case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of @@ -655,7 +658,7 @@ HOLogic.mk_imp (p, list_comb (h, ts1 @ map (NominalDatatype.mk_perm [] pi') ts2)) end) ps))) - (fn _ => EVERY (rtac raw_induct 1 :: map (fn intr_vs => + (fn _ => EVERY (resolve_tac ctxt' [raw_induct] 1 :: map (fn intr_vs => full_simp_tac eqvt_simpset 1 THEN eqvt_tac pi' intr_vs) intrs')) |> singleton (Proof_Context.export ctxt' ctxt))) diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Sat Jul 18 20:54:56 2015 +0200 @@ -109,8 +109,8 @@ | inst_conj_all _ _ _ _ _ = NONE; fun inst_conj_all_tac ctxt k = EVERY - [TRY (EVERY [etac conjE 1, rtac conjI 1, atac 1]), - REPEAT_DETERM_N k (etac allE 1), + [TRY (EVERY [eresolve_tac ctxt [conjE] 1, resolve_tac ctxt [conjI] 1, assume_tac ctxt 1]), + REPEAT_DETERM_N k (eresolve_tac ctxt [allE] 1), simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm id_apply}]) 1]; fun map_term f t u = (case f t u of @@ -134,9 +134,9 @@ val prop = Thm.prop_of th; fun prove t = Goal.prove ctxt [] [] t (fn _ => - EVERY [cut_facts_tac [th] 1, etac rev_mp 1, + EVERY [cut_facts_tac [th] 1, eresolve_tac ctxt [rev_mp] 1, REPEAT_DETERM (FIRSTGOAL (resolve_tac ctxt monos)), - REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))]) + REPEAT_DETERM (resolve_tac ctxt [impI] 1 THEN (assume_tac ctxt 1 ORELSE tac))]) in Option.map prove (map_term f prop (the_default prop opt)) end; fun abs_params params t = @@ -321,11 +321,11 @@ ([at_inst, fin, fs_atom] MRS @{thm at_set_avoiding}); val (([(_, cx)], th1 :: th2 :: ths), ctxt') = Obtain.result (fn ctxt' => EVERY - [rtac avoid_th 1, + [resolve_tac ctxt' [avoid_th] 1, full_simp_tac (put_simpset HOL_ss ctxt' addsimps [@{thm fresh_star_prod_set}]) 1, full_simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [@{thm id_apply}]) 1, rotate_tac 1 1, - REPEAT (etac conjE 1)]) + REPEAT (eresolve_tac ctxt' [conjE] 1)]) [] ctxt; val (Ts1, _ :: Ts2) = take_prefix (not o equal T) (map snd sets); val pTs = map NominalAtoms.mk_permT (Ts1 @ Ts2); @@ -348,10 +348,10 @@ fun mk_ind_proof ctxt' thss = Goal.prove ctxt' [] prems' concl' (fn {prems = ihyps, context = ctxt} => let val th = Goal.prove ctxt [] [] concl (fn {context, ...} => - rtac raw_induct 1 THEN + resolve_tac ctxt [raw_induct] 1 THEN EVERY (maps (fn (((((_, sets, oprems, _), vc_compat_ths), vc_compat_vs), ihyp), vs_ihypt) => - [REPEAT (rtac allI 1), simp_tac (put_simpset eqvt_ss context) 1, + [REPEAT (resolve_tac ctxt [allI] 1), simp_tac (put_simpset eqvt_ss context) 1, SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} => let val (cparams', (pis, z)) = @@ -366,7 +366,7 @@ if null (preds_of ps t) then SOME th else map_thm ctxt' (split_conj (K o I) names) - (etac conjunct1 1) monos NONE th) + (eresolve_tac ctxt' [conjunct1] 1) monos NONE th) (gprems ~~ oprems); val vc_compat_ths' = map2 (fn th => fn p => let @@ -378,7 +378,7 @@ (HOLogic.mk_Trueprop (list_comb (h, map (fold_rev (NominalDatatype.mk_perm []) pis) ts))) (fn _ => simp_tac (put_simpset HOL_basic_ss ctxt' addsimps - (fresh_star_bij @ finite_ineq)) 1 THEN rtac th' 1) + (fresh_star_bij @ finite_ineq)) 1 THEN resolve_tac ctxt' [th'] 1) end) vc_compat_ths vc_compat_vs; val (vc_compat_ths1, vc_compat_ths2) = chop (length vc_compat_ths - length sets) vc_compat_ths'; @@ -416,8 +416,9 @@ val th = Goal.prove ctxt'' [] [] (HOLogic.mk_Trueprop (list_comb (P $ hd ts, map (fold_rev (NominalDatatype.mk_perm []) pis') (tl ts)))) - (fn _ => EVERY ([simp_tac (put_simpset eqvt_ss ctxt'') 1, rtac ihyp' 1] @ - map (fn th => rtac th 1) fresh_ths3 @ + (fn _ => EVERY ([simp_tac (put_simpset eqvt_ss ctxt'') 1, + resolve_tac ctxt'' [ihyp'] 1] @ + map (fn th => resolve_tac ctxt'' [th] 1) fresh_ths3 @ [REPEAT_DETERM_N (length gprems) (simp_tac (put_simpset HOL_basic_ss ctxt'' addsimps [inductive_forall_def'] @@ -431,9 +432,10 @@ in resolve_tac ctxt' final' 1 end) context 1]) (prems ~~ thss ~~ vc_compat' ~~ ihyps ~~ prems''))) in - cut_facts_tac [th] 1 THEN REPEAT (etac conjE 1) THEN + cut_facts_tac [th] 1 THEN REPEAT (eresolve_tac ctxt' [conjE] 1) THEN REPEAT (REPEAT (resolve_tac ctxt' [conjI, impI] 1) THEN - etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN + eresolve_tac ctxt' [impE] 1 THEN + assume_tac ctxt' 1 THEN REPEAT (eresolve_tac ctxt' @{thms allE_Nil} 1) THEN asm_full_simp_tac ctxt 1) end) |> fresh_postprocess ctxt' |> diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Nominal/nominal_permeq.ML Sat Jul 18 20:54:56 2015 +0200 @@ -218,7 +218,7 @@ fun perm_compose_tac ctxt i = ("analysing permutation compositions on the lhs", fn st => EVERY - [rtac trans i, + [resolve_tac ctxt [trans] i, asm_full_simp_tac (empty_simpset ctxt addsimprocs [perm_compose_simproc]) i, asm_full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [perm_aux_fold]) i] st); @@ -230,14 +230,15 @@ (* pi o f = rhs *) (* is transformed to *) (* %x. pi o (f ((rev pi) o x)) = rhs *) -fun unfold_perm_fun_def_tac i = +fun unfold_perm_fun_def_tac ctxt i = ("unfolding of permutations on functions", - rtac (perm_fun_def RS meta_eq_to_obj_eq RS trans) i) + resolve_tac ctxt [perm_fun_def RS meta_eq_to_obj_eq RS trans] i) (* applies the ext-rule such that *) (* *) (* f = g goes to /\x. f x = g x *) -fun ext_fun_tac i = ("extensionality expansion of functions", rtac @{thm ext} i); +fun ext_fun_tac ctxt i = + ("extensionality expansion of functions", resolve_tac ctxt @{thms ext} i); (* perm_extend_simp_tac_i is perm_simp plus additional tactics *) @@ -248,13 +249,14 @@ let fun perm_extend_simp_tac_aux tactical ctxt n = if n=0 then K all_tac else DETERM o - (FIRST'[fn i => tactical ctxt ("splitting conjunctions on the rhs", rtac conjI i), - fn i => tactical ctxt (perm_simp asm_full_simp_tac ctxt i), - fn i => tactical ctxt (perm_compose_tac ctxt i), - fn i => tactical ctxt (apply_cong_tac ctxt i), - fn i => tactical ctxt (unfold_perm_fun_def_tac i), - fn i => tactical ctxt (ext_fun_tac i)] - THEN_ALL_NEW (TRY o (perm_extend_simp_tac_aux tactical ctxt (n-1)))) + (FIRST' + [fn i => tactical ctxt ("splitting conjunctions on the rhs", resolve_tac ctxt [conjI] i), + fn i => tactical ctxt (perm_simp asm_full_simp_tac ctxt i), + fn i => tactical ctxt (perm_compose_tac ctxt i), + fn i => tactical ctxt (apply_cong_tac ctxt i), + fn i => tactical ctxt (unfold_perm_fun_def_tac ctxt i), + fn i => tactical ctxt (ext_fun_tac ctxt i)] + THEN_ALL_NEW (TRY o (perm_extend_simp_tac_aux tactical ctxt (n-1)))) in perm_extend_simp_tac_aux tactical ctxt 10 end; @@ -266,10 +268,10 @@ val simps = [supports_def, Thm.symmetric fresh_def, fresh_prod] in EVERY [tactical ctxt ("unfolding of supports ", simp_tac (put_simpset HOL_basic_ss ctxt addsimps simps) i), - tactical ctxt ("stripping of foralls ", REPEAT_DETERM (rtac allI i)), - tactical ctxt ("geting rid of the imps ", rtac impI i), - tactical ctxt ("eliminating conjuncts ", REPEAT_DETERM (etac conjE i)), - tactical ctxt ("applying eqvt_simp ", eqvt_simp_tac_gen_i asm_full_simp_tac tactical ctxt i )] + tactical ctxt ("stripping of foralls ", REPEAT_DETERM (resolve_tac ctxt [allI] i)), + tactical ctxt ("geting rid of the imps ", resolve_tac ctxt [impI] i), + tactical ctxt ("eliminating conjuncts ", REPEAT_DETERM (eresolve_tac ctxt [conjE] i)), + tactical ctxt ("applying eqvt_simp ", eqvt_simp_tac_gen_i asm_full_simp_tac tactical ctxt i)] end; diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Nominal/nominal_thmdecls.ML --- a/src/HOL/Nominal/nominal_thmdecls.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Nominal/nominal_thmdecls.ML Sat Jul 18 20:54:56 2015 +0200 @@ -58,12 +58,12 @@ val mypifree = Thm.global_cterm_of thy (Const (@{const_name "rev"}, T --> T) $ pi') val perm_pi_simp = Global_Theory.get_thms thy "perm_pi_simp" in - EVERY1 [tactic ctxt ("iffI applied", rtac @{thm iffI}), - tactic ctxt ("remove pi with perm_boolE", dtac @{thm perm_boolE}), - tactic ctxt ("solve with orig_thm", etac orig_thm), + EVERY1 [tactic ctxt ("iffI applied", resolve_tac ctxt @{thms iffI}), + tactic ctxt ("remove pi with perm_boolE", dresolve_tac ctxt @{thms perm_boolE}), + tactic ctxt ("solve with orig_thm", eresolve_tac ctxt [orig_thm]), tactic ctxt ("applies orig_thm instantiated with rev pi", - dtac (Drule.cterm_instantiate [(mypi,mypifree)] orig_thm)), - tactic ctxt ("getting rid of the pi on the right", rtac @{thm perm_boolI}), + dresolve_tac ctxt [Drule.cterm_instantiate [(mypi,mypifree)] orig_thm]), + tactic ctxt ("getting rid of the pi on the right", resolve_tac ctxt @{thms perm_boolI}), tactic ctxt ("getting rid of all remaining perms", full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps perm_pi_simp))] end; diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Prolog/prolog.ML --- a/src/HOL/Prolog/prolog.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Prolog/prolog.ML Sat Jul 18 20:54:56 2015 +0200 @@ -74,7 +74,7 @@ (*val hyp_resolve_tac = Subgoal.FOCUS_PREMS (fn {prems, ...} => resolve_tac (maps atomizeD prems) 1); -- is nice, but cannot instantiate unknowns in the assumptions *) -val hyp_resolve_tac = SUBGOAL (fn (subgoal, i) => +fun hyp_resolve_tac ctxt = SUBGOAL (fn (subgoal, i) => let fun ap (Const(@{const_name All},_)$Abs(_,_,t))=(case ap t of (k,a,t) => (k+1,a ,t)) | ap (Const(@{const_name HOL.implies},_)$_$t) =(case ap t of (k,_,t) => (k,true ,t)) @@ -91,9 +91,9 @@ val concl = HOLogic.dest_Trueprop (Logic.strip_assums_concl subgoal); fun drot_tac k i = DETERM (rotate_tac k i); fun spec_tac 0 i = all_tac - | spec_tac k i = EVERY' [dtac spec, drot_tac ~1, spec_tac (k-1)] i; + | spec_tac k i = EVERY' [dresolve_tac ctxt [spec], drot_tac ~1, spec_tac (k-1)] i; fun dup_spec_tac k i = if k = 0 then all_tac else EVERY' - [DETERM o (etac all_dupE), drot_tac ~2, spec_tac (k-1)] i; + [DETERM o (eresolve_tac ctxt [all_dupE]), drot_tac ~2, spec_tac (k-1)] i; fun same_head _ (Const (x,_)) (Const (y,_)) = x = y | same_head k (s$_) (t$_) = same_head k s t | same_head k (Bound i) (Bound j) = i = j + k @@ -101,10 +101,10 @@ fun mapn f n [] = [] | mapn f n (x::xs) = f n x::mapn f (n+1) xs; fun pres_tac (k,arrow,t) n i = drot_tac n i THEN ( - if same_head k t concl - then dup_spec_tac k i THEN - (if arrow then etac mp i THEN drot_tac (~n) i else atac i) - else no_tac); + if same_head k t concl + then dup_spec_tac k i THEN + (if arrow then eresolve_tac ctxt [mp] i THEN drot_tac (~n) i else assume_tac ctxt i) + else no_tac); val ptacs = mapn (fn n => fn t => pres_tac (ap (HOLogic.dest_Trueprop t)) n i) 0 prems; in Library.foldl (op APPEND) (no_tac, ptacs) end); @@ -112,16 +112,16 @@ fun ptac ctxt prog = let val proga = maps (atomizeD ctxt) prog (* atomize the prog *) in (REPEAT_DETERM1 o FIRST' [ - rtac TrueI, (* "True" *) - rtac conjI, (* "[| P; Q |] ==> P & Q" *) - rtac allI, (* "(!!x. P x) ==> ! x. P x" *) - rtac exI, (* "P x ==> ? x. P x" *) - rtac impI THEN' (* "(P ==> Q) ==> P --> Q" *) + resolve_tac ctxt [TrueI], (* "True" *) + resolve_tac ctxt [conjI], (* "[| P; Q |] ==> P & Q" *) + resolve_tac ctxt [allI], (* "(!!x. P x) ==> ! x. P x" *) + resolve_tac ctxt [exI], (* "P x ==> ? x. P x" *) + resolve_tac ctxt [impI] THEN' (* "(P ==> Q) ==> P --> Q" *) asm_full_simp_tac (put_simpset atomize_ss ctxt) THEN' (* atomize the asms *) - (REPEAT_DETERM o (etac conjE)) (* split the asms *) + (REPEAT_DETERM o (eresolve_tac ctxt [conjE])) (* split the asms *) ]) ORELSE' resolve_tac ctxt [disjI1,disjI2] (* "P ==> P | Q","Q ==> P | Q"*) - ORELSE' ((resolve_tac ctxt proga APPEND' hyp_resolve_tac) + ORELSE' ((resolve_tac ctxt proga APPEND' hyp_resolve_tac ctxt) THEN' (fn _ => check_HOHH_tac2)) end; diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/SET_Protocol/Cardholder_Registration.thy --- a/src/HOL/SET_Protocol/Cardholder_Registration.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy Sat Jul 18 20:54:56 2015 +0200 @@ -540,7 +540,7 @@ (fn i => EVERY [forward_tac ctxt @{thms Gets_certificate_valid} i, assume_tac ctxt i, - etac conjE i, REPEAT (hyp_subst_tac ctxt i)])) + eresolve_tac ctxt [conjE] i, REPEAT (hyp_subst_tac ctxt i)])) *} text{*The @{text "(no_asm)"} attribute is essential, since it retains diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/SET_Protocol/Event_SET.thy --- a/src/HOL/SET_Protocol/Event_SET.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/SET_Protocol/Event_SET.thy Sat Jul 18 20:54:56 2015 +0200 @@ -183,7 +183,7 @@ ML {* fun analz_mono_contra_tac ctxt = - rtac @{thm analz_impI} THEN' + resolve_tac ctxt @{thms analz_impI} THEN' REPEAT1 o (dresolve_tac ctxt @{thms analz_mono_contra}) THEN' mp_tac ctxt *} diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/SPARK/Tools/spark_vcs.ML --- a/src/HOL/SPARK/Tools/spark_vcs.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML Sat Jul 18 20:54:56 2015 +0200 @@ -206,22 +206,22 @@ val UNIV_eq = Goal.prove lthy [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (HOLogic.mk_UNIV T, HOLogic.mk_set T cs))) - (fn _ => - rtac @{thm subset_antisym} 1 THEN - rtac @{thm subsetI} 1 THEN - Old_Datatype_Aux.exh_tac lthy (K (#exhaust (BNF_LFP_Compat.the_info - (Proof_Context.theory_of lthy) [BNF_LFP_Compat.Keep_Nesting] tyname'))) 1 THEN - ALLGOALS (asm_full_simp_tac lthy)); + (fn {context = ctxt, ...} => + resolve_tac ctxt @{thms subset_antisym} 1 THEN + resolve_tac ctxt @{thms subsetI} 1 THEN + Old_Datatype_Aux.exh_tac ctxt (K (#exhaust (BNF_LFP_Compat.the_info + (Proof_Context.theory_of ctxt) [BNF_LFP_Compat.Keep_Nesting] tyname'))) 1 THEN + ALLGOALS (asm_full_simp_tac ctxt)); val finite_UNIV = Goal.prove lthy [] [] (HOLogic.mk_Trueprop (Const (@{const_name finite}, HOLogic.mk_setT T --> HOLogic.boolT) $ HOLogic.mk_UNIV T)) - (fn _ => simp_tac (lthy addsimps [UNIV_eq]) 1); + (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [UNIV_eq]) 1); val card_UNIV = Goal.prove lthy [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (card, HOLogic.mk_number HOLogic.natT k))) - (fn _ => simp_tac (lthy addsimps [UNIV_eq]) 1); + (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [UNIV_eq]) 1); val range_pos = Goal.prove lthy [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq @@ -232,20 +232,20 @@ HOLogic.intT --> HOLogic.mk_setT HOLogic.intT) $ HOLogic.mk_number HOLogic.intT 0 $ (@{term int} $ card)))) - (fn _ => - simp_tac (lthy addsimps [card_UNIV]) 1 THEN - simp_tac (lthy addsimps [UNIV_eq, def1]) 1 THEN - rtac @{thm subset_antisym} 1 THEN - simp_tac lthy 1 THEN - rtac @{thm subsetI} 1 THEN - asm_full_simp_tac (lthy addsimps @{thms interval_expand} + (fn {context = ctxt, ...} => + simp_tac (ctxt addsimps [card_UNIV]) 1 THEN + simp_tac (ctxt addsimps [UNIV_eq, def1]) 1 THEN + resolve_tac ctxt @{thms subset_antisym} 1 THEN + simp_tac ctxt 1 THEN + resolve_tac ctxt @{thms subsetI} 1 THEN + asm_full_simp_tac (ctxt addsimps @{thms interval_expand} delsimps @{thms atLeastLessThan_iff}) 1); val lthy' = Class.prove_instantiation_instance (fn ctxt => Class.intro_classes_tac ctxt [] THEN - rtac finite_UNIV 1 THEN - rtac range_pos 1 THEN + resolve_tac ctxt [finite_UNIV] 1 THEN + resolve_tac ctxt [range_pos] 1 THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps [def3]) 1 THEN simp_tac (put_simpset HOL_basic_ss ctxt addsimps [def2]) 1) lthy; @@ -254,23 +254,24 @@ val n = HOLogic.mk_number HOLogic.intT i; val th = Goal.prove lthy' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (p $ c, n))) - (fn _ => simp_tac (lthy' addsimps [def1]) 1); + (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [def1]) 1); val th' = Goal.prove lthy' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (v $ n, c))) - (fn _ => - rtac (@{thm inj_pos} RS @{thm injD}) 1 THEN - simp_tac (lthy' addsimps [@{thm pos_val}, range_pos, card_UNIV, th]) 1) + (fn {context = ctxt, ...} => + resolve_tac ctxt [@{thm inj_pos} RS @{thm injD}] 1 THEN + simp_tac (ctxt addsimps [@{thm pos_val}, range_pos, card_UNIV, th]) 1) in (th, th') end) cs); val first_el = Goal.prove lthy' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (@{const_name first_el}, T), hd cs))) - (fn _ => simp_tac (lthy' addsimps [@{thm first_el_def}, hd val_eqs]) 1); + (fn {context = ctxt, ...} => simp_tac (ctxt addsimps [@{thm first_el_def}, hd val_eqs]) 1); val last_el = Goal.prove lthy' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (Const (@{const_name last_el}, T), List.last cs))) - (fn _ => simp_tac (lthy' addsimps [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1); + (fn {context = ctxt, ...} => + simp_tac (ctxt addsimps [@{thm last_el_def}, List.last val_eqs, card_UNIV]) 1); in lthy' |> Local_Theory.note diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Statespace/distinct_tree_prover.ML --- a/src/HOL/Statespace/distinct_tree_prover.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Sat Jul 18 20:54:56 2015 +0200 @@ -345,7 +345,7 @@ Const (@{const_name Trueprop}, _) $ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ x $ y)) => (case get_fst_success (neq_x_y ctxt x y) names of - SOME neq => rtac neq i + SOME neq => resolve_tac ctxt [neq] i | NONE => no_tac) | _ => no_tac)) diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Statespace/state_fun.ML Sat Jul 18 20:54:56 2015 +0200 @@ -248,7 +248,7 @@ val eq1 = Goal.prove ctxt0 [] [] (Logic.list_all (vars, Logic.mk_equals (trm, trm'))) - (fn _ => rtac meta_ext 1 THEN simp_tac ctxt1 1); + (fn _ => resolve_tac ctxt0 [meta_ext] 1 THEN simp_tac ctxt1 1); val eq2 = Simplifier.asm_full_rewrite ctxt2 (Thm.dest_equals_rhs (Thm.cprop_of eq1)); in SOME (Thm.transitive eq1 eq2) end | _ => NONE) diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Statespace/state_space.ML Sat Jul 18 20:54:56 2015 +0200 @@ -204,7 +204,7 @@ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ (x as Free _) $ (y as Free _))) => (case neq_x_y ctxt x y of - SOME neq => rtac neq i + SOME neq => resolve_tac ctxt [neq] i | NONE => no_tac) | _ => no_tac)); @@ -222,7 +222,7 @@ let val distinct_thm = Proof_Context.get_thm ctxt dist_thm_name; val rule = DistinctTreeProver.distinct_implProver ctxt distinct_thm goal; - in rtac rule i end); + in resolve_tac ctxt [rule] i end); fun tac ctxt = Locale.intro_locales_tac true ctxt [] THEN ALLGOALS (solve_tac ctxt); diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/TLA/Memory/MemoryImplementation.thy --- a/src/HOL/TLA/Memory/MemoryImplementation.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Sat Jul 18 20:54:56 2015 +0200 @@ -227,7 +227,7 @@ val config_fast_solver = Attrib.setup_config_bool @{binding fast_solver} (K false); val fast_solver = mk_solver "fast_solver" (fn ctxt => if Config.get ctxt config_fast_solver - then assume_tac ctxt ORELSE' (etac notE) + then assume_tac ctxt ORELSE' (eresolve_tac ctxt [notE]) else K no_tac); \ @@ -797,7 +797,7 @@ ML \ fun split_idle_tac ctxt = SELECT_GOAL - (TRY (rtac @{thm actionI} 1) THEN + (TRY (resolve_tac ctxt @{thms actionI} 1) THEN Induct_Tacs.case_tac ctxt "(s,t) \ unchanged (e p, c p, r p, m p, rmhist!p)" [] NONE 1 THEN rewrite_goals_tac ctxt @{thms action_rews} THEN forward_tac ctxt [temp_use ctxt @{thm Step1_4_7}] 1 THEN diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/TLA/TLA.thy --- a/src/HOL/TLA/TLA.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/TLA/TLA.thy Sat Jul 18 20:54:56 2015 +0200 @@ -284,23 +284,24 @@ lemma box_thin: "\ sigma \ \F; PROP W \ \ PROP W" . ML \ -fun merge_box_tac i = - REPEAT_DETERM (EVERY [etac @{thm box_conjE} i, atac i, etac @{thm box_thin} i]) +fun merge_box_tac ctxt i = + REPEAT_DETERM (EVERY [eresolve_tac ctxt @{thms box_conjE} i, assume_tac ctxt i, + eresolve_tac ctxt @{thms box_thin} i]) fun merge_temp_box_tac ctxt i = - REPEAT_DETERM (EVERY [etac @{thm box_conjE_temp} i, atac i, + REPEAT_DETERM (EVERY [eresolve_tac ctxt @{thms box_conjE_temp} i, assume_tac ctxt i, Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "behavior")] [] @{thm box_thin} i]) fun merge_stp_box_tac ctxt i = - REPEAT_DETERM (EVERY [etac @{thm box_conjE_stp} i, atac i, + REPEAT_DETERM (EVERY [eresolve_tac ctxt @{thms box_conjE_stp} i, assume_tac ctxt i, Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state")] [] @{thm box_thin} i]) fun merge_act_box_tac ctxt i = - REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i, + REPEAT_DETERM (EVERY [eresolve_tac ctxt @{thms box_conjE_act} i, assume_tac ctxt i, Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state * state")] [] @{thm box_thin} i]) \ -method_setup merge_box = \Scan.succeed (K (SIMPLE_METHOD' merge_box_tac))\ +method_setup merge_box = \Scan.succeed (SIMPLE_METHOD' o merge_box_tac)\ method_setup merge_temp_box = \Scan.succeed (SIMPLE_METHOD' o merge_temp_box_tac)\ method_setup merge_stp_box = \Scan.succeed (SIMPLE_METHOD' o merge_stp_box_tac)\ method_setup merge_act_box = \Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac)\ @@ -577,9 +578,9 @@ SELECT_GOAL (EVERY [auto_tac ctxt, - TRY (merge_box_tac 1), - rtac (temp_use ctxt @{thm INV1}) 1, (* fail if the goal is not a box *) - TRYALL (etac @{thm Stable})]); + TRY (merge_box_tac ctxt 1), + resolve_tac ctxt [temp_use ctxt @{thm INV1}] 1, (* fail if the goal is not a box *) + TRYALL (eresolve_tac ctxt @{thms Stable})]); (* auto_inv_tac applies inv_tac and then tries to attack the subgoals in simple cases it may be able to handle goals like \ MyProg \ \Inv. diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML --- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML Sat Jul 18 20:54:56 2015 +0200 @@ -975,9 +975,9 @@ raise SKELETON (*FIXME or classify it as a Caboose: TRY (HEADGOAL atac) *) else case hd skel of - Assumed => TRY (HEADGOAL atac) THEN rest (tl skel) memo - | Caboose => TRY (HEADGOAL atac) - | Unconjoin => rtac @{thm conjI} 1 THEN rest (tl skel) memo + Assumed => TRY (HEADGOAL (assume_tac ctxt)) THEN rest (tl skel) memo + | Caboose => TRY (HEADGOAL (assume_tac ctxt)) + | Unconjoin => resolve_tac ctxt @{thms conjI} 1 THEN rest (tl skel) memo | Split (split_node, solved_node, antes) => let val split_fmla = node_info (#meta pannot) #fmla split_node @@ -993,13 +993,13 @@ val split_thm = simulate_split ctxt split_fmla minor_prems_assumps conclusion in - rtac split_thm 1 THEN rest (tl skel) memo + resolve_tac ctxt [split_thm] 1 THEN rest (tl skel) memo end | Step s => let - val (tac, memo') = tac_and_memo s memo + val (th, memo') = tac_and_memo s memo in - rtac tac 1 THEN rest (tl skel) memo' + resolve_tac ctxt [th] 1 THEN rest (tl skel) memo' end | Definition n => let @@ -1008,7 +1008,7 @@ NONE => error ("Did not find definition: " ^ n) | SOME binding => Global_Theory.get_thm thy (Binding.name_of binding) in - rtac def_thm 1 THEN rest (tl skel) memo + resolve_tac ctxt [def_thm] 1 THEN rest (tl skel) memo end | Axiom n => let @@ -1017,7 +1017,7 @@ NONE => error ("Did not find axiom: " ^ n) | SOME binding => Global_Theory.get_thm thy (Binding.name_of binding) in - rtac ax_thm 1 THEN rest (tl skel) memo + resolve_tac ctxt [ax_thm] 1 THEN rest (tl skel) memo end | _ => raise SKELETON in tactic st end @@ -1065,7 +1065,7 @@ let fun thm ctxt'' = prover_tac ctxt'' prob_name (hd skel |> stock_to_string) val reconstructed_inference = thm ctxt' - fun rec_inf_tac st = HEADGOAL (rtac (thm ctxt')) st + fun rec_inf_tac st = HEADGOAL (resolve_tac ctxt' [thm ctxt']) st in (reconstructed_inference, rec_inf_tac) end) @@ -1088,17 +1088,17 @@ (hd skel, Thm.prop_of @{thm asm_rl} |> SOME, - SOME (@{thm asm_rl}, TRY (HEADGOAL atac))) :: rest memo ctxt + SOME (@{thm asm_rl}, TRY (HEADGOAL (assume_tac ctxt)))) :: rest memo ctxt | Caboose => [(Caboose, Thm.prop_of @{thm asm_rl} |> SOME, - SOME (@{thm asm_rl}, TRY (HEADGOAL atac)))] + SOME (@{thm asm_rl}, TRY (HEADGOAL (assume_tac ctxt))))] | Unconjoin => (hd skel, Thm.prop_of @{thm conjI} |> SOME, - SOME (@{thm conjI}, rtac @{thm conjI} 1)) :: rest memo ctxt + SOME (@{thm conjI}, resolve_tac ctxt @{thms conjI} 1)) :: rest memo ctxt | Split (split_node, solved_node, antes) => let val split_fmla = node_info (#meta pannot) #fmla split_node @@ -1117,7 +1117,7 @@ (hd skel, Thm.prop_of split_thm |> SOME, - SOME (split_thm, rtac split_thm 1)) :: rest memo ctxt + SOME (split_thm, resolve_tac ctxt [split_thm] 1)) :: rest memo ctxt end | Step node => let @@ -1180,7 +1180,7 @@ (hd skel, Thm.prop_of (def_thm thy) |> SOME, - SOME (def_thm thy, HEADGOAL (rtac (def_thm thy)))) :: rest memo ctxt + SOME (def_thm thy, HEADGOAL (resolve_tac ctxt [def_thm thy]))) :: rest memo ctxt end | Axiom n => let @@ -1192,7 +1192,7 @@ (hd skel, Thm.prop_of ax_thm |> SOME, - SOME (ax_thm, rtac ax_thm 1)) :: rest memo ctxt + SOME (ax_thm, resolve_tac ctxt [ax_thm] 1)) :: rest memo ctxt end end @@ -1216,7 +1216,7 @@ TPTP_Proof.is_inference_called "solved_all_splits" (the last_inference_info) then (@{thm asm_rl}, all_tac) - else (solved_all_splits, TRY (rtac solved_all_splits 1)) + else (solved_all_splits, TRY (resolve_tac ctxt [solved_all_splits] 1)) end in (*Build a tactic from a skeleton. This is naive because it uses the naive skeleton. @@ -1226,8 +1226,8 @@ let val thy = Proof_Context.theory_of ctxt in - rtac @{thm ccontr} 1 - THEN dtac neg_eq_false 1 + resolve_tac ctxt @{thms ccontr} 1 + THEN dresolve_tac ctxt [neg_eq_false] 1 THEN (sas_if_needed_tac ctxt prob_name |> #2) THEN skel_to_naive_tactic ctxt prover_tac prob_name (make_skeleton ctxt @@ -1241,9 +1241,9 @@ val thy = Proof_Context.theory_of ctxt in (Synth_step "ccontr", Thm.prop_of @{thm ccontr} |> SOME, - SOME (@{thm ccontr}, rtac @{thm ccontr} 1)) :: + SOME (@{thm ccontr}, resolve_tac ctxt @{thms ccontr} 1)) :: (Synth_step "neg_eq_false", Thm.prop_of neg_eq_false |> SOME, - SOME (neg_eq_false, dtac neg_eq_false 1)) :: + SOME (neg_eq_false, dresolve_tac ctxt [neg_eq_false] 1)) :: (Synth_step "sas_if_needed_tac", Thm.prop_of @{thm asm_rl} (*FIXME *) |> SOME, SOME (sas_if_needed_tac ctxt prob_name)) :: skel_to_naive_tactic_dbg prover_tac ctxt prob_name diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/TPTP/TPTP_Proof_Reconstruction.thy --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sat Jul 18 20:54:56 2015 +0200 @@ -282,13 +282,13 @@ val thm = Goal.prove ctxt [] [] (Logic.mk_implies (hyp_clause, new_hyp)) (fn _ => - (REPEAT_DETERM (HEADGOAL (rtac @{thm allI}))) + (REPEAT_DETERM (HEADGOAL (resolve_tac ctxt @{thms allI}))) THEN (REPEAT_DETERM (HEADGOAL (nominal_inst_parametermatch_tac ctxt @{thm allE}))) - THEN HEADGOAL atac) + THEN HEADGOAL (assume_tac ctxt)) in - dtac thm i st + dresolve_tac ctxt [thm] i st end end *} @@ -305,8 +305,8 @@ (TPTP_Reconstruct.remove_polarity true t; true) handle TPTP_Reconstruct.UNPOLARISED _ => false -val polarise_subgoal_hyps = - COND' (SOME #> TERMPRED is_polarised (fn _ => true)) (K no_tac) (dtac @{thm polarise}) +fun polarise_subgoal_hyps ctxt = + COND' (SOME #> TERMPRED is_polarised (fn _ => true)) (K no_tac) (dresolve_tac ctxt @{thms polarise}) *} lemma simp_meta [rule_format]: @@ -336,10 +336,10 @@ lemma solved_all_splits: "False = True \ False" by simp ML {* -val solved_all_splits_tac = - TRY (etac @{thm conjE} 1) - THEN rtac @{thm solved_all_splits} 1 - THEN atac 1 +fun solved_all_splits_tac ctxt = + TRY (eresolve_tac ctxt @{thms conjE} 1) + THEN resolve_tac ctxt @{thms solved_all_splits} 1 + THEN assume_tac ctxt 1 *} lemma lots_of_logic_expansions_meta [rule_format]: @@ -433,10 +433,10 @@ fun instantiate_tac vars = instantiate_vars ctxt vars - THEN (HEADGOAL atac) + THEN (HEADGOAL (assume_tac ctxt)) in HEADGOAL (canonicalise_qtfr_order ctxt) - THEN (REPEAT_DETERM (HEADGOAL (rtac @{thm allI}))) + THEN (REPEAT_DETERM (HEADGOAL (resolve_tac ctxt @{thms allI}))) THEN REPEAT_DETERM (HEADGOAL (nominal_inst_parametermatch_tac ctxt @{thm allE})) (*now only the variable to instantiate should be left*) THEN FIRST (map instantiate_tac ordered_instances) @@ -470,8 +470,8 @@ let val default_tac = (TRY o CHANGED o (rewrite_goal_tac ctxt @{thms prop_normalise})) - THEN' rtac @{thm notI} - THEN' (REPEAT_DETERM o etac @{thm conjE}) + THEN' resolve_tac ctxt @{thms notI} + THEN' (REPEAT_DETERM o eresolve_tac ctxt @{thms conjE}) THEN' (TRY o (expander_animal ctxt)) in default_tac ORELSE' resolve_tac ctxt @{thms flip} @@ -646,8 +646,6 @@ ML {* fun forall_neg_tac candidate_consts ctxt i = fn st => let - val thy = Proof_Context.theory_of ctxt - val gls = Thm.prop_of st |> Logic.strip_horn @@ -749,7 +747,7 @@ else raise (NO_SKOLEM_DEF (def_name, bnd_name, conclusion))) in - rtac (Drule.export_without_context thm) i st + resolve_tac ctxt [Drule.export_without_context thm] i st end handle SKOLEM_DEF _ => no_tac st *} @@ -960,12 +958,12 @@ ML {* fun new_skolem_tac ctxt consts_candidates = let - fun tec thm = - dtac thm + fun tac thm = + dresolve_tac ctxt [thm] THEN' instantiate_skols ctxt consts_candidates in if null consts_candidates then K no_tac - else FIRST' (map tec @{thms lift_exists}) + else FIRST' (map tac @{thms lift_exists}) end *} @@ -1142,7 +1140,7 @@ those free variables into logical variables.*) |> Thm.forall_intr_frees |> Drule.export_without_context - in dtac rule i st end + in dresolve_tac ctxt [rule] i st end handle NO_GOALS => no_tac st fun closure tac = @@ -1151,10 +1149,10 @@ SOLVE o (tac THEN' (batter_tac ctxt ORELSE' assume_tac ctxt)) val search_tac = ASAP - (rtac @{thm disjI1} APPEND' rtac @{thm disjI2}) + (resolve_tac ctxt @{thms disjI1} APPEND' resolve_tac ctxt @{thms disjI2}) (FIRST' (map closure [dresolve_tac ctxt @{thms dec_commut_eq}, - dtac @{thm dec_commut_disj}, + dresolve_tac ctxt @{thms dec_commut_disj}, elim_tac])) in (CHANGED o search_tac) i st @@ -1306,14 +1304,15 @@ v \A = True; B = False\ \ R *) -fun weak_conj_tac drule = - dtac drule THEN' (REPEAT_DETERM o etac @{thm conjE}) +fun weak_conj_tac ctxt drule = + dresolve_tac ctxt [drule] THEN' + (REPEAT_DETERM o eresolve_tac ctxt @{thms conjE}) *} ML {* -val uncurry_lit_neg_tac = - dtac @{lemma "(A \ B \ C) = False \ (A & B \ C) = False" by auto} - #> REPEAT_DETERM +fun uncurry_lit_neg_tac ctxt = + REPEAT_DETERM o + dresolve_tac ctxt [@{lemma "(A \ B \ C) = False \ (A & B \ C) = False" by auto}] *} ML {* @@ -1326,10 +1325,10 @@ let val rule = mk_standard_cnf ctxt kind arity; in - (weak_conj_tac rule THEN' atac) i st + (weak_conj_tac ctxt rule THEN' assume_tac ctxt) i st end in - (uncurry_lit_neg_tac + (uncurry_lit_neg_tac ctxt THEN' TPTP_Reconstruct_Library.reassociate_conjs_tac ctxt THEN' core_tactic) i st end @@ -1473,13 +1472,13 @@ (*use as elim rule to remove premises*) lemma insa_prems: "\Q; P\ \ P" by auto ML {* -fun cleanup_skolem_defs feats = +fun cleanup_skolem_defs ctxt feats = let (*remove hypotheses from skolem defs, after testing that they look like skolem defs*) val dehypothesise_skolem_defs = COND' (SOME #> TERMPRED (fn _ => true) conc_is_skolem_def) - (REPEAT_DETERM o etac @{thm insa_prems}) + (REPEAT_DETERM o eresolve_tac ctxt @{thms insa_prems}) (K no_tac) in if can_feature (CleanUp [RemoveHypothesesFromSkolemDefs]) feats then @@ -1497,11 +1496,11 @@ ML {* (*given a goal state, indicates the skolem constants committed-to in it (i.e. appearing in LHS of a skolem definition)*) -val which_skolem_concs_used = fn st => +fun which_skolem_concs_used ctxt = fn st => let val feats = [CleanUp [RemoveHypothesesFromSkolemDefs, RemoveDuplicates]] val scrubup_tac = - cleanup_skolem_defs feats + cleanup_skolem_defs ctxt feats THEN remove_duplicates_tac feats in scrubup_tac st @@ -1547,7 +1546,7 @@ (*predicate over the type of the leading quantified variable*) ML {* -val extcnf_forall_special_pos_tac = +fun extcnf_forall_special_pos_tac ctxt = let val bool = ["True", "False"] @@ -1555,16 +1554,16 @@ val bool_to_bool = ["% _ . True", "% _ . False", "% x . x", "Not"] - val tecs = + val tacs = map (fn t_s => (* FIXME proper context!? *) Rule_Insts.eres_inst_tac @{context} [((("x", 0), Position.none), t_s)] [] @{thm allE} - THEN' atac) + THEN' assume_tac ctxt) in - (TRY o etac @{thm forall_pos_lift}) - THEN' (atac + (TRY o eresolve_tac ctxt @{thms forall_pos_lift}) + THEN' (assume_tac ctxt ORELSE' FIRST' (*FIXME could check the type of the leading quantified variable, instead of trying everything*) - (tecs (bool @ bool_to_bool))) + (tacs (bool @ bool_to_bool))) end *} @@ -1573,9 +1572,9 @@ lemma efq: "[|A = True; A = False|] ==> R" by auto ML {* -val efq_tac = - (etac @{thm efq} THEN' atac) - ORELSE' atac +fun efq_tac ctxt = + (eresolve_tac ctxt @{thms efq} THEN' assume_tac ctxt) + ORELSE' assume_tac ctxt *} ML {* @@ -1586,13 +1585,13 @@ consisting of a Skolem definition*) fun extcnf_combined_tac' ctxt i = fn st => let - val skolem_consts_used_so_far = which_skolem_concs_used st + val skolem_consts_used_so_far = which_skolem_concs_used ctxt st val consts_diff' = subtract (op =) skolem_consts_used_so_far consts_diff fun feat_to_tac feat = case feat of - Close_Branch => trace_tac' ctxt "mark: closer" efq_tac - | ConjI => trace_tac' ctxt "mark: conjI" (rtac @{thm conjI}) + Close_Branch => trace_tac' ctxt "mark: closer" (efq_tac ctxt) + | ConjI => trace_tac' ctxt "mark: conjI" (resolve_tac ctxt @{thms conjI}) | King_Cong => trace_tac' ctxt "mark: expander_animal" (expander_animal ctxt) | Break_Hypotheses => trace_tac' ctxt "mark: break_hypotheses" (break_hypotheses_tac ctxt) | RemoveRedundantQuantifications => K all_tac @@ -1603,28 +1602,28 @@ (REPEAT_DETERM o remove_redundant_quantification_in_lit) *) - | Assumption => atac + | Assumption => assume_tac ctxt (*FIXME both Existential_Free and Existential_Var run same code*) | Existential_Free => trace_tac' ctxt "mark: forall_neg" (exists_tac ctxt feats consts_diff') | Existential_Var => trace_tac' ctxt "mark: forall_neg" (exists_tac ctxt feats consts_diff') | Universal => trace_tac' ctxt "mark: forall_pos" (forall_tac ctxt feats) - | Not_pos => trace_tac' ctxt "mark: not_pos" (dtac @{thm leo2_rules(9)}) - | Not_neg => trace_tac' ctxt "mark: not_neg" (dtac @{thm leo2_rules(10)}) - | Or_pos => trace_tac' ctxt "mark: or_pos" (dtac @{thm leo2_rules(5)}) (*could add (6) for negated conjunction*) - | Or_neg => trace_tac' ctxt "mark: or_neg" (dtac @{thm leo2_rules(7)}) + | Not_pos => trace_tac' ctxt "mark: not_pos" (dresolve_tac ctxt @{thms leo2_rules(9)}) + | Not_neg => trace_tac' ctxt "mark: not_neg" (dresolve_tac ctxt @{thms leo2_rules(10)}) + | Or_pos => trace_tac' ctxt "mark: or_pos" (dresolve_tac ctxt @{thms leo2_rules(5)}) (*could add (6) for negated conjunction*) + | Or_neg => trace_tac' ctxt "mark: or_neg" (dresolve_tac ctxt @{thms leo2_rules(7)}) | Equal_pos => trace_tac' ctxt "mark: equal_pos" (dresolve_tac ctxt (@{thms eq_pos_bool} @ [@{thm leo2_rules(3)}, @{thm eq_pos_func}])) | Equal_neg => trace_tac' ctxt "mark: equal_neg" (dresolve_tac ctxt [@{thm eq_neg_bool}, @{thm leo2_rules(4)}]) | Donkey_Cong => trace_tac' ctxt "mark: donkey_cong" (simper_animal ctxt THEN' ex_expander_tac ctxt) - | Extuni_Bool2 => trace_tac' ctxt "mark: extuni_bool2" (dtac @{thm extuni_bool2}) - | Extuni_Bool1 => trace_tac' ctxt "mark: extuni_bool1" (dtac @{thm extuni_bool1}) - | Extuni_Bind => trace_tac' ctxt "mark: extuni_triv" (etac @{thm extuni_triv}) - | Extuni_Triv => trace_tac' ctxt "mark: extuni_triv" (etac @{thm extuni_triv}) + | Extuni_Bool2 => trace_tac' ctxt "mark: extuni_bool2" (dresolve_tac ctxt @{thms extuni_bool2}) + | Extuni_Bool1 => trace_tac' ctxt "mark: extuni_bool1" (dresolve_tac ctxt @{thms extuni_bool1}) + | Extuni_Bind => trace_tac' ctxt "mark: extuni_triv" (eresolve_tac ctxt @{thms extuni_triv}) + | Extuni_Triv => trace_tac' ctxt "mark: extuni_triv" (eresolve_tac ctxt @{thms extuni_triv}) | Extuni_Dec => trace_tac' ctxt "mark: extuni_dec_tac" (extuni_dec_tac ctxt) - | Extuni_FlexRigid => trace_tac' ctxt "mark: extuni_flex_rigid" (atac ORELSE' asm_full_simp_tac ctxt) - | Extuni_Func => trace_tac' ctxt "mark: extuni_func" (dtac @{thm extuni_func}) + | Extuni_FlexRigid => trace_tac' ctxt "mark: extuni_flex_rigid" (assume_tac ctxt ORELSE' asm_full_simp_tac ctxt) + | Extuni_Func => trace_tac' ctxt "mark: extuni_func" (dresolve_tac ctxt @{thms extuni_func}) | Polarity_switch => trace_tac' ctxt "mark: polarity_switch" (eresolve_tac ctxt @{thms polarity_switch}) - | Forall_special_pos => trace_tac' ctxt "mark: dorall_special_pos" extcnf_forall_special_pos_tac + | Forall_special_pos => trace_tac' ctxt "mark: dorall_special_pos" (extcnf_forall_special_pos_tac ctxt) val core_tac = get_loop_feats feats @@ -1668,8 +1667,8 @@ @{const_name Pure.imp}] fun strip_qtfrs_tac ctxt = - REPEAT_DETERM (HEADGOAL (rtac @{thm allI})) - THEN REPEAT_DETERM (HEADGOAL (etac @{thm exE})) + REPEAT_DETERM (HEADGOAL (resolve_tac ctxt @{thms allI})) + THEN REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt @{thms exE})) THEN HEADGOAL (canonicalise_qtfr_order ctxt) THEN ((REPEAT (HEADGOAL (nominal_inst_parametermatch_tac ctxt @{thm allE}))) @@ -1846,7 +1845,7 @@ then we should be left with skolem definitions: absorb them as axioms into the theory.*) val cleanup = - cleanup_skolem_defs feats + cleanup_skolem_defs ctxt feats THEN remove_duplicates_tac feats THEN (if can_feature AbsorbSkolemDefs feats then ALLGOALS (absorb_skolem_def ctxt prob_name_opt) @@ -1868,9 +1867,9 @@ can be simply eliminated -- they're redundant*) (*FIXME instead of just using allE, instantiate to a silly term, to remove opportunities for unification.*) - THEN (REPEAT_DETERM (etac @{thm allE} 1)) + THEN (REPEAT_DETERM (eresolve_tac ctxt @{thms allE} 1)) - THEN (REPEAT_DETERM (rtac @{thm allI} 1)) + THEN (REPEAT_DETERM (resolve_tac ctxt @{thms allI} 1)) THEN (if have_loop_feats then REPEAT (CHANGED @@ -1914,32 +1913,33 @@ discharged. *) val kill_meta_eqs_tac = - dtac @{thm un_meta_polarise} - THEN' rtac @{thm meta_polarise} - THEN' (REPEAT_DETERM o (etac @{thm conjE})) - THEN' (REPEAT_DETERM o (rtac @{thm conjI} ORELSE' atac)) + dresolve_tac ctxt @{thms un_meta_polarise} + THEN' resolve_tac ctxt @{thms meta_polarise} + THEN' (REPEAT_DETERM o (eresolve_tac ctxt @{thms conjE})) + THEN' (REPEAT_DETERM o (resolve_tac ctxt @{thms conjI} ORELSE' assume_tac ctxt)) val continue_reducing_tac = - rtac @{thm meta_eq_to_obj_eq} 1 + resolve_tac ctxt @{thms meta_eq_to_obj_eq} 1 THEN (REPEAT_DETERM (ex_expander_tac ctxt 1)) - THEN TRY (polarise_subgoal_hyps 1) (*no need to REPEAT_DETERM here, since there should only be one hypothesis*) - THEN TRY (dtac @{thm eq_reflection} 1) + THEN TRY (polarise_subgoal_hyps ctxt 1) (*no need to REPEAT_DETERM here, since there should only be one hypothesis*) + THEN TRY (dresolve_tac ctxt @{thms eq_reflection} 1) THEN (TRY ((CHANGED o rewrite_goal_tac ctxt (@{thm expand_iff} :: @{thms simp_meta})) 1)) - THEN HEADGOAL (rtac @{thm reflexive} - ORELSE' atac + THEN HEADGOAL (resolve_tac ctxt @{thms reflexive} + ORELSE' assume_tac ctxt ORELSE' kill_meta_eqs_tac) val tactic = - (rtac @{thm polarise} 1 THEN atac 1) + (resolve_tac ctxt @{thms polarise} 1 THEN assume_tac ctxt 1) ORELSE - (REPEAT_DETERM (etac @{thm conjE} 1 THEN etac @{thm drop_first_hypothesis} 1) + (REPEAT_DETERM (eresolve_tac ctxt @{thms conjE} 1 THEN + eresolve_tac ctxt @{thms drop_first_hypothesis} 1) THEN PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion) THEN (REPEAT_DETERM (ex_expander_tac ctxt 1)) THEN (TRY ((CHANGED o rewrite_goal_tac ctxt @{thms simp_meta}) 1)) THEN PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion) THEN - (HEADGOAL atac + (HEADGOAL (assume_tac ctxt) ORELSE (unfold_tac ctxt depends_on_defs THEN IF_UNSOLVED continue_reducing_tac))) @@ -2117,12 +2117,12 @@ *) | "copy" => HEADGOAL - (atac + (assume_tac ctxt ORELSE' - (rtac @{thm polarise} - THEN' atac)) + (resolve_tac ctxt @{thms polarise} + THEN' assume_tac ctxt)) | "polarity_switch" => nonfull_extcnf_combined_tac [Polarity_switch] - | "solved_all_splits" => solved_all_splits_tac + | "solved_all_splits" => solved_all_splits_tac ctxt | "extcnf_not_pos" => nonfull_extcnf_combined_tac [Not_pos] | "extcnf_forall_pos" => nonfull_extcnf_combined_tac [Universal] | "negate_conjecture" => fail ctxt "Should not handle negate_conjecture here" @@ -2138,7 +2138,7 @@ | "extuni_bool2" => nonfull_extcnf_combined_tac [Extuni_Bool2] | "extuni_bool1" => nonfull_extcnf_combined_tac [Extuni_Bool1] | "extuni_dec" => - HEADGOAL atac + HEADGOAL (assume_tac ctxt) ORELSE nonfull_extcnf_combined_tac [Extuni_Dec] | "extuni_bind" => nonfull_extcnf_combined_tac [Extuni_Bind] | "extuni_triv" => nonfull_extcnf_combined_tac [Extuni_Triv] @@ -2161,7 +2161,7 @@ | "split_preprocessing" => (REPEAT (HEADGOAL (split_simp_tac ctxt))) THEN TRY (PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion)) - THEN HEADGOAL atac + THEN HEADGOAL (assume_tac ctxt) (*FIXME some of these could eventually be handled specially*) | "fac_restr" => default_tac diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/UNITY/Comp/Alloc.thy --- a/src/HOL/UNITY/Comp/Alloc.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/UNITY/Comp/Alloc.thy Sat Jul 18 20:54:56 2015 +0200 @@ -712,7 +712,7 @@ fun rename_client_map_tac ctxt = EVERY [ simp_tac (ctxt addsimps [@{thm rename_guarantees_eq_rename_inv}]) 1, - rtac @{thm guarantees_PLam_I} 1, + resolve_tac ctxt @{thms guarantees_PLam_I} 1, assume_tac ctxt 2, (*preserves: routine reasoning*) asm_simp_tac (ctxt addsimps [@{thm lift_preserves_sub}]) 2, @@ -899,9 +899,9 @@ text{*safety (1), step 4 (final result!) *} theorem System_safety: "System : system_safety" apply (unfold system_safety_def) - apply (tactic {* rtac (Always_Int_rule [@{thm System_sum_bounded}, + apply (tactic {* resolve_tac @{context} [Always_Int_rule [@{thm System_sum_bounded}, @{thm Always_tokens_giv_le_allocGiv}, @{thm Always_tokens_allocRel_le_rel}] RS - @{thm Always_weaken}) 1 *}) + @{thm Always_weaken}] 1 *}) apply auto apply (rule setsum_fun_mono [THEN order_trans]) apply (drule_tac [2] order_trans) @@ -942,8 +942,8 @@ lemma System_Bounded_allocAsk: "System : Always {s. ALL i NbT}" apply (auto simp add: Collect_all_imp_eq) - apply (tactic {* rtac (Always_Int_rule [@{thm Always_allocAsk_le_ask}, - @{thm System_Bounded_ask}] RS @{thm Always_weaken}) 1 *}) + apply (tactic {* resolve_tac @{context} [Always_Int_rule [@{thm Always_allocAsk_le_ask}, + @{thm System_Bounded_ask}] RS @{thm Always_weaken}] 1 *}) apply (auto dest: set_mono) done diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/UNITY/Simple/NSP_Bad.thy --- a/src/HOL/UNITY/Simple/NSP_Bad.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Sat Jul 18 20:54:56 2015 +0200 @@ -104,11 +104,11 @@ fun ns_constrains_tac ctxt i = SELECT_GOAL (EVERY - [REPEAT (etac @{thm Always_ConstrainsI} 1), + [REPEAT (eresolve_tac ctxt @{thms Always_ConstrainsI} 1), REPEAT (resolve_tac ctxt [@{thm StableI}, @{thm stableI}, @{thm constrains_imp_Constrains}] 1), - rtac @{thm ns_constrainsI} 1, + resolve_tac ctxt @{thms ns_constrainsI} 1, full_simp_tac ctxt 1, - REPEAT (FIRSTGOAL (etac disjE)), + REPEAT (FIRSTGOAL (eresolve_tac ctxt [disjE])), ALLGOALS (clarify_tac (ctxt delrules [impI, @{thm impCE}])), REPEAT (FIRSTGOAL (analz_mono_contra_tac ctxt)), ALLGOALS (asm_simp_tac ctxt)]) i; @@ -116,10 +116,10 @@ (*Tactic for proving secrecy theorems*) fun ns_induct_tac ctxt = (SELECT_GOAL o EVERY) - [rtac @{thm AlwaysI} 1, + [resolve_tac ctxt @{thms AlwaysI} 1, force_tac ctxt 1, (*"reachable" gets in here*) - rtac (@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}) 1, + resolve_tac ctxt [@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}] 1, ns_constrains_tac ctxt 1]; *} diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/UNITY/UNITY_tactics.ML --- a/src/HOL/UNITY/UNITY_tactics.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/UNITY/UNITY_tactics.ML Sat Jul 18 20:54:56 2015 +0200 @@ -7,7 +7,9 @@ (*Combines two invariance ASSUMPTIONS into one. USEFUL??*) fun Always_Int_tac ctxt = - dtac @{thm Always_Int_I} THEN' assume_tac ctxt THEN' etac @{thm Always_thin} + dresolve_tac ctxt @{thms Always_Int_I} THEN' + assume_tac ctxt THEN' + eresolve_tac ctxt @{thms Always_thin} (*Combines a list of invariance THEOREMS into one.*) val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I}) @@ -19,16 +21,16 @@ (EVERY [REPEAT (Always_Int_tac ctxt 1), (*reduce the fancy safety properties to "constrains"*) - REPEAT (etac @{thm Always_ConstrainsI} 1 + REPEAT (eresolve_tac ctxt @{thms Always_ConstrainsI} 1 ORELSE resolve_tac ctxt [@{thm StableI}, @{thm stableI}, @{thm constrains_imp_Constrains}] 1), (*for safety, the totalize operator can be ignored*) simp_tac (put_simpset HOL_ss ctxt addsimps [@{thm mk_total_program_def}, @{thm totalize_constrains_iff}]) 1, - rtac @{thm constrainsI} 1, + resolve_tac ctxt @{thms constrainsI} 1, full_simp_tac ctxt 1, - REPEAT (FIRSTGOAL (etac disjE)), + REPEAT (FIRSTGOAL (eresolve_tac ctxt [disjE])), ALLGOALS (clarify_tac ctxt), ALLGOALS (asm_full_simp_tac ctxt)]) i; @@ -37,7 +39,7 @@ SELECT_GOAL (EVERY [REPEAT (Always_Int_tac ctxt 1), - etac @{thm Always_LeadsTo_Basis} 1 + eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1 ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, @{thm EnsuresI}, @{thm ensuresI}] 1), diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/Word/Word.thy Sat Jul 18 20:54:56 2015 +0200 @@ -1562,8 +1562,8 @@ |> fold Simplifier.add_cong @{thms power_False_cong})), rewrite_goals_tac ctxt @{thms word_size}, ALLGOALS (fn n => REPEAT (resolve_tac ctxt [allI, impI] n) THEN - REPEAT (etac conjE n) THEN - REPEAT (dtac @{thm word_of_int_inverse} n + REPEAT (eresolve_tac ctxt [conjE] n) THEN + REPEAT (dresolve_tac ctxt @{thms word_of_int_inverse} n THEN assume_tac ctxt n THEN assume_tac ctxt n)), TRYALL arith_tac' ] @@ -2063,9 +2063,9 @@ |> fold Splitter.add_split @{thms unat_splits} |> fold Simplifier.add_cong @{thms power_False_cong})), rewrite_goals_tac ctxt @{thms word_size}, - ALLGOALS (fn n => REPEAT (resolve_tac ctxt [allI, impI] n) THEN - REPEAT (etac conjE n) THEN - REPEAT (dtac @{thm of_nat_inverse} n THEN atac n)), + ALLGOALS (fn n => REPEAT (resolve_tac ctxt [allI, impI] n) THEN + REPEAT (eresolve_tac ctxt [conjE] n) THEN + REPEAT (dresolve_tac ctxt @{thms of_nat_inverse} n THEN assume_tac ctxt n)), TRYALL arith_tac' ] end diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/ex/Cartouche_Examples.thy --- a/src/HOL/ex/Cartouche_Examples.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/ex/Cartouche_Examples.thy Sat Jul 18 20:54:56 2015 +0200 @@ -33,7 +33,7 @@ [OF \x = y\]}.\ have "x = y" - by (tactic \rtac @{thm \x = y\} 1\) -- \more cartouches involving ML\ + by (tactic \resolve_tac @{context} @{thms \x = y\} 1\) -- \more cartouches involving ML\ end @@ -230,10 +230,10 @@ \ lemma "A \ B \ B \ A" - apply (ml_tactic \rtac @{thm impI} 1\) - apply (ml_tactic \etac @{thm conjE} 1\) - apply (ml_tactic \rtac @{thm conjI} 1\) - apply (ml_tactic \ALLGOALS atac\) + apply (ml_tactic \resolve_tac @{context} @{thms impI} 1\) + apply (ml_tactic \eresolve_tac @{context} @{thms conjE} 1\) + apply (ml_tactic \resolve_tac @{context} @{thms conjI} 1\) + apply (ml_tactic \ALLGOALS (assume_tac @{context})\) done lemma "A \ B \ B \ A" by (ml_tactic \blast_tac ctxt 1\) @@ -251,14 +251,17 @@ \ lemma "A \ B \ B \ A" - apply \rtac @{thm impI} 1\ - apply \etac @{thm conjE} 1\ - apply \rtac @{thm conjI} 1\ - apply \ALLGOALS atac\ + apply \resolve_tac @{context} @{thms impI} 1\ + apply \eresolve_tac @{context} @{thms conjE} 1\ + apply \resolve_tac @{context} @{thms conjI} 1\ + apply \ALLGOALS (assume_tac @{context})\ done lemma "A \ B \ B \ A" - by (\rtac @{thm impI} 1\, \etac @{thm conjE} 1\, \rtac @{thm conjI} 1\, \atac 1\+) + by (\resolve_tac @{context} @{thms impI} 1\, + \eresolve_tac @{context} @{thms conjE} 1\, + \resolve_tac @{context} @{thms conjI} 1\, + \assume_tac @{context} 1\+) subsection \ML syntax\ diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/ex/Iff_Oracle.thy --- a/src/HOL/ex/Iff_Oracle.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/ex/Iff_Oracle.thy Sat Jul 18 20:54:56 2015 +0200 @@ -58,7 +58,7 @@ method_setup iff = \Scan.lift Parse.nat >> (fn n => fn ctxt => SIMPLE_METHOD - (HEADGOAL (rtac (iff_oracle (Proof_Context.theory_of ctxt, n))) + (HEADGOAL (resolve_tac ctxt [iff_oracle (Proof_Context.theory_of ctxt, n)]) handle Fail _ => no_tac))\ diff -r 80ca4a065a48 -r 02924903a6fd src/HOL/ex/Meson_Test.thy --- a/src/HOL/ex/Meson_Test.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/HOL/ex/Meson_Test.thy Sat Jul 18 20:54:56 2015 +0200 @@ -29,7 +29,7 @@ val nnf25 = Meson.make_nnf ctxt prem25; val xsko25 = Meson.skolemize ctxt nnf25; *} - apply (tactic {* cut_tac xsko25 1 THEN REPEAT (etac exE 1) *}) + apply (tactic {* cut_tac xsko25 1 THEN REPEAT (eresolve_tac @{context} [exE] 1) *}) ML_val {* val ctxt = @{context}; val [_, sko25] = #prems (#1 (Subgoal.focus ctxt 1 NONE (#goal @{Isar.goal}))); @@ -39,7 +39,7 @@ val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go25 :: horns25)) ctxt; Goal.prove ctxt' [] [] @{prop False} (fn _ => - rtac go25 1 THEN + resolve_tac ctxt' [go25] 1 THEN Meson.depth_prolog_tac ctxt' horns25); *} oops @@ -53,7 +53,7 @@ val nnf26 = Meson.make_nnf ctxt prem26; val xsko26 = Meson.skolemize ctxt nnf26; *} - apply (tactic {* cut_tac xsko26 1 THEN REPEAT (etac exE 1) *}) + apply (tactic {* cut_tac xsko26 1 THEN REPEAT (eresolve_tac @{context} [exE] 1) *}) ML_val {* val ctxt = @{context}; val [_, sko26] = #prems (#1 (Subgoal.focus ctxt 1 NONE (#goal @{Isar.goal}))); @@ -65,7 +65,7 @@ val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go26 :: horns26)) ctxt; Goal.prove ctxt' [] [] @{prop False} (fn _ => - rtac go26 1 THEN + resolve_tac ctxt' [go26] 1 THEN Meson.depth_prolog_tac ctxt' horns26); (*7 ms*) (*Proof is of length 107!!*) *} @@ -80,7 +80,7 @@ val nnf43 = Meson.make_nnf ctxt prem43; val xsko43 = Meson.skolemize ctxt nnf43; *} - apply (tactic {* cut_tac xsko43 1 THEN REPEAT (etac exE 1) *}) + apply (tactic {* cut_tac xsko43 1 THEN REPEAT (eresolve_tac @{context} [exE] 1) *}) ML_val {* val ctxt = @{context}; val [_, sko43] = #prems (#1 (Subgoal.focus ctxt 1 NONE (#goal @{Isar.goal}))); @@ -92,7 +92,7 @@ val ctxt' = fold Thm.declare_hyps (maps (#hyps o Thm.crep_thm) (go43 :: horns43)) ctxt; Goal.prove ctxt' [] [] @{prop False} (fn _ => - rtac go43 1 THEN + resolve_tac ctxt' [go43] 1 THEN Meson.best_prolog_tac ctxt' Meson.size_of_subgoals horns43); (*7ms*) *} oops diff -r 80ca4a065a48 -r 02924903a6fd src/Provers/Arith/assoc_fold.ML --- a/src/Provers/Arith/assoc_fold.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/Provers/Arith/assoc_fold.ML Sat Jul 18 20:54:56 2015 +0200 @@ -44,8 +44,10 @@ val (lits, others) = sift_terms plus (lhs, ([],[])) val _ = length lits < 2 andalso raise Assoc_fail (*we can't reduce the number of terms*) val rhs = plus $ mk_sum plus lits $ mk_sum plus others - val th = Goal.prove ctxt [] [] (Logic.mk_equals (lhs, rhs)) - (fn _ => rtac Data.eq_reflection 1 THEN simp_tac (put_simpset Data.assoc_ss ctxt) 1) + val th = + Goal.prove ctxt [] [] (Logic.mk_equals (lhs, rhs)) (fn _ => + resolve_tac ctxt [Data.eq_reflection] 1 THEN + simp_tac (put_simpset Data.assoc_ss ctxt) 1) in SOME th end handle Assoc_fail => NONE; end; diff -r 80ca4a065a48 -r 02924903a6fd src/Provers/Arith/cancel_numeral_factor.ML --- a/src/Provers/Arith/cancel_numeral_factor.ML Sat Jul 18 20:53:05 2015 +0200 +++ b/src/Provers/Arith/cancel_numeral_factor.ML Sat Jul 18 20:54:56 2015 +0200 @@ -72,7 +72,7 @@ in Option.map (export o Data.simplify_meta_eq ctxt) (Data.prove_conv - [Data.trans_tac ctxt reshape, rtac Data.cancel 1, + [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.cancel] 1, Data.numeral_simp_tac ctxt] ctxt prems (t', rhs)) end (* FIXME avoid handling of generic exceptions *) diff -r 80ca4a065a48 -r 02924903a6fd src/Sequents/LK.thy --- a/src/Sequents/LK.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/Sequents/LK.thy Sat Jul 18 20:54:56 2015 +0200 @@ -178,7 +178,7 @@ apply (lem p1) apply safe apply (tactic {* - REPEAT (rtac @{thm cut} 1 THEN + REPEAT (resolve_tac @{context} @{thms cut} 1 THEN DEPTH_SOLVE_1 (resolve_tac @{context} [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN Cla.safe_tac @{context} 1) *}) @@ -191,7 +191,7 @@ apply (lem p1) apply safe apply (tactic {* - REPEAT (rtac @{thm cut} 1 THEN + REPEAT (resolve_tac @{context} @{thms cut} 1 THEN DEPTH_SOLVE_1 (resolve_tac @{context} [@{thm thinL}, @{thm thinR}, @{thm p2} COMP @{thm monotonic}] 1) THEN Cla.safe_tac @{context} 1) *}) diff -r 80ca4a065a48 -r 02924903a6fd src/Sequents/LK0.thy --- a/src/Sequents/LK0.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/Sequents/LK0.thy Sat Jul 18 20:54:56 2015 +0200 @@ -154,12 +154,12 @@ (*Cut and thin, replacing the right-side formula*) fun cutR_tac ctxt s i = Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] [] @{thm cut} i THEN - rtac @{thm thinR} i + resolve_tac ctxt @{thms thinR} i (*Cut and thin, replacing the left-side formula*) fun cutL_tac ctxt s i = Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] [] @{thm cut} i THEN - rtac @{thm thinL} (i + 1) + resolve_tac ctxt @{thms thinL} (i + 1) *} @@ -244,11 +244,11 @@ {* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack LK_dup_pack ctxt))) *} method_setup lem = {* - Attrib.thm >> (fn th => fn _ => + Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (fn i => - rtac (@{thm thinR} RS @{thm cut}) i THEN - REPEAT (rtac @{thm thinL} i) THEN - rtac th i)) + resolve_tac ctxt [@{thm thinR} RS @{thm cut}] i THEN + REPEAT (resolve_tac ctxt @{thms thinL} i) THEN + resolve_tac ctxt [th] i)) *} diff -r 80ca4a065a48 -r 02924903a6fd src/ZF/UNITY/Constrains.thy --- a/src/ZF/UNITY/Constrains.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/ZF/UNITY/Constrains.thy Sat Jul 18 20:54:56 2015 +0200 @@ -460,7 +460,9 @@ {* (*Combines two invariance ASSUMPTIONS into one. USEFUL??*) fun Always_Int_tac ctxt = - dtac @{thm Always_Int_I} THEN' assume_tac ctxt THEN' etac @{thm Always_thin}; + dresolve_tac ctxt @{thms Always_Int_I} THEN' + assume_tac ctxt THEN' + eresolve_tac ctxt @{thms Always_thin}; (*Combines a list of invariance THEOREMS into one.*) val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I}); @@ -470,26 +472,28 @@ fun constrains_tac ctxt = SELECT_GOAL (EVERY [REPEAT (Always_Int_tac ctxt 1), - REPEAT (etac @{thm Always_ConstrainsI} 1 + REPEAT (eresolve_tac ctxt @{thms Always_ConstrainsI} 1 ORELSE resolve_tac ctxt [@{thm StableI}, @{thm stableI}, @{thm constrains_imp_Constrains}] 1), - rtac @{thm constrainsI} 1, + resolve_tac ctxt @{thms constrainsI} 1, (* Three subgoals *) rewrite_goal_tac ctxt [@{thm st_set_def}] 3, REPEAT (force_tac ctxt 2), full_simp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems program})) 1, ALLGOALS (clarify_tac ctxt), - REPEAT (FIRSTGOAL (etac @{thm disjE})), + REPEAT (FIRSTGOAL (eresolve_tac ctxt @{thms disjE})), ALLGOALS (clarify_tac ctxt), - REPEAT (FIRSTGOAL (etac @{thm disjE})), + REPEAT (FIRSTGOAL (eresolve_tac ctxt @{thms disjE})), ALLGOALS (clarify_tac ctxt), ALLGOALS (asm_full_simp_tac ctxt), ALLGOALS (clarify_tac ctxt)]); (*For proving invariants*) fun always_tac ctxt i = - rtac @{thm AlwaysI} i THEN force_tac ctxt i THEN constrains_tac ctxt i; + resolve_tac ctxt @{thms AlwaysI} i THEN + force_tac ctxt i + THEN constrains_tac ctxt i; *} method_setup safety = {* diff -r 80ca4a065a48 -r 02924903a6fd src/ZF/UNITY/SubstAx.thy --- a/src/ZF/UNITY/SubstAx.thy Sat Jul 18 20:53:05 2015 +0200 +++ b/src/ZF/UNITY/SubstAx.thy Sat Jul 18 20:54:56 2015 +0200 @@ -353,7 +353,7 @@ fun ensures_tac ctxt sact = SELECT_GOAL (EVERY [REPEAT (Always_Int_tac ctxt 1), - etac @{thm Always_LeadsTo_Basis} 1 + eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1 ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, @{thm EnsuresI}, @{thm ensuresI}] 1), @@ -364,10 +364,11 @@ (*simplify the command's domain*) simp_tac (ctxt addsimps [@{thm domain_def}]) 3, (* proving the domain part *) - clarify_tac ctxt 3, dtac @{thm swap} 3, force_tac ctxt 4, - rtac @{thm ReplaceI} 3, force_tac ctxt 3, force_tac ctxt 4, - asm_full_simp_tac ctxt 3, rtac @{thm conjI} 3, simp_tac ctxt 4, - REPEAT (rtac @{thm state_update_type} 3), + clarify_tac ctxt 3, + dresolve_tac ctxt @{thms swap} 3, force_tac ctxt 4, + resolve_tac ctxt @{thms ReplaceI} 3, force_tac ctxt 3, force_tac ctxt 4, + asm_full_simp_tac ctxt 3, resolve_tac ctxt @{thms conjI} 3, simp_tac ctxt 4, + REPEAT (resolve_tac ctxt @{thms state_update_type} 3), constrains_tac ctxt 1, ALLGOALS (clarify_tac ctxt), ALLGOALS (asm_full_simp_tac (ctxt addsimps [@{thm st_set_def}])),