[STATEMENT]
lemma stone_phi_embed_homomorphism:
  "sup_inf_top_bot_uminus_ord_homomorphism stone_phi_embed"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_inf_top_bot_uminus_ord_homomorphism stone_phi_embed
[PROOF STEP]
proof (intro conjI)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. sup_homomorphism stone_phi_embed
 2. inf_homomorphism stone_phi_embed
 3. top_homomorphism stone_phi_embed
 4. bot_homomorphism stone_phi_embed
 5. uminus_homomorphism stone_phi_embed
 6. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
let ?p = "\<lambda>f . triple.pairs_uminus (Rep_phi f)"
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. sup_homomorphism stone_phi_embed
 2. inf_homomorphism stone_phi_embed
 3. top_homomorphism stone_phi_embed
 4. bot_homomorphism stone_phi_embed
 5. uminus_homomorphism stone_phi_embed
 6. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
let ?pp = "\<lambda>f x . ?p f (?p f x)"
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. sup_homomorphism stone_phi_embed
 2. inf_homomorphism stone_phi_embed
 3. top_homomorphism stone_phi_embed
 4. bot_homomorphism stone_phi_embed
 5. uminus_homomorphism stone_phi_embed
 6. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
let ?q = "\<lambda>f x . ?pp f (Rep_stone_phi_pair x)"
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. sup_homomorphism stone_phi_embed
 2. inf_homomorphism stone_phi_embed
 3. top_homomorphism stone_phi_embed
 4. bot_homomorphism stone_phi_embed
 5. uminus_homomorphism stone_phi_embed
 6. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
show "\<forall>x y::'a stone_phi_pair . stone_phi_embed (x \<squnion> y) = stone_phi_embed x \<squnion> stone_phi_embed y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_homomorphism stone_phi_embed
[PROOF STEP]
proof (intro allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<squnion> y) = stone_phi_embed x \<squnion> stone_phi_embed y
[PROOF STEP]
fix x y :: "'a stone_phi_pair"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<squnion> y) = stone_phi_embed x \<squnion> stone_phi_embed y
[PROOF STEP]
have 1: "\<forall>f . triple.pairs_sup (?q f x) (?q f y) = ?q f (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
fix f :: "('a regular,'a dense) phi"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
let ?r = "Rep_phi f"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
obtain x1 x2 y1 y2 where 2: "(x1,x2) = Rep_stone_phi_pair x \<and> (y1,y2) = Rep_stone_phi_pair y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2 y1 y2. (x1, x2) = Rep_stone_phi_pair x \<and> (y1, y2) = Rep_stone_phi_pair y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

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

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
hence "triple.pairs_sup (?q f x) (?q f y) = triple.pairs_sup (?pp f (x1,x2)) (?pp f (y1,y2))"
[PROOF STATE]
proof (prove)
using this:
(x1, x2) = Rep_stone_phi_pair x \<and> (y1, y2) = Rep_stone_phi_pair y

goal (1 subgoal):
 1. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (y1, y2)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (y1, y2)))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (y1, y2)))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
have "... = triple.pairs_sup (--x1,?r (-x1)) (--y1,?r (-y1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (y1, y2))) = stone_phi.pairs_sup (- - x1, Rep_phi f (- x1)) (- - y1, Rep_phi f (- y1))
[PROOF STEP]
by (simp add: triple.pairs_uminus.simps triple_def)
[PROOF STATE]
proof (state)
this:
stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (y1, y2))) = stone_phi.pairs_sup (- - x1, Rep_phi f (- x1)) (- - y1, Rep_phi f (- y1))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (y1, y2))) = stone_phi.pairs_sup (- - x1, Rep_phi f (- x1)) (- - y1, Rep_phi f (- y1))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
have "... = (--x1 \<squnion> --y1,?r (-x1) \<sqinter> ?r (-y1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi.pairs_sup (- - x1, Rep_phi f (- x1)) (- - y1, Rep_phi f (- y1)) = (- - x1 \<squnion> - - y1, Rep_phi f (- x1) \<sqinter> Rep_phi f (- y1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stone_phi.pairs_sup (- - x1, Rep_phi f (- x1)) (- - y1, Rep_phi f (- y1)) = (- - x1 \<squnion> - - y1, Rep_phi f (- x1) \<sqinter> Rep_phi f (- y1))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
stone_phi.pairs_sup (- - x1, Rep_phi f (- x1)) (- - y1, Rep_phi f (- y1)) = (- - x1 \<squnion> - - y1, Rep_phi f (- x1) \<sqinter> Rep_phi f (- y1))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
have "... = (--(x1 \<squnion> y1),?r (-(x1 \<squnion> y1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- - x1 \<squnion> - - y1, Rep_phi f (- x1) \<sqinter> Rep_phi f (- y1)) = (- - (x1 \<squnion> y1), Rep_phi f (- (x1 \<squnion> y1)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(- - x1 \<squnion> - - y1, Rep_phi f (- x1) \<sqinter> Rep_phi f (- y1)) = (- - (x1 \<squnion> y1), Rep_phi f (- (x1 \<squnion> y1)))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(- - x1 \<squnion> - - y1, Rep_phi f (- x1) \<sqinter> Rep_phi f (- y1)) = (- - (x1 \<squnion> y1), Rep_phi f (- (x1 \<squnion> y1)))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
have "... = ?pp f (x1 \<squnion> y1,x2 \<sqinter> y2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- - (x1 \<squnion> y1), Rep_phi f (- (x1 \<squnion> y1))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1 \<squnion> y1, x2 \<sqinter> y2))
[PROOF STEP]
by (simp add: triple.pairs_uminus.simps triple_def)
[PROOF STATE]
proof (state)
this:
(- - (x1 \<squnion> y1), Rep_phi f (- (x1 \<squnion> y1))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1 \<squnion> y1, x2 \<sqinter> y2))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(- - (x1 \<squnion> y1), Rep_phi f (- (x1 \<squnion> y1))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1 \<squnion> y1, x2 \<sqinter> y2))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
have "... = ?pp f (triple.pairs_sup (x1,x2) (y1,y2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1 \<squnion> y1, x2 \<sqinter> y2)) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (stone_phi.pairs_sup (x1, x2) (y1, y2)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1 \<squnion> y1, x2 \<sqinter> y2)) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (stone_phi.pairs_sup (x1, x2) (y1, y2)))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1 \<squnion> y1, x2 \<sqinter> y2)) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (stone_phi.pairs_sup (x1, x2) (y1, y2)))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
have "... = ?q f (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (stone_phi.pairs_sup (x1, x2) (y1, y2))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
(x1, x2) = Rep_stone_phi_pair x \<and> (y1, y2) = Rep_stone_phi_pair y

