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