additional Eisbach combinators and utility methods
authorkleing
Sat Mar 17 18:51:56 2018 +1100 (14 months ago)
changeset 67899730fa992da38
parent 67898 736673784fac
child 67900 5a1b0076d7f0
additional Eisbach combinators and utility methods

(by Daniel Matichuck)
src/HOL/Eisbach/Eisbach.thy
     1.1 --- a/src/HOL/Eisbach/Eisbach.thy	Sat Mar 17 21:54:33 2018 +0100
     1.2 +++ b/src/HOL/Eisbach/Eisbach.thy	Sat Mar 17 18:51:56 2018 +1100
     1.3 @@ -20,6 +20,116 @@
     1.4  ML_file "eisbach_rule_insts.ML"
     1.5  ML_file "match_method.ML"
     1.6  
     1.7 +
     1.8  method solves methods m = (m; fail)
     1.9  
    1.10 +method repeat_new methods m = (m ; (repeat_new \<open>m\<close>)?)
    1.11 +
    1.12 +
    1.13 +section \<open>Debugging methods\<close>
    1.14 +
    1.15 +method_setup print_raw_goal = \<open>Scan.succeed (fn ctxt => fn facts =>
    1.16 +  (fn (ctxt, st) => (
    1.17 +     Output.writeln (Thm.string_of_thm ctxt st);
    1.18 +     Seq.make_results (Seq.single (ctxt, st)))))\<close>
    1.19 +
    1.20 +method_setup print_headgoal =
    1.21 +  \<open>Scan.succeed (fn ctxt => fn _ => fn (ctxt', thm) =>
    1.22 +    ((SUBGOAL (fn (t,_) =>
    1.23 +     (Output.writeln
    1.24 +     (Pretty.string_of (Syntax.pretty_term ctxt t)); all_tac)) 1 thm);
    1.25 +     (Seq.make_results (Seq.single (ctxt', thm)))))\<close>
    1.26 +
    1.27 +ML \<open>fun method_evaluate text ctxt facts =
    1.28 +  Method.NO_CONTEXT_TACTIC ctxt
    1.29 +    (Method.evaluate_runtime text ctxt facts)\<close>
    1.30 +
    1.31 +method_setup timeit =
    1.32 + \<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
    1.33 +   let
    1.34 +     fun timed_tac st seq = Seq.make (fn () => Option.map (apsnd (timed_tac st))
    1.35 +       (timeit (fn () => (Seq.pull seq))));
    1.36 +
    1.37 +     fun tac st' =
    1.38 +       timed_tac st' (method_evaluate m ctxt facts st');
    1.39 +
    1.40 +   in SIMPLE_METHOD tac [] end)
    1.41 +\<close>
    1.42 +
    1.43 +
    1.44 +section \<open>Simple Combinators\<close>
    1.45 +
    1.46 +method_setup defer_tac = \<open>Scan.succeed (fn _ => SIMPLE_METHOD (defer_tac 1))\<close>
    1.47 +method_setup prefer_last = \<open>Scan.succeed (fn _ => SIMPLE_METHOD (PRIMITIVE (Thm.permute_prems 0 ~1)))\<close>
    1.48 +
    1.49 +method_setup all =
    1.50 + \<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
    1.51 +   let
    1.52 +     fun tac i st' =
    1.53 +       Goal.restrict i 1 st'
    1.54 +       |> method_evaluate m ctxt facts
    1.55 +       |> Seq.map (Goal.unrestrict i)
    1.56 +
    1.57 +   in SIMPLE_METHOD (ALLGOALS tac) facts end)
    1.58 +\<close>
    1.59 +
    1.60 +method_setup determ =
    1.61 + \<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
    1.62 +   let
    1.63 +     fun tac st' = method_evaluate m ctxt facts st'
    1.64 +
    1.65 +   in SIMPLE_METHOD (DETERM tac) facts end)
    1.66 +\<close>
    1.67 +
    1.68 +method_setup changed =
    1.69 + \<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
    1.70 +   let
    1.71 +     fun tac st' = method_evaluate m ctxt facts st'
    1.72 +
    1.73 +   in SIMPLE_METHOD (CHANGED tac) facts end)
    1.74 +\<close>
    1.75 +
    1.76 +
    1.77 +text \<open>The following @{text fails} and @{text succeeds} methods protect the goal from the effect
    1.78 +      of a method, instead simply determining whether or not it can be applied to the current goal.
    1.79 +      The @{text fails} method inverts success, only succeeding if the given method would fail.\<close>
    1.80 +
    1.81 +method_setup fails =
    1.82 + \<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
    1.83 +   let
    1.84 +     fun fail_tac st' =
    1.85 +       (case Seq.pull (method_evaluate m ctxt facts st') of
    1.86 +          SOME _ => Seq.empty
    1.87 +        | NONE => Seq.single st')
    1.88 +
    1.89 +   in SIMPLE_METHOD fail_tac facts end)
    1.90 +\<close>
    1.91 +
    1.92 +method_setup succeeds =
    1.93 + \<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
    1.94 +   let
    1.95 +     fun can_tac st' =
    1.96 +       (case Seq.pull (method_evaluate m ctxt facts st') of
    1.97 +          SOME (st'',_) => Seq.single st'
    1.98 +        | NONE => Seq.empty)
    1.99 +
   1.100 +   in SIMPLE_METHOD can_tac facts end)
   1.101 +\<close>
   1.102 +
   1.103 +
   1.104 +
   1.105 +text \<open>Finding a goal based on successful application of a method\<close>
   1.106 +
   1.107 +method_setup find_goal =
   1.108 + \<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
   1.109 +   let
   1.110 +     fun prefer_first i = SELECT_GOAL
   1.111 +       (fn st' =>
   1.112 +         (case Seq.pull (method_evaluate m ctxt facts st') of
   1.113 +           SOME (st'',_) => Seq.single st''
   1.114 +         | NONE => Seq.empty)) i THEN prefer_tac i
   1.115 +
   1.116 +   in SIMPLE_METHOD (FIRSTGOAL prefer_first) facts end)\<close>
   1.117 +
   1.118 +
   1.119  end