goal (1 subgoal):
 1. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (stone_phi.pairs_sup (x1, x2) (y1, y2))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
by (simp add: sup_stone_phi_pair.rep_eq)
[PROOF STATE]
proof (state)
this:
triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (stone_phi.pairs_sup (x1, x2) (y1, y2))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
show "triple.pairs_sup (?q f x) (?q f y) = ?q f (x \<squnion> y)"
[PROOF STATE]
proof (prove)
using this:
stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))

goal (1 subgoal):
 1. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>f. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<squnion> y) = stone_phi_embed x \<squnion> stone_phi_embed y
[PROOF STEP]
have "stone_phi_embed x \<squnion> stone_phi_embed y = Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then Rep_stone_phi_pair x else ?q f x) \<squnion> Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then Rep_stone_phi_pair y else ?q f y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi_embed x \<squnion> stone_phi_embed y = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) \<squnion> Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stone_phi_embed x \<squnion> stone_phi_embed y = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) \<squnion> Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<squnion> y) = stone_phi_embed x \<squnion> stone_phi_embed y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
stone_phi_embed x \<squnion> stone_phi_embed y = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) \<squnion> Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<squnion> y) = stone_phi_embed x \<squnion> stone_phi_embed y
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . triple.pairs_sup (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else ?q f x) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else ?q f y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) \<squnion> Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = Abs_lifted_pair (\<lambda>f. stone_phi.pairs_sup (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))))
[PROOF STEP]
by (rule sup_lifted_pair.abs_eq) (simp_all add: eq_onp_same_args stone_phi_embed_triple_pair)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) \<squnion> Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = Abs_lifted_pair (\<lambda>f. stone_phi.pairs_sup (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<squnion> y) = stone_phi_embed x \<squnion> stone_phi_embed y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) \<squnion> Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = Abs_lifted_pair (\<lambda>f. stone_phi.pairs_sup (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<squnion> y) = stone_phi_embed x \<squnion> stone_phi_embed y
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then triple.pairs_sup (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else triple.pairs_sup (?q f x) (?q f y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. stone_phi.pairs_sup (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_sup (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))))
[PROOF STEP]
by (simp add: if_distrib_2)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. stone_phi.pairs_sup (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_sup (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<squnion> y) = stone_phi_embed x \<squnion> stone_phi_embed y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. stone_phi.pairs_sup (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_sup (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<squnion> y) = stone_phi_embed x \<squnion> stone_phi_embed y
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then triple.pairs_sup (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else ?q f (x \<squnion> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_sup (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_sup (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y))))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<forall>f. stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))

goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_sup (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_sup (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y))))
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_sup (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_sup (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y))))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<squnion> y) = stone_phi_embed x \<squnion> stone_phi_embed y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_sup (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else stone_phi.pairs_sup (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_sup (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y))))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<squnion> y) = stone_phi_embed x \<squnion> stone_phi_embed y
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then Rep_stone_phi_pair (x \<squnion> y) else ?q f (x \<squnion> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_sup (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair (x \<squnion> y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y))))
[PROOF STEP]
by (metis sup_stone_phi_pair.rep_eq)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_sup (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair (x \<squnion> y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y))))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<squnion> y) = stone_phi_embed x \<squnion> stone_phi_embed y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_sup (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair (x \<squnion> y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y))))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<squnion> y) = stone_phi_embed x \<squnion> stone_phi_embed y
[PROOF STEP]
have "... = stone_phi_embed (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair (x \<squnion> y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))) = stone_phi_embed (x \<squnion> y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair (x \<squnion> y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<squnion> y)))) = stone_phi_embed (x \<squnion> y)

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

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

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

goal (5 subgoals):
 1. inf_homomorphism stone_phi_embed
 2. top_homomorphism stone_phi_embed
 3. bot_homomorphism stone_phi_embed
 4. uminus_homomorphism stone_phi_embed
 5. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. inf_homomorphism stone_phi_embed
 2. top_homomorphism stone_phi_embed
 3. bot_homomorphism stone_phi_embed
 4. uminus_homomorphism stone_phi_embed
 5. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
let ?p = "\<lambda>f . triple.pairs_uminus (Rep_phi f)"
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. inf_homomorphism stone_phi_embed
 2. top_homomorphism stone_phi_embed
 3. bot_homomorphism stone_phi_embed
 4. uminus_homomorphism stone_phi_embed
 5. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
