[STATEMENT]
lemma pairs_sup_closed:
  assumes "(x,y) \<in> pairs"
      and "(z,w) \<in> pairs"
    shows "pairs_sup (x,y) (z,w) \<in> pairs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pairs_sup (x, y) (z, w) \<in> pairs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pairs_sup (x, y) (z, w) \<in> pairs
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> pairs
(z, w) \<in> pairs
[PROOF STEP]
obtain u v where "y = phi (-x) \<squnion> up_filter u \<and> w = phi (-z) \<squnion> up_filter v"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> pairs
(z, w) \<in> pairs

goal (1 subgoal):
 1. (\<And>u v. y = phi (- x) \<squnion> up_filter u \<and> w = phi (- z) \<squnion> up_filter v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using pairs_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> pairs
(z, w) \<in> pairs
pairs = {(x, y). \<exists>z. y = phi (- x) \<squnion> up_filter z}

goal (1 subgoal):
 1. (\<And>u v. y = phi (- x) \<squnion> up_filter u \<and> w = phi (- z) \<squnion> up_filter v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y = phi (- x) \<squnion> up_filter u \<and> w = phi (- z) \<squnion> up_filter v

goal (1 subgoal):
 1. pairs_sup (x, y) (z, w) \<in> pairs
[PROOF STEP]
hence "pairs_sup (x,y) (z,w) = (x \<squnion> z,(phi (-x) \<squnion> up_filter u) \<sqinter> (phi (-z) \<squnion> up_filter v))"
[PROOF STATE]
proof (prove)
using this:
y = phi (- x) \<squnion> up_filter u \<and> w = phi (- z) \<squnion> up_filter v

goal (1 subgoal):
 1. pairs_sup (x, y) (z, w) = (x \<squnion> z, (phi (- x) \<squnion> up_filter u) \<sqinter> (phi (- z) \<squnion> up_filter v))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pairs_sup (x, y) (z, w) = (x \<squnion> z, (phi (- x) \<squnion> up_filter u) \<sqinter> (phi (- z) \<squnion> up_filter v))

goal (1 subgoal):
 1. pairs_sup (x, y) (z, w) \<in> pairs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pairs_sup (x, y) (z, w) = (x \<squnion> z, (phi (- x) \<squnion> up_filter u) \<sqinter> (phi (- z) \<squnion> up_filter v))

goal (1 subgoal):
 1. pairs_sup (x, y) (z, w) \<in> pairs
[PROOF STEP]
have "... = (x \<squnion> z,(phi (-x) \<sqinter> phi (-z)) \<squnion> (phi (-x) \<sqinter> up_filter v) \<squnion> (up_filter u \<sqinter> phi (-z)) \<squnion> (up_filter u \<sqinter> up_filter v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<squnion> z, (phi (- x) \<squnion> up_filter u) \<sqinter> (phi (- z) \<squnion> up_filter v)) = (x \<squnion> z, phi (- x) \<sqinter> phi (- z) \<squnion> phi (- x) \<sqinter> up_filter v \<squnion> up_filter u \<sqinter> phi (- z) \<squnion> up_filter u \<sqinter> up_filter v)
[PROOF STEP]
by (simp add: inf.sup_commute inf_sup_distrib1 sup_commute sup_left_commute)
[PROOF STATE]
proof (state)
this:
(x \<squnion> z, (phi (- x) \<squnion> up_filter u) \<sqinter> (phi (- z) \<squnion> up_filter v)) = (x \<squnion> z, phi (- x) \<sqinter> phi (- z) \<squnion> phi (- x) \<sqinter> up_filter v \<squnion> up_filter u \<sqinter> phi (- z) \<squnion> up_filter u \<sqinter> up_filter v)

goal (1 subgoal):
 1. pairs_sup (x, y) (z, w) \<in> pairs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x \<squnion> z, (phi (- x) \<squnion> up_filter u) \<sqinter> (phi (- z) \<squnion> up_filter v)) = (x \<squnion> z, phi (- x) \<sqinter> phi (- z) \<squnion> phi (- x) \<sqinter> up_filter v \<squnion> up_filter u \<sqinter> phi (- z) \<squnion> up_filter u \<sqinter> up_filter v)

goal (1 subgoal):
 1. pairs_sup (x, y) (z, w) \<in> pairs
[PROOF STEP]
have "... = (x \<squnion> z,phi (-(x \<squnion> z)) \<squnion> (phi (-x) \<sqinter> up_filter v) \<squnion> (up_filter u \<sqinter> phi (-z)) \<squnion> (up_filter u \<sqinter> up_filter v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<squnion> z, phi (- x) \<sqinter> phi (- z) \<squnion> phi (- x) \<sqinter> up_filter v \<squnion> up_filter u \<sqinter> phi (- z) \<squnion> up_filter u \<sqinter> up_filter v) = (x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> phi (- x) \<sqinter> up_filter v \<squnion> up_filter u \<sqinter> phi (- z) \<squnion> up_filter u \<sqinter> up_filter v)
[PROOF STEP]
using hom
[PROOF STATE]
proof (prove)
using this:
bounded_lattice_homomorphism phi

goal (1 subgoal):
 1. (x \<squnion> z, phi (- x) \<sqinter> phi (- z) \<squnion> phi (- x) \<sqinter> up_filter v \<squnion> up_filter u \<sqinter> phi (- z) \<squnion> up_filter u \<sqinter> up_filter v) = (x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> phi (- x) \<sqinter> up_filter v \<squnion> up_filter u \<sqinter> phi (- z) \<squnion> up_filter u \<sqinter> up_filter v)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x \<squnion> z, phi (- x) \<sqinter> phi (- z) \<squnion> phi (- x) \<sqinter> up_filter v \<squnion> up_filter u \<sqinter> phi (- z) \<squnion> up_filter u \<sqinter> up_filter v) = (x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> phi (- x) \<sqinter> up_filter v \<squnion> up_filter u \<sqinter> phi (- z) \<squnion> up_filter u \<sqinter> up_filter v)

