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

author | paulson |

Tue, 28 Jul 1998 16:33:43 +0200 | |

changeset 5205 | 602354039306 |

parent 5204 | 858da18069d7 |

child 5206 | a3f26b19cd7e |

Changed "goal" to "Goal"

--- a/doc-src/Intro/advanced.tex Tue Jul 28 16:30:56 1998 +0200 +++ b/doc-src/Intro/advanced.tex Tue Jul 28 16:33:43 1998 +0200 @@ -5,11 +5,11 @@ Look through {\em Isabelle's Object-Logics\/} and try proving some simple theorems. You probably should begin with first-order logic -({\tt FOL} or~{\tt LK}). Try working some of the examples provided, -and others from the literature. Set theory~({\tt ZF}) and -Constructive Type Theory~({\tt CTT}) form a richer world for +(\texttt{FOL} or~\texttt{LK}). Try working some of the examples provided, +and others from the literature. Set theory~(\texttt{ZF}) and +Constructive Type Theory~(\texttt{CTT}) form a richer world for mathematical reasoning and, again, many examples are in the -literature. Higher-order logic~({\tt HOL}) is Isabelle's most +literature. Higher-order logic~(\texttt{HOL}) is Isabelle's most elaborate logic. Its types and functions are identified with those of the meta-logic. @@ -37,24 +37,34 @@ \index{examples!of deriving rules}\index{assumptions!of main goal} The subgoal module supports the derivation of rules, as discussed in -\S\ref{deriving}. The \ttindex{goal} command, when supplied a goal of -the form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, creates -$\phi\Imp\phi$ as the initial proof state and returns a list -consisting of the theorems ${\theta@i\;[\theta@i]}$, for $i=1$, -\ldots,~$k$. These meta-assumptions are also recorded internally, -allowing {\tt result} (which is called by {\tt qed}) to discharge them -in the original order. +\S\ref{deriving}. When the \ttindex{Goal} command is supplied a formula of +the form $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, there are two +possibilities: +\begin{itemize} +\item If all of the premises $\theta@1$, \ldots, $\theta@k$ are simple + formulae{} (they do not involve the meta-connectives $\Forall$ or + $\Imp$) then the command sets the goal to be + $\List{\theta@1; \ldots; \theta@k} \Imp \phi$ and returns the empty list. +\item If one or more premises involves the meta-connectives $\Forall$ or + $\Imp$, then the command sets the goal to be $\phi$ and returns a list + consisting of the theorems ${\theta@i\;[\theta@i]}$, for $i=1$, \ldots,~$k$. + These meta-assumptions are also recorded internally, allowing + \texttt{result} (which is called by \texttt{qed}) to discharge them in the + original order. +\end{itemize} +Rules that discharge assumptions or introduce eigenvariables have complex +premises, and the second case applies. -Let us derive $\conj$ elimination using Isabelle. -Until now, calling {\tt goal} has returned an empty list, which we have -thrown away. In this example, the list contains the two premises of the -rule. We bind them to the \ML\ identifiers {\tt major} and {\tt -minor}:\footnote{Some ML compilers will print a message such as {\em -binding not exhaustive}. This warns that {\tt goal} must return a -2-element list. Otherwise, the pattern-match will fail; ML will -raise exception \xdx{Match}.} +Let us derive $\conj$ elimination. Until now, calling \texttt{Goal} has +returned an empty list, which we have ignored. In this example, the list +contains the two premises of the rule, since one of them involves the $\Imp$ +connective. We bind them to the \ML\ identifiers \texttt{major} and {\tt + minor}:\footnote{Some ML compilers will print a message such as {\em binding + not exhaustive}. This warns that \texttt{Goal} must return a 2-element + list. Otherwise, the pattern-match will fail; ML will raise exception + \xdx{Match}.} \begin{ttbox} -val [major,minor] = goal FOL.thy +val [major,minor] = Goal "[| P&Q; [| P; Q |] ==> R |] ==> R"; {\out Level 0} {\out R} @@ -63,7 +73,7 @@ {\out val minor = "[| P; Q |] ==> R [[| P; Q |] ==> R]" : thm} \end{ttbox} Look at the minor premise, recalling that meta-level assumptions are -shown in brackets. Using {\tt minor}, we reduce $R$ to the subgoals +shown in brackets. Using \texttt{minor}, we reduce $R$ to the subgoals $P$ and~$Q$: \begin{ttbox} by (resolve_tac [minor] 1); @@ -133,7 +143,7 @@ Taking this point of view, Isabelle does not unfold definitions automatically during proofs. Rewriting must be explicit and selective. Isabelle provides tactics and meta-rules for rewriting, and a version of -the {\tt goal} command that unfolds the conclusion and premises of the rule +the \texttt{Goal} command that unfolds the conclusion and premises of the rule being derived. For example, the intuitionistic definition of negation given above may seem @@ -146,12 +156,11 @@ \subsection{Deriving the $\neg$ introduction rule} -To derive $(\neg I)$, we may call {\tt goal} with the appropriate -formula. Again, {\tt goal} returns a list consisting of the rule's -premises. We bind this one-element list to the \ML\ identifier {\tt - prems}. +To derive $(\neg I)$, we may call \texttt{Goal} with the appropriate formula. +Again, the rule's premises involve a meta-connective, and \texttt{Goal} +returns one-element list. We bind this list to the \ML\ identifier \texttt{prems}. \begin{ttbox} -val prems = goal FOL.thy "(P ==> False) ==> ~P"; +val prems = Goal "(P ==> False) ==> ~P"; {\out Level 0} {\out ~P} {\out 1. ~P} @@ -192,12 +201,12 @@ \end{ttbox} \indexbold{*notI theorem} -There is a simpler way of conducting this proof. The \ttindex{goalw} -command starts a backward proof, as does {\tt goal}, but it also +There is a simpler way of conducting this proof. The \ttindex{Goalw} +command starts a backward proof, as does \texttt{Goal}, but it also unfolds definitions. Thus there is no need to call \ttindex{rewrite_goals_tac}: \begin{ttbox} -val prems = goalw FOL.thy [not_def] +val prems = Goalw [not_def] "(P ==> False) ==> ~P"; {\out Level 0} {\out ~P} @@ -207,124 +216,48 @@ \subsection{Deriving the $\neg$ elimination rule} -Let us derive the rule $(\neg E)$. The proof follows that of~{\tt conjE} +Let us derive the rule $(\neg E)$. The proof follows that of~\texttt{conjE} above, with an additional step to unfold negation in the major premise. -Although the {\tt goalw} command is best for this, let us -try~{\tt goal} to see another way of unfolding definitions. After -binding the premises to \ML\ identifiers, we apply \tdx{FalseE}: +The \texttt{Goalw} command is best for this: it unfolds definitions not only +in the conclusion but the premises. \begin{ttbox} -val [major,minor] = goal FOL.thy "[| ~P; P |] ==> R"; +Goalw [not_def] "[| ~P; P |] ==> R"; {\out Level 0} -{\out R} -{\out 1. R} -{\out val major = "~ P [~ P]" : thm} -{\out val minor = "P [P]" : thm} -\ttbreak +{\out [| ~ P; P |] ==> R} +{\out 1. [| P --> False; P |] ==> R} +\end{ttbox} +As the first step, we apply \tdx{FalseE}: +\begin{ttbox} by (resolve_tac [FalseE] 1); {\out Level 1} -{\out R} -{\out 1. False} +{\out [| ~ P; P |] ==> R} +{\out 1. [| P --> False; P |] ==> False} \end{ttbox} +% Everything follows from falsity. And we can prove falsity using the premises and Modus Ponens: \begin{ttbox} -by (resolve_tac [mp] 1); +by (eresolve_tac [mp] 1); {\out Level 2} -{\out R} -{\out 1. ?P1 --> False} -{\out 2. ?P1} -\end{ttbox} -For subgoal~1, we transform the major premise from~$\neg P$ -to~${P\imp\bot}$. The function \ttindex{rewrite_rule}, given a list of -definitions, unfolds them in a theorem. Rewriting does not -affect the theorem's hypothesis, which remains~$\neg P$: -\begin{ttbox} -rewrite_rule [not_def] major; -{\out val it = "P --> False [~P]" : thm} -by (resolve_tac [it] 1); +{\out [| ~ P; P |] ==> R} +{\out 1. P ==> P} +\ttbreak +by (assume_tac 1); {\out Level 3} -{\out R} -{\out 1. P} -\end{ttbox} -The subgoal {\tt?P1} has been instantiated to~{\tt P}, which we can prove -using the minor premise: -\begin{ttbox} -by (resolve_tac [minor] 1); -{\out Level 4} -{\out R} +{\out [| ~ P; P |] ==> R} {\out No subgoals!} +\ttbreak qed "notE"; {\out val notE = "[| ~?P; ?P |] ==> ?R" : thm} \end{ttbox} -\indexbold{*notE theorem} + \medskip -Again, there is a simpler way of conducting this proof. Recall that -the \ttindex{goalw} command unfolds definitions the conclusion; it also -unfolds definitions in the premises: -\begin{ttbox} -val [major,minor] = goalw FOL.thy [not_def] - "[| ~P; P |] ==> R"; -{\out val major = "P --> False [~ P]" : thm} -{\out val minor = "P [P]" : thm} -\end{ttbox} -Observe the difference in {\tt major}; the premises are unfolded without -calling~\ttindex{rewrite_rule}. Incidentally, the four calls to -\ttindex{resolve_tac} above can be collapsed to one, with the help -of~\ttindex{RS}; this is a typical example of forward reasoning from a -complex premise. -\begin{ttbox} -minor RS (major RS mp RS FalseE); -{\out val it = "?P [P, ~P]" : thm} -by (resolve_tac [it] 1); -{\out Level 1} -{\out R} -{\out No subgoals!} -\end{ttbox} -\index{definitions!and derived rules|)} +\texttt{Goalw} unfolds definitions in the premises even when it has to return +them as a list. Another way of unfolding definitions in a theorem is by +applying the function \ttindex{rewrite_rule}. -\goodbreak\medskip\index{*"!"! symbol!in main goal} -Finally, here is a trick that is sometimes useful. If the goal -has an outermost meta-quantifier, then \ttindex{goal} and \ttindex{goalw} -do not return the rule's premises in the list of theorems; instead, the -premises become assumptions in subgoal~1. -%%%It does not matter which variables are quantified over. -\begin{ttbox} -goalw FOL.thy [not_def] "!!P R. [| ~P; P |] ==> R"; -{\out Level 0} -{\out !!P R. [| ~ P; P |] ==> R} -{\out 1. !!P R. [| P --> False; P |] ==> R} -val it = [] : thm list -\end{ttbox} -The proof continues as before. But instead of referring to \ML\ -identifiers, we refer to assumptions using {\tt eresolve_tac} or -{\tt assume_tac}: -\begin{ttbox} -by (resolve_tac [FalseE] 1); -{\out Level 1} -{\out !!P R. [| ~ P; P |] ==> R} -{\out 1. !!P R. [| P --> False; P |] ==> False} -\ttbreak -by (eresolve_tac [mp] 1); -{\out Level 2} -{\out !!P R. [| ~ P; P |] ==> R} -{\out 1. !!P R. P ==> P} -\ttbreak -by (assume_tac 1); -{\out Level 3} -{\out !!P R. [| ~ P; P |] ==> R} -{\out No subgoals!} -\end{ttbox} -Calling \ttindex{qed} strips the meta-quantifiers, so the resulting -theorem is the same as before. -\begin{ttbox} -qed "notE"; -{\out val notE = "[| ~?P; ?P |] ==> ?R" : thm} -\end{ttbox} -Do not use the {\tt!!}\ trick if the premises contain meta-level -connectives, because \ttindex{eresolve_tac} and \ttindex{assume_tac} would -not be able to handle the resulting assumptions. The trick is not suitable -for deriving the introduction rule~$(\neg I)$. +\index{definitions!and derived rules|)} \section{Defining theories}\label{sec:defining-theories} @@ -353,7 +286,7 @@ sort for type variables. A constant declaration can specify an associated concrete syntax. The translations section specifies rewrite rules on abstract syntax trees, handling notations and -abbreviations. \index{*ML section} The {\tt ML} section may contain +abbreviations. \index{*ML section} The \texttt{ML} section may contain code to perform arbitrary syntactic transformations. The main declaration forms are discussed below. There are some more sections not presented here, the full syntax can be found in @@ -377,16 +310,16 @@ T}{\tt.thy}, writes a corresponding file of {\ML} code {\tt.{\it T}.thy.ML}, reads the latter file, and deletes it if no errors occurred. This declares the {\ML} structure~$T$, which contains a -component {\tt thy} denoting the new theory, a component for each +component \texttt{thy} denoting the new theory, a component for each rule, and everything declared in {\it ML code}. Errors may arise during the translation to {\ML} (say, a misspelled keyword) or during creation of the new theory (say, a type error in a -rule). But if all goes well, {\tt use_thy} will finally read the file +rule). But if all goes well, \texttt{use_thy} will finally read the file {\it T}{\tt.ML} (if it exists). This file typically contains proofs that refer to the components of~$T$. The structure is automatically opened, so its components may be referred to by unqualified names, -e.g.\ just {\tt thy} instead of $T${\tt .thy}. +e.g.\ just \texttt{thy} instead of $T$\texttt{.thy}. \ttindexbold{use_thy} automatically loads a theory's parents before loading the theory itself. When a theory file is modified, many @@ -409,7 +342,7 @@ \end{ttbox} where $c@1$, \ldots, $c@n$ are constants and $\tau@1$, \ldots, $\tau@n$ are types. The types must be enclosed in quotation marks if they contain -user-declared infix type constructors like {\tt *}. Each +user-declared infix type constructors like \texttt{*}. Each constant must be enclosed in quotation marks unless it is a valid identifier. To declare $c@1$, \ldots, $c@n$ as constants of type $\tau$, the $n$ declarations may be abbreviated to a single line: @@ -427,7 +360,7 @@ enclosed in quotation marks. \indexbold{definitions} The {\bf definition part} is similar, but with -the keyword {\tt defs} instead of {\tt rules}. {\bf Definitions} are +the keyword \texttt{defs} instead of \texttt{rules}. {\bf Definitions} are rules of the form $s \equiv t$, and should serve only as abbreviations. The simplest form of a definition is $f \equiv t$, where $f$ is a constant. Also allowed are $\eta$-equivalent forms of @@ -460,7 +393,7 @@ "xor(P,Q) == P & ~Q | ~P & Q" end \end{ttbox} -{\tt constdefs} generates the names {\tt nand_def} and {\tt xor_def} +\texttt{constdefs} generates the names \texttt{nand_def} and \texttt{xor_def} automatically, which is why it is restricted to alphanumeric identifiers. In general it has the form \begin{ttbox} @@ -478,7 +411,7 @@ \begin{ttbox} defs prime_def "prime(p) == (m divides p) --> (m=1 | m=p)" \end{ttbox} -Isabelle rejects this ``definition'' because of the extra {\tt m} on the +Isabelle rejects this ``definition'' because of the extra \texttt{m} on the right-hand side, which would introduce an inconsistency. What you should have written is \begin{ttbox} @@ -544,11 +477,11 @@ constructor~$fun$ has the arity $(logic,logic)logic$; in higher-order logic, it is declared also to have arity $(term,term)term$. -Theory {\tt List} declares the 1-place type constructor $list$, gives -it arity $(term)term$, and declares constants $Nil$ and $Cons$ with +Theory \texttt{List} declares the 1-place type constructor $list$, gives +it the arity $(term)term$, and declares constants $Nil$ and $Cons$ with polymorphic types:% -\footnote{In the {\tt consts} part, type variable {\tt'a} has the default - sort, which is {\tt term}. See the {\em Reference Manual\/} +\footnote{In the \texttt{consts} part, type variable {\tt'a} has the default + sort, which is \texttt{term}. See the {\em Reference Manual\/} \iflabelundefined{sec:ref-defining-theories}{}% {(\S\ref{sec:ref-defining-theories})} for more information.} \index{examples!of theories} @@ -634,10 +567,10 @@ If :: [o,o,o] => o ("if _ then _ else _") \end{ttbox} This declares a constant $If$ of type $[o,o,o] \To o$ with concrete syntax {\tt - if~$P$ then~$Q$ else~$R$} as well as {\tt If($P$,$Q$,$R$)}. Underscores + if~$P$ then~$Q$ else~$R$} as well as \texttt{If($P$,$Q$,$R$)}. Underscores denote argument positions. -The declaration above does not allow the {\tt if}-{\tt then}-{\tt +The declaration above does not allow the \texttt{if}-\texttt{then}-{\tt else} construct to be printed split across several lines, even if it is too long to fit on one line. Pretty-printing information can be added to specify the layout of mixfix operators. For details, see @@ -661,7 +594,7 @@ If :: [o,o,o] => o ("if _ then _ else _" [100,0,0] 99) \end{ttbox} defines concrete syntax for a conditional whose first argument cannot have -the form {\tt if~$P$ then~$Q$ else~$R$} because it must have a priority +the form \texttt{if~$P$ then~$Q$ else~$R$} because it must have a priority of at least~100. We may of course write \begin{quote}\tt if (if $P$ then $Q$ else $R$) then $S$ else $T$ @@ -686,10 +619,10 @@ \end{ttbox} \begin{warn} - The name of the type constructor is~{\tt *} and not {\tt op~*}, as + The name of the type constructor is~\texttt{*} and not \texttt{op~*}, as it would be in the case of an infix constant. Only infix type - constructors can have symbolic names like~{\tt *}. General mixfix - syntax for types may be introduced via appropriate {\tt syntax} + constructors can have symbolic names like~\texttt{*}. General mixfix + syntax for types may be introduced via appropriate \texttt{syntax} declarations. \end{warn} @@ -840,16 +773,16 @@ add_def "m+n == rec(m, n, \%x y. Suc(y))" end \end{ttbox} -In axiom {\tt add_def}, recall that \verb|%| stands for~$\lambda$. -Loading this theory file creates the \ML\ structure {\tt Nat}, which +In axiom \texttt{add_def}, recall that \verb|%| stands for~$\lambda$. +Loading this theory file creates the \ML\ structure \texttt{Nat}, which contains the theory and axioms. \subsection{Proving some recursion equations} -File {\tt FOL/ex/Nat.ML} contains proofs involving this theory of the +Theory \texttt{FOL/ex/Nat} contains proofs involving this theory of the natural numbers. As a trivial example, let us derive recursion equations for \verb$+$. Here is the zero case: \begin{ttbox} -goalw Nat.thy [add_def] "0+n = n"; +Goalw [add_def] "0+n = n"; {\out Level 0} {\out 0 + n = n} {\out 1. rec(0,n,\%x y. Suc(y)) = n} @@ -862,7 +795,7 @@ \end{ttbox} And here is the successor case: \begin{ttbox} -goalw Nat.thy [add_def] "Suc(m)+n = Suc(m+n)"; +Goalw [add_def] "Suc(m)+n = Suc(m+n)"; {\out Level 0} {\out Suc(m) + n = Suc(m + n)} {\out 1. rec(Suc(m),n,\%x y. Suc(y)) = Suc(rec(m,n,\%x y. Suc(y)))} @@ -889,7 +822,7 @@ $\forall n.\Var{P}(n)$ --- but putting a subgoal into this form requires refinement by~$(\forall E)$, which is equally hard! -The tactic {\tt res_inst_tac}, like {\tt resolve_tac}, refines a subgoal by +The tactic \texttt{res_inst_tac}, like \texttt{resolve_tac}, refines a subgoal by a rule. But it also accepts explicit instantiations for the rule's schematic variables. \begin{description} @@ -908,7 +841,7 @@ in the context of a particular subgoal: free variables receive the same types as they have in the subgoal, and parameters may appear. Type variable instantiations may appear in~{\it insts}, but they are seldom -required: {\tt res_inst_tac} instantiates type variables automatically +required: \texttt{res_inst_tac} instantiates type variables automatically whenever the type of~$e@i$ is an instance of the type of~$\Var{v@i}$. \subsection{A simple proof by induction} @@ -917,7 +850,7 @@ use~$(induct)$, we instantiate~$\Var{n}$ to~$k$; Isabelle finds a good instantiation for~$\Var{P}$. \begin{ttbox} -goal Nat.thy "~ (Suc(k) = k)"; +Goal "~ (Suc(k) = k)"; {\out Level 0} {\out Suc(k) ~= k} {\out 1. Suc(k) ~= k} @@ -932,7 +865,7 @@ is the base case, with $k$ replaced by~0. Subgoal~2 is the inductive step, with $k$ replaced by~$Suc(x)$ and with an induction hypothesis for~$x$. The rest of the proof demonstrates~\tdx{notI}, \tdx{notE} and the -other rules of theory {\tt Nat}. The base case holds by~\ttindex{Suc_neq_0}: +other rules of theory \texttt{Nat}. The base case holds by~\ttindex{Suc_neq_0}: \begin{ttbox} by (resolve_tac [notI] 1); {\out Level 2} @@ -966,14 +899,14 @@ \end{ttbox} -\subsection{An example of ambiguity in {\tt resolve_tac}} +\subsection{An example of ambiguity in \texttt{resolve_tac}} \index{examples!of induction}\index{unification!higher-order} -If you try the example above, you may observe that {\tt res_inst_tac} is +If you try the example above, you may observe that \texttt{res_inst_tac} is not actually needed. Almost by chance, \ttindex{resolve_tac} finds the right instantiation for~$(induct)$ to yield the desired next state. With more complex formulae, our luck fails. \begin{ttbox} -goal Nat.thy "(k+m)+n = k+(m+n)"; +Goal "(k+m)+n = k+(m+n)"; {\out Level 0} {\out k + m + n = k + (m + n)} {\out 1. k + m + n = k + (m + n)} @@ -1036,14 +969,14 @@ be packaged into a {\bf simplification set},\index{simplification sets} or {\bf simpset}. We augment the implicit simpset of {\FOL} with the equations proved in the previous section, namely $0+n=n$ and -${\tt Suc}(m)+n={\tt Suc}(m+n)$: +$\texttt{Suc}(m)+n=\texttt{Suc}(m+n)$: \begin{ttbox} Addsimps [add_0, add_Suc]; \end{ttbox} We state the goal for associativity of addition, and use \ttindex{res_inst_tac} to invoke induction on~$k$: \begin{ttbox} -goal Nat.thy "(k+m)+n = k+(m+n)"; +Goal "(k+m)+n = k+(m+n)"; {\out Level 0} {\out k + m + n = k + (m + n)} {\out 1. k + m + n = k + (m + n)} @@ -1082,7 +1015,7 @@ \index{Prolog interpreter|bold} To demonstrate the power of tacticals, let us construct a Prolog interpreter and execute programs involving lists.\footnote{To run these -examples, see the file {\tt FOL/ex/Prolog.ML}.} The Prolog program +examples, see the file \texttt{FOL/ex/Prolog.ML}.} The Prolog program consists of a theory. We declare a type constructor for lists, with an arity declaration to say that $(\tau)list$ is of class~$term$ provided~$\tau$ is: @@ -1111,7 +1044,7 @@ \index{examples!of theories} Theory \thydx{Prolog} extends first-order logic in order to make use of the class~$term$ and the type~$o$. The interpreter does not use the -rules of~{\tt FOL}. +rules of~\texttt{FOL}. \begin{ttbox} Prolog = FOL + types 'a list @@ -1129,9 +1062,9 @@ \subsection{Simple executions} Repeated application of the rules solves Prolog goals. Let us append the lists $[a,b,c]$ and~$[d,e]$. As the rules are applied, the -answer builds up in~{\tt ?x}. +answer builds up in~\texttt{?x}. \begin{ttbox} -goal Prolog.thy "app(a:b:c:Nil, d:e:Nil, ?x)"; +Goal "app(a:b:c:Nil, d:e:Nil, ?x)"; {\out Level 0} {\out app(a : b : c : Nil, d : e : Nil, ?x)} {\out 1. app(a : b : c : Nil, d : e : Nil, ?x)} @@ -1163,7 +1096,7 @@ with $[c,d]$ to produce $[a,b,c,d]$? Using \ttindex{REPEAT}, we find the answer at once, $[a,b]$: \begin{ttbox} -goal Prolog.thy "app(?x, c:d:Nil, a:b:c:d:Nil)"; +Goal "app(?x, c:d:Nil, a:b:c:d:Nil)"; {\out Level 0} {\out app(?x, c : d : Nil, a : b : c : d : Nil)} {\out 1. app(?x, c : d : Nil, a : b : c : d : Nil)} @@ -1181,7 +1114,7 @@ question has five solutions. Using \ttindex{REPEAT} to apply the rules, we quickly find the first solution, namely $x=[]$ and $y=[a,b,c,d]$: \begin{ttbox} -goal Prolog.thy "app(?x, ?y, a:b:c:d:Nil)"; +Goal "app(?x, ?y, a:b:c:d:Nil)"; {\out Level 0} {\out app(?x, ?y, a : b : c : d : Nil)} {\out 1. app(?x, ?y, a : b : c : d : Nil)} @@ -1221,11 +1154,11 @@ \subsection{Depth-first search} \index{search!depth-first} Now let us try $rev$, reversing a list. -Bundle the rules together as the \ML{} identifier {\tt rules}. Naive +Bundle the rules together as the \ML{} identifier \texttt{rules}. Naive reverse requires 120 inferences for this 14-element list, but the tactic terminates in a few seconds. \begin{ttbox} -goal Prolog.thy "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)"; +Goal "rev(a:b:c:d:e:f:g:h:i:j:k:l:m:n:Nil, ?w)"; {\out Level 0} {\out rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil, ?w)} {\out 1. rev(a : b : c : d : e : f : g : h : i : j : k : l : m : n : Nil,} @@ -1242,7 +1175,7 @@ We may execute $rev$ backwards. This, too, should reverse a list. What is the reverse of $[a,b,c]$? \begin{ttbox} -goal Prolog.thy "rev(?x, a:b:c:Nil)"; +Goal "rev(?x, a:b:c:Nil)"; {\out Level 0} {\out rev(?x, a : b : c : Nil)} {\out 1. rev(?x, a : b : c : Nil)} @@ -1269,7 +1202,7 @@ {\out No subgoals!} \end{ttbox} \ttindex{REPEAT} goes wrong because it is only a repetition tactical, not a -search tactical. {\tt REPEAT} stops when it cannot continue, regardless of +search tactical. \texttt{REPEAT} stops when it cannot continue, regardless of which state is reached. The tactical \ttindex{DEPTH_FIRST} searches for a satisfactory state, as specified by an \ML{} predicate. Below, \ttindex{has_fewer_prems} specifies that the proof state should have no @@ -1280,7 +1213,7 @@ \end{ttbox} Since Prolog uses depth-first search, this tactic is a (slow!) Prolog interpreter. We return to the start of the proof using -\ttindex{choplev}, and apply {\tt prolog_tac}: +\ttindex{choplev}, and apply \texttt{prolog_tac}: \begin{ttbox} choplev 0; {\out Level 0} @@ -1292,9 +1225,9 @@ {\out rev(c : b : a : Nil, a : b : c : Nil)} {\out No subgoals!} \end{ttbox} -Let us try {\tt prolog_tac} on one more example, containing four unknowns: +Let us try \texttt{prolog_tac} on one more example, containing four unknowns: \begin{ttbox} -goal Prolog.thy "rev(a:?x:c:?y:Nil, d:?z:b:?u)"; +Goal "rev(a:?x:c:?y:Nil, d:?z:b:?u)"; {\out Level 0} {\out rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)} {\out 1. rev(a : ?x : c : ?y : Nil, d : ?z : b : ?u)}

