src/HOL/Isar_examples/KnasterTarski.thy
author wenzelm
Sat Sep 04 21:13:01 1999 +0200 (1999-09-04)
changeset 7480 0a0e0dbe1269
parent 7253 a494a78fea39
child 7761 7fab9592384f
permissions -rw-r--r--
replaced ?? by ?;
wenzelm@6882
     1
(*  Title:      HOL/Isar_examples/KnasterTarski.thy
wenzelm@6882
     2
    ID:         $Id$
wenzelm@6882
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6882
     4
wenzelm@6882
     5
Typical textbook proof example.
wenzelm@6882
     6
*)
wenzelm@6882
     7
wenzelm@6882
     8
wenzelm@6882
     9
theory KnasterTarski = Main:;
wenzelm@6882
    10
wenzelm@7153
    11
text {*
wenzelm@7153
    12
 According to the book ``Introduction to Lattices and Order'' (by
wenzelm@7153
    13
 B. A. Davey and H. A. Priestley, CUP 1990), the Knaster-Tarski
wenzelm@7153
    14
 fixpoint theorem is as follows (pages 93--94).  Note that we have
wenzelm@7153
    15
 dualized their argument, and tuned the notation a little bit.
wenzelm@7153
    16
wenzelm@7153
    17
 \paragraph{The Knaster-Tarski Fixpoint Theorem.}  Let $L$ be a
wenzelm@7153
    18
 complete lattice and $f \colon L \to L$ an order-preserving map.
wenzelm@7153
    19
 Then $\bigwedge \{ x \in L \mid f(x) \le x \}$ is a fixpoint of $f$.
wenzelm@7153
    20
wenzelm@7153
    21
 \textbf{Proof.} Let $H = \{x \in L \mid f(x) \le x\}$ and $a =
wenzelm@7153
    22
 \bigwedge H$.  For all $x \in H$ we have $a \le x$, so $f(a) \le f(x)
wenzelm@7153
    23
 \le x$.  Thus $f(a)$ is a lower bound of $H$, whence $f(a) \le a$.
wenzelm@7153
    24
 We now use this inequality to prove the reverse one (!) and thereby
wenzelm@7153
    25
 complete the proof that $a$ is a fixpoint.  Since $f$ is
wenzelm@7153
    26
 order-preserving, $f(f(a)) \le f(a)$.  This says $f(a) \in H$, so $a
wenzelm@7153
    27
 \le f(a)$.
wenzelm@7153
    28
*};
wenzelm@6883
    29
wenzelm@6893
    30
text {*
wenzelm@7153
    31
 Our proof below closely follows this presentation.  Virtually all of
wenzelm@7153
    32
 the prose narration has been rephrased in terms of formal Isar
wenzelm@7153
    33
 language elements.  Just as many textbook-style proofs, there is a
wenzelm@7153
    34
 strong bias towards forward reasoning, and little hierarchical
wenzelm@6897
    35
 structure.
wenzelm@6893
    36
*};
wenzelm@6882
    37
wenzelm@6939
    38
theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a";
wenzelm@6882
    39
proof;
wenzelm@7480
    40
  let ?H = "{u. f u <= u}";
wenzelm@7480
    41
  let ?a = "Inter ?H";
wenzelm@6882
    42
wenzelm@6897
    43
  assume mono: "mono f";
wenzelm@7480
    44
  show "f ?a = ?a";
wenzelm@7133
    45
  proof -;
wenzelm@6897
    46
    {{;
wenzelm@6897
    47
      fix x;
wenzelm@7480
    48
      assume mem: "x : ?H";
wenzelm@7480
    49
      hence "?a <= x"; by (rule Inter_lower);
wenzelm@7480
    50
      with mono; have "f ?a <= f x"; ..;
wenzelm@6897
    51
      also; from mem; have "... <= x"; ..;
wenzelm@7480
    52
      finally; have "f ?a <= x"; .;
wenzelm@6898
    53
    }};
wenzelm@7480
    54
    hence ge: "f ?a <= ?a"; by (rule Inter_greatest);
wenzelm@6898
    55
    {{;
wenzelm@7480
    56
      also; presume "... <= f ?a";
wenzelm@7480
    57
      finally (order_antisym); show ?thesis; .;
wenzelm@6898
    58
    }};
wenzelm@7480
    59
    from mono ge; have "f (f ?a) <= f ?a"; ..;
wenzelm@7480
    60
    hence "f ?a : ?H"; ..;
wenzelm@7480
    61
    thus "?a <= f ?a"; by (rule Inter_lower);
wenzelm@6898
    62
  qed;
wenzelm@6898
    63
qed;
wenzelm@6898
    64
wenzelm@6898
    65
wenzelm@6882
    66
end;