summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | lcp |

Fri, 15 Apr 1994 16:47:15 +0200 | |

changeset 321 | 998f1c5adafb |

parent 320 | 76ae17549558 |

child 322 | bacfaeeea007 |

penultimate Springer draft

--- 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|)}