6580

1 
%% $Id$


2 
\chapter{HigherOrder Logic}


3 
\index{higherorder logic(}


4 
\index{HOL system@{\sc hol} system}


5 


6 
The theory~\thydx{HOL} implements higherorder logic. It is based on


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


8 
Church's original paper~\cite{church40}. Andrews's


9 
book~\cite{andrews86} is a full description of the original


10 
Churchstyle higherorder logic. Experience with the {\sc hol} system


11 
has demonstrated that higherorder logic is widely applicable in many


12 
areas of mathematics and computer science, not just hardware


13 
verification, {\sc hol}'s original \textit{raison d'\^etre\/}. It is


14 
weaker than {\ZF} set theory but for most applications this does not


15 
matter. If you prefer {\ML} to Lisp, you will probably prefer \HOL\


16 
to~{\ZF}.


17 


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


19 
different syntax. Ancient releases of Isabelle included still another version


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


21 
version no longer exists, but \thydx{ZF} supports a similar style of


22 
reasoning.} follows $\lambda$calculus and functional programming. Function


23 
application is curried. To apply the function~$f$ of type


24 
$\tau@1\To\tau@2\To\tau@3$ to the arguments~$a$ and~$b$ in \HOL, you simply


25 
write $f\,a\,b$. There is no `apply' operator as in \thydx{ZF}. Note that


26 
$f(a,b)$ means ``$f$ applied to the pair $(a,b)$'' in \HOL. We write ordered


27 
pairs as $(a,b)$, not $\langle a,b\rangle$ as in {\ZF}.


28 


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


30 
identifies objectlevel types with metalevel types, taking advantage of


31 
Isabelle's builtin typechecker. It identifies objectlevel functions


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


33 
and application.


34 


35 
These identifications allow Isabelle to support \HOL\ particularly


36 
nicely, but they also mean that \HOL\ requires more sophistication


37 
from the user  in particular, an understanding of Isabelle's type


38 
system. Beginners should work with \texttt{show_types} (or even


39 
\texttt{show_sorts}) set to \texttt{true}.


40 
% Gain experience by


41 
%working in firstorder logic before attempting to use higherorder logic.


42 
%This chapter assumes familiarity with~{\FOL{}}.


43 


44 


45 
\begin{figure}


46 
\begin{constants}


47 
\it name &\it metatype & \it description \\


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


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


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


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


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


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


54 
\end{constants}


55 
\subcaption{Constants}


56 


57 
\begin{constants}


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


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


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


61 
\it symbol &\it name &\it metatype & \it description \\


62 
\tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha$ &


63 
Hilbert description ($\varepsilon$) \\


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


65 
universal quantifier ($\forall$) \\


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


67 
existential quantifier ($\exists$) \\


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


69 
unique existence ($\exists!$)\\


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


71 
least element


72 
\end{constants}


73 
\subcaption{Binders}


74 


75 
\begin{constants}


76 
\index{*"= symbol}


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


78 
\index{*" symbol}


79 
\index{*"""> symbol}


80 
\it symbol & \it metatype & \it priority & \it description \\


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


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


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


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


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


86 
less than or equals ($\leq$)\\


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


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


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


90 
\end{constants}


91 
\subcaption{Infixes}


92 
\caption{Syntax of \texttt{HOL}} \label{holconstants}


93 
\end{figure}


94 


95 


96 
\begin{figure}


97 
\index{*let symbol}


98 
\index{*in symbol}


99 
\dquotes


100 
\[\begin{array}{rclcl}


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


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


103 
&  &


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


105 
&  &


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


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


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


109 
&  & term " = " term \\


110 
&  & term " \ttilde= " term \\


111 
&  & term " < " term \\


112 
&  & term " <= " term \\


113 
&  & "\ttilde\ " formula \\


114 
&  & formula " \& " formula \\


115 
&  & formula "  " formula \\


116 
&  & formula " > " formula \\


117 
&  & "!~~~" id~id^* " . " formula


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


119 
&  & "?~~~" id~id^* " . " formula


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


121 
&  & "?!~~" id~id^* " . " formula


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


123 
\end{array}


124 
\]


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


126 
\end{figure}


127 


128 


129 
\section{Syntax}


130 


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


132 
binders), while Fig.\ts\ref{holgrammar} presents the grammar of


133 
higherorder logic. Note that $a$\verb~=$b$ is translated to


134 
$\neg(a=b)$.


135 


136 
\begin{warn}


137 
\HOL\ has no ifandonlyif connective; logical equivalence is expressed


138 
using equality. But equality has a high priority, as befitting a


139 
relation, while ifandonlyif typically has the lowest priority. Thus,


140 
$\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$.


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


142 
parentheses.


143 
\end{warn}


144 


145 
\subsection{Types and classes}


146 
The universal type class of higherorder terms is called~\cldx{term}.


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


148 
particular the equality symbol and quantifiers are polymorphic over


149 
class \texttt{term}.


150 


151 
The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus,


152 
formulae are terms. The builtin type~\tydx{fun}, which constructs


153 
function types, is overloaded with arity {\tt(term,\thinspace


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


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


156 
functions.


157 


158 
\HOL\ offers various methods for introducing new types.


159 
See~\S\ref{sec:HOL:Types} and~\S\ref{sec:HOL:datatype}.


160 


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


162 
signatures; the relations $<$ and $\leq$ are polymorphic over this


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


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


165 
\cldx{order} of \cldx{ord} which axiomatizes partially ordered types


166 
(w.r.t.\ $\le$).


167 


168 
Three other syntactic type classes  \cldx{plus}, \cldx{minus} and


169 
\cldx{times}  permit overloading of the operators {\tt+},\index{*"+


170 
symbol} {\tt}\index{*" symbol} and {\tt*}.\index{*"* symbol} In


171 
particular, {\tt} is instantiated for set difference and subtraction


172 
on natural numbers.


173 


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


175 
type constraints. Type inference may otherwise make the goal more


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


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


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


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


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


181 
type $nat$.


182 


183 
\begin{warn}


184 
If resolution fails for no obvious reason, try setting


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


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


187 
well, causing Isabelle to display type classes and sorts.


188 


189 
\index{unification!incompleteness of}


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


191 
guarantee to find instantiations for type variables automatically. Be


192 
prepared to use \ttindex{res_inst_tac} instead of \texttt{resolve_tac},


193 
possibly instantiating type variables. Setting


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


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


196 
\end{warn}


197 


198 


199 
\subsection{Binders}


200 


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


202 
some~$x$ satisfying~$P$, if such exists. Since all terms in \HOL\


203 
denote something, a description is always meaningful, but we do not


204 
know its value unless $P$ defines it uniquely. We may write


205 
descriptions as \cdx{Eps}($\lambda x. P[x]$) or use the syntax


206 
\hbox{\tt \at $x$.\ $P[x]$}.


207 


208 
Existential quantification is defined by


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


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


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


212 
quantifications. For instance, $\exists!x\,y. P\,x\,y$ abbreviates


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


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


215 


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


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


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


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


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


221 
notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also


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


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


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


225 
to \texttt{false}, then~\texttt{ALL} and~\texttt{EX} are displayed.


226 


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


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


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


230 
Fig.~\ref{holdefs}). The definition uses Hilbert's $\varepsilon$


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


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


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


234 
$\le$ need not be a wellordering, not even an order at all!}


235 


236 
\medskip All these binders have priority 10.


237 


238 
\begin{warn}


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


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


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


242 
\end{warn}


243 


244 

6620

245 
\subsection{The let and case constructions}

6580

246 
Local abbreviations can be introduced by a \texttt{let} construct whose


247 
syntax appears in Fig.\ts\ref{holgrammar}. Internally it is translated into


248 
the constant~\cdx{Let}. It can be expanded by rewriting with its


249 
definition, \tdx{Let_def}.


250 


251 
\HOL\ also defines the basic syntax


252 
\[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"" \dots ""~c@n~"=>"~e@n\]


253 
as a uniform means of expressing \texttt{case} constructs. Therefore \texttt{case}


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


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


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


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


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


259 


260 
\begin{warn}


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


262 
quantifiers, which requires additional enclosing parentheses in the context


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


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


265 
else\dots})$.


266 
\end{warn}


267 


268 
\section{Rules of inference}


269 


270 
\begin{figure}


271 
\begin{ttbox}\makeatother


272 
\tdx{refl} t = (t::'a)


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


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


275 
\tdx{impI} (P ==> Q) ==> P>Q


276 
\tdx{mp} [ P>Q; P ] ==> Q


277 
\tdx{iff} (P>Q) > (Q>P) > (P=Q)


278 
\tdx{selectI} P(x::'a) ==> P(@x. P x)


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


280 
\end{ttbox}


281 
\caption{The \texttt{HOL} rules} \label{holrules}


282 
\end{figure}


283 


284 
Figure~\ref{holrules} shows the primitive inference rules of~\HOL{},


285 
with their~{\ML} names. Some of the rules deserve additional


286 
comments:


287 
\begin{ttdescription}


288 
\item[\tdx{ext}] expresses extensionality of functions.


289 
\item[\tdx{iff}] asserts that logically equivalent formulae are


290 
equal.


291 
\item[\tdx{selectI}] gives the defining property of the Hilbert


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


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


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


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


296 
shown by Diaconescu; see Paulson~\cite{paulsonCOLOG} for details.}


297 
\end{ttdescription}


298 


299 


300 
\begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message


301 
\begin{ttbox}\makeatother


302 
\tdx{True_def} True == ((\%x::bool. x)=(\%x. x))


303 
\tdx{All_def} All == (\%P. P = (\%x. True))


304 
\tdx{Ex_def} Ex == (\%P. P(@x. P x))


305 
\tdx{False_def} False == (!P. P)


306 
\tdx{not_def} not == (\%P. P>False)


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


308 
\tdx{or_def} op  == (\%P Q. !R. (P>R) > (Q>R) > R)


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


310 


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


312 
\tdx{if_def} If P x y ==


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


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


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


316 
\end{ttbox}


317 
\caption{The \texttt{HOL} definitions} \label{holdefs}


318 
\end{figure}


319 


320 


321 
\HOL{} follows standard practice in higherorder logic: only a few


322 
connectives are taken as primitive, with the remainder defined obscurely


323 
(Fig.\ts\ref{holdefs}). Gordon's {\sc hol} system expresses the


324 
corresponding definitions \cite[page~270]{mgordonhol} using


325 
objectequality~({\tt=}), which is possible because equality in


326 
higherorder logic may equate formulae and even functions over formulae.


327 
But theory~\HOL{}, like all other Isabelle theories, uses


328 
metaequality~({\tt==}) for definitions.


329 
\begin{warn}


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


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


332 
or, better still, using highlevel tactics


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


334 
\end{warn}


335 


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


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


338 
type variables explicitly by calling \texttt{res_inst_tac}.


339 


340 


341 
\begin{figure}


342 
\begin{ttbox}


343 
\tdx{sym} s=t ==> t=s


344 
\tdx{trans} [ r=s; s=t ] ==> r=t


345 
\tdx{ssubst} [ t=s; P s ] ==> P t


346 
\tdx{box_equals} [ a=b; a=c; b=d ] ==> c=d


347 
\tdx{arg_cong} x = y ==> f x = f y


348 
\tdx{fun_cong} f = g ==> f x = g x


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


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


351 
\subcaption{Equality}


352 


353 
\tdx{TrueI} True


354 
\tdx{FalseE} False ==> P


355 


356 
\tdx{conjI} [ P; Q ] ==> P&Q


357 
\tdx{conjunct1} [ P&Q ] ==> P


358 
\tdx{conjunct2} [ P&Q ] ==> Q


359 
\tdx{conjE} [ P&Q; [ P; Q ] ==> R ] ==> R


360 


361 
\tdx{disjI1} P ==> PQ


362 
\tdx{disjI2} Q ==> PQ


363 
\tdx{disjE} [ P  Q; P ==> R; Q ==> R ] ==> R


364 


365 
\tdx{notI} (P ==> False) ==> ~ P


366 
\tdx{notE} [ ~ P; P ] ==> R


367 
\tdx{impE} [ P>Q; P; Q ==> R ] ==> R


368 
\subcaption{Propositional logic}


369 


370 
\tdx{iffI} [ P ==> Q; Q ==> P ] ==> P=Q


371 
\tdx{iffD1} [ P=Q; P ] ==> Q


372 
\tdx{iffD2} [ P=Q; Q ] ==> P


373 
\tdx{iffE} [ P=Q; [ P > Q; Q > P ] ==> R ] ==> R


374 
%


375 
%\tdx{eqTrueI} P ==> P=True


376 
%\tdx{eqTrueE} P=True ==> P


377 
\subcaption{Logical equivalence}


378 


379 
\end{ttbox}


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


381 
\end{figure}


382 


383 


384 
\begin{figure}


385 
\begin{ttbox}\makeatother


386 
\tdx{allI} (!!x. P x) ==> !x. P x


387 
\tdx{spec} !x. P x ==> P x


388 
\tdx{allE} [ !x. P x; P x ==> R ] ==> R


389 
\tdx{all_dupE} [ !x. P x; [ P x; !x. P x ] ==> R ] ==> R


390 


391 
\tdx{exI} P x ==> ? x. P x


392 
\tdx{exE} [ ? x. P x; !!x. P x ==> Q ] ==> Q


393 


394 
\tdx{ex1I} [ P a; !!x. P x ==> x=a ] ==> ?! x. P x


395 
\tdx{ex1E} [ ?! x. P x; !!x. [ P x; ! y. P y > y=x ] ==> R


396 
] ==> R


397 


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


399 
\subcaption{Quantifiers and descriptions}


400 


401 
\tdx{ccontr} (~P ==> False) ==> P


402 
\tdx{classical} (~P ==> P) ==> P


403 
\tdx{excluded_middle} ~P  P


404 


405 
\tdx{disjCI} (~Q ==> P) ==> PQ


406 
\tdx{exCI} (! x. ~ P x ==> P a) ==> ? x. P x


407 
\tdx{impCE} [ P>Q; ~ P ==> R; Q ==> R ] ==> R


408 
\tdx{iffCE} [ P=Q; [ P;Q ] ==> R; [ ~P; ~Q ] ==> R ] ==> R


409 
\tdx{notnotD} ~~P ==> P


410 
\tdx{swap} ~P ==> (~Q ==> P) ==> Q


411 
\subcaption{Classical logic}


412 


413 
%\tdx{if_True} (if True then x else y) = x


414 
%\tdx{if_False} (if False then x else y) = y


415 
\tdx{if_P} P ==> (if P then x else y) = x


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


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


418 
\subcaption{Conditionals}


419 
\end{ttbox}


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


421 
\end{figure}


422 


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


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


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


426 
conjunctions, implications, and universal quantifiers.


427 


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


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


430 
simplifying both sides of an equation.


431 


432 
The following simple tactics are occasionally useful:


433 
\begin{ttdescription}


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


435 
repeatedly to remove all outermost universal quantifiers and implications


436 
from subgoal $i$.


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


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


439 
with the added assumptions $P$ and $\neg P$, respectively.


440 
\end{ttdescription}


441 


442 


443 
\begin{figure}


444 
\begin{center}


445 
\begin{tabular}{rrr}


446 
\it name &\it metatype & \it description \\


447 
\index{{}@\verb'{}' symbol}


448 
\verb{} & $\alpha\,set$ & the empty set \\


449 
\cdx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$


450 
& insertion of element \\


451 
\cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$


452 
& comprehension \\


453 
\cdx{Compl} & $\alpha\,set\To\alpha\,set$


454 
& complement \\


455 
\cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$


456 
& intersection over a set\\


457 
\cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$


458 
& union over a set\\


459 
\cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$


460 
&set of sets intersection \\


461 
\cdx{Union} & $(\alpha\,set)set\To\alpha\,set$


462 
&set of sets union \\


463 
\cdx{Pow} & $\alpha\,set \To (\alpha\,set)set$


464 
& powerset \\[1ex]


465 
\cdx{range} & $(\alpha\To\beta )\To\beta\,set$


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


467 
\cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$


468 
& bounded quantifiers


469 
\end{tabular}


470 
\end{center}


471 
\subcaption{Constants}


472 


473 
\begin{center}


474 
\begin{tabular}{llrrr}


475 
\it symbol &\it name &\it metatype & \it priority & \it description \\


476 
\sdx{INT} & \cdx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &


477 
intersection over a type\\


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


479 
union over a type


480 
\end{tabular}


481 
\end{center}


482 
\subcaption{Binders}


483 


484 
\begin{center}


485 
\index{*"`"` symbol}


