--- a/doc-src/Ref/goals.tex Sun Mar 01 12:37:59 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,722 +0,0 @@
-%% $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: