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

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

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

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

theory Stone_Construction

imports P_Algebras Filters

begin

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

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

subsection ‹The Triple of a Stone Algebra›

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

subsubsection ‹Regular Elements›

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

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

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

setup_lifting type_definition_regular

instantiation regular :: (stone_algebra) boolean_algebra
begin

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

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

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

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

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

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

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

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

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

end

instantiation regular :: (non_trivial_stone_algebra) non_trivial_boolean_algebra
begin

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

end

subsubsection ‹Dense Elements›

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

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

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

setup_lifting type_definition_dense

instantiation dense :: (stone_algebra) distrib_lattice_top
begin

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

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

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

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

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

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

end

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

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

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

type_synonym 'a dense_filter = "'a dense filter"

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

setup_lifting type_definition_dense_filter_type

instantiation dense_filter_type :: (stone_algebra) bounded_distrib_lattice
begin

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

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

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

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

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

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

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

end

subsubsection ‹The Structure Map›

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

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

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

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

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

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

subsection ‹Properties of Triples›

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

context triple
begin

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

end

subsection ‹The Stone Algebra of a Triple›

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

typedef (overloaded) ('a,'b) phi = "{ f::'a::non_trivial_boolean_algebra ⇒ 'b::distrib_lattice_top filter . bounded_lattice_homomorphism f }"
proof -
  from ultra_filter_exists obtain F :: "'a set" where 1: "ultra_filter F"
    by auto
  hence 2: "prime_filter F"
    using ultra_filter_prime by auto
  let ?f = "λx . if 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)"
      by (simp add: triple_def)
    thus "triple.pairs_bot ∈ triple.pairs (Rep_phi f)"
      using triple.regular_pairs triple.phi_top by fastforce
  qed
  thus ?thesis
    by auto
qed

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

setup_lifting type_definition_lifted_pair

text ‹
The lifted pairs form a Stone algebra.
›

instantiation lifted_pair :: (non_trivial_boolean_algebra,distrib_lattice_top) stone_algebra
begin

text ‹
All operations are lifted point-wise.
›

lift_definition sup_lifted_pair :: "('a,'b) lifted_pair ⇒ ('a,'b) lifted_pair ⇒ ('a,'b) lifted_pair" is "λxf yf f . triple.pairs_sup (xf f) (yf f)"
  by (metis (no_types, opaque_lifting) 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, opaque_lifting) 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, opaque_lifting) 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, opaque_lifting) 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, opaque_lifting) simp_phi triple_def triple.pairs_top_closed)

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

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

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

end

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

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

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

setup_lifting type_definition_stone_phi_pair

instantiation stone_phi_pair :: (stone_algebra) sup_inf_top_bot_uminus_ord
begin

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

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

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

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

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

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

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

instance ..

end

(*
instantiation stone_phi_pair :: (stone_algebra) stone_algebra
begin

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

end
*)

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

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

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

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

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

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

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

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

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

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

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

instantiation stone_phi_pair :: (non_trivial_stone_algebra) stone_algebra
begin

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

end

subsection ‹Stone Algebra Isomorphism›

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

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

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

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

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

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

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

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

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

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

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

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

subsection ‹Triple Isomorphism›

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

subsubsection ‹Boolean Algebra Isomorphism›

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

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

setup_lifting type_definition_lifted_boolean_algebra

instantiation lifted_boolean_algebra :: (non_trivial_boolean_algebra,distrib_lattice_top) boolean_algebra
begin

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

lift_definition inf_lifted_boolean_algebra :: "('a,'b) lifted_boolean_algebra ⇒ ('a,'b) lifted_boolean_algebra ⇒ ('a,'b) lifted_boolean_algebra" is "λxf yf f . inf (xf f) (yf f)" .

lift_definition minus_lifted_boolean_algebra :: "('a,'b) lifted_boolean_algebra ⇒ ('a,'b) lifted_boolean_algebra ⇒ ('a,'b) lifted_boolean_algebra" is "λxf yf f . minus (xf f) (yf f)" .

lift_definition uminus_lifted_boolean_algebra :: "('a,'b) lifted_boolean_algebra ⇒ ('a,'b) lifted_boolean_algebra" is "λxf f . uminus (xf f)" .

lift_definition bot_lifted_boolean_algebra :: "('a,'b) lifted_boolean_algebra" is "λf . bot" ..

lift_definition top_lifted_boolean_algebra :: "('a,'b) lifted_boolean_algebra" is "λf . top" ..

lift_definition less_eq_lifted_boolean_algebra :: "('a,'b) lifted_boolean_algebra ⇒ ('a,'b) lifted_boolean_algebra ⇒ bool" is "λxf yf . ∀f . less_eq (xf f) (yf f)" .

lift_definition less_lifted_boolean_algebra :: "('a,'b) lifted_boolean_algebra ⇒ ('a,'b) lifted_boolean_algebra ⇒ bool" is "λxf yf . (∀f . less_eq (xf f) (yf f)) ∧ ¬ (∀f . less_eq (yf f) (xf f))" .

instance
  apply intro_classes
  subgoal apply transfer by auto
  subgoal apply transfer by auto
  subgoal apply transfer using order_trans by blast
  subgoal apply transfer using antisym ext by blast
  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 (simp add: sup_inf_distrib1)
  subgoal apply transfer by auto
  subgoal apply transfer by auto
  subgoal apply transfer by (simp add: diff_eq)
  done

end

text ‹
The following two definitions give the Boolean algebra isomorphism.
›

abbreviation ba_iso_inv :: "('a::non_trivial_boolean_algebra,'b::distrib_lattice_top) lifted_boolean_algebra ⇒ ('a,'b) lifted_pair regular"
  where "ba_iso_inv ≡ λxf . Abs_regular (Abs_lifted_pair (λf . (Rep_lifted_boolean_algebra xf f,Rep_phi f (-Rep_lifted_boolean_algebra xf f))))"

