# Theory HOL-Eisbach.Eisbach

```(*  Title:      HOL/Eisbach/Eisbach.thy
Author:     Daniel Matichuk, NICTA/UNSW

Main entry point for Eisbach proof method language.
*)

theory Eisbach
imports Pure
keywords
"method" :: thy_decl and
"conclusion"
"declares"
"methods"
"¦" "⇒"
"uses"
begin

ML_file ‹parse_tools.ML›
ML_file ‹method_closure.ML›
ML_file ‹eisbach_rule_insts.ML›
ML_file ‹match_method.ML›

method solves methods m ‹Apply method only when it solves the goal› = m; fail

method repeat_new methods m
‹apply method recursively to the subgoals it generates› =
(m ; (repeat_new ‹m›)?)

section ‹Debugging methods›

method_setup print_raw_goal = ‹Scan.succeed (fn ctxt => fn facts =>
(fn (ctxt, st) => (
Output.writeln (Thm.string_of_thm ctxt st);
Seq.make_results (Seq.single (ctxt, st)))))›
‹print the entire goal statement›

‹Scan.succeed (fn ctxt => fn _ => fn (ctxt', thm) =>
((SUBGOAL (fn (t,_) =>
(Output.writeln
(Pretty.string_of (Syntax.pretty_term ctxt t)); all_tac)) 1 thm);
(Seq.make_results (Seq.single (ctxt', thm)))))›
‹print the first subgoal›

ML ‹fun method_evaluate text ctxt facts =
NO_CONTEXT_TACTIC ctxt
(Method.evaluate_runtime text ctxt facts)›

method_setup timeit =
‹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)
›
‹print timing information from running the parameter method›

section ‹Simple Combinators›

method_setup defer_tac =
‹Scan.succeed (fn _ => SIMPLE_METHOD (defer_tac 1))›
‹make first subgoal the last subgoal. Like "defer" but as proof method›

method_setup prefer_last =
‹Scan.succeed (fn _ => SIMPLE_METHOD (PRIMITIVE (Thm.permute_prems 0 ~1)))›
‹make last subgoal the first subgoal.›

method_setup all =
‹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)
›
‹apply parameter method to all subgoals›

method_setup determ =
‹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)
›
‹constrain result sequence to 0 or 1 elements›

method_setup changed =
‹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)
›
‹fail if the proof state has not changed after parameter method has run›

text ‹The following ‹fails› and ‹succeeds› 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 ‹fails› method inverts success, only succeeding if the given method would fail.›

method_setup fails =
‹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)
›
‹succeed if the parameter method fails›

method_setup succeeds =
‹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)
›
‹succeed without proof state change if the parameter method has non-empty result sequence›

text ‹Finding a goal based on successful application of a method›

method_setup find_goal =
‹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)›
‹find first subgoal where parameter method succeeds, make this the first subgoal, and run method›

end
```