author  wenzelm 
Mon, 13 Mar 2000 13:21:39 +0100  
changeset 8434  5e4bba59bfaa 
parent 8424  a1a41257f45f 
child 8443  0ed4b608ba4b 
permissions  rwrr 
6580  1 
%% $Id$ 
2 
\chapter{HigherOrder Logic} 

3 
\index{higherorder logic(} 

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

5 

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

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

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

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

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

11 
has demonstrated that higherorder logic is widely applicable in many 

12 
areas of mathematics and computer science, not just hardware 

7490  13 
verification, {\sc hol}'s original \textit{raison d'{\^e}tre\/}. It is 
6580  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$\\ 

7490  49 
\cdx{Not} & $bool\To bool$ & negation ($\lnot$) \\ 
6580  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 \\ 

7245
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

62 
\sdx{SOME} or \tt\at & \cdx{Eps} & $(\alpha\To bool)\To\alpha$ & 
6580  63 
Hilbert description ($\varepsilon$) \\ 
7245
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

64 
\sdx{ALL} or {\tt!~} & \cdx{All} & $(\alpha\To bool)\To bool$ & 
6580  65 
universal quantifier ($\forall$) \\ 
7245
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

66 
\sdx{EX} or {\tt?~} & \cdx{Ex} & $(\alpha\To bool)\To bool$ & 
6580  67 
existential quantifier ($\exists$) \\ 
7245
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

68 
\texttt{EX!} or {\tt?!} & \cdx{Ex1} & $(\alpha\To bool)\To bool$ & 
6580  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$} \\ 

7245
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

102 
&  & "SOME~" id " . " formula 
6580  103 
&  & "\at~" id " . " formula \\ 
104 
&  & 

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

106 
&  & 

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

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

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

110 
&  & term " = " term \\ 

111 
&  & term " \ttilde= " term \\ 

112 
&  & term " < " term \\ 

113 
&  & term " <= " term \\ 

114 
&  & "\ttilde\ " formula \\ 

115 
&  & formula " \& " formula \\ 

116 
&  & formula "  " formula \\ 

117 
&  & formula " > " formula \\ 

7245
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

118 
&  & "ALL~" id~id^* " . " formula 
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

119 
&  & "!~~~" id~id^* " . " formula \\ 
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

120 
&  & "EX~~" id~id^* " . " formula 
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

121 
&  & "?~~~" id~id^* " . " formula \\ 
6580  122 
&  & "EX!~" id~id^* " . " formula 
7245
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

123 
&  & "?!~~" id~id^* " . " formula \\ 
6580  124 
\end{array} 
125 
\] 

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

127 
\end{figure} 

128 

129 

130 
\section{Syntax} 

131 

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

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

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

7490  135 
$\lnot(a=b)$. 
6580  136 

137 
\begin{warn} 

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

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

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

7490  141 
$\lnot\lnot P=P$ abbreviates $\lnot\lnot (P=P)$ and not $(\lnot\lnot P)=P$. 
6580  142 
When using $=$ to mean logical equivalence, enclose both operands in 
143 
parentheses. 

144 
\end{warn} 

145 

146 
\subsection{Types and classes} 

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

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

149 
particular the equality symbol and quantifiers are polymorphic over 

150 
class \texttt{term}. 

151 

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

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

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

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

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

157 
functions. 

158 

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

7490  160 
See~{\S}\ref{sec:HOL:Types} and~{\S}\ref{sec:HOL:datatype}. 
6580  161 

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

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

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

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

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

7490  167 
(w.r.t.\ $\leq$). 
6580  168 

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

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

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

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

173 
on natural numbers. 

174 

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

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

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

7490  178 
variables $i$, $j$ and $k$ in the goal $i \leq j \Imp i \leq j+k$ have type 
6580  179 
$\alpha::\{ord,plus\}$, although you may have expected them to have some 
180 
numeric type, e.g. $nat$. Instead you should have stated the goal as 

7490  181 
$(i::nat) \leq j \Imp i \leq j+k$, which causes all three variables to have 
6580  182 
type $nat$. 
183 

184 
\begin{warn} 

185 
If resolution fails for no obvious reason, try setting 

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

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

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

189 

190 
\index{unification!incompleteness of} 

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

192 
guarantee to find instantiations for type variables automatically. Be 

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

194 
possibly instantiating type variables. Setting 

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

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

