proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
--- a/NEWS Sun Nov 09 11:05:20 2014 +0100
+++ b/NEWS Sun Nov 09 14:08:00 2014 +0100
@@ -190,6 +190,9 @@
*** ML ***
+* Proper context for various elementary tactics: compose_tac,
+Splitter.split_tac etc. Minor INCOMPATIBILITY.
+
* Tactical PARALLEL_ALLGOALS is the most common way to refer to
PARALLEL_GOALS.
--- a/src/Doc/Implementation/Tactic.thy Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Doc/Implementation/Tactic.thy Sun Nov 09 14:08:00 2014 +0100
@@ -492,14 +492,14 @@
text %mlref \<open>
\begin{mldecls}
- @{index_ML compose_tac: "(bool * thm * int) -> int -> tactic"} \\
+ @{index_ML compose_tac: "Proof.context -> (bool * thm * int) -> int -> tactic"} \\
@{index_ML Drule.compose: "thm * int * thm -> thm"} \\
@{index_ML_op COMP: "thm * thm -> thm"} \\
\end{mldecls}
\begin{description}
- \item @{ML compose_tac}~@{text "(flag, rule, m) i"} refines subgoal
+ \item @{ML compose_tac}~@{text "ctxt (flag, rule, m) i"} refines subgoal
@{text "i"} using @{text "rule"}, without lifting. The @{text
"rule"} is taken to have the form @{text "\<psi>\<^sub>1 \<Longrightarrow> \<dots> \<psi>\<^sub>m \<Longrightarrow> \<psi>"}, where
@{text "\<psi>"} need not be atomic; thus @{text "m"} determines the
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Sun Nov 09 14:08:00 2014 +0100
@@ -47,7 +47,7 @@
fun linr_tac ctxt q =
Object_Logic.atomize_prems_tac ctxt
- THEN' (REPEAT_DETERM o split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
+ THEN' (REPEAT_DETERM o split_tac ctxt [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
THEN' SUBGOAL (fn (g, i) =>
let
val thy = Proof_Context.theory_of ctxt
--- a/src/HOL/Decision_Procs/mir_tac.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML Sun Nov 09 14:08:00 2014 +0100
@@ -67,7 +67,7 @@
Object_Logic.atomize_prems_tac ctxt
THEN' simp_tac (put_simpset HOL_basic_ss ctxt
addsimps [@{thm "abs_ge_zero"}] addsimps @{thms simp_thms})
- THEN' (REPEAT_DETERM o split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
+ THEN' (REPEAT_DETERM o split_tac ctxt [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
THEN' SUBGOAL (fn (g, i) =>
let
val thy = Proof_Context.theory_of ctxt
--- a/src/HOL/HOL.thy Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/HOL.thy Sun Nov 09 14:08:00 2014 +0100
@@ -274,7 +274,7 @@
apply (rule refl)
done
-ML {* val cong_tac = Cong_Tac.cong_tac @{thm cong} *}
+ML {* fun cong_tac ctxt = Cong_Tac.cong_tac ctxt @{thm cong} *}
subsubsection {* Equality of booleans -- iff *}
--- a/src/HOL/HOLCF/Tr.thy Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/HOLCF/Tr.thy Sun Nov 09 14:08:00 2014 +0100
@@ -154,7 +154,7 @@
ML {*
fun split_If_tac ctxt =
simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm If2_def} RS sym])
- THEN' (split_tac [@{thm split_If2}])
+ THEN' (split_tac ctxt [@{thm split_If2}])
*}
subsection "Rewriting of HOLCF operations to HOL functions"
--- a/src/HOL/Library/simps_case_conv.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Library/simps_case_conv.ML Sun Nov 09 14:08:00 2014 +0100
@@ -88,7 +88,7 @@
fun tac ctxt {splits, intros, defs} =
let val ctxt' = Classical.addSIs (ctxt, intros) in
- REPEAT_DETERM1 (FIRSTGOAL (split_tac splits))
+ REPEAT_DETERM1 (FIRSTGOAL (split_tac ctxt splits))
THEN Local_Defs.unfold_tac ctxt defs
THEN safe_tac ctxt'
end
--- a/src/HOL/List.thy Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/List.thy Sun Nov 09 14:08:00 2014 +0100
@@ -610,7 +610,7 @@
| dest_if _ = NONE
fun tac _ [] = rtac set_singleton 1 ORELSE rtac inst_Collect_mem_eq 1
| tac ctxt (If :: cont) =
- Splitter.split_tac [@{thm split_if}] 1
+ Splitter.split_tac ctxt [@{thm split_if}] 1
THEN rtac @{thm conjI} 1
THEN rtac @{thm impI} 1
THEN Subgoal.FOCUS (fn {prems, context, ...} =>
@@ -631,7 +631,7 @@
Ctr_Sugar.ctr_sugar_of ctxt (fst (dest_Type T))
in
(* do case distinction *)
- Splitter.split_tac [split] 1
+ Splitter.split_tac ctxt [split] 1
THEN EVERY (map_index (fn (i', _) =>
(if i' < length case_thms - 1 then rtac @{thm conjI} 1 else all_tac)
THEN REPEAT_DETERM (rtac @{thm allI} 1)
--- a/src/HOL/Nominal/nominal_datatype.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Sun Nov 09 14:08:00 2014 +0100
@@ -654,7 +654,7 @@
((Rep RS perm_closed1 RS Abs_inverse) ::
(if atom1 = atom2 then []
else [Rep RS perm_closed2 RS Abs_inverse]))) 1,
- cong_tac 1,
+ cong_tac ctxt 1,
rtac refl 1,
rtac cp1' 1]) thy)
(Abs_inverse_thms ~~ Rep_thms ~~ perm_defs ~~ new_type_names ~~
--- a/src/HOL/Nominal/nominal_fresh_fun.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML Sun Nov 09 14:08:00 2014 +0100
@@ -10,7 +10,7 @@
(* FIXME res_inst_tac mostly obsolete, cf. Subgoal.FOCUS *)
(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
-fun gen_res_inst_tac_term instf tyinst tinst elim th i st =
+fun gen_res_inst_tac_term ctxt instf tyinst tinst elim th i st =
let
val thy = theory_of_thm st;
val cgoal = nth (cprems_of st) (i - 1);
@@ -27,18 +27,18 @@
(map (pairself (cterm_of thy)) tinst')
(Thm.lift_rule cgoal th)
in
- compose_tac (elim, th', nprems_of th) i st
+ compose_tac ctxt (elim, th', nprems_of th) i st
end handle General.Subscript => Seq.empty;
(* FIXME proper SUBGOAL/CSUBGOAL instead of cprems_of etc. *)
-val res_inst_tac_term =
- gen_res_inst_tac_term (curry Thm.instantiate);
+fun res_inst_tac_term ctxt =
+ gen_res_inst_tac_term ctxt (curry Thm.instantiate);
-val res_inst_tac_term' =
- gen_res_inst_tac_term (K Drule.cterm_instantiate) [];
+fun res_inst_tac_term' ctxt =
+ gen_res_inst_tac_term ctxt (K Drule.cterm_instantiate) [];
fun cut_inst_tac_term' ctxt tinst th =
- res_inst_tac_term' tinst false (Rule_Insts.make_elim_preserve ctxt th);
+ res_inst_tac_term' ctxt tinst false (Rule_Insts.make_elim_preserve ctxt th);
fun get_dyn_thm thy name atom_name =
Global_Theory.get_thm thy name handle ERROR _ =>
--- a/src/HOL/Nominal/nominal_permeq.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Nominal/nominal_permeq.ML Sun Nov 09 14:08:00 2014 +0100
@@ -227,7 +227,7 @@
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);
-fun apply_cong_tac i = ("application of congruence", cong_tac i);
+fun apply_cong_tac ctxt i = ("application of congruence", cong_tac ctxt i);
(* unfolds the definition of permutations *)
@@ -256,7 +256,7 @@
(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 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))))
@@ -315,7 +315,7 @@
val ctxt' = ctxt addsimps [supp_prod,supp_unit,finite_Un,finite_emptyI,conj_absorb]@fin_supp
in
(tactical ctxt ("guessing of the right supports-set",
- EVERY [compose_tac (false, supports_rule'', 2) i,
+ EVERY [compose_tac ctxt (false, supports_rule'', 2) i,
asm_full_simp_tac ctxt' (i+1),
supports_tac_i tactical ctxt i])) st
end
@@ -357,7 +357,7 @@
[(cert (head_of S), cert s')] supports_fresh_rule'
in
(tactical ctxt ("guessing of the right set that supports the goal",
- (EVERY [compose_tac (false, supports_fresh_rule'', 3) i,
+ (EVERY [compose_tac ctxt (false, supports_fresh_rule'', 3) i,
asm_full_simp_tac ctxt1 (i+2),
asm_full_simp_tac ctxt2 (i+1),
supports_tac_i tactical ctxt i]))) st
--- a/src/HOL/Nominal/nominal_primrec.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Sun Nov 09 14:08:00 2014 +0100
@@ -376,7 +376,7 @@
Proof.apply (Method.Basic (fn ctxt => fn _ =>
NO_CASES
(rewrite_goals_tac ctxt defs_thms THEN
- compose_tac (false, rule, length rule_prems) 1))) |>
+ compose_tac ctxt (false, rule, length rule_prems) 1))) |>
Seq.hd
end;
--- a/src/HOL/SPARK/Tools/spark_vcs.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/SPARK/Tools/spark_vcs.ML Sun Nov 09 14:08:00 2014 +0100
@@ -209,7 +209,7 @@
(fn _ =>
rtac @{thm subset_antisym} 1 THEN
rtac @{thm subsetI} 1 THEN
- Old_Datatype_Aux.exh_tac (K (#exhaust (BNF_LFP_Compat.the_info
+ 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));
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Sun Nov 09 14:08:00 2014 +0100
@@ -133,8 +133,8 @@
HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE'
eresolve_tac falseEs ORELSE'
resolve_tac split_connectI ORELSE'
- Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
- Splitter.split_tac (split_if :: splits) ORELSE'
+ Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE'
+ Splitter.split_tac ctxt (split_if :: splits) ORELSE'
eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
etac notE THEN' atac ORELSE'
(CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
@@ -171,8 +171,8 @@
SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
(rtac refl ORELSE' atac ORELSE'
resolve_tac (@{thm Code.abort_def} :: split_connectI) ORELSE'
- Splitter.split_tac (split_if :: splits) ORELSE'
- Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
+ Splitter.split_tac ctxt (split_if :: splits) ORELSE'
+ Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE'
mk_primcorec_assumption_tac ctxt discIs ORELSE'
distinct_in_prems_tac distincts ORELSE'
(TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))))
@@ -204,7 +204,7 @@
SELECT_GOAL (unfold_thms_tac ctxt unfold_lets) THEN' REPEAT_DETERM o
(rtac refl ORELSE' atac ORELSE'
resolve_tac split_connectI ORELSE'
- Splitter.split_tac (split_if :: splits) ORELSE'
+ Splitter.split_tac ctxt (split_if :: splits) ORELSE'
distinct_in_prems_tac distincts ORELSE'
rtac sym THEN' atac ORELSE'
etac notE THEN' atac));
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Sun Nov 09 14:08:00 2014 +0100
@@ -421,7 +421,7 @@
[(Old_Datatype_Aux.ind_tac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac ctxt) 1,
REPEAT (EVERY
[rtac allI 1, rtac impI 1,
- Old_Datatype_Aux.exh_tac (exh_thm_of dt_info) 1,
+ Old_Datatype_Aux.exh_tac ctxt (exh_thm_of dt_info) 1,
REPEAT (EVERY
[hyp_subst_tac ctxt 1,
rewrite_goals_tac ctxt rewrites,
@@ -430,7 +430,7 @@
ORELSE (EVERY
[REPEAT (eresolve_tac (Scons_inject ::
map make_elim [Leaf_inject, Inl_inject, Inr_inject]) 1),
- REPEAT (cong_tac 1), rtac refl 1,
+ REPEAT (cong_tac ctxt 1), rtac refl 1,
REPEAT (atac 1 ORELSE (EVERY
[REPEAT (rtac @{thm ext} 1),
REPEAT (eresolve_tac (mp :: allE ::
--- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML Sun Nov 09 14:08:00 2014 +0100
@@ -53,7 +53,7 @@
val app_bnds : term -> int -> term
val ind_tac : thm -> string list -> int -> tactic
- val exh_tac : (string -> thm) -> int -> tactic
+ val exh_tac : Proof.context -> (string -> thm) -> int -> tactic
exception Datatype
exception Datatype_Empty of string
@@ -155,7 +155,7 @@
(* perform exhaustive case analysis on last parameter of subgoal i *)
-fun exh_tac exh_thm_of = CSUBGOAL (fn (cgoal, i) =>
+fun exh_tac ctxt exh_thm_of = CSUBGOAL (fn (cgoal, i) =>
let
val thy = Thm.theory_of_cterm cgoal;
val goal = term_of cgoal;
@@ -167,7 +167,7 @@
val exhaustion' =
cterm_instantiate [(cterm_of thy (head_of lhs),
cterm_of thy (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))] exhaustion;
- in compose_tac (false, exhaustion', nprems_of exhaustion) i end);
+ in compose_tac ctxt (false, exhaustion', nprems_of exhaustion) i end);
(********************** Internal description of datatypes *********************)
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML Sun Nov 09 14:08:00 2014 +0100
@@ -431,7 +431,7 @@
Goal.prove_sorry_global thy [] [] t
(fn {context = ctxt, ...} =>
EVERY [resolve_tac [allI] 1,
- Old_Datatype_Aux.exh_tac (K exhaustion) 1,
+ Old_Datatype_Aux.exh_tac ctxt (K exhaustion) 1,
ALLGOALS (fn i => tac ctxt i (i - 1))])
end;
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML Sun Nov 09 14:08:00 2014 +0100
@@ -308,7 +308,7 @@
in
trace_tac ctxt options ("Term " ^ (Syntax.string_of_term ctxt t) ^
" splitting with rules \n" ^ Display.string_of_thm ctxt split_asm)
- THEN TRY (Splitter.split_asm_tac [split_asm] 1
+ THEN TRY (Splitter.split_asm_tac ctxt [split_asm] 1
THEN (trace_tac ctxt options "after splitting with split_asm rules")
(* THEN (Simplifier.asm_full_simp_tac (put_simpset HOL_basic_ss ctxt) 1)
THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
@@ -320,7 +320,7 @@
else all_tac
in
split_term_tac (HOLogic.mk_tuple out_ts)
- THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1)
+ THEN (DETERM (TRY ((Splitter.split_asm_tac ctxt [@{thm "split_if_asm"}] 1)
THEN (etac @{thm botE} 2))))
end
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Nov 09 14:08:00 2014 +0100
@@ -392,7 +392,7 @@
(* (op =) (t $ ...) (t' $ ...) ----> Cong provided type of t does not need lifting *)
(* merge with previous tactic *)
- Cong_Tac.cong_tac @{thm cong} THEN'
+ Cong_Tac.cong_tac ctxt @{thm cong} THEN'
RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
(* resolving with R x y assumptions *)
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML Sun Nov 09 14:08:00 2014 +0100
@@ -308,14 +308,14 @@
(* congruence *)
-fun ctac prems i st = st |> (
+fun ctac ctxt prems i st = st |> (
resolve_tac (@{thm refl} :: prems) i
- ORELSE (cong_tac i THEN ctac prems (i + 1) THEN ctac prems i))
+ ORELSE (cong_tac ctxt i THEN ctac ctxt prems (i + 1) THEN ctac ctxt prems i))
fun cong_basic ctxt thms t =
let val st = Thm.trivial (certify_prop ctxt t)
in
- (case Seq.pull (ctac thms 1 st) of
+ (case Seq.pull (ctac ctxt thms 1 st) of
SOME (thm, _) => thm
| NONE => raise THM ("cong", 0, thms @ [st]))
end
--- a/src/HOL/Tools/lin_arith.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Tools/lin_arith.ML Sun Nov 09 14:08:00 2014 +0100
@@ -723,7 +723,7 @@
if null splits orelse length splits > Config.get ctxt split_limit then
no_tac
else if null (#2 (hd splits)) then
- split_tac split_thms i
+ split_tac ctxt split_thms i
else
(* disallow a split that involves non-locally bound variables *)
(* (except when bound by outermost meta-quantifiers) *)
@@ -866,7 +866,7 @@
(* split_limit may trigger. *)
(* Therefore splitting outside of simple_tac may allow us to prove *)
(* some goals that simple_tac alone would fail on. *)
- (REPEAT_DETERM o split_tac (#splits (get_arith_data ctxt)))
+ (REPEAT_DETERM o split_tac ctxt (#splits (get_arith_data ctxt)))
(lin_arith_tac ctxt ex);
in
--- a/src/HOL/Tools/record.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/Tools/record.ML Sun Nov 09 14:08:00 2014 +0100
@@ -1458,7 +1458,7 @@
(or on s if there are no parameters).
Instatiation of record variable (and predicate) in rule is calculated to
avoid problems with higher order unification.*)
-fun try_param_tac s rule = CSUBGOAL (fn (cgoal, i) =>
+fun try_param_tac ctxt s rule = CSUBGOAL (fn (cgoal, i) =>
let
val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
@@ -1484,7 +1484,7 @@
| (_, T) :: _ =>
[(P, fold_rev Term.abs params (if ca then concl else incr_boundvars 1 (Abs (s, T, concl)))),
(x, fold_rev Term.abs params (Bound 0))])) rule';
- in compose_tac (false, rule'', nprems_of rule) i end);
+ in compose_tac ctxt (false, rule'', nprems_of rule) i end);
fun extension_definition name fields alphas zeta moreT more vars thy =
@@ -2119,15 +2119,16 @@
Goal.prove_sorry_global defs_thy [] [] induct_scheme_prop
(fn {context = ctxt, ...} =>
EVERY
- [case parent_induct of NONE => all_tac | SOME ind => try_param_tac rN ind 1,
- try_param_tac rN ext_induct 1,
+ [case parent_induct of NONE => all_tac | SOME ind => try_param_tac ctxt rN ind 1,
+ try_param_tac ctxt rN ext_induct 1,
asm_simp_tac (put_simpset HOL_basic_ss ctxt) 1]));
val induct = timeit_msg ctxt "record induct proof:" (fn () =>
- Goal.prove_sorry_global defs_thy [] [#1 induct_prop] (#2 induct_prop) (fn {prems, ...} =>
- try_param_tac rN induct_scheme 1
- THEN try_param_tac "more" @{thm unit.induct} 1
- THEN resolve_tac prems 1));
+ Goal.prove_sorry_global defs_thy [] [#1 induct_prop] (#2 induct_prop)
+ (fn {context = ctxt, prems, ...} =>
+ try_param_tac ctxt rN induct_scheme 1
+ THEN try_param_tac ctxt "more" @{thm unit.induct} 1
+ THEN resolve_tac prems 1));
val surjective = timeit_msg ctxt "record surjective proof:" (fn () =>
Goal.prove_sorry_global defs_thy [] [] surjective_prop
@@ -2150,7 +2151,7 @@
val cases = timeit_msg ctxt "record cases proof:" (fn () =>
Goal.prove_sorry_global defs_thy [] [] cases_prop
(fn {context = ctxt, ...} =>
- try_param_tac rN cases_scheme 1 THEN
+ try_param_tac ctxt rN cases_scheme 1 THEN
ALLGOALS (asm_full_simp_tac
(put_simpset HOL_basic_ss ctxt addsimps @{thms unit_all_eq1}))));
--- a/src/HOL/ex/SVC_Oracle.thy Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/ex/SVC_Oracle.thy Sun Nov 09 14:08:00 2014 +0100
@@ -109,13 +109,15 @@
abstracted. Use via compose_tac, which performs no lifting but will
instantiate variables.*)
-val svc_tac = CSUBGOAL (fn (ct, i) =>
+fun svc_tac ctxt = CSUBGOAL (fn (ct, i) =>
let
val thy = Thm.theory_of_cterm ct;
val (abs_goal, _) = svc_abstract (Thm.term_of ct);
val th = svc_oracle (Thm.cterm_of thy abs_goal);
- in compose_tac (false, th, 0) i end
+ in compose_tac ctxt (false, th, 0) i end
handle TERM _ => no_tac);
*}
+method_setup svc = {* Scan.succeed (SIMPLE_METHOD' o svc_tac) *}
+
end
--- a/src/HOL/ex/svc_test.thy Sun Nov 09 11:05:20 2014 +0100
+++ b/src/HOL/ex/svc_test.thy Sun Nov 09 14:08:00 2014 +0100
@@ -11,7 +11,7 @@
in its length, though @{text "fast"} manages.
*}
lemma "P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P=P"
- by (tactic {* svc_tac 1 *})
+ by svc
subsection {* Some big tautologies supplied by John Harrison *}
@@ -39,7 +39,7 @@
(~v4 | v5 | v6) &
(~v7 | ~v8 | v9) &
(~v10 | ~v11 | v12))"
- by (tactic {* svc_tac 1 *})
+ by svc
lemma dk17_be:
"(GE17 <-> ~IN4 & ~IN3 & ~IN2 & ~IN1) &
@@ -117,7 +117,7 @@
(OUT2 <-> WRES8 & ~IN9 | WRES10 & IN8) &
(OUT1 <-> WRES7 & IN8) &
(OUT0 <-> WRES7 & ~IN8)"
- by (tactic {* svc_tac 1 *})
+ by svc
text {* @{text "fast"} only takes a couple of seconds. *}
@@ -221,7 +221,7 @@
WRES16 & WRES7 |
WRES18 & WRES0 & ~IN5 |
WRES19)"
- by (tactic {* svc_tac 1 *})
+ by svc
subsection {* Linear arithmetic *}
@@ -229,20 +229,20 @@
lemma "x ~= 14 & x ~= 13 & x ~= 12 & x ~= 11 & x ~= 10 & x ~= 9 &
x ~= 8 & x ~= 7 & x ~= 6 & x ~= 5 & x ~= 4 & x ~= 3 &
x ~= 2 & x ~= 1 & 0 < x & x < 16 --> 15 = (x::int)"
- by (tactic {* svc_tac 1 *})
+ by svc
text {*merely to test polarity handling in the presence of biconditionals*}
lemma "(x < (y::int)) = (x+1 <= y)"
- by (tactic {* svc_tac 1 *})
+ by svc
subsection {* Natural number examples requiring implicit "non-negative" assumptions *}
lemma "(3::nat)*a <= 2 + 4*b + 6*c & 11 <= 2*a + b + 2*c &
a + 3*b <= 5 + 2*c --> 2 + 3*b <= 2*a + 6*c"
- by (tactic {* svc_tac 1 *})
+ by svc
lemma "(n::nat) < 2 ==> (n = 0) | (n = 1)"
- by (tactic {* svc_tac 1 *})
+ by svc
end
--- a/src/Provers/blast.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Provers/blast.ML Sun Nov 09 14:08:00 2014 +0100
@@ -43,7 +43,7 @@
val not_name: string
val notE: thm (* [| ~P; P |] ==> R *)
val ccontr: thm
- val hyp_subst_tac: bool -> int -> tactic
+ val hyp_subst_tac: Proof.context -> bool -> int -> tactic
end;
signature BLAST =
@@ -1021,7 +1021,7 @@
trace_prover state brs0;
if lim<0 then (cond_tracing trace (fn () => "Limit reached."); backtrack trace choices)
else
- prv (Data.hyp_subst_tac trace :: tacs,
+ prv (Data.hyp_subst_tac ctxt trace :: tacs,
brs0::trs, choices,
equalSubst ctxt
(G, {pairs = (br,haz)::pairs,
--- a/src/Provers/hypsubst.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Provers/hypsubst.ML Sun Nov 09 14:08:00 2014 +0100
@@ -50,7 +50,7 @@
val hyp_subst_tac_thin : bool -> Proof.context -> int -> tactic
val hyp_subst_thin : bool Config.T
val hyp_subst_tac : Proof.context -> int -> tactic
- val blast_hyp_subst_tac : bool -> int -> tactic
+ val blast_hyp_subst_tac : Proof.context -> bool -> int -> tactic
val stac : thm -> int -> tactic
end;
@@ -162,11 +162,12 @@
val ssubst = Drule.zero_var_indexes (Data.sym RS Data.subst);
-fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) =>
+fun inst_subst_tac ctxt b rl = CSUBGOAL (fn (cBi, i) =>
case try (Logic.strip_assums_hyp #> hd #>
Data.dest_Trueprop #> Data.dest_eq #> pairself contract) (Thm.term_of cBi) of
SOME (t, t') =>
let
+ val thy = Proof_Context.theory_of ctxt;
val Bi = Thm.term_of cBi;
val ps = Logic.strip_params Bi;
val U = Term.fastype_of1 (rev (map snd ps), t);
@@ -182,10 +183,9 @@
(case (if b then t else t') of
Bound j => subst_bounds (map Bound ((1 upto j) @ 0 :: (j + 2 upto length ps)), Q)
| t => Term.abstract_over (t, Term.incr_boundvars 1 Q));
- val thy = Thm.theory_of_thm rl';
val (instT, _) = Thm.match (pairself (cterm_of thy o Logic.mk_type) (V, U));
in
- compose_tac (true, Drule.instantiate_normalize (instT,
+ compose_tac ctxt (true, Drule.instantiate_normalize (instT,
map (pairself (cterm_of thy))
[(Var (ixn, Ts ---> U --> body_type T), u),
(Var (fst (dest_Var (head_of v1)), Ts ---> U), fold_rev Term.abs ps t),
@@ -204,7 +204,7 @@
(*Old version of the tactic above -- slower but the only way
to handle equalities containing Vars.*)
-fun vars_gen_hyp_subst_tac bnd = SUBGOAL(fn (Bi,i) =>
+fun vars_gen_hyp_subst_tac ctxt bnd = SUBGOAL(fn (Bi,i) =>
let val n = length(Logic.strip_assums_hyp Bi) - 1
val (k, (orient, is_free)) = eq_var bnd false true Bi
val rl = if is_free then dup_subst else ssubst
@@ -214,7 +214,7 @@
(EVERY [REPEAT_DETERM_N k (eresolve_tac [Data.rev_mp] i),
rotate_tac 1 i,
REPEAT_DETERM_N (n-k) (eresolve_tac [Data.rev_mp] i),
- inst_subst_tac orient rl i,
+ inst_subst_tac ctxt orient rl i,
REPEAT_DETERM_N n (imp_intr_tac i THEN rotate_tac ~1 i)])
end
handle THM _ => no_tac | EQ_VAR => no_tac);
@@ -224,7 +224,7 @@
and on Free variables if thin=true*)
fun hyp_subst_tac_thin thin ctxt =
REPEAT_DETERM1 o FIRST' [ematch_tac [Data.thin_refl],
- gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac false,
+ gen_hyp_subst_tac ctxt false, vars_gen_hyp_subst_tac ctxt false,
if thin then thin_free_eq_tac else K no_tac];
val hyp_subst_thin = Attrib.setup_config_bool @{binding hypsubst_thin} (K false);
@@ -235,7 +235,7 @@
(*Substitutes for Bound variables only -- this is always safe*)
fun bound_hyp_subst_tac ctxt =
REPEAT_DETERM1 o (gen_hyp_subst_tac ctxt true
- ORELSE' vars_gen_hyp_subst_tac true);
+ ORELSE' vars_gen_hyp_subst_tac ctxt true);
(** Version for Blast_tac. Hyps that are affected by the substitution are
moved to the front. Defect: even trivial changes are noticed, such as
@@ -270,7 +270,7 @@
in imptac (0, rev hyps) end;
-fun blast_hyp_subst_tac trace = SUBGOAL(fn (Bi,i) =>
+fun blast_hyp_subst_tac ctxt trace = SUBGOAL(fn (Bi,i) =>
let val (k, (symopt, _)) = eq_var false false false Bi
val hyps0 = map Data.dest_Trueprop (Logic.strip_assums_hyp Bi)
(*omit selected equality, returning other hyps*)
@@ -282,7 +282,7 @@
(EVERY [REPEAT_DETERM_N k (eresolve_tac [Data.rev_mp] i),
rotate_tac 1 i,
REPEAT_DETERM_N (n-k) (eresolve_tac [Data.rev_mp] i),
- inst_subst_tac symopt (if symopt then ssubst else Data.subst) i,
+ inst_subst_tac ctxt symopt (if symopt then ssubst else Data.subst) i,
all_imp_intr_tac hyps i])
end
handle THM _ => no_tac | EQ_VAR => no_tac);
--- a/src/Provers/splitter.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Provers/splitter.ML Sun Nov 09 14:08:00 2014 +0100
@@ -29,9 +29,9 @@
theory -> typ list -> term -> (thm * (typ * typ * int list) list * int list * typ * term) list
(* first argument is a "cmap", returns a list of "split packs" *)
(* the "real" interface, providing a number of tactics *)
- val split_tac : thm list -> int -> tactic
- val split_inside_tac: thm list -> int -> tactic
- val split_asm_tac : thm list -> int -> tactic
+ val split_tac : Proof.context -> thm list -> int -> tactic
+ val split_inside_tac: Proof.context -> thm list -> int -> tactic
+ val split_asm_tac : Proof.context -> thm list -> int -> tactic
val add_split: thm -> Proof.context -> Proof.context
val del_split: thm -> Proof.context -> Proof.context
val split_add: attribute
@@ -353,17 +353,17 @@
i : number of subgoal the tactic should be applied to
*****************************************************************************)
-fun split_tac [] i = no_tac
- | split_tac splits i =
+fun split_tac _ [] i = no_tac
+ | split_tac ctxt splits i =
let val cmap = cmap_of_split_thms splits
- fun lift_tac Ts t p st = compose_tac (false, inst_lift Ts t p st i, 2) i st
+ fun lift_tac Ts t p st = compose_tac ctxt (false, inst_lift Ts t p st i, 2) i st
fun lift_split_tac state =
let val (Ts, t, splits) = select cmap state i
in case splits of
[] => no_tac state
| (thm, apsns, pos, TB, tt)::_ =>
(case apsns of
- [] => compose_tac (false, inst_split Ts t tt thm TB state i, 0) i state
+ [] => compose_tac ctxt (false, inst_split Ts t tt thm TB state i, 0) i state
| p::_ => EVERY [lift_tac Ts t p,
resolve_tac [reflexive_thm] (i+1),
lift_split_tac] state)
@@ -385,8 +385,8 @@
splits : list of split-theorems to be tried
****************************************************************************)
-fun split_asm_tac [] = K no_tac
- | split_asm_tac splits =
+fun split_asm_tac _ [] = K no_tac
+ | split_asm_tac ctxt splits =
let val cname_list = map (fst o fst o split_thm_info) splits;
fun tac (t,i) =
@@ -408,18 +408,18 @@
THEN REPEAT (dresolve_tac [Data.notnotD] i)) i;
in if n<0 then no_tac else (DETERM (EVERY'
[rotate_tac n, eresolve_tac [Data.contrapos2],
- split_tac splits,
+ split_tac ctxt splits,
rotate_tac ~1, eresolve_tac [Data.contrapos], rotate_tac ~1,
flat_prems_tac] i))
end;
in SUBGOAL tac
end;
-fun gen_split_tac [] = K no_tac
- | gen_split_tac (split::splits) =
+fun gen_split_tac _ [] = K no_tac
+ | gen_split_tac ctxt (split::splits) =
let val (_,asm) = split_thm_info split
- in (if asm then split_asm_tac else split_tac) [split] ORELSE'
- gen_split_tac splits
+ in (if asm then split_asm_tac else split_tac) ctxt [split] ORELSE'
+ gen_split_tac ctxt splits
end;
@@ -437,8 +437,8 @@
fun add_split split ctxt =
let
val (name, asm) = split_thm_info split
- val tac = (if asm then split_asm_tac else split_tac) [split]
- in Simplifier.addloop (ctxt, (split_name name asm, K tac)) end;
+ fun tac ctxt' = (if asm then split_asm_tac else split_tac) ctxt' [split]
+ in Simplifier.addloop (ctxt, (split_name name asm, tac)) end;
fun del_split split ctxt =
let val (name, asm) = split_thm_info split
@@ -468,7 +468,7 @@
val _ =
Theory.setup
(Method.setup @{binding split}
- (Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ths))))
+ (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED_PROP o gen_split_tac ctxt ths)))
"apply case split rule");
end;
--- a/src/Pure/Isar/expression.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Pure/Isar/expression.ML Sun Nov 09 14:08:00 2014 +0100
@@ -683,8 +683,9 @@
val intro = Goal.prove_global defs_thy [] norm_ts statement
(fn {context = ctxt, ...} =>
rewrite_goals_tac ctxt [pred_def] THEN
- compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
- compose_tac (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
+ compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
+ compose_tac defs_ctxt
+ (false, Conjunction.intr_balanced (map (Thm.assume o cert) norm_ts), 0) 1);
val conjuncts =
(Drule.equal_elim_rule2 OF
@@ -695,7 +696,7 @@
|> Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (defs @ conjuncts));
val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
Element.prove_witness axioms_ctxt t
- (rewrite_goals_tac axioms_ctxt defs THEN compose_tac (false, ax, 0) 1));
+ (rewrite_goals_tac axioms_ctxt defs THEN compose_tac axioms_ctxt (false, ax, 0) 1));
in ((statement, intro, axioms), defs_thy) end;
in
--- a/src/Pure/Tools/rule_insts.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Pure/Tools/rule_insts.ML Sun Nov 09 14:08:00 2014 +0100
@@ -270,7 +270,7 @@
(map lifttvar envT', map liftpair cenv)
(Thm.lift_rule cgoal thm)
in
- compose_tac (bires_flag, rule, nprems_of thm) i
+ compose_tac ctxt' (bires_flag, rule, nprems_of thm) i
end) i st;
in tac end;
--- a/src/Pure/tactic.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Pure/tactic.ML Sun Nov 09 14:08:00 2014 +0100
@@ -10,7 +10,7 @@
val rule_by_tactic: Proof.context -> tactic -> thm -> thm
val assume_tac: int -> tactic
val eq_assume_tac: int -> tactic
- val compose_tac: (bool * thm * int) -> int -> tactic
+ val compose_tac: Proof.context -> (bool * thm * int) -> int -> tactic
val make_elim: thm -> thm
val biresolve_tac: (bool * thm) list -> int -> tactic
val resolve_tac: thm list -> int -> tactic
@@ -111,8 +111,8 @@
(*The composition rule/state: no lifting or var renaming.
The arg = (bires_flg, orule, m); see Thm.bicompose for explanation.*)
-fun compose_tac arg i =
- PRIMSEQ (Thm.bicompose NONE {flatten = true, match = false, incremented = false} arg i);
+fun compose_tac ctxt arg i =
+ PRIMSEQ (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false} arg i);
(*Converts a "destruct" rule like P&Q==>P to an "elimination" rule
like [| P&Q; P==>R |] ==> R *)
--- a/src/Tools/atomize_elim.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Tools/atomize_elim.ML Sun Nov 09 14:08:00 2014 +0100
@@ -120,7 +120,7 @@
val rule = instantiate' [SOME (ctyp_of_term cthesis)] [NONE, SOME cthesis]
@{thm meta_spec}
in
- compose_tac (false, rule, 1) i
+ compose_tac ctxt (false, rule, 1) i
end
in
quantify_thesis
--- a/src/Tools/cong_tac.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Tools/cong_tac.ML Sun Nov 09 14:08:00 2014 +0100
@@ -6,13 +6,13 @@
signature CONG_TAC =
sig
- val cong_tac: thm -> int -> tactic
+ val cong_tac: Proof.context -> thm -> int -> tactic
end;
structure Cong_Tac: CONG_TAC =
struct
-fun cong_tac cong = CSUBGOAL (fn (cgoal, i) =>
+fun cong_tac ctxt cong = CSUBGOAL (fn (cgoal, i) =>
let
val cert = Thm.cterm_of (Thm.theory_of_cterm cgoal);
val goal = Thm.term_of cgoal;
@@ -28,7 +28,7 @@
|> map (fn (t, u) => (cert (Term.head_of t), cert (fold_rev Term.abs ps u)));
in
fn st =>
- compose_tac (false, Drule.cterm_instantiate insts cong', 2) i st
+ compose_tac ctxt (false, Drule.cterm_instantiate insts cong', 2) i st
handle THM _ => no_tac st
end
| _ => no_tac)
--- a/src/Tools/induct.ML Sun Nov 09 11:05:20 2014 +0100
+++ b/src/Tools/induct.ML Sun Nov 09 14:08:00 2014 +0100
@@ -684,7 +684,7 @@
in
(case goal_concl n [] goal of
SOME concl =>
- (compose_tac (false, spec_rule (goal_prefix n goal) concl, 1) THEN'
+ (compose_tac ctxt (false, spec_rule (goal_prefix n goal) concl, 1) THEN'
resolve_tac [asm_rl]) i
| NONE => all_tac)
end);