src/HOL/Isar_Examples/Knaster_Tarski.thy
 author blanchet Thu Sep 11 18:54:36 2014 +0200 (2014-09-11) changeset 58306 117ba6cbe414 parent 41413 64cd30d6b0b8 child 58614 7338eb25226c permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
1 (*  Title:      HOL/Isar_Examples/Knaster_Tarski.thy
2     Author:     Markus Wenzel, TU Muenchen
4 Typical textbook proof example.
5 *)
7 header {* Textbook-style reasoning: the Knaster-Tarski Theorem *}
9 theory Knaster_Tarski
10 imports Main "~~/src/HOL/Library/Lattice_Syntax"
11 begin
14 subsection {* Prose version *}
16 text {* According to the textbook \cite[pages
17   93--94]{davey-priestley}, the Knaster-Tarski fixpoint theorem is as
18   follows.\footnote{We have dualized the argument, and tuned the
19   notation a little bit.}
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}.
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)"}. *}
34 subsection {* Formal versions *}
36 text {* The Isar proof below closely follows the original
37   presentation.  Virtually all of the prose narration has been
38   rephrased in terms of formal Isar language elements.  Just as many
39   textbook-style proofs, there is a strong bias towards forward proof,
40   and several bends in the course of reasoning. *}
42 theorem Knaster_Tarski:
43   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
44   assumes "mono f"
45   shows "\<exists>a. f a = a"
46 proof
47   let ?H = "{u. f u \<le> u}"
48   let ?a = "\<Sqinter>?H"
49   show "f ?a = ?a"
50   proof -
51     {
52       fix x
53       assume "x \<in> ?H"
54       then have "?a \<le> x" by (rule Inf_lower)
55       with `mono f` have "f ?a \<le> f x" ..
56       also from `x \<in> ?H` have "\<dots> \<le> x" ..
57       finally have "f ?a \<le> x" .
58     }
59     then have "f ?a \<le> ?a" by (rule Inf_greatest)
60     {
61       also presume "\<dots> \<le> f ?a"
62       finally (order_antisym) show ?thesis .
63     }
64     from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" ..
65     then have "f ?a \<in> ?H" ..
66     then show "?a \<le> f ?a" by (rule Inf_lower)
67   qed
68 qed
70 text {* Above we have used several advanced Isar language elements,
71   such as explicit block structure and weak assumptions.  Thus we have
72   mimicked the particular way of reasoning of the original text.
74   In the subsequent version the order of reasoning is changed to
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
77   forward manner.  We are certainly more at ease here, requiring only
78   the most basic features of the Isar language. *}
80 theorem Knaster_Tarski':
81   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
82   assumes "mono f"
83   shows "\<exists>a. f a = a"
84 proof
85   let ?H = "{u. f u \<le> u}"
86   let ?a = "\<Sqinter>?H"
87   show "f ?a = ?a"
88   proof (rule order_antisym)
89     show "f ?a \<le> ?a"
90     proof (rule Inf_greatest)
91       fix x
92       assume "x \<in> ?H"
93       then have "?a \<le> x" by (rule Inf_lower)
94       with `mono f` have "f ?a \<le> f x" ..
95       also from `x \<in> ?H` have "\<dots> \<le> x" ..
96       finally show "f ?a \<le> x" .
97     qed
98     show "?a \<le> f ?a"
99     proof (rule Inf_lower)
100       from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" ..
101       then show "f ?a \<in> ?H" ..
102     qed
103   qed
104 qed
106 end