197 
\end{warn} 

198 

199 

200 
\subsection{Binders} 

201 

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

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

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

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

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

7245
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

207 
\hbox{\tt SOME~$x$.~$P[x]$}. 
6580  208 

209 
Existential quantification is defined by 

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

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

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

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

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

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

216 

7245
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

217 
\medskip 
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

218 

65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

219 
\index{*"! symbol}\index{*"? symbol}\index{HOL system@{\sc hol} system} The 
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

220 
basic Isabelle/HOL binders have two notations. Apart from the usual 
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

221 
\texttt{ALL} and \texttt{EX} for $\forall$ and $\exists$, Isabelle/HOL also 
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

222 
supports the original notation of Gordon's {\sc hol} system: \texttt{!}\ 
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

223 
and~\texttt{?}. In the latter case, the existential quantifier \emph{must} be 
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

224 
followed by a space; thus {\tt?x} is an unknown, while \verb'? x. f x=y' is a 
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

225 
quantification. Both notations are accepted for input. The print mode 
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

226 
``\ttindexbold{HOL}'' governs the output notation. If enabled (e.g.\ by 
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

227 
passing option \texttt{m HOL} to the \texttt{isabelle} executable), 
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

228 
then~{\tt!}\ and~{\tt?}\ are displayed. 
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

229 

65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

230 
\medskip 
6580  231 

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

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

7490  234 
to be the least (w.r.t.\ $\leq$) $x$ such that $P~x$ holds (see 
6580  235 
Fig.~\ref{holdefs}). The definition uses Hilbert's $\varepsilon$ 
236 
choice operator, so \texttt{Least} is always meaningful, but may yield 

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

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

7490  239 
$\leq$ need not be a wellordering, not even an order at all!} 
6580  240 

241 
\medskip All these binders have priority 10. 

242 

243 
\begin{warn} 

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

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

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

247 
\end{warn} 

248 

249 

6620  250 
\subsection{The let and case constructions} 
6580  251 
Local abbreviations can be introduced by a \texttt{let} construct whose 
252 
syntax appears in Fig.\ts\ref{holgrammar}. Internally it is translated into 

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

254 
definition, \tdx{Let_def}. 

255 

256 
\HOL\ also defines the basic syntax 

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

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

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

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

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

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

7490  263 
(see~{\S}\ref{sec:HOL:datatype}). 
6580  264 

265 
\begin{warn} 

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

267 
quantifiers, which requires additional enclosing parentheses in the context 

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

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

270 
else\dots})$. 

271 
\end{warn} 

272 

273 
\section{Rules of inference} 

274 

275 
\begin{figure} 

276 
\begin{ttbox}\makeatother 

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

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

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

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

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

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

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

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

285 
\end{ttbox} 

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

287 
\end{figure} 

288 

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

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

291 
comments: 

292 
\begin{ttdescription} 

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

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

295 
equal. 

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

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

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

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

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

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

302 
\end{ttdescription} 

303 

304 

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

306 
\begin{ttbox}\makeatother 

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

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

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

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

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

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

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

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

315 

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

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

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

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

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

321 
\end{ttbox} 

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

323 
\end{figure} 

324 

325 

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

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

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

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

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

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

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

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

334 
\begin{warn} 

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

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

337 
or, better still, using highlevel tactics 

7490  338 
(see~{\S}\ref{sec:HOL:genericpackages}). 
6580  339 
\end{warn} 
340 

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

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

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

344 

345 

346 
\begin{figure} 

347 
\begin{ttbox} 

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

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

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

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

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

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

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

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

356 
\subcaption{Equality} 

357 

358 
\tdx{TrueI} True 

359 
\tdx{FalseE} False ==> P 

360 

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

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

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

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

365 

366 
\tdx{disjI1} P ==> PQ 

367 
\tdx{disjI2} Q ==> PQ 

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

369 

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

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

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

373 
\subcaption{Propositional logic} 

374 

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

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

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

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

379 
% 

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

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

382 
\subcaption{Logical equivalence} 

383 

384 
\end{ttbox} 

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

386 
\end{figure} 

387 

388 

389 
\begin{figure} 

390 
\begin{ttbox}\makeatother 

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

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

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

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

395 

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

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

398 

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

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

401 
] ==> R 

402 

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

404 
\subcaption{Quantifiers and descriptions} 

