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