author  paulson 
Fri, 30 Jun 2000 17:51:56 +0200  
changeset 9212  4afe62073b41 
parent 8628  b3d9d8446473 
child 9258  2121ff73a37d 
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 

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

146 
\subsection{Types and overloading} 
6580  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 

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

159 
\HOL\ allows new types to be declared as subsets of existing types; 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

160 
see~{\S}\ref{sec:HOL:Types}. MLlike datatypes can also be declared; see 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

161 
~{\S}\ref{sec:HOL:datatype}. 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

162 

4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

163 
Several syntactic type classes  \cldx{plus}, \cldx{minus}, 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

164 
\cldx{times} and 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

165 
\cldx{power}  permit overloading of the operators {\tt+},\index{*"+ 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

166 
symbol} {\tt}\index{*" symbol}, {\tt*}.\index{*"* symbol} 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

167 
and \verb^.\index{^@\verb.^. symbol} 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

168 
% 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

169 
They are overloaded to denote the obvious arithmetic operations on types 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

170 
\tdx{nat}, \tdx{int} and~\tdx{real}. (With the \verb^ operator, the 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

171 
exponent always has type~\tdx{nat}.) Nonarithmetic overloadings are also 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

172 
done: the operator {\tt} can denote set difference, while \verb^ can 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

173 
denote exponentiation of relations (iterated composition). Unary minus is 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

174 
also written as~{\tt} and is overloaded like its 2place counterpart; it even 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

175 
can stand for set complement. 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

176 

4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

177 
The constant \cdx{0} is also overloaded. It serves as the zero element of 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

178 
several types, of which the most important is \tdx{nat} (the natural 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

179 
numbers). The type class \cldx{plus_ac0} comprises all types for which 0 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

180 
and~+ satisfy the laws $x+y=y+x$, $(x+y)+z = x+(y+z)$ and $0+x = x$. These 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

181 
types include the numeric ones \tdx{nat}, \tdx{int} and~\tdx{real} and also 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

182 
multisets. The summation operator \cdx{setsum} is available for all types in 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

183 
this class. 
6580  184 

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

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

186 
signatures. The relations $<$ and $\leq$ are polymorphic over this 
6580  187 
class, as are the functions \cdx{mono}, \cdx{min} and \cdx{max}, and 
188 
the \cdx{LEAST} operator. \thydx{Ord} also defines a subclass 

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

189 
\cldx{order} of \cldx{ord} which axiomatizes the types that are partially 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

190 
ordered with respect to~$\leq$. A further subclass \cldx{linorder} of 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

191 
\cldx{order} axiomatizes linear orderings. 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

192 
For details, see the file \texttt{Ord.thy}. 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

193 

6580  194 
If you state a goal containing overloaded functions, you may need to include 
195 
type constraints. Type inference may otherwise make the goal more 

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

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

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

203 
\begin{warn} 

204 
If resolution fails for no obvious reason, try setting 

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

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

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

208 

209 
\index{unification!incompleteness of} 

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

211 
guarantee to find instantiations for type variables automatically. Be 

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

213 
possibly instantiating type variables. Setting 

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

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

216 
\end{warn} 

217 

218 

219 
\subsection{Binders} 

220 

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

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

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

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

225 
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

226 
\hbox{\tt SOME~$x$.~$P[x]$}. 
6580  227 

228 
Existential quantification is defined by 

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

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

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

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

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

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

235 

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

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

237 

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

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

239 
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

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

241 
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

242 
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

243 
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

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

245 
``\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

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

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

248 

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

249 
\medskip 
6580  250 

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

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

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

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

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

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

260 
\medskip All these binders have priority 10. 

261 

262 
\begin{warn} 

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

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

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

266 
\end{warn} 

267 

268 

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

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

273 
definition, \tdx{Let_def}. 

274 

275 
\HOL\ also defines the basic syntax 

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

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

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

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

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

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

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

284 
\begin{warn} 

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

286 
quantifiers, which requires additional enclosing parentheses in the context 

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

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

289 
else\dots})$. 

290 
\end{warn} 

291 

292 
\section{Rules of inference} 

