--- a/src/HOL/Fun.thy Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Fun.thy Thu Oct 30 22:45:19 2014 +0100
@@ -839,8 +839,8 @@
| (T, SOME rhs) =>
SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
(fn _ =>
- rtac eq_reflection 1 THEN
- rtac @{thm ext} 1 THEN
+ resolve_tac [eq_reflection] 1 THEN
+ resolve_tac @{thms ext} 1 THEN
simp_tac (put_simpset ss ctxt) 1))
end
in proc end
--- a/src/HOL/HOL.thy Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/HOL.thy Thu Oct 30 22:45:19 2014 +0100
@@ -905,7 +905,7 @@
apply (rule ex1E [OF major])
apply (rule prem)
apply (tactic {* ares_tac @{thms allI} 1 *})+
-apply (tactic {* etac (Classical.dup_elim @{thm allE}) 1 *})
+apply (tactic {* eresolve_tac [Classical.dup_elim @{thm allE}] 1 *})
apply iprover
done
@@ -1822,7 +1822,7 @@
proof
assume "PROP ?ofclass"
show "PROP ?equal"
- by (tactic {* ALLGOALS (rtac (Thm.unconstrainT @{thm eq_equal})) *})
+ by (tactic {* ALLGOALS (resolve_tac [Thm.unconstrainT @{thm eq_equal}]) *})
(fact `PROP ?ofclass`)
next
assume "PROP ?equal"
@@ -1921,7 +1921,10 @@
let
fun eval_tac ctxt =
let val conv = Code_Runtime.dynamic_holds_conv ctxt
- in CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN' rtac TrueI end
+ in
+ CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1 conv)) ctxt) THEN'
+ resolve_tac [TrueI]
+ end
in
Scan.succeed (SIMPLE_METHOD' o eval_tac)
end
@@ -1932,7 +1935,7 @@
SIMPLE_METHOD'
(CHANGED_PROP o
(CONVERSION (Nbe.dynamic_conv ctxt)
- THEN_ALL_NEW (TRY o rtac TrueI))))
+ THEN_ALL_NEW (TRY o resolve_tac [TrueI]))))
*} "solve goal by normalization"
@@ -1979,7 +1982,7 @@
val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
in
fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
- fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
+ fun smp_tac j = EVERY'[dresolve_tac (smp j), assume_tac];
end;
local
--- a/src/HOL/Product_Type.thy Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Product_Type.thy Thu Oct 30 22:45:19 2014 +0100
@@ -1324,9 +1324,10 @@
SOME (Goal.prove ctxt [] []
(Const (@{const_name Pure.eq}, T --> T --> propT) $ S $ S')
(K (EVERY
- [rtac eq_reflection 1, rtac @{thm subset_antisym} 1,
- rtac subsetI 1, dtac CollectD 1, simp,
- rtac subsetI 1, rtac CollectI 1, simp])))
+ [resolve_tac [eq_reflection] 1,
+ resolve_tac @{thms subset_antisym} 1,
+ resolve_tac [subsetI] 1, dresolve_tac [CollectD] 1, simp,
+ resolve_tac [subsetI] 1, resolve_tac [CollectI] 1, simp])))
end
else NONE)
| _ => NONE)
--- a/src/HOL/Set.thy Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Set.thy Thu Oct 30 22:45:19 2014 +0100
@@ -71,10 +71,11 @@
simproc_setup defined_Collect ("{x. P x & Q x}") = {*
fn _ => Quantifier1.rearrange_Collect
(fn _ =>
- rtac @{thm Collect_cong} 1 THEN
- rtac @{thm iffI} 1 THEN
+ resolve_tac @{thms Collect_cong} 1 THEN
+ resolve_tac @{thms iffI} 1 THEN
ALLGOALS
- (EVERY' [REPEAT_DETERM o etac @{thm conjE}, DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))
+ (EVERY' [REPEAT_DETERM o eresolve_tac @{thms conjE},
+ DEPTH_SOLVE_1 o ares_tac @{thms conjI}]))
*}
lemmas CollectE = CollectD [elim_format]
@@ -382,7 +383,7 @@
setup {*
map_theory_claset (fn ctxt =>
- ctxt addbefore ("bspec", fn _ => dtac @{thm bspec} THEN' assume_tac))
+ ctxt addbefore ("bspec", fn _ => dresolve_tac @{thms bspec} THEN' assume_tac))
*}
ML {*
--- a/src/HOL/Tools/Function/function_lib.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Tools/Function/function_lib.ML Thu Oct 30 22:45:19 2014 +0100
@@ -113,7 +113,7 @@
then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
(K (rewrite_goals_tac ctxt ac
- THEN rtac Drule.reflexive_thm 1))
+ THEN resolve_tac [Drule.reflexive_thm] 1))
end
(* instance for unions *)
--- a/src/HOL/Tools/Function/partial_function.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML Thu Oct 30 22:45:19 2014 +0100
@@ -90,7 +90,7 @@
if Term.is_open arg then no_tac
else ((DETERM o strip_cases o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0)
- THEN_ALL_NEW etac @{thm thin_rl}
+ THEN_ALL_NEW eresolve_tac @{thms thin_rl}
THEN_ALL_NEW (CONVERSION
(params_conv ~1 (fn ctxt' =>
arg_conv (arg_conv (abs_conv (K conv) ctxt'))) ctxt))) i
@@ -290,7 +290,7 @@
val rec_rule = let open Conv in
Goal.prove lthy' (map (fst o dest_Free) args) [] eqn (fn _ =>
CONVERSION ((arg_conv o arg1_conv o head_conv o rewr_conv) (mk_meta_eq unfold)) 1
- THEN rtac @{thm refl} 1) end;
+ THEN resolve_tac @{thms refl} 1) end;
in
lthy'
|> Local_Theory.note (eq_abinding, [rec_rule])
--- a/src/HOL/Tools/Meson/meson.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Tools/Meson/meson.ML Thu Oct 30 22:45:19 2014 +0100
@@ -167,19 +167,19 @@
(rename_bound_vars_RS th rl handle THM _ => tryall rls)
in tryall rls end;
-(* Special version of "rtac" that works around an explosion in the unifier.
+(* Special version of "resolve_tac" that works around an explosion in the unifier.
If the goal has the form "?P c", the danger is that resolving it against a
property of the form "... c ... c ... c ..." will lead to a huge unification
problem, due to the (spurious) choices between projection and imitation. The
workaround is to instantiate "?P := (%c. ... c ... c ... c ...)" manually. *)
-fun quant_rtac th i st =
+fun quant_resolve_tac th i st =
case (concl_of st, prop_of th) of
(@{const Trueprop} $ (Var _ $ (c as Free _)), @{const Trueprop} $ _) =>
let
val cc = cterm_of (theory_of_thm th) c
val ct = Thm.dest_arg (cprop_of th)
- in rtac th i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
- | _ => rtac th i st
+ in resolve_tac [th] i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
+ | _ => resolve_tac [th] i st
(*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
e.g. from conj_forward, should have the form
@@ -187,7 +187,7 @@
and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
fun forward_res ctxt nf st =
let
- fun tacf [prem] = quant_rtac (nf prem) 1
+ fun tacf [prem] = quant_resolve_tac (nf prem) 1
| tacf prems =
error (cat_lines
("Bad proof state in forward_res, please inform lcp@cl.cam.ac.uk:" ::
@@ -288,7 +288,7 @@
fun forward_res2 nf hyps st =
case Seq.pull
(REPEAT
- (Misc_Legacy.METAHYPS (fn major::minors => rtac (nf (minors@hyps) major) 1) 1)
+ (Misc_Legacy.METAHYPS (fn major::minors => resolve_tac [nf (minors @ hyps) major] 1) 1)
st)
of SOME(th,_) => th
| NONE => raise THM("forward_res2", 0, [st]);
@@ -700,14 +700,14 @@
fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
fun skolemize_prems_tac ctxt prems =
- cut_facts_tac (maps (try_skolemize_etc ctxt) prems) THEN' REPEAT o etac exE
+ cut_facts_tac (maps (try_skolemize_etc ctxt) prems) THEN' REPEAT o eresolve_tac [exE]
(*Basis of all meson-tactics. Supplies cltac with clauses: HOL disjunctions.
Function mkcl converts theorems to clauses.*)
fun MESON preskolem_tac mkcl cltac ctxt i st =
SELECT_GOAL
(EVERY [Object_Logic.atomize_prems_tac ctxt 1,
- rtac @{thm ccontr} 1,
+ resolve_tac @{thms ccontr} 1,
preskolem_tac,
Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
EVERY1 [skolemize_prems_tac ctxt negs,
--- a/src/HOL/Tools/Meson/meson_clausify.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Thu Oct 30 22:45:19 2014 +0100
@@ -208,8 +208,8 @@
|> Drule.beta_conv cabs |> Thm.apply cTrueprop
fun tacf [prem] =
rewrite_goals_tac ctxt @{thms skolem_def [abs_def]}
- THEN rtac ((prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]})
- RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex") 1
+ THEN resolve_tac [(prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]})
+ RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex"] 1
in
Goal.prove_internal ctxt [ex_tm] conc tacf
|> forall_intr_list frees
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Thu Oct 30 22:45:19 2014 +0100
@@ -531,7 +531,7 @@
if forall (curry (op =) 1) ns then all_tac else copy_prems_tac (rev ns) [] i
| copy_prems_tac (1 :: ms) ns i = rotate_tac 1 i THEN copy_prems_tac ms (1 :: ns) i
| copy_prems_tac (m :: ms) ns i =
- etac copy_prem i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
+ eresolve_tac [copy_prem] i THEN copy_prems_tac ms (m div 2 :: (m + 1) div 2 :: ns) i
(* Metis generates variables of the form _nnn. *)
val is_metis_fresh_variable = String.isPrefix "_"
@@ -578,10 +578,10 @@
end
| _ => raise Fail "expected a single non-zapped, non-Metis Var")
in
- (DETERM (etac @{thm allE} i THEN rotate_tac ~1 i) THEN PRIMITIVE do_instantiate) st
+ (DETERM (eresolve_tac @{thms allE} i THEN rotate_tac ~1 i) THEN PRIMITIVE do_instantiate) st
end
-fun fix_exists_tac t = etac exE THEN' rename_tac [t |> dest_Var |> fst |> fst]
+fun fix_exists_tac t = eresolve_tac [exE] THEN' rename_tac [t |> dest_Var |> fst |> fst]
fun release_quantifier_tac thy (skolem, t) =
(if skolem then fix_exists_tac else instantiate_forall_tac thy) t
@@ -730,7 +730,8 @@
cat_lines (map string_of_subst_info substs))
*)
- fun cut_and_ex_tac axiom = cut_tac axiom 1 THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
+ fun cut_and_ex_tac axiom =
+ cut_tac axiom 1 THEN TRY (REPEAT_ALL_NEW (eresolve_tac @{thms exE}) 1)
fun rotation_of_subgoal i =
find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
@@ -742,7 +743,7 @@
THEN copy_prems_tac (map snd ax_counts) [] 1)
THEN release_clusters_tac thy ax_counts substs ordered_clusters 1
THEN match_tac [prems_imp_false] 1
- THEN ALLGOALS (fn i => rtac @{thm Meson.skolem_COMBK_I} i
+ THEN ALLGOALS (fn i => resolve_tac @{thms Meson.skolem_COMBK_I} i
THEN rotate_tac (rotation_of_subgoal i) i
THEN PRIMITIVE (unify_first_prem_with_concl thy i)
THEN assume_tac i
--- a/src/HOL/Tools/Metis/metis_tactic.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Thu Oct 30 22:45:19 2014 +0100
@@ -61,7 +61,7 @@
fun lam_lifted_of_metis ctxt type_enc sym_tab concealed mth =
let
val thy = Proof_Context.theory_of ctxt
- val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN rtac refl 1
+ val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN resolve_tac [refl] 1
val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth
val ct = cterm_of thy (HOLogic.mk_Trueprop t)
in Goal.prove_internal ctxt [] ct (K tac) |> Meson.make_meta_clause end
@@ -102,7 +102,7 @@
so that "Thm.equal_elim" works below. *)
val t0 $ _ $ t2 = prop_of eq_th
val eq_ct = t0 $ prop_of th $ t2 |> cterm_of thy
- val eq_th' = Goal.prove_internal ctxt [] eq_ct (K (rtac eq_th 1))
+ val eq_th' = Goal.prove_internal ctxt [] eq_ct (K (resolve_tac [eq_th] 1))
in Thm.equal_elim eq_th' th end
fun clause_params ordering =
--- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Thu Oct 30 22:45:19 2014 +0100
@@ -150,7 +150,7 @@
NONE => NONE
| SOME u' => SOME (t |> getP |> snd |> head_of |> cert, cert u'))) (ts ~~ ts');
val indrule' = cterm_instantiate insts indrule;
- in rtac indrule' i end);
+ in resolve_tac [indrule'] i end);
(* perform exhaustive case analysis on last parameter of subgoal i *)
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML Thu Oct 30 22:45:19 2014 +0100
@@ -247,7 +247,8 @@
val rewrites = rec_rewrites' @ map (snd o snd) defs;
in
map (fn eq => Goal.prove ctxt frees [] eq
- (fn {context = ctxt', ...} => EVERY [rewrite_goals_tac ctxt' rewrites, rtac refl 1])) eqs
+ (fn {context = ctxt', ...} =>
+ EVERY [rewrite_goals_tac ctxt' rewrites, resolve_tac [refl] 1])) eqs
end;
in ((prefix, (fs, defs)), prove) end
handle PrimrecError (msg, some_eqn) =>
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Thu Oct 30 22:45:19 2014 +0100
@@ -57,10 +57,10 @@
(Logic.strip_imp_concl t)
(fn {prems, ...} =>
EVERY
- [rtac induct' 1,
- REPEAT (rtac TrueI 1),
- REPEAT ((rtac impI 1) THEN (eresolve_tac prems 1)),
- REPEAT (rtac TrueI 1)])
+ [resolve_tac [induct'] 1,
+ REPEAT (resolve_tac [TrueI] 1),
+ REPEAT ((resolve_tac [impI] 1) THEN (eresolve_tac prems 1)),
+ REPEAT (resolve_tac [TrueI] 1)])
end;
val casedist_thms =
@@ -176,16 +176,16 @@
in
(EVERY
[DETERM tac,
- REPEAT (etac @{thm ex1E} 1), rtac @{thm ex1I} 1,
+ REPEAT (eresolve_tac @{thms ex1E} 1), resolve_tac @{thms ex1I} 1,
DEPTH_SOLVE_1 (ares_tac [intr] 1),
- REPEAT_DETERM_N k (etac thin_rl 1 THEN rotate_tac 1 1),
- etac elim 1,
+ REPEAT_DETERM_N k (eresolve_tac [thin_rl] 1 THEN rotate_tac 1 1),
+ eresolve_tac [elim] 1,
REPEAT_DETERM_N j distinct_tac,
TRY (dresolve_tac inject 1),
- REPEAT (etac conjE 1), hyp_subst_tac ctxt 1,
- REPEAT (EVERY [etac allE 1, dtac mp 1, atac 1]),
+ REPEAT (eresolve_tac [conjE] 1), hyp_subst_tac ctxt 1,
+ REPEAT (EVERY [eresolve_tac [allE] 1, dresolve_tac [mp] 1, assume_tac 1]),
TRY (hyp_subst_tac ctxt 1),
- rtac refl 1,
+ resolve_tac [refl] 1,
REPEAT_DETERM_N (n - j - 1) distinct_tac],
intrs, j + 1)
end;
@@ -211,7 +211,7 @@
(HOLogic.mk_Trueprop (Old_Datatype_Aux.mk_conj rec_unique_ts))
(fn {context = ctxt, ...} =>
#1 (fold (mk_unique_tac ctxt) (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
- (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1 THEN
+ (((resolve_tac [induct'] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1 THEN
rewrite_goals_tac ctxt [mk_meta_eq @{thm choice_eq}], rec_intrs)))))
end;
@@ -254,10 +254,10 @@
Goal.prove_sorry_global thy2 [] [] t
(fn {context = ctxt, ...} => EVERY
[rewrite_goals_tac ctxt reccomb_defs,
- rtac @{thm the1_equality} 1,
+ resolve_tac @{thms the1_equality} 1,
resolve_tac rec_unique_thms 1,
resolve_tac rec_intrs 1,
- REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
+ REPEAT (resolve_tac [allI] 1 ORELSE resolve_tac rec_total_thms 1)]))
(Old_Datatype_Prop.make_primrecs reccomb_names descr thy2);
in
thy2
@@ -338,7 +338,8 @@
fun prove_case t =
Goal.prove_sorry_global thy2 [] [] t (fn {context = ctxt, ...} =>
- EVERY [rewrite_goals_tac ctxt (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1]);
+ EVERY [rewrite_goals_tac ctxt (case_defs @ map mk_meta_eq primrec_thms),
+ resolve_tac [refl] 1]);
fun prove_cases (Type (Tcon, _)) ts =
(case Ctr_Sugar.ctr_sugar_of ctxt Tcon of
@@ -379,7 +380,7 @@
val _ $ (_ $ lhs $ _) = hd (Logic.strip_assums_hyp (hd (prems_of exhaustion)));
val exhaustion' = cterm_instantiate [(cert lhs, cert (Free ("x", T)))] exhaustion;
fun tac ctxt =
- EVERY [rtac exhaustion' 1,
+ EVERY [resolve_tac [exhaustion'] 1,
ALLGOALS (asm_simp_tac
(put_simpset HOL_ss ctxt addsimps (dist_rewrites' @ inject @ case_thms')))];
in
@@ -405,7 +406,7 @@
let
fun prove_case_cong_weak t =
Goal.prove_sorry_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
- (fn {prems, ...} => EVERY [rtac (hd prems RS arg_cong) 1]);
+ (fn {prems, ...} => EVERY [resolve_tac [hd prems RS arg_cong] 1]);
val case_cong_weaks =
map prove_case_cong_weak (Old_Datatype_Prop.make_case_cong_weaks case_names descr thy);
@@ -423,12 +424,13 @@
let
(* For goal i, select the correct disjunct to attack, then prove it *)
fun tac ctxt i 0 =
- EVERY [TRY (rtac disjI1 i), hyp_subst_tac ctxt i, REPEAT (rtac exI i), rtac refl i]
- | tac ctxt i n = rtac disjI2 i THEN tac ctxt i (n - 1);
+ EVERY [TRY (resolve_tac [disjI1] i), hyp_subst_tac ctxt i,
+ REPEAT (resolve_tac [exI] i), resolve_tac [refl] i]
+ | tac ctxt i n = resolve_tac [disjI2] i THEN tac ctxt i (n - 1);
in
Goal.prove_sorry_global thy [] [] t
(fn {context = ctxt, ...} =>
- EVERY [rtac allI 1,
+ EVERY [resolve_tac [allI] 1,
Old_Datatype_Aux.exh_tac (K exhaustion) 1,
ALLGOALS (fn i => tac ctxt i (i - 1))])
end;
@@ -457,8 +459,8 @@
EVERY [
simp_tac (put_simpset HOL_ss ctxt addsimps [hd prems]) 1,
cut_tac nchotomy'' 1,
- REPEAT (etac disjE 1 THEN REPEAT (etac exE 1) THEN simplify 1),
- REPEAT (etac exE 1) THEN simplify 1 (* Get last disjunct *)]
+ REPEAT (eresolve_tac [disjE] 1 THEN REPEAT (eresolve_tac [exE] 1) THEN simplify 1),
+ REPEAT (eresolve_tac [exE] 1) THEN simplify 1 (* Get last disjunct *)]
end)
end;
--- a/src/HOL/Tools/cnf.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Tools/cnf.ML Thu Oct 30 22:45:19 2014 +0100
@@ -141,7 +141,7 @@
if i > nprems_of thm then
thm
else
- not_disj_to_prem (i+1) (Seq.hd (REPEAT_DETERM (rtac clause2raw_not_disj i) thm))
+ not_disj_to_prem (i+1) (Seq.hd (REPEAT_DETERM (resolve_tac [clause2raw_not_disj] i) thm))
(* moves all premises to hyps, i.e. "[...] |- A1 ==> ... ==> An ==> B" *)
(* becomes "[..., A1, ..., An] |- B" *)
(* Thm.thm -> Thm.thm *)
@@ -154,7 +154,7 @@
(* [...] |- ~x1 ==> ... ==> ~xn ==> False *)
|> not_disj_to_prem 1
(* [...] |- x1' ==> ... ==> xn' ==> False *)
- |> Seq.hd o TRYALL (rtac clause2raw_not_not)
+ |> Seq.hd o TRYALL (resolve_tac [clause2raw_not_not])
(* [..., x1', ..., xn'] |- False *)
|> prems_to_hyps
end;
@@ -529,7 +529,7 @@
(* ------------------------------------------------------------------------- *)
fun weakening_tac i =
- dtac weakening_thm i THEN atac (i+1);
+ dresolve_tac [weakening_thm] i THEN assume_tac (i+1);
(* ------------------------------------------------------------------------- *)
(* cnf_rewrite_tac: converts all premises of the 'i'-th subgoal to CNF *)
--- a/src/HOL/Tools/coinduction.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Tools/coinduction.ML Thu Oct 30 22:45:19 2014 +0100
@@ -37,7 +37,7 @@
let
val n = nth (prems_of st) (i - 1) |> Logic.strip_assums_hyp |> length;
in
- (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o etac thin_rl)) i st
+ (THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o eresolve_tac [thin_rl])) i st
end;
fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _, _) =>
@@ -87,13 +87,15 @@
val e = length eqs;
val p = length prems;
in
- HEADGOAL (EVERY' [rtac thm,
+ HEADGOAL (EVERY' [resolve_tac [thm],
EVERY' (map (fn var =>
- rtac (cterm_instantiate_pos [NONE, SOME (certify ctxt var)] exI)) vars),
- if p = 0 then CONJ_WRAP' (K (rtac refl)) eqs
- else REPEAT_DETERM_N e o (rtac conjI THEN' rtac refl) THEN' CONJ_WRAP' rtac prems,
+ resolve_tac [cterm_instantiate_pos [NONE, SOME (certify ctxt var)] exI]) vars),
+ if p = 0 then CONJ_WRAP' (K (resolve_tac [refl])) eqs
+ else
+ REPEAT_DETERM_N e o (resolve_tac [conjI] THEN' resolve_tac [refl]) THEN'
+ CONJ_WRAP' (resolve_tac o single) prems,
K (ALLGOALS_SKIP skip
- (REPEAT_DETERM_N (length vars) o (etac exE THEN' rotate_tac ~1) THEN'
+ (REPEAT_DETERM_N (length vars) o (eresolve_tac [exE] THEN' rotate_tac ~1) THEN'
DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
(case prems of
[] => all_tac
--- a/src/HOL/Tools/inductive.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Tools/inductive.ML Thu Oct 30 22:45:19 2014 +0100
@@ -169,8 +169,8 @@
| mk_names a n = map (fn i => a ^ string_of_int i) (1 upto n);
fun select_disj 1 1 = []
- | select_disj _ 1 = [rtac disjI1]
- | select_disj n i = rtac disjI2 :: select_disj (n - 1) (i - 1);
+ | select_disj _ 1 = [resolve_tac [disjI1]]
+ | select_disj n i = resolve_tac [disjI2] :: select_disj (n - 1) (i - 1);
@@ -378,12 +378,13 @@
[] []
(HOLogic.mk_Trueprop
(Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
- (fn _ => EVERY [rtac @{thm monoI} 1,
+ (fn _ => EVERY [resolve_tac @{thms monoI} 1,
REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI'}] 1),
REPEAT (FIRST
- [atac 1,
+ [assume_tac 1,
resolve_tac (map (mk_mono ctxt) monos @ get_monos ctxt) 1,
- etac @{thm le_funE} 1, dtac @{thm le_boolD} 1])]));
+ eresolve_tac @{thms le_funE} 1,
+ dresolve_tac @{thms le_boolD} 1])]));
(* prove introduction rules *)
@@ -401,7 +402,7 @@
val intrs = map_index (fn (i, intr) =>
Goal.prove_sorry ctxt [] [] intr (fn _ => EVERY
[rewrite_goals_tac ctxt rec_preds_defs,
- rtac (unfold RS iffD2) 1,
+ resolve_tac [unfold RS iffD2] 1,
EVERY1 (select_disj (length intr_ts) (i + 1)),
(*Not ares_tac, since refl must be tried before any equality assumptions;
backtracking may occur if the premises have extra variables!*)
@@ -447,7 +448,7 @@
(fn {context = ctxt4, prems} => EVERY
[cut_tac (hd prems) 1,
rewrite_goals_tac ctxt4 rec_preds_defs,
- dtac (unfold RS iffD1) 1,
+ dresolve_tac [unfold RS iffD1] 1,
REPEAT (FIRSTGOAL (eresolve_tac rules1)),
REPEAT (FIRSTGOAL (eresolve_tac rules2)),
EVERY (map (fn prem =>
@@ -494,37 +495,39 @@
val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
fun prove_intr1 (i, _) = Subgoal.FOCUS_PREMS (fn {params, prems, ...} =>
EVERY1 (select_disj (length c_intrs) (i + 1)) THEN
- EVERY (replicate (length params) (rtac @{thm exI} 1)) THEN
- (if null prems then rtac @{thm TrueI} 1
+ EVERY (replicate (length params) (resolve_tac @{thms exI} 1)) THEN
+ (if null prems then resolve_tac @{thms TrueI} 1
else
let
val (prems', last_prem) = split_last prems;
in
- EVERY (map (fn prem => (rtac @{thm conjI} 1 THEN rtac prem 1)) prems') THEN
- rtac last_prem 1
+ EVERY (map (fn prem =>
+ (resolve_tac @{thms conjI} 1 THEN resolve_tac [prem] 1)) prems') THEN
+ resolve_tac [last_prem] 1
end)) ctxt' 1;
fun prove_intr2 (((_, _, us, _), ts, params'), intr) =
- EVERY (replicate (length params') (etac @{thm exE} 1)) THEN
- (if null ts andalso null us then rtac intr 1
+ EVERY (replicate (length params') (eresolve_tac @{thms exE} 1)) THEN
+ (if null ts andalso null us then resolve_tac [intr] 1
else
- EVERY (replicate (length ts + length us - 1) (etac @{thm conjE} 1)) THEN
+ EVERY (replicate (length ts + length us - 1) (eresolve_tac @{thms conjE} 1)) THEN
Subgoal.FOCUS_PREMS (fn {context = ctxt'', params, prems, ...} =>
let
val (eqs, prems') = chop (length us) prems;
val rew_thms = map (fn th => th RS @{thm eq_reflection}) eqs;
in
rewrite_goal_tac ctxt'' rew_thms 1 THEN
- rtac intr 1 THEN
- EVERY (map (fn p => rtac p 1) prems')
+ resolve_tac [intr] 1 THEN
+ EVERY (map (fn p => resolve_tac [p] 1) prems')
end) ctxt' 1);
in
Goal.prove_sorry ctxt' [] [] eq (fn _ =>
- rtac @{thm iffI} 1 THEN etac (#1 elim) 1 THEN
+ resolve_tac @{thms iffI} 1 THEN
+ eresolve_tac [#1 elim] 1 THEN
EVERY (map_index prove_intr1 c_intrs) THEN
- (if null c_intrs then etac @{thm FalseE} 1
+ (if null c_intrs then eresolve_tac @{thms FalseE} 1
else
let val (c_intrs', last_c_intr) = split_last c_intrs in
- EVERY (map (fn ci => etac @{thm disjE} 1 THEN prove_intr2 ci) c_intrs') THEN
+ EVERY (map (fn ci => eresolve_tac @{thms disjE} 1 THEN prove_intr2 ci) c_intrs') THEN
prove_intr2 last_c_intr
end))
|> rulify ctxt'
@@ -729,16 +732,16 @@
val induct = Goal.prove_sorry ctxt'' [] ind_prems ind_concl
(fn {context = ctxt3, prems} => EVERY
[rewrite_goals_tac ctxt3 [inductive_conj_def],
- DETERM (rtac raw_fp_induct 1),
+ DETERM (resolve_tac [raw_fp_induct] 1),
REPEAT (resolve_tac [@{thm le_funI}, @{thm le_boolI}] 1),
rewrite_goals_tac ctxt3 simp_thms2,
(*This disjE separates out the introduction rules*)
REPEAT (FIRSTGOAL (eresolve_tac [disjE, exE, FalseE])),
(*Now break down the individual cases. No disjE here in case
some premise involves disjunction.*)
- REPEAT (FIRSTGOAL (etac conjE ORELSE' bound_hyp_subst_tac ctxt3)),
+ REPEAT (FIRSTGOAL (eresolve_tac [conjE] ORELSE' bound_hyp_subst_tac ctxt3)),
REPEAT (FIRSTGOAL
- (resolve_tac [conjI, impI] ORELSE' (etac notE THEN' atac))),
+ (resolve_tac [conjI, impI] ORELSE' (eresolve_tac [notE] THEN' assume_tac))),
EVERY (map (fn prem => DEPTH_SOLVE_1 (ares_tac [rewrite_rule ctxt3
(inductive_conj_def :: rec_preds_defs @ simp_thms2) prem,
conjI, refl] 1)) prems)]);
@@ -749,9 +752,9 @@
REPEAT (EVERY
[REPEAT (resolve_tac [conjI, impI] 1),
REPEAT (eresolve_tac [@{thm le_funE}, @{thm le_boolE}] 1),
- atac 1,
+ assume_tac 1,
rewrite_goals_tac ctxt3 simp_thms1,
- atac 1])]);
+ assume_tac 1])]);
in singleton (Proof_Context.export ctxt'' ctxt''') (induct RS lemma) end;
--- a/src/HOL/Tools/inductive_set.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Tools/inductive_set.ML Thu Oct 30 22:45:19 2014 +0100
@@ -75,11 +75,14 @@
SOME (close (Goal.prove ctxt [] [])
(Logic.mk_equals (t, fold_rev Term.abs xs (m $ p $ (bop $ S $ S'))))
(K (EVERY
- [rtac eq_reflection 1, REPEAT (rtac @{thm ext} 1), rtac iffI 1,
- EVERY [etac conjE 1, rtac IntI 1, simp, simp,
- etac IntE 1, rtac conjI 1, simp, simp] ORELSE
- EVERY [etac disjE 1, rtac UnI1 1, simp, rtac UnI2 1, simp,
- etac UnE 1, rtac disjI1 1, simp, rtac disjI2 1, simp]])))
+ [resolve_tac [eq_reflection] 1, REPEAT (resolve_tac @{thms ext} 1),
+ resolve_tac [iffI] 1,
+ EVERY [eresolve_tac [conjE] 1, resolve_tac [IntI] 1, simp, simp,
+ eresolve_tac [IntE] 1, resolve_tac [conjI] 1, simp, simp] ORELSE
+ EVERY [eresolve_tac [disjE] 1, resolve_tac [UnI1] 1, simp,
+ resolve_tac [UnI2] 1, simp,
+ eresolve_tac [UnE] 1, resolve_tac [disjI1] 1, simp,
+ resolve_tac [disjI2] 1, simp]])))
handle ERROR _ => NONE))
in
case strip_comb t of
@@ -502,8 +505,9 @@
fold_rev (Term.abs o pair "x") Ts
(HOLogic.mk_mem (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
list_comb (c, params))))))
- (K (REPEAT (rtac @{thm ext} 1) THEN simp_tac (put_simpset HOL_basic_ss lthy addsimps
- [def, mem_Collect_eq, @{thm split_conv}]) 1))
+ (K (REPEAT (resolve_tac @{thms ext} 1) THEN
+ simp_tac (put_simpset HOL_basic_ss lthy addsimps
+ [def, mem_Collect_eq, @{thm split_conv}]) 1))
in
lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
[Attrib.internal (K pred_set_conv_att)]),
--- a/src/HOL/Tools/lin_arith.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Tools/lin_arith.ML Thu Oct 30 22:45:19 2014 +0100
@@ -731,11 +731,11 @@
end)
in
EVERY' [
- REPEAT_DETERM o etac rev_mp,
+ REPEAT_DETERM o eresolve_tac [rev_mp],
cond_split_tac,
- rtac @{thm ccontr},
+ resolve_tac @{thms ccontr},
prem_nnf_tac ctxt,
- TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' etac disjE))
+ TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' eresolve_tac [disjE]))
]
end;
@@ -758,7 +758,7 @@
THEN_ALL_NEW
(CONVERSION Drule.beta_eta_conversion
THEN'
- (TRY o (etac notE THEN' eq_assume_tac)))
+ (TRY o (eresolve_tac [notE] THEN' eq_assume_tac)))
) i
)
end;
@@ -835,11 +835,12 @@
REPEAT_DETERM
(eresolve_tac [@{thm conjE}, @{thm exE}] 1 ORELSE
filter_prems_tac test 1 ORELSE
- etac @{thm disjE} 1) THEN
- (DETERM (etac @{thm notE} 1 THEN eq_assume_tac 1) ORELSE
+ eresolve_tac @{thms disjE} 1) THEN
+ (DETERM (eresolve_tac @{thms notE} 1 THEN eq_assume_tac 1) ORELSE
ref_tac 1);
in EVERY'[TRY o filter_prems_tac test,
- REPEAT_DETERM o etac @{thm rev_mp}, prep_tac, rtac @{thm ccontr}, prem_nnf_tac ctxt,
+ REPEAT_DETERM o eresolve_tac @{thms rev_mp}, prep_tac,
+ resolve_tac @{thms ccontr}, prem_nnf_tac ctxt,
SELECT_GOAL (DEPTH_SOLVE refute_prems_tac)]
end;
@@ -872,7 +873,8 @@
fun gen_tac ex ctxt =
FIRST' [simple_tac ctxt,
- Object_Logic.full_atomize_tac ctxt THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
+ Object_Logic.full_atomize_tac ctxt THEN'
+ (REPEAT_DETERM o resolve_tac [impI]) THEN' raw_tac ctxt ex];
val tac = gen_tac true;
--- a/src/HOL/Tools/sat.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Tools/sat.ML Thu Oct 30 22:45:19 2014 +0100
@@ -406,7 +406,7 @@
fun rawsat_tac ctxt i =
Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
- rtac (rawsat_thm ctxt' (map cprop_of prems)) 1) ctxt i;
+ resolve_tac [rawsat_thm ctxt' (map cprop_of prems)] 1) ctxt i;
(* ------------------------------------------------------------------------- *)
(* pre_cnf_tac: converts the i-th subgoal *)
@@ -421,7 +421,7 @@
(* ------------------------------------------------------------------------- *)
fun pre_cnf_tac ctxt =
- rtac @{thm ccontr} THEN'
+ resolve_tac @{thms ccontr} THEN'
Object_Logic.atomize_prems_tac ctxt THEN'
CONVERSION Drule.beta_eta_conversion;
@@ -433,7 +433,7 @@
(* ------------------------------------------------------------------------- *)
fun cnfsat_tac ctxt i =
- (etac FalseE i) ORELSE (REPEAT_DETERM (etac conjE i) THEN rawsat_tac ctxt i);
+ (eresolve_tac [FalseE] i) ORELSE (REPEAT_DETERM (eresolve_tac [conjE] i) THEN rawsat_tac ctxt i);
(* ------------------------------------------------------------------------- *)
(* cnfxsat_tac: checks if the empty clause "False" occurs among the *)
@@ -443,8 +443,8 @@
(* ------------------------------------------------------------------------- *)
fun cnfxsat_tac ctxt i =
- (etac FalseE i) ORELSE
- (REPEAT_DETERM (etac conjE i ORELSE etac exE i) THEN rawsat_tac ctxt i);
+ (eresolve_tac [FalseE] i) ORELSE
+ (REPEAT_DETERM (eresolve_tac [conjE] i ORELSE eresolve_tac [exE] i) THEN rawsat_tac ctxt i);
(* ------------------------------------------------------------------------- *)
(* sat_tac: tactic for calling an external SAT solver, taking as input an *)
--- a/src/HOL/Tools/set_comprehension_pointfree.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML Thu Oct 30 22:45:19 2014 +0100
@@ -314,95 +314,96 @@
val collectI' = @{lemma "\<not> P a ==> a \<notin> {x. P x}" by auto}
val collectE' = @{lemma "a \<notin> {x. P x} ==> (\<not> P a ==> Q) ==> Q" by auto}
-fun elim_Collect_tac ctxt = dtac @{thm iffD1[OF mem_Collect_eq]}
+fun elim_Collect_tac ctxt = dresolve_tac @{thms iffD1 [OF mem_Collect_eq]}
THEN' (REPEAT_DETERM o (eresolve_tac @{thms exE}))
- THEN' REPEAT_DETERM o etac @{thm conjE}
+ THEN' REPEAT_DETERM o eresolve_tac @{thms conjE}
THEN' TRY o hyp_subst_tac ctxt;
-fun intro_image_tac ctxt = rtac @{thm image_eqI}
+fun intro_image_tac ctxt = resolve_tac @{thms image_eqI}
THEN' (REPEAT_DETERM1 o
- (rtac @{thm refl}
- ORELSE' rtac
- @{thm arg_cong2[OF refl, where f="op =", OF prod.case, THEN iffD2]}
+ (resolve_tac @{thms refl}
+ ORELSE' resolve_tac @{thms arg_cong2 [OF refl, where f = "op =", OF prod.case, THEN iffD2]}
ORELSE' CONVERSION (Conv.params_conv ~1 (K (Conv.concl_conv ~1
(HOLogic.Trueprop_conv
(HOLogic.eq_conv Conv.all_conv (Conv.rewr_conv (mk_meta_eq case_prod_distrib)))))) ctxt)))
-fun elim_image_tac ctxt = etac @{thm imageE}
+fun elim_image_tac ctxt = eresolve_tac @{thms imageE}
THEN' REPEAT_DETERM o CHANGED o
(TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.case})
- THEN' REPEAT_DETERM o etac @{thm Pair_inject}
+ THEN' REPEAT_DETERM o eresolve_tac @{thms Pair_inject}
THEN' TRY o hyp_subst_tac ctxt)
fun tac1_of_formula ctxt (Int (fm1, fm2)) =
- TRY o etac @{thm conjE}
- THEN' rtac @{thm IntI}
+ TRY o eresolve_tac @{thms conjE}
+ THEN' resolve_tac @{thms IntI}
THEN' (fn i => tac1_of_formula ctxt fm2 (i + 1))
THEN' tac1_of_formula ctxt fm1
| tac1_of_formula ctxt (Un (fm1, fm2)) =
- etac @{thm disjE} THEN' rtac @{thm UnI1}
+ eresolve_tac @{thms disjE} THEN' resolve_tac @{thms UnI1}
THEN' tac1_of_formula ctxt fm1
- THEN' rtac @{thm UnI2}
+ THEN' resolve_tac @{thms UnI2}
THEN' tac1_of_formula ctxt fm2
| tac1_of_formula ctxt (Atom _) =
- REPEAT_DETERM1 o (atac
- ORELSE' rtac @{thm SigmaI}
- ORELSE' ((rtac @{thm CollectI} ORELSE' rtac collectI') THEN'
+ REPEAT_DETERM1 o (assume_tac
+ ORELSE' resolve_tac @{thms SigmaI}
+ ORELSE' ((resolve_tac @{thms CollectI} ORELSE' resolve_tac [collectI']) THEN'
TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]))
- ORELSE' ((rtac @{thm vimageI2} ORELSE' rtac vimageI2') THEN'
+ ORELSE' ((resolve_tac @{thms vimageI2} ORELSE' resolve_tac [vimageI2']) THEN'
TRY o simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]))
- ORELSE' (rtac @{thm image_eqI} THEN'
+ ORELSE' (resolve_tac @{thms image_eqI} THEN'
(REPEAT_DETERM o
- (rtac @{thm refl}
- ORELSE' rtac @{thm arg_cong2[OF refl, where f="op =", OF prod.case, THEN iffD2]})))
- ORELSE' rtac @{thm UNIV_I}
- ORELSE' rtac @{thm iffD2[OF Compl_iff]}
- ORELSE' atac)
+ (resolve_tac @{thms refl}
+ ORELSE' resolve_tac @{thms arg_cong2[OF refl, where f = "op =", OF prod.case, THEN iffD2]})))
+ ORELSE' resolve_tac @{thms UNIV_I}
+ ORELSE' resolve_tac @{thms iffD2[OF Compl_iff]}
+ ORELSE' assume_tac)
fun tac2_of_formula ctxt (Int (fm1, fm2)) =
- TRY o etac @{thm IntE}
- THEN' TRY o rtac @{thm conjI}
+ TRY o eresolve_tac @{thms IntE}
+ THEN' TRY o resolve_tac @{thms conjI}
THEN' (fn i => tac2_of_formula ctxt fm2 (i + 1))
THEN' tac2_of_formula ctxt fm1
| tac2_of_formula ctxt (Un (fm1, fm2)) =
- etac @{thm UnE} THEN' rtac @{thm disjI1}
+ eresolve_tac @{thms UnE} THEN' resolve_tac @{thms disjI1}
THEN' tac2_of_formula ctxt fm1
- THEN' rtac @{thm disjI2}
+ THEN' resolve_tac @{thms disjI2}
THEN' tac2_of_formula ctxt fm2
| tac2_of_formula ctxt (Atom _) =
REPEAT_DETERM o
- (atac
- ORELSE' dtac @{thm iffD1[OF mem_Sigma_iff]}
- ORELSE' etac @{thm conjE}
- ORELSE' ((etac @{thm CollectE} ORELSE' etac collectE') THEN'
+ (assume_tac
+ ORELSE' dresolve_tac @{thms iffD1[OF mem_Sigma_iff]}
+ ORELSE' eresolve_tac @{thms conjE}
+ ORELSE' ((eresolve_tac @{thms CollectE} ORELSE' eresolve_tac [collectE']) THEN'
TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}]) THEN'
- REPEAT_DETERM o etac @{thm Pair_inject} THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl})
- ORELSE' (etac @{thm imageE}
+ REPEAT_DETERM o eresolve_tac @{thms Pair_inject} THEN' TRY o hyp_subst_tac ctxt THEN'
+ TRY o resolve_tac @{thms refl})
+ ORELSE' (eresolve_tac @{thms imageE}
THEN' (REPEAT_DETERM o CHANGED o
(TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps @{thms split_paired_all prod.case})
- THEN' REPEAT_DETERM o etac @{thm Pair_inject}
- THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl})))
- ORELSE' etac @{thm ComplE}
- ORELSE' ((etac @{thm vimageE} ORELSE' etac vimageE')
+ THEN' REPEAT_DETERM o eresolve_tac @{thms Pair_inject}
+ THEN' TRY o hyp_subst_tac ctxt THEN' TRY o resolve_tac @{thms refl})))
+ ORELSE' eresolve_tac @{thms ComplE}
+ ORELSE' ((eresolve_tac @{thms vimageE} ORELSE' eresolve_tac [vimageE'])
THEN' TRY o full_simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm prod.case}])
- THEN' TRY o hyp_subst_tac ctxt THEN' TRY o rtac @{thm refl}))
+ THEN' TRY o hyp_subst_tac ctxt THEN' TRY o resolve_tac @{thms refl}))
fun tac ctxt fm =
let
- val subset_tac1 = rtac @{thm subsetI}
+ val subset_tac1 = resolve_tac @{thms subsetI}
THEN' elim_Collect_tac ctxt
THEN' intro_image_tac ctxt
THEN' tac1_of_formula ctxt fm
- val subset_tac2 = rtac @{thm subsetI}
+ val subset_tac2 = resolve_tac @{thms subsetI}
THEN' elim_image_tac ctxt
- THEN' rtac @{thm iffD2[OF mem_Collect_eq]}
+ THEN' resolve_tac @{thms iffD2[OF mem_Collect_eq]}
THEN' REPEAT_DETERM o resolve_tac @{thms exI}
- THEN' (TRY o REPEAT_ALL_NEW (rtac @{thm conjI}))
- THEN' (K (TRY (FIRSTGOAL ((TRY o hyp_subst_tac ctxt) THEN' rtac @{thm refl}))))
+ THEN' (TRY o REPEAT_ALL_NEW (resolve_tac @{thms conjI}))
+ THEN' (K (TRY (FIRSTGOAL ((TRY o hyp_subst_tac ctxt) THEN' resolve_tac @{thms refl}))))
THEN' (fn i => EVERY (rev (map_index (fn (j, f) =>
- REPEAT_DETERM (etac @{thm IntE} (i + j)) THEN tac2_of_formula ctxt f (i + j)) (strip_Int fm))))
+ REPEAT_DETERM (eresolve_tac @{thms IntE} (i + j)) THEN
+ tac2_of_formula ctxt f (i + j)) (strip_Int fm))))
in
- rtac @{thm subset_antisym} THEN' subset_tac1 THEN' subset_tac2
+ resolve_tac @{thms subset_antisym} THEN' subset_tac1 THEN' subset_tac2
end;
@@ -429,18 +430,18 @@
fun is_eq th = is_some (try (HOLogic.dest_eq o HOLogic.dest_Trueprop) (prop_of th))
val unfold_thms = @{thms split_paired_all mem_Collect_eq prod.case}
fun tac ctxt =
- rtac @{thm set_eqI}
+ resolve_tac @{thms set_eqI}
THEN' simp_tac (put_simpset HOL_basic_ss ctxt addsimps unfold_thms)
- THEN' rtac @{thm iffI}
- THEN' REPEAT_DETERM o rtac @{thm exI}
- THEN' rtac @{thm conjI} THEN' rtac @{thm refl} THEN' atac
- THEN' REPEAT_DETERM o etac @{thm exE}
- THEN' etac @{thm conjE}
- THEN' REPEAT_DETERM o etac @{thm Pair_inject}
+ THEN' resolve_tac @{thms iffI}
+ THEN' REPEAT_DETERM o resolve_tac @{thms exI}
+ THEN' resolve_tac @{thms conjI} THEN' resolve_tac @{thms refl} THEN' assume_tac
+ THEN' REPEAT_DETERM o eresolve_tac @{thms exE}
+ THEN' eresolve_tac @{thms conjE}
+ THEN' REPEAT_DETERM o eresolve_tac @{thms Pair_inject}
THEN' Subgoal.FOCUS (fn {prems, ...} =>
(* FIXME inner context!? *)
simp_tac (put_simpset HOL_basic_ss ctxt addsimps (filter is_eq prems)) 1) ctxt
- THEN' TRY o atac
+ THEN' TRY o assume_tac
in
case try mk_term (term_of ct) of
NONE => Thm.reflexive ct
--- a/src/HOL/Tools/simpdata.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/HOL/Tools/simpdata.ML Thu Oct 30 22:45:19 2014 +0100
@@ -81,7 +81,7 @@
(*Congruence rules for = (instead of ==)*)
fun mk_meta_cong (_: Proof.context) rl = zero_var_indexes
(let val rl' = Seq.hd (TRYALL (fn i => fn st =>
- rtac (lift_meta_eq_to_obj_eq i st) i st) rl)
+ resolve_tac [lift_meta_eq_to_obj_eq i st] i st) rl)
in mk_meta_eq rl' handle THM _ =>
if can Logic.dest_equals (concl_of rl') then rl'
else error "Conclusion of congruence rules must be =-equality"
@@ -119,7 +119,7 @@
val sol_thms =
reflexive_thm :: @{thm TrueI} :: @{thm refl} :: Simplifier.prems_of ctxt;
fun sol_tac i =
- FIRST [resolve_tac sol_thms i, atac i , etac @{thm FalseE} i] ORELSE
+ FIRST [resolve_tac sol_thms i, assume_tac i , eresolve_tac @{thms FalseE} i] ORELSE
(match_tac intros THEN_ALL_NEW sol_tac) i
in
(fn i => REPEAT_DETERM (match_tac @{thms simp_impliesI} i)) THEN' sol_tac
--- a/src/Provers/Arith/fast_lin_arith.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML Thu Oct 30 22:45:19 2014 +0100
@@ -815,7 +815,7 @@
all_tac) THEN
PRIMITIVE (trace_thm ctxt ["State after neqE:"]) THEN
(* use theorems generated from the actual justifications *)
- Subgoal.FOCUS (fn {prems, ...} => rtac (mkthm ctxt prems j) 1) ctxt i
+ Subgoal.FOCUS (fn {prems, ...} => resolve_tac [mkthm ctxt prems j] 1) ctxt i
in
(* rewrite "[| A1; ...; An |] ==> B" to "[| A1; ...; An; ~B |] ==> False" *)
DETERM (resolve_tac [LA_Logic.notI, LA_Logic.ccontr] i) THEN
--- a/src/Provers/order.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/Provers/order.ML Thu Oct 30 22:45:19 2014 +0100
@@ -1243,10 +1243,10 @@
in
Subgoal.FOCUS (fn {prems = asms, ...} =>
let val thms = map (prove (prems @ asms)) prfs
- in rtac (prove thms prf) 1 end) ctxt n st
+ in resolve_tac [prove thms prf] 1 end) ctxt n st
end
handle Contr p =>
- (Subgoal.FOCUS (fn {prems = asms, ...} => rtac (prove asms p) 1) ctxt n st
+ (Subgoal.FOCUS (fn {prems = asms, ...} => resolve_tac [prove asms p] 1) ctxt n st
handle General.Subscript => Seq.empty)
| Cannot => Seq.empty
| General.Subscript => Seq.empty)
--- a/src/Provers/quasi.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/Provers/quasi.ML Thu Oct 30 22:45:19 2014 +0100
@@ -565,9 +565,9 @@
in
Subgoal.FOCUS (fn {prems, ...} =>
let val thms = map (prove prems) prfs
- in rtac (prove thms prf) 1 end) ctxt n st
+ in resolve_tac [prove thms prf] 1 end) ctxt n st
end
- handle Contr p => Subgoal.FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
+ handle Contr p => Subgoal.FOCUS (fn {prems, ...} => resolve_tac [prove prems p] 1) ctxt n st
| Cannot => Seq.empty);
@@ -585,10 +585,10 @@
in
Subgoal.FOCUS (fn {prems, ...} =>
let val thms = map (prove prems) prfs
- in rtac (prove thms prf) 1 end) ctxt n st
+ in resolve_tac [prove thms prf] 1 end) ctxt n st
end
handle Contr p =>
- (Subgoal.FOCUS (fn {prems, ...} => rtac (prove prems p) 1) ctxt n st
+ (Subgoal.FOCUS (fn {prems, ...} => resolve_tac [prove prems p] 1) ctxt n st
handle General.Subscript => Seq.empty)
| Cannot => Seq.empty
| General.Subscript => Seq.empty);
--- a/src/Provers/trancl.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/Provers/trancl.ML Thu Oct 30 22:45:19 2014 +0100
@@ -545,7 +545,7 @@
let
val SOME (_, _, rel', _) = decomp (term_of concl);
val thms = map (prove thy rel' prems) prfs
- in rtac (prove thy rel' thms prf) 1 end) ctxt n st
+ in resolve_tac [prove thy rel' thms prf] 1 end) ctxt n st
end
handle Cannot => Seq.empty);
@@ -564,7 +564,7 @@
let
val SOME (_, _, rel', _) = decomp (term_of concl);
val thms = map (prove thy rel' prems) prfs
- in rtac (prove thy rel' thms prf) 1 end) ctxt n st
+ in resolve_tac [prove thy rel' thms prf] 1 end) ctxt n st
end
handle Cannot => Seq.empty | General.Subscript => Seq.empty);
--- a/src/Tools/coherent.ML Thu Oct 30 16:55:29 2014 +0100
+++ b/src/Tools/coherent.ML Thu Oct 30 22:45:19 2014 +0100
@@ -215,7 +215,7 @@
(** external interface **)
fun coherent_tac ctxt rules = SUBPROOF (fn {prems, concl, params, context = ctxt', ...} =>
- rtac (rulify_elim_conv ctxt' concl RS Drule.equal_elim_rule2) 1 THEN
+ resolve_tac [rulify_elim_conv ctxt' concl RS Drule.equal_elim_rule2] 1 THEN
SUBPROOF (fn {prems = prems', concl, context = ctxt'', ...} =>
let
val xs =
@@ -227,7 +227,7 @@
valid ctxt'' (map (mk_rule ctxt'') (prems' @ prems @ rules)) (term_of concl)
(mk_dom xs) Net.empty 0 0 of
NONE => no_tac
- | SOME prf => rtac (thm_of_cl_prf ctxt'' concl [] prf) 1)
+ | SOME prf => resolve_tac [thm_of_cl_prf ctxt'' concl [] prf] 1)
end) ctxt' 1) ctxt;
val _ = Theory.setup