# HG changeset patch # User lcp # Date 767030937 -7200 # Node ID 13660d5f6a7737420434a03c36496f6e9b9afe51 # Parent 2fda15dd1e0f0259f29dcf676318ad2f156e752f final Springer copy diff -r 2fda15dd1e0f -r 13660d5f6a77 doc-src/Intro/advanced.tex --- a/doc-src/Intro/advanced.tex Fri Apr 22 12:43:53 1994 +0200 +++ b/doc-src/Intro/advanced.tex Fri Apr 22 18:08:57 1994 +0200 @@ -9,9 +9,8 @@ the literature. Set theory~({\tt ZF}) and Constructive Type Theory~({\tt 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 sophisticated logic, because its types and functions are -identified with those of the meta-logic; this may cause difficulties for -beginners. +Isabelle's most sophisticated logic because its types and functions are +identified with those of the meta-logic. Choose a logic that you already understand. Isabelle is a proof tool, not a teaching tool; if you do not know how to do a particular proof @@ -113,10 +112,10 @@ \Var{P}\bimp \Var{Q} & \equiv & (\Var{P}\imp \Var{Q}) \conj (\Var{Q}\imp \Var{P}) \end{eqnarray*} -\index{meta-rewriting} +\index{meta-rewriting}% Isabelle permits {\bf meta-level rewriting} using definitions such as these. {\bf Unfolding} replaces every instance -of $\neg \Var{P}$ by the corresponding instance of $\Var{P}\imp\bot$. For +of $\neg \Var{P}$ by the corresponding instance of ${\Var{P}\imp\bot}$. For example, $\forall x.\neg (P(x)\conj \neg R(x,0))$ unfolds to \[ \forall x.(P(x)\conj R(x,0)\imp\bot)\imp\bot. \] {\bf Folding} a definition replaces occurrences of the right-hand side by @@ -124,7 +123,7 @@ When you define new concepts, you should derive rules asserting their abstract properties, and then forget their definitions. This supports -modularity: if you later change the definitions, without affecting their +modularity: if you later change the definitions without affecting their abstract properties, then most of your proofs will carry through without change. Indiscriminate unfolding makes a subgoal grow exponentially, becoming unreadable. @@ -336,7 +335,7 @@ \(T\) = \(S@1\) + \(\cdots\) + \(S@n\) + classes {\it class declarations} default {\it sort} -types {\it type declarations} +types {\it type declarations and synonyms} arities {\it arity declarations} consts {\it constant declarations} rules {\it rule declarations} @@ -361,30 +360,30 @@ or more other theories, inheriting their types, constants, syntax, etc. The theory \thydx{Pure} contains nothing but Isabelle's meta-logic. -Each theory definition must reside in a separate file, whose name is -determined as follows: the theory name, say {\tt ListFn}, is converted to -lower case and {\tt.thy} is appended, yielding the filename {\tt - listfn.thy}. Isabelle uses this convention to locate the file containing -a given theory; \ttindexbold{use_thy} automatically loads a theory's -parents before loading the theory itself. +Each theory definition must reside in a separate file, whose name is the +theory's with {\tt.thy} appended. For example, theory {\tt ListFn} resides +on a file named {\tt ListFn.thy}. Isabelle uses this convention to locate the +file containing a given theory; \ttindexbold{use_thy} automatically loads a +theory's parents before loading the theory itself. -Calling \ttindexbold{use_thy}~{\tt"}{\it T\/}{\tt"} reads a theory from the -file {\it t}{\tt.thy}, writes the corresponding {\ML} code to the file -{\tt.}{\it t}{\tt.thy.ML}, reads the latter file, and deletes it if no errors -occured. This declares the {\ML} structure~$T$, which contains a component +Calling \ttindexbold{use_thy}~{\tt"{\it T\/}"} reads a theory from the +file {\it T}{\tt.thy}, writes the corresponding {\ML} code to the file +{\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 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 {\it t}{\tt.ML}, if +all goes well, {\tt use_thy} will finally read the file {\it T}{\tt.ML}, if it exists. This file typically begins with the {\ML} declaration {\tt open}~$T$ and contains proofs that refer to the components of~$T$. When a theory file is modified, many theories may have to be reloaded. Isabelle records the modification times and dependencies of theory files. -See the {\em Reference Manual\/} -\iflabelundefined{sec:reloading-theories}{}{(\S\ref{sec:reloading-theories})} +See +\iflabelundefined{sec:reloading-theories}{the {\em Reference Manual\/}}% + {\S\ref{sec:reloading-theories}} for more details. @@ -491,7 +490,7 @@ A type constructor may be overloaded (subject to certain conditions) by appearing in several arity declarations. For instance, the function type -constructor~$\To$ has the arity $(logic,logic)logic$; in higher-order +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 @@ -521,7 +520,7 @@ translator passes them verbatim to the {\ML} output file. \end{warn} -\subsection{Type synonyms}\indexbold{types!synonyms} +\subsection{Type synonyms}\indexbold{type synonyms} Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar to those found in \ML. Such synonyms are defined in the type declaration part and are fairly self explanatory: @@ -791,7 +790,7 @@ \end{ttbox} \subsection{Proving some recursion equations} -File {\tt FOL/ex/nat.ML} contains proofs involving this theory of the +File {\tt FOL/ex/Nat.ML} 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} @@ -969,7 +968,7 @@ number is exponential in the size of the formula. \subsection{Proving that addition is associative} -Let us invoke the induction rule properly properly, using~{\tt +Let us invoke the induction rule properly, using~{\tt res_inst_tac}. At the same time, we shall have a glimpse at Isabelle's simplification tactics, which are described in \iflabelundefined{simp-chap}% @@ -981,7 +980,7 @@ perhaps proving it. For efficiency, the rewrite rules must be packaged into a {\bf simplification set},\index{simplification sets} or {\bf simpset}. We take the standard simpset for first-order logic and -insert the equations for~{\tt add} proved in the previous section, namely +insert the equations proved in the previous section, namely $0+n=n$ and ${\tt Suc}(m)+n={\tt Suc}(m+n)$: \begin{ttbox} val add_ss = FOL_ss addrews [add_0, add_Suc]; @@ -1003,7 +1002,7 @@ \end{ttbox} The base case holds easily; both sides reduce to $m+n$. The tactic~\ttindex{simp_tac} rewrites with respect to the given simplification -set, applying the rewrite rules for~{\tt +}: +set, applying the rewrite rules for addition: \begin{ttbox} by (simp_tac add_ss 1); {\out Level 2} @@ -1011,7 +1010,7 @@ {\out 1. !!x. x + m + n = x + (m + n) ==>} {\out Suc(x) + m + n = Suc(x) + (m + n)} \end{ttbox} -The inductive step requires rewriting by the equations for~{\tt add} +The inductive step requires rewriting by the equations for addition together the induction hypothesis, which is also an equation. The tactic~\ttindex{asm_simp_tac} rewrites using a simplification set and any useful assumptions: @@ -1028,7 +1027,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 {\tt 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: @@ -1199,7 +1198,7 @@ {\out 1. app(Nil, ?x1 : Nil, a : b : c : Nil)} \end{ttbox} The tactic has failed to find a solution! It reached a dead end at -subgoal~1: there is no~$\Var{x1}$ such that [] appended with~$[\Var{x1}]$ +subgoal~1: there is no~$\Var{x@1}$ such that [] appended with~$[\Var{x@1}]$ equals~$[a,b,c]$. Backtracking explores other outcomes. \begin{ttbox} back(); diff -r 2fda15dd1e0f -r 13660d5f6a77 doc-src/Intro/foundations.tex --- a/doc-src/Intro/foundations.tex Fri Apr 22 12:43:53 1994 +0200 +++ b/doc-src/Intro/foundations.tex Fri Apr 22 18:08:57 1994 +0200 @@ -50,21 +50,24 @@ \end{figure} \section{Formalizing logical syntax in Isabelle}\label{sec:logical-syntax} +\index{first-order logic} + Figure~\ref{fol-fig} presents intuitionistic first-order logic, including equality. Let us see how to formalize this logic in Isabelle, illustrating the main features of Isabelle's polymorphic meta-logic. +\index{lambda calc@$\lambda$-calculus} Isabelle represents syntax using the simply typed $\lambda$-calculus. We declare a type for each syntactic category of the logic. We declare a constant for each symbol of the logic, giving each $n$-place operation an $n$-argument curried function type. Most importantly, $\lambda$-abstraction represents variable binding in quantifiers. -\index{lambda calc@$\lambda$-calculus} \index{lambda - abs@$\lambda$-abstractions} -\index{types!syntax of}\index{types!function}\index{*fun type} -Isabelle has \ML-style type constructors such as~$(\alpha)list$, where +\index{types!syntax of}\index{types!function}\index{*fun type} +\index{type constructors} +Isabelle has \ML-style polymorphic types such as~$(\alpha)list$, where +$list$ is a type constructor and $\alpha$ is a type variable; for example, $(bool)list$ is the type of lists of booleans. Function types have the form $(\sigma,\tau)fun$ or $\sigma\To\tau$, where $\sigma$ and $\tau$ are types. Curried function types may be abbreviated: @@ -116,8 +119,9 @@ precedences, so that we write $P\conj Q\disj R$ instead of $\disj(\conj(P,Q), R)$. -\S\ref{sec:defining-theories} below describes the syntax of Isabelle theory -files and illustrates it by extending our logic with mathematical induction. +Section~\ref{sec:defining-theories} below describes the syntax of Isabelle +theory files and illustrates it by extending our logic with mathematical +induction. \subsection{Polymorphic types and constants} \label{polymorphic} @@ -164,7 +168,7 @@ We give~$o$ and function types the class $logic$ rather than~$term$, since they are not legal types for terms. We may introduce new types of class $term$ --- for instance, type $string$ or $real$ --- at any time. We can -even declare type constructors such as $(\alpha)list$, and state that type +even declare type constructors such as~$list$, and state that type $(\tau)list$ belongs to class~$term$ provided $\tau$ does; equality applies to lists of natural numbers but not to lists of formulae. We may summarize this paragraph by a set of {\bf arity declarations} for type @@ -176,7 +180,7 @@ list & :: & (term)term \end{eqnarray*} (Recall that $fun$ is the type constructor for function types.) -In higher-order logic, equality does apply to truth values and +In \rmindex{higher-order logic}, equality does apply to truth values and functions; this requires the arity declarations ${o::term}$ and ${fun::(term,term)term}$. The class system can also handle overloading.\index{overloading|bold} We could declare $arith$ to be the @@ -186,7 +190,7 @@ {+},{-},{\times},{/} & :: & [\alpha{::}arith,\alpha]\To \alpha \end{eqnarray*} If we declare new types $real$ and $complex$ of class $arith$, then we -effectively have three sets of operators: +in effect have three sets of operators: \begin{eqnarray*} {+},{-},{\times},{/} & :: & [nat,nat]\To nat \\ {+},{-},{\times},{/} & :: & [real,real]\To real \\ @@ -216,7 +220,10 @@ Even with overloading, each term has a unique, most general type. For this to be possible, the class and type declarations must satisfy certain -technical constraints~\cite{nipkow-prehofer}. +technical constraints; see +\iflabelundefined{sec:ref-defining-theories}% + {Sect.\ Defining Theories in the {\em Reference Manual}}% + {\S\ref{sec:ref-defining-theories}}. \subsection{Higher types and quantifiers} @@ -338,10 +345,10 @@ \noindent Next, consider the disjunction rules. The discharge of assumption in $(\disj E)$ is expressed using $\Imp$: +\index{assumptions!discharge of}% $$ P \Imp P\disj Q \qquad Q \Imp P\disj Q \eqno(\disj I1,2) $$ $$ \List{P\disj Q; P\Imp R; Q\Imp R} \Imp R \eqno(\disj E) $$ - -\noindent\index{assumptions!discharge of} +% To understand this treatment of assumptions in natural deduction, look at implication. The rule $({\imp}I)$ is the classic example of natural deduction: to prove that $P\imp Q$ is true, assume $P$ @@ -421,9 +428,8 @@ A {\bf signature} contains the information necessary for type checking, parsing and pretty printing a term. It specifies classes and their -relationships; types, with their arities, and constants, with -their types. It also contains syntax rules, specified using mixfix -declarations. +relationships, types and their arities, constants and their types, etc. It +also contains syntax rules, specified using mixfix declarations. Two signatures can be merged provided their specifications are compatible --- they must not, for example, assign different types to the same constant. @@ -457,13 +463,13 @@ {} & {} &\hbox{Pure}& {} & {} \end{array} \] -\end{tt} +\end{tt}% Each Isabelle proof typically works within a single theory, which is associated with the proof state. However, many different theories may coexist at the same time, and you may work in each of these during a single session. -\begin{warn}\index{constants!clashes with variables} +\begin{warn}\index{constants!clashes with variables}% Confusing problems arise if you work in the wrong theory. Each theory defines its own syntax. An identifier may be regarded in one theory as a constant and in another as a variable. @@ -481,7 +487,7 @@ properties must be demonstrated separately for each object-logic. The meta-logic is defined by a collection of inference rules, including -equational rules for the $\lambda$-calculus, and logical rules. The rules +equational rules for the $\lambda$-calculus and logical rules. The rules for~$\Imp$ and~$\Forall$ resemble those for~$\imp$ and~$\forall$ in Fig.\ts\ref{fol-fig}. Proofs performed using the primitive meta-rules would be lengthy; Isabelle proofs normally use certain derived rules. @@ -562,7 +568,7 @@ equation \[ t(\Var{h@1}(t),\ldots,\Var{h@m}(t)) \qeq g(u@1,\ldots,u@k). $$ -\begin{warn}\index{unification!incompleteness of} +\begin{warn}\index{unification!incompleteness of}% Huet's unification procedure is complete. Isabelle's polymorphic version, which solves for type unknowns as well as for term unknowns, is incomplete. The problem is that projection requires type information. In @@ -637,7 +643,7 @@ \] When resolving two rules, the unknowns in the first rule are renamed, by subscripting, to make them distinct from the unknowns in the second rule. To -resolve $({\imp}E)$ with itself, the first copy of the rule would become +resolve $({\imp}E)$ with itself, the first copy of the rule becomes \[ \List{\Var{P@1}\imp \Var{Q@1}; \Var{P@1}} \Imp \Var{Q@1}. \] Resolving this with $({\imp}E)$ in the first premise, unifying $\Var{Q@1}$ with $\Var{P}\imp \Var{Q}$, is the meta-level inference @@ -647,9 +653,8 @@ \List{\Var{P}\imp \Var{Q}; \Var{P}} \Imp \Var{Q}} \] Renaming the unknowns in the resolvent, we have derived the -object-level rule +object-level rule\index{rules!derived} \[ \infer{Q.}{R\imp (P\imp Q) & R & P} \] -\index{rules!derived} Joining rules in this fashion is a simple way of proving theorems. The derived rules are conservative extensions of the object-logic, and may permit simpler proofs. Let us consider another example. Suppose we have the axiom @@ -797,9 +802,10 @@ To refine subgoal~$i$ of a proof state by a rule, perform the following resolution: \[ \infer{\hbox{new proof state}}{\hbox{rule} & & \hbox{proof state}} \] -If the rule is $\List{\psi'@1; \ldots; \psi'@m} \Imp \psi'$ after lifting -over subgoal~$i$, and the proof state is $\List{\phi@1; \ldots; \phi@n} -\Imp \phi$, then the new proof state is (for~$1\leq i\leq n$) +Suppose the rule is $\List{\psi'@1; \ldots; \psi'@m} \Imp \psi'$ after +lifting over subgoal~$i$'s assumptions and parameters. If the proof state +is $\List{\phi@1; \ldots; \phi@n} \Imp \phi$, then the new proof state is +(for~$1\leq i\leq n$) \[ (\List{\phi@1; \ldots; \phi@{i-1}; \psi'@1; \ldots; \psi'@m; \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s. \] Substitution~$s$ unifies $\psi'$ with~$\phi@i$. In the proof state, @@ -974,9 +980,8 @@ tries~$tac1$ and returns the result if non-empty; otherwise, it uses~$tac2$. \item[REPEAT $tac$] is a repetition tactic. Applied to a state, it -returns all states reachable by applying~$tac$ as long as possible (until -it would fail). $REPEAT$ can be expressed in a few lines of \ML{} using -{\tt THEN} and~{\tt ORELSE}. +returns all states reachable by applying~$tac$ as long as possible --- until +it would fail. \end{ttdescription} For instance, this tactic repeatedly applies $tac1$ and~$tac2$, giving $tac1$ priority: @@ -999,7 +1004,7 @@ \index{elim-resolution|bold}\index{assumptions!deleting} Consider proving the theorem $((R\disj R)\disj R)\disj R\imp R$. By -$({\imp}I)$, we prove $R$ from the assumption $((R\disj R)\disj R)\disj R$. +$({\imp}I)$, we prove~$R$ from the assumption $((R\disj R)\disj R)\disj R$. Applying $(\disj E)$ to this assumption yields two subgoals, one that assumes~$R$ (and is therefore trivial) and one that assumes $(R\disj R)\disj R$. This subgoal admits another application of $(\disj E)$. Since @@ -1008,9 +1013,8 @@ \[ \List{((R\disj R)\disj R)\disj R; (R\disj R)\disj R; R\disj R; R} \Imp R. \] In general, using $(\disj E)$ on the assumption $P\disj Q$ creates two new subgoals with the additional assumption $P$ or~$Q$. In these subgoals, -$P\disj Q$ is redundant. It wastes space; worse, it could make a theorem -prover repeatedly apply~$(\disj E)$, looping. Other elimination rules pose -similar problems. In first-order logic, only universally quantified +$P\disj Q$ is redundant. Other elimination rules behave +similarly. In first-order logic, only universally quantified assumptions are sometimes needed more than once --- say, to prove $P(f(f(a)))$ from the assumptions $\forall x.P(x)\imp P(f(x))$ and~$P(a)$. @@ -1053,7 +1057,7 @@ \[ \List{\Var{P}\disj \Var{Q};\; \Var{P}\Imp \Var{R};\; \Var{Q}\Imp \Var{R}} \Imp \Var{R} \] and the proof state is $(P\disj P\Imp P)\Imp (P\disj P\imp P)$. The -lifted rule would be +lifted rule is \[ \begin{array}{l@{}l} \lbrakk\;& P\disj P \Imp \Var{P@1}\disj\Var{Q@1}; \\ & \List{P\disj P ;\; \Var{P@1}} \Imp \Var{R@1}; \\ @@ -1061,10 +1065,10 @@ \rbrakk\;& \Imp \Var{R@1} \end{array} \] -Unification would take the simultaneous equations +Unification takes the simultaneous equations $P\disj P \qeq \Var{P@1}\disj\Var{Q@1}$ and $\Var{R@1} \qeq P$, yielding $\Var{P@1}\equiv\Var{Q@1}\equiv\Var{R@1} \equiv P$. The new proof state -would be simply +is simply \[ \List{P \Imp P;\; P \Imp P} \Imp (P\disj P\imp P). \] Elim-resolution's simultaneous unification gives better control @@ -1110,14 +1114,13 @@ \[ \infer[\quad\hbox{to the elimination rule}\quad]{Q}{P@1 & \ldots & P@m} \infer{R.}{P@1 & \ldots & P@m & \infer*{R}{[Q]}} \] -\index{destruct-resolution} -{\bf Destruct-resolution} combines this transformation with -elim-resolution. It applies a destruction rule to some assumption of a -subgoal. Given the rule above, it replaces the assumption~$P@1$ by~$Q$, -with new subgoals of showing instances of $P@2$, \ldots,~$P@m$. -Destruct-resolution works forward from a subgoal's assumptions. Ordinary -resolution performs forward reasoning from theorems, as illustrated -in~\S\ref{joining}. +{\bf Destruct-resolution}\index{destruct-resolution} combines this +transformation with elim-resolution. It applies a destruction rule to some +assumption of a subgoal. Given the rule above, it replaces the +assumption~$P@1$ by~$Q$, with new subgoals of showing instances of $P@2$, +\ldots,~$P@m$. Destruct-resolution works forward from a subgoal's +assumptions. Ordinary resolution performs forward reasoning from theorems, +as illustrated in~\S\ref{joining}. \subsection{Deriving rules by resolution} \label{deriving} @@ -1149,10 +1152,14 @@ state \[ \phantom{\List{P\conj Q;\; P\conj Q}} \llap{$\List{P;Q}$}\Imp R \quad [\,\List{P;Q}\Imp R\,]. \] -Resolving subgoals~1 and~2 with $({\conj}E1)$ and $({\conj}E2)$, +Resolving subgoals~1 and~2 with~$({\conj}E1)$ and~$({\conj}E2)$, respectively, yields the state -\[ \List{P\conj Q;\; P\conj Q}\Imp R \quad [\,\List{P;Q}\Imp R\,]. \] -Resolving both subgoals with the assumption $P\conj Q$ yields +\[ \List{P\conj \Var{Q@1};\; \Var{P@2}\conj Q}\Imp R + \quad [\,\List{P;Q}\Imp R\,]. +\] +The unknowns $\Var{Q@1}$ and~$\Var{P@2}$ arise from unconstrained +subformulae in the premises of~$({\conj}E1)$ and~$({\conj}E2)$. Resolving +both subgoals with the assumption $P\conj Q$ instantiates the unknowns to yield \[ R \quad [\, \List{P;Q}\Imp R, P\conj Q \,]. \] The proof may use the meta-assumptions in any order, and as often as necessary; when finished, we discharge them in the correct order to @@ -1163,7 +1170,7 @@ schematic variables. \begin{warn} -Schematic variables are not allowed in meta-assumptions because they would -complicate lifting. Meta-assumptions remain fixed throughout a proof. + Schematic variables are not allowed in meta-assumptions, for a variety of + reasons. Meta-assumptions remain fixed throughout a proof. \end{warn} diff -r 2fda15dd1e0f -r 13660d5f6a77 doc-src/Intro/getting.tex --- a/doc-src/Intro/getting.tex Fri Apr 22 12:43:53 1994 +0200 +++ b/doc-src/Intro/getting.tex Fri Apr 22 18:08:57 1994 +0200 @@ -38,12 +38,15 @@ symbols. Identifiers that are not reserved words may serve as free variables or -constants. A type identifier consists of an identifier prefixed by a -prime, for example {\tt'a} and \hbox{\tt'hello}. An unknown (or type -unknown) consists of a question mark, an identifier (or type identifier), -and a subscript. The subscript, a non-negative integer, allows the -renaming of unknowns prior to unification.% -% +constants. A {\bf type identifier} consists of an identifier prefixed by a +prime, for example {\tt'a} and \hbox{\tt'hello}. Type identifiers stand +for (free) type variables, which remain fixed during a proof. +\index{type identifiers} + +An {\bf unknown}\index{unknowns} (or type unknown) consists of a question +mark, an identifier (or type identifier), and a subscript. The subscript, +a non-negative integer, +allows the renaming of unknowns prior to unification.% \footnote{The subscript may appear after the identifier, separated by a dot; this prevents ambiguity when the identifier ends with a digit. Thus {\tt?z6.0} has identifier {\tt"z6"} and subscript~0, while {\tt?a0.5} @@ -62,7 +65,7 @@ contains the `logical' types. Sorts are lists of classes enclosed in braces~\} and \{; singleton sorts may be abbreviated by dropping the braces. -\index{types!syntax of|bold} +\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::\{ord,arith\}}. @@ -72,10 +75,10 @@ \index{*[ symbol}\index{*] symbol} \begin{array}{lll} \multicolumn{3}{c}{\hbox{ASCII Notation for Types}} \\ \hline - t "::" C & t :: C & \hbox{class constraint} \\ - t "::" "\{" C@1 "," \ldots "," C@n "\}" & - t :: \{C@1,\dots,C@n\} & \hbox{sort constraint} \\ - \sigma"=>"\tau & \sigma\To\tau & \hbox{function type} \\ + \alpha "::" C & \alpha :: C & \hbox{class constraint} \\ + \alpha "::" "\{" C@1 "," \ldots "," C@n "\}" & + \alpha :: \{C@1,\dots,C@n\} & \hbox{sort constraint} \\ + \sigma " => " \tau & \sigma\To\tau & \hbox{function type} \\ "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau & [\sigma@1,\ldots,\sigma@n] \To\tau & \hbox{curried function type} \\ "(" \tau@1"," \ldots "," \tau@n ")" tycon & @@ -83,7 +86,7 @@ \end{array} \] Terms are those of the typed $\lambda$-calculus. -\index{terms!syntax of|bold} +\index{terms!syntax of|bold}\index{type constraints} \[\dquotes \index{%@{\tt\%} symbol}\index{lambda abs@$\lambda$-abstractions} \index{*:: symbol} @@ -180,11 +183,11 @@ \subsection{Basic operations on theorems} \index{theorems!basic operations on|bold} \index{LCF system} -Meta-level theorems have type \mltydx{thm} and represent the theorems and -inference rules of object-logics. Isabelle's meta-logic is implemented -using the {\sc lcf} approach: each meta-level inference rule is represented by -a function from theorems to theorems. Object-level rules are taken as -axioms. +Meta-level theorems have the \ML{} type \mltydx{thm}. They represent the +theorems and inference rules of object-logics. Isabelle's meta-logic is +implemented using the {\sc lcf} approach: each meta-level inference rule is +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} @@ -214,9 +217,14 @@ growth. \end{ttdescription} The rules of a theory are normally bound to \ML\ identifiers. Suppose we -are running an Isabelle session containing natural deduction first-order -logic. Let us try an example given in~\S\ref{joining}. We first print -\tdx{mp}, which is the rule~$({\imp}E)$, then resolve it with itself. +are running an Isabelle session containing theory~\FOL, natural deduction +first-order logic.\footnote{For a listing of the \FOL{} rules and their + \ML{} names, turn to +\iflabelundefined{fol-rules}{{\em Isabelle's Object-Logics}}% + {page~\pageref{fol-rules}}.} +Let us try an example given in~\S\ref{joining}. We +first print \tdx{mp}, which is the rule~$({\imp}E)$, then resolve it with +itself. \begin{ttbox} prth mp; {\out [| ?P --> ?Q; ?P |] ==> ?Q} @@ -225,14 +233,14 @@ {\out [| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q} {\out val it = "[| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q" : thm} \end{ttbox} -User input appears in {\tt typewriter characters}, and output appears in -{\sltt slanted typewriter characters}. \ML's response {\out val }~\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.\footnote{This works - under both Poly/ML and Standard ML of New Jersey.} Printing commands -like {\tt prth} omit the quotes and the surrounding {\tt val \ldots :\ - thm}. Ignoring their side-effects, the commands are identity functions. +User input appears in {\footnotesize\tt typewriter characters}, and output +appears in {\sltt slanted typewriter characters}. \ML's response {\out val + }~\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 + \ldots :\ thm}. Ignoring their side-effects, the commands are identity +functions. To contrast {\tt RS} with {\tt RSN}, we resolve \tdx{conjunct1}, which stands for~$(\conj E1)$, with~\tdx{mp}. @@ -568,11 +576,15 @@ \section{Quantifier reasoning} -\index{quantifiers}\index{parameters}\index{unknowns} +\index{quantifiers}\index{parameters}\index{unknowns}\index{unknowns!function} This section illustrates how Isabelle enforces quantifier provisos. -Quantifier rules create terms such as~$\Var{f}(x,z)$, where~$\Var{f}$ is a -function unknown and $x$ and~$z$ are parameters. This may be replaced by -any term, possibly containing free occurrences of $x$ and~$z$. +Suppose that $x$, $y$ and~$z$ are parameters of a subgoal. Quantifier +rules create terms such as~$\Var{f}(x,z)$, where~$\Var{f}$ is a function +unknown. Instantiating $\Var{f}$ to $\lambda x\,z.t$ has the effect of +replacing~$\Var{f}(x,z)$ by~$t$, where the term~$t$ may contain free +occurrences of~$x$ and~$z$. On the other hand, no instantiation +of~$\Var{f}$ can replace~$\Var{f}(x,z)$ by a term containing free +occurrences of~$y$, since parameters are bound variables. \subsection{Two quantifier proofs: a success and a failure} \index{examples!with quantifiers} @@ -721,7 +733,7 @@ \paragraph{The right approach.} To do this proof, the rules must be applied in the correct order. -Eigenvariables should be created before unknowns. The +Parameters should be created before unknowns. The \ttindex{choplev} command returns to an earlier stage of the proof; let us return to the result of applying~$({\imp}I)$: \begin{ttbox} @@ -768,8 +780,8 @@ \index{tacticals} \index{examples!of tacticals} Repeated application of rules can be effective, but the rules should be -attempted in an order that delays the creation of unknowns. Let us return -to the original goal using \ttindex{choplev}: +attempted in the correct order. Let us return to the original goal using +\ttindex{choplev}: \begin{ttbox} choplev 0; {\out Level 0} @@ -853,12 +865,13 @@ \index{classical reasoner} Although Isabelle cannot compete with fully automatic theorem provers, it provides enough automation to tackle substantial examples. The classical -reasoner can be set up for any classical natural deduction logic ---- see the {\em Reference Manual}. +reasoner can be set up for any classical natural deduction logic; +see \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% + {Chap.\ts\ref{chap:classical}}. -Rules are packaged into bundles called {\bf classical sets}. The package -provides several tactics, which apply rules using naive algorithms, using -unification to handle quantifiers. The most useful tactic +Rules are packaged into {\bf classical sets}. The classical reasoner +provides several tactics, which apply rules using naive algorithms. +Unification handles quantifiers as shown above. The most useful tactic is~\ttindex{fast_tac}. Let us solve problems~40 and~60 of Pelletier~\cite{pelletier86}. (The @@ -900,8 +913,9 @@ {\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))} {\out No subgoals!} \end{ttbox} -The classical reasoner is not restricted to the usual logical -connectives. The natural deduction rules for unions and intersections in -set theory resemble those for disjunction and conjunction, and in the -infinitary case, for quantifiers. The package is valuable for reasoning in -set theory. +The classical reasoner is not restricted to the usual logical connectives. +The natural deduction rules for unions and intersections resemble those for +disjunction and conjunction. The rules for infinite unions and +intersections resemble those for quantifiers. Given such rules, the classical +reasoner is effective for reasoning in set theory. +