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