[STATEMENT]
lemma stone_phi_embed_injective:
  "inj stone_phi_embed"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj stone_phi_embed
[PROOF STEP]
proof (rule injI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. stone_phi_embed x = stone_phi_embed y \<Longrightarrow> x = y
[PROOF STEP]
fix x y :: "'a stone_phi_pair"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. stone_phi_embed x = stone_phi_embed y \<Longrightarrow> x = y
[PROOF STEP]
have 1: "Rep_phi (Abs_phi stone_phi) = stone_phi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_phi (Abs_phi stone_phi) = stone_phi
[PROOF STEP]
by (simp add: Abs_phi_inverse stone_phi.hom)
[PROOF STATE]
proof (state)
this:
Rep_phi (Abs_phi stone_phi) = stone_phi

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed x = stone_phi_embed y \<Longrightarrow> x = y
[PROOF STEP]
assume 2: "stone_phi_embed x = stone_phi_embed y"
[PROOF STATE]
proof (state)
this:
stone_phi_embed x = stone_phi_embed y

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed x = stone_phi_embed y \<Longrightarrow> x = y
[PROOF STEP]
have "\<forall>x::'a stone_phi_pair . Rep_lifted_pair (stone_phi_embed x) = (\<lambda>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)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. Rep_lifted_pair (stone_phi_embed x) = (\<lambda>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)))
[PROOF STEP]
by (simp add: Abs_lifted_pair_inverse stone_phi_embed_triple_pair)
[PROOF STATE]
proof (state)
this:
\<forall>x. Rep_lifted_pair (stone_phi_embed x) = (\<lambda>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)))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed x = stone_phi_embed y \<Longrightarrow> x = y
[PROOF STEP]
hence "(\<lambda>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))) = (\<lambda>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)))"
[PROOF STATE]
proof (prove)
using this:
\<forall>x. Rep_lifted_pair (stone_phi_embed x) = (\<lambda>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)))

goal (1 subgoal):
 1. (\<lambda>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))) = (\<lambda>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)))
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
\<forall>x. Rep_lifted_pair (stone_phi_embed x) = (\<lambda>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)))
stone_phi_embed x = stone_phi_embed y

goal (1 subgoal):
 1. (\<lambda>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))) = (\<lambda>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)))
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
(\<lambda>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))) = (\<lambda>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)))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed x = stone_phi_embed y \<Longrightarrow> x = y
[PROOF STEP]
hence "Rep_stone_phi_pair x = Rep_stone_phi_pair y"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>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))) = (\<lambda>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)))

goal (1 subgoal):
 1. Rep_stone_phi_pair x = Rep_stone_phi_pair y
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
(\<lambda>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))) = (\<lambda>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)))
Rep_phi (Abs_phi stone_phi) = stone_phi

goal (1 subgoal):
 1. Rep_stone_phi_pair x = Rep_stone_phi_pair y
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
Rep_stone_phi_pair x = Rep_stone_phi_pair y

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed x = stone_phi_embed y \<Longrightarrow> x = y
[PROOF STEP]
thus "x = y"
[PROOF STATE]
proof (prove)
using this:
Rep_stone_phi_pair x = Rep_stone_phi_pair y

goal (1 subgoal):
 1. x = y
[PROOF STEP]
by (simp add: Rep_stone_phi_pair_inject)
[PROOF STATE]
proof (state)
this:
x = y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stone_phi_embed_order_injective:
  assumes "stone_phi_embed x \<le> stone_phi_embed y"
    shows "x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
let ?f = "Abs_phi stone_phi"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
have "\<forall>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)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f. stone_phi.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)))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
stone_phi_embed x \<le> stone_phi_embed y

goal (1 subgoal):
 1. \<forall>f. stone_phi.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)))
[PROOF STEP]
by (subst less_eq_lifted_pair.abs_eq[THEN sym]) (simp_all add: eq_onp_same_args stone_phi_embed_triple_pair)
[PROOF STATE]
proof (state)
this:
\<forall>f. stone_phi.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)))

goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
hence "triple.pairs_less_eq (if Rep_phi ?f = (stone_phi::'a regular \<Rightarrow> '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 \<Rightarrow> '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)))"
[PROOF STATE]
proof (prove)
using this:
\<forall>f. stone_phi.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)))

goal (1 subgoal):
 1. stone_phi.pairs_less_eq (if Rep_phi (Abs_phi stone_phi) = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi (Abs_phi stone_phi)) (triple.pairs_uminus (Rep_phi (Abs_phi stone_phi)) (Rep_stone_phi_pair x))) (if Rep_phi (Abs_phi stone_phi) = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi (Abs_phi stone_phi)) (triple.pairs_uminus (Rep_phi (Abs_phi stone_phi)) (Rep_stone_phi_pair y)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stone_phi.pairs_less_eq (if Rep_phi (Abs_phi stone_phi) = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi (Abs_phi stone_phi)) (triple.pairs_uminus (Rep_phi (Abs_phi stone_phi)) (Rep_stone_phi_pair x))) (if Rep_phi (Abs_phi stone_phi) = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi (Abs_phi stone_phi)) (triple.pairs_uminus (Rep_phi (Abs_phi stone_phi)) (Rep_stone_phi_pair y)))

goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
hence "triple.pairs_less_eq (Rep_stone_phi_pair x) (Rep_stone_phi_pair y)"
[PROOF STATE]
proof (prove)
using this:
stone_phi.pairs_less_eq (if Rep_phi (Abs_phi stone_phi) = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi (Abs_phi stone_phi)) (triple.pairs_uminus (Rep_phi (Abs_phi stone_phi)) (Rep_stone_phi_pair x))) (if Rep_phi (Abs_phi stone_phi) = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi (Abs_phi stone_phi)) (triple.pairs_uminus (Rep_phi (Abs_phi stone_phi)) (Rep_stone_phi_pair y)))

goal (1 subgoal):
 1. stone_phi.pairs_less_eq (Rep_stone_phi_pair x) (Rep_stone_phi_pair y)
[PROOF STEP]
by (simp add: Abs_phi_inverse stone_phi.hom)
[PROOF STATE]
proof (state)
this:
stone_phi.pairs_less_eq (Rep_stone_phi_pair x) (Rep_stone_phi_pair y)

goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
thus "x \<le> y"
[PROOF STATE]
proof (prove)
using this:
stone_phi.pairs_less_eq (Rep_stone_phi_pair x) (Rep_stone_phi_pair y)

goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
by (simp add: less_eq_stone_phi_pair.rep_eq)
[PROOF STATE]
proof (state)
this:
x \<le> y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stone_phi_embed_strict_order_isomorphism:
  "x < y \<longleftrightarrow> stone_phi_embed x < stone_phi_embed y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x < y) = (stone_phi_embed x < stone_phi_embed y)
[PROOF STEP]
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)


[STATEMENT]
lemma sa_iso_triple_pair:
  "(Abs_regular (--x),stone_phi (Abs_regular (-x)) \<squnion> up_filter (Abs_dense (x \<squnion> -x))) \<in> triple.pairs stone_phi"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<in> stone_phi.pairs
[PROOF STEP]
by (metis (mono_tags, lifting) double_compl eq_onp_same_args stone_phi.sa_iso_pair uminus_regular.abs_eq)


[STATEMENT]
lemma stone_phi_inf_dense:
  "stone_phi (Abs_regular (-x)) \<sqinter> up_filter (Abs_dense (y \<squnion> -y)) \<le> up_filter (Abs_dense (y \<squnion> -y \<squnion> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)) \<le> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)) \<le> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))
[PROOF STEP]
have "Rep_filter (stone_phi (Abs_regular (-x)) \<sqinter> up_filter (Abs_dense (y \<squnion> -y))) \<le> \<up>(Abs_dense (y \<squnion> -y \<squnion> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<subseteq> \<up>Abs_dense (y \<squnion> - y \<squnion> x)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<Longrightarrow> xa \<in> \<up>Abs_dense (y \<squnion> - y \<squnion> x)
[PROOF STEP]
fix z :: "'a dense"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<Longrightarrow> xa \<in> \<up>Abs_dense (y \<squnion> - y \<squnion> x)
[PROOF STEP]
let ?r = "Rep_dense z"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<Longrightarrow> xa \<in> \<up>Abs_dense (y \<squnion> - y \<squnion> x)
[PROOF STEP]
assume "z \<in> Rep_filter (stone_phi (Abs_regular (-x)) \<sqinter> up_filter (Abs_dense (y \<squnion> -y)))"
[PROOF STATE]
proof (state)
this:
z \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)))

goal (1 subgoal):
 1. \<And>xa. xa \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<Longrightarrow> xa \<in> \<up>Abs_dense (y \<squnion> - y \<squnion> x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
z \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)))

goal (1 subgoal):
 1. \<And>xa. xa \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<Longrightarrow> xa \<in> \<up>Abs_dense (y \<squnion> - y \<squnion> x)
[PROOF STEP]
have "... = Rep_filter (stone_phi (Abs_regular (-x))) \<inter> Rep_filter (up_filter (Abs_dense (y \<squnion> -y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) = Filters.filter.Rep_filter (stone_phi (Abs_regular (- x))) \<inter> Filters.filter.Rep_filter (up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
by (simp add: inf_filter.rep_eq)
[PROOF STATE]
proof (state)
this:
Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) = Filters.filter.Rep_filter (stone_phi (Abs_regular (- x))) \<inter> Filters.filter.Rep_filter (up_filter (Abs_dense (y \<squnion> - y)))

goal (1 subgoal):
 1. \<And>xa. xa \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<Longrightarrow> xa \<in> \<up>Abs_dense (y \<squnion> - y \<squnion> x)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) = Filters.filter.Rep_filter (stone_phi (Abs_regular (- x))) \<inter> Filters.filter.Rep_filter (up_filter (Abs_dense (y \<squnion> - y)))

goal (1 subgoal):
 1. \<And>xa. xa \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<Longrightarrow> xa \<in> \<up>Abs_dense (y \<squnion> - y \<squnion> x)
[PROOF STEP]
have "... = stone_phi_base (Abs_regular (-x)) \<inter> \<up>(Abs_dense (y \<squnion> -y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Filters.filter.Rep_filter (stone_phi (Abs_regular (- x))) \<inter> Filters.filter.Rep_filter (up_filter (Abs_dense (y \<squnion> - y))) = stone_phi_base (Abs_regular (- x)) \<inter> \<up>Abs_dense (y \<squnion> - y)
[PROOF STEP]
by (metis Abs_filter_inverse mem_Collect_eq up_filter stone_phi_base_filter stone_phi_def)
[PROOF STATE]
proof (state)
this:
Filters.filter.Rep_filter (stone_phi (Abs_regular (- x))) \<inter> Filters.filter.Rep_filter (up_filter (Abs_dense (y \<squnion> - y))) = stone_phi_base (Abs_regular (- x)) \<inter> \<up>Abs_dense (y \<squnion> - y)

goal (1 subgoal):
 1. \<And>xa. xa \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<Longrightarrow> xa \<in> \<up>Abs_dense (y \<squnion> - y \<squnion> x)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
z \<in> stone_phi_base (Abs_regular (- x)) \<inter> \<up>Abs_dense (y \<squnion> - y)
[PROOF STEP]
have "--x \<le> ?r \<and> Abs_dense (y \<squnion> -y) \<le> z"
[PROOF STATE]
proof (prove)
using this:
z \<in> stone_phi_base (Abs_regular (- x)) \<inter> \<up>Abs_dense (y \<squnion> - y)

goal (1 subgoal):
 1. - - x \<le> Rep_dense z \<and> Abs_dense (y \<squnion> - y) \<le> z
[PROOF STEP]
by (metis (mono_tags, lifting) Abs_regular_inverse Int_Collect mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
- - x \<le> Rep_dense z \<and> Abs_dense (y \<squnion> - y) \<le> z

goal (1 subgoal):
 1. \<And>xa. xa \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<Longrightarrow> xa \<in> \<up>Abs_dense (y \<squnion> - y \<squnion> x)
[PROOF STEP]
hence "--x \<le> ?r \<and> y \<squnion> -y \<le> ?r"
[PROOF STATE]
proof (prove)
using this:
- - x \<le> Rep_dense z \<and> Abs_dense (y \<squnion> - y) \<le> z

goal (1 subgoal):
 1. - - x \<le> Rep_dense z \<and> y \<squnion> - y \<le> Rep_dense z
[PROOF STEP]
by (simp add: Abs_dense_inverse less_eq_dense.rep_eq)
[PROOF STATE]
proof (state)
this:
- - x \<le> Rep_dense z \<and> y \<squnion> - y \<le> Rep_dense z

goal (1 subgoal):
 1. \<And>xa. xa \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<Longrightarrow> xa \<in> \<up>Abs_dense (y \<squnion> - y \<squnion> x)
[PROOF STEP]
hence "y \<squnion> -y \<squnion> x \<le> ?r"
[PROOF STATE]
proof (prove)
using this:
- - x \<le> Rep_dense z \<and> y \<squnion> - y \<le> Rep_dense z

goal (1 subgoal):
 1. y \<squnion> - y \<squnion> x \<le> Rep_dense z
[PROOF STEP]
using order_trans pp_increasing
[PROOF STATE]
proof (prove)
using this:
- - x \<le> Rep_dense z \<and> y \<squnion> - y \<le> Rep_dense z
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z
?x \<le> - - ?x

goal (1 subgoal):
 1. y \<squnion> - y \<squnion> x \<le> Rep_dense z
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<squnion> - y \<squnion> x \<le> Rep_dense z

goal (1 subgoal):
 1. \<And>xa. xa \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<Longrightarrow> xa \<in> \<up>Abs_dense (y \<squnion> - y \<squnion> x)
[PROOF STEP]
hence "Abs_dense (y \<squnion> -y \<squnion> x) \<le> Abs_dense ?r"
[PROOF STATE]
proof (prove)
using this:
y \<squnion> - y \<squnion> x \<le> Rep_dense z

goal (1 subgoal):
 1. Abs_dense (y \<squnion> - y \<squnion> x) \<le> Abs_dense (Rep_dense z)
[PROOF STEP]
by (subst less_eq_dense.abs_eq) (simp_all add: eq_onp_same_args)
[PROOF STATE]
proof (state)
this:
Abs_dense (y \<squnion> - y \<squnion> x) \<le> Abs_dense (Rep_dense z)

goal (1 subgoal):
 1. \<And>xa. xa \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<Longrightarrow> xa \<in> \<up>Abs_dense (y \<squnion> - y \<squnion> x)
[PROOF STEP]
thus "z \<in> \<up>(Abs_dense (y \<squnion> -y \<squnion> x))"
[PROOF STATE]
proof (prove)
using this:
Abs_dense (y \<squnion> - y \<squnion> x) \<le> Abs_dense (Rep_dense z)

goal (1 subgoal):
 1. z \<in> \<up>Abs_dense (y \<squnion> - y \<squnion> x)
[PROOF STEP]
by (simp add: Rep_dense_inverse)
[PROOF STATE]
proof (state)
this:
z \<in> \<up>Abs_dense (y \<squnion> - y \<squnion> x)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<subseteq> \<up>Abs_dense (y \<squnion> - y \<squnion> x)

goal (1 subgoal):
 1. stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)) \<le> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))
[PROOF STEP]
hence "Abs_filter (Rep_filter (stone_phi (Abs_regular (-x)) \<sqinter> up_filter (Abs_dense (y \<squnion> -y)))) \<le> up_filter (Abs_dense (y \<squnion> -y \<squnion> x))"
[PROOF STATE]
proof (prove)
using this:
Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<subseteq> \<up>Abs_dense (y \<squnion> - y \<squnion> x)

goal (1 subgoal):
 1. Filters.filter.Abs_filter (Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)))) \<le> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))
[PROOF STEP]
by (simp add: eq_onp_same_args less_eq_filter.abs_eq)
[PROOF STATE]
proof (state)
this:
Filters.filter.Abs_filter (Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)))) \<le> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))

goal (1 subgoal):
 1. stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)) \<le> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Filters.filter.Abs_filter (Filters.filter.Rep_filter (stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)))) \<le> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))

goal (1 subgoal):
 1. stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)) \<le> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))
[PROOF STEP]
by (simp add: Rep_filter_inverse)
[PROOF STATE]
proof (state)
this:
stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)) \<le> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma stone_phi_complement:
  "complement (stone_phi (Abs_regular (-x))) (stone_phi (Abs_regular (--x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. complement (stone_phi (Abs_regular (- x))) (stone_phi (Abs_regular (- - x)))
[PROOF STEP]
by (metis (mono_tags, lifting) eq_onp_same_args stone_phi.phi_complemented uminus_regular.abs_eq)


[STATEMENT]
lemma up_dense_stone_phi:
  "up_filter (Abs_dense (x \<squnion> -x)) \<le> stone_phi (Abs_regular (--x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. up_filter (Abs_dense (x \<squnion> - x)) \<le> stone_phi (Abs_regular (- - x))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. up_filter (Abs_dense (x \<squnion> - x)) \<le> stone_phi (Abs_regular (- - x))
[PROOF STEP]
have "\<up>(Abs_dense (x \<squnion> -x)) \<le> stone_phi_base (Abs_regular (--x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<up>Abs_dense (x \<squnion> - x) \<subseteq> stone_phi_base (Abs_regular (- - x))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> \<up>Abs_dense (x \<squnion> - x) \<Longrightarrow> xa \<in> stone_phi_base (Abs_regular (- - x))
[PROOF STEP]
fix z :: "'a dense"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> \<up>Abs_dense (x \<squnion> - x) \<Longrightarrow> xa \<in> stone_phi_base (Abs_regular (- - x))
[PROOF STEP]
let ?r = "Rep_dense z"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> \<up>Abs_dense (x \<squnion> - x) \<Longrightarrow> xa \<in> stone_phi_base (Abs_regular (- - x))
[PROOF STEP]
assume "z \<in> \<up>(Abs_dense (x \<squnion> -x))"
[PROOF STATE]
proof (state)
this:
z \<in> \<up>Abs_dense (x \<squnion> - x)

