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