486 
\index{*": symbol}


487 
\index{*"<"= symbol}


488 
\begin{tabular}{rrrr}


489 
\it symbol & \it metatype & \it priority & \it description \\


490 
\tt `` & $[\alpha\To\beta ,\alpha\,set]\To \beta\,set$


491 
& Left 90 & image \\


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


493 
& Left 70 & intersection ($\int$) \\


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


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


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


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


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


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


500 
\end{tabular}


501 
\end{center}


502 
\subcaption{Infixes}


503 
\caption{Syntax of the theory \texttt{Set}} \label{holsetsyntax}


504 
\end{figure}


505 


506 


507 
\begin{figure}


508 
\begin{center} \tt\frenchspacing


509 
\index{*"! symbol}


510 
\begin{tabular}{rrr}


511 
\it external & \it internal & \it description \\


512 
$a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm nonmembership\\


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


514 
{\ttlbrace}$x$. $P[x]${\ttrbrace} & Collect($\lambda x. P[x]$) &


515 
\rm comprehension \\


516 
\sdx{INT} $x$:$A$. $B[x]$ & INTER $A$ $\lambda x. B[x]$ &


517 
\rm intersection \\


518 
\sdx{UN}{\tt\ } $x$:$A$. $B[x]$ & UNION $A$ $\lambda x. B[x]$ &


519 
\rm union \\


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


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


522 
\rm bounded $\forall$ \\


523 
\sdx{?} $x$:$A$. $P[x]$ or \sdx{EX}{\tt\ } $x$:$A$. $P[x]$ &


524 
Bex $A$ $\lambda x. P[x]$ & \rm bounded $\exists$


525 
\end{tabular}


526 
\end{center}


527 
\subcaption{Translations}


528 


529 
\dquotes


530 
\[\begin{array}{rclcl}


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


532 
&  & "{\ttlbrace}{\ttrbrace}" \\


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


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


535 
&  & term " `` " term \\


536 
&  & term " Int " term \\


537 
&  & term " Un " term \\


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


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


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


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


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


543 
&  & term " : " term \\


544 
&  & term " \ttilde: " term \\


545 
&  & term " <= " term \\


546 
&  & "!~" id ":" term " . " formula


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


548 
&  & "?~" id ":" term " . " formula


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


550 
\end{array}


551 
\]


552 
\subcaption{Full Grammar}


553 
\caption{Syntax of the theory \texttt{Set} (continued)} \label{holsetsyntax2}


554 
\end{figure}


555 


556 


557 
\section{A formulation of set theory}


558 
Historically, higherorder logic gives a foundation for Russell and


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


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


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


562 
\begin{itemize}


563 
\item


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


565 
define universes for sets, but typechecking is still significant.


566 
\item


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


568 
may be defined by absolute comprehension.


569 
\item


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


571 
have a more complex type.


572 
\end{itemize}


573 
Finite unions and intersections have the same behaviour in \HOL\ as they


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


575 
denoting the universal set for the given type.


576 


577 
\subsection{Syntax of set theory}\index{*set type}


578 
\HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is


579 
essentially the same as $\alpha\To bool$. The new type is defined for


580 
clarity and to avoid complications involving function types in unification.


581 
The isomorphisms between the two types are declared explicitly. They are


582 
very natural: \texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while


583 
\hbox{\tt op :} maps in the other direction (ignoring argument order).


584 


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


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


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


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


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


590 
$\neg(a\in b)$.


591 


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


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


594 
\begin{eqnarray*}


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


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


597 
\end{eqnarray*}


598 


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


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


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


602 
x. P[x])$. It defines sets by absolute comprehension, which is impossible


603 
in~{\ZF}; the type of~$x$ implicitly restricts the comprehension.


604 


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


606 
\begin{eqnarray*}


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


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


609 
\end{eqnarray*}


610 
The constants~\cdx{Ball} and~\cdx{Bex} are defined


611 
accordingly. Instead of \texttt{Ball $A$ $P$} and \texttt{Bex $A$ $P$} we may


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


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


614 
%


615 
\hbox{\tt !~$x$:$A$.\ $P[x]$} and \hbox{\tt ?~$x$:$A$.\ $P[x]$}. Isabelle's


616 
usual quantifier symbols, \sdx{ALL} and \sdx{EX}, are also accepted


617 
for input. As with the primitive quantifiers, the {\ML} reference


618 
\ttindex{HOL_quantifiers} specifies which notation to use for output.


619 


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


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


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


623 
\sdx{INT}~\hbox{\tt$x$:$A$.\ $B[x]$}.


624 


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


626 
B[x]$, are written \sdx{UN}~\hbox{\tt$x$.\ $B[x]$} and


627 
\sdx{INT}~\hbox{\tt$x$.\ $B[x]$}. They are equivalent to the previous


628 
union and intersection operators when $A$ is the universal set.


629 


630 
The operators $\bigcup A$ and $\bigcap A$ act upon sets of sets. They are


631 
not binders, but are equal to $\bigcup@{x\in A}x$ and $\bigcap@{x\in A}x$,


632 
respectively.


633 


634 


635 


636 
\begin{figure} \underscoreon


637 
\begin{ttbox}


638 
\tdx{mem_Collect_eq} (a : {\ttlbrace}x. P x{\ttrbrace}) = P a


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


640 


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


642 
\tdx{insert_def} insert a B == {\ttlbrace}x. x=a{\ttrbrace} Un B


643 
\tdx{Ball_def} Ball A P == ! x. x:A > P x


644 
\tdx{Bex_def} Bex A P == ? x. x:A & P x


645 
\tdx{subset_def} A <= B == ! x:A. x:B


646 
\tdx{Un_def} A Un B == {\ttlbrace}x. x:A  x:B{\ttrbrace}


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


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


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


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


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


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


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


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


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


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


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


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


659 
\end{ttbox}


660 
\caption{Rules of the theory \texttt{Set}} \label{holsetrules}


661 
\end{figure}


662 


663 


664 
\begin{figure} \underscoreon


665 
\begin{ttbox}


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


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


668 
\tdx{CollectE} [ a : {\ttlbrace}x. P x{\ttrbrace}; P a ==> W ] ==> W


669 


670 
\tdx{ballI} [ !!x. x:A ==> P x ] ==> ! x:A. P x


671 
\tdx{bspec} [ ! x:A. P x; x:A ] ==> P x


672 
\tdx{ballE} [ ! x:A. P x; P x ==> Q; ~ x:A ==> Q ] ==> Q


673 


674 
\tdx{bexI} [ P x; x:A ] ==> ? x:A. P x


675 
\tdx{bexCI} [ ! x:A. ~ P x ==> P a; a:A ] ==> ? x:A. P x


676 
\tdx{bexE} [ ? x:A. P x; !!x. [ x:A; P x ] ==> Q ] ==> Q


677 
\subcaption{Comprehension and Bounded quantifiers}


678 


679 
\tdx{subsetI} (!!x. x:A ==> x:B) ==> A <= B


680 
\tdx{subsetD} [ A <= B; c:A ] ==> c:B


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


682 


683 
\tdx{subset_refl} A <= A


684 
\tdx{subset_trans} [ A<=B; B<=C ] ==> A<=C


685 


686 
\tdx{equalityI} [ A <= B; B <= A ] ==> A = B


687 
\tdx{equalityD1} A = B ==> A<=B


688 
\tdx{equalityD2} A = B ==> B<=A


689 
\tdx{equalityE} [ A = B; [ A<=B; B<=A ] ==> P ] ==> P


690 


691 
\tdx{equalityCE} [ A = B; [ c:A; c:B ] ==> P;


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


693 
] ==> P


694 
\subcaption{The subset and equality relations}


695 
\end{ttbox}


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


697 
\end{figure}


698 


699 


700 
\begin{figure} \underscoreon


701 
\begin{ttbox}


702 
\tdx{emptyE} a : {\ttlbrace}{\ttrbrace} ==> P


703 


704 
\tdx{insertI1} a : insert a B


705 
\tdx{insertI2} a : B ==> a : insert b B


706 
\tdx{insertE} [ a : insert b A; a=b ==> P; a:A ==> P ] ==> P


707 


708 
\tdx{ComplI} [ c:A ==> False ] ==> c : Compl A


709 
\tdx{ComplD} [ c : Compl A ] ==> ~ c:A


710 


711 
\tdx{UnI1} c:A ==> c : A Un B


712 
\tdx{UnI2} c:B ==> c : A Un B


713 
\tdx{UnCI} (~c:B ==> c:A) ==> c : A Un B


714 
\tdx{UnE} [ c : A Un B; c:A ==> P; c:B ==> P ] ==> P


715 


716 
\tdx{IntI} [ c:A; c:B ] ==> c : A Int B


717 
\tdx{IntD1} c : A Int B ==> c:A


718 
\tdx{IntD2} c : A Int B ==> c:B


719 
\tdx{IntE} [ c : A Int B; [ c:A; c:B ] ==> P ] ==> P


720 


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


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


723 


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


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


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


727 


728 
\tdx{UnionI} [ X:C; A:X ] ==> A : Union C


729 
\tdx{UnionE} [ A : Union C; !!X.[ A:X; X:C ] ==> R ] ==> R


730 


731 
\tdx{InterI} [ !!X. X:C ==> A:X ] ==> A : Inter C


732 
\tdx{InterD} [ A : Inter C; X:C ] ==> A:X


733 
\tdx{InterE} [ A : Inter C; A:X ==> R; ~ X:C ==> R ] ==> R


734 


735 
\tdx{PowI} A<=B ==> A: Pow B


736 
\tdx{PowD} A: Pow B ==> A<=B


737 


738 
\tdx{imageI} [ x:A ] ==> f x : f``A


739 
\tdx{imageE} [ b : f``A; !!x.[ b=f x; x:A ] ==> P ] ==> P


740 


741 
\tdx{rangeI} f x : range f


742 
\tdx{rangeE} [ b : range f; !!x.[ b=f x ] ==> P ] ==> P


743 
\end{ttbox}


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


745 
\end{figure}


746 


747 


748 
\subsection{Axioms and rules of set theory}


749 
Figure~\ref{holsetrules} presents the rules of theory \thydx{Set}. The


750 
axioms \tdx{mem_Collect_eq} and \tdx{Collect_mem_eq} assert


751 
that the functions \texttt{Collect} and \hbox{\tt op :} are isomorphisms. Of


752 
course, \hbox{\tt op :} also serves as the membership relation.


753 


754 
All the other axioms are definitions. They include the empty set, bounded


755 
quantifiers, unions, intersections, complements and the subset relation.


756 
They also include straightforward constructions on functions: image~({\tt``})


757 
and \texttt{range}.


758 


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


760 
%The statement ${\tt inj_on}~f~A$ asserts that $f$ is injective on the


761 
%set~$A$, which specifies a subset of its domain type. In a type


762 
%definition, $f$ is the abstraction function and $A$ is the set of valid


763 
%representations; we should not expect $f$ to be injective outside of~$A$.


764 


765 
%\begin{figure} \underscoreon


766 
%\begin{ttbox}


767 
%\tdx{Inv_f_f} inj f ==> Inv f (f x) = x


768 
%\tdx{f_Inv_f} y : range f ==> f(Inv f y) = y


769 
%


770 
%\tdx{Inv_injective}


771 
% [ Inv f x=Inv f y; x: range f; y: range f ] ==> x=y


772 
%


773 
%


774 
%\tdx{monoI} [ !!A B. A <= B ==> f A <= f B ] ==> mono f


775 
%\tdx{monoD} [ mono f; A <= B ] ==> f A <= f B


776 
%


777 
%\tdx{injI} [ !! x y. f x = f y ==> x=y ] ==> inj f


778 
%\tdx{inj_inverseI} (!!x. g(f x) = x) ==> inj f


779 
%\tdx{injD} [ inj f; f x = f y ] ==> x=y


780 
%


781 
%\tdx{inj_onI} (!!x y. [ f x=f y; x:A; y:A ] ==> x=y) ==> inj_on f A


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


783 
%


784 
%\tdx{inj_on_inverseI}


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


786 
%\tdx{inj_on_contraD}


787 
% [ inj_on f A; x~=y; x:A; y:A ] ==> ~ f x=f y


788 
%\end{ttbox}


789 
%\caption{Derived rules involving functions} \label{holfun}


790 
%\end{figure}


791 


792 


793 
\begin{figure} \underscoreon


794 
\begin{ttbox}


795 
\tdx{Union_upper} B:A ==> B <= Union A


796 
\tdx{Union_least} [ !!X. X:A ==> X<=C ] ==> Union A <= C


797 


798 
\tdx{Inter_lower} B:A ==> Inter A <= B


799 
\tdx{Inter_greatest} [ !!X. X:A ==> C<=X ] ==> C <= Inter A


800 


801 
\tdx{Un_upper1} A <= A Un B


802 
\tdx{Un_upper2} B <= A Un B


803 
\tdx{Un_least} [ A<=C; B<=C ] ==> A Un B <= C


804 


805 
\tdx{Int_lower1} A Int B <= A


806 
\tdx{Int_lower2} A Int B <= B


807 
\tdx{Int_greatest} [ C<=A; C<=B ] ==> C <= A Int B


808 
\end{ttbox}


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


810 
\end{figure}


811 


812 


813 
\begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message


814 
\begin{ttbox}


815 
\tdx{Int_absorb} A Int A = A


816 
\tdx{Int_commute} A Int B = B Int A


817 
\tdx{Int_assoc} (A Int B) Int C = A Int (B Int C)


818 
\tdx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)


