author | wenzelm |
Mon, 06 Oct 1997 18:22:22 +0200 | |
changeset 3776 | 38f8ec304b95 |
parent 3707 | 40856b593501 |
child 3853 | 73c074f41749 |
permissions | -rw-r--r-- |
1460 | 1 |
(* Title: Pure/goals.ML |
0 | 2 |
ID: $Id$ |
1460 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
6 |
Goal stack package. The goal stack initially holds a dummy proof, and can |
|
7 |
never become empty. Each goal stack consists of a list of levels. The |
|
8 |
undo list is a list of goal stacks. Finally, there may be a stack of |
|
9 |
pending proofs. |
|
10 |
*) |
|
11 |
||
12 |
||
13 |
signature GOALS = |
|
14 |
sig |
|
15 |
type proof |
|
1460 | 16 |
val ba : int -> unit |
17 |
val back : unit -> unit |
|
18 |
val bd : thm -> int -> unit |
|
19 |
val bds : thm list -> int -> unit |
|
20 |
val be : thm -> int -> unit |
|
21 |
val bes : thm list -> int -> unit |
|
22 |
val br : thm -> int -> unit |
|
23 |
val brs : thm list -> int -> unit |
|
24 |
val bw : thm -> unit |
|
25 |
val bws : thm list -> unit |
|
26 |
val by : tactic -> unit |
|
27 |
val byev : tactic list -> unit |
|
28 |
val chop : unit -> unit |
|
29 |
val choplev : int -> unit |
|
30 |
val fa : unit -> unit |
|
31 |
val fd : thm -> unit |
|
32 |
val fds : thm list -> unit |
|
33 |
val fe : thm -> unit |
|
34 |
val fes : thm list -> unit |
|
35 |
val filter_goal : (term*term->bool) -> thm list -> int -> thm list |
|
36 |
val fr : thm -> unit |
|
37 |
val frs : thm list -> unit |
|
38 |
val getgoal : int -> term |
|
39 |
val gethyps : int -> thm list |
|
40 |
val goal : theory -> string -> thm list |
|
41 |
val goalw : theory -> thm list -> string -> thm list |
|
42 |
val goalw_cterm : thm list -> cterm -> thm list |
|
3532 | 43 |
val print_current_goals_fn : (int -> int -> thm -> unit) ref |
1460 | 44 |
val pop_proof : unit -> thm list |
45 |
val pr : unit -> unit |
|
2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2514
diff
changeset
|
46 |
val prlev : int -> unit |
2514 | 47 |
val prlim : int -> unit |
1628
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
48 |
val pr_latex : unit -> unit |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
49 |
val printgoal_latex : int -> unit |
1460 | 50 |
val premises : unit -> thm list |
51 |
val prin : term -> unit |
|
52 |
val printyp : typ -> unit |
|
53 |
val pprint_term : term -> pprint_args -> unit |
|
54 |
val pprint_typ : typ -> pprint_args -> unit |
|
55 |
val print_exn : exn -> 'a |
|
56 |
val print_sign_exn : Sign.sg -> exn -> 'a |
|
57 |
val proof_timing : bool ref |
|
58 |
val prove_goal : theory -> string -> (thm list -> tactic list) -> thm |
|
577 | 59 |
val prove_goalw : theory->thm list->string->(thm list->tactic list)->thm |
1460 | 60 |
val prove_goalw_cterm : thm list->cterm->(thm list->tactic list)->thm |
61 |
val push_proof : unit -> unit |
|
62 |
val read : string -> term |
|
63 |
val ren : string -> int -> unit |
|
64 |
val restore_proof : proof -> thm list |
|
65 |
val result : unit -> thm |
|
3532 | 66 |
val result_error_fn : (thm -> string -> thm) ref |
1460 | 67 |
val rotate_proof : unit -> thm list |
68 |
val uresult : unit -> thm |
|
69 |
val save_proof : unit -> proof |
|
70 |
val topthm : unit -> thm |
|
71 |
val undo : unit -> unit |
|
0 | 72 |
end; |
73 |
||
1500 | 74 |
structure Goals : GOALS = |
0 | 75 |
struct |
76 |
||
77 |
(*Each level of goal stack includes a proof state and alternative states, |
|
78 |
the output of the tactic applied to the preceeding level. *) |
|
79 |
type gstack = (thm * thm Sequence.seq) list; |
|
80 |
||
81 |
datatype proof = Proof of gstack list * thm list * (bool*thm->thm); |
|
82 |
||
83 |
(*** References ***) |
|
84 |
||
85 |
(*Should process time be printed after proof steps?*) |
|
86 |
val proof_timing = ref false; |
|
87 |
||
88 |
(*Current assumption list -- set by "goal".*) |
|
89 |
val curr_prems = ref([] : thm list); |
|
90 |
||
91 |
(*Return assumption list -- useful if you didn't save "goal"'s result. *) |
|
92 |
fun premises() = !curr_prems; |
|
93 |
||
94 |
(*Current result maker -- set by "goal", used by "result". *) |
|
95 |
val curr_mkresult = |
|
96 |
ref((fn _=> error"No goal has been supplied in subgoal module") |
|
97 |
: bool*thm->thm); |
|
98 |
||
2878
bf7b6833e4d7
changed signature of dummy goal from proto_pure to pure;
wenzelm
parents:
2580
diff
changeset
|
99 |
val dummy = trivial(read_cterm Sign.pure |
0 | 100 |
("PROP No_goal_has_been_supplied",propT)); |
101 |
||
102 |
(*List of previous goal stacks, for the undo operation. Set by setstate. |
|
103 |
A list of lists!*) |
|
104 |
val undo_list = ref([[(dummy, Sequence.null)]] : gstack list); |
|
105 |
||
106 |
(* Stack of proof attempts *) |
|
107 |
val proofstack = ref([]: proof list); |
|
108 |
||
109 |
||
110 |
(*** Setting up goal-directed proof ***) |
|
111 |
||
112 |
(*Generates the list of new theories when the proof state's signature changes*) |
|
113 |
fun sign_error (sign,sign') = |
|
114 |
let val stamps = #stamps(Sign.rep_sg sign') \\ |
|
115 |
#stamps(Sign.rep_sg sign) |
|
116 |
in case stamps of |
|
117 |
[stamp] => "\nNew theory: " ^ !stamp |
|
118 |
| _ => "\nNew theories: " ^ space_implode ", " (map ! stamps) |
|
119 |
end; |
|
120 |
||
1928 | 121 |
(*Default action is to print an error message; could be suppressed for |
122 |
special applications.*) |
|
3669
3384c6f1f095
removed print_goals_ref (which was broken anyway);
wenzelm
parents:
3536
diff
changeset
|
123 |
fun result_error_default state msg : thm = |
3384c6f1f095
removed print_goals_ref (which was broken anyway);
wenzelm
parents:
3536
diff
changeset
|
124 |
(writeln "Bad final proof state:"; |
3384c6f1f095
removed print_goals_ref (which was broken anyway);
wenzelm
parents:
3536
diff
changeset
|
125 |
print_goals (!goals_limit) state; |
3384c6f1f095
removed print_goals_ref (which was broken anyway);
wenzelm
parents:
3536
diff
changeset
|
126 |
writeln msg; raise ERROR); |
1928 | 127 |
|
3532 | 128 |
val result_error_fn = ref result_error_default; |
1928 | 129 |
|
0 | 130 |
(*Common treatment of "goal" and "prove_goal": |
131 |
Return assumptions, initial proof state, and function to make result. *) |
|
132 |
fun prepare_proof rths chorn = |
|
230 | 133 |
let val {sign, t=horn,...} = rep_cterm chorn; |
0 | 134 |
val (_,As,B) = Logic.strip_horn(horn); |
230 | 135 |
val cAs = map (cterm_of sign) As; |
1413 | 136 |
val prems = map (rewrite_rule rths o forall_elim_vars(0) o assume) cAs |
137 |
and st0 = (rewrite_goals_rule rths o trivial) (cterm_of sign B) |
|
0 | 138 |
(*discharges assumptions from state in the order they appear in goal; |
1460 | 139 |
checks (if requested) that resulting theorem is equivalent to goal. *) |
0 | 140 |
fun mkresult (check,state) = |
696
eb5b42442b14
Pure/goals/prepare_proof/mkresult: now smashes flexflex pairs in the final
lcp
parents:
678
diff
changeset
|
141 |
let val state = Sequence.hd (flexflex_rule state) |
1565 | 142 |
handle THM _ => state (*smash flexflex pairs*) |
1460 | 143 |
val ngoals = nprems_of state |
1219 | 144 |
val th = strip_shyps (implies_intr_list cAs state) |
1240 | 145 |
val {hyps,prop,sign=sign',...} = rep_thm th |
146 |
val xshyps = extra_shyps th; |
|
2169
31ba286f2307
Removed "standard" call from uresult, to allow specialist applications
paulson
parents:
2126
diff
changeset
|
147 |
in if not check then th |
3532 | 148 |
else if not (Sign.eq_sg(sign,sign')) then !result_error_fn state |
1460 | 149 |
("Signature of proof state has changed!" ^ |
150 |
sign_error (sign,sign')) |
|
3532 | 151 |
else if ngoals>0 then !result_error_fn state |
1460 | 152 |
(string_of_int ngoals ^ " unsolved goals!") |
3532 | 153 |
else if not (null hyps) then !result_error_fn state |
0 | 154 |
("Additional hypotheses:\n" ^ |
155 |
cat_lines (map (Sign.string_of_term sign) hyps)) |
|
3532 | 156 |
else if not (null xshyps) then !result_error_fn state |
1240 | 157 |
("Extra sort hypotheses: " ^ |
2962 | 158 |
commas (map Sorts.str_of_sort xshyps)) |
1460 | 159 |
else if Pattern.matches (#tsig(Sign.rep_sg sign)) |
160 |
(term_of chorn, prop) |
|
161 |
then standard th |
|
3532 | 162 |
else !result_error_fn state "proved a different theorem" |
0 | 163 |
end |
678
6151b7f3b606
Modified pattern.ML to perform proper matching of Higher-Order Patterns.
nipkow
parents:
577
diff
changeset
|
164 |
in |
6151b7f3b606
Modified pattern.ML to perform proper matching of Higher-Order Patterns.
nipkow
parents:
577
diff
changeset
|
165 |
if Sign.eq_sg(sign, #sign(rep_thm st0)) |
0 | 166 |
then (prems, st0, mkresult) |
167 |
else error ("Definitions would change the proof state's signature" ^ |
|
1460 | 168 |
sign_error (sign, #sign(rep_thm st0))) |
0 | 169 |
end |
170 |
handle THM(s,_,_) => error("prepare_proof: exception THM was raised!\n" ^ s); |
|
171 |
||
172 |
(*Prints exceptions readably to users*) |
|
577 | 173 |
fun print_sign_exn_unit sign e = |
0 | 174 |
case e of |
175 |
THM (msg,i,thms) => |
|
1460 | 176 |
(writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg); |
177 |
seq print_thm thms) |
|
0 | 178 |
| THEORY (msg,thys) => |
1460 | 179 |
(writeln ("Exception THEORY raised:\n" ^ msg); |
180 |
seq print_theory thys) |
|
0 | 181 |
| TERM (msg,ts) => |
1460 | 182 |
(writeln ("Exception TERM raised:\n" ^ msg); |
183 |
seq (writeln o Sign.string_of_term sign) ts) |
|
0 | 184 |
| TYPE (msg,Ts,ts) => |
1460 | 185 |
(writeln ("Exception TYPE raised:\n" ^ msg); |
186 |
seq (writeln o Sign.string_of_typ sign) Ts; |
|
187 |
seq (writeln o Sign.string_of_term sign) ts) |
|
0 | 188 |
| e => raise e; |
189 |
||
577 | 190 |
(*Prints an exception, then fails*) |
191 |
fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise ERROR); |
|
192 |
||
0 | 193 |
(** the prove_goal.... commands |
194 |
Prove theorem using the listed tactics; check it has the specified form. |
|
195 |
Augment signature with all type assignments of goal. |
|
196 |
Syntax is similar to "goal" command for easy keyboard use. **) |
|
197 |
||
198 |
(*Version taking the goal as a cterm*) |
|
199 |
fun prove_goalw_cterm rths chorn tacsf = |
|
200 |
let val (prems, st0, mkresult) = prepare_proof rths chorn |
|
201 |
val tac = EVERY (tacsf prems) |
|
202 |
fun statef() = |
|
1500 | 203 |
(case Sequence.pull (tac st0) of |
1460 | 204 |
Some(st,_) => st |
205 |
| _ => error ("prove_goal: tactic failed")) |
|
545
fc4ff96bb0e9
Pure/goals.ML: prove_goalw_cterm now does its own exception-handling, moved
lcp
parents:
253
diff
changeset
|
206 |
in mkresult (true, cond_timeit (!proof_timing) statef) end |
914
cae574c09137
Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest
lcp
parents:
696
diff
changeset
|
207 |
handle e => (print_sign_exn_unit (#sign (rep_cterm chorn)) e; |
1460 | 208 |
error ("The exception above was raised for\n" ^ |
209 |
string_of_cterm chorn)); |
|
545
fc4ff96bb0e9
Pure/goals.ML: prove_goalw_cterm now does its own exception-handling, moved
lcp
parents:
253
diff
changeset
|
210 |
|
0 | 211 |
|
212 |
(*Version taking the goal as a string*) |
|
213 |
fun prove_goalw thy rths agoal tacsf = |
|
214 |
let val sign = sign_of thy |
|
230 | 215 |
val chorn = read_cterm sign (agoal,propT) |
545
fc4ff96bb0e9
Pure/goals.ML: prove_goalw_cterm now does its own exception-handling, moved
lcp
parents:
253
diff
changeset
|
216 |
in prove_goalw_cterm rths chorn tacsf end |
fc4ff96bb0e9
Pure/goals.ML: prove_goalw_cterm now does its own exception-handling, moved
lcp
parents:
253
diff
changeset
|
217 |
handle ERROR => error (*from read_cterm?*) |
3536 | 218 |
("The error(s) above occurred for " ^ quote agoal); |
0 | 219 |
|
220 |
(*String version with no meta-rewrite-rules*) |
|
221 |
fun prove_goal thy = prove_goalw thy []; |
|
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 |
||
3532 | 236 |
(*Print goals of current level*) |
237 |
fun print_current_goals_default n max th = |
|
3669
3384c6f1f095
removed print_goals_ref (which was broken anyway);
wenzelm
parents:
3536
diff
changeset
|
238 |
(writeln ("Level " ^ string_of_int n); print_goals max th); |
3532 | 239 |
|
240 |
val print_current_goals_fn = ref print_current_goals_default; |
|
241 |
||
0 | 242 |
(*Print a level of the goal stack.*) |
3532 | 243 |
fun print_top ((th, _), pairs) = |
244 |
!print_current_goals_fn (length pairs) (!goals_limit) th; |
|
0 | 245 |
|
246 |
(*Printing can raise exceptions, so the assignment occurs last. |
|
247 |
Can do setstate[(st,Sequence.null)] to set st as the state. *) |
|
248 |
fun setstate newgoals = |
|
249 |
(print_top (pop newgoals); undo_list := newgoals :: !undo_list); |
|
250 |
||
251 |
(*Given a proof state transformation, return a command that updates |
|
252 |
the goal stack*) |
|
253 |
fun make_command com = setstate (com (pop (getstate()))); |
|
254 |
||
255 |
(*Apply a function on proof states to the current goal stack*) |
|
256 |
fun apply_fun f = f (pop(getstate())); |
|
257 |
||
258 |
(*Return the top theorem, representing the proof state*) |
|
259 |
fun topthm () = apply_fun (fn ((th,_), _) => th); |
|
260 |
||
261 |
(*Return the final result. *) |
|
262 |
fun result () = !curr_mkresult (true, topthm()); |
|
263 |
||
264 |
(*Return the result UNCHECKED that it equals the goal -- for synthesis, |
|
265 |
answer extraction, or other instantiation of Vars *) |
|
266 |
fun uresult () = !curr_mkresult (false, topthm()); |
|
267 |
||
268 |
(*Get subgoal i from goal stack*) |
|
2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2514
diff
changeset
|
269 |
fun getgoal i = List.nth (prems_of (topthm()), i-1) |
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2514
diff
changeset
|
270 |
handle Subscript => error"getgoal: Goal number out of range"; |
0 | 271 |
|
272 |
(*Return subgoal i's hypotheses as meta-level assumptions. |
|
273 |
For debugging uses of METAHYPS*) |
|
274 |
local exception GETHYPS of thm list |
|
275 |
in |
|
276 |
fun gethyps i = |
|
1500 | 277 |
(METAHYPS (fn hyps => raise (GETHYPS hyps)) i (topthm()); []) |
0 | 278 |
handle GETHYPS hyps => hyps |
279 |
end; |
|
280 |
||
281 |
(*Which thms could apply to goal i? (debugs tactics involving filter_thms) *) |
|
282 |
fun filter_goal could ths i = filter_thms could (999, getgoal i, ths); |
|
283 |
||
284 |
(*For inspecting earlier levels of the backward proof*) |
|
285 |
fun chop_level n (pair,pairs) = |
|
286 |
let val level = length pairs |
|
2126
d927beecedf8
Allowing negative levels (as offsets) in prlev and choplev
paulson
parents:
1928
diff
changeset
|
287 |
in if n<0 andalso ~n <= level |
2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2514
diff
changeset
|
288 |
then List.drop (pair::pairs, ~n) |
2126
d927beecedf8
Allowing negative levels (as offsets) in prlev and choplev
paulson
parents:
1928
diff
changeset
|
289 |
else if 0<=n andalso n<= level |
2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2514
diff
changeset
|
290 |
then List.drop (pair::pairs, level - n) |
0 | 291 |
else error ("Level number must lie between 0 and " ^ |
1460 | 292 |
string_of_int level) |
0 | 293 |
end; |
294 |
||
2514 | 295 |
(*Print the given level of the proof; prlev ~1 prints previous level*) |
0 | 296 |
fun prlev n = apply_fun (print_top o pop o (chop_level n)); |
297 |
fun pr () = apply_fun print_top; |
|
298 |
||
2514 | 299 |
(*Set goals_limit and print again*) |
300 |
fun prlim n = (goals_limit:=n; pr()); |
|
301 |
||
0 | 302 |
(** the goal.... commands |
303 |
Read main goal. Set global variables curr_prems, curr_mkresult. |
|
304 |
Initial subgoal and premises are rewritten using rths. **) |
|
305 |
||
306 |
(*Version taking the goal as a cterm; if you have a term t and theory thy, use |
|
230 | 307 |
goalw_cterm rths (cterm_of (sign_of thy) t); *) |
0 | 308 |
fun goalw_cterm rths chorn = |
309 |
let val (prems, st0, mkresult) = prepare_proof rths chorn |
|
310 |
in undo_list := []; |
|
311 |
setstate [ (st0, Sequence.null) ]; |
|
312 |
curr_prems := prems; |
|
313 |
curr_mkresult := mkresult; |
|
314 |
prems |
|
315 |
end; |
|
316 |
||
317 |
(*Version taking the goal as a string*) |
|
318 |
fun goalw thy rths agoal = |
|
230 | 319 |
goalw_cterm rths (read_cterm(sign_of thy)(agoal,propT)) |
0 | 320 |
handle ERROR => error (*from type_assign, etc via prepare_proof*) |
3536 | 321 |
("The error(s) above occurred for " ^ quote agoal); |
0 | 322 |
|
323 |
(*String version with no meta-rewrite-rules*) |
|
324 |
fun goal thy = goalw thy []; |
|
325 |
||
326 |
(*Proof step "by" the given tactic -- apply tactic to the proof state*) |
|
327 |
fun by_com tac ((th,ths), pairs) : gstack = |
|
1500 | 328 |
(case Sequence.pull(tac th) of |
0 | 329 |
None => error"by: tactic failed" |
330 |
| Some(th2,ths2) => |
|
331 |
(if eq_thm(th,th2) |
|
3707
40856b593501
Prints warnings using the "warning" function instead of "writeln"
paulson
parents:
3669
diff
changeset
|
332 |
then warning "Warning: same as previous level" |
1460 | 333 |
else if eq_thm_sg(th,th2) then () |
3532 | 334 |
else writeln ("Warning: signature of proof state has changed" ^ |
1460 | 335 |
sign_error (#sign(rep_thm th), #sign(rep_thm th2))); |
0 | 336 |
((th2,ths2)::(th,ths)::pairs))); |
337 |
||
338 |
fun by tac = cond_timeit (!proof_timing) |
|
339 |
(fn() => make_command (by_com tac)); |
|
340 |
||
341 |
(* byev[tac1,...,tacn] applies tac1 THEN ... THEN tacn. |
|
342 |
Good for debugging proofs involving prove_goal.*) |
|
343 |
val byev = by o EVERY; |
|
344 |
||
345 |
||
346 |
(*Backtracking means find an alternative result from a tactic. |
|
347 |
If none at this level, try earlier levels*) |
|
348 |
fun backtrack [] = error"back: no alternatives" |
|
349 |
| backtrack ((th,thstr) :: pairs) = |
|
350 |
(case Sequence.pull thstr of |
|
1460 | 351 |
None => (writeln"Going back a level..."; backtrack pairs) |
352 |
| Some(th2,thstr2) => |
|
353 |
(if eq_thm(th,th2) |
|
3707
40856b593501
Prints warnings using the "warning" function instead of "writeln"
paulson
parents:
3669
diff
changeset
|
354 |
then warning "Warning: same as previous choice at this level" |
1460 | 355 |
else if eq_thm_sg(th,th2) then () |
3707
40856b593501
Prints warnings using the "warning" function instead of "writeln"
paulson
parents:
3669
diff
changeset
|
356 |
else warning "Warning: signature of proof state has changed"; |
1460 | 357 |
(th2,thstr2)::pairs)); |
0 | 358 |
|
359 |
fun back() = setstate (backtrack (getstate())); |
|
360 |
||
361 |
(*Chop back to previous level of the proof*) |
|
362 |
fun choplev n = make_command (chop_level n); |
|
363 |
||
364 |
(*Chopping back the goal stack*) |
|
365 |
fun chop () = make_command (fn (_,pairs) => pairs); |
|
366 |
||
367 |
(*Restore the previous proof state; discard current state. *) |
|
368 |
fun undo() = case !undo_list of |
|
369 |
[] => error"No proof state" |
|
370 |
| [_] => error"Already at initial state" |
|
371 |
| _::newundo => (undo_list := newundo; pr()) ; |
|
372 |
||
373 |
||
374 |
(*** Managing the proof stack ***) |
|
375 |
||
376 |
fun save_proof() = Proof(!undo_list, !curr_prems, !curr_mkresult); |
|
377 |
||
378 |
fun restore_proof(Proof(ul,prems,mk)) = |
|
379 |
(undo_list:= ul; curr_prems:= prems; curr_mkresult := mk; prems); |
|
380 |
||
381 |
||
382 |
fun top_proof() = case !proofstack of |
|
1460 | 383 |
[] => error("Stack of proof attempts is empty!") |
0 | 384 |
| p::ps => (p,ps); |
385 |
||
386 |
(* push a copy of the current proof state on to the stack *) |
|
387 |
fun push_proof() = (proofstack := (save_proof() :: !proofstack)); |
|
388 |
||
389 |
(* discard the top proof state of the stack *) |
|
390 |
fun pop_proof() = |
|
391 |
let val (p,ps) = top_proof() |
|
392 |
val prems = restore_proof p |
|
393 |
in proofstack := ps; pr(); prems end; |
|
394 |
||
395 |
(* rotate the stack so that the top element goes to the bottom *) |
|
396 |
fun rotate_proof() = let val (p,ps) = top_proof() |
|
1460 | 397 |
in proofstack := ps@[save_proof()]; |
398 |
restore_proof p; |
|
399 |
pr(); |
|
400 |
!curr_prems |
|
401 |
end; |
|
0 | 402 |
|
403 |
||
404 |
(** Shortcuts for commonly-used tactics **) |
|
405 |
||
406 |
fun bws rls = by (rewrite_goals_tac rls); |
|
407 |
fun bw rl = bws [rl]; |
|
408 |
||
409 |
fun brs rls i = by (resolve_tac rls i); |
|
410 |
fun br rl = brs [rl]; |
|
411 |
||
412 |
fun bes rls i = by (eresolve_tac rls i); |
|
413 |
fun be rl = bes [rl]; |
|
414 |
||
415 |
fun bds rls i = by (dresolve_tac rls i); |
|
416 |
fun bd rl = bds [rl]; |
|
417 |
||
418 |
fun ba i = by (assume_tac i); |
|
419 |
||
420 |
fun ren str i = by (rename_tac str i); |
|
421 |
||
422 |
(** Shortcuts to work on the first applicable subgoal **) |
|
423 |
||
424 |
fun frs rls = by (FIRSTGOAL (trace_goalno_tac (resolve_tac rls))); |
|
425 |
fun fr rl = frs [rl]; |
|
426 |
||
427 |
fun fes rls = by (FIRSTGOAL (trace_goalno_tac (eresolve_tac rls))); |
|
428 |
fun fe rl = fes [rl]; |
|
429 |
||
430 |
fun fds rls = by (FIRSTGOAL (trace_goalno_tac (dresolve_tac rls))); |
|
431 |
fun fd rl = fds [rl]; |
|
432 |
||
433 |
fun fa() = by (FIRSTGOAL (trace_goalno_tac assume_tac)); |
|
434 |
||
435 |
(** Reading and printing terms wrt the current theory **) |
|
436 |
||
437 |
fun top_sg() = #sign(rep_thm(topthm())); |
|
438 |
||
230 | 439 |
fun read s = term_of (read_cterm (top_sg()) |
1460 | 440 |
(s, (TVar(("DUMMY",0),[])))); |
0 | 441 |
|
442 |
(*Print a term under the current signature of the proof state*) |
|
443 |
fun prin t = writeln (Sign.string_of_term (top_sg()) t); |
|
444 |
||
445 |
fun printyp T = writeln (Sign.string_of_typ (top_sg()) T); |
|
446 |
||
447 |
fun pprint_term t = Sign.pprint_term (top_sg()) t; |
|
448 |
||
449 |
fun pprint_typ T = Sign.pprint_typ (top_sg()) T; |
|
450 |
||
1628
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
451 |
(* Redirect output of function f:unit->unit to LaTeX *) |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
452 |
fun redirect_to_latex f = |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
453 |
let |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
454 |
val s = ref "" |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
455 |
val old_prs_fn = !prs_fn |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
456 |
in |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
457 |
(prs_fn := (fn a => s := !s ^ a); |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
458 |
f (); |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
459 |
latex (!s); |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
460 |
prs_fn := old_prs_fn) |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
461 |
end; |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
462 |
|
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
463 |
(* Display current proof state in xdvi window *) |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
464 |
fun pr_latex () = redirect_to_latex pr; |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
465 |
|
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
466 |
(* Display goal n of current proof state in xdvi window *) |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
467 |
fun printgoal_latex n = redirect_to_latex (fn () => prin(getgoal n)); |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
468 |
|
0 | 469 |
(*Prints exceptions nicely at top level; |
470 |
raises the exception in order to have a polymorphic type!*) |
|
914
cae574c09137
Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest
lcp
parents:
696
diff
changeset
|
471 |
fun print_exn e = (print_sign_exn_unit (top_sg()) e; raise e); |
0 | 472 |
|
473 |
end; |
|
1500 | 474 |
|
475 |
open Goals; |