%% $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.

Previous releases of Isabelle included a different 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}

               \\[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.@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,x,y) = x

\tdx{if_False}        if(False,x,y) = y

\tdx{if_P}            P ==> if(P,x,y) = x

\tdx{if_not_P}        ~ P ==> if(P,x,y) = y

\tdx{expand_if}       P(if(Q,x,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,\ldots,{\tt insert}(a@n,\{\}))

\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 $\langle a,b\rangle$ \\

  \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 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