author  paulson 
Tue, 28 Jul 1998 16:33:43 +0200  
changeset 5205  602354039306 
parent 4374  245b64afefe2 
child 5371  e27558a68b8d 
permissions  rwrr 
104  1 
%% $Id$ 
2 
\chapter{Proof Management: The Subgoal Module} 

3 
\index{proofs(} 

4 
\index{subgoal module(} 

5 
\index{reading!goalssee{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@{n1},\Psi@{n1}),\; \ldots,\; (\psi@0,[])] \] 
11 
where $\psi@n$ is the current proof state, $\psi@{n1}$ 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} 

5205  27 
Most proofs begin with \texttt{goal} or \texttt{goalw} and require no other 
28 
commands than \texttt{by}, \texttt{chop} and \texttt{undo}. They typically end 

29 
with a call to \texttt{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} 

5205  38 
The \texttt{goal} commands start a new proof by setting the goal. They 
104  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 metahypotheses taken from the main goal. If 

44 
this list is nonempty, 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 

5205  51 
function \texttt{premises}. When the proof is finished, \texttt{qed} 
3108  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 metarewrite rules. This 
332  57 
expansion affects both the initial subgoal and the premises, which would 
5205  58 
otherwise require use of \texttt{rewrite_goals_tac} and 
59 
\texttt{rewrite_rule}. 

104  60 

321  61 
\begin{ttdescription} 
62 
\item[\ttindexbold{goal} {\it theory} {\it formula};] 

104  63 
begins a new proof, where {\it theory} is usually an \ML\ identifier 
64 
and the {\it formula\/} is written as an \ML\ string. 

65 

321  66 
\item[\ttindexbold{goalw} {\it theory} {\it defs} {\it formula};] 
5205  67 
is like \texttt{goal} but also applies the list of {\it defs\/} as 
104  68 
metarewrite rules to the first subgoal and the premises. 
321  69 
\index{metarewriting} 
104  70 

3108  71 
\item[\ttindexbold{goalw_cterm} {\it theory} {\it defs} {\it ct};] is 
5205  72 
a version of \texttt{goalw} for programming applications. The main 
3108  73 
goal is supplied as a cterm, not as a string. Typically, the cterm 
5205  74 
is created from a term~$t$ by \texttt{cterm_of (sign_of thy) $t$}. 
3108  75 
\index{*cterm_of}\index{*sign_of} 
104  76 

77 
\item[\ttindexbold{premises}()] 

321  78 
returns the list of metahypotheses associated with the current proof (in 
79 
case you forgot to bind them to an \ML{} identifier). 

80 
\end{ttdescription} 

81 

104  82 

83 
\subsection{Applying a tactic} 

321  84 
\index{tactics!commands for applying} 
104  85 
\begin{ttbox} 
86 
by : tactic > unit 

87 
byev : tactic list > unit 

88 
\end{ttbox} 

89 
These commands extend the state list. They apply a tactic to the current 

90 
proof state. If the tactic succeeds, it returns a nonempty sequence of 

91 
next states. The head of the sequence becomes the next state, while the 

5205  92 
tail is retained for backtracking (see~\texttt{back}). 
321  93 
\begin{ttdescription} \item[\ttindexbold{by} {\it tactic};] 
104  94 
applies the {\it tactic\/} to the proof state. 
95 

321  96 
\item[\ttindexbold{byev} {\it tactics};] 
104  97 
applies the list of {\it tactics}, one at a time. It is useful for testing 
5205  98 
calls to \texttt{prove_goal}, and abbreviates \texttt{by (EVERY {\it 
104  99 
tactics})}. 
321  100 
\end{ttdescription} 
104  101 

286  102 
\noindent{\it Error indications:}\nobreak 
104  103 
\begin{itemize} 
286  104 
\item {\footnotesize\tt "by:\ tactic failed"} means that the tactic 
105 
returned an empty sequence when applied to the current proof state. 

106 
\item {\footnotesize\tt "Warning:\ same as previous level"} means that the 

107 
new proof state is identical to the previous state. 

108 
\item{\footnotesize\tt "Warning:\ signature of proof state has changed"} 

109 
means that some rule was applied whose theory is outside the theory of 

110 
the initial proof state. This could signify a mistake such as expressing 

111 
the goal in intuitionistic logic and proving it using classical logic. 

104  112 
\end{itemize} 
113 

