# HG changeset patch # User wenzelm # Date 862831451 -7200 # Node ID 98af809fee4692aacc0b215321083ea03f387ef1 # Parent 4d01cdc119d20a05e8c6450e7dda49b7807e441c misc updates, tuning, cleanup; diff -r 4d01cdc119d2 -r 98af809fee46 doc-src/Intro/advanced.tex --- a/doc-src/Intro/advanced.tex Mon May 05 12:15:53 1997 +0200 +++ b/doc-src/Intro/advanced.tex Mon May 05 13:24:11 1997 +0200 @@ -3,14 +3,15 @@ Before continuing, it might be wise to try some of your own examples in Isabelle, reinforcing your knowledge of the basic functions. -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 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. +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 +mathematical reasoning and, again, many examples are in the +literature. Higher-order logic~({\tt HOL}) is Isabelle's most +elaborate logic. 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 @@ -36,11 +37,12 @@ \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} to discharge them +\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. Let us derive $\conj$ elimination using Isabelle. @@ -91,13 +93,13 @@ {\out No subgoals!} \end{ttbox} Calling \ttindex{topthm} returns the current proof state as a theorem. -Note that it contains assumptions. Calling \ttindex{result} discharges the -assumptions --- both occurrences of $P\conj Q$ are discharged as one --- -and makes the variables schematic. +Note that it contains assumptions. Calling \ttindex{qed} discharges +the assumptions --- both occurrences of $P\conj Q$ are discharged as +one --- and makes the variables schematic. \begin{ttbox} topthm(); {\out val it = "R [P & Q, P & Q, [| P; Q |] ==> R]" : thm} -val conjE = result(); +qed "conjE"; {\out val conjE = "[| ?P & ?Q; [| ?P; ?Q |] ==> ?R |] ==> ?R" : thm} \end{ttbox} @@ -139,8 +141,8 @@ \[ \infer[({\neg}I)]{\neg P}{\infer*{\bot}{[P]}} \qquad \infer[({\neg}E)]{Q}{\neg P & P} \] This requires proving the following meta-formulae: -$$ (P\Imp\bot) \Imp \neg P \eqno(\neg I)$$ -$$ \List{\neg P; P} \Imp Q. \eqno(\neg E)$$ +$$ (P\Imp\bot) \Imp \neg P \eqno(\neg I) $$ +$$ \List{\neg P; P} \Imp Q. \eqno(\neg E) $$ \subsection{Deriving the $\neg$ introduction rule} @@ -185,7 +187,7 @@ {\out ~P} {\out No subgoals!} \ttbreak -val notI = result(); +qed "notI"; {\out val notI = "(?P ==> False) ==> ~?P" : thm} \end{ttbox} \indexbold{*notI theorem} @@ -251,7 +253,7 @@ {\out Level 4} {\out R} {\out No subgoals!} -val notE = result(); +qed "notE"; {\out val notE = "[| ~?P; ?P |] ==> ?R" : thm} \end{ttbox} \indexbold{*notE theorem} @@ -313,10 +315,10 @@ {\out !!P R. [| ~ P; P |] ==> R} {\out No subgoals!} \end{ttbox} -Calling \ttindex{result} strips the meta-quantifiers, so the resulting +Calling \ttindex{qed} strips the meta-quantifiers, so the resulting theorem is the same as before. \begin{ttbox} -val notE = result(); +qed "notE"; {\out val notE = "[| ~?P; ?P |] ==> ?R" : thm} \end{ttbox} Do not use the {\tt!!}\ trick if the premises contain meta-level @@ -328,62 +330,67 @@ \section{Defining theories}\label{sec:defining-theories} \index{theories!defining|(} -Isabelle makes no distinction between simple extensions of a logic --- like -defining a type~$bool$ with constants~$true$ and~$false$ --- and defining -an entire logic. A theory definition has the form +Isabelle makes no distinction between simple extensions of a logic --- +like specifying a type~$bool$ with constants~$true$ and~$false$ --- +and defining an entire logic. A theory definition has a form like \begin{ttbox} \(T\) = \(S@1\) + \(\cdots\) + \(S@n\) + classes {\it class declarations} default {\it sort} types {\it type declarations and synonyms} -arities {\it arity declarations} +arities {\it type arity declarations} consts {\it constant declarations} -translations {\it translation declarations} -defs {\it definitions} +syntax {\it syntactic constant declarations} +translations {\it ast translation rules} +defs {\it meta-logical definitions} rules {\it rule declarations} end ML {\it ML code} \end{ttbox} This declares the theory $T$ to extend the existing theories -$S@1$,~\ldots,~$S@n$. It may declare new classes, types, arities -(overloadings of existing types), constants and rules; it can specify the -default sort for type variables. A constant declaration can specify an -associated concrete syntax. The translations section specifies rewrite -rules on abstract syntax trees, for defining notations and abbreviations. -\index{*ML section} -The {\tt ML} section contains code to perform arbitrary syntactic -transformations. The main declaration forms are discussed below. -The full syntax can be found in \iflabelundefined{app:TheorySyntax}{the - appendix of the {\it Reference Manual}}{App.\ts\ref{app:TheorySyntax}}. +$S@1$,~\ldots,~$S@n$. It may introduce new classes, types, arities +(of existing types), constants and rules; it can specify the default +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 +code to perform arbitrary syntactic transformations. The main +declaration forms are discussed below. The full syntax can be found +in \iflabelundefined{app:TheorySyntax}{an appendix of the {\it + Reference Manual}}{App.\ts\ref{app:TheorySyntax}}. Also note that +object-logics may add further theory sections, for example {\tt + typedef}, {\tt datatype} in \HOL. -All the declaration parts can be omitted or repeated and may appear in any -order, except that the {\ML} section must be last. In the simplest case, $T$ -is just the union of $S@1$,~\ldots,~$S@n$. New theories always extend one or -more other theories, inheriting their types, constants, syntax, etc. The -theory \thydx{Pure} contains nothing but Isabelle's meta-logic. +All the declaration parts can be omitted or repeated and may appear in +any order, except that the {\ML} section must be last (after the {\tt + end} keyword). In the simplest case, $T$ is just the union of +$S@1$,~\ldots,~$S@n$. New theories always extend one or more other +theories, inheriting their types, constants, syntax, etc. The theory +\thydx{Pure} contains nothing but Isabelle's meta-logic. The variant +\thydx{CPure} offers the more usual higher-order function application +syntax $t\,u@1\ldots\,u@n$ instead of $t(u@1,\ldots,u@n)$. -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. +Each theory definition must reside in a separate file, whose name is +the theory's with {\tt.thy} appended. Calling +\ttindexbold{use_thy}~{\tt"{\it T\/}"} reads the definition from {\it + 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 +rule, and everything declared in {\it ML code}. -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 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}. -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 -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 +\ttindexbold{use_thy} automatically loads a theory's parents before +loading the theory itself. When a theory file is modified, many +theories may have to be reloaded. Isabelle records the modification +times and dependencies of theory files. See \iflabelundefined{sec:reloading-theories}{the {\em Reference Manual\/}}% {\S\ref{sec:reloading-theories}} for more details. @@ -418,23 +425,23 @@ $rule@n$ are expressions of type~$prop$. Each rule {\em must\/} be 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 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. Isabelle also -allows a derived form where the arguments of~$f$ appear on the left: -\begin{itemize} -\item In uncurried syntax: $f(x@1,\dots,x@n) \equiv u$ (\FOL, \ZF, \dots) -\item In curried syntax: $f~x@1~\dots~x@n \equiv u$ (\HOL, \HOLCF) -\end{itemize} -Isabelle checks for common errors in definitions, such as extra variables on -the right-hand side. Determined users can write non-conservative -`definitions' by using mutual recursion, for example; the consequences of -such actions are their responsibility. +\indexbold{definitions} The {\bf definition part} is similar, but with +the keyword {\tt defs} instead of {\tt 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, +where the arguments of~$f$ appear applied on the left-hand side of the +equation instead of abstracted on the right-hand side. -\index{examples!of theories} -This theory extends first-order logic by declaring and defining two constants, -{\em nand} and {\em xor}: +Isabelle checks for common errors in definitions, such as extra +variables on the right-hand side, but currently does not a complete +test of well-formedness. Thus determined users can write +non-conservative `definitions' by using mutual recursion, for example; +the consequences of such actions are their responsibility. + +\index{examples!of theories} This example theory extends first-order +logic by declaring and defining two constants, {\em nand} and {\em + xor}: \begin{ttbox} Gate = FOL + consts nand,xor :: [o,o] => o @@ -557,11 +564,11 @@ arities \(tycon@1\), \ldots, \(tycon@n\) :: \(arity\) \end{ttbox} -\begin{warn} -Arity declarations resemble constant declarations, but there are {\it no\/} -quotation marks! Types and rules must be quoted because the theory -translator passes them verbatim to the {\ML} output file. -\end{warn} +%\begin{warn} +%Arity declarations resemble constant declarations, but there are {\it no\/} +%quotation marks! Types and rules must be quoted because the theory +%translator passes them verbatim to the {\ML} output file. +%\end{warn} \subsection{Type synonyms}\indexbold{type synonyms} Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar @@ -579,11 +586,11 @@ signal = nat stream 'a list \end{ttbox} -A synonym is merely an abbreviation for some existing type expression. Hence -synonyms may not be recursive! Internally all synonyms are fully expanded. As -a consequence Isabelle output never contains synonyms. Their main purpose is -to improve the readability of theories. Synonyms can be used just like any -other type: +A synonym is merely an abbreviation for some existing type expression. +Hence synonyms may not be recursive! Internally all synonyms are +fully expanded. As a consequence Isabelle output never contains +synonyms. Their main purpose is to improve the readability of theory +definitions. Synonyms can be used just like any other type: \begin{ttbox} consts and,or :: gate negate :: signal => signal @@ -623,10 +630,10 @@ if~$P$ then~$Q$ else~$R$} as well as {\tt If($P$,$Q$,$R$)}. Underscores denote argument positions. -The declaration above does not allow the {\tt if}-{\tt then}-{\tt else} -construct to be 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 +The declaration above does not allow the {\tt if}-{\tt 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 \iflabelundefined{Defining-Logics}% {the {\it Reference Manual}, chapter `Defining Logics'}% {Chap.\ts\ref{Defining-Logics}}. @@ -672,9 +679,11 @@ \end{ttbox} \begin{warn} -The name of the type constructor is~{\tt *} and not {\tt op~*}, as it would -be in the case of an infix constant. Only infix type constructors can have -symbolic names like~{\tt *}. There is no general mixfix syntax for types. + The name of the type constructor is~{\tt *} and not {\tt 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} + declarations. \end{warn} @@ -826,11 +835,7 @@ \end{ttbox} In axiom {\tt add_def}, recall that \verb|%| stands for~$\lambda$. Loading this theory file creates the \ML\ structure {\tt Nat}, which -contains the theory and axioms. Opening structure {\tt Nat} lets us write -{\tt induct} instead of {\tt Nat.induct}, and so forth. -\begin{ttbox} -open Nat; -\end{ttbox} +contains the theory and axioms. \subsection{Proving some recursion equations} File {\tt FOL/ex/Nat.ML} contains proofs involving this theory of the @@ -846,7 +851,7 @@ {\out Level 1} {\out 0 + n = n} {\out No subgoals!} -val add_0 = result(); +qed "add_0"; \end{ttbox} And here is the successor case: \begin{ttbox} @@ -859,7 +864,7 @@ {\out Level 1} {\out Suc(m) + n = Suc(m + n)} {\out No subgoals!} -val add_Suc = result(); +qed "add_Suc"; \end{ttbox} The induction rule raises some complications, which are discussed next. \index{theories!defining|)} diff -r 4d01cdc119d2 -r 98af809fee46 doc-src/Intro/foundations.tex --- a/doc-src/Intro/foundations.tex Mon May 05 12:15:53 1997 +0200 +++ b/doc-src/Intro/foundations.tex Mon May 05 13:24:11 1997 +0200 @@ -72,11 +72,13 @@ form $(\sigma,\tau)fun$ or $\sigma\To\tau$, where $\sigma$ and $\tau$ are types. Curried function types may be abbreviated: \[ \sigma@1\To (\cdots \sigma@n\To \tau\cdots) \quad \hbox{as} \quad - [\sigma@1, \ldots, \sigma@n] \To \tau \] +[\sigma@1, \ldots, \sigma@n] \To \tau \] -\index{terms!syntax of} -The syntax for terms is summarised below. Note that function application is -written $t(u)$ rather than the usual $t\,u$. +\index{terms!syntax of} The syntax for terms is summarised below. +Note that there are two versions of function application syntax +available in Isabelle: either $t\,u$, which is the usual form for +higher-order languages, or $t(u)$, trying to look more like +first-order. The latter syntax is used throughout the manual. \[ \index{lambda abs@$\lambda$-abstractions}\index{function applications} \begin{array}{ll} @@ -322,7 +324,9 @@ One of the simplest rules is $(\conj E1)$. Making everything explicit, its formalization in the meta-logic is -$$ \Forall P\;Q. Trueprop(P\conj Q) \Imp Trueprop(P). \eqno(\conj E1) $$ +$$ +\Forall P\;Q. Trueprop(P\conj Q) \Imp Trueprop(P). \eqno(\conj E1) +$$ This may look formidable, but it has an obvious reading: for all object-level truth values $P$ and~$Q$, if $P\conj Q$ is true then so is~$P$. The reading is correct because the meta-logic has simple models, where @@ -400,13 +404,13 @@ The $\forall E$ rule exploits $\beta$-conversion. Hiding $Trueprop$, the $\forall$ axioms are $$ \left(\Forall x. P(x)\right) \Imp \forall x.P(x) \eqno(\forall I) $$ -$$ (\forall x.P(x)) \Imp P(t). \eqno(\forall E)$$ +$$ (\forall x.P(x)) \Imp P(t). \eqno(\forall E) $$ \noindent We have defined the object-level universal quantifier~($\forall$) using~$\Forall$. But we do not require meta-level counterparts of all the connectives of the object-logic! Consider the existential quantifier: -$$ P(t) \Imp \exists x.P(x) \eqno(\exists I)$$ +$$ P(t) \Imp \exists x.P(x) \eqno(\exists I) $$ $$ \List{\exists x.P(x);\; \Forall x. P(x)\Imp Q} \Imp Q \eqno(\exists E) $$ Let us verify $(\exists E)$ semantically. Suppose that the premises hold; since $\exists x.P(x)$ is true, we may choose an~$a$ such that $P(a)$ is @@ -420,47 +424,48 @@ rule~$(subst)$ uses~$P$ as a template for substitution, inferring $P[u/x]$ from~$P[t/x]$. When we formalize this as an axiom, the template becomes a function variable: -$$ \List{t=u; P(t)} \Imp P(u). \eqno(subst)$$ +$$ \List{t=u; P(t)} \Imp P(u). \eqno(subst) $$ \subsection{Signatures and theories} \index{signatures|bold} A {\bf signature} contains the information necessary for type checking, -parsing and pretty printing a term. It specifies classes and their +parsing and pretty printing a term. It specifies type classes and their relationships, types and their arities, constants and their types, etc. It -also contains syntax rules, specified using mixfix declarations. +also contains grammar 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. Under similar conditions, a signature can be extended. Signatures are managed internally by Isabelle; users seldom encounter them. -\index{theories|bold} -A {\bf theory} consists of a signature plus a collection of axioms. The -{\bf pure} theory contains only the meta-logic. Theories can be combined -provided their signatures are compatible. A theory definition extends an -existing theory with further signature specifications --- classes, types, -constants and mixfix declarations --- plus a list of axioms, expressed as -strings to be parsed. A theory can formalize a small piece of mathematics, -such as lists and their operations, or an entire logic. A mathematical -development typically involves many theories in a hierarchy. For example, -the pure theory could be extended to form a theory for -Fig.\ts\ref{fol-fig}; this could be extended in two separate ways to form a -theory for natural numbers and a theory for lists; the union of these two -could be extended into a theory defining the length of a list: +\index{theories|bold} A {\bf theory} consists of a signature plus a +collection of axioms. The {\Pure} theory contains only the +meta-logic. Theories can be combined provided their signatures are +compatible. A theory definition extends an existing theory with +further signature specifications --- classes, types, constants and +mixfix declarations --- plus lists of axioms and definitions etc., +expressed as strings to be parsed. A theory can formalize a small +piece of mathematics, such as lists and their operations, or an entire +logic. A mathematical development typically involves many theories in +a hierarchy. For example, the {\Pure} theory could be extended to +form a theory for Fig.\ts\ref{fol-fig}; this could be extended in two +separate ways to form a theory for natural numbers and a theory for +lists; the union of these two could be extended into a theory defining +the length of a list: \begin{tt} \[ \begin{array}{c@{}c@{}c@{}c@{}c} - {} & {} & \hbox{Length} & {} & {} \\ - {} & {} & \uparrow & {} & {} \\ - {} & {} &\hbox{Nat}+\hbox{List}& {} & {} \\ - {} & \nearrow & {} & \nwarrow & {} \\ + {} & {} &\hbox{Pure}& {} & {} \\ + {} & {} & \downarrow & {} & {} \\ + {} & {} &\hbox{FOL} & {} & {} \\ + {} & \swarrow & {} & \searrow & {} \\ \hbox{Nat} & {} & {} & {} & \hbox{List} \\ - {} & \nwarrow & {} & \nearrow & {} \\ - {} & {} &\hbox{FOL} & {} & {} \\ - {} & {} & \uparrow & {} & {} \\ - {} & {} &\hbox{Pure}& {} & {} + {} & \searrow & {} & \swarrow & {} \\ + {} & {} &\hbox{Nat}+\hbox{List}& {} & {} \\ + {} & {} & \downarrow & {} & {} \\ + {} & {} & \hbox{Length} & {} & {} \end{array} \] \end{tt}% @@ -472,7 +477,7 @@ \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. + constant and in another as a variable, for example. \end{warn} \section{Proof construction in Isabelle} @@ -566,7 +571,7 @@ where $\Var{h@1}$, \ldots, $\Var{h@m}$ are new unknowns. Assuming there are no other occurrences of~$\Var{f}$, equation~(\ref{hou-eqn}) simplifies to the equation -\[ t(\Var{h@1}(t),\ldots,\Var{h@m}(t)) \qeq g(u@1,\ldots,u@k). $$ +\[ t(\Var{h@1}(t),\ldots,\Var{h@m}(t)) \qeq g(u@1,\ldots,u@k). \] \begin{warn}\index{unification!incompleteness of}% Huet's unification procedure is complete. Isabelle's polymorphic version, @@ -634,11 +639,11 @@ one for each unifier of $\psi$ with $\phi@i$. Isabelle returns these conclusions as a sequence (lazy list). -Resolution expects the rules to have no outer quantifiers~($\Forall$). It -may rename or instantiate any schematic variables, but leaves free -variables unchanged. When constructing a theory, Isabelle puts the rules -into a standard form containing no free variables; for instance, $({\imp}E)$ -becomes +Resolution expects the rules to have no outer quantifiers~($\Forall$). +It may rename or instantiate any schematic variables, but leaves free +variables unchanged. When constructing a theory, Isabelle puts the +rules into a standard form containing only schematic variables; +for instance, $({\imp}E)$ becomes \[ \List{\Var{P}\imp \Var{Q}; \Var{P}} \Imp \Var{Q}. \] When resolving two rules, the unknowns in the first rule are renamed, by @@ -770,7 +775,7 @@ forward from facts. It can also support backward proof, where we start with a goal and refine it to progressively simpler subgoals until all have been solved. {\sc lcf} and its descendants {\sc hol} and Nuprl provide -tactics and tacticals, which constitute a high-level language for +tactics and tacticals, which constitute a sophisticated language for expressing proof searches. {\bf Tactics} refine subgoals while {\bf tacticals} combine tactics. @@ -1074,7 +1079,7 @@ Elim-resolution's simultaneous unification gives better control than ordinary resolution. Recall the substitution rule: $$ \List{\Var{t}=\Var{u}; \Var{P}(\Var{t})} \Imp \Var{P}(\Var{u}) - \eqno(subst) $$ +\eqno(subst) $$ Unsuitable for ordinary resolution because $\Var{P}(\Var{u})$ admits many unifiers, $(subst)$ works well with elim-resolution. It deletes some assumption of the form $x=y$ and replaces every~$y$ by~$x$ in the subgoal @@ -1146,7 +1151,7 @@ meta-theorem $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, with no assumptions. This represents the desired rule. Let us derive the general $\conj$ elimination rule: -$$ \infer{R}{P\conj Q & \infer*{R}{[P,Q]}} \eqno(\conj E)$$ +$$ \infer{R}{P\conj Q & \infer*{R}{[P,Q]}} \eqno(\conj E) $$ We assume $P\conj Q$ and $\List{P;Q}\Imp R$, and commence backward proof in the state $R\Imp R$. Resolving this with the second assumption yields the state diff -r 4d01cdc119d2 -r 98af809fee46 doc-src/Intro/getting.tex --- a/doc-src/Intro/getting.tex Mon May 05 12:15:53 1997 +0200 +++ b/doc-src/Intro/getting.tex Mon May 05 13:24:11 1997 +0200 @@ -1,19 +1,25 @@ %% $Id$ \part{Getting Started with Isabelle}\label{chap:getting} -Let us consider how to perform simple proofs using Isabelle. At present, -Isabelle's user interface is \ML. Proofs are conducted by applying certain -\ML{} functions, which update a stored proof state. All syntax must be -expressed using {\sc ascii} characters. Menu-driven graphical interfaces -are under construction, but Isabelle users will always need to know some -\ML, at least to use tacticals. +Let us consider how to perform simple proofs using Isabelle. At +present, Isabelle's user interface is \ML. Proofs are conducted by +applying certain \ML{} functions, which update a stored proof state. +Basically, all syntax must be expressed using plain {\sc ascii} +characters. There are also mechanisms built into Isabelle that support +alternative syntaxes, for example using mathematical symbols from a +special screen font. The meta-logic and major object-logics already +provide such fancy output as an option. -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 users can operate on these data structures by -writing \ML{} programs. +%FIXME remove +%Menu-driven graphical interfaces are under construction, but Isabelle +%users will always need to know some \ML, at least to use tacticals. + +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 +users can operate on these data structures by writing \ML{} programs. \section{Forward proof}\label{sec:forward} \index{forward proof|(} This section describes the concrete syntax for types, terms and theorems, @@ -65,10 +71,11 @@ 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{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\}}. +\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 + ord, arith\ttrbrace}. \[\dquotes \index{*:: symbol}\index{*=> symbol} \index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol} @@ -76,7 +83,7 @@ \begin{array}{lll} \multicolumn{3}{c}{\hbox{ASCII Notation for Types}} \\ \hline \alpha "::" C & \alpha :: C & \hbox{class constraint} \\ - \alpha "::" "\{" C@1 "," \ldots "," C@n "\}" & + \alpha "::" "\ttlbrace" C@1 "," \ldots "," C@n "\ttrbrace" & \alpha :: \{C@1,\dots,C@n\} & \hbox{sort constraint} \\ \sigma " => " \tau & \sigma\To\tau & \hbox{function type} \\ "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau & @@ -118,7 +125,7 @@ \List{\phi@1;\ldots;\phi@n} \Imp \psi & \hbox{nested implication} \\ "!!" x "." \phi & \Forall x.\phi & \hbox{meta-quantification} \\ "!!" x@1\ldots x@n "." \phi & - \Forall x@1. \ldots \Forall x@n.\phi & \hbox{nested quantification} + \Forall x@1. \ldots x@n.\phi & \hbox{nested quantification} \end{array} \] Flex-flex constraints are meta-equalities arising from unification; they @@ -138,8 +145,8 @@ PROP ?psi ==> PROP ?theta \end{ttbox} -Symbols of object-logics also must be rendered into {\sc ascii}, typically -as follows: +Symbols of object-logics are typically rendered into {\sc ascii} as +follows: \[ \begin{tabular}{l@{\quad}l@{\quad}l} \tt True & $\top$ & true \\ \tt False & $\bot$ & false \\ @@ -154,9 +161,8 @@ \] To illustrate the notation, consider two axioms for first-order logic: $$ \List{P; Q} \Imp P\conj Q \eqno(\conj I) $$ -$$ \List{\exists x.P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E) $$ -Using the {\tt [|\ldots|]} shorthand, $({\conj}I)$ translates into -{\sc ascii} characters as +$$ \List{\exists x.P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E) $$ +$({\conj}I)$ translates into {\sc ascii} characters as \begin{ttbox} [| ?P; ?Q |] ==> ?P & ?Q \end{ttbox} @@ -406,14 +412,19 @@ applies the {\it tactic\/} to the current proof state, raising an exception if the tactic fails. -\item[\ttindex{undo}(); ] +\item[\ttindex{undo}(); ] reverts to the previous proof state. Undo can be repeated but cannot be undone. Do not omit the parentheses; typing {\tt\ \ undo;\ \ } merely causes \ML\ to echo the value of that function. -\item[\ttindex{result}()] +\item[\ttindex{result}();] returns the theorem just proved, in a standard format. It fails if 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 + theorem database and binds it to an \ML{} identifier. + \end{ttdescription} The commands and tactics given above are cumbersome for interactive use. Although our examples will use the full commands, you may prefer Isabelle's @@ -494,9 +505,9 @@ {\out No subgoals!} \end{ttbox} Isabelle tells us that there are no longer any subgoals: the proof is -complete. Calling {\tt result} returns the theorem. +complete. Calling {\tt qed} stores the theorem. \begin{ttbox} -val mythm = result(); +qed "mythm"; {\out val mythm = "?P | ?P --> ?P" : thm} \end{ttbox} Isabelle has replaced the free variable~{\tt P} by the scheme @@ -664,7 +675,7 @@ The reflexivity axiom does not unify with subgoal~1. \begin{ttbox} by (resolve_tac [refl] 1); -{\out by: tactic returned no results} +{\out by: tactic failed} \end{ttbox} There can be no proof of $\exists y.\forall x.x=y$ by the soundness of first-order logic. I have elsewhere proved the faithfulness of Isabelle's @@ -727,7 +738,7 @@ proof by assumption will fail. \begin{ttbox} by (assume_tac 1); -{\out by: tactic returned no results} +{\out by: tactic failed} {\out uncaught exception ERROR} \end{ttbox}