Theory HOL-Eisbach.Eisbach

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