abbreviation ba_iso :: "('a::non_trivial_boolean_algebra,'b::distrib_lattice_top) lifted_pair regular ⇒ ('a,'b) lifted_boolean_algebra"
  where "ba_iso ≡ λpf . Abs_lifted_boolean_algebra (λf . fst (Rep_lifted_pair (Rep_regular pf) f))"

lemma ba_iso_inv_lifted_pair:
  "(Rep_lifted_boolean_algebra xf f,Rep_phi f (-Rep_lifted_boolean_algebra xf f)) ∈ triple.pairs (Rep_phi f)"
  by (metis (no_types, opaque_lifting) double_compl simp_phi triple.pairs_uminus.simps triple_def triple.pairs_uminus_closed)

lemma ba_iso_inv_regular:
  "regular (Abs_lifted_pair (λf . (Rep_lifted_boolean_algebra xf f,Rep_phi f (-Rep_lifted_boolean_algebra xf f))))"
proof -
  have "∀f . (Rep_lifted_boolean_algebra xf f,Rep_phi f (-Rep_lifted_boolean_algebra xf f)) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_lifted_boolean_algebra xf f,Rep_phi f (-Rep_lifted_boolean_algebra xf f)))"
    by (simp add: triple.pairs_uminus.simps triple_def)
  hence "Abs_lifted_pair (λf . (Rep_lifted_boolean_algebra xf f,Rep_phi f (-Rep_lifted_boolean_algebra xf f))) = --Abs_lifted_pair (λf . (Rep_lifted_boolean_algebra xf f,Rep_phi f (-Rep_lifted_boolean_algebra xf f)))"
    by (simp add: triple.pairs_uminus_closed triple_def eq_onp_def uminus_lifted_pair.abs_eq ba_iso_inv_lifted_pair)
  thus ?thesis
    by simp
qed

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

lemma ba_iso_left_invertible:
  "ba_iso_inv (ba_iso pf) = pf"
proof -
  have 1: "∀f . snd (Rep_lifted_pair (Rep_regular pf) f) = Rep_phi f (-fst (Rep_lifted_pair (Rep_regular pf) f))"
  proof
    fix f :: "('a,'b) phi"
    let ?r = "Rep_phi f"
    have "triple ?r"
      by (simp add: triple_def)
    hence 2: "∀p . triple.pairs_uminus ?r p = (-fst p,?r (fst p))"
      by (metis prod.collapse triple.pairs_uminus.simps)
    have 3: "Rep_regular pf = --Rep_regular pf"
      by (simp add: regular_in_p_image_iff)
    show "snd (Rep_lifted_pair (Rep_regular pf) f) = ?r (-fst (Rep_lifted_pair (Rep_regular pf) f))"
      using 2 3 by (metis fstI sndI uminus_lifted_pair.rep_eq)
  qed
  have "ba_iso_inv (ba_iso pf) = Abs_regular (Abs_lifted_pair (λf . (fst (Rep_lifted_pair (Rep_regular pf) f),Rep_phi f (-fst (Rep_lifted_pair (Rep_regular pf) f)))))"
    by (simp add: Abs_lifted_boolean_algebra_inverse)
  also have "... = Abs_regular (Abs_lifted_pair (Rep_lifted_pair (Rep_regular pf)))"
    using 1 by (metis prod.collapse)
  also have "... = pf"
    by (simp add: Rep_regular_inverse Rep_lifted_pair_inverse)
  finally show ?thesis
    .
qed

lemma ba_iso_right_invertible:
  "ba_iso (ba_iso_inv xf) = xf"
proof -
  let ?rf = "Rep_lifted_boolean_algebra xf"
  have 1: "∀f . (-?rf f,Rep_phi f (?rf f)) ∈ triple.pairs (Rep_phi f) ∧ (?rf f,Rep_phi f (-?rf f)) ∈ triple.pairs (Rep_phi f)"
  proof
    fix f
    have "up_filter top = bot"
      by (simp add: bot_filter.abs_eq)
    hence "(∃z . Rep_phi f (?rf f) = Rep_phi f (?rf f) ⊔ up_filter z) ∧ (∃z . Rep_phi f (-?rf f) = Rep_phi f (-?rf f) ⊔ up_filter z)"
      by (metis sup_bot_right)
    thus "(-?rf f,Rep_phi f (?rf f)) ∈ triple.pairs (Rep_phi f) ∧ (?rf f,Rep_phi f (-?rf f)) ∈ triple.pairs (Rep_phi f)"
      by (simp add: triple_def triple.pairs_def)
  qed
  have "regular (Abs_lifted_pair (λf . (?rf f,Rep_phi f (-?rf f))))"
  proof -
    have "--Abs_lifted_pair (λf . (?rf f,Rep_phi f (-?rf f))) = -Abs_lifted_pair (λf . triple.pairs_uminus (Rep_phi f) (?rf f,Rep_phi f (-?rf f)))"
      using 1 by (simp add: eq_onp_same_args uminus_lifted_pair.abs_eq)
    also have "... = -Abs_lifted_pair (λf . (-?rf f,Rep_phi f (?rf f)))"
      by (metis (no_types, lifting) simp_phi triple_def triple.pairs_uminus.simps)
    also have "... = Abs_lifted_pair (λf . triple.pairs_uminus (Rep_phi f) (-?rf f,Rep_phi f (?rf f)))"
      using 1 by (simp add: eq_onp_same_args uminus_lifted_pair.abs_eq)
    also have "... = Abs_lifted_pair (λf . (?rf f,Rep_phi f (-?rf f)))"
      by (metis (no_types, lifting) simp_phi triple_def triple.pairs_uminus.simps double_compl)
    finally show ?thesis
      by simp
  qed
  hence "in_p_image (Abs_lifted_pair (λf . (?rf f,Rep_phi f (-?rf f))))"
    by blast
  thus ?thesis
    using 1 by (simp add: Rep_lifted_boolean_algebra_inverse Abs_lifted_pair_inverse Abs_regular_inverse)
