104
|
1 |
%% $Id$
|
287
|
2 |
\chapter{Higher-Order logic}
|
|
3 |
The directory~\ttindexbold{HOL} contains a theory for higher-order logic.
|
|
4 |
It is based on Gordon's~{\sc hol} system~\cite{mgordon88a}, which itself is
|
|
5 |
based on Church~\cite{church40}. Andrews~\cite{andrews86} is a full
|
|
6 |
description of higher-order logic. Gordon's work has demonstrated that
|
|
7 |
higher-order logic is useful for hardware verification; beyond this, it is
|
|
8 |
widely applicable in many areas of mathematics. It is weaker than {\ZF}
|
|
9 |
set theory but for most applications this does not matter. If you prefer
|
306
|
10 |
{\ML} to Lisp, you will probably prefer \HOL\ to~{\ZF}.
|
104
|
11 |
|
|
12 |
Previous releases of Isabelle included a completely different version
|
306
|
13 |
of~\HOL, with explicit type inference rules~\cite{paulson-COLOG}. This
|
104
|
14 |
version no longer exists, but \ttindex{ZF} supports a similar style of
|
|
15 |
reasoning.
|
|
16 |
|
306
|
17 |
\HOL\ has a distinct feel, compared with {\ZF} and {\CTT}. It
|
104
|
18 |
identifies object-level types with meta-level types, taking advantage of
|
|
19 |
Isabelle's built-in type checker. It identifies object-level functions
|
|
20 |
with meta-level functions, so it uses Isabelle's operations for abstraction
|
|
21 |
and application. There is no ``apply'' operator: function applications are
|
|
22 |
written as simply~$f(a)$ rather than $f{\tt`}a$.
|
|
23 |
|
306
|
24 |
These identifications allow Isabelle to support \HOL\ particularly nicely,
|
|
25 |
but they also mean that \HOL\ requires more sophistication from the user
|
104
|
26 |
--- in particular, an understanding of Isabelle's type system. Beginners
|
|
27 |
should gain experience by working in first-order logic, before attempting
|
|
28 |
to use higher-order logic. This chapter assumes familiarity with~{\FOL{}}.
|
|
29 |
|
|
30 |
|
|
31 |
\begin{figure}
|
|
32 |
\begin{center}
|
|
33 |
\begin{tabular}{rrr}
|
111
|
34 |
\it name &\it meta-type & \it description \\
|
|
35 |
\idx{Trueprop}& $bool\To prop$ & coercion to $prop$\\
|
|
36 |
\idx{not} & $bool\To bool$ & negation ($\neg$) \\
|
|
37 |
\idx{True} & $bool$ & tautology ($\top$) \\
|
|
38 |
\idx{False} & $bool$ & absurdity ($\bot$) \\
|
|
39 |
\idx{if} & $[bool,\alpha,\alpha]\To\alpha::term$ & conditional \\
|
306
|
40 |
\idx{Inv} & $(\alpha\To\beta)\To(\beta\To\alpha)$ & function inversion\\
|
|
41 |
\idx{Let} & $[\alpha,\alpha\To\beta]\To\beta$ & let binder
|
104
|
42 |
\end{tabular}
|
|
43 |
\end{center}
|
|
44 |
\subcaption{Constants}
|
|
45 |
|
|
46 |
\begin{center}
|
306
|
47 |
\index{"@@{\tt\at}|bold}
|
|
48 |
\index{*"!|bold}
|
|
49 |
\index{*"?"!|bold}
|
104
|
50 |
\begin{tabular}{llrrr}
|
111
|
51 |
\it symbol &\it name &\it meta-type & \it prec & \it description \\
|
306
|
52 |
\tt\at & \idx{Eps} & $(\alpha\To bool)\To\alpha::term$ & 10 &
|
111
|
53 |
Hilbert description ($\epsilon$) \\
|
306
|
54 |
\tt! & \idx{All} & $(\alpha::term\To bool)\To bool$ & 10 &
|
111
|
55 |
universal quantifier ($\forall$) \\
|
104
|
56 |
\idx{?} & \idx{Ex} & $(\alpha::term\To bool)\To bool$ & 10 &
|
111
|
57 |
existential quantifier ($\exists$) \\
|
306
|
58 |
\tt?! & \idx{Ex1} & $(\alpha::term\To bool)\To bool$ & 10 &
|
111
|
59 |
unique existence ($\exists!$)
|
104
|
60 |
\end{tabular}
|
|
61 |
\end{center}
|
|
62 |
\subcaption{Binders}
|
|
63 |
|
|
64 |
\begin{center}
|
306
|
65 |
\index{*"E"X"!|bold}
|
104
|
66 |
\begin{tabular}{llrrr}
|
111
|
67 |
\it symbol &\it name &\it meta-type & \it prec & \it description \\
|
104
|
68 |
\idx{ALL} & \idx{All} & $(\alpha::term\To bool)\To bool$ & 10 &
|
111
|
69 |
universal quantifier ($\forall$) \\
|
104
|
70 |
\idx{EX} & \idx{Ex} & $(\alpha::term\To bool)\To bool$ & 10 &
|
111
|
71 |
existential quantifier ($\exists$) \\
|
306
|
72 |
\tt EX! & \idx{Ex1} & $(\alpha::term\To bool)\To bool$ & 10 &
|
111
|
73 |
unique existence ($\exists!$)
|
104
|
74 |
\end{tabular}
|
|
75 |
\end{center}
|
|
76 |
\subcaption{Alternative quantifiers}
|
|
77 |
|
|
78 |
\begin{center}
|
|
79 |
\indexbold{*"=}
|
|
80 |
\indexbold{&@{\tt\&}}
|
|
81 |
\indexbold{*"|}
|
|
82 |
\indexbold{*"-"-">}
|
|
83 |
\begin{tabular}{rrrr}
|
111
|
84 |
\it symbol & \it meta-type & \it precedence & \it description \\
|
|
85 |
\idx{o} & $[\beta\To\gamma,\alpha\To\beta]\To (\alpha\To\gamma)$ &
|
|
86 |
Right 50 & composition ($\circ$) \\
|
|
87 |
\tt = & $[\alpha::term,\alpha]\To bool$ & Left 50 & equality ($=$) \\
|
|
88 |
\tt \& & $[bool,bool]\To bool$ & Right 35 & conjunction ($\conj$) \\
|
|
89 |
\tt | & $[bool,bool]\To bool$ & Right 30 & disjunction ($\disj$) \\
|
|
90 |
\tt --> & $[bool,bool]\To bool$ & Right 25 & implication ($\imp$) \\
|
|
91 |
\tt < & $[\alpha::ord,\alpha]\To bool$ & Left 50 & less than ($<$) \\
|
|
92 |
\tt <= & $[\alpha::ord,\alpha]\To bool$ & Left 50 &
|
|
93 |
less than or equals ($\leq$)
|
104
|
94 |
\end{tabular}
|
|
95 |
\end{center}
|
|
96 |
\subcaption{Infixes}
|
|
97 |
\caption{Syntax of {\tt HOL}} \label{hol-constants}
|
|
98 |
\end{figure}
|
|
99 |
|
|
100 |
|
306
|
101 |
\begin{figure}
|
|
102 |
\indexbold{*let}
|
|
103 |
\indexbold{*in}
|
104
|
104 |
\dquotes
|
|
105 |
\[\begin{array}{rcl}
|
|
106 |
term & = & \hbox{expression of class~$term$} \\
|
306
|
107 |
& | & "\at~~" id~id^* " . " formula \\
|
|
108 |
& | & "let"~id~"="~term";"\dots";"~id~"="~term~"in"~term \\[2ex]
|
104
|
109 |
formula & = & \hbox{expression of type~$bool$} \\
|
111
|
110 |
& | & term " = " term \\
|
|
111 |
& | & term " \ttilde= " term \\
|
|
112 |
& | & term " < " term \\
|
|
113 |
& | & term " <= " term \\
|
|
114 |
& | & "\ttilde\ " formula \\
|
|
115 |
& | & formula " \& " formula \\
|
|
116 |
& | & formula " | " formula \\
|
|
117 |
& | & formula " --> " formula \\
|
|
118 |
& | & "!~~~" id~id^* " . " formula \\
|
|
119 |
& | & "?~~~" id~id^* " . " formula \\
|
|
120 |
& | & "?!~~" id~id^* " . " formula \\
|
|
121 |
& | & "ALL~" id~id^* " . " formula \\
|
|
122 |
& | & "EX~~" id~id^* " . " formula \\
|
|
123 |
& | & "EX!~" id~id^* " . " formula
|
104
|
124 |
\end{array}
|
|
125 |
\]
|
|
126 |
\subcaption{Grammar}
|
306
|
127 |
\caption{Full grammar for \HOL} \label{hol-grammar}
|
104
|
128 |
\end{figure}
|
|
129 |
|
|
130 |
|
|
131 |
\section{Syntax}
|
|
132 |
Type inference is automatic, exploiting Isabelle's type classes. The class
|
|
133 |
of higher-order terms is called {\it term\/}; type variables range over
|
|
134 |
this class by default. The equality symbol and quantifiers are polymorphic
|
|
135 |
over class {\it term}.
|
|
136 |
|
|
137 |
Class {\it ord\/} consists of all ordered types; the relations $<$ and
|
|
138 |
$\leq$ are polymorphic over this class, as are the functions
|
|
139 |
\ttindex{mono}, \ttindex{min} and \ttindex{max}. Three other
|
|
140 |
type classes --- {\it plus}, {\it minus\/} and {\it times} --- permit
|
|
141 |
overloading of the operators {\tt+}, {\tt-} and {\tt*}. In particular,
|
|
142 |
{\tt-} is overloaded for set difference and subtraction.
|
|
143 |
\index{*"+}\index{-@{\tt-}}\index{*@{\tt*}}
|
|
144 |
|
|
145 |
Figure~\ref{hol-constants} lists the constants (including infixes and
|
287
|
146 |
binders), while Fig.\ts \ref{hol-grammar} presents the grammar of
|
|
147 |
higher-order logic. Note that $a$\verb|~=|$b$ is translated to
|
|
148 |
\verb|~(|$a$=$b$\verb|)|.
|
104
|
149 |
|
287
|
150 |
\subsection{Types}\label{HOL-types}
|
104
|
151 |
The type of formulae, {\it bool} belongs to class {\it term}; thus,
|
|
152 |
formulae are terms. The built-in type~$fun$, which constructs function
|
|
153 |
types, is overloaded such that $\sigma\To\tau$ belongs to class~$term$ if
|
|
154 |
$\sigma$ and~$\tau$ do; this allows quantification over functions. Types
|
306
|
155 |
in \HOL\ must be non-empty; otherwise the quantifier rules would be
|
287
|
156 |
unsound~\cite[\S7]{paulson-COLOG}.
|
104
|
157 |
|
|
158 |
Gordon's {\sc hol} system supports {\bf type definitions}. A type is
|
|
159 |
defined by exhibiting an existing type~$\sigma$, a predicate~$P::\sigma\To
|
|
160 |
bool$, and a theorem of the form $\exists x::\sigma.P(x)$. Thus~$P$
|
|
161 |
specifies a non-empty subset of~$\sigma$, and the new type denotes this
|
|
162 |
subset. New function constants are generated to establish an isomorphism
|
|
163 |
between the new type and the subset. If type~$\sigma$ involves type
|
|
164 |
variables $\alpha@1$, \ldots, $\alpha@n$, then the type definition creates
|
|
165 |
a type constructor $(\alpha@1,\ldots,\alpha@n)ty$ rather than a particular
|
|
166 |
type.
|
|
167 |
|
|
168 |
Isabelle does not support type definitions at present. Instead, they are
|
|
169 |
mimicked by explicit definitions of isomorphism functions. These should be
|
|
170 |
accompanied by theorems of the form $\exists x::\sigma.P(x)$, but this is
|
|
171 |
not checked.
|
|
172 |
|
|
173 |
|
|
174 |
\subsection{Binders}
|
|
175 |
Hilbert's {\bf description} operator~$\epsilon x.P[x]$ stands for some~$a$
|
306
|
176 |
satisfying~$P[a]$, if such exists. Since all terms in \HOL\ denote
|
104
|
177 |
something, a description is always meaningful, but we do not know its value
|
|
178 |
unless $P[x]$ defines it uniquely. We may write descriptions as
|
|
179 |
\ttindexbold{Eps}($P$) or use the syntax
|
|
180 |
\hbox{\tt \at $x$.$P[x]$}. Existential quantification is defined
|
|
181 |
by
|
|
182 |
\[ \exists x.P(x) \equiv P(\epsilon x.P(x)) \]
|
|
183 |
The unique existence quantifier, $\exists!x.P[x]$, is defined in terms
|
|
184 |
of~$\exists$ and~$\forall$. An Isabelle binder, it admits nested
|
|
185 |
quantifications. For instance, $\exists!x y.P(x,y)$ abbreviates
|
|
186 |
$\exists!x. \exists!y.P(x,y)$; note that this does not mean that there
|
|
187 |
exists a unique pair $(x,y)$ satisfying~$P(x,y)$.
|
|
188 |
|
|
189 |
\index{*"!}\index{*"?}
|
306
|
190 |
Quantifiers have two notations. As in Gordon's {\sc hol} system, \HOL\
|
104
|
191 |
uses~{\tt!}\ and~{\tt?}\ to stand for $\forall$ and $\exists$. The
|
|
192 |
existential quantifier must be followed by a space; thus {\tt?x} is an
|
|
193 |
unknown, while \verb'? x.f(x)=y' is a quantification. Isabelle's usual
|
|
194 |
notation for quantifiers, \ttindex{ALL} and \ttindex{EX}, is also
|
|
195 |
available. Both notations are accepted for input. The {\ML} reference
|
|
196 |
\ttindexbold{HOL_quantifiers} governs the output notation. If set to {\tt
|
|
197 |
true}, then~{\tt!}\ and~{\tt?}\ are displayed; this is the default. If set
|
|
198 |
to {\tt false}, then~{\tt ALL} and~{\tt EX} are displayed.
|
|
199 |
|
|
200 |
\begin{warn}
|
|
201 |
Although the description operator does not usually allow iteration of the
|
|
202 |
form \hbox{\tt \at $x@1 \dots x@n$.$P[x@1,\dots,x@n]$}, there are cases where
|
|
203 |
this is legal. If \hbox{\tt \at $y$.$P[x,y]$} is of type~{\it bool},
|
|
204 |
then \hbox{\tt \at $x\,y$.$P[x,y]$} is legal. The pretty printer will
|
|
205 |
display \hbox{\tt \at $x$.\at $y$.$P[x,y]$} as
|
|
206 |
\hbox{\tt \at $x\,y$.$P[x,y]$}.
|
|
207 |
\end{warn}
|
|
208 |
|
306
|
209 |
\subsection{\idx{let} and \idx{case}}
|
|
210 |
Local abbreviations can be introduced via a \ttindex{let}-construct whose
|
|
211 |
syntax is shown in Fig.~\ref{hol-grammar}. Internally it is translated into
|
|
212 |
the constant \ttindex{Let} and can be expanded by rewriting with its
|
|
213 |
definition \ttindex{Let_def}.
|
|
214 |
|
|
215 |
\HOL\ also defines the basic syntax {\dquotes$"case"~e~"of"~c@1~"=>"~e@1~"|"
|
|
216 |
\dots "|"~c@n~"=>"~e@n$} for {\tt case}-constructs, which means that {\tt
|
|
217 |
case} and \ttindex{of} are reserved words. However, so far this is mere
|
|
218 |
syntax and has no logical meaning. In order to be useful it needs to be
|
|
219 |
filled with life by translating certain case constructs into meaningful
|
|
220 |
terms. For an example see the case construct for the type of lists below.
|
|
221 |
|
|
222 |
|
|
223 |
\begin{figure}
|
287
|
224 |
\begin{ttbox}\makeatother
|
104
|
225 |
\idx{refl} t = t::'a
|
|
226 |
\idx{subst} [| s=t; P(s) |] ==> P(t::'a)
|
287
|
227 |
\idx{ext} (!!x::'a. f(x)::'b = g(x)) ==> (\%x.f(x)) = (\%x.g(x))
|
104
|
228 |
\idx{impI} (P ==> Q) ==> P-->Q
|
|
229 |
\idx{mp} [| P-->Q; P |] ==> Q
|
|
230 |
\idx{iff} (P-->Q) --> (Q-->P) --> (P=Q)
|
|
231 |
\idx{selectI} P(x::'a) ==> P(@x.P(x))
|
|
232 |
\idx{True_or_False} (P=True) | (P=False)
|
|
233 |
\subcaption{basic rules}
|
|
234 |
|
287
|
235 |
\idx{True_def} True = ((\%x.x)=(\%x.x))
|
|
236 |
\idx{All_def} All = (\%P. P = (\%x.True))
|
|
237 |
\idx{Ex_def} Ex = (\%P. P(@x.P(x)))
|
104
|
238 |
\idx{False_def} False = (!P.P)
|
287
|
239 |
\idx{not_def} not = (\%P. P-->False)
|
|
240 |
\idx{and_def} op & = (\%P Q. !R. (P-->Q-->R) --> R)
|
|
241 |
\idx{or_def} op | = (\%P Q. !R. (P-->R) --> (Q-->R) --> R)
|
|
242 |
\idx{Ex1_def} Ex1 = (\%P. ? x. P(x) & (! y. P(y) --> y=x))
|
104
|
243 |
\subcaption{Definitions of the logical constants}
|
|
244 |
|
287
|
245 |
\idx{Inv_def} Inv = (\%(f::'a=>'b) y. @x. f(x)=y)
|
|
246 |
\idx{o_def} op o = (\%(f::'b=>'c) g (x::'a). f(g(x)))
|
|
247 |
\idx{if_def} if = (\%P x y.@z::'a.(P=True --> z=x) & (P=False --> z=y))
|
306
|
248 |
\idx{Let_def} Let(s,f) = f(s)
|
104
|
249 |
\subcaption{Further definitions}
|
|
250 |
\end{ttbox}
|
|
251 |
\caption{Rules of {\tt HOL}} \label{hol-rules}
|
|
252 |
\end{figure}
|
|
253 |
|
|
254 |
|
287
|
255 |
\begin{figure}
|
104
|
256 |
\begin{ttbox}
|
|
257 |
\idx{sym} s=t ==> t=s
|
|
258 |
\idx{trans} [| r=s; s=t |] ==> r=t
|
|
259 |
\idx{ssubst} [| t=s; P(s) |] ==> P(t::'a)
|
|
260 |
\idx{box_equals} [| a=b; a=c; b=d |] ==> c=d
|
|
261 |
\idx{arg_cong} s=t ==> f(s)=f(t)
|
|
262 |
\idx{fun_cong} s::'a=>'b = t ==> s(x)=t(x)
|
|
263 |
\subcaption{Equality}
|
|
264 |
|
|
265 |
\idx{TrueI} True
|
|
266 |
\idx{FalseE} False ==> P
|
|
267 |
|
|
268 |
\idx{conjI} [| P; Q |] ==> P&Q
|
|
269 |
\idx{conjunct1} [| P&Q |] ==> P
|
|
270 |
\idx{conjunct2} [| P&Q |] ==> Q
|
|
271 |
\idx{conjE} [| P&Q; [| P; Q |] ==> R |] ==> R
|
|
272 |
|
|
273 |
\idx{disjI1} P ==> P|Q
|
|
274 |
\idx{disjI2} Q ==> P|Q
|
|
275 |
\idx{disjE} [| P | Q; P ==> R; Q ==> R |] ==> R
|
|
276 |
|
|
277 |
\idx{notI} (P ==> False) ==> ~ P
|
|
278 |
\idx{notE} [| ~ P; P |] ==> R
|
|
279 |
\idx{impE} [| P-->Q; P; Q ==> R |] ==> R
|
|
280 |
\subcaption{Propositional logic}
|
|
281 |
|
|
282 |
\idx{iffI} [| P ==> Q; Q ==> P |] ==> P=Q
|
|
283 |
\idx{iffD1} [| P=Q; P |] ==> Q
|
|
284 |
\idx{iffD2} [| P=Q; Q |] ==> P
|
|
285 |
\idx{iffE} [| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R
|
|
286 |
|
|
287 |
\idx{eqTrueI} P ==> P=True
|
|
288 |
\idx{eqTrueE} P=True ==> P
|
|
289 |
\subcaption{Logical equivalence}
|
|
290 |
|
|
291 |
\end{ttbox}
|
306
|
292 |
\caption{Derived rules for \HOL} \label{hol-lemmas1}
|
104
|
293 |
\end{figure}
|
|
294 |
|
|
295 |
|
287
|
296 |
\begin{figure}
|
|
297 |
\begin{ttbox}\makeatother
|
104
|
298 |
\idx{allI} (!!x::'a. P(x)) ==> !x. P(x)
|
|
299 |
\idx{spec} !x::'a.P(x) ==> P(x)
|
|
300 |
\idx{allE} [| !x.P(x); P(x) ==> R |] ==> R
|
|
301 |
\idx{all_dupE} [| !x.P(x); [| P(x); !x.P(x) |] ==> R |] ==> R
|
|
302 |
|
|
303 |
\idx{exI} P(x) ==> ? x::'a.P(x)
|
|
304 |
\idx{exE} [| ? x::'a.P(x); !!x. P(x) ==> Q |] ==> Q
|
|
305 |
|
|
306 |
\idx{ex1I} [| P(a); !!x. P(x) ==> x=a |] ==> ?! x. P(x)
|
|
307 |
\idx{ex1E} [| ?! x.P(x); !!x. [| P(x); ! y. P(y) --> y=x |] ==> R
|
|
308 |
|] ==> R
|
|
309 |
|
|
310 |
\idx{select_equality} [| P(a); !!x. P(x) ==> x=a |] ==> (@x.P(x)) = a
|
|
311 |
\subcaption{Quantifiers and descriptions}
|
|
312 |
|
|
313 |
\idx{ccontr} (~P ==> False) ==> P
|
|
314 |
\idx{classical} (~P ==> P) ==> P
|
|
315 |
\idx{excluded_middle} ~P | P
|
|
316 |
|
|
317 |
\idx{disjCI} (~Q ==> P) ==> P|Q
|
|
318 |
\idx{exCI} (! x. ~ P(x) ==> P(a)) ==> ? x.P(x)
|
|
319 |
\idx{impCE} [| P-->Q; ~ P ==> R; Q ==> R |] ==> R
|
287
|
320 |
\idx{iffCE} [| P=Q; [| P; Q |] ==> R; [| ~P; ~Q |] ==> R |] ==> R
|
104
|
321 |
\idx{notnotD} ~~P ==> P
|
|
322 |
\idx{swap} ~P ==> (~Q ==> P) ==> Q
|
|
323 |
\subcaption{Classical logic}
|
|
324 |
|
|
325 |
\idx{if_True} if(True,x,y) = x
|
|
326 |
\idx{if_False} if(False,x,y) = y
|
|
327 |
\idx{if_P} P ==> if(P,x,y) = x
|
|
328 |
\idx{if_not_P} ~ P ==> if(P,x,y) = y
|
|
329 |
\idx{expand_if} P(if(Q,x,y)) = ((Q --> P(x)) & (~Q --> P(y)))
|
|
330 |
\subcaption{Conditionals}
|
|
331 |
\end{ttbox}
|
|
332 |
\caption{More derived rules} \label{hol-lemmas2}
|
|
333 |
\end{figure}
|
|
334 |
|
|
335 |
|
|
336 |
\section{Rules of inference}
|
|
337 |
The basic theory has the {\ML} identifier \ttindexbold{HOL.thy}. However,
|
|
338 |
many further theories are defined, introducing product and sum types, the
|
|
339 |
natural numbers, etc.
|
|
340 |
|
|
341 |
Figure~\ref{hol-rules} shows the inference rules with their~{\ML} names.
|
|
342 |
They follow standard practice in higher-order logic: only a few connectives
|
|
343 |
are taken as primitive, with the remainder defined obscurely.
|
|
344 |
|
287
|
345 |
Unusually, the definitions are expressed using object-equality~({\tt=})
|
|
346 |
rather than meta-equality~({\tt==}). This is possible because equality in
|
|
347 |
higher-order logic may equate formulae and even functions over formulae.
|
|
348 |
On the other hand, meta-equality is Isabelle's usual symbol for making
|
|
349 |
definitions. Take care to note which form of equality is used before
|
|
350 |
attempting a proof.
|
104
|
351 |
|
|
352 |
Some of the rules mention type variables; for example, {\tt refl} mentions
|
|
353 |
the type variable~{\tt'a}. This facilitates explicit instantiation of the
|
|
354 |
type variables. By default, such variables range over class {\it term}.
|
|
355 |
|
|
356 |
\begin{warn}
|
|
357 |
Where function types are involved, Isabelle's unification code does not
|
|
358 |
guarantee to find instantiations for type variables automatically. If
|
|
359 |
resolution fails for no obvious reason, try setting \ttindex{show_types} to
|
|
360 |
{\tt true}, causing Isabelle to display types of terms. (Possibly, set
|
|
361 |
\ttindex{show_sorts} to {\tt true} also, causing Isabelle to display sorts.)
|
|
362 |
Be prepared to use \ttindex{res_inst_tac} instead of {\tt resolve_tac}.
|
|
363 |
Setting \ttindex{Unify.trace_types} to {\tt true} causes Isabelle to
|
|
364 |
report omitted search paths during unification.
|
|
365 |
\end{warn}
|
|
366 |
|
|
367 |
Here are further comments on the rules:
|
|
368 |
\begin{description}
|
|
369 |
\item[\ttindexbold{ext}]
|
|
370 |
expresses extensionality of functions.
|
|
371 |
\item[\ttindexbold{iff}]
|
|
372 |
asserts that logically equivalent formulae are equal.
|
|
373 |
\item[\ttindexbold{selectI}]
|
|
374 |
gives the defining property of the Hilbert $\epsilon$-operator. The
|
|
375 |
derived rule \ttindexbold{select_equality} (see below) is often easier to use.
|
|
376 |
\item[\ttindexbold{True_or_False}]
|
|
377 |
makes the logic classical.\footnote{In fact, the $\epsilon$-operator
|
|
378 |
already makes the logic classical, as shown by Diaconescu;
|
|
379 |
see Paulson~\cite{paulson-COLOG} for details.}
|
|
380 |
\end{description}
|
|
381 |
|
|
382 |
\begin{warn}
|
306
|
383 |
\HOL\ has no if-and-only-if connective; logical equivalence is expressed
|
104
|
384 |
using equality. But equality has a high precedence, as befitting a
|
|
385 |
relation, while if-and-only-if typically has the lowest precedence. Thus,
|
|
386 |
$\neg\neg P=P$ abbreviates $\neg\neg (P=P)$ and not $(\neg\neg P)=P$. When
|
|
387 |
using $=$ to mean logical equivalence, enclose both operands in
|
|
388 |
parentheses.
|
|
389 |
\end{warn}
|
|
390 |
|
|
391 |
Some derived rules are shown in Figures~\ref{hol-lemmas1}
|
|
392 |
and~\ref{hol-lemmas2}, with their {\ML} names. These include natural rules
|
|
393 |
for the logical connectives, as well as sequent-style elimination rules for
|
|
394 |
conjunctions, implications, and universal quantifiers.
|
|
395 |
|
|
396 |
Note the equality rules: \ttindexbold{ssubst} performs substitution in
|
|
397 |
backward proofs, while \ttindexbold{box_equals} supports reasoning by
|
|
398 |
simplifying both sides of an equation.
|
|
399 |
|
287
|
400 |
See the files {\tt HOL/hol.thy} and
|
|
401 |
{\tt HOL/hol.ML} for complete listings of the rules and
|
104
|
402 |
derived rules.
|
|
403 |
|
|
404 |
|
|
405 |
\section{Generic packages}
|
306
|
406 |
\HOL\ instantiates most of Isabelle's generic packages;
|
287
|
407 |
see {\tt HOL/ROOT.ML} for details.
|
104
|
408 |
\begin{itemize}
|
|
409 |
\item
|
306
|
410 |
Because it includes a general substitution rule, \HOL\ instantiates the
|
104
|
411 |
tactic \ttindex{hyp_subst_tac}, which substitutes for an equality
|
|
412 |
throughout a subgoal and its hypotheses.
|
|
413 |
\item
|
|
414 |
It instantiates the simplifier, defining~\ttindexbold{HOL_ss} as the
|
|
415 |
simplification set for higher-order logic. Equality~($=$), which also
|
|
416 |
expresses logical equivalence, may be used for rewriting. See the file
|
287
|
417 |
{\tt HOL/simpdata.ML} for a complete listing of the simplification
|
104
|
418 |
rules.
|
|
419 |
\item
|
|
420 |
It instantiates the classical reasoning module. See~\S\ref{hol-cla-prover}
|
|
421 |
for details.
|
|
422 |
\end{itemize}
|
|
423 |
|
|
424 |
|
|
425 |
\begin{figure}
|
|
426 |
\begin{center}
|
|
427 |
\begin{tabular}{rrr}
|
111
|
428 |
\it name &\it meta-type & \it description \\
|
104
|
429 |
\index{"{"}@{\tt\{\}}}
|
111
|
430 |
{\tt\{\}} & $\alpha\,set$ & the empty set \\
|
|
431 |
\idx{insert} & $[\alpha,\alpha\,set]\To \alpha\,set$
|
|
432 |
& insertion of element \\
|
|
433 |
\idx{Collect} & $(\alpha\To bool)\To\alpha\,set$
|
|
434 |
& comprehension \\
|
|
435 |
\idx{Compl} & $(\alpha\,set)\To\alpha\,set$
|
|
436 |
& complement \\
|
104
|
437 |
\idx{INTER} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
|
111
|
438 |
& intersection over a set\\
|
104
|
439 |
\idx{UNION} & $[\alpha\,set,\alpha\To\beta\,set]\To\beta\,set$
|
111
|
440 |
& union over a set\\
|
104
|
441 |
\idx{Inter} & $((\alpha\,set)set)\To\alpha\,set$
|
111
|
442 |
&set of sets intersection \\
|
104
|
443 |
\idx{Union} & $((\alpha\,set)set)\To\alpha\,set$
|
111
|
444 |
&set of sets union \\
|
|
445 |
\idx{range} & $(\alpha\To\beta )\To\beta\,set$
|
|
446 |
& range of a function \\[1ex]
|
|
447 |
\idx{Ball}~~\idx{Bex} & $[\alpha\,set,\alpha\To bool]\To bool$
|
|
448 |
& bounded quantifiers \\
|
|
449 |
\idx{mono} & $(\alpha\,set\To\beta\,set)\To bool$
|
|
450 |
& monotonicity \\
|
104
|
451 |
\idx{inj}~~\idx{surj}& $(\alpha\To\beta )\To bool$
|
111
|
452 |
& injective/surjective \\
|
|
453 |
\idx{inj_onto} & $[\alpha\To\beta ,\alpha\,set]\To bool$
|
|
454 |
& injective over subset
|
104
|
455 |
\end{tabular}
|
|
456 |
\end{center}
|
|
457 |
\subcaption{Constants}
|
|
458 |
|
|
459 |
\begin{center}
|
|
460 |
\begin{tabular}{llrrr}
|
111
|
461 |
\it symbol &\it name &\it meta-type & \it prec & \it description \\
|
104
|
462 |
\idx{INT} & \idx{INTER1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
|
111
|
463 |
intersection over a type\\
|
104
|
464 |
\idx{UN} & \idx{UNION1} & $(\alpha\To\beta\,set)\To\beta\,set$ & 10 &
|
111
|
465 |
union over a type
|
104
|
466 |
\end{tabular}
|
|
467 |
\end{center}
|
|
468 |
\subcaption{Binders}
|
|
469 |
|
|
470 |
\begin{center}
|
|
471 |
\indexbold{*"`"`}
|
|
472 |
\indexbold{*":}
|
|
473 |
\indexbold{*"<"=}
|
|
474 |
\begin{tabular}{rrrr}
|
111
|
475 |
\it symbol & \it meta-type & \it precedence & \it description \\
|
|
476 |
\tt `` & $[\alpha\To\beta ,\alpha\,set]\To (\beta\,set)$
|
|
477 |
& Left 90 & image \\
|
|
478 |
\idx{Int} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
|
|
479 |
& Left 70 & intersection ($\inter$) \\
|
|
480 |
\idx{Un} & $[\alpha\,set,\alpha\,set]\To\alpha\,set$
|
|
481 |
& Left 65 & union ($\union$) \\
|
|
482 |
\tt: & $[\alpha ,\alpha\,set]\To bool$
|
|
483 |
& Left 50 & membership ($\in$) \\
|
|
484 |
\tt <= & $[\alpha\,set,\alpha\,set]\To bool$
|
|
485 |
& Left 50 & subset ($\subseteq$)
|
104
|
486 |
\end{tabular}
|
|
487 |
\end{center}
|
|
488 |
\subcaption{Infixes}
|
306
|
489 |
\caption{Syntax of \HOL's set theory} \label{hol-set-syntax}
|
104
|
490 |
\end{figure}
|
|
491 |
|
|
492 |
|
|
493 |
\begin{figure}
|
|
494 |
\begin{center} \tt\frenchspacing
|
306
|
495 |
\index{*"!|bold}
|
104
|
496 |
\begin{tabular}{rrr}
|
111
|
497 |
\it external & \it internal & \it description \\
|
104
|
498 |
$a$ \ttilde: $b$ & \ttilde($a$ : $b$) & \rm negated membership\\
|
154
|
499 |
\{$a@1$, $\ldots$, $a@n$\} & insert($a@1$,$\cdots$,insert($a@n$,\{\})) &
|
104
|
500 |
\rm finite set \\
|
111
|
501 |
\{$x$.$P[x]$\} & Collect($\lambda x.P[x]$) &
|
104
|
502 |
\rm comprehension \\
|
111
|
503 |
\idx{INT} $x$:$A$.$B[x]$ & INTER($A$,$\lambda x.B[x]$) &
|
|
504 |
\rm intersection over a set \\
|
|
505 |
\idx{UN} $x$:$A$.$B[x]$ & UNION($A$,$\lambda x.B[x]$) &
|
|
506 |
\rm union over a set \\
|
306
|
507 |
\tt ! $x$:$A$.$P[x]$ & Ball($A$,$\lambda x.P[x]$) &
|
111
|
508 |
\rm bounded $\forall$ \\
|
|
509 |
\idx{?} $x$:$A$.$P[x]$ & Bex($A$,$\lambda x.P[x]$) &
|
|
510 |
\rm bounded $\exists$ \\[1ex]
|
|
511 |
\idx{ALL} $x$:$A$.$P[x]$ & Ball($A$,$\lambda x.P[x]$) &
|
|
512 |
\rm bounded $\forall$ \\
|
|
513 |
\idx{EX} $x$:$A$.$P[x]$ & Bex($A$,$\lambda x.P[x]$) &
|
|
514 |
\rm bounded $\exists$
|
104
|
515 |
\end{tabular}
|
|
516 |
\end{center}
|
|
517 |
\subcaption{Translations}
|
|
518 |
|
|
519 |
\dquotes
|
|
520 |
\[\begin{array}{rcl}
|
|
521 |
term & = & \hbox{other terms\ldots} \\
|
111
|
522 |
& | & "\{\}" \\
|
|
523 |
& | & "\{ " term\; ("," term)^* " \}" \\
|
|
524 |
& | & "\{ " id " . " formula " \}" \\
|
|
525 |
& | & term " `` " term \\
|
|
526 |
& | & term " Int " term \\
|
|
527 |
& | & term " Un " term \\
|
|
528 |
& | & "INT~~" id ":" term " . " term \\
|
|
529 |
& | & "UN~~~" id ":" term " . " term \\
|
|
530 |
& | & "INT~~" id~id^* " . " term \\
|
|
531 |
& | & "UN~~~" id~id^* " . " term \\[2ex]
|
104
|
532 |
formula & = & \hbox{other formulae\ldots} \\
|
111
|
533 |
& | & term " : " term \\
|
|
534 |
& | & term " \ttilde: " term \\
|
|
535 |
& | & term " <= " term \\
|
|
536 |
& | & "!~~~" id ":" term " . " formula \\
|
|
537 |
& | & "?~~~" id ":" term " . " formula \\
|
|
538 |
& | & "ALL " id ":" term " . " formula \\
|
|
539 |
& | & "EX~~" id ":" term " . " formula
|
104
|
540 |
\end{array}
|
|
541 |
\]
|
|
542 |
\subcaption{Full Grammar}
|
306
|
543 |
\caption{Syntax of \HOL's set theory (continued)} \label{hol-set-syntax2}
|
104
|
544 |
\end{figure}
|
|
545 |
|
|
546 |
|
287
|
547 |
\begin{figure} \underscoreon
|
104
|
548 |
\begin{ttbox}
|
|
549 |
\idx{mem_Collect_eq} (a : \{x.P(x)\}) = P(a)
|
|
550 |
\idx{Collect_mem_eq} \{x.x:A\} = A
|
|
551 |
\subcaption{Isomorphisms between predicates and sets}
|
|
552 |
|
154
|
553 |
\idx{empty_def} \{\} == \{x.x=False\}
|
104
|
554 |
\idx{insert_def} insert(a,B) == \{x.x=a\} Un B
|
|
555 |
\idx{Ball_def} Ball(A,P) == ! x. x:A --> P(x)
|
|
556 |
\idx{Bex_def} Bex(A,P) == ? x. x:A & P(x)
|
|
557 |
\idx{subset_def} A <= B == ! x:A. x:B
|
|
558 |
\idx{Un_def} A Un B == \{x.x:A | x:B\}
|
|
559 |
\idx{Int_def} A Int B == \{x.x:A & x:B\}
|
|
560 |
\idx{set_diff_def} A - B == \{x.x:A & x~:B\}
|
|
561 |
\idx{Compl_def} Compl(A) == \{x. ~ x:A\}
|
|
562 |
\idx{INTER_def} INTER(A,B) == \{y. ! x:A. y: B(x)\}
|
|
563 |
\idx{UNION_def} UNION(A,B) == \{y. ? x:A. y: B(x)\}
|
|
564 |
\idx{INTER1_def} INTER1(B) == INTER(\{x.True\}, B)
|
|
565 |
\idx{UNION1_def} UNION1(B) == UNION(\{x.True\}, B)
|
|
566 |
\idx{Inter_def} Inter(S) == (INT x:S. x)
|
|
567 |
\idx{Union_def} Union(S) == (UN x:S. x)
|
|
568 |
\idx{image_def} f``A == \{y. ? x:A. y=f(x)\}
|
|
569 |
\idx{range_def} range(f) == \{y. ? x. y=f(x)\}
|
|
570 |
\idx{mono_def} mono(f) == !A B. A <= B --> f(A) <= f(B)
|
|
571 |
\idx{inj_def} inj(f) == ! x y. f(x)=f(y) --> x=y
|
|
572 |
\idx{surj_def} surj(f) == ! y. ? x. y=f(x)
|
|
573 |
\idx{inj_onto_def} inj_onto(f,A) == !x:A. !y:A. f(x)=f(y) --> x=y
|
|
574 |
\subcaption{Definitions}
|
|
575 |
\end{ttbox}
|
306
|
576 |
\caption{Rules of \HOL's set theory} \label{hol-set-rules}
|
104
|
577 |
\end{figure}
|
|
578 |
|
|
579 |
|
287
|
580 |
\begin{figure} \underscoreon
|
104
|
581 |
\begin{ttbox}
|
|
582 |
\idx{CollectI} [| P(a) |] ==> a : \{x.P(x)\}
|
|
583 |
\idx{CollectD} [| a : \{x.P(x)\} |] ==> P(a)
|
|
584 |
\idx{CollectE} [| a : \{x.P(x)\}; P(a) ==> W |] ==> W
|
|
585 |
\idx{Collect_cong} [| !!x. P(x)=Q(x) |] ==> \{x. P(x)\} = \{x. Q(x)\}
|
|
586 |
\subcaption{Comprehension}
|
|
587 |
|
|
588 |
\idx{ballI} [| !!x. x:A ==> P(x) |] ==> ! x:A. P(x)
|
|
589 |
\idx{bspec} [| ! x:A. P(x); x:A |] ==> P(x)
|
|
590 |
\idx{ballE} [| ! x:A. P(x); P(x) ==> Q; ~ x:A ==> Q |] ==> Q
|
|
591 |
\idx{ball_cong} [| A=A'; !!x. x:A' ==> P(x) = P'(x) |] ==>
|
|
592 |
(! x:A. P(x)) = (! x:A'. P'(x))
|
|
593 |
|
|
594 |
\idx{bexI} [| P(x); x:A |] ==> ? x:A. P(x)
|
|
595 |
\idx{bexCI} [| ! x:A. ~ P(x) ==> P(a); a:A |] ==> ? x:A.P(x)
|
|
596 |
\idx{bexE} [| ? x:A. P(x); !!x. [| x:A; P(x) |] ==> Q |] ==> Q
|
|
597 |
\subcaption{Bounded quantifiers}
|
|
598 |
|
|
599 |
\idx{subsetI} (!!x.x:A ==> x:B) ==> A <= B
|
|
600 |
\idx{subsetD} [| A <= B; c:A |] ==> c:B
|
|
601 |
\idx{subsetCE} [| A <= B; ~ (c:A) ==> P; c:B ==> P |] ==> P
|
|
602 |
|
|
603 |
\idx{subset_refl} A <= A
|
|
604 |
\idx{subset_antisym} [| A <= B; B <= A |] ==> A = B
|
|
605 |
\idx{subset_trans} [| A<=B; B<=C |] ==> A<=C
|
|
606 |
|
|
607 |
\idx{set_ext} [| !!x. (x:A) = (x:B) |] ==> A = B
|
|
608 |
\idx{equalityD1} A = B ==> A<=B
|
|
609 |
\idx{equalityD2} A = B ==> B<=A
|
|
610 |
\idx{equalityE} [| A = B; [| A<=B; B<=A |] ==> P |] ==> P
|
|
611 |
|
|
612 |
\idx{equalityCE} [| A = B; [| c:A; c:B |] ==> P;
|
|
613 |
[| ~ c:A; ~ c:B |] ==> P
|
|
614 |
|] ==> P
|
|
615 |
\subcaption{The subset and equality relations}
|
|
616 |
\end{ttbox}
|
|
617 |
\caption{Derived rules for set theory} \label{hol-set1}
|
|
618 |
\end{figure}
|
|
619 |
|
|
620 |
|
287
|
621 |
\begin{figure} \underscoreon
|
104
|
622 |
\begin{ttbox}
|
|
623 |
\idx{emptyE} a : \{\} ==> P
|
|
624 |
|
|
625 |
\idx{insertI1} a : insert(a,B)
|
|
626 |
\idx{insertI2} a : B ==> a : insert(b,B)
|
114
|
627 |
\idx{insertE} [| a : insert(b,A); a=b ==> P; a:A ==> P |] ==> P
|
104
|
628 |
|
|
629 |
\idx{ComplI} [| c:A ==> False |] ==> c : Compl(A)
|
|
630 |
\idx{ComplD} [| c : Compl(A) |] ==> ~ c:A
|
|
631 |
|
|
632 |
\idx{UnI1} c:A ==> c : A Un B
|
|
633 |
\idx{UnI2} c:B ==> c : A Un B
|
|
634 |
\idx{UnCI} (~c:B ==> c:A) ==> c : A Un B
|
|
635 |
\idx{UnE} [| c : A Un B; c:A ==> P; c:B ==> P |] ==> P
|
|
636 |
|
|
637 |
\idx{IntI} [| c:A; c:B |] ==> c : A Int B
|
|
638 |
\idx{IntD1} c : A Int B ==> c:A
|
|
639 |
\idx{IntD2} c : A Int B ==> c:B
|
|
640 |
\idx{IntE} [| c : A Int B; [| c:A; c:B |] ==> P |] ==> P
|
|
641 |
|
|
642 |
\idx{UN_I} [| a:A; b: B(a) |] ==> b: (UN x:A. B(x))
|
|
643 |
\idx{UN_E} [| b: (UN x:A. B(x)); !!x.[| x:A; b:B(x) |] ==> R |] ==> R
|
|
644 |
|
|
645 |
\idx{INT_I} (!!x. x:A ==> b: B(x)) ==> b : (INT x:A. B(x))
|
|
646 |
\idx{INT_D} [| b: (INT x:A. B(x)); a:A |] ==> b: B(a)
|
|
647 |
\idx{INT_E} [| b: (INT x:A. B(x)); b: B(a) ==> R; ~ a:A ==> R |] ==> R
|
|
648 |
|
|
649 |
\idx{UnionI} [| X:C; A:X |] ==> A : Union(C)
|
|
650 |
\idx{UnionE} [| A : Union(C); !!X.[| A:X; X:C |] ==> R |] ==> R
|
|
651 |
|
|
652 |
\idx{InterI} [| !!X. X:C ==> A:X |] ==> A : Inter(C)
|
|
653 |
\idx{InterD} [| A : Inter(C); X:C |] ==> A:X
|
|
654 |
\idx{InterE} [| A : Inter(C); A:X ==> R; ~ X:C ==> R |] ==> R
|
|
655 |
\end{ttbox}
|
|
656 |
\caption{Further derived rules for set theory} \label{hol-set2}
|
|
657 |
\end{figure}
|
|
658 |
|
|
659 |
|
|
660 |
\section{A formulation of set theory}
|
|
661 |
Historically, higher-order logic gives a foundation for Russell and
|
|
662 |
Whitehead's theory of classes. Let us use modern terminology and call them
|
|
663 |
{\bf sets}, but note that these sets are distinct from those of {\ZF} set
|
|
664 |
theory, and behave more like {\ZF} classes.
|
|
665 |
\begin{itemize}
|
|
666 |
\item
|
|
667 |
Sets are given by predicates over some type~$\sigma$. Types serve to
|
|
668 |
define universes for sets, but type checking is still significant.
|
|
669 |
\item
|
|
670 |
There is a universal set (for each type). Thus, sets have complements, and
|
|
671 |
may be defined by absolute comprehension.
|
|
672 |
\item
|
|
673 |
Although sets may contain other sets as elements, the containing set must
|
|
674 |
have a more complex type.
|
|
675 |
\end{itemize}
|
306
|
676 |
Finite unions and intersections have the same behaviour in \HOL\ as they
|
|
677 |
do in~{\ZF}. In \HOL\ the intersection of the empty set is well-defined,
|
104
|
678 |
denoting the universal set for the given type.
|
|
679 |
|
|
680 |
\subsection{Syntax of set theory}
|
287
|
681 |
The type $\alpha\,set$ is essentially the same as $\alpha\To bool$. The
|
|
682 |
new type is defined for clarity and to avoid complications involving
|
|
683 |
function types in unification. Since Isabelle does not support type
|
|
684 |
definitions (as mentioned in \S\ref{HOL-types}), the isomorphisms between
|
|
685 |
the two types are declared explicitly. Here they are natural: {\tt
|
|
686 |
Collect} maps $\alpha\To bool$ to $\alpha\,set$, while \hbox{\tt op :}
|
|
687 |
maps in the other direction (ignoring argument order).
|
104
|
688 |
|
|
689 |
Figure~\ref{hol-set-syntax} lists the constants, infixes, and syntax
|
|
690 |
translations. Figure~\ref{hol-set-syntax2} presents the grammar of the new
|
|
691 |
constructs. Infix operators include union and intersection ($A\union B$
|
|
692 |
and $A\inter B$), the subset and membership relations, and the image
|
|
693 |
operator~{\tt``}. Note that $a$\verb|~:|$b$ is translated to
|
|
694 |
\verb|~(|$a$:$b$\verb|)|. The {\tt\{\ldots\}} notation abbreviates finite
|
|
695 |
sets constructed in the obvious manner using~{\tt insert} and~$\{\}$ (the
|
|
696 |
empty set):
|
|
697 |
\begin{eqnarray*}
|
154
|
698 |
\{a,b,c\} & \equiv & {\tt insert}(a,{\tt insert}(b,{\tt insert}(c,\{\})))
|
104
|
699 |
\end{eqnarray*}
|
|
700 |
|
|
701 |
The set \hbox{\tt\{$x$.$P[x]$\}} consists of all $x$ (of suitable type)
|
|
702 |
that satisfy~$P[x]$, where $P[x]$ is a formula that may contain free
|
|
703 |
occurrences of~$x$. This syntax expands to \ttindexbold{Collect}$(\lambda
|
|
704 |
x.P[x])$.
|
|
705 |
|
|
706 |
The set theory defines two {\bf bounded quantifiers}:
|
|
707 |
\begin{eqnarray*}
|
|
708 |
\forall x\in A.P[x] &\hbox{which abbreviates}& \forall x. x\in A\imp P[x] \\
|
|
709 |
\exists x\in A.P[x] &\hbox{which abbreviates}& \exists x. x\in A\conj P[x]
|
|
710 |
\end{eqnarray*}
|
|
711 |
The constants~\ttindexbold{Ball} and~\ttindexbold{Bex} are defined
|
|
712 |
accordingly. Instead of {\tt Ball($A$,$P$)} and {\tt Bex($A$,$P$)} we may
|
|
713 |
write\index{*"!}\index{*"?}\index{*ALL}\index{*EX}
|
|
714 |
\hbox{\tt !~$x$:$A$.$P[x]$} and \hbox{\tt ?~$x$:$A$.$P[x]$}.
|
|
715 |
Isabelle's usual notation, \ttindex{ALL} and \ttindex{EX}, is also
|
|
716 |
available. As with
|
|
717 |
ordinary quantifiers, the contents of \ttindexbold{HOL_quantifiers} specifies
|
|
718 |
which notation should be used for output.
|
|
719 |
|
|
720 |
Unions and intersections over sets, namely $\bigcup@{x\in A}B[x]$ and
|
|
721 |
$\bigcap@{x\in A}B[x]$, are written
|
|
722 |
\ttindexbold{UN}~\hbox{\tt$x$:$A$.$B[x]$} and
|
|
723 |
\ttindexbold{INT}~\hbox{\tt$x$:$A$.$B[x]$}.
|
|
724 |
Unions and intersections over types, namely $\bigcup@x B[x]$ and
|
|
725 |
$\bigcap@x B[x]$, are written
|
|
726 |
\ttindexbold{UN}~\hbox{\tt$x$.$B[x]$} and
|
|
727 |
\ttindexbold{INT}~\hbox{\tt$x$.$B[x]$}; they are equivalent to the previous
|
|
728 |
union/intersection operators when $A$ is the universal set.
|
|
729 |
The set of set union and intersection operators ($\bigcup A$ and $\bigcap
|
|
730 |
A$) are not binders, but equals $\bigcup@{x\in A}x$ and $\bigcap@{x\in
|
|
731 |
A}x$, respectively.
|
|
732 |
|
|
733 |
\subsection{Axioms and rules of set theory}
|
|
734 |
The axioms \ttindexbold{mem_Collect_eq} and
|
|
735 |
\ttindexbold{Collect_mem_eq} assert that the functions {\tt Collect} and
|
|
736 |
\hbox{\tt op :} are isomorphisms.
|
287
|
737 |
All the other axioms are definitions; see Fig.\ts \ref{hol-set-rules}.
|
104
|
738 |
These include straightforward properties of functions: image~({\tt``}) and
|
|
739 |
{\tt range}, and predicates concerning monotonicity, injectiveness, etc.
|
|
740 |
|
306
|
741 |
\HOL's set theory has the {\ML} identifier \ttindexbold{Set.thy}.
|
104
|
742 |
|
287
|
743 |
\begin{figure} \underscoreon
|
104
|
744 |
\begin{ttbox}
|
|
745 |
\idx{imageI} [| x:A |] ==> f(x) : f``A
|
|
746 |
\idx{imageE} [| b : f``A; !!x.[| b=f(x); x:A |] ==> P |] ==> P
|
|
747 |
|
|
748 |
\idx{rangeI} f(x) : range(f)
|
|
749 |
\idx{rangeE} [| b : range(f); !!x.[| b=f(x) |] ==> P |] ==> P
|
|
750 |
|
|
751 |
\idx{monoI} [| !!A B. A <= B ==> f(A) <= f(B) |] ==> mono(f)
|
|
752 |
\idx{monoD} [| mono(f); A <= B |] ==> f(A) <= f(B)
|
|
753 |
|
|
754 |
\idx{injI} [| !! x y. f(x) = f(y) ==> x=y |] ==> inj(f)
|
|
755 |
\idx{inj_inverseI} (!!x. g(f(x)) = x) ==> inj(f)
|
|
756 |
\idx{injD} [| inj(f); f(x) = f(y) |] ==> x=y
|
|
757 |
|
|
758 |
\idx{Inv_f_f} inj(f) ==> Inv(f,f(x)) = x
|
|
759 |
\idx{f_Inv_f} y : range(f) ==> f(Inv(f,y)) = y
|
|
760 |
|
|
761 |
\idx{Inv_injective}
|
|
762 |
[| Inv(f,x)=Inv(f,y); x: range(f); y: range(f) |] ==> x=y
|
|
763 |
|
|
764 |
\idx{inj_ontoI}
|
|
765 |
(!! x y. [| f(x) = f(y); x:A; y:A |] ==> x=y) ==> inj_onto(f,A)
|
|
766 |
|
|
767 |
\idx{inj_onto_inverseI}
|
|
768 |
(!!x. x:A ==> g(f(x)) = x) ==> inj_onto(f,A)
|
|
769 |
|
|
770 |
\idx{inj_ontoD}
|
|
771 |
[| inj_onto(f,A); f(x)=f(y); x:A; y:A |] ==> x=y
|
|
772 |
|
|
773 |
\idx{inj_onto_contraD}
|
|
774 |
[| inj_onto(f,A); x~=y; x:A; y:A |] ==> ~ f(x)=f(y)
|
|
775 |
\end{ttbox}
|
|
776 |
\caption{Derived rules involving functions} \label{hol-fun}
|
|
777 |
\end{figure}
|
|
778 |
|
|
779 |
|
287
|
780 |
\begin{figure} \underscoreon
|
104
|
781 |
\begin{ttbox}
|
|
782 |
\idx{Union_upper} B:A ==> B <= Union(A)
|
|
783 |
\idx{Union_least} [| !!X. X:A ==> X<=C |] ==> Union(A) <= C
|
|
784 |
|
|
785 |
\idx{Inter_lower} B:A ==> Inter(A) <= B
|
|
786 |
\idx{Inter_greatest} [| !!X. X:A ==> C<=X |] ==> C <= Inter(A)
|
|
787 |
|
|
788 |
\idx{Un_upper1} A <= A Un B
|
|
789 |
\idx{Un_upper2} B <= A Un B
|
|
790 |
\idx{Un_least} [| A<=C; B<=C |] ==> A Un B <= C
|
|
791 |
|
|
792 |
\idx{Int_lower1} A Int B <= A
|
|
793 |
\idx{Int_lower2} A Int B <= B
|
|
794 |
\idx{Int_greatest} [| C<=A; C<=B |] ==> C <= A Int B
|
|
795 |
\end{ttbox}
|
|
796 |
\caption{Derived rules involving subsets} \label{hol-subset}
|
|
797 |
\end{figure}
|
|
798 |
|
|
799 |
|
287
|
800 |
\begin{figure} \underscoreon
|
104
|
801 |
\begin{ttbox}
|
|
802 |
\idx{Int_absorb} A Int A = A
|
|
803 |
\idx{Int_commute} A Int B = B Int A
|
|
804 |
\idx{Int_assoc} (A Int B) Int C = A Int (B Int C)
|
|
805 |
\idx{Int_Un_distrib} (A Un B) Int C = (A Int C) Un (B Int C)
|
|
806 |
|
|
807 |
\idx{Un_absorb} A Un A = A
|
|
808 |
\idx{Un_commute} A Un B = B Un A
|
|
809 |
\idx{Un_assoc} (A Un B) Un C = A Un (B Un C)
|
|
810 |
\idx{Un_Int_distrib} (A Int B) Un C = (A Un C) Int (B Un C)
|
|
811 |
|
|
812 |
\idx{Compl_disjoint} A Int Compl(A) = \{x.False\}
|
|
813 |
\idx{Compl_partition} A Un Compl(A) = \{x.True\}
|
|
814 |
\idx{double_complement} Compl(Compl(A)) = A
|
|
815 |
\idx{Compl_Un} Compl(A Un B) = Compl(A) Int Compl(B)
|
|
816 |
\idx{Compl_Int} Compl(A Int B) = Compl(A) Un Compl(B)
|
|
817 |
|
|
818 |
\idx{Union_Un_distrib} Union(A Un B) = Union(A) Un Union(B)
|
287
|
819 |
\idx{Int_Union} A Int Union(B) = (UN C:B. A Int C)
|
104
|
820 |
\idx{Un_Union_image}
|
|
821 |
(UN x:C. A(x) Un B(x)) = Union(A``C) Un Union(B``C)
|
|
822 |
|
|
823 |
\idx{Inter_Un_distrib} Inter(A Un B) = Inter(A) Int Inter(B)
|
287
|
824 |
\idx{Un_Inter} A Un Inter(B) = (INT C:B. A Un C)
|
104
|
825 |
\idx{Int_Inter_image}
|
|
826 |
(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)
|
|
827 |
\end{ttbox}
|
|
828 |
\caption{Set equalities} \label{hol-equalities}
|
|
829 |
\end{figure}
|
|
830 |
|
|
831 |
|
|
832 |
\subsection{Derived rules for sets}
|
|
833 |
Figures~\ref{hol-set1} and~\ref{hol-set2} present derived rules. Most
|
|
834 |
are obvious and resemble rules of Isabelle's {\ZF} set theory. The
|
|
835 |
rules named $XXX${\tt_cong} break down equalities. Certain rules, such as
|
|
836 |
\ttindexbold{subsetCE}, \ttindexbold{bexCI} and \ttindexbold{UnCI}, are
|
|
837 |
designed for classical reasoning; the more natural rules \ttindexbold{subsetD},
|
|
838 |
\ttindexbold{bexI}, \ttindexbold{Un1} and~\ttindexbold{Un2} are not
|
|
839 |
strictly necessary. Similarly, \ttindexbold{equalityCE} supports classical
|
|
840 |
reasoning about extensionality, after the fashion of \ttindex{iffCE}. See
|
287
|
841 |
the file {\tt HOL/set.ML} for proofs pertaining to set theory.
|
104
|
842 |
|
287
|
843 |
Figure~\ref{hol-fun} presents derived inference rules involving functions. See
|
|
844 |
the file {\tt HOL/fun.ML} for a complete listing.
|
104
|
845 |
|
|
846 |
Figure~\ref{hol-subset} presents lattice properties of the subset relation.
|
287
|
847 |
See the file {\tt HOL/subset.ML}.
|
104
|
848 |
|
|
849 |
Figure~\ref{hol-equalities} presents set equalities. See
|
287
|
850 |
{\tt HOL/equalities.ML}.
|
104
|
851 |
|
|
852 |
|
287
|
853 |
\begin{figure}
|
104
|
854 |
\begin{center}
|
|
855 |
\begin{tabular}{rrr}
|
111
|
856 |
\it name &\it meta-type & \it description \\
|
|
857 |
\idx{Pair} & $[\alpha,\beta]\To \alpha\times\beta$
|
|
858 |
& ordered pairs $\langle a,b\rangle$ \\
|
287
|
859 |
\idx{fst} & $\alpha\times\beta \To \alpha$ & first projection\\
|
111
|
860 |
\idx{snd} & $\alpha\times\beta \To \beta$ & second projection\\
|
|
861 |
\idx{split} & $[\alpha\times\beta, [\alpha,\beta]\To\gamma] \To \gamma$
|
287
|
862 |
& generalized projection\\
|
|
863 |
\idx{Sigma} &
|
|
864 |
$[\alpha\,set, \alpha\To\beta\,set]\To(\alpha\times\beta)set$ &
|
|
865 |
general sum of sets
|
104
|
866 |
\end{tabular}
|
|
867 |
\end{center}
|
|
868 |
\subcaption{Constants}
|
|
869 |
|
287
|
870 |
\begin{ttbox}\makeatletter
|
104
|
871 |
\idx{fst_def} fst(p) == @a. ? b. p = <a,b>
|
|
872 |
\idx{snd_def} snd(p) == @b. ? a. p = <a,b>
|
|
873 |
\idx{split_def} split(p,c) == c(fst(p),snd(p))
|
287
|
874 |
\idx{Sigma_def} Sigma(A,B) == UN x:A. UN y:B(x). \{<x,y>\}
|
104
|
875 |
\subcaption{Definitions}
|
|
876 |
|
|
877 |
\idx{Pair_inject} [| <a, b> = <a',b'>; [| a=a'; b=b' |] ==> R |] ==> R
|
|
878 |
|
|
879 |
\idx{fst} fst(<a,b>) = a
|
|
880 |
\idx{snd} snd(<a,b>) = b
|
|
881 |
\idx{split} split(<a,b>, c) = c(a,b)
|
|
882 |
|
|
883 |
\idx{surjective_pairing} p = <fst(p),snd(p)>
|
287
|
884 |
|
|
885 |
\idx{SigmaI} [| a:A; b:B(a) |] ==> <a,b> : Sigma(A,B)
|
|
886 |
|
|
887 |
\idx{SigmaE} [| c: Sigma(A,B);
|
|
888 |
!!x y.[| x:A; y:B(x); c=<x,y> |] ==> P |] ==> P
|
104
|
889 |
\subcaption{Derived rules}
|
|
890 |
\end{ttbox}
|
|
891 |
\caption{Type $\alpha\times\beta$}
|
|
892 |
\label{hol-prod}
|
|
893 |
\end{figure}
|
|
894 |
|
|
895 |
|
287
|
896 |
\begin{figure}
|
104
|
897 |
\begin{center}
|
|
898 |
\begin{tabular}{rrr}
|
111
|
899 |
\it name &\it meta-type & \it description \\
|
|
900 |
\idx{Inl} & $\alpha \To \alpha+\beta$ & first injection\\
|
|
901 |
\idx{Inr} & $\beta \To \alpha+\beta$ & second injection\\
|
306
|
902 |
\idx{sum_case} & $[\alpha+\beta, \alpha\To\gamma, \beta\To\gamma] \To\gamma$
|
111
|
903 |
& conditional
|
104
|
904 |
\end{tabular}
|
|
905 |
\end{center}
|
|
906 |
\subcaption{Constants}
|
|
907 |
|
287
|
908 |
\begin{ttbox}\makeatletter
|
306
|
909 |
\idx{sum_case_def} sum_case == (\%p f g. @z. (!x. p=Inl(x) --> z=f(x)) &
|
|
910 |
(!y. p=Inr(y) --> z=g(y)))
|
104
|
911 |
\subcaption{Definition}
|
|
912 |
|
|
913 |
\idx{Inl_not_Inr} ~ Inl(a)=Inr(b)
|
|
914 |
|
|
915 |
\idx{inj_Inl} inj(Inl)
|
|
916 |
\idx{inj_Inr} inj(Inr)
|
|
917 |
|
|
918 |
\idx{sumE} [| !!x::'a. P(Inl(x)); !!y::'b. P(Inr(y)) |] ==> P(s)
|
|
919 |
|
306
|
920 |
\idx{sum_case_Inl} sum_case(Inl(x), f, g) = f(x)
|
|
921 |
\idx{sum_case_Inr} sum_case(Inr(x), f, g) = g(x)
|
104
|
922 |
|
306
|
923 |
\idx{surjective_sum} sum_case(s, %x::'a. f(Inl(x)), %y::'b. f(Inr(y))) = f(s)
|
104
|
924 |
\subcaption{Derived rules}
|
|
925 |
\end{ttbox}
|
|
926 |
\caption{Rules for type $\alpha+\beta$}
|
|
927 |
\label{hol-sum}
|
|
928 |
\end{figure}
|
|
929 |
|
|
930 |
|
|
931 |
\section{Types}
|
|
932 |
The basic higher-order logic is augmented with a tremendous amount of
|
|
933 |
material, including support for recursive function and type definitions.
|
|
934 |
Space does not permit a detailed discussion. The present section describes
|
|
935 |
product, sum, natural number and list types.
|
|
936 |
|
|
937 |
\subsection{Product and sum types}
|
306
|
938 |
\HOL\ defines the product type $\alpha\times\beta$ and the sum type
|
104
|
939 |
$\alpha+\beta$, with the ordered pair syntax {\tt<$a$,$b$>}, using fairly
|
287
|
940 |
standard constructions (Figs.~\ref{hol-prod} and~\ref{hol-sum}). Because
|
|
941 |
Isabelle does not support abstract type definitions, the isomorphisms
|
|
942 |
between these types and their representations are made explicitly.
|
104
|
943 |
|
|
944 |
Most of the definitions are suppressed, but observe that the projections
|
|
945 |
and conditionals are defined as descriptions. Their properties are easily
|
287
|
946 |
proved using \ttindex{select_equality}. See {\tt HOL/prod.thy} and
|
|
947 |
{\tt HOL/sum.thy} for details.
|
104
|
948 |
|
287
|
949 |
\begin{figure}
|
104
|
950 |
\indexbold{*"<}
|
|
951 |
\begin{center}
|
|
952 |
\begin{tabular}{rrr}
|
111
|
953 |
\it symbol & \it meta-type & \it description \\
|
|
954 |
\idx{0} & $nat$ & zero \\
|
|
955 |
\idx{Suc} & $nat \To nat$ & successor function\\
|
104
|
956 |
\idx{nat_case} & $[nat, \alpha, nat\To\alpha] \To\alpha$
|
111
|
957 |
& conditional\\
|
104
|
958 |
\idx{nat_rec} & $[nat, \alpha, [nat, \alpha]\To\alpha] \To \alpha$
|
111
|
959 |
& primitive recursor\\
|
104
|
960 |
\idx{pred_nat} & $(nat\times nat) set$ & predecessor relation
|
|
961 |
\end{tabular}
|
|
962 |
\end{center}
|
|
963 |
|
|
964 |
\begin{center}
|
|
965 |
\indexbold{*"+}
|
|
966 |
\index{*@{\tt*}|bold}
|
|
967 |
\index{/@{\tt/}|bold}
|
|
968 |
\index{//@{\tt//}|bold}
|
|
969 |
\index{+@{\tt+}|bold}
|
|
970 |
\index{-@{\tt-}|bold}
|
|
971 |
\begin{tabular}{rrrr}
|
111
|
972 |
\it symbol & \it meta-type & \it precedence & \it description \\
|
|
973 |
\tt * & $[nat,nat]\To nat$ & Left 70 & multiplication \\
|
|
974 |
\tt / & $[nat,nat]\To nat$ & Left 70 & division\\
|
|
975 |
\tt // & $[nat,nat]\To nat$ & Left 70 & modulus\\
|
|
976 |
\tt + & $[nat,nat]\To nat$ & Left 65 & addition\\
|
|
977 |
\tt - & $[nat,nat]\To nat$ & Left 65 & subtraction
|
104
|
978 |
\end{tabular}
|
|
979 |
\end{center}
|
|
980 |
\subcaption{Constants and infixes}
|
|
981 |
|
287
|
982 |
\begin{ttbox}\makeatother
|
|
983 |
\idx{nat_case_def} nat_case == (\%n a f. @z. (n=0 --> z=a) &
|
104
|
984 |
(!x. n=Suc(x) --> z=f(x)))
|
|
985 |
\idx{pred_nat_def} pred_nat == \{p. ? n. p = <n, Suc(n)>\}
|
|
986 |
\idx{less_def} m<n == <m,n>:pred_nat^+
|
|
987 |
\idx{nat_rec_def} nat_rec(n,c,d) ==
|
287
|
988 |
wfrec(pred_nat, n, \%l g.nat_case(l, c, \%m.d(m,g(m))))
|
104
|
989 |
|
287
|
990 |
\idx{add_def} m+n == nat_rec(m, n, \%u v.Suc(v))
|
|
991 |
\idx{diff_def} m-n == nat_rec(n, m, \%u v. nat_rec(v, 0, \%x y.x))
|
|
992 |
\idx{mult_def} m*n == nat_rec(m, 0, \%u v. n + v)
|
|
993 |
\idx{mod_def} m//n == wfrec(trancl(pred_nat), m, \%j f. if(j<n,j,f(j-n)))
|
104
|
994 |
\idx{quo_def} m/n == wfrec(trancl(pred_nat),
|
287
|
995 |
m, \%j f. if(j<n,0,Suc(f(j-n))))
|
104
|
996 |
\subcaption{Definitions}
|
|
997 |
\end{ttbox}
|
|
998 |
\caption{Defining $nat$, the type of natural numbers} \label{hol-nat1}
|
|
999 |
\end{figure}
|
|
1000 |
|
|
1001 |
|
287
|
1002 |
\begin{figure} \underscoreon
|
104
|
1003 |
\begin{ttbox}
|
|
1004 |
\idx{nat_induct} [| P(0); !!k. [| P(k) |] ==> P(Suc(k)) |] ==> P(n)
|
|
1005 |
|
|
1006 |
\idx{Suc_not_Zero} Suc(m) ~= 0
|
|
1007 |
\idx{inj_Suc} inj(Suc)
|
|
1008 |
\idx{n_not_Suc_n} n~=Suc(n)
|
|
1009 |
\subcaption{Basic properties}
|
|
1010 |
|
|
1011 |
\idx{pred_natI} <n, Suc(n)> : pred_nat
|
|
1012 |
\idx{pred_natE}
|
|
1013 |
[| p : pred_nat; !!x n. [| p = <n, Suc(n)> |] ==> R |] ==> R
|
|
1014 |
|
|
1015 |
\idx{nat_case_0} nat_case(0, a, f) = a
|
|
1016 |
\idx{nat_case_Suc} nat_case(Suc(k), a, f) = f(k)
|
|
1017 |
|
|
1018 |
\idx{wf_pred_nat} wf(pred_nat)
|
|
1019 |
\idx{nat_rec_0} nat_rec(0,c,h) = c
|
|
1020 |
\idx{nat_rec_Suc} nat_rec(Suc(n), c, h) = h(n, nat_rec(n,c,h))
|
|
1021 |
\subcaption{Case analysis and primitive recursion}
|
|
1022 |
|
|
1023 |
\idx{less_trans} [| i<j; j<k |] ==> i<k
|
|
1024 |
\idx{lessI} n < Suc(n)
|
|
1025 |
\idx{zero_less_Suc} 0 < Suc(n)
|
|
1026 |
|
|
1027 |
\idx{less_not_sym} n<m --> ~ m<n
|
|
1028 |
\idx{less_not_refl} ~ n<n
|
|
1029 |
\idx{not_less0} ~ n<0
|
|
1030 |
|
|
1031 |
\idx{Suc_less_eq} (Suc(m) < Suc(n)) = (m<n)
|
|
1032 |
\idx{less_induct} [| !!n. [| ! m. m<n --> P(m) |] ==> P(n) |] ==> P(n)
|
|
1033 |
|
|
1034 |
\idx{less_linear} m<n | m=n | n<m
|
|
1035 |
\subcaption{The less-than relation}
|
|
1036 |
\end{ttbox}
|
|
1037 |
\caption{Derived rules for~$nat$} \label{hol-nat2}
|
|
1038 |
\end{figure}
|
|
1039 |
|
|
1040 |
|
|
1041 |
\subsection{The type of natural numbers, $nat$}
|
306
|
1042 |
\HOL\ defines the natural numbers in a roundabout but traditional way.
|
104
|
1043 |
The axiom of infinity postulates an type~$ind$ of individuals, which is
|
|
1044 |
non-empty and closed under an injective operation. The natural numbers are
|
|
1045 |
inductively generated by choosing an arbitrary individual for~0 and using
|
|
1046 |
the injective operation to take successors. As usual, the isomorphisms
|
|
1047 |
between~$nat$ and its representation are made explicitly.
|
|
1048 |
|
|
1049 |
The definition makes use of a least fixed point operator \ttindex{lfp},
|
|
1050 |
defined using the Knaster-Tarski theorem. This in turn defines an operator
|
|
1051 |
\ttindex{trancl} for taking the transitive closure of a relation. See
|
287
|
1052 |
files {\tt HOL/lfp.thy} and {\tt HOL/trancl.thy} for
|
|
1053 |
details. The definition of~$nat$ resides on {\tt HOL/nat.thy}.
|
104
|
1054 |
|
|
1055 |
Type $nat$ is postulated to belong to class~$ord$, which overloads $<$ and
|
|
1056 |
$\leq$ on the natural numbers. As of this writing, Isabelle provides no
|
|
1057 |
means of verifying that such overloading is sensible. On the other hand,
|
306
|
1058 |
the \HOL\ theory includes no polymorphic axioms stating general properties
|
104
|
1059 |
of $<$ and $\leq$.
|
|
1060 |
|
287
|
1061 |
File {\tt HOL/arith.ML} develops arithmetic on the natural numbers.
|
104
|
1062 |
It defines addition, multiplication, subtraction, division, and remainder,
|
|
1063 |
proving the theorem $a \bmod b + (a/b)\times b = a$. Division and
|
|
1064 |
remainder are defined by repeated subtraction, which requires well-founded
|
|
1065 |
rather than primitive recursion.
|
|
1066 |
|
|
1067 |
Primitive recursion makes use of \ttindex{wfrec}, an operator for recursion
|
287
|
1068 |
along arbitrary well-founded relations; see {\tt HOL/wf.ML} for the
|
104
|
1069 |
development. The predecessor relation, \ttindexbold{pred_nat}, is shown to
|
|
1070 |
be well-founded; recursion along this relation is primitive recursion,
|
|
1071 |
while its transitive closure is~$<$.
|
|
1072 |
|
287
|
1073 |
\begin{figure}
|
104
|
1074 |
\begin{center}
|
|
1075 |
\begin{tabular}{rrr}
|
111
|
1076 |
\it symbol & \it meta-type & \it description \\
|
306
|
1077 |
\idx{Nil} & $\alpha list$ & empty list\\
|
|
1078 |
\idx{null} & $\alpha list \To bool$ & emptyness test\\
|
|
1079 |
\idx{hd} & $\alpha list \To \alpha$ & head \\
|
|
1080 |
\idx{tl} & $\alpha list \To \alpha list$ & tail \\
|
|
1081 |
\idx{ttl} & $\alpha list \To \alpha list$ & total tail \\
|
|
1082 |
\idx{map} & $(\alpha\To\beta) \To (\alpha list \To \beta list)$
|
|
1083 |
& mapping functional\\
|
|
1084 |
\idx{list_all}& $(\alpha \To bool) \To (\alpha list \To bool)$
|
|
1085 |
& forall functional\\
|
|
1086 |
\idx{filter} & $(\alpha \To bool) \To (\alpha list \To \alpha list)$
|
|
1087 |
& filter functional\\
|
111
|
1088 |
\idx{list_rec} & $[\alpha list, \beta, [\alpha ,\alpha list,
|
104
|
1089 |
\beta]\To\beta] \To \beta$
|
306
|
1090 |
& list recursor
|
|
1091 |
\end{tabular}
|
|
1092 |
\end{center}
|
|
1093 |
|
|
1094 |
\begin{center}
|
|
1095 |
\index{"# @{\tt\#}|bold}
|
|
1096 |
\index{"@@{\tt\at}|bold}
|
|
1097 |
\begin{tabular}{rrrr}
|
|
1098 |
\it symbol & \it meta-type & \it precedence & \it description \\
|
|
1099 |
\tt \# & $[\alpha,\alpha list]\To \alpha list$ & Right 65 & cons \\
|
|
1100 |
\tt\at & $[\alpha list,\alpha list]\To \alpha list$ & Left 65 & append \\
|
|
1101 |
\idx{mem} & $[\alpha,\alpha list]\To bool$ & Left 55 & membership
|
104
|
1102 |
\end{tabular}
|
|
1103 |
\end{center}
|
306
|
1104 |
\subcaption{Constants and infixes}
|
|
1105 |
|
|
1106 |
\begin{center} \tt\frenchspacing
|
|
1107 |
\begin{tabular}{rrr}
|
|
1108 |
\it external & \it internal & \it description \\{}
|
|
1109 |
\idx{[]} & Nil & empty list \\{}
|
|
1110 |
[$x@1$, $\dots$, $x@n$] & $x@1$\#$\cdots$\#$x@n$\#[] &
|
|
1111 |
\rm finite list \\{}
|
|
1112 |
[$x$:$xs$ . $P$] & filter(\%$x$.$P$,$xs$) & list comprehension\\
|
|
1113 |
\begin{tabular}{r@{}l}
|
|
1114 |
\idx{case} $e$ of&\ [] => $a$\\
|
|
1115 |
|&\ $x$\#$xs$ => $b$
|
|
1116 |
\end{tabular} & list_case($e$,$a$,\%$x~xs$.$b$)
|
|
1117 |
& case analysis
|
|
1118 |
\end{tabular}
|
|
1119 |
\end{center}
|
|
1120 |
\subcaption{Translations}
|
104
|
1121 |
|
|
1122 |
\begin{ttbox}
|
306
|
1123 |
\idx{list_induct} [| P([]); !!x xs. [| P(xs) |] ==> P(x#xs)) |] ==> P(l)
|
104
|
1124 |
|
306
|
1125 |
\idx{Cons_not_Nil} (x # xs) ~= []
|
|
1126 |
\idx{Cons_Cons_eq} ((x # xs) = (y # ys)) = (x=y & xs=ys)
|
|
1127 |
\subcaption{Induction and freeness}
|
104
|
1128 |
\end{ttbox}
|
|
1129 |
\caption{The type of lists and its operations} \label{hol-list}
|
|
1130 |
\end{figure}
|
|
1131 |
|
306
|
1132 |
\begin{figure}
|
|
1133 |
\begin{ttbox}\makeatother
|
|
1134 |
list_rec([],c,h) = c list_rec(a \# l, c, h) = h(a, l, list_rec(l,c,h))
|
|
1135 |
list_case([],c,h) = c list_case(x # xs, c, h) = h(x, xs)
|
|
1136 |
map(f,[]) = [] map(f, x \# xs) = f(x) \# map(f,xs)
|
|
1137 |
null([]) = True null(x # xs) = False
|
|
1138 |
hd(x # xs) = x tl(x # xs) = xs
|
|
1139 |
ttl([]) = [] ttl(x # xs) = xs
|
|
1140 |
[] @ ys = ys (x # xs) \at ys = x # xs \at ys
|
|
1141 |
x mem [] = False x mem y # ys = if(y = x, True, x mem ys)
|
|
1142 |
filter(P, []) = [] filter(P,x#xs) = if(P(x),x#filter(P,xs),filter(P,xs))
|
|
1143 |
list_all(P,[]) = True list_all(P, x # xs) = (P(x) & list_all(P, xs))
|
|
1144 |
\end{ttbox}
|
|
1145 |
\caption{Rewrite rules for lists} \label{hol-list-simps}
|
|
1146 |
\end{figure}
|
104
|
1147 |
|
|
1148 |
\subsection{The type constructor for lists, $\alpha\,list$}
|
306
|
1149 |
\HOL's definition of lists is an example of an experimental method for
|
|
1150 |
handling recursive data types. The details need not concern us here; see the
|
|
1151 |
file {\tt HOL/list.ML}. Figure~\ref{hol-list} presents the basic list
|
|
1152 |
operations, with their types and properties. In particular,
|
104
|
1153 |
\ttindexbold{list_rec} is a primitive recursion operator for lists, in the
|
|
1154 |
style of Martin-L\"of type theory. It is derived from well-founded
|
|
1155 |
recursion, a general principle that can express arbitrary total recursive
|
306
|
1156 |
functions. The basic rewrite rules shown in Fig.~\ref{hol-list-simps} are
|
|
1157 |
contained, together with additional useful lemmas, in the simpset {\tt
|
|
1158 |
list_ss}. Induction over the variable $xs$ in subgoal $i$ is performed by
|
|
1159 |
{\tt list_ind_tac "$xs$" $i$}.
|
104
|
1160 |
|
|
1161 |
|
|
1162 |
\subsection{The type constructor for lazy lists, $\alpha\,llist$}
|
|
1163 |
The definition of lazy lists demonstrates methods for handling infinite
|
|
1164 |
data structures and co-induction in higher-order logic. It defines an
|
|
1165 |
operator for co-recursion on lazy lists, which is used to define a few
|
|
1166 |
simple functions such as map and append. Co-recursion cannot easily define
|
|
1167 |
operations such as filter, which can compute indefinitely before yielding
|
|
1168 |
the next element (if any!) of the lazy list. A co-induction principle is
|
|
1169 |
defined for proving equations on lazy lists. See the files
|
287
|
1170 |
{\tt HOL/llist.thy} and {\tt HOL/llist.ML} for the formal
|
104
|
1171 |
derivations. I have written a report discussing the treatment of lazy
|
|
1172 |
lists, and finite lists also~\cite{paulson-coind}.
|
|
1173 |
|
|
1174 |
|
|
1175 |
\section{Classical proof procedures} \label{hol-cla-prover}
|
306
|
1176 |
\HOL\ derives classical introduction rules for $\disj$ and~$\exists$, as
|
104
|
1177 |
well as classical elimination rules for~$\imp$ and~$\bimp$, and the swap
|
287
|
1178 |
rule (Fig.~\ref{hol-lemmas2}).
|
104
|
1179 |
|
|
1180 |
The classical reasoning module is set up for \HOL, as the structure
|
|
1181 |
\ttindexbold{Classical}. This structure is open, so {\ML} identifiers such
|
|
1182 |
as {\tt step_tac}, {\tt fast_tac}, {\tt best_tac}, etc., refer to it.
|
|
1183 |
|
306
|
1184 |
\HOL\ defines the following classical rule sets:
|
104
|
1185 |
\begin{ttbox}
|
|
1186 |
prop_cs : claset
|
|
1187 |
HOL_cs : claset
|
|
1188 |
HOL_dup_cs : claset
|
|
1189 |
set_cs : claset
|
|
1190 |
\end{ttbox}
|
|
1191 |
\begin{description}
|
|
1192 |
\item[\ttindexbold{prop_cs}] contains the propositional rules, namely
|
|
1193 |
those for~$\top$, $\bot$, $\conj$, $\disj$, $\neg$, $\imp$ and~$\bimp$,
|
|
1194 |
along with the rule~\ttindex{refl}.
|
|
1195 |
|
|
1196 |
\item[\ttindexbold{HOL_cs}]
|
|
1197 |
extends {\tt prop_cs} with the safe rules \ttindex{allI} and~\ttindex{exE}
|
|
1198 |
and the unsafe rules \ttindex{allE} and~\ttindex{exI}, as well as rules for
|
|
1199 |
unique existence. Search using this is incomplete since quantified
|
|
1200 |
formulae are used at most once.
|
|
1201 |
|
|
1202 |
\item[\ttindexbold{HOL_dup_cs}]
|
|
1203 |
extends {\tt prop_cs} with the safe rules \ttindex{allI} and~\ttindex{exE}
|
|
1204 |
and the unsafe rules \ttindex{all_dupE} and~\ttindex{exCI}, as well as
|
|
1205 |
rules for unique existence. Search using this is complete --- quantified
|
|
1206 |
formulae may be duplicated --- but frequently fails to terminate. It is
|
|
1207 |
generally unsuitable for depth-first search.
|
|
1208 |
|
|
1209 |
\item[\ttindexbold{set_cs}]
|
|
1210 |
extends {\tt HOL_cs} with rules for the bounded quantifiers, subsets,
|
|
1211 |
comprehensions, unions/intersections, complements, finite setes, images and
|
|
1212 |
ranges.
|
|
1213 |
\end{description}
|
|
1214 |
\noindent
|
|
1215 |
See the {\em Reference Manual} for more discussion of classical proof
|
|
1216 |
methods.
|
|
1217 |
|
|
1218 |
|
111
|
1219 |
\section{The examples directories}
|
|
1220 |
Directory {\tt Subst} contains Martin Coen's mechanization of a theory of
|
|
1221 |
substitutions and unifiers. It is based on Paulson's previous
|
114
|
1222 |
mechanization in {\LCF}~\cite{paulson85} of Manna and Waldinger's
|
111
|
1223 |
theory~\cite{mw81}.
|
|
1224 |
|
|
1225 |
Directory {\tt ex} contains other examples and experimental proofs in
|
306
|
1226 |
\HOL. Here is an overview of the more interesting files.
|
104
|
1227 |
\begin{description}
|
287
|
1228 |
\item[{\tt HOL/ex/meson.ML}]
|
104
|
1229 |
contains an experimental implementation of the MESON proof procedure,
|
|
1230 |
inspired by Plaisted~\cite{plaisted90}. It is much more powerful than
|
|
1231 |
Isabelle's classical module.
|
|
1232 |
|
287
|
1233 |
\item[{\tt HOL/ex/mesontest.ML}]
|
104
|
1234 |
contains test data for the MESON proof procedure.
|
|
1235 |
|
287
|
1236 |
\item[{\tt HOL/ex/set.ML}]
|
|
1237 |
proves Cantor's Theorem, which is presented below, and the
|
|
1238 |
Schr\"oder-Bernstein Theorem.
|
104
|
1239 |
|
287
|
1240 |
\item[{\tt HOL/ex/pl.ML}]
|
104
|
1241 |
proves the soundness and completeness of classical propositional logic,
|
|
1242 |
given a truth table semantics. The only connective is $\imp$. A
|
|
1243 |
Hilbert-style axiom system is specified, and its set of theorems defined
|
|
1244 |
inductively.
|
|
1245 |
|
287
|
1246 |
\item[{\tt HOL/ex/term.ML}]
|
111
|
1247 |
contains proofs about an experimental recursive type definition;
|
|
1248 |
the recursion goes through the type constructor~$list$.
|
104
|
1249 |
|
287
|
1250 |
\item[{\tt HOL/ex/simult.ML}]
|
104
|
1251 |
defines primitives for solving mutually recursive equations over sets.
|
|
1252 |
It constructs sets of trees and forests as an example, including induction
|
|
1253 |
and recursion rules that handle the mutual recursion.
|
111
|
1254 |
|
287
|
1255 |
\item[{\tt HOL/ex/mt.ML}]
|
111
|
1256 |
contains Jacob Frost's formalization~\cite{frost93} of a co-induction
|
|
1257 |
example by Milner and Tofte~\cite{milner-coind}.
|
104
|
1258 |
\end{description}
|
|
1259 |
|
|
1260 |
|
|
1261 |
\section{Example: deriving the conjunction rules}
|
306
|
1262 |
\HOL\ comes with a body of derived rules, ranging from simple properties
|
104
|
1263 |
of the logical constants and set theory to well-founded recursion. Many of
|
|
1264 |
them are worth studying.
|
|
1265 |
|
|
1266 |
Deriving natural deduction rules for the logical constants from their
|
|
1267 |
definitions is an archetypal example of higher-order reasoning. Let us
|
|
1268 |
verify two conjunction rules:
|
|
1269 |
\[ \infer[({\conj}I)]{P\conj Q}{P & Q} \qquad\qquad
|
|
1270 |
\infer[({\conj}E1)]{P}{P\conj Q}
|
|
1271 |
\]
|
|
1272 |
|
|
1273 |
\subsection{The introduction rule}
|
|
1274 |
We begin by stating the rule as the goal. The list of premises $[P,Q]$ is
|
|
1275 |
bound to the {\ML} variable~{\tt prems}.
|
|
1276 |
\begin{ttbox}
|
|
1277 |
val prems = goal HOL.thy "[| P; Q |] ==> P&Q";
|
|
1278 |
{\out Level 0}
|
|
1279 |
{\out P & Q}
|
|
1280 |
{\out 1. P & Q}
|
111
|
1281 |
{\out val prems = ["P [P]", "Q [Q]"] : thm list}
|
104
|
1282 |
\end{ttbox}
|
|
1283 |
The next step is to unfold the definition of conjunction. But
|
306
|
1284 |
\ttindex{and_def} uses \HOL's internal equality, so
|
104
|
1285 |
\ttindex{rewrite_goals_tac} is unsuitable.
|
|
1286 |
Instead, we perform substitution using the rule \ttindex{ssubst}:
|
|
1287 |
\begin{ttbox}
|
|
1288 |
by (resolve_tac [and_def RS ssubst] 1);
|
|
1289 |
{\out Level 1}
|
|
1290 |
{\out P & Q}
|
|
1291 |
{\out 1. ! R. (P --> Q --> R) --> R}
|
|
1292 |
\end{ttbox}
|
|
1293 |
We now apply $(\forall I)$ and $({\imp}I)$:
|
|
1294 |
\begin{ttbox}
|
|
1295 |
by (resolve_tac [allI] 1);
|
|
1296 |
{\out Level 2}
|
|
1297 |
{\out P & Q}
|
|
1298 |
{\out 1. !!R. (P --> Q --> R) --> R}
|
287
|
1299 |
\ttbreak
|
104
|
1300 |
by (resolve_tac [impI] 1);
|
|
1301 |
{\out Level 3}
|
|
1302 |
{\out P & Q}
|
|
1303 |
{\out 1. !!R. P --> Q --> R ==> R}
|
|
1304 |
\end{ttbox}
|
|
1305 |
The assumption is a nested implication, which may be eliminated
|
|
1306 |
using~\ttindex{mp} resolved with itself. Elim-resolution, here, performs
|
|
1307 |
backwards chaining. More straightforward would be to use~\ttindex{impE}
|
|
1308 |
twice.
|
|
1309 |
\index{*RS}
|
|
1310 |
\begin{ttbox}
|
|
1311 |
by (eresolve_tac [mp RS mp] 1);
|
|
1312 |
{\out Level 4}
|
|
1313 |
{\out P & Q}
|
|
1314 |
{\out 1. !!R. P}
|
|
1315 |
{\out 2. !!R. Q}
|
|
1316 |
\end{ttbox}
|
|
1317 |
These two subgoals are simply the premises:
|
|
1318 |
\begin{ttbox}
|
|
1319 |
by (REPEAT (resolve_tac prems 1));
|
|
1320 |
{\out Level 5}
|
|
1321 |
{\out P & Q}
|
|
1322 |
{\out No subgoals!}
|
|
1323 |
\end{ttbox}
|
|
1324 |
|
|
1325 |
|
|
1326 |
\subsection{The elimination rule}
|
|
1327 |
Again, we bind the list of premises (in this case $[P\conj Q]$)
|
|
1328 |
to~{\tt prems}.
|
|
1329 |
\begin{ttbox}
|
|
1330 |
val prems = goal HOL.thy "[| P & Q |] ==> P";
|
|
1331 |
{\out Level 0}
|
|
1332 |
{\out P}
|
|
1333 |
{\out 1. P}
|
111
|
1334 |
{\out val prems = ["P & Q [P & Q]"] : thm list}
|
104
|
1335 |
\end{ttbox}
|
|
1336 |
Working with premises that involve defined constants can be tricky. We
|
|
1337 |
must expand the definition of conjunction in the meta-assumption $P\conj
|
|
1338 |
Q$. The rule \ttindex{subst} performs substitution in forward proofs.
|
287
|
1339 |
We get {\it two\/} resolvents since the vacuous substitution is valid:
|
104
|
1340 |
\begin{ttbox}
|
|
1341 |
prems RL [and_def RS subst];
|
|
1342 |
{\out val it = ["! R. (P --> Q --> R) --> R [P & Q]",}
|
|
1343 |
{\out "P & Q [P & Q]"] : thm list}
|
|
1344 |
\end{ttbox}
|
|
1345 |
By applying $(\forall E)$ and $({\imp}E)$ to the resolvents, we dispose of
|
287
|
1346 |
the vacuous one and put the other into a convenient form:\footnote {Why use
|
|
1347 |
{\tt [spec] RL [mp]} instead of {\tt [spec RS mp]} to join the rules? In
|
|
1348 |
higher-order logic, {\tt spec RS mp} fails because the resolution yields
|
|
1349 |
two results, namely ${\List{\forall x.x; P}\Imp Q}$ and ${\List{\forall
|
|
1350 |
x.P(x)\imp Q(x); P(x)}\Imp Q(x)}$. In first-order logic, the
|
|
1351 |
resolution yields only the latter result because $\forall x.x$ is not a
|
|
1352 |
first-order formula; in fact, it is equivalent to falsity.} \index{*RL}
|
104
|
1353 |
\begin{ttbox}
|
|
1354 |
prems RL [and_def RS subst] RL [spec] RL [mp];
|
|
1355 |
{\out val it = ["P --> Q --> ?Q ==> ?Q [P & Q]"] : thm list}
|
|
1356 |
\end{ttbox}
|
|
1357 |
This is a list containing a single rule, which is directly applicable to
|
|
1358 |
our goal:
|
|
1359 |
\begin{ttbox}
|
|
1360 |
by (resolve_tac it 1);
|
|
1361 |
{\out Level 1}
|
|
1362 |
{\out P}
|
|
1363 |
{\out 1. P --> Q --> P}
|
|
1364 |
\end{ttbox}
|
|
1365 |
The subgoal is a trivial implication. Recall that \ttindex{ares_tac} is a
|
|
1366 |
combination of \ttindex{assume_tac} and \ttindex{resolve_tac}.
|
|
1367 |
\begin{ttbox}
|
|
1368 |
by (REPEAT (ares_tac [impI] 1));
|
|
1369 |
{\out Level 2}
|
|
1370 |
{\out P}
|
|
1371 |
{\out No subgoals!}
|
|
1372 |
\end{ttbox}
|
|
1373 |
|
|
1374 |
|
|
1375 |
\section{Example: Cantor's Theorem}
|
|
1376 |
Cantor's Theorem states that every set has more subsets than it has
|
|
1377 |
elements. It has become a favourite example in higher-order logic since
|
|
1378 |
it is so easily expressed:
|
|
1379 |
\[ \forall f::[\alpha,\alpha]\To bool. \exists S::\alpha\To bool.
|
|
1380 |
\forall x::\alpha. f(x) \not= S
|
|
1381 |
\]
|
|
1382 |
Viewing types as sets, $\alpha\To bool$ represents the powerset
|
|
1383 |
of~$\alpha$. This version states that for every function from $\alpha$ to
|
|
1384 |
its powerset, some subset is outside its range.
|
306
|
1385 |
The Isabelle proof uses \HOL's set theory, with the type $\alpha\,set$ and
|
104
|
1386 |
the operator \ttindex{range}. Since it avoids quantification, we may
|
|
1387 |
inspect the subset found by the proof.
|
|
1388 |
\begin{ttbox}
|
|
1389 |
goal Set.thy "~ ?S : range(f :: 'a=>'a set)";
|
|
1390 |
{\out Level 0}
|
|
1391 |
{\out ~ ?S : range(f)}
|
|
1392 |
{\out 1. ~ ?S : range(f)}
|
|
1393 |
\end{ttbox}
|
|
1394 |
The first two steps are routine. The rule \ttindex{rangeE} reasons that,
|
|
1395 |
since $\Var{S}\in range(f)$, we have $\Var{S}=f(x)$ for some~$x$.
|
|
1396 |
\begin{ttbox}
|
|
1397 |
by (resolve_tac [notI] 1);
|
|
1398 |
{\out Level 1}
|
|
1399 |
{\out ~ ?S : range(f)}
|
|
1400 |
{\out 1. ?S : range(f) ==> False}
|
287
|
1401 |
\ttbreak
|
104
|
1402 |
by (eresolve_tac [rangeE] 1);
|
|
1403 |
{\out Level 2}
|
|
1404 |
{\out ~ ?S : range(f)}
|
|
1405 |
{\out 1. !!x. ?S = f(x) ==> False}
|
|
1406 |
\end{ttbox}
|
|
1407 |
Next, we apply \ttindex{equalityCE}, reasoning that since $\Var{S}=f(x)$,
|
|
1408 |
we have $\Var{c}\in \Var{S}$ if and only if $\Var{c}\in f(x)$ for
|
|
1409 |
any~$\Var{c}$.
|
|
1410 |
\begin{ttbox}
|
|
1411 |
by (eresolve_tac [equalityCE] 1);
|
|
1412 |
{\out Level 3}
|
|
1413 |
{\out ~ ?S : range(f)}
|
|
1414 |
{\out 1. !!x. [| ?c3(x) : ?S; ?c3(x) : f(x) |] ==> False}
|
|
1415 |
{\out 2. !!x. [| ~ ?c3(x) : ?S; ~ ?c3(x) : f(x) |] ==> False}
|
|
1416 |
\end{ttbox}
|
|
1417 |
Now we use a bit of creativity. Suppose that $\Var{S}$ has the form of a
|
|
1418 |
comprehension. Then $\Var{c}\in\{x.\Var{P}(x)\}$ implies
|
|
1419 |
$\Var{P}(\Var{c})\}$.\index{*CollectD}
|
|
1420 |
\begin{ttbox}
|
|
1421 |
by (dresolve_tac [CollectD] 1);
|
|
1422 |
{\out Level 4}
|
|
1423 |
{\out ~ \{x. ?P7(x)\} : range(f)}
|
|
1424 |
{\out 1. !!x. [| ?c3(x) : f(x); ?P7(?c3(x)) |] ==> False}
|
|
1425 |
{\out 2. !!x. [| ~ ?c3(x) : \{x. ?P7(x)\}; ~ ?c3(x) : f(x) |] ==> False}
|
|
1426 |
\end{ttbox}
|
|
1427 |
Forcing a contradiction between the two assumptions of subgoal~1 completes
|
287
|
1428 |
the instantiation of~$S$. It is now the set $\{x. x\not\in f(x)\}$, the
|
|
1429 |
standard diagonal construction.
|
104
|
1430 |
\begin{ttbox}
|
|
1431 |
by (contr_tac 1);
|
|
1432 |
{\out Level 5}
|
|
1433 |
{\out ~ \{x. ~ x : f(x)\} : range(f)}
|
|
1434 |
{\out 1. !!x. [| ~ x : \{x. ~ x : f(x)\}; ~ x : f(x) |] ==> False}
|
|
1435 |
\end{ttbox}
|
|
1436 |
The rest should be easy. To apply \ttindex{CollectI} to the negated
|
|
1437 |
assumption, we employ \ttindex{swap_res_tac}:
|
|
1438 |
\begin{ttbox}
|
|
1439 |
by (swap_res_tac [CollectI] 1);
|
|
1440 |
{\out Level 6}
|
|
1441 |
{\out ~ \{x. ~ x : f(x)\} : range(f)}
|
|
1442 |
{\out 1. !!x. [| ~ x : f(x); ~ False |] ==> ~ x : f(x)}
|
287
|
1443 |
\ttbreak
|
104
|
1444 |
by (assume_tac 1);
|
|
1445 |
{\out Level 7}
|
|
1446 |
{\out ~ \{x. ~ x : f(x)\} : range(f)}
|
|
1447 |
{\out No subgoals!}
|
|
1448 |
\end{ttbox}
|
|
1449 |
How much creativity is required? As it happens, Isabelle can prove this
|
|
1450 |
theorem automatically. The classical set \ttindex{set_cs} contains rules
|
306
|
1451 |
for most of the constructs of \HOL's set theory. We augment it with
|
104
|
1452 |
\ttindex{equalityCE} --- set equalities are not broken up by default ---
|
|
1453 |
and apply best-first search. Depth-first search would diverge, but
|
|
1454 |
best-first search successfully navigates through the large search space.
|
|
1455 |
\begin{ttbox}
|
|
1456 |
choplev 0;
|
|
1457 |
{\out Level 0}
|
|
1458 |
{\out ~ ?S : range(f)}
|
|
1459 |
{\out 1. ~ ?S : range(f)}
|
287
|
1460 |
\ttbreak
|
104
|
1461 |
by (best_tac (set_cs addSEs [equalityCE]) 1);
|
|
1462 |
{\out Level 1}
|
|
1463 |
{\out ~ \{x. ~ x : f(x)\} : range(f)}
|
|
1464 |
{\out No subgoals!}
|
|
1465 |
\end{ttbox}
|