[STATEMENT]
lemma sa_iso:
  "stone_algebra_isomorphism sa_iso"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bounded_lattice_homomorphism sa_iso \<and> uminus_homomorphism sa_iso) \<and> bij sa_iso
[PROOF STEP]
proof (intro conjI)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. sup_homomorphism sa_iso
 2. inf_homomorphism sa_iso
 3. top_homomorphism sa_iso
 4. bot_homomorphism sa_iso
 5. uminus_homomorphism sa_iso
 6. bij sa_iso
[PROOF STEP]
have "Abs_stone_phi_pair (Abs_regular (--bot),stone_phi (Abs_regular (-bot)) \<squnion> up_filter (Abs_dense (bot \<squnion> -bot))) = Abs_stone_phi_pair (bot,stone_phi top \<squnion> up_filter top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_stone_phi_pair (Abs_regular (- - bot), stone_phi (Abs_regular (- bot)) \<squnion> up_filter (Abs_dense (bot \<squnion> - bot))) = Abs_stone_phi_pair (bot, stone_phi top \<squnion> up_filter top)
[PROOF STEP]
by (simp add: bot_regular.abs_eq top_regular.abs_eq top_dense.abs_eq)
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (Abs_regular (- - bot), stone_phi (Abs_regular (- bot)) \<squnion> up_filter (Abs_dense (bot \<squnion> - bot))) = Abs_stone_phi_pair (bot, stone_phi top \<squnion> up_filter top)

goal (6 subgoals):
 1. sup_homomorphism sa_iso
 2. inf_homomorphism sa_iso
 3. top_homomorphism sa_iso
 4. bot_homomorphism sa_iso
 5. uminus_homomorphism sa_iso
 6. bij sa_iso
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (Abs_regular (- - bot), stone_phi (Abs_regular (- bot)) \<squnion> up_filter (Abs_dense (bot \<squnion> - bot))) = Abs_stone_phi_pair (bot, stone_phi top \<squnion> up_filter top)

goal (6 subgoals):
 1. sup_homomorphism sa_iso
 2. inf_homomorphism sa_iso
 3. top_homomorphism sa_iso
 4. bot_homomorphism sa_iso
 5. uminus_homomorphism sa_iso
 6. bij sa_iso
[PROOF STEP]
have "... = Abs_stone_phi_pair (bot,stone_phi top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_stone_phi_pair (bot, stone_phi top \<squnion> up_filter top) = Abs_stone_phi_pair (bot, stone_phi top)
[PROOF STEP]
by (simp add: stone_phi.hom)
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (bot, stone_phi top \<squnion> up_filter top) = Abs_stone_phi_pair (bot, stone_phi top)

goal (6 subgoals):
 1. sup_homomorphism sa_iso
 2. inf_homomorphism sa_iso
 3. top_homomorphism sa_iso
 4. bot_homomorphism sa_iso
 5. uminus_homomorphism sa_iso
 6. bij sa_iso
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (bot, stone_phi top \<squnion> up_filter top) = Abs_stone_phi_pair (bot, stone_phi top)

goal (6 subgoals):
 1. sup_homomorphism sa_iso
 2. inf_homomorphism sa_iso
 3. top_homomorphism sa_iso
 4. bot_homomorphism sa_iso
 5. uminus_homomorphism sa_iso
 6. bij sa_iso
[PROOF STEP]
have "... = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_stone_phi_pair (bot, stone_phi top) = bot
[PROOF STEP]
by (simp add: bot_stone_phi_pair_def stone_phi.phi_top)
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (bot, stone_phi top) = bot

goal (6 subgoals):
 1. sup_homomorphism sa_iso
 2. inf_homomorphism sa_iso
 3. top_homomorphism sa_iso
 4. bot_homomorphism sa_iso
 5. uminus_homomorphism sa_iso
 6. bij sa_iso
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Abs_stone_phi_pair (Abs_regular (- - bot), stone_phi (Abs_regular (- bot)) \<squnion> up_filter (Abs_dense (bot \<squnion> - bot))) = bot
[PROOF STEP]
show "sa_iso bot = bot"
[PROOF STATE]
proof (prove)
using this:
Abs_stone_phi_pair (Abs_regular (- - bot), stone_phi (Abs_regular (- bot)) \<squnion> up_filter (Abs_dense (bot \<squnion> - bot))) = bot

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

goal (5 subgoals):
 1. sup_homomorphism sa_iso
 2. inf_homomorphism sa_iso
 3. top_homomorphism sa_iso
 4. uminus_homomorphism sa_iso
 5. bij sa_iso
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. sup_homomorphism sa_iso
 2. inf_homomorphism sa_iso
 3. top_homomorphism sa_iso
 4. uminus_homomorphism sa_iso
 5. bij sa_iso
[PROOF STEP]
have "Abs_stone_phi_pair (Abs_regular (--top),stone_phi (Abs_regular (-top)) \<squnion> up_filter (Abs_dense (top \<squnion> -top))) = Abs_stone_phi_pair (top,stone_phi bot \<squnion> up_filter top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_stone_phi_pair (Abs_regular (- - top), stone_phi (Abs_regular (- top)) \<squnion> up_filter (Abs_dense (top \<squnion> - top))) = Abs_stone_phi_pair (top, stone_phi bot \<squnion> up_filter top)
[PROOF STEP]
by (simp add: bot_regular.abs_eq top_regular.abs_eq top_dense.abs_eq)
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (Abs_regular (- - top), stone_phi (Abs_regular (- top)) \<squnion> up_filter (Abs_dense (top \<squnion> - top))) = Abs_stone_phi_pair (top, stone_phi bot \<squnion> up_filter top)

goal (5 subgoals):
 1. sup_homomorphism sa_iso
 2. inf_homomorphism sa_iso
 3. top_homomorphism sa_iso
 4. uminus_homomorphism sa_iso
 5. bij sa_iso
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (Abs_regular (- - top), stone_phi (Abs_regular (- top)) \<squnion> up_filter (Abs_dense (top \<squnion> - top))) = Abs_stone_phi_pair (top, stone_phi bot \<squnion> up_filter top)