qed

text ‹
The isomorphism is established by proving the remaining Boolean algebra homomorphism properties.
›

lemma ba_iso:
  "boolean_algebra_isomorphism ba_iso"
proof (intro conjI)
  show "Abs_lifted_boolean_algebra (λf . fst (Rep_lifted_pair (Rep_regular bot) f)) = bot"
    by (simp add: bot_lifted_boolean_algebra_def bot_regular.rep_eq bot_lifted_pair.rep_eq)
  show "Abs_lifted_boolean_algebra (λf . fst (Rep_lifted_pair (Rep_regular top) f)) = top"
    by (simp add: top_lifted_boolean_algebra_def top_regular.rep_eq top_lifted_pair.rep_eq)
  show "∀pf qf . Abs_lifted_boolean_algebra (λf::('a,'b) phi . fst (Rep_lifted_pair (Rep_regular (pf ⊔ qf)) f)) = Abs_lifted_boolean_algebra (λf . fst (Rep_lifted_pair (Rep_regular pf) f)) ⊔ Abs_lifted_boolean_algebra (λf . fst (Rep_lifted_pair (Rep_regular qf) f))"
  proof (intro allI)
    fix pf qf :: "('a,'b) lifted_pair regular"
    {
      fix f
      obtain x y z w where 1: "(x,y) = Rep_lifted_pair (Rep_regular pf) f ∧ (z,w) = Rep_lifted_pair (Rep_regular qf) f"
        using prod.collapse by blast
      have "triple (Rep_phi f)"
        by (simp add: triple_def)
      hence "fst (triple.pairs_sup (x,y) (z,w)) = fst (x,y) ⊔ fst (z,w)"
        using triple.pairs_sup.simps by force
      hence "fst (triple.pairs_sup (Rep_lifted_pair (Rep_regular pf) f) (Rep_lifted_pair (Rep_regular qf) f)) = fst (Rep_lifted_pair (Rep_regular pf) f) ⊔ fst (Rep_lifted_pair (Rep_regular qf) f)"
        using 1 by simp
      hence "fst (Rep_lifted_pair (Rep_regular (pf ⊔ qf)) f) = fst (Rep_lifted_pair (Rep_regular pf) f) ⊔ fst (Rep_lifted_pair (Rep_regular qf) f)"
        by (unfold sup_regular.rep_eq sup_lifted_pair.rep_eq) simp
    }
    thus "Abs_lifted_boolean_algebra (λf . fst (Rep_lifted_pair (Rep_regular (pf ⊔ qf)) f)) = Abs_lifted_boolean_algebra (λf . fst (Rep_lifted_pair (Rep_regular pf) f)) ⊔ Abs_lifted_boolean_algebra (λf . fst (Rep_lifted_pair (Rep_regular qf) f))"
      by (simp add: eq_onp_same_args sup_lifted_boolean_algebra.abs_eq sup_regular.rep_eq sup_lifted_boolean_algebra.rep_eq)
  qed
  show 1: "∀pf qf . Abs_lifted_boolean_algebra (λf::('a,'b) phi . fst (Rep_lifted_pair (Rep_regular (pf ⊓ qf)) f)) = Abs_lifted_boolean_algebra (λf . fst (Rep_lifted_pair (Rep_regular pf) f)) ⊓ Abs_lifted_boolean_algebra (λf . fst (Rep_lifted_pair (Rep_regular qf) f))"
  proof (intro allI)
    fix pf qf :: "('a,'b) lifted_pair regular"
    {
      fix f
      obtain x y z w where 1: "(x,y) = Rep_lifted_pair (Rep_regular pf) f ∧ (z,w) = Rep_lifted_pair (Rep_regular qf) f"
        using prod.collapse by blast
      have "triple (Rep_phi f)"
        by (simp add: triple_def)
      hence "fst (triple.pairs_inf (x,y) (z,w)) = fst (x,y) ⊓ fst (z,w)"
        using triple.pairs_inf.simps by force
      hence "fst (triple.pairs_inf (Rep_lifted_pair (Rep_regular pf) f) (Rep_lifted_pair (Rep_regular qf) f)) = fst (Rep_lifted_pair (Rep_regular pf) f) ⊓ fst (Rep_lifted_pair (Rep_regular qf) f)"
        using 1 by simp
      hence "fst (Rep_lifted_pair (Rep_regular (pf ⊓ qf)) f) = fst (Rep_lifted_pair (Rep_regular pf) f) ⊓ fst (Rep_lifted_pair (Rep_regular qf) f)"
        by (unfold inf_regular.rep_eq inf_lifted_pair.rep_eq) simp
    }
    thus "Abs_lifted_boolean_algebra (λf . fst (Rep_lifted_pair (Rep_regular (pf ⊓ qf)) f)) = Abs_lifted_boolean_algebra (λf . fst (Rep_lifted_pair (Rep_regular pf) f)) ⊓ Abs_lifted_boolean_algebra (λf . fst (Rep_lifted_pair (Rep_regular qf) f))"
      by (simp add: eq_onp_same_args inf_lifted_boolean_algebra.abs_eq inf_regular.rep_eq inf_lifted_boolean_algebra.rep_eq)
  qed
  show "∀pf . Abs_lifted_boolean_algebra (λf::('a,'b) phi . fst (Rep_lifted_pair (Rep_regular (-pf)) f)) = -Abs_lifted_boolean_algebra (λf . fst (Rep_lifted_pair (Rep_regular pf) f))"
  proof
    fix pf :: "('a,'b) lifted_pair regular"
    {
      fix f
      obtain x y where 1: "(x,y) = Rep_lifted_pair (Rep_regular pf) f"
        using prod.collapse by blast
      have "triple (Rep_phi f)"
        by (simp add: triple_def)
      hence "fst (triple.pairs_uminus (Rep_phi f) (x,y)) = -fst (x,y)"
        using triple.pairs_uminus.simps by force
      hence "fst (triple.pairs_uminus (Rep_phi f) (Rep_lifted_pair (Rep_regular pf) f)) = -fst (Rep_lifted_pair (Rep_regular pf) f)"
        using 1 by simp
      hence "fst (Rep_lifted_pair (Rep_regular (-pf)) f) = -fst (Rep_lifted_pair (Rep_regular pf) f)"
        by (unfold uminus_regular.rep_eq uminus_lifted_pair.rep_eq) simp
    }
    thus "Abs_lifted_boolean_algebra (λf . fst (Rep_lifted_pair (Rep_regular (-pf)) f)) = -Abs_lifted_boolean_algebra (λf . fst (Rep_lifted_pair (Rep_regular pf) f))"
      by (simp add: eq_onp_same_args uminus_lifted_boolean_algebra.abs_eq uminus_regular.rep_eq uminus_lifted_boolean_algebra.rep_eq)
  qed
  thus "∀pf qf . Abs_lifted_boolean_algebra (λf::('a,'b) phi . fst (Rep_lifted_pair (Rep_regular (pf - qf)) f)) = Abs_lifted_boolean_algebra (λf . fst (Rep_lifted_pair (Rep_regular pf) f)) - Abs_lifted_boolean_algebra (λf . fst (Rep_lifted_pair (Rep_regular qf) f))"
    using 1 by (simp add: diff_eq)
  show "bij ba_iso"
    by (rule invertible_bij[where g=ba_iso_inv]) (simp_all add: ba_iso_left_invertible ba_iso_right_invertible)
