author  paulson 
Tue, 10 Feb 2004 12:02:11 +0100  
changeset 14378  69c4d5997669 
parent 9695  ec7d7f877712 
permissions  rwrr 
104  1 
%% $Id$ 
315  2 
\chapter{HigherOrder Logic} 
3 
\index{higherorder logic(} 

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

5 

9695  6 
The theory~\thydx{HOL} implements higherorder logic. It is based on 
7 
Gordon's~{\sc hol} system~\cite{mgordonhol}, which itself is based on 

8 
Church's original paper~\cite{church40}. Andrews's book~\cite{andrews86} is a 

9 
full description of higherorder logic. Experience with the {\sc hol} system 

10 
has demonstrated that higherorder logic is useful for hardware verification; 

11 
beyond this, it is widely applicable in many areas of mathematics. It is 

12 
weaker than ZF set theory but for most applications this does not matter. If 

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

104  14 

9695  15 
Previous releases of Isabelle included a different version of~HOL, with 
315  16 
explicit type inference rules~\cite{paulsonCOLOG}. This version no longer 
17 
exists, but \thydx{ZF} supports a similar style of reasoning. 

104  18 

9695  19 
HOL has a distinct feel, compared with ZF and CTT. It identifies objectlevel 
20 
types with metalevel types, taking advantage of Isabelle's builtin type 

21 
checker. It identifies objectlevel functions with metalevel functions, so 

22 
it uses Isabelle's operations for abstraction and application. There is no 

23 
`apply' operator: function applications are written as simply~$f(a)$ rather 

24 
than $f{\tt`}a$. 

104  25 

9695  26 
These identifications allow Isabelle to support HOL particularly nicely, but 
27 
they also mean that HOL requires more sophistication from the user  in 

28 
particular, an understanding of Isabelle's type system. Beginners should work 

29 
with {\tt show_types} set to {\tt true}. Gain experience by working in 

30 
firstorder logic before attempting to use higherorder logic. This chapter 

31 
assumes familiarity with~FOL. 

104  32 

33 

34 
\begin{figure} 

35 
\begin{center} 

36 
\begin{tabular}{rrr} 

111  37 
\it name &\it metatype & \it description \\ 
315  38 
\cdx{Trueprop}& $bool\To prop$ & coercion to $prop$\\ 
39 
\cdx{not} & $bool\To bool$ & negation ($\neg$) \\ 

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

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

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

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

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

104  45 
\end{tabular} 
46 
\end{center} 

47 
\subcaption{Constants} 

48 

49 
\begin{center} 