goal (5 subgoals):
 1. sup_homomorphism sa_iso
 2. inf_homomorphism sa_iso
 3. top_homomorphism sa_iso
 4. uminus_homomorphism sa_iso
 5. bij sa_iso
[PROOF STEP]
have "... = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_stone_phi_pair (top, stone_phi bot \<squnion> up_filter top) = top
[PROOF STEP]
by (simp add: stone_phi.phi_bot top_stone_phi_pair_def)
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (top, stone_phi bot \<squnion> up_filter top) = top

goal (5 subgoals):
 1. sup_homomorphism sa_iso
 2. inf_homomorphism sa_iso
 3. top_homomorphism sa_iso
 4. uminus_homomorphism sa_iso
 5. bij sa_iso
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Abs_stone_phi_pair (Abs_regular (- - top), stone_phi (Abs_regular (- top)) \<squnion> up_filter (Abs_dense (top \<squnion> - top))) = top
[PROOF STEP]
show "sa_iso top = top"
[PROOF STATE]
proof (prove)
using this:
Abs_stone_phi_pair (Abs_regular (- - top), stone_phi (Abs_regular (- top)) \<squnion> up_filter (Abs_dense (top \<squnion> - top))) = top

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

goal (4 subgoals):
 1. sup_homomorphism sa_iso
 2. inf_homomorphism sa_iso
 3. uminus_homomorphism sa_iso
 4. bij sa_iso
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. sup_homomorphism sa_iso
 2. inf_homomorphism sa_iso
 3. uminus_homomorphism sa_iso
 4. bij sa_iso
[PROOF STEP]
have 1: "\<forall>x y::'a . dense (x \<squnion> -x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. dense (x \<squnion> - x \<squnion> y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>x y. dense (x \<squnion> - x \<squnion> y)

goal (4 subgoals):
 1. sup_homomorphism sa_iso
 2. inf_homomorphism sa_iso
 3. uminus_homomorphism sa_iso
 4. bij sa_iso
[PROOF STEP]
have 2: "\<forall>x y::'a . up_filter (Abs_dense (x \<squnion> -x \<squnion> y)) \<le> (stone_phi (Abs_regular (-x)) \<squnion> up_filter (Abs_dense (x \<squnion> -x))) \<sqinter> (stone_phi (Abs_regular (-y)) \<squnion> up_filter (Abs_dense (y \<squnion> -y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) \<le> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<sqinter> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
proof (intro allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) \<le> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<sqinter> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
fix x y :: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) \<le> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<sqinter> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
let ?u = "Abs_dense (x \<squnion> -x \<squnion> --y)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) \<le> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<sqinter> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
let ?v = "Abs_dense (y \<squnion> -y)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) \<le> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<sqinter> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
have "\<up>(Abs_dense (x \<squnion> -x \<squnion> y)) \<le> Rep_filter (stone_phi (Abs_regular (-y)) \<squnion> up_filter ?v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<up>Abs_dense (x \<squnion> - x \<squnion> y) \<subseteq> Filters.filter.Rep_filter (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> \<up>Abs_dense (x \<squnion> - x \<squnion> y) \<Longrightarrow> xa \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xa. xa \<in> \<up>Abs_dense (x \<squnion> - x \<squnion> y) \<Longrightarrow> xa \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
assume "z \<in> \<up>(Abs_dense (x \<squnion> -x \<squnion> y))"
[PROOF STATE]
proof (state)
this:
z \<in> \<up>Abs_dense (x \<squnion> - x \<squnion> y)

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

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

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

goal (1 subgoal):
 1. x \<squnion> - x \<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 \<squnion> - x \<squnion> y \<le> Rep_dense z

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

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

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

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

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>xa. xa \<in> \<up>Abs_dense (x \<squnion> - x \<squnion> y) \<Longrightarrow> xa \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
have "-Rep_regular (Abs_regular (-y)) = --y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - Rep_regular (Abs_regular (- y)) = - - y
[PROOF STEP]
by (metis (mono_tags, lifting) mem_Collect_eq Abs_regular_inverse)
[PROOF STATE]
proof (state)
this:
- Rep_regular (Abs_regular (- y)) = - - y

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

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

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

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

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

goal (1 subgoal):
 1. Abs_dense (x \<squnion> - x \<squnion> - - y) \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- y)))
[PROOF STEP]
by (metis mem_Collect_eq stone_phi_def stone_phi_base_filter Abs_filter_inverse)
[PROOF STATE]
proof (state)
this:
Abs_dense (x \<squnion> - x \<squnion> - - y) \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- y)))

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

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

goal (1 subgoal):
 1. Abs_dense (y \<squnion> - y) \<in> Filters.filter.Rep_filter (up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
by (metis Abs_filter_inverse mem_Collect_eq up_filter)
[PROOF STATE]
proof (state)
this:
Abs_dense (y \<squnion> - y) \<in> Filters.filter.Rep_filter (up_filter (Abs_dense (y \<squnion> - y)))

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

goal (1 subgoal):
 1. z \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
using 4 5 sup_filter.rep_eq filter_sup_def
[PROOF STATE]
proof (prove)
using this:
Abs_dense (y \<squnion> - y) \<in> Filters.filter.Rep_filter (up_filter (Abs_dense (y \<squnion> - y)))
Abs_dense (x \<squnion> - x \<squnion> - - y) \<sqinter> Abs_dense (y \<squnion> - y) \<le> z
Abs_dense (x \<squnion> - x \<squnion> - - y) \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- y)))
Filters.filter.Rep_filter (?x \<squnion> ?xa) = filter_sup (Filters.filter.Rep_filter ?x) (Filters.filter.Rep_filter ?xa)
filter_sup ?F ?G \<equiv> {z. \<exists>x\<in>?F. \<exists>y\<in>?G. x \<sqinter> y \<le> z}

