Theory P_Algebras
section ‹Pseudocomplemented Algebras›
text ‹
This theory expands lattices with a pseudocomplement operation.
In particular, we consider the following algebraic structures:
\begin{itemize}
\item pseudocomplemented lattices (p-algebras)
\item pseudocomplemented distributive lattices (distributive p-algebras)
\item Stone algebras
\item Heyting semilattices
\item Heyting lattices
\item Heyting algebras
\item Heyting-Stone algebras
\item Brouwer algebras
\item Boolean algebras
\end{itemize}
Most of these structures and many results in this theory are discussed in \<^cite>‹"BalbesDwinger1974" and "Birkhoff1967" and "Blyth2005" and "Curry1977" and "Graetzer1971" and "Maddux1996"›.
›
theory P_Algebras
imports Lattice_Basics
begin
subsection ‹P-Algebras›
text ‹
In this section we add a pseudocomplement operation to lattices and to distributive lattices.
›
subsubsection ‹Pseudocomplemented Lattices›
text ‹
The pseudocomplement of an element ‹y› is the greatest element whose meet with ‹y› is the least element of the lattice.
›
class p_algebra = bounded_lattice + uminus +
assumes pseudo_complement: "x ⊓ y = bot ⟷ x ≤ -y"
begin
subclass sup_inf_top_bot_uminus_ord .
text ‹
Regular elements and dense elements are frequently used in pseudocomplemented algebras.
›
abbreviation "regular x ≡ x = --x"
abbreviation "dense x ≡ -x = bot"
abbreviation "complemented x ≡ ∃y . x ⊓ y = bot ∧ x ⊔ y = top"
abbreviation "in_p_image x ≡ ∃y . x = -y"
abbreviation "selection s x ≡ s = --s ⊓ x"
abbreviation "dense_elements ≡ { x . dense x }"
abbreviation "regular_elements ≡ { x . in_p_image x }"
lemma p_bot [simp]:
"-bot = top"
using inf_top.left_neutral pseudo_complement top_unique by blast
lemma p_top [simp]:
"-top = bot"
by (metis eq_refl inf_top.comm_neutral pseudo_complement)
text ‹
The pseudocomplement satisfies the following half of the requirements of a complement.
›
lemma inf_p [simp]:
"x ⊓ -x = bot"
using inf.commute pseudo_complement by fastforce
lemma p_inf [simp]:
"-x ⊓ x = bot"
by (simp add: inf_commute)
lemma pp_inf_p:
"--x ⊓ -x = bot"
by simp
text ‹
The double complement is a closure operation.
›
lemma pp_increasing:
"x ≤ --x"
using inf_p pseudo_complement by blast
lemma ppp [simp]:
"---x = -x"
by (metis order.antisym inf.commute order_trans pseudo_complement pp_increasing)
lemma pp_idempotent:
"----x = --x"
by simp
lemma regular_in_p_image_iff:
"regular x ⟷ in_p_image x"
by auto
lemma pseudo_complement_pp:
"x ⊓ y = bot ⟷ --x ≤ -y"
by (metis inf_commute pseudo_complement ppp)
lemma p_antitone:
"x ≤ y ⟹ -y ≤ -x"
by (metis inf_commute order_trans pseudo_complement pp_increasing)
lemma p_antitone_sup:
"-(x ⊔ y) ≤ -x"
by (simp add: p_antitone)
lemma p_antitone_inf:
"-x ≤ -(x ⊓ y)"
by (simp add: p_antitone)
lemma p_antitone_iff:
"x ≤ -y ⟷ y ≤ -x"
using order_lesseq_imp p_antitone pp_increasing by blast
lemma pp_isotone:
"x ≤ y ⟹ --x ≤ --y"
by (simp add: p_antitone)
lemma pp_isotone_sup:
"--x ≤ --(x ⊔ y)"
by (simp add: p_antitone)
lemma pp_isotone_inf:
"--(x ⊓ y) ≤ --x"
by (simp add: p_antitone)
text ‹
One of De Morgan's laws holds in pseudocomplemented lattices.
›
lemma p_dist_sup [simp]:
"-(x ⊔ y) = -x ⊓ -y"
apply (rule order.antisym)
apply (simp add: p_antitone)
using inf_le1 inf_le2 le_sup_iff p_antitone_iff by blast
lemma p_supdist_inf:
"-x ⊔ -y ≤ -(x ⊓ y)"
by (simp add: p_antitone)
lemma pp_dist_pp_sup [simp]:
"--(--x ⊔ --y) = --(x ⊔ y)"
by simp
lemma p_sup_p [simp]:
"-(x ⊔ -x) = bot"
by simp
lemma pp_sup_p [simp]:
"--(x ⊔ -x) = top"
by simp
lemma dense_pp:
"dense x ⟷ --x = top"
by (metis p_bot p_top ppp)
lemma dense_sup_p:
"dense (x ⊔ -x)"
by simp
lemma regular_char:
"regular x ⟷ (∃y . x = -y)"
by auto
lemma pp_inf_bot_iff:
"x ⊓ y = bot ⟷ --x ⊓ y = bot"
by (simp add: pseudo_complement_pp)
text ‹
Weak forms of the shunting property hold.
Most require a pseudocomplemented element on the right-hand side.
›
lemma p_shunting_swap:
"x ⊓ y ≤ -z ⟷ x ⊓ z ≤ -y"
by (metis inf_assoc inf_commute pseudo_complement)
lemma pp_inf_below_iff:
"x ⊓ y ≤ -z ⟷ --x ⊓ y ≤ -z"
by (simp add: inf_commute p_shunting_swap)
lemma p_inf_pp [simp]:
"-(x ⊓ --y) = -(x ⊓ y)"
apply (rule order.antisym)
apply (simp add: inf.coboundedI2 p_antitone pp_increasing)
using inf_commute p_antitone_iff pp_inf_below_iff by auto
lemma p_inf_pp_pp [simp]:
"-(--x ⊓ --y) = -(x ⊓ y)"
by (simp add: inf_commute)
lemma regular_closed_inf:
"regular x ⟹ regular y ⟹ regular (x ⊓ y)"
by (metis p_dist_sup ppp)
lemma regular_closed_p:
"regular (-x)"
by simp
lemma regular_closed_pp:
"regular (--x)"
by simp
lemma regular_closed_bot:
"regular bot"
by simp
lemma regular_closed_top:
"regular top"
by simp
lemma pp_dist_inf [simp]:
"--(x ⊓ y) = --x ⊓ --y"
by (metis p_dist_sup p_inf_pp_pp ppp)
lemma inf_import_p [simp]:
"x ⊓ -(x ⊓ y) = x ⊓ -y"
apply (rule order.antisym)
using p_shunting_swap apply fastforce
using inf.sup_right_isotone p_antitone by auto
text ‹
Pseudocomplements are unique.
›
lemma p_unique:
"(∀x . x ⊓ y = bot ⟷ x ≤ z) ⟹ z = -y"
using inf.order_eq_iff pseudo_complement by auto
lemma maddux_3_5:
"x ⊔ x = x ⊔ -(y ⊔ -y)"
by simp
lemma shunting_1_pp:
"x ≤ --y ⟷ x ⊓ -y = bot"
by (simp add: pseudo_complement)
lemma pp_pp_inf_bot_iff:
"x ⊓ y = bot ⟷ --x ⊓ --y = bot"
by (simp add: pseudo_complement_pp)
lemma inf_pp_semi_commute:
"x ⊓ --y ≤ --(x ⊓ y)"
using inf.eq_refl p_antitone_iff p_inf_pp by presburger
lemma inf_pp_commute:
"--(--x ⊓ y) = --x ⊓ --y"
by simp
lemma sup_pp_semi_commute:
"x ⊔ --y ≤ --(x ⊔ y)"
by (simp add: p_antitone_iff)
lemma regular_sup:
"regular z ⟹ (x ≤ z ∧ y ≤ z ⟷ --(x ⊔ y) ≤ z)"
apply (rule iffI)
apply (metis le_supI pp_isotone)
using dual_order.trans sup_ge2 pp_increasing pp_isotone_sup by blast
lemma dense_closed_inf:
"dense x ⟹ dense y ⟹ dense (x ⊓ y)"
by (simp add: dense_pp)
lemma dense_closed_sup:
"dense x ⟹ dense y ⟹ dense (x ⊔ y)"
by simp
lemma dense_closed_pp:
"dense x ⟹ dense (--x)"
by simp
lemma dense_closed_top:
"dense top"
by simp
lemma dense_up_closed:
"dense x ⟹ x ≤ y ⟹ dense y"
using dense_pp top_le pp_isotone by auto
lemma regular_dense_top:
"regular x ⟹ dense x ⟹ x = top"
using p_bot by blast
lemma selection_char:
"selection s x ⟷ (∃y . s = -y ⊓ x)"
by (metis inf_import_p inf_commute regular_closed_p)
lemma selection_closed_inf:
"selection s x ⟹ selection t x ⟹ selection (s ⊓ t) x"
by (metis inf_assoc inf_commute inf_idem pp_dist_inf)
lemma selection_closed_pp:
"regular x ⟹ selection s x ⟹ selection (--s) x"
by (metis pp_dist_inf)
lemma selection_closed_bot:
"selection bot x"
by simp
lemma selection_closed_id:
"selection x x"
using inf.le_iff_sup pp_increasing by auto
text ‹
Conjugates are usually studied for Boolean algebras, however, some of their properties generalise to pseudocomplemented algebras.
›
lemma conjugate_unique_p:
assumes "conjugate f g"
and "conjugate f h"
shows "uminus ∘ g = uminus ∘ h"
proof -
have "∀x y . x ⊓ g y = bot ⟷ x ⊓ h y = bot"
using assms conjugate_def inf.commute by simp
hence "∀x y . x ≤ -(g y) ⟷ x ≤ -(h y)"
using inf.commute pseudo_complement by simp
hence "∀y . -(g y) = -(h y)"
using order.eq_iff by blast
thus ?thesis
by auto
qed
lemma conjugate_symmetric:
"conjugate f g ⟹ conjugate g f"
by (simp add: conjugate_def inf_commute)
lemma additive_isotone:
"additive f ⟹ isotone f"
by (metis additive_def isotone_def le_iff_sup)
lemma dual_additive_antitone:
assumes "dual_additive f"
shows "isotone (uminus ∘ f)"
proof -
have "∀x y . f (x ⊔ y) ≤ f x"
using assms dual_additive_def by simp
hence "∀x y . x ≤ y ⟶ f y ≤ f x"
by (metis sup_absorb2)
hence "∀x y . x ≤ y ⟶ -(f x) ≤ -(f y)"
by (simp add: p_antitone)
thus ?thesis
by (simp add: isotone_def)
qed
lemma conjugate_dual_additive:
assumes "conjugate f g"
shows "dual_additive (uminus ∘ f)"
proof -
have 1: "∀x y z . -z ≤ -(f (x ⊔ y)) ⟷ -z ≤ -(f x) ∧ -z ≤ -(f y)"
proof (intro allI)
fix x y z
have "(-z ≤ -(f (x ⊔ y))) = (f (x ⊔ y) ⊓ -z = bot)"
by (simp add: p_antitone_iff pseudo_complement)
also have "... = ((x ⊔ y) ⊓ g(-z) = bot)"
using assms conjugate_def by auto
also have "... = (x ⊔ y ≤ -(g(-z)))"
by (simp add: pseudo_complement)
also have "... = (x ≤ -(g(-z)) ∧ y ≤ -(g(-z)))"
by (simp add: le_sup_iff)
also have "... = (x ⊓ g(-z) = bot ∧ y ⊓ g(-z) = bot)"
by (simp add: pseudo_complement)
also have "... = (f x ⊓ -z = bot ∧ f y ⊓ -z = bot)"
using assms conjugate_def by auto
also have "... = (-z ≤ -(f x) ∧ -z ≤ -(f y))"
by (simp add: p_antitone_iff pseudo_complement)
finally show "-z ≤ -(f (x ⊔ y)) ⟷ -z ≤ -(f x) ∧ -z ≤ -(f y)"
by simp
qed
have "∀x y . -(f (x ⊔ y)) = -(f x) ⊓ -(f y)"
proof (intro allI)
fix x y
have "-(f x) ⊓ -(f y) = --(-(f x) ⊓ -(f y))"
by simp
hence "-(f x) ⊓ -(f y) ≤ -(f (x ⊔ y))"
using 1 by (metis inf_le1 inf_le2)
thus "-(f (x ⊔ y)) = -(f x) ⊓ -(f y)"
using 1 order.antisym by fastforce
qed
thus ?thesis
using dual_additive_def by simp
qed
lemma conjugate_isotone_pp:
"conjugate f g ⟹ isotone (uminus ∘ uminus ∘ f)"
by (simp add: comp_assoc conjugate_dual_additive dual_additive_antitone)
lemma conjugate_char_1_pp:
"conjugate f g ⟷ (∀x y . f(x ⊓ -(g y)) ≤ --f x ⊓ -y ∧ g(y ⊓ -(f x)) ≤ --g y ⊓ -x)"
proof
assume 1: "conjugate f g"
show "∀x y . f(x ⊓ -(g y)) ≤ --f x ⊓ -y ∧ g(y ⊓ -(f x)) ≤ --g y ⊓ -x"
proof (intro allI)
fix x y
have 2: "f(x ⊓ -(g y)) ≤ -y"
using 1 by (simp add: conjugate_def pseudo_complement)
have "f(x ⊓ -(g y)) ≤ --f(x ⊓ -(g y))"
by (simp add: pp_increasing)
also have "... ≤ --f x"
using 1 conjugate_isotone_pp isotone_def by simp
finally have 3: "f(x ⊓ -(g y)) ≤ --f x ⊓ -y"
using 2 by simp
have 4: "isotone (uminus ∘ uminus ∘ g)"
using 1 conjugate_isotone_pp conjugate_symmetric by auto
have 5: "g(y ⊓ -(f x)) ≤ -x"
using 1 by (metis conjugate_def inf.cobounded2 inf_commute pseudo_complement)
have "g(y ⊓ -(f x)) ≤ --g(y ⊓ -(f x))"
by (simp add: pp_increasing)
also have "... ≤ --g y"
using 4 isotone_def by auto
finally have "g(y ⊓ -(f x)) ≤ --g y ⊓ -x"
using 5 by simp
thus "f(x ⊓ -(g y)) ≤ --f x ⊓ -y ∧ g(y ⊓ -(f x)) ≤ --g y ⊓ -x"
using 3 by simp
qed
next
assume 6: "∀x y . f(x ⊓ -(g y)) ≤ --f x ⊓ -y ∧ g(y ⊓ -(f x)) ≤ --g y ⊓ -x"
hence 7: "∀x y . f x ⊓ y = bot ⟶ x ⊓ g y = bot"
by (metis inf.le_iff_sup inf.le_sup_iff inf_commute pseudo_complement)
have "∀x y . x ⊓ g y = bot ⟶ f x ⊓ y = bot"
using 6 by (metis inf.le_iff_sup inf.le_sup_iff inf_commute pseudo_complement)
thus "conjugate f g"
using 7 conjugate_def by auto
qed
lemma conjugate_char_1_isotone:
"conjugate f g ⟹ isotone f ⟹ isotone g ⟹ f(x ⊓ -(g y)) ≤ f x ⊓ -y ∧ g(y ⊓ -(f x)) ≤ g y ⊓ -x"
by (simp add: conjugate_char_1_pp ord.isotone_def)
lemma dense_lattice_char_1:
"(∀x y . x ⊓ y = bot ⟶ x = bot ∨ y = bot) ⟷ (∀x . x ≠ bot ⟶ dense x)"
by (metis inf_top.left_neutral p_bot p_inf pp_inf_bot_iff)
lemma dense_lattice_char_2:
"(∀x y . x ⊓ y = bot ⟶ x = bot ∨ y = bot) ⟷ (∀x . regular x ⟶ x = bot ∨ x = top)"
by (metis dense_lattice_char_1 inf_top.left_neutral p_inf regular_closed_p regular_closed_top)
lemma restrict_below_Rep_eq:
"x ⊓ --y ≤ z ⟹ x ⊓ y = x ⊓ z ⊓ y"
by (metis inf.absorb2 inf.commute inf.left_commute pp_increasing)
end
text ‹
The following class gives equational axioms for the pseudocomplement operation.
›
class p_algebra_eq = bounded_lattice + uminus +
assumes p_bot_eq: "-bot = top"
and p_top_eq: "-top = bot"
and inf_import_p_eq: "x ⊓ -(x ⊓ y) = x ⊓ -y"
begin
lemma inf_p_eq:
"x ⊓ -x = bot"
by (metis inf_bot_right inf_import_p_eq inf_top_right p_top_eq)
subclass p_algebra
apply unfold_locales
apply (rule iffI)
apply (metis inf.orderI inf_import_p_eq inf_top.right_neutral p_bot_eq)
by (metis (full_types) inf.left_commute inf.orderE inf_bot_right inf_commute inf_p_eq)
end
subsubsection ‹Pseudocomplemented Distributive Lattices›
text ‹
We obtain further properties if we assume that the lattice operations are distributive.
›
class pd_algebra = p_algebra + bounded_distrib_lattice
begin
lemma p_inf_sup_below:
"-x ⊓ (x ⊔ y) ≤ y"
by (simp add: inf_sup_distrib1)
lemma pp_inf_sup_p [simp]:
"--x ⊓ (x ⊔ -x) = x"
using inf.absorb2 inf_sup_distrib1 pp_increasing by auto
lemma complement_p:
"x ⊓ y = bot ⟹ x ⊔ y = top ⟹ -x = y"
by (metis pseudo_complement inf.commute inf_top.left_neutral sup.absorb_iff1 sup.commute sup_bot.right_neutral sup_inf_distrib2 p_inf)
lemma complemented_regular:
"complemented x ⟹ regular x"
using complement_p inf.commute sup.commute by fastforce
lemma regular_inf_dense:
"∃y z . regular y ∧ dense z ∧ x = y ⊓ z"
by (metis pp_inf_sup_p dense_sup_p ppp)
lemma maddux_3_12 [simp]:
"(x ⊔ -y) ⊓ (x ⊔ y) = x"
by (metis p_inf sup_bot_right sup_inf_distrib1)
lemma maddux_3_13 [simp]:
"(x ⊔ y) ⊓ -x = y ⊓ -x"
by (simp add: inf_sup_distrib2)
lemma maddux_3_20:
"((v ⊓ w) ⊔ (-v ⊓ x)) ⊓ -((v ⊓ y) ⊔ (-v ⊓ z)) = (v ⊓ w ⊓ -y) ⊔ (-v ⊓ x ⊓ -z)"
proof -
have "v ⊓ w ⊓ -(v ⊓ y) ⊓ -(-v ⊓ z) = v ⊓ w ⊓ -(v ⊓ y)"
by (meson inf.cobounded1 inf_absorb1 le_infI1 p_antitone_iff)
also have "... = v ⊓ w ⊓ -y"
using inf.sup_relative_same_increasing inf_import_p inf_le1 by blast
finally have 1: "v ⊓ w ⊓ -(v ⊓ y) ⊓ -(-v ⊓ z) = v ⊓ w ⊓ -y"
.
have "-v ⊓ x ⊓ -(v ⊓ y) ⊓ -(-v ⊓ z) = -v ⊓ x ⊓ -(-v ⊓ z)"
by (simp add: inf.absorb1 le_infI1 p_antitone_inf)
also have "... = -v ⊓ x ⊓ -z"
by (simp add: inf.assoc inf_left_commute)
finally have 2: "-v ⊓ x ⊓ -(v ⊓ y) ⊓ -(-v ⊓ z) = -v ⊓ x ⊓ -z"
.
have "((v ⊓ w) ⊔ (-v ⊓ x)) ⊓ -((v ⊓ y) ⊔ (-v ⊓ z)) = (v ⊓ w ⊓ -(v ⊓ y) ⊓ -(-v ⊓ z)) ⊔ (-v ⊓ x ⊓ -(v ⊓ y) ⊓ -(-v ⊓ z))"
by (simp add: inf_assoc inf_sup_distrib2)
also have "... = (v ⊓ w ⊓ -y) ⊔ (-v ⊓ x ⊓ -z)"
using 1 2 by simp
finally show ?thesis
.
qed
lemma order_char_1:
"x ≤ y ⟷ x ≤ y ⊔ -x"
by (metis inf.sup_left_isotone inf_sup_absorb le_supI1 maddux_3_12 sup_commute)
lemma order_char_2:
"x ≤ y ⟷ x ⊔ -x ≤ y ⊔ -x"
using order_char_1 by auto
lemma half_shunting:
"x ≤ y ⊔ z ⟹ x ⊓ -z ≤ y"
by (metis inf.sup_right_isotone inf_commute inf_sup_distrib1 sup.boundedE maddux_3_12)
end
subsection ‹Stone Algebras›
text ‹
A Stone algebra is a distributive lattice with a pseudocomplement that satisfies the following equation.
We thus obtain the other half of the requirements of a complement at least for the regular elements.
›
class stone_algebra = pd_algebra +
assumes stone [simp]: "-x ⊔ --x = top"
begin
text ‹
As a consequence, we obtain both De Morgan's laws for all elements.
›
lemma p_dist_inf [simp]:
"-(x ⊓ y) = -x ⊔ -y"
proof (rule p_unique[THEN sym], rule allI, rule iffI)
fix w
assume "w ⊓ (x ⊓ y) = bot"
hence "w ⊓ --x ⊓ y = bot"
using inf_commute inf_left_commute pseudo_complement by auto
hence 1: "w ⊓ --x ≤ -y"
by (simp add: pseudo_complement)
have "w = (w ⊓ -x) ⊔ (w ⊓ --x)"
using distrib_imp2 sup_inf_distrib1 by auto
thus "w ≤ -x ⊔ -y"
using 1 by (metis inf_le2 sup.mono)
next
fix w
assume "w ≤ -x ⊔ -y"
thus "w ⊓ (x ⊓ y) = bot"
using order_trans p_supdist_inf pseudo_complement by blast
qed
lemma pp_dist_sup [simp]:
"--(x ⊔ y) = --x ⊔ --y"
by simp
lemma regular_closed_sup:
"regular x ⟹ regular y ⟹ regular (x ⊔ y)"
by simp
text ‹
The regular elements are precisely the ones having a complement.
›
lemma regular_complemented_iff:
"regular x ⟷ complemented x"
by (metis inf_p stone complemented_regular)
lemma selection_closed_sup:
"selection s x ⟹ selection t x ⟹ selection (s ⊔ t) x"
by (simp add: inf_sup_distrib2)
lemma huntington_3_pp [simp]:
"-(-x ⊔ -y) ⊔ -(-x ⊔ y) = --x"
by (metis p_dist_inf p_inf sup.commute sup_bot_left sup_inf_distrib1)
lemma maddux_3_3 [simp]:
"-(x ⊔ y) ⊔ -(x ⊔ -y) = -x"
by (simp add: sup_commute sup_inf_distrib1)
lemma maddux_3_11_pp:
"(x ⊓ -y) ⊔ (x ⊓ --y) = x"
by (metis inf_sup_distrib1 inf_top_right stone)
lemma maddux_3_19_pp:
"(-x ⊓ y) ⊔ (--x ⊓ z) = (--x ⊔ y) ⊓ (-x ⊔ z)"
proof -
have "(--x ⊔ y) ⊓ (-x ⊔ z) = (--x ⊓ z) ⊔ (y ⊓ -x) ⊔ (y ⊓ z)"
by (simp add: inf.commute inf_sup_distrib1 sup.assoc)
also have "... = (--x ⊓ z) ⊔ (y ⊓ -x) ⊔ (y ⊓ z ⊓ (-x ⊔ --x))"
by simp
also have "... = (--x ⊓ z) ⊔ ((y ⊓ -x) ⊔ (y ⊓ -x ⊓ z)) ⊔ (y ⊓ z ⊓ --x)"
using inf_sup_distrib1 sup_assoc inf_commute inf_assoc by presburger
also have "... = (--x ⊓ z) ⊔ (y ⊓ -x) ⊔ (y ⊓ z ⊓ --x)"
by simp
also have "... = ((--x ⊓ z) ⊔ (--x ⊓ z ⊓ y)) ⊔ (y ⊓ -x)"
by (simp add: inf_assoc inf_commute sup.left_commute sup_commute)
also have "... = (--x ⊓ z) ⊔ (y ⊓ -x)"
by simp
finally show ?thesis
by (simp add: inf_commute sup_commute)
qed
lemma compl_inter_eq_pp:
"--x ⊓ y = --x ⊓ z ⟹ -x ⊓ y = -x ⊓ z ⟹ y = z"
by (metis inf_commute inf_p inf_sup_distrib1 inf_top.right_neutral p_bot p_dist_inf)
lemma maddux_3_21_pp [simp]:
"--x ⊔ (-x ⊓ y) = --x ⊔ y"
by (simp add: sup.commute sup_inf_distrib1)
lemma shunting_2_pp:
"x ≤ --y ⟷ -x ⊔ --y = top"
by (metis inf_top_left p_bot p_dist_inf pseudo_complement)
lemma shunting_p:
"x ⊓ y ≤ -z ⟷ x ≤ -z ⊔ -y"
by (metis inf.assoc p_dist_inf p_shunting_swap pseudo_complement)
text ‹
The following weak shunting property is interesting as it does not require the element ‹z› on the right-hand side to be regular.
›
lemma shunting_var_p:
"x ⊓ -y ≤ z ⟷ x ≤ z ⊔ --y"
proof
assume "x ⊓ -y ≤ z"
hence "z ⊔ --y = --y ⊔ (z ⊔ x ⊓ -y)"
by (simp add: sup.absorb1 sup.commute)
thus "x ≤ z ⊔ --y"
by (metis inf_commute maddux_3_21_pp sup.commute sup.left_commute sup_left_divisibility)
next
assume "x ≤ z ⊔ --y"
thus "x ⊓ -y ≤ z"
by (metis inf.mono maddux_3_12 sup_ge2)
qed
lemma conjugate_char_2_pp:
"conjugate f g ⟷ f bot = bot ∧ g bot = bot ∧ (∀x y . f x ⊓ y ≤ --(f(x ⊓ --(g y))) ∧ g y ⊓ x ≤ --(g(y ⊓ --(f x))))"
proof
assume 1: "conjugate f g"
hence 2: "dual_additive (uminus ∘ g)"
using conjugate_symmetric conjugate_dual_additive by auto
show "f bot = bot ∧ g bot = bot ∧ (∀x y . f x ⊓ y ≤ --(f(x ⊓ --(g y))) ∧ g y ⊓ x ≤ --(g(y ⊓ --(f x))))"
proof (intro conjI)
show "f bot = bot"
using 1 by (metis conjugate_def inf_idem inf_bot_left)
next
show "g bot = bot"
using 1 by (metis conjugate_def inf_idem inf_bot_right)
next
show "∀x y . f x ⊓ y ≤ --(f(x ⊓ --(g y))) ∧ g y ⊓ x ≤ --(g(y ⊓ --(f x)))"
proof (intro allI)
fix x y
have 3: "y ≤ -(f(x ⊓ -(g y)))"
using 1 by (simp add: conjugate_def pseudo_complement inf_commute)
have 4: "x ≤ -(g(y ⊓ -(f x)))"
using 1 conjugate_def inf.commute pseudo_complement by fastforce
have "y ⊓ -(f(x ⊓ --(g y))) = y ⊓ -(f(x ⊓ -(g y))) ⊓ -(f(x ⊓ --(g y)))"
using 3 by (simp add: inf.le_iff_sup inf_commute)
also have "... = y ⊓ -(f((x ⊓ -(g y)) ⊔ (x ⊓ --(g y))))"
using 1 conjugate_dual_additive dual_additive_def inf_assoc by auto
also have "... = y ⊓ -(f x)"
by (simp add: maddux_3_11_pp)
also have "... ≤ -(f x)"
by simp
finally have 5: "f x ⊓ y ≤ --(f(x ⊓ --(g y)))"
by (simp add: inf_commute p_shunting_swap)
have "x ⊓ -(g(y ⊓ --(f x))) = x ⊓ -(g(y ⊓ -(f x))) ⊓ -(g(y ⊓ --(f x)))"
using 4 by (simp add: inf.le_iff_sup inf_commute)
also have "... = x ⊓ -(g((y ⊓ -(f x)) ⊔ (y ⊓ --(f x))))"
using 2 by (simp add: dual_additive_def inf_assoc)
also have "... = x ⊓ -(g y)"
by (simp add: maddux_3_11_pp)
also have "... ≤ -(g y)"
by simp
finally have "g y ⊓ x ≤ --(g(y ⊓ --(f x)))"
by (simp add: inf_commute p_shunting_swap)
thus "f x ⊓ y ≤ --(f(x ⊓ --(g y))) ∧ g y ⊓ x ≤ --(g(y ⊓ --(f x)))"
using 5 by simp
qed
qed
next
assume "f bot = bot ∧ g bot = bot ∧ (∀x y . f x ⊓ y ≤ --(f(x ⊓ --(g y))) ∧ g y ⊓ x ≤ --(g(y ⊓ --(f x))))"
thus "conjugate f g"
by (unfold conjugate_def, metis inf_commute le_bot pp_inf_bot_iff regular_closed_bot)
qed
lemma conjugate_char_2_pp_additive:
assumes "conjugate f g"
and "additive f"
and "additive g"
shows "f x ⊓ y ≤ f(x ⊓ --(g y)) ∧ g y ⊓ x ≤ g(y ⊓ --(f x))"
proof -
have "f x ⊓ y = f ((x ⊓ --g y) ⊔ (x ⊓ -g y)) ⊓ y"
by (simp add: sup.commute sup_inf_distrib1)
also have "... = (f (x ⊓ --g y) ⊓ y) ⊔ (f (x ⊓ -g y) ⊓ y)"
using assms(2) additive_def inf_sup_distrib2 by auto
also have "... = f (x ⊓ --g y) ⊓ y"
by (metis assms(1) conjugate_def inf_le2 pseudo_complement sup_bot.right_neutral)
finally have 2: "f x ⊓ y ≤ f (x ⊓ --g y)"
by simp
have "g y ⊓ x = g ((y ⊓ --f x) ⊔ (y ⊓ -f x)) ⊓ x"
by (simp add: sup.commute sup_inf_distrib1)
also have "... = (g (y ⊓ --f x) ⊓ x) ⊔ (g (y ⊓ -f x) ⊓ x)"
using assms(3) additive_def inf_sup_distrib2 by auto
also have "... = g (y ⊓ --f x) ⊓ x"
by (metis assms(1) conjugate_def inf.cobounded2 pseudo_complement sup_bot.right_neutral inf_commute)
finally have "g y ⊓ x ≤ g (y ⊓ --f x)"
by simp
thus ?thesis
using 2 by simp
qed
end
abbreviation stone_algebra_isomorphism :: "('a::stone_algebra ⇒ 'b::stone_algebra) ⇒ bool"
where "stone_algebra_isomorphism f ≡ sup_inf_top_bot_uminus_isomorphism f"
text ‹
Every bounded linear order can be expanded to a Stone algebra.
The pseudocomplement takes ‹bot› to the ‹top› and every other element to ‹bot›.
›
class linorder_stone_algebra_expansion = linorder_lattice_expansion + uminus +
assumes uminus_def [simp]: "-x = (if x = bot then top else bot)"
begin
subclass stone_algebra
apply unfold_locales
using bot_unique min_def top_le by auto
text ‹
The regular elements are the least and greatest elements.
All elements except the least element are dense.
›
lemma regular_bot_top:
"regular x ⟷ x = bot ∨ x = top"
by simp
lemma not_bot_dense:
"x ≠ bot ⟹ --x = top"
by simp
end
subsection ‹Heyting Algebras›
text ‹
In this section we add a relative pseudocomplement operation to semilattices and to lattices.
›
subsubsection ‹Heyting Semilattices›
text ‹
The pseudocomplement of an element ‹y› relative to an element ‹z› is the least element whose meet with ‹y› is below ‹z›.
This can be stated as a Galois connection.
Specialising ‹z = bot› gives (non-relative) pseudocomplements.
Many properties can already be shown if the underlying structure is just a semilattice.
›
class implies =
fixes implies :: "'a ⇒ 'a ⇒ 'a" (infixl ‹↝› 65)
class heyting_semilattice = semilattice_inf + implies +
assumes implies_galois: "x ⊓ y ≤ z ⟷ x ≤ y ↝ z"
begin
lemma implies_below_eq [simp]:
"y ⊓ (x ↝ y) = y"
using implies_galois inf.absorb_iff1 inf.cobounded1 by blast
lemma implies_increasing:
"x ≤ y ↝ x"
by (simp add: inf.orderI)
lemma implies_galois_swap:
"x ≤ y ↝ z ⟷ y ≤ x ↝ z"
by (metis implies_galois inf_commute)
lemma implies_galois_var:
"x ⊓ y ≤ z ⟷ y ≤ x ↝ z"
by (simp add: implies_galois_swap implies_galois)
lemma implies_galois_increasing:
"x ≤ y ↝ (x ⊓ y)"
using implies_galois by blast
lemma implies_galois_decreasing:
"(y ↝ x) ⊓ y ≤ x"
using implies_galois by blast
lemma implies_mp_below:
"x ⊓ (x ↝ y) ≤ y"
using implies_galois_decreasing inf_commute by auto
lemma implies_isotone:
"x ≤ y ⟹ z ↝ x ≤ z ↝ y"
using implies_galois order_trans by blast
lemma implies_antitone:
"x ≤ y ⟹ y ↝ z ≤ x ↝ z"
by (meson implies_galois_swap order_lesseq_imp)
lemma implies_isotone_inf:
"x ↝ (y ⊓ z) ≤ x ↝ y"
by (simp add: implies_isotone)
lemma implies_antitone_inf:
"x ↝ z ≤ (x ⊓ y) ↝ z"
by (simp add: implies_antitone)
lemma implies_curry:
"x ↝ (y ↝ z) = (x ⊓ y) ↝ z"
by (metis implies_galois_decreasing implies_galois inf_assoc order.antisym)
lemma implies_curry_flip:
"x ↝ (y ↝ z) = y ↝ (x ↝ z)"
by (simp add: implies_curry inf_commute)
lemma triple_implies [simp]:
"((x ↝ y) ↝ y) ↝ y = x ↝ y"
using implies_antitone implies_galois_swap order.eq_iff by auto
lemma implies_mp_eq [simp]:
"x ⊓ (x ↝ y) = x ⊓ y"
by (metis implies_below_eq implies_mp_below inf_left_commute inf.absorb2)
lemma implies_dist_implies:
"x ↝ (y ↝ z) ≤ (x ↝ y) ↝ (x ↝ z)"
using implies_curry implies_curry_flip by auto
lemma implies_import_inf [simp]:
"x ⊓ ((x ⊓ y) ↝ (x ↝ z)) = x ⊓ (y ↝ z)"
by (metis implies_curry implies_mp_eq inf_commute)
lemma implies_dist_inf:
"x ↝ (y ⊓ z) = (x ↝ y) ⊓ (x ↝ z)"
proof -
have "(x ↝ y) ⊓ (x ↝ z) ⊓ x ≤ y ⊓ z"
by (simp add: implies_galois)
hence "(x ↝ y) ⊓ (x ↝ z) ≤ x ↝ (y ⊓ z)"
using implies_galois by blast
thus ?thesis
by (simp add: implies_isotone order.eq_iff)
qed
lemma implies_itself_top:
"y ≤ x ↝ x"
by (simp add: implies_galois_swap implies_increasing)
lemma inf_implies_top:
"z ≤ (x ⊓ y) ↝ x"
using implies_galois_var le_infI1 by blast
lemma inf_inf_implies [simp]:
"z ⊓ ((x ⊓ y) ↝ x) = z"
by (simp add: inf_implies_top inf_absorb1)
lemma le_implies_top:
"x ≤ y ⟹ z ≤ x ↝ y"
using implies_antitone implies_itself_top order.trans by blast
lemma le_iff_le_implies:
"x ≤ y ⟷ x ≤ x ↝ y"
using implies_galois inf_idem by force
lemma implies_inf_isotone:
"x ↝ y ≤ (x ⊓ z) ↝ (y ⊓ z)"
by (metis implies_curry implies_galois_increasing implies_isotone)
lemma implies_transitive:
"(x ↝ y) ⊓ (y ↝ z) ≤ x ↝ z"
using implies_dist_implies implies_galois_var implies_increasing order_lesseq_imp by blast
lemma implies_inf_absorb [simp]:
"x ↝ (x ⊓ y) = x ↝ y"
using implies_dist_inf implies_itself_top inf.absorb_iff2 by auto
lemma implies_implies_absorb [simp]:
"x ↝ (x ↝ y) = x ↝ y"
by (simp add: implies_curry)
lemma implies_inf_identity:
"(x ↝ y) ⊓ y = y"
by (simp add: inf_commute)
lemma implies_itself_same:
"x ↝ x = y ↝ y"
by (simp add: le_implies_top order.eq_iff)
end
text ‹
The following class gives equational axioms for the relative pseudocomplement operation (inequalities can be written as equations).
›
class heyting_semilattice_eq = semilattice_inf + implies +
assumes implies_mp_below: "x ⊓ (x ↝ y) ≤ y"
and implies_galois_increasing: "x ≤ y ↝ (x ⊓ y)"
and implies_isotone_inf: "x ↝ (y ⊓ z) ≤ x ↝ y"
begin
subclass heyting_semilattice
apply unfold_locales
apply (rule iffI)
apply (metis implies_galois_increasing implies_isotone_inf inf.absorb2 order_lesseq_imp)
by (metis implies_mp_below inf_commute order_trans inf_mono order_refl)
end
text ‹
The following class allows us to explicitly give the pseudocomplement of an element relative to itself.
›
class bounded_heyting_semilattice = bounded_semilattice_inf_top + heyting_semilattice
begin
lemma implies_itself [simp]:
"x ↝ x = top"
using implies_galois inf_le2 top_le by blast
lemma implies_order:
"x ≤ y ⟷ x ↝ y = top"
by (metis implies_galois inf_top.left_neutral top_unique)
lemma inf_implies [simp]:
"(x ⊓ y) ↝ x = top"
using implies_order inf_le1 by blast
lemma top_implies [simp]:
"top ↝ x = x"
by (metis implies_mp_eq inf_top.left_neutral)
end
subsubsection ‹Heyting Lattices›
text ‹
We obtain further properties if the underlying structure is a lattice.
In particular, the lattice operations are automatically distributive in this case.
›
class heyting_lattice = lattice + heyting_semilattice
begin
lemma sup_distrib_inf_le:
"(x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ (y ⊓ z)"
proof -
have "x ⊔ z ≤ y ↝ (x ⊔ (y ⊓ z))"
using implies_galois_var implies_increasing sup.bounded_iff sup.cobounded2 by blast
hence "x ⊔ y ≤ (x ⊔ z) ↝ (x ⊔ (y ⊓ z))"
using implies_galois_swap implies_increasing le_sup_iff by blast
thus ?thesis
by (simp add: implies_galois)
qed
subclass distrib_lattice
apply unfold_locales
using distrib_sup_le order.eq_iff sup_distrib_inf_le by auto
lemma implies_isotone_sup:
"x ↝ y ≤ x ↝ (y ⊔ z)"
by (simp add: implies_isotone)
lemma implies_antitone_sup:
"(x ⊔ y) ↝ z ≤ x ↝ z"
by (simp add: implies_antitone)
lemma implies_sup:
"x ↝ z ≤ (y ↝ z) ↝ ((x ⊔ y) ↝ z)"
proof -
have "(x ↝ z) ⊓ (y ↝ z) ⊓ y ≤ z"
by (simp add: implies_galois)
hence "(x ↝ z) ⊓ (y ↝ z) ⊓ (x ⊔ y) ≤ z"
using implies_galois_swap implies_galois_var by fastforce
thus ?thesis
by (simp add: implies_galois)
qed
lemma implies_dist_sup:
"(x ⊔ y) ↝ z = (x ↝ z) ⊓ (y ↝ z)"
apply (rule order.antisym)
apply (simp add: implies_antitone)
by (simp add: implies_sup implies_galois)
lemma implies_antitone_isotone:
"(x ⊔ y) ↝ (x ⊓ y) ≤ x ↝ y"
by (simp add: implies_antitone_sup implies_dist_inf le_infI2)
lemma implies_antisymmetry:
"(x ↝ y) ⊓ (y ↝ x) = (x ⊔ y) ↝ (x ⊓ y)"
by (metis implies_dist_sup implies_inf_absorb inf.commute)
lemma sup_inf_implies [simp]:
"(x ⊔ y) ⊓ (x ↝ y) = y"
by (simp add: inf_sup_distrib2 sup.absorb2)
lemma implies_subdist_sup:
"(x ↝ y) ⊔ (x ↝ z) ≤ x ↝ (y ⊔ z)"
by (simp add: implies_isotone)
lemma implies_subdist_inf:
"(x ↝ z) ⊔ (y ↝ z) ≤ (x ⊓ y) ↝ z"
by (simp add: implies_antitone)
lemma implies_sup_absorb:
"(x ↝ y) ⊔ z ≤ (x ⊔ z) ↝ (y ⊔ z)"
by (metis implies_dist_sup implies_isotone_sup implies_increasing inf_inf_implies le_sup_iff sup_inf_implies)
lemma sup_below_implies_implies:
"x ⊔ y ≤ (x ↝ y) ↝ y"
by (simp add: implies_dist_sup implies_galois_swap implies_increasing)
end
class bounded_heyting_lattice = bounded_lattice + heyting_lattice
begin
subclass bounded_heyting_semilattice ..
lemma implies_bot [simp]:
"bot ↝ x = top"
using implies_galois top_unique by fastforce
end
subsubsection ‹Heyting Algebras›
text ‹
The pseudocomplement operation can be defined in Heyting algebras, but it is typically not part of their signature.
We add the definition as an axiom so that we can use the class hierarchy, for example, to inherit results from the class ‹pd_algebra›.
›
class heyting_algebra = bounded_heyting_lattice + uminus +
assumes uminus_eq: "-x = x ↝ bot"
begin
subclass pd_algebra
apply unfold_locales
using bot_unique implies_galois uminus_eq by auto
lemma boolean_implies_below:
"-x ⊔ y ≤ x ↝ y"
by (simp add: implies_increasing implies_isotone uminus_eq)
lemma negation_implies:
"-(x ↝ y) = --x ⊓ -y"
proof (rule order.antisym)
show "-(x ↝ y) ≤ --x ⊓ -y"
using boolean_implies_below p_antitone by auto
next
have "x ⊓ -y ⊓ (x ↝ y) = bot"
by (metis implies_mp_eq inf_p inf_bot_left inf_commute inf_left_commute)
hence "--x ⊓ -y ⊓ (x ↝ y) = bot"
using pp_inf_bot_iff inf_assoc by auto
thus "--x ⊓ -y ≤ -(x ↝ y)"
by (simp add: pseudo_complement)
qed
lemma double_negation_dist_implies:
"--(x ↝ y) = --x ↝ --y"
apply (rule order.antisym)
apply (metis pp_inf_below_iff implies_galois_decreasing implies_galois negation_implies ppp)
by (simp add: p_antitone_iff negation_implies)
end
text ‹
The following class gives equational axioms for Heyting algebras.
›
class heyting_algebra_eq = bounded_lattice + implies + uminus +
assumes implies_mp_eq: "x ⊓ (x ↝ y) = x ⊓ y"
and implies_import_inf: "x ⊓ ((x ⊓ y) ↝ (x ↝ z)) = x ⊓ (y ↝ z)"
and inf_inf_implies: "z ⊓ ((x ⊓ y) ↝ x) = z"
and uminus_eq_eq: "-x = x ↝ bot"
begin
subclass heyting_algebra
apply unfold_locales
apply (rule iffI)
apply (metis implies_import_inf inf.sup_left_divisibility inf_inf_implies le_iff_inf)
apply (metis implies_mp_eq inf.commute inf.le_sup_iff inf.sup_right_isotone)
by (simp add: uminus_eq_eq)
end
text ‹
A relative pseudocomplement is not enough to obtain the Stone equation, so we add it in the following class.
›
class heyting_stone_algebra = heyting_algebra +
assumes heyting_stone: "-x ⊔ --x = top"
begin
subclass stone_algebra
by unfold_locales (simp add: heyting_stone)
end
subsubsection ‹Brouwer Algebras›
text ‹
Brouwer algebras are dual to Heyting algebras.
The dual pseudocomplement of an element ‹y› relative to an element ‹x› is the least element whose join with ‹y› is above ‹x›.
We can now use the binary operation provided by Boolean algebras in Isabelle/HOL because it is compatible with dual relative pseudocomplements (not relative pseudocomplements).
›
class brouwer_algebra = bounded_lattice + minus + uminus +
assumes minus_galois: "x ≤ y ⊔ z ⟷ x - y ≤ z"
and uminus_eq_minus: "-x = top - x"
begin