293 

294 
\begin{figure} 

295 
\begin{ttbox}\makeatother 

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

296 
\tdx{refl} t = (t::'a) 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

297 
\tdx{subst} [ s = t; P s ] ==> P (t::'a) 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

298 
\tdx{ext} (!!x::'a. (f x :: 'b) = g x) ==> (\%x. f x) = (\%x. g x) 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

299 
\tdx{impI} (P ==> Q) ==> P>Q 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

300 
\tdx{mp} [ P>Q; P ] ==> Q 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

301 
\tdx{iff} (P>Q) > (Q>P) > (P=Q) 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

302 
\tdx{selectI} P(x::'a) ==> P(@x. P x) 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

303 
\tdx{True_or_False} (P=True)  (P=False) 
6580  304 
\end{ttbox} 
305 
\caption{The \texttt{HOL} rules} \label{holrules} 

306 
\end{figure} 

307 

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

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

310 
comments: 

311 
\begin{ttdescription} 

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

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

314 
equal. 

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

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

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

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

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

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

321 
\end{ttdescription} 

322 

323 

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

325 
\begin{ttbox}\makeatother 

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

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

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

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

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

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

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

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

334 

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

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

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

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

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

340 
\end{ttbox} 

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

342 
\end{figure} 

343 

344 

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

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

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

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

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

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

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

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

353 
\begin{warn} 

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

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

356 
or, better still, using highlevel tactics 

7490  357 
(see~{\S}\ref{sec:HOL:genericpackages}). 
6580  358 
\end{warn} 
359 

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

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

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

363 

364 

365 
\begin{figure} 

366 
\begin{ttbox} 

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

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

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

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

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

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

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

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

375 
\subcaption{Equality} 

376 

377 
\tdx{TrueI} True 

378 
\tdx{FalseE} False ==> P 

379 

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

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

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

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

384 

385 
\tdx{disjI1} P ==> PQ 

386 
\tdx{disjI2} Q ==> PQ 

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

388 

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

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

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

392 
\subcaption{Propositional logic} 

393 

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

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

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

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

398 
% 

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

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

401 
\subcaption{Logical equivalence} 

402 

403 
\end{ttbox} 

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

405 
\end{figure} 

406 

407 

408 
\begin{figure} 

409 
\begin{ttbox}\makeatother 

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

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

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

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

414 

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

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

417 

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

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

420 
] ==> R 

421 

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

423 
\subcaption{Quantifiers and descriptions} 

424 

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

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

427 
\tdx{excluded_middle} ~P  P 

428 

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

429 
\tdx{disjCI} (~Q ==> P) ==> PQ 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

430 
\tdx{exCI} (! x. ~ P x ==> P a) ==> ? x. P x 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

431 
\tdx{impCE} [ P>Q; ~ P ==> R; Q ==> R ] ==> R 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

432 
\tdx{iffCE} [ P=Q; [ P;Q ] ==> R; [ ~P; ~Q ] ==> R ] ==> R 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

433 
\tdx{notnotD} ~~P ==> P 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

434 
\tdx{swap} ~P ==> (~Q ==> P) ==> Q 
6580  435 
\subcaption{Classical logic} 
436 

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

437 
\tdx{if_P} P ==> (if P then x else y) = x 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

438 
\tdx{if_not_P} ~ P ==> (if P then x else y) = y 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

439 
\tdx{split_if} P(if Q then x else y) = ((Q > P x) & (~Q > P y)) 
6580  440 
\subcaption{Conditionals} 
441 
\end{ttbox} 

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

443 
\end{figure} 

444 

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

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

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

448 
conjunctions, implications, and universal quantifiers. 

449 

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

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

452 
simplifying both sides of an equation. 

453 

454 
The following simple tactics are occasionally useful: 

455 
\begin{ttdescription} 

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

457 
repeatedly to remove all outermost universal quantifiers and implications 

458 
from subgoal $i$. 

8443  459 
\item[\ttindexbold{case_tac} {\tt"}$P${\tt"} $i$] performs case distinction on 
460 
$P$ for subgoal $i$: the latter is replaced by two identical subgoals with 

461 
the added assumptions $P$ and $\lnot P$, respectively. 

7490  462 
\item[\ttindexbold{smp_tac} $j$ $i$] applies $j$ times \texttt{spec} and then 
463 
\texttt{mp} in subgoal $i$, which is typically useful when forwardchaining 

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

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

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

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

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

6580  469 
\end{ttdescription} 
470 

471 

472 
\begin{figure} 

473 
\begin{center} 

474 
\begin{tabular}{rrr} 

475 
\it name &\it metatype & \it description \\ 

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

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

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

479 
& insertion of element \\ 

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

481 
& comprehension \\ 

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

483 
& intersection over a set\\ 

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

485 
& union over a set\\ 

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

487 
&set of sets intersection \\ 

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

489 
&set of sets union \\ 

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

491 
& powerset \\[1ex] 

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

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

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

495 
& bounded quantifiers 

496 
\end{tabular} 

497 
\end{center} 

498 
\subcaption{Constants} 

499 

500 
\begin{center} 

501 
\begin{tabular}{llrrr} 

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

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

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

504 
intersection\\ 
6580  505 
\sdx{UN} & \cdx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 & 
9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

506 
union 
6580  507 
\end{tabular} 
508 
\end{center} 

509 
\subcaption{Binders} 

510 

511 
\begin{center} 

512 
\index{*"`"` symbol} 

513 
\index{*": symbol} 

514 
\index{*"<"= symbol} 

515 
\begin{tabular}{rrrr} 

516 
\it symbol & \it metatype & \it priority & \it description \\ 

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

518 
& Left 90 & image \\ 

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

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

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

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

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

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

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

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

527 
\end{tabular} 

528 
\end{center} 

529 
\subcaption{Infixes} 

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

531 
\end{figure} 

532 

533 

534 
\begin{figure} 

535 
\begin{center} \tt\frenchspacing 

536 
\index{*"! symbol} 

537 
\begin{tabular}{rrr} 

538 
\it external & \it internal & \it description \\ 

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

539 
$a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm not in\\ 
6580  540 
{\ttlbrace}$a@1$, $\ldots${\ttrbrace} & insert $a@1$ $\ldots$ {\ttlbrace}{\ttrbrace} & \rm finite set \\ 
541 
{\ttlbrace}$x$. $P[x]${\ttrbrace} & Collect($\lambda x. P[x]$) & 

542 
\rm comprehension \\ 

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

544 
\rm intersection \\ 

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

546 
\rm union \\ 

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

547 
\sdx{ALL} $x$:$A$.\ $P[x]$ or \texttt{!} $x$:$A$.\ $P[x]$ & 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

548 
Ball $A$ $\lambda x.\ P[x]$ & 
6580  549 
\rm bounded $\forall$ \\ 
9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

550 
\sdx{EX}{\tt\ } $x$:$A$.\ $P[x]$ or \texttt{?} $x$:$A$.\ $P[x]$ & 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

551 
Bex $A$ $\lambda x.\ P[x]$ & \rm bounded $\exists$ 
6580  552 
\end{tabular} 
553 
\end{center} 

554 
\subcaption{Translations} 

555 

556 
\dquotes 

557 
\[\begin{array}{rclcl} 

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

559 
&  & "{\ttlbrace}{\ttrbrace}" \\ 

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

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

562 
&  & term " `` " term \\ 

563 
&  & term " Int " term \\ 

564 
&  & term " Un " term \\ 

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

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

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

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

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

570 
&  & term " : " term \\ 

571 
&  & term " \ttilde: " term \\ 

572 
&  & term " <= " term \\ 

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

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

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

576 
&  & "?~" id ":" term " . " formula \\ 
6580  577 
\end{array} 
578 
\] 

579 
\subcaption{Full Grammar} 

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

581 
\end{figure} 

582 

583 

584 
\section{A formulation of set theory} 

585 
Historically, higherorder logic gives a foundation for Russell and 

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

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

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

589 
\begin{itemize} 

590 
\item 

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

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

593 
\item 

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

595 
may be defined by absolute comprehension. 

596 
\item 

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

598 
have a more complex type. 

599 
\end{itemize} 

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

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

602 
denoting the universal set for the given type. 

603 

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

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

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

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

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

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

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

611 

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

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

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

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

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

7490  617 
$\lnot(a\in b)$. 
6580  618 

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

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

621 
\begin{eqnarray*} 

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

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

624 
\end{eqnarray*} 

625 

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

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

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

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

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

631 

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

633 
\begin{eqnarray*} 

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

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

636 
\end{eqnarray*} 

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

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

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

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

641 
% 

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

642 
\hbox{\tt ALL~$x$:$A$.\ $P[x]$} and \hbox{\tt EX~$x$:$A$.\ $P[x]$}. The 
9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

643 
original notation of Gordon's {\sc hol} system is supported as well: 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

644 
\texttt{!}\ and \texttt{?}. 
6580  645 

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

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

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

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

650 

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

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

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

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

655 

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

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

658 
respectively. 

659 

660 

661 

662 
\begin{figure} \underscoreon 

663 
\begin{ttbox} 

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

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

666 

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

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

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

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

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

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

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

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

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

675 
\tdx{Compl_def} A == {\ttlbrace}x. ~ x:A{\ttrbrace} 
6580  676 
\tdx{INTER_def} INTER A B == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace} 
677 
\tdx{UNION_def} UNION A B == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace} 

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

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

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

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

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

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

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

685 
\end{ttbox} 

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

687 
\end{figure} 

688 

689 

690 
\begin{figure} \underscoreon 

691 
\begin{ttbox} 

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

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

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

695 

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

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

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

699 

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

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

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

703 
\subcaption{Comprehension and Bounded quantifiers} 

704 

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

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

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

708 

709 
\tdx{subset_refl} A <= A 

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

711 

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

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

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

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

716 

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

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

719 
] ==> P 

720 
\subcaption{The subset and equality relations} 

721 
\end{ttbox} 

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

723 
\end{figure} 

724 

725 

726 
\begin{figure} \underscoreon 

727 
\begin{ttbox} 

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

729 

730 
\tdx{insertI1} a : insert a B 

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

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

733 

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

734 
\tdx{ComplI} [ c:A ==> False ] ==> c : A 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

735 
\tdx{ComplD} [ c : A ] ==> ~ c:A 
6580  736 

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

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

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

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

741 

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

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

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

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

746 

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

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

749 

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

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

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

753 

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

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

756 

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

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

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

760 

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

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

763 

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

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

766 

767 
\tdx{rangeI} f x : range f 

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

769 
\end{ttbox} 

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

771 
\end{figure} 

772 

773 

774 
\subsection{Axioms and rules of set theory} 

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

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

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

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

779 

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

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

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

783 
and \texttt{range}. 

784 

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

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

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

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

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

790 

791 
%\begin{figure} \underscoreon 

792 
%\begin{ttbox} 

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

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

795 
% 

796 
%\tdx{Inv_injective} 

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

798 
% 

799 
% 

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

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

802 
% 

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

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

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

806 
% 

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

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

809 
% 

810 
%\tdx{inj_on_inverseI} 

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

812 
%\tdx{inj_on_contraD} 

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

814 
%\end{ttbox} 

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

816 
%\end{figure} 

817 

818 

819 
\begin{figure} \underscoreon 

820 
\begin{ttbox} 

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

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

823 

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

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

826 

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

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

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

830 

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

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

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

834 
\end{ttbox} 

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

836 
\end{figure} 

837 

838 

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

840 
\begin{ttbox} 

841 
\tdx{Int_absorb} A Int A = A 

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

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

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

845 

846 
\tdx{Un_absorb} A Un A = A 

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

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

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

850 

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

851 
\tdx{Compl_disjoint} A Int (A) = {\ttlbrace}x. False{\ttrbrace} 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

852 
\tdx{Compl_partition} A Un (A) = {\ttlbrace}x. True{\ttrbrace} 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

853 
\tdx{double_complement} (A) = A 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

854 
\tdx{Compl_Un} (A Un B) = (A) Int (B) 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

855 
\tdx{Compl_Int} (A Int B) = (A) Un (B) 
6580  856 

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

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

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

859 
%\tdx{Un_Union_image} (UN x:C.(A x) Un (B x)) = Union(A``C) Un Union(B``C) 
6580  860 

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

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

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

863 
%\tdx{Int_Inter_image} (INT x:C.(A x) Int (B x)) = Inter(A``C) Int Inter(B``C) 
6580  864 
\end{ttbox} 
865 
\caption{Set equalities} \label{holequalities} 

866 
\end{figure} 

867 

868 

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

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

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

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

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

874 
strictly necessary but yield more natural proofs. Similarly, 

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

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

877 
proofs pertaining to set theory. 

878 

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

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

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

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

883 

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

885 
include commutative, associative and distributive laws involving unions, 

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

887 
HOL/equalities.ML}. 

888 

889 
\begin{warn} 

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

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

892 
\end{warn} 

893 

894 
\begin{figure} 

895 
\begin{center} 

896 
\begin{tabular}{rrr} 

897 
\it name &\it metatype & \it description \\ 

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

899 
& injective/surjective \\ 

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

901 
& injective over subset\\ 

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

903 
\end{tabular} 

904 
\end{center} 

905 

906 
\underscoreon 

907 
\begin{ttbox} 

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

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

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

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

912 
\end{ttbox} 

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

914 
\end{figure} 

915 

916 
\subsection{Properties of functions}\nopagebreak 

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

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

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

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

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

922 

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

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

925 

7283  926 

6580  927 
\section{Generic packages} 
928 
\label{sec:HOL:genericpackages} 

929 

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

931 
simplifier and the classical reasoner. 

932 

933 
\subsection{Simplification and substitution} 

934 

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

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

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

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

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

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

941 
simplification rules. 

942 

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

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

945 
and simplification. 

946 

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

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

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

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

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

952 
\end{warn} 

953 

8604  954 
\begin{warn}\index{simplification!of \texttt{if}}\label{ifsimp}% 
955 
By default only the condition of an \ttindex{if} is simplified but not the 

956 
\texttt{then} and \texttt{else} parts. Of course the latter are simplified 

957 
once the condition simplifies to \texttt{True} or \texttt{False}. To ensure 

958 
full simplification of all parts of a conditional you must remove 

959 
\ttindex{if_weak_cong} from the simpset, \verb$delcongs [if_weak_cong]$. 

960 
\end{warn} 

961 

6580  962 
If the simplifier cannot use a certain rewrite rule  either because 
963 
of nontermination or because its lefthand side is too flexible  

964 
then you might try \texttt{stac}: 

965 
\begin{ttdescription} 

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

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

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

969 
may be necessary to select the desired ones. 

970 

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

972 
additional (first) subgoal. 

973 
\end{ttdescription} 

974 

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

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

977 
\HOL's general substitution rule. 

978 

979 
\subsubsection{Case splitting} 

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

981 

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

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

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

985 
expressed by the theorem \tdx{split_if}: 

986 
$$ 

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

7490  988 
((\Var{b} \to \Var{P}(\Var{x})) \land (\lnot \Var{b} \to \Var{P}(\Var{y}))) 
6580  989 
\eqno{(*)} 
990 
$$ 

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

992 
\[ 

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

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

995 
\] 

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

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

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

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

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

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

1002 
simpset, as in 

1003 
\begin{ttbox} 

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

1005 
\end{ttbox} 

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

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

1008 
\texttt{if} have been eliminated. 

1009 

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

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

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

1013 
the inverse of \texttt{addsplits}: 

1014 
\begin{ttbox} 

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

1016 
\end{ttbox} 

1017 

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

1019 
\[ 

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

1021 
\] 

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

1023 
right form because internally the lefthand side is 

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

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

6580  1027 

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

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

1030 
\begin{ttbox} 

1031 
\ttindexbold{Addsplits}: thm list > unit 

1032 
\ttindexbold{Delsplits}: thm list > unit 

1033 
\end{ttbox} 

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

1035 

1036 
\subsection{Classical reasoning} 

1037 

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

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

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

1041 

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

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

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

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

1047 
the classical rules, 

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

1050 

1051 

7283  1052 
\section{Calling the decision procedure SVC}\label{sec:HOL:SVC} 
1053 

1054 
\index{SVC decision procedure(} 

1055 

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

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

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

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

1060 
linear arithmetic. Subexpressions that SVC cannot handle are automatically 

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

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

1063 
\begin{ttbox} 

1064 
svc_tac : int > tactic 

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

1066 
\end{ttbox} 

1067 

1068 
\begin{ttdescription} 

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

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

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

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

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

1074 

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

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

1077 
syntax, SVC's response. 

1078 
\end{ttdescription} 

1079 

1080 
Here is an example, with tracing turned on: 

1081 
\begin{ttbox} 

1082 
set Svc.trace; 

1083 
{\out val it : bool = true} 

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

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

1086 

1087 
by (svc_tac 1); 

1088 
{\out Subgoal abstracted to} 

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

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

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

1092 
{\out Calling SVC:} 

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

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

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

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

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

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

1099 
{\out SVC Returns:} 

1100 
{\out VALID} 

1101 
{\out Level 1} 

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

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

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

1105 
{\out No subgoals!} 

1106 
\end{ttbox} 

1107 

1108 

1109 
\begin{warn} 

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

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

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

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

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

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

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

1117 
\end{warn} 

1118 

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

1120 
\begin{ttbox} 

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

1122 
\end{ttbox} 

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

1124 
variables: 

1125 
\begin{ttdescription} 

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

1127 
distribution directory. 

1128 

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

1130 
operating system. 

1131 
\end{ttdescription} 

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

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

1134 
\texttt{SVC_HOME} is defined. 

1135 

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

1137 
Heilmann. 

1138 

1139 

1140 
\index{SVC decision procedure)} 

1141 

1142 

1143 

1144 

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

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

1148 
introducing new types in general. The most important type 

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

7490  1150 
{\S}\ref{sec:HOL:datatype}. 
6580  1151 

1152 

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

1154 
\label{subsec:prodsum} 

1155 

1156 
\begin{figure}[htbp] 

1157 
\begin{constants} 

1158 
\it symbol & \it metatype & & \it description \\ 

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

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

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

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

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

1164 
& & generalized projection\\ 

1165 
\cdx{Sigma} & 

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

1167 
& general sum of sets 

1168 
\end{constants} 

1169 
\begin{ttbox}\makeatletter 

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

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

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

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

1174 

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

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

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

1178 

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

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

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

1182 

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

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

1185 

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

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1187 

4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1188 
\tdx{SigmaE} [ c:Sigma A B; !!x y.[ x:A; y:B x; c=(x,y) ] ==> P 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1189 
] ==> P 
6580  1190 
\end{ttbox} 
1191 
\caption{Type $\alpha\times\beta$}\label{holprod} 

1192 
\end{figure} 

1193 

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

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

1196 
tuples are simulated by pairs nested to the right: 

1197 
\begin{center} 

1198 
\begin{tabular}{cc} 

1199 
external & internal \\ 

1200 
\hline 

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

1202 
\hline 

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

1204 
\end{tabular} 

1205 
\end{center} 

1206 
In addition, it is possible to use tuples 

1207 
as patterns in abstractions: 

1208 
\begin{center} 

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

1210 
\end{center} 

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

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1212 
\begin{eqnarray*} 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1213 
\hbox{\tt\%($x$,$y$,$z$).\ $t$} 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1214 
& \leadsto & \hbox{\tt\%($x$,($y$,$z$)).\ $t$} \\ 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1215 
& \leadsto & \hbox{\tt split(\%$x$.\%($y$,$z$).\ $t$)}\\ 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1216 
& \leadsto & \hbox{\tt split(\%$x$.\ split(\%$y$ $z$.\ $t$))} 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1217 
\end{eqnarray*} 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1218 
The reverse translation is performed upon printing. 
6580  1219 
\begin{warn} 
1220 
The translation between patterns and \texttt{split} is performed automatically 

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

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

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

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

1225 
\end{warn} 

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

1227 
variable binding construct which is internally described by a 

1228 
$\lambda$abstraction. Some important examples are 

1229 
\begin{description} 

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

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

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

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

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

1235 
\end{description} 

1236 

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

1238 
\begin{ttdescription} 

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

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

1241 
each component. A simple example: 

1242 
\begin{ttbox} 

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

1244 
by(split_all_tac 1); 

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

1246 
\end{ttbox} 

1247 
\end{ttdescription} 

1248 

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

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

1251 
\begin{ttbox} 

1252 
\tdx{unit_eq} u = () 

1253 
\end{ttbox} 

1254 
\bigskip 

1255 

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

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

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

1259 

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

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

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

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

6580  1267 

1268 
\begin{figure} 

1269 
\begin{constants} 

1270 
\it symbol & \it metatype & & \it description \\ 

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

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

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

1274 
& & conditional 

1275 
\end{constants} 

1276 
\begin{ttbox}\makeatletter 

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

1278 

1279 
\tdx{inj_Inl} inj Inl 

1280 
\tdx{inj_Inr} inj Inr 

1281 

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

1283 

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

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

1286 

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

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

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

1292 
\end{figure} 

1293 

1294 
\begin{figure} 

1295 
\index{*"< symbol} 

1296 
\index{*"* symbol} 

1297 
\index{*div symbol} 

1298 
\index{*mod symbol} 

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1299 
\index{*dvd symbol} 
6580  1300 
\index{*"+ symbol} 
1301 
\index{*" symbol} 

1302 
\begin{constants} 

1303 
\it symbol & \it metatype & \it priority & \it description \\ 

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1304 
\cdx{0} & $\alpha$ & & zero \\ 
6580  1305 
\cdx{Suc} & $nat \To nat$ & & successor function\\ 
9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1306 
\tt * & $[\alpha,\alpha]\To \alpha$ & Left 70 & multiplication \\ 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1307 
\tt div & $[\alpha,\alpha]\To \alpha$ & Left 70 & division\\ 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1308 
\tt mod & $[\alpha,\alpha]\To \alpha$ & Left 70 & modulus\\ 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1309 
\tt dvd & $[\alpha,\alpha]\To bool$ & Left 70 & ``divides'' relation\\ 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1310 
\tt + & $[\alpha,\alpha]\To \alpha$ & Left 65 & addition\\ 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1311 
\tt  & $[\alpha,\alpha]\To \alpha$ & Left 65 & subtraction 
6580  1312 
\end{constants} 
1313 
\subcaption{Constants and infixes} 

1314 

1315 
\begin{ttbox}\makeatother 

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

1317 

1318 
\tdx{Suc_not_Zero} Suc m ~= 0 

1319 
\tdx{inj_Suc} inj Suc 

1320 
\tdx{n_not_Suc_n} n~=Suc n 

1321 
\subcaption{Basic properties} 

1322 
\end{ttbox} 

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

1324 
\end{figure} 

1325 

1326 

1327 
\begin{figure} 

1328 
\begin{ttbox}\makeatother 

1329 
0+n = n 

1330 
(Suc m)+n = Suc(m+n) 

1331 

1332 
m0 = m 

1333 
0n = n 

1334 
Suc(m)Suc(n) = mn 

1335 

1336 
0*n = 0 

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

1338 

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

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

1341 

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

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

1344 
\end{ttbox} 

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

1346 
\end{figure} 

1347 

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

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

1350 

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

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

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

1354 
natural numbers are inductively generated by choosing an arbitrary individual 

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

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

1357 

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1358 
Type~\tydx{nat} is an instance of class~\cldx{ord}, which makes the overloaded 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1359 
functions of this class (especially \cdx{<} and \cdx{<=}, but also \cdx{min}, 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1360 
\cdx{max} and \cdx{LEAST}) available on \tydx{nat}. Theory \thydx{Nat} builds 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1361 
on \texttt{NatDef} and shows that {\tt<=} is a linear order, so \tydx{nat} is 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1362 
also an instance of class \cldx{linorder}. 
6580  1363 

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

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

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

1367 
proved include commutative, associative, distributive, identity and 

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

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

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

1371 

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

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

1376 
\begin{ttbox} 

1377 
\sdx{primrec} 

1378 
"0 + n = n" 

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

1380 
\end{ttbox} 

1381 
There is also a \sdx{case}construct 

1382 
of the form 

1383 
\begin{ttbox} 

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

1385 
\end{ttbox} 

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

1387 
the order of the two cases. 

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

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

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

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

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

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

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

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

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

1399 

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

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

1402 
theorem \tdx{less_induct}: 

1403 
\begin{ttbox} 

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

1405 
\end{ttbox} 

1406 

1407 

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1408 
\subsection{Numerical types and numerical reasoning} 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1409 

4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1410 
The integers (type \tdx{int}) are also available in \HOL, and the reals (type 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1411 
\tdx{real}) are available in the logic image \texttt{HOLReal}. They support 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1412 
the expected operations of addition (\texttt{+}), subtraction (\texttt{}) and 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1413 
multiplication (\texttt{*}), and much else. Type \tdx{int} provides the 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1414 
\texttt{div} and \texttt{mod} operators, while type \tdx{real} provides real 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1415 
division and other operations. Both types belong to class \cldx{linorder}, so 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1416 
they inherit the relational operators and all the usual properties of linear 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1417 
orderings. For full details, please survey the theories in subdirectories 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1418 
\texttt{Integ} and \texttt{Real}. 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1419 

4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1420 
All three numeric types admit numerals of the form \texttt{\#$sd\ldots d$}, 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1421 
where $s$ is an optional minus sign and $d\ldots d$ is a string of digits. 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1422 
Numerals are represented internally by a datatype for binary notation, which 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1423 
allows numerical calculations to be performed by rewriting. For example, the 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1424 
integer division of \texttt{\#54342339} by \texttt{\#3452} takes about five 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1425 
seconds. By default, the simplifier cancels like terms on the opposite sites 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1426 
of relational operators (reducing \texttt{z+x<x+y} to \texttt{z<y}, for 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1427 
instance. The simplifier also collects like terms, replacing 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1428 
\texttt{x+y+x*\#3} by \texttt{\#4*x+y}. 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1429 

4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1430 
Sometimes numerals are not wanted, because for example \texttt{n+\#3} does not 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1431 
match a pattern of the form \texttt{Suc $k$}. You can rearrange the form of 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1432 
an arithmetic expression by proving (via \texttt{subgoal_tac}) a lemma such 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1433 
as \texttt{n+\#3 = Suc (Suc (Suc n))}. As an alternative, you can disable the 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1434 
fancier simplifications by using a basic simpset such as \texttt{HOL_ss} 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1435 
rather than the default one, \texttt{simpset()}. 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1436 

6580  1437 
Reasoning about arithmetic inequalities can be tedious. Fortunately HOL 
9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1438 
provides a decision procedure for quantifierfree linear arithmetic (that is, 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1439 
addition and subtraction). The simplifier invokes a weak version of this 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1440 
decision procedure automatically. If this is not sufficent, you can invoke the 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1441 
full procedure \ttindex{arith_tac} explicitly. It copes with arbitrary 
6580  1442 
formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt}, {\tt Suc}, {\tt 
1443 
min}, {\tt max} and numerical constants; other subterms are treated as 

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1444 
atomic; subformulae not involving numerical types are ignored; quantified 
6580  1445 
subformulae are ignored unless they are positive universal or negative 
1446 
existential. Note that the running time is exponential in the number of 

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

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

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

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

1451 

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

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

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

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

9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1456 
\texttt{div} and \texttt{mod}. Use \texttt{thms_containing} or the 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1457 
\texttt{find}functions to locate them (see the {\em Reference Manual\/}). 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1458 

4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1459 
\index{nat@{\textit{nat}} type)} 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1460 

6580  1461 

1462 
\begin{figure} 

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

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

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

1466 
\index{*"! symbol} 

1467 
\begin{constants} 

1468 
\it symbol & \it metatype & \it priority & \it description \\ 

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

ff2c3ffd38ee
used to be part of 'logics' manual;
wenzelm
