# HG changeset patch # User berghofe # Date 1312492864 -7200 # Node ID b2158f1996521b6ed7d1dc1b69e668da7807b94b # Parent b63a6bc144cfadde339f205db24038ceb27ce03a# Parent ce4e3090f01a9742010182508d3e6963be5bc6f1 merged diff -r b63a6bc144cf -r b2158f199652 NEWS --- 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 diff -r b63a6bc144cf -r b2158f199652 src/HOL/Complete_Lattice.thy --- 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 \ \B = (\b\B. a \ b)" + assumes sup_Inf: "a \ \B = (\b\B. a \ b)" +begin + +(*lemma dual_complete_distrib_lattice: + "class.complete_distrib_lattice Sup Inf (op \) (op >) sup inf \ \" + 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 \ \{b, c} = (\d\{b, c}. a \ d)" . + then show "a \ b \ c = (a \ b) \ (a \ 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 "_ \ _"} 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 - "\A = (\x. \{y. \f\A. y = f x})" + "\A = (\x. \f\A. f x)" lemma Inf_apply: - "(\A) x = \{y. \f\A. y = f x}" + "(\A) x = (\f\A. f x)" by (simp add: Inf_fun_def) definition - "\A = (\x. \{y. \f\A. y = f x})" + "\A = (\x. \f\A. f x)" lemma Sup_apply: - "(\A) x = \{y. \f\A. y = f x}" + "(\A) x = (\f\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 @@ "(\y\A. f y) x = (\y\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 .. diff -r b63a6bc144cf -r b2158f199652 src/HOL/Orderings.thy --- 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 diff -r b63a6bc144cf -r b2158f199652 src/HOL/Predicate.thy --- 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 \ (op =) y \ x = y" by (auto simp add: mem_def) -instantiation pred :: (type) "{complete_lattice, boolean_algebra}" +instantiation pred :: (type) complete_boolean_algebra begin definition