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 \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}.
30 \subsection{Starting a backward proof}
31 \index{proofs!starting}
33 Goal : string -> thm list
34 Goalw : thm list -> string -> thm list
35 goal : theory -> string -> thm list
36 goalw : theory -> thm list -> string -> thm list
37 goalw_cterm : thm list -> cterm -> thm list
38 premises : unit -> thm list
41 The goal commands start a new proof by setting the goal. They replace
42 the current state list by a new one consisting of the initial proof
43 state. They also empty the \ttindex{undo} list; this command cannot
46 They all return a list of meta-hypotheses taken from the main goal. If
47 this list is non-empty, bind its value to an \ML{} identifier by typing
50 val prems = goal{\it theory\/ formula};
51 \end{ttbox}\index{assumptions!of main goal}
52 These assumptions typically serve as the premises when you are
53 deriving a rule. They are also stored internally and can be retrieved
54 later by the function \texttt{premises}. When the proof is finished,
55 \texttt{qed} compares the stored assumptions with the actual
56 assumptions in the proof state.
58 The capital versions of \texttt{Goal} are the basic user level
59 commands and should be preferred over the more primitive lowercase
60 \texttt{goal} commands. Apart from taking the current theory context
61 as implicit argument, the former ones try to be smart in handling
62 meta-hypotheses when deriving rules. Thus \texttt{prems} have to be
63 seldom bound explicitly, the effect is as if \texttt{cut_facts_tac}
64 had been called automatically.
66 \index{definitions!unfolding}
67 Some of the commands unfold definitions using meta-rewrite rules. This
68 expansion affects both the initial subgoal and the premises, which would
69 otherwise require use of \texttt{rewrite_goals_tac} and
70 \texttt{rewrite_rule}.
73 \item[\ttindexbold{Goal} {\it formula};] begins a new proof, where
74 {\it formula\/} is written as an \ML\ string.
76 \item[\ttindexbold{Goalw} {\it defs} {\it formula};] is like
77 \texttt{Goal} but also applies the list of {\it defs\/} as
78 meta-rewrite rules to the first subgoal and the premises.
79 \index{meta-rewriting}
81 \item[\ttindexbold{goal} {\it theory} {\it formula};]
82 begins a new proof, where {\it theory} is usually an \ML\ identifier
83 and the {\it formula\/} is written as an \ML\ string.
85 \item[\ttindexbold{goalw} {\it theory} {\it defs} {\it formula};]
86 is like \texttt{goal} but also applies the list of {\it defs\/} as
87 meta-rewrite rules to the first subgoal and the premises.
88 \index{meta-rewriting}
90 \item[\ttindexbold{goalw_cterm} {\it theory} {\it defs} {\it ct};] is
91 a version of \texttt{goalw} for programming applications. The main
92 goal is supplied as a cterm, not as a string. Typically, the cterm
93 is created from a term~$t$ by \texttt{cterm_of (sign_of thy) $t$}.
94 \index{*cterm_of}\index{*sign_of}
96 \item[\ttindexbold{premises}()]
97 returns the list of meta-hypotheses associated with the current proof (in
98 case you forgot to bind them to an \ML{} identifier).
102 \subsection{Applying a tactic}
103 \index{tactics!commands for applying}
106 byev : tactic list -> unit
108 These commands extend the state list. They apply a tactic to the current
109 proof state. If the tactic succeeds, it returns a non-empty sequence of
110 next states. The head of the sequence becomes the next state, while the
111 tail is retained for backtracking (see~\texttt{back}).
112 \begin{ttdescription} \item[\ttindexbold{by} {\it tactic};]
113 applies the {\it tactic\/} to the proof state.
115 \item[\ttindexbold{byev} {\it tactics};]
116 applies the list of {\it tactics}, one at a time. It is useful for testing
117 calls to \texttt{prove_goal}, and abbreviates \texttt{by (EVERY {\it
121 \noindent{\it Error indications:}\nobreak
123 \item {\footnotesize\tt "by:\ tactic failed"} means that the tactic
124 returned an empty sequence when applied to the current proof state.
125 \item {\footnotesize\tt "Warning:\ same as previous level"} means that the
126 new proof state is identical to the previous state.
127 \item{\footnotesize\tt "Warning:\ signature of proof state has changed"}
128 means that some rule was applied whose theory is outside the theory of
129 the initial proof state. This could signify a mistake such as expressing
130 the goal in intuitionistic logic and proving it using classical logic.
133 \subsection{Extracting and storing the proved theorem}
134 \label{ExtractingAndStoringTheProvedTheorem}
135 \index{theorems!extracting proved}
139 uresult : unit -> thm
140 bind_thm : string * thm -> unit
141 store_thm : string * thm -> thm
143 \begin{ttdescription}
144 \item[\ttindexbold{qed} $name$;] is the usual way of ending a proof.
145 It combines \texttt{result} and \texttt{bind_thm}: it gets the theorem
146 using \texttt{result()} and stores it the theorem database associated
147 with its theory. See below for details.
149 \item[\ttindexbold{result}()]\index{assumptions!of main goal}
150 returns the final theorem, after converting the free variables to
151 schematics. It discharges the assumptions supplied to the matching
152 \texttt{goal} command.
154 It raises an exception unless the proof state passes certain checks. There
155 must be no assumptions other than those supplied to \texttt{goal}. There
156 must be no subgoals. The theorem proved must be a (first-order) instance
157 of the original goal, as stated in the \texttt{goal} command. This allows
158 {\bf answer extraction} --- instantiation of variables --- but no other
159 changes to the main goal. The theorem proved must have the same signature
160 as the initial proof state.
162 These checks are needed because an Isabelle tactic can return any proof
165 \item[\ttindexbold{uresult}()] is like \texttt{result()} but omits the checks.
166 It is needed when the initial goal contains function unknowns, when
167 definitions are unfolded in the main goal (by calling
168 \ttindex{rewrite_tac}),\index{definitions!unfolding} or when
169 \ttindex{assume_ax} has been used.
171 \item[\ttindexbold{bind_thm} ($name$, $thm$);]\index{theorems!storing}
172 stores \texttt{standard $thm$} (see \S\ref{MiscellaneousForwardRules})
173 in the theorem database associated with its theory and in the {\ML}
174 variable $name$. The theorem can be retrieved from the database
175 using \texttt{get_thm} (see \S\ref{BasicOperationsOnTheories}).
177 \item[\ttindexbold{store_thm} ($name$, $thm$)]\index{theorems!storing}
178 stores $thm$ in the theorem database associated with its theory and
179 returns that theorem.
183 \subsection{Extracting axioms and stored theorems}
184 \index{theories!axioms of}\index{axioms!extracting}
185 \index{theories!theorems of}\index{theorems!extracting}
188 thms : xstring -> thm list
189 get_axiom : theory -> xstring -> thm
190 get_thm : theory -> xstring -> thm
191 get_thms : theory -> xstring -> thm list
192 axioms_of : theory -> (string * thm) list
193 thms_of : theory -> (string * thm) list
194 assume_ax : theory -> string -> thm
196 \begin{ttdescription}
198 \item[\ttindexbold{thm} $name$] is the basic user function for
199 extracting stored theorems from the current theory context.
201 \item[\ttindexbold{thms} $name$] is like \texttt{thm}, but returns a
202 whole list associated with $name$ rather than a single theorem.
203 Typically this will be collections stored by packages, e.g.\
206 \item[\ttindexbold{get_axiom} $thy$ $name$] returns an axiom with the
207 given $name$ from $thy$ or any of its ancestors, raising exception
208 \xdx{THEORY} if none exists. Merging theories can cause several
209 axioms to have the same name; {\tt get_axiom} returns an arbitrary
210 one. Usually, axioms are also stored as theorems and may be
211 retrieved via \texttt{get_thm} as well.
213 \item[\ttindexbold{get_thm} $thy$ $name$] is analogous to {\tt
214 get_axiom}, but looks for a theorem stored in the theory's
215 database. Like {\tt get_axiom} it searches all parents of a theory
216 if the theorem is not found directly in $thy$.
218 \item[\ttindexbold{get_thms} $thy$ $name$] is like \texttt{get_thm}
219 for retrieving theorem lists stored within the theory. It returns a
220 singleton list if $name$ actually refers to a theorem rather than a
223 \item[\ttindexbold{axioms_of} $thy$] returns the axioms of this theory
224 node, not including the ones of its ancestors.
226 \item[\ttindexbold{thms_of} $thy$] returns all theorems stored within
227 the database of this theory node, not including the ones of its
230 \item[\ttindexbold{assume_ax} $thy$ $formula$] reads the {\it formula}
231 using the syntax of $thy$, following the same conventions as axioms
232 in a theory definition. You can thus pretend that {\it formula} is
233 an axiom and use the resulting theorem like an axiom. Actually {\tt
234 assume_ax} returns an assumption; \ttindex{qed} and
235 \ttindex{result} complain about additional assumptions, but
236 \ttindex{uresult} does not.
238 For example, if {\it formula} is
239 \hbox{\tt a=b ==> b=a} then the resulting theorem has the form
240 \hbox{\verb'?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]'}
244 \subsection{Retrieving theorems}
245 \index{theorems!retrieving}
247 The following functions retrieve theorems (together with their names)
248 from the theorem database that is associated with the current proof
249 state's theory. They can only find theorems that have explicitly been
250 stored in the database using \ttindex{qed}, \ttindex{bind_thm} or
253 findI : int -> (string * thm) list
254 findE : int -> int -> (string * thm) list
255 findEs : int -> (string * thm) list
256 thms_containing : xstring list -> (string * thm) list
258 \begin{ttdescription}
259 \item[\ttindexbold{findI} $i$]\index{assumptions!of main goal}
260 returns all ``introduction rules'' applicable to subgoal $i$ --- all
261 theorems whose conclusion matches (rather than unifies with) subgoal
262 $i$. Useful in connection with \texttt{resolve_tac}.
264 \item[\ttindexbold{findE} $n$ $i$] returns all ``elimination rules''
265 applicable to premise $n$ of subgoal $i$ --- all those theorems whose
266 first premise matches premise $n$ of subgoal $i$. Useful in connection with
267 \texttt{eresolve_tac} and \texttt{dresolve_tac}.
269 \item[\ttindexbold{findEs} $i$] returns all ``elimination rules'' applicable
270 to subgoal $i$ --- all those theorems whose first premise matches some
271 premise of subgoal $i$. Useful in connection with \texttt{eresolve_tac} and
272 \texttt{dresolve_tac}.
274 \item[\ttindexbold{thms_containing} $consts$] returns all theorems
275 that contain all of a given set of constants. Note that a few basic
276 constants like \verb$==>$ are ignored.
280 \subsection{Undoing and backtracking}
283 choplev : int -> unit
287 \begin{ttdescription}
288 \item[\ttindexbold{chop}();]
289 deletes the top level of the state list, cancelling the last \ttindex{by}
290 command. It provides a limited undo facility, and the \texttt{undo} command
293 \item[\ttindexbold{choplev} {\it n};]
294 truncates the state list to level~{\it n}, if $n\geq0$. A negative value
295 of~$n$ refers to the $n$th previous level:
296 \hbox{\verb|choplev ~1|} has the same effect as \texttt{chop}.
298 \item[\ttindexbold{back}();]
299 searches the state list for a non-empty branch point, starting from the top
300 level. The first one found becomes the current proof state --- the most
301 recent alternative branch is taken. This is a form of interactive
304 \item[\ttindexbold{undo}();]
305 cancels the most recent change to the proof state by the commands \ttindex{by},
306 \texttt{chop}, \texttt{choplev}, and~\texttt{back}. It {\bf cannot}
307 cancel \texttt{goal} or \texttt{undo} itself. It can be repeated to
308 cancel a series of commands.
312 \noindent{\it Error indications for \texttt{back}:}\par\nobreak
314 \item{\footnotesize\tt"Warning:\ same as previous choice at this level"}
315 means \texttt{back} found a non-empty branch point, but that it contained
316 the same proof state as the current one.
317 \item{\footnotesize\tt "Warning:\ signature of proof state has changed"}
318 means the signature of the alternative proof state differs from that of
320 \item {\footnotesize\tt "back:\ no alternatives"} means \texttt{back} could
321 find no alternative proof state.
324 \subsection{Printing the proof state}\label{sec:goals-printing}
325 \index{proof state!printing of}
330 goals_limit: int ref \hfill{\bf initially 10}
332 See also the printing control options described
333 in~\S\ref{sec:printing-control}.
334 \begin{ttdescription}
335 \item[\ttindexbold{pr}();]
336 prints the current proof state.
338 \item[\ttindexbold{prlev} {\it n};]
339 prints the proof state at level {\it n}, if $n\geq0$. A negative value
340 of~$n$ refers to the $n$th previous level. This command allows
341 you to review earlier stages of the proof.
343 \item[\ttindexbold{prlim} {\it k};]
344 prints the current proof state, limiting the number of subgoals to~$k$. It
345 updates \texttt{goals_limit} (see below) and is helpful when there are many
348 \item[\ttindexbold{goals_limit} := {\it k};]
349 specifies~$k$ as the maximum number of subgoals to print.
354 \index{timing statistics}\index{proofs!timing}
356 proof_timing: bool ref \hfill{\bf initially false}
359 \begin{ttdescription}
360 \item[set \ttindexbold{proof_timing};]
361 makes the \ttindex{by} and \ttindex{prove_goal} commands display how much
362 processor time was spent. This information is compiler-dependent.
366 \section{Shortcuts for applying tactics}
367 \index{shortcuts!for \texttt{by} commands}
368 These commands call \ttindex{by} with common tactics. Their chief purpose
369 is to minimise typing, although the scanning shortcuts are useful in their
370 own right. Chapter~\ref{tactics} explains the tactics themselves.
372 \subsection{Refining a given subgoal}
375 br : thm -> int -> unit
376 be : thm -> int -> unit
377 bd : thm -> int -> unit
378 brs : thm list -> int -> unit
379 bes : thm list -> int -> unit
380 bds : thm list -> int -> unit
383 \begin{ttdescription}
384 \item[\ttindexbold{ba} {\it i};]
385 performs \texttt{by (assume_tac {\it i});}
387 \item[\ttindexbold{br} {\it thm} {\it i};]
388 performs \texttt{by (resolve_tac [{\it thm}] {\it i});}
390 \item[\ttindexbold{be} {\it thm} {\it i};]
391 performs \texttt{by (eresolve_tac [{\it thm}] {\it i});}
393 \item[\ttindexbold{bd} {\it thm} {\it i};]
394 performs \texttt{by (dresolve_tac [{\it thm}] {\it i});}
396 \item[\ttindexbold{brs} {\it thms} {\it i};]
397 performs \texttt{by (resolve_tac {\it thms} {\it i});}
399 \item[\ttindexbold{bes} {\it thms} {\it i};]
400 performs \texttt{by (eresolve_tac {\it thms} {\it i});}
402 \item[\ttindexbold{bds} {\it thms} {\it i};]
403 performs \texttt{by (dresolve_tac {\it thms} {\it i});}
407 \subsection{Scanning shortcuts}
408 These shortcuts scan for a suitable subgoal (starting from subgoal~1).
409 They refine the first subgoal for which the tactic succeeds. Thus, they
410 require less typing than \texttt{br}, etc. They display the selected
411 subgoal's number; please watch this, for it may not be what you expect!
418 frs : thm list -> unit
419 fes : thm list -> unit
420 fds : thm list -> unit
423 \begin{ttdescription}
424 \item[\ttindexbold{fa}();]
425 solves some subgoal by assumption.
427 \item[\ttindexbold{fr} {\it thm};]
428 refines some subgoal using \texttt{resolve_tac [{\it thm}]}
430 \item[\ttindexbold{fe} {\it thm};]
431 refines some subgoal using \texttt{eresolve_tac [{\it thm}]}
433 \item[\ttindexbold{fd} {\it thm};]
434 refines some subgoal using \texttt{dresolve_tac [{\it thm}]}
436 \item[\ttindexbold{frs} {\it thms};]
437 refines some subgoal using \texttt{resolve_tac {\it thms}}
439 \item[\ttindexbold{fes} {\it thms};]
440 refines some subgoal using \texttt{eresolve_tac {\it thms}}
442 \item[\ttindexbold{fds} {\it thms};]
443 refines some subgoal using \texttt{dresolve_tac {\it thms}}
446 \subsection{Other shortcuts}
449 bws : thm list -> unit
450 ren : string -> int -> unit
452 \begin{ttdescription}
453 \item[\ttindexbold{bw} {\it def};] performs \texttt{by
454 (rewrite_goals_tac [{\it def}]);} It unfolds definitions in the
455 subgoals (but not the main goal), by meta-rewriting with the given
456 definition (see also \S\ref{sec:rewrite_goals}).
457 \index{meta-rewriting}
459 \item[\ttindexbold{bws}]
460 is like \texttt{bw} but takes a list of definitions.
462 \item[\ttindexbold{ren} {\it names} {\it i};]
463 performs \texttt{by (rename_tac {\it names} {\it i});} it renames
464 parameters in subgoal~$i$. (Ignore the message {\footnotesize\tt Warning:\
465 same as previous level}.)
466 \index{parameters!renaming}
470 \section{Executing batch proofs}
471 \index{batch execution}%
472 To save space below, let type \texttt{tacfun} abbreviate \texttt{thm list ->
473 tactic list}, which is the type of a tactical proof.
475 prove_goal : theory -> string -> tacfun -> thm
476 qed_goal : string -> theory -> string -> tacfun -> unit
477 prove_goalw: theory -> thm list -> string -> tacfun -> thm
478 qed_goalw : string -> theory -> thm list -> string -> tacfun -> unit
479 prove_goalw_cterm: thm list -> cterm -> tacfun -> thm
481 These batch functions create an initial proof state, then apply a tactic to
482 it, yielding a sequence of final proof states. The head of the sequence is
483 returned, provided it is an instance of the theorem originally proposed.
484 The forms \texttt{prove_goal}, \texttt{prove_goalw} and \texttt{prove_goalw_cterm}
485 are analogous to \texttt{goal}, \texttt{goalw} and \texttt{goalw_cterm}.
487 The tactic is specified by a function from theorem lists to tactic lists.
488 The function is applied to the list of meta-assumptions taken from
489 the main goal. The resulting tactics are applied in sequence (using {\tt
490 EVERY}). For example, a proof consisting of the commands
492 val prems = goal {\it theory} {\it formula};
493 by \(tac@1\); \ldots by \(tac@n\);
496 can be transformed to an expression as follows:
498 qed_goal "my_thm" {\it theory} {\it formula}
499 (fn prems=> [ \(tac@1\), \ldots, \(tac@n\) ]);
501 The methods perform identical processing of the initial {\it formula} and
502 the final proof state. But \texttt{prove_goal} executes the tactic as a
503 atomic operation, bypassing the subgoal module; the current interactive
506 \begin{ttdescription}
507 \item[\ttindexbold{prove_goal} {\it theory} {\it formula} {\it tacsf};]
508 executes a proof of the {\it formula\/} in the given {\it theory}, using
509 the given tactic function.
511 \item[\ttindexbold{qed_goal} $name$ $theory$ $formula$ $tacsf$;] acts
512 like \texttt{prove_goal} but also stores the resulting theorem in the
513 theorem database associated with its theory and in the {\ML}
514 variable $name$ (see \S\ref{ExtractingAndStoringTheProvedTheorem}).
516 \item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula}
517 {\it tacsf};]\index{meta-rewriting}
518 is like \texttt{prove_goal} but also applies the list of {\it defs\/} as
519 meta-rewrite rules to the first subgoal and the premises.
521 \item[\ttindexbold{qed_goalw} $name$ $theory$ $defs$ $formula$ $tacsf$;]
522 is analogous to \texttt{qed_goal}.
524 \item[\ttindexbold{prove_goalw_cterm} {\it theory} {\it defs} {\it ct}
526 is a version of \texttt{prove_goalw} for programming applications. The main
527 goal is supplied as a cterm, not as a string. Typically, the cterm is
528 created from a term~$t$ as follows:
530 cterm_of (sign_of thy) \(t\)
532 \index{*cterm_of}\index{*sign_of}
536 \section{Managing multiple proofs}
537 \index{proofs!managing multiple}
538 You may save the current state of the subgoal module and resume work on it
539 later. This serves two purposes.
541 \item At some point, you may be uncertain of the next step, and
544 \item During a proof, you may see that a lemma should be proved first.
546 Each saved proof state consists of a list of levels; \ttindex{chop} behaves
547 independently for each of the saved proofs. In addition, each saved state
548 carries a separate \ttindex{undo} list.
550 \subsection{The stack of proof states}
551 \index{proofs!stacking}
553 push_proof : unit -> unit
554 pop_proof : unit -> thm list
555 rotate_proof : unit -> thm list
557 The subgoal module maintains a stack of proof states. Most subgoal
558 commands affect only the top of the stack. The \ttindex{Goal} command {\em
559 replaces\/} the top of the stack; the only command that pushes a proof on the
560 stack is \texttt{push_proof}.
562 To save some point of the proof, call \texttt{push_proof}. You may now
563 state a lemma using \texttt{goal}, or simply continue to apply tactics.
564 Later, you can return to the saved point by calling \texttt{pop_proof} or
565 \texttt{rotate_proof}.
567 To view the entire stack, call \texttt{rotate_proof} repeatedly; as it rotates
568 the stack, it prints the new top element.
570 \begin{ttdescription}
571 \item[\ttindexbold{push_proof}();]
572 duplicates the top element of the stack, pushing a copy of the current
573 proof state on to the stack.
575 \item[\ttindexbold{pop_proof}();]
576 discards the top element of the stack. It returns the list of
577 assumptions associated with the new proof; you should bind these to an
578 \ML\ identifier. They can also be obtained by calling \ttindex{premises}.
580 \item[\ttindexbold{rotate_proof}();]
581 \index{assumptions!of main goal}
582 rotates the stack, moving the top element to the bottom. It returns the
583 list of assumptions associated with the new proof.
587 \subsection{Saving and restoring proof states}
588 \index{proofs!saving and restoring}
590 save_proof : unit -> proof
591 restore_proof : proof -> thm list
593 States of the subgoal module may be saved as \ML\ values of
594 type~\mltydx{proof}, and later restored.
596 \begin{ttdescription}
597 \item[\ttindexbold{save_proof}();]
598 returns the current state, which is on top of the stack.
600 \item[\ttindexbold{restore_proof} {\it prf};]\index{assumptions!of main goal}
601 replaces the top of the stack by~{\it prf}. It returns the list of
602 assumptions associated with the new proof.
606 \section{*Debugging and inspecting}
607 \index{tactics!debugging}
608 These functions can be useful when you are debugging a tactic. They refer
609 to the current proof state stored in the subgoal module. A tactic
610 should never call them; it should operate on the proof state supplied as its
613 \subsection{Reading and printing terms}
614 \index{terms!reading of}\index{terms!printing of}\index{types!printing of}
616 read : string -> term
618 printyp : typ -> unit
620 These read and print terms (or types) using the syntax associated with the
623 \begin{ttdescription}
624 \item[\ttindexbold{read} {\it string}]
625 reads the {\it string} as a term, without type-checking.
627 \item[\ttindexbold{prin} {\it t};]
628 prints the term~$t$ at the terminal.
630 \item[\ttindexbold{printyp} {\it T};]
631 prints the type~$T$ at the terminal.
634 \subsection{Inspecting the proof state}
635 \index{proofs!inspecting the state}
638 getgoal : int -> term
639 gethyps : int -> thm list
642 \begin{ttdescription}
643 \item[\ttindexbold{topthm}()]
644 returns the proof state as an Isabelle theorem. This is what \ttindex{by}
645 would supply to a tactic at this point. It omits the post-processing of
646 \ttindex{result} and \ttindex{uresult}.
648 \item[\ttindexbold{getgoal} {\it i}]
649 returns subgoal~$i$ of the proof state, as a term. You may print
650 this using \texttt{prin}, though you may have to examine the internal
651 data structure in order to locate the problem!
653 \item[\ttindexbold{gethyps} {\it i}]
654 returns the hypotheses of subgoal~$i$ as meta-level assumptions. In
655 these theorems, the subgoal's parameters become free variables. This
656 command is supplied for debugging uses of \ttindex{METAHYPS}.
660 \subsection{Filtering lists of rules}
662 filter_goal: (term*term->bool) -> thm list -> int -> thm list
665 \begin{ttdescription}
666 \item[\ttindexbold{filter_goal} {\it could} {\it ths} {\it i}]
667 applies \texttt{filter_thms {\it could}} to subgoal~$i$ of the proof
668 state and returns the list of theorems that survive the filtering.
671 \index{subgoal module|)}
677 %%% TeX-master: "ref"