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