goal (1 subgoal):
 1. pairs_sup (x, y) (z, w) \<in> pairs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x \<squnion> z, phi (- x) \<sqinter> phi (- z) \<squnion> phi (- x) \<sqinter> up_filter v \<squnion> up_filter u \<sqinter> phi (- z) \<squnion> up_filter u \<sqinter> up_filter v) = (x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> phi (- x) \<sqinter> up_filter v \<squnion> up_filter u \<sqinter> phi (- z) \<squnion> up_filter u \<sqinter> up_filter v)

goal (1 subgoal):
 1. pairs_sup (x, y) (z, w) \<in> pairs
[PROOF STEP]
have "... = (x \<squnion> z,phi (-(x \<squnion> z)) \<squnion> up_filter (rho (-x) v) \<squnion> up_filter (rho (-z) u) \<squnion> (up_filter u \<sqinter> up_filter v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> phi (- x) \<sqinter> up_filter v \<squnion> up_filter u \<sqinter> phi (- z) \<squnion> up_filter u \<sqinter> up_filter v) = (x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> up_filter (rho (- x) v) \<squnion> up_filter (rho (- z) u) \<squnion> up_filter u \<sqinter> up_filter v)
[PROOF STEP]
by (metis inf.sup_commute rho_char)
[PROOF STATE]
proof (state)
this:
(x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> phi (- x) \<sqinter> up_filter v \<squnion> up_filter u \<sqinter> phi (- z) \<squnion> up_filter u \<sqinter> up_filter v) = (x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> up_filter (rho (- x) v) \<squnion> up_filter (rho (- z) u) \<squnion> up_filter u \<sqinter> up_filter v)

goal (1 subgoal):
 1. pairs_sup (x, y) (z, w) \<in> pairs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> phi (- x) \<sqinter> up_filter v \<squnion> up_filter u \<sqinter> phi (- z) \<squnion> up_filter u \<sqinter> up_filter v) = (x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> up_filter (rho (- x) v) \<squnion> up_filter (rho (- z) u) \<squnion> up_filter u \<sqinter> up_filter v)

goal (1 subgoal):
 1. pairs_sup (x, y) (z, w) \<in> pairs
[PROOF STEP]
have "... = (x \<squnion> z,phi (-(x \<squnion> z)) \<squnion> up_filter (rho (-x) v) \<squnion> up_filter (rho (-z) u) \<squnion> up_filter (u \<squnion> v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> up_filter (rho (- x) v) \<squnion> up_filter (rho (- z) u) \<squnion> up_filter u \<sqinter> up_filter v) = (x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> up_filter (rho (- x) v) \<squnion> up_filter (rho (- z) u) \<squnion> up_filter (u \<squnion> v))
[PROOF STEP]
by (metis up_filter_dist_sup)
[PROOF STATE]
proof (state)
this:
(x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> up_filter (rho (- x) v) \<squnion> up_filter (rho (- z) u) \<squnion> up_filter u \<sqinter> up_filter v) = (x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> up_filter (rho (- x) v) \<squnion> up_filter (rho (- z) u) \<squnion> up_filter (u \<squnion> v))

goal (1 subgoal):
 1. pairs_sup (x, y) (z, w) \<in> pairs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> up_filter (rho (- x) v) \<squnion> up_filter (rho (- z) u) \<squnion> up_filter u \<sqinter> up_filter v) = (x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> up_filter (rho (- x) v) \<squnion> up_filter (rho (- z) u) \<squnion> up_filter (u \<squnion> v))

goal (1 subgoal):
 1. pairs_sup (x, y) (z, w) \<in> pairs
