New version of type sections and many small changes.
authornipkow
Sat Dec 23 12:50:53 1995 +0100 (1995-12-23)
changeset 1422bc628f4ef0cb
parent 1421 1471e85624a7
child 1423 5726a8243d3f
New version of type sections and many small changes.
doc-src/Logics/HOL.tex
     1.1 --- a/doc-src/Logics/HOL.tex	Fri Dec 22 13:38:57 1995 +0100
     1.2 +++ b/doc-src/Logics/HOL.tex	Sat Dec 23 12:50:53 1995 +0100
     1.3 @@ -38,8 +38,7 @@
     1.4  
     1.5  
     1.6  \begin{figure} 
     1.7 -\begin{center}
     1.8 -\begin{tabular}{rrr} 
     1.9 +\begin{constants}
    1.10    \it name      &\it meta-type  & \it description \\ 
    1.11    \cdx{Trueprop}& $bool\To prop$                & coercion to $prop$\\
    1.12    \cdx{not}     & $bool\To bool$                & negation ($\neg$) \\
    1.13 @@ -48,15 +47,13 @@
    1.14    \cdx{If}      & $[bool,\alpha,\alpha]\To\alpha::term$ & conditional \\
    1.15    \cdx{Inv}     & $(\alpha\To\beta)\To(\beta\To\alpha)$ & function inversion\\
    1.16    \cdx{Let}     & $[\alpha,\alpha\To\beta]\To\beta$ & let binder
    1.17 -\end{tabular}
    1.18 -\end{center}
    1.19 +\end{constants}
    1.20  \subcaption{Constants}
    1.21  
    1.22 -\begin{center}
    1.23 +\begin{constants}
    1.24  \index{"@@{\tt\at} symbol}
    1.25  \index{*"! symbol}\index{*"? symbol}
    1.26  \index{*"?"! symbol}\index{*"E"X"! symbol}
    1.27 -\begin{tabular}{llrrr} 
    1.28    \it symbol &\it name     &\it meta-type & \it description \\
    1.29    \tt\at & \cdx{Eps}  & $(\alpha\To bool)\To\alpha::term$ & 
    1.30          Hilbert description ($\epsilon$) \\
    1.31 @@ -66,16 +63,14 @@
    1.32          existential quantifier ($\exists$) \\
    1.33    {\tt?!} or {\tt EX!}  & \cdx{Ex1}  & $(\alpha::term\To bool)\To bool$ & 
    1.34          unique existence ($\exists!$)
    1.35 -\end{tabular}
    1.36 -\end{center}
    1.37 +\end{constants}
    1.38  \subcaption{Binders} 
    1.39  
    1.40 -\begin{center}
    1.41 +\begin{constants}
    1.42  \index{*"= symbol}
    1.43  \index{&@{\tt\&} symbol}
    1.44  \index{*"| symbol}
    1.45  \index{*"-"-"> symbol}
    1.46 -\begin{tabular}{rrrr} 
    1.47    \it symbol    & \it meta-type & \it priority & \it description \\ 
    1.48    \sdx{o}       & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & 
    1.49          Left 55 & composition ($\circ$) \\
    1.50 @@ -86,8 +81,7 @@
    1.51    \tt \&        & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\
    1.52    \tt |         & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\
    1.53    \tt -->       & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$)
    1.54 -\end{tabular}
    1.55 -\end{center}
    1.56 +\end{constants}
    1.57  \subcaption{Infixes}
    1.58  \caption{Syntax of {\tt HOL}} \label{hol-constants}
    1.59  \end{figure}
    1.60 @@ -161,25 +155,8 @@
    1.61  belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification
    1.62  over functions.
    1.63  
    1.64 -Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
    1.65 -unsound.  I have commented on this elsewhere~\cite[\S7]{paulson-COLOG}.
    1.66 -
    1.67 -\index{type definitions}
    1.68 -Gordon's {\sc hol} system supports {\bf type definitions}.  A type is
    1.69 -defined by exhibiting an existing type~$\sigma$, a predicate~$P::\sigma\To
    1.70 -bool$, and a theorem of the form $\exists x::\sigma.P~x$.  Thus~$P$
    1.71 -specifies a non-empty subset of~$\sigma$, and the new type denotes this
    1.72 -subset.  New function constants are generated to establish an isomorphism
    1.73 -between the new type and the subset.  If type~$\sigma$ involves type
    1.74 -variables $\alpha@1$, \ldots, $\alpha@n$, then the type definition creates
    1.75 -a type constructor $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular
    1.76 -type.  Melham~\cite{melham89} discusses type definitions at length, with
    1.77 -examples. 
    1.78 -
    1.79 -Isabelle does not support type definitions at present.  Instead, they are
    1.80 -mimicked by explicit definitions of isomorphism functions.  The definitions
    1.81 -should be supported by theorems of the form $\exists x::\sigma.P~x$, but
    1.82 -Isabelle cannot enforce this.
    1.83 +HOL offers various methods for introducing new types. For details
    1.84 +see~\S\ref{sec:HOL:Types} and~\S\ref{sec:HOL:datatype}.
    1.85  
    1.86  
    1.87  \subsection{Binders}
    1.88 @@ -220,13 +197,15 @@
    1.89  
    1.90  \HOL\ also defines the basic syntax
    1.91  \[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\] 
    1.92 -as a uniform means of expressing {\tt case} constructs.  Therefore {\tt
    1.93 -  case} and \sdx{of} are reserved words.  However, so far this is mere
    1.94 -syntax and has no logical meaning.  By declaring translations, you can
    1.95 -cause instances of the {\tt case} construct to denote applications of
    1.96 -particular case operators.  The patterns supplied for $c@1$,~\ldots,~$c@n$
    1.97 -distinguish among the different case operators.  For an example, see the
    1.98 -case construct for lists on page~\pageref{hol-list} below.
    1.99 +as a uniform means of expressing {\tt case} constructs.  Therefore {\tt case}
   1.100 +and \sdx{of} are reserved words.  Initially, this is mere syntax and has no
   1.101 +logical meaning.  By declaring translations, you can cause instances of the
   1.102 +{\tt case} construct to denote applications of particular case operators.
   1.103 +This is what happens automatically for each {\tt datatype} declaration. For
   1.104 +example \verb$datatype nat = Z | S nat$ declares a translation between
   1.105 +\verb$case x of Z => a | S n => b$ and \verb$nat_case a (%n.b) x$, where
   1.106 +\verb$nat_case$ is some appropriate function.
   1.107 +
   1.108  
   1.109  \begin{figure}
   1.110  \begin{ttbox}\makeatother
   1.111 @@ -405,7 +384,7 @@
   1.112  
   1.113  \begin{figure} 
   1.114  \begin{center}
   1.115 -\begin{tabular}{rrr} 
   1.116 +\begin{tabular}{rrr}
   1.117    \it name      &\it meta-type  & \it description \\ 
   1.118  \index{{}@\verb'{}' symbol}
   1.119    \verb|{}|     & $\alpha\,set$         & the empty set \\
   1.120 @@ -543,7 +522,7 @@
   1.121  do in~{\ZF}.  In \HOL\ the intersection of the empty set is well-defined,
   1.122  denoting the universal set for the given type.
   1.123  
   1.124 -
   1.125 +% FIXME: define set via typedef
   1.126  \subsection{Syntax of set theory}\index{*set type}
   1.127  \HOL's set theory is called \thydx{Set}.  The type $\alpha\,set$ is
   1.128  essentially the same as $\alpha\To bool$.  The new type is defined for
   1.129 @@ -604,6 +583,7 @@
   1.130  respectively.
   1.131  
   1.132  
   1.133 +% FIXME: remove the two laws connecting mem and Collect
   1.134  \begin{figure} \underscoreon
   1.135  \begin{ttbox}
   1.136  \tdx{mem_Collect_eq}    (a : \{x.P x\}) = P a
   1.137 @@ -845,87 +825,25 @@
   1.138  classical reasoner; see file {\tt HOL/equalities.ML}.
   1.139  
   1.140  
   1.141 -\begin{figure}
   1.142 -\begin{constants}
   1.143 -  \it symbol    & \it meta-type &           & \it description \\ 
   1.144 -  \cdx{Pair}    & $[\alpha,\beta]\To \alpha\times\beta$
   1.145 -        & & ordered pairs $(a,b)$ \\
   1.146 -  \cdx{fst}     & $\alpha\times\beta \To \alpha$        & & first projection\\
   1.147 -  \cdx{snd}     & $\alpha\times\beta \To \beta$         & & second projection\\
   1.148 -  \cdx{split}   & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$ 
   1.149 -        & & generalized projection\\
   1.150 -  \cdx{Sigma}  & 
   1.151 -        $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
   1.152 -        & general sum of sets
   1.153 -\end{constants}
   1.154 -\begin{ttbox}\makeatletter
   1.155 -\tdx{fst_def}      fst p     == @a. ? b. p = (a,b)
   1.156 -\tdx{snd_def}      snd p     == @b. ? a. p = (a,b)
   1.157 -\tdx{split_def}    split c p == c (fst p) (snd p)
   1.158 -\tdx{Sigma_def}    Sigma A B == UN x:A. UN y:B x. \{(x,y)\}
   1.159 -
   1.160 -
   1.161 -\tdx{Pair_inject}  [| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R
   1.162 -\tdx{fst_conv}     fst (a,b) = a
   1.163 -\tdx{snd_conv}     snd (a,b) = b
   1.164 -\tdx{split}        split c (a,b) = c a b
   1.165 -
   1.166 -\tdx{surjective_pairing}  p = (fst p,snd p)
   1.167 -
   1.168 -\tdx{SigmaI}       [| a:A;  b:B a |] ==> (a,b) : Sigma A B
   1.169 -
   1.170 -\tdx{SigmaE}       [| c: Sigma A B;  
   1.171 -                !!x y.[| x:A; y:B x; c=(x,y) |] ==> P |] ==> P
   1.172 -\end{ttbox}
   1.173 -\caption{Type $\alpha\times\beta$}\label{hol-prod}
   1.174 -\end{figure} 
   1.175 -
   1.176 -
   1.177 -\begin{figure}
   1.178 -\begin{constants}
   1.179 -  \it symbol    & \it meta-type &           & \it description \\ 
   1.180 -  \cdx{Inl}     & $\alpha \To \alpha+\beta$    & & first injection\\
   1.181 -  \cdx{Inr}     & $\beta \To \alpha+\beta$     & & second injection\\
   1.182 -  \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$
   1.183 -        & & conditional
   1.184 -\end{constants}
   1.185 -\begin{ttbox}\makeatletter
   1.186 -\tdx{sum_case_def}   sum_case == (\%f g p. @z. (!x. p=Inl x --> z=f x) &
   1.187 -                                        (!y. p=Inr y --> z=g y))
   1.188 -
   1.189 -\tdx{Inl_not_Inr}    ~ Inl a=Inr b
   1.190 -
   1.191 -\tdx{inj_Inl}        inj Inl
   1.192 -\tdx{inj_Inr}        inj Inr
   1.193 -
   1.194 -\tdx{sumE}           [| !!x::'a. P(Inl x);  !!y::'b. P(Inr y) |] ==> P s
   1.195 -
   1.196 -\tdx{sum_case_Inl}   sum_case f g (Inl x) = f x
   1.197 -\tdx{sum_case_Inr}   sum_case f g (Inr x) = g x
   1.198 -
   1.199 -\tdx{surjective_sum} sum_case (\%x::'a. f(Inl x)) (\%y::'b. f(Inr y)) s = f s
   1.200 -\end{ttbox}
   1.201 -\caption{Type $\alpha+\beta$}\label{hol-sum}
   1.202 -\end{figure}
   1.203 -
   1.204 -
   1.205 -\section{Generic packages and classical reasoning}
   1.206 +\section{Generic packages}
   1.207  \HOL\ instantiates most of Isabelle's generic packages;
   1.208  see {\tt HOL/ROOT.ML} for details.
   1.209 -\begin{itemize}
   1.210 -\item 
   1.211 +
   1.212 +\subsection{Substitution and simplification}
   1.213 +
   1.214  Because it includes a general substitution rule, \HOL\ instantiates the
   1.215 -tactic {\tt hyp_subst_tac}, which substitutes for an equality
   1.216 -throughout a subgoal and its hypotheses.
   1.217 -\item 
   1.218 +tactic {\tt hyp_subst_tac}, which substitutes for an equality throughout a
   1.219 +subgoal and its hypotheses.
   1.220 +
   1.221  It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the
   1.222  simplification set for higher-order logic.  Equality~($=$), which also
   1.223 -expresses logical equivalence, may be used for rewriting.  See the file
   1.224 -{\tt HOL/simpdata.ML} for a complete listing of the simplification
   1.225 -rules.
   1.226 -\item 
   1.227 -It instantiates the classical reasoner, as described below. 
   1.228 -\end{itemize}
   1.229 +expresses logical equivalence, may be used for rewriting.  See the file {\tt
   1.230 +HOL/simpdata.ML} for a complete listing of the simplification rules.
   1.231 +
   1.232 +See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
   1.233 +{Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution
   1.234 +and simplification.
   1.235 +
   1.236  \begin{warn}\index{simplification!of conjunctions}
   1.237    The simplifier is not set up to reduce, for example, \verb$a = b & ...a...$
   1.238    to \verb$a = b & ...b...$: it does not use the left part of a conjunction
   1.239 @@ -934,6 +852,8 @@
   1.240    down rewriting and is therefore not included by default.
   1.241  \end{warn}
   1.242  
   1.243 +\subsection{Classical reasoning}
   1.244 +
   1.245  \HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
   1.246  well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
   1.247  rule; recall Fig.\ts\ref{hol-lemmas2} above.
   1.248 @@ -968,27 +888,145 @@
   1.249  for more discussion of classical proof methods.
   1.250  
   1.251  
   1.252 -\section{Types}
   1.253 -The basic higher-order logic is augmented with a tremendous amount of
   1.254 -material, including support for recursive function and type definitions.  A
   1.255 -detailed discussion appears elsewhere~\cite{paulson-coind}.  The simpler
   1.256 -definitions are the same as those used by the {\sc hol} system, but my
   1.257 -treatment of recursive types differs from Melham's~\cite{melham89}.  The
   1.258 -present section describes product, sum, natural number and list types.
   1.259 +\section{Types}\label{sec:HOL:Types}
   1.260 +This section describes HOL's basic predefined types (\verb$*$, \verb$+$, {\tt
   1.261 +  nat} and {\tt list}) and ways for introducing new types. The most important
   1.262 +type construction, the {\tt datatype}, is treated separately in
   1.263 +\S\ref{sec:HOL:datatype}.
   1.264  
   1.265  \subsection{Product and sum types}\index{*"* type}\index{*"+ type}
   1.266 -Theory \thydx{Prod} defines the product type $\alpha\times\beta$, with
   1.267 -the ordered pair syntax {\tt($a$,$b$)}.  Theory \thydx{Sum} defines the
   1.268 -sum type $\alpha+\beta$.  These use fairly standard constructions; see
   1.269 -Figs.\ts\ref{hol-prod} and~\ref{hol-sum}.  Because Isabelle does not
   1.270 -support abstract type definitions, the isomorphisms between these types and
   1.271 -their representations are made explicitly.
   1.272 +
   1.273 +\begin{figure}
   1.274 +\begin{constants}
   1.275 +  \it symbol    & \it meta-type &           & \it description \\ 
   1.276 +  \cdx{Pair}    & $[\alpha,\beta]\To \alpha\times\beta$
   1.277 +        & & ordered pairs $(a,b)$ \\
   1.278 +  \cdx{fst}     & $\alpha\times\beta \To \alpha$        & & first projection\\
   1.279 +  \cdx{snd}     & $\alpha\times\beta \To \beta$         & & second projection\\
   1.280 +  \cdx{split}   & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$ 
   1.281 +        & & generalized projection\\
   1.282 +  \cdx{Sigma}  & 
   1.283 +        $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
   1.284 +        & general sum of sets
   1.285 +\end{constants}
   1.286 +\begin{ttbox}\makeatletter
   1.287 +%\tdx{fst_def}      fst p     == @a. ? b. p = (a,b)
   1.288 +%\tdx{snd_def}      snd p     == @b. ? a. p = (a,b)
   1.289 +%\tdx{split_def}    split c p == c (fst p) (snd p)
   1.290 +\tdx{Sigma_def}    Sigma A B == UN x:A. UN y:B x. \{(x,y)\}
   1.291 +
   1.292 +\tdx{Pair_inject}  [| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R
   1.293 +\tdx{PairE}        [| !!x y. p = (x,y) ==> Q |] ==> Q
   1.294 +\tdx{Pair_eq}      ((a,b) = (a',b')) = (a=a' & b=b')
   1.295 +
   1.296 +\tdx{fst_conv}     fst (a,b) = a
   1.297 +\tdx{snd_conv}     snd (a,b) = b
   1.298 +\tdx{surjective_pairing}  p = (fst p,snd p)
   1.299 +
   1.300 +\tdx{split}        split c (a,b) = c a b
   1.301 +\tdx{expand_split} R(split c p) = (! x y. p = (x,y) --> R(c x y))
   1.302 +
   1.303 +\tdx{SigmaI}       [| a:A;  b:B a |] ==> (a,b) : Sigma A B
   1.304 +\tdx{SigmaE}       [| c: Sigma A B;  
   1.305 +                !!x y.[| x:A; y:B x; c=(x,y) |] ==> P |] ==> P
   1.306 +\end{ttbox}
   1.307 +\caption{Type $\alpha\times\beta$}\label{hol-prod}
   1.308 +\end{figure} 
   1.309  
   1.310 -Most of the definitions are suppressed, but observe that the projections
   1.311 -and conditionals are defined as descriptions.  Their properties are easily
   1.312 -proved using \tdx{select_equality}.  
   1.313 +Theory \thydx{Prod} (Fig.\ts\ref{hol-prod}) defines the product type
   1.314 +$\alpha\times\beta$, with the ordered pair syntax {\tt($a$,$b$)}. Tuples are
   1.315 +simulated by pairs nested to the right:
   1.316 +\begin{center}
   1.317 +\begin{tabular}{|c|c|}
   1.318 +\hline
   1.319 +external & internal \\
   1.320 +\hline
   1.321 +$\tau@1 * \dots * \tau@n$ & $\tau@1 * (\dots (\tau@{n-1} * \tau@n)\dots)$ \\
   1.322 +\hline
   1.323 +$(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\
   1.324 +\hline
   1.325 +\end{tabular}
   1.326 +\end{center}
   1.327 +In addition, it is possible to use tuples
   1.328 +as patterns in abstractions:
   1.329 +\begin{center}
   1.330 +\begin{tabular}{|c|c|}
   1.331 +\hline
   1.332 +external & internal \\
   1.333 +\hline
   1.334 +{\tt\%($x$,$y$).$t$} & {\tt split(\%$x$ $y$.$t$)} \\
   1.335 +\hline
   1.336 +\end{tabular}
   1.337 +\end{center}
   1.338 +Nested patterns are possible and are translated stepwise:
   1.339 +{\tt\%($x$,$y$,$z$).$t$} $\leadsto$ {\tt\%($x$,($y$,$z$)).$t$} $\leadsto$
   1.340 +{\tt split(\%$x$.\%($y$,$z$).$t$)} $\leadsto$ {\tt split(\%$x$.split(\%$y$
   1.341 +  $z$.$t$))}. The reverse translation is performed upon printing.
   1.342 +\begin{warn}
   1.343 +  The translation between patterns and {\tt split} is performed automatically
   1.344 +  by the parser and printer. This means that the internal and external form
   1.345 +  of a term may differ, which has to be taken into account during the proof
   1.346 +  process. For example the term {\tt (\%(x,y).(y,x))(a,b)} requires the
   1.347 +  theorem {\tt split} to rewrite to {\tt(b,a)}.
   1.348 +\end{warn}
   1.349 +In addition to explicit $\lambda$-abstractions, patterns can be used in any
   1.350 +variable binding construct which is internally described by a
   1.351 +$\lambda$-abstraction. Some important examples are
   1.352 +\begin{description}
   1.353 +\item[Let:] {\tt let {\it pattern} = $t$ in $u$}
   1.354 +\item[Quantifiers:] {\tt !~{\it pattern}:$A$.~$P$}
   1.355 +\item[Choice:] {\underscoreon \tt @~{\it pattern}~.~$P$}
   1.356 +\item[Set operations:] {\tt UN~{\it pattern}:$A$.~$B$}
   1.357 +\item[Sets:] {\tt \{~{\it pattern}~.~$P$~\}}
   1.358 +\end{description}
   1.359 +% FIXME: remove comment in HOL/Prod.thy concerning printing
   1.360 +% FIXME: remove ML code from HOL/Prod.thy
   1.361  
   1.362 -\begin{figure} 
   1.363 +Theory {\tt Prod} also introduces the degenerate product type {\tt unit}
   1.364 +which contains only a single element named {\tt()} with the property
   1.365 +\begin{ttbox}
   1.366 +\tdx{unit_eq}       u = ()
   1.367 +\end{ttbox}
   1.368 +\bigskip
   1.369 +
   1.370 +Theory \thydx{Sum} (Fig.~\ref{hol-sum}) defines the sum type $\alpha+\beta$
   1.371 +which associates to the right and has a lower priority than $*$: $\tau@1 +
   1.372 +\tau@2 + \tau@3*\tau@4$ means $\tau@1 + (\tau@2 + (\tau@3*\tau@4))$.
   1.373 +
   1.374 +The definition of products and sums in terms of existing types is not shown.
   1.375 +The constructions are fairly standard and can be found in the respective {\tt
   1.376 +  thy}-files.
   1.377 +
   1.378 +\begin{figure}
   1.379 +\begin{constants}
   1.380 +  \it symbol    & \it meta-type &           & \it description \\ 
   1.381 +  \cdx{Inl}     & $\alpha \To \alpha+\beta$    & & first injection\\
   1.382 +  \cdx{Inr}     & $\beta \To \alpha+\beta$     & & second injection\\
   1.383 +  \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$
   1.384 +        & & conditional
   1.385 +\end{constants}
   1.386 +\begin{ttbox}\makeatletter
   1.387 +%\tdx{sum_case_def}   sum_case == (\%f g p. @z. (!x. p=Inl x --> z=f x) &
   1.388 +%                                        (!y. p=Inr y --> z=g y))
   1.389 +%
   1.390 +\tdx{Inl_not_Inr}    ~ Inl a=Inr b
   1.391 +
   1.392 +\tdx{inj_Inl}        inj Inl
   1.393 +\tdx{inj_Inr}        inj Inr
   1.394 +
   1.395 +\tdx{sumE}           [| !!x::'a. P(Inl x);  !!y::'b. P(Inr y) |] ==> P s
   1.396 +
   1.397 +\tdx{sum_case_Inl}   sum_case f g (Inl x) = f x
   1.398 +\tdx{sum_case_Inr}   sum_case f g (Inr x) = g x
   1.399 +
   1.400 +\tdx{surjective_sum} sum_case (\%x::'a. f(Inl x)) (\%y::'b. f(Inr y)) s = f s
   1.401 +\tdx{expand_sum_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &
   1.402 +                                     (! y. s = Inr(y) --> R(g(y))))
   1.403 +\end{ttbox}
   1.404 +\caption{Type $\alpha+\beta$}\label{hol-sum}
   1.405 +\end{figure}
   1.406 +
   1.407 +\begin{figure}
   1.408  \index{*"< symbol}
   1.409  \index{*"* symbol}
   1.410  \index{*div symbol}
   1.411 @@ -1003,7 +1041,6 @@
   1.412          & & conditional\\
   1.413    \cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$
   1.414          & & primitive recursor\\
   1.415 -  \cdx{pred_nat} & $(nat\times nat) set$ & & predecessor relation\\
   1.416    \tt *         & $[nat,nat]\To nat$    &  Left 70      & multiplication \\
   1.417    \tt div       & $[nat,nat]\To nat$    &  Left 70      & division\\
   1.418    \tt mod       & $[nat,nat]\To nat$    &  Left 70      & modulus\\
   1.419 @@ -1013,46 +1050,38 @@
   1.420  \subcaption{Constants and infixes}
   1.421  
   1.422  \begin{ttbox}\makeatother
   1.423 -\tdx{nat_case_def}  nat_case == (\%a f n. @z. (n=0 --> z=a) & 
   1.424 -                                       (!x. n=Suc x --> z=f x))
   1.425 -\tdx{pred_nat_def}  pred_nat == \{p. ? n. p = (n, Suc n)\} 
   1.426 -\tdx{less_def}      m<n      == (m,n):pred_nat^+
   1.427 -\tdx{nat_rec_def}   nat_rec n c d == 
   1.428 -               wfrec pred_nat n (nat_case (\%g.c) (\%m g. d m (g m)))
   1.429 -
   1.430 -\tdx{add_def}   m+n     == nat_rec m n (\%u v. Suc v)
   1.431 -\tdx{diff_def}  m-n     == nat_rec n m (\%u v. nat_rec v 0 (\%x y.x))
   1.432 -\tdx{mult_def}  m*n     == nat_rec m 0 (\%u v. n + v)
   1.433 -\tdx{mod_def}   m mod n == wfrec (trancl pred_nat)
   1.434 -                        m (\%j f. if j<n then j else f j-n))
   1.435 -\tdx{quo_def}   m div n == wfrec (trancl pred_nat), 
   1.436 -                        m (\%j f. if j<n then 0 else Suc(f j-n))
   1.437 -\subcaption{Definitions}
   1.438 -\end{ttbox}
   1.439 -\caption{Defining {\tt nat}, the type of natural numbers} \label{hol-nat1}
   1.440 -\end{figure}
   1.441 -
   1.442 -
   1.443 -\begin{figure} \underscoreon
   1.444 -\begin{ttbox}
   1.445  \tdx{nat_induct}     [| P 0; !!k. [| P k |] ==> P(Suc k) |]  ==> P n
   1.446  
   1.447  \tdx{Suc_not_Zero}   Suc m ~= 0
   1.448  \tdx{inj_Suc}        inj Suc
   1.449  \tdx{n_not_Suc_n}    n~=Suc n
   1.450  \subcaption{Basic properties}
   1.451 +\end{ttbox}
   1.452 +\caption{Defining {\tt nat}, the type of natural numbers} \label{hol-nat1}
   1.453 +\end{figure}
   1.454  
   1.455 -\tdx{pred_natI}      (n, Suc n) : pred_nat
   1.456 -\tdx{pred_natE}
   1.457 -    [| p : pred_nat;  !!x n. [| p = (n, Suc n) |] ==> R |] ==> R
   1.458  
   1.459 +\begin{figure}
   1.460 +\begin{ttbox}\makeatother
   1.461  \tdx{nat_case_0}     nat_case a f 0 = a
   1.462  \tdx{nat_case_Suc}   nat_case a f (Suc k) = f k
   1.463  
   1.464 -\tdx{wf_pred_nat}    wf pred_nat
   1.465  \tdx{nat_rec_0}      nat_rec 0 c h = c
   1.466  \tdx{nat_rec_Suc}    nat_rec (Suc n) c h = h n (nat_rec n c h)
   1.467 -\subcaption{Case analysis and primitive recursion}
   1.468 +
   1.469 +\tdx{add_0}        0+n           = n
   1.470 +\tdx{add_Suc}      (Suc m)+n     = Suc(m+n)
   1.471 +\tdx{diff_0}       m-0           = m
   1.472 +\tdx{diff_0_eq_0}  0-n           = n
   1.473 +\tdx{diff_Suc_Suc} Suc(m)-Suc(n) = m-n
   1.474 +\tdx{mult_def}     0*n           = 0
   1.475 +\tdx{mult_Suc}     Suc(m)*n      = n + m*n
   1.476 +
   1.477 +\tdx{mod_less}     m<n ==> m mod n = m
   1.478 +\tdx{mod_geq}      [| 0<n;  ~m<n |] ==> m mod n = (m-n) mod n
   1.479 +\tdx{div_less}     m<n ==> m div n = 0
   1.480 +\tdx{div_geq}      [| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)
   1.481 +\subcaption{Recursion equations}
   1.482  
   1.483  \tdx{less_trans}     [| i<j;  j<k |] ==> i<k
   1.484  \tdx{lessI}          n < Suc n
   1.485 @@ -1071,31 +1100,27 @@
   1.486  \caption{Derived rules for {\tt nat}} \label{hol-nat2}
   1.487  \end{figure}
   1.488  
   1.489 +\subsection{The type of natural numbers, {\tt nat}}
   1.490 +%FIXME: introduce separate type proto_nat
   1.491  
   1.492 -\subsection{The type of natural numbers, {\tt nat}}
   1.493  The theory \thydx{Nat} defines the natural numbers in a roundabout but
   1.494  traditional way.  The axiom of infinity postulates an type~\tydx{ind} of
   1.495  individuals, which is non-empty and closed under an injective operation.
   1.496  The natural numbers are inductively generated by choosing an arbitrary
   1.497  individual for~0 and using the injective operation to take successors.  As
   1.498  usual, the isomorphisms between~\tydx{nat} and its representation are made
   1.499 -explicitly.
   1.500 +explicitly. For details see the file {\tt Nat.thy}.
   1.501  
   1.502 -The definition makes use of a least fixed point operator \cdx{lfp},
   1.503 -defined using the Knaster-Tarski theorem.  This is used to define the
   1.504 -operator \cdx{trancl}, for taking the transitive closure of a relation.
   1.505 -Primitive recursion makes use of \cdx{wfrec}, an operator for recursion
   1.506 -along arbitrary well-founded relations.  The corresponding theories are
   1.507 -called {\tt Lfp}, {\tt Trancl} and {\tt WF}\@.  Elsewhere I have described
   1.508 -similar constructions in the context of set theory~\cite{paulson-set-II}.
   1.509 +%The definition makes use of a least fixed point operator \cdx{lfp},
   1.510 +%defined using the Knaster-Tarski theorem.  This is used to define the
   1.511 +%operator \cdx{trancl}, for taking the transitive closure of a relation.
   1.512 +%Primitive recursion makes use of \cdx{wfrec}, an operator for recursion
   1.513 +%along arbitrary well-founded relations.  The corresponding theories are
   1.514 +%called {\tt Lfp}, {\tt Trancl} and {\tt WF}\@.  Elsewhere I have described
   1.515 +%similar constructions in the context of set theory~\cite{paulson-set-II}.
   1.516  
   1.517  Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which
   1.518 -overloads $<$ and $\leq$ on the natural numbers.  As of this writing,
   1.519 -Isabelle provides no means of verifying that such overloading is sensible;
   1.520 -there is no means of specifying the operators' properties and verifying
   1.521 -that instances of the operators satisfy those properties.  To be safe, the
   1.522 -\HOL\ theory includes no polymorphic axioms asserting general properties of
   1.523 -$<$ and~$\leq$.
   1.524 +overloads $<$ and $\leq$ on the natural numbers.
   1.525  
   1.526  Theory \thydx{Arith} develops arithmetic on the natural numbers.  It
   1.527  defines addition, multiplication, subtraction, division, and remainder.
   1.528 @@ -1106,23 +1131,25 @@
   1.529  well-founded rather than primitive recursion.  See Figs.\ts\ref{hol-nat1}
   1.530  and~\ref{hol-nat2}.
   1.531  
   1.532 -The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
   1.533 -Recursion along this relation resembles primitive recursion, but is
   1.534 -stronger because we are in higher-order logic; using primitive recursion to
   1.535 -define a higher-order function, we can easily Ackermann's function, which
   1.536 -is not primitive recursive \cite[page~104]{thompson91}.
   1.537 -The transitive closure of \cdx{pred_nat} is~$<$.  Many functions on the
   1.538 -natural numbers are most easily expressed using recursion along~$<$.
   1.539 +%The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
   1.540 +%Recursion along this relation resembles primitive recursion, but is
   1.541 +%stronger because we are in higher-order logic; using primitive recursion to
   1.542 +%define a higher-order function, we can easily Ackermann's function, which
   1.543 +%is not primitive recursive \cite[page~104]{thompson91}.
   1.544 +%The transitive closure of \cdx{pred_nat} is~$<$.  Many functions on the
   1.545 +%natural numbers are most easily expressed using recursion along~$<$.
   1.546  
   1.547  The tactic {\tt\ttindex{nat_ind_tac} "$n$" $i$} performs induction over the
   1.548  variable~$n$ in subgoal~$i$.
   1.549  
   1.550 +%FIXME add nth
   1.551  \begin{figure}
   1.552 +\index{#@{\tt[]} symbol}
   1.553  \index{#@{\tt\#} symbol}
   1.554  \index{"@@{\tt\at} symbol}
   1.555  \begin{constants}
   1.556    \it symbol & \it meta-type & \it priority & \it description \\
   1.557 -  \cdx{Nil}     & $\alpha list$ & & empty list\\
   1.558 +  \tt[]    & $\alpha list$ & & empty list\\
   1.559    \tt \#   & $[\alpha,\alpha list]\To \alpha list$ & Right 65 & 
   1.560          list constructor \\
   1.561    \cdx{null}    & $\alpha list \To bool$ & & emptiness test\\
   1.562 @@ -1130,23 +1157,25 @@
   1.563    \cdx{tl}      & $\alpha list \To \alpha list$ & & tail \\
   1.564    \cdx{ttl}     & $\alpha list \To \alpha list$ & & total tail \\
   1.565    \tt\at  & $[\alpha list,\alpha list]\To \alpha list$ & Left 65 & append \\
   1.566 -  \sdx{mem}  & $[\alpha,\alpha list]\To bool$    &  Left 55   & membership\\
   1.567    \cdx{map}     & $(\alpha\To\beta) \To (\alpha list \To \beta list)$
   1.568          & & mapping functional\\
   1.569    \cdx{filter}  & $(\alpha \To bool) \To (\alpha list \To \alpha list)$
   1.570          & & filter functional\\
   1.571    \cdx{list_all}& $(\alpha \To bool) \To (\alpha list \To bool)$
   1.572          & & forall functional\\
   1.573 -  \cdx{list_rec}        & $[\alpha list, \beta, [\alpha ,\alpha list,
   1.574 -\beta]\To\beta] \To \beta$
   1.575 -        & & list recursor
   1.576 +  \sdx{mem}  & $[\alpha,\alpha list]\To bool$    &  Left 55   & membership\\
   1.577 +  \cdx{length}  & $\alpha list \To nat$ & & length \\
   1.578 +%  \cdx{nth}  & $nat \To \alpha list \To \alpha$ & & indexing \\
   1.579 +  \cdx{foldl}   & $(\beta\To\alpha\To\beta) \To \beta \To \alpha list \To \beta$ &
   1.580 +  & iteration \\
   1.581 +  \cdx{flat}   & $(\alpha list) list\To \alpha list$ & & flattening \\
   1.582 +  \cdx{rev}     & $\alpha list \To \alpha list$ & & reverse \\
   1.583  \end{constants}
   1.584  \subcaption{Constants and infixes}
   1.585  
   1.586  \begin{center} \tt\frenchspacing
   1.587  \begin{tabular}{rrr} 
   1.588    \it external        & \it internal  & \it description \\{}
   1.589 -  \sdx{[]}            & Nil           & \rm empty list \\{}
   1.590    [$x@1$, $\dots$, $x@n$]  &  $x@1$ \# $\cdots$ \# $x@n$ \# [] &
   1.591          \rm finite list \\{}
   1.592    [$x$:$l$. $P$]  & filter ($\lambda x{.}P$) $l$ & 
   1.593 @@ -1154,28 +1183,12 @@
   1.594  \end{tabular}
   1.595  \end{center}
   1.596  \subcaption{Translations}
   1.597 -
   1.598 -\begin{ttbox}
   1.599 -\tdx{list_induct}    [| P [];  !!x xs. [| P xs |] ==> P x#xs) |]  ==> P l
   1.600 -
   1.601 -\tdx{Cons_not_Nil}   (x # xs) ~= []
   1.602 -\tdx{Cons_Cons_eq}   ((x # xs) = (y # ys)) = (x=y & xs=ys)
   1.603 -\subcaption{Induction and freeness}
   1.604 -\end{ttbox}
   1.605  \caption{The theory \thydx{List}} \label{hol-list}
   1.606  \end{figure}
   1.607  
   1.608 +
   1.609  \begin{figure}
   1.610  \begin{ttbox}\makeatother
   1.611 -\tdx{list_rec_Nil}    list_rec [] c h = c  
   1.612 -\tdx{list_rec_Cons}   list_rec (a#l) c h = h a l (list_rec l c h)
   1.613 -
   1.614 -\tdx{list_case_Nil}   list_case c h [] = c 
   1.615 -\tdx{list_case_Cons}  list_case c h (x#xs) = h x xs
   1.616 -
   1.617 -\tdx{map_Nil}         map f [] = []
   1.618 -\tdx{map_Cons}        map f (x#xs) = f x # map f xs
   1.619 -
   1.620  \tdx{null_Nil}        null [] = True
   1.621  \tdx{null_Cons}       null (x#xs) = False
   1.622  
   1.623 @@ -1186,50 +1199,162 @@
   1.624  \tdx{ttl_Cons}        ttl (x#xs) = xs
   1.625  
   1.626  \tdx{append_Nil}      [] @ ys = ys
   1.627 -\tdx{append_Cons}     (x#xs) \at ys = x # xs \at ys
   1.628 +\tdx{append_Cons}     (x#xs) @ ys = x # xs @ ys
   1.629  
   1.630 -\tdx{mem_Nil}         x mem [] = False
   1.631 -\tdx{mem_Cons}        x mem (y#ys) = (if y=x then True else x mem ys)
   1.632 +\tdx{map_Nil}         map f [] = []
   1.633 +\tdx{map_Cons}        map f (x#xs) = f x # map f xs
   1.634  
   1.635  \tdx{filter_Nil}      filter P [] = []
   1.636  \tdx{filter_Cons}     filter P (x#xs) = (if P x then x#filter P xs else filter P xs)
   1.637  
   1.638  \tdx{list_all_Nil}    list_all P [] = True
   1.639  \tdx{list_all_Cons}   list_all P (x#xs) = (P x & list_all P xs)
   1.640 +
   1.641 +\tdx{mem_Nil}         x mem [] = False
   1.642 +\tdx{mem_Cons}        x mem (y#ys) = (if y=x then True else x mem ys)
   1.643 +
   1.644 +\tdx{length_Nil}      length([]) = 0
   1.645 +\tdx{length_Cons}     length(x#xs) = Suc(length(xs))
   1.646 +
   1.647 +\tdx{foldl_Nil}       foldl f a [] = a
   1.648 +\tdx{foldl_Cons}      foldl f a (x#xs) = foldl f (f a x) xs
   1.649 +
   1.650 +\tdx{flat_Nil}        flat([]) = []
   1.651 +\tdx{flat_Cons}       flat(x#xs) = x @ flat(xs)
   1.652 +
   1.653 +\tdx{rev_Nil}         rev([]) = []
   1.654 +\tdx{rev_Cons}        rev(x#xs) = rev(xs) @ [x]
   1.655  \end{ttbox}
   1.656 -\caption{Rewrite rules for lists} \label{hol-list-simps}
   1.657 +\caption{Rewrite rules for lists} \label{fig:HOL:list-simps}
   1.658  \end{figure}
   1.659  
   1.660  
   1.661  \subsection{The type constructor for lists, {\tt list}}
   1.662  \index{*list type}
   1.663  
   1.664 -\HOL's definition of lists is an example of an experimental method for
   1.665 -handling recursive data types.  Figure~\ref{hol-list} presents the theory
   1.666 -\thydx{List}: the basic list operations with their types and properties.
   1.667 +Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list
   1.668 +operations with their types and syntax. The type constructor {\tt list} is
   1.669 +defined as a {\tt datatype} with the constructors {\tt[]} and {\tt\#}.  This
   1.670 +yields an induction tactic {\tt list.induct_tac} and a list of freeness
   1.671 +theorems {\tt list.simps}.
   1.672 +A \sdx{case} construct of the form
   1.673 +\begin{center}\tt
   1.674 +case $e$ of [] => $a$  |  x\#xs => b
   1.675 +\end{center}
   1.676 +is defined by translation. For details see~\S\ref{sec:HOL:datatype}.
   1.677  
   1.678 -The \sdx{case} construct is defined by the following translation:
   1.679 -{\dquotes
   1.680 -\begin{eqnarray*}
   1.681 -  \begin{array}{r@{\;}l@{}l}
   1.682 -  "case " e " of" & "[]"    & " => " a\\
   1.683 -              "|" & x"\#"xs & " => " b
   1.684 -  \end{array} 
   1.685 -  & \equiv &
   1.686 -  "list_case"~a~(\lambda x\;xs.b)~e
   1.687 -\end{eqnarray*}}%
   1.688 -The theory includes \cdx{list_rec}, a primitive recursion operator
   1.689 -for lists.  It is derived from well-founded recursion, a general principle
   1.690 -that can express arbitrary total recursive functions.
   1.691 -
   1.692 -The simpset \ttindex{list_ss} contains, along with additional useful lemmas,
   1.693 -the basic rewrite rules that appear in Fig.\ts\ref{hol-list-simps}.
   1.694 -
   1.695 -The tactic {\tt\ttindex{list_ind_tac} "$xs$" $i$} performs induction over the
   1.696 -variable~$xs$ in subgoal~$i$.
   1.697 +{\tt List} provides a basic library of list processing functions defined by
   1.698 +primitive recursion (see~\S\ref{sec:HOL:primrec}). The recursion equations
   1.699 +are shown in Fig.\ts\ref{fig:HOL:list-simps}.
   1.700  
   1.701  
   1.702 +\subsection{Introducing new types}
   1.703 +%FIXME: syntax of typedef: subtype -> typedef; name -> id
   1.704 +%FIXME: typevarlist and infix/mixfix in Ref manual and in sec:datatype
   1.705 +
   1.706 +The \HOL-methodology dictates that all extension to a theory should be
   1.707 +conservative and thus preserve consistency. There are two basic type
   1.708 +extension mechanisms which meet this criterion: {\em type synonyms\/} and
   1.709 +{\em type definitions\/}. The former are inherited from {\tt Pure} and are
   1.710 +described elsewhere.
   1.711 +\begin{warn}
   1.712 +  Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
   1.713 +  unsound~\cite[\S7]{paulson-COLOG}.
   1.714 +\end{warn}
   1.715 +A \bfindex{type definition} identifies the new type with a subset of an
   1.716 +existing type. More precisely, the new type is defined by exhibiting an
   1.717 +existing type~$\tau$, a set~$A::(\tau)set$, and a theorem of the form $x:A$.
   1.718 +Thus~$A$ is a non-empty subset of~$\tau$, and the new type denotes this
   1.719 +subset.  New functions are generated to establish an isomorphism between the
   1.720 +new type and the subset.  If type~$\tau$ involves type variables $\alpha@1$,
   1.721 +\ldots, $\alpha@n$, then the type definition creates a type constructor
   1.722 +$(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular type.
   1.723 +
   1.724 +\begin{figure}[htbp]
   1.725 +\begin{rail}
   1.726 +typedef  : 'typedef' ( () | '(' tname ')') type '=' set witness;
   1.727 +type    : typevarlist name ( () | '(' infix ')' );
   1.728 +tname   : name;
   1.729 +set     : string;
   1.730 +witness : () | '(' id ')';
   1.731 +\end{rail}
   1.732 +\caption{Syntax of type definition}
   1.733 +\label{fig:HOL:typedef}
   1.734 +\end{figure}
   1.735 +
   1.736 +The syntax for type definitions is shown in Fig.~\ref{fig:HOL:typedef}. For
   1.737 +the definition of ``typevarlist'' and ``infix'' see
   1.738 +\iflabelundefined{chap:classical}
   1.739 +{the appendix of the {\em Reference Manual\/}}%
   1.740 +{Appendix~\ref{app:TheorySyntax}}. The remaining nonterminals have the
   1.741 +following meaning:
   1.742 +\begin{description}
   1.743 +\item[\it type]: the new type constructor $(\alpha@1,\dots,\alpha@n)ty$ with
   1.744 +  optional infix annotation.
   1.745 +\item[\it tname]: an alphanumeric name $T$ for the type constructor $ty$, in
   1.746 +  case $ty$ is a symbolic name. Default: $ty$.
   1.747 +\item[\it set]: the representing subset $A$.
   1.748 +\item[\it witness]: name of a theorem of the form $a:A$ proving
   1.749 +  non-emptiness. Can be omitted in case Isabelle manages to prove
   1.750 +  non-emptiness automatically.
   1.751 +\end{description}
   1.752 +If all context conditions are met (no duplicate type variables in
   1.753 +'typevarlist', no extra type variables in 'set', and no free term variables
   1.754 +in 'set'), the following components are added to the theory:
   1.755 +\begin{itemize}
   1.756 +\item a type $ty :: (term,\dots)term$;
   1.757 +\item constants
   1.758 +\begin{eqnarray*}
   1.759 +T &::& (\tau)set \\
   1.760 +Rep_T &::& (\alpha@1,\dots,\alpha@n)ty \To \tau \\
   1.761 +Abs_T &::& \tau \To (\alpha@1,\dots,\alpha@n)ty
   1.762 +\end{eqnarray*}
   1.763 +\item a definition and three axioms
   1.764 +\[
   1.765 +\begin{array}{ll}
   1.766 +T{\tt_def} & T \equiv A \\
   1.767 +{\tt Rep_}T & Rep_T(x) : T \\
   1.768 +{\tt Rep_}T{\tt_inverse} & Abs_T(Rep_T(x)) = x \\
   1.769 +{\tt Abs_}T{\tt_inverse} & y:T \Imp Rep_T(Abs_T(y)) = y
   1.770 +\end{array}
   1.771 +\]
   1.772 +stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$
   1.773 +and its inverse $Abs_T$.
   1.774 +\end{itemize}
   1.775 +Here are two simple examples where emptiness is proved automatically:
   1.776 +\begin{ttbox}
   1.777 +typedef unit = "\{False\}"
   1.778 +
   1.779 +typedef (prod)
   1.780 +  ('a, 'b) "*"    (infixr 20)
   1.781 +      = "\{f . EX (a::'a) (b::'b). f = (\%x y. x = a & y = b)\}"
   1.782 +\end{ttbox}
   1.783 +
   1.784 +Type definitions permit the introduction of abstract data types in a safe
   1.785 +way, namely by providing models based on already existing types. Given some
   1.786 +abstract axiomatic description $P$ of a type, this involves two steps:
   1.787 +\begin{enumerate}
   1.788 +\item Find an appropriate type $\tau$ and subset $A$ which has the desired
   1.789 +  properties $P$, and make the above type definition based on this
   1.790 +  representation.
   1.791 +\item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.
   1.792 +\end{enumerate}
   1.793 +You can now forget about the representation and work solely in terms of the
   1.794 +abstract properties $P$.
   1.795 +
   1.796 +\begin{warn}
   1.797 +If you introduce a new type (constructor) $ty$ axiomatically, i.e.\ by
   1.798 +declaring the type and its operations and by stating the desired axioms, you
   1.799 +should make sure the type has a non-empty model. You must also have a clause
   1.800 +\begin{ttbox}
   1.801 +arities \(ty\): (term,\(\dots\),term)term
   1.802 +\end{ttbox}
   1.803 +in your theory file to tell Isabelle that elements of type $ty$ are in class
   1.804 +{\tt term}, the class of all HOL terms.
   1.805 +\end{warn}
   1.806 +
   1.807  \section{Datatype declarations}
   1.808 +\label{sec:HOL:datatype}
   1.809  \index{*datatype|(}
   1.810  
   1.811  \underscoreon
   1.812 @@ -1469,6 +1594,7 @@
   1.813  because the simplifier will dispose of them automatically.
   1.814  
   1.815  \subsection{Primitive recursive functions}
   1.816 +\label{sec:HOL:primrec}
   1.817  \index{primitive recursion|(}
   1.818  \index{*primrec|(}
   1.819  
   1.820 @@ -1711,7 +1837,7 @@
   1.821  consts Fin :: 'a set => 'a set set
   1.822  inductive "Fin A"
   1.823    intrs
   1.824 -    emptyI  "{} : Fin A"
   1.825 +    emptyI  "\{\} : Fin A"
   1.826      insertI "[| a: A;  b: Fin A |] ==> insert a b : Fin A"
   1.827  \end{ttbox}
   1.828  The resulting theory structure contains a substructure, called~{\tt Fin}.