author  wenzelm 
Wed, 26 Jul 2006 00:44:44 +0200  
changeset 20207  4c57e850e8d5 
parent 17662  c6165cf72e6a 
child 22921  475ff421a6a3 
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 

9695  8 
Church's original paper~\cite{church40}. Andrews's book~\cite{andrews86} is a 
9 
full description of the original Churchstyle higherorder logic. Experience 

10 
with the {\sc hol} system has demonstrated that higherorder logic is widely 

11 
applicable in many areas of mathematics and computer science, not just 

12 
hardware verification, {\sc hol}'s original \textit{raison d'{\^e}tre\/}. It 

13 
is weaker than ZF set theory but for most applications this does not matter. 

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

15 

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

17 
syntax. Ancient releases of Isabelle included still another version of~HOL, 

18 
with explicit type inference rules~\cite{paulsonCOLOG}. This version no 

19 
longer exists, but \thydx{ZF} supports a similar style of reasoning.} 

20 
follows $\lambda$calculus and functional programming. Function application 

21 
is curried. To apply the function~$f$ of type $\tau@1\To\tau@2\To\tau@3$ to 

22 
the arguments~$a$ and~$b$ in HOL, you simply write $f\,a\,b$. There is no 

23 
`apply' operator as in \thydx{ZF}. Note that $f(a,b)$ means ``$f$ applied to 

24 
the pair $(a,b)$'' in HOL. We write ordered pairs as $(a,b)$, not $\langle 

25 
a,b\rangle$ as in ZF. 

26 

27 
HOL has a distinct feel, compared with ZF and CTT. It identifies objectlevel 

28 
types with metalevel types, taking advantage of Isabelle's builtin 

29 
typechecker. It identifies objectlevel functions with metalevel functions, 

30 
so it uses Isabelle's operations for abstraction and application. 

31 

32 
These identifications allow Isabelle to support HOL particularly nicely, but 

33 
they also mean that HOL requires more sophistication from the user  in 

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

35 
with \texttt{show_types} (or even \texttt{show_sorts}) set to \texttt{true}. 

6580  36 

37 

38 
\begin{figure} 

39 
\begin{constants} 

40 
\it name &\it metatype & \it description \\ 

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

7490  42 
\cdx{Not} & $bool\To bool$ & negation ($\lnot$) \\ 
6580  43 
\cdx{True} & $bool$ & tautology ($\top$) \\ 
44 
\cdx{False} & $bool$ & absurdity ($\bot$) \\ 

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

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

47 
\end{constants} 

48 
\subcaption{Constants} 

49 

50 
\begin{constants} 

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

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

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

54 
\it symbol &\it name &\it metatype & \it description \\ 

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

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

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

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

61 
\texttt{EX!} or {\tt?!} & \cdx{Ex1} & $(\alpha\To bool)\To bool$ & 
6580  62 
unique existence ($\exists!$)\\ 
63 
\texttt{LEAST} & \cdx{Least} & $(\alpha::ord \To bool)\To\alpha$ & 

64 
least element 

65 
\end{constants} 

66 
\subcaption{Binders} 

67 

68 
\begin{constants} 

69 
\index{*"= symbol} 

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

71 
\index{*" symbol} 

72 
\index{*"""> symbol} 

73 
\it symbol & \it metatype & \it priority & \it description \\ 

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

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

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

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

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

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

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

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

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

83 
\end{constants} 

84 
\subcaption{Infixes} 

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

86 
\end{figure} 

87 

88 

89 
\begin{figure} 

90 
\index{*let symbol} 

91 
\index{*in symbol} 

92 
\dquotes 

93 
\[\begin{array}{rclcl} 

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

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

95 
&  & "SOME~" id " . " formula 
6580  96 
&  & "\at~" id " . " formula \\ 
97 
&  & 

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

99 
&  & 

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

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

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

103 
&  & term " = " term \\ 

104 
&  & term " \ttilde= " term \\ 

105 
&  & term " < " term \\ 

106 
&  & term " <= " term \\ 

107 
&  & "\ttilde\ " formula \\ 

108 
&  & formula " \& " formula \\ 

109 
&  & formula "  " formula \\ 

110 
&  & formula " > " formula \\ 

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

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

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

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

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

116 
&  & "?!~~" id~id^* " . " formula \\ 
6580  117 
\end{array} 
118 
\] 

9695  119 
\caption{Full grammar for HOL} \label{holgrammar} 
6580  120 
\end{figure} 
121 

122 

123 
\section{Syntax} 

124 

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

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

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

7490  128 
$\lnot(a=b)$. 
6580  129 

130 
\begin{warn} 

9695  131 
HOL has no ifandonlyif connective; logical equivalence is expressed using 
132 
equality. But equality has a high priority, as befitting a relation, while 

133 
ifandonlyif typically has the lowest priority. Thus, $\lnot\lnot P=P$ 

134 
abbreviates $\lnot\lnot (P=P)$ and not $(\lnot\lnot P)=P$. When using $=$ 

135 
to mean logical equivalence, enclose both operands in parentheses. 

6580  136 
\end{warn} 
137 

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

138 
\subsection{Types and overloading} 
6580  139 
The universal type class of higherorder terms is called~\cldx{term}. 
140 
By default, explicit type variables have class \cldx{term}. In 

141 
particular the equality symbol and quantifiers are polymorphic over 

142 
class \texttt{term}. 

143 

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

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

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

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

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

149 
functions. 

150 

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

152 
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

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

154 

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

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

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

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

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

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

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

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

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

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

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

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

166 
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

167 
can stand for set complement. 
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 
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

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

171 
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

172 
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

173 
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

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

175 
this class. 
6580  176 

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

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

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

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

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

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

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

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

185 

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

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

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

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

195 
\begin{warn} 

196 
If resolution fails for no obvious reason, try setting 

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

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

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

200 

201 
\index{unification!incompleteness of} 

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

203 
guarantee to find instantiations for type variables automatically. Be 

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

205 
possibly instantiating type variables. Setting 

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

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

208 
\end{warn} 

209 

210 

211 
\subsection{Binders} 

212 

9695  213 
Hilbert's {\bf description} operator~$\varepsilon x. P[x]$ stands for some~$x$ 
214 
satisfying~$P$, if such exists. Since all terms in HOL denote something, a 

215 
description is always meaningful, but we do not know its value unless $P$ 

216 
defines it uniquely. We may write descriptions as \cdx{Eps}($\lambda x. 

217 
P[x]$) or use the syntax \hbox{\tt SOME~$x$.~$P[x]$}. 

6580  218 

219 
Existential quantification is defined by 

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

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

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

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

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

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

226 

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

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

228 

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

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

230 
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

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

232 
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

233 
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

234 
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

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

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

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

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

239 

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

240 
\medskip 
6580  241 

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

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

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

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

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

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

251 
\medskip All these binders have priority 10. 

252 

253 
\begin{warn} 

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

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

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

257 
\end{warn} 

258 

259 

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

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

264 
definition, \tdx{Let_def}. 

265 

9695  266 
HOL also defines the basic syntax 
6580  267 
\[\dquotes"case"~e~"of"~c@1~"=>"~e@1~"" \dots ""~c@n~"=>"~e@n\] 
268 
as a uniform means of expressing \texttt{case} constructs. Therefore \texttt{case} 

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

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

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

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

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

275 
\begin{warn} 

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

277 
quantifiers, which requires additional enclosing parentheses in the context 

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

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

280 
else\dots})$. 

281 
\end{warn} 

282 

283 
\section{Rules of inference} 

284 

285 
\begin{figure} 

286 
\begin{ttbox}\makeatother 

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

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

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

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

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

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

292 
\tdx{iff} (P>Q) > (Q>P) > (P=Q) 
9969  293 
\tdx{someI} P(x::'a) ==> P(@x. P x) 
9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

294 
\tdx{True_or_False} (P=True)  (P=False) 
6580  295 
\end{ttbox} 
296 
\caption{The \texttt{HOL} rules} \label{holrules} 

297 
\end{figure} 

298 

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

6580  301 
\begin{ttdescription} 
302 
\item[\tdx{ext}] expresses extensionality of functions. 

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

304 
equal. 

9969  305 
\item[\tdx{someI}] gives the defining property of the Hilbert 
6580  306 
$\varepsilon$operator. It is a form of the Axiom of Choice. The derived rule 
9969  307 
\tdx{some_equality} (see below) is often easier to use. 
6580  308 
\item[\tdx{True_or_False}] makes the logic classical.\footnote{In 
309 
fact, the $\varepsilon$operator already makes the logic classical, as 

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

311 
\end{ttdescription} 

312 

313 

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

315 
\begin{ttbox}\makeatother 

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

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

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

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

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

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

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

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

324 

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

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

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

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

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

330 
\end{ttbox} 

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

332 
\end{figure} 

333 

334 

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

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

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

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

342 
definitions. 

6580  343 
\begin{warn} 
344 
The definitions above should never be expanded and are shown for completeness 

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

346 
or, better still, using highlevel tactics 

7490  347 
(see~{\S}\ref{sec:HOL:genericpackages}). 
6580  348 
\end{warn} 
349 

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

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

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

353 

354 

355 
\begin{figure} 

356 
\begin{ttbox} 

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

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

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

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

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

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

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

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

365 
\subcaption{Equality} 

366 

367 
\tdx{TrueI} True 

368 
\tdx{FalseE} False ==> P 

369 

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

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

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

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

374 

375 
\tdx{disjI1} P ==> PQ 

376 
\tdx{disjI2} Q ==> PQ 

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

378 

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

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

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

382 
\subcaption{Propositional logic} 

383 

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

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

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

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

388 
\subcaption{Logical equivalence} 

389 

390 
\end{ttbox} 

9695  391 
\caption{Derived rules for HOL} \label{hollemmas1} 
6580  392 
\end{figure} 
14013  393 
% 
394 
%\tdx{eqTrueI} P ==> P=True 

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

6580  396 

397 

398 
\begin{figure} 

399 
\begin{ttbox}\makeatother 

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

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

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

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

404 

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

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

407 

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

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

410 
] ==> R 

411 

9969  412 
\tdx{some_equality} [ P a; !!x. P x ==> x=a ] ==> (@x. P x) = a 
6580  413 
\subcaption{Quantifiers and descriptions} 
414 

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

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

417 
\tdx{excluded_middle} ~P  P 

418 

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

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

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

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

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

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

424 
\tdx{swap} ~P ==> (~Q ==> P) ==> Q 
6580  425 
\subcaption{Classical logic} 
426 

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

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

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

429 
\tdx{split_if} P(if Q then x else y) = ((Q > P x) & (~Q > P y)) 
6580  430 
\subcaption{Conditionals} 
431 
\end{ttbox} 

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

433 
\end{figure} 

434 

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

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

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

438 
conjunctions, implications, and universal quantifiers. 

439 

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

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

442 
simplifying both sides of an equation. 

443 

444 
The following simple tactics are occasionally useful: 

445 
\begin{ttdescription} 

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

447 
repeatedly to remove all outermost universal quantifiers and implications 

448 
from subgoal $i$. 

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

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

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

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

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

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

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

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

6580  459 
\end{ttdescription} 
460 

461 

462 
\begin{figure} 

463 
\begin{center} 

464 
\begin{tabular}{rrr} 

465 
\it name &\it metatype & \it description \\ 

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

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

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

469 
& insertion of element \\ 

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

471 
& comprehension \\ 

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

473 
& intersection over a set\\ 

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

475 
& union over a set\\ 

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

477 
&set of sets intersection \\ 

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

479 
&set of sets union \\ 

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

481 
& powerset \\[1ex] 

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

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

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

485 
& bounded quantifiers 

486 
\end{tabular} 

487 
\end{center} 

488 
\subcaption{Constants} 

489 

490 
\begin{center} 

491 
\begin{tabular}{llrrr} 

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

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

494 
intersection\\ 
6580  495 
\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

496 
union 
6580  497 
\end{tabular} 
498 
\end{center} 

499 
\subcaption{Binders} 

500 

501 
\begin{center} 

502 
\index{*"`"` symbol} 

