1 (* Title: Pure/old_goals.ML |
|
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 Copyright 1993 University of Cambridge |
|
4 |
|
5 Old-style goal stack package. The goal stack initially holds a dummy |
|
6 proof, and can never become empty. Each goal stack consists of a list |
|
7 of levels. The undo list is a list of goal stacks. Finally, there |
|
8 may be a stack of pending proofs. |
|
9 *) |
|
10 |
|
11 signature OLD_GOALS = |
|
12 sig |
|
13 type proof |
|
14 val premises: unit -> thm list |
|
15 val reset_goals: unit -> unit |
|
16 val result_error_fn: (thm -> string -> thm) Unsynchronized.ref |
|
17 val print_sign_exn: theory -> exn -> 'a |
|
18 val prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm |
|
19 val prove_goalw_cterm_nocheck: thm list->cterm->(thm list->tactic list)->thm |
|
20 val prove_goalw: theory -> thm list -> string -> (thm list -> tactic list) -> thm |
|
21 val prove_goal: theory -> string -> (thm list -> tactic list) -> thm |
|
22 val topthm: unit -> thm |
|
23 val result: unit -> thm |
|
24 val uresult: unit -> thm |
|
25 val getgoal: int -> term |
|
26 val print_exn: exn -> 'a |
|
27 val filter_goal: (term*term->bool) -> thm list -> int -> thm list |
|
28 val prlev: int -> unit |
|
29 val pr: unit -> unit |
|
30 val prlim: int -> unit |
|
31 val goalw_cterm: thm list -> cterm -> thm list |
|
32 val goalw: theory -> thm list -> string -> thm list |
|
33 val goal: theory -> string -> thm list |
|
34 val Goalw: thm list -> string -> thm list |
|
35 val Goal: string -> thm list |
|
36 val simple_prove_goal_cterm: cterm->(thm list->tactic list)->thm |
|
37 val by: tactic -> unit |
|
38 val byev: tactic list -> unit |
|
39 val back: unit -> unit |
|
40 val choplev: int -> unit |
|
41 val chop: unit -> unit |
|
42 val undo: unit -> unit |
|
43 val save_proof: unit -> proof |
|
44 val restore_proof: proof -> thm list |
|
45 val push_proof: unit -> unit |
|
46 val pop_proof: unit -> thm list |
|
47 val rotate_proof: unit -> thm list |
|
48 val qed: string -> unit |
|
49 val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit |
|
50 val qed_goalw: string -> theory -> thm list -> string |
|
51 -> (thm list -> tactic list) -> unit |
|
52 val qed_spec_mp: string -> unit |
|
53 val qed_goal_spec_mp: string -> theory -> string -> (thm list -> tactic list) -> unit |
|
54 val qed_goalw_spec_mp: string -> theory -> thm list -> string |
|
55 -> (thm list -> tactic list) -> unit |
|
56 end; |
|
57 |
|
58 structure OldGoals: OLD_GOALS = |
|
59 struct |
|
60 |
|
61 |
|
62 (*** Goal package ***) |
|
63 |
|
64 (*Each level of goal stack includes a proof state and alternative states, |
|
65 the output of the tactic applied to the preceeding level. *) |
|
66 type gstack = (thm * thm Seq.seq) list; |
|
67 |
|
68 datatype proof = Proof of gstack list * thm list * (bool*thm->thm); |
|
69 |
|
70 |
|
71 (*** References ***) |
|
72 |
|
73 (*Current assumption list -- set by "goal".*) |
|
74 val curr_prems = Unsynchronized.ref([] : thm list); |
|
75 |
|
76 (*Return assumption list -- useful if you didn't save "goal"'s result. *) |
|
77 fun premises() = !curr_prems; |
|
78 |
|
79 (*Current result maker -- set by "goal", used by "result". *) |
|
80 fun init_mkresult _ = error "No goal has been supplied in subgoal module"; |
|
81 val curr_mkresult = Unsynchronized.ref (init_mkresult: bool*thm->thm); |
|
82 |
|
83 (*List of previous goal stacks, for the undo operation. Set by setstate. |
|
84 A list of lists!*) |
|
85 val undo_list = Unsynchronized.ref([[(asm_rl, Seq.empty)]] : gstack list); |
|
86 |
|
87 (* Stack of proof attempts *) |
|
88 val proofstack = Unsynchronized.ref([]: proof list); |
|
89 |
|
90 (*reset all refs*) |
|
91 fun reset_goals () = |
|
92 (curr_prems := []; curr_mkresult := init_mkresult; |
|
93 undo_list := [[(asm_rl, Seq.empty)]]); |
|
94 |
|
95 |
|
96 (*** Setting up goal-directed proof ***) |
|
97 |
|
98 (*Generates the list of new theories when the proof state's theory changes*) |
|
99 fun thy_error (thy,thy') = |
|
100 let val names = subtract (op =) (Context.display_names thy) (Context.display_names thy') |
|
101 in case names of |
|
102 [name] => "\nNew theory: " ^ name |
|
103 | _ => "\nNew theories: " ^ space_implode ", " names |
|
104 end; |
|
105 |
|
106 (*Default action is to print an error message; could be suppressed for |
|
107 special applications.*) |
|
108 fun result_error_default state msg : thm = |
|
109 Pretty.str "Bad final proof state:" :: |
|
110 Goal_Display.pretty_goals_without_context (!goals_limit) state @ |
|
111 [Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error; |
|
112 |
|
113 val result_error_fn = Unsynchronized.ref result_error_default; |
|
114 |
|
115 |
|
116 (*Common treatment of "goal" and "prove_goal": |
|
117 Return assumptions, initial proof state, and function to make result. |
|
118 "atomic" indicates if the goal should be wrapped up in the function |
|
119 "Goal::prop=>prop" to avoid assumptions being returned separately. |
|
120 *) |
|
121 fun prepare_proof atomic rths chorn = |
|
122 let |
|
123 val thy = Thm.theory_of_cterm chorn; |
|
124 val horn = Thm.term_of chorn; |
|
125 val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg; |
|
126 val (As, B) = Logic.strip_horn horn; |
|
127 val atoms = atomic andalso |
|
128 forall (fn t => not (can Logic.dest_implies t orelse Logic.is_all t)) As; |
|
129 val (As,B) = if atoms then ([],horn) else (As,B); |
|
130 val cAs = map (cterm_of thy) As; |
|
131 val prems = map (rewrite_rule rths o Thm.forall_elim_vars 0 o Thm.assume) cAs; |
|
132 val cB = cterm_of thy B; |
|
133 val st0 = let val st = Goal.init cB |> fold Thm.weaken cAs |
|
134 in rewrite_goals_rule rths st end |
|
135 (*discharges assumptions from state in the order they appear in goal; |
|
136 checks (if requested) that resulting theorem is equivalent to goal. *) |
|
137 fun mkresult (check,state) = |
|
138 let val state = Seq.hd (Thm.flexflex_rule state) |
|
139 handle THM _ => state (*smash flexflex pairs*) |
|
140 val ngoals = nprems_of state |
|
141 val ath = implies_intr_list cAs state |
|
142 val th = Goal.conclude ath |
|
143 val thy' = Thm.theory_of_thm th |
|
144 val {hyps, prop, ...} = Thm.rep_thm th |
|
145 val final_th = Drule.export_without_context th |
|
146 in if not check then final_th |
|
147 else if not (Theory.eq_thy(thy,thy')) then !result_error_fn state |
|
148 ("Theory of proof state has changed!" ^ |
|
149 thy_error (thy,thy')) |
|
150 else if ngoals>0 then !result_error_fn state |
|
151 (string_of_int ngoals ^ " unsolved goals!") |
|
152 else if not (null hyps) then !result_error_fn state |
|
153 ("Additional hypotheses:\n" ^ |
|
154 cat_lines (map (Syntax.string_of_term_global thy) hyps)) |
|
155 else if Pattern.matches thy |
|
156 (Envir.beta_norm (term_of chorn), Envir.beta_norm prop) |
|
157 then final_th |
|
158 else !result_error_fn state "proved a different theorem" |
|
159 end |
|
160 in |
|
161 if Theory.eq_thy(thy, Thm.theory_of_thm st0) |
|
162 then (prems, st0, mkresult) |
|
163 else error ("Definitions would change the proof state's theory" ^ |
|
164 thy_error (thy, Thm.theory_of_thm st0)) |
|
165 end |
|
166 handle THM(s,_,_) => error("prepare_proof: exception THM was raised!\n" ^ s); |
|
167 |
|
168 (*Prints exceptions readably to users*) |
|
169 fun print_sign_exn_unit thy e = |
|
170 case e of |
|
171 THM (msg,i,thms) => |
|
172 (writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg); |
|
173 List.app (writeln o Display.string_of_thm_global thy) thms) |
|
174 | THEORY (msg,thys) => |
|
175 (writeln ("Exception THEORY raised:\n" ^ msg); |
|
176 List.app (writeln o Context.str_of_thy) thys) |
|
177 | TERM (msg,ts) => |
|
178 (writeln ("Exception TERM raised:\n" ^ msg); |
|
179 List.app (writeln o Syntax.string_of_term_global thy) ts) |
|
180 | TYPE (msg,Ts,ts) => |
|
181 (writeln ("Exception TYPE raised:\n" ^ msg); |
|
182 List.app (writeln o Syntax.string_of_typ_global thy) Ts; |
|
183 List.app (writeln o Syntax.string_of_term_global thy) ts) |
|
184 | e => raise e; |
|
185 |
|
186 (*Prints an exception, then fails*) |
|
187 fun print_sign_exn thy e = (print_sign_exn_unit thy e; raise ERROR ""); |
|
188 |
|
189 (** the prove_goal.... commands |
|
190 Prove theorem using the listed tactics; check it has the specified form. |
|
191 Augment theory with all type assignments of goal. |
|
192 Syntax is similar to "goal" command for easy keyboard use. **) |
|
193 |
|
194 (*Version taking the goal as a cterm*) |
|
195 fun prove_goalw_cterm_general check rths chorn tacsf = |
|
196 let val (prems, st0, mkresult) = prepare_proof false rths chorn |
|
197 val tac = EVERY (tacsf prems) |
|
198 fun statef() = |
|
199 (case Seq.pull (tac st0) of |
|
200 SOME(st,_) => st |
|
201 | _ => error ("prove_goal: tactic failed")) |
|
202 in mkresult (check, cond_timeit (!Output.timing) "" statef) end; |
|
203 |
|
204 (*Two variants: one checking the result, one not. |
|
205 Neither prints runtime messages: they are for internal packages.*) |
|
206 fun prove_goalw_cterm rths chorn = |
|
207 setmp_CRITICAL Output.timing false (prove_goalw_cterm_general true rths chorn) |
|
208 and prove_goalw_cterm_nocheck rths chorn = |
|
209 setmp_CRITICAL Output.timing false (prove_goalw_cterm_general false rths chorn); |
|
210 |
|
211 |
|
212 (*Version taking the goal as a string*) |
|
213 fun prove_goalw thy rths agoal tacsf = |
|
214 let val chorn = cterm_of thy (Syntax.read_prop_global thy agoal) |
|
215 in prove_goalw_cterm_general true rths chorn tacsf end |
|
216 handle ERROR msg => cat_error msg (*from read_prop?*) |
|
217 ("The error(s) above occurred for " ^ quote agoal); |
|
218 |
|
219 (*String version with no meta-rewrite-rules*) |
|
220 fun prove_goal thy = prove_goalw thy []; |
|
221 |
|
222 |
|
223 |
|
224 (*** Commands etc ***) |
|
225 |
|
226 (*Return the current goal stack, if any, from undo_list*) |
|
227 fun getstate() : gstack = case !undo_list of |
|
228 [] => error"No current state in subgoal module" |
|
229 | x::_ => x; |
|
230 |
|
231 (*Pops the given goal stack*) |
|
232 fun pop [] = error"Cannot go back past the beginning of the proof!" |
|
233 | pop (pair::pairs) = (pair,pairs); |
|
234 |
|
235 |
|
236 (* Print a level of the goal stack *) |
|
237 |
|
238 fun print_top ((th, _), pairs) = |
|
239 let |
|
240 val n = length pairs; |
|
241 val m = (! goals_limit); |
|
242 val ngoals = nprems_of th; |
|
243 in |
|
244 [Pretty.str ("Level " ^ string_of_int n ^ |
|
245 (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^ |
|
246 (if ngoals <> 1 then "s" else "") ^ ")" |
|
247 else ""))] @ |
|
248 Goal_Display.pretty_goals_without_context m th |
|
249 end |> Pretty.chunks |> Pretty.writeln; |
|
250 |
|
251 (*Printing can raise exceptions, so the assignment occurs last. |
|
252 Can do setstate[(st,Seq.empty)] to set st as the state. *) |
|
253 fun setstate newgoals = |
|
254 (print_top (pop newgoals); undo_list := newgoals :: !undo_list); |
|
255 |
|
256 (*Given a proof state transformation, return a command that updates |
|
257 the goal stack*) |
|
258 fun make_command com = setstate (com (pop (getstate()))); |
|
259 |
|
260 (*Apply a function on proof states to the current goal stack*) |
|
261 fun apply_fun f = f (pop(getstate())); |
|
262 |
|
263 (*Return the top theorem, representing the proof state*) |
|
264 fun topthm () = apply_fun (fn ((th,_), _) => th); |
|
265 |
|
266 (*Return the final result. *) |
|
267 fun result () = !curr_mkresult (true, topthm()); |
|
268 |
|
269 (*Return the result UNCHECKED that it equals the goal -- for synthesis, |
|
270 answer extraction, or other instantiation of Vars *) |
|
271 fun uresult () = !curr_mkresult (false, topthm()); |
|
272 |
|
273 (*Get subgoal i from goal stack*) |
|
274 fun getgoal i = Logic.get_goal (prop_of (topthm())) i; |
|
275 |
|
276 (*Prints exceptions nicely at top level; |
|
277 raises the exception in order to have a polymorphic type!*) |
|
278 fun print_exn e = (print_sign_exn_unit (Thm.theory_of_thm (topthm())) e; raise e); |
|
279 |
|
280 (*Which thms could apply to goal i? (debugs tactics involving filter_thms) *) |
|
281 fun filter_goal could ths i = filter_thms could (999, getgoal i, ths); |
|
282 |
|
283 (*For inspecting earlier levels of the backward proof*) |
|
284 fun chop_level n (pair,pairs) = |
|
285 let val level = length pairs |
|
286 in if n<0 andalso ~n <= level |
|
287 then List.drop (pair::pairs, ~n) |
|
288 else if 0<=n andalso n<= level |
|
289 then List.drop (pair::pairs, level - n) |
|
290 else error ("Level number must lie between 0 and " ^ |
|
291 string_of_int level) |
|
292 end; |
|
293 |
|
294 (*Print the given level of the proof; prlev ~1 prints previous level*) |
|
295 fun prlev n = apply_fun (print_top o pop o (chop_level n)); |
|
296 fun pr () = apply_fun print_top; |
|
297 |
|
298 (*Set goals_limit and print again*) |
|
299 fun prlim n = (goals_limit:=n; pr()); |
|
300 |
|
301 (** the goal.... commands |
|
302 Read main goal. Set global variables curr_prems, curr_mkresult. |
|
303 Initial subgoal and premises are rewritten using rths. **) |
|
304 |
|
305 (*Version taking the goal as a cterm; if you have a term t and theory thy, use |
|
306 goalw_cterm rths (cterm_of thy t); *) |
|
307 fun agoalw_cterm atomic rths chorn = |
|
308 let val (prems, st0, mkresult) = prepare_proof atomic rths chorn |
|
309 in undo_list := []; |
|
310 setstate [ (st0, Seq.empty) ]; |
|
311 curr_prems := prems; |
|
312 curr_mkresult := mkresult; |
|
313 prems |
|
314 end; |
|
315 |
|
316 val goalw_cterm = agoalw_cterm false; |
|
317 |
|
318 (*Version taking the goal as a string*) |
|
319 fun agoalw atomic thy rths agoal = |
|
320 agoalw_cterm atomic rths (cterm_of thy (Syntax.read_prop_global thy agoal)) |
|
321 handle ERROR msg => cat_error msg (*from type_assign, etc via prepare_proof*) |
|
322 ("The error(s) above occurred for " ^ quote agoal); |
|
323 |
|
324 val goalw = agoalw false; |
|
325 fun goal thy = goalw thy []; |
|
326 |
|
327 (*now the versions that wrap the goal up in `Goal' to make it atomic*) |
|
328 fun Goalw thms s = agoalw true (ML_Context.the_global_context ()) thms s; |
|
329 val Goal = Goalw []; |
|
330 |
|
331 (*simple version with minimal amount of checking and postprocessing*) |
|
332 fun simple_prove_goal_cterm G f = |
|
333 let |
|
334 val As = Drule.strip_imp_prems G; |
|
335 val B = Drule.strip_imp_concl G; |
|
336 val asms = map Assumption.assume As; |
|
337 fun check NONE = error "prove_goal: tactic failed" |
|
338 | check (SOME (thm, _)) = (case nprems_of thm of |
|
339 0 => thm |
|
340 | i => !result_error_fn thm (string_of_int i ^ " unsolved goals!")) |
|
341 in |
|
342 Drule.export_without_context (implies_intr_list As |
|
343 (check (Seq.pull (EVERY (f asms) (Thm.trivial B))))) |
|
344 end; |
|
345 |
|
346 |
|
347 (*Proof step "by" the given tactic -- apply tactic to the proof state*) |
|
348 fun by_com tac ((th,ths), pairs) : gstack = |
|
349 (case Seq.pull(tac th) of |
|
350 NONE => error"by: tactic failed" |
|
351 | SOME(th2,ths2) => |
|
352 (if Thm.eq_thm(th,th2) |
|
353 then warning "Warning: same as previous level" |
|
354 else if Thm.eq_thm_thy(th,th2) then () |
|
355 else warning ("Warning: theory of proof state has changed" ^ |
|
356 thy_error (Thm.theory_of_thm th, Thm.theory_of_thm th2)); |
|
357 ((th2,ths2)::(th,ths)::pairs))); |
|
358 |
|
359 fun by tac = cond_timeit (!Output.timing) "" |
|
360 (fn() => make_command (by_com tac)); |
|
361 |
|
362 (* byev[tac1,...,tacn] applies tac1 THEN ... THEN tacn. |
|
363 Good for debugging proofs involving prove_goal.*) |
|
364 val byev = by o EVERY; |
|
365 |
|
366 |
|
367 (*Backtracking means find an alternative result from a tactic. |
|
368 If none at this level, try earlier levels*) |
|
369 fun backtrack [] = error"back: no alternatives" |
|
370 | backtrack ((th,thstr) :: pairs) = |
|
371 (case Seq.pull thstr of |
|
372 NONE => (writeln"Going back a level..."; backtrack pairs) |
|
373 | SOME(th2,thstr2) => |
|
374 (if Thm.eq_thm(th,th2) |
|
375 then warning "Warning: same as previous choice at this level" |
|
376 else if Thm.eq_thm_thy(th,th2) then () |
|
377 else warning "Warning: theory of proof state has changed"; |
|
378 (th2,thstr2)::pairs)); |
|
379 |
|
380 fun back() = setstate (backtrack (getstate())); |
|
381 |
|
382 (*Chop back to previous level of the proof*) |
|
383 fun choplev n = make_command (chop_level n); |
|
384 |
|
385 (*Chopping back the goal stack*) |
|
386 fun chop () = make_command (fn (_,pairs) => pairs); |
|
387 |
|
388 (*Restore the previous proof state; discard current state. *) |
|
389 fun undo() = case !undo_list of |
|
390 [] => error"No proof state" |
|
391 | [_] => error"Already at initial state" |
|
392 | _::newundo => (undo_list := newundo; pr()) ; |
|
393 |
|
394 |
|
395 (*** Managing the proof stack ***) |
|
396 |
|
397 fun save_proof() = Proof(!undo_list, !curr_prems, !curr_mkresult); |
|
398 |
|
399 fun restore_proof(Proof(ul,prems,mk)) = |
|
400 (undo_list:= ul; curr_prems:= prems; curr_mkresult := mk; prems); |
|
401 |
|
402 |
|
403 fun top_proof() = case !proofstack of |
|
404 [] => error("Stack of proof attempts is empty!") |
|
405 | p::ps => (p,ps); |
|
406 |
|
407 (* push a copy of the current proof state on to the stack *) |
|
408 fun push_proof() = (proofstack := (save_proof() :: !proofstack)); |
|
409 |
|
410 (* discard the top proof state of the stack *) |
|
411 fun pop_proof() = |
|
412 let val (p,ps) = top_proof() |
|
413 val prems = restore_proof p |
|
414 in proofstack := ps; pr(); prems end; |
|
415 |
|
416 (* rotate the stack so that the top element goes to the bottom *) |
|
417 fun rotate_proof() = |
|
418 let val (p,ps) = top_proof() |
|
419 in proofstack := ps@[save_proof()]; |
|
420 restore_proof p; |
|
421 pr(); |
|
422 !curr_prems |
|
423 end; |
|
424 |
|
425 |
|
426 (** theorem bindings **) |
|
427 |
|
428 fun qed name = ML_Context.ml_store_thm (name, result ()); |
|
429 fun qed_goal name thy goal tacsf = ML_Context.ml_store_thm (name, prove_goal thy goal tacsf); |
|
430 fun qed_goalw name thy rews goal tacsf = |
|
431 ML_Context.ml_store_thm (name, prove_goalw thy rews goal tacsf); |
|
432 fun qed_spec_mp name = |
|
433 ML_Context.ml_store_thm (name, Object_Logic.rulify_no_asm (result ())); |
|
434 fun qed_goal_spec_mp name thy s p = |
|
435 bind_thm (name, Object_Logic.rulify_no_asm (prove_goal thy s p)); |
|
436 fun qed_goalw_spec_mp name thy defs s p = |
|
437 bind_thm (name, Object_Logic.rulify_no_asm (prove_goalw thy defs s p)); |
|
438 |
|
439 end; |
|
440 |
|