1.1 --- a/src/HOL/Complete_Lattice.thy	Wed Aug 03 16:08:02 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Wed Aug 03 23:21:52 2011 +0200
     1.3 @@ -392,7 +392,29 @@
     1.4  
     1.5  end
     1.6  
     1.7 -class complete_boolean_algebra = boolean_algebra + complete_lattice
     1.8 +class complete_distrib_lattice = complete_lattice +
     1.9 +  assumes inf_Sup: "a \<sqinter> \<Squnion>B = (\<Squnion>b\<in>B. a \<sqinter> b)"
    1.10 +  assumes sup_Inf: "a \<squnion> \<Sqinter>B = (\<Sqinter>b\<in>B. a \<squnion> b)"
    1.11 +begin
    1.12 +
    1.13 +(*lemma dual_complete_distrib_lattice:
    1.14 +  "class.complete_distrib_lattice Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom>"
    1.15 +  apply (rule class.complete_distrib_lattice.intro)
    1.16 +  apply (fact dual_complete_lattice)
    1.17 +  apply (rule class.complete_distrib_lattice_axioms.intro)
    1.18 +  apply (simp_all add: inf_Sup sup_Inf)*)
    1.19 +
    1.20 +subclass distrib_lattice proof -- {* Question: is it sufficient to include @{class distrib_lattice}
    1.21 +  and proof @{fact inf_Sup} and @{fact sup_Inf} from that? *}
    1.22 +  fix a b c
    1.23 +  from sup_Inf have "a \<squnion> \<Sqinter>{b, c} = (\<Sqinter>d\<in>{b, c}. a \<squnion> d)" .
    1.24 +  then show "a \<squnion> b \<sqinter> c = (a \<squnion> b) \<sqinter> (a \<squnion> c)" by (simp add: INF_def Inf_binary)
    1.25 +qed
    1.26 +
    1.27 +end
    1.28 +
    1.29 +class complete_boolean_algebra = boolean_algebra + complete_lattice -- {* Question: is this
    1.30 +  also a @{class complete_distrib_lattice}? *}
    1.31  begin
    1.32  
    1.33  lemma dual_complete_boolean_algebra:
    1.34 @@ -489,7 +511,7 @@
    1.35  
    1.36  subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
    1.37  
    1.38 -instantiation bool :: complete_boolean_algebra
    1.39 +instantiation bool :: complete_lattice
    1.40  begin
    1.41  
    1.42  definition
    1.43 @@ -521,26 +543,28 @@
    1.44      by (auto simp add: Bex_def SUP_def Sup_bool_def)
    1.45  qed
    1.46  
    1.47 +instance bool :: "{complete_distrib_lattice, complete_boolean_algebra}" proof
    1.48 +qed (auto simp add: Inf_bool_def Sup_bool_def)
    1.49 +
    1.50  instantiation "fun" :: (type, complete_lattice) complete_lattice
    1.51  begin
    1.52  
    1.53  definition
    1.54 -  "\<Sqinter>A = (\<lambda>x. \<Sqinter>{y. \<exists>f\<in>A. y = f x})"
    1.55 +  "\<Sqinter>A = (\<lambda>x. \<Sqinter>f\<in>A. f x)"
    1.56  
    1.57  lemma Inf_apply:
    1.58 -  "(\<Sqinter>A) x = \<Sqinter>{y. \<exists>f\<in>A. y = f x}"
    1.59 +  "(\<Sqinter>A) x = (\<Sqinter>f\<in>A. f x)"
    1.60    by (simp add: Inf_fun_def)
    1.61  
    1.62  definition
    1.63 -  "\<Squnion>A = (\<lambda>x. \<Squnion>{y. \<exists>f\<in>A. y = f x})"
    1.64 +  "\<Squnion>A = (\<lambda>x. \<Squnion>f\<in>A. f x)"
    1.65  
    1.66  lemma Sup_apply:
    1.67 -  "(\<Squnion>A) x = \<Squnion>{y. \<exists>f\<in>A. y = f x}"
    1.68 +  "(\<Squnion>A) x = (\<Squnion>f\<in>A. f x)"
    1.69    by (simp add: Sup_fun_def)
    1.70  
    1.71  instance proof
    1.72 -qed (auto simp add: le_fun_def Inf_apply Sup_apply
    1.73 -  intro: Inf_lower Sup_upper Inf_greatest Sup_least)
    1.74 +qed (auto simp add: le_fun_def Inf_apply Sup_apply intro: INF_leI le_SUP_I le_INF_I SUP_leI)
    1.75  
    1.76  end
    1.77  
    1.78 @@ -552,6 +576,9 @@
    1.79    "(\<Squnion>y\<in>A. f y) x = (\<Squnion>y\<in>A. f y x)"
    1.80    by (auto intro: arg_cong [of _ _ Sup] simp add: SUP_def Sup_apply)
    1.81  
    1.82 +instance "fun" :: (type, complete_distrib_lattice) complete_distrib_lattice proof
    1.83 +qed (auto simp add: inf_apply sup_apply Inf_apply Sup_apply INF_def SUP_def inf_Sup sup_Inf image_image)
    1.84 +
    1.85  instance "fun" :: (type, complete_boolean_algebra) complete_boolean_algebra ..
    1.86  
    1.87