503 
\index{*": symbol} 

504 
\index{*"<"= symbol} 

505 
\begin{tabular}{rrrr} 

506 
\it symbol & \it metatype & \it priority & \it description \\ 

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

508 
& Left 90 & image \\ 

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

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

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

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

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

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

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

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

517 
\end{tabular} 

518 
\end{center} 

519 
\subcaption{Infixes} 

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

521 
\end{figure} 

522 

523 

524 
\begin{figure} 

525 
\begin{center} \tt\frenchspacing 

526 
\index{*"! symbol} 

527 
\begin{tabular}{rrr} 

528 
\it external & \it internal & \it description \\ 

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

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

532 
\rm comprehension \\ 

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

534 
\rm intersection \\ 

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

536 
\rm union \\ 

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

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

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

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

541 
Bex $A$ $\lambda x.\ P[x]$ & \rm bounded $\exists$ 
6580  542 
\end{tabular} 
543 
\end{center} 

544 
\subcaption{Translations} 

545 

546 
\dquotes 

547 
\[\begin{array}{rclcl} 

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

549 
&  & "{\ttlbrace}{\ttrbrace}" \\ 

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

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

552 
&  & term " `` " term \\ 

553 
&  & term " Int " term \\ 

554 
&  & term " Un " term \\ 

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

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

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

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

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

560 
&  & term " : " term \\ 

561 
&  & term " \ttilde: " term \\ 

562 
&  & term " <= " term \\ 

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

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

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

566 
&  & "?~" id ":" term " . " formula \\ 
6580  567 
\end{array} 
568 
\] 

569 
\subcaption{Full Grammar} 

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

571 
\end{figure} 

572 

573 

574 
\section{A formulation of set theory} 

575 
Historically, higherorder logic gives a foundation for Russell and 

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

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

6580  579 
\begin{itemize} 
580 
\item 

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

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

583 
\item 

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

585 
may be defined by absolute comprehension. 

586 
\item 

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

588 
have a more complex type. 

589 
\end{itemize} 

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

592 
universal set for the given type. 

6580  593 

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

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

597 
avoid complications involving function types in unification. The isomorphisms 

598 
between the two types are declared explicitly. They are very natural: 

599 
\texttt{Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt op :} 

600 
maps in the other direction (ignoring argument order). 

6580  601 

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

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

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

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

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

7490  607 
$\lnot(a\in b)$. 
6580  608 

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

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

611 
\begin{eqnarray*} 

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

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

614 
\end{eqnarray*} 

615 

9695  616 
The set \hbox{\tt{\ttlbrace}$x$.\ $P[x]${\ttrbrace}} consists of all $x$ (of 
617 
suitable type) that satisfy~$P[x]$, where $P[x]$ is a formula that may contain 

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

619 
P[x])$. It defines sets by absolute comprehension, which is impossible in~ZF; 

620 
the type of~$x$ implicitly restricts the comprehension. 

6580  621 

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

623 
\begin{eqnarray*} 

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

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

626 
\end{eqnarray*} 

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

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

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

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

631 
% 

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

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

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

634 
\texttt{!}\ and \texttt{?}. 
6580  635 

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

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

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

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

640 

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

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

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

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

645 

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

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

648 
respectively. 

649 

650 

651 

652 
\begin{figure} \underscoreon 

653 
\begin{ttbox} 

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

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

656 

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

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

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

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

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

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

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

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

665 
\tdx{Compl_def} A == {\ttlbrace}x. ~ x:A{\ttrbrace} 
6580  666 
\tdx{INTER_def} INTER A B == {\ttlbrace}y. ! x:A. y: B x{\ttrbrace} 
667 
\tdx{UNION_def} UNION A B == {\ttlbrace}y. ? x:A. y: B x{\ttrbrace} 

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

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

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

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

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

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

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

675 
\end{ttbox} 

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

677 
\end{figure} 

678 

679 

680 
\begin{figure} \underscoreon 

681 
\begin{ttbox} 

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

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

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

685 

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

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

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

689 

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

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

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

693 
\subcaption{Comprehension and Bounded quantifiers} 

694 

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

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

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

698 

699 
\tdx{subset_refl} A <= A 

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

701 

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

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

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

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

706 

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

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

709 
] ==> P 