819 


820 
\tdx{Un_absorb} A Un A = A


821 
\tdx{Un_commute} A Un B = B Un A


822 
\tdx{Un_assoc} (A Un B) Un C = A Un (B Un C)


823 
\tdx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)


824 


825 
\tdx{Compl_disjoint} A Int (Compl A) = {\ttlbrace}x. False{\ttrbrace}


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


827 
\tdx{double_complement} Compl(Compl A) = A


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


829 
\tdx{Compl_Int} Compl(A Int B) = (Compl A) Un (Compl B)


830 


831 
\tdx{Union_Un_distrib} Union(A Un B) = (Union A) Un (Union B)


832 
\tdx{Int_Union} A Int (Union B) = (UN C:B. A Int C)


833 
\tdx{Un_Union_image} (UN x:C.(A x) Un (B x)) = Union(A``C) Un Union(B``C)


834 


835 
\tdx{Inter_Un_distrib} Inter(A Un B) = (Inter A) Int (Inter B)


836 
\tdx{Un_Inter} A Un (Inter B) = (INT C:B. A Un C)


837 
\tdx{Int_Inter_image} (INT x:C.(A x) Int (B x)) = Inter(A``C) Int Inter(B``C)


838 
\end{ttbox}


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


840 
\end{figure}


841 