goal (1 subgoal):
 1. \<And>xa. xa \<in> \<up>Abs_dense (x \<squnion> - x) \<Longrightarrow> xa \<in> stone_phi_base (Abs_regular (- - x))
[PROOF STEP]
hence "---x \<le> ?r"
[PROOF STATE]
proof (prove)
using this:
z \<in> \<up>Abs_dense (x \<squnion> - x)

goal (1 subgoal):
 1. - - - x \<le> Rep_dense z
[PROOF STEP]
by (simp add: Abs_dense_inverse less_eq_dense.rep_eq)
[PROOF STATE]
proof (state)
this:
- - - x \<le> Rep_dense z

goal (1 subgoal):
 1. \<And>xa. xa \<in> \<up>Abs_dense (x \<squnion> - x) \<Longrightarrow> xa \<in> stone_phi_base (Abs_regular (- - x))
[PROOF STEP]
hence "-Rep_regular (Abs_regular (--x)) \<le> ?r"
[PROOF STATE]
proof (prove)
using this:
- - - x \<le> Rep_dense z

goal (1 subgoal):
 1. - Rep_regular (Abs_regular (- - x)) \<le> Rep_dense z
[PROOF STEP]
by (metis (mono_tags, lifting) Abs_regular_inverse mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
- Rep_regular (Abs_regular (- - x)) \<le> Rep_dense z

goal (1 subgoal):
 1. \<And>xa. xa \<in> \<up>Abs_dense (x \<squnion> - x) \<Longrightarrow> xa \<in> stone_phi_base (Abs_regular (- - x))
[PROOF STEP]
thus "z \<in> stone_phi_base (Abs_regular (--x))"
[PROOF STATE]
proof (prove)
using this:
- Rep_regular (Abs_regular (- - x)) \<le> Rep_dense z

goal (1 subgoal):
 1. z \<in> stone_phi_base (Abs_regular (- - x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
z \<in> stone_phi_base (Abs_regular (- - x))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<up>Abs_dense (x \<squnion> - x) \<subseteq> stone_phi_base (Abs_regular (- - x))

goal (1 subgoal):
 1. up_filter (Abs_dense (x \<squnion> - x)) \<le> stone_phi (Abs_regular (- - x))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<up>Abs_dense (x \<squnion> - x) \<subseteq> stone_phi_base (Abs_regular (- - x))

goal (1 subgoal):
 1. up_filter (Abs_dense (x \<squnion> - x)) \<le> stone_phi (Abs_regular (- - x))
[PROOF STEP]
by (unfold stone_phi_def, subst less_eq_filter.abs_eq, simp_all add: eq_onp_same_args stone_phi_base_filter)
[PROOF STATE]
proof (state)
this:
up_filter (Abs_dense (x \<squnion> - x)) \<le> stone_phi (Abs_regular (- - x))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sa_iso_left_invertible:
  "sa_iso_inv (sa_iso x) = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sa_iso_inv (sa_iso x) = x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sa_iso_inv (sa_iso x) = x
[PROOF STEP]
have "up_filter (triple.rho_pair stone_phi (Abs_regular (--x),stone_phi (Abs_regular (-x)) \<squnion> up_filter (Abs_dense (x \<squnion> -x)))) = stone_phi (Abs_regular (--x)) \<sqinter> (stone_phi (Abs_regular (-x)) \<squnion> up_filter (Abs_dense (x \<squnion> -x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. up_filter (stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) = stone_phi (Abs_regular (- - x)) \<sqinter> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))
[PROOF STEP]
using sa_iso_triple_pair stone_phi.get_rho_pair_char
[PROOF STATE]
proof (prove)
using this:
(Abs_regular (- - ?x), stone_phi (Abs_regular (- ?x)) \<squnion> up_filter (Abs_dense (?x \<squnion> - ?x))) \<in> stone_phi.pairs
(?x, ?y) \<in> stone_phi.pairs \<Longrightarrow> up_filter (stone_phi.rho_pair (?x, ?y)) = stone_phi ?x \<sqinter> ?y

goal (1 subgoal):
 1. up_filter (stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) = stone_phi (Abs_regular (- - x)) \<sqinter> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
up_filter (stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) = stone_phi (Abs_regular (- - x)) \<sqinter> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))

goal (1 subgoal):
 1. sa_iso_inv (sa_iso x) = x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
up_filter (stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) = stone_phi (Abs_regular (- - x)) \<sqinter> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))

goal (1 subgoal):
 1. sa_iso_inv (sa_iso x) = x
[PROOF STEP]
have "... = stone_phi (Abs_regular (--x)) \<sqinter> up_filter (Abs_dense (x \<squnion> -x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi (Abs_regular (- - x)) \<sqinter> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) = stone_phi (Abs_regular (- - x)) \<sqinter> up_filter (Abs_dense (x \<squnion> - x))
[PROOF STEP]
by (simp add: inf.sup_commute inf_sup_distrib1 stone_phi_complement)
[PROOF STATE]
proof (state)
this:
stone_phi (Abs_regular (- - x)) \<sqinter> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) = stone_phi (Abs_regular (- - x)) \<sqinter> up_filter (Abs_dense (x \<squnion> - x))

goal (1 subgoal):
 1. sa_iso_inv (sa_iso x) = x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
stone_phi (Abs_regular (- - x)) \<sqinter> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) = stone_phi (Abs_regular (- - x)) \<sqinter> up_filter (Abs_dense (x \<squnion> - x))

goal (1 subgoal):
 1. sa_iso_inv (sa_iso x) = x
[PROOF STEP]
have "... = up_filter (Abs_dense (x \<squnion> -x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi (Abs_regular (- - x)) \<sqinter> up_filter (Abs_dense (x \<squnion> - x)) = up_filter (Abs_dense (x \<squnion> - x))
[PROOF STEP]
using up_dense_stone_phi inf.absorb2
[PROOF STATE]
proof (prove)
using this:
up_filter (Abs_dense (?x \<squnion> - ?x)) \<le> stone_phi (Abs_regular (- - ?x))
?b \<le> ?a \<Longrightarrow> ?a \<sqinter> ?b = ?b