710 
\subcaption{The subset and equality relations} 

711 
\end{ttbox} 

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

713 
\end{figure} 

714 

715 

716 
\begin{figure} \underscoreon 

717 
\begin{ttbox} 

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

719 

720 
\tdx{insertI1} a : insert a B 

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

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

723 

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

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

725 
\tdx{ComplD} [ c : A ] ==> ~ c:A 
6580  726 

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

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

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

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

731 

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

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

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

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

736 

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

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

739 

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

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

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

743 

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

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

746 

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

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

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

750 

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

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

753 

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

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

756 

757 
\tdx{rangeI} f x : range f 

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

759 
\end{ttbox} 

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

761 
\end{figure} 

762 

763 

764 
\subsection{Axioms and rules of set theory} 

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

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

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

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

769 

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

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

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

773 
and \texttt{range}. 

774 

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

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

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

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

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

780 

781 
%\begin{figure} \underscoreon 

782 
%\begin{ttbox} 

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

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

785 
% 

786 
%\tdx{Inv_injective} 

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

788 
% 

789 
% 

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

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

792 
% 

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

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

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

796 
% 

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

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

799 
% 

800 
%\tdx{inj_on_inverseI} 

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

802 
%\tdx{inj_on_contraD} 

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

804 
%\end{ttbox} 

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

