1.1 --- a/src/HOL/Isar_examples/KnasterTarski.thy	Tue Mar 31 13:34:48 2009 +0200
     1.2 +++ b/src/HOL/Isar_examples/KnasterTarski.thy	Tue Mar 31 14:09:28 2009 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Isar_examples/KnasterTarski.thy
     1.5 -    ID:         $Id$
     1.6      Author:     Markus Wenzel, TU Muenchen
     1.7  
     1.8  Typical textbook proof example.
     1.9 @@ -7,100 +6,104 @@
    1.10  
    1.11  header {* Textbook-style reasoning: the Knaster-Tarski Theorem *}
    1.12  
    1.13 -theory KnasterTarski imports Main begin
    1.14 +theory KnasterTarski
    1.15 +imports Main Lattice_Syntax
    1.16 +begin
    1.17  
    1.18  
    1.19  subsection {* Prose version *}
    1.20  
    1.21  text {*
    1.22 - According to the textbook \cite[pages 93--94]{davey-priestley}, the
    1.23 - Knaster-Tarski fixpoint theorem is as follows.\footnote{We have
    1.24 - dualized the argument, and tuned the notation a little bit.}
    1.25 +  According to the textbook \cite[pages 93--94]{davey-priestley}, the
    1.26 +  Knaster-Tarski fixpoint theorem is as follows.\footnote{We have
    1.27 +  dualized the argument, and tuned the notation a little bit.}
    1.28  
    1.29 - \medskip \textbf{The Knaster-Tarski Fixpoint Theorem.}  Let $L$ be a
    1.30 - complete lattice and $f \colon L \to L$ an order-preserving map.
    1.31 - Then $\bigwedge \{ x \in L \mid f(x) \le x \}$ is a fixpoint of $f$.
    1.32 +  \textbf{The Knaster-Tarski Fixpoint Theorem.}  Let @{text L} be a
    1.33 +  complete lattice and @{text "f: L \<rightarrow> L"} an order-preserving map.
    1.34 +  Then @{text "\<Sqinter>{x \<in> L | f(x) \<le> x}"} is a fixpoint of @{text f}.
    1.35  
    1.36 - \textbf{Proof.} Let $H = \{x \in L \mid f(x) \le x\}$ and $a =
    1.37 - \bigwedge H$.  For all $x \in H$ we have $a \le x$, so $f(a) \le f(x)
    1.38 - \le x$.  Thus $f(a)$ is a lower bound of $H$, whence $f(a) \le a$.
    1.39 - We now use this inequality to prove the reverse one (!) and thereby
    1.40 - complete the proof that $a$ is a fixpoint.  Since $f$ is
    1.41 - order-preserving, $f(f(a)) \le f(a)$.  This says $f(a) \in H$, so $a
    1.42 - \le f(a)$.
    1.43 +  \textbf{Proof.} Let @{text "H = {x \<in> L | f(x) \<le> x}"} and @{text "a =
    1.44 +  \<Sqinter>H"}.  For all @{text "x \<in> H"} we have @{text "a \<le> x"}, so @{text
    1.45 +  "f(a) \<le> f(x) \<le> x"}.  Thus @{text "f(a)"} is a lower bound of @{text
    1.46 +  H}, whence @{text "f(a) \<le> a"}.  We now use this inequality to prove
    1.47 +  the reverse one (!) and thereby complete the proof that @{text a} is
    1.48 +  a fixpoint.  Since @{text f} is order-preserving, @{text "f(f(a)) \<le>
    1.49 +  f(a)"}.  This says @{text "f(a) \<in> H"}, so @{text "a \<le> f(a)"}.
    1.50  *}
    1.51  
    1.52  
    1.53  subsection {* Formal versions *}
    1.54  
    1.55  text {*
    1.56 - The Isar proof below closely follows the original presentation.
    1.57 - Virtually all of the prose narration has been rephrased in terms of
    1.58 - formal Isar language elements.  Just as many textbook-style proofs,
    1.59 - there is a strong bias towards forward proof, and several bends
    1.60 - in the course of reasoning.
    1.61 +  The Isar proof below closely follows the original presentation.
    1.62 +  Virtually all of the prose narration has been rephrased in terms of
    1.63 +  formal Isar language elements.  Just as many textbook-style proofs,
    1.64 +  there is a strong bias towards forward proof, and several bends in
    1.65 +  the course of reasoning.
    1.66  *}
    1.67  
    1.68 -theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a"
    1.69 +theorem Knaster_Tarski:
    1.70 +  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
    1.71 +  assumes "mono f"
    1.72 +  shows "\<exists>a. f a = a"
    1.73  proof
    1.74 -  let ?H = "{u. f u <= u}"
    1.75 -  let ?a = "Inter ?H"
    1.76 -
    1.77 -  assume mono: "mono f"
    1.78 +  let ?H = "{u. f u \<le> u}"
    1.79 +  let ?a = "\<Sqinter>?H"
    1.80    show "f ?a = ?a"
    1.81    proof -
    1.82      {
    1.83        fix x
    1.84 -      assume H: "x : ?H"
    1.85 -      hence "?a <= x" by (rule Inter_lower)
    1.86 -      with mono have "f ?a <= f x" ..
    1.87 -      also from H have "... <= x" ..
    1.88 -      finally have "f ?a <= x" .
    1.89 +      assume "x \<in> ?H"
    1.90 +      then have "?a \<le> x" by (rule Inf_lower)
    1.91 +      with `mono f` have "f ?a \<le> f x" ..
    1.92 +      also from `x \<in> ?H` have "\<dots> \<le> x" ..
    1.93 +      finally have "f ?a \<le> x" .
    1.94      }
    1.95 -    hence ge: "f ?a <= ?a" by (rule Inter_greatest)
    1.96 +    then have "f ?a \<le> ?a" by (rule Inf_greatest)
    1.97      {
    1.98 -      also presume "... <= f ?a"
    1.99 +      also presume "\<dots> \<le> f ?a"
   1.100        finally (order_antisym) show ?thesis .
   1.101      }
   1.102 -    from mono ge have "f (f ?a) <= f ?a" ..
   1.103 -    hence "f ?a : ?H" by simp
   1.104 -    thus "?a <= f ?a" by (rule Inter_lower)
   1.105 +    from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" ..
   1.106 +    then have "f ?a \<in> ?H" ..
   1.107 +    then show "?a \<le> f ?a" by (rule Inf_lower)
   1.108    qed
   1.109  qed
   1.110  
   1.111  text {*
   1.112 - Above we have used several advanced Isar language elements, such as
   1.113 - explicit block structure and weak assumptions.  Thus we have mimicked
   1.114 - the particular way of reasoning of the original text.
   1.115 +  Above we have used several advanced Isar language elements, such as
   1.116 +  explicit block structure and weak assumptions.  Thus we have
   1.117 +  mimicked the particular way of reasoning of the original text.
   1.118  
   1.119 - In the subsequent version the order of reasoning is changed to
   1.120 - achieve structured top-down decomposition of the problem at the outer
   1.121 - level, while only the inner steps of reasoning are done in a forward
   1.122 - manner.  We are certainly more at ease here, requiring only the most
   1.123 - basic features of the Isar language.
   1.124 +  In the subsequent version the order of reasoning is changed to
   1.125 +  achieve structured top-down decomposition of the problem at the
   1.126 +  outer level, while only the inner steps of reasoning are done in a
   1.127 +  forward manner.  We are certainly more at ease here, requiring only
   1.128 +  the most basic features of the Isar language.
   1.129  *}
   1.130  
   1.131 -theorem KnasterTarski': "mono f ==> EX a::'a set. f a = a"
   1.132 +theorem Knaster_Tarski':
   1.133 +  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
   1.134 +  assumes "mono f"
   1.135 +  shows "\<exists>a. f a = a"
   1.136  proof
   1.137 -  let ?H = "{u. f u <= u}"
   1.138 -  let ?a = "Inter ?H"
   1.139 -
   1.140 -  assume mono: "mono f"
   1.141 +  let ?H = "{u. f u \<le> u}"
   1.142 +  let ?a = "\<Sqinter>?H"
   1.143    show "f ?a = ?a"
   1.144    proof (rule order_antisym)
   1.145 -    show ge: "f ?a <= ?a"
   1.146 -    proof (rule Inter_greatest)
   1.147 +    show "f ?a \<le> ?a"
   1.148 +    proof (rule Inf_greatest)
   1.149        fix x
   1.150 -      assume H: "x : ?H"
   1.151 -      hence "?a <= x" by (rule Inter_lower)
   1.152 -      with mono have "f ?a <= f x" ..
   1.153 -      also from H have "... <= x" ..
   1.154 -      finally show "f ?a <= x" .
   1.155 +      assume "x \<in> ?H"
   1.156 +      then have "?a \<le> x" by (rule Inf_lower)
   1.157 +      with `mono f` have "f ?a \<le> f x" ..
   1.158 +      also from `x \<in> ?H` have "\<dots> \<le> x" ..
   1.159 +      finally show "f ?a \<le> x" .
   1.160      qed
   1.161 -    show "?a <= f ?a"
   1.162 -    proof (rule Inter_lower)
   1.163 -      from mono ge have "f (f ?a) <= f ?a" ..
   1.164 -      thus "f ?a : ?H" by simp
   1.165 +    show "?a \<le> f ?a"
   1.166 +    proof (rule Inf_lower)
   1.167 +      from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" ..
   1.168 +      then show "f ?a \<in> ?H" ..
   1.169      qed
   1.170    qed
   1.171  qed