# HG changeset patch
# User wenzelm
# Date 1196114364 -3600
# Node ID f81b3be9dfdd1d4498a146bfa3e10f8137c2f9db
# Parent  d2c6183909287899062b7c12deb07fb3aea7a468
some more lemmas due to Peter Lammich;

diff -r d2c618390928 -r f81b3be9dfdd src/HOL/Lattice/CompleteLattice.thy
--- a/src/HOL/Lattice/CompleteLattice.thy	Mon Nov 26 22:59:21 2007 +0100
+++ b/src/HOL/Lattice/CompleteLattice.thy	Mon Nov 26 22:59:24 2007 +0100
@@ -117,24 +117,70 @@
 *}
 
 theorem Knaster_Tarski:
-  "(\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y) \<Longrightarrow> \<exists>a::'a::complete_lattice. f a = a"
-proof
-  assume mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
-  let ?H = "{u. f u \<sqsubseteq> u}" let ?a = "\<Sqinter>?H"
-  have ge: "f ?a \<sqsubseteq> ?a"
-  proof
-    fix x assume x: "x \<in> ?H"
-    then have "?a \<sqsubseteq> x" ..
-    then have "f ?a \<sqsubseteq> f x" by (rule mono)
-    also from x have "... \<sqsubseteq> x" ..
-    finally show "f ?a \<sqsubseteq> x" .
+  assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
+  shows "\<exists>a::'a::complete_lattice. f a = a \<and> (\<forall>a'. f a' = a' \<longrightarrow> a \<sqsubseteq> a')"
+proof -
+  let ?H = "{u. f u \<sqsubseteq> u}"
+  let ?a = "\<Sqinter>?H"
+  have "f ?a = ?a"
+  proof -
+    have ge: "f ?a \<sqsubseteq> ?a"
+    proof
+      fix x assume x: "x \<in> ?H"
+      then have "?a \<sqsubseteq> x" ..
+      then have "f ?a \<sqsubseteq> f x" by (rule mono)
+      also from x have "... \<sqsubseteq> x" ..
+      finally show "f ?a \<sqsubseteq> x" .
+    qed
+    also have "?a \<sqsubseteq> f ?a"
+    proof
+      from ge have "f (f ?a) \<sqsubseteq> f ?a" by (rule mono)
+      then show "f ?a \<in> ?H" ..
+    qed
+    finally show ?thesis .
   qed
-  also have "?a \<sqsubseteq> f ?a"
-  proof
-    from ge have "f (f ?a) \<sqsubseteq> f ?a" by (rule mono)
-    then show "f ?a \<in> ?H" ..
+  moreover {
+    fix a'
+    assume "f a' = a'"
+    then have "f a' \<sqsubseteq> a'" by (simp only: leq_refl)
+    then have "a' \<in> ?H" ..
+    then have "?a \<sqsubseteq> a'" ..
+  }
+  ultimately show ?thesis by blast
+qed
+
+
+theorem Knaster_Tarski_dual:
+  assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
+  shows "\<exists>a::'a::complete_lattice. f a = a \<and> (\<forall>a'. f a' = a' \<longrightarrow> a' \<sqsubseteq> a)"
+proof -
+  let ?H = "{u. u \<sqsubseteq> f u}"
+  let ?a = "\<Squnion>?H"
+  have "f ?a = ?a"
+  proof -
+    have le: "?a \<sqsubseteq> f ?a"
+    proof
+      fix x assume x: "x \<in> ?H"
+      then have "x \<sqsubseteq> f x" ..
+      also from x have "x \<sqsubseteq> ?a" ..
+      then have "f x \<sqsubseteq> f ?a" by (rule mono)
+      finally show "x \<sqsubseteq> f ?a" .
+    qed
+    have "f ?a \<sqsubseteq> ?a"
+    proof
+      from le have "f ?a \<sqsubseteq> f (f ?a)" by (rule mono)
+      then show "f ?a \<in> ?H" ..
+    qed
+    from this and le show ?thesis by (rule leq_antisym)
   qed
-  finally show "f ?a = ?a" .
+  moreover {
+    fix a'
+    assume "f a' = a'"
+    then have "a' \<sqsubseteq> f a'" by (simp only: leq_refl)
+    then have "a' \<in> ?H" ..
+    then have "a' \<sqsubseteq> ?a" ..
+  }
+  ultimately show ?thesis by blast
 qed
 
 
@@ -146,10 +192,11 @@
 *}
 
 definition
-  bottom :: "'a::complete_lattice"    ("\<bottom>") where
+  bottom :: "'a::complete_lattice"  ("\<bottom>") where
   "\<bottom> = \<Sqinter>UNIV"
+
 definition
-  top :: "'a::complete_lattice"    ("\<top>") where
+  top :: "'a::complete_lattice"  ("\<top>") where
   "\<top> = \<Squnion>UNIV"
 
 lemma bottom_least [intro?]: "\<bottom> \<sqsubseteq> x"
diff -r d2c618390928 -r f81b3be9dfdd src/HOL/Lattice/Lattice.thy
--- a/src/HOL/Lattice/Lattice.thy	Mon Nov 26 22:59:21 2007 +0100
+++ b/src/HOL/Lattice/Lattice.thy	Mon Nov 26 22:59:24 2007 +0100
@@ -582,18 +582,19 @@
 qed
 
 text {*
-  \medskip A semi-morphisms is a function $f$ that preserves the
+  \medskip A semi-morphisms is a function @{text f} that preserves the
   lattice operations in the following manner: @{term "f (x \<sqinter> y) \<sqsubseteq> f x
   \<sqinter> f y"} and @{term "f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"}, respectively.  Any of
   these properties is equivalent with monotonicity.
-*}  (* FIXME dual version !? *)
+*}
 
 theorem meet_semimorph:
   "(\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y) \<equiv> (\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y)"
 proof
   assume morph: "\<And>x y. f (x \<sqinter> y) \<sqsubseteq> f x \<sqinter> f y"
   fix x y :: "'a::lattice"
-  assume "x \<sqsubseteq> y" then have "x \<sqinter> y = x" ..
+  assume "x \<sqsubseteq> y"
+  then have "x \<sqinter> y = x" ..
   then have "x = x \<sqinter> y" ..
   also have "f \<dots> \<sqsubseteq> f x \<sqinter> f y" by (rule morph)
   also have "\<dots> \<sqsubseteq> f y" ..
@@ -611,4 +612,27 @@
   qed
 qed
 
+lemma join_semimorph:
+  "(\<And>x y. f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)) \<equiv> (\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y)"
+proof
+  assume morph: "\<And>x y. f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"
+  fix x y :: "'a::lattice"
+  assume "x \<sqsubseteq> y" then have "x \<squnion> y = y" ..
+  have "f x \<sqsubseteq> f x \<squnion> f y" ..
+  also have "\<dots> \<sqsubseteq> f (x \<squnion> y)" by (rule morph)
+  also from `x \<sqsubseteq> y` have "x \<squnion> y = y" ..
+  finally show "f x \<sqsubseteq> f y" .
+next
+  assume mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f y"
+  show "\<And>x y. f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"
+  proof -
+    fix x y
+    show "f x \<squnion> f y \<sqsubseteq> f (x \<squnion> y)"
+    proof
+      have "x \<sqsubseteq> x \<squnion> y" .. then show "f x \<sqsubseteq> f (x \<squnion> y)" by (rule mono)
+      have "y \<sqsubseteq> x \<squnion> y" .. then show "f y \<sqsubseteq> f (x \<squnion> y)" by (rule mono)
+    qed
+  qed
+qed
+
 end