104

1 
%% $Id$


2 
\chapter{Higherorder logic}


3 
The directory~\ttindexbold{HOL} contains a theory for higherorder logic

111

4 
based on Gordon's~{\sc hol} system~\cite{mgordon88a}, which itself is based on

104

5 
Church~\cite{church40}. Andrews~\cite{andrews86} is a full description of


6 
higherorder logic. Gordon's work has demonstrated that higherorder logic


7 
is useful for hardware verification; beyond this, it is widely applicable


8 
in many areas of mathematics. It is weaker than {\ZF} set theory but for


9 
most applications this does not matter. If you prefer {\ML} to Lisp, you


10 
will probably prefer {\HOL} to~{\ZF}.


11 


12 
Previous releases of Isabelle included a completely different version


13 
of~{\HOL}, with explicit type inference rules~\cite{paulsonCOLOG}. This


14 
version no longer exists, but \ttindex{ZF} supports a similar style of


15 
reasoning.


16 


17 
{\HOL} has a distinct feel, compared with {\ZF} and {\CTT}. It


18 
identifies objectlevel types with metalevel types, taking advantage of


19 
Isabelle's builtin type checker. It identifies objectlevel functions


20 
with metalevel functions, so it uses Isabelle's operations for abstraction


21 
and application. There is no ``apply'' operator: function applications are


