doc-src/Ref/goals.tex

major refactorings in code generator modules

%% $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: