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

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

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

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

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

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

(*
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)
  by (simp add: uminus_eq_minus)

lemma curry_minus:
  "x - (y ⊔ z) = (x - y) - z"
  by (simp add: brouwer.implies_curry sup_commute)

lemma minus_subdist_sup:
  "(x - z) ⊔ (y - z) ≤ (x ⊔ y) - z"
  by (simp add: brouwer.implies_dist_inf)

lemma inf_sup_minus:
  "(x ⊓ y) ⊔ (x - y) = x"
  by (simp add: inf.absorb1 brouwer.inf_sup_distrib2)

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)
  by (simp add: diff_eq)

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

lemma maddux_3_1:
  "x ⊔ -x = y ⊔ -y"
  by simp

lemma maddux_3_4:
  "x ⊔ (y ⊔ -y) = z ⊔ -z"
  by simp

lemma maddux_3_11 [simp]:
  "(x ⊓ y) ⊔ (x ⊓ -y) = x"
  using brouwer.maddux_3_12 sup.commute by auto

lemma maddux_3_19:
  "(-x ⊓ y) ⊔ (x ⊓ z) = (x ⊔ y) ⊓ (-x ⊔ z)"
  using maddux_3_19_pp by auto

lemma compl_inter_eq:
  "x ⊓ y = x ⊓ z ⟹ -x ⊓ y = -x ⊓ z ⟹ y = z"
  by (metis inf_commute maddux_3_11)

lemma maddux_3_21 [simp]:
  "x ⊔ (-x ⊓ y) = x ⊔ y"
  by (simp add: sup_inf_distrib1)

lemma shunting_1:
  "x ≤ y ⟷ x ⊓ -y = bot"
  by (simp add: pseudo_complement)

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

lemma dual_additive_additive:
  "dual_additive (uminus ∘ f) ⟹ additive f"
  by (metis additive_def compl_eq_compl_iff dual_additive_def p_dist_sup o_def)

lemma conjugate_additive:
  "conjugate f g ⟹ additive f"
  by (simp add: conjugate_dual_additive dual_additive_additive)

lemma conjugate_isotone:
  "conjugate f g ⟹ isotone f"
  by (simp add: conjugate_additive additive_isotone)

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

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))"
  by (simp add: conjugate_char_2_pp)

lemma shunting:
  "x ⊓ y ≤ z ⟷ x ≤ z ⊔ -y"
  by (simp add: heyting.implies_galois sup.commute)

lemma shunting_var:
  "x ⊓ -y ≤ z ⟷ x ≤ z ⊔ y"
  by (simp add: shunting)

end

class non_trivial_stone_algebra = non_trivial_bounded_order + stone_algebra

class non_trivial_boolean_algebra = non_trivial_stone_algebra + boolean_algebra

end