author haftmann Sat, 24 Dec 2011 15:53:07 +0100 changeset 45960 e1b09bfb52f1 parent 45959 184d36538e51 child 45961 5cefe17916a6
lattice type class instances for `set`; added code lemma for Set.bind
```--- a/src/HOL/Complete_Lattices.thy	Sat Dec 24 15:53:07 2011 +0100
+++ b/src/HOL/Complete_Lattices.thy	Sat Dec 24 15:53:07 2011 +0100
@@ -608,6 +608,24 @@

instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..

+instantiation "set" :: (type) complete_lattice
+begin
+
+definition
+  "\<Sqinter>A = {x. \<Sqinter>((\<lambda>B. x \<in> B) ` A)}"
+
+definition
+  "\<Squnion>A = {x. \<Squnion>((\<lambda>B. x \<in> B) ` A)}"
+
+instance proof
+qed (auto simp add: less_eq_set_def Inf_set_def Sup_set_def Inf_bool_def Sup_bool_def le_fun_def)
+
+end
+
+instance "set" :: (type) complete_boolean_algebra
+proof
+qed (auto simp add: INF_def SUP_def Inf_set_def Sup_set_def image_def)
+

subsection {* Inter *}

@@ -624,7 +642,7 @@
have "(\<forall>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<forall>B\<in>A. x \<in> B)"
by auto
then show "x \<in> \<Inter>A \<longleftrightarrow> x \<in> {x. \<forall>B \<in> A. x \<in> B}"
+    by (simp add: Inf_set_def image_def)
qed

lemma Inter_iff [simp,no_atp]: "A \<in> \<Inter>C \<longleftrightarrow> (\<forall>X\<in>C. A \<in> X)"
@@ -807,7 +825,7 @@
have "(\<exists>Q\<in>{P. \<exists>B\<in>A. P \<longleftrightarrow> x \<in> B}. Q) \<longleftrightarrow> (\<exists>B\<in>A. x \<in> B)"
by auto
then show "x \<in> \<Union>A \<longleftrightarrow> x \<in> {x. \<exists>B\<in>A. x \<in> B}"
+    by (simp add: Sup_set_def image_def)
qed

lemma Union_iff [simp, no_atp]:
@@ -906,6 +924,10 @@
"(\<Union>x\<in>A. B x) = {y. \<exists>x\<in>A. y \<in> B x}"