doc-src/Ref/goals.tex

added new example by John Harrison

%% $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 {\tt goal} or {\tt goalw} and require no other
commands than {\tt by}, {\tt chop} and {\tt undo}.  They typically end with
a call to {\tt result}.
\subsection{Starting a backward proof}
\index{proofs!starting}
\begin{ttbox} 
goal        : theory -> string -> thm list 
goalw       : theory -> thm list -> string -> thm list 
goalw_cterm : thm list -> Sign.cterm -> thm list 
premises    : unit -> thm list
\end{ttbox}
The {\tt 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 serve as the premises when you are deriving a rule.  They
are also stored internally and can be retrieved later by the function {\tt
  premises}.  When the proof is finished, {\tt result} compares the
stored assumptions with the actual assumptions in the proof state.

\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 {\tt rewrite_goals_tac} and
{\tt rewrite_rule}.

\index{*"!"! symbol!in main goal}
If the main goal has the form {\tt"!!{\it vars}.\ \ldots"}, with an
outermost quantifier, then the list of premises will be empty.  Subgoal~1
will contain the meta-quantified {\it vars\/} as parameters and the goal's
premises as assumptions.  This avoids having to call
\ttindex{cut_facts_tac} with the list of premises (\S\ref{cut_facts_tac}).

\begin{ttdescription}
\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 {\tt 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 theory} {\it defs} {\it ct};] 
is a version of {\tt goalw} for programming applications.  The main goal is
supplied as a cterm, not as a string.  Typically, the cterm is created from
a term~$t$ by \hbox{\tt Sign.cterm_of (sign_of thy) $t$}.
\index{*Sign.cterm_of}\index{*sign_of}

\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~{\tt 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 {\tt prove_goal}, and abbreviates \hbox{\tt 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} 
result    : unit -> thm
uresult   : unit -> thm
bind_thm  : string * thm -> unit
qed       : string -> unit
\end{ttbox}
\begin{ttdescription}
\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 
  {\tt goal} command.  

  It raises an exception unless the proof state passes certain checks.  There
  must be no assumptions other than those supplied to {\tt goal}.  There
  must be no subgoals.  The theorem proved must be a (first-order) instance
  of the original goal, as stated in the {\tt 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 {\tt 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 of}
  stores {\tt standard($thm$)} (see \S\ref{MiscellaneousForwardRules})
  in Isabelle's theorem database and in the ML variable $name$. The
  theorem can be retrieved from Isabelle's database by {\tt get_thm}
  (see \S\ref{BasicOperationsOnTheories}).

\item[\ttindexbold{qed} $name$]
  combines {\tt result} and {\tt bind_thm} in that it first uses {\tt
  result()} to get the theorem and then stores it like {\tt bind_thm}.
\end{ttdescription}


\subsection{Retrieving theorems}
\index{theorems!retrieving}

The following functions retrieve theorems (together with their names) from
the theorem database.  Hence 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 : string 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 {\tt 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
  {\tt eresolve_tac} and {\tt 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 {\tt eresolve_tac} and
  {\tt dresolve_tac}.

\item[\ttindexbold{thms_containing} $strings$] returns all theorems that
  contain all of the constants in $strings$.  Note that a few basic constants
  like \verb$==>$ are ignored.
\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 {\tt undo} command
can cancel it.

\item[\ttindexbold{choplev} {\it n};] 
truncates the state list to level~{\it n}. 

\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},
{\tt chop}, {\tt choplev}, and~{\tt back}.  It {\bf cannot}
cancel {\tt goal} or {\tt 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 {\tt 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 {\tt 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
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}.  This allows you to review the
previous steps of the proof.

\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} 
proof_timing: bool ref \hfill{\bf initially false}
\end{ttbox}

\begin{ttdescription}
\item[\ttindexbold{proof_timing} := true;] 
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 {\tt 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 \hbox{\tt by (assume_tac {\it i});}

\item[\ttindexbold{br} {\it thm} {\it i};] 
performs \hbox{\tt by (resolve_tac [{\it thm}] {\it i});}

\item[\ttindexbold{be} {\it thm} {\it i};] 
performs \hbox{\tt by (eresolve_tac [{\it thm}] {\it i});}

\item[\ttindexbold{bd} {\it thm} {\it i};] 
performs \hbox{\tt by (dresolve_tac [{\it thm}] {\it i});}

\item[\ttindexbold{brs} {\it thms} {\it i};] 
performs \hbox{\tt by (resolve_tac {\it thms} {\it i});}

\item[\ttindexbold{bes} {\it thms} {\it i};] 
performs \hbox{\tt by (eresolve_tac {\it thms} {\it i});}

\item[\ttindexbold{bds} {\it thms} {\it i};] 
performs \hbox{\tt 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 {\tt 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 \hbox{\tt resolve_tac [{\it thm}]}

\item[\ttindexbold{fe} {\it thm};] 
refines some subgoal using \hbox{\tt eresolve_tac [{\it thm}]}

\item[\ttindexbold{fd} {\it thm};] 
refines some subgoal using \hbox{\tt dresolve_tac [{\it thm}]}

\item[\ttindexbold{frs} {\it thms};] 
refines some subgoal using \hbox{\tt resolve_tac {\it thms}}

\item[\ttindexbold{fes} {\it thms};] 
refines some subgoal using \hbox{\tt eresolve_tac {\it thms}} 

\item[\ttindexbold{fds} {\it thms};] 
refines some subgoal using \hbox{\tt 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 \hbox{\tt by (rewrite_goals_tac [{\it def}]);}
It unfolds definitions in the subgoals (but not the main goal), by
meta-rewriting with the given definition.
\index{meta-rewriting}

\item[\ttindexbold{bws}] 
is like {\tt bw} but takes a list of definitions.

\item[\ttindexbold{ren} {\it names} {\it i};] 
performs \hbox{\tt 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}
\index{batch execution}
\begin{ttbox}
prove_goal :         theory->          string->(thm list->tactic list)->thm
qed_goal   : string->theory->          string->(thm list->tactic list)->unit
prove_goalw:         theory->thm list->string->(thm list->tactic list)->thm
qed_goalw  : string->theory->thm list->string->(thm list->tactic list)->unit
prove_goalw_cterm: thm list->Sign.cterm->(thm list->tactic list)->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 {\tt prove_goal}, {\tt prove_goalw} and {\tt prove_goalw_cterm}
are analogous to {\tt goal}, {\tt goalw} and {\tt 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\);
val my_thm = result();
\end{ttbox}
can be transformed to an expression as follows:
\begin{ttbox} 
val my_thm = prove_goal {\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 {\tt 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 {\tt prove_goal} but also stores the resulting theorem in
Isabelle's theorem database 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 {\tt 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 {\tt qed_goal}.

\item[\ttindexbold{prove_goalw_cterm} {\it theory} {\it defs} {\it ct}
      {\it tacsf};] 
is a version of {\tt prove_goalw} for programming applications.  The main
goal is supplied as a cterm, not as a string.  Typically, the cterm is
created from a term~$t$ as follows:
\begin{ttbox}
Sign.cterm_of (sign_of thy) \(t\)
\end{ttbox}
\index{*Sign.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 {\tt push_proof}.

To save some point of the proof, call {\tt push_proof}.  You may now
state a lemma using {\tt goal}, or simply continue to apply tactics.
Later, you can return to the saved point by calling {\tt pop_proof} or 
{\tt rotate_proof}. 

To view the entire stack, call {\tt 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 specialized operations support the debugging of tactics.  They refer
to the current proof state of the subgoal module.

\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 {\tt 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 \hbox{\tt 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|)}