Quelle Complemented_Lattices.thy Sprache: Isabelle

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

section \<open>Complemented Lattices\<close>

theory Complemented_Lattices
  imports Main
begin

text \<open>The following class \<open>complemented_lattice\<close> describes complemented lattices (with
  \<^const>\<open>uminus\<close> for the complement). The definition follows
  \<^url>\<open>https://en.wikipedia.org/wiki/Complemented_lattice#Definition_and_basic_properties\<close>.
  Additionally, it adopts the convention from \<^class>\<open>boolean_algebra\<close> of defining
  \<^const>\<open>minus\<close> in terms of the complement.\<close>

class complemented_lattice = bounded_lattice + uminus + minus
  opening lattice_syntax +
  assumes inf_compl_bot [simp]: \<open>x \<sqinter> - x = \<bottom>\<close>
    and sup_compl_top [simp]: \<open>x \<squnion> - x = \<top>\<close>
    and diff_eq: \<open>x - y = x \<sqinter> - y\<close>
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]: \<open>- x \<sqinter> x = \<bottom>\<close>
  by (simp add: inf_commute)

lemma compl_sup_top [simp]: \<open>- x \<squnion> x = \<top>\<close>
  by (simp add: sup_commute)

end

class complete_complemented_lattice = complemented_lattice + complete_lattice

text \<open>The following class \<open>complemented_lattice\<close> describes orthocomplemented lattices,
  following   \<^url>\<open>https://en.wikipedia.org/wiki/Complemented_lattice#Orthocomplementation\<close>.\<close>
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]: \<open>- x = - y \<longleftrightarrow> x = y\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
proof
  assume ?P
  then have \<open>- (- x) = - (- y)\<close>
    by simp
  then show ?Q
    by simp
next
  assume ?Q
  then show ?P
    by simp
qed

lemma compl_bot_eq [simp]: \<open>- \<bottom> = \<top>\<close>
proof -
  have \<open>- \<bottom> = - (\<top> \<sqinter> - \<top>)\<close>
    by simp
  also have \<open>\<dots> = \<top>\<close>
    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 \<open>De Morgan's law\<close> \<comment> \<open>Proof from \<^url>\<open>https://planetmath.org/orthocomplementedlattice\<close>\<close>
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 \<open>x \<le> - (-x \<sqinter> -y)\<close>
    by (metis inf.cobounded1 ortho_antimono ortho_involution)
  moreover have \<open>y \<le> - (-x \<sqinter> -y)\<close>
    by (metis inf.cobounded2 ortho_antimono ortho_involution)
  ultimately have \<open>x \<squnion> y \<le> - (-x \<sqinter> -y)\<close>
    by auto
  hence 2: \<open>-x \<sqinter> -y \<le> - (x \<squnion> y)\<close>
    using ortho_antimono by fastforce
  from 1 2 show ?thesis
    using dual_order.antisym by blast
qed

text \<open>De Morgan's law\<close>
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: \<open>x \<squnion> a \<squnion> (- x \<squnion> b) = \<top>\<close>
  by (simp add: sup_commute sup_left_commute)

lemma sup_cancel_left2: \<open>- x \<squnion> a \<squnion> (x \<squnion> b) = \<top>\<close>
  by (simp add: sup.commute sup_left_commute)

lemma inf_cancel_left1: \<open>x \<sqinter> a \<sqinter> (- x \<sqinter> b) = \<bottom>\<close>
  by (simp add: inf.left_commute inf_commute)

lemma inf_cancel_left2: \<open>- x \<sqinter> a \<sqinter> (x \<sqinter> b) = \<bottom>\<close>
  using inf.left_commute inf_commute by auto

lemma sup_compl_top_left1 [simp]: \<open>- x \<squnion> (x \<squnion> y) = \<top>\<close>
  by (simp add: sup_assoc[symmetric])

lemma sup_compl_top_left2 [simp]: \<open>x \<squnion> (- x \<squnion> y) = \<top>\<close>
  using sup_compl_top_left1[of "- x" y] by simp

lemma inf_compl_bot_left1 [simp]: \<open>- x \<sqinter> (x \<sqinter> y) = \<bottom>\<close>
  by (simp add: inf_assoc[symmetric])

lemma inf_compl_bot_left2 [simp]: \<open>x \<sqinter> (- x \<sqinter> y) = \<bottom>\<close>
  using inf_compl_bot_left1[of "- x" y] by simp

lemma inf_compl_bot_right [simp]: \<open>x \<sqinter> (y \<sqinter> - x) = \<bottom>\<close>
  by (subst inf_left_commute) simp

end

class complete_orthocomplemented_lattice = orthocomplemented_lattice + complete_lattice
begin

subclass complete_complemented_lattice ..

end

text \<open>The following class \<open>orthomodular_lattice\<close> describes orthomodular lattices,
following   \<^url>\<open>https://en.wikipedia.org/wiki/Complemented_lattice#Orthomodular_lattices\<close>.\<close>
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 \<open>x \<squnion> - x \<sqinter> y = y\<close>
    if \<open>x \<le> y\<close>
    using that
    by (simp add: sup.absorb_iff2 sup_inf_distrib1)
  show \<open>x - y = x \<sqinter> - y\<close>
    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 :: \<open>'a::conditionally_complete_lattice set\<close>
  assumes bdd: \<open>bdd_above A\<close>
  assumes B: \<open>\<And>a. a\<in>A \<Longrightarrow> \<exists>b\<in>B. b \<ge> a\<close>
  assumes A: \<open>\<And>b. b\<in>B \<Longrightarrow> \<exists>a\<in>A. a \<ge> b\<close>
  shows \<open>Sup A = Sup B\<close>
proof (cases \<open>B = {}\<close>)
  case True
  with A B have \<open>A = {}\<close>
    by auto
  with True show ?thesis by simp
next
  case False
  have \<open>bdd_above B\<close>
    by (meson A bdd bdd_above_def order_trans)
  have \<open>A \<noteq> {}\<close>
    using A False by blast
  moreover have \<open>a \<le> Sup B\<close> if \<open>a \<in> A\<close> for a
  proof -
    obtain b where \<open>b \<in> B\<close> and \<open>b \<ge> a\<close>
      using B \<open>a \<in> A\<close> by auto
    then show ?thesis
      apply (rule cSup_upper2)
      using \<open>bdd_above B\<close> by simp
  qed
  moreover have \<open>Sup B \<le> c\<close> if \<open>\<And>a. a \<in> A \<Longrightarrow> a \<le> c\<close> for c
    using False apply (rule cSup_least)
    using A that by fastforce
  ultimately show ?thesis
    by (rule cSup_eq_non_empty)
qed

end

quality99%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.