104

1 
%% $Id$


2 
\chapter{Proof Management: The Subgoal Module}


3 
\index{proofs(}


4 
\index{subgoal module(}


5 
\index{reading!goalssee{proofs, starting}}


6 
The subgoal module stores the current proof state and many previous states;


7 
commands can produce new states or return to previous ones. The {\em state


8 
list\/} at level $n$ is a list of pairs


9 
\[ [(\psi@n,\Psi@n),\; (\psi@{n1},\Psi@{n1}),\; \ldots,\; (\psi@0,[])] \]


10 
where $\psi@n$ is the current proof state, $\psi@{n1}$ is the previous


11 
one, \ldots, and $\psi@0$ is the initial proof state. The $\Psi@i$ are


12 
sequences (lazy lists) of proof states, storing branch points where a


13 
tactic returned a list longer than one. The state lists permit various


14 
forms of backtracking.


15 


16 
Chopping elements from the state list reverts to previous proof states.


17 
Besides this, the \ttindex{undo} command keeps a list of state lists. The


18 
module actually maintains a stack of state lists, to support several


19 
proofs at the same time.


20 


21 
The subgoal module always contains some proof state. At the start of the


22 
Isabelle session, this state consists of a dummy formula.


23 


24 


25 
\section{Basic commands}


26 
Most proofs begin with {\tt goal} or {\tt goalw} and require no other


27 
commands than {\tt by}, {\tt chop} and {\tt undo}. They typically end with


28 
a call to {\tt result}.


29 
\subsection{Starting a backward proof}


30 
\index{proofs!startingbold}


31 
\begin{ttbox}


32 
goal : theory > string > thm list


33 
goalw : theory > thm list > string > thm list


34 
goalw_cterm : thm list > Sign.cterm > thm list


35 
premises : unit > thm list


36 
\end{ttbox}


37 
The {\tt goal} commands start a new proof by setting the goal. They


38 
replace the current state list by a new one consisting of the initial proof


39 
state. They also empty the \ttindex{undo} list; this command cannot be


40 
undone!


41 


42 
They all return a list of metahypotheses taken from the main goal. If


43 
this list is nonempty, bind its value to an \ML{} identifier by typing


44 
something like


45 
\begin{ttbox}


46 
val prems = it;


47 
\end{ttbox}


48 
These assumptions serve as the premises when you are deriving a rule. They


49 
are also stored internally and can be retrieved later by the function {\tt


50 
premises}. When the proof is finished, \ttindex{result} compares the


51 
stored assumptions with the actual assumptions in the proof state.


52 


53 
Some of the commands unfold definitions using metarewrite rules. This


54 
expansion affects both the first subgoal and the premises, which would


55 
otherwise require use of \ttindex{rewrite_goals_tac} and


56 
\ttindex{rewrite_rule}.


57 


58 
If the main goal has the form {\tt"!!{\it vars}.\ \ldots"}, with an outermost


59 
quantifier, then the list of premises will be empty. Subgoal~1 will


60 
contain the metaquantified {\it vars\/} as parameters and the goal's premises


61 
as assumptions. This is useful when the next step of the proof would


62 
otherwise be to call \ttindex{cut_facts_tac} with the list of premises


63 
(\S\ref{cut_facts_tac}).


64 


65 
\begin{description}


66 
\item[\ttindexbold{goal} {\it theory} {\it formula}; ]


67 
begins a new proof, where {\it theory} is usually an \ML\ identifier


68 
and the {\it formula\/} is written as an \ML\ string.


69 


70 
\item[\ttindexbold{goalw} {\it theory} {\it defs} {\it formula}; ]


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


72 
metarewrite rules to the first subgoal and the premises.


73 
\index{rewriting!metalevel}


74 


75 
\item[\ttindexbold{goalw_cterm} {\it theory} {\it defs} {\it ct}; ]


76 
is a version of {\tt goalw} for special applications. The main goal is


77 
supplied as a cterm, not as a string. Typically, the cterm is created from


78 
a term~$t$ by \hbox{\tt Sign.cterm_of (sign_of thy) $t$}.


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


80 


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


82 
returns the list of metahypotheses associated with the current proof, in


83 
case you forget to bind them to an \ML{} identifier.


84 
\end{description}


85 


86 
\subsection{Applying a tactic}


87 
\index{tactics!commands for applyingbold}


88 
\begin{ttbox}


89 
by : tactic > unit


90 
byev : tactic list > unit


91 
\end{ttbox}


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


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


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


95 
tail is retained for backtracking (see~{\tt back}).


96 
\begin{description} \item[\ttindexbold{by} {\it tactic}; ]


97 
applies the {\it tactic\/} to the proof state.


98 


99 
\item[\ttindexbold{byev} {\it tactics}; ]


100 
applies the list of {\it tactics}, one at a time. It is useful for testing


101 
calls to {\tt prove_goal}, and abbreviates \hbox{\tt by (EVERY {\it


102 
tactics})}.


103 
\end{description}


104 


105 
\noindent{\bf Error indications:}


106 
\begin{itemize}


107 
\item


108 
{\tt "by:\ tactic failed"} means that the tactic returned an empty


109 
sequence when applied to the current proof state.


110 
\item


111 
{\tt "Warning:\ same as previous level"} means that the new proof state


112 
is identical to the previous state.


113 
\item


114 
{\tt "Warning:\ signature of proof state has changed"} means that a rule


115 
was applied from outside the theory of the initial proof state. This


116 
guards against mistakes such as expressing the goal in intuitionistic logic


117 
and proving it using classical logic.


118 
\end{itemize}


119 


120 
\subsection{Extracting the proved theorem}


121 
\index{ending a proofbold}


122 
\begin{ttbox}


123 
result : unit > thm


124 
uresult : unit > thm


125 
\end{ttbox}


126 
\begin{description}


127 
\item[\ttindexbold{result}()]


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


129 
schematics. It discharges the assumptions supplied to the matching


130 
\ttindex{goal} command.


131 


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


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


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


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


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 


140 
\item[\ttindexbold{uresult}()]


141 
is similar but omits the checks given above. It is needed when the initial


142 
goal contains function unknowns, when definitions are unfolded in the main


143 
goal, or when \ttindex{assume_ax} has been used.


144 
\end{description}


145 


146 


147 
\subsection{Undoing and backtracking}


148 
\index{undoing a proof commandbold}


149 
\index{backtracking commandsee{\tt back}}


150 
\begin{ttbox}


151 
chop : unit > unit


152 
choplev : int > unit


153 
back : unit > unit


154 
undo : unit > unit


155 
\end{ttbox}


156 
\begin{description}


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


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


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


160 
can cancel it.


161 


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


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


164 


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


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


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


168 
recent alternative branch is taken.


169 


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


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


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


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


174 
cancel a series of commands.


175 
\end{description}


176 
\noindent{\bf Error indications for {\tt back}:}


177 
\begin{itemize}


178 
\item


179 
{\tt"Warning:\ same as previous choice at this level"} means that {\tt


180 
back} found a nonempty branch point, but that it contained the same proof


181 
state as the current one.


182 
\item


183 
{\tt "Warning:\ signature of proof state has changed"} means the signature


184 
of the alternative proof state differs from that of the current state.


185 
\item


186 
{\tt "back:\ no alternatives"} means {\tt back} could find no alternative


187 
proof state.


188 
\end{itemize}


189 


190 
\subsection{Printing the proof state}


191 
\index{printing!proof statebold}


192 
\begin{ttbox}


193 
pr : unit > unit


194 
prlev : int > unit


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


196 
\end{ttbox}


197 
\begin{description}


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


199 
prints the current proof state.


200 


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


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


203 
previous steps of the proof.


204 


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


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


207 
\end{description}


208 


209 


210 
\subsection{Timing}


211 
\index{printing!timing statisticsbold}\index{proofs!timingbold}


212 
\begin{ttbox}


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


214 
\end{ttbox}


215 


216 
\begin{description}


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


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


219 
processor time was spent. This information is compilerdependent.


220 
\end{description}


221 


222 


223 
\section{Shortcuts for applying tactics}


224 
\index{shortcuts!for ``{\tt by}'' commandsbold}


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


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


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


228 


229 
\subsection{Refining a given subgoal}


230 
\begin{ttbox}


231 
ba: int > unit


232 
br: thm > int > unit


233 
be: thm > int > unit


234 
bd: thm > int > unit


235 
\end{ttbox}


236 


237 
\begin{description}


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


239 
performs \hbox{\tt by (assume_tac {\it i});}\index{*assume_tac}


240 


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


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


243 


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


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


246 


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


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


249 
\end{description}


250 


251 
\subsubsection{Resolution with a list of theorems}


252 
\begin{ttbox}


253 
brs: thm list > int > unit


254 
bes: thm list > int > unit


255 
bds: thm list > int > unit


256 
\end{ttbox}


257 


258 
\begin{description}


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


260 
performs \hbox{\tt by (resolve_tac {\it thms} {\it i});}\index{*resolve_tac}


261 


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


263 
performs \hbox{\tt by (eresolve_tac {\it thms} {\it i});}\index{*eresolve_tac}


264 


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


266 
performs \hbox{\tt by (dresolve_tac {\it thms} {\it i});}\index{*dresolve_tac}


267 
\end{description}


268 


269 


270 
\subsection{Scanning shortcuts}


271 
\index{shortcuts!scanning for subgoalsbold}


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


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


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


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


276 


277 
\subsubsection{Proof by assumption and resolution}


278 
\begin{ttbox}


279 
fa: unit > unit


280 
fr: thm > unit


281 
fe: thm > unit


282 
fd: thm > unit


283 
\end{ttbox}


284 


285 
\begin{description}


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


287 
solves some subgoal by assumption.\index{*assume_tac}


288 


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


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


291 
\index{*resolve_tac}


292 


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


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


295 
\index{*eresolve_tac}


296 


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


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


299 
\index{*dresolve_tac}


300 
\end{description}


301 


302 
\subsubsection{Resolution with a list of theorems}


303 
\begin{ttbox}


304 
frs: thm list > unit


305 
fes: thm list > unit


306 
fds: thm list > unit


307 
\end{ttbox}


308 


309 
\begin{description}


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


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


312 
\index{*resolve_tac}


313 


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


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


316 
\index{*eresolve_tac}


317 


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


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


320 
\index{*dresolve_tac}


321 
\end{description}


322 


323 
\subsection{Other shortcuts}


324 
\begin{ttbox}


325 
bw : thm > unit


326 
bws : thm list > unit


327 
ren : string > int > unit


328 
\end{ttbox}


329 
\begin{description}


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


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


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


333 
metarewriting with the given definition.\index{*rewrite_goals_tac}


334 
\index{rewriting!metalevel}


335 


336 
\item[\ttindexbold{bws}]


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


338 


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


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


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


342 
previous level}.)


