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