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}


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


47 
val prems = it;

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 metarewrite rules. This


56 
expansion affects both the first 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 metaquantified {\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 
metarewrite rules to the first subgoal and the premises.

321

75 
\index{metarewriting}

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 metahypotheses 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 nonempty 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 


120 
\subsection{Extracting the proved theorem}

321

121 
\index{theorems!from subgoal module}

104

122 
\begin{ttbox}


123 
result : unit > thm


124 
uresult : unit > thm


125 
\end{ttbox}

321

126 
\begin{ttdescription}


127 
\item[\ttindexbold{result}()]\index{assumptions!of main goal}

104

128 
returns the final theorem, after converting the free variables to


129 
schematics. It discharges the assumptions supplied to the matching

321

130 
{\tt goal} command.

104

131 


132 
It raises an exception unless the proof state passes certain checks. There

321

133 
must be no assumptions other than those supplied to {\tt goal}. There

104

134 
must be no subgoals. The theorem proved must be a (firstorder) instance

321

135 
of the original goal, as stated in the {\tt goal} command. This allows

104

136 
{\bf answer extraction}  instantiation of variables  but no other


137 
changes to the main goal. The theorem proved must have the same signature


138 
as the initial proof state.


139 

321

140 
These checks are needed because an Isabelle tactic can return any proof


141 
state at all.


142 


143 
\item[\ttindexbold{uresult}()] is like {\tt result()} but omits the checks.


144 
It is needed when the initial goal contains function unknowns, when


145 
definitions are unfolded in the main goal (by calling


146 
\ttindex{rewrite_tac}),\index{definitions!unfolding} or when


147 
\ttindex{assume_ax} has been used.


148 
\end{ttdescription}

104

149 


150 


151 
\subsection{Undoing and backtracking}


152 
\begin{ttbox}


153 
chop : unit > unit


154 
choplev : int > unit


155 
back : unit > unit


156 
undo : unit > unit


157 
\end{ttbox}

321

158 
\begin{ttdescription}

104

159 
\item[\ttindexbold{chop}();]


160 
deletes the top level of the state list, cancelling the last \ttindex{by}


161 
command. It provides a limited undo facility, and the {\tt undo} command


162 
can cancel it.


163 


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


165 
truncates the state list to level~{\it n}.


166 


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


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


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

286

170 
recent alternative branch is taken. This is a form of interactive


171 
backtracking.

104

172 


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


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


175 
{\tt chop}, {\tt choplev}, and~{\tt back}. It {\bf cannot}


176 
cancel {\tt goal} or {\tt undo} itself. It can be repeated to


177 
cancel a series of commands.

321

178 
\end{ttdescription}

286

179 


180 
\goodbreak


181 
\noindent{\it Error indications for {\tt back}:}\par\nobreak

104

182 
\begin{itemize}

286

183 
\item{\footnotesize\tt"Warning:\ same as previous choice at this level"}


184 
means {\tt back} found a nonempty branch point, but that it contained


185 
the same proof state as the current one.


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


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


188 
the current state.


189 
\item {\footnotesize\tt "back:\ no alternatives"} means {\tt back} could


190 
find no alternative proof state.

104

191 
\end{itemize}


192 


193 
\subsection{Printing the proof state}

321

194 
\index{proof state!printing of}

104

195 
\begin{ttbox}


196 
pr : unit > unit


197 
prlev : int > unit


198 
goals_limit: int ref \hfill{\bf initially 10}


199 
\end{ttbox}

321

200 
\begin{ttdescription}

104

201 
\item[\ttindexbold{pr}();]


202 
prints the current proof state.


203 


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


205 
prints the proof state at level {\it n}. This allows you to review the


206 
previous steps of the proof.


207 

321

208 
\item[\ttindexbold{goals_limit} := {\it k};]

104

209 
specifies~$k$ as the maximum number of subgoals to print.

321

210 
\end{ttdescription}

104

211 


212 


213 
\subsection{Timing}

321

214 
\index{timing statistics}\index{proofs!timing}

104

215 
\begin{ttbox}


216 
proof_timing: bool ref \hfill{\bf initially false}


217 
\end{ttbox}


218 

321

219 
\begin{ttdescription}


220 
\item[\ttindexbold{proof_timing} := true;]

104

221 
makes the \ttindex{by} and \ttindex{prove_goal} commands display how much


222 
processor time was spent. This information is compilerdependent.

321

223 
\end{ttdescription}

104

224 


225 


226 
\section{Shortcuts for applying tactics}

321

227 
\index{shortcuts!for {\tt by} commands}

104

228 
These commands call \ttindex{by} with common tactics. Their chief purpose


229 
is to minimise typing, although the scanning shortcuts are useful in their


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


231 


232 
\subsection{Refining a given subgoal}


233 
\begin{ttbox}

321

234 
ba : int > unit


235 
br : thm > int > unit


236 
be : thm > int > unit


237 
bd : thm > int > unit


238 
brs : thm list > int > unit


239 
bes : thm list > int > unit


240 
bds : thm list > int > unit

104

241 
\end{ttbox}


242 

321

243 
\begin{ttdescription}

104

244 
\item[\ttindexbold{ba} {\it i};]

321

245 
performs \hbox{\tt by (assume_tac {\it i});}

104

246 


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

321

248 
performs \hbox{\tt by (resolve_tac [{\it thm}] {\it i});}

104

249 


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

321

251 
performs \hbox{\tt by (eresolve_tac [{\it thm}] {\it i});}

104

252 


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

321

254 
performs \hbox{\tt by (dresolve_tac [{\it thm}] {\it i});}

104

255 


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

321

257 
performs \hbox{\tt by (resolve_tac {\it thms} {\it i});}

104

258 


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

321

260 
performs \hbox{\tt by (eresolve_tac {\it thms} {\it i});}

104

261 


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

321

263 
performs \hbox{\tt by (dresolve_tac {\it thms} {\it i});}


264 
\end{ttdescription}

104

265 


266 


267 
\subsection{Scanning shortcuts}


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


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


270 
require less typing than {\tt br}, etc. They display the selected


271 
subgoal's number; please watch this, for it may not be what you expect!


272 


273 
\begin{ttbox}

321

274 
fa : unit > unit


275 
fr : thm > unit


276 
fe : thm > unit


277 
fd : thm > unit


278 
frs : thm list > unit


279 
fes : thm list > unit


280 
fds : thm list > unit

104

281 
\end{ttbox}


282 

321

283 
\begin{ttdescription}

104

284 
\item[\ttindexbold{fa}();]

321

285 
solves some subgoal by assumption.

104

286 


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


288 
refines some subgoal using \hbox{\tt resolve_tac [{\it thm}]}


289 


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


291 
refines some subgoal using \hbox{\tt eresolve_tac [{\it thm}]}


292 


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


294 
refines some subgoal using \hbox{\tt dresolve_tac [{\it thm}]}


295 


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


297 
refines some subgoal using \hbox{\tt resolve_tac {\it thms}}


298 


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


300 
refines some subgoal using \hbox{\tt eresolve_tac {\it thms}}


301 


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


303 
refines some subgoal using \hbox{\tt dresolve_tac {\it thms}}

321

304 
\end{ttdescription}

104

305 


306 
\subsection{Other shortcuts}


307 
\begin{ttbox}


308 
bw : thm > unit


309 
bws : thm list > unit


310 
ren : string > int > unit


311 
\end{ttbox}

321

312 
\begin{ttdescription}

104

313 
\item[\ttindexbold{bw} {\it def};]


314 
performs \hbox{\tt by (rewrite_goals_tac [{\it def}]);}


315 
It unfolds definitions in the subgoals (but not the main goal), by

321

316 
metarewriting with the given definition.


317 
\index{metarewriting}

104

318 


319 
\item[\ttindexbold{bws}]


320 
is like {\tt bw} but takes a list of definitions.


321 


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


323 
performs \hbox{\tt by (rename_tac {\it names} {\it i});} it renames


324 
parameters in subgoal~$i$. (Ignore the message {\tt Warning:\ same as


325 
previous level}.)

321

326 
\index{parameters!renaming}


327 
\end{ttdescription}

104

328 


329 

321

330 
\section{Executing batch proofs}


331 
\index{batch execution}

286

332 
\begin{ttbox}

104

333 
prove_goal : theory> string>(thm list>tactic list)>thm


334 
prove_goalw : theory>thm list>string>(thm list>tactic list)>thm


335 
prove_goalw_cterm: thm list>Sign.cterm>(thm list>tactic list)>thm


336 
\end{ttbox}

321

337 
These batch functions create an initial proof state, then apply a tactic to


338 
it, yielding a sequence of final proof states. The head of the sequence is

104

339 
returned, provided it is an instance of the theorem originally proposed.


340 
The forms {\tt prove_goal}, {\tt prove_goalw} and {\tt prove_goalw_cterm}

321

341 
are analogous to {\tt goal}, {\tt goalw} and {\tt goalw_cterm}.

104

342 


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


344 
The function is applied to the list of metahypotheses taken from the main


345 
goal. The resulting tactics are applied in sequence (using {\tt EVERY}).


346 
For example, a proof consisting of the commands


347 
\begin{ttbox}


348 
val prems = goal {\it theory} {\it formula};


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


350 
val my_thm = result();


351 
\end{ttbox}


352 
can be transformed to an expression as follows:


353 
\begin{ttbox}


354 
val my_thm = prove_goal {\it theory} {\it formula}


355 
(fn prems=> [ \(tac@1\), \ldots, \(tac@n\) ]);


356 
\end{ttbox}


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


358 
the final proof state, but {\tt prove_goal} executes the tactic as a

321

359 
atomic operation, bypassing the subgoal module.


360 


361 
A batch proof may alternatively consist of subgoal commands encapsulated


362 
using~{\tt let}:

104

363 
\begin{ttbox}


364 
val my_thm =


365 
let val prems = goal {\it theory} {\it formula}


366 
in by \(tac@1\); \ldots by \(tac@n\); result() end;


367 
\end{ttbox}


368 

321

369 
\begin{ttdescription}


370 
\item[\ttindexbold{prove_goal} {\it theory} {\it formula} {\it tacsf};]

104

371 
executes a proof of the {\it formula\/} in the given {\it theory}, using


372 
the given tactic function.


373 


374 
\item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula}

