Theory P_Algebras

(* Title:      Pseudocomplemented Algebras
Author:     Walter Guttmann
Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

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,Birkhoff1967,Blyth2005,Curry1977,Graetzer1971,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"

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"

lemma p_antitone_inf:
"-x ≤ -(x ⊓ y)"

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"

lemma pp_isotone_sup:
"--x ≤ --(x ⊔ y)"

lemma pp_isotone_inf:
"--(x ⊓ y) ≤ --x"

text ‹
One of De Morgan's laws holds in pseudocomplemented lattices.
›

lemma p_dist_sup [simp]:
"-(x ⊔ y) = -x ⊓ -y"
apply (rule order.antisym)
using inf_le1 inf_le2 le_sup_iff p_antitone_iff by blast

lemma p_supdist_inf:
"-x ⊔ -y ≤ -(x ⊓ y)"

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"

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"

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)"

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

"x ⊔ x = x ⊔ -(y ⊔ -y)"
by simp

lemma shunting_1_pp:
"x ≤ --y ⟷ x ⊓ -y = bot"

lemma pp_pp_inf_bot_iff:
"x ⊓ y = bot ⟷ --x ⊓ --y = bot"

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)"

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)"

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"

shows "isotone (uminus ∘ f)"
proof -
have "∀x y . f (x ⊔ y) ≤ f x"
hence "∀x y . x ≤ y ⟶ f y ≤ f x"
by (metis sup_absorb2)
hence "∀x y . x ≤ y ⟶ -(f x) ≤ -(f y)"
thus ?thesis
qed

assumes "conjugate f g"
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)"
also have "... = ((x ⊔ y) ⊓ g(-z) = bot)"
using assms conjugate_def by auto
also have "... = (x ⊔ y ≤ -(g(-z)))"
also have "... = (x ≤ -(g(-z)) ∧ y ≤ -(g(-z)))"
also have "... = (x ⊓ g(-z) = bot ∧ y ⊓ g(-z) = bot)"
also have "... = (f x ⊓ -z = bot ∧ f y ⊓ -z = bot)"
using assms conjugate_def by auto
also have "... = (-z ≤ -(f x) ∧ -z ≤ -(f y))"
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
qed

lemma conjugate_isotone_pp:
"conjugate f g ⟹ isotone (uminus ∘ uminus ∘ f)"

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))"
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))"
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"

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)

(*
lemma p_inf_sup_below: "-x ⊓ (x ⊔ y) ≤ y" nitpick [expect=genuine] oops
lemma complement_p: "x ⊓ y = bot ∧ x ⊔ y = top ⟶ -x = y" nitpick [expect=genuine] oops
lemma complemented_regular: "complemented x ⟶ regular x" nitpick [expect=genuine] oops
*)

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"

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)

"(x ⊔ -y) ⊓ (x ⊔ y) = x"
by (metis p_inf sup_bot_right sup_inf_distrib1)

"(x ⊔ y) ⊓ -x = y ⊓ -x"

"((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"
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))"
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)

(*
lemma pp_dist_sup [simp]: "--(x ⊔ y) = --x ⊔ --y" nitpick [expect=genuine] oops
lemma regular_closed_sup: "regular x ∧ regular y ⟶ regular (x ⊔ y)" nitpick [expect=genuine] oops
lemma regular_complemented_iff: "regular x ⟷ complemented x" nitpick [expect=genuine] oops
lemma selection_closed_sup: "selection s x ∧ selection t x ⟶ selection (s ⊔ t) x" nitpick [expect=genuine] oops
lemma stone [simp]: "-x ⊔ --x = top" nitpick [expect=genuine] oops
*)

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"
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"

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)

"-(x ⊔ y) ⊔ -(x ⊔ -y) = -x"

"(x ⊓ -y) ⊔ (x ⊓ --y) = x"
by (metis inf_sup_distrib1 inf_top_right stone)

"(-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
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)

"--x ⊔ (-x ⊓ y) = --x ⊔ y"

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)"
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"
qed

