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