842 


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


844 
obvious and resemble rules of Isabelle's {\ZF} set theory. Certain rules,


845 
such as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI},


846 
are designed for classical reasoning; the rules \tdx{subsetD},


847 
\tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are not


848 
strictly necessary but yield more natural proofs. Similarly,


849 
\tdx{equalityCE} supports classical reasoning about extensionality,


850 
after the fashion of \tdx{iffCE}. See the file \texttt{HOL/Set.ML} for


851 
proofs pertaining to set theory.


852 


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


854 
Unions form least upper bounds; nonempty intersections form greatest lower


855 
bounds. Reasoning directly about subsets often yields clearer proofs than


856 
reasoning about the membership relation. See the file \texttt{HOL/subset.ML}.


857 


858 
Figure~\ref{holequalities} presents many common set equalities. They


859 
include commutative, associative and distributive laws involving unions,


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


861 
HOL/equalities.ML}.


862 


863 
\begin{warn}


864 
\texttt{Blast_tac} proves many settheoretic theorems automatically.


865 
Hence you seldom need to refer to the theorems above.


866 
\end{warn}


867 


868 
\begin{figure}


869 
\begin{center}


870 
\begin{tabular}{rrr}


871 
\it name &\it metatype & \it description \\


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


873 
& injective/surjective \\


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