goal (1 subgoal):
 1. z \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z \<in> Filters.filter.Rep_filter (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))

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

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

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

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

goal (1 subgoal):
 1. \<And>x y. up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) \<le> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<sqinter> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
have "... = stone_phi (Abs_regular (-y)) \<squnion> up_filter ?v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Filters.filter.Abs_filter (Filters.filter.Rep_filter (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))) = stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y))
[PROOF STEP]
by (simp add: Rep_filter_inverse)
[PROOF STATE]
proof (state)
this:
Filters.filter.Abs_filter (Filters.filter.Rep_filter (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))) = stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y))

goal (1 subgoal):
 1. \<And>x y. up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) \<le> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<sqinter> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) \<le> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y))
[PROOF STEP]
show "up_filter (Abs_dense (x \<squnion> -x \<squnion> y)) \<le> (stone_phi (Abs_regular (-x)) \<squnion> up_filter (Abs_dense (x \<squnion> -x))) \<sqinter> (stone_phi (Abs_regular (-y)) \<squnion> up_filter (Abs_dense (y \<squnion> -y)))"
[PROOF STATE]
proof (prove)
using this:
up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) \<le> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y))

goal (1 subgoal):
 1. up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) \<le> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<sqinter> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
by (metis le_infI le_supI2 sup_bot.right_neutral up_filter_dense_antitone)
[PROOF STATE]
proof (state)
this:
up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) \<le> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<sqinter> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))

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

goal (4 subgoals):
 1. sup_homomorphism sa_iso
 2. inf_homomorphism sa_iso
 3. uminus_homomorphism sa_iso
 4. bij sa_iso
[PROOF STEP]
have 6: "\<forall>x::'a . in_p_image (-x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. in_p_image (- x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x. in_p_image (- x)

goal (4 subgoals):
 1. sup_homomorphism sa_iso
 2. inf_homomorphism sa_iso
 3. uminus_homomorphism sa_iso
 4. bij sa_iso
[PROOF STEP]
show "\<forall>x y::'a . sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_homomorphism sa_iso
[PROOF STEP]
proof (intro allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y
[PROOF STEP]
fix x y :: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y
[PROOF STEP]
have 7: "up_filter (Abs_dense (x \<squnion> -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. up_filter (Abs_dense (x \<squnion> - 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. up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)) \<le> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))
[PROOF STEP]
have "up_filter (Abs_dense (x \<squnion> -x)) \<sqinter> up_filter (Abs_dense (y \<squnion> -y)) = up_filter (Abs_dense (x \<squnion> -x) \<squnion> Abs_dense (y \<squnion> -y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)) = up_filter (Abs_dense (x \<squnion> - x) \<squnion> Abs_dense (y \<squnion> - y))
[PROOF STEP]
by (metis up_filter_dist_sup)
[PROOF STATE]
proof (state)
this:
up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)) = up_filter (Abs_dense (x \<squnion> - x) \<squnion> Abs_dense (y \<squnion> - y))

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

goal (1 subgoal):
 1. up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)) \<le> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))
[PROOF STEP]
have "... = up_filter (Abs_dense (x \<squnion> -x \<squnion> (y \<squnion> -y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. up_filter (Abs_dense (x \<squnion> - x) \<squnion> Abs_dense (y \<squnion> - y)) = up_filter (Abs_dense (x \<squnion> - x \<squnion> (y \<squnion> - y)))
[PROOF STEP]
by (subst sup_dense.abs_eq) (simp_all add: eq_onp_same_args)
[PROOF STATE]
proof (state)
this:
up_filter (Abs_dense (x \<squnion> - x) \<squnion> Abs_dense (y \<squnion> - y)) = up_filter (Abs_dense (x \<squnion> - x \<squnion> (y \<squnion> - y)))

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

goal (1 subgoal):
 1. up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)) \<le> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))
[PROOF STEP]
have "... = up_filter (Abs_dense (y \<squnion> -y \<squnion> x \<squnion> -x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. up_filter (Abs_dense (x \<squnion> - x \<squnion> (y \<squnion> - y))) = up_filter (Abs_dense (y \<squnion> - y \<squnion> x \<squnion> - x))
[PROOF STEP]
by (simp add: sup_commute sup_left_commute)
[PROOF STATE]
proof (state)
this:
up_filter (Abs_dense (x \<squnion> - x \<squnion> (y \<squnion> - y))) = up_filter (Abs_dense (y \<squnion> - y \<squnion> x \<squnion> - x))

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

goal (1 subgoal):
 1. up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)) \<le> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))
[PROOF STEP]
have "... \<le> up_filter (Abs_dense (y \<squnion> -y \<squnion> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. up_filter (Abs_dense (y \<squnion> - y \<squnion> x \<squnion> - x)) \<le> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))
[PROOF STEP]
using up_filter_dense_antitone
[PROOF STATE]
proof (prove)
using this:
up_filter (Abs_dense (?x \<squnion> - ?x \<squnion> ?y \<squnion> ?z)) \<le> up_filter (Abs_dense (?x \<squnion> - ?x \<squnion> ?y))

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

goal (1 subgoal):
 1. up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)) \<le> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)) \<le> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)) \<le> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))

goal (1 subgoal):
 1. up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)) \<le> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
up_filter (Abs_dense (x \<squnion> - 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
[PROOF STATE]
proof (state)
this:
up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)) \<le> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y
[PROOF STEP]
have "Abs_dense (x \<squnion> y \<squnion> -(x \<squnion> y)) = Abs_dense ((x \<squnion> -x \<squnion> y) \<sqinter> (y \<squnion> -y \<squnion> x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y)) = Abs_dense ((x \<squnion> - x \<squnion> y) \<sqinter> (y \<squnion> - y \<squnion> x))
[PROOF STEP]
by (simp add: sup_commute sup_inf_distrib1 sup_left_commute)
[PROOF STATE]
proof (state)
this:
Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y)) = Abs_dense ((x \<squnion> - x \<squnion> y) \<sqinter> (y \<squnion> - y \<squnion> x))

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

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y
[PROOF STEP]
have "... = Abs_dense (x \<squnion> -x \<squnion> y) \<sqinter> Abs_dense (y \<squnion> -y \<squnion> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_dense ((x \<squnion> - x \<squnion> y) \<sqinter> (y \<squnion> - y \<squnion> x)) = Abs_dense (x \<squnion> - x \<squnion> y) \<sqinter> Abs_dense (y \<squnion> - y \<squnion> x)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. dense (x \<squnion> - x \<squnion> y)

