--- 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
--- 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}]) @
--- 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 \<Longrightarrow> fix(f) ---> c"
--- 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
--- 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)
--- 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
(*>*) \<open>val thm =
Reification.conv @{context} @{thms interp.simps} @{cterm "x < y \<and> x < z"}\<close> (*<*)
-by (tactic \<open>ALLGOALS (rtac thm)\<close>)
+by (tactic \<open>ALLGOALS (resolve_tac @{context} [thm])\<close>)
(*>*)
text \<open>
--- 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 \<and> B"
- apply (tactic \<open>rtac @{thm conjI} 1\<close>)
+ apply (tactic \<open>resolve_tac @{context} @{thms conjI} 1\<close>)
using a apply (tactic \<open>resolve_tac @{context} facts 1\<close>)
using b apply (tactic \<open>resolve_tac @{context} facts 1\<close>)
done
@@ -374,7 +374,7 @@
using a and b
ML_val \<open>@{Isar.goal}\<close>
apply (tactic \<open>Method.insert_tac facts 1\<close>)
- apply (tactic \<open>(rtac @{thm conjI} THEN_ALL_NEW atac) 1\<close>)
+ apply (tactic \<open>(resolve_tac @{context} @{thms conjI} THEN_ALL_NEW assume_tac @{context}) 1\<close>)
done
end
--- 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"
\<open>val ctxt0 = @{context};
val (([(_, x)], [B]), ctxt1) = ctxt0
- |> Obtain.result (fn _ => etac @{thm exE} 1) [@{thm ex}];\<close>
+ |> Obtain.result (fn _ => eresolve_tac ctxt0 @{thms exE} 1) [@{thm ex}];\<close>
ML_prf %"ML"
\<open>singleton (Proof_Context.export ctxt1 ctxt0) @{thm refl};\<close>
ML_prf %"ML"
--- 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},
--- 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;
--- 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
--- 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*)
--- 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);
--- 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*)
--- 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);
--- 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},
--- 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"
--- 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"
--- 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"
--- 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},
--- 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},
--- 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"
--- 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)
--- 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-)};
*}
--- 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)
--- 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\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w, s') \<Longrightarrow> \<forall>m. n\<le>m \<longrightarrow> G\<turnstile>s \<midarrow>t\<succ>\<midarrow>m\<rightarrow> (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
--- 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)
--- 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>\<mu> R1 R2 (map_sp\<^sub>\<mu> f1 f2 sp) (map_sp\<^sub>\<mu> g1 g2 sp') =
rel_sp\<^sub>\<mu> (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>\<mu>.rel_compp sp\<^sub>\<mu>.rel_conversep sp\<^sub>\<mu>.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
*})
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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")
--- 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 =
--- 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)
--- 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 = \<bottom> \<Longrightarrow> R"
--- 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
--- 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
--- 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
--- 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]
--- 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
--- 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
--- 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*)
--- 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
--- 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;
--- 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 @@
--\<open>20 subgoals left\<close>
apply(tactic\<open>TRYALL (clarify_tac @{context})\<close>)
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
-apply(tactic \<open>TRYALL (etac disjE)\<close>)
+apply(tactic \<open>TRYALL (eresolve_tac @{context} [disjE])\<close>)
apply simp_all
-apply(tactic \<open>TRYALL(EVERY'[rtac disjI2,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac @{context}])\<close>)
-apply(tactic \<open>TRYALL(EVERY'[rtac disjI2,etac subset_trans,rtac @{thm Graph9},force_tac @{context}])\<close>)
-apply(tactic \<open>TRYALL(EVERY'[rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}])\<close>)
+apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI2],
+ resolve_tac @{context} [subset_trans],
+ eresolve_tac @{context} @{thms Graph3},
+ force_tac @{context},
+ assume_tac @{context}])\<close>)
+apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI2],
+ eresolve_tac @{context} [subset_trans],
+ resolve_tac @{context} @{thms Graph9},
+ force_tac @{context}])\<close>)
+apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI1],
+ eresolve_tac @{context} @{thms psubset_subset_trans},
+ resolve_tac @{context} @{thms Graph9},
+ force_tac @{context}])\<close>)
done
subsubsection \<open>Interference freedom Mutator-Collector\<close>
--- 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 @@
--\<open>14 subgoals left\<close>
apply(tactic \<open>TRYALL (clarify_tac @{context})\<close>)
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
-apply(tactic \<open>TRYALL (rtac conjI)\<close>)
-apply(tactic \<open>TRYALL (rtac impI)\<close>)
-apply(tactic \<open>TRYALL (etac disjE)\<close>)
-apply(tactic \<open>TRYALL (etac conjE)\<close>)
-apply(tactic \<open>TRYALL (etac disjE)\<close>)
-apply(tactic \<open>TRYALL (etac disjE)\<close>)
+apply(tactic \<open>TRYALL (resolve_tac @{context} [conjI])\<close>)
+apply(tactic \<open>TRYALL (resolve_tac @{context} [impI])\<close>)
+apply(tactic \<open>TRYALL (eresolve_tac @{context} [disjE])\<close>)
+apply(tactic \<open>TRYALL (eresolve_tac @{context} [conjE])\<close>)
+apply(tactic \<open>TRYALL (eresolve_tac @{context} [disjE])\<close>)
+apply(tactic \<open>TRYALL (eresolve_tac @{context} [disjE])\<close>)
--\<open>72 subgoals left\<close>
apply(simp_all add:Graph6 Graph7 Graph8 Append_to_free0 Append_to_free1 Graph12)
--\<open>35 subgoals left\<close>
-apply(tactic \<open>TRYALL(EVERY'[rtac disjI1,rtac subset_trans,etac @{thm Graph3},force_tac @{context}, assume_tac @{context}])\<close>)
+apply(tactic \<open>TRYALL(EVERY'[resolve_tac @{context} [disjI1],
+ resolve_tac @{context} [subset_trans],
+ eresolve_tac @{context} @{thms Graph3},
+ force_tac @{context},
+ assume_tac @{context}])\<close>)
--\<open>28 subgoals left\<close>
-apply(tactic \<open>TRYALL (etac conjE)\<close>)
-apply(tactic \<open>TRYALL (etac disjE)\<close>)
+apply(tactic \<open>TRYALL (eresolve_tac @{context} [conjE])\<close>)
+apply(tactic \<open>TRYALL (eresolve_tac @{context} [disjE])\<close>)
--\<open>34 subgoals left\<close>
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)
--\<open>47 subgoals left\<close>
-apply(tactic \<open>TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{context}])\<close>)
+apply(tactic \<open>TRYALL(EVERY'[REPEAT o resolve_tac @{context} [disjI2],
+ eresolve_tac @{context} @{thms subset_psubset_trans},
+ eresolve_tac @{context} @{thms Graph11},
+ force_tac @{context}])\<close>)
--\<open>41 subgoals left\<close>
-apply(tactic \<open>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}])])\<close>)
+apply(tactic \<open>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})])\<close>)
--\<open>35 subgoals left\<close>
-apply(tactic \<open>TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{context}])\<close>)
+apply(tactic \<open>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}])\<close>)
--\<open>31 subgoals left\<close>
-apply(tactic \<open>TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}])\<close>)
+apply(tactic \<open>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}])\<close>)
--\<open>29 subgoals left\<close>
-apply(tactic \<open>TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{context}])\<close>)
+apply(tactic \<open>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}])\<close>)
--\<open>25 subgoals left\<close>
-apply(tactic \<open>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}])])\<close>)
+apply(tactic \<open>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})])\<close>)
--\<open>10 subgoals left\<close>
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
--- 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 @@
--\<open>112 subgoals left\<close>
apply(simp_all (no_asm))
--\<open>43 subgoals left\<close>
-apply(tactic \<open>ALLGOALS (conjI_Tac (K all_tac))\<close>)
+apply(tactic \<open>ALLGOALS (conjI_Tac @{context} (K all_tac))\<close>)
--\<open>419 subgoals left\<close>
apply(tactic \<open>ALLGOALS (clarify_tac @{context})\<close>)
--\<open>99 subgoals left\<close>
--- 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:\<close>
ML \<open>
-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) )
\<close>
@@ -326,119 +326,123 @@
ML \<open>
-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])
\<close>
@@ -482,18 +486,18 @@
text \<open>Tactics useful for dealing with the generated verification conditions:\<close>
method_setup conjI_tac = \<open>
- Scan.succeed (K (SIMPLE_METHOD' (conjI_Tac (K all_tac))))\<close>
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (conjI_Tac ctxt (K all_tac)))\<close>
"verification condition generator for interference freedom tests"
ML \<open>
-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) )
\<close>
method_setup disjE_tac = \<open>
- Scan.succeed (K (SIMPLE_METHOD' (disjE_Tac (K all_tac))))\<close>
+ Scan.succeed (fn ctxt => SIMPLE_METHOD' (disjE_Tac ctxt (K all_tac)))\<close>
"verification condition generator for interference freedom tests"
end
--- 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)
--- 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)
--- 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: "<c,s> -n-> t ==> <c,s> -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,s> -c-> t ==> ? n. <c,s> -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,s> -c-> t = (? n. <c,s> -n-> t)"
--- 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
--- 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))
--- 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
--- 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
--- 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)
--- 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;
--- 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);
--- 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)])
--- 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'
--- 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)
--- 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)))
--- 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' |>
--- 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;
--- 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;
--- 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;
--- 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
--- 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
*}
--- 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
--- 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))
--- 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)
--- 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);
--- 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);
\<close>
@@ -797,7 +797,7 @@
ML \<open>
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) \<Turnstile> 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
--- 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: "\<lbrakk> sigma \<Turnstile> \<box>F; PROP W \<rbrakk> \<Longrightarrow> PROP W" .
ML \<open>
-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])
\<close>
-method_setup merge_box = \<open>Scan.succeed (K (SIMPLE_METHOD' merge_box_tac))\<close>
+method_setup merge_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_box_tac)\<close>
method_setup merge_temp_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_temp_box_tac)\<close>
method_setup merge_stp_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_stp_box_tac)\<close>
method_setup merge_act_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac)\<close>
@@ -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 \<turnstile> MyProg \<longrightarrow> \<box>Inv.
--- 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
--- 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 \<Longrightarrow> 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
\<lbrakk>A = True; B = False\<rbrakk> \<Longrightarrow> 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 \<longrightarrow> B \<longrightarrow> C) = False \<Longrightarrow> (A & B \<longrightarrow> C) = False" by auto}
- #> REPEAT_DETERM
+fun uncurry_lit_neg_tac ctxt =
+ REPEAT_DETERM o
+ dresolve_tac ctxt [@{lemma "(A \<longrightarrow> B \<longrightarrow> C) = False \<Longrightarrow> (A & B \<longrightarrow> 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: "\<lbrakk>Q; P\<rbrakk> \<Longrightarrow> 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
--- 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<Nclients.
ALL elt : set ((sub i o allocAsk) s). elt \<le> 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
--- 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];
*}
--- 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),
--- 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
--- 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 \<open>x = y\<close>]}.\<close>
have "x = y"
- by (tactic \<open>rtac @{thm \<open>x = y\<close>} 1\<close>) -- \<open>more cartouches involving ML\<close>
+ by (tactic \<open>resolve_tac @{context} @{thms \<open>x = y\<close>} 1\<close>) -- \<open>more cartouches involving ML\<close>
end
@@ -230,10 +230,10 @@
\<close>
lemma "A \<and> B \<longrightarrow> B \<and> A"
- apply (ml_tactic \<open>rtac @{thm impI} 1\<close>)
- apply (ml_tactic \<open>etac @{thm conjE} 1\<close>)
- apply (ml_tactic \<open>rtac @{thm conjI} 1\<close>)
- apply (ml_tactic \<open>ALLGOALS atac\<close>)
+ apply (ml_tactic \<open>resolve_tac @{context} @{thms impI} 1\<close>)
+ apply (ml_tactic \<open>eresolve_tac @{context} @{thms conjE} 1\<close>)
+ apply (ml_tactic \<open>resolve_tac @{context} @{thms conjI} 1\<close>)
+ apply (ml_tactic \<open>ALLGOALS (assume_tac @{context})\<close>)
done
lemma "A \<and> B \<longrightarrow> B \<and> A" by (ml_tactic \<open>blast_tac ctxt 1\<close>)
@@ -251,14 +251,17 @@
\<close>
lemma "A \<and> B \<longrightarrow> B \<and> A"
- apply \<open>rtac @{thm impI} 1\<close>
- apply \<open>etac @{thm conjE} 1\<close>
- apply \<open>rtac @{thm conjI} 1\<close>
- apply \<open>ALLGOALS atac\<close>
+ apply \<open>resolve_tac @{context} @{thms impI} 1\<close>
+ apply \<open>eresolve_tac @{context} @{thms conjE} 1\<close>
+ apply \<open>resolve_tac @{context} @{thms conjI} 1\<close>
+ apply \<open>ALLGOALS (assume_tac @{context})\<close>
done
lemma "A \<and> B \<longrightarrow> B \<and> A"
- by (\<open>rtac @{thm impI} 1\<close>, \<open>etac @{thm conjE} 1\<close>, \<open>rtac @{thm conjI} 1\<close>, \<open>atac 1\<close>+)
+ by (\<open>resolve_tac @{context} @{thms impI} 1\<close>,
+ \<open>eresolve_tac @{context} @{thms conjE} 1\<close>,
+ \<open>resolve_tac @{context} @{thms conjI} 1\<close>,
+ \<open>assume_tac @{context} 1\<close>+)
subsection \<open>ML syntax\<close>
--- 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 =
\<open>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))\<close>
--- 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
--- 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;
--- 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 *)
--- 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) *})
--- 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))
*}
--- 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 = {*
--- 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}])),