(* 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