2 \chapter{Proof Management: The Subgoal Module}
4 \index{subgoal module|(}
5 \index{reading!goals|see{proofs, starting}}
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
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.
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.
22 The subgoal module always contains some proof state. At the start of the
23 Isabelle session, this state consists of a dummy formula.
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}
31 \index{proofs!starting}
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
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
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
47 val prems = goal{\it theory\/ formula};
48 \end{ttbox}\index{assumptions!of main goal}
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
51 premises}. When the proof is finished, {\tt result} compares the
52 stored assumptions with the actual assumptions in the proof state.
54 \index{definitions!unfolding}
55 Some of the commands unfold definitions using meta-rewrite rules. This
56 expansion affects both the initial subgoal and the premises, which would
57 otherwise require use of {\tt rewrite_goals_tac} and
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}).
68 \item[\ttindexbold{goal} {\it theory} {\it formula};]
69 begins a new proof, where {\it theory} is usually an \ML\ identifier
70 and the {\it formula\/} is written as an \ML\ string.
72 \item[\ttindexbold{goalw} {\it theory} {\it defs} {\it formula};]
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.
75 \index{meta-rewriting}
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
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}
83 \item[\ttindexbold{premises}()]
84 returns the list of meta-hypotheses associated with the current proof (in
85 case you forgot to bind them to an \ML{} identifier).
89 \subsection{Applying a tactic}
90 \index{tactics!commands for applying}
93 byev : tactic list -> unit
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}).
99 \begin{ttdescription} \item[\ttindexbold{by} {\it tactic};]
100 applies the {\it tactic\/} to the proof state.
102 \item[\ttindexbold{byev} {\it tactics};]
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
108 \noindent{\it Error indications:}\nobreak
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.
120 \subsection{Extracting and storing the proved theorem}
121 \label{ExtractingAndStoringTheProvedTheorem}
122 \index{theorems!extracting proved}
125 uresult : unit -> thm
126 bind_thm : string * thm -> unit
129 \begin{ttdescription}
130 \item[\ttindexbold{result}()]\index{assumptions!of main goal}
131 returns the final theorem, after converting the free variables to
132 schematics. It discharges the assumptions supplied to the matching
135 It raises an exception unless the proof state passes certain checks. There
136 must be no assumptions other than those supplied to {\tt goal}. There
137 must be no subgoals. The theorem proved must be a (first-order) instance
138 of the original goal, as stated in the {\tt goal} command. This allows
139 {\bf answer extraction} --- instantiation of variables --- but no other
140 changes to the main goal. The theorem proved must have the same signature
141 as the initial proof state.
143 These checks are needed because an Isabelle tactic can return any proof
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.
152 \item[\ttindexbold{bind_thm}($name$, $thm$)]\index{theorems!storing of}
153 stores {\tt standard($thm$)} (see \S\ref{MiscellaneousForwardRules})
154 in Isabelle's theorem database and in the ML variable $name$. The
155 theorem can be retrieved from Isabelle's database by {\tt get_thm}
156 (see \S\ref{BasicOperationsOnTheories}).
158 \item[\ttindexbold{qed} $name$]
159 combines {\tt result} and {\tt bind_thm} in that it first uses {\tt
160 result()} to get the theorem and then stores it like {\tt bind_thm}.
164 \subsection{Retrieving theorems}
165 \index{theorems!retrieving}
167 The following functions retrieve theorems (together with their names) from
168 the theorem database. Hence they can only find theorems that have explicitly
169 been stored in the database using \ttindex{qed}, \ttindex{bind_thm} or
172 findI : int -> (string * thm) list
173 findE : int -> int -> (string * thm) list
174 findEs : int -> (string * thm) list
175 thms_containing : string list -> (string * thm) list
177 \begin{ttdescription}
178 \item[\ttindexbold{findI} $i$]\index{assumptions!of main goal}
179 returns all ``introduction rules'' applicable to subgoal $i$ --- all
180 theorems whose conclusion matches (rather than unifies with) subgoal
181 $i$. Useful in connection with {\tt resolve_tac}.
183 \item[\ttindexbold{findE} $n$ $i$] returns all ``elimination rules''
184 applicable to premise $n$ of subgoal $i$ --- all those theorems whose
185 first premise matches premise $n$ of subgoal $i$. Useful in connection with
186 {\tt eresolve_tac} and {\tt dresolve_tac}.
188 \item[\ttindexbold{findEs} $i$] returns all ``elimination rules'' applicable
189 to subgoal $i$ --- all those theorems whose first premise matches some
190 premise of subgoal $i$. Useful in connection with {\tt eresolve_tac} and
193 \item[\ttindexbold{thms_containing} $strings$] returns all theorems that
194 contain all of the constants in $strings$. Note that a few basic constants
195 like \verb$==>$ are ignored.
199 \subsection{Undoing and backtracking}
202 choplev : int -> unit
206 \begin{ttdescription}
207 \item[\ttindexbold{chop}();]
208 deletes the top level of the state list, cancelling the last \ttindex{by}
209 command. It provides a limited undo facility, and the {\tt undo} command
212 \item[\ttindexbold{choplev} {\it n};]
213 truncates the state list to level~{\it n}.
215 \item[\ttindexbold{back}();]
216 searches the state list for a non-empty branch point, starting from the top
217 level. The first one found becomes the current proof state --- the most
218 recent alternative branch is taken. This is a form of interactive
221 \item[\ttindexbold{undo}();]
222 cancels the most recent change to the proof state by the commands \ttindex{by},
223 {\tt chop}, {\tt choplev}, and~{\tt back}. It {\bf cannot}
224 cancel {\tt goal} or {\tt undo} itself. It can be repeated to
225 cancel a series of commands.
229 \noindent{\it Error indications for {\tt back}:}\par\nobreak
231 \item{\footnotesize\tt"Warning:\ same as previous choice at this level"}
232 means {\tt back} found a non-empty branch point, but that it contained
233 the same proof state as the current one.
234 \item{\footnotesize\tt "Warning:\ signature of proof state has changed"}
235 means the signature of the alternative proof state differs from that of
237 \item {\footnotesize\tt "back:\ no alternatives"} means {\tt back} could
238 find no alternative proof state.
241 \subsection{Printing the proof state}\label{sec:goals-printing}
242 \index{proof state!printing of}
246 goals_limit: int ref \hfill{\bf initially 10}
248 See also the printing control options described in
249 \S\ref{sec:printing-control}.
250 \begin{ttdescription}
251 \item[\ttindexbold{pr}();]
252 prints the current proof state.
254 \item[\ttindexbold{prlev} {\it n};]
255 prints the proof state at level {\it n}. This allows you to review the
256 previous steps of the proof.
258 \item[\ttindexbold{goals_limit} := {\it k};]
259 specifies~$k$ as the maximum number of subgoals to print.
264 \index{timing statistics}\index{proofs!timing}
266 proof_timing: bool ref \hfill{\bf initially false}
269 \begin{ttdescription}
270 \item[\ttindexbold{proof_timing} := true;]
271 makes the \ttindex{by} and \ttindex{prove_goal} commands display how much
272 processor time was spent. This information is compiler-dependent.
276 \section{Shortcuts for applying tactics}
277 \index{shortcuts!for {\tt by} commands}
278 These commands call \ttindex{by} with common tactics. Their chief purpose
279 is to minimise typing, although the scanning shortcuts are useful in their
280 own right. Chapter~\ref{tactics} explains the tactics themselves.
282 \subsection{Refining a given subgoal}
285 br : thm -> int -> unit
286 be : thm -> int -> unit
287 bd : thm -> int -> unit
288 brs : thm list -> int -> unit
289 bes : thm list -> int -> unit
290 bds : thm list -> int -> unit
293 \begin{ttdescription}
294 \item[\ttindexbold{ba} {\it i};]
295 performs \hbox{\tt by (assume_tac {\it i});}
297 \item[\ttindexbold{br} {\it thm} {\it i};]
298 performs \hbox{\tt by (resolve_tac [{\it thm}] {\it i});}
300 \item[\ttindexbold{be} {\it thm} {\it i};]
301 performs \hbox{\tt by (eresolve_tac [{\it thm}] {\it i});}
303 \item[\ttindexbold{bd} {\it thm} {\it i};]
304 performs \hbox{\tt by (dresolve_tac [{\it thm}] {\it i});}
306 \item[\ttindexbold{brs} {\it thms} {\it i};]
307 performs \hbox{\tt by (resolve_tac {\it thms} {\it i});}
309 \item[\ttindexbold{bes} {\it thms} {\it i};]
310 performs \hbox{\tt by (eresolve_tac {\it thms} {\it i});}
312 \item[\ttindexbold{bds} {\it thms} {\it i};]
313 performs \hbox{\tt by (dresolve_tac {\it thms} {\it i});}
317 \subsection{Scanning shortcuts}
318 These shortcuts scan for a suitable subgoal (starting from subgoal~1).
319 They refine the first subgoal for which the tactic succeeds. Thus, they
320 require less typing than {\tt br}, etc. They display the selected
321 subgoal's number; please watch this, for it may not be what you expect!
328 frs : thm list -> unit
329 fes : thm list -> unit
330 fds : thm list -> unit
333 \begin{ttdescription}
334 \item[\ttindexbold{fa}();]
335 solves some subgoal by assumption.
337 \item[\ttindexbold{fr} {\it thm};]
338 refines some subgoal using \hbox{\tt resolve_tac [{\it thm}]}
340 \item[\ttindexbold{fe} {\it thm};]
341 refines some subgoal using \hbox{\tt eresolve_tac [{\it thm}]}
343 \item[\ttindexbold{fd} {\it thm};]
344 refines some subgoal using \hbox{\tt dresolve_tac [{\it thm}]}
346 \item[\ttindexbold{frs} {\it thms};]
347 refines some subgoal using \hbox{\tt resolve_tac {\it thms}}
349 \item[\ttindexbold{fes} {\it thms};]
350 refines some subgoal using \hbox{\tt eresolve_tac {\it thms}}
352 \item[\ttindexbold{fds} {\it thms};]
353 refines some subgoal using \hbox{\tt dresolve_tac {\it thms}}
356 \subsection{Other shortcuts}
359 bws : thm list -> unit
360 ren : string -> int -> unit
362 \begin{ttdescription}
363 \item[\ttindexbold{bw} {\it def};]
364 performs \hbox{\tt by (rewrite_goals_tac [{\it def}]);}
365 It unfolds definitions in the subgoals (but not the main goal), by
366 meta-rewriting with the given definition.
367 \index{meta-rewriting}
369 \item[\ttindexbold{bws}]
370 is like {\tt bw} but takes a list of definitions.
372 \item[\ttindexbold{ren} {\it names} {\it i};]
373 performs \hbox{\tt by (rename_tac {\it names} {\it i});} it renames
374 parameters in subgoal~$i$. (Ignore the message {\footnotesize\tt Warning:\
375 same as previous level}.)
376 \index{parameters!renaming}
380 \section{Executing batch proofs}
381 \index{batch execution}
383 prove_goal : theory-> string->(thm list->tactic list)->thm
384 qed_goal : string->theory-> string->(thm list->tactic list)->unit
385 prove_goalw: theory->thm list->string->(thm list->tactic list)->thm
386 qed_goalw : string->theory->thm list->string->(thm list->tactic list)->unit
387 prove_goalw_cterm: thm list->Sign.cterm->(thm list->tactic list)->thm
389 These batch functions create an initial proof state, then apply a tactic to
390 it, yielding a sequence of final proof states. The head of the sequence is
391 returned, provided it is an instance of the theorem originally proposed.
392 The forms {\tt prove_goal}, {\tt prove_goalw} and {\tt prove_goalw_cterm}
393 are analogous to {\tt goal}, {\tt goalw} and {\tt goalw_cterm}.
395 The tactic is specified by a function from theorem lists to tactic lists.
396 The function is applied to the list of meta-assumptions taken from
397 the main goal. The resulting tactics are applied in sequence (using {\tt
398 EVERY}). For example, a proof consisting of the commands
400 val prems = goal {\it theory} {\it formula};
401 by \(tac@1\); \ldots by \(tac@n\);
402 val my_thm = result();
404 can be transformed to an expression as follows:
406 val my_thm = prove_goal {\it theory} {\it formula}
407 (fn prems=> [ \(tac@1\), \ldots, \(tac@n\) ]);
409 The methods perform identical processing of the initial {\it formula} and
410 the final proof state. But {\tt prove_goal} executes the tactic as a
411 atomic operation, bypassing the subgoal module; the current interactive
414 \begin{ttdescription}
415 \item[\ttindexbold{prove_goal} {\it theory} {\it formula} {\it tacsf};]
416 executes a proof of the {\it formula\/} in the given {\it theory}, using
417 the given tactic function.
419 \item[\ttindexbold{qed_goal} $name$ $theory$ $formula$ $tacsf$;]
420 acts like {\tt prove_goal} but also stores the resulting theorem in
421 Isabelle's theorem database and in the ML variable $name$ (see
422 \S\ref{ExtractingAndStoringTheProvedTheorem}).
424 \item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula}
425 {\it tacsf};]\index{meta-rewriting}
426 is like {\tt prove_goal} but also applies the list of {\it defs\/} as
427 meta-rewrite rules to the first subgoal and the premises.
429 \item[\ttindexbold{qed_goalw} $name$ $theory$ $defs$ $formula$ $tacsf$;]
430 is analogous to {\tt qed_goal}.
432 \item[\ttindexbold{prove_goalw_cterm} {\it theory} {\it defs} {\it ct}
434 is a version of {\tt prove_goalw} for programming applications. The main
435 goal is supplied as a cterm, not as a string. Typically, the cterm is
436 created from a term~$t$ as follows:
438 Sign.cterm_of (sign_of thy) \(t\)
440 \index{*Sign.cterm_of}\index{*sign_of}
444 \section{Managing multiple proofs}
445 \index{proofs!managing multiple}
446 You may save the current state of the subgoal module and resume work on it
447 later. This serves two purposes.
449 \item At some point, you may be uncertain of the next step, and
452 \item During a proof, you may see that a lemma should be proved first.
454 Each saved proof state consists of a list of levels; \ttindex{chop} behaves
455 independently for each of the saved proofs. In addition, each saved state
456 carries a separate \ttindex{undo} list.
458 \subsection{The stack of proof states}
459 \index{proofs!stacking}
461 push_proof : unit -> unit
462 pop_proof : unit -> thm list
463 rotate_proof : unit -> thm list
465 The subgoal module maintains a stack of proof states. Most subgoal
466 commands affect only the top of the stack. The \ttindex{goal} command {\em
467 replaces\/} the top of the stack; the only command that pushes a proof on the
468 stack is {\tt push_proof}.
470 To save some point of the proof, call {\tt push_proof}. You may now
471 state a lemma using {\tt goal}, or simply continue to apply tactics.
472 Later, you can return to the saved point by calling {\tt pop_proof} or
475 To view the entire stack, call {\tt rotate_proof} repeatedly; as it rotates
476 the stack, it prints the new top element.
478 \begin{ttdescription}
479 \item[\ttindexbold{push_proof}();]
480 duplicates the top element of the stack, pushing a copy of the current
481 proof state on to the stack.
483 \item[\ttindexbold{pop_proof}();]
484 discards the top element of the stack. It returns the list of
485 assumptions associated with the new proof; you should bind these to an
486 \ML\ identifier. They can also be obtained by calling \ttindex{premises}.
488 \item[\ttindexbold{rotate_proof}();]
489 \index{assumptions!of main goal}
490 rotates the stack, moving the top element to the bottom. It returns the
491 list of assumptions associated with the new proof.
495 \subsection{Saving and restoring proof states}
496 \index{proofs!saving and restoring}
498 save_proof : unit -> proof
499 restore_proof : proof -> thm list
501 States of the subgoal module may be saved as \ML\ values of
502 type~\mltydx{proof}, and later restored.
504 \begin{ttdescription}
505 \item[\ttindexbold{save_proof}();]
506 returns the current state, which is on top of the stack.
508 \item[\ttindexbold{restore_proof} {\it prf};]\index{assumptions!of main goal}
509 replaces the top of the stack by~{\it prf}. It returns the list of
510 assumptions associated with the new proof.
514 \section{Debugging and inspecting}
515 \index{tactics!debugging}
516 These specialized operations support the debugging of tactics. They refer
517 to the current proof state of the subgoal module.
519 \subsection{Reading and printing terms}
520 \index{terms!reading of}\index{terms!printing of}\index{types!printing of}
522 read : string -> term
524 printyp : typ -> unit
526 These read and print terms (or types) using the syntax associated with the
529 \begin{ttdescription}
530 \item[\ttindexbold{read} {\it string}]
531 reads the {\it string} as a term, without type checking.
533 \item[\ttindexbold{prin} {\it t};]
534 prints the term~$t$ at the terminal.
536 \item[\ttindexbold{printyp} {\it T};]
537 prints the type~$T$ at the terminal.
540 \subsection{Inspecting the proof state}
541 \index{proofs!inspecting the state}
544 getgoal : int -> term
545 gethyps : int -> thm list
548 \begin{ttdescription}
549 \item[\ttindexbold{topthm}()]
550 returns the proof state as an Isabelle theorem. This is what \ttindex{by}
551 would supply to a tactic at this point. It omits the post-processing of
552 \ttindex{result} and \ttindex{uresult}.
554 \item[\ttindexbold{getgoal} {\it i}]
555 returns subgoal~$i$ of the proof state, as a term. You may print
556 this using {\tt prin}, though you may have to examine the internal
557 data structure in order to locate the problem!
559 \item[\ttindexbold{gethyps} {\it i}]
560 returns the hypotheses of subgoal~$i$ as meta-level assumptions. In
561 these theorems, the subgoal's parameters become free variables. This
562 command is supplied for debugging uses of \ttindex{METAHYPS}.
565 \subsection{Filtering lists of rules}
567 filter_goal: (term*term->bool) -> thm list -> int -> thm list
570 \begin{ttdescription}
571 \item[\ttindexbold{filter_goal} {\it could} {\it ths} {\it i}]
572 applies \hbox{\tt filter_thms {\it could}} to subgoal~$i$ of the proof
573 state and returns the list of theorems that survive the filtering.
576 \index{subgoal module|)}