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