diff -r e537c91b043d -r 38c15efe603b src/HOL/Lattices.thy --- a/src/HOL/Lattices.thy Fri Nov 30 16:23:52 2007 +0100 +++ b/src/HOL/Lattices.thy Fri Nov 30 20:13:03 2007 +0100 @@ -479,16 +479,34 @@ subsection {* Bool as lattice *} -instance bool :: distrib_lattice - inf_bool_eq: "P \ Q \ P \ Q" - sup_bool_eq: "P \ Q \ P \ Q" +instantiation bool :: distrib_lattice +begin + +definition + inf_bool_eq: "P \ Q \ P \ Q" + +definition + sup_bool_eq: "P \ Q \ P \ Q" + +instance by intro_classes (auto simp add: inf_bool_eq sup_bool_eq le_bool_def) -instance bool :: complete_lattice - Inf_bool_def: "\A \ \x\A. x" - Sup_bool_def: "\A \ \x\A. x" +end + +instantiation bool :: complete_lattice +begin + +definition + Inf_bool_def: "\A \ (\x\A. x)" + +definition + Sup_bool_def: "\A \ (\x\A. x)" + +instance by intro_classes (auto simp add: Inf_bool_def Sup_bool_def le_bool_def) +end + lemma Inf_empty_bool [simp]: "\{}" unfolding Inf_bool_def by auto @@ -506,12 +524,19 @@ subsection {* Set as lattice *} -instance set :: (type) distrib_lattice - inf_set_eq: "A \ B \ A \ B" - sup_set_eq: "A \ B \ A \ B" +instantiation set :: (type) distrib_lattice +begin + +definition + inf_set_eq [code func del]: "A \ B = A \ B" + +definition + sup_set_eq [code func del]: "A \ B = A \ B" + +instance by intro_classes (auto simp add: inf_set_eq sup_set_eq) -lemmas [code func del] = inf_set_eq sup_set_eq +end lemma mono_Int: "mono f \ f (A \ B) \ f A \ f B" apply (fold inf_set_eq sup_set_eq) @@ -523,12 +548,19 @@ apply (erule mono_sup) done -instance set :: (type) complete_lattice - Inf_set_def: "\S \ \S" - Sup_set_def: "\S \ \S" +instantiation set :: (type) complete_lattice +begin + +definition + Inf_set_def [code func del]: "\S \ \S" + +definition + Sup_set_def [code func del]: "\S \ \S" + +instance by intro_classes (auto simp add: Inf_set_def Sup_set_def) -lemmas [code func del] = Inf_set_def Sup_set_def +end lemma top_set_eq: "top = UNIV" by (iprover intro!: subset_antisym subset_UNIV top_greatest) @@ -539,9 +571,16 @@ subsection {* Fun as lattice *} -instance "fun" :: (type, lattice) lattice - inf_fun_eq: "f \ g \ (\x. f x \ g x)" - sup_fun_eq: "f \ g \ (\x. f x \ g x)" +instantiation "fun" :: (type, lattice) lattice +begin + +definition + inf_fun_eq [code func del]: "f \ g = (\x. f x \ g x)" + +definition + sup_fun_eq [code func del]: "f \ g = (\x. f x \ g x)" + +instance apply intro_classes unfolding inf_fun_eq sup_fun_eq apply (auto intro: le_funI) @@ -551,19 +590,26 @@ apply (auto dest: le_funD) done -lemmas [code func del] = inf_fun_eq sup_fun_eq +end instance "fun" :: (type, distrib_lattice) distrib_lattice by default (auto simp add: inf_fun_eq sup_fun_eq sup_inf_distrib1) -instance "fun" :: (type, complete_lattice) complete_lattice - Inf_fun_def: "\A \ (\x. \{y. \f\A. y = f x})" - Sup_fun_def: "\A \ (\x. \{y. \f\A. y = f x})" +instantiation "fun" :: (type, complete_lattice) complete_lattice +begin + +definition + Inf_fun_def [code func del]: "\A = (\x. \{y. \f\A. y = f x})" + +definition + Sup_fun_def [code func del]: "\A = (\x. \{y. \f\A. y = f x})" + +instance by intro_classes (auto simp add: Inf_fun_def Sup_fun_def le_fun_def intro: Inf_lower Sup_upper Inf_greatest Sup_least) -lemmas [code func del] = Inf_fun_def Sup_fun_def +end lemma Inf_empty_fun: "\{} = (\_. \{})"