goal (1 subgoal):
 1. Abs_dense ((x \<squnion> - x \<squnion> y) \<sqinter> (y \<squnion> - y \<squnion> x)) = Abs_dense (x \<squnion> - x \<squnion> y) \<sqinter> Abs_dense (y \<squnion> - y \<squnion> x)
[PROOF STEP]
by (metis (mono_tags, lifting) Abs_dense_inverse Rep_dense_inverse inf_dense.rep_eq mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
Abs_dense ((x \<squnion> - x \<squnion> y) \<sqinter> (y \<squnion> - y \<squnion> x)) = Abs_dense (x \<squnion> - x \<squnion> y) \<sqinter> Abs_dense (y \<squnion> - y \<squnion> x)

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y)) = Abs_dense (x \<squnion> - x \<squnion> y) \<sqinter> Abs_dense (y \<squnion> - y \<squnion> x)
[PROOF STEP]
have 8: "up_filter (Abs_dense (x \<squnion> y \<squnion> -(x \<squnion> y))) = up_filter (Abs_dense (x \<squnion> -x \<squnion> y)) \<squnion> up_filter (Abs_dense (y \<squnion> -y \<squnion> x))"
[PROOF STATE]
proof (prove)
using this:
Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y)) = Abs_dense (x \<squnion> - x \<squnion> y) \<sqinter> Abs_dense (y \<squnion> - y \<squnion> x)

goal (1 subgoal):
 1. up_filter (Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y))) = up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))
[PROOF STEP]
by (simp add: up_filter_dist_inf)
[PROOF STATE]
proof (state)
this:
up_filter (Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y))) = up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))

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

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y
[PROOF STEP]
have "... \<le> (stone_phi (Abs_regular (-x)) \<squnion> up_filter (Abs_dense (x \<squnion> -x))) \<sqinter> (stone_phi (Abs_regular (-y)) \<squnion> up_filter (Abs_dense (y \<squnion> -y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> x)) \<le> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<sqinter> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) \<le> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<sqinter> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))

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

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
up_filter (Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y))) \<le> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<sqinter> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
have 9: "(stone_phi (Abs_regular (-x)) \<sqinter> stone_phi (Abs_regular (-y))) \<squnion> up_filter (Abs_dense (x \<squnion> y \<squnion> -(x \<squnion> y))) \<le> ..."
[PROOF STATE]
proof (prove)
using this:
up_filter (Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y))) \<le> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<sqinter> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))

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

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y
[PROOF STEP]
have "... = (stone_phi (Abs_regular (-x)) \<sqinter> stone_phi (Abs_regular (-y))) \<squnion> (stone_phi (Abs_regular (-x)) \<sqinter> up_filter (Abs_dense (y \<squnion> -y))) \<squnion> ((up_filter (Abs_dense (x \<squnion> -x)) \<sqinter> stone_phi (Abs_regular (-y))) \<squnion> (up_filter (Abs_dense (x \<squnion> -x)) \<sqinter> up_filter (Abs_dense (y \<squnion> -y))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<sqinter> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y))) = stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)) \<squnion> (up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
by (metis (no_types) inf_sup_distrib1 inf_sup_distrib2)
[PROOF STATE]
proof (state)
this:
(stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<sqinter> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y))) = stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)) \<squnion> (up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)))

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

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y
[PROOF STEP]
have "... \<le> (stone_phi (Abs_regular (-x)) \<sqinter> stone_phi (Abs_regular (-y))) \<squnion> up_filter (Abs_dense (y \<squnion> -y \<squnion> x)) \<squnion> ((up_filter (Abs_dense (x \<squnion> -x)) \<sqinter> stone_phi (Abs_regular (-y))) \<squnion> (up_filter (Abs_dense (x \<squnion> -x)) \<sqinter> up_filter (Abs_dense (y \<squnion> -y))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)) \<squnion> (up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<le> stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> x)) \<squnion> (up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
by (meson sup_left_isotone sup_right_isotone stone_phi_inf_dense)
[PROOF STATE]
proof (state)
this:
stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> stone_phi (Abs_regular (- x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)) \<squnion> (up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<le> stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> x)) \<squnion> (up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)))

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

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y
[PROOF STEP]
have "... \<le> (stone_phi (Abs_regular (-x)) \<sqinter> stone_phi (Abs_regular (-y))) \<squnion> up_filter (Abs_dense (y \<squnion> -y \<squnion> x)) \<squnion> (up_filter (Abs_dense (x \<squnion> -x \<squnion> y)) \<squnion> (up_filter (Abs_dense (x \<squnion> -x)) \<sqinter> up_filter (Abs_dense (y \<squnion> -y))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> x)) \<squnion> (up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<le> stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> x)) \<squnion> (up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
by (metis inf.commute sup_left_isotone sup_right_isotone stone_phi_inf_dense)
[PROOF STATE]
proof (state)
this:
stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> x)) \<squnion> (up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<le> stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> x)) \<squnion> (up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y)))

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

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y
[PROOF STEP]
have "... \<le> (stone_phi (Abs_regular (-x)) \<sqinter> stone_phi (Abs_regular (-y))) \<squnion> up_filter (Abs_dense (y \<squnion> -y \<squnion> x)) \<squnion> up_filter (Abs_dense (x \<squnion> -x \<squnion> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> x)) \<squnion> (up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<le> stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x \<squnion> y))
[PROOF STEP]
using 7
[PROOF STATE]
proof (prove)
using this:
up_filter (Abs_dense (x \<squnion> - 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> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> x)) \<squnion> (up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<le> stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x \<squnion> y))
[PROOF STEP]
by (simp add: sup.absorb1 sup_commute sup_left_commute)
[PROOF STATE]
proof (state)
this:
stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> x)) \<squnion> (up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) \<sqinter> up_filter (Abs_dense (y \<squnion> - y))) \<le> stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x \<squnion> y))

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

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y
[PROOF STEP]
have "... = (stone_phi (Abs_regular (-x)) \<sqinter> stone_phi (Abs_regular (-y))) \<squnion> up_filter (Abs_dense (x \<squnion> y \<squnion> -(x \<squnion> y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) = stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y)))
[PROOF STEP]
using 8
[PROOF STATE]
proof (prove)
using this:
up_filter (Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y))) = up_filter (Abs_dense (x \<squnion> - x \<squnion> y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> x))

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

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

