# HG changeset patch # User wenzelm # Date 904228871 -7200 # Node ID 8b22b93dba2c9619b57cb418e9833699fa7b7c56 # Parent 0c9e6d860485b1532f12c2602de71473081fe8f8 Goal, Goalw; thm, thms; moved get_thm etc. from theories.tex; diff -r 0c9e6d860485 -r 8b22b93dba2c doc-src/Ref/goals.tex --- a/doc-src/Ref/goals.tex Thu Aug 27 16:40:37 1998 +0200 +++ b/doc-src/Ref/goals.tex Thu Aug 27 16:41:11 1998 +0200 @@ -24,21 +24,24 @@ \section{Basic commands} -Most proofs begin with \texttt{goal} or \texttt{goalw} and require no other +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 : theory -> string -> thm list +\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 \texttt{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! + +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 @@ -46,11 +49,19 @@ \begin{ttbox} val prems = goal{\it theory\/ formula}; \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 \texttt{premises}. When the proof is finished, \texttt{qed} -compares the stored assumptions with the actual assumptions in the -proof state. +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 @@ -59,6 +70,14 @@ \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. @@ -161,6 +180,67 @@ \end{ttdescription} +\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}