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