875 
& injective over subset\\


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


877 
\end{tabular}


878 
\end{center}


879 


880 
\underscoreon


881 
\begin{ttbox}


882 
\tdx{inj_def} inj f == ! x y. f x=f y > x=y


883 
\tdx{surj_def} surj f == ! y. ? x. y=f x


884 
\tdx{inj_on_def} inj_on f A == !x:A. !y:A. f x=f y > x=y


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


886 
\end{ttbox}


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


888 
\end{figure}


889 


890 
\subsection{Properties of functions}\nopagebreak


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


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


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


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


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


896 


897 
There is also a large collection of monotonicity theorems for constructions


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


899 


900 
\section{Generic packages}


901 
\label{sec:HOL:genericpackages}


902 


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


904 
simplifier and the classical reasoner.


905 


906 
\subsection{Simplification and substitution}


907 


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


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


910 
simplification set for higherorder logic is~\ttindexbold{HOL_ss};


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


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


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


914 
simplification rules.


915 


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


917 
{Chaps.\ts\ref{substitution} and~\ref{simpchap}} for details of substitution


918 
and simplification.


919 


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


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


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


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


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


925 
\end{warn}


926 


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


928 
of nontermination or because its lefthand side is too flexible 


929 
then you might try \texttt{stac}:


930 
\begin{ttdescription}


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


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


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


