author  wenzelm 
Mon, 02 Jan 1995 12:16:12 +0100  
changeset 841  14b96e3bd4ab 
parent 705  9fb068497df4 
child 861  28a593f4b600 
permissions  rwrr 
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\\ 
594
33a6bdb62a18
Logics/HOL: Section 3, added Pow and its rule. New sections 6 on the
lcp
parents:
580
diff
changeset

417 
\cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$ 
111  418 
&set of sets intersection \\ 
594
33a6bdb62a18
Logics/HOL: Section 3, added Pow and its rule. New sections 6 on the
lcp
parents:
580
diff
changeset

419 
\cdx{Union} & $(\alpha\,set)set\To\alpha\,set$ 
111  420 
&set of sets union \\ 
594
33a6bdb62a18
Logics/HOL: Section 3, added Pow and its rule. New sections 6 on the
lcp
parents:
580
diff
changeset

421 
\cdx{Pow} & $\alpha\,set \To (\alpha\,set)set$ 
33a6bdb62a18
Logics/HOL: Section 3, added Pow and its rule. New sections 6 on the
lcp
parents:
580
diff
changeset

422 
& powerset \\[1ex] 
315  423 
\cdx{range} & $(\alpha\To\beta )\To\beta\,set$ 
111  424 
& range of a function \\[1ex] 
315  425 
\cdx{Ball}~~\cdx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$ 
111  426 
& bounded quantifiers \\ 
315  427 
\cdx{mono} & $(\alpha\,set\To\beta\,set)\To bool$ 
111  428 
& monotonicity \\ 
315  429 
\cdx{inj}~~\cdx{surj}& $(\alpha\To\beta )\To bool$ 
111  430 
& injective/surjective \\ 
315  431 
\cdx{inj_onto} & $[\alpha\To\beta ,\alpha\,set]\To bool$ 
111  432 
& injective over subset 
104  433 
\end{tabular} 
434 
\end{center} 

435 
\subcaption{Constants} 

436 

437 
\begin{center} 

438 
\begin{tabular}{llrrr} 

315  439 
\it symbol &\it name &\it metatype & \it priority & \it description \\ 
440 
\sdx{INT} & \cdx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & 

111  441 
intersection over a type\\ 
315  442 
\sdx{UN} & \cdx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & 
111  443 
union over a type 
104  444 
\end{tabular} 
445 
\end{center} 

446 
\subcaption{Binders} 

447 

448 
\begin{center} 

