haftmann@21249: (* Title: HOL/Lattices.thy haftmann@21249: Author: Tobias Nipkow haftmann@21249: *) haftmann@21249: haftmann@22454: header {* Abstract lattices *} haftmann@21249: haftmann@21249: theory Lattices haftmann@35121: imports Orderings Groups haftmann@21249: begin haftmann@21249: haftmann@35301: subsection {* Abstract semilattice *} haftmann@35301: haftmann@35301: text {* haftmann@35301: This locales provide a basic structure for interpretation into haftmann@35301: bigger structures; extensions require careful thinking, otherwise haftmann@35301: undesired effects may occur due to interpretation. haftmann@35301: *} haftmann@35301: haftmann@35301: locale semilattice = abel_semigroup + haftmann@35301: assumes idem [simp]: "f a a = a" haftmann@35301: begin haftmann@35301: haftmann@35301: lemma left_idem [simp]: haftmann@35301: "f a (f a b) = f a b" haftmann@35301: by (simp add: assoc [symmetric]) haftmann@35301: haftmann@35301: end haftmann@35301: haftmann@35301: haftmann@35301: subsection {* Idempotent semigroup *} haftmann@35301: haftmann@35301: class ab_semigroup_idem_mult = ab_semigroup_mult + haftmann@35301: assumes mult_idem: "x * x = x" haftmann@35301: haftmann@35301: sublocale ab_semigroup_idem_mult < times!: semilattice times proof haftmann@35301: qed (fact mult_idem) haftmann@35301: haftmann@35301: context ab_semigroup_idem_mult haftmann@35301: begin haftmann@35301: haftmann@35301: lemmas mult_left_idem = times.left_idem haftmann@35301: haftmann@35301: end haftmann@35301: haftmann@35301: haftmann@35724: subsection {* Concrete lattices *} haftmann@21249: haftmann@25206: notation wenzelm@25382: less_eq (infix "\" 50) and haftmann@32568: less (infix "\" 50) and haftmann@32568: top ("\") and haftmann@32568: bot ("\") haftmann@25206: haftmann@35028: class semilattice_inf = order + haftmann@21249: fixes inf :: "'a \ 'a \ 'a" (infixl "\" 70) haftmann@22737: assumes inf_le1 [simp]: "x \ y \ x" haftmann@22737: and inf_le2 [simp]: "x \ y \ y" nipkow@21733: and inf_greatest: "x \ y \ x \ z \ x \ y \ z" haftmann@21249: haftmann@35028: class semilattice_sup = order + haftmann@21249: fixes sup :: "'a \ 'a \ 'a" (infixl "\" 65) haftmann@22737: assumes sup_ge1 [simp]: "x \ x \ y" haftmann@22737: and sup_ge2 [simp]: "y \ x \ y" nipkow@21733: and sup_least: "y \ x \ z \ x \ y \ z \ x" haftmann@26014: begin haftmann@26014: haftmann@26014: text {* Dual lattice *} haftmann@26014: haftmann@31991: lemma dual_semilattice: haftmann@36635: "class.semilattice_inf (op \) (op >) sup" haftmann@36635: by (rule class.semilattice_inf.intro, rule dual_order) haftmann@27682: (unfold_locales, simp_all add: sup_least) haftmann@26014: haftmann@26014: end haftmann@21249: haftmann@35028: class lattice = semilattice_inf + semilattice_sup haftmann@21249: wenzelm@25382: haftmann@28562: subsubsection {* Intro and elim rules*} nipkow@21733: haftmann@35028: context semilattice_inf nipkow@21733: begin haftmann@21249: haftmann@32064: lemma le_infI1: haftmann@32064: "a \ x \ a \ b \ x" haftmann@32064: by (rule order_trans) auto haftmann@21249: haftmann@32064: lemma le_infI2: haftmann@32064: "b \ x \ a \ b \ x" haftmann@32064: by (rule order_trans) auto nipkow@21733: haftmann@32064: lemma le_infI: "x \ a \ x \ b \ x \ a \ b" huffman@36008: by (rule inf_greatest) (* FIXME: duplicate lemma *) haftmann@21249: haftmann@32064: lemma le_infE: "x \ a \ b \ (x \ a \ x \ b \ P) \ P" huffman@36008: by (blast intro: order_trans inf_le1 inf_le2) haftmann@21249: nipkow@21734: lemma le_inf_iff [simp]: haftmann@32064: "x \ y \ z \ x \ y \ x \ z" haftmann@32064: by (blast intro: le_infI elim: le_infE) nipkow@21733: haftmann@32064: lemma le_iff_inf: haftmann@32064: "x \ y \ x \ y = x" haftmann@32064: by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1]) haftmann@21249: huffman@36008: lemma inf_mono: "a \ c \ b \ d \ a \ b \ c \ d" huffman@36008: by (fast intro: inf_greatest le_infI1 le_infI2) huffman@36008: haftmann@25206: lemma mono_inf: haftmann@35028: fixes f :: "'a \ 'b\semilattice_inf" haftmann@34007: shows "mono f \ f (A \ B) \ f A \ f B" haftmann@25206: by (auto simp add: mono_def intro: Lattices.inf_greatest) nipkow@21733: haftmann@25206: end nipkow@21733: haftmann@35028: context semilattice_sup nipkow@21733: begin haftmann@21249: haftmann@32064: lemma le_supI1: haftmann@32064: "x \ a \ x \ a \ b" haftmann@25062: by (rule order_trans) auto haftmann@21249: haftmann@32064: lemma le_supI2: haftmann@32064: "x \ b \ x \ a \ b" haftmann@25062: by (rule order_trans) auto nipkow@21733: haftmann@32064: lemma le_supI: haftmann@32064: "a \ x \ b \ x \ a \ b \ x" huffman@36008: by (rule sup_least) (* FIXME: duplicate lemma *) haftmann@21249: haftmann@32064: lemma le_supE: haftmann@32064: "a \ b \ x \ (a \ x \ b \ x \ P) \ P" huffman@36008: by (blast intro: order_trans sup_ge1 sup_ge2) haftmann@22422: haftmann@32064: lemma le_sup_iff [simp]: haftmann@32064: "x \ y \ z \ x \ z \ y \ z" haftmann@32064: by (blast intro: le_supI elim: le_supE) nipkow@21733: haftmann@32064: lemma le_iff_sup: haftmann@32064: "x \ y \ x \ y = y" haftmann@32064: by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1]) nipkow@21734: huffman@36008: lemma sup_mono: "a \ c \ b \ d \ a \ b \ c \ d" huffman@36008: by (fast intro: sup_least le_supI1 le_supI2) huffman@36008: haftmann@25206: lemma mono_sup: haftmann@35028: fixes f :: "'a \ 'b\semilattice_sup" haftmann@34007: shows "mono f \ f A \ f B \ f (A \ B)" haftmann@25206: by (auto simp add: mono_def intro: Lattices.sup_least) nipkow@21733: haftmann@25206: end haftmann@23878: nipkow@21733: haftmann@32064: subsubsection {* Equational laws *} haftmann@21249: haftmann@35028: sublocale semilattice_inf < inf!: semilattice inf haftmann@34973: proof haftmann@34973: fix a b c haftmann@34973: show "(a \ b) \ c = a \ (b \ c)" haftmann@34973: by (rule antisym) (auto intro: le_infI1 le_infI2) haftmann@34973: show "a \ b = b \ a" haftmann@34973: by (rule antisym) auto haftmann@34973: show "a \ a = a" haftmann@34973: by (rule antisym) auto haftmann@34973: qed haftmann@34973: haftmann@35028: context semilattice_inf nipkow@21733: begin nipkow@21733: haftmann@34973: lemma inf_assoc: "(x \ y) \ z = x \ (y \ z)" haftmann@34973: by (fact inf.assoc) nipkow@21733: haftmann@34973: lemma inf_commute: "(x \ y) = (y \ x)" haftmann@34973: by (fact inf.commute) nipkow@21733: haftmann@34973: lemma inf_left_commute: "x \ (y \ z) = y \ (x \ z)" haftmann@34973: by (fact inf.left_commute) nipkow@21733: haftmann@34973: lemma inf_idem: "x \ x = x" haftmann@34973: by (fact inf.idem) haftmann@34973: haftmann@34973: lemma inf_left_idem: "x \ (x \ y) = x \ y" haftmann@34973: by (fact inf.left_idem) nipkow@21733: haftmann@32642: lemma inf_absorb1: "x \ y \ x \ y = x" haftmann@32064: by (rule antisym) auto nipkow@21733: haftmann@32642: lemma inf_absorb2: "y \ x \ x \ y = y" haftmann@32064: by (rule antisym) auto haftmann@34973: haftmann@32064: lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem nipkow@21733: nipkow@21733: end nipkow@21733: haftmann@35028: sublocale semilattice_sup < sup!: semilattice sup haftmann@34973: proof haftmann@34973: fix a b c haftmann@34973: show "(a \ b) \ c = a \ (b \ c)" haftmann@34973: by (rule antisym) (auto intro: le_supI1 le_supI2) haftmann@34973: show "a \ b = b \ a" haftmann@34973: by (rule antisym) auto haftmann@34973: show "a \ a = a" haftmann@34973: by (rule antisym) auto haftmann@34973: qed haftmann@34973: haftmann@35028: context semilattice_sup nipkow@21733: begin haftmann@21249: haftmann@34973: lemma sup_assoc: "(x \ y) \ z = x \ (y \ z)" haftmann@34973: by (fact sup.assoc) nipkow@21733: haftmann@34973: lemma sup_commute: "(x \ y) = (y \ x)" haftmann@34973: by (fact sup.commute) nipkow@21733: haftmann@34973: lemma sup_left_commute: "x \ (y \ z) = y \ (x \ z)" haftmann@34973: by (fact sup.left_commute) nipkow@21733: haftmann@34973: lemma sup_idem: "x \ x = x" haftmann@34973: by (fact sup.idem) haftmann@34973: haftmann@34973: lemma sup_left_idem: "x \ (x \ y) = x \ y" haftmann@34973: by (fact sup.left_idem) nipkow@21733: haftmann@32642: lemma sup_absorb1: "y \ x \ x \ y = x" haftmann@32064: by (rule antisym) auto nipkow@21733: haftmann@32642: lemma sup_absorb2: "x \ y \ x \ y = y" haftmann@32064: by (rule antisym) auto haftmann@21249: haftmann@32064: lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem nipkow@21733: nipkow@21733: end haftmann@21249: nipkow@21733: context lattice nipkow@21733: begin nipkow@21733: haftmann@31991: lemma dual_lattice: haftmann@36635: "class.lattice (op \) (op >) sup inf" haftmann@36635: by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order) haftmann@31991: (unfold_locales, auto) haftmann@31991: nipkow@21733: lemma inf_sup_absorb: "x \ (x \ y) = x" haftmann@25102: by (blast intro: antisym inf_le1 inf_greatest sup_ge1) nipkow@21733: nipkow@21733: lemma sup_inf_absorb: "x \ (x \ y) = x" haftmann@25102: by (blast intro: antisym sup_ge1 sup_least inf_le1) nipkow@21733: haftmann@32064: lemmas inf_sup_aci = inf_aci sup_aci nipkow@21734: haftmann@22454: lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2 haftmann@22454: nipkow@21734: text{* Towards distributivity *} haftmann@21249: nipkow@21734: lemma distrib_sup_le: "x \ (y \ z) \ (x \ y) \ (x \ z)" haftmann@32064: by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) nipkow@21734: nipkow@21734: lemma distrib_inf_le: "(x \ y) \ (x \ z) \ x \ (y \ z)" haftmann@32064: by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) nipkow@21734: nipkow@21734: text{* If you have one of them, you have them all. *} haftmann@21249: nipkow@21733: lemma distrib_imp1: haftmann@21249: assumes D: "!!x y z. x \ (y \ z) = (x \ y) \ (x \ z)" haftmann@21249: shows "x \ (y \ z) = (x \ y) \ (x \ z)" haftmann@21249: proof- haftmann@21249: have "x \ (y \ z) = (x \ (x \ z)) \ (y \ z)" by(simp add:sup_inf_absorb) krauss@34209: also have "\ = x \ (z \ (x \ y))" by(simp add:D inf_commute sup_assoc) haftmann@21249: also have "\ = ((x \ y) \ x) \ ((x \ y) \ z)" haftmann@21249: by(simp add:inf_sup_absorb inf_commute) haftmann@21249: also have "\ = (x \ y) \ (x \ z)" by(simp add:D) haftmann@21249: finally show ?thesis . haftmann@21249: qed haftmann@21249: nipkow@21733: lemma distrib_imp2: haftmann@21249: assumes D: "!!x y z. x \ (y \ z) = (x \ y) \ (x \ z)" haftmann@21249: shows "x \ (y \ z) = (x \ y) \ (x \ z)" haftmann@21249: proof- haftmann@21249: have "x \ (y \ z) = (x \ (x \ z)) \ (y \ z)" by(simp add:inf_sup_absorb) krauss@34209: also have "\ = x \ (z \ (x \ y))" by(simp add:D sup_commute inf_assoc) haftmann@21249: also have "\ = ((x \ y) \ x) \ ((x \ y) \ z)" haftmann@21249: by(simp add:sup_inf_absorb sup_commute) haftmann@21249: also have "\ = (x \ y) \ (x \ z)" by(simp add:D) haftmann@21249: finally show ?thesis . haftmann@21249: qed haftmann@21249: nipkow@21733: end haftmann@21249: haftmann@32568: subsubsection {* Strict order *} haftmann@32568: haftmann@35028: context semilattice_inf haftmann@32568: begin haftmann@32568: haftmann@32568: lemma less_infI1: haftmann@32568: "a \ x \ a \ b \ x" haftmann@32642: by (auto simp add: less_le inf_absorb1 intro: le_infI1) haftmann@32568: haftmann@32568: lemma less_infI2: haftmann@32568: "b \ x \ a \ b \ x" haftmann@32642: by (auto simp add: less_le inf_absorb2 intro: le_infI2) haftmann@32568: haftmann@32568: end haftmann@32568: haftmann@35028: context semilattice_sup haftmann@32568: begin haftmann@32568: haftmann@32568: lemma less_supI1: haftmann@34007: "x \ a \ x \ a \ b" haftmann@32568: proof - haftmann@35028: interpret dual: semilattice_inf "op \" "op >" sup haftmann@32568: by (fact dual_semilattice) haftmann@34007: assume "x \ a" haftmann@34007: then show "x \ a \ b" haftmann@32568: by (fact dual.less_infI1) haftmann@32568: qed haftmann@32568: haftmann@32568: lemma less_supI2: haftmann@34007: "x \ b \ x \ a \ b" haftmann@32568: proof - haftmann@35028: interpret dual: semilattice_inf "op \" "op >" sup haftmann@32568: by (fact dual_semilattice) haftmann@34007: assume "x \ b" haftmann@34007: then show "x \ a \ b" haftmann@32568: by (fact dual.less_infI2) haftmann@32568: qed haftmann@32568: haftmann@32568: end haftmann@32568: haftmann@21249: haftmann@24164: subsection {* Distributive lattices *} haftmann@21249: haftmann@22454: class distrib_lattice = lattice + haftmann@21249: assumes sup_inf_distrib1: "x \ (y \ z) = (x \ y) \ (x \ z)" haftmann@21249: nipkow@21733: context distrib_lattice nipkow@21733: begin nipkow@21733: nipkow@21733: lemma sup_inf_distrib2: haftmann@21249: "(y \ z) \ x = (y \ x) \ (z \ x)" haftmann@32064: by(simp add: inf_sup_aci sup_inf_distrib1) haftmann@21249: nipkow@21733: lemma inf_sup_distrib1: haftmann@21249: "x \ (y \ z) = (x \ y) \ (x \ z)" haftmann@21249: by(rule distrib_imp2[OF sup_inf_distrib1]) haftmann@21249: nipkow@21733: lemma inf_sup_distrib2: haftmann@21249: "(y \ z) \ x = (y \ x) \ (z \ x)" haftmann@32064: by(simp add: inf_sup_aci inf_sup_distrib1) haftmann@21249: haftmann@31991: lemma dual_distrib_lattice: haftmann@36635: "class.distrib_lattice (op \) (op >) sup inf" haftmann@36635: by (rule class.distrib_lattice.intro, rule dual_lattice) haftmann@31991: (unfold_locales, fact inf_sup_distrib1) haftmann@31991: huffman@36008: lemmas sup_inf_distrib = huffman@36008: sup_inf_distrib1 sup_inf_distrib2 huffman@36008: huffman@36008: lemmas inf_sup_distrib = huffman@36008: inf_sup_distrib1 inf_sup_distrib2 huffman@36008: nipkow@21733: lemmas distrib = haftmann@21249: sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2 haftmann@21249: nipkow@21733: end nipkow@21733: haftmann@21249: haftmann@34007: subsection {* Bounded lattices and boolean algebras *} haftmann@31991: kaliszyk@36352: class bounded_lattice_bot = lattice + bot haftmann@31991: begin haftmann@31991: haftmann@31991: lemma inf_bot_left [simp]: haftmann@34007: "\ \ x = \" haftmann@31991: by (rule inf_absorb1) simp haftmann@31991: haftmann@31991: lemma inf_bot_right [simp]: haftmann@34007: "x \ \ = \" haftmann@31991: by (rule inf_absorb2) simp haftmann@31991: kaliszyk@36352: lemma sup_bot_left [simp]: kaliszyk@36352: "\ \ x = x" kaliszyk@36352: by (rule sup_absorb2) simp kaliszyk@36352: kaliszyk@36352: lemma sup_bot_right [simp]: kaliszyk@36352: "x \ \ = x" kaliszyk@36352: by (rule sup_absorb1) simp kaliszyk@36352: kaliszyk@36352: lemma sup_eq_bot_iff [simp]: kaliszyk@36352: "x \ y = \ \ x = \ \ y = \" kaliszyk@36352: by (simp add: eq_iff) kaliszyk@36352: kaliszyk@36352: end kaliszyk@36352: kaliszyk@36352: class bounded_lattice_top = lattice + top kaliszyk@36352: begin kaliszyk@36352: haftmann@31991: lemma sup_top_left [simp]: haftmann@34007: "\ \ x = \" haftmann@31991: by (rule sup_absorb1) simp haftmann@31991: haftmann@31991: lemma sup_top_right [simp]: haftmann@34007: "x \ \ = \" haftmann@31991: by (rule sup_absorb2) simp haftmann@31991: haftmann@31991: lemma inf_top_left [simp]: haftmann@34007: "\ \ x = x" haftmann@31991: by (rule inf_absorb2) simp haftmann@31991: haftmann@31991: lemma inf_top_right [simp]: haftmann@34007: "x \ \ = x" haftmann@31991: by (rule inf_absorb1) simp haftmann@31991: huffman@36008: lemma inf_eq_top_iff [simp]: huffman@36008: "x \ y = \ \ x = \ \ y = \" huffman@36008: by (simp add: eq_iff) haftmann@32568: kaliszyk@36352: end kaliszyk@36352: kaliszyk@36352: class bounded_lattice = bounded_lattice_bot + bounded_lattice_top kaliszyk@36352: begin kaliszyk@36352: kaliszyk@36352: lemma dual_bounded_lattice: haftmann@36635: "class.bounded_lattice (op \) (op >) (op \) (op \) \ \" kaliszyk@36352: by unfold_locales (auto simp add: less_le_not_le) haftmann@32568: haftmann@34007: end haftmann@34007: haftmann@34007: class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus + haftmann@34007: assumes inf_compl_bot: "x \ - x = \" haftmann@34007: and sup_compl_top: "x \ - x = \" haftmann@34007: assumes diff_eq: "x - y = x \ - y" haftmann@34007: begin haftmann@34007: haftmann@34007: lemma dual_boolean_algebra: haftmann@36635: "class.boolean_algebra (\x y. x \ - y) uminus (op \) (op >) (op \) (op \) \ \" haftmann@36635: by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice) haftmann@34007: (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq) haftmann@34007: haftmann@34007: lemma compl_inf_bot: haftmann@34007: "- x \ x = \" haftmann@34007: by (simp add: inf_commute inf_compl_bot) haftmann@34007: haftmann@34007: lemma compl_sup_top: haftmann@34007: "- x \ x = \" haftmann@34007: by (simp add: sup_commute sup_compl_top) haftmann@34007: haftmann@31991: lemma compl_unique: haftmann@34007: assumes "x \ y = \" haftmann@34007: and "x \ y = \" haftmann@31991: shows "- x = y" haftmann@31991: proof - haftmann@31991: have "(x \ - x) \ (- x \ y) = (x \ y) \ (- x \ y)" haftmann@31991: using inf_compl_bot assms(1) by simp haftmann@31991: then have "(- x \ x) \ (- x \ y) = (y \ x) \ (y \ - x)" haftmann@31991: by (simp add: inf_commute) haftmann@31991: then have "- x \ (x \ y) = y \ (x \ - x)" haftmann@31991: by (simp add: inf_sup_distrib1) haftmann@34007: then have "- x \ \ = y \ \" haftmann@31991: using sup_compl_top assms(2) by simp krauss@34209: then show "- x = y" by simp haftmann@31991: qed haftmann@31991: haftmann@31991: lemma double_compl [simp]: haftmann@31991: "- (- x) = x" haftmann@31991: using compl_inf_bot compl_sup_top by (rule compl_unique) haftmann@31991: haftmann@31991: lemma compl_eq_compl_iff [simp]: haftmann@31991: "- x = - y \ x = y" haftmann@31991: proof haftmann@31991: assume "- x = - y" huffman@36008: then have "- (- x) = - (- y)" by (rule arg_cong) haftmann@31991: then show "x = y" by simp haftmann@31991: next haftmann@31991: assume "x = y" haftmann@31991: then show "- x = - y" by simp haftmann@31991: qed haftmann@31991: haftmann@31991: lemma compl_bot_eq [simp]: haftmann@34007: "- \ = \" haftmann@31991: proof - haftmann@34007: from sup_compl_top have "\ \ - \ = \" . haftmann@31991: then show ?thesis by simp haftmann@31991: qed haftmann@31991: haftmann@31991: lemma compl_top_eq [simp]: haftmann@34007: "- \ = \" haftmann@31991: proof - haftmann@34007: from inf_compl_bot have "\ \ - \ = \" . haftmann@31991: then show ?thesis by simp haftmann@31991: qed haftmann@31991: haftmann@31991: lemma compl_inf [simp]: haftmann@31991: "- (x \ y) = - x \ - y" haftmann@31991: proof (rule compl_unique) huffman@36008: have "(x \ y) \ (- x \ - y) = (y \ (x \ - x)) \ (x \ (y \ - y))" huffman@36008: by (simp only: inf_sup_distrib inf_aci) huffman@36008: then show "(x \ y) \ (- x \ - y) = \" haftmann@31991: by (simp add: inf_compl_bot) haftmann@31991: next huffman@36008: have "(x \ y) \ (- x \ - y) = (- y \ (x \ - x)) \ (- x \ (y \ - y))" huffman@36008: by (simp only: sup_inf_distrib sup_aci) huffman@36008: then show "(x \ y) \ (- x \ - y) = \" haftmann@31991: by (simp add: sup_compl_top) haftmann@31991: qed haftmann@31991: haftmann@31991: lemma compl_sup [simp]: haftmann@31991: "- (x \ y) = - x \ - y" haftmann@31991: proof - haftmann@34007: interpret boolean_algebra "\x y. x \ - y" uminus "op \" "op >" "op \" "op \" \ \ haftmann@31991: by (rule dual_boolean_algebra) haftmann@31991: then show ?thesis by simp haftmann@31991: qed haftmann@31991: huffman@36008: lemma compl_mono: huffman@36008: "x \ y \ - y \ - x" huffman@36008: proof - huffman@36008: assume "x \ y" huffman@36008: then have "x \ y = y" by (simp only: le_iff_sup) huffman@36008: then have "- (x \ y) = - y" by simp huffman@36008: then have "- x \ - y = - y" by simp huffman@36008: then have "- y \ - x = - y" by (simp only: inf_commute) huffman@36008: then show "- y \ - x" by (simp only: le_iff_inf) huffman@36008: qed huffman@36008: huffman@36008: lemma compl_le_compl_iff: (* TODO: declare [simp] ? *) huffman@36008: "- x \ - y \ y \ x" huffman@36008: by (auto dest: compl_mono) huffman@36008: haftmann@31991: end haftmann@31991: haftmann@31991: haftmann@22454: subsection {* Uniqueness of inf and sup *} haftmann@22454: haftmann@35028: lemma (in semilattice_inf) inf_unique: haftmann@22454: fixes f (infixl "\" 70) haftmann@34007: assumes le1: "\x y. x \ y \ x" and le2: "\x y. x \ y \ y" haftmann@34007: and greatest: "\x y z. x \ y \ x \ z \ x \ y \ z" haftmann@22737: shows "x \ y = x \ y" haftmann@22454: proof (rule antisym) haftmann@34007: show "x \ y \ x \ y" by (rule le_infI) (rule le1, rule le2) haftmann@22454: next haftmann@34007: have leI: "\x y z. x \ y \ x \ z \ x \ y \ z" by (blast intro: greatest) haftmann@34007: show "x \ y \ x \ y" by (rule leI) simp_all haftmann@22454: qed haftmann@22454: haftmann@35028: lemma (in semilattice_sup) sup_unique: haftmann@22454: fixes f (infixl "\" 70) haftmann@34007: assumes ge1 [simp]: "\x y. x \ x \ y" and ge2: "\x y. y \ x \ y" haftmann@34007: and least: "\x y z. y \ x \ z \ x \ y \ z \ x" haftmann@22737: shows "x \ y = x \ y" haftmann@22454: proof (rule antisym) haftmann@34007: show "x \ y \ x \ y" by (rule le_supI) (rule ge1, rule ge2) haftmann@22454: next haftmann@34007: have leI: "\x y z. x \ z \ y \ z \ x \ y \ z" by (blast intro: least) haftmann@34007: show "x \ y \ x \ y" by (rule leI) simp_all haftmann@22454: qed huffman@36008: haftmann@22454: haftmann@22916: subsection {* @{const min}/@{const max} on linear orders as haftmann@22916: special case of @{const inf}/@{const sup} *} haftmann@22916: haftmann@32512: sublocale linorder < min_max!: distrib_lattice less_eq less min max haftmann@28823: proof haftmann@22916: fix x y z haftmann@32512: show "max x (min y z) = min (max x y) (max x z)" haftmann@32512: by (auto simp add: min_def max_def) haftmann@22916: qed (auto simp add: min_def max_def not_le less_imp_le) haftmann@21249: haftmann@35028: lemma inf_min: "inf = (min \ 'a\{semilattice_inf, linorder} \ 'a \ 'a)" haftmann@25102: by (rule ext)+ (auto intro: antisym) nipkow@21733: haftmann@35028: lemma sup_max: "sup = (max \ 'a\{semilattice_sup, linorder} \ 'a \ 'a)" haftmann@25102: by (rule ext)+ (auto intro: antisym) nipkow@21733: haftmann@21249: lemmas le_maxI1 = min_max.sup_ge1 haftmann@21249: lemmas le_maxI2 = min_max.sup_ge2 haftmann@21381: haftmann@34973: lemmas min_ac = min_max.inf_assoc min_max.inf_commute haftmann@34973: min_max.inf.left_commute haftmann@21249: haftmann@34973: lemmas max_ac = min_max.sup_assoc min_max.sup_commute haftmann@34973: min_max.sup.left_commute haftmann@34973: haftmann@21249: haftmann@22454: subsection {* Bool as lattice *} haftmann@22454: haftmann@31991: instantiation bool :: boolean_algebra haftmann@25510: begin haftmann@25510: haftmann@25510: definition haftmann@31991: bool_Compl_def: "uminus = Not" haftmann@31991: haftmann@31991: definition haftmann@31991: bool_diff_def: "A - B \ A \ \ B" haftmann@31991: haftmann@31991: definition haftmann@25510: inf_bool_eq: "P \ Q \ P \ Q" haftmann@25510: haftmann@25510: definition haftmann@25510: sup_bool_eq: "P \ Q \ P \ Q" haftmann@25510: haftmann@31991: instance proof haftmann@31991: qed (simp_all add: inf_bool_eq sup_bool_eq le_bool_def haftmann@31991: bot_bool_eq top_bool_eq bool_Compl_def bool_diff_def, auto) haftmann@22454: haftmann@25510: end haftmann@25510: haftmann@32781: lemma sup_boolI1: haftmann@32781: "P \ P \ Q" haftmann@32781: by (simp add: sup_bool_eq) haftmann@32781: haftmann@32781: lemma sup_boolI2: haftmann@32781: "Q \ P \ Q" haftmann@32781: by (simp add: sup_bool_eq) haftmann@32781: haftmann@32781: lemma sup_boolE: haftmann@32781: "P \ Q \ (P \ R) \ (Q \ R) \ R" haftmann@32781: by (auto simp add: sup_bool_eq) haftmann@32781: haftmann@23878: haftmann@23878: subsection {* Fun as lattice *} haftmann@23878: haftmann@25510: instantiation "fun" :: (type, lattice) lattice haftmann@25510: begin haftmann@25510: haftmann@25510: definition haftmann@28562: inf_fun_eq [code del]: "f \ g = (\x. f x \ g x)" haftmann@25510: haftmann@25510: definition haftmann@28562: sup_fun_eq [code del]: "f \ g = (\x. f x \ g x)" haftmann@25510: haftmann@32780: instance proof haftmann@32780: qed (simp_all add: le_fun_def inf_fun_eq sup_fun_eq) haftmann@23878: haftmann@25510: end haftmann@23878: haftmann@23878: instance "fun" :: (type, distrib_lattice) distrib_lattice haftmann@31991: proof haftmann@32780: qed (simp_all add: inf_fun_eq sup_fun_eq sup_inf_distrib1) haftmann@31991: haftmann@34007: instance "fun" :: (type, bounded_lattice) bounded_lattice .. haftmann@34007: haftmann@31991: instantiation "fun" :: (type, uminus) uminus haftmann@31991: begin haftmann@31991: haftmann@31991: definition haftmann@31991: fun_Compl_def: "- A = (\x. - A x)" haftmann@31991: haftmann@31991: instance .. haftmann@31991: haftmann@31991: end haftmann@31991: haftmann@31991: instantiation "fun" :: (type, minus) minus haftmann@31991: begin haftmann@31991: haftmann@31991: definition haftmann@31991: fun_diff_def: "A - B = (\x. A x - B x)" haftmann@31991: haftmann@31991: instance .. haftmann@31991: haftmann@31991: end haftmann@31991: haftmann@31991: instance "fun" :: (type, boolean_algebra) boolean_algebra haftmann@31991: proof haftmann@31991: qed (simp_all add: inf_fun_eq sup_fun_eq bot_fun_eq top_fun_eq fun_Compl_def fun_diff_def haftmann@31991: inf_compl_bot sup_compl_top diff_eq) haftmann@23878: berghofe@26794: haftmann@25062: no_notation wenzelm@25382: less_eq (infix "\" 50) and wenzelm@25382: less (infix "\" 50) and wenzelm@25382: inf (infixl "\" 70) and haftmann@32568: sup (infixl "\" 65) and haftmann@32568: top ("\") and haftmann@32568: bot ("\") haftmann@25062: haftmann@21249: end