--- 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"
--- 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