934 
may be necessary to select the desired ones.


935 


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


937 
additional (first) subgoal.


938 
\end{ttdescription}


939 


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


941 
for an equality throughout a subgoal and its hypotheses. This tactic uses


942 
\HOL's general substitution rule.


943 


944 
\subsubsection{Case splitting}


945 
\label{subsec:HOL:case:splitting}


946 


947 
\HOL{} also provides convenient means for case splitting during


948 
rewriting. Goals containing a subterm of the form \texttt{if}~$b$~{\tt


949 
then\dots else\dots} often require a case distinction on $b$. This is


950 
expressed by the theorem \tdx{split_if}:


951 
$$


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


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


954 
\eqno{(*)}


955 
$$


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


957 
\[


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


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


960 
\]


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


962 
lefthand side is not a higherorder pattern in the sense of


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


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


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


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


967 
simpset, as in


968 
\begin{ttbox}


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


970 
\end{ttbox}


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


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


973 
\texttt{if} have been eliminated.


974 


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


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


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


978 
the inverse of \texttt{addsplits}:


979 
\begin{ttbox}


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


981 
\end{ttbox}


982 


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


984 
\[


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


986 
\]


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


988 
right form because internally the lefthand side is


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


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


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


992 


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


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


995 
\begin{ttbox}


996 
\ttindexbold{Addsplits}: thm list > unit


997 
\ttindexbold{Delsplits}: thm list > unit


998 
\end{ttbox}


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


1000 


1001 
\subsection{Classical reasoning}


1002 


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


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


1005 
rule; recall Fig.\ts\ref{hollemmas2} above.


1006 


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


1008 
Best_tac} refer to the default claset (\texttt{claset()}), which works for most


1009 
purposes. Named clasets include \ttindexbold{prop_cs}, which includes the


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


1011 
rules. See the file \texttt{HOL/cladata.ML} for lists of the classical rules,


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


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


1014 


1015 


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


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


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


1019 
introducing new types in general. The most important type


1020 
construction, the \texttt{datatype}, is treated separately in


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


1022 


1023 


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


1025 
\label{subsec:prodsum}


1026 


1027 
\begin{figure}[htbp]


1028 
\begin{constants}


1029 
\it symbol & \it metatype & & \it description \\


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


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


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


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


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


1035 
& & generalized projection\\


1036 
\cdx{Sigma} &


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


1038 
& general sum of sets


1039 
\end{constants}


1040 
\begin{ttbox}\makeatletter


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


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


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


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


1045 


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


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


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


1049 


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


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


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


1053 


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


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


1056 


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


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


1059 
\end{ttbox}


1060 
\caption{Type $\alpha\times\beta$}\label{holprod}


1061 
\end{figure}


1062 


1063 
Theory \thydx{Prod} (Fig.\ts\ref{holprod}) defines the product type


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


1065 
tuples are simulated by pairs nested to the right:


1066 
\begin{center}


1067 
\begin{tabular}{cc}


1068 
external & internal \\


1069 
\hline


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


1071 
\hline


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


1073 
\end{tabular}


1074 
\end{center}


1075 
In addition, it is possible to use tuples


1076 
as patterns in abstractions:


