src/HOL/Eisbach/Eisbach.thy
author kleing
Sat Mar 17 18:51:56 2018 +1100 (15 months ago)
changeset 67899 730fa992da38
parent 63527 59eff6e56d81
child 69272 15e9ed5b28fb
permissions -rw-r--r--
additional Eisbach combinators and utility methods

(by Daniel Matichuck)
     1 (*  Title:      HOL/Eisbach/Eisbach.thy
     2     Author:     Daniel Matichuk, NICTA/UNSW
     3 
     4 Main entry point for Eisbach proof method language.
     5 *)
     6 
     7 theory Eisbach
     8 imports Pure
     9 keywords
    10   "method" :: thy_decl and
    11   "conclusion"
    12   "declares"
    13   "methods"
    14   "\<bar>" "\<Rightarrow>"
    15   "uses"
    16 begin
    17 
    18 ML_file "parse_tools.ML"
    19 ML_file "method_closure.ML"
    20 ML_file "eisbach_rule_insts.ML"
    21 ML_file "match_method.ML"
    22 
    23 
    24 method solves methods m = (m; fail)
    25 
    26 method repeat_new methods m = (m ; (repeat_new \<open>m\<close>)?)
    27 
    28 
    29 section \<open>Debugging methods\<close>
    30 
    31 method_setup print_raw_goal = \<open>Scan.succeed (fn ctxt => fn facts =>
    32   (fn (ctxt, st) => (
    33      Output.writeln (Thm.string_of_thm ctxt st);
    34      Seq.make_results (Seq.single (ctxt, st)))))\<close>
    35 
    36 method_setup print_headgoal =
    37   \<open>Scan.succeed (fn ctxt => fn _ => fn (ctxt', thm) =>
    38     ((SUBGOAL (fn (t,_) =>
    39      (Output.writeln
    40      (Pretty.string_of (Syntax.pretty_term ctxt t)); all_tac)) 1 thm);
    41      (Seq.make_results (Seq.single (ctxt', thm)))))\<close>
    42 
    43 ML \<open>fun method_evaluate text ctxt facts =
    44   Method.NO_CONTEXT_TACTIC ctxt
    45     (Method.evaluate_runtime text ctxt facts)\<close>
    46 
    47 method_setup timeit =
    48  \<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
    49    let
    50      fun timed_tac st seq = Seq.make (fn () => Option.map (apsnd (timed_tac st))
    51        (timeit (fn () => (Seq.pull seq))));
    52 
    53      fun tac st' =
    54        timed_tac st' (method_evaluate m ctxt facts st');
    55 
    56    in SIMPLE_METHOD tac [] end)
    57 \<close>
    58 
    59 
    60 section \<open>Simple Combinators\<close>
    61 
    62 method_setup defer_tac = \<open>Scan.succeed (fn _ => SIMPLE_METHOD (defer_tac 1))\<close>
    63 method_setup prefer_last = \<open>Scan.succeed (fn _ => SIMPLE_METHOD (PRIMITIVE (Thm.permute_prems 0 ~1)))\<close>
    64 
    65 method_setup all =
    66  \<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
    67    let
    68      fun tac i st' =
    69        Goal.restrict i 1 st'
    70        |> method_evaluate m ctxt facts
    71        |> Seq.map (Goal.unrestrict i)
    72 
    73    in SIMPLE_METHOD (ALLGOALS tac) facts end)
    74 \<close>
    75 
    76 method_setup determ =
    77  \<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
    78    let
    79      fun tac st' = method_evaluate m ctxt facts st'
    80 
    81    in SIMPLE_METHOD (DETERM tac) facts end)
    82 \<close>
    83 
    84 method_setup changed =
    85  \<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
    86    let
    87      fun tac st' = method_evaluate m ctxt facts st'
    88 
    89    in SIMPLE_METHOD (CHANGED tac) facts end)
    90 \<close>
    91 
    92 
    93 text \<open>The following @{text fails} and @{text succeeds} methods protect the goal from the effect
    94       of a method, instead simply determining whether or not it can be applied to the current goal.
    95       The @{text fails} method inverts success, only succeeding if the given method would fail.\<close>
    96 
    97 method_setup fails =
    98  \<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
    99    let
   100      fun fail_tac st' =
   101        (case Seq.pull (method_evaluate m ctxt facts st') of
   102           SOME _ => Seq.empty
   103         | NONE => Seq.single st')
   104 
   105    in SIMPLE_METHOD fail_tac facts end)
   106 \<close>
   107 
   108 method_setup succeeds =
   109  \<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
   110    let
   111      fun can_tac st' =
   112        (case Seq.pull (method_evaluate m ctxt facts st') of
   113           SOME (st'',_) => Seq.single st'
   114         | NONE => Seq.empty)
   115 
   116    in SIMPLE_METHOD can_tac facts end)
   117 \<close>
   118 
   119 
   120 
   121 text \<open>Finding a goal based on successful application of a method\<close>
   122 
   123 method_setup find_goal =
   124  \<open>Method.text_closure >> (fn m => fn ctxt => fn facts =>
   125    let
   126      fun prefer_first i = SELECT_GOAL
   127        (fn st' =>
   128          (case Seq.pull (method_evaluate m ctxt facts st') of
   129            SOME (st'',_) => Seq.single st''
   130          | NONE => Seq.empty)) i THEN prefer_tac i
   131 
   132    in SIMPLE_METHOD (FIRSTGOAL prefer_first) facts end)\<close>
   133 
   134 
   135 end