Session Stone_Algebras

Theory Lattice_Basics

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

section ‹Lattice Basics›

text ‹
This theory provides notations, basic definitions and facts of lattice-related structures used throughout the subsequent development.
›

theory Lattice_Basics

imports Main

begin

subsection ‹General Facts and Notations›

text ‹
The following results extend basic Isabelle/HOL facts.
›

lemma imp_as_conj:
  assumes "P x  Q x"
  shows "P x  Q x  P x"
  using assms by auto

lemma if_distrib_2:
  "f (if c then x else y) (if c then z else w) = (if c then f x z else f y w)"
  by simp

lemma left_invertible_inj:
  "(x . g (f x) = x)  inj f"
  by (metis injI)

lemma invertible_bij:
  assumes "x . g (f x) = x"
      and "y . f (g y) = y"
    shows "bij f"
  by (metis assms bijI')

lemma finite_ne_subset_induct [consumes 3, case_names singleton insert]:
  assumes "finite F"
      and "F  {}"
      and "F  S"
      and singleton: "x . P {x}"
      and insert: "x F . finite F  F  {}  F  S  x  S  x  F  P F  P (insert x F)"
    shows "P F"
  using assms(1-3)
  apply (induct rule: finite_ne_induct)
  apply (simp add: singleton)
  by (simp add: insert)

lemma finite_set_of_finite_funs_pred:
  assumes "finite { x::'a . True }"
      and "finite { y::'b . P y }"
    shows "finite { f . (x::'a . P (f x)) }"
  using assms finite_set_of_finite_funs by force

text ‹
We use the following notations for the join, meet and complement operations.
Changing the precedence of the unary complement allows us to write terms like --x› instead of -(-x)›.
›

context sup
begin

notation sup (infixl "" 65)

definition additive :: "('a  'a)  bool"
  where "additive f  x y . f (x  y) = f x  f y"

end

context inf
begin

notation inf (infixl "" 67)

end

context uminus
begin

no_notation uminus ("- _" [81] 80)

notation uminus ("- _" [80] 80)

end

subsection ‹Orders›

text ‹
We use the following definition of monotonicity for operations defined in classes.
The standard mono› places a sort constraint on the target type.
We also give basic properties of Galois connections and lift orders to functions.
›

context ord
begin

definition isotone :: "('a  'a)  bool"
  where "isotone f  x y . x  y  f x  f y"

definition galois :: "('a  'a)  ('a  'a)  bool"
  where "galois l u  x y . l x  y  x  u y"

definition lifted_less_eq :: "('a  'a)  ('a  'a)  bool" ("(_ ≤≤ _)" [51, 51] 50)
  where "f ≤≤ g  x . f x  g x"

end

context order
begin

lemma order_lesseq_imp:
  "(z . x  z  y  z)  y  x"
  using order_trans by blast

lemma galois_char:
  "galois l u  (x . x  u (l x))  (x . l (u x)  x)  isotone l  isotone u"
  apply (rule iffI)
  apply (metis (full_types) galois_def isotone_def order_refl order_trans)
  using galois_def isotone_def order_trans by blast

lemma galois_closure:
  "galois l u  l x = l (u (l x))  u x = u (l (u x))"
  by (simp add: galois_char isotone_def order.antisym)

lemma lifted_reflexive:
  "f = g  f ≤≤ g"
  by (simp add: lifted_less_eq_def)

lemma lifted_transitive:
  "f ≤≤ g  g ≤≤ h  f ≤≤ h"
  using lifted_less_eq_def order_trans by blast

lemma lifted_antisymmetric:
  "f ≤≤ g  g ≤≤ f  f = g"
  by (rule ext, rule order.antisym) (simp_all add: lifted_less_eq_def)

text ‹
If the image of a finite non-empty set under f› is a totally ordered, there is an element that minimises the value of f›.
›

lemma finite_set_minimal:
  assumes "finite s"
      and "s  {}"
      and "xs . ys . f x  f y  f y  f x"
    shows "ms . zs . f m  f z"
  apply (rule finite_ne_subset_induct[where S=s])
  apply (rule assms(1))
  apply (rule assms(2))
  apply simp
  apply simp
  by (metis assms(3) insert_iff order_trans subsetD)

end

subsection ‹Semilattices›

text ‹
The following are basic facts in semilattices.
›

context semilattice_sup
begin

lemma sup_left_isotone:
  "x  y  x  z  y  z"
  using sup.mono by blast

lemma sup_right_isotone:
  "x  y  z  x  z  y"
  using sup.mono by blast

lemma sup_left_divisibility:
  "x  y  (z . x  z = y)"
  using sup.absorb2 sup.cobounded1 by blast

lemma sup_right_divisibility:
  "x  y  (z . z  x = y)"
  by (metis sup.cobounded2 sup.orderE)

lemma sup_same_context:
  "x  y  z  y  x  z  x  z = y  z"
  by (simp add: le_iff_sup sup_left_commute)

lemma sup_relative_same_increasing:
  "x  y  x  z = x  w  y  z = y  w"
  using sup.assoc sup_right_divisibility by auto

end

text ‹
Every bounded semilattice is a commutative monoid.
Finite sums defined in commutative monoids are available via the following sublocale.
›

context bounded_semilattice_sup_bot
begin

sublocale sup_monoid: comm_monoid_add where plus = sup and zero = bot
  apply unfold_locales
  apply (simp add: sup_assoc)
  apply (simp add: sup_commute)
  by simp

end

context semilattice_inf
begin

lemma inf_same_context:
  "x  y  z  y  x  z  x  z = y  z"
  using order.antisym by auto

end

text ‹
The following class requires only the existence of upper bounds, which is a property common to bounded semilattices and (not necessarily bounded) lattices.
We use it in our development of filters.
›

class directed_semilattice_inf = semilattice_inf +
  assumes ub: "z . x  z  y  z"

text ‹
We extend the inf› sublocale, which dualises the order in semilattices, to bounded semilattices.
›

context bounded_semilattice_inf_top
begin

subclass directed_semilattice_inf
  apply unfold_locales
  using top_greatest by blast

sublocale inf: bounded_semilattice_sup_bot where sup = inf and less_eq = greater_eq and less = greater and bot = top
  by unfold_locales (simp_all add: less_le_not_le)

end

subsection ‹Lattices›

context lattice
begin

subclass directed_semilattice_inf
  apply unfold_locales
  using sup_ge1 sup_ge2 by blast

definition dual_additive :: "('a  'a)  bool"
  where "dual_additive f  x y . f (x  y) = f x  f y"

end

text ‹
Not every bounded lattice has complements, but two elements might still be complements of each other as captured in the following definition.
In this situation we can apply, for example, the shunting property shown below.
We introduce most definitions using the abbreviation› command.
›

context bounded_lattice
begin

abbreviation "complement x y  x  y = top  x  y = bot"

lemma complement_symmetric:
  "complement x y  complement y x"
  by (simp add: inf.commute sup.commute)

definition conjugate :: "('a  'a)  ('a  'a)  bool"
  where "conjugate f g  x y . f x  y = bot  x  g y = bot"

end

class dense_lattice = bounded_lattice +
  assumes bot_meet_irreducible: "x  y = bot  x = bot  y = bot"

context distrib_lattice
begin

lemma relative_equality:
  "x  z = y  z  x  z = y  z  x = y"
  by (metis inf.commute inf_sup_absorb inf_sup_distrib2)

end

text ‹
Distributive lattices with a greatest element are widely used in the construction theorem for Stone algebras.
›

class distrib_lattice_bot = bounded_lattice_bot + distrib_lattice

class distrib_lattice_top = bounded_lattice_top + distrib_lattice

class bounded_distrib_lattice = bounded_lattice + distrib_lattice
begin

subclass distrib_lattice_bot ..

subclass distrib_lattice_top ..

lemma complement_shunting:
  assumes "complement z w"
    shows "z  x  y  x  w  y"
proof
  assume 1: "z  x  y"
  have "x = (z  w)  x"
    by (simp add: assms)
  also have "...  y  (w  x)"
    using 1 sup.commute sup.left_commute inf_sup_distrib2 sup_right_divisibility by fastforce
  also have "...  w  y"
    by (simp add: inf.coboundedI1)
  finally show "x  w  y"
    .
next
  assume "x  w  y"
  hence "z  x  z  (w  y)"
    using inf.sup_right_isotone by auto
  also have "... = z  y"
    by (simp add: assms inf_sup_distrib1)
  also have "...  y"
    by simp
  finally show "z  x  y"
    .
qed

end

subsection ‹Linear Orders›

text ‹
We next consider lattices with a linear order structure.
In such lattices, join and meet are selective operations, which give the maximum and the minimum of two elements, respectively.
Moreover, the lattice is automatically distributive.
›

class bounded_linorder = linorder + order_bot + order_top

class linear_lattice = lattice + linorder
begin

lemma max_sup:
  "max x y = x  y"
  by (metis max.boundedI max.cobounded1 max.cobounded2 sup_unique)

lemma min_inf:
  "min x y = x  y"
  by (simp add: inf.absorb1 inf.absorb2 min_def)

lemma sup_inf_selective:
  "(x  y = x  x  y = y)  (x  y = y  x  y = x)"
  by (meson inf.absorb1 inf.absorb2 le_cases sup.absorb1 sup.absorb2)

lemma sup_selective:
  "x  y = x  x  y = y"
  using sup_inf_selective by blast

lemma inf_selective:
  "x  y = x  x  y = y"
  using sup_inf_selective by blast

subclass distrib_lattice
  apply standard
  apply (rule order.antisym)
   apply (auto simp add: le_supI2)
  apply (metis inf_selective inf.coboundedI1 inf.coboundedI2 order.eq_iff)
  done

lemma sup_less_eq:
  "x  y  z  x  y  x  z"
  by (metis le_supI1 le_supI2 sup_selective)

lemma inf_less_eq:
  "x  y  z  x  z  y  z"
  by (metis inf.coboundedI1 inf.coboundedI2 inf_selective)

lemma sup_inf_sup:
  "x  y = (x  y)  (x  y)"
  by (metis sup_commute sup_inf_absorb sup_left_commute)

end

text ‹
The following class derives additional properties if the linear order of the lattice has a least and a greatest element.
›

class linear_bounded_lattice = bounded_lattice + linorder
begin

subclass linear_lattice ..

subclass bounded_linorder ..

subclass bounded_distrib_lattice ..

lemma sup_dense:
  "x  top  y  top  x  y  top"
  by (metis sup_selective)

lemma inf_dense:
  "x  bot  y  bot  x  y  bot"
  by (metis inf_selective)

lemma sup_not_bot:
  "x  bot  x  y  bot"
  by simp

lemma inf_not_top:
  "x  top  x  y  top"
  by simp

subclass dense_lattice
  apply unfold_locales
  using inf_dense by blast

end

text ‹
Every bounded linear order can be expanded to a bounded lattice.
Join and meet are maximum and minimum, respectively.
›

class linorder_lattice_expansion = bounded_linorder + sup + inf +
  assumes sup_def [simp]: "x  y = max x y"
  assumes inf_def [simp]: "x  y = min x y"
begin

subclass linear_bounded_lattice
  apply unfold_locales
  by auto

end

subsection ‹Non-trivial Algebras›

text ‹
Some results, such as the existence of certain filters, require that the algebras are not trivial.
This is not an assumption of the order and lattice classes that come with Isabelle/HOL; for example, bot = top› may hold in bounded lattices.
›

class non_trivial =
  assumes consistent: "x y . x  y"

class non_trivial_order = non_trivial + order

class non_trivial_order_bot = non_trivial_order + order_bot

class non_trivial_bounded_order = non_trivial_order_bot + order_top
begin

lemma bot_not_top:
  "bot  top"
proof -
  from consistent obtain x y :: 'a where "x  y"
    by auto
  thus ?thesis
    by (metis bot_less top.extremum_strict)
qed

end

subsection ‹Homomorphisms›

text ‹
This section gives definitions of lattice homomorphisms and isomorphisms and basic properties.
›

class sup_inf_top_bot_uminus = sup + inf + top + bot + uminus
class sup_inf_top_bot_uminus_ord = sup_inf_top_bot_uminus + ord

context boolean_algebra
begin

subclass sup_inf_top_bot_uminus_ord .

end

abbreviation sup_homomorphism :: "('a::sup  'b::sup)  bool"
  where "sup_homomorphism f  x y . f (x  y) = f x  f y"

abbreviation inf_homomorphism :: "('a::inf  'b::inf)  bool"
  where "inf_homomorphism f  x y . f (x  y) = f x  f y"

abbreviation bot_homomorphism :: "('a::bot  'b::bot)  bool"
  where "bot_homomorphism f  f bot = bot"

abbreviation top_homomorphism :: "('a::top  'b::top)  bool"
  where "top_homomorphism f  f top = top"

abbreviation minus_homomorphism :: "('a::minus  'b::minus)  bool"
  where "minus_homomorphism f  x y . f (x - y) = f x - f y"

abbreviation uminus_homomorphism :: "('a::uminus  'b::uminus)  bool"
  where "uminus_homomorphism f  x . f (-x) = -f x"

abbreviation sup_inf_homomorphism :: "('a::{sup,inf}  'b::{sup,inf})  bool"
  where "sup_inf_homomorphism f  sup_homomorphism f  inf_homomorphism f"

abbreviation sup_inf_top_homomorphism :: "('a::{sup,inf,top}  'b::{sup,inf,top})  bool"
  where "sup_inf_top_homomorphism f  sup_inf_homomorphism f  top_homomorphism f"

abbreviation sup_inf_top_bot_homomorphism :: "('a::{sup,inf,top,bot}  'b::{sup,inf,top,bot})  bool"
  where "sup_inf_top_bot_homomorphism f  sup_inf_top_homomorphism f  bot_homomorphism f"

abbreviation bounded_lattice_homomorphism :: "('a::bounded_lattice  'b::bounded_lattice)  bool"
  where "bounded_lattice_homomorphism f  sup_inf_top_bot_homomorphism f"

abbreviation sup_inf_top_bot_uminus_homomorphism :: "('a::sup_inf_top_bot_uminus  'b::sup_inf_top_bot_uminus)  bool"
  where "sup_inf_top_bot_uminus_homomorphism f  sup_inf_top_bot_homomorphism f  uminus_homomorphism f"

abbreviation sup_inf_top_bot_uminus_ord_homomorphism :: "('a::sup_inf_top_bot_uminus_ord  'b::sup_inf_top_bot_uminus_ord)  bool"
  where "sup_inf_top_bot_uminus_ord_homomorphism f  sup_inf_top_bot_uminus_homomorphism f  (x y . x  y  f x  f y)"

abbreviation sup_inf_top_isomorphism :: "('a::{sup,inf,top}  'b::{sup,inf,top})  bool"
  where "sup_inf_top_isomorphism f  sup_inf_top_homomorphism f  bij f"

abbreviation bounded_lattice_top_isomorphism :: "('a::bounded_lattice_top  'b::bounded_lattice_top)  bool"
  where "bounded_lattice_top_isomorphism f  sup_inf_top_isomorphism f"

abbreviation sup_inf_top_bot_uminus_isomorphism :: "('a::sup_inf_top_bot_uminus  'b::sup_inf_top_bot_uminus)  bool"
  where "sup_inf_top_bot_uminus_isomorphism f  sup_inf_top_bot_uminus_homomorphism f  bij f"

abbreviation boolean_algebra_isomorphism :: "('a::boolean_algebra  'b::boolean_algebra)  bool"
  where "boolean_algebra_isomorphism f  sup_inf_top_bot_uminus_isomorphism f  minus_homomorphism f"

lemma sup_homomorphism_mono:
  "sup_homomorphism (f::'a::semilattice_sup  'b::semilattice_sup)  mono f"
  by (metis le_iff_sup monoI)

lemma sup_isomorphism_ord_isomorphism:
  assumes "sup_homomorphism (f::'a::semilattice_sup  'b::semilattice_sup)"
      and "bij f"
    shows "x  y  f x  f y"
proof
  assume "x  y"
  thus "f x  f y"
    by (metis assms(1) le_iff_sup)
next
  assume "f x  f y"
  hence "f (x  y) = f y"
    by (simp add: assms(1) le_iff_sup)
  hence "x  y = y"
    by (metis injD bij_is_inj assms(2))
  thus "x  y"
    by (simp add: le_iff_sup)
qed

lemma minus_homomorphism_default:
  assumes "x y::'a::{inf,minus,uminus} . x - y = x  -y"
      and "x y::'b::{inf,minus,uminus} . x - y = x  -y"
      and "inf_homomorphism (f::'a  'b)"
      and "uminus_homomorphism f"
    shows "minus_homomorphism f"
  by (simp add: assms)

end

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

Theory Filters

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

section ‹Filters›

text ‹
This theory develops filters based on orders, semilattices, lattices and distributive lattices.
We prove the ultrafilter lemma for orders with a least element.
We show the following structure theorems:
\begin{itemize}
\item The set of filters over a directed semilattice forms a lattice with a greatest element.
\item The set of filters over a bounded semilattice forms a bounded lattice.
\item The set of filters over a distributive lattice with a greatest element forms a bounded distributive lattice.
\end{itemize}
Another result is that in a distributive lattice ultrafilters are prime filters.
We also prove a lemma of Gr\"atzer and Schmidt about principal filters.

We apply these results in proving the construction theorem for Stone algebras (described in a separate theory).
See, for example, \cite{BalbesDwinger1974,Birkhoff1967,Blyth2005,DaveyPriestley2002,Graetzer1971} for further results about filters.
›

theory Filters

imports Lattice_Basics

begin

subsection ‹Orders›

text ‹
This section gives the basic definitions related to filters in terms of orders.
The main result is the ultrafilter lemma.
›

context ord
begin

abbreviation down :: "'a  'a set" ("_" [81] 80)
  where "x  { y . y  x }"

abbreviation down_set :: "'a set  'a set" ("_" [81] 80)
  where "X  { y . xX . y  x }"

abbreviation is_down_set :: "'a set  bool"
  where "is_down_set X  xX . y . y  x  yX"

abbreviation is_principal_down :: "'a set  bool"
  where "is_principal_down X  x . X = x"

abbreviation up :: "'a  'a set" ("_" [81] 80)
  where "x  { y . x  y }"

abbreviation up_set :: "'a set  'a set" ("_" [81] 80)
  where "X  { y . xX . x  y }"

abbreviation is_up_set :: "'a set  bool"
  where "is_up_set X  xX . y . x  y  yX"

abbreviation is_principal_up :: "'a set  bool"
  where "is_principal_up X  x . X = x"

text ‹
A filter is a non-empty, downward directed, up-closed set.
›

definition filter :: "'a set  bool"
  where "filter F  (F  {})  (xF . yF . zF . z  x  z  y)  is_up_set F"

abbreviation proper_filter :: "'a set  bool"
  where "proper_filter F  filter F  F  UNIV"

abbreviation ultra_filter :: "'a set  bool"
  where "ultra_filter F  proper_filter F  (G . proper_filter G  F  G  F = G)"

abbreviation filters :: "'a set set"
  where "filters  { F::'a set . filter F }"

lemma filter_map_filter:
  assumes "filter F"
      and "mono f"
      and "x y . f x  y  (z . x  z  y = f z)"
    shows "filter (f ` F)"
proof (unfold ord_class.filter_def, intro conjI)
  show "f ` F  {}"
    using assms(1) ord_class.filter_def by auto
next
  show "xf ` F . yf ` F . zf ` F . z  x  z  y"
  proof (intro ballI)
    fix x y
    assume "x  f ` F" and "y  f ` F"
    then obtain u v where 1: "x = f u  u  F  y = f v  v  F"
      by auto
    then obtain w where "w  u  w  v  w  F"
      by (meson assms(1) ord_class.filter_def)
    thus "zf ` F . z  x  z  y"
      using 1 assms(2) mono_def image_eqI by blast
  qed
next
  show "is_up_set (f ` F)"
  proof
    fix x
    assume "x  f ` F"
    then obtain u where 1: "x = f u  u  F"
      by auto
    show "y . x  y  y  f ` F"
    proof (rule allI, rule impI)
      fix y
      assume "x  y"
      hence "f u  y"
        using 1 by simp
      then obtain z where "u  z  y = f z"
        using assms(3) by auto
      thus "y  f ` F"
        by (meson 1 assms(1) image_iff ord_class.filter_def)
    qed
  qed
qed

end

context order
begin

lemma self_in_downset [simp]:
  "x  x"
  by simp

lemma self_in_upset [simp]:
  "x  x"
  by simp

lemma up_filter [simp]:
  "filter (x)"
  using filter_def order_lesseq_imp by auto

lemma up_set_up_set [simp]:
  "is_up_set (X)"
  using order.trans by fastforce

lemma up_injective:
  "x = y  x = y"
  using order.antisym by auto

lemma up_antitone:
  "x  y  y  x"
  by auto

end

context order_bot
begin

lemma bot_in_downset [simp]:
  "bot  x"
  by simp

lemma down_bot [simp]:
  "bot = {bot}"
  by (simp add: bot_unique)

lemma up_bot [simp]:
  "bot = UNIV"
  by simp

text ‹
The following result is the ultrafilter lemma, generalised from \cite[10.17]{DaveyPriestley2002} to orders with a least element.
Its proof uses Isabelle/HOL's Zorn_Lemma›, which requires closure under union of arbitrary (possibly empty) chains.
Actually, the proof does not use any of the underlying order properties except bot_least›.
›

lemma ultra_filter:
  assumes "proper_filter F"
    shows "G . ultra_filter G  F  G"
proof -
  let ?A = "{ G . (proper_filter G  F  G)  G = {} }"
  have "C  chains ?A . C  ?A"
  proof
    fix C :: "'a set set"
    let ?D = "C - {{}}"
    assume 1: "C  chains ?A"
    hence 2: "x?D . H?D . x  H  proper_filter H"
      using chainsD2 by fastforce
    have 3: "?D = C"
      by blast
    have "?D  ?A"
    proof (cases "?D = {}")
      assume "?D = {}"
      thus ?thesis
        by auto
    next
      assume 4: "?D  {}"
      then obtain G where "G  ?D"
        by auto
      hence 5: "F  ?D"
        using 1 chainsD2 by blast
      have 6: "is_up_set (?D)"
      proof
        fix x
        assume "x  ?D"
        then obtain H where "x  H  H  ?D  filter H"
          using 2 by auto
        thus "y . x  y  y?D"
          using filter_def UnionI by fastforce
      qed
      have 7: "?D  UNIV"
      proof (rule ccontr)
        assume "¬ ?D  UNIV"
        then obtain H where "bot  H  proper_filter H"
          using 2 by blast
        thus False
          by (meson UNIV_I bot_least filter_def subsetI subset_antisym)
      qed
      {
        fix x y
        assume "x?D  y?D"
        then obtain H I where 8: "x  H  H  ?D  filter H  y  I  I  ?D  filter I"
          using 2 by metis
        have "z?D . z  x  z  y"
        proof (cases "H  I")
          assume "H  I"
          hence "zI . z  x  z  y"
            using 8 by (metis subsetCE filter_def)
          thus ?thesis
            using 8 by (metis UnionI)
        next
          assume "¬ (H  I)"
          hence "I  H"
            using 1 8 by (meson DiffE chainsD)
          hence "zH . z  x  z  y"
            using 8 by (metis subsetCE filter_def)
          thus ?thesis
            using 8 by (metis UnionI)
        qed
      }
      thus ?thesis
        using 4 5 6 7 filter_def by auto
    qed
    thus "C  ?A"
      using 3 by simp
  qed
  hence "M?A . X?A . M  X  X = M"
    by (rule Zorn_Lemma)
  then obtain M where 9: "M  ?A  (X?A . M  X  X = M)"
    by auto
  hence 10: "M  {}"
    using assms filter_def by auto
  {
    fix G
    assume 11: "proper_filter G  M  G"
    hence "F  G"
      using 9 10 by blast
    hence "M = G"
      using 9 11 by auto
  }
  thus ?thesis
    using 9 10 by blast
qed

end

context order_top
begin

lemma down_top [simp]:
  "top = UNIV"
  by simp

lemma top_in_upset [simp]:
  "top  x"
  by simp

lemma up_top [simp]:
  "top = {top}"
  by (simp add: top_unique)

lemma filter_top [simp]:
  "filter {top}"
  using filter_def top_unique by auto

lemma top_in_filter [simp]:
  "filter F  top  F"
  using filter_def by fastforce

end

text ‹
The existence of proper filters and ultrafilters requires that the underlying order contains at least two elements.
›

context non_trivial_order
begin

lemma proper_filter_exists:
  "F . proper_filter F"
proof -
  from consistent obtain x y :: 'a where "x  y"
    by auto
  hence "x  UNIV  y  UNIV"
    using order.antisym by blast
  hence "proper_filter (x)  proper_filter (y)"
    by simp
  thus ?thesis
    by blast
qed

end

context non_trivial_order_bot
begin

lemma ultra_filter_exists:
  "F . ultra_filter F"
  using ultra_filter proper_filter_exists by blast

end

context non_trivial_bounded_order
begin

lemma proper_filter_top:
  "proper_filter {top}"
  using bot_not_top filter_top by blast

lemma ultra_filter_top:
  "G . ultra_filter G  top  G"
  using ultra_filter proper_filter_top by fastforce

end

subsection ‹Lattices›

text ‹
This section develops the lattice structure of filters based on a semilattice structure of the underlying order.
The main results are that filters over a directed semilattice form a lattice with a greatest element and that filters over a bounded semilattice form a bounded lattice.
›

context semilattice_sup
begin

abbreviation prime_filter :: "'a set  bool"
  where "prime_filter F  proper_filter F  (x y . x  y  F  x  F  y  F)"

end

context semilattice_inf
begin

lemma filter_inf_closed:
  "filter F  x  F  y  F  x  y  F"
  by (meson filter_def inf.boundedI)

lemma filter_univ:
  "filter UNIV"
  by (meson UNIV_I UNIV_not_empty filter_def inf.cobounded1 inf.cobounded2)

text ‹
The operation filter_sup› is the join operation in the lattice of filters.
›

definition "filter_sup F G  { z . xF . yG . x  y  z }"

lemma filter_sup:
  assumes "filter F"
      and "filter G"
    shows "filter (filter_sup F G)"
proof -
  have "F  {}  G  {}"
    using assms filter_def by blast
  hence 1: "filter_sup F G  {}"
    using filter_sup_def by blast
  have 2: "xfilter_sup F G . yfilter_sup F G . zfilter_sup F G . z  x  z  y"
  proof
    fix x
    assume "xfilter_sup F G"
    then obtain t u where 3: "t  F  u  G  t  u  x"
      using filter_sup_def by auto
    show "yfilter_sup F G . zfilter_sup F G . z  x  z  y"
    proof
      fix y
      assume "yfilter_sup F G"
      then obtain v w where 4: "v  F  w  G  v  w  y"
        using filter_sup_def by auto
      let ?z = "(t  v)  (u  w)"
      have 5: "?z  x  ?z  y"
        using 3 4 by (meson order.trans inf.cobounded1 inf.cobounded2 inf_mono)
      have "?z  filter_sup F G"
        unfolding filter_sup_def using assms 3 4 filter_inf_closed by blast
      thus "zfilter_sup F G . z  x  z  y"
        using 5 by blast
    qed
  qed
  have "xfilter_sup F G . y . x  y  y  filter_sup F G"
    unfolding filter_sup_def using order_trans by blast
  thus ?thesis
    using 1 2 filter_def by presburger
qed

lemma filter_sup_left_upper_bound:
  assumes "filter G"
    shows "F  filter_sup F G"
proof -
  from assms obtain y where "yG"
    using all_not_in_conv filter_def by auto
  thus ?thesis
    unfolding filter_sup_def using inf.cobounded1 by blast
qed

lemma filter_sup_symmetric:
  "filter_sup F G = filter_sup G F"
  unfolding filter_sup_def using inf.commute by fastforce

lemma filter_sup_right_upper_bound:
  "filter F  G  filter_sup F G"
  using filter_sup_symmetric filter_sup_left_upper_bound by simp

lemma filter_sup_least_upper_bound:
  assumes "filter H"
      and "F  H"
      and "G  H"
    shows "filter_sup F G  H"
proof
  fix x
  assume "x  filter_sup F G"
  then obtain y z where 1: "y  F  z  G  y  z  x"
    using filter_sup_def by auto
  hence "y  H  z  H"
    using assms(2-3) by auto
  hence "y  z  H"
    by (simp add: assms(1) filter_inf_closed)
  thus "x  H"
    using 1 assms(1) filter_def by auto
qed

lemma filter_sup_left_isotone:
  "G  H  filter_sup G F  filter_sup H F"
  unfolding filter_sup_def by blast

lemma filter_sup_right_isotone:
  "G  H  filter_sup F G  filter_sup F H"
  unfolding filter_sup_def by blast

lemma filter_sup_right_isotone_var:
  "filter_sup F (G  H)  filter_sup F H"
  unfolding filter_sup_def by blast

lemma up_dist_inf:
  "(x  y) = filter_sup (x) (y)"
proof
  show "(x  y)  filter_sup (x) (y)"
    unfolding filter_sup_def by blast
next
  show "filter_sup (x) (y)  (x  y)"
  proof
    fix z
    assume "z  filter_sup (x) (y)"
    then obtain u v where "ux  vy  u  v  z"
      using filter_sup_def by auto
    hence "x  y  z"
      using order.trans inf_mono by blast
    thus "z  (x  y)"
      by blast
  qed
qed

text ‹
The following result is part of \cite[Exercise 2.23]{DaveyPriestley2002}.
›

lemma filter_inf_filter [simp]:
  assumes "filter F"
    shows "filter ({ y . zF . x  z = y})"
proof -
  let ?G = "{ y . zF . x  z = y}"
  have "F  {}"
    using assms filter_def by simp
  hence 1: "?G  {}"
    by blast
  have 2: "is_up_set ?G"
    by auto
  {
    fix y z
    assume "y  ?G  z  ?G"
    then obtain v w where "v  F  w  F  x  v  y  x  w  z"
      by auto
    hence "v  w  F  x  (v  w)  y  z"
      by (meson assms filter_inf_closed order.trans inf.boundedI inf.cobounded1 inf.cobounded2)
    hence "u?G . u  y  u  z"
      by auto
  }
  hence "x?G . y?G . z?G . z  x  z  y"
    by auto
  thus ?thesis
    using 1 2 filter_def by presburger
qed

end

context directed_semilattice_inf
begin

text ‹
Set intersection is the meet operation in the lattice of filters.
›

lemma filter_inf:
  assumes "filter F"
      and "filter G"
    shows "filter (F  G)"
proof (unfold filter_def, intro conjI)
  from assms obtain x y where 1: "xF  yG"
    using all_not_in_conv filter_def by auto
  from ub obtain z where "x  z  y  z"
    by auto
  hence "z  F  G"
    using 1 by (meson assms Int_iff filter_def)
  thus "F  G  {}"
    by blast
next
  show "is_up_set (F  G)"
    by (meson assms Int_iff filter_def)
next
  show "xF  G . yF  G . zF  G . z  x  z  y"
    by (metis assms Int_iff filter_inf_closed inf.cobounded2 inf.commute)
qed

end

text ‹
We introduce the following type of filters to instantiate the lattice classes and thereby inherit the results shown about lattices.
›

typedef (overloaded) 'a filter = "{ F::'a::order set . filter F }"
  by (meson mem_Collect_eq up_filter)

lemma simp_filter [simp]:
  "filter (Rep_filter x)"
  using Rep_filter by simp

setup_lifting type_definition_filter

text ‹
The set of filters over a directed semilattice forms a lattice with a greatest element.
›

instantiation filter :: (directed_semilattice_inf) bounded_lattice_top
begin

lift_definition top_filter :: "'a filter" is UNIV
  by (simp add: filter_univ)

lift_definition sup_filter :: "'a filter  'a filter  'a filter" is filter_sup
  by (simp add: filter_sup)

lift_definition inf_filter :: "'a filter  'a filter  'a filter" is inter
  by (simp add: filter_inf)

lift_definition less_eq_filter :: "'a filter  'a filter  bool" is subset_eq .

lift_definition less_filter :: "'a filter  'a filter  bool" is subset .

instance
  apply intro_classes
  subgoal apply transfer by (simp add: less_le_not_le)
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by (simp add: filter_sup_left_upper_bound)
  subgoal apply transfer by (simp add: filter_sup_right_upper_bound)
  subgoal apply transfer by (simp add: filter_sup_least_upper_bound)
  subgoal apply transfer by simp
  done

end

context bounded_semilattice_inf_top
begin

abbreviation "filter_complements F G  filter F  filter G  filter_sup F G = UNIV  F  G = {top}"

end

text ‹
The set of filters over a bounded semilattice forms a bounded lattice.
›

instantiation filter :: (bounded_semilattice_inf_top) bounded_lattice
begin

lift_definition bot_filter :: "'a filter" is "{top}"
  by simp

instance
  apply intro_classes
  apply transfer
  by simp

end

context lattice
begin

lemma up_dist_sup:
  "(x  y) = x  y"
  by auto

end

text ‹
For convenience, the following function injects principal filters into the filter type.
We cannot define it in the order› class since the type filter requires the sort constraint order› that is not available in the class.
The result of the function is a filter by lemma up_filter›.
›

abbreviation up_filter :: "'a::order  'a filter"
  where "up_filter x  Abs_filter (x)"

lemma up_filter_dist_inf:
  "up_filter ((x::'a::lattice)  y) = up_filter x  up_filter y"
  by (simp add: eq_onp_def sup_filter.abs_eq up_dist_inf)

lemma up_filter_dist_sup:
  "up_filter ((x::'a::lattice)  y) = up_filter x  up_filter y"
  by (metis eq_onp_def inf_filter.abs_eq up_dist_sup up_filter)

lemma up_filter_injective:
  "up_filter x = up_filter y  x = y"
  by (metis Abs_filter_inject mem_Collect_eq up_filter up_injective)

lemma up_filter_antitone:
  "x  y  up_filter y  up_filter x"
  by (metis eq_onp_same_args less_eq_filter.abs_eq up_antitone up_filter)

text ‹
The following definition applies a function to each element of a filter.
The subsequent lemma gives conditions under which the result of this application is a filter.
›

abbreviation filter_map :: "('a::order  'b::order)  'a filter  'b filter"
  where "filter_map f F  Abs_filter (f ` Rep_filter F)"

lemma filter_map_filter:
  assumes "mono f"
      and "x y . f x  y  (z . x  z  y = f z)"
    shows "filter (f ` Rep_filter F)"
  by (simp add: assms inf.filter_map_filter)

subsection ‹Distributive Lattices›

text ‹
In this section we additionally assume that the underlying order forms a distributive lattice.
Then filters form a bounded distributive lattice if the underlying order has a greatest element.
Moreover ultrafilters are prime filters.
We also prove a lemma of Gr\"atzer and Schmidt about principal filters.
›

context distrib_lattice
begin

lemma filter_sup_left_dist_inf:
  assumes "filter F"
      and "filter G"
      and "filter H"
    shows "filter_sup F (G  H) = filter_sup F G  filter_sup F H"
proof
  show "filter_sup F (G  H)  filter_sup F G  filter_sup F H"
    unfolding filter_sup_def using filter_sup_right_isotone_var by blast
next
  show "filter_sup F G  filter_sup F H  filter_sup F (G  H)"
  proof
    fix x
    assume "x  filter_sup F G  filter_sup F H"
    then obtain t u v w where 1: "t  F  u  G  v  F  w  H  t  u  x  v  w  x"
      using filter_sup_def by auto
    let ?y = "t  v"
    let ?z = "u  w"
    have 2: "?y  F"
      using 1 by (simp add: assms(1) filter_inf_closed)
    have 3: "?z  G  H"
      using 1 by (meson assms(2-3) Int_iff filter_def sup_ge1 sup_ge2)
    have "?y  ?z = (t  v  u)  (t  v  w)"
      by (simp add: inf_sup_distrib1)
    also have "...  (t  u)  (v  w)"
      by (metis inf.cobounded1 inf.cobounded2 inf.left_idem inf_mono sup.mono)
    also have "...  x"
      using 1 by (simp add: le_supI)
    finally show "x  filter_sup F (G  H)"
      unfolding filter_sup_def using 2 3 by blast
  qed
qed

lemma filter_inf_principal_rep:
  "F  G = z  (xF . yG . z = x  y)"
  by force

lemma filter_sup_principal_rep:
  assumes "filter F"
      and "filter G"
      and "filter_sup F G = z"
    shows "xF . yG . z = x  y"
proof -
  from assms(3) obtain x y where 1: "xF  yG  x  y  z"
    unfolding filter_sup_def using order_refl by blast
  hence 2: "x  z  F  y  z  G"
    by (meson assms(1-2) sup_ge1 filter_def)
  have "(x  z)  (y  z) = z"
    using 1 sup_absorb2 sup_inf_distrib2 by fastforce
  thus ?thesis
    using 2 by force
qed

lemma inf_sup_principal_aux:
  assumes "filter F"
      and "filter G"
      and "is_principal_up (filter_sup F G)"
      and "is_principal_up (F  G)"
    shows "is_principal_up F"
proof -
  from assms(3-4) obtain x y where 1: "filter_sup F G = x  F  G = y"
    by blast
  from filter_inf_principal_rep obtain t u where 2: "tF  uG  y = t  u"
    using 1 by meson
  from filter_sup_principal_rep obtain v w where 3: "vF  wG  x = v  w"
    using 1 by (meson assms(1-2))
  have "t  filter_sup F G  u  filter_sup F G"
    unfolding filter_sup_def using 2 inf.cobounded1 inf.cobounded2 by blast
  hence "x  t  x  u"
    using 1 by blast
  hence 4: "(t  v)  (u  w) = x"
    using 3 by (simp add: inf.absorb2 inf.assoc inf.left_commute)
  have "(t  v)  (u  w)  F  (t  v)  (u  w)  G"
    using 2 3 by (metis (no_types, lifting) assms(1-2) filter_inf_closed sup.cobounded1 sup.cobounded2 filter_def)
  hence "y  (t  v)  (u  w)"
    using 1 Int_iff by blast
  hence 5: "(t  v)  (u  w) = y"
    using 2 by (simp add: order.antisym inf.coboundedI1)
  have "F = (t  v)"
  proof
    show "F  (t  v)"
    proof
      fix z
      assume 6: "z  F"
      hence "z  filter_sup F G"
        unfolding filter_sup_def using 2 inf.cobounded1 by blast
      hence "x  z"
        using 1 by simp
      hence 7: "(t  v  z)  (u  w) = x"
        using 4 by (metis inf.absorb1 inf.assoc inf.commute)
      have "z  u  F  z  u  G  z  w  F  z  w  G"
        using 2 3 6 by (meson assms(1-2) filter_def sup_ge1 sup_ge2)
      hence "y  (z  u)  (z  w)"
        using 1 Int_iff filter_inf_closed by auto
      hence 8: "(t  v  z)  (u  w) = y"
        using 5 by (metis inf.absorb1 sup.commute sup_inf_distrib2)
      have "t  v  z = t  v"
        using 4 5 7 8 relative_equality by blast
      thus "z  (t  v)"
        by (simp add: inf.orderI)
    qed
  next
    show "(t  v)  F"
    proof
      fix z
      have 9: "t  v  F"
        using 2 3 by (simp add: assms(1) filter_inf_closed)
      assume "z  (t  v)"
      hence "t  v  z" by simp
      thus "z  F"
        using assms(1) 9 filter_def by auto
    qed
  qed
  thus ?thesis
    by blast
qed

text ‹
The following result is \cite[Lemma II]{GraetzerSchmidt1958}.
If both join and meet of two filters are principal filters, both filters are principal filters.
›

lemma inf_sup_principal:
  assumes "filter F"
      and "filter G"
      and "is_principal_up (filter_sup F G)"
      and "is_principal_up (F  G)"
    shows "is_principal_up F  is_principal_up G"
proof -
  have "filter G  filter F  is_principal_up (filter_sup G F)  is_principal_up (G  F)"
    by (simp add: assms Int_commute filter_sup_symmetric)
  thus ?thesis
    using assms(3) inf_sup_principal_aux by blast
qed

lemma filter_sup_absorb_inf: "filter F  filter G  filter_sup (F  G) G = G"
  by (simp add: filter_inf filter_sup_least_upper_bound filter_sup_left_upper_bound filter_sup_symmetric subset_antisym)

lemma filter_inf_absorb_sup: "filter F  filter G  filter_sup F G  G = G"
  apply (rule subset_antisym)
  apply simp
  by (simp add: filter_sup_right_upper_bound)

lemma filter_inf_right_dist_sup:
  assumes "filter F"
      and "filter G"
      and "filter H"
    shows "filter_sup F G  H = filter_sup (F  H) (G  H)"
proof -
  have "filter_sup (F  H) (G  H) = filter_sup (F  H) G  filter_sup (F  H) H"
    by (simp add: assms filter_sup_left_dist_inf filter_inf)
  also have "... = filter_sup (F  H) G  H"
    using assms(1,3) filter_sup_absorb_inf by simp
  also have "... = filter_sup F G  filter_sup G H  H"
    using assms filter_sup_left_dist_inf filter_sup_symmetric by simp
  also have "... = filter_sup F G  H"
    by (simp add: assms(2-3) filter_inf_absorb_sup semilattice_inf_class.inf_assoc)
  finally show ?thesis
    by simp
qed

text ‹
The following result generalises \cite[10.11]{DaveyPriestley2002} to distributive lattices as remarked after that section.
›

lemma ultra_filter_prime:
  assumes "ultra_filter F"
    shows "prime_filter F"
proof -
  {
    fix x y
    assume 1: "x  y  F  x  F"
    let ?G = "{ z . wF . x  w = z }"
    have 2: "filter ?G"
      using assms filter_inf_filter by simp
    have "x  ?G"
      using 1 by auto
    hence 3: "F  ?G"
      using 1 by auto
    have "F  ?G"
      using inf_le2 order_trans by blast
    hence "?G = UNIV"
      using 2 3 assms by blast
    then obtain z where 4: "z  F  x  z  y"
      by blast
    hence "y  z = (x  y)  z"
      by (simp add: inf_sup_distrib2 sup_absorb2)
    also have "...  F"
      using 1 4 assms filter_inf_closed by auto
    finally have "y  F"
      using assms by (simp add: filter_def)
  }
  thus ?thesis
    using assms by blast
qed

lemma up_dist_inf_inter:
  assumes "is_up_set S"
    shows "(x  y)  S = filter_sup (x  S) (y  S)  S"
proof
  show "(x  y)  S  filter_sup (x  S) (y  S)  S"
  proof
    fix z
    let ?x = "x  z"
    let ?y = "y  z"
    assume "z  (x  y)  S"
    hence 1: "x  y  z  z  S"
      by auto
    hence "?x  (x  S)  ?y  (y  S)  ?x  ?y  z"
      using assms sup_absorb2 sup_inf_distrib2 by fastforce
    thus "z  filter_sup (x  S) (y  S)  S"
      using filter_sup_def 1 by fastforce
  qed
next
  show "filter_sup (x  S) (y  S)  S  (x  y)  S"
  proof
    fix z
    assume "z  filter_sup (x  S) (y  S)  S"
    then obtain u v where 2: "ux  vy  u  v  z  z  S"
      using filter_sup_def by auto
    hence "x  y  z"
      using order.trans inf_mono by blast
    thus "z  (x  y)  S"
      using 2 by blast
  qed
qed

end

context distrib_lattice_bot
begin

lemma prime_filter:
  "proper_filter F  G . prime_filter G  F  G"
  by (metis ultra_filter ultra_filter_prime)

end

context distrib_lattice_top
begin

lemma complemented_filter_inf_principal:
  assumes "filter_complements F G"
    shows "is_principal_up (F  x)"
proof -
  have 1: "filter F  filter G"
    by (simp add: assms)
  hence 2: "filter (F  x)  filter (G  x)"
    by (simp add: filter_inf)
  have "(F  x)  (G  x) = {top}"
    using assms Int_assoc Int_insert_left_if1 inf_bot_left inf_sup_aci(3) top_in_upset inf.idem by auto
  hence 3: "is_principal_up ((F  x)  (G  x))"
    using up_top by blast
  have "filter_sup (F  x) (G  x) = filter_sup F G  x"
    using 1 filter_inf_right_dist_sup up_filter by auto
  also have "... = x"
    by (simp add: assms)
  finally have "is_principal_up (filter_sup (F  x) (G  x))"
    by auto
  thus ?thesis
    using 1 2 3 inf_sup_principal_aux by blast
qed

end

text ‹
The set of filters over a distributive lattice with a greatest element forms a bounded distributive lattice.
›

instantiation filter :: (distrib_lattice_top) bounded_distrib_lattice
begin

instance
  apply intro_classes
  apply transfer
  by (simp add: filter_sup_left_dist_inf)

end

end

Theory Stone_Construction

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

section ‹Stone Construction›

text ‹
This theory proves the uniqueness theorem for the triple representation of Stone algebras and the construction theorem of Stone algebras \cite{ChenGraetzer1969,Katrinak1973}.
Every Stone algebra $S$ has an associated triple consisting of
\begin{itemize}
\item the set of regular elements $B(S)$ of $S$,
\item the set of dense elements $D(S)$ of $S$, and
\item the structure map $\varphi(S) : B(S) \to F(D(S))$ defined by $\varphi(x) = {\uparrow} x \cap D(S)$.
\end{itemize}
Here $F(X)$ is the set of filters of a partially ordered set $X$.
We first show that
\begin{itemize}
\item $B(S)$ is a Boolean algebra,
\item $D(S)$ is a distributive lattice with a greatest element, whence $F(D(S))$ is a bounded distributive lattice, and
\item $\varphi(S)$ is a bounded lattice homomorphism.
\end{itemize}
Next, from a triple $T = (B,D,\varphi)$ such that $B$ is a Boolean algebra, $D$ is a distributive lattice with a greatest element and $\varphi : B \to F(D)$ is a bounded lattice homomorphism, we construct a Stone algebra $S(T)$.
The elements of $S(T)$ are pairs taken from $B \times F(D)$ following the construction of \cite{Katrinak1973}.
We need to represent $S(T)$ as a type to be able to instantiate the Stone algebra class.
Because the pairs must satisfy a condition depending on $\varphi$, this would require dependent types.
Since Isabelle/HOL does not have dependent types, we use a function lifting instead.
The lifted pairs form a Stone algebra.

Next, we specialise the construction to start with the triple associated with a Stone algebra $S$, that is, we construct $S(B(S),D(S),\varphi(S))$.
In this case, we can instantiate the lifted pairs to obtain a type of pairs (that no longer implements a dependent type).
To achieve this, we construct an embedding of the type of pairs into the lifted pairs, so that we inherit the Stone algebra axioms (using a technique of universal algebra that works for universally quantified equations and equational implications).

Next, we show that the Stone algebras $S(B(S),D(S),\varphi(S))$ and $S$ are isomorphic.
We give explicit mappings in both directions.
This implies the uniqueness theorem for the triple representation of Stone algebras.

Finally, we show that the triples $(B(S(T)),D(S(T)),\varphi(S(T)))$ and $T$ are isomorphic.
This requires an isomorphism of the Boolean algebras $B$ and $B(S(T))$, an isomorphism of the distributive lattices $D$ and $D(S(T))$, and a proof that they preserve the structure maps.
We give explicit mappings of the Boolean algebra isomorphism and the distributive lattice isomorphism in both directions.
This implies the construction theorem of Stone algebras.
Because $S(T)$ is implemented by lifted pairs, so are $B(S(T))$ and $D(S(T))$; we therefore also lift $B$ and $D$ to establish the isomorphisms.
›

theory Stone_Construction

imports P_Algebras Filters

begin

text ‹
A triple consists of a Boolean algebra, a distributive lattice with a greatest element, and a structure map.
The Boolean algebra and the distributive lattice are represented as HOL types.
Because both occur in the type of the structure map, the triple is determined simply by the structure map and its HOL type.
The structure map needs to be a bounded lattice homomorphism.
›

locale triple =
  fixes phi :: "'a::boolean_algebra  'b::distrib_lattice_top filter"
  assumes hom: "bounded_lattice_homomorphism phi"

subsection ‹The Triple of a Stone Algebra›

text ‹
In this section we construct the triple associated to a Stone algebra.
›

subsubsection ‹Regular Elements›

text ‹
The regular elements of a Stone algebra form a Boolean subalgebra.
›

typedef (overloaded) 'a regular = "regular_elements::'a::stone_algebra set"
  by auto

lemma simp_regular [simp]:
  "y . Rep_regular x = -y"
  using Rep_regular by simp

setup_lifting type_definition_regular

instantiation regular :: (stone_algebra) boolean_algebra
begin

lift_definition sup_regular :: "'a regular  'a regular  'a regular" is sup
  by (meson regular_in_p_image_iff regular_closed_sup)

lift_definition inf_regular :: "'a regular  'a regular  'a regular" is inf
  by (meson regular_in_p_image_iff regular_closed_inf)

lift_definition minus_regular :: "'a regular  'a regular  'a regular" is "λx y . x  -y"
  by (meson regular_in_p_image_iff regular_closed_inf)

lift_definition uminus_regular :: "'a regular  'a regular" is uminus
  by auto

lift_definition bot_regular :: "'a regular" is bot
  by (meson regular_in_p_image_iff regular_closed_bot)

lift_definition top_regular :: "'a regular" is top
  by (meson regular_in_p_image_iff regular_closed_top)

lift_definition less_eq_regular :: "'a regular  'a regular  bool" is less_eq .

lift_definition less_regular :: "'a regular  'a regular  bool" is less .

instance
  apply intro_classes
  subgoal apply transfer by (simp add: less_le_not_le)
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by (simp add: sup_inf_distrib1)
  subgoal apply transfer by simp
  subgoal apply transfer by auto
  subgoal apply transfer by simp
  done

end

instantiation regular :: (non_trivial_stone_algebra) non_trivial_boolean_algebra
begin

instance
proof (intro_classes, rule ccontr)
  assume "¬(x y::'a regular . x  y)"
  hence "(bot::'a regular) = top"
    by simp
  hence "(bot::'a) = top"
    by (metis bot_regular.rep_eq top_regular.rep_eq)
  thus False
    by (simp add: bot_not_top)
qed

end

subsubsection ‹Dense Elements›

text ‹
The dense elements of a Stone algebra form a distributive lattice with a greatest element.
›

typedef (overloaded) 'a dense = "dense_elements::'a::stone_algebra set"
  using dense_closed_top by blast

lemma simp_dense [simp]:
  "-Rep_dense x = bot"
  using Rep_dense by simp

setup_lifting type_definition_dense

instantiation dense :: (stone_algebra) distrib_lattice_top
begin

lift_definition sup_dense :: "'a dense  'a dense  'a dense" is sup
  by simp

lift_definition inf_dense :: "'a dense  'a dense  'a dense" is inf
  by simp

lift_definition top_dense :: "'a dense" is top
  by simp

lift_definition less_eq_dense :: "'a dense  'a dense  bool" is less_eq .

lift_definition less_dense :: "'a dense  'a dense  bool" is less .

instance
  apply intro_classes
  subgoal apply transfer by (simp add: inf.less_le_not_le)
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by (simp add: sup_inf_distrib1)
  done

end

lemma up_filter_dense_antitone_dense:
  "dense (x  -x  y)  dense (x  -x  y  z)"
  by simp

lemma up_filter_dense_antitone:
  "up_filter (Abs_dense (x  -x  y  z))  up_filter (Abs_dense (x  -x  y))"
  by (unfold up_filter_antitone[THEN sym]) (simp add: Abs_dense_inverse less_eq_dense.rep_eq)

text ‹
The filters of dense elements of a Stone algebra form a bounded distributive lattice.
›

type_synonym 'a dense_filter = "'a dense filter"

typedef (overloaded) 'a dense_filter_type = "{ x::'a dense_filter . True }"
  using filter_top by blast

setup_lifting type_definition_dense_filter_type

instantiation dense_filter_type :: (stone_algebra) bounded_distrib_lattice
begin

lift_definition sup_dense_filter_type :: "'a dense_filter_type  'a dense_filter_type  'a dense_filter_type" is sup .

lift_definition inf_dense_filter_type :: "'a dense_filter_type  'a dense_filter_type  'a dense_filter_type" is inf .

lift_definition bot_dense_filter_type :: "'a dense_filter_type" is bot ..

lift_definition top_dense_filter_type :: "'a dense_filter_type" is top ..

lift_definition less_eq_dense_filter_type :: "'a dense_filter_type  'a dense_filter_type  bool" is less_eq .

lift_definition less_dense_filter_type :: "'a dense_filter_type  'a dense_filter_type  bool" is less .

instance
  apply intro_classes
  subgoal apply transfer by (simp add: inf.less_le_not_le)
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by simp
  subgoal apply transfer by (simp add: sup_inf_distrib1)
  done

end

subsubsection ‹The Structure Map›

text ‹
The structure map of a Stone algebra is a bounded lattice homomorphism.
It maps a regular element x› to the set of all dense elements above -x›.
This set is a filter.
›

abbreviation stone_phi_base :: "'a::stone_algebra regular  'a dense set"
  where "stone_phi_base x  { y . -Rep_regular x  Rep_dense y }"

lemma stone_phi_base_filter:
  "filter (stone_phi_base x)"
  apply (unfold filter_def, intro conjI)
  apply (metis Collect_empty_eq top_dense.rep_eq top_greatest)
  apply (metis inf_dense.rep_eq inf_le2 le_inf_iff mem_Collect_eq)
  using order_trans less_eq_dense.rep_eq by blast

definition stone_phi :: "'a::stone_algebra regular  'a dense_filter"
  where "stone_phi x = Abs_filter (stone_phi_base x)"

text ‹
To show that we obtain a triple, we only need to prove that stone_phi› is a bounded lattice homomorphism.
The Boolean algebra and the distributive lattice requirements are taken care of by the type system.
›

interpretation stone_phi: triple "stone_phi"
proof (unfold_locales, intro conjI)
  have 1: "Rep_regular (Abs_regular bot) = bot"
    by (metis bot_regular.rep_eq bot_regular_def)
  show "stone_phi bot = bot"
    apply (unfold stone_phi_def bot_regular_def 1 p_bot bot_filter_def)
    by (metis (mono_tags, lifting) Collect_cong Rep_dense_inject order_refl singleton_conv top.extremum_uniqueI top_dense.rep_eq)
next
  show "stone_phi top = top"
    by (metis Collect_cong stone_phi_def UNIV_I bot.extremum dense_closed_top top_empty_eq top_filter.abs_eq top_regular.rep_eq top_set_def)
next
  show "x y::'a regular . stone_phi (x  y) = stone_phi x  stone_phi y"
  proof (intro allI)
    fix x y :: "'a regular"
    have "stone_phi_base (x  y) = filter_sup (stone_phi_base x) (stone_phi_base y)"
    proof (rule set_eqI, rule iffI)
      fix z
      assume 2: "z  stone_phi_base (x  y)"
      let ?t = "-Rep_regular x  Rep_dense z"
      let ?u = "-Rep_regular y  Rep_dense z"
      let ?v = "Abs_dense ?t"
      let ?w = "Abs_dense ?u"
      have 3: "?v  stone_phi_base x  ?w  stone_phi_base y"
        by (simp add: Abs_dense_inverse)
      have "?v  ?w = Abs_dense (?t  ?u)"
        by (simp add: eq_onp_def inf_dense.abs_eq)
      also have "... = Abs_dense (-Rep_regular (x  y)  Rep_dense z)"
        by (simp add: distrib(1) sup_commute sup_regular.rep_eq)
      also have "... = Abs_dense (Rep_dense z)"
        using 2 by (simp add: le_iff_sup)
      also have "... = z"
        by (simp add: Rep_dense_inverse)
      finally show "z  filter_sup (stone_phi_base x) (stone_phi_base y)"
        using 3 mem_Collect_eq order_refl filter_sup_def by fastforce
    next
      fix z
      assume "z  filter_sup (stone_phi_base x) (stone_phi_base y)"
      then obtain v w where 4: "v  stone_phi_base x  w  stone_phi_base y  v  w  z"
        unfolding filter_sup_def by auto
      have "-Rep_regular (x  y) = Rep_regular (-(x  y))"
        by (metis uminus_regular.rep_eq)
      also have "... = -Rep_regular x  -Rep_regular y"
        by (simp add: inf_regular.rep_eq uminus_regular.rep_eq)
      also have "...  Rep_dense v  Rep_dense w"
        using 4 inf_mono mem_Collect_eq by blast
      also have "... = Rep_dense (v  w)"
        by (simp add: inf_dense.rep_eq)
      also have "...  Rep_dense z"
        using 4 by (simp add: less_eq_dense.rep_eq)
      finally show "z  stone_phi_base (x  y)"
        by simp
    qed
    thus "stone_phi (x  y) = stone_phi x  stone_phi y"
      by (simp add: stone_phi_def eq_onp_same_args stone_phi_base_filter sup_filter.abs_eq)
  qed
next
  show "x y::'a regular . stone_phi (x  y) = stone_phi x  stone_phi y"
  proof (intro allI)
    fix x y :: "'a regular"
    have "z . -Rep_regular (x  y)  Rep_dense z  -Rep_regular x  Rep_dense z  -Rep_regular y  Rep_dense z"
      by (simp add: inf_regular.rep_eq)
    hence "stone_phi_base (x  y) = (stone_phi_base x)  (stone_phi_base y)"
      by auto
    thus "stone_phi (x  y) = stone_phi x  stone_phi y"
      by (simp add: stone_phi_def eq_onp_same_args stone_phi_base_filter inf_filter.abs_eq)
  qed
qed

subsection ‹Properties of Triples›

text ‹
In this section we construct a certain set of pairs from a triple, introduce operations on these pairs and develop their properties.
The given set and operations will form a Stone algebra.
›

context triple
begin

lemma phi_bot:
  "phi bot = Abs_filter {top}"
  by (metis hom bot_filter_def)

lemma phi_top:
  "phi top = Abs_filter UNIV"
  by (metis hom top_filter_def)

text ‹
The occurrence of phi› in the following definition of the pairs creates a need for dependent types.
›

definition pairs :: "('a × 'b filter) set"
  where "pairs = { (x,y) . z . y = phi (-x)  up_filter z }"

text ‹
Operations on pairs are defined in the following.
They will be used to establish that the pairs form a Stone algebra.
›

fun pairs_less_eq :: "('a × 'b filter)  ('a × 'b filter)  bool"
  where "pairs_less_eq (x,y) (z,w) = (x  z  w  y)"

fun pairs_less :: "('a × 'b filter)  ('a × 'b filter)  bool"
  where "pairs_less (x,y) (z,w) = (pairs_less_eq (x,y) (z,w)  ¬ pairs_less_eq (z,w) (x,y))"

fun pairs_sup :: "('a × 'b filter)  ('a × 'b filter)  ('a × 'b filter)"
  where "pairs_sup (x,y) (z,w) = (x  z,y  w)"

fun pairs_inf :: "('a × 'b filter)  ('a × 'b filter)  ('a × 'b filter)"
  where "pairs_inf (x,y) (z,w) = (x  z,y  w)"

fun pairs_minus :: "('a × 'b filter)  ('a × 'b filter)  ('a × 'b filter)"
  where "pairs_minus (x,y) (z,w) = (x  -z,y  phi z)"

fun pairs_uminus :: "('a × 'b filter)  ('a × 'b filter)"
  where "pairs_uminus (x,y) = (-x,phi x)"

abbreviation pairs_bot :: "('a × 'b filter)"
  where "pairs_bot  (bot,Abs_filter UNIV)"

abbreviation pairs_top :: "('a × 'b filter)"
  where "pairs_top  (top,Abs_filter {top})"

lemma pairs_top_in_set:
  "(x,y)  pairs  top  Rep_filter y"
  by simp

lemma phi_complemented:
  "complement (phi x) (phi (-x))"
  by (metis hom inf_compl_bot sup_compl_top)

lemma phi_inf_principal:
  "z . up_filter z = phi x  up_filter y"
proof -
  let ?F = "Rep_filter (phi x)"
  let ?G = "Rep_filter (phi (-x))"
  have 1: "eq_onp filter ?F ?F  eq_onp filter (y) (y)"
    by (simp add: eq_onp_def)
  have "filter_complements ?F ?G"
    apply (intro conjI)
    apply simp
    apply simp
    apply (metis (no_types) phi_complemented sup_filter.rep_eq top_filter.rep_eq)
    by (metis (no_types) phi_complemented inf_filter.rep_eq bot_filter.rep_eq)
  hence "is_principal_up (?F  y)"
    using complemented_filter_inf_principal by blast
  then obtain z where "z = ?F  y"
    by auto
  hence "up_filter z = Abs_filter (?F  y)"
    by simp
  also have "... = Abs_filter ?F  up_filter y"
    using 1 inf_filter.abs_eq by force
  also have "... = phi x  up_filter y"
    by (simp add: Rep_filter_inverse)
  finally show ?thesis
    by auto
qed

text ‹
Quite a bit of filter theory is involved in showing that the intersection of phi x› with a principal filter is a principal filter, so the following function can extract its least element.
›

fun rho :: "'a  'b  'b"
  where "rho x y = (SOME z . up_filter z = phi x  up_filter y)"

lemma rho_char:
  "up_filter (rho x y) = phi x  up_filter y"
  by (metis (mono_tags) someI_ex rho.simps phi_inf_principal)

text ‹
The following results show that the pairs are closed under the given operations.
›

lemma pairs_sup_closed:
  assumes "(x,y)  pairs"
      and "(z,w)  pairs"
    shows "pairs_sup (x,y) (z,w)  pairs"
proof -
  from assms obtain u v where "y = phi (-x)  up_filter u  w = phi (-z)  up_filter v"
    using pairs_def by auto
  hence "pairs_sup (x,y) (z,w) = (x  z,(phi (-x)  up_filter u)  (phi (-z)  up_filter v))"
    by simp
  also have "... = (x  z,(phi (-x)  phi (-z))  (phi (-x)  up_filter v)  (up_filter u  phi (-z))  (up_filter u  up_filter v))"
    by (simp add: inf.sup_commute inf_sup_distrib1 sup_commute sup_left_commute)
  also have "... = (x  z,phi (-(x  z))  (phi (-x)  up_filter v)  (up_filter u  phi (-z))  (up_filter u  up_filter v))"
    using hom by simp
  also have "... = (x  z,phi (-(x  z))  up_filter (rho (-x) v)  up_filter (rho (-z) u)  (up_filter u  up_filter v))"
    by (metis inf.sup_commute rho_char)
  also have "... = (x  z,phi (-(x  z))  up_filter (rho (-x) v)  up_filter (rho (-z) u)  up_filter (u  v))"
    by (metis up_filter_dist_sup)
  also have "... = (x  z,phi (-(x  z))  up_filter (rho (-x) v  rho (-z) u  (u  v)))"
    by (simp add: sup_commute sup_left_commute up_filter_dist_inf)
  finally show ?thesis
    using pairs_def by auto
qed

lemma pairs_inf_closed:
  assumes "(x,y)  pairs"
      and "(z,w)  pairs"
    shows "pairs_inf (x,y) (z,w)  pairs"
proof -
  from assms obtain u v where "y = phi (-x)  up_filter u  w = phi (-z)  up_filter v"
    using pairs_def by auto
  hence "pairs_inf (x,y) (z,w) = (x  z,(phi (-x)  up_filter u)  (phi (-z)  up_filter v))"
    by simp
  also have "... = (x  z,(phi (-x)  phi (-z))  (up_filter u  up_filter v))"
    by (simp add: sup_commute sup_left_commute)
  also have "... = (x  z,phi (-(x  z))  (up_filter u  up_filter v))"
    using hom by simp
  also have "... = (x  z,phi (-(x  z))  up_filter (u  v))"
    by (simp add: up_filter_dist_inf)
  finally show ?thesis
    using pairs_def by auto
qed

lemma pairs_uminus_closed:
  "pairs_uminus (x,y)  pairs"
proof -
  have "pairs_uminus (x,y) = (-x,phi (--x)  bot)"
    by simp
  also have "... = (-x,phi (--x)  up_filter top)"
    by (simp add: bot_filter.abs_eq)
  finally show ?thesis
    by (metis (mono_tags, lifting) mem_Collect_eq old.prod.case pairs_def)
qed

lemma pairs_bot_closed:
  "pairs_bot  pairs"
  using pairs_def phi_top triple.hom triple_axioms by fastforce

lemma pairs_top_closed:
  "pairs_top  pairs"
  by (metis p_bot pairs_uminus.simps pairs_uminus_closed phi_bot)

text ‹
We prove enough properties of the pair operations so that we can later show they form a Stone algebra.
›

lemma pairs_sup_dist_inf:
  "(x,y)  pairs  (z,w)  pairs  (u,v)  pairs  pairs_sup (x,y) (pairs_inf (z,w) (u,v)) = pairs_inf (pairs_sup (x,y) (z,w)) (pairs_sup (x,y) (u,v))"
  using sup_inf_distrib1 inf_sup_distrib1 by auto

lemma pairs_phi_less_eq:
  "(x,y)  pairs  phi (-x)  y"
  using pairs_def by auto

lemma pairs_uminus_galois:
  assumes "(x,y)  pairs"
      and "(z,w)  pairs"
    shows "pairs_inf (x,y) (z,w) = pairs_bot  pairs_less_eq (x,y) (pairs_uminus (z,w))"
proof -
  have 1: "x  z = bot  y  w = Abs_filter UNIV  phi z  y"
    by (metis (no_types, lifting) assms(1) heyting.implies_inf_absorb hom le_supE pairs_phi_less_eq sup_bot_right)
  have 2: "x  -z  phi z  y  y  w = Abs_filter UNIV"
  proof
    assume 3: "x  -z  phi z  y"
    have "Abs_filter UNIV = phi z  phi (-z)"
      using hom phi_complemented phi_top by auto
    also have "...  y  w"
      using 3 assms(2) sup_mono pairs_phi_less_eq by auto
    finally show "y  w = Abs_filter UNIV"
      using hom phi_top top.extremum_uniqueI by auto
  qed
  have "x  z = bot  x  -z"
    by (simp add: shunting_1)
  thus ?thesis
    using 1 2 Pair_inject pairs_inf.simps pairs_less_eq.simps pairs_uminus.simps by auto
qed

lemma pairs_stone:
  "(x,y)  pairs  pairs_sup (pairs_uminus (x,y)) (pairs_uminus (pairs_uminus (x,y))) = pairs_top"
  by (metis hom pairs_sup.simps pairs_uminus.simps phi_bot phi_complemented stone)

text ‹
The following results show how the regular elements and the dense elements among the pairs look like.
›

abbreviation "dense_pairs  { (x,y) . (x,y)  pairs  pairs_uminus (x,y) = pairs_bot }"
abbreviation "regular_pairs  { (x,y) . (x,y)  pairs  pairs_uminus (pairs_uminus (x,y)) = (x,y) }"
abbreviation "is_principal_up_filter x  y . x = up_filter y"

lemma dense_pairs:
  "dense_pairs = { (x,y) . x = top  is_principal_up_filter y }"
proof -
  have "dense_pairs = { (x,y) . (x,y)  pairs  x = top }"
    by (metis Pair_inject compl_bot_eq double_compl pairs_uminus.simps phi_top)
  also have "... = { (x,y) . (z . y = up_filter z)  x = top }"
    using hom pairs_def by auto
  finally show ?thesis
    by auto
qed

lemma regular_pairs:
  "regular_pairs = { (x,y) . y = phi (-x) }"
  using pairs_def pairs_uminus_closed by fastforce

text ‹
The following extraction function will be used in defining one direction of the Stone algebra isomorphism.
›

fun rho_pair :: "'a × 'b filter  'b"
  where "rho_pair (x,y) = (SOME z . up_filter z = phi x  y)"

lemma get_rho_pair_char:
  assumes "(x,y)  pairs"
    shows "up_filter (rho_pair (x,y)) = phi x  y"
proof -
  from assms obtain w where "y = phi (-x)  up_filter w"
    using pairs_def by auto
  hence "phi x  y = phi x  up_filter w"
    by (simp add: inf_sup_distrib1 phi_complemented)
  thus ?thesis
    using rho_char by auto
qed

lemma sa_iso_pair:
  "(--x,phi (-x)  up_filter y)  pairs"
  using pairs_def by auto

end

subsection ‹The Stone Algebra of a Triple›

text ‹
In this section we prove that the set of pairs constructed in a triple forms a Stone Algebra.
The following type captures the parameter phi› on which the type of triples depends.
This parameter is the structure map that occurs in the definition of the set of pairs.
The set of all structure maps is the set of all bounded lattice homomorphisms (of appropriate type).
In order to make it a HOL type, we need to show that at least one such structure map exists.
To this end we use the ultrafilter lemma: the required bounded lattice homomorphism is essentially the characteristic map of an ultrafilter, but the latter must exist.
In particular, the underlying Boolean algebra must contain at least two elements.
›

typedef (overloaded) ('a,'b) phi = "{ f::'a::non_trivial_boolean_algebra  'b::distrib_lattice_top filter . bounded_lattice_homomorphism f }"
proof -
  from ultra_filter_exists obtain F :: "'a set" where 1: "ultra_filter F"
    by auto
  hence 2: "prime_filter F"
    using ultra_filter_prime by auto
  let ?f = "λx . if xF then top else bot::'b filter"
  have "bounded_lattice_homomorphism ?f"
  proof (intro conjI)
    show "?f bot = bot"
      using 1 by (meson bot.extremum filter_def subset_eq top.extremum_unique)
  next
    show "?f top = top"
      using 1 by simp
  next
    show "x y . ?f (x  y) = ?f x  ?f y"
    proof (intro allI)
      fix x y
      show "?f (x  y) = ?f x  ?f y"
        apply (cases "x  F"; cases "y  F")
        using 1 filter_def apply fastforce
        using 1 filter_def apply fastforce
        using 1 filter_def apply fastforce
        using 2 sup_bot_left by auto
   qed
  next
    show "x y . ?f (x  y) = ?f x  ?f y"
    proof (intro allI)
      fix x y
      show "?f (x  y) = ?f x  ?f y"
        apply (cases "x  F"; cases "y  F")
        using 1 apply (simp add: filter_inf_closed)
        using 1 apply (metis (mono_tags, lifting) brouwer.inf_sup_ord(4) inf_top_left filter_def)
        using 1 apply (metis (mono_tags, lifting) brouwer.inf_sup_ord(3) inf_top_right filter_def)
        using 1 filter_def by force
    qed
  qed
  hence "?f  {f . bounded_lattice_homomorphism f}"
    by simp
  thus ?thesis
    by meson
qed

lemma simp_phi [simp]:
  "bounded_lattice_homomorphism (Rep_phi x)"
  using Rep_phi by simp

setup_lifting type_definition_phi

text ‹
The following implements the dependent type of pairs depending on structure maps.
It uses functions from structure maps to pairs with the requirement that, for each structure map, the corresponding pair is contained in the set of pairs constructed for a triple with that structure map.

If this type could be defined in the locale triple› and instantiated to Stone algebras there, there would be no need for the lifting and we could work with triples directly.
›

typedef (overloaded) ('a,'b) lifted_pair = "{ pf::('a::non_trivial_boolean_algebra,'b::distrib_lattice_top) phi  'a × 'b filter . f . pf f  triple.pairs (Rep_phi f) }"
proof -
  have "f::('a,'b) phi . triple.pairs_bot  triple.pairs (Rep_phi f)"
  proof
    fix f :: "('a,'b) phi"
    have "triple (Rep_phi f)"
      by (simp add: triple_def)
    thus "triple.pairs_bot  triple.pairs (Rep_phi f)"
      using triple.regular_pairs triple.phi_top by fastforce
  qed
  thus ?thesis
    by auto
qed

lemma simp_lifted_pair [simp]:
  "f . Rep_lifted_pair pf f  triple.pairs (Rep_phi f)"
  using Rep_lifted_pair by simp

setup_lifting type_definition_lifted_pair

text ‹
The lifted pairs form a Stone algebra.
›

instantiation lifted_pair :: (non_trivial_boolean_algebra,distrib_lattice_top) stone_algebra
begin

text ‹
All operations are lifted point-wise.
›

lift_definition sup_lifted_pair :: "('a,'b) lifted_pair  ('a,'b) lifted_pair  ('a,'b) lifted_pair" is "λxf yf f . triple.pairs_sup (xf f) (yf f)"
  by (metis (no_types, hide_lams) simp_phi triple_def triple.pairs_sup_closed prod.collapse)

lift_definition inf_lifted_pair :: "('a,'b) lifted_pair  ('a,'b) lifted_pair  ('a,'b) lifted_pair" is "λxf yf f . triple.pairs_inf (xf f) (yf f)"
  by (metis (no_types, hide_lams) simp_phi triple_def triple.pairs_inf_closed prod.collapse)

lift_definition uminus_lifted_pair :: "('a,'b) lifted_pair  ('a,'b) lifted_pair" is "λxf f . triple.pairs_uminus (Rep_phi f) (xf f)"
  by (metis (no_types, hide_lams) simp_phi triple_def triple.pairs_uminus_closed prod.collapse)

lift_definition bot_lifted_pair :: "('a,'b) lifted_pair" is "λf . triple.pairs_bot"
  by (metis (no_types, hide_lams) simp_phi triple_def triple.pairs_bot_closed)

lift_definition top_lifted_pair :: "('a,'b) lifted_pair" is "λf . triple.pairs_top"
  by (metis (no_types, hide_lams) simp_phi triple_def triple.pairs_top_closed)

lift_definition less_eq_lifted_pair :: "('a,'b) lifted_pair  ('a,'b) lifted_pair  bool" is "λxf yf . f . triple.pairs_less_eq (xf f) (yf f)" .

lift_definition less_lifted_pair :: "('a,'b) lifted_pair  ('a,'b) lifted_pair  bool" is "λxf yf . (f . triple.pairs_less_eq (xf f) (yf f))  ¬ (f . triple.pairs_less_eq (yf f) (xf f))" .

instance
proof intro_classes
  fix xf yf :: "('a,'b) lifted_pair"
  show "xf < yf  xf  yf  ¬ yf  xf"
    by (simp add: less_lifted_pair.rep_eq less_eq_lifted_pair.rep_eq)
next
  fix xf :: "('a,'b) lifted_pair"
  {
    fix f :: "('a,'b) phi"
    have 1: "triple (Rep_phi f)"
      by (simp add: triple_def)
    let ?x = "Rep_lifted_pair xf f"
    obtain x1 x2 where "(x1,x2) = ?x"
      using prod.collapse by blast
    hence "triple.pairs_less_eq ?x ?x"
      using 1 by (metis triple.pairs_less_eq.simps order_refl)
  }
  thus "xf  xf"
    by (simp add: less_eq_lifted_pair.rep_eq)
next
  fix xf yf zf :: "('a,'b) lifted_pair"
  assume 1: "xf  yf" and 2: "yf  zf"
  {
    fix f :: "('a,'b) phi"
    have 3: "triple (Rep_phi f)"
      by (simp add: triple_def)
    let ?x = "Rep_lifted_pair xf f"
    let ?y = "Rep_lifted_pair yf f"
    let ?z = "Rep_lifted_pair zf f"
    obtain x1 x2 y1 y2 z1 z2 where 4: "(x1,x2) = ?x  (y1,y2) = ?y  (z1,z2) = ?z"
      using prod.collapse by blast
    have "triple.pairs_less_eq ?x ?y  triple.pairs_less_eq ?y ?z"
      using 1 2 3 less_eq_lifted_pair.rep_eq by simp
    hence "triple.pairs_less_eq ?x ?z"
      using 3 4 by (metis (mono_tags, lifting) triple.pairs_less_eq.simps order_trans)
  }
  thus "xf  zf"
    by (simp add: less_eq_lifted_pair.rep_eq)
next
  fix xf yf :: "('a,'b) lifted_pair"
  assume 1: "xf  yf" and 2: "yf  xf"
  {
    fix f :: "('a,'b) phi"
    have 3: "triple (Rep_phi f)"
      by (simp add: triple_def)
    let ?x = "Rep_lifted_pair xf f"
    let ?y = "Rep_lifted_pair yf f"
    obtain x1 x2 y1 y2 where 4: "(x1,x2) = ?x  (y1,y2) = ?y"
      using prod.collapse by blast
    have "triple.pairs_less_eq ?x ?y  triple.pairs_less_eq ?y ?x"
      using 1 2 3 less_eq_lifted_pair.rep_eq by simp
    hence "?x = ?y"
      using 3 4 by (metis (mono_tags, lifting) triple.pairs_less_eq.simps antisym)
  }
  thus "xf = yf"
    by (metis Rep_lifted_pair_inverse ext)
next
  fix xf yf :: "('a,'b) lifted_pair"
  {
    fix f :: "('a,'b) phi"
    have 1: "triple (Rep_phi f)"
      by (simp add: triple_def)
    let ?x = "Rep_lifted_pair xf f"
    let ?y = "Rep_lifted_pair yf f"
    obtain x1 x2 y1 y2 where "(x1,x2) = ?x  (y1,y2) = ?y"
      using prod.collapse by blast
    hence "triple.pairs_less_eq (triple.pairs_inf ?x ?y) ?y"
      using 1 by (metis (mono_tags, lifting) inf_sup_ord(2) sup.cobounded2 triple.pairs_inf.simps triple.pairs_less_eq.simps inf_lifted_pair.rep_eq)
  }
  thus "xf  yf  yf"
    by (simp add: less_eq_lifted_pair.rep_eq inf_lifted_pair.rep_eq)
next
  fix xf yf :: "('a,'b) lifted_pair"
  {
    fix f :: "('a,'b) phi"
    have 1: "triple (Rep_phi f)"
      by (simp add: triple_def)
    let ?x = "Rep_lifted_pair xf f"
    let ?y = "Rep_lifted_pair yf f"
    obtain x1 x2 y1 y2 where "(x1,x2) = ?x  (y1,y2) = ?y"
      using prod.collapse by blast
    hence "triple.pairs_less_eq (triple.pairs_inf ?x ?y) ?x"
      using 1 by (metis (mono_tags, lifting) inf_sup_ord(1) sup.cobounded1 triple.pairs_inf.simps triple.pairs_less_eq.simps inf_lifted_pair.rep_eq)
  }
  thus "xf  yf  xf"
    by (simp add: less_eq_lifted_pair.rep_eq inf_lifted_pair.rep_eq)
next
  fix xf yf zf :: "('a,'b) lifted_pair"
  assume 1: "xf  yf" and 2: "xf  zf"
  {
    fix f :: "('a,'b) phi"
    have 3: "triple (Rep_phi f)"
      by (simp add: triple_def)
    let ?x = "Rep_lifted_pair xf f"
    let ?y = "Rep_lifted_pair yf f"
    let ?z = "Rep_lifted_pair zf f"
    obtain x1 x2 y1 y2 z1 z2 where 4: "(x1,x2) = ?x  (y1,y2) = ?y  (z1,z2) = ?z"
      using prod.collapse by blast
    have "triple.pairs_less_eq ?x ?y  triple.pairs_less_eq ?x ?z"
      using 1 2 3 less_eq_lifted_pair.rep_eq by simp
    hence "triple.pairs_less_eq ?x (triple.pairs_inf ?y ?z)"
      using 3 4 by (metis (mono_tags, lifting) le_inf_iff sup.bounded_iff triple.pairs_inf.simps triple.pairs_less_eq.simps)
  }
  thus "xf  yf  zf"
    by (simp add: less_eq_lifted_pair.rep_eq inf_lifted_pair.rep_eq)
next
  fix xf yf :: "('a,'b) lifted_pair"
  {
    fix f :: "('a,'b) phi"
    have 1: "triple (Rep_phi f)"
      by (simp add: triple_def)
    let ?x = "Rep_lifted_pair xf f"
    let ?y = "Rep_lifted_pair yf f"
    obtain x1 x2 y1 y2 where "(x1,x2) = ?x  (y1,y2) = ?y"
      using prod.collapse by blast
    hence "triple.pairs_less_eq ?x (triple.pairs_sup ?x ?y)"
      using 1 by (metis (no_types, lifting) inf_commute sup.cobounded1 inf.cobounded2 triple.pairs_sup.simps triple.pairs_less_eq.simps sup_lifted_pair.rep_eq)
  }
  thus "xf  xf  yf"
    by (simp add: less_eq_lifted_pair.rep_eq sup_lifted_pair.rep_eq)
next
  fix xf yf :: "('a,'b) lifted_pair"
  {
    fix f :: "('a,'b) phi"
    have 1: "triple (Rep_phi f)"
      by (simp add: triple_def)
    let ?x = "Rep_lifted_pair xf f"
    let ?y = "Rep_lifted_pair yf f"
    obtain x1 x2 y1 y2 where "(x1,x2) = ?x  (y1,y2) = ?y"
      using prod.collapse by blast
    hence "triple.pairs_less_eq ?y (triple.pairs_sup ?x ?y)"
      using 1 by (metis (no_types, lifting) sup.cobounded2 inf.cobounded2 triple.pairs_sup.simps triple.pairs_less_eq.simps sup_lifted_pair.rep_eq)
  }
  thus "yf  xf  yf"
    by (simp add: less_eq_lifted_pair.rep_eq sup_lifted_pair.rep_eq)
next
  fix xf yf zf :: "('a,'b) lifted_pair"
  assume 1: "yf  xf" and 2: "zf  xf"
  {
    fix f :: "('a,'b) phi"
    have 3: "triple (Rep_phi f)"
      by (simp add: triple_def)
    let ?x = "Rep_lifted_pair xf f"
    let ?y = "Rep_lifted_pair yf f"
    let ?z = "Rep_lifted_pair zf f"
    obtain x1 x2 y1 y2 z1 z2 where 4: "(x1,x2) = ?x  (y1,y2) = ?y  (z1,z2) = ?z"
      using prod.collapse by blast
    have "triple.pairs_less_eq ?y ?x  triple.pairs_less_eq ?z ?x"
      using 1 2 3 less_eq_lifted_pair.rep_eq by simp
    hence "triple.pairs_less_eq (triple.pairs_sup ?y ?z) ?x"
      using 3 4 by (metis (mono_tags, lifting) le_inf_iff sup.bounded_iff triple.pairs_sup.simps triple.pairs_less_eq.simps)
  }
  thus "yf  zf  xf"
    by (simp add: less_eq_lifted_pair.rep_eq sup_lifted_pair.rep_eq)
next
  fix xf :: "('a,'b) lifted_pair"
  {
    fix f :: "('a,'b) phi"
    have 1: "triple (Rep_phi f)"
      by (simp add: triple_def)
    let ?x = "Rep_lifted_pair xf f"
    obtain x1 x2 where "(x1,x2) = ?x"
      using prod.collapse by blast
    hence "triple.pairs_less_eq triple.pairs_bot ?x"
      using 1 by (metis bot.extremum top_greatest top_filter.abs_eq triple.pairs_less_eq.simps)
  }
  thus "bot  xf"
    by (simp add: less_eq_lifted_pair.rep_eq bot_lifted_pair.rep_eq)
next
  fix xf :: "('a,'b) lifted_pair"
  {
    fix f :: "('a,'b) phi"
    have 1: "triple (Rep_phi f)"
      by (simp add: triple_def)
    let ?x = "Rep_lifted_pair xf f"
    obtain x1 x2 where "(x1,x2) = ?x"
      using prod.collapse by blast
    hence "triple.pairs_less_eq ?x triple.pairs_top"
      using 1 by (metis top.extremum bot_least bot_filter.abs_eq triple.pairs_less_eq.simps)
  }
  thus "xf  top"
    by (simp add: less_eq_lifted_pair.rep_eq top_lifted_pair.rep_eq)
next
  fix xf yf zf :: "('a,'b) lifted_pair"
  {
    fix f :: "('a,'b) phi"
    have 1: "triple (Rep_phi f)"
      by (simp add: triple_def)
    let ?x = "Rep_lifted_pair xf f"
    let ?y = "Rep_lifted_pair yf f"
    let ?z = "Rep_lifted_pair zf f"
    obtain x1 x2 y1 y2 z1 z2 where "(x1,x2) = ?x  (y1,y2) = ?y  (z1,z2) = ?z"
      using prod.collapse by blast
    hence "triple.pairs_sup ?x (triple.pairs_inf ?y ?z) = triple.pairs_inf (triple.pairs_sup ?x ?y) (triple.pairs_sup ?x ?z)"
      using 1 by (metis (no_types) sup_inf_distrib1 inf_sup_distrib1 triple.pairs_sup.simps triple.pairs_inf.simps)
  }
  thus "xf  (yf  zf) = (xf  yf)  (xf  zf)"
    by (metis Rep_lifted_pair_inverse ext sup_lifted_pair.rep_eq inf_lifted_pair.rep_eq)
next
  fix xf yf :: "('a,'b) lifted_pair"
  {
    fix f :: "('a,'b) phi"
    have 1: "triple (Rep_phi f)"
      by (simp add: triple_def)
    let ?x = "Rep_lifted_pair xf f"
    let ?y = "Rep_lifted_pair yf f"
    obtain x1 x2 y1 y2 where 2: "(x1,x2) = ?x  (y1,y2) = ?y"
      using prod.collapse by blast
    have "?x  triple.pairs (Rep_phi f)  ?y  triple.pairs (Rep_phi f)"
      by simp
    hence "(triple.pairs_inf ?x ?y = triple.pairs_bot)  triple.pairs_less_eq ?x (triple.pairs_uminus (Rep_phi f) ?y)"
      using 1 2 by (metis triple.pairs_uminus_galois)
  }
  hence "f . (Rep_lifted_pair (xf  yf) f = Rep_lifted_pair bot f)  triple.pairs_less_eq (Rep_lifted_pair xf f) (Rep_lifted_pair (-yf) f)"
    using bot_lifted_pair.rep_eq inf_lifted_pair.rep_eq uminus_lifted_pair.rep_eq by simp
  hence "(Rep_lifted_pair (xf  yf) = Rep_lifted_pair bot)  xf  -yf"
    using less_eq_lifted_pair.rep_eq by auto
  thus "(xf  yf = bot)  (xf  -yf)"
    by (simp add: Rep_lifted_pair_inject)
next
  fix xf :: "('a,'b) lifted_pair"
  {
    fix f :: "('a,'b) phi"
    have 1: "triple (Rep_phi f)"
      by (simp add: triple_def)
    let ?x = "Rep_lifted_pair xf f"
    obtain x1 x2 where "(x1,x2) = ?x"
      using prod.collapse by blast
    hence "triple.pairs_sup (triple.pairs_uminus (Rep_phi f) ?x) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) ?x)) = triple.pairs_top"
      using 1 by (metis simp_lifted_pair triple.pairs_stone)
  }
  hence "Rep_lifted_pair (-xf  --xf) = Rep_lifted_pair top"
    using sup_lifted_pair.rep_eq uminus_lifted_pair.rep_eq top_lifted_pair.rep_eq by simp
  thus "-xf  --xf = top"
    by (simp add: Rep_lifted_pair_inject)
qed

end

subsection ‹The Stone Algebra of the Triple of a Stone Algebra›

text ‹
In this section we specialise the above construction to a particular structure map, namely the one obtained in the triple of a Stone algebra.
For this particular structure map (as well as for any other particular structure map) the resulting type is no longer a dependent type.
It is just the set of pairs obtained for the given structure map.
›

typedef (overloaded) 'a stone_phi_pair = "triple.pairs (stone_phi::'a::stone_algebra regular  'a dense_filter)"
  using stone_phi.pairs_bot_closed by auto

setup_lifting type_definition_stone_phi_pair

instantiation stone_phi_pair :: (stone_algebra) sup_inf_top_bot_uminus_ord
begin

lift_definition sup_stone_phi_pair :: "'a stone_phi_pair  'a stone_phi_pair  'a stone_phi_pair" is triple.pairs_sup
  using stone_phi.pairs_sup_closed by auto

lift_definition inf_stone_phi_pair :: "'a stone_phi_pair  'a stone_phi_pair  'a stone_phi_pair" is triple.pairs_inf
  using stone_phi.pairs_inf_closed by auto

lift_definition uminus_stone_phi_pair :: "'a stone_phi_pair  'a stone_phi_pair" is "triple.pairs_uminus stone_phi"
  using stone_phi.pairs_uminus_closed by auto

lift_definition bot_stone_phi_pair :: "'a stone_phi_pair" is "triple.pairs_bot"
  by (rule stone_phi.pairs_bot_closed)

lift_definition top_stone_phi_pair :: "'a stone_phi_pair" is "triple.pairs_top"
  by (rule stone_phi.pairs_top_closed)

lift_definition less_eq_stone_phi_pair :: "'a stone_phi_pair  'a stone_phi_pair  bool" is triple.pairs_less_eq .

lift_definition less_stone_phi_pair :: "'a stone_phi_pair  'a stone_phi_pair  bool" is triple.pairs_less .

instance ..

end

(*
instantiation stone_phi_pair :: (stone_algebra) stone_algebra
begin

instance
  apply intro_classes
  subgoal apply transfer by auto
  subgoal apply transfer by auto
  subgoal apply transfer by auto
  subgoal apply transfer by auto
  subgoal apply transfer by auto
  subgoal apply transfer by auto
  subgoal apply transfer by auto
  subgoal apply transfer by auto
  subgoal apply transfer by auto
  subgoal apply transfer by auto
  subgoal apply transfer by (metis (no_types, lifting) Pair_inject compl_bot_eq heyting.implies_order stone_phi.pairs_less_eq.elims(3) stone_phi.phi_top stone_phi.triple_axioms sup_top_left top_greatest triple_def)
  subgoal apply transfer by (metis (no_types, lifting) Pair_inject stone_phi.pairs_less_eq.elims(3) top.extremum bot_least bot_filter.abs_eq)
  subgoal apply transfer using stone_phi.triple_axioms triple.pairs_sup_dist_inf by fastforce
  subgoal apply transfer using stone_phi.pairs_uminus_galois by fastforce
  subgoal apply transfer using stone_phi.pairs_stone by fastforce
  done

end
*)

text ‹
The result is a Stone algebra and could be proved so by repeating and specialising the above proof for lifted pairs.
We choose a different approach, namely by embedding the type of pairs into the lifted type.
The embedding injects a pair x› into a function as the value at the given structure map; this makes the embedding injective.
The value of the function at any other structure map needs to be carefully chosen so that the resulting function is a Stone algebra homomorphism.
We use --x›, which is essentially a projection to the regular element component of x›, whence the image has the structure of a Boolean algebra.
›

fun stone_phi_embed :: "'a::non_trivial_stone_algebra stone_phi_pair  ('a regular,'a dense) lifted_pair"
  where "stone_phi_embed x = Abs_lifted_pair (λf . if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x)))"

text ‹
The following lemma shows that in both cases the value of the function is a valid pair for the given structure map.
›

lemma stone_phi_embed_triple_pair:
  "(if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x)))  triple.pairs (Rep_phi f)"
  by (metis (no_types, hide_lams) Rep_stone_phi_pair simp_phi surj_pair triple.pairs_uminus_closed triple_def)

text ‹
The following result shows that the embedding preserves the operations of Stone algebras.
Of course, it is not (yet) a Stone algebra homomorphism as we do not know (yet) that the domain of the embedding is a Stone algebra.
To establish the latter is the purpose of the embedding.
›

lemma stone_phi_embed_homomorphism:
  "sup_inf_top_bot_uminus_ord_homomorphism stone_phi_embed"
proof (intro conjI)
  let ?p = "λf . triple.pairs_uminus (Rep_phi f)"
  let ?pp = "λf x . ?p f (?p f x)"
  let ?q = "λf x . ?pp f (Rep_stone_phi_pair x)"
  show "x y::'a stone_phi_pair . stone_phi_embed (x  y) = stone_phi_embed x  stone_phi_embed y"
  proof (intro allI)
    fix x y :: "'a stone_phi_pair"
    have 1: "f . triple.pairs_sup (?q f x) (?q f y) = ?q f (x  y)"
    proof
      fix f :: "('a regular,'a dense) phi"
      let ?r = "Rep_phi f"
      obtain x1 x2 y1 y2 where 2: "(x1,x2) = Rep_stone_phi_pair x  (y1,y2) = Rep_stone_phi_pair y"
        using prod.collapse by blast
      hence "triple.pairs_sup (?q f x) (?q f y) = triple.pairs_sup (?pp f (x1,x2)) (?pp f (y1,y2))"
        by simp
      also have "... = triple.pairs_sup (--x1,?r (-x1)) (--y1,?r (-y1))"
        by (simp add: triple.pairs_uminus.simps triple_def)
      also have "... = (--x1  --y1,?r (-x1)  ?r (-y1))"
        by simp
      also have "... = (--(x1  y1),?r (-(x1  y1)))"
        by simp
      also have "... = ?pp f (x1  y1,x2  y2)"
        by (simp add: triple.pairs_uminus.simps triple_def)
      also have "... = ?pp f (triple.pairs_sup (x1,x2) (y1,y2))"
        by simp
      also have "... = ?q f (x  y)"
        using 2 by (simp add: sup_stone_phi_pair.rep_eq)
      finally show "triple.pairs_sup (?q f x) (?q f y) = ?q f (x  y)"
        .
    qed
    have "stone_phi_embed x  stone_phi_embed y = Abs_lifted_pair (λf . if Rep_phi f = stone_phi then Rep_stone_phi_pair x else ?q f x)  Abs_lifted_pair (λf . if Rep_phi f = stone_phi then Rep_stone_phi_pair y else ?q f y)"
      by simp
    also have "... = Abs_lifted_pair (λf . triple.pairs_sup (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else ?q f x) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else ?q f y))"
      by (rule sup_lifted_pair.abs_eq) (simp_all add: eq_onp_same_args stone_phi_embed_triple_pair)
    also have "... = Abs_lifted_pair (λf . if Rep_phi f = stone_phi then triple.pairs_sup (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else triple.pairs_sup (?q f x) (?q f y))"
      by (simp add: if_distrib_2)
    also have "... = Abs_lifted_pair (λf . if Rep_phi f = stone_phi then triple.pairs_sup (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else ?q f (x  y))"
      using 1 by meson
    also have "... = Abs_lifted_pair (λf . if Rep_phi f = stone_phi then Rep_stone_phi_pair (x  y) else ?q f (x  y))"
      by (metis sup_stone_phi_pair.rep_eq)
    also have "... = stone_phi_embed (x  y)"
      by simp
    finally show "stone_phi_embed (x  y) = stone_phi_embed x  stone_phi_embed y"
      by simp
  qed
next
  let ?p = "λf . triple.pairs_uminus (Rep_phi f)"
  let ?pp = "λf x . ?p f (?p f x)"
  let ?q = "λf x . ?pp f (Rep_stone_phi_pair x)"
  show "x y::'a stone_phi_pair . stone_phi_embed (x  y) = stone_phi_embed x  stone_phi_embed y"
  proof (intro allI)
    fix x y :: "'a stone_phi_pair"
    have 1: "f . triple.pairs_inf (?q f x) (?q f y) = ?q f (x  y)"
    proof
      fix f :: "('a regular,'a dense) phi"
      let ?r = "Rep_phi f"
      obtain x1 x2 y1 y2 where 2: "(x1,x2) = Rep_stone_phi_pair x  (y1,y2) = Rep_stone_phi_pair y"
        using prod.collapse by blast
      hence "triple.pairs_inf (?q f x) (?q f y) = triple.pairs_inf (?pp f (x1,x2)) (?pp f (y1,y2))"
        by simp
      also have "... = triple.pairs_inf (--x1,?r (-x1)) (--y1,?r (-y1))"
        by (simp add: triple.pairs_uminus.simps triple_def)
      also have "... = (--x1  --y1,?r (-x1)  ?r (-y1))"
        by simp
      also have "... = (--(x1  y1),?r (-(x1  y1)))"
        by simp
      also have "... = ?pp f (x1  y1,x2  y2)"
        by (simp add: triple.pairs_uminus.simps triple_def)
      also have "... = ?pp f (triple.pairs_inf (x1,x2) (y1,y2))"
        by simp
      also have "... = ?q f (x  y)"
        using 2 by (simp add: inf_stone_phi_pair.rep_eq)
      finally show "triple.pairs_inf (?q f x) (?q f y) = ?q f (x  y)"
        .
    qed
    have "stone_phi_embed x  stone_phi_embed y = Abs_lifted_pair (λf . if Rep_phi f = stone_phi then Rep_stone_phi_pair x else ?q f x)  Abs_lifted_pair (λf . if Rep_phi f = stone_phi then Rep_stone_phi_pair y else ?q f y)"
      by simp
    also have "... = Abs_lifted_pair (λf . triple.pairs_inf (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else ?q f x) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else ?q f y))"
      by (rule inf_lifted_pair.abs_eq) (simp_all add: eq_onp_same_args stone_phi_embed_triple_pair)
    also have "... = Abs_lifted_pair (λf . if Rep_phi f = stone_phi then triple.pairs_inf (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else triple.pairs_inf (?q f x) (?q f y))"
      by (simp add: if_distrib_2)
    also have "... = Abs_lifted_pair (λf . if Rep_phi f = stone_phi then triple.pairs_inf (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else ?q f (x  y))"
      using 1 by meson
    also have "... = Abs_lifted_pair (λf . if Rep_phi f = stone_phi then Rep_stone_phi_pair (x  y) else ?q f (x  y))"
      by (metis inf_stone_phi_pair.rep_eq)
    also have "... = stone_phi_embed (x  y)"
      by simp
    finally show "stone_phi_embed (x  y) = stone_phi_embed x  stone_phi_embed y"
      by simp
  qed
next
  have "stone_phi_embed (top::'a stone_phi_pair) = Abs_lifted_pair (λf . if Rep_phi f = stone_phi then Rep_stone_phi_pair top else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair top)))"
    by simp
  also have "... = Abs_lifted_pair (λf . if Rep_phi f = stone_phi then (top,bot) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (top,bot)))"
    by (metis (no_types, hide_lams) bot_filter.abs_eq top_stone_phi_pair.rep_eq)
  also have "... = Abs_lifted_pair (λf . if Rep_phi f = stone_phi then (top,bot) else triple.pairs_uminus (Rep_phi f) (bot,top))"
    by (metis (no_types, hide_lams) dense_closed_top simp_phi triple.pairs_uminus.simps triple_def)
  also have "... = Abs_lifted_pair (λf . if Rep_phi f = stone_phi then (top,bot) else (top,bot))"
    by (metis (no_types, hide_lams) p_bot simp_phi triple.pairs_uminus.simps triple_def)
  also have "... = Abs_lifted_pair (λf . (top,Abs_filter {top}))"
    by (simp add: bot_filter.abs_eq)
  also have "... = top"
    by (rule top_lifted_pair.abs_eq[THEN sym])
  finally show "stone_phi_embed (top::'a stone_phi_pair) = top"
    .
next
  have "stone_phi_embed (bot::'a stone_phi_pair) = Abs_lifted_pair (λf . if Rep_phi f = stone_phi then Rep_stone_phi_pair bot else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair bot)))"
    by simp
  also have "... = Abs_lifted_pair (λf . if Rep_phi f = stone_phi then (bot,top) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (bot,top)))"
    by (metis (no_types, hide_lams) top_filter.abs_eq bot_stone_phi_pair.rep_eq)
  also have "... = Abs_lifted_pair (λf . if Rep_phi f = stone_phi then (bot,top) else triple.pairs_uminus (Rep_phi f) (top,bot))"
    by (metis (no_types, hide_lams) p_bot simp_phi triple.pairs_uminus.simps triple_def)
  also have "... = Abs_lifted_pair (λf . if Rep_phi f = stone_phi then (bot,top) else (bot,top))"
    by (metis (no_types, hide_lams) p_top simp_phi triple.pairs_uminus.simps triple_def)
  also have "... = Abs_lifted_pair (λf . (bot,Abs_filter UNIV))"
    by (simp add: top_filter.abs_eq)
  also have "... = bot"
    by (rule bot_lifted_pair.abs_eq[THEN sym])
  finally show "stone_phi_embed (bot::'a stone_phi_pair) = bot"
    .
next
  let ?p = "λf . triple.pairs_uminus (Rep_phi f)"
  let ?pp = "λf x . ?p f (?p f x)"
  let ?q = "λf x . ?pp f (Rep_stone_phi_pair x)"
  show "x::'a stone_phi_pair . stone_phi_embed (-x) = -stone_phi_embed x"
  proof (intro allI)
    fix x :: "'a stone_phi_pair"
    have 1: "f . triple.pairs_uminus (Rep_phi f) (?q f x) = ?q f (-x)"
    proof
      fix f :: "('a regular,'a dense) phi"
      let ?r = "Rep_phi f"
      obtain x1 x2 where 2: "(x1,x2) = Rep_stone_phi_pair x"
        using prod.collapse by blast
      hence "triple.pairs_uminus (Rep_phi f) (?q f x) = triple.pairs_uminus (Rep_phi f) (?pp f (x1,x2))"
        by simp
      also have "... = triple.pairs_uminus (Rep_phi f) (--x1,?r (-x1))"
        by (simp add: triple.pairs_uminus.simps triple_def)
      also have "... = (---x1,?r (--x1))"
        by (simp add: triple.pairs_uminus.simps triple_def)
      also have "... = ?pp f (-x1,stone_phi x1)"
        by (simp add: triple.pairs_uminus.simps triple_def)
      also have "... = ?pp f (triple.pairs_uminus stone_phi (x1,x2))"
        by simp
      also have "... = ?q f (-x)"
        using 2 by (simp add: uminus_stone_phi_pair.rep_eq)
      finally show "triple.pairs_uminus (Rep_phi f) (?q f x) = ?q f (-x)"
        .
    qed
    have "-stone_phi_embed x = -Abs_lifted_pair (λf . if Rep_phi f = stone_phi then Rep_stone_phi_pair x else ?q f x)"
      by simp
    also have "... = Abs_lifted_pair (λf . triple.pairs_uminus (Rep_phi f) (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else ?q f x))"
      by (rule uminus_lifted_pair.abs_eq) (simp_all add: eq_onp_same_args stone_phi_embed_triple_pair)
    also have "... = Abs_lifted_pair (λf . if Rep_phi f = stone_phi then triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x) else triple.pairs_uminus (Rep_phi f) (?q f x))"
      by (simp add: if_distrib)
    also have "... = Abs_lifted_pair (λf . if Rep_phi f = stone_phi then triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x) else ?q f (-x))"
      using 1 by meson
    also have "... = Abs_lifted_pair (λf . if Rep_phi f = stone_phi then Rep_stone_phi_pair (-x) else ?q f (-x))"
      by (metis uminus_stone_phi_pair.rep_eq)
    also have "... = stone_phi_embed (-x)"
      by simp
    finally show "stone_phi_embed (-x) = -stone_phi_embed x"
      by simp
  qed
next
  let ?p = "λf . triple.pairs_uminus (Rep_phi f)"
  let ?pp = "λf x . ?p f (?p f x)"
  let ?q = "λf x . ?pp f (Rep_stone_phi_pair x)"
  show "x y::'a stone_phi_pair . x  y  stone_phi_embed x  stone_phi_embed y"
  proof (intro allI, rule impI)
    fix x y :: "'a stone_phi_pair"
    assume 1: "x  y"
    have "f . triple.pairs_less_eq (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else ?q f x) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else ?q f y)"
    proof
      fix f :: "('a regular,'a dense) phi"
      let ?r = "Rep_phi f"
      obtain x1 x2 y1 y2 where 2: "(x1,x2) = Rep_stone_phi_pair x  (y1,y2) = Rep_stone_phi_pair y"
        using prod.collapse by blast
      have "x1  y1"
        using 1 2 by (metis less_eq_stone_phi_pair.rep_eq stone_phi.pairs_less_eq.simps)
      hence "--x1  --y1  ?r (-y1)  ?r (-x1)"
        by (metis compl_le_compl_iff le_iff_sup simp_phi)
      hence "triple.pairs_less_eq (--x1,?r (-x1)) (--y1,?r (-y1))"
        by simp
      hence "triple.pairs_less_eq (?pp f (x1,x2)) (?pp f (y1,y2))"
        by (simp add: triple.pairs_uminus.simps triple_def)
      hence "triple.pairs_less_eq (?q f x) (?q f y)"
        using 2 by simp
      hence "if ?r = stone_phi then triple.pairs_less_eq (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else triple.pairs_less_eq (?q f x) (?q f y)"
        using 1 by (simp add: less_eq_stone_phi_pair.rep_eq)
      thus "triple.pairs_less_eq (if ?r = stone_phi then Rep_stone_phi_pair x else ?q f x) (if ?r = stone_phi then Rep_stone_phi_pair y else ?q f y)"
        by (simp add: if_distrib_2)
    qed
    hence "Abs_lifted_pair (λf . if Rep_phi f = stone_phi then Rep_stone_phi_pair x else ?q f x)  Abs_lifted_pair (λf . if Rep_phi f = stone_phi then Rep_stone_phi_pair y else ?q f y)"
      by (subst less_eq_lifted_pair.abs_eq) (simp_all add: eq_onp_same_args stone_phi_embed_triple_pair)
    thus "stone_phi_embed x  stone_phi_embed y"
      by simp
  qed
qed

text ‹
The following lemmas show that the embedding is injective and reflects the order.
The latter allows us to easily inherit properties involving inequalities from the target of the embedding, without transforming them to equations.
›

lemma stone_phi_embed_injective:
  "inj stone_phi_embed"
proof (rule injI)
  fix x y :: "'a stone_phi_pair"
  have 1: "Rep_phi (Abs_phi stone_phi) = stone_phi"
    by (simp add: Abs_phi_inverse stone_phi.hom)
  assume 2: "stone_phi_embed x = stone_phi_embed y"
  have "x::'a stone_phi_pair . Rep_lifted_pair (stone_phi_embed x) = (λf . if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x)))"
    by (simp add: Abs_lifted_pair_inverse stone_phi_embed_triple_pair)
  hence "(λf . if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = (λf . if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))"
    using 2 by metis
  hence "Rep_stone_phi_pair x = Rep_stone_phi_pair y"
    using 1 by metis
  thus "x = y"
    by (simp add: Rep_stone_phi_pair_inject)
qed

lemma stone_phi_embed_order_injective:
  assumes "stone_phi_embed x  stone_phi_embed y"
    shows "x  y"
proof -
  let ?f = "Abs_phi stone_phi"
  have "f . triple.pairs_less_eq (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))"
    using assms by (subst less_eq_lifted_pair.abs_eq[THEN sym]) (simp_all add: eq_onp_same_args stone_phi_embed_triple_pair)
  hence "triple.pairs_less_eq (if Rep_phi ?f = (stone_phi::'a regular  'a dense_filter) then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi ?f) (triple.pairs_uminus (Rep_phi ?f) (Rep_stone_phi_pair x))) (if Rep_phi ?f = (stone_phi::'a regular  'a dense_filter) then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi ?f) (triple.pairs_uminus (Rep_phi ?f) (Rep_stone_phi_pair y)))"
    by simp
  hence "triple.pairs_less_eq (Rep_stone_phi_pair x) (Rep_stone_phi_pair y)"
    by (simp add: Abs_phi_inverse stone_phi.hom)
  thus "x  y"
    by (simp add: less_eq_stone_phi_pair.rep_eq)
qed

lemma stone_phi_embed_strict_order_isomorphism:
  "x < y  stone_phi_embed x < stone_phi_embed y"
  by (smt less_eq_stone_phi_pair.rep_eq less_le_not_le less_stone_phi_pair.rep_eq stone_phi.pairs_less.elims(2,3) stone_phi_embed_homomorphism stone_phi_embed_order_injective)

text ‹
Now all Stone algebra axioms can be inherited using the embedding.
This is due to the fact that the axioms are universally quantified equations or conditional equations (or inequalities); this is called a quasivariety in universal algebra.
It would be useful to have this construction available for arbitrary quasivarieties.
›

instantiation stone_phi_pair :: (non_trivial_stone_algebra) stone_algebra
begin

instance
  apply intro_classes
  apply (metis (mono_tags, lifting) stone_phi_embed_homomorphism stone_phi_embed_strict_order_isomorphism stone_phi_embed_order_injective less_le_not_le)
  apply (simp add: stone_phi_embed_order_injective)
  apply (meson order.trans stone_phi_embed_homomorphism stone_phi_embed_order_injective)
  apply (meson stone_phi_embed_homomorphism antisym stone_phi_embed_injective injD)
  apply (metis inf.sup_ge1 stone_phi_embed_homomorphism stone_phi_embed_order_injective)
  apply (metis inf.sup_ge2 stone_phi_embed_homomorphism stone_phi_embed_order_injective)
  apply (metis inf_greatest stone_phi_embed_homomorphism stone_phi_embed_order_injective)
  apply (metis stone_phi_embed_homomorphism stone_phi_embed_order_injective sup_ge1)
  apply (metis stone_phi_embed_homomorphism stone_phi_embed_order_injective sup.cobounded2)
  apply (metis stone_phi_embed_homomorphism stone_phi_embed_order_injective sup_least)
  apply (metis bot.extremum stone_phi_embed_homomorphism stone_phi_embed_order_injective)
  apply (metis stone_phi_embed_homomorphism stone_phi_embed_order_injective top_greatest)
  apply (metis (mono_tags, lifting) stone_phi_embed_homomorphism sup_inf_distrib1 stone_phi_embed_injective injD)
  apply (metis stone_phi_embed_homomorphism stone_phi_embed_injective injD stone_phi_embed_order_injective pseudo_complement)
  by (metis injD stone_phi_embed_homomorphism stone_phi_embed_injective stone)

end

subsection ‹Stone Algebra Isomorphism›

text ‹
In this section we prove that the Stone algebra of the triple of a Stone algebra is isomorphic to the original Stone algebra.
The following two definitions give the isomorphism.
›

abbreviation sa_iso_inv :: "'a::non_trivial_stone_algebra stone_phi_pair  'a"
  where "sa_iso_inv  λp . Rep_regular (fst (Rep_stone_phi_pair p))  Rep_dense (triple.rho_pair stone_phi (Rep_stone_phi_pair p))"

abbreviation sa_iso :: "'a::non_trivial_stone_algebra  'a stone_phi_pair"
  where "sa_iso  λx . Abs_stone_phi_pair (Abs_regular (--x),stone_phi (Abs_regular (-x))  up_filter (Abs_dense (x  -x)))"

lemma sa_iso_triple_pair:
  "(Abs_regular (--x),stone_phi (Abs_regular (-x))  up_filter (Abs_dense (x  -x)))  triple.pairs stone_phi"
  by (metis (mono_tags, lifting) double_compl eq_onp_same_args stone_phi.sa_iso_pair uminus_regular.abs_eq)

lemma stone_phi_inf_dense:
  "stone_phi (Abs_regular (-x))  up_filter (Abs_dense (y  -y))  up_filter (Abs_dense (y  -y  x))"
proof -
  have "Rep_filter (stone_phi (Abs_regular (-x))  up_filter (Abs_dense (y  -y)))  (Abs_dense (y  -y  x))"
  proof
    fix z :: "'a dense"
    let ?r = "Rep_dense z"
    assume "z  Rep_filter (stone_phi (Abs_regular (-x))  up_filter (Abs_dense (y  -y)))"
    also have "... = Rep_filter (stone_phi (Abs_regular (-x)))  Rep_filter (up_filter (Abs_dense (y  -y)))"
      by (simp add: inf_filter.rep_eq)
    also have "... = stone_phi_base (Abs_regular (-x))  (Abs_dense (y  -y))"
      by (metis Abs_filter_inverse mem_Collect_eq up_filter stone_phi_base_filter stone_phi_def)
    finally have "--x  ?r  Abs_dense (y  -y)  z"
      by (metis (mono_tags, lifting) Abs_regular_inverse Int_Collect mem_Collect_eq)
    hence "--x  ?r  y  -y  ?r"
      by (simp add: Abs_dense_inverse less_eq_dense.rep_eq)
    hence "y  -y  x  ?r"
      using order_trans pp_increasing by auto
    hence "Abs_dense (y  -y  x)  Abs_dense ?r"
      by (subst less_eq_dense.abs_eq) (simp_all add: eq_onp_same_args)
    thus "z  (Abs_dense (y  -y  x))"
      by (simp add: Rep_dense_inverse)
  qed
  hence "Abs_filter (Rep_filter (stone_phi (Abs_regular (-x))  up_filter (Abs_dense (y  -y))))  up_filter (Abs_dense (y  -y  x))"
    by (simp add: eq_onp_same_args less_eq_filter.abs_eq)
  thus ?thesis
    by (simp add: Rep_filter_inverse)
qed

lemma stone_phi_complement:
  "complement (stone_phi (Abs_regular (-x))) (stone_phi (Abs_regular (--x)))"
  by (metis (mono_tags, lifting) eq_onp_same_args stone_phi.phi_complemented uminus_regular.abs_eq)

lemma up_dense_stone_phi:
  "up_filter (Abs_dense (x  -x))  stone_phi (Abs_regular (--x))"
proof -
  have "(Abs_dense (x  -x))  stone_phi_base (Abs_regular (--x))"
  proof
    fix z :: "'a dense"
    let ?r = "Rep_dense z"
    assume "z  (Abs_dense (x  -x))"
    hence "---x  ?r"
      by (simp add: Abs_dense_inverse less_eq_dense.rep_eq)
    hence "-Rep_regular (Abs_regular (--x))  ?r"
      by (metis (mono_tags, lifting) Abs_regular_inverse mem_Collect_eq)
    thus "z  stone_phi_base (Abs_regular (--x))"
      by simp
  qed
  thus ?thesis
    by (unfold stone_phi_def, subst less_eq_filter.abs_eq, simp_all add: eq_onp_same_args stone_phi_base_filter)
qed

text ‹
The following two results prove that the isomorphisms are mutually inverse.
›

lemma sa_iso_left_invertible:
  "sa_iso_inv (sa_iso x) = x"
proof -
  have "up_filter (triple.rho_pair stone_phi (Abs_regular (--x),stone_phi (Abs_regular (-x))  up_filter (Abs_dense (x  -x)))) = stone_phi (Abs_regular (--x))  (stone_phi (Abs_regular (-x))  up_filter (Abs_dense (x  -x)))"
    using sa_iso_triple_pair stone_phi.get_rho_pair_char by blast
  also have "... = stone_phi (Abs_regular (--x))  up_filter (Abs_dense (x  -x))"
    by (simp add: inf.sup_commute inf_sup_distrib1 stone_phi_complement)
  also have "... = up_filter (Abs_dense (x  -x))"
    using up_dense_stone_phi inf.absorb2 by auto
  finally have 1: "triple.rho_pair stone_phi (Abs_regular (--x),stone_phi (Abs_regular (-x))  up_filter (Abs_dense (x  -x))) = Abs_dense (x  -x)"
    using up_filter_injective by auto
  have "sa_iso_inv (sa_iso x) = (λp . Rep_regular (fst p)  Rep_dense (triple.rho_pair stone_phi p)) (Abs_regular (--x),stone_phi (Abs_regular (-x))  up_filter (Abs_dense (x  -x)))"
    by (simp add: Abs_stone_phi_pair_inverse sa_iso_triple_pair)
  also have "... = Rep_regular (Abs_regular (--x))  Rep_dense (triple.rho_pair stone_phi (Abs_regular (--x),stone_phi (Abs_regular (-x))  up_filter (Abs_dense (x  -x))))"
    by simp
  also have "... = --x  Rep_dense (Abs_dense (x  -x))"
    using 1 by (subst Abs_regular_inverse) auto
  also have "... = --x  (x  -x)"
    by (subst Abs_dense_inverse) simp_all
  also have "... = x"
    by simp
  finally show ?thesis
    by auto
qed

lemma sa_iso_right_invertible:
  "sa_iso (sa_iso_inv p) = p"
proof -
  obtain x y where 1: "(x,y) = Rep_stone_phi_pair p"
    using prod.collapse by blast
  hence 2: "(x,y)  triple.pairs stone_phi"
    by (simp add: Rep_stone_phi_pair)
  hence 3: "stone_phi (-x)  y"
    by (simp add: stone_phi.pairs_phi_less_eq)
  have 4: "z . z  Rep_filter (stone_phi x  y)  -Rep_regular x  Rep_dense z"
  proof (rule allI, rule impI)
    fix z :: "'a dense"
    let ?r = "Rep_dense z"
    assume "z  Rep_filter (stone_phi x  y)"
    hence "z  Rep_filter (stone_phi x)"
      by (simp add: inf_filter.rep_eq)
    also have "... = stone_phi_base x"
      by (simp add: stone_phi_def Abs_filter_inverse stone_phi_base_filter)
    finally show "-Rep_regular x  ?r"
      by simp
  qed
  have "triple.rho_pair stone_phi (x,y)  (triple.rho_pair stone_phi (x,y))"
    by simp
  also have "... = Rep_filter (Abs_filter ((triple.rho_pair stone_phi (x,y))))"
    by (simp add: Abs_filter_inverse)
  also have "... = Rep_filter (stone_phi x  y)"
    using 2 stone_phi.get_rho_pair_char by fastforce
  finally have "triple.rho_pair stone_phi (x,y)  Rep_filter (stone_phi x  y)"
    by simp
  hence 5: "-Rep_regular x  Rep_dense (triple.rho_pair stone_phi (x,y))"
    using 4 by simp
  have 6: "sa_iso_inv p = Rep_regular x  Rep_dense (triple.rho_pair stone_phi (x,y))"
    using 1 by (metis fstI)
  hence "-sa_iso_inv p = -Rep_regular x"
    by simp
  hence "sa_iso (sa_iso_inv p) = Abs_stone_phi_pair (Abs_regular (--Rep_regular x),stone_phi (Abs_regular (-Rep_regular x))  up_filter (Abs_dense ((Rep_regular x  Rep_dense (triple.rho_pair stone_phi (x,y)))  -Rep_regular x)))"
    using 6 by simp
  also have "... = Abs_stone_phi_pair (x,stone_phi (-x)  up_filter (Abs_dense ((Rep_regular x  Rep_dense (triple.rho_pair stone_phi (x,y)))  -Rep_regular x)))"
    by (metis (mono_tags, lifting) Rep_regular_inverse double_compl uminus_regular.rep_eq)
  also have "... = Abs_stone_phi_pair (x,stone_phi (-x)  up_filter (Abs_dense (Rep_dense (triple.rho_pair stone_phi (x,y))  -Rep_regular x)))"
    by (metis inf_sup_aci(5) maddux_3_21_pp simp_regular)
  also have "... = Abs_stone_phi_pair (x,stone_phi (-x)  up_filter (Abs_dense (Rep_dense (triple.rho_pair stone_phi (x,y)))))"
    using 5 by (simp add: sup.absorb1)
  also have "... = Abs_stone_phi_pair (x,stone_phi (-x)  up_filter (triple.rho_pair stone_phi (x,y)))"
    by (simp add: Rep_dense_inverse)
  also have "... = Abs_stone_phi_pair (x,stone_phi (-x)  (stone_phi x  y))"
    using 2 stone_phi.get_rho_pair_char by fastforce
  also have "... = Abs_stone_phi_pair (x,stone_phi (-x)  y)"
    by (simp add: stone_phi.phi_complemented sup.commute sup_inf_distrib1)
  also have "... = Abs_stone_phi_pair (x,y)"
    using 3 by (simp add: le_iff_sup)
  also have "... = p"
    using 1 by (simp add: Rep_stone_phi_pair_inverse)
  finally show ?thesis
    .
qed

text ‹
It remains to show the homomorphism properties, which is done in the following result.
›

lemma sa_iso:
  "stone_algebra_isomorphism sa_iso"
proof (intro conjI)
  have "Abs_stone_phi_pair (Abs_regular (--bot),stone_phi (Abs_regular (-bot))  up_filter (Abs_dense (bot  -bot))) = Abs_stone_phi_pair (bot,stone_phi top  up_filter top)"
    by (simp add: bot_regular.abs_eq top_regular.abs_eq top_dense.abs_eq)
  also have "... = Abs_stone_phi_pair (bot,stone_phi top)"
    by (simp add: stone_phi.hom)
  also have "... = bot"
    by (simp add: bot_stone_phi_pair_def stone_phi.phi_top)
  finally show "sa_iso bot = bot"
    .
