
1 %% $Id$ 

2 \chapter{HigherOrder Logic} 

3 \index{higherorder logic(} 

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

5 

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

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

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

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

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

11 has demonstrated that higherorder logic is widely applicable in many 

12 areas of mathematics and computer science, not just hardware 

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

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

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

16 to~{\ZF}. 

17 

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

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

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

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

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

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

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

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

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

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

28 

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

30 identifies objectlevel types with metalevel types, taking advantage of 

31 Isabelle's builtin typechecker. It identifies objectlevel functions 

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

33 and application. 

34 

35 These identifications allow Isabelle to support \HOL\ particularly 

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

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

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

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

40 % Gain experience by 

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

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

43 

44 

45 \begin{figure} 

46 \begin{constants} 

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

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

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

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

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

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

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

54 \end{constants} 

55 \subcaption{Constants} 

56 

57 \begin{constants} 

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

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

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

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

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

63 Hilbert description ($\varepsilon$) \\ 

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

65 universal quantifier ($\forall$) \\ 

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

67 existential quantifier ($\exists$) \\ 

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

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

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

71 least element 

72 \end{constants} 

73 \subcaption{Binders} 

74 

75 \begin{constants} 

76 \index{*"= symbol} 

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

78 \index{*" symbol} 

79 \index{*"""> symbol} 

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

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

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

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

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

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

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

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

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

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

90 \end{constants} 

91 \subcaption{Infixes} 

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

93 \end{figure} 

94 

95 

96 \begin{figure} 

97 \index{*let symbol} 

98 \index{*in symbol} 

99 \dquotes 

100 \[\begin{array}{rclcl} 

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

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

103 &  & 

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

105 &  & 

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

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

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

109 &  & term " = " term \\ 

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

111 &  & term " < " term \\ 

112 &  & term " <= " term \\ 

113 &  & "\ttilde\ " formula \\ 

114 &  & formula " \& " formula \\ 

115 &  & formula "  " formula \\ 

116 &  & formula " > " formula \\ 

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

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

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

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

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

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

123 \end{array} 

124 \] 

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

126 \end{figure} 

127 

128 

129 \section{Syntax} 

130 

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

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

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

134 $\neg(a=b)$. 

135 

136 \begin{warn} 

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

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

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

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

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

142 parentheses. 

143 \end{warn} 

144 

145 \subsection{Types and classes} 

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

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

148 particular the equality symbol and quantifiers are polymorphic over 

149 class \texttt{term}. 

150 

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

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

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

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

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

156 functions. 

157 

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

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

160 

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

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

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

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

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

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

167 

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

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

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

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

172 on natural numbers. 

173 

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

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

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

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

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

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

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

181 type $nat$. 

182 

183 \begin{warn} 

184 If resolution fails for no obvious reason, try setting 

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

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

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

188 

189 \index{unification!incompleteness of} 

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

191 guarantee to find instantiations for type variables automatically. Be 

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

193 possibly instantiating type variables. Setting 

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

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

196 \end{warn} 

197 

198 

199 \subsection{Binders} 

200 

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

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

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

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

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

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

207 

208 Existential quantification is defined by 

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

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

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

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

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

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

215 

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

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

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

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

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

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

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

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

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

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

226 

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

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

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

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

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

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

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

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

235 

236 \medskip All these binders have priority 10. 

237 

238 \begin{warn} 

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

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

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

242 \end{warn} 

243 

244 

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

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

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

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

249 definition, \tdx{Let_def}. 

250 

251 \HOL\ also defines the basic syntax 

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

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

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

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

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

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

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

259 

260 \begin{warn} 

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

262 quantifiers, which requires additional enclosing parentheses in the context 

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

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

265 else\dots})$. 

266 \end{warn} 

267 

268 \section{Rules of inference} 

269 

270 \begin{figure} 

271 \begin{ttbox}\makeatother 

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

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

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

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

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

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

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

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

280 \end{ttbox} 

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

282 \end{figure} 

283 

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

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

286 comments: 

287 \begin{ttdescription} 

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

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

290 equal. 

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

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

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

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

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

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

297 \end{ttdescription} 

298 

299 

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

301 \begin{ttbox}\makeatother 

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

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

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

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

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

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

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

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

310 

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

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

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

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

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

316 \end{ttbox} 

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

318 \end{figure} 

319 

320 

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

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

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

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

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

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

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

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

329 \begin{warn} 

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

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

332 or, better still, using highlevel tactics 

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

334 \end{warn} 

335 

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

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

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

339 

340 

341 \begin{figure} 

342 \begin{ttbox} 

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

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

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

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

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

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

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

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

351 \subcaption{Equality} 

352 

353 \tdx{TrueI} True 

354 \tdx{FalseE} False ==> P 

355 

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

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

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

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

360 

361 \tdx{disjI1} P ==> PQ 

362 \tdx{disjI2} Q ==> PQ 

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

364 

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

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

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

368 \subcaption{Propositional logic} 

369 

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

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

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

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

374 % 

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

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

377 \subcaption{Logical equivalence} 

378 

379 \end{ttbox} 

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

381 \end{figure} 

382 

383 

384 \begin{figure} 

385 \begin{ttbox}\makeatother 

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

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

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

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

390 

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

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

393 

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

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

396 ] ==> R 

397 

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

399 \subcaption{Quantifiers and descriptions} 

400 

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

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

403 \tdx{excluded_middle} ~P  P 

404 

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

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

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

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

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

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

411 \subcaption{Classical logic} 

412 

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

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

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

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

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

418 \subcaption{Conditionals} 

419 \end{ttbox} 

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

421 \end{figure} 

422 

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

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

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

426 conjunctions, implications, and universal quantifiers. 

427 

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

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

430 simplifying both sides of an equation. 

431 

432 The following simple tactics are occasionally useful: 

433 \begin{ttdescription} 

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

435 repeatedly to remove all outermost universal quantifiers and implications 

436 from subgoal $i$. 

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

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

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

440 \end{ttdescription} 

441 

442 

443 \begin{figure} 

444 \begin{center} 

445 \begin{tabular}{rrr} 

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

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

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

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

450 & insertion of element \\ 

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

452 & comprehension \\ 

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

454 & complement \\ 

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

456 & intersection over a set\\ 

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

458 & union over a set\\ 

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

460 &set of sets intersection \\ 

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

462 &set of sets union \\ 

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

464 & powerset \\[1ex] 

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

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

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

468 & bounded quantifiers 

469 \end{tabular} 

470 \end{center} 

471 \subcaption{Constants} 

472 

473 \begin{center} 

474 \begin{tabular}{llrrr} 

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

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

477 intersection over a type\\ 

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

479 union over a type 

480 \end{tabular} 

481 \end{center} 

482 \subcaption{Binders} 

483 

484 \begin{center} 

485 \index{*"`"` symbol} 

486 \index{*": symbol} 

487 \index{*"<"= symbol} 

488 \begin{tabular}{rrrr} 

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

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

491 & Left 90 & image \\ 

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

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

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

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

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

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

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

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

500 \end{tabular} 

501 \end{center} 

502 \subcaption{Infixes} 

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

504 \end{figure} 

505 

506 

507 \begin{figure} 

508 \begin{center} \tt\frenchspacing 

509 \index{*"! symbol} 

510 \begin{tabular}{rrr} 

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

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

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

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

515 \rm comprehension \\ 

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

517 \rm intersection \\ 

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

519 \rm union \\ 

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

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

522 \rm bounded $\forall$ \\ 

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

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

525 \end{tabular} 

526 \end{center} 

527 \subcaption{Translations} 

528 

529 \dquotes 

530 \[\begin{array}{rclcl} 

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

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

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

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

535 &  & term " `` " term \\ 

536 &  & term " Int " term \\ 

537 &  & term " Un " term \\ 

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

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

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

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

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

543 &  & term " : " term \\ 

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

545 &  & term " <= " term \\ 

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

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

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

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

550 \end{array} 

551 \] 

552 \subcaption{Full Grammar} 

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

554 \end{figure} 

555 

556 

557 \section{A formulation of set theory} 

558 Historically, higherorder logic gives a foundation for Russell and 

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

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

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

562 \begin{itemize} 

563 \item 

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

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

566 \item 

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

568 may be defined by absolute comprehension. 

569 \item 

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

571 have a more complex type. 

572 \end{itemize} 

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

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

575 denoting the universal set for the given type. 

576 

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

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

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

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

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

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

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

584 

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

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

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

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

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

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

591 

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

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

594 \begin{eqnarray*} 

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

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

597 \end{eqnarray*} 

598 

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

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

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

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

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

604 

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

606 \begin{eqnarray*} 

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

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

609 \end{eqnarray*} 

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

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

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

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

614 % 

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

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

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

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

619 

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

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

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

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

624 

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

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

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

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

629 

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

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

632 respectively. 

633 

634 

635 

636 \begin{figure} \underscoreon 

637 \begin{ttbox} 

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

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

640 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

659 \end{ttbox} 

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

661 \end{figure} 

662 

663 

664 \begin{figure} \underscoreon 

665 \begin{ttbox} 

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

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

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

669 

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

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

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

673 

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

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

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

677 \subcaption{Comprehension and Bounded quantifiers} 

678 

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

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

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

682 

683 \tdx{subset_refl} A <= A 

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

685 

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

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

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

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

690 

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

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

693 ] ==> P 

694 \subcaption{The subset and equality relations} 

695 \end{ttbox} 

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

697 \end{figure} 

698 

699 

700 \begin{figure} \underscoreon 

701 \begin{ttbox} 

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

703 

704 \tdx{insertI1} a : insert a B 

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

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

707 

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

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

710 

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

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

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

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

715 

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

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

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

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

720 

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

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

723 

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

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

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

727 

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

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

730 

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

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

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

734 

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

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

737 

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

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

740 

741 \tdx{rangeI} f x : range f 

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

743 \end{ttbox} 

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

745 \end{figure} 

746 

747 

748 \subsection{Axioms and rules of set theory} 

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

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

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

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

753 

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

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

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

757 and \texttt{range}. 

758 

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

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

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

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

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

764 

765 %\begin{figure} \underscoreon 

766 %\begin{ttbox} 

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

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

769 % 

770 %\tdx{Inv_injective} 

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

772 % 

773 % 

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

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

776 % 

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

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

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

780 % 

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

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

783 % 

784 %\tdx{inj_on_inverseI} 

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

786 %\tdx{inj_on_contraD} 

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

788 %\end{ttbox} 

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

790 %\end{figure} 

791 

792 

793 \begin{figure} \underscoreon 

794 \begin{ttbox} 

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

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

797 

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

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

800 

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

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

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

804 

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

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

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

808 \end{ttbox} 

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

810 \end{figure} 

811 

812 

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

814 \begin{ttbox} 

815 \tdx{Int_absorb} A Int A = A 

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

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

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

819 

820 \tdx{Un_absorb} A Un A = A 

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

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

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

824 

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

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

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

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

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

830 

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

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

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

834 

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

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

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

838 \end{ttbox} 

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

840 \end{figure} 

841 

842 

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

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

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

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

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

848 strictly necessary but yield more natural proofs. Similarly, 

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

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

851 proofs pertaining to set theory. 

852 

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

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

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

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

857 

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

859 include commutative, associative and distributive laws involving unions, 

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

861 HOL/equalities.ML}. 

862 

863 \begin{warn} 

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

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

866 \end{warn} 

867 

868 \begin{figure} 

869 \begin{center} 

870 \begin{tabular}{rrr} 

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

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

873 & injective/surjective \\ 

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

875 & injective over subset\\ 

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

877 \end{tabular} 

878 \end{center} 

879 

880 \underscoreon 

881 \begin{ttbox} 

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

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

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

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

886 \end{ttbox} 

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

888 \end{figure} 

889 

890 \subsection{Properties of functions}\nopagebreak 

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

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

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

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

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

896 

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

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

899 

900 \section{Generic packages} 

901 \label{sec:HOL:genericpackages} 

902 

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

904 simplifier and the classical reasoner. 

905 

906 \subsection{Simplification and substitution} 

907 

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

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

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

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

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

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

914 simplification rules. 

915 

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

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

918 and simplification. 

919 

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

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

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

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

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

925 \end{warn} 

926 

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

928 of nontermination or because its lefthand side is too flexible  

929 then you might try \texttt{stac}: 

930 \begin{ttdescription} 

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

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

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

934 may be necessary to select the desired ones. 

935 

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

937 additional (first) subgoal. 

938 \end{ttdescription} 

939 

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

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

942 \HOL's general substitution rule. 

943 

944 \subsubsection{Case splitting} 

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

946 

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

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

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

950 expressed by the theorem \tdx{split_if}: 

951 $$ 

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

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

954 \eqno{(*)} 

955 $$ 

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

957 \[ 

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

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

960 \] 

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

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

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

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

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

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

967 simpset, as in 

968 \begin{ttbox} 

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

970 \end{ttbox} 

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

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

973 \texttt{if} have been eliminated. 

974 

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

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

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

978 the inverse of \texttt{addsplits}: 

979 \begin{ttbox} 

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

981 \end{ttbox} 

982 

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

984 \[ 

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

986 \] 

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

988 right form because internally the lefthand side is 

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

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

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

992 

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

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

995 \begin{ttbox} 

996 \ttindexbold{Addsplits}: thm list > unit 

997 \ttindexbold{Delsplits}: thm list > unit 

998 \end{ttbox} 

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

1000 

1001 \subsection{Classical reasoning} 

1002 

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

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

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

1006 

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

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

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

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

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

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

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

1014 

1015 

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

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

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

1019 introducing new types in general. The most important type 

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

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

1022 

1023 

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

1025 \label{subsec:prodsum} 

1026 

1027 \begin{figure}[htbp] 

1028 \begin{constants} 

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

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

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

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

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

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

1035 & & generalized projection\\ 

1036 \cdx{Sigma} & 

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

1038 & general sum of sets 

1039 \end{constants} 

1040 \begin{ttbox}\makeatletter 

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

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

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

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

1045 

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

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

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

1049 

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

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

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

1053 

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

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

1056 

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

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

1059 \end{ttbox} 

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

1061 \end{figure} 

1062 

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

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

1065 tuples are simulated by pairs nested to the right: 

1066 \begin{center} 

1067 \begin{tabular}{cc} 

1068 external & internal \\ 

1069 \hline 

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

1071 \hline 

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

1073 \end{tabular} 

1074 \end{center} 

1075 In addition, it is possible to use tuples 

1076 as patterns in abstractions: 

1077 \begin{center} 

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

1079 \end{center} 

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

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

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

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

1084 \begin{warn} 

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

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

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

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

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

1090 \end{warn} 

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

1092 variable binding construct which is internally described by a 

1093 $\lambda$abstraction. Some important examples are 

1094 \begin{description} 

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

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

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

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

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

1100 \end{description} 

1101 

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

1103 \begin{ttdescription} 

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

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

1106 each component. A simple example: 

1107 \begin{ttbox} 

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

1109 by(split_all_tac 1); 

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

1111 \end{ttbox} 

1112 \end{ttdescription} 

1113 

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

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

1116 \begin{ttbox} 

1117 \tdx{unit_eq} u = () 

1118 \end{ttbox} 

1119 \bigskip 

1120 

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

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

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

1124 

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

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

1127 respective theory files. 

1128 

1129 \begin{figure} 

1130 \begin{constants} 

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

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

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

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

1135 & & conditional 

1136 \end{constants} 

1137 \begin{ttbox}\makeatletter 

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

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

1140 % 

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

1142 

1143 \tdx{inj_Inl} inj Inl 

1144 \tdx{inj_Inr} inj Inr 

1145 

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

1147 

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

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

1150 

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

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

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

1154 \end{ttbox} 

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

1156 \end{figure} 

1157 

1158 \begin{figure} 

1159 \index{*"< symbol} 

1160 \index{*"* symbol} 

1161 \index{*div symbol} 

1162 \index{*mod symbol} 

1163 \index{*"+ symbol} 

1164 \index{*" symbol} 

1165 \begin{constants} 

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

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

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

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

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

1171 % & & primitive recursor\\ 

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

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

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

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

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

1177 \end{constants} 

1178 \subcaption{Constants and infixes} 

1179 

1180 \begin{ttbox}\makeatother 

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

1182 

1183 \tdx{Suc_not_Zero} Suc m ~= 0 

1184 \tdx{inj_Suc} inj Suc 

1185 \tdx{n_not_Suc_n} n~=Suc n 

1186 \subcaption{Basic properties} 

1187 \end{ttbox} 

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

1189 \end{figure} 

1190 

1191 

1192 \begin{figure} 

1193 \begin{ttbox}\makeatother 

1194 0+n = n 

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

1196 

1197 m0 = m 

1198 0n = n 

1199 Suc(m)Suc(n) = mn 

1200 

1201 0*n = 0 

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

1203 

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

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

1206 

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

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

1209 \end{ttbox} 

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

1211 \end{figure} 

1212 

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

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

1215 

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

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

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

1219 natural numbers are inductively generated by choosing an arbitrary individual 

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

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

1222 

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

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

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

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

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

1228 

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

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

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

1232 proved include commutative, associative, distributive, identity and 

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

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

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

1236 

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

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

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

1240 the standard convention. 

1241 \begin{ttbox} 

1242 \sdx{primrec} 

1243 "0 + n = n" 

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

1245 \end{ttbox} 

1246 There is also a \sdx{case}construct 

1247 of the form 

1248 \begin{ttbox} 

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

1250 \end{ttbox} 

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

1252 the order of the two cases. 

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

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

1255 

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

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

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

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

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

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

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

1263 

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

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

1266 theorem \tdx{less_induct}: 

1267 \begin{ttbox} 

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

1269 \end{ttbox} 

1270 

1271 

1272 Reasoning about arithmetic inequalities can be tedious. Fortunately HOL 

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

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

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

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

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

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

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

1280 subformulae are ignored unless they are positive universal or negative 

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

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

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

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

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

1286 

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

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

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

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

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

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

1293 

1294 \begin{figure} 

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

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

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

1298 \index{*"! symbol} 

1299 \begin{constants} 

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

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

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

1303 list constructor \\ 

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

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

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

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

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

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

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

1311 & & apply to all\\ 

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

1313 & & filter functional\\ 

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

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

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

1317 & iteration \\ 

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

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

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

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

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

1323 take or drop a prefix \\ 

1324 \cdx{takeWhile},\\ 

1325 \cdx{dropWhile} & 

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

1327 take or drop a prefix 

1328 \end{constants} 

1329 \subcaption{Constants and infixes} 

1330 

1331 \begin{center} \tt\frenchspacing 

1332 \begin{tabular}{rrr} 

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

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

1335 \rm finite list \\{} 

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

1337 \rm list comprehension 

1338 \end{tabular} 

1339 \end{center} 

1340 \subcaption{Translations} 

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

1342 \end{figure} 

1343 

1344 

1345 \begin{figure} 

1346 \begin{ttbox}\makeatother 

1347 null [] = True 

1348 null (x#xs) = False 

1349 

1350 hd (x#xs) = x 

1351 tl (x#xs) = xs 

1352 tl [] = [] 

1353 

1354 [] @ ys = ys 

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

1356 

1357 map f [] = [] 

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

1359 

1360 filter P [] = [] 

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

1362 

1363 set [] = \ttlbrace\ttrbrace 

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

1365 

1366 x mem [] = False 

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

1368 

1369 foldl f a [] = a 

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

1371 

1372 concat([]) = [] 

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

1374 

1375 rev([]) = [] 

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

1377 

1378 length([]) = 0 

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

1380 

1381 xs!0 = hd xs 

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

1383 

1384 take n [] = [] 

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

1386 

1387 drop n [] = [] 

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

1389 

1390 takeWhile P [] = [] 

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

1392 

1393 dropWhile P [] = [] 

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

1395 \end{ttbox} 

1396 \caption{Recursions equations for list processing functions} 

1397 \label{fig:HOL:listsimps} 

1398 \end{figure} 

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

1400 

1401 

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

1403 \label{subsec:list} 

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

1405 

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

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

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

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

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

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

1412 \begin{center}\tt 

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

1414 \end{center} 

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

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

1417 \[ 

1418 \begin{array}{l} 

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

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

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

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

1423 \end{array} 

1424 \] 

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

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

1427 

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

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

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

1431 

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

1433 

1434 

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

1436 

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

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

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

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

1441 syntactic abbreviations that have no logical meaning. 

1442 

1443 \begin{warn} 

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

1445 unsound, because $\exists x. x=x$ is a theorem \cite[\S7]{paulsonCOLOG}. 

1446 \end{warn} 

1447 A \bfindex{type definition} identifies the new type with a subset of 

1448 an existing type. More precisely, the new type is defined by 

1449 exhibiting an existing type~$\tau$, a set~$A::\tau\,set$, and a 

1450 theorem of the form $x:A$. Thus~$A$ is a nonempty subset of~$\tau$, 

1451 and the new type denotes this subset. New functions are defined that 

1452 establish an isomorphism between the new type and the subset. If 

1453 type~$\tau$ involves type variables $\alpha@1$, \ldots, $\alpha@n$, 

1454 then the type definition creates a type constructor 

1455 $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular type. 

1456 

1457 \begin{figure}[htbp] 

1458 \begin{rail} 

1459 typedef : 'typedef' ( ()  '(' name ')') type '=' set witness; 

1460 

1461 type : typevarlist name ( ()  '(' infix ')' ); 

1462 set : string; 

1463 witness : ()  '(' id ')'; 

1464 \end{rail} 

1465 \caption{Syntax of type definitions} 

1466 \label{fig:HOL:typedef} 

1467 \end{figure} 

1468 

1469 The syntax for type definitions is shown in Fig.~\ref{fig:HOL:typedef}. For 

1470 the definition of `typevarlist' and `infix' see 

1471 \iflabelundefined{chap:classical} 

1472 {the appendix of the {\em Reference Manual\/}}% 

1473 {Appendix~\ref{app:TheorySyntax}}. The remaining nonterminals have the 

1474 following meaning: 

1475 \begin{description} 

1476 \item[\it type:] the new type constructor $(\alpha@1,\dots,\alpha@n)ty$ with 

1477 optional infix annotation. 

1478 \item[\it name:] an alphanumeric name $T$ for the type constructor 

1479 $ty$, in case $ty$ is a symbolic name. Defaults to $ty$. 

1480 \item[\it set:] the representing subset $A$. 

1481 \item[\it witness:] name of a theorem of the form $a:A$ proving 

1482 nonemptiness. It can be omitted in case Isabelle manages to prove 

1483 nonemptiness automatically. 

1484 \end{description} 

1485 If all context conditions are met (no duplicate type variables in 

1486 `typevarlist', no extra type variables in `set', and no free term variables 

1487 in `set'), the following components are added to the theory: 

1488 \begin{itemize} 

1489 \item a type $ty :: (term,\dots,term)term$ 

1490 \item constants 

1491 \begin{eqnarray*} 

1492 T &::& \tau\;set \\ 

1493 Rep_T &::& (\alpha@1,\dots,\alpha@n)ty \To \tau \\ 

1494 Abs_T &::& \tau \To (\alpha@1,\dots,\alpha@n)ty 

1495 \end{eqnarray*} 

1496 \item a definition and three axioms 

1497 \[ 

1498 \begin{array}{ll} 

1499 T{\tt_def} & T \equiv A \\ 

1500 {\tt Rep_}T & Rep_T\,x \in T \\ 

1501 {\tt Rep_}T{\tt_inverse} & Abs_T\,(Rep_T\,x) = x \\ 

1502 {\tt Abs_}T{\tt_inverse} & y \in T \Imp Rep_T\,(Abs_T\,y) = y 

1503 \end{array} 

1504 \] 

1505 stating that $(\alpha@1,\dots,\alpha@n)ty$ is isomorphic to $A$ by $Rep_T$ 

1506 and its inverse $Abs_T$. 

1507 \end{itemize} 

1508 Below are two simple examples of \HOL\ type definitions. Nonemptiness 

1509 is proved automatically here. 

1510 \begin{ttbox} 

1511 typedef unit = "{\ttlbrace}True{\ttrbrace}" 

1512 

1513 typedef (prod) 

1514 ('a, 'b) "*" (infixr 20) 

1515 = "{\ttlbrace}f . EX (a::'a) (b::'b). f = (\%x y. x = a & y = b){\ttrbrace}" 

1516 \end{ttbox} 

1517 

1518 Type definitions permit the introduction of abstract data types in a safe 

1519 way, namely by providing models based on already existing types. Given some 

1520 abstract axiomatic description $P$ of a type, this involves two steps: 

1521 \begin{enumerate} 

1522 \item Find an appropriate type $\tau$ and subset $A$ which has the desired 

1523 properties $P$, and make a type definition based on this representation. 

1524 \item Prove that $P$ holds for $ty$ by lifting $P$ from the representation. 

1525 \end{enumerate} 

1526 You can now forget about the representation and work solely in terms of the 

1527 abstract properties $P$. 

1528 

1529 \begin{warn} 

1530 If you introduce a new type (constructor) $ty$ axiomatically, i.e.\ by 

1531 declaring the type and its operations and by stating the desired axioms, you 

1532 should make sure the type has a nonempty model. You must also have a clause 

1533 \par 

1534 \begin{ttbox} 

1535 arities \(ty\) :: (term,\thinspace\(\dots\),{\thinspace}term){\thinspace}term 

1536 \end{ttbox} 

1537 in your theory file to tell Isabelle that $ty$ is in class \texttt{term}, the 

1538 class of all \HOL\ types. 

1539 \end{warn} 

1540 

1541 

1542 \section{Records} 

1543 

1544 At a first approximation, records are just a minor generalisation of tuples, 

1545 where components may be addressed by labels instead of just position (think of 

1546 {\ML}, for example). The version of records offered by Isabelle/HOL is 

1547 slightly more advanced, though, supporting \emph{extensible record schemes}. 

1548 This admits operations that are polymorphic with respect to record extension, 

1549 yielding ``objectoriented'' effects like (single) inheritance. See also 

1550 \cite{NaraschewskiWenzel:1998:TPHOL} for more details on objectoriented 

1551 verification and record subtyping in HOL. 

1552 

1553 

1554 \subsection{Basics} 

1555 

1556 Isabelle/HOL supports fixed and schematic records both at the level of terms 

1557 and types. The concrete syntax is as follows: 

1558 

1559 \begin{center} 

1560 \begin{tabular}{lll} 

1561 & record terms & record types \\ \hline 

1562 fixed & $\record{x = a\fs y = b}$ & $\record{x \ty A\fs y \ty B}$ \\ 

1563 schematic & $\record{x = a\fs y = b\fs \more = m}$ & 

1564 $\record{x \ty A\fs y \ty B\fs \more \ty M}$ \\ 

1565 \end{tabular} 

1566 \end{center} 

1567 

1568 \noindent The \textsc{ascii} representation of $\record{x = a}$ is \texttt{( x = a )}. 

1569 

1570 A fixed record $\record{x = a\fs y = b}$ has field $x$ of value $a$ and field 

1571 $y$ of value $b$. The corresponding type is $\record{x \ty A\fs y \ty B}$, 

1572 assuming that $a \ty A$ and $b \ty B$. 

1573 

1574 A record scheme like $\record{x = a\fs y = b\fs \more = m}$ contains fields 

1575 $x$ and $y$ as before, but also possibly further fields as indicated by the 

1576 ``$\more$'' notation (which is actually part of the syntax). The improper 

1577 field ``$\more$'' of a record scheme is called the \emph{more part}. 

1578 Logically it is just a free variable, which is occasionally referred to as 

1579 \emph{row variable} in the literature. The more part of a record scheme may 

1580 be instantiated by zero or more further components. For example, above scheme 

1581 might get instantiated to $\record{x = a\fs y = b\fs z = c\fs \more = m'}$, 

1582 where $m'$ refers to a different more part. Fixed records are special 

1583 instances of record schemes, where ``$\more$'' is properly terminated by the 

1584 $() :: unit$ element. Actually, $\record{x = a\fs y = b}$ is just an 

1585 abbreviation for $\record{x = a\fs y = b\fs \more = ()}$. 

1586 

1587 \medskip 

1588 

1589 There are two key features that make extensible records in a simply typed 

1590 language like HOL feasible: 

1591 \begin{enumerate} 

1592 \item the more part is internalised, as a free term or type variable, 

1593 \item field names are externalised, they cannot be accessed within the logic 

1594 as firstclass values. 

1595 \end{enumerate} 

1596 

1597 \medskip 

1598 

1599 In Isabelle/HOL record types have to be defined explicitly, fixing their field 

1600 names and types, and their (optional) parent record (see 

1601 \S\ref{sec:HOL:recorddef}). Afterwards, records may be formed using above 

1602 syntax, while obeying the canonical order of fields as given by their 

1603 declaration. The record package also provides several operations like 

1604 selectors and updates (see \S\ref{sec:HOL:recordops}), together with 

1605 characteristic properties (see \S\ref{sec:HOL:recordthms}). 

1606 

1607 There is an example theory demonstrating most basic aspects of extensible 

1608 records (see theory \texttt{HOL/ex/Points} in the Isabelle sources). 

1609 

1610 

1611 \subsection{Defining records}\label{sec:HOL:recorddef} 

1612 

1613 The theory syntax for record type definitions is shown in 

1614 Fig.~\ref{fig:HOL:record}. For the definition of `typevarlist' and `type' see 

1615 \iflabelundefined{chap:classical} 

1616 {the appendix of the {\em Reference Manual\/}}% 

1617 {Appendix~\ref{app:TheorySyntax}}. 

1618 

1619 \begin{figure}[htbp] 

1620 \begin{rail} 

1621 record : 'record' typevarlist name '=' parent (field +); 

1622 

1623 parent : ( ()  type '+'); 

1624 field : name '::' type; 

1625 \end{rail} 

1626 \caption{Syntax of record type definitions} 

1627 \label{fig:HOL:record} 

1628 \end{figure} 

1629 

1630 A general \ttindex{record} specification is of the following form: 

1631 \[ 

1632 \mathtt{record}~(\alpha@1, \dots, \alpha@n) \, t ~=~ 

1633 (\tau@1, \dots, \tau@m) \, s ~+~ c@1 :: \sigma@1 ~ \dots ~ c@l :: \sigma@l 

1634 \] 

1635 where $\vec\alpha@n$ are distinct type variables, and $\vec\tau@m$, 

1636 $\vec\sigma@l$ are types containing at most variables from $\vec\alpha@n$. 

1637 Type constructor $t$ has to be new, while $s$ has to specify an existing 

1638 record type. Furthermore, the $\vec c@l$ have to be distinct field names. 

1639 There has to be at least one field. 

1640 

1641 In principle, field names may never be shared with other records. This is no 

1642 actual restriction in practice, since $\vec c@l$ are internally declared 

1643 within a separate name space qualified by the name $t$ of the record. 

1644 

1645 \medskip 

1646 

1647 Above definition introduces a new record type $(\vec\alpha@n) \, t$ by 

1648 extending an existing one $(\vec\tau@m) \, s$ by new fields $\vec c@l \ty 

1649 \vec\sigma@l$. The parent record specification is optional, by omitting it 

1650 $t$ becomes a \emph{root record}. The hierarchy of all records declared 

1651 within a theory forms a forest structure, i.e.\ a set of trees, where any of 

1652 these is rooted by some root record. 

1653 

1654 For convenience, $(\vec\alpha@n) \, t$ is made a type abbreviation for the 

1655 fixed record type $\record{\vec c@l \ty \vec\sigma@l}$, and $(\vec\alpha@n, 

1656 \zeta) \, t_scheme$ is made an abbreviation for $\record{\vec c@l \ty 

1657 \vec\sigma@l\fs \more \ty \zeta}$. 

1658 

1659 \medskip 

1660 

1661 The following simple example defines a root record type $point$ with fields $x 

1662 \ty nat$ and $y \ty nat$, and record type $cpoint$ by extending $point$ with 

1663 an additional $colour$ component. 

1664 

1665 \begin{ttbox} 

1666 record point = 

1667 x :: nat 

1668 y :: nat 

1669 

1670 record cpoint = point + 

1671 colour :: string 

1672 \end{ttbox} 

1673 

1674 

1675 \subsection{Record operations}\label{sec:HOL:recordops} 

1676 

1677 Any record definition of the form presented above produces certain standard 

1678 operations. Selectors and updates are provided for any field, including the 

1679 improper one ``$more$''. There are also cumulative record constructor 

1680 functions. 

1681 

1682 To simplify the presentation below, we first assume that $(\vec\alpha@n) \, t$ 

1683 is a root record with fields $\vec c@l \ty \vec\sigma@l$. 

1684 

1685 \medskip 

1686 

1687 \textbf{Selectors} and \textbf{updates} are available for any field (including 

1688 ``$more$'') as follows: 

1689 \begin{matharray}{lll} 

1690 c@i & \ty & \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \To \sigma@i \\ 

1691 c@i_update & \ty & \sigma@i \To \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \To 

1692 \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} 

1693 \end{matharray} 

1694 

1695 There is some special syntax for updates: $r \, \record{x \asn a}$ abbreviates 

1696 term $x_update \, a \, r$. Repeated updates are also supported: $r \, 

1697 \record{x \asn a} \, \record{y \asn b} \, \record{z \asn c}$ may be written as 

1698 $r \, \record{x \asn a\fs y \asn b\fs z \asn c}$. Note that because of 

1699 postfix notation the order of fields shown here is reverse than in the actual 

1700 term. This might lead to confusion in conjunction with proof tools like 

1701 ordered rewriting. 

1702 

1703 Since repeated updates are just function applications, fields may be freely 

1704 permuted in $\record{x \asn a\fs y \asn b\fs z \asn c}$, as far as the logic 

1705 is concerned. Thus commutativity of updates can be proven within the logic 

1706 for any two fields, but not as a general theorem: fields are not firstclass 

1707 values. 

1708 

1709 \medskip 

1710 

1711 \textbf{Make} operations provide cumulative record constructor functions: 

1712 \begin{matharray}{lll} 

1713 make & \ty & \vec\sigma@l \To \record{\vec c@l \ty \vec \sigma@l} \\ 

1714 make_scheme & \ty & \vec\sigma@l \To 

1715 \zeta \To \record{\vec c@l \ty \vec \sigma@l, \more \ty \zeta} \\ 

1716 \end{matharray} 

1717 \noindent 

1718 These functions are curried. The corresponding definitions in terms of actual 

1719 record terms are part of the standard simpset. Thus $point\dtt make\,a\,b$ 

1720 rewrites to $\record{x = a\fs y = b}$. 

1721 

1722 \medskip 

1723 

1724 Any of above selector, update and make operations are declared within a local 

1725 name space prefixed by the name $t$ of the record. In case that different 

1726 records share base names of fields, one has to qualify names explicitly (e.g.\ 

1727 $t\dtt c@i_update$). This is recommended especially for operations like 

1728 $make$ or $update_more$ that always have the same base name. Just use $t\dtt 

1729 make$ etc.\ to avoid confusion. 

1730 

1731 \bigskip 

1732 

1733 We reconsider the case of nonroot records, which are derived of some parent 

1734 record. In general, the latter may depend on another parent as well, 

1735 resulting in a list of \emph{ancestor records}. Appending the lists of fields 

1736 of all ancestors results in a certain field prefix. The record package 

1737 automatically takes care of this by lifting operations over this context of 

1738 ancestor fields. Assuming that $(\vec\alpha@n) \, t$ has ancestor fields 

1739 $\vec d@k \ty \vec\rho@k$, selectors will get the following types: 

1740 \begin{matharray}{lll} 

1741 c@i & \ty & \record{\vec d@k \ty \vec\rho@k, \vec c@l \ty \vec \sigma@l, \more \ty \zeta} 

1742 \To \sigma@i 

1743 \end{matharray} 

1744 \noindent 

1745 Update and make operations are analogous. 

1746 

1747 

1748 \subsection{Proof tools}\label{sec:HOL:recordthms} 

1749 

1750 The record package provides the following proof rules for any record type $t$. 

1751 \begin{enumerate} 

1752 

1753 \item Standard conversions (selectors or updates applied to record constructor 

1754 terms, make function definitions) are part of the standard simpset (via 

1755 \texttt{addsimps}). 

1756 

1757 \item Inject equations of a form analogous to $((x, y) = (x', y')) \equiv x=x' 

1758 \conj y=y'$ are made part of the standard simpset and claset (via 

1759 \texttt{addIffs}). 

1760 

1761 \item A tactic for record field splitting (\ttindex{record_split_tac}) is made 

1762 part of the standard claset (via \texttt{addSWrapper}). This tactic is 

1763 based on rules analogous to $(\All x PROP~P~x) \equiv (\All{a~b} PROP~P(a, 

1764 b))$ for any field. 

1765 \end{enumerate} 

1766 

1767 The first two kinds of rules are stored within the theory as $t\dtt simps$ and 

1768 $t\dtt iffs$, respectively. In some situations it might be appropriate to 

1769 expand the definitions of updates: $t\dtt updates$. Following a new trend in 

1770 Isabelle system architecture, these names are \emph{not} bound at the {\ML} 

1771 level, though. 

1772 

1773 \medskip 

1774 

1775 The example theory \texttt{HOL/ex/Points} demonstrates typical proofs 

1776 concerning records. The basic idea is to make \ttindex{record_split_tac} 

1777 expand quantified record variables and then simplify by the conversion rules. 

1778 By using a combination of the simplifier and classical prover together with 

1779 the default simpset and claset, record problems should be solved with a single 

1780 stroke of \texttt{Auto_tac} or \texttt{Force_tac}. 

1781 

1782 

1783 \section{Datatype definitions} 

1784 \label{sec:HOL:datatype} 

1785 \index{*datatype(} 

1786 

1787 Inductive datatypes, similar to those of \ML, frequently appear in 

1788 applications of Isabelle/HOL. In principle, such types could be defined by 

1789 hand via \texttt{typedef} (see \S\ref{sec:typedef}), but this would be far too 

1790 tedious. The \ttindex{datatype} definition package of \HOL\ automates such 

1791 chores. It generates an appropriate \texttt{typedef} based on a least 

1792 fixedpoint construction, and proves freeness theorems and induction rules, as 

1793 well as theorems for recursion and case combinators. The user just has to 

1794 give a simple specification of new inductive types using a notation similar to 

1795 {\ML} or Haskell. 

1796 

1797 The current datatype package can handle both mutual and indirect recursion. 

1798 It also offers to represent existing types as datatypes giving the advantage 

1799 of a more uniform view on standard theories. 

1800 

1801 

1802 \subsection{Basics} 

1803 \label{subsec:datatype:basics} 

1804 

1805 A general \texttt{datatype} definition is of the following form: 

1806 \[ 

1807 \begin{array}{llcl} 

1808 \mathtt{datatype} & (\alpha@1,\ldots,\alpha@h)t@1 & = & 

1809 C^1@1~\tau^1@{1,1}~\ldots~\tau^1@{1,m^1@1} ~\mid~ \ldots ~\mid~ 

1810 C^1@{k@1}~\tau^1@{k@1,1}~\ldots~\tau^1@{k@1,m^1@{k@1}} \\ 

1811 & & \vdots \\ 

1812 \mathtt{and} & (\alpha@1,\ldots,\alpha@h)t@n & = & 

1813 C^n@1~\tau^n@{1,1}~\ldots~\tau^n@{1,m^n@1} ~\mid~ \ldots ~\mid~ 

1814 C^n@{k@n}~\tau^n@{k@n,1}~\ldots~\tau^n@{k@n,m^n@{k@n}} 

1815 \end{array} 

1816 \] 

1817 where $\alpha@i$ are type variables, $C^j@i$ are distinct constructor 

1818 names and $\tau^j@{i,i'}$ are {\em admissible} types containing at 

1819 most the type variables $\alpha@1, \ldots, \alpha@h$. A type $\tau$ 

1820 occurring in a \texttt{datatype} definition is {\em admissible} iff 

1821 \begin{itemize} 

1822 \item $\tau$ is nonrecursive, i.e.\ $\tau$ does not contain any of the 

1823 newly defined type constructors $t@1,\ldots,t@n$, or 

1824 \item $\tau = (\alpha@1,\ldots,\alpha@h)t@{j'}$ where $1 \leq j' \leq n$, or 

1825 \item $\tau = (\tau'@1,\ldots,\tau'@{h'})t'$, where $t'$ is 

1826 the type constructor of an already existing datatype and $\tau'@1,\ldots,\tau'@{h'}$ 

1827 are admissible types. 

1828 \end{itemize} 

1829 If some $(\alpha@1,\ldots,\alpha@h)t@{j'}$ occurs in a type $\tau^j@{i,i'}$ 

1830 of the form 

1831 \[ 

1832 (\ldots,\ldots ~ (\alpha@1,\ldots,\alpha@h)t@{j'} ~ \ldots,\ldots)t' 

1833 \] 

1834 this is called a {\em nested} (or \emph{indirect}) occurrence. A very simple 

1835 example of a datatype is the type \texttt{list}, which can be defined by 

1836 \begin{ttbox} 

1837 datatype 'a list = Nil 

1838  Cons 'a ('a list) 

1839 \end{ttbox} 

1840 Arithmetic expressions \texttt{aexp} and boolean expressions \texttt{bexp} can be modelled 

1841 by the mutually recursive datatype definition 

1842 \begin{ttbox} 

1843 datatype 'a aexp = If_then_else ('a bexp) ('a aexp) ('a aexp) 

1844  Sum ('a aexp) ('a aexp) 

1845  Diff ('a aexp) ('a aexp) 

1846  Var 'a 

1847  Num nat 

1848 and 'a bexp = Less ('a aexp) ('a aexp) 

1849  And ('a bexp) ('a bexp) 

1850  Or ('a bexp) ('a bexp) 

1851 \end{ttbox} 

1852 The datatype \texttt{term}, which is defined by 

1853 \begin{ttbox} 

1854 datatype ('a, 'b) term = Var 'a 

1855  App 'b ((('a, 'b) term) list) 

1856 \end{ttbox} 

1857 is an example for a datatype with nested recursion. 

1858 

1859 \medskip 

1860 

1861 Types in HOL must be nonempty. Each of the new datatypes 

1862 $(\alpha@1,\ldots,\alpha@h)t@j$ with $1 \le j \le n$ is nonempty iff it has a 

1863 constructor $C^j@i$ with the following property: for all argument types 

1864 $\tau^j@{i,i'}$ of the form $(\alpha@1,\ldots,\alpha@h)t@{j'}$ the datatype 

1865 $(\alpha@1,\ldots,\alpha@h)t@{j'}$ is nonempty. 

1866 

1867 If there are no nested occurrences of the newly defined datatypes, obviously 

1868 at least one of the newly defined datatypes $(\alpha@1,\ldots,\alpha@h)t@j$ 

1869 must have a constructor $C^j@i$ without recursive arguments, a \emph{base 

1870 case}, to ensure that the new types are nonempty. If there are nested 

1871 occurrences, a datatype can even be nonempty without having a base case 

1872 itself. Since \texttt{list} is a nonempty datatype, \texttt{datatype t = C (t 

1873 list)} is nonempty as well. 

1874 

1875 

1876 \subsubsection{Freeness of the constructors} 

1877 

1878 The datatype constructors are automatically defined as functions of their 

1879 respective type: 

1880 \[ C^j@i :: [\tau^j@{i,1},\dots,\tau^j@{i,m^j@i}] \To (\alpha@1,\dots,\alpha@h)t@j \] 

1881 These functions have certain {\em freeness} properties. They construct 

1882 distinct values: 

1883 \[ 

1884 C^j@i~x@1~\dots~x@{m^j@i} \neq C^j@{i'}~y@1~\dots~y@{m^j@{i'}} \qquad 

1885 \mbox{for all}~ i \neq i'. 

1886 \] 

1887 The constructor functions are injective: 

1888 \[ 

1889 (C^j@i~x@1~\dots~x@{m^j@i} = C^j@i~y@1~\dots~y@{m^j@i}) = 

1890 (x@1 = y@1 \land \dots \land x@{m^j@i} = y@{m^j@i}) 

1891 \] 

1892 Because the number of distinctness inequalities is quadratic in the number of 

1893 constructors, a different representation is used if there are $7$ or more of 

1894 them. In that case every constructor term is mapped to a natural number: 

1895 \[ 

1896 t@j_ord \, (C^j@i \, x@1 \, \dots \, x@{m^j@i}) = i  1 

1897 \] 

1898 Then distinctness of constructor terms is expressed by: 

1899 \[ 

1900 t@j_ord \, x \neq t@j_ord \, y \Imp x \neq y. 

1901 \] 

1902 

1903 \subsubsection{Structural induction} 

1904 

1905 The datatype package also provides structural induction rules. For 

1906 datatypes without nested recursion, this is of the following form: 

1907 \[ 

1908 \infer{P@1~x@1 \wedge \dots \wedge P@n~x@n} 

1909 {\begin{array}{lcl} 

1910 \Forall x@1 \dots x@{m^1@1}. 

1911 \List{P@{s^1@{1,1}}~x@{r^1@{1,1}}; \dots; 

1912 P@{s^1@{1,l^1@1}}~x@{r^1@{1,l^1@1}}} & \Imp & 

1913 P@1~\left(C^1@1~x@1~\dots~x@{m^1@1}\right) \\ 

1914 & \vdots \\ 

1915 \Forall x@1 \dots x@{m^1@{k@1}}. 

1916 \List{P@{s^1@{k@1,1}}~x@{r^1@{k@1,1}}; \dots; 

1917 P@{s^1@{k@1,l^1@{k@1}}}~x@{r^1@{k@1,l^1@{k@1}}}} & \Imp & 

1918 P@1~\left(C^1@{k@1}~x@1~\ldots~x@{m^1@{k@1}}\right) \\ 

1919 & \vdots \\ 

1920 \Forall x@1 \dots x@{m^n@1}. 

1921 \List{P@{s^n@{1,1}}~x@{r^n@{1,1}}; \dots; 

1922 P@{s^n@{1,l^n@1}}~x@{r^n@{1,l^n@1}}} & \Imp & 

1923 P@n~\left(C^n@1~x@1~\ldots~x@{m^n@1}\right) \\ 

1924 & \vdots \\ 

1925 \Forall x@1 \dots x@{m^n@{k@n}}. 

1926 \List{P@{s^n@{k@n,1}}~x@{r^n@{k@n,1}}; \dots 

1927 P@{s^n@{k@n,l^n@{k@n}}}~x@{r^n@{k@n,l^n@{k@n}}}} & \Imp & 

1928 P@n~\left(C^n@{k@n}~x@1~\ldots~x@{m^n@{k@n}}\right) 

1929 \end{array}} 

1930 \] 

1931 where 

1932 \[ 

1933 \begin{array}{rcl} 

1934 Rec^j@i & := & 

1935 \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots, 

1936 \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\} = \\[2ex] 

1937 && \left\{(i',i'')~\left~ 

1938 1\leq i' \leq m^j@i \wedge 1 \leq i'' \leq n \wedge 

1939 \tau^j@{i,i'} = (\alpha@1,\ldots,\alpha@h)t@{i''}\right.\right\} 

1940 \end{array} 

1941 \] 

1942 i.e.\ the properties $P@j$ can be assumed for all recursive arguments. 

1943 

1944 For datatypes with nested recursion, such as the \texttt{term} example from 

1945 above, things are a bit more complicated. Conceptually, Isabelle/HOL unfolds 

1946 a definition like 

1947 \begin{ttbox} 

1948 datatype ('a, 'b) term = Var 'a 

1949  App 'b ((('a, 'b) term) list) 

1950 \end{ttbox} 

1951 to an equivalent definition without nesting: 

1952 \begin{ttbox} 

1953 datatype ('a, 'b) term = Var 

1954  App 'b (('a, 'b) term_list) 

1955 and ('a, 'b) term_list = Nil' 

1956  Cons' (('a,'b) term) (('a,'b) term_list) 

1957 \end{ttbox} 

1958 Note however, that the type \texttt{('a,'b) term_list} and the constructors {\tt 

1959 Nil'} and \texttt{Cons'} are not really introduced. One can directly work with 

1960 the original (isomorphic) type \texttt{(('a, 'b) term) list} and its existing 

1961 constructors \texttt{Nil} and \texttt{Cons}. Thus, the structural induction rule for 

1962 \texttt{term} gets the form 

1963 \[ 

1964 \infer{P@1~x@1 \wedge P@2~x@2} 

1965 {\begin{array}{l} 

1966 \Forall x.~P@1~(\mathtt{Var}~x) \\ 

1967 \Forall x@1~x@2.~P@2~x@2 \Imp P@1~(\mathtt{App}~x@1~x@2) \\ 

1968 P@2~\mathtt{Nil} \\ 

1969 \Forall x@1~x@2. \List{P@1~x@1; P@2~x@2} \Imp P@2~(\mathtt{Cons}~x@1~x@2) 

1970 \end{array}} 

1971 \] 

1972 Note that there are two predicates $P@1$ and $P@2$, one for the type \texttt{('a,'b) term} 

1973 and one for the type \texttt{(('a, 'b) term) list}. 

1974 

1975 \medskip In principle, inductive types are already fully determined by 

1976 freeness and structural induction. For convenience in applications, 

1977 the following derived constructions are automatically provided for any 

1978 datatype. 

1979 

1980 \subsubsection{The \sdx{case} construct} 

1981 

1982 The type comes with an \MLlike \texttt{case}construct: 

1983 \[ 

1984 \begin{array}{rrcl} 

1985 \mbox{\tt case}~e~\mbox{\tt of} & C^j@1~x@{1,1}~\dots~x@{1,m^j@1} & \To & e@1 \\ 

1986 \vdots \\ 

1987 \mid & C^j@{k@j}~x@{k@j,1}~\dots~x@{k@j,m^j@{k@j}} & \To & e@{k@j} 

1988 \end{array} 

1989 \] 

1990 where the $x@{i,j}$ are either identifiers or nested tuple patterns as in 

1991 \S\ref{subsec:prodsum}. 

1992 \begin{warn} 

1993 All constructors must be present, their order is fixed, and nested patterns 

1994 are not supported (with the exception of tuples). Violating this 

1995 restriction results in strange error messages. 

1996 \end{warn} 

1997 

1998 To perform case distinction on a goal containing a \texttt{case}construct, 

1999 the theorem $t@j.$\texttt{split} is provided: 

2000 \[ 

2001 \begin{array}{@{}rcl@{}} 

2002 P(t@j_\mathtt{case}~f@1~\dots~f@{k@j}~e) &\!\!\!=& 

2003 \!\!\! ((\forall x@1 \dots x@{m^j@1}. e = C^j@1~x@1\dots x@{m^j@1} \to 

2004 P(f@1~x@1\dots x@{m^j@1})) \\ 

2005 &&\!\!\! ~\land~ \dots ~\land \\ 

2006 &&~\!\!\! (\forall x@1 \dots x@{m^j@{k@j}}. e = C^j@{k@j}~x@1\dots x@{m^j@{k@j}} \to 

2007 P(f@{k@j}~x@1\dots x@{m^j@{k@j}}))) 

2008 \end{array} 

2009 \] 

2010 where $t@j$\texttt{_case} is the internal name of the \texttt{case}construct. 

2011 This theorem can be added to a simpset via \ttindex{addsplits} 

2012 (see~\S\ref{subsec:HOL:case:splitting}). 

2013 

2014 \subsubsection{The function \cdx{size}}\label{sec:HOL:size} 

2015 

2016 Theory \texttt{Arith} declares a generic function \texttt{size} of type 

2017 $\alpha\To nat$. Each datatype defines a particular instance of \texttt{size} 

2018 by overloading according to the following scheme: 

2019 %%% FIXME: This formula is too big and is completely unreadable 

2020 \[ 

2021 size(C^j@i~x@1~\dots~x@{m^j@i}) = \! 

2022 \left\{ 

2023 \begin{array}{ll} 

2024 0 & \!\mbox{if $Rec^j@i = \emptyset$} \\ 

2025 \!\!\begin{array}{l} 

2026 size~x@{r^j@{i,1}} + \cdots \\ 

2027 \cdots + size~x@{r^j@{i,l^j@i}} + 1 

2028 \end{array} & 

2029 \!\mbox{if $Rec^j@i = \left\{\left(r^j@{i,1},s^j@{i,1}\right),\ldots, 

2030 \left(r^j@{i,l^j@i},s^j@{i,l^j@i}\right)\right\}$} 

2031 \end{array} 

2032 \right. 

2033 \] 

2034 where $Rec^j@i$ is defined above. Viewing datatypes as generalised trees, the 

2035 size of a leaf is 0 and the size of a node is the sum of the sizes of its 

2036 subtrees ${}+1$. 

2037 

2038 \subsection{Defining datatypes} 

2039 

2040 The theory syntax for datatype definitions is shown in 

2041 Fig.~\ref{datatypegrammar}. In order to be wellformed, a datatype 

2042 definition has to obey the rules stated in the previous section. As a result 

2043 the theory is extended with the new types, the constructors, and the theorems 

2044 listed in the previous section. 

2045 

2046 \begin{figure} 

2047 \begin{rail} 

2048 datatype : 'datatype' typedecls; 

2049 

2050 typedecls: ( newtype '=' (cons + '') ) + 'and' 

2051 ; 

2052 newtype : typevarlist id ( ()  '(' infix ')' ) 

2053 ; 

2054 cons : name (argtype *) ( ()  ( '(' mixfix ')' ) ) 

2055 ; 

2056 argtype : id  tid  ('(' typevarlist id ')') 

2057 ; 

2058 \end{rail} 

2059 \caption{Syntax of datatype declarations} 

2060 \label{datatypegrammar} 

2061 \end{figure} 

2062 

2063 Most of the theorems about datatypes become part of the default simpset and 

2064 you never need to see them again because the simplifier applies them 

2065 automatically. Only induction or exhaustion are usually invoked by hand. 

2066 \begin{ttdescription} 

2067 \item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$] 

2068 applies structural induction on variable $x$ to subgoal $i$, provided the 

2069 type of $x$ is a datatype. 

2070 \item[\ttindexbold{mutual_induct_tac} 

2071 {\tt["}$x@1${\tt",}$\ldots${\tt,"}$x@n${\tt"]} $i$] applies simultaneous 

2072 structural induction on the variables $x@1,\ldots,x@n$ to subgoal $i$. This 

2073 is the canonical way to prove properties of mutually recursive datatypes 

2074 such as \texttt{aexp} and \texttt{bexp}, or datatypes with nested recursion such as 

2075 \texttt{term}. 

2076 \end{ttdescription} 

2077 In some cases, induction is overkill and a case distinction over all 

2078 constructors of the datatype suffices. 

2079 \begin{ttdescription} 

2080 \item[\ttindexbold{exhaust_tac} {\tt"}$u${\tt"} $i$] 

2081 performs an exhaustive case analysis for the term $u$ whose type 

2082 must be a datatype. If the datatype has $k@j$ constructors 

2083 $C^j@1$, \dots $C^j@{k@j}$, subgoal $i$ is replaced by $k@j$ new subgoals which 

2084 contain the additional assumption $u = C^j@{i'}~x@1~\dots~x@{m^j@{i'}}$ for 

2085 $i'=1$, $\dots$,~$k@j$. 

2086 \end{ttdescription} 

2087 

2088 Note that induction is only allowed on free variables that should not occur 

2089 among the premises of the subgoal. Exhaustion applies to arbitrary terms. 

2090 

2091 \bigskip 

2092 

2093 

2094 For the technically minded, we exhibit some more details. Processing the 

2095 theory file produces an \ML\ structure which, in addition to the usual 

2096 components, contains a structure named $t$ for each datatype $t$ defined in 

2097 the file. Each structure $t$ contains the following elements: 

2098 \begin{ttbox} 

2099 val distinct : thm list 

2100 val inject : thm list 

2101 val induct : thm 

2102 val exhaust : thm 

2103 val cases : thm list 

2104 val split : thm 

2105 val split_asm : thm 

2106 val recs : thm list 

2107 val size : thm list 

2108 val simps : thm list 

2109 \end{ttbox} 

2110 \texttt{distinct}, \texttt{inject}, \texttt{induct}, \texttt{size} 

2111 and \texttt{split} contain the theorems 

2112 described above. For user convenience, \texttt{distinct} contains 

2113 inequalities in both directions. The reduction rules of the {\tt 

2114 case}construct are in \texttt{cases}. All theorems from {\tt 

2115 distinct}, \texttt{inject} and \texttt{cases} are combined in \texttt{simps}. 

2116 In case of mutually recursive datatypes, \texttt{recs}, \texttt{size}, \texttt{induct} 

2117 and \texttt{simps} are contained in a separate structure named $t@1_\ldots_t@n$. 

2118 

2119 

2120 \subsection{Representing existing types as datatypes} 

2121 

2122 For foundational reasons, some basic types such as \texttt{nat}, \texttt{*}, {\tt 

2123 +}, \texttt{bool} and \texttt{unit} are not defined in a \texttt{datatype} section, 

2124 but by more primitive means using \texttt{typedef}. To be able to use the 

2125 tactics \texttt{induct_tac} and \texttt{exhaust_tac} and to define functions by 

2126 primitive recursion on these types, such types may be represented as actual 

2127 datatypes. This is done by specifying an induction rule, as well as theorems 

2128 stating the distinctness and injectivity of constructors in a {\tt 

2129 rep_datatype} section. For type \texttt{nat} this works as follows: 

2130 \begin{ttbox} 

2131 rep_datatype nat 

2132 distinct Suc_not_Zero, Zero_not_Suc 

2133 inject Suc_Suc_eq 

2134 induct nat_induct 

2135 \end{ttbox} 

2136 The datatype package automatically derives additional theorems for recursion 

2137 and case combinators from these rules. Any of the basic HOL types mentioned 

2138 above are represented as datatypes. Try an induction on \texttt{bool} 

2139 today. 

2140 

2141 

2142 \subsection{Examples} 

2143 

2144 \subsubsection{The datatype $\alpha~mylist$} 

2145 

2146 We want to define a type $\alpha~mylist$. To do this we have to build a new 

2147 theory that contains the type definition. We start from the theory 

2148 \texttt{Datatype} instead of \texttt{Main} in order to avoid clashes with the 

2149 \texttt{List} theory of Isabelle/HOL. 

2150 \begin{ttbox} 

2151 MyList = Datatype + 

2152 datatype 'a mylist = Nil  Cons 'a ('a mylist) 

2153 end 

2154 \end{ttbox} 

2155 After loading the theory, we can prove $Cons~x~xs\neq xs$, for example. To 

2156 ease the induction applied below, we state the goal with $x$ quantified at the 

2157 objectlevel. This will be stripped later using \ttindex{qed_spec_mp}. 

2158 \begin{ttbox} 

2159 Goal "!x. Cons x xs ~= xs"; 

2160 {\out Level 0} 

2161 {\out ! x. Cons x xs ~= xs} 

2162 {\out 1. ! x. Cons x xs ~= xs} 

2163 \end{ttbox} 

2164 This can be proved by the structural induction tactic: 

2165 \begin{ttbox} 

2166 by (induct_tac "xs" 1); 

2167 {\out Level 1} 

2168 {\out ! x. Cons x xs ~= xs} 

2169 {\out 1. ! x. Cons x Nil ~= Nil} 

2170 {\out 2. !!a mylist.} 

2171 {\out ! x. Cons x mylist ~= mylist ==>} 

2172 {\out ! x. Cons x (Cons a mylist) ~= Cons a mylist} 

2173 \end{ttbox} 

2174 The first subgoal can be proved using the simplifier. Isabelle/HOL has 

2175 already added the freeness properties of lists to the default simplification 

2176 set. 

2177 \begin{ttbox} 

2178 by (Simp_tac 1); 

2179 {\out Level 2} 

2180 {\out ! x. Cons x xs ~= xs} 

2181 {\out 1. !!a mylist.} 

2182 {\out ! x. Cons x mylist ~= mylist ==>} 

2183 {\out ! x. Cons x (Cons a mylist) ~= Cons a mylist} 

2184 \end{ttbox} 

2185 Similarly, we prove the remaining goal. 

2186 \begin{ttbox} 

2187 by (Asm_simp_tac 1); 

2188 {\out Level 3} 

2189 {\out ! x. Cons x xs ~= xs} 

2190 {\out No subgoals!} 

2191 \ttbreak 

2192 qed_spec_mp "not_Cons_self"; 

2193 {\out val not_Cons_self = "Cons x xs ~= xs" : thm} 

2194 \end{ttbox} 

2195 Because both subgoals could have been proved by \texttt{Asm_simp_tac} 

2196 we could have done that in one step: 

2197 \begin{ttbox} 

2198 by (ALLGOALS Asm_simp_tac); 

2199 \end{ttbox} 

2200 

2201 

2202 \subsubsection{The datatype $\alpha~mylist$ with mixfix syntax} 

2203 

2204 In this example we define the type $\alpha~mylist$ again but this time 

2205 we want to write \texttt{[]} for \texttt{Nil} and we want to use infix 

2206 notation \verb# for \texttt{Cons}. To do this we simply add mixfix 

2207 annotations after the constructor declarations as follows: 

2208 \begin{ttbox} 

2209 MyList = Datatype + 

2210 datatype 'a mylist = 

2211 Nil ("[]")  

2212 Cons 'a ('a mylist) (infixr "#" 70) 

2213 end 

2214 \end{ttbox} 

2215 Now the theorem in the previous example can be written \verbx#xs ~= xs. 

2216 

2217 

2218 \subsubsection{A datatype for weekdays} 

2219 

2220 This example shows a datatype that consists of 7 constructors: 

2221 \begin{ttbox} 

2222 Days = Main + 

2223 datatype days = Mon  Tue  Wed  Thu  Fri  Sat  Sun 

2224 end 

2225 \end{ttbox} 

2226 Because there are more than 6 constructors, inequality is expressed via a function 

2227 \verbdays_ord. The theorem \verbMon ~= Tue is not directly 

2228 contained among the distinctness theorems, but the simplifier can 

2229 prove it thanks to rewrite rules inherited from theory \texttt{Arith}: 

2230 \begin{ttbox} 

2231 Goal "Mon ~= Tue"; 

2232 by (Simp_tac 1); 

2233 \end{ttbox} 

2234 You need not derive such inequalities explicitly: the simplifier will dispose 

2235 of them automatically. 

2236 \index{*datatype)} 

2237 

2238 

2239 \section{Recursive function definitions}\label{sec:HOL:recursive} 

2240 \index{recursive functionssee{recursion}} 

2241 

2242 Isabelle/HOL provides two main mechanisms of defining recursive functions. 

2243 \begin{enumerate} 

2244 \item \textbf{Primitive recursion} is available only for datatypes, and it is 

2245 somewhat restrictive. Recursive calls are only allowed on the argument's 

2246 immediate constituents. On the other hand, it is the form of recursion most 

2247 often wanted, and it is easy to use. 

2248 

2249 \item \textbf{Wellfounded recursion} requires that you supply a wellfounded 

2250 relation that governs the recursion. Recursive calls are only allowed if 

2251 they make the argument decrease under the relation. Complicated recursion 

2252 forms, such as nested recursion, can be dealt with. Termination can even be 

2253 proved at a later time, though having unsolved termination conditions around 

2254 can make work difficult.% 

2255 \footnote{This facility is based on Konrad Slind's TFL 

2256 package~\cite{slindtfl}. Thanks are due to Konrad for implementing TFL 

2257 and assisting with its installation.} 

2258 \end{enumerate} 

2259 

2260 Following good HOL tradition, these declarations do not assert arbitrary 

2261 axioms. Instead, they define the function using a recursion operator. Both 

2262 HOL and ZF derive the theory of wellfounded recursion from first 

2263 principles~\cite{paulsonsetII}. Primitive recursion over some datatype 

2264 relies on the recursion operator provided by the datatype package. With 

2265 either form of function definition, Isabelle proves the desired recursion 

2266 equations as theorems. 

2267 

2268 

2269 \subsection{Primitive recursive functions} 

2270 \label{sec:HOL:primrec} 

2271 \index{recursion!primitive(} 

2272 \index{*primrec(} 

2273 

2274 Datatypes come with a uniform way of defining functions, {\bf primitive 

2275 recursion}. In principle, one could introduce primitive recursive functions 

2276 by asserting their reduction rules as new axioms, but this is not recommended: 

2277 \begin{ttbox}\slshape 

2278 Append = Main + 

2279 consts app :: ['a list, 'a list] => 'a list 

2280 rules 

2281 app_Nil "app [] ys = ys" 

2282 app_Cons "app (x#xs) ys = x#app xs ys" 

2283 end 

2284 \end{ttbox} 

2285 Asserting axioms brings the danger of accidentally asserting nonsense, as 

2286 in \verb$app [] ys = us$. 

2287 

2288 The \ttindex{primrec} declaration is a safe means of defining primitive 

2289 recursive functions on datatypes: 

2290 \begin{ttbox} 

2291 Append = Main + 

2292 consts app :: ['a list, 'a list] => 'a list 

2293 primrec 

2294 "app [] ys = ys" 

2295 "app (x#xs) ys = x#app xs ys" 

2296 end 

2297 \end{ttbox} 

2298 Isabelle will now check that the two rules do indeed form a primitive 

2299 recursive definition. For example 

2300 \begin{ttbox} 

2301 primrec 

2302 "app [] ys = us" 

2303 \end{ttbox} 

2304 is rejected with an error message ``\texttt{Extra variables on rhs}''. 

2305 

2306 \bigskip 

2307 

2308 The general form of a primitive recursive definition is 

2309 \begin{ttbox} 

2310 primrec 

2311 {\it reduction rules} 

2312 \end{ttbox} 

2313 where \textit{reduction rules} specify one or more equations of the form 

2314 \[ f \, x@1 \, \dots \, x@m \, (C \, y@1 \, \dots \, y@k) \, z@1 \, 

2315 \dots \, z@n = r \] such that $C$ is a constructor of the datatype, $r$ 

2316 contains only the free variables on the lefthand side, and all recursive 

2317 calls in $r$ are of the form $f \, \dots \, y@i \, \dots$ for some $i$. There 

2318 must be at most one reduction rule for each constructor. The order is 

2319 immaterial. For missing constructors, the function is defined to return a 

2320 default value. 

2321 

2322 If you would like to refer to some rule by name, then you must prefix 

2323 the rule with an identifier. These identifiers, like those in the 

2324 \texttt{rules} section of a theory, will be visible at the \ML\ level. 

2325 

2326 The primitive recursive function can have infix or mixfix syntax: 

2327 \begin{ttbox}\underscoreon 

2328 consts "@" :: ['a list, 'a list] => 'a list (infixr 60) 

2329 primrec 

2330 "[] @ ys = ys" 

2331 "(x#xs) @ ys = x#(xs @ ys)" 

2332 \end{ttbox} 

2333 

2334 The reduction rules become part of the default simpset, which 

2335 leads to short proof scripts: 

2336 \begin{ttbox}\underscoreon 

2337 Goal "(xs @ ys) @ zs = xs @ (ys @ zs)"; 

2338 by (induct\_tac "xs" 1); 

2339 by (ALLGOALS Asm\_simp\_tac); 

2340 \end{ttbox} 

2341 

2342 \subsubsection{Example: Evaluation of expressions} 

2343 Using mutual primitive recursion, we can define evaluation functions \texttt{eval_aexp} 

2344 and \texttt{eval_bexp} for the datatypes of arithmetic and boolean expressions mentioned in 

2345 \S\ref{subsec:datatype:basics}: 

2346 \begin{ttbox} 

2347 consts 

2348 eval_aexp :: "['a => nat, 'a aexp] => nat" 

2349 eval_bexp :: "['a => nat, 'a bexp] => bool" 

2350 

2351 primrec 

2352 "eval_aexp env (If_then_else b a1 a2) = 

2353 (if eval_bexp env b then eval_aexp env a1 else eval_aexp env a2)" 

2354 "eval_aexp env (Sum a1 a2) = eval_aexp env a1 + eval_aexp env a2" 

2355 "eval_aexp env (Diff a1 a2) = eval_aexp env a1  eval_aexp env a2" 

2356 "eval_aexp env (Var v) = env v" 

2357 "eval_aexp env (Num n) = n" 

2358 

2359 "eval_bexp env (Less a1 a2) = (eval_aexp env a1 < eval_aexp env a2)" 

2360 "eval_bexp env (And b1 b2) = (eval_bexp env b1 & eval_bexp env b2)" 

2361 "eval_bexp env (Or b1 b2) = (eval_bexp env b1 & eval_bexp env b2)" 

2362 \end{ttbox} 

2363 Since the value of an expression depends on the value of its variables, 

2364 the functions \texttt{eval_aexp} and \texttt{eval_bexp} take an additional 

2365 parameter, an {\em environment} of type \texttt{'a => nat}, which maps 

2366 variables to their values. 

2367 

2368 Similarly, we may define substitution functions \texttt{subst_aexp} 

2369 and \texttt{subst_bexp} for expressions: The mapping \texttt{f} of type 

2370 \texttt{'a => 'a aexp} given as a parameter is lifted canonically 

2371 on the types {'a aexp} and {'a bexp}: 

2372 \begin{ttbox} 

2373 consts 

2374 subst_aexp :: "['a => 'b aexp, 'a aexp] => 'b aexp" 

2375 subst_bexp :: "['a => 'b aexp, 'a bexp] => 'b bexp" 

2376 

2377 primrec 

2378 "subst_aexp f (If_then_else b a1 a2) = 

2379 If_then_else (subst_bexp f b) (subst_aexp f a1) (subst_aexp f a2)" 

2380 "subst_aexp f (Sum a1 a2) = Sum (subst_aexp f a1) (subst_aexp f a2)" 

2381 "subst_aexp f (Diff a1 a2) = Diff (subst_aexp f a1) (subst_aexp f a2)" 

2382 "subst_aexp f (Var v) = f v" 

2383 "subst_aexp f (Num n) = Num n" 

2384 

2385 "subst_bexp f (Less a1 a2) = Less (subst_aexp f a1) (subst_aexp f a2)" 

2386 "subst_bexp f (And b1 b2) = And (subst_bexp f b1) (subst_bexp f b2)" 

2387 "subst_bexp f (Or b1 b2) = Or (subst_bexp f b1) (subst_bexp f b2)" 

2388 \end{ttbox} 

2389 In textbooks about semantics one often finds {\em substitution theorems}, 

2390 which express the relationship between substitution and evaluation. For 

2391 \texttt{'a aexp} and \texttt{'a bexp}, we can prove such a theorem by mutual 

2392 induction, followed by simplification: 

2393 \begin{ttbox} 

2394 Goal 

2395 "eval_aexp env (subst_aexp (Var(v := a')) a) = 

2396 eval_aexp (env(v := eval_aexp env a')) a & 

2397 eval_bexp env (subst_bexp (Var(v := a')) b) = 

2398 eval_bexp (env(v := eval_aexp env a')) b"; 

2399 by (mutual_induct_tac ["a","b"] 1); 

2400 by (ALLGOALS Asm_full_simp_tac); 

2401 \end{ttbox} 

2402 

2403 \subsubsection{Example: A substitution function for terms} 

2404 Functions on datatypes with nested recursion, such as the type 

2405 \texttt{term} mentioned in \S\ref{subsec:datatype:basics}, are 

2406 also defined by mutual primitive recursion. A substitution 

2407 function \texttt{subst_term} on type \texttt{term}, similar to the functions 

2408 \texttt{subst_aexp} and \texttt{subst_bexp} described above, can 

2409 be defined as follows: 

2410 \begin{ttbox} 

2411 consts 

2412 subst_term :: "['a => ('a, 'b) term, ('a, 'b) term] => ('a, 'b) term" 

2413 subst_term_list :: 

2414 "['a => ('a, 'b) term, ('a, 'b) term list] => ('a, 'b) term list" 

2415 

2416 primrec 

2417 "subst_term f (Var a) = f a" 

2418 "subst_term f (App b ts) = App b (subst_term_list f ts)" 

2419 

2420 "subst_term_list f [] = []" 

2421 "subst_term_list f (t # ts) = 

2422 subst_term f t # subst_term_list f ts" 

2423 \end{ttbox} 

2424 The recursion scheme follows the structure of the unfolded definition of type 

2425 \texttt{term} shown in \S\ref{subsec:datatype:basics}. To prove properties of 

2426 this substitution function, mutual induction is needed: 

2427 \begin{ttbox} 

2428 Goal 

2429 "(subst_term ((subst_term f1) o f2) t) = 

2430 (subst_term f1 (subst_term f2 t)) & 

2431 (subst_term_list ((subst_term f1) o f2) ts) = 

2432 (subst_term_list f1 (subst_term_list f2 ts))"; 

2433 by (mutual_induct_tac ["t", "ts"] 1); 

2434 by (ALLGOALS Asm_full_simp_tac); 

2435 \end{ttbox} 

2436 

2437 \index{recursion!primitive)} 

2438 \index{*primrec)} 

2439 

2440 

2441 \subsection{General recursive functions} 

2442 \label{sec:HOL:recdef} 

2443 \index{recursion!general(} 

2444 \index{*recdef(} 

2445 

2446 Using \texttt{recdef}, you can declare functions involving nested recursion 

2447 and patternmatching. Recursion need not involve datatypes and there are few 

2448 syntactic restrictions. Termination is proved by showing that each recursive 

2449 call makes the argument smaller in a suitable sense, which you specify by 

2450 supplying a wellfounded relation. 

2451 

2452 Here is a simple example, the Fibonacci function. The first line declares 

2453 \texttt{fib} to be a constant. The wellfounded relation is simply~$<$ (on 

2454 the natural numbers). Patternmatching is used here: \texttt{1} is a 

2455 macro for \texttt{Suc~0}. 

2456 \begin{ttbox} 

2457 consts fib :: "nat => nat" 

2458 recdef fib "less_than" 

2459 "fib 0 = 0" 

2460 "fib 1 = 1" 

2461 "fib (Suc(Suc x)) = (fib x + fib (Suc x))" 

2462 \end{ttbox} 

2463 

2464 With \texttt{recdef}, function definitions may be incomplete, and patterns may 

2465 overlap, as in functional programming. The \texttt{recdef} package 

2466 disambiguates overlapping patterns by taking the order of rules into account. 

2467 For missing patterns, the function is defined to return a default value. 

2468 

2469 %For example, here is a declaration of the list function \cdx{hd}: 

2470 %\begin{ttbox} 

2471 %consts hd :: 'a list => 'a 

2472 %recdef hd "\{\}" 

2473 % "hd (x#l) = x" 

2474 %\end{ttbox} 

2475 %Because this function is not recursive, we may supply the empty wellfounded 

2476 %relation, $\{\}$. 

2477 

2478 The wellfounded relation defines a notion of ``smaller'' for the function's 

2479 argument type. The relation $\prec$ is \textbf{wellfounded} provided it 

2480 admits no infinitely decreasing chains 

2481 \[ \cdots\prec x@n\prec\cdots\prec x@1. \] 

2482 If the function's argument has type~$\tau$, then $\prec$ has to be a relation 

2483 over~$\tau$: it must have type $(\tau\times\tau)set$. 

2484 

2485 Proving wellfoundedness can be tricky, so Isabelle/HOL provides a collection 

2486 of operators for building wellfounded relations. The package recognises 

2487 these operators and automatically proves that the constructed relation is 

2488 wellfounded. Here are those operators, in order of importance: 

2489 \begin{itemize} 

2490 \item \texttt{less_than} is ``less than'' on the natural numbers. 

2491 (It has type $(nat\times nat)set$, while $<$ has type $[nat,nat]\To bool$. 

2492 

2493 \item $\mathop{\mathtt{measure}} f$, where $f$ has type $\tau\To nat$, is the 

2494 relation~$\prec$ on type~$\tau$ such that $x\prec y$ iff $f(x)<f(y)$. 

2495 Typically, $f$ takes the recursive function's arguments (as a tuple) and 

2496 returns a result expressed in terms of the function \texttt{size}. It is 

2497 called a \textbf{measure function}. Recall that \texttt{size} is overloaded 

2498 and is defined on all datatypes (see \S\ref{sec:HOL:size}). 

2499 

2500 \item $\mathop{\mathtt{inv_image}} f\;R$ is a generalisation of 

2501 \texttt{measure}. It specifies a relation such that $x\prec y$ iff $f(x)$ 

2502 is less than $f(y)$ according to~$R$, which must itself be a wellfounded 

2503 relation. 

2504 

2505 \item $R@1\texttt{**}R@2$ is the lexicographic product of two relations. It 

2506 is a relation on pairs and satisfies $(x@1,x@2)\prec(y@1,y@2)$ iff $x@1$ 

2507 is less than $y@1$ according to~$R@1$ or $x@1=y@1$ and $x@2$ 

2508 is less than $y@2$ according to~$R@2$. 

2509 

2510 \item \texttt{finite_psubset} is the proper subset relation on finite sets. 

2511 \end{itemize} 

2512 

2513 We can use \texttt{measure} to declare Euclid's algorithm for the greatest 

2514 common divisor. The measure function, $\lambda(m,n). n$, specifies that the 

2515 recursion terminates because argument~$n$ decreases. 

2516 \begin{ttbox} 

2517 recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)" 

2518 "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" 

2519 \end{ttbox} 

2520 

2521 The general form of a wellfounded recursive definition is 

2522 \begin{ttbox} 

2523 recdef {\it function} {\it rel} 

2524 congs {\it congruence rules} {\bf(optional)} 

2525 simpset {\it simplification set} {\bf(optional)} 

2526 {\it reduction rules} 

2527 \end{ttbox} 

2528 where 

2529 \begin{itemize} 

2530 \item \textit{function} is the name of the function, either as an \textit{id} 

2531 or a \textit{string}. 

2532 

2533 \item \textit{rel} is a {\HOL} expression for the wellfounded termination 

2534 relation. 

2535 

2536 \item \textit{congruence rules} are required only in highly exceptional 

2537 circumstances. 

2538 

2539 \item The \textit{simplification set} is used to prove that the supplied 

2540 relation is wellfounded. It is also used to prove the \textbf{termination 

2541 conditions}: assertions that arguments of recursive calls decrease under 

2542 \textit{rel}. By default, simplification uses \texttt{simpset()}, which 

2543 is sufficient to prove wellfoundedness for the builtin relations listed 

2544 above. 

2545 

2546 \item \textit{reduction rules} specify one or more recursion equations. Each 

2547 lefthand side must have the form $f\,t$, where $f$ is the function and $t$ 

2548 is a tuple of distinct variables. If more than one equation is present then 

2549 $f$ is defined by patternmatching on components of its argument whose type 

2550 is a \texttt{datatype}. 

2551 

2552 Unlike with \texttt{primrec}, the reduction rules are not added to the 

2553 default simpset, and individual rules may not be labelled with identifiers. 

2554 However, the identifier $f$\texttt{.rules} is visible at the \ML\ level 

2555 as a list of theorems. 

2556 \end{itemize} 

2557 

2558 With the definition of \texttt{gcd} shown above, Isabelle/HOL is unable to 

2559 prove one termination condition. It remains as a precondition of the 

2560 recursion theorems. 

2561 \begin{ttbox} 

2562 gcd.rules; 

2563 {\out ["! m n. n ~= 0 > m mod n < n} 

2564 {\out ==> gcd (?m, ?n) = (if ?n = 0 then ?m else gcd (?n, ?m mod ?n))"] } 

2565 {\out : thm list} 

2566 \end{ttbox} 

2567 The theory \texttt{HOL/ex/Primes} illustrates how to prove termination 

2568 conditions afterwards. The function \texttt{Tfl.tgoalw} is like the standard 

2569 function \texttt{goalw}, which sets up a goal to prove, but its argument 

2570 should be the identifier $f$\texttt{.rules} and its effect is to set up a 

2571 proof of the termination conditions: 

2572 \begin{ttbox} 

2573 Tfl.tgoalw thy [] gcd.rules; 

2574 {\out Level 0} 

2575 {\out ! m n. n ~= 0 > m mod n < n} 

2576 {\out 1. ! m n. n ~= 0 > m mod n < n} 

2577 \end{ttbox} 

2578 This subgoal has a onestep proof using \texttt{simp_tac}. Once the theorem 

2579 is proved, it can be used to eliminate the termination conditions from 

2580 elements of \texttt{gcd.rules}. Theory \texttt{HOL/Subst/Unify} is a much 

2581 more complicated example of this process, where the termination conditions can 

2582 only be proved by complicated reasoning involving the recursive function 

2583 itself. 

2584 

2585 Isabelle/HOL can prove the \texttt{gcd} function's termination condition 

2586 automatically if supplied with the right simpset. 

2587 \begin{ttbox} 

2588 recdef gcd "measure ((\%(m,n). n) ::nat*nat=>nat)" 

2589 simpset "simpset() addsimps [mod_less_divisor, zero_less_eq]" 

2590 "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))" 

2591 \end{ttbox} 

2592 

2593 A \texttt{recdef} definition also returns an induction rule specialised for 

2594 the recursive function. For the \texttt{gcd} function above, the induction 

2595 rule is 

2596 \begin{ttbox} 

2597 gcd.induct; 

2598 {\out "(!!m n. n ~= 0 > ?P n (m mod n) ==> ?P m n) ==> ?P ?u ?v" : thm} 

2599 \end{ttbox} 

2600 This rule should be used to reason inductively about the \texttt{gcd} 

2601 function. It usually makes the induction hypothesis available at all 

2602 recursive calls, leading to very direct proofs. If any termination conditions 

2603 remain unproved, they will become additional premises of this rule. 

2604 

2605 \index{recursion!general)} 

2606 \index{*recdef)} 

2607 

2608 

2609 \section{Inductive and coinductive definitions} 

2610 \index{*inductive(} 

2611 \index{*coinductive(} 

2612 

2613 An {\bf inductive definition} specifies the least set~$R$ closed under given 

2614 rules. (Applying a rule to elements of~$R$ yields a result within~$R$.) For 

2615 example, a structural operational semantics is an inductive definition of an 

2616 evaluation relation. Dually, a {\bf coinductive definition} specifies the 

2617 greatest set~$R$ consistent with given rules. (Every element of~$R$ can be 

2618 seen as arising by applying a rule to elements of~$R$.) An important example 

2619 is using bisimulation relations to formalise equivalence of processes and 

2620 infinite data structures. 

2621 

2622 A theory file may contain any number of inductive and coinductive 

2623 definitions. They may be intermixed with other declarations; in 

2624 particular, the (co)inductive sets {\bf must} be declared separately as 

2625 constants, and may have mixfix syntax or be subject to syntax translations. 

2626 

2627 Each (co)inductive definition adds definitions to the theory and also 

2628 proves some theorems. Each definition creates an \ML\ structure, which is a 

2629 substructure of the main theory structure. 

2630 

2631 This package is related to the \ZF\ one, described in a separate 

2632 paper,% 

2633 \footnote{It appeared in CADE~\cite{paulsonCADE}; a longer version is 

2634 distributed with Isabelle.} % 

2635 which you should refer to in case of difficulties. The package is simpler 

2636 than \ZF's thanks to \HOL's extralogical automatic typechecking. The types 

2637 of the (co)inductive sets determine the domain of the fixedpoint definition, 

2638 and the package does not have to use inference rules for typechecking. 

2639 

2640 

2641 \subsection{The result structure} 

2642 Many of the result structure's components have been discussed in the paper; 

2643 others are selfexplanatory. 

2644 \begin{description} 

2645 \item[\tt defs] is the list of definitions of the recursive sets. 

2646 

2647 \item[\tt mono] is a monotonicity theorem for the fixedpoint operator. 

2648 

2649 \item[\tt unfold] is a fixedpoint equation for the recursive set (the union of 

2650 the recursive sets, in the case of mutual recursion). 

2651 

2652 \item[\tt intrs] is the list of introduction rules, now proved as theorems, for 

2653 the recursive sets. The rules are also available individually, using the 

2654 names given them in the theory file. 

2655 

2656 \item[\tt elims] is the list of elimination rule. 

2657 

2658 \item[\tt elim] is the head of the list \texttt{elims}. 

2659 

2660 \item[\tt mk_cases] is a function to create simplified instances of {\tt 

2661 elim} using freeness reasoning on underlying datatypes. 

2662 \end{description} 

2663 

2664 For an inductive definition, the result structure contains the 

2665 rule \texttt{induct}. For a 

2666 coinductive definition, it contains the rule \verbcoinduct. 

2667 

2668 Figure~\ref{defresultfig} summarises the two result signatures, 

2669 specifying the types of all these components. 

2670 

2671 \begin{figure} 

2672 \begin{ttbox} 

2673 sig 

2674 val defs : thm list 

2675 val mono : thm 

2676 val unfold : thm 

2677 val intrs : thm list 

2678 val elims : thm list 

2679 val elim : thm 

2680 val mk_cases : string > thm 

2681 {\it(Inductive definitions only)} 

2682 val induct : thm 

2683 {\it(coinductive definitions only)} 

2684 val coinduct : thm 

2685 end 

2686 \end{ttbox} 

2687 \hrule 

2688 \caption{The {\ML} result of a (co)inductive definition} \label{defresultfig} 

2689 \end{figure} 

2690 

2691 \subsection{The syntax of a (co)inductive definition} 

2692 An inductive definition has the form 

2693 \begin{ttbox} 

2694 inductive {\it inductive sets} 

2695 intrs {\it introduction rules} 

2696 monos {\it monotonicity theorems} 

2697 con_defs {\it constructor definitions} 

2698 \end{ttbox} 

2699 A coinductive definition is identical, except that it starts with the keyword 

2700 \texttt{coinductive}. 

2701 

2702 The \texttt{monos} and \texttt{con_defs} sections are optional. If present, 

2703 each is specified by a list of identifiers. 

2704 

2705 \begin{itemize} 

2706 \item The \textit{inductive sets} are specified by one or more strings. 

2707 

2708 \item The \textit{introduction rules} specify one or more introduction rules in 

2709 the form \textit{ident\/}~\textit{string}, where the identifier gives the name of 

2710 the rule in the result structure. 

2711 

2712 \item The \textit{monotonicity theorems} are required for each operator 

2713 applied to a recursive set in the introduction rules. There {\bf must} 

2714 be a theorem of the form $A\subseteq B\Imp M(A)\subseteq M(B)$, for each 

2715 premise $t\in M(R@i)$ in an introduction rule! 

2716 

2717 \item The \textit{constructor definitions} contain definitions of constants 

2718 appearing in the introduction rules. In most cases it can be omitted. 

2719 \end{itemize} 

2720 

2721 

2722 \subsection{Example of an inductive definition} 

2723 Two declarations, included in a theory file, define the finite powerset 

2724 operator. First we declare the constant~\texttt{Fin}. Then we declare it 

2725 inductively, with two introduction rules: 

2726 \begin{ttbox} 

2727 consts Fin :: 'a set => 'a set set 

2728 inductive "Fin A" 

2729 intrs 

2730 emptyI "{\ttlbrace}{\ttrbrace} : Fin A" 

2731 insertI "[ a: A; b: Fin A ] ==> insert a b : Fin A" 

2732 \end{ttbox} 

2733 The resulting theory structure contains a substructure, called~\texttt{Fin}. 

2734 It contains the \texttt{Fin}$~A$ introduction rules as the list \texttt{Fin.intrs}, 

2735 and also individually as \texttt{Fin.emptyI} and \texttt{Fin.consI}. The induction 

2736 rule is \texttt{Fin.induct}. 

2737 

2738 For another example, here is a theory file defining the accessible 

2739 part of a relation. The main thing to note is the use of~\texttt{Pow} in 

2740 the sole introduction rule, and the corresponding mention of the rule 

2741 \verbPow_mono in the \texttt{monos} list. The paper 

2742 \cite{paulsonCADE} discusses a \ZF\ version of this example in more 

2743 detail. 

2744 \begin{ttbox} 

2745 Acc = WF + 

2746 consts pred :: "['b, ('a * 'b)set] => 'a set" (*Set of predecessors*) 

2747 acc :: "('a * 'a)set => 'a set" (*Accessible part*) 

2748 defs pred_def "pred x r == {y. (y,x):r}" 

2749 inductive "acc r" 

2750 intrs 

2751 pred "pred a r: Pow(acc r) ==> a: acc r" 

2752 monos Pow_mono 

2753 end 

2754 \end{ttbox} 

2755 The Isabelle distribution contains many other inductive definitions. Simple 

2756 examples are collected on subdirectory \texttt{HOL/Induct}. The theory 

2757 \texttt{HOL/Induct/LList} contains coinductive definitions. Larger examples 

2758 may be found on other subdirectories of \texttt{HOL}, such as \texttt{IMP}, 

2759 \texttt{Lambda} and \texttt{Auth}. 

2760 

2761 \index{*coinductive)} \index{*inductive)} 

2762 

2763 

2764 \section{The examples directories} 

2765 

2766 Directory \texttt{HOL/Auth} contains theories for proving the correctness of 

2767 cryptographic protocols. The approach is based upon operational 

2768 semantics~\cite{paulsonsecurity} rather than the more usual belief logics. 

2769 On the same directory are proofs for some standard examples, such as the 

2770 NeedhamSchroeder publickey authentication protocol~\cite{paulsonns} 

2771 and the OtwayRees protocol. 

2772 

2773 Directory \texttt{HOL/IMP} contains a formalization of various denotational, 

2774 operational and axiomatic semantics of a simple whilelanguage, the necessary 

2775 equivalence proofs, soundness and completeness of the Hoare rules with respect 

2776 to the 

2777 denotational semantics, and soundness and completeness of a verification 

2778 condition generator. Much of development is taken from 

2779 Winskel~\cite{winskel93}. For details see~\cite{nipkowIMP}. 

2780 

2781 Directory \texttt{HOL/Hoare} contains a user friendly surface syntax for Hoare 

2782 logic, including a tactic for generating verificationconditions. 

2783 

2784 Directory \texttt{HOL/MiniML} contains a formalization of the type system of the 

2785 core functional language MiniML and a correctness proof for its type 

2786 inference algorithm $\cal W$~\cite{milner78,nazarethnipkow}. 

2787 

2788 Directory \texttt{HOL/Lambda} contains a formalization of untyped 

2789 $\lambda$calculus in de~Bruijn notation and ChurchRosser proofs for $\beta$ 

2790 and $\eta$ reduction~\cite{NipkowCR}. 

2791 

2792 Directory \texttt{HOL/Subst} contains Martin Coen's mechanization of a theory of 

2793 substitutions and unifiers. It is based on Paulson's previous 

2794 mechanisation in {\LCF}~\cite{paulson85} of Manna and Waldinger's 

2795 theory~\cite{mw81}. It demonstrates a complicated use of \texttt{recdef}, 

2796 with nested recursion. 

2797 

2798 Directory \texttt{HOL/Induct} presents simple examples of (co)inductive 

2799 definitions and datatypes. 

2800 \begin{itemize} 

2801 \item Theory \texttt{PropLog} proves the soundness and completeness of 

2802 classical propositional logic, given a truth table semantics. The only 

2803 connective is $\imp$. A Hilbertstyle axiom system is specified, and its 

2804 set of theorems defined inductively. A similar proof in \ZF{} is 

2805 described elsewhere~\cite{paulsonsetII}. 

2806 

2807 \item Theory \texttt{Term} defines the datatype \texttt{term}. 

2808 

2809 \item Theory \texttt{ABexp} defines arithmetic and boolean expressions 

2810 as mutually recursive datatypes. 

2811 

2812 \item The definition of lazy lists demonstrates methods for handling 

2813 infinite data structures and coinduction in higherorder 

2814 logic~\cite{paulsoncoind}.% 

2815 \footnote{To be precise, these lists are \emph{potentially infinite} rather 

2816 than lazy. Lazy implies a particular operational semantics.} 

2817 Theory \thydx{LList} defines an operator for 

2818 corecursion on lazy lists, which is used to define a few simple functions 

2819 such as map and append. A coinduction principle is defined 

2820 for proving equations on lazy lists. 

2821 

2822 \item Theory \thydx{LFilter} defines the filter functional for lazy lists. 

2823 This functional is notoriously difficult to define because finding the next 

2824 element meeting the predicate requires possibly unlimited search. It is not 

2825 computable, but can be expressed using a combination of induction and 

2826 corecursion. 

2827 

2828 \item Theory \thydx{Exp} illustrates the use of iterated inductive definitions 

2829 to express a programming language semantics that appears to require mutual 

2830 induction. Iterated induction allows greater modularity. 

2831 \end{itemize} 

2832 

2833 Directory \texttt{HOL/ex} contains other examples and experimental proofs in 

2834 {\HOL}. 

2835 \begin{itemize} 

2836 \item Theory \texttt{Recdef} presents many examples of using \texttt{recdef} 

2837 to define recursive functions. Another example is \texttt{Fib}, which 

2838 defines the Fibonacci function. 

2839 

2840 \item Theory \texttt{Primes} defines the Greatest Common Divisor of two 

2841 natural numbers and proves a key lemma of the Fundamental Theorem of 

2842 Arithmetic: if $p$ is prime and $p$ divides $m\times n$ then $p$ divides~$m$ 

2843 or $p$ divides~$n$. 

2844 

2845 \item Theory \texttt{Primrec} develops some computation theory. It 

2846 inductively defines the set of primitive recursive functions and presents a 

2847 proof that Ackermann's function is not primitive recursive. 

2848 

2849 \item File \texttt{cla.ML} demonstrates the classical reasoner on over sixty 

2850 predicate calculus theorems, ranging from simple tautologies to 

2851 moderately difficult problems involving equality and quantifiers. 

2852 

2853 \item File \texttt{meson.ML} contains an experimental implementation of the {\sc 

2854 meson} proof procedure, inspired by Plaisted~\cite{plaisted90}. It is 

2855 much more powerful than Isabelle's classical reasoner. But it is less 

2856 useful in practice because it works only for pure logic; it does not 

2857 accept derived rules for the set theory primitives, for example. 

2858 

2859 \item File \texttt{mesontest.ML} contains test data for the {\sc meson} proof 

2860 procedure. These are mostly taken from Pelletier \cite{pelletier86}. 

2861 

2862 \item File \texttt{set.ML} proves Cantor's Theorem, which is presented in 

2863 \S\ref{sec:holcantor} below, and the Schr\"oderBernstein Theorem. 

2864 

2865 \item Theory \texttt{MT} contains Jacob Frost's formalization~\cite{frost93} of 

2866 Milner and Tofte's coinduction example~\cite{milnercoind}. This 

2867 substantial proof concerns the soundness of a type system for a simple 

2868 functional language. The semantics of recursion is given by a cyclic 

2869 environment, which makes a coinductive argument appropriate. 

2870 \end{itemize} 

2871 

2872 

2873 \goodbreak 

2874 \section{Example: Cantor's Theorem}\label{sec:holcantor} 

2875 Cantor's Theorem states that every set has more subsets than it has 

2876 elements. It has become a favourite example in higherorder logic since 

2877 it is so easily expressed: 

2878 \[ \forall f::\alpha \To \alpha \To bool. \exists S::\alpha\To bool. 

2879 \forall x::\alpha. f~x \not= S 

2880 \] 

2881 % 

2882 Viewing types as sets, $\alpha\To bool$ represents the powerset 

2883 of~$\alpha$. This version states that for every function from $\alpha$ to 

2884 its powerset, some subset is outside its range. 

2885 

2886 The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and 

2887 the operator \cdx{range}. 

2888 \begin{ttbox} 

2889 context Set.thy; 

2890 \end{ttbox} 

2891 The set~$S$ is given as an unknown instead of a 

2892 quantified variable so that we may inspect the subset found by the proof. 

2893 \begin{ttbox} 

2894 Goal "?S ~: range\thinspace(f :: 'a=>'a set)"; 

2895 {\out Level 0} 

2896 {\out ?S ~: range f} 

2897 {\out 1. ?S ~: range f} 

2898 \end{ttbox} 

2899 The first two steps are routine. The rule \tdx{rangeE} replaces 

2900 $\Var{S}\in \texttt{range} \, f$ by $\Var{S}=f~x$ for some~$x$. 

2901 \begin{ttbox} 

2902 by (resolve_tac [notI] 1); 

2903 {\out Level 1} 

2904 {\out ?S ~: range f} 

2905 {\out 1. ?S : range f ==> False} 

2906 \ttbreak 

2907 by (eresolve_tac [rangeE] 1); 

2908 {\out Level 2} 

2909 {\out ?S ~: range f} 

2910 {\out 1. !!x. ?S = f x ==> False} 

2911 \end{ttbox} 

2912 Next, we apply \tdx{equalityCE}, reasoning that since $\Var{S}=f~x$, 

2913 we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f~x$ for 

2914 any~$\Var{c}$. 

2915 \begin{ttbox} 

2916 by (eresolve_tac [equalityCE] 1); 

2917 {\out Level 3} 

2918 {\out ?S ~: range f} 

2919 {\out 1. !!x. [ ?c3 x : ?S; ?c3 x : f x ] ==> False} 

2920 {\out 2. !!x. [ ?c3 x ~: ?S; ?c3 x ~: f x ] ==> False} 

2921 \end{ttbox} 

2922 Now we use a bit of creativity. Suppose that~$\Var{S}$ has the form of a 

2923 comprehension. Then $\Var{c}\in\{x.\Var{P}~x\}$ implies 

2924 $\Var{P}~\Var{c}$. Destructresolution using \tdx{CollectD} 

2925 instantiates~$\Var{S}$ and creates the new assumption. 

2926 \begin{ttbox} 

2927 by (dresolve_tac [CollectD] 1); 

2928 {\out Level 4} 

2929 {\out {\ttlbrace}x. ?P7 x{\ttrbrace} ~: range f} 

2930 {\out 1. !!x. [ ?c3 x : f x; ?P7(?c3 x) ] ==> False} 

2931 {\out 2. !!x. [ ?c3 x ~: {\ttlbrace}x. ?P7 x{\ttrbrace}; ?c3 x ~: f x ] ==> False} 

2932 \end{ttbox} 

2933 Forcing a contradiction between the two assumptions of subgoal~1 

2934 completes the instantiation of~$S$. It is now the set $\{x. x\not\in 

2935 f~x\}$, which is the standard diagonal construction. 

2936 \begin{ttbox} 

2937 by (contr_tac 1); 

2938 {\out Level 5} 

2939 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} 

2940 {\out 1. !!x. [ x ~: {\ttlbrace}x. x ~: f x{\ttrbrace}; x ~: f x ] ==> False} 

2941 \end{ttbox} 

2942 The rest should be easy. To apply \tdx{CollectI} to the negated 

2943 assumption, we employ \ttindex{swap_res_tac}: 

2944 \begin{ttbox} 

2945 by (swap_res_tac [CollectI] 1); 

2946 {\out Level 6} 

2947 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} 

2948 {\out 1. !!x. [ x ~: f x; ~ False ] ==> x ~: f x} 

2949 \ttbreak 

2950 by (assume_tac 1); 

2951 {\out Level 7} 

2952 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} 

2953 {\out No subgoals!} 

2954 \end{ttbox} 

2955 How much creativity is required? As it happens, Isabelle can prove this 

2956 theorem automatically. The default classical set \texttt{claset()} contains rules 

2957 for most of the constructs of \HOL's set theory. We must augment it with 

2958 \tdx{equalityCE} to break up set equalities, and then apply bestfirst 

2959 search. Depthfirst search would diverge, but bestfirst search 

2960 successfully navigates through the large search space. 

2961 \index{search!bestfirst} 

2962 \begin{ttbox} 

2963 choplev 0; 

2964 {\out Level 0} 

2965 {\out ?S ~: range f} 

2966 {\out 1. ?S ~: range f} 

2967 \ttbreak 

2968 by (best_tac (claset() addSEs [equalityCE]) 1); 

2969 {\out Level 1} 

2970 {\out {\ttlbrace}x. x ~: f x{\ttrbrace} ~: range f} 

2971 {\out No subgoals!} 

2972 \end{ttbox} 

2973 If you run this example interactively, make sure your current theory contains 

2974 theory \texttt{Set}, for example by executing \ttindex{context}~{\tt Set.thy}. 

2975 Otherwise the default claset may not contain the rules for set theory. 

2976 \index{higherorder logic)} 

2977 

2978 %%% Local Variables: 

2979 %%% mode: latex 

2980 %%% TeXmaster: "logics" 

2981 %%% End: 