%% $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);