let ?pp = "\<lambda>f x . ?p f (?p f x)"
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. inf_homomorphism stone_phi_embed
 2. top_homomorphism stone_phi_embed
 3. bot_homomorphism stone_phi_embed
 4. uminus_homomorphism stone_phi_embed
 5. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
let ?q = "\<lambda>f x . ?pp f (Rep_stone_phi_pair x)"
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. inf_homomorphism stone_phi_embed
 2. top_homomorphism stone_phi_embed
 3. bot_homomorphism stone_phi_embed
 4. uminus_homomorphism stone_phi_embed
 5. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
show "\<forall>x y::'a stone_phi_pair . stone_phi_embed (x \<sqinter> y) = stone_phi_embed x \<sqinter> stone_phi_embed y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inf_homomorphism stone_phi_embed
[PROOF STEP]
proof (intro allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<sqinter> y) = stone_phi_embed x \<sqinter> stone_phi_embed y
[PROOF STEP]
fix x y :: "'a stone_phi_pair"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<sqinter> y) = stone_phi_embed x \<sqinter> stone_phi_embed y
[PROOF STEP]
have 1: "\<forall>f . triple.pairs_inf (?q f x) (?q f y) = ?q f (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
fix f :: "('a regular,'a dense) phi"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
let ?r = "Rep_phi f"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
obtain x1 x2 y1 y2 where 2: "(x1,x2) = Rep_stone_phi_pair x \<and> (y1,y2) = Rep_stone_phi_pair y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2 y1 y2. (x1, x2) = Rep_stone_phi_pair x \<and> (y1, y2) = Rep_stone_phi_pair y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

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

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
hence "triple.pairs_inf (?q f x) (?q f y) = triple.pairs_inf (?pp f (x1,x2)) (?pp f (y1,y2))"
[PROOF STATE]
proof (prove)
using this:
(x1, x2) = Rep_stone_phi_pair x \<and> (y1, y2) = Rep_stone_phi_pair y

goal (1 subgoal):
 1. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (y1, y2)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (y1, y2)))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (y1, y2)))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
have "... = triple.pairs_inf (--x1,?r (-x1)) (--y1,?r (-y1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (y1, y2))) = stone_phi.pairs_inf (- - x1, Rep_phi f (- x1)) (- - y1, Rep_phi f (- y1))
[PROOF STEP]
by (simp add: triple.pairs_uminus.simps triple_def)
[PROOF STATE]
proof (state)
this:
stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (y1, y2))) = stone_phi.pairs_inf (- - x1, Rep_phi f (- x1)) (- - y1, Rep_phi f (- y1))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (y1, y2))) = stone_phi.pairs_inf (- - x1, Rep_phi f (- x1)) (- - y1, Rep_phi f (- y1))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
have "... = (--x1 \<sqinter> --y1,?r (-x1) \<squnion> ?r (-y1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi.pairs_inf (- - x1, Rep_phi f (- x1)) (- - y1, Rep_phi f (- y1)) = (- - x1 \<sqinter> - - y1, Rep_phi f (- x1) \<squnion> Rep_phi f (- y1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stone_phi.pairs_inf (- - x1, Rep_phi f (- x1)) (- - y1, Rep_phi f (- y1)) = (- - x1 \<sqinter> - - y1, Rep_phi f (- x1) \<squnion> Rep_phi f (- y1))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
stone_phi.pairs_inf (- - x1, Rep_phi f (- x1)) (- - y1, Rep_phi f (- y1)) = (- - x1 \<sqinter> - - y1, Rep_phi f (- x1) \<squnion> Rep_phi f (- y1))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
have "... = (--(x1 \<sqinter> y1),?r (-(x1 \<sqinter> y1)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- - x1 \<sqinter> - - y1, Rep_phi f (- x1) \<squnion> Rep_phi f (- y1)) = (- - (x1 \<sqinter> y1), Rep_phi f (- (x1 \<sqinter> y1)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(- - x1 \<sqinter> - - y1, Rep_phi f (- x1) \<squnion> Rep_phi f (- y1)) = (- - (x1 \<sqinter> y1), Rep_phi f (- (x1 \<sqinter> y1)))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(- - x1 \<sqinter> - - y1, Rep_phi f (- x1) \<squnion> Rep_phi f (- y1)) = (- - (x1 \<sqinter> y1), Rep_phi f (- (x1 \<sqinter> y1)))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
have "... = ?pp f (x1 \<sqinter> y1,x2 \<squnion> y2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- - (x1 \<sqinter> y1), Rep_phi f (- (x1 \<sqinter> y1))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1 \<sqinter> y1, x2 \<squnion> y2))
[PROOF STEP]
by (simp add: triple.pairs_uminus.simps triple_def)
[PROOF STATE]
proof (state)
this:
(- - (x1 \<sqinter> y1), Rep_phi f (- (x1 \<sqinter> y1))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1 \<sqinter> y1, x2 \<squnion> y2))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(- - (x1 \<sqinter> y1), Rep_phi f (- (x1 \<sqinter> y1))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1 \<sqinter> y1, x2 \<squnion> y2))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
have "... = ?pp f (triple.pairs_inf (x1,x2) (y1,y2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1 \<sqinter> y1, x2 \<squnion> y2)) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (stone_phi.pairs_inf (x1, x2) (y1, y2)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1 \<sqinter> y1, x2 \<squnion> y2)) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (stone_phi.pairs_inf (x1, x2) (y1, y2)))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1 \<sqinter> y1, x2 \<squnion> y2)) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (stone_phi.pairs_inf (x1, x2) (y1, y2)))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
have "... = ?q f (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (stone_phi.pairs_inf (x1, x2) (y1, y2))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
(x1, x2) = Rep_stone_phi_pair x \<and> (y1, y2) = Rep_stone_phi_pair y

