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
```     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 Lattice_Syntax
```
```    11 begin
```
```    12
```
```    13
```
```    14 subsection {* Prose version *}
```
```    15
```
```    16 text {*
```
```    17   According to the textbook \cite[pages 93--94]{davey-priestley}, the
```
```    18   Knaster-Tarski fixpoint theorem is as follows.\footnote{We have
```
```    19   dualized the argument, and tuned the 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
```
```    35 subsection {* Formal versions *}
```
```    36
```
```    37 text {*
```
```    38   The Isar proof below closely follows the original presentation.
```
```    39   Virtually all of the prose narration has been rephrased in terms of
```
```    40   formal Isar language elements.  Just as many textbook-style proofs,
```
```    41   there is a strong bias towards forward proof, and several bends in
```
```    42   the course of reasoning.
```
```    43 *}
```
```    44
```
```    45 theorem Knaster_Tarski:
```
```    46   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
```
```    47   assumes "mono f"
```
```    48   shows "\<exists>a. f a = a"
```
```    49 proof
```
```    50   let ?H = "{u. f u \<le> u}"
```
```    51   let ?a = "\<Sqinter>?H"
```
```    52   show "f ?a = ?a"
```
```    53   proof -
```
```    54     {
```
```    55       fix x
```
```    56       assume "x \<in> ?H"
```
```    57       then have "?a \<le> x" by (rule Inf_lower)
```
```    58       with `mono f` have "f ?a \<le> f x" ..
```
```    59       also from `x \<in> ?H` have "\<dots> \<le> x" ..
```
```    60       finally have "f ?a \<le> x" .
```
```    61     }
```
```    62     then have "f ?a \<le> ?a" by (rule Inf_greatest)
```
```    63     {
```
```    64       also presume "\<dots> \<le> f ?a"
```
```    65       finally (order_antisym) show ?thesis .
```
```    66     }
```
```    67     from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" ..
```
```    68     then have "f ?a \<in> ?H" ..
```
```    69     then show "?a \<le> f ?a" by (rule Inf_lower)
```
```    70   qed
```
```    71 qed
```
```    72
```
```    73 text {*
```
```    74   Above we have used several advanced Isar language elements, such as
```
```    75   explicit block structure and weak assumptions.  Thus we have
```
```    76   mimicked the particular way of reasoning of the original text.
```
```    77
```
```    78   In the subsequent version the order of reasoning is changed to
```
```    79   achieve structured top-down decomposition of the problem at the
```
```    80   outer level, while only the inner steps of reasoning are done in a
```
```    81   forward manner.  We are certainly more at ease here, requiring only
```
```    82   the most basic features of the Isar language.
```
```    83 *}
```
```    84
```
```    85 theorem Knaster_Tarski':
```
```    86   fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
```
```    87   assumes "mono f"
```
```    88   shows "\<exists>a. f a = a"
```
```    89 proof
```
```    90   let ?H = "{u. f u \<le> u}"
```
```    91   let ?a = "\<Sqinter>?H"
```
```    92   show "f ?a = ?a"
```
```    93   proof (rule order_antisym)
```
```    94     show "f ?a \<le> ?a"
```
```    95     proof (rule Inf_greatest)
```
```    96       fix x
```
```    97       assume "x \<in> ?H"
```
```    98       then have "?a \<le> x" by (rule Inf_lower)
```
```    99       with `mono f` have "f ?a \<le> f x" ..
```
```   100       also from `x \<in> ?H` have "\<dots> \<le> x" ..
```
```   101       finally show "f ?a \<le> x" .
```
```   102     qed
```
```   103     show "?a \<le> f ?a"
```
```   104     proof (rule Inf_lower)
```
```   105       from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" ..
```
```   106       then show "f ?a \<in> ?H" ..
```
```   107     qed
```
```   108   qed
```
```   109 qed
```
```   110
```
```   111 end
```