866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

114 
\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

115 
\label{ExtractingAndStoringTheProvedTheorem} 
1233
2856f382f033
minor corrections to indexing; added thms_containing
paulson
parents:
1225
diff
changeset

116 
\index{theorems!extracting proved} 
104  117 
\begin{ttbox} 
1283  118 
qed : string > unit 
866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

119 
result : unit > thm 
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

120 
uresult : unit > thm 
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

121 
bind_thm : string * thm > unit 
1283  122 
store_thm : string * thm > thm 
104  123 
\end{ttbox} 
321  124 
\begin{ttdescription} 
4317  125 
\item[\ttindexbold{qed} $name$;] is the usual way of ending a proof. 
5205  126 
It combines \texttt{result} and \texttt{bind_thm}: it gets the theorem 
127 
using \texttt{result()} and stores it the theorem database associated 

4317  128 
with its theory. See below for details. 
1283  129 

321  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 
5205  133 
\texttt{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 
5205  136 
must be no assumptions other than those supplied to \texttt{goal}. There 
866
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 (firstorder) instance 
5205  138 
of the original goal, as stated in the \texttt{goal} command. This allows 
866
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 

5205  146 
\item[\ttindexbold{uresult}()] is like \texttt{result()} but omits the checks. 
321  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. 

4317  151 

152 
\item[\ttindexbold{bind_thm} ($name$, $thm$);]\index{theorems!storing} 

5205  153 
stores \texttt{standard $thm$} (see \S\ref{MiscellaneousForwardRules}) 
4317  154 
in the theorem database associated with its theory and in the {\ML} 
155 
variable $name$. The theorem can be retrieved from the database 

5205  156 
using \texttt{get_thm} (see \S\ref{BasicOperationsOnTheories}). 
4317  157 

158 
\item[\ttindexbold{store_thm} ($name$, $thm$)]\index{theorems!storing} 

159 
stores $thm$ in the theorem database associated with its theory and 

160 
returns that theorem. 

321  161 
\end{ttdescription} 
104  162 

163 

1222  164 
\subsection{Retrieving theorems} 
165 
\index{theorems!retrieving} 

166 

4317  167 
The following functions retrieve theorems (together with their names) 
168 
from the theorem database that is associated with the current proof 

169 
state's theory. They can only find theorems that have explicitly been 

170 
stored in the database using \ttindex{qed}, \ttindex{bind_thm} or 

1222  171 
related functions. 
172 
\begin{ttbox} 

4317  173 
findI : int > (string * thm) list 
174 
findE : int > int > (string * thm) list 

175 
findEs : int > (string * thm) list 

176 
thms_containing : xstring list > (string * thm) list 

1222  177 
\end{ttbox} 
178 
\begin{ttdescription} 

179 
\item[\ttindexbold{findI} $i$]\index{assumptions!of main goal} 

1225  180 
returns all ``introduction rules'' applicable to subgoal $i$  all 
1222  181 
theorems whose conclusion matches (rather than unifies with) subgoal 
5205  182 
$i$. Useful in connection with \texttt{resolve_tac}. 
1222  183 

184 
\item[\ttindexbold{findE} $n$ $i$] returns all ``elimination rules'' 

1225  185 
applicable to premise $n$ of subgoal $i$  all those theorems whose 
186 
first premise matches premise $n$ of subgoal $i$. Useful in connection with 

5205  187 
\texttt{eresolve_tac} and \texttt{dresolve_tac}. 
1222  188 

189 
\item[\ttindexbold{findEs} $i$] returns all ``elimination rules'' applicable 

1225  190 
to subgoal $i$  all those theorems whose first premise matches some 
5205  191 
premise of subgoal $i$. Useful in connection with \texttt{eresolve_tac} and 
192 
\texttt{dresolve_tac}. 

4317  193 

194 
\item[\ttindexbold{thms_containing} $consts$] returns all theorems 

195 
that contain all of a given set of constants. Note that a few basic 

196 
constants like \verb$==>$ are ignored. 

1222  197 
\end{ttdescription} 
198 

199 

104  200 
\subsection{Undoing and backtracking} 
201 
\begin{ttbox} 

202 
chop : unit > unit 

203 
choplev : int > unit 

204 
back : unit > unit 

205 
undo : unit > unit 

206 
\end{ttbox} 

321  207 
\begin{ttdescription} 
104  208 
\item[\ttindexbold{chop}();] 
209 
deletes the top level of the state list, cancelling the last \ttindex{by} 

5205  210 
command. It provides a limited undo facility, and the \texttt{undo} command 
104  211 
can cancel it. 
212 

213 
\item[\ttindexbold{choplev} {\it n};] 

2128
4e8644805af2
Documents the use of negative arguments to choplev and prlev
paulson
parents:
1283
diff
changeset

214 
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

215 
of~$n$ refers to the $n$th previous level: 
5205  216 
\hbox{\verbchoplev ~1} has the same effect as \texttt{chop}. 
104  217 

218 
\item[\ttindexbold{back}();] 

219 
searches the state list for a nonempty branch point, starting from the top 

220 
level. The first one found becomes the current proof state  the most 

286  221 
recent alternative branch is taken. This is a form of interactive 
222 
backtracking. 

104  223 

224 
\item[\ttindexbold{undo}();] 

225 
cancels the most recent change to the proof state by the commands \ttindex{by}, 

5205  226 
\texttt{chop}, \texttt{choplev}, and~\texttt{back}. It {\bf cannot} 
227 
cancel \texttt{goal} or \texttt{undo} itself. It can be repeated to 

104  228 
cancel a series of commands. 
321  229 
\end{ttdescription} 
286  230 

231 
\goodbreak 

5205  232 
\noindent{\it Error indications for \texttt{back}:}\par\nobreak 
104  233 
\begin{itemize} 
286  234 
\item{\footnotesize\tt"Warning:\ same as previous choice at this level"} 
5205  235 
means \texttt{back} found a nonempty branch point, but that it contained 
286  236 
the same proof state as the current one. 
237 
\item{\footnotesize\tt "Warning:\ signature of proof state has changed"} 

238 
means the signature of the alternative proof state differs from that of 

239 
the current state. 

5205  240 
\item {\footnotesize\tt "back:\ no alternatives"} means \texttt{back} could 
286  241 
find no alternative proof state. 
104  242 
\end{itemize} 
243 

507  244 
\subsection{Printing the proof state}\label{sec:goalsprinting} 
321  245 
\index{proof state!printing of} 
104  246 
\begin{ttbox} 
247 
pr : unit > unit 

248 
prlev : int > unit 

2528  249 
prlim : int > unit 
104  250 
goals_limit: int ref \hfill{\bf initially 10} 
251 
\end{ttbox} 

2528  252 
See also the printing control options described 
253 
in~\S\ref{sec:printingcontrol}. 

321  254 
\begin{ttdescription} 
104  255 
\item[\ttindexbold{pr}();] 
256 
prints the current proof state. 

257 

258 
\item[\ttindexbold{prlev} {\it n};] 

2128
4e8644805af2
Documents the use of negative arguments to choplev and prlev
paulson
parents:
1283
diff
changeset

259 
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

260 
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

261 
you to review earlier stages of the proof. 
104  262 

2528  263 
\item[\ttindexbold{prlim} {\it k};] 
264 
prints the current proof state, limiting the number of subgoals to~$k$. It 

5205  265 
updates \texttt{goals_limit} (see below) and is helpful when there are many 
2528  266 
subgoals. 
267 

321  268 
\item[\ttindexbold{goals_limit} := {\it k};] 
104  269 
specifies~$k$ as the maximum number of subgoals to print. 
321  270 
\end{ttdescription} 
104  271 

272 

273 
\subsection{Timing} 

321  274 
\index{timing statistics}\index{proofs!timing} 
104  275 
\begin{ttbox} 
276 
proof_timing: bool ref \hfill{\bf initially false} 

277 
\end{ttbox} 

278 

321  279 
\begin{ttdescription} 
4317  280 
\item[set \ttindexbold{proof_timing};] 
104  281 
makes the \ttindex{by} and \ttindex{prove_goal} commands display how much 
282 
processor time was spent. This information is compilerdependent. 

321  283 
\end{ttdescription} 
104  284 

285 

286 
\section{Shortcuts for applying tactics} 

5205  287 
\index{shortcuts!for \texttt{by} commands} 
104  288 
These commands call \ttindex{by} with common tactics. Their chief purpose 
289 
is to minimise typing, although the scanning shortcuts are useful in their 

290 
own right. Chapter~\ref{tactics} explains the tactics themselves. 

291 

292 
\subsection{Refining a given subgoal} 

293 
\begin{ttbox} 

321  294 
ba : int > unit 
295 
br : thm > int > unit 

296 
be : thm > int > unit 

297 
bd : thm > int > unit 

298 
brs : thm list > int > unit 

299 
bes : thm list > int > unit 

300 
bds : thm list > int > unit 

104  301 
\end{ttbox} 
302 

321  303 
\begin{ttdescription} 
104  304 
\item[\ttindexbold{ba} {\it i};] 
5205  305 
performs \texttt{by (assume_tac {\it i});} 
104  306 

307 
\item[\ttindexbold{br} {\it thm} {\it i};] 

5205  308 
performs \texttt{by (resolve_tac [{\it thm}] {\it i});} 
104  309 

310 
\item[\ttindexbold{be} {\it thm} {\it i};] 

5205  311 
performs \texttt{by (eresolve_tac [{\it thm}] {\it i});} 
104  312 

313 
\item[\ttindexbold{bd} {\it thm} {\it i};] 

5205  314 
performs \texttt{by (dresolve_tac [{\it thm}] {\it i});} 
104  315 

316 
\item[\ttindexbold{brs} {\it thms} {\it i};] 

5205  317 
performs \texttt{by (resolve_tac {\it thms} {\it i});} 
104  318 

319 
\item[\ttindexbold{bes} {\it thms} {\it i};] 

5205  320 
performs \texttt{by (eresolve_tac {\it thms} {\it i});} 
104  321 

322 
\item[\ttindexbold{bds} {\it thms} {\it i};] 

5205  323 
performs \texttt{by (dresolve_tac {\it thms} {\it i});} 
321  324 
\end{ttdescription} 
104  325 

326 

327 
\subsection{Scanning shortcuts} 

328 
These shortcuts scan for a suitable subgoal (starting from subgoal~1). 

329 
They refine the first subgoal for which the tactic succeeds. Thus, they 

5205  330 
require less typing than \texttt{br}, etc. They display the selected 
104  331 
subgoal's number; please watch this, for it may not be what you expect! 
332 

333 
\begin{ttbox} 

321  334 
fa : unit > unit 
335 
fr : thm > unit 

336 
fe : thm > unit 

337 
fd : thm > unit 

338 
frs : thm list > unit 

339 
fes : thm list > unit 

340 
fds : thm list > unit 

104  341 
\end{ttbox} 
342 

321  343 
\begin{ttdescription} 
104  344 
\item[\ttindexbold{fa}();] 
321  345 
solves some subgoal by assumption. 
104  346 

347 
\item[\ttindexbold{fr} {\it thm};] 

5205  348 
refines some subgoal using \texttt{resolve_tac [{\it thm}]} 
104  349 

350 
\item[\ttindexbold{fe} {\it thm};] 

5205  351 
refines some subgoal using \texttt{eresolve_tac [{\it thm}]} 
104  352 

353 
\item[\ttindexbold{fd} {\it thm};] 

5205  354 
refines some subgoal using \texttt{dresolve_tac [{\it thm}]} 
104  355 

356 
\item[\ttindexbold{frs} {\it thms};] 

5205  357 
refines some subgoal using \texttt{resolve_tac {\it thms}} 
104  358 

359 
\item[\ttindexbold{fes} {\it thms};] 

5205  360 
refines some subgoal using \texttt{eresolve_tac {\it thms}} 
104  361 

362 
\item[\ttindexbold{fds} {\it thms};] 

5205  363 
refines some subgoal using \texttt{dresolve_tac {\it thms}} 
321  364 
\end{ttdescription} 
104  365 

366 
\subsection{Other shortcuts} 

367 
\begin{ttbox} 

368 
bw : thm > unit 

369 
bws : thm list > unit 

370 
ren : string > int > unit 

371 
\end{ttbox} 

321  372 
\begin{ttdescription} 
5205  373 
\item[\ttindexbold{bw} {\it def};] performs \texttt{by 
4317  374 
(rewrite_goals_tac [{\it def}]);} It unfolds definitions in the 
375 
subgoals (but not the main goal), by metarewriting with the given 

376 
definition (see also \S\ref{sec:rewrite_goals}). 

377 
\index{metarewriting} 

104  378 

379 
\item[\ttindexbold{bws}] 

5205  380 
is like \texttt{bw} but takes a list of definitions. 
104  381 

382 
\item[\ttindexbold{ren} {\it names} {\it i};] 

5205  383 
performs \texttt{by (rename_tac {\it names} {\it i});} it renames 
332  384 
parameters in subgoal~$i$. (Ignore the message {\footnotesize\tt Warning:\ 
385 
same as previous level}.) 

321  386 
\index{parameters!renaming} 
387 
\end{ttdescription} 

104  388 

389 

321  390 
\section{Executing batch proofs} 
3128
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

391 
\index{batch execution}% 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

392 
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

393 
tactic list}, which is the type of a tactical proof. 
286  394 
\begin{ttbox} 
3128
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

