Theory HOL-Library.Complemented_Lattices
section ‹Complemented Lattices›
theory Complemented_Lattices
imports Main
begin
text ‹The following class ‹complemented_lattice› describes complemented lattices (with
\<^const>‹uminus› for the complement). The definition follows
🌐‹https://en.wikipedia.org/wiki/Complemented_lattice#Definition_and_basic_properties›.
Additionally, it adopts the convention from \<^class>‹boolean_algebra› of defining
\<^const>‹minus› in terms of the complement.›
class complemented_lattice = bounded_lattice + uminus + minus
opening lattice_syntax +
assumes inf_compl_bot [simp]: ‹x ⊓ - x = ⊥›
and sup_compl_top [simp]: ‹x ⊔ - x = ⊤›
and diff_eq: ‹x - y = x ⊓ - y›
begin
lemma dual_complemented_lattice:
"class.complemented_lattice (λx y. x ⊔ (- y)) uminus (⊔) (λx y. y ≤ x) (λx y. y < x) (⊓) ⊤ ⊥"
proof (rule class.complemented_lattice.intro)
show "class.bounded_lattice (⊔) (λx y. y ≤ x) (λx y. y < x) (⊓) ⊤ ⊥"
by (rule dual_bounded_lattice)
show "class.complemented_lattice_axioms (λx y. x ⊔ - y) uminus (⊔) (⊓) ⊤ ⊥"
by (unfold_locales, auto simp add: diff_eq)
qed
lemma compl_inf_bot [simp]: ‹- x ⊓ x = ⊥›
by (simp add: inf_commute)
lemma compl_sup_top [simp]: ‹- x ⊔ x = ⊤›
by (simp add: sup_commute)
end
class complete_complemented_lattice = complemented_lattice + complete_lattice
text ‹The following class ‹complemented_lattice› describes orthocomplemented lattices,
following 🌐‹https://en.wikipedia.org/wiki/Complemented_lattice#Orthocomplementation›.›
class orthocomplemented_lattice = complemented_lattice
opening lattice_syntax +
assumes ortho_involution [simp]: "- (- x) = x"
and ortho_antimono: "x ≤ y ⟹ - x ≥ - y" begin
lemma dual_orthocomplemented_lattice:
"class.orthocomplemented_lattice (λx y. x ⊔ - y) uminus (⊔) (λx y. y ≤ x) (λx y. y < x) (⊓) ⊤ ⊥"
proof (rule class.orthocomplemented_lattice.intro)
show "class.complemented_lattice (λx y. x ⊔ - y) uminus (⊔) (λx y. y ≤ x) (λx y. y < x) (⊓) ⊤ ⊥"
by (rule dual_complemented_lattice)
show "class.orthocomplemented_lattice_axioms uminus (λx y. y ≤ x)"
by (unfold_locales, auto simp add: diff_eq intro: ortho_antimono)
qed
lemma compl_eq_compl_iff [simp]: ‹- x = - y ⟷ x = y› (is ‹?P ⟷ ?Q›)
proof
assume ?P
then have ‹- (- x) = - (- y)›
by simp
then show ?Q
by simp
next
assume ?Q
then show ?P
by simp
qed
lemma compl_bot_eq [simp]: ‹- ⊥ = ⊤›
proof -
have ‹- ⊥ = - (⊤ ⊓ - ⊤)›
by simp
also have ‹… = ⊤›
by (simp only: inf_top_left) simp
finally show ?thesis .
qed
lemma compl_top_eq [simp]: "- ⊤ = ⊥"
using compl_bot_eq ortho_involution by blast
text ‹De Morgan's law›
lemma compl_sup [simp]: "- (x ⊔ y) = - x ⊓ - y"
proof -
have "- (x ⊔ y) ≤ - x"
by (simp add: ortho_antimono)
moreover have "- (x ⊔ y) ≤ - y"
by (simp add: ortho_antimono)
ultimately have 1: "- (x ⊔ y) ≤ - x ⊓ - y"
by (simp add: sup.coboundedI1)
have ‹x ≤ - (-x ⊓ -y)›
by (metis inf.cobounded1 ortho_antimono ortho_involution)
moreover have ‹y ≤ - (-x ⊓ -y)›
by (metis inf.cobounded2 ortho_antimono ortho_involution)
ultimately have ‹x ⊔ y ≤ - (-x ⊓ -y)›
by auto
hence 2: ‹-x ⊓ -y ≤ - (x ⊔ y)›
using ortho_antimono by fastforce
from 1 2 show ?thesis
using dual_order.antisym by blast
qed
text ‹De Morgan's law›
lemma compl_inf [simp]: "- (x ⊓ y) = - x ⊔ - y"
using compl_sup
by (metis ortho_involution)
lemma compl_mono:
assumes "x ≤ y"
shows "- y ≤ - x"
by (simp add: assms local.ortho_antimono)
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"
using assms ortho_antimono by fastforce
lemma compl_le_swap2:
assumes "- y ≤ x"
shows "- x ≤ y"
using assms local.ortho_antimono by fastforce
lemma compl_less_compl_iff[simp]: "- x < - y ⟷ y < x"
by (auto simp add: less_le)
lemma compl_less_swap1:
assumes "y < - x"
shows "x < - y"
using assms compl_less_compl_iff by fastforce
lemma compl_less_swap2:
assumes "- y < x"
shows "- x < y"
using assms compl_le_swap1 compl_le_swap2 less_le_not_le by auto
lemma sup_cancel_left1: ‹x ⊔ a ⊔ (- x ⊔ b) = ⊤›
by (simp add: sup_commute sup_left_commute)
lemma sup_cancel_left2: ‹- x ⊔ a ⊔ (x ⊔ b) = ⊤›
by (simp add: sup.commute sup_left_commute)
lemma inf_cancel_left1: ‹x ⊓ a ⊓ (- x ⊓ b) = ⊥›
by (simp add: inf.left_commute inf_commute)
lemma inf_cancel_left2: ‹- x ⊓ a ⊓ (x ⊓ b) = ⊥›
using inf.left_commute inf_commute by auto
lemma sup_compl_top_left1 [simp]: ‹- x ⊔ (x ⊔ y) = ⊤›
by (simp add: sup_assoc[symmetric])
lemma sup_compl_top_left2 [simp]: ‹x ⊔ (- x ⊔ y) = ⊤›
using sup_compl_top_left1[of "- x" y] by simp
lemma inf_compl_bot_left1 [simp]: ‹- x ⊓ (x ⊓ y) = ⊥›
by (simp add: inf_assoc[symmetric])
lemma inf_compl_bot_left2 [simp]: ‹x ⊓ (- x ⊓ y) = ⊥›
using inf_compl_bot_left1[of "- x" y] by simp
lemma inf_compl_bot_right [simp]: ‹x ⊓ (y ⊓ - x) = ⊥›
by (subst inf_left_commute) simp
end
class complete_orthocomplemented_lattice = orthocomplemented_lattice + complete_lattice
begin
subclass complete_complemented_lattice ..
end
text ‹The following class ‹orthomodular_lattice› describes orthomodular lattices,
following 🌐‹https://en.wikipedia.org/wiki/Complemented_lattice#Orthomodular_lattices›.›
class orthomodular_lattice = orthocomplemented_lattice
opening lattice_syntax +
assumes orthomodular: "x ≤ y ⟹ x ⊔ (- x) ⊓ y = y" begin
lemma dual_orthomodular_lattice:
"class.orthomodular_lattice (λx y. x ⊔ - y) uminus (⊔) (λx y. y ≤ x) (λx y. y < x) (⊓) ⊤ ⊥"
proof (rule class.orthomodular_lattice.intro)
show "class.orthocomplemented_lattice (λx y. x ⊔ - y) uminus (⊔) (λx y. y ≤ x) (λx y. y < x) (⊓) ⊤ ⊥"
by (rule dual_orthocomplemented_lattice)
show "class.orthomodular_lattice_axioms uminus (⊔) (λx y. y ≤ x) (⊓)"
proof (unfold_locales)
show "(x::'a) ⊓ (- x ⊔ y) = y"
if "(y::'a) ≤ x"
for x :: 'a
and y :: 'a
using that local.compl_eq_compl_iff local.ortho_antimono local.orthomodular by fastforce
qed
qed
end
class complete_orthomodular_lattice = orthomodular_lattice + complete_lattice
begin
subclass complete_orthocomplemented_lattice ..
end
context boolean_algebra
opening lattice_syntax
begin
subclass orthomodular_lattice
proof
fix x y
show ‹x ⊔ - x ⊓ y = y›
if ‹x ≤ y›
using that
by (simp add: sup.absorb_iff2 sup_inf_distrib1)
show ‹x - y = x ⊓ - y›
by (simp add: diff_eq)
qed auto
end
context complete_boolean_algebra
begin
subclass complete_orthomodular_lattice ..
end
lemma image_of_maximum:
fixes f::"'a::order ⇒ 'b::conditionally_complete_lattice"
assumes "mono f"
and "⋀x. x:M ⟹ x≤m"
and "m:M"
shows "(SUP x∈M. f x) = f m"
by (smt (verit, ccfv_threshold) assms(1) assms(2) assms(3) cSup_eq_maximum imageE imageI monoD)
lemma cSup_eq_cSup:
fixes A B :: ‹'a::conditionally_complete_lattice set›
assumes bdd: ‹bdd_above A›
assumes B: ‹⋀a. a∈A ⟹ ∃b∈B. b ≥ a›
assumes A: ‹⋀b. b∈B ⟹ ∃a∈A. a ≥ b›
shows ‹Sup A = Sup B›
proof (cases ‹B = {}›)
case True
with A B have ‹A = {}›
by auto
with True show ?thesis by simp
next
case False
have ‹bdd_above B›
by (meson A bdd bdd_above_def order_trans)
have ‹A ≠ {}›
using A False by blast
moreover have ‹a ≤ Sup B› if ‹a ∈ A› for a
proof -
obtain b where ‹b ∈ B› and ‹b ≥ a›
using B ‹a ∈ A› by auto
then show ?thesis
apply (rule cSup_upper2)
using ‹bdd_above B› by simp
qed
moreover have ‹Sup B ≤ c› if ‹⋀a. a ∈ A ⟹ a ≤ c› for c
using False apply (rule cSup_least)
using A that by fastforce
ultimately show ?thesis
by (rule cSup_eq_non_empty)
qed
end