343 
\index{*rename_tac}\index{parameters!renaming}


344 
\end{description}


345 


346 


347 


348 
\section{Advanced features}


349 
\subsection{Executing batch proofs}


350 
\index{proofs!batchbold}


351 
\index{batch executionbold}


352 
\begin{ttbox}


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


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


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


356 
\end{ttbox}


357 
A collection of derivations may be stored for batch execution using these


358 
functions. They create an initial proof state, then apply a tactic to it,


359 
yielding a sequence of final proof states. The head of the sequence is


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


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


362 
are analogous to \ttindex{goal}, \ttindex{goalw} and \ttindex{goalw_cterm}.


363 


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


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


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


367 
For example, a proof consisting of the commands


368 
\begin{ttbox}


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


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


371 
val my_thm = result();


372 
\end{ttbox}


373 
can be transformed to an expression as follows:


374 
\begin{ttbox}


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


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


377 
\end{ttbox}


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


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


380 
atomic operation, bypassing the subgoal module. The commands can also be


381 
encapsulated in an expression using~{\tt let}:


382 
\begin{ttbox}


383 
val my_thm =


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


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


386 
\end{ttbox}


387 


388 
\begin{description}


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


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


391 
the given tactic function.


392 


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


394 
{\it tacsf}; ]


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