1077 
\begin{center}


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


1079 
\end{center}


1080 
Nested patterns are also supported. They are translated stepwise:


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


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


1083 
$z$.\ $t$))}. The reverse translation is performed upon printing.


1084 
\begin{warn}


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


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


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


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


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


1090 
\end{warn}


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


1092 
variable binding construct which is internally described by a


1093 
$\lambda$abstraction. Some important examples are


1094 
\begin{description}


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


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


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


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


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


1100 
\end{description}


1101 


1102 
There is a simple tactic which supports reasoning about patterns:


1103 
\begin{ttdescription}


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


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


1106 
each component. A simple example:


1107 
\begin{ttbox}


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


1109 
by(split_all_tac 1);


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


1111 
\end{ttbox}


1112 
\end{ttdescription}


1113 


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


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


1116 
\begin{ttbox}


1117 
\tdx{unit_eq} u = ()


1118 
\end{ttbox}


1119 
\bigskip


1120 


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


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


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


1124 


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


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


1127 
respective theory files.


1128 


1129 
\begin{figure}


1130 
\begin{constants}


1131 
\it symbol & \it metatype & & \it description \\


1132 
\cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\


1133 
\cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\


1134 
\cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$


1135 
& & conditional


1136 
\end{constants}


1137 
\begin{ttbox}\makeatletter


1138 
%\tdx{sum_case_def} sum_case == (\%f g p. @z. (!x. p=Inl x > z=f x) &


1139 
% (!y. p=Inr y > z=g y))


1140 
%


1141 
\tdx{Inl_not_Inr} Inl a ~= Inr b


1142 


1143 
\tdx{inj_Inl} inj Inl


1144 
\tdx{inj_Inr} inj Inr


1145 


1146 
\tdx{sumE} [ !!x. P(Inl x); !!y. P(Inr y) ] ==> P s


1147 


1148 
\tdx{sum_case_Inl} sum_case f g (Inl x) = f x


1149 
\tdx{sum_case_Inr} sum_case f g (Inr x) = g x


1150 


1151 
\tdx{surjective_sum} sum_case (\%x. f(Inl x)) (\%y. f(Inr y)) s = f s


