# Theory Lattice_ZF

(*    This file is a part of IsarMathLib -
a library of formalized mathematics for Isabelle/Isar.

This program is free software; Redistribution and use in source and binary forms,
with or without modification, are permitted provided that the following conditions are met:

1. Redistributions of source code must retain the above copyright notice,
this list of conditions and the following disclaimer.
2. Redistributions in binary form must reproduce the above copyright notice,
this list of conditions and the following disclaimer in the documentation and/or
other materials provided with the distribution.
3. The name of the author may not be used to endorse or promote products
derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE AUTHOR AS IS'' AND ANY EXPRESS OR IMPLIED
WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED.
IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS;
OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR
OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE,
EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

*)

section ‹Semilattices and Lattices ›

theory Lattice_ZF imports Order_ZF_1a func1

begin

text‹ Lattices can be introduced in algebraic way as commutative idempotent ($x\cdot x =x$)
semigroups or as partial orders with some additional properties. These two approaches are
equivalent. In this theory we will use the order-theoretic approach. ›

subsection‹Semilattices›

text‹ We start with a relation $r$ which is a partial order on a set $L$. Such situation is defined
in ‹Order_ZF› as the predicate ‹IsPartOrder(L,r)›. ›

text‹ A partially ordered $(L,r)$ set is a join-semilattice if each two-element subset of $L$
has a supremum (i.e. the least upper bound). ›

definition
"IsJoinSemilattice(L,r) ≡
r⊆L×L ∧ IsPartOrder(L,r) ∧ (∀x∈L. ∀y∈L. HasAsupremum(r,{x,y}))"

text‹ A partially ordered $(L,r)$ set is a meet-semilattice if each two-element subset of $L$
has an infimum (i.e. the greatest lower bound). ›

definition
"IsMeetSemilattice(L,r) ≡
r⊆L×L ∧ IsPartOrder(L,r) ∧ (∀x∈L. ∀y∈L. HasAnInfimum(r,{x,y}))"

text‹ A partially ordered $(L,r)$ set is a lattice if it is both join and meet-semilattice, i.e. if
every two element set has a supremum (least upper bound) and infimum (greatest lower bound). ›

definition
IsAlattice (infixl "{is a lattice on}" 90) where
"r {is a lattice on} L ≡ IsJoinSemilattice(L,r) ∧ IsMeetSemilattice(L,r)"

text‹ Join is a binary operation whose value on a pair $\langle x,y\rangle$
is defined as the supremum of the set $\{ x,y\}$. ›

definition
"Join(L,r) ≡ {⟨p,Supremum(r,{fst(p),snd(p)})⟩ . p ∈ L×L}"

text‹ Meet is a binary operation whose value on a pair $\langle x,y\rangle$
is defined as the infimum of the set $\{ x,y\}$.›

definition
"Meet(L,r) ≡ {⟨p,Infimum(r,{fst(p),snd(p)})⟩ . p ∈ L×L}"

text‹Linear order is a lattice.›

lemma lin_is_latt: assumes "r⊆L×L" and "IsLinOrder(L,r)"
shows "r {is a lattice on} L"
proof -
from assms(2) have "IsPartOrder(L,r)" using Order_ZF_1_L2 by simp
with assms have "IsMeetSemilattice(L,r)" unfolding IsLinOrder_def IsMeetSemilattice_def
using inf_sup_two_el(1) by auto
moreover from assms ‹IsPartOrder(L,r)› have "IsJoinSemilattice(L,r)"
unfolding IsLinOrder_def IsJoinSemilattice_def using inf_sup_two_el(3) by auto
ultimately show ?thesis unfolding IsAlattice_def by simp
qed

text‹ In a join-semilattice join is indeed a binary operation. ›

lemma join_is_binop: assumes "IsJoinSemilattice(L,r)"
shows "Join(L,r) :  L×L → L"
proof -
from assms have "∀p ∈ L×L. Supremum(r,{fst(p),snd(p)}) ∈ L"
unfolding IsJoinSemilattice_def IsPartOrder_def HasAsupremum_def using sup_in_space
by auto
then show ?thesis unfolding Join_def using ZF_fun_from_total by simp
qed

text‹ The value of ‹Join(L,r)› on a pair $\langle x,y\rangle$ is the supremum
of the set $\{ x,y\}$, hence its is greater or equal than both. ›