qed

subsubsection ‹Distributive Lattice Isomorphism›

text ‹
We carry out a similar development for the isomorphism of distributive lattices.
Again, the original distributive lattice with a greatest element needs to be lifted to match the lifted pairs.
›

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

setup_lifting type_definition_lifted_distrib_lattice_top

instantiation lifted_distrib_lattice_top :: (non_trivial_boolean_algebra,distrib_lattice_top) distrib_lattice_top
begin

lift_definition sup_lifted_distrib_lattice_top :: "('a,'b) lifted_distrib_lattice_top ⇒ ('a,'b) lifted_distrib_lattice_top ⇒ ('a,'b) lifted_distrib_lattice_top" is "λxf yf f . sup (xf f) (yf f)" .

lift_definition inf_lifted_distrib_lattice_top :: "('a,'b) lifted_distrib_lattice_top ⇒ ('a,'b) lifted_distrib_lattice_top ⇒ ('a,'b) lifted_distrib_lattice_top" is "λxf yf f . inf (xf f) (yf f)" .

lift_definition top_lifted_distrib_lattice_top :: "('a,'b) lifted_distrib_lattice_top" is "λf . top" ..

lift_definition less_eq_lifted_distrib_lattice_top :: "('a,'b) lifted_distrib_lattice_top ⇒ ('a,'b) lifted_distrib_lattice_top ⇒ bool" is "λxf yf . ∀f . less_eq (xf f) (yf f)" .

lift_definition less_lifted_distrib_lattice_top :: "('a,'b) lifted_distrib_lattice_top ⇒ ('a,'b) lifted_distrib_lattice_top ⇒ bool" is "λxf yf . (∀f . less_eq (xf f) (yf f)) ∧ ¬ (∀f . less_eq (yf f) (xf f))" .

instance
  apply intro_classes
  subgoal apply transfer by auto
  subgoal apply transfer by auto
  subgoal apply transfer using order_trans by blast
  subgoal apply transfer using antisym ext by blast
  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 (simp add: sup_inf_distrib1)
  done

end

text ‹
The following function extracts the least element of the filter of a dense pair, which turns out to be a principal filter.
It is used to define one of the isomorphisms below.
›

fun get_dense :: "('a::non_trivial_boolean_algebra,'b::distrib_lattice_top) lifted_pair dense ⇒ ('a,'b) phi ⇒ 'b"
  where "get_dense pf f = (SOME z . Rep_lifted_pair (Rep_dense pf) f = (top,up_filter z))"

lemma get_dense_char:
  "Rep_lifted_pair (Rep_dense pf) f = (top,up_filter (get_dense pf f))"
proof -
  obtain x y where 1: "(x,y) = Rep_lifted_pair (Rep_dense pf) f ∧ (x,y) ∈ triple.pairs (Rep_phi f) ∧ triple.pairs_uminus (Rep_phi f) (x,y) = triple.pairs_bot"
    by (metis bot_lifted_pair.rep_eq prod.collapse simp_dense simp_lifted_pair uminus_lifted_pair.rep_eq)
  hence 2: "x = top"
    by (simp add: triple.intro triple.pairs_uminus.simps dense_pp)
  have "triple (Rep_phi f)"
    by (simp add: triple_def)
  hence "∃z. y = Rep_phi f (-x) ⊔ up_filter z"
    using 1 triple.pairs_def by blast
  then obtain z where "y = up_filter z"
    using 2 by auto
  hence "Rep_lifted_pair (Rep_dense pf) f = (top,up_filter z)"
    using 1 2 by simp
  thus ?thesis
    by (metis (mono_tags, lifting) tfl_some get_dense.simps)
qed

text ‹
The following two definitions give the distributive lattice isomorphism.
›

abbreviation dl_iso_inv :: "('a::non_trivial_boolean_algebra,'b::distrib_lattice_top) lifted_distrib_lattice_top ⇒ ('a,'b) lifted_pair dense"
  where "dl_iso_inv ≡ λxf . Abs_dense (Abs_lifted_pair (λf . (top,up_filter (Rep_lifted_distrib_lattice_top xf f))))"

abbreviation dl_iso :: "('a::non_trivial_boolean_algebra,'b::distrib_lattice_top) lifted_pair dense ⇒ ('a,'b) lifted_distrib_lattice_top"
  where "dl_iso ≡ λpf . Abs_lifted_distrib_lattice_top (get_dense pf)"

