5824
|
1 |
(* Title: Pure/Isar/method.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel, TU Muenchen
|
|
4 |
|
|
5 |
Proof methods.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature BASIC_METHOD =
|
|
9 |
sig
|
|
10 |
val print_methods: theory -> unit
|
|
11 |
val Method: bstring -> (Args.src -> Proof.context -> Proof.method) -> string -> unit
|
|
12 |
end;
|
|
13 |
|
|
14 |
signature METHOD =
|
|
15 |
sig
|
|
16 |
include BASIC_METHOD
|
|
17 |
val LIFT: tactic -> thm -> (thm * (indexname * term) list * (string * tthm list) list) Seq.seq
|
|
18 |
val METHOD: (tthm list -> tactic) -> Proof.method
|
|
19 |
val METHOD0: tactic -> Proof.method
|
|
20 |
val fail: Proof.method
|
|
21 |
val succeed: Proof.method
|
|
22 |
val trivial: Proof.method
|
|
23 |
val assumption: Proof.method
|
|
24 |
val forward_chain: thm list -> thm list -> thm Seq.seq
|
|
25 |
val rule_tac: tthm list -> tthm list -> int -> tactic
|
|
26 |
val rule: tthm list -> Proof.method
|
|
27 |
val method: theory -> Args.src -> Proof.context -> Proof.method
|
|
28 |
val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list
|
|
29 |
-> theory -> theory
|
|
30 |
datatype text =
|
|
31 |
Basic of (Proof.context -> Proof.method) |
|
|
32 |
Source of Args.src |
|
|
33 |
Then of text list |
|
|
34 |
Orelse of text list |
|
|
35 |
Try of text |
|
|
36 |
Repeat of text |
|
|
37 |
Repeat1 of text
|
|
38 |
val dynamic_method: string -> (Proof.context -> Proof.method)
|
|
39 |
val refine: text -> Proof.state -> Proof.state Seq.seq
|
|
40 |
val tac: text -> Proof.state -> Proof.state Seq.seq
|
|
41 |
val etac: text -> Proof.state -> Proof.state Seq.seq
|
|
42 |
val proof: text option -> Proof.state -> Proof.state Seq.seq
|
|
43 |
val end_block: Proof.state -> Proof.state Seq.seq
|
|
44 |
val terminal_proof: text -> Proof.state -> Proof.state Seq.seq
|
|
45 |
val trivial_proof: Proof.state -> Proof.state Seq.seq
|
|
46 |
val default_proof: Proof.state -> Proof.state Seq.seq
|
|
47 |
val qed: bstring option -> theory attribute list option -> Proof.state
|
|
48 |
-> theory * (string * string * tthm)
|
|
49 |
val syntax: (Args.T list -> 'a * Args.T list) -> ('a -> 'b) -> Args.src -> 'b
|
|
50 |
val no_args: 'a -> Args.src -> Proof.context -> 'a
|
|
51 |
val thm_args: (tthm list -> 'a) -> Args.src -> Proof.context -> 'a
|
|
52 |
val sectioned_args: (Proof.context -> 'a) -> ('a * tthm list -> 'b) ->
|
|
53 |
(string * ('b * tthm list -> 'b)) list -> ('b -> 'c) -> Args.src -> Proof.context -> 'c
|
|
54 |
val setup: (theory -> theory) list
|
|
55 |
end;
|
|
56 |
|
|
57 |
structure Method: METHOD =
|
|
58 |
struct
|
|
59 |
|
|
60 |
|
|
61 |
(** proof methods **)
|
|
62 |
|
|
63 |
(* method from tactic *)
|
|
64 |
|
|
65 |
fun LIFT tac goal = Seq.map (fn x => (x, [], [])) (tac goal);
|
|
66 |
fun METHOD tacf = Proof.method (LIFT o tacf);
|
|
67 |
fun METHOD0 tac = METHOD (fn [] => tac | _ => error "Method may not be used with facts");
|
|
68 |
|
|
69 |
|
|
70 |
(* primitive *)
|
|
71 |
|
|
72 |
val fail = METHOD (K no_tac);
|
|
73 |
val succeed = METHOD (K all_tac);
|
|
74 |
|
|
75 |
|
|
76 |
(* trivial, assumption *)
|
|
77 |
|
|
78 |
fun trivial_tac [] = K all_tac
|
|
79 |
| trivial_tac facts =
|
|
80 |
let
|
|
81 |
val thms = map Attribute.thm_of facts;
|
|
82 |
val r = ~ (length facts);
|
|
83 |
in metacuts_tac thms THEN' rotate_tac r end;
|
|
84 |
|
|
85 |
val trivial = METHOD (ALLGOALS o trivial_tac);
|
|
86 |
val assumption = METHOD (fn facts => FIRSTGOAL (trivial_tac facts THEN' assume_tac));
|
|
87 |
|
|
88 |
val asm_finish = METHOD (K (TRYALL assume_tac));
|
|
89 |
|
|
90 |
|
|
91 |
(* rule *)
|
|
92 |
|
|
93 |
fun res th i rule = Thm.biresolution false [(false, th)] i rule handle THM _ => Seq.empty;
|
|
94 |
|
|
95 |
fun multi_resolve facts rule =
|
|
96 |
let
|
|
97 |
fun multi_res i [] = Seq.single rule
|
|
98 |
| multi_res i (th :: ths) = Seq.flat (Seq.map (res th i) (multi_res (i + 1) ths))
|
|
99 |
in multi_res 1 facts end;
|
|
100 |
|
|
101 |
fun forward_chain facts rules = Seq.flat (Seq.map (multi_resolve facts) (Seq.of_list rules));
|
|
102 |
|
|
103 |
fun rule_tac rules [] = resolve_tac (map Attribute.thm_of rules)
|
|
104 |
| rule_tac erules facts =
|
|
105 |
let
|
|
106 |
val rules = forward_chain (map Attribute.thm_of facts) (map Attribute.thm_of erules);
|
|
107 |
fun tac i state = Seq.flat (Seq.map (fn rule => Tactic.rtac rule i state) rules);
|
|
108 |
in tac end;
|
|
109 |
|
|
110 |
fun rule rules = METHOD (FIRSTGOAL o rule_tac rules);
|
|
111 |
|
|
112 |
|
|
113 |
|
|
114 |
(** methods theory data **)
|
|
115 |
|
|
116 |
(* data kind 'Isar/methods' *)
|
|
117 |
|
|
118 |
structure MethodsDataArgs =
|
|
119 |
struct
|
|
120 |
val name = "Isar/methods";
|
|
121 |
type T =
|
|
122 |
{space: NameSpace.T,
|
|
123 |
meths: (((Args.src -> Proof.context -> Proof.method) * string) * stamp) Symtab.table};
|
|
124 |
|
|
125 |
val empty = {space = NameSpace.empty, meths = Symtab.empty};
|
|
126 |
val prep_ext = I;
|
|
127 |
fun merge ({space = space1, meths = meths1}, {space = space2, meths = meths2}) =
|
|
128 |
{space = NameSpace.merge (space1, space2),
|
|
129 |
meths = Symtab.merge eq_snd (meths1, meths2) handle Symtab.DUPS dups =>
|
|
130 |
error ("Attempt to merge different versions of methods " ^ commas_quote dups)};
|
|
131 |
|
|
132 |
fun print _ {space, meths} =
|
|
133 |
let
|
|
134 |
fun prt_meth (name, ((_, comment), _)) = Pretty.block
|
|
135 |
[Pretty.str (NameSpace.cond_extern space name ^ ":"), Pretty.brk 2, Pretty.str comment];
|
|
136 |
in
|
|
137 |
Pretty.writeln (Display.pretty_name_space ("method name space", space));
|
|
138 |
Pretty.writeln (Pretty.big_list "methods:" (map prt_meth (Symtab.dest meths)))
|
|
139 |
end;
|
|
140 |
end;
|
|
141 |
|
|
142 |
structure MethodsData = TheoryDataFun(MethodsDataArgs);
|
|
143 |
val print_methods = MethodsData.print;
|
|
144 |
|
|
145 |
|
|
146 |
(* get methods *)
|
|
147 |
|
|
148 |
fun method thy =
|
|
149 |
let
|
|
150 |
val {space, meths} = MethodsData.get thy;
|
|
151 |
|
|
152 |
fun meth ((raw_name, args), pos) =
|
|
153 |
let val name = NameSpace.intern space raw_name in
|
|
154 |
(case Symtab.lookup (meths, name) of
|
|
155 |
None => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos)
|
|
156 |
| Some ((mth, _), _) => mth ((name, args), pos))
|
|
157 |
end;
|
|
158 |
in meth end;
|
|
159 |
|
|
160 |
|
|
161 |
(* add_methods *)
|
|
162 |
|
|
163 |
fun add_methods raw_meths thy =
|
|
164 |
let
|
|
165 |
val full = Sign.full_name (Theory.sign_of thy);
|
|
166 |
val new_meths =
|
|
167 |
map (fn (name, f, comment) => (full name, ((f, comment), stamp ()))) raw_meths;
|
|
168 |
|
|
169 |
val {space, meths} = MethodsData.get thy;
|
|
170 |
val space' = NameSpace.extend (space, map fst new_meths);
|
|
171 |
val meths' = Symtab.extend (meths, new_meths) handle Symtab.DUPS dups =>
|
|
172 |
error ("Duplicate declaration of method(s) " ^ commas_quote dups);
|
|
173 |
in
|
|
174 |
thy |> MethodsData.put {space = space', meths = meths'}
|
|
175 |
end;
|
|
176 |
|
|
177 |
(*implicit version*)
|
|
178 |
fun Method name meth cmt = Context.>> (add_methods [(name, meth, cmt)]);
|
|
179 |
|
|
180 |
|
|
181 |
(* argument syntax *)
|
|
182 |
|
|
183 |
val methodN = "method";
|
|
184 |
fun syntax scan = Args.syntax methodN scan;
|
|
185 |
|
|
186 |
fun no_args x = syntax (Scan.succeed (fn (_: Proof.context) => x)) I;
|
|
187 |
|
|
188 |
(* FIXME move? *)
|
|
189 |
fun thm_args f = syntax (Scan.repeat Args.name)
|
|
190 |
(fn names => fn ctxt => f (ProofContext.get_tthmss ctxt names));
|
|
191 |
|
|
192 |
fun sectioned_args get_data def_sect sects f =
|
|
193 |
syntax (Args.sectioned (map fst sects))
|
|
194 |
(fn (names, sect_names) => fn ctxt =>
|
|
195 |
let
|
|
196 |
val get_thms = ProofContext.get_tthmss ctxt;
|
|
197 |
val thms = get_thms names;
|
|
198 |
val sect_thms = map (apsnd get_thms) sect_names;
|
|
199 |
|
|
200 |
fun apply_sect (data, (s, ths)) =
|
|
201 |
(case assoc (sects, s) of
|
|
202 |
Some add => add (data, ths)
|
|
203 |
| None => error ("Unknown argument section " ^ quote s));
|
|
204 |
in f (foldl apply_sect (def_sect (get_data ctxt, thms), sect_thms)) end);
|
|
205 |
|
|
206 |
|
|
207 |
|
|
208 |
(** method text **)
|
|
209 |
|
|
210 |
(* datatype text *)
|
|
211 |
|
|
212 |
datatype text =
|
|
213 |
Basic of (Proof.context -> Proof.method) |
|
|
214 |
Source of Args.src |
|
|
215 |
Then of text list |
|
|
216 |
Orelse of text list |
|
|
217 |
Try of text |
|
|
218 |
Repeat of text |
|
|
219 |
Repeat1 of text;
|
|
220 |
|
|
221 |
|
|
222 |
(* dynamic methods *)
|
|
223 |
|
|
224 |
fun dynamic_method name = (fn ctxt =>
|
|
225 |
method (ProofContext.theory_of ctxt) ((name, []), Position.none) ctxt);
|
|
226 |
|
|
227 |
|
|
228 |
(* refine *)
|
|
229 |
|
|
230 |
fun refine text state =
|
|
231 |
let
|
|
232 |
val thy = Proof.theory_of state;
|
|
233 |
|
|
234 |
fun eval (Basic mth) = Proof.refine mth
|
|
235 |
| eval (Source src) = Proof.refine (method thy src)
|
|
236 |
| eval (Then txts) = Seq.EVERY (map eval txts)
|
|
237 |
| eval (Orelse txts) = Seq.FIRST (map eval txts)
|
|
238 |
| eval (Try txt) = Seq.TRY (eval txt)
|
|
239 |
| eval (Repeat txt) = Seq.REPEAT (eval txt)
|
|
240 |
| eval (Repeat1 txt) = Seq.REPEAT1 (eval txt);
|
|
241 |
in eval text state end;
|
|
242 |
|
|
243 |
|
|
244 |
(* unstructured steps *)
|
|
245 |
|
|
246 |
fun tac text state =
|
|
247 |
state
|
|
248 |
|> Proof.goal_facts (K [])
|
|
249 |
|> refine text;
|
|
250 |
|
|
251 |
fun etac text state =
|
|
252 |
state
|
|
253 |
|> Proof.goal_facts Proof.the_facts
|
|
254 |
|> refine text;
|
|
255 |
|
|
256 |
|
|
257 |
(* proof steps *)
|
|
258 |
|
|
259 |
val default_txt = Source (("default", []), Position.none);
|
|
260 |
val finishN = "finish";
|
|
261 |
|
|
262 |
fun proof opt_text state =
|
|
263 |
state
|
|
264 |
|> Proof.assert_backward
|
|
265 |
|> refine (if_none opt_text default_txt)
|
|
266 |
|> Seq.map Proof.enter_forward;
|
|
267 |
|
|
268 |
|
|
269 |
(* conclusions *)
|
|
270 |
|
|
271 |
val end_block = Proof.end_block (dynamic_method finishN);
|
|
272 |
|
|
273 |
fun terminal_proof text = Seq.THEN (proof (Some text), end_block);
|
|
274 |
val trivial_proof = terminal_proof (Basic (K trivial));
|
|
275 |
val default_proof = terminal_proof default_txt;
|
|
276 |
|
|
277 |
val qed = Proof.qed (dynamic_method finishN);
|
|
278 |
|
|
279 |
|
|
280 |
|
|
281 |
(** theory setup **)
|
|
282 |
|
|
283 |
(* pure_methods *)
|
|
284 |
|
|
285 |
val pure_methods =
|
|
286 |
[("fail", no_args fail, "force failure"),
|
|
287 |
("succeed", no_args succeed, "succeed"),
|
|
288 |
("trivial", no_args trivial, "proof all goals trivially"),
|
|
289 |
("assumption", no_args assumption, "proof by assumption"),
|
|
290 |
("finish", no_args asm_finish, "finish proof by assumption"),
|
|
291 |
("rule", thm_args rule, "apply primitive rule")];
|
|
292 |
|
|
293 |
|
|
294 |
(* setup *)
|
|
295 |
|
|
296 |
val setup = [MethodsData.init, add_methods pure_methods];
|
|
297 |
|
|
298 |
|
|
299 |
end;
|
|
300 |
|
|
301 |
|
|
302 |
structure BasicMethod: BASIC_METHOD = Method;
|
|
303 |
open BasicMethod;
|