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