lemma join_val:
assumes "IsJoinSemilattice(L,r)" "x∈L" "y∈L"
defines "j ≡ Join(L,r)⟨x,y⟩"
shows "j∈L" "j = Supremum(r,{x,y})" "⟨x,j⟩ ∈ r" "⟨y,j⟩ ∈ r"
proof -
from assms(1) have "Join(L,r) :  L×L → L" using join_is_binop by simp
with assms(2,3,4) show "j = Supremum(r,{x,y})" unfolding Join_def using ZF_fun_from_tot_val
by auto
from assms(2,3,4) ‹Join(L,r) : L×L → L›  show "j∈L" using apply_funtype by simp
from assms(1,2,3) have "r ⊆ L×L" "antisym(r)" "HasAminimum(r,⋂z∈{x,y}. r{z})"
unfolding IsJoinSemilattice_def IsPartOrder_def HasAsupremum_def by auto
with ‹j = Supremum(r,{x,y})› show "⟨x,j⟩ ∈ r" and "⟨y,j⟩ ∈ r"
using sup_in_space(2) by auto
qed

text‹ In a meet-semilattice meet is indeed a binary operation. ›

lemma meet_is_binop: assumes "IsMeetSemilattice(L,r)"
shows "Meet(L,r) :  L×L → L"
proof -
from assms have "∀p ∈ L×L. Infimum(r,{fst(p),snd(p)}) ∈ L"
unfolding IsMeetSemilattice_def IsPartOrder_def HasAnInfimum_def using inf_in_space
by auto
then show ?thesis unfolding Meet_def using ZF_fun_from_total by simp
qed

text‹ The value of ‹Meet(L,r)› on a pair $\langle x,y\rangle$ is the infimum
of the set $\{ x,y\}$, hence is less or equal than both. ›

lemma meet_val:
assumes "IsMeetSemilattice(L,r)" "x∈L" "y∈L"
defines "m ≡ Meet(L,r)⟨x,y⟩"
shows "m∈L" "m = Infimum(r,{x,y})" "⟨m,x⟩ ∈ r" "⟨m,y⟩ ∈ r"
proof -
from assms(1) have "Meet(L,r) : L×L → L" using meet_is_binop by simp
with assms(2,3,4) show  "m = Infimum(r,{x,y})" unfolding Meet_def using ZF_fun_from_tot_val
by auto
from assms(2,3,4) ‹Meet(L,r) : L×L → L›  show "m∈L" using apply_funtype by simp
from assms(1,2,3) have "r ⊆ L×L" "antisym(r)" "HasAmaximum(r,⋂z∈{x,y}. r-{z})"
unfolding IsMeetSemilattice_def IsPartOrder_def HasAnInfimum_def by auto
with ‹m = Infimum(r,{x,y})› show "⟨m,x⟩ ∈ r" and "⟨m,y⟩ ∈ r"
using inf_in_space(2) by auto
qed

text‹In a (nonempty) meet semi-lattice the relation down-directs the set. ›

lemma meet_down_directs: assumes "IsMeetSemilattice(L,r)" "L≠0"
shows "r {down-directs} L"
proof -
{ fix x y assume "x∈L" "y∈L"
let ?m = "Meet(L,r)⟨x,y⟩"
from assms(1) ‹x∈L› ‹y∈L› have  "?m∈L" "⟨?m,x⟩ ∈ r" "⟨?m,y⟩ ∈ r"
using meet_val by auto
} hence "∀x∈L. ∀y∈L. ∃m∈L. ⟨m,x⟩ ∈ r ∧⟨m,y⟩ ∈ r"
by blast
with assms(2) show ?thesis unfolding DownDirects_def by simp
qed

text‹In a (nonempty) join semi-lattice the relation up-directs the set. ›

lemma join_up_directs: assumes "IsJoinSemilattice(L,r)" "L≠0"
shows "r {up-directs} L"
proof -
{ fix x y assume "x∈L" "y∈L"
let ?m = "Join(L,r)⟨x,y⟩"
from assms(1) ‹x∈L› ‹y∈L› have  "?m∈L" "⟨x,?m⟩ ∈ r" "⟨y,?m⟩ ∈ r"
using join_val by auto
} hence "∀x∈L. ∀y∈L. ∃m∈L. ⟨x,m⟩ ∈ r ∧⟨y,m⟩ ∈ r"
by blast
with assms(2) show ?thesis unfolding UpDirects_def by simp
qed

text‹ The next locale defines a a notation for join-semilattice. We will use the $\sqcup$ symbol
rather than more common $\vee$ to avoid confusion with logical "or". ›

locale join_semilatt =
fixes L
fixes r
assumes joinLatt: "IsJoinSemilattice(L,r)"
fixes join (infixl "⊔" 71)
defines join_def [simp]: "x ⊔ y ≡ Join(L,r)⟨x,y⟩"
fixes sup ("sup _" )
defines sup_def [simp]: "sup A  ≡ Supremum(r,A)"