321

375 
{\it tacsf};]\index{metarewriting}

104

376 
is like {\tt prove_goal} but also applies the list of {\it defs\/} as


377 
metarewrite rules to the first subgoal and the premises.


378 


379 
\item[\ttindexbold{prove_goalw_cterm} {\it theory} {\it defs} {\it ct}

321

380 
{\it tacsf};]


381 
is a version of {\tt prove_goalw} for programming applications. The main

104

382 
goal is supplied as a cterm, not as a string. Typically, the cterm is

286

383 
created from a term~$t$ as follows:


384 
\begin{ttbox}


385 
Sign.cterm_of (sign_of thy) \(t\)


386 
\end{ttbox}

104

387 
\index{*Sign.cterm_of}\index{*sign_of}

321

388 
\end{ttdescription}

104

389 


390 

321

391 
\section{Managing multiple proofs}


392 
\index{proofs!managing multiple}

104

393 
You may save the current state of the subgoal module and resume work on it


394 
later. This serves two purposes.


395 
\begin{enumerate}


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


397 
wish to experiment.


398 


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


400 
\end{enumerate}


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


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


403 
carries a separate \ttindex{undo} list.


404 

321

405 
\subsection{The stack of proof states}


406 
\index{proofs!stacking}

104

407 
\begin{ttbox}