315  449 
\index{*"`"` symbol} 
450 
\index{*": symbol} 

451 
\index{*"<"= symbol} 

104  452 
\begin{tabular}{rrrr} 
315  453 
\it symbol & \it metatype & \it priority & \it description \\ 
111  454 
\tt `` & $[\alpha\To\beta ,\alpha\,set]\To (\beta\,set)$ 
455 
& Left 90 & image \\ 

315  456 
\sdx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ 
111  457 
& Left 70 & intersection ($\inter$) \\ 
315  458 
\sdx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$ 
111  459 
& Left 65 & union ($\union$) \\ 
460 
\tt: & $[\alpha ,\alpha\,set]\To bool$ 

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

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

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

104  464 
\end{tabular} 
465 
\end{center} 

466 
\subcaption{Infixes} 

315  467 
\caption{Syntax of the theory {\tt Set}} \label{holsetsyntax} 
104  468 
\end{figure} 
469 

470 

471 
\begin{figure} 

472 
\begin{center} \tt\frenchspacing 

315  473 
\index{*"! symbol} 
104  474 
\begin{tabular}{rrr} 
111  475 
\it external & \it internal & \it description \\ 
315  476 
$a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm nonmembership\\ 
477 
\{$a@1$, $\ldots$\} & insert($a@1$, $\ldots$\{\}) & \rm finite set \\ 

111  478 
\{$x$.$P[x]$\} & Collect($\lambda x.P[x]$) & 
104  479 
\rm comprehension \\ 
315  480 
\sdx{INT} $x$:$A$.$B[x]$ & INTER($A$,$\lambda x.B[x]$) & 
481 
\rm intersection \\ 

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

483 
\rm union \\ 

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

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

111  486 
\rm bounded $\forall$ \\ 
315  487 
\sdx{?} $x$:$A$.$P[x]$ or \sdx{EX}{\tt\ } $x$:$A$.$P[x]$ & 
488 
Bex($A$,$\lambda x.P[x]$) & \rm bounded $\exists$ 

104  489 
\end{tabular} 
490 
\end{center} 

491 
\subcaption{Translations} 

492 

493 
\dquotes 

315  494 
\[\begin{array}{rclcl} 
104  495 
term & = & \hbox{other terms\ldots} \\ 
111  496 
&  & "\{\}" \\ 
497 
&  & "\{ " term\; ("," term)^* " \}" \\ 

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

499 
&  & term " `` " term \\ 

500 
&  & term " Int " term \\ 

501 
&  & term " Un " term \\ 

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

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

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

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

104  506 
formula & = & \hbox{other formulae\ldots} \\ 
111  507 
&  & term " : " term \\ 
508 
&  & term " \ttilde: " term \\ 

509 
&  & term " <= " term \\ 

315  510 
&  & "!~" id ":" term " . " formula 
111  511 
&  & "ALL " id ":" term " . " formula \\ 
315  512 
&  & "?~" id ":" term " . " formula 
111  513 
&  & "EX~~" id ":" term " . " formula 
104  514 
\end{array} 
515 
\] 

516 
\subcaption{Full Grammar} 

315  517 
\caption{Syntax of the theory {\tt Set} (continued)} \label{holsetsyntax2} 
104  518 
\end{figure} 
519 

520 

521 
\section{A formulation of set theory} 

522 
Historically, higherorder logic gives a foundation for Russell and 

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

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

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

526 
\begin{itemize} 

527 
\item 

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

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

530 
\item 

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

532 
may be defined by absolute comprehension. 

533 
\item 

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

535 
have a more complex type. 

536 
\end{itemize} 

306  537 
Finite unions and intersections have the same behaviour in \HOL\ as they 
538 
do in~{\ZF}. In \HOL\ the intersection of the empty set is welldefined, 

104  539 
denoting the universal set for the given type. 
540 

315  541 

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

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

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

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

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

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

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

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

550 
argument order). 

104  551 

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

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

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

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

315  556 
operator~{\tt``}\@. Note that $a$\verb~:$b$ is translated to 
557 
$\neg(a\in b)$. 

558 

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

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

104  561 
\begin{eqnarray*} 
315  562 
\{a@1, \ldots, a@n\} & \equiv & 
563 
{\tt insert}(a@1,\ldots,{\tt insert}(a@n,\{\})) 

104  564 
\end{eqnarray*} 
565 

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

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

315  568 
occurrences of~$x$. This syntax expands to \cdx{Collect}$(\lambda 
569 
x.P[x])$. It defines sets by absolute comprehension, which is impossible 

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

104  571 

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

573 
\begin{eqnarray*} 

315  574 
\forall x\in A.P[x] &\hbox{abbreviates}& \forall x. x\in A\imp P[x] \\ 
575 
\exists x\in A.P[x] &\hbox{abbreviates}& \exists x. x\in A\conj P[x] 

104  576 
\end{eqnarray*} 
315  577 
The constants~\cdx{Ball} and~\cdx{Bex} are defined 
104  578 
accordingly. Instead of {\tt Ball($A$,$P$)} and {\tt Bex($A$,$P$)} we may 
315  579 
write\index{*"! symbol}\index{*"? symbol} 
580 
\index{*ALL symbol}\index{*EX symbol} 

581 
% 

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

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

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

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

104  586 

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

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

315  589 
\sdx{UN}~\hbox{\tt$x$:$A$.$B[x]$} and 
590 
\sdx{INT}~\hbox{\tt$x$:$A$.$B[x]$}. 

591 

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

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

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

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

596 

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

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

599 
respectively. 

600 

601 

602 
\begin{figure} \underscoreon 

603 
\begin{ttbox} 

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

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

104  606 

841  607 
\tdx{empty_def} \{\} == \{x.False\} 
315  608 
\tdx{insert_def} insert(a,B) == \{x.x=a\} Un B 
609 
\tdx{Ball_def} Ball(A,P) == ! x. x:A > P(x) 

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

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

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

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

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

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

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

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

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

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

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

594
33a6bdb62a18
Logics/HOL: Section 3, added Pow and its rule. New sections 6 on the
lcp
parents:
580
diff
changeset

621 
\tdx{Union_def} Union(S) == (UN x:S. x) 
33a6bdb62a18
Logics/HOL: Section 3, added Pow and its rule. New sections 6 on the
lcp
parents:
580
diff
changeset

622 
\tdx{Pow_def} Pow(A) == \{B. B <= A\} 
315  623 
\tdx{image_def} f``A == \{y. ? x:A. y=f(x)\} 
624 
\tdx{range_def} range(f) == \{y. ? x. y=f(x)\} 

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

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

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

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

629 
\end{ttbox} 

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

631 
\end{figure} 

632 

104  633 

315  634 
\begin{figure} \underscoreon 
635 
\begin{ttbox} 

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

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

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

639 

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

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

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

643 

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

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

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

647 
\subcaption{Comprehension and Bounded quantifiers} 

648 

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

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

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

652 

653 
\tdx{subset_refl} A <= A 

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

655 

471  656 
\tdx{equalityI} [ A <= B; B <= A ] ==> A = B 
315  657 
\tdx{equalityD1} A = B ==> A<=B 
658 
\tdx{equalityD2} A = B ==> B<=A 

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

660 

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

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

663 
] ==> P 

664 
\subcaption{The subset and equality relations} 

665 
\end{ttbox} 

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

667 
\end{figure} 

668 

104  669 

287  670 
\begin{figure} \underscoreon 
104  671 
\begin{ttbox} 
315  672 
\tdx{emptyE} a : \{\} ==> P 
673 

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

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

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

104  677 

315  678 
\tdx{ComplI} [ c:A ==> False ] ==> c : Compl(A) 
679 
\tdx{ComplD} [ c : Compl(A) ] ==> ~ c:A 

680 

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

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

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

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

104  685 

315  686 
\tdx{IntI} [ c:A; c:B ] ==> c : A Int B 
687 
\tdx{IntD1} c : A Int B ==> c:A 

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

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

690 

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

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

104  693 

315  694 
\tdx{INT_I} (!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x)) 
695 
\tdx{INT_D} [ b: (INT x:A. B(x)); a:A ] ==> b: B(a) 

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

697 

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

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

700 

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

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

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

594
33a6bdb62a18
Logics/HOL: Section 3, added Pow and its rule. New sections 6 on the
lcp
parents:
580
diff
changeset

704 

33a6bdb62a18
Logics/HOL: Section 3, added Pow and its rule. New sections 6 on the
lcp
parents:
580
diff
changeset

705 
\tdx{PowI} A<=B ==> A: Pow(B) 
33a6bdb62a18
Logics/HOL: Section 3, added Pow and its rule. New sections 6 on the
lcp
parents:
580
diff
changeset

706 
\tdx{PowD} A: Pow(B) ==> A<=B 
315  707 
\end{ttbox} 
708 
\caption{Further derived rules for set theory} \label{holset2} 

709 
\end{figure} 

710 

104  711 

315  712 
\subsection{Axioms and rules of set theory} 
713 
Figure~\ref{holsetrules} presents the rules of theory \thydx{Set}. The 

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

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

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

104  717 

315  718 
All the other axioms are definitions. They include the empty set, bounded 
719 
quantifiers, unions, intersections, complements and the subset relation. 

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

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

722 
surjectiveness. 

723 

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

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

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

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

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

729 

730 
\begin{figure} \underscoreon 

731 
\begin{ttbox} 

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

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

104  734 

315  735 
%\tdx{Inv_injective} 
736 
% [ Inv(f,x)=Inv(f,y); x: range(f); y: range(f) ] ==> x=y 

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 

104  743 

315  744 
\tdx{monoI} [ !!A B. A <= B ==> f(A) <= f(B) ] ==> mono(f) 
745 
\tdx{monoD} [ mono(f); A <= B ] ==> f(A) <= f(B) 

746 

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

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

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

750 

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

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

753 

754 
\tdx{inj_onto_inverseI} 

104  755 
(!!x. x:A ==> g(f(x)) = x) ==> inj_onto(f,A) 
315  756 
\tdx{inj_onto_contraD} 
104  757 
[ inj_onto(f,A); x~=y; x:A; y:A ] ==> ~ f(x)=f(y) 
758 
\end{ttbox} 

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

760 
\end{figure} 

761 

762 

287  763 
\begin{figure} \underscoreon 
104  764 
\begin{ttbox} 
315  765 
\tdx{Union_upper} B:A ==> B <= Union(A) 
766 
\tdx{Union_least} [ !!X. X:A ==> X<=C ] ==> Union(A) <= C 

104  767 

315  768 
\tdx{Inter_lower} B:A ==> Inter(A) <= B 
769 
\tdx{Inter_greatest} [ !!X. X:A ==> C<=X ] ==> C <= Inter(A) 

104  770 

315  771 
\tdx{Un_upper1} A <= A Un B 
772 
\tdx{Un_upper2} B <= A Un B 

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

104  774 

315  775 
\tdx{Int_lower1} A Int B <= A 
776 
\tdx{Int_lower2} A Int B <= B 

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

104  778 
\end{ttbox} 
779 
\caption{Derived rules involving subsets} \label{holsubset} 

780 
\end{figure} 

781 

782 

315  783 
\begin{figure} \underscoreon \hfuzz=4pt%suppress "Overfull \hbox" message 
104  784 
\begin{ttbox} 
315  785 
\tdx{Int_absorb} A Int A = A 
786 
\tdx{Int_commute} A Int B = B Int A 

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

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

104  789 

315  790 
\tdx{Un_absorb} A Un A = A 
791 
\tdx{Un_commute} A Un B = B Un A 

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

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

104  794 

315  795 
\tdx{Compl_disjoint} A Int Compl(A) = \{x.False\} 
796 
\tdx{Compl_partition} A Un Compl(A) = \{x.True\} 

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

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

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

104  800 

315  801 
\tdx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B) 
802 
\tdx{Int_Union} A Int Union(B) = (UN C:B. A Int C) 

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

104  804 

315  805 
\tdx{Inter_Un_distrib} Inter(A Un B) = Inter(A) Int Inter(B) 
806 
\tdx{Un_Inter} A Un Inter(B) = (INT C:B. A Un C) 

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

104  808 
\end{ttbox} 
809 
\caption{Set equalities} \label{holequalities} 

810 
\end{figure} 

811 

812 

315  813 
Figures~\ref{holset1} and~\ref{holset2} present derived rules. Most are 
814 
obvious and resemble rules of Isabelle's {\ZF} set theory. Certain rules, 

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

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

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

818 
strictly necessary but yield more natural proofs. Similarly, 

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

344  820 
after the fashion of \tdx{iffCE}. See the file {\tt HOL/Set.ML} for 
315  821 
proofs pertaining to set theory. 
104  822 

315  823 
Figure~\ref{holfun} presents derived inference rules involving functions. 
824 
They also include rules for \cdx{Inv}, which is defined in theory~{\tt 

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

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

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

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

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

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

104  831 

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

315  833 
Unions form least upper bounds; nonempty intersections form greatest lower 
834 
bounds. Reasoning directly about subsets often yields clearer proofs than 

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

104  836 

315  837 
Figure~\ref{holequalities} presents many common set equalities. They 
838 
include commutative, associative and distributive laws involving unions, 

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

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

104  841 

842 

287  843 
\begin{figure} 
315  844 
\begin{constants} 
344  845 
\it symbol & \it metatype & & \it description \\ 
315  846 
\cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$ 
847 
& & ordered pairs $\langle a,b\rangle$ \\ 

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

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

705  850 
\cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$ 
315  851 
& & generalized projection\\ 
852 
\cdx{Sigma} & 

287  853 
$[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ & 
315  854 
& general sum of sets 
855 
\end{constants} 

287  856 
\begin{ttbox}\makeatletter 
315  857 
\tdx{fst_def} fst(p) == @a. ? b. p = <a,b> 
858 
\tdx{snd_def} snd(p) == @b. ? a. p = <a,b> 

705  859 
\tdx{split_def} split(c,p) == c(fst(p),snd(p)) 
315  860 
\tdx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\} 
104  861 

862 

315  863 
\tdx{Pair_inject} [ <a, b> = <a',b'>; [ a=a'; b=b' ] ==> R ] ==> R 
349  864 
\tdx{fst_conv} fst(<a,b>) = a 
865 
\tdx{snd_conv} snd(<a,b>) = b 

705  866 
\tdx{split} split(c, <a,b>) = c(a,b) 
104  867 

315  868 
\tdx{surjective_pairing} p = <fst(p),snd(p)> 
287  869 

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

315  872 
\tdx{SigmaE} [ c: Sigma(A,B); 
287  873 
!!x y.[ x:A; y:B(x); c=<x,y> ] ==> P ] ==> P 
104  874 
\end{ttbox} 
315  875 
\caption{Type $\alpha\times\beta$}\label{holprod} 
104  876 
\end{figure} 
877 

878 

287  879 
\begin{figure} 
315  880 
\begin{constants} 
344  881 
\it symbol & \it metatype & & \it description \\ 
315  882 
\cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\ 
883 
\cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\ 

705  884 
\cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$ 
315  885 
& & conditional 
886 
\end{constants} 

887 
\begin{ttbox}\makeatletter 

705  888 
\tdx{sum_case_def} sum_case == (\%f g p. @z. (!x. p=Inl(x) > z=f(x)) & 
315  889 
(!y. p=Inr(y) > z=g(y))) 
104  890 

315  891 
\tdx{Inl_not_Inr} ~ Inl(a)=Inr(b) 
104  892 

315  893 
\tdx{inj_Inl} inj(Inl) 
894 
\tdx{inj_Inr} inj(Inr) 

104  895 

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

705  898 
\tdx{sum_case_Inl} sum_case(f, g, Inl(x)) = f(x) 
899 
\tdx{sum_case_Inr} sum_case(f, g, Inr(x)) = g(x) 

104  900 

705  901 
\tdx{surjective_sum} sum_case(\%x::'a. f(Inl(x)), \%y::'b. f(Inr(y)), s) = f(s) 
104  902 
\end{ttbox} 
315  903 
\caption{Type $\alpha+\beta$}\label{holsum} 
104  904 
\end{figure} 
905 

906 

344  907 
\section{Generic packages and classical reasoning} 
908 
\HOL\ instantiates most of Isabelle's generic packages; 

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

910 
\begin{itemize} 

911 
\item 

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

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

914 
throughout a subgoal and its hypotheses. 

915 
\item 

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

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

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

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

920 
rules. 

921 
\item 

922 
It instantiates the classical reasoner, as described below. 

923 
\end{itemize} 

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

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

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

927 

928 
The classical reasoner is set up as the structure 

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

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

931 
\HOL\ defines the following classical rule sets: 

932 
\begin{ttbox} 

933 
prop_cs : claset 

934 
HOL_cs : claset 

935 
set_cs : claset 

936 
\end{ttbox} 

937 
\begin{ttdescription} 

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

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

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

941 

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

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

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

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

946 
once. 

947 

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

949 
quantifiers, subsets, comprehensions, unions and intersections, 

950 
complements, finite sets, images and ranges. 

951 
\end{ttdescription} 

952 
\noindent 

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

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

955 
for more discussion of classical proof methods. 

956 

957 

104  958 
\section{Types} 
959 
The basic higherorder logic is augmented with a tremendous amount of 

315  960 
material, including support for recursive function and type definitions. A 
961 
detailed discussion appears elsewhere~\cite{paulsoncoind}. The simpler 

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

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

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

104  965 

315  966 
\subsection{Product and sum types}\index{*"* type}\index{*"+ type} 
967 
Theory \thydx{Prod} defines the product type $\alpha\times\beta$, with 

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

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

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

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

972 
their representations are made explicitly. 

104  973 

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

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

344  976 
proved using \tdx{select_equality}. 
104  977 

287  978 
\begin{figure} 
315  979 
\index{*"< symbol} 
980 
\index{*"* symbol} 

344  981 
\index{*div symbol} 
982 
\index{*mod symbol} 

315  983 
\index{*"+ symbol} 
984 
\index{*" symbol} 

985 
\begin{constants} 

986 
\it symbol & \it metatype & \it priority & \it description \\ 

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

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

705  989 
\cdx{nat_case} & $[\alpha, nat\To\alpha, nat] \To\alpha$ 
315  990 
& & conditional\\ 
991 
\cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$ 

992 
& & primitive recursor\\ 

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

111  994 
\tt * & $[nat,nat]\To nat$ & Left 70 & multiplication \\ 
344  995 
\tt div & $[nat,nat]\To nat$ & Left 70 & division\\ 
996 
\tt mod & $[nat,nat]\To nat$ & Left 70 & modulus\\ 

111  997 
\tt + & $[nat,nat]\To nat$ & Left 65 & addition\\ 
998 
\tt  & $[nat,nat]\To nat$ & Left 65 & subtraction 

315  999 
\end{constants} 
104  1000 
\subcaption{Constants and infixes} 
1001 

287  1002 
\begin{ttbox}\makeatother 
705  1003 
\tdx{nat_case_def} nat_case == (\%a f n. @z. (n=0 > z=a) & 
344  1004 
(!x. n=Suc(x) > z=f(x))) 
315  1005 
\tdx{pred_nat_def} pred_nat == \{p. ? n. p = <n, Suc(n)>\} 
1006 
\tdx{less_def} m<n == <m,n>:pred_nat^+ 

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

705  1008 
wfrec(pred_nat, n, nat_case(\%g.c, \%m g. d(m,g(m)))) 
104  1009 

344  1010 
\tdx{add_def} m+n == nat_rec(m, n, \%u v.Suc(v)) 
1011 
\tdx{diff_def} mn == nat_rec(n, m, \%u v. nat_rec(v, 0, \%x y.x)) 

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

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

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

287  1015 
m, \%j f. if(j<n,0,Suc(f(jn)))) 
104  1016 
\subcaption{Definitions} 
1017 
\end{ttbox} 

315  1018 
\caption{Defining {\tt nat}, the type of natural numbers} \label{holnat1} 
104  1019 
\end{figure} 
1020 

1021 

287  1022 
\begin{figure} \underscoreon 
104  1023 
\begin{ttbox} 
315  1024 
\tdx{nat_induct} [ P(0); !!k. [ P(k) ] ==> P(Suc(k)) ] ==> P(n) 
104  1025 

315  1026 
\tdx{Suc_not_Zero} Suc(m) ~= 0 
1027 
\tdx{inj_Suc} inj(Suc) 

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

104  1029 
\subcaption{Basic properties} 
1030 

315  1031 
\tdx{pred_natI} <n, Suc(n)> : pred_nat 
1032 
\tdx{pred_natE} 

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

705  1035 
\tdx{nat_case_0} nat_case(a, f, 0) = a 
1036 
\tdx{nat_case_Suc} nat_case(a, f, Suc(k)) = f(k) 

104  1037 

315  1038 
\tdx{wf_pred_nat} wf(pred_nat) 
1039 
\tdx{nat_rec_0} nat_rec(0,c,h) = c 

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

104  1041 
\subcaption{Case analysis and primitive recursion} 
1042 

315  1043 
\tdx{less_trans} [ i<j; j<k ] ==> i<k 
1044 
\tdx{lessI} n < Suc(n) 

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

104  1046 

315  1047 
\tdx{less_not_sym} n<m > ~ m<n 
1048 
\tdx{less_not_refl} ~ n<n 

1049 
\tdx{not_less0} ~ n<0 

104  1050 

315  1051 
\tdx{Suc_less_eq} (Suc(m) < Suc(n)) = (m<n) 
1052 
\tdx{less_induct} [ !!n. [ ! m. m<n > P(m) ] ==> P(n) ] ==> P(n) 

104  1053 

315  1054 
\tdx{less_linear} m<n  m=n  n<m 
104  1055 
\subcaption{The lessthan relation} 
1056 
\end{ttbox} 

344  1057 
\caption{Derived rules for {\tt nat}} \label{holnat2} 
104  1058 
\end{figure} 
1059 

1060 

315  1061 
\subsection{The type of natural numbers, {\tt nat}} 
1062 
The theory \thydx{Nat} defines the natural numbers in a roundabout but 

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

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

1065 
The natural numbers are inductively generated by choosing an arbitrary 

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

344  1067 
usual, the isomorphisms between~\tydx{nat} and its representation are made 
315  1068 
explicitly. 
104  1069 

315  1070 
The definition makes use of a least fixed point operator \cdx{lfp}, 
1071 
defined using the KnasterTarski theorem. This is used to define the 

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

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

1074 
along arbitrary wellfounded relations. The corresponding theories are 

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

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

104  1077 

315  1078 
Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which 
1079 
overloads $<$ and $\leq$ on the natural numbers. As of this writing, 

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

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

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

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

1084 
$<$ and~$\leq$. 

104  1085 

315  1086 
Theory \thydx{Arith} develops arithmetic on the natural numbers. It 
1087 
defines addition, multiplication, subtraction, division, and remainder. 

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

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

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

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

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

1093 
and~\ref{holnat2}. 

104  1094 

315  1095 
The predecessor relation, \cdx{pred_nat}, is shown to be wellfounded. 
1096 
Recursion along this relation resembles primitive recursion, but is 

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

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

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

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

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

1102 

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

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

104  1105 

287  1106 
\begin{figure} 
315  1107 
\index{#@{\tt\#} symbol} 
1108 
\index{"@@{\tt\at} symbol} 

1109 
\begin{constants} 

1110 
\it symbol & \it metatype & \it priority & \it description \\ 

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

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

1113 
list constructor \\ 

344  1114 
\cdx{null} & $\alpha list \To bool$ & & emptiness test\\ 
315  1115 
\cdx{hd} & $\alpha list \To \alpha$ & & head \\ 
1116 
\cdx{tl} & $\alpha list \To \alpha list$ & & tail \\ 

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

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

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

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

1121 
& & mapping functional\\ 

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

1123 
& & filter functional\\ 

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

1125 
& & forall functional\\ 

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

104  1127 
\beta]\To\beta] \To \beta$ 
315  1128 
& & list recursor 
1129 
\end{constants} 

306  1130 
\subcaption{Constants and infixes} 
1131 

1132 
\begin{center} \tt\frenchspacing 

1133 
\begin{tabular}{rrr} 

315  1134 
\it external & \it internal & \it description \\{} 
1135 
\sdx{[]} & Nil & \rm empty list \\{} 

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

306  1137 
\rm finite list \\{} 
344  1138 
[$x$:$l$. $P$] & filter($\lambda x{.}P$, $l$) & 
315  1139 
\rm list comprehension 
306  1140 
\end{tabular} 
1141 
\end{center} 

1142 
\subcaption{Translations} 

104  1143 

1144 
\begin{ttbox} 

315  1145 
\tdx{list_induct} [ P([]); !!x xs. [ P(xs) ] ==> P(x#xs)) ] ==> P(l) 
104  1146 

315  1147 
\tdx{Cons_not_Nil} (x # xs) ~= [] 
1148 
\tdx{Cons_Cons_eq} ((x # xs) = (y # ys)) = (x=y & xs=ys) 

306  1149 
\subcaption{Induction and freeness} 
104  1150 
\end{ttbox} 
315  1151 
\caption{The theory \thydx{List}} \label{hollist} 
104  1152 
\end{figure} 
1153 

306  1154 
\begin{figure} 
1155 
\begin{ttbox}\makeatother 

471  1156 
\tdx{list_rec_Nil} list_rec([],c,h) = c 
1157 
\tdx{list_rec_Cons} list_rec(a#l, c, h) = h(a, l, list_rec(l,c,h)) 

315  1158 

705  1159 
\tdx{list_case_Nil} list_case(c, h, []) = c 
1160 
\tdx{list_case_Cons} list_case(c, h, x#xs) = h(x, xs) 

315  1161 

471  1162 
\tdx{map_Nil} map(f,[]) = [] 
1163 
\tdx{map_Cons} map(f, x \# xs) = f(x) \# map(f,xs) 

315  1164 

471  1165 
\tdx{null_Nil} null([]) = True 
1166 
\tdx{null_Cons} null(x#xs) = False 

315  1167 

471  1168 
\tdx{hd_Cons} hd(x#xs) = x 
1169 
\tdx{tl_Cons} tl(x#xs) = xs 

315  1170 

471  1171 
\tdx{ttl_Nil} ttl([]) = [] 
1172 
\tdx{ttl_Cons} ttl(x#xs) = xs 

315  1173 

471  1174 
\tdx{append_Nil} [] @ ys = ys 
1175 
\tdx{append_Cons} (x#xs) \at ys = x # xs \at ys 

315  1176 

471  1177 
\tdx{mem_Nil} x mem [] = False 
1178 
\tdx{mem_Cons} x mem (y#ys) = if(y=x, True, x mem ys) 

315  1179 

471  1180 
\tdx{filter_Nil} filter(P, []) = [] 
1181 
\tdx{filter_Cons} filter(P,x#xs) = if(P(x), x#filter(P,xs), filter(P,xs)) 

315  1182 

471  1183 
\tdx{list_all_Nil} list_all(P,[]) = True 
1184 
\tdx{list_all_Cons} list_all(P, x#xs) = (P(x) & list_all(P, xs)) 

306  1185 
\end{ttbox} 
1186 
\caption{Rewrite rules for lists} \label{hollistsimps} 

1187 
\end{figure} 

104  1188 

315  1189 

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

1191 
\index{*list type} 

1192 

306  1193 
\HOL's definition of lists is an example of an experimental method for 
315  1194 
handling recursive data types. Figure~\ref{hollist} presents the theory 
1195 
\thydx{List}: the basic list operations with their types and properties. 

1196 

344  1197 
The \sdx{case} construct is defined by the following translation: 
315  1198 
{\dquotes 
1199 
\begin{eqnarray*} 

344  1200 
\begin{array}{r@{\;}l@{}l} 
315  1201 
"case " e " of" & "[]" & " => " a\\ 
1202 
"" & x"\#"xs & " => " b 

1203 
\end{array} 

1204 
& \equiv & 

705  1205 
"list_case"(a, \lambda x\;xs.b, e) 
344  1206 
\end{eqnarray*}}% 
315  1207 
The theory includes \cdx{list_rec}, a primitive recursion operator 
1208 
for lists. It is derived from wellfounded recursion, a general principle 

1209 
that can express arbitrary total recursive functions. 

1210 

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

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

1213 

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

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

104  1216 

1217 

464  1218 
\section{Datatype declarations} 
1219 
\index{*datatype(} 

1220 

1221 
\underscoreon 

1222 

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

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

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

1226 
datatype} represents a compact way of doing this. 

1227 

1228 

1229 
\subsection{Foundations} 

1230 

1231 
A datatype declaration has the following general structure: 

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

580  1233 
C_1(\tau_{11},\dots,\tau_{1k_1}) ~\mid~ \dots ~\mid~ 
1234 
C_m(\tau_{m1},\dots,\tau_{mk_m}) 

464  1235 
\] 
580  1236 
where $\alpha_i$ are type variables, $C_i$ are distinct constructor names and 
464  1237 
$\tau_{ij}$ are one of the following: 
1238 
\begin{itemize} 

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

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

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

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

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

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

1245 
least one constructor must consist of only nonrecursive type 

1246 
components.} 

1247 
\end{itemize} 

580  1248 
If you would like one of the $\tau_{ij}$ to be a complex type expression 
1249 
$\tau$ you need to declare a new type synonym $syn = \tau$ first and use 

1250 
$syn$ in place of $\tau$. Of course this does not work if $\tau$ mentions the 

1251 
recursive type itself, thus ruling out problematic cases like \[ \mbox{\tt 

1252 
datatype}~ t ~=~ C(t \To t) \] together with unproblematic ones like \[ 

1253 
\mbox{\tt datatype}~ t ~=~ C(t~list). \] 

1254 

464  1255 
The constructors are automatically defined as functions of their respective 
1256 
type: 

580  1257 
\[ C_j : [\tau_{j1},\dots,\tau_{jk_j}] \To (\alpha_1,\dots,\alpha_n)t \] 
464  1258 
These functions have certain {\em freeness} properties: 
1259 
\begin{description} 

465  1260 
\item[\tt distinct] They are distinct: 
580  1261 
\[ C_i(x_1,\dots,x_{k_i}) \neq C_j(y_1,\dots,y_{k_j}) \qquad 
465  1262 
\mbox{for all}~ i \neq j. 
1263 
\] 

464  1264 
\item[\tt inject] They are injective: 
580  1265 
\[ (C_j(x_1,\dots,x_{k_j}) = C_j(y_1,\dots,y_{k_j})) = 
464  1266 
(x_1 = y_1 \land \dots \land x_{k_j} = y_{k_j}) 
1267 
\] 

1268 
\end{description} 

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

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

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

1272 
natural number 

1273 
\[ 

1274 
\begin{array}{lcl} 

580  1275 
\mbox{\it t\_ord}(C_1(x_1,\dots,x_{k_1})) & = & 0 \\ 
464  1276 
& \vdots & \\ 
580  1277 
\mbox{\it t\_ord}(C_m(x_1,\dots,x_{k_m})) & = & m1 
464  1278 
\end{array} 
1279 
\] 

465  1280 
and distinctness of constructors is expressed by: 
464  1281 
\[ 
1282 
\mbox{\it t\_ord}(x) \neq \mbox{\it t\_ord}(y) \Imp x \neq y. 

1283 
\] 

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

1285 
\[ 

1286 
\infer{P(x)} 

1287 
{\begin{array}{lcl} 

1288 
\Forall x_1\dots x_{k_1}. 

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

580  1290 
\Imp & P(C_1(x_1,\dots,x_{k_1})) \\ 
464  1291 
& \vdots & \\ 
1292 
\Forall x_1\dots x_{k_m}. 

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

580  1294 
\Imp & P(C_m(x_1,\dots,x_{k_m})) 
464  1295 
\end{array}} 
1296 
\] 

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

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

1299 
all arguments of the recursive type. 

1300 

465  1301 
The type also comes with an \MLlike \sdx{case}construct: 
464  1302 
\[ 
1303 
\begin{array}{rrcl} 

580  1304 
\mbox{\tt case}~e~\mbox{\tt of} & C_1(x_{11},\dots,x_{1k_1}) & \To & e_1 \\ 
464  1305 
\vdots \\ 
580  1306 
\mid & C_m(x_{m1},\dots,x_{mk_m}) & \To & e_m 
464  1307 
\end{array} 
1308 
\] 

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

1310 
fixed, and nested patterns are not supported. 

1311 

1312 

1313 
\subsection{Defining datatypes} 

1314 

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

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

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

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

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

1320 
section. 

1321 

1322 
\begin{figure} 

1323 
\begin{rail} 

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

1325 
; 

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

1327 
; 

1328 
typ : typevarlist id 

1329 
 tid 

594
33a6bdb62a18
Logics/HOL: Section 3, added Pow and its rule. New sections 6 on the
lcp
parents:
580
diff
changeset

1330 
; 
464  1331 
typevarlist : ()  tid  '(' (tid + ',') ')' 
1332 
; 

1333 
\end{rail} 

1334 
\caption{Syntax of datatype declarations} 

1335 
\label{datatypegrammar} 

1336 
\end{figure} 

1337 

465  1338 
Reading the theory file produces a structure which, in addition to the usual 
464  1339 
components, contains a structure named $t$ for each datatype $t$ defined in 
465  1340 
the file.\footnote{Otherwise multiple datatypes in the same theory file would 
1341 
lead to name clashes.} Each structure $t$ contains the following elements: 

464  1342 
\begin{ttbox} 
465  1343 
val distinct : thm list 
464  1344 
val inject : thm list 
465  1345 
val induct : thm 
464  1346 
val cases : thm list 
1347 
val simps : thm list 

1348 
val induct_tac : string > int > tactic 

1349 
\end{ttbox} 

465  1350 
{\tt distinct}, {\tt inject} and {\tt induct} contain the theorems described 
1351 
above. For convenience {\tt distinct} contains inequalities in both 

1352 
directions. 

464  1353 
\begin{warn} 
1354 
If there are five or more constructors, the {\em t\_ord} scheme is used for 

465  1355 
{\tt distinct}. In this case the theory {\tt Arith} must be contained 
1356 
in the current theory, if necessary by including it explicitly. 

464  1357 
\end{warn} 
465  1358 
The reduction rules of the {\tt case}construct are in {\tt cases}. All 
1359 
theorems from {\tt distinct}, {\tt inject} and {\tt cases} are combined in 

464  1360 
{\tt simps} for use with the simplifier. The tactic ``{\verb$induct_tac$~{\em 
1361 
var i}\/}'' applies structural induction over variable {\em var} to 

1362 
subgoal {\em i}. 

1363 

1364 

1365 
\subsection{Examples} 

1366 

1367 
\subsubsection{The datatype $\alpha~list$} 

1368 

465 