goal (1 subgoal):
 1. (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<sqinter> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y))) = stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y)))
[PROOF STEP]
using 9
[PROOF STATE]
proof (prove)
using this:
(stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<sqinter> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y))) \<le> stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y)))
stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y))) \<le> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<sqinter> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))

goal (1 subgoal):
 1. (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<sqinter> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y))) = stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y)))
[PROOF STEP]
using antisym
[PROOF STATE]
proof (prove)
using this:
(stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<sqinter> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y))) \<le> stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y)))
stone_phi (Abs_regular (- x)) \<sqinter> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y))) \<le> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) \<sqinter> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))
\<lbrakk>?a \<le> ?b; ?b \<le> ?a\<rbrakk> \<Longrightarrow> ?a = ?b

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

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

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

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

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y
[PROOF STEP]
have "... = stone_phi (Abs_regular (-(x \<squnion> y))) \<squnion> up_filter (Abs_dense (x \<squnion> y \<squnion> -(x \<squnion> y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi (Abs_regular (- x) \<sqinter> Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y))) = stone_phi (Abs_regular (- (x \<squnion> y))) \<squnion> up_filter (Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y)))
[PROOF STEP]
using 6
[PROOF STATE]
proof (prove)
using this:
\<forall>x. in_p_image (- x)

goal (1 subgoal):
 1. stone_phi (Abs_regular (- x) \<sqinter> Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y))) = stone_phi (Abs_regular (- (x \<squnion> y))) \<squnion> up_filter (Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y)))
[PROOF STEP]
by (subst inf_regular.abs_eq) (simp_all add: eq_onp_same_args)
[PROOF STATE]
proof (state)
this:
stone_phi (Abs_regular (- x) \<sqinter> Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y))) = stone_phi (Abs_regular (- (x \<squnion> y))) \<squnion> up_filter (Abs_dense (x \<squnion> y \<squnion> - (x \<squnion> y)))

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

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

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y
[PROOF STEP]
have "Abs_regular (--(x \<squnion> y)) = Abs_regular (--x) \<squnion> Abs_regular (--y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_regular (- - (x \<squnion> y)) = Abs_regular (- - x) \<squnion> Abs_regular (- - y)
[PROOF STEP]
using 6
[PROOF STATE]
proof (prove)
using this:
\<forall>x. in_p_image (- x)

goal (1 subgoal):
 1. Abs_regular (- - (x \<squnion> y)) = Abs_regular (- - x) \<squnion> Abs_regular (- - y)
[PROOF STEP]
by (subst sup_regular.abs_eq) (simp_all add: eq_onp_same_args)
[PROOF STATE]
proof (state)
this:
Abs_regular (- - (x \<squnion> y)) = Abs_regular (- - x) \<squnion> Abs_regular (- - y)

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

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

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

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

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y
[PROOF STEP]
have "... = Abs_stone_phi_pair (Abs_regular (--x),stone_phi (Abs_regular (-x)) \<squnion> up_filter (Abs_dense (x \<squnion> -x))) \<squnion> Abs_stone_phi_pair (Abs_regular (--y),stone_phi (Abs_regular (-y)) \<squnion> up_filter (Abs_dense (y \<squnion> -y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_stone_phi_pair (stone_phi.pairs_sup (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) (Abs_regular (- - y), stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))) = sa_iso x \<squnion> sa_iso y
[PROOF STEP]
by (rule sup_stone_phi_pair.abs_eq[THEN sym]) (simp_all add: eq_onp_same_args sa_iso_triple_pair)
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (stone_phi.pairs_sup (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) (Abs_regular (- - y), stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))) = sa_iso x \<squnion> sa_iso y

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y
[PROOF STEP]
show "sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y"
[PROOF STATE]
proof (prove)
using this:
sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y

goal (1 subgoal):
 1. sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sa_iso (x \<squnion> y) = sa_iso x \<squnion> sa_iso y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
sup_homomorphism sa_iso

goal (3 subgoals):
 1. inf_homomorphism sa_iso
 2. uminus_homomorphism sa_iso
 3. bij sa_iso
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. inf_homomorphism sa_iso
 2. uminus_homomorphism sa_iso
 3. bij sa_iso
[PROOF STEP]
have 1: "\<forall>x y::'a . dense (x \<squnion> -x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. dense (x \<squnion> - x \<squnion> y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<forall>x y. dense (x \<squnion> - x \<squnion> y)

goal (3 subgoals):
 1. inf_homomorphism sa_iso
 2. uminus_homomorphism sa_iso
 3. bij sa_iso
[PROOF STEP]
have 2: "\<forall>x::'a . in_p_image (-x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x. in_p_image (- x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>x. in_p_image (- x)

goal (3 subgoals):
 1. inf_homomorphism sa_iso
 2. uminus_homomorphism sa_iso
 3. bij sa_iso