goal (1 subgoal):
 1. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (stone_phi.pairs_inf (x1, x2) (y1, y2))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
by (simp add: inf_stone_phi_pair.rep_eq)
[PROOF STATE]
proof (state)
this:
triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (stone_phi.pairs_inf (x1, x2) (y1, y2))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
show "triple.pairs_inf (?q f x) (?q f y) = ?q f (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
using this:
stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))

goal (1 subgoal):
 1. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>f. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<sqinter> y) = stone_phi_embed x \<sqinter> stone_phi_embed y
[PROOF STEP]
have "stone_phi_embed x \<sqinter> stone_phi_embed y = Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then Rep_stone_phi_pair x else ?q f x) \<sqinter> Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then Rep_stone_phi_pair y else ?q f y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi_embed x \<sqinter> stone_phi_embed y = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) \<sqinter> Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stone_phi_embed x \<sqinter> stone_phi_embed y = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) \<sqinter> Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<sqinter> y) = stone_phi_embed x \<sqinter> stone_phi_embed y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
stone_phi_embed x \<sqinter> stone_phi_embed y = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) \<sqinter> Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<sqinter> y) = stone_phi_embed x \<sqinter> stone_phi_embed y
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . triple.pairs_inf (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else ?q f x) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else ?q f y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) \<sqinter> Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = Abs_lifted_pair (\<lambda>f. stone_phi.pairs_inf (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))))
[PROOF STEP]
by (rule inf_lifted_pair.abs_eq) (simp_all add: eq_onp_same_args stone_phi_embed_triple_pair)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) \<sqinter> Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = Abs_lifted_pair (\<lambda>f. stone_phi.pairs_inf (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<sqinter> y) = stone_phi_embed x \<sqinter> stone_phi_embed y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) \<sqinter> Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = Abs_lifted_pair (\<lambda>f. stone_phi.pairs_inf (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<sqinter> y) = stone_phi_embed x \<sqinter> stone_phi_embed y
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then triple.pairs_inf (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else triple.pairs_inf (?q f x) (?q f y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. stone_phi.pairs_inf (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_inf (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))))
[PROOF STEP]
by (simp add: if_distrib_2)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. stone_phi.pairs_inf (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_inf (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<sqinter> y) = stone_phi_embed x \<sqinter> stone_phi_embed y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. stone_phi.pairs_inf (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_inf (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<sqinter> y) = stone_phi_embed x \<sqinter> stone_phi_embed y
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then triple.pairs_inf (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else ?q f (x \<sqinter> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_inf (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_inf (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y))))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<forall>f. stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))

goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_inf (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_inf (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y))))
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_inf (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_inf (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y))))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<sqinter> y) = stone_phi_embed x \<sqinter> stone_phi_embed y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_inf (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else stone_phi.pairs_inf (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_inf (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y))))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<sqinter> y) = stone_phi_embed x \<sqinter> stone_phi_embed y
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then Rep_stone_phi_pair (x \<sqinter> y) else ?q f (x \<sqinter> y))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_inf (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair (x \<sqinter> y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y))))
[PROOF STEP]
by (metis inf_stone_phi_pair.rep_eq)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_inf (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair (x \<sqinter> y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y))))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<sqinter> y) = stone_phi_embed x \<sqinter> stone_phi_embed y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then stone_phi.pairs_inf (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair (x \<sqinter> y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y))))

goal (1 subgoal):
 1. \<And>x y. stone_phi_embed (x \<sqinter> y) = stone_phi_embed x \<sqinter> stone_phi_embed y
[PROOF STEP]
have "... = stone_phi_embed (x \<sqinter> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair (x \<sqinter> y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))) = stone_phi_embed (x \<sqinter> y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair (x \<sqinter> y) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (x \<sqinter> y)))) = stone_phi_embed (x \<sqinter> y)

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

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

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

goal (4 subgoals):
 1. top_homomorphism stone_phi_embed
 2. bot_homomorphism stone_phi_embed
 3. uminus_homomorphism stone_phi_embed
 4. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. top_homomorphism stone_phi_embed
 2. bot_homomorphism stone_phi_embed
 3. uminus_homomorphism stone_phi_embed
 4. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
have "stone_phi_embed (top::'a stone_phi_pair) = Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then Rep_stone_phi_pair top else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair top)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi_embed top = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair top else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair top)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stone_phi_embed top = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair top else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair top)))

goal (4 subgoals):
 1. top_homomorphism stone_phi_embed
 2. bot_homomorphism stone_phi_embed
 3. uminus_homomorphism stone_phi_embed
 4. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
stone_phi_embed top = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair top else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair top)))

goal (4 subgoals):
 1. top_homomorphism stone_phi_embed
 2. bot_homomorphism stone_phi_embed
 3. uminus_homomorphism stone_phi_embed
 4. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then (top,bot) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (top,bot)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair top else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair top))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (top, bot) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (top, bot)))
[PROOF STEP]
by (metis (no_types, opaque_lifting) bot_filter.abs_eq top_stone_phi_pair.rep_eq)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair top else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair top))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (top, bot) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (top, bot)))

