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