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›

method_setup print_headgoal =
  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