1 (*<*)theory Logic imports Main begin(*>*) |
|
2 |
|
3 section{*Logic \label{sec:Logic}*} |
|
4 |
|
5 subsection{*Propositional logic*} |
|
6 |
|
7 subsubsection{*Introduction rules*} |
|
8 |
|
9 text{* We start with a really trivial toy proof to introduce the basic |
|
10 features of structured proofs. *} |
|
11 lemma "A \<longrightarrow> A" |
|
12 proof (rule impI) |
|
13 assume a: "A" |
|
14 show "A" by(rule a) |
|
15 qed |
|
16 text{*\noindent |
|
17 The operational reading: the \isakeyword{assume}-\isakeyword{show} |
|
18 block proves @{prop"A \<Longrightarrow> A"} (@{term a} is a degenerate rule (no |
|
19 assumptions) that proves @{term A} outright), which rule |
|
20 @{thm[source]impI} (@{thm impI}) turns into the desired @{prop"A \<longrightarrow> |
|
21 A"}. However, this text is much too detailed for comfort. Therefore |
|
22 Isar implements the following principle: \begin{quote}\em Command |
|
23 \isakeyword{proof} automatically tries to select an introduction rule |
|
24 based on the goal and a predefined list of rules. \end{quote} Here |
|
25 @{thm[source]impI} is applied automatically: *} |
|
26 |
|
27 lemma "A \<longrightarrow> A" |
|
28 proof |
|
29 assume a: A |
|
30 show A by(rule a) |
|
31 qed |
|
32 |
|
33 text{*\noindent As you see above, single-identifier formulae such as @{term A} |
|
34 need not be enclosed in double quotes. However, we will continue to do so for |
|
35 uniformity. |
|
36 |
|
37 Instead of applying fact @{text a} via the @{text rule} method, we can |
|
38 also push it directly onto our goal. The proof is then immediate, |
|
39 which is formally written as ``.'' in Isar: *} |
|
40 lemma "A \<longrightarrow> A" |
|
41 proof |
|
42 assume a: "A" |
|
43 from a show "A" . |
|
44 qed |
|
45 |
|
46 text{* We can also push several facts towards a goal, and put another |
|
47 rule in between to establish some result that is one step further |
|
48 removed. We illustrate this by introducing a trivial conjunction: *} |
|
49 lemma "A \<longrightarrow> A \<and> A" |
|
50 proof |
|
51 assume a: "A" |
|
52 from a and a show "A \<and> A" by(rule conjI) |
|
53 qed |
|
54 text{*\noindent Rule @{thm[source]conjI} is of course @{thm conjI}. |
|
55 |
|
56 Proofs of the form \isakeyword{by}@{text"(rule"}~\emph{name}@{text")"} |
|
57 can be abbreviated to ``..'' if \emph{name} refers to one of the |
|
58 predefined introduction rules (or elimination rules, see below): *} |
|
59 |
|
60 lemma "A \<longrightarrow> A \<and> A" |
|
61 proof |
|
62 assume a: "A" |
|
63 from a and a show "A \<and> A" .. |
|
64 qed |
|
65 text{*\noindent |
|
66 This is what happens: first the matching introduction rule @{thm[source]conjI} |
|
67 is applied (first ``.''), the remaining problem is solved immediately (second ``.''). *} |
|
68 |
|
69 subsubsection{*Elimination rules*} |
|
70 |
|
71 text{*A typical elimination rule is @{thm[source]conjE}, $\land$-elimination: |
|
72 @{thm[display,indent=5]conjE} In the following proof it is applied |
|
73 by hand, after its first (\emph{major}) premise has been eliminated via |
|
74 @{text"[OF ab]"}: *} |
|
75 lemma "A \<and> B \<longrightarrow> B \<and> A" |
|
76 proof |
|
77 assume ab: "A \<and> B" |
|
78 show "B \<and> A" |
|
79 proof (rule conjE[OF ab]) -- {*@{text"conjE[OF ab]"}: @{thm conjE[OF ab]} *} |
|
80 assume a: "A" and b: "B" |
|
81 from b and a show ?thesis .. |
|
82 qed |
|
83 qed |
|
84 text{*\noindent Note that the term @{text"?thesis"} always stands for the |
|
85 ``current goal'', i.e.\ the enclosing \isakeyword{show} (or |
|
86 \isakeyword{have}) statement. |
|
87 |
|
88 This is too much proof text. Elimination rules should be selected |
|
89 automatically based on their major premise, the formula or rather connective |
|
90 to be eliminated. In Isar they are triggered by facts being fed |
|
91 \emph{into} a proof. Syntax: |
|
92 \begin{center} |
|
93 \isakeyword{from} \emph{fact} \isakeyword{show} \emph{proposition} \emph{proof} |
|
94 \end{center} |
|
95 where \emph{fact} stands for the name of a previously proved |
|
96 proposition, e.g.\ an assumption, an intermediate result or some global |
|
97 theorem, which may also be modified with @{text OF} etc. |
|
98 The \emph{fact} is ``piped'' into the \emph{proof}, which can deal with it |
|
99 how it chooses. If the \emph{proof} starts with a plain \isakeyword{proof}, |
|
100 an elimination rule (from a predefined list) is applied |
|
101 whose first premise is solved by the \emph{fact}. Thus the proof above |
|
102 is equivalent to the following one: *} |
|
103 |
|
104 lemma "A \<and> B \<longrightarrow> B \<and> A" |
|
105 proof |
|
106 assume ab: "A \<and> B" |
|
107 from ab show "B \<and> A" |
|
108 proof |
|
109 assume a: "A" and b: "B" |
|
110 from b and a show ?thesis .. |
|
111 qed |
|
112 qed |
|
113 |
|
114 text{* Now we come to a second important principle: |
|
115 \begin{quote}\em |
|
116 Try to arrange the sequence of propositions in a UNIX-like pipe, |
|
117 such that the proof of each proposition builds on the previous proposition. |
|
118 \end{quote} |
|
119 The previous proposition can be referred to via the fact @{text this}. |
|
120 This greatly reduces the need for explicit naming of propositions. We also |
|
121 rearrange the additional inner assumptions into proper order for immediate use: |
|
122 *} |
|
123 lemma "A \<and> B \<longrightarrow> B \<and> A" |
|
124 proof |
|
125 assume "A \<and> B" |
|
126 from this show "B \<and> A" |
|
127 proof |
|
128 assume "B" "A" |
|
129 from this show ?thesis .. |
|
130 qed |
|
131 qed |
|
132 |
|
133 text{*\noindent Because of the frequency of \isakeyword{from}~@{text |
|
134 this}, Isar provides two abbreviations: |
|
135 \begin{center} |
|
136 \begin{tabular}{r@ {\quad=\quad}l} |
|
137 \isakeyword{then} & \isakeyword{from} @{text this} \\ |
|
138 \isakeyword{thus} & \isakeyword{then} \isakeyword{show} |
|
139 \end{tabular} |
|
140 \end{center} |
|
141 |
|
142 Here is an alternative proof that operates purely by forward reasoning: *} |
|
143 lemma "A \<and> B \<longrightarrow> B \<and> A" |
|
144 proof |
|
145 assume ab: "A \<and> B" |
|
146 from ab have a: "A" .. |
|
147 from ab have b: "B" .. |
|
148 from b a show "B \<and> A" .. |
|
149 qed |
|
150 |
|
151 text{*\noindent It is worth examining this text in detail because it |
|
152 exhibits a number of new concepts. For a start, it is the first time |
|
153 we have proved intermediate propositions (\isakeyword{have}) on the |
|
154 way to the final \isakeyword{show}. This is the norm in nontrivial |
|
155 proofs where one cannot bridge the gap between the assumptions and the |
|
156 conclusion in one step. To understand how the proof works we need to |
|
157 explain more Isar details: |
|
158 \begin{itemize} |
|
159 \item |
|
160 Method @{text rule} can be given a list of rules, in which case |
|
161 @{text"(rule"}~\textit{rules}@{text")"} applies the first matching |
|
162 rule in the list \textit{rules}. |
|
163 \item Command \isakeyword{from} can be |
|
164 followed by any number of facts. Given \isakeyword{from}~@{text |
|
165 f}$_1$~\dots~@{text f}$_n$, the proof step |
|
166 @{text"(rule"}~\textit{rules}@{text")"} following a \isakeyword{have} |
|
167 or \isakeyword{show} searches \textit{rules} for a rule whose first |
|
168 $n$ premises can be proved by @{text f}$_1$~\dots~@{text f}$_n$ in the |
|
169 given order. |
|
170 \item ``..'' is short for |
|
171 @{text"by(rule"}~\textit{elim-rules intro-rules}@{text")"}\footnote{or |
|
172 merely @{text"(rule"}~\textit{intro-rules}@{text")"} if there are no facts |
|
173 fed into the proof}, where \textit{elim-rules} and \textit{intro-rules} |
|
174 are the predefined elimination and introduction rule. Thus |
|
175 elimination rules are tried first (if there are incoming facts). |
|
176 \end{itemize} |
|
177 Hence in the above proof both \isakeyword{have}s are proved via |
|
178 @{thm[source]conjE} triggered by \isakeyword{from}~@{text ab} whereas |
|
179 in the \isakeyword{show} step no elimination rule is applicable and |
|
180 the proof succeeds with @{thm[source]conjI}. The latter would fail had |
|
181 we written \isakeyword{from}~@{text"a b"} instead of |
|
182 \isakeyword{from}~@{text"b a"}. |
|
183 |
|
184 A plain \isakeyword{proof} with no argument is short for |
|
185 \isakeyword{proof}~@{text"(rule"}~\textit{elim-rules intro-rules}@{text")"}\footnotemark[1]. |
|
186 This means that the matching rule is selected by the incoming facts and the goal exactly as just explained. |
|
187 |
|
188 Although we have only seen a few introduction and elimination rules so |
|
189 far, Isar's predefined rules include all the usual natural deduction |
|
190 rules. We conclude our exposition of propositional logic with an extended |
|
191 example --- which rules are used implicitly where? *} |
|
192 lemma "\<not> (A \<and> B) \<longrightarrow> \<not> A \<or> \<not> B" |
|
193 proof |
|
194 assume n: "\<not> (A \<and> B)" |
|
195 show "\<not> A \<or> \<not> B" |
|
196 proof (rule ccontr) |
|
197 assume nn: "\<not> (\<not> A \<or> \<not> B)" |
|
198 have "\<not> A" |
|
199 proof |
|
200 assume a: "A" |
|
201 have "\<not> B" |
|
202 proof |
|
203 assume b: "B" |
|
204 from a and b have "A \<and> B" .. |
|
205 with n show False .. |
|
206 qed |
|
207 hence "\<not> A \<or> \<not> B" .. |
|
208 with nn show False .. |
|
209 qed |
|
210 hence "\<not> A \<or> \<not> B" .. |
|
211 with nn show False .. |
|
212 qed |
|
213 qed |
|
214 text{*\noindent |
|
215 Rule @{thm[source]ccontr} (``classical contradiction'') is |
|
216 @{thm ccontr[no_vars]}. |
|
217 Apart from demonstrating the strangeness of classical |
|
218 arguments by contradiction, this example also introduces two new |
|
219 abbreviations: |
|
220 \begin{center} |
|
221 \begin{tabular}{l@ {\quad=\quad}l} |
|
222 \isakeyword{hence} & \isakeyword{then} \isakeyword{have} \\ |
|
223 \isakeyword{with}~\emph{facts} & |
|
224 \isakeyword{from}~\emph{facts} @{text this} |
|
225 \end{tabular} |
|
226 \end{center} |
|
227 *} |
|
228 |
|
229 |
|
230 subsection{*Avoiding duplication*} |
|
231 |
|
232 text{* So far our examples have been a bit unnatural: normally we want to |
|
233 prove rules expressed with @{text"\<Longrightarrow>"}, not @{text"\<longrightarrow>"}. Here is an example: |
|
234 *} |
|
235 lemma "A \<and> B \<Longrightarrow> B \<and> A" |
|
236 proof |
|
237 assume "A \<and> B" thus "B" .. |
|
238 next |
|
239 assume "A \<and> B" thus "A" .. |
|
240 qed |
|
241 text{*\noindent The \isakeyword{proof} always works on the conclusion, |
|
242 @{prop"B \<and> A"} in our case, thus selecting $\land$-introduction. Hence |
|
243 we must show @{prop B} and @{prop A}; both are proved by |
|
244 $\land$-elimination and the proofs are separated by \isakeyword{next}: |
|
245 \begin{description} |
|
246 \item[\isakeyword{next}] deals with multiple subgoals. For example, |
|
247 when showing @{term"A \<and> B"} we need to show both @{term A} and @{term |
|
248 B}. Each subgoal is proved separately, in \emph{any} order. The |
|
249 individual proofs are separated by \isakeyword{next}. \footnote{Each |
|
250 \isakeyword{show} must prove one of the pending subgoals. If a |
|
251 \isakeyword{show} matches multiple subgoals, e.g.\ if the subgoals |
|
252 contain ?-variables, the first one is proved. Thus the order in which |
|
253 the subgoals are proved can matter --- see |
|
254 \S\ref{sec:CaseDistinction} for an example.} |
|
255 |
|
256 Strictly speaking \isakeyword{next} is only required if the subgoals |
|
257 are proved in different assumption contexts which need to be |
|
258 separated, which is not the case above. For clarity we |
|
259 have employed \isakeyword{next} anyway and will continue to do so. |
|
260 \end{description} |
|
261 |
|
262 This is all very well as long as formulae are small. Let us now look at some |
|
263 devices to avoid repeating (possibly large) formulae. A very general method |
|
264 is pattern matching: *} |
|
265 |
|
266 lemma "large_A \<and> large_B \<Longrightarrow> large_B \<and> large_A" |
|
267 (is "?AB \<Longrightarrow> ?B \<and> ?A") |
|
268 proof |
|
269 assume "?AB" thus "?B" .. |
|
270 next |
|
271 assume "?AB" thus "?A" .. |
|
272 qed |
|
273 text{*\noindent Any formula may be followed by |
|
274 @{text"("}\isakeyword{is}~\emph{pattern}@{text")"} which causes the pattern |
|
275 to be matched against the formula, instantiating the @{text"?"}-variables in |
|
276 the pattern. Subsequent uses of these variables in other terms causes |
|
277 them to be replaced by the terms they stand for. |
|
278 |
|
279 We can simplify things even more by stating the theorem by means of the |
|
280 \isakeyword{assumes} and \isakeyword{shows} elements which allow direct |
|
281 naming of assumptions: *} |
|
282 |
|
283 lemma assumes ab: "large_A \<and> large_B" |
|
284 shows "large_B \<and> large_A" (is "?B \<and> ?A") |
|
285 proof |
|
286 from ab show "?B" .. |
|
287 next |
|
288 from ab show "?A" .. |
|
289 qed |
|
290 text{*\noindent Note the difference between @{text ?AB}, a term, and |
|
291 @{text ab}, a fact. |
|
292 |
|
293 Finally we want to start the proof with $\land$-elimination so we |
|
294 don't have to perform it twice, as above. Here is a slick way to |
|
295 achieve this: *} |
|
296 |
|
297 lemma assumes ab: "large_A \<and> large_B" |
|
298 shows "large_B \<and> large_A" (is "?B \<and> ?A") |
|
299 using ab |
|
300 proof |
|
301 assume "?B" "?A" thus ?thesis .. |
|
302 qed |
|
303 text{*\noindent Command \isakeyword{using} can appear before a proof |
|
304 and adds further facts to those piped into the proof. Here @{text ab} |
|
305 is the only such fact and it triggers $\land$-elimination. Another |
|
306 frequent idiom is as follows: |
|
307 \begin{center} |
|
308 \isakeyword{from} \emph{major-facts}~ |
|
309 \isakeyword{show} \emph{proposition}~ |
|
310 \isakeyword{using} \emph{minor-facts}~ |
|
311 \emph{proof} |
|
312 \end{center} |
|
313 |
|
314 Sometimes it is necessary to suppress the implicit application of rules in a |
|
315 \isakeyword{proof}. For example \isakeyword{show(s)}~@{prop[source]"P \<or> Q"} |
|
316 would trigger $\lor$-introduction, requiring us to prove @{prop P}, which may |
|
317 not be what we had in mind. |
|
318 A simple ``@{text"-"}'' prevents this \emph{faux pas}: *} |
|
319 |
|
320 lemma assumes ab: "A \<or> B" shows "B \<or> A" |
|
321 proof - |
|
322 from ab show ?thesis |
|
323 proof |
|
324 assume A thus ?thesis .. |
|
325 next |
|
326 assume B thus ?thesis .. |
|
327 qed |
|
328 qed |
|
329 text{*\noindent Alternatively one can feed @{prop"A \<or> B"} directly |
|
330 into the proof, thus triggering the elimination rule: *} |
|
331 lemma assumes ab: "A \<or> B" shows "B \<or> A" |
|
332 using ab |
|
333 proof |
|
334 assume A thus ?thesis .. |
|
335 next |
|
336 assume B thus ?thesis .. |
|
337 qed |
|
338 text{* \noindent Remember that eliminations have priority over |
|
339 introductions. |
|
340 |
|
341 \subsection{Avoiding names} |
|
342 |
|
343 Too many names can easily clutter a proof. We already learned |
|
344 about @{text this} as a means of avoiding explicit names. Another |
|
345 handy device is to refer to a fact not by name but by contents: for |
|
346 example, writing @{text "`A \<or> B`"} (enclosing the formula in back quotes) |
|
347 refers to the fact @{text"A \<or> B"} |
|
348 without the need to name it. Here is a simple example, a revised version |
|
349 of the previous proof *} |
|
350 |
|
351 lemma assumes "A \<or> B" shows "B \<or> A" |
|
352 using `A \<or> B` |
|
353 (*<*)oops(*>*) |
|
354 text{*\noindent which continues as before. |
|
355 |
|
356 Clearly, this device of quoting facts by contents is only advisable |
|
357 for small formulae. In such cases it is superior to naming because the |
|
358 reader immediately sees what the fact is without needing to search for |
|
359 it in the preceding proof text. |
|
360 |
|
361 The assumptions of a lemma can also be referred to via their |
|
362 predefined name @{text assms}. Hence the @{text"`A \<or> B`"} in the |
|
363 previous proof can also be replaced by @{text assms}. Note that @{text |
|
364 assms} refers to the list of \emph{all} assumptions. To pick out a |
|
365 specific one, say the second, write @{text"assms(2)"}. |
|
366 |
|
367 This indexing notation $name(.)$ works for any $name$ that stands for |
|
368 a list of facts, for example $f$@{text".simps"}, the equations of the |
|
369 recursively defined function $f$. You may also select sublists by writing |
|
370 $name(2-3)$. |
|
371 |
|
372 Above we recommended the UNIX-pipe model (i.e. @{text this}) to avoid |
|
373 the need to name propositions. But frequently we needed to feed more |
|
374 than one previously derived fact into a proof step. Then the UNIX-pipe |
|
375 model appears to break down and we need to name the different facts to |
|
376 refer to them. But this can be avoided: *} |
|
377 lemma assumes "A \<and> B" shows "B \<and> A" |
|
378 proof - |
|
379 from `A \<and> B` have "B" .. |
|
380 moreover |
|
381 from `A \<and> B` have "A" .. |
|
382 ultimately show "B \<and> A" .. |
|
383 qed |
|
384 text{*\noindent You can combine any number of facts @{term A1} \dots\ @{term |
|
385 An} into a sequence by separating their proofs with |
|
386 \isakeyword{moreover}. After the final fact, \isakeyword{ultimately} stands |
|
387 for \isakeyword{from}~@{term A1}~\dots~@{term An}. This avoids having to |
|
388 introduce names for all of the sequence elements. |
|
389 |
|
390 |
|
391 \subsection{Predicate calculus} |
|
392 |
|
393 Command \isakeyword{fix} introduces new local variables into a |
|
394 proof. The pair \isakeyword{fix}-\isakeyword{show} corresponds to @{text"\<And>"} |
|
395 (the universal quantifier at the |
|
396 meta-level) just like \isakeyword{assume}-\isakeyword{show} corresponds to |
|
397 @{text"\<Longrightarrow>"}. Here is a sample proof, annotated with the rules that are |
|
398 applied implicitly: *} |
|
399 lemma assumes P: "\<forall>x. P x" shows "\<forall>x. P(f x)" |
|
400 proof --"@{thm[source]allI}: @{thm allI}" |
|
401 fix a |
|
402 from P show "P(f a)" .. --"@{thm[source]allE}: @{thm allE}" |
|
403 qed |
|
404 text{*\noindent Note that in the proof we have chosen to call the bound |
|
405 variable @{term a} instead of @{term x} merely to show that the choice of |
|
406 local names is irrelevant. |
|
407 |
|
408 Next we look at @{text"\<exists>"} which is a bit more tricky. |
|
409 *} |
|
410 |
|
411 lemma assumes Pf: "\<exists>x. P(f x)" shows "\<exists>y. P y" |
|
412 proof - |
|
413 from Pf show ?thesis |
|
414 proof -- "@{thm[source]exE}: @{thm exE}" |
|
415 fix x |
|
416 assume "P(f x)" |
|
417 thus ?thesis .. -- "@{thm[source]exI}: @{thm exI}" |
|
418 qed |
|
419 qed |
|
420 text{*\noindent Explicit $\exists$-elimination as seen above can become |
|
421 cumbersome in practice. The derived Isar language element |
|
422 \isakeyword{obtain} provides a more appealing form of generalised |
|
423 existence reasoning: *} |
|
424 |
|
425 lemma assumes Pf: "\<exists>x. P(f x)" shows "\<exists>y. P y" |
|
426 proof - |
|
427 from Pf obtain x where "P(f x)" .. |
|
428 thus "\<exists>y. P y" .. |
|
429 qed |
|
430 text{*\noindent Note how the proof text follows the usual mathematical style |
|
431 of concluding $P(x)$ from $\exists x. P(x)$, while carefully introducing $x$ |
|
432 as a new local variable. Technically, \isakeyword{obtain} is similar to |
|
433 \isakeyword{fix} and \isakeyword{assume} together with a soundness proof of |
|
434 the elimination involved. |
|
435 |
|
436 Here is a proof of a well known tautology. |
|
437 Which rule is used where? *} |
|
438 |
|
439 lemma assumes ex: "\<exists>x. \<forall>y. P x y" shows "\<forall>y. \<exists>x. P x y" |
|
440 proof |
|
441 fix y |
|
442 from ex obtain x where "\<forall>y. P x y" .. |
|
443 hence "P x y" .. |
|
444 thus "\<exists>x. P x y" .. |
|
445 qed |
|
446 |
|
447 subsection{*Making bigger steps*} |
|
448 |
|
449 text{* So far we have confined ourselves to single step proofs. Of course |
|
450 powerful automatic methods can be used just as well. Here is an example, |
|
451 Cantor's theorem that there is no surjective function from a set to its |
|
452 powerset: *} |
|
453 theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)" |
|
454 proof |
|
455 let ?S = "{x. x \<notin> f x}" |
|
456 show "?S \<notin> range f" |
|
457 proof |
|
458 assume "?S \<in> range f" |
|
459 then obtain y where "?S = f y" .. |
|
460 show False |
|
461 proof cases |
|
462 assume "y \<in> ?S" |
|
463 with `?S = f y` show False by blast |
|
464 next |
|
465 assume "y \<notin> ?S" |
|
466 with `?S = f y` show False by blast |
|
467 qed |
|
468 qed |
|
469 qed |
|
470 text{*\noindent |
|
471 For a start, the example demonstrates two new constructs: |
|
472 \begin{itemize} |
|
473 \item \isakeyword{let} introduces an abbreviation for a term, in our case |
|
474 the witness for the claim. |
|
475 \item Proof by @{text"cases"} starts a proof by cases. Note that it remains |
|
476 implicit what the two cases are: it is merely expected that the two subproofs |
|
477 prove @{text"P \<Longrightarrow> ?thesis"} and @{text"\<not>P \<Longrightarrow> ?thesis"} (in that order) |
|
478 for some @{term P}. |
|
479 \end{itemize} |
|
480 If you wonder how to \isakeyword{obtain} @{term y}: |
|
481 via the predefined elimination rule @{thm rangeE[no_vars]}. |
|
482 |
|
483 Method @{text blast} is used because the contradiction does not follow easily |
|
484 by just a single rule. If you find the proof too cryptic for human |
|
485 consumption, here is a more detailed version; the beginning up to |
|
486 \isakeyword{obtain} stays unchanged. *} |
|
487 |
|
488 theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)" |
|
489 proof |
|
490 let ?S = "{x. x \<notin> f x}" |
|
491 show "?S \<notin> range f" |
|
492 proof |
|
493 assume "?S \<in> range f" |
|
494 then obtain y where "?S = f y" .. |
|
495 show False |
|
496 proof cases |
|
497 assume "y \<in> ?S" |
|
498 hence "y \<notin> f y" by simp |
|
499 hence "y \<notin> ?S" by(simp add: `?S = f y`) |
|
500 with `y \<in> ?S` show False by contradiction |
|
501 next |
|
502 assume "y \<notin> ?S" |
|
503 hence "y \<in> f y" by simp |
|
504 hence "y \<in> ?S" by(simp add: `?S = f y`) |
|
505 with `y \<notin> ?S` show False by contradiction |
|
506 qed |
|
507 qed |
|
508 qed |
|
509 text{*\noindent Method @{text contradiction} succeeds if both $P$ and |
|
510 $\neg P$ are among the assumptions and the facts fed into that step, in any order. |
|
511 |
|
512 As it happens, Cantor's theorem can be proved automatically by best-first |
|
513 search. Depth-first search would diverge, but best-first search successfully |
|
514 navigates through the large search space: |
|
515 *} |
|
516 |
|
517 theorem "\<exists>S. S \<notin> range (f :: 'a \<Rightarrow> 'a set)" |
|
518 by best |
|
519 (* Of course this only works in the context of HOL's carefully |
|
520 constructed introduction and elimination rules for set theory.*) |
|
521 |
|
522 subsection{*Raw proof blocks*} |
|
523 |
|
524 text{* Although we have shown how to employ powerful automatic methods like |
|
525 @{text blast} to achieve bigger proof steps, there may still be the |
|
526 tendency to use the default introduction and elimination rules to |
|
527 decompose goals and facts. This can lead to very tedious proofs: |
|
528 *} |
|
529 lemma "\<forall>x y. A x y \<and> B x y \<longrightarrow> C x y" |
|
530 proof |
|
531 fix x show "\<forall>y. A x y \<and> B x y \<longrightarrow> C x y" |
|
532 proof |
|
533 fix y show "A x y \<and> B x y \<longrightarrow> C x y" |
|
534 proof |
|
535 assume "A x y \<and> B x y" |
|
536 show "C x y" sorry |
|
537 qed |
|
538 qed |
|
539 qed |
|
540 text{*\noindent Since we are only interested in the decomposition and not the |
|
541 actual proof, the latter has been replaced by |
|
542 \isakeyword{sorry}. Command \isakeyword{sorry} proves anything but is |
|
543 only allowed in quick and dirty mode, the default interactive mode. It |
|
544 is very convenient for top down proof development. |
|
545 |
|
546 Luckily we can avoid this step by step decomposition very easily: *} |
|
547 |
|
548 lemma "\<forall>x y. A x y \<and> B x y \<longrightarrow> C x y" |
|
549 proof - |
|
550 have "\<And>x y. \<lbrakk> A x y; B x y \<rbrakk> \<Longrightarrow> C x y" |
|
551 proof - |
|
552 fix x y assume "A x y" "B x y" |
|
553 show "C x y" sorry |
|
554 qed |
|
555 thus ?thesis by blast |
|
556 qed |
|
557 |
|
558 text{*\noindent |
|
559 This can be simplified further by \emph{raw proof blocks}, i.e.\ |
|
560 proofs enclosed in braces: *} |
|
561 |
|
562 lemma "\<forall>x y. A x y \<and> B x y \<longrightarrow> C x y" |
|
563 proof - |
|
564 { fix x y assume "A x y" "B x y" |
|
565 have "C x y" sorry } |
|
566 thus ?thesis by blast |
|
567 qed |
|
568 |
|
569 text{*\noindent The result of the raw proof block is the same theorem |
|
570 as above, namely @{prop"\<And>x y. \<lbrakk> A x y; B x y \<rbrakk> \<Longrightarrow> C x y"}. Raw |
|
571 proof blocks are like ordinary proofs except that they do not prove |
|
572 some explicitly stated property but that the property emerges directly |
|
573 out of the \isakeyword{fixe}s, \isakeyword{assume}s and |
|
574 \isakeyword{have} in the block. Thus they again serve to avoid |
|
575 duplication. Note that the conclusion of a raw proof block is stated with |
|
576 \isakeyword{have} rather than \isakeyword{show} because it is not the |
|
577 conclusion of some pending goal but some independent claim. |
|
578 |
|
579 The general idea demonstrated in this subsection is very |
|
580 important in Isar and distinguishes it from \isa{apply}-style proofs: |
|
581 \begin{quote}\em |
|
582 Do not manipulate the proof state into a particular form by applying |
|
583 proof methods but state the desired form explicitly and let the proof |
|
584 methods verify that from this form the original goal follows. |
|
585 \end{quote} |
|
586 This yields more readable and also more robust proofs. |
|
587 |
|
588 \subsubsection{General case distinctions} |
|
589 |
|
590 As an important application of raw proof blocks we show how to deal |
|
591 with general case distinctions --- more specific kinds are treated in |
|
592 \S\ref{sec:CaseDistinction}. Imagine that you would like to prove some |
|
593 goal by distinguishing $n$ cases $P_1$, \dots, $P_n$. You show that |
|
594 the $n$ cases are exhaustive (i.e.\ $P_1 \lor \dots \lor P_n$) and |
|
595 that each case $P_i$ implies the goal. Taken together, this proves the |
|
596 goal. The corresponding Isar proof pattern (for $n = 3$) is very handy: |
|
597 *} |
|
598 text_raw{*\renewcommand{\isamarkupcmt}[1]{#1}*} |
|
599 (*<*)lemma "XXX"(*>*) |
|
600 proof - |
|
601 have "P\<^isub>1 \<or> P\<^isub>2 \<or> P\<^isub>3" (*<*)sorry(*>*) -- {*\dots*} |
|
602 moreover |
|
603 { assume P\<^isub>1 |
|
604 -- {*\dots*} |
|
605 have ?thesis (*<*)sorry(*>*) -- {*\dots*} } |
|
606 moreover |
|
607 { assume P\<^isub>2 |
|
608 -- {*\dots*} |
|
609 have ?thesis (*<*)sorry(*>*) -- {*\dots*} } |
|
610 moreover |
|
611 { assume P\<^isub>3 |
|
612 -- {*\dots*} |
|
613 have ?thesis (*<*)sorry(*>*) -- {*\dots*} } |
|
614 ultimately show ?thesis by blast |
|
615 qed |
|
616 text_raw{*\renewcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}*} |
|
617 |
|
618 |
|
619 subsection{*Further refinements*} |
|
620 |
|
621 text{* This subsection discusses some further tricks that can make |
|
622 life easier although they are not essential. *} |
|
623 |
|
624 subsubsection{*\isakeyword{and}*} |
|
625 |
|
626 text{* Propositions (following \isakeyword{assume} etc) may but need not be |
|
627 separated by \isakeyword{and}. This is not just for readability |
|
628 (\isakeyword{from} \isa{A} \isakeyword{and} \isa{B} looks nicer than |
|
629 \isakeyword{from} \isa{A} \isa{B}) but for structuring lists of propositions |
|
630 into possibly named blocks. In |
|
631 \begin{center} |
|
632 \isakeyword{assume} \isa{A:} $A_1$ $A_2$ \isakeyword{and} \isa{B:} $A_3$ |
|
633 \isakeyword{and} $A_4$ |
|
634 \end{center} |
|
635 label \isa{A} refers to the list of propositions $A_1$ $A_2$ and |
|
636 label \isa{B} to $A_3$. *} |
|
637 |
|
638 subsubsection{*\isakeyword{note}*} |
|
639 text{* If you want to remember intermediate fact(s) that cannot be |
|
640 named directly, use \isakeyword{note}. For example the result of raw |
|
641 proof block can be named by following it with |
|
642 \isakeyword{note}~@{text"some_name = this"}. As a side effect, |
|
643 @{text this} is set to the list of facts on the right-hand side. You |
|
644 can also say @{text"note some_fact"}, which simply sets @{text this}, |
|
645 i.e.\ recalls @{text"some_fact"}, e.g.\ in a \isakeyword{moreover} sequence. *} |
|
646 |
|
647 |
|
648 subsubsection{*\isakeyword{fixes}*} |
|
649 |
|
650 text{* Sometimes it is necessary to decorate a proposition with type |
|
651 constraints, as in Cantor's theorem above. These type constraints tend |
|
652 to make the theorem less readable. The situation can be improved a |
|
653 little by combining the type constraint with an outer @{text"\<And>"}: *} |
|
654 |
|
655 theorem "\<And>f :: 'a \<Rightarrow> 'a set. \<exists>S. S \<notin> range f" |
|
656 (*<*)oops(*>*) |
|
657 text{*\noindent However, now @{term f} is bound and we need a |
|
658 \isakeyword{fix}~\isa{f} in the proof before we can refer to @{term f}. |
|
659 This is avoided by \isakeyword{fixes}: *} |
|
660 |
|
661 theorem fixes f :: "'a \<Rightarrow> 'a set" shows "\<exists>S. S \<notin> range f" |
|
662 (*<*)oops(*>*) |
|
663 text{* \noindent |
|
664 Even better, \isakeyword{fixes} allows to introduce concrete syntax locally:*} |
|
665 |
|
666 lemma comm_mono: |
|
667 fixes r :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix ">" 60) and |
|
668 f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "++" 70) |
|
669 assumes comm: "\<And>x y::'a. x ++ y = y ++ x" and |
|
670 mono: "\<And>x y z::'a. x > y \<Longrightarrow> x ++ z > y ++ z" |
|
671 shows "x > y \<Longrightarrow> z ++ x > z ++ y" |
|
672 by(simp add: comm mono) |
|
673 |
|
674 text{*\noindent The concrete syntax is dropped at the end of the proof and the |
|
675 theorem becomes @{thm[display,margin=60]comm_mono} |
|
676 \tweakskip *} |
|
677 |
|
678 subsubsection{*\isakeyword{obtain}*} |
|
679 |
|
680 text{* The \isakeyword{obtain} construct can introduce multiple |
|
681 witnesses and propositions as in the following proof fragment:*} |
|
682 |
|
683 lemma assumes A: "\<exists>x y. P x y \<and> Q x y" shows "R" |
|
684 proof - |
|
685 from A obtain x y where P: "P x y" and Q: "Q x y" by blast |
|
686 (*<*)oops(*>*) |
|
687 text{* Remember also that one does not even need to start with a formula |
|
688 containing @{text"\<exists>"} as we saw in the proof of Cantor's theorem. |
|
689 *} |
|
690 |
|
691 subsubsection{*Combining proof styles*} |
|
692 |
|
693 text{* Finally, whole \isa{apply}-scripts may appear in the leaves of the |
|
694 proof tree, although this is best avoided. Here is a contrived example: *} |
|
695 |
|
696 lemma "A \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> B" |
|
697 proof |
|
698 assume a: "A" |
|
699 show "(A \<longrightarrow>B) \<longrightarrow> B" |
|
700 apply(rule impI) |
|
701 apply(erule impE) |
|
702 apply(rule a) |
|
703 apply assumption |
|
704 done |
|
705 qed |
|
706 |
|
707 text{*\noindent You may need to resort to this technique if an |
|
708 automatic step fails to prove the desired proposition. |
|
709 |
|
710 When converting a proof from \isa{apply}-style into Isar you can proceed |
|
711 in a top-down manner: parts of the proof can be left in script form |
|
712 while the outer structure is already expressed in Isar. *} |
|
713 |
|
714 (*<*)end(*>*) |
|