more general types Proof.method / context_tactic;
proper context for Method.insert_tac;
tuned;
--- a/NEWS Sat Dec 12 15:37:42 2015 +0100
+++ b/NEWS Sun Dec 13 21:56:15 2015 +0100
@@ -626,6 +626,12 @@
*** ML ***
+* Isar proof methods are based on a slightly more general type
+context_tactic, which allows to change the proof context dynamically
+(e.g. to update cases) and indicate explicit Seq.Error results. Former
+METHOD_CASES is superseded by CONTEXT_METHOD; further combinators are
+provided in src/Pure/Isar/method.ML for convenience. INCOMPATIBILITY.
+
* Antiquotation @{undefined} or \<^undefined> inlines (raise Match).
* The auxiliary module Pure/display.ML has been eliminated. Its
--- a/src/Doc/Implementation/Isar.thy Sat Dec 12 15:37:42 2015 +0100
+++ b/src/Doc/Implementation/Isar.thy Sun Dec 13 21:56:15 2015 +0100
@@ -165,12 +165,12 @@
section \<open>Proof methods\<close>
-text \<open>A \<open>method\<close> is a function \<open>context \<rightarrow> thm\<^sup>* \<rightarrow> goal
- \<rightarrow> (cases \<times> goal)\<^sup>*\<^sup>*\<close> that operates on the full Isar goal
- configuration with context, goal facts, and tactical goal state and
- enumerates possible follow-up goal states, with the potential
- addition of named extensions of the proof context (\<^emph>\<open>cases\<close>).
- The latter feature is rarely used.
+text \<open>
+ A \<open>method\<close> is a function \<open>thm\<^sup>* \<rightarrow> context * goal \<rightarrow> (context \<times> goal)\<^sup>*\<^sup>*\<close>
+ that operates on the full Isar goal configuration with context, goal facts,
+ and tactical goal state and enumerates possible follow-up goal states. Under
+ normal circumstances, the goal context remains unchanged, but it is also
+ possible to declare named extensions of the proof context (\<^emph>\<open>cases\<close>).
This means a proof method is like a structurally enhanced tactic
(cf.\ \secref{sec:tactics}). The well-formedness conditions for
@@ -287,11 +287,11 @@
text %mlref \<open>
\begin{mldecls}
@{index_ML_type Proof.method} \\
- @{index_ML METHOD_CASES: "(thm list -> cases_tactic) -> Proof.method"} \\
+ @{index_ML CONTEXT_METHOD: "(thm list -> context_tactic) -> Proof.method"} \\
@{index_ML METHOD: "(thm list -> tactic) -> Proof.method"} \\
@{index_ML SIMPLE_METHOD: "tactic -> Proof.method"} \\
@{index_ML SIMPLE_METHOD': "(int -> tactic) -> Proof.method"} \\
- @{index_ML Method.insert_tac: "thm list -> int -> tactic"} \\
+ @{index_ML Method.insert_tac: "Proof.context -> thm list -> int -> tactic"} \\
@{index_ML Method.setup: "binding -> (Proof.context -> Proof.method) context_parser ->
string -> theory -> theory"} \\
\end{mldecls}
@@ -299,9 +299,11 @@
\<^descr> Type @{ML_type Proof.method} represents proof methods as
abstract type.
- \<^descr> @{ML METHOD_CASES}~\<open>(fn facts => cases_tactic)\<close> wraps
- \<open>cases_tactic\<close> depending on goal facts as proof method with
- cases; the goal context is passed via method syntax.
+ \<^descr> @{ML CONTEXT_METHOD}~\<open>(fn facts => context_tactic)\<close> wraps \<open>context_tactic\<close>
+ depending on goal facts as a general proof method that may change the proof
+ context dynamically. A typical operation is @{ML
+ Proof_Context.update_cases}, which is wrapped up as combinator @{index_ML
+ CONTEXT_CASES} for convenience.
\<^descr> @{ML METHOD}~\<open>(fn facts => tactic)\<close> wraps \<open>tactic\<close> depending on goal facts as regular proof method; the goal
context is passed via method syntax.
@@ -315,7 +317,7 @@
addresses a specific subgoal as simple proof method that operates on
subgoal 1. Goal facts are inserted into the subgoal then the \<open>tactic\<close> is applied.
- \<^descr> @{ML Method.insert_tac}~\<open>facts i\<close> inserts \<open>facts\<close> into subgoal \<open>i\<close>. This is convenient to reproduce
+ \<^descr> @{ML Method.insert_tac}~\<open>ctxt facts i\<close> inserts \<open>facts\<close> into subgoal \<open>i\<close>. This is convenient to reproduce
part of the @{ML SIMPLE_METHOD} or @{ML SIMPLE_METHOD'} wrapping
within regular @{ML METHOD}, for example.
@@ -348,7 +350,7 @@
have "A \<and> B"
using a and b
ML_val \<open>@{Isar.goal}\<close>
- apply (tactic \<open>Method.insert_tac facts 1\<close>)
+ apply (tactic \<open>Method.insert_tac @{context} facts 1\<close>)
apply (tactic \<open>(resolve_tac @{context} @{thms conjI} THEN_ALL_NEW assume_tac @{context}) 1\<close>)
done
end
--- a/src/HOL/Eisbach/match_method.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Eisbach/match_method.ML Sun Dec 13 21:56:15 2015 +0100
@@ -294,9 +294,6 @@
(text', ctxt')
end;
-fun DROP_CASES (tac: cases_tactic) : tactic =
- tac #> Seq.map (fn (_, st) => st);
-
fun prep_fact_pat ((x, args), pat) ctxt =
let
val ((params, pat'), ctxt') = Variable.focus NONE pat ctxt;
@@ -675,11 +672,15 @@
in
(case m of
Match_Fact net =>
- Seq.map (fn (text, ctxt') => Method_Closure.method_evaluate text ctxt' using st)
- (make_fact_matches goal_ctxt (Item_Net.retrieve net))
+ make_fact_matches goal_ctxt (Item_Net.retrieve net)
+ |> Seq.map (fn (text, ctxt') =>
+ Method_Closure.method_evaluate text ctxt' using (ctxt', st)
+ |> Seq.filter_results |> Seq.map snd)
| Match_Term net =>
- Seq.map (fn (text, ctxt') => Method_Closure.method_evaluate text ctxt' using st)
- (make_term_matches goal_ctxt (Item_Net.retrieve net))
+ make_term_matches goal_ctxt (Item_Net.retrieve net)
+ |> Seq.map (fn (text, ctxt') =>
+ Method_Closure.method_evaluate text ctxt' using (ctxt', st)
+ |> Seq.filter_results |> Seq.map snd)
| match_kind =>
if Thm.no_prems st then Seq.empty
else
@@ -758,9 +759,9 @@
end;
fun apply_text (text, ctxt') =
- DROP_CASES (Method_Closure.method_evaluate text ctxt' using) focused_goal
- |> Seq.maps (DETERM (do_retrofit ctxt'))
- |> Seq.map (pair ([]: Rule_Cases.cases));
+ Method.NO_CONTEXT_TACTIC ctxt'
+ (Method_Closure.method_evaluate text ctxt' using) focused_goal
+ |> Seq.maps (DETERM (do_retrofit ctxt'));
in Seq.map apply_text texts end)
end;
@@ -770,16 +771,19 @@
(parse_match_kind :--
(fn kind => Scan.lift @{keyword "in"} |-- Parse.enum1' "\<bar>" (parse_named_pats kind)) >>
(fn (matches, bodies) => fn ctxt =>
- METHOD_CASES (fn using => Method.RUNTIME (fn st =>
+ CONTEXT_METHOD (fn using => Method.RUNTIME (fn (goal_ctxt, st) =>
let
- fun exec (pats, fixes, text) goal =
+ fun exec (pats, fixes, text) st' =
let
val ctxt' =
fold Variable.declare_term fixes ctxt
(*FIXME Is this a good idea? We really only care about the maxidx*)
|> fold (fn (_, t) => Variable.declare_term t) pats;
- in real_match using ctxt' fixes matches text pats goal end;
- in Seq.flat (Seq.FIRST (map exec bodies) st) end))))
+ in real_match using ctxt' fixes matches text pats st' end;
+ in
+ Seq.flat (Seq.FIRST (map exec bodies) st)
+ |> Method.CONTEXT goal_ctxt
+ end))))
"structural analysis/matching on goals");
end;
--- a/src/HOL/Filter.thy Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Filter.thy Sun Dec 13 21:56:15 2015 +0100
@@ -233,24 +233,23 @@
frequently_imp_iff
ML \<open>
- fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) =>
- let
- val mp_thms = facts RL @{thms eventually_rev_mp}
- val raw_elim_thm =
- (@{thm allI} RS @{thm always_eventually})
- |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
- |> fold (fn _ => fn thm => @{thm impI} RS thm) facts
- val cases_prop =
- Thm.prop_of
- (Rule_Cases.internalize_params (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal)))
- val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
- in
- CASES cases (resolve_tac ctxt [raw_elim_thm] i)
- end)
+ fun eventually_elim_tac facts =
+ CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
+ let
+ val mp_thms = facts RL @{thms eventually_rev_mp}
+ val raw_elim_thm =
+ (@{thm allI} RS @{thm always_eventually})
+ |> fold (fn thm1 => fn thm2 => thm2 RS thm1) mp_thms
+ |> fold (fn _ => fn thm => @{thm impI} RS thm) facts
+ val cases_prop =
+ Thm.prop_of
+ (Rule_Cases.internalize_params (raw_elim_thm RS Goal.init (Thm.cterm_of ctxt goal)))
+ val cases = Rule_Cases.make_common ctxt cases_prop [(("elim", []), [])]
+ in CONTEXT_CASES cases (resolve_tac ctxt [raw_elim_thm] i) (ctxt, st) end)
\<close>
method_setup eventually_elim = \<open>
- Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt))
+ Scan.succeed (fn _ => CONTEXT_METHOD (fn facts => eventually_elim_tac facts 1))
\<close> "elimination of eventually quantifiers"
subsubsection \<open>Finer-than relation\<close>
--- a/src/HOL/Fun_Def.thy Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Fun_Def.thy Sun Dec 13 21:56:15 2015 +0100
@@ -103,7 +103,7 @@
ML_file "Tools/Function/induction_schema.ML"
method_setup induction_schema = \<open>
- Scan.succeed (EMPTY_CASES oo Induction_Schema.induction_schema_tac)
+ Scan.succeed (Method.CONTEXT_TACTIC oo Induction_Schema.induction_schema_tac)
\<close> "prove an induction principle"
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Sun Dec 13 21:56:15 2015 +0100
@@ -154,7 +154,7 @@
fun can_apply time tac st =
let
val {context = ctxt, facts, goal} = Proof.goal st
- val full_tac = HEADGOAL (Method.insert_tac facts THEN' tac ctxt)
+ val full_tac = HEADGOAL (Method.insert_tac ctxt facts THEN' tac ctxt)
in
(case try (TimeLimit.timeLimit time (Seq.pull o full_tac)) goal of
SOME (SOME _) => true
--- a/src/HOL/Nominal/nominal_induct.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Nominal/nominal_induct.ML Sun Dec 13 21:56:15 2015 +0100
@@ -5,9 +5,9 @@
structure NominalInduct:
sig
- val nominal_induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+ val nominal_induct_tac: bool -> (binding option * (term * bool)) option list list ->
(string * typ) list -> (string * typ) list list -> thm list ->
- thm list -> int -> cases_tactic
+ thm list -> int -> context_tactic
val nominal_induct_method: (Proof.context -> Proof.method) context_parser
end =
struct
@@ -81,7 +81,7 @@
(* nominal_induct_tac *)
-fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts =
+fun nominal_induct_tac simp def_insts avoiding fixings rules facts i (ctxt, st) =
let
val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list;
val atomized_defs = map (map (Conv.fconv_rule (Induct.atomize_cterm ctxt))) defs;
@@ -94,8 +94,8 @@
fun rule_cases ctxt r =
let val r' = if simp then Induct.simplified_rule ctxt r else r
in Rule_Cases.make_nested ctxt (Thm.prop_of r') (Induct.rulified_term ctxt r') end;
- in
- (fn i => fn st =>
+
+ fun context_tac _ _ =
rules
|> inst_mutual_rule ctxt insts avoiding
|> Rule_Cases.consume ctxt (flat defs) facts
@@ -108,7 +108,7 @@
val xs = nth_list fixings (j - 1);
val k = nth concls (j - 1) + more_consumes
in
- Method.insert_tac (more_facts @ adefs) THEN'
+ Method.insert_tac ctxt (more_facts @ adefs) THEN'
(if simp then
Induct.rotate_tac k (length adefs) THEN'
Induct.arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
@@ -120,13 +120,13 @@
Induct.guess_instance ctxt
(finish_rule (Induct.internalize ctxt more_consumes rule)) i st'
|> Seq.maps (fn rule' =>
- CASES (rule_cases ctxt rule' cases)
+ CONTEXT_CASES (rule_cases ctxt rule' cases)
(resolve_tac ctxt [rename_params_rule false [] rule'] i THEN
- PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
- THEN_ALL_NEW_CASES
+ PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) (ctxt, st'))));
+ in
+ (context_tac CONTEXT_THEN_ALL_NEW
((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac ctxt)
- else K all_tac)
- THEN_ALL_NEW Induct.rulify_tac ctxt)
+ else K all_tac) THEN_ALL_NEW Induct.rulify_tac ctxt)) i (ctxt, st)
end;
@@ -169,8 +169,8 @@
Scan.lift (Args.mode Induct.no_simpN) --
(Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
avoiding -- fixing -- rule_spec) >>
- (fn (no_simp, (((x, y), z), w)) => fn ctxt => fn facts =>
- HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts));
+ (fn (no_simp, (((x, y), z), w)) => fn _ => fn facts =>
+ (nominal_induct_tac (not no_simp) x y z w facts 1));
end;
--- a/src/HOL/Nominal/nominal_primrec.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Sun Dec 13 21:56:15 2015 +0100
@@ -372,11 +372,10 @@
|> snd
end)
[goals] |>
- Proof.apply (Method.Basic (fn ctxt => fn _ =>
- EMPTY_CASES
+ Proof.refine_singleton (Method.Basic (fn ctxt => fn _ =>
+ Method.CONTEXT_TACTIC
(rewrite_goals_tac ctxt defs_thms THEN
- compose_tac ctxt (false, rule, length rule_prems) 1))) |>
- Seq.hd
+ compose_tac ctxt (false, rule, length rule_prems) 1)))
end;
in
--- a/src/HOL/Partial_Function.thy Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Partial_Function.thy Sun Dec 13 21:56:15 2015 +0100
@@ -443,7 +443,7 @@
declaration \<open>Partial_Function.init "tailrec" @{term tailrec.fixp_fun}
@{term tailrec.mono_body} @{thm tailrec.fixp_rule_uc} @{thm tailrec.fixp_induct_uc}
- (SOME @{thm fixp_induct_tailrec[where c=undefined]})\<close>
+ (SOME @{thm fixp_induct_tailrec[where c = undefined]})\<close>
declaration \<open>Partial_Function.init "option" @{term option.fixp_fun}
@{term option.mono_body} @{thm option.fixp_rule_uc} @{thm option.fixp_induct_uc}
--- a/src/HOL/Tools/BNF/bnf_def.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML Sun Dec 13 21:56:15 2015 +0100
@@ -1706,8 +1706,7 @@
(lthy
|> Proof.theorem NONE (uncurry (register_bnf plugins key) oo after_qed mk_wit_thms)
(map (single o rpair []) goals @ nontriv_wit_goals)
- |> Proof.refine (Method.primitive_text (K I))
- |> Seq.hd)
+ |> Proof.refine_singleton (Method.primitive_text (K I)))
end) o prepare_def Do_Inline (user_policy Note_Some) false I Syntax.read_typ Syntax.read_term
NONE Binding.empty Binding.empty [] raw_csts;
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Sun Dec 13 21:56:15 2015 +0100
@@ -319,7 +319,7 @@
unfold_thms_tac ctxt [bd_card_order RS @{thm card_order_csum_cone_cexp_def}] THEN
unfold_thms_tac ctxt @{thms cprod_def Field_card_of} THEN
EVERY' [rtac ctxt (Drule.rotate_prems 1 ctrans), rtac ctxt surj_imp_ordLeq_inst, rtac ctxt subsetI,
- Method.insert_tac inserts, REPEAT_DETERM o dtac ctxt meta_spec,
+ Method.insert_tac ctxt inserts, REPEAT_DETERM o dtac ctxt meta_spec,
REPEAT_DETERM o eresolve_tac ctxt [exE, Tactic.make_elim conjunct1], etac ctxt CollectE,
if live = 1 then K all_tac
else REPEAT_DETERM_N (live - 2) o (etac ctxt conjE THEN' rotate_tac ~1) THEN' etac ctxt conjE,
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sun Dec 13 21:56:15 2015 +0100
@@ -1579,8 +1579,7 @@
val primcorecursive_cmd = (fn (goalss, after_qed, lthy) =>
lthy
|> Proof.theorem NONE after_qed goalss
- |> Proof.refine (Method.primitive_text (K I))
- |> Seq.hd) ooo primcorec_ursive_cmd false;
+ |> Proof.refine_singleton (Method.primitive_text (K I))) ooo primcorec_ursive_cmd false;
val primcorec_cmd = (fn (goalss, after_qed, lthy) =>
lthy |> after_qed (map (fn [] => [] | _ => use_primcorecursive ()) goalss)) ooo
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Sun Dec 13 21:56:15 2015 +0100
@@ -54,7 +54,7 @@
assume_tac ctxt;
fun mk_primcorec_nchotomy_tac ctxt exhaust_discs =
- HEADGOAL (Method.insert_tac exhaust_discs THEN' clean_blast_tac ctxt);
+ HEADGOAL (Method.insert_tac ctxt exhaust_discs THEN' clean_blast_tac ctxt);
fun mk_primcorec_exhaust_tac ctxt frees n nchotomy =
let val ks = 1 upto n in
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Sun Dec 13 21:56:15 2015 +0100
@@ -1082,7 +1082,7 @@
fun mk_rel_coinduct_tac ctxt CIHs in_rels in_Jrels helper_indss helper_coind1s helper_coind2s =
let val n = length in_rels;
in
- Method.insert_tac CIHs 1 THEN
+ Method.insert_tac ctxt CIHs 1 THEN
unfold_thms_tac ctxt (@{thm choice_iff} :: @{thm ex_simps(6)[symmetric]} :: in_rels) THEN
REPEAT_DETERM (etac ctxt exE 1) THEN
CONJ_WRAP' (fn (in_Jrel, (helper_inds, (helper_coind1, helper_coind2))) =>
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Sun Dec 13 21:56:15 2015 +0100
@@ -356,7 +356,7 @@
let
val n = length card_of_min_algs;
in
- EVERY' [Method.insert_tac (map (fn thm => thm RS @{thm ex_bij_betw}) card_of_min_algs),
+ EVERY' [Method.insert_tac ctxt (map (fn thm => thm RS @{thm ex_bij_betw}) card_of_min_algs),
REPEAT_DETERM o dtac ctxt meta_spec, REPEAT_DETERM o etac ctxt exE, rtac ctxt rev_mp,
rtac ctxt copy, REPEAT_DETERM_N n o assume_tac ctxt,
rtac ctxt impI, REPEAT_DETERM o eresolve_tac ctxt [exE, conjE], REPEAT_DETERM_N n o rtac ctxt exI,
--- a/src/HOL/Tools/BNF/bnf_lift.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_lift.ML Sun Dec 13 21:56:15 2015 +0100
@@ -345,10 +345,9 @@
(fn (goals, after_qed, definitions, lthy) =>
lthy
|> Proof.theorem NONE after_qed (map (single o rpair []) goals)
- |> Proof.refine (Method.Basic (fn ctxt => SIMPLE_METHOD (unfold_thms_tac ctxt definitions)))
- |> Seq.hd
- |> Proof.refine (Method.primitive_text (K I))
- |> Seq.hd) oo
+ |> Proof.refine_singleton
+ (Method.Basic (fn ctxt => SIMPLE_METHOD (unfold_thms_tac ctxt definitions)))
+ |> Proof.refine_singleton (Method.primitive_text (K I))) oo
prepare_common prepare_name prepare_sort prepare_term prepare_thm o apfst (apfst (apsnd SOME));
fun prepare_solve prepare_name prepare_typ prepare_sort prepare_thm tacs =
--- a/src/HOL/Tools/Function/function.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/Function/function.ML Sun Dec 13 21:56:15 2015 +0100
@@ -171,7 +171,7 @@
in
lthy'
|> Proof.theorem NONE (snd oo afterqed) [[(Logic.unprotect (Thm.concl_of goal_state), [])]]
- |> Proof.refine (Method.primitive_text (K (K goal_state))) |> Seq.hd
+ |> Proof.refine_singleton (Method.primitive_text (K (K goal_state)))
end
val function =
--- a/src/HOL/Tools/Function/function_elims.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/Function/function_elims.ML Sun Dec 13 21:56:15 2015 +0100
@@ -121,7 +121,7 @@
fun prep_subgoal_tac i =
REPEAT (eresolve_tac ctxt @{thms Pair_inject} i)
- THEN Method.insert_tac (case asms_thms of thm :: thms => (thm RS sym) :: thms) i
+ THEN Method.insert_tac ctxt (case asms_thms of thm :: thms => (thm RS sym) :: thms) i
THEN propagate_tac ctxt i
THEN TRY ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN assume_tac ctxt i)
THEN bool_subst_tac ctxt i;
--- a/src/HOL/Tools/Function/induction_schema.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML Sun Dec 13 21:56:15 2015 +0100
@@ -345,7 +345,7 @@
fun mk_ind_tac comp_tac pres_tac term_tac ctxt facts =
(* FIXME proper use of facts!? *)
- (ALLGOALS (Method.insert_tac facts)) THEN HEADGOAL (SUBGOAL (fn (t, i) =>
+ (ALLGOALS (Method.insert_tac ctxt facts)) THEN HEADGOAL (SUBGOAL (fn (t, i) =>
let
val (ctxt', _, cases, concl) = dest_hhf ctxt t
val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl
--- a/src/HOL/Tools/Function/partial_function.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML Sun Dec 13 21:56:15 2015 +0100
@@ -62,8 +62,6 @@
(*** Automated monotonicity proofs ***)
-fun strip_cases ctac = ctac #> Seq.map snd;
-
(*rewrite conclusion with k-th assumtion*)
fun rewrite_with_asm_tac ctxt k =
Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
@@ -95,7 +93,7 @@
| SOME (arg, conv) =>
let open Conv in
if Term.is_open arg then no_tac
- else ((DETERM o strip_cases o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
+ else ((DETERM o Method.NO_CONTEXT_TACTIC ctxt o Induct.cases_tac false [[SOME arg]] NONE [])
THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0)
THEN_ALL_NEW eresolve_tac ctxt @{thms thin_rl}
THEN_ALL_NEW (CONVERSION
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sun Dec 13 21:56:15 2015 +0100
@@ -407,7 +407,7 @@
by (simp add: eq_onp_same_args rel_fun_eq_onp_rel)}
fun lift_sel_tac exhaust_rule dt_rules wits ctxt i =
- (Method.insert_tac wits THEN'
+ (Method.insert_tac ctxt wits THEN'
eq_onp_to_top_tac ctxt THEN' (* normalize *)
rtac ctxt unfold_lift_sel_rsp THEN'
case_tac exhaust_rule ctxt THEN_ALL_NEW (
@@ -559,7 +559,7 @@
val TFrees = Term.add_tfreesT qty []
fun non_empty_typedef_tac non_empty_pred ctxt i =
- (Method.insert_tac [non_empty_pred] THEN'
+ (Method.insert_tac ctxt [non_empty_pred] THEN'
SELECT_GOAL (Local_Defs.unfold_tac ctxt [mem_Collect_eq]) THEN' assume_tac ctxt) i
val uTname = unique_Tname (rty, qty)
val Tdef_set = HOLogic.mk_Collect ("x", rty, pred $ Free("x", rty));
--- a/src/HOL/Tools/Metis/metis_tactic.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Sun Dec 13 21:56:15 2015 +0100
@@ -272,7 +272,7 @@
fun metis_method ((override_type_encs, lam_trans), ths) ctxt facts =
let val (schem_facts, nonschem_facts) = List.partition has_tvar facts in
- HEADGOAL (Method.insert_tac nonschem_facts THEN'
+ HEADGOAL (Method.insert_tac ctxt nonschem_facts THEN'
CHANGED_PROP o metis_tac (these override_type_encs)
(the_default default_metis_lam_trans lam_trans) ctxt (schem_facts @ ths))
end
--- a/src/HOL/Tools/Qelim/cooper.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Sun Dec 13 21:56:15 2015 +0100
@@ -870,7 +870,7 @@
val simpset_ctxt =
put_simpset (fst (get ctxt)) ctxt delsimps del_ths addsimps add_ths
in
- Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}))
+ Method.insert_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems arith}))
THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
THEN_ALL_NEW simp_tac simpset_ctxt
--- a/src/HOL/Tools/SMT/z3_replay_methods.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML Sun Dec 13 21:56:15 2015 +0100
@@ -133,7 +133,7 @@
fun prove ctxt t tac = by_tac ctxt [] [] [] t (K o tac)
fun prop_tac ctxt prems =
- Method.insert_tac prems
+ Method.insert_tac ctxt prems
THEN' SUBGOAL (fn (prop, i) =>
if Term.size_of_term prop > 100 then SAT.satx_tac ctxt i
else (Classical.fast_tac ctxt ORELSE' Clasimp.force_tac ctxt) i)
@@ -324,7 +324,7 @@
by fast+}
fun cong_full ctxt thms t = prove ctxt t (fn ctxt' =>
- Method.insert_tac thms
+ Method.insert_tac ctxt thms
THEN' (Classical.fast_tac ctxt'
ORELSE' dresolve_tac ctxt cong_dest_rules
THEN' Classical.fast_tac ctxt'))
@@ -615,7 +615,7 @@
(* theory lemmas *)
fun arith_th_lemma_tac ctxt prems =
- Method.insert_tac prems
+ Method.insert_tac ctxt prems
THEN' SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms z3div_def z3mod_def})
THEN' Arith_Data.arith_tac ctxt
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Sun Dec 13 21:56:15 2015 +0100
@@ -114,7 +114,7 @@
end
fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
- Method.insert_tac local_facts THEN'
+ Method.insert_tac ctxt local_facts THEN'
(case meth of
Metis_Method (type_enc_opt, lam_trans_opt) =>
let
@@ -131,7 +131,7 @@
| Simp_Size_Method =>
Simplifier.asm_full_simp_tac (ctxt addsimps (@{thm size_ne_size_imp_ne} :: global_facts))
| _ =>
- Method.insert_tac global_facts THEN'
+ Method.insert_tac ctxt global_facts THEN'
(case meth of
SATx_Method => SAT.satx_tac ctxt
| Blast_Method => blast_tac ctxt
--- a/src/HOL/Tools/arith_data.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/arith_data.ML Sun Dec 13 21:56:15 2015 +0100
@@ -48,8 +48,8 @@
(Scan.succeed (fn ctxt =>
METHOD (fn facts =>
HEADGOAL
- (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
- THEN' arith_tac ctxt))))
+ (Method.insert_tac ctxt (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
+ THEN' arith_tac ctxt))))
"various arithmetic decision procedures");
--- a/src/HOL/Tools/coinduction.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/coinduction.ML Sun Dec 13 21:56:15 2015 +0100
@@ -8,7 +8,7 @@
signature COINDUCTION =
sig
- val coinduction_tac: Proof.context -> term list -> thm option -> thm list -> cases_tactic
+ val coinduction_tac: term list -> thm option -> thm list -> int -> context_tactic
end;
structure Coinduction : COINDUCTION =
@@ -37,85 +37,85 @@
(THEN_ALL_NEW_SKIP skip tac (REPEAT_DETERM_N n o eresolve0_tac [thin_rl])) i st
end;
-fun coinduction_tac ctxt raw_vars opt_raw_thm prems = HEADGOAL (SUBGOAL_CASES (fn (goal, _) =>
- let
- val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
- fun find_coinduct t =
- Induct.find_coinductP ctxt t @
- (try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default [])
- val raw_thm =
- (case opt_raw_thm of
- SOME raw_thm => raw_thm
- | NONE => goal |> Logic.strip_assums_concl |> find_coinduct |> hd);
- val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1
- val cases = Rule_Cases.get raw_thm |> fst
- in
- HEADGOAL (
- Object_Logic.rulify_tac ctxt THEN'
- Method.insert_tac prems THEN'
- Object_Logic.atomize_prems_tac ctxt THEN'
- DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} =>
- let
- val vars = raw_vars @ map (Thm.term_of o snd) params;
- val names_ctxt = ctxt
- |> fold Variable.declare_names vars
- |> fold Variable.declare_thm (raw_thm :: prems);
- val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
- val (instT, inst) = Thm.match (thm_concl, concl);
- val rhoTs = map (fn (v, T) => (TVar v, Thm.typ_of T)) instT;
- val rhots = map (fn (v, t) => (Var v, Thm.term_of t)) inst;
- val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
- |> map (subst_atomic_types rhoTs);
- val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
- val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
- |>> (fn names => Variable.variant_fixes names names_ctxt) ;
- val eqs =
- @{map 3} (fn name => fn T => fn (_, rhs) =>
- HOLogic.mk_eq (Free (name, T), rhs))
- names Ts raw_eqs;
- val phi = eqs @ map (HOLogic.dest_Trueprop o Thm.prop_of) prems
- |> try (Library.foldr1 HOLogic.mk_conj)
- |> the_default @{term True}
- |> Ctr_Sugar_Util.list_exists_free vars
- |> Term.map_abs_vars (Variable.revert_fixed ctxt)
- |> fold_rev Term.absfree (names ~~ Ts)
- |> Thm.cterm_of ctxt;
- val thm = infer_instantiate' ctxt [SOME phi] raw_thm;
- val e = length eqs;
- val p = length prems;
- in
- HEADGOAL (EVERY' [resolve_tac ctxt [thm],
- EVERY' (map (fn var =>
- resolve_tac ctxt
- [infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt var)] exI]) vars),
- if p = 0 then Ctr_Sugar_Util.CONJ_WRAP' (K (resolve_tac ctxt [refl])) eqs
- else
- REPEAT_DETERM_N e o (resolve_tac ctxt [conjI] THEN' resolve_tac ctxt [refl]) THEN'
- Ctr_Sugar_Util.CONJ_WRAP' (resolve_tac ctxt o single) prems,
- K (ALLGOALS_SKIP skip
- (REPEAT_DETERM_N (length vars) o (eresolve_tac ctxt [exE] THEN' rotate_tac ~1) THEN'
- DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
- (case prems of
- [] => all_tac
- | inv :: case_prems =>
- let
- val (init, last) = funpow_yield (p + e - 1) (HOLogic.conj_elim ctxt) inv;
- val inv_thms = init @ [last];
- val eqs = take e inv_thms;
- fun is_local_var t =
- member (fn (t, (_, t')) => t aconv (Thm.term_of t')) params t;
- val (eqs, assms') =
- filter_in_out (is_local_var o lhs_of_eq o Thm.prop_of) eqs;
- val assms = assms' @ drop e inv_thms
- in
- HEADGOAL (Method.insert_tac (assms @ case_prems)) THEN
- Ctr_Sugar_General_Tactics.unfold_thms_tac ctxt eqs
- end)) ctxt)))])
- end) ctxt) THEN'
- K (prune_params_tac ctxt))
- #> Seq.maps (fn st =>
- CASES (Rule_Cases.make_common ctxt (Thm.prop_of st) cases) all_tac st)
- end));
+fun coinduction_tac raw_vars opt_raw_thm prems =
+ CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
+ let
+ val lhs_of_eq = HOLogic.dest_Trueprop #> HOLogic.dest_eq #> fst;
+ fun find_coinduct t =
+ Induct.find_coinductP ctxt t @
+ (try (Induct.find_coinductT ctxt o fastype_of o lhs_of_eq) t |> the_default []);
+ val raw_thm =
+ (case opt_raw_thm of
+ SOME raw_thm => raw_thm
+ | NONE => goal |> Logic.strip_assums_concl |> find_coinduct |> hd);
+ val skip = Integer.max 1 (Rule_Cases.get_consumes raw_thm) - 1;
+ val cases = Rule_Cases.get raw_thm |> fst;
+ in
+ ((Object_Logic.rulify_tac ctxt THEN'
+ Method.insert_tac ctxt prems THEN'
+ Object_Logic.atomize_prems_tac ctxt THEN'
+ DELETE_PREMS_AFTER skip (Subgoal.FOCUS (fn {concl, context = ctxt, params, prems, ...} =>
+ let
+ val vars = raw_vars @ map (Thm.term_of o snd) params;
+ val names_ctxt = ctxt
+ |> fold Variable.declare_names vars
+ |> fold Variable.declare_thm (raw_thm :: prems);
+ val thm_concl = Thm.cprop_of raw_thm |> strip_imp_concl;
+ val (instT, inst) = Thm.match (thm_concl, concl);
+ val rhoTs = map (fn (v, T) => (TVar v, Thm.typ_of T)) instT;
+ val rhots = map (fn (v, t) => (Var v, Thm.term_of t)) inst;
+ val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
+ |> map (subst_atomic_types rhoTs);
+ val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
+ val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
+ |>> (fn names => Variable.variant_fixes names names_ctxt) ;
+ val eqs =
+ @{map 3} (fn name => fn T => fn (_, rhs) =>
+ HOLogic.mk_eq (Free (name, T), rhs))
+ names Ts raw_eqs;
+ val phi = eqs @ map (HOLogic.dest_Trueprop o Thm.prop_of) prems
+ |> try (Library.foldr1 HOLogic.mk_conj)
+ |> the_default @{term True}
+ |> Ctr_Sugar_Util.list_exists_free vars
+ |> Term.map_abs_vars (Variable.revert_fixed ctxt)
+ |> fold_rev Term.absfree (names ~~ Ts)
+ |> Thm.cterm_of ctxt;
+ val thm = infer_instantiate' ctxt [SOME phi] raw_thm;
+ val e = length eqs;
+ val p = length prems;
+ in
+ HEADGOAL (EVERY' [resolve_tac ctxt [thm],
+ EVERY' (map (fn var =>
+ resolve_tac ctxt
+ [infer_instantiate' ctxt [NONE, SOME (Thm.cterm_of ctxt var)] exI]) vars),
+ if p = 0 then Ctr_Sugar_Util.CONJ_WRAP' (K (resolve_tac ctxt [refl])) eqs
+ else
+ REPEAT_DETERM_N e o (resolve_tac ctxt [conjI] THEN' resolve_tac ctxt [refl]) THEN'
+ Ctr_Sugar_Util.CONJ_WRAP' (resolve_tac ctxt o single) prems,
+ K (ALLGOALS_SKIP skip
+ (REPEAT_DETERM_N (length vars) o (eresolve_tac ctxt [exE] THEN' rotate_tac ~1) THEN'
+ DELETE_PREMS_AFTER 0 (Subgoal.FOCUS (fn {prems, params, context = ctxt, ...} =>
+ (case prems of
+ [] => all_tac
+ | inv :: case_prems =>
+ let
+ val (init, last) = funpow_yield (p + e - 1) (HOLogic.conj_elim ctxt) inv;
+ val inv_thms = init @ [last];
+ val eqs = take e inv_thms;
+ fun is_local_var t =
+ member (fn (t, (_, t')) => t aconv (Thm.term_of t')) params t;
+ val (eqs, assms') =
+ filter_in_out (is_local_var o lhs_of_eq o Thm.prop_of) eqs;
+ val assms = assms' @ drop e inv_thms
+ in
+ HEADGOAL (Method.insert_tac ctxt (assms @ case_prems)) THEN
+ Ctr_Sugar_General_Tactics.unfold_thms_tac ctxt eqs
+ end)) ctxt)))])
+ end) ctxt) THEN'
+ K (prune_params_tac ctxt)) i) st
+ |> Seq.maps (fn st' =>
+ CONTEXT_CASES (Rule_Cases.make_common ctxt (Thm.prop_of st') cases) all_tac (ctxt, st'))
+ end);
local
@@ -152,8 +152,8 @@
Theory.setup
(Method.setup @{binding coinduction}
(arbitrary -- Scan.option coinduct_rule >>
- (fn (arbitrary, opt_rule) => fn ctxt => fn facts =>
- Seq.DETERM (coinduction_tac ctxt arbitrary opt_rule facts)))
+ (fn (arbitrary, opt_rule) => fn _ => fn facts =>
+ Seq.DETERM (coinduction_tac arbitrary opt_rule facts 1)))
"coinduction on types or predicates/sets");
end;
--- a/src/HOL/Tools/functor.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/functor.ML Sun Dec 13 21:56:15 2015 +0100
@@ -128,10 +128,11 @@
(mapper21 $ (mapper32 $ x), mapper31 $ x);
val comp_prop = fold_rev Logic.all (map Free (args21 @ args32)) eq1;
val compositionality_prop = fold_rev Logic.all (map Free (args21 @ args32) @ [x]) eq2;
- fun prove_compositionality ctxt comp_thm = Goal.prove_sorry ctxt [] [] compositionality_prop
- (K (ALLGOALS (Method.insert_tac [@{thm fun_cong} OF [comp_thm]]
- THEN' Simplifier.asm_lr_simp_tac (put_simpset compositionality_ss ctxt)
- THEN_ALL_NEW (Goal.assume_rule_tac ctxt))));
+ fun prove_compositionality ctxt comp_thm =
+ Goal.prove_sorry ctxt [] [] compositionality_prop
+ (K (ALLGOALS (Method.insert_tac ctxt [@{thm fun_cong} OF [comp_thm]]
+ THEN' Simplifier.asm_lr_simp_tac (put_simpset compositionality_ss ctxt)
+ THEN_ALL_NEW (Goal.assume_rule_tac ctxt))));
in (comp_prop, prove_compositionality) end;
val identity_ss =
@@ -152,9 +153,10 @@
val rhs = HOLogic.id_const T;
val (id_prop, identity_prop) =
apply2 (HOLogic.mk_Trueprop o HOLogic.mk_eq o rpair rhs) (lhs1, lhs2);
- fun prove_identity ctxt id_thm = Goal.prove_sorry ctxt [] [] identity_prop
- (K (ALLGOALS (Method.insert_tac [id_thm] THEN'
- Simplifier.asm_lr_simp_tac (put_simpset identity_ss ctxt))));
+ fun prove_identity ctxt id_thm =
+ Goal.prove_sorry ctxt [] [] identity_prop
+ (K (ALLGOALS (Method.insert_tac ctxt [id_thm] THEN'
+ Simplifier.asm_lr_simp_tac (put_simpset identity_ss ctxt))));
in (id_prop, prove_identity) end;
--- a/src/HOL/Tools/groebner.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/groebner.ML Sun Dec 13 21:56:15 2015 +0100
@@ -970,7 +970,7 @@
val cfs = (map swap o #multi_ideal thy evs ps)
(map Thm.dest_arg1 (conjuncts bod))
val ws = map (exitac ctxt o AList.lookup op aconvc cfs) evs
- in EVERY (rev ws) THEN Method.insert_tac prems 1
+ in EVERY (rev ws) THEN Method.insert_tac ctxt prems 1
THEN ring_tac add_ths del_ths ctxt 1
end
in
--- a/src/HOL/Tools/lin_arith.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/lin_arith.ML Sun Dec 13 21:56:15 2015 +0100
@@ -895,7 +895,9 @@
Method.setup @{binding linarith}
(Scan.succeed (fn ctxt =>
METHOD (fn facts =>
- HEADGOAL (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
+ HEADGOAL
+ (Method.insert_tac ctxt
+ (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
THEN' tac ctxt)))) "linear arithmetic" #>
Arith_Data.add_tactic "linear arithmetic" tac;
--- a/src/HOL/Tools/try0.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/try0.ML Sun Dec 13 21:56:15 2015 +0100
@@ -70,7 +70,8 @@
((name ^ attrs |> attrs <> "" ? enclose "(" ")") ^
(if all_goals andalso Thm.nprems_of (#goal (Proof.goal st)) > 1 then "[1]" else ""))
I (#goal o Proof.goal)
- (apply_named_method_on_first_goal (Proof.context_of st) (name ^ attrs)) st
+ (apply_named_method_on_first_goal (Proof.context_of st) (name ^ attrs)
+ #> Seq.filter_results) st
end
else
NONE;
--- a/src/Provers/Arith/fast_lin_arith.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML Sun Dec 13 21:56:15 2015 +0100
@@ -695,7 +695,7 @@
end);
fun prems_lin_arith_tac ctxt =
- Method.insert_tac (Simplifier.prems_of ctxt) THEN'
+ Method.insert_tac ctxt (Simplifier.prems_of ctxt) THEN'
simpset_lin_arith_tac ctxt;
fun lin_arith_tac ctxt =
--- a/src/Pure/Isar/element.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/Pure/Isar/element.ML Sun Dec 13 21:56:15 2015 +0100
@@ -272,7 +272,7 @@
local
val refine_witness =
- Proof.refine (Method.Basic (fn ctxt => EMPTY_CASES o
+ Proof.refine_singleton (Method.Basic (fn ctxt => Method.CONTEXT_TACTIC o
K (ALLGOALS (CONJUNCTS (ALLGOALS (CONJUNCTS (TRYALL (resolve_tac ctxt [Drule.protectI]))))))));
fun gen_witness_proof proof after_qed wit_propss eq_props =
@@ -283,7 +283,7 @@
fun after_qed' thmss =
let val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss);
in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
- in proof after_qed' propss #> refine_witness #> Seq.hd end;
+ in proof after_qed' propss #> refine_witness end;
fun proof_local cmd goal_ctxt int after_qed propp =
let
--- a/src/Pure/Isar/isar_syn.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sun Dec 13 21:56:15 2015 +0100
@@ -699,16 +699,16 @@
val _ =
Outer_Syntax.command @{command_keyword apply} "initial goal refinement step (unstructured)"
- (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_results m))));
+ (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply m))));
val _ =
Outer_Syntax.command @{command_keyword apply_end} "terminal goal refinement step (unstructured)"
- (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end_results m))));
+ (Method.parse >> (fn m => (Method.report m; Toplevel.proofs (Proof.apply_end m))));
val _ =
Outer_Syntax.command @{command_keyword proof} "backward proof step"
(Scan.option Method.parse >> (fn m =>
- (Option.map Method.report m; Toplevel.proofs (Proof.proof_results m))));
+ (Option.map Method.report m; Toplevel.proofs (Proof.proof m))));
(* subgoal focus *)
--- a/src/Pure/Isar/method.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/Pure/Isar/method.ML Sun Dec 13 21:56:15 2015 +0100
@@ -4,34 +4,35 @@
Isar proof methods.
*)
-infix 1 THEN_ALL_NEW_CASES;
+infix 1 CONTEXT_THEN_ALL_NEW;
signature BASIC_METHOD =
sig
- type cases_state = Rule_Cases.cases * thm
- type cases_tactic = thm -> cases_state Seq.seq
- val CASES: Rule_Cases.cases -> tactic -> cases_tactic
- val EMPTY_CASES: tactic -> cases_tactic
- val SUBGOAL_CASES: (term * int -> cases_tactic) -> int -> cases_tactic
- val THEN_ALL_NEW_CASES: (int -> cases_tactic) * (int -> tactic) -> int -> cases_tactic
+ type context_state = Proof.context * thm
+ type context_tactic = context_state -> context_state Seq.result Seq.seq
+ val CONTEXT_CASES: Rule_Cases.cases -> tactic -> context_tactic
+ val CONTEXT_SUBGOAL: (term * int -> context_tactic) -> int -> context_tactic
+ val CONTEXT_THEN_ALL_NEW: (int -> context_tactic) * (int -> tactic) -> int -> context_tactic
end;
signature METHOD =
sig
include BASIC_METHOD
- type method = thm list -> cases_tactic
- val METHOD_CASES: (thm list -> cases_tactic) -> method
+ type method = thm list -> context_tactic
+ val CONTEXT: Proof.context -> thm Seq.seq -> context_state Seq.result Seq.seq
+ val CONTEXT_TACTIC: tactic -> context_tactic
+ val NO_CONTEXT_TACTIC: Proof.context -> context_tactic -> tactic
+ val CONTEXT_METHOD: (thm list -> context_tactic) -> method
val METHOD: (thm list -> tactic) -> method
val fail: method
val succeed: method
- val insert_tac: thm list -> int -> tactic
+ val insert_tac: Proof.context -> thm list -> int -> tactic
val insert: thm list -> method
- val insert_facts: method
val SIMPLE_METHOD: tactic -> method
val SIMPLE_METHOD': (int -> tactic) -> method
val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
- val goal_cases_tac: Proof.context -> string list -> cases_tactic
- val cheating: Proof.context -> bool -> method
+ val goal_cases_tac: string list -> context_tactic
+ val cheating: bool -> method
val intro: Proof.context -> thm list -> method
val elim: Proof.context -> thm list -> method
val unfold: thm list -> Proof.context -> method
@@ -83,9 +84,9 @@
val closure: bool Config.T
val method_cmd: Proof.context -> Token.src -> Proof.context -> method
val detect_closure_state: thm -> bool
- val STATIC: (unit -> unit) -> cases_tactic
- val RUNTIME: cases_tactic -> cases_tactic
- val sleep: Time.time -> cases_tactic
+ val STATIC: (unit -> unit) -> context_tactic
+ val RUNTIME: context_tactic -> context_tactic
+ val sleep: Time.time -> context_tactic
val evaluate: text -> Proof.context -> method
type modifier = {init: Proof.context -> Proof.context, attribute: attribute, pos: Position.T}
val modifier: attribute -> Position.T -> modifier
@@ -105,33 +106,44 @@
(** proof methods **)
-(* tactics with cases *)
+(* tactics with proof context / cases *)
+
+type context_state = Proof.context * thm;
+type context_tactic = context_state -> context_state Seq.result Seq.seq;
-type cases_state = Rule_Cases.cases * thm;
-type cases_tactic = thm -> cases_state Seq.seq;
+fun CONTEXT ctxt : thm Seq.seq -> context_state Seq.result Seq.seq =
+ Seq.map (Seq.Result o pair ctxt);
-fun CASES cases tac st = Seq.map (pair cases) (tac st);
-fun EMPTY_CASES tac = CASES [] tac;
+fun CONTEXT_TACTIC tac : context_tactic =
+ fn (ctxt, st) => CONTEXT ctxt (tac st);
+
+fun NO_CONTEXT_TACTIC ctxt (tac: context_tactic) st =
+ tac (ctxt, st) |> Seq.filter_results |> Seq.map snd;
-fun SUBGOAL_CASES tac i st =
- (case try Logic.nth_prem (i, Thm.prop_of st) of
- SOME goal => tac (goal, i) st
- | NONE => Seq.empty);
+fun CONTEXT_CASES cases tac : context_tactic =
+ fn (ctxt, st) => CONTEXT (Proof_Context.update_cases cases ctxt) (tac st);
-fun (tac1 THEN_ALL_NEW_CASES tac2) i st =
- st |> tac1 i |> Seq.maps (fn (cases, st') =>
- CASES cases (Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)) st');
+fun CONTEXT_SUBGOAL tac i : context_tactic =
+ fn (ctxt, st) =>
+ (case try Logic.nth_prem (i, Thm.prop_of st) of
+ SOME goal => tac (goal, i) (ctxt, st)
+ | NONE => Seq.empty);
+
+fun (tac1 CONTEXT_THEN_ALL_NEW tac2) i : context_tactic =
+ fn (ctxt, st) =>
+ (ctxt, st) |> tac1 i |> Seq.maps_results (fn (ctxt', st') =>
+ CONTEXT ctxt' ((Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)) st'));
(* type method *)
-type method = thm list -> cases_tactic;
+type method = thm list -> context_tactic;
-fun METHOD_CASES tac : method =
- fn facts => Seq.THEN (ALLGOALS Goal.conjunction_tac, tac facts);
+fun CONTEXT_METHOD tac : method =
+ fn facts => CONTEXT_TACTIC (ALLGOALS Goal.conjunction_tac) #> Seq.maps_results (tac facts);
fun METHOD tac : method =
- fn facts => EMPTY_CASES (ALLGOALS Goal.conjunction_tac THEN tac facts);
+ fn facts => CONTEXT_TACTIC (ALLGOALS Goal.conjunction_tac THEN tac facts);
val fail = METHOD (K no_tac);
val succeed = METHOD (K all_tac);
@@ -139,42 +151,42 @@
(* insert facts *)
-local
+fun insert_tac _ [] _ = all_tac
+ | insert_tac ctxt facts i =
+ EVERY (map (fn r => resolve_tac ctxt [Drule.forall_intr_vars r COMP_INCR revcut_rl] i) facts);
-fun cut_rule_tac rule =
- resolve0_tac [Drule.forall_intr_vars rule COMP_INCR revcut_rl];
+fun insert thms =
+ CONTEXT_METHOD (fn _ => fn (ctxt, st) => st |> ALLGOALS (insert_tac ctxt thms) |> CONTEXT ctxt);
-in
-fun insert_tac [] _ = all_tac
- | insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts);
-
-val insert_facts = METHOD (ALLGOALS o insert_tac);
-fun insert thms = METHOD (fn _ => ALLGOALS (insert_tac thms));
+fun SIMPLE_METHOD tac =
+ CONTEXT_METHOD (fn facts => fn (ctxt, st) =>
+ st |> (ALLGOALS (insert_tac ctxt facts) THEN tac) |> CONTEXT ctxt);
-fun SIMPLE_METHOD tac = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN tac);
-fun SIMPLE_METHOD'' quant tac = METHOD (fn facts => quant (insert_tac facts THEN' tac));
+fun SIMPLE_METHOD'' quant tac =
+ CONTEXT_METHOD (fn facts => fn (ctxt, st) =>
+ st |> quant (insert_tac ctxt facts THEN' tac) |> CONTEXT ctxt);
+
val SIMPLE_METHOD' = SIMPLE_METHOD'' HEADGOAL;
-end;
-
(* goals as cases *)
-fun goal_cases_tac ctxt case_names st =
- let
- val cases =
- (if null case_names then map string_of_int (1 upto Thm.nprems_of st) else case_names)
- |> map (rpair [] o rpair [])
- |> Rule_Cases.make_common ctxt (Thm.prop_of (Rule_Cases.internalize_params st));
- in Seq.single (cases, st) end;
+fun goal_cases_tac case_names : context_tactic =
+ fn (ctxt, st) =>
+ let
+ val cases =
+ (if null case_names then map string_of_int (1 upto Thm.nprems_of st) else case_names)
+ |> map (rpair [] o rpair [])
+ |> Rule_Cases.make_common ctxt (Thm.prop_of (Rule_Cases.internalize_params st));
+ in CONTEXT_CASES cases all_tac (ctxt, st) end;
(* cheating *)
-fun cheating ctxt int = METHOD (fn _ => fn st =>
+fun cheating int = CONTEXT_METHOD (fn _ => fn (ctxt, st) =>
if int orelse Config.get ctxt quick_and_dirty then
- ALLGOALS (Skip_Proof.cheat_tac ctxt) st
+ CONTEXT ctxt (ALLGOALS (Skip_Proof.cheat_tac ctxt) st)
else error "Cheating requires quick_and_dirty mode!");
@@ -195,7 +207,7 @@
fun atomize false ctxt =
SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac ctxt)
| atomize true ctxt =
- EMPTY_CASES o K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt));
+ CONTEXT_TACTIC o K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac ctxt));
(* this -- resolve facts directly *)
@@ -293,7 +305,7 @@
(* intros_tac -- pervasive search spanned by intro rules *)
fun gen_intros_tac goals ctxt intros facts =
- goals (insert_tac facts THEN'
+ goals (insert_tac ctxt facts THEN'
REPEAT_ALL_NEW (resolve_tac ctxt intros))
THEN Tactic.distinct_subgoals_tac;
@@ -369,7 +381,7 @@
val standard_text = Source (Token.make_src ("standard", Position.none) []);
val this_text = Basic this;
val done_text = Basic (K (SIMPLE_METHOD all_tac));
-fun sorry_text int = Basic (fn ctxt => cheating ctxt int);
+fun sorry_text int = Basic (fn _ => cheating int);
fun finish_text (NONE, immed) = Basic (finish immed)
| finish_text (SOME txt, immed) =
@@ -455,7 +467,7 @@
let
val src' = map Token.init_assignable src;
val ctxt' = Context_Position.not_really ctxt;
- val _ = Seq.pull (method ctxt' src' ctxt' [] (Goal.protect 0 Drule.dummy_thm));
+ val _ = Seq.pull (method ctxt' src' ctxt' [] (ctxt', Goal.protect 0 Drule.dummy_thm));
in map Token.closure src' end;
val closure = Config.bool (Config.declare ("Method.closure", @{here}) (K (Config.Bool true)));
@@ -473,39 +485,47 @@
NONE => false
| SOME t => Term.is_dummy_pattern t);
-fun STATIC test st =
- if detect_closure_state st then (test (); Seq.single ([], st)) else Seq.empty;
+fun STATIC test : context_tactic =
+ fn (ctxt, st) =>
+ if detect_closure_state st then (test (); Seq.single (Seq.Result (ctxt, st))) else Seq.empty;
-fun RUNTIME (tac: cases_tactic) st =
- if detect_closure_state st then Seq.empty else tac st;
+fun RUNTIME (tac: context_tactic) (ctxt, st) =
+ if detect_closure_state st then Seq.empty else tac (ctxt, st);
-fun sleep t = RUNTIME (fn st => (OS.Process.sleep t; Seq.single ([], st)));
+fun sleep t = RUNTIME (fn ctxt_st => (OS.Process.sleep t; Seq.single (Seq.Result ctxt_st)));
(* evaluate method text *)
local
-fun APPEND_CASES (tac: cases_tactic) ((cases, st): cases_state) =
- tac st |> Seq.map (fn (cases', st') => (cases @ cases', st'));
-
-fun BYPASS_CASES (tac: tactic) ((cases, st): cases_state) =
- tac st |> Seq.map (pair cases);
-
val op THEN = Seq.THEN;
-val preparation = BYPASS_CASES (ALLGOALS Goal.conjunction_tac);
+fun BYPASS_CONTEXT (tac: tactic) =
+ fn result =>
+ (case result of
+ Seq.Error _ => Seq.single result
+ | Seq.Result (ctxt, st) => tac st |> CONTEXT ctxt);
+
+val preparation = BYPASS_CONTEXT (ALLGOALS Goal.conjunction_tac);
fun RESTRICT_GOAL i n method =
- BYPASS_CASES (PRIMITIVE (Goal.restrict i n)) THEN
+ BYPASS_CONTEXT (PRIMITIVE (Goal.restrict i n)) THEN
method THEN
- BYPASS_CASES (PRIMITIVE (Goal.unrestrict i));
+ BYPASS_CONTEXT (PRIMITIVE (Goal.unrestrict i));
fun SELECT_GOAL method i = RESTRICT_GOAL i 1 method;
-fun (method1 THEN_ALL_NEW method2) i (st: cases_state) =
- st |> (method1 i THEN (fn st' =>
- Seq.INTERVAL method2 i (i + Thm.nprems_of (snd st') - Thm.nprems_of (snd st)) st'));
+fun (method1 THEN_ALL_NEW method2) i (result : context_state Seq.result) =
+ (case result of
+ Seq.Error _ => Seq.single result
+ | Seq.Result (_, st) =>
+ result |> method1 i
+ |> Seq.maps (fn result' =>
+ (case result' of
+ Seq.Error _ => Seq.single result'
+ | Seq.Result (_, st') =>
+ result' |> Seq.INTERVAL method2 i (i + Thm.nprems_of st' - Thm.nprems_of st))))
fun COMBINATOR1 comb [meth] = comb meth
| COMBINATOR1 _ _ = raise Fail "Method combinator requires exactly one argument";
@@ -514,7 +534,7 @@
| combinator Then_All_New =
(fn [] => Seq.single
| methods =>
- preparation THEN foldl1 (op THEN_ALL_NEW) (map SELECT_GOAL methods) 1)
+ preparation THEN (foldl1 (op THEN_ALL_NEW) (map SELECT_GOAL methods) 1))
| combinator Orelse = Seq.FIRST
| combinator Try = COMBINATOR1 Seq.TRY
| combinator Repeat1 = COMBINATOR1 Seq.REPEAT1
@@ -525,15 +545,16 @@
fun evaluate text ctxt =
let
- fun eval (Basic meth) = APPEND_CASES o meth ctxt
- | eval (Source src) = APPEND_CASES o method_cmd ctxt src ctxt
+ fun eval0 m facts = Seq.single #> Seq.maps_results (m facts);
+ fun eval (Basic m) = eval0 (m ctxt)
+ | eval (Source src) = eval0 (method_cmd ctxt src ctxt)
| eval (Combinator (_, c, txts)) =
let
val comb = combinator c;
val meths = map eval txts;
in fn facts => comb (map (fn meth => meth facts) meths) end;
val meth = eval text;
- in fn facts => fn st => meth facts ([], st) end;
+ in fn facts => fn ctxt_st => meth facts (Seq.Result ctxt_st) end;
end;
@@ -711,21 +732,19 @@
setup @{binding succeed} (Scan.succeed (K succeed)) "succeed" #>
setup @{binding sleep} (Scan.lift Parse.real >> (fn s => fn _ => fn _ => sleep (seconds s)))
"succeed after delay (in seconds)" #>
- setup @{binding "-"} (Scan.succeed (K insert_facts))
+ setup @{binding "-"} (Scan.succeed (K (SIMPLE_METHOD all_tac)))
"insert current facts, nothing else" #>
- setup @{binding goal_cases} (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn ctxt =>
- METHOD_CASES (fn _ => fn st =>
- let
- val _ =
- (case drop (Thm.nprems_of st) names of
- [] => ()
- | bad =>
- if detect_closure_state st then ()
- else
- (* FIXME Seq.Error *)
- error ("Excessive case names: " ^ commas_quote (map Token.content_of bad) ^
- Position.here (Position.set_range (Token.range_of bad))));
- in goal_cases_tac ctxt (map Token.content_of names) st end)))
+ setup @{binding goal_cases} (Scan.lift (Scan.repeat Args.name_token) >> (fn names => fn _ =>
+ CONTEXT_METHOD (fn _ => fn (ctxt, st) =>
+ (case drop (Thm.nprems_of st) names of
+ [] => NONE
+ | bad =>
+ if detect_closure_state st then NONE
+ else
+ SOME (fn () => ("Excessive case names: " ^ commas_quote (map Token.content_of bad) ^
+ Position.here (Position.set_range (Token.range_of bad)))))
+ |> (fn SOME msg => Seq.single (Seq.Error msg)
+ | NONE => goal_cases_tac (map Token.content_of names) (ctxt, st)))))
"bind cases for goals" #>
setup @{binding insert} (Attrib.thms >> (K o insert))
"insert theorems, ignoring facts" #>
@@ -754,7 +773,7 @@
"rotate assumptions of goal" #>
setup @{binding tactic} (parse_tactic >> (K o METHOD))
"ML tactic as proof method" #>
- setup @{binding raw_tactic} (parse_tactic >> (fn tac => fn _ => EMPTY_CASES o tac))
+ setup @{binding raw_tactic} (parse_tactic >> (fn tac => fn _ => CONTEXT_TACTIC o tac))
"ML tactic as raw proof method");
@@ -767,7 +786,7 @@
structure Basic_Method: BASIC_METHOD = Method;
open Basic_Method;
-val METHOD_CASES = Method.METHOD_CASES;
+val CONTEXT_METHOD = Method.CONTEXT_METHOD;
val METHOD = Method.METHOD;
val SIMPLE_METHOD = Method.SIMPLE_METHOD;
val SIMPLE_METHOD' = Method.SIMPLE_METHOD';
--- a/src/Pure/Isar/obtain.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/Pure/Isar/obtain.ML Sun Dec 13 21:56:15 2015 +0100
@@ -266,7 +266,7 @@
val ((thesis_var, thesis), thesis_ctxt) = obtain_thesis ctxt;
val st = Goal.init (Thm.cterm_of ctxt thesis);
val rule =
- (case SINGLE (Method.insert_tac facts 1 THEN tac thesis_ctxt) st of
+ (case SINGLE (Method.insert_tac thesis_ctxt facts 1 THEN tac thesis_ctxt) st of
NONE => raise THM ("Obtain.result: tactic failed", 0, facts)
| SOME th =>
check_result thesis_ctxt thesis (Raw_Simplifier.norm_hhf thesis_ctxt (Goal.conclude th)));
@@ -413,9 +413,8 @@
(SOME before_qed) after_qed
[] [] [(Thm.empty_binding, [(Logic.mk_term goal, []), (goal, [])])]
|> snd
- |> Proof.refine (Method.primitive_text (fn _ => fn _ =>
- Goal.init (Thm.cterm_of ctxt thesis)))
- |> Seq.hd
+ |> Proof.refine_singleton
+ (Method.primitive_text (fn _ => fn _ => Goal.init (Thm.cterm_of ctxt thesis)))
end;
in
--- a/src/Pure/Isar/proof.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/Pure/Isar/proof.ML Sun Dec 13 21:56:15 2015 +0100
@@ -35,8 +35,9 @@
val has_bottom_goal: state -> bool
val using_facts: thm list -> state -> state
val pretty_state: state -> Pretty.T list
- val refine: Method.text -> state -> state Seq.seq
- val refine_end: Method.text -> state -> state Seq.seq
+ val refine: Method.text -> state -> state Seq.result Seq.seq
+ val refine_end: Method.text -> state -> state Seq.result Seq.seq
+ val refine_singleton: Method.text -> state -> state
val refine_insert: thm list -> state -> state
val refine_primitive: (Proof.context -> thm -> thm) -> state -> state
val raw_goal: state -> {context: context, facts: thm list, goal: thm}
@@ -90,14 +91,11 @@
val end_block: state -> state
val begin_notepad: context -> state
val end_notepad: state -> context
- val proof: Method.text option -> state -> state Seq.seq
- val proof_results: Method.text_range option -> state -> state Seq.result Seq.seq
+ val proof: Method.text_range option -> state -> state Seq.result Seq.seq
val defer: int -> state -> state
val prefer: int -> state -> state
- val apply: Method.text -> state -> state Seq.seq
- val apply_end: Method.text -> state -> state Seq.seq
- val apply_results: Method.text_range -> state -> state Seq.result Seq.seq
- val apply_end_results: Method.text_range -> state -> state Seq.result Seq.seq
+ val apply: Method.text_range -> state -> state Seq.result Seq.seq
+ val apply_end: Method.text_range -> state -> state Seq.result Seq.seq
val local_qed: Method.text_range option * bool -> state -> state
val theorem: Method.text option -> (thm list list -> context -> context) ->
(term * term list) list list -> context -> state
@@ -424,14 +422,13 @@
fun apply_method text ctxt state =
find_goal state |> (fn (goal_ctxt, {statement, using, goal, before_qed, after_qed}) =>
- Method.evaluate text ctxt using goal
- |> Seq.map (fn (meth_cases, goal') =>
+ Method.evaluate text ctxt using (goal_ctxt, goal)
+ |> Seq.map_result (fn (goal_ctxt', goal') =>
let
- val goal_ctxt' = goal_ctxt
- |> Proof_Context.update_cases_legacy (no_goal_cases goal @ goal_cases ctxt goal')
- |> Proof_Context.update_cases meth_cases;
+ val goal_ctxt'' = goal_ctxt'
+ |> Proof_Context.update_cases_legacy (no_goal_cases goal @ goal_cases ctxt goal');
val state' = state
- |> map_goal (K (goal_ctxt', statement, using, goal', before_qed, after_qed));
+ |> map_goal (K (goal_ctxt'', statement, using, goal', before_qed, after_qed));
in state' end));
in
@@ -439,11 +436,13 @@
fun refine text state = apply_method text (context_of state) state;
fun refine_end text state = apply_method text (#1 (find_goal state)) state;
-fun refine_insert ths =
- Seq.hd o refine (Method.Basic (K (Method.insert ths)));
+fun refine_singleton text = refine text #> Seq.the_result "";
-fun refine_primitive r = (* FIXME Seq.Error!? *)
- Seq.hd o refine (Method.Basic (fn ctxt => fn _ => EMPTY_CASES (PRIMITIVE (r ctxt))));
+fun refine_insert ths =
+ refine_singleton (Method.Basic (K (Method.insert ths)));
+
+fun refine_primitive r =
+ refine_singleton (Method.Basic (fn ctxt => fn _ => Method.CONTEXT_TACTIC (PRIMITIVE (r ctxt))));
end;
@@ -924,17 +923,15 @@
(* sub-proofs *)
fun proof opt_text =
- assert_backward
- #> refine (the_default Method.standard_text opt_text)
- #> Seq.map
- (using_facts []
- #> enter_forward
- #> open_block
- #> reset_goal);
-
-fun proof_results arg =
- Seq.APPEND (proof (Method.text arg) #> Seq.make_results,
- method_error "initial" (Method.position arg));
+ Seq.APPEND
+ (assert_backward
+ #> refine (the_default Method.standard_text (Method.text opt_text))
+ #> Seq.map_result
+ (using_facts []
+ #> enter_forward
+ #> open_block
+ #> reset_goal),
+ method_error "initial" (Method.position opt_text));
fun end_proof bot (prev_pos, (opt_text, immed)) =
let
@@ -951,8 +948,8 @@
|> assert_current_goal true
|> using_facts []
|> `before_qed |-> (refine o the_default Method.succeed_text)
- |> Seq.maps (refine finish_text)
- |> Seq.make_results, method_error "terminal" terminal_pos)
+ |> Seq.maps_results (refine finish_text),
+ method_error "terminal" terminal_pos)
#> Seq.maps_results (Seq.single o finished_goal finished_pos)
end;
@@ -966,21 +963,18 @@
fun defer i =
assert_no_chain #>
- refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL defer_tac i))) #> Seq.hd;
+ refine_singleton (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL defer_tac i)));
fun prefer i =
assert_no_chain #>
- refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL prefer_tac i))) #> Seq.hd;
-
-fun apply text = assert_backward #> refine text #> Seq.map (using_facts []);
-
-fun apply_end text = assert_forward #> refine_end text;
+ refine_singleton (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL prefer_tac i)));
-fun apply_results (text, (pos, _)) =
- Seq.APPEND (apply text #> Seq.make_results, method_error "" pos);
+fun apply (text, (pos, _)) =
+ Seq.APPEND (assert_backward #> refine text #> Seq.map_result (using_facts []),
+ method_error "" pos);
-fun apply_end_results (text, (pos, _)) =
- Seq.APPEND (apply_end text #> Seq.make_results, method_error "" pos);
+fun apply_end (text, (pos, _)) =
+ Seq.APPEND (assert_forward #> refine_end text, method_error "" pos);
@@ -1002,10 +996,9 @@
in map (Logic.mk_term o Var) vars end;
fun refine_terms n =
- refine (Method.Basic (fn ctxt => EMPTY_CASES o
+ refine_singleton (Method.Basic (fn ctxt => Method.CONTEXT_TACTIC o
K (HEADGOAL (PRECISE_CONJUNCTS n
- (HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac ctxt [Drule.termI]))))))))
- #> Seq.hd;
+ (HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac ctxt [Drule.termI]))))))));
in
@@ -1042,7 +1035,7 @@
|> chaining ? (`the_facts #-> using_facts)
|> reset_facts
|> not (null vars) ? refine_terms (length goal_propss)
- |> null goal_props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
+ |> null goal_props ? refine_singleton (Method.Basic Method.assumption)
end;
fun generic_qed state =
@@ -1151,7 +1144,7 @@
local
fun terminal_proof qeds initial terminal =
- proof_results (SOME initial) #> Seq.maps_results (qeds (#2 (#2 initial), terminal))
+ proof (SOME initial) #> Seq.maps_results (qeds (#2 (#2 initial), terminal))
#> Seq.the_result "";
in
--- a/src/Pure/Tools/find_theorems.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/Pure/Tools/find_theorems.ML Sun Dec 13 21:56:15 2015 +0100
@@ -429,7 +429,7 @@
val assms =
Proof_Context.get_fact ctxt (Facts.named "local.assms")
handle ERROR _ => [];
- val add_prems = Seq.hd o TRY (Method.insert_tac assms 1);
+ val add_prems = Seq.hd o TRY (Method.insert_tac ctxt assms 1);
val opt_goal' = Option.map add_prems opt_goal;
in
filter ctxt (all_facts_of ctxt)
--- a/src/Pure/Tools/rule_insts.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/Pure/Tools/rule_insts.ML Sun Dec 13 21:56:15 2015 +0100
@@ -306,10 +306,10 @@
Args.goal_spec -- Scan.optional (Scan.lift (named_insts --| Args.$$$ "in")) ([], []) --
Attrib.thms >> (fn ((quant, (insts, fixes)), thms) => fn ctxt => METHOD (fn facts =>
if null insts andalso null fixes
- then quant (Method.insert_tac facts THEN' tac ctxt thms)
+ then quant (Method.insert_tac ctxt facts THEN' tac ctxt thms)
else
(case thms of
- [thm] => quant (Method.insert_tac facts THEN' inst_tac ctxt insts fixes thm)
+ [thm] => quant (Method.insert_tac ctxt facts THEN' inst_tac ctxt insts fixes thm)
| _ => error "Cannot have instantiations with multiple rules")));
--- a/src/Pure/simplifier.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/Pure/simplifier.ML Sun Dec 13 21:56:15 2015 +0100
@@ -370,12 +370,12 @@
fun method_setup more_mods =
Method.setup @{binding simp}
(simp_method more_mods (fn ctxt => fn tac => fn facts =>
- HEADGOAL (Method.insert_tac facts THEN'
+ HEADGOAL (Method.insert_tac ctxt facts THEN'
(CHANGED_PROP oo tac) ctxt)))
"simplification" #>
Method.setup @{binding simp_all}
(simp_method more_mods (fn ctxt => fn tac => fn facts =>
- ALLGOALS (Method.insert_tac facts) THEN
+ ALLGOALS (Method.insert_tac ctxt facts) THEN
(CHANGED_PROP o PARALLEL_ALLGOALS o tac) ctxt))
"simplification (all goals)";
--- a/src/Pure/tactical.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/Pure/tactical.ML Sun Dec 13 21:56:15 2015 +0100
@@ -47,7 +47,7 @@
val ALLGOALS: (int -> tactic) -> tactic
val SOMEGOAL: (int -> tactic) -> tactic
val FIRSTGOAL: (int -> tactic) -> tactic
- val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
+ val HEADGOAL: (int -> tactic) -> tactic
val REPEAT_SOME: (int -> tactic) -> tactic
val REPEAT_DETERM_SOME: (int -> tactic) -> tactic
val REPEAT_FIRST: (int -> tactic) -> tactic
@@ -358,7 +358,7 @@
following usual convention for subgoal-based tactics.*)
fun (tac1 THEN_ALL_NEW tac2) i st =
st |> (tac1 i THEN (fn st' =>
- Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st) st'));
+ st' |> Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)));
(*Repeatedly dig into any emerging subgoals.*)
fun REPEAT_ALL_NEW tac =
--- a/src/Tools/induct.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/Tools/induct.ML Sun Dec 13 21:56:15 2015 +0100
@@ -71,23 +71,21 @@
val rotate_tac: int -> int -> int -> tactic
val internalize: Proof.context -> int -> thm -> thm
val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
- val cases_tac: Proof.context -> bool -> term option list list -> thm option ->
- thm list -> int -> cases_tactic
+ val cases_tac: bool -> term option list list -> thm option -> thm list -> int -> context_tactic
val get_inductT: Proof.context -> term option list list -> thm list list
val gen_induct_tac: ((Rule_Cases.info * int) * thm -> (Rule_Cases.info * int) * thm) ->
- Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+ bool -> (binding option * (term * bool)) option list list ->
(string * typ) list list -> term option list -> thm list option ->
- thm list -> int -> cases_tactic
- val induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+ thm list -> int -> context_tactic
+ val induct_tac: bool -> (binding option * (term * bool)) option list list ->
(string * typ) list list -> term option list -> thm list option ->
- thm list -> int -> cases_tactic
- val coinduct_tac: Proof.context -> term option list -> term option list -> thm option ->
- thm list -> int -> cases_tactic
+ thm list -> int -> context_tactic
+ val coinduct_tac: term option list -> term option list -> thm option ->
+ thm list -> int -> context_tactic
val gen_induct_setup: binding ->
- (Proof.context -> bool -> (binding option * (term * bool)) option list list ->
+ (bool -> (binding option * (term * bool)) option list list ->
(string * typ) list list -> term option list -> thm list option ->
- thm list -> int -> cases_tactic) ->
- local_theory -> local_theory
+ thm list -> int -> context_tactic) -> local_theory -> local_theory
end;
functor Induct(Induct_Args: INDUCT_ARGS): INDUCT =
@@ -479,33 +477,33 @@
in
-fun cases_tac ctxt simp insts opt_rule facts =
- let
- fun inst_rule r =
- (if null insts then r
- else
- (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
- |> maps (prep_inst ctxt align_left I)
- |> infer_instantiate ctxt) r)
- |> simp ? mark_constraints (Rule_Cases.get_constraints r) ctxt
- |> pair (Rule_Cases.get r);
-
- val (opt_rule', facts') =
- (case (opt_rule, facts) of
- (NONE, th :: ths) =>
- if is_some (Object_Logic.elim_concl ctxt th) then (SOME th, ths)
- else (opt_rule, facts)
- | _ => (opt_rule, facts));
-
- val ruleq =
- (case opt_rule' of
- SOME r => Seq.single (inst_rule r)
- | NONE =>
- (get_casesP ctxt facts' @ get_casesT ctxt insts @ [Induct_Args.cases_default])
- |> tap (trace_rules ctxt casesN)
- |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
- in
- fn i => fn st =>
+fun cases_tac simp insts opt_rule facts i : context_tactic =
+ fn (ctxt, st) =>
+ let
+ fun inst_rule r =
+ (if null insts then r
+ else
+ (align_left "Rule has fewer premises than arguments given" (Thm.prems_of r) insts
+ |> maps (prep_inst ctxt align_left I)
+ |> infer_instantiate ctxt) r)
+ |> simp ? mark_constraints (Rule_Cases.get_constraints r) ctxt
+ |> pair (Rule_Cases.get r);
+
+ val (opt_rule', facts') =
+ (case (opt_rule, facts) of
+ (NONE, th :: ths) =>
+ if is_some (Object_Logic.elim_concl ctxt th) then (SOME th, ths)
+ else (opt_rule, facts)
+ | _ => (opt_rule, facts));
+
+ val ruleq =
+ (case opt_rule' of
+ SOME r => Seq.single (inst_rule r)
+ | NONE =>
+ (get_casesP ctxt facts' @ get_casesT ctxt insts @ [Induct_Args.cases_default])
+ |> tap (trace_rules ctxt casesN)
+ |> Seq.of_list |> Seq.maps (Seq.try inst_rule));
+ in
ruleq
|> Seq.maps (Rule_Cases.consume ctxt [] facts')
|> Seq.maps (fn ((cases, (_, facts'')), rule) =>
@@ -513,12 +511,12 @@
val rule' = rule
|> simp ? (simplified_rule' ctxt #> unmark_constraints ctxt);
in
- CASES (Rule_Cases.make_common ctxt
+ CONTEXT_CASES (Rule_Cases.make_common ctxt
(Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
- ((Method.insert_tac facts'' THEN' resolve_tac ctxt [rule'] THEN_ALL_NEW
- (if simp then TRY o trivial_tac ctxt else K all_tac)) i) st
+ ((Method.insert_tac ctxt facts'' THEN' resolve_tac ctxt [rule'] THEN_ALL_NEW
+ (if simp then TRY o trivial_tac ctxt else K all_tac)) i) (ctxt, st)
end)
- end;
+ end;
end;
@@ -741,8 +739,8 @@
fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
| get_inductP _ _ = [];
-fun gen_induct_tac mod_cases ctxt simp def_insts arbitrary taking opt_rule facts =
- SUBGOAL_CASES (fn (_, i) =>
+fun gen_induct_tac mod_cases simp def_insts arbitrary taking opt_rule facts =
+ CONTEXT_SUBGOAL (fn (_, i) => fn (ctxt, st) =>
let
val ((insts, defs), defs_ctxt) = fold_map add_defs def_insts ctxt |>> split_list;
val atomized_defs = map (map (Conv.fconv_rule (atomize_cterm defs_ctxt))) defs;
@@ -773,8 +771,8 @@
val nonames = map (fn ((cn, _), cls) => ((cn, []), cls));
val cases' = if Thm.eq_thm_prop (rule', rule'') then cases else nonames cases;
in Rule_Cases.make_nested ctxt (Thm.prop_of rule'') (rulified_term ctxt rule'') cases' end;
- in
- fn st =>
+
+ fun context_tac _ _ =
ruleq
|> Seq.maps (Rule_Cases.consume defs_ctxt (flat defs) facts)
|> Seq.maps (fn (((cases, concls), (more_consumes, more_facts)), rule) =>
@@ -786,7 +784,7 @@
val xs = nth_list arbitrary (j - 1);
val k = nth concls (j - 1) + more_consumes;
in
- Method.insert_tac (more_facts @ adefs) THEN'
+ Method.insert_tac defs_ctxt (more_facts @ adefs) THEN'
(if simp then
rotate_tac k (length adefs) THEN'
arbitrary_tac defs_ctxt k (List.partition (member op = frees) xs |> op @)
@@ -794,17 +792,19 @@
arbitrary_tac defs_ctxt k xs)
end)
THEN' inner_atomize_tac defs_ctxt) j))
- THEN' atomize_tac defs_ctxt) i st |> Seq.maps (fn st' =>
+ THEN' atomize_tac defs_ctxt) i st
+ |> Seq.maps (fn st' =>
guess_instance ctxt (internalize ctxt more_consumes rule) i st'
|> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
|> Seq.maps (fn rule' =>
- CASES (rule_cases ctxt rule' cases)
+ CONTEXT_CASES (rule_cases ctxt rule' cases)
(resolve_tac ctxt [rule'] i THEN
- PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st')))
- end)
- THEN_ALL_NEW_CASES
+ PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) (ctxt, st'))));
+ in
+ (context_tac CONTEXT_THEN_ALL_NEW
((if simp then simplify_tac ctxt THEN' (TRY o trivial_tac ctxt) else K all_tac)
- THEN_ALL_NEW rulify_tac ctxt);
+ THEN_ALL_NEW rulify_tac ctxt)) i (ctxt, st)
+ end)
val induct_tac = gen_induct_tac I;
@@ -831,15 +831,15 @@
in
-fun coinduct_tac ctxt inst taking opt_rule facts = SUBGOAL_CASES (fn (goal, i) =>
- let
- fun inst_rule r =
- if null inst then `Rule_Cases.get r
- else
- infer_instantiate ctxt (prep_inst ctxt align_right I (main_prop_of r, inst)) r
- |> pair (Rule_Cases.get r);
- in
- fn st =>
+fun coinduct_tac inst taking opt_rule facts =
+ CONTEXT_SUBGOAL (fn (goal, i) => fn (ctxt, st) =>
+ let
+ fun inst_rule r =
+ if null inst then `Rule_Cases.get r
+ else
+ infer_instantiate ctxt (prep_inst ctxt align_right I (main_prop_of r, inst)) r
+ |> pair (Rule_Cases.get r);
+ in
(case opt_rule of
SOME r => Seq.single (inst_rule r)
| NONE =>
@@ -851,10 +851,10 @@
guess_instance ctxt rule i st
|> Seq.map (rule_instance ctxt (burrow_options (Variable.polymorphic ctxt) taking))
|> Seq.maps (fn rule' =>
- CASES (Rule_Cases.make_common ctxt
+ CONTEXT_CASES (Rule_Cases.make_common ctxt
(Thm.prop_of (Rule_Cases.internalize_params rule')) cases)
- (Method.insert_tac more_facts i THEN resolve_tac ctxt [rule'] i) st))
- end);
+ (Method.insert_tac ctxt more_facts i THEN resolve_tac ctxt [rule'] i) (ctxt, st)))
+ end);
end;
@@ -919,8 +919,8 @@
(Scan.lift (Args.mode no_simpN) --
(Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
(arbitrary -- taking -- Scan.option induct_rule)) >>
- (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn ctxt => fn facts =>
- Seq.DETERM (HEADGOAL (tac ctxt (not no_simp) insts arbitrary taking opt_rule facts))))
+ (fn (no_simp, (insts, ((arbitrary, taking), opt_rule))) => fn _ => fn facts =>
+ Seq.DETERM (tac (not no_simp) insts arbitrary taking opt_rule facts 1)))
"induction on types or predicates/sets";
val _ =
@@ -928,15 +928,15 @@
(Method.local_setup @{binding cases}
(Scan.lift (Args.mode no_simpN) --
(Parse.and_list' (Scan.repeat (unless_more_args inst)) -- Scan.option cases_rule) >>
- (fn (no_simp, (insts, opt_rule)) => fn ctxt =>
- METHOD_CASES (fn facts => Seq.DETERM (HEADGOAL
- (cases_tac ctxt (not no_simp) insts opt_rule facts)))))
+ (fn (no_simp, (insts, opt_rule)) => fn _ =>
+ CONTEXT_METHOD (fn facts =>
+ Seq.DETERM (cases_tac (not no_simp) insts opt_rule facts 1))))
"case analysis on types or predicates/sets" #>
gen_induct_setup @{binding induct} induct_tac #>
Method.local_setup @{binding coinduct}
(Scan.repeat (unless_more_args inst) -- taking -- Scan.option coinduct_rule >>
- (fn ((insts, taking), opt_rule) => fn ctxt => fn facts =>
- Seq.DETERM (HEADGOAL (coinduct_tac ctxt insts taking opt_rule facts))))
+ (fn ((insts, taking), opt_rule) => fn _ => fn facts =>
+ Seq.DETERM (coinduct_tac insts taking opt_rule facts 1)))
"coinduction on types or predicates/sets");
end;
--- a/src/Tools/induction.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/Tools/induction.ML Sun Dec 13 21:56:15 2015 +0100
@@ -7,10 +7,9 @@
signature INDUCTION =
sig
- val induction_tac: Proof.context -> bool ->
- (binding option * (term * bool)) option list list ->
+ val induction_tac: bool -> (binding option * (term * bool)) option list list ->
(string * typ) list list -> term option list -> thm list option ->
- thm list -> int -> cases_tactic
+ thm list -> int -> context_tactic
end
structure Induction: INDUCTION =