408 
push_proof : unit > unit


409 
pop_proof : unit > thm list


410 
rotate_proof : unit > thm list


411 
\end{ttbox}


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

321

413 
commands affect only the top of the stack. The \ttindex{goal} command {\em


414 
replaces\/} the top of the stack; the only command that pushes a proof on the

104

415 
stack is {\tt push_proof}.


416 


417 
To save some point of the proof, call {\tt push_proof}. You may now

321

418 
state a lemma using {\tt goal}, or simply continue to apply tactics.

104

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


420 
{\tt rotate_proof}.


421 


422 
To view the entire stack, call {\tt rotate_proof} repeatedly; as it rotates


423 
the stack, it prints the new top element.


424 

321

425 
\begin{ttdescription}

104

426 
\item[\ttindexbold{push_proof}();]


427 
duplicates the top element of the stack, pushing a copy of the current


428 
proof state on to the stack.


429 


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


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


432 
metahypotheses associated with the new proof; you should bind these to an


433 
\ML\ identifier. They can also be obtained by calling \ttindex{premises}.


434 

321

435 
\item[\ttindexbold{rotate_proof}();]


436 
\index{assumptions!of main goal}

104

437 
rotates the stack, moving the top element to the bottom. It returns the


438 
list of assumptions associated with the new proof.