--- a/doc-src/Intro/getting.tex Tue Jul 28 16:30:56 1998 +0200 +++ b/doc-src/Intro/getting.tex Tue Jul 28 16:33:43 1998 +0200 @@ -12,9 +12,9 @@ Object-logics are built upon Pure Isabelle, which implements the meta-logic and provides certain fundamental data structures: types, terms, signatures, theorems and theories, tactics and tacticals. -These data structures have the corresponding \ML{} types {\tt typ}, -{\tt term}, {\tt Sign.sg}, {\tt thm}, {\tt theory} and {\tt tactic}; -tacticals have function types such as {\tt tactic->tactic}. Isabelle +These data structures have the corresponding \ML{} types \texttt{typ}, +\texttt{term}, \texttt{Sign.sg}, \texttt{thm}, \texttt{theory} and \texttt{tactic}; +tacticals have function types such as \texttt{tactic->tactic}. Isabelle users can operate on these data structures by writing \ML{} programs. @@ -33,7 +33,7 @@ \index{identifiers}\index{reserved words} An {\bf identifier} is a string of letters, digits, underscores~(\verb|_|) and single quotes~({\tt'}), beginning with a letter. Single quotes are -regarded as primes; for instance {\tt x'} is read as~$x'$. Identifiers are +regarded as primes; for instance \texttt{x'} is read as~$x'$. Identifiers are separated by white space and special characters. {\bf Reserved words} are identifiers that appear in Isabelle syntax definitions. @@ -78,7 +78,7 @@ \index{types!syntax of|bold}\index{sort constraints} Types are written with a syntax like \ML's. The built-in type \tydx{prop} is the type of propositions. Type variables can be constrained to particular -classes or sorts, for example {\tt 'a::term} and {\tt ?'b::\ttlbrace +classes or sorts, for example \texttt{'a::term} and \texttt{?'b::\ttlbrace ord, arith\ttrbrace}. \[\dquotes \index{*:: symbol}\index{*=> symbol} @@ -116,7 +116,7 @@ The theorems and rules of an object-logic are represented by theorems in the meta-logic, which are expressed using meta-formulae. Since the meta-logic is higher-order, meta-formulae~$\phi$, $\psi$, $\theta$,~\ldots{} -are just terms of type~{\tt prop}. +are just terms of type~\texttt{prop}. \index{meta-implication} \index{meta-quantifiers}\index{meta-equality} \index{*"!"! symbol}\index{*"["| symbol}\index{*"|"] symbol} @@ -146,7 +146,7 @@ prevent such ambiguities, Isabelle's syntax does not allow a meta-formula to consist of a variable. Variables of type~\tydx{prop} are seldom useful, but you can make a variable stand for a meta-formula by prefixing -it with the symbol {\tt PROP}:\index{*PROP symbol} +it with the symbol \texttt{PROP}:\index{*PROP symbol} \begin{ttbox} PROP ?psi ==> PROP ?theta \end{ttbox} @@ -201,9 +201,9 @@ represented by a function from theorems to theorems. Object-level rules are taken as axioms. -The main theorem printing commands are {\tt prth}, {\tt prths} and~{\tt - prthq}. Of the other operations on theorems, most useful are {\tt RS} -and {\tt RSN}, which perform resolution. +The main theorem printing commands are \texttt{prth}, \texttt{prths} and~{\tt + prthq}. Of the other operations on theorems, most useful are \texttt{RS} +and \texttt{RSN}, which perform resolution. \index{theorems!printing of} \begin{ttdescription} @@ -250,11 +250,11 @@ }~\ldots{} is compiler-dependent and will sometimes be suppressed. This session illustrates two formats for the display of theorems. Isabelle's top-level displays theorems as \ML{} values, enclosed in quotes. Printing -commands like {\tt prth} omit the quotes and the surrounding {\tt val +commands like \texttt{prth} omit the quotes and the surrounding \texttt{val \ldots :\ thm}. Ignoring their side-effects, the commands are identity functions. -To contrast {\tt RS} with {\tt RSN}, we resolve +To contrast \texttt{RS} with \texttt{RSN}, we resolve \tdx{conjunct1}, which stands for~$(\conj E1)$, with~\tdx{mp}. \begin{ttbox} conjunct1 RS mp; @@ -269,8 +269,8 @@ \] % Rules can be derived by pasting other rules together. Let us join -\tdx{spec}, which stands for~$(\forall E)$, with {\tt mp} and {\tt - conjunct1}. In \ML{}, the identifier~{\tt it} denotes the value just +\tdx{spec}, which stands for~$(\forall E)$, with \texttt{mp} and {\tt + conjunct1}. In \ML{}, the identifier~\texttt{it} denotes the value just printed. \begin{ttbox} spec; @@ -302,7 +302,7 @@ procedure does not enumerate the unifiers; instead, it retains flex-flex equations as constraints on future unifications. Flex-flex constraints occasionally become attached to a proof state; more frequently, they appear -during use of {\tt RS} and~{\tt RSN}: +during use of \texttt{RS} and~\texttt{RSN}: \begin{ttbox} refl; {\out val it = "?a = ?a" : thm} @@ -333,7 +333,7 @@ $\Var{g}\equiv\lambda y.?h(k(y))$. \begin{warn} -\ttindex{RS} and \ttindex{RSN} fail (by raising exception {\tt THM}) unless +\ttindex{RS} and \ttindex{RSN} fail (by raising exception \texttt{THM}) unless the resolution delivers {\bf exactly one} resolvent. For multiple results, use \ttindex{RL} and \ttindex{RLN}, which operate on theorem lists. The following example uses \ttindex{read_instantiate} to create an instance @@ -362,14 +362,14 @@ \index{forward proof|)} \section{Backward proof} -Although {\tt RS} and {\tt RSN} are fine for simple forward reasoning, +Although \texttt{RS} and \texttt{RSN} are fine for simple forward reasoning, large proofs require tactics. Isabelle provides a suite of commands for conducting a backward proof using tactics. \subsection{The basic tactics} -The tactics {\tt assume_tac}, {\tt -resolve_tac}, {\tt eresolve_tac}, and {\tt dresolve_tac} suffice for most -single-step proofs. Although {\tt eresolve_tac} and {\tt dresolve_tac} are +The tactics \texttt{assume_tac}, {\tt +resolve_tac}, \texttt{eresolve_tac}, and \texttt{dresolve_tac} suffice for most +single-step proofs. Although \texttt{eresolve_tac} and \texttt{dresolve_tac} are not strictly necessary, they simplify proofs involving elimination and destruction rules. All the tactics act on a subgoal designated by a positive integer~$i$, failing if~$i$ is out of range. The resolution @@ -391,9 +391,9 @@ none of the rules generates next states. \item[\ttindex{eresolve_tac} {\it thms} {\it i}] \index{elim-resolution} - performs elim-resolution. Like {\tt resolve_tac~{\it thms}~{\it i\/}} - followed by {\tt assume_tac~{\it i}}, it applies a rule then solves its - first premise by assumption. But {\tt eresolve_tac} additionally deletes + performs elim-resolution. Like \texttt{resolve_tac~{\it thms}~{\it i\/}} + followed by \texttt{assume_tac~{\it i}}, it applies a rule then solves its + first premise by assumption. But \texttt{eresolve_tac} additionally deletes that assumption from any subgoals arising from the resolution. \item[\ttindex{dresolve_tac} {\it thms} {\it i}] @@ -410,7 +410,7 @@ backtracking through the proof space, going away to prove lemmas, etc.; of its many commands, most important are the following: \begin{ttdescription} -\item[\ttindex{goal} {\it theory} {\it formula}; ] +\item[\ttindex{Goal} {\it formula}; ] begins a new proof, where $theory$ is usually an \ML\ identifier and the {\it formula\/} is written as an \ML\ string. @@ -428,7 +428,7 @@ unproved subgoals are left, etc. \item[\ttindex{qed} {\it name};] is the usual way of ending a proof. - It gets the theorem using {\tt result}, stores it in Isabelle's + It gets the theorem using \texttt{result}, stores it in Isabelle's theorem database and binds it to an \ML{} identifier. \end{ttdescription} @@ -451,21 +451,19 @@ \subsection{A trivial example in propositional logic} \index{examples!propositional} -Directory {\tt FOL} of the Isabelle distribution defines the theory of +Directory \texttt{FOL} of the Isabelle distribution defines the theory of first-order logic. Let us try the example from \S\ref{prop-proof}, entering the goal $P\disj P\imp P$ in that theory.\footnote{To run these - examples, see the file {\tt FOL/ex/intro.ML}. The files {\tt README} and - {\tt Makefile} on the directories {\tt Pure} and {\tt FOL} explain how to - build first-order logic.} + examples, see the file \texttt{FOL/ex/intro.ML}.} \begin{ttbox} -goal FOL.thy "P|P --> P"; +Goal "P|P --> P"; {\out Level 0} {\out P | P --> P} {\out 1. P | P --> P} \end{ttbox}\index{level of a proof} Isabelle responds by printing the initial proof state, which has $P\disj P\imp P$ as the main goal and the only subgoal. The {\bf level} of the -state is the number of {\tt by} commands that have been applied to reach +state is the number of \texttt{by} commands that have been applied to reach it. We now use \ttindex{resolve_tac} to apply the rule \tdx{impI}, or~$({\imp}I)$, to subgoal~1: \begin{ttbox} @@ -496,7 +494,7 @@ {\out 1. P | P ==> ?P1 | P} {\out 2. [| P | P; ?P1 |] ==> P} \end{ttbox} -Next we tackle subgoal~2, instantiating {\tt?P1} to~{\tt P} in subgoal~1. +Next we tackle subgoal~2, instantiating {\tt?P1} to~\texttt{P} in subgoal~1. \begin{ttbox} by (assume_tac 2); {\out Level 4} @@ -511,12 +509,12 @@ {\out No subgoals!} \end{ttbox} Isabelle tells us that there are no longer any subgoals: the proof is -complete. Calling {\tt qed} stores the theorem. +complete. Calling \texttt{qed} stores the theorem. \begin{ttbox} qed "mythm"; {\out val mythm = "?P | ?P --> ?P" : thm} \end{ttbox} -Isabelle has replaced the free variable~{\tt P} by the scheme +Isabelle has replaced the free variable~\texttt{P} by the scheme variable~{\tt?P}\@. Free variables in the proof state remain fixed throughout the proof. Isabelle finally converts them to scheme variables so that the resulting theorem can be instantiated with any formula. @@ -528,12 +526,12 @@ \subsection{Part of a distributive law} \index{examples!propositional} To demonstrate the tactics \ttindex{eresolve_tac}, \ttindex{dresolve_tac} -and the tactical {\tt REPEAT}, let us prove part of the distributive +and the tactical \texttt{REPEAT}, let us prove part of the distributive law \[ (P\conj Q)\disj R \,\bimp\, (P\disj R)\conj (Q\disj R). \] We begin by stating the goal to Isabelle and applying~$({\imp}I)$ to it: \begin{ttbox} -goal FOL.thy "(P & Q) | R --> (P | R)"; +Goal "(P & Q) | R --> (P | R)"; {\out Level 0} {\out P & Q | R --> P | R} {\out 1. P & Q | R --> P | R} @@ -543,7 +541,7 @@ {\out P & Q | R --> P | R} {\out 1. P & Q | R ==> P | R} \end{ttbox} -Previously we applied~(${\disj}E)$ using {\tt resolve_tac}, but +Previously we applied~(${\disj}E)$ using \texttt{resolve_tac}, but \ttindex{eresolve_tac} deletes the assumption after use. The resulting proof state is simpler. \begin{ttbox} @@ -556,9 +554,9 @@ Using \ttindex{dresolve_tac}, we can apply~(${\conj}E1)$ to subgoal~1, replacing the assumption $P\conj Q$ by~$P$. Normally we should apply the rule~(${\conj}E)$, given in~\S\ref{destruct}. That is an elimination rule -and requires {\tt eresolve_tac}; it would replace $P\conj Q$ by the two +and requires \texttt{eresolve_tac}; it would replace $P\conj Q$ by the two assumptions~$P$ and~$Q$. Because the present example does not need~$Q$, we -may try out {\tt dresolve_tac}. +may try out \texttt{dresolve_tac}. \begin{ttbox} by (dresolve_tac [conjunct1] 1); {\out Level 3} @@ -580,8 +578,8 @@ {\out 1. P ==> P} {\out 2. R ==> R} \end{ttbox} -Two calls of {\tt assume_tac} can finish the proof. The -tactical~\ttindex{REPEAT} here expresses a tactic that calls {\tt assume_tac~1} +Two calls of \texttt{assume_tac} can finish the proof. The +tactical~\ttindex{REPEAT} here expresses a tactic that calls \texttt{assume_tac~1} as many times as possible. We can restrict attention to subgoal~1 because the other subgoals move up after subgoal~1 disappears. \begin{ttbox} @@ -617,7 +615,7 @@ The proof of $\forall x.\exists y.x=y$ demonstrates the introduction rules $(\forall I)$ and~$(\exists I)$. We state the goal and apply $(\forall I)$: \begin{ttbox} -goal FOL.thy "ALL x. EX y. x=y"; +Goal "ALL x. EX y. x=y"; {\out Level 0} {\out ALL x. EX y. x = y} {\out 1. ALL x. EX y. x = y} @@ -627,9 +625,9 @@ {\out ALL x. EX y. x = y} {\out 1. !!x. EX y. x = y} \end{ttbox} -The variable~{\tt x} is no longer universally quantified, but is a +The variable~\texttt{x} is no longer universally quantified, but is a parameter in the subgoal; thus, it is universally quantified at the -meta-level. The subgoal must be proved for all possible values of~{\tt x}. +meta-level. The subgoal must be proved for all possible values of~\texttt{x}. To remove the existential quantifier, we apply the rule $(\exists I)$: \begin{ttbox} @@ -638,9 +636,9 @@ {\out ALL x. EX y. x = y} {\out 1. !!x. x = ?y1(x)} \end{ttbox} -The bound variable {\tt y} has become {\tt?y1(x)}. This term consists of -the function unknown~{\tt?y1} applied to the parameter~{\tt x}. -Instances of {\tt?y1(x)} may or may not contain~{\tt x}. We resolve the +The bound variable \texttt{y} has become {\tt?y1(x)}. This term consists of +the function unknown~{\tt?y1} applied to the parameter~\texttt{x}. +Instances of {\tt?y1(x)} may or may not contain~\texttt{x}. We resolve the subgoal with the reflexivity axiom. \begin{ttbox} by (resolve_tac [refl] 1); @@ -658,7 +656,7 @@ We state the goal $\exists y.\forall x.x=y$, which is not a theorem, and try~$(\exists I)$: \begin{ttbox} -goal FOL.thy "EX y. ALL x. x=y"; +Goal "EX y. ALL x. x=y"; {\out Level 0} {\out EX y. ALL x. x = y} {\out 1. EX y. ALL x. x = y} @@ -668,8 +666,8 @@ {\out EX y. ALL x. x = y} {\out 1. ALL x. x = ?y} \end{ttbox} -The unknown {\tt ?y} may be replaced by any term, but this can never -introduce another bound occurrence of~{\tt x}. We now apply~$(\forall I)$: +The unknown \texttt{?y} may be replaced by any term, but this can never +introduce another bound occurrence of~\texttt{x}. We now apply~$(\forall I)$: \begin{ttbox} by (resolve_tac [allI] 1); {\out Level 2} @@ -677,7 +675,7 @@ {\out 1. !!x. x = ?y} \end{ttbox} Compare our position with the previous Level~2. Instead of {\tt?y1(x)} we -have~{\tt?y}, whose instances may not contain the bound variable~{\tt x}. +have~{\tt?y}, whose instances may not contain the bound variable~\texttt{x}. The reflexivity axiom does not unify with subgoal~1. \begin{ttbox} by (resolve_tac [refl] 1); @@ -696,10 +694,10 @@ will demonstrate how parameters and unknowns develop. If they appear in the wrong order, the proof will fail. -This section concludes with a demonstration of {\tt REPEAT} -and~{\tt ORELSE}. +This section concludes with a demonstration of \texttt{REPEAT} +and~\texttt{ORELSE}. \begin{ttbox} -goal FOL.thy "(ALL x y.P(x,y)) --> (ALL z w.P(w,z))"; +Goal "(ALL x y.P(x,y)) --> (ALL z w.P(w,z))"; {\out Level 0} {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} {\out 1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} @@ -711,7 +709,7 @@ \end{ttbox} \paragraph{The wrong approach.} -Using {\tt dresolve_tac}, we apply the rule $(\forall E)$, bound to the +Using \texttt{dresolve_tac}, we apply the rule $(\forall E)$, bound to the \ML\ identifier \tdx{spec}. Then we apply $(\forall I)$. \begin{ttbox} by (dresolve_tac [spec] 1); @@ -724,7 +722,7 @@ {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} {\out 1. !!z. ALL y. P(?x1,y) ==> ALL w. P(w,z)} \end{ttbox} -The unknown {\tt ?x1} and the parameter {\tt z} have appeared. We again +The unknown \texttt{?x1} and the parameter \texttt{z} have appeared. We again apply $(\forall E)$ and~$(\forall I)$. \begin{ttbox} by (dresolve_tac [spec] 1); @@ -737,10 +735,10 @@ {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} {\out 1. !!z w. P(?x1,?y3(z)) ==> P(w,z)} \end{ttbox} -The unknown {\tt ?y3} and the parameter {\tt w} have appeared. Each +The unknown \texttt{?y3} and the parameter \texttt{w} have appeared. Each unknown is applied to the parameters existing at the time of its creation; -instances of~{\tt ?x1} cannot contain~{\tt z} or~{\tt w}, while instances -of {\tt?y3(z)} can only contain~{\tt z}. Due to the restriction on~{\tt ?x1}, +instances of~\texttt{?x1} cannot contain~\texttt{z} or~\texttt{w}, while instances +of {\tt?y3(z)} can only contain~\texttt{z}. Due to the restriction on~\texttt{?x1}, proof by assumption will fail. \begin{ttbox} by (assume_tac 1); @@ -771,7 +769,7 @@ {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} {\out 1. !!z w. ALL x y. P(x,y) ==> P(w,z)} \end{ttbox} -The parameters {\tt z} and~{\tt w} have appeared. We now create the +The parameters \texttt{z} and~\texttt{w} have appeared. We now create the unknowns: \begin{ttbox} by (dresolve_tac [spec] 1); @@ -785,7 +783,7 @@ {\out 1. !!z w. P(?x3(z,w),?y4(z,w)) ==> P(w,z)} \end{ttbox} Both {\tt?x3(z,w)} and~{\tt?y4(z,w)} could become any terms containing {\tt -z} and~{\tt w}: +z} and~\texttt{w}: \begin{ttbox} by (assume_tac 1); {\out Level 6} @@ -825,9 +823,9 @@ \[ (\forall x. P(x) \imp Q) \,\bimp\, ((\exists x. P(x)) \imp Q). \] We state the left-to-right half to Isabelle in the normal way. Since $\imp$ is nested to the right, $({\imp}I)$ can be applied twice; we -use {\tt REPEAT}: +use \texttt{REPEAT}: \begin{ttbox} -goal FOL.thy "(ALL x.P(x) --> Q) --> (EX x.P(x)) --> Q"; +Goal "(ALL x.P(x) --> Q) --> (EX x.P(x)) --> Q"; {\out Level 0} {\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} {\out 1. (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} @@ -857,7 +855,7 @@ {\out 1. !!x. [| P(x); P(?x3(x)) --> Q |] ==> Q} \end{ttbox} Because we applied $(\exists E)$ before $(\forall E)$, the unknown -term~{\tt?x3(x)} may depend upon the parameter~{\tt x}. +term~{\tt?x3(x)} may depend upon the parameter~\texttt{x}. Although $({\imp}E)$ is a destruction rule, it works with \ttindex{eresolve_tac} to perform backward chaining. This technique is @@ -868,8 +866,8 @@ {\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} {\out 1. !!x. P(x) ==> P(?x3(x))} \end{ttbox} -The tactic has reduced~{\tt Q} to~{\tt P(?x3(x))}, deleting the -implication. The final step is trivial, thanks to the occurrence of~{\tt x}. +The tactic has reduced~\texttt{Q} to~\texttt{P(?x3(x))}, deleting the +implication. The final step is trivial, thanks to the occurrence of~\texttt{x}. \begin{ttbox} by (assume_tac 1); {\out Level 5} @@ -895,7 +893,7 @@ backslashes~\hbox{\verb|\|\ldots\verb|\|} are an \ML{} string escape sequence, to break the long string over two lines.) \begin{ttbox} -goal FOL.thy "(EX y. ALL x. J(y,x) <-> ~J(x,x)) \ttback +Goal "(EX y. ALL x. J(y,x) <-> ~J(x,x)) \ttback \ttback --> ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"; {\out Level 0} {\out (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->} @@ -914,10 +912,10 @@ {\out No subgoals!} \end{ttbox} Sceptics may examine the proof by calling the package's single-step -tactics, such as~{\tt step_tac}. This would take up much space, however, +tactics, such as~\texttt{step_tac}. This would take up much space, however, so let us proceed to the next example: \begin{ttbox} -goal FOL.thy "ALL x. P(x,f(x)) <-> \ttback +Goal "ALL x. P(x,f(x)) <-> \ttback \ttback (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"; {\out Level 0} {\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))}

