Quelle  Complemented_Lattices.thy

(*  Title:      HOL/Library/Complemented_Lattices.thy
  Authors: Jose Manuel Rodriguez Caballero, Dominique Unruh
*)

section ‹Complemented Lattices›

theory Complemented_Lattices
  imports Main
begin

text ‹The following class ‹complemented_lattice› describes complemented lattices (with
  🍋‹uminus› for the complement). The definition follows
  🪙‹https://en.wikipedia.org/wiki/Complemented_lattice#Definition_and_basic_properties›.
  Additionally, it adopts the convention from 🍋‹boolean_algebra› of defining
  🍋‹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› 🍋 ‹Proof from 🪙‹https://planetmath.org/orthocomplementedlattice›\›
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