lemma dl_iso_inv_lifted_pair:
  "(top,up_filter (Rep_lifted_distrib_lattice_top xf f)) ∈ triple.pairs (Rep_phi f)"
  by (metis (no_types, opaque_lifting) compl_bot_eq double_compl simp_phi sup_bot.left_neutral triple.sa_iso_pair triple_def)

lemma dl_iso_inv_dense:
  "dense (Abs_lifted_pair (λf . (top,up_filter (Rep_lifted_distrib_lattice_top xf f))))"
proof -
  have "∀f . triple.pairs_uminus (Rep_phi f) (top,up_filter (Rep_lifted_distrib_lattice_top xf f)) = triple.pairs_bot"
    by (simp add: top_filter.abs_eq triple.pairs_uminus.simps triple_def)
  hence "bot = -Abs_lifted_pair (λf . (top,up_filter (Rep_lifted_distrib_lattice_top xf f)))"
    by (simp add: eq_onp_def uminus_lifted_pair.abs_eq dl_iso_inv_lifted_pair bot_lifted_pair_def)
  thus ?thesis
    by simp
qed

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

lemma dl_iso_left_invertible:
  "dl_iso_inv (dl_iso pf) = pf"
proof -
  have "dl_iso_inv (dl_iso pf) = Abs_dense (Abs_lifted_pair (λf . (top,up_filter (get_dense pf f))))"
    by (metis Abs_lifted_distrib_lattice_top_inverse UNIV_I UNIV_def)
  also have "... = Abs_dense (Abs_lifted_pair (Rep_lifted_pair (Rep_dense pf)))"
    by (metis get_dense_char)
  also have "... = pf"
    by (simp add: Rep_dense_inverse Rep_lifted_pair_inverse)
  finally show ?thesis
    .
qed

lemma dl_iso_right_invertible:
  "dl_iso (dl_iso_inv xf) = xf"
proof -
  let ?rf = "Rep_lifted_distrib_lattice_top xf"
  let ?pf = "Abs_dense (Abs_lifted_pair (λf . (top,up_filter (?rf f))))"
  have 1: "∀f . (top,up_filter (?rf f)) ∈ triple.pairs (Rep_phi f)"
  proof
    fix f :: "('a,'b) phi"
    have "triple (Rep_phi f)"
      by (simp add: triple_def)
    thus "(top,up_filter (?rf f)) ∈ triple.pairs (Rep_phi f)"
      using triple.pairs_def by force
  qed
  have 2: "dense (Abs_lifted_pair (λf . (top,up_filter (?rf f))))"
  proof -
    have "-Abs_lifted_pair (λf . (top,up_filter (?rf f))) = Abs_lifted_pair (λf . triple.pairs_uminus (Rep_phi f) (top,up_filter (?rf f)))"
      using 1 by (simp add: eq_onp_same_args uminus_lifted_pair.abs_eq)
    also have "... = Abs_lifted_pair (λf . (bot,Rep_phi f top))"
      by (simp add: triple.pairs_uminus.simps triple_def)
    also have "... = Abs_lifted_pair (λf . triple.pairs_bot)"
      by (metis (no_types, opaque_lifting) simp_phi triple.phi_top triple_def)
    also have "... = bot"
      by (simp add: bot_lifted_pair_def)
    finally show ?thesis
      by simp
  qed
  have "get_dense ?pf = ?rf"
  proof
    fix f
    have "(top,up_filter (get_dense ?pf f)) = Rep_lifted_pair (Rep_dense ?pf) f"
      by (metis get_dense_char)
    also have "... = Rep_lifted_pair (Abs_lifted_pair (λf . (top,up_filter (?rf f)))) f"
      using Abs_dense_inverse 2 by force
    also have "... = (top,up_filter (?rf f))"
      using 1 by (simp add: Abs_lifted_pair_inverse)
    finally show "get_dense ?pf f = ?rf f"
      using up_filter_injective by auto
  qed
  thus ?thesis
    by (simp add: Rep_lifted_distrib_lattice_top_inverse)
qed

text ‹
To obtain the isomorphism, it remains to show the homomorphism properties of lattices with a greatest element.
›

lemma dl_iso:
  "bounded_lattice_top_isomorphism dl_iso"
proof (intro conjI)
  have "get_dense top = (λf::('a,'b) phi . top)"
  proof
    fix f :: "('a,'b) phi"
    have "Rep_lifted_pair (Rep_dense top) f = (top,Abs_filter {top})"
      by (simp add: top_dense.rep_eq top_lifted_pair.rep_eq)
    hence "up_filter (get_dense top f) = Abs_filter {top}"
      by (metis prod.inject get_dense_char)
    hence "Rep_filter (up_filter (get_dense top f)) = {top}"
      by (metis bot_filter.abs_eq bot_filter.rep_eq)
    thus "get_dense top f = top"
      by (metis self_in_upset singletonD Abs_filter_inverse mem_Collect_eq up_filter)
  qed
  thus "Abs_lifted_distrib_lattice_top (get_dense top::('a,'b) phi ⇒ 'b) = top"
    by (metis top_lifted_distrib_lattice_top_def)
