# Lattice Proofs

A key part of mathematics is proofs, on this site I would like to include proofs in a consistant way across all the topics, I am therefore using a program called Isabelle which is a proof assistant. More about this program on this page.

This is taken from Isabelle code (from this site) but I have not put the complete code here, just an outline.

In mathematics, a join-semilattice (or upper semilattice) is a partially ordered set that has a join (a least upper bound) for any nonempty finite subset. Dually, a meet-semilattice (or lower semilattice) is a partially ordered set which has a meet (or greatest lower bound) for any nonempty finite subset. Every join-semilattice is a meet-semilattice in the inverse order and vice versa.

Semilattices can also be defined algebraically: join and meet are associative, commutative, idempotent binary operations, and any such operation induces a partial order (and the respective inverse order) such that the result of the operation for any two elements is the least upper bound (or greatest lower bound) of the elements with respect to this partial order.

A lattice is a partially ordered set that is both a meet- and join-semilattice with respect to the same partial order. Algebraically, a lattice is a set with two associative, commutative idempotent binary operations linked by corresponding absorption laws.

### Abstract Semilattice

A lattice has both a join and a meet operation but a semilattice has only one of these operatiors.

Join and meet are associative, commutative, idempotent binary operations.

Idempotent means:

• a /\ a = a
• a \/ a = a

From which we can derive:

• a /\ (a /\ b) = a /\ b
• a \/ (a \/ b) = a \/ b

There is also a right-hand version of these.

Absorptive means:

• a \/ (a /\ b) = a /\ (a \/ b) = a

This is represented in Isabelle code (from this site) by starting with an abelian group, which gives associative and commutitive binary operation (as discussed on this page) and adds the idempotent axiom like this:

 So the 'f' can represent either '/\' or '\/' depending on wheter it is an infimum (meet) or supremum (join) semilattice. A lattice is then built from one of each. ```locale semilattice = abel_semigroup + assumes idem [simp]: "f a a = a" begin lemma 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) end```

### Idempotent semigroup

 ```class ab_semigroup_idem_mult = ab_semigroup_mult + assumes mult_idem: "x * x = x"```

### Semilattice

 ```class inf = fixes inf :: "'a => 'a => 'a" (infixl "\" 70) class sup = fixes sup :: "'a => 'a => 'a" (infixl "\" 65) subsection {* Concrete lattices *} notation less_eq (infix "\" 50) and less (infix "\" 50) class semilattice_inf = order + inf + assumes inf_le1 [simp]: "x \ y \ x" and inf_le2 [simp]: "x \ y \ y" and inf_greatest: "x \ y ==> x \ z ==> x \ y \ z" class semilattice_sup = order + sup + assumes sup_ge1 [simp]: "x \ x \ y" and sup_ge2 [simp]: "y \ x \ y" and sup_least: "y \ x ==> z \ x ==> y \ z \ x" begin```

### Lattice

 `class lattice = semilattice_inf + semilattice_sup`

### Dual lattice

 ```text {* 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) end```

### Introduction and Elimination Rules

infimum also known as meet (a /\ b) or greatest lower bound.

 ```context semilattice_inf begin lemma le_infI1: "a \ x ==> a \ b \ x" by (rule order_trans) auto lemma le_infI2: "b \ x ==> a \ b \ x" by (rule order_trans) auto lemma le_infI: "x \ a ==> x \ b ==> x \ a \ b" by (rule inf_greatest) (* FIXME: duplicate lemma *) lemma le_infE: "x \ a \ b ==> (x \ a ==> x \ b ==> P) ==> P" by (blast intro: order_trans inf_le1 inf_le2) lemma le_inf_iff [simp]: "x \ y \ z <-> x \ y ∧ x \ z" by (blast intro: le_infI elim: le_infE) lemma le_iff_inf: "x \ y <-> x \ y = x" by (auto intro: le_infI1 antisym dest: eq_iff [THEN iffD1]) lemma inf_mono: "a \ c ==> b \ d ==> a \ b \ c \ d" by (fast intro: inf_greatest le_infI1 le_infI2) lemma mono_inf: fixes f :: "'a => 'b::semilattice_inf" shows "mono f ==> f (A \ B) \ f A \ f B" by (auto simp add: mono_def intro: Lattices.inf_greatest) end```