321

439 
\end{ttdescription}

104

440 


441 

321

442 
\subsection{Saving and restoring proof states}


443 
\index{proofs!saving and restoring}

104

444 
\begin{ttbox}


445 
save_proof : unit > proof


446 
restore_proof : proof > thm list


447 
\end{ttbox}


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

321

449 
type~\mltydx{proof}, and later restored.

104

450 

321

451 
\begin{ttdescription}

104

452 
\item[\ttindexbold{save_proof}();]


453 
returns the current state, which is on top of the stack.


454 

321

455 
\item[\ttindexbold{restore_proof} {\it prf};]\index{assumptions!of main goal}


456 
replaces the top of the stack by~{\it prf}. It returns the list of


457 
assumptions associated with the new proof.


458 
\end{ttdescription}

104

459 


460 

321

461 
\section{Debugging and inspecting}


462 
\index{tactics!debugging}

104

463 
These specialized operations support the debugging of tactics. They refer

321

464 
to the current proof state of the subgoal module.

104

465 

321

466 
\subsection{Reading and printing terms}


467 
\index{terms!reading of}\index{terms!printing of}\index{types!printing of}

104

468 
\begin{ttbox}


469 
read : string > term


470 
prin : term > unit


471 
printyp : typ > unit


472 
\end{ttbox}


473 
These read and print terms (or types) using the syntax associated with the


474 
proof state.


475 

321

476 
\begin{ttdescription}

104

477 
\item[\ttindexbold{read} {\it string}]


478 
reads the {\it string} as a term, without type checking.


479 


480 
\item[\ttindexbold{prin} {\it t};]


481 
prints the term~$t$ at the terminal.


482 


483 
\item[\ttindexbold{printyp} {\it T};]


484 
prints the type~$T$ at the terminal.

321

485 
\end{ttdescription}

104

486 

321

487 
\subsection{Inspecting the proof state}


488 
\index{proofs!inspecting the state}

104

489 
\begin{ttbox}


490 
topthm : unit > thm


491 
getgoal : int > term


492 
gethyps : int > thm list


493 
\end{ttbox}


494 

321

495 
\begin{ttdescription}

104

496 
\item[\ttindexbold{topthm}()]


497 
returns the proof state as an Isabelle theorem. This is what \ttindex{by}


498 
would supply to a tactic at this point. It omits the postprocessing of


499 
\ttindex{result} and \ttindex{uresult}.


500 


501 
\item[\ttindexbold{getgoal} {\it i}]


502 
returns subgoal~$i$ of the proof state, as a term. You may print


503 
this using {\tt prin}, though you may have to examine the internal


504 
data structure in order to locate the problem!


505 

321

506 
\item[\ttindexbold{gethyps} {\it i}]


507 
returns the hypotheses of subgoal~$i$ as metalevel assumptions. In


508 
these theorems, the subgoal's parameters become free variables. This


509 
command is supplied for debugging uses of \ttindex{METAHYPS}.


510 
\end{ttdescription}

104

511 

321

512 
\subsection{Filtering lists of rules}

104

513 
\begin{ttbox}


514 
filter_goal: (term*term>bool) > thm list > int > thm list


515 
\end{ttbox}


516 

321

517 
\begin{ttdescription}

104

518 
\item[\ttindexbold{filter_goal} {\it could} {\it ths} {\it i}]


519 
applies \hbox{\tt filter_thms {\it could}} to subgoal~$i$ of the proof


520 
state and returns the list of theorems that survive the filtering.

321

521 
\end{ttdescription}

104

522 


523 
\index{subgoal module)}


524 
\index{proofs)}
