--- a/doc-src/Logics/HOL.tex Mon May 12 16:44:58 1997 +0200
+++ b/doc-src/Logics/HOL.tex Mon May 12 16:46:07 1997 +0200
@@ -197,7 +197,8 @@
\subsection{Binders}
-Hilbert's {\bf description} operator~$\varepsilon x.P\,x$ stands for
+
+Hilbert's {\bf description} operator~$\varepsilon x.P[x]$ stands for
some~$x$ satisfying~$P$, if such exists. Since all terms in \HOL\
denote something, a description is always meaningful, but we do not
know its value unless $P$ defines it uniquely. We may write
@@ -209,8 +210,8 @@
The unique existence quantifier, $\exists!x.P$, is defined in terms
of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested
quantifications. For instance, $\exists!x\,y.P\,x\,y$ abbreviates
-$\exists!x. \exists!y.P~x~y$; note that this does not mean that there
-exists a unique pair $(x,y)$ satisfying~$P~x~y$.
+$\exists!x. \exists!y.P\,x\,y$; note that this does not mean that there
+exists a unique pair $(x,y)$ satisfying~$P\,x\,y$.
\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system}
Quantifiers have two notations. As in Gordon's {\sc hol} system, \HOL\
@@ -227,11 +228,10 @@
variable of type $\tau$, then the term \cdx{LEAST}~$x.P[x]$ is defined
to be the least (w.r.t.\ $\le$) $x$ such that $P~x$ holds (see
Fig.~\ref{hol-defs}). The definition uses Hilbert's $\varepsilon$
-choice operator. So this is always meaningful, but may yield nothing
-useful in case there is not a unique least element satisfying
-$P$.\footnote{Note that class $ord$ does not require much of its
- instances, so $\le$ need not be a well-ordering, not even an order
- at all!}
+choice operator, so \texttt{Least} is always meaningful, but may yield
+nothing useful in case there is not a unique least element satisfying
+$P$.\footnote{Class $ord$ does not require much of its instances, so
+ $\le$ need not be a well-ordering, not even an order at all!}
\medskip All these binders have priority 10.
@@ -281,8 +281,9 @@
\caption{The {\tt HOL} rules} \label{hol-rules}
\end{figure}
-Figure~\ref{hol-rules} shows the inference rules of~\HOL{}, with their~{\ML}
-names. Some of the rules deserve additional comments:
+Figure~\ref{hol-rules} shows the primitive inference rules of~\HOL{},
+with their~{\ML} names. Some of the rules deserve additional
+comments:
\begin{ttdescription}
\item[\tdx{ext}] expresses extensionality of functions.
\item[\tdx{iff}] asserts that logically equivalent formulae are
@@ -449,7 +450,7 @@
& insertion of element \\
\cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$
& comprehension \\
- \cdx{Compl} & $(\alpha\,set)\To\alpha\,set$
+ \cdx{Compl} & $\alpha\,set\To\alpha\,set$
& complement \\
\cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
& intersection over a set\\
@@ -1177,7 +1178,7 @@
\subsection{The type of natural numbers, {\tt nat}}
The theory \thydx{NatDef} defines the natural numbers in a roundabout
-but traditional way. The axiom of infinity postulates an
+but traditional way. The axiom of infinity postulates a
type~\tydx{ind} of individuals, which is non-empty and closed under an
injective operation. The natural numbers are inductively generated by
choosing an arbitrary individual for~0 and using the injective
@@ -1402,13 +1403,14 @@
Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
unsound, because $\exists x. x=x$ is a theorem \cite[\S7]{paulson-COLOG}.
\end{warn}
-A \bfindex{type definition} identifies the new type with a subset of an
-existing type. More precisely, the new type is defined by exhibiting an
-existing type~$\tau$, a set~$A::(\tau)set$, and a theorem of the form $x:A$.
-Thus~$A$ is a non-empty subset of~$\tau$, and the new type denotes this
-subset. New functions are defined that establish an isomorphism between the
-new type and the subset. If type~$\tau$ involves type variables $\alpha@1$,
-\ldots, $\alpha@n$, then the type definition creates a type constructor
+A \bfindex{type definition} identifies the new type with a subset of
+an existing type. More precisely, the new type is defined by
+exhibiting an existing type~$\tau$, a set~$A::\tau\,set$, and a
+theorem of the form $x:A$. Thus~$A$ is a non-empty subset of~$\tau$,
+and the new type denotes this subset. New functions are defined that
+establish an isomorphism between the new type and the subset. If
+type~$\tau$ involves type variables $\alpha@1$, \ldots, $\alpha@n$,
+then the type definition creates a type constructor
$(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular type.
\begin{figure}[htbp]
@@ -1442,7 +1444,7 @@
`typevarlist', no extra type variables in `set', and no free term variables
in `set'), the following components are added to the theory:
\begin{itemize}
-\item a type $ty :: (term,\dots)term$;
+\item a type $ty :: (term,\dots,term)term$
\item constants
\begin{eqnarray*}
T &::& \tau\;set \\
@@ -1461,8 +1463,8 @@
stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$
and its inverse $Abs_T$.
\end{itemize}
-Below are two simple examples of \HOL\ type definitions. Emptiness is
-proved automatically here.
+Below are two simple examples of \HOL\ type definitions. Non-emptiness
+is proved automatically here.
\begin{ttbox}
typedef unit = "{\ttlbrace}True{\ttrbrace}"
@@ -1498,12 +1500,13 @@
\label{sec:HOL:datatype}
\index{*datatype|(}
-Inductive datatypes similar to those of \ML{} frequently appear in
+Inductive datatypes, similar to those of \ML, frequently appear in
non-trivial applications of \HOL. In principle, such types could be
defined by hand via \texttt{typedef} (see \S\ref{sec:typedef}), but
this would be far too tedious. The \ttindex{datatype} definition
-package of \HOL\ automates such chores. It generates freeness and
-induction rules from a very simple description provided by the user.
+package of \HOL\ automates such chores. It generates freeness theorems
+and induction rules from a very simple description of the new type
+provided by the user.
\subsection{Basics}
@@ -1527,7 +1530,7 @@
\item the newly defined type $(\alpha@1, \dots, \alpha@n) \, t$.
\end{itemize}
Recursive occurences of $(\alpha@1, \dots, \alpha@n) \, t$ are quite
-restricted. To ensure that the new type is not empty, at least one
+restricted. To ensure that the new type is non-empty, at least one
constructor must consist of only non-recursive type components. If
you would like one of the $\tau@{ij}$ to be a complex type expression
$\tau$ you need to declare a new type synonym $syn = \tau$ first and
@@ -1538,35 +1541,31 @@
The constructors are automatically defined as functions of their respective
type:
-\[ C@j : [\tau@{j1},\dots,\tau@{jk@j}] \To (\alpha@1,\dots,\alpha@n)t \]
-These functions have certain {\em freeness} properties:
-\begin{itemize}
-
-\item They are distinct:
- \[
- C@i~x@1~\dots~x@{k@i} \neq C@j~y@1~\dots~y@{k@j} \qquad
- \mbox{for all}~ i \neq j.
- \]
-
-\item They are injective:
- \[
- (C@j~x@1~\dots~x@{k@j} = C@j~y@1~\dots~y@{k@j}) =
- (x@1 = y@1 \land \dots \land x@{k@j} = y@{k@j})
- \]
-\end{itemize}
+\[ C@j :: [\tau@{j1},\dots,\tau@{jk@j}] \To (\alpha@1,\dots,\alpha@n)t \]
+These functions have certain {\em freeness} properties --- they are
+distinct:
+\[
+C@i~x@1~\dots~x@{k@i} \neq C@j~y@1~\dots~y@{k@j} \qquad
+\mbox{for all}~ i \neq j.
+\]
+and they are injective:
+\[
+(C@j~x@1~\dots~x@{k@j} = C@j~y@1~\dots~y@{k@j}) =
+(x@1 = y@1 \land \dots \land x@{k@j} = y@{k@j})
+\]
Because the number of inequalities is quadratic in the number of
constructors, a different representation is used if there are $7$ or
more of them. In that case every constructor term is mapped to a
natural number:
\[
-t_ord \, (C@i \, x@1 \, \dots \, x@{k@1}) = i - 1
+t_ord \, (C@i \, x@1 \, \dots \, x@{k@i}) = i - 1
\]
Then distinctness of constructor terms is expressed by:
\[
t_ord \, x \neq t_ord \, y \Imp x \neq y.
\]
-\medskip Furthermore, the following structural induction rule is
+\medskip Generally, the following structural induction rule is
provided:
\[
\infer{P \, x}
@@ -1584,7 +1583,7 @@
= (\alpha@1,\dots,\alpha@n)t \}$, i.e.\ the property $P$ can be assumed for
all arguments of the recursive type.
-The type also comes with an \ML-like \sdx{case}-construct:
+\medskip The type also comes with an \ML-like \sdx{case}-construct:
\[
\begin{array}{rrcl}
\mbox{\tt case}~e~\mbox{\tt of} & C@1~x@{11}~\dots~x@{1k@1} & \To & e@1 \\
@@ -1663,7 +1662,7 @@
\subsubsection{The datatype $\alpha~list$}
We want to define the type $\alpha~list$.\footnote{This is just an
- example. There is already a list type in \HOL, of course.} To do
+ example, there is already a list type in \HOL, of course.} To do
this we have to build a new theory that contains the type definition.
We start from the basic {\tt HOL} theory.
\begin{ttbox}
@@ -1671,8 +1670,10 @@
datatype 'a list = Nil | Cons 'a ('a list)
end
\end{ttbox}
-After loading the theory (\verb$use_thy "MyList"$), we can prove
-$Cons~x~xs\neq xs$.
+After loading the theory (with \verb$use_thy "MyList"$), we can prove
+$Cons~x~xs\neq xs$. To ease the induction applied below, we state the
+goal with $x$ quantified at the object-level. This will be stripped
+later using \ttindex{qed_spec_mp}.
\begin{ttbox}
goal MyList.thy "!x. Cons x xs ~= xs";
{\out Level 0}
@@ -1706,9 +1707,12 @@
{\out Level 3}
{\out ! x. Cons x xs ~= xs}
{\out No subgoals!}
+\ttbreak
+qed_spec_mp "not_Cons_self";
+{\out val not_Cons_self = "Cons x xs ~= xs";}
\end{ttbox}
-Because both subgoals were proved by almost the same tactic we could have
-done that in one step using
+Because both subgoals could have been proved by \texttt{Asm_simp_tac}
+we could have done that in one step:
\begin{ttbox}
by (ALLGOALS Asm_simp_tac);
\end{ttbox}
@@ -1736,16 +1740,16 @@
This example shows a datatype that consists of 7 constructors:
\begin{ttbox}
Days = Arith +
- datatype days = Mo | Tu | We | Th | Fr | Sa | So
+ datatype days = Mon | Tue | Wed | Thu | Fri | Sat | Sun
end
\end{ttbox}
-Because there are more than 6 constructors, the theory must be based on
-{\tt Arith}. Inequality is defined via a function \verb|days_ord|. The
-theorem \verb|Mo ~= Tu| is not directly contained among the distinctness
-theorems, but the simplifier can prove it thanks to rewrite rules inherited
-from theory {\tt Arith}.
+Because there are more than 6 constructors, the theory must be based
+on {\tt Arith}. Inequality is expressed via a function
+\verb|days_ord|. The theorem \verb|Mon ~= Tue| is not directly
+contained among the distinctness theorems, but the simplifier can
+prove it thanks to rewrite rules inherited from theory {\tt Arith}:
\begin{ttbox}
-goal Days.thy "Mo ~= Tu";
+goal Days.thy "Mon ~= Tue";
by (Simp_tac 1);
\end{ttbox}
You need not derive such inequalities explicitly: the simplifier will dispose
@@ -1763,7 +1767,7 @@
new axioms, e.g.\
\begin{ttbox}
Append = MyList +
-consts app :: ['a list,'a list] => 'a list
+consts app :: ['a list, 'a list] => 'a list
rules
app_Nil "app [] ys = ys"
app_Cons "app (x#xs) ys = x#app xs ys"
@@ -1776,7 +1780,7 @@
functions on datatypes --- \ttindex{primrec}:
\begin{ttbox}
Append = MyList +
-consts app :: ['a list,'a list] => 'a list
+consts app :: ['a list, 'a list] => 'a list
primrec app MyList.list
"app [] ys = ys"
"app (x#xs) ys = x#app xs ys"
@@ -1827,7 +1831,7 @@
The primitive recursive function can have infix or mixfix syntax:
\begin{ttbox}\underscoreon
Append = MyList +
-consts "@" :: ['a list,'a list] => 'a list (infixr 60)
+consts "@" :: ['a list, 'a list] => 'a list (infixr 60)
primrec "op @" MyList.list
"[] @ ys = ys"
"(x#xs) @ ys = x#(xs @ ys)"