[PROOF STEP]
have 3: "\<forall>x y::'a . stone_phi (Abs_regular (-y)) \<squnion> up_filter (Abs_dense (x \<squnion> -x)) = stone_phi (Abs_regular (-y)) \<squnion> up_filter (Abs_dense (x \<squnion> -x \<squnion> -y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) = stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x \<squnion> - y))
[PROOF STEP]
proof (intro allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) = stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x \<squnion> - y))
[PROOF STEP]
fix x y :: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) = stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x \<squnion> - y))
[PROOF STEP]
have 4: "up_filter (Abs_dense (x \<squnion> -x)) \<le> stone_phi (Abs_regular (-y)) \<squnion> up_filter (Abs_dense (x \<squnion> -x \<squnion> -y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. up_filter (Abs_dense (x \<squnion> - x)) \<le> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x \<squnion> - y))
[PROOF STEP]
by (metis (no_types, lifting) complement_shunting stone_phi_inf_dense stone_phi_complement complement_symmetric)
[PROOF STATE]
proof (state)
this:
up_filter (Abs_dense (x \<squnion> - x)) \<le> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x \<squnion> - y))

goal (1 subgoal):
 1. \<And>x y. stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) = stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x \<squnion> - y))
[PROOF STEP]
have "up_filter (Abs_dense (x \<squnion> -x \<squnion> -y)) \<le> up_filter (Abs_dense (x \<squnion> -x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. up_filter (Abs_dense (x \<squnion> - x \<squnion> - y)) \<le> up_filter (Abs_dense (x \<squnion> - x))
[PROOF STEP]
by (metis sup_idem up_filter_dense_antitone)
[PROOF STATE]
proof (state)
this:
up_filter (Abs_dense (x \<squnion> - x \<squnion> - y)) \<le> up_filter (Abs_dense (x \<squnion> - x))

goal (1 subgoal):
 1. \<And>x y. stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) = stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x \<squnion> - y))
[PROOF STEP]
thus "stone_phi (Abs_regular (-y)) \<squnion> up_filter (Abs_dense (x \<squnion> -x)) = stone_phi (Abs_regular (-y)) \<squnion> up_filter (Abs_dense (x \<squnion> -x \<squnion> -y))"
[PROOF STATE]
proof (prove)
using this:
up_filter (Abs_dense (x \<squnion> - x \<squnion> - y)) \<le> up_filter (Abs_dense (x \<squnion> - x))

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x y. stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) = stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x \<squnion> - y))

goal (3 subgoals):
 1. inf_homomorphism sa_iso
 2. uminus_homomorphism sa_iso
 3. bij sa_iso
[PROOF STEP]
show "\<forall>x y::'a . sa_iso (x \<sqinter> y) = sa_iso x \<sqinter> sa_iso y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inf_homomorphism sa_iso
[PROOF STEP]
proof (intro allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<sqinter> y) = sa_iso x \<sqinter> sa_iso y
[PROOF STEP]
fix x y :: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<sqinter> y) = sa_iso x \<sqinter> sa_iso y
[PROOF STEP]
have "Abs_dense ((x \<sqinter> y) \<squnion> -(x \<sqinter> y)) = Abs_dense ((x \<squnion> -x \<squnion> -y) \<sqinter> (y \<squnion> -y \<squnion> -x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_dense (x \<sqinter> y \<squnion> - (x \<sqinter> y)) = Abs_dense ((x \<squnion> - x \<squnion> - y) \<sqinter> (y \<squnion> - y \<squnion> - x))
[PROOF STEP]
by (simp add: sup_commute sup_inf_distrib1 sup_left_commute)
[PROOF STATE]
proof (state)
this:
Abs_dense (x \<sqinter> y \<squnion> - (x \<sqinter> y)) = Abs_dense ((x \<squnion> - x \<squnion> - y) \<sqinter> (y \<squnion> - y \<squnion> - x))

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

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<sqinter> y) = sa_iso x \<sqinter> sa_iso y
[PROOF STEP]
have "... = Abs_dense (x \<squnion> -x \<squnion> -y) \<sqinter> Abs_dense (y \<squnion> -y \<squnion> -x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_dense ((x \<squnion> - x \<squnion> - y) \<sqinter> (y \<squnion> - y \<squnion> - x)) = Abs_dense (x \<squnion> - x \<squnion> - y) \<sqinter> Abs_dense (y \<squnion> - y \<squnion> - x)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. dense (x \<squnion> - x \<squnion> y)

goal (1 subgoal):
 1. Abs_dense ((x \<squnion> - x \<squnion> - y) \<sqinter> (y \<squnion> - y \<squnion> - x)) = Abs_dense (x \<squnion> - x \<squnion> - y) \<sqinter> Abs_dense (y \<squnion> - y \<squnion> - x)