(* Whether conjugate_char_2_pp can be proved in pd_algebra or in p_algebra is unknown. *)
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)"
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))))"
also have "... = y ⊓ -(f x)"
also have "... ≤ -(f x)"
by simp
finally have 5: "f x ⊓ y ≤ --(f(x ⊓ --(g y)))"
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))))"
also have "... = x ⊓ -(g y)"
also have "... ≤ -(g y)"
by simp
finally have "g y ⊓ x ≤ --(g(y ⊓ --(f x)))"
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

assumes "conjugate f 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"
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"
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

(*
lemma compl_le_swap2_iff: "-x ≤ y ⟷ -y ≤ x" nitpick [expect=genuine] oops
lemma huntington_3: "x = -(-x ⊔ -y) ⊔ -(-x ⊔ y)" nitpick [expect=genuine] oops
lemma maddux_3_1: "x ⊔ -x = y ⊔ -y" nitpick [expect=genuine] oops
lemma maddux_3_4: "x ⊔ (y ⊔ -y) = z ⊔ -z" nitpick [expect=genuine] oops
lemma maddux_3_11: "x = (x ⊓ y) ⊔ (x ⊓ -y)" nitpick [expect=genuine] oops
lemma maddux_3_19: "(-x ⊓ y) ⊔ (x ⊓ z) = (x ⊔ y) ⊓ (-x ⊔ z)" nitpick [expect=genuine] oops
lemma compl_inter_eq: "x ⊓ y = x ⊓ z ∧ -x ⊓ y = -x ⊓ z ⟶ y = z" nitpick [expect=genuine] oops
lemma maddux_3_21: "x ⊔ y = x ⊔ (-x ⊓ y)" nitpick [expect=genuine] oops
lemma shunting_1: "x ≤ y ⟷ x ⊓ -y = bot" nitpick [expect=genuine] oops
lemma shunting_2: "x ≤ y ⟷ -x ⊔ y = top" nitpick [expect=genuine] oops
lemma conjugate_unique: "conjugate f g ∧ conjugate f h ⟶ g = h" nitpick [expect=genuine] oops
lemma conjugate_isotone_pp: "conjugate f g ⟶ isotone f" nitpick [expect=genuine] oops
lemma conjugate_char_1: "conjugate f g ⟷ (∀x y . f(x ⊓ -(g y)) ≤ f x ⊓ -y ∧ g(y ⊓ -(f x)) ≤ g y ⊓ -x)" nitpick [expect=genuine] oops
lemma conjugate_char_2: "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))" nitpick [expect=genuine] oops
lemma shunting: "x ⊓ y ≤ z ⟷ x ≤ z ⊔ -y" nitpick [expect=genuine] oops
lemma shunting_var: "x ⊓ -y ≤ z ⟷ x ≤ z ⊔ y" nitpick [expect=genuine] oops
lemma sup_compl_top: "x ⊔ -x = top" nitpick [expect=genuine] oops
lemma selection_closed_p: "selection s x ⟶ selection (-s) x" nitpick [expect=genuine] oops
lemma selection_closed_pp: "selection s x ⟶ selection (--s) x" nitpick [expect=genuine] oops
*)

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"

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"

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"

lemma implies_antitone_inf:
"x ↝ z ≤ (x ⊓ y) ↝ z"

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)"

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"
hence "(x ↝ y) ⊓ (x ↝ z) ≤ x ↝ (y ⊓ z)"
using implies_galois by blast
thus ?thesis
qed

lemma implies_itself_top:
"y ≤ x ↝ x"

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"

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"

lemma implies_inf_identity:
"(x ↝ y) ⊓ y = y"

lemma implies_itself_same:
"x ↝ x = y ↝ y"

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
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)"

lemma implies_antitone_sup:
"(x ⊔ y) ↝ z ≤ x ↝ z"

lemma implies_sup:
"x ↝ z ≤ (y ↝ z) ↝ ((x ⊔ y) ↝ z)"
proof -
have "(x ↝ z) ⊓ (y ↝ z) ⊓ y ≤ z"
hence "(x ↝ z) ⊓ (y ↝ z) ⊓ (x ⊔ y) ≤ z"
using implies_galois_swap implies_galois_var by fastforce
thus ?thesis
qed

