|
1 \part{Using Isabelle from the ML Top-Level}\label{chap:getting} |
|
2 |
|
3 Most Isabelle users write proof scripts using the Isar language, as described in the \emph{Tutorial}, and debug them through the Proof General user interface~\cite{proofgeneral}. Isabelle's original user interface --- based on the \ML{} top-level --- is still available, however. |
|
4 Proofs are conducted by |
|
5 applying certain \ML{} functions, which update a stored proof state. |
|
6 All syntax can be expressed using plain {\sc ascii} |
|
7 characters, but Isabelle can support |
|
8 alternative syntaxes, for example using mathematical symbols from a |
|
9 special screen font. The meta-logic and main object-logics already |
|
10 provide such fancy output as an option. |
|
11 |
|
12 Object-logics are built upon Pure Isabelle, which implements the |
|
13 meta-logic and provides certain fundamental data structures: types, |
|
14 terms, signatures, theorems and theories, tactics and tacticals. |
|
15 These data structures have the corresponding \ML{} types \texttt{typ}, |
|
16 \texttt{term}, \texttt{Sign.sg}, \texttt{thm}, \texttt{theory} and \texttt{tactic}; |
|
17 tacticals have function types such as \texttt{tactic->tactic}. Isabelle |
|
18 users can operate on these data structures by writing \ML{} programs. |
|
19 |
|
20 |
|
21 \section{Forward proof}\label{sec:forward} \index{forward proof|(} |
|
22 This section describes the concrete syntax for types, terms and theorems, |
|
23 and demonstrates forward proof. The examples are set in first-order logic. |
|
24 The command to start Isabelle running first-order logic is |
|
25 \begin{ttbox} |
|
26 isabelle FOL |
|
27 \end{ttbox} |
|
28 Note that just typing \texttt{isabelle} usually brings up higher-order logic |
|
29 (HOL) by default. |
|
30 |
|
31 |
|
32 \subsection{Lexical matters} |
|
33 \index{identifiers}\index{reserved words} |
|
34 An {\bf identifier} is a string of letters, digits, underscores~(\verb|_|) |
|
35 and single quotes~({\tt'}), beginning with a letter. Single quotes are |
|
36 regarded as primes; for instance \texttt{x'} is read as~$x'$. Identifiers are |
|
37 separated by white space and special characters. {\bf Reserved words} are |
|
38 identifiers that appear in Isabelle syntax definitions. |
|
39 |
|
40 An Isabelle theory can declare symbols composed of special characters, such |
|
41 as {\tt=}, {\tt==}, {\tt=>} and {\tt==>}. (The latter three are part of |
|
42 the syntax of the meta-logic.) Such symbols may be run together; thus if |
|
43 \verb|}| and \verb|{| are used for set brackets then \verb|{{a},{a,b}}| is |
|
44 valid notation for a set of sets --- but only if \verb|}}| and \verb|{{| |
|
45 have not been declared as symbols! The parser resolves any ambiguity by |
|
46 taking the longest possible symbol that has been declared. Thus the string |
|
47 {\tt==>} is read as a single symbol. But \hbox{\tt= =>} is read as two |
|
48 symbols. |
|
49 |
|
50 Identifiers that are not reserved words may serve as free variables or |
|
51 constants. A {\bf type identifier} consists of an identifier prefixed by a |
|
52 prime, for example {\tt'a} and \hbox{\tt'hello}. Type identifiers stand |
|
53 for (free) type variables, which remain fixed during a proof. |
|
54 \index{type identifiers} |
|
55 |
|
56 An {\bf unknown}\index{unknowns} (or type unknown) consists of a question |
|
57 mark, an identifier (or type identifier), and a subscript. The subscript, |
|
58 a non-negative integer, |
|
59 allows the renaming of unknowns prior to unification.% |
|
60 \footnote{The subscript may appear after the identifier, separated by a |
|
61 dot; this prevents ambiguity when the identifier ends with a digit. Thus |
|
62 {\tt?z6.0} has identifier {\tt"z6"} and subscript~0, while {\tt?a0.5} |
|
63 has identifier {\tt"a0"} and subscript~5. If the identifier does not |
|
64 end with a digit, then no dot appears and a subscript of~0 is omitted; |
|
65 for example, {\tt?hello} has identifier {\tt"hello"} and subscript |
|
66 zero, while {\tt?z6} has identifier {\tt"z"} and subscript~6. The same |
|
67 conventions apply to type unknowns. The question mark is {\it not\/} |
|
68 part of the identifier!} |
|
69 |
|
70 |
|
71 \subsection{Syntax of types and terms} |
|
72 \index{classes!built-in|bold}\index{syntax!of types and terms} |
|
73 |
|
74 Classes are denoted by identifiers; the built-in class \cldx{logic} |
|
75 contains the `logical' types. Sorts are lists of classes enclosed in |
|
76 braces~\} and \{; singleton sorts may be abbreviated by dropping the braces. |
|
77 |
|
78 \index{types!syntax of|bold}\index{sort constraints} Types are written |
|
79 with a syntax like \ML's. The built-in type \tydx{prop} is the type |
|
80 of propositions. Type variables can be constrained to particular |
|
81 classes or sorts, for example \texttt{'a::term} and \texttt{?'b::\ttlbrace |
|
82 ord, arith\ttrbrace}. |
|
83 \[\dquotes |
|
84 \index{*:: symbol}\index{*=> symbol} |
|
85 \index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol} |
|
86 \index{*[ symbol}\index{*] symbol} |
|
87 \begin{array}{ll} |
|
88 \multicolumn{2}{c}{\hbox{ASCII Notation for Types}} \\ \hline |
|
89 \alpha "::" C & \hbox{class constraint} \\ |
|
90 \alpha "::" "\ttlbrace" C@1 "," \ldots "," C@n "\ttrbrace" & |
|
91 \hbox{sort constraint} \\ |
|
92 \sigma " => " \tau & \hbox{function type } \sigma\To\tau \\ |
|
93 "[" \sigma@1 "," \ldots "," \sigma@n "] => " \tau |
|
94 & \hbox{$n$-argument function type} \\ |
|
95 "(" \tau@1"," \ldots "," \tau@n ")" tycon & \hbox{type construction} |
|
96 \end{array} |
|
97 \] |
|
98 Terms are those of the typed $\lambda$-calculus. |
|
99 \index{terms!syntax of|bold}\index{type constraints} |
|
100 \[\dquotes |
|
101 \index{%@{\tt\%} symbol}\index{lambda abs@$\lambda$-abstractions} |
|
102 \index{*:: symbol} |
|
103 \begin{array}{ll} |
|
104 \multicolumn{2}{c}{\hbox{ASCII Notation for Terms}} \\ \hline |
|
105 t "::" \sigma & \hbox{type constraint} \\ |
|
106 "\%" x "." t & \hbox{abstraction } \lambda x.t \\ |
|
107 "\%" x@1\ldots x@n "." t & \hbox{abstraction over several arguments} \\ |
|
108 t "(" u@1"," \ldots "," u@n ")" & |
|
109 \hbox{application to several arguments (FOL and ZF)} \\ |
|
110 t\; u@1 \ldots\; u@n & \hbox{application to several arguments (HOL)} |
|
111 \end{array} |
|
112 \] |
|
113 Note that HOL uses its traditional ``higher-order'' syntax for application, |
|
114 which differs from that used in FOL. |
|
115 |
|
116 The theorems and rules of an object-logic are represented by theorems in |
|
117 the meta-logic, which are expressed using meta-formulae. Since the |
|
118 meta-logic is higher-order, meta-formulae~$\phi$, $\psi$, $\theta$,~\ldots{} |
|
119 are just terms of type~\texttt{prop}. |
|
120 \index{meta-implication} |
|
121 \index{meta-quantifiers}\index{meta-equality} |
|
122 \index{*"!"! symbol} |
|
123 |
|
124 \index{["!@{\tt[\char124} symbol} %\char124 is vertical bar. We use ! because | stopped working |
|
125 \index{"!]@{\tt\char124]} symbol} % so these are [| and |] |
|
126 |
|
127 \index{*== symbol}\index{*=?= symbol}\index{*==> symbol} |
|
128 \[\dquotes |
|
129 \begin{array}{l@{\quad}l@{\quad}l} |
|
130 \multicolumn{3}{c}{\hbox{ASCII Notation for Meta-Formulae}} \\ \hline |
|
131 a " == " b & a\equiv b & \hbox{meta-equality} \\ |
|
132 a " =?= " b & a\qeq b & \hbox{flex-flex constraint} \\ |
|
133 \phi " ==> " \psi & \phi\Imp \psi & \hbox{meta-implication} \\ |
|
134 "[|" \phi@1 ";" \ldots ";" \phi@n "|] ==> " \psi & |
|
135 \List{\phi@1;\ldots;\phi@n} \Imp \psi & \hbox{nested implication} \\ |
|
136 "!!" x "." \phi & \Forall x.\phi & \hbox{meta-quantification} \\ |
|
137 "!!" x@1\ldots x@n "." \phi & |
|
138 \Forall x@1. \ldots x@n.\phi & \hbox{nested quantification} |
|
139 \end{array} |
|
140 \] |
|
141 Flex-flex constraints are meta-equalities arising from unification; they |
|
142 require special treatment. See~\S\ref{flexflex}. |
|
143 \index{flex-flex constraints} |
|
144 |
|
145 \index{*Trueprop constant} |
|
146 Most logics define the implicit coercion $Trueprop$ from object-formulae to |
|
147 propositions. This could cause an ambiguity: in $P\Imp Q$, do the |
|
148 variables $P$ and $Q$ stand for meta-formulae or object-formulae? If the |
|
149 latter, $P\Imp Q$ really abbreviates $Trueprop(P)\Imp Trueprop(Q)$. To |
|
150 prevent such ambiguities, Isabelle's syntax does not allow a meta-formula |
|
151 to consist of a variable. Variables of type~\tydx{prop} are seldom |
|
152 useful, but you can make a variable stand for a meta-formula by prefixing |
|
153 it with the symbol \texttt{PROP}:\index{*PROP symbol} |
|
154 \begin{ttbox} |
|
155 PROP ?psi ==> PROP ?theta |
|
156 \end{ttbox} |
|
157 |
|
158 Symbols of object-logics are typically rendered into {\sc ascii} as |
|
159 follows: |
|
160 \[ \begin{tabular}{l@{\quad}l@{\quad}l} |
|
161 \tt True & $\top$ & true \\ |
|
162 \tt False & $\bot$ & false \\ |
|
163 \tt $P$ \& $Q$ & $P\conj Q$ & conjunction \\ |
|
164 \tt $P$ | $Q$ & $P\disj Q$ & disjunction \\ |
|
165 \verb'~' $P$ & $\neg P$ & negation \\ |
|
166 \tt $P$ --> $Q$ & $P\imp Q$ & implication \\ |
|
167 \tt $P$ <-> $Q$ & $P\bimp Q$ & bi-implication \\ |
|
168 \tt ALL $x\,y\,z$ .\ $P$ & $\forall x\,y\,z.P$ & for all \\ |
|
169 \tt EX $x\,y\,z$ .\ $P$ & $\exists x\,y\,z.P$ & there exists |
|
170 \end{tabular} |
|
171 \] |
|
172 To illustrate the notation, consider two axioms for first-order logic: |
|
173 $$ \List{P; Q} \Imp P\conj Q \eqno(\conj I) $$ |
|
174 $$ \List{\exists x. P(x); \Forall x. P(x)\imp Q} \Imp Q \eqno(\exists E) $$ |
|
175 $({\conj}I)$ translates into {\sc ascii} characters as |
|
176 \begin{ttbox} |
|
177 [| ?P; ?Q |] ==> ?P & ?Q |
|
178 \end{ttbox} |
|
179 The schematic variables let unification instantiate the rule. To avoid |
|
180 cluttering logic definitions with question marks, Isabelle converts any |
|
181 free variables in a rule to schematic variables; we normally declare |
|
182 $({\conj}I)$ as |
|
183 \begin{ttbox} |
|
184 [| P; Q |] ==> P & Q |
|
185 \end{ttbox} |
|
186 This variables convention agrees with the treatment of variables in goals. |
|
187 Free variables in a goal remain fixed throughout the proof. After the |
|
188 proof is finished, Isabelle converts them to scheme variables in the |
|
189 resulting theorem. Scheme variables in a goal may be replaced by terms |
|
190 during the proof, supporting answer extraction, program synthesis, and so |
|
191 forth. |
|
192 |
|
193 For a final example, the rule $(\exists E)$ is rendered in {\sc ascii} as |
|
194 \begin{ttbox} |
|
195 [| EX x. P(x); !!x. P(x) ==> Q |] ==> Q |
|
196 \end{ttbox} |
|
197 |
|
198 |
|
199 \subsection{Basic operations on theorems} |
|
200 \index{theorems!basic operations on|bold} |
|
201 \index{LCF system} |
|
202 Meta-level theorems have the \ML{} type \mltydx{thm}. They represent the |
|
203 theorems and inference rules of object-logics. Isabelle's meta-logic is |
|
204 implemented using the {\sc lcf} approach: each meta-level inference rule is |
|
205 represented by a function from theorems to theorems. Object-level rules |
|
206 are taken as axioms. |
|
207 |
|
208 The main theorem printing commands are \texttt{prth}, \texttt{prths} and~{\tt |
|
209 prthq}. Of the other operations on theorems, most useful are \texttt{RS} |
|
210 and \texttt{RSN}, which perform resolution. |
|
211 |
|
212 \index{theorems!printing of} |
|
213 \begin{ttdescription} |
|
214 \item[\ttindex{prth} {\it thm};] |
|
215 pretty-prints {\it thm\/} at the terminal. |
|
216 |
|
217 \item[\ttindex{prths} {\it thms};] |
|
218 pretty-prints {\it thms}, a list of theorems. |
|
219 |
|
220 \item[\ttindex{prthq} {\it thmq};] |
|
221 pretty-prints {\it thmq}, a sequence of theorems; this is useful for |
|
222 inspecting the output of a tactic. |
|
223 |
|
224 \item[$thm1$ RS $thm2$] \index{*RS} |
|
225 resolves the conclusion of $thm1$ with the first premise of~$thm2$. |
|
226 |
|
227 \item[$thm1$ RSN $(i,thm2)$] \index{*RSN} |
|
228 resolves the conclusion of $thm1$ with the $i$th premise of~$thm2$. |
|
229 |
|
230 \item[\ttindex{standard} $thm$] |
|
231 puts $thm$ into a standard format. It also renames schematic variables |
|
232 to have subscript zero, improving readability and reducing subscript |
|
233 growth. |
|
234 \end{ttdescription} |
|
235 The rules of a theory are normally bound to \ML\ identifiers. Suppose we are |
|
236 running an Isabelle session containing theory~FOL, natural deduction |
|
237 first-order logic.\footnote{For a listing of the FOL rules and their \ML{} |
|
238 names, turn to |
|
239 \iflabelundefined{fol-rules}{{\em Isabelle's Object-Logics}}% |
|
240 {page~\pageref{fol-rules}}.} |
|
241 Let us try an example given in~\S\ref{joining}. We |
|
242 first print \tdx{mp}, which is the rule~$({\imp}E)$, then resolve it with |
|
243 itself. |
|
244 \begin{ttbox} |
|
245 prth mp; |
|
246 {\out [| ?P --> ?Q; ?P |] ==> ?Q} |
|
247 {\out val it = "[| ?P --> ?Q; ?P |] ==> ?Q" : thm} |
|
248 prth (mp RS mp); |
|
249 {\out [| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q} |
|
250 {\out val it = "[| ?P1 --> ?P --> ?Q; ?P1; ?P |] ==> ?Q" : thm} |
|
251 \end{ttbox} |
|
252 User input appears in {\footnotesize\tt typewriter characters}, and output |
|
253 appears in{\out slanted typewriter characters}. \ML's response {\out val |
|
254 }~\ldots{} is compiler-dependent and will sometimes be suppressed. This |
|
255 session illustrates two formats for the display of theorems. Isabelle's |
|
256 top-level displays theorems as \ML{} values, enclosed in quotes. Printing |
|
257 commands like \texttt{prth} omit the quotes and the surrounding \texttt{val |
|
258 \ldots :\ thm}. Ignoring their side-effects, the printing commands are |
|
259 identity functions. |
|
260 |
|
261 To contrast \texttt{RS} with \texttt{RSN}, we resolve |
|
262 \tdx{conjunct1}, which stands for~$(\conj E1)$, with~\tdx{mp}. |
|
263 \begin{ttbox} |
|
264 conjunct1 RS mp; |
|
265 {\out val it = "[| (?P --> ?Q) & ?Q1; ?P |] ==> ?Q" : thm} |
|
266 conjunct1 RSN (2,mp); |
|
267 {\out val it = "[| ?P --> ?Q; ?P & ?Q1 |] ==> ?Q" : thm} |
|
268 \end{ttbox} |
|
269 These correspond to the following proofs: |
|
270 \[ \infer[({\imp}E)]{Q}{\infer[({\conj}E1)]{P\imp Q}{(P\imp Q)\conj Q@1} & P} |
|
271 \qquad |
|
272 \infer[({\imp}E)]{Q}{P\imp Q & \infer[({\conj}E1)]{P}{P\conj Q@1}} |
|
273 \] |
|
274 % |
|
275 Rules can be derived by pasting other rules together. Let us join |
|
276 \tdx{spec}, which stands for~$(\forall E)$, with \texttt{mp} and {\tt |
|
277 conjunct1}. In \ML{}, the identifier~\texttt{it} denotes the value just |
|
278 printed. |
|
279 \begin{ttbox} |
|
280 spec; |
|
281 {\out val it = "ALL x. ?P(x) ==> ?P(?x)" : thm} |
|
282 it RS mp; |
|
283 {\out val it = "[| ALL x. ?P3(x) --> ?Q2(x); ?P3(?x1) |] ==>} |
|
284 {\out ?Q2(?x1)" : thm} |
|
285 it RS conjunct1; |
|
286 {\out val it = "[| ALL x. ?P4(x) --> ?P6(x) & ?Q5(x); ?P4(?x2) |] ==>} |
|
287 {\out ?P6(?x2)" : thm} |
|
288 standard it; |
|
289 {\out val it = "[| ALL x. ?P(x) --> ?Pa(x) & ?Q(x); ?P(?x) |] ==>} |
|
290 {\out ?Pa(?x)" : thm} |
|
291 \end{ttbox} |
|
292 By resolving $(\forall E)$ with (${\imp}E)$ and (${\conj}E1)$, we have |
|
293 derived a destruction rule for formulae of the form $\forall x. |
|
294 P(x)\imp(Q(x)\conj R(x))$. Used with destruct-resolution, such specialized |
|
295 rules provide a way of referring to particular assumptions. |
|
296 \index{assumptions!use of} |
|
297 |
|
298 \subsection{*Flex-flex constraints} \label{flexflex} |
|
299 \index{flex-flex constraints|bold}\index{unknowns!function} |
|
300 In higher-order unification, {\bf flex-flex} equations are those where both |
|
301 sides begin with a function unknown, such as $\Var{f}(0)\qeq\Var{g}(0)$. |
|
302 They admit a trivial unifier, here $\Var{f}\equiv \lambda x.\Var{a}$ and |
|
303 $\Var{g}\equiv \lambda y.\Var{a}$, where $\Var{a}$ is a new unknown. They |
|
304 admit many other unifiers, such as $\Var{f} \equiv \lambda x.\Var{g}(0)$ |
|
305 and $\{\Var{f} \equiv \lambda x.x,\, \Var{g} \equiv \lambda x.0\}$. Huet's |
|
306 procedure does not enumerate the unifiers; instead, it retains flex-flex |
|
307 equations as constraints on future unifications. Flex-flex constraints |
|
308 occasionally become attached to a proof state; more frequently, they appear |
|
309 during use of \texttt{RS} and~\texttt{RSN}: |
|
310 \begin{ttbox} |
|
311 refl; |
|
312 {\out val it = "?a = ?a" : thm} |
|
313 exI; |
|
314 {\out val it = "?P(?x) ==> EX x. ?P(x)" : thm} |
|
315 refl RS exI; |
|
316 {\out val it = "EX x. ?a3(x) = ?a2(x)" [.] : thm} |
|
317 \end{ttbox} |
|
318 % |
|
319 The mysterious symbol \texttt{[.]} indicates that the result is subject to |
|
320 a meta-level hypothesis. We can make all such hypotheses visible by setting the |
|
321 \ttindexbold{show_hyps} flag: |
|
322 \begin{ttbox} |
|
323 set show_hyps; |
|
324 {\out val it = true : bool} |
|
325 refl RS exI; |
|
326 {\out val it = "EX x. ?a3(x) = ?a2(x)" ["?a3(?x) =?= ?a2(?x)"] : thm} |
|
327 \end{ttbox} |
|
328 |
|
329 \noindent |
|
330 Renaming variables, this is $\exists x.\Var{f}(x)=\Var{g}(x)$ with |
|
331 the constraint ${\Var{f}(\Var{u})\qeq\Var{g}(\Var{u})}$. Instances |
|
332 satisfying the constraint include $\exists x.\Var{f}(x)=\Var{f}(x)$ and |
|
333 $\exists x.x=\Var{u}$. Calling \ttindex{flexflex_rule} removes all |
|
334 constraints by applying the trivial unifier:\index{*prthq} |
|
335 \begin{ttbox} |
|
336 prthq (flexflex_rule it); |
|
337 {\out EX x. ?a4 = ?a4} |
|
338 \end{ttbox} |
|
339 Isabelle simplifies flex-flex equations to eliminate redundant bound |
|
340 variables. In $\lambda x\,y.\Var{f}(k(y),x) \qeq \lambda x\,y.\Var{g}(y)$, |
|
341 there is no bound occurrence of~$x$ on the right side; thus, there will be |
|
342 none on the left in a common instance of these terms. Choosing a new |
|
343 variable~$\Var{h}$, Isabelle assigns $\Var{f}\equiv \lambda u\,v.?h(u)$, |
|
344 simplifying the left side to $\lambda x\,y.\Var{h}(k(y))$. Dropping $x$ |
|
345 from the equation leaves $\lambda y.\Var{h}(k(y)) \qeq \lambda |
|
346 y.\Var{g}(y)$. By $\eta$-conversion, this simplifies to the assignment |
|
347 $\Var{g}\equiv\lambda y.?h(k(y))$. |
|
348 |
|
349 \begin{warn} |
|
350 \ttindex{RS} and \ttindex{RSN} fail (by raising exception \texttt{THM}) unless |
|
351 the resolution delivers {\bf exactly one} resolvent. For multiple results, |
|
352 use \ttindex{RL} and \ttindex{RLN}, which operate on theorem lists. The |
|
353 following example uses \ttindex{read_instantiate} to create an instance |
|
354 of \tdx{refl} containing no schematic variables. |
|
355 \begin{ttbox} |
|
356 val reflk = read_instantiate [("a","k")] refl; |
|
357 {\out val reflk = "k = k" : thm} |
|
358 \end{ttbox} |
|
359 |
|
360 \noindent |
|
361 A flex-flex constraint is no longer possible; resolution does not find a |
|
362 unique unifier: |
|
363 \begin{ttbox} |
|
364 reflk RS exI; |
|
365 {\out uncaught exception} |
|
366 {\out THM ("RSN: multiple unifiers", 1,} |
|
367 {\out ["k = k", "?P(?x) ==> EX x. ?P(x)"])} |
|
368 \end{ttbox} |
|
369 Using \ttindex{RL} this time, we discover that there are four unifiers, and |
|
370 four resolvents: |
|
371 \begin{ttbox} |
|
372 [reflk] RL [exI]; |
|
373 {\out val it = ["EX x. x = x", "EX x. k = x",} |
|
374 {\out "EX x. x = k", "EX x. k = k"] : thm list} |
|
375 \end{ttbox} |
|
376 \end{warn} |
|
377 |
|
378 \index{forward proof|)} |
|
379 |
|
380 \section{Backward proof} |
|
381 Although \texttt{RS} and \texttt{RSN} are fine for simple forward reasoning, |
|
382 large proofs require tactics. Isabelle provides a suite of commands for |
|
383 conducting a backward proof using tactics. |
|
384 |
|
385 \subsection{The basic tactics} |
|
386 The tactics \texttt{assume_tac}, {\tt |
|
387 resolve_tac}, \texttt{eresolve_tac}, and \texttt{dresolve_tac} suffice for most |
|
388 single-step proofs. Although \texttt{eresolve_tac} and \texttt{dresolve_tac} are |
|
389 not strictly necessary, they simplify proofs involving elimination and |
|
390 destruction rules. All the tactics act on a subgoal designated by a |
|
391 positive integer~$i$, failing if~$i$ is out of range. The resolution |
|
392 tactics try their list of theorems in left-to-right order. |
|
393 |
|
394 \begin{ttdescription} |
|
395 \item[\ttindex{assume_tac} {\it i}] \index{tactics!assumption} |
|
396 is the tactic that attempts to solve subgoal~$i$ by assumption. Proof by |
|
397 assumption is not a trivial step; it can falsify other subgoals by |
|
398 instantiating shared variables. There may be several ways of solving the |
|
399 subgoal by assumption. |
|
400 |
|
401 \item[\ttindex{resolve_tac} {\it thms} {\it i}]\index{tactics!resolution} |
|
402 is the basic resolution tactic, used for most proof steps. The $thms$ |
|
403 represent object-rules, which are resolved against subgoal~$i$ of the |
|
404 proof state. For each rule, resolution forms next states by unifying the |
|
405 conclusion with the subgoal and inserting instantiated premises in its |
|
406 place. A rule can admit many higher-order unifiers. The tactic fails if |
|
407 none of the rules generates next states. |
|
408 |
|
409 \item[\ttindex{eresolve_tac} {\it thms} {\it i}] \index{elim-resolution} |
|
410 performs elim-resolution. Like \texttt{resolve_tac~{\it thms}~{\it i\/}} |
|
411 followed by \texttt{assume_tac~{\it i}}, it applies a rule then solves its |
|
412 first premise by assumption. But \texttt{eresolve_tac} additionally deletes |
|
413 that assumption from any subgoals arising from the resolution. |
|
414 |
|
415 \item[\ttindex{dresolve_tac} {\it thms} {\it i}] |
|
416 \index{forward proof}\index{destruct-resolution} |
|
417 performs destruct-resolution with the~$thms$, as described |
|
418 in~\S\ref{destruct}. It is useful for forward reasoning from the |
|
419 assumptions. |
|
420 \end{ttdescription} |
|
421 |
|
422 \subsection{Commands for backward proof} |
|
423 \index{proofs!commands for} |
|
424 Tactics are normally applied using the subgoal module, which maintains a |
|
425 proof state and manages the proof construction. It allows interactive |
|
426 backtracking through the proof space, going away to prove lemmas, etc.; of |
|
427 its many commands, most important are the following: |
|
428 \begin{ttdescription} |
|
429 \item[\ttindex{Goal} {\it formula}; ] |
|
430 begins a new proof, where the {\it formula\/} is written as an \ML\ string. |
|
431 |
|
432 \item[\ttindex{by} {\it tactic}; ] |
|
433 applies the {\it tactic\/} to the current proof |
|
434 state, raising an exception if the tactic fails. |
|
435 |
|
436 \item[\ttindex{undo}(); ] |
|
437 reverts to the previous proof state. Undo can be repeated but cannot be |
|
438 undone. Do not omit the parentheses; typing {\tt\ \ undo;\ \ } merely |
|
439 causes \ML\ to echo the value of that function. |
|
440 |
|
441 \item[\ttindex{result}();] |
|
442 returns the theorem just proved, in a standard format. It fails if |
|
443 unproved subgoals are left, etc. |
|
444 |
|
445 \item[\ttindex{qed} {\it name};] is the usual way of ending a proof. |
|
446 It gets the theorem using \texttt{result}, stores it in Isabelle's |
|
447 theorem database and binds it to an \ML{} identifier. |
|
448 |
|
449 \end{ttdescription} |
|
450 The commands and tactics given above are cumbersome for interactive use. |
|
451 Although our examples will use the full commands, you may prefer Isabelle's |
|
452 shortcuts: |
|
453 \begin{center} \tt |
|
454 \index{*br} \index{*be} \index{*bd} \index{*ba} |
|
455 \begin{tabular}{l@{\qquad\rm abbreviates\qquad}l} |
|
456 ba {\it i}; & by (assume_tac {\it i}); \\ |
|
457 |
|
458 br {\it thm} {\it i}; & by (resolve_tac [{\it thm}] {\it i}); \\ |
|
459 |
|
460 be {\it thm} {\it i}; & by (eresolve_tac [{\it thm}] {\it i}); \\ |
|
461 |
|
462 bd {\it thm} {\it i}; & by (dresolve_tac [{\it thm}] {\it i}); |
|
463 \end{tabular} |
|
464 \end{center} |
|
465 |
|
466 \subsection{A trivial example in propositional logic} |
|
467 \index{examples!propositional} |
|
468 |
|
469 Directory \texttt{FOL} of the Isabelle distribution defines the theory of |
|
470 first-order logic. Let us try the example from \S\ref{prop-proof}, |
|
471 entering the goal $P\disj P\imp P$ in that theory.\footnote{To run these |
|
472 examples, see the file \texttt{FOL/ex/intro.ML}.} |
|
473 \begin{ttbox} |
|
474 Goal "P|P --> P"; |
|
475 {\out Level 0} |
|
476 {\out P | P --> P} |
|
477 {\out 1. P | P --> P} |
|
478 \end{ttbox}\index{level of a proof} |
|
479 Isabelle responds by printing the initial proof state, which has $P\disj |
|
480 P\imp P$ as the main goal and the only subgoal. The {\bf level} of the |
|
481 state is the number of \texttt{by} commands that have been applied to reach |
|
482 it. We now use \ttindex{resolve_tac} to apply the rule \tdx{impI}, |
|
483 or~$({\imp}I)$, to subgoal~1: |
|
484 \begin{ttbox} |
|
485 by (resolve_tac [impI] 1); |
|
486 {\out Level 1} |
|
487 {\out P | P --> P} |
|
488 {\out 1. P | P ==> P} |
|
489 \end{ttbox} |
|
490 In the new proof state, subgoal~1 is $P$ under the assumption $P\disj P$. |
|
491 (The meta-implication {\tt==>} indicates assumptions.) We apply |
|
492 \tdx{disjE}, or~(${\disj}E)$, to that subgoal: |
|
493 \begin{ttbox} |
|
494 by (resolve_tac [disjE] 1); |
|
495 {\out Level 2} |
|
496 {\out P | P --> P} |
|
497 {\out 1. P | P ==> ?P1 | ?Q1} |
|
498 {\out 2. [| P | P; ?P1 |] ==> P} |
|
499 {\out 3. [| P | P; ?Q1 |] ==> P} |
|
500 \end{ttbox} |
|
501 At Level~2 there are three subgoals, each provable by assumption. We |
|
502 deviate from~\S\ref{prop-proof} by tackling subgoal~3 first, using |
|
503 \ttindex{assume_tac}. This affects subgoal~1, updating {\tt?Q1} to~{\tt |
|
504 P}. |
|
505 \begin{ttbox} |
|
506 by (assume_tac 3); |
|
507 {\out Level 3} |
|
508 {\out P | P --> P} |
|
509 {\out 1. P | P ==> ?P1 | P} |
|
510 {\out 2. [| P | P; ?P1 |] ==> P} |
|
511 \end{ttbox} |
|
512 Next we tackle subgoal~2, instantiating {\tt?P1} to~\texttt{P} in subgoal~1. |
|
513 \begin{ttbox} |
|
514 by (assume_tac 2); |
|
515 {\out Level 4} |
|
516 {\out P | P --> P} |
|
517 {\out 1. P | P ==> P | P} |
|
518 \end{ttbox} |
|
519 Lastly we prove the remaining subgoal by assumption: |
|
520 \begin{ttbox} |
|
521 by (assume_tac 1); |
|
522 {\out Level 5} |
|
523 {\out P | P --> P} |
|
524 {\out No subgoals!} |
|
525 \end{ttbox} |
|
526 Isabelle tells us that there are no longer any subgoals: the proof is |
|
527 complete. Calling \texttt{qed} stores the theorem. |
|
528 \begin{ttbox} |
|
529 qed "mythm"; |
|
530 {\out val mythm = "?P | ?P --> ?P" : thm} |
|
531 \end{ttbox} |
|
532 Isabelle has replaced the free variable~\texttt{P} by the scheme |
|
533 variable~{\tt?P}\@. Free variables in the proof state remain fixed |
|
534 throughout the proof. Isabelle finally converts them to scheme variables |
|
535 so that the resulting theorem can be instantiated with any formula. |
|
536 |
|
537 As an exercise, try doing the proof as in \S\ref{prop-proof}, observing how |
|
538 instantiations affect the proof state. |
|
539 |
|
540 |
|
541 \subsection{Part of a distributive law} |
|
542 \index{examples!propositional} |
|
543 To demonstrate the tactics \ttindex{eresolve_tac}, \ttindex{dresolve_tac} |
|
544 and the tactical \texttt{REPEAT}, let us prove part of the distributive |
|
545 law |
|
546 \[ (P\conj Q)\disj R \,\bimp\, (P\disj R)\conj (Q\disj R). \] |
|
547 We begin by stating the goal to Isabelle and applying~$({\imp}I)$ to it: |
|
548 \begin{ttbox} |
|
549 Goal "(P & Q) | R --> (P | R)"; |
|
550 {\out Level 0} |
|
551 {\out P & Q | R --> P | R} |
|
552 {\out 1. P & Q | R --> P | R} |
|
553 \ttbreak |
|
554 by (resolve_tac [impI] 1); |
|
555 {\out Level 1} |
|
556 {\out P & Q | R --> P | R} |
|
557 {\out 1. P & Q | R ==> P | R} |
|
558 \end{ttbox} |
|
559 Previously we applied~(${\disj}E)$ using \texttt{resolve_tac}, but |
|
560 \ttindex{eresolve_tac} deletes the assumption after use. The resulting proof |
|
561 state is simpler. |
|
562 \begin{ttbox} |
|
563 by (eresolve_tac [disjE] 1); |
|
564 {\out Level 2} |
|
565 {\out P & Q | R --> P | R} |
|
566 {\out 1. P & Q ==> P | R} |
|
567 {\out 2. R ==> P | R} |
|
568 \end{ttbox} |
|
569 Using \ttindex{dresolve_tac}, we can apply~(${\conj}E1)$ to subgoal~1, |
|
570 replacing the assumption $P\conj Q$ by~$P$. Normally we should apply the |
|
571 rule~(${\conj}E)$, given in~\S\ref{destruct}. That is an elimination rule |
|
572 and requires \texttt{eresolve_tac}; it would replace $P\conj Q$ by the two |
|
573 assumptions~$P$ and~$Q$. Because the present example does not need~$Q$, we |
|
574 may try out \texttt{dresolve_tac}. |
|
575 \begin{ttbox} |
|
576 by (dresolve_tac [conjunct1] 1); |
|
577 {\out Level 3} |
|
578 {\out P & Q | R --> P | R} |
|
579 {\out 1. P ==> P | R} |
|
580 {\out 2. R ==> P | R} |
|
581 \end{ttbox} |
|
582 The next two steps apply~(${\disj}I1$) and~(${\disj}I2$) in an obvious manner. |
|
583 \begin{ttbox} |
|
584 by (resolve_tac [disjI1] 1); |
|
585 {\out Level 4} |
|
586 {\out P & Q | R --> P | R} |
|
587 {\out 1. P ==> P} |
|
588 {\out 2. R ==> P | R} |
|
589 \ttbreak |
|
590 by (resolve_tac [disjI2] 2); |
|
591 {\out Level 5} |
|
592 {\out P & Q | R --> P | R} |
|
593 {\out 1. P ==> P} |
|
594 {\out 2. R ==> R} |
|
595 \end{ttbox} |
|
596 Two calls of \texttt{assume_tac} can finish the proof. The |
|
597 tactical~\ttindex{REPEAT} here expresses a tactic that calls \texttt{assume_tac~1} |
|
598 as many times as possible. We can restrict attention to subgoal~1 because |
|
599 the other subgoals move up after subgoal~1 disappears. |
|
600 \begin{ttbox} |
|
601 by (REPEAT (assume_tac 1)); |
|
602 {\out Level 6} |
|
603 {\out P & Q | R --> P | R} |
|
604 {\out No subgoals!} |
|
605 \end{ttbox} |
|
606 |
|
607 |
|
608 \section{Quantifier reasoning} |
|
609 \index{quantifiers}\index{parameters}\index{unknowns}\index{unknowns!function} |
|
610 This section illustrates how Isabelle enforces quantifier provisos. |
|
611 Suppose that $x$, $y$ and~$z$ are parameters of a subgoal. Quantifier |
|
612 rules create terms such as~$\Var{f}(x,z)$, where~$\Var{f}$ is a function |
|
613 unknown. Instantiating $\Var{f}$ to $\lambda x\,z.t$ has the effect of |
|
614 replacing~$\Var{f}(x,z)$ by~$t$, where the term~$t$ may contain free |
|
615 occurrences of~$x$ and~$z$. On the other hand, no instantiation |
|
616 of~$\Var{f}$ can replace~$\Var{f}(x,z)$ by a term containing free |
|
617 occurrences of~$y$, since parameters are bound variables. |
|
618 |
|
619 \subsection{Two quantifier proofs: a success and a failure} |
|
620 \index{examples!with quantifiers} |
|
621 Let us contrast a proof of the theorem $\forall x.\exists y.x=y$ with an |
|
622 attempted proof of the non-theorem $\exists y.\forall x.x=y$. The former |
|
623 proof succeeds, and the latter fails, because of the scope of quantified |
|
624 variables~\cite{paulson-found}. Unification helps even in these trivial |
|
625 proofs. In $\forall x.\exists y.x=y$ the $y$ that `exists' is simply $x$, |
|
626 but we need never say so. This choice is forced by the reflexive law for |
|
627 equality, and happens automatically. |
|
628 |
|
629 \paragraph{The successful proof.} |
|
630 The proof of $\forall x.\exists y.x=y$ demonstrates the introduction rules |
|
631 $(\forall I)$ and~$(\exists I)$. We state the goal and apply $(\forall I)$: |
|
632 \begin{ttbox} |
|
633 Goal "ALL x. EX y. x=y"; |
|
634 {\out Level 0} |
|
635 {\out ALL x. EX y. x = y} |
|
636 {\out 1. ALL x. EX y. x = y} |
|
637 \ttbreak |
|
638 by (resolve_tac [allI] 1); |
|
639 {\out Level 1} |
|
640 {\out ALL x. EX y. x = y} |
|
641 {\out 1. !!x. EX y. x = y} |
|
642 \end{ttbox} |
|
643 The variable~\texttt{x} is no longer universally quantified, but is a |
|
644 parameter in the subgoal; thus, it is universally quantified at the |
|
645 meta-level. The subgoal must be proved for all possible values of~\texttt{x}. |
|
646 |
|
647 To remove the existential quantifier, we apply the rule $(\exists I)$: |
|
648 \begin{ttbox} |
|
649 by (resolve_tac [exI] 1); |
|
650 {\out Level 2} |
|
651 {\out ALL x. EX y. x = y} |
|
652 {\out 1. !!x. x = ?y1(x)} |
|
653 \end{ttbox} |
|
654 The bound variable \texttt{y} has become {\tt?y1(x)}. This term consists of |
|
655 the function unknown~{\tt?y1} applied to the parameter~\texttt{x}. |
|
656 Instances of {\tt?y1(x)} may or may not contain~\texttt{x}. We resolve the |
|
657 subgoal with the reflexivity axiom. |
|
658 \begin{ttbox} |
|
659 by (resolve_tac [refl] 1); |
|
660 {\out Level 3} |
|
661 {\out ALL x. EX y. x = y} |
|
662 {\out No subgoals!} |
|
663 \end{ttbox} |
|
664 Let us consider what has happened in detail. The reflexivity axiom is |
|
665 lifted over~$x$ to become $\Forall x.\Var{f}(x)=\Var{f}(x)$, which is |
|
666 unified with $\Forall x.x=\Var{y@1}(x)$. The function unknowns $\Var{f}$ |
|
667 and~$\Var{y@1}$ are both instantiated to the identity function, and |
|
668 $x=\Var{y@1}(x)$ collapses to~$x=x$ by $\beta$-reduction. |
|
669 |
|
670 \paragraph{The unsuccessful proof.} |
|
671 We state the goal $\exists y.\forall x.x=y$, which is not a theorem, and |
|
672 try~$(\exists I)$: |
|
673 \begin{ttbox} |
|
674 Goal "EX y. ALL x. x=y"; |
|
675 {\out Level 0} |
|
676 {\out EX y. ALL x. x = y} |
|
677 {\out 1. EX y. ALL x. x = y} |
|
678 \ttbreak |
|
679 by (resolve_tac [exI] 1); |
|
680 {\out Level 1} |
|
681 {\out EX y. ALL x. x = y} |
|
682 {\out 1. ALL x. x = ?y} |
|
683 \end{ttbox} |
|
684 The unknown \texttt{?y} may be replaced by any term, but this can never |
|
685 introduce another bound occurrence of~\texttt{x}. We now apply~$(\forall I)$: |
|
686 \begin{ttbox} |
|
687 by (resolve_tac [allI] 1); |
|
688 {\out Level 2} |
|
689 {\out EX y. ALL x. x = y} |
|
690 {\out 1. !!x. x = ?y} |
|
691 \end{ttbox} |
|
692 Compare our position with the previous Level~2. Instead of {\tt?y1(x)} we |
|
693 have~{\tt?y}, whose instances may not contain the bound variable~\texttt{x}. |
|
694 The reflexivity axiom does not unify with subgoal~1. |
|
695 \begin{ttbox} |
|
696 by (resolve_tac [refl] 1); |
|
697 {\out by: tactic failed} |
|
698 \end{ttbox} |
|
699 There can be no proof of $\exists y.\forall x.x=y$ by the soundness of |
|
700 first-order logic. I have elsewhere proved the faithfulness of Isabelle's |
|
701 encoding of first-order logic~\cite{paulson-found}; there could, of course, be |
|
702 faults in the implementation. |
|
703 |
|
704 |
|
705 \subsection{Nested quantifiers} |
|
706 \index{examples!with quantifiers} |
|
707 Multiple quantifiers create complex terms. Proving |
|
708 \[ (\forall x\,y.P(x,y)) \imp (\forall z\,w.P(w,z)) \] |
|
709 will demonstrate how parameters and unknowns develop. If they appear in |
|
710 the wrong order, the proof will fail. |
|
711 |
|
712 This section concludes with a demonstration of \texttt{REPEAT} |
|
713 and~\texttt{ORELSE}. |
|
714 \begin{ttbox} |
|
715 Goal "(ALL x y.P(x,y)) --> (ALL z w.P(w,z))"; |
|
716 {\out Level 0} |
|
717 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} |
|
718 {\out 1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} |
|
719 \ttbreak |
|
720 by (resolve_tac [impI] 1); |
|
721 {\out Level 1} |
|
722 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} |
|
723 {\out 1. ALL x y. P(x,y) ==> ALL z w. P(w,z)} |
|
724 \end{ttbox} |
|
725 |
|
726 \paragraph{The wrong approach.} |
|
727 Using \texttt{dresolve_tac}, we apply the rule $(\forall E)$, bound to the |
|
728 \ML\ identifier \tdx{spec}. Then we apply $(\forall I)$. |
|
729 \begin{ttbox} |
|
730 by (dresolve_tac [spec] 1); |
|
731 {\out Level 2} |
|
732 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} |
|
733 {\out 1. ALL y. P(?x1,y) ==> ALL z w. P(w,z)} |
|
734 \ttbreak |
|
735 by (resolve_tac [allI] 1); |
|
736 {\out Level 3} |
|
737 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} |
|
738 {\out 1. !!z. ALL y. P(?x1,y) ==> ALL w. P(w,z)} |
|
739 \end{ttbox} |
|
740 The unknown \texttt{?x1} and the parameter \texttt{z} have appeared. We again |
|
741 apply $(\forall E)$ and~$(\forall I)$. |
|
742 \begin{ttbox} |
|
743 by (dresolve_tac [spec] 1); |
|
744 {\out Level 4} |
|
745 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} |
|
746 {\out 1. !!z. P(?x1,?y3(z)) ==> ALL w. P(w,z)} |
|
747 \ttbreak |
|
748 by (resolve_tac [allI] 1); |
|
749 {\out Level 5} |
|
750 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} |
|
751 {\out 1. !!z w. P(?x1,?y3(z)) ==> P(w,z)} |
|
752 \end{ttbox} |
|
753 The unknown \texttt{?y3} and the parameter \texttt{w} have appeared. Each |
|
754 unknown is applied to the parameters existing at the time of its creation; |
|
755 instances of~\texttt{?x1} cannot contain~\texttt{z} or~\texttt{w}, while instances |
|
756 of {\tt?y3(z)} can only contain~\texttt{z}. Due to the restriction on~\texttt{?x1}, |
|
757 proof by assumption will fail. |
|
758 \begin{ttbox} |
|
759 by (assume_tac 1); |
|
760 {\out by: tactic failed} |
|
761 {\out uncaught exception ERROR} |
|
762 \end{ttbox} |
|
763 |
|
764 \paragraph{The right approach.} |
|
765 To do this proof, the rules must be applied in the correct order. |
|
766 Parameters should be created before unknowns. The |
|
767 \ttindex{choplev} command returns to an earlier stage of the proof; |
|
768 let us return to the result of applying~$({\imp}I)$: |
|
769 \begin{ttbox} |
|
770 choplev 1; |
|
771 {\out Level 1} |
|
772 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} |
|
773 {\out 1. ALL x y. P(x,y) ==> ALL z w. P(w,z)} |
|
774 \end{ttbox} |
|
775 Previously we made the mistake of applying $(\forall E)$ before $(\forall I)$. |
|
776 \begin{ttbox} |
|
777 by (resolve_tac [allI] 1); |
|
778 {\out Level 2} |
|
779 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} |
|
780 {\out 1. !!z. ALL x y. P(x,y) ==> ALL w. P(w,z)} |
|
781 \ttbreak |
|
782 by (resolve_tac [allI] 1); |
|
783 {\out Level 3} |
|
784 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} |
|
785 {\out 1. !!z w. ALL x y. P(x,y) ==> P(w,z)} |
|
786 \end{ttbox} |
|
787 The parameters \texttt{z} and~\texttt{w} have appeared. We now create the |
|
788 unknowns: |
|
789 \begin{ttbox} |
|
790 by (dresolve_tac [spec] 1); |
|
791 {\out Level 4} |
|
792 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} |
|
793 {\out 1. !!z w. ALL y. P(?x3(z,w),y) ==> P(w,z)} |
|
794 \ttbreak |
|
795 by (dresolve_tac [spec] 1); |
|
796 {\out Level 5} |
|
797 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} |
|
798 {\out 1. !!z w. P(?x3(z,w),?y4(z,w)) ==> P(w,z)} |
|
799 \end{ttbox} |
|
800 Both {\tt?x3(z,w)} and~{\tt?y4(z,w)} could become any terms containing {\tt |
|
801 z} and~\texttt{w}: |
|
802 \begin{ttbox} |
|
803 by (assume_tac 1); |
|
804 {\out Level 6} |
|
805 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} |
|
806 {\out No subgoals!} |
|
807 \end{ttbox} |
|
808 |
|
809 \paragraph{A one-step proof using tacticals.} |
|
810 \index{tacticals} \index{examples!of tacticals} |
|
811 |
|
812 Repeated application of rules can be effective, but the rules should be |
|
813 attempted in the correct order. Let us return to the original goal using |
|
814 \ttindex{choplev}: |
|
815 \begin{ttbox} |
|
816 choplev 0; |
|
817 {\out Level 0} |
|
818 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} |
|
819 {\out 1. (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} |
|
820 \end{ttbox} |
|
821 As we have just seen, \tdx{allI} should be attempted |
|
822 before~\tdx{spec}, while \ttindex{assume_tac} generally can be |
|
823 attempted first. Such priorities can easily be expressed |
|
824 using~\ttindex{ORELSE}, and repeated using~\ttindex{REPEAT}. |
|
825 \begin{ttbox} |
|
826 by (REPEAT (assume_tac 1 ORELSE resolve_tac [impI,allI] 1 |
|
827 ORELSE dresolve_tac [spec] 1)); |
|
828 {\out Level 1} |
|
829 {\out (ALL x y. P(x,y)) --> (ALL z w. P(w,z))} |
|
830 {\out No subgoals!} |
|
831 \end{ttbox} |
|
832 |
|
833 |
|
834 \subsection{A realistic quantifier proof} |
|
835 \index{examples!with quantifiers} |
|
836 To see the practical use of parameters and unknowns, let us prove half of |
|
837 the equivalence |
|
838 \[ (\forall x. P(x) \imp Q) \,\bimp\, ((\exists x. P(x)) \imp Q). \] |
|
839 We state the left-to-right half to Isabelle in the normal way. |
|
840 Since $\imp$ is nested to the right, $({\imp}I)$ can be applied twice; we |
|
841 use \texttt{REPEAT}: |
|
842 \begin{ttbox} |
|
843 Goal "(ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q"; |
|
844 {\out Level 0} |
|
845 {\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} |
|
846 {\out 1. (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} |
|
847 \ttbreak |
|
848 by (REPEAT (resolve_tac [impI] 1)); |
|
849 {\out Level 1} |
|
850 {\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} |
|
851 {\out 1. [| ALL x. P(x) --> Q; EX x. P(x) |] ==> Q} |
|
852 \end{ttbox} |
|
853 We can eliminate the universal or the existential quantifier. The |
|
854 existential quantifier should be eliminated first, since this creates a |
|
855 parameter. The rule~$(\exists E)$ is bound to the |
|
856 identifier~\tdx{exE}. |
|
857 \begin{ttbox} |
|
858 by (eresolve_tac [exE] 1); |
|
859 {\out Level 2} |
|
860 {\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} |
|
861 {\out 1. !!x. [| ALL x. P(x) --> Q; P(x) |] ==> Q} |
|
862 \end{ttbox} |
|
863 The only possibility now is $(\forall E)$, a destruction rule. We use |
|
864 \ttindex{dresolve_tac}, which discards the quantified assumption; it is |
|
865 only needed once. |
|
866 \begin{ttbox} |
|
867 by (dresolve_tac [spec] 1); |
|
868 {\out Level 3} |
|
869 {\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} |
|
870 {\out 1. !!x. [| P(x); P(?x3(x)) --> Q |] ==> Q} |
|
871 \end{ttbox} |
|
872 Because we applied $(\exists E)$ before $(\forall E)$, the unknown |
|
873 term~{\tt?x3(x)} may depend upon the parameter~\texttt{x}. |
|
874 |
|
875 Although $({\imp}E)$ is a destruction rule, it works with |
|
876 \ttindex{eresolve_tac} to perform backward chaining. This technique is |
|
877 frequently useful. |
|
878 \begin{ttbox} |
|
879 by (eresolve_tac [mp] 1); |
|
880 {\out Level 4} |
|
881 {\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} |
|
882 {\out 1. !!x. P(x) ==> P(?x3(x))} |
|
883 \end{ttbox} |
|
884 The tactic has reduced~\texttt{Q} to~\texttt{P(?x3(x))}, deleting the |
|
885 implication. The final step is trivial, thanks to the occurrence of~\texttt{x}. |
|
886 \begin{ttbox} |
|
887 by (assume_tac 1); |
|
888 {\out Level 5} |
|
889 {\out (ALL x. P(x) --> Q) --> (EX x. P(x)) --> Q} |
|
890 {\out No subgoals!} |
|
891 \end{ttbox} |
|
892 |
|
893 |
|
894 \subsection{The classical reasoner} |
|
895 \index{classical reasoner} |
|
896 Isabelle provides enough automation to tackle substantial examples. |
|
897 The classical |
|
898 reasoner can be set up for any classical natural deduction logic; |
|
899 see \iflabelundefined{chap:classical}{the {\em Reference Manual\/}}% |
|
900 {Chap.\ts\ref{chap:classical}}. |
|
901 It cannot compete with fully automatic theorem provers, but it is |
|
902 competitive with tools found in other interactive provers. |
|
903 |
|
904 Rules are packaged into {\bf classical sets}. The classical reasoner |
|
905 provides several tactics, which apply rules using naive algorithms. |
|
906 Unification handles quantifiers as shown above. The most useful tactic |
|
907 is~\ttindex{Blast_tac}. |
|
908 |
|
909 Let us solve problems~40 and~60 of Pelletier~\cite{pelletier86}. (The |
|
910 backslashes~\hbox{\verb|\|\ldots\verb|\|} are an \ML{} string escape |
|
911 sequence, to break the long string over two lines.) |
|
912 \begin{ttbox} |
|
913 Goal "(EX y. ALL x. J(y,x) <-> ~J(x,x)) \ttback |
|
914 \ttback --> ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"; |
|
915 {\out Level 0} |
|
916 {\out (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->} |
|
917 {\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))} |
|
918 {\out 1. (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->} |
|
919 {\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))} |
|
920 \end{ttbox} |
|
921 \ttindex{Blast_tac} proves subgoal~1 at a stroke. |
|
922 \begin{ttbox} |
|
923 by (Blast_tac 1); |
|
924 {\out Depth = 0} |
|
925 {\out Depth = 1} |
|
926 {\out Level 1} |
|
927 {\out (EX y. ALL x. J(y,x) <-> ~J(x,x)) -->} |
|
928 {\out ~(ALL x. EX y. ALL z. J(z,y) <-> ~J(z,x))} |
|
929 {\out No subgoals!} |
|
930 \end{ttbox} |
|
931 Sceptics may examine the proof by calling the package's single-step |
|
932 tactics, such as~\texttt{step_tac}. This would take up much space, however, |
|
933 so let us proceed to the next example: |
|
934 \begin{ttbox} |
|
935 Goal "ALL x. P(x,f(x)) <-> \ttback |
|
936 \ttback (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"; |
|
937 {\out Level 0} |
|
938 {\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))} |
|
939 {\out 1. ALL x. P(x,f(x)) <->} |
|
940 {\out (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))} |
|
941 \end{ttbox} |
|
942 Again, subgoal~1 succumbs immediately. |
|
943 \begin{ttbox} |
|
944 by (Blast_tac 1); |
|
945 {\out Depth = 0} |
|
946 {\out Depth = 1} |
|
947 {\out Level 1} |
|
948 {\out ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))} |
|
949 {\out No subgoals!} |
|
950 \end{ttbox} |
|
951 The classical reasoner is not restricted to the usual logical connectives. |
|
952 The natural deduction rules for unions and intersections resemble those for |
|
953 disjunction and conjunction. The rules for infinite unions and |
|
954 intersections resemble those for quantifiers. Given such rules, the classical |
|
955 reasoner is effective for reasoning in set theory. |
|
956 |