395 
prove_goal : theory > string > tacfun > thm 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

396 
qed_goal : string > theory > string > tacfun > unit 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

397 
prove_goalw: theory > thm list > string > tacfun > thm 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

398 
qed_goalw : string > theory > thm list > string > tacfun > unit 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

399 
prove_goalw_cterm: thm list > cterm > tacfun > thm 
104  400 
\end{ttbox} 
321  401 
These batch functions create an initial proof state, then apply a tactic to 
402 
it, yielding a sequence of final proof states. The head of the sequence is 

104  403 
returned, provided it is an instance of the theorem originally proposed. 
5205  404 
The forms \texttt{prove_goal}, \texttt{prove_goalw} and \texttt{prove_goalw_cterm} 
405 
are analogous to \texttt{goal}, \texttt{goalw} and \texttt{goalw_cterm}. 

104  406 

407 
The tactic is specified by a function from theorem lists to tactic lists. 

332  408 
The function is applied to the list of metaassumptions taken from 
409 
the main goal. The resulting tactics are applied in sequence (using {\tt 

410 
EVERY}). For example, a proof consisting of the commands 

104  411 
\begin{ttbox} 
412 
val prems = goal {\it theory} {\it formula}; 

413 
by \(tac@1\); \ldots by \(tac@n\); 