[PROOF STEP]
by (metis (mono_tags, lifting) Abs_dense_inverse Rep_dense_inverse inf_dense.rep_eq mem_Collect_eq)
[PROOF STATE]
proof (state)
this:
Abs_dense ((x \<squnion> - x \<squnion> - y) \<sqinter> (y \<squnion> - y \<squnion> - x)) = Abs_dense (x \<squnion> - x \<squnion> - y) \<sqinter> Abs_dense (y \<squnion> - y \<squnion> - x)

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<sqinter> y) = sa_iso x \<sqinter> sa_iso y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Abs_dense (x \<sqinter> y \<squnion> - (x \<sqinter> y)) = Abs_dense (x \<squnion> - x \<squnion> - y) \<sqinter> Abs_dense (y \<squnion> - y \<squnion> - x)
[PROOF STEP]
have 5: "up_filter (Abs_dense ((x \<sqinter> y) \<squnion> -(x \<sqinter> y))) = up_filter (Abs_dense (x \<squnion> -x \<squnion> -y)) \<squnion> up_filter (Abs_dense (y \<squnion> -y \<squnion> -x))"
[PROOF STATE]
proof (prove)
using this:
Abs_dense (x \<sqinter> y \<squnion> - (x \<sqinter> y)) = Abs_dense (x \<squnion> - x \<squnion> - y) \<sqinter> Abs_dense (y \<squnion> - y \<squnion> - x)

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

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<sqinter> y) = sa_iso x \<sqinter> sa_iso y
[PROOF STEP]
have "(stone_phi (Abs_regular (-x)) \<squnion> up_filter (Abs_dense (x \<squnion> -x))) \<squnion> (stone_phi (Abs_regular (-y)) \<squnion> up_filter (Abs_dense (y \<squnion> -y))) = (stone_phi (Abs_regular (-y)) \<squnion> up_filter (Abs_dense (x \<squnion> -x))) \<squnion> (stone_phi (Abs_regular (-x)) \<squnion> up_filter (Abs_dense (y \<squnion> -y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) \<squnion> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y))) = stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) \<squnion> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))
[PROOF STEP]
by (simp add: inf_sup_aci(6) sup_left_commute)
[PROOF STATE]
proof (state)
this:
stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) \<squnion> (stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y))) = stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) \<squnion> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))

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

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<sqinter> y) = sa_iso x \<sqinter> sa_iso y
[PROOF STEP]
have "... = (stone_phi (Abs_regular (-y)) \<squnion> up_filter (Abs_dense (x \<squnion> -x \<squnion> -y))) \<squnion> (stone_phi (Abs_regular (-x)) \<squnion> up_filter (Abs_dense (y \<squnion> -y \<squnion> -x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) \<squnion> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (y \<squnion> - y))) = stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x \<squnion> - y)) \<squnion> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> - x)))
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
\<forall>x y. stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)) = stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x \<squnion> - y))

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

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

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<sqinter> y) = sa_iso x \<sqinter> sa_iso y
[PROOF STEP]
have "... = (stone_phi (Abs_regular (-x)) \<squnion> stone_phi (Abs_regular (-y))) \<squnion> (up_filter (Abs_dense (x \<squnion> -x \<squnion> -y)) \<squnion> up_filter (Abs_dense (y \<squnion> -y \<squnion> -x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x \<squnion> - y)) \<squnion> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> - x))) = stone_phi (Abs_regular (- x)) \<squnion> stone_phi (Abs_regular (- y)) \<squnion> (up_filter (Abs_dense (x \<squnion> - x \<squnion> - y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> - x)))
[PROOF STEP]
by (simp add: inf_sup_aci(6) sup_left_commute)
[PROOF STATE]
proof (state)
this:
stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<squnion> - x \<squnion> - y)) \<squnion> (stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> - x))) = stone_phi (Abs_regular (- x)) \<squnion> stone_phi (Abs_regular (- y)) \<squnion> (up_filter (Abs_dense (x \<squnion> - x \<squnion> - y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> - x)))

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

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<sqinter> y) = sa_iso x \<sqinter> sa_iso y
[PROOF STEP]
have "... = (stone_phi (Abs_regular (-x)) \<squnion> stone_phi (Abs_regular (-y))) \<squnion> up_filter (Abs_dense ((x \<sqinter> y) \<squnion> -(x \<sqinter> y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi (Abs_regular (- x)) \<squnion> stone_phi (Abs_regular (- y)) \<squnion> (up_filter (Abs_dense (x \<squnion> - x \<squnion> - y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> - x))) = stone_phi (Abs_regular (- x)) \<squnion> stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<sqinter> y \<squnion> - (x \<sqinter> y)))
[PROOF STEP]
using 5
[PROOF STATE]
proof (prove)
using this:
up_filter (Abs_dense (x \<sqinter> y \<squnion> - (x \<sqinter> y))) = up_filter (Abs_dense (x \<squnion> - x \<squnion> - y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y \<squnion> - x))

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

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

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

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

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

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

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<sqinter> y) = sa_iso x \<sqinter> sa_iso y
[PROOF STEP]
have "... = stone_phi (Abs_regular (-(x \<sqinter> y))) \<squnion> up_filter (Abs_dense ((x \<sqinter> y) \<squnion> -(x \<sqinter> y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi (Abs_regular (- x) \<squnion> Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<sqinter> y \<squnion> - (x \<sqinter> y))) = stone_phi (Abs_regular (- (x \<sqinter> y))) \<squnion> up_filter (Abs_dense (x \<sqinter> y \<squnion> - (x \<sqinter> y)))
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
\<forall>x. in_p_image (- x)

goal (1 subgoal):
 1. stone_phi (Abs_regular (- x) \<squnion> Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<sqinter> y \<squnion> - (x \<sqinter> y))) = stone_phi (Abs_regular (- (x \<sqinter> y))) \<squnion> up_filter (Abs_dense (x \<sqinter> y \<squnion> - (x \<sqinter> y)))
[PROOF STEP]
by (subst sup_regular.abs_eq) (simp_all add: eq_onp_same_args)
[PROOF STATE]
proof (state)
this:
stone_phi (Abs_regular (- x) \<squnion> Abs_regular (- y)) \<squnion> up_filter (Abs_dense (x \<sqinter> y \<squnion> - (x \<sqinter> y))) = stone_phi (Abs_regular (- (x \<sqinter> y))) \<squnion> up_filter (Abs_dense (x \<sqinter> y \<squnion> - (x \<sqinter> y)))

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

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

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<sqinter> y) = sa_iso x \<sqinter> sa_iso y
[PROOF STEP]
have "Abs_regular (--(x \<sqinter> y)) = Abs_regular (--x) \<sqinter> Abs_regular (--y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_regular (- - (x \<sqinter> y)) = Abs_regular (- - x) \<sqinter> Abs_regular (- - y)
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
\<forall>x. in_p_image (- x)

goal (1 subgoal):
 1. Abs_regular (- - (x \<sqinter> y)) = Abs_regular (- - x) \<sqinter> Abs_regular (- - y)
