diff -r 1471e85624a7 -r bc628f4ef0cb doc-src/Logics/HOL.tex --- 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 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 m mod n = m +\tdx{mod_geq} [| 0 m mod n = (m-n) mod n +\tdx{div_less} m m div n = 0 +\tdx{div_geq} [| 0 m div n = Suc((m-n) div n) +\subcaption{Recursion equations} \tdx{less_trans} [| i i 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}.