goal (4 subgoals):
 1. top_homomorphism stone_phi_embed
 2. bot_homomorphism stone_phi_embed
 3. uminus_homomorphism stone_phi_embed
 4. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair top else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair top))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (top, bot) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (top, bot)))

goal (4 subgoals):
 1. top_homomorphism stone_phi_embed
 2. bot_homomorphism stone_phi_embed
 3. uminus_homomorphism stone_phi_embed
 4. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then (top,bot) else triple.pairs_uminus (Rep_phi f) (bot,top))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (top, bot) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (top, bot))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (top, bot) else triple.pairs_uminus (Rep_phi f) (bot, top))
[PROOF STEP]
by (metis (no_types, opaque_lifting) dense_closed_top simp_phi triple.pairs_uminus.simps triple_def)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (top, bot) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (top, bot))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (top, bot) else triple.pairs_uminus (Rep_phi f) (bot, top))

goal (4 subgoals):
 1. top_homomorphism stone_phi_embed
 2. bot_homomorphism stone_phi_embed
 3. uminus_homomorphism stone_phi_embed
 4. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (top, bot) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (top, bot))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (top, bot) else triple.pairs_uminus (Rep_phi f) (bot, top))

goal (4 subgoals):
 1. top_homomorphism stone_phi_embed
 2. bot_homomorphism stone_phi_embed
 3. uminus_homomorphism stone_phi_embed
 4. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then (top,bot) else (top,bot))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (top, bot) else triple.pairs_uminus (Rep_phi f) (bot, top)) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (top, bot) else (top, bot))
[PROOF STEP]
by (metis (no_types, opaque_lifting) p_bot simp_phi triple.pairs_uminus.simps triple_def)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (top, bot) else triple.pairs_uminus (Rep_phi f) (bot, top)) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (top, bot) else (top, bot))

goal (4 subgoals):
 1. top_homomorphism stone_phi_embed
 2. bot_homomorphism stone_phi_embed
 3. uminus_homomorphism stone_phi_embed
 4. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (top, bot) else triple.pairs_uminus (Rep_phi f) (bot, top)) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (top, bot) else (top, bot))

goal (4 subgoals):
 1. top_homomorphism stone_phi_embed
 2. bot_homomorphism stone_phi_embed
 3. uminus_homomorphism stone_phi_embed
 4. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . (top,Abs_filter {top}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (top, bot) else (top, bot)) = Abs_lifted_pair (\<lambda>f. stone_phi.pairs_top)
[PROOF STEP]
by (simp add: bot_filter.abs_eq)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (top, bot) else (top, bot)) = Abs_lifted_pair (\<lambda>f. stone_phi.pairs_top)

goal (4 subgoals):
 1. top_homomorphism stone_phi_embed
 2. bot_homomorphism stone_phi_embed
 3. uminus_homomorphism stone_phi_embed
 4. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (top, bot) else (top, bot)) = Abs_lifted_pair (\<lambda>f. stone_phi.pairs_top)

goal (4 subgoals):
 1. top_homomorphism stone_phi_embed
 2. bot_homomorphism stone_phi_embed
 3. uminus_homomorphism stone_phi_embed
 4. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
have "... = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. stone_phi.pairs_top) = top
[PROOF STEP]
by (rule top_lifted_pair.abs_eq[THEN sym])
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. stone_phi.pairs_top) = top

goal (4 subgoals):
 1. top_homomorphism stone_phi_embed
 2. bot_homomorphism stone_phi_embed
 3. uminus_homomorphism stone_phi_embed
 4. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
top_homomorphism stone_phi_embed
[PROOF STEP]
show "stone_phi_embed (top::'a stone_phi_pair) = top"
[PROOF STATE]
proof (prove)
using this:
top_homomorphism stone_phi_embed

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

goal (3 subgoals):
 1. bot_homomorphism stone_phi_embed
 2. uminus_homomorphism stone_phi_embed
 3. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. bot_homomorphism stone_phi_embed
 2. uminus_homomorphism stone_phi_embed
 3. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
have "stone_phi_embed (bot::'a stone_phi_pair) = Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then Rep_stone_phi_pair bot else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair bot)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stone_phi_embed bot = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair bot else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair bot)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stone_phi_embed bot = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair bot else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair bot)))

goal (3 subgoals):
 1. bot_homomorphism stone_phi_embed
 2. uminus_homomorphism stone_phi_embed
 3. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
stone_phi_embed bot = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair bot else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair bot)))

goal (3 subgoals):
 1. bot_homomorphism stone_phi_embed
 2. uminus_homomorphism stone_phi_embed
 3. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then (bot,top) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (bot,top)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair bot else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair bot))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (bot, top) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (bot, top)))
[PROOF STEP]
by (metis (no_types, opaque_lifting) top_filter.abs_eq bot_stone_phi_pair.rep_eq)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair bot else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair bot))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (bot, top) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (bot, top)))

goal (3 subgoals):
 1. bot_homomorphism stone_phi_embed
 2. uminus_homomorphism stone_phi_embed
 3. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair bot else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair bot))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (bot, top) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (bot, top)))

goal (3 subgoals):
 1. bot_homomorphism stone_phi_embed
 2. uminus_homomorphism stone_phi_embed
 3. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then (bot,top) else triple.pairs_uminus (Rep_phi f) (top,bot))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (bot, top) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (bot, top))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (bot, top) else triple.pairs_uminus (Rep_phi f) (top, bot))
