summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Ref/goals.tex

author | nipkow |

Wed, 04 Aug 2004 11:25:08 +0200 | |

changeset 15106 | e8cef6993701 |

parent 13479 | 7123ae179212 |

permissions | -rw-r--r-- |

aded comment

%% $Id$ \chapter{Proof Management: The Subgoal Module} \index{proofs|(} \index{subgoal module|(} \index{reading!goals|see{proofs, starting}} The subgoal module stores the current proof state\index{proof state} and many previous states; commands can produce new states or return to previous ones. The {\em state list\/} at level $n$ is a list of pairs \[ [(\psi@n,\Psi@n),\; (\psi@{n-1},\Psi@{n-1}),\; \ldots,\; (\psi@0,[])] \] where $\psi@n$ is the current proof state, $\psi@{n-1}$ is the previous one, \ldots, and $\psi@0$ is the initial proof state. The $\Psi@i$ are sequences (lazy lists) of proof states, storing branch points where a tactic returned a list longer than one. The state lists permit various forms of backtracking. Chopping elements from the state list reverts to previous proof states. Besides this, the \ttindex{undo} command keeps a list of state lists. The module actually maintains a stack of state lists, to support several proofs at the same time. The subgoal module always contains some proof state. At the start of the Isabelle session, this state consists of a dummy formula. \section{Basic commands} Most proofs begin with \texttt{Goal} or \texttt{Goalw} and require no other commands than \texttt{by}, \texttt{chop} and \texttt{undo}. They typically end with a call to \texttt{qed}. \subsection{Starting a backward proof} \index{proofs!starting} \begin{ttbox} Goal : string -> thm list Goalw : thm list -> string -> thm list goal : theory -> string -> thm list goalw : theory -> thm list -> string -> thm list goalw_cterm : thm list -> cterm -> thm list premises : unit -> thm list \end{ttbox} The goal commands start a new proof by setting the goal. They replace the current state list by a new one consisting of the initial proof state. They also empty the \ttindex{undo} list; this command cannot be undone! They all return a list of meta-hypotheses taken from the main goal. If this list is non-empty, bind its value to an \ML{} identifier by typing something like \begin{ttbox} val prems = goal{\it theory\/ formula}; \end{ttbox}\index{assumptions!of main goal} These assumptions typically serve as the premises when you are deriving a rule. They are also stored internally and can be retrieved later by the function \texttt{premises}. When the proof is finished, \texttt{qed} compares the stored assumptions with the actual assumptions in the proof state. The capital versions of \texttt{Goal} are the basic user level commands and should be preferred over the more primitive lowercase \texttt{goal} commands. Apart from taking the current theory context as implicit argument, the former ones try to be smart in handling meta-hypotheses when deriving rules. Thus \texttt{prems} have to be seldom bound explicitly, the effect is as if \texttt{cut_facts_tac} had been called automatically. \index{definitions!unfolding} Some of the commands unfold definitions using meta-rewrite rules. This expansion affects both the initial subgoal and the premises, which would otherwise require use of \texttt{rewrite_goals_tac} and \texttt{rewrite_rule}. \begin{ttdescription} \item[\ttindexbold{Goal} {\it formula};] begins a new proof, where {\it formula\/} is written as an \ML\ string. \item[\ttindexbold{Goalw} {\it defs} {\it formula};] is like \texttt{Goal} but also applies the list of {\it defs\/} as meta-rewrite rules to the first subgoal and the premises. \index{meta-rewriting} \item[\ttindexbold{goal} {\it theory} {\it formula};] begins a new proof, where {\it theory} is usually an \ML\ identifier and the {\it formula\/} is written as an \ML\ string. \item[\ttindexbold{goalw} {\it theory} {\it defs} {\it formula};] is like \texttt{goal} but also applies the list of {\it defs\/} as meta-rewrite rules to the first subgoal and the premises. \index{meta-rewriting} \item[\ttindexbold{goalw_cterm} {\it defs} {\it ct};] is a version of \texttt{goalw} intended for programming. The main goal is supplied as a cterm, not as a string. See also \texttt{prove_goalw_cterm}, \S\ref{sec:executing-batch}. \item[\ttindexbold{premises}()] returns the list of meta-hypotheses associated with the current proof (in case you forgot to bind them to an \ML{} identifier). \end{ttdescription} \subsection{Applying a tactic} \index{tactics!commands for applying} \begin{ttbox} by : tactic -> unit byev : tactic list -> unit \end{ttbox} These commands extend the state list. They apply a tactic to the current proof state. If the tactic succeeds, it returns a non-empty sequence of next states. The head of the sequence becomes the next state, while the tail is retained for backtracking (see~\texttt{back}). \begin{ttdescription} \item[\ttindexbold{by} {\it tactic};] applies the {\it tactic\/} to the proof state. \item[\ttindexbold{byev} {\it tactics};] applies the list of {\it tactics}, one at a time. It is useful for testing calls to \texttt{prove_goal}, and abbreviates \texttt{by (EVERY {\it tactics})}. \end{ttdescription} \noindent{\it Error indications:}\nobreak \begin{itemize} \item {\footnotesize\tt "by:\ tactic failed"} means that the tactic returned an empty sequence when applied to the current proof state. \item {\footnotesize\tt "Warning:\ same as previous level"} means that the new proof state is identical to the previous state. \item{\footnotesize\tt "Warning:\ signature of proof state has changed"} means that some rule was applied whose theory is outside the theory of the initial proof state. This could signify a mistake such as expressing the goal in intuitionistic logic and proving it using classical logic. \end{itemize} \subsection{Extracting and storing the proved theorem} \label{ExtractingAndStoringTheProvedTheorem} \index{theorems!extracting proved} \begin{ttbox} qed : string -> unit no_qed : unit -> unit result : unit -> thm uresult : unit -> thm bind_thm : string * thm -> unit bind_thms : string * thm list -> unit store_thm : string * thm -> thm store_thms : string * thm list -> thm list \end{ttbox} \begin{ttdescription} \item[\ttindexbold{qed} $name$;] is the usual way of ending a proof. It combines \texttt{result} and \texttt{bind_thm}: it gets the theorem using \texttt{result()} and stores it the theorem database associated with its theory. See below for details. \item[\ttindexbold{no_qed}();] indicates that the proof is not concluded by a proper \texttt{qed} command. This is a do-nothing operation, it merely helps user interfaces such as Proof~General \cite{proofgeneral} to figure out the structure of the {\ML} text. \item[\ttindexbold{result}()]\index{assumptions!of main goal} returns the final theorem, after converting the free variables to schematics. It discharges the assumptions supplied to the matching \texttt{goal} command. It raises an exception unless the proof state passes certain checks. There must be no assumptions other than those supplied to \texttt{goal}. There must be no subgoals. The theorem proved must be a (first-order) instance of the original goal, as stated in the \texttt{goal} command. This allows {\bf answer extraction} --- instantiation of variables --- but no other changes to the main goal. The theorem proved must have the same signature as the initial proof state. These checks are needed because an Isabelle tactic can return any proof state at all. \item[\ttindexbold{uresult}()] is like \texttt{result()} but omits the checks. It is needed when the initial goal contains function unknowns, when definitions are unfolded in the main goal (by calling \ttindex{rewrite_tac}),\index{definitions!unfolding} or when \ttindex{assume_ax} has been used. \item[\ttindexbold{bind_thm} ($name$, $thm$);]\index{theorems!storing} stores \texttt{standard $thm$} (see \S\ref{MiscellaneousForwardRules}) in the theorem database associated with its theory and in the {\ML} variable $name$. The theorem can be retrieved from the database using \texttt{get_thm} (see \S\ref{BasicOperationsOnTheories}). \item[\ttindexbold{store_thm} ($name$, $thm$)]\index{theorems!storing} stores $thm$ in the theorem database associated with its theory and returns that theorem. \item[\ttindexbold{bind_thms} \textrm{and} \ttindexbold{store_thms}] are similar to \texttt{bind_thm} and \texttt{store_thm}, but store lists of theorems. \end{ttdescription} The name argument of \texttt{qed}, \texttt{bind_thm} etc.\ may be the empty string as well; in that case the result is \emph{not} stored, but proper checks and presentation of the result still apply. \subsection{Extracting axioms and stored theorems} \index{theories!axioms of}\index{axioms!extracting} \index{theories!theorems of}\index{theorems!extracting} \begin{ttbox} thm : xstring -> thm thms : xstring -> thm list get_axiom : theory -> xstring -> thm get_thm : theory -> xstring -> thm get_thms : theory -> xstring -> thm list axioms_of : theory -> (string * thm) list thms_of : theory -> (string * thm) list assume_ax : theory -> string -> thm \end{ttbox} \begin{ttdescription} \item[\ttindexbold{thm} $name$] is the basic user function for extracting stored theorems from the current theory context. \item[\ttindexbold{thms} $name$] is like \texttt{thm}, but returns a whole list associated with $name$ rather than a single theorem. Typically this will be collections stored by packages, e.g.\ \verb|list.simps|. \item[\ttindexbold{get_axiom} $thy$ $name$] returns an axiom with the given $name$ from $thy$ or any of its ancestors, raising exception \xdx{THEORY} if none exists. Merging theories can cause several axioms to have the same name; {\tt get_axiom} returns an arbitrary one. Usually, axioms are also stored as theorems and may be retrieved via \texttt{get_thm} as well. \item[\ttindexbold{get_thm} $thy$ $name$] is analogous to {\tt get_axiom}, but looks for a theorem stored in the theory's database. Like {\tt get_axiom} it searches all parents of a theory if the theorem is not found directly in $thy$. \item[\ttindexbold{get_thms} $thy$ $name$] is like \texttt{get_thm} for retrieving theorem lists stored within the theory. It returns a singleton list if $name$ actually refers to a theorem rather than a theorem list. \item[\ttindexbold{axioms_of} $thy$] returns the axioms of this theory node, not including the ones of its ancestors. \item[\ttindexbold{thms_of} $thy$] returns all theorems stored within the database of this theory node, not including the ones of its ancestors. \item[\ttindexbold{assume_ax} $thy$ $formula$] reads the {\it formula} using the syntax of $thy$, following the same conventions as axioms in a theory definition. You can thus pretend that {\it formula} is an axiom and use the resulting theorem like an axiom. Actually {\tt assume_ax} returns an assumption; \ttindex{qed} and \ttindex{result} complain about additional assumptions, but \ttindex{uresult} does not. For example, if {\it formula} is \hbox{\tt a=b ==> b=a} then the resulting theorem has the form \hbox{\verb'?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]'} \end{ttdescription} \subsection{Retrieving theorems} \index{theorems!retrieving} The following functions retrieve theorems (together with their names) from the theorem database that is associated with the current proof state's theory. They can only find theorems that have explicitly been stored in the database using \ttindex{qed}, \ttindex{bind_thm} or related functions. \begin{ttbox} findI : int -> (string * thm) list findE : int -> int -> (string * thm) list findEs : int -> (string * thm) list thms_containing : xstring list -> (string * thm) list \end{ttbox} \begin{ttdescription} \item[\ttindexbold{findI} $i$]\index{assumptions!of main goal} returns all ``introduction rules'' applicable to subgoal $i$ --- all theorems whose conclusion matches (rather than unifies with) subgoal $i$. Useful in connection with \texttt{resolve_tac}. \item[\ttindexbold{findE} $n$ $i$] returns all ``elimination rules'' applicable to premise $n$ of subgoal $i$ --- all those theorems whose first premise matches premise $n$ of subgoal $i$. Useful in connection with \texttt{eresolve_tac} and \texttt{dresolve_tac}. \item[\ttindexbold{findEs} $i$] returns all ``elimination rules'' applicable to subgoal $i$ --- all those theorems whose first premise matches some premise of subgoal $i$. Useful in connection with \texttt{eresolve_tac} and \texttt{dresolve_tac}. \item[\ttindexbold{thms_containing} $consts$] returns all theorems that contain \emph{all} of the given constants. \end{ttdescription} \subsection{Undoing and backtracking} \begin{ttbox} chop : unit -> unit choplev : int -> unit back : unit -> unit undo : unit -> unit \end{ttbox} \begin{ttdescription} \item[\ttindexbold{chop}();] deletes the top level of the state list, cancelling the last \ttindex{by} command. It provides a limited undo facility, and the \texttt{undo} command can cancel it. \item[\ttindexbold{choplev} {\it n};] truncates the state list to level~{\it n}, if $n\geq0$. A negative value of~$n$ refers to the $n$th previous level: \hbox{\verb|choplev ~1|} has the same effect as \texttt{chop}. \item[\ttindexbold{back}();] searches the state list for a non-empty branch point, starting from the top level. The first one found becomes the current proof state --- the most recent alternative branch is taken. This is a form of interactive backtracking. \item[\ttindexbold{undo}();] cancels the most recent change to the proof state by the commands \ttindex{by}, \texttt{chop}, \texttt{choplev}, and~\texttt{back}. It {\bf cannot} cancel \texttt{goal} or \texttt{undo} itself. It can be repeated to cancel a series of commands. \end{ttdescription} \goodbreak \noindent{\it Error indications for {\tt back}:}\par\nobreak \begin{itemize} \item{\footnotesize\tt"Warning:\ same as previous choice at this level"} means \texttt{back} found a non-empty branch point, but that it contained the same proof state as the current one. \item{\footnotesize\tt "Warning:\ signature of proof state has changed"} means the signature of the alternative proof state differs from that of the current state. \item {\footnotesize\tt "back:\ no alternatives"} means \texttt{back} could find no alternative proof state. \end{itemize} \subsection{Printing the proof state}\label{sec:goals-printing} \index{proof state!printing of} \begin{ttbox} pr : unit -> unit prlev : int -> unit prlim : int -> unit goals_limit: int ref \hfill{\bf initially 10} \end{ttbox} See also the printing control options described in~\S\ref{sec:printing-control}. \begin{ttdescription} \item[\ttindexbold{pr}();] prints the current proof state. \item[\ttindexbold{prlev} {\it n};] prints the proof state at level {\it n}, if $n\geq0$. A negative value of~$n$ refers to the $n$th previous level. This command allows you to review earlier stages of the proof. \item[\ttindexbold{prlim} {\it k};] prints the current proof state, limiting the number of subgoals to~$k$. It updates \texttt{goals_limit} (see below) and is helpful when there are many subgoals. \item[\ttindexbold{goals_limit} := {\it k};] specifies~$k$ as the maximum number of subgoals to print. \end{ttdescription} \subsection{Timing} \index{timing statistics}\index{proofs!timing} \begin{ttbox} timing: bool ref \hfill{\bf initially false} \end{ttbox} \begin{ttdescription} \item[set \ttindexbold{timing};] enables global timing in Isabelle. In particular, this makes the \ttindex{by} and \ttindex{prove_goal} commands display how much processor time was spent. This information is compiler-dependent. \end{ttdescription} \section{Shortcuts for applying tactics} \index{shortcuts!for \texttt{by} commands} These commands call \ttindex{by} with common tactics. Their chief purpose is to minimise typing, although the scanning shortcuts are useful in their own right. Chapter~\ref{tactics} explains the tactics themselves. \subsection{Refining a given subgoal} \begin{ttbox} ba : int -> unit br : thm -> int -> unit be : thm -> int -> unit bd : thm -> int -> unit brs : thm list -> int -> unit bes : thm list -> int -> unit bds : thm list -> int -> unit \end{ttbox} \begin{ttdescription} \item[\ttindexbold{ba} {\it i};] performs \texttt{by (assume_tac {\it i});} \item[\ttindexbold{br} {\it thm} {\it i};] performs \texttt{by (resolve_tac [{\it thm}] {\it i});} \item[\ttindexbold{be} {\it thm} {\it i};] performs \texttt{by (eresolve_tac [{\it thm}] {\it i});} \item[\ttindexbold{bd} {\it thm} {\it i};] performs \texttt{by (dresolve_tac [{\it thm}] {\it i});} \item[\ttindexbold{brs} {\it thms} {\it i};] performs \texttt{by (resolve_tac {\it thms} {\it i});} \item[\ttindexbold{bes} {\it thms} {\it i};] performs \texttt{by (eresolve_tac {\it thms} {\it i});} \item[\ttindexbold{bds} {\it thms} {\it i};] performs \texttt{by (dresolve_tac {\it thms} {\it i});} \end{ttdescription} \subsection{Scanning shortcuts} These shortcuts scan for a suitable subgoal (starting from subgoal~1). They refine the first subgoal for which the tactic succeeds. Thus, they require less typing than \texttt{br}, etc. They display the selected subgoal's number; please watch this, for it may not be what you expect! \begin{ttbox} fa : unit -> unit fr : thm -> unit fe : thm -> unit fd : thm -> unit frs : thm list -> unit fes : thm list -> unit fds : thm list -> unit \end{ttbox} \begin{ttdescription} \item[\ttindexbold{fa}();] solves some subgoal by assumption. \item[\ttindexbold{fr} {\it thm};] refines some subgoal using \texttt{resolve_tac [{\it thm}]} \item[\ttindexbold{fe} {\it thm};] refines some subgoal using \texttt{eresolve_tac [{\it thm}]} \item[\ttindexbold{fd} {\it thm};] refines some subgoal using \texttt{dresolve_tac [{\it thm}]} \item[\ttindexbold{frs} {\it thms};] refines some subgoal using \texttt{resolve_tac {\it thms}} \item[\ttindexbold{fes} {\it thms};] refines some subgoal using \texttt{eresolve_tac {\it thms}} \item[\ttindexbold{fds} {\it thms};] refines some subgoal using \texttt{dresolve_tac {\it thms}} \end{ttdescription} \subsection{Other shortcuts} \begin{ttbox} bw : thm -> unit bws : thm list -> unit ren : string -> int -> unit \end{ttbox} \begin{ttdescription} \item[\ttindexbold{bw} {\it def};] performs \texttt{by (rewrite_goals_tac [{\it def}]);} It unfolds definitions in the subgoals (but not the main goal), by meta-rewriting with the given definition (see also \S\ref{sec:rewrite_goals}). \index{meta-rewriting} \item[\ttindexbold{bws}] is like \texttt{bw} but takes a list of definitions. \item[\ttindexbold{ren} {\it names} {\it i};] performs \texttt{by (rename_tac {\it names} {\it i});} it renames parameters in subgoal~$i$. (Ignore the message {\footnotesize\tt Warning:\ same as previous level}.) \index{parameters!renaming} \end{ttdescription} \section{Executing batch proofs}\label{sec:executing-batch} \index{batch execution}% To save space below, let type \texttt{tacfn} abbreviate \texttt{thm list -> tactic list}, which is the type of a tactical proof. \begin{ttbox} prove_goal : theory -> string -> tacfn -> thm qed_goal : string -> theory -> string -> tacfn -> unit prove_goalw: theory -> thm list -> string -> tacfn -> thm qed_goalw : string -> theory -> thm list -> string -> tacfn -> unit prove_goalw_cterm: thm list -> cterm -> tacfn -> thm \end{ttbox} These batch functions create an initial proof state, then apply a tactic to it, yielding a sequence of final proof states. The head of the sequence is returned, provided it is an instance of the theorem originally proposed. The forms \texttt{prove_goal}, \texttt{prove_goalw} and \texttt{prove_goalw_cterm} are analogous to \texttt{goal}, \texttt{goalw} and \texttt{goalw_cterm}. The tactic is specified by a function from theorem lists to tactic lists. The function is applied to the list of meta-assumptions taken from the main goal. The resulting tactics are applied in sequence (using {\tt EVERY}). For example, a proof consisting of the commands \begin{ttbox} val prems = goal {\it theory} {\it formula}; by \(tac@1\); \ldots by \(tac@n\); qed "my_thm"; \end{ttbox} can be transformed to an expression as follows: \begin{ttbox} qed_goal "my_thm" {\it theory} {\it formula} (fn prems=> [ \(tac@1\), \ldots, \(tac@n\) ]); \end{ttbox} The methods perform identical processing of the initial {\it formula} and the final proof state. But \texttt{prove_goal} executes the tactic as a atomic operation, bypassing the subgoal module; the current interactive proof is unaffected. % \begin{ttdescription} \item[\ttindexbold{prove_goal} {\it theory} {\it formula} {\it tacsf};] executes a proof of the {\it formula\/} in the given {\it theory}, using the given tactic function. \item[\ttindexbold{qed_goal} $name$ $theory$ $formula$ $tacsf$;] acts like \texttt{prove_goal} but it also stores the resulting theorem in the theorem database associated with its theory and in the {\ML} variable $name$ (see \S\ref{ExtractingAndStoringTheProvedTheorem}). \item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula} {\it tacsf};]\index{meta-rewriting} is like \texttt{prove_goal} but also applies the list of {\it defs\/} as meta-rewrite rules to the first subgoal and the premises. \item[\ttindexbold{qed_goalw} $name$ $theory$ $defs$ $formula$ $tacsf$;] is analogous to \texttt{qed_goal}. \item[\ttindexbold{prove_goalw_cterm} {\it defs} {\it ct} {\it tacsf};] is a version of \texttt{prove_goalw} intended for programming. The main goal is supplied as a cterm, not as a string. A cterm carries a theory with it, and can be created from a term~$t$ by \begin{ttbox} cterm_of (sign_of thy) \(t\) \end{ttbox} \index{*cterm_of}\index{*sign_of} \end{ttdescription} \section{Internal proofs} \begin{ttbox} Tactic.prove: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm Tactic.prove_standard: Sign.sg -> string list -> term list -> term -> (thm list -> tactic) -> thm \end{ttbox} These functions provide a clean internal interface for programmed proofs. The special overhead of top-level statements (cf.\ \verb,prove_goalw_cterm,) is omitted. Statements may be established within a local contexts of fixed variables and assumptions, which are the only hypotheses to be discharged in the result. \begin{ttdescription} \item[\ttindexbold{Tactic.prove}~$sg~xs~As~C~tacf$] establishes the result $\Forall xs. As \Imp C$ via the given tactic (which is a function taking the assumptions as local premises). \item[\ttindexbold{Tactic.prove_standard}] is simular to \verb,Tactic.prove,, but performs the \verb,standard, operation on the result, essentially turning it into a top-level statement. Never do this for local proofs within other proof tools! \end{ttdescription} \section{Managing multiple proofs} \index{proofs!managing multiple} You may save the current state of the subgoal module and resume work on it later. This serves two purposes. \begin{enumerate} \item At some point, you may be uncertain of the next step, and wish to experiment. \item During a proof, you may see that a lemma should be proved first. \end{enumerate} Each saved proof state consists of a list of levels; \ttindex{chop} behaves independently for each of the saved proofs. In addition, each saved state carries a separate \ttindex{undo} list. \subsection{The stack of proof states} \index{proofs!stacking} \begin{ttbox} push_proof : unit -> unit pop_proof : unit -> thm list rotate_proof : unit -> thm list \end{ttbox} The subgoal module maintains a stack of proof states. Most subgoal commands affect only the top of the stack. The \ttindex{Goal} command {\em replaces\/} the top of the stack; the only command that pushes a proof on the stack is \texttt{push_proof}. To save some point of the proof, call \texttt{push_proof}. You may now state a lemma using \texttt{goal}, or simply continue to apply tactics. Later, you can return to the saved point by calling \texttt{pop_proof} or \texttt{rotate_proof}. To view the entire stack, call \texttt{rotate_proof} repeatedly; as it rotates the stack, it prints the new top element. \begin{ttdescription} \item[\ttindexbold{push_proof}();] duplicates the top element of the stack, pushing a copy of the current proof state on to the stack. \item[\ttindexbold{pop_proof}();] discards the top element of the stack. It returns the list of assumptions associated with the new proof; you should bind these to an \ML\ identifier. They can also be obtained by calling \ttindex{premises}. \item[\ttindexbold{rotate_proof}();] \index{assumptions!of main goal} rotates the stack, moving the top element to the bottom. It returns the list of assumptions associated with the new proof. \end{ttdescription} \subsection{Saving and restoring proof states} \index{proofs!saving and restoring} \begin{ttbox} save_proof : unit -> proof restore_proof : proof -> thm list \end{ttbox} States of the subgoal module may be saved as \ML\ values of type~\mltydx{proof}, and later restored. \begin{ttdescription} \item[\ttindexbold{save_proof}();] returns the current state, which is on top of the stack. \item[\ttindexbold{restore_proof} {\it prf};]\index{assumptions!of main goal} replaces the top of the stack by~{\it prf}. It returns the list of assumptions associated with the new proof. \end{ttdescription} \section{*Debugging and inspecting} \index{tactics!debugging} These functions can be useful when you are debugging a tactic. They refer to the current proof state stored in the subgoal module. A tactic should never call them; it should operate on the proof state supplied as its argument. \subsection{Reading and printing terms} \index{terms!reading of}\index{terms!printing of}\index{types!printing of} \begin{ttbox} read : string -> term prin : term -> unit printyp : typ -> unit \end{ttbox} These read and print terms (or types) using the syntax associated with the proof state. \begin{ttdescription} \item[\ttindexbold{read} {\it string}] reads the {\it string} as a term, without type-checking. \item[\ttindexbold{prin} {\it t};] prints the term~$t$ at the terminal. \item[\ttindexbold{printyp} {\it T};] prints the type~$T$ at the terminal. \end{ttdescription} \subsection{Inspecting the proof state} \index{proofs!inspecting the state} \begin{ttbox} topthm : unit -> thm getgoal : int -> term gethyps : int -> thm list \end{ttbox} \begin{ttdescription} \item[\ttindexbold{topthm}()] returns the proof state as an Isabelle theorem. This is what \ttindex{by} would supply to a tactic at this point. It omits the post-processing of \ttindex{result} and \ttindex{uresult}. \item[\ttindexbold{getgoal} {\it i}] returns subgoal~$i$ of the proof state, as a term. You may print this using \texttt{prin}, though you may have to examine the internal data structure in order to locate the problem! \item[\ttindexbold{gethyps} {\it i}] returns the hypotheses of subgoal~$i$ as meta-level assumptions. In these theorems, the subgoal's parameters become free variables. This command is supplied for debugging uses of \ttindex{METAHYPS}. \end{ttdescription} \subsection{Filtering lists of rules} \begin{ttbox} filter_goal: (term*term->bool) -> thm list -> int -> thm list \end{ttbox} \begin{ttdescription} \item[\ttindexbold{filter_goal} {\it could} {\it ths} {\it i}] applies \texttt{filter_thms {\it could}} to subgoal~$i$ of the proof state and returns the list of theorems that survive the filtering. \end{ttdescription} \index{subgoal module|)} \index{proofs|)} %%% Local Variables: %%% mode: latex %%% TeX-master: "ref" %%% End: