%% $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 the original Church-style higher-order logic.  Experience

 with the {\sc hol} system has demonstrated that higher-order logic is widely

 applicable in many areas of mathematics and computer science, not just

 hardware verification, {\sc hol}'s original \textit{raison d'{\^e}tre\/}.  It

 is weaker than ZF set theory but for most applications this does not matter.

 If you prefer {\ML} to Lisp, you will probably prefer HOL to~ZF.

 The syntax of HOL\footnote{Earlier versions of Isabelle's HOL used a different

   syntax.  Ancient releases of Isabelle included still another version of~HOL,

   with explicit type inference rules~\cite{paulson-COLOG}.  This version no

   longer exists, but \thydx{ZF} supports a similar style of reasoning.}

 follows $\lambda$-calculus and functional programming.  Function application

 is curried.  To apply the function~$f$ of type $\tau@1\To\tau@2\To\tau@3$ to

 the arguments~$a$ and~$b$ in HOL, you simply write $f\,a\,b$.  There is no

 `apply' operator as in \thydx{ZF}.  Note that $f(a,b)$ means ``$f$ applied to

 the pair $(a,b)$'' in HOL.  We write ordered pairs as $(a,b)$, not $\langle

 a,b\rangle$ as in ZF.

 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.

 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 \texttt{show_types} (or even \texttt{show_sorts}) set to \texttt{true}.

 \begin{figure}

 \begin{constants}

   \it name      &\it meta-type  & \it description \\

   \cdx{Trueprop}& $bool\To prop$                & coercion to $prop$\\

   \cdx{Not}     & $bool\To bool$                & negation ($\lnot$) \\

   \cdx{True}    & $bool$                        & tautology ($\top$) \\

   \cdx{False}   & $bool$                        & absurdity ($\bot$) \\

   \cdx{If}      & $[bool,\alpha,\alpha]\To\alpha$ & conditional \\

   \cdx{Let}     & $[\alpha,\alpha\To\beta]\To\beta$ & let binder

 \end{constants}

 \subcaption{Constants}

 \begin{constants}

 \index{"@@{\tt\at} symbol}

 \index{*"! symbol}\index{*"? symbol}

 \index{*"?"! symbol}\index{*"E"X"! symbol}

   \it symbol &\it name     &\it meta-type & \it description \\

   \sdx{SOME} or \tt\at & \cdx{Eps}  & $(\alpha\To bool)\To\alpha$ & 

         Hilbert description ($\varepsilon$) \\

   \sdx{ALL} or {\tt!~} & \cdx{All}  & $(\alpha\To bool)\To bool$ & 

         universal quantifier ($\forall$) \\

   \sdx{EX} or {\tt?~}  & \cdx{Ex}   & $(\alpha\To bool)\To bool$ & 

         existential quantifier ($\exists$) \\

   \texttt{EX!} or {\tt?!} & \cdx{Ex1}  & $(\alpha\To bool)\To bool$ & 

         unique existence ($\exists!$)\\

   \texttt{LEAST}  & \cdx{Least}  & $(\alpha::ord \To bool)\To\alpha$ & 

         least element

 \end{constants}

 \subcaption{Binders} 

 \begin{constants}

 \index{*"= symbol}

 \index{&@{\tt\&} symbol}

 \index{*"| symbol}

 \index{*"-"-"> symbol}

   \it symbol    & \it meta-type & \it priority & \it description \\ 

   \sdx{o}       & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & 

         Left 55 & composition ($\circ$) \\

   \tt =         & $[\alpha,\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{constants}

 \subcaption{Infixes}

 \caption{Syntax of \texttt{HOL}} \label{hol-constants}

 \end{figure}

 \begin{figure}

 \index{*let symbol}

 \index{*in symbol}

 \dquotes

 \[\begin{array}{rclcl}

     term & = & \hbox{expression of class~$term$} \\

          & | & "SOME~" id " . " formula

          & | & "\at~" id " . " formula \\

          & | & 

     \multicolumn{3}{l}{"let"~id~"="~term";"\dots";"~id~"="~term~"in"~term} \\

          & | & 

     \multicolumn{3}{l}{"if"~formula~"then"~term~"else"~term} \\

          & | & "LEAST"~ id " . " formula \\[2ex]

  formula & = & \hbox{expression of type~$bool$} \\

          & | & term " = " term \\

          & | & term " \ttilde= " term \\

          & | & term " < " term \\

          & | & term " <= " term \\

          & | & "\ttilde\ " formula \\

          & | & formula " \& " formula \\

          & | & formula " | " formula \\

          & | & formula " --> " formula \\

          & | & "ALL~" id~id^* " . " formula

          & | & "!~~~" id~id^* " . " formula \\

          & | & "EX~~" id~id^* " . " formula 

          & | & "?~~~" id~id^* " . " formula \\

          & | & "EX!~" id~id^* " . " formula

          & | & "?!~~" id~id^* " . " formula \\

   \end{array}

 \]

 \caption{Full grammar for HOL} \label{hol-grammar}

 \end{figure} 

 \section{Syntax}

 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

 $\lnot(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, $\lnot\lnot P=P$

   abbreviates $\lnot\lnot (P=P)$ and not $(\lnot\lnot P)=P$.  When using $=$

   to mean logical equivalence, enclose both operands in parentheses.

 \end{warn}

 \subsection{Types and overloading}

 The universal type class of higher-order terms is called~\cldx{term}.

 By default, explicit type variables have class \cldx{term}.  In

 particular the equality symbol and quantifiers are polymorphic over

 class \texttt{term}.

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

   term)\thinspace term}.  Thus, $\sigma\To\tau$ belongs to class~{\tt

   term} if $\sigma$ and~$\tau$ do, allowing quantification over

 functions.

 HOL allows new types to be declared as subsets of existing types;

 see~{\S}\ref{sec:HOL:Types}.  ML-like datatypes can also be declared; see

 ~{\S}\ref{sec:HOL:datatype}.

 Several syntactic type classes --- \cldx{plus}, \cldx{minus},

 \cldx{times} and

 \cldx{power} --- permit overloading of the operators {\tt+},\index{*"+

   symbol} {\tt-}\index{*"- symbol}, {\tt*}.\index{*"* symbol} 

 and \verb|^|.\index{^@\verb.^. symbol} 

 %

 They are overloaded to denote the obvious arithmetic operations on types

 \tdx{nat}, \tdx{int} and~\tdx{real}. (With the \verb|^| operator, the

 exponent always has type~\tdx{nat}.)  Non-arithmetic overloadings are also

 done: the operator {\tt-} can denote set difference, while \verb|^| can

 denote exponentiation of relations (iterated composition).  Unary minus is

 also written as~{\tt-} and is overloaded like its 2-place counterpart; it even

 can stand for set complement.

 The constant \cdx{0} is also overloaded.  It serves as the zero element of

 several types, of which the most important is \tdx{nat} (the natural

 numbers).  The type class \cldx{plus_ac0} comprises all types for which 0

 and~+ satisfy the laws $x+y=y+x$, $(x+y)+z = x+(y+z)$ and $0+x = x$.  These

 types include the numeric ones \tdx{nat}, \tdx{int} and~\tdx{real} and also

 multisets.  The summation operator \cdx{setsum} is available for all types in

 this class. 

 Theory \thydx{Ord} defines the syntactic class \cldx{ord} of order

 signatures.  The relations $<$ and $\leq$ are polymorphic over this

 class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and

 the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass

 \cldx{order} of \cldx{ord} which axiomatizes the types that are partially

 ordered with respect to~$\leq$.  A further subclass \cldx{linorder} of

 \cldx{order} axiomatizes linear orderings.

 For details, see the file \texttt{Ord.thy}.

 If you state a goal containing overloaded functions, you may need to include

 type constraints.  Type inference may otherwise make the goal more

 polymorphic than you intended, with confusing results.  For example, the

 variables $i$, $j$ and $k$ in the goal $i \leq j \Imp i \leq j+k$ have type

 $\alpha::\{ord,plus\}$, although you may have expected them to have some

 numeric type, e.g. $nat$.  Instead you should have stated the goal as

 $(i::nat) \leq j \Imp i \leq j+k$, which causes all three variables to have

 type $nat$.

 \begin{warn}

   If resolution fails for no obvious reason, try setting

   \ttindex{show_types} to \texttt{true}, causing Isabelle to display

   types of terms.  Possibly set \ttindex{show_sorts} to \texttt{true} as

   well, causing Isabelle to display type classes and 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 \texttt{resolve_tac},

   possibly instantiating type variables.  Setting

   \ttindex{Unify.trace_types} to \texttt{true} causes Isabelle to report

   omitted search paths during unification.\index{tracing!of unification}

 \end{warn}

 \subsection{Binders}

 Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for some~$x$

 satisfying~$P$, if such exists.  Since all terms in HOL denote something, a

 description is always meaningful, but we do not know its value unless $P$

 defines it uniquely.  We may write descriptions as \cdx{Eps}($\lambda x.

 P[x]$) or use the syntax \hbox{\tt SOME~$x$.~$P[x]$}.

 Existential quantification is defined by

 \[ \exists x. P~x \;\equiv\; P(\varepsilon x. P~x). \]

 The unique existence quantifier, $\exists!x. P$, 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$.

 \medskip

 \index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} The

 basic Isabelle/HOL binders have two notations.  Apart from the usual

 \texttt{ALL} and \texttt{EX} for $\forall$ and $\exists$, Isabelle/HOL also

 supports the original notation of Gordon's {\sc hol} system: \texttt{!}\ 

 and~\texttt{?}.  In the latter case, the existential quantifier \emph{must} be

 followed by a space; thus {\tt?x} is an unknown, while \verb'? x. f x=y' is a

 quantification.  Both notations are accepted for input.  The print mode

 ``\ttindexbold{HOL}'' governs the output notation.  If enabled (e.g.\ by

 passing option \texttt{-m HOL} to the \texttt{isabelle} executable),

 then~{\tt!}\ and~{\tt?}\ are displayed.

 \medskip

 If $\tau$ is a type of class \cldx{ord}, $P$ a formula and $x$ a

 variable of type $\tau$, then the term \cdx{LEAST}~$x. P[x]$ is defined

 to be the least (w.r.t.\ $\leq$) $x$ such that $P~x$ holds (see

 Fig.~\ref{hol-defs}).  The definition uses Hilbert's $\varepsilon$

 choice operator, so \texttt{Least} is always meaningful, but may yield

 nothing useful in case there is not a unique least element satisfying

 $P$.\footnote{Class $ord$ does not require much of its instances, so

   $\leq$ need not be a well-ordering, not even an order at all!}

 \medskip All these binders have priority 10.

 \begin{warn}

 The low priority of binders means that they need to be enclosed in

 parenthesis when they occur in the context of other operations.  For example,

 instead of $P \land \forall x. Q$ you need to write $P \land (\forall x. Q)$.

 \end{warn}

 \subsection{The let and case constructions}

 Local abbreviations can be introduced by a \texttt{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 \texttt{case} constructs.  Therefore \texttt{case}

 and \sdx{of} are reserved words.  Initially, this is mere syntax and has no

 logical meaning.  By declaring translations, you can cause instances of the

 \texttt{case} construct to denote applications of particular case operators.

 This is what happens automatically for each \texttt{datatype} definition

 (see~{\S}\ref{sec:HOL:datatype}).

 \begin{warn}

 Both \texttt{if} and \texttt{case} constructs have as low a priority as

 quantifiers, which requires additional enclosing parentheses in the context

 of most other operations.  For example, instead of $f~x = {\tt if\dots

 then\dots else}\dots$ you need to write $f~x = ({\tt if\dots then\dots

 else\dots})$.

 \end{warn}

 \section{Rules of inference}

 \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{someI}         P(x::'a) ==> P(@x. P x)

 \tdx{True_or_False} (P=True) | (P=False)

 \end{ttbox}

 \caption{The \texttt{HOL} rules} \label{hol-rules}

 \end{figure}

 Figure~\ref{hol-rules} shows the primitive 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{someI}] gives the defining property of the Hilbert

   $\varepsilon$-operator.  It is a form of the Axiom of Choice.  The derived rule

   \tdx{some_equality} (see below) is often easier to use.

 \item[\tdx{True_or_False}] makes the logic classical.\footnote{In

     fact, the $\varepsilon$-operator already makes the logic classical, as

     shown by Diaconescu; see Paulson~\cite{paulson-COLOG} for details.}

 \end{ttdescription}

 \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{o_def}      op o     == (\%(f::'b=>'c) g x::'a. f(g x))

 \tdx{if_def}     If P x y ==

               (\%P x y. @z::'a.(P=True --> z=x) & (P=False --> z=y))

 \tdx{Let_def}    Let s f  == f s

 \tdx{Least_def}  Least P  == @x. P(x) & (ALL y. P(y) --> x <= y)"

 \end{ttbox}

 \caption{The \texttt{HOL} definitions} \label{hol-defs}

 \end{figure}

 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.

 \begin{warn}

 The definitions above should never be expanded and are shown for completeness

 only.  Instead users should reason in terms of the derived rules shown below

 or, better still, using high-level tactics

 (see~{\S}\ref{sec:HOL:generic-packages}).

 \end{warn}

 Some of the rules mention type variables; for example, \texttt{refl}

 mentions the type variable~{\tt'a}.  This allows you to instantiate

 type variables explicitly by calling \texttt{res_inst_tac}.

 \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

 \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

 \tdx{cong}        [| f = g; x = y |] ==> f x = g y

 \tdx{not_sym}     t ~= s ==> s ~= t

 \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. P x) ==> !x. P x

 \tdx{spec}      !x. 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. P x

 \tdx{exE}       [| ? x. 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{some_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_P}         P ==> (if P then x else y) = x

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

 \tdx{split_if}     P(if Q then x else y) = ((Q --> P x) & (~Q --> P y))

 \subcaption{Conditionals}

 \end{ttbox}

 \caption{More derived rules} \label{hol-lemmas2}

 \end{figure}

 Some derived rules are shown in Figures~\ref{hol-lemmas1}

 and~\ref{hol-lemmas2}, with their {\ML} names.  These include natural rules

 for the logical connectives, as well as sequent-style elimination rules for

 conjunctions, implications, and universal quantifiers.  

 Note the equality rules: \tdx{ssubst} performs substitution in

 backward proofs, while \tdx{box_equals} supports reasoning by

 simplifying both sides of an equation.

 The following simple tactics are occasionally useful:

 \begin{ttdescription}

 \item[\ttindexbold{strip_tac} $i$] applies \texttt{allI} and \texttt{impI}

   repeatedly to remove all outermost universal quantifiers and implications

   from subgoal $i$.

 \item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction on

   $P$ for subgoal $i$: the latter is replaced by two identical subgoals with

   the added assumptions $P$ and $\lnot P$, respectively.

 \item[\ttindexbold{smp_tac} $j$ $i$] applies $j$ times \texttt{spec} and then

   \texttt{mp} in subgoal $i$, which is typically useful when forward-chaining 

   from an induction hypothesis. As a generalization of \texttt{mp_tac}, 

   if there are assumptions $\forall \vec{x}. P \vec{x} \imp Q \vec{x}$ and 

   $P \vec{a}$, ($\vec{x}$ being a vector of $j$ variables)

   then it replaces the universally quantified implication by $Q \vec{a}$. 

   It may instantiate unknowns. It fails if it can do nothing.

 \end{ttdescription}

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

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

   \sdx{UN}  & \cdx{UNION1}  & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & 

         union 

 \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 ($\int$) \\

   \sdx{Un}      & $[\alpha\,set,\alpha\,set]\To\alpha\,set$

         & Left 65 & union ($\un$) \\

   \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 \texttt{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 not in\\

   {\ttlbrace}$a@1$, $\ldots${\ttrbrace}  &  insert $a@1$ $\ldots$ {\ttlbrace}{\ttrbrace} & \rm finite set \\

   {\ttlbrace}$x$. $P[x]${\ttrbrace}        &  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 \\

   \sdx{ALL} $x$:$A$.\ $P[x]$ or \texttt{!} $x$:$A$.\ $P[x]$ &

         Ball $A$ $\lambda x.\ P[x]$ & 

         \rm bounded $\forall$ \\

   \sdx{EX}{\tt\ } $x$:$A$.\ $P[x]$ or \texttt{?} $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} \\

          & | & "{\ttlbrace}{\ttrbrace}" \\

          & | & "{\ttlbrace} " term\; ("," term)^* " {\ttrbrace}" \\

          & | & "{\ttlbrace} " id " . " formula " {\ttrbrace}" \\

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

          & | & "ALL " id ":" term " . " formula

          & | & "!~" id ":" term " . " formula \\

          & | & "EX~~" id ":" term " . " formula

          & | & "?~" id ":" term " . " formula \\

   \end{array}

 \]

 \subcaption{Full Grammar}

 \caption{Syntax of the theory \texttt{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.  The isomorphisms

 between the two types are declared explicitly.  They are very natural:

 \texttt{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\un B$

 and $A\int B$), the subset and membership relations, and the image

 operator~{\tt``}\@.  Note that $a$\verb|~:|$b$ is translated to

 $\lnot(a\in b)$.  

 The $\{a@1,\ldots\}$ notation abbreviates finite sets constructed in

 the obvious manner using~\texttt{insert} and~$\{\}$:

 \begin{eqnarray*}

   \{a, b, c\} & \equiv &

   \texttt{insert} \, a \, ({\tt insert} \, b \, ({\tt insert} \, c \, \{\}))

 \end{eqnarray*}

 The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} 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 \texttt{Ball $A$ $P$} and \texttt{Bex $A$ $P$} we may

 write\index{*"! symbol}\index{*"? symbol}

 \index{*ALL symbol}\index{*EX symbol} 

 %

 \hbox{\tt ALL~$x$:$A$.\ $P[x]$} and \hbox{\tt EX~$x$:$A$.\ $P[x]$}.  The

 original notation of Gordon's {\sc hol} system is supported as well:

 \texttt{!}\ and \texttt{?}.

 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 : {\ttlbrace}x. P x{\ttrbrace}) = P a

 \tdx{Collect_mem_eq}    {\ttlbrace}x. x:A{\ttrbrace} = A

 \tdx{empty_def}         {\ttlbrace}{\ttrbrace}          == {\ttlbrace}x. False{\ttrbrace}

 \tdx{insert_def}        insert a B  == {\ttlbrace}x. x=a{\ttrbrace} 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      == {\ttlbrace}x. x:A | x:B{\ttrbrace}

 \tdx{Int_def}           A Int B     == {\ttlbrace}x. x:A & x:B{\ttrbrace}

 \tdx{set_diff_def}      A - B       == {\ttlbrace}x. x:A & x~:B{\ttrbrace}

 \tdx{Compl_def}         -A          == {\ttlbrace}x. ~ x:A{\ttrbrace}

 \tdx{INTER_def}         INTER A B   == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace}

 \tdx{UNION_def}         UNION A B   == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace}

 \tdx{INTER1_def}        INTER1 B    == INTER {\ttlbrace}x. True{\ttrbrace} B 

 \tdx{UNION1_def}        UNION1 B    == UNION {\ttlbrace}x. True{\ttrbrace} B 

 \tdx{Inter_def}         Inter S     == (INT x:S. x)

 \tdx{Union_def}         Union S     == (UN  x:S. x)

 \tdx{Pow_def}           Pow A       == {\ttlbrace}B. B <= A{\ttrbrace}

 \tdx{image_def}         f``A        == {\ttlbrace}y. ? x:A. y=f x{\ttrbrace}

 \tdx{range_def}         range f     == {\ttlbrace}y. ? x. y=f x{\ttrbrace}

 \end{ttbox}

 \caption{Rules of the theory \texttt{Set}} \label{hol-set-rules}

 \end{figure}

 \begin{figure} \underscoreon

 \begin{ttbox}

 \tdx{CollectI}        [| P a |] ==> a : {\ttlbrace}x. P x{\ttrbrace}

 \tdx{CollectD}        [| a : {\ttlbrace}x. P x{\ttrbrace} |] ==> P a

 \tdx{CollectE}        [| a : {\ttlbrace}x. P x{\ttrbrace};  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 : {\ttlbrace}{\ttrbrace} ==> 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 : -A

 \tdx{ComplD}   [| c : -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

 \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

 \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 \texttt{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 constructions on functions: image~({\tt``})

 and \texttt{range}.

 %The predicate \cdx{inj_on} is used for simulating type definitions.

 %The statement ${\tt inj_on}~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{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_onI}  (!!x y. [| f x=f y; x:A; y:A |] ==> x=y) ==> inj_on f A

 %\tdx{inj_onD}  [| inj_on f A;  f x=f y;  x:A;  y:A |] ==> x=y

 %

 %\tdx{inj_on_inverseI}

 %    (!!x. x:A ==> g(f x) = x) ==> inj_on f A

 %\tdx{inj_on_contraD}

 %    [| inj_on 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 (-A) = {\ttlbrace}x. False{\ttrbrace}

 \tdx{Compl_partition}   A Un  (-A) = {\ttlbrace}x. True{\ttrbrace}

 \tdx{double_complement} -(-A) = A

 \tdx{Compl_Un}          -(A Un B)  = (-A) Int (-B)

 \tdx{Compl_Int}         -(A Int B) = (-A) Un (-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 \texttt{HOL/Set.ML} for proofs

 pertaining to set theory.

 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 \texttt{HOL/subset.ML}.

 Figure~\ref{hol-equalities} presents many common set equalities.  They

 include commutative, associative and distributive laws involving unions,

 intersections and complements.  For a complete listing see the file {\tt

 HOL/equalities.ML}.

 \begin{warn}

 \texttt{Blast_tac} proves many set-theoretic theorems automatically.

 Hence you seldom need to refer to the theorems above.

 \end{warn}

 \begin{figure}

 \begin{center}

 \begin{tabular}{rrr}

   \it name      &\it meta-type  & \it description \\ 

   \cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$

         & injective/surjective \\

   \cdx{inj_on}        & $[\alpha\To\beta ,\alpha\,set]\To bool$

         & injective over subset\\

   \cdx{inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & inverse function

 \end{tabular}

 \end{center}

 \underscoreon

 \begin{ttbox}

 \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_on_def}      inj_on f A == !x:A. !y:A. f x=f y --> x=y

 \tdx{inv_def}         inv f      == (\%y. @x. f(x)=y)

 \end{ttbox}

 \caption{Theory \thydx{Fun}} \label{fig:HOL:Fun}

 \end{figure}

 \subsection{Properties of functions}\nopagebreak

 Figure~\ref{fig:HOL:Fun} presents a theory of simple properties of functions.

 Note that ${\tt inv}~f$ uses Hilbert's $\varepsilon$ to yield an inverse

 of~$f$.  See the file \texttt{HOL/Fun.ML} for a complete listing of the derived

 rules.  Reasoning about function composition (the operator~\sdx{o}) and the

 predicate~\cdx{surj} is done simply by expanding the definitions.

 There is also a large collection of monotonicity theorems for constructions

 on sets in the file \texttt{HOL/mono.ML}.

 \section{Generic packages}

 \label{sec:HOL:generic-packages}

 HOL instantiates most of Isabelle's generic packages, making available the

 simplifier and the classical reasoner.

 \subsection{Simplification and substitution}

 Simplification tactics tactics such as \texttt{Asm_simp_tac} and \texttt{Full_simp_tac} use the default simpset

 (\texttt{simpset()}), which works for most purposes.  A quite minimal

 simplification set for higher-order logic is~\ttindexbold{HOL_ss};

 even more frugal is \ttindexbold{HOL_basic_ss}.  Equality~($=$), which

 also expresses logical equivalence, may be used for rewriting.  See

 the file \texttt{HOL/simpdata.ML} for a complete listing of the basic

 simplification rules.

 See \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%

 {Chaps.\ts\ref{substitution} and~\ref{simp-chap}} for details of substitution

 and simplification.

 \begin{warn}\index{simplification!of conjunctions}%

   Reducing $a=b\conj P(a)$ to $a=b\conj P(b)$ is sometimes advantageous.  The

   left part of a conjunction helps in simplifying the right part.  This effect

   is not available by default: it can be slow.  It can be obtained by

   including \ttindex{conj_cong} in a simpset, \verb$addcongs [conj_cong]$.

 \end{warn}

 \begin{warn}\index{simplification!of \texttt{if}}\label{if-simp}%

   By default only the condition of an \ttindex{if} is simplified but not the

   \texttt{then} and \texttt{else} parts. Of course the latter are simplified

   once the condition simplifies to \texttt{True} or \texttt{False}. To ensure

   full simplification of all parts of a conditional you must remove

   \ttindex{if_weak_cong} from the simpset, \verb$delcongs [if_weak_cong]$.

 \end{warn}

 If the simplifier cannot use a certain rewrite rule --- either because

 of nontermination or because its left-hand side is too flexible ---

 then you might try \texttt{stac}:

 \begin{ttdescription}

 \item[\ttindexbold{stac} $thm$ $i,$] where $thm$ is of the form $lhs = rhs$,

   replaces in subgoal $i$ instances of $lhs$ by corresponding instances of

   $rhs$.  In case of multiple instances of $lhs$ in subgoal $i$, backtracking

   may be necessary to select the desired ones.

 If $thm$ is a conditional equality, the instantiated condition becomes an

 additional (first) subgoal.

 \end{ttdescription}

 HOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for an

 equality throughout a subgoal and its hypotheses.  This tactic uses HOL's

 general substitution rule.

 \subsubsection{Case splitting}

 \label{subsec:HOL:case:splitting}

 HOL also provides convenient means for case splitting during rewriting. Goals

 containing a subterm of the form \texttt{if}~$b$~{\tt then\dots else\dots}

 often require a case distinction on $b$. This is expressed by the theorem

 \tdx{split_if}:

 $$

 \Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~

 ((\Var{b} \to \Var{P}(\Var{x})) \land (\lnot \Var{b} \to \Var{P}(\Var{y})))

 \eqno{(*)}

 $$

 For example, a simple instance of $(*)$ is

 \[

 x \in (\mbox{\tt if}~x \in A~{\tt then}~A~\mbox{\tt else}~\{x\})~=~

 ((x \in A \to x \in A) \land (x \notin A \to x \in \{x\}))

 \]

 Because $(*)$ is too general as a rewrite rule for the simplifier (the

 left-hand side is not a higher-order pattern in the sense of

 \iflabelundefined{chap:simplification}{the {\em Reference Manual\/}}%

 {Chap.\ts\ref{chap:simplification}}), there is a special infix function 

 \ttindexbold{addsplits} of type \texttt{simpset * thm list -> simpset}

 (analogous to \texttt{addsimps}) that adds rules such as $(*)$ to a

 simpset, as in

 \begin{ttbox}

 by(simp_tac (simpset() addsplits [split_if]) 1);

 \end{ttbox}

 The effect is that after each round of simplification, one occurrence of

 \texttt{if} is split acording to \texttt{split_if}, until all occurences of

 \texttt{if} have been eliminated.

 It turns out that using \texttt{split_if} is almost always the right thing to

 do. Hence \texttt{split_if} is already included in the default simpset. If

 you want to delete it from a simpset, use \ttindexbold{delsplits}, which is

 the inverse of \texttt{addsplits}:

 \begin{ttbox}

 by(simp_tac (simpset() delsplits [split_if]) 1);

 \end{ttbox}

 In general, \texttt{addsplits} accepts rules of the form

 \[

 \Var{P}(c~\Var{x@1}~\dots~\Var{x@n})~=~ rhs

 \]

 where $c$ is a constant and $rhs$ is arbitrary. Note that $(*)$ is of the

 right form because internally the left-hand side is

 $\Var{P}(\mathtt{If}~\Var{b}~\Var{x}~~\Var{y})$. Important further examples

 are splitting rules for \texttt{case} expressions (see~{\S}\ref{subsec:list}

 and~{\S}\ref{subsec:datatype:basics}).

 Analogous to \texttt{Addsimps} and \texttt{Delsimps}, there are also

 imperative versions of \texttt{addsplits} and \texttt{delsplits}

 \begin{ttbox}

 \ttindexbold{Addsplits}: thm list -> unit

 \ttindexbold{Delsplits}: thm list -> unit

 \end{ttbox}

 for adding splitting rules to, and deleting them from the current simpset.

 \subsection{Classical reasoning}

 HOL derives classical introduction rules for $\disj$ and~$\exists$, as well as

 classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule; recall

 Fig.\ts\ref{hol-lemmas2} above.

 The classical reasoner is installed.  Tactics such as \texttt{Blast_tac} and

 {\tt Best_tac} refer to the default claset (\texttt{claset()}), which works

 for most purposes.  Named clasets include \ttindexbold{prop_cs}, which

 includes the propositional rules, and \ttindexbold{HOL_cs}, which also

 includes quantifier rules.  See the file \texttt{HOL/cladata.ML} for lists of

 the classical rules,

 and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}%

 {Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods.

 \section{Calling the decision procedure SVC}\label{sec:HOL:SVC}

 \index{SVC decision procedure|(}

 The Stanford Validity Checker (SVC) is a tool that can check the validity of

 certain types of formulae.  If it is installed on your machine, then

 Isabelle/HOL can be configured to call it through the tactic

 \ttindex{svc_tac}.  It is ideal for large tautologies and complex problems in

 linear arithmetic.  Subexpressions that SVC cannot handle are automatically

 replaced by variables, so you can call the tactic on any subgoal.  See the

 file \texttt{HOL/ex/svc_test.ML} for examples.

 \begin{ttbox} 

 svc_tac   : int -> tactic

 Svc.trace : bool ref      \hfill{\bf initially false}

 \end{ttbox}

 \begin{ttdescription}

 \item[\ttindexbold{svc_tac} $i$] attempts to prove subgoal~$i$ by translating

   it into a formula recognized by~SVC\@.  If it succeeds then the subgoal is

   removed.  It fails if SVC is unable to prove the subgoal.  It crashes with

   an error message if SVC appears not to be installed.  Numeric variables may

   have types \texttt{nat}, \texttt{int} or \texttt{real}.

 \item[\ttindexbold{Svc.trace}] is a flag that, if set, causes \texttt{svc_tac}

   to trace its operations: abstraction of the subgoal, translation to SVC

   syntax, SVC's response.

 \end{ttdescription}

 Here is an example, with tracing turned on:

 \begin{ttbox}

 set Svc.trace;

 {\out val it : bool = true}

 Goal "(#3::nat)*a <= #2 + #4*b + #6*c  & #11 <= #2*a + b + #2*c & \ttback

 \ttback     a + #3*b <= #5 + #2*c  --> #2 + #3*b <= #2*a + #6*c";

 by (svc_tac 1);

 {\out Subgoal abstracted to}

 {\out #3 * a <= #2 + #4 * b + #6 * c &}

 {\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->}

 {\out #2 + #3 * b <= #2 * a + #6 * c}

 {\out Calling SVC:}

 {\out (=> (<= 0  (F_c) )  (=> (<= 0  (F_b) )  (=> (<= 0  (F_a) )}

 {\out   (=> (AND (<= {* 3  (F_a) }  {+ {+ 2  {* 4  (F_b) } }  }

 {\out {* 6  (F_c) } } )  (AND (<= 11  {+ {+ {* 2  (F_a) }  (F_b) }}

 {\out   {* 2  (F_c) } } )  (<= {+ (F_a)  {* 3  (F_b) } }  {+ 5  }

 {\out {* 2  (F_c) } } ) ) )  (< {+ 2  {* 3  (F_b) } }  {+ 1  {+ }

 {\out {* 2  (F_a) }  {* 6  (F_c) } } } ) ) ) ) ) }

 {\out SVC Returns:}

 {\out VALID}

 {\out Level 1}

 {\out #3 * a <= #2 + #4 * b + #6 * c &}

 {\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c -->}

 {\out #2 + #3 * b <= #2 * a + #6 * c}

 {\out No subgoals!}

 \end{ttbox}

 \begin{warn}

 Calling \ttindex{svc_tac} entails an above-average risk of

 unsoundness.  Isabelle does not check SVC's result independently.  Moreover,

 the tactic translates the submitted formula using code that lies outside

 Isabelle's inference core.  Theorems that depend upon results proved using SVC

 (and other oracles) are displayed with the annotation \texttt{[!]} attached.

 You can also use \texttt{\#der (rep_thm $th$)} to examine the proof object of

 theorem~$th$, as described in the \emph{Reference Manual}.  

 \end{warn}

 To start, first download SVC from the Internet at URL

 \begin{ttbox}

 http://agamemnon.stanford.edu/~levitt/vc/index.html

 \end{ttbox}

 and install it using the instructions supplied.  SVC requires two environment

 variables:

 \begin{ttdescription}

 \item[\ttindexbold{SVC_HOME}] is an absolute pathname to the SVC

     distribution directory. 

   \item[\ttindexbold{SVC_MACHINE}] identifies the type of computer and

     operating system.  

 \end{ttdescription}

 You can set these environment variables either using the Unix shell or through

 an Isabelle \texttt{settings} file.  Isabelle assumes SVC to be installed if

 \texttt{SVC_HOME} is defined.

 \paragraph*{Acknowledgement.}  This interface uses code supplied by S{\o}ren

 Heilmann.

 \index{SVC decision procedure|)}

 \section{Types}\label{sec:HOL:Types}

 This section describes HOL's basic predefined types ($\alpha \times \beta$,

 $\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for introducing new

 types in general.  The most important type construction, the

 \texttt{datatype}, is treated separately in {\S}\ref{sec:HOL:datatype}.

 \subsection{Product and sum types}\index{*"* type}\index{*"+ type}

 \label{subsec:prod-sum}

 \begin{figure}[htbp]

 \begin{constants}

   \it symbol    & \it meta-type &           & \it description \\ 

   \cdx{Pair}    & $[\alpha,\beta]\To \alpha\times\beta$

         & & ordered pairs $(a,b)$ \\

   \cdx{fst}     & $\alpha\times\beta \To \alpha$        & & first projection\\

   \cdx{snd}     & $\alpha\times\beta \To \beta$         & & second projection\\

   \cdx{split}   & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$ 

         & & generalized projection\\

   \cdx{Sigma}  & 

         $[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &

         & general sum of sets

 \end{constants}

 \begin{ttbox}\makeatletter

 %\tdx{fst_def}      fst p     == @a. ? b. p = (a,b)

 %\tdx{snd_def}      snd p     == @b. ? a. p = (a,b)

 %\tdx{split_def}    split c p == c (fst p) (snd p)

 \tdx{Sigma_def}    Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace}

 \tdx{Pair_eq}      ((a,b) = (a',b')) = (a=a' & b=b')

 \tdx{Pair_inject}  [| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R

 \tdx{PairE}        [| !!x y. p = (x,y) ==> Q |] ==> Q

 \tdx{fst_conv}     fst (a,b) = a

 \tdx{snd_conv}     snd (a,b) = b

 \tdx{surjective_pairing}  p = (fst p,snd p)

 \tdx{split}        split c (a,b) = c a b

 \tdx{split_split}  R(split c p) = (! x y. p = (x,y) --> R(c x y))

 \tdx{SigmaI}    [| a:A;  b:B a |] ==> (a,b) : Sigma A B

 \tdx{SigmaE}    [| c:Sigma A B; !!x y.[| x:A; y:B x; c=(x,y) |] ==> P 

           |] ==> P

 \end{ttbox}

 \caption{Type $\alpha\times\beta$}\label{hol-prod}

 \end{figure} 

 Theory \thydx{Prod} (Fig.\ts\ref{hol-prod}) defines the product type

 $\alpha\times\beta$, with the ordered pair syntax $(a, b)$.  General

 tuples are simulated by pairs nested to the right:

 \begin{center}

 \begin{tabular}{c|c}

 external & internal \\

 \hline

 $\tau@1 \times \dots \times \tau@n$ & $\tau@1 \times (\dots (\tau@{n-1} \times \tau@n)\dots)$ \\

 \hline

 $(t@1,\dots,t@n)$ & $(t@1,(\dots,(t@{n-1},t@n)\dots)$ \\

 \end{tabular}

 \end{center}

 In addition, it is possible to use tuples

 as patterns in abstractions:

 \begin{center}

 {\tt\%($x$,$y$). $t$} \quad stands for\quad \texttt{split(\%$x$\thinspace$y$.\ $t$)} 

 \end{center}

 Nested patterns are also supported.  They are translated stepwise:

 \begin{eqnarray*}

 \hbox{\tt\%($x$,$y$,$z$).\ $t$} 

    & \leadsto & \hbox{\tt\%($x$,($y$,$z$)).\ $t$} \\

    & \leadsto & \hbox{\tt split(\%$x$.\%($y$,$z$).\ $t$)}\\

    & \leadsto & \hbox{\tt split(\%$x$.\ split(\%$y$ $z$.\ $t$))}

 \end{eqnarray*}

 The reverse translation is performed upon printing.

 \begin{warn}

   The translation between patterns and \texttt{split} is performed automatically

   by the parser and printer.  Thus the internal and external form of a term

   may differ, which can affects proofs.  For example the term {\tt

   (\%(x,y).(y,x))(a,b)} requires the theorem \texttt{split} (which is in the

   default simpset) to rewrite to {\tt(b,a)}.

 \end{warn}

 In addition to explicit $\lambda$-abstractions, patterns can be used in any

 variable binding construct which is internally described by a

 $\lambda$-abstraction.  Some important examples are

 \begin{description}

 \item[Let:] \texttt{let {\it pattern} = $t$ in $u$}

 \item[Quantifiers:] \texttt{ALL~{\it pattern}:$A$.~$P$}

 \item[Choice:] {\underscoreon \tt SOME~{\it pattern}.~$P$}

 \item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$}

 \item[Sets:] \texttt{{\ttlbrace}{\it pattern}.~$P${\ttrbrace}}

 \end{description}

 There is a simple tactic which supports reasoning about patterns:

 \begin{ttdescription}

 \item[\ttindexbold{split_all_tac} $i$] replaces in subgoal $i$ all

   {\tt!!}-quantified variables of product type by individual variables for

   each component.  A simple example:

 \begin{ttbox}

 {\out 1. !!p. (\%(x,y,z). (x, y, z)) p = p}

 by(split_all_tac 1);

 {\out 1. !!x xa ya. (\%(x,y,z). (x, y, z)) (x, xa, ya) = (x, xa, ya)}

 \end{ttbox}

 \end{ttdescription}

 Theory \texttt{Prod} also introduces the degenerate product type \texttt{unit}

 which contains only a single element named {\tt()} with the property

 \begin{ttbox}

 \tdx{unit_eq}       u = ()

 \end{ttbox}

 \bigskip

 Theory \thydx{Sum} (Fig.~\ref{hol-sum}) defines the sum type $\alpha+\beta$

 which associates to the right and has a lower priority than $*$: $\tau@1 +

 \tau@2 + \tau@3*\tau@4$ means $\tau@1 + (\tau@2 + (\tau@3*\tau@4))$.

 The definition of products and sums in terms of existing types is not

 shown.  The constructions are fairly standard and can be found in the

 respective theory files. Although the sum and product types are

 constructed manually for foundational reasons, they are represented as

 actual datatypes later (see {\S}\ref{subsec:datatype:rep_datatype}).

 Therefore, the theory \texttt{Datatype} should be used instead of

 \texttt{Sum} or \texttt{Prod}.

 \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{Inl_not_Inr}    Inl a ~= Inr b

 \tdx{inj_Inl}        inj Inl

 \tdx{inj_Inr}        inj Inr

 \tdx{sumE}           [| !!x. P(Inl x);  !!y. 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. f(Inl x)) (\%y. f(Inr y)) s = f s

 \tdx{sum.split_case} R(sum_case f g s) = ((! x. s = Inl(x) --> R(f(x))) &

                                      (! y. s = Inr(y) --> R(g(y))))

 \end{ttbox}

 \caption{Type $\alpha+\beta$}\label{hol-sum}

 \end{figure}

 \begin{figure}

 \index{*"< symbol}

 \index{*"* symbol}

 \index{*div symbol}

 \index{*mod symbol}

 \index{*dvd symbol}

 \index{*"+ symbol}

 \index{*"- symbol}

 \begin{constants}

   \it symbol    & \it meta-type & \it priority & \it description \\ 

   \cdx{0}       & $\alpha$  & & zero \\

   \cdx{Suc}     & $nat \To nat$ & & successor function\\

   \tt *    & $[\alpha,\alpha]\To \alpha$    &  Left 70 & multiplication \\

   \tt div  & $[\alpha,\alpha]\To \alpha$    &  Left 70 & division\\

   \tt mod  & $[\alpha,\alpha]\To \alpha$    &  Left 70 & modulus\\

   \tt dvd  & $[\alpha,\alpha]\To bool$     &  Left 70 & ``divides'' relation\\

   \tt +    & $[\alpha,\alpha]\To \alpha$    &  Left 65 & addition\\

   \tt -    & $[\alpha,\alpha]\To \alpha$    &  Left 65 & subtraction

 \end{constants}

 \subcaption{Constants and infixes}

 \begin{ttbox}\makeatother

 \tdx{nat_induct}     [| P 0; !!n. P n ==> P(Suc n) |]  ==> P n

 \tdx{Suc_not_Zero}   Suc m ~= 0

 \tdx{inj_Suc}        inj Suc

 \tdx{n_not_Suc_n}    n~=Suc n

 \subcaption{Basic properties}

 \end{ttbox}

 \caption{The type of natural numbers, \tydx{nat}} \label{hol-nat1}

 \end{figure}

 \begin{figure}

 \begin{ttbox}\makeatother

               0+n           = n

               (Suc m)+n     = Suc(m+n)

               m-0           = m

               0-n           = n

               Suc(m)-Suc(n) = m-n

               0*n           = 0

               Suc(m)*n      = n + m*n

 \tdx{mod_less}      m<n ==> m mod n = m

 \tdx{mod_geq}       [| 0<n;  ~m<n |] ==> m mod n = (m-n) mod n

 \tdx{div_less}      m<n ==> m div n = 0

 \tdx{div_geq}       [| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)

 \end{ttbox}

 \caption{Recursion equations for the arithmetic operators} \label{hol-nat2}

 \end{figure}

 \subsection{The type of natural numbers, \textit{nat}}

 \index{nat@{\textit{nat}} type|(}

 The theory \thydx{NatDef} defines the natural numbers in a roundabout but

 traditional way.  The axiom of infinity postulates a 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.  This is a least

 fixedpoint construction.  For details see the file \texttt{NatDef.thy}.

 Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the overloaded

 functions of this class (especially \cdx{<} and \cdx{<=}, but also \cdx{min},

 \cdx{max} and \cdx{LEAST}) available on \tydx{nat}.  Theory \thydx{Nat} builds

 on \texttt{NatDef} and shows that {\tt<=} is a linear order, so \tydx{nat} is

 also an instance of class \cldx{linorder}.

 Theory \thydx{Arith} develops arithmetic on the natural numbers.  It defines

 addition, multiplication and subtraction.  Theory \thydx{Divides} defines

 division, remainder and the ``divides'' relation.  The numerous theorems

 proved include commutative, associative, distributive, identity and

 cancellation laws.  See Figs.\ts\ref{hol-nat1} and~\ref{hol-nat2}.  The

 recursion equations for the operators \texttt{+}, \texttt{-} and \texttt{*} on

 \texttt{nat} are part of the default simpset.

 Functions on \tydx{nat} can be defined by primitive or well-founded recursion;

 see {\S}\ref{sec:HOL:recursive}.  A simple example is addition.

 Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following

 the standard convention.

 \begin{ttbox}

 \sdx{primrec}

       "0 + n = n"

   "Suc m + n = Suc (m + n)"

 \end{ttbox}

 There is also a \sdx{case}-construct

 of the form

 \begin{ttbox}

 case \(e\) of 0 => \(a\) | Suc \(m\) => \(b\)

 \end{ttbox}

 Note that Isabelle insists on precisely this format; you may not even change

 the order of the two cases.

 Both \texttt{primrec} and \texttt{case} are realized by a recursion operator

 \cdx{nat_rec}, which is available because \textit{nat} is represented as

 a datatype (see {\S}\ref{subsec:datatype:rep_datatype}).

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

 Tactic {\tt\ttindex{induct_tac} "$n$" $i$} performs induction on variable~$n$

 in subgoal~$i$ using theorem \texttt{nat_induct}.  There is also the derived

 theorem \tdx{less_induct}:

 \begin{ttbox}

 [| !!n. [| ! m. m<n --> P m |] ==> P n |]  ==>  P n

 \end{ttbox}

 \subsection{Numerical types and numerical reasoning}

 The integers (type \tdx{int}) are also available in HOL, and the reals (type

 \tdx{real}) are available in the logic image \texttt{HOL-Real}.  They support

 the expected operations of addition (\texttt{+}), subtraction (\texttt{-}) and

 multiplication (\texttt{*}), and much else.  Type \tdx{int} provides the

 \texttt{div} and \texttt{mod} operators, while type \tdx{real} provides real

 division and other operations.  Both types belong to class \cldx{linorder}, so

 they inherit the relational operators and all the usual properties of linear

 orderings.  For full details, please survey the theories in subdirectories

 \texttt{Integ} and \texttt{Real}.

 All three numeric types admit numerals of the form \texttt{\#$sd\ldots d$},

 where $s$ is an optional minus sign and $d\ldots d$ is a string of digits.

 Numerals are represented internally by a datatype for binary notation, which

 allows numerical calculations to be performed by rewriting.  For example, the

 integer division of \texttt{\#54342339} by \texttt{\#3452} takes about five

 seconds.  By default, the simplifier cancels like terms on the opposite sites

 of relational operators (reducing \texttt{z+x<x+y} to \texttt{z<y}, for

 instance.  The simplifier also collects like terms, replacing

 \texttt{x+y+x*\#3} by \texttt{\#4*x+y}.

 Sometimes numerals are not wanted, because for example \texttt{n+\#3} does not

 match a pattern of the form \texttt{Suc $k$}.  You can re-arrange the form of

 an arithmetic expression by proving (via \texttt{subgoal_tac}) a lemma such

 as \texttt{n+\#3 = Suc (Suc (Suc n))}.  As an alternative, you can disable the

 fancier simplifications by using a basic simpset such as \texttt{HOL_ss}

 rather than the default one, \texttt{simpset()}.

 Reasoning about arithmetic inequalities can be tedious.  Fortunately HOL

 provides a decision procedure for quantifier-free linear arithmetic (that is,

 addition and subtraction). The simplifier invokes a weak version of this

 decision procedure automatically. If this is not sufficent, you can invoke the

 full procedure \ttindex{arith_tac} explicitly.  It copes with arbitrary

 formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt-}, {\tt Suc}, {\tt

   min}, {\tt max} and numerical constants; other subterms are treated as

 atomic; subformulae not involving numerical types are ignored; quantified

 subformulae are ignored unless they are positive universal or negative

 existential. Note that the running time is exponential in the number of

 occurrences of {\tt min}, {\tt max}, and {\tt-} because they require case

 distinctions. Note also that \texttt{arith_tac} is not complete: if

 divisibility plays a role, it may fail to prove a valid formula, for example

 $m+m \neq n+n+1$. Fortunately such examples are rare in practice.

 If \texttt{arith_tac} fails you, try to find relevant arithmetic results in

 the library.  The theory \texttt{NatDef} contains theorems about {\tt<} and

 {\tt<=}, the theory \texttt{Arith} contains theorems about \texttt{+},

 \texttt{-} and \texttt{*}, and theory \texttt{Divides} contains theorems about

 \texttt{div} and \texttt{mod}.  Use \texttt{thms_containing} or the

 \texttt{find}-functions to locate them (see the {\em Reference Manual\/}).

 \index{nat@{\textit{nat}} type|)}

 \begin{figure}

 \index{#@{\tt[]} symbol}

 \index{#@{\tt\#} symbol}

 \index{"@@{\tt\at} symbol}

 \index{*"! symbol}

 \begin{constants}

   \it symbol & \it meta-type & \it priority & \it description \\

   \tt[]    & $\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{last}    & $\alpha\,list \To \alpha$ & & last element \\

   \cdx{butlast} & $\alpha\,list \To \alpha\,list$ & & drop last element \\

   \tt\at  & $[\alpha\,list,\alpha\,list]\To \alpha\,list$ & Left 65 & append \\

   \cdx{map}     & $(\alpha\To\beta) \To (\alpha\,list \To \beta\,list)$

         & & apply to all\\

   \cdx{filter}  & $(\alpha \To bool) \To (\alpha\,list \To \alpha\,list)$

         & & filter functional\\

   \cdx{set}& $\alpha\,list \To \alpha\,set$ & & elements\\

   \sdx{mem}  & $\alpha \To \alpha\,list \To bool$  &  Left 55   & membership\\

   \cdx{foldl}   & $(\beta\To\alpha\To\beta) \To \beta \To \alpha\,list \To \beta$ &

   & iteration \\

   \cdx{concat}   & $(\alpha\,list)list\To \alpha\,list$ & & concatenation \\

   \cdx{rev}     & $\alpha\,list \To \alpha\,list$ & & reverse \\

   \cdx{length}  & $\alpha\,list \To nat$ & & length \\

   \tt! & $\alpha\,list \To nat \To \alpha$ & Left 100 & indexing \\

   \cdx{take}, \cdx{drop} & $nat \To \alpha\,list \To \alpha\,list$ &&

     take/drop a prefix \\

   \cdx{takeWhile},\\

   \cdx{dropWhile} &

     $(\alpha \To bool) \To \alpha\,list \To \alpha\,list$ &&

     take/drop a prefix

 \end{constants}

 \subcaption{Constants and infixes}

 \begin{center} \tt\frenchspacing

 \begin{tabular}{rrr} 

   \it external        & \it internal  & \it description \\{}

   [$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}

 \caption{The theory \thydx{List}} \label{hol-list}

 \end{figure}

 \begin{figure}

 \begin{ttbox}\makeatother

 null [] = True

 null (x#xs) = False

 hd (x#xs) = x

 tl (x#xs) = xs

 tl [] = []

 [] @ ys = ys

 (x#xs) @ ys = x # xs @ ys

 set [] = \ttlbrace\ttrbrace

 set (x#xs) = insert x (set xs)

 x mem [] = False

 x mem (y#ys) = (if y=x then True else x mem ys)

 concat([]) = []

 concat(x#xs) = x @ concat(xs)

 rev([]) = []

 rev(x#xs) = rev(xs) @ [x]

 length([]) = 0

 length(x#xs) = Suc(length(xs))

 xs!0 = hd xs

 xs!(Suc n) = (tl xs)!n

 \end{ttbox}

 \caption{Simple list processing functions}

 \label{fig:HOL:list-simps}

 \end{figure}

 \begin{figure}

 \begin{ttbox}\makeatother

 map f [] = []

 map f (x#xs) = f x # map f xs

 filter P [] = []

 filter P (x#xs) = (if P x then x#filter P xs else filter P xs)

 foldl f a [] = a

 foldl f a (x#xs) = foldl f (f a x) xs

 take n [] = []

 take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)

 drop n [] = []

 drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)

 takeWhile P [] = []

 takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])

 dropWhile P [] = []

 dropWhile P (x#xs) = (if P x then dropWhile P xs else xs)

 \end{ttbox}

 \caption{Further list processing functions}

 \label{fig:HOL:list-simps2}

 \end{figure}

 \subsection{The type constructor for lists, \textit{list}}

 \label{subsec:list}

 \index{list@{\textit{list}} type|(}

 Figure~\ref{hol-list} presents the theory \thydx{List}: the basic list

 operations with their types and syntax.  Type $\alpha \; list$ is

 defined as a \texttt{datatype} with the constructors {\tt[]} and {\tt\#}.

 As a result the generic structural induction and case analysis tactics

 \texttt{induct\_tac} and \texttt{cases\_tac} also become available for

 lists.  A \sdx{case} construct of the form

 \begin{center}\tt

 case $e$ of [] => $a$  |  \(x\)\#\(xs\) => b

 \end{center}

 is defined by translation.  For details see~{\S}\ref{sec:HOL:datatype}. There

 is also a case splitting rule \tdx{split_list_case}

 \[

 \begin{array}{l}

 P(\mathtt{case}~e~\mathtt{of}~\texttt{[] =>}~a ~\texttt{|}~

                x\texttt{\#}xs~\texttt{=>}~f~x~xs) ~= \\

 ((e = \texttt{[]} \to P(a)) \land

  (\forall x~ xs. e = x\texttt{\#}xs \to P(f~x~xs)))

 \end{array}

 \]

 which can be fed to \ttindex{addsplits} just like

 \texttt{split_if} (see~{\S}\ref{subsec:HOL:case:splitting}).

 \texttt{List} provides a basic library of list processing functions defined by

 primitive recursion (see~{\S}\ref{sec:HOL:primrec}).  The recursion equations

 are shown in Figs.\ts\ref{fig:HOL:list-simps} and~\ref{fig:HOL:list-simps2}.

 \index{list@{\textit{list}} type|)}

 \subsection{Introducing new types} \label{sec:typedef}

 The HOL-methodology dictates that all extensions to a theory should be

 \textbf{definitional}.  The type definition mechanism that meets this

 criterion is \ttindex{typedef}.  Note that \emph{type synonyms}, which are

 inherited from Pure and described elsewhere, are just syntactic abbreviations

 that have no logical meaning.

 \begin{warn}

   Types in HOL must be non-empty; otherwise the quantifier rules would be

   unsound, because $\exists x. x=x$ is a theorem \cite[{\S}7]{paulson-COLOG}.

 \end{warn}

 A \bfindex{type definition} identifies the new type with a subset of

 an existing type.  More precisely, the new type is defined by

 exhibiting an existing type~$\tau$, a set~$A::\tau\,set$, and a

 theorem of the form $x:A$.  Thus~$A$ is a non-empty subset of~$\tau$,

 and the new type denotes this subset.  New functions are defined that

 establish an isomorphism between the new type and the subset.  If

 type~$\tau$ involves type variables $\alpha@1$, \ldots, $\alpha@n$,

 then the type definition creates a type constructor

 $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular type.

 \begin{figure}[htbp]

 \begin{rail}

 typedef  : 'typedef' ( () | '(' name ')') type '=' set witness;

 type    : typevarlist name ( () | '(' infix ')' );

 set     : string;

 witness : () | '(' id ')';

 \end{rail}

 \caption{Syntax of type definitions}

 \label{fig:HOL:typedef}

 \end{figure}

 The syntax for type definitions is shown in Fig.~\ref{fig:HOL:typedef}.  For

 the definition of `typevarlist' and `infix' see

 \iflabelundefined{chap:classical}

 {the appendix of the {\em Reference Manual\/}}%

 {Appendix~\ref{app:TheorySyntax}}.  The remaining nonterminals have the

 following meaning:

 \begin{description}

 \item[\it type:] the new type constructor $(\alpha@1,\dots,\alpha@n)ty$ with

   optional infix annotation.

 \item[\it name:] an alphanumeric name $T$ for the type constructor

   $ty$, in case $ty$ is a symbolic name.  Defaults to $ty$.

 \item[\it set:] the representing subset $A$.

 \item[\it witness:] name of a theorem of the form $a:A$ proving

   non-emptiness.  It can be omitted in case Isabelle manages to prove

   non-emptiness automatically.

 \end{description}

 If all context conditions are met (no duplicate type variables in

 `typevarlist', no extra type variables in `set', and no free term variables

 in `set'), the following components are added to the theory:

 \begin{itemize}

 \item a type $ty :: (term,\dots,term)term$

 \item constants

 \begin{eqnarray*}

 T &::& \tau\;set \\

 Rep_T &::& (\alpha@1,\dots,\alpha@n)ty \To \tau \\

 Abs_T &::& \tau \To (\alpha@1,\dots,\alpha@n)ty

 \end{eqnarray*}

 \item a definition and three axioms

 \[

 \begin{array}{ll}

 T{\tt_def} & T \equiv A \\

 {\tt Rep_}T & Rep_T\,x \in T \\

 {\tt Rep_}T{\tt_inverse} & Abs_T\,(Rep_T\,x) = x \\

 {\tt Abs_}T{\tt_inverse} & y \in T \Imp Rep_T\,(Abs_T\,y) = y

 \end{array}

 \]

 stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$

 and its inverse $Abs_T$.

 \end{itemize}

 Below are two simple examples of HOL type definitions.  Non-emptiness is

 proved automatically here.

 \begin{ttbox}

 typedef unit = "{\ttlbrace}True{\ttrbrace}"

 typedef (prod)

   ('a, 'b) "*"    (infixr 20)

       = "{\ttlbrace}f . EX (a::'a) (b::'b). f = (\%x y. x = a & y = b){\ttrbrace}"

 \end{ttbox}

 Type definitions permit the introduction of abstract data types in a safe

 way, namely by providing models based on already existing types.  Given some

 abstract axiomatic description $P$ of a type, this involves two steps:

 \begin{enumerate}

 \item Find an appropriate type $\tau$ and subset $A$ which has the desired

   properties $P$, and make a type definition based on this representation.

 \item Prove that $P$ holds for $ty$ by lifting $P$ from the representation.

 \end{enumerate}

 You can now forget about the representation and work solely in terms of the

 abstract properties $P$.

 \begin{warn}

 If you introduce a new type (constructor) $ty$ axiomatically, i.e.\ by

 declaring the type and its operations and by stating the desired axioms, you

 should make sure the type has a non-empty model.  You must also have a clause

 \par

 \begin{ttbox}

 arities \(ty\) :: (term,\thinspace\(\dots\),{\thinspace}term){\thinspace}term

 \end{ttbox}

 in your theory file to tell Isabelle that $ty$ is in class \texttt{term}, the

 class of all HOL types.

 \end{warn}

 \section{Records}

 At a first approximation, records are just a minor generalisation of tuples,

 where components may be addressed by labels instead of just position (think of

 {\ML}, for example).  The version of records offered by Isabelle/HOL is

 slightly more advanced, though, supporting \emph{extensible record schemes}.

 This admits operations that are polymorphic with respect to record extension,

 yielding ``object-oriented'' effects like (single) inheritance.  See also

 \cite{NaraschewskiW-TPHOLs98} for more details on object-oriented

 verification and record subtyping in HOL.

 \subsection{Basics}

 Isabelle/HOL supports fixed and schematic records both at the level of terms

 and types.  The concrete syntax is as follows:

 \begin{center}

 \begin{tabular}{l|l|l}

   & record terms & record types \\ \hline

   fixed & $\record{x = a\fs y = b}$ & $\record{x \ty A\fs y \ty B}$ \\

   schematic & $\record{x = a\fs y = b\fs \more = m}$ &

     $\record{x \ty A\fs y \ty B\fs \more \ty M}$ \\

 \end{tabular}

 \end{center}

 \noindent The \textsc{ascii} representation of $\record{x = a}$ is \texttt{(| x = a |)}.

 A fixed record $\record{x = a\fs y = b}$ has field $x$ of value $a$ and field

 $y$ of value $b$.  The corresponding type is $\record{x \ty A\fs y \ty B}$,

 assuming that $a \ty A$ and $b \ty B$.

 A record scheme like $\record{x = a\fs y = b\fs \more = m}$ contains fields

 $x$ and $y$ as before, but also possibly further fields as indicated by the

 ``$\more$'' notation (which is actually part of the syntax).  The improper

 field ``$\more$'' of a record scheme is called the \emph{more part}.

 Logically it is just a free variable, which is occasionally referred to as

 \emph{row variable} in the literature.  The more part of a record scheme may

 be instantiated by zero or more further components.  For example, above scheme

 might get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more = m'}$,

 where $m'$ refers to a different more part.  Fixed records are special

 instances of record schemes, where ``$\more$'' is properly terminated by the

 $() :: unit$ element.  Actually, $\record{x = a\fs y = b}$ is just an

 abbreviation for $\record{x = a\fs y = b\fs \more = ()}$.

 \medskip

 There are two key features that make extensible records in a simply typed

 language like HOL feasible:

 \begin{enumerate}

 \item the more part is internalised, as a free term or type variable,

 \item field names are externalised, they cannot be accessed within the logic

   as first-class values.

 \end{enumerate}

 \medskip

 In Isabelle/HOL record types have to be defined explicitly, fixing their field

 names and types, and their (optional) parent record (see

 {\S}\ref{sec:HOL:record-def}).  Afterwards, records may be formed using above

 syntax, while obeying the canonical order of fields as given by their

 declaration.  The record package also provides several operations like

 selectors and updates (see {\S}\ref{sec:HOL:record-ops}), together with

 characteristic properties (see {\S}\ref{sec:HOL:record-thms}).

 There is an example theory demonstrating most basic aspects of extensible

 records (see theory \texttt{HOL/ex/Records} in the Isabelle sources).

 \subsection{Defining records}\label{sec:HOL:record-def}

 The theory syntax for record type definitions is shown in

 Fig.~\ref{fig:HOL:record}.  For the definition of `typevarlist' and `type' see

 \iflabelundefined{chap:classical}

 {the appendix of the {\em Reference Manual\/}}%

 {Appendix~\ref{app:TheorySyntax}}.

 \begin{figure}[htbp]

 \begin{rail}

 record  : 'record' typevarlist name '=' parent (field +);

 parent  : ( () | type '+');

 field   : name '::' type;

 \end{rail}

 \caption{Syntax of record type definitions}

 \label{fig:HOL:record}

 \end{figure}

 A general \ttindex{record} specification is of the following form:

 \[

 \mathtt{record}~(\alpha@1, \dots, \alpha@n) \, t ~=~

   (\tau@1, \dots, \tau@m) \, s ~+~ c@1 :: \sigma@1 ~ \dots ~ c@l :: \sigma@l

 \]

 where $\vec\alpha@n$ are distinct type variables, and $\vec\tau@m$,

 $\vec\sigma@l$ are types containing at most variables from $\vec\alpha@n$.

 Type constructor $t$ has to be new, while $s$ has to specify an existing

 record type.  Furthermore, the $\vec c@l$ have to be distinct field names.

 There has to be at least one field.

 In principle, field names may never be shared with other records.  This is no

 actual restriction in practice, since $\vec c@l$ are internally declared

 within a separate name space qualified by the name $t$ of the record.

 \medskip

 Above definition introduces a new record type $(\vec\alpha@n) \, t$ by

 extending an existing one $(\vec\tau@m) \, s$ by new fields $\vec c@l \ty

 \vec\sigma@l$.  The parent record specification is optional, by omitting it

 $t$ becomes a \emph{root record}.  The hierarchy of all records declared

 within a theory forms a forest structure, i.e.\ a set of trees, where any of

 these is rooted by some root record.

 For convenience, $(\vec\alpha@n) \, t$ is made a type abbreviation for the

 fixed record type $\record{\vec c@l \ty \vec\sigma@l}$, and $(\vec\alpha@n,

 \zeta) \, t_scheme$ is made an abbreviation for $\record{\vec c@l \ty

   \vec\sigma@l\fs \more \ty \zeta}$.

 \medskip

 The following simple example defines a root record type $point$ with fields $x

 \ty nat$ and $y \ty nat$, and record type $cpoint$ by extending $point$ with

 an additional $colour$ component.

 \begin{ttbox}

   record point =

     x :: nat

     y :: nat

   record cpoint = point +

     colour :: string

 \end{ttbox}

 \subsection{Record operations}\label{sec:HOL:record-ops}

 Any record definition of the form presented above produces certain standard

 operations.  Selectors and updates are provided for any field, including the

 improper one ``$more$''.  There are also cumulative record constructor

 functions.

 To simplify the presentation below, we first assume that $(\vec\alpha@n) \, t$

 is a root record with fields $\vec c@l \ty \vec\sigma@l$.

 \medskip

 \textbf{Selectors} and \textbf{updates} are available for any field (including

 ``$more$'') as follows:

 \begin{matharray}{lll}

   c@i & \ty & \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \To \sigma@i \\

   c@i_update & \ty & \sigma@i \To \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \To

     \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta}

 \end{matharray}

 There is some special syntax for updates: $r \, \record{x \asn a}$ abbreviates

 term $x_update \, a \, r$.  Repeated updates are supported as well: $r \,

 \record{x \asn a} \, \record{y \asn b} \, \record{z \asn c}$ may be written as

 $r \, \record{x \asn a\fs y \asn b\fs z \asn c}$.  Note that because of

 postfix notation the order of fields shown here is reverse than in the actual

 term.  This might lead to confusion in conjunction with special proof tools

 such as ordered rewriting.

 Since repeated updates are just function applications, fields may be freely

 permuted in $\record{x \asn a\fs y \asn b\fs z \asn c}$, as far as the logic

 is concerned.  Thus commutativity of updates can be proven within the logic

 for any two fields, but not as a general theorem: fields are not first-class

 values.

 \medskip

 \textbf{Make} operations provide cumulative record constructor functions:

 \begin{matharray}{lll}

   make & \ty & \vec\sigma@l \To \record{\vec c@l \ty \vec \sigma@l} \\

   make_scheme & \ty & \vec\sigma@l \To

     \zeta \To \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \\

 \end{matharray}

 \noindent

 These functions are curried.  The corresponding definitions in terms of actual

 record terms are part of the standard simpset.  Thus $point\dtt make\,a\,b$

 rewrites to $\record{x = a\fs y = b}$.

 \medskip

 Any of above selector, update and make operations are declared within a local

 name space prefixed by the name $t$ of the record.  In case that different

 records share base names of fields, one has to qualify names explicitly (e.g.\ 

 $t\dtt c@i_update$).  This is recommended especially for operations like

 $make$ or $update_more$ that always have the same base name.  Just use $t\dtt

 make$ etc.\ to avoid confusion.

 \bigskip

 We reconsider the case of non-root records, which are derived of some parent

 record.  In general, the latter may depend on another parent as well,

 resulting in a list of \emph{ancestor records}.  Appending the lists of fields

 of all ancestors results in a certain field prefix.  The record package

 automatically takes care of this by lifting operations over this context of

 ancestor fields.  Assuming that $(\vec\alpha@n) \, t$ has ancestor fields

 $\vec d@k \ty \vec\rho@k$, selectors will get the following types:

 \begin{matharray}{lll}

   c@i & \ty & \record{\vec d@k \ty \vec\rho@k, \vec c@l \ty \vec \sigma@l, \more \ty \zeta}

     \To \sigma@i

 \end{matharray}

 \noindent

 Update and make operations are analogous.

 \subsection{Record proof tools}\label{sec:HOL:record-thms}

 The record package declares the following proof rules for any record type $t$.

 \begin{enumerate}

 \item Standard conversions (selectors or updates applied to record constructor

   terms, make function definitions) are part of the standard simpset (via

   \texttt{addsimps}).

 \item Selectors applied to updated records are automatically reduced by

   simplification procedure \ttindex{record_simproc}, which is part of the

   default simpset.

 \item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x'

   \conj y=y'$ are made part of the standard simpset and claset (via

   \texttt{addIffs}).

 \item The introduction rule for record equality analogous to $x~r = x~r' \Imp

   y~r = y~r' \Imp \dots \Imp r = r'$ is added to the simpset and to the claset

   (as an ``extra introduction'').

 \item A tactic for record field splitting (\ttindex{record_split_tac}) may be

   made part of the claset (via \texttt{addSWrapper}).  This tactic is based on

   rules analogous to $(\All x PROP~P~x) \equiv (\All{a~b} PROP~P(a, b))$ for

   any field.

 \end{enumerate}

 The first two kinds of rules are stored within the theory as $t\dtt simps$ and

 $t\dtt iffs$, respectively; record equality introduction is available as

 $t\dtt equality$.  In some situations it might be appropriate to expand the

 definitions of updates: $t\dtt update_defs$.  Note that these names are

 \emph{not} bound at the {\ML} level.

 \medskip

 Most of the time, plain Simplification should be sufficient to solve goals

 involving records.  Combinations of the Simplifier and Classical Reasoner

 (\texttt{Auto_tac} or \texttt{Force_tac}) are very useful, too.  The example

 theory \texttt{HOL/ex/Records} demonstrates typical proofs concerning records.

 \section{Datatype definitions}

 \label{sec:HOL:datatype}

 \index{*datatype|(}

 Inductive datatypes, similar to those of \ML, frequently appear in

 applications of Isabelle/HOL.  In principle, such types could be defined by

 hand via \texttt{typedef} (see {\S}\ref{sec:typedef}), but this would be far too

 tedious.  The \ttindex{datatype} definition package of Isabelle/HOL (cf.\ 

 \cite{Berghofer-Wenzel:1999:TPHOL}) automates such chores.  It generates an

 appropriate \texttt{typedef} based on a least fixed-point construction, and

 proves freeness theorems and induction rules, as well as theorems for

 recursion and case combinators.  The user just has to give a simple

 specification of new inductive types using a notation similar to {\ML} or

 Haskell.

 The current datatype package can handle both mutual and indirect recursion.

 It also offers to represent existing types as datatypes giving the advantage

 of a more uniform view on standard theories.

 \subsection{Basics}

 \label{subsec:datatype:basics}

 A general \texttt{datatype} definition is of the following form:

 \[

 \begin{array}{llcl}

 \mathtt{datatype} & (\vec{\alpha})t@1 & = &

   C^1@1~\tau^1@{1,1}~\ldots~\tau^1@{1,m^1@1} ~\mid~ \ldots ~\mid~

     C^1@{k@1}~\tau^1@{k@1,1}~\ldots~\tau^1@{k@1,m^1@{k@1}} \\

  & & \vdots \\

 \mathtt{and} & (\vec{\alpha})t@n & = &

   C^n@1~\tau^n@{1,1}~\ldots~\tau^n@{1,m^n@1} ~\mid~ \ldots ~\mid~

     C^n@{k@n}~\tau^n@{k@n,1}~\ldots~\tau^n@{k@n,m^n@{k@n}}

 \end{array}

 \]

 where $\vec{\alpha} = (\alpha@1,\ldots,\alpha@h)$ is a list of type variables,

 $C^j@i$ are distinct constructor names and $\tau^j@{i,i'}$ are {\em

   admissible} types containing at most the type variables $\alpha@1, \ldots,

 \alpha@h$. A type $\tau$ occurring in a \texttt{datatype} definition is {\em

   admissible} if and only if

 \begin{itemize}

 \item $\tau$ is non-recursive, i.e.\ $\tau$ does not contain any of the

 newly defined type constructors $t@1,\ldots,t@n$, or

 \item $\tau = (\vec{\alpha})t@{j'}$ where $1 \leq j' \leq n$, or

 \item $\tau = (\tau'@1,\ldots,\tau'@{h'})t'$, where $t'$ is

 the type constructor of an already existing datatype and $\tau'@1,\ldots,\tau'@{h'}$

 are admissible types.

 \item $\tau = \sigma \to \tau'$, where $\tau'$ is an admissible

 type and $\sigma$ is non-recursive (i.e. the occurrences of the newly defined

 types are {\em strictly positive})

 \end{itemize}

 If some $(\vec{\alpha})t@{j'}$ occurs in a type $\tau^j@{i,i'}$

 of the form

 \[

 (\ldots,\ldots ~ (\vec{\alpha})t@{j'} ~ \ldots,\ldots)t'

 \]

 this is called a {\em nested} (or \emph{indirect}) occurrence. A very simple

 example of a datatype is the type \texttt{list}, which can be defined by

 \begin{ttbox}

 datatype 'a list = Nil

                  | Cons 'a ('a list)

 \end{ttbox}

 Arithmetic expressions \texttt{aexp} and boolean expressions \texttt{bexp} can be modelled

 by the mutually recursive datatype definition

 \begin{ttbox}

 datatype 'a aexp = If_then_else ('a bexp) ('a aexp) ('a aexp)

                  | Sum ('a aexp) ('a aexp)

                  | Diff ('a aexp) ('a aexp)

                  | Var 'a

                  | Num nat

 and      'a bexp = Less ('a aexp) ('a aexp)

                  | And ('a bexp) ('a bexp)

                  | Or ('a bexp) ('a bexp)

 \end{ttbox}

 The datatype \texttt{term}, which is defined by

 \begin{ttbox}

 datatype ('a, 'b) term = Var 'a

                        | App 'b ((('a, 'b) term) list)

 \end{ttbox}

 is an example for a datatype with nested recursion. Using nested recursion

 involving function spaces, we may also define infinitely branching datatypes, e.g.

 \begin{ttbox}

 datatype 'a tree = Atom 'a | Branch "nat => 'a tree"

 \end{ttbox}

 \medskip

 Types in HOL must be non-empty. Each of the new datatypes

 $(\vec{\alpha})t@j$ with $1 \leq j \leq n$ is non-empty if and only if it has a

 constructor $C^j@i$ with the following property: for all argument types

 $\tau^j@{i,i'}$ of the form $(\vec{\alpha})t@{j'}$ the datatype

 $(\vec{\alpha})t@{j'}$ is non-empty.

 If there are no nested occurrences of the newly defined datatypes, obviously

 at least one of the newly defined datatypes $(\vec{\alpha})t@j$

 must have a constructor $C^j@i$ without recursive arguments, a \emph{base

   case}, to ensure that the new types are non-empty. If there are nested

 occurrences, a datatype can even be non-empty without having a base case

 itself. Since \texttt{list} is a non-empty datatype, \texttt{datatype t = C (t

   list)} is non-empty as well.

 \subsubsection{Freeness of the constructors}

 The datatype constructors are automatically defined as functions of their

 respective type:

 \[ C^j@i :: [\tau^j@{i,1},\dots,\tau^j@{i,m^j@i}] \To (\alpha@1,\dots,\alpha@h)t@j \]

 These functions have certain {\em freeness} properties.  They construct

 distinct values:

 \[

 C^j@i~x@1~\dots~x@{m^j@i} \neq C^j@{i'}~y@1~\dots~y@{m^j@{i'}} \qquad

 \mbox{for all}~ i \neq i'.

 \]

 The constructor functions are injective:

 \[

 (C^j@i~x@1~\dots~x@{m^j@i} = C^j@i~y@1~\dots~y@{m^j@i}) =

 (x@1 = y@1 \land \dots \land x@{m^j@i} = y@{m^j@i})

 \]

 Since the number of distinctness inequalities is quadratic in the number of

 constructors, the datatype package avoids proving them separately if there are

 too many constructors. Instead, specific inequalities are proved by a suitable

 simplification procedure on demand.\footnote{This procedure, which is already part

 of the default simpset, may be referred to by the ML identifier

 \texttt{DatatypePackage.distinct_simproc}.}

 \subsubsection{Structural induction}

 The datatype package also provides structural induction rules.  For

 datatypes without nested recursion, this is of the following form:

 \[

 \infer{P@1~x@1 \land \dots \land P@n~x@n}

   {\begin{array}{lcl}

      \Forall x@1 \dots x@{m^1@1}.

        \List{P@{s^1@{1,1}}~x@{r^1@{1,1}}; \dots;

          P@{s^1@{1,l^1@1}}~x@{r^1@{1,l^1@1}}} & \Imp &

            P@1~\left(C^1@1~x@1~\dots~x@{m^1@1}\right) \\

      & \vdots \\

      \Forall x@1 \dots x@{m^1@{k@1}}.

        \List{P@{s^1@{k@1,1}}~x@{r^1@{k@1,1}}; \dots;

          P@{s^1@{k@1,l^1@{k@1}}}~x@{r^1@{k@1,l^1@{k@1}}}} & \Imp &

            P@1~\left(C^1@{k@1}~x@1~\ldots~x@{m^1@{k@1}}\right) \\

      & \vdots \\

      \Forall x@1 \dots x@{m^n@1}.

        \List{P@{s^n@{1,1}}~x@{r^n@{1,1}}; \dots;

          P@{s^n@{1,l^n@1}}~x@{r^n@{1,l^n@1}}} & \Imp &

            P@n~\left(C^n@1~x@1~\ldots~x@{m^n@1}\right) \\

      & \vdots \\

      \Forall x@1 \dots x@{m^n@{k@n}}.

        \List{P@{s^n@{k@n,1}}~x@{r^n@{k@n,1}}; \dots

          P@{s^n@{k@n,l^n@{k@n}}}~x@{r^n@{k@n,l^n@{k@n}}}} & \Imp &

            P@n~\left(C^n@{k@n}~x@1~\ldots~x@{m^n@{k@n}}\right)

    \end{array}}

 \]

 where

 \[

 \begin{array}{rcl}

 Rec^j@i & := &

    \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots,

      \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\} = \\[2ex]

 && \left\{(i',i'')~\left|~

      1\leq i' \leq m^j@i \land 1 \leq i'' \leq n \land

        \tau^j@{i,i'} = (\alpha@1,\ldots,\alpha@h)t@{i''}\right.\right\}

 \end{array}

 \]

 i.e.\ the properties $P@j$ can be assumed for all recursive arguments.

 For datatypes with nested recursion, such as the \texttt{term} example from

 above, things are a bit more complicated.  Conceptually, Isabelle/HOL unfolds

 a definition like

 \begin{ttbox}

 datatype ('a,'b) term = Var 'a

                       | App 'b ((('a, 'b) term) list)

 \end{ttbox}

 to an equivalent definition without nesting:

 \begin{ttbox}

 datatype ('a,'b) term      = Var

                            | App 'b (('a, 'b) term_list)

 and      ('a,'b) term_list = Nil'

                            | Cons' (('a,'b) term) (('a,'b) term_list)

 \end{ttbox}

 Note however, that the type \texttt{('a,'b) term_list} and the constructors {\tt

   Nil'} and \texttt{Cons'} are not really introduced.  One can directly work with

 the original (isomorphic) type \texttt{(('a, 'b) term) list} and its existing

 constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for

 \texttt{term} gets the form

 \[

 \infer{P@1~x@1 \land P@2~x@2}

   {\begin{array}{l}

      \Forall x.~P@1~(\mathtt{Var}~x) \\

      \Forall x@1~x@2.~P@2~x@2 \Imp P@1~(\mathtt{App}~x@1~x@2) \\

      P@2~\mathtt{Nil} \\

      \Forall x@1~x@2. \List{P@1~x@1; P@2~x@2} \Imp P@2~(\mathtt{Cons}~x@1~x@2)

    \end{array}}

 \]

 Note that there are two predicates $P@1$ and $P@2$, one for the type \texttt{('a,'b) term}

 and one for the type \texttt{(('a, 'b) term) list}.

 For a datatype with function types such as \texttt{'a tree}, the induction rule

 is of the form

 \[

 \infer{P~t}

   {\Forall a.~P~(\mathtt{Atom}~a) &

    \Forall ts.~(\forall x.~P~(ts~x)) \Imp P~(\mathtt{Branch}~ts)}

 \]

 \medskip In principle, inductive types are already fully determined by

 freeness and structural induction.  For convenience in applications,

 the following derived constructions are automatically provided for any

 datatype.

 \subsubsection{The \sdx{case} construct}

 The type comes with an \ML-like \texttt{case}-construct:

 \[

 \begin{array}{rrcl}

 \mbox{\tt case}~e~\mbox{\tt of} & C^j@1~x@{1,1}~\dots~x@{1,m^j@1} & \To & e@1 \\

                            \vdots \\

                            \mid & C^j@{k@j}~x@{k@j,1}~\dots~x@{k@j,m^j@{k@j}} & \To & e@{k@j}

 \end{array}

 \]

 where the $x@{i,j}$ are either identifiers or nested tuple patterns as in

 {\S}\ref{subsec:prod-sum}.

 \begin{warn}

   All constructors must be present, their order is fixed, and nested patterns

   are not supported (with the exception of tuples).  Violating this

   restriction results in strange error messages.

 \end{warn}

 To perform case distinction on a goal containing a \texttt{case}-construct,

 the theorem $t@j.$\texttt{split} is provided:

 \[

 \begin{array}{@{}rcl@{}}

 P(t@j_\mathtt{case}~f@1~\dots~f@{k@j}~e) &\!\!\!=&

 \!\!\! ((\forall x@1 \dots x@{m^j@1}. e = C^j@1~x@1\dots x@{m^j@1} \to

                              P(f@1~x@1\dots x@{m^j@1})) \\

 &&\!\!\! ~\land~ \dots ~\land \\

 &&~\!\!\! (\forall x@1 \dots x@{m^j@{k@j}}. e = C^j@{k@j}~x@1\dots x@{m^j@{k@j}} \to

                              P(f@{k@j}~x@1\dots x@{m^j@{k@j}})))

 \end{array}

 \]

 where $t@j$\texttt{_case} is the internal name of the \texttt{case}-construct.

 This theorem can be added to a simpset via \ttindex{addsplits}

 (see~{\S}\ref{subsec:HOL:case:splitting}).

 Case splitting on assumption works as well, by using the rule

 $t@j.$\texttt{split_asm} in the same manner.  Both rules are available under

 $t@j.$\texttt{splits} (this name is \emph{not} bound in ML, though).

 \begin{warn}\index{simplification!of \texttt{case}}%

   By default only the selector expression ($e$ above) in a

   \texttt{case}-construct is simplified, in analogy with \texttt{if} (see

   page~\pageref{if-simp}). Only if that reduces to a constructor is one of

   the arms of the \texttt{case}-construct exposed and simplified. To ensure

   full simplification of all parts of a \texttt{case}-construct for datatype

   $t$, remove $t$\texttt{.}\ttindexbold{case_weak_cong} from the simpset, for

   example by \texttt{delcongs [thm "$t$.weak_case_cong"]}.

 \end{warn}

 \subsubsection{The function \cdx{size}}\label{sec:HOL:size}

 Theory \texttt{Arith} declares a generic function \texttt{size} of type

 $\alpha\To nat$.  Each datatype defines a particular instance of \texttt{size}

 by overloading according to the following scheme:

 %%% FIXME: This formula is too big and is completely unreadable

 \[

 size(C^j@i~x@1~\dots~x@{m^j@i}) = \!

 \left\{

 \begin{array}{ll}

 0 & \!\mbox{if $Rec^j@i = \emptyset$} \\

 1+\sum\limits@{h=1}^{l^j@i}size~x@{r^j@{i,h}} &

  \!\mbox{if $Rec^j@i = \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots,

   \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\}$}

 \end{array}

 \right.

 \]

 where $Rec^j@i$ is defined above.  Viewing datatypes as generalised trees, the

 size of a leaf is 0 and the size of a node is the sum of the sizes of its

 subtrees ${}+1$.

 \subsection{Defining datatypes}

 The theory syntax for datatype definitions is shown in

 Fig.~\ref{datatype-grammar}.  In order to be well-formed, a datatype

 definition has to obey the rules stated in the previous section.  As a result

 the theory is extended with the new types, the constructors, and the theorems

 listed in the previous section.

 \begin{figure}

 \begin{rail}

 datatype : 'datatype' typedecls;

 typedecls: ( newtype '=' (cons + '|') ) + 'and'

          ;

 newtype  : typevarlist id ( () | '(' infix ')' )

          ;

 cons     : name (argtype *) ( () | ( '(' mixfix ')' ) )

          ;

 argtype  : id | tid | ('(' typevarlist id ')')

          ;

 \end{rail}

 \caption{Syntax of datatype declarations}

 \label{datatype-grammar}

 \end{figure}

 Most of the theorems about datatypes become part of the default simpset and

 you never need to see them again because the simplifier applies them

 automatically.  Only induction or case distinction are usually invoked by hand.

 \begin{ttdescription}

 \item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$]

  applies structural induction on variable $x$ to subgoal $i$, provided the

  type of $x$ is a datatype.

 \item[\texttt{induct_tac}

   {\tt"}$x@1$ $\ldots$ $x@n${\tt"} $i$] applies simultaneous

   structural induction on the variables $x@1,\ldots,x@n$ to subgoal $i$.  This

   is the canonical way to prove properties of mutually recursive datatypes

   such as \texttt{aexp} and \texttt{bexp}, or datatypes with nested recursion such as

   \texttt{term}.

 \end{ttdescription}

 In some cases, induction is overkill and a case distinction over all

 constructors of the datatype suffices.

 \begin{ttdescription}

 \item[\ttindexbold{case_tac} {\tt"}$u${\tt"} $i$]

  performs a case analysis for the term $u$ whose type  must be a datatype.

  If the datatype has $k@j$ constructors  $C^j@1$, \dots $C^j@{k@j}$, subgoal

  $i$ is replaced by $k@j$ new subgoals which  contain the additional

  assumption $u = C^j@{i'}~x@1~\dots~x@{m^j@{i'}}$ for  $i'=1$, $\dots$,~$k@j$.

 \end{ttdescription}

 Note that induction is only allowed on free variables that should not occur

 among the premises of the subgoal. Case distinction applies to arbitrary terms.

 \bigskip

 For the technically minded, we exhibit some more details.  Processing the

 theory file produces an \ML\ structure which, in addition to the usual

 components, contains a structure named $t$ for each datatype $t$ defined in

 the file.  Each structure $t$ contains the following elements:

 \begin{ttbox}

 val distinct : thm list

 val inject : thm list

 val induct : thm

 val exhaust : thm

 val cases : thm list

 val split : thm

 val split_asm : thm

 val recs : thm list

 val size : thm list

 val simps : thm list

 \end{ttbox}

 \texttt{distinct}, \texttt{inject}, \texttt{induct}, \texttt{size}

 and \texttt{split} contain the theorems

 described above.  For user convenience, \texttt{distinct} contains

 inequalities in both directions.  The reduction rules of the {\tt

   case}-construct are in \texttt{cases}.  All theorems from {\tt

   distinct}, \texttt{inject} and \texttt{cases} are combined in \texttt{simps}.

 In case of mutually recursive datatypes, \texttt{recs}, \texttt{size}, \texttt{induct}

 and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$.

 \subsection{Representing existing types as datatypes}\label{subsec:datatype:rep_datatype}

 For foundational reasons, some basic types such as \texttt{nat}, \texttt{*}, {\tt

   +}, \texttt{bool} and \texttt{unit} are not defined in a \texttt{datatype} section,

 but by more primitive means using \texttt{typedef}. To be able to use the

 tactics \texttt{induct_tac} and \texttt{case_tac} and to define functions by

 primitive recursion on these types, such types may be represented as actual

 datatypes.  This is done by specifying an induction rule, as well as theorems

 stating the distinctness and injectivity of constructors in a {\tt

   rep_datatype} section.  For type \texttt{nat} this works as follows:

 \begin{ttbox}

 rep_datatype nat

   distinct Suc_not_Zero, Zero_not_Suc

   inject   Suc_Suc_eq

   induct   nat_induct

 \end{ttbox}

 The datatype package automatically derives additional theorems for recursion

 and case combinators from these rules.  Any of the basic HOL types mentioned

 above are represented as datatypes.  Try an induction on \texttt{bool}

 today.

 \subsection{Examples}

 \subsubsection{The datatype $\alpha~mylist$}

 We want to define a type $\alpha~mylist$. To do this we have to build a new

 theory that contains the type definition.  We start from the theory

 \texttt{Datatype} instead of \texttt{Main} in order to avoid clashes with the

 \texttt{List} theory of Isabelle/HOL.

 \begin{ttbox}

 MyList = Datatype +

   datatype 'a mylist = Nil | Cons 'a ('a mylist)

 end

 \end{ttbox}

 After loading the theory, we can prove $Cons~x~xs\neq xs$, for example.  To

 ease the induction applied below, we state the goal with $x$ quantified at the

 object-level.  This will be stripped later using \ttindex{qed_spec_mp}.

 \begin{ttbox}

 Goal "!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 (induct_tac "xs" 1);

 {\out Level 1}

 {\out ! x. Cons x xs ~= xs}

 {\out  1. ! x. Cons x Nil ~= Nil}

 {\out  2. !!a mylist.}

 {\out        ! x. Cons x mylist ~= mylist ==>}

 {\out        ! x. Cons x (Cons a mylist) ~= Cons a mylist}

 \end{ttbox}

 The first subgoal can be proved using the simplifier.  Isabelle/HOL has

 already added the freeness properties of lists to the default simplification

 set.

 \begin{ttbox}

 by (Simp_tac 1);

 {\out Level 2}

 {\out ! x. Cons x xs ~= xs}

 {\out  1. !!a mylist.}

 {\out        ! x. Cons x mylist ~= mylist ==>}

 {\out        ! x. Cons x (Cons a mylist) ~= Cons a mylist}

 \end{ttbox}

 Similarly, we prove the remaining goal.

 \begin{ttbox}

 by (Asm_simp_tac 1);

 {\out Level 3}

 {\out ! x. Cons x xs ~= xs}

 {\out No subgoals!}

 \ttbreak

 qed_spec_mp "not_Cons_self";

 {\out val not_Cons_self = "Cons x xs ~= xs" : thm}

 \end{ttbox}

 Because both subgoals could have been proved by \texttt{Asm_simp_tac}

 we could have done that in one step:

 \begin{ttbox}

 by (ALLGOALS Asm_simp_tac);

 \end{ttbox}

 \subsubsection{The datatype $\alpha~mylist$ with mixfix syntax}

 In this example we define the type $\alpha~mylist$ again but this time

 we want to write \texttt{[]} for \texttt{Nil} and we want to use infix

 notation \verb|#| for \texttt{Cons}.  To do this we simply add mixfix

 annotations after the constructor declarations as follows:

 \begin{ttbox}

 MyList = Datatype +

   datatype 'a mylist =

     Nil ("[]")  |

     Cons 'a ('a mylist)  (infixr "#" 70)

 end

 \end{ttbox}

 Now the theorem in the previous example can be written \verb|x#xs ~= xs|.

 \subsubsection{A datatype for weekdays}

 This example shows a datatype that consists of 7 constructors:

 \begin{ttbox}

 Days = Main +

   datatype days = Mon | Tue | Wed | Thu | Fri | Sat | Sun

 end

 \end{ttbox}

 Because there are more than 6 constructors, inequality is expressed via a function

 \verb|days_ord|.  The theorem \verb|Mon ~= Tue| is not directly

 contained among the distinctness theorems, but the simplifier can

 prove it thanks to rewrite rules inherited from theory \texttt{Arith}:

 \begin{ttbox}

 Goal "Mon ~= Tue";

 by (Simp_tac 1);

 \end{ttbox}

 You need not derive such inequalities explicitly: the simplifier will dispose

 of them automatically.

 \index{*datatype|)}

 \section{Recursive function definitions}\label{sec:HOL:recursive}

 \index{recursive functions|see{recursion}}

 Isabelle/HOL provides two main mechanisms of defining recursive functions.

 \begin{enumerate}

 \item \textbf{Primitive recursion} is available only for datatypes, and it is

   somewhat restrictive.  Recursive calls are only allowed on the argument's

   immediate constituents.  On the other hand, it is the form of recursion most

   often wanted, and it is easy to use.

 \item \textbf{Well-founded recursion} requires that you supply a well-founded

   relation that governs the recursion.  Recursive calls are only allowed if

   they make the argument decrease under the relation.  Complicated recursion

   forms, such as nested recursion, can be dealt with.  Termination can even be

   proved at a later time, though having unsolved termination conditions around

   can make work difficult.%

   \footnote{This facility is based on Konrad Slind's TFL

     package~\cite{slind-tfl}.  Thanks are due to Konrad for implementing TFL

     and assisting with its installation.}

 \end{enumerate}

 Following good HOL tradition, these declarations do not assert arbitrary

 axioms.  Instead, they define the function using a recursion operator.  Both

 HOL and ZF derive the theory of well-founded recursion from first

 principles~\cite{paulson-set-II}.  Primitive recursion over some datatype

 relies on the recursion operator provided by the datatype package.  With

 either form of function definition, Isabelle proves the desired recursion

 equations as theorems.

 \subsection{Primitive recursive functions}

 \label{sec:HOL:primrec}

 \index{recursion!primitive|(}

 \index{*primrec|(}

 Datatypes come with a uniform way of defining functions, {\bf primitive

   recursion}.  In principle, one could introduce primitive recursive functions

 by asserting their reduction rules as new axioms, but this is not recommended:

 \begin{ttbox}\slshape

 Append = Main +

 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}

 Asserting axioms brings the danger of accidentally asserting nonsense, as

 in \verb$app [] ys = us$.

 The \ttindex{primrec} declaration is a safe means of defining primitive

 recursive functions on datatypes:

 \begin{ttbox}

 Append = Main +

 consts app :: ['a list, 'a list] => 'a list

 primrec

    "app [] ys = ys"

    "app (x#xs) ys = x#app xs ys"

 end

 \end{ttbox}

 Isabelle will now check that the two rules do indeed form a primitive

 recursive definition.  For example

 \begin{ttbox}

 primrec

     "app [] ys = us"

 \end{ttbox}

 is rejected with an error message ``\texttt{Extra variables on rhs}''.

 \bigskip

 The general form of a primitive recursive definition is

 \begin{ttbox}

 primrec

     {\it reduction rules}

 \end{ttbox}

 where \textit{reduction rules} specify one or more equations 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 at most one reduction rule for each constructor.  The order is

 immaterial.  For missing constructors, the function is defined to return a

 default value.  

 If you would like to refer to some rule by name, then you must prefix

 the rule with an identifier.  These identifiers, like those in the

 \texttt{rules} section of a theory, will be visible at the \ML\ level.

 The primitive recursive function can have infix or mixfix syntax:

 \begin{ttbox}\underscoreon

 consts "@"  :: ['a list, 'a list] => 'a list  (infixr 60)

 primrec

    "[] @ ys = ys"

    "(x#xs) @ ys = x#(xs @ ys)"

 \end{ttbox}

 The reduction rules become part of the default simpset, which

 leads to short proof scripts:

 \begin{ttbox}\underscoreon

 Goal "(xs @ ys) @ zs = xs @ (ys @ zs)";

 by (induct\_tac "xs" 1);

 by (ALLGOALS Asm\_simp\_tac);

 \end{ttbox}

 \subsubsection{Example: Evaluation of expressions}

 Using mutual primitive recursion, we can define evaluation functions \texttt{evala}

 and \texttt{eval_bexp} for the datatypes of arithmetic and boolean expressions mentioned in

 {\S}\ref{subsec:datatype:basics}:

 \begin{ttbox}

 consts

   evala :: "['a => nat, 'a aexp] => nat"

   evalb :: "['a => nat, 'a bexp] => bool"

 primrec

   "evala env (If_then_else b a1 a2) =

      (if evalb env b then evala env a1 else evala env a2)"

   "evala env (Sum a1 a2) = evala env a1 + evala env a2"

   "evala env (Diff a1 a2) = evala env a1 - evala env a2"

   "evala env (Var v) = env v"

   "evala env (Num n) = n"

   "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"

   "evalb env (And b1 b2) = (evalb env b1 & evalb env b2)"

   "evalb env (Or b1 b2) = (evalb env b1 & evalb env b2)"

 \end{ttbox}

 Since the value of an expression depends on the value of its variables,

 the functions \texttt{evala} and \texttt{evalb} take an additional

 parameter, an {\em environment} of type \texttt{'a => nat}, which maps

 variables to their values.

 Similarly, we may define substitution functions \texttt{substa}

 and \texttt{substb} for expressions: The mapping \texttt{f} of type

 \texttt{'a => 'a aexp} given as a parameter is lifted canonically

 on the types \texttt{'a aexp} and \texttt{'a bexp}:

 \begin{ttbox}

 consts

   substa :: "['a => 'b aexp, 'a aexp] => 'b aexp"

   substb :: "['a => 'b aexp, 'a bexp] => 'b bexp"

 primrec

   "substa f (If_then_else b a1 a2) =

      If_then_else (substb f b) (substa f a1) (substa f a2)"

   "substa f (Sum a1 a2) = Sum (substa f a1) (substa f a2)"

   "substa f (Diff a1 a2) = Diff (substa f a1) (substa f a2)"

   "substa f (Var v) = f v"

   "substa f (Num n) = Num n"

   "substb f (Less a1 a2) = Less (substa f a1) (substa f a2)"

   "substb f (And b1 b2) = And (substb f b1) (substb f b2)"

   "substb f (Or b1 b2) = Or (substb f b1) (substb f b2)"

 \end{ttbox}

 In textbooks about semantics one often finds {\em substitution theorems},

 which express the relationship between substitution and evaluation. For

 \texttt{'a aexp} and \texttt{'a bexp}, we can prove such a theorem by mutual

 induction, followed by simplification:

 \begin{ttbox}

 Goal

   "evala env (substa (Var(v := a')) a) =

      evala (env(v := evala env a')) a &

    evalb env (substb (Var(v := a')) b) =

      evalb (env(v := evala env a')) b";

 by (induct_tac "a b" 1);

 by (ALLGOALS Asm_full_simp_tac);

 \end{ttbox}

 \subsubsection{Example: A substitution function for terms}

 Functions on datatypes with nested recursion, such as the type

 \texttt{term} mentioned in {\S}\ref{subsec:datatype:basics}, are

 also defined by mutual primitive recursion. A substitution

 function \texttt{subst_term} on type \texttt{term}, similar to the functions

 \texttt{substa} and \texttt{substb} described above, can

 be defined as follows:

 \begin{ttbox}

 consts

   subst_term :: "['a => ('a,'b) term, ('a,'b) term] => ('a,'b) term"

   subst_term_list ::

     "['a => ('a,'b) term, ('a,'b) term list] => ('a,'b) term list"

 primrec

   "subst_term f (Var a) = f a"

   "subst_term f (App b ts) = App b (subst_term_list f ts)"

   "subst_term_list f [] = []"

   "subst_term_list f (t # ts) =

      subst_term f t # subst_term_list f ts"

 \end{ttbox}

 The recursion scheme follows the structure of the unfolded definition of type

 \texttt{term} shown in {\S}\ref{subsec:datatype:basics}. To prove properties of

 this substitution function, mutual induction is needed:

 \begin{ttbox}

 Goal

   "(subst_term ((subst_term f1) o f2) t) =

      (subst_term f1 (subst_term f2 t)) &

    (subst_term_list ((subst_term f1) o f2) ts) =

      (subst_term_list f1 (subst_term_list f2 ts))";

 by (induct_tac "t ts" 1);

 by (ALLGOALS Asm_full_simp_tac);

 \end{ttbox}

 \subsubsection{Example: A map function for infinitely branching trees}

 Defining functions on infinitely branching datatypes by primitive

 recursion is just as easy. For example, we can define a function

 \texttt{map_tree} on \texttt{'a tree} as follows:

 \begin{ttbox}

 consts

   map_tree :: "('a => 'b) => 'a tree => 'b tree"

 primrec

   "map_tree f (Atom a) = Atom (f a)"

   "map_tree f (Branch ts) = Branch (\%x. map_tree f (ts x))"

 \end{ttbox}

 Note that all occurrences of functions such as \texttt{ts} in the

 \texttt{primrec} clauses must be applied to an argument. In particular,

 \texttt{map_tree f o ts} is not allowed.

 \index{recursion!primitive|)}

 \index{*primrec|)}

 \subsection{General recursive functions}

 \label{sec:HOL:recdef}