author wenzelm Mon, 12 May 1997 16:46:07 +0200 changeset 3160 08e364dfe518 parent 3159 22ebe2bd5e45 child 3161 d2c6f15f38f4
minor tuning;
 doc-src/Logics/HOL.tex file | annotate | diff | comparison | revisions
--- 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)"`