doc-src/Ref/goals.tex

add lemma diff_Suc_1

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