3108  414 
qed "my_thm"; 
104  415 
\end{ttbox} 
416 
can be transformed to an expression as follows: 

417 
\begin{ttbox} 

3108  418 
qed_goal "my_thm" {\it theory} {\it formula} 
104  419 
(fn prems=> [ \(tac@1\), \ldots, \(tac@n\) ]); 
420 
\end{ttbox} 

421 
The methods perform identical processing of the initial {\it formula} and 

5205  422 
the final proof state. But \texttt{prove_goal} executes the tactic as a 
332  423 
atomic operation, bypassing the subgoal module; the current interactive 
424 
proof is unaffected. 

425 
% 

321  426 
\begin{ttdescription} 
427 
\item[\ttindexbold{prove_goal} {\it theory} {\it formula} {\it tacsf};] 

104  428 
executes a proof of the {\it formula\/} in the given {\it theory}, using 
429 
the given tactic function. 

430 

4317  431 
\item[\ttindexbold{qed_goal} $name$ $theory$ $formula$ $tacsf$;] acts 
5205  432 
like \texttt{prove_goal} but also stores the resulting theorem in the 
4317  433 
theorem database associated with its theory and in the {\ML} 
434 
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

435 

104  436 
\item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula} 
321  437 
{\it tacsf};]\index{metarewriting} 
5205  438 
is like \texttt{prove_goal} but also applies the list of {\it defs\/} as 
104  439 
metarewrite rules to the first subgoal and the premises. 
440 

