author | wenzelm |
Wed, 05 Dec 2001 03:19:47 +0100 | |
changeset 12387 | fe2353a8d1e8 |
parent 10636 | d1efa59ea259 |
child 16417 | 9bc16273c2d4 |
permissions | -rw-r--r-- |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Isar_examples/BasicLogic.thy |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Muenchen |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
4 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
5 |
Basic propositional and quantifier reasoning. |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
6 |
*) |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
7 |
|
10007 | 8 |
header {* Basic logical reasoning *} |
7748 | 9 |
|
10007 | 10 |
theory BasicLogic = Main: |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
11 |
|
7761 | 12 |
|
10007 | 13 |
subsection {* Pure backward reasoning *} |
7740 | 14 |
|
7820 | 15 |
text {* |
16 |
In order to get a first idea of how Isabelle/Isar proof documents may |
|
17 |
look like, we consider the propositions $I$, $K$, and $S$. The |
|
18 |
following (rather explicit) proofs should require little extra |
|
19 |
explanations. |
|
10007 | 20 |
*} |
7001 | 21 |
|
10007 | 22 |
lemma I: "A --> A" |
23 |
proof |
|
24 |
assume A |
|
25 |
show A by assumption |
|
26 |
qed |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
27 |
|
10007 | 28 |
lemma K: "A --> B --> A" |
29 |
proof |
|
30 |
assume A |
|
31 |
show "B --> A" |
|
32 |
proof |
|
33 |
show A by assumption |
|
34 |
qed |
|
35 |
qed |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
36 |
|
10007 | 37 |
lemma S: "(A --> B --> C) --> (A --> B) --> A --> C" |
38 |
proof |
|
39 |
assume "A --> B --> C" |
|
40 |
show "(A --> B) --> A --> C" |
|
41 |
proof |
|
42 |
assume "A --> B" |
|
43 |
show "A --> C" |
|
44 |
proof |
|
45 |
assume A |
|
46 |
show C |
|
47 |
proof (rule mp) |
|
48 |
show "B --> C" by (rule mp) |
|
49 |
show B by (rule mp) |
|
50 |
qed |
|
51 |
qed |
|
52 |
qed |
|
53 |
qed |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
54 |
|
7820 | 55 |
text {* |
56 |
Isar provides several ways to fine-tune the reasoning, avoiding |
|
7874 | 57 |
excessive detail. Several abbreviated language elements are |
7820 | 58 |
available, enabling the writer to express proofs in a more concise |
59 |
way, even without referring to any automated proof tools yet. |
|
7761 | 60 |
|
7820 | 61 |
First of all, proof by assumption may be abbreviated as a single dot. |
10007 | 62 |
*} |
7820 | 63 |
|
10007 | 64 |
lemma "A --> A" |
65 |
proof |
|
66 |
assume A |
|
67 |
show A . |
|
68 |
qed |
|
7820 | 69 |
|
70 |
text {* |
|
71 |
In fact, concluding any (sub-)proof already involves solving any |
|
7860 | 72 |
remaining goals by assumption\footnote{This is not a completely |
7982 | 73 |
trivial operation, as proof by assumption may involve full |
74 |
higher-order unification.}. Thus we may skip the rather vacuous body |
|
75 |
of the above proof as well. |
|
10007 | 76 |
*} |
7820 | 77 |
|
10007 | 78 |
lemma "A --> A" |
79 |
proof |
|
80 |
qed |
|
7820 | 81 |
|
82 |
text {* |
|
83 |
Note that the \isacommand{proof} command refers to the $\idt{rule}$ |
|
84 |
method (without arguments) by default. Thus it implicitly applies a |
|
85 |
single rule, as determined from the syntactic form of the statements |
|
86 |
involved. The \isacommand{by} command abbreviates any proof with |
|
87 |
empty body, so the proof may be further pruned. |
|
10007 | 88 |
*} |
7820 | 89 |
|
10007 | 90 |
lemma "A --> A" |
91 |
by rule |
|
7820 | 92 |
|
93 |
text {* |
|
7874 | 94 |
Proof by a single rule may be abbreviated as double-dot. |
10007 | 95 |
*} |
7820 | 96 |
|
10007 | 97 |
lemma "A --> A" .. |
7820 | 98 |
|
99 |
text {* |
|
100 |
Thus we have arrived at an adequate representation of the proof of a |
|
7860 | 101 |
tautology that holds by a single standard rule.\footnote{Apparently, |
7982 | 102 |
the rule here is implication introduction.} |
10007 | 103 |
*} |
7820 | 104 |
|
105 |
text {* |
|
7874 | 106 |
Let us also reconsider $K$. Its statement is composed of iterated |
7820 | 107 |
connectives. Basic decomposition is by a single rule at a time, |
108 |
which is why our first version above was by nesting two proofs. |
|
109 |
||
110 |
The $\idt{intro}$ proof method repeatedly decomposes a goal's |
|
111 |
conclusion.\footnote{The dual method is $\idt{elim}$, acting on a |
|
112 |
goal's premises.} |
|
10007 | 113 |
*} |
7820 | 114 |
|
10007 | 115 |
lemma "A --> B --> A" |
12387 | 116 |
proof (intro impI) |
10007 | 117 |
assume A |
118 |
show A . |
|
119 |
qed |
|
7820 | 120 |
|
121 |
text {* |
|
122 |
Again, the body may be collapsed. |
|
10007 | 123 |
*} |
7820 | 124 |
|
10007 | 125 |
lemma "A --> B --> A" |
12387 | 126 |
by (intro impI) |
7820 | 127 |
|
128 |
text {* |
|
129 |
Just like $\idt{rule}$, the $\idt{intro}$ and $\idt{elim}$ proof |
|
130 |
methods pick standard structural rules, in case no explicit arguments |
|
131 |
are given. While implicit rules are usually just fine for single |
|
7982 | 132 |
rule application, this may go too far with iteration. Thus in |
7820 | 133 |
practice, $\idt{intro}$ and $\idt{elim}$ would be typically |
134 |
restricted to certain structures by giving a few rules only, e.g.\ |
|
7860 | 135 |
\isacommand{proof}~($\idt{intro}$~\name{impI}~\name{allI}) to strip |
136 |
implications and universal quantifiers. |
|
7820 | 137 |
|
7874 | 138 |
Such well-tuned iterated decomposition of certain structures is the |
139 |
prime application of $\idt{intro}$ and $\idt{elim}$. In contrast, |
|
140 |
terminal steps that solve a goal completely are usually performed by |
|
141 |
actual automated proof methods (such as |
|
7820 | 142 |
\isacommand{by}~$\idt{blast}$). |
10007 | 143 |
*} |
7820 | 144 |
|
145 |
||
10007 | 146 |
subsection {* Variations of backward vs.\ forward reasoning *} |
7820 | 147 |
|
148 |
text {* |
|
149 |
Certainly, any proof may be performed in backward-style only. On the |
|
150 |
other hand, small steps of reasoning are often more naturally |
|
151 |
expressed in forward-style. Isar supports both backward and forward |
|
152 |
reasoning as a first-class concept. In order to demonstrate the |
|
153 |
difference, we consider several proofs of $A \conj B \impl B \conj |
|
154 |
A$. |
|
155 |
||
156 |
The first version is purely backward. |
|
10007 | 157 |
*} |
7001 | 158 |
|
10007 | 159 |
lemma "A & B --> B & A" |
160 |
proof |
|
161 |
assume "A & B" |
|
162 |
show "B & A" |
|
163 |
proof |
|
164 |
show B by (rule conjunct2) |
|
165 |
show A by (rule conjunct1) |
|
166 |
qed |
|
167 |
qed |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
168 |
|
7820 | 169 |
text {* |
170 |
Above, the $\idt{conjunct}_{1/2}$ projection rules had to be named |
|
7982 | 171 |
explicitly, since the goals $B$ and $A$ did not provide any |
172 |
structural clue. This may be avoided using \isacommand{from} to |
|
173 |
focus on $\idt{prems}$ (i.e.\ the $A \conj B$ assumption) as the |
|
174 |
current facts, enabling the use of double-dot proofs. Note that |
|
175 |
\isacommand{from} already does forward-chaining, involving the |
|
176 |
\name{conjE} rule here. |
|
10007 | 177 |
*} |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
178 |
|
10007 | 179 |
lemma "A & B --> B & A" |
180 |
proof |
|
181 |
assume "A & B" |
|
182 |
show "B & A" |
|
183 |
proof |
|
184 |
from prems show B .. |
|
185 |
from prems show A .. |
|
186 |
qed |
|
187 |
qed |
|
7604 | 188 |
|
7820 | 189 |
text {* |
190 |
In the next version, we move the forward step one level upwards. |
|
191 |
Forward-chaining from the most recent facts is indicated by the |
|
192 |
\isacommand{then} command. Thus the proof of $B \conj A$ from $A |
|
193 |
\conj B$ actually becomes an elimination, rather than an |
|
194 |
introduction. The resulting proof structure directly corresponds to |
|
195 |
that of the $\name{conjE}$ rule, including the repeated goal |
|
196 |
proposition that is abbreviated as $\var{thesis}$ below. |
|
10007 | 197 |
*} |
7820 | 198 |
|
10007 | 199 |
lemma "A & B --> B & A" |
200 |
proof |
|
201 |
assume "A & B" |
|
202 |
then show "B & A" |
|
203 |
proof -- {* rule \name{conjE} of $A \conj B$ *} |
|
204 |
assume A B |
|
205 |
show ?thesis .. -- {* rule \name{conjI} of $B \conj A$ *} |
|
206 |
qed |
|
207 |
qed |
|
7820 | 208 |
|
209 |
text {* |
|
7874 | 210 |
In the subsequent version we flatten the structure of the main body |
211 |
by doing forward reasoning all the time. Only the outermost |
|
212 |
decomposition step is left as backward. |
|
10007 | 213 |
*} |
7820 | 214 |
|
10007 | 215 |
lemma "A & B --> B & A" |
216 |
proof |
|
217 |
assume ab: "A & B" |
|
218 |
from ab have a: A .. |
|
219 |
from ab have b: B .. |
|
220 |
from b a show "B & A" .. |
|
221 |
qed |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
222 |
|
7820 | 223 |
text {* |
9659 | 224 |
We can still push forward-reasoning a bit further, even at the risk |
7820 | 225 |
of getting ridiculous. Note that we force the initial proof step to |
7982 | 226 |
do nothing here, by referring to the ``-'' proof method. |
10007 | 227 |
*} |
7820 | 228 |
|
10007 | 229 |
lemma "A & B --> B & A" |
230 |
proof - |
|
231 |
{ |
|
232 |
assume ab: "A & B" |
|
233 |
from ab have a: A .. |
|
234 |
from ab have b: B .. |
|
235 |
from b a have "B & A" .. |
|
236 |
} |
|
237 |
thus ?thesis .. -- {* rule \name{impI} *} |
|
238 |
qed |
|
7820 | 239 |
|
240 |
text {* |
|
241 |
\medskip With these examples we have shifted through a whole range |
|
242 |
from purely backward to purely forward reasoning. Apparently, in the |
|
243 |
extreme ends we get slightly ill-structured proofs, which also |
|
244 |
require much explicit naming of either rules (backward) or local |
|
245 |
facts (forward). |
|
246 |
||
247 |
The general lesson learned here is that good proof style would |
|
248 |
achieve just the \emph{right} balance of top-down backward |
|
7982 | 249 |
decomposition, and bottom-up forward composition. In general, there |
7820 | 250 |
is no single best way to arrange some pieces of formal reasoning, of |
251 |
course. Depending on the actual applications, the intended audience |
|
7874 | 252 |
etc., rules (and methods) on the one hand vs.\ facts on the other |
253 |
hand have to be emphasized in an appropriate way. This requires the |
|
254 |
proof writer to develop good taste, and some practice, of course. |
|
10007 | 255 |
*} |
7820 | 256 |
|
257 |
text {* |
|
258 |
For our example the most appropriate way of reasoning is probably the |
|
259 |
middle one, with conjunction introduction done after elimination. |
|
260 |
This reads even more concisely using \isacommand{thus}, which |
|
261 |
abbreviates \isacommand{then}~\isacommand{show}.\footnote{In the same |
|
262 |
vein, \isacommand{hence} abbreviates |
|
263 |
\isacommand{then}~\isacommand{have}.} |
|
10007 | 264 |
*} |
7820 | 265 |
|
10007 | 266 |
lemma "A & B --> B & A" |
267 |
proof |
|
268 |
assume "A & B" |
|
269 |
thus "B & A" |
|
270 |
proof |
|
271 |
assume A B |
|
272 |
show ?thesis .. |
|
273 |
qed |
|
274 |
qed |
|
7820 | 275 |
|
276 |
||
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
277 |
|
10007 | 278 |
subsection {* A few examples from ``Introduction to Isabelle'' *} |
7001 | 279 |
|
7820 | 280 |
text {* |
281 |
We rephrase some of the basic reasoning examples of |
|
7982 | 282 |
\cite{isabelle-intro}, using HOL rather than FOL. |
10007 | 283 |
*} |
7820 | 284 |
|
10007 | 285 |
subsubsection {* A propositional proof *} |
7833 | 286 |
|
287 |
text {* |
|
288 |
We consider the proposition $P \disj P \impl P$. The proof below |
|
289 |
involves forward-chaining from $P \disj P$, followed by an explicit |
|
290 |
case-analysis on the two \emph{identical} cases. |
|
10007 | 291 |
*} |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
292 |
|
10007 | 293 |
lemma "P | P --> P" |
294 |
proof |
|
295 |
assume "P | P" |
|
296 |
thus P |
|
7833 | 297 |
proof -- {* |
298 |
rule \name{disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$} |
|
10007 | 299 |
*} |
300 |
assume P show P . |
|
301 |
next |
|
302 |
assume P show P . |
|
303 |
qed |
|
304 |
qed |
|
7833 | 305 |
|
306 |
text {* |
|
307 |
Case splits are \emph{not} hardwired into the Isar language as a |
|
308 |
special feature. The \isacommand{next} command used to separate the |
|
309 |
cases above is just a short form of managing block structure. |
|
310 |
||
311 |
\medskip In general, applying proof methods may split up a goal into |
|
312 |
separate ``cases'', i.e.\ new subgoals with individual local |
|
313 |
assumptions. The corresponding proof text typically mimics this by |
|
314 |
establishing results in appropriate contexts, separated by blocks. |
|
315 |
||
7860 | 316 |
In order to avoid too much explicit parentheses, the Isar system |
7833 | 317 |
implicitly opens an additional block for any new goal, the |
318 |
\isacommand{next} statement then closes one block level, opening a |
|
7982 | 319 |
new one. The resulting behavior is what one would expect from |
320 |
separating cases, only that it is more flexible. E.g.\ an induction |
|
7833 | 321 |
base case (which does not introduce local assumptions) would |
322 |
\emph{not} require \isacommand{next} to separate the subsequent step |
|
323 |
case. |
|
324 |
||
325 |
\medskip In our example the situation is even simpler, since the two |
|
7874 | 326 |
cases actually coincide. Consequently the proof may be rephrased as |
327 |
follows. |
|
10007 | 328 |
*} |
7833 | 329 |
|
10007 | 330 |
lemma "P | P --> P" |
331 |
proof |
|
332 |
assume "P | P" |
|
333 |
thus P |
|
334 |
proof |
|
335 |
assume P |
|
336 |
show P . |
|
337 |
show P . |
|
338 |
qed |
|
339 |
qed |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
340 |
|
7833 | 341 |
text {* |
342 |
Again, the rather vacuous body of the proof may be collapsed. Thus |
|
7860 | 343 |
the case analysis degenerates into two assumption steps, which are |
344 |
implicitly performed when concluding the single rule step of the |
|
345 |
double-dot proof as follows. |
|
10007 | 346 |
*} |
7833 | 347 |
|
10007 | 348 |
lemma "P | P --> P" |
349 |
proof |
|
350 |
assume "P | P" |
|
351 |
thus P .. |
|
352 |
qed |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
353 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
354 |
|
10007 | 355 |
subsubsection {* A quantifier proof *} |
7833 | 356 |
|
357 |
text {* |
|
358 |
To illustrate quantifier reasoning, let us prove $(\ex x P \ap (f \ap |
|
359 |
x)) \impl (\ex x P \ap x)$. Informally, this holds because any $a$ |
|
360 |
with $P \ap (f \ap a)$ may be taken as a witness for the second |
|
361 |
existential statement. |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
362 |
|
7833 | 363 |
The first proof is rather verbose, exhibiting quite a lot of |
364 |
(redundant) detail. It gives explicit rules, even with some |
|
365 |
instantiation. Furthermore, we encounter two new language elements: |
|
366 |
the \isacommand{fix} command augments the context by some new |
|
367 |
``arbitrary, but fixed'' element; the \isacommand{is} annotation |
|
368 |
binds term abbreviations by higher-order pattern matching. |
|
10007 | 369 |
*} |
7833 | 370 |
|
10636 | 371 |
lemma "(EX x. P (f x)) --> (EX y. P y)" |
10007 | 372 |
proof |
373 |
assume "EX x. P (f x)" |
|
10636 | 374 |
thus "EX y. P y" |
7833 | 375 |
proof (rule exE) -- {* |
376 |
rule \name{exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$} |
|
10007 | 377 |
*} |
378 |
fix a |
|
379 |
assume "P (f a)" (is "P ?witness") |
|
380 |
show ?thesis by (rule exI [of P ?witness]) |
|
381 |
qed |
|
382 |
qed |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
383 |
|
7833 | 384 |
text {* |
7982 | 385 |
While explicit rule instantiation may occasionally improve |
386 |
readability of certain aspects of reasoning, it is usually quite |
|
7833 | 387 |
redundant. Above, the basic proof outline gives already enough |
388 |
structural clues for the system to infer both the rules and their |
|
389 |
instances (by higher-order unification). Thus we may as well prune |
|
390 |
the text as follows. |
|
10007 | 391 |
*} |
7833 | 392 |
|
10636 | 393 |
lemma "(EX x. P (f x)) --> (EX y. P y)" |
10007 | 394 |
proof |
395 |
assume "EX x. P (f x)" |
|
10636 | 396 |
thus "EX y. P y" |
10007 | 397 |
proof |
398 |
fix a |
|
399 |
assume "P (f a)" |
|
400 |
show ?thesis .. |
|
401 |
qed |
|
402 |
qed |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
403 |
|
9477 | 404 |
text {* |
405 |
Explicit $\exists$-elimination as seen above can become quite |
|
406 |
cumbersome in practice. The derived Isar language element |
|
407 |
``\isakeyword{obtain}'' provides a more handsome way to do |
|
408 |
generalized existence reasoning. |
|
10007 | 409 |
*} |
9477 | 410 |
|
10636 | 411 |
lemma "(EX x. P (f x)) --> (EX y. P y)" |
10007 | 412 |
proof |
413 |
assume "EX x. P (f x)" |
|
10636 | 414 |
then obtain a where "P (f a)" .. |
415 |
thus "EX y. P y" .. |
|
10007 | 416 |
qed |
9477 | 417 |
|
418 |
text {* |
|
419 |
Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and |
|
420 |
\isakeyword{assume} together with a soundness proof of the |
|
421 |
elimination involved. Thus it behaves similar to any other forward |
|
422 |
proof element. Also note that due to the nature of general existence |
|
423 |
reasoning involved here, any result exported from the context of an |
|
424 |
\isakeyword{obtain} statement may \emph{not} refer to the parameters |
|
425 |
introduced there. |
|
10007 | 426 |
*} |
9477 | 427 |
|
428 |
||
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
429 |
|
10007 | 430 |
subsubsection {* Deriving rules in Isabelle *} |
7001 | 431 |
|
7833 | 432 |
text {* |
7982 | 433 |
We derive the conjunction elimination rule from the corresponding |
434 |
projections. The proof is quite straight-forward, since |
|
435 |
Isabelle/Isar supports non-atomic goals and assumptions fully |
|
436 |
transparently. |
|
10007 | 437 |
*} |
7001 | 438 |
|
10007 | 439 |
theorem conjE: "A & B ==> (A ==> B ==> C) ==> C" |
440 |
proof - |
|
441 |
assume "A & B" |
|
442 |
assume r: "A ==> B ==> C" |
|
443 |
show C |
|
444 |
proof (rule r) |
|
445 |
show A by (rule conjunct1) |
|
446 |
show B by (rule conjunct2) |
|
447 |
qed |
|
448 |
qed |
|
7001 | 449 |
|
7860 | 450 |
text {* |
451 |
Note that classic Isabelle handles higher rules in a slightly |
|
452 |
different way. The tactic script as given in \cite{isabelle-intro} |
|
453 |
for the same example of \name{conjE} depends on the primitive |
|
454 |
\texttt{goal} command to decompose the rule into premises and |
|
7982 | 455 |
conclusion. The actual result would then emerge by discharging of |
7860 | 456 |
the context at \texttt{qed} time. |
10007 | 457 |
*} |
7860 | 458 |
|
10007 | 459 |
end |