315  50 
\index{"@@{\tt\at} symbol} 
51 
\index{*"! symbol}\index{*"? symbol} 

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

104  53 
\begin{tabular}{llrrr} 
315  54 
\it symbol &\it name &\it metatype & \it description \\ 
55 
\tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha::term$ & 

111  56 
Hilbert description ($\epsilon$) \\ 
315  57 
{\tt!~} or \sdx{ALL} & \cdx{All} & $(\alpha::term\To bool)\To bool$ & 
111  58 
universal quantifier ($\forall$) \\ 
315  59 
{\tt?~} or \sdx{EX} & \cdx{Ex} & $(\alpha::term\To bool)\To bool$ & 
111  60 
existential quantifier ($\exists$) \\ 
315  61 
{\tt?!} or {\tt EX!} & \cdx{Ex1} & $(\alpha::term\To bool)\To bool$ & 
111  62 
unique existence ($\exists!$) 
104  63 
\end{tabular} 
64 
\end{center} 

65 
\subcaption{Binders} 

66 

67 
\begin{center} 

315  68 
\index{*"= symbol} 
69 
\index{&@{\tt\&} symbol} 

70 
\index{*" symbol} 

71 
\index{*"""> symbol} 

104  72 
\begin{tabular}{rrrr} 
315  73 
\it symbol & \it metatype & \it priority & \it description \\ 
74 
\sdx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ & 

111  75 
Right 50 & composition ($\circ$) \\ 
76 
\tt = & $[\alpha::term,\alpha]\To bool$ & Left 50 & equality ($=$) \\ 

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

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

111  80 
\tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\ 
81 
\tt  & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\ 

315  82 
\tt > & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$) 
104  83 
\end{tabular} 
84 
\end{center} 

85 
\subcaption{Infixes} 

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

87 
\end{figure} 

88 

89 

306  90 
\begin{figure} 
315  91 
\index{*let symbol} 
92 
\index{*in symbol} 

104  93 
\dquotes 
315  94 
\[\begin{array}{rclcl} 
104  95 
term & = & \hbox{expression of class~$term$} \\ 
315  96 
&  & "\at~" id~id^* " . " formula \\ 
97 
&  & 

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

99 
\\[2ex] 

104  100 
formula & = & \hbox{expression of type~$bool$} \\ 
111  101 
&  & term " = " term \\ 
102 
&  & term " \ttilde= " term \\ 

103 
&  & term " < " term \\ 

104 
&  & term " <= " term \\ 

105 
&  & "\ttilde\ " formula \\ 

106 
&  & formula " \& " formula \\ 

107 
&  & formula "  " formula \\ 

108 
&  & formula " > " formula \\ 

315  109 
&  & "!~~~" id~id^* " . " formula 
111  110 
&  & "ALL~" id~id^* " . " formula \\ 
315  111 
&  & "?~~~" id~id^* " . " formula 
111  112 
&  & "EX~~" id~id^* " . " formula \\ 
315  113 
&  & "?!~~" id~id^* " . " formula 
111  114 
&  & "EX!~" id~id^* " . " formula 
104  115 
\end{array} 
116 
\] 

9695  117 
\caption{Full grammar for HOL} \label{holgrammar} 
104  118 
\end{figure} 
119 

120 

121 
\section{Syntax} 

315  122 
The type class of higherorder terms is called~\cldx{term}. Type variables 
123 
range over this class by default. The equality symbol and quantifiers are 

124 
polymorphic over class {\tt term}. 

104  125 

315  126 
Class \cldx{ord} consists of all ordered types; the relations $<$ and 
104  127 
$\leq$ are polymorphic over this class, as are the functions 
315  128 
\cdx{mono}, \cdx{min} and \cdx{max}. Three other 
129 
type classes  \cldx{plus}, \cldx{minus} and \cldx{times}  permit 

104  130 
overloading of the operators {\tt+}, {\tt} and {\tt*}. In particular, 
131 
{\tt} is overloaded for set difference and subtraction. 

315  132 
\index{*"+ symbol} 
133 
\index{*" symbol} 

134 
\index{*"* symbol} 

104  135 

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

315  137 
binders), while Fig.\ts\ref{holgrammar} presents the grammar of 
287  138 
higherorder logic. Note that $a$\verb~=$b$ is translated to 
315  139 
$\neg(a=b)$. 
140 

141 
\begin{warn} 

9695  142 
HOL has no ifandonlyif connective; logical equivalence is expressed 
315  143 
using equality. But equality has a high priority, as befitting a 
144 
relation, while ifandonlyif typically has the lowest priority. Thus, 

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

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

147 
parentheses. 

148 
\end{warn} 

104  149 

287  150 
\subsection{Types}\label{HOLtypes} 
315  151 
The type of formulae, \tydx{bool}, belongs to class \cldx{term}; thus, 
152 
formulae are terms. The builtin type~\tydx{fun}, which constructs function 

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

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

155 
over functions. 

104  156 

9695  157 
Types in HOL must be nonempty; otherwise the quantifier rules would be 
315  158 
unsound. I have commented on this elsewhere~\cite[\S7]{paulsonCOLOG}. 
159 

160 
\index{type definitions} 

104  161 
Gordon's {\sc hol} system supports {\bf type definitions}. A type is 
162 
defined by exhibiting an existing type~$\sigma$, a predicate~$P::\sigma\To 

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

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

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

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

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

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

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

104  171 

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

315  173 
mimicked by explicit definitions of isomorphism functions. The definitions 
174 
should be supported by theorems of the form $\exists x::\sigma.P(x)$, but 

175 
Isabelle cannot enforce this. 

104  176 

177 

178 
\subsection{Binders} 

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

9695  180 
satisfying~$P[a]$, if such exists. Since all terms in HOL denote something, a 
181 
description is always meaningful, but we do not know its value unless $P[x]$ 

182 
defines it uniquely. We may write descriptions as \cdx{Eps}($P$) or use the 

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

315  184 

185 
Existential quantification is defined by 

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

104  187 
The unique existence quantifier, $\exists!x.P[x]$, is defined in terms 
188 
of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested 

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

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

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

192 

315  193 
\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} 
9695  194 
Quantifiers have two notations. As in Gordon's {\sc hol} system, HOL 
104  195 
uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$. The 
196 
existential quantifier must be followed by a space; thus {\tt?x} is an 

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

9695  198 
notation for quantifiers, \sdx{ALL} and \sdx{EX}, is also available. Both 
199 
notations are accepted for input. The {\ML} reference 

104  200 
\ttindexbold{HOL_quantifiers} governs the output notation. If set to {\tt 
9695  201 
true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set 
104  202 
to {\tt false}, then~{\tt ALL} and~{\tt EX} are displayed. 
203 

315  204 
All these binders have priority 10. 
205 

206 

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

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

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

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

211 
definition, \tdx{Let_def}. 

104  212 

9695  213 
HOL also defines the basic syntax 
315  214 
\[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"" \dots ""~c@n~"=>"~e@n\] 
215 
as a uniform means of expressing {\tt case} constructs. Therefore {\tt 

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

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

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

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

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

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

222 

306  223 

315  224 
\begin{figure} 
225 
\begin{ttbox}\makeatother 

453  226 
\tdx{refl} t = (t::'a) 
315  227 
\tdx{subst} [ s=t; P(s) ] ==> P(t::'a) 
453  228 
\tdx{ext} (!!x::'a. (f(x)::'b) = g(x)) ==> (\%x.f(x)) = (\%x.g(x)) 
315  229 
\tdx{impI} (P ==> Q) ==> P>Q 
230 
\tdx{mp} [ P>Q; P ] ==> Q 

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

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

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

234 
\end{ttbox} 

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

236 
\end{figure} 

306  237 

238 

344  239 
\begin{figure}\hfuzz=4pt%suppress "Overfull \hbox" message 
287  240 
\begin{ttbox}\makeatother 
453  241 
\tdx{True_def} True == ((\%x::bool.x)=(\%x.x)) 
344  242 
\tdx{All_def} All == (\%P. P = (\%x.True)) 
243 
\tdx{Ex_def} Ex == (\%P. P(@x.P(x))) 

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

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

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

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

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

315  249 

344  250 
\tdx{Inv_def} Inv == (\%(f::'a=>'b) y. @x. f(x)=y) 
251 
\tdx{o_def} op o == (\%(f::'b=>'c) g (x::'a). f(g(x))) 

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

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

315  254 
\end{ttbox} 
255 
\caption{The {\tt HOL} definitions} \label{holdefs} 

256 
\end{figure} 

257 

258 

259 
\section{Rules of inference} 

9695  260 
Figure~\ref{holrules} shows the inference rules of~HOL, with their~{\ML} 
261 
names. Some of the rules deserve additional comments: 

315  262 
\begin{ttdescription} 
263 
\item[\tdx{ext}] expresses extensionality of functions. 

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

265 
equal. 

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

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

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

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

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

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

272 
\end{ttdescription} 

104  273 

9695  274 
HOL follows standard practice in higherorder logic: only a few connectives 
275 
are taken as primitive, with the remainder defined obscurely 

344  276 
(Fig.\ts\ref{holdefs}). Gordon's {\sc hol} system expresses the 
277 
corresponding definitions \cite[page~270]{mgordonhol} using 

9695  278 
objectequality~({\tt=}), which is possible because equality in higherorder 
279 
logic may equate formulae and even functions over formulae. But theory~HOL, 

280 
like all other Isabelle theories, uses metaequality~({\tt==}) for 

281 
definitions. 

315  282 

344  283 
Some of the rules mention type variables; for 
284 
example, {\tt refl} mentions the type variable~{\tt'a}. This allows you to 

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

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

104  287 

315  288 
Include type constraints whenever you state a polymorphic goal. Type 
289 
inference may otherwise make the goal more polymorphic than you intended, 

290 
with confusing results. 

291 

292 
\begin{warn} 

293 
If resolution fails for no obvious reason, try setting 

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

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

296 
Isabelle to display sorts. 

297 

298 
\index{unification!incompleteness of} 

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

300 
guarantee to find instantiations for type variables automatically. Be 

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

302 
possibly instantiating type variables. Setting 

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

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

305 
\end{warn} 

104  306 

307 

287  308 
\begin{figure} 
104  309 
\begin{ttbox} 
315  310 
\tdx{sym} s=t ==> t=s 
311 
\tdx{trans} [ r=s; s=t ] ==> r=t 

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

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

453  314 
\tdx{arg_cong} x=y ==> f(x)=f(y) 
315 
\tdx{fun_cong} f=g ==> f(x)=g(x) 

104  316 
\subcaption{Equality} 
317 

315  318 
\tdx{TrueI} True 
319 
\tdx{FalseE} False ==> P 

104  320 

315  321 
\tdx{conjI} [ P; Q ] ==> P&Q 
322 
\tdx{conjunct1} [ P&Q ] ==> P 

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

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

104  325 

315  326 
\tdx{disjI1} P ==> PQ 
327 
\tdx{disjI2} Q ==> PQ 

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

104  329 

315  330 
\tdx{notI} (P ==> False) ==> ~ P 
331 
\tdx{notE} [ ~ P; P ] ==> R 

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

104  333 
\subcaption{Propositional logic} 
334 

315  335 
\tdx{iffI} [ P ==> Q; Q ==> P ] ==> P=Q 
336 
\tdx{iffD1} [ P=Q; P ] ==> Q 

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

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

104  339 

315  340 
\tdx{eqTrueI} P ==> P=True 
341 
\tdx{eqTrueE} P=True ==> P 

104  342 
\subcaption{Logical equivalence} 
343 

344 
\end{ttbox} 

9695  345 
\caption{Derived rules for HOL} \label{hollemmas1} 
104  346 
\end{figure} 
347 

348 

287  349 
\begin{figure} 
350 
\begin{ttbox}\makeatother 

315  351 
\tdx{allI} (!!x::'a. P(x)) ==> !x. P(x) 
352 
\tdx{spec} !x::'a.P(x) ==> P(x) 

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

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

104  355 

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

104  358 

315  359 
\tdx{ex1I} [ P(a); !!x. P(x) ==> x=a ] ==> ?! x. P(x) 
360 
\tdx{ex1E} [ ?! x.P(x); !!x. [ P(x); ! y. P(y) > y=x ] ==> R 

104  361 
] ==> R 
362 

315  363 
\tdx{select_equality} [ P(a); !!x. P(x) ==> x=a ] ==> (@x.P(x)) = a 
104  364 
\subcaption{Quantifiers and descriptions} 
365 

315  366 
\tdx{ccontr} (~P ==> False) ==> P 
367 
\tdx{classical} (~P ==> P) ==> P 

368 
\tdx{excluded_middle} ~P  P 

104  369 

315  370 
\tdx{disjCI} (~Q ==> P) ==> PQ 
371 
\tdx{exCI} (! x. ~ P(x) ==> P(a)) ==> ? x.P(x) 

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

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

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

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

104  376 
\subcaption{Classical logic} 
377 

315  378 
\tdx{if_True} if(True,x,y) = x 
379 
\tdx{if_False} if(False,x,y) = y 

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

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

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

104  383 
\subcaption{Conditionals} 
384 
\end{ttbox} 

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

386 
\end{figure} 

387 

388 

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

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

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

392 
conjunctions, implications, and universal quantifiers. 

393 

315  394 
Note the equality rules: \tdx{ssubst} performs substitution in 
395 
backward proofs, while \tdx{box_equals} supports reasoning by 

104  396 
simplifying both sides of an equation. 
397 

398 

399 
\begin{figure} 

400 
\begin{center} 

401 
\begin{tabular}{rrr} 

111  402 
\it name &\it metatype & \it description \\ 
315  403 
\index{{}@\verb'{}' symbol} 
404 
\verb{} & $\alpha\,set$ & the empty set \\ 

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

111  406 
& insertion of element \\ 
315  407 
\cdx{Collect} & $(\alpha\To bool)\To\alpha\,set$ 
111  408 
& comprehension \\ 
315  409 
\cdx{Compl} & $(\alpha\,set)\To\alpha\,set$ 
111  410 
& complement \\ 
315  411 
\cdx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$ 
111  412 
& intersection over a set\\ 
315  413 
\cdx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$ 
111  414 
& 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

415 
\cdx{Inter} & $(\alpha\,set)set\To\alpha\,set$ 
111  416 
&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

417 
\cdx{Union} & $(\alpha\,set)set\To\alpha\,set$ 
111  418 
&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

419 
\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

420 
& powerset \\[1ex] 
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 

9695  522 
{\bf sets}, but note that these sets are distinct from those of ZF set theory, 
523 
and behave more like ZF classes. 

104  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} 

9695  535 
Finite unions and intersections have the same behaviour in HOL as they do 
536 
in~ZF. In HOL the intersection of the empty set is welldefined, denoting the 

537 
universal set for the given type. 

104  538 

315  539 

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

9695  541 
HOL's set theory is called \thydx{Set}. The type $\alpha\,set$ is essentially 
542 
the same as $\alpha\To bool$. The new type is defined for clarity and to 

543 
avoid complications involving function types in unification. Since Isabelle 

544 
does not support type definitions (as mentioned in \S\ref{HOLtypes}), the 

545 
isomorphisms between the two types are declared explicitly. Here they are 

546 
natural: {\tt Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt 

547 
op :} maps in the other direction (ignoring argument order). 

104  548 

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

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

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

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

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

555 

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

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

104  558 
\begin{eqnarray*} 
315  559 
\{a@1, \ldots, a@n\} & \equiv & 
560 
{\tt insert}(a@1,\ldots,{\tt insert}(a@n,\{\})) 

104  561 
\end{eqnarray*} 
562 

9695  563 
The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type) that 
564 
satisfy~$P[x]$, where $P[x]$ is a formula that may contain free occurrences 

565 
of~$x$. This syntax expands to \cdx{Collect}$(\lambda x.P[x])$. It defines 

566 
sets by absolute comprehension, which is impossible in~ZF; the type of~$x$ 

567 
implicitly restricts the comprehension. 

104  568 

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

570 
\begin{eqnarray*} 

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

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

578 
% 

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

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

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

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

104  583 

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

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

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

588 

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

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

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

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

593 

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

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

596 
respectively. 

597 

598 

599 
\begin{figure} \underscoreon 

600 
\begin{ttbox} 

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

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

104  603 

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

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

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

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

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

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

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

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

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

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

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

617 
\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

618 
\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

619 
\tdx{Pow_def} Pow(A) == \{B. B <= A\} 
315  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_trans} [ A<=B; B<=C ] ==> A<=C 

652 

471  653 
\tdx{equalityI} [ A <= B; B <= A ] ==> A = B 
315  654 
\tdx{equalityD1} A = B ==> A<=B 
655 
\tdx{equalityD2} A = B ==> B<=A 

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

657 

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

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

660 
] ==> P 

661 
\subcaption{The subset and equality relations} 

662 
\end{ttbox} 

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

664 
\end{figure} 

665 

104  666 

287  667 
\begin{figure} \underscoreon 
104  668 
\begin{ttbox} 
315  669 
\tdx{emptyE} a : \{\} ==> P 
670 

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

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

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

104  674 

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

677 

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

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

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

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

104  682 

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

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

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

687 

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

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

104  690 

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

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

694 

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

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

697 

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

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

700 
\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

701 

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

702 
\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

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

706 
\end{figure} 

707 

104  708 

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

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

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

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

104  714 

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

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

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

719 
surjectiveness. 

720 

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

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

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

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

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

726 

727 
\begin{figure} \underscoreon 

728 
\begin{ttbox} 

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

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

104  731 

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

734 
% 

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

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

737 

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

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

104  740 

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

743 

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

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

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

747 

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

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

750 

751 
\tdx{inj_onto_inverseI} 

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

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

757 
\end{figure} 

758 

759 

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

104  764 

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

104  767 

315  768 
\tdx{Un_upper1} A <= A Un B 
769 
\tdx{Un_upper2} B <= A Un B 

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

104  771 

315  772 
\tdx{Int_lower1} A Int B <= A 
773 
\tdx{Int_lower2} A Int B <= B 

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

104  775 
\end{ttbox} 
776 
\caption{Derived rules involving subsets} \label{holsubset} 

777 
\end{figure} 

778 

779 

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

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

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

104  786 

315  787 
\tdx{Un_absorb} A Un A = A 
788 
\tdx{Un_commute} A Un B = B Un A 

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

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

104  791 

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

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

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

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

104  797 

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

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

104  801 

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

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

104  805 
\end{ttbox} 
806 
\caption{Set equalities} \label{holequalities} 

807 
\end{figure} 

808 

809 

315  810 
Figures~\ref{holset1} and~\ref{holset2} present derived rules. Most are 
9695  811 
obvious and resemble rules of Isabelle's ZF set theory. Certain rules, such 
812 
as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI}, are designed for classical 

813 
reasoning; the rules \tdx{subsetD}, \tdx{bexI}, \tdx{Un1} and~\tdx{Un2} are 

814 
not strictly necessary but yield more natural proofs. Similarly, 

815 
\tdx{equalityCE} supports classical reasoning about extensionality, after the 

816 
fashion of \tdx{iffCE}. See the file {\tt HOL/Set.ML} for proofs pertaining 

817 
to set theory. 

104  818 

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

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

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

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

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

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

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

104  827 

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

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

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

104  832 

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

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

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

104  837 

838 

287  839 
\begin{figure} 
315  840 
\begin{constants} 
344  841 
\it symbol & \it metatype & & \it description \\ 
315  842 
\cdx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$ 
843 
& & ordered pairs $\langle a,b\rangle$ \\ 

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

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

705  846 
\cdx{split} & $[[\alpha,\beta]\To\gamma, \alpha\times\beta] \To \gamma$ 
315  847 
& & generalized projection\\ 
848 
\cdx{Sigma} & 

287  849 
$[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ & 
315  850 
& general sum of sets 
851 
\end{constants} 

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

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

858 

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

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

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

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

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

874 

287  875 
\begin{figure} 
315  876 
\begin{constants} 
344  877 
\it symbol & \it metatype & & \it description \\ 
315  878 
\cdx{Inl} & $\alpha \To \alpha+\beta$ & & first injection\\ 
879 
\cdx{Inr} & $\beta \To \alpha+\beta$ & & second injection\\ 

705  880 
\cdx{sum_case} & $[\alpha\To\gamma, \beta\To\gamma, \alpha+\beta] \To\gamma$ 
315  881 
& & conditional 
882 
\end{constants} 

883 
\begin{ttbox}\makeatletter 

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

315  887 
\tdx{Inl_not_Inr} ~ Inl(a)=Inr(b) 
104  888 

315  889 
\tdx{inj_Inl} inj(Inl) 
890 
\tdx{inj_Inr} inj(Inr) 

104  891 

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

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

104  896 

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

902 

344  903 
\section{Generic packages and classical reasoning} 
9695  904 
HOL instantiates most of Isabelle's generic packages; see {\tt HOL/ROOT.ML} 
905 
for details. 

344  906 
\begin{itemize} 
9695  907 
\item Because it includes a general substitution rule, HOL instantiates the 
908 
tactic {\tt hyp_subst_tac}, which substitutes for an equality throughout a 

909 
subgoal and its hypotheses. 

344  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} 

9695  919 
HOL derives classical introduction rules for $\disj$ and~$\exists$, as well as 
920 
classical elimination rules for~$\imp$ and~$\bimp$, and the swap rule; recall 

921 
Fig.\ts\ref{hollemmas2} above. 

344  922 

9695  923 
The classical reasoner is set up as the structure {\tt Classical}. This 
924 
structure is open, so {\ML} identifiers such as {\tt step_tac}, {\tt 

925 
fast_tac}, {\tt best_tac}, etc., refer to it. HOL defines the following 

926 
classical rule sets: 

344  927 
\begin{ttbox} 
928 
prop_cs : claset 

929 
HOL_cs : claset 

930 
set_cs : claset 

931 
\end{ttbox} 

932 
\begin{ttdescription} 

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

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

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

936 

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

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

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

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

941 
once. 

942 

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

944 
quantifiers, subsets, comprehensions, unions and intersections, 

945 
complements, finite sets, images and ranges. 

946 
\end{ttdescription} 

947 
\noindent 

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

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

950 
for more discussion of classical proof methods. 

951 

952 

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

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

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

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

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

104  960 

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

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

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

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

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

967 
their representations are made explicitly. 

104  968 

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

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

344  971 
proved using \tdx{select_equality}. 
104  972 

287  973 
\begin{figure} 
315  974 
\index{*"< symbol} 
975 
\index{*"* symbol} 

344  976 
\index{*div symbol} 
977 
\index{*mod symbol} 

315  978 
\index{*"+ symbol} 
979 
\index{*" symbol} 

980 
\begin{constants} 

981 
\it symbol & \it metatype & \it priority & \it description \\ 

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

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

705  984 
\cdx{nat_case} & $[\alpha, nat\To\alpha, nat] \To\alpha$ 
315  985 
& & conditional\\ 
986 
\cdx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$ 

987 
& & primitive recursor\\ 

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

111  989 
\tt * & $[nat,nat]\To nat$ & Left 70 & multiplication \\ 
344  990 
\tt div & $[nat,nat]\To nat$ & Left 70 & division\\ 
991 
\tt mod & $[nat,nat]\To nat$ & Left 70 & modulus\\ 

111  992 
\tt + & $[nat,nat]\To nat$ & Left 65 & addition\\ 
993 
\tt  & $[nat,nat]\To nat$ & Left 65 & subtraction 

315  994 
\end{constants} 
104  995 
\subcaption{Constants and infixes} 
996 

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

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

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

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

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

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

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

287  1010 
m, \%j f. if(j<n,0,Suc(f(jn)))) 
104  1011 
\subcaption{Definitions} 
1012 
\end{ttbox} 

315  1013 
\caption{Defining {\tt nat}, the type of natural numbers} \label{holnat1} 
104  1014 
\end{figure} 
1015 

1016 

287  1017 
\begin{figure} \underscoreon 
104  1018 
\begin{ttbox} 
315  1019 
\tdx{nat_induct} [ P(0); !!k. [ P(k) ] ==> P(Suc(k)) ] ==> P(n) 
104  1020 

315  1021 
\tdx{Suc_not_Zero} Suc(m) ~= 0 
1022 
\tdx{inj_Suc} inj(Suc) 

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

104  1024 
\subcaption{Basic properties} 
1025 

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

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

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

104  1032 

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

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

104  1036 
\subcaption{Case analysis and primitive recursion} 
1037 

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

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

104  1041 

315  1042 
\tdx{less_not_sym} n<m > ~ m<n 
1043 
\tdx{less_not_refl} ~ n<n 

1044 
\tdx{not_less0} ~ n<0 

104  1045 

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

104  1048 

315  1049 
\tdx{less_linear} m<n  m=n  n<m 
104  1050 
\subcaption{The lessthan relation} 
1051 
\end{ttbox} 

344  1052 
\caption{Derived rules for {\tt nat}} \label{holnat2} 
104  1053 
\end{figure} 
1054 

1055 

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

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

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

1060 
The natural numbers are inductively generated by choosing an arbitrary 

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

344  1062 
usual, the isomorphisms between~\tydx{nat} and its representation are made 
315  1063 
explicitly. 
104  1064 

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

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

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

1069 
along arbitrary wellfounded relations. The corresponding theories are 

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

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

104  1072 

9695  1073 
Type~\tydx{nat} is postulated to belong to class~\cldx{ord}, which overloads 
1074 
$<$ and $\leq$ on the natural numbers. As of this writing, Isabelle provides 

1075 
no means of verifying that such overloading is sensible; there is no means of 

1076 
specifying the operators' properties and verifying that instances of the 

1077 
operators satisfy those properties. To be safe, the HOL theory includes no 

1078 
polymorphic axioms asserting general properties of $<$ and~$\leq$. 

104  1079 

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

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

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

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

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

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

1087 
and~\ref{holnat2}. 

104  1088 

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

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

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

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

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

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

1096 

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

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

104  1099 

287  1100 
\begin{figure} 
315  1101 
\index{#@{\tt\#} symbol} 
1102 
\index{"@@{\tt\at} symbol} 

1103 
\begin{constants} 

1104 
\it symbol & \it metatype & \it priority & \it description \\ 

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

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

1107 
list constructor \\ 

344  1108 
\cdx{null} & $\alpha list \To bool$ & & emptiness test\\ 
315  1109 
\cdx{hd} & $\alpha list \To \alpha$ & & head \\ 
1110 
\cdx{tl} & $\alpha list \To \alpha list$ & & tail \\ 

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

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

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

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

1115 
& & mapping functional\\ 

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

1117 
& & filter functional\\ 

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

1119 
& & forall functional\\ 

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

104  1121 
\beta]\To\beta] \To \beta$ 
315  1122 
& & list recursor 
1123 
\end{constants} 

306  1124 
\subcaption{Constants and infixes} 
1125 

1126 
\begin{center} \tt\frenchspacing 

1127 
\begin{tabular}{rrr} 

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

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

306  1131 
\rm finite list \\{} 
344  1132 
[$x$:$l$. $P$] & filter($\lambda x{.}P$, $l$) & 
315  1133 
\rm list comprehension 
306  1134 
\end{tabular} 
1135 
\end{center} 

1136 
\subcaption{Translations} 

104  1137 

1138 
\begin{ttbox} 

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

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

306  1143 
\subcaption{Induction and freeness} 
104  1144 
\end{ttbox} 
315  1145 
\caption{The theory \thydx{List}} \label{hollist} 
104  1146 
\end{figure} 
1147 

306  1148 
\begin{figure} 
1149 
\begin{ttbox}\makeatother 

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

315  1152 

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

315  1155 

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

315  1158 

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

315  1161 

471  1162 
\tdx{hd_Cons} hd(x#xs) = x 
1163 
\tdx{tl_Cons} tl(x#xs) = xs 

315  1164 

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

315  1167 

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

315  1170 

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

315  1173 

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

315  1176 

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

306  1179 
\end{ttbox} 
1180 
\caption{Rewrite rules for lists} \label{hollistsimps} 

1181 
\end{figure} 

104  1182 

315  1183 

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

1185 
\index{*list type} 

1186 

9695  1187 
HOL's definition of lists is an example of an experimental method for handling 
1188 
recursive data types. Figure~\ref{hollist} presents the theory \thydx{List}: 

1189 
the basic list operations with their types and properties. 

315  1190 

344  1191 
The \sdx{case} construct is defined by the following translation: 
315  1192 
{\dquotes 
1193 
\begin{eqnarray*} 

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

1197 
\end{array} 

1198 
& \equiv & 

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

1203 
that can express arbitrary total recursive functions. 

1204 

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

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

1207 

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

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

104  1210 

1211 

464  1212 
\section{Datatype declarations} 
1213 
\index{*datatype(} 

1214 

1215 
\underscoreon 

1216 

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

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

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

1220 
datatype} represents a compact way of doing this. 

1221 

1222 

1223 
\subsection{Foundations} 

1224 

1225 
A datatype declaration has the following general structure: 

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

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

464  1229 
\] 
580  1230 
where $\alpha_i$ are type variables, $C_i$ are distinct constructor names and 
464  1231 
$\tau_{ij}$ are one of the following: 
1232 
\begin{itemize} 

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

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

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

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

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

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

1239 
least one constructor must consist of only nonrecursive type 

1240 
components.} 

1241 
\end{itemize} 

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

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

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

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

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

1248 

464  1249 
The constructors are automatically defined as functions of their respective 
1250 
type: 

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

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

464  1258 
\item[\tt inject] They are injective: 
580  1259 
\[ (C_j(x_1,\dots,x_{k_j}) = C_j(y_1,\dots,y_{k_j})) = 
464  1260 
(x_1 = y_1 \land \dots \land x_{k_j} = y_{k_j}) 
1261 
\] 

1262 
\end{description} 

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

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

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

1266 
natural number 

1267 
\[ 

1268 
\begin{array}{lcl} 

580  1269 
\mbox{\it t\_ord}(C_1(x_1,\dots,x_{k_1})) & = & 0 \\ 
464  1270 
& \vdots & \\ 
580  1271 
\mbox{\it t\_ord}(C_m(x_1,\dots,x_{k_m})) & = & m1 
464  1272 
\end{array} 
1273 
\] 

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

1277 
\] 

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

1279 
\[ 

1280 
\infer{P(x)} 

1281 
{\begin{array}{lcl} 

1282 
\Forall x_1\dots x_{k_1}. 

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

580  1284 
\Imp & P(C_1(x_1,\dots,x_{k_1})) \\ 
464  1285 
& \vdots & \\ 
1286 
\Forall x_1\dots x_{k_m}. 

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

580  1288 
\Imp & P(C_m(x_1,\dots,x_{k_m})) 
464  1289 
\end{array}} 
1290 
\] 

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

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

1293 
all arguments of the recursive type. 

1294 

465  1295 
The type also comes with an \MLlike \sdx{case}construct: 
464  1296 
\[ 
1297 
\begin{array}{rrcl} 

580  1298 
\mbox{\tt case}~e~\mbox{\tt of} & C_1(x_{11},\dots,x_{1k_1}) & \To & e_1 \\ 
464  1299 
\vdots \\ 
580  1300 
\mid & C_m(x_{m1},\dots,x_{mk_m}) & \To & e_m 
464  1301 
\end{array} 
1302 
\] 

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

1304 
fixed, and nested patterns are not supported. 

1305 

1306 

1307 
\subsection{Defining datatypes} 

1308 

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

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

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

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

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

1314 
section. 

1315 

1316 
\begin{figure} 

1317 
\begin{rail} 

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

1319 
; 

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

1321 
; 

1322 
typ : typevarlist id 

1323 
 tid 

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

1324 
; 
464  1325 
typevarlist : ()  tid  '(' (tid + ',') ')' 
1326 
; 

1327 
\end{rail} 

1328 
\caption{Syntax of datatype declarations} 

1329 
\label{datatypegrammar} 

1330 
\end{figure} 

1331 

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

464  1336 
\begin{ttbox} 
465  1337 
val distinct : thm list 
464  1338 
val inject : thm list 
465  1339 
val induct : thm 
464  1340 
val cases : thm list 
1341 
val simps : thm list 

1342 
val induct_tac : string > int > tactic 

1343 
\end{ttbox} 

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

1346 
directions. 

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

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

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

1086  1354 
{\tt simps} for use with the simplifier. The tactic {\verb$induct_tac$~{\em 
1355 
var i}\/} applies structural induction over variable {\em var} to 

464  1356 
subgoal {\em i}. 
1357 

1358 

1359 
\subsection{Examples} 

1360 
