104

1 
%% $Id$

315

2 
\chapter{HigherOrder Logic}


3 
\index{higherorder logic(}


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


5 


6 
The theory~\thydx{HOL} implements higherorder logic.

344

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

315

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


9 
book~\cite{andrews86} is a full description of higherorder logic.


10 
Experience with the {\sc hol} system has demonstrated that higherorder


11 
logic is useful for hardware verification; beyond this, it is widely


12 
applicable in many areas of mathematics. It is weaker than {\ZF} set


13 
theory but for most applications this does not matter. If you prefer {\ML}


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

104

15 

315

16 
Previous releases of Isabelle included a different version of~\HOL, with


17 
explicit type inference rules~\cite{paulsonCOLOG}. This version no longer


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

104

19 

306

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

104

21 
identifies objectlevel types with metalevel types, taking advantage of


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


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

315

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

104

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


26 

306

27 
These identifications allow Isabelle to support \HOL\ particularly nicely,


28 
but they also mean that \HOL\ requires more sophistication from the user

104

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

315

30 
should work with {\tt show_types} set to {\tt true}. Gain experience by


31 
working in firstorder logic before attempting to use higherorder logic.


32 
This chapter assumes familiarity with~{\FOL{}}.

104

33 


34 


35 
\begin{figure}


36 
\begin{center}


37 
\begin{tabular}{rrr}

111

38 
\it name &\it metatype & \it description \\

315

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


40 
\cdx{not} & $bool\To bool$ & negation ($\neg$) \\


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


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


43 
\cdx{if} & $[bool,\alpha,\alpha]\To\alpha::term$ & conditional \\


44 
\cdx{Inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & function inversion\\


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

104

46 
\end{tabular}


47 
\end{center}


48 
\subcaption{Constants}


49 


50 
\begin{center}

315

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


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


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

104

54 
\begin{tabular}{llrrr}

315

55 
\it symbol &\it name &\it metatype & \it description \\


56 
\tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha::term$ &

111

57 
Hilbert description ($\epsilon$) \\

315

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

111

59 
universal quantifier ($\forall$) \\

315

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

111

61 
existential quantifier ($\exists$) \\

315

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

111

63 
unique existence ($\exists!$)

104

64 
\end{tabular}


65 
\end{center}


66 
\subcaption{Binders}


67 


68 
\begin{center}

315

69 
\index{*"= symbol}


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


71 
\index{*" symbol}


72 
\index{*"""> symbol}

104

73 
\begin{tabular}{rrrr}

315

74 
\it symbol & \it metatype & \it priority & \it description \\


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

111

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


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

315

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


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


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

111

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


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

315

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

104

84 
\end{tabular}


85 
\end{center}


86 
\subcaption{Infixes}


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


88 
\end{figure}


89 


90 

306

91 
\begin{figure}

315

92 
\index{*let symbol}


93 
\index{*in symbol}

104

94 
\dquotes

315

95 
\[\begin{array}{rclcl}

104

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

315

97 
&  & "\at~" id~id^* " . " formula \\


98 
&  &


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


100 
\\[2ex]

104

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

111

102 
&  & term " = " term \\


103 
&  & term " \ttilde= " term \\


104 
&  & term " < " term \\


105 
&  & term " <= " term \\


106 
&  & "\ttilde\ " formula \\


107 
&  & formula " \& " formula \\


108 
&  & formula "  " formula \\


109 
&  & formula " > " formula \\

315

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

111

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

315

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

111

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

315

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

111

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

104

116 
\end{array}


117 
\]

306

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

104

119 
\end{figure}


120 


121 


122 
\section{Syntax}

315

123 
The type class of higherorder terms is called~\cldx{term}. Type variables


124 
range over this class by default. The equality symbol and quantifiers are


125 
polymorphic over class {\tt term}.

104

126 

315

127 
Class \cldx{ord} consists of all ordered types; the relations $<$ and

104

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

315

129 
\cdx{mono}, \cdx{min} and \cdx{max}. Three other


130 
type classes  \cldx{plus}, \cldx{minus} and \cldx{times}  permit

104

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


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

315

133 
\index{*"+ symbol}


134 
\index{*" symbol}


135 
\index{*"* symbol}

104

136 


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

315

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

287

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

315

140 
$\neg(a=b)$.


141 


142 
\begin{warn}


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


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


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


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


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


148 
parentheses.


149 
\end{warn}

104

150 

287

151 
\subsection{Types}\label{HOLtypes}

315

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


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


154 
types, is overloaded with arity {\tt(term,term)term}. Thus, $\sigma\To\tau$


155 
belongs to class~{\tt term} if $\sigma$ and~$\tau$ do, allowing quantification


156 
over functions.

104

157 

315

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


159 
unsound. I have commented on this elsewhere~\cite[\S7]{paulsonCOLOG}.


160 


161 
\index{type definitions}

104

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


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


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


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


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


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


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


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

344

170 
type. Melham~\cite{melham89} discusses type definitions at length, with


171 
examples.

104

172 


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

315

174 
mimicked by explicit definitions of isomorphism functions. The definitions


175 
should be supported by theorems of the form $\exists x::\sigma.P(x)$, but


176 
Isabelle cannot enforce this.

104

177 


178 


179 
\subsection{Binders}


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

306

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

104

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


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

315

184 
\cdx{Eps}($P$) or use the syntax


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


186 


187 
Existential quantification is defined by


188 
\[ \exists x.P(x) \;\equiv\; P(\epsilon x.P(x)). \]

104

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


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


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


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


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


194 

315

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

306

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

104

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


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


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

315

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

104

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


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


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


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


205 

315

206 
All these binders have priority 10.


207 


208 


209 
\subsection{The \sdx{let} and \sdx{case} constructions}


210 
Local abbreviations can be introduced by a {\tt let} construct whose


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


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


213 
definition, \tdx{Let_def}.

104

214 

315

215 
\HOL\ also defines the basic syntax


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


217 
as a uniform means of expressing {\tt case} constructs. Therefore {\tt


218 
case} and \sdx{of} are reserved words. However, so far this is mere


219 
syntax and has no logical meaning. By declaring translations, you can


220 
cause instances of the {\tt case} construct to denote applications of


221 
particular case operators. The patterns supplied for $c@1$,~\ldots,~$c@n$


222 
distinguish among the different case operators. For an example, see the


223 
case construct for lists on page~\pageref{hollist} below.


224 

306

225 

315

226 
\begin{figure}


227 
\begin{ttbox}\makeatother

453

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

315

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

453

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

315

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


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


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


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


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


236 
\end{ttbox}


237 
\caption{The {\tt HOL} rules} \label{holrules}


238 
\end{figure}

306

239 


240 

344

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

287

242 
\begin{ttbox}\makeatother

453

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

344

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


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


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


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


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


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


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

315

251 

344

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


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


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


255 
\tdx{Let_def} Let(s,f) == f(s)

315

256 
\end{ttbox}


257 
\caption{The {\tt HOL} definitions} \label{holdefs}


258 
\end{figure}


259 


260 


261 
\section{Rules of inference}


262 
Figure~\ref{holrules} shows the inference rules of~\HOL{}, with


263 
their~{\ML} names. Some of the rules deserve additional comments:


264 
\begin{ttdescription}


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


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


267 
equal.


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


269 
$\epsilon$operator. It is a form of the Axiom of Choice. The derived rule


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


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


272 
fact, the $\epsilon$operator already makes the logic classical, as


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


274 
\end{ttdescription}

104

275 

315

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


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

344

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


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


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


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


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


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

315

284 

344

285 
Some of the rules mention type variables; for


286 
example, {\tt refl} mentions the type variable~{\tt'a}. This allows you to


287 
instantiate type variables explicitly by calling {\tt res_inst_tac}. By


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

104

289 

315

290 
Include type constraints whenever you state a polymorphic goal. Type


291 
inference may otherwise make the goal more polymorphic than you intended,


292 
with confusing results.


293 


294 
\begin{warn}


295 
If resolution fails for no obvious reason, try setting


296 
\ttindex{show_types} to {\tt true}, causing Isabelle to display types of


297 
terms. Possibly set \ttindex{show_sorts} to {\tt true} as well, causing


298 
Isabelle to display sorts.


299 


300 
\index{unification!incompleteness of}


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


302 
guarantee to find instantiations for type variables automatically. Be


303 
prepared to use \ttindex{res_inst_tac} instead of {\tt resolve_tac},


304 
possibly instantiating type variables. Setting


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


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


307 
\end{warn}

104

308 


309 

287

310 
\begin{figure}

104

311 
\begin{ttbox}

315

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


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


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


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

453

316 
\tdx{arg_cong} x=y ==> f(x)=f(y)


317 
\tdx{fun_cong} f=g ==> f(x)=g(x)

104

318 
\subcaption{Equality}


319 

315

320 
\tdx{TrueI} True


321 
\tdx{FalseE} False ==> P

104

322 

315

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


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


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


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

104

327 

315

328 
\tdx{disjI1} P ==> PQ


329 
\tdx{disjI2} Q ==> PQ


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

104

331 

315

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


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


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

104

335 
\subcaption{Propositional logic}


336 

315

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


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


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


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

104

341 

315

342 
\tdx{eqTrueI} P ==> P=True


343 
\tdx{eqTrueE} P=True ==> P

104

344 
\subcaption{Logical equivalence}


345 


346 
\end{ttbox}

306

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

104

348 
\end{figure}


349 


350 

287

351 
\begin{figure}


352 
\begin{ttbox}\makeatother

315

353 
\tdx{allI} (!!x::'a. P(x)) ==> !x. P(x)


354 
\tdx{spec} !x::'a.P(x) ==> P(x)


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


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

104

357 

315

358 
\tdx{exI} P(x) ==> ? x::'a.P(x)


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

104

360 

315

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


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

104

363 
] ==> R


364 

315

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

104

366 
\subcaption{Quantifiers and descriptions}


367 

315

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


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


370 
\tdx{excluded_middle} ~P  P

104

371 

315

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


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


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


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


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


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

104

378 
\subcaption{Classical logic}


379 

315

380 
\tdx{if_True} if(True,x,y) = x


381 
\tdx{if_False} if(False,x,y) = y


382 
\tdx{if_P} P ==> if(P,x,y) = x


383 
\tdx{if_not_P} ~ P ==> if(P,x,y) = y


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

104

385 
\subcaption{Conditionals}


386 
\end{ttbox}


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


388 
\end{figure}


389 


390 


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


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


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


394 
conjunctions, implications, and universal quantifiers.


395 

315

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


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

104

398 
simplifying both sides of an equation.


399 


400 


401 
\begin{figure}


402 
\begin{center}


403 
\begin{tabular}{rrr}

111

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

315

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


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


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

111

408 
& insertion of element \\

315

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

111

410 
& comprehension \\

315

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

111

412 
& complement \\

315

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

111

414 
& intersection over a set\\

315

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

111

416 
& union over a set\\

315

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

111

418 
&set of sets intersection \\

315

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

111

420 
&set of sets union \\

315

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

111

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

315

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

111

424 
& bounded quantifiers \\

315

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

111

426 
& monotonicity \\

315

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

111

428 
& injective/surjective \\

315

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

111

430 
& injective over subset

104

431 
\end{tabular}


432 
\end{center}


433 
\subcaption{Constants}


434 


435 
\begin{center}


436 
\begin{tabular}{llrrr}

315

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


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

111

439 
intersection over a type\\

315

440 
\sdx{UN} & \cdx{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}

315

447 
\index{*"`"` symbol}


448 
\index{*": symbol}


449 
\index{*"<"= symbol}

104

450 
\begin{tabular}{rrrr}

315

451 
\it symbol & \it metatype & \it priority & \it description \\

111

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


453 
& Left 90 & image \\

315

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

111

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

315

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

111

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}

315

465 
\caption{Syntax of the theory {\tt Set}} \label{holsetsyntax}

104

466 
\end{figure}


467 


468 


469 
\begin{figure}


470 
\begin{center} \tt\frenchspacing

315

471 
\index{*"! symbol}

104

472 
\begin{tabular}{rrr}

111

473 
\it external & \it internal & \it description \\

315

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


475 
\{$a@1$, $\ldots$\} & insert($a@1$, $\ldots$\{\}) & \rm finite set \\

111

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

104

477 
\rm comprehension \\

315

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


479 
\rm intersection \\


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


481 
\rm union \\


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


483 
Ball($A$,$\lambda x.P[x]$) &

111

484 
\rm bounded $\forall$ \\

315

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


486 
Bex($A$,$\lambda x.P[x]$) & \rm bounded $\exists$

104

487 
\end{tabular}


488 
\end{center}


489 
\subcaption{Translations}


490 


491 
\dquotes

315

492 
\[\begin{array}{rclcl}

104

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

111

494 
&  & "\{\}" \\


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


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


497 
&  & term " `` " term \\


498 
&  & term " Int " term \\


499 
&  & term " Un " term \\


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


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


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


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

104

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

111

505 
&  & term " : " term \\


506 
&  & term " \ttilde: " term \\


507 
&  & term " <= " term \\

315

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

111

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

315

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

111

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

104

512 
\end{array}


513 
\]


514 
\subcaption{Full Grammar}

315

515 
\caption{Syntax of the theory {\tt Set} (continued)} \label{holsetsyntax2}

104

516 
\end{figure}


517 


518 


519 
\section{A formulation of set theory}


520 
Historically, higherorder logic gives a foundation for Russell and


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


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


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


524 
\begin{itemize}


525 
\item


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


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


528 
\item


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


530 
may be defined by absolute comprehension.


531 
\item


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


533 
have a more complex type.


534 
\end{itemize}

306

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


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

104

537 
denoting the universal set for the given type.


538 

315

539 


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


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


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


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


544 
Since Isabelle does not support type definitions (as mentioned in


545 
\S\ref{HOLtypes}), the isomorphisms between the two types are declared


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


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


548 
argument order).

104

549 


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


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


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


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

315

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


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


556 


557 
The {\tt\{\ldots\}} notation abbreviates finite sets constructed in the


558 
obvious manner using~{\tt insert} and~$\{\}$:

104

559 
\begin{eqnarray*}

315

560 
\{a@1, \ldots, a@n\} & \equiv &


561 
{\tt insert}(a@1,\ldots,{\tt insert}(a@n,\{\}))

104

562 
\end{eqnarray*}


563 


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


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

315

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


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


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

104

569 


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


571 
\begin{eqnarray*}

315

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


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

104

574 
\end{eqnarray*}

315

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

104

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

315

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


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


579 
%


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


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


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


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

104

584 


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


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

315

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


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


589 


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


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


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


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


594 


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


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


597 
respectively.


598 


599 


600 
\begin{figure} \underscoreon


601 
\begin{ttbox}


602 
\tdx{mem_Collect_eq} (a : \{x.P(x)\}) = P(a)


603 
\tdx{Collect_mem_eq} \{x.x:A\} = A

104

604 

315

605 
\tdx{empty_def} \{\} == \{x.x=False\}


606 
\tdx{insert_def} insert(a,B) == \{x.x=a\} Un B


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


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


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


610 
\tdx{Un_def} A Un B == \{x.x:A  x:B\}


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


612 
\tdx{set_diff_def} A  B == \{x.x:A & x~:B\}


613 
\tdx{Compl_def} Compl(A) == \{x. ~ x:A\}


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


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


616 
\tdx{INTER1_def} INTER1(B) == INTER(\{x.True\}, B)


617 
\tdx{UNION1_def} UNION1(B) == UNION(\{x.True\}, B)


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


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


620 
\tdx{image_def} f``A == \{y. ? x:A. y=f(x)\}


621 
\tdx{range_def} range(f) == \{y. ? x. y=f(x)\}


622 
\tdx{mono_def} mono(f) == !A B. A <= B > f(A) <= f(B)


623 
\tdx{inj_def} inj(f) == ! x y. f(x)=f(y) > x=y


624 
\tdx{surj_def} surj(f) == ! y. ? x. y=f(x)


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


626 
\end{ttbox}


627 
\caption{Rules of the theory {\tt Set}} \label{holsetrules}


628 
\end{figure}


629 

104

630 

315

631 
\begin{figure} \underscoreon


632 
\begin{ttbox}


633 
\tdx{CollectI} [ P(a) ] ==> a : \{x.P(x)\}


634 
\tdx{CollectD} [ a : \{x.P(x)\} ] ==> P(a)


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


636 


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


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


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


640 


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


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


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


644 
\subcaption{Comprehension and Bounded quantifiers}


645 


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


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


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


649 


650 
\tdx{subset_refl} A <= A


651 
\tdx{subset_antisym} [ A <= B; B <= A ] ==> A = B


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


653 


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


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


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


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


658 


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


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


661 
] ==> P


662 
\subcaption{The subset and equality relations}


663 
\end{ttbox}


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


665 
\end{figure}


666 

104

667 

287

668 
\begin{figure} \underscoreon

104

669 
\begin{ttbox}

315

670 
\tdx{emptyE} a : \{\} ==> P


671 


672 
\tdx{insertI1} a : insert(a,B)


673 
\tdx{insertI2} a : B ==> a : insert(b,B)


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

104

675 

315

676 
\tdx{ComplI} [ c:A ==> False ] ==> c : Compl(A)


677 
\tdx{ComplD} [ c : Compl(A) ] ==> ~ c:A


678 


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


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


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


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

104

683 

315

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


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


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


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


688 


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


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

104

691 

315

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


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


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


695 


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


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


698 


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


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


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


702 
\end{ttbox}


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


704 
\end{figure}


705 

104

706 

315

707 
\subsection{Axioms and rules of set theory}


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


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


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


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

104

712 

315

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


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


715 
They also include straightforward properties of functions: image~({\tt``}) and


716 
{\tt range}, and predicates concerning monotonicity, injectiveness and


717 
surjectiveness.


718 


719 
The predicate \cdx{inj_onto} is used for simulating type definitions.


720 
The statement ${\tt inj_onto}(f,A)$ asserts that $f$ is injective on the


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


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


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


724 


725 
\begin{figure} \underscoreon


726 
\begin{ttbox}


727 
\tdx{Inv_f_f} inj(f) ==> Inv(f,f(x)) = x


728 
\tdx{f_Inv_f} y : range(f) ==> f(Inv(f,y)) = y

104

729 

315

730 
%\tdx{Inv_injective}


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


732 
%


733 
\tdx{imageI} [ x:A ] ==> f(x) : f``A


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


735 


736 
\tdx{rangeI} f(x) : range(f)


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

104

738 

315

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


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


741 


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


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


744 
\tdx{injD} [ inj(f); f(x) = f(y) ] ==> x=y


745 


746 
\tdx{inj_ontoI} (!!x y. [ f(x)=f(y); x:A; y:A ] ==> x=y) ==> inj_onto(f,A)


747 
\tdx{inj_ontoD} [ inj_onto(f,A); f(x)=f(y); x:A; y:A ] ==> x=y


748 


749 
\tdx{inj_onto_inverseI}

104

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

315

751 
\tdx{inj_onto_contraD}

104

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


753 
\end{ttbox}


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


755 
\end{figure}


756 


757 

287

758 
\begin{figure} \underscoreon

104

759 
\begin{ttbox}

315

760 
\tdx{Union_upper} B:A ==> B <= Union(A)


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

104

762 

315

763 
\tdx{Inter_lower} B:A ==> Inter(A) <= B


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

104

765 

315

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


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


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

104

769 

315

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


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


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

104

773 
\end{ttbox}


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


775 
\end{figure}


776 


777 

315

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

104

779 
\begin{ttbox}

315

780 
\tdx{Int_absorb} A Int A = A


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


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


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

104

784 

315

785 
\tdx{Un_absorb} A Un A = A


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


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


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

104

789 

315

790 
\tdx{Compl_disjoint} A Int Compl(A) = \{x.False\}


791 
\tdx{Compl_partition} A Un Compl(A) = \{x.True\}


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


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


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

104

795 

315

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


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


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

104

799 

315

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


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


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

104

803 
\end{ttbox}


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


805 
\end{figure}


806 


807 

315

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


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


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


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


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


813 
strictly necessary but yield more natural proofs. Similarly,


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

344

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

315

816 
proofs pertaining to set theory.

104

817 

315

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


819 
They also include rules for \cdx{Inv}, which is defined in theory~{\tt


820 
HOL}; note that ${\tt Inv}(f)$ applies the Axiom of Choice to yield an


821 
inverse of~$f$. They also include natural deduction rules for the image


822 
and range operators, and for the predicates {\tt inj} and {\tt inj_onto}.


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


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


825 
the file {\tt HOL/fun.ML} for a complete listing of the derived rules.

104

826 


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

315

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


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


830 
reasoning about the membership relation. See the file {\tt HOL/subset.ML}.

104

831 

315

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


833 
include commutative, associative and distributive laws involving unions,


834 
intersections and complements. The proofs are mostly trivial, using the


835 
classical reasoner; see file {\tt HOL/equalities.ML}.

104

836 


837 

287

838 
\begin{figure}

315

839 
\begin{constants}

344

840 
\it symbol & \it metatype & & \it description \\

315

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


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


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


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


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


846 
& & generalized projection\\


847 
\cdx{Sigma} &

287

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

315

849 
& general sum of sets


850 
\end{constants}

287

851 
\begin{ttbox}\makeatletter

315

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


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


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


855 
\tdx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}

104

856 


857 

315

858 
\tdx{Pair_inject} [ <a, b> = <a',b'>; [ a=a'; b=b' ] ==> R ] ==> R

349

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


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

315

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

104

862 

315

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

287

864 

315

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

287

866 

315

867 
\tdx{SigmaE} [ c: Sigma(A,B);

287

868 
!!x y.[ x:A; y:B(x); c=<x,y> ] ==> P ] ==> P

104

869 
\end{ttbox}

315

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

104

871 
\end{figure}


872 


873 

287

874 
\begin{figure}

315

875 
\begin{constants}

344

876 
\it symbol & \it metatype & & \it description \\

315

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


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


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


880 
& & conditional


881 
\end{constants}


882 
\begin{ttbox}\makeatletter


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


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

104

885 

315

886 
\tdx{Inl_not_Inr} ~ Inl(a)=Inr(b)

104

887 

315

888 
\tdx{inj_Inl} inj(Inl)


889 
\tdx{inj_Inr} inj(Inr)

104

890 

315

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

104

892 

315

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


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

104

895 

315

896 
\tdx{surjective_sum} sum_case(s, \%x::'a. f(Inl(x)), \%y::'b. f(Inr(y))) = f(s)

104

897 
\end{ttbox}

315

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

104

899 
\end{figure}


900 


901 

344

902 
\section{Generic packages and classical reasoning}


903 
\HOL\ instantiates most of Isabelle's generic packages;


904 
see {\tt HOL/ROOT.ML} for details.


905 
\begin{itemize}


906 
\item


907 
Because it includes a general substitution rule, \HOL\ instantiates the


908 
tactic {\tt hyp_subst_tac}, which substitutes for an equality


909 
throughout a subgoal and its hypotheses.


910 
\item


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


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


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


914 
{\tt HOL/simpdata.ML} for a complete listing of the simplification


915 
rules.


916 
\item


917 
It instantiates the classical reasoner, as described below.


918 
\end{itemize}


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


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


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


922 


923 
The classical reasoner is set up as the structure


924 
{\tt Classical}. This structure is open, so {\ML} identifiers such


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


926 
\HOL\ defines the following classical rule sets:


927 
\begin{ttbox}


928 
prop_cs : claset


929 
HOL_cs : claset


930 
HOL_dup_cs : claset


931 
set_cs : claset


932 
\end{ttbox}


933 
\begin{ttdescription}


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


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


936 
along with the rule~{\tt refl}.


937 


938 
\item[\ttindexbold{HOL_cs}] extends {\tt prop_cs} with the safe rules


939 
{\tt allI} and~{\tt exE} and the unsafe rules {\tt allE}


940 
and~{\tt exI}, as well as rules for unique existence. Search using


941 
this classical set is incomplete: quantified formulae are used at most


942 
once.


943 


944 
\item[\ttindexbold{HOL_dup_cs}] extends {\tt prop_cs} with the safe rules


945 
{\tt allI} and~{\tt exE} and the unsafe rules \tdx{all_dupE}


946 
and~\tdx{exCI}, as well as rules for unique existence. Search using


947 
this is complete  quantified formulae may be duplicated  but


948 
frequently fails to terminate. It is generally unsuitable for


949 
depthfirst search.


950 


951 
\item[\ttindexbold{set_cs}] extends {\tt HOL_cs} with rules for the bounded


952 
quantifiers, subsets, comprehensions, unions and intersections,


953 
complements, finite sets, images and ranges.


954 
\end{ttdescription}


955 
\noindent


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


957 
{Chap.\ts\ref{chap:classical}}


958 
for more discussion of classical proof methods.


959 


960 

104

961 
\section{Types}


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

315

963 
material, including support for recursive function and type definitions. A


964 
detailed discussion appears elsewhere~\cite{paulsoncoind}. The simpler


965 
definitions are the same as those used the {\sc hol} system, but my


966 
treatment of recursive types differs from Melham's~\cite{melham89}. The


967 
present section describes product, sum, natural number and list types.

104

968 

315

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


970 
Theory \thydx{Prod} defines the product type $\alpha\times\beta$, with


971 
the ordered pair syntax {\tt<$a$,$b$>}. Theory \thydx{Sum} defines the


972 
sum type $\alpha+\beta$. These use fairly standard constructions; see


973 
Figs.\ts\ref{holprod} and~\ref{holsum}. Because Isabelle does not


974 
support abstract type definitions, the isomorphisms between these types and


975 
their representations are made explicitly.

104

976 


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


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

344

979 
proved using \tdx{select_equality}.

104

980 

287

981 
\begin{figure}

315

982 
\index{*"< symbol}


983 
\index{*"* symbol}

344

984 
\index{*div symbol}


985 
\index{*mod symbol}

315

986 
\index{*"+ symbol}


987 
\index{*" symbol}


988 
\begin{constants}


989 
\it symbol & \it metatype & \it priority & \it description \\


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


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


992 
\cdx{nat_case} & $[nat, \alpha, nat\To\alpha] \To\alpha$


993 
& & conditional\\


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


995 
& & primitive recursor\\


996 
\cdx{pred_nat} & $(nat\times nat) set$ & & predecessor relation\\

111

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

344

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


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

111

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


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

315

1002 
\end{constants}

104

1003 
\subcaption{Constants and infixes}


1004 

287

1005 
\begin{ttbox}\makeatother

315

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

344

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

315

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


1009 
\tdx{less_def} m<n == <m,n>:pred_nat^+


1010 
\tdx{nat_rec_def} nat_rec(n,c,d) ==

287

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

104

1012 

344

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


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


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


1016 
\tdx{mod_def} m mod n == wfrec(trancl(pred_nat), m, \%j f. if(j<n,j,f(jn)))


1017 
\tdx{quo_def} m div n == wfrec(trancl(pred_nat),

287

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

104

1019 
\subcaption{Definitions}


1020 
\end{ttbox}

315

1021 
\caption{Defining {\tt nat}, the type of natural numbers} \label{holnat1}

104

1022 
\end{figure}


1023 


1024 

287

1025 
\begin{figure} \underscoreon

104

1026 
\begin{ttbox}

315

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

104

1028 

315

1029 
\tdx{Suc_not_Zero} Suc(m) ~= 0


1030 
\tdx{inj_Suc} inj(Suc)


1031 
\tdx{n_not_Suc_n} n~=Suc(n)

104

1032 
\subcaption{Basic properties}


1033 

315

1034 
\tdx{pred_natI} <n, Suc(n)> : pred_nat


1035 
\tdx{pred_natE}

104

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


1037 

315

1038 
\tdx{nat_case_0} nat_case(0, a, f) = a


1039 
\tdx{nat_case_Suc} nat_case(Suc(k), a, f) = f(k)

104

1040 

315

1041 
\tdx{wf_pred_nat} wf(pred_nat)


1042 
\tdx{nat_rec_0} nat_rec(0,c,h) = c


1043 
\tdx{nat_rec_Suc} nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h))

104

1044 
\subcaption{Case analysis and primitive recursion}


1045 

315

1046 
\tdx{less_trans} [ i<j; j<k ] ==> i<k


1047 
\tdx{lessI} n < Suc(n)


1048 
\tdx{zero_less_Suc} 0 < Suc(n)

104

1049 

315

1050 
\tdx{less_not_sym} n<m > ~ m<n


1051 
\tdx{less_not_refl} ~ n<n


1052 
\tdx{not_less0} ~ n<0

104

1053 

315

1054 
\tdx{Suc_less_eq} (Suc(m) < Suc(n)) = (m<n)


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

104

1056 

315

1057 
\tdx{less_linear} m<n  m=n  n<m

104

1058 
\subcaption{The lessthan relation}


1059 
\end{ttbox}

344

1060 
\caption{Derived rules for {\tt nat}} \label{holnat2}

104

1061 
\end{figure}


1062 


1063 

315

1064 
\subsection{The type of natural numbers, {\tt nat}}


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


1066 
traditional way. The axiom of infinity postulates an type~\tydx{ind} of


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


1068 
The natural numbers are inductively generated by choosing an arbitrary


1069 
individual for~0 and using the injective operation to take successors. As

344

1070 
usual, the isomorphisms between~\tydx{nat} and its representation are made

315

1071 
explicitly.

104

1072 

315

1073 
The definition makes use of a least fixed point operator \cdx{lfp},


1074 
defined using the KnasterTarski theorem. This is used to define the


1075 
operator \cdx{trancl}, for taking the transitive closure of a relation.


1076 
Primitive recursion makes use of \cdx{wfrec}, an operator for recursion


1077 
along arbitrary wellfounded relations. The corresponding theories are


1078 
called {\tt Lfp}, {\tt Trancl} and {\tt WF}\@. Elsewhere I have described


1079 
similar constructions in the context of set theory~\cite{paulsonsetII}.

104

1080 

315

1081 
Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which


1082 
overloads $<$ and $\leq$ on the natural numbers. As of this writing,


1083 
Isabelle provides no means of verifying that such overloading is sensible;


1084 
there is no means of specifying the operators' properties and verifying


1085 
that instances of the operators satisfy those properties. To be safe, the


1086 
\HOL\ theory includes no polymorphic axioms asserting general properties of


1087 
$<$ and~$\leq$.

104

1088 

315

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


1090 
defines addition, multiplication, subtraction, division, and remainder.


1091 
Many of their properties are proved: commutative, associative and


1092 
distributive laws, identity and cancellation laws, etc. The most


1093 
interesting result is perhaps the theorem $a \bmod b + (a/b)\times b = a$.


1094 
Division and remainder are defined by repeated subtraction, which requires


1095 
wellfounded rather than primitive recursion. See Figs.\ts\ref{holnat1}


1096 
and~\ref{holnat2}.

104

1097 

315

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


1099 
Recursion along this relation resembles primitive recursion, but is


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


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


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


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


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


1105 


1106 
The tactic {\tt\ttindex{nat_ind_tac} "$n$" $i$} performs induction over the


1107 
variable~$n$ in subgoal~$i$.

104

1108 

287

1109 
\begin{figure}

315

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


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


1112 
\begin{constants}


1113 
\it symbol & \it metatype & \it priority & \it description \\


1114 
\cdx{Nil} & $\alpha list$ & & empty list\\


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


1116 
list constructor \\

344

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

315

1118 
\cdx{hd} & $\alpha list \To \alpha$ & & head \\


1119 
\cdx{tl} & $\alpha list \To \alpha list$ & & tail \\


1120 
\cdx{ttl} & $\alpha list \To \alpha list$ & & total tail \\


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


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


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


1124 
& & mapping functional\\


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


1126 
& & filter functional\\


1127 
\cdx{list_all}& $(\alpha \To bool) \To (\alpha list \To bool)$


1128 
& & forall functional\\


1129 
\cdx{list_rec} & $[\alpha list, \beta, [\alpha ,\alpha list,

104

1130 
\beta]\To\beta] \To \beta$

315

1131 
& & list recursor


1132 
\end{constants}

306

1133 
\subcaption{Constants and infixes}


1134 


1135 
\begin{center} \tt\frenchspacing


1136 
\begin{tabular}{rrr}

315

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


1138 
\sdx{[]} & Nil & \rm empty list \\{}


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

306

1140 
\rm finite list \\{}

344

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

315

1142 
\rm list comprehension

306

1143 
\end{tabular}


1144 
\end{center}


1145 
\subcaption{Translations}

104

1146 


1147 
\begin{ttbox}

315

1148 
\tdx{list_induct} [ P([]); !!x xs. [ P(xs) ] ==> P(x#xs)) ] ==> P(l)

104

1149 

315

1150 
\tdx{Cons_not_Nil} (x # xs) ~= []


1151 
\tdx{Cons_Cons_eq} ((x # xs) = (y # ys)) = (x=y & xs=ys)

306

1152 
\subcaption{Induction and freeness}

104

1153 
\end{ttbox}

315

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

104

1155 
\end{figure}


1156 

306

1157 
\begin{figure}


1158 
\begin{ttbox}\makeatother

315

1159 
\tdx{list_rec_Nil} list_rec([],c,h) = c


1160 
\tdx{list_rec_Cons} list_rec(a \# l, c, h) = h(a, l, list_rec(l,c,h))


1161 


1162 
\tdx{list_case_Nil} list_case([],c,h) = c


1163 
\tdx{list_case_Cons} list_case(x # xs, c, h) = h(x, xs)


1164 


1165 
\tdx{map_Nil} map(f,[]) = []


1166 
\tdx{map_Cons} map(f, x \# xs) = f(x) \# map(f,xs)


1167 


1168 
\tdx{null_Nil} null([]) = True


1169 
\tdx{null_Cons} null(x # xs) = False


1170 


1171 
\tdx{hd_Cons} hd(x # xs) = x


1172 
\tdx{tl_Cons} tl(x # xs) = xs


1173 


1174 
\tdx{ttl_Nil} ttl([]) = []


1175 
\tdx{ttl_Cons} ttl(x # xs) = xs


1176 


1177 
\tdx{append_Nil} [] @ ys = ys


1178 
\tdx{append_Cons} (x # xs) \at ys = x # xs \at ys


1179 


1180 
\tdx{mem_Nil} x mem [] = False


1181 
\tdx{mem_Cons} x mem y # ys = if(y = x, True, x mem ys)


1182 


1183 
\tdx{filter_Nil} filter(P, []) = []


1184 
\tdx{filter_Cons} filter(P,x#xs) = if(P(x),x#filter(P,xs),filter(P,xs))


1185 


1186 
\tdx{list_all_Nil} list_all(P,[]) = True


1187 
\tdx{list_all_Cons} list_all(P, x # xs) = (P(x) & list_all(P, xs))

306

1188 
\end{ttbox}


1189 
\caption{Rewrite rules for lists} \label{hollistsimps}


1190 
\end{figure}

104

1191 

315

1192 


1193 
\subsection{The type constructor for lists, {\tt list}}


1194 
\index{*list type}


1195 

306

1196 
\HOL's definition of lists is an example of an experimental method for

315

1197 
handling recursive data types. Figure~\ref{hollist} presents the theory


1198 
\thydx{List}: the basic list operations with their types and properties.


1199 

344

1200 
The \sdx{case} construct is defined by the following translation:

315

1201 
{\dquotes


1202 
\begin{eqnarray*}

344

1203 
\begin{array}{r@{\;}l@{}l}

315

1204 
"case " e " of" & "[]" & " => " a\\


1205 
"" & x"\#"xs & " => " b


1206 
\end{array}


1207 
& \equiv &

344

1208 
"list_case"(e, a, \lambda x\;xs.b)


1209 
\end{eqnarray*}}%

315

1210 
The theory includes \cdx{list_rec}, a primitive recursion operator


1211 
for lists. It is derived from wellfounded recursion, a general principle


1212 
that can express arbitrary total recursive functions.


1213 


1214 
The simpset \ttindex{list_ss} contains, along with additional useful lemmas,


1215 
the basic rewrite rules that appear in Fig.\ts\ref{hollistsimps}.


1216 


1217 
The tactic {\tt\ttindex{list_ind_tac} "$xs$" $i$} performs induction over the


1218 
variable~$xs$ in subgoal~$i$.

104

1219 


1220 

315

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


1222 
\index{*llist type}


1223 

104

1224 
The definition of lazy lists demonstrates methods for handling infinite

344

1225 
data structures and coinduction in higherorder logic. Theory


1226 
\thydx{LList} defines an operator for corecursion on lazy lists, which is


1227 
used to define a few simple functions such as map and append. Corecursion


1228 
cannot easily define operations such as filter, which can compute


1229 
indefinitely before yielding the next element (if any!) of the lazy list.


1230 
A coinduction principle is defined for proving equations on lazy lists.

315

1231 


1232 
I have written a paper discussing the treatment of lazy lists; it also


1233 
covers finite lists~\cite{paulsoncoind}.

104

1234 


1235 

464

1236 
\section{Datatype declarations}


1237 
\index{*datatype(}


1238 


1239 
\underscoreon


1240 


1241 
It is often necessary to extend a theory with \MLlike datatypes. This


1242 
extension consists of the new type, declarations of its constructors and


1243 
rules that describe the new type. The theory definition section {\tt


1244 
datatype} represents a compact way of doing this.


1245 


1246 


1247 
\subsection{Foundations}


1248 


1249 
A datatype declaration has the following general structure:


1250 
\[ \mbox{\tt datatype}~ (\alpha_1,\dots,\alpha_n)t ~=~


1251 
c_1(\tau_{11},\dots,\tau_{1k_1}) ~\mid~ \dots ~\mid~


1252 
c_m(\tau_{m1},\dots,\tau_{mk_m})


1253 
\]


1254 
where $\alpha_i$ are type variables, $c_i$ are distinct constructor names and


1255 
$\tau_{ij}$ are one of the following:


1256 
\begin{itemize}


1257 
\item type variables $\alpha_1,\dots,\alpha_n$,


1258 
\item types $(\beta_1,\dots,\beta_l)s$ where $s$ is a previously declared


1259 
type or type synonym and $\{\beta_1,\dots,\beta_l\} \subseteq


1260 
\{\alpha_1,\dots,\alpha_n\}$,


1261 
\item the newly defined type $(\alpha_1,\dots,\alpha_n)t$ \footnote{This


1262 
makes it a recursive type. To ensure that the new type is not empty at


1263 
least one constructor must consist of only nonrecursive type


1264 
components.}


1265 
\end{itemize}


1266 
The constructors are automatically defined as functions of their respective


1267 
type:


1268 
\[ c_j : [\tau_{j1},\dots,\tau_{jk_j}] \To (\alpha_1,\dots,\alpha_n)t \]


1269 
These functions have certain {\em freeness} properties:


1270 
\begin{description}

465

1271 
\item[\tt distinct] They are distinct:


1272 
\[ c_i(x_1,\dots,x_{k_i}) \neq c_j(y_1,\dots,y_{k_j}) \qquad


1273 
\mbox{for all}~ i \neq j.


1274 
\]

464

1275 
\item[\tt inject] They are injective:


1276 
\[ (c_j(x_1,\dots,x_{k_j}) = c_j(y_1,\dots,y_{k_j})) =


1277 
(x_1 = y_1 \land \dots \land x_{k_j} = y_{k_j})


1278 
\]


1279 
\end{description}


1280 
Because the number of inequalities is quadratic in the number of


1281 
constructors, a different method is used if their number exceeds


1282 
a certain value, currently 4. In that case every constructor is mapped to a


1283 
natural number


1284 
\[


1285 
\begin{array}{lcl}


1286 
\mbox{\it t\_ord}(c_1(x_1,\dots,x_{k_1})) & = & 0 \\


1287 
& \vdots & \\


1288 
\mbox{\it t\_ord}(c_m(x_1,\dots,x_{k_m})) & = & m1


1289 
\end{array}


1290 
\]

465

1291 
and distinctness of constructors is expressed by:

464

1292 
\[


1293 
\mbox{\it t\_ord}(x) \neq \mbox{\it t\_ord}(y) \Imp x \neq y.


1294 
\]


1295 
In addition a structural induction axiom {\tt induct} is provided:


1296 
\[


1297 
\infer{P(x)}


1298 
{\begin{array}{lcl}


1299 
\Forall x_1\dots x_{k_1}.


1300 
\List{P(x_{r_{11}}); \dots; P(x_{r_{1l_1}})} &


1301 
\Imp & P(c_1(x_1,\dots,x_{k_1})) \\


1302 
& \vdots & \\


1303 
\Forall x_1\dots x_{k_m}.


1304 
\List{P(x_{r_{m1}}); \dots; P(x_{r_{ml_m}})} &


1305 
\Imp & P(c_m(x_1,\dots,x_{k_m}))


1306 
\end{array}}


1307 
\]


1308 
where $\{r_{j1},\dots,r_{jl_j}\} = \{i \in \{1,\dots k_j\} ~\mid~ \tau_{ji}


1309 
= (\alpha_1,\dots,\alpha_n)t \}$, i.e.\ the property $P$ can be assumed for


1310 
all arguments of the recursive type.


1311 

465

1312 
The type also comes with an \MLlike \sdx{case}construct:

464

1313 
\[


1314 
\begin{array}{rrcl}

465

1315 
\mbox{\tt case}~e~\mbox{\tt of} & c_1(x_{11},\dots,x_{1k_1}) & \To & e_1 \\

464

1316 
\vdots \\

465

1317 
\mid & c_m(x_{m1},\dots,x_{mk_m}) & \To & e_m

464

1318 
\end{array}


1319 
\]


1320 
In contrast to \ML, {\em all} constructors must be present, their order is


1321 
fixed, and nested patterns are not supported.


1322 


1323 


1324 
\subsection{Defining datatypes}


1325 


1326 
A datatype is defined in a theory definition file using the keyword {\tt


1327 
datatype}. The definition following {\tt datatype} must conform to the


1328 
syntax of {\em typedecl} specified in Fig.~\ref{datatypegrammar} and must


1329 
obey the rules in the previous section. As a result the theory is extended


1330 
with the new type, the constructors, and the theorems listed in the previous


1331 
section.


1332 


1333 
\begin{figure}


1334 
\begin{rail}


1335 
typedecl : typevarlist id '=' (cons + '')


1336 
;


1337 
cons : (id  string) ( ()  '(' (typ + ',') ')' ) ( ()  mixfix )


1338 
;


1339 
typ : typevarlist id


1340 
 tid


1341 
;


1342 
typevarlist : ()  tid  '(' (tid + ',') ')'


1343 
;


1344 
\end{rail}


1345 
\caption{Syntax of datatype declarations}


1346 
\label{datatypegrammar}


1347 
\end{figure}


1348 

465

1349 
Reading the theory file produces a structure which, in addition to the usual

464

1350 
components, contains a structure named $t$ for each datatype $t$ defined in

465

1351 
the file.\footnote{Otherwise multiple datatypes in the same theory file would


1352 
lead to name clashes.} Each structure $t$ contains the following elements:

464

1353 
\begin{ttbox}

465

1354 
val distinct : thm list

464

1355 
val inject : thm list

465

1356 
val induct : thm

464

1357 
val cases : thm list


1358 
val simps : thm list


1359 
val induct_tac : string > int > tactic


1360 
\end{ttbox}

465

1361 
{\tt distinct}, {\tt inject} and {\tt induct} contain the theorems described


1362 
above. For convenience {\tt distinct} contains inequalities in both


1363 
directions.

464

1364 
\begin{warn}


1365 
If there are five or more constructors, the {\em t\_ord} scheme is used for

465

1366 
{\tt distinct}. In this case the theory {\tt Arith} must be contained


1367 
in the current theory, if necessary by including it explicitly.

464

1368 
\end{warn}

465

1369 
The reduction rules of the {\tt case}construct are in {\tt cases}. All


1370 
theorems from {\tt distinct}, {\tt inject} and {\tt cases} are combined in

464

1371 
{\tt simps} for use with the simplifier. The tactic ``{\verb$induct_tac$~{\em


1372 
var i}\/}'' applies structural induction over variable {\em var} to


1373 
subgoal {\em i}.


1374 


1375 


1376 
\subsection{Examples}


1377 < 