1 (*<*) |
|
2 theory Isar |
|
3 imports LaTeXsugar |
|
4 begin |
|
5 ML{* quick_and_dirty := true *} |
|
6 (*>*) |
|
7 text{* |
|
8 Apply-scripts are unreadable and hard to maintain. The language of choice |
|
9 for larger proofs is \concept{Isar}. The two key features of Isar are: |
|
10 \begin{itemize} |
|
11 \item It is structured, not linear. |
|
12 \item It is readable without running it because |
|
13 you need to state what you are proving at any given point. |
|
14 \end{itemize} |
|
15 Whereas apply-scripts are like assembly language programs, Isar proofs |
|
16 are like structured programs with comments. A typical Isar proof looks like this: |
|
17 *}text{* |
|
18 \begin{tabular}{@ {}l} |
|
19 \isacom{proof}\\ |
|
20 \quad\isacom{assume} @{text"\""}$\mathit{formula}_0$@{text"\""}\\ |
|
21 \quad\isacom{have} @{text"\""}$\mathit{formula}_1$@{text"\""} \quad\isacom{by} @{text simp}\\ |
|
22 \quad\vdots\\ |
|
23 \quad\isacom{have} @{text"\""}$\mathit{formula}_n$@{text"\""} \quad\isacom{by} @{text blast}\\ |
|
24 \quad\isacom{show} @{text"\""}$\mathit{formula}_{n+1}$@{text"\""} \quad\isacom{by} @{text \<dots>}\\ |
|
25 \isacom{qed} |
|
26 \end{tabular} |
|
27 *}text{* |
|
28 It proves $\mathit{formula}_0 \Longrightarrow \mathit{formula}_{n+1}$ |
|
29 (provided each proof step succeeds). |
|
30 The intermediate \isacom{have} statements are merely stepping stones |
|
31 on the way towards the \isacom{show} statement that proves the actual |
|
32 goal. In more detail, this is the Isar core syntax: |
|
33 \medskip |
|
34 |
|
35 \begin{tabular}{@ {}lcl@ {}} |
|
36 \textit{proof} &=& \isacom{by} \textit{method}\\ |
|
37 &$\mid$& \isacom{proof} [\textit{method}] \ \textit{step}$^*$ \ \isacom{qed} |
|
38 \end{tabular} |
|
39 \medskip |
|
40 |
|
41 \begin{tabular}{@ {}lcl@ {}} |
|
42 \textit{step} &=& \isacom{fix} \textit{variables} \\ |
|
43 &$\mid$& \isacom{assume} \textit{proposition} \\ |
|
44 &$\mid$& [\isacom{from} \textit{fact}$^+$] (\isacom{have} $\mid$ \isacom{show}) \ \textit{proposition} \ \textit{proof} |
|
45 \end{tabular} |
|
46 \medskip |
|
47 |
|
48 \begin{tabular}{@ {}lcl@ {}} |
|
49 \textit{proposition} &=& [\textit{name}:] @{text"\""}\textit{formula}@{text"\""} |
|
50 \end{tabular} |
|
51 \medskip |
|
52 |
|
53 \begin{tabular}{@ {}lcl@ {}} |
|
54 \textit{fact} &=& \textit{name} \ $\mid$ \ \dots |
|
55 \end{tabular} |
|
56 \medskip |
|
57 |
|
58 \noindent A proof can either be an atomic \isacom{by} with a single proof |
|
59 method which must finish off the statement being proved, for example @{text |
|
60 auto}. Or it can be a \isacom{proof}--\isacom{qed} block of multiple |
|
61 steps. Such a block can optionally begin with a proof method that indicates |
|
62 how to start off the proof, e.g.\ \mbox{@{text"(induction xs)"}}. |
|
63 |
|
64 A step either assumes a proposition or states a proposition |
|
65 together with its proof. The optional \isacom{from} clause |
|
66 indicates which facts are to be used in the proof. |
|
67 Intermediate propositions are stated with \isacom{have}, the overall goal |
|
68 with \isacom{show}. A step can also introduce new local variables with |
|
69 \isacom{fix}. Logically, \isacom{fix} introduces @{text"\<And>"}-quantified |
|
70 variables, \isacom{assume} introduces the assumption of an implication |
|
71 (@{text"\<Longrightarrow>"}) and \isacom{have}/\isacom{show} the conclusion. |
|
72 |
|
73 Propositions are optionally named formulas. These names can be referred to in |
|
74 later \isacom{from} clauses. In the simplest case, a fact is such a name. |
|
75 But facts can also be composed with @{text OF} and @{text of} as shown in |
|
76 \S\ref{sec:forward-proof}---hence the \dots\ in the above grammar. Note |
|
77 that assumptions, intermediate \isacom{have} statements and global lemmas all |
|
78 have the same status and are thus collectively referred to as |
|
79 \concept{facts}. |
|
80 |
|
81 Fact names can stand for whole lists of facts. For example, if @{text f} is |
|
82 defined by command \isacom{fun}, @{text"f.simps"} refers to the whole list of |
|
83 recursion equations defining @{text f}. Individual facts can be selected by |
|
84 writing @{text"f.simps(2)"}, whole sublists by @{text"f.simps(2-4)"}. |
|
85 |
|
86 |
|
87 \section{Isar by example} |
|
88 |
|
89 We show a number of proofs of Cantor's theorem that a function from a set to |
|
90 its powerset cannot be surjective, illustrating various features of Isar. The |
|
91 constant @{const surj} is predefined. |
|
92 *} |
|
93 |
|
94 lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)" |
|
95 proof |
|
96 assume 0: "surj f" |
|
97 from 0 have 1: "\<forall>A. \<exists>a. A = f a" by(simp add: surj_def) |
|
98 from 1 have 2: "\<exists>a. {x. x \<notin> f x} = f a" by blast |
|
99 from 2 show "False" by blast |
|
100 qed |
|
101 |
|
102 text{* |
|
103 The \isacom{proof} command lacks an explicit method how to perform |
|
104 the proof. In such cases Isabelle tries to use some standard introduction |
|
105 rule, in the above case for @{text"\<not>"}: |
|
106 \[ |
|
107 \inferrule{ |
|
108 \mbox{@{thm (prem 1) notI}}} |
|
109 {\mbox{@{thm (concl) notI}}} |
|
110 \] |
|
111 In order to prove @{prop"~ P"}, assume @{text P} and show @{text False}. |
|
112 Thus we may assume @{prop"surj f"}. The proof shows that names of propositions |
|
113 may be (single!) digits---meaningful names are hard to invent and are often |
|
114 not necessary. Both \isacom{have} steps are obvious. The second one introduces |
|
115 the diagonal set @{term"{x. x \<notin> f x}"}, the key idea in the proof. |
|
116 If you wonder why @{text 2} directly implies @{text False}: from @{text 2} |
|
117 it follows that @{prop"a \<notin> f a \<longleftrightarrow> a \<in> f a"}. |
|
118 |
|
119 \subsection{@{text this}, @{text then}, @{text hence} and @{text thus}} |
|
120 |
|
121 Labels should be avoided. They interrupt the flow of the reader who has to |
|
122 scan the context for the point where the label was introduced. Ideally, the |
|
123 proof is a linear flow, where the output of one step becomes the input of the |
|
124 next step, piping the previously proved fact into the next proof, just like |
|
125 in a UNIX pipe. In such cases the predefined name @{text this} can be used |
|
126 to refer to the proposition proved in the previous step. This allows us to |
|
127 eliminate all labels from our proof (we suppress the \isacom{lemma} statement): |
|
128 *} |
|
129 (*<*) |
|
130 lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)" |
|
131 (*>*) |
|
132 proof |
|
133 assume "surj f" |
|
134 from this have "\<exists>a. {x. x \<notin> f x} = f a" by(auto simp: surj_def) |
|
135 from this show "False" by blast |
|
136 qed |
|
137 |
|
138 text{* We have also taken the opportunity to compress the two \isacom{have} |
|
139 steps into one. |
|
140 |
|
141 To compact the text further, Isar has a few convenient abbreviations: |
|
142 \medskip |
|
143 |
|
144 \begin{tabular}{rcl} |
|
145 \isacom{then} &=& \isacom{from} @{text this}\\ |
|
146 \isacom{thus} &=& \isacom{then} \isacom{show}\\ |
|
147 \isacom{hence} &=& \isacom{then} \isacom{have} |
|
148 \end{tabular} |
|
149 \medskip |
|
150 |
|
151 \noindent |
|
152 With the help of these abbreviations the proof becomes |
|
153 *} |
|
154 (*<*) |
|
155 lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)" |
|
156 (*>*) |
|
157 proof |
|
158 assume "surj f" |
|
159 hence "\<exists>a. {x. x \<notin> f x} = f a" by(auto simp: surj_def) |
|
160 thus "False" by blast |
|
161 qed |
|
162 text{* |
|
163 |
|
164 There are two further linguistic variations: |
|
165 \medskip |
|
166 |
|
167 \begin{tabular}{rcl} |
|
168 (\isacom{have}$\mid$\isacom{show}) \ \textit{prop} \ \isacom{using} \ \textit{facts} |
|
169 &=& |
|
170 \isacom{from} \ \textit{facts} \ (\isacom{have}$\mid$\isacom{show}) \ \textit{prop}\\ |
|
171 \isacom{with} \ \textit{facts} &=& \isacom{from} \ \textit{facts} \isa{this} |
|
172 \end{tabular} |
|
173 \medskip |
|
174 |
|
175 \noindent The \isacom{using} idiom de-emphasizes the used facts by moving them |
|
176 behind the proposition. |
|
177 |
|
178 \subsection{Structured lemma statements: \isacom{fixes}, \isacom{assumes}, \isacom{shows}} |
|
179 |
|
180 Lemmas can also be stated in a more structured fashion. To demonstrate this |
|
181 feature with Cantor's theorem, we rephrase @{prop"\<not> surj f"} |
|
182 a little: |
|
183 *} |
|
184 |
|
185 lemma |
|
186 fixes f :: "'a \<Rightarrow> 'a set" |
|
187 assumes s: "surj f" |
|
188 shows "False" |
|
189 |
|
190 txt{* The optional \isacom{fixes} part allows you to state the types of |
|
191 variables up front rather than by decorating one of their occurrences in the |
|
192 formula with a type constraint. The key advantage of the structured format is |
|
193 the \isacom{assumes} part that allows you to name each assumption; multiple |
|
194 assumptions can be separated by \isacom{and}. The |
|
195 \isacom{shows} part gives the goal. The actual theorem that will come out of |
|
196 the proof is @{prop"surj f \<Longrightarrow> False"}, but during the proof the assumption |
|
197 @{prop"surj f"} is available under the name @{text s} like any other fact. |
|
198 *} |
|
199 |
|
200 proof - |
|
201 have "\<exists> a. {x. x \<notin> f x} = f a" using s |
|
202 by(auto simp: surj_def) |
|
203 thus "False" by blast |
|
204 qed |
|
205 |
|
206 text{* In the \isacom{have} step the assumption @{prop"surj f"} is now |
|
207 referenced by its name @{text s}. The duplication of @{prop"surj f"} in the |
|
208 above proofs (once in the statement of the lemma, once in its proof) has been |
|
209 eliminated. |
|
210 |
|
211 \begin{warn} |
|
212 Note the dash after the \isacom{proof} |
|
213 command. It is the null method that does nothing to the goal. Leaving it out |
|
214 would ask Isabelle to try some suitable introduction rule on the goal @{const |
|
215 False}---but there is no suitable introduction rule and \isacom{proof} |
|
216 would fail. |
|
217 \end{warn} |
|
218 |
|
219 Stating a lemma with \isacom{assumes}-\isacom{shows} implicitly introduces the |
|
220 name @{text assms} that stands for the list of all assumptions. You can refer |
|
221 to individual assumptions by @{text"assms(1)"}, @{text"assms(2)"} etc, |
|
222 thus obviating the need to name them individually. |
|
223 |
|
224 \section{Proof patterns} |
|
225 |
|
226 We show a number of important basic proof patterns. Many of them arise from |
|
227 the rules of natural deduction that are applied by \isacom{proof} by |
|
228 default. The patterns are phrased in terms of \isacom{show} but work for |
|
229 \isacom{have} and \isacom{lemma}, too. |
|
230 |
|
231 We start with two forms of \concept{case analysis}: |
|
232 starting from a formula @{text P} we have the two cases @{text P} and |
|
233 @{prop"~P"}, and starting from a fact @{prop"P \<or> Q"} |
|
234 we have the two cases @{text P} and @{text Q}: |
|
235 *}text_raw{* |
|
236 \begin{tabular}{@ {}ll@ {}} |
|
237 \begin{minipage}[t]{.4\textwidth} |
|
238 \isa{% |
|
239 *} |
|
240 (*<*)lemma "R" proof-(*>*) |
|
241 show "R" |
|
242 proof cases |
|
243 assume "P" |
|
244 txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} |
|
245 show "R" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} |
|
246 next |
|
247 assume "\<not> P" |
|
248 txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} |
|
249 show "R" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} |
|
250 qed(*<*)oops(*>*) |
|
251 text_raw {* } |
|
252 \end{minipage} |
|
253 & |
|
254 \begin{minipage}[t]{.4\textwidth} |
|
255 \isa{% |
|
256 *} |
|
257 (*<*)lemma "R" proof-(*>*) |
|
258 have "P \<or> Q" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} |
|
259 then show "R" |
|
260 proof |
|
261 assume "P" |
|
262 txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} |
|
263 show "R" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} |
|
264 next |
|
265 assume "Q" |
|
266 txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} |
|
267 show "R" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} |
|
268 qed(*<*)oops(*>*) |
|
269 |
|
270 text_raw {* } |
|
271 \end{minipage} |
|
272 \end{tabular} |
|
273 \medskip |
|
274 \begin{isamarkuptext}% |
|
275 How to prove a logical equivalence: |
|
276 \end{isamarkuptext}% |
|
277 \isa{% |
|
278 *} |
|
279 (*<*)lemma "P\<longleftrightarrow>Q" proof-(*>*) |
|
280 show "P \<longleftrightarrow> Q" |
|
281 proof |
|
282 assume "P" |
|
283 txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} |
|
284 show "Q" (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*} |
|
285 next |
|
286 assume "Q" |
|
287 txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} |
|
288 show "P" (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*} |
|
289 qed(*<*)qed(*>*) |
|
290 text_raw {* } |
|
291 \medskip |
|
292 \begin{isamarkuptext}% |
|
293 Proofs by contradiction: |
|
294 \end{isamarkuptext}% |
|
295 \begin{tabular}{@ {}ll@ {}} |
|
296 \begin{minipage}[t]{.4\textwidth} |
|
297 \isa{% |
|
298 *} |
|
299 (*<*)lemma "\<not> P" proof-(*>*) |
|
300 show "\<not> P" |
|
301 proof |
|
302 assume "P" |
|
303 txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} |
|
304 show "False" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} |
|
305 qed(*<*)oops(*>*) |
|
306 |
|
307 text_raw {* } |
|
308 \end{minipage} |
|
309 & |
|
310 \begin{minipage}[t]{.4\textwidth} |
|
311 \isa{% |
|
312 *} |
|
313 (*<*)lemma "P" proof-(*>*) |
|
314 show "P" |
|
315 proof (rule ccontr) |
|
316 assume "\<not>P" |
|
317 txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} |
|
318 show "False" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} |
|
319 qed(*<*)oops(*>*) |
|
320 |
|
321 text_raw {* } |
|
322 \end{minipage} |
|
323 \end{tabular} |
|
324 \medskip |
|
325 \begin{isamarkuptext}% |
|
326 The name @{thm[source] ccontr} stands for ``classical contradiction''. |
|
327 |
|
328 How to prove quantified formulas: |
|
329 \end{isamarkuptext}% |
|
330 \begin{tabular}{@ {}ll@ {}} |
|
331 \begin{minipage}[t]{.4\textwidth} |
|
332 \isa{% |
|
333 *} |
|
334 (*<*)lemma "ALL x. P x" proof-(*>*) |
|
335 show "\<forall>x. P(x)" |
|
336 proof |
|
337 fix x |
|
338 txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} |
|
339 show "P(x)" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} |
|
340 qed(*<*)oops(*>*) |
|
341 |
|
342 text_raw {* } |
|
343 \end{minipage} |
|
344 & |
|
345 \begin{minipage}[t]{.4\textwidth} |
|
346 \isa{% |
|
347 *} |
|
348 (*<*)lemma "EX x. P(x)" proof-(*>*) |
|
349 show "\<exists>x. P(x)" |
|
350 proof |
|
351 txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} |
|
352 show "P(witness)" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} |
|
353 qed |
|
354 (*<*)oops(*>*) |
|
355 |
|
356 text_raw {* } |
|
357 \end{minipage} |
|
358 \end{tabular} |
|
359 \medskip |
|
360 \begin{isamarkuptext}% |
|
361 In the proof of \noquotes{@{prop[source]"\<forall>x. P(x)"}}, |
|
362 the step \isacom{fix}~@{text x} introduces a locally fixed variable @{text x} |
|
363 into the subproof, the proverbial ``arbitrary but fixed value''. |
|
364 Instead of @{text x} we could have chosen any name in the subproof. |
|
365 In the proof of \noquotes{@{prop[source]"\<exists>x. P(x)"}}, |
|
366 @{text witness} is some arbitrary |
|
367 term for which we can prove that it satisfies @{text P}. |
|
368 |
|
369 How to reason forward from \noquotes{@{prop[source] "\<exists>x. P(x)"}}: |
|
370 \end{isamarkuptext}% |
|
371 *} |
|
372 (*<*)lemma True proof- assume 1: "EX x. P x"(*>*) |
|
373 have "\<exists>x. P(x)" (*<*)by(rule 1)(*>*)txt_raw{*\ $\dots$\\*} |
|
374 then obtain x where p: "P(x)" by blast |
|
375 (*<*)oops(*>*) |
|
376 text{* |
|
377 After the \isacom{obtain} step, @{text x} (we could have chosen any name) |
|
378 is a fixed local |
|
379 variable, and @{text p} is the name of the fact |
|
380 \noquotes{@{prop[source] "P(x)"}}. |
|
381 This pattern works for one or more @{text x}. |
|
382 As an example of the \isacom{obtain} command, here is the proof of |
|
383 Cantor's theorem in more detail: |
|
384 *} |
|
385 |
|
386 lemma "\<not> surj(f :: 'a \<Rightarrow> 'a set)" |
|
387 proof |
|
388 assume "surj f" |
|
389 hence "\<exists>a. {x. x \<notin> f x} = f a" by(auto simp: surj_def) |
|
390 then obtain a where "{x. x \<notin> f x} = f a" by blast |
|
391 hence "a \<notin> f a \<longleftrightarrow> a \<in> f a" by blast |
|
392 thus "False" by blast |
|
393 qed |
|
394 |
|
395 text_raw{* |
|
396 \begin{isamarkuptext}% |
|
397 |
|
398 Finally, how to prove set equality and subset relationship: |
|
399 \end{isamarkuptext}% |
|
400 \begin{tabular}{@ {}ll@ {}} |
|
401 \begin{minipage}[t]{.4\textwidth} |
|
402 \isa{% |
|
403 *} |
|
404 (*<*)lemma "A = (B::'a set)" proof-(*>*) |
|
405 show "A = B" |
|
406 proof |
|
407 show "A \<subseteq> B" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} |
|
408 next |
|
409 show "B \<subseteq> A" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} |
|
410 qed(*<*)qed(*>*) |
|
411 |
|
412 text_raw {* } |
|
413 \end{minipage} |
|
414 & |
|
415 \begin{minipage}[t]{.4\textwidth} |
|
416 \isa{% |
|
417 *} |
|
418 (*<*)lemma "A <= (B::'a set)" proof-(*>*) |
|
419 show "A \<subseteq> B" |
|
420 proof |
|
421 fix x |
|
422 assume "x \<in> A" |
|
423 txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} |
|
424 show "x \<in> B" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} |
|
425 qed(*<*)qed(*>*) |
|
426 |
|
427 text_raw {* } |
|
428 \end{minipage} |
|
429 \end{tabular} |
|
430 \begin{isamarkuptext}% |
|
431 \section{Streamlining proofs} |
|
432 |
|
433 \subsection{Pattern matching and quotations} |
|
434 |
|
435 In the proof patterns shown above, formulas are often duplicated. |
|
436 This can make the text harder to read, write and maintain. Pattern matching |
|
437 is an abbreviation mechanism to avoid such duplication. Writing |
|
438 \begin{quote} |
|
439 \isacom{show} \ \textit{formula} @{text"("}\isacom{is} \textit{pattern}@{text")"} |
|
440 \end{quote} |
|
441 matches the pattern against the formula, thus instantiating the unknowns in |
|
442 the pattern for later use. As an example, consider the proof pattern for |
|
443 @{text"\<longleftrightarrow>"}: |
|
444 \end{isamarkuptext}% |
|
445 *} |
|
446 (*<*)lemma "formula\<^isub>1 \<longleftrightarrow> formula\<^isub>2" proof-(*>*) |
|
447 show "formula\<^isub>1 \<longleftrightarrow> formula\<^isub>2" (is "?L \<longleftrightarrow> ?R") |
|
448 proof |
|
449 assume "?L" |
|
450 txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} |
|
451 show "?R" (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*} |
|
452 next |
|
453 assume "?R" |
|
454 txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} |
|
455 show "?L" (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*} |
|
456 qed(*<*)qed(*>*) |
|
457 |
|
458 text{* Instead of duplicating @{text"formula\<^isub>i"} in the text, we introduce |
|
459 the two abbreviations @{text"?L"} and @{text"?R"} by pattern matching. |
|
460 Pattern matching works wherever a formula is stated, in particular |
|
461 with \isacom{have} and \isacom{lemma}. |
|
462 |
|
463 The unknown @{text"?thesis"} is implicitly matched against any goal stated by |
|
464 \isacom{lemma} or \isacom{show}. Here is a typical example: *} |
|
465 |
|
466 lemma "formula" |
|
467 proof - |
|
468 txt_raw{*\\\mbox{}\quad$\vdots$\\\mbox{}\hspace{-1.4ex}*} |
|
469 show ?thesis (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*} |
|
470 qed |
|
471 |
|
472 text{* |
|
473 Unknowns can also be instantiated with \isacom{let} commands |
|
474 \begin{quote} |
|
475 \isacom{let} @{text"?t"} = @{text"\""}\textit{some-big-term}@{text"\""} |
|
476 \end{quote} |
|
477 Later proof steps can refer to @{text"?t"}: |
|
478 \begin{quote} |
|
479 \isacom{have} @{text"\""}\dots @{text"?t"} \dots@{text"\""} |
|
480 \end{quote} |
|
481 \begin{warn} |
|
482 Names of facts are introduced with @{text"name:"} and refer to proved |
|
483 theorems. Unknowns @{text"?X"} refer to terms or formulas. |
|
484 \end{warn} |
|
485 |
|
486 Although abbreviations shorten the text, the reader needs to remember what |
|
487 they stand for. Similarly for names of facts. Names like @{text 1}, @{text 2} |
|
488 and @{text 3} are not helpful and should only be used in short proofs. For |
|
489 longer proofs, descriptive names are better. But look at this example: |
|
490 \begin{quote} |
|
491 \isacom{have} \ @{text"x_gr_0: \"x > 0\""}\\ |
|
492 $\vdots$\\ |
|
493 \isacom{from} @{text "x_gr_0"} \dots |
|
494 \end{quote} |
|
495 The name is longer than the fact it stands for! Short facts do not need names, |
|
496 one can refer to them easily by quoting them: |
|
497 \begin{quote} |
|
498 \isacom{have} \ @{text"\"x > 0\""}\\ |
|
499 $\vdots$\\ |
|
500 \isacom{from} @{text "`x>0`"} \dots |
|
501 \end{quote} |
|
502 Note that the quotes around @{text"x>0"} are \concept{back quotes}. |
|
503 They refer to the fact not by name but by value. |
|
504 |
|
505 \subsection{\isacom{moreover}} |
|
506 |
|
507 Sometimes one needs a number of facts to enable some deduction. Of course |
|
508 one can name these facts individually, as shown on the right, |
|
509 but one can also combine them with \isacom{moreover}, as shown on the left: |
|
510 *}text_raw{* |
|
511 \begin{tabular}{@ {}ll@ {}} |
|
512 \begin{minipage}[t]{.4\textwidth} |
|
513 \isa{% |
|
514 *} |
|
515 (*<*)lemma "P" proof-(*>*) |
|
516 have "P\<^isub>1" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} |
|
517 moreover have "P\<^isub>2" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} |
|
518 moreover |
|
519 txt_raw{*\\$\vdots$\\\hspace{-1.4ex}*}(*<*)have "True" ..(*>*) |
|
520 moreover have "P\<^isub>n" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} |
|
521 ultimately have "P" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} |
|
522 (*<*)oops(*>*) |
|
523 |
|
524 text_raw {* } |
|
525 \end{minipage} |
|
526 & |
|
527 \qquad |
|
528 \begin{minipage}[t]{.4\textwidth} |
|
529 \isa{% |
|
530 *} |
|
531 (*<*)lemma "P" proof-(*>*) |
|
532 have lab\<^isub>1: "P\<^isub>1" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} |
|
533 have lab\<^isub>2: "P\<^isub>2" (*<*)sorry(*>*)txt_raw{*\ $\dots$*} |
|
534 txt_raw{*\\$\vdots$\\\hspace{-1.4ex}*} |
|
535 have lab\<^isub>n: "P\<^isub>n" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} |
|
536 from lab\<^isub>1 lab\<^isub>2 txt_raw{*\ $\dots$\\*} |
|
537 have "P" (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} |
|
538 (*<*)oops(*>*) |
|
539 |
|
540 text_raw {* } |
|
541 \end{minipage} |
|
542 \end{tabular} |
|
543 \begin{isamarkuptext}% |
|
544 The \isacom{moreover} version is no shorter but expresses the structure more |
|
545 clearly and avoids new names. |
|
546 |
|
547 \subsection{Raw proof blocks} |
|
548 |
|
549 Sometimes one would like to prove some lemma locally within a proof. |
|
550 A lemma that shares the current context of assumptions but that |
|
551 has its own assumptions and is generalized over its locally fixed |
|
552 variables at the end. This is what a \concept{raw proof block} does: |
|
553 \begin{quote} |
|
554 @{text"{"} \isacom{fix} @{text"x\<^isub>1 \<dots> x\<^isub>n"}\\ |
|
555 \mbox{}\ \ \ \isacom{assume} @{text"A\<^isub>1 \<dots> A\<^isub>m"}\\ |
|
556 \mbox{}\ \ \ $\vdots$\\ |
|
557 \mbox{}\ \ \ \isacom{have} @{text"B"}\\ |
|
558 @{text"}"} |
|
559 \end{quote} |
|
560 proves @{text"\<lbrakk> A\<^isub>1; \<dots> ; A\<^isub>m \<rbrakk> \<Longrightarrow> B"} |
|
561 where all @{text"x\<^isub>i"} have been replaced by unknowns @{text"?x\<^isub>i"}. |
|
562 \begin{warn} |
|
563 The conclusion of a raw proof block is \emph{not} indicated by \isacom{show} |
|
564 but is simply the final \isacom{have}. |
|
565 \end{warn} |
|
566 |
|
567 As an example we prove a simple fact about divisibility on integers. |
|
568 The definition of @{text "dvd"} is @{thm dvd_def}. |
|
569 \end{isamarkuptext}% |
|
570 *} |
|
571 |
|
572 lemma fixes a b :: int assumes "b dvd (a+b)" shows "b dvd a" |
|
573 proof - |
|
574 { fix k assume k: "a+b = b*k" |
|
575 have "\<exists>k'. a = b*k'" |
|
576 proof |
|
577 show "a = b*(k - 1)" using k by(simp add: algebra_simps) |
|
578 qed } |
|
579 then show ?thesis using assms by(auto simp add: dvd_def) |
|
580 qed |
|
581 |
|
582 text{* Note that the result of a raw proof block has no name. In this example |
|
583 it was directly piped (via \isacom{then}) into the final proof, but it can |
|
584 also be named for later reference: you simply follow the block directly by a |
|
585 \isacom{note} command: |
|
586 \begin{quote} |
|
587 \isacom{note} \ @{text"name = this"} |
|
588 \end{quote} |
|
589 This introduces a new name @{text name} that refers to @{text this}, |
|
590 the fact just proved, in this case the preceding block. In general, |
|
591 \isacom{note} introduces a new name for one or more facts. |
|
592 |
|
593 \section{Case analysis and induction} |
|
594 |
|
595 \subsection{Datatype case analysis} |
|
596 |
|
597 We have seen case analysis on formulas. Now we want to distinguish |
|
598 which form some term takes: is it @{text 0} or of the form @{term"Suc n"}, |
|
599 is it @{term"[]"} or of the form @{term"x#xs"}, etc. Here is a typical example |
|
600 proof by case analysis on the form of @{text xs}: |
|
601 *} |
|
602 |
|
603 lemma "length(tl xs) = length xs - 1" |
|
604 proof (cases xs) |
|
605 assume "xs = []" |
|
606 thus ?thesis by simp |
|
607 next |
|
608 fix y ys assume "xs = y#ys" |
|
609 thus ?thesis by simp |
|
610 qed |
|
611 |
|
612 text{* Function @{text tl} (''tail'') is defined by @{thm tl.simps(1)} and |
|
613 @{thm tl.simps(2)}. Note that the result type of @{const length} is @{typ nat} |
|
614 and @{prop"0 - 1 = (0::nat)"}. |
|
615 |
|
616 This proof pattern works for any term @{text t} whose type is a datatype. |
|
617 The goal has to be proved for each constructor @{text C}: |
|
618 \begin{quote} |
|
619 \isacom{fix} \ @{text"x\<^isub>1 \<dots> x\<^isub>n"} \isacom{assume} @{text"\"t = C x\<^isub>1 \<dots> x\<^isub>n\""} |
|
620 \end{quote} |
|
621 Each case can be written in a more compact form by means of the \isacom{case} |
|
622 command: |
|
623 \begin{quote} |
|
624 \isacom{case} @{text "(C x\<^isub>1 \<dots> x\<^isub>n)"} |
|
625 \end{quote} |
|
626 This is equivalent to the explicit \isacom{fix}-\isacom{assume} line |
|
627 but also gives the assumption @{text"\"t = C x\<^isub>1 \<dots> x\<^isub>n\""} a name: @{text C}, |
|
628 like the constructor. |
|
629 Here is the \isacom{case} version of the proof above: |
|
630 *} |
|
631 (*<*)lemma "length(tl xs) = length xs - 1"(*>*) |
|
632 proof (cases xs) |
|
633 case Nil |
|
634 thus ?thesis by simp |
|
635 next |
|
636 case (Cons y ys) |
|
637 thus ?thesis by simp |
|
638 qed |
|
639 |
|
640 text{* Remember that @{text Nil} and @{text Cons} are the alphanumeric names |
|
641 for @{text"[]"} and @{text"#"}. The names of the assumptions |
|
642 are not used because they are directly piped (via \isacom{thus}) |
|
643 into the proof of the claim. |
|
644 |
|
645 \subsection{Structural induction} |
|
646 |
|
647 We illustrate structural induction with an example based on natural numbers: |
|
648 the sum (@{text"\<Sum>"}) of the first @{text n} natural numbers |
|
649 (@{text"{0..n::nat}"}) is equal to \mbox{@{term"n*(n+1) div 2::nat"}}. |
|
650 Never mind the details, just focus on the pattern: |
|
651 *} |
|
652 |
|
653 lemma "\<Sum>{0..n::nat} = n*(n+1) div 2" |
|
654 proof (induction n) |
|
655 show "\<Sum>{0..0::nat} = 0*(0+1) div 2" by simp |
|
656 next |
|
657 fix n assume "\<Sum>{0..n::nat} = n*(n+1) div 2" |
|
658 thus "\<Sum>{0..Suc n} = Suc n*(Suc n+1) div 2" by simp |
|
659 qed |
|
660 |
|
661 text{* Except for the rewrite steps, everything is explicitly given. This |
|
662 makes the proof easily readable, but the duplication means it is tedious to |
|
663 write and maintain. Here is how pattern |
|
664 matching can completely avoid any duplication: *} |
|
665 |
|
666 lemma "\<Sum>{0..n::nat} = n*(n+1) div 2" (is "?P n") |
|
667 proof (induction n) |
|
668 show "?P 0" by simp |
|
669 next |
|
670 fix n assume "?P n" |
|
671 thus "?P(Suc n)" by simp |
|
672 qed |
|
673 |
|
674 text{* The first line introduces an abbreviation @{text"?P n"} for the goal. |
|
675 Pattern matching @{text"?P n"} with the goal instantiates @{text"?P"} to the |
|
676 function @{term"\<lambda>n. \<Sum>{0..n::nat} = n*(n+1) div 2"}. Now the proposition to |
|
677 be proved in the base case can be written as @{text"?P 0"}, the induction |
|
678 hypothesis as @{text"?P n"}, and the conclusion of the induction step as |
|
679 @{text"?P(Suc n)"}. |
|
680 |
|
681 Induction also provides the \isacom{case} idiom that abbreviates |
|
682 the \isacom{fix}-\isacom{assume} step. The above proof becomes |
|
683 *} |
|
684 (*<*)lemma "\<Sum>{0..n::nat} = n*(n+1) div 2"(*>*) |
|
685 proof (induction n) |
|
686 case 0 |
|
687 show ?case by simp |
|
688 next |
|
689 case (Suc n) |
|
690 thus ?case by simp |
|
691 qed |
|
692 |
|
693 text{* |
|
694 The unknown @{text "?case"} is set in each case to the required |
|
695 claim, i.e.\ @{text"?P 0"} and \mbox{@{text"?P(Suc n)"}} in the above proof, |
|
696 without requiring the user to define a @{text "?P"}. The general |
|
697 pattern for induction over @{typ nat} is shown on the left-hand side: |
|
698 *}text_raw{* |
|
699 \begin{tabular}{@ {}ll@ {}} |
|
700 \begin{minipage}[t]{.4\textwidth} |
|
701 \isa{% |
|
702 *} |
|
703 (*<*)lemma "P(n::nat)" proof -(*>*) |
|
704 show "P(n)" |
|
705 proof (induction n) |
|
706 case 0 |
|
707 txt_raw{*\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{-1ex}*} |
|
708 show ?case (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*} |
|
709 next |
|
710 case (Suc n) |
|
711 txt_raw{*\\\mbox{}\ \ $\vdots$\\\mbox{}\hspace{-1ex}*} |
|
712 show ?case (*<*)sorry(*>*) txt_raw{*\ $\dots$\\*} |
|
713 qed(*<*)qed(*>*) |
|
714 |
|
715 text_raw {* } |
|
716 \end{minipage} |
|
717 & |
|
718 \begin{minipage}[t]{.4\textwidth} |
|
719 ~\\ |
|
720 ~\\ |
|
721 \isacom{let} @{text"?case = \"P(0)\""}\\ |
|
722 ~\\ |
|
723 ~\\ |
|
724 ~\\[1ex] |
|
725 \isacom{fix} @{text n} \isacom{assume} @{text"Suc: \"P(n)\""}\\ |
|
726 \isacom{let} @{text"?case = \"P(Suc n)\""}\\ |
|
727 \end{minipage} |
|
728 \end{tabular} |
|
729 \medskip |
|
730 *} |
|
731 text{* |
|
732 On the right side you can see what the \isacom{case} command |
|
733 on the left stands for. |
|
734 |
|
735 In case the goal is an implication, induction does one more thing: the |
|
736 proposition to be proved in each case is not the whole implication but only |
|
737 its conclusion; the premises of the implication are immediately made |
|
738 assumptions of that case. That is, if in the above proof we replace |
|
739 \isacom{show}~@{text"P(n)"} by |
|
740 \mbox{\isacom{show}~@{text"A(n) \<Longrightarrow> P(n)"}} |
|
741 then \isacom{case}~@{text 0} stands for |
|
742 \begin{quote} |
|
743 \isacom{assume} \ @{text"0: \"A(0)\""}\\ |
|
744 \isacom{let} @{text"?case = \"P(0)\""} |
|
745 \end{quote} |
|
746 and \isacom{case}~@{text"(Suc n)"} stands for |
|
747 \begin{quote} |
|
748 \isacom{fix} @{text n}\\ |
|
749 \isacom{assume} @{text"Suc:"} |
|
750 \begin{tabular}[t]{l}@{text"\"A(n) \<Longrightarrow> P(n)\""}\\@{text"\"A(Suc n)\""}\end{tabular}\\ |
|
751 \isacom{let} @{text"?case = \"P(Suc n)\""} |
|
752 \end{quote} |
|
753 The list of assumptions @{text Suc} is actually subdivided |
|
754 into @{text"Suc.IH"}, the induction hypotheses (here @{text"A(n) \<Longrightarrow> P(n)"}) |
|
755 and @{text"Suc.prems"}, the premises of the goal being proved |
|
756 (here @{text"A(Suc n)"}). |
|
757 |
|
758 Induction works for any datatype. |
|
759 Proving a goal @{text"\<lbrakk> A\<^isub>1(x); \<dots>; A\<^isub>k(x) \<rbrakk> \<Longrightarrow> P(x)"} |
|
760 by induction on @{text x} generates a proof obligation for each constructor |
|
761 @{text C} of the datatype. The command @{text"case (C x\<^isub>1 \<dots> x\<^isub>n)"} |
|
762 performs the following steps: |
|
763 \begin{enumerate} |
|
764 \item \isacom{fix} @{text"x\<^isub>1 \<dots> x\<^isub>n"} |
|
765 \item \isacom{assume} the induction hypotheses (calling them @{text C.IH}) |
|
766 and the premises \mbox{@{text"A\<^isub>i(C x\<^isub>1 \<dots> x\<^isub>n)"}} (calling them @{text"C.prems"}) |
|
767 and calling the whole list @{text C} |
|
768 \item \isacom{let} @{text"?case = \"P(C x\<^isub>1 \<dots> x\<^isub>n)\""} |
|
769 \end{enumerate} |
|
770 |
|
771 \subsection{Rule induction} |
|
772 |
|
773 Recall the inductive and recursive definitions of even numbers in |
|
774 \autoref{sec:inductive-defs}: |
|
775 *} |
|
776 |
|
777 inductive ev :: "nat \<Rightarrow> bool" where |
|
778 ev0: "ev 0" | |
|
779 evSS: "ev n \<Longrightarrow> ev(Suc(Suc n))" |
|
780 |
|
781 fun even :: "nat \<Rightarrow> bool" where |
|
782 "even 0 = True" | |
|
783 "even (Suc 0) = False" | |
|
784 "even (Suc(Suc n)) = even n" |
|
785 |
|
786 text{* We recast the proof of @{prop"ev n \<Longrightarrow> even n"} in Isar. The |
|
787 left column shows the actual proof text, the right column shows |
|
788 the implicit effect of the two \isacom{case} commands:*}text_raw{* |
|
789 \begin{tabular}{@ {}l@ {\qquad}l@ {}} |
|
790 \begin{minipage}[t]{.5\textwidth} |
|
791 \isa{% |
|
792 *} |
|
793 |
|
794 lemma "ev n \<Longrightarrow> even n" |
|
795 proof(induction rule: ev.induct) |
|
796 case ev0 |
|
797 show ?case by simp |
|
798 next |
|
799 case evSS |
|
800 |
|
801 |
|
802 |
|
803 thus ?case by simp |
|
804 qed |
|
805 |
|
806 text_raw {* } |
|
807 \end{minipage} |
|
808 & |
|
809 \begin{minipage}[t]{.5\textwidth} |
|
810 ~\\ |
|
811 ~\\ |
|
812 \isacom{let} @{text"?case = \"even 0\""}\\ |
|
813 ~\\ |
|
814 ~\\ |
|
815 \isacom{fix} @{text n}\\ |
|
816 \isacom{assume} @{text"evSS:"} |
|
817 \begin{tabular}[t]{l} @{text"\"ev n\""}\\@{text"\"even n\""}\end{tabular}\\ |
|
818 \isacom{let} @{text"?case = \"even(Suc(Suc n))\""}\\ |
|
819 \end{minipage} |
|
820 \end{tabular} |
|
821 \medskip |
|
822 *} |
|
823 text{* |
|
824 The proof resembles structural induction, but the induction rule is given |
|
825 explicitly and the names of the cases are the names of the rules in the |
|
826 inductive definition. |
|
827 Let us examine the two assumptions named @{thm[source]evSS}: |
|
828 @{prop "ev n"} is the premise of rule @{thm[source]evSS}, which we may assume |
|
829 because we are in the case where that rule was used; @{prop"even n"} |
|
830 is the induction hypothesis. |
|
831 \begin{warn} |
|
832 Because each \isacom{case} command introduces a list of assumptions |
|
833 named like the case name, which is the name of a rule of the inductive |
|
834 definition, those rules now need to be accessed with a qualified name, here |
|
835 @{thm[source] ev.ev0} and @{thm[source] ev.evSS} |
|
836 \end{warn} |
|
837 |
|
838 In the case @{thm[source]evSS} of the proof above we have pretended that the |
|
839 system fixes a variable @{text n}. But unless the user provides the name |
|
840 @{text n}, the system will just invent its own name that cannot be referred |
|
841 to. In the above proof, we do not need to refer to it, hence we do not give |
|
842 it a specific name. In case one needs to refer to it one writes |
|
843 \begin{quote} |
|
844 \isacom{case} @{text"(evSS m)"} |
|
845 \end{quote} |
|
846 just like \isacom{case}~@{text"(Suc n)"} in earlier structural inductions. |
|
847 The name @{text m} is an arbitrary choice. As a result, |
|
848 case @{thm[source] evSS} is derived from a renamed version of |
|
849 rule @{thm[source] evSS}: @{text"ev m \<Longrightarrow> ev(Suc(Suc m))"}. |
|
850 Here is an example with a (contrived) intermediate step that refers to @{text m}: |
|
851 *} |
|
852 |
|
853 lemma "ev n \<Longrightarrow> even n" |
|
854 proof(induction rule: ev.induct) |
|
855 case ev0 show ?case by simp |
|
856 next |
|
857 case (evSS m) |
|
858 have "even(Suc(Suc m)) = even m" by simp |
|
859 thus ?case using `even m` by blast |
|
860 qed |
|
861 |
|
862 text{* |
|
863 \indent |
|
864 In general, let @{text I} be a (for simplicity unary) inductively defined |
|
865 predicate and let the rules in the definition of @{text I} |
|
866 be called @{text "rule\<^isub>1"}, \dots, @{text "rule\<^isub>n"}. A proof by rule |
|
867 induction follows this pattern: |
|
868 *} |
|
869 |
|
870 (*<*) |
|
871 inductive I where rule\<^isub>1: "I()" | rule\<^isub>2: "I()" | rule\<^isub>n: "I()" |
|
872 lemma "I x \<Longrightarrow> P x" proof-(*>*) |
|
873 show "I x \<Longrightarrow> P x" |
|
874 proof(induction rule: I.induct) |
|
875 case rule\<^isub>1 |
|
876 txt_raw{*\\[-.4ex]\mbox{}\ \ $\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*} |
|
877 show ?case (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} |
|
878 next |
|
879 txt_raw{*\\[-.4ex]$\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*} |
|
880 (*<*) |
|
881 case rule\<^isub>2 |
|
882 show ?case sorry |
|
883 (*>*) |
|
884 next |
|
885 case rule\<^isub>n |
|
886 txt_raw{*\\[-.4ex]\mbox{}\ \ $\vdots$\\[-.4ex]\mbox{}\hspace{-1ex}*} |
|
887 show ?case (*<*)sorry(*>*)txt_raw{*\ $\dots$\\*} |
|
888 qed(*<*)qed(*>*) |
|
889 |
|
890 text{* |
|
891 One can provide explicit variable names by writing |
|
892 \isacom{case}~@{text"(rule\<^isub>i x\<^isub>1 \<dots> x\<^isub>k)"}, thus renaming the first @{text k} |
|
893 free variables in rule @{text i} to @{text"x\<^isub>1 \<dots> x\<^isub>k"}, |
|
894 going through rule @{text i} from left to right. |
|
895 |
|
896 \subsection{Assumption naming} |
|
897 |
|
898 In any induction, \isacom{case}~@{text name} sets up a list of assumptions |
|
899 also called @{text name}, which is subdivided into three parts: |
|
900 \begin{description} |
|
901 \item[@{text name.IH}] contains the induction hypotheses. |
|
902 \item[@{text name.hyps}] contains all the other hypotheses of this case in the |
|
903 induction rule. For rule inductions these are the hypotheses of rule |
|
904 @{text name}, for structural inductions these are empty. |
|
905 \item[@{text name.prems}] contains the (suitably instantiated) premises |
|
906 of the statement being proved, i.e. the @{text A\<^isub>i} when |
|
907 proving @{text"\<lbrakk> A\<^isub>1; \<dots>; A\<^isub>n \<rbrakk> \<Longrightarrow> A"}. |
|
908 \end{description} |
|
909 \begin{warn} |
|
910 Proof method @{text induct} differs from @{text induction} |
|
911 only in this naming policy: @{text induct} does not distinguish |
|
912 @{text IH} from @{text hyps} but subsumes @{text IH} under @{text hyps}. |
|
913 \end{warn} |
|
914 |
|
915 More complicated inductive proofs than the ones we have seen so far |
|
916 often need to refer to specific assumptions---just @{text name} or even |
|
917 @{text name.prems} and @{text name.IH} can be too unspecific. |
|
918 This is where the indexing of fact lists comes in handy, e.g.\ |
|
919 @{text"name.IH(2)"} or @{text"name.prems(1-2)"}. |
|
920 |
|
921 \subsection{Rule inversion} |
|
922 |
|
923 Rule inversion is case analysis of which rule could have been used to |
|
924 derive some fact. The name \concept{rule inversion} emphasizes that we are |
|
925 reasoning backwards: by which rules could some given fact have been proved? |
|
926 For the inductive definition of @{const ev}, rule inversion can be summarized |
|
927 like this: |
|
928 @{prop[display]"ev n \<Longrightarrow> n = 0 \<or> (EX k. n = Suc(Suc k) \<and> ev k)"} |
|
929 The realisation in Isabelle is a case analysis. |
|
930 A simple example is the proof that @{prop"ev n \<Longrightarrow> ev (n - 2)"}. We |
|
931 already went through the details informally in \autoref{sec:Logic:even}. This |
|
932 is the Isar proof: |
|
933 *} |
|
934 (*<*) |
|
935 notepad |
|
936 begin fix n |
|
937 (*>*) |
|
938 assume "ev n" |
|
939 from this have "ev(n - 2)" |
|
940 proof cases |
|
941 case ev0 thus "ev(n - 2)" by (simp add: ev.ev0) |
|
942 next |
|
943 case (evSS k) thus "ev(n - 2)" by (simp add: ev.evSS) |
|
944 qed |
|
945 (*<*) |
|
946 end |
|
947 (*>*) |
|
948 |
|
949 text{* The key point here is that a case analysis over some inductively |
|
950 defined predicate is triggered by piping the given fact |
|
951 (here: \isacom{from}~@{text this}) into a proof by @{text cases}. |
|
952 Let us examine the assumptions available in each case. In case @{text ev0} |
|
953 we have @{text"n = 0"} and in case @{text evSS} we have @{prop"n = Suc(Suc k)"} |
|
954 and @{prop"ev k"}. In each case the assumptions are available under the name |
|
955 of the case; there is no fine grained naming schema like for induction. |
|
956 |
|
957 Sometimes some rules could not have been used to derive the given fact |
|
958 because constructors clash. As an extreme example consider |
|
959 rule inversion applied to @{prop"ev(Suc 0)"}: neither rule @{text ev0} nor |
|
960 rule @{text evSS} can yield @{prop"ev(Suc 0)"} because @{text"Suc 0"} unifies |
|
961 neither with @{text 0} nor with @{term"Suc(Suc n)"}. Impossible cases do not |
|
962 have to be proved. Hence we can prove anything from @{prop"ev(Suc 0)"}: |
|
963 *} |
|
964 (*<*) |
|
965 notepad begin fix P |
|
966 (*>*) |
|
967 assume "ev(Suc 0)" then have P by cases |
|
968 (*<*) |
|
969 end |
|
970 (*>*) |
|
971 |
|
972 text{* That is, @{prop"ev(Suc 0)"} is simply not provable: *} |
|
973 |
|
974 lemma "\<not> ev(Suc 0)" |
|
975 proof |
|
976 assume "ev(Suc 0)" then show False by cases |
|
977 qed |
|
978 |
|
979 text{* Normally not all cases will be impossible. As a simple exercise, |
|
980 prove that \mbox{@{prop"\<not> ev(Suc(Suc(Suc 0)))"}.} |
|
981 *} |
|
982 |
|
983 (* |
|
984 lemma "\<not> ev(Suc(Suc(Suc 0)))" |
|
985 proof |
|
986 assume "ev(Suc(Suc(Suc 0)))" |
|
987 then show False |
|
988 proof cases |
|
989 case evSS |
|
990 from `ev(Suc 0)` show False by cases |
|
991 qed |
|
992 qed |
|
993 *) |
|
994 |
|
995 (*<*) |
|
996 end |
|
997 (*>*) |
|