--- a/doc-src/Logics/HOL.tex Fri Dec 22 13:38:57 1995 +0100
+++ b/doc-src/Logics/HOL.tex Sat Dec 23 12:50:53 1995 +0100
@@ -38,8 +38,7 @@
\begin{figure}
-\begin{center}
-\begin{tabular}{rrr}
+\begin{constants}
\it name &\it meta-type & \it description \\
\cdx{Trueprop}& $bool\To prop$ & coercion to $prop$\\
\cdx{not} & $bool\To bool$ & negation ($\neg$) \\
@@ -48,15 +47,13 @@
\cdx{If} & $[bool,\alpha,\alpha]\To\alpha::term$ & conditional \\
\cdx{Inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & function inversion\\
\cdx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder
-\end{tabular}
-\end{center}
+\end{constants}
\subcaption{Constants}
-\begin{center}
+\begin{constants}
\index{"@@{\tt\at} symbol}
\index{*"! symbol}\index{*"? symbol}
\index{*"?"! symbol}\index{*"E"X"! symbol}
-\begin{tabular}{llrrr}
\it symbol &\it name &\it meta-type & \it description \\
\tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha::term$ &
Hilbert description ($\epsilon$) \\
@@ -66,16 +63,14 @@
existential quantifier ($\exists$) \\
{\tt?!} or {\tt EX!} & \cdx{Ex1} & $(\alpha::term\To bool)\To bool$ &
unique existence ($\exists!$)
-\end{tabular}
-\end{center}
+\end{constants}
\subcaption{Binders}
-\begin{center}
+\begin{constants}
\index{*"= symbol}
\index{&@{\tt\&} symbol}
\index{*"| symbol}
\index{*"-"-"> symbol}
-\begin{tabular}{rrrr}
\it symbol & \it meta-type & \it priority & \it description \\
\sdx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ &
Left 55 & composition ($\circ$) \\
@@ -86,8 +81,7 @@
\tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\
\tt | & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\
\tt --> & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$)
-\end{tabular}
-\end{center}
+\end{constants}
\subcaption{Infixes}
\caption{Syntax of {\tt HOL}} \label{hol-constants}
\end{figure}
@@ -161,25 +155,8 @@
belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification
over functions.
-Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
-unsound. I have commented on this elsewhere~\cite[\S7]{paulson-COLOG}.
-
-\index{type definitions}
-Gordon's {\sc hol} system supports {\bf type definitions}. A type is
-defined by exhibiting an existing type~$\sigma$, a predicate~$P::\sigma\To
-bool$, and a theorem of the form $\exists x::\sigma.P~x$. Thus~$P$
-specifies a non-empty subset of~$\sigma$, and the new type denotes this
-subset. New function constants are generated to establish an isomorphism
-between the new type and the subset. If type~$\sigma$ 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. Melham~\cite{melham89} discusses type definitions at length, with
-examples.
-
-Isabelle does not support type definitions at present. Instead, they are
-mimicked by explicit definitions of isomorphism functions. The definitions
-should be supported by theorems of the form $\exists x::\sigma.P~x$, but
-Isabelle cannot enforce this.
+HOL offers various methods for introducing new types. For details
+see~\S\ref{sec:HOL:Types} and~\S\ref{sec:HOL:datatype}.
\subsection{Binders}
@@ -220,13 +197,15 @@
\HOL\ also defines the basic syntax
\[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"|" \dots "|"~c@n~"=>"~e@n\]
-as a uniform means of expressing {\tt case} constructs. Therefore {\tt
- case} and \sdx{of} are reserved words. However, so far this is mere
-syntax and has no logical meaning. By declaring translations, you can
-cause instances of the {\tt case} construct to denote applications of
-particular case operators. The patterns supplied for $c@1$,~\ldots,~$c@n$
-distinguish among the different case operators. For an example, see the
-case construct for lists on page~\pageref{hol-list} below.
+as a uniform means of expressing {\tt case} constructs. Therefore {\tt case}
+and \sdx{of} are reserved words. Initially, this is mere syntax and has no
+logical meaning. By declaring translations, you can cause instances of the
+{\tt case} construct to denote applications of particular case operators.
+This is what happens automatically for each {\tt datatype} declaration. For
+example \verb$datatype nat = Z | S nat$ declares a translation between
+\verb$case x of Z => a | S n => b$ and \verb$nat_case a (%n.b) x$, where
+\verb$nat_case$ is some appropriate function.
+
\begin{figure}
\begin{ttbox}\makeatother
@@ -405,7 +384,7 @@
\begin{figure}
\begin{center}
-\begin{tabular}{rrr}
+\begin{tabular}{rrr}
\it name &\it meta-type & \it description \\
\index{{}@\verb'{}' symbol}
\verb|{}| & $\alpha\,set$ & the empty set \\
@@ -543,7 +522,7 @@
do in~{\ZF}. In \HOL\ the intersection of the empty set is well-defined,
denoting the universal set for the given type.
-
+% FIXME: define set via typedef
\subsection{Syntax of set theory}\index{*set type}
\HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is
essentially the same as $\alpha\To bool$. The new type is defined for
@@ -604,6 +583,7 @@
respectively.
+% FIXME: remove the two laws connecting mem and Collect
\begin{figure} \underscoreon
\begin{ttbox}
\tdx{mem_Collect_eq} (a : \{x.P x\}) = P a
@@ -845,87 +825,25 @@
classical reasoner; see file {\tt HOL/equalities.ML}.
-\begin{figure}
-\begin{constants}
- \it symbol & \it meta-type & & \it description \\
- \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$
- & & ordered pairs $(a,b)$ \\
- \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\
- \cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\
- \cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$
- & & generalized projection\\
- \cdx{Sigma} &
- $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
- & general sum of sets
-\end{constants}
-\begin{ttbox}\makeatletter
-\tdx{fst_def} fst p == @a. ? b. p = (a,b)
-\tdx{snd_def} snd p == @b. ? a. p = (a,b)
-\tdx{split_def} split c p == c (fst p) (snd p)
-\tdx{Sigma_def} Sigma A B == UN x:A. UN y:B x. \{(x,y)\}
-
-
-\tdx{Pair_inject} [| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R
-\tdx{fst_conv} fst (a,b) = a
-\tdx{snd_conv} snd (a,b) = b
-\tdx{split} split c (a,b) = c a b
-
-\tdx{surjective_pairing} p = (fst p,snd p)
-
-\tdx{SigmaI} [| a:A; b:B a |] ==> (a,b) : Sigma A B
-
-\tdx{SigmaE} [| c: Sigma A B;
- !!x y.[| x:A; y:B x; c=(x,y) |] ==> P |] ==> P
-\end{ttbox}
-\caption{Type $\alpha\times\beta$}\label{hol-prod}
-\end{figure}
-
-
-\begin{figure}
-\begin{constants}
- \it symbol & \it meta-type & & \it description \\
- \cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\
- \cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\
- \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$
- & & conditional
-\end{constants}
-\begin{ttbox}\makeatletter
-\tdx{sum_case_def} sum_case == (\%f g p. @z. (!x. p=Inl x --> z=f x) &
- (!y. p=Inr y --> z=g y))
-
-\tdx{Inl_not_Inr} ~ Inl a=Inr b
-
-\tdx{inj_Inl} inj Inl
-\tdx{inj_Inr} inj Inr
-
-\tdx{sumE} [| !!x::'a. P(Inl x); !!y::'b. P(Inr y) |] ==> P s
-
-\tdx{sum_case_Inl} sum_case f g (Inl x) = f x
-\tdx{sum_case_Inr} sum_case f g (Inr x) = g x
-
-\tdx{surjective_sum} sum_case (\%x::'a. f(Inl x)) (\%y::'b. f(Inr y)) s = f s
-\end{ttbox}
-\caption{Type $\alpha+\beta$}\label{hol-sum}
-\end{figure}
-
-
-\section{Generic packages and classical reasoning}
+\section{Generic packages}
\HOL\ instantiates most of Isabelle's generic packages;
see {\tt HOL/ROOT.ML} for details.
-\begin{itemize}
-\item
+
+\subsection{Substitution and simplification}
+
Because it includes a general substitution rule, \HOL\ instantiates the
-tactic {\tt hyp_subst_tac}, which substitutes for an equality
-throughout a subgoal and its hypotheses.
-\item
+tactic {\tt hyp_subst_tac}, which substitutes for an equality throughout a
+subgoal and its hypotheses.
+
It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the
simplification set for higher-order logic. Equality~($=$), which also
-expresses logical equivalence, may be used for rewriting. See the file
-{\tt HOL/simpdata.ML} for a complete listing of the simplification
-rules.
-\item
-It instantiates the classical reasoner, as described below.
-\end{itemize}
+expresses logical equivalence, may be used for rewriting. See the file {\tt
+HOL/simpdata.ML} for a complete listing of the simplification rules.
+
+See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
+{Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution
+and simplification.
+
\begin{warn}\index{simplification!of conjunctions}
The simplifier is not set up to reduce, for example, \verb$a = b & ...a...$
to \verb$a = b & ...b...$: it does not use the left part of a conjunction
@@ -934,6 +852,8 @@
down rewriting and is therefore not included by default.
\end{warn}
+\subsection{Classical reasoning}
+
\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
rule; recall Fig.\ts\ref{hol-lemmas2} above.
@@ -968,27 +888,145 @@
for more discussion of classical proof methods.
-\section{Types}
-The basic higher-order logic is augmented with a tremendous amount of
-material, including support for recursive function and type definitions. A
-detailed discussion appears elsewhere~\cite{paulson-coind}. The simpler
-definitions are the same as those used by the {\sc hol} system, but my
-treatment of recursive types differs from Melham's~\cite{melham89}. The
-present section describes product, sum, natural number and list types.
+\section{Types}\label{sec:HOL:Types}
+This section describes HOL's basic predefined types (\verb$*$, \verb$+$, {\tt
+ nat} and {\tt list}) and ways for introducing new types. The most important
+type construction, the {\tt datatype}, is treated separately in
+\S\ref{sec:HOL:datatype}.
\subsection{Product and sum types}\index{*"* type}\index{*"+ type}
-Theory \thydx{Prod} defines the product type $\alpha\times\beta$, with
-the ordered pair syntax {\tt($a$,$b$)}. Theory \thydx{Sum} defines the
-sum type $\alpha+\beta$. These use fairly standard constructions; see
-Figs.\ts\ref{hol-prod} and~\ref{hol-sum}. Because Isabelle does not
-support abstract type definitions, the isomorphisms between these types and
-their representations are made explicitly.
+
+\begin{figure}
+\begin{constants}
+ \it symbol & \it meta-type & & \it description \\
+ \cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$
+ & & ordered pairs $(a,b)$ \\
+ \cdx{fst} & $\alpha\times\beta \To \alpha$ & & first projection\\
+ \cdx{snd} & $\alpha\times\beta \To \beta$ & & second projection\\
+ \cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$
+ & & generalized projection\\
+ \cdx{Sigma} &
+ $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
+ & general sum of sets
+\end{constants}
+\begin{ttbox}\makeatletter
+%\tdx{fst_def} fst p == @a. ? b. p = (a,b)
+%\tdx{snd_def} snd p == @b. ? a. p = (a,b)
+%\tdx{split_def} split c p == c (fst p) (snd p)
+\tdx{Sigma_def} Sigma A B == UN x:A. UN y:B x. \{(x,y)\}
+
+\tdx{Pair_inject} [| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R
+\tdx{PairE} [| !!x y. p = (x,y) ==> Q |] ==> Q
+\tdx{Pair_eq} ((a,b) = (a',b')) = (a=a' & b=b')
+
+\tdx{fst_conv} fst (a,b) = a
+\tdx{snd_conv} snd (a,b) = b
+\tdx{surjective_pairing} p = (fst p,snd p)
+
+\tdx{split} split c (a,b) = c a b
+\tdx{expand_split} R(split c p) = (! x y. p = (x,y) --> R(c x y))
+
+\tdx{SigmaI} [| a:A; b:B a |] ==> (a,b) : Sigma A B
+\tdx{SigmaE} [| c: Sigma A B;
+ !!x y.[| x:A; y:B x; c=(x,y) |] ==> P |] ==> P
+\end{ttbox}
+\caption{Type $\alpha\times\beta$}\label{hol-prod}
+\end{figure}
-Most of the definitions are suppressed, but observe that the projections
-and conditionals are defined as descriptions. Their properties are easily
-proved using \tdx{select_equality}.
+Theory \thydx{Prod} (Fig.\ts\ref{hol-prod}) defines the product type
+$\alpha\times\beta$, with the ordered pair syntax {\tt($a$,$b$)}. Tuples are
+simulated by pairs nested to the right:
+\begin{center}
+\begin{tabular}{|c|c|}
+\hline
+external & internal \\
+\hline
+$\tau@1 * \dots * \tau@n$ & $\tau@1 * (\dots (\tau@{n-1} * \tau@n)\dots)$ \\
+\hline
+$(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\
+\hline
+\end{tabular}
+\end{center}
+In addition, it is possible to use tuples
+as patterns in abstractions:
+\begin{center}
+\begin{tabular}{|c|c|}
+\hline
+external & internal \\
+\hline
+{\tt\%($x$,$y$).$t$} & {\tt split(\%$x$ $y$.$t$)} \\
+\hline
+\end{tabular}
+\end{center}
+Nested patterns are possible and are translated stepwise:
+{\tt\%($x$,$y$,$z$).$t$} $\leadsto$ {\tt\%($x$,($y$,$z$)).$t$} $\leadsto$
+{\tt split(\%$x$.\%($y$,$z$).$t$)} $\leadsto$ {\tt split(\%$x$.split(\%$y$
+ $z$.$t$))}. The reverse translation is performed upon printing.
+\begin{warn}
+ The translation between patterns and {\tt split} is performed automatically
+ by the parser and printer. This means that the internal and external form
+ of a term may differ, which has to be taken into account during the proof
+ process. For example the term {\tt (\%(x,y).(y,x))(a,b)} requires the
+ theorem {\tt split} to rewrite to {\tt(b,a)}.
+\end{warn}
+In addition to explicit $\lambda$-abstractions, patterns can be used in any
+variable binding construct which is internally described by a
+$\lambda$-abstraction. Some important examples are
+\begin{description}
+\item[Let:] {\tt let {\it pattern} = $t$ in $u$}
+\item[Quantifiers:] {\tt !~{\it pattern}:$A$.~$P$}
+\item[Choice:] {\underscoreon \tt @~{\it pattern}~.~$P$}
+\item[Set operations:] {\tt UN~{\it pattern}:$A$.~$B$}
+\item[Sets:] {\tt \{~{\it pattern}~.~$P$~\}}
+\end{description}
+% FIXME: remove comment in HOL/Prod.thy concerning printing
+% FIXME: remove ML code from HOL/Prod.thy
-\begin{figure}
+Theory {\tt Prod} also introduces the degenerate product type {\tt unit}
+which contains only a single element named {\tt()} with the property
+\begin{ttbox}
+\tdx{unit_eq} u = ()
+\end{ttbox}
+\bigskip
+
+Theory \thydx{Sum} (Fig.~\ref{hol-sum}) defines the sum type $\alpha+\beta$
+which associates to the right and has a lower priority than $*$: $\tau@1 +
+\tau@2 + \tau@3*\tau@4$ means $\tau@1 + (\tau@2 + (\tau@3*\tau@4))$.
+
+The definition of products and sums in terms of existing types is not shown.
+The constructions are fairly standard and can be found in the respective {\tt
+ thy}-files.
+
+\begin{figure}
+\begin{constants}
+ \it symbol & \it meta-type & & \it description \\
+ \cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\
+ \cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\
+ \cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$
+ & & conditional
+\end{constants}
+\begin{ttbox}\makeatletter
+%\tdx{sum_case_def} sum_case == (\%f g p. @z. (!x. p=Inl x --> z=f x) &
+% (!y. p=Inr y --> z=g y))
+%
+\tdx{Inl_not_Inr} ~ Inl a=Inr b
+
+\tdx{inj_Inl} inj Inl
+\tdx{inj_Inr} inj Inr
+
+\tdx{sumE} [| !!x::'a. P(Inl x); !!y::'b. P(Inr y) |] ==> P s
+
+\tdx{sum_case_Inl} sum_case f g (Inl x) = f x
+\tdx{sum_case_Inr} sum_case f g (Inr x) = g x
+
+\tdx{surjective_sum} sum_case (\%x::'a. f(Inl x)) (\%y::'b. f(Inr y)) s = f s
+\tdx{expand_sum_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &
+ (! y. s = Inr(y) --> R(g(y))))
+\end{ttbox}
+\caption{Type $\alpha+\beta$}\label{hol-sum}
+\end{figure}
+
+\begin{figure}
\index{*"< symbol}
\index{*"* symbol}
\index{*div symbol}
@@ -1003,7 +1041,6 @@
& & conditional\\
\cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$
& & primitive recursor\\
- \cdx{pred_nat} & $(nat\times nat) set$ & & predecessor relation\\
\tt * & $[nat,nat]\To nat$ & Left 70 & multiplication \\
\tt div & $[nat,nat]\To nat$ & Left 70 & division\\
\tt mod & $[nat,nat]\To nat$ & Left 70 & modulus\\
@@ -1013,46 +1050,38 @@
\subcaption{Constants and infixes}
\begin{ttbox}\makeatother
-\tdx{nat_case_def} nat_case == (\%a f n. @z. (n=0 --> z=a) &
- (!x. n=Suc x --> z=f x))
-\tdx{pred_nat_def} pred_nat == \{p. ? n. p = (n, Suc n)\}
-\tdx{less_def} m<n == (m,n):pred_nat^+
-\tdx{nat_rec_def} nat_rec n c d ==
- wfrec pred_nat n (nat_case (\%g.c) (\%m g. d m (g m)))
-
-\tdx{add_def} m+n == nat_rec m n (\%u v. Suc v)
-\tdx{diff_def} m-n == nat_rec n m (\%u v. nat_rec v 0 (\%x y.x))
-\tdx{mult_def} m*n == nat_rec m 0 (\%u v. n + v)
-\tdx{mod_def} m mod n == wfrec (trancl pred_nat)
- m (\%j f. if j<n then j else f j-n))
-\tdx{quo_def} m div n == wfrec (trancl pred_nat),
- m (\%j f. if j<n then 0 else Suc(f j-n))
-\subcaption{Definitions}
-\end{ttbox}
-\caption{Defining {\tt nat}, the type of natural numbers} \label{hol-nat1}
-\end{figure}
-
-
-\begin{figure} \underscoreon
-\begin{ttbox}
\tdx{nat_induct} [| P 0; !!k. [| P k |] ==> P(Suc k) |] ==> P n
\tdx{Suc_not_Zero} Suc m ~= 0
\tdx{inj_Suc} inj Suc
\tdx{n_not_Suc_n} n~=Suc n
\subcaption{Basic properties}
+\end{ttbox}
+\caption{Defining {\tt nat}, the type of natural numbers} \label{hol-nat1}
+\end{figure}
-\tdx{pred_natI} (n, Suc n) : pred_nat
-\tdx{pred_natE}
- [| p : pred_nat; !!x n. [| p = (n, Suc n) |] ==> R |] ==> R
+\begin{figure}
+\begin{ttbox}\makeatother
\tdx{nat_case_0} nat_case a f 0 = a
\tdx{nat_case_Suc} nat_case a f (Suc k) = f k
-\tdx{wf_pred_nat} wf pred_nat
\tdx{nat_rec_0} nat_rec 0 c h = c
\tdx{nat_rec_Suc} nat_rec (Suc n) c h = h n (nat_rec n c h)
-\subcaption{Case analysis and primitive recursion}
+
+\tdx{add_0} 0+n = n
+\tdx{add_Suc} (Suc m)+n = Suc(m+n)
+\tdx{diff_0} m-0 = m
+\tdx{diff_0_eq_0} 0-n = n
+\tdx{diff_Suc_Suc} Suc(m)-Suc(n) = m-n
+\tdx{mult_def} 0*n = 0
+\tdx{mult_Suc} Suc(m)*n = n + m*n
+
+\tdx{mod_less} m<n ==> m mod n = m
+\tdx{mod_geq} [| 0<n; ~m<n |] ==> m mod n = (m-n) mod n
+\tdx{div_less} m<n ==> m div n = 0
+\tdx{div_geq} [| 0<n; ~m<n |] ==> m div n = Suc((m-n) div n)
+\subcaption{Recursion equations}
\tdx{less_trans} [| i<j; j<k |] ==> i<k
\tdx{lessI} n < Suc n
@@ -1071,31 +1100,27 @@
\caption{Derived rules for {\tt nat}} \label{hol-nat2}
\end{figure}
+\subsection{The type of natural numbers, {\tt nat}}
+%FIXME: introduce separate type proto_nat
-\subsection{The type of natural numbers, {\tt nat}}
The theory \thydx{Nat} defines the natural numbers in a roundabout but
traditional way. The axiom of infinity postulates an 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. As
usual, the isomorphisms between~\tydx{nat} and its representation are made
-explicitly.
+explicitly. For details see the file {\tt Nat.thy}.
-The definition makes use of a least fixed point operator \cdx{lfp},
-defined using the Knaster-Tarski theorem. This is used to define the
-operator \cdx{trancl}, for taking the transitive closure of a relation.
-Primitive recursion makes use of \cdx{wfrec}, an operator for recursion
-along arbitrary well-founded relations. The corresponding theories are
-called {\tt Lfp}, {\tt Trancl} and {\tt WF}\@. Elsewhere I have described
-similar constructions in the context of set theory~\cite{paulson-set-II}.
+%The definition makes use of a least fixed point operator \cdx{lfp},
+%defined using the Knaster-Tarski theorem. This is used to define the
+%operator \cdx{trancl}, for taking the transitive closure of a relation.
+%Primitive recursion makes use of \cdx{wfrec}, an operator for recursion
+%along arbitrary well-founded relations. The corresponding theories are
+%called {\tt Lfp}, {\tt Trancl} and {\tt WF}\@. Elsewhere I have described
+%similar constructions in the context of set theory~\cite{paulson-set-II}.
Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which
-overloads $<$ and $\leq$ on the natural numbers. As of this writing,
-Isabelle provides no means of verifying that such overloading is sensible;
-there is no means of specifying the operators' properties and verifying
-that instances of the operators satisfy those properties. To be safe, the
-\HOL\ theory includes no polymorphic axioms asserting general properties of
-$<$ and~$\leq$.
+overloads $<$ and $\leq$ on the natural numbers.
Theory \thydx{Arith} develops arithmetic on the natural numbers. It
defines addition, multiplication, subtraction, division, and remainder.
@@ -1106,23 +1131,25 @@
well-founded rather than primitive recursion. See Figs.\ts\ref{hol-nat1}
and~\ref{hol-nat2}.
-The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
-Recursion along this relation resembles primitive recursion, but is
-stronger because we are in higher-order logic; using primitive recursion to
-define a higher-order function, we can easily Ackermann's function, which
-is not primitive recursive \cite[page~104]{thompson91}.
-The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the
-natural numbers are most easily expressed using recursion along~$<$.
+%The predecessor relation, \cdx{pred_nat}, is shown to be well-founded.
+%Recursion along this relation resembles primitive recursion, but is
+%stronger because we are in higher-order logic; using primitive recursion to
+%define a higher-order function, we can easily Ackermann's function, which
+%is not primitive recursive \cite[page~104]{thompson91}.
+%The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the
+%natural numbers are most easily expressed using recursion along~$<$.
The tactic {\tt\ttindex{nat_ind_tac} "$n$" $i$} performs induction over the
variable~$n$ in subgoal~$i$.
+%FIXME add nth
\begin{figure}
+\index{#@{\tt[]} symbol}
\index{#@{\tt\#} symbol}
\index{"@@{\tt\at} symbol}
\begin{constants}
\it symbol & \it meta-type & \it priority & \it description \\
- \cdx{Nil} & $\alpha list$ & & empty list\\
+ \tt[] & $\alpha list$ & & empty list\\
\tt \# & $[\alpha,\alpha list]\To \alpha list$ & Right 65 &
list constructor \\
\cdx{null} & $\alpha list \To bool$ & & emptiness test\\
@@ -1130,23 +1157,25 @@
\cdx{tl} & $\alpha list \To \alpha list$ & & tail \\
\cdx{ttl} & $\alpha list \To \alpha list$ & & total tail \\
\tt\at & $[\alpha list,\alpha list]\To \alpha list$ & Left 65 & append \\
- \sdx{mem} & $[\alpha,\alpha list]\To bool$ & Left 55 & membership\\
\cdx{map} & $(\alpha\To\beta) \To (\alpha list \To \beta list)$
& & mapping functional\\
\cdx{filter} & $(\alpha \To bool) \To (\alpha list \To \alpha list)$
& & filter functional\\
\cdx{list_all}& $(\alpha \To bool) \To (\alpha list \To bool)$
& & forall functional\\
- \cdx{list_rec} & $[\alpha list, \beta, [\alpha ,\alpha list,
-\beta]\To\beta] \To \beta$
- & & list recursor
+ \sdx{mem} & $[\alpha,\alpha list]\To bool$ & Left 55 & membership\\
+ \cdx{length} & $\alpha list \To nat$ & & length \\
+% \cdx{nth} & $nat \To \alpha list \To \alpha$ & & indexing \\
+ \cdx{foldl} & $(\beta\To\alpha\To\beta) \To \beta \To \alpha list \To \beta$ &
+ & iteration \\
+ \cdx{flat} & $(\alpha list) list\To \alpha list$ & & flattening \\
+ \cdx{rev} & $\alpha list \To \alpha list$ & & reverse \\
\end{constants}
\subcaption{Constants and infixes}
\begin{center} \tt\frenchspacing
\begin{tabular}{rrr}
\it external & \it internal & \it description \\{}
- \sdx{[]} & Nil & \rm empty list \\{}
[$x@1$, $\dots$, $x@n$] & $x@1$ \# $\cdots$ \# $x@n$ \# [] &
\rm finite list \\{}
[$x$:$l$. $P$] & filter ($\lambda x{.}P$) $l$ &
@@ -1154,28 +1183,12 @@
\end{tabular}
\end{center}
\subcaption{Translations}
-
-\begin{ttbox}
-\tdx{list_induct} [| P []; !!x xs. [| P xs |] ==> P x#xs) |] ==> P l
-
-\tdx{Cons_not_Nil} (x # xs) ~= []
-\tdx{Cons_Cons_eq} ((x # xs) = (y # ys)) = (x=y & xs=ys)
-\subcaption{Induction and freeness}
-\end{ttbox}
\caption{The theory \thydx{List}} \label{hol-list}
\end{figure}
+
\begin{figure}
\begin{ttbox}\makeatother
-\tdx{list_rec_Nil} list_rec [] c h = c
-\tdx{list_rec_Cons} list_rec (a#l) c h = h a l (list_rec l c h)
-
-\tdx{list_case_Nil} list_case c h [] = c
-\tdx{list_case_Cons} list_case c h (x#xs) = h x xs
-
-\tdx{map_Nil} map f [] = []
-\tdx{map_Cons} map f (x#xs) = f x # map f xs
-
\tdx{null_Nil} null [] = True
\tdx{null_Cons} null (x#xs) = False
@@ -1186,50 +1199,162 @@
\tdx{ttl_Cons} ttl (x#xs) = xs
\tdx{append_Nil} [] @ ys = ys
-\tdx{append_Cons} (x#xs) \at ys = x # xs \at ys
+\tdx{append_Cons} (x#xs) @ ys = x # xs @ ys
-\tdx{mem_Nil} x mem [] = False
-\tdx{mem_Cons} x mem (y#ys) = (if y=x then True else x mem ys)
+\tdx{map_Nil} map f [] = []
+\tdx{map_Cons} map f (x#xs) = f x # map f xs
\tdx{filter_Nil} filter P [] = []
\tdx{filter_Cons} filter P (x#xs) = (if P x then x#filter P xs else filter P xs)
\tdx{list_all_Nil} list_all P [] = True
\tdx{list_all_Cons} list_all P (x#xs) = (P x & list_all P xs)
+
+\tdx{mem_Nil} x mem [] = False
+\tdx{mem_Cons} x mem (y#ys) = (if y=x then True else x mem ys)
+
+\tdx{length_Nil} length([]) = 0
+\tdx{length_Cons} length(x#xs) = Suc(length(xs))
+
+\tdx{foldl_Nil} foldl f a [] = a
+\tdx{foldl_Cons} foldl f a (x#xs) = foldl f (f a x) xs
+
+\tdx{flat_Nil} flat([]) = []
+\tdx{flat_Cons} flat(x#xs) = x @ flat(xs)
+
+\tdx{rev_Nil} rev([]) = []
+\tdx{rev_Cons} rev(x#xs) = rev(xs) @ [x]
\end{ttbox}
-\caption{Rewrite rules for lists} \label{hol-list-simps}
+\caption{Rewrite rules for lists} \label{fig:HOL:list-simps}
\end{figure}
\subsection{The type constructor for lists, {\tt list}}
\index{*list type}
-\HOL's definition of lists is an example of an experimental method for
-handling recursive data types. Figure~\ref{hol-list} presents the theory
-\thydx{List}: the basic list operations with their types and properties.
+Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list
+operations with their types and syntax. The type constructor {\tt list} is
+defined as a {\tt datatype} with the constructors {\tt[]} and {\tt\#}. This
+yields an induction tactic {\tt list.induct_tac} and a list of freeness
+theorems {\tt list.simps}.
+A \sdx{case} construct of the form
+\begin{center}\tt
+case $e$ of [] => $a$ | x\#xs => b
+\end{center}
+is defined by translation. For details see~\S\ref{sec:HOL:datatype}.
-The \sdx{case} construct is defined by the following translation:
-{\dquotes
-\begin{eqnarray*}
- \begin{array}{r@{\;}l@{}l}
- "case " e " of" & "[]" & " => " a\\
- "|" & x"\#"xs & " => " b
- \end{array}
- & \equiv &
- "list_case"~a~(\lambda x\;xs.b)~e
-\end{eqnarray*}}%
-The theory includes \cdx{list_rec}, a primitive recursion operator
-for lists. It is derived from well-founded recursion, a general principle
-that can express arbitrary total recursive functions.
-
-The simpset \ttindex{list_ss} contains, along with additional useful lemmas,
-the basic rewrite rules that appear in Fig.\ts\ref{hol-list-simps}.
-
-The tactic {\tt\ttindex{list_ind_tac} "$xs$" $i$} performs induction over the
-variable~$xs$ in subgoal~$i$.
+{\tt List} provides a basic library of list processing functions defined by
+primitive recursion (see~\S\ref{sec:HOL:primrec}). The recursion equations
+are shown in Fig.\ts\ref{fig:HOL:list-simps}.
+\subsection{Introducing new types}
+%FIXME: syntax of typedef: subtype -> typedef; name -> id
+%FIXME: typevarlist and infix/mixfix in Ref manual and in sec:datatype
+
+The \HOL-methodology dictates that all extension to a theory should be
+conservative and thus preserve consistency. There are two basic type
+extension mechanisms which meet this criterion: {\em type synonyms\/} and
+{\em type definitions\/}. The former are inherited from {\tt Pure} and are
+described elsewhere.
+\begin{warn}
+ Types in \HOL\ must be non-empty; otherwise the quantifier rules would be
+ unsound~\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 generated to 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' ( () | '(' tname ')') type '=' set witness;
+type : typevarlist name ( () | '(' infix ')' );
+tname : name;
+set : string;
+witness : () | '(' id ')';
+\end{rail}
+\caption{Syntax of type definition}
+\label{fig:HOL:typedef}
+\end{figure}
+
+The syntax for type definitions is shown in Fig.~\ref{fig:HOL:typedef}. For
+the definition of ``typevarlist'' and ``infix'' see
+\iflabelundefined{chap:classical}
+{the appendix of the {\em Reference Manual\/}}%
+{Appendix~\ref{app:TheorySyntax}}. The remaining nonterminals have the
+following meaning:
+\begin{description}
+\item[\it type]: the new type constructor $(\alpha@1,\dots,\alpha@n)ty$ with
+ optional infix annotation.
+\item[\it tname]: an alphanumeric name $T$ for the type constructor $ty$, in
+ case $ty$ is a symbolic name. Default: $ty$.
+\item[\it set]: the representing subset $A$.
+\item[\it witness]: name of a theorem of the form $a:A$ proving
+ non-emptiness. Can be omitted in case Isabelle manages to prove
+ non-emptiness automatically.
+\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 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{eqnarray*}
+\item a definition and three axioms
+\[
+\begin{array}{ll}
+T{\tt_def} & T \equiv A \\
+{\tt Rep_}T & Rep_T(x) : T \\
+{\tt Rep_}T{\tt_inverse} & Abs_T(Rep_T(x)) = x \\
+{\tt Abs_}T{\tt_inverse} & y:T \Imp Rep_T(Abs_T(y)) = y
+\end{array}
+\]
+stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$
+and its inverse $Abs_T$.
+\end{itemize}
+Here are two simple examples where emptiness is proved automatically:
+\begin{ttbox}
+typedef unit = "\{False\}"
+
+typedef (prod)
+ ('a, 'b) "*" (infixr 20)
+ = "\{f . EX (a::'a) (b::'b). f = (\%x y. x = a & y = b)\}"
+\end{ttbox}
+
+Type definitions permit the introduction of abstract data types in a safe
+way, namely by providing models based on already existing types. Given some
+abstract axiomatic description $P$ of a type, this involves two steps:
+\begin{enumerate}
+\item Find an appropriate type $\tau$ and subset $A$ which has the desired
+ properties $P$, and make the above type definition based on this
+ representation.
+\item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.
+\end{enumerate}
+You can now forget about the representation and work solely in terms of the
+abstract properties $P$.
+
+\begin{warn}
+If you introduce a new type (constructor) $ty$ axiomatically, i.e.\ by
+declaring the type and its operations and by stating the desired axioms, you
+should make sure the type has a non-empty model. You must also have a clause
+\begin{ttbox}
+arities \(ty\): (term,\(\dots\),term)term
+\end{ttbox}
+in your theory file to tell Isabelle that elements of type $ty$ are in class
+{\tt term}, the class of all HOL terms.
+\end{warn}
+
\section{Datatype declarations}
+\label{sec:HOL:datatype}
\index{*datatype|(}
\underscoreon
@@ -1469,6 +1594,7 @@
because the simplifier will dispose of them automatically.
\subsection{Primitive recursive functions}
+\label{sec:HOL:primrec}
\index{primitive recursion|(}
\index{*primrec|(}
@@ -1711,7 +1837,7 @@
consts Fin :: 'a set => 'a set set
inductive "Fin A"
intrs
- emptyI "{} : Fin A"
+ emptyI "\{\} : Fin A"
insertI "[| a: A; b: Fin A |] ==> insert a b : Fin A"
\end{ttbox}
The resulting theory structure contains a substructure, called~{\tt Fin}.