|
1 %% $Id$ |
|
2 \part{Foundations} |
|
3 This Part presents Isabelle's logical foundations in detail: |
|
4 representing logical syntax in the typed $\lambda$-calculus; expressing |
|
5 inference rules in Isabelle's meta-logic; combining rules by resolution. |
|
6 Readers wishing to use Isabelle immediately may prefer to skip straight to |
|
7 Part~II, using this Part (via the index) for reference only. |
|
8 |
|
9 \begin{figure} |
|
10 \begin{eqnarray*} |
|
11 \neg P & \hbox{abbreviates} & P\imp\bot \\ |
|
12 P\bimp Q & \hbox{abbreviates} & (P\imp Q) \conj (Q\imp P) |
|
13 \end{eqnarray*} |
|
14 \vskip 4ex |
|
15 |
|
16 \(\begin{array}{c@{\qquad\qquad}c} |
|
17 \infer[({\conj}I)]{P\conj Q}{P & Q} & |
|
18 \infer[({\conj}E1)]{P}{P\conj Q} \qquad |
|
19 \infer[({\conj}E2)]{Q}{P\conj Q} \\[4ex] |
|
20 |
|
21 \infer[({\disj}I1)]{P\disj Q}{P} \qquad |
|
22 \infer[({\disj}I2)]{P\disj Q}{Q} & |
|
23 \infer[({\disj}E)]{R}{P\disj Q & \infer*{R}{[P]} & \infer*{R}{[Q]}}\\[4ex] |
|
24 |
|
25 \infer[({\imp}I)]{P\imp Q}{\infer*{Q}{[P]}} & |
|
26 \infer[({\imp}E)]{Q}{P\imp Q & P} \\[4ex] |
|
27 |
|
28 & |
|
29 \infer[({\bot}E)]{P}{\bot}\\[4ex] |
|
30 |
|
31 \infer[({\forall}I)*]{\forall x.P}{P} & |
|
32 \infer[({\forall}E)]{P[t/x]}{\forall x.P} \\[3ex] |
|
33 |
|
34 \infer[({\exists}I)]{\exists x.P}{P[t/x]} & |
|
35 \infer[({\exists}E)*]{Q}{{\exists x.P} & \infer*{Q}{[P]} } \\[3ex] |
|
36 |
|
37 {t=t} \,(refl) & \vcenter{\infer[(subst)]{P[u/x]}{t=u & P[t/x]}} |
|
38 \end{array} \) |
|
39 |
|
40 \bigskip\bigskip |
|
41 *{\em Eigenvariable conditions\/}: |
|
42 |
|
43 $\forall I$: provided $x$ is not free in the assumptions |
|
44 |
|
45 $\exists E$: provided $x$ is not free in $Q$ or any assumption except $P$ |
|
46 \caption{Intuitionistic first-order logic} \label{fol-fig} |
|
47 \end{figure} |
|
48 |
|
49 \section{Formalizing logical syntax in Isabelle} |
|
50 \index{Isabelle!formalizing syntax|bold} |
|
51 Figure~\ref{fol-fig} presents intuitionistic first-order logic, |
|
52 including equality and the natural numbers. Let us see how to formalize |
|
53 this logic in Isabelle, illustrating the main features of Isabelle's |
|
54 polymorphic meta-logic. |
|
55 |
|
56 Isabelle represents syntax using the typed $\lambda$-calculus. We declare |
|
57 a type for each syntactic category of the logic. We declare a constant for |
|
58 each symbol of the logic, giving each $n$-ary operation an $n$-argument |
|
59 curried function type. Most importantly, $\lambda$-abstraction represents |
|
60 variable binding in quantifiers. |
|
61 |
|
62 \index{$\To$|bold}\index{types} |
|
63 Isabelle has \ML-style type constructors such as~$(\alpha)list$, where |
|
64 $(bool)list$ is the type of lists of booleans. Function types have the |
|
65 form $\sigma\To\tau$, where $\sigma$ and $\tau$ are types. Functions |
|
66 taking $n$~arguments require curried function types; we may abbreviate |
|
67 \[ \sigma@1\To (\cdots \sigma@n\To \tau\cdots) \quad \hbox{as} \quad |
|
68 [\sigma@1, \ldots, \sigma@n] \To \tau. $$ |
|
69 |
|
70 The syntax for terms is summarised below. Note that function application is |
|
71 written $t(u)$ rather than the usual $t\,u$. |
|
72 \[ |
|
73 \begin{array}{ll} |
|
74 t :: \sigma & \hbox{type constraint, on a term or variable} \\ |
|
75 \lambda x.t & \hbox{abstraction} \\ |
|
76 \lambda x@1\ldots x@n.t |
|
77 & \hbox{curried abstraction, $\lambda x@1. \ldots \lambda x@n.t$} \\ |
|
78 t(u) & \hbox{application} \\ |
|
79 t (u@1, \ldots, u@n) & \hbox{curried application, $t(u@1)\ldots(u@n)$} |
|
80 \end{array} |
|
81 \] |
|
82 |
|
83 |
|
84 \subsection{Simple types and constants} |
|
85 \index{types!simple|bold} |
|
86 The syntactic categories of our logic (Figure~\ref{fol-fig}) are |
|
87 {\bf formulae} and {\bf terms}. Formulae denote truth |
|
88 values, so (following logical tradition) we call their type~$o$. Terms can |
|
89 be constructed using~0 and~$Suc$, requiring a type~$nat$ of natural |
|
90 numbers. Later, we shall see how to admit terms of other types. |
|
91 |
|
92 After declaring the types~$o$ and~$nat$, we may declare constants for the |
|
93 symbols of our logic. Since $\bot$ denotes a truth value (falsity) and 0 |
|
94 denotes a number, we put \begin{eqnarray*} |
|
95 \bot & :: & o \\ |
|
96 0 & :: & nat. |
|
97 \end{eqnarray*} |
|
98 If a symbol requires operands, the corresponding constant must have a |
|
99 function type. In our logic, the successor function |
|
100 ($Suc$) is from natural numbers to natural numbers, negation ($\neg$) is a |
|
101 function from truth values to truth values, and the binary connectives are |
|
102 curried functions taking two truth values as arguments: |
|
103 \begin{eqnarray*} |
|
104 Suc & :: & nat\To nat \\ |
|
105 {\neg} & :: & o\To o \\ |
|
106 \conj,\disj,\imp,\bimp & :: & [o,o]\To o |
|
107 \end{eqnarray*} |
|
108 |
|
109 Isabelle allows us to declare the binary connectives as infixes, with |
|
110 appropriate precedences, so that we write $P\conj Q\disj R$ instead of |
|
111 $\disj(\conj(P,Q), R)$. |
|
112 |
|
113 |
|
114 \subsection{Polymorphic types and constants} \label{polymorphic} |
|
115 \index{types!polymorphic|bold} |
|
116 Which type should we assign to the equality symbol? If we tried |
|
117 $[nat,nat]\To o$, then equality would be restricted to the natural |
|
118 numbers; we would have to declare different equality symbols for each |
|
119 type. Isabelle's type system is polymorphic, so we could declare |
|
120 \begin{eqnarray*} |
|
121 {=} & :: & [\alpha,\alpha]\To o. |
|
122 \end{eqnarray*} |
|
123 But this is also wrong. The declaration is too polymorphic; $\alpha$ |
|
124 ranges over all types, including~$o$ and $nat\To nat$. Thus, it admits |
|
125 $\bot=\neg(\bot)$ and $Suc=Suc$ as formulae, which is acceptable in |
|
126 higher-order logic but not in first-order logic. |
|
127 |
|
128 Isabelle's \bfindex{classes} control polymorphism. Each type variable |
|
129 belongs to a class, which denotes a set of types. Classes are partially |
|
130 ordered by the subclass relation, which is essentially the subset relation |
|
131 on the sets of types. They closely resemble the classes of the functional |
|
132 language Haskell~\cite{haskell-tutorial,haskell-report}. Nipkow and |
|
133 Prehofer discuss type inference for type classes~\cite{nipkow-prehofer}. |
|
134 |
|
135 Isabelle provides the built-in class $logic$, which consists of the logical |
|
136 types: the ones we want to reason about. Let us declare a class $term$, to |
|
137 consist of all legal types of terms in our logic. The subclass structure |
|
138 is now $term\le logic$. |
|
139 |
|
140 We declare $nat$ to be in class $term$. Type variables of class~$term$ |
|
141 should resemble Standard~\ML's equality type variables, which range over |
|
142 those types that possess an equality test. Thus, we declare the equality |
|
143 constant by |
|
144 \begin{eqnarray*} |
|
145 {=} & :: & [\alpha{::}term,\alpha]\To o |
|
146 \end{eqnarray*} |
|
147 We give function types and~$o$ the class $logic$ rather than~$term$, since |
|
148 they are not legal types for terms. We may introduce new types of class |
|
149 $term$ --- for instance, type $string$ or $real$ --- at any time. We can |
|
150 even declare type constructors such as $(\alpha)list$, and state that type |
|
151 $(\sigma)list$ belongs to class~$term$ provided $\sigma$ does; equality |
|
152 applies to lists of natural numbers but not to lists of formulae. We may |
|
153 summarize this paragraph by a set of {\bf arity declarations} for type |
|
154 constructors: |
|
155 \index{$\To$|bold}\index{arities!declaring} |
|
156 \begin{eqnarray*} |
|
157 o & :: & logic \\ |
|
158 {\To} & :: & (logic,logic)logic \\ |
|
159 nat, string, real & :: & term \\ |
|
160 list & :: & (term)term |
|
161 \end{eqnarray*} |
|
162 Higher-order logic, where equality does apply to truth values and |
|
163 functions, would require different arity declarations, namely ${o::term}$ |
|
164 and ${{\To}::(term,term)term}$. The class system can also handle |
|
165 overloading.\index{overloading|bold} We could declare $arith$ to be the |
|
166 subclass of $term$ consisting of the `arithmetic' types, such as~$nat$. |
|
167 Then we could declare the operators |
|
168 \begin{eqnarray*} |
|
169 {+},{-},{\times},{/} & :: & [\alpha{::}arith,\alpha]\To \alpha |
|
170 \end{eqnarray*} |
|
171 If we declare new types $real$ and $complex$ of class $arith$, then we |
|
172 effectively have three sets of operators: |
|
173 \begin{eqnarray*} |
|
174 {+},{-},{\times},{/} & :: & [nat,nat]\To nat \\ |
|
175 {+},{-},{\times},{/} & :: & [real,real]\To real \\ |
|
176 {+},{-},{\times},{/} & :: & [complex,complex]\To complex |
|
177 \end{eqnarray*} |
|
178 Isabelle will regard these as distinct constants, each of which can be defined |
|
179 separately. We could even introduce the type $(\alpha)vector$, make |
|
180 $(\sigma)vector$ belong to $arith$ provided $\sigma$ is in $arith$, and define |
|
181 \begin{eqnarray*} |
|
182 {+} & :: & [(\sigma)vector,(\sigma)vector]\To (\sigma)vector |
|
183 \end{eqnarray*} |
|
184 in terms of ${+} :: [\sigma,\sigma]\To \sigma$. |
|
185 |
|
186 Although we have pretended so far that a type variable belongs to only one |
|
187 class --- Isabelle's concrete syntax helps to uphold this illusion --- it |
|
188 may in fact belong to any finite number of classes. For example suppose |
|
189 that we had declared yet another class $ord \le term$, the class of all |
|
190 `ordered' types, and a constant |
|
191 \begin{eqnarray*} |
|
192 {\le} & :: & [\alpha{::}ord,\alpha]\To o. |
|
193 \end{eqnarray*} |
|
194 In this context the variable $x$ in $x \le (x+x)$ will be assigned type |
|
195 $\alpha{::}\{arith,ord\}$, i.e.\ $\alpha$ belongs to both $arith$ and $ord$. |
|
196 Semantically the set $\{arith,ord\}$ should be understood |
|
197 as the intersection of the sets of types represented by $arith$ and $ord$. |
|
198 Such intersections of classes are called \bfindex{sorts}. The empty |
|
199 intersection of classes, $\{\}$, contains all types and is thus the |
|
200 {\bf universal sort}. |
|
201 |
|
202 The type checker handles overloading, assigning each term a unique type. For |
|
203 this to be possible, the class and type declarations must satisfy certain |
|
204 technical constraints~\cite{nipkow-prehofer}. |
|
205 |
|
206 \subsection{Higher types and quantifiers} |
|
207 \index{types!higher|bold} |
|
208 Quantifiers are regarded as operations upon functions. Ignoring polymorphism |
|
209 for the moment, consider the formula $\forall x. P(x)$, where $x$ ranges |
|
210 over type~$nat$. This is true if $P(x)$ is true for all~$x$. Abstracting |
|
211 $P(x)$ into a function, this is the same as saying that $\lambda x.P(x)$ |
|
212 returns true for all arguments. Thus, the universal quantifier can be |
|
213 represented by a constant |
|
214 \begin{eqnarray*} |
|
215 \forall & :: & (nat\To o) \To o, |
|
216 \end{eqnarray*} |
|
217 which is essentially an infinitary truth table. The representation of $\forall |
|
218 x. P(x)$ is $\forall(\lambda x. P(x))$. |
|
219 |
|
220 The existential quantifier is treated |
|
221 in the same way. Other binding operators are also easily handled; for |
|
222 instance, the summation operator $\Sigma@{k=i}^j f(k)$ can be represented as |
|
223 $\Sigma(i,j,\lambda k.f(k))$, where |
|
224 \begin{eqnarray*} |
|
225 \Sigma & :: & [nat,nat, nat\To nat] \To nat. |
|
226 \end{eqnarray*} |
|
227 Quantifiers may be polymorphic. We may define $\forall$ and~$\exists$ over |
|
228 all legal types of terms, not just the natural numbers, and |
|
229 allow summations over all arithmetic types: |
|
230 \begin{eqnarray*} |
|
231 \forall,\exists & :: & (\alpha{::}term\To o) \To o \\ |
|
232 \Sigma & :: & [nat,nat, nat\To \alpha{::}arith] \To \alpha |
|
233 \end{eqnarray*} |
|
234 Observe that the index variables still have type $nat$, while the values |
|
235 being summed may belong to any arithmetic type. |
|
236 |
|
237 |
|
238 \section{Formalizing logical rules in Isabelle} |
|
239 \index{meta-logic|bold} |
|
240 \index{Isabelle!formalizing rules|bold} |
|
241 \index{$\Imp$|bold}\index{$\Forall$|bold}\index{$\equiv$|bold} |
|
242 \index{implication!meta-level|bold} |
|
243 \index{quantifiers!meta-level|bold} |
|
244 \index{equality!meta-level|bold} |
|
245 Object-logics are formalized by extending Isabelle's meta-logic, which is |
|
246 intuitionistic higher-order logic. The meta-level connectives are {\bf |
|
247 implication}, the {\bf universal quantifier}, and {\bf equality}. |
|
248 \begin{itemize} |
|
249 \item The implication \(\phi\Imp \psi\) means `\(\phi\) implies |
|
250 \(\psi\)', and expresses logical {\bf entailment}. |
|
251 |
|
252 \item The quantification \(\Forall x.\phi\) means `\(\phi\) is true for |
|
253 all $x$', and expresses {\bf generality} in rules and axiom schemes. |
|
254 |
|
255 \item The equality \(a\equiv b\) means `$a$ equals $b$', for expressing |
|
256 \bfindex{definitions} (see~\S\ref{definitions}). Equalities left over |
|
257 from the unification process, so called \bfindex{flex-flex equations}, |
|
258 are written $a\qeq b$. The two equality symbols have the same logical |
|
259 meaning. |
|
260 |
|
261 \end{itemize} |
|
262 The syntax of the meta-logic is formalized in precisely in the same manner |
|
263 as object-logics, using the typed $\lambda$-calculus. Analogous to |
|
264 type~$o$ above, there is a built-in type $prop$ of meta-level truth values. |
|
265 Meta-level formulae will have this type. Type $prop$ belongs to |
|
266 class~$logic$; also, $\sigma\To\tau$ belongs to $logic$ provided $\sigma$ |
|
267 and $\tau$ do. Here are the types of the built-in connectives: |
|
268 \begin{eqnarray*} |
|
269 \Imp & :: & [prop,prop]\To prop \\ |
|
270 \Forall & :: & (\alpha{::}logic\To prop) \To prop \\ |
|
271 {\equiv} & :: & [\alpha{::}\{\},\alpha]\To prop \\ |
|
272 \qeq & :: & [\alpha{::}\{\},\alpha]\To prop c |
|
273 \end{eqnarray*} |
|
274 The restricted polymorphism in $\Forall$ excludes certain types, those used |
|
275 just for parsing. |
|
276 |
|
277 In our formalization of first-order logic, we declared a type~$o$ of |
|
278 object-level truth values, rather than using~$prop$ for this purpose. If |
|
279 we declared the object-level connectives to have types such as |
|
280 ${\neg}::prop\To prop$, then these connectives would be applicable to |
|
281 meta-level formulae. Keeping $prop$ and $o$ as separate types maintains |
|
282 the distinction between the meta-level and the object-level. To formalize |
|
283 the inference rules, we shall need to relate the two levels; accordingly, |
|
284 we declare the constant |
|
285 \index{Trueprop@{$Trueprop$}} |
|
286 \begin{eqnarray*} |
|
287 Trueprop & :: & o\To prop. |
|
288 \end{eqnarray*} |
|
289 We may regard $Trueprop$ as a meta-level predicate, reading $Trueprop(P)$ as |
|
290 `$P$ is true at the object-level.' Put another way, $Trueprop$ is a coercion |
|
291 from $o$ to $prop$. |
|
292 |
|
293 |
|
294 \subsection{Expressing propositional rules} |
|
295 \index{rules!propositional|bold} |
|
296 We shall illustrate the use of the meta-logic by formalizing the rules of |
|
297 Figure~\ref{fol-fig}. Each object-level rule is expressed as a meta-level |
|
298 axiom. |
|
299 |
|
300 One of the simplest rules is $(\conj E1)$. Making |
|
301 everything explicit, its formalization in the meta-logic is |
|
302 $$ \Forall P\;Q. Trueprop(P\conj Q) \Imp Trueprop(P). \eqno(\conj E1) $$ |
|
303 This may look formidable, but it has an obvious reading: for all object-level |
|
304 truth values $P$ and~$Q$, if $P\conj Q$ is true then so is~$P$. The |
|
305 reading is correct because the meta-logic has simple models, where |
|
306 types denote sets and $\Forall$ really means `for all.' |
|
307 |
|
308 \index{Trueprop@{$Trueprop$}} |
|
309 Isabelle adopts notational conventions to ease the writing of rules. We may |
|
310 hide the occurrences of $Trueprop$ by making it an implicit coercion. |
|
311 Outer universal quantifiers may be dropped. Finally, the nested implication |
|
312 \[ \phi@1\Imp(\cdots \phi@n\Imp\psi\cdots) \] |
|
313 may be abbreviated as $\List{\phi@1; \ldots; \phi@n} \Imp \psi$, which |
|
314 formalizes a rule of $n$~premises. |
|
315 |
|
316 Using these conventions, the conjunction rules become the following axioms. |
|
317 These fully specify the properties of~$\conj$: |
|
318 $$ \List{P; Q} \Imp P\conj Q \eqno(\conj I) $$ |
|
319 $$ P\conj Q \Imp P \qquad P\conj Q \Imp Q \eqno(\conj E1,2) $$ |
|
320 |
|
321 \noindent |
|
322 Next, consider the disjunction rules. The discharge of assumption in |
|
323 $(\disj E)$ is expressed using $\Imp$: |
|
324 $$ P \Imp P\disj Q \qquad Q \Imp P\disj Q \eqno(\disj I1,2) $$ |
|
325 $$ \List{P\disj Q; P\Imp R; Q\Imp R} \Imp R \eqno(\disj E) $$ |
|
326 |
|
327 \noindent |
|
328 To understand this treatment of assumptions\index{assumptions} in natural |
|
329 deduction, look at implication. The rule $({\imp}I)$ is the classic |
|
330 example of natural deduction: to prove that $P\imp Q$ is true, assume $P$ |
|
331 is true and show that $Q$ must then be true. More concisely, if $P$ |
|
332 implies $Q$ (at the meta-level), then $P\imp Q$ is true (at the |
|
333 object-level). Showing the coercion explicitly, this is formalized as |
|
334 \[ (Trueprop(P)\Imp Trueprop(Q)) \Imp Trueprop(P\imp Q). \] |
|
335 The rule $({\imp}E)$ is straightforward; hiding $Trueprop$, the axioms to |
|
336 specify $\imp$ are |
|
337 $$ (P \Imp Q) \Imp P\imp Q \eqno({\imp}I) $$ |
|
338 $$ \List{P\imp Q; P} \Imp Q. \eqno({\imp}E) $$ |
|
339 |
|
340 \noindent |
|
341 Finally, the intuitionistic contradiction rule is formalized as the axiom |
|
342 $$ \bot \Imp P. \eqno(\bot E) $$ |
|
343 |
|
344 \begin{warn} |
|
345 Earlier versions of Isabelle, and certain |
|
346 papers~\cite{paulson89,paulson700}, use $\List{P}$ to mean $Trueprop(P)$. |
|
347 \index{Trueprop@{$Trueprop$}} |
|
348 \end{warn} |
|
349 |
|
350 \subsection{Quantifier rules and substitution} |
|
351 \index{rules!quantifier|bold}\index{substitution|bold} |
|
352 \index{variables!bound} |
|
353 Isabelle expresses variable binding using $\lambda$-abstraction; for instance, |
|
354 $\forall x.P$ is formalized as $\forall(\lambda x.P)$. Recall that $F(t)$ |
|
355 is Isabelle's syntax for application of the function~$F$ to the argument~$t$; |
|
356 it is not a meta-notation for substitution. On the other hand, a substitution |
|
357 will take place if $F$ has the form $\lambda x.P$; Isabelle transforms |
|
358 $(\lambda x.P)(t)$ to~$P[t/x]$ by $\beta$-conversion. Thus, we can express |
|
359 inference rules that involve substitution for bound variables. |
|
360 |
|
361 \index{parameters|bold}\index{eigenvariables|see{parameters}} |
|
362 A logic may attach provisos to certain of its rules, especially quantifier |
|
363 rules. We cannot hope to formalize arbitrary provisos. Fortunately, those |
|
364 typical of quantifier rules always have the same form, namely `$x$ not free in |
|
365 \ldots {\it (some set of formulae)},' where $x$ is a variable (called a {\bf |
|
366 parameter} or {\bf eigenvariable}) in some premise. Isabelle treats |
|
367 provisos using~$\Forall$, its inbuilt notion of `for all'. |
|
368 |
|
369 \index{$\Forall$} |
|
370 The purpose of the proviso `$x$ not free in \ldots' is |
|
371 to ensure that the premise may not make assumptions about the value of~$x$, |
|
372 and therefore holds for all~$x$. We formalize $(\forall I)$ by |
|
373 \[ \left(\Forall x. Trueprop(P(x))\right) \Imp Trueprop(\forall x.P(x)). \] |
|
374 This means, `if $P(x)$ is true for all~$x$, then $\forall x.P(x)$ is true.' |
|
375 The $\forall E$ rule exploits $\beta$-conversion. Hiding $Trueprop$, the |
|
376 $\forall$ axioms are |
|
377 $$ \left(\Forall x. P(x)\right) \Imp \forall x.P(x) \eqno(\forall I) $$ |
|
378 $$ \forall x.P(x) \Imp P(t). \eqno(\forall E)$$ |
|
379 |
|
380 \noindent |
|
381 We have defined the object-level universal quantifier~($\forall$) |
|
382 using~$\Forall$. But we do not require meta-level counterparts of all the |
|
383 connectives of the object-logic! Consider the existential quantifier: |
|
384 $$ P(t) \Imp \exists x.P(x) \eqno(\exists I)$$ |
|
385 $$ \List{\exists x.P(x);\; \Forall x. P(x)\Imp Q} \Imp Q \eqno(\exists E) $$ |
|
386 Let us verify $(\exists E)$ semantically. Suppose that the premises |
|
387 hold; since $\exists x.P(x)$ is true, we may choose $a$ such that $P(a)$ is |
|
388 true. Instantiating $\Forall x. P(x)\Imp Q$ with $a$ yields $P(a)\Imp Q$, and |
|
389 we obtain the desired conclusion, $Q$. |
|
390 |
|
391 The treatment of substitution deserves mention. The rule |
|
392 \[ \infer{P[u/t]}{t=u & P} \] |
|
393 would be hard to formalize in Isabelle. It calls for replacing~$t$ by $u$ |
|
394 throughout~$P$, which cannot be expressed using $\beta$-conversion. Our |
|
395 rule~$(subst)$ uses the occurrences of~$x$ in~$P$ as a template for |
|
396 substitution, inferring $P[u/x]$ from~$P[t/x]$. When we formalize this as |
|
397 an axiom, the template becomes a function variable: |
|
398 $$ \List{t=u; P(t)} \Imp P(u). \eqno(subst)$$ |
|
399 |
|
400 |
|
401 \subsection{Signatures and theories} |
|
402 \index{signatures|bold}\index{theories|bold} |
|
403 A {\bf signature} contains the information necessary for type checking, |
|
404 parsing and pretty printing. It specifies classes and their |
|
405 relationships; types, with their arities, and constants, with |
|
406 their types. It also contains syntax rules, specified using mixfix |
|
407 declarations. |
|
408 |
|
409 Two signatures can be merged provided their specifications are compatible --- |
|
410 they must not, for example, assign different types to the same constant. |
|
411 Under similar conditions, a signature can be extended. Signatures are |
|
412 managed internally by Isabelle; users seldom encounter them. |
|
413 |
|
414 A {\bf theory} consists of a signature plus a collection of axioms. The |
|
415 {\bf pure} theory contains only the meta-logic. Theories can be combined |
|
416 provided their signatures are compatible. A theory definition extends an |
|
417 existing theory with further signature specifications --- classes, types, |
|
418 constants and mixfix declarations --- plus a list of axioms, expressed as |
|
419 strings to be parsed. A theory can formalize a small piece of mathematics, |
|
420 such as lists and their operations, or an entire logic. A mathematical |
|
421 development typically involves many theories in a hierarchy. For example, |
|
422 the pure theory could be extended to form a theory for |
|
423 Figure~\ref{fol-fig}; this could be extended in two separate ways to form a |
|
424 theory for natural numbers and a theory for lists; the union of these two |
|
425 could be extended into a theory defining the length of a list: |
|
426 \[ \bf |
|
427 \begin{array}{c@{}c@{}c@{}c@{}c} |
|
428 {} & {} & \hbox{Length} & {} & {} \\ |
|
429 {} & {} & \uparrow & {} & {} \\ |
|
430 {} & {} &\hbox{Nat}+\hbox{List}& {} & {} \\ |
|
431 {} & \nearrow & {} & \nwarrow & {} \\ |
|
432 \hbox{Nat} & {} & {} & {} & \hbox{List} \\ |
|
433 {} & \nwarrow & {} & \nearrow & {} \\ |
|
434 {} & {} &\hbox{FOL} & {} & {} \\ |
|
435 {} & {} & \uparrow & {} & {} \\ |
|
436 {} & {} &\hbox{Pure}& {} & {} |
|
437 \end{array} |
|
438 \] |
|
439 Each Isabelle proof typically works within a single theory, which is |
|
440 associated with the proof state. However, many different theories may |
|
441 coexist at the same time, and you may work in each of these during a single |
|
442 session. |
|
443 |
|
444 |
|
445 \section{Proof construction in Isabelle} |
|
446 \index{Isabelle!proof construction in|bold} |
|
447 There is a one-to-one correspondence between meta-level proofs and |
|
448 object-level proofs~\cite{paulson89}. To each use of a meta-level axiom, |
|
449 such as $(\forall I)$, there is a use of the corresponding object-level |
|
450 rule. Object-level assumptions and parameters have meta-level |
|
451 counterparts. The meta-level formalization is {\bf faithful}, admitting no |
|
452 incorrect object-level inferences, and {\bf adequate}, admitting all |
|
453 correct object-level inferences. These properties must be demonstrated |
|
454 separately for each object-logic. |
|
455 |
|
456 The meta-logic is defined by a collection of inference rules, including |
|
457 equational rules for the $\lambda$-calculus, and logical rules. The rules |
|
458 for~$\Imp$ and~$\Forall$ resemble those for~$\imp$ and~$\forall$ in |
|
459 Figure~\ref{fol-fig}. Proofs performed using the primitive meta-rules |
|
460 would be lengthy; Isabelle proofs normally use certain derived rules. |
|
461 {\bf Resolution}, in particular, is convenient for backward proof. |
|
462 |
|
463 Unification is central to theorem proving. It supports quantifier |
|
464 reasoning by allowing certain `unknown' terms to be instantiated later, |
|
465 possibly in stages. When proving that the time required to sort $n$ |
|
466 integers is proportional to~$n^2$, we need not state the constant of |
|
467 proportionality; when proving that a hardware adder will deliver the sum of |
|
468 its inputs, we need not state how many clock ticks will be required. Such |
|
469 quantities often emerge from the proof. |
|
470 |
|
471 \index{variables!schematic|see{unknowns}} |
|
472 Isabelle provides {\bf schematic variables}, or \bfindex{unknowns}, for |
|
473 unification. Logically, unknowns are free variables. Pragmatically, they |
|
474 may be instantiated during a proof, while ordinary variables remain fixed. |
|
475 Unknowns are written with a ?\ prefix and are frequently subscripted: |
|
476 $\Var{a}$, $\Var{a@1}$, $\Var{a@2}$, \ldots, $\Var{P}$, $\Var{P@1}$, \ldots. |
|
477 |
|
478 Recall that an inference rule of the form |
|
479 \[ \infer{\phi}{\phi@1 & \ldots & \phi@n} \] |
|
480 is formalized in Isabelle's meta-logic as the axiom |
|
481 $\List{\phi@1; \ldots; \phi@n} \Imp \phi$. |
|
482 Such axioms resemble {\sc Prolog}'s Horn clauses, and can be combined by |
|
483 resolution --- Isabelle's principal proof method. Resolution yields both |
|
484 forward and backward proof. Backward proof works by unifying a goal with |
|
485 the conclusion of a rule, whose premises become new subgoals. Forward proof |
|
486 works by unifying theorems with the premises of a rule, deriving a new theorem. |
|
487 |
|
488 Isabelle axioms will require an extended notion of resolution, because |
|
489 they differ from Horn clauses in two major respects: |
|
490 \begin{itemize} |
|
491 \item They are written in the typed $\lambda$-calculus, and therefore must be |
|
492 resolved using higher-order unification. |
|
493 |
|
494 \item Horn clauses are composed of atomic formulae. Any formula of the form |
|
495 $Trueprop(\cdots)$ is atomic, but axioms such as ${\imp}I$ and $\forall I$ |
|
496 contain non-atomic formulae. |
|
497 \index{Trueprop@{$Trueprop$}} |
|
498 \end{itemize} |
|
499 Isabelle should not be confused with classical resolution theorem provers |
|
500 such as Otter~\cite{wos-bledsoe}. At the meta-level, Isabelle proves |
|
501 theorems in their positive form, not by refutation. However, an |
|
502 object-logic that includes a contradiction rule may employ a refutation |
|
503 proof procedure. |
|
504 |
|
505 |
|
506 \subsection{Higher-order unification} |
|
507 \index{unification!higher-order|bold} |
|
508 Unification is equation solving. The solution of $f(\Var{x},c) \qeq |
|
509 f(d,\Var{y})$ is $\Var{x}\equiv d$ and $\Var{y}\equiv c$. {\bf |
|
510 Higher-order unification} is equation solving for typed $\lambda$-terms. |
|
511 To handle $\beta$-conversion, it must reduce $(\lambda x.t)u$ to $t[u/x]$. |
|
512 That is easy --- in the typed $\lambda$-calculus, all reduction sequences |
|
513 terminate at a normal form. But it must guess the unknown |
|
514 function~$\Var{f}$ in order to solve the equation |
|
515 \begin{equation} \label{hou-eqn} |
|
516 \Var{f}(t) \qeq g(u@1,\ldots,u@k). |
|
517 \end{equation} |
|
518 Huet's~\cite{huet75} search procedure solves equations by imitation and |
|
519 projection. {\bf Imitation}\index{imitation|bold} makes~$\Var{f}$ apply |
|
520 leading symbol (if a constant) of the right-hand side. To solve |
|
521 equation~(\ref{hou-eqn}), it guesses |
|
522 \[ \Var{f} \equiv \lambda x. g(\Var{h@1}(x),\ldots,\Var{h@k}(x)), \] |
|
523 where $\Var{h@1}$, \ldots, $\Var{h@k}$ are new unknowns. Assuming there are no |
|
524 other occurrences of~$\Var{f}$, equation~(\ref{hou-eqn}) simplifies to the |
|
525 set of equations |
|
526 \[ \Var{h@1}(t)\qeq u@1 \quad\ldots\quad \Var{h@k}(t)\qeq u@k. \] |
|
527 If the procedure solves these equations, instantiating $\Var{h@1}$, \ldots, |
|
528 $\Var{h@k}$, then it yields an instantiation for~$\Var{f}$. |
|
529 |
|
530 \index{projection|bold} |
|
531 {\bf Projection} makes $\Var{f}$ apply one of its arguments. To solve |
|
532 equation~(\ref{hou-eqn}), if $t$ expects~$m$ arguments and delivers a |
|
533 result of suitable type, it guesses |
|
534 \[ \Var{f} \equiv \lambda x. x(\Var{h@1}(x),\ldots,\Var{h@m}(x)), \] |
|
535 where $\Var{h@1}$, \ldots, $\Var{h@m}$ are new unknowns. Assuming there are no |
|
536 other occurrences of~$\Var{f}$, equation~(\ref{hou-eqn}) simplifies to the |
|
537 equation |
|
538 \[ t(\Var{h@1}(t),\ldots,\Var{h@m}(t)) \qeq g(u@1,\ldots,u@k). $$ |
|
539 |
|
540 \begin{warn} |
|
541 Huet's unification procedure is complete. Isabelle's polymorphic version, |
|
542 which solves for type unknowns as well as for term unknowns, is incomplete. |
|
543 The problem is that projection requires type information. In |
|
544 equation~(\ref{hou-eqn}), if the type of~$t$ is unknown, then projections |
|
545 are possible for all~$m\geq0$, and the types of the $\Var{h@i}$ will be |
|
546 similarly unconstrained. Therefore, Isabelle never attempts such |
|
547 projections, and may fail to find unifiers where a type unknown turns out |
|
548 to be a function type. |
|
549 \end{warn} |
|
550 |
|
551 \index{unknowns!of function type|bold} |
|
552 Given $\Var{f}(t@1,\ldots,t@n)\qeq u$, Huet's procedure could make up to |
|
553 $n+1$ guesses. The search tree and set of unifiers may be infinite. But |
|
554 higher-order unification can work effectively, provided you are careful |
|
555 with {\bf function unknowns}: |
|
556 \begin{itemize} |
|
557 \item Equations with no function unknowns are solved using first-order |
|
558 unification, extended to treat bound variables. For example, $\lambda x.x |
|
559 \qeq \lambda x.\Var{y}$ has no solution because $\Var{y}\equiv x$ would |
|
560 capture the free variable~$x$. |
|
561 |
|
562 \item An occurrence of the term $\Var{f}(x,y,z)$, where the arguments are |
|
563 distinct bound variables, causes no difficulties. Its projections can only |
|
564 match the corresponding variables. |
|
565 |
|
566 \item Even an equation such as $\Var{f}(a)\qeq a+a$ is all right. It has |
|
567 four solutions, but Isabelle evaluates them lazily, trying projection before |
|
568 imitation. The first solution is usually the one desired: |
|
569 \[ \Var{f}\equiv \lambda x. x+x \quad |
|
570 \Var{f}\equiv \lambda x. a+x \quad |
|
571 \Var{f}\equiv \lambda x. x+a \quad |
|
572 \Var{f}\equiv \lambda x. a+a \] |
|
573 \item Equations such as $\Var{f}(\Var{x},\Var{y})\qeq t$ and |
|
574 $\Var{f}(\Var{g}(x))\qeq t$ admit vast numbers of unifiers, and must be |
|
575 avoided. |
|
576 \end{itemize} |
|
577 In problematic cases, you may have to instantiate some unknowns before |
|
578 invoking unification. |
|
579 |
|
580 |
|
581 \subsection{Joining rules by resolution} \label{joining} |
|
582 \index{resolution|bold} |
|
583 Let $\List{\psi@1; \ldots; \psi@m} \Imp \psi$ and $\List{\phi@1; \ldots; |
|
584 \phi@n} \Imp \phi$ be two Isabelle theorems, representing object-level rules. |
|
585 Choosing some~$i$ from~1 to~$n$, suppose that $\psi$ and $\phi@i$ have a |
|
586 higher-order unifier. Writing $Xs$ for the application of substitution~$s$ to |
|
587 expression~$X$, this means there is some~$s$ such that $\psi s\equiv \phi@i s$. |
|
588 By resolution, we may conclude |
|
589 \[ (\List{\phi@1; \ldots; \phi@{i-1}; \psi@1; \ldots; \psi@m; |
|
590 \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s. |
|
591 \] |
|
592 The substitution~$s$ may instantiate unknowns in both rules. In short, |
|
593 resolution is the following rule: |
|
594 \[ \infer[(\psi s\equiv \phi@i s)] |
|
595 {(\List{\phi@1; \ldots; \phi@{i-1}; \psi@1; \ldots; \psi@m; |
|
596 \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s} |
|
597 {\List{\psi@1; \ldots; \psi@m} \Imp \psi & & |
|
598 \List{\phi@1; \ldots; \phi@n} \Imp \phi} |
|
599 \] |
|
600 It operates at the meta-level, on Isabelle theorems, and is justified by |
|
601 the properties of $\Imp$ and~$\Forall$. It takes the number~$i$ (for |
|
602 $1\leq i\leq n$) as a parameter and may yield infinitely many conclusions, |
|
603 one for each unifier of $\psi$ with $\phi@i$. Isabelle returns these |
|
604 conclusions as a sequence (lazy list). |
|
605 |
|
606 Resolution expects the rules to have no outer quantifiers~($\Forall$). It |
|
607 may rename or instantiate any schematic variables, but leaves free |
|
608 variables unchanged. When constructing a theory, Isabelle puts the rules |
|
609 into a standard form containing no free variables; for instance, $({\imp}E)$ |
|
610 becomes |
|
611 \[ \List{\Var{P}\imp \Var{Q}; \Var{P}} \Imp \Var{Q}. |
|
612 \] |
|
613 When resolving two rules, the unknowns in the first rule are renamed, by |
|
614 subscripting, to make them distinct from the unknowns in the second rule. To |
|
615 resolve $({\imp}E)$ with itself, the first copy of the rule would become |
|
616 \[ \List{\Var{P@1}\imp \Var{Q@1}; \Var{P@1}} \Imp \Var{Q@1}. \] |
|
617 Resolving this with $({\imp}E)$ in the first premise, unifying $\Var{Q@1}$ with |
|
618 $\Var{P}\imp \Var{Q}$, is the meta-level inference |
|
619 \[ \infer{\List{\Var{P@1}\imp (\Var{P}\imp \Var{Q}); \Var{P@1}; \Var{P}} |
|
620 \Imp\Var{Q}.} |
|
621 {\List{\Var{P@1}\imp \Var{Q@1}; \Var{P@1}} \Imp \Var{Q@1} & & |
|
622 \List{\Var{P}\imp \Var{Q}; \Var{P}} \Imp \Var{Q}} |
|
623 \] |
|
624 Renaming the unknowns in the resolvent, we have derived the |
|
625 object-level rule |
|
626 \[ \infer{Q.}{R\imp (P\imp Q) & R & P} \] |
|
627 \index{rules!derived} |
|
628 Joining rules in this fashion is a simple way of proving theorems. The |
|
629 derived rules are conservative extensions of the object-logic, and may permit |
|
630 simpler proofs. Let us consider another example. Suppose we have the axiom |
|
631 $$ \forall x\,y. Suc(x)=Suc(y)\imp x=y. \eqno (inject) $$ |
|
632 |
|
633 \noindent |
|
634 The standard form of $(\forall E)$ is |
|
635 $\forall x.\Var{P}(x) \Imp \Var{P}(\Var{t})$. |
|
636 Resolving $(inject)$ with $(\forall E)$ replaces $\Var{P}$ by |
|
637 $\lambda x. \forall y. Suc(x)=Suc(y)\imp x=y$ and leaves $\Var{t}$ |
|
638 unchanged, yielding |
|
639 \[ \forall y. Suc(\Var{t})=Suc(y)\imp \Var{t}=y. \] |
|
640 Resolving this with $(\forall E)$ puts a subscript on~$\Var{t}$ |
|
641 and yields |
|
642 \[ Suc(\Var{t@1})=Suc(\Var{t})\imp \Var{t@1}=\Var{t}. \] |
|
643 Resolving this with $({\imp}E)$ increases the subscripts and yields |
|
644 \[ Suc(\Var{t@2})=Suc(\Var{t@1})\Imp \Var{t@2}=\Var{t@1}. |
|
645 \] |
|
646 We have derived the rule |
|
647 \[ \infer{m=n,}{Suc(m)=Suc(n)} \] |
|
648 which goes directly from $Suc(m)=Suc(n)$ to $m=n$. It is handy for simplifying |
|
649 an equation like $Suc(Suc(Suc(m)))=Suc(Suc(Suc(0)))$. |
|
650 |
|
651 |
|
652 \subsection{Lifting a rule into a context} |
|
653 The rules $({\imp}I)$ and $(\forall I)$ may seem unsuitable for |
|
654 resolution. They have non-atomic premises, namely $P\Imp Q$ and $\Forall |
|
655 x.P(x)$, while the conclusions of all the rules are atomic (they have the form |
|
656 $Trueprop(\cdots)$). Isabelle gets round the problem through a meta-inference |
|
657 called \bfindex{lifting}. Let us consider how to construct proofs such as |
|
658 \[ \infer[({\imp}I)]{P\imp(Q\imp R)} |
|
659 {\infer[({\imp}I)]{Q\imp R} |
|
660 {\infer*{R}{[P] & [Q]}}} |
|
661 \qquad |
|
662 \infer[(\forall I)]{\forall x\,y.P(x,y)} |
|
663 {\infer[(\forall I)]{\forall y.P(x,y)}{P(x,y)}} |
|
664 \] |
|
665 |
|
666 \subsubsection{Lifting over assumptions} |
|
667 \index{lifting!over assumptions|bold} |
|
668 Lifting over $\theta\Imp{}$ is the following meta-inference rule: |
|
669 \[ \infer{\List{\theta\Imp\phi@1; \ldots; \theta\Imp\phi@n} \Imp |
|
670 (\theta \Imp \phi)} |
|
671 {\List{\phi@1; \ldots; \phi@n} \Imp \phi} \] |
|
672 This is clearly sound: if $\List{\phi@1; \ldots; \phi@n} \Imp \phi$ is true and |
|
673 $\theta\Imp\phi@1$, \ldots, $\theta\Imp\phi@n$, $\theta$ are all true then |
|
674 $\phi$ must be true. Iterated lifting over a series of meta-formulae |
|
675 $\theta@k$, \ldots, $\theta@1$ yields an object-rule whose conclusion is |
|
676 $\List{\theta@1; \ldots; \theta@k} \Imp \phi$. Typically the $\theta@i$ are |
|
677 the assumptions in a natural deduction proof; lifting copies them into a rule's |
|
678 premises and conclusion. |
|
679 |
|
680 When resolving two rules, Isabelle lifts the first one if necessary. The |
|
681 standard form of $({\imp}I)$ is |
|
682 \[ (\Var{P} \Imp \Var{Q}) \Imp \Var{P}\imp \Var{Q}. \] |
|
683 To resolve this rule with itself, Isabelle modifies one copy as follows: it |
|
684 renames the unknowns to $\Var{P@1}$ and $\Var{Q@1}$, then lifts the rule over |
|
685 $\Var{P}\Imp{}$: |
|
686 \[ \List{\List{\Var{P}; \Var{P@1}} \Imp \Var{Q@1}; \Var{P}} |
|
687 \Imp \Var{P@1}\imp \Var{Q@1}. \] |
|
688 Unifying $\Var{P}\Imp \Var{P@1}\imp\Var{Q@1}$ with $\Var{P} \Imp |
|
689 \Var{Q}$ instantiates $\Var{Q}$ to ${\Var{P@1}\imp\Var{Q@1}}$. |
|
690 Resolution yields |
|
691 \[ (\List{\Var{P}; \Var{P@1}} \Imp \Var{Q@1}) \Imp |
|
692 \Var{P}\imp(\Var{P@1}\imp\Var{Q@1}). \] |
|
693 This represents the derived rule |
|
694 \[ \infer{P\imp(Q\imp R).}{\infer*{R}{[P,Q]}} \] |
|
695 |
|
696 \subsubsection{Lifting over parameters} |
|
697 \index{lifting!over parameters|bold} |
|
698 An analogous form of lifting handles premises of the form $\Forall x\ldots\,$. |
|
699 Here, lifting prefixes an object-rule's premises and conclusion with $\Forall |
|
700 x$. At the same time, lifting introduces a dependence upon~$x$. It replaces |
|
701 each unknown $\Var{a}$ in the rule by $\Var{a'}(x)$, where $\Var{a'}$ is a new |
|
702 unknown (by subscripting) of suitable type --- necessarily a function type. In |
|
703 short, lifting is the meta-inference |
|
704 \[ \infer{\List{\Forall x.\phi@1^x; \ldots; \Forall x.\phi@n^x} |
|
705 \Imp \Forall x.\phi^x,} |
|
706 {\List{\phi@1; \ldots; \phi@n} \Imp \phi} \] |
|
707 where $\phi^x$ stands for the result of lifting unknowns over~$x$ in $\phi$. |
|
708 It is not hard to verify that this meta-inference is sound. |
|
709 For example, $(\disj I)$ might be lifted to |
|
710 \[ (\Forall x.\Var{P@1}(x)) \Imp (\Forall x. \Var{P@1}(x)\disj \Var{Q@1}(x))\] |
|
711 and $(\forall I)$ to |
|
712 \[ (\Forall x\,y.\Var{P@1}(x,y)) \Imp (\Forall x. \forall y.\Var{P@1}(x,y)). \] |
|
713 Isabelle has renamed a bound variable in $(\forall I)$ from $x$ to~$y$, |
|
714 avoiding a clash. Resolving the above with $(\forall I)$ is the meta-inference |
|
715 \[ \infer{\Forall x\,y.\Var{P@1}(x,y)) \Imp \forall x\,y.\Var{P@1}(x,y)) } |
|
716 {(\Forall x\,y.\Var{P@1}(x,y)) \Imp |
|
717 (\Forall x. \forall y.\Var{P@1}(x,y)) & |
|
718 (\Forall x.\Var{P}(x)) \Imp (\forall x.\Var{P}(x))} \] |
|
719 Here, $\Var{P}$ is replaced by $\lambda x.\forall y.\Var{P@1}(x,y)$; the |
|
720 resolvent expresses the derived rule |
|
721 \[ \vcenter{ \infer{\forall x\,y.Q(x,y)}{Q(x,y)} } |
|
722 \quad\hbox{provided $x$, $y$ not free in the assumptions} |
|
723 \] |
|
724 I discuss lifting and parameters at length elsewhere~\cite{paulson89}. |
|
725 Miller goes into even greater detail~\cite{miller-jsc}. |
|
726 |
|
727 |
|
728 \section{Backward proof by resolution} |
|
729 \index{resolution!in backward proof}\index{proof!backward|bold} |
|
730 Resolution is convenient for deriving simple rules and for reasoning |
|
731 forward from facts. It can also support backward proof, where we start |
|
732 with a goal and refine it to progressively simpler subgoals until all have |
|
733 been solved. {\sc lcf} (and its descendants {\sc hol} and Nuprl) provide |
|
734 tactics and tacticals, which constitute a high-level language for |
|
735 expressing proof searches. \bfindex{Tactics} perform primitive refinements |
|
736 while \bfindex{tacticals} combine tactics. |
|
737 |
|
738 \index{LCF} |
|
739 Isabelle's tactics and tacticals work differently from {\sc lcf}'s. An |
|
740 Isabelle rule is {\bf bidirectional}: there is no distinction between |
|
741 inputs and outputs. {\sc lcf} has a separate tactic for each rule; |
|
742 Isabelle performs refinement by any rule in a uniform fashion, using |
|
743 resolution. |
|
744 |
|
745 \index{subgoals|bold}\index{main goal|bold} |
|
746 Isabelle works with meta-level theorems of the form |
|
747 \( \List{\phi@1; \ldots; \phi@n} \Imp \phi \). |
|
748 We have viewed this as the {\bf rule} with premises |
|
749 $\phi@1$,~\ldots,~$\phi@n$ and conclusion~$\phi$. It can also be viewed as |
|
750 the \bfindex{proof state} with subgoals $\phi@1$,~\ldots,~$\phi@n$ and main |
|
751 goal~$\phi$. |
|
752 |
|
753 To prove the formula~$\phi$, take $\phi\Imp \phi$ as the initial proof |
|
754 state. This assertion is, trivially, a theorem. At a later stage in the |
|
755 backward proof, a typical proof state is $\List{\phi@1; \ldots; \phi@n} |
|
756 \Imp \phi$. This proof state is a theorem, guaranteeing that the subgoals |
|
757 $\phi@1$,~\ldots,~$\phi@n$ imply~$\phi$. If $m=0$ then we have |
|
758 proved~$\phi$ outright. If $\phi$ contains unknowns, they may become |
|
759 instantiated during the proof; a proof state may be $\List{\phi@1; \ldots; |
|
760 \phi@n} \Imp \phi'$, where $\phi'$ is an instance of~$\phi$. |
|
761 |
|
762 \subsection{Refinement by resolution} |
|
763 \index{refinement|bold} |
|
764 To refine subgoal~$i$ of a proof state by a rule, perform the following |
|
765 resolution: |
|
766 \[ \infer{\hbox{new proof state}}{\hbox{rule} & & \hbox{proof state}} \] |
|
767 If the rule is $\List{\psi'@1; \ldots; \psi'@m} \Imp \psi'$ after lifting |
|
768 over subgoal~$i$, and the proof state is $\List{\phi@1; \ldots; \phi@n} |
|
769 \Imp \phi$, then the new proof state is (for~$1\leq i\leq n$) |
|
770 \[ (\List{\phi@1; \ldots; \phi@{i-1}; \psi'@1; |
|
771 \ldots; \psi'@m; \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s. \] |
|
772 Substitution~$s$ unifies $\psi'$ with~$\phi@i$. In the proof state, |
|
773 subgoal~$i$ is replaced by $m$ new subgoals, the rule's instantiated premises. |
|
774 If some of the rule's unknowns are left un-instantiated, they become new |
|
775 unknowns in the proof state. Refinement by~$(\exists I)$, namely |
|
776 \[ \Var{P}(\Var{t}) \Imp \exists x. \Var{P}(x), \] |
|
777 inserts a new unknown derived from~$\Var{t}$ by subscripting and lifting. |
|
778 We do not have to specify an `existential witness' when |
|
779 applying~$(\exists I)$. Further resolutions may instantiate unknowns in |
|
780 the proof state. |
|
781 |
|
782 \subsection{Proof by assumption} |
|
783 \index{proof!by assumption|bold} |
|
784 In the course of a natural deduction proof, parameters $x@1$, \ldots,~$x@l$ and |
|
785 assumptions $\theta@1$, \ldots, $\theta@k$ accumulate, forming a context for |
|
786 each subgoal. Repeated lifting steps can lift a rule into any context. To |
|
787 aid readability, Isabelle puts contexts into a normal form, gathering the |
|
788 parameters at the front: |
|
789 \begin{equation} \label{context-eqn} |
|
790 \Forall x@1 \ldots x@l. \List{\theta@1; \ldots; \theta@k}\Imp\theta. |
|
791 \end{equation} |
|
792 Under the usual reading of the connectives, this expresses that $\theta$ |
|
793 follows from $\theta@1$,~\ldots~$\theta@k$ for arbitrary |
|
794 $x@1$,~\ldots,~$x@l$. It is trivially true if $\theta$ equals any of |
|
795 $\theta@1$,~\ldots~$\theta@k$, or is unifiable with any of them. This |
|
796 models proof by assumption in natural deduction. |
|
797 |
|
798 Isabelle automates the meta-inference for proof by assumption. Its arguments |
|
799 are the meta-theorem $\List{\phi@1; \ldots; \phi@n} \Imp \phi$, and some~$i$ |
|
800 from~1 to~$n$, where $\phi@i$ has the form~(\ref{context-eqn}). Its results |
|
801 are meta-theorems of the form |
|
802 \[ (\List{\phi@1; \ldots; \phi@{i-1}; \phi@{i+1}; \phi@n} \Imp \phi)s \] |
|
803 for each $s$ and~$j$ such that $s$ unifies $\lambda x@1 \ldots x@l. \theta@j$ |
|
804 with $\lambda x@1 \ldots x@l. \theta$. Isabelle supplies the parameters |
|
805 $x@1$,~\ldots,~$x@l$ to higher-order unification as bound variables, which |
|
806 regards them as unique constants with a limited scope --- this enforces |
|
807 parameter provisos~\cite{paulson89}. |
|
808 |
|
809 The premise represents a proof state with~$n$ subgoals, of which the~$i$th is |
|
810 to be solved by assumption. Isabelle searches the subgoal's context for an |
|
811 assumption, say $\theta@j$, that can solve it by unification. For each |
|
812 unifier, the meta-inference returns an instantiated proof state from which the |
|
813 $i$th subgoal has been removed. Isabelle searches for a unifying assumption; |
|
814 for readability and robustness, proofs do not refer to assumptions by number. |
|
815 |
|
816 Consider the proof state $(\List{P(a); P(b)} \Imp P(\Var{x})) \Imp Q(\Var{x})$. |
|
817 Proof by assumption (with $i=1$, the only possibility) yields two results: |
|
818 \begin{itemize} |
|
819 \item $Q(a)$, instantiating $\Var{x}\equiv a$ |
|
820 \item $Q(b)$, instantiating $\Var{x}\equiv b$ |
|
821 \end{itemize} |
|
822 Here, proof by assumption affects the main goal. It could also affect |
|
823 other subgoals. Consider the effect of having the |
|
824 additional subgoal ${\List{P(b); P(c)} \Imp P(\Var{x})}$. |
|
825 |
|
826 \subsection{A propositional proof} \label{prop-proof} |
|
827 \index{examples!propositional} |
|
828 Our first example avoids quantifiers. Given the main goal $P\disj P\imp |
|
829 P$, Isabelle creates the initial state |
|
830 \[ (P\disj P\imp P)\Imp (P\disj P\imp P). \] |
|
831 Bear in mind that every proof state we derive will be a meta-theorem, |
|
832 expressing that the subgoals imply the main goal. The first step is to refine |
|
833 subgoal~1 by (${\imp}I)$, creating a new state where $P\disj P$ is an |
|
834 assumption: |
|
835 \[ (P\disj P\Imp P)\Imp (P\disj P\imp P) \] |
|
836 The next step is $(\disj E)$, which replaces subgoal~1 by three new subgoals. |
|
837 Because of lifting, each subgoal contains a copy of the context --- the |
|
838 assumption $P\disj P$. (In fact, this assumption is now redundant; we shall |
|
839 shortly see how to get rid of it!) The new proof state is the following |
|
840 meta-theorem, laid out for clarity: |
|
841 \[ \begin{array}{l@{}l@{\qquad\qquad}l} |
|
842 \lbrakk\;& P\disj P\Imp \Var{P@1}\disj\Var{Q@1}; & \hbox{(subgoal 1)} \\ |
|
843 & \List{P\disj P; \Var{P@1}} \Imp P; & \hbox{(subgoal 2)} \\ |
|
844 & \List{P\disj P; \Var{Q@1}} \Imp P & \hbox{(subgoal 3)} \\ |
|
845 \rbrakk\;& \Imp (P\disj P\imp P) & \hbox{(main goal)} |
|
846 \end{array} |
|
847 \] |
|
848 Notice the unknowns in the proof state. Because we have applied $(\disj E)$, |
|
849 we must prove some disjunction, $\Var{P@1}\disj\Var{Q@1}$. Of course, |
|
850 subgoal~1 is provable by assumption. This instantiates both $\Var{P@1}$ and |
|
851 $\Var{Q@1}$ to~$P$ throughout the proof state: |
|
852 \[ \begin{array}{l@{}l@{\qquad\qquad}l} |
|
853 \lbrakk\;& \List{P\disj P; P} \Imp P; & \hbox{(subgoal 1)} \\ |
|
854 & \List{P\disj P; P} \Imp P & \hbox{(subgoal 2)} \\ |
|
855 \rbrakk\;& \Imp (P\disj P\imp P) & \hbox{(main goal)} |
|
856 \end{array} \] |
|
857 Both of the remaining subgoals can be proved by assumption. After two such |
|
858 steps, the proof state is simply the meta-theorem $P\disj P\imp P$. This is |
|
859 our desired result. |
|
860 |
|
861 \subsection{A quantifier proof} |
|
862 \index{examples!with quantifiers} |
|
863 To illustrate quantifiers and $\Forall$-lifting, let us prove |
|
864 $(\exists x.P(f(x)))\imp(\exists x.P(x))$. The initial proof |
|
865 state is the trivial meta-theorem |
|
866 \[ (\exists x.P(f(x)))\imp(\exists x.P(x)) \Imp |
|
867 (\exists x.P(f(x)))\imp(\exists x.P(x)). \] |
|
868 As above, the first step is refinement by (${\imp}I)$: |
|
869 \[ (\exists x.P(f(x))\Imp \exists x.P(x)) \Imp |
|
870 (\exists x.P(f(x)))\imp(\exists x.P(x)) |
|
871 \] |
|
872 The next step is $(\exists E)$, which replaces subgoal~1 by two new subgoals. |
|
873 Both have the assumption $\exists x.P(f(x))$. The new proof |
|
874 state is the meta-theorem |
|
875 \[ \begin{array}{l@{}l@{\qquad\qquad}l} |
|
876 \lbrakk\;& \exists x.P(f(x)) \Imp \exists x.\Var{P@1}(x); & \hbox{(subgoal 1)} \\ |
|
877 & \Forall x.\List{\exists x.P(f(x)); \Var{P@1}(x)} \Imp |
|
878 \exists x.P(x) & \hbox{(subgoal 2)} \\ |
|
879 \rbrakk\;& \Imp (\exists x.P(f(x)))\imp(\exists x.P(x)) & \hbox{(main goal)} |
|
880 \end{array} |
|
881 \] |
|
882 The unknown $\Var{P@1}$ appears in both subgoals. Because we have applied |
|
883 $(\exists E)$, we must prove $\exists x.\Var{P@1}(x)$, where $\Var{P@1}(x)$ may |
|
884 become any formula possibly containing~$x$. Proving subgoal~1 by assumption |
|
885 instantiates $\Var{P@1}$ to~$\lambda x.P(f(x))$: |
|
886 \[ \left(\Forall x.\List{\exists x.P(f(x)); P(f(x))} \Imp |
|
887 \exists x.P(x)\right) |
|
888 \Imp (\exists x.P(f(x)))\imp(\exists x.P(x)) |
|
889 \] |
|
890 The next step is refinement by $(\exists I)$. The rule is lifted into the |
|
891 context of the parameter~$x$ and the assumption $P(f(x))$. This ensures that |
|
892 the context is copied to the subgoal and allows the existential witness to |
|
893 depend upon~$x$: |
|
894 \[ \left(\Forall x.\List{\exists x.P(f(x)); P(f(x))} \Imp |
|
895 P(\Var{x@2}(x))\right) |
|
896 \Imp (\exists x.P(f(x)))\imp(\exists x.P(x)) |
|
897 \] |
|
898 The existential witness, $\Var{x@2}(x)$, consists of an unknown |
|
899 applied to a parameter. Proof by assumption unifies $\lambda x.P(f(x))$ |
|
900 with $\lambda x.P(\Var{x@2}(x))$, instantiating $\Var{x@2}$ to $f$. The final |
|
901 proof state contains no subgoals: $(\exists x.P(f(x)))\imp(\exists x.P(x))$. |
|
902 |
|
903 |
|
904 \subsection{Tactics and tacticals} |
|
905 \index{tactics|bold}\index{tacticals|bold} |
|
906 {\bf Tactics} perform backward proof. Isabelle tactics differ from those |
|
907 of {\sc lcf}, {\sc hol} and Nuprl by operating on entire proof states, |
|
908 rather than on individual subgoals. An Isabelle tactic is a function that |
|
909 takes a proof state and returns a sequence (lazy list) of possible |
|
910 successor states. Sequences are coded in ML as functions, a standard |
|
911 technique~\cite{paulson91}. Isabelle represents proof states by theorems. |
|
912 |
|
913 Basic tactics execute the meta-rules described above, operating on a |
|
914 given subgoal. The {\bf resolution tactics} take a list of rules and |
|
915 return next states for each combination of rule and unifier. The {\bf |
|
916 assumption tactic} examines the subgoal's assumptions and returns next |
|
917 states for each combination of assumption and unifier. Lazy lists are |
|
918 essential because higher-order resolution may return infinitely many |
|
919 unifiers. If there are no matching rules or assumptions then no next |
|
920 states are generated; a tactic application that returns an empty list is |
|
921 said to {\bf fail}. |
|
922 |
|
923 Sequences realize their full potential with {\bf tacticals} --- operators |
|
924 for combining tactics. Depth-first search, breadth-first search and |
|
925 best-first search (where a heuristic function selects the best state to |
|
926 explore) return their outcomes as a sequence. Isabelle provides such |
|
927 procedures in the form of tacticals. Simpler procedures can be expressed |
|
928 directly using the basic tacticals {\it THEN}, {\it ORELSE} and {\it REPEAT}: |
|
929 \begin{description} |
|
930 \item[$tac1\;THEN\;tac2$] is a tactic for sequential composition. Applied |
|
931 to a proof state, it returns all states reachable in two steps by applying |
|
932 $tac1$ followed by~$tac2$. |
|
933 |
|
934 \item[$tac1\;ORELSE\;tac2$] is a choice tactic. Applied to a state, it |
|
935 tries~$tac1$ and returns the result if non-empty; otherwise, it uses~$tac2$. |
|
936 |
|
937 \item[$REPEAT\;tac$] is a repetition tactic. Applied to a state, it |
|
938 returns all states reachable by applying~$tac$ as long as possible (until |
|
939 it would fail). $REPEAT$ can be expressed in a few lines of \ML{} using |
|
940 {\it THEN} and~{\it ORELSE}. |
|
941 \end{description} |
|
942 For instance, this tactic repeatedly applies $tac1$ and~$tac2$, giving |
|
943 $tac1$ priority: |
|
944 \[ REPEAT(tac1\;ORELSE\;tac2) \] |
|
945 |
|
946 |
|
947 \section{Variations on resolution} |
|
948 In principle, resolution and proof by assumption suffice to prove all |
|
949 theorems. However, specialized forms of resolution are helpful for working |
|
950 with elimination rules. Elim-resolution applies an elimination rule to an |
|
951 assumption; destruct-resolution is similar, but applies a rule in a forward |
|
952 style. |
|
953 |
|
954 The last part of the section shows how the techniques for proving theorems |
|
955 can also serve to derive rules. |
|
956 |
|
957 \subsection{Elim-resolution} |
|
958 \index{elim-resolution|bold} |
|
959 Consider proving the theorem $((R\disj R)\disj R)\disj R\imp R$. By |
|
960 $({\imp}I)$, we prove $R$ from the assumption $((R\disj R)\disj R)\disj R$. |
|
961 Applying $(\disj E)$ to this assumption yields two subgoals, one that |
|
962 assumes~$R$ (and is therefore trivial) and one that assumes $(R\disj |
|
963 R)\disj R$. This subgoal admits another application of $(\disj E)$. Since |
|
964 natural deduction never discards assumptions, we eventually generate a |
|
965 subgoal containing much that is redundant: |
|
966 \[ \List{((R\disj R)\disj R)\disj R; (R\disj R)\disj R; R\disj R; R} \Imp R. \] |
|
967 In general, using $(\disj E)$ on the assumption $P\disj Q$ creates two new |
|
968 subgoals with the additional assumption $P$ or~$Q$. In these subgoals, |
|
969 $P\disj Q$ is redundant. It wastes space; worse, it could make a theorem |
|
970 prover repeatedly apply~$(\disj E)$, looping. Other elimination rules pose |
|
971 similar problems. In first-order logic, only universally quantified |
|
972 assumptions are sometimes needed more than once --- say, to prove |
|
973 $P(f(f(a)))$ from the assumptions $\forall x.P(x)\imp P(f(x))$ and~$P(a)$. |
|
974 |
|
975 Many logics can be formulated as sequent calculi that delete redundant |
|
976 assumptions after use. The rule $(\disj E)$ might become |
|
977 \[ \infer[\disj\hbox{-left}] |
|
978 {\Gamma,P\disj Q,\Delta \turn \Theta} |
|
979 {\Gamma,P,\Delta \turn \Theta && \Gamma,Q,\Delta \turn \Theta} \] |
|
980 In backward proof, a goal containing $P\disj Q$ on the left of the~$\turn$ |
|
981 (that is, as an assumption) splits into two subgoals, replacing $P\disj Q$ |
|
982 by $P$ or~$Q$. But the sequent calculus, with its explicit handling of |
|
983 assumptions, can be tiresome to use. |
|
984 |
|
985 Elim-resolution is Isabelle's way of getting sequent calculus behaviour |
|
986 from natural deduction rules. It lets an elimination rule consume an |
|
987 assumption. Elim-resolution takes a rule $\List{\psi@1; \ldots; \psi@m} |
|
988 \Imp \psi$ a proof state $\List{\phi@1; \ldots; \phi@n} \Imp \phi$, and a |
|
989 subgoal number~$i$. The rule must have at least one premise, thus $m>0$. |
|
990 Write the rule's lifted form as $\List{\psi'@1; \ldots; \psi'@m} \Imp |
|
991 \psi'$. Ordinary resolution would attempt to reduce~$\phi@i$, |
|
992 replacing subgoal~$i$ by $m$ new ones. Elim-resolution tries {\bf |
|
993 simultaneously} to reduce~$\phi@i$ and to solve~$\psi'@1$ by assumption; it |
|
994 returns a sequence of next states. Each of these replaces subgoal~$i$ by |
|
995 instances of $\psi'@2$, \ldots, $\psi'@m$ from which the selected |
|
996 assumption has been deleted. Suppose $\phi@i$ has the parameter~$x$ and |
|
997 assumptions $\theta@1$,~\ldots,~$\theta@k$. Then $\psi'@1$, the rule's first |
|
998 premise after lifting, will be |
|
999 \( \Forall x. \List{\theta@1; \ldots; \theta@k}\Imp \psi^{x}@1 \). |
|
1000 Elim-resolution tries to unify simultaneously $\psi'\qeq\phi@i$ and |
|
1001 $\lambda x. \theta@j \qeq \lambda x. \psi^{x}@1$, for $j=1$,~\ldots,~$k$. |
|
1002 |
|
1003 Let us redo the example from~\S\ref{prop-proof}. The elimination rule |
|
1004 is~$(\disj E)$, |
|
1005 \[ \List{\Var{P}\disj \Var{Q};\; \Var{P}\Imp \Var{R};\; \Var{Q}\Imp \Var{R}} |
|
1006 \Imp \Var{R} \] |
|
1007 and the proof state is $(P\disj P\Imp P)\Imp (P\disj P\imp P)$. The |
|
1008 lifted rule would be |
|
1009 \[ \begin{array}{l@{}l} |
|
1010 \lbrakk\;& P\disj P \Imp \Var{P@1}\disj\Var{Q@1}; \\ |
|
1011 & \List{P\disj P ;\; \Var{P@1}} \Imp \Var{R@1}; \\ |
|
1012 & \List{P\disj P ;\; \Var{Q@1}} \Imp \Var{R@1} \\ |
|
1013 \rbrakk\;& \Imp \Var{R@1} |
|
1014 \end{array} |
|
1015 \] |
|
1016 Unification would take the simultaneous equations |
|
1017 $P\disj P \qeq \Var{P@1}\disj\Var{Q@1}$ and $\Var{R@1} \qeq P$, yielding |
|
1018 $\Var{P@1}\equiv\Var{Q@1}\equiv\Var{R@1} \equiv P$. The new proof state |
|
1019 would be simply |
|
1020 \[ \List{P \Imp P;\; P \Imp P} \Imp (P\disj P\imp P). |
|
1021 \] |
|
1022 Elim-resolution's simultaneous unification gives better control |
|
1023 than ordinary resolution. Recall the substitution rule: |
|
1024 $$ \List{\Var{t}=\Var{u}; \Var{P}(\Var{t})} \Imp \Var{P}(\Var{u}) |
|
1025 \eqno(subst) $$ |
|
1026 Unsuitable for ordinary resolution because $\Var{P}(\Var{u})$ admits many |
|
1027 unifiers, $(subst)$ works well with elim-resolution. It deletes some |
|
1028 assumption of the form $x=y$ and replaces every~$y$ by~$x$ in the subgoal |
|
1029 formula. The simultaneous unification instantiates $\Var{u}$ to~$y$; if |
|
1030 $y$ is not an unknown, then $\Var{P}(y)$ can easily be unified with another |
|
1031 formula. |
|
1032 |
|
1033 In logical parlance, the premise containing the connective to be eliminated |
|
1034 is called the \bfindex{major premise}. Elim-resolution expects the major |
|
1035 premise to come first. The order of the premises is significant in |
|
1036 Isabelle. |
|
1037 |
|
1038 \subsection{Destruction rules} \label{destruct} |
|
1039 \index{destruction rules|bold}\index{proof!forward} |
|
1040 Looking back to Figure~\ref{fol-fig}, notice that there are two kinds of |
|
1041 elimination rule. The rules $({\conj}E1)$, $({\conj}E2)$, $({\imp}E)$ and |
|
1042 $({\forall}E)$ extract the conclusion from the major premise. In Isabelle |
|
1043 parlance, such rules are called \bfindex{destruction rules}; they are readable |
|
1044 and easy to use in forward proof. The rules $({\disj}E)$, $({\bot}E)$ and |
|
1045 $({\exists}E)$ work by discharging assumptions; they support backward proof |
|
1046 in a style reminiscent of the sequent calculus. |
|
1047 |
|
1048 The latter style is the most general form of elimination rule. In natural |
|
1049 deduction, there is no way to recast $({\disj}E)$, $({\bot}E)$ or |
|
1050 $({\exists}E)$ as destruction rules. But we can write general elimination |
|
1051 rules for $\conj$, $\imp$ and~$\forall$: |
|
1052 \[ |
|
1053 \infer{R}{P\conj Q & \infer*{R}{[P,Q]}} \qquad |
|
1054 \infer{R}{P\imp Q & P & \infer*{R}{[Q]}} \qquad |
|
1055 \infer{Q}{\forall x.P & \infer*{Q}{[P[t/x]]}} |
|
1056 \] |
|
1057 Because they are concise, destruction rules are simpler to derive than the |
|
1058 corresponding elimination rules. To facilitate their use in backward |
|
1059 proof, Isabelle provides a means of transforming a destruction rule such as |
|
1060 \[ \infer[\quad\hbox{to the elimination rule}\quad]{Q}{P@1 & \ldots & P@m} |
|
1061 \infer{R.}{P@1 & \ldots & P@m & \infer*{R}{[Q]}} |
|
1062 \] |
|
1063 \index{destruct-resolution|bold} |
|
1064 {\bf Destruct-resolution} combines this transformation with |
|
1065 elim-resolution. It applies a destruction rule to some assumption of a |
|
1066 subgoal. Given the rule above, it replaces the assumption~$P@1$ by~$Q$, |
|
1067 with new subgoals of showing instances of $P@2$, \ldots,~$P@m$. |
|
1068 Destruct-resolution works forward from a subgoal's assumptions. Ordinary |
|
1069 resolution performs forward reasoning from theorems, as illustrated |
|
1070 in~\S\ref{joining}. |
|
1071 |
|
1072 |
|
1073 \subsection{Deriving rules by resolution} \label{deriving} |
|
1074 \index{rules!derived|bold} |
|
1075 The meta-logic, itself a form of the predicate calculus, is defined by a |
|
1076 system of natural deduction rules. Each theorem may depend upon |
|
1077 meta-assumptions. The theorem that~$\phi$ follows from the assumptions |
|
1078 $\phi@1$, \ldots, $\phi@n$ is written |
|
1079 \[ \phi \quad [\phi@1,\ldots,\phi@n]. \] |
|
1080 A more conventional notation might be $\phi@1,\ldots,\phi@n \turn \phi$, |
|
1081 but Isabelle's notation is more readable with large formulae. |
|
1082 |
|
1083 Meta-level natural deduction provides a convenient mechanism for deriving |
|
1084 new object-level rules. To derive the rule |
|
1085 \[ \infer{\phi,}{\theta@1 & \ldots & \theta@k} \] |
|
1086 assume the premises $\theta@1$,~\ldots,~$\theta@k$ at the |
|
1087 meta-level. Then prove $\phi$, possibly using these assumptions. |
|
1088 Starting with a proof state $\phi\Imp\phi$, assumptions may accumulate, |
|
1089 reaching a final state such as |
|
1090 \[ \phi \quad [\theta@1,\ldots,\theta@k]. \] |
|
1091 The meta-rule for $\Imp$ introduction discharges an assumption. |
|
1092 Discharging them in the order $\theta@k,\ldots,\theta@1$ yields the |
|
1093 meta-theorem $\List{\theta@1; \ldots; \theta@k} \Imp \phi$, with no |
|
1094 assumptions. This represents the desired rule. |
|
1095 Let us derive the general $\conj$ elimination rule: |
|
1096 $$ \infer{R}{P\conj Q & \infer*{R}{[P,Q]}} \eqno(\conj E)$$ |
|
1097 We assume $P\conj Q$ and $\List{P;Q}\Imp R$, and commence backward proof in |
|
1098 the state $R\Imp R$. Resolving this with the second assumption yields the |
|
1099 state |
|
1100 \[ \phantom{\List{P\conj Q;\; P\conj Q}} |
|
1101 \llap{$\List{P;Q}$}\Imp R \quad [\,\List{P;Q}\Imp R\,]. \] |
|
1102 Resolving subgoals~1 and~2 with $({\conj}E1)$ and $({\conj}E2)$, |
|
1103 respectively, yields the state |
|
1104 \[ \List{P\conj Q;\; P\conj Q}\Imp R \quad [\,\List{P;Q}\Imp R\,]. \] |
|
1105 Resolving both subgoals with the assumption $P\conj Q$ yields |
|
1106 \[ R \quad [\, \List{P;Q}\Imp R, P\conj Q \,]. \] |
|
1107 The proof may use the meta-assumptions in any order, and as often as |
|
1108 necessary; when finished, we discharge them in the correct order to |
|
1109 obtain the desired form: |
|
1110 \[ \List{P\conj Q;\; \List{P;Q}\Imp R} \Imp R \] |
|
1111 We have derived the rule using free variables, which prevents their |
|
1112 premature instantiation during the proof; we may now replace them by |
|
1113 schematic variables. |
|
1114 |
|
1115 \begin{warn} |
|
1116 Schematic variables are not allowed in (meta) assumptions because they would |
|
1117 complicate lifting. Assumptions remain fixed throughout a proof. |
|
1118 \end{warn} |
|
1119 |
|
1120 % Local Variables: |
|
1121 % mode: latex |
|
1122 % TeX-master: t |
|
1123 % End: |