405 

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

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

408 
\tdx{excluded_middle} ~P  P 

409 

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

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

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

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

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

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

416 
\subcaption{Classical logic} 

417 

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

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

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

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

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

423 
\subcaption{Conditionals} 

424 
\end{ttbox} 

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

426 
\end{figure} 

427 

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

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

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

431 
conjunctions, implications, and universal quantifiers. 

432 

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

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

435 
simplifying both sides of an equation. 

436 

437 
The following simple tactics are occasionally useful: 

438 
\begin{ttdescription} 

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

440 
repeatedly to remove all outermost universal quantifiers and implications 

441 
from subgoal $i$. 

8424  442 
\item[\ttindexbold{cases_tac} {\tt"}$P${\tt"} $i$] performs case distinction 
6580  443 
on $P$ for subgoal $i$: the latter is replaced by two identical subgoals 
7490  444 
with the added assumptions $P$ and $\lnot P$, respectively. 
445 
\item[\ttindexbold{smp_tac} $j$ $i$] applies $j$ times \texttt{spec} and then 

446 
\texttt{mp} in subgoal $i$, which is typically useful when forwardchaining 

447 
from an induction hypothesis. As a generalization of \texttt{mp_tac}, 

448 
if there are assumptions $\forall \vec{x}. P \vec{x} \imp Q \vec{x}$ and 

449 
$P \vec{a}$, ($\vec{x}$ being a vector of $j$ variables) 

450 
then it replaces the universally quantified implication by $Q \vec{a}$. 

451 
It may instantiate unknowns. It fails if it can do nothing. 

6580  452 
\end{ttdescription} 
453 

454 

455 
\begin{figure} 

456 
\begin{center} 

457 
\begin{tabular}{rrr} 

458 
\it name &\it metatype & \it description \\ 

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

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

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

462 
& insertion of element \\ 

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

464 
& comprehension \\ 

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

466 
& complement \\ 

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

468 
& intersection over a set\\ 

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

470 
& union over a set\\ 

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

472 
&set of sets intersection \\ 

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

474 
&set of sets union \\ 

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

476 
& powerset \\[1ex] 

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

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

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

480 
& bounded quantifiers 

481 
\end{tabular} 

482 
\end{center} 

483 
\subcaption{Constants} 

484 

485 
\begin{center} 

486 
\begin{tabular}{llrrr} 

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

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

489 
intersection over a type\\ 

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

491 
union over a type 

492 
\end{tabular} 

493 
\end{center} 

494 
\subcaption{Binders} 

495 

496 
\begin{center} 