[PROOF STEP]
by (metis (no_types, opaque_lifting) p_bot simp_phi triple.pairs_uminus.simps triple_def)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (bot, top) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (bot, top))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (bot, top) else triple.pairs_uminus (Rep_phi f) (top, bot))

goal (3 subgoals):
 1. bot_homomorphism stone_phi_embed
 2. uminus_homomorphism stone_phi_embed
 3. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (bot, top) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (bot, top))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (bot, top) else triple.pairs_uminus (Rep_phi f) (top, bot))

goal (3 subgoals):
 1. bot_homomorphism stone_phi_embed
 2. uminus_homomorphism stone_phi_embed
 3. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then (bot,top) else (bot,top))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (bot, top) else triple.pairs_uminus (Rep_phi f) (top, bot)) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (bot, top) else (bot, top))
[PROOF STEP]
by (metis (no_types, opaque_lifting) p_top simp_phi triple.pairs_uminus.simps triple_def)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (bot, top) else triple.pairs_uminus (Rep_phi f) (top, bot)) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (bot, top) else (bot, top))

goal (3 subgoals):
 1. bot_homomorphism stone_phi_embed
 2. uminus_homomorphism stone_phi_embed
 3. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (bot, top) else triple.pairs_uminus (Rep_phi f) (top, bot)) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (bot, top) else (bot, top))

goal (3 subgoals):
 1. bot_homomorphism stone_phi_embed
 2. uminus_homomorphism stone_phi_embed
 3. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . (bot,Abs_filter UNIV))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (bot, top) else (bot, top)) = Abs_lifted_pair (\<lambda>f. stone_phi.pairs_bot)
[PROOF STEP]
by (simp add: top_filter.abs_eq)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (bot, top) else (bot, top)) = Abs_lifted_pair (\<lambda>f. stone_phi.pairs_bot)

goal (3 subgoals):
 1. bot_homomorphism stone_phi_embed
 2. uminus_homomorphism stone_phi_embed
 3. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then (bot, top) else (bot, top)) = Abs_lifted_pair (\<lambda>f. stone_phi.pairs_bot)

goal (3 subgoals):
 1. bot_homomorphism stone_phi_embed
 2. uminus_homomorphism stone_phi_embed
 3. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
have "... = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. stone_phi.pairs_bot) = bot
[PROOF STEP]
by (rule bot_lifted_pair.abs_eq[THEN sym])
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. stone_phi.pairs_bot) = bot

goal (3 subgoals):
 1. bot_homomorphism stone_phi_embed
 2. uminus_homomorphism stone_phi_embed
 3. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
bot_homomorphism stone_phi_embed
[PROOF STEP]
show "stone_phi_embed (bot::'a stone_phi_pair) = bot"
[PROOF STATE]
proof (prove)
using this:
bot_homomorphism stone_phi_embed

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

goal (2 subgoals):
 1. uminus_homomorphism stone_phi_embed
 2. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. uminus_homomorphism stone_phi_embed
 2. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
let ?p = "\<lambda>f . triple.pairs_uminus (Rep_phi f)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. uminus_homomorphism stone_phi_embed
 2. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
let ?pp = "\<lambda>f x . ?p f (?p f x)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. uminus_homomorphism stone_phi_embed
 2. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
let ?q = "\<lambda>f x . ?pp f (Rep_stone_phi_pair x)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. uminus_homomorphism stone_phi_embed
 2. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
show "\<forall>x::'a stone_phi_pair . stone_phi_embed (-x) = -stone_phi_embed x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uminus_homomorphism stone_phi_embed
[PROOF STEP]
proof (intro allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. stone_phi_embed (- x) = - stone_phi_embed x
[PROOF STEP]
fix x :: "'a stone_phi_pair"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. stone_phi_embed (- x) = - stone_phi_embed x
[PROOF STEP]
have 1: "\<forall>f . triple.pairs_uminus (Rep_phi f) (?q f x) = ?q f (-x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))
[PROOF STEP]
fix f :: "('a regular,'a dense) phi"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))
[PROOF STEP]
let ?r = "Rep_phi f"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))
[PROOF STEP]
obtain x1 x2 where 2: "(x1,x2) = Rep_stone_phi_pair x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2. (x1, x2) = Rep_stone_phi_pair x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

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

goal (1 subgoal):
 1. \<And>f. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))
[PROOF STEP]
hence "triple.pairs_uminus (Rep_phi f) (?q f x) = triple.pairs_uminus (Rep_phi f) (?pp f (x1,x2))"
[PROOF STATE]
proof (prove)
using this:
(x1, x2) = Rep_stone_phi_pair x

goal (1 subgoal):
 1. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2)))

goal (1 subgoal):
 1. \<And>f. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2)))

goal (1 subgoal):
 1. \<And>f. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))
[PROOF STEP]
have "... = triple.pairs_uminus (Rep_phi f) (--x1,?r (-x1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2))) = triple.pairs_uminus (Rep_phi f) (- - x1, Rep_phi f (- x1))
[PROOF STEP]
by (simp add: triple.pairs_uminus.simps triple_def)
[PROOF STATE]
proof (state)
this:
triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2))) = triple.pairs_uminus (Rep_phi f) (- - x1, Rep_phi f (- x1))

goal (1 subgoal):
 1. \<And>f. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2))) = triple.pairs_uminus (Rep_phi f) (- - x1, Rep_phi f (- x1))

goal (1 subgoal):
 1. \<And>f. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))
