src/HOL/Isar_examples/KnasterTarski.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 16417 9bc16273c2d4 child 26812 c0fa62fa0e5b permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     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