806 
%\end{figure} 

807 

808 

809 
\begin{figure} \underscoreon 

810 
\begin{ttbox} 

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

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

813 

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

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

816 

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

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

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

820 

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

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

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

824 
\end{ttbox} 

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

826 
\end{figure} 

827 

828 

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

830 
\begin{ttbox} 

831 
\tdx{Int_absorb} A Int A = A 

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

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

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

835 

836 
\tdx{Un_absorb} A Un A = A 

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

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

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

840 

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

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

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

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

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

845 
\tdx{Compl_Int} (A Int B) = (A) Un (B) 
6580  846 

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

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

849 

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

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

14013  852 

6580  853 
\end{ttbox} 
854 
\caption{Set equalities} \label{holequalities} 

855 
\end{figure} 

14013  856 
%\tdx{Un_Union_image} (UN x:C.(A x) Un (B x)) = Union(A``C) Un Union(B``C) 
857 
%\tdx{Int_Inter_image} (INT x:C.(A x) Int (B x)) = Inter(A``C) Int Inter(B``C) 

6580  858 

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

9695  860 
obvious and resemble rules of Isabelle's ZF set theory. Certain rules, such 
861 
as \tdx{subsetCE}, \tdx{bexCI} and \tdx{UnCI}, are designed for classical 

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

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

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

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

