Theory Lattice_ZF

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

    Copyright (C) 2020  Slawomir Kolodynski

    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