lemma implies_dist_sup:
"(x ⊔ y) ↝ z = (x ↝ z) ⊓ (y ↝ z)"
apply (rule order.antisym)

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"

lemma implies_subdist_sup:
"(x ↝ y) ⊔ (x ↝ z) ≤ x ↝ (y ⊔ z)"

lemma implies_subdist_inf:
"(x ↝ z) ⊔ (y ↝ z) ≤ (x ⊓ y) ↝ z"

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)"
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)

(*
lemma stone: "-x ⊔ --x = top" nitpick [expect=genuine] oops
*)

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)

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

(*
lemma pre_linear: "(x ↝ y) ⊔ (y ↝ x) = top" nitpick [expect=genuine] oops
*)

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

sublocale brouwer: heyting_algebra where inf = sup and less_eq = greater_eq and less = greater and sup = inf and bot = top and top = bot and implies = "λx y . y - x"
apply unfold_locales
apply simp
apply simp
apply simp
apply simp
apply (metis minus_galois sup_commute)

lemma curry_minus:
"x - (y ⊔ z) = (x - y) - z"

lemma minus_subdist_sup:
"(x - z) ⊔ (y - z) ≤ (x ⊔ y) - z"

lemma inf_sup_minus:
"(x ⊓ y) ⊔ (x - y) = x"

end

subsection ‹Boolean Algebras›

text ‹
This section integrates Boolean algebras in the above hierarchy.
In particular, we strengthen several results shown above.
›

context boolean_algebra
begin

text ‹
Every Boolean algebra is a Stone algebra, a Heyting algebra and a Brouwer algebra.
›

subclass stone_algebra
apply unfold_locales
apply (rule iffI)
apply (metis compl_sup_top inf.orderI inf_bot_right inf_sup_distrib1 inf_top_right sup_inf_absorb)
using inf.commute inf.sup_right_divisibility apply fastforce
by simp

sublocale heyting: heyting_algebra where implies = "λx y . -x ⊔ y"
apply unfold_locales
apply (rule iffI)
using shunting_var_p sup_commute apply fastforce
using shunting_var_p sup_commute apply force
by simp

subclass brouwer_algebra
apply unfold_locales
apply (simp add: diff_eq shunting_var_p sup.commute)

lemma huntington_3 [simp]:
"-(-x ⊔ -y) ⊔ -(-x ⊔ y) = x"
using huntington_3_pp by auto

"x ⊔ -x = y ⊔ -y"
by simp

"x ⊔ (y ⊔ -y) = z ⊔ -z"
by simp

"(x ⊓ y) ⊔ (x ⊓ -y) = x"

"(-x ⊓ y) ⊔ (x ⊓ z) = (x ⊔ y) ⊓ (-x ⊔ z)"

lemma compl_inter_eq:
"x ⊓ y = x ⊓ z ⟹ -x ⊓ y = -x ⊓ z ⟹ y = z"

"x ⊔ (-x ⊓ y) = x ⊔ y"

lemma shunting_1:
"x ≤ y ⟷ x ⊓ -y = bot"

lemma uminus_involutive:
"uminus ∘ uminus = id"
by auto

lemma uminus_injective:
"uminus ∘ f = uminus ∘ g ⟹ f = g"
by (metis comp_assoc id_o minus_comp_minus)

lemma conjugate_unique:
"conjugate f g ⟹ conjugate f h ⟹ g = h"
using conjugate_unique_p uminus_injective by blast

"conjugate f g ⟹ additive f"

lemma conjugate_isotone:
"conjugate f g ⟹ isotone f"

lemma conjugate_char_1:
"conjugate f g ⟷ (∀x y . f(x ⊓ -(g y)) ≤ f x ⊓ -y ∧ g(y ⊓ -(f x)) ≤ g y ⊓ -x)"

lemma conjugate_char_2:
"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))"

lemma shunting:
"x ⊓ y ≤ z ⟷ x ≤ z ⊔ -y"

lemma shunting_var:
"x ⊓ -y ≤ z ⟷ x ≤ z ⊔ y"