ML \<open>fun method_evaluate text ctxt facts =
NO_CONTEXT_TACTIC ctxt
(Method.evaluate_runtime text ctxt facts)\<close>
method_setup timeit = \<open>Method.text_closure >> (fn m => fn ctxt => fn facts => let fun timed_tac st seq = Seq.make (fn () => Option.map (apsnd (timed_tac st))
(timeit (fn () => (Seq.pull seq))));
fun tac st' =
timed_tac st' (method_evaluate m ctxt facts st');
in SIMPLE_METHOD tac [] end) \<close> \<open>print timing information from running the parameter method\<close>
section \<open>Simple Combinators\<close>
method_setup defer_tac = \<open>Scan.succeed (fn _ => SIMPLE_METHOD (defer_tac 1))\<close> \<open>make first subgoal the last subgoal. Like "defer" but as proof method\<close>
method_setup prefer_last = \<open>Scan.succeed (fn _ => SIMPLE_METHOD (PRIMITIVE (Thm.permute_prems 0 ~1)))\<close> \<open>make last subgoal the first subgoal.\<close>
method_setup all = \<open>Method.text_closure >> (fn m => fn ctxt => fn facts => let fun tac i st' =
Goal.restrict i 1 st'
|> method_evaluate m ctxt facts
|> Seq.map (Goal.unrestrict i)
in SIMPLE_METHOD (ALLGOALS tac) facts end) \<close> \<open>apply parameter method to all subgoals\<close>
method_setup determ = \<open>Method.text_closure >> (fn m => fn ctxt => fn facts => let fun tac st' = method_evaluate m ctxt facts st'
in SIMPLE_METHOD (DETERM tac) facts end) \<close> \<open>constrain result sequence to 0 or 1 elements\<close>
method_setup changed = \<open>Method.text_closure >> (fn m => fn ctxt => fn facts => let fun tac st' = method_evaluate m ctxt facts st'
in SIMPLE_METHOD (CHANGED tac) facts end) \<close> \<open>fail if the proof state has not changed after parameter method has run\<close>
text\<open>The following \<open>fails\<close> and \<open>succeeds\<close> methods protect the goal from the effect
of a method, instead simply determining whether or not it can be applied to the current goal.
The \<open>fails\<close> method inverts success, only succeeding if the given method would fail.\<close>
method_setup fails = \<open>Method.text_closure >> (fn m => fn ctxt => fn facts => let fun fail_tac st' =
(case Seq.pull (method_evaluate m ctxt facts st') of
SOME _ => Seq.empty
| NONE => Seq.single st')
in SIMPLE_METHOD fail_tac facts end) \<close> \<open>succeed if the parameter method fails\<close>
method_setup succeeds = \<open>Method.text_closure >> (fn m => fn ctxt => fn facts => let fun can_tac st' =
(case Seq.pull (method_evaluate m ctxt facts st') of
SOME (st'',_) => Seq.single st'
| NONE => Seq.empty)
in SIMPLE_METHOD can_tac facts end) \<close> \<open>succeed without proof state change if the parameter method has non-empty result sequence\<close>
text\<open>Finding a goal based on successful application of a method\<close>
method_setup find_goal = \<open>Method.text_closure >> (fn m => fn ctxt => fn facts => let fun prefer_first i = SELECT_GOAL
(fn st' =>
(case Seq.pull (method_evaluate m ctxt facts st') of
SOME (st'',_) => Seq.single st''
| NONE => Seq.empty)) i THEN prefer_tac i
in SIMPLE_METHOD (FIRSTGOAL prefer_first) facts end)\<close> \<open>find first subgoal where parameter method succeeds, make this the first subgoal, and run method\<close>
end
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
