1 theory Synopsis |
|
2 imports Base Main |
|
3 begin |
|
4 |
|
5 chapter {* Synopsis *} |
|
6 |
|
7 section {* Notepad *} |
|
8 |
|
9 text {* |
|
10 An Isar proof body serves as mathematical notepad to compose logical |
|
11 content, consisting of types, terms, facts. |
|
12 *} |
|
13 |
|
14 |
|
15 subsection {* Types and terms *} |
|
16 |
|
17 notepad |
|
18 begin |
|
19 txt {* Locally fixed entities: *} |
|
20 fix x -- {* local constant, without any type information yet *} |
|
21 fix x :: 'a -- {* variant with explicit type-constraint for subsequent use*} |
|
22 |
|
23 fix a b |
|
24 assume "a = b" -- {* type assignment at first occurrence in concrete term *} |
|
25 |
|
26 txt {* Definitions (non-polymorphic): *} |
|
27 def x \<equiv> "t::'a" |
|
28 |
|
29 txt {* Abbreviations (polymorphic): *} |
|
30 let ?f = "\<lambda>x. x" |
|
31 term "?f ?f" |
|
32 |
|
33 txt {* Notation: *} |
|
34 write x ("***") |
|
35 end |
|
36 |
|
37 |
|
38 subsection {* Facts *} |
|
39 |
|
40 text {* |
|
41 A fact is a simultaneous list of theorems. |
|
42 *} |
|
43 |
|
44 |
|
45 subsubsection {* Producing facts *} |
|
46 |
|
47 notepad |
|
48 begin |
|
49 |
|
50 txt {* Via assumption (``lambda''): *} |
|
51 assume a: A |
|
52 |
|
53 txt {* Via proof (``let''): *} |
|
54 have b: B sorry |
|
55 |
|
56 txt {* Via abbreviation (``let''): *} |
|
57 note c = a b |
|
58 |
|
59 end |
|
60 |
|
61 |
|
62 subsubsection {* Referencing facts *} |
|
63 |
|
64 notepad |
|
65 begin |
|
66 txt {* Via explicit name: *} |
|
67 assume a: A |
|
68 note a |
|
69 |
|
70 txt {* Via implicit name: *} |
|
71 assume A |
|
72 note this |
|
73 |
|
74 txt {* Via literal proposition (unification with results from the proof text): *} |
|
75 assume A |
|
76 note `A` |
|
77 |
|
78 assume "\<And>x. B x" |
|
79 note `B a` |
|
80 note `B b` |
|
81 end |
|
82 |
|
83 |
|
84 subsubsection {* Manipulating facts *} |
|
85 |
|
86 notepad |
|
87 begin |
|
88 txt {* Instantiation: *} |
|
89 assume a: "\<And>x. B x" |
|
90 note a |
|
91 note a [of b] |
|
92 note a [where x = b] |
|
93 |
|
94 txt {* Backchaining: *} |
|
95 assume 1: A |
|
96 assume 2: "A \<Longrightarrow> C" |
|
97 note 2 [OF 1] |
|
98 note 1 [THEN 2] |
|
99 |
|
100 txt {* Symmetric results: *} |
|
101 assume "x = y" |
|
102 note this [symmetric] |
|
103 |
|
104 assume "x \<noteq> y" |
|
105 note this [symmetric] |
|
106 |
|
107 txt {* Adhoc-simplification (take care!): *} |
|
108 assume "P ([] @ xs)" |
|
109 note this [simplified] |
|
110 end |
|
111 |
|
112 |
|
113 subsubsection {* Projections *} |
|
114 |
|
115 text {* |
|
116 Isar facts consist of multiple theorems. There is notation to project |
|
117 interval ranges. |
|
118 *} |
|
119 |
|
120 notepad |
|
121 begin |
|
122 assume stuff: A B C D |
|
123 note stuff(1) |
|
124 note stuff(2-3) |
|
125 note stuff(2-) |
|
126 end |
|
127 |
|
128 |
|
129 subsubsection {* Naming conventions *} |
|
130 |
|
131 text {* |
|
132 \begin{itemize} |
|
133 |
|
134 \item Lower-case identifiers are usually preferred. |
|
135 |
|
136 \item Facts can be named after the main term within the proposition. |
|
137 |
|
138 \item Facts should \emph{not} be named after the command that |
|
139 introduced them (@{command "assume"}, @{command "have"}). This is |
|
140 misleading and hard to maintain. |
|
141 |
|
142 \item Natural numbers can be used as ``meaningless'' names (more |
|
143 appropriate than @{text "a1"}, @{text "a2"} etc.) |
|
144 |
|
145 \item Symbolic identifiers are supported (e.g. @{text "*"}, @{text |
|
146 "**"}, @{text "***"}). |
|
147 |
|
148 \end{itemize} |
|
149 *} |
|
150 |
|
151 |
|
152 subsection {* Block structure *} |
|
153 |
|
154 text {* |
|
155 The formal notepad is block structured. The fact produced by the last |
|
156 entry of a block is exported into the outer context. |
|
157 *} |
|
158 |
|
159 notepad |
|
160 begin |
|
161 { |
|
162 have a: A sorry |
|
163 have b: B sorry |
|
164 note a b |
|
165 } |
|
166 note this |
|
167 note `A` |
|
168 note `B` |
|
169 end |
|
170 |
|
171 text {* Explicit blocks as well as implicit blocks of nested goal |
|
172 statements (e.g.\ @{command have}) automatically introduce one extra |
|
173 pair of parentheses in reserve. The @{command next} command allows |
|
174 to ``jump'' between these sub-blocks. *} |
|
175 |
|
176 notepad |
|
177 begin |
|
178 |
|
179 { |
|
180 have a: A sorry |
|
181 next |
|
182 have b: B |
|
183 proof - |
|
184 show B sorry |
|
185 next |
|
186 have c: C sorry |
|
187 next |
|
188 have d: D sorry |
|
189 qed |
|
190 } |
|
191 |
|
192 txt {* Alternative version with explicit parentheses everywhere: *} |
|
193 |
|
194 { |
|
195 { |
|
196 have a: A sorry |
|
197 } |
|
198 { |
|
199 have b: B |
|
200 proof - |
|
201 { |
|
202 show B sorry |
|
203 } |
|
204 { |
|
205 have c: C sorry |
|
206 } |
|
207 { |
|
208 have d: D sorry |
|
209 } |
|
210 qed |
|
211 } |
|
212 } |
|
213 |
|
214 end |
|
215 |
|
216 |
|
217 section {* Calculational reasoning \label{sec:calculations-synopsis} *} |
|
218 |
|
219 text {* |
|
220 For example, see @{file "~~/src/HOL/Isar_Examples/Group.thy"}. |
|
221 *} |
|
222 |
|
223 |
|
224 subsection {* Special names in Isar proofs *} |
|
225 |
|
226 text {* |
|
227 \begin{itemize} |
|
228 |
|
229 \item term @{text "?thesis"} --- the main conclusion of the |
|
230 innermost pending claim |
|
231 |
|
232 \item term @{text "\<dots>"} --- the argument of the last explicitly |
|
233 stated result (for infix application this is the right-hand side) |
|
234 |
|
235 \item fact @{text "this"} --- the last result produced in the text |
|
236 |
|
237 \end{itemize} |
|
238 *} |
|
239 |
|
240 notepad |
|
241 begin |
|
242 have "x = y" |
|
243 proof - |
|
244 term ?thesis |
|
245 show ?thesis sorry |
|
246 term ?thesis -- {* static! *} |
|
247 qed |
|
248 term "\<dots>" |
|
249 thm this |
|
250 end |
|
251 |
|
252 text {* Calculational reasoning maintains the special fact called |
|
253 ``@{text calculation}'' in the background. Certain language |
|
254 elements combine primary @{text this} with secondary @{text |
|
255 calculation}. *} |
|
256 |
|
257 |
|
258 subsection {* Transitive chains *} |
|
259 |
|
260 text {* The Idea is to combine @{text this} and @{text calculation} |
|
261 via typical @{text trans} rules (see also @{command |
|
262 print_trans_rules}): *} |
|
263 |
|
264 thm trans |
|
265 thm less_trans |
|
266 thm less_le_trans |
|
267 |
|
268 notepad |
|
269 begin |
|
270 txt {* Plain bottom-up calculation: *} |
|
271 have "a = b" sorry |
|
272 also |
|
273 have "b = c" sorry |
|
274 also |
|
275 have "c = d" sorry |
|
276 finally |
|
277 have "a = d" . |
|
278 |
|
279 txt {* Variant using the @{text "\<dots>"} abbreviation: *} |
|
280 have "a = b" sorry |
|
281 also |
|
282 have "\<dots> = c" sorry |
|
283 also |
|
284 have "\<dots> = d" sorry |
|
285 finally |
|
286 have "a = d" . |
|
287 |
|
288 txt {* Top-down version with explicit claim at the head: *} |
|
289 have "a = d" |
|
290 proof - |
|
291 have "a = b" sorry |
|
292 also |
|
293 have "\<dots> = c" sorry |
|
294 also |
|
295 have "\<dots> = d" sorry |
|
296 finally |
|
297 show ?thesis . |
|
298 qed |
|
299 next |
|
300 txt {* Mixed inequalities (require suitable base type): *} |
|
301 fix a b c d :: nat |
|
302 |
|
303 have "a < b" sorry |
|
304 also |
|
305 have "b \<le> c" sorry |
|
306 also |
|
307 have "c = d" sorry |
|
308 finally |
|
309 have "a < d" . |
|
310 end |
|
311 |
|
312 |
|
313 subsubsection {* Notes *} |
|
314 |
|
315 text {* |
|
316 \begin{itemize} |
|
317 |
|
318 \item The notion of @{text trans} rule is very general due to the |
|
319 flexibility of Isabelle/Pure rule composition. |
|
320 |
|
321 \item User applications may declare their own rules, with some care |
|
322 about the operational details of higher-order unification. |
|
323 |
|
324 \end{itemize} |
|
325 *} |
|
326 |
|
327 |
|
328 subsection {* Degenerate calculations and bigstep reasoning *} |
|
329 |
|
330 text {* The Idea is to append @{text this} to @{text calculation}, |
|
331 without rule composition. *} |
|
332 |
|
333 notepad |
|
334 begin |
|
335 txt {* A vacuous proof: *} |
|
336 have A sorry |
|
337 moreover |
|
338 have B sorry |
|
339 moreover |
|
340 have C sorry |
|
341 ultimately |
|
342 have A and B and C . |
|
343 next |
|
344 txt {* Slightly more content (trivial bigstep reasoning): *} |
|
345 have A sorry |
|
346 moreover |
|
347 have B sorry |
|
348 moreover |
|
349 have C sorry |
|
350 ultimately |
|
351 have "A \<and> B \<and> C" by blast |
|
352 next |
|
353 txt {* More ambitious bigstep reasoning involving structured results: *} |
|
354 have "A \<or> B \<or> C" sorry |
|
355 moreover |
|
356 { assume A have R sorry } |
|
357 moreover |
|
358 { assume B have R sorry } |
|
359 moreover |
|
360 { assume C have R sorry } |
|
361 ultimately |
|
362 have R by blast -- {* ``big-bang integration'' of proof blocks (occasionally fragile) *} |
|
363 end |
|
364 |
|
365 |
|
366 section {* Induction *} |
|
367 |
|
368 subsection {* Induction as Natural Deduction *} |
|
369 |
|
370 text {* In principle, induction is just a special case of Natural |
|
371 Deduction (see also \secref{sec:natural-deduction-synopsis}). For |
|
372 example: *} |
|
373 |
|
374 thm nat.induct |
|
375 print_statement nat.induct |
|
376 |
|
377 notepad |
|
378 begin |
|
379 fix n :: nat |
|
380 have "P n" |
|
381 proof (rule nat.induct) -- {* fragile rule application! *} |
|
382 show "P 0" sorry |
|
383 next |
|
384 fix n :: nat |
|
385 assume "P n" |
|
386 show "P (Suc n)" sorry |
|
387 qed |
|
388 end |
|
389 |
|
390 text {* |
|
391 In practice, much more proof infrastructure is required. |
|
392 |
|
393 The proof method @{method induct} provides: |
|
394 \begin{itemize} |
|
395 |
|
396 \item implicit rule selection and robust instantiation |
|
397 |
|
398 \item context elements via symbolic case names |
|
399 |
|
400 \item support for rule-structured induction statements, with local |
|
401 parameters, premises, etc. |
|
402 |
|
403 \end{itemize} |
|
404 *} |
|
405 |
|
406 notepad |
|
407 begin |
|
408 fix n :: nat |
|
409 have "P n" |
|
410 proof (induct n) |
|
411 case 0 |
|
412 show ?case sorry |
|
413 next |
|
414 case (Suc n) |
|
415 from Suc.hyps show ?case sorry |
|
416 qed |
|
417 end |
|
418 |
|
419 |
|
420 subsubsection {* Example *} |
|
421 |
|
422 text {* |
|
423 The subsequent example combines the following proof patterns: |
|
424 \begin{itemize} |
|
425 |
|
426 \item outermost induction (over the datatype structure of natural |
|
427 numbers), to decompose the proof problem in top-down manner |
|
428 |
|
429 \item calculational reasoning (\secref{sec:calculations-synopsis}) |
|
430 to compose the result in each case |
|
431 |
|
432 \item solving local claims within the calculation by simplification |
|
433 |
|
434 \end{itemize} |
|
435 *} |
|
436 |
|
437 lemma |
|
438 fixes n :: nat |
|
439 shows "(\<Sum>i=0..n. i) = n * (n + 1) div 2" |
|
440 proof (induct n) |
|
441 case 0 |
|
442 have "(\<Sum>i=0..0. i) = (0::nat)" by simp |
|
443 also have "\<dots> = 0 * (0 + 1) div 2" by simp |
|
444 finally show ?case . |
|
445 next |
|
446 case (Suc n) |
|
447 have "(\<Sum>i=0..Suc n. i) = (\<Sum>i=0..n. i) + (n + 1)" by simp |
|
448 also have "\<dots> = n * (n + 1) div 2 + (n + 1)" by (simp add: Suc.hyps) |
|
449 also have "\<dots> = (n * (n + 1) + 2 * (n + 1)) div 2" by simp |
|
450 also have "\<dots> = (Suc n * (Suc n + 1)) div 2" by simp |
|
451 finally show ?case . |
|
452 qed |
|
453 |
|
454 text {* This demonstrates how induction proofs can be done without |
|
455 having to consider the raw Natural Deduction structure. *} |
|
456 |
|
457 |
|
458 subsection {* Induction with local parameters and premises *} |
|
459 |
|
460 text {* Idea: Pure rule statements are passed through the induction |
|
461 rule. This achieves convenient proof patterns, thanks to some |
|
462 internal trickery in the @{method induct} method. |
|
463 |
|
464 Important: Using compact HOL formulae with @{text "\<forall>/\<longrightarrow>"} is a |
|
465 well-known anti-pattern! It would produce useless formal noise. |
|
466 *} |
|
467 |
|
468 notepad |
|
469 begin |
|
470 fix n :: nat |
|
471 fix P :: "nat \<Rightarrow> bool" |
|
472 fix Q :: "'a \<Rightarrow> nat \<Rightarrow> bool" |
|
473 |
|
474 have "P n" |
|
475 proof (induct n) |
|
476 case 0 |
|
477 show "P 0" sorry |
|
478 next |
|
479 case (Suc n) |
|
480 from `P n` show "P (Suc n)" sorry |
|
481 qed |
|
482 |
|
483 have "A n \<Longrightarrow> P n" |
|
484 proof (induct n) |
|
485 case 0 |
|
486 from `A 0` show "P 0" sorry |
|
487 next |
|
488 case (Suc n) |
|
489 from `A n \<Longrightarrow> P n` |
|
490 and `A (Suc n)` show "P (Suc n)" sorry |
|
491 qed |
|
492 |
|
493 have "\<And>x. Q x n" |
|
494 proof (induct n) |
|
495 case 0 |
|
496 show "Q x 0" sorry |
|
497 next |
|
498 case (Suc n) |
|
499 from `\<And>x. Q x n` show "Q x (Suc n)" sorry |
|
500 txt {* Local quantification admits arbitrary instances: *} |
|
501 note `Q a n` and `Q b n` |
|
502 qed |
|
503 end |
|
504 |
|
505 |
|
506 subsection {* Implicit induction context *} |
|
507 |
|
508 text {* The @{method induct} method can isolate local parameters and |
|
509 premises directly from the given statement. This is convenient in |
|
510 practical applications, but requires some understanding of what is |
|
511 going on internally (as explained above). *} |
|
512 |
|
513 notepad |
|
514 begin |
|
515 fix n :: nat |
|
516 fix Q :: "'a \<Rightarrow> nat \<Rightarrow> bool" |
|
517 |
|
518 fix x :: 'a |
|
519 assume "A x n" |
|
520 then have "Q x n" |
|
521 proof (induct n arbitrary: x) |
|
522 case 0 |
|
523 from `A x 0` show "Q x 0" sorry |
|
524 next |
|
525 case (Suc n) |
|
526 from `\<And>x. A x n \<Longrightarrow> Q x n` -- {* arbitrary instances can be produced here *} |
|
527 and `A x (Suc n)` show "Q x (Suc n)" sorry |
|
528 qed |
|
529 end |
|
530 |
|
531 |
|
532 subsection {* Advanced induction with term definitions *} |
|
533 |
|
534 text {* Induction over subexpressions of a certain shape are delicate |
|
535 to formalize. The Isar @{method induct} method provides |
|
536 infrastructure for this. |
|
537 |
|
538 Idea: sub-expressions of the problem are turned into a defined |
|
539 induction variable; often accompanied with fixing of auxiliary |
|
540 parameters in the original expression. *} |
|
541 |
|
542 notepad |
|
543 begin |
|
544 fix a :: "'a \<Rightarrow> nat" |
|
545 fix A :: "nat \<Rightarrow> bool" |
|
546 |
|
547 assume "A (a x)" |
|
548 then have "P (a x)" |
|
549 proof (induct "a x" arbitrary: x) |
|
550 case 0 |
|
551 note prem = `A (a x)` |
|
552 and defn = `0 = a x` |
|
553 show "P (a x)" sorry |
|
554 next |
|
555 case (Suc n) |
|
556 note hyp = `\<And>x. n = a x \<Longrightarrow> A (a x) \<Longrightarrow> P (a x)` |
|
557 and prem = `A (a x)` |
|
558 and defn = `Suc n = a x` |
|
559 show "P (a x)" sorry |
|
560 qed |
|
561 end |
|
562 |
|
563 |
|
564 section {* Natural Deduction \label{sec:natural-deduction-synopsis} *} |
|
565 |
|
566 subsection {* Rule statements *} |
|
567 |
|
568 text {* |
|
569 Isabelle/Pure ``theorems'' are always natural deduction rules, |
|
570 which sometimes happen to consist of a conclusion only. |
|
571 |
|
572 The framework connectives @{text "\<And>"} and @{text "\<Longrightarrow>"} indicate the |
|
573 rule structure declaratively. For example: *} |
|
574 |
|
575 thm conjI |
|
576 thm impI |
|
577 thm nat.induct |
|
578 |
|
579 text {* |
|
580 The object-logic is embedded into the Pure framework via an implicit |
|
581 derivability judgment @{term "Trueprop :: bool \<Rightarrow> prop"}. |
|
582 |
|
583 Thus any HOL formulae appears atomic to the Pure framework, while |
|
584 the rule structure outlines the corresponding proof pattern. |
|
585 |
|
586 This can be made explicit as follows: |
|
587 *} |
|
588 |
|
589 notepad |
|
590 begin |
|
591 write Trueprop ("Tr") |
|
592 |
|
593 thm conjI |
|
594 thm impI |
|
595 thm nat.induct |
|
596 end |
|
597 |
|
598 text {* |
|
599 Isar provides first-class notation for rule statements as follows. |
|
600 *} |
|
601 |
|
602 print_statement conjI |
|
603 print_statement impI |
|
604 print_statement nat.induct |
|
605 |
|
606 |
|
607 subsubsection {* Examples *} |
|
608 |
|
609 text {* |
|
610 Introductions and eliminations of some standard connectives of |
|
611 the object-logic can be written as rule statements as follows. (The |
|
612 proof ``@{command "by"}~@{method blast}'' serves as sanity check.) |
|
613 *} |
|
614 |
|
615 lemma "(P \<Longrightarrow> False) \<Longrightarrow> \<not> P" by blast |
|
616 lemma "\<not> P \<Longrightarrow> P \<Longrightarrow> Q" by blast |
|
617 |
|
618 lemma "P \<Longrightarrow> Q \<Longrightarrow> P \<and> Q" by blast |
|
619 lemma "P \<and> Q \<Longrightarrow> (P \<Longrightarrow> Q \<Longrightarrow> R) \<Longrightarrow> R" by blast |
|
620 |
|
621 lemma "P \<Longrightarrow> P \<or> Q" by blast |
|
622 lemma "Q \<Longrightarrow> P \<or> Q" by blast |
|
623 lemma "P \<or> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R" by blast |
|
624 |
|
625 lemma "(\<And>x. P x) \<Longrightarrow> (\<forall>x. P x)" by blast |
|
626 lemma "(\<forall>x. P x) \<Longrightarrow> P x" by blast |
|
627 |
|
628 lemma "P x \<Longrightarrow> (\<exists>x. P x)" by blast |
|
629 lemma "(\<exists>x. P x) \<Longrightarrow> (\<And>x. P x \<Longrightarrow> R) \<Longrightarrow> R" by blast |
|
630 |
|
631 lemma "x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A \<inter> B" by blast |
|
632 lemma "x \<in> A \<inter> B \<Longrightarrow> (x \<in> A \<Longrightarrow> x \<in> B \<Longrightarrow> R) \<Longrightarrow> R" by blast |
|
633 |
|
634 lemma "x \<in> A \<Longrightarrow> x \<in> A \<union> B" by blast |
|
635 lemma "x \<in> B \<Longrightarrow> x \<in> A \<union> B" by blast |
|
636 lemma "x \<in> A \<union> B \<Longrightarrow> (x \<in> A \<Longrightarrow> R) \<Longrightarrow> (x \<in> B \<Longrightarrow> R) \<Longrightarrow> R" by blast |
|
637 |
|
638 |
|
639 subsection {* Isar context elements *} |
|
640 |
|
641 text {* We derive some results out of the blue, using Isar context |
|
642 elements and some explicit blocks. This illustrates their meaning |
|
643 wrt.\ Pure connectives, without goal states getting in the way. *} |
|
644 |
|
645 notepad |
|
646 begin |
|
647 { |
|
648 fix x |
|
649 have "B x" sorry |
|
650 } |
|
651 have "\<And>x. B x" by fact |
|
652 |
|
653 next |
|
654 |
|
655 { |
|
656 assume A |
|
657 have B sorry |
|
658 } |
|
659 have "A \<Longrightarrow> B" by fact |
|
660 |
|
661 next |
|
662 |
|
663 { |
|
664 def x \<equiv> t |
|
665 have "B x" sorry |
|
666 } |
|
667 have "B t" by fact |
|
668 |
|
669 next |
|
670 |
|
671 { |
|
672 obtain x :: 'a where "B x" sorry |
|
673 have C sorry |
|
674 } |
|
675 have C by fact |
|
676 |
|
677 end |
|
678 |
|
679 |
|
680 subsection {* Pure rule composition *} |
|
681 |
|
682 text {* |
|
683 The Pure framework provides means for: |
|
684 |
|
685 \begin{itemize} |
|
686 |
|
687 \item backward-chaining of rules by @{inference resolution} |
|
688 |
|
689 \item closing of branches by @{inference assumption} |
|
690 |
|
691 \end{itemize} |
|
692 |
|
693 Both principles involve higher-order unification of @{text \<lambda>}-terms |
|
694 modulo @{text "\<alpha>\<beta>\<eta>"}-equivalence (cf.\ Huet and Miller). *} |
|
695 |
|
696 notepad |
|
697 begin |
|
698 assume a: A and b: B |
|
699 thm conjI |
|
700 thm conjI [of A B] -- "instantiation" |
|
701 thm conjI [of A B, OF a b] -- "instantiation and composition" |
|
702 thm conjI [OF a b] -- "composition via unification (trivial)" |
|
703 thm conjI [OF `A` `B`] |
|
704 |
|
705 thm conjI [OF disjI1] |
|
706 end |
|
707 |
|
708 text {* Note: Low-level rule composition is tedious and leads to |
|
709 unreadable~/ unmaintainable expressions in the text. *} |
|
710 |
|
711 |
|
712 subsection {* Structured backward reasoning *} |
|
713 |
|
714 text {* Idea: Canonical proof decomposition via @{command fix}~/ |
|
715 @{command assume}~/ @{command show}, where the body produces a |
|
716 natural deduction rule to refine some goal. *} |
|
717 |
|
718 notepad |
|
719 begin |
|
720 fix A B :: "'a \<Rightarrow> bool" |
|
721 |
|
722 have "\<And>x. A x \<Longrightarrow> B x" |
|
723 proof - |
|
724 fix x |
|
725 assume "A x" |
|
726 show "B x" sorry |
|
727 qed |
|
728 |
|
729 have "\<And>x. A x \<Longrightarrow> B x" |
|
730 proof - |
|
731 { |
|
732 fix x |
|
733 assume "A x" |
|
734 show "B x" sorry |
|
735 } -- "implicit block structure made explicit" |
|
736 note `\<And>x. A x \<Longrightarrow> B x` |
|
737 -- "side exit for the resulting rule" |
|
738 qed |
|
739 end |
|
740 |
|
741 |
|
742 subsection {* Structured rule application *} |
|
743 |
|
744 text {* |
|
745 Idea: Previous facts and new claims are composed with a rule from |
|
746 the context (or background library). |
|
747 *} |
|
748 |
|
749 notepad |
|
750 begin |
|
751 assume r1: "A \<Longrightarrow> B \<Longrightarrow> C" -- {* simple rule (Horn clause) *} |
|
752 |
|
753 have A sorry -- "prefix of facts via outer sub-proof" |
|
754 then have C |
|
755 proof (rule r1) |
|
756 show B sorry -- "remaining rule premises via inner sub-proof" |
|
757 qed |
|
758 |
|
759 have C |
|
760 proof (rule r1) |
|
761 show A sorry |
|
762 show B sorry |
|
763 qed |
|
764 |
|
765 have A and B sorry |
|
766 then have C |
|
767 proof (rule r1) |
|
768 qed |
|
769 |
|
770 have A and B sorry |
|
771 then have C by (rule r1) |
|
772 |
|
773 next |
|
774 |
|
775 assume r2: "A \<Longrightarrow> (\<And>x. B1 x \<Longrightarrow> B2 x) \<Longrightarrow> C" -- {* nested rule *} |
|
776 |
|
777 have A sorry |
|
778 then have C |
|
779 proof (rule r2) |
|
780 fix x |
|
781 assume "B1 x" |
|
782 show "B2 x" sorry |
|
783 qed |
|
784 |
|
785 txt {* The compound rule premise @{prop "\<And>x. B1 x \<Longrightarrow> B2 x"} is better |
|
786 addressed via @{command fix}~/ @{command assume}~/ @{command show} |
|
787 in the nested proof body. *} |
|
788 end |
|
789 |
|
790 |
|
791 subsection {* Example: predicate logic *} |
|
792 |
|
793 text {* |
|
794 Using the above principles, standard introduction and elimination proofs |
|
795 of predicate logic connectives of HOL work as follows. |
|
796 *} |
|
797 |
|
798 notepad |
|
799 begin |
|
800 have "A \<longrightarrow> B" and A sorry |
|
801 then have B .. |
|
802 |
|
803 have A sorry |
|
804 then have "A \<or> B" .. |
|
805 |
|
806 have B sorry |
|
807 then have "A \<or> B" .. |
|
808 |
|
809 have "A \<or> B" sorry |
|
810 then have C |
|
811 proof |
|
812 assume A |
|
813 then show C sorry |
|
814 next |
|
815 assume B |
|
816 then show C sorry |
|
817 qed |
|
818 |
|
819 have A and B sorry |
|
820 then have "A \<and> B" .. |
|
821 |
|
822 have "A \<and> B" sorry |
|
823 then have A .. |
|
824 |
|
825 have "A \<and> B" sorry |
|
826 then have B .. |
|
827 |
|
828 have False sorry |
|
829 then have A .. |
|
830 |
|
831 have True .. |
|
832 |
|
833 have "\<not> A" |
|
834 proof |
|
835 assume A |
|
836 then show False sorry |
|
837 qed |
|
838 |
|
839 have "\<not> A" and A sorry |
|
840 then have B .. |
|
841 |
|
842 have "\<forall>x. P x" |
|
843 proof |
|
844 fix x |
|
845 show "P x" sorry |
|
846 qed |
|
847 |
|
848 have "\<forall>x. P x" sorry |
|
849 then have "P a" .. |
|
850 |
|
851 have "\<exists>x. P x" |
|
852 proof |
|
853 show "P a" sorry |
|
854 qed |
|
855 |
|
856 have "\<exists>x. P x" sorry |
|
857 then have C |
|
858 proof |
|
859 fix a |
|
860 assume "P a" |
|
861 show C sorry |
|
862 qed |
|
863 |
|
864 txt {* Less awkward version using @{command obtain}: *} |
|
865 have "\<exists>x. P x" sorry |
|
866 then obtain a where "P a" .. |
|
867 end |
|
868 |
|
869 text {* Further variations to illustrate Isar sub-proofs involving |
|
870 @{command show}: *} |
|
871 |
|
872 notepad |
|
873 begin |
|
874 have "A \<and> B" |
|
875 proof -- {* two strictly isolated subproofs *} |
|
876 show A sorry |
|
877 next |
|
878 show B sorry |
|
879 qed |
|
880 |
|
881 have "A \<and> B" |
|
882 proof -- {* one simultaneous sub-proof *} |
|
883 show A and B sorry |
|
884 qed |
|
885 |
|
886 have "A \<and> B" |
|
887 proof -- {* two subproofs in the same context *} |
|
888 show A sorry |
|
889 show B sorry |
|
890 qed |
|
891 |
|
892 have "A \<and> B" |
|
893 proof -- {* swapped order *} |
|
894 show B sorry |
|
895 show A sorry |
|
896 qed |
|
897 |
|
898 have "A \<and> B" |
|
899 proof -- {* sequential subproofs *} |
|
900 show A sorry |
|
901 show B using `A` sorry |
|
902 qed |
|
903 end |
|
904 |
|
905 |
|
906 subsubsection {* Example: set-theoretic operators *} |
|
907 |
|
908 text {* There is nothing special about logical connectives (@{text |
|
909 "\<and>"}, @{text "\<or>"}, @{text "\<forall>"}, @{text "\<exists>"} etc.). Operators from |
|
910 set-theory or lattice-theory work analogously. It is only a matter |
|
911 of rule declarations in the library; rules can be also specified |
|
912 explicitly. |
|
913 *} |
|
914 |
|
915 notepad |
|
916 begin |
|
917 have "x \<in> A" and "x \<in> B" sorry |
|
918 then have "x \<in> A \<inter> B" .. |
|
919 |
|
920 have "x \<in> A" sorry |
|
921 then have "x \<in> A \<union> B" .. |
|
922 |
|
923 have "x \<in> B" sorry |
|
924 then have "x \<in> A \<union> B" .. |
|
925 |
|
926 have "x \<in> A \<union> B" sorry |
|
927 then have C |
|
928 proof |
|
929 assume "x \<in> A" |
|
930 then show C sorry |
|
931 next |
|
932 assume "x \<in> B" |
|
933 then show C sorry |
|
934 qed |
|
935 |
|
936 next |
|
937 have "x \<in> \<Inter>A" |
|
938 proof |
|
939 fix a |
|
940 assume "a \<in> A" |
|
941 show "x \<in> a" sorry |
|
942 qed |
|
943 |
|
944 have "x \<in> \<Inter>A" sorry |
|
945 then have "x \<in> a" |
|
946 proof |
|
947 show "a \<in> A" sorry |
|
948 qed |
|
949 |
|
950 have "a \<in> A" and "x \<in> a" sorry |
|
951 then have "x \<in> \<Union>A" .. |
|
952 |
|
953 have "x \<in> \<Union>A" sorry |
|
954 then obtain a where "a \<in> A" and "x \<in> a" .. |
|
955 end |
|
956 |
|
957 |
|
958 section {* Generalized elimination and cases *} |
|
959 |
|
960 subsection {* General elimination rules *} |
|
961 |
|
962 text {* |
|
963 The general format of elimination rules is illustrated by the |
|
964 following typical representatives: |
|
965 *} |
|
966 |
|
967 thm exE -- {* local parameter *} |
|
968 thm conjE -- {* local premises *} |
|
969 thm disjE -- {* split into cases *} |
|
970 |
|
971 text {* |
|
972 Combining these characteristics leads to the following general scheme |
|
973 for elimination rules with cases: |
|
974 |
|
975 \begin{itemize} |
|
976 |
|
977 \item prefix of assumptions (or ``major premises'') |
|
978 |
|
979 \item one or more cases that enable to establish the main conclusion |
|
980 in an augmented context |
|
981 |
|
982 \end{itemize} |
|
983 *} |
|
984 |
|
985 notepad |
|
986 begin |
|
987 assume r: |
|
988 "A1 \<Longrightarrow> A2 \<Longrightarrow> (* assumptions *) |
|
989 (\<And>x y. B1 x y \<Longrightarrow> C1 x y \<Longrightarrow> R) \<Longrightarrow> (* case 1 *) |
|
990 (\<And>x y. B2 x y \<Longrightarrow> C2 x y \<Longrightarrow> R) \<Longrightarrow> (* case 2 *) |
|
991 R (* main conclusion *)" |
|
992 |
|
993 have A1 and A2 sorry |
|
994 then have R |
|
995 proof (rule r) |
|
996 fix x y |
|
997 assume "B1 x y" and "C1 x y" |
|
998 show ?thesis sorry |
|
999 next |
|
1000 fix x y |
|
1001 assume "B2 x y" and "C2 x y" |
|
1002 show ?thesis sorry |
|
1003 qed |
|
1004 end |
|
1005 |
|
1006 text {* Here @{text "?thesis"} is used to refer to the unchanged goal |
|
1007 statement. *} |
|
1008 |
|
1009 |
|
1010 subsection {* Rules with cases *} |
|
1011 |
|
1012 text {* |
|
1013 Applying an elimination rule to some goal, leaves that unchanged |
|
1014 but allows to augment the context in the sub-proof of each case. |
|
1015 |
|
1016 Isar provides some infrastructure to support this: |
|
1017 |
|
1018 \begin{itemize} |
|
1019 |
|
1020 \item native language elements to state eliminations |
|
1021 |
|
1022 \item symbolic case names |
|
1023 |
|
1024 \item method @{method cases} to recover this structure in a |
|
1025 sub-proof |
|
1026 |
|
1027 \end{itemize} |
|
1028 *} |
|
1029 |
|
1030 print_statement exE |
|
1031 print_statement conjE |
|
1032 print_statement disjE |
|
1033 |
|
1034 lemma |
|
1035 assumes A1 and A2 -- {* assumptions *} |
|
1036 obtains |
|
1037 (case1) x y where "B1 x y" and "C1 x y" |
|
1038 | (case2) x y where "B2 x y" and "C2 x y" |
|
1039 sorry |
|
1040 |
|
1041 |
|
1042 subsubsection {* Example *} |
|
1043 |
|
1044 lemma tertium_non_datur: |
|
1045 obtains |
|
1046 (T) A |
|
1047 | (F) "\<not> A" |
|
1048 by blast |
|
1049 |
|
1050 notepad |
|
1051 begin |
|
1052 fix x y :: 'a |
|
1053 have C |
|
1054 proof (cases "x = y" rule: tertium_non_datur) |
|
1055 case T |
|
1056 from `x = y` show ?thesis sorry |
|
1057 next |
|
1058 case F |
|
1059 from `x \<noteq> y` show ?thesis sorry |
|
1060 qed |
|
1061 end |
|
1062 |
|
1063 |
|
1064 subsubsection {* Example *} |
|
1065 |
|
1066 text {* |
|
1067 Isabelle/HOL specification mechanisms (datatype, inductive, etc.) |
|
1068 provide suitable derived cases rules. |
|
1069 *} |
|
1070 |
|
1071 datatype foo = Foo | Bar foo |
|
1072 |
|
1073 notepad |
|
1074 begin |
|
1075 fix x :: foo |
|
1076 have C |
|
1077 proof (cases x) |
|
1078 case Foo |
|
1079 from `x = Foo` show ?thesis sorry |
|
1080 next |
|
1081 case (Bar a) |
|
1082 from `x = Bar a` show ?thesis sorry |
|
1083 qed |
|
1084 end |
|
1085 |
|
1086 |
|
1087 subsection {* Obtaining local contexts *} |
|
1088 |
|
1089 text {* A single ``case'' branch may be inlined into Isar proof text |
|
1090 via @{command obtain}. This proves @{prop "(\<And>x. B x \<Longrightarrow> thesis) \<Longrightarrow> |
|
1091 thesis"} on the spot, and augments the context afterwards. *} |
|
1092 |
|
1093 notepad |
|
1094 begin |
|
1095 fix B :: "'a \<Rightarrow> bool" |
|
1096 |
|
1097 obtain x where "B x" sorry |
|
1098 note `B x` |
|
1099 |
|
1100 txt {* Conclusions from this context may not mention @{term x} again! *} |
|
1101 { |
|
1102 obtain x where "B x" sorry |
|
1103 from `B x` have C sorry |
|
1104 } |
|
1105 note `C` |
|
1106 end |
|
1107 |
|
1108 end |
|