--- a/doc-src/Intro/intro.ind Tue Jul 28 16:30:56 1998 +0200 +++ b/doc-src/Intro/intro.ind Tue Jul 28 16:33:43 1998 +0200 @@ -1,7 +1,6 @@ \begin{theindex} \item {\tt !!} symbol, 26 - \subitem in main goal, 46 \item {\tt\%} symbol, 25 \item {\tt ::} symbol, 25 \item {\tt ==} symbol, 26 @@ -19,9 +18,9 @@ \item {\tt allI} theorem, 38 \item arities - \subitem declaring, 4, \bold{49} - \item {\tt Asm_simp_tac}, 60 - \item {\tt assume_tac}, 30, 32, 38, 47 + \subitem declaring, 4, \bold{48} + \item {\tt Asm_simp_tac}, 59 + \item {\tt assume_tac}, 30, 32, 38 \item assumptions \subitem deleting, 20 \subitem discharge of, 7 @@ -29,14 +28,14 @@ \subitem of main goal, 41 \subitem use of, 16, 28 \item axioms - \subitem Peano, 55 + \subitem Peano, 54 \indexspace \item {\tt ba}, 31 - \item {\tt back}, 59, 63 + \item {\tt back}, 58, 62 \item backtracking - \subitem Prolog style, 62 + \subitem Prolog style, 61 \item {\tt bd}, 31 \item {\tt be}, 31 \item {\tt Blast_tac}, 39, 40 @@ -45,26 +44,26 @@ \indexspace - \item {\tt choplev}, 37, 38, 65 + \item {\tt choplev}, 37, 38, 64 \item classes, 3 \subitem built-in, \bold{25} \item classical reasoner, 39 \item {\tt conjunct1} theorem, 28 \item constants, 3 \subitem clashes with variables, 9 - \subitem declaring, \bold{48} - \subitem overloaded, 54 + \subitem declaring, \bold{47} + \subitem overloaded, 53 \subitem polymorphic, 3 - \item {\tt CPure} theory, 47 + \item {\tt CPure} theory, 46 \indexspace - \item definitions, 6, \bold{48} - \subitem and derived rules, 43--46 - \item {\tt DEPTH_FIRST}, 64 + \item definitions, 6, \bold{47} + \subitem and derived rules, 43--45 + \item {\tt DEPTH_FIRST}, 63 \item destruct-resolution, 22, 30 \item {\tt disjE} theorem, 31 - \item {\tt dres_inst_tac}, 57 + \item {\tt dres_inst_tac}, 56 \item {\tt dresolve_tac}, 30, 33, 39 \indexspace @@ -73,14 +72,14 @@ \item elim-resolution, \bold{20}, 30 \item equality \subitem polymorphic, 3 - \item {\tt eres_inst_tac}, 57 - \item {\tt eresolve_tac}, 30, 33, 39, 47 + \item {\tt eres_inst_tac}, 56 + \item {\tt eresolve_tac}, 30, 33, 39 \item examples \subitem of deriving rules, 41 - \subitem of induction, 57, 58 - \subitem of simplification, 60 + \subitem of induction, 56, 57 + \subitem of simplification, 59 \subitem of tacticals, 37 - \subitem of theories, 48, 50--54, 56, 61 + \subitem of theories, 47, 49--53, 55, 60 \subitem propositional, 17, 31, 33 \subitem with quantifiers, 18, 34, 36, 38 \item {\tt exE} theorem, 38 @@ -97,20 +96,20 @@ \indexspace - \item {\tt goal}, 30, 41, 46 - \item {\tt goalw}, 44--46 + \item {\tt Goal}, 30, 41 + \item {\tt Goalw}, 44 \indexspace - \item {\tt has_fewer_prems}, 64 + \item {\tt has_fewer_prems}, 63 \item higher-order logic, 4 \indexspace \item identifiers, 24 \item {\tt impI} theorem, 31, 44 - \item infixes, 52 - \item instantiation, 57--60 + \item infixes, 51 + \item instantiation, 56--59 \item Isabelle \subitem object-logics supported, i \subitem overview, i @@ -136,31 +135,31 @@ \item meta-implication, \bold{5}, 7, 26 \item meta-quantifiers, \bold{5}, 8, 26 \item meta-rewriting, 43 - \item mixfix declarations, 52, 53, 56 + \item mixfix declarations, 51, 52, 55 \item ML, i - \item {\tt ML} section, 47 + \item {\tt ML} section, 46 \item {\tt mp} theorem, 27, 28 \indexspace - \item {\tt Nat} theory, 56 + \item {\tt Nat} theory, 55 \item {\tt nat} type, 3 \item {\tt not_def} theorem, 44 - \item {\tt notE} theorem, \bold{45}, 58 - \item {\tt notI} theorem, \bold{44}, 58 + \item {\tt notE} theorem, 57 + \item {\tt notI} theorem, \bold{44}, 57 \indexspace \item {\tt o} type, 3, 4 \item {\tt ORELSE}, 38 - \item overloading, \bold{4}, 53 + \item overloading, \bold{4}, 52 \indexspace \item parameters, \bold{8}, 34 \subitem lifting over, 15 - \item {\tt Prolog} theory, 61 - \item Prolog interpreter, \bold{61} + \item {\tt Prolog} theory, 60 + \item Prolog interpreter, \bold{60} \item proof state, 16 \item proofs \subitem commands for, 30 @@ -170,33 +169,33 @@ \item {\tt prth}, 27 \item {\tt prthq}, 27, 29 \item {\tt prths}, 27 - \item {\tt Pure} theory, 47 + \item {\tt Pure} theory, 46 \indexspace - \item {\tt qed}, 31, 42, 46 + \item {\tt qed}, 31, 43 \item quantifiers, 5, 8, 34 \indexspace \item {\tt read_instantiate}, 29 \item {\tt refl} theorem, 29 - \item {\tt REPEAT}, 34, 38, 62, 64 - \item {\tt res_inst_tac}, 57, 60 + \item {\tt REPEAT}, 34, 38, 61, 63 + \item {\tt res_inst_tac}, 56, 59 \item reserved words, 24 \item resolution, 10, \bold{12} \subitem in backward proof, 15 - \subitem with instantiation, 57 - \item {\tt resolve_tac}, 30, 31, 46, 58 + \subitem with instantiation, 56 + \item {\tt resolve_tac}, 30, 31, 57 \item {\tt result}, 31 - \item {\tt rewrite_goals_tac}, 44 - \item {\tt rewrite_rule}, 45, 46 + \item {\tt rewrite_goals_tac}, 44, 45 + \item {\tt rewrite_rule}, 45 \item {\tt RL}, 29 \item {\tt RLN}, 29 - \item {\tt RS}, 27, 29, 46 + \item {\tt RS}, 27, 29 \item {\tt RSN}, 27, 29 \item rules - \subitem declaring, 48 + \subitem declaring, 47 \subitem derived, 13, \bold{22}, 41, 43 \subitem destruction, 21 \subitem elimination, 21 @@ -206,18 +205,18 @@ \indexspace \item search - \subitem depth-first, 63 + \subitem depth-first, 62 \item signatures, \bold{9} - \item {\tt Simp_tac}, 60 - \item simplification, 60 - \item simplification sets, 60 + \item {\tt Simp_tac}, 59 + \item simplification, 59 + \item simplification sets, 59 \item sort constraints, 25 \item sorts, \bold{5} \item {\tt spec} theorem, 28, 36, 38 \item {\tt standard}, 27 \item substitution, \bold{8} - \item {\tt Suc_inject}, 58 - \item {\tt Suc_neq_0}, 58 + \item {\tt Suc_inject}, 57 + \item {\tt Suc_neq_0}, 57 \item syntax \subitem of types and terms, 25 @@ -234,16 +233,16 @@ \subitem basic operations on, \bold{27} \subitem printing of, 27 \item theories, \bold{9} - \subitem defining, 47--57 + \subitem defining, 46--56 \item {\tt thm} ML type, 27 - \item {\tt topthm}, 42 + \item {\tt topthm}, 43 \item {\tt Trueprop} constant, 6, 7, 26 \item type constraints, 25 \item type constructors, 1 \item type identifiers, 25 - \item type synonyms, \bold{51} + \item type synonyms, \bold{50} \item types - \subitem declaring, \bold{49} + \subitem declaring, \bold{48} \subitem function, 1 \subitem higher, \bold{5} \subitem polymorphic, \bold{3} @@ -254,11 +253,11 @@ \item {\tt undo}, 31 \item unification - \subitem higher-order, \bold{11}, 58 + \subitem higher-order, \bold{11}, 57 \subitem incompleteness of, 11 \item unknowns, 10, 25, 34 \subitem function, \bold{11}, 29, 34 - \item {\tt use_thy}, \bold{47, 48} + \item {\tt use_thy}, \bold{46, 47} \indexspace