next
  show "∀pf qf :: ('a,'b) lifted_pair dense . Abs_lifted_distrib_lattice_top (get_dense (pf ⊔ qf)) = Abs_lifted_distrib_lattice_top (get_dense pf) ⊔ Abs_lifted_distrib_lattice_top (get_dense qf)"
  proof (intro allI)
    fix pf qf :: "('a,'b) lifted_pair dense"
    have 1: "Abs_lifted_distrib_lattice_top (get_dense pf) ⊔ Abs_lifted_distrib_lattice_top (get_dense qf) = Abs_lifted_distrib_lattice_top (λf . get_dense pf f ⊔ get_dense qf f)"
      by (simp add: eq_onp_same_args sup_lifted_distrib_lattice_top.abs_eq)
    have "(λf . get_dense (pf ⊔ qf) f) = (λf . get_dense pf f ⊔ get_dense qf f)"
    proof
      fix f
      have "(top,up_filter (get_dense (pf ⊔ qf) f)) = Rep_lifted_pair (Rep_dense (pf ⊔ qf)) f"
        by (metis get_dense_char)
      also have "... = triple.pairs_sup (Rep_lifted_pair (Rep_dense pf) f) (Rep_lifted_pair (Rep_dense qf) f)"
        by (simp add: sup_lifted_pair.rep_eq sup_dense.rep_eq)
      also have "... = triple.pairs_sup (top,up_filter (get_dense pf f)) (top,up_filter (get_dense qf f))"
        by (metis get_dense_char)
      also have "... = (top,up_filter (get_dense pf f) ⊓ up_filter (get_dense qf f))"
        by (metis (no_types, lifting) calculation prod.simps(1) simp_phi triple.pairs_sup.simps triple_def)
      also have "... = (top,up_filter (get_dense pf f ⊔ get_dense qf f))"
        by (metis up_filter_dist_sup)
      finally show "get_dense (pf ⊔ qf) f = get_dense pf f ⊔ get_dense qf f"
        using up_filter_injective by blast
    qed
    thus "Abs_lifted_distrib_lattice_top (get_dense (pf ⊔ qf)) = Abs_lifted_distrib_lattice_top (get_dense pf) ⊔ Abs_lifted_distrib_lattice_top (get_dense qf)"
      using 1 by metis
  qed
next
  show "∀pf qf :: ('a,'b) lifted_pair dense . Abs_lifted_distrib_lattice_top (get_dense (pf ⊓ qf)) = Abs_lifted_distrib_lattice_top (get_dense pf) ⊓ Abs_lifted_distrib_lattice_top (get_dense qf)"
  proof (intro allI)
    fix pf qf :: "('a,'b) lifted_pair dense"
    have 1: "Abs_lifted_distrib_lattice_top (get_dense pf) ⊓ Abs_lifted_distrib_lattice_top (get_dense qf) = Abs_lifted_distrib_lattice_top (λf . get_dense pf f ⊓ get_dense qf f)"
      by (simp add: eq_onp_same_args inf_lifted_distrib_lattice_top.abs_eq)
    have "(λf . get_dense (pf ⊓ qf) f) = (λf . get_dense pf f ⊓ get_dense qf f)"
    proof
      fix f
      have "(top,up_filter (get_dense (pf ⊓ qf) f)) = Rep_lifted_pair (Rep_dense (pf ⊓ qf)) f"
        by (metis get_dense_char)
      also have "... = triple.pairs_inf (Rep_lifted_pair (Rep_dense pf) f) (Rep_lifted_pair (Rep_dense qf) f)"
        by (simp add: inf_lifted_pair.rep_eq inf_dense.rep_eq)
      also have "... = triple.pairs_inf (top,up_filter (get_dense pf f)) (top,up_filter (get_dense qf f))"
        by (metis get_dense_char)
      also have "... = (top,up_filter (get_dense pf f) ⊔ up_filter (get_dense qf f))"
        by (metis (no_types, lifting) calculation prod.simps(1) simp_phi triple.pairs_inf.simps triple_def)
      also have "... = (top,up_filter (get_dense pf f ⊓ get_dense qf f))"
        by (metis up_filter_dist_inf)
      finally show "get_dense (pf ⊓ qf) f = get_dense pf f ⊓ get_dense qf f"
        using up_filter_injective by blast
    qed
    thus "Abs_lifted_distrib_lattice_top (get_dense (pf ⊓ qf)) = Abs_lifted_distrib_lattice_top (get_dense pf) ⊓ Abs_lifted_distrib_lattice_top (get_dense qf)"
      using 1 by metis
  qed
next
  show "bij dl_iso"
    by (rule invertible_bij[where g=dl_iso_inv]) (simp_all add: dl_iso_left_invertible dl_iso_right_invertible)
qed

subsubsection ‹Structure Map Preservation›

text ‹
We finally show that the isomorphisms are compatible with the structure maps.
This involves lifting the distributive lattice isomorphism to filters of distributive lattices (as these are the targets of the structure maps).
To this end, we first show that the lifted isomorphism preserves filters.
›

lemma phi_iso_filter:
  "filter ((λqf::('a::non_trivial_boolean_algebra,'b::distrib_lattice_top) lifted_pair dense . Rep_lifted_distrib_lattice_top (dl_iso qf) f) ` Rep_filter (stone_phi pf))"
proof (rule filter_map_filter)
  show "mono (λqf::('a::non_trivial_boolean_algebra,'b::distrib_lattice_top) lifted_pair dense . Rep_lifted_distrib_lattice_top (dl_iso qf) f)"
    by (metis (no_types, lifting) mono_def dl_iso le_iff_sup sup_lifted_distrib_lattice_top.rep_eq)
