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

 \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,j,f(j-n)))

 \tdx{quo_def}   m div n == wfrec(trancl(pred_nat), 

                         m, \%j f. if(j<n,0,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, True, x mem ys)

 \tdx{filter_Nil}      filter(P, []) = []

 \tdx{filter_Cons}     filter(P,x#xs) = if(P(x), x#filter(P,xs), 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|)}

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