supremum also known as the join (a \/ b) or least upper bound.

 ```context semilattice_sup begin lemma le_supI1: "x \ a ==> x \ a \ b" by (rule order_trans) auto lemma le_supI2: "x \ b ==> x \ a \ b" by (rule order_trans) auto lemma le_supI: "a \ x ==> b \ x ==> a \ b \ x" by (rule sup_least) (* FIXME: duplicate lemma *) lemma le_supE: "a \ b \ x ==> (a \ x ==> b \ x ==> P) ==> P" by (blast intro: order_trans sup_ge1 sup_ge2) lemma le_sup_iff [simp]: "x \ y \ z <-> x \ z ∧ y \ z" by (blast intro: le_supI elim: le_supE) lemma le_iff_sup: "x \ y <-> x \ y = y" by (auto intro: le_supI2 antisym dest: eq_iff [THEN iffD1]) lemma sup_mono: "a \ c ==> b \ d ==> a \ b \ c \ d" by (fast intro: sup_least le_supI1 le_supI2) lemma mono_sup: fixes f :: "'a => 'b::semilattice_sup" shows "mono f ==> f A \ f B \ f (A \ B)" by (auto simp add: mono_def intro: Lattices.sup_least) end```

### Equational laws

 ``` subsubsection {* Equational laws *} sublocale semilattice_inf < inf!: semilattice inf proof fix a b c show "(a \ b) \ c = a \ (b \ c)" by (rule antisym) (auto intro: le_infI1 le_infI2) show "a \ b = b \ a" by (rule antisym) auto show "a \ a = a" by (rule antisym) auto qed context semilattice_inf begin lemma inf_assoc: "(x \ y) \ z = x \ (y \ z)" by (fact inf.assoc) lemma inf_commute: "(x \ y) = (y \ x)" by (fact inf.commute) lemma inf_left_commute: "x \ (y \ z) = y \ (x \ z)" by (fact inf.left_commute) lemma inf_idem: "x \ x = x" by (fact inf.idem) (* already simp *) lemma inf_left_idem: "x \ (x \ y) = x \ y" by (fact inf.left_idem) (* already simp *) lemma inf_right_idem: "(x \ y) \ y = x \ y" by (fact inf.right_idem) (* already simp *) lemma inf_absorb1: "x \ y ==> x \ y = x" by (rule antisym) auto lemma inf_absorb2: "y \ x ==> x \ y = y" by (rule antisym) auto lemmas inf_aci = inf_commute inf_assoc inf_left_commute inf_left_idem end sublocale semilattice_sup < sup!: semilattice sup proof fix a b c show "(a \ b) \ c = a \ (b \ c)" by (rule antisym) (auto intro: le_supI1 le_supI2) show "a \ b = b \ a" by (rule antisym) auto show "a \ a = a" by (rule antisym) auto qed context semilattice_sup begin lemma sup_assoc: "(x \ y) \ z = x \ (y \ z)" by (fact sup.assoc) lemma sup_commute: "(x \ y) = (y \ x)" by (fact sup.commute) lemma sup_left_commute: "x \ (y \ z) = y \ (x \ z)" by (fact sup.left_commute) lemma sup_idem: "x \ x = x" by (fact sup.idem) (* already simp *) lemma sup_left_idem [simp]: "x \ (x \ y) = x \ y" by (fact sup.left_idem) lemma sup_absorb1: "y \ x ==> x \ y = x" by (rule antisym) auto lemma sup_absorb2: "x \ y ==> x \ y = y" by (rule antisym) auto lemmas sup_aci = sup_commute sup_assoc sup_left_commute sup_left_idem end context lattice begin lemma 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 \ (x \ y) = x" by (blast intro: antisym inf_le1 inf_greatest sup_ge1) lemma sup_inf_absorb [simp]: "x \ (x \ y) = x" by (blast intro: antisym sup_ge1 sup_least inf_le1) lemmas inf_sup_aci = inf_aci sup_aci lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2 text{* Towards distributivity *} lemma distrib_sup_le: "x \ (y \ z) \ (x \ y) \ (x \ z)" by (auto intro: le_infI1 le_infI2 le_supI1 le_supI2) lemma distrib_inf_le: "(x \ y) \ (x \ z) \ x \ (y \ 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 \ (y \ z) = (x \ y) \ (x \ z)" shows "x \ (y \ z) = (x \ y) \ (x \ z)" proof- have "x \ (y \ z) = (x \ (x \ z)) \ (y \ z)" by simp also have "… = x \ (z \ (x \ y))" by (simp add: D inf_commute sup_assoc del: sup_inf_absorb) also have "… = ((x \ y) \ x) \ ((x \ y) \ z)" by(simp add: inf_commute) also have "… = (x \ y) \ (x \ z)" by(simp add:D) finally show ?thesis . qed lemma distrib_imp2: assumes D: "!!x y z. x \ (y \ z) = (x \ y) \ (x \ z)" shows "x \ (y \ z) = (x \ y) \ (x \ z)" proof- have "x \ (y \ z) = (x \ (x \ z)) \ (y \ z)" by simp also have "… = x \ (z \ (x \ y))" by (simp add: D sup_commute inf_assoc del: inf_sup_absorb) also have "… = ((x \ y) \ x) \ ((x \ y) \ z)" by(simp add: sup_commute) also have "… = (x \ y) \ (x \ z)" by(simp add:D) finally show ?thesis . qed end subsubsection {* Strict order *} context semilattice_inf begin lemma less_infI1: "a \ x ==> a \ b \ x" by (auto simp add: less_le inf_absorb1 intro: le_infI1) lemma less_infI2: "b \ x ==> a \ b \ x" by (auto simp add: less_le inf_absorb2 intro: le_infI2) end context semilattice_sup begin lemma less_supI1: "x \ a ==> x \ a \ b" using dual_semilattice by (rule semilattice_inf.less_infI1) lemma less_supI2: "x \ b ==> x \ a \ b" using dual_semilattice by (rule semilattice_inf.less_infI2) end subsection {* Distributive lattices *} class distrib_lattice = lattice + assumes sup_inf_distrib1: "x \ (y \ z) = (x \ y) \ (x \ z)" context distrib_lattice begin lemma sup_inf_distrib2: "(y \ z) \ x = (y \ x) \ (z \ x)" by (simp add: sup_commute sup_inf_distrib1) lemma inf_sup_distrib1: "x \ (y \ z) = (x \ y) \ (x \ z)" by (rule distrib_imp2 [OF sup_inf_distrib1]) lemma inf_sup_distrib2: "(y \ z) \ x = (y \ x) \ (z \ 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_distrib2 lemmas inf_sup_distrib = inf_sup_distrib1 inf_sup_distrib2 lemmas distrib = sup_inf_distrib1 sup_inf_distrib2 inf_sup_distrib1 inf_sup_distrib2 end subsection {* Bounded lattices and boolean algebras *} class bounded_lattice_bot = lattice + bot begin lemma inf_bot_left [simp]: "⊥ \ x = ⊥" by (rule inf_absorb1) simp lemma inf_bot_right [simp]: "x \ ⊥ = ⊥" by (rule inf_absorb2) simp lemma sup_bot_left [simp]: "⊥ \ x = x" by (rule sup_absorb2) simp lemma sup_bot_right [simp]: "x \ ⊥ = x" by (rule sup_absorb1) simp lemma sup_eq_bot_iff [simp]: "x \ y = ⊥ <-> x = ⊥ ∧ y = ⊥" by (simp add: eq_iff) end class bounded_lattice_top = lattice + top begin lemma sup_top_left [simp]: "\ \ x = \" by (rule sup_absorb1) simp lemma sup_top_right [simp]: "x \ \ = \" by (rule sup_absorb2) simp lemma inf_top_left [simp]: "\ \ x = x" by (rule inf_absorb2) simp lemma inf_top_right [simp]: "x \ \ = x" by (rule inf_absorb1) simp lemma inf_eq_top_iff [simp]: "x \ y = \ <-> x = \ ∧ y = \" by (simp add: eq_iff) end class bounded_lattice = bounded_lattice_bot + bounded_lattice_top begin lemma dual_bounded_lattice: "class.bounded_lattice sup greater_eq greater inf \ ⊥" by unfold_locales (auto simp add: less_le_not_le) end class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus + assumes inf_compl_bot: "x \ - x = ⊥" and sup_compl_top: "x \ - x = \" assumes diff_eq: "x - y = x \ - y" begin lemma dual_boolean_algebra: "class.boolean_algebra (λx y. x \ - y) uminus sup greater_eq greater inf \ ⊥" 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 \ x = ⊥" by (simp add: inf_commute inf_compl_bot) lemma compl_sup_top [simp]: "- x \ x = \" by (simp add: sup_commute sup_compl_top) lemma compl_unique: assumes "x \ y = ⊥" and "x \ y = \" shows "- x = y" proof - have "(x \ - x) \ (- x \ y) = (x \ y) \ (- x \ y)" using inf_compl_bot assms(1) by simp then have "(- x \ x) \ (- x \ y) = (y \ x) \ (y \ - x)" by (simp add: inf_commute) then have "- x \ (x \ y) = y \ (x \ - x)" by (simp add: inf_sup_distrib1) then have "- x \ \ = y \ \" using sup_compl_top assms(2) by simp then show "- x = y" by simp qed lemma 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 simp next assume "x = y" then show "- x = - y" by simp qed lemma compl_bot_eq [simp]: "- ⊥ = \" proof - from sup_compl_top have "⊥ \ - ⊥ = \" . then show ?thesis by simp qed lemma compl_top_eq [simp]: "- \ = ⊥" proof - from inf_compl_bot have "\ \ - \ = ⊥" . then show ?thesis by simp qed lemma compl_inf [simp]: "- (x \ y) = - x \ - y" proof (rule compl_unique) have "(x \ y) \ (- x \ - y) = (y \ (x \ - x)) \ (x \ (y \ - y))" by (simp only: inf_sup_distrib inf_aci) then show "(x \ y) \ (- x \ - y) = ⊥" by (simp add: inf_compl_bot) next have "(x \ y) \ (- x \ - y) = (- y \ (x \ - x)) \ (- x \ (y \ - y))" by (simp only: sup_inf_distrib sup_aci) then show "(x \ y) \ (- x \ - y) = \" by (simp add: sup_compl_top) qed lemma compl_sup [simp]: "- (x \ y) = - x \ - y" using dual_boolean_algebra by (rule boolean_algebra.compl_inf) lemma compl_mono: "x \ y ==> - y \ - x" proof - assume "x \ y" then have "x \ y = y" by (simp only: le_iff_sup) then have "- (x \ y) = - y" by simp then have "- x \ - y = - y" by simp then have "- y \ - x = - y" by (simp only: inf_commute) then show "- y \ - x" by (simp only: le_iff_inf) qed lemma compl_le_compl_iff [simp]: "- x \ - y <-> y \ x" by (auto dest: compl_mono) lemma compl_le_swap1: assumes "y \ - x" shows "x \ -y" proof - from assms have "- (- x) \ - y" by (simp only: compl_le_compl_iff) then show ?thesis by simp qed lemma compl_le_swap2: assumes "- y \ x" shows "- x \ y" proof - from assms have "- x \ - (- y)" by (simp only: compl_le_compl_iff) then show ?thesis by simp qed lemma compl_less_compl_iff: (* TODO: declare [simp] ? *) "- x \ - y <-> y \ x" by (auto simp add: less_le) lemma compl_less_swap1: assumes "y \ - x" shows "x \ - y" proof - from assms have "- (- x) \ - y" by (simp only: compl_less_compl_iff) then show ?thesis by simp qed lemma compl_less_swap2: assumes "- y \ x" shows "- x \ y" proof - from assms have "- x \ - (- y)" by (simp only: compl_less_compl_iff) then show ?thesis by simp qed end subsection {* Uniqueness of inf and sup *} lemma (in semilattice_inf) inf_unique: fixes f (infixl "\" 70) assumes le1: "!!x y. x \ y \ x" and le2: "!!x y. x \ y \ y" and greatest: "!!x y z. x \ y ==> x \ z ==> x \ y \ z" shows "x \ y = x \ y" proof (rule antisym) show "x \ y \ x \ y" by (rule le_infI) (rule le1, rule le2) next have leI: "!!x y z. x \ y ==> x \ z ==> x \ y \ z" by (blast intro: greatest) show "x \ y \ x \ y" by (rule leI) simp_all qed lemma (in semilattice_sup) sup_unique: fixes f (infixl "∇" 70) assumes ge1 [simp]: "!!x y. x \ x ∇ y" and ge2: "!!x y. y \ x ∇ y" and least: "!!x y z. y \ x ==> z \ x ==> y ∇ z \ x" shows "x \ y = x ∇ y" proof (rule antisym) show "x \ y \ x ∇ y" by (rule le_supI) (rule ge1, rule ge2) next have leI: "!!x y z. x \ z ==> y \ z ==> x ∇ y \ z" by (blast intro: least) show "x ∇ y \ x \ y" by (rule leI) simp_all qed subsection {* @{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 max proof 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_ge1 lemmas le_maxI2 = min_max.sup_ge2 lemmas min_ac = min_max.inf_assoc min_max.inf_commute min_max.inf.left_commute lemmas max_ac = min_max.sup_assoc min_max.sup_commute min_max.sup.left_commute subsection {* Lattice on @{typ bool} *} instantiation bool :: boolean_algebra begin definition bool_Compl_def [simp]: "uminus = Not" definition bool_diff_def [simp]: "A - B <-> A ∧ ¬ B" definition [simp]: "P \ Q <-> P ∧ Q" definition [simp]: "P \ Q <-> P ∨ Q" instance proof qed auto end lemma sup_boolI1: "P ==> P \ Q" by simp lemma sup_boolI2: "Q ==> P \ Q" by simp lemma sup_boolE: "P \ Q ==> (P ==> R) ==> (Q ==> R) ==> R" by auto subsection {* Lattice on @{typ "_ => _"} *} instantiation "fun" :: (type, lattice) lattice begin definition "f \ g = (λx. f x \ g x)" lemma inf_apply [simp, code]: "(f \ g) x = f x \ g x" by (simp add: inf_fun_def) definition "f \ g = (λx. f x \ g x)" lemma sup_apply [simp, code]: "(f \ g) x = f x \ g x" by (simp add: sup_fun_def) instance proof qed (simp_all add: le_fun_def) end instance "fun" :: (type, distrib_lattice) distrib_lattice proof qed (rule ext, simp add: sup_inf_distrib1) instance "fun" :: (type, bounded_lattice) bounded_lattice .. instantiation "fun" :: (type, uminus) uminus begin definition fun_Compl_def: "- A = (λx. - A x)" lemma uminus_apply [simp, code]: "(- A) x = - (A x)" by (simp add: fun_Compl_def) instance .. end instantiation "fun" :: (type, minus) minus begin definition 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 .. end instance "fun" :: (type, boolean_algebra) boolean_algebra proof qed (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 \ B) x" by (simp add: inf_fun_def) lemma inf2I: "A x y ==> B x y ==> (A \ B) x y" by (simp add: inf_fun_def) lemma inf1E: "(A \ B) x ==> (A x ==> B x ==> P) ==> P" by (simp add: inf_fun_def) lemma inf2E: "(A \ B) x y ==> (A x y ==> B x y ==> P) ==> P" by (simp add: inf_fun_def) lemma inf1D1: "(A \ B) x ==> A x" by (simp add: inf_fun_def) lemma inf2D1: "(A \ B) x y ==> A x y" by (simp add: inf_fun_def) lemma inf1D2: "(A \ B) x ==> B x" by (simp add: inf_fun_def) lemma inf2D2: "(A \ B) x y ==> B x y" by (simp add: inf_fun_def) lemma sup1I1: "A x ==> (A \ B) x" by (simp add: sup_fun_def) lemma sup2I1: "A x y ==> (A \ B) x y" by (simp add: sup_fun_def) lemma sup1I2: "B x ==> (A \ B) x" by (simp add: sup_fun_def) lemma sup2I2: "B x y ==> (A \ B) x y" by (simp add: sup_fun_def) lemma sup1E: "(A \ B) x ==> (A x ==> P) ==> (B x ==> P) ==> P" by (simp add: sup_fun_def) iprover lemma sup2E: "(A \ B) x y ==> (A x y ==> P) ==> (B x y ==> P) ==> P" by (simp add: sup_fun_def) iprover text {* \medskip Classical introduction rule: no commitment to @{text A} vs @{text B}. *} lemma sup1CI: "(¬ B x ==> A x) ==> (A \ B) x" by (auto simp add: sup_fun_def) lemma sup2CI: "(¬ B x y ==> A x y) ==> (A \ B) x y" by (auto simp add: sup_fun_def) no_notation less_eq (infix "\" 50) and less (infix "\" 50) end ```