author | nipkow |
Fri, 06 Feb 1998 18:55:57 +0100 | |
changeset 4606 | 73227403d497 |
parent 4374 | 245b64afefe2 |
child 5205 | 602354039306 |
permissions | -rw-r--r-- |
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 |
|
3108 | 28 |
commands than {\tt by}, {\tt chop} and {\tt undo}. They typically end |
29 |
with a call to {\tt qed}. |
|
104 | 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 |
|
3108 | 35 |
goalw_cterm : thm list -> cterm -> thm list |
104 | 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} |
3108 | 49 |
These assumptions serve as the premises when you are deriving a rule. |
50 |
They are also stored internally and can be retrieved later by the |
|
51 |
function {\tt premises}. When the proof is finished, {\tt qed} |
|
52 |
compares the stored assumptions with the actual assumptions in the |
|
53 |
proof state. |
|
104 | 54 |
|
321 | 55 |
\index{definitions!unfolding} |
104 | 56 |
Some of the commands unfold definitions using meta-rewrite rules. This |
332 | 57 |
expansion affects both the initial subgoal and the premises, which would |
321 | 58 |
otherwise require use of {\tt rewrite_goals_tac} and |
59 |
{\tt rewrite_rule}. |
|
104 | 60 |
|
321 | 61 |
\index{*"!"! symbol!in main goal} |
62 |
If the main goal has the form {\tt"!!{\it vars}.\ \ldots"}, with an |
|
63 |
outermost quantifier, then the list of premises will be empty. Subgoal~1 |
|
64 |
will contain the meta-quantified {\it vars\/} as parameters and the goal's |
|
65 |
premises as assumptions. This avoids having to call |
|
66 |
\ttindex{cut_facts_tac} with the list of premises (\S\ref{cut_facts_tac}). |
|
104 | 67 |
|
321 | 68 |
\begin{ttdescription} |
69 |
\item[\ttindexbold{goal} {\it theory} {\it formula};] |
|
104 | 70 |
begins a new proof, where {\it theory} is usually an \ML\ identifier |
71 |
and the {\it formula\/} is written as an \ML\ string. |
|
72 |
||
321 | 73 |
\item[\ttindexbold{goalw} {\it theory} {\it defs} {\it formula};] |
104 | 74 |
is like {\tt goal} but also applies the list of {\it defs\/} as |
75 |
meta-rewrite rules to the first subgoal and the premises. |
|
321 | 76 |
\index{meta-rewriting} |
104 | 77 |
|
3108 | 78 |
\item[\ttindexbold{goalw_cterm} {\it theory} {\it defs} {\it ct};] is |
79 |
a version of {\tt goalw} for programming applications. The main |
|
80 |
goal is supplied as a cterm, not as a string. Typically, the cterm |
|
81 |
is created from a term~$t$ by \hbox{\tt cterm_of (sign_of thy) $t$}. |
|
82 |
\index{*cterm_of}\index{*sign_of} |
|
104 | 83 |
|
84 |
\item[\ttindexbold{premises}()] |
|
321 | 85 |
returns the list of meta-hypotheses associated with the current proof (in |
86 |
case you forgot to bind them to an \ML{} identifier). |
|
87 |
\end{ttdescription} |
|
88 |
||
104 | 89 |
|
90 |
\subsection{Applying a tactic} |
|
321 | 91 |
\index{tactics!commands for applying} |
104 | 92 |
\begin{ttbox} |
93 |
by : tactic -> unit |
|
94 |
byev : tactic list -> unit |
|
95 |
\end{ttbox} |
|
96 |
These commands extend the state list. They apply a tactic to the current |
|
97 |
proof state. If the tactic succeeds, it returns a non-empty sequence of |
|
98 |
next states. The head of the sequence becomes the next state, while the |
|
99 |
tail is retained for backtracking (see~{\tt back}). |
|
321 | 100 |
\begin{ttdescription} \item[\ttindexbold{by} {\it tactic};] |
104 | 101 |
applies the {\it tactic\/} to the proof state. |
102 |
||
321 | 103 |
\item[\ttindexbold{byev} {\it tactics};] |
104 | 104 |
applies the list of {\it tactics}, one at a time. It is useful for testing |
105 |
calls to {\tt prove_goal}, and abbreviates \hbox{\tt by (EVERY {\it |
|
106 |
tactics})}. |
|
321 | 107 |
\end{ttdescription} |
104 | 108 |
|
286 | 109 |
\noindent{\it Error indications:}\nobreak |
104 | 110 |
\begin{itemize} |
286 | 111 |
\item {\footnotesize\tt "by:\ tactic failed"} means that the tactic |
112 |
returned an empty sequence when applied to the current proof state. |
|
113 |
\item {\footnotesize\tt "Warning:\ same as previous level"} means that the |
|
114 |
new proof state is identical to the previous state. |
|
115 |
\item{\footnotesize\tt "Warning:\ signature of proof state has changed"} |
|
116 |
means that some rule was applied whose theory is outside the theory of |
|
117 |
the initial proof state. This could signify a mistake such as expressing |
|
118 |
the goal in intuitionistic logic and proving it using classical logic. |
|
104 | 119 |
\end{itemize} |
120 |
||
866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset
|
121 |
\subsection{Extracting and storing the proved theorem} |
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset
|
122 |
\label{ExtractingAndStoringTheProvedTheorem} |
1233
2856f382f033
minor corrections to indexing; added thms_containing
paulson
parents:
1225
diff
changeset
|
123 |
\index{theorems!extracting proved} |
104 | 124 |
\begin{ttbox} |
1283 | 125 |
qed : string -> unit |
866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset
|
126 |
result : unit -> thm |
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset
|
127 |
uresult : unit -> thm |
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset
|
128 |
bind_thm : string * thm -> unit |
1283 | 129 |
store_thm : string * thm -> thm |
104 | 130 |
\end{ttbox} |
321 | 131 |
\begin{ttdescription} |
4317 | 132 |
\item[\ttindexbold{qed} $name$;] is the usual way of ending a proof. |
133 |
It combines {\tt result} and {\tt bind_thm}: it gets the theorem |
|
134 |
using {\tt result()} and stores it the theorem database associated |
|
135 |
with its theory. See below for details. |
|
1283 | 136 |
|
321 | 137 |
\item[\ttindexbold{result}()]\index{assumptions!of main goal} |
866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset
|
138 |
returns the final theorem, after converting the free variables to |
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset
|
139 |
schematics. It discharges the assumptions supplied to the matching |
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset
|
140 |
{\tt goal} command. |
104 | 141 |
|
866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset
|
142 |
It raises an exception unless the proof state passes certain checks. There |
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset
|
143 |
must be no assumptions other than those supplied to {\tt goal}. There |
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset
|
144 |
must be no subgoals. The theorem proved must be a (first-order) instance |
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset
|
145 |
of the original goal, as stated in the {\tt goal} command. This allows |
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset
|
146 |
{\bf answer extraction} --- instantiation of variables --- but no other |
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset
|
147 |
changes to the main goal. The theorem proved must have the same signature |
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset
|
148 |
as the initial proof state. |
104 | 149 |
|
866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset
|
150 |
These checks are needed because an Isabelle tactic can return any proof |
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset
|
151 |
state at all. |
321 | 152 |
|
153 |
\item[\ttindexbold{uresult}()] is like {\tt result()} but omits the checks. |
|
154 |
It is needed when the initial goal contains function unknowns, when |
|
155 |
definitions are unfolded in the main goal (by calling |
|
156 |
\ttindex{rewrite_tac}),\index{definitions!unfolding} or when |
|
157 |
\ttindex{assume_ax} has been used. |
|
4317 | 158 |
|
159 |
\item[\ttindexbold{bind_thm} ($name$, $thm$);]\index{theorems!storing} |
|
4374 | 160 |
stores {\tt standard $thm$} (see \S\ref{MiscellaneousForwardRules}) |
4317 | 161 |
in the theorem database associated with its theory and in the {\ML} |
162 |
variable $name$. The theorem can be retrieved from the database |
|
163 |
using {\tt get_thm} (see \S\ref{BasicOperationsOnTheories}). |
|
164 |
||
165 |
\item[\ttindexbold{store_thm} ($name$, $thm$)]\index{theorems!storing} |
|
166 |
stores $thm$ in the theorem database associated with its theory and |
|
167 |
returns that theorem. |
|
321 | 168 |
\end{ttdescription} |
104 | 169 |
|
170 |
||
1222 | 171 |
\subsection{Retrieving theorems} |
172 |
\index{theorems!retrieving} |
|
173 |
||
4317 | 174 |
The following functions retrieve theorems (together with their names) |
175 |
from the theorem database that is associated with the current proof |
|
176 |
state's theory. They can only find theorems that have explicitly been |
|
177 |
stored in the database using \ttindex{qed}, \ttindex{bind_thm} or |
|
1222 | 178 |
related functions. |
179 |
\begin{ttbox} |
|
4317 | 180 |
findI : int -> (string * thm) list |
181 |
findE : int -> int -> (string * thm) list |
|
182 |
findEs : int -> (string * thm) list |
|
183 |
thms_containing : xstring list -> (string * thm) list |
|
1222 | 184 |
\end{ttbox} |
185 |
\begin{ttdescription} |
|
186 |
\item[\ttindexbold{findI} $i$]\index{assumptions!of main goal} |
|
1225 | 187 |
returns all ``introduction rules'' applicable to subgoal $i$ --- all |
1222 | 188 |
theorems whose conclusion matches (rather than unifies with) subgoal |
1225 | 189 |
$i$. Useful in connection with {\tt resolve_tac}. |
1222 | 190 |
|
191 |
\item[\ttindexbold{findE} $n$ $i$] returns all ``elimination rules'' |
|
1225 | 192 |
applicable to premise $n$ of subgoal $i$ --- all those theorems whose |
193 |
first premise matches premise $n$ of subgoal $i$. Useful in connection with |
|
1222 | 194 |
{\tt eresolve_tac} and {\tt dresolve_tac}. |
195 |
||
196 |
\item[\ttindexbold{findEs} $i$] returns all ``elimination rules'' applicable |
|
1225 | 197 |
to subgoal $i$ --- all those theorems whose first premise matches some |
198 |
premise of subgoal $i$. Useful in connection with {\tt eresolve_tac} and |
|
1222 | 199 |
{\tt dresolve_tac}. |
4317 | 200 |
|
201 |
\item[\ttindexbold{thms_containing} $consts$] returns all theorems |
|
202 |
that contain all of a given set of constants. Note that a few basic |
|
203 |
constants like \verb$==>$ are ignored. |
|
1222 | 204 |
\end{ttdescription} |
205 |
||
206 |
||
104 | 207 |
\subsection{Undoing and backtracking} |
208 |
\begin{ttbox} |
|
209 |
chop : unit -> unit |
|
210 |
choplev : int -> unit |
|
211 |
back : unit -> unit |
|
212 |
undo : unit -> unit |
|
213 |
\end{ttbox} |
|
321 | 214 |
\begin{ttdescription} |
104 | 215 |
\item[\ttindexbold{chop}();] |
216 |
deletes the top level of the state list, cancelling the last \ttindex{by} |
|
217 |
command. It provides a limited undo facility, and the {\tt undo} command |
|
218 |
can cancel it. |
|
219 |
||
220 |
\item[\ttindexbold{choplev} {\it n};] |
|
2128
4e8644805af2
Documents the use of negative arguments to choplev and prlev
paulson
parents:
1283
diff
changeset
|
221 |
truncates the state list to level~{\it n}, if $n\geq0$. A negative value |
4e8644805af2
Documents the use of negative arguments to choplev and prlev
paulson
parents:
1283
diff
changeset
|
222 |
of~$n$ refers to the $n$th previous level: |
4e8644805af2
Documents the use of negative arguments to choplev and prlev
paulson
parents:
1283
diff
changeset
|
223 |
\hbox{\verb|choplev ~1|} has the same effect as {\tt chop}. |
104 | 224 |
|
225 |
\item[\ttindexbold{back}();] |
|
226 |
searches the state list for a non-empty branch point, starting from the top |
|
227 |
level. The first one found becomes the current proof state --- the most |
|
286 | 228 |
recent alternative branch is taken. This is a form of interactive |
229 |
backtracking. |
|
104 | 230 |
|
231 |
\item[\ttindexbold{undo}();] |
|
232 |
cancels the most recent change to the proof state by the commands \ttindex{by}, |
|
233 |
{\tt chop}, {\tt choplev}, and~{\tt back}. It {\bf cannot} |
|
234 |
cancel {\tt goal} or {\tt undo} itself. It can be repeated to |
|
235 |
cancel a series of commands. |
|
321 | 236 |
\end{ttdescription} |
286 | 237 |
|
238 |
\goodbreak |
|
239 |
\noindent{\it Error indications for {\tt back}:}\par\nobreak |
|
104 | 240 |
\begin{itemize} |
286 | 241 |
\item{\footnotesize\tt"Warning:\ same as previous choice at this level"} |
242 |
means {\tt back} found a non-empty branch point, but that it contained |
|
243 |
the same proof state as the current one. |
|
244 |
\item{\footnotesize\tt "Warning:\ signature of proof state has changed"} |
|
245 |
means the signature of the alternative proof state differs from that of |
|
246 |
the current state. |
|
247 |
\item {\footnotesize\tt "back:\ no alternatives"} means {\tt back} could |
|
248 |
find no alternative proof state. |
|
104 | 249 |
\end{itemize} |
250 |
||
507 | 251 |
\subsection{Printing the proof state}\label{sec:goals-printing} |
321 | 252 |
\index{proof state!printing of} |
104 | 253 |
\begin{ttbox} |
254 |
pr : unit -> unit |
|
255 |
prlev : int -> unit |
|
2528 | 256 |
prlim : int -> unit |
104 | 257 |
goals_limit: int ref \hfill{\bf initially 10} |
258 |
\end{ttbox} |
|
2528 | 259 |
See also the printing control options described |
260 |
in~\S\ref{sec:printing-control}. |
|
321 | 261 |
\begin{ttdescription} |
104 | 262 |
\item[\ttindexbold{pr}();] |
263 |
prints the current proof state. |
|
264 |
||
265 |
\item[\ttindexbold{prlev} {\it n};] |
|
2128
4e8644805af2
Documents the use of negative arguments to choplev and prlev
paulson
parents:
1283
diff
changeset
|
266 |
prints the proof state at level {\it n}, if $n\geq0$. A negative value |
4e8644805af2
Documents the use of negative arguments to choplev and prlev
paulson
parents:
1283
diff
changeset
|
267 |
of~$n$ refers to the $n$th previous level. This command allows |
4e8644805af2
Documents the use of negative arguments to choplev and prlev
paulson
parents:
1283
diff
changeset
|
268 |
you to review earlier stages of the proof. |
104 | 269 |
|
2528 | 270 |
\item[\ttindexbold{prlim} {\it k};] |
271 |
prints the current proof state, limiting the number of subgoals to~$k$. It |
|
272 |
updates {\tt goals_limit} (see below) and is helpful when there are many |
|
273 |
subgoals. |
|
274 |
||
321 | 275 |
\item[\ttindexbold{goals_limit} := {\it k};] |
104 | 276 |
specifies~$k$ as the maximum number of subgoals to print. |
321 | 277 |
\end{ttdescription} |
104 | 278 |
|
279 |
||
280 |
\subsection{Timing} |
|
321 | 281 |
\index{timing statistics}\index{proofs!timing} |
104 | 282 |
\begin{ttbox} |
283 |
proof_timing: bool ref \hfill{\bf initially false} |
|
284 |
\end{ttbox} |
|
285 |
||
321 | 286 |
\begin{ttdescription} |
4317 | 287 |
\item[set \ttindexbold{proof_timing};] |
104 | 288 |
makes the \ttindex{by} and \ttindex{prove_goal} commands display how much |
289 |
processor time was spent. This information is compiler-dependent. |
|
321 | 290 |
\end{ttdescription} |
104 | 291 |
|
292 |
||
293 |
\section{Shortcuts for applying tactics} |
|
321 | 294 |
\index{shortcuts!for {\tt by} commands} |
104 | 295 |
These commands call \ttindex{by} with common tactics. Their chief purpose |
296 |
is to minimise typing, although the scanning shortcuts are useful in their |
|
297 |
own right. Chapter~\ref{tactics} explains the tactics themselves. |
|
298 |
||
299 |
\subsection{Refining a given subgoal} |
|
300 |
\begin{ttbox} |
|
321 | 301 |
ba : int -> unit |
302 |
br : thm -> int -> unit |
|
303 |
be : thm -> int -> unit |
|
304 |
bd : thm -> int -> unit |
|
305 |
brs : thm list -> int -> unit |
|
306 |
bes : thm list -> int -> unit |
|
307 |
bds : thm list -> int -> unit |
|
104 | 308 |
\end{ttbox} |
309 |
||
321 | 310 |
\begin{ttdescription} |
104 | 311 |
\item[\ttindexbold{ba} {\it i};] |
321 | 312 |
performs \hbox{\tt by (assume_tac {\it i});} |
104 | 313 |
|
314 |
\item[\ttindexbold{br} {\it thm} {\it i};] |
|
321 | 315 |
performs \hbox{\tt by (resolve_tac [{\it thm}] {\it i});} |
104 | 316 |
|
317 |
\item[\ttindexbold{be} {\it thm} {\it i};] |
|
321 | 318 |
performs \hbox{\tt by (eresolve_tac [{\it thm}] {\it i});} |
104 | 319 |
|
320 |
\item[\ttindexbold{bd} {\it thm} {\it i};] |
|
321 | 321 |
performs \hbox{\tt by (dresolve_tac [{\it thm}] {\it i});} |
104 | 322 |
|
323 |
\item[\ttindexbold{brs} {\it thms} {\it i};] |
|
321 | 324 |
performs \hbox{\tt by (resolve_tac {\it thms} {\it i});} |
104 | 325 |
|
326 |
\item[\ttindexbold{bes} {\it thms} {\it i};] |
|
321 | 327 |
performs \hbox{\tt by (eresolve_tac {\it thms} {\it i});} |
104 | 328 |
|
329 |
\item[\ttindexbold{bds} {\it thms} {\it i};] |
|
321 | 330 |
performs \hbox{\tt by (dresolve_tac {\it thms} {\it i});} |
331 |
\end{ttdescription} |
|
104 | 332 |
|
333 |
||
334 |
\subsection{Scanning shortcuts} |
|
335 |
These shortcuts scan for a suitable subgoal (starting from subgoal~1). |
|
336 |
They refine the first subgoal for which the tactic succeeds. Thus, they |
|
337 |
require less typing than {\tt br}, etc. They display the selected |
|
338 |
subgoal's number; please watch this, for it may not be what you expect! |
|
339 |
||
340 |
\begin{ttbox} |
|
321 | 341 |
fa : unit -> unit |
342 |
fr : thm -> unit |
|
343 |
fe : thm -> unit |
|
344 |
fd : thm -> unit |
|
345 |
frs : thm list -> unit |
|
346 |
fes : thm list -> unit |
|
347 |
fds : thm list -> unit |
|
104 | 348 |
\end{ttbox} |
349 |
||
321 | 350 |
\begin{ttdescription} |
104 | 351 |
\item[\ttindexbold{fa}();] |
321 | 352 |
solves some subgoal by assumption. |
104 | 353 |
|
354 |
\item[\ttindexbold{fr} {\it thm};] |
|
355 |
refines some subgoal using \hbox{\tt resolve_tac [{\it thm}]} |
|
356 |
||
357 |
\item[\ttindexbold{fe} {\it thm};] |
|
358 |
refines some subgoal using \hbox{\tt eresolve_tac [{\it thm}]} |
|
359 |
||
360 |
\item[\ttindexbold{fd} {\it thm};] |
|
361 |
refines some subgoal using \hbox{\tt dresolve_tac [{\it thm}]} |
|
362 |
||
363 |
\item[\ttindexbold{frs} {\it thms};] |
|
364 |
refines some subgoal using \hbox{\tt resolve_tac {\it thms}} |
|
365 |
||
366 |
\item[\ttindexbold{fes} {\it thms};] |
|
367 |
refines some subgoal using \hbox{\tt eresolve_tac {\it thms}} |
|
368 |
||
369 |
\item[\ttindexbold{fds} {\it thms};] |
|
370 |
refines some subgoal using \hbox{\tt dresolve_tac {\it thms}} |
|
321 | 371 |
\end{ttdescription} |
104 | 372 |
|
373 |
\subsection{Other shortcuts} |
|
374 |
\begin{ttbox} |
|
375 |
bw : thm -> unit |
|
376 |
bws : thm list -> unit |
|
377 |
ren : string -> int -> unit |
|
378 |
\end{ttbox} |
|
321 | 379 |
\begin{ttdescription} |
4317 | 380 |
\item[\ttindexbold{bw} {\it def};] performs \hbox{\tt by |
381 |
(rewrite_goals_tac [{\it def}]);} It unfolds definitions in the |
|
382 |
subgoals (but not the main goal), by meta-rewriting with the given |
|
383 |
definition (see also \S\ref{sec:rewrite_goals}). |
|
384 |
\index{meta-rewriting} |
|
104 | 385 |
|
386 |
\item[\ttindexbold{bws}] |
|
387 |
is like {\tt bw} but takes a list of definitions. |
|
388 |
||
389 |
\item[\ttindexbold{ren} {\it names} {\it i};] |
|
390 |
performs \hbox{\tt by (rename_tac {\it names} {\it i});} it renames |
|
332 | 391 |
parameters in subgoal~$i$. (Ignore the message {\footnotesize\tt Warning:\ |
392 |
same as previous level}.) |
|
321 | 393 |
\index{parameters!renaming} |
394 |
\end{ttdescription} |
|
104 | 395 |
|
396 |
||
321 | 397 |
\section{Executing batch proofs} |
3128
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset
|
398 |
\index{batch execution}% |
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset
|
399 |
To save space below, let type \texttt{tacfun} abbreviate \texttt{thm list -> |
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset
|
400 |
tactic list}, which is the type of a tactical proof. |
286 | 401 |
\begin{ttbox} |
3128
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset
|
402 |
prove_goal : theory -> string -> tacfun -> thm |
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset
|
403 |
qed_goal : string -> theory -> string -> tacfun -> unit |
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset
|
404 |
prove_goalw: theory -> thm list -> string -> tacfun -> thm |
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset
|
405 |
qed_goalw : string -> theory -> thm list -> string -> tacfun -> unit |
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset
|
406 |
prove_goalw_cterm: thm list -> cterm -> tacfun -> thm |
104 | 407 |
\end{ttbox} |
321 | 408 |
These batch functions create an initial proof state, then apply a tactic to |
409 |
it, yielding a sequence of final proof states. The head of the sequence is |
|
104 | 410 |
returned, provided it is an instance of the theorem originally proposed. |
411 |
The forms {\tt prove_goal}, {\tt prove_goalw} and {\tt prove_goalw_cterm} |
|
321 | 412 |
are analogous to {\tt goal}, {\tt goalw} and {\tt goalw_cterm}. |
104 | 413 |
|
414 |
The tactic is specified by a function from theorem lists to tactic lists. |
|
332 | 415 |
The function is applied to the list of meta-assumptions taken from |
416 |
the main goal. The resulting tactics are applied in sequence (using {\tt |
|
417 |
EVERY}). For example, a proof consisting of the commands |
|
104 | 418 |
\begin{ttbox} |
419 |
val prems = goal {\it theory} {\it formula}; |
|
420 |
by \(tac@1\); \ldots by \(tac@n\); |
|
3108 | 421 |
qed "my_thm"; |
104 | 422 |
\end{ttbox} |
423 |
can be transformed to an expression as follows: |
|
424 |
\begin{ttbox} |
|
3108 | 425 |
qed_goal "my_thm" {\it theory} {\it formula} |
104 | 426 |
(fn prems=> [ \(tac@1\), \ldots, \(tac@n\) ]); |
427 |
\end{ttbox} |
|
428 |
The methods perform identical processing of the initial {\it formula} and |
|
332 | 429 |
the final proof state. But {\tt prove_goal} executes the tactic as a |
430 |
atomic operation, bypassing the subgoal module; the current interactive |
|
431 |
proof is unaffected. |
|
432 |
% |
|
321 | 433 |
\begin{ttdescription} |
434 |
\item[\ttindexbold{prove_goal} {\it theory} {\it formula} {\it tacsf};] |
|
104 | 435 |
executes a proof of the {\it formula\/} in the given {\it theory}, using |
436 |
the given tactic function. |
|
437 |
||
4317 | 438 |
\item[\ttindexbold{qed_goal} $name$ $theory$ $formula$ $tacsf$;] acts |
439 |
like {\tt prove_goal} but also stores the resulting theorem in the |
|
440 |
theorem database associated with its theory and in the {\ML} |
|
441 |
variable $name$ (see \S\ref{ExtractingAndStoringTheProvedTheorem}). |
|
866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset
|
442 |
|
104 | 443 |
\item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula} |
321 | 444 |
{\it tacsf};]\index{meta-rewriting} |
104 | 445 |
is like {\tt prove_goal} but also applies the list of {\it defs\/} as |
446 |
meta-rewrite rules to the first subgoal and the premises. |
|
447 |
||
866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset
|
448 |
\item[\ttindexbold{qed_goalw} $name$ $theory$ $defs$ $formula$ $tacsf$;] |
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset
|
449 |
is analogous to {\tt qed_goal}. |
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset
|
450 |
|
104 | 451 |
\item[\ttindexbold{prove_goalw_cterm} {\it theory} {\it defs} {\it ct} |
321 | 452 |
{\it tacsf};] |
453 |
is a version of {\tt prove_goalw} for programming applications. The main |
|
104 | 454 |
goal is supplied as a cterm, not as a string. Typically, the cterm is |
286 | 455 |
created from a term~$t$ as follows: |
456 |
\begin{ttbox} |
|
3108 | 457 |
cterm_of (sign_of thy) \(t\) |
286 | 458 |
\end{ttbox} |
3108 | 459 |
\index{*cterm_of}\index{*sign_of} |
321 | 460 |
\end{ttdescription} |
104 | 461 |
|
462 |
||
321 | 463 |
\section{Managing multiple proofs} |
464 |
\index{proofs!managing multiple} |
|
104 | 465 |
You may save the current state of the subgoal module and resume work on it |
466 |
later. This serves two purposes. |
|
467 |
\begin{enumerate} |
|
468 |
\item At some point, you may be uncertain of the next step, and |
|
469 |
wish to experiment. |
|
470 |
||
471 |
\item During a proof, you may see that a lemma should be proved first. |
|
472 |
\end{enumerate} |
|
473 |
Each saved proof state consists of a list of levels; \ttindex{chop} behaves |
|
474 |
independently for each of the saved proofs. In addition, each saved state |
|
475 |
carries a separate \ttindex{undo} list. |
|
476 |
||
321 | 477 |
\subsection{The stack of proof states} |
478 |
\index{proofs!stacking} |
|
104 | 479 |
\begin{ttbox} |
480 |
push_proof : unit -> unit |
|
481 |
pop_proof : unit -> thm list |
|
482 |
rotate_proof : unit -> thm list |
|
483 |
\end{ttbox} |
|
484 |
The subgoal module maintains a stack of proof states. Most subgoal |
|
321 | 485 |
commands affect only the top of the stack. The \ttindex{goal} command {\em |
486 |
replaces\/} the top of the stack; the only command that pushes a proof on the |
|
104 | 487 |
stack is {\tt push_proof}. |
488 |
||
489 |
To save some point of the proof, call {\tt push_proof}. You may now |
|
321 | 490 |
state a lemma using {\tt goal}, or simply continue to apply tactics. |
104 | 491 |
Later, you can return to the saved point by calling {\tt pop_proof} or |
492 |
{\tt rotate_proof}. |
|
493 |
||
494 |
To view the entire stack, call {\tt rotate_proof} repeatedly; as it rotates |
|
495 |
the stack, it prints the new top element. |
|
496 |
||
321 | 497 |
\begin{ttdescription} |
104 | 498 |
\item[\ttindexbold{push_proof}();] |
499 |
duplicates the top element of the stack, pushing a copy of the current |
|
500 |
proof state on to the stack. |
|
501 |
||
502 |
\item[\ttindexbold{pop_proof}();] |
|
503 |
discards the top element of the stack. It returns the list of |
|
332 | 504 |
assumptions associated with the new proof; you should bind these to an |
104 | 505 |
\ML\ identifier. They can also be obtained by calling \ttindex{premises}. |
506 |
||
321 | 507 |
\item[\ttindexbold{rotate_proof}();] |
508 |
\index{assumptions!of main goal} |
|
104 | 509 |
rotates the stack, moving the top element to the bottom. It returns the |
510 |
list of assumptions associated with the new proof. |
|
321 | 511 |
\end{ttdescription} |
104 | 512 |
|
513 |
||
321 | 514 |
\subsection{Saving and restoring proof states} |
515 |
\index{proofs!saving and restoring} |
|
104 | 516 |
\begin{ttbox} |
517 |
save_proof : unit -> proof |
|
518 |
restore_proof : proof -> thm list |
|
519 |
\end{ttbox} |
|
520 |
States of the subgoal module may be saved as \ML\ values of |
|
321 | 521 |
type~\mltydx{proof}, and later restored. |
104 | 522 |
|
321 | 523 |
\begin{ttdescription} |
104 | 524 |
\item[\ttindexbold{save_proof}();] |
525 |
returns the current state, which is on top of the stack. |
|
526 |
||
321 | 527 |
\item[\ttindexbold{restore_proof} {\it prf};]\index{assumptions!of main goal} |
528 |
replaces the top of the stack by~{\it prf}. It returns the list of |
|
529 |
assumptions associated with the new proof. |
|
530 |
\end{ttdescription} |
|
104 | 531 |
|
532 |
||
4317 | 533 |
\section{*Debugging and inspecting} |
321 | 534 |
\index{tactics!debugging} |
2611 | 535 |
These functions can be useful when you are debugging a tactic. They refer |
536 |
to the current proof state stored in the subgoal module. A tactic |
|
537 |
should never call them; it should operate on the proof state supplied as its |
|
538 |
argument. |
|
104 | 539 |
|
321 | 540 |
\subsection{Reading and printing terms} |
541 |
\index{terms!reading of}\index{terms!printing of}\index{types!printing of} |
|
104 | 542 |
\begin{ttbox} |
543 |
read : string -> term |
|
544 |
prin : term -> unit |
|
545 |
printyp : typ -> unit |
|
546 |
\end{ttbox} |
|
547 |
These read and print terms (or types) using the syntax associated with the |
|
548 |
proof state. |
|
549 |
||
321 | 550 |
\begin{ttdescription} |
104 | 551 |
\item[\ttindexbold{read} {\it string}] |
552 |
reads the {\it string} as a term, without type checking. |
|
553 |
||
554 |
\item[\ttindexbold{prin} {\it t};] |
|
555 |
prints the term~$t$ at the terminal. |
|
556 |
||
557 |
\item[\ttindexbold{printyp} {\it T};] |
|
558 |
prints the type~$T$ at the terminal. |
|
321 | 559 |
\end{ttdescription} |
104 | 560 |
|
321 | 561 |
\subsection{Inspecting the proof state} |
562 |
\index{proofs!inspecting the state} |
|
104 | 563 |
\begin{ttbox} |
564 |
topthm : unit -> thm |
|
565 |
getgoal : int -> term |
|
566 |
gethyps : int -> thm list |
|
567 |
\end{ttbox} |
|
568 |
||
321 | 569 |
\begin{ttdescription} |
104 | 570 |
\item[\ttindexbold{topthm}()] |
571 |
returns the proof state as an Isabelle theorem. This is what \ttindex{by} |
|
572 |
would supply to a tactic at this point. It omits the post-processing of |
|
573 |
\ttindex{result} and \ttindex{uresult}. |
|
574 |
||
575 |
\item[\ttindexbold{getgoal} {\it i}] |
|
576 |
returns subgoal~$i$ of the proof state, as a term. You may print |
|
577 |
this using {\tt prin}, though you may have to examine the internal |
|
578 |
data structure in order to locate the problem! |
|
579 |
||
321 | 580 |
\item[\ttindexbold{gethyps} {\it i}] |
581 |
returns the hypotheses of subgoal~$i$ as meta-level assumptions. In |
|
582 |
these theorems, the subgoal's parameters become free variables. This |
|
583 |
command is supplied for debugging uses of \ttindex{METAHYPS}. |
|
584 |
\end{ttdescription} |
|
104 | 585 |
|
2611 | 586 |
|
321 | 587 |
\subsection{Filtering lists of rules} |
104 | 588 |
\begin{ttbox} |
589 |
filter_goal: (term*term->bool) -> thm list -> int -> thm list |
|
590 |
\end{ttbox} |
|
591 |
||
321 | 592 |
\begin{ttdescription} |
104 | 593 |
\item[\ttindexbold{filter_goal} {\it could} {\it ths} {\it i}] |
594 |
applies \hbox{\tt filter_thms {\it could}} to subgoal~$i$ of the proof |
|
595 |
state and returns the list of theorems that survive the filtering. |
|
321 | 596 |
\end{ttdescription} |
104 | 597 |
|
598 |
\index{subgoal module|)} |
|
599 |
\index{proofs|)} |