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

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

notation uminus ("- _"  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"

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 "∀x∈s . ∀y∈s . f x ≤ f y ∨ f y ≤ f x"
shows "∃m∈s . ∀z∈s . 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"

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

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"

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"
also have "... ≤ y ⊔ (w ⊓ x)"
using 1 sup.commute sup.left_commute inf_sup_distrib2 sup_right_divisibility by fastforce
also have "... ≤ w ⊔ y"
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"
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 (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"
hence "x ⊔ y = y"
by (metis injD bij_is_inj assms(2))
thus "x ≤ y"
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"

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"

lemma pp_inf_p:
"--x ⊓ -x = bot"
by simp

text ‹
The double complement is a closure operation.
›

lemma pp_increasing:
"x ≤ --x"
using inf_p pseudo_complement by blast

lemma ppp [simp]:
"---x = -x"
by (metis order.antisym inf.commute order_trans pseudo_complement pp_increasing)

lemma pp_idempotent:
"----x = --x"
by simp

lemma regular_in_p_image_iff:
"regular x ⟷ in_p_image x"
by auto

lemma pseudo_complement_pp:
"x ⊓ y = bot ⟷ --x ≤ -y"
by (metis inf_commute pseudo_complement ppp)

lemma p_antitone:
"x ≤ y ⟹ -y ≤ -x"
by (metis inf_commute order_trans pseudo_complement pp_increasing)

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

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

lemma p_antitone_iff:
"x ≤ -y ⟷ y ≤ -x"
using order_lesseq_imp p_antitone pp_increasing by blast

lemma pp_isotone:
"x ≤ y ⟹ --x ≤ --y"

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

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

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

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

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

lemma pp_dist_pp_sup [simp]:
"--(--x ⊔ --y) = --(x ⊔ y)"
by simp

lemma p_sup_p [simp]:
"-(x ⊔ -x) = bot"
by simp

lemma pp_sup_p [simp]:
"--(x ⊔ -x) = top"
by simp

lemma dense_pp:
"dense x ⟷ --x = top"
by (metis p_bot p_top ppp)

lemma dense_sup_p:
"dense (x ⊔ -x)"
by simp

lemma regular_char:
"regular x ⟷ (∃y . x = -y)"
by auto

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

text ‹
Weak forms of the shunting property hold.
Most require a pseudocomplemented element on the right-hand side.
›

lemma p_shunting_swap:
"x ⊓ y ≤ -z ⟷ x ⊓ z ≤ -y"
by (metis inf_assoc inf_commute pseudo_complement)

lemma pp_inf_below_iff:
"x ⊓ y ≤ -z ⟷ --x ⊓ y ≤ -z"

lemma p_inf_pp [simp]:
"-(x ⊓ --y) = -(x ⊓ y)"
apply (rule order.antisym)
apply (simp add: inf.coboundedI2 p_antitone pp_increasing)
using inf_commute p_antitone_iff pp_inf_below_iff by auto

lemma p_inf_pp_pp [simp]:
"-(--x ⊓ --y) = -(x ⊓ y)"

lemma regular_closed_inf:
"regular x ⟹ regular y ⟹ regular (x ⊓ y)"
by (metis p_dist_sup ppp)

lemma regular_closed_p:
"regular (-x)"
by simp

lemma regular_closed_pp:
"regular (--x)"
by simp

lemma regular_closed_bot:
"regular bot"
by simp

lemma regular_closed_top:
"regular top"
by simp

lemma pp_dist_inf [simp]:
"--(x ⊓ y) = --x ⊓ --y"
by (metis p_dist_sup p_inf_pp_pp ppp)

lemma inf_import_p [simp]:
"x ⊓ -(x ⊓ y) = x ⊓ -y"
apply (rule order.antisym)
using p_shunting_swap apply fastforce
using inf.sup_right_isotone p_antitone by auto

text ‹
Pseudocomplements are unique.
›

lemma p_unique:
"(∀x . x ⊓ y = bot ⟷ x ≤ z) ⟹ z = -y"
using inf.order_eq_iff pseudo_complement by auto

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

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

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

lemma inf_pp_semi_commute:
"x ⊓ --y ≤ --(x ⊓ y)"
using inf.eq_refl p_antitone_iff p_inf_pp by presburger

lemma inf_pp_commute:
"--(--x ⊓ y) = --x ⊓ --y"
by simp

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

lemma regular_sup:
"regular z ⟹ (x ≤ z ∧ y ≤ z ⟷ --(x ⊔ y) ≤ z)"
apply (rule iffI)
apply (metis le_supI pp_isotone)
using dual_order.trans sup_ge2 pp_increasing pp_isotone_sup by blast

lemma dense_closed_inf:
"dense x ⟹ dense y ⟹ dense (x ⊓ y)"

lemma dense_closed_sup:
"dense x ⟹ dense y ⟹ dense (x ⊔ y)"
by simp

lemma dense_closed_pp:
"dense x ⟹ dense (--x)"
by simp

lemma dense_closed_top:
"dense top"
by simp

lemma dense_up_closed:
"dense x ⟹ x ≤ y ⟹ dense y"
using dense_pp top_le pp_isotone by auto

lemma regular_dense_top:
"regular x ⟹ dense x ⟹ x = top"
using p_bot by blast

lemma selection_char:
"selection s x ⟷ (∃y . s = -y ⊓ x)"
by (metis inf_import_p inf_commute regular_closed_p)

lemma selection_closed_inf:
"selection s x ⟹ selection t x ⟹ selection (s ⊓ t) x"
by (metis inf_assoc inf_commute inf_idem pp_dist_inf)

lemma selection_closed_pp:
"regular x ⟹ selection s x ⟹ selection (--s) x"
by (metis pp_dist_inf)

lemma selection_closed_bot:
"selection bot x"
by simp

lemma selection_closed_id:
"selection x x"
using inf.le_iff_sup pp_increasing by auto

text ‹
Conjugates are usually studied for Boolean algebras, however, some of their properties generalise to pseudocomplemented algebras.
›

lemma conjugate_unique_p:
assumes "conjugate f g"
and "conjugate f h"
shows "uminus ∘ g = uminus ∘ h"
proof -
have "∀x y . x ⊓ g y = bot ⟷ x ⊓ h y = bot"
using assms conjugate_def inf.commute by simp
hence "∀x y . x ≤ -(g y) ⟷ x ≤ -(h y)"
using inf.commute pseudo_complement by simp
hence "∀y . -(g y) = -(h y)"
using order.eq_iff by blast
thus ?thesis
by auto
qed

lemma conjugate_symmetric:
"conjugate f g ⟹ conjugate g f"

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

assumes "conjugate f g"
proof -
have 1: "∀x y z . -z ≤ -(f (x ⊔ y)) ⟷ -z ≤ -(f x) ∧ -z ≤ -(f y)"
proof (intro allI)
fix x y z
have "(-z ≤ -(f (x ⊔ y))) = (f (x ⊔ y) ⊓ -z = bot)"
also have "... = ((x ⊔ y) ⊓ g(-z) = bot)"
using assms conjugate_def by auto
also have "... = (x ⊔ y ≤ -(g(-z)))"
also have "... = (x ≤ -(g(-z)) ∧ y ≤ -(g(-z)))"
also have "... = (x ⊓ g(-z) = bot ∧ y ⊓ g(-z) = bot)"
also have "... = (f x ⊓ -z = bot ∧ f y ⊓ -z = bot)"
using assms conjugate_def by auto
also have "... = (-z ≤ -(f x) ∧ -z ≤ -(f y))"
finally show "-z ≤ -(f (x ⊔ y)) ⟷ -z ≤ -(f x) ∧ -z ≤ -(f y)"
by simp
qed
have "∀x y . -(f (x ⊔ y)) = -(f x) ⊓ -(f y)"
proof (intro allI)
fix x y
have "-(f x) ⊓ -(f y) = --(-(f x) ⊓ -(f y))"
by simp
hence "-(f x) ⊓ -(f y) ≤ -(f (x ⊔ y))"
using 1 by (metis inf_le1 inf_le2)
thus "-(f (x ⊔ y)) = -(f x) ⊓ -(f y)"
using 1 order.antisym by fastforce
qed
thus ?thesis
qed

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

lemma conjugate_char_1_pp:
"conjugate f g ⟷ (∀x y . f(x ⊓ -(g y)) ≤ --f x ⊓ -y ∧ g(y ⊓ -(f x)) ≤ --g y ⊓ -x)"
proof
assume 1: "conjugate f g"
show "∀x y . f(x ⊓ -(g y)) ≤ --f x ⊓ -y ∧ g(y ⊓ -(f x)) ≤ --g y ⊓ -x"
proof (intro allI)
fix x y
have 2: "f(x ⊓ -(g y)) ≤ -y"
using 1 by (simp add: conjugate_def pseudo_complement)
have "f(x ⊓ -(g y)) ≤ --f(x ⊓ -(g y))"
also have "... ≤ --f x"
using 1 conjugate_isotone_pp isotone_def by simp
finally have 3: "f(x ⊓ -(g y)) ≤ --f x ⊓ -y"
using 2 by simp
have 4: "isotone (uminus ∘ uminus ∘ g)"
using 1 conjugate_isotone_pp conjugate_symmetric by auto
have 5: "g(y ⊓ -(f x)) ≤ -x"
using 1 by (metis conjugate_def inf.cobounded2 inf_commute pseudo_complement)
have "g(y ⊓ -(f x)) ≤ --g(y ⊓ -(f x))"
also have "... ≤ --g y"
using 4 isotone_def by auto
finally have "g(y ⊓ -(f x)) ≤ --g y ⊓ -x"
using 5 by simp
thus "f(x ⊓ -(g y)) ≤ --f x ⊓ -y ∧ g(y ⊓ -(f x)) ≤ --g y ⊓ -x"
using 3 by simp
qed
next
assume 6: "∀x y . f(x ⊓ -(g y)) ≤ --f x ⊓ -y ∧ g(y ⊓ -(f x)) ≤ --g y ⊓ -x"
hence 7: "∀x y . f x ⊓ y = bot ⟶ x ⊓ g y = bot"
by (metis inf.le_iff_sup inf.le_sup_iff inf_commute pseudo_complement)
have "∀x y . x ⊓ g y = bot ⟶ f x ⊓ y = bot"
using 6 by (metis inf.le_iff_sup inf.le_sup_iff inf_commute pseudo_complement)
thus "conjugate f g"
using 7 conjugate_def by auto
qed

lemma conjugate_char_1_isotone:
"conjugate f g ⟹ isotone f ⟹ isotone g ⟹ f(x ⊓ -(g y)) ≤ f x ⊓ -y ∧ g(y ⊓ -(f x)) ≤ g y ⊓ -x"

lemma dense_lattice_char_1:
"(∀x y . x ⊓ y = bot ⟶ x = bot ∨ y = bot) ⟷ (∀x . x ≠ bot ⟶ dense x)"
by (metis inf_top.left_neutral p_bot p_inf pp_inf_bot_iff)

lemma dense_lattice_char_2:
"(∀x y . x ⊓ y = bot ⟶ x = bot ∨ y = bot) ⟷ (∀x . regular x ⟶ x = bot ∨ x = top)"
by (metis dense_lattice_char_1 inf_top.left_neutral p_inf regular_closed_p regular_closed_top)

lemma restrict_below_Rep_eq:
"x ⊓ --y ≤ z ⟹ x ⊓ y = x ⊓ z ⊓ y"
by (metis inf.absorb2 inf.commute inf.left_commute pp_increasing)

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

end

text ‹
The following class gives equational axioms for the pseudocomplement operation.
›

class p_algebra_eq = bounded_lattice + uminus +
assumes p_bot_eq: "-bot = top"
and p_top_eq: "-top = bot"
and inf_import_p_eq: "x ⊓ -(x ⊓ y) = x ⊓ -y"
begin

lemma inf_p_eq:
"x ⊓ -x = bot"
by (metis inf_bot_right inf_import_p_eq inf_top_right p_top_eq)

subclass p_algebra
apply unfold_locales
apply (rule iffI)
apply (metis inf.orderI inf_import_p_eq inf_top.right_neutral p_bot_eq)
by (metis (full_types) inf.left_commute inf.orderE inf_bot_right inf_commute inf_p_eq)

end

subsubsection ‹Pseudocomplemented Distributive Lattices›

text ‹
We obtain further properties if we assume that the lattice operations are distributive.
›

class pd_algebra = p_algebra + bounded_distrib_lattice
begin

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

lemma pp_inf_sup_p [simp]:
"--x ⊓ (x ⊔ -x) = x"
using inf.absorb2 inf_sup_distrib1 pp_increasing by auto

lemma complement_p:
"x ⊓ y = bot ⟹ x ⊔ y = top ⟹ -x = y"
by (metis pseudo_complement inf.commute inf_top.left_neutral sup.absorb_iff1 sup.commute sup_bot.right_neutral sup_inf_distrib2 p_inf)

lemma complemented_regular:
"complemented x ⟹ regular x"
using complement_p inf.commute sup.commute by fastforce

lemma regular_inf_dense:
"∃y z . regular y ∧ dense z ∧ x = y ⊓ z"
by (metis pp_inf_sup_p dense_sup_p ppp)

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

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

"((v ⊓ w) ⊔ (-v ⊓ x)) ⊓ -((v ⊓ y) ⊔ (-v ⊓ z)) = (v ⊓ w ⊓ -y) ⊔ (-v ⊓ x ⊓ -z)"
proof -
have "v ⊓ w ⊓ -(v ⊓ y) ⊓ -(-v ⊓ z) = v ⊓ w ⊓ -(v ⊓ y)"
by (meson inf.cobounded1 inf_absorb1 le_infI1 p_antitone_iff)
also have "... = v ⊓ w ⊓ -y"
using inf.sup_relative_same_increasing inf_import_p inf_le1 by blast
finally have 1: "v ⊓ w ⊓ -(v ⊓ y) ⊓ -(-v ⊓ z) = v ⊓ w ⊓ -y"
.
have "-v ⊓ x ⊓ -(v ⊓ y) ⊓ -(-v ⊓ z) = -v ⊓ x ⊓ -(-v ⊓ z)"
by (simp add: inf.absorb1 le_infI1 p_antitone_inf)
also have "... = -v ⊓ x ⊓ -z"
finally have 2: "-v ⊓ x ⊓ -(v ⊓ y) ⊓ -(-v ⊓ z) = -v ⊓ x ⊓ -z"
.
have "((v ⊓ w) ⊔ (-v ⊓ x)) ⊓ -((v ⊓ y) ⊔ (-v ⊓ z)) = (v ⊓ w ⊓ -(v ⊓ y) ⊓ -(-v ⊓ z)) ⊔ (-v ⊓ x ⊓ -(v ⊓ y) ⊓ -(-v ⊓ z))"
also have "... = (v ⊓ w ⊓ -y) ⊔ (-v ⊓ x ⊓ -z)"
using 1 2 by simp
finally show ?thesis
.
qed

lemma order_char_1:
"x ≤ y ⟷ x ≤ y ⊔ -x"
by (metis inf.sup_left_isotone inf_sup_absorb le_supI1 maddux_3_12 sup_commute)

lemma order_char_2:
"x ≤ y ⟷ x ⊔ -x ≤ y ⊔ -x"
using order_char_1 by auto

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

end

subsection ‹Stone Algebras›

text ‹
A Stone algebra is a distributive lattice with a pseudocomplement that satisfies the following equation.
We thus obtain the other half of the requirements of a complement at least for the regular elements.
›

class stone_algebra = pd_algebra +
assumes stone [simp]: "-x ⊔ --x = top"
begin

text ‹
As a consequence, we obtain both De Morgan's laws for all elements.
›

lemma p_dist_inf [simp]:
"-(x ⊓ y) = -x ⊔ -y"
proof (rule p_unique[THEN sym], rule allI, rule iffI)
fix w
assume "w ⊓ (x ⊓ y) = bot"
hence "w ⊓ --x ⊓ y = bot"
using inf_commute inf_left_commute pseudo_complement by auto
hence 1: "w ⊓ --x ≤ -y"
have "w = (w ⊓ -x) ⊔ (w ⊓ --x)"
using distrib_imp2 sup_inf_distrib1 by auto
thus "w ≤ -x ⊔ -y"
using 1 by (metis inf_le2 sup.mono)
next
fix w
assume "w ≤ -x ⊔ -y"
thus "w ⊓ (x ⊓ y) = bot"
using order_trans p_supdist_inf pseudo_complement by blast
qed

lemma pp_dist_sup [simp]:
"--(x ⊔ y) = --x ⊔ --y"
by simp

lemma regular_closed_sup:
"regular x ⟹ regular y ⟹ regular (x ⊔ y)"
by simp

text ‹
The regular elements are precisely the ones having a complement.
›

lemma regular_complemented_iff:
"regular x ⟷ complemented x"
by (metis inf_p stone complemented_regular)

lemma selection_closed_sup:
"selection s x ⟹ selection t x ⟹ selection (s ⊔ t) x"

lemma huntington_3_pp [simp]:
"-(-x ⊔ -y) ⊔ -(-x ⊔ y) = --x"
by (metis p_dist_inf p_inf sup.commute sup_bot_left sup_inf_distrib1)

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

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

"(-x ⊓ y) ⊔ (--x ⊓ z) = (--x ⊔ y) ⊓ (-x ⊔ z)"
proof -
have "(--x ⊔ y) ⊓ (-x ⊔ z) = (--x ⊓ z) ⊔ (y ⊓ -x) ⊔ (y ⊓ z)"
by (simp add: inf.commute inf_sup_distrib1 sup.assoc)
also have "... = (--x ⊓ z) ⊔ (y ⊓ -x) ⊔ (y ⊓ z ⊓ (-x ⊔ --x))"
by simp
also have "... = (--x ⊓ z) ⊔ ((y ⊓ -x) ⊔ (y ⊓ -x ⊓ z)) ⊔ (y ⊓ z ⊓ --x)"
using inf_sup_distrib1 sup_assoc inf_commute inf_assoc by presburger
also have "... = (--x ⊓ z) ⊔ (y ⊓ -x) ⊔ (y ⊓ z ⊓ --x)"
by simp
also have "... = ((--x ⊓ z) ⊔ (--x ⊓ z ⊓ y)) ⊔ (y ⊓ -x)"
by (simp add: inf_assoc inf_commute sup.left_commute sup_commute)
also have "... = (--x ⊓ z) ⊔ (y ⊓ -x)"
by simp
finally show ?thesis
qed

lemma compl_inter_eq_pp:
"--x ⊓ y = --x ⊓ z ⟹ -x ⊓ y = -x ⊓ z ⟹ y = z"
by (metis inf_commute inf_p inf_sup_distrib1 inf_top.right_neutral p_bot p_dist_inf)

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

lemma shunting_2_pp:
"x ≤ --y ⟷ -x ⊔ --y = top"
by (metis inf_top_left p_bot p_dist_inf pseudo_complement)

lemma shunting_p:
"x ⊓ y ≤ -z ⟷ x ≤ -z ⊔ -y"
by (metis inf.assoc p_dist_inf p_shunting_swap pseudo_complement)

text ‹
The following weak shunting property is interesting as it does not require the element ‹z› on the right-hand side to be regular.
›

lemma shunting_var_p:
"x ⊓ -y ≤ z ⟷ x ≤ z ⊔ --y"
proof
assume "x ⊓ -y ≤ z"
hence "z ⊔ --y = --y ⊔ (z ⊔ x ⊓ -y)"
thus "x ≤ z ⊔ --y"
by (metis inf_commute maddux_3_21_pp sup.commute sup.left_commute sup_left_divisibility)
next
assume "x ≤ z ⊔ --y"
thus "x ⊓ -y ≤ z"
qed

(* Whether conjugate_char_2_pp can be proved in pd_algebra or in p_algebra is unknown. *)
lemma conjugate_char_2_pp:
"conjugate f g ⟷ f bot = bot ∧ g bot = bot ∧ (∀x y . f x ⊓ y ≤ --(f(x ⊓ --(g y))) ∧ g y ⊓ x ≤ --(g(y ⊓ --(f x))))"
proof
assume 1: "conjugate f g"
hence 2: "dual_additive (uminus ∘ g)"
show "f bot = bot ∧ g bot = bot ∧ (∀x y . f x ⊓ y ≤ --(f(x ⊓ --(g y))) ∧ g y ⊓ x ≤ --(g(y ⊓ --(f x))))"
proof (intro conjI)
show "f bot = bot"
using 1 by (metis conjugate_def inf_idem inf_bot_left)
next
show "g bot = bot"
using 1 by (metis conjugate_def inf_idem inf_bot_right)
next
show "∀x y . f x ⊓ y ≤ --(f(x ⊓ --(g y))) ∧ g y ⊓ x ≤ --(g(y ⊓ --(f x)))"
proof (intro allI)
fix x y
have 3: "y ≤ -(f(x ⊓ -(g y)))"
using 1 by (simp add: conjugate_def pseudo_complement inf_commute)
have 4: "x ≤ -(g(y ⊓ -(f x)))"
using 1 conjugate_def inf.commute pseudo_complement by fastforce
have "y ⊓ -(f(x ⊓ --(g y))) = y ⊓ -(f(x ⊓ -(g y))) ⊓ -(f(x ⊓ --(g y)))"
using 3 by (simp add: inf.le_iff_sup inf_commute)
also have "... = y ⊓ -(f((x ⊓ -(g y)) ⊔ (x ⊓ --(g y))))"
also have "... = y ⊓ -(f x)"
also have "... ≤ -(f x)"
by simp
finally have 5: "f x ⊓ y ≤ --(f(x ⊓ --(g y)))"
have "x ⊓ -(g(y ⊓ --(f x))) = x ⊓ -(g(y ⊓ -(f x))) ⊓ -(g(y ⊓ --(f x)))"
using 4 by (simp add: inf.le_iff_sup inf_commute)
also have "... = x ⊓ -(g((y ⊓ -(f x)) ⊔ (y ⊓ --(f x))))"
also have "... = x ⊓ -(g y)"
also have "... ≤ -(g y)"
by simp
finally have "g y ⊓ x ≤ --(g(y ⊓ --(f x)))"
thus "f x ⊓ y ≤ --(f(x ⊓ --(g y))) ∧ g y ⊓ x ≤ --(g(y ⊓ --(f x)))"
using 5 by simp
qed
qed
next
assume "f bot = bot ∧ g bot = bot ∧ (∀x y . f x ⊓ y ≤ --(f(x ⊓ --(g y))) ∧ g y ⊓ x ≤ --(g(y ⊓ --(f x))))"
thus "conjugate f g"
by (unfold conjugate_def, metis inf_commute le_bot pp_inf_bot_iff regular_closed_bot)
qed

assumes "conjugate f g"
shows "f x ⊓ y ≤ f(x ⊓ --(g y)) ∧ g y ⊓ x ≤ g(y ⊓ --(f x))"
proof -
have "f x ⊓ y = f ((x ⊓ --g y) ⊔ (x ⊓ -g y)) ⊓ y"
also have "... = (f (x ⊓ --g y) ⊓ y) ⊔ (f (x ⊓ -g y) ⊓ y)"
using assms(2) additive_def inf_sup_distrib2 by auto
also have "... = f (x ⊓ --g y) ⊓ y"
by (metis assms(1) conjugate_def inf_le2 pseudo_complement sup_bot.right_neutral)
finally have 2: "f x ⊓ y ≤ f (x ⊓ --g y)"
by simp
have "g y ⊓ x = g ((y ⊓ --f x) ⊔ (y ⊓ -f x)) ⊓ x"
also have "... = (g (y ⊓ --f x) ⊓ x) ⊔ (g (y ⊓ -f x) ⊓ x)"
using assms(3) additive_def inf_sup_distrib2 by auto
also have "... = g (y ⊓ --f x) ⊓ x"
by (metis assms(1) conjugate_def inf.cobounded2 pseudo_complement sup_bot.right_neutral inf_commute)
finally have "g y ⊓ x ≤ g (y ⊓ --f x)"
by simp
thus ?thesis
using 2 by simp
qed

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

end

abbreviation stone_algebra_isomorphism :: "('a::stone_algebra ⇒ 'b::stone_algebra) ⇒ bool"
where "stone_algebra_isomorphism f ≡ sup_inf_top_bot_uminus_isomorphism f"

text ‹
Every bounded linear order can be expanded to a Stone algebra.
The pseudocomplement takes ‹bot› to the ‹top› and every other element to ‹bot›.
›

class linorder_stone_algebra_expansion = linorder_lattice_expansion + uminus +
assumes uminus_def [simp]: "-x = (if x = bot then top else bot)"
begin

subclass stone_algebra
apply unfold_locales
using bot_unique min_def top_le by auto

text ‹
The regular elements are the least and greatest elements.
All elements except the least element are dense.
›

lemma regular_bot_top:
"regular x ⟷ x = bot ∨ x = top"
by simp

lemma not_bot_dense:
"x ≠ bot ⟹ --x = top"
by simp

end

subsection ‹Heyting Algebras›

text ‹
In this section we add a relative pseudocomplement operation to semilattices and to lattices.
›

subsubsection ‹Heyting Semilattices›

text ‹
The pseudocomplement of an element ‹y› relative to an element ‹z› is the least element whose meet with ‹y› is below ‹z›.
This can be stated as a Galois connection.
Specialising ‹z = bot› gives (non-relative) pseudocomplements.
Many properties can already be shown if the underlying structure is just a semilattice.
›

class implies =
fixes implies :: "'a ⇒ 'a ⇒ 'a" (infixl "↝" 65)

class heyting_semilattice = semilattice_inf + implies +
assumes implies_galois: "x ⊓ y ≤ z ⟷ x ≤ y ↝ z"
begin

lemma implies_below_eq [simp]:
"y ⊓ (x ↝ y) = y"
using implies_galois inf.absorb_iff1 inf.cobounded1 by blast

lemma implies_increasing:
"x ≤ y ↝ x"

lemma implies_galois_swap:
"x ≤ y ↝ z ⟷ y ≤ x ↝ z"
by (metis implies_galois inf_commute)

lemma implies_galois_var:
"x ⊓ y ≤ z ⟷ y ≤ x ↝ z"

lemma implies_galois_increasing:
"x ≤ y ↝ (x ⊓ y)"
using implies_galois by blast

lemma implies_galois_decreasing:
"(y ↝ x) ⊓ y ≤ x"
using implies_galois by blast

lemma implies_mp_below:
"x ⊓ (x ↝ y) ≤ y"
using implies_galois_decreasing inf_commute by auto

lemma implies_isotone:
"x ≤ y ⟹ z ↝ x ≤ z ↝ y"
using implies_galois order_trans by blast

lemma implies_antitone:
"x ≤ y ⟹ y ↝ z ≤ x ↝ z"
by (meson implies_galois_swap order_lesseq_imp)

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

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

lemma implies_curry:
"x ↝ (y ↝ z) = (x ⊓ y) ↝ z"
by (metis implies_galois_decreasing implies_galois inf_assoc order.antisym)

lemma implies_curry_flip:
"x ↝ (y ↝ z) = y ↝ (x ↝ z)"

lemma triple_implies [simp]:
"((x ↝ y) ↝ y) ↝ y = x ↝ y"
using implies_antitone implies_galois_swap order.eq_iff by auto

lemma implies_mp_eq [simp]:
"x ⊓ (x ↝ y) = x ⊓ y"
by (metis implies_below_eq implies_mp_below inf_left_commute inf.absorb2)

lemma implies_dist_implies:
"x ↝ (y ↝ z) ≤ (x ↝ y) ↝ (x ↝ z)"
using implies_curry implies_curry_flip by auto

lemma implies_import_inf [simp]:
"x ⊓ ((x ⊓ y) ↝ (x ↝ z)) = x ⊓ (y ↝ z)"
by (metis implies_curry implies_mp_eq inf_commute)

lemma implies_dist_inf:
"x ↝ (y ⊓ z) = (x ↝ y) ⊓ (x ↝ z)"
proof -
have "(x ↝ y) ⊓ (x ↝ z) ⊓ x ≤ y ⊓ z"
hence "(x ↝ y) ⊓ (x ↝ z) ≤ x ↝ (y ⊓ z)"
using implies_galois by blast
thus ?thesis
qed

lemma implies_itself_top:
"y ≤ x ↝ x"

lemma inf_implies_top:
"z ≤ (x ⊓ y) ↝ x"
using implies_galois_var le_infI1 by blast

lemma inf_inf_implies [simp]:
"z ⊓ ((x ⊓ y) ↝ x) = z"

lemma le_implies_top:
"x ≤ y ⟹ z ≤ x ↝ y"
using implies_antitone implies_itself_top order.trans by blast

lemma le_iff_le_implies:
"x ≤ y ⟷ x ≤ x ↝ y"
using implies_galois inf_idem by force

lemma implies_inf_isotone:
"x ↝ y ≤ (x ⊓ z) ↝ (y ⊓ z)"
by (metis implies_curry implies_galois_increasing implies_isotone)

lemma implies_transitive:
"(x ↝ y) ⊓ (y ↝ z) ≤ x ↝ z"
using implies_dist_implies implies_galois_var implies_increasing order_lesseq_imp by blast

lemma implies_inf_absorb [simp]:
"x ↝ (x ⊓ y) = x ↝ y"
using implies_dist_inf implies_itself_top inf.absorb_iff2 by auto

lemma implies_implies_absorb [simp]:
"x ↝ (x ↝ y) = x ↝ y"

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

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

end

text ‹
The following class gives equational axioms for the relative pseudocomplement operation (inequalities can be written as equations).
›

class heyting_semilattice_eq = semilattice_inf + implies +
assumes implies_mp_below: "x ⊓ (x ↝ y) ≤ y"
and implies_galois_increasing: "x ≤ y ↝ (x ⊓ y)"
and implies_isotone_inf: "x ↝ (y ⊓ z) ≤ x ↝ y"
begin

subclass heyting_semilattice
apply unfold_locales
apply (rule iffI)
apply (metis implies_galois_increasing implies_isotone_inf inf.absorb2 order_lesseq_imp)
by (metis implies_mp_below inf_commute order_trans inf_mono order_refl)

end

text ‹
The following class allows us to explicitly give the pseudocomplement of an element relative to itself.
›

class bounded_heyting_semilattice = bounded_semilattice_inf_top + heyting_semilattice
begin

lemma implies_itself [simp]:
"x ↝ x = top"
using implies_galois inf_le2 top_le by blast

lemma implies_order:
"x ≤ y ⟷ x ↝ y = top"
by (metis implies_galois inf_top.left_neutral top_unique)

lemma inf_implies [simp]:
"(x ⊓ y) ↝ x = top"
using implies_order inf_le1 by blast

lemma top_implies [simp]:
"top ↝ x = x"
by (metis implies_mp_eq inf_top.left_neutral)

end

subsubsection ‹Heyting Lattices›

text ‹
We obtain further properties if the underlying structure is a lattice.
In particular, the lattice operations are automatically distributive in this case.
›

class heyting_lattice = lattice + heyting_semilattice
begin

lemma sup_distrib_inf_le:
"(x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ (y ⊓ z)"
proof -
have "x ⊔ z ≤ y ↝ (x ⊔ (y ⊓ z))"
using implies_galois_var implies_increasing sup.bounded_iff sup.cobounded2 by blast
hence "x ⊔ y ≤ (x ⊔ z) ↝ (x ⊔ (y ⊓ z))"
using implies_galois_swap implies_increasing le_sup_iff by blast
thus ?thesis
qed

subclass distrib_lattice
apply unfold_locales
using distrib_sup_le order.eq_iff sup_distrib_inf_le by auto

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

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

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

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

lemma implies_antitone_isotone:
"(x ⊔ y) ↝ (x ⊓ y) ≤ x ↝ y"
by (simp add: implies_antitone_sup implies_dist_inf le_infI2)

lemma implies_antisymmetry:
"(x ↝ y) ⊓ (y ↝ x) = (x ⊔ y) ↝ (x ⊓ y)"
by (metis implies_dist_sup implies_inf_absorb inf.commute)

lemma sup_inf_implies [simp]:
"(x ⊔ y) ⊓ (x ↝ y) = y"

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

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

lemma implies_sup_absorb:
"(x ↝ y) ⊔ z ≤ (x ⊔ z) ↝ (y ⊔ z)"
by (metis implies_dist_sup implies_isotone_sup implies_increasing inf_inf_implies le_sup_iff sup_inf_implies)

lemma sup_below_implies_implies:
"x ⊔ y ≤ (x ↝ y) ↝ y"
by (simp add: implies_dist_sup implies_galois_swap implies_increasing)

end

class bounded_heyting_lattice = bounded_lattice + heyting_lattice
begin

subclass bounded_heyting_semilattice ..

lemma implies_bot [simp]:
"bot ↝ x = top"
using implies_galois top_unique by fastforce

end

subsubsection ‹Heyting Algebras›

text ‹
The pseudocomplement operation can be defined in Heyting algebras, but it is typically not part of their signature.
We add the definition as an axiom so that we can use the class hierarchy, for example, to inherit results from the class ‹pd_algebra›.
›

class heyting_algebra = bounded_heyting_lattice + uminus +
assumes uminus_eq: "-x = x ↝ bot"
begin

subclass pd_algebra
apply unfold_locales
using bot_unique implies_galois uminus_eq by auto

lemma boolean_implies_below:
"-x ⊔ y ≤ x ↝ y"
by (simp add: implies_increasing implies_isotone uminus_eq)

lemma negation_implies:
"-(x ↝ y) = --x ⊓ -y"
proof (rule order.antisym)
show "-(x ↝ y) ≤ --x ⊓ -y"
using boolean_implies_below p_antitone by auto
next
have "x ⊓ -y ⊓ (x ↝ y) = bot"
by (metis implies_mp_eq inf_p inf_bot_left inf_commute inf_left_commute)
hence "--x ⊓ -y ⊓ (x ↝ y) = bot"
using pp_inf_bot_iff inf_assoc by auto
thus "--x ⊓ -y ≤ -(x ↝ y)"
qed

lemma double_negation_dist_implies:
"--(x ↝ y) = --x ↝ --y"
apply (rule order.antisym)
apply (metis pp_inf_below_iff implies_galois_decreasing implies_galois negation_implies ppp)

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

end

text ‹
The following class gives equational axioms for Heyting algebras.
›

class heyting_algebra_eq = bounded_lattice + implies + uminus +
assumes implies_mp_eq: "x ⊓ (x ↝ y) = x ⊓ y"
and implies_import_inf: "x ⊓ ((x ⊓ y) ↝ (x ↝ z)) = x ⊓ (y ↝ z)"
and inf_inf_implies: "z ⊓ ((x ⊓ y) ↝ x) = z"
and uminus_eq_eq: "-x = x ↝ bot"
begin

subclass heyting_algebra
apply unfold_locales
apply (rule iffI)
apply (metis implies_import_inf inf.sup_left_divisibility inf_inf_implies le_iff_inf)
apply (metis implies_mp_eq inf.commute inf.le_sup_iff inf.sup_right_isotone)

end

text ‹
A relative pseudocomplement is not enough to obtain the Stone equation, so we add it in the following class.
›

class heyting_stone_algebra = heyting_algebra +
assumes heyting_stone: "-x ⊔ --x = top"
begin

subclass stone_algebra

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

end

subsubsection ‹Brouwer Algebras›

text ‹
Brouwer algebras are dual to Heyting algebras.
The dual pseudocomplement of an element ‹y› relative to an element ‹x› is the least element whose join with ‹y› is above ‹x›.
We can now use the binary operation provided by Boolean algebras in Isabelle/HOL because it is compatible with dual relative pseudocomplements (not relative pseudocomplements).
›

class brouwer_algebra = bounded_lattice + minus + uminus +
assumes minus_galois: "x ≤ y ⊔ z ⟷ x - y ≤ z"
and uminus_eq_minus: "-x = top - x"
begin

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

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

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

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

end

subsection ‹Boolean Algebras›

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

context boolean_algebra
begin

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

"conjugate f g ⟹ additive f"

lemma conjugate_isotone:
"conjugate f g ⟹ isotone f"

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

lemma conjugate_char_2:
"conjugate f g ⟷ f bot = bot ∧ g bot = bot ∧ (∀x y . f x ⊓ y ≤ f(x ⊓ g y) ∧ g y ⊓ x ≤ g(y ⊓ f x))"

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

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

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" ("↓_"  80)
where "↓x ≡ { y . y ≤ x }"

abbreviation down_set :: "'a set ⇒ 'a set" ("⇓_"  80)
where "⇓X ≡ { y . ∃x∈X . y ≤ x }"

abbreviation is_down_set :: "'a set ⇒ bool"
where "is_down_set X ≡ ∀x∈X . ∀y . y ≤ x ⟶ y∈X"

abbreviation is_principal_down :: "'a set ⇒ bool"
where "is_principal_down X ≡ ∃x . X = ↓x"

abbreviation up :: "'a ⇒ 'a set" ("↑_"  80)
where "↑x ≡ { y . x ≤ y }"

abbreviation up_set :: "'a set ⇒ 'a set" ("⇑_"  80)
where "⇑X ≡ { y . ∃x∈X . x ≤ y }"

abbreviation is_up_set :: "'a set ⇒ bool"
where "is_up_set X ≡ ∀x∈X . ∀y . x ≤ y ⟶ y∈X"

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 ≠ {}) ∧ (∀x∈F . ∀y∈F . ∃z∈F . 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 "∀x∈f  F . ∀y∈f  F . ∃z∈f  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 "∃z∈f  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}"

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 "∃z∈I . 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 "∃z∈H . 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}"

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 . ∃x∈F . ∃y∈G . 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: "∀x∈filter_sup F G . ∀y∈filter_sup F G . ∃z∈filter_sup F G . z ≤ x ∧ z ≤ y"
proof
fix x
assume "x∈filter_sup F G"
then obtain t u where 3: "t ∈ F ∧ u ∈ G ∧ t ⊓ u ≤ x"
using filter_sup_def by auto
show "∀y∈filter_sup F G . ∃z∈filter_sup F G . z ≤ x ∧ z ≤ y"
proof
fix y
assume "y∈filter_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 "∃z∈filter_sup F G . z ≤ x ∧ z ≤ y"
using 5 by blast
qed
qed
have "∀x∈filter_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 "y∈G"
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"
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 "u∈↑x ∧ v∈↑y ∧ 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 . ∃z∈F . x ⊓ z = y})"
proof -
let ?G = "⇑{ y . ∃z∈F . 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: "x∈F ∧ y∈G"
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 "∀x∈F ∩ G . ∀y∈F ∩ G . ∃z∈F ∩ 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