396 
metarewrite rules to the first subgoal and the premises.


397 
\index{rewriting!metalevel}


398 


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


400 
{\it tacsf}; ]


401 
is a version of {\tt prove_goalw} for special applications. The main


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


403 
created from a term~$t$ by \hbox{\tt Sign.cterm_of (sign_of thy) $t$}.


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


405 
\end{description}


406 


407 


408 
\subsection{Managing multiple proofs}


409 
\index{proofs!managing multiplebold}


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


411 
later. This serves two purposes.


412 
\begin{enumerate}


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


414 
wish to experiment.


415 


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


417 
\end{enumerate}


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


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


420 
carries a separate \ttindex{undo} list.


421 


422 
\subsubsection{The stack of proof states}


423 
\index{proofs!stackingbold}


424 
\begin{ttbox}


425 
push_proof : unit > unit


426 
pop_proof : unit > thm list


427 
rotate_proof : unit > thm list


428 
\end{ttbox}


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


430 
commands affect only the top of the stack. The \ttindex{goal} command {\bf


431 
replaces} the top of the stack; the only command that pushes a proof on the


432 
stack is {\tt push_proof}.


433 


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


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


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


437 
{\tt rotate_proof}.


438 


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


440 
the stack, it prints the new top element.


441 


442 
\begin{description}


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


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