goal (1 subgoal):
 1. stone_phi (Abs_regular (- - x)) \<sqinter> up_filter (Abs_dense (x \<squnion> - x)) = up_filter (Abs_dense (x \<squnion> - x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
stone_phi (Abs_regular (- - x)) \<sqinter> up_filter (Abs_dense (x \<squnion> - x)) = up_filter (Abs_dense (x \<squnion> - x))

goal (1 subgoal):
 1. sa_iso_inv (sa_iso x) = x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
up_filter (stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) = up_filter (Abs_dense (x \<squnion> - x))
[PROOF STEP]
have 1: "triple.rho_pair stone_phi (Abs_regular (--x),stone_phi (Abs_regular (-x)) \<squnion> up_filter (Abs_dense (x \<squnion> -x))) = Abs_dense (x \<squnion> -x)"
[PROOF STATE]
proof (prove)
using this:
up_filter (stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) = up_filter (Abs_dense (x \<squnion> - x))

goal (1 subgoal):
 1. stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) = Abs_dense (x \<squnion> - x)
[PROOF STEP]
using up_filter_injective
[PROOF STATE]
proof (prove)
using this:
up_filter (stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) = up_filter (Abs_dense (x \<squnion> - x))
up_filter ?x = up_filter ?y \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) = Abs_dense (x \<squnion> - x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) = Abs_dense (x \<squnion> - x)

goal (1 subgoal):
 1. sa_iso_inv (sa_iso x) = x
[PROOF STEP]
have "sa_iso_inv (sa_iso x) = (\<lambda>p . Rep_regular (fst p) \<sqinter> Rep_dense (triple.rho_pair stone_phi p)) (Abs_regular (--x),stone_phi (Abs_regular (-x)) \<squnion> up_filter (Abs_dense (x \<squnion> -x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sa_iso_inv (sa_iso x) = Rep_regular (fst (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) \<sqinter> Rep_dense (stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))))
[PROOF STEP]
by (simp add: Abs_stone_phi_pair_inverse sa_iso_triple_pair)
[PROOF STATE]
proof (state)
this:
sa_iso_inv (sa_iso x) = Rep_regular (fst (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) \<sqinter> Rep_dense (stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))))

goal (1 subgoal):
 1. sa_iso_inv (sa_iso x) = x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sa_iso_inv (sa_iso x) = Rep_regular (fst (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) \<sqinter> Rep_dense (stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))))

goal (1 subgoal):
 1. sa_iso_inv (sa_iso x) = x
[PROOF STEP]
have "... = Rep_regular (Abs_regular (--x)) \<sqinter> Rep_dense (triple.rho_pair stone_phi (Abs_regular (--x),stone_phi (Abs_regular (-x)) \<squnion> up_filter (Abs_dense (x \<squnion> -x))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_regular (fst (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) \<sqinter> Rep_dense (stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) = Rep_regular (Abs_regular (- - x)) \<sqinter> Rep_dense (stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Rep_regular (fst (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) \<sqinter> Rep_dense (stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) = Rep_regular (Abs_regular (- - x)) \<sqinter> Rep_dense (stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))))

goal (1 subgoal):
 1. sa_iso_inv (sa_iso x) = x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Rep_regular (fst (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) \<sqinter> Rep_dense (stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) = Rep_regular (Abs_regular (- - x)) \<sqinter> Rep_dense (stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))))

goal (1 subgoal):
 1. sa_iso_inv (sa_iso x) = x
[PROOF STEP]
have "... = --x \<sqinter> Rep_dense (Abs_dense (x \<squnion> -x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_regular (Abs_regular (- - x)) \<sqinter> Rep_dense (stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) = - - x \<sqinter> Rep_dense (Abs_dense (x \<squnion> - x))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) = Abs_dense (x \<squnion> - x)

goal (1 subgoal):
 1. Rep_regular (Abs_regular (- - x)) \<sqinter> Rep_dense (stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) = - - x \<sqinter> Rep_dense (Abs_dense (x \<squnion> - x))
[PROOF STEP]
by (subst Abs_regular_inverse) auto
[PROOF STATE]
proof (state)
this:
Rep_regular (Abs_regular (- - x)) \<sqinter> Rep_dense (stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) = - - x \<sqinter> Rep_dense (Abs_dense (x \<squnion> - x))