lift_definition sup_filter :: "'a filter ⇒ 'a filter ⇒ 'a filter" is filter_sup

lift_definition inf_filter :: "'a filter ⇒ 'a filter ⇒ 'a filter" is inter

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

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)"
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 ⟹ (∃x∈F . ∃y∈G . z = x ⊔ y)"
by force

lemma filter_sup_principal_rep:
assumes "filter F"
and "filter G"
and "filter_sup F G = ↑z"
shows "∃x∈F . ∃y∈G . z = x ⊓ y"
proof -
from assms(3) obtain x y where 1: "x∈F ∧ y∈G ∧ 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: "t∈F ∧ u∈G ∧ y = t ⊔ u"
using 1 by meson
from filter_sup_principal_rep obtain v w where 3: "v∈F ∧ w∈G ∧ 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)"
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

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 . ∃w∈F . 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"
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: "u∈↑x ∧ v∈↑y ∧ 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"
hence 2: "filter (F ∩ ↑x) ∧ filter (G ∩ ↑x)"
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"
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

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
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"
have "?v ⊓ ?w = Abs_dense (?t ⊓ ?u)"
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"
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"
also have "... ≤ Rep_dense v ⊓ Rep_dense w"
using 4 inf_mono mem_Collect_eq by blast
also have "... = Rep_dense (v ⊓ w)"
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"
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)"
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"
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))"
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))"
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)"
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"
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"
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 x∈F 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)"
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"
next
fix xf :: "('a,'b) lifted_pair"
{
fix f :: "('a,'b) phi"
have 1: "triple (Rep_phi f)"
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"
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)"
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"
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)"
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)"
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"
next
fix xf yf :: "('a,'b) lifted_pair"
{
fix f :: "('a,'b) phi"
have 1: "triple (Rep_phi f)"
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"
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)"
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"
next
fix xf yf :: "('a,'b) lifted_pair"
{
fix f :: "('a,'b) phi"
have 1: "triple (Rep_phi f)"
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"
next
fix xf yf :: "('a,'b) lifted_pair"
{
fix f :: "('a,'b) phi"
have 1: "triple (Rep_phi f)"
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"
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)"
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"
next
fix xf :: "('a,'b) lifted_pair"
{
fix f :: "('a,'b) phi"
have 1: "triple (Rep_phi f)"
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"
next
fix xf :: "('a,'b) lifted_pair"
{
fix f :: "('a,'b) phi"
have 1: "triple (Rep_phi f)"
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"
next
fix xf yf zf :: "('a,'b) lifted_pair"
{
fix f :: "('a,'b) phi"
have 1: "triple (Rep_phi f)"
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)"
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)"
next
fix xf :: "('a,'b) lifted_pair"
{
fix f :: "('a,'b) phi"
have 1: "triple (Rep_phi f)"
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"
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))"
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)"
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))"
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))"
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)"
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))"
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}))"
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))"
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))"
also have "... = (---x1,?r (--x1))"
also have "... = ?pp f (-x1,stone_phi x1)"
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))"
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))"
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)"
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"
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)))"
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"
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)"
thus "x ≤ y"
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 (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)))"
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"
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))"
qed
hence "Abs_filter (Rep_filter (stone_phi (Abs_regular (-x)) ⊓ up_filter (Abs_dense (y ⊔ -y)))) ≤ up_filter (Abs_dense (y ⊔ -y ⊔ x))"
thus ?thesis
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"
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)))"
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"
hence 3: "stone_phi (-x) ≤ y"
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)"
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))))"
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)))"
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)))"
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)"
also have "... = bot"
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"
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"
have "y ≤ x ⊔ -x ⊔ --y"
hence "(x ⊔ -x ⊔ --y) ⊓ (y ⊔ -y) = y ⊔ ((x ⊔ -x ⊔ --y) ⊓ -y)"
also have "... = y ⊔ ((x ⊔ -x) ⊓ -y)"
also have "... ≤ Rep_dense z"
using 3 by (meson le_infI1 sup.bounded_iff)
finally have "Abs_dense ((x ⊔ -x ⊔ --y) ⊓ (y ⊔ -y)) ≤ z"
hence 4: "?u ⊓ ?v ≤ z"
have "-Rep_regular (Abs_regular (-y)) = --y"
by (metis (mono_tags, lifting) mem_Collect_eq Abs_regular_inverse)
also have "... ≤ Rep_dense ?u"
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))"
also have "... = stone_phi (Abs_regular (-y)) ⊔ up_filter ?v"
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))"
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))"
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))) ≤ ..."
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)))"
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))"
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)))"
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)))"
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)))"
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)"
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)"