next
  show "∀qf y . Rep_lifted_distrib_lattice_top (dl_iso qf) f ≤ y ⟶ (∃rf . qf ≤ rf ∧ y = Rep_lifted_distrib_lattice_top (dl_iso rf) f)"
  proof (intro allI, rule impI)
    fix qf :: "('a,'b) lifted_pair dense"
    fix y :: 'b
    assume 1: "Rep_lifted_distrib_lattice_top (dl_iso qf) f ≤ y"
    let ?rf = "Abs_dense (Abs_lifted_pair (λg . if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g))"
    have 2: "∀g . (if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g) ∈ triple.pairs (Rep_phi g)"
      by (metis Abs_lifted_distrib_lattice_top_inverse dl_iso_inv_lifted_pair mem_Collect_eq simp_lifted_pair)
    hence "-Abs_lifted_pair (λg . if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g) = Abs_lifted_pair (λg . triple.pairs_uminus (Rep_phi g) (if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g))"
      by (simp add: eq_onp_def uminus_lifted_pair.abs_eq)
    also have "... = Abs_lifted_pair (λg . if g = f then triple.pairs_uminus (Rep_phi g) (top,up_filter y) else triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_dense qf) g))"
      by (simp add: if_distrib)
    also have "... = Abs_lifted_pair (λg . if g = f then (bot,top) else triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_dense qf) g))"
      by (subst triple.pairs_uminus.simps, simp add: triple_def, metis compl_top_eq simp_phi)
    also have "... = Abs_lifted_pair (λg . if g = f then (bot,top) else (bot,top))"
      by (metis bot_lifted_pair.rep_eq simp_dense top_filter.abs_eq uminus_lifted_pair.rep_eq)
    also have "... = bot"
      by (simp add: bot_lifted_pair.abs_eq top_filter.abs_eq)
    finally have 3: "Abs_lifted_pair (λg . if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g) ∈ dense_elements"
      by blast
    hence "(top,up_filter (get_dense (Abs_dense (Abs_lifted_pair (λg . if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) f)) = Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (λg . if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) f"
      by (metis (mono_tags, lifting) get_dense_char)
    also have "... = Rep_lifted_pair (Abs_lifted_pair (λg . if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) f"
      using 3 by (simp add: Abs_dense_inverse)
    also have "... = (top,up_filter y)"
      using 2 by (simp add: Abs_lifted_pair_inverse)
    finally have "get_dense (Abs_dense (Abs_lifted_pair (λg . if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) f = y"
      using up_filter_injective by blast
    hence 4: "Rep_lifted_distrib_lattice_top (dl_iso ?rf) f = y"
      by (simp add: Abs_lifted_distrib_lattice_top_inverse)
    {
      fix g
      have "Rep_lifted_distrib_lattice_top (dl_iso qf) g ≤ Rep_lifted_distrib_lattice_top (dl_iso ?rf) g"
      proof (cases "g = f")
        assume "g = f"
        thus ?thesis
          using 1 4 by simp
      next
        assume 5: "g ≠ f"
        have "(top,up_filter (get_dense ?rf g)) = Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (λg . if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g"
          by (metis (mono_tags, lifting) get_dense_char)
        also have "... = Rep_lifted_pair (Abs_lifted_pair (λg . if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) g"
          using 3 by (simp add: Abs_dense_inverse)
        also have "... = Rep_lifted_pair (Rep_dense qf) g"
          using 2 5 by (simp add: Abs_lifted_pair_inverse)
        also have "... = (top,up_filter (get_dense qf g))"
          using get_dense_char by auto
        finally have "get_dense ?rf g = get_dense qf g"
          using up_filter_injective by blast
        thus "Rep_lifted_distrib_lattice_top (dl_iso qf) g ≤ Rep_lifted_distrib_lattice_top (dl_iso ?rf) g"
          by (simp add: Abs_lifted_distrib_lattice_top_inverse)
      qed
    }
    hence "Rep_lifted_distrib_lattice_top (dl_iso qf) ≤ Rep_lifted_distrib_lattice_top (dl_iso ?rf)"
      by (simp add: le_funI)
    hence 6: "dl_iso qf ≤ dl_iso ?rf"
      by (simp add: le_funD less_eq_lifted_distrib_lattice_top.rep_eq)
    hence "qf ≤ ?rf"
      by (metis (no_types, lifting) dl_iso sup_isomorphism_ord_isomorphism)
    thus "∃rf . qf ≤ rf ∧ y = Rep_lifted_distrib_lattice_top (dl_iso rf) f"
      using 4 by auto
  qed
qed

text ‹
The commutativity property states that the same result is obtained in two ways by starting with a regular lifted pair ‹pf›:
\begin{itemize}
\item apply the Boolean algebra isomorphism to the pair; then apply a structure map ‹f› to obtain a filter of dense elements; or,
\item apply the structure map ‹stone_phi› to the pair; then apply the distributive lattice isomorphism lifted to the resulting filter.
\end{itemize}
›

lemma phi_iso:
  "Rep_phi f (Rep_lifted_boolean_algebra (ba_iso pf) f) = filter_map (λqf::('a::non_trivial_boolean_algebra,'b::distrib_lattice_top) lifted_pair dense . Rep_lifted_distrib_lattice_top (dl_iso qf) f) (stone_phi pf)"