22 
written as simply~$f(a)$ rather than $f{\tt`}a$.


23 


24 
These identifications allow Isabelle to support {\HOL} particularly nicely,


25 
but they also mean that {\HOL} requires more sophistication from the user


26 
 in particular, an understanding of Isabelle's type system. Beginners


27 
should gain experience by working in firstorder logic, before attempting


28 
to use higherorder logic. This chapter assumes familiarity with~{\FOL{}}.


29 


30 


31 
\begin{figure}


32 
\begin{center}


33 
\begin{tabular}{rrr}

111

34 
\it name &\it metatype & \it description \\


35 
\idx{Trueprop}& $bool\To prop$ & coercion to $prop$\\


36 
\idx{not} & $bool\To bool$ & negation ($\neg$) \\


37 
\idx{True} & $bool$ & tautology ($\top$) \\


38 
\idx{False} & $bool$ & absurdity ($\bot$) \\


39 
\idx{if} & $[bool,\alpha,\alpha]\To\alpha::term$ & conditional \\


40 
\idx{Inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & function inversion

104

41 
\end{tabular}


42 
\end{center}


43 
\subcaption{Constants}


44 


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


46 
\begin{center}


47 
\begin{tabular}{llrrr}

111

48 
\it symbol &\it name &\it metatype & \it prec & \it description \\

104

49 
\tt\at & \idx{Eps} & $(\alpha\To bool)\To\alpha::term$ & 10 &

111

50 
Hilbert description ($\epsilon$) \\

104

51 
\idx{!} & \idx{All} & $(\alpha::term\To bool)\To bool$ & 10 &

111

52 
universal quantifier ($\forall$) \\

104

53 
\idx{?} & \idx{Ex} & $(\alpha::term\To bool)\To bool$ & 10 &

111

54 
existential quantifier ($\exists$) \\

104

55 
\idx{?!} & \idx{Ex1} & $(\alpha::term\To bool)\To bool$ & 10 &

111

56 
unique existence ($\exists!$)

104

57 
\end{tabular}


58 
\end{center}


59 
\subcaption{Binders}


60 


61 
\begin{center}


62 
\begin{tabular}{llrrr}

111

63 
\it symbol &\it name &\it metatype & \it prec & \it description \\

104

64 
\idx{ALL} & \idx{All} & $(\alpha::term\To bool)\To bool$ & 10 &

111

65 
universal quantifier ($\forall$) \\

104

66 
\idx{EX} & \idx{Ex} & $(\alpha::term\To bool)\To bool$ & 10 &

111

67 
existential quantifier ($\exists$) \\

104

68 
\idx{EX!} & \idx{Ex1} & $(\alpha::term\To bool)\To bool$ & 10 &

111

69 
unique existence ($\exists!$)

104

70 
\end{tabular}


71 
\end{center}


72 
\subcaption{Alternative quantifiers}


73 


74 
\begin{center}


75 
\indexbold{*"=}


76 
\indexbold{&@{\tt\&}}


77 
\indexbold{*"}


78 
\indexbold{*""">}


79 
\begin{tabular}{rrrr}

111

80 
\it symbol & \it metatype & \it precedence & \it description \\


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


82 
Right 50 & composition ($\circ$) \\


83 
\tt = & $[\alpha::term,\alpha]\To bool$ & Left 50 & equality ($=$) \\


84 
\tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\


85 
\tt  & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\


86 
\tt > & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$) \\


87 
\tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\


88 
\tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 &


89 
less than or equals ($\leq$)

104

90 
\end{tabular}


91 
\end{center}


92 
\subcaption{Infixes}


93 
\caption{Syntax of {\tt HOL}} \label{holconstants}


94 
\end{figure}


95 


96 


97 
\begin{figure}


98 
\dquotes


99 
\[\begin{array}{rcl}


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

111

101 
&  & "\at~~" id~id^* " . " formula \\[2ex]

104

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

111

103 
&  & term " = " term \\


104 
&  & term " \ttilde= " term \\


105 
&  & term " < " term \\


106 
&  & term " <= " term \\


107 
&  & "\ttilde\ " formula \\


108 
&  & formula " \& " formula \\


109 
&  & formula "  " formula \\


110 
&  & formula " > " formula \\


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


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


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


114 
&  & "ALL~" id~id^* " . " formula \\


115 
&  & "EX~~" id~id^* " . " formula \\


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

104

117 
\end{array}


118 
\]


119 
\subcaption{Grammar}


120 
\caption{Full grammar for {\HOL}} \label{holgrammar}


121 
\end{figure}


122 


123 


124 
\section{Syntax}


125 
Type inference is automatic, exploiting Isabelle's type classes. The class


126 
of higherorder terms is called {\it term\/}; type variables range over


127 
this class by default. The equality symbol and quantifiers are polymorphic


128 
over class {\it term}.


129 


130 
Class {\it ord\/} consists of all ordered types; the relations $<$ and


131 
$\leq$ are polymorphic over this class, as are the functions


132 
\ttindex{mono}, \ttindex{min} and \ttindex{max}. Three other


133 
type classes  {\it plus}, {\it minus\/} and {\it times}  permit


134 
overloading of the operators {\tt+}, {\tt} and {\tt*}. In particular,


135 
{\tt} is overloaded for set difference and subtraction.


136 
\index{*"+}\index{@{\tt}}\index{*@{\tt*}}


137 


138 
Figure~\ref{holconstants} lists the constants (including infixes and


139 
binders), while Figure~\ref{holgrammar} presents the grammar. Note that


140 
$a$\verb~=$b$ is translated to \verb~($a$=$b$\verb).


141 


142 
\subsection{Types}


143 
The type of formulae, {\it bool} belongs to class {\it term}; thus,


144 
formulae are terms. The builtin type~$fun$, which constructs function


145 
types, is overloaded such that $\sigma\To\tau$ belongs to class~$term$ if


146 
$\sigma$ and~$\tau$ do; this allows quantification over functions. Types


147 
in {\HOL} must be nonempty because of the form of quantifier


148 
rules~\cite[\S7]{paulsonCOLOG}.


149 


150 
Gordon's {\sc hol} system supports {\bf type definitions}. A type is


151 
defined by exhibiting an existing type~$\sigma$, a predicate~$P::\sigma\To


152 
bool$, and a theorem of the form $\exists x::\sigma.P(x)$. Thus~$P$


153 
specifies a nonempty subset of~$\sigma$, and the new type denotes this


154 
subset. New function constants are generated to establish an isomorphism


155 
between the new type and the subset. If type~$\sigma$ involves type


156 
variables $\alpha@1$, \ldots, $\alpha@n$, then the type definition creates


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


158 
type.


159 


160 
Isabelle does not support type definitions at present. Instead, they are


161 
mimicked by explicit definitions of isomorphism functions. These should be


162 
accompanied by theorems of the form $\exists x::\sigma.P(x)$, but this is


163 
not checked.


164 


165 


166 
\subsection{Binders}


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


168 
satisfying~$P[a]$, if such exists. Since all terms in {\HOL} denote


169 
something, a description is always meaningful, but we do not know its value


170 
unless $P[x]$ defines it uniquely. We may write descriptions as


171 
\ttindexbold{Eps}($P$) or use the syntax


172 
\hbox{\tt \at $x$.$P[x]$}. Existential quantification is defined


173 
by


174 
\[ \exists x.P(x) \equiv P(\epsilon x.P(x)) \]


175 
The unique existence quantifier, $\exists!x.P[x]$, is defined in terms


176 
of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested


177 
quantifications. For instance, $\exists!x y.P(x,y)$ abbreviates


178 
$\exists!x. \exists!y.P(x,y)$; note that this does not mean that there


179 
exists a unique pair $(x,y)$ satisfying~$P(x,y)$.


180 


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


182 
Quantifiers have two notations. As in Gordon's {\sc hol} system, {\HOL}


183 
uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$. The


184 
existential quantifier must be followed by a space; thus {\tt?x} is an


185 
unknown, while \verb'? x.f(x)=y' is a quantification. Isabelle's usual


186 
notation for quantifiers, \ttindex{ALL} and \ttindex{EX}, is also


187 
available. Both notations are accepted for input. The {\ML} reference


188 
\ttindexbold{HOL_quantifiers} governs the output notation. If set to {\tt


189 
true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set


190 
to {\tt false}, then~{\tt ALL} and~{\tt EX} are displayed.


191 


192 
\begin{warn}


193 
Although the description operator does not usually allow iteration of the


194 
form \hbox{\tt \at $x@1 \dots x@n$.$P[x@1,\dots,x@n]$}, there are cases where


195 
this is legal. If \hbox{\tt \at $y$.$P[x,y]$} is of type~{\it bool},


196 
then \hbox{\tt \at $x\,y$.$P[x,y]$} is legal. The pretty printer will


197 
display \hbox{\tt \at $x$.\at $y$.$P[x,y]$} as


198 
\hbox{\tt \at $x\,y$.$P[x,y]$}.


199 
\end{warn}


200 


201 
\begin{figure} \makeatother


202 
\begin{ttbox}


203 
\idx{refl} t = t::'a


204 
\idx{subst} [ s=t; P(s) ] ==> P(t::'a)


205 
\idx{ext} (!!x::'a. f(x)::'b = g(x)) ==> (%x.f(x)) = (%x.g(x))


206 
\idx{impI} (P ==> Q) ==> P>Q


207 
\idx{mp} [ P>Q; P ] ==> Q


208 
\idx{iff} (P>Q) > (Q>P) > (P=Q)


209 
\idx{selectI} P(x::'a) ==> P(@x.P(x))


210 
\idx{True_or_False} (P=True)  (P=False)


211 
\subcaption{basic rules}


212 


213 
\idx{True_def} True = ((%x.x)=(%x.x))


214 
\idx{All_def} All = (%P. P = (%x.True))


215 
\idx{Ex_def} Ex = (%P. P(@x.P(x)))


216 
\idx{False_def} False = (!P.P)


217 
\idx{not_def} not = (%P. P>False)


218 
\idx{and_def} op & = (%P Q. !R. (P>Q>R) > R)


219 
\idx{or_def} op  = (%P Q. !R. (P>R) > (Q>R) > R)


220 
\idx{Ex1_def} Ex1 = (%P. ? x. P(x) & (! y. P(y) > y=x))


221 
\subcaption{Definitions of the logical constants}


222 


223 
\idx{Inv_def} Inv = (%(f::'a=>'b) y. @x. f(x)=y)


224 
\idx{o_def} op o = (%(f::'b=>'c) g (x::'a). f(g(x)))


225 
\idx{if_def} if = (%P x y.@z::'a.(P=True > z=x) & (P=False > z=y))


226 
\subcaption{Further definitions}


227 
\end{ttbox}


228 
\caption{Rules of {\tt HOL}} \label{holrules}


229 
\end{figure}


230 


231 


232 
\begin{figure} \makeatother


233 
\begin{ttbox}


234 
\idx{sym} s=t ==> t=s


235 
\idx{trans} [ r=s; s=t ] ==> r=t


236 
\idx{ssubst} [ t=s; P(s) ] ==> P(t::'a)


237 
\idx{box_equals} [ a=b; a=c; b=d ] ==> c=d


238 
\idx{arg_cong} s=t ==> f(s)=f(t)


239 
\idx{fun_cong} s::'a=>'b = t ==> s(x)=t(x)


240 
\subcaption{Equality}


241 


242 
\idx{TrueI} True


243 
\idx{FalseE} False ==> P


244 


245 
\idx{conjI} [ P; Q ] ==> P&Q


246 
\idx{conjunct1} [ P&Q ] ==> P


247 
\idx{conjunct2} [ P&Q ] ==> Q


248 
\idx{conjE} [ P&Q; [ P; Q ] ==> R ] ==> R


249 


250 
\idx{disjI1} P ==> PQ


251 
\idx{disjI2} Q ==> PQ


252 
\idx{disjE} [ P  Q; P ==> R; Q ==> R ] ==> R


253 


254 
\idx{notI} (P ==> False) ==> ~ P


255 
\idx{notE} [ ~ P; P ] ==> R


256 
\idx{impE} [ P>Q; P; Q ==> R ] ==> R


257 
\subcaption{Propositional logic}


258 


259 
\idx{iffI} [ P ==> Q; Q ==> P ] ==> P=Q


260 
\idx{iffD1} [ P=Q; P ] ==> Q


261 
\idx{iffD2} [ P=Q; Q ] ==> P


262 
\idx{iffE} [ P=Q; [ P > Q; Q > P ] ==> R ] ==> R


263 


264 
\idx{eqTrueI} P ==> P=True


265 
\idx{eqTrueE} P=True ==> P


266 
\subcaption{Logical equivalence}


267 


268 
\end{ttbox}


269 
\caption{Derived rules for {\HOL}} \label{hollemmas1}


270 
\end{figure}


271 


272 


273 
\begin{figure} \makeatother


274 
\begin{ttbox}


275 
\idx{allI} (!!x::'a. P(x)) ==> !x. P(x)


276 
\idx{spec} !x::'a.P(x) ==> P(x)


277 
\idx{allE} [ !x.P(x); P(x) ==> R ] ==> R


278 
\idx{all_dupE} [ !x.P(x); [ P(x); !x.P(x) ] ==> R ] ==> R


279 


280 
\idx{exI} P(x) ==> ? x::'a.P(x)


281 
\idx{exE} [ ? x::'a.P(x); !!x. P(x) ==> Q ] ==> Q


282 


283 
\idx{ex1I} [ P(a); !!x. P(x) ==> x=a ] ==> ?! x. P(x)


284 
\idx{ex1E} [ ?! x.P(x); !!x. [ P(x); ! y. P(y) > y=x ] ==> R


285 
] ==> R


286 


287 
\idx{select_equality} [ P(a); !!x. P(x) ==> x=a ] ==> (@x.P(x)) = a


288 
\subcaption{Quantifiers and descriptions}


289 


290 
\idx{ccontr} (~P ==> False) ==> P


291 
\idx{classical} (~P ==> P) ==> P


292 
\idx{excluded_middle} ~P  P


293 


294 
\idx{disjCI} (~Q ==> P) ==> PQ


295 
\idx{exCI} (! x. ~ P(x) ==> P(a)) ==> ? x.P(x)


296 
\idx{impCE} [ P>Q; ~ P ==> R; Q ==> R ] ==> R


297 
\idx{iffCE} [ P<>Q; [ P; Q ] ==> R; [ ~P; ~Q ] ==> R ] ==> R


298 
\idx{notnotD} ~~P ==> P


299 
\idx{swap} ~P ==> (~Q ==> P) ==> Q


300 
\subcaption{Classical logic}


301 


302 
\idx{if_True} if(True,x,y) = x


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


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


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


306 
\idx{expand_if} P(if(Q,x,y)) = ((Q > P(x)) & (~Q > P(y)))


307 
\subcaption{Conditionals}


308 
\end{ttbox}


309 
\caption{More derived rules} \label{hollemmas2}


310 
\end{figure}


311 


312 


313 
\section{Rules of inference}


314 
The basic theory has the {\ML} identifier \ttindexbold{HOL.thy}. However,


315 
many further theories are defined, introducing product and sum types, the


316 
natural numbers, etc.


317 


318 
Figure~\ref{holrules} shows the inference rules with their~{\ML} names.


319 
They follow standard practice in higherorder logic: only a few connectives


320 
are taken as primitive, with the remainder defined obscurely.


321 


322 
Unusually, the definitions use objectequality~({\tt=}) rather than


323 
metaequality~({\tt==}). This is possible because equality in higherorder


324 
logic may equate formulae and even functions over formulae. On the other


325 
hand, metaequality is Isabelle's usual symbol for making definitions.


326 
Take care to note which form of equality is used before attempting a proof.


327 


328 
Some of the rules mention type variables; for example, {\tt refl} mentions


329 
the type variable~{\tt'a}. This facilitates explicit instantiation of the


330 
type variables. By default, such variables range over class {\it term}.


331 


332 
\begin{warn}


333 
Where function types are involved, Isabelle's unification code does not


334 
guarantee to find instantiations for type variables automatically. If


335 
resolution fails for no obvious reason, try setting \ttindex{show_types} to


336 
{\tt true}, causing Isabelle to display types of terms. (Possibly, set


337 
\ttindex{show_sorts} to {\tt true} also, causing Isabelle to display sorts.)


338 
Be prepared to use \ttindex{res_inst_tac} instead of {\tt resolve_tac}.


339 
Setting \ttindex{Unify.trace_types} to {\tt true} causes Isabelle to


340 
report omitted search paths during unification.


341 
\end{warn}


342 


343 
Here are further comments on the rules:


344 
\begin{description}


345 
\item[\ttindexbold{ext}]


346 
expresses extensionality of functions.


347 
\item[\ttindexbold{iff}]


348 
asserts that logically equivalent formulae are equal.


349 
\item[\ttindexbold{selectI}]


350 
gives the defining property of the Hilbert $\epsilon$operator. The


351 
derived rule \ttindexbold{select_equality} (see below) is often easier to use.


352 
\item[\ttindexbold{True_or_False}]


353 
makes the logic classical.\footnote{In fact, the $\epsilon$operator


354 
already makes the logic classical, as shown by Diaconescu;


355 
see Paulson~\cite{paulsonCOLOG} for details.}


356 
\end{description}


357 


358 
\begin{warn}


359 
{\HOL} has no ifandonlyif connective; logical equivalence is expressed


360 
using equality. But equality has a high precedence, as befitting a


361 
relation, while ifandonlyif typically has the lowest precedence. Thus,


362 
$\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$. When


363 
using $=$ to mean logical equivalence, enclose both operands in


364 
parentheses.


365 
\end{warn}


366 


367 
Some derived rules are shown in Figures~\ref{hollemmas1}


368 
and~\ref{hollemmas2}, with their {\ML} names. These include natural rules


369 
for the logical connectives, as well as sequentstyle elimination rules for


370 
conjunctions, implications, and universal quantifiers.


371 


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


373 
backward proofs, while \ttindexbold{box_equals} supports reasoning by


374 
simplifying both sides of an equation.


375 


376 
See the files \ttindexbold{HOL/hol.thy} and


377 
\ttindexbold{HOL/hol.ML} for complete listings of the rules and


378 
derived rules.


379 


380 


381 
\section{Generic packages}


382 
{\HOL} instantiates most of Isabelle's generic packages;


383 
see \ttindexbold{HOL/ROOT.ML} for details.


384 
\begin{itemize}


385 
\item


386 
Because it includes a general substitution rule, {\HOL} instantiates the


387 
tactic \ttindex{hyp_subst_tac}, which substitutes for an equality


388 
throughout a subgoal and its hypotheses.


389 
\item


390 
It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the


391 
simplification set for higherorder logic. Equality~($=$), which also


392 
expresses logical equivalence, may be used for rewriting. See the file


393 
\ttindexbold{HOL/simpdata.ML} for a complete listing of the simplification


394 
rules.


395 
\item


396 
It instantiates the classical reasoning module. See~\S\ref{holclaprover}


397 
for details.


398 
\end{itemize}


399 


400 


401 
\begin{figure}


402 
\begin{center}


403 
\begin{tabular}{rrr}

111

404 
\it name &\it metatype & \it description \\

104

405 
\index{"{"}@{\tt\{\}}}

111

406 
{\tt\{\}} & $\alpha\,set$ & the empty set \\


407 
\idx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$


408 
& insertion of element \\


409 
\idx{Collect} & $(\alpha\To bool)\To\alpha\,set$


410 
& comprehension \\


411 
\idx{Compl} & $(\alpha\,set)\To\alpha\,set$


412 
& complement \\

104

413 
\idx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$

111

414 
& intersection over a set\\

104

415 
\idx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$

111

416 
& union over a set\\

104

417 
\idx{Inter} & $((\alpha\,set)set)\To\alpha\,set$

111

418 
&set of sets intersection \\

104

419 
\idx{Union} & $((\alpha\,set)set)\To\alpha\,set$

111

420 
&set of sets union \\


421 
\idx{range} & $(\alpha\To\beta )\To\beta\,set$


422 
& range of a function \\[1ex]


423 
\idx{Ball}~~\idx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$


424 
& bounded quantifiers \\


425 
\idx{mono} & $(\alpha\,set\To\beta\,set)\To bool$


426 
& monotonicity \\

104

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

111

428 
& injective/surjective \\


429 
\idx{inj_onto} & $[\alpha\To\beta ,\alpha\,set]\To bool$


430 
& injective over subset

104

431 
\end{tabular}


432 
\end{center}


433 
\subcaption{Constants}


434 


435 
\begin{center}


436 
\begin{tabular}{llrrr}

111

437 
\it symbol &\it name &\it metatype & \it prec & \it description \\

104

438 
\idx{INT} & \idx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &

111

439 
intersection over a type\\

104

440 
\idx{UN} & \idx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &

111

441 
union over a type

104

442 
\end{tabular}


443 
\end{center}


444 
\subcaption{Binders}


445 


446 
\begin{center}


447 
\indexbold{*"`"`}


448 
\indexbold{*":}


449 
\indexbold{*"<"=}


450 
\begin{tabular}{rrrr}

111

451 
\it symbol & \it metatype & \it precedence & \it description \\


452 
\tt `` & $[\alpha\To\beta ,\alpha\,set]\To (\beta\,set)$


453 
& Left 90 & image \\


454 
\idx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$


455 
& Left 70 & intersection ($\inter$) \\


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


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


458 
\tt: & $[\alpha ,\alpha\,set]\To bool$


459 
& Left 50 & membership ($\in$) \\


460 
\tt <= & $[\alpha\,set,\alpha\,set]\To bool$


461 
& Left 50 & subset ($\subseteq$)

104

462 
\end{tabular}


463 
\end{center}


464 
\subcaption{Infixes}


465 
\caption{Syntax of {\HOL}'s set theory} \label{holsetsyntax}


466 
\end{figure}


467 


468 


469 
\begin{figure}


470 
\begin{center} \tt\frenchspacing


471 
\begin{tabular}{rrr}

111

472 
\it external & \it internal & \it description \\

104

473 
$a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm negated membership\\


474 
\{$a@1$, $\ldots$, $a@n$\} & insert($a@1$,$\cdots$,insert($a@n$,0)) &


475 
\rm finite set \\

111

476 
\{$x$.$P[x]$\} & Collect($\lambda x.P[x]$) &

104

477 
\rm comprehension \\

111

478 
\idx{INT} $x$:$A$.$B[x]$ & INTER($A$,$\lambda x.B[x]$) &


479 
\rm intersection over a set \\


480 
\idx{UN} $x$:$A$.$B[x]$ & UNION($A$,$\lambda x.B[x]$) &


481 
\rm union over a set \\


482 
\idx{!} $x$:$A$.$P[x]$ & Ball($A$,$\lambda x.P[x]$) &


483 
\rm bounded $\forall$ \\


484 
\idx{?} $x$:$A$.$P[x]$ & Bex($A$,$\lambda x.P[x]$) &


485 
\rm bounded $\exists$ \\[1ex]


486 
\idx{ALL} $x$:$A$.$P[x]$ & Ball($A$,$\lambda x.P[x]$) &


487 
\rm bounded $\forall$ \\


488 
\idx{EX} $x$:$A$.$P[x]$ & Bex($A$,$\lambda x.P[x]$) &


489 
\rm bounded $\exists$

104

490 
\end{tabular}


491 
\end{center}


492 
\subcaption{Translations}


493 


494 
\dquotes


495 
\[\begin{array}{rcl}


496 
term & = & \hbox{other terms\ldots} \\

111

497 
&  & "\{\}" \\


498 
&  & "\{ " term\; ("," term)^* " \}" \\


499 
&  & "\{ " id " . " formula " \}" \\


500 
&  & term " `` " term \\


501 
&  & term " Int " term \\


502 
&  & term " Un " term \\


503 
&  & "INT~~" id ":" term " . " term \\


504 
&  & "UN~~~" id ":" term " . " term \\


505 
&  & "INT~~" id~id^* " . " term \\


506 
&  & "UN~~~" id~id^* " . " term \\[2ex]

104

507 
formula & = & \hbox{other formulae\ldots} \\

111

508 
&  & term " : " term \\


509 
&  & term " \ttilde: " term \\


510 
&  & term " <= " term \\


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


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


513 
&  & "ALL " id ":" term " . " formula \\


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

104

515 
\end{array}


516 
\]


517 
\subcaption{Full Grammar}


518 
\caption{Syntax of {\HOL}'s set theory (continued)} \label{holsetsyntax2}


519 
\end{figure}


520 


521 


522 
\begin{figure} \makeatother


523 
\begin{ttbox}


524 
\idx{mem_Collect_eq} (a : \{x.P(x)\}) = P(a)


525 
\idx{Collect_mem_eq} \{x.x:A\} = A


526 
\subcaption{Isomorphisms between predicates and sets}


527 


528 
\idx{empty_def} \{\} == \{x.x= False\}


529 
\idx{insert_def} insert(a,B) == \{x.x=a\} Un B


530 
\idx{Ball_def} Ball(A,P) == ! x. x:A > P(x)


531 
\idx{Bex_def} Bex(A,P) == ? x. x:A & P(x)


532 
\idx{subset_def} A <= B == ! x:A. x:B


533 
\idx{Un_def} A Un B == \{x.x:A  x:B\}


534 
\idx{Int_def} A Int B == \{x.x:A & x:B\}


535 
\idx{set_diff_def} A  B == \{x.x:A & x~:B\}


536 
\idx{Compl_def} Compl(A) == \{x. ~ x:A\}


537 
\idx{INTER_def} INTER(A,B) == \{y. ! x:A. y: B(x)\}


538 
\idx{UNION_def} UNION(A,B) == \{y. ? x:A. y: B(x)\}


539 
\idx{INTER1_def} INTER1(B) == INTER(\{x.True\}, B)


540 
\idx{UNION1_def} UNION1(B) == UNION(\{x.True\}, B)


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


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


543 
\idx{image_def} f``A == \{y. ? x:A. y=f(x)\}


544 
\idx{range_def} range(f) == \{y. ? x. y=f(x)\}


545 
\idx{mono_def} mono(f) == !A B. A <= B > f(A) <= f(B)


546 
\idx{inj_def} inj(f) == ! x y. f(x)=f(y) > x=y


547 
\idx{surj_def} surj(f) == ! y. ? x. y=f(x)


548 
\idx{inj_onto_def} inj_onto(f,A) == !x:A. !y:A. f(x)=f(y) > x=y


549 
\subcaption{Definitions}


550 
\end{ttbox}


551 
\caption{Rules of {\HOL}'s set theory} \label{holsetrules}


552 
\end{figure}


553 


554 


555 
\begin{figure} \makeatother


556 
\begin{ttbox}


557 
\idx{CollectI} [ P(a) ] ==> a : \{x.P(x)\}


558 
\idx{CollectD} [ a : \{x.P(x)\} ] ==> P(a)


559 
\idx{CollectE} [ a : \{x.P(x)\}; P(a) ==> W ] ==> W


560 
\idx{Collect_cong} [ !!x. P(x)=Q(x) ] ==> \{x. P(x)\} = \{x. Q(x)\}


561 
\subcaption{Comprehension}


562 


563 
\idx{ballI} [ !!x. x:A ==> P(x) ] ==> ! x:A. P(x)


564 
\idx{bspec} [ ! x:A. P(x); x:A ] ==> P(x)


565 
\idx{ballE} [ ! x:A. P(x); P(x) ==> Q; ~ x:A ==> Q ] ==> Q


566 
\idx{ball_cong} [ A=A'; !!x. x:A' ==> P(x) = P'(x) ] ==>


567 
(! x:A. P(x)) = (! x:A'. P'(x))


568 


569 
\idx{bexI} [ P(x); x:A ] ==> ? x:A. P(x)


570 
\idx{bexCI} [ ! x:A. ~ P(x) ==> P(a); a:A ] ==> ? x:A.P(x)


571 
\idx{bexE} [ ? x:A. P(x); !!x. [ x:A; P(x) ] ==> Q ] ==> Q


572 
\subcaption{Bounded quantifiers}


573 


574 
\idx{subsetI} (!!x.x:A ==> x:B) ==> A <= B


575 
\idx{subsetD} [ A <= B; c:A ] ==> c:B


576 
\idx{subsetCE} [ A <= B; ~ (c:A) ==> P; c:B ==> P ] ==> P


577 


578 
\idx{subset_refl} A <= A


579 
\idx{subset_antisym} [ A <= B; B <= A ] ==> A = B


580 
\idx{subset_trans} [ A<=B; B<=C ] ==> A<=C


581 


582 
\idx{set_ext} [ !!x. (x:A) = (x:B) ] ==> A = B


583 
\idx{equalityD1} A = B ==> A<=B


584 
\idx{equalityD2} A = B ==> B<=A


585 
\idx{equalityE} [ A = B; [ A<=B; B<=A ] ==> P ] ==> P


586 


587 
\idx{equalityCE} [ A = B; [ c:A; c:B ] ==> P;


588 
[ ~ c:A; ~ c:B ] ==> P


589 
] ==> P


590 
\subcaption{The subset and equality relations}


591 
\end{ttbox}


592 
\caption{Derived rules for set theory} \label{holset1}


593 
\end{figure}


594 


595 


596 
\begin{figure} \makeatother


597 
\begin{ttbox}


598 
\idx{emptyE} a : \{\} ==> P


599 


600 
\idx{insertI1} a : insert(a,B)


601 
\idx{insertI2} a : B ==> a : insert(b,B)


602 
\idx{insertE} [ a : insert(b,A); a=b ==> P; a:A ==> P ] ==>


603 


604 
\idx{ComplI} [ c:A ==> False ] ==> c : Compl(A)


605 
\idx{ComplD} [ c : Compl(A) ] ==> ~ c:A


606 


607 
\idx{UnI1} c:A ==> c : A Un B


608 
\idx{UnI2} c:B ==> c : A Un B


609 
\idx{UnCI} (~c:B ==> c:A) ==> c : A Un B


610 
\idx{UnE} [ c : A Un B; c:A ==> P; c:B ==> P ] ==> P


611 


612 
\idx{IntI} [ c:A; c:B ] ==> c : A Int B


613 
\idx{IntD1} c : A Int B ==> c:A


614 
\idx{IntD2} c : A Int B ==> c:B


615 
\idx{IntE} [ c : A Int B; [ c:A; c:B ] ==> P ] ==> P


616 


617 
\idx{UN_I} [ a:A; b: B(a) ] ==> b: (UN x:A. B(x))


618 
\idx{UN_E} [ b: (UN x:A. B(x)); !!x.[ x:A; b:B(x) ] ==> R ] ==> R


619 


620 
\idx{INT_I} (!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))


621 
\idx{INT_D} [ b: (INT x:A. B(x)); a:A ] ==> b: B(a)


622 
\idx{INT_E} [ b: (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R ] ==> R


623 


624 
\idx{UnionI} [ X:C; A:X ] ==> A : Union(C)


625 
\idx{UnionE} [ A : Union(C); !!X.[ A:X; X:C ] ==> R ] ==> R


626 


627 
\idx{InterI} [ !!X. X:C ==> A:X ] ==> A : Inter(C)


628 
\idx{InterD} [ A : Inter(C); X:C ] ==> A:X


629 
\idx{InterE} [ A : Inter(C); A:X ==> R; ~ X:C ==> R ] ==> R


630 
\end{ttbox}


631 
\caption{Further derived rules for set theory} \label{holset2}


632 
\end{figure}


633 


634 


635 
\section{A formulation of set theory}


636 
Historically, higherorder logic gives a foundation for Russell and


637 
Whitehead's theory of classes. Let us use modern terminology and call them


638 
{\bf sets}, but note that these sets are distinct from those of {\ZF} set


639 
theory, and behave more like {\ZF} classes.


640 
\begin{itemize}


641 
\item


642 
Sets are given by predicates over some type~$\sigma$. Types serve to


643 
define universes for sets, but type checking is still significant.


644 
\item


645 
There is a universal set (for each type). Thus, sets have complements, and


646 
may be defined by absolute comprehension.


647 
\item


648 
Although sets may contain other sets as elements, the containing set must


649 
have a more complex type.


650 
\end{itemize}


651 
Finite unions and intersections have the same behaviour in {\HOL} as they


652 
do in~{\ZF}. In {\HOL} the intersection of the empty set is welldefined,


653 
denoting the universal set for the given type.


654 


655 
\subsection{Syntax of set theory}


656 
The type $\alpha\,set$ is essentially the same as $\alpha\To bool$. The new


657 
type is defined for clarity and to avoid complications involving function


658 
types in unification. Since Isabelle does not support type definitions (as


659 
discussed above), the isomorphisms between the two types are declared


660 
explicitly. Here they are natural: {\tt Collect} maps $\alpha\To bool$ to


661 
$\alpha\,set$, while \hbox{\tt op :} maps in the other direction (ignoring


662 
argument order).


663 


664 
Figure~\ref{holsetsyntax} lists the constants, infixes, and syntax


665 
translations. Figure~\ref{holsetsyntax2} presents the grammar of the new


666 
constructs. Infix operators include union and intersection ($A\union B$


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


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


669 
\verb~($a$:$b$\verb). The {\tt\{\ldots\}} notation abbreviates finite


670 
sets constructed in the obvious manner using~{\tt insert} and~$\{\}$ (the


671 
empty set):


672 
\begin{eqnarray*}


673 
\{a,b,c\} & \equiv & {\tt insert}(a,{\tt insert}(b,{\tt insert}(c,\emptyset)))


674 
\end{eqnarray*}


675 


676 
The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type)


677 
that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free


678 
occurrences of~$x$. This syntax expands to \ttindexbold{Collect}$(\lambda


679 
x.P[x])$.


680 


681 
The set theory defines two {\bf bounded quantifiers}:


682 
\begin{eqnarray*}


683 
\forall x\in A.P[x] &\hbox{which abbreviates}& \forall x. x\in A\imp P[x] \\


684 
\exists x\in A.P[x] &\hbox{which abbreviates}& \exists x. x\in A\conj P[x]


685 
\end{eqnarray*}


686 
The constants~\ttindexbold{Ball} and~\ttindexbold{Bex} are defined


687 
accordingly. Instead of {\tt Ball($A$,$P$)} and {\tt Bex($A$,$P$)} we may


688 
write\index{*"!}\index{*"?}\index{*ALL}\index{*EX}


689 
\hbox{\tt !~$x$:$A$.$P[x]$} and \hbox{\tt ?~$x$:$A$.$P[x]$}.


690 
Isabelle's usual notation, \ttindex{ALL} and \ttindex{EX}, is also


691 
available. As with


692 
ordinary quantifiers, the contents of \ttindexbold{HOL_quantifiers} specifies


693 
which notation should be used for output.


694 


695 
Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and


696 
$\bigcap@{x\in A}B[x]$, are written


697 
\ttindexbold{UN}~\hbox{\tt$x$:$A$.$B[x]$} and


698 
\ttindexbold{INT}~\hbox{\tt$x$:$A$.$B[x]$}.


699 
Unions and intersections over types, namely $\bigcup@x B[x]$ and


700 
$\bigcap@x B[x]$, are written


701 
\ttindexbold{UN}~\hbox{\tt$x$.$B[x]$} and


702 
\ttindexbold{INT}~\hbox{\tt$x$.$B[x]$}; they are equivalent to the previous


703 
union/intersection operators when $A$ is the universal set.


704 
The set of set union and intersection operators ($\bigcup A$ and $\bigcap


705 
A$) are not binders, but equals $\bigcup@{x\in A}x$ and $\bigcap@{x\in


706 
A}x$, respectively.


707 


708 
\subsection{Axioms and rules of set theory}


709 
The axioms \ttindexbold{mem_Collect_eq} and


710 
\ttindexbold{Collect_mem_eq} assert that the functions {\tt Collect} and


711 
\hbox{\tt op :} are isomorphisms.


712 
All the other axioms are definitions; see Figure~\ref{holsetrules}.


713 
These include straightforward properties of functions: image~({\tt``}) and


714 
{\tt range}, and predicates concerning monotonicity, injectiveness, etc.


715 


716 
{\HOL}'s set theory has the {\ML} identifier \ttindexbold{Set.thy}.


717 


718 
\begin{figure} \makeatother


719 
\begin{ttbox}


720 
\idx{imageI} [ x:A ] ==> f(x) : f``A


721 
\idx{imageE} [ b : f``A; !!x.[ b=f(x); x:A ] ==> P ] ==> P


722 


723 
\idx{rangeI} f(x) : range(f)


724 
\idx{rangeE} [ b : range(f); !!x.[ b=f(x) ] ==> P ] ==> P


725 


726 
\idx{monoI} [ !!A B. A <= B ==> f(A) <= f(B) ] ==> mono(f)


727 
\idx{monoD} [ mono(f); A <= B ] ==> f(A) <= f(B)


728 


729 
\idx{injI} [ !! x y. f(x) = f(y) ==> x=y ] ==> inj(f)


730 
\idx{inj_inverseI} (!!x. g(f(x)) = x) ==> inj(f)


731 
\idx{injD} [ inj(f); f(x) = f(y) ] ==> x=y


732 


733 
\idx{Inv_f_f} inj(f) ==> Inv(f,f(x)) = x


734 
\idx{f_Inv_f} y : range(f) ==> f(Inv(f,y)) = y


735 


736 
\idx{Inv_injective}


737 
[ Inv(f,x)=Inv(f,y); x: range(f); y: range(f) ] ==> x=y


738 


739 
\idx{inj_ontoI}


740 
(!! x y. [ f(x) = f(y); x:A; y:A ] ==> x=y) ==> inj_onto(f,A)


741 


742 
\idx{inj_onto_inverseI}


743 
(!!x. x:A ==> g(f(x)) = x) ==> inj_onto(f,A)


744 


745 
\idx{inj_ontoD}


746 
[ inj_onto(f,A); f(x)=f(y); x:A; y:A ] ==> x=y


747 


748 
\idx{inj_onto_contraD}


749 
[ inj_onto(f,A); x~=y; x:A; y:A ] ==> ~ f(x)=f(y)


750 
\end{ttbox}


751 
\caption{Derived rules involving functions} \label{holfun}


752 
\end{figure}


753 


754 


755 
\begin{figure} \makeatother


756 
\begin{ttbox}


757 
\idx{Union_upper} B:A ==> B <= Union(A)


758 
\idx{Union_least} [ !!X. X:A ==> X<=C ] ==> Union(A) <= C


759 


760 
\idx{Inter_lower} B:A ==> Inter(A) <= B


761 
\idx{Inter_greatest} [ !!X. X:A ==> C<=X ] ==> C <= Inter(A)


762 


763 
\idx{Un_upper1} A <= A Un B


764 
\idx{Un_upper2} B <= A Un B


765 
\idx{Un_least} [ A<=C; B<=C ] ==> A Un B <= C


766 


767 
\idx{Int_lower1} A Int B <= A


768 
\idx{Int_lower2} A Int B <= B


769 
\idx{Int_greatest} [ C<=A; C<=B ] ==> C <= A Int B


770 
\end{ttbox}


771 
\caption{Derived rules involving subsets} \label{holsubset}


772 
\end{figure}


773 


774 


775 
\begin{figure} \makeatother


776 
\begin{ttbox}


777 
\idx{Int_absorb} A Int A = A


778 
\idx{Int_commute} A Int B = B Int A


779 
\idx{Int_assoc} (A Int B) Int C = A Int (B Int C)


780 
\idx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)


781 


782 
\idx{Un_absorb} A Un A = A


783 
\idx{Un_commute} A Un B = B Un A


784 
\idx{Un_assoc} (A Un B) Un C = A Un (B Un C)


785 
\idx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)


786 


787 
\idx{Compl_disjoint} A Int Compl(A) = \{x.False\}


788 
\idx{Compl_partition} A Un Compl(A) = \{x.True\}


789 
\idx{double_complement} Compl(Compl(A)) = A


790 
\idx{Compl_Un} Compl(A Un B) = Compl(A) Int Compl(B)


791 
\idx{Compl_Int} Compl(A Int B) = Compl(A) Un Compl(B)


792 


793 
\idx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B)


794 
\idx{Int_Union_image} A Int Union(B) = (UN C:B. A Int C)


795 
\idx{Un_Union_image}


796 
(UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)


797 


798 
\idx{Inter_Un_distrib} Inter(A Un B) = Inter(A) Int Inter(B)


799 
\idx{Un_Inter_image} A Un Inter(B) = (INT C:B. A Un C)


800 
\idx{Int_Inter_image}


801 
(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)


802 
\end{ttbox}


803 
\caption{Set equalities} \label{holequalities}


804 
\end{figure}


805 


806 


807 
\subsection{Derived rules for sets}


808 
Figures~\ref{holset1} and~\ref{holset2} present derived rules. Most


809 
are obvious and resemble rules of Isabelle's {\ZF} set theory. The


810 
rules named $XXX${\tt_cong} break down equalities. Certain rules, such as


811 
\ttindexbold{subsetCE}, \ttindexbold{bexCI} and \ttindexbold{UnCI}, are


812 
designed for classical reasoning; the more natural rules \ttindexbold{subsetD},


813 
\ttindexbold{bexI}, \ttindexbold{Un1} and~\ttindexbold{Un2} are not


814 
strictly necessary. Similarly, \ttindexbold{equalityCE} supports classical


815 
reasoning about extensionality, after the fashion of \ttindex{iffCE}. See


816 
the file \ttindexbold{HOL/set.ML} for proofs pertaining to set theory.


817 


818 
Figure~\ref{holfun} presents derived rules involving functions. See


819 
the file \ttindexbold{HOL/fun.ML} for a complete listing.


820 


821 
Figure~\ref{holsubset} presents lattice properties of the subset relation.


822 
See \ttindexbold{HOL/subset.ML}.


823 


824 
Figure~\ref{holequalities} presents set equalities. See


825 
\ttindexbold{HOL/equalities.ML}.


826 


827 


828 
\begin{figure} \makeatother


829 
\begin{center}


830 
\begin{tabular}{rrr}

111

831 
\it name &\it metatype & \it description \\


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


833 
& ordered pairs $\langle a,b\rangle$ \\


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


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


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


837 
& generalized projection

104

838 
\end{tabular}


839 
\end{center}


840 
\subcaption{Constants}


841 


842 
\begin{ttbox}


843 
\idx{fst_def} fst(p) == @a. ? b. p = <a,b>


844 
\idx{snd_def} snd(p) == @b. ? a. p = <a,b>


845 
\idx{split_def} split(p,c) == c(fst(p),snd(p))


846 
\subcaption{Definitions}


847 


848 
\idx{Pair_inject} [ <a, b> = <a',b'>; [ a=a'; b=b' ] ==> R ] ==> R


849 


850 
\idx{fst} fst(<a,b>) = a


851 
\idx{snd} snd(<a,b>) = b


852 
\idx{split} split(<a,b>, c) = c(a,b)


853 


854 
\idx{surjective_pairing} p = <fst(p),snd(p)>


855 
\subcaption{Derived rules}


856 
\end{ttbox}


857 
\caption{Type $\alpha\times\beta$}


858 
\label{holprod}


859 
\end{figure}


860 


861 


862 
\begin{figure} \makeatother


863 
\begin{center}


864 
\begin{tabular}{rrr}

111

865 
\it name &\it metatype & \it description \\


866 
\idx{Inl} & $\alpha \To \alpha+\beta$ & first injection\\


867 
\idx{Inr} & $\beta \To \alpha+\beta$ & second injection\\


868 
\idx{case} & $[\alpha+\beta, \alpha\To\gamma, \beta\To\gamma] \To\gamma$


869 
& conditional

104

870 
\end{tabular}


871 
\end{center}


872 
\subcaption{Constants}


873 


874 
\begin{ttbox}


875 
\idx{case_def} case == (%p f g. @z. (!x. p=Inl(x) > z=f(x)) &


876 
(!y. p=Inr(y) > z=g(y)))


877 
\subcaption{Definition}


878 


879 
\idx{Inl_not_Inr} ~ Inl(a)=Inr(b)


880 


881 
\idx{inj_Inl} inj(Inl)


882 
\idx{inj_Inr} inj(Inr)


883 


884 
\idx{sumE} [ !!x::'a. P(Inl(x)); !!y::'b. P(Inr(y)) ] ==> P(s)


885 


886 
\idx{case_Inl} case(Inl(x), f, g) = f(x)


887 
\idx{case_Inr} case(Inr(x), f, g) = g(x)


888 


889 
\idx{surjective_sum} case(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s)


890 
\subcaption{Derived rules}


891 
\end{ttbox}


892 
\caption{Rules for type $\alpha+\beta$}


893 
\label{holsum}


894 
\end{figure}


895 


896 


897 
\section{Types}


898 
The basic higherorder logic is augmented with a tremendous amount of


899 
material, including support for recursive function and type definitions.


900 
Space does not permit a detailed discussion. The present section describes


901 
product, sum, natural number and list types.


902 


903 
\subsection{Product and sum types}


904 
{\HOL} defines the product type $\alpha\times\beta$ and the sum type


905 
$\alpha+\beta$, with the ordered pair syntax {\tt<$a$,$b$>}, using fairly


906 
standard constructions (Figures~\ref{holprod} and~\ref{holsum}). Because


907 
Isabelle does not support type definitions, the isomorphisms between these


908 
types and their representations are made explicitly.


909 


910 
Most of the definitions are suppressed, but observe that the projections


911 
and conditionals are defined as descriptions. Their properties are easily


912 
proved using \ttindex{select_equality}. See \ttindexbold{HOL/prod.thy} and


913 
\ttindexbold{HOL/sum.thy} for details.


914 


915 
\begin{figure} \makeatother


916 
\indexbold{*"<}


917 
\begin{center}


918 
\begin{tabular}{rrr}

111

919 
\it symbol & \it metatype & \it description \\


920 
\idx{0} & $nat$ & zero \\


921 
\idx{Suc} & $nat \To nat$ & successor function\\

104

922 
\idx{nat_case} & $[nat, \alpha, nat\To\alpha] \To\alpha$

111

923 
& conditional\\

104

924 
\idx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$

111

925 
& primitive recursor\\

104

926 
\idx{pred_nat} & $(nat\times nat) set$ & predecessor relation


927 
\end{tabular}


928 
\end{center}


929 


930 
\begin{center}


931 
\indexbold{*"+}


932 
\index{*@{\tt*}bold}


933 
\index{/@{\tt/}bold}


934 
\index{//@{\tt//}bold}


935 
\index{+@{\tt+}bold}


936 
\index{@{\tt}bold}


937 
\begin{tabular}{rrrr}

111

938 
\it symbol & \it metatype & \it precedence & \it description \\


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


940 
\tt / & $[nat,nat]\To nat$ & Left 70 & division\\


941 
\tt // & $[nat,nat]\To nat$ & Left 70 & modulus\\


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


943 
\tt  & $[nat,nat]\To nat$ & Left 65 & subtraction

104

944 
\end{tabular}


945 
\end{center}


946 
\subcaption{Constants and infixes}


947 


948 
\begin{ttbox}


949 
\idx{nat_case_def} nat_case == (%n a f. @z. (n=0 > z=a) &


950 
(!x. n=Suc(x) > z=f(x)))


951 
\idx{pred_nat_def} pred_nat == \{p. ? n. p = <n, Suc(n)>\}


952 
\idx{less_def} m<n == <m,n>:pred_nat^+


953 
\idx{nat_rec_def} nat_rec(n,c,d) ==


954 
wfrec(pred_nat, n, %l g.nat_case(l, c, %m.d(m,g(m))))


955 


956 
\idx{add_def} m+n == nat_rec(m, n, %u v.Suc(v))


957 
\idx{diff_def} mn == nat_rec(n, m, %u v. nat_rec(v, 0, %x y.x))


958 
\idx{mult_def} m*n == nat_rec(m, 0, %u v. n + v)


959 
\idx{mod_def} m//n == wfrec(trancl(pred_nat), m, %j f. if(j<n,j,f(jn)))


960 
\idx{quo_def} m/n == wfrec(trancl(pred_nat),


961 
m, %j f. if(j<n,0,Suc(f(jn))))


962 
\subcaption{Definitions}


963 
\end{ttbox}


964 
\caption{Defining $nat$, the type of natural numbers} \label{holnat1}


965 
\end{figure}


966 


967 


968 
\begin{figure} \makeatother


969 
\begin{ttbox}


970 
\idx{nat_induct} [ P(0); !!k. [ P(k) ] ==> P(Suc(k)) ] ==> P(n)


971 


972 
\idx{Suc_not_Zero} Suc(m) ~= 0


973 
\idx{inj_Suc} inj(Suc)


974 
\idx{n_not_Suc_n} n~=Suc(n)


975 
\subcaption{Basic properties}


976 


977 
\idx{pred_natI} <n, Suc(n)> : pred_nat


978 
\idx{pred_natE}


979 
[ p : pred_nat; !!x n. [ p = <n, Suc(n)> ] ==> R ] ==> R


980 


981 
\idx{nat_case_0} nat_case(0, a, f) = a


982 
\idx{nat_case_Suc} nat_case(Suc(k), a, f) = f(k)


983 


984 
\idx{wf_pred_nat} wf(pred_nat)


985 
\idx{nat_rec_0} nat_rec(0,c,h) = c


986 
\idx{nat_rec_Suc} nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h))


987 
\subcaption{Case analysis and primitive recursion}


988 


989 
\idx{less_trans} [ i<j; j<k ] ==> i<k


990 
\idx{lessI} n < Suc(n)


991 
\idx{zero_less_Suc} 0 < Suc(n)


992 


993 
\idx{less_not_sym} n<m > ~ m<n


994 
\idx{less_not_refl} ~ n<n


995 
\idx{not_less0} ~ n<0


996 


997 
\idx{Suc_less_eq} (Suc(m) < Suc(n)) = (m<n)


998 
\idx{less_induct} [ !!n. [ ! m. m<n > P(m) ] ==> P(n) ] ==> P(n)


999 


1000 
\idx{less_linear} m<n  m=n  n<m


1001 
\subcaption{The lessthan relation}


1002 
\end{ttbox}


1003 
\caption{Derived rules for~$nat$} \label{holnat2}


1004 
\end{figure}


1005 


1006 


1007 
\subsection{The type of natural numbers, $nat$}


1008 
{\HOL} defines the natural numbers in a roundabout but traditional way.


1009 
The axiom of infinity postulates an type~$ind$ of individuals, which is


1010 
nonempty and closed under an injective operation. The natural numbers are


1011 
inductively generated by choosing an arbitrary individual for~0 and using


1012 
the injective operation to take successors. As usual, the isomorphisms


1013 
between~$nat$ and its representation are made explicitly.


1014 


1015 
The definition makes use of a least fixed point operator \ttindex{lfp},


1016 
defined using the KnasterTarski theorem. This in turn defines an operator


1017 
\ttindex{trancl} for taking the transitive closure of a relation. See


1018 
files \ttindexbold{HOL/lfp.thy} and \ttindexbold{HOL/trancl.thy} for


1019 
details. The definition of~$nat$ resides on \ttindexbold{HOL/nat.thy}.


1020 


1021 
Type $nat$ is postulated to belong to class~$ord$, which overloads $<$ and


1022 
$\leq$ on the natural numbers. As of this writing, Isabelle provides no


1023 
means of verifying that such overloading is sensible. On the other hand,


1024 
the {\HOL} theory includes no polymorphic axioms stating general properties


1025 
of $<$ and $\leq$.


1026 


1027 
File \ttindexbold{HOL/arith.ML} develops arithmetic on the natural numbers.


1028 
It defines addition, multiplication, subtraction, division, and remainder,


1029 
proving the theorem $a \bmod b + (a/b)\times b = a$. Division and


1030 
remainder are defined by repeated subtraction, which requires wellfounded


1031 
rather than primitive recursion.


1032 


1033 
Primitive recursion makes use of \ttindex{wfrec}, an operator for recursion


1034 
along arbitrary wellfounded relations; see \ttindexbold{HOL/wf.ML} for the


1035 
development. The predecessor relation, \ttindexbold{pred_nat}, is shown to


1036 
be wellfounded; recursion along this relation is primitive recursion,


1037 
while its transitive closure is~$<$.


1038 


1039 


1040 
\begin{figure} \makeatother


1041 
\begin{center}


1042 
\begin{tabular}{rrr}

111

1043 
\it symbol & \it metatype & \it description \\


1044 
\idx{Nil} & $\alpha list$ & the empty list\\


1045 
\idx{Cons} & $[\alpha, \alpha list] \To \alpha list$


1046 
& list constructor\\


1047 
\idx{list_rec} & $[\alpha list, \beta, [\alpha ,\alpha list,

104

1048 
\beta]\To\beta] \To \beta$

111

1049 
& list recursor\\


1050 
\idx{map} & $(\alpha\To\beta) \To (\alpha list \To \beta list)$


1051 
& mapping functional

104

1052 
\end{tabular}


1053 
\end{center}


1054 
\subcaption{Constants}


1055 


1056 
\begin{ttbox}


1057 
\idx{map_def} map(f,xs) == list_rec(xs, Nil, %x l r. Cons(f(x), r))


1058 
\subcaption{Definition}


1059 


1060 
\idx{list_induct}


1061 
[ P(Nil); !!x xs. [ P(xs) ] ==> P(Cons(x,xs)) ] ==> P(l)


1062 


1063 
\idx{Cons_not_Nil} ~ Cons(x,xs) = Nil


1064 
\idx{Cons_Cons_eq} (Cons(x,xs)=Cons(y,ys)) = (x=y & xs=ys)


1065 


1066 
\idx{list_rec_Nil} list_rec(Nil,c,h) = c


1067 
\idx{list_rec_Cons} list_rec(Cons(a,l), c, h) = h(a, l, list_rec(l,c,h))


1068 


1069 
\idx{map_Nil} map(f,Nil) = Nil


1070 
\idx{map_Cons} map(f, Cons(x,xs)) = Cons(f(x), map(f,xs))


1071 
\end{ttbox}


1072 
\caption{The type of lists and its operations} \label{hollist}


1073 
\end{figure}


1074 


1075 


1076 
\subsection{The type constructor for lists, $\alpha\,list$}


1077 
{\HOL}'s definition of lists is an example of an experimental method for


1078 
handling recursive data types. The details need not concern us here; see


1079 
the file \ttindexbold{HOL/list.ML}. Figure~\ref{hollist} presents the


1080 
basic list operations, with their types and properties. In particular,


1081 
\ttindexbold{list_rec} is a primitive recursion operator for lists, in the


1082 
style of MartinL\"of type theory. It is derived from wellfounded


1083 
recursion, a general principle that can express arbitrary total recursive


1084 
functions.


1085 


1086 


1087 
\subsection{The type constructor for lazy lists, $\alpha\,llist$}


1088 
The definition of lazy lists demonstrates methods for handling infinite


1089 
data structures and coinduction in higherorder logic. It defines an


1090 
operator for corecursion on lazy lists, which is used to define a few


1091 
simple functions such as map and append. Corecursion cannot easily define


1092 
operations such as filter, which can compute indefinitely before yielding


1093 
the next element (if any!) of the lazy list. A coinduction principle is


1094 
defined for proving equations on lazy lists. See the files


1095 
\ttindexbold{HOL/llist.thy} and \ttindexbold{HOL/llist.ML} for the formal


1096 
derivations. I have written a report discussing the treatment of lazy


1097 
lists, and finite lists also~\cite{paulsoncoind}.


1098 


1099 


1100 
\section{Classical proof procedures} \label{holclaprover}


1101 
{\HOL} derives classical introduction rules for $\disj$ and~$\exists$, as


1102 
well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap


1103 
rule (Figure~\ref{hollemmas2}).


1104 


1105 
The classical reasoning module is set up for \HOL, as the structure


1106 
\ttindexbold{Classical}. This structure is open, so {\ML} identifiers such


1107 
as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.


1108 


1109 
{\HOL} defines the following classical rule sets:


1110 
\begin{ttbox}


1111 
prop_cs : claset


1112 
HOL_cs : claset


1113 
HOL_dup_cs : claset


1114 
set_cs : claset


1115 
\end{ttbox}


1116 
\begin{description}


1117 
\item[\ttindexbold{prop_cs}] contains the propositional rules, namely


1118 
those for~$\top$, $\bot$, $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$,


1119 
along with the rule~\ttindex{refl}.


1120 


1121 
\item[\ttindexbold{HOL_cs}]


1122 
extends {\tt prop_cs} with the safe rules \ttindex{allI} and~\ttindex{exE}


1123 
and the unsafe rules \ttindex{allE} and~\ttindex{exI}, as well as rules for


1124 
unique existence. Search using this is incomplete since quantified


1125 
formulae are used at most once.


1126 


1127 
\item[\ttindexbold{HOL_dup_cs}]


1128 
extends {\tt prop_cs} with the safe rules \ttindex{allI} and~\ttindex{exE}


1129 
and the unsafe rules \ttindex{all_dupE} and~\ttindex{exCI}, as well as


1130 
rules for unique existence. Search using this is complete  quantified


1131 
formulae may be duplicated  but frequently fails to terminate. It is


1132 
generally unsuitable for depthfirst search.


1133 


1134 
\item[\ttindexbold{set_cs}]


1135 
extends {\tt HOL_cs} with rules for the bounded quantifiers, subsets,


1136 
comprehensions, unions/intersections, complements, finite setes, images and


1137 
ranges.


1138 
\end{description}


1139 
\noindent


1140 
See the {\em Reference Manual} for more discussion of classical proof


1141 
methods.


1142 


1143 

111

1144 
\section{The examples directories}


1145 
Directory {\tt Subst} contains Martin Coen's mechanization of a theory of


1146 
substitutions and unifiers. It is based on Paulson's previous


1147 
mechanization in {\LCF}~\cite{paulson85} of theory Manna and Waldinger's


1148 
theory~\cite{mw81}.


1149 


1150 
Directory {\tt ex} contains other examples and experimental proofs in


1151 
{\HOL}. Here is an overview of the more interesting files.

104

1152 
\begin{description}


1153 
\item[\ttindexbold{HOL/ex/meson.ML}]


1154 
contains an experimental implementation of the MESON proof procedure,


1155 
inspired by Plaisted~\cite{plaisted90}. It is much more powerful than


1156 
Isabelle's classical module.


1157 

111

1158 
\item[\ttindexbold{HOL/ex/mesontest.ML}]

104

1159 
contains test data for the MESON proof procedure.


1160 


1161 
\item[\ttindexbold{HOL/ex/set.ML}]


1162 
proves Cantor's Theorem (see below) and the Schr\"oderBernstein Theorem.


1163 

111

1164 
\item[\ttindexbold{HOL/ex/pl.ML}]

104

1165 
proves the soundness and completeness of classical propositional logic,


1166 
given a truth table semantics. The only connective is $\imp$. A


1167 
Hilbertstyle axiom system is specified, and its set of theorems defined


1168 
inductively.


1169 

111

1170 
\item[\ttindexbold{HOL/ex/term.ML}]


1171 
contains proofs about an experimental recursive type definition;


1172 
the recursion goes through the type constructor~$list$.

104

1173 


1174 
\item[\ttindexbold{HOL/ex/simult.ML}]


1175 
defines primitives for solving mutually recursive equations over sets.


1176 
It constructs sets of trees and forests as an example, including induction


1177 
and recursion rules that handle the mutual recursion.

111

1178 


1179 
\item[\ttindexbold{HOL/ex/mt.ML}]


1180 
contains Jacob Frost's formalization~\cite{frost93} of a coinduction


1181 
example by Milner and Tofte~\cite{milnercoind}.

104

1182 
\end{description}


1183 


1184 


1185 
\section{Example: deriving the conjunction rules}


1186 
{\HOL} comes with a body of derived rules, ranging from simple properties


1187 
of the logical constants and set theory to wellfounded recursion. Many of


1188 
them are worth studying.


1189 


1190 
Deriving natural deduction rules for the logical constants from their


1191 
definitions is an archetypal example of higherorder reasoning. Let us


1192 
verify two conjunction rules:


1193 
\[ \infer[({\conj}I)]{P\conj Q}{P & Q} \qquad\qquad


1194 
\infer[({\conj}E1)]{P}{P\conj Q}


1195 
\]


1196 


1197 
\subsection{The introduction rule}


1198 
We begin by stating the rule as the goal. The list of premises $[P,Q]$ is


1199 
bound to the {\ML} variable~{\tt prems}.


1200 
\begin{ttbox}


1201 
val prems = goal HOL.thy "[ P; Q ] ==> P&Q";


1202 
{\out Level 0}


1203 
{\out P & Q}


1204 
{\out 1. P & Q}

111

1205 
{\out val prems = ["P [P]", "Q [Q]"] : thm list}

104

1206 
\end{ttbox}


1207 
The next step is to unfold the definition of conjunction. But


1208 
\ttindex{and_def} uses {\HOL}'s internal equality, so


1209 
\ttindex{rewrite_goals_tac} is unsuitable.


1210 
Instead, we perform substitution using the rule \ttindex{ssubst}:


1211 
\begin{ttbox}


1212 
by (resolve_tac [and_def RS ssubst] 1);


1213 
{\out Level 1}


1214 
{\out P & Q}


1215 
{\out 1. ! R. (P > Q > R) > R}


1216 
\end{ttbox}


1217 
We now apply $(\forall I)$ and $({\imp}I)$:


1218 
\begin{ttbox}


1219 
by (resolve_tac [allI] 1);


1220 
{\out Level 2}


1221 
{\out P & Q}


1222 
{\out 1. !!R. (P > Q > R) > R}


1223 
by (resolve_tac [impI] 1);


1224 
{\out Level 3}


1225 
{\out P & Q}


1226 
{\out 1. !!R. P > Q > R ==> R}


1227 
\end{ttbox}


1228 
The assumption is a nested implication, which may be eliminated


1229 
using~\ttindex{mp} resolved with itself. Elimresolution, here, performs


1230 
backwards chaining. More straightforward would be to use~\ttindex{impE}


1231 
twice.


1232 
\index{*RS}


1233 
\begin{ttbox}


1234 
by (eresolve_tac [mp RS mp] 1);


1235 
{\out Level 4}


1236 
{\out P & Q}


1237 
{\out 1. !!R. P}


1238 
{\out 2. !!R. Q}


1239 
\end{ttbox}


1240 
These two subgoals are simply the premises:


1241 
\begin{ttbox}


1242 
by (REPEAT (resolve_tac prems 1));


1243 
{\out Level 5}


1244 
{\out P & Q}


1245 
{\out No subgoals!}


1246 
\end{ttbox}


1247 


1248 


1249 
\subsection{The elimination rule}


1250 
Again, we bind the list of premises (in this case $[P\conj Q]$)


1251 
to~{\tt prems}.


1252 
\begin{ttbox}


1253 
val prems = goal HOL.thy "[ P & Q ] ==> P";


1254 
{\out Level 0}


1255 
{\out P}


1256 
{\out 1. P}

111

1257 
{\out val prems = ["P & Q [P & Q]"] : thm list}

104

1258 
\end{ttbox}


1259 
Working with premises that involve defined constants can be tricky. We


1260 
must expand the definition of conjunction in the metaassumption $P\conj


1261 
Q$. The rule \ttindex{subst} performs substitution in forward proofs.


1262 
We get two resolvents, since the vacuous substitution is valid:


1263 
\begin{ttbox}


1264 
prems RL [and_def RS subst];


1265 
{\out val it = ["! R. (P > Q > R) > R [P & Q]",}


1266 
{\out "P & Q [P & Q]"] : thm list}


1267 
\end{ttbox}


1268 
By applying $(\forall E)$ and $({\imp}E)$ to the resolvents, we dispose of

111

1269 
the vacuous one and put the other into a convenient form:\footnote


1270 
{In higherorder logic, {\tt spec RS mp} fails because the resolution yields


1271 
two results, namely $\List{\forall x.x; P}\Imp Q$ and $\List{\forall


1272 
x.P(x)\imp Q(x); P(x)}\Imp Q(x)$. In firstorder logic, the resolution


1273 
yields only the latter result.}

104

1274 
\index{*RL}


1275 
\begin{ttbox}


1276 
prems RL [and_def RS subst] RL [spec] RL [mp];


1277 
{\out val it = ["P > Q > ?Q ==> ?Q [P & Q]"] : thm list}


1278 
\end{ttbox}


1279 
This is a list containing a single rule, which is directly applicable to


1280 
our goal:


1281 
\begin{ttbox}


1282 
by (resolve_tac it 1);


1283 
{\out Level 1}


1284 
{\out P}


1285 
{\out 1. P > Q > P}


1286 
\end{ttbox}


1287 
The subgoal is a trivial implication. Recall that \ttindex{ares_tac} is a


1288 
combination of \ttindex{assume_tac} and \ttindex{resolve_tac}.


1289 
\begin{ttbox}


1290 
by (REPEAT (ares_tac [impI] 1));


1291 
{\out Level 2}


1292 
{\out P}


1293 
{\out No subgoals!}


1294 
\end{ttbox}


1295 


1296 


1297 
\section{Example: Cantor's Theorem}


1298 
Cantor's Theorem states that every set has more subsets than it has


1299 
elements. It has become a favourite example in higherorder logic since


1300 
it is so easily expressed:


1301 
\[ \forall f::[\alpha,\alpha]\To bool. \exists S::\alpha\To bool.


1302 
\forall x::\alpha. f(x) \not= S


1303 
\]


1304 
Viewing types as sets, $\alpha\To bool$ represents the powerset


1305 
of~$\alpha$. This version states that for every function from $\alpha$ to


1306 
its powerset, some subset is outside its range.


1307 


1308 
The Isabelle proof uses {\HOL}'s set theory, with the type $\alpha\,set$ and


1309 
the operator \ttindex{range}. Since it avoids quantification, we may


1310 
inspect the subset found by the proof.


1311 
\begin{ttbox}


1312 
goal Set.thy "~ ?S : range(f :: 'a=>'a set)";


1313 
{\out Level 0}


1314 
{\out ~ ?S : range(f)}


1315 
{\out 1. ~ ?S : range(f)}


1316 
\end{ttbox}


1317 
The first two steps are routine. The rule \ttindex{rangeE} reasons that,


1318 
since $\Var{S}\in range(f)$, we have $\Var{S}=f(x)$ for some~$x$.


1319 
\begin{ttbox}


1320 
by (resolve_tac [notI] 1);


1321 
{\out Level 1}


1322 
{\out ~ ?S : range(f)}


1323 
{\out 1. ?S : range(f) ==> False}


1324 
by (eresolve_tac [rangeE] 1);


1325 
{\out Level 2}


1326 
{\out ~ ?S : range(f)}


1327 
{\out 1. !!x. ?S = f(x) ==> False}


1328 
\end{ttbox}


1329 
Next, we apply \ttindex{equalityCE}, reasoning that since $\Var{S}=f(x)$,


1330 
we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f(x)$ for


1331 
any~$\Var{c}$.


1332 
\begin{ttbox}


1333 
by (eresolve_tac [equalityCE] 1);


1334 
{\out Level 3}


1335 
{\out ~ ?S : range(f)}


1336 
{\out 1. !!x. [ ?c3(x) : ?S; ?c3(x) : f(x) ] ==> False}


1337 
{\out 2. !!x. [ ~ ?c3(x) : ?S; ~ ?c3(x) : f(x) ] ==> False}


1338 
\end{ttbox}


1339 
Now we use a bit of creativity. Suppose that $\Var{S}$ has the form of a


1340 
comprehension. Then $\Var{c}\in\{x.\Var{P}(x)\}$ implies


1341 
$\Var{P}(\Var{c})\}$.\index{*CollectD}


1342 
\begin{ttbox}


1343 
by (dresolve_tac [CollectD] 1);


1344 
{\out Level 4}


1345 
{\out ~ \{x. ?P7(x)\} : range(f)}


1346 
{\out 1. !!x. [ ?c3(x) : f(x); ?P7(?c3(x)) ] ==> False}


1347 
{\out 2. !!x. [ ~ ?c3(x) : \{x. ?P7(x)\}; ~ ?c3(x) : f(x) ] ==> False}


1348 
\end{ttbox}


1349 
Forcing a contradiction between the two assumptions of subgoal~1 completes


1350 
the instantiation of~$S$. It is now $\{x. x\not\in f(x)\}$, the standard


1351 
diagonal construction.


1352 
\begin{ttbox}


1353 
by (contr_tac 1);


1354 
{\out Level 5}


1355 
{\out ~ \{x. ~ x : f(x)\} : range(f)}


1356 
{\out 1. !!x. [ ~ x : \{x. ~ x : f(x)\}; ~ x : f(x) ] ==> False}


1357 
\end{ttbox}


1358 
The rest should be easy. To apply \ttindex{CollectI} to the negated


1359 
assumption, we employ \ttindex{swap_res_tac}:


1360 
\begin{ttbox}


1361 
by (swap_res_tac [CollectI] 1);


1362 
{\out Level 6}


1363 
{\out ~ \{x. ~ x : f(x)\} : range(f)}


1364 
{\out 1. !!x. [ ~ x : f(x); ~ False ] ==> ~ x : f(x)}


1365 
by (assume_tac 1);


1366 
{\out Level 7}


1367 
{\out ~ \{x. ~ x : f(x)\} : range(f)}


1368 
{\out No subgoals!}


1369 
\end{ttbox}


1370 
How much creativity is required? As it happens, Isabelle can prove this


1371 
theorem automatically. The classical set \ttindex{set_cs} contains rules


1372 
for most of the constructs of {\HOL}'s set theory. We augment it with


1373 
\ttindex{equalityCE}  set equalities are not broken up by default 


1374 
and apply bestfirst search. Depthfirst search would diverge, but


1375 
bestfirst search successfully navigates through the large search space.


1376 
\begin{ttbox}


1377 
choplev 0;


1378 
{\out Level 0}


1379 
{\out ~ ?S : range(f)}


1380 
{\out 1. ~ ?S : range(f)}


1381 
by (best_tac (set_cs addSEs [equalityCE]) 1);


1382 
{\out Level 1}


1383 
{\out ~ \{x. ~ x : f(x)\} : range(f)}


1384 
{\out No subgoals!}


1385 
\end{ttbox}
