merged

--- a/NEWS	Thu Aug 04 17:40:48 2011 +0200
+++ b/NEWS	Thu Aug 04 23:21:04 2011 +0200
@@ -67,6 +67,7 @@
 generalized theorems INF_cong and SUP_cong.  New type classes for complete
 boolean algebras and complete linear orders.  Lemmas Inf_less_iff,
 less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder.
+Changes proposition of lemmas Inf_fun_def, Sup_fun_def, Inf_apply, Sup_apply.
 More consistent and less misunderstandable names:
   INFI_def ~> INF_def
   SUPR_def ~> SUP_def

--- a/src/HOL/Complete_Lattice.thy	Thu Aug 04 17:40:48 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Thu Aug 04 23:21:04 2011 +0200
@@ -392,7 +392,29 @@
 
 end
 
-class complete_boolean_algebra = boolean_algebra + complete_lattice
+class complete_distrib_lattice = complete_lattice +
+  assumes inf_Sup: "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
+  assumes sup_Inf: "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
+begin
+
+(*lemma dual_complete_distrib_lattice:
+  "class.complete_distrib_lattice Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom>"
+  apply (rule class.complete_distrib_lattice.intro)
+  apply (fact dual_complete_lattice)
+  apply (rule class.complete_distrib_lattice_axioms.intro)
+  apply (simp_all add: inf_Sup sup_Inf)*)
+
+subclass distrib_lattice proof -- {* Question: is it sufficient to include @{class distrib_lattice}
+  and prove @{text inf_Sup} and @{text sup_Inf} from that? *}
+  fix a b c
+  from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" .
+  then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_binary)
+qed
+
+end
+
+class complete_boolean_algebra = boolean_algebra + complete_lattice -- {* Question: is this
+  also a @{class complete_distrib_lattice}? *}
 begin
 
 lemma dual_complete_boolean_algebra:
@@ -489,7 +511,7 @@
 
 subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
 
-instantiation bool :: complete_boolean_algebra
+instantiation bool :: complete_lattice
 begin
 
 definition
@@ -521,26 +543,28 @@
     by (auto simp add: Bex_def SUP_def Sup_bool_def)
 qed
 
+instance bool :: "{complete_distrib_lattice, complete_boolean_algebra}" proof
+qed (auto simp add: Inf_bool_def Sup_bool_def)
+
 instantiation "fun" :: (type, complete_lattice) complete_lattice
 begin
 
 definition
-  "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
+  "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)"
 
 lemma Inf_apply:
-  "(\<Sqinter>A) x = \<Sqinter>{y. \<exists>f\<in>A. y = f x}"
+  "(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)"
   by (simp add: Inf_fun_def)
 
 definition
-  "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
+  "\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)"
 
 lemma Sup_apply:
-  "(\<Squnion>A) x = \<Squnion>{y. \<exists>f\<in>A. y = f x}"
+  "(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)"
   by (simp add: Sup_fun_def)
 
 instance proof
-qed (auto simp add: le_fun_def Inf_apply Sup_apply
-  intro: Inf_lower Sup_upper Inf_greatest Sup_least)
+qed (auto simp add: le_fun_def Inf_apply Sup_apply intro: INF_leI le_SUP_I le_INF_I SUP_leI)
 
 end
 
@@ -552,6 +576,9 @@
   "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
   by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def Sup_apply)
 
+instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice proof
+qed (auto simp add: inf_apply sup_apply Inf_apply Sup_apply INF_def SUP_def inf_Sup sup_Inf image_image)
+
 instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
 
 

--- a/src/HOL/Orderings.thy	Thu Aug 04 17:40:48 2011 +0200
+++ b/src/HOL/Orderings.thy	Thu Aug 04 23:21:04 2011 +0200
@@ -1246,7 +1246,7 @@
 
 subsection {* Order on bool *}
 
-instantiation bool :: "{order, bot, top}"
+instantiation bool :: "{bot, top}"
 begin
 
 definition

--- a/src/HOL/Predicate.thy	Thu Aug 04 17:40:48 2011 +0200
+++ b/src/HOL/Predicate.thy	Thu Aug 04 23:21:04 2011 +0200
@@ -431,7 +431,7 @@
   "x \<in> (op =) y \<longleftrightarrow> x = y"
   by (auto simp add: mem_def)
 
-instantiation pred :: (type) "{complete_lattice, boolean_algebra}"
+instantiation pred :: (type) complete_boolean_algebra
 begin
 
 definition