doc-src/Logics/Old_HOL.tex

indentation and renaming of rules

%% $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{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{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
\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\times\beta, [\alpha,\beta]\To\gamma] \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(p,c) == 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(<a,b>, c) = 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+\beta, \alpha\To\gamma, \beta\To\gamma] \To\gamma$
        & & conditional
\end{constants}
\begin{ttbox}\makeatletter
\tdx{sum_case_def}   sum_case == (\%p f g. @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(Inl(x), f, g) = f(x)
\tdx{sum_case_Inr}   sum_case(Inr(x), f, g) = g(x)

\tdx{surjective_sum} sum_case(s, \%x::'a. f(Inl(x)), \%y::'b. f(Inr(y))) = 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
HOL_dup_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{HOL_dup_cs}] extends {\tt prop_cs} with the safe rules
  {\tt allI} and~{\tt exE} and the unsafe rules \tdx{all_dupE}
  and~\tdx{exCI}, as well as rules for unique existence.  Search using
  this is complete --- quantified formulae may be duplicated --- but
  frequently fails to terminate.  It is generally unsuitable for
  depth-first search.

\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} & $[nat, \alpha, nat\To\alpha] \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 == (\%n a f. @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, \%l g.nat_case(l, c, \%m.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(0, a, f) = a
\tdx{nat_case_Suc}   nat_case(Suc(k), a, f) = 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(x#xs, c, h) = 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"(e, a, \lambda x\;xs.b)
\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$.


\subsection{The type constructor for lazy lists, {\tt llist}}
\index{*llist type}

The definition of lazy lists demonstrates methods for handling infinite
data structures and coinduction in higher-order logic.  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.

I have written a paper discussing the treatment of lazy lists; it also
covers finite lists~\cite{paulson-coind}.


\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}
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{Defining functions on datatypes}

Normally one wants to define functions dealing with a newly defined type and
prove properties of these functions. As an example let us define \verb|@| for
concatenation and {\tt ttl} for the (total) tail of a list, i.e.\ the list
without its first element:
\begin{ttbox}
List_fun = MyList +
consts ttl  :: "'a list => 'a list"
       "@"  :: "['a list,'a list] => 'a list"  (infixr 60)
rules 
       ttl_def   "ttl (l)  == case l of [] => []  |  y#ys => ys"

       app_Nil   "[] @ ys = ys"
       app_Cons  "(x#xs) @ ys = x#(xs @ ys)"
end
\end{ttbox}
Let us have a look at the use of {\tt case} in the definition of {\tt ttl}.
The expression {\tt case e of [] => [] | y\#ys => ys} evaluates to {\tt []}
if \verb|e=[]| and to {\tt ys} if \verb|e=y#ys|. These properties are
trivial to derive by simplification:
\begin{ttbox}
val mylist_ss = HOL_ss addsimps MyList.list.simps;

goalw List_fun.thy [List_fun.ttl_def] "ttl([]) = []";
by (simp_tac mylist_ss 1);
val ttl_Nil = result();

goalw List_fun.thy [List_fun.ttl_def] "ttl(y#ys) = ys";
by (simp_tac mylist_ss 1);
val ttl_Cons = result();

val list_fun_ss = mylist_ss addsimps
      [ttl_Nil, ttl_Cons, List_fun.app_Nil, List_fun.app_Cons];
\end{ttbox}
Note that we include the derived properties in our simpset, not the original
definition of {\tt ttl}. The former are better behaved because they only
apply if the argument is already a constructor.

One could have defined \verb$@$ with a single {\tt case}-construct
\begin{ttbox}
app_def "x @ y == case x of [] => y  |  z#zs => z # (zs @ y)"
\end{ttbox}  
and derived \verb$app_Nil$ and \verb$app_Cons$ from it. But \verb$app_def$ is
not easy to work with: the left-hand side matches a subterm of the right-hand
side, which causes the simplifier to loop.

Here is a simple proof of the associativity of \verb$@$:
\begin{ttbox}
goal List_fun.thy "(x @ y) @ z = x @ (y @ z)";
by (MyList.list.induct_tac "x" 1);
by (simp_tac list_fun_ss 1);
by (asm_simp_tac list_fun_ss 1);
\end{ttbox}
The last two steps can again be combined using {\tt ALLGOALS}.


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

\index{*datatype|)}
\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/ex} contains other examples and experimental proofs in
{\HOL}.  Here is an overview of the more interesting files.
\begin{ttdescription}
\item[HOL/ex/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[HOL/ex/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[HOL/ex/mesontest.ML] contains test data for the {\sc meson} proof
  procedure.  These are mostly taken from Pelletier \cite{pelletier86}.

\item[HOL/ex/set.ML] proves Cantor's Theorem, which is presented in
  \S\ref{sec:hol-cantor} below, and the Schr\"oder-Bernstein Theorem.

\item[HOL/ex/InSort.ML] and {\tt HOL/ex/Qsort.ML} contain correctness
  proofs about insertion sort and quick sort.

\item[HOL/ex/PL.ML] 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[HOL/ex/Term.ML] 
  contains proofs about an experimental recursive type definition;
  the recursion goes through the type constructor~\tydx{list}.

\item[HOL/ex/Simult.ML] defines primitives for solving mutually recursive
  equations over sets.  It constructs sets of trees and forests as an
  example, including induction and recursion rules that handle the mutual
  recursion.

\item[HOL/ex/MT.ML] 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{ttdescription}


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