866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

441 
\item[\ttindexbold{qed_goalw} $name$ $theory$ $defs$ $formula$ $tacsf$;] 
5205  442 
is analogous to \texttt{qed_goal}. 
866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

443 

104  444 
\item[\ttindexbold{prove_goalw_cterm} {\it theory} {\it defs} {\it ct} 
321  445 
{\it tacsf};] 
5205  446 
is a version of \texttt{prove_goalw} for programming applications. The main 
104  447 
goal is supplied as a cterm, not as a string. Typically, the cterm is 
286  448 
created from a term~$t$ as follows: 
449 
\begin{ttbox} 

3108  450 
cterm_of (sign_of thy) \(t\) 
286  451 
\end{ttbox} 
3108  452 
\index{*cterm_of}\index{*sign_of} 
321  453 
\end{ttdescription} 
104  454 

455 

321  456 
\section{Managing multiple proofs} 
457 
\index{proofs!managing multiple} 

104  458 
You may save the current state of the subgoal module and resume work on it 
459 
later. This serves two purposes. 

460 
\begin{enumerate} 

461 
\item At some point, you may be uncertain of the next step, and 

462 
wish to experiment. 

463 

464 
\item During a proof, you may see that a lemma should be proved first. 

465 
\end{enumerate} 

466 
Each saved proof state consists of a list of levels; \ttindex{chop} behaves 

