# Theory Lattices

Up to index of Isabelle/HOL-Proofs

theory Lattices
imports Groups
`(*  Title:      HOL/Lattices.thy    Author:     Tobias Nipkow*)header {* Abstract lattices *}theory Latticesimports Orderings Groupsbeginsubsection {* Abstract semilattice *}text {*  This locales provide a basic structure for interpretation into  bigger structures;  extensions require careful thinking, otherwise  undesired effects may occur due to interpretation.*}locale semilattice = abel_semigroup +  assumes idem [simp]: "f a a = a"beginlemma left_idem [simp]: "f a (f a b) = f a b"by (simp add: assoc [symmetric])lemma right_idem [simp]: "f (f a b) b = f a b"by (simp add: assoc)endsubsection {* Idempotent semigroup *}class ab_semigroup_idem_mult = ab_semigroup_mult +  assumes mult_idem: "x * x = x"sublocale ab_semigroup_idem_mult < times!: semilattice times proofqed (fact mult_idem)context ab_semigroup_idem_multbeginlemmas mult_left_idem = times.left_idemendsubsection {* Syntactic infimum and supremum operations *}class inf =  fixes inf :: "'a => 'a => 'a" (infixl "\<sqinter>" 70)class sup =   fixes sup :: "'a => 'a => 'a" (infixl "\<squnion>" 65)subsection {* Concrete lattices *}notation  less_eq  (infix "\<sqsubseteq>" 50) and  less  (infix "\<sqsubset>" 50)class semilattice_inf =  order + inf +  assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"  and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"  and inf_greatest: "x \<sqsubseteq> y ==> x \<sqsubseteq> z ==> x \<sqsubseteq> y \<sqinter> z"class semilattice_sup = order + sup +  assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"  and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"  and sup_least: "y \<sqsubseteq> x ==> z \<sqsubseteq> x ==> y \<squnion> z \<sqsubseteq> x"begintext {* Dual lattice *}lemma dual_semilattice:  "class.semilattice_inf sup greater_eq greater"by (rule class.semilattice_inf.intro, rule dual_order)  (unfold_locales, simp_all add: sup_least)endclass lattice = semilattice_inf + semilattice_supsubsubsection {* Intro and elim rules*}context semilattice_infbeginlemma le_infI1:  "a \<sqsubseteq> x ==> a \<sqinter> b \<sqsubseteq> x"  by (rule order_trans) autolemma le_infI2:  "b \<sqsubseteq> x ==> a \<sqinter> b \<sqsubseteq> x"  by (rule order_trans) autolemma le_infI: "x \<sqsubseteq> a ==> x \<sqsubseteq> b ==> x \<sqsubseteq> a \<sqinter> b"  by (rule inf_greatest) (* FIXME: duplicate lemma *)lemma le_infE: "x \<sqsubseteq> a \<sqinter> b ==> (x \<sqsubseteq> a ==> x \<sqsubseteq> b ==> P) ==> P"  by (blast intro: order_trans inf_le1 inf_le2)lemma le_inf_iff [simp]:  "x \<sqsubseteq> y \<sqinter> z <-> x \<sqsubseteq> y ∧ x \<sqsubseteq> z"  by (blast intro: le_infI elim: le_infE)lemma le_iff_inf:  "x \<sqsubseteq> y <-> x \<sqinter> y = x"  by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1])lemma inf_mono: "a \<sqsubseteq> c ==> b \<sqsubseteq> d ==> a \<sqinter> b \<sqsubseteq> c \<sqinter> d"  by (fast intro: inf_greatest le_infI1 le_infI2)lemma mono_inf:  fixes f :: "'a => 'b::semilattice_inf"  shows "mono f ==> f (A \<sqinter> B) \<sqsubseteq> f A \<sqinter> f B"  by (auto simp add: mono_def intro: Lattices.inf_greatest)endcontext semilattice_supbeginlemma le_supI1:  "x \<sqsubseteq> a ==> x \<sqsubseteq> a \<squnion> b"  by (rule order_trans) autolemma le_supI2:  "x \<sqsubseteq> b ==> x \<sqsubseteq> a \<squnion> b"  by (rule order_trans) auto lemma le_supI:  "a \<sqsubseteq> x ==> b \<sqsubseteq> x ==> a \<squnion> b \<sqsubseteq> x"  by (rule sup_least) (* FIXME: duplicate lemma *)lemma le_supE:  "a \<squnion> b \<sqsubseteq> x ==> (a \<sqsubseteq> x ==> b \<sqsubseteq> x ==> P) ==> P"  by (blast intro: order_trans sup_ge1 sup_ge2)lemma le_sup_iff [simp]:  "x \<squnion> y \<sqsubseteq> z <-> x \<sqsubseteq> z ∧ y \<sqsubseteq> z"  by (blast intro: le_supI elim: le_supE)lemma le_iff_sup:  "x \<sqsubseteq> y <-> x \<squnion> y = y"  by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1])lemma sup_mono: "a \<sqsubseteq> c ==> b \<sqsubseteq> d ==> a \<squnion> b \<sqsubseteq> c \<squnion> d"  by (fast intro: sup_least le_supI1 le_supI2)lemma mono_sup:  fixes f :: "'a => 'b::semilattice_sup"  shows "mono f ==> f A \<squnion> f B \<sqsubseteq> f (A \<squnion> B)"  by (auto simp add: mono_def intro: Lattices.sup_least)endsubsubsection {* Equational laws *}sublocale semilattice_inf < inf!: semilattice infproof  fix a b c  show "(a \<sqinter> b) \<sqinter> c = a \<sqinter> (b \<sqinter> c)"    by (rule antisym) (auto intro: le_infI1 le_infI2)  show "a \<sqinter> b = b \<sqinter> a"    by (rule antisym) auto  show "a \<sqinter> a = a"    by (rule antisym) autoqedcontext semilattice_infbeginlemma inf_assoc: "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"  by (fact inf.assoc)lemma inf_commute: "(x \<sqinter> y) = (y \<sqinter> x)"  by (fact inf.commute)lemma inf_left_commute: "x \<sqinter> (y \<sqinter> z) = y \<sqinter> (x \<sqinter> z)"  by (fact inf.left_commute)lemma inf_idem: "x \<sqinter> x = x"  by (fact inf.idem) (* already simp *)lemma inf_left_idem: "x \<sqinter> (x \<sqinter> y) = x \<sqinter> y"  by (fact inf.left_idem) (* already simp *)lemma inf_right_idem: "(x \<sqinter> y) \<sqinter> y = x \<sqinter> y"  by (fact inf.right_idem) (* already simp *)lemma inf_absorb1: "x \<sqsubseteq> y ==> x \<sqinter> y = x"  by (rule antisym) autolemma inf_absorb2: "y \<sqsubseteq> x ==> x \<sqinter> y = y"  by (rule antisym) auto lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idemendsublocale semilattice_sup < sup!: semilattice supproof  fix a b c  show "(a \<squnion> b) \<squnion> c = a \<squnion> (b \<squnion> c)"    by (rule antisym) (auto intro: le_supI1 le_supI2)  show "a \<squnion> b = b \<squnion> a"    by (rule antisym) auto  show "a \<squnion> a = a"    by (rule antisym) autoqedcontext semilattice_supbeginlemma sup_assoc: "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"  by (fact sup.assoc)lemma sup_commute: "(x \<squnion> y) = (y \<squnion> x)"  by (fact sup.commute)lemma sup_left_commute: "x \<squnion> (y \<squnion> z) = y \<squnion> (x \<squnion> z)"  by (fact sup.left_commute)lemma sup_idem: "x \<squnion> x = x"  by (fact sup.idem) (* already simp *)lemma sup_left_idem [simp]: "x \<squnion> (x \<squnion> y) = x \<squnion> y"  by (fact sup.left_idem)lemma sup_absorb1: "y \<sqsubseteq> x ==> x \<squnion> y = x"  by (rule antisym) autolemma sup_absorb2: "x \<sqsubseteq> y ==> x \<squnion> y = y"  by (rule antisym) autolemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idemendcontext latticebeginlemma dual_lattice:  "class.lattice sup (op ≥) (op >) inf"  by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)    (unfold_locales, auto)lemma inf_sup_absorb [simp]: "x \<sqinter> (x \<squnion> y) = x"  by (blast intro: antisym inf_le1 inf_greatest sup_ge1)lemma sup_inf_absorb [simp]: "x \<squnion> (x \<sqinter> y) = x"  by (blast intro: antisym sup_ge1 sup_least inf_le1)lemmas inf_sup_aci = inf_aci sup_acilemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2text{* Towards distributivity *}lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"  by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"  by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2)text{* If you have one of them, you have them all. *}lemma distrib_imp1:assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"shows "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"proof-  have "x \<squnion> (y \<sqinter> z) = (x \<squnion> (x \<sqinter> z)) \<squnion> (y \<sqinter> z)" by simp  also have "… = x \<squnion> (z \<sqinter> (x \<squnion> y))"    by (simp add: D inf_commute sup_assoc del: sup_inf_absorb)  also have "… = ((x \<squnion> y) \<sqinter> x) \<squnion> ((x \<squnion> y) \<sqinter> z)"    by(simp add: inf_commute)  also have "… = (x \<squnion> y) \<sqinter> (x \<squnion> z)" by(simp add:D)  finally show ?thesis .qedlemma distrib_imp2:assumes D: "!!x y z. x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"shows "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"proof-  have "x \<sqinter> (y \<squnion> z) = (x \<sqinter> (x \<squnion> z)) \<sqinter> (y \<squnion> z)" by simp  also have "… = x \<sqinter> (z \<squnion> (x \<sqinter> y))"    by (simp add: D sup_commute inf_assoc del: inf_sup_absorb)  also have "… = ((x \<sqinter> y) \<squnion> x) \<sqinter> ((x \<sqinter> y) \<squnion> z)"    by(simp add: sup_commute)  also have "… = (x \<sqinter> y) \<squnion> (x \<sqinter> z)" by(simp add:D)  finally show ?thesis .qedendsubsubsection {* Strict order *}context semilattice_infbeginlemma less_infI1:  "a \<sqsubset> x ==> a \<sqinter> b \<sqsubset> x"  by (auto simp add: less_le inf_absorb1 intro: le_infI1)lemma less_infI2:  "b \<sqsubset> x ==> a \<sqinter> b \<sqsubset> x"  by (auto simp add: less_le inf_absorb2 intro: le_infI2)endcontext semilattice_supbeginlemma less_supI1:  "x \<sqsubset> a ==> x \<sqsubset> a \<squnion> b"  using dual_semilattice  by (rule semilattice_inf.less_infI1)lemma less_supI2:  "x \<sqsubset> b ==> x \<sqsubset> a \<squnion> b"  using dual_semilattice  by (rule semilattice_inf.less_infI2)endsubsection {* Distributive lattices *}class distrib_lattice = lattice +  assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"context distrib_latticebeginlemma sup_inf_distrib2:  "(y \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"  by (simp add: sup_commute sup_inf_distrib1)lemma inf_sup_distrib1:  "x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"  by (rule distrib_imp2 [OF sup_inf_distrib1])lemma inf_sup_distrib2:  "(y \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (z \<sqinter> x)"  by (simp add: inf_commute inf_sup_distrib1)lemma dual_distrib_lattice:  "class.distrib_lattice sup (op ≥) (op >) inf"  by (rule class.distrib_lattice.intro, rule dual_lattice)    (unfold_locales, fact inf_sup_distrib1)lemmas sup_inf_distrib =  sup_inf_distrib1 sup_inf_distrib2lemmas inf_sup_distrib =  inf_sup_distrib1 inf_sup_distrib2lemmas distrib =  sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2endsubsection {* Bounded lattices and boolean algebras *}class bounded_lattice_bot = lattice + botbeginlemma inf_bot_left [simp]:  "⊥ \<sqinter> x = ⊥"  by (rule inf_absorb1) simplemma inf_bot_right [simp]:  "x \<sqinter> ⊥ = ⊥"  by (rule inf_absorb2) simplemma sup_bot_left [simp]:  "⊥ \<squnion> x = x"  by (rule sup_absorb2) simplemma sup_bot_right [simp]:  "x \<squnion> ⊥ = x"  by (rule sup_absorb1) simplemma sup_eq_bot_iff [simp]:  "x \<squnion> y = ⊥ <-> x = ⊥ ∧ y = ⊥"  by (simp add: eq_iff)endclass bounded_lattice_top = lattice + topbeginlemma sup_top_left [simp]:  "\<top> \<squnion> x = \<top>"  by (rule sup_absorb1) simplemma sup_top_right [simp]:  "x \<squnion> \<top> = \<top>"  by (rule sup_absorb2) simplemma inf_top_left [simp]:  "\<top> \<sqinter> x = x"  by (rule inf_absorb2) simplemma inf_top_right [simp]:  "x \<sqinter> \<top> = x"  by (rule inf_absorb1) simplemma inf_eq_top_iff [simp]:  "x \<sqinter> y = \<top> <-> x = \<top> ∧ y = \<top>"  by (simp add: eq_iff)endclass bounded_lattice = bounded_lattice_bot + bounded_lattice_topbeginlemma dual_bounded_lattice:  "class.bounded_lattice sup greater_eq greater inf \<top> ⊥"  by unfold_locales (auto simp add: less_le_not_le)endclass boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus +  assumes inf_compl_bot: "x \<sqinter> - x = ⊥"    and sup_compl_top: "x \<squnion> - x = \<top>"  assumes diff_eq: "x - y = x \<sqinter> - y"beginlemma dual_boolean_algebra:  "class.boolean_algebra (λx y. x \<squnion> - y) uminus sup greater_eq greater inf \<top> ⊥"  by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)    (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)lemma compl_inf_bot [simp]:  "- x \<sqinter> x = ⊥"  by (simp add: inf_commute inf_compl_bot)lemma compl_sup_top [simp]:  "- x \<squnion> x = \<top>"  by (simp add: sup_commute sup_compl_top)lemma compl_unique:  assumes "x \<sqinter> y = ⊥"    and "x \<squnion> y = \<top>"  shows "- x = y"proof -  have "(x \<sqinter> - x) \<squnion> (- x \<sqinter> y) = (x \<sqinter> y) \<squnion> (- x \<sqinter> y)"    using inf_compl_bot assms(1) by simp  then have "(- x \<sqinter> x) \<squnion> (- x \<sqinter> y) = (y \<sqinter> x) \<squnion> (y \<sqinter> - x)"    by (simp add: inf_commute)  then have "- x \<sqinter> (x \<squnion> y) = y \<sqinter> (x \<squnion> - x)"    by (simp add: inf_sup_distrib1)  then have "- x \<sqinter> \<top> = y \<sqinter> \<top>"    using sup_compl_top assms(2) by simp  then show "- x = y" by simpqedlemma double_compl [simp]:  "- (- x) = x"  using compl_inf_bot compl_sup_top by (rule compl_unique)lemma compl_eq_compl_iff [simp]:  "- x = - y <-> x = y"proof  assume "- x = - y"  then have "- (- x) = - (- y)" by (rule arg_cong)  then show "x = y" by simpnext  assume "x = y"  then show "- x = - y" by simpqedlemma compl_bot_eq [simp]:  "- ⊥ = \<top>"proof -  from sup_compl_top have "⊥ \<squnion> - ⊥ = \<top>" .  then show ?thesis by simpqedlemma compl_top_eq [simp]:  "- \<top> = ⊥"proof -  from inf_compl_bot have "\<top> \<sqinter> - \<top> = ⊥" .  then show ?thesis by simpqedlemma compl_inf [simp]:  "- (x \<sqinter> y) = - x \<squnion> - y"proof (rule compl_unique)  have "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = (y \<sqinter> (x \<sqinter> - x)) \<squnion> (x \<sqinter> (y \<sqinter> - y))"    by (simp only: inf_sup_distrib inf_aci)  then show "(x \<sqinter> y) \<sqinter> (- x \<squnion> - y) = ⊥"    by (simp add: inf_compl_bot)next  have "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = (- y \<squnion> (x \<squnion> - x)) \<sqinter> (- x \<squnion> (y \<squnion> - y))"    by (simp only: sup_inf_distrib sup_aci)  then show "(x \<sqinter> y) \<squnion> (- x \<squnion> - y) = \<top>"    by (simp add: sup_compl_top)qedlemma compl_sup [simp]:  "- (x \<squnion> y) = - x \<sqinter> - y"  using dual_boolean_algebra  by (rule boolean_algebra.compl_inf)lemma compl_mono:  "x \<sqsubseteq> y ==> - y \<sqsubseteq> - x"proof -  assume "x \<sqsubseteq> y"  then have "x \<squnion> y = y" by (simp only: le_iff_sup)  then have "- (x \<squnion> y) = - y" by simp  then have "- x \<sqinter> - y = - y" by simp  then have "- y \<sqinter> - x = - y" by (simp only: inf_commute)  then show "- y \<sqsubseteq> - x" by (simp only: le_iff_inf)qedlemma compl_le_compl_iff [simp]:  "- x \<sqsubseteq> - y <-> y \<sqsubseteq> x"  by (auto dest: compl_mono)lemma compl_le_swap1:  assumes "y \<sqsubseteq> - x" shows "x \<sqsubseteq> -y"proof -  from assms have "- (- x) \<sqsubseteq> - y" by (simp only: compl_le_compl_iff)  then show ?thesis by simpqedlemma compl_le_swap2:  assumes "- y \<sqsubseteq> x" shows "- x \<sqsubseteq> y"proof -  from assms have "- x \<sqsubseteq> - (- y)" by (simp only: compl_le_compl_iff)  then show ?thesis by simpqedlemma compl_less_compl_iff: (* TODO: declare [simp] ? *)  "- x \<sqsubset> - y <-> y \<sqsubset> x"  by (auto simp add: less_le)lemma compl_less_swap1:  assumes "y \<sqsubset> - x" shows "x \<sqsubset> - y"proof -  from assms have "- (- x) \<sqsubset> - y" by (simp only: compl_less_compl_iff)  then show ?thesis by simpqedlemma compl_less_swap2:  assumes "- y \<sqsubset> x" shows "- x \<sqsubset> y"proof -  from assms have "- x \<sqsubset> - (- y)" by (simp only: compl_less_compl_iff)  then show ?thesis by simpqedendsubsection {* Uniqueness of inf and sup *}lemma (in semilattice_inf) inf_unique:  fixes f (infixl "\<triangle>" 70)  assumes le1: "!!x y. x \<triangle> y \<sqsubseteq> x" and le2: "!!x y. x \<triangle> y \<sqsubseteq> y"  and greatest: "!!x y z. x \<sqsubseteq> y ==> x \<sqsubseteq> z ==> x \<sqsubseteq> y \<triangle> z"  shows "x \<sqinter> y = x \<triangle> y"proof (rule antisym)  show "x \<triangle> y \<sqsubseteq> x \<sqinter> y" by (rule le_infI) (rule le1, rule le2)next  have leI: "!!x y z. x \<sqsubseteq> y ==> x \<sqsubseteq> z ==> x \<sqsubseteq> y \<triangle> z" by (blast intro: greatest)  show "x \<sqinter> y \<sqsubseteq> x \<triangle> y" by (rule leI) simp_allqedlemma (in semilattice_sup) sup_unique:  fixes f (infixl "∇" 70)  assumes ge1 [simp]: "!!x y. x \<sqsubseteq> x ∇ y" and ge2: "!!x y. y \<sqsubseteq> x ∇ y"  and least: "!!x y z. y \<sqsubseteq> x ==> z \<sqsubseteq> x ==> y ∇ z \<sqsubseteq> x"  shows "x \<squnion> y = x ∇ y"proof (rule antisym)  show "x \<squnion> y \<sqsubseteq> x ∇ y" by (rule le_supI) (rule ge1, rule ge2)next  have leI: "!!x y z. x \<sqsubseteq> z ==> y \<sqsubseteq> z ==> x ∇ y \<sqsubseteq> z" by (blast intro: least)  show "x ∇ y \<sqsubseteq> x \<squnion> y" by (rule leI) simp_allqedsubsection {* @{const min}/@{const max} on linear orders as  special case of @{const inf}/@{const sup} *}sublocale linorder < min_max!: distrib_lattice min less_eq less maxproof  fix x y z  show "max x (min y z) = min (max x y) (max x z)"    by (auto simp add: min_def max_def)qed (auto simp add: min_def max_def not_le less_imp_le)lemma inf_min: "inf = (min :: 'a::{semilattice_inf, linorder} => 'a => 'a)"  by (rule ext)+ (auto intro: antisym)lemma sup_max: "sup = (max :: 'a::{semilattice_sup, linorder} => 'a => 'a)"  by (rule ext)+ (auto intro: antisym)lemmas le_maxI1 = min_max.sup_ge1lemmas le_maxI2 = min_max.sup_ge2 lemmas min_ac = min_max.inf_assoc min_max.inf_commute  min_max.inf.left_commutelemmas max_ac = min_max.sup_assoc min_max.sup_commute  min_max.sup.left_commutesubsection {* Lattice on @{typ bool} *}instantiation bool :: boolean_algebrabegindefinition  bool_Compl_def [simp]: "uminus = Not"definition  bool_diff_def [simp]: "A - B <-> A ∧ ¬ B"definition  [simp]: "P \<sqinter> Q <-> P ∧ Q"definition  [simp]: "P \<squnion> Q <-> P ∨ Q"instance proofqed autoendlemma sup_boolI1:  "P ==> P \<squnion> Q"  by simplemma sup_boolI2:  "Q ==> P \<squnion> Q"  by simplemma sup_boolE:  "P \<squnion> Q ==> (P ==> R) ==> (Q ==> R) ==> R"  by autosubsection {* Lattice on @{typ "_ => _"} *}instantiation "fun" :: (type, lattice) latticebegindefinition  "f \<sqinter> g = (λx. f x \<sqinter> g x)"lemma inf_apply [simp, code]:  "(f \<sqinter> g) x = f x \<sqinter> g x"  by (simp add: inf_fun_def)definition  "f \<squnion> g = (λx. f x \<squnion> g x)"lemma sup_apply [simp, code]:  "(f \<squnion> g) x = f x \<squnion> g x"  by (simp add: sup_fun_def)instance proofqed (simp_all add: le_fun_def)endinstance "fun" :: (type, distrib_lattice) distrib_lattice proofqed (rule ext, simp add: sup_inf_distrib1)instance "fun" :: (type, bounded_lattice) bounded_lattice ..instantiation "fun" :: (type, uminus) uminusbegindefinition  fun_Compl_def: "- A = (λx. - A x)"lemma uminus_apply [simp, code]:  "(- A) x = - (A x)"  by (simp add: fun_Compl_def)instance ..endinstantiation "fun" :: (type, minus) minusbegindefinition  fun_diff_def: "A - B = (λx. A x - B x)"lemma minus_apply [simp, code]:  "(A - B) x = A x - B x"  by (simp add: fun_diff_def)instance ..endinstance "fun" :: (type, boolean_algebra) boolean_algebra proofqed (rule ext, simp_all add: inf_compl_bot sup_compl_top diff_eq)+subsection {* Lattice on unary and binary predicates *}lemma inf1I: "A x ==> B x ==> (A \<sqinter> B) x"  by (simp add: inf_fun_def)lemma inf2I: "A x y ==> B x y ==> (A \<sqinter> B) x y"  by (simp add: inf_fun_def)lemma inf1E: "(A \<sqinter> B) x ==> (A x ==> B x ==> P) ==> P"  by (simp add: inf_fun_def)lemma inf2E: "(A \<sqinter> B) x y ==> (A x y ==> B x y ==> P) ==> P"  by (simp add: inf_fun_def)lemma inf1D1: "(A \<sqinter> B) x ==> A x"  by (simp add: inf_fun_def)lemma inf2D1: "(A \<sqinter> B) x y ==> A x y"  by (simp add: inf_fun_def)lemma inf1D2: "(A \<sqinter> B) x ==> B x"  by (simp add: inf_fun_def)lemma inf2D2: "(A \<sqinter> B) x y ==> B x y"  by (simp add: inf_fun_def)lemma sup1I1: "A x ==> (A \<squnion> B) x"  by (simp add: sup_fun_def)lemma sup2I1: "A x y ==> (A \<squnion> B) x y"  by (simp add: sup_fun_def)lemma sup1I2: "B x ==> (A \<squnion> B) x"  by (simp add: sup_fun_def)lemma sup2I2: "B x y ==> (A \<squnion> B) x y"  by (simp add: sup_fun_def)lemma sup1E: "(A \<squnion> B) x ==> (A x ==> P) ==> (B x ==> P) ==> P"  by (simp add: sup_fun_def) iproverlemma sup2E: "(A \<squnion> B) x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P"  by (simp add: sup_fun_def) iprovertext {*  \medskip Classical introduction rule: no commitment to @{text A} vs  @{text B}.*}lemma sup1CI: "(¬ B x ==> A x) ==> (A \<squnion> B) x"  by (auto simp add: sup_fun_def)lemma sup2CI: "(¬ B x y ==> A x y) ==> (A \<squnion> B) x y"  by (auto simp add: sup_fun_def)no_notation  less_eq (infix "\<sqsubseteq>" 50) and  less (infix "\<sqsubset>" 50)end`