866 
pertaining to set theory. 

6580  867 

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

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

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

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

872 

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

874 
include commutative, associative and distributive laws involving unions, 

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

876 
HOL/equalities.ML}. 

877 

878 
\begin{warn} 

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

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

881 
\end{warn} 

882 

883 
\begin{figure} 

884 
\begin{center} 

885 
\begin{tabular}{rrr} 

886 
\it name &\it metatype & \it description \\ 

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

888 
& injective/surjective \\ 

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

890 
& injective over subset\\ 

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

892 
\end{tabular} 

893 
\end{center} 

894 

895 
\underscoreon 

896 
\begin{ttbox} 

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

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

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

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

901 
\end{ttbox} 

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

903 
\end{figure} 

904 

905 
\subsection{Properties of functions}\nopagebreak 

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

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

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

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

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

911 

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

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

914 

7283  915 

6580  916 
\section{Generic packages} 
917 
\label{sec:HOL:genericpackages} 

918 

9695  919 
HOL instantiates most of Isabelle's generic packages, making available the 
6580  920 
simplifier and the classical reasoner. 
921 

922 
\subsection{Simplification and substitution} 

923 

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

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

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

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

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

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

930 
simplification rules. 

931 

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

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

934 
and simplification. 

935 

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

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

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

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

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

941 
\end{warn} 

942 

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

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

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

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

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

949 
\end{warn} 

950 

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

953 
then you might try \texttt{stac}: 

954 
\begin{ttdescription} 

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

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

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

958 
may be necessary to select the desired ones. 

959 

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

961 
additional (first) subgoal. 

962 
\end{ttdescription} 

963 

9695  964 
HOL provides the tactic \ttindex{hyp_subst_tac}, which substitutes for an 
965 
equality throughout a subgoal and its hypotheses. This tactic uses HOL's 

966 
general substitution rule. 

6580  967 

968 
\subsubsection{Case splitting} 

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

970 

9695  971 
HOL also provides convenient means for case splitting during rewriting. Goals 
972 
containing a subterm of the form \texttt{if}~$b$~{\tt then\dots else\dots} 

973 
often require a case distinction on $b$. This is expressed by the theorem 

974 
\tdx{split_if}: 

6580  975 
$$ 
976 
\Var{P}(\mbox{\tt if}~\Var{b}~{\tt then}~\Var{x}~\mbox{\tt else}~\Var{y})~=~ 

7490  977 
((\Var{b} \to \Var{P}(\Var{x})) \land (\lnot \Var{b} \to \Var{P}(\Var{y}))) 
6580  978 
\eqno{(*)} 
979 
$$ 

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

