doc-src/Logics/HOL.tex

   omitted search paths during unification.\index{tracing!of unification}
 \end{warn}
 
 
 \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
 descriptions as \cdx{Eps}($\lambda x.P[x]$) or use the syntax
 \hbox{\tt \at $x$.$P[x]$}.

 Existential quantification is defined by
 \[ \exists x.P~x \;\equiv\; P(\varepsilon x.P~x). \]
 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\
 uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$.  The
 existential quantifier must be followed by a space; thus {\tt?x} is an

 
 If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a
 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.
 
 \begin{warn}
 The low priority of binders means that they need to be enclosed in

 \tdx{True_or_False}  (P=True) | (P=False)
 \end{ttbox}
 \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
   equal.
 \item[\tdx{selectI}] gives the defining property of the Hilbert

   \verb|{}|     & $\alpha\,set$         & the empty set \\
   \cdx{insert}  & $[\alpha,\alpha\,set]\To \alpha\,set$
         & 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\\
   \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
         & union over a set\\

 \end{figure}
 
 \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
 operation to take successors.  For details see the file
 \texttt{NatDef.thy}.

 
 \begin{warn}
   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]
 \begin{rail}
 typedef  : 'typedef' ( () | '(' name ')') type '=' set witness;

 \end{description}
 If all context conditions are met (no duplicate type variables in
 `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 \\
 Rep_T &::& (\alpha@1,\dots,\alpha@n)ty \To \tau \\
 Abs_T &::& \tau \To (\alpha@1,\dots,\alpha@n)ty

 \end{array}
 \]
 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}"
 
 typedef (prod)
   ('a, 'b) "*"    (infixr 20)

 
 \section{Datatype declarations}
 \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}
 
 The general \HOL\ \texttt{datatype} definition is of the following form:

   \dots, \beta@l\} \subseteq \{\alpha@1, \dots, \alpha@n\}$,
   
 \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
 use $syn$ in place of $\tau$. Of course this does not work if $\tau$
 mentions the recursive type itself, thus ruling out problematic cases
 like $\mathtt{datatype}~ t ~=~ C \, (t \To t)$, but also unproblematic
 ones like $\mathtt{datatype}~ t ~=~ C \, (t~list)$.
 
 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}
 {\begin{array}{lcl}
 \Forall x@1\dots x@{k@1}.

 \]
 where $\{r@{j1},\dots,r@{jl@j}\} = \{i \in \{1,\dots k@j\} ~\mid~ \tau@{ji}
 = (\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 \\
                            \vdots \\
                            \mid & C@m~x@{m1}~\dots~x@{mk@m} & \To & e@m

 \subsection{Examples}
 
 \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}
 MyList = HOL +
   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}
 {\out ! x. Cons x xs ~= xs}
 {\out  1. ! x. Cons x xs ~= xs}

 \begin{ttbox}
 by (Asm_simp_tac 1);
 {\out Level 3}
 {\out ! x. Cons x xs ~= xs}
 {\out No subgoals!}
-\end{ttbox}
-Because both subgoals were proved by almost the same tactic we could have
-done that in one step using
+\ttbreak
+qed_spec_mp "not_Cons_self";
+{\out val not_Cons_self = "Cons x xs ~= xs";}
+\end{ttbox}
+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}
 
 

 \subsubsection{A datatype for weekdays}
 
 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}.
-\begin{ttbox}
-goal Days.thy "Mo ~= Tu";
+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 "Mon ~= Tue";
 by (Simp_tac 1);
 \end{ttbox}
 You need not derive such inequalities explicitly: the simplifier will dispose
 of them automatically.
 

   primitive recursion}. In principle it would be possible to define
 primitive recursive functions by asserting their reduction rules as
 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"
 end
 \end{ttbox}

 
 \HOL\ provides a save mechanism to define primitive recursive
 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"
 end
 \end{ttbox}

 intermixed with other declarations.
 
 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)"
 end
 \end{ttbox}