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