467 
independently for each of the saved proofs. In addition, each saved state 

468 
carries a separate \ttindex{undo} list. 

469 

321  470 
\subsection{The stack of proof states} 
471 
\index{proofs!stacking} 

104  472 
\begin{ttbox} 
473 
push_proof : unit > unit 

474 
pop_proof : unit > thm list 

475 
rotate_proof : unit > thm list 

476 
\end{ttbox} 

477 
The subgoal module maintains a stack of proof states. Most subgoal 

5205  478 
commands affect only the top of the stack. The \ttindex{Goal} command {\em 
321  479 
replaces\/} the top of the stack; the only command that pushes a proof on the 
5205  480 
stack is \texttt{push_proof}. 
104  481 

5205  482 
To save some point of the proof, call \texttt{push_proof}. You may now 
483 
state a lemma using \texttt{goal}, or simply continue to apply tactics. 

484 
Later, you can return to the saved point by calling \texttt{pop_proof} or 

485 
\texttt{rotate_proof}. 

104  486 

5205  487 
To view the entire stack, call \texttt{rotate_proof} repeatedly; as it rotates 
104  488 
the stack, it prints the new top element. 
489 

321  490 
\begin{ttdescription} 
104  491 
\item[\ttindexbold{push_proof}();] 
492 
duplicates the top element of the stack, pushing a copy of the current 

493 
proof state on to the stack. 

494 

495 
\item[\ttindexbold{pop_proof}();] 

496 
discards the top element of the stack. It returns the list of 

332  497 
assumptions associated with the new proof; you should bind these to an 
104  498 
\ML\ identifier. They can also be obtained by calling \ttindex{premises}. 
499 

321  500 
\item[\ttindexbold{rotate_proof}();] 
501 
\index{assumptions!of main goal} 

104  502 
rotates the stack, moving the top element to the bottom. It returns the 
503 
list of assumptions associated with the new proof. 

321  504 
\end{ttdescription} 
104  505 

506 

321  507 
\subsection{Saving and restoring proof states} 
508 
\index{proofs!saving and restoring} 

104  509 
\begin{ttbox} 
510 
save_proof : unit > proof 

511 
restore_proof : proof > thm list 

512 
\end{ttbox} 

513 
States of the subgoal module may be saved as \ML\ values of 

321  514 
type~\mltydx{proof}, and later restored. 
104  515 

321  516 
\begin{ttdescription} 
104  517 
\item[\ttindexbold{save_proof}();] 
518 
returns the current state, which is on top of the stack. 

519 

321  520 
\item[\ttindexbold{restore_proof} {\it prf};]\index{assumptions!of main goal} 
521 
replaces the top of the stack by~{\it prf}. It returns the list of 

522 
assumptions associated with the new proof. 

523 
\end{ttdescription} 

104  524 

525 

4317  526 
\section{*Debugging and inspecting} 
321  527 
\index{tactics!debugging} 
2611  528 
These functions can be useful when you are debugging a tactic. They refer 
529 
to the current proof state stored in the subgoal module. A tactic 

530 
should never call them; it should operate on the proof state supplied as its 

531 
argument. 

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 postprocessing 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 

5205  570 
this using \texttt{prin}, though you may have to examine the internal 
104  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 metalevel 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 

2611  579 

321  580 
\subsection{Filtering lists of rules} 
104  581 
\begin{ttbox} 
582 
filter_goal: (term*term>bool) > thm list > int > thm list 

583 
\end{ttbox} 

584 

321  585 
\begin{ttdescription} 
104  586 
\item[\ttindexbold{filter_goal} {\it could} {\it ths} {\it i}] 
5205  587 
applies \texttt{filter_thms {\it could}} to subgoal~$i$ of the proof 
104  588 
state and returns the list of theorems that survive the filtering. 
321  589 
\end{ttdescription} 
104  590 

591 
\index{subgoal module)} 

592 
\index{proofs)} 