author  paulson 
Mon, 30 May 2011 16:10:12 +0100  
changeset 43077  7d69154d824b 
parent 42673  43766deefc16 
child 43270  bc72c1ccc89e 
permissions  rwrr 
6580  1 
\chapter{HigherOrder Logic} 
2 
\index{higherorder logic(} 

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

4 

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

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

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

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

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

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

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

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

14 

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

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

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

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

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

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

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

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

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

24 
a,b\rangle$ as in ZF. 

25 

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

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

28 
typechecker. It identifies objectlevel functions with metalevel functions, 

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

30 

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

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

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

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

6580  35 

36 

37 
\begin{figure} 

38 
\begin{constants} 

39 
\it name &\it metatype & \it description \\ 

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

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

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

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

46 
\end{constants} 

47 
\subcaption{Constants} 

48 

49 
\begin{constants} 

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

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

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

53 
\it symbol &\it name &\it metatype & \it description \\ 

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

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

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

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

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

63 
least element 

64 
\end{constants} 

65 
\subcaption{Binders} 

66 

67 
\begin{constants} 

68 
\index{*"= symbol} 

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

43077
7d69154d824b
Workaround for bug involving makeindex, hyperref and the  symbol
paulson
parents:
42673
diff
changeset

70 
\index{"!@{\tt\char124} symbol} %\char124 is vertical bar. We use ! because  stopped working 
6580  71 
\index{*"""> symbol} 
72 
\it symbol & \it metatype & \it priority & \it description \\ 

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

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

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

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

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

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

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

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

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

82 
\end{constants} 

83 
\subcaption{Infixes} 

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

85 
\end{figure} 

86 

87 

88 
\begin{figure} 

89 
\index{*let symbol} 

90 
\index{*in symbol} 

91 
\dquotes 

92 
\[\begin{array}{rclcl} 

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

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

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

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

98 
&  & 

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

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

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

102 
&  & term " = " term \\ 

103 
&  & term " \ttilde= " term \\ 

104 
&  & term " < " term \\ 

105 
&  & term " <= " term \\ 

106 
&  & "\ttilde\ " formula \\ 

107 
&  & formula " \& " formula \\ 

108 
&  & formula "  " formula \\ 

109 
&  & formula " > " formula \\ 

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

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

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

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

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

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

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

121 

122 
\section{Syntax} 

123 

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

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

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

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

129 
\begin{warn} 

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

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

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

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

6580  135 
\end{warn} 
136 

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

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

140 
particular the equality symbol and quantifiers are polymorphic over 

141 
class \texttt{term}. 

142 

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

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

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

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

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

148 
functions. 

149 

9695  150 
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

151 
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

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

153 

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

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

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

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

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

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

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

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

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

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

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

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

165 
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

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

167 

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

168 
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

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

170 
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

171 
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

172 
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

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

174 
this class. 
6580  175 

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

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

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

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

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

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

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

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

184 

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

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

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

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

194 
\begin{warn} 

195 
If resolution fails for no obvious reason, try setting 

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

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

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

199 

200 
\index{unification!incompleteness of} 

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

202 
guarantee to find instantiations for type variables automatically. Be 

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

204 
possibly instantiating type variables. Setting 

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

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

207 
\end{warn} 

208 

209 

210 
\subsection{Binders} 

211 

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

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

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

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

6580  217 

218 
Existential quantification is defined by 

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

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

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

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

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

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

225 

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

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

227 

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

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

229 
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

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

231 
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

232 
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

233 
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

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

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

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

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

238 

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

239 
\medskip 
6580  240 

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

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

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

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

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

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

250 
\medskip All these binders have priority 10. 

251 

252 
\begin{warn} 

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

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

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

256 
\end{warn} 

257 

258 

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

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

263 
definition, \tdx{Let_def}. 

264 

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

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

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

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

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

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

274 
\begin{warn} 

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

276 
quantifiers, which requires additional enclosing parentheses in the context 

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

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

279 
else\dots})$. 

280 
\end{warn} 

281 

282 
\section{Rules of inference} 

283 

284 
\begin{figure} 

285 
\begin{ttbox}\makeatother 

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

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

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

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

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

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

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

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

296 
\end{figure} 

297 

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

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

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

303 
equal. 

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

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

310 
\end{ttdescription} 

311 

312 

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

314 
\begin{ttbox}\makeatother 

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

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

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

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

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

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

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

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

323 

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

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

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

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

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

329 
\end{ttbox} 

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

331 
\end{figure} 

332 

333 

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

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

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

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

341 
definitions. 

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

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

345 
or, better still, using highlevel tactics 

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

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

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

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

352 

353 

354 
\begin{figure} 

355 
\begin{ttbox} 

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

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

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

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

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

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

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

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

364 
\subcaption{Equality} 

365 

366 
\tdx{TrueI} True 

367 
\tdx{FalseE} False ==> P 

368 

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

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

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

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

373 

374 
\tdx{disjI1} P ==> PQ 

375 
\tdx{disjI2} Q ==> PQ 

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

377 

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

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

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

381 
\subcaption{Propositional logic} 

382 

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

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

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

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

387 
\subcaption{Logical equivalence} 

388 

389 
\end{ttbox} 

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

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

6580  395 

396 

397 
\begin{figure} 

398 
\begin{ttbox}\makeatother 

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

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

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

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

403 

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

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

406 

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

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

409 
] ==> R 

410 

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

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

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

416 
\tdx{excluded_middle} ~P  P 

417 

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

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

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

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

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

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

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

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

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

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

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

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

432 
\end{figure} 

433 

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

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

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

437 
conjunctions, implications, and universal quantifiers. 

438 

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

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

441 
simplifying both sides of an equation. 

442 

443 
The following simple tactics are occasionally useful: 

444 
\begin{ttdescription} 

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

446 
repeatedly to remove all outermost universal quantifiers and implications 

447 
from subgoal $i$. 

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

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

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

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

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

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

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

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

6580  458 
\end{ttdescription} 
459 

460 

461 
\begin{figure} 

462 
\begin{center} 

463 
\begin{tabular}{rrr} 

464 
\it name &\it metatype & \it description \\ 

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

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

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

468 
& insertion of element \\ 

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

470 
& comprehension \\ 

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

472 
& intersection over a set\\ 

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

474 
& union over a set\\ 

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

476 
&set of sets intersection \\ 

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

478 
&set of sets union \\ 

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

480 
& powerset \\[1ex] 

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

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

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

484 
& bounded quantifiers 

485 
\end{tabular} 

486 
\end{center} 

487 
\subcaption{Constants} 

488 

489 
\begin{center} 

490 
\begin{tabular}{llrrr} 

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

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

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

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

498 
\subcaption{Binders} 

499 

500 
\begin{center} 

501 
\index{*"`"` symbol} 

502 
\index{*": symbol} 

503 
\index{*"<"= symbol} 

504 
\begin{tabular}{rrrr} 

505 
\it symbol & \it metatype & \it priority & \it description \\ 

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

507 
& Left 90 & image \\ 

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

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

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

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

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

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

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

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

516 
\end{tabular} 

517 
\end{center} 

518 
\subcaption{Infixes} 

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

520 
\end{figure} 

521 

522 

523 
\begin{figure} 

524 
\begin{center} \tt\frenchspacing 

525 
\index{*"! symbol} 

526 
\begin{tabular}{rrr} 

527 
\it external & \it internal & \it description \\ 

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

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

531 
\rm comprehension \\ 

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

533 
\rm intersection \\ 

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

535 
\rm union \\ 

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

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

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

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

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

543 
\subcaption{Translations} 

544 

545 
\dquotes 

546 
\[\begin{array}{rclcl} 

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

548 
&  & "{\ttlbrace}{\ttrbrace}" \\ 

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

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

551 
&  & term " `` " term \\ 

552 
&  & term " Int " term \\ 

553 
&  & term " Un " term \\ 

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

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

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

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

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

559 
&  & term " : " term \\ 

560 
&  & term " \ttilde: " term \\ 

561 
&  & term " <= " term \\ 

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

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

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

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

568 
\subcaption{Full Grammar} 

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

570 
\end{figure} 

571 

572 

573 
\section{A formulation of set theory} 

574 
Historically, higherorder logic gives a foundation for Russell and 

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

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

6580  578 
\begin{itemize} 
579 
\item 

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

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

582 
\item 

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

584 
may be defined by absolute comprehension. 

585 
\item 

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

587 
have a more complex type. 

588 
\end{itemize} 

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

591 
universal set for the given type. 

6580  592 

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

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

596 
avoid complications involving function types in unification. The isomorphisms 

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

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

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

6580  600 

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

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

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

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

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

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

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

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

610 
\begin{eqnarray*} 

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

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

613 
\end{eqnarray*} 

614 

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

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

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

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

6580  620 

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

622 
\begin{eqnarray*} 

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

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

625 
\end{eqnarray*} 

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

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

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

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

630 
% 

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

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

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

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

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

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

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

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

639 

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

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

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

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

644 

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

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

647 
respectively. 

648 

649 

650 

651 
\begin{figure} \underscoreon 

652 
\begin{ttbox} 

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

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

655 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

674 
\end{ttbox} 

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

676 
\end{figure} 

677 

678 

679 
\begin{figure} \underscoreon 

680 
\begin{ttbox} 

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

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

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

684 

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

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

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

688 

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

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

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

692 
\subcaption{Comprehension and Bounded quantifiers} 

693 

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

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

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

697 

698 
\tdx{subset_refl} A <= A 

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

700 

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

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

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

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

705 

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

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

708 
] ==> P 

709 
\subcaption{The subset and equality relations} 

710 
\end{ttbox} 

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

712 
\end{figure} 

713 

714 

715 
\begin{figure} \underscoreon 

716 
\begin{ttbox} 

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

718 

719 
\tdx{insertI1} a : insert a B 

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

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

722 

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

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

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

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

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

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

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

730 

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

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

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

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

735 

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

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

738 

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

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

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

742 

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

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

745 

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

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

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

749 

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

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

752 

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

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

755 

756 
\tdx{rangeI} f x : range f 

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

758 
\end{ttbox} 

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

760 
\end{figure} 

761 

762 

763 
\subsection{Axioms and rules of set theory} 

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

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

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

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

768 

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

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

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

772 
and \texttt{range}. 

773 

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

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

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

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

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

779 

780 
%\begin{figure} \underscoreon 

781 
%\begin{ttbox} 

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

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

784 
% 

785 
%\tdx{Inv_injective} 

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

787 
% 

788 
% 

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

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

791 
% 

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

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

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

795 
% 

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

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

798 
% 

799 
%\tdx{inj_on_inverseI} 

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

801 
%\tdx{inj_on_contraD} 

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

803 
%\end{ttbox} 

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

805 
%\end{figure} 

806 

807 

808 
\begin{figure} \underscoreon 

809 
\begin{ttbox} 

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

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

812 

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

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

815 

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

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

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

819 

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

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

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

823 
\end{ttbox} 

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

825 
\end{figure} 

826 

827 

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

829 
\begin{ttbox} 

830 
\tdx{Int_absorb} A Int A = A 

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

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

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

834 

835 
\tdx{Un_absorb} A Un A = A 

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

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

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

839 

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

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

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

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

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

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

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

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

848 

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

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

14013  851 

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

854 
\end{figure} 

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

6580  857 

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

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

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

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

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

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

865 
pertaining to set theory. 

6580  866 

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

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

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

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

871 

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

873 
include commutative, associative and distributive laws involving unions, 

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

875 
HOL/equalities.ML}. 

876 

877 
\begin{warn} 

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

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

880 
\end{warn} 

881 

882 
\begin{figure} 

883 
\begin{center} 

884 
\begin{tabular}{rrr} 

885 
\it name &\it metatype & \it description \\ 

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

887 
& injective/surjective \\ 

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

889 
& injective over subset\\ 

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

891 
\end{tabular} 

892 
\end{center} 

893 

894 
\underscoreon 

895 
\begin{ttbox} 

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

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

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

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

900 
\end{ttbox} 

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

902 
\end{figure} 

903 

904 
\subsection{Properties of functions}\nopagebreak 

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

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

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

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

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

910 

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

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

913 

7283  914 

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

917 

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

921 
\subsection{Simplification and substitution} 

922 

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

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

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

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

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

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

929 
simplification rules. 

930 

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

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

933 
and simplification. 

934 

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

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

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

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

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

940 
\end{warn} 

941 

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

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

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

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

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

948 
\end{warn} 

949 

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

952 
then you might try \texttt{stac}: 

953 
\begin{ttdescription} 

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

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

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

957 
may be necessary to select the desired ones. 

958 

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

960 
additional (first) subgoal. 

961 
\end{ttdescription} 

962 

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

965 
general substitution rule. 

6580  966 

967 
\subsubsection{Case splitting} 

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

969 

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

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

973 
\tdx{split_if}: 

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

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

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

980 
\[ 

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

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

983 
\] 

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

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

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

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

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

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

990 
simpset, as in 

991 
\begin{ttbox} 

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

993 
\end{ttbox} 

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

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

996 
\texttt{if} have been eliminated. 

997 

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

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

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

1001 
the inverse of \texttt{addsplits}: 

1002 
\begin{ttbox} 

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

1004 
\end{ttbox} 

1005 

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

1007 
\[ 

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

1009 
\] 

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

1011 
right form because internally the lefthand side is 

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

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

6580  1015 

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

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

1018 
\begin{ttbox} 

1019 
\ttindexbold{Addsplits}: thm list > unit 

1020 
\ttindexbold{Delsplits}: thm list > unit 

1021 
\end{ttbox} 

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

1023 

1024 
\subsection{Classical reasoning} 

1025 

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

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

6580  1029 

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

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

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

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

1035 
the classical rules, 

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

1038 

1039 

13012  1040 
%FIXME outdated, both from the Isabelle and SVC perspective 
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. 

7283  1117 

13012  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)} 

7283  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 
%\tdx{fst_def} fst p == @a. ? b. p = (a,b) 

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

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

14013  1160 
\begin{ttbox}\makeatletter 
6580  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$} 

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

6580  1221 
\item[Set operations:] \texttt{UN~{\it pattern}:$A$.~$B$} 
10109  1222 
\item[Sets:] \texttt{{\ttlbrace}{\it pattern}.~$P${\ttrbrace}} 
6580  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 

15455  1339 
The theory \thydx{Nat} defines the natural numbers in a roundabout but 
6580  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 

15455  1344 
fixedpoint construction. 
6580  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}, 
15455  1348 
\cdx{max} and \cdx{LEAST}) available on \tydx{nat}. Theory \thydx{Nat} 
1349 
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

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

15455  1352 
Theory \thydx{NatArith} develops arithmetic on the natural numbers. It defines 
6580  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 
14024  1399 
\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

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 
14024  1406 
\texttt{Integ}, \texttt{Real}, and \texttt{Complex}. 
9212
4afe62073b41
overloading, axclasses, numerals and general tidying
paulson
parents:
8628
diff
changeset

1407 

13012  1408 
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

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 
13012  1412 
integer division of \texttt{54342339} by \texttt{3452} takes about five 
9212
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 
13012  1415 
instance. The simplifier also collects like terms, replacing \texttt{x+y+x*3} 
1416 
by \texttt{4*x+y}. 

1417 

1418 
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

1419 
match a pattern of the form \texttt{Suc $k$}. You can rearrange the form of 
13012  1420 
an arithmetic expression by proving (via \texttt{subgoal_tac}) a lemma such as 
1421 
\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

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 

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

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

9212
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 
31101
26c7bb764a38
qualified names for Lin_Arith tactics and simprocs
haftmann
parents:
30686
diff
changeset

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

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

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

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

31101
26c7bb764a38
qualified names for Lin_Arith tactics and simprocs
haftmann
parents:
30686
diff
changeset

1440 
If the formula involves explicit quantifiers, \texttt{Lin_Arith.tac} may take 
15455  1441 
superexponential time and space. 
1442 

31101
26c7bb764a38
qualified names for Lin_Arith tactics and simprocs
haftmann
parents:
30686
diff
changeset

1443 
If \texttt{Lin_Arith.tac} fails, try to find relevant arithmetic results in 
22921
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
17662
diff
changeset

1444 
the library. The theories \texttt{Nat} and \texttt{NatArith} contain 
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
17662
diff
changeset

1445 
theorems about {\tt<}, {\tt<=}, \texttt{+}, \texttt{} and \texttt{*}. 
475ff421a6a3
consts in consts_code Isar commands are now referred to by usual term syntax
haftmann
parents:
17662
diff
changeset

1446 
Theory \texttt{Divides} contains theorems about \texttt{div} and 
