|
1 (* Title: HOL/Isar_examples/Knaster_Tarski.thy |
|
2 Author: Markus Wenzel, TU Muenchen |
|
3 |
|
4 Typical textbook proof example. |
|
5 *) |
|
6 |
|
7 header {* Textbook-style reasoning: the Knaster-Tarski Theorem *} |
|
8 |
|
9 theory Knaster_Tarski |
|
10 imports Main Lattice_Syntax |
|
11 begin |
|
12 |
|
13 |
|
14 subsection {* Prose version *} |
|
15 |
|
16 text {* |
|
17 According to the textbook \cite[pages 93--94]{davey-priestley}, the |
|
18 Knaster-Tarski fixpoint theorem is as follows.\footnote{We have |
|
19 dualized the argument, and tuned the notation a little bit.} |
|
20 |
|
21 \textbf{The Knaster-Tarski Fixpoint Theorem.} Let @{text L} be a |
|
22 complete lattice and @{text "f: L \<rightarrow> L"} an order-preserving map. |
|
23 Then @{text "\<Sqinter>{x \<in> L | f(x) \<le> x}"} is a fixpoint of @{text f}. |
|
24 |
|
25 \textbf{Proof.} Let @{text "H = {x \<in> L | f(x) \<le> x}"} and @{text "a = |
|
26 \<Sqinter>H"}. For all @{text "x \<in> H"} we have @{text "a \<le> x"}, so @{text |
|
27 "f(a) \<le> f(x) \<le> x"}. Thus @{text "f(a)"} is a lower bound of @{text |
|
28 H}, whence @{text "f(a) \<le> a"}. We now use this inequality to prove |
|
29 the reverse one (!) and thereby complete the proof that @{text a} is |
|
30 a fixpoint. Since @{text f} is order-preserving, @{text "f(f(a)) \<le> |
|
31 f(a)"}. This says @{text "f(a) \<in> H"}, so @{text "a \<le> f(a)"}. |
|
32 *} |
|
33 |
|
34 |
|
35 subsection {* Formal versions *} |
|
36 |
|
37 text {* |
|
38 The Isar proof below closely follows the original presentation. |
|
39 Virtually all of the prose narration has been rephrased in terms of |
|
40 formal Isar language elements. Just as many textbook-style proofs, |
|
41 there is a strong bias towards forward proof, and several bends in |
|
42 the course of reasoning. |
|
43 *} |
|
44 |
|
45 theorem Knaster_Tarski: |
|
46 fixes f :: "'a::complete_lattice \<Rightarrow> 'a" |
|
47 assumes "mono f" |
|
48 shows "\<exists>a. f a = a" |
|
49 proof |
|
50 let ?H = "{u. f u \<le> u}" |
|
51 let ?a = "\<Sqinter>?H" |
|
52 show "f ?a = ?a" |
|
53 proof - |
|
54 { |
|
55 fix x |
|
56 assume "x \<in> ?H" |
|
57 then have "?a \<le> x" by (rule Inf_lower) |
|
58 with `mono f` have "f ?a \<le> f x" .. |
|
59 also from `x \<in> ?H` have "\<dots> \<le> x" .. |
|
60 finally have "f ?a \<le> x" . |
|
61 } |
|
62 then have "f ?a \<le> ?a" by (rule Inf_greatest) |
|
63 { |
|
64 also presume "\<dots> \<le> f ?a" |
|
65 finally (order_antisym) show ?thesis . |
|
66 } |
|
67 from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" .. |
|
68 then have "f ?a \<in> ?H" .. |
|
69 then show "?a \<le> f ?a" by (rule Inf_lower) |
|
70 qed |
|
71 qed |
|
72 |
|
73 text {* |
|
74 Above we have used several advanced Isar language elements, such as |
|
75 explicit block structure and weak assumptions. Thus we have |
|
76 mimicked the particular way of reasoning of the original text. |
|
77 |
|
78 In the subsequent version the order of reasoning is changed to |
|
79 achieve structured top-down decomposition of the problem at the |
|
80 outer level, while only the inner steps of reasoning are done in a |
|
81 forward manner. We are certainly more at ease here, requiring only |
|
82 the most basic features of the Isar language. |
|
83 *} |
|
84 |
|
85 theorem Knaster_Tarski': |
|
86 fixes f :: "'a::complete_lattice \<Rightarrow> 'a" |
|
87 assumes "mono f" |
|
88 shows "\<exists>a. f a = a" |
|
89 proof |
|
90 let ?H = "{u. f u \<le> u}" |
|
91 let ?a = "\<Sqinter>?H" |
|
92 show "f ?a = ?a" |
|
93 proof (rule order_antisym) |
|
94 show "f ?a \<le> ?a" |
|
95 proof (rule Inf_greatest) |
|
96 fix x |
|
97 assume "x \<in> ?H" |
|
98 then have "?a \<le> x" by (rule Inf_lower) |
|
99 with `mono f` have "f ?a \<le> f x" .. |
|
100 also from `x \<in> ?H` have "\<dots> \<le> x" .. |
|
101 finally show "f ?a \<le> x" . |
|
102 qed |
|
103 show "?a \<le> f ?a" |
|
104 proof (rule Inf_lower) |
|
105 from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" .. |
|
106 then show "f ?a \<in> ?H" .. |
|
107 qed |
|
108 qed |
|
109 qed |
|
110 |
|
111 end |