--- a/doc-src/Logics/FOL.tex Tue Jul 28 16:30:56 1998 +0200 +++ b/doc-src/Logics/FOL.tex Tue Jul 28 16:33:43 1998 +0200 @@ -678,7 +678,7 @@ The introduction rule, given the premises $P\Imp Q$ and $\neg P\Imp R$, concludes $if(P,Q,R)$. We propose the conclusion as the main goal -using~\ttindex{goalw}, which uses \texttt{if_def} to rewrite occurrences +using~\ttindex{Goalw}, which uses \texttt{if_def} to rewrite occurrences of $if$ in the subgoal. \begin{ttbox} val prems = Goalw [if_def] @@ -710,7 +710,7 @@ {\out 1. S} \end{ttbox} The major premise contains an occurrence of~$if$, but the version returned -by \ttindex{goalw} (and bound to the {\ML} variable~\texttt{major}) has the +by \ttindex{Goalw} (and bound to the {\ML} variable~\texttt{major}) has the definition expanded. Now \ttindex{cut_facts_tac} inserts~\texttt{major} as an assumption in the subgoal, so that \ttindex{blast_tac} can break it down. \begin{ttbox} @@ -729,9 +729,9 @@ \iflabelundefined{definitions}{{\em Introduction to Isabelle}}% {\S\ref{definitions}}, there are other ways of treating definitions when deriving a rule. We can start the -proof using \texttt{goal}, which does not expand definitions, instead of -\texttt{goalw}. We can use \ttindex{rew_tac} -to expand definitions in the subgoals --- perhaps after calling +proof using \texttt{Goal}, which does not expand definitions, instead of +\texttt{Goalw}. We can use \ttindex{rew_tac} +to expand definitions in the subgoals---perhaps after calling \ttindex{cut_facts_tac} to insert the rule's premises. We can use \ttindex{rewrite_rule}, which is a meta-inference rule, to expand definitions in the premises directly.