445 
proof state on to the stack.


446 


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


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


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


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


451 


452 
\item[\ttindexbold{rotate_proof}]


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


454 
list of assumptions associated with the new proof.


455 
\end{description}


456 


457 


458 
\subsubsection{Saving and restoring proof states}


459 
\index{proofs!saving and restoringbold}


460 
\begin{ttbox}


461 
save_proof : unit > proof


462 
restore_proof : proof > thm list


463 
\end{ttbox}


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


465 
type~\ttindex{proof}, and later restored.


466 


467 
\begin{description}


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


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


470 


471 
\item[\ttindexbold{restore_proof} {\it prf}]


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


473 
assumptions associated with the new proof.


474 
\end{description}


475 


476 


477 
\subsection{Debugging and inspecting}


478 
\index{proofs!debuggingbold}


479 
\index{debugging}


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


481 
to the current proof state of the subgoal module, and fail if there is no


482 
proof underway.


483 


484 
\subsubsection{Reading and printing terms}


485 
\index{reading!termsbold}\index{printing!terms}\index{printing!types}


486 
\begin{ttbox}


487 
read : string > term


488 
prin : term > unit


489 
printyp : typ > unit


490 
\end{ttbox}


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


492 
proof state.


493 


494 
\begin{description}


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


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


497 


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


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


500 


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


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


503 
\end{description}


504 


505 
\subsubsection{Inspecting the proof state}


506 
\index{proofs!inspecting the statebold}


507 
\begin{ttbox}


508 
topthm : unit > thm


509 
getgoal : int > term


510 
gethyps : int > thm list


511 
\end{ttbox}


512 


513 
\begin{description}


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


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


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


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


518 


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


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


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


522 
data structure in order to locate the problem!


523 


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


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


526 
theorems, the subgoal's parameters become free variables. This command is


527 
supplied for debugging uses of \ttindex{METAHYPS}.


528 
\end{description}


529 


530 
\subsubsection{Filtering lists of rules}


531 
\begin{ttbox}


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


533 
\end{ttbox}


534 


535 
\begin{description}


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


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


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


539 
\end{description}


540 


541 
\index{subgoal module)}


542 
\index{proofs)}
