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