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 defs} {\it ct};] is
91 a version of \texttt{goalw} intended for programming. The main
92 goal is supplied as a cterm, not as a string. See also
93 \texttt{prove_goalw_cterm}, \S\ref{sec:executing-batch}.
95 \item[\ttindexbold{premises}()]
96 returns the list of meta-hypotheses associated with the current proof (in
97 case you forgot to bind them to an \ML{} identifier).
101 \subsection{Applying a tactic}
102 \index{tactics!commands for applying}
105 byev : tactic list -> unit
107 These commands extend the state list. They apply a tactic to the current
108 proof state. If the tactic succeeds, it returns a non-empty sequence of
109 next states. The head of the sequence becomes the next state, while the
110 tail is retained for backtracking (see~\texttt{back}).
111 \begin{ttdescription} \item[\ttindexbold{by} {\it tactic};]
112 applies the {\it tactic\/} to the proof state.
114 \item[\ttindexbold{byev} {\it tactics};]
115 applies the list of {\it tactics}, one at a time. It is useful for testing
116 calls to \texttt{prove_goal}, and abbreviates \texttt{by (EVERY {\it
120 \noindent{\it Error indications:}\nobreak
122 \item {\footnotesize\tt "by:\ tactic failed"} means that the tactic
123 returned an empty sequence when applied to the current proof state.
124 \item {\footnotesize\tt "Warning:\ same as previous level"} means that the
125 new proof state is identical to the previous state.
126 \item{\footnotesize\tt "Warning:\ signature of proof state has changed"}
127 means that some rule was applied whose theory is outside the theory of
128 the initial proof state. This could signify a mistake such as expressing
129 the goal in intuitionistic logic and proving it using classical logic.
132 \subsection{Extracting and storing the proved theorem}
133 \label{ExtractingAndStoringTheProvedTheorem}
134 \index{theorems!extracting proved}
137 no_qed : unit -> unit
139 uresult : unit -> thm
140 bind_thm : string * thm -> unit
141 bind_thms : string * thm list -> unit
142 store_thm : string * thm -> thm
143 store_thms : string * thm list -> thm list
145 \begin{ttdescription}
146 \item[\ttindexbold{qed} $name$;] is the usual way of ending a proof.
147 It combines \texttt{result} and \texttt{bind_thm}: it gets the theorem
148 using \texttt{result()} and stores it the theorem database associated
149 with its theory. See below for details.
151 \item[\ttindexbold{no_qed}();] indicates that the proof is not concluded by a
152 proper \texttt{qed} command. This is a do-nothing operation, it merely
153 helps user interfaces such as Proof~General \cite{proofgeneral} to figure
154 out the structure of the {\ML} text.
156 \item[\ttindexbold{result}()]\index{assumptions!of main goal}
157 returns the final theorem, after converting the free variables to
158 schematics. It discharges the assumptions supplied to the matching
159 \texttt{goal} command.
161 It raises an exception unless the proof state passes certain checks. There
162 must be no assumptions other than those supplied to \texttt{goal}. There
163 must be no subgoals. The theorem proved must be a (first-order) instance
164 of the original goal, as stated in the \texttt{goal} command. This allows
165 {\bf answer extraction} --- instantiation of variables --- but no other
166 changes to the main goal. The theorem proved must have the same signature
167 as the initial proof state.
169 These checks are needed because an Isabelle tactic can return any proof
172 \item[\ttindexbold{uresult}()] is like \texttt{result()} but omits the checks.
173 It is needed when the initial goal contains function unknowns, when
174 definitions are unfolded in the main goal (by calling
175 \ttindex{rewrite_tac}),\index{definitions!unfolding} or when
176 \ttindex{assume_ax} has been used.
178 \item[\ttindexbold{bind_thm} ($name$, $thm$);]\index{theorems!storing}
179 stores \texttt{standard $thm$} (see \S\ref{MiscellaneousForwardRules})
180 in the theorem database associated with its theory and in the {\ML}
181 variable $name$. The theorem can be retrieved from the database
182 using \texttt{get_thm} (see \S\ref{BasicOperationsOnTheories}).
184 \item[\ttindexbold{store_thm} ($name$, $thm$)]\index{theorems!storing}
185 stores $thm$ in the theorem database associated with its theory and
186 returns that theorem.
188 \item[\ttindexbold{bind_thms} \textrm{and} \ttindexbold{store_thms}] are similar to
189 \texttt{bind_thm} and \texttt{store_thm}, but store lists of theorems.
193 The name argument of \texttt{qed}, \texttt{bind_thm} etc.\ may be the empty
194 string as well; in that case the result is \emph{not} stored, but proper
195 checks and presentation of the result still apply.
198 \subsection{Extracting axioms and stored theorems}
199 \index{theories!axioms of}\index{axioms!extracting}
200 \index{theories!theorems of}\index{theorems!extracting}
203 thms : xstring -> thm list
204 get_axiom : theory -> xstring -> thm
205 get_thm : theory -> xstring -> thm
206 get_thms : theory -> xstring -> thm list
207 axioms_of : theory -> (string * thm) list
208 thms_of : theory -> (string * thm) list
209 assume_ax : theory -> string -> thm
211 \begin{ttdescription}
213 \item[\ttindexbold{thm} $name$] is the basic user function for
214 extracting stored theorems from the current theory context.
216 \item[\ttindexbold{thms} $name$] is like \texttt{thm}, but returns a
217 whole list associated with $name$ rather than a single theorem.
218 Typically this will be collections stored by packages, e.g.\
221 \item[\ttindexbold{get_axiom} $thy$ $name$] returns an axiom with the
222 given $name$ from $thy$ or any of its ancestors, raising exception
223 \xdx{THEORY} if none exists. Merging theories can cause several
224 axioms to have the same name; {\tt get_axiom} returns an arbitrary
225 one. Usually, axioms are also stored as theorems and may be
226 retrieved via \texttt{get_thm} as well.
228 \item[\ttindexbold{get_thm} $thy$ $name$] is analogous to {\tt
229 get_axiom}, but looks for a theorem stored in the theory's
230 database. Like {\tt get_axiom} it searches all parents of a theory
231 if the theorem is not found directly in $thy$.
233 \item[\ttindexbold{get_thms} $thy$ $name$] is like \texttt{get_thm}
234 for retrieving theorem lists stored within the theory. It returns a
235 singleton list if $name$ actually refers to a theorem rather than a
238 \item[\ttindexbold{axioms_of} $thy$] returns the axioms of this theory
239 node, not including the ones of its ancestors.
241 \item[\ttindexbold{thms_of} $thy$] returns all theorems stored within
242 the database of this theory node, not including the ones of its
245 \item[\ttindexbold{assume_ax} $thy$ $formula$] reads the {\it formula}
246 using the syntax of $thy$, following the same conventions as axioms
247 in a theory definition. You can thus pretend that {\it formula} is
248 an axiom and use the resulting theorem like an axiom. Actually {\tt
249 assume_ax} returns an assumption; \ttindex{qed} and
250 \ttindex{result} complain about additional assumptions, but
251 \ttindex{uresult} does not.
253 For example, if {\it formula} is
254 \hbox{\tt a=b ==> b=a} then the resulting theorem has the form
255 \hbox{\verb'?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]'}
259 \subsection{Retrieving theorems}
260 \index{theorems!retrieving}
262 The following functions retrieve theorems (together with their names)
263 from the theorem database that is associated with the current proof
264 state's theory. They can only find theorems that have explicitly been
265 stored in the database using \ttindex{qed}, \ttindex{bind_thm} or
268 findI : int -> (string * thm) list
269 findE : int -> int -> (string * thm) list
270 findEs : int -> (string * thm) list
271 thms_containing : xstring list -> (string * thm) list
273 \begin{ttdescription}
274 \item[\ttindexbold{findI} $i$]\index{assumptions!of main goal}
275 returns all ``introduction rules'' applicable to subgoal $i$ --- all
276 theorems whose conclusion matches (rather than unifies with) subgoal
277 $i$. Useful in connection with \texttt{resolve_tac}.
279 \item[\ttindexbold{findE} $n$ $i$] returns all ``elimination rules''
280 applicable to premise $n$ of subgoal $i$ --- all those theorems whose
281 first premise matches premise $n$ of subgoal $i$. Useful in connection with
282 \texttt{eresolve_tac} and \texttt{dresolve_tac}.
284 \item[\ttindexbold{findEs} $i$] returns all ``elimination rules'' applicable
285 to subgoal $i$ --- all those theorems whose first premise matches some
286 premise of subgoal $i$. Useful in connection with \texttt{eresolve_tac} and
287 \texttt{dresolve_tac}.
289 \item[\ttindexbold{thms_containing} $consts$] returns all theorems that
290 contain \emph{all} of the given constants.
294 \subsection{Undoing and backtracking}
297 choplev : int -> unit
301 \begin{ttdescription}
302 \item[\ttindexbold{chop}();]
303 deletes the top level of the state list, cancelling the last \ttindex{by}
304 command. It provides a limited undo facility, and the \texttt{undo} command
307 \item[\ttindexbold{choplev} {\it n};]
308 truncates the state list to level~{\it n}, if $n\geq0$. A negative value
309 of~$n$ refers to the $n$th previous level:
310 \hbox{\verb|choplev ~1|} has the same effect as \texttt{chop}.
312 \item[\ttindexbold{back}();]
313 searches the state list for a non-empty branch point, starting from the top
314 level. The first one found becomes the current proof state --- the most
315 recent alternative branch is taken. This is a form of interactive
318 \item[\ttindexbold{undo}();]
319 cancels the most recent change to the proof state by the commands \ttindex{by},
320 \texttt{chop}, \texttt{choplev}, and~\texttt{back}. It {\bf cannot}
321 cancel \texttt{goal} or \texttt{undo} itself. It can be repeated to
322 cancel a series of commands.
326 \noindent{\it Error indications for {\tt back}:}\par\nobreak
328 \item{\footnotesize\tt"Warning:\ same as previous choice at this level"}
329 means \texttt{back} found a non-empty branch point, but that it contained
330 the same proof state as the current one.
331 \item{\footnotesize\tt "Warning:\ signature of proof state has changed"}
332 means the signature of the alternative proof state differs from that of
334 \item {\footnotesize\tt "back:\ no alternatives"} means \texttt{back} could
335 find no alternative proof state.
338 \subsection{Printing the proof state}\label{sec:goals-printing}
339 \index{proof state!printing of}
344 goals_limit: int ref \hfill{\bf initially 10}
346 See also the printing control options described
347 in~\S\ref{sec:printing-control}.
348 \begin{ttdescription}
349 \item[\ttindexbold{pr}();]
350 prints the current proof state.
352 \item[\ttindexbold{prlev} {\it n};]
353 prints the proof state at level {\it n}, if $n\geq0$. A negative value
354 of~$n$ refers to the $n$th previous level. This command allows
355 you to review earlier stages of the proof.
357 \item[\ttindexbold{prlim} {\it k};]
358 prints the current proof state, limiting the number of subgoals to~$k$. It
359 updates \texttt{goals_limit} (see below) and is helpful when there are many
362 \item[\ttindexbold{goals_limit} := {\it k};]
363 specifies~$k$ as the maximum number of subgoals to print.
368 \index{timing statistics}\index{proofs!timing}
370 timing: bool ref \hfill{\bf initially false}
373 \begin{ttdescription}
374 \item[set \ttindexbold{timing};] enables global timing in Isabelle. In
375 particular, this makes the \ttindex{by} and \ttindex{prove_goal} commands
376 display how much processor time was spent. This information is
381 \section{Shortcuts for applying tactics}
382 \index{shortcuts!for \texttt{by} commands}
383 These commands call \ttindex{by} with common tactics. Their chief purpose
384 is to minimise typing, although the scanning shortcuts are useful in their
385 own right. Chapter~\ref{tactics} explains the tactics themselves.
387 \subsection{Refining a given subgoal}
390 br : thm -> int -> unit
391 be : thm -> int -> unit
392 bd : thm -> int -> unit
393 brs : thm list -> int -> unit
394 bes : thm list -> int -> unit
395 bds : thm list -> int -> unit
398 \begin{ttdescription}
399 \item[\ttindexbold{ba} {\it i};]
400 performs \texttt{by (assume_tac {\it i});}
402 \item[\ttindexbold{br} {\it thm} {\it i};]
403 performs \texttt{by (resolve_tac [{\it thm}] {\it i});}
405 \item[\ttindexbold{be} {\it thm} {\it i};]
406 performs \texttt{by (eresolve_tac [{\it thm}] {\it i});}
408 \item[\ttindexbold{bd} {\it thm} {\it i};]
409 performs \texttt{by (dresolve_tac [{\it thm}] {\it i});}
411 \item[\ttindexbold{brs} {\it thms} {\it i};]
412 performs \texttt{by (resolve_tac {\it thms} {\it i});}
414 \item[\ttindexbold{bes} {\it thms} {\it i};]
415 performs \texttt{by (eresolve_tac {\it thms} {\it i});}
417 \item[\ttindexbold{bds} {\it thms} {\it i};]
418 performs \texttt{by (dresolve_tac {\it thms} {\it i});}
422 \subsection{Scanning shortcuts}
423 These shortcuts scan for a suitable subgoal (starting from subgoal~1).
424 They refine the first subgoal for which the tactic succeeds. Thus, they
425 require less typing than \texttt{br}, etc. They display the selected
426 subgoal's number; please watch this, for it may not be what you expect!
433 frs : thm list -> unit
434 fes : thm list -> unit
435 fds : thm list -> unit
438 \begin{ttdescription}
439 \item[\ttindexbold{fa}();]
440 solves some subgoal by assumption.
442 \item[\ttindexbold{fr} {\it thm};]
443 refines some subgoal using \texttt{resolve_tac [{\it thm}]}
445 \item[\ttindexbold{fe} {\it thm};]
446 refines some subgoal using \texttt{eresolve_tac [{\it thm}]}
448 \item[\ttindexbold{fd} {\it thm};]
449 refines some subgoal using \texttt{dresolve_tac [{\it thm}]}
451 \item[\ttindexbold{frs} {\it thms};]
452 refines some subgoal using \texttt{resolve_tac {\it thms}}
454 \item[\ttindexbold{fes} {\it thms};]
455 refines some subgoal using \texttt{eresolve_tac {\it thms}}
457 \item[\ttindexbold{fds} {\it thms};]
458 refines some subgoal using \texttt{dresolve_tac {\it thms}}
461 \subsection{Other shortcuts}
464 bws : thm list -> unit
465 ren : string -> int -> unit
467 \begin{ttdescription}
468 \item[\ttindexbold{bw} {\it def};] performs \texttt{by
469 (rewrite_goals_tac [{\it def}]);} It unfolds definitions in the
470 subgoals (but not the main goal), by meta-rewriting with the given
471 definition (see also \S\ref{sec:rewrite_goals}).
472 \index{meta-rewriting}
474 \item[\ttindexbold{bws}]
475 is like \texttt{bw} but takes a list of definitions.
477 \item[\ttindexbold{ren} {\it names} {\it i};]
478 performs \texttt{by (rename_tac {\it names} {\it i});} it renames
479 parameters in subgoal~$i$. (Ignore the message {\footnotesize\tt Warning:\
480 same as previous level}.)
481 \index{parameters!renaming}
485 \section{Executing batch proofs}\label{sec:executing-batch}
486 \index{batch execution}%
487 To save space below, let type \texttt{tacfn} abbreviate \texttt{thm list ->
488 tactic list}, which is the type of a tactical proof.
490 prove_goal : theory -> string -> tacfn -> thm
491 qed_goal : string -> theory -> string -> tacfn -> unit
492 prove_goalw: theory -> thm list -> string -> tacfn -> thm
493 qed_goalw : string -> theory -> thm list -> string -> tacfn -> unit
494 prove_goalw_cterm: thm list -> cterm -> tacfn -> thm
496 These batch functions create an initial proof state, then apply a tactic to
497 it, yielding a sequence of final proof states. The head of the sequence is
498 returned, provided it is an instance of the theorem originally proposed.
499 The forms \texttt{prove_goal}, \texttt{prove_goalw} and
500 \texttt{prove_goalw_cterm} are analogous to \texttt{goal}, \texttt{goalw} and
501 \texttt{goalw_cterm}.
503 The tactic is specified by a function from theorem lists to tactic lists.
504 The function is applied to the list of meta-assumptions taken from
505 the main goal. The resulting tactics are applied in sequence (using {\tt
506 EVERY}). For example, a proof consisting of the commands
508 val prems = goal {\it theory} {\it formula};
509 by \(tac@1\); \ldots by \(tac@n\);
512 can be transformed to an expression as follows:
514 qed_goal "my_thm" {\it theory} {\it formula}
515 (fn prems=> [ \(tac@1\), \ldots, \(tac@n\) ]);
517 The methods perform identical processing of the initial {\it formula} and
518 the final proof state. But \texttt{prove_goal} executes the tactic as a
519 atomic operation, bypassing the subgoal module; the current interactive
522 \begin{ttdescription}
523 \item[\ttindexbold{prove_goal} {\it theory} {\it formula} {\it tacsf};]
524 executes a proof of the {\it formula\/} in the given {\it theory}, using
525 the given tactic function.
527 \item[\ttindexbold{qed_goal} $name$ $theory$ $formula$ $tacsf$;] acts
528 like \texttt{prove_goal} but it also stores the resulting theorem in the
529 theorem database associated with its theory and in the {\ML}
530 variable $name$ (see \S\ref{ExtractingAndStoringTheProvedTheorem}).
532 \item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula}
533 {\it tacsf};]\index{meta-rewriting}
534 is like \texttt{prove_goal} but also applies the list of {\it defs\/} as
535 meta-rewrite rules to the first subgoal and the premises.
537 \item[\ttindexbold{qed_goalw} $name$ $theory$ $defs$ $formula$ $tacsf$;]
538 is analogous to \texttt{qed_goal}.
540 \item[\ttindexbold{prove_goalw_cterm} {\it defs} {\it ct}
542 is a version of \texttt{prove_goalw} intended for programming. The main
543 goal is supplied as a cterm, not as a string. A cterm carries a theory with
544 it, and can be created from a term~$t$ by
546 cterm_of (sign_of thy) \(t\)
548 \index{*cterm_of}\index{*sign_of}
552 \section{Managing multiple proofs}
553 \index{proofs!managing multiple}
554 You may save the current state of the subgoal module and resume work on it
555 later. This serves two purposes.
557 \item At some point, you may be uncertain of the next step, and
560 \item During a proof, you may see that a lemma should be proved first.
562 Each saved proof state consists of a list of levels; \ttindex{chop} behaves
563 independently for each of the saved proofs. In addition, each saved state
564 carries a separate \ttindex{undo} list.
566 \subsection{The stack of proof states}
567 \index{proofs!stacking}
569 push_proof : unit -> unit
570 pop_proof : unit -> thm list
571 rotate_proof : unit -> thm list
573 The subgoal module maintains a stack of proof states. Most subgoal
574 commands affect only the top of the stack. The \ttindex{Goal} command {\em
575 replaces\/} the top of the stack; the only command that pushes a proof on the
576 stack is \texttt{push_proof}.
578 To save some point of the proof, call \texttt{push_proof}. You may now
579 state a lemma using \texttt{goal}, or simply continue to apply tactics.
580 Later, you can return to the saved point by calling \texttt{pop_proof} or
581 \texttt{rotate_proof}.
583 To view the entire stack, call \texttt{rotate_proof} repeatedly; as it rotates
584 the stack, it prints the new top element.
586 \begin{ttdescription}
587 \item[\ttindexbold{push_proof}();]
588 duplicates the top element of the stack, pushing a copy of the current
589 proof state on to the stack.
591 \item[\ttindexbold{pop_proof}();]
592 discards the top element of the stack. It returns the list of
593 assumptions associated with the new proof; you should bind these to an
594 \ML\ identifier. They can also be obtained by calling \ttindex{premises}.
596 \item[\ttindexbold{rotate_proof}();]
597 \index{assumptions!of main goal}
598 rotates the stack, moving the top element to the bottom. It returns the
599 list of assumptions associated with the new proof.
603 \subsection{Saving and restoring proof states}
604 \index{proofs!saving and restoring}
606 save_proof : unit -> proof
607 restore_proof : proof -> thm list
609 States of the subgoal module may be saved as \ML\ values of
610 type~\mltydx{proof}, and later restored.
612 \begin{ttdescription}
613 \item[\ttindexbold{save_proof}();]
614 returns the current state, which is on top of the stack.
616 \item[\ttindexbold{restore_proof} {\it prf};]\index{assumptions!of main goal}
617 replaces the top of the stack by~{\it prf}. It returns the list of
618 assumptions associated with the new proof.
622 \section{*Debugging and inspecting}
623 \index{tactics!debugging}
624 These functions can be useful when you are debugging a tactic. They refer
625 to the current proof state stored in the subgoal module. A tactic
626 should never call them; it should operate on the proof state supplied as its
629 \subsection{Reading and printing terms}
630 \index{terms!reading of}\index{terms!printing of}\index{types!printing of}
632 read : string -> term
634 printyp : typ -> unit
636 These read and print terms (or types) using the syntax associated with the
639 \begin{ttdescription}
640 \item[\ttindexbold{read} {\it string}]
641 reads the {\it string} as a term, without type-checking.
643 \item[\ttindexbold{prin} {\it t};]
644 prints the term~$t$ at the terminal.
646 \item[\ttindexbold{printyp} {\it T};]
647 prints the type~$T$ at the terminal.
650 \subsection{Inspecting the proof state}
651 \index{proofs!inspecting the state}
654 getgoal : int -> term
655 gethyps : int -> thm list
658 \begin{ttdescription}
659 \item[\ttindexbold{topthm}()]
660 returns the proof state as an Isabelle theorem. This is what \ttindex{by}
661 would supply to a tactic at this point. It omits the post-processing of
662 \ttindex{result} and \ttindex{uresult}.
664 \item[\ttindexbold{getgoal} {\it i}]
665 returns subgoal~$i$ of the proof state, as a term. You may print
666 this using \texttt{prin}, though you may have to examine the internal
667 data structure in order to locate the problem!
669 \item[\ttindexbold{gethyps} {\it i}]
670 returns the hypotheses of subgoal~$i$ as meta-level assumptions. In
671 these theorems, the subgoal's parameters become free variables. This
672 command is supplied for debugging uses of \ttindex{METAHYPS}.
676 \subsection{Filtering lists of rules}
678 filter_goal: (term*term->bool) -> thm list -> int -> thm list
681 \begin{ttdescription}
682 \item[\ttindexbold{filter_goal} {\it could} {\it ths} {\it i}]
683 applies \texttt{filter_thms {\it could}} to subgoal~$i$ of the proof
684 state and returns the list of theorems that survive the filtering.
687 \index{subgoal module|)}
693 %%% TeX-master: "ref"