[PROOF STEP]
have "... = (---x1,?r (--x1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple.pairs_uminus (Rep_phi f) (- - x1, Rep_phi f (- x1)) = (- - - x1, Rep_phi f (- - x1))
[PROOF STEP]
by (simp add: triple.pairs_uminus.simps triple_def)
[PROOF STATE]
proof (state)
this:
triple.pairs_uminus (Rep_phi f) (- - x1, Rep_phi f (- x1)) = (- - - x1, Rep_phi f (- - x1))

goal (1 subgoal):
 1. \<And>f. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
triple.pairs_uminus (Rep_phi f) (- - x1, Rep_phi f (- x1)) = (- - - x1, Rep_phi f (- - x1))

goal (1 subgoal):
 1. \<And>f. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))
[PROOF STEP]
have "... = ?pp f (-x1,stone_phi x1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (- - - x1, Rep_phi f (- - x1)) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (- x1, stone_phi x1))
[PROOF STEP]
by (simp add: triple.pairs_uminus.simps triple_def)
[PROOF STATE]
proof (state)
this:
(- - - x1, Rep_phi f (- - x1)) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (- x1, stone_phi x1))

goal (1 subgoal):
 1. \<And>f. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(- - - x1, Rep_phi f (- - x1)) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (- x1, stone_phi x1))

goal (1 subgoal):
 1. \<And>f. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))
[PROOF STEP]
have "... = ?pp f (triple.pairs_uminus stone_phi (x1,x2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (- x1, stone_phi x1)) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (stone_phi.pairs_uminus (x1, x2)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (- x1, stone_phi x1)) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (stone_phi.pairs_uminus (x1, x2)))

goal (1 subgoal):
 1. \<And>f. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (- x1, stone_phi x1)) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (stone_phi.pairs_uminus (x1, x2)))

goal (1 subgoal):
 1. \<And>f. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))
[PROOF STEP]
have "... = ?q f (-x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (stone_phi.pairs_uminus (x1, x2))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
(x1, x2) = Rep_stone_phi_pair x

goal (1 subgoal):
 1. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (stone_phi.pairs_uminus (x1, x2))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))
[PROOF STEP]
by (simp add: uminus_stone_phi_pair.rep_eq)
[PROOF STATE]
proof (state)
this:
triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (stone_phi.pairs_uminus (x1, x2))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))

goal (1 subgoal):
 1. \<And>f. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))
[PROOF STEP]
show "triple.pairs_uminus (Rep_phi f) (?q f x) = ?q f (-x)"
[PROOF STATE]
proof (prove)
using this:
triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))

goal (1 subgoal):
 1. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>f. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))

goal (1 subgoal):
 1. \<And>x. stone_phi_embed (- x) = - stone_phi_embed x
[PROOF STEP]
have "-stone_phi_embed x = -Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then Rep_stone_phi_pair x else ?q f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - stone_phi_embed x = - Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
- stone_phi_embed x = - Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x)))

goal (1 subgoal):
 1. \<And>x. stone_phi_embed (- x) = - stone_phi_embed x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- stone_phi_embed x = - Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x)))

goal (1 subgoal):
 1. \<And>x. stone_phi_embed (- x) = - stone_phi_embed x
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . triple.pairs_uminus (Rep_phi f) (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else ?q f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))))
[PROOF STEP]
by (rule uminus_lifted_pair.abs_eq) (simp_all add: eq_onp_same_args stone_phi_embed_triple_pair)
[PROOF STATE]
proof (state)
this:
- Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))))

goal (1 subgoal):
 1. \<And>x. stone_phi_embed (- x) = - stone_phi_embed x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))))

goal (1 subgoal):
 1. \<And>x. stone_phi_embed (- x) = - stone_phi_embed x
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x) else triple.pairs_uminus (Rep_phi f) (?q f x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))))
[PROOF STEP]
by (simp add: if_distrib)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))))

goal (1 subgoal):
 1. \<And>x. stone_phi_embed (- x) = - stone_phi_embed x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))))

goal (1 subgoal):
 1. \<And>x. stone_phi_embed (- x) = - stone_phi_embed x
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x) else ?q f (-x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x))))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<forall>f. triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))

goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x))))
[PROOF STEP]
by meson
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x))))

goal (1 subgoal):
 1. \<And>x. stone_phi_embed (- x) = - stone_phi_embed x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x))))

goal (1 subgoal):
 1. \<And>x. stone_phi_embed (- x) = - stone_phi_embed x
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then Rep_stone_phi_pair (-x) else ?q f (-x))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair (- x) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x))))
[PROOF STEP]
by (metis uminus_stone_phi_pair.rep_eq)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair (- x) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x))))

goal (1 subgoal):
 1. \<And>x. stone_phi_embed (- x) = - stone_phi_embed x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))) = Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair (- x) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x))))

goal (1 subgoal):
 1. \<And>x. stone_phi_embed (- x) = - stone_phi_embed x
[PROOF STEP]
have "... = stone_phi_embed (-x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair (- x) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))) = stone_phi_embed (- x)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair (- x) else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair (- x)))) = stone_phi_embed (- x)

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

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

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

goal (1 subgoal):
 1. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