goal (1 subgoal):
 1. sa_iso_inv (sa_iso x) = x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Rep_regular (Abs_regular (- - x)) \<sqinter> Rep_dense (stone_phi.rho_pair (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) = - - x \<sqinter> Rep_dense (Abs_dense (x \<squnion> - x))

goal (1 subgoal):
 1. sa_iso_inv (sa_iso x) = x
[PROOF STEP]
have "... = --x \<sqinter> (x \<squnion> -x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - - x \<sqinter> Rep_dense (Abs_dense (x \<squnion> - x)) = - - x \<sqinter> (x \<squnion> - x)
[PROOF STEP]
by (subst Abs_dense_inverse) simp_all
[PROOF STATE]
proof (state)
this:
- - x \<sqinter> Rep_dense (Abs_dense (x \<squnion> - x)) = - - x \<sqinter> (x \<squnion> - x)

goal (1 subgoal):
 1. sa_iso_inv (sa_iso x) = x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- - x \<sqinter> Rep_dense (Abs_dense (x \<squnion> - x)) = - - x \<sqinter> (x \<squnion> - x)

goal (1 subgoal):
 1. sa_iso_inv (sa_iso x) = x
[PROOF STEP]
have "... = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - - x \<sqinter> (x \<squnion> - x) = x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- - x \<sqinter> (x \<squnion> - x) = x

goal (1 subgoal):
 1. sa_iso_inv (sa_iso x) = x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sa_iso_inv (sa_iso x) = x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sa_iso_inv (sa_iso x) = x

goal (1 subgoal):
 1. sa_iso_inv (sa_iso x) = x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sa_iso_inv (sa_iso x) = x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sa_iso_right_invertible:
  "sa_iso (sa_iso_inv p) = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
obtain x y where 1: "(x,y) = Rep_stone_phi_pair p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. (x, y) = Rep_stone_phi_pair p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. (\<And>x y. (x, y) = Rep_stone_phi_pair p \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(x, y) = Rep_stone_phi_pair p

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
hence 2: "(x,y) \<in> triple.pairs stone_phi"
[PROOF STATE]
proof (prove)
using this:
(x, y) = Rep_stone_phi_pair p

goal (1 subgoal):
 1. (x, y) \<in> stone_phi.pairs
[PROOF STEP]
by (simp add: Rep_stone_phi_pair)
[PROOF STATE]
proof (state)
this:
(x, y) \<in> stone_phi.pairs

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
hence 3: "stone_phi (-x) \<le> y"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> stone_phi.pairs

goal (1 subgoal):
 1. stone_phi (- x) \<le> y
[PROOF STEP]
by (simp add: stone_phi.pairs_phi_less_eq)
[PROOF STATE]
proof (state)
this:
stone_phi (- x) \<le> y

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
have 4: "\<forall>z . z \<in> Rep_filter (stone_phi x \<sqinter> y) \<longrightarrow> -Rep_regular x \<le> Rep_dense z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>z. z \<in> Filters.filter.Rep_filter (stone_phi x \<sqinter> y) \<longrightarrow> - Rep_regular x \<le> Rep_dense z
[PROOF STEP]
proof (rule allI, rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. z \<in> Filters.filter.Rep_filter (stone_phi x \<sqinter> y) \<Longrightarrow> - Rep_regular x \<le> Rep_dense z
[PROOF STEP]
fix z :: "'a dense"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. z \<in> Filters.filter.Rep_filter (stone_phi x \<sqinter> y) \<Longrightarrow> - Rep_regular x \<le> Rep_dense z
[PROOF STEP]
let ?r = "Rep_dense z"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. z \<in> Filters.filter.Rep_filter (stone_phi x \<sqinter> y) \<Longrightarrow> - Rep_regular x \<le> Rep_dense z
[PROOF STEP]
assume "z \<in> Rep_filter (stone_phi x \<sqinter> y)"
[PROOF STATE]
proof (state)
this:
z \<in> Filters.filter.Rep_filter (stone_phi x \<sqinter> y)

goal (1 subgoal):
 1. \<And>z. z \<in> Filters.filter.Rep_filter (stone_phi x \<sqinter> y) \<Longrightarrow> - Rep_regular x \<le> Rep_dense z
[PROOF STEP]
hence "z \<in> Rep_filter (stone_phi x)"
[PROOF STATE]
proof (prove)
using this:
z \<in> Filters.filter.Rep_filter (stone_phi x \<sqinter> y)

goal (1 subgoal):
 1. z \<in> Filters.filter.Rep_filter (stone_phi x)
[PROOF STEP]
by (simp add: inf_filter.rep_eq)
[PROOF STATE]
proof (state)
this:
z \<in> Filters.filter.Rep_filter (stone_phi x)

goal (1 subgoal):
 1. \<And>z. z \<in> Filters.filter.Rep_filter (stone_phi x \<sqinter> y) \<Longrightarrow> - Rep_regular x \<le> Rep_dense z
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
z \<in> Filters.filter.Rep_filter (stone_phi x)

goal (1 subgoal):
 1. \<And>z. z \<in> Filters.filter.Rep_filter (stone_phi x \<sqinter> y) \<Longrightarrow> - Rep_regular x \<le> Rep_dense z
[PROOF STEP]
have "... = stone_phi_base x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Filters.filter.Rep_filter (stone_phi x) = stone_phi_base x
[PROOF STEP]
by (simp add: stone_phi_def Abs_filter_inverse stone_phi_base_filter)
[PROOF STATE]
proof (state)
this:
Filters.filter.Rep_filter (stone_phi x) = stone_phi_base x

goal (1 subgoal):
 1. \<And>z. z \<in> Filters.filter.Rep_filter (stone_phi x \<sqinter> y) \<Longrightarrow> - Rep_regular x \<le> Rep_dense z
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
z \<in> stone_phi_base x
[PROOF STEP]
show "-Rep_regular x \<le> ?r"
[PROOF STATE]
proof (prove)
using this:
z \<in> stone_phi_base x

goal (1 subgoal):
 1. - Rep_regular x \<le> Rep_dense z
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- Rep_regular x \<le> Rep_dense z

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>z. z \<in> Filters.filter.Rep_filter (stone_phi x \<sqinter> y) \<longrightarrow> - Rep_regular x \<le> Rep_dense z

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
have "triple.rho_pair stone_phi (x,y) \<in> \<up>(triple.rho_pair stone_phi (x,y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi.rho_pair (x, y) \<in> \<up>stone_phi.rho_pair (x, y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stone_phi.rho_pair (x, y) \<in> \<up>stone_phi.rho_pair (x, y)

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
stone_phi.rho_pair (x, y) \<in> \<up>stone_phi.rho_pair (x, y)

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
have "... = Rep_filter (Abs_filter (\<up>(triple.rho_pair stone_phi (x,y))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<up>stone_phi.rho_pair (x, y) = Filters.filter.Rep_filter (up_filter (stone_phi.rho_pair (x, y)))
[PROOF STEP]
by (simp add: Abs_filter_inverse)
[PROOF STATE]
proof (state)
this:
\<up>stone_phi.rho_pair (x, y) = Filters.filter.Rep_filter (up_filter (stone_phi.rho_pair (x, y)))

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<up>stone_phi.rho_pair (x, y) = Filters.filter.Rep_filter (up_filter (stone_phi.rho_pair (x, y)))

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
have "... = Rep_filter (stone_phi x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Filters.filter.Rep_filter (up_filter (stone_phi.rho_pair (x, y))) = Filters.filter.Rep_filter (stone_phi x \<sqinter> y)
[PROOF STEP]
using 2 stone_phi.get_rho_pair_char
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> stone_phi.pairs
(?x, ?y) \<in> stone_phi.pairs \<Longrightarrow> up_filter (stone_phi.rho_pair (?x, ?y)) = stone_phi ?x \<sqinter> ?y

goal (1 subgoal):
 1. Filters.filter.Rep_filter (up_filter (stone_phi.rho_pair (x, y))) = Filters.filter.Rep_filter (stone_phi x \<sqinter> y)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Filters.filter.Rep_filter (up_filter (stone_phi.rho_pair (x, y))) = Filters.filter.Rep_filter (stone_phi x \<sqinter> y)

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
stone_phi.rho_pair (x, y) \<in> Filters.filter.Rep_filter (stone_phi x \<sqinter> y)
[PROOF STEP]
have "triple.rho_pair stone_phi (x,y) \<in> Rep_filter (stone_phi x \<sqinter> y)"
[PROOF STATE]
proof (prove)
using this:
stone_phi.rho_pair (x, y) \<in> Filters.filter.Rep_filter (stone_phi x \<sqinter> y)

goal (1 subgoal):
 1. stone_phi.rho_pair (x, y) \<in> Filters.filter.Rep_filter (stone_phi x \<sqinter> y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stone_phi.rho_pair (x, y) \<in> Filters.filter.Rep_filter (stone_phi x \<sqinter> y)

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
hence 5: "-Rep_regular x \<le> Rep_dense (triple.rho_pair stone_phi (x,y))"
[PROOF STATE]
proof (prove)
using this:
stone_phi.rho_pair (x, y) \<in> Filters.filter.Rep_filter (stone_phi x \<sqinter> y)

goal (1 subgoal):
 1. - Rep_regular x \<le> Rep_dense (stone_phi.rho_pair (x, y))
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
stone_phi.rho_pair (x, y) \<in> Filters.filter.Rep_filter (stone_phi x \<sqinter> y)
\<forall>z. z \<in> Filters.filter.Rep_filter (stone_phi x \<sqinter> y) \<longrightarrow> - Rep_regular x \<le> Rep_dense z

goal (1 subgoal):
 1. - Rep_regular x \<le> Rep_dense (stone_phi.rho_pair (x, y))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- Rep_regular x \<le> Rep_dense (stone_phi.rho_pair (x, y))

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
have 6: "sa_iso_inv p = Rep_regular x \<sqinter> Rep_dense (triple.rho_pair stone_phi (x,y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sa_iso_inv p = Rep_regular x \<sqinter> Rep_dense (stone_phi.rho_pair (x, y))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
(x, y) = Rep_stone_phi_pair p

goal (1 subgoal):
 1. sa_iso_inv p = Rep_regular x \<sqinter> Rep_dense (stone_phi.rho_pair (x, y))
[PROOF STEP]
by (metis fstI)
[PROOF STATE]
proof (state)
this:
sa_iso_inv p = Rep_regular x \<sqinter> Rep_dense (stone_phi.rho_pair (x, y))

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
hence "-sa_iso_inv p = -Rep_regular x"
[PROOF STATE]
proof (prove)
using this:
sa_iso_inv p = Rep_regular x \<sqinter> Rep_dense (stone_phi.rho_pair (x, y))

goal (1 subgoal):
 1. - sa_iso_inv p = - Rep_regular x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- sa_iso_inv p = - Rep_regular x

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
hence "sa_iso (sa_iso_inv p) = Abs_stone_phi_pair (Abs_regular (--Rep_regular x),stone_phi (Abs_regular (-Rep_regular x)) \<squnion> up_filter (Abs_dense ((Rep_regular x \<sqinter> Rep_dense (triple.rho_pair stone_phi (x,y))) \<squnion> -Rep_regular x)))"
[PROOF STATE]
proof (prove)
using this:
- sa_iso_inv p = - Rep_regular x

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = Abs_stone_phi_pair (Abs_regular (- - Rep_regular x), stone_phi (Abs_regular (- Rep_regular x)) \<squnion> up_filter (Abs_dense (Rep_regular x \<sqinter> Rep_dense (stone_phi.rho_pair (x, y)) \<squnion> - Rep_regular x)))
[PROOF STEP]
using 6
[PROOF STATE]
proof (prove)
using this:
- sa_iso_inv p = - Rep_regular x
sa_iso_inv p = Rep_regular x \<sqinter> Rep_dense (stone_phi.rho_pair (x, y))

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = Abs_stone_phi_pair (Abs_regular (- - Rep_regular x), stone_phi (Abs_regular (- Rep_regular x)) \<squnion> up_filter (Abs_dense (Rep_regular x \<sqinter> Rep_dense (stone_phi.rho_pair (x, y)) \<squnion> - Rep_regular x)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sa_iso (sa_iso_inv p) = Abs_stone_phi_pair (Abs_regular (- - Rep_regular x), stone_phi (Abs_regular (- Rep_regular x)) \<squnion> up_filter (Abs_dense (Rep_regular x \<sqinter> Rep_dense (stone_phi.rho_pair (x, y)) \<squnion> - Rep_regular x)))

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sa_iso (sa_iso_inv p) = Abs_stone_phi_pair (Abs_regular (- - Rep_regular x), stone_phi (Abs_regular (- Rep_regular x)) \<squnion> up_filter (Abs_dense (Rep_regular x \<sqinter> Rep_dense (stone_phi.rho_pair (x, y)) \<squnion> - Rep_regular x)))

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
have "... = Abs_stone_phi_pair (x,stone_phi (-x) \<squnion> up_filter (Abs_dense ((Rep_regular x \<sqinter> Rep_dense (triple.rho_pair stone_phi (x,y))) \<squnion> -Rep_regular x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_stone_phi_pair (Abs_regular (- - Rep_regular x), stone_phi (Abs_regular (- Rep_regular x)) \<squnion> up_filter (Abs_dense (Rep_regular x \<sqinter> Rep_dense (stone_phi.rho_pair (x, y)) \<squnion> - Rep_regular x))) = Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (Abs_dense (Rep_regular x \<sqinter> Rep_dense (stone_phi.rho_pair (x, y)) \<squnion> - Rep_regular x)))
[PROOF STEP]
by (metis (mono_tags, lifting) Rep_regular_inverse double_compl uminus_regular.rep_eq)
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (Abs_regular (- - Rep_regular x), stone_phi (Abs_regular (- Rep_regular x)) \<squnion> up_filter (Abs_dense (Rep_regular x \<sqinter> Rep_dense (stone_phi.rho_pair (x, y)) \<squnion> - Rep_regular x))) = Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (Abs_dense (Rep_regular x \<sqinter> Rep_dense (stone_phi.rho_pair (x, y)) \<squnion> - Rep_regular x)))

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (Abs_regular (- - Rep_regular x), stone_phi (Abs_regular (- Rep_regular x)) \<squnion> up_filter (Abs_dense (Rep_regular x \<sqinter> Rep_dense (stone_phi.rho_pair (x, y)) \<squnion> - Rep_regular x))) = Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (Abs_dense (Rep_regular x \<sqinter> Rep_dense (stone_phi.rho_pair (x, y)) \<squnion> - Rep_regular x)))

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
have "... = Abs_stone_phi_pair (x,stone_phi (-x) \<squnion> up_filter (Abs_dense (Rep_dense (triple.rho_pair stone_phi (x,y)) \<squnion> -Rep_regular x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (Abs_dense (Rep_regular x \<sqinter> Rep_dense (stone_phi.rho_pair (x, y)) \<squnion> - Rep_regular x))) = Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (Abs_dense (Rep_dense (stone_phi.rho_pair (x, y)) \<squnion> - Rep_regular x)))
[PROOF STEP]
by (metis inf_sup_aci(5) maddux_3_21_pp simp_regular)
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (Abs_dense (Rep_regular x \<sqinter> Rep_dense (stone_phi.rho_pair (x, y)) \<squnion> - Rep_regular x))) = Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (Abs_dense (Rep_dense (stone_phi.rho_pair (x, y)) \<squnion> - Rep_regular x)))

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (Abs_dense (Rep_regular x \<sqinter> Rep_dense (stone_phi.rho_pair (x, y)) \<squnion> - Rep_regular x))) = Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (Abs_dense (Rep_dense (stone_phi.rho_pair (x, y)) \<squnion> - Rep_regular x)))

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
have "... = Abs_stone_phi_pair (x,stone_phi (-x) \<squnion> up_filter (Abs_dense (Rep_dense (triple.rho_pair stone_phi (x,y)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (Abs_dense (Rep_dense (stone_phi.rho_pair (x, y)) \<squnion> - Rep_regular x))) = Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (Abs_dense (Rep_dense (stone_phi.rho_pair (x, y)))))
[PROOF STEP]
using 5
[PROOF STATE]
proof (prove)
using this:
- Rep_regular x \<le> Rep_dense (stone_phi.rho_pair (x, y))