--- a/doc-src/Logics/logics.bbl Tue Jul 28 16:30:56 1998 +0200 +++ b/doc-src/Logics/logics.bbl Tue Jul 28 16:33:43 1998 +0200 @@ -192,6 +192,13 @@ \newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12 International Conference}, LNAI 814, pages 148--161. Springer, 1994. +\bibitem{paulson-final} +Lawrence~C. Paulson. +\newblock A concrete final coalgebra theorem for {ZF} set theory. +\newblock In Peter Dybjer, Bengt Nordstr{\"om}, and Jan Smith, editors, {\em + Types for Proofs and Programs: International Workshop {TYPES '94}}, LNCS 996, + pages 120--139. Springer, 1995. + \bibitem{paulson-set-II} Lawrence~C. Paulson. \newblock Set theory for verification: {II}. {Induction} and recursion. @@ -222,13 +229,6 @@ International Conference on Computer Logic}, LNCS 417, pages 246--274, Tallinn, Published 1990. Estonian Academy of Sciences, Springer. -\bibitem{paulson-final} -Lawrence~C. Paulson. -\newblock A concrete final coalgebra theorem for {ZF} set theory. -\newblock In Peter Dybjer, Bengt Nordstr{\"om}, and Jan Smith, editors, {\em - Types for Proofs and Programs: International Workshop {TYPES '94}}, LNCS 996, - pages 120--139. Springer, published 1995. - \bibitem{pelletier86} F.~J. Pelletier. \newblock Seventy-five problems for testing automatic theorem provers.

--- a/doc-src/Logics/logics.ind Tue Jul 28 16:30:56 1998 +0200 +++ b/doc-src/Logics/logics.ind Tue Jul 28 16:33:43 1998 +0200 @@ -352,7 +352,7 @@ \item {\tt gfp_subset} theorem, 45 \item {\tt gfp_Tarski} theorem, 45 \item {\tt gfp_upperbound} theorem, 45 - \item {\tt goalw}, 18, 19 + \item {\tt Goalw}, 18, 19 \indexspace

--- a/doc-src/Ref/defining.tex Tue Jul 28 16:30:56 1998 +0200 +++ b/doc-src/Ref/defining.tex Tue Jul 28 16:33:43 1998 +0200 @@ -799,7 +799,7 @@ After loading this definition from the file {\tt Hilbert.thy}, you can start to prove theorems in the logic: \begin{ttbox} -goal Hilbert.thy "P --> P"; +Goal "P --> P"; {\out Level 0} {\out P --> P} {\out 1. P --> P} @@ -880,7 +880,7 @@ \end{ttbox} Now we can prove mixed theorems like \begin{ttbox} -goal MinIFC.thy "P & False --> Q"; +Goal "P & False --> Q"; by (resolve_tac [MinI.impI] 1); by (dresolve_tac [MinC.conjE2] 1); by (eresolve_tac [MinIF.FalseE] 1);

--- a/doc-src/Ref/goals.tex Tue Jul 28 16:30:56 1998 +0200 +++ b/doc-src/Ref/goals.tex Tue Jul 28 16:33:43 1998 +0200 @@ -24,9 +24,9 @@ \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 qed}. +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} @@ -35,7 +35,7 @@ goalw_cterm : thm list -> cterm -> thm list premises : unit -> thm list \end{ttbox} -The {\tt goal} commands start a new proof by setting the goal. They +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! @@ -48,22 +48,15 @@ \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, {\tt qed} +function \texttt{premises}. When the proof is finished, \texttt{qed} 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 initial subgoal and the premises, which would -otherwise require use of {\tt rewrite_goals_tac} and -{\tt rewrite_rule}. - -\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}). +otherwise require use of \texttt{rewrite_goals_tac} and +\texttt{rewrite_rule}. \begin{ttdescription} \item[\ttindexbold{goal} {\it theory} {\it formula};] @@ -71,14 +64,14 @@ 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 +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 theory} {\it defs} {\it ct};] is - a version of {\tt goalw} for programming applications. The main + a version of \texttt{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 cterm_of (sign_of thy) $t$}. + is created from a term~$t$ by \texttt{cterm_of (sign_of thy) $t$}. \index{*cterm_of}\index{*sign_of} \item[\ttindexbold{premises}()] @@ -96,13 +89,13 @@ 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}). +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 {\tt prove_goal}, and abbreviates \hbox{\tt by (EVERY {\it +calls to \texttt{prove_goal}, and abbreviates \texttt{by (EVERY {\it tactics})}. \end{ttdescription} @@ -130,19 +123,19 @@ \end{ttbox} \begin{ttdescription} \item[\ttindexbold{qed} $name$;] is the usual way of ending a proof. - It combines {\tt result} and {\tt bind_thm}: it gets the theorem - using {\tt result()} and stores it the theorem database associated + 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{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 - {\tt goal} command. + \texttt{goal} command. It raises an exception unless the proof state passes certain checks. There - must be no assumptions other than those supplied to {\tt goal}. 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 {\tt goal} command. This allows + 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. @@ -150,17 +143,17 @@ 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. +\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 {\tt standard $thm$} (see \S\ref{MiscellaneousForwardRules}) + 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 {\tt get_thm} (see \S\ref{BasicOperationsOnTheories}). + 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 @@ -186,17 +179,17 @@ \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 {\tt resolve_tac}. + $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 - {\tt eresolve_tac} and {\tt dresolve_tac}. + \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 {\tt eresolve_tac} and - {\tt dresolve_tac}. + 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 all of a given set of constants. Note that a few basic @@ -214,13 +207,13 @@ \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 +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 {\tt chop}. +\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 @@ -230,21 +223,21 @@ \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 +\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 +\noindent{\it Error indications for \texttt{back}:}\par\nobreak \begin{itemize} \item{\footnotesize\tt"Warning:\ same as previous choice at this level"} - means {\tt back} found a non-empty branch point, but that it contained + 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 {\tt back} could +\item {\footnotesize\tt "back:\ no alternatives"} means \texttt{back} could find no alternative proof state. \end{itemize} @@ -269,7 +262,7 @@ \item[\ttindexbold{prlim} {\it k};] prints the current proof state, limiting the number of subgoals to~$k$. It -updates {\tt goals_limit} (see below) and is helpful when there are many +updates \texttt{goals_limit} (see below) and is helpful when there are many subgoals. \item[\ttindexbold{goals_limit} := {\it k};] @@ -291,7 +284,7 @@ \section{Shortcuts for applying tactics} -\index{shortcuts!for {\tt by} commands} +\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. @@ -309,32 +302,32 @@ \begin{ttdescription} \item[\ttindexbold{ba} {\it i};] -performs \hbox{\tt by (assume_tac {\it i});} +performs \texttt{by (assume_tac {\it i});} \item[\ttindexbold{br} {\it thm} {\it i};] -performs \hbox{\tt by (resolve_tac [{\it thm}] {\it i});} +performs \texttt{by (resolve_tac [{\it thm}] {\it i});} \item[\ttindexbold{be} {\it thm} {\it i};] -performs \hbox{\tt by (eresolve_tac [{\it thm}] {\it i});} +performs \texttt{by (eresolve_tac [{\it thm}] {\it i});} \item[\ttindexbold{bd} {\it thm} {\it i};] -performs \hbox{\tt by (dresolve_tac [{\it thm}] {\it i});} +performs \texttt{by (dresolve_tac [{\it thm}] {\it i});} \item[\ttindexbold{brs} {\it thms} {\it i};] -performs \hbox{\tt by (resolve_tac {\it thms} {\it i});} +performs \texttt{by (resolve_tac {\it thms} {\it i});} \item[\ttindexbold{bes} {\it thms} {\it i};] -performs \hbox{\tt by (eresolve_tac {\it thms} {\it i});} +performs \texttt{by (eresolve_tac {\it thms} {\it i});} \item[\ttindexbold{bds} {\it thms} {\it i};] -performs \hbox{\tt by (dresolve_tac {\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 {\tt br}, etc. They display the selected +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} @@ -352,22 +345,22 @@ solves some subgoal by assumption. \item[\ttindexbold{fr} {\it thm};] -refines some subgoal using \hbox{\tt resolve_tac [{\it thm}]} +refines some subgoal using \texttt{resolve_tac [{\it thm}]} \item[\ttindexbold{fe} {\it thm};] -refines some subgoal using \hbox{\tt eresolve_tac [{\it thm}]} +refines some subgoal using \texttt{eresolve_tac [{\it thm}]} \item[\ttindexbold{fd} {\it thm};] -refines some subgoal using \hbox{\tt dresolve_tac [{\it thm}]} +refines some subgoal using \texttt{dresolve_tac [{\it thm}]} \item[\ttindexbold{frs} {\it thms};] -refines some subgoal using \hbox{\tt resolve_tac {\it thms}} +refines some subgoal using \texttt{resolve_tac {\it thms}} \item[\ttindexbold{fes} {\it thms};] -refines some subgoal using \hbox{\tt eresolve_tac {\it thms}} +refines some subgoal using \texttt{eresolve_tac {\it thms}} \item[\ttindexbold{fds} {\it thms};] -refines some subgoal using \hbox{\tt dresolve_tac {\it thms}} +refines some subgoal using \texttt{dresolve_tac {\it thms}} \end{ttdescription} \subsection{Other shortcuts} @@ -377,17 +370,17 @@ ren : string -> int -> unit \end{ttbox} \begin{ttdescription} -\item[\ttindexbold{bw} {\it def};] performs \hbox{\tt by +\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 {\tt bw} but takes a list of definitions. +is like \texttt{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 +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} @@ -408,8 +401,8 @@ 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 {\tt goal}, {\tt goalw} and {\tt goalw_cterm}. +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 @@ -426,7 +419,7 @@ (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 +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. % @@ -436,21 +429,21 @@ the given tactic function. \item[\ttindexbold{qed_goal} $name$ $theory$ $formula$ $tacsf$;] acts - like {\tt prove_goal} but also stores the resulting theorem in the + like \texttt{prove_goal} but 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 {\tt prove_goal} but also applies the list of {\it defs\/} as +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 {\tt qed_goal}. +is analogous to \texttt{qed_goal}. \item[\ttindexbold{prove_goalw_cterm} {\it theory} {\it defs} {\it ct} {\it tacsf};] -is a version of {\tt prove_goalw} for programming applications. The main +is a version of \texttt{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} @@ -482,16 +475,16 @@ 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 +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}. +stack is \texttt{push_proof}. -To save some point of the proof, call {\tt push_proof}. You may now -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 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 {\tt rotate_proof} repeatedly; as it rotates +To view the entire stack, call \texttt{rotate_proof} repeatedly; as it rotates the stack, it prints the new top element. \begin{ttdescription} @@ -574,7 +567,7 @@ \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 +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}] @@ -591,7 +584,7 @@ \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 +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}

--- a/doc-src/Ref/ref.ind Tue Jul 28 16:30:56 1998 +0200 +++ b/doc-src/Ref/ref.ind Tue Jul 28 16:33:43 1998 +0200 @@ -1,7 +1,6 @@ \begin{theindex} \item {\tt !!} symbol, 69 - \subitem in main goal, 8 \item {\tt\$}, \bold{60}, 86 \item {\tt\%} symbol, 69 \item {\tt ::} symbol, 69, 70 @@ -65,7 +64,7 @@ \item {\tt APPEND}, \bold{29}, 31 \item {\tt APPEND'}, 36 \item {\tt Appl}, 83 - \item {\tt aprop} nonterminal, \bold{68} + \item {\tt aprop} nonterminal, \bold{70} \item {\tt ares_tac}, \bold{20} \item {\tt args} nonterminal, 93 \item {\tt Arith} theory, 118 @@ -186,7 +185,7 @@ \item {\tt cterm_of}, 8, 14, \bold{62} \item {\tt ctyp}, \bold{63} \item {\tt ctyp_of}, \bold{64} - \item {\tt cut_facts_tac}, 8, \bold{20}, 101 + \item {\tt cut_facts_tac}, \bold{20}, 101 \item {\tt cut_inst_tac}, \bold{20} \item {\tt cut_rl} theorem, 22 @@ -242,7 +241,7 @@ \item {\tt ematch_tac}, \bold{18} \item {\tt empty} constant, 92 \item {\tt empty_cs}, \bold{132} - \item {\tt empty_ss}, \bold{107} + \item {\tt empty_ss}, \bold{106} \item {\tt eq_assume_tac}, \bold{18}, 131 \item {\tt eq_assumption}, \bold{47} \item {\tt eq_mp_tac}, \bold{139} @@ -333,7 +332,8 @@ \item {\tt get_thms}, \bold{57} \item {\tt getgoal}, \bold{16} \item {\tt gethyps}, \bold{16}, 34 - \item {\tt goal}, \bold{8}, 14 + \item {\tt Goal}, 14 + \item {\tt goal}, \bold{8} \item {\tt goals_limit}, \bold{11} \item {\tt goalw}, \bold{8} \item {\tt goalw_cterm}, \bold{8} @@ -619,8 +619,8 @@ \item {\tt setsubgoaler}, \bold{110}, 125 \item {\tt settermless}, \bold{117} \item shortcuts + \subitem for \texttt{by} commands, 11 \subitem for tactics, 20 - \subitem for {\tt by} commands, 11 \item {\tt show_brackets}, \bold{4} \item {\tt show_consts}, \bold{4} \item {\tt show_hyps}, \bold{4} @@ -759,7 +759,7 @@ \subitem joining by resolution, 38 \subitem of pure theory, 22 \subitem printing of, 37 - \subitem retrieving, 10 + \subitem retrieving, 9 \subitem size of, 33 \subitem standardizing, 40 \subitem storing, 9

--- a/doc-src/Ref/simplifier.tex Tue Jul 28 16:30:56 1998 +0200 +++ b/doc-src/Ref/simplifier.tex Tue Jul 28 16:33:43 1998 +0200 @@ -72,7 +72,7 @@ of \texttt{Simp_tac} as follows: \begin{ttbox} context Arith.thy; -goal Arith.thy "0 + (x + 0) = x + 0 + 0"; +Goal "0 + (x + 0) = x + 0 + 0"; {\out 1. 0 + (x + 0) = x + 0 + 0} by (Simp_tac 1); {\out Level 1} @@ -180,22 +180,22 @@ \medskip -Good simpsets are hard to design. As a rule of thump, generally -useful ``simplification rules'' like $\Var{n}+0 = \Var{n}$ should be -added to the current simpset right after they have been proved. Those -of a more specific nature (e.g.\ the laws of de~Morgan, which alter -the structure of a formula) should only be added for specific proofs -and deleted again afterwards. Conversely, it may also happen that a -generally useful rule needs to be removed for a certain proof and is -added again afterwards. The need of frequent temporary additions or -deletions may indicate a badly designed simpset. +Good simpsets are hard to design. Rules that obviously simplify, +like $\Var{n}+0 = \Var{n}$, should be added to the current simpset right after +they have been proved. More specific ones (such as distributive laws, which +duplicate subterms) should be added only for specific proofs and deleted +afterwards. Conversely, sometimes a rule needs +to be removed for a certain proof and restored afterwards. The need of +frequent additions or deletions may indicate a badly designed +simpset. \begin{warn} The union of the parent simpsets (as described above) is not always a good starting point for the new theory. If some ancestors have deleted simplification rules because they are no longer wanted, while others have left those rules in, then the union will contain - the unwanted rules. + the unwanted rules. After this union is formed, changes to + a parent simpset have no effect on the child simpset. \end{warn} @@ -728,7 +728,7 @@ \section{Examples of using the simplifier} \index{examples!of simplification} Assume we are working within {\tt - FOL} (cf.\ \texttt{FOL/ex/Nat}) and that + FOL} (see the file \texttt{FOL/ex/Nat}) and that \begin{ttdescription} \item[Nat.thy] is a theory including the constants $0$, $Suc$ and $+$, @@ -750,7 +750,7 @@ Proofs by induction typically involve simplification. Here is a proof that~0 is a right identity: \begin{ttbox} -goal Nat.thy "m+0 = m"; +Goal "m+0 = m"; {\out Level 0} {\out m + 0 = m} {\out 1. m + 0 = m} @@ -786,7 +786,7 @@ Let us prove a similar result involving more complex terms. We prove that addition is commutative. \begin{ttbox} -goal Nat.thy "m+Suc(n) = Suc(m+n)"; +Goal "m+Suc(n) = Suc(m+n)"; {\out Level 0} {\out m + Suc(n) = Suc(m + n)} {\out 1. m + Suc(n) = Suc(m + n)} @@ -850,8 +850,7 @@ Here is a conjecture to be proved for an arbitrary function~$f$ satisfying the law $f(Suc(\Var{n})) = Suc(f(\Var{n}))$: \begin{ttbox} -val [prem] = goal Nat.thy - "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)"; +val [prem] = Goal "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)"; {\out Level 0} {\out f(i + j) = i + f(j)} {\out 1. f(i + j) = i + f(j)} @@ -1014,7 +1013,7 @@ Our desired theorem now reads $\texttt{sum} \, (\lambda i.i) \, (n+1) = n\times(n+1)/2$. The Isabelle goal has both sides multiplied by~$2$: \begin{ttbox} -goal NatSum.thy "2 * sum (\%i.i) (Suc n) = n * Suc n"; +Goal "2 * sum (\%i.i) (Suc n) = n * Suc n"; {\out Level 0} {\out 2 * sum (\%i. i) (Suc n) = n * Suc n} {\out 1. 2 * sum (\%i. i) (Suc n) = n * Suc n}