let ?p = "\<lambda>f . triple.pairs_uminus (Rep_phi f)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
let ?pp = "\<lambda>f x . ?p f (?p f x)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
let ?q = "\<lambda>f x . ?pp f (Rep_stone_phi_pair x)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
show "\<forall>x y::'a stone_phi_pair . x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
proof (intro allI, rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
fix x y :: "'a stone_phi_pair"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
assume 1: "x \<le> y"
[PROOF STATE]
proof (state)
this:
x \<le> y

goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
have "\<forall>f . triple.pairs_less_eq (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else ?q f x) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else ?q f y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f. stone_phi.pairs_less_eq (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_less_eq (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))
[PROOF STEP]
fix f :: "('a regular,'a dense) phi"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_less_eq (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))
[PROOF STEP]
let ?r = "Rep_phi f"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_less_eq (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))
[PROOF STEP]
obtain x1 x2 y1 y2 where 2: "(x1,x2) = Rep_stone_phi_pair x \<and> (y1,y2) = Rep_stone_phi_pair y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x1 x2 y1 y2. (x1, x2) = Rep_stone_phi_pair x \<and> (y1, y2) = Rep_stone_phi_pair y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

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

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_less_eq (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))
[PROOF STEP]
have "x1 \<le> y1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x1 \<le> y1
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
x \<le> y
(x1, x2) = Rep_stone_phi_pair x \<and> (y1, y2) = Rep_stone_phi_pair y

goal (1 subgoal):
 1. x1 \<le> y1
[PROOF STEP]
by (metis less_eq_stone_phi_pair.rep_eq stone_phi.pairs_less_eq.simps)
[PROOF STATE]
proof (state)
this:
x1 \<le> y1

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_less_eq (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))
[PROOF STEP]
hence "--x1 \<le> --y1 \<and> ?r (-y1) \<le> ?r (-x1)"
[PROOF STATE]
proof (prove)
using this:
x1 \<le> y1

goal (1 subgoal):
 1. - - x1 \<le> - - y1 \<and> Rep_phi f (- y1) \<le> Rep_phi f (- x1)
[PROOF STEP]
by (metis compl_le_compl_iff le_iff_sup simp_phi)
[PROOF STATE]
proof (state)
this:
- - x1 \<le> - - y1 \<and> Rep_phi f (- y1) \<le> Rep_phi f (- x1)

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_less_eq (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))
[PROOF STEP]
hence "triple.pairs_less_eq (--x1,?r (-x1)) (--y1,?r (-y1))"
[PROOF STATE]
proof (prove)
using this:
- - x1 \<le> - - y1 \<and> Rep_phi f (- y1) \<le> Rep_phi f (- x1)

goal (1 subgoal):
 1. stone_phi.pairs_less_eq (- - x1, Rep_phi f (- x1)) (- - y1, Rep_phi f (- y1))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
stone_phi.pairs_less_eq (- - x1, Rep_phi f (- x1)) (- - y1, Rep_phi f (- y1))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_less_eq (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))
[PROOF STEP]
hence "triple.pairs_less_eq (?pp f (x1,x2)) (?pp f (y1,y2))"
[PROOF STATE]
proof (prove)
using this:
stone_phi.pairs_less_eq (- - x1, Rep_phi f (- x1)) (- - y1, Rep_phi f (- y1))

goal (1 subgoal):
 1. stone_phi.pairs_less_eq (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (y1, y2)))
[PROOF STEP]
by (simp add: triple.pairs_uminus.simps triple_def)
[PROOF STATE]
proof (state)
this:
stone_phi.pairs_less_eq (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (y1, y2)))

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_less_eq (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))
[PROOF STEP]
hence "triple.pairs_less_eq (?q f x) (?q f y)"
[PROOF STATE]
proof (prove)
using this:
stone_phi.pairs_less_eq (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (y1, y2)))

goal (1 subgoal):
 1. stone_phi.pairs_less_eq (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
stone_phi.pairs_less_eq (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (x1, x2))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (y1, y2)))
(x1, x2) = Rep_stone_phi_pair x \<and> (y1, y2) = Rep_stone_phi_pair y

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

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

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

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

goal (1 subgoal):
 1. \<And>f. stone_phi.pairs_less_eq (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))
[PROOF STEP]
thus "triple.pairs_less_eq (if ?r = stone_phi then Rep_stone_phi_pair x else ?q f x) (if ?r = stone_phi then Rep_stone_phi_pair y else ?q f y)"
[PROOF STATE]
proof (prove)
using this:
if Rep_phi f = stone_phi then stone_phi.pairs_less_eq (Rep_stone_phi_pair x) (Rep_stone_phi_pair y) else stone_phi.pairs_less_eq (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>f. stone_phi.pairs_less_eq (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))

goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
hence "Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then Rep_stone_phi_pair x else ?q f x) \<le> Abs_lifted_pair (\<lambda>f . if Rep_phi f = stone_phi then Rep_stone_phi_pair y else ?q f y)"
[PROOF STATE]
proof (prove)
using this:
\<forall>f. stone_phi.pairs_less_eq (if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) (if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))

goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) \<le> Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))
[PROOF STEP]
by (subst less_eq_lifted_pair.abs_eq) (simp_all add: eq_onp_same_args stone_phi_embed_triple_pair)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) \<le> Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))

goal (1 subgoal):
 1. \<And>x y. x \<le> y \<Longrightarrow> stone_phi_embed x \<le> stone_phi_embed y
[PROOF STEP]
thus "stone_phi_embed x \<le> stone_phi_embed y"
[PROOF STATE]
proof (prove)
using this:
Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair x else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair x))) \<le> Abs_lifted_pair (\<lambda>f. if Rep_phi f = stone_phi then Rep_stone_phi_pair y else triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_stone_phi_pair y)))

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>x y. x \<le> y \<longrightarrow> stone_phi_embed x \<le> stone_phi_embed y

goal:
No subgoals!
[PROOF STEP]
qed