summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Intro/foundations.tex

changeset 3103 | 98af809fee46 |

parent 1878 | ac8e534b4834 |

child 3106 | 5396e99c02af |

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