104
|
1 |
%% $Id$
|
|
2 |
\chapter{Proof Management: The Subgoal Module}
|
|
3 |
\index{proofs|(}
|
|
4 |
\index{subgoal module|(}
|
|
5 |
\index{reading!goals|see{proofs, starting}}
|
321
|
6 |
|
|
7 |
The subgoal module stores the current proof state\index{proof state} and
|
|
8 |
many previous states; commands can produce new states or return to previous
|
|
9 |
ones. The {\em state list\/} at level $n$ is a list of pairs
|
104
|
10 |
\[ [(\psi@n,\Psi@n),\; (\psi@{n-1},\Psi@{n-1}),\; \ldots,\; (\psi@0,[])] \]
|
|
11 |
where $\psi@n$ is the current proof state, $\psi@{n-1}$ is the previous
|
|
12 |
one, \ldots, and $\psi@0$ is the initial proof state. The $\Psi@i$ are
|
|
13 |
sequences (lazy lists) of proof states, storing branch points where a
|
|
14 |
tactic returned a list longer than one. The state lists permit various
|
|
15 |
forms of backtracking.
|
|
16 |
|
|
17 |
Chopping elements from the state list reverts to previous proof states.
|
|
18 |
Besides this, the \ttindex{undo} command keeps a list of state lists. The
|
|
19 |
module actually maintains a stack of state lists, to support several
|
|
20 |
proofs at the same time.
|
|
21 |
|
|
22 |
The subgoal module always contains some proof state. At the start of the
|
|
23 |
Isabelle session, this state consists of a dummy formula.
|
|
24 |
|
|
25 |
|
|
26 |
\section{Basic commands}
|
|
27 |
Most proofs begin with {\tt goal} or {\tt goalw} and require no other
|
|
28 |
commands than {\tt by}, {\tt chop} and {\tt undo}. They typically end with
|
|
29 |
a call to {\tt result}.
|
|
30 |
\subsection{Starting a backward proof}
|
321
|
31 |
\index{proofs!starting}
|
104
|
32 |
\begin{ttbox}
|
|
33 |
goal : theory -> string -> thm list
|
|
34 |
goalw : theory -> thm list -> string -> thm list
|
|
35 |
goalw_cterm : thm list -> Sign.cterm -> thm list
|
|
36 |
premises : unit -> thm list
|
|
37 |
\end{ttbox}
|
|
38 |
The {\tt goal} commands start a new proof by setting the goal. They
|
|
39 |
replace the current state list by a new one consisting of the initial proof
|
|
40 |
state. They also empty the \ttindex{undo} list; this command cannot be
|
|
41 |
undone!
|
|
42 |
|
|
43 |
They all return a list of meta-hypotheses taken from the main goal. If
|
|
44 |
this list is non-empty, bind its value to an \ML{} identifier by typing
|
|
45 |
something like
|
|
46 |
\begin{ttbox}
|
332
|
47 |
val prems = goal{\it theory\/ formula};
|
321
|
48 |
\end{ttbox}\index{assumptions!of main goal}
|
104
|
49 |
These assumptions serve as the premises when you are deriving a rule. They
|
|
50 |
are also stored internally and can be retrieved later by the function {\tt
|
321
|
51 |
premises}. When the proof is finished, {\tt result} compares the
|
104
|
52 |
stored assumptions with the actual assumptions in the proof state.
|
|
53 |
|
321
|
54 |
\index{definitions!unfolding}
|
104
|
55 |
Some of the commands unfold definitions using meta-rewrite rules. This
|
332
|
56 |
expansion affects both the initial subgoal and the premises, which would
|
321
|
57 |
otherwise require use of {\tt rewrite_goals_tac} and
|
|
58 |
{\tt rewrite_rule}.
|
104
|
59 |
|
321
|
60 |
\index{*"!"! symbol!in main goal}
|
|
61 |
If the main goal has the form {\tt"!!{\it vars}.\ \ldots"}, with an
|
|
62 |
outermost quantifier, then the list of premises will be empty. Subgoal~1
|
|
63 |
will contain the meta-quantified {\it vars\/} as parameters and the goal's
|
|
64 |
premises as assumptions. This avoids having to call
|
|
65 |
\ttindex{cut_facts_tac} with the list of premises (\S\ref{cut_facts_tac}).
|
104
|
66 |
|
321
|
67 |
\begin{ttdescription}
|
|
68 |
\item[\ttindexbold{goal} {\it theory} {\it formula};]
|
104
|
69 |
begins a new proof, where {\it theory} is usually an \ML\ identifier
|
|
70 |
and the {\it formula\/} is written as an \ML\ string.
|
|
71 |
|
321
|
72 |
\item[\ttindexbold{goalw} {\it theory} {\it defs} {\it formula};]
|
104
|
73 |
is like {\tt goal} but also applies the list of {\it defs\/} as
|
|
74 |
meta-rewrite rules to the first subgoal and the premises.
|
321
|
75 |
\index{meta-rewriting}
|
104
|
76 |
|
321
|
77 |
\item[\ttindexbold{goalw_cterm} {\it theory} {\it defs} {\it ct};]
|
|
78 |
is a version of {\tt goalw} for programming applications. The main goal is
|
104
|
79 |
supplied as a cterm, not as a string. Typically, the cterm is created from
|
|
80 |
a term~$t$ by \hbox{\tt Sign.cterm_of (sign_of thy) $t$}.
|
|
81 |
\index{*Sign.cterm_of}\index{*sign_of}
|
|
82 |
|
|
83 |
\item[\ttindexbold{premises}()]
|
321
|
84 |
returns the list of meta-hypotheses associated with the current proof (in
|
|
85 |
case you forgot to bind them to an \ML{} identifier).
|
|
86 |
\end{ttdescription}
|
|
87 |
|
104
|
88 |
|
|
89 |
\subsection{Applying a tactic}
|
321
|
90 |
\index{tactics!commands for applying}
|
104
|
91 |
\begin{ttbox}
|
|
92 |
by : tactic -> unit
|
|
93 |
byev : tactic list -> unit
|
|
94 |
\end{ttbox}
|
|
95 |
These commands extend the state list. They apply a tactic to the current
|
|
96 |
proof state. If the tactic succeeds, it returns a non-empty sequence of
|
|
97 |
next states. The head of the sequence becomes the next state, while the
|
|
98 |
tail is retained for backtracking (see~{\tt back}).
|
321
|
99 |
\begin{ttdescription} \item[\ttindexbold{by} {\it tactic};]
|
104
|
100 |
applies the {\it tactic\/} to the proof state.
|
|
101 |
|
321
|
102 |
\item[\ttindexbold{byev} {\it tactics};]
|
104
|
103 |
applies the list of {\it tactics}, one at a time. It is useful for testing
|
|
104 |
calls to {\tt prove_goal}, and abbreviates \hbox{\tt by (EVERY {\it
|
|
105 |
tactics})}.
|
321
|
106 |
\end{ttdescription}
|
104
|
107 |
|
286
|
108 |
\noindent{\it Error indications:}\nobreak
|
104
|
109 |
\begin{itemize}
|
286
|
110 |
\item {\footnotesize\tt "by:\ tactic failed"} means that the tactic
|
|
111 |
returned an empty sequence when applied to the current proof state.
|
|
112 |
\item {\footnotesize\tt "Warning:\ same as previous level"} means that the
|
|
113 |
new proof state is identical to the previous state.
|
|
114 |
\item{\footnotesize\tt "Warning:\ signature of proof state has changed"}
|
|
115 |
means that some rule was applied whose theory is outside the theory of
|
|
116 |
the initial proof state. This could signify a mistake such as expressing
|
|
117 |
the goal in intuitionistic logic and proving it using classical logic.
|
104
|
118 |
\end{itemize}
|
|
119 |
|
|
120 |
\subsection{Extracting the proved theorem}
|
321
|
121 |
\index{theorems!from subgoal module}
|
104
|
122 |
\begin{ttbox}
|
|
123 |
result : unit -> thm
|
|
124 |
uresult : unit -> thm
|
|
125 |
\end{ttbox}
|
321
|
126 |
\begin{ttdescription}
|
|
127 |
\item[\ttindexbold{result}()]\index{assumptions!of main goal}
|
104
|
128 |
returns the final theorem, after converting the free variables to
|
|
129 |
schematics. It discharges the assumptions supplied to the matching
|
321
|
130 |
{\tt goal} command.
|
104
|
131 |
|
|
132 |
It raises an exception unless the proof state passes certain checks. There
|
321
|
133 |
must be no assumptions other than those supplied to {\tt goal}. There
|
104
|
134 |
must be no subgoals. The theorem proved must be a (first-order) instance
|
321
|
135 |
of the original goal, as stated in the {\tt goal} command. This allows
|
104
|
136 |
{\bf answer extraction} --- instantiation of variables --- but no other
|
|
137 |
changes to the main goal. The theorem proved must have the same signature
|
|
138 |
as the initial proof state.
|
|
139 |
|
321
|
140 |
These checks are needed because an Isabelle tactic can return any proof
|
|
141 |
state at all.
|
|
142 |
|
|
143 |
\item[\ttindexbold{uresult}()] is like {\tt result()} but omits the checks.
|
|
144 |
It is needed when the initial goal contains function unknowns, when
|
|
145 |
definitions are unfolded in the main goal (by calling
|
|
146 |
\ttindex{rewrite_tac}),\index{definitions!unfolding} or when
|
|
147 |
\ttindex{assume_ax} has been used.
|
|
148 |
\end{ttdescription}
|
104
|
149 |
|
|
150 |
|
|
151 |
\subsection{Undoing and backtracking}
|
|
152 |
\begin{ttbox}
|
|
153 |
chop : unit -> unit
|
|
154 |
choplev : int -> unit
|
|
155 |
back : unit -> unit
|
|
156 |
undo : unit -> unit
|
|
157 |
\end{ttbox}
|
321
|
158 |
\begin{ttdescription}
|
104
|
159 |
\item[\ttindexbold{chop}();]
|
|
160 |
deletes the top level of the state list, cancelling the last \ttindex{by}
|
|
161 |
command. It provides a limited undo facility, and the {\tt undo} command
|
|
162 |
can cancel it.
|
|
163 |
|
|
164 |
\item[\ttindexbold{choplev} {\it n};]
|
|
165 |
truncates the state list to level~{\it n}.
|
|
166 |
|
|
167 |
\item[\ttindexbold{back}();]
|
|
168 |
searches the state list for a non-empty branch point, starting from the top
|
|
169 |
level. The first one found becomes the current proof state --- the most
|
286
|
170 |
recent alternative branch is taken. This is a form of interactive
|
|
171 |
backtracking.
|
104
|
172 |
|
|
173 |
\item[\ttindexbold{undo}();]
|
|
174 |
cancels the most recent change to the proof state by the commands \ttindex{by},
|
|
175 |
{\tt chop}, {\tt choplev}, and~{\tt back}. It {\bf cannot}
|
|
176 |
cancel {\tt goal} or {\tt undo} itself. It can be repeated to
|
|
177 |
cancel a series of commands.
|
321
|
178 |
\end{ttdescription}
|
286
|
179 |
|
|
180 |
\goodbreak
|
|
181 |
\noindent{\it Error indications for {\tt back}:}\par\nobreak
|
104
|
182 |
\begin{itemize}
|
286
|
183 |
\item{\footnotesize\tt"Warning:\ same as previous choice at this level"}
|
|
184 |
means {\tt back} found a non-empty branch point, but that it contained
|
|
185 |
the same proof state as the current one.
|
|
186 |
\item{\footnotesize\tt "Warning:\ signature of proof state has changed"}
|
|
187 |
means the signature of the alternative proof state differs from that of
|
|
188 |
the current state.
|
|
189 |
\item {\footnotesize\tt "back:\ no alternatives"} means {\tt back} could
|
|
190 |
find no alternative proof state.
|
104
|
191 |
\end{itemize}
|
|
192 |
|
|
193 |
\subsection{Printing the proof state}
|
321
|
194 |
\index{proof state!printing of}
|
104
|
195 |
\begin{ttbox}
|
|
196 |
pr : unit -> unit
|
|
197 |
prlev : int -> unit
|
|
198 |
goals_limit: int ref \hfill{\bf initially 10}
|
|
199 |
\end{ttbox}
|
321
|
200 |
\begin{ttdescription}
|
104
|
201 |
\item[\ttindexbold{pr}();]
|
|
202 |
prints the current proof state.
|
|
203 |
|
|
204 |
\item[\ttindexbold{prlev} {\it n};]
|
|
205 |
prints the proof state at level {\it n}. This allows you to review the
|
|
206 |
previous steps of the proof.
|
|
207 |
|
321
|
208 |
\item[\ttindexbold{goals_limit} := {\it k};]
|
104
|
209 |
specifies~$k$ as the maximum number of subgoals to print.
|
321
|
210 |
\end{ttdescription}
|
104
|
211 |
|
|
212 |
|
|
213 |
\subsection{Timing}
|
321
|
214 |
\index{timing statistics}\index{proofs!timing}
|
104
|
215 |
\begin{ttbox}
|
|
216 |
proof_timing: bool ref \hfill{\bf initially false}
|
|
217 |
\end{ttbox}
|
|
218 |
|
321
|
219 |
\begin{ttdescription}
|
|
220 |
\item[\ttindexbold{proof_timing} := true;]
|
104
|
221 |
makes the \ttindex{by} and \ttindex{prove_goal} commands display how much
|
|
222 |
processor time was spent. This information is compiler-dependent.
|
321
|
223 |
\end{ttdescription}
|
104
|
224 |
|
|
225 |
|
|
226 |
\section{Shortcuts for applying tactics}
|
321
|
227 |
\index{shortcuts!for {\tt by} commands}
|
104
|
228 |
These commands call \ttindex{by} with common tactics. Their chief purpose
|
|
229 |
is to minimise typing, although the scanning shortcuts are useful in their
|
|
230 |
own right. Chapter~\ref{tactics} explains the tactics themselves.
|
|
231 |
|
|
232 |
\subsection{Refining a given subgoal}
|
|
233 |
\begin{ttbox}
|
321
|
234 |
ba : int -> unit
|
|
235 |
br : thm -> int -> unit
|
|
236 |
be : thm -> int -> unit
|
|
237 |
bd : thm -> int -> unit
|
|
238 |
brs : thm list -> int -> unit
|
|
239 |
bes : thm list -> int -> unit
|
|
240 |
bds : thm list -> int -> unit
|
104
|
241 |
\end{ttbox}
|
|
242 |
|
321
|
243 |
\begin{ttdescription}
|
104
|
244 |
\item[\ttindexbold{ba} {\it i};]
|
321
|
245 |
performs \hbox{\tt by (assume_tac {\it i});}
|
104
|
246 |
|
|
247 |
\item[\ttindexbold{br} {\it thm} {\it i};]
|
321
|
248 |
performs \hbox{\tt by (resolve_tac [{\it thm}] {\it i});}
|
104
|
249 |
|
|
250 |
\item[\ttindexbold{be} {\it thm} {\it i};]
|
321
|
251 |
performs \hbox{\tt by (eresolve_tac [{\it thm}] {\it i});}
|
104
|
252 |
|
|
253 |
\item[\ttindexbold{bd} {\it thm} {\it i};]
|
321
|
254 |
performs \hbox{\tt by (dresolve_tac [{\it thm}] {\it i});}
|
104
|
255 |
|
|
256 |
\item[\ttindexbold{brs} {\it thms} {\it i};]
|
321
|
257 |
performs \hbox{\tt by (resolve_tac {\it thms} {\it i});}
|
104
|
258 |
|
|
259 |
\item[\ttindexbold{bes} {\it thms} {\it i};]
|
321
|
260 |
performs \hbox{\tt by (eresolve_tac {\it thms} {\it i});}
|
104
|
261 |
|
|
262 |
\item[\ttindexbold{bds} {\it thms} {\it i};]
|
321
|
263 |
performs \hbox{\tt by (dresolve_tac {\it thms} {\it i});}
|
|
264 |
\end{ttdescription}
|
104
|
265 |
|
|
266 |
|
|
267 |
\subsection{Scanning shortcuts}
|
|
268 |
These shortcuts scan for a suitable subgoal (starting from subgoal~1).
|
|
269 |
They refine the first subgoal for which the tactic succeeds. Thus, they
|
|
270 |
require less typing than {\tt br}, etc. They display the selected
|
|
271 |
subgoal's number; please watch this, for it may not be what you expect!
|
|
272 |
|
|
273 |
\begin{ttbox}
|
321
|
274 |
fa : unit -> unit
|
|
275 |
fr : thm -> unit
|
|
276 |
fe : thm -> unit
|
|
277 |
fd : thm -> unit
|
|
278 |
frs : thm list -> unit
|
|
279 |
fes : thm list -> unit
|
|
280 |
fds : thm list -> unit
|
104
|
281 |
\end{ttbox}
|
|
282 |
|
321
|
283 |
\begin{ttdescription}
|
104
|
284 |
\item[\ttindexbold{fa}();]
|
321
|
285 |
solves some subgoal by assumption.
|
104
|
286 |
|
|
287 |
\item[\ttindexbold{fr} {\it thm};]
|
|
288 |
refines some subgoal using \hbox{\tt resolve_tac [{\it thm}]}
|
|
289 |
|
|
290 |
\item[\ttindexbold{fe} {\it thm};]
|
|
291 |
refines some subgoal using \hbox{\tt eresolve_tac [{\it thm}]}
|
|
292 |
|
|
293 |
\item[\ttindexbold{fd} {\it thm};]
|
|
294 |
refines some subgoal using \hbox{\tt dresolve_tac [{\it thm}]}
|
|
295 |
|
|
296 |
\item[\ttindexbold{frs} {\it thms};]
|
|
297 |
refines some subgoal using \hbox{\tt resolve_tac {\it thms}}
|
|
298 |
|
|
299 |
\item[\ttindexbold{fes} {\it thms};]
|
|
300 |
refines some subgoal using \hbox{\tt eresolve_tac {\it thms}}
|
|
301 |
|
|
302 |
\item[\ttindexbold{fds} {\it thms};]
|
|
303 |
refines some subgoal using \hbox{\tt dresolve_tac {\it thms}}
|
321
|
304 |
\end{ttdescription}
|
104
|
305 |
|
|
306 |
\subsection{Other shortcuts}
|
|
307 |
\begin{ttbox}
|
|
308 |
bw : thm -> unit
|
|
309 |
bws : thm list -> unit
|
|
310 |
ren : string -> int -> unit
|
|
311 |
\end{ttbox}
|
321
|
312 |
\begin{ttdescription}
|
104
|
313 |
\item[\ttindexbold{bw} {\it def};]
|
|
314 |
performs \hbox{\tt by (rewrite_goals_tac [{\it def}]);}
|
|
315 |
It unfolds definitions in the subgoals (but not the main goal), by
|
321
|
316 |
meta-rewriting with the given definition.
|
|
317 |
\index{meta-rewriting}
|
104
|
318 |
|
|
319 |
\item[\ttindexbold{bws}]
|
|
320 |
is like {\tt bw} but takes a list of definitions.
|
|
321 |
|
|
322 |
\item[\ttindexbold{ren} {\it names} {\it i};]
|
|
323 |
performs \hbox{\tt by (rename_tac {\it names} {\it i});} it renames
|
332
|
324 |
parameters in subgoal~$i$. (Ignore the message {\footnotesize\tt Warning:\
|
|
325 |
same as previous level}.)
|
321
|
326 |
\index{parameters!renaming}
|
|
327 |
\end{ttdescription}
|
104
|
328 |
|
|
329 |
|
321
|
330 |
\section{Executing batch proofs}
|
|
331 |
\index{batch execution}
|
286
|
332 |
\begin{ttbox}
|
104
|
333 |
prove_goal : theory-> string->(thm list->tactic list)->thm
|
|
334 |
prove_goalw : theory->thm list->string->(thm list->tactic list)->thm
|
|
335 |
prove_goalw_cterm: thm list->Sign.cterm->(thm list->tactic list)->thm
|
|
336 |
\end{ttbox}
|
321
|
337 |
These batch functions create an initial proof state, then apply a tactic to
|
|
338 |
it, yielding a sequence of final proof states. The head of the sequence is
|
104
|
339 |
returned, provided it is an instance of the theorem originally proposed.
|
|
340 |
The forms {\tt prove_goal}, {\tt prove_goalw} and {\tt prove_goalw_cterm}
|
321
|
341 |
are analogous to {\tt goal}, {\tt goalw} and {\tt goalw_cterm}.
|
104
|
342 |
|
|
343 |
The tactic is specified by a function from theorem lists to tactic lists.
|
332
|
344 |
The function is applied to the list of meta-assumptions taken from
|
|
345 |
the main goal. The resulting tactics are applied in sequence (using {\tt
|
|
346 |
EVERY}). For example, a proof consisting of the commands
|
104
|
347 |
\begin{ttbox}
|
|
348 |
val prems = goal {\it theory} {\it formula};
|
|
349 |
by \(tac@1\); \ldots by \(tac@n\);
|
|
350 |
val my_thm = result();
|
|
351 |
\end{ttbox}
|
|
352 |
can be transformed to an expression as follows:
|
|
353 |
\begin{ttbox}
|
|
354 |
val my_thm = prove_goal {\it theory} {\it formula}
|
|
355 |
(fn prems=> [ \(tac@1\), \ldots, \(tac@n\) ]);
|
|
356 |
\end{ttbox}
|
|
357 |
The methods perform identical processing of the initial {\it formula} and
|
332
|
358 |
the final proof state. But {\tt prove_goal} executes the tactic as a
|
|
359 |
atomic operation, bypassing the subgoal module; the current interactive
|
|
360 |
proof is unaffected.
|
|
361 |
%
|
321
|
362 |
\begin{ttdescription}
|
|
363 |
\item[\ttindexbold{prove_goal} {\it theory} {\it formula} {\it tacsf};]
|
104
|
364 |
executes a proof of the {\it formula\/} in the given {\it theory}, using
|
|
365 |
the given tactic function.
|
|
366 |
|
|
367 |
\item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula}
|
321
|
368 |
{\it tacsf};]\index{meta-rewriting}
|
104
|
369 |
is like {\tt prove_goal} but also applies the list of {\it defs\/} as
|
|
370 |
meta-rewrite rules to the first subgoal and the premises.
|
|
371 |
|
|
372 |
\item[\ttindexbold{prove_goalw_cterm} {\it theory} {\it defs} {\it ct}
|
321
|
373 |
{\it tacsf};]
|
|
374 |
is a version of {\tt prove_goalw} for programming applications. The main
|
104
|
375 |
goal is supplied as a cterm, not as a string. Typically, the cterm is
|
286
|
376 |
created from a term~$t$ as follows:
|
|
377 |
\begin{ttbox}
|
|
378 |
Sign.cterm_of (sign_of thy) \(t\)
|
|
379 |
\end{ttbox}
|
104
|
380 |
\index{*Sign.cterm_of}\index{*sign_of}
|
321
|
381 |
\end{ttdescription}
|
104
|
382 |
|
|
383 |
|
321
|
384 |
\section{Managing multiple proofs}
|
|
385 |
\index{proofs!managing multiple}
|
104
|
386 |
You may save the current state of the subgoal module and resume work on it
|
|
387 |
later. This serves two purposes.
|
|
388 |
\begin{enumerate}
|
|
389 |
\item At some point, you may be uncertain of the next step, and
|
|
390 |
wish to experiment.
|
|
391 |
|
|
392 |
\item During a proof, you may see that a lemma should be proved first.
|
|
393 |
\end{enumerate}
|
|
394 |
Each saved proof state consists of a list of levels; \ttindex{chop} behaves
|
|
395 |
independently for each of the saved proofs. In addition, each saved state
|
|
396 |
carries a separate \ttindex{undo} list.
|
|
397 |
|
321
|
398 |
\subsection{The stack of proof states}
|
|
399 |
\index{proofs!stacking}
|
104
|
400 |
\begin{ttbox}
|
|
401 |
push_proof : unit -> unit
|
|
402 |
pop_proof : unit -> thm list
|
|
403 |
rotate_proof : unit -> thm list
|
|
404 |
\end{ttbox}
|
|
405 |
The subgoal module maintains a stack of proof states. Most subgoal
|
321
|
406 |
commands affect only the top of the stack. The \ttindex{goal} command {\em
|
|
407 |
replaces\/} the top of the stack; the only command that pushes a proof on the
|
104
|
408 |
stack is {\tt push_proof}.
|
|
409 |
|
|
410 |
To save some point of the proof, call {\tt push_proof}. You may now
|
321
|
411 |
state a lemma using {\tt goal}, or simply continue to apply tactics.
|
104
|
412 |
Later, you can return to the saved point by calling {\tt pop_proof} or
|
|
413 |
{\tt rotate_proof}.
|
|
414 |
|
|
415 |
To view the entire stack, call {\tt rotate_proof} repeatedly; as it rotates
|
|
416 |
the stack, it prints the new top element.
|
|
417 |
|
321
|
418 |
\begin{ttdescription}
|
104
|
419 |
\item[\ttindexbold{push_proof}();]
|
|
420 |
duplicates the top element of the stack, pushing a copy of the current
|
|
421 |
proof state on to the stack.
|
|
422 |
|
|
423 |
\item[\ttindexbold{pop_proof}();]
|
|
424 |
discards the top element of the stack. It returns the list of
|
332
|
425 |
assumptions associated with the new proof; you should bind these to an
|
104
|
426 |
\ML\ identifier. They can also be obtained by calling \ttindex{premises}.
|
|
427 |
|
321
|
428 |
\item[\ttindexbold{rotate_proof}();]
|
|
429 |
\index{assumptions!of main goal}
|
104
|
430 |
rotates the stack, moving the top element to the bottom. It returns the
|
|
431 |
list of assumptions associated with the new proof.
|
321
|
432 |
\end{ttdescription}
|
104
|
433 |
|
|
434 |
|
321
|
435 |
\subsection{Saving and restoring proof states}
|
|
436 |
\index{proofs!saving and restoring}
|
104
|
437 |
\begin{ttbox}
|
|
438 |
save_proof : unit -> proof
|
|
439 |
restore_proof : proof -> thm list
|
|
440 |
\end{ttbox}
|
|
441 |
States of the subgoal module may be saved as \ML\ values of
|
321
|
442 |
type~\mltydx{proof}, and later restored.
|
104
|
443 |
|
321
|
444 |
\begin{ttdescription}
|
104
|
445 |
\item[\ttindexbold{save_proof}();]
|
|
446 |
returns the current state, which is on top of the stack.
|
|
447 |
|
321
|
448 |
\item[\ttindexbold{restore_proof} {\it prf};]\index{assumptions!of main goal}
|
|
449 |
replaces the top of the stack by~{\it prf}. It returns the list of
|
|
450 |
assumptions associated with the new proof.
|
|
451 |
\end{ttdescription}
|
104
|
452 |
|
|
453 |
|
321
|
454 |
\section{Debugging and inspecting}
|
|
455 |
\index{tactics!debugging}
|
104
|
456 |
These specialized operations support the debugging of tactics. They refer
|
321
|
457 |
to the current proof state of the subgoal module.
|
104
|
458 |
|
321
|
459 |
\subsection{Reading and printing terms}
|
|
460 |
\index{terms!reading of}\index{terms!printing of}\index{types!printing of}
|
104
|
461 |
\begin{ttbox}
|
|
462 |
read : string -> term
|
|
463 |
prin : term -> unit
|
|
464 |
printyp : typ -> unit
|
|
465 |
\end{ttbox}
|
|
466 |
These read and print terms (or types) using the syntax associated with the
|
|
467 |
proof state.
|
|
468 |
|
321
|
469 |
\begin{ttdescription}
|
104
|
470 |
\item[\ttindexbold{read} {\it string}]
|
|
471 |
reads the {\it string} as a term, without type checking.
|
|
472 |
|
|
473 |
\item[\ttindexbold{prin} {\it t};]
|
|
474 |
prints the term~$t$ at the terminal.
|
|
475 |
|
|
476 |
\item[\ttindexbold{printyp} {\it T};]
|
|
477 |
prints the type~$T$ at the terminal.
|
321
|
478 |
\end{ttdescription}
|
104
|
479 |
|
321
|
480 |
\subsection{Inspecting the proof state}
|
|
481 |
\index{proofs!inspecting the state}
|
104
|
482 |
\begin{ttbox}
|
|
483 |
topthm : unit -> thm
|
|
484 |
getgoal : int -> term
|
|
485 |
gethyps : int -> thm list
|
|
486 |
\end{ttbox}
|
|
487 |
|
321
|
488 |
\begin{ttdescription}
|
104
|
489 |
\item[\ttindexbold{topthm}()]
|
|
490 |
returns the proof state as an Isabelle theorem. This is what \ttindex{by}
|
|
491 |
would supply to a tactic at this point. It omits the post-processing of
|
|
492 |
\ttindex{result} and \ttindex{uresult}.
|
|
493 |
|
|
494 |
\item[\ttindexbold{getgoal} {\it i}]
|
|
495 |
returns subgoal~$i$ of the proof state, as a term. You may print
|
|
496 |
this using {\tt prin}, though you may have to examine the internal
|
|
497 |
data structure in order to locate the problem!
|
|
498 |
|
321
|
499 |
\item[\ttindexbold{gethyps} {\it i}]
|
|
500 |
returns the hypotheses of subgoal~$i$ as meta-level assumptions. In
|
|
501 |
these theorems, the subgoal's parameters become free variables. This
|
|
502 |
command is supplied for debugging uses of \ttindex{METAHYPS}.
|
|
503 |
\end{ttdescription}
|
104
|
504 |
|
321
|
505 |
\subsection{Filtering lists of rules}
|
104
|
506 |
\begin{ttbox}
|
|
507 |
filter_goal: (term*term->bool) -> thm list -> int -> thm list
|
|
508 |
\end{ttbox}
|
|
509 |
|
321
|
510 |
\begin{ttdescription}
|
104
|
511 |
\item[\ttindexbold{filter_goal} {\it could} {\it ths} {\it i}]
|
|
512 |
applies \hbox{\tt filter_thms {\it could}} to subgoal~$i$ of the proof
|
|
513 |
state and returns the list of theorems that survive the filtering.
|
321
|
514 |
\end{ttdescription}
|
104
|
515 |
|
|
516 |
\index{subgoal module|)}
|
|
517 |
\index{proofs|)}
|