1152 
\tdx{split_sum_case} R(sum_case f g s) = ((! x. s = Inl(x) > R(f(x))) &


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


1154 
\end{ttbox}


1155 
\caption{Type $\alpha+\beta$}\label{holsum}


1156 
\end{figure}


1157 


1158 
\begin{figure}


1159 
\index{*"< symbol}


1160 
\index{*"* symbol}


1161 
\index{*div symbol}


1162 
\index{*mod symbol}


1163 
\index{*"+ symbol}


1164 
\index{*" symbol}


1165 
\begin{constants}


1166 
\it symbol & \it metatype & \it priority & \it description \\


1167 
\cdx{0} & $nat$ & & zero \\


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


1169 
% \cdx{nat_case} & $[\alpha, nat\To\alpha, nat] \To\alpha$ & & conditional\\


1170 
% \cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$


1171 
% & & primitive recursor\\


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


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


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


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


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


1177 
\end{constants}


1178 
\subcaption{Constants and infixes}


1179 


1180 
\begin{ttbox}\makeatother


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


1182 


1183 
\tdx{Suc_not_Zero} Suc m ~= 0


1184 
\tdx{inj_Suc} inj Suc


1185 
\tdx{n_not_Suc_n} n~=Suc n


1186 
\subcaption{Basic properties}


1187 
\end{ttbox}


1188 
\caption{The type of natural numbers, \tydx{nat}} \label{holnat1}


1189 
\end{figure}


1190 


1191 


1192 
\begin{figure}


1193 
\begin{ttbox}\makeatother


1194 
0+n = n


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


1196 


1197 
m0 = m


1198 
0n = n


1199 
Suc(m)Suc(n) = mn


1200 


1201 
0*n = 0


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


1203 


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


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


1206 


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


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


1209 
\end{ttbox}


1210 
\caption{Recursion equations for the arithmetic operators} \label{holnat2}


1211 
\end{figure}


1212 


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


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


1215 


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


1217 
traditional way. The axiom of infinity postulates a type~\tydx{ind} of


1218 
individuals, which is nonempty and closed under an injective operation. The


1219 
natural numbers are inductively generated by choosing an arbitrary individual


1220 
for~0 and using the injective operation to take successors. This is a least


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


1222 


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


1224 
overloaded functions of this class (esp.\ \cdx{<} and \cdx{<=}, but also


1225 
\cdx{min}, \cdx{max} and \cdx{LEAST}) available on \tydx{nat}. Theory


1226 
\thydx{Nat} builds on \texttt{NatDef} and shows that {\tt<=} is a partial order,


1227 
so \tydx{nat} is also an instance of class \cldx{order}.


1228 


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


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


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


1232 
proved include commutative, associative, distributive, identity and


1233 
cancellation laws. See Figs.\ts\ref{holnat1} and~\ref{holnat2}. The


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


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


1236 


1237 
Functions on \tydx{nat} can be defined by primitive or wellfounded recursion;


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


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


1240 
the standard convention.


1241 
\begin{ttbox}


1242 
\sdx{primrec}


1243 
"0 + n = n"


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


1245 
\end{ttbox}


1246 
There is also a \sdx{case}construct


1247 
of the form


1248 
\begin{ttbox}


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


1250 
\end{ttbox}


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


1252 
the order of the two cases.


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


1254 
\cdx{nat_rec}, the details of which can be found in theory \texttt{NatDef}.


1255 


1256 
%The predecessor relation, \cdx{pred_nat}, is shown to be wellfounded.


1257 
%Recursion along this relation resembles primitive recursion, but is


1258 
%stronger because we are in higherorder logic; using primitive recursion to


1259 
%define a higherorder function, we can easily Ackermann's function, which


1260 
%is not primitive recursive \cite[page~104]{thompson91}.


1261 
%The transitive closure of \cdx{pred_nat} is~$<$. Many functions on the


1262 
%natural numbers are most easily expressed using recursion along~$<$.


1263 


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


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


1266 
theorem \tdx{less_induct}:


1267 
\begin{ttbox}


1268 
[ !!n. [ ! m. m<n > P m ] ==> P n ] ==> P n


1269 
\end{ttbox}


1270 


1271 


1272 
Reasoning about arithmetic inequalities can be tedious. Fortunately HOL


1273 
provides a decision procedure for quantifierfree linear arithmetic (i.e.\


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


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


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


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


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


1279 
atomic; subformulae not involving type $nat$ are ignored; quantified


1280 
subformulae are ignored unless they are positive universal or negative


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


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


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


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


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


1286 


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


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


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


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


1291 
\texttt{div} and \texttt{mod}. Use the \texttt{find}functions to locate them


1292 
(see the {\em Reference Manual\/}).


1293 


1294 
\begin{figure}


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


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


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


1298 
\index{*"! symbol}


1299 
\begin{constants}


1300 
\it symbol & \it metatype & \it priority & \it description \\


1301 
\tt[] & $\alpha\,list$ & & empty list\\


1302 
\tt \# & $[\alpha,\alpha\,list]\To \alpha\,list$ & Right 65 &


1303 
list constructor \\


1304 
\cdx{null} & $\alpha\,list \To bool$ & & emptiness test\\


1305 
\cdx{hd} & $\alpha\,list \To \alpha$ & & head \\


1306 
\cdx{tl} & $\alpha\,list \To \alpha\,list$ & & tail \\


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


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


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


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


1311 
& & apply to all\\


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


1313 
& & filter functional\\


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


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


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


1317 
& iteration \\


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


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


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


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


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


1323 
take or drop a prefix \\


1324 
\cdx{takeWhile},\\


1325 
\cdx{dropWhile} &


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


1327 
take or drop a prefix


1328 
\end{constants}


1329 
\subcaption{Constants and infixes}


1330 


1331 
\begin{center} \tt\frenchspacing


1332 
\begin{tabular}{rrr}


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


1334 
[$x@1$, $\dots$, $x@n$] & $x@1$ \# $\cdots$ \# $x@n$ \# [] &


1335 
\rm finite list \\{}


1336 
[$x$:$l$. $P$] & filter ($\lambda x{.}P$) $l$ &


1337 
\rm list comprehension


1338 
\end{tabular}


1339 
\end{center}


1340 
\subcaption{Translations}


1341 
\caption{The theory \thydx{List}} \label{hollist}


1342 
\end{figure}


1343 


1344 


1345 
\begin{figure}


1346 
\begin{ttbox}\makeatother


1347 
null [] = True


1348 
null (x#xs) = False


1349 


1350 
hd (x#xs) = x


1351 
tl (x#xs) = xs


1352 
tl [] = []


1353 


1354 
[] @ ys = ys


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


1356 


1357 
map f [] = []


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


1359 


1360 
filter P [] = []


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


1362 


1363 
set [] = \ttlbrace\ttrbrace


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


1365 


1366 
x mem [] = False


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


1368 


1369 
foldl f a [] = a


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


1371 


1372 
concat([]) = []


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


1374 


1375 
rev([]) = []


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


1377 


1378 
length([]) = 0


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


1380 


1381 
xs!0 = hd xs


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


1383 


1384 
take n [] = []


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


1386 


1387 
drop n [] = []


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


1389 


1390 
takeWhile P [] = []


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


1392 


1393 
dropWhile P [] = []


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


1395 
\end{ttbox}


1396 
\caption{Recursions equations for list processing functions}


1397 
\label{fig:HOL:listsimps}


1398 
\end{figure}


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


1400 


1401 


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


1403 
\label{subsec:list}


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


1405 


1406 
Figure~\ref{hollist} presents the theory \thydx{List}: the basic list


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


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


1409 
As a result the generic structural induction and case analysis tactics


1410 
\texttt{induct\_tac} and \texttt{exhaust\_tac} also become available for


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


1412 
\begin{center}\tt


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


1414 
\end{center}


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


1416 
is also a case splitting rule \tdx{split_list_case}


1417 
\[


1418 
\begin{array}{l}


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


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


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


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


1423 
\end{array}


1424 
\]


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


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


1427 


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


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


1430 
are shown in Fig.\ts\ref{fig:HOL:listsimps}.


1431 


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


1433 


1434 


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


1436 


1437 
The \HOLmethodology dictates that all extensions to a theory should


1438 
be \textbf{definitional}. The type definition mechanism that


1439 
meets this criterion is \ttindex{typedef}. Note that \emph{type synonyms},


1440 
which are inherited from {\Pure} and described elsewhere, are just


1441 
syntactic abbreviations that have no logical meaning.


1442 


1443 
\begin{warn}


1444 
Types in \HOL\ must be nonempty; otherwise the quantifier rules would be


1445 
unsound, because $\exists x. x=x$ is a theorem \cite[\S7]{paulsonCOLOG}.


1446 
\end{warn}


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


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


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


1450 
theorem of the form $x:A$. Thus~$A$ is a nonempty subset of~$\tau$,


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


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


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


1454 
then the type definition creates a type constructor


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


1456 


1457 
\begin{figure}[htbp]


1458 
\begin{rail}


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


1460 


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


1462 
set : string;


1463 
witness : ()  '(' id ')';


1464 
\end{rail}


1465 
\caption{Syntax of type definitions}


1466 
\label{fig:HOL:typedef}


1467 
\end{figure}


1468 


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


1470 
the definition of `typevarlist' and `infix' see


1471 
\iflabelundefined{chap:classical}


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


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


1474 
following meaning:


1475 
\begin{description}


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


1477 
optional infix annotation.


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


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


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


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


1482 
nonemptiness. It can be omitted in case Isabelle manages to prove


1483 
nonemptiness automatically.


1484 
\end{description}


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


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


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


1488 
\begin{itemize}


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


1490 
\item constants


1491 
\begin{eqnarray*}


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


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


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


1495 
\end{eqnarray*}


1496 
\item a definition and three axioms


1497 
\[


1498 
\begin{array}{ll}


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


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


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


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


1503 
\end{array}


1504 
\]


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


1506 
and its inverse $Abs_T$.


1507 
\end{itemize}


1508 
Below are two simple examples of \HOL\ type definitions. Nonemptiness


1509 
is proved automatically here.


1510 
\begin{ttbox}


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


1512 


1513 
typedef (prod)


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


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


1516 
\end{ttbox}


1517 


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


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


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


1521 
\begin{enumerate}


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


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

