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