proof -
  let ?r = "Rep_phi f"
  let ?ppf = "λg . triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)"
  have 1: "triple ?r"
    by (simp add: triple_def)
  have 2: "Rep_filter (?r (fst (Rep_lifted_pair (Rep_regular pf) f))) ⊆ { z . ∃qf . -Rep_regular pf ≤ Rep_dense qf ∧ z = get_dense qf f }"
  proof
    fix z
    obtain x where 3: "x = fst (Rep_lifted_pair (Rep_regular pf) f)"
      by simp
    assume "z ∈ Rep_filter (?r (fst (Rep_lifted_pair (Rep_regular pf) f)))"
    hence "↑z ⊆ Rep_filter (?r x)"
      using 3 filter_def by fastforce
    hence 4: "up_filter z ≤ ?r x"
      by (metis Rep_filter_cases Rep_filter_inverse less_eq_filter.rep_eq mem_Collect_eq up_filter)
    have 5: "∀g . ?ppf g ∈ triple.pairs (Rep_phi g)"
      by (metis (no_types) simp_lifted_pair uminus_lifted_pair.rep_eq)
    let ?zf = "λg . if g = f then (top,up_filter z) else triple.pairs_top"
    have 6: "∀g . ?zf g ∈ triple.pairs (Rep_phi g)"
    proof
      fix g :: "('a,'b) phi"
      have "triple (Rep_phi g)"
        by (simp add: triple_def)
      hence "(top,up_filter z) ∈ triple.pairs (Rep_phi g)"
        using triple.pairs_def by force
      thus "?zf g ∈ triple.pairs (Rep_phi g)"
        by (metis simp_lifted_pair top_lifted_pair.rep_eq)
    qed
    hence "-Abs_lifted_pair ?zf = Abs_lifted_pair (λg . triple.pairs_uminus (Rep_phi g) (?zf g))"
      by (subst uminus_lifted_pair.abs_eq) (simp_all add: eq_onp_same_args)
    also have "... = Abs_lifted_pair (λg . if g = f then triple.pairs_uminus (Rep_phi g) (top,up_filter z) else triple.pairs_uminus (Rep_phi g) triple.pairs_top)"
      by (rule arg_cong[where f=Abs_lifted_pair]) auto
    also have "... = Abs_lifted_pair (λg . triple.pairs_bot)"
      using 1 by (metis bot_lifted_pair.rep_eq dense_closed_top top_lifted_pair.rep_eq triple.pairs_uminus.simps uminus_lifted_pair.rep_eq)
    finally have 7: "Abs_lifted_pair ?zf ∈ dense_elements"
      by (simp add: bot_lifted_pair.abs_eq)
    let ?qf = "Abs_dense (Abs_lifted_pair ?zf)"
    have "∀g . triple.pairs_less_eq (?ppf g) (?zf g)"
    proof
      fix g
      show "triple.pairs_less_eq (?ppf g) (?zf g)"
      proof (cases "g = f")
        assume 8: "g = f"
        hence 9: "?ppf g = (-x,?r x)"
          using 1 3 by (metis prod.collapse triple.pairs_uminus.simps)
        have "triple.pairs_less_eq (-x,?r x) (top,up_filter z)"
          using 1 4 by (meson inf.bot_least triple.pairs_less_eq.simps)
        thus ?thesis
          using 8 9 by simp
      next
        assume 10: "g ≠ f"
        have "triple.pairs_less_eq (?ppf g) triple.pairs_top"
          using 1 by (metis (no_types, opaque_lifting) bot.extremum top_greatest prod.collapse triple_def triple.pairs_less_eq.simps triple.phi_bot)
        thus ?thesis
          using 10 by simp
      qed
    qed
    hence "Abs_lifted_pair ?ppf ≤ Abs_lifted_pair ?zf"
      using 5 6 by (subst less_eq_lifted_pair.abs_eq) (simp_all add: eq_onp_same_args)
    hence 11: "-Rep_regular pf ≤ Rep_dense ?qf"
      using 7 by (simp add: uminus_lifted_pair_def Abs_dense_inverse)
    have "(top,up_filter (get_dense ?qf f)) = Rep_lifted_pair (Rep_dense ?qf) f"
      by (metis get_dense_char)
    also have "... = (top,up_filter z)"
      using 6 7 Abs_dense_inverse Abs_lifted_pair_inverse by force
    finally have "z = get_dense ?qf f"
      using up_filter_injective by force
    thus "z ∈ { z . ∃qf . -Rep_regular pf ≤ Rep_dense qf ∧ z = get_dense qf f }"
      using 11 by auto
  qed
  have 12: "Rep_filter (?r (fst (Rep_lifted_pair (Rep_regular pf) f))) ⊇ { z . ∃qf . -Rep_regular pf ≤ Rep_dense qf ∧ z = get_dense qf f }"
  proof
    fix z
    assume "z ∈ { z . ∃qf . -Rep_regular pf ≤ Rep_dense qf ∧ z = get_dense qf f }"
    hence "∃qf . -Rep_regular pf ≤ Rep_dense qf ∧ z = get_dense qf f"
      by auto
    hence "triple.pairs_less_eq (Rep_lifted_pair (-Rep_regular pf) f) (top,up_filter z)"
      by (metis less_eq_lifted_pair.rep_eq get_dense_char)
    hence "up_filter z ≤ snd (Rep_lifted_pair (-Rep_regular pf) f)"
      using 1 by (metis (no_types, opaque_lifting) prod.collapse triple.pairs_less_eq.simps)
    also have "... = snd (?ppf f)"
      by (metis uminus_lifted_pair.rep_eq)
    also have "... = ?r (fst (Rep_lifted_pair (Rep_regular pf) f))"
      using 1 by (metis (no_types) prod.collapse prod.inject triple.pairs_uminus.simps)
    finally have "Rep_filter (up_filter z) ⊆ Rep_filter (?r (fst (Rep_lifted_pair (Rep_regular pf) f)))"
      by (simp add: less_eq_filter.rep_eq)
    hence "↑z ⊆ Rep_filter (?r (fst (Rep_lifted_pair (Rep_regular pf) f)))"
      by (metis Abs_filter_inverse mem_Collect_eq up_filter)
    thus "z ∈ Rep_filter (?r (fst (Rep_lifted_pair (Rep_regular pf) f)))"
      by blast
  qed
  have 13: "∀qf∈Rep_filter (stone_phi pf) . Rep_lifted_distrib_lattice_top (Abs_lifted_distrib_lattice_top (get_dense qf)) f = get_dense qf f"
    by (metis Abs_lifted_distrib_lattice_top_inverse UNIV_I UNIV_def)
  have "Rep_filter (?r (fst (Rep_lifted_pair (Rep_regular pf) f))) = { z . ∃qf∈stone_phi_base pf . z = get_dense qf f }"
    using 2 12 by simp
  hence "?r (fst (Rep_lifted_pair (Rep_regular pf) f)) = Abs_filter { z . ∃qf∈stone_phi_base pf . z = get_dense qf f }"
    by (metis Rep_filter_inverse)
  hence "?r (Rep_lifted_boolean_algebra (ba_iso pf) f) = Abs_filter { z . ∃qf∈Rep_filter (stone_phi pf) . z = Rep_lifted_distrib_lattice_top (dl_iso qf) f }"
    using 13 by (simp add: Abs_filter_inverse stone_phi_base_filter stone_phi_def Abs_lifted_boolean_algebra_inverse)
  thus ?thesis
    by (simp add: image_def)
qed

end