981 
\[ 

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

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

984 
\] 

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

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

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

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

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

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

991 
simpset, as in 

992 
\begin{ttbox} 

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

994 
\end{ttbox} 

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

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

997 
\texttt{if} have been eliminated. 

998 

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

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

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

1002 
the inverse of \texttt{addsplits}: 

1003 
\begin{ttbox} 

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

1005 
\end{ttbox} 

1006 

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

1008 
\[ 

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

1010 
\] 

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

1012 
right form because internally the lefthand side is 

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

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

6580  1016 

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

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

1019 
\begin{ttbox} 

1020 
\ttindexbold{Addsplits}: thm list > unit 

1021 
\ttindexbold{Delsplits}: thm list > unit 

1022 
\end{ttbox} 

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

1024 

1025 
\subsection{Classical reasoning} 

1026 

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

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

6580  1030 

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

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

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

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

1036 
the classical rules, 

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

1039 

1040 

13012  1041 
%FIXME outdated, both from the Isabelle and SVC perspective 
1042 
% \section{Calling the decision procedure SVC}\label{sec:HOL:SVC} 

1043 

1044 
% \index{SVC decision procedure(} 

1045 

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

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

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

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

1050 
% linear arithmetic. Subexpressions that SVC cannot handle are automatically 

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

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

1053 
% \begin{ttbox} 

1054 
% svc_tac : int > tactic 

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

1056 
% \end{ttbox} 

1057 

1058 
% \begin{ttdescription} 

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

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

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

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

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

1064 

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

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

1067 
% syntax, SVC's response. 

1068 
% \end{ttdescription} 

1069 

1070 
% Here is an example, with tracing turned on: 

1071 
% \begin{ttbox} 

1072 
% set Svc.trace; 

1073 
% {\out val it : bool = true} 

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

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

1076 

1077 
% by (svc_tac 1); 

1078 
% {\out Subgoal abstracted to} 

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 Calling SVC:} 

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

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

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

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

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

1088 
% {\out {* 2 (F_a) } {* 6 (F_c) } } } ) ) ) ) ) } 

1089 
% {\out SVC Returns:} 

1090 
% {\out VALID} 

1091 
% {\out Level 1} 

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

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

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

1095 
% {\out No subgoals!} 

1096 
% \end{ttbox} 

1097 

1098 

1099 
% \begin{warn} 

1100 
% Calling \ttindex{svc_tac} entails an aboveaverage risk of 

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

1102 
% the tactic translates the submitted formula using code that lies outside 

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

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

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

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

1107 
% \end{warn} 

1108 

1109 
% To start, first download SVC from the Internet at URL 

1110 
% \begin{ttbox} 

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

1112 
% \end{ttbox} 

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

1114 
% variables: 

1115 
% \begin{ttdescription} 

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

1117 
% distribution directory. 

7283  1118 

13012  1119 
% \item[\ttindexbold{SVC_MACHINE}] identifies the type of computer and 
1120 
% operating system. 

1121 
% \end{ttdescription} 

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

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

1124 
% \texttt{SVC_HOME} is defined. 

1125 

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

1127 
% Heilmann. 

1128 

1129 

1130 
% \index{SVC decision procedure)} 

7283  1131 

1132 

1133 

1134 

6580  1135 
\section{Types}\label{sec:HOL:Types} 
9695  1136 
This section describes HOL's basic predefined types ($\alpha \times \beta$, 
1137 
$\alpha + \beta$, $nat$ and $\alpha \; list$) and ways for introducing new 

1138 
types in general. The most important type construction, the 

1139 
\texttt{datatype}, is treated separately in {\S}\ref{sec:HOL:datatype}. 

6580  1140 

1141 

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

1143 
\label{subsec:prodsum} 

1144 

1145 
\begin{figure}[htbp] 

1146 
\begin{constants} 

1147 
\it symbol & \it metatype & & \it description \\ 

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

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

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

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

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

1153 
& & generalized projection\\ 

1154 
\cdx{Sigma} & 

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

1156 
& general sum of sets 

1157 
\end{constants} 

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

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

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

14013  1161 
\begin{ttbox}\makeatletter 
6580  1162 
\tdx{Sigma_def} Sigma A B == UN x:A. UN y:B x. {\ttlbrace}(x,y){\ttrbrace} 
1163 

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

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

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

1167 

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

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

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