goal (1 subgoal):
 1. Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (Abs_dense (Rep_dense (stone_phi.rho_pair (x, y)) \<squnion> - Rep_regular x))) = Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (Abs_dense (Rep_dense (stone_phi.rho_pair (x, y)))))
[PROOF STEP]
by (simp add: sup.absorb1)
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (Abs_dense (Rep_dense (stone_phi.rho_pair (x, y)) \<squnion> - Rep_regular x))) = Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (Abs_dense (Rep_dense (stone_phi.rho_pair (x, y)))))

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (Abs_dense (Rep_dense (stone_phi.rho_pair (x, y)) \<squnion> - Rep_regular x))) = Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (Abs_dense (Rep_dense (stone_phi.rho_pair (x, y)))))

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
have "... = Abs_stone_phi_pair (x,stone_phi (-x) \<squnion> up_filter (triple.rho_pair stone_phi (x,y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (Abs_dense (Rep_dense (stone_phi.rho_pair (x, y))))) = Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (stone_phi.rho_pair (x, y)))
[PROOF STEP]
by (simp add: Rep_dense_inverse)
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (Abs_dense (Rep_dense (stone_phi.rho_pair (x, y))))) = Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (stone_phi.rho_pair (x, y)))

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (Abs_dense (Rep_dense (stone_phi.rho_pair (x, y))))) = Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (stone_phi.rho_pair (x, y)))

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
have "... = Abs_stone_phi_pair (x,stone_phi (-x) \<squnion> (stone_phi x \<sqinter> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (stone_phi.rho_pair (x, y))) = Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> stone_phi x \<sqinter> y)
[PROOF STEP]
using 2 stone_phi.get_rho_pair_char
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> stone_phi.pairs
(?x, ?y) \<in> stone_phi.pairs \<Longrightarrow> up_filter (stone_phi.rho_pair (?x, ?y)) = stone_phi ?x \<sqinter> ?y