[PROOF STEP]
by (subst inf_regular.abs_eq) (simp_all add: eq_onp_same_args)
[PROOF STATE]
proof (state)
this:
Abs_regular (- - (x \<sqinter> y)) = Abs_regular (- - x) \<sqinter> Abs_regular (- - y)

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

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

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

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

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<sqinter> y) = sa_iso x \<sqinter> sa_iso y
[PROOF STEP]
have "... = Abs_stone_phi_pair (Abs_regular (--x),stone_phi (Abs_regular (-x)) \<squnion> up_filter (Abs_dense (x \<squnion> -x))) \<sqinter> Abs_stone_phi_pair (Abs_regular (--y),stone_phi (Abs_regular (-y)) \<squnion> up_filter (Abs_dense (y \<squnion> -y)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_stone_phi_pair (stone_phi.pairs_inf (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) (Abs_regular (- - y), stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))) = sa_iso x \<sqinter> sa_iso y
[PROOF STEP]
by (rule inf_stone_phi_pair.abs_eq[THEN sym]) (simp_all add: eq_onp_same_args sa_iso_triple_pair)
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (stone_phi.pairs_inf (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))) (Abs_regular (- - y), stone_phi (Abs_regular (- y)) \<squnion> up_filter (Abs_dense (y \<squnion> - y)))) = sa_iso x \<sqinter> sa_iso y

goal (1 subgoal):
 1. \<And>x y. sa_iso (x \<sqinter> y) = sa_iso x \<sqinter> sa_iso y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sa_iso (x \<sqinter> y) = sa_iso x \<sqinter> sa_iso y
[PROOF STEP]
show "sa_iso (x \<sqinter> y) = sa_iso x \<sqinter> sa_iso y"
[PROOF STATE]
proof (prove)
using this:
sa_iso (x \<sqinter> y) = sa_iso x \<sqinter> sa_iso y

goal (1 subgoal):
 1. sa_iso (x \<sqinter> y) = sa_iso x \<sqinter> sa_iso y
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
sa_iso (x \<sqinter> y) = sa_iso x \<sqinter> sa_iso y

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
inf_homomorphism sa_iso

goal (2 subgoals):
 1. uminus_homomorphism sa_iso
 2. bij sa_iso
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. uminus_homomorphism sa_iso
 2. bij sa_iso
[PROOF STEP]
show "\<forall>x::'a . sa_iso (-x) = -sa_iso x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uminus_homomorphism sa_iso
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. sa_iso (- x) = - sa_iso x
[PROOF STEP]
fix x :: 'a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. sa_iso (- x) = - sa_iso x
[PROOF STEP]
have "sa_iso (-x) = Abs_stone_phi_pair (Abs_regular (---x),stone_phi (Abs_regular (--x)) \<squnion> up_filter top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sa_iso (- x) = Abs_stone_phi_pair (Abs_regular (- - - x), stone_phi (Abs_regular (- - x)) \<squnion> up_filter top)
[PROOF STEP]
by (simp add: top_dense_def)
[PROOF STATE]
proof (state)
this:
sa_iso (- x) = Abs_stone_phi_pair (Abs_regular (- - - x), stone_phi (Abs_regular (- - x)) \<squnion> up_filter top)

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

goal (1 subgoal):
 1. \<And>x. sa_iso (- x) = - sa_iso x
[PROOF STEP]
have "... = Abs_stone_phi_pair (Abs_regular (---x),stone_phi (Abs_regular (--x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_stone_phi_pair (Abs_regular (- - - x), stone_phi (Abs_regular (- - x)) \<squnion> up_filter top) = Abs_stone_phi_pair (Abs_regular (- - - x), stone_phi (Abs_regular (- - x)))
[PROOF STEP]
by (metis bot_filter.abs_eq sup_bot.right_neutral up_top)
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (Abs_regular (- - - x), stone_phi (Abs_regular (- - x)) \<squnion> up_filter top) = Abs_stone_phi_pair (Abs_regular (- - - x), stone_phi (Abs_regular (- - x)))

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

goal (1 subgoal):
 1. \<And>x. sa_iso (- x) = - sa_iso x
[PROOF STEP]
have "... = Abs_stone_phi_pair (triple.pairs_uminus 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. Abs_stone_phi_pair (Abs_regular (- - - x), stone_phi (Abs_regular (- - x))) = Abs_stone_phi_pair (stone_phi.pairs_uminus (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))))
[PROOF STEP]
by (subst uminus_regular.abs_eq[THEN sym], unfold eq_onp_same_args) auto
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (Abs_regular (- - - x), stone_phi (Abs_regular (- - x))) = Abs_stone_phi_pair (stone_phi.pairs_uminus (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x))))

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

goal (1 subgoal):
 1. \<And>x. sa_iso (- x) = - sa_iso x
[PROOF STEP]
have "... = -sa_iso x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_stone_phi_pair (stone_phi.pairs_uminus (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) = - sa_iso x
[PROOF STEP]
by (simp add: eq_onp_def sa_iso_triple_pair uminus_stone_phi_pair.abs_eq)
[PROOF STATE]
proof (state)
this:
Abs_stone_phi_pair (stone_phi.pairs_uminus (Abs_regular (- - x), stone_phi (Abs_regular (- x)) \<squnion> up_filter (Abs_dense (x \<squnion> - x)))) = - sa_iso x

goal (1 subgoal):
 1. \<And>x. sa_iso (- x) = - sa_iso x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
sa_iso (- x) = - sa_iso x
[PROOF STEP]
show "sa_iso (-x) = -sa_iso x"
[PROOF STATE]
proof (prove)
using this:
sa_iso (- x) = - sa_iso x

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
uminus_homomorphism sa_iso

goal (1 subgoal):
 1. bij sa_iso
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bij sa_iso
[PROOF STEP]
show "bij sa_iso"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij sa_iso
[PROOF STEP]
by (metis (mono_tags, lifting) sa_iso_left_invertible sa_iso_right_invertible invertible_bij[where g=sa_iso_inv])
[PROOF STATE]
proof (state)
this:
bij sa_iso

goal:
No subgoals!
[PROOF STEP]
qed