--- a/doc-src/Logics/HOL.tex Fri May 09 19:43:16 1997 +0200
+++ b/doc-src/Logics/HOL.tex Fri May 09 19:43:44 1997 +0200
@@ -5,13 +5,15 @@
The theory~\thydx{HOL} implements higher-order logic. It is based on
Gordon's~{\sc hol} system~\cite{mgordon-hol}, which itself is based on
-Church's original paper~\cite{church40}. Andrews's book~\cite{andrews86} is
-a full description of higher-order logic. Experience with the {\sc hol}
-system has demonstrated that higher-order logic is widely applicable in many
-areas of mathematics and computer science, not just hardware verification,
-{\sc hol}'s original {\it raison d'\^etre\/}. It is weaker than {\ZF} set
-theory but for most applications this does not matter. If you prefer {\ML}
-to Lisp, you will probably prefer \HOL\ to~{\ZF}.
+Church's original paper~\cite{church40}. Andrews's
+book~\cite{andrews86} is a full description of the original
+Church-style higher-order logic. Experience with the {\sc hol} system
+has demonstrated that higher-order logic is widely applicable in many
+areas of mathematics and computer science, not just hardware
+verification, {\sc hol}'s original {\it raison d'\^etre\/}. It is
+weaker than {\ZF} set theory but for most applications this does not
+matter. If you prefer {\ML} to Lisp, you will probably prefer \HOL\
+to~{\ZF}.
The syntax of \HOL\footnote{Earlier versions of Isabelle's \HOL\ used a
different syntax. Ancient releases of Isabelle included still another version
@@ -30,10 +32,11 @@
with meta-level functions, so it uses Isabelle's operations for abstraction
and application.
-These identifications allow Isabelle to support \HOL\ particularly nicely,
-but they also mean that \HOL\ requires more sophistication from the user
---- in particular, an understanding of Isabelle's type system. Beginners
-should work with {\tt show_types} set to {\tt true}.
+These identifications allow Isabelle to support \HOL\ particularly
+nicely, but they also mean that \HOL\ requires more sophistication
+from the user --- in particular, an understanding of Isabelle's type
+system. Beginners should work with {\tt show_types} (or even
+\texttt{show_sorts}) set to {\tt true}.
% Gain experience by
%working in first-order logic before attempting to use higher-order logic.
%This chapter assumes familiarity with~{\FOL{}}.
@@ -64,7 +67,7 @@
existential quantifier ($\exists$) \\
{\tt?!} or {\tt EX!} & \cdx{Ex1} & $(\alpha\To bool)\To bool$ &
unique existence ($\exists!$)\\
- {\tt LEAST} & \cdx{Least} & $(\alpha\To bool)\To\alpha$ &
+ {\tt LEAST} & \cdx{Least} & $(\alpha::ord \To bool)\To\alpha$ &
least element
\end{constants}
\subcaption{Binders}
@@ -140,29 +143,33 @@
\end{warn}
\subsection{Types and classes}
-The type class of higher-order terms is called~\cldx{term}. By default,
-explicit type variables have class \cldx{term}. In particular the equality
-symbol and quantifiers are polymorphic over class {\tt term}.
+The universal type class of higher-order terms is called~\cldx{term}.
+By default, explicit type variables have class \cldx{term}. In
+particular the equality symbol and quantifiers are polymorphic over
+class {\tt term}.
The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,
-formulae are terms. The built-in type~\tydx{fun}, which constructs function
-types, is overloaded with arity {\tt(term,term)term}. Thus, $\sigma\To\tau$
-belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification
-over functions.
+formulae are terms. The built-in type~\tydx{fun}, which constructs
+function types, is overloaded with arity {\tt(term,\thinspace
+ term)\thinspace term}. Thus, $\sigma\To\tau$ belongs to class~{\tt
+ term} if $\sigma$ and~$\tau$ do, allowing quantification over
+functions.
-HOL offers various methods for introducing new
-types. See~\S\ref{sec:HOL:Types} and~\S\ref{sec:HOL:datatype}.
+\HOL\ offers various methods for introducing new types.
+See~\S\ref{sec:HOL:Types} and~\S\ref{sec:HOL:datatype}.
-Theory \thydx{Ord} defines the class \cldx{ord} of all ordered types; the
-relations $<$ and $\leq$ are polymorphic over this class, as are the functions
-\cdx{mono}, \cdx{min} and \cdx{max}, and the least element operator
-\cdx{LEAST}. \thydx{Ord} also defines the subclass \cldx{order} of \cldx{ord}
-which axiomatizes partially ordered types (w.r.t.\ $\le$).
+Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order
+signatures; the relations $<$ and $\leq$ are polymorphic over this
+class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and
+the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass
+\cldx{order} of \cldx{ord} which axiomatizes partially ordered types
+(w.r.t.\ $\le$).
-Three other type classes --- \cldx{plus}, \cldx{minus} and \cldx{times} ---
-permit overloading of the operators {\tt+},\index{*"+ symbol}
-{\tt-}\index{*"- symbol} and {\tt*}.\index{*"* symbol} In particular, {\tt-}
-is overloaded for set difference and subtraction.
+Three other syntactic type classes --- \cldx{plus}, \cldx{minus} and
+\cldx{times} --- permit overloading of the operators {\tt+},\index{*"+
+ symbol} {\tt-}\index{*"- symbol} and {\tt*}.\index{*"* symbol} In
+particular, {\tt-} is instantiated for set difference and subtraction
+on natural numbers.
If you state a goal containing overloaded functions, you may need to include
type constraints. Type inference may otherwise make the goal more
@@ -175,9 +182,9 @@
\begin{warn}
If resolution fails for no obvious reason, try setting
- \ttindex{show_types} to {\tt true}, causing Isabelle to display types of
- terms. Possibly set \ttindex{show_sorts} to {\tt true} as well, causing
- Isabelle to display sorts.
+ \ttindex{show_types} to {\tt true}, causing Isabelle to display
+ types of terms. Possibly set \ttindex{show_sorts} to {\tt true} as
+ well, causing Isabelle to display type classes and sorts.
\index{unification!incompleteness of}
Where function types are involved, Isabelle's unification code does not
@@ -190,11 +197,12 @@
\subsection{Binders}
-Hilbert's {\bf description} operator~$\varepsilon x.P$ 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$) or use the syntax \hbox{\tt \at $x$.$P$}.
+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). \]
@@ -215,12 +223,17 @@
true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set
to {\tt false}, then~{\tt ALL} and~{\tt EX} are displayed.
-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$ denotes the least (w.r.t.\
-$\le$) $x$ such that $P~x$ holds (see Fig.~\ref{hol-defs}). Note that
-unless $\le$ is a linear order, the result is not uniquely defined.
+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!}
-All these binders have priority 10.
+\medskip All these binders have priority 10.
\begin{warn}
The low priority of binders means that they need to be enclosed in
@@ -241,12 +254,12 @@
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
+This is what happens automatically for each {\tt datatype} definition
(see~\S\ref{sec:HOL:datatype}).
\begin{warn}
Both {\tt if} and {\tt case} constructs have as low a priority as
-quantifiers, which requires additional enclosing parenthesis in the context
+quantifiers, which requires additional enclosing parentheses in the context
of most other operations. For example, instead of $f~x = if \dots then \dots
else \dots$ you need to write $f~x = (if \dots then \dots else
\dots)$.
@@ -256,13 +269,13 @@
\begin{figure}
\begin{ttbox}\makeatother
-\tdx{refl} t = t
-\tdx{subst} [| s=t; P s |] ==> P t
-\tdx{ext} (!!x. f x = g x) ==> (\%x.f x) = (\%x.g x)
+\tdx{refl} t = (t::'a)
+\tdx{subst} [| s = t; P s |] ==> P (t::'a)
+\tdx{ext} (!!x::'a. (f x :: 'b) = g x) ==> (\%x.f x) = (\%x.g x)
\tdx{impI} (P ==> Q) ==> P-->Q
\tdx{mp} [| P-->Q; P |] ==> Q
\tdx{iff} (P-->Q) --> (Q-->P) --> (P=Q)
-\tdx{selectI} P(x) ==> P(@x.P x)
+\tdx{selectI} P(x::'a) ==> P(@x.P x)
\tdx{True_or_False} (P=True) | (P=False)
\end{ttbox}
\caption{The {\tt HOL} rules} \label{hol-rules}
@@ -294,10 +307,11 @@
\tdx{or_def} op | == (\%P Q. !R. (P-->R) --> (Q-->R) --> R)
\tdx{Ex1_def} Ex1 == (\%P. ? x. P x & (! y. P y --> y=x))
-\tdx{o_def} op o == (\%f g x. f(g x))
-\tdx{if_def} If P x y == (\%P x y.@z.(P=True --> z=x) & (P=False --> z=y))
+\tdx{o_def} op o == (\%(f::'b=>'c) g x::'a. f(g x))
+\tdx{if_def} If P x y ==
+ (\%P x y. @z::'a.(P=True --> z=x) & (P=False --> z=y))
\tdx{Let_def} Let s f == f s
-\tdx{Least_def} Least P == @x. P(x) & (ALL y. y<x --> ~P(y))
+\tdx{Least_def} Least P == @x. P(x) & (ALL y. P(y) --> x <= y)"
\end{ttbox}
\caption{The {\tt HOL} definitions} \label{hol-defs}
\end{figure}
@@ -475,9 +489,9 @@
\tt `` & $[\alpha\To\beta ,\alpha\,set]\To (\beta\,set)$
& Left 90 & image \\
\sdx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
- & Left 70 & intersection ($\inter$) \\
+ & Left 70 & intersection ($\int$) \\
\sdx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
- & Left 65 & union ($\union$) \\
+ & Left 65 & union ($\un$) \\
\tt: & $[\alpha ,\alpha\,set]\To bool$
& Left 50 & membership ($\in$) \\
\tt <= & $[\alpha\,set,\alpha\,set]\To bool$
@@ -495,8 +509,8 @@
\begin{tabular}{rrr}
\it external & \it internal & \it description \\
$a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm non-membership\\
- \{$a@1$, $\ldots$\} & insert $a@1$ $\ldots$ \{\} & \rm finite set \\
- \{$x$.$P[x]$\} & Collect($\lambda x.P[x]$) &
+ {\ttlbrace}$a@1$, $\ldots${\ttrbrace} & insert $a@1$ $\ldots$ {\ttlbrace}{\ttrbrace} & \rm finite set \\
+ {\ttlbrace}$x$.$P[x]${\ttrbrace} & Collect($\lambda x.P[x]$) &
\rm comprehension \\
\sdx{INT} $x$:$A$.$B[x]$ & INTER $A$ $\lambda x.B[x]$ &
\rm intersection \\
@@ -514,9 +528,9 @@
\dquotes
\[\begin{array}{rclcl}
term & = & \hbox{other terms\ldots} \\
- & | & "\{\}" \\
- & | & "\{ " term\; ("," term)^* " \}" \\
- & | & "\{ " id " . " formula " \}" \\
+ & | & "{\ttlbrace}{\ttrbrace}" \\
+ & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\
+ & | & "{\ttlbrace} " id " . " formula " {\ttrbrace}" \\
& | & term " `` " term \\
& | & term " Int " term \\
& | & term " Un " term \\
@@ -569,19 +583,19 @@
Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new
-constructs. Infix operators include union and intersection ($A\union B$
-and $A\inter B$), the subset and membership relations, and the image
+constructs. Infix operators include union and intersection ($A\un B$
+and $A\int B$), the subset and membership relations, and the image
operator~{\tt``}\@. Note that $a$\verb|~:|$b$ is translated to
$\neg(a\in b)$.
-The {\tt\{\ldots\}} notation abbreviates finite sets constructed in the
-obvious manner using~{\tt insert} and~$\{\}$:
+The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in
+the obvious manner using~{\tt insert} and~$\{\}$:
\begin{eqnarray*}
- \{a@1, \ldots, a@n\} & \equiv &
- {\tt insert}~a@1~({\tt insert}\ldots({\tt insert}~a@n~\{\})\ldots)
+ \{a, b, c\} & \equiv &
+ {\tt insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\}))
\end{eqnarray*}
-The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type)
+The set \hbox{\tt{\ttlbrace}$x$.$P[x]${\ttrbrace}} consists of all $x$ (of suitable type)
that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda
x.P[x])$. It defines sets by absolute comprehension, which is impossible
@@ -620,27 +634,27 @@
\begin{figure} \underscoreon
\begin{ttbox}
-\tdx{mem_Collect_eq} (a : \{x.P x\}) = P a
-\tdx{Collect_mem_eq} \{x.x:A\} = A
+\tdx{mem_Collect_eq} (a : {\ttlbrace}x.P x{\ttrbrace}) = P a
+\tdx{Collect_mem_eq} {\ttlbrace}x.x:A{\ttrbrace} = A
-\tdx{empty_def} \{\} == \{x.False\}
-\tdx{insert_def} insert a B == \{x.x=a\} Un B
+\tdx{empty_def} {\ttlbrace}{\ttrbrace} == {\ttlbrace}x.False{\ttrbrace}
+\tdx{insert_def} insert a B == {\ttlbrace}x.x=a{\ttrbrace} Un B
\tdx{Ball_def} Ball A P == ! x. x:A --> P x
\tdx{Bex_def} Bex A P == ? x. x:A & P x
\tdx{subset_def} A <= B == ! x:A. x:B
-\tdx{Un_def} A Un B == \{x.x:A | x:B\}
-\tdx{Int_def} A Int B == \{x.x:A & x:B\}
-\tdx{set_diff_def} A - B == \{x.x:A & x~:B\}
-\tdx{Compl_def} Compl A == \{x. ~ x:A\}
-\tdx{INTER_def} INTER A B == \{y. ! x:A. y: B x\}
-\tdx{UNION_def} UNION A B == \{y. ? x:A. y: B x\}
-\tdx{INTER1_def} INTER1 B == INTER \{x.True\} B
-\tdx{UNION1_def} UNION1 B == UNION \{x.True\} B
+\tdx{Un_def} A Un B == {\ttlbrace}x.x:A | x:B{\ttrbrace}
+\tdx{Int_def} A Int B == {\ttlbrace}x.x:A & x:B{\ttrbrace}
+\tdx{set_diff_def} A - B == {\ttlbrace}x.x:A & x~:B{\ttrbrace}
+\tdx{Compl_def} Compl A == {\ttlbrace}x. ~ x:A{\ttrbrace}
+\tdx{INTER_def} INTER A B == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace}
+\tdx{UNION_def} UNION A B == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace}
+\tdx{INTER1_def} INTER1 B == INTER {\ttlbrace}x.True{\ttrbrace} B
+\tdx{UNION1_def} UNION1 B == UNION {\ttlbrace}x.True{\ttrbrace} B
\tdx{Inter_def} Inter S == (INT x:S. x)
\tdx{Union_def} Union S == (UN x:S. x)
-\tdx{Pow_def} Pow A == \{B. B <= A\}
-\tdx{image_def} f``A == \{y. ? x:A. y=f x\}
-\tdx{range_def} range f == \{y. ? x. y=f x\}
+\tdx{Pow_def} Pow A == {\ttlbrace}B. B <= A{\ttrbrace}
+\tdx{image_def} f``A == {\ttlbrace}y. ? x:A. y=f x{\ttrbrace}
+\tdx{range_def} range f == {\ttlbrace}y. ? x. y=f x{\ttrbrace}
\end{ttbox}
\caption{Rules of the theory {\tt Set}} \label{hol-set-rules}
\end{figure}
@@ -648,9 +662,9 @@
\begin{figure} \underscoreon
\begin{ttbox}
-\tdx{CollectI} [| P a |] ==> a : \{x.P x\}
-\tdx{CollectD} [| a : \{x.P x\} |] ==> P a
-\tdx{CollectE} [| a : \{x.P x\}; P a ==> W |] ==> W
+\tdx{CollectI} [| P a |] ==> a : {\ttlbrace}x.P x{\ttrbrace}
+\tdx{CollectD} [| a : {\ttlbrace}x.P x{\ttrbrace} |] ==> P a
+\tdx{CollectE} [| a : {\ttlbrace}x.P x{\ttrbrace}; P a ==> W |] ==> W
\tdx{ballI} [| !!x. x:A ==> P x |] ==> ! x:A. P x
\tdx{bspec} [| ! x:A. P x; x:A |] ==> P x
@@ -684,7 +698,7 @@
\begin{figure} \underscoreon
\begin{ttbox}
-\tdx{emptyE} a : \{\} ==> P
+\tdx{emptyE} a : {\ttlbrace}{\ttrbrace} ==> P
\tdx{insertI1} a : insert a B
\tdx{insertI2} a : B ==> a : insert b B
@@ -807,8 +821,8 @@
\tdx{Un_assoc} (A Un B) Un C = A Un (B Un C)
\tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)
-\tdx{Compl_disjoint} A Int (Compl A) = \{x.False\}
-\tdx{Compl_partition} A Un (Compl A) = \{x.True\}
+\tdx{Compl_disjoint} A Int (Compl A) = {\ttlbrace}x.False{\ttrbrace}
+\tdx{Compl_partition} A Un (Compl A) = {\ttlbrace}x.True{\ttrbrace}
\tdx{double_complement} Compl(Compl A) = A
\tdx{Compl_Un} Compl(A Un B) = (Compl A) Int (Compl B)
\tdx{Compl_Int} Compl(A Int B) = (Compl A) Un (Compl B)
@@ -888,15 +902,16 @@
\HOL\ instantiates most of Isabelle's generic packages, making available the
simplifier and the classical reasoner.
-\subsection{Substitution and simplification}
+\subsection{Simplification and substitution}
-The simplifier is available in \HOL. Tactics such as {\tt Asm_simp_tac} and
-{\tt
-Full_simp_tac} use the default simpset ({\tt!simpset}), which works for most
-purposes. A minimal simplification set for higher-order logic
-is~\ttindexbold{HOL_ss}. Equality~($=$), which also expresses logical
-equivalence, may be used for rewriting. See the file {\tt HOL/simpdata.ML}
-for a complete listing of the basic simplification rules.
+The simplifier is available in \HOL. Tactics such as {\tt
+ Asm_simp_tac} and {\tt Full_simp_tac} use the default simpset
+({\tt!simpset}), which works for most purposes. A quite minimal
+simplification set for higher-order logic is~\ttindexbold{HOL_ss},
+even more frugal is \ttindexbold{HOL_basic_ss}. Equality~($=$), which
+also expresses logical equivalence, may be used for rewriting. See
+the file {\tt HOL/simpdata.ML} for a complete listing of the basic
+simplification rules.
See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
{Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution
@@ -909,9 +924,9 @@
including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.
\end{warn}
-If the simplifier cannot use a certain rewrite rule---either because of
-nontermination or because its left-hand side is too flexible---then you might
-try {\tt stac}:
+If the simplifier cannot use a certain rewrite rule --- either because
+of nontermination or because its left-hand side is too flexible ---
+then you might try {\tt stac}:
\begin{ttdescription}
\item[\ttindexbold{stac} $thm$ $i,$] where $thm$ is of the form $lhs = rhs$,
replaces in subgoal $i$ instances of $lhs$ by corresponding instances of
@@ -943,11 +958,13 @@
\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
+This section describes \HOL's basic predefined types ($\alpha \times
+\beta$, $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for
+introducing new types in general. 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}
\label{subsec:prod-sum}
@@ -968,7 +985,7 @@
%\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{Sigma_def} Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace}
\tdx{Pair_eq} ((a,b) = (a',b')) = (a=a' & b=b')
\tdx{Pair_inject} [| (a, b) = (a',b'); [| a=a'; b=b' |] ==> R |] ==> R
@@ -988,14 +1005,14 @@
\end{figure}
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:
+$\alpha\times\beta$, with the ordered pair syntax $(a, b)$. General
+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)$ \\
+$\tau@1 \times \dots \times \tau@n$ & $\tau@1 \times (\dots (\tau@{n-1} \times \tau@n)\dots)$ \\
\hline
$(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\
\hline
@@ -1004,7 +1021,7 @@
In addition, it is possible to use tuples
as patterns in abstractions:
\begin{center}
-{\tt\%($x$,$y$).$t$} \quad stands for\quad {\tt split(\%$x$ $y$.$t$)}
+{\tt\%($x$,$y$).$t$} \quad stands for\quad {\tt split(\%$x$\thinspace$y$.$t$)}
\end{center}
Nested patterns are also supported. They are translated stepwise:
{\tt\%($x$,$y$,$z$).$t$} $\leadsto$ {\tt\%($x$,($y$,$z$)).$t$} $\leadsto$
@@ -1025,7 +1042,7 @@
\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$~\}}
+\item[Sets:] {\tt {\ttlbrace}~{\it pattern}~.~$P$~{\ttrbrace}}
\end{description}
There is a simple tactic which supports reasoning about patterns:
@@ -1051,9 +1068,9 @@
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.
+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 theory files.
\begin{figure}
\begin{constants}
@@ -1067,7 +1084,7 @@
%\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{Inl_not_Inr} Inl a ~= Inr b
\tdx{inj_Inl} inj Inl
\tdx{inj_Inr} inj Inr
@@ -1159,13 +1176,13 @@
\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 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. For details see the file {\tt NatDef.thy}.
+The theory \thydx{NatDef} 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. For details see the file
+\texttt{NatDef.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
@@ -1179,7 +1196,7 @@
overloaded functions of this class (esp.\ \cdx{<} and \cdx{<=}, but also
\cdx{min}, \cdx{max} and \cdx{LEAST}) available on {\tt nat}. Theory
\thydx{Nat} builds on {\tt NatDef} and shows that {\tt<=} is a partial order,
-i.e.\ {\tt nat} is an instance of class {\tt order}.
+i.e.\ {\tt nat} is even an instance of class {\tt order}.
Theory \thydx{Arith} develops arithmetic on the natural numbers. It
defines addition, multiplication, subtraction, division, and remainder.
@@ -1187,10 +1204,11 @@
distributive laws, identity and cancellation laws, etc.
% The most
%interesting result is perhaps the theorem $a \bmod b + (a/b)\times b = a$.
-Division and remainder are defined by repeated subtraction, which requires
-well-founded rather than primitive recursion. See Figs.\ts\ref{hol-nat1}
-and~\ref{hol-nat2}. The recursion equations for the operators {\tt +}, {\tt
--} and {\tt *} are part of the default simpset.
+Division and remainder are defined by repeated subtraction, which
+requires well-founded rather than primitive recursion. See
+Figs.\ts\ref{hol-nat1} and~\ref{hol-nat2}. The recursion equations for
+the operators {\tt +}, {\tt -} and {\tt *} on \texttt{nat} are part of
+the default simpset.
Functions on {\tt nat} can be defined by primitive recursion, for example
addition:
@@ -1199,11 +1217,11 @@
"0 + n = n"
"Suc m + n = Suc(m + n)"
\end{ttbox}
-(Remember that the name of an infix operator $\oplus$ is {\tt op}~$\oplus$.)
-The general format for defining primitive recursive functions on {\tt nat}
-follows the rules for primitive recursive functions on datatypes
-(see~\S\ref{sec:HOL:primrec}).
-There is also a \sdx{case}-construct of the form
+Remember that the name of infix operators usually has an {\tt op}
+prefixed. The general format for defining primitive recursive
+functions on {\tt nat} follows the rules for primitive recursive
+functions on datatypes (see~\S\ref{sec:HOL:primrec}). There is also a
+\sdx{case}-construct of the form
\begin{ttbox}
case \(e\) of 0 => \(a\) | Suc \(m\) => \(b\)
\end{ttbox}
@@ -1222,7 +1240,7 @@
Tactic {\tt\ttindex{induct_tac} "$n$" $i$} performs induction on variable~$n$
in subgoal~$i$ using theorem {\tt nat_induct}. There is also the derived
-theorem \tdx{less_induct}
+theorem \tdx{less_induct}:
\begin{ttbox}
[| !!n. [| ! m. m<n --> P m |] ==> P n |] ==> P n
\end{ttbox}
@@ -1234,7 +1252,7 @@
{\tt 0}, {\tt Suc}, {\tt<} and {\tt<=}. The following goals are all solved by
{\tt trans_tac 1}:
\begin{ttbox}
-{\out 1. [| \dots |] ==> m <= Suc(Suc m)}
+{\out 1. \dots ==> m <= Suc(Suc m)}
{\out 1. [| \dots i <= j \dots Suc j <= k \dots |] ==> i < k}
{\out 1. [| \dots Suc m <= n \dots ~ m < n \dots |] ==> \dots}
\end{ttbox}
@@ -1266,8 +1284,6 @@
& & 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{set_of_list}& $\alpha\,list \To \alpha\,set$ & & elements\\
\sdx{mem} & $[\alpha,\alpha\,list]\To bool$ & Left 55 & membership\\
\cdx{foldl} & $(\beta\To\alpha\To\beta) \To \beta \To \alpha\,list \To \beta$ &
@@ -1316,7 +1332,7 @@
filter P [] = []
filter P (x#xs) = (if P x then x#filter P xs else filter P xs)
-set_of_list [] = \{\}
+set_of_list [] = \ttlbrace\ttrbrace
set_of_list (x#xs) = insert x (set_of_list xs)
x mem [] = False
@@ -1358,10 +1374,11 @@
\index{*list type}
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\#}. As a
-result the generic induction tactic \ttindex{induct_tac} also performs
-structural induction over lists. A \sdx{case} construct of the form
+operations with their types and syntax. Type $\alpha \; list$ is
+defined as a {\tt datatype} with the constructors {\tt[]} and {\tt\#}.
+As a result the generic induction tactic \ttindex{induct_tac} also
+performs structural induction over lists. A \sdx{case} construct of
+the form
\begin{center}\tt
case $e$ of [] => $a$ | \(x\)\#\(xs\) => b
\end{center}
@@ -1372,13 +1389,15 @@
are shown in Fig.\ts\ref{fig:HOL:list-simps}.
-\subsection{Introducing new types}
+\subsection{Introducing new types} \label{sec:typedef}
-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.
+The \HOL-methodology dictates that all extensions to a theory should
+be \textbf{definitional}. The basic type definition mechanism which
+meets this criterion --- w.r.t.\ the standard model theory of
+\textsc{hol} --- is \ttindex{typedef}. Note that \emph{type synonyms},
+which are inherited from {\Pure} and described elsewhere, are just
+syntactic abbreviations that have no logical meaning.
+
\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}.
@@ -1394,13 +1413,12 @@
\begin{figure}[htbp]
\begin{rail}
-typedef : 'typedef' ( () | '(' tname ')') type '=' set witness;
+typedef : 'typedef' ( () | '(' name ')') type '=' set witness;
type : typevarlist name ( () | '(' infix ')' );
-tname : name;
set : string;
witness : () | '(' id ')';
\end{rail}
-\caption{Syntax of type definition}
+\caption{Syntax of type definitions}
\label{fig:HOL:typedef}
\end{figure}
@@ -1411,13 +1429,13 @@
{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
+\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
+\item[\it name:] an alphanumeric name $T$ for the type constructor
+ $ty$, in case $ty$ is a symbolic name. Defaults to $ty$.
+\item[\it set:] the representing subset $A$.
+\item[\it witness:] name of a theorem of the form $a:A$ proving
+ non-emptiness. It 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
@@ -1427,7 +1445,7 @@
\item a type $ty :: (term,\dots)term$;
\item constants
\begin{eqnarray*}
-T &::& (\tau)set \\
+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*}
@@ -1435,21 +1453,22 @@
\[
\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
+{\tt Rep_}T & Rep_T\,x \in T \\
+{\tt Rep_}T{\tt_inverse} & Abs_T\,(Rep_T\,x) = x \\
+{\tt Abs_}T{\tt_inverse} & y \in 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:
+Below are two simple examples of \HOL\ type definitions. Emptiness is
+proved automatically here.
\begin{ttbox}
-typedef unit = "\{True\}"
+typedef unit = "{\ttlbrace}True{\ttrbrace}"
typedef (prod)
('a, 'b) "*" (infixr 20)
- = "\{f . EX (a::'a) (b::'b). f = (\%x y. x = a & y = b)\}"
+ = "{\ttlbrace}f . EX (a::'a) (b::'b). f = (\%x y. x = a & y = b){\ttrbrace}"
\end{ttbox}
Type definitions permit the introduction of abstract data types in a safe
@@ -1469,105 +1488,111 @@
should make sure the type has a non-empty model. You must also have a clause
\par
\begin{ttbox}
-arities \(ty\): (term,\(\dots\),term)term
+arities \(ty\) :: (term,\thinspace\(\dots\),{\thinspace}term){\thinspace}term
\end{ttbox}
in your theory file to tell Isabelle that $ty$ is in class {\tt term}, the
-class of all HOL types.
+class of all \HOL\ types.
\end{warn}
\section{Datatype declarations}
\label{sec:HOL:datatype}
\index{*datatype|(}
-It is often necessary to extend a theory with \ML-like datatypes. This
-extension consists of the new type, declarations of its constructors and
-rules that describe the new type. The theory definition section {\tt
-datatype} automates this.
+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.
-\subsection{Foundations}
-
-\underscoreon
+\subsection{Basics}
-A datatype declaration has the following general structure:
-\[ \mbox{\tt datatype}~ (\alpha_1,\dots,\alpha_n)t ~=~
- C_1~\tau_{11}~\dots~\tau_{1k_1} ~\mid~ \dots ~\mid~
- C_m~\tau_{m1}~\dots~\tau_{mk_m}
+The general \HOL\ \texttt{datatype} definition is of the following form:
+\[
+\mathtt{datatype}~(\alpha@1, \dots, \alpha@n) \, t ~=~
+C@1~\tau@{11}~\dots~\tau@{1k@1} ~\mid~ \dots ~\mid~
+C@m~\tau@{m1}~\dots~\tau@{mk@m}
\]
-where $\alpha_i$ are type variables, $C_i$ are distinct constructor names and
-$\tau_{ij}$ are one of the following:
+where $\alpha@i$ are type variables, $C@i$ are distinct constructor
+names and $\tau@{ij}$ are types. The latter may be one of the
+following:
\begin{itemize}
-\item type variables $\alpha_1,\dots,\alpha_n$,
-\item types $(\beta_1,\dots,\beta_l)s$ where $s$ is a previously declared
- type or type synonym and $\{\beta_1,\dots,\beta_l\} \subseteq
- \{\alpha_1,\dots,\alpha_n\}$,
-\item the newly defined type $(\alpha_1,\dots,\alpha_n)t$ \footnote{This
- makes it a recursive type. To ensure that the new type is not empty at
- least one constructor must consist of only non-recursive type
- components.}
+\item type variables $\alpha@1, \dots, \alpha@n$,
+
+\item types $(\beta@1, \dots, \beta@l) \, t'$ where $t'$ is a
+ previously declared type constructor or type synonym and $\{\beta@1,
+ \dots, \beta@l\} \subseteq \{\alpha@1, \dots, \alpha@n\}$,
+
+\item the newly defined type $(\alpha@1, \dots, \alpha@n) \, t$.
\end{itemize}
-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 \[ \mbox{\tt
- datatype}~ t ~=~ C(t \To t) \] together with unproblematic ones like \[
-\mbox{\tt datatype}~ t ~=~ C(t~list). \]
+Recursive occurences of $(\alpha@1, \dots, \alpha@n) \, t$ are quite
+restricted. To ensure that the new type is not 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 \]
+\[ C@j : [\tau@{j1},\dots,\tau@{jk@j}] \To (\alpha@1,\dots,\alpha@n)t \]
These functions have certain {\em freeness} properties:
-\begin{description}
-\item[\tt distinct] 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[\tt inject] 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{description}
+\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}
Because the number of inequalities is quadratic in the number of
-constructors, a different method is used if their number exceeds
-a certain value, currently 6. In that case every constructor is mapped to a
-natural number
+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:
\[
-\begin{array}{lcl}
-\mbox{\it t\_ord}(C_1~x_1~\dots~x_{k_1}) & = & 0 \\
-& \vdots & \\
-\mbox{\it t\_ord}(C_m x_1~\dots~x_{k_m}) & = & m-1
-\end{array}
+t_ord \, (C@i \, x@1 \, \dots \, x@{k@1}) = i - 1
\]
-and distinctness of constructors is expressed by:
+Then distinctness of constructor terms is expressed by:
\[
-\mbox{\it t\_ord}~x \neq \mbox{\it t\_ord}~y \Imp x \neq y.
+t_ord \, x \neq t_ord \, y \Imp x \neq y.
\]
-In addition a structural induction axiom {\tt induct} is provided:
+
+\medskip Furthermore, the following structural induction rule is
+provided:
\[
-\infer{P x}
+\infer{P \, x}
{\begin{array}{lcl}
-\Forall x_1\dots x_{k_1}.
- \List{P~x_{r_{11}}; \dots; P~x_{r_{1l_1}}} &
- \Imp & P(C_1~x_1~\dots~x_{k_1}) \\
+\Forall x@1\dots x@{k@1}.
+ \List{P~x@{r@{11}}; \dots; P~x@{r@{1l@1}}} &
+ \Imp & P \, (C@1~x@1~\dots~x@{k@1}) \\
& \vdots & \\
-\Forall x_1\dots x_{k_m}.
- \List{P~x_{r_{m1}}; \dots; P~x_{r_{ml_m}}} &
- \Imp & P(C_m~x_1~\dots~x_{k_m})
+\Forall x@1\dots x@{k@m}.
+ \List{P~x@{r@{m1}}; \dots; P~x@{r@{ml@m}}} &
+ \Imp & P \, (C@m~x@1~\dots~x@{k@m})
\end{array}}
\]
-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
+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:
\[
\begin{array}{rrcl}
-\mbox{\tt case}~e~\mbox{\tt of} & C_1~x_{11}~\dots~x_{1k_1} & \To & e_1 \\
+\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
+ \mid & C@m~x@{m1}~\dots~x@{mk@m} & \To & e@m
\end{array}
\]
-where the $x_{ij}$ are either identifiers or nested tuple patterns as in
+where the $x@{ij}$ are either identifiers or nested tuple patterns as in
\S\ref{subsec:prod-sum}.
\begin{warn}
In contrast to \ML, {\em all} constructors must be present, their order is
@@ -1575,16 +1600,15 @@
Violating this restriction results in strange error messages.
\end{warn}
-\underscoreoff
\subsection{Defining datatypes}
-A datatype is defined in a theory definition file using the keyword {\tt
- datatype}. The definition following {\tt datatype} must conform to the
-syntax of {\em typedecl} specified in Fig.~\ref{datatype-grammar} and must
-obey the rules in the previous section. As a result the theory is extended
-with the new type, the constructors, and the theorems listed in the previous
-section.
+A datatype is defined in a theory definition file using the keyword
+{\tt datatype}. The definition following this must conform to the
+syntax of {\em typedecl} specified in Fig.~\ref{datatype-grammar} and
+must obey the rules in the previous section. As a result the theory is
+extended with the new type, the constructors, and the theorems listed
+in the previous section.
\begin{figure}
\begin{rail}
@@ -1600,9 +1624,10 @@
\end{figure}
\begin{warn}
- If there are 7 or more constructors, the {\it t\_ord} scheme is used for
- distinctness theorems. In this case the theory {\tt Arith} must be
- contained in the current theory, if necessary by including it explicitly.
+ If there are 7 or more constructors, the {\it t\_ord} scheme is used
+ for distinctness theorems. In this case the theory {\tt Arith} must
+ be contained in the current theory, if necessary by including it
+ explicitly as a parent.
\end{warn}
Most of the theorems about the datatype become part of the default simpset
@@ -1615,10 +1640,10 @@
\end{ttdescription}
For the technically minded, we give a more detailed description.
-Reading the theory file produces a structure which, in addition to the usual
-components, contains a structure named $t$ for each datatype $t$ defined in
-the file.\footnote{Otherwise multiple datatypes in the same theory file would
- lead to name clashes.} Each structure $t$ contains the following elements:
+Reading the theory file produces a structure which, in addition to the
+usual components, contains a structure named $t$ for each datatype $t$
+defined in the file. Each structure $t$ contains the following
+elements:
\begin{ttbox}
val distinct : thm list
val inject : thm list
@@ -1627,19 +1652,20 @@
val simps : thm list
val induct_tac : string -> int -> tactic
\end{ttbox}
-{\tt distinct}, {\tt inject} and {\tt induct} contain the theorems described
-above. For convenience {\tt distinct} contains inequalities in both
-directions. The reduction rules of the {\tt case}-construct are in {\tt
-cases}. All theorems from {\tt distinct}, {\tt inject} and {\tt cases} are
-combined in {\tt simps}.
+{\tt distinct}, {\tt inject} and {\tt induct} contain the theorems
+described above. For user convenience, {\tt distinct} contains
+inequalities in both directions. The reduction rules of the {\tt
+ case}-construct are in {\tt cases}. All theorems from {\tt
+ distinct}, {\tt inject} and {\tt cases} are combined in {\tt simps}.
\subsection{Examples}
\subsubsection{The datatype $\alpha~list$}
-We want to define the type $\alpha~list$.\footnote{Of course there is a list
- type in HOL already. This is only an example.} To do this we have to build
-a new theory that contains the type definition. We start from {\tt HOL}.
+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
+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)
@@ -1696,8 +1722,9 @@
after the constructor declarations as follows:
\begin{ttbox}
MyList = HOL +
- datatype 'a list = "[]" ("[]")
- | "#" 'a ('a list) (infixr 70)
+ datatype 'a list =
+ Nil ("[]") |
+ Cons 'a ('a list) (infixr "#" 70)
end
\end{ttbox}
Now the theorem in the previous example can be written \verb|x#xs ~= xs|. The
@@ -1706,7 +1733,7 @@
\subsubsection{A datatype for weekdays}
-This example shows a datatype that consists of more than 6 constructors:
+This example shows a datatype that consists of 7 constructors:
\begin{ttbox}
Days = Arith +
datatype days = Mo | Tu | We | Th | Fr | Sa | So
@@ -1730,9 +1757,10 @@
\index{primitive recursion|(}
\index{*primrec|(}
-Datatypes come with a uniform way of defining functions, {\bf primitive
- recursion}. Although it is possible to define primitive recursive functions
-by asserting their reduction rules as new axioms, e.g.\
+Datatypes come with a uniform way of defining functions, {\bf
+ 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
@@ -1741,9 +1769,11 @@
app_Cons "app (x#xs) ys = x#app xs ys"
end
\end{ttbox}
-this carries with it the danger of accidentally asserting an inconsistency,
-as in \verb$app [] ys = us$. Therefore primitive recursive functions on
-datatypes can be defined with a special syntax:
+This carries with it the danger of accidentally asserting an
+inconsistency, as in \verb$app [] ys = us$, though.
+
+\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
@@ -1759,10 +1789,8 @@
primrec app MyList.list
"app [] ys = us"
\end{ttbox}
-is rejected:
-\begin{ttbox}
-Extra variables on rhs
-\end{ttbox}
+is rejected with an error message \texttt{Extra variables on rhs}.
+
\bigskip
The general form of a primitive recursive definition is
@@ -1773,33 +1801,29 @@
where
\begin{itemize}
\item {\it function} is the name of the function, either as an {\it id} or a
- {\it string}. The function must already have been declared.
-\item {\it type} is the name of the datatype, either as an {\it id} or in the
- long form {\it Thy.t}, where {\it Thy} is the name of the parent theory the
- datatype was declared in, and $t$ the name of the datatype. The long form
- is required if the {\tt datatype} and the {\tt primrec} sections are in
- different theories.
-\item {\it reduction rules} specify one or more equations of the form \[
- f~x@1~\dots~x@m~(C~y@1~\dots~y@k)~z@1~\dots~z@n = r \] such that $C$ is a
- constructor of the datatype, $r$ contains only the free variables on the
- left-hand side, and all recursive calls in $r$ are of the form
- $f~\dots~y@i~\dots$ for some $i$. There must be exactly one reduction rule
- for each constructor. The order is immaterial. {\em All reduction rules are
- added to the default {\tt simpset}.}
+ {\it string}. The function must already have been declared as a constant.
+\item {\it type} is the name of the datatype, either as an {\it id} or
+ in the long form \texttt{$T$.$t$} ($T$ is the name of the theory
+ where the datatype has been declared, $t$ the name of the datatype).
+ The long form is required if the {\tt datatype} and the {\tt
+ primrec} sections are in different theories.
+\item {\it reduction rules} specify one or more equations of the form
+ \[ f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \,
+ \dots \, z@n = r \] such that $C$ is a constructor of the datatype,
+ $r$ contains only the free variables on the left-hand side, and all
+ recursive calls in $r$ are of the form $f \, \dots \, y@i \, \dots$
+ for some $i$. There must be exactly one reduction rule for each
+ constructor. The order is immaterial. Also note that all reduction
+ rules are added to the default simpset!
- If you would like to refer to some rule explicitly, you have to prefix each
- rule with an identifier (like in the {\tt rules} section of the first {\tt
- Append} theory above) that will serve as the name of the corresponding
- theorem at the \ML\ level.
+If you would like to refer to some rule explicitly, you have to prefix
+each rule with an identifier (like in the {\tt rules} section of the
+axiomatic {\tt Append} theory above) that will serve as the name of
+the corresponding theorem at the \ML\ level.
\end{itemize}
A theory file may contain any number of {\tt primrec} sections which may be
intermixed with other declarations.
-For the consistency-conscious user it may be reassuring to know that {\tt
- primrec} does not assert the reduction rules as new axioms but derives them
-as theorems from an explicit definition of the recursive function in terms of
-a recursion operator on the datatype.
-
The primitive recursive function can have infix or mixfix syntax:
\begin{ttbox}\underscoreon
Append = MyList +
@@ -1829,6 +1853,11 @@
%Nevertheless {\tt tl} is total, although we do not know what the result of
%\verb$tl([])$ is.
+\medskip For the definitionally-minded user it may be reassuring to
+know that {\tt primrec} does not assert the reduction rules as new
+axioms but derives them as theorems from an explicit definition of the
+recursive function in terms of a recursion operator on the datatype.
+
\index{primitive recursion|)}
\index{*primrec|)}
\index{*datatype|)}
@@ -1856,13 +1885,13 @@
proves some theorems. Each definition creates an ML structure, which is a
substructure of the main theory structure.
-This package is derived from the ZF one, described in a
-separate paper,\footnote{It appeared in CADE~\cite{paulson-CADE} and a
- longer version is distributed with Isabelle.} which you should refer to
-in case of difficulties. The package is simpler than ZF's thanks to HOL's
-automatic type-checking. The type of the (co)inductive determines the
-domain of the fixedpoint definition, and the package does not use inference
-rules for type-checking.
+This package is derived from the \ZF\ one, described in a separate
+paper,\footnote{It appeared in CADE~\cite{paulson-CADE}, a longer
+ version is distributed with Isabelle.} which you should refer to in
+case of difficulties. The package is simpler than \ZF's thanks to
+\HOL's automatic type-checking. The type of the (co)inductive
+determines the domain of the fixedpoint definition, and the package
+does not use inference rules for type-checking.
\subsection{The result structure}
@@ -1929,10 +1958,11 @@
{\tt coinductive}.
The {\tt monos} and {\tt con_defs} sections are optional. If present,
-each is specified as a string, which must be a valid ML expression of type
-{\tt thm list}. It is simply inserted into the {\tt .thy.ML} file; if it
-is ill-formed, it will trigger ML error messages. You can then inspect the
-file on your directory.
+each is specified as a string, which must be a valid \ML{} expression
+of type {\tt thm list}. It is simply inserted into the generated
+\ML{} file that is generated from the theory definition; if it is
+ill-formed, it will trigger ML error messages. You can then inspect
+the file on your directory.
\begin{itemize}
\item The {\it inductive sets} are specified by one or more strings.
@@ -1954,9 +1984,9 @@
\begin{itemize}
\item The theory must separately declare the recursive sets as
constants.
-
-\item The names of the recursive sets must be identifiers, not infix
-operators.
+
+\item The names of the recursive sets must be alphanumeric
+ identifiers.
\item Side-conditions must not be conjunctions. However, an introduction rule
may contain any number of side-conditions.
@@ -1974,7 +2004,7 @@
consts Fin :: 'a set => 'a set set
inductive "Fin A"
intrs
- emptyI "\{\} : Fin A"
+ emptyI "{\ttlbrace}{\ttrbrace} : 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}.
@@ -1982,11 +2012,12 @@
and also individually as {\tt Fin.emptyI} and {\tt Fin.consI}. The induction
rule is {\tt Fin.induct}.
-For another example, here is a theory file defining the accessible part of a
-relation. The main thing to note is the use of~{\tt Pow} in the sole
-introduction rule, and the corresponding mention of the rule
-\verb|Pow_mono| in the {\tt monos} list. The paper discusses a ZF version
-of this example in more detail.
+For another example, here is a theory file defining the accessible
+part of a relation. The main thing to note is the use of~{\tt Pow} in
+the sole introduction rule, and the corresponding mention of the rule
+\verb|Pow_mono| in the {\tt monos} list. The paper
+\cite{paulson-CADE} discusses a \ZF\ version of this example in more
+detail.
\begin{ttbox}
Acc = WF +
consts pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*)
@@ -1998,11 +2029,11 @@
monos "[Pow_mono]"
end
\end{ttbox}
-The HOL distribution contains many other inductive definitions. Simple
-examples are collected on subdirectory \texttt{Induct}. The theory {\tt
- HOL/Induct/LList.thy} contains coinductive definitions. Larger examples may
-be found on other subdirectories, such as {\tt IMP}, {\tt Lambda} and {\tt
- Auth}.
+The \HOL{} distribution contains many other inductive definitions.
+Simple examples are collected on subdirectory \texttt{Induct}. The
+theory {\tt HOL/Induct/LList.thy} contains coinductive definitions.
+Larger examples may be found on other subdirectories, such as {\tt
+ IMP}, {\tt Lambda} and {\tt Auth}.
\index{*coinductive|)} \index{*inductive|)}
@@ -2108,7 +2139,7 @@
Cantor's Theorem states that every set has more subsets than it has
elements. It has become a favourite example in higher-order logic since
it is so easily expressed:
-\[ \forall f::[\alpha,\alpha]\To bool. \exists S::\alpha\To bool.
+\[ \forall f::\alpha \To \alpha \To bool. \exists S::\alpha\To bool.
\forall x::\alpha. f~x \not= S
\]
%
@@ -2120,22 +2151,22 @@
the operator \cdx{range}. The set~$S$ is given as an unknown instead of a
quantified variable so that we may inspect the subset found by the proof.
\begin{ttbox}
-goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
+goal Set.thy "?S ~: range\thinspace(f :: 'a=>'a set)";
{\out Level 0}
-{\out ~ ?S : range f}
-{\out 1. ~ ?S : range f}
+{\out ?S ~: range f}
+{\out 1. ?S ~: range f}
\end{ttbox}
The first two steps are routine. The rule \tdx{rangeE} replaces
-$\Var{S}\in {\tt range} f$ by $\Var{S}=f~x$ for some~$x$.
+$\Var{S}\in {\tt range} \, f$ by $\Var{S}=f~x$ for some~$x$.
\begin{ttbox}
by (resolve_tac [notI] 1);
{\out Level 1}
-{\out ~ ?S : range f}
+{\out ?S ~: range f}
{\out 1. ?S : range f ==> False}
\ttbreak
by (eresolve_tac [rangeE] 1);
{\out Level 2}
-{\out ~ ?S : range f}
+{\out ?S ~: range f}
{\out 1. !!x. ?S = f x ==> False}
\end{ttbox}
Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f~x$,
@@ -2144,9 +2175,9 @@
\begin{ttbox}
by (eresolve_tac [equalityCE] 1);
{\out Level 3}
-{\out ~ ?S : range f}
+{\out ?S ~: range f}
{\out 1. !!x. [| ?c3 x : ?S; ?c3 x : f x |] ==> False}
-{\out 2. !!x. [| ~ ?c3 x : ?S; ~ ?c3 x : f x |] ==> False}
+{\out 2. !!x. [| ?c3 x ~: ?S; ?c3 x ~: f x |] ==> False}
\end{ttbox}
Now we use a bit of creativity. Suppose that~$\Var{S}$ has the form of a
comprehension. Then $\Var{c}\in\{x.\Var{P}~x\}$ implies
@@ -2155,30 +2186,30 @@
\begin{ttbox}
by (dresolve_tac [CollectD] 1);
{\out Level 4}
-{\out ~ \{x. ?P7 x\} : range f}
+{\out {\ttlbrace}x. ?P7 x{\ttrbrace} ~: range f}
{\out 1. !!x. [| ?c3 x : f x; ?P7(?c3 x) |] ==> False}
-{\out 2. !!x. [| ~ ?c3 x : \{x. ?P7 x\}; ~ ?c3 x : f x |] ==> False}
+{\out 2. !!x. [| ?c3 x ~: {\ttlbrace}x. ?P7 x{\ttrbrace}; ?c3 x ~: f x |] ==> False}
\end{ttbox}
-Forcing a contradiction between the two assumptions of subgoal~1 completes
-the instantiation of~$S$. It is now the set $\{x. x\not\in f~x\}$, which
-is the standard diagonal construction.
+Forcing a contradiction between the two assumptions of subgoal~1
+completes the instantiation of~$S$. It is now the set $\{x. x\not\in
+f~x\}$, which is the standard diagonal construction.
\begin{ttbox}
by (contr_tac 1);
{\out Level 5}
-{\out ~ \{x. ~ x : f x\} : range f}
-{\out 1. !!x. [| ~ x : \{x. ~ x : f x\}; ~ x : f x |] ==> False}
+{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
+{\out 1. !!x. [| x ~: {\ttlbrace}x. x ~: f x{\ttrbrace}; x ~: f x |] ==> False}
\end{ttbox}
The rest should be easy. To apply \tdx{CollectI} to the negated
assumption, we employ \ttindex{swap_res_tac}:
\begin{ttbox}
by (swap_res_tac [CollectI] 1);
{\out Level 6}
-{\out ~ \{x. ~ x : f x\} : range f}
-{\out 1. !!x. [| ~ x : f x; ~ False |] ==> ~ x : f x}
+{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
+{\out 1. !!x. [| x ~: f x; ~ False |] ==> x ~: f x}
\ttbreak
by (assume_tac 1);
{\out Level 7}
-{\out ~ \{x. ~ x : f x\} : range f}
+{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
{\out No subgoals!}
\end{ttbox}
How much creativity is required? As it happens, Isabelle can prove this
@@ -2191,12 +2222,12 @@
\begin{ttbox}
choplev 0;
{\out Level 0}
-{\out ~ ?S : range f}
-{\out 1. ~ ?S : range f}
+{\out ?S ~: range f}
+{\out 1. ?S ~: range f}
\ttbreak
by (best_tac (!claset addSEs [equalityCE]) 1);
{\out Level 1}
-{\out ~ \{x. ~ x : f x\} : range f}
+{\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f}
{\out No subgoals!}
\end{ttbox}
If you run this example interactively, make sure your current theory contains