next
  have "Abs_stone_phi_pair (Abs_regular (--top),stone_phi (Abs_regular (-top))  up_filter (Abs_dense (top  -top))) = Abs_stone_phi_pair (top,stone_phi bot  up_filter top)"
    by (simp add: bot_regular.abs_eq top_regular.abs_eq top_dense.abs_eq)
  also have "... = top"
    by (simp add: stone_phi.phi_bot top_stone_phi_pair_def)
  finally show "sa_iso top = top"
    .
next
  have 1: "x y::'a . dense (x  -x  y)"
    by simp
  have 2: "x y::'a . up_filter (Abs_dense (x  -x  y))  (stone_phi (Abs_regular (-x))  up_filter (Abs_dense (x  -x)))  (stone_phi (Abs_regular (-y))  up_filter (Abs_dense (y  -y)))"
  proof (intro allI)
    fix x y :: 'a
    let ?u = "Abs_dense (x  -x  --y)"
    let ?v = "Abs_dense (y  -y)"
    have "(Abs_dense (x  -x  y))  Rep_filter (stone_phi (Abs_regular (-y))  up_filter ?v)"
    proof
      fix z
      assume "z  (Abs_dense (x  -x  y))"
      hence "Abs_dense (x  -x  y)  z"
        by simp
      hence 3: "x  -x  y  Rep_dense z"
        by (simp add: Abs_dense_inverse less_eq_dense.rep_eq)
      have "y  x  -x  --y"
        by (simp add: le_supI2 pp_increasing)
      hence "(x  -x  --y)  (y  -y) = y  ((x  -x  --y)  -y)"
        by (simp add: le_iff_sup sup_inf_distrib1)
      also have "... = y  ((x  -x)  -y)"
        by (simp add: inf_commute inf_sup_distrib1)
      also have "...  Rep_dense z"
        using 3 by (meson le_infI1 sup.bounded_iff)
      finally have "Abs_dense ((x  -x  --y)  (y  -y))  z"
        by (simp add: Abs_dense_inverse less_eq_dense.rep_eq)
      hence 4: "?u  ?v  z"
        by (simp add: eq_onp_same_args inf_dense.abs_eq)
      have "-Rep_regular (Abs_regular (-y)) = --y"
        by (metis (mono_tags, lifting) mem_Collect_eq Abs_regular_inverse)
      also have "...  Rep_dense ?u"
        by (simp add: Abs_dense_inverse)
      finally have "?u  stone_phi_base (Abs_regular (-y))"
        by simp
      hence 5: "?u  Rep_filter (stone_phi (Abs_regular (-y)))"
        by (metis mem_Collect_eq stone_phi_def stone_phi_base_filter Abs_filter_inverse)
      have "?v  ?v"
        by simp
      hence "?v  Rep_filter (up_filter ?v)"
        by (metis Abs_filter_inverse mem_Collect_eq up_filter)
      thus "z  Rep_filter (stone_phi (Abs_regular (-y))  up_filter ?v)"
        using 4 5 sup_filter.rep_eq filter_sup_def by blast
    qed
    hence "up_filter (Abs_dense (x  -x  y))  Abs_filter (Rep_filter (stone_phi (Abs_regular (-y))  up_filter ?v))"
      by (simp add: eq_onp_same_args less_eq_filter.abs_eq)
    also have "... = stone_phi (Abs_regular (-y))  up_filter ?v"
      by (simp add: Rep_filter_inverse)
    finally show "up_filter (Abs_dense (x  -x  y))  (stone_phi (Abs_regular (-x))  up_filter (Abs_dense (x  -x)))  (stone_phi (Abs_regular (-y))  up_filter (Abs_dense (y  -y)))"
      by (metis le_infI le_supI2 sup_bot.right_neutral up_filter_dense_antitone)
  qed
  have 6: "x::'a . in_p_image (-x)"
    by auto
  show "x y::'a . sa_iso (x  y) = sa_iso x  sa_iso y"
  proof (intro allI)
    fix x y :: 'a
    have 7: "up_filter (Abs_dense (x  -x))  up_filter (Abs_dense (y  -y))  up_filter (Abs_dense (y  -y  x))"
    proof -
      have "up_filter (Abs_dense (x  -x))  up_filter (Abs_dense (y  -y)) = up_filter (Abs_dense (x  -x)  Abs_dense (y  -y))"
        by (metis up_filter_dist_sup)
      also have "... = up_filter (Abs_dense (x  -x  (y  -y)))"
        by (subst sup_dense.abs_eq) (simp_all add: eq_onp_same_args)
      also have "... = up_filter (Abs_dense (y  -y  x  -x))"
        by (simp add: sup_commute sup_left_commute)
      also have "...  up_filter (Abs_dense (y  -y  x))"
        using up_filter_dense_antitone by auto
      finally show ?thesis
        .
    qed
    have "Abs_dense (x  y  -(x  y)) = Abs_dense ((x  -x  y)  (y  -y  x))"
      by (simp add: sup_commute sup_inf_distrib1 sup_left_commute)
    also have "... = Abs_dense (x  -x  y)  Abs_dense (y  -y  x)"
      using 1 by (metis (mono_tags, lifting) Abs_dense_inverse Rep_dense_inverse inf_dense.rep_eq mem_Collect_eq)
    finally have 8: "up_filter (Abs_dense (x  y  -(x  y))) = up_filter (Abs_dense (x  -x  y))  up_filter (Abs_dense (y  -y  x))"
      by (simp add: up_filter_dist_inf)
    also have "...  (stone_phi (Abs_regular (-x))  up_filter (Abs_dense (x  -x)))  (stone_phi (Abs_regular (-y))  up_filter (Abs_dense (y  -y)))"
      using 2 by (simp add: inf.sup_commute le_sup_iff)
    finally have 9: "(stone_phi (Abs_regular (-x))  stone_phi (Abs_regular (-y)))  up_filter (Abs_dense (x  y  -(x  y)))  ..."
      by (simp add: le_supI1)
    have "... = (stone_phi (Abs_regular (-x))  stone_phi (Abs_regular (-y)))  (stone_phi (Abs_regular (-x))  up_filter (Abs_dense (y  -y)))  ((up_filter (Abs_dense (x  -x))  stone_phi (Abs_regular (-y)))  (up_filter (Abs_dense (x  -x))  up_filter (Abs_dense (y  -y))))"
      by (metis (no_types) inf_sup_distrib1 inf_sup_distrib2)
    also have "...  (stone_phi (Abs_regular (-x))  stone_phi (Abs_regular (-y)))  up_filter (Abs_dense (y  -y  x))  ((up_filter (Abs_dense (x  -x))  stone_phi (Abs_regular (-y)))  (up_filter (Abs_dense (x  -x))  up_filter (Abs_dense (y  -y))))"
      by (meson sup_left_isotone sup_right_isotone stone_phi_inf_dense)
    also have "...  (stone_phi (Abs_regular (-x))  stone_phi (Abs_regular (-y)))  up_filter (Abs_dense (y  -y  x))  (up_filter (Abs_dense (x  -x  y))  (up_filter (Abs_dense (x  -x))  up_filter (Abs_dense (y  -y))))"
      by (metis inf.commute sup_left_isotone sup_right_isotone stone_phi_inf_dense)
    also have "...  (stone_phi (Abs_regular (-x))  stone_phi (Abs_regular (-y)))  up_filter (Abs_dense (y  -y  x))  up_filter (Abs_dense (x  -x  y))"
      using 7 by (simp add: sup.absorb1 sup_commute sup_left_commute)
    also have "... = (stone_phi (Abs_regular (-x))  stone_phi (Abs_regular (-y)))  up_filter (Abs_dense (x  y  -(x  y)))"
      using 8 by (simp add: sup.commute sup.left_commute)
    finally have "(stone_phi (Abs_regular (-x))  up_filter (Abs_dense (x  -x)))  (stone_phi (Abs_regular (-y))  up_filter (Abs_dense (y  -y))) = ..."
      using 9 using antisym by blast
    also have "... = stone_phi (Abs_regular (-x)  Abs_regular (-y))  up_filter (Abs_dense (x  y  -(x  y)))"
      by (simp add: stone_phi.hom)
    also have "... = stone_phi (Abs_regular (-(x  y)))  up_filter (Abs_dense (x  y  -(x  y)))"
      using 6 by (subst inf_regular.abs_eq) (simp_all add: eq_onp_same_args)
    finally have 10: "stone_phi (Abs_regular (-(x  y)))  up_filter (Abs_dense (x  y  -(x  y))) = (stone_phi (Abs_regular (-x))  up_filter (Abs_dense (x  -x)))  (stone_phi (Abs_regular (-y))  up_filter (Abs_dense (y  -y)))"
      by simp
    have "Abs_regular (--(x  y)) = Abs_regular (--x)  Abs_regular (--y)"
      using 6 by (subst sup_regular.abs_eq) (simp_all add: eq_onp_same_args)
    hence "Abs_stone_phi_pair (Abs_regular (--(x  y)),stone_phi (Abs_regular (-(x  y)))  up_filter (Abs_dense (x  y  -(x  y)))) = Abs_stone_phi_pair (triple.pairs_sup (Abs_regular (--x),stone_phi (Abs_regular (-x))  up_filter (Abs_dense (x  -x))) (Abs_regular (--y),stone_phi (Abs_regular (-y))  up_filter (Abs_dense (y  -y))))"
      using 10 by auto
    also have "... = Abs_stone_phi_pair (Abs_regular (--x),stone_phi (Abs_regular (-x))  up_filter (Abs_dense (x  -x)))  Abs_stone_phi_pair (Abs_regular (--y),stone_phi (Abs_regular (-y))  up_filter (Abs_dense (y  -y)))"
      by (rule sup_stone_phi_pair.abs_eq[THEN sym]) (simp_all add: eq_onp_same_args sa_iso_triple_pair)
    finally show "sa_iso (x  y) = sa_iso x  sa_iso y"
      .
  qed
next
  have 1: "x y::'a . dense (x  -x  y)"
    by simp
  have 2: "x::'a . in_p_image (-x)"
    by auto
  have 3: "x y::'a . stone_phi (Abs_regular (-y))  up_filter (Abs_dense (x  -x)) = stone_phi (Abs_regular (-y))  up_filter (Abs_dense (x  -x  -y))"
  proof (intro allI)
    fix x y :: 'a
    have 4: "up_filter (Abs_dense (x  -x))  stone_phi (Abs_regular (-y))  up_filter (Abs_dense (x  -x  -y))"
      by (metis (no_types, lifting) complement_shunting stone_phi_inf_dense stone_phi_complement complement_symmetric)
    have "up_filter (Abs_dense (x  -x  -y))  up_filter (Abs_dense (x  -x))"
      by (metis sup_idem up_filter_dense_antitone)
    thus "stone_phi (Abs_regular (-y))  up_filter (Abs_dense (x  -x)) = stone_phi (Abs_regular (-y))  up_filter (Abs_dense (x  -x  -y))"
      using 4 by (simp add: le_iff_sup sup_commute sup_left_commute)
  qed
  show "x y::'a . sa_iso (x  y) = sa_iso x  sa_iso y"
  proof (intro allI)
    fix x y :: 'a
    have "Abs_dense ((x  y)  -(x  y)) = Abs_dense ((x  -x  -y)  (y  -y  -x))"
      by (simp add: sup_commute sup_inf_distrib1 sup_left_commute)
    also have "... = Abs_dense (x  -x  -y)  Abs_dense (y  -y  -x)"
      using 1 by (metis (mono_tags, lifting) Abs_dense_inverse Rep_dense_inverse inf_dense.rep_eq mem_Collect_eq)
    finally have 5: "up_filter (Abs_dense ((x  y)  -(x  y))) = up_filter (Abs_dense (x  -x  -y))  up_filter (Abs_dense (y  -y  -x))"
      by (simp add: up_filter_dist_inf)
    have "(stone_phi (Abs_regular (-x))  up_filter (Abs_dense (x  -x)))  (stone_phi (Abs_regular (-y))  up_filter (Abs_dense (y  -y))) = (stone_phi (Abs_regular (-y))  up_filter (Abs_dense (x  -x)))  (stone_phi (Abs_regular (-x))  up_filter (Abs_dense (y  -y)))"
      by (simp add: inf_sup_aci(6) sup_left_commute)
    also have "... = (stone_phi (Abs_regular (-y))  up_filter (Abs_dense (x  -x  -y)))  (stone_phi (Abs_regular (-x))  up_filter (Abs_dense (y  -y  -x)))"
      using 3 by simp
    also have "... = (stone_phi (Abs_regular (-x))  stone_phi (Abs_regular (-y)))  (up_filter (Abs_dense (x  -x  -y))  up_filter (Abs_dense (y  -y  -x)))"
      by (simp add: inf_sup_aci(6) sup_left_commute)
    also have "... = (stone_phi (Abs_regular (-x))  stone_phi (Abs_regular (-y)))  up_filter (Abs_dense ((x  y)  -(x  y)))"
      using 5 by (simp add: sup.commute sup.left_commute)
    finally have "(stone_phi (Abs_regular (-x))  up_filter (Abs_dense (x  -x)))  (stone_phi (Abs_regular (-y))  up_filter (Abs_dense (y  -y))) = ..."
      by simp
    also have "... = stone_phi (Abs_regular (-x)  Abs_regular (-y))  up_filter (Abs_dense ((x  y)  -(x  y)))"
      by (simp add: stone_phi.hom)
    also have "... = stone_phi (Abs_regular (-(x  y)))  up_filter (Abs_dense ((x  y)  -(x  y)))"
      using 2 by (subst sup_regular.abs_eq) (simp_all add: eq_onp_same_args)
    finally have 6: "stone_phi (Abs_regular (-(x  y)))  up_filter (Abs_dense ((x  y)  -(x  y))) = (stone_phi (Abs_regular (-x))  up_filter (Abs_dense (x  -x)))  (stone_phi (Abs_regular (-y))  up_filter (Abs_dense (y  -y)))"
      by simp
    have "Abs_regular (--(x  y)) = Abs_regular (--x)  Abs_regular (--y)"
      using 2 by (subst inf_regular.abs_eq) (simp_all add: eq_onp_same_args)
    hence "Abs_stone_phi_pair (Abs_regular (--(x  y)),stone_phi (Abs_regular (-(x  y)))  up_filter (Abs_dense ((x  y)  -(x  y)))) = Abs_stone_phi_pair (triple.pairs_inf (Abs_regular (--x),stone_phi (Abs_regular (-x))  up_filter (Abs_dense (x  -x))) (Abs_regular (--y),stone_phi (Abs_regular (-y))  up_filter (Abs_dense (y  -y))))"
      using 6 by auto
    also have "... = Abs_stone_phi_pair (Abs_regular (--x),stone_phi (Abs_regular (-x))  up_filter (Abs_dense (x  -x)))  Abs_stone_phi_pair (Abs_regular (--y),stone_phi (Abs_regular (-y))  up_filter (Abs_dense (y  -y)))"
      by (rule inf_stone_phi_pair.abs_eq[THEN sym]) (simp_all add: eq_onp_same_args sa_iso_triple_pair)
    finally show "sa_iso (x  y) = sa_iso x  sa_iso y"
      .
  qed
next
  show "x::'a . sa_iso (-x) = -sa_iso x"
  proof
    fix x :: 'a
    have "sa_iso (-x) = Abs_stone_phi_pair (Abs_regular (---x),stone_phi (Abs_regular (--x))  up_filter top)"
      by (simp add: top_dense_def)
    also have "... = Abs_stone_phi_pair (Abs_regular (---x),stone_phi (Abs_regular (--x)))"
      by (metis bot_filter.abs_eq sup_bot.right_neutral up_top)
    also have "... = Abs_stone_phi_pair (triple.pairs_uminus stone_phi (Abs_regular (--x),stone_phi (Abs_regular (-x))  up_filter (Abs_dense (x  -x))))"
      by (subst uminus_regular.abs_eq[THEN sym], unfold eq_onp_same_args) auto
    also have "... = -sa_iso x"
      by (simp add: eq_onp_def sa_iso_triple_pair uminus_stone_phi_pair.abs_eq)
    finally show "sa_iso (-x) = -sa_iso x"
      by simp
  qed
next
  show "bij sa_iso"
    by (metis (mono_tags, lifting) sa_iso_left_invertible sa_iso_right_invertible invertible_bij[where g=sa_iso_inv])
qed

subsection ‹Triple Isomorphism›

text ‹
In this section we prove that the triple of the Stone algebra of a triple is isomorphic to the original triple.
The notion of isomorphism for triples is described in \cite{ChenGraetzer1969}.
It amounts to an isomorphism of Boolean algebras, an isomorphism of distributive lattices with a greatest element, and a commuting diagram involving the structure maps.
›

subsubsection ‹Boolean Algebra Isomorphism›

text ‹
We first define and prove the isomorphism of Boolean algebras.
Because the Stone algebra of a triple is implemented as a lifted pair, we also lift the Boolean algebra.
›

typedef (overloaded) ('a,'b) lifted_boolean_algebra = "{ xf::('a::non_trivial_boolean_algebra,'b::distrib_lattice_top) phi  'a . True }"
  by simp

setup_lifting type_definition_lifted_boolean_algebra

instantiation lifted_boolean_algebra :: (non_trivial_boolean_algebra,distrib_lattice_top) boolean_algebra
begin

lift_definition sup_lifted_boolean_algebra :: "('a,'b) lifted_boolean_algebra  ('a,'b) lifted_boolean_algebra  ('a,'b) lifted_boolean_algebra" is "λxf yf f . sup (xf f) (yf f)"