497 
\index{*"`"` symbol} 

498 
\index{*": symbol} 

499 
\index{*"<"= symbol} 

500 
\begin{tabular}{rrrr} 

501 
\it symbol & \it metatype & \it priority & \it description \\ 

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

503 
& Left 90 & image \\ 

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

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

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

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

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

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

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

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

512 
\end{tabular} 

513 
\end{center} 

514 
\subcaption{Infixes} 

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

516 
\end{figure} 

517 

518 

519 
\begin{figure} 

520 
\begin{center} \tt\frenchspacing 

521 
\index{*"! symbol} 

522 
\begin{tabular}{rrr} 

523 
\it external & \it internal & \it description \\ 

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

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

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

527 
\rm comprehension \\ 

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

529 
\rm intersection \\ 

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

531 
\rm union \\ 

7245
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

532 
\sdx{ALL} $x$:$A$. $P[x]$ or \sdx{!} $x$:$A$. $P[x]$ & 
6580  533 
Ball $A$ $\lambda x. P[x]$ & 
534 
\rm bounded $\forall$ \\ 

7245
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

535 
\sdx{EX}{\tt\ } $x$:$A$. $P[x]$ or \sdx{?} $x$:$A$. $P[x]$ & 
6580  536 
Bex $A$ $\lambda x. P[x]$ & \rm bounded $\exists$ 
537 
\end{tabular} 

538 
\end{center} 

539 
\subcaption{Translations} 

540 

541 
\dquotes 

542 
\[\begin{array}{rclcl} 

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

544 
&  & "{\ttlbrace}{\ttrbrace}" \\ 

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

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

547 
&  & term " `` " term \\ 

548 
&  & term " Int " term \\ 

549 
&  & term " Un " term \\ 

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

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

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

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

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

555 
&  & term " : " term \\ 

556 
&  & term " \ttilde: " term \\ 

557 
&  & term " <= " term \\ 

7245
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

558 
&  & "ALL " id ":" term " . " formula 
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

559 
&  & "!~" id ":" term " . " formula \\ 
6580  560 
&  & "EX~~" id ":" term " . " formula 
7245
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

561 
&  & "?~" id ":" term " . " formula \\ 
6580  562 
\end{array} 
563 
\] 

564 
\subcaption{Full Grammar} 

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

566 
\end{figure} 

567 

568 

569 
\section{A formulation of set theory} 

570 
Historically, higherorder logic gives a foundation for Russell and 

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

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

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

574 
\begin{itemize} 

575 
\item 

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

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

578 
\item 

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

580 
may be defined by absolute comprehension. 

581 
\item 

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

583 
have a more complex type. 

584 
\end{itemize} 

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

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

587 
denoting the universal set for the given type. 

588 

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

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

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

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

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

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

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

596 

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

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

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

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

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

7490  602 
$\lnot(a\in b)$. 
6580  603 

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

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

606 
\begin{eqnarray*} 

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

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

609 
\end{eqnarray*} 

610 

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

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

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

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

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

616 

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

618 
\begin{eqnarray*} 

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

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

621 
\end{eqnarray*} 

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

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

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

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

626 
% 

7245
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

627 
\hbox{\tt ALL~$x$:$A$.\ $P[x]$} and \hbox{\tt EX~$x$:$A$.\ $P[x]$}. The 
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

628 
original notation of Gordon's {\sc hol} system is supported as well: \sdx{!}\ 
65ccac4e1f3f
eliminated HOL_quantifiers (replaced by "HOL" print mode);
wenzelm
parents:
7044
diff
changeset

629 
and \sdx{?}. 
6580  630 

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

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

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

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

635 

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

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

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

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

640 

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

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

643 
respectively. 

644 

645 

646 

647 
\begin{figure} \underscoreon 

648 
\begin{ttbox} 

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

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

651 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

670 
\end{ttbox} 

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

672 
\end{figure} 

673 

674 

675 
\begin{figure} \underscoreon 

676 
\begin{ttbox} 

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

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

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

680 

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

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

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

684 

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

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

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

688 
\subcaption{Comprehension and Bounded quantifiers} 

689 

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

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

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

693 

694 
\tdx{subset_refl} A <= A 

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

696 

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

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

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

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

701 

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

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

704 
] ==> P 

705 
\subcaption{The subset and equality relations} 

706 
\end{ttbox} 

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

708 
\end{figure} 

709 

710 

711 
\begin{figure} \underscoreon 

712 
\begin{ttbox} 

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

714 

715 
\tdx{insertI1} a : insert a B 

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

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

718 

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

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

721 

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

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

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

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

726 

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

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

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

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

731 

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

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

734 

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

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

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

738 

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

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

741 

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

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

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

745 

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

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

748 

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

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

751 

752 
\tdx{rangeI} f x : range f 

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

754 
\end{ttbox} 

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

756 
\end{figure} 

757 

758 

759 
\subsection{Axioms and rules of set theory} 

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

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

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

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

764 

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

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

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

768 
and \texttt{range}. 

769 

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

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

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

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

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

775 

776 
%\begin{figure} \underscoreon 

777 
%\begin{ttbox} 

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

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

780 
% 

781 
%\tdx{Inv_injective} 

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

783 
% 

784 
% 

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

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

787 
% 

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

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

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

791 
% 

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

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

794 
% 

795 
%\tdx{inj_on_inverseI} 

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

797 
%\tdx{inj_on_contraD} 

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

799 
%\end{ttbox} 

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

801 
%\end{figure} 

802 

803 

804 
\begin{figure} \underscoreon 

805 
\begin{ttbox} 

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

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

808 

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

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

811 

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

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

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

815 

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

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

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

819 
\end{ttbox} 

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

821 
\end{figure} 

822 

823 

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

825 
\begin{ttbox} 

826 
\tdx{Int_absorb} A Int A = A 

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

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

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

830 

831 
\tdx{Un_absorb} A Un A = A 

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

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

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

835 

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

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

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

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

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

841 

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

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

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

845 

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

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

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

849 
\end{ttbox} 

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

851 
\end{figure} 

852 

853 

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

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

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

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

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

859 
strictly necessary but yield more natural proofs. Similarly, 

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

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

862 
proofs pertaining to set theory. 

863 

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

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

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

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

868 

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

870 
include commutative, associative and distributive laws involving unions, 

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

872 
HOL/equalities.ML}. 

873 

874 
\begin{warn} 

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

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

877 
\end{warn} 

878 

879 
\begin{figure} 

880 
\begin{center} 

881 
\begin{tabular}{rrr} 

882 
\it name &\it metatype & \it description \\ 

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

884 
& injective/surjective \\ 

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

886 
& injective over subset\\ 

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

888 
\end{tabular} 

889 
\end{center} 

890 

891 
\underscoreon 

892 
\begin{ttbox} 

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

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

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

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

897 
\end{ttbox} 

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

899 
\end{figure} 

900 

901 
\subsection{Properties of functions}\nopagebreak 

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

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

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

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

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

907 

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

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

910 

7283  911 

6580  912 
\section{Generic packages} 
913 
\label{sec:HOL:genericpackages} 

914 

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

916 
simplifier and the classical reasoner. 

917 

918 
\subsection{Simplification and substitution} 

919 

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

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

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

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

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

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

926 
simplification rules. 

927 

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

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

930 
and simplification. 

931 

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

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

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

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

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

937 
\end{warn} 

938 

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

940 
of nontermination or because its lefthand side is too flexible  

941 
then you might try \texttt{stac}: 

942 
\begin{ttdescription} 

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

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

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

946 
may be necessary to select the desired ones. 

947 

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

949 
additional (first) subgoal. 

950 
\end{ttdescription} 

951 

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

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

954 
\HOL's general substitution rule. 

955 

956 
\subsubsection{Case splitting} 

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

958 

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

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

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

962 
expressed by the theorem \tdx{split_if}: 

963 
$$ 

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

7490  965 
((\Var{b} \to \Var{P}(\Var{x})) \land (\lnot \Var{b} \to \Var{P}(\Var{y}))) 
6580  966 
\eqno{(*)} 
967 
$$ 

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

969 
\[ 

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

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

972 
\] 

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

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

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

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

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

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

979 
simpset, as in 

980 
\begin{ttbox} 

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

982 
\end{ttbox} 

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

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

985 
\texttt{if} have been eliminated. 

986 

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

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

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

990 
the inverse of \texttt{addsplits}: 

991 
\begin{ttbox} 

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

993 
\end{ttbox} 

994 

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

996 
\[ 

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

998 
\] 

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

1000 
right form because internally the lefthand side is 

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

7490  1002 
are splitting rules for \texttt{case} expressions (see~{\S}\ref{subsec:list} 
1003 
and~{\S}\ref{subsec:datatype:basics}). 

6580  1004 

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

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

1007 
\begin{ttbox} 

1008 
\ttindexbold{Addsplits}: thm list > unit 

1009 
\ttindexbold{Delsplits}: thm list > unit 

1010 
\end{ttbox} 

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

1012 

1013 
\subsection{Classical reasoning} 

1014 

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

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

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

1018 

7283  1019 
The classical reasoner is installed. Tactics such as \texttt{Blast_tac} and 
1020 
{\tt Best_tac} refer to the default claset (\texttt{claset()}), which works 

1021 
for most purposes. Named clasets include \ttindexbold{prop_cs}, which 

1022 
includes the propositional rules, and \ttindexbold{HOL_cs}, which also 

1023 
includes quantifier rules. See the file \texttt{HOL/cladata.ML} for lists of 

1024 
the classical rules, 

6580  1025 
and \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% 
1026 
{Chap.\ts\ref{chap:classical}} for more discussion of classical proof methods. 

1027 

1028 

7283  1029 
\section{Calling the decision procedure SVC}\label{sec:HOL:SVC} 
1030 

1031 
\index{SVC decision procedure(} 

1032 

1033 
The Stanford Validity Checker (SVC) is a tool that can check the validity of 

1034 
certain types of formulae. If it is installed on your machine, then 

1035 
Isabelle/HOL can be configured to call it through the tactic 

1036 
\ttindex{svc_tac}. It is ideal for large tautologies and complex problems in 

1037 
linear arithmetic. Subexpressions that SVC cannot handle are automatically 

1038 
replaced by variables, so you can call the tactic on any subgoal. See the 

1039 
file \texttt{HOL/ex/svc_test.ML} for examples. 

1040 
\begin{ttbox} 

1041 
svc_tac : int > tactic 

1042 
Svc.trace : bool ref \hfill{\bf initially false} 

1043 
\end{ttbox} 

1044 

1045 
\begin{ttdescription} 

1046 
\item[\ttindexbold{svc_tac} $i$] attempts to prove subgoal~$i$ by translating 

1047 
it into a formula recognized by~SVC\@. If it succeeds then the subgoal is 

1048 
removed. It fails if SVC is unable to prove the subgoal. It crashes with 

1049 
an error message if SVC appears not to be installed. Numeric variables may 

1050 
have types \texttt{nat}, \texttt{int} or \texttt{real}. 

1051 

1052 
\item[\ttindexbold{Svc.trace}] is a flag that, if set, causes \texttt{svc_tac} 

1053 
to trace its operations: abstraction of the subgoal, translation to SVC 

1054 
syntax, SVC's response. 

1055 
\end{ttdescription} 

1056 

1057 
Here is an example, with tracing turned on: 

1058 
\begin{ttbox} 

1059 
set Svc.trace; 

1060 
{\out val it : bool = true} 

1061 
Goal "(#3::nat)*a <= #2 + #4*b + #6*c & #11 <= #2*a + b + #2*c & \ttback 

1062 
\ttback a + #3*b <= #5 + #2*c > #2 + #3*b <= #2*a + #6*c"; 

1063 

1064 
by (svc_tac 1); 

1065 
{\out Subgoal abstracted to} 

1066 
{\out #3 * a <= #2 + #4 * b + #6 * c &} 

1067 
{\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c >} 

1068 
{\out #2 + #3 * b <= #2 * a + #6 * c} 

1069 
{\out Calling SVC:} 

1070 
{\out (=> (<= 0 (F_c) ) (=> (<= 0 (F_b) ) (=> (<= 0 (F_a) )} 

1071 
{\out (=> (AND (<= {* 3 (F_a) } {+ {+ 2 {* 4 (F_b) } } } 

1072 
{\out {* 6 (F_c) } } ) (AND (<= 11 {+ {+ {* 2 (F_a) } (F_b) }} 

1073 
{\out {* 2 (F_c) } } ) (<= {+ (F_a) {* 3 (F_b) } } {+ 5 } 

1074 
{\out {* 2 (F_c) } } ) ) ) (< {+ 2 {* 3 (F_b) } } {+ 1 {+ } 

1075 
{\out {* 2 (F_a) } {* 6 (F_c) } } } ) ) ) ) ) } 

1076 
{\out SVC Returns:} 

1077 
{\out VALID} 

1078 
{\out Level 1} 

1079 
{\out #3 * a <= #2 + #4 * b + #6 * c &} 

1080 
{\out #11 <= #2 * a + b + #2 * c & a + #3 * b <= #5 + #2 * c >} 

1081 
{\out #2 + #3 * b <= #2 * a + #6 * c} 

1082 
{\out No subgoals!} 

1083 
\end{ttbox} 

1084 

1085 

1086 
\begin{warn} 

1087 
Calling \ttindex{svc_tac} entails an aboveaverage risk of 

1088 
unsoundness. Isabelle does not check SVC's result independently. Moreover, 

1089 
the tactic translates the submitted formula using code that lies outside 

1090 
Isabelle's inference core. Theorems that depend upon results proved using SVC 

1091 
(and other oracles) are displayed with the annotation \texttt{[!]} attached. 

1092 
You can also use \texttt{\#der (rep_thm $th$)} to examine the proof object of 

1093 
theorem~$th$, as described in the \emph{Reference Manual}. 

1094 
\end{warn} 

1095 

1096 
To start, first download SVC from the Internet at URL 

1097 
\begin{ttbox} 

1098 
http://agamemnon.stanford.edu/~levitt/vc/index.html 

1099 
\end{ttbox} 

1100 
and install it using the instructions supplied. SVC requires two environment 

1101 
variables: 

1102 
\begin{ttdescription} 

1103 
\item[\ttindexbold{SVC_HOME}] is an absolute pathname to the SVC 

1104 
distribution directory. 

1105 

1106 
\item[\ttindexbold{SVC_MACHINE}] identifies the type of computer and 

1107 
operating system. 

1108 
\end{ttdescription} 

1109 
You can set these environment variables either using the Unix shell or through 

1110 
an Isabelle \texttt{settings} file. Isabelle assumes SVC to be installed if 

1111 
\texttt{SVC_HOME} is defined. 

1112 

1113 
\paragraph*{Acknowledgement.} This interface uses code supplied by S{\o}ren 

1114 
Heilmann. 

1115 

1116 

1117 
\index{SVC decision procedure)} 

1118 

1119 

1120 

1121 

6580  1122 
\section{Types}\label{sec:HOL:Types} 
1123 
This section describes \HOL's basic predefined types ($\alpha \times 

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

1125 
introducing new types in general. The most important type 

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

7490  1127 
{\S}\ref{sec:HOL:datatype}. 
6580  1128 

1129 

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

1131 
\label{subsec:prodsum} 

1132 

1133 
\begin{figure}[htbp] 

1134 
\begin{constants} 

1135 
\it symbol & \it metatype & & \it description \\ 

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

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

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

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

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

1141 
& & generalized projection\\ 

1142 
\cdx{Sigma} & 

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

1144 
& general sum of sets 

1145 
\end{constants} 

1146 
\begin{ttbox}\makeatletter 

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

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

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

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

1151 

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

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

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

1155 

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

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

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

1159 

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

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

1162 

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

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

1165 
\end{ttbox} 

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

1167 
\end{figure} 

1168 

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

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

1171 
tuples are simulated by pairs nested to the right: 

1172 
\begin{center} 

1173 
\begin{tabular}{cc} 

1174 
external & internal \\ 

1175 
\hline 

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

1177 
\hline 

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

1179 
\end{tabular} 

1180 
\end{center} 

1181 
In addition, it is possible to use tuples 

1182 
as patterns in abstractions: 

1183 
\begin{center} 

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

1185 
\end{center} 

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

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

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

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

1190 
\begin{warn} 

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

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

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

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

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

1196 
\end{warn} 

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

1198 
variable binding construct which is internally described by a 

1199 
$\lambda$abstraction. Some important examples are 

1200 
\begin{description} 

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

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

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

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

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

1206 
\end{description} 

1207 

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

1209 
\begin{ttdescription} 

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

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

1212 
each component. A simple example: 

1213 
\begin{ttbox} 

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

1215 
by(split_all_tac 1); 

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

1217 
\end{ttbox} 

1218 
\end{ttdescription} 

1219 

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

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

1222 
\begin{ttbox} 

1223 
\tdx{unit_eq} u = () 

1224 
\end{ttbox} 

1225 
\bigskip 

1226 

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

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

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

1230 

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

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

7325  1233 
respective theory files. Although the sum and product types are 
1234 
constructed manually for foundational reasons, they are represented as 

7490  1235 
actual datatypes later (see {\S}\ref{subsec:datatype:rep_datatype}). 
7325  1236 
Therefore, the theory \texttt{Datatype} should be used instead of 
1237 
\texttt{Sum} or \texttt{Prod}. 

6580  1238 

1239 
\begin{figure} 

1240 
\begin{constants} 

1241 
\it symbol & \it metatype & & \it description \\ 

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

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

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

1245 
& & conditional 

1246 
\end{constants} 

1247 
\begin{ttbox}\makeatletter 

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

1249 

1250 
\tdx{inj_Inl} inj Inl 

1251 
\tdx{inj_Inr} inj Inr 

1252 

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

1254 

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

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

1257 

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

7325  1259 
\tdx{sum.split_case} R(sum_case f g s) = ((! x. s = Inl(x) > R(f(x))) & 
6580  1260 
(! y. s = Inr(y) > R(g(y)))) 
1261 
\end{ttbox} 

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

1263 
\end{figure} 

1264 

1265 
\begin{figure} 

1266 
\index{*"< symbol} 

1267 
\index{*"* symbol} 

1268 
\index{*div symbol} 

1269 
\index{*mod symbol} 

1270 
\index{*"+ symbol} 

1271 
\index{*" symbol} 

1272 
\begin{constants} 

1273 
\it symbol & \it metatype & \it priority & \it description \\ 

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

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

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

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

1278 
% & & primitive recursor\\ 

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

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

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

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

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

1284 
\end{constants} 

1285 
\subcaption{Constants and infixes} 

1286 

1287 
\begin{ttbox}\makeatother 

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

1289 

1290 
\tdx{Suc_not_Zero} Suc m ~= 0 

1291 
\tdx{inj_Suc} inj Suc 

1292 
\tdx{n_not_Suc_n} n~=Suc n 

1293 
\subcaption{Basic properties} 

1294 
\end{ttbox} 

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

1296 
\end{figure} 

1297 

1298 

1299 
\begin{figure} 

1300 
\begin{ttbox}\makeatother 

1301 
0+n = n 

1302 
(Suc m)+n = Suc(m+n) 

1303 

1304 
m0 = m 

1305 
0n = n 

1306 
Suc(m)Suc(n) = mn 

1307 

1308 
0*n = 0 

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

1310 

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

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

1313 

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

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

1316 
\end{ttbox} 

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

1318 
\end{figure} 

1319 

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

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

1322 

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

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

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

1326 
natural numbers are inductively generated by choosing an arbitrary individual 

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

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

1329 

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

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

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

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

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

1335 

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

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

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

1339 
proved include commutative, associative, distributive, identity and 

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

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

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

1343 

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

7490  1345 
see {\S}\ref{sec:HOL:recursive}. A simple example is addition. 
6580  1346 
Here, \texttt{op +} is the name of the infix operator~\texttt{+}, following 
1347 
the standard convention. 

1348 
\begin{ttbox} 

1349 
\sdx{primrec} 

1350 
"0 + n = n" 

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

1352 
\end{ttbox} 

1353 
There is also a \sdx{case}construct 

1354 
of the form 

1355 
\begin{ttbox} 

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

1357 
\end{ttbox} 

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

1359 
the order of the two cases. 

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

7325  1361 
\cdx{nat_rec}, which is available because \textit{nat} is represented as 
7490  1362 
a datatype (see {\S}\ref{subsec:datatype:rep_datatype}). 
6580  1363 

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

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

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

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

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

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

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

1371 

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

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

1374 
theorem \tdx{less_induct}: 

1375 
\begin{ttbox} 

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

1377 
\end{ttbox} 

1378 

1379 

1380 
Reasoning about arithmetic inequalities can be tedious. Fortunately HOL 

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

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

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

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

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

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

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

1388 
subformulae are ignored unless they are positive universal or negative 

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

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

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

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

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

1394 

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

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

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

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

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

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

1401 

1402 
\begin{figure} 

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

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

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

1406 
\index{*"! symbol} 

1407 
\begin{constants} 

1408 
\it symbol & \it metatype & \it priority & \it description \\ 

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

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

1411 
list constructor \\ 

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

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

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

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

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

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

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

1419 
& & apply to all\\ 

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

1421 
& & filter functional\\ 

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

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

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

1425 
& iteration \\ 

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

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

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

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

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

1431 
take or drop a prefix \\ 

1432 
\cdx{takeWhile},\\ 

1433 
\cdx{dropWhile} & 

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

1435 
take or drop a prefix 

1436 
\end{constants} 

1437 
\subcaption{Constants and infixes} 

1438 

1439 
\begin{center} \tt\frenchspacing 

1440 
\begin{tabular}{rrr} 

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

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

1443 
\rm finite list \\{} 

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

1445 
\rm list comprehension 

1446 
\end{tabular} 

1447 
\end{center} 

1448 
\subcaption{Translations} 

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

1450 
\end{figure} 

1451 

1452 

1453 
\begin{figure} 

1454 
\begin{ttbox}\makeatother 

1455 
null [] = True 

1456 
null (x#xs) = False 

1457 

1458 
hd (x#xs) = x 

1459 
tl (x#xs) = xs 

1460 
tl [] = [] 

1461 

1462 
[] @ ys = ys 

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

1464 

1465 
map f [] = [] 

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

1467 

1468 
filter P [] = [] 

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

1470 

1471 
set [] = \ttlbrace\ttrbrace 

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

1473 

1474 
x mem [] = False 

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

1476 

1477 
foldl f a [] = a 

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

1479 

1480 
concat([]) = [] 

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

1482 

1483 
rev([]) = [] 

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

1485 

1486 
length([]) = 0 

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

1488 

1489 
xs!0 = hd xs 

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

1491 

1492 
take n [] = [] 

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

1494 

1495 
drop n [] = [] 

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