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