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