--- a/doc-src/Logics/CHOL.tex Tue Mar 30 13:17:55 1999 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1897 +0,0 @@
-%% $Id$
-\chapter{Higher-Order Logic}
-\index{higher-order logic|(}
-\index{HOL system@{\sc hol} system}
-
-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 useful for hardware verification;
-beyond this, it is widely applicable in many areas of mathematics. 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 Isabelle's \HOL\ has recently been changed to look more like the
-traditional syntax of higher-order logic. Function application is now
-curried. To apply the function~$f$ to the arguments~$a$ and~$b$ in \HOL, you
-must write $f\,a\,b$. Note that $f(a,b)$ means ``$f$ applied to the pair
-$(a,b)$'' in \HOL. We write ordered pairs as $(a,b)$, not $\langle
-a,b\rangle$ as in {\ZF} and earlier versions of \HOL. Early releases of
-Isabelle included still another version of~\HOL, with explicit type inference
-rules~\cite{paulson-COLOG}. This version no longer exists, but \thydx{ZF}
-supports a similar style of reasoning.
-
-\HOL\ has a distinct feel, compared with {\ZF} and {\CTT}. It
-identifies object-level types with meta-level types, taking advantage of
-Isabelle's built-in type checker. It identifies object-level functions
-with meta-level functions, so it uses Isabelle's operations for abstraction
-and application. There is no `apply' operator: function applications are
-written as simply~$f~a$ rather than $f{\tt`}a$.
-
-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}. Gain experience by
-working in first-order logic before attempting to use higher-order logic.
-This chapter assumes familiarity with~{\FOL{}}.
-
-
-\begin{figure}
-\begin{center}
-\begin{tabular}{rrr}
- \it name &\it meta-type & \it description \\
- \cdx{Trueprop}& $bool\To prop$ & coercion to $prop$\\
- \cdx{not} & $bool\To bool$ & negation ($\neg$) \\
- \cdx{True} & $bool$ & tautology ($\top$) \\
- \cdx{False} & $bool$ & absurdity ($\bot$) \\
- \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}
-\subcaption{Constants}
-
-\begin{center}
-\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$) \\
- {\tt!~} or \sdx{ALL} & \cdx{All} & $(\alpha::term\To bool)\To bool$ &
- universal quantifier ($\forall$) \\
- {\tt?~} or \sdx{EX} & \cdx{Ex} & $(\alpha::term\To bool)\To bool$ &
- existential quantifier ($\exists$) \\
- {\tt?!} or {\tt EX!} & \cdx{Ex1} & $(\alpha::term\To bool)\To bool$ &
- unique existence ($\exists!$)
-\end{tabular}
-\end{center}
-\subcaption{Binders}
-
-\begin{center}
-\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)$ &
- Right 50 & composition ($\circ$) \\
- \tt = & $[\alpha::term,\alpha]\To bool$ & Left 50 & equality ($=$) \\
- \tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\
- \tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 &
- less than or equals ($\leq$)\\
- \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}
-\subcaption{Infixes}
-\caption{Syntax of {\tt HOL}} \label{hol-constants}
-\end{figure}
-
-
-\begin{figure}
-\index{*let symbol}
-\index{*in symbol}
-\dquotes
-\[\begin{array}{rclcl}
- term & = & \hbox{expression of class~$term$} \\
- & | & "\at~" id~id^* " . " formula \\
- & | &
- \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\
- & | &
- \multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\[2ex]
- formula & = & \hbox{expression of type~$bool$} \\
- & | & term " = " term \\
- & | & term " \ttilde= " term \\
- & | & term " < " term \\
- & | & term " <= " term \\
- & | & "\ttilde\ " formula \\
- & | & formula " \& " formula \\
- & | & formula " | " formula \\
- & | & formula " --> " formula \\
- & | & "!~~~" id~id^* " . " formula
- & | & "ALL~" id~id^* " . " formula \\
- & | & "?~~~" id~id^* " . " formula
- & | & "EX~~" id~id^* " . " formula \\
- & | & "?!~~" id~id^* " . " formula
- & | & "EX!~" id~id^* " . " formula
- \end{array}
-\]
-\caption{Full grammar for \HOL} \label{hol-grammar}
-\end{figure}
-
-
-\section{Syntax}
-The type class of higher-order terms is called~\cldx{term}. Type variables
-range over this class by default. The equality symbol and quantifiers are
-polymorphic over class {\tt term}.
-
-Class \cldx{ord} consists of all ordered types; the relations $<$ and
-$\leq$ are polymorphic over this class, as are the functions
-\cdx{mono}, \cdx{min} and \cdx{max}. Three other
-type classes --- \cldx{plus}, \cldx{minus} and \cldx{times} --- permit
-overloading of the operators {\tt+}, {\tt-} and {\tt*}. In particular,
-{\tt-} is overloaded for set difference and subtraction.
-\index{*"+ symbol}
-\index{*"- symbol}
-\index{*"* symbol}
-
-Figure~\ref{hol-constants} lists the constants (including infixes and
-binders), while Fig.\ts\ref{hol-grammar} presents the grammar of
-higher-order logic. Note that $a$\verb|~=|$b$ is translated to
-$\neg(a=b)$.
-
-\begin{warn}
- \HOL\ has no if-and-only-if connective; logical equivalence is expressed
- using equality. But equality has a high priority, as befitting a
- relation, while if-and-only-if typically has the lowest priority. Thus,
- $\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.
- When using $=$ to mean logical equivalence, enclose both operands in
- parentheses.
-\end{warn}
-
-\subsection{Types}\label{hol-types}
-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.
-
-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.
-
-
-\subsection{Binders}
-Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$
-satisfying~$P[a]$, if such exists. Since all terms in \HOL\ denote
-something, a description is always meaningful, but we do not know its value
-unless $P[x]$ defines it uniquely. We may write descriptions as
-\cdx{Eps}($P$) or use the syntax
-\hbox{\tt \at $x$.$P[x]$}.
-
-Existential quantification is defined by
-\[ \exists x.P~x \;\equiv\; P(\epsilon x.P~x). \]
-The unique existence quantifier, $\exists!x.P[x]$, is defined in terms
-of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested
-quantifications. For instance, $\exists!x y.P~x~y$ abbreviates
-$\exists!x. \exists!y.P~x~y$; note that this does not mean that there
-exists a unique pair $(x,y)$ satisfying~$P~x~y$.
-
-\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system}
-Quantifiers have two notations. As in Gordon's {\sc hol} system, \HOL\
-uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$. The
-existential quantifier must be followed by a space; thus {\tt?x} is an
-unknown, while \verb'? x.f x=y' is a quantification. Isabelle's usual
-notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also
-available. Both notations are accepted for input. The {\ML} reference
-\ttindexbold{HOL_quantifiers} governs the output notation. If set to {\tt
-true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set
-to {\tt false}, then~{\tt ALL} and~{\tt EX} are displayed.
-
-All these binders have priority 10.
-
-
-\subsection{The \sdx{let} and \sdx{case} constructions}
-Local abbreviations can be introduced by a {\tt let} construct whose
-syntax appears in Fig.\ts\ref{hol-grammar}. Internally it is translated into
-the constant~\cdx{Let}. It can be expanded by rewriting with its
-definition, \tdx{Let_def}.
-
-\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.
-
-\begin{figure}
-\begin{ttbox}\makeatother
-\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::'a) ==> P(@x.P x)
-\tdx{True_or_False} (P=True) | (P=False)
-\end{ttbox}
-\caption{The {\tt HOL} rules} \label{hol-rules}
-\end{figure}
-
-
-\begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message
-\begin{ttbox}\makeatother
-\tdx{True_def} True == ((\%x::bool.x)=(\%x.x))
-\tdx{All_def} All == (\%P. P = (\%x.True))
-\tdx{Ex_def} Ex == (\%P. P(@x.P x))
-\tdx{False_def} False == (!P.P)
-\tdx{not_def} not == (\%P. P-->False)
-\tdx{and_def} op & == (\%P Q. !R. (P-->Q-->R) --> R)
-\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{Inv_def} Inv == (\%(f::'a=>'b) y. @x. f x=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
-\end{ttbox}
-\caption{The {\tt HOL} definitions} \label{hol-defs}
-\end{figure}
-
-
-\section{Rules of inference}
-Figure~\ref{hol-rules} shows the inference rules of~\HOL{}, with
-their~{\ML} names. Some of the rules deserve additional comments:
-\begin{ttdescription}
-\item[\tdx{ext}] expresses extensionality of functions.
-\item[\tdx{iff}] asserts that logically equivalent formulae are
- equal.
-\item[\tdx{selectI}] gives the defining property of the Hilbert
- $\epsilon$-operator. It is a form of the Axiom of Choice. The derived rule
- \tdx{select_equality} (see below) is often easier to use.
-\item[\tdx{True_or_False}] makes the logic classical.\footnote{In
- fact, the $\epsilon$-operator already makes the logic classical, as
- shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}
-\end{ttdescription}
-
-\HOL{} follows standard practice in higher-order logic: only a few
-connectives are taken as primitive, with the remainder defined obscurely
-(Fig.\ts\ref{hol-defs}). Gordon's {\sc hol} system expresses the
-corresponding definitions \cite[page~270]{mgordon-hol} using
-object-equality~({\tt=}), which is possible because equality in
-higher-order logic may equate formulae and even functions over formulae.
-But theory~\HOL{}, like all other Isabelle theories, uses
-meta-equality~({\tt==}) for definitions.
-
-Some of the rules mention type variables; for example, {\tt refl}
-mentions the type variable~{\tt'a}. This allows you to instantiate
-type variables explicitly by calling {\tt res_inst_tac}. By default,
-explicit type variables have class \cldx{term}.
-
-Include type constraints whenever you state a polymorphic goal. Type
-inference may otherwise make the goal more polymorphic than you intended,
-with confusing results.
-
-\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.
-
- \index{unification!incompleteness of}
- Where function types are involved, Isabelle's unification code does not
- guarantee to find instantiations for type variables automatically. Be
- prepared to use \ttindex{res_inst_tac} instead of {\tt resolve_tac},
- possibly instantiating type variables. Setting
- \ttindex{Unify.trace_types} to {\tt true} causes Isabelle to report
- omitted search paths during unification.\index{tracing!of unification}
-\end{warn}
-
-
-\begin{figure}
-\begin{ttbox}
-\tdx{sym} s=t ==> t=s
-\tdx{trans} [| r=s; s=t |] ==> r=t
-\tdx{ssubst} [| t=s; P s |] ==> P(t::'a)
-\tdx{box_equals} [| a=b; a=c; b=d |] ==> c=d
-\tdx{arg_cong} x=y ==> f x=f y
-\tdx{fun_cong} f=g ==> f x=g x
-\subcaption{Equality}
-
-\tdx{TrueI} True
-\tdx{FalseE} False ==> P
-
-\tdx{conjI} [| P; Q |] ==> P&Q
-\tdx{conjunct1} [| P&Q |] ==> P
-\tdx{conjunct2} [| P&Q |] ==> Q
-\tdx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R
-
-\tdx{disjI1} P ==> P|Q
-\tdx{disjI2} Q ==> P|Q
-\tdx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R
-
-\tdx{notI} (P ==> False) ==> ~ P
-\tdx{notE} [| ~ P; P |] ==> R
-\tdx{impE} [| P-->Q; P; Q ==> R |] ==> R
-\subcaption{Propositional logic}
-
-\tdx{iffI} [| P ==> Q; Q ==> P |] ==> P=Q
-\tdx{iffD1} [| P=Q; P |] ==> Q
-\tdx{iffD2} [| P=Q; Q |] ==> P
-\tdx{iffE} [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
-
-\tdx{eqTrueI} P ==> P=True
-\tdx{eqTrueE} P=True ==> P
-\subcaption{Logical equivalence}
-
-\end{ttbox}
-\caption{Derived rules for \HOL} \label{hol-lemmas1}
-\end{figure}
-
-
-\begin{figure}
-\begin{ttbox}\makeatother
-\tdx{allI} (!!x::'a. P x) ==> !x. P x
-\tdx{spec} !x::'a.P x ==> P x
-\tdx{allE} [| !x.P x; P x ==> R |] ==> R
-\tdx{all_dupE} [| !x.P x; [| P x; !x.P x |] ==> R |] ==> R
-
-\tdx{exI} P x ==> ? x::'a.P x
-\tdx{exE} [| ? x::'a.P x; !!x. P x ==> Q |] ==> Q
-
-\tdx{ex1I} [| P a; !!x. P x ==> x=a |] ==> ?! x. P x
-\tdx{ex1E} [| ?! x.P x; !!x. [| P x; ! y. P y --> y=x |] ==> R
- |] ==> R
-
-\tdx{select_equality} [| P a; !!x. P x ==> x=a |] ==> (@x.P x) = a
-\subcaption{Quantifiers and descriptions}
-
-\tdx{ccontr} (~P ==> False) ==> P
-\tdx{classical} (~P ==> P) ==> P
-\tdx{excluded_middle} ~P | P
-
-\tdx{disjCI} (~Q ==> P) ==> P|Q
-\tdx{exCI} (! x. ~ P x ==> P a) ==> ? x.P x
-\tdx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R
-\tdx{iffCE} [| P=Q; [| P;Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R
-\tdx{notnotD} ~~P ==> P
-\tdx{swap} ~P ==> (~Q ==> P) ==> Q
-\subcaption{Classical logic}
-
-\tdx{if_True} (if True then x else y) = x
-\tdx{if_False} (if False then x else y) = y
-\tdx{if_P} P ==> (if P then x else y) = x
-\tdx{if_not_P} ~ P ==> (if P then x else y) = y
-\tdx{expand_if} P(if Q then x else y) = ((Q --> P x) & (~Q --> P y))
-\subcaption{Conditionals}
-\end{ttbox}
-\caption{More derived rules} \label{hol-lemmas2}
-\end{figure}
-
-
-Some derived rules are shown in Figures~\ref{hol-lemmas1}
-and~\ref{hol-lemmas2}, with their {\ML} names. These include natural rules
-for the logical connectives, as well as sequent-style elimination rules for
-conjunctions, implications, and universal quantifiers.
-
-Note the equality rules: \tdx{ssubst} performs substitution in
-backward proofs, while \tdx{box_equals} supports reasoning by
-simplifying both sides of an equation.
-
-
-\begin{figure}
-\begin{center}
-\begin{tabular}{rrr}
- \it name &\it meta-type & \it description \\
-\index{{}@\verb'{}' symbol}
- \verb|{}| & $\alpha\,set$ & the empty set \\
- \cdx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$
- & insertion of element \\
- \cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$
- & comprehension \\
- \cdx{Compl} & $(\alpha\,set)\To\alpha\,set$
- & complement \\
- \cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
- & intersection over a set\\
- \cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
- & union over a set\\
- \cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$
- &set of sets intersection \\
- \cdx{Union} & $(\alpha\,set)set\To\alpha\,set$
- &set of sets union \\
- \cdx{Pow} & $\alpha\,set \To (\alpha\,set)set$
- & powerset \\[1ex]
- \cdx{range} & $(\alpha\To\beta )\To\beta\,set$
- & range of a function \\[1ex]
- \cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$
- & bounded quantifiers \\
- \cdx{mono} & $(\alpha\,set\To\beta\,set)\To bool$
- & monotonicity \\
- \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$
- & injective/surjective \\
- \cdx{inj_onto} & $[\alpha\To\beta ,\alpha\,set]\To bool$
- & injective over subset
-\end{tabular}
-\end{center}
-\subcaption{Constants}
-
-\begin{center}
-\begin{tabular}{llrrr}
- \it symbol &\it name &\it meta-type & \it priority & \it description \\
- \sdx{INT} & \cdx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
- intersection over a type\\
- \sdx{UN} & \cdx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
- union over a type
-\end{tabular}
-\end{center}
-\subcaption{Binders}
-
-\begin{center}
-\index{*"`"` symbol}
-\index{*": symbol}
-\index{*"<"= symbol}
-\begin{tabular}{rrrr}
- \it symbol & \it meta-type & \it priority & \it description \\
- \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$) \\
- \sdx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
- & Left 65 & union ($\union$) \\
- \tt: & $[\alpha ,\alpha\,set]\To bool$
- & Left 50 & membership ($\in$) \\
- \tt <= & $[\alpha\,set,\alpha\,set]\To bool$
- & Left 50 & subset ($\subseteq$)
-\end{tabular}
-\end{center}
-\subcaption{Infixes}
-\caption{Syntax of the theory {\tt Set}} \label{hol-set-syntax}
-\end{figure}
-
-
-\begin{figure}
-\begin{center} \tt\frenchspacing
-\index{*"! symbol}
-\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]$) &
- \rm comprehension \\
- \sdx{INT} $x$:$A$.$B[x]$ & INTER $A$ $\lambda x.B[x]$ &
- \rm intersection \\
- \sdx{UN}{\tt\ } $x$:$A$.$B[x]$ & UNION $A$ $\lambda x.B[x]$ &
- \rm union \\
- \tt ! $x$:$A$.$P[x]$ or \sdx{ALL} $x$:$A$.$P[x]$ &
- Ball $A$ $\lambda x.P[x]$ &
- \rm bounded $\forall$ \\
- \sdx{?} $x$:$A$.$P[x]$ or \sdx{EX}{\tt\ } $x$:$A$.$P[x]$ &
- Bex $A$ $\lambda x.P[x]$ & \rm bounded $\exists$
-\end{tabular}
-\end{center}
-\subcaption{Translations}
-
-\dquotes
-\[\begin{array}{rclcl}
- term & = & \hbox{other terms\ldots} \\
- & | & "\{\}" \\
- & | & "\{ " term\; ("," term)^* " \}" \\
- & | & "\{ " id " . " formula " \}" \\
- & | & term " `` " term \\
- & | & term " Int " term \\
- & | & term " Un " term \\
- & | & "INT~~" id ":" term " . " term \\
- & | & "UN~~~" id ":" term " . " term \\
- & | & "INT~~" id~id^* " . " term \\
- & | & "UN~~~" id~id^* " . " term \\[2ex]
- formula & = & \hbox{other formulae\ldots} \\
- & | & term " : " term \\
- & | & term " \ttilde: " term \\
- & | & term " <= " term \\
- & | & "!~" id ":" term " . " formula
- & | & "ALL " id ":" term " . " formula \\
- & | & "?~" id ":" term " . " formula
- & | & "EX~~" id ":" term " . " formula
- \end{array}
-\]
-\subcaption{Full Grammar}
-\caption{Syntax of the theory {\tt Set} (continued)} \label{hol-set-syntax2}
-\end{figure}
-
-
-\section{A formulation of set theory}
-Historically, higher-order logic gives a foundation for Russell and
-Whitehead's theory of classes. Let us use modern terminology and call them
-{\bf sets}, but note that these sets are distinct from those of {\ZF} set
-theory, and behave more like {\ZF} classes.
-\begin{itemize}
-\item
-Sets are given by predicates over some type~$\sigma$. Types serve to
-define universes for sets, but type checking is still significant.
-\item
-There is a universal set (for each type). Thus, sets have complements, and
-may be defined by absolute comprehension.
-\item
-Although sets may contain other sets as elements, the containing set must
-have a more complex type.
-\end{itemize}
-Finite unions and intersections have the same behaviour in \HOL\ as they
-do in~{\ZF}. In \HOL\ the intersection of the empty set is well-defined,
-denoting the universal set for the given type.
-
-
-\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
-clarity and to avoid complications involving function types in unification.
-Since Isabelle does not support type definitions (as mentioned in
-\S\ref{hol-types}), the isomorphisms between the two types are declared
-explicitly. Here they are natural: {\tt Collect} maps $\alpha\To bool$ to
-$\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring
-argument order).
-
-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
-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~$\{\}$:
-\begin{eqnarray*}
- \{a@1, \ldots, a@n\} & \equiv &
- {\tt insert}~a@1~({\tt insert}\ldots({\tt insert}~a@n~\{\})\ldots)
-\end{eqnarray*}
-
-The set \hbox{\tt\{$x$.$P[x]$\}} 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
-in~{\ZF}; the type of~$x$ implicitly restricts the comprehension.
-
-The set theory defines two {\bf bounded quantifiers}:
-\begin{eqnarray*}
- \forall x\in A.P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\
- \exists x\in A.P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x]
-\end{eqnarray*}
-The constants~\cdx{Ball} and~\cdx{Bex} are defined
-accordingly. Instead of {\tt Ball $A$ $P$} and {\tt Bex $A$ $P$} we may
-write\index{*"! symbol}\index{*"? symbol}
-\index{*ALL symbol}\index{*EX symbol}
-%
-\hbox{\tt !~$x$:$A$.$P[x]$} and \hbox{\tt ?~$x$:$A$.$P[x]$}. Isabelle's
-usual quantifier symbols, \sdx{ALL} and \sdx{EX}, are also accepted
-for input. As with the primitive quantifiers, the {\ML} reference
-\ttindex{HOL_quantifiers} specifies which notation to use for output.
-
-Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and
-$\bigcap@{x\in A}B[x]$, are written
-\sdx{UN}~\hbox{\tt$x$:$A$.$B[x]$} and
-\sdx{INT}~\hbox{\tt$x$:$A$.$B[x]$}.
-
-Unions and intersections over types, namely $\bigcup@x B[x]$ and $\bigcap@x
-B[x]$, are written \sdx{UN}~\hbox{\tt$x$.$B[x]$} and
-\sdx{INT}~\hbox{\tt$x$.$B[x]$}. They are equivalent to the previous
-union and intersection operators when $A$ is the universal set.
-
-The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets. They are
-not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$,
-respectively.
-
-
-\begin{figure} \underscoreon
-\begin{ttbox}
-\tdx{mem_Collect_eq} (a : \{x.P x\}) = P a
-\tdx{Collect_mem_eq} \{x.x:A\} = A
-
-\tdx{empty_def} \{\} == \{x.False\}
-\tdx{insert_def} insert a B == \{x.x=a\} 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{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{mono_def} mono f == !A B. A <= B --> f A <= f B
-\tdx{inj_def} inj f == ! x y. f x=f y --> x=y
-\tdx{surj_def} surj f == ! y. ? x. y=f x
-\tdx{inj_onto_def} inj_onto f A == !x:A. !y:A. f x=f y --> x=y
-\end{ttbox}
-\caption{Rules of the theory {\tt Set}} \label{hol-set-rules}
-\end{figure}
-
-
-\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{ballI} [| !!x. x:A ==> P x |] ==> ! x:A. P x
-\tdx{bspec} [| ! x:A. P x; x:A |] ==> P x
-\tdx{ballE} [| ! x:A. P x; P x ==> Q; ~ x:A ==> Q |] ==> Q
-
-\tdx{bexI} [| P x; x:A |] ==> ? x:A. P x
-\tdx{bexCI} [| ! x:A. ~ P x ==> P a; a:A |] ==> ? x:A.P x
-\tdx{bexE} [| ? x:A. P x; !!x. [| x:A; P x |] ==> Q |] ==> Q
-\subcaption{Comprehension and Bounded quantifiers}
-
-\tdx{subsetI} (!!x.x:A ==> x:B) ==> A <= B
-\tdx{subsetD} [| A <= B; c:A |] ==> c:B
-\tdx{subsetCE} [| A <= B; ~ (c:A) ==> P; c:B ==> P |] ==> P
-
-\tdx{subset_refl} A <= A
-\tdx{subset_trans} [| A<=B; B<=C |] ==> A<=C
-
-\tdx{equalityI} [| A <= B; B <= A |] ==> A = B
-\tdx{equalityD1} A = B ==> A<=B
-\tdx{equalityD2} A = B ==> B<=A
-\tdx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P
-
-\tdx{equalityCE} [| A = B; [| c:A; c:B |] ==> P;
- [| ~ c:A; ~ c:B |] ==> P
- |] ==> P
-\subcaption{The subset and equality relations}
-\end{ttbox}
-\caption{Derived rules for set theory} \label{hol-set1}
-\end{figure}
-
-
-\begin{figure} \underscoreon
-\begin{ttbox}
-\tdx{emptyE} a : \{\} ==> P
-
-\tdx{insertI1} a : insert a B
-\tdx{insertI2} a : B ==> a : insert b B
-\tdx{insertE} [| a : insert b A; a=b ==> P; a:A ==> P |] ==> P
-
-\tdx{ComplI} [| c:A ==> False |] ==> c : Compl A
-\tdx{ComplD} [| c : Compl A |] ==> ~ c:A
-
-\tdx{UnI1} c:A ==> c : A Un B
-\tdx{UnI2} c:B ==> c : A Un B
-\tdx{UnCI} (~c:B ==> c:A) ==> c : A Un B
-\tdx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P
-
-\tdx{IntI} [| c:A; c:B |] ==> c : A Int B
-\tdx{IntD1} c : A Int B ==> c:A
-\tdx{IntD2} c : A Int B ==> c:B
-\tdx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P
-
-\tdx{UN_I} [| a:A; b: B a |] ==> b: (UN x:A. B x)
-\tdx{UN_E} [| b: (UN x:A. B x); !!x.[| x:A; b:B x |] ==> R |] ==> R
-
-\tdx{INT_I} (!!x. x:A ==> b: B x) ==> b : (INT x:A. B x)
-\tdx{INT_D} [| b: (INT x:A. B x); a:A |] ==> b: B a
-\tdx{INT_E} [| b: (INT x:A. B x); b: B a ==> R; ~ a:A ==> R |] ==> R
-
-\tdx{UnionI} [| X:C; A:X |] ==> A : Union C
-\tdx{UnionE} [| A : Union C; !!X.[| A:X; X:C |] ==> R |] ==> R
-
-\tdx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter C
-\tdx{InterD} [| A : Inter C; X:C |] ==> A:X
-\tdx{InterE} [| A : Inter C; A:X ==> R; ~ X:C ==> R |] ==> R
-
-\tdx{PowI} A<=B ==> A: Pow B
-\tdx{PowD} A: Pow B ==> A<=B
-\end{ttbox}
-\caption{Further derived rules for set theory} \label{hol-set2}
-\end{figure}
-
-
-\subsection{Axioms and rules of set theory}
-Figure~\ref{hol-set-rules} presents the rules of theory \thydx{Set}. The
-axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert
-that the functions {\tt Collect} and \hbox{\tt op :} are isomorphisms. Of
-course, \hbox{\tt op :} also serves as the membership relation.
-
-All the other axioms are definitions. They include the empty set, bounded
-quantifiers, unions, intersections, complements and the subset relation.
-They also include straightforward properties of functions: image~({\tt``}) and
-{\tt range}, and predicates concerning monotonicity, injectiveness and
-surjectiveness.
-
-The predicate \cdx{inj_onto} is used for simulating type definitions.
-The statement ${\tt inj_onto}~f~A$ asserts that $f$ is injective on the
-set~$A$, which specifies a subset of its domain type. In a type
-definition, $f$ is the abstraction function and $A$ is the set of valid
-representations; we should not expect $f$ to be injective outside of~$A$.
-
-\begin{figure} \underscoreon
-\begin{ttbox}
-\tdx{Inv_f_f} inj f ==> Inv f (f x) = x
-\tdx{f_Inv_f} y : range f ==> f(Inv f y) = y
-
-%\tdx{Inv_injective}
-% [| Inv f x=Inv f y; x: range f; y: range f |] ==> x=y
-%
-\tdx{imageI} [| x:A |] ==> f x : f``A
-\tdx{imageE} [| b : f``A; !!x.[| b=f x; x:A |] ==> P |] ==> P
-
-\tdx{rangeI} f x : range f
-\tdx{rangeE} [| b : range f; !!x.[| b=f x |] ==> P |] ==> P
-
-\tdx{monoI} [| !!A B. A <= B ==> f A <= f B |] ==> mono f
-\tdx{monoD} [| mono f; A <= B |] ==> f A <= f B
-
-\tdx{injI} [| !! x y. f x = f y ==> x=y |] ==> inj f
-\tdx{inj_inverseI} (!!x. g(f x) = x) ==> inj f
-\tdx{injD} [| inj f; f x = f y |] ==> x=y
-
-\tdx{inj_ontoI} (!!x y. [| f x=f y; x:A; y:A |] ==> x=y) ==> inj_onto f A
-\tdx{inj_ontoD} [| inj_onto f A; f x=f y; x:A; y:A |] ==> x=y
-
-\tdx{inj_onto_inverseI}
- (!!x. x:A ==> g(f x) = x) ==> inj_onto f A
-\tdx{inj_onto_contraD}
- [| inj_onto f A; x~=y; x:A; y:A |] ==> ~ f x=f y
-\end{ttbox}
-\caption{Derived rules involving functions} \label{hol-fun}
-\end{figure}
-
-
-\begin{figure} \underscoreon
-\begin{ttbox}
-\tdx{Union_upper} B:A ==> B <= Union A
-\tdx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union A <= C
-
-\tdx{Inter_lower} B:A ==> Inter A <= B
-\tdx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter A
-
-\tdx{Un_upper1} A <= A Un B
-\tdx{Un_upper2} B <= A Un B
-\tdx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C
-
-\tdx{Int_lower1} A Int B <= A
-\tdx{Int_lower2} A Int B <= B
-\tdx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B
-\end{ttbox}
-\caption{Derived rules involving subsets} \label{hol-subset}
-\end{figure}
-
-
-\begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message
-\begin{ttbox}
-\tdx{Int_absorb} A Int A = A
-\tdx{Int_commute} A Int B = B Int A
-\tdx{Int_assoc} (A Int B) Int C = A Int (B Int C)
-\tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)
-
-\tdx{Un_absorb} A Un A = A
-\tdx{Un_commute} A Un B = B Un A
-\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{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)
-
-\tdx{Union_Un_distrib} Union(A Un B) = (Union A) Un (Union B)
-\tdx{Int_Union} A Int (Union B) = (UN C:B. A Int C)
-\tdx{Un_Union_image} (UN x:C.(A x) Un (B x)) = Union(A``C) Un Union(B``C)
-
-\tdx{Inter_Un_distrib} Inter(A Un B) = (Inter A) Int (Inter B)
-\tdx{Un_Inter} A Un (Inter B) = (INT C:B. A Un C)
-\tdx{Int_Inter_image} (INT x:C.(A x) Int (B x)) = Inter(A``C) Int Inter(B``C)
-\end{ttbox}
-\caption{Set equalities} \label{hol-equalities}
-\end{figure}
-
-
-Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most are
-obvious and resemble rules of Isabelle's {\ZF} set theory. Certain rules,
-such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},
-are designed for classical reasoning; the rules \tdx{subsetD},
-\tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not
-strictly necessary but yield more natural proofs. Similarly,
-\tdx{equalityCE} supports classical reasoning about extensionality,
-after the fashion of \tdx{iffCE}. See the file {\tt HOL/Set.ML} for
-proofs pertaining to set theory.
-
-Figure~\ref{hol-fun} presents derived inference rules involving functions.
-They also include rules for \cdx{Inv}, which is defined in theory~{\tt
- HOL}; note that ${\tt Inv}~f$ applies the Axiom of Choice to yield an
-inverse of~$f$. They also include natural deduction rules for the image
-and range operators, and for the predicates {\tt inj} and {\tt inj_onto}.
-Reasoning about function composition (the operator~\sdx{o}) and the
-predicate~\cdx{surj} is done simply by expanding the definitions. See
-the file {\tt HOL/fun.ML} for a complete listing of the derived rules.
-
-Figure~\ref{hol-subset} presents lattice properties of the subset relation.
-Unions form least upper bounds; non-empty intersections form greatest lower
-bounds. Reasoning directly about subsets often yields clearer proofs than
-reasoning about the membership relation. See the file {\tt HOL/subset.ML}.
-
-Figure~\ref{hol-equalities} presents many common set equalities. They
-include commutative, associative and distributive laws involving unions,
-intersections and complements. The proofs are mostly trivial, using the
-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}
-\HOL\ instantiates most of Isabelle's generic packages;
-see {\tt HOL/ROOT.ML} for details.
-\begin{itemize}
-\item
-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
-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}
-\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.
-
-The classical reasoner is set up as the structure
-{\tt Classical}. This structure is open, so {\ML} identifiers such
-as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.
-\HOL\ defines the following classical rule sets:
-\begin{ttbox}
-prop_cs : claset
-HOL_cs : claset
-set_cs : claset
-\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{prop_cs}] contains the propositional rules, namely
-those for~$\top$, $\bot$, $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$,
-along with the rule~{\tt refl}.
-
-\item[\ttindexbold{HOL_cs}] extends {\tt prop_cs} with the safe rules
- {\tt allI} and~{\tt exE} and the unsafe rules {\tt allE}
- and~{\tt exI}, as well as rules for unique existence. Search using
- this classical set is incomplete: quantified formulae are used at most
- once.
-
-\item[\ttindexbold{set_cs}] extends {\tt HOL_cs} with rules for the bounded
- quantifiers, subsets, comprehensions, unions and intersections,
- complements, finite sets, images and ranges.
-\end{ttdescription}
-\noindent
-See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%
- {Chap.\ts\ref{chap:classical}}
-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.
-
-\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.
-
-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}.
-
-\begin{figure}
-\index{*"< symbol}
-\index{*"* symbol}
-\index{*div symbol}
-\index{*mod symbol}
-\index{*"+ symbol}
-\index{*"- symbol}
-\begin{constants}
- \it symbol & \it meta-type & \it priority & \it description \\
- \cdx{0} & $nat$ & & zero \\
- \cdx{Suc} & $nat \To nat$ & & successor function\\
- \cdx{nat_case} & $[\alpha, nat\To\alpha, nat] \To\alpha$
- & & 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\\
- \tt + & $[nat,nat]\To nat$ & Left 65 & addition\\
- \tt - & $[nat,nat]\To nat$ & Left 65 & subtraction
-\end{constants}
-\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}
-
-\tdx{pred_natI} (n, Suc n) : pred_nat
-\tdx{pred_natE}
- [| p : pred_nat; !!x n. [| p = (n, Suc n) |] ==> R |] ==> R
-
-\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{less_trans} [| i<j; j<k |] ==> i<k
-\tdx{lessI} n < Suc n
-\tdx{zero_less_Suc} 0 < Suc n
-
-\tdx{less_not_sym} n<m --> ~ m<n
-\tdx{less_not_refl} ~ n<n
-\tdx{not_less0} ~ n<0
-
-\tdx{Suc_less_eq} (Suc m < Suc n) = (m<n)
-\tdx{less_induct} [| !!n. [| ! m. m<n --> P m |] ==> P n |] ==> P n
-
-\tdx{less_linear} m<n | m=n | n<m
-\subcaption{The less-than relation}
-\end{ttbox}
-\caption{Derived rules for {\tt nat}} \label{hol-nat2}
-\end{figure}
-
-
-\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.
-
-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$.
-
-Theory \thydx{Arith} develops arithmetic on the natural numbers. It
-defines addition, multiplication, subtraction, division, and remainder.
-Many of their properties are proved: commutative, associative and
-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 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$.
-
-\begin{figure}
-\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,\alpha list]\To \alpha list$ & Right 65 &
- list constructor \\
- \cdx{null} & $\alpha list \To bool$ & & emptiness test\\
- \cdx{hd} & $\alpha list \To \alpha$ & & head \\
- \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
-\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$ &
- \rm list comprehension
-\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
-
-\tdx{hd_Cons} hd (x#xs) = x
-\tdx{tl_Cons} tl (x#xs) = xs
-
-\tdx{ttl_Nil} ttl [] = []
-\tdx{ttl_Cons} ttl (x#xs) = xs
-
-\tdx{append_Nil} [] @ ys = ys
-\tdx{append_Cons} (x#xs) \at ys = x # xs \at ys
-
-\tdx{mem_Nil} x mem [] = False
-\tdx{mem_Cons} x mem (y#ys) = (if y=x then True else x mem ys)
-
-\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)
-\end{ttbox}
-\caption{Rewrite rules for lists} \label{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.
-
-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$.
-
-
-\section{Datatype declarations}
-\index{*datatype|(}
-
-\underscoreon
-
-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} represents a compact way of doing this.
-
-
-\subsection{Foundations}
-
-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}
-\]
-where $\alpha_i$ are type variables, $C_i$ are distinct constructor names and
-$\tau_{ij}$ are 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.}
-\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). \]
-
-The constructors are automatically defined as functions of their respective
-type:
-\[ C_j : [\tau_{j1},\dots,\tau_{jk_j}] \To (\alpha_1,\dots,\alpha_n)t \]
-These functions have certain {\em freeness} properties:
-\begin{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}
-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 4. In that case every constructor 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}
-\]
-and distinctness of constructors is expressed by:
-\[
-\mbox{\it t\_ord}~x \neq \mbox{\it t\_ord}~y \Imp x \neq y.
-\]
-In addition a structural induction axiom {\tt induct} is provided:
-\[
-\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}) \\
- & \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})
-\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
-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 \\
- \vdots \\
- \mid & C_m~x_{m1}~\dots~x_{mk_m} & \To & e_m
-\end{array}
-\]
-In contrast to \ML, {\em all} constructors must be present, their order is
-fixed, and nested patterns are not supported.
-
-
-\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.
-
-\begin{figure}
-\begin{rail}
-typedecl : typevarlist id '=' (cons + '|')
- ;
-cons : (id | string) ( () | '(' (typ + ',') ')' ) ( () | mixfix )
- ;
-typ : typevarlist id
- | tid
- ;
-typevarlist : () | tid | '(' (tid + ',') ')'
- ;
-\end{rail}
-\caption{Syntax of datatype declarations}
-\label{datatype-grammar}
-\end{figure}
-
-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:
-\begin{ttbox}
-val distinct : thm list
-val inject : thm list
-val induct : thm
-val cases : thm list
-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.
-\begin{warn}
- If there are five or more constructors, the {\em t\_ord} scheme is used for
- {\tt distinct}. In this case the theory {\tt Arith} must be contained
- in the current theory, if necessary by including it explicitly.
-\end{warn}
-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} for use with the simplifier. The tactic {\verb$induct_tac$~{\em
- var i}\/} applies structural induction over variable {\em var} to
-subgoal {\em i}.
-
-
-\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}.
-\begin{ttbox}
-MyList = HOL +
- datatype 'a list = Nil | Cons 'a ('a list)
-end
-\end{ttbox}
-After loading the theory (\verb$use_thy "MyList"$), we can prove
-$Cons~x~xs\neq xs$. First we build a suitable simpset for the simplifier:
-\begin{ttbox}
-val mylist_ss = HOL_ss addsimps MyList.list.simps;
-goal MyList.thy "!x. Cons x xs ~= xs";
-{\out Level 0}
-{\out ! x. Cons x xs ~= xs}
-{\out 1. ! x. Cons x xs ~= xs}
-\end{ttbox}
-This can be proved by the structural induction tactic:
-\begin{ttbox}
-by (MyList.list.induct_tac "xs" 1);
-{\out Level 1}
-{\out ! x. Cons x xs ~= xs}
-{\out 1. ! x. Cons x Nil ~= Nil}
-{\out 2. !!a list.}
-{\out ! x. Cons x list ~= list ==>}
-{\out ! x. Cons x (Cons a list) ~= Cons a list}
-\end{ttbox}
-The first subgoal can be proved with the simplifier and the distinctness
-axioms which are part of \verb$mylist_ss$.
-\begin{ttbox}
-by (simp_tac mylist_ss 1);
-{\out Level 2}
-{\out ! x. Cons x xs ~= xs}
-{\out 1. !!a list.}
-{\out ! x. Cons x list ~= list ==>}
-{\out ! x. Cons x (Cons a list) ~= Cons a list}
-\end{ttbox}
-Using the freeness axioms we can quickly prove the remaining goal.
-\begin{ttbox}
-by (asm_simp_tac mylist_ss 1);
-{\out Level 3}
-{\out ! x. Cons x xs ~= xs}
-{\out No subgoals!}
-\end{ttbox}
-Because both subgoals were proved by almost the same tactic we could have
-done that in one step using
-\begin{ttbox}
-by (ALLGOALS (asm_simp_tac mylist_ss));
-\end{ttbox}
-
-
-\subsubsection{The datatype $\alpha~list$ with mixfix syntax}
-
-In this example we define the type $\alpha~list$ again but this time we want
-to write {\tt []} instead of {\tt Nil} and we want to use the infix operator
-\verb|#| instead of {\tt Cons}. To do this we simply add mixfix annotations
-after the constructor declarations as follows:
-\begin{ttbox}
-MyList = HOL +
- datatype 'a list = "[]" ("[]")
- | "#" 'a ('a list) (infixr 70)
-end
-\end{ttbox}
-Now the theorem in the previous example can be written \verb|x#xs ~= xs|. The
-proof is the same.
-
-
-\subsubsection{A datatype for weekdays}
-
-This example shows a datatype that consists of more than four constructors:
-\begin{ttbox}
-Days = Arith +
- datatype days = Mo | Tu | We | Th | Fr | Sa | So
-end
-\end{ttbox}
-Because there are more than four constructors, the theory must be based on
-{\tt Arith}. Inequality is defined via a function \verb|days_ord|. Although
-the expression \verb|Mo ~= Tu| is not directly contained in {\tt distinct},
-it can be proved by the simplifier if \verb$arith_ss$ is used:
-\begin{ttbox}
-val days_ss = arith_ss addsimps Days.days.simps;
-
-goal Days.thy "Mo ~= Tu";
-by (simp_tac days_ss 1);
-\end{ttbox}
-Note that usually it is not necessary to derive these inequalities explicitly
-because the simplifier will dispose of them automatically.
-
-\subsection{Primitive recursive functions}
-\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.\
-\begin{ttbox}
-Append = MyList +
-consts app :: "['a list,'a list] => 'a list"
-rules
- app_Nil "app [] ys = ys"
- app_Cons "app (x#xs) ys = x#app xs ys"
-end
-\end{ttbox}
-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:
-\begin{ttbox}
-Append = MyList +
-consts app :: "'['a list,'a list] => 'a list"
-primrec app MyList.list
- app_Nil "app [] ys = ys"
- app_Cons "app (x#xs) ys = x#app xs ys"
-end
-\end{ttbox}
-The system will now check that the two rules \verb$app_Nil$ and
-\verb$app_Cons$ do indeed form a primitive recursive definition, thus
-ensuring that consistency is maintained. For example
-\begin{ttbox}
-primrec app MyList.list
- app_Nil "app [] ys = us"
-\end{ttbox}
-is rejected:
-\begin{ttbox}
-Extra variables on rhs
-\end{ttbox}
-\bigskip
-
-The general form of a primitive recursive definition is
-\begin{ttbox}
-primrec {\it function} {\it type}
- {\it reduction rules}
-\end{ttbox}
-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 named equations of the form
- {\it id\/}~{\it string}, where the identifier gives the name of the rule in
- the result structure, and {\it string} is a reduction rule 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.
-\end{itemize}
-A theory file may contain any number of {\tt primrec} sections which may be
-intermixed with other declarations.
-
-For the consistency-sensitive 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 also use infix or mixfix syntax:
-\begin{ttbox}
-Append = MyList +
-consts "@" :: "['a list,'a list] => 'a list" (infixr 60)
-primrec "op @" MyList.list
- app_Nil "[] @ ys = ys"
- app_Cons "(x#xs) @ ys = x#(xs @ ys)"
-end
-\end{ttbox}
-
-The reduction rules become part of the ML structure \verb$Append$ and can
-be used to prove theorems about the function:
-\begin{ttbox}
-val append_ss = HOL_ss addsimps [Append.app_Nil,Append.app_Cons];
-
-goal Append.thy "(xs @ ys) @ zs = xs @ (ys @ zs)";
-by (MyList.list.induct_tac "xs" 1);
-by (ALLGOALS(asm_simp_tac append_ss));
-\end{ttbox}
-
-%Note that underdefined primitive recursive functions are allowed:
-%\begin{ttbox}
-%Tl = MyList +
-%consts tl :: "'a list => 'a list"
-%primrec tl MyList.list
-% tl_Cons "tl(x#xs) = xs"
-%end
-%\end{ttbox}
-%Nevertheless {\tt tl} is total, although we do not know what the result of
-%\verb$tl([])$ is.
-
-\index{primitive recursion|)}
-\index{*primrec|)}
-\index{*datatype|)}
-
-
-\section{Inductive and coinductive definitions}
-\index{*inductive|(}
-\index{*coinductive|(}
-
-An {\bf inductive definition} specifies the least set closed under given
-rules. For example, a structural operational semantics is an inductive
-definition of an evaluation relation. Dually, a {\bf coinductive
- definition} specifies the greatest set closed under given rules. An
-important example is using bisimulation relations to formalize equivalence
-of processes and infinite data structures.
-
-A theory file may contain any number of inductive and coinductive
-definitions. They may be intermixed with other declarations; in
-particular, the (co)inductive sets {\bf must} be declared separately as
-constants, and may have mixfix syntax or be subject to syntax translations.
-
-Each (co)inductive definition adds definitions to the theory and also
-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.
-
-
-\subsection{The result structure}
-Many of the result structure's components have been discussed in the paper;
-others are self-explanatory.
-\begin{description}
-\item[\tt thy] is the new theory containing the recursive sets.
-
-\item[\tt defs] is the list of definitions of the recursive sets.
-
-\item[\tt mono] is a monotonicity theorem for the fixedpoint operator.
-
-\item[\tt unfold] is a fixedpoint equation for the recursive set (the union of
-the recursive sets, in the case of mutual recursion).
-
-\item[\tt intrs] is the list of introduction rules, now proved as theorems, for
-the recursive sets. The rules are also available individually, using the
-names given them in the theory file.
-
-\item[\tt elim] is the elimination rule.
-
-\item[\tt mk\_cases] is a function to create simplified instances of {\tt
-elim}, using freeness reasoning on some underlying datatype.
-\end{description}
-
-For an inductive definition, the result structure contains two induction rules,
-{\tt induct} and \verb|mutual_induct|. For a coinductive definition, it
-contains the rule \verb|coinduct|.
-
-Figure~\ref{def-result-fig} summarizes the two result signatures,
-specifying the types of all these components.
-
-\begin{figure}
-\begin{ttbox}
-sig
-val thy : theory
-val defs : thm list
-val mono : thm
-val unfold : thm
-val intrs : thm list
-val elim : thm
-val mk_cases : thm list -> string -> thm
-{\it(Inductive definitions only)}
-val induct : thm
-val mutual_induct: thm
-{\it(Coinductive definitions only)}
-val coinduct : thm
-end
-\end{ttbox}
-\hrule
-\caption{The result of a (co)inductive definition} \label{def-result-fig}
-\end{figure}
-
-\subsection{The syntax of a (co)inductive definition}
-An inductive definition has the form
-\begin{ttbox}
-inductive {\it inductive sets}
- intrs {\it introduction rules}
- monos {\it monotonicity theorems}
- con_defs {\it constructor definitions}
-\end{ttbox}
-A coinductive definition is identical, except that it starts with the keyword
-{\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.
-
-\begin{itemize}
-\item The {\it inductive sets} are specified by one or more strings.
-
-\item The {\it introduction rules} specify one or more introduction rules in
- the form {\it ident\/}~{\it string}, where the identifier gives the name of
- the rule in the result structure.
-
-\item The {\it monotonicity theorems} are required for each operator
- applied to a recursive set in the introduction rules. There {\bf must}
- be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each
- premise $t\in M(R_i)$ in an introduction rule!
-
-\item The {\it constructor definitions} contain definitions of constants
- appearing in the introduction rules. In most cases it can be omitted.
-\end{itemize}
-
-The package has a few notable restrictions:
-\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 Side-conditions must not be conjunctions. However, an introduction rule
-may contain any number of side-conditions.
-
-\item Side-conditions of the form $x=t$, where the variable~$x$ does not
- occur in~$t$, will be substituted through the rule \verb|mutual_induct|.
-\end{itemize}
-
-
-\subsection{Example of an inductive definition}
-Two declarations, included in a theory file, define the finite powerset
-operator. First we declare the constant~{\tt Fin}. Then we declare it
-inductively, with two introduction rules:
-\begin{ttbox}
-consts Fin :: "'a set => 'a set set"
-inductive "Fin A"
- intrs
- 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}.
-It contains the {\tt Fin}$~A$ introduction rules as the list {\tt Fin.intrs},
-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.
-\begin{ttbox}
-Acc = WF +
-consts pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*)
- acc :: "('a * 'a)set => 'a set" (*Accessible part*)
-defs pred_def "pred x r == {y. (y,x):r}"
-inductive "acc r"
- intrs
- pred "pred a r: Pow(acc r) ==> a: acc r"
- monos "[Pow_mono]"
-end
-\end{ttbox}
-The HOL distribution contains many other inductive definitions, such as the
-theory {\tt HOL/ex/PropLog.thy} and the directory {\tt HOL/IMP}. The
-theory {\tt HOL/ex/LList.thy} contains coinductive definitions.
-
-\index{*coinductive|)} \index{*inductive|)} \underscoreoff
-
-
-\section{The examples directories}
-Directory {\tt HOL/Subst} contains Martin Coen's mechanisation of a theory of
-substitutions and unifiers. It is based on Paulson's previous
-mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's
-theory~\cite{mw81}.
-
-Directory {\tt HOL/IMP} contains a mechanised version of a semantic
-equivalence proof taken from Winskel~\cite{winskel93}. It formalises the
-denotational and operational semantics of a simple while-language, then
-proves the two equivalent. It contains several datatype and inductive
-definitions, and demonstrates their use.
-
-Directory {\tt HOL/ex} contains other examples and experimental proofs in
-{\HOL}. Here is an overview of the more interesting files.
-\begin{itemize}
-\item File {\tt cla.ML} demonstrates the classical reasoner on over sixty
- predicate calculus theorems, ranging from simple tautologies to
- moderately difficult problems involving equality and quantifiers.
-
-\item File {\tt meson.ML} contains an experimental implementation of the {\sc
- meson} proof procedure, inspired by Plaisted~\cite{plaisted90}. It is
- much more powerful than Isabelle's classical reasoner. But it is less
- useful in practice because it works only for pure logic; it does not
- accept derived rules for the set theory primitives, for example.
-
-\item File {\tt mesontest.ML} contains test data for the {\sc meson} proof
- procedure. These are mostly taken from Pelletier \cite{pelletier86}.
-
-\item File {\tt set.ML} proves Cantor's Theorem, which is presented in
- \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem.
-
-\item Theories {\tt InSort} and {\tt Qsort} prove correctness properties of
- insertion sort and quick sort.
-
-\item The definition of lazy lists demonstrates methods for handling
- infinite data structures and coinduction in higher-order
- logic~\cite{paulson-coind}. Theory \thydx{LList} defines an operator for
- corecursion on lazy lists, which is used to define a few simple functions
- such as map and append. Corecursion cannot easily define operations such
- as filter, which can compute indefinitely before yielding the next
- element (if any!) of the lazy list. A coinduction principle is defined
- for proving equations on lazy lists.
-
-\item Theory {\tt PropLog} proves the soundness and completeness of
- classical propositional logic, given a truth table semantics. The only
- connective is $\imp$. A Hilbert-style axiom system is specified, and its
- set of theorems defined inductively. A similar proof in \ZF{} is
- described elsewhere~\cite{paulson-set-II}.
-
-\item Theory {\tt Term} develops an experimental recursive type definition;
- the recursion goes through the type constructor~\tydx{list}.
-
-\item Theory {\tt Simult} constructs mutually recursive sets of trees and
- forests, including induction and recursion rules.
-
-\item Theory {\tt MT} contains Jacob Frost's formalization~\cite{frost93} of
- Milner and Tofte's coinduction example~\cite{milner-coind}. This
- substantial proof concerns the soundness of a type system for a simple
- functional language. The semantics of recursion is given by a cyclic
- environment, which makes a coinductive argument appropriate.
-\end{itemize}
-
-
-\goodbreak
-\section{Example: Cantor's Theorem}\label{sec:hol-cantor}
-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 x::\alpha. f~x \not= S
-\]
-%
-Viewing types as sets, $\alpha\To bool$ represents the powerset
-of~$\alpha$. This version states that for every function from $\alpha$ to
-its powerset, some subset is outside its range.
-
-The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and
-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)";
-{\out Level 0}
-{\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$.
-\begin{ttbox}
-by (resolve_tac [notI] 1);
-{\out Level 1}
-{\out ~ ?S : range f}
-{\out 1. ?S : range f ==> False}
-\ttbreak
-by (eresolve_tac [rangeE] 1);
-{\out Level 2}
-{\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$,
-we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f~x$ for
-any~$\Var{c}$.
-\begin{ttbox}
-by (eresolve_tac [equalityCE] 1);
-{\out Level 3}
-{\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}
-\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
-$\Var{P}~\Var{c}$. Destruct-resolution using \tdx{CollectD}
-instantiates~$\Var{S}$ and creates the new assumption.
-\begin{ttbox}
-by (dresolve_tac [CollectD] 1);
-{\out Level 4}
-{\out ~ \{x. ?P7 x\} : 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}
-\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.
-\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}
-\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}
-\ttbreak
-by (assume_tac 1);
-{\out Level 7}
-{\out ~ \{x. ~ x : f x\} : range f}
-{\out No subgoals!}
-\end{ttbox}
-How much creativity is required? As it happens, Isabelle can prove this
-theorem automatically. The classical set \ttindex{set_cs} contains rules
-for most of the constructs of \HOL's set theory. We must augment it with
-\tdx{equalityCE} to break up set equalities, and then apply best-first
-search. Depth-first search would diverge, but best-first search
-successfully navigates through the large search space.
-\index{search!best-first}
-\begin{ttbox}
-choplev 0;
-{\out Level 0}
-{\out ~ ?S : range f}
-{\out 1. ~ ?S : range f}
-\ttbreak
-by (best_tac (set_cs addSEs [equalityCE]) 1);
-{\out Level 1}
-{\out ~ \{x. ~ x : f x\} : range f}
-{\out No subgoals!}
-\end{ttbox}
-
-\index{higher-order logic|)}
--- a/doc-src/Logics/logics.bbl Tue Mar 30 13:17:55 1999 +0200
+++ b/doc-src/Logics/logics.bbl Wed Mar 31 16:14:20 1999 +0200
@@ -1,202 +1,3 @@
-\begin{thebibliography}{10}
-
-\bibitem{andrews86}
-Peter~B. Andrews.
-\newblock {\em An Introduction to Mathematical Logic and Type Theory: To Truth
- Through Proof}.
-\newblock Academic Press, 1986.
-
-\bibitem{church40}
-Alonzo Church.
-\newblock A formulation of the simple theory of types.
-\newblock {\em Journal of Symbolic Logic}, 5:56--68, 1940.
-
-\bibitem{coen92}
-Martin~D. Coen.
-\newblock {\em Interactive Program Derivation}.
-\newblock PhD thesis, University of Cambridge, November 1992.
-\newblock Computer Laboratory Technical Report 272.
-
-\bibitem{constable86}
-R.~L. Constable et~al.
-\newblock {\em Implementing Mathematics with the Nuprl Proof Development
- System}.
-\newblock Prentice-Hall, 1986.
-
-\bibitem{felty91a}
-Amy Felty.
-\newblock A logic program for transforming sequent proofs to natural deduction
- proofs.
-\newblock In Peter Schroeder-Heister, editor, {\em Extensions of Logic
- Programming}, LNAI 475, pages 157--178. Springer, 1991.
-
-\bibitem{frost93}
-Jacob Frost.
-\newblock A case study of co-induction in {Isabelle HOL}.
-\newblock Technical Report 308, Computer Laboratory, University of Cambridge,
- August 1993.
-
-\bibitem{gallier86}
-J.~H. Gallier.
-\newblock {\em Logic for Computer Science: Foundations of Automatic Theorem
- Proving}.
-\newblock Harper \& Row, 1986.
-
-\bibitem{mgordon-hol}
-M.~J.~C. Gordon and T.~F. Melham.
-\newblock {\em Introduction to {HOL}: A Theorem Proving Environment for Higher
- Order Logic}.
-\newblock Cambridge University Press, 1993.
-
-\bibitem{huet78}
-G.~P. Huet and B.~Lang.
-\newblock Proving and applying program transformations expressed with
- second-order patterns.
-\newblock {\em Acta Informatica}, 11:31--55, 1978.
-
-\bibitem{alf}
-Lena Magnusson and Bengt {Nordstr\"{o}m}.
-\newblock The {ALF} proof editor and its proof engine.
-\newblock In Henk Barendregt and Tobias Nipkow, editors, {\em Types for Proofs
- and Programs: International Workshop {TYPES '93}}, LNCS 806, pages 213--237.
- Springer, published 1994.
-
-\bibitem{mw81}
-Zohar Manna and Richard Waldinger.
-\newblock Deductive synthesis of the unification algorithm.
-\newblock {\em Science of Computer Programming}, 1(1):5--48, 1981.
-
-\bibitem{martinlof84}
-Per Martin-L\"of.
-\newblock {\em Intuitionistic type theory}.
-\newblock Bibliopolis, 1984.
-
-\bibitem{milner78}
-Robin Milner.
-\newblock A theory of type polymorphism in programming.
-\newblock {\em Journal of Computer and System Sciences}, 17:348--375, 1978.
-
-\bibitem{milner-coind}
-Robin Milner and Mads Tofte.
-\newblock Co-induction in relational semantics.
-\newblock {\em Theoretical Computer Science}, 87:209--220, 1991.
-
-\bibitem{Naraschewski-Wenzel:1998:TPHOL}
-Wolfgang Naraschewski and Markus Wenzel.
-\newblock Object-oriented verification based on record subtyping in
- higher-order logic.
-\newblock In Jim Grundy and Malcolm Newey, editors, {\em Theorem Proving in
- Higher Order Logics: {TPHOLs} '98}, LNCS 1479, pages 349--366, 1998.
-
-\bibitem{nazareth-nipkow}
-Dieter Nazareth and Tobias Nipkow.
-\newblock Formal verification of algorithm {W}: The monomorphic case.
-\newblock In von Wright et~al. \cite{tphols96}, pages 331--345.
-
-\bibitem{Nipkow-CR}
-Tobias Nipkow.
-\newblock More {Church-Rosser} proofs (in {Isabelle/HOL}).
-\newblock In Michael McRobbie and John~K. Slaney, editors, {\em Automated
- Deduction --- {CADE}-13 International Conference}, LNAI 1104, pages 733--747.
- Springer, 1996.
-
-\bibitem{nipkow-IMP}
-Tobias Nipkow.
-\newblock Winskel is (almost) right: Towards a mechanized semantics textbook.
-\newblock In V.~Chandru and V.~Vinay, editors, {\em Foundations of Software
- Technology and Theoretical Computer Science}, volume 1180 of {\em LNCS},
- pages 180--192. Springer, 1996.
-
-\bibitem{nordstrom90}
-Bengt {Nordstr\"om}, Kent Petersson, and Jan Smith.
-\newblock {\em Programming in {Martin-L\"of}'s Type Theory. An Introduction}.
-\newblock Oxford University Press, 1990.
-
-\bibitem{paulson85}
-Lawrence~C. Paulson.
-\newblock Verifying the unification algorithm in {LCF}.
-\newblock {\em Science of Computer Programming}, 5:143--170, 1985.
-
-\bibitem{paulson87}
-Lawrence~C. Paulson.
-\newblock {\em Logic and Computation: Interactive proof with Cambridge LCF}.
-\newblock Cambridge University Press, 1987.
-
-\bibitem{paulson-CADE}
-Lawrence~C. Paulson.
-\newblock A fixedpoint approach to implementing (co)inductive definitions.
-\newblock In Alan Bundy, editor, {\em Automated Deduction --- {CADE}-12
- International Conference}, LNAI 814, pages 148--161. Springer, 1994.
-
-\bibitem{paulson-set-II}
-Lawrence~C. Paulson.
-\newblock Set theory for verification: {II}. {Induction} and recursion.
-\newblock {\em Journal of Automated Reasoning}, 15(2):167--215, 1995.
-
-\bibitem{paulson-ns}
-Lawrence~C. Paulson.
-\newblock Mechanized proofs of security protocols: {Needham-Schroeder} with
- public keys.
-\newblock Technical Report 413, Computer Laboratory, University of Cambridge,
- January 1997.
-
-\bibitem{paulson-coind}
-Lawrence~C. Paulson.
-\newblock Mechanizing coinduction and corecursion in higher-order logic.
-\newblock {\em Journal of Logic and Computation}, 7(2):175--204, March 1997.
-
-\bibitem{paulson-security}
-Lawrence~C. Paulson.
-\newblock Proving properties of security protocols by induction.
-\newblock In {\em 10th Computer Security Foundations Workshop}, pages 70--83.
- IEEE Computer Society Press, 1997.
-
-\bibitem{isabelle-ZF}
-Lawrence~C. Paulson.
-\newblock {Isabelle}'s logics: {FOL} and {ZF}.
-\newblock Technical report, Computer Laboratory, University of Cambridge, 1999.
-
-\bibitem{paulson-COLOG}
-Lawrence~C. Paulson.
-\newblock A formulation of the simple theory of types (for {Isabelle}).
-\newblock In P.~Martin-L\"of and G.~Mints, editors, {\em COLOG-88:
- International Conference on Computer Logic}, LNCS 417, pages 246--274,
- Tallinn, Published 1990. Estonian Academy of Sciences, Springer.
-
-\bibitem{pelletier86}
-F.~J. Pelletier.
-\newblock Seventy-five problems for testing automatic theorem provers.
-\newblock {\em Journal of Automated Reasoning}, 2:191--216, 1986.
-\newblock Errata, JAR 4 (1988), 235--236 and JAR 18 (1997), 135.
-
-\bibitem{plaisted90}
-David~A. Plaisted.
-\newblock A sequent-style model elimination strategy and a positive refinement.
-\newblock {\em Journal of Automated Reasoning}, 6(4):389--402, 1990.
-
-\bibitem{slind-tfl}
-Konrad Slind.
-\newblock Function definition in higher-order logic.
-\newblock In von Wright et~al. \cite{tphols96}.
-
-\bibitem{takeuti87}
-G.~Takeuti.
-\newblock {\em Proof Theory}.
-\newblock North-Holland, 2nd edition, 1987.
-
-\bibitem{thompson91}
-Simon Thompson.
-\newblock {\em Type Theory and Functional Programming}.
-\newblock Addison-Wesley, 1991.
-
-\bibitem{tphols96}
-J.~von Wright, J.~Grundy, and J.~Harrison, editors.
-\newblock {\em Theorem Proving in Higher Order Logics: {TPHOLs} '96}, LNCS
- 1125, 1996.
-
-\bibitem{winskel93}
-Glynn Winskel.
-\newblock {\em The Formal Semantics of Programming Languages}.
-\newblock MIT Press, 1993.
+\begin{thebibliography}{}
\end{thebibliography}