goal (1 subgoal):
 1. Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (stone_phi.rho_pair (x, y))) = Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> stone_phi x \<sqinter> y)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (stone_phi.rho_pair (x, y))) = Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> stone_phi x \<sqinter> y)

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> up_filter (stone_phi.rho_pair (x, y))) = Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> stone_phi x \<sqinter> y)

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
have "... = Abs_stone_phi_pair (x,stone_phi (-x) \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> stone_phi x \<sqinter> y) = Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> y)
[PROOF STEP]
by (simp add: stone_phi.phi_complemented sup.commute sup_inf_distrib1)
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> stone_phi x \<sqinter> y) = Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> y)

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> stone_phi x \<sqinter> y) = Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> y)

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
have "... = Abs_stone_phi_pair (x,y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> y) = Abs_stone_phi_pair (x, y)
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
stone_phi (- x) \<le> y

goal (1 subgoal):
 1. Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> y) = Abs_stone_phi_pair (x, y)
[PROOF STEP]
by (simp add: le_iff_sup)
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> y) = Abs_stone_phi_pair (x, y)

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (x, stone_phi (- x) \<squnion> y) = Abs_stone_phi_pair (x, y)

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
have "... = p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_stone_phi_pair (x, y) = p
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
(x, y) = Rep_stone_phi_pair p

goal (1 subgoal):
 1. Abs_stone_phi_pair (x, y) = p
[PROOF STEP]
by (simp add: Rep_stone_phi_pair_inverse)
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (x, y) = p

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sa_iso (sa_iso_inv p) = p
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sa_iso (sa_iso_inv p) = p

goal (1 subgoal):
 1. sa_iso (sa_iso_inv p) = p
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sa_iso (sa_iso_inv p) = p

goal:
No subgoals!
[PROOF STEP]
qed