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