# HG changeset patch
# User haftmann
# Date 1324738387 -3600
# Node ID e1b09bfb52f1f059cfde41ddbbbdcf75d81bd666
# Parent  184d36538e51d31597223e778e6d69f53e87d4e5
lattice type class instances for `set`; added code lemma for Set.bind

diff -r 184d36538e51 -r e1b09bfb52f1 src/HOL/Complete_Lattices.thy
--- 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_fun_def) (simp add: mem_def)
+    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_fun_def) (simp add: mem_def)
+    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}"
   by (auto simp add: SUP_def)
 
+lemma bind_UNION [code]:
+  "Set.bind A f = UNION A f"
+  by (simp add: bind_def UNION_eq)
+
 lemma Union_image_eq [simp]:
   "\<Union>(B ` A) = (\<Union>x\<in>A. B x)"
   by (rule sym) (fact SUP_def)