text‹ Join of the elements of the lattice is in the lattice. ›

lemma (in join_semilatt) join_props: assumes "x∈L" "y∈L"
shows "x⊔y ∈ L" and "x⊔y = sup {x,y}"
proof -
from joinLatt assms have "Join(L,r)⟨x,y⟩ ∈ L" using join_is_binop apply_funtype
by blast
thus "x⊔y ∈ L" by simp
from joinLatt assms have "Join(L,r)⟨x,y⟩ = Supremum(r,{x,y})" using join_val(2)
by simp
thus "x⊔y = sup {x,y}" by simp
qed

text‹ Join is associative. ›

lemma (in join_semilatt) join_assoc: assumes "x∈L" "y∈L" "z∈L"
shows "x⊔(y⊔z) = x⊔y⊔z"
proof -
from joinLatt assms(2,3) have "x⊔(y⊔z) = x⊔(sup {y,z})" using join_val(2) by simp
also from assms joinLatt have "... = sup {sup {x}, sup {y,z}}"
unfolding IsJoinSemilattice_def IsPartOrder_def using join_props sup_inf_singl(2)
by auto
also have "... = sup {x,y,z}"
proof -
let ?𝒯 = "{{x},{y,z}}"
from joinLatt have "r ⊆ L×L" "antisym(r)" "trans(r)"
unfolding IsJoinSemilattice_def IsPartOrder_def by auto
moreover from joinLatt assms have "∀T∈?𝒯. HasAsupremum(r,T)"
unfolding IsJoinSemilattice_def IsPartOrder_def using sup_inf_singl(1) by blast
moreover from joinLatt assms have "HasAsupremum(r,{Supremum(r,T).T∈?𝒯})"
unfolding IsJoinSemilattice_def IsPartOrder_def  HasAsupremum_def
using sup_in_space(1) sup_inf_singl(2) by auto
ultimately have "Supremum(r,{Supremum(r,T).T∈?𝒯}) = Supremum(r,⋃?𝒯)" by (rule sup_sup)
moreover have "{Supremum(r,T).T∈?𝒯} = {sup {x}, sup {y,z}}" and "⋃?𝒯 = {x,y,z}"
by auto
ultimately show "(sup {sup {x}, sup {y,z}}) =  sup {x,y,z}" by simp
qed
also have "... = sup {sup {x,y}, sup {z}}"
proof -
let ?𝒯 = "{{x,y},{z}}"
from joinLatt have "r ⊆ L×L" "antisym(r)" "trans(r)"
unfolding IsJoinSemilattice_def IsPartOrder_def by auto
moreover from joinLatt assms have "∀T∈?𝒯. HasAsupremum(r,T)"
unfolding IsJoinSemilattice_def IsPartOrder_def using sup_inf_singl(1) by blast
moreover from joinLatt assms have "HasAsupremum(r,{Supremum(r,T).T∈?𝒯})"
unfolding IsJoinSemilattice_def IsPartOrder_def  HasAsupremum_def
using sup_in_space(1) sup_inf_singl(2) by auto
ultimately have "Supremum(r,{Supremum(r,T).T∈?𝒯}) = Supremum(r,⋃?𝒯)" by (rule sup_sup)
moreover have "{Supremum(r,T).T∈?𝒯} = {sup {x,y}, sup {z}}" and "⋃?𝒯 = {x,y,z}"
by auto
ultimately show "(sup {x,y,z}) = sup {sup {x,y}, sup {z}}" by auto
qed
also from assms joinLatt have "... = sup {sup {x,y}, z}"
unfolding IsJoinSemilattice_def IsPartOrder_def using join_props sup_inf_singl(2)
by auto
also from assms joinLatt have "... = (sup {x,y}) ⊔ z "
unfolding IsJoinSemilattice_def IsPartOrder_def using join_props by auto
also from joinLatt assms(1,2) have "... = x⊔y⊔z" using join_val(2) by simp
finally show "x⊔(y⊔z) = x⊔y⊔z" by simp
qed

text‹ Join is idempotent. ›

lemma (in join_semilatt) join_idempotent: assumes "x∈L" shows "x⊔x = x"
using joinLatt assms join_val(2) IsJoinSemilattice_def IsPartOrder_def sup_inf_singl(2)
by auto

text‹ The ‹meet_semilatt› locale is the dual of the join-semilattice locale defined above.
We will use the $\sqcap$ symbol to denote join, giving it ab bit higher precedence.›

