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