[PROOF STEP]
have "... = (x \<squnion> z,phi (-(x \<squnion> z)) \<squnion> up_filter (rho (-x) v \<sqinter> rho (-z) u \<sqinter> (u \<squnion> v)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> up_filter (rho (- x) v) \<squnion> up_filter (rho (- z) u) \<squnion> up_filter (u \<squnion> v)) = (x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> up_filter (rho (- x) v \<sqinter> rho (- z) u \<sqinter> (u \<squnion> v)))
[PROOF STEP]
by (simp add: sup_commute sup_left_commute up_filter_dist_inf)
[PROOF STATE]
proof (state)
this:
(x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> up_filter (rho (- x) v) \<squnion> up_filter (rho (- z) u) \<squnion> up_filter (u \<squnion> v)) = (x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> up_filter (rho (- x) v \<sqinter> rho (- z) u \<sqinter> (u \<squnion> v)))

goal (1 subgoal):
 1. pairs_sup (x, y) (z, w) \<in> pairs
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
pairs_sup (x, y) (z, w) = (x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> up_filter (rho (- x) v \<sqinter> rho (- z) u \<sqinter> (u \<squnion> v)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pairs_sup (x, y) (z, w) = (x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> up_filter (rho (- x) v \<sqinter> rho (- z) u \<sqinter> (u \<squnion> v)))

goal (1 subgoal):
 1. pairs_sup (x, y) (z, w) \<in> pairs
[PROOF STEP]
using pairs_def
[PROOF STATE]
proof (prove)
using this:
pairs_sup (x, y) (z, w) = (x \<squnion> z, phi (- (x \<squnion> z)) \<squnion> up_filter (rho (- x) v \<sqinter> rho (- z) u \<sqinter> (u \<squnion> v)))
pairs = {(x, y). \<exists>z. y = phi (- x) \<squnion> up_filter z}

goal (1 subgoal):
 1. pairs_sup (x, y) (z, w) \<in> pairs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pairs_sup (x, y) (z, w) \<in> pairs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pairs_inf_closed:
  assumes "(x,y) \<in> pairs"
      and "(z,w) \<in> pairs"
    shows "pairs_inf (x,y) (z,w) \<in> pairs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pairs_inf (x, y) (z, w) \<in> pairs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pairs_inf (x, y) (z, w) \<in> pairs
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> pairs
(z, w) \<in> pairs
[PROOF STEP]
obtain u v where "y = phi (-x) \<squnion> up_filter u \<and> w = phi (-z) \<squnion> up_filter v"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> pairs
(z, w) \<in> pairs

goal (1 subgoal):
 1. (\<And>u v. y = phi (- x) \<squnion> up_filter u \<and> w = phi (- z) \<squnion> up_filter v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using pairs_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> pairs
(z, w) \<in> pairs
pairs = {(x, y). \<exists>z. y = phi (- x) \<squnion> up_filter z}

goal (1 subgoal):
 1. (\<And>u v. y = phi (- x) \<squnion> up_filter u \<and> w = phi (- z) \<squnion> up_filter v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y = phi (- x) \<squnion> up_filter u \<and> w = phi (- z) \<squnion> up_filter v

goal (1 subgoal):
 1. pairs_inf (x, y) (z, w) \<in> pairs
[PROOF STEP]
hence "pairs_inf (x,y) (z,w) = (x \<sqinter> z,(phi (-x) \<squnion> up_filter u) \<squnion> (phi (-z) \<squnion> up_filter v))"
[PROOF STATE]
proof (prove)
using this:
y = phi (- x) \<squnion> up_filter u \<and> w = phi (- z) \<squnion> up_filter v

goal (1 subgoal):
 1. pairs_inf (x, y) (z, w) = (x \<sqinter> z, phi (- x) \<squnion> up_filter u \<squnion> (phi (- z) \<squnion> up_filter v))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pairs_inf (x, y) (z, w) = (x \<sqinter> z, phi (- x) \<squnion> up_filter u \<squnion> (phi (- z) \<squnion> up_filter v))

goal (1 subgoal):
 1. pairs_inf (x, y) (z, w) \<in> pairs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pairs_inf (x, y) (z, w) = (x \<sqinter> z, phi (- x) \<squnion> up_filter u \<squnion> (phi (- z) \<squnion> up_filter v))

goal (1 subgoal):
 1. pairs_inf (x, y) (z, w) \<in> pairs
[PROOF STEP]
have "... = (x \<sqinter> z,(phi (-x) \<squnion> phi (-z)) \<squnion> (up_filter u \<squnion> up_filter v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> z, phi (- x) \<squnion> up_filter u \<squnion> (phi (- z) \<squnion> up_filter v)) = (x \<sqinter> z, phi (- x) \<squnion> phi (- z) \<squnion> (up_filter u \<squnion> up_filter v))
[PROOF STEP]
by (simp add: sup_commute sup_left_commute)
[PROOF STATE]
proof (state)
this:
(x \<sqinter> z, phi (- x) \<squnion> up_filter u \<squnion> (phi (- z) \<squnion> up_filter v)) = (x \<sqinter> z, phi (- x) \<squnion> phi (- z) \<squnion> (up_filter u \<squnion> up_filter v))

goal (1 subgoal):
 1. pairs_inf (x, y) (z, w) \<in> pairs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x \<sqinter> z, phi (- x) \<squnion> up_filter u \<squnion> (phi (- z) \<squnion> up_filter v)) = (x \<sqinter> z, phi (- x) \<squnion> phi (- z) \<squnion> (up_filter u \<squnion> up_filter v))

goal (1 subgoal):
 1. pairs_inf (x, y) (z, w) \<in> pairs
[PROOF STEP]
have "... = (x \<sqinter> z,phi (-(x \<sqinter> z)) \<squnion> (up_filter u \<squnion> up_filter v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> z, phi (- x) \<squnion> phi (- z) \<squnion> (up_filter u \<squnion> up_filter v)) = (x \<sqinter> z, phi (- (x \<sqinter> z)) \<squnion> (up_filter u \<squnion> up_filter v))
[PROOF STEP]
using hom
[PROOF STATE]
proof (prove)
using this:
bounded_lattice_homomorphism phi

goal (1 subgoal):
 1. (x \<sqinter> z, phi (- x) \<squnion> phi (- z) \<squnion> (up_filter u \<squnion> up_filter v)) = (x \<sqinter> z, phi (- (x \<sqinter> z)) \<squnion> (up_filter u \<squnion> up_filter v))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x \<sqinter> z, phi (- x) \<squnion> phi (- z) \<squnion> (up_filter u \<squnion> up_filter v)) = (x \<sqinter> z, phi (- (x \<sqinter> z)) \<squnion> (up_filter u \<squnion> up_filter v))

goal (1 subgoal):
 1. pairs_inf (x, y) (z, w) \<in> pairs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(x \<sqinter> z, phi (- x) \<squnion> phi (- z) \<squnion> (up_filter u \<squnion> up_filter v)) = (x \<sqinter> z, phi (- (x \<sqinter> z)) \<squnion> (up_filter u \<squnion> up_filter v))

goal (1 subgoal):
 1. pairs_inf (x, y) (z, w) \<in> pairs
[PROOF STEP]
have "... = (x \<sqinter> z,phi (-(x \<sqinter> z)) \<squnion> up_filter (u \<sqinter> v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> z, phi (- (x \<sqinter> z)) \<squnion> (up_filter u \<squnion> up_filter v)) = (x \<sqinter> z, phi (- (x \<sqinter> z)) \<squnion> up_filter (u \<sqinter> v))
[PROOF STEP]
by (simp add: up_filter_dist_inf)
[PROOF STATE]
proof (state)
this:
(x \<sqinter> z, phi (- (x \<sqinter> z)) \<squnion> (up_filter u \<squnion> up_filter v)) = (x \<sqinter> z, phi (- (x \<sqinter> z)) \<squnion> up_filter (u \<sqinter> v))

goal (1 subgoal):
 1. pairs_inf (x, y) (z, w) \<in> pairs
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
pairs_inf (x, y) (z, w) = (x \<sqinter> z, phi (- (x \<sqinter> z)) \<squnion> up_filter (u \<sqinter> v))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pairs_inf (x, y) (z, w) = (x \<sqinter> z, phi (- (x \<sqinter> z)) \<squnion> up_filter (u \<sqinter> v))

goal (1 subgoal):
 1. pairs_inf (x, y) (z, w) \<in> pairs
[PROOF STEP]
using pairs_def
[PROOF STATE]
proof (prove)
using this:
pairs_inf (x, y) (z, w) = (x \<sqinter> z, phi (- (x \<sqinter> z)) \<squnion> up_filter (u \<sqinter> v))
pairs = {(x, y). \<exists>z. y = phi (- x) \<squnion> up_filter z}

goal (1 subgoal):
 1. pairs_inf (x, y) (z, w) \<in> pairs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
pairs_inf (x, y) (z, w) \<in> pairs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pairs_uminus_closed:
  "pairs_uminus (x,y) \<in> pairs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pairs_uminus (x, y) \<in> pairs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. pairs_uminus (x, y) \<in> pairs
[PROOF STEP]
have "pairs_uminus (x,y) = (-x,phi (--x) \<squnion> bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pairs_uminus (x, y) = (- x, phi (- - x) \<squnion> bot)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
pairs_uminus (x, y) = (- x, phi (- - x) \<squnion> bot)

goal (1 subgoal):
 1. pairs_uminus (x, y) \<in> pairs
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
pairs_uminus (x, y) = (- x, phi (- - x) \<squnion> bot)

goal (1 subgoal):
 1. pairs_uminus (x, y) \<in> pairs
[PROOF STEP]
have "... = (-x,phi (--x) \<squnion> up_filter top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- x, phi (- - x) \<squnion> bot) = (- x, phi (- - x) \<squnion> up_filter top)
[PROOF STEP]
by (simp add: bot_filter.abs_eq)
[PROOF STATE]
proof (state)
this:
(- x, phi (- - x) \<squnion> bot) = (- x, phi (- - x) \<squnion> up_filter top)

goal (1 subgoal):
 1. pairs_uminus (x, y) \<in> pairs
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
pairs_uminus (x, y) = (- x, phi (- - x) \<squnion> up_filter top)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
pairs_uminus (x, y) = (- x, phi (- - x) \<squnion> up_filter top)

goal (1 subgoal):
 1. pairs_uminus (x, y) \<in> pairs
[PROOF STEP]
by (metis (mono_tags, lifting) mem_Collect_eq old.prod.case pairs_def)
[PROOF STATE]
proof (state)
this:
pairs_uminus (x, y) \<in> pairs

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pairs_bot_closed:
  "pairs_bot \<in> pairs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pairs_bot \<in> pairs
[PROOF STEP]
using pairs_def phi_top triple.hom triple_axioms
[PROOF STATE]
proof (prove)
using this:
pairs = {(x, y). \<exists>z. y = phi (- x) \<squnion> up_filter z}
phi top = Filters.filter.Abs_filter UNIV
triple ?phi \<Longrightarrow> bounded_lattice_homomorphism ?phi
triple phi

goal (1 subgoal):
 1. pairs_bot \<in> pairs
[PROOF STEP]
by fastforce


[STATEMENT]
lemma pairs_top_closed:
  "pairs_top \<in> pairs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pairs_top \<in> pairs
[PROOF STEP]
by (metis p_bot pairs_uminus.simps pairs_uminus_closed phi_bot)


[STATEMENT]
lemma pairs_sup_dist_inf:
  "(x,y) \<in> pairs \<Longrightarrow> (z,w) \<in> pairs \<Longrightarrow> (u,v) \<in> pairs \<Longrightarrow> pairs_sup (x,y) (pairs_inf (z,w) (u,v)) = pairs_inf (pairs_sup (x,y) (z,w)) (pairs_sup (x,y) (u,v))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, y) \<in> pairs; (z, w) \<in> pairs; (u, v) \<in> pairs\<rbrakk> \<Longrightarrow> pairs_sup (x, y) (pairs_inf (z, w) (u, v)) = pairs_inf (pairs_sup (x, y) (z, w)) (pairs_sup (x, y) (u, v))
[PROOF STEP]
using sup_inf_distrib1 inf_sup_distrib1
[PROOF STATE]
proof (prove)
using this:
?x \<squnion> ?y \<sqinter> ?z = (?x \<squnion> ?y) \<sqinter> (?x \<squnion> ?z)
?x \<sqinter> (?y \<squnion> ?z) = ?x \<sqinter> ?y \<squnion> ?x \<sqinter> ?z

goal (1 subgoal):
 1. \<lbrakk>(x, y) \<in> pairs; (z, w) \<in> pairs; (u, v) \<in> pairs\<rbrakk> \<Longrightarrow> pairs_sup (x, y) (pairs_inf (z, w) (u, v)) = pairs_inf (pairs_sup (x, y) (z, w)) (pairs_sup (x, y) (u, v))
[PROOF STEP]
by auto


[STATEMENT]
lemma pairs_phi_less_eq:
  "(x,y) \<in> pairs \<Longrightarrow> phi (-x) \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> pairs \<Longrightarrow> phi (- x) \<le> y
[PROOF STEP]
using pairs_def
[PROOF STATE]
proof (prove)
using this:
pairs = {(x, y). \<exists>z. y = phi (- x) \<squnion> up_filter z}

goal (1 subgoal):
 1. (x, y) \<in> pairs \<Longrightarrow> phi (- x) \<le> y
[PROOF STEP]
by auto


[STATEMENT]
lemma pairs_uminus_galois:
  assumes "(x,y) \<in> pairs"
      and "(z,w) \<in> pairs"
    shows "pairs_inf (x,y) (z,w) = pairs_bot \<longleftrightarrow> pairs_less_eq (x,y) (pairs_uminus (z,w))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pairs_inf (x, y) (z, w) = pairs_bot) = pairs_less_eq (x, y) (pairs_uminus (z, w))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (pairs_inf (x, y) (z, w) = pairs_bot) = pairs_less_eq (x, y) (pairs_uminus (z, w))
[PROOF STEP]
have 1: "x \<sqinter> z = bot \<and> y \<squnion> w = Abs_filter UNIV \<longrightarrow> phi z \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sqinter> z = bot \<and> y \<squnion> w = Filters.filter.Abs_filter UNIV \<longrightarrow> phi z \<le> y
[PROOF STEP]
by (metis (no_types, lifting) assms(1) heyting.implies_inf_absorb hom le_supE pairs_phi_less_eq sup_bot_right)
[PROOF STATE]
proof (state)
this:
x \<sqinter> z = bot \<and> y \<squnion> w = Filters.filter.Abs_filter UNIV \<longrightarrow> phi z \<le> y

goal (1 subgoal):
 1. (pairs_inf (x, y) (z, w) = pairs_bot) = pairs_less_eq (x, y) (pairs_uminus (z, w))
[PROOF STEP]
have 2: "x \<le> -z \<and> phi z \<le> y \<longrightarrow> y \<squnion> w = Abs_filter UNIV"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> - z \<and> phi z \<le> y \<longrightarrow> y \<squnion> w = Filters.filter.Abs_filter UNIV
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<le> - z \<and> phi z \<le> y \<Longrightarrow> y \<squnion> w = Filters.filter.Abs_filter UNIV
[PROOF STEP]
assume 3: "x \<le> -z \<and> phi z \<le> y"
[PROOF STATE]
proof (state)
this:
x \<le> - z \<and> phi z \<le> y

goal (1 subgoal):
 1. x \<le> - z \<and> phi z \<le> y \<Longrightarrow> y \<squnion> w = Filters.filter.Abs_filter UNIV
[PROOF STEP]
have "Abs_filter UNIV = phi z \<squnion> phi (-z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Filters.filter.Abs_filter UNIV = phi z \<squnion> phi (- z)
[PROOF STEP]
using hom phi_complemented phi_top
[PROOF STATE]
proof (prove)
using this:
bounded_lattice_homomorphism phi
complement (phi ?x) (phi (- ?x))
phi top = Filters.filter.Abs_filter UNIV

goal (1 subgoal):
 1. Filters.filter.Abs_filter UNIV = phi z \<squnion> phi (- z)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Filters.filter.Abs_filter UNIV = phi z \<squnion> phi (- z)

goal (1 subgoal):
 1. x \<le> - z \<and> phi z \<le> y \<Longrightarrow> y \<squnion> w = Filters.filter.Abs_filter UNIV
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Filters.filter.Abs_filter UNIV = phi z \<squnion> phi (- z)

goal (1 subgoal):
 1. x \<le> - z \<and> phi z \<le> y \<Longrightarrow> y \<squnion> w = Filters.filter.Abs_filter UNIV
[PROOF STEP]
have "... \<le> y \<squnion> w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. phi z \<squnion> phi (- z) \<le> y \<squnion> w
[PROOF STEP]
using 3 assms(2) sup_mono pairs_phi_less_eq
[PROOF STATE]
proof (prove)
using this:
x \<le> - z \<and> phi z \<le> y
(z, w) \<in> pairs
\<lbrakk>?a \<le> ?c; ?b \<le> ?d\<rbrakk> \<Longrightarrow> ?a \<squnion> ?b \<le> ?c \<squnion> ?d
(?x, ?y) \<in> pairs \<Longrightarrow> phi (- ?x) \<le> ?y

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

goal (1 subgoal):
 1. x \<le> - z \<and> phi z \<le> y \<Longrightarrow> y \<squnion> w = Filters.filter.Abs_filter UNIV
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Filters.filter.Abs_filter UNIV \<le> y \<squnion> w
[PROOF STEP]
show "y \<squnion> w = Abs_filter UNIV"
[PROOF STATE]
proof (prove)
using this:
Filters.filter.Abs_filter UNIV \<le> y \<squnion> w

goal (1 subgoal):
 1. y \<squnion> w = Filters.filter.Abs_filter UNIV
[PROOF STEP]
using hom phi_top top.extremum_uniqueI
[PROOF STATE]
proof (prove)
using this:
Filters.filter.Abs_filter UNIV \<le> y \<squnion> w
bounded_lattice_homomorphism phi
phi top = Filters.filter.Abs_filter UNIV
top \<le> ?a \<Longrightarrow> ?a = top

goal (1 subgoal):
 1. y \<squnion> w = Filters.filter.Abs_filter UNIV
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y \<squnion> w = Filters.filter.Abs_filter UNIV

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
x \<le> - z \<and> phi z \<le> y \<longrightarrow> y \<squnion> w = Filters.filter.Abs_filter UNIV

goal (1 subgoal):
 1. (pairs_inf (x, y) (z, w) = pairs_bot) = pairs_less_eq (x, y) (pairs_uminus (z, w))
[PROOF STEP]
have "x \<sqinter> z = bot \<longleftrightarrow> x \<le> -z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x \<sqinter> z = bot) = (x \<le> - z)
[PROOF STEP]
by (simp add: shunting_1)
[PROOF STATE]
proof (state)
this:
(x \<sqinter> z = bot) = (x \<le> - z)

goal (1 subgoal):
 1. (pairs_inf (x, y) (z, w) = pairs_bot) = pairs_less_eq (x, y) (pairs_uminus (z, w))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(x \<sqinter> z = bot) = (x \<le> - z)

goal (1 subgoal):
 1. (pairs_inf (x, y) (z, w) = pairs_bot) = pairs_less_eq (x, y) (pairs_uminus (z, w))
[PROOF STEP]
using 1 2 Pair_inject pairs_inf.simps pairs_less_eq.simps pairs_uminus.simps
[PROOF STATE]
proof (prove)
using this:
(x \<sqinter> z = bot) = (x \<le> - z)
x \<sqinter> z = bot \<and> y \<squnion> w = Filters.filter.Abs_filter UNIV \<longrightarrow> phi z \<le> y
x \<le> - z \<and> phi z \<le> y \<longrightarrow> y \<squnion> w = Filters.filter.Abs_filter UNIV
\<lbrakk>(?a, ?b) = (?a', ?b'); \<lbrakk>?a = ?a'; ?b = ?b'\<rbrakk> \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R
pairs_inf (?x, ?y) (?z, ?w) = (?x \<sqinter> ?z, ?y \<squnion> ?w)
pairs_less_eq (?x, ?y) (?z, ?w) = (?x \<le> ?z \<and> ?w \<le> ?y)
pairs_uminus (?x, ?y) = (- ?x, phi ?x)

goal (1 subgoal):
 1. (pairs_inf (x, y) (z, w) = pairs_bot) = pairs_less_eq (x, y) (pairs_uminus (z, w))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(pairs_inf (x, y) (z, w) = pairs_bot) = pairs_less_eq (x, y) (pairs_uminus (z, w))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma pairs_stone:
  "(x,y) \<in> pairs \<Longrightarrow> pairs_sup (pairs_uminus (x,y)) (pairs_uminus (pairs_uminus (x,y))) = pairs_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> pairs \<Longrightarrow> pairs_sup (pairs_uminus (x, y)) (pairs_uminus (pairs_uminus (x, y))) = pairs_top
[PROOF STEP]
by (metis hom pairs_sup.simps pairs_uminus.simps phi_bot phi_complemented stone)


[STATEMENT]
lemma dense_pairs:
  "dense_pairs = { (x,y) . x = top \<and> is_principal_up_filter y }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). (x, y) \<in> pairs \<and> pairs_uminus (x, y) = pairs_bot} = {(x, y). x = top \<and> (\<exists>ya. y = up_filter ya)}
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {(x, y). (x, y) \<in> pairs \<and> pairs_uminus (x, y) = pairs_bot} = {(x, y). x = top \<and> (\<exists>ya. y = up_filter ya)}
[PROOF STEP]
have "dense_pairs = { (x,y) . (x,y) \<in> pairs \<and> x = top }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). (x, y) \<in> pairs \<and> pairs_uminus (x, y) = pairs_bot} = {(x, y). (x, y) \<in> pairs \<and> x = top}
[PROOF STEP]
by (metis Pair_inject compl_bot_eq double_compl pairs_uminus.simps phi_top)
[PROOF STATE]
proof (state)
this:
{(x, y). (x, y) \<in> pairs \<and> pairs_uminus (x, y) = pairs_bot} = {(x, y). (x, y) \<in> pairs \<and> x = top}

goal (1 subgoal):
 1. {(x, y). (x, y) \<in> pairs \<and> pairs_uminus (x, y) = pairs_bot} = {(x, y). x = top \<and> (\<exists>ya. y = up_filter ya)}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{(x, y). (x, y) \<in> pairs \<and> pairs_uminus (x, y) = pairs_bot} = {(x, y). (x, y) \<in> pairs \<and> x = top}

goal (1 subgoal):
 1. {(x, y). (x, y) \<in> pairs \<and> pairs_uminus (x, y) = pairs_bot} = {(x, y). x = top \<and> (\<exists>ya. y = up_filter ya)}
[PROOF STEP]
have "... = { (x,y) . (\<exists>z . y = up_filter z) \<and> x = top }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, y). (x, y) \<in> pairs \<and> x = top} = {(x, y). (\<exists>z. y = up_filter z) \<and> x = top}
[PROOF STEP]
using hom pairs_def
[PROOF STATE]
proof (prove)
using this:
bounded_lattice_homomorphism phi
pairs = {(x, y). \<exists>z. y = phi (- x) \<squnion> up_filter z}

goal (1 subgoal):
 1. {(x, y). (x, y) \<in> pairs \<and> x = top} = {(x, y). (\<exists>z. y = up_filter z) \<and> x = top}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(x, y). (x, y) \<in> pairs \<and> x = top} = {(x, y). (\<exists>z. y = up_filter z) \<and> x = top}

goal (1 subgoal):
 1. {(x, y). (x, y) \<in> pairs \<and> pairs_uminus (x, y) = pairs_bot} = {(x, y). x = top \<and> (\<exists>ya. y = up_filter ya)}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
{(x, y). (x, y) \<in> pairs \<and> pairs_uminus (x, y) = pairs_bot} = {(x, y). (\<exists>z. y = up_filter z) \<and> x = top}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{(x, y). (x, y) \<in> pairs \<and> pairs_uminus (x, y) = pairs_bot} = {(x, y). (\<exists>z. y = up_filter z) \<and> x = top}

goal (1 subgoal):
 1. {(x, y). (x, y) \<in> pairs \<and> pairs_uminus (x, y) = pairs_bot} = {(x, y). x = top \<and> (\<exists>ya. y = up_filter ya)}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{(x, y). (x, y) \<in> pairs \<and> pairs_uminus (x, y) = pairs_bot} = {(x, y). x = top \<and> (\<exists>ya. y = up_filter ya)}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma regular_pairs:
  "regular_pairs = { (x,y) . y = phi (-x) }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. regular_pairs = {(x, y). y = phi (- x)}
[PROOF STEP]
using pairs_def pairs_uminus_closed
[PROOF STATE]
proof (prove)
using this:
pairs = {(x, y). \<exists>z. y = phi (- x) \<squnion> up_filter z}
pairs_uminus (?x, ?y) \<in> pairs

goal (1 subgoal):
 1. regular_pairs = {(x, y). y = phi (- x)}
[PROOF STEP]
by fastforce


[STATEMENT]
lemma get_rho_pair_char:
  assumes "(x,y) \<in> pairs"
    shows "up_filter (rho_pair (x,y)) = phi x \<sqinter> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. up_filter (rho_pair (x, y)) = phi x \<sqinter> y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. up_filter (rho_pair (x, y)) = phi x \<sqinter> y
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> pairs
[PROOF STEP]
obtain w where "y = phi (-x) \<squnion> up_filter w"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> pairs

goal (1 subgoal):
 1. (\<And>w. y = phi (- x) \<squnion> up_filter w \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using pairs_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> pairs
pairs = {(x, y). \<exists>z. y = phi (- x) \<squnion> up_filter z}

goal (1 subgoal):
 1. (\<And>w. y = phi (- x) \<squnion> up_filter w \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y = phi (- x) \<squnion> up_filter w

goal (1 subgoal):
 1. up_filter (rho_pair (x, y)) = phi x \<sqinter> y
[PROOF STEP]
hence "phi x \<sqinter> y = phi x \<sqinter> up_filter w"
[PROOF STATE]
proof (prove)
using this:
y = phi (- x) \<squnion> up_filter w

goal (1 subgoal):
 1. phi x \<sqinter> y = phi x \<sqinter> up_filter w
[PROOF STEP]
by (simp add: inf_sup_distrib1 phi_complemented)
[PROOF STATE]
proof (state)
this:
phi x \<sqinter> y = phi x \<sqinter> up_filter w

goal (1 subgoal):
 1. up_filter (rho_pair (x, y)) = phi x \<sqinter> y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
phi x \<sqinter> y = phi x \<sqinter> up_filter w

goal (1 subgoal):
 1. up_filter (rho_pair (x, y)) = phi x \<sqinter> y
[PROOF STEP]
using rho_char
[PROOF STATE]
proof (prove)
using this:
phi x \<sqinter> y = phi x \<sqinter> up_filter w
up_filter (rho ?x ?y) = phi ?x \<sqinter> up_filter ?y

goal (1 subgoal):
 1. up_filter (rho_pair (x, y)) = phi x \<sqinter> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
up_filter (rho_pair (x, y)) = phi x \<sqinter> y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sa_iso_pair:
  "(--x,phi (-x) \<squnion> up_filter y) \<in> pairs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- - x, phi (- x) \<squnion> up_filter y) \<in> pairs
[PROOF STEP]
using pairs_def
[PROOF STATE]
proof (prove)
using this:
pairs = {(x, y). \<exists>z. y = phi (- x) \<squnion> up_filter z}

goal (1 subgoal):
 1. (- - x, phi (- x) \<squnion> up_filter y) \<in> pairs
[PROOF STEP]
by auto


[STATEMENT]
lemma simp_phi [simp]:
  "bounded_lattice_homomorphism (Rep_phi x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_lattice_homomorphism (Rep_phi x)
[PROOF STEP]
using Rep_phi
[PROOF STATE]
proof (prove)
using this:
Rep_phi ?x \<in> {f. bounded_lattice_homomorphism f}

goal (1 subgoal):
 1. bounded_lattice_homomorphism (Rep_phi x)
[PROOF STEP]
by simp


[STATEMENT]
lemma simp_lifted_pair [simp]:
  "\<forall>f . Rep_lifted_pair pf f \<in> triple.pairs (Rep_phi f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f. Rep_lifted_pair pf f \<in> triple.pairs (Rep_phi f)
[PROOF STEP]
using Rep_lifted_pair
[PROOF STATE]
proof (prove)
using this:
Rep_lifted_pair ?x \<in> {pf. \<forall>f. pf f \<in> triple.pairs (Rep_phi f)}

goal (1 subgoal):
 1. \<forall>f. Rep_lifted_pair pf f \<in> triple.pairs (Rep_phi f)
[PROOF STEP]
by simp


[STATEMENT]
lemma stone_phi_embed_triple_pair:
  "(if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) \<in> triple.pairs (Rep_phi f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) \<in> triple.pairs (Rep_phi f)
[PROOF STEP]
by (metis (no_types, opaque_lifting) Rep_stone_phi_pair simp_phi surj_pair triple.pairs_uminus_closed triple_def)