1171 

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

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

1174 

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

1176 

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

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

1178 
] ==> P 
6580  1179 
\end{ttbox} 
1180 
\caption{Type $\alpha\times\beta$}\label{holprod} 

1181 
\end{figure} 

1182 

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

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

1185 
tuples are simulated by pairs nested to the right: 

1186 
\begin{center} 

1187 
\begin{tabular}{cc} 

1188 
external & internal \\ 

1189 
\hline 

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

1191 
\hline 

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

1193 
\end{tabular} 

1194 
\end{center} 

1195 
In addition, it is possible to use tuples 

1196 
as patterns in abstractions: 

1197 
\begin{center} 

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

1199 
\end{center} 

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

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

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

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

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

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

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

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

1207 
The reverse translation is performed upon printing. 
6580  1208 
\begin{warn} 
1209 
The translation between patterns and \texttt{split} is performed automatically 

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

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

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

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

1214 
\end{warn} 

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

1216 
variable binding construct which is internally described by a 

1217 
$\lambda$abstraction. Some important examples are 

1218 
\begin{description} 

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

10109  1220 
\item[Quantifiers:] \texttt{ALL~{\it pattern}:$A$.~$P$} 
1221 
\item[Choice:] {\underscoreon \tt SOME~{\it pattern}.~$P$} 

6580  1222 
\item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$} 
10109  1223 
\item[Sets:] \texttt{{\ttlbrace}{\it pattern}.~$P${\ttrbrace}} 
6580  1224 
\end{description} 
1225 

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

1227 
\begin{ttdescription} 

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

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

1230 
each component. A simple example: 

1231 
\begin{ttbox} 

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

1233 
by(split_all_tac 1); 

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

1235 
\end{ttbox} 

1236 
\end{ttdescription} 

1237 

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

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

1240 
\begin{ttbox} 

1241 
\tdx{unit_eq} u = () 

1242 
\end{ttbox} 

1243 
\bigskip 

1244 

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

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

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

1248 

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

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

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

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

6580  1256 

1257 
\begin{figure} 

1258 
\begin{constants} 

1259 
\it symbol & \it metatype & & \it description \\ 

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

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

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

1263 
& & conditional 

1264 
\end{constants} 

1265 
\begin{ttbox}\makeatletter 

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

1267 

1268 
\tdx{inj_Inl} inj Inl 

1269 
\tdx{inj_Inr} inj Inr 

1270 

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

1272 

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

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

1275 

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

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

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

1281 
\end{figure} 

1282 

1283 
\begin{figure} 

1284 
\index{*"< symbol} 

1285 
\index{*"* symbol} 

1286 
\index{*div symbol} 

1287 
\index{*mod symbol} 

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

1288 
\index{*dvd symbol} 
6580  1289 
\index{*"+ symbol} 
1290 
\index{*" symbol} 

1291 
\begin{constants} 

1292 
\it symbol & \it metatype & \it priority & \it description \\ 

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

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

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

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

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

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

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

1300 
\tt  & $[\alpha,\alpha]\To \alpha$ & Left 65 & subtraction 
6580  1301 
\end{constants} 
1302 
\subcaption{Constants and infixes} 

1303 

1304 
\begin{ttbox}\makeatother 

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

1306 

1307 
\tdx{Suc_not_Zero} Suc m ~= 0 

1308 
\tdx{inj_Suc} inj Suc 

1309 
\tdx{n_not_Suc_n} n~=Suc n 

1310 
\subcaption{Basic properties} 

1311 
\end{ttbox} 

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

1313 
\end{figure} 

1314 

1315 

1316 
\begin{figure} 

1317 
\begin{ttbox}\makeatother 

1318 
0+n = n 

1319 
(Suc m)+n = Suc(m+n) 

1320 

1321 
m0 = m 

1322 
0n = n 

1323 
Suc(m)Suc(n) = mn 

1324 

1325 
0*n = 0 

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

1327 

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

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

1330 

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

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

1333 
\end{ttbox} 

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

1335 
\end{figure} 

1336 

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

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

1339 

15455  1340 
The theory \thydx{Nat} defines the natural numbers in a roundabout but 
6580  1341 
traditional way. The axiom of infinity postulates a type~\tydx{ind} of 
1342 
individuals, which is nonempty and closed under an injective operation. The 

1343 
natural numbers are inductively generated by choosing an arbitrary individual 

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

15455  1345 
fixedpoint construction. 
6580  1346 

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

1347 
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

1348 
functions of this class (especially \cdx{<} and \cdx{<=}, but also \cdx{min}, 
15455  1349 
\cdx{max} and \cdx{LEAST}) available on \tydx{nat}. Theory \thydx{Nat} 
1350 
also shows that {\tt<=} is a linear order, so \tydx{nat} is 

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

1351 
also an instance of class \cldx{linorder}. 
6580  1352 

15455  1353 
Theory \thydx{NatArith} develops arithmetic on the natural numbers. It defines 
6580  1354 
addition, multiplication and subtraction. Theory \thydx{Divides} defines 
1355 
division, remainder and the ``divides'' relation. The numerous theorems 

1356 
proved include commutative, associative, distributive, identity and 

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

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

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

1360 

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

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

1365 
\begin{ttbox} 

1366 
\sdx{primrec} 

1367 
"0 + n = n" 

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

1369 
\end{ttbox} 

1370 
There is also a \sdx{case}construct 

1371 
of the form 

1372 
\begin{ttbox} 

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

1374 
\end{ttbox} 

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

1376 
the order of the two cases. 

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

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

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

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

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

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

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

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

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

1388 

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

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

1391 
theorem \tdx{less_induct}: 

1392 
\begin{ttbox} 

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

1394 
\end{ttbox} 

1395 

1396 

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

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

1398 

9695  1399 
The integers (type \tdx{int}) are also available in HOL, and the reals (type 
14024  1400 
\tdx{real}) are available in the logic image \texttt{HOLComplex}. They support 
9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

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

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

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

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

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

1406 
orderings. For full details, please survey the theories in subdirectories 
14024  1407 
\texttt{Integ}, \texttt{Real}, and \texttt{Complex}. 
9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1408 

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

1410 
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

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

1412 
allows numerical calculations to be performed by rewriting. For example, the 
13012  1413 
integer division of \texttt{54342339} by \texttt{3452} takes about five 
9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

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

1415 
of relational operators (reducing \texttt{z+x<x+y} to \texttt{z<y}, for 
13012  1416 
instance. The simplifier also collects like terms, replacing \texttt{x+y+x*3} 
1417 
by \texttt{4*x+y}. 

1418 

1419 
Sometimes numerals are not wanted, because for example \texttt{n+3} does not 

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

1420 
match a pattern of the form \texttt{Suc $k$}. You can rearrange the form of 
13012  1421 
an arithmetic expression by proving (via \texttt{subgoal_tac}) a lemma such as 
1422 
\texttt{n+3 = Suc (Suc (Suc n))}. As an alternative, you can disable the 

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

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

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

1425 

15455  1426 
Reasoning about arithmetic inequalities can be tedious. Fortunately, HOL 
1427 
provides a decision procedure for \emph{linear arithmetic}: formulae involving 

1428 
addition and subtraction. The simplifier invokes a weak version of this 

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

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

1430 
full procedure \ttindex{arith_tac} explicitly. It copes with arbitrary 
6580  1431 
formulae involving {\tt=}, {\tt<}, {\tt<=}, {\tt+}, {\tt}, {\tt Suc}, {\tt 
15455  1432 
min}, {\tt max} and numerical constants. Other subterms are treated as 
1433 
atomic, while subformulae not involving numerical types are ignored. Quantified 

6580  1434 
subformulae are ignored unless they are positive universal or negative 
15455  1435 
existential. The running time is exponential in the number of 
6580  1436 
occurrences of {\tt min}, {\tt max}, and {\tt} because they require case 
15455  1437 
distinctions. 
1438 
If {\tt k} is a numeral, then {\tt div k}, {\tt mod k} and 

1439 
{\tt k dvd} are also supported. The former two are eliminated 

1440 
by case distinctions, again blowing up the running time. 

1441 
If the formula involves explicit quantifiers, \texttt{arith_tac} may take 

1442 
superexponential time and space. 

1443 

1444 
If \texttt{arith_tac} fails, try to find relevant arithmetic results in the library. The theories \texttt{Nat} and \texttt{NatArith} contain theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{} and \texttt{*}. Theory \texttt{Divides} contains theorems about \texttt{div} and \texttt{mod}. Use Proof General's \emph{find} button (or other search facilities) to locate them. 

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

1445 

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

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

1447 

6580