locale meet_semilatt =
fixes L
fixes r
assumes meetLatt: "IsMeetSemilattice(L,r)"
fixes join (infixl "⊓" 72)
defines join_def [simp]: "x ⊓ y ≡ Meet(L,r)⟨x,y⟩"
fixes sup ("inf _" )
defines sup_def [simp]: "inf A  ≡ Infimum(r,A)"

text‹ Meet of the elements of the lattice is in the lattice. ›

lemma (in meet_semilatt) meet_props: assumes "x∈L" "y∈L"
shows "x⊓y ∈ L" and "x⊓y = inf {x,y}"
proof -
from meetLatt assms have "Meet(L,r)⟨x,y⟩ ∈ L" using meet_is_binop apply_funtype
by blast
thus "x⊓y ∈ L" by simp
from meetLatt assms have "Meet(L,r)⟨x,y⟩ = Infimum(r,{x,y})" using meet_val(2) by blast
thus "x⊓y = inf {x,y}" by simp
qed

text‹ Meet is associative. ›

lemma (in meet_semilatt) meet_assoc: assumes "x∈L" "y∈L" "z∈L"
shows "x⊓(y⊓z) = x⊓y⊓z"
proof -
from meetLatt assms(2,3) have "x⊓(y⊓z) = x⊓(inf {y,z})" using meet_val by simp
also from assms meetLatt have "... = inf {inf {x}, inf {y,z}}"
unfolding IsMeetSemilattice_def IsPartOrder_def using meet_props sup_inf_singl(4)
by auto
also have "... = inf {x,y,z}"
proof -
let ?𝒯 = "{{x},{y,z}}"
from meetLatt have "r ⊆ L×L" "antisym(r)" "trans(r)"
unfolding IsMeetSemilattice_def IsPartOrder_def by auto
moreover from meetLatt assms have "∀T∈?𝒯. HasAnInfimum(r,T)"
unfolding IsMeetSemilattice_def IsPartOrder_def using sup_inf_singl(3) by blast
moreover from meetLatt assms have "HasAnInfimum(r,{Infimum(r,T).T∈?𝒯})"
unfolding IsMeetSemilattice_def IsPartOrder_def  HasAnInfimum_def
using inf_in_space(1) sup_inf_singl(4) by auto
ultimately have "Infimum(r,{Infimum(r,T).T∈?𝒯}) = Infimum(r,⋃?𝒯)" by (rule inf_inf)
moreover have "{Infimum(r,T).T∈?𝒯} = {inf {x}, inf {y,z}}" and "⋃?𝒯 = {x,y,z}"
by auto
ultimately show "(inf {inf {x}, inf {y,z}}) =  inf {x,y,z}" by simp
qed
also have "... = inf {inf {x,y}, inf {z}}"
proof -
let ?𝒯 = "{{x,y},{z}}"
from meetLatt have "r ⊆ L×L" "antisym(r)" "trans(r)"
unfolding IsMeetSemilattice_def IsPartOrder_def by auto
moreover from meetLatt assms have "∀T∈?𝒯. HasAnInfimum(r,T)"
unfolding IsMeetSemilattice_def IsPartOrder_def using sup_inf_singl(3) by blast
moreover from meetLatt assms have "HasAnInfimum(r,{Infimum(r,T).T∈?𝒯})"
unfolding IsMeetSemilattice_def IsPartOrder_def HasAnInfimum_def
using inf_in_space(1) sup_inf_singl(4) by auto
ultimately have "Infimum(r,{Infimum(r,T).T∈?𝒯}) = Infimum(r,⋃?𝒯)" by (rule inf_inf)
moreover have "{Infimum(r,T).T∈?𝒯} = {inf {x,y}, inf {z}}" and "⋃?𝒯 = {x,y,z}"
by auto
ultimately show "(inf {x,y,z}) = inf {inf {x,y}, inf {z}}" by auto
qed
also from assms meetLatt have "... = inf {inf {x,y}, z}"
unfolding IsMeetSemilattice_def IsPartOrder_def using meet_props sup_inf_singl(4)
by auto
also from assms meetLatt have "... = (inf {x,y}) ⊓ z "
unfolding IsMeetSemilattice_def IsPartOrder_def using meet_props by auto
also from meetLatt assms(1,2) have "... = x⊓y⊓z" using meet_val by simp
finally show "x⊓(y⊓z) = x⊓y⊓z" by simp
qed

text‹ Meet is idempotent. ›

lemma (in meet_semilatt) meet_idempotent: assumes "x∈L" shows "x⊓x = x"
using meetLatt assms meet_val IsMeetSemilattice_def IsPartOrder_def sup_inf_singl(4)
by auto

end