author | wenzelm |
Mon, 16 Nov 1998 11:32:28 +0100 | |
changeset 5893 | c755dfd02509 |
parent 5775 | cbd439ed350d |
child 5955 | 6727d29d164f |
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 |
signature GOALS = |
|
13 |
sig |
|
14 |
type proof |
|
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
15 |
val atomic_goal : theory -> string -> thm list |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
16 |
val atomic_goalw : theory -> thm list -> string -> thm list |
1460 | 17 |
val ba : int -> unit |
18 |
val back : unit -> unit |
|
19 |
val bd : thm -> int -> unit |
|
20 |
val bds : thm list -> int -> unit |
|
21 |
val be : thm -> int -> unit |
|
22 |
val bes : thm list -> int -> unit |
|
23 |
val br : thm -> int -> unit |
|
24 |
val brs : thm list -> int -> unit |
|
25 |
val bw : thm -> unit |
|
26 |
val bws : thm list -> unit |
|
27 |
val by : tactic -> unit |
|
28 |
val byev : tactic list -> unit |
|
29 |
val chop : unit -> unit |
|
30 |
val choplev : int -> unit |
|
5246 | 31 |
val export : thm -> thm |
1460 | 32 |
val fa : unit -> unit |
33 |
val fd : thm -> unit |
|
34 |
val fds : thm list -> unit |
|
35 |
val fe : thm -> unit |
|
36 |
val fes : thm list -> unit |
|
37 |
val filter_goal : (term*term->bool) -> thm list -> int -> thm list |
|
38 |
val fr : thm -> unit |
|
39 |
val frs : thm list -> unit |
|
40 |
val getgoal : int -> term |
|
41 |
val gethyps : int -> thm list |
|
42 |
val goal : theory -> string -> thm list |
|
43 |
val goalw : theory -> thm list -> string -> thm list |
|
44 |
val goalw_cterm : thm list -> cterm -> thm list |
|
5729
5d66410cceae
support current_goals_markers ref variable for print_current_goals;
wenzelm
parents:
5614
diff
changeset
|
45 |
val current_goals_markers: (string * string * string) ref |
5246 | 46 |
val print_current_goals_default: (int -> int -> thm -> unit) |
3532 | 47 |
val print_current_goals_fn : (int -> int -> thm -> unit) ref |
1460 | 48 |
val pop_proof : unit -> thm list |
49 |
val pr : unit -> unit |
|
2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2514
diff
changeset
|
50 |
val prlev : int -> unit |
2514 | 51 |
val prlim : int -> unit |
1628
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
52 |
val pr_latex : unit -> unit |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
53 |
val printgoal_latex : int -> unit |
1460 | 54 |
val premises : unit -> thm list |
55 |
val prin : term -> unit |
|
56 |
val printyp : typ -> unit |
|
57 |
val pprint_term : term -> pprint_args -> unit |
|
58 |
val pprint_typ : typ -> pprint_args -> unit |
|
59 |
val print_exn : exn -> 'a |
|
60 |
val print_sign_exn : Sign.sg -> exn -> 'a |
|
61 |
val proof_timing : bool ref |
|
62 |
val prove_goal : theory -> string -> (thm list -> tactic list) -> thm |
|
577 | 63 |
val prove_goalw : theory->thm list->string->(thm list->tactic list)->thm |
1460 | 64 |
val prove_goalw_cterm : thm list->cterm->(thm list->tactic list)->thm |
5311
f3f71669878e
Rule mk_triv_goal for making instances of triv_goal
paulson
parents:
5246
diff
changeset
|
65 |
val prove_goalw_cterm_nocheck : thm list->cterm->(thm list->tactic list)->thm |
1460 | 66 |
val push_proof : unit -> unit |
67 |
val read : string -> term |
|
68 |
val ren : string -> int -> unit |
|
69 |
val restore_proof : proof -> thm list |
|
70 |
val result : unit -> thm |
|
3532 | 71 |
val result_error_fn : (thm -> string -> thm) ref |
1460 | 72 |
val rotate_proof : unit -> thm list |
73 |
val uresult : unit -> thm |
|
74 |
val save_proof : unit -> proof |
|
75 |
val topthm : unit -> thm |
|
76 |
val undo : unit -> unit |
|
0 | 77 |
end; |
78 |
||
1500 | 79 |
structure Goals : GOALS = |
0 | 80 |
struct |
81 |
||
82 |
(*Each level of goal stack includes a proof state and alternative states, |
|
83 |
the output of the tactic applied to the preceeding level. *) |
|
4270 | 84 |
type gstack = (thm * thm Seq.seq) list; |
0 | 85 |
|
86 |
datatype proof = Proof of gstack list * thm list * (bool*thm->thm); |
|
87 |
||
5246 | 88 |
|
0 | 89 |
(*** References ***) |
90 |
||
91 |
(*Should process time be printed after proof steps?*) |
|
92 |
val proof_timing = ref false; |
|
93 |
||
94 |
(*Current assumption list -- set by "goal".*) |
|
95 |
val curr_prems = ref([] : thm list); |
|
96 |
||
97 |
(*Return assumption list -- useful if you didn't save "goal"'s result. *) |
|
98 |
fun premises() = !curr_prems; |
|
99 |
||
100 |
(*Current result maker -- set by "goal", used by "result". *) |
|
101 |
val curr_mkresult = |
|
102 |
ref((fn _=> error"No goal has been supplied in subgoal module") |
|
103 |
: bool*thm->thm); |
|
104 |
||
5092 | 105 |
val dummy = trivial(read_cterm (sign_of ProtoPure.thy) |
0 | 106 |
("PROP No_goal_has_been_supplied",propT)); |
107 |
||
108 |
(*List of previous goal stacks, for the undo operation. Set by setstate. |
|
109 |
A list of lists!*) |
|
4270 | 110 |
val undo_list = ref([[(dummy, Seq.empty)]] : gstack list); |
0 | 111 |
|
112 |
(* Stack of proof attempts *) |
|
113 |
val proofstack = ref([]: proof list); |
|
114 |
||
115 |
||
116 |
(*** Setting up goal-directed proof ***) |
|
117 |
||
118 |
(*Generates the list of new theories when the proof state's signature changes*) |
|
119 |
fun sign_error (sign,sign') = |
|
3974 | 120 |
let val names = Sign.stamp_names_of sign' \\ Sign.stamp_names_of sign |
121 |
in case names of |
|
122 |
[name] => "\nNew theory: " ^ name |
|
123 |
| _ => "\nNew theories: " ^ space_implode ", " names |
|
0 | 124 |
end; |
125 |
||
1928 | 126 |
(*Default action is to print an error message; could be suppressed for |
127 |
special applications.*) |
|
3669
3384c6f1f095
removed print_goals_ref (which was broken anyway);
wenzelm
parents:
3536
diff
changeset
|
128 |
fun result_error_default state msg : thm = |
3384c6f1f095
removed print_goals_ref (which was broken anyway);
wenzelm
parents:
3536
diff
changeset
|
129 |
(writeln "Bad final proof state:"; |
3384c6f1f095
removed print_goals_ref (which was broken anyway);
wenzelm
parents:
3536
diff
changeset
|
130 |
print_goals (!goals_limit) state; |
3384c6f1f095
removed print_goals_ref (which was broken anyway);
wenzelm
parents:
3536
diff
changeset
|
131 |
writeln msg; raise ERROR); |
1928 | 132 |
|
3532 | 133 |
val result_error_fn = ref result_error_default; |
1928 | 134 |
|
5246 | 135 |
(* alternative to standard: this function does not discharge the hypotheses |
136 |
first. Is used for locales, in the following function prepare_proof *) |
|
137 |
fun varify th = |
|
138 |
let val {maxidx,...} = rep_thm th |
|
139 |
in |
|
140 |
th |> forall_intr_frees |> forall_elim_vars (maxidx + 1) |
|
141 |
|> Thm.strip_shyps |> Thm.implies_intr_shyps |
|
142 |
|> zero_var_indexes |> Thm.varifyT |> Thm.compress |
|
143 |
end; |
|
144 |
||
145 |
(** exporting a theorem out of a locale means turning all meta-hyps into assumptions |
|
146 |
and expand and cancel the locale definitions. It's relatively easy, because |
|
147 |
a definiendum is a locale const, hence Free, hence Var, after standard **) |
|
148 |
val export = standard o Seq.hd o (REPEAT (FIRSTGOAL (rtac reflexive_thm))) o standard; |
|
149 |
||
0 | 150 |
(*Common treatment of "goal" and "prove_goal": |
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
151 |
Return assumptions, initial proof state, and function to make result. |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
152 |
"atomic" indicates if the goal should be wrapped up in the function |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
153 |
"Goal::prop=>prop" to avoid assumptions being returned separately. |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
154 |
*) |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
155 |
fun prepare_proof atomic rths chorn = |
230 | 156 |
let val {sign, t=horn,...} = rep_cterm chorn; |
0 | 157 |
val (_,As,B) = Logic.strip_horn(horn); |
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
158 |
val atoms = atomic andalso |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
159 |
forall (fn t => not(Logic.is_implies t orelse Logic.is_all t)) As; |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
160 |
val (As,B) = if atoms then ([],horn) else (As,B); |
230 | 161 |
val cAs = map (cterm_of sign) As; |
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
162 |
val prems = map (rewrite_rule rths o forall_elim_vars(0) o assume) cAs; |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
163 |
val cB = cterm_of sign B; |
5311
f3f71669878e
Rule mk_triv_goal for making instances of triv_goal
paulson
parents:
5246
diff
changeset
|
164 |
val st0 = let val st = Drule.mk_triv_goal cB |
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
165 |
in rewrite_goals_rule rths st end |
0 | 166 |
(*discharges assumptions from state in the order they appear in goal; |
1460 | 167 |
checks (if requested) that resulting theorem is equivalent to goal. *) |
0 | 168 |
fun mkresult (check,state) = |
4270 | 169 |
let val state = Seq.hd (flexflex_rule state) |
1565 | 170 |
handle THM _ => state (*smash flexflex pairs*) |
1460 | 171 |
val ngoals = nprems_of state |
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
172 |
val ath = strip_shyps (implies_intr_list cAs state) |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
173 |
val th = ath RS Drule.rev_triv_goal |
1240 | 174 |
val {hyps,prop,sign=sign',...} = rep_thm th |
175 |
val xshyps = extra_shyps th; |
|
2169
31ba286f2307
Removed "standard" call from uresult, to allow specialist applications
paulson
parents:
2126
diff
changeset
|
176 |
in if not check then th |
3532 | 177 |
else if not (Sign.eq_sg(sign,sign')) then !result_error_fn state |
1460 | 178 |
("Signature of proof state has changed!" ^ |
179 |
sign_error (sign,sign')) |
|
3532 | 180 |
else if ngoals>0 then !result_error_fn state |
1460 | 181 |
(string_of_int ngoals ^ " unsolved goals!") |
5246 | 182 |
else if (not (null hyps) andalso (not (Locale.in_locale hyps sign))) |
183 |
then !result_error_fn state |
|
5748
5a571d57183f
better reporting of "Additional hypotheses" in a locale
paulson
parents:
5729
diff
changeset
|
184 |
("Additional hypotheses:\n" ^ |
5a571d57183f
better reporting of "Additional hypotheses" in a locale
paulson
parents:
5729
diff
changeset
|
185 |
cat_lines |
5a571d57183f
better reporting of "Additional hypotheses" in a locale
paulson
parents:
5729
diff
changeset
|
186 |
(map (Sign.string_of_term sign) |
5a571d57183f
better reporting of "Additional hypotheses" in a locale
paulson
parents:
5729
diff
changeset
|
187 |
(filter (fn x => (not (Locale.in_locale [x] sign))) |
5a571d57183f
better reporting of "Additional hypotheses" in a locale
paulson
parents:
5729
diff
changeset
|
188 |
hyps))) |
3532 | 189 |
else if not (null xshyps) then !result_error_fn state |
1240 | 190 |
("Extra sort hypotheses: " ^ |
3853 | 191 |
commas (map (Sign.str_of_sort sign) xshyps)) |
1460 | 192 |
else if Pattern.matches (#tsig(Sign.rep_sg sign)) |
193 |
(term_of chorn, prop) |
|
5246 | 194 |
then (if (null(hyps)) then standard th |
195 |
else varify th) |
|
3532 | 196 |
else !result_error_fn state "proved a different theorem" |
0 | 197 |
end |
678
6151b7f3b606
Modified pattern.ML to perform proper matching of Higher-Order Patterns.
nipkow
parents:
577
diff
changeset
|
198 |
in |
6151b7f3b606
Modified pattern.ML to perform proper matching of Higher-Order Patterns.
nipkow
parents:
577
diff
changeset
|
199 |
if Sign.eq_sg(sign, #sign(rep_thm st0)) |
0 | 200 |
then (prems, st0, mkresult) |
201 |
else error ("Definitions would change the proof state's signature" ^ |
|
1460 | 202 |
sign_error (sign, #sign(rep_thm st0))) |
0 | 203 |
end |
204 |
handle THM(s,_,_) => error("prepare_proof: exception THM was raised!\n" ^ s); |
|
205 |
||
206 |
(*Prints exceptions readably to users*) |
|
577 | 207 |
fun print_sign_exn_unit sign e = |
0 | 208 |
case e of |
209 |
THM (msg,i,thms) => |
|
1460 | 210 |
(writeln ("Exception THM " ^ string_of_int i ^ " raised:\n" ^ msg); |
211 |
seq print_thm thms) |
|
0 | 212 |
| THEORY (msg,thys) => |
1460 | 213 |
(writeln ("Exception THEORY raised:\n" ^ msg); |
4994 | 214 |
seq (Pretty.writeln o Display.pretty_theory) thys) |
0 | 215 |
| TERM (msg,ts) => |
1460 | 216 |
(writeln ("Exception TERM raised:\n" ^ msg); |
217 |
seq (writeln o Sign.string_of_term sign) ts) |
|
0 | 218 |
| TYPE (msg,Ts,ts) => |
1460 | 219 |
(writeln ("Exception TYPE raised:\n" ^ msg); |
220 |
seq (writeln o Sign.string_of_typ sign) Ts; |
|
221 |
seq (writeln o Sign.string_of_term sign) ts) |
|
0 | 222 |
| e => raise e; |
223 |
||
577 | 224 |
(*Prints an exception, then fails*) |
225 |
fun print_sign_exn sign e = (print_sign_exn_unit sign e; raise ERROR); |
|
226 |
||
0 | 227 |
(** the prove_goal.... commands |
228 |
Prove theorem using the listed tactics; check it has the specified form. |
|
229 |
Augment signature with all type assignments of goal. |
|
230 |
Syntax is similar to "goal" command for easy keyboard use. **) |
|
231 |
||
232 |
(*Version taking the goal as a cterm*) |
|
5311
f3f71669878e
Rule mk_triv_goal for making instances of triv_goal
paulson
parents:
5246
diff
changeset
|
233 |
fun prove_goalw_cterm_general check rths chorn tacsf = |
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
234 |
let val (prems, st0, mkresult) = prepare_proof false rths chorn |
0 | 235 |
val tac = EVERY (tacsf prems) |
236 |
fun statef() = |
|
4270 | 237 |
(case Seq.pull (tac st0) of |
1460 | 238 |
Some(st,_) => st |
239 |
| _ => error ("prove_goal: tactic failed")) |
|
5311
f3f71669878e
Rule mk_triv_goal for making instances of triv_goal
paulson
parents:
5246
diff
changeset
|
240 |
in mkresult (check, 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
|
241 |
handle e => (print_sign_exn_unit (#sign (rep_cterm chorn)) e; |
1460 | 242 |
error ("The exception above was raised for\n" ^ |
243 |
string_of_cterm chorn)); |
|
545
fc4ff96bb0e9
Pure/goals.ML: prove_goalw_cterm now does its own exception-handling, moved
lcp
parents:
253
diff
changeset
|
244 |
|
5614
0e8b45a7d104
Now prove_goalw_cterm never prints timing statistics
paulson
parents:
5311
diff
changeset
|
245 |
(*Two variants: one checking the result, one not. |
0e8b45a7d104
Now prove_goalw_cterm never prints timing statistics
paulson
parents:
5311
diff
changeset
|
246 |
Neither prints runtime messages: they are for internal packages.*) |
0e8b45a7d104
Now prove_goalw_cterm never prints timing statistics
paulson
parents:
5311
diff
changeset
|
247 |
fun prove_goalw_cterm rths chorn = |
0e8b45a7d104
Now prove_goalw_cterm never prints timing statistics
paulson
parents:
5311
diff
changeset
|
248 |
setmp proof_timing false (prove_goalw_cterm_general true rths chorn) |
0e8b45a7d104
Now prove_goalw_cterm never prints timing statistics
paulson
parents:
5311
diff
changeset
|
249 |
and prove_goalw_cterm_nocheck rths chorn = |
0e8b45a7d104
Now prove_goalw_cterm never prints timing statistics
paulson
parents:
5311
diff
changeset
|
250 |
setmp proof_timing false (prove_goalw_cterm_general false rths chorn); |
5311
f3f71669878e
Rule mk_triv_goal for making instances of triv_goal
paulson
parents:
5246
diff
changeset
|
251 |
|
0 | 252 |
|
253 |
(*Version taking the goal as a string*) |
|
254 |
fun prove_goalw thy rths agoal tacsf = |
|
255 |
let val sign = sign_of thy |
|
230 | 256 |
val chorn = read_cterm sign (agoal,propT) |
5614
0e8b45a7d104
Now prove_goalw_cterm never prints timing statistics
paulson
parents:
5311
diff
changeset
|
257 |
in prove_goalw_cterm_general true rths chorn tacsf end |
545
fc4ff96bb0e9
Pure/goals.ML: prove_goalw_cterm now does its own exception-handling, moved
lcp
parents:
253
diff
changeset
|
258 |
handle ERROR => error (*from read_cterm?*) |
3536 | 259 |
("The error(s) above occurred for " ^ quote agoal); |
0 | 260 |
|
261 |
(*String version with no meta-rewrite-rules*) |
|
262 |
fun prove_goal thy = prove_goalw thy []; |
|
263 |
||
264 |
||
265 |
(*** Commands etc ***) |
|
266 |
||
267 |
(*Return the current goal stack, if any, from undo_list*) |
|
268 |
fun getstate() : gstack = case !undo_list of |
|
269 |
[] => error"No current state in subgoal module" |
|
270 |
| x::_ => x; |
|
271 |
||
272 |
(*Pops the given goal stack*) |
|
273 |
fun pop [] = error"Cannot go back past the beginning of the proof!" |
|
274 |
| pop (pair::pairs) = (pair,pairs); |
|
275 |
||
276 |
||
3532 | 277 |
(*Print goals of current level*) |
5729
5d66410cceae
support current_goals_markers ref variable for print_current_goals;
wenzelm
parents:
5614
diff
changeset
|
278 |
val current_goals_markers = ref ("", "", ""); |
5d66410cceae
support current_goals_markers ref variable for print_current_goals;
wenzelm
parents:
5614
diff
changeset
|
279 |
|
3532 | 280 |
fun print_current_goals_default n max th = |
5729
5d66410cceae
support current_goals_markers ref variable for print_current_goals;
wenzelm
parents:
5614
diff
changeset
|
281 |
let val ref (begin_state, end_state, begin_goal) = current_goals_markers in |
5775
cbd439ed350d
tuned current_goals_markers semantics to avoid empty lines;
wenzelm
parents:
5748
diff
changeset
|
282 |
if begin_state = "" then () else writeln begin_state; |
5729
5d66410cceae
support current_goals_markers ref variable for print_current_goals;
wenzelm
parents:
5614
diff
changeset
|
283 |
writeln ("Level " ^ string_of_int n); |
5d66410cceae
support current_goals_markers ref variable for print_current_goals;
wenzelm
parents:
5614
diff
changeset
|
284 |
Locale.print_goals_marker begin_goal max th; |
5775
cbd439ed350d
tuned current_goals_markers semantics to avoid empty lines;
wenzelm
parents:
5748
diff
changeset
|
285 |
if end_state = "" then () else writeln end_state |
5729
5d66410cceae
support current_goals_markers ref variable for print_current_goals;
wenzelm
parents:
5614
diff
changeset
|
286 |
end; |
3532 | 287 |
|
288 |
val print_current_goals_fn = ref print_current_goals_default; |
|
289 |
||
0 | 290 |
(*Print a level of the goal stack.*) |
3532 | 291 |
fun print_top ((th, _), pairs) = |
292 |
!print_current_goals_fn (length pairs) (!goals_limit) th; |
|
0 | 293 |
|
294 |
(*Printing can raise exceptions, so the assignment occurs last. |
|
4270 | 295 |
Can do setstate[(st,Seq.empty)] to set st as the state. *) |
0 | 296 |
fun setstate newgoals = |
297 |
(print_top (pop newgoals); undo_list := newgoals :: !undo_list); |
|
298 |
||
299 |
(*Given a proof state transformation, return a command that updates |
|
300 |
the goal stack*) |
|
301 |
fun make_command com = setstate (com (pop (getstate()))); |
|
302 |
||
303 |
(*Apply a function on proof states to the current goal stack*) |
|
304 |
fun apply_fun f = f (pop(getstate())); |
|
305 |
||
306 |
(*Return the top theorem, representing the proof state*) |
|
307 |
fun topthm () = apply_fun (fn ((th,_), _) => th); |
|
308 |
||
309 |
(*Return the final result. *) |
|
310 |
fun result () = !curr_mkresult (true, topthm()); |
|
311 |
||
312 |
(*Return the result UNCHECKED that it equals the goal -- for synthesis, |
|
313 |
answer extraction, or other instantiation of Vars *) |
|
314 |
fun uresult () = !curr_mkresult (false, topthm()); |
|
315 |
||
316 |
(*Get subgoal i from goal stack*) |
|
2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2514
diff
changeset
|
317 |
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
|
318 |
handle Subscript => error"getgoal: Goal number out of range"; |
0 | 319 |
|
320 |
(*Return subgoal i's hypotheses as meta-level assumptions. |
|
321 |
For debugging uses of METAHYPS*) |
|
322 |
local exception GETHYPS of thm list |
|
323 |
in |
|
324 |
fun gethyps i = |
|
1500 | 325 |
(METAHYPS (fn hyps => raise (GETHYPS hyps)) i (topthm()); []) |
0 | 326 |
handle GETHYPS hyps => hyps |
327 |
end; |
|
328 |
||
329 |
(*Which thms could apply to goal i? (debugs tactics involving filter_thms) *) |
|
330 |
fun filter_goal could ths i = filter_thms could (999, getgoal i, ths); |
|
331 |
||
332 |
(*For inspecting earlier levels of the backward proof*) |
|
333 |
fun chop_level n (pair,pairs) = |
|
334 |
let val level = length pairs |
|
2126
d927beecedf8
Allowing negative levels (as offsets) in prlev and choplev
paulson
parents:
1928
diff
changeset
|
335 |
in if n<0 andalso ~n <= level |
2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2514
diff
changeset
|
336 |
then List.drop (pair::pairs, ~n) |
2126
d927beecedf8
Allowing negative levels (as offsets) in prlev and choplev
paulson
parents:
1928
diff
changeset
|
337 |
else if 0<=n andalso n<= level |
2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2514
diff
changeset
|
338 |
then List.drop (pair::pairs, level - n) |
0 | 339 |
else error ("Level number must lie between 0 and " ^ |
1460 | 340 |
string_of_int level) |
0 | 341 |
end; |
342 |
||
2514 | 343 |
(*Print the given level of the proof; prlev ~1 prints previous level*) |
0 | 344 |
fun prlev n = apply_fun (print_top o pop o (chop_level n)); |
345 |
fun pr () = apply_fun print_top; |
|
346 |
||
2514 | 347 |
(*Set goals_limit and print again*) |
348 |
fun prlim n = (goals_limit:=n; pr()); |
|
349 |
||
0 | 350 |
(** the goal.... commands |
351 |
Read main goal. Set global variables curr_prems, curr_mkresult. |
|
352 |
Initial subgoal and premises are rewritten using rths. **) |
|
353 |
||
354 |
(*Version taking the goal as a cterm; if you have a term t and theory thy, use |
|
230 | 355 |
goalw_cterm rths (cterm_of (sign_of thy) t); *) |
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
356 |
fun agoalw_cterm atomic rths chorn = |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
357 |
let val (prems, st0, mkresult) = prepare_proof atomic rths chorn |
0 | 358 |
in undo_list := []; |
4270 | 359 |
setstate [ (st0, Seq.empty) ]; |
0 | 360 |
curr_prems := prems; |
361 |
curr_mkresult := mkresult; |
|
362 |
prems |
|
363 |
end; |
|
364 |
||
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
365 |
val goalw_cterm = agoalw_cterm false; |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
366 |
|
0 | 367 |
(*Version taking the goal as a string*) |
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
368 |
fun agoalw atomic thy rths agoal = |
5246 | 369 |
agoalw_cterm atomic rths (Locale.read_cterm(sign_of thy)(agoal,propT)) |
370 |
handle ERROR => error (*from type_assign, etc via prepare_proof*) |
|
371 |
("The error(s) above occurred for " ^ quote agoal); |
|
0 | 372 |
|
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
373 |
val goalw = agoalw false; |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
374 |
|
0 | 375 |
(*String version with no meta-rewrite-rules*) |
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
376 |
fun agoal atomic thy = agoalw atomic thy []; |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
377 |
val goal = agoal false; |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
378 |
|
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
379 |
(*now the versions that wrap the goal up in `Goal' to make it atomic*) |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
380 |
|
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
381 |
val atomic_goalw = agoalw true; |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
382 |
val atomic_goal = agoal true; |
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4994
diff
changeset
|
383 |
|
0 | 384 |
|
385 |
(*Proof step "by" the given tactic -- apply tactic to the proof state*) |
|
386 |
fun by_com tac ((th,ths), pairs) : gstack = |
|
4270 | 387 |
(case Seq.pull(tac th) of |
0 | 388 |
None => error"by: tactic failed" |
389 |
| Some(th2,ths2) => |
|
390 |
(if eq_thm(th,th2) |
|
3707
40856b593501
Prints warnings using the "warning" function instead of "writeln"
paulson
parents:
3669
diff
changeset
|
391 |
then warning "Warning: same as previous level" |
1460 | 392 |
else if eq_thm_sg(th,th2) then () |
4280 | 393 |
else warning ("Warning: signature of proof state has changed" ^ |
1460 | 394 |
sign_error (#sign(rep_thm th), #sign(rep_thm th2))); |
0 | 395 |
((th2,ths2)::(th,ths)::pairs))); |
396 |
||
397 |
fun by tac = cond_timeit (!proof_timing) |
|
398 |
(fn() => make_command (by_com tac)); |
|
399 |
||
400 |
(* byev[tac1,...,tacn] applies tac1 THEN ... THEN tacn. |
|
401 |
Good for debugging proofs involving prove_goal.*) |
|
402 |
val byev = by o EVERY; |
|
403 |
||
404 |
||
405 |
(*Backtracking means find an alternative result from a tactic. |
|
406 |
If none at this level, try earlier levels*) |
|
407 |
fun backtrack [] = error"back: no alternatives" |
|
408 |
| backtrack ((th,thstr) :: pairs) = |
|
4270 | 409 |
(case Seq.pull thstr of |
1460 | 410 |
None => (writeln"Going back a level..."; backtrack pairs) |
411 |
| Some(th2,thstr2) => |
|
412 |
(if eq_thm(th,th2) |
|
3707
40856b593501
Prints warnings using the "warning" function instead of "writeln"
paulson
parents:
3669
diff
changeset
|
413 |
then warning "Warning: same as previous choice at this level" |
1460 | 414 |
else if eq_thm_sg(th,th2) then () |
3707
40856b593501
Prints warnings using the "warning" function instead of "writeln"
paulson
parents:
3669
diff
changeset
|
415 |
else warning "Warning: signature of proof state has changed"; |
1460 | 416 |
(th2,thstr2)::pairs)); |
0 | 417 |
|
418 |
fun back() = setstate (backtrack (getstate())); |
|
419 |
||
420 |
(*Chop back to previous level of the proof*) |
|
421 |
fun choplev n = make_command (chop_level n); |
|
422 |
||
423 |
(*Chopping back the goal stack*) |
|
424 |
fun chop () = make_command (fn (_,pairs) => pairs); |
|
425 |
||
426 |
(*Restore the previous proof state; discard current state. *) |
|
427 |
fun undo() = case !undo_list of |
|
428 |
[] => error"No proof state" |
|
429 |
| [_] => error"Already at initial state" |
|
430 |
| _::newundo => (undo_list := newundo; pr()) ; |
|
431 |
||
432 |
||
433 |
(*** Managing the proof stack ***) |
|
434 |
||
435 |
fun save_proof() = Proof(!undo_list, !curr_prems, !curr_mkresult); |
|
436 |
||
437 |
fun restore_proof(Proof(ul,prems,mk)) = |
|
438 |
(undo_list:= ul; curr_prems:= prems; curr_mkresult := mk; prems); |
|
439 |
||
440 |
||
441 |
fun top_proof() = case !proofstack of |
|
1460 | 442 |
[] => error("Stack of proof attempts is empty!") |
0 | 443 |
| p::ps => (p,ps); |
444 |
||
445 |
(* push a copy of the current proof state on to the stack *) |
|
446 |
fun push_proof() = (proofstack := (save_proof() :: !proofstack)); |
|
447 |
||
448 |
(* discard the top proof state of the stack *) |
|
449 |
fun pop_proof() = |
|
450 |
let val (p,ps) = top_proof() |
|
451 |
val prems = restore_proof p |
|
452 |
in proofstack := ps; pr(); prems end; |
|
453 |
||
454 |
(* rotate the stack so that the top element goes to the bottom *) |
|
455 |
fun rotate_proof() = let val (p,ps) = top_proof() |
|
1460 | 456 |
in proofstack := ps@[save_proof()]; |
457 |
restore_proof p; |
|
458 |
pr(); |
|
459 |
!curr_prems |
|
460 |
end; |
|
0 | 461 |
|
462 |
||
463 |
(** Shortcuts for commonly-used tactics **) |
|
464 |
||
465 |
fun bws rls = by (rewrite_goals_tac rls); |
|
466 |
fun bw rl = bws [rl]; |
|
467 |
||
468 |
fun brs rls i = by (resolve_tac rls i); |
|
469 |
fun br rl = brs [rl]; |
|
470 |
||
471 |
fun bes rls i = by (eresolve_tac rls i); |
|
472 |
fun be rl = bes [rl]; |
|
473 |
||
474 |
fun bds rls i = by (dresolve_tac rls i); |
|
475 |
fun bd rl = bds [rl]; |
|
476 |
||
477 |
fun ba i = by (assume_tac i); |
|
478 |
||
479 |
fun ren str i = by (rename_tac str i); |
|
480 |
||
481 |
(** Shortcuts to work on the first applicable subgoal **) |
|
482 |
||
483 |
fun frs rls = by (FIRSTGOAL (trace_goalno_tac (resolve_tac rls))); |
|
484 |
fun fr rl = frs [rl]; |
|
485 |
||
486 |
fun fes rls = by (FIRSTGOAL (trace_goalno_tac (eresolve_tac rls))); |
|
487 |
fun fe rl = fes [rl]; |
|
488 |
||
489 |
fun fds rls = by (FIRSTGOAL (trace_goalno_tac (dresolve_tac rls))); |
|
490 |
fun fd rl = fds [rl]; |
|
491 |
||
492 |
fun fa() = by (FIRSTGOAL (trace_goalno_tac assume_tac)); |
|
493 |
||
494 |
(** Reading and printing terms wrt the current theory **) |
|
495 |
||
496 |
fun top_sg() = #sign(rep_thm(topthm())); |
|
497 |
||
230 | 498 |
fun read s = term_of (read_cterm (top_sg()) |
1460 | 499 |
(s, (TVar(("DUMMY",0),[])))); |
0 | 500 |
|
501 |
(*Print a term under the current signature of the proof state*) |
|
502 |
fun prin t = writeln (Sign.string_of_term (top_sg()) t); |
|
503 |
||
504 |
fun printyp T = writeln (Sign.string_of_typ (top_sg()) T); |
|
505 |
||
506 |
fun pprint_term t = Sign.pprint_term (top_sg()) t; |
|
507 |
||
508 |
fun pprint_typ T = Sign.pprint_typ (top_sg()) T; |
|
509 |
||
4211 | 510 |
(* FIXME !? *) |
511 |
(* output to LaTeX / xdvi *) |
|
512 |
fun latex s = |
|
513 |
execute ("( cd /tmp ; echo \"" ^ s ^ |
|
514 |
"\" | isa2latex -s > $$.tex ; latex $$.tex ; xdvi $$.dvi ; rm $$.* ) > /dev/null &"); |
|
515 |
||
1628
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
516 |
(* Redirect output of function f:unit->unit to LaTeX *) |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
517 |
fun redirect_to_latex f = |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
518 |
let |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
519 |
val s = ref "" |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
520 |
val old_prs_fn = !prs_fn |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
521 |
in |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
522 |
(prs_fn := (fn a => s := !s ^ a); |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
523 |
f (); |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
524 |
latex (!s); |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
525 |
prs_fn := old_prs_fn) |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
526 |
end; |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
527 |
|
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
528 |
(* Display current proof state in xdvi window *) |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
529 |
fun pr_latex () = redirect_to_latex pr; |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
530 |
|
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
531 |
(* Display goal n of current proof state in xdvi window *) |
60136fdd80c4
Added functions pr_latex and printgoal_latex which
berghofe
parents:
1580
diff
changeset
|
532 |
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
|
533 |
|
0 | 534 |
(*Prints exceptions nicely at top level; |
535 |
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
|
536 |
fun print_exn e = (print_sign_exn_unit (top_sg()) e; raise e); |
0 | 537 |
|
538 |
end; |
|
1500 | 539 |
|
5246 | 540 |
|
541 |
||
1500 | 542 |
open Goals; |