--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Complemented_Lattices.thy Thu Apr 07 05:55:48 2022 +0000
@@ -0,0 +1,272 @@
+(* 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 (\<lambda>x y. x \<squnion> (- y)) uminus (\<squnion>) (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x) (\<sqinter>) \<top> \<bottom>"
+proof (rule class.complemented_lattice.intro)
+ show "class.bounded_lattice (\<squnion>) (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x) (\<sqinter>) \<top> \<bottom>"
+ by (rule dual_bounded_lattice)
+ show "class.complemented_lattice_axioms (\<lambda>x y. x \<squnion> - y) uminus (\<squnion>) (\<sqinter>) \<top> \<bottom>"
+ 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 \<le> y \<Longrightarrow> - x \<ge> - y" begin
+
+lemma dual_orthocomplemented_lattice:
+ "class.orthocomplemented_lattice (\<lambda>x y. x \<squnion> - y) uminus (\<squnion>) (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x) (\<sqinter>) \<top> \<bottom>"
+proof (rule class.orthocomplemented_lattice.intro)
+ show "class.complemented_lattice (\<lambda>x y. x \<squnion> - y) uminus (\<squnion>) (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x) (\<sqinter>) \<top> \<bottom>"
+ by (rule dual_complemented_lattice)
+ show "class.orthocomplemented_lattice_axioms uminus (\<lambda>x y. y \<le> 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]: "- \<top> = \<bottom>"
+ 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 \<squnion> y) = - x \<sqinter> - y"
+proof -
+ have "- (x \<squnion> y) \<le> - x"
+ by (simp add: ortho_antimono)
+ moreover have "- (x \<squnion> y) \<le> - y"
+ by (simp add: ortho_antimono)
+ ultimately have 1: "- (x \<squnion> y) \<le> - x \<sqinter> - 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 \<sqinter> y) = - x \<squnion> - y"
+ using compl_sup
+ by (metis ortho_involution)
+
+lemma compl_mono:
+ assumes "x \<le> y"
+ shows "- y \<le> - x"
+ by (simp add: assms local.ortho_antimono)
+
+lemma compl_le_compl_iff [simp]: "- x \<le> - y \<longleftrightarrow> y \<le> x"
+ by (auto dest: compl_mono)
+
+lemma compl_le_swap1:
+ assumes "y \<le> - x"
+ shows "x \<le> -y"
+ using assms ortho_antimono by fastforce
+
+lemma compl_le_swap2:
+ assumes "- y \<le> x"
+ shows "- x \<le> y"
+ using assms local.ortho_antimono by fastforce
+
+lemma compl_less_compl_iff[simp]: "- x < - y \<longleftrightarrow> 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 \<le> y \<Longrightarrow> x \<squnion> (- x) \<sqinter> y = y" begin
+
+lemma dual_orthomodular_lattice:
+ "class.orthomodular_lattice (\<lambda>x y. x \<squnion> - y) uminus (\<squnion>) (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x) (\<sqinter>) \<top> \<bottom>"
+proof (rule class.orthomodular_lattice.intro)
+ show "class.orthocomplemented_lattice (\<lambda>x y. x \<squnion> - y) uminus (\<squnion>) (\<lambda>x y. y \<le> x) (\<lambda>x y. y < x) (\<sqinter>) \<top> \<bottom>"
+ by (rule dual_orthocomplemented_lattice)
+ show "class.orthomodular_lattice_axioms uminus (\<squnion>) (\<lambda>x y. y \<le> x) (\<sqinter>)"
+ proof (unfold_locales)
+ show "(x::'a) \<sqinter> (- x \<squnion> y) = y"
+ if "(y::'a) \<le> 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 \<Rightarrow> 'b::conditionally_complete_lattice"
+ assumes "mono f"
+ and "\<And>x. x:M \<Longrightarrow> x\<le>m"
+ and "m:M"
+ shows "(SUP x\<in>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