--- a/doc-src/Ref/goals.tex Fri Apr 15 16:37:59 1994 +0200
+++ b/doc-src/Ref/goals.tex Fri Apr 15 16:47:15 1994 +0200
@@ -3,9 +3,10 @@
\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
+
+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
@@ -27,7 +28,7 @@
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}
+\index{proofs!starting}
\begin{ttbox}
goal : theory -> string -> thm list
goalw : theory -> thm list -> string -> thm list
@@ -44,47 +45,49 @@
something like
\begin{ttbox}
val prems = it;
-\end{ttbox}
+\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, \ttindex{result} compares the
+ 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 first subgoal and the premises, which would
-otherwise require use of \ttindex{rewrite_goals_tac} and
-\ttindex{rewrite_rule}.
+otherwise require use of {\tt rewrite_goals_tac} and
+{\tt 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}).
+\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{description}
-\item[\ttindexbold{goal} {\it theory} {\it formula}; ]
+\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}; ]
+\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}
+\index{meta-rewriting}
-\item[\ttindexbold{goalw_cterm} {\it theory} {\it defs} {\it ct}; ]
-is a version of {\tt goalw} for special applications. The main goal is
+\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 forget to bind them to an \ML{} identifier.
-\end{description}
+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|bold}
+\index{tactics!commands for applying}
\begin{ttbox}
by : tactic -> unit
byev : tactic list -> unit
@@ -93,14 +96,14 @@
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}; ]
+\begin{ttdescription} \item[\ttindexbold{by} {\it tactic};]
applies the {\it tactic\/} to the proof state.
-\item[\ttindexbold{byev} {\it tactics}; ]
+\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}
+\end{ttdescription}
\noindent{\it Error indications:}\nobreak
\begin{itemize}
@@ -115,41 +118,44 @@
\end{itemize}
\subsection{Extracting the proved theorem}
-\index{ending a proof|bold}
+\index{theorems!from subgoal module}
\begin{ttbox}
result : unit -> thm
uresult : unit -> thm
\end{ttbox}
-\begin{description}
-\item[\ttindexbold{result}()]
+\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
-\ttindex{goal} command.
+{\tt 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 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 \ttindex{goal} command. This allows
+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.
-\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}
+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.
+\end{ttdescription}
\subsection{Undoing and backtracking}
-\index{backtracking command|see{\tt back}}
\begin{ttbox}
chop : unit -> unit
choplev : int -> unit
back : unit -> unit
undo : unit -> unit
\end{ttbox}
-\begin{description}
+\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
@@ -169,7 +175,7 @@
{\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}
+\end{ttdescription}
\goodbreak
\noindent{\it Error indications for {\tt back}:}\par\nobreak
@@ -185,13 +191,13 @@
\end{itemize}
\subsection{Printing the proof state}
-\index{printing!proof state|bold}
+\index{proof state!printing of}
\begin{ttbox}
pr : unit -> unit
prlev : int -> unit
goals_limit: int ref \hfill{\bf initially 10}
\end{ttbox}
-\begin{description}
+\begin{ttdescription}
\item[\ttindexbold{pr}();]
prints the current proof state.
@@ -199,123 +205,103 @@
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};]
+\item[\ttindexbold{goals_limit} := {\it k};]
specifies~$k$ as the maximum number of subgoals to print.
-\end{description}
+\end{ttdescription}
\subsection{Timing}
-\index{printing!timing statistics|bold}\index{proofs!timing|bold}
+\index{timing statistics}\index{proofs!timing}
\begin{ttbox}
proof_timing: bool ref \hfill{\bf initially false}
\end{ttbox}
-\begin{description}
-\item[\ttindexbold{proof_timing} \tt:= true;]
+\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{description}
+\end{ttdescription}
\section{Shortcuts for applying tactics}
-\index{shortcuts!for ``{\tt by}'' commands|bold}
+\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
+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{description}
+\begin{ttdescription}
\item[\ttindexbold{ba} {\it i};]
-performs \hbox{\tt by (assume_tac {\it i});}\index{*assume_tac}
+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});}\index{*resolve_tac}
+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});}\index{*eresolve_tac}
+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});}\index{*dresolve_tac}
-\end{description}
+performs \hbox{\tt by (dresolve_tac [{\it thm}] {\it i});}
-\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}
+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});}\index{*eresolve_tac}
+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});}\index{*dresolve_tac}
-\end{description}
+performs \hbox{\tt by (dresolve_tac {\it thms} {\it i});}
+\end{ttdescription}
\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
+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{description}
+\begin{ttdescription}
\item[\ttindexbold{fa}();]
-solves some subgoal by assumption.\index{*assume_tac}
+solves some subgoal by assumption.
\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}
+\end{ttdescription}
\subsection{Other shortcuts}
\begin{ttbox}
@@ -323,12 +309,12 @@
bws : thm list -> unit
ren : string -> int -> unit
\end{ttbox}
-\begin{description}
+\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{*rewrite_goals_tac}
-\index{rewriting!meta-level}
+meta-rewriting with the given definition.
+\index{meta-rewriting}
\item[\ttindexbold{bws}]
is like {\tt bw} but takes a list of definitions.
@@ -337,26 +323,22 @@
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}
-
+\index{parameters!renaming}
+\end{ttdescription}
-\section{Advanced features}
-\subsection{Executing batch proofs}
-\index{proofs!batch|bold}
-\index{batch execution|bold}
+\section{Executing batch proofs}
+\index{batch execution}
\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
+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 \ttindex{goal}, \ttindex{goalw} and \ttindex{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-hypotheses taken from the main
@@ -374,38 +356,40 @@
\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}:
+atomic operation, bypassing the subgoal module.
+
+A batch proof may alternatively consist of subgoal commands encapsulated
+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}; ]
+\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{prove_goalw} {\it theory} {\it defs} {\it formula}
- {\it tacsf}; ]\index{rewriting!meta-level}
+ {\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{prove_goalw_cterm} {\it theory} {\it defs} {\it ct}
- {\it tacsf}; ]
-is a version of {\tt prove_goalw} for special applications. The main
+ {\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{description}
+\end{ttdescription}
-\subsection{Managing multiple proofs}
-\index{proofs!managing multiple|bold}
+\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}
@@ -418,27 +402,27 @@
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}
+\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 {\bf
-replaces} the top of the stack; the only command that pushes a proof on the
+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 \ttindex{goal}, or simply continue to apply tactics.
+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{description}
+\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.
@@ -448,40 +432,39 @@
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}]
+\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{description}
+\end{ttdescription}
-\subsubsection{Saving and restoring proof states}
-\index{proofs!saving and restoring|bold}
+\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~\ttindex{proof}, and later restored.
+type~\mltydx{proof}, and later restored.
-\begin{description}
+\begin{ttdescription}
\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}
+\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}
-\subsection{Debugging and inspecting}
-\index{proofs!debugging|bold}
-\index{debugging}
+\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, and fail if there is no
-proof underway.
+to the current proof state of the subgoal module.
-\subsubsection{Reading and printing terms}
-\index{reading!terms|bold}\index{printing!terms}\index{printing!types}
+\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
@@ -490,7 +473,7 @@
These read and print terms (or types) using the syntax associated with the
proof state.
-\begin{description}
+\begin{ttdescription}
\item[\ttindexbold{read} {\it string}]
reads the {\it string} as a term, without type checking.
@@ -499,17 +482,17 @@
\item[\ttindexbold{printyp} {\it T};]
prints the type~$T$ at the terminal.
-\end{description}
+\end{ttdescription}
-\subsubsection{Inspecting the proof state}
-\index{proofs!inspecting the state|bold}
+\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{description}
+\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
@@ -520,22 +503,22 @@
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}
+\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}
-\subsubsection{Filtering lists of rules}
+\subsection{Filtering lists of rules}
\begin{ttbox}
filter_goal: (term*term->bool) -> thm list -> int -> thm list
\end{ttbox}
-\begin{description}
+\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{description}
+\end{ttdescription}
\index{subgoal module|)}
\index{proofs|)}