author  wenzelm 
Mon, 28 Aug 2000 13:52:38 +0200  
changeset 9695  ec7d7f877712 
parent 9258  2121ff73a37d 
child 9969  4753185f1dd2 
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) 
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

293 
\tdx{selectI} P(x::'a) ==> P(@x. P x) 
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. 

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

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

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

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 
% 

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

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

391 
\subcaption{Logical equivalence} 

392 

393 
\end{ttbox} 

9695  394 
\caption{Derived rules for HOL} \label{hollemmas1} 
6580  395 
\end{figure} 
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 

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

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) 

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

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

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

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

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

856 
\end{figure} 

857 

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 

7283  1041 
\section{Calling the decision procedure SVC}\label{sec:HOL:SVC} 
1042 

1043 
\index{SVC decision procedure(} 

1044 

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

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

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

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

1049 
linear arithmetic. Subexpressions that SVC cannot handle are automatically 

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

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

1052 
\begin{ttbox} 

1053 
svc_tac : int > tactic 

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

1055 
\end{ttbox} 

1056 

1057 
\begin{ttdescription} 

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

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

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

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

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

1063 

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

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

1066 
syntax, SVC's response. 

1067 
\end{ttdescription} 

1068 

1069 
Here is an example, with tracing turned on: 

1070 
\begin{ttbox} 

1071 
set Svc.trace; 

1072 
{\out val it : bool = true} 

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

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

1075 

1076 
by (svc_tac 1); 

1077 
{\out Subgoal abstracted to} 

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

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

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

1081 
{\out Calling SVC:} 

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

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

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

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

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

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

1088 
{\out SVC Returns:} 

1089 
{\out VALID} 

1090 
{\out Level 1} 

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

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

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

1094 
{\out No subgoals!} 

1095 
\end{ttbox} 

1096 

1097 

1098 
\begin{warn} 

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

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

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

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

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

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

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

1106 
\end{warn} 

1107 

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

1109 
\begin{ttbox} 

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

1111 
\end{ttbox} 

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

1113 
variables: 

1114 
\begin{ttdescription} 

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

1116 
distribution directory. 

1117 

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

1119 
operating system. 

1120 
\end{ttdescription} 

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

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

1123 
\texttt{SVC_HOME} is defined. 

1124 

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

1126 
Heilmann. 

1127 

1128 

1129 
\index{SVC decision procedure)} 

1130 

1131 

1132 

1133 

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

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

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

6580  1139 

1140 

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

1142 
\label{subsec:prodsum} 

1143 

1144 
\begin{figure}[htbp] 

1145 
\begin{constants} 

1146 
\it symbol & \it metatype & & \it description \\ 

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

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

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

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

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

1152 
& & generalized projection\\ 

1153 
\cdx{Sigma} & 

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

1155 
& general sum of sets 

1156 
\end{constants} 

1157 
\begin{ttbox}\makeatletter 

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) 

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

1162 

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

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

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

1166 

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

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

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

1170 

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

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

1173 

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

1175 

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

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

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

1180 
\end{figure} 

1181 

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

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

1184 
tuples are simulated by pairs nested to the right: 

1185 
\begin{center} 

1186 
\begin{tabular}{cc} 

1187 
external & internal \\ 

1188 
\hline 

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

1190 
\hline 

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

1192 
\end{tabular} 

1193 
\end{center} 

1194 
In addition, it is possible to use tuples 

1195 
as patterns in abstractions: 

1196 
\begin{center} 

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

1198 
\end{center} 

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

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

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

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

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

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

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

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

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

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

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

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

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

1213 
\end{warn} 

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

1215 
variable binding construct which is internally described by a 

1216 
$\lambda$abstraction. Some important examples are 

1217 
\begin{description} 

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

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

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

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

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

1223 
\end{description} 

1224 

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

1226 
\begin{ttdescription} 

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

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

1229 
each component. A simple example: 

1230 
\begin{ttbox} 

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

1232 
by(split_all_tac 1); 

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

1234 
\end{ttbox} 

1235 
\end{ttdescription} 

1236 

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

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

1239 
\begin{ttbox} 

1240 
\tdx{unit_eq} u = () 

1241 
\end{ttbox} 

1242 
\bigskip 

1243 

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

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

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

1247 

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

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

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

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

6580  1255 

1256 
\begin{figure} 

1257 
\begin{constants} 

1258 
\it symbol & \it metatype & & \it description \\ 

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

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

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

1262 
& & conditional 

1263 
\end{constants} 

1264 
\begin{ttbox}\makeatletter 

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

1266 

1267 
\tdx{inj_Inl} inj Inl 

1268 
\tdx{inj_Inr} inj Inr 

1269 

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

1271 

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

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

1274 

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

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

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

1280 
\end{figure} 

1281 

1282 
\begin{figure} 

1283 
\index{*"< symbol} 

1284 
\index{*"* symbol} 

1285 
\index{*div symbol} 

1286 
\index{*mod symbol} 

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

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

1290 
\begin{constants} 

1291 
\it symbol & \it metatype & \it priority & \it description \\ 

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

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

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

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

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

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

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

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

1302 

1303 
\begin{ttbox}\makeatother 

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

1305 

1306 
\tdx{Suc_not_Zero} Suc m ~= 0 

1307 
\tdx{inj_Suc} inj Suc 

1308 
\tdx{n_not_Suc_n} n~=Suc n 

1309 
\subcaption{Basic properties} 

1310 
\end{ttbox} 

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

1312 
\end{figure} 

1313 

1314 

1315 
\begin{figure} 

1316 
\begin{ttbox}\makeatother 

1317 
0+n = n 

1318 
(Suc m)+n = Suc(m+n) 

1319 

1320 
m0 = m 

1321 
0n = n 

1322 
Suc(m)Suc(n) = mn 

1323 

1324 
0*n = 0 

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

1326 

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

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

1329 

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

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

1332 
\end{ttbox} 

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

1334 
\end{figure} 

1335 

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

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

1338 

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

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

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

1342 
natural numbers are inductively generated by choosing an arbitrary individual 

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

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

1345 

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

1346 
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

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

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

1349 
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

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

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

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

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

1355 
proved include commutative, associative, distributive, identity and 

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

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

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

1359 

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

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

1364 
\begin{ttbox} 

1365 
\sdx{primrec} 

1366 
"0 + n = n" 

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

1368 
\end{ttbox} 

1369 
There is also a \sdx{case}construct 

1370 
of the form 

1371 
\begin{ttbox} 

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

1373 
\end{ttbox} 

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

1375 
the order of the two cases. 

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

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

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

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

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

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

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

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

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

1387 

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

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

1390 
theorem \tdx{less_induct}: 

1391 
\begin{ttbox} 

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

1393 
\end{ttbox} 

1394 

1395 

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

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

1397 

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

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

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

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

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

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

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

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

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

1407 

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

1408 
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

1409 
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

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

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

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

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

1414 
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

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

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

1417 

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

1418 
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

1419 
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

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

1421 
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

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

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

1424 

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

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

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

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

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

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

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

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

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

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

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

1439 

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

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

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

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

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

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

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

1446 

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

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

1448 

6580  1449 

1450 
\begin{figure} 

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

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

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

1454 
\index{*"! symbol} 

1455 
\begin{constants} 