--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Ref/goals.tex Wed Nov 10 05:00:57 1993 +0100
@@ -0,0 +1,542 @@
+%% $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 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|bold}
+\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 = it;
+\end{ttbox}
+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, \ttindex{result} compares the
+stored assumptions with the actual assumptions in the proof state.
+
+Some of the commands unfold definitions using meta-rewrite rules. This
+expansion affects both the first subgoal and the premises, which would
+otherwise require use of \ttindex{rewrite_goals_tac} and
+\ttindex{rewrite_rule}.
+
+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 is useful when the next step of the proof would
+otherwise be to call \ttindex{cut_facts_tac} with the list of premises
+(\S\ref{cut_facts_tac}).
+
+\begin{description}
+\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{rewriting!meta-level}
+
+\item[\ttindexbold{goalw_cterm} {\it theory} {\it defs} {\it ct}; ]
+is a version of {\tt goalw} for special 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 forget to bind them to an \ML{} identifier.
+\end{description}
+
+\subsection{Applying a tactic}
+\index{tactics!commands for applying|bold}
+\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{description} \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{description}
+
+\noindent{\bf Error indications:}
+\begin{itemize}
+\item
+{\tt "by:\ tactic failed"} means that the tactic returned an empty
+sequence when applied to the current proof state.
+\item
+{\tt "Warning:\ same as previous level"} means that the new proof state
+is identical to the previous state.
+\item
+{\tt "Warning:\ signature of proof state has changed"} means that a rule
+was applied from outside the theory of the initial proof state. This
+guards against mistakes such as expressing the goal in intuitionistic logic
+and proving it using classical logic.
+\end{itemize}
+
+\subsection{Extracting the proved theorem}
+\index{ending a proof|bold}
+\begin{ttbox}
+result : unit -> thm
+uresult : unit -> thm
+\end{ttbox}
+\begin{description}
+\item[\ttindexbold{result}()]
+returns the final theorem, after converting the free variables to
+schematics. It discharges the assumptions supplied to the matching
+\ttindex{goal} command.
+
+It raises an exception unless the proof state passes certain checks. There
+must be no assumptions other than those supplied to \ttindex{goal}. There
+must be no subgoals. The theorem proved must be a (first-order) instance
+of the original goal, as stated in the \ttindex{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.
+
+\item[\ttindexbold{uresult}()]
+is similar but omits the checks given above. It is needed when the initial
+goal contains function unknowns, when definitions are unfolded in the main
+goal, or when \ttindex{assume_ax} has been used.
+\end{description}
+
+
+\subsection{Undoing and backtracking}
+\index{undoing a proof command|bold}
+\index{backtracking command|see{\tt back}}
+\begin{ttbox}
+chop : unit -> unit
+choplev : int -> unit
+back : unit -> unit
+undo : unit -> unit
+\end{ttbox}
+\begin{description}
+\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.
+
+\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{description}
+\noindent{\bf Error indications for {\tt back}:}
+\begin{itemize}
+\item
+{\tt"Warning:\ same as previous choice at this level"} means that {\tt
+back} found a non-empty branch point, but that it contained the same proof
+state as the current one.
+\item
+{\tt "Warning:\ signature of proof state has changed"} means the signature
+of the alternative proof state differs from that of the current state.
+\item
+{\tt "back:\ no alternatives"} means {\tt back} could find no alternative
+proof state.
+\end{itemize}
+
+\subsection{Printing the proof state}
+\index{printing!proof state|bold}
+\begin{ttbox}
+pr : unit -> unit
+prlev : int -> unit
+goals_limit: int ref \hfill{\bf initially 10}
+\end{ttbox}
+\begin{description}
+\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} \tt:= {\it k};]
+specifies~$k$ as the maximum number of subgoals to print.
+\end{description}
+
+
+\subsection{Timing}
+\index{printing!timing statistics|bold}\index{proofs!timing|bold}
+\begin{ttbox}
+proof_timing: bool ref \hfill{\bf initially false}
+\end{ttbox}
+
+\begin{description}
+\item[\ttindexbold{proof_timing} \tt:= true;]
+makes the \ttindex{by} and \ttindex{prove_goal} commands display how much
+processor time was spent. This information is compiler-dependent.
+\end{description}
+
+
+\section{Shortcuts for applying tactics}
+\index{shortcuts!for ``{\tt by}'' commands|bold}
+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
+\end{ttbox}
+
+\begin{description}
+\item[\ttindexbold{ba} {\it i};]
+performs \hbox{\tt by (assume_tac {\it i});}\index{*assume_tac}
+
+\item[\ttindexbold{br} {\it thm} {\it i};]
+performs \hbox{\tt by (resolve_tac [{\it thm}] {\it i});}\index{*resolve_tac}
+
+\item[\ttindexbold{be} {\it thm} {\it i};]
+performs \hbox{\tt by (eresolve_tac [{\it thm}] {\it i});}\index{*eresolve_tac}
+
+\item[\ttindexbold{bd} {\it thm} {\it i};]
+performs \hbox{\tt by (dresolve_tac [{\it thm}] {\it i});}\index{*dresolve_tac}
+\end{description}
+
+\subsubsection{Resolution with a list of theorems}
+\begin{ttbox}
+brs: thm list -> int -> unit
+bes: thm list -> int -> unit
+bds: thm list -> int -> unit
+\end{ttbox}
+
+\begin{description}
+\item[\ttindexbold{brs} {\it thms} {\it i};]
+performs \hbox{\tt by (resolve_tac {\it thms} {\it i});}\index{*resolve_tac}
+
+\item[\ttindexbold{bes} {\it thms} {\it i};]
+performs \hbox{\tt by (eresolve_tac {\it thms} {\it i});}\index{*eresolve_tac}
+
+\item[\ttindexbold{bds} {\it thms} {\it i};]
+performs \hbox{\tt by (dresolve_tac {\it thms} {\it i});}\index{*dresolve_tac}
+\end{description}
+
+
+\subsection{Scanning shortcuts}
+\index{shortcuts!scanning for subgoals|bold}
+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!
+
+\subsubsection{Proof by assumption and resolution}
+\begin{ttbox}
+fa: unit -> unit
+fr: thm -> unit
+fe: thm -> unit
+fd: thm -> unit
+\end{ttbox}
+
+\begin{description}
+\item[\ttindexbold{fa}();]
+solves some subgoal by assumption.\index{*assume_tac}
+
+\item[\ttindexbold{fr} {\it thm};]
+refines some subgoal using \hbox{\tt resolve_tac [{\it thm}]}
+\index{*resolve_tac}
+
+\item[\ttindexbold{fe} {\it thm};]
+refines some subgoal using \hbox{\tt eresolve_tac [{\it thm}]}
+\index{*eresolve_tac}
+
+\item[\ttindexbold{fd} {\it thm};]
+refines some subgoal using \hbox{\tt dresolve_tac [{\it thm}]}
+\index{*dresolve_tac}
+\end{description}
+
+\subsubsection{Resolution with a list of theorems}
+\begin{ttbox}
+frs: thm list -> unit
+fes: thm list -> unit
+fds: thm list -> unit
+\end{ttbox}
+
+\begin{description}
+\item[\ttindexbold{frs} {\it thms};]
+refines some subgoal using \hbox{\tt resolve_tac {\it thms}}
+\index{*resolve_tac}
+
+\item[\ttindexbold{fes} {\it thms};]
+refines some subgoal using \hbox{\tt eresolve_tac {\it thms}}
+\index{*eresolve_tac}
+
+\item[\ttindexbold{fds} {\it thms};]
+refines some subgoal using \hbox{\tt dresolve_tac {\it thms}}
+\index{*dresolve_tac}
+\end{description}
+
+\subsection{Other shortcuts}
+\begin{ttbox}
+bw : thm -> unit
+bws : thm list -> unit
+ren : string -> int -> unit
+\end{ttbox}
+\begin{description}
+\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{*rewrite_goals_tac}
+\index{rewriting!meta-level}
+
+\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 {\tt Warning:\ same as
+previous level}.)
+\index{*rename_tac}\index{parameters!renaming}
+\end{description}
+
+
+
+\section{Advanced features}
+\subsection{Executing batch proofs}
+\index{proofs!batch|bold}
+\index{batch execution|bold}
+\begin{ttbox}
+prove_goal : theory-> string->(thm list->tactic list)->thm
+prove_goalw : theory->thm list->string->(thm list->tactic list)->thm
+prove_goalw_cterm: thm list->Sign.cterm->(thm list->tactic list)->thm
+\end{ttbox}
+A collection of derivations may be stored for batch execution using these
+functions. They 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 \ttindex{goal}, \ttindex{goalw} and \ttindex{goalw_cterm}.
+
+The tactic is specified by a function from theorem lists to tactic lists.
+The function is applied to the list of meta-hypotheses 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 commands can also be
+encapsulated in an expression using~{\tt let}:
+\begin{ttbox}
+val my_thm =
+ let val prems = goal {\it theory} {\it formula}
+ in by \(tac@1\); \ldots by \(tac@n\); result() end;
+\end{ttbox}
+
+\begin{description}
+\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{prove_goalw} {\it theory} {\it defs} {\it formula}
+ {\it tacsf}; ]
+is like {\tt prove_goal} but also applies the list of {\it defs\/} as
+meta-rewrite rules to the first subgoal and the premises.
+\index{rewriting!meta-level}
+
+\item[\ttindexbold{prove_goalw_cterm} {\it theory} {\it defs} {\it ct}
+ {\it tacsf}; ]
+is a version of {\tt prove_goalw} for special 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}
+\end{description}
+
+
+\subsection{Managing multiple proofs}
+\index{proofs!managing multiple|bold}
+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.
+
+\subsubsection{The stack of proof states}
+\index{proofs!stacking|bold}
+\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 {\bf
+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 \ttindex{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{description}
+\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
+meta-hypotheses 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}]
+rotates the stack, moving the top element to the bottom. It returns the
+list of assumptions associated with the new proof.
+\end{description}
+
+
+\subsubsection{Saving and restoring proof states}
+\index{proofs!saving and restoring|bold}
+\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~\ttindex{proof}, and later restored.
+
+\begin{description}
+\item[\ttindexbold{save_proof}();]
+returns the current state, which is on top of the stack.
+
+\item[\ttindexbold{restore_proof} {\it prf}]
+replaces the top of the stack by~{\it prf}. It returns the list of
+assumptions associated with the new proof.
+\end{description}
+
+
+\subsection{Debugging and inspecting}
+\index{proofs!debugging|bold}
+\index{debugging}
+These specialized operations support the debugging of tactics. They refer
+to the current proof state of the subgoal module, and fail if there is no
+proof underway.
+
+\subsubsection{Reading and printing terms}
+\index{reading!terms|bold}\index{printing!terms}\index{printing!types}
+\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{description}
+\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{description}
+
+\subsubsection{Inspecting the proof state}
+\index{proofs!inspecting the state|bold}
+\begin{ttbox}
+topthm : unit -> thm
+getgoal : int -> term
+gethyps : int -> thm list
+\end{ttbox}
+
+\begin{description}
+\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{description}
+
+\subsubsection{Filtering lists of rules}
+\begin{ttbox}
+filter_goal: (term*term->bool) -> thm list -> int -> thm list
+\end{ttbox}
+
+\begin{description}
+\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{description}
+
+\index{subgoal module|)}
+\index{proofs|)}