[STATEMENT]
lemma ba_iso_inv_lifted_pair:
  "(Rep_lifted_boolean_algebra xf f,Rep_phi f (-Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f)
[PROOF STEP]
by (metis (no_types, opaque_lifting) double_compl simp_phi triple.pairs_uminus.simps triple_def triple.pairs_uminus_closed)


[STATEMENT]
lemma ba_iso_inv_regular:
  "regular (Abs_lifted_pair (\<lambda>f . (Rep_lifted_boolean_algebra xf f,Rep_phi f (-Rep_lifted_boolean_algebra xf f))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))
[PROOF STEP]
have "\<forall>f . (Rep_lifted_boolean_algebra xf f,Rep_phi f (-Rep_lifted_boolean_algebra xf f)) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_lifted_boolean_algebra xf f,Rep_phi f (-Rep_lifted_boolean_algebra xf f)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)))
[PROOF STEP]
by (simp add: triple.pairs_uminus.simps triple_def)
[PROOF STATE]
proof (state)
this:
\<forall>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)))

goal (1 subgoal):
 1. regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))
[PROOF STEP]
hence "Abs_lifted_pair (\<lambda>f . (Rep_lifted_boolean_algebra xf f,Rep_phi f (-Rep_lifted_boolean_algebra xf f))) = --Abs_lifted_pair (\<lambda>f . (Rep_lifted_boolean_algebra xf f,Rep_phi f (-Rep_lifted_boolean_algebra xf f)))"
[PROOF STATE]
proof (prove)
using this:
\<forall>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)) = triple.pairs_uminus (Rep_phi f) (triple.pairs_uminus (Rep_phi f) (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)))

goal (1 subgoal):
 1. regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))
[PROOF STEP]
by (simp add: triple.pairs_uminus_closed triple_def eq_onp_def uminus_lifted_pair.abs_eq ba_iso_inv_lifted_pair)
[PROOF STATE]
proof (state)
this:
regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))

goal (1 subgoal):
 1. regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))

goal (1 subgoal):
 1. regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ba_iso_left_invertible:
  "ba_iso_inv (ba_iso pf) = pf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ba_iso_inv (ba_iso pf) = pf
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ba_iso_inv (ba_iso pf) = pf
[PROOF STEP]
have 1: "\<forall>f . snd (Rep_lifted_pair (Rep_regular pf) f) = Rep_phi f (-fst (Rep_lifted_pair (Rep_regular pf) f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f. snd (Rep_lifted_pair (Rep_regular pf) f) = Rep_phi f (- fst (Rep_lifted_pair (Rep_regular pf) f))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. snd (Rep_lifted_pair (Rep_regular pf) f) = Rep_phi f (- fst (Rep_lifted_pair (Rep_regular pf) f))
[PROOF STEP]
fix f :: "('a,'b) phi"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. snd (Rep_lifted_pair (Rep_regular pf) f) = Rep_phi f (- fst (Rep_lifted_pair (Rep_regular pf) f))
[PROOF STEP]
let ?r = "Rep_phi f"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. snd (Rep_lifted_pair (Rep_regular pf) f) = Rep_phi f (- fst (Rep_lifted_pair (Rep_regular pf) f))
[PROOF STEP]
have "triple ?r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple (Rep_phi f)
[PROOF STEP]
by (simp add: triple_def)
[PROOF STATE]
proof (state)
this:
triple (Rep_phi f)

goal (1 subgoal):
 1. \<And>f. snd (Rep_lifted_pair (Rep_regular pf) f) = Rep_phi f (- fst (Rep_lifted_pair (Rep_regular pf) f))
[PROOF STEP]
hence 2: "\<forall>p . triple.pairs_uminus ?r p = (-fst p,?r (fst p))"
[PROOF STATE]
proof (prove)
using this:
triple (Rep_phi f)

goal (1 subgoal):
 1. \<forall>p. triple.pairs_uminus (Rep_phi f) p = (- fst p, Rep_phi f (fst p))
[PROOF STEP]
by (metis prod.collapse triple.pairs_uminus.simps)
[PROOF STATE]
proof (state)
this:
\<forall>p. triple.pairs_uminus (Rep_phi f) p = (- fst p, Rep_phi f (fst p))

goal (1 subgoal):
 1. \<And>f. snd (Rep_lifted_pair (Rep_regular pf) f) = Rep_phi f (- fst (Rep_lifted_pair (Rep_regular pf) f))
[PROOF STEP]
have 3: "Rep_regular pf = --Rep_regular pf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. regular (Rep_regular pf)
[PROOF STEP]
by (simp add: regular_in_p_image_iff)
[PROOF STATE]
proof (state)
this:
regular (Rep_regular pf)

goal (1 subgoal):
 1. \<And>f. snd (Rep_lifted_pair (Rep_regular pf) f) = Rep_phi f (- fst (Rep_lifted_pair (Rep_regular pf) f))
[PROOF STEP]
show "snd (Rep_lifted_pair (Rep_regular pf) f) = ?r (-fst (Rep_lifted_pair (Rep_regular pf) f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (Rep_lifted_pair (Rep_regular pf) f) = Rep_phi f (- fst (Rep_lifted_pair (Rep_regular pf) f))
[PROOF STEP]
using 2 3
[PROOF STATE]
proof (prove)
using this:
\<forall>p. triple.pairs_uminus (Rep_phi f) p = (- fst p, Rep_phi f (fst p))
regular (Rep_regular pf)

goal (1 subgoal):
 1. snd (Rep_lifted_pair (Rep_regular pf) f) = Rep_phi f (- fst (Rep_lifted_pair (Rep_regular pf) f))
[PROOF STEP]
by (metis fstI sndI uminus_lifted_pair.rep_eq)
[PROOF STATE]
proof (state)
this:
snd (Rep_lifted_pair (Rep_regular pf) f) = Rep_phi f (- fst (Rep_lifted_pair (Rep_regular pf) f))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>f. snd (Rep_lifted_pair (Rep_regular pf) f) = Rep_phi f (- fst (Rep_lifted_pair (Rep_regular pf) f))

goal (1 subgoal):
 1. ba_iso_inv (ba_iso pf) = pf
[PROOF STEP]
have "ba_iso_inv (ba_iso pf) = Abs_regular (Abs_lifted_pair (\<lambda>f . (fst (Rep_lifted_pair (Rep_regular pf) f),Rep_phi f (-fst (Rep_lifted_pair (Rep_regular pf) f)))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ba_iso_inv (ba_iso pf) = Abs_regular (Abs_lifted_pair (\<lambda>f. (fst (Rep_lifted_pair (Rep_regular pf) f), Rep_phi f (- fst (Rep_lifted_pair (Rep_regular pf) f)))))
[PROOF STEP]
by (simp add: Abs_lifted_boolean_algebra_inverse)
[PROOF STATE]
proof (state)
this:
ba_iso_inv (ba_iso pf) = Abs_regular (Abs_lifted_pair (\<lambda>f. (fst (Rep_lifted_pair (Rep_regular pf) f), Rep_phi f (- fst (Rep_lifted_pair (Rep_regular pf) f)))))

goal (1 subgoal):
 1. ba_iso_inv (ba_iso pf) = pf
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
ba_iso_inv (ba_iso pf) = Abs_regular (Abs_lifted_pair (\<lambda>f. (fst (Rep_lifted_pair (Rep_regular pf) f), Rep_phi f (- fst (Rep_lifted_pair (Rep_regular pf) f)))))

goal (1 subgoal):
 1. ba_iso_inv (ba_iso pf) = pf
[PROOF STEP]
have "... = Abs_regular (Abs_lifted_pair (Rep_lifted_pair (Rep_regular pf)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_regular (Abs_lifted_pair (\<lambda>f. (fst (Rep_lifted_pair (Rep_regular pf) f), Rep_phi f (- fst (Rep_lifted_pair (Rep_regular pf) f))))) = Abs_regular (Abs_lifted_pair (Rep_lifted_pair (Rep_regular pf)))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<forall>f. snd (Rep_lifted_pair (Rep_regular pf) f) = Rep_phi f (- fst (Rep_lifted_pair (Rep_regular pf) f))

goal (1 subgoal):
 1. Abs_regular (Abs_lifted_pair (\<lambda>f. (fst (Rep_lifted_pair (Rep_regular pf) f), Rep_phi f (- fst (Rep_lifted_pair (Rep_regular pf) f))))) = Abs_regular (Abs_lifted_pair (Rep_lifted_pair (Rep_regular pf)))
[PROOF STEP]
by (metis prod.collapse)
[PROOF STATE]
proof (state)
this:
Abs_regular (Abs_lifted_pair (\<lambda>f. (fst (Rep_lifted_pair (Rep_regular pf) f), Rep_phi f (- fst (Rep_lifted_pair (Rep_regular pf) f))))) = Abs_regular (Abs_lifted_pair (Rep_lifted_pair (Rep_regular pf)))

goal (1 subgoal):
 1. ba_iso_inv (ba_iso pf) = pf
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_regular (Abs_lifted_pair (\<lambda>f. (fst (Rep_lifted_pair (Rep_regular pf) f), Rep_phi f (- fst (Rep_lifted_pair (Rep_regular pf) f))))) = Abs_regular (Abs_lifted_pair (Rep_lifted_pair (Rep_regular pf)))

goal (1 subgoal):
 1. ba_iso_inv (ba_iso pf) = pf
[PROOF STEP]
have "... = pf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_regular (Abs_lifted_pair (Rep_lifted_pair (Rep_regular pf))) = pf
[PROOF STEP]
by (simp add: Rep_regular_inverse Rep_lifted_pair_inverse)
[PROOF STATE]
proof (state)
this:
Abs_regular (Abs_lifted_pair (Rep_lifted_pair (Rep_regular pf))) = pf

goal (1 subgoal):
 1. ba_iso_inv (ba_iso pf) = pf
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
ba_iso_inv (ba_iso pf) = pf
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ba_iso_inv (ba_iso pf) = pf

goal (1 subgoal):
 1. ba_iso_inv (ba_iso pf) = pf
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ba_iso_inv (ba_iso pf) = pf

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ba_iso_right_invertible:
  "ba_iso (ba_iso_inv xf) = xf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ba_iso (ba_iso_inv xf) = xf
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ba_iso (ba_iso_inv xf) = xf
[PROOF STEP]
let ?rf = "Rep_lifted_boolean_algebra xf"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ba_iso (ba_iso_inv xf) = xf
[PROOF STEP]
have 1: "\<forall>f . (-?rf f,Rep_phi f (?rf f)) \<in> triple.pairs (Rep_phi f) \<and> (?rf f,Rep_phi f (-?rf f)) \<in> triple.pairs (Rep_phi f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f. (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f) \<and> (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f) \<and> (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f)
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f) \<and> (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f)
[PROOF STEP]
have "up_filter top = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. up_filter top = bot
[PROOF STEP]
by (simp add: bot_filter.abs_eq)
[PROOF STATE]
proof (state)
this:
up_filter top = bot

goal (1 subgoal):
 1. \<And>f. (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f) \<and> (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f)
[PROOF STEP]
hence "(\<exists>z . Rep_phi f (?rf f) = Rep_phi f (?rf f) \<squnion> up_filter z) \<and> (\<exists>z . Rep_phi f (-?rf f) = Rep_phi f (-?rf f) \<squnion> up_filter z)"
[PROOF STATE]
proof (prove)
using this:
up_filter top = bot

goal (1 subgoal):
 1. (\<exists>z. Rep_phi f (Rep_lifted_boolean_algebra xf f) = Rep_phi f (Rep_lifted_boolean_algebra xf f) \<squnion> up_filter z) \<and> (\<exists>z. Rep_phi f (- Rep_lifted_boolean_algebra xf f) = Rep_phi f (- Rep_lifted_boolean_algebra xf f) \<squnion> up_filter z)
[PROOF STEP]
by (metis sup_bot_right)
[PROOF STATE]
proof (state)
this:
(\<exists>z. Rep_phi f (Rep_lifted_boolean_algebra xf f) = Rep_phi f (Rep_lifted_boolean_algebra xf f) \<squnion> up_filter z) \<and> (\<exists>z. Rep_phi f (- Rep_lifted_boolean_algebra xf f) = Rep_phi f (- Rep_lifted_boolean_algebra xf f) \<squnion> up_filter z)

goal (1 subgoal):
 1. \<And>f. (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f) \<and> (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f)
[PROOF STEP]
thus "(-?rf f,Rep_phi f (?rf f)) \<in> triple.pairs (Rep_phi f) \<and> (?rf f,Rep_phi f (-?rf f)) \<in> triple.pairs (Rep_phi f)"
[PROOF STATE]
proof (prove)
using this:
(\<exists>z. Rep_phi f (Rep_lifted_boolean_algebra xf f) = Rep_phi f (Rep_lifted_boolean_algebra xf f) \<squnion> up_filter z) \<and> (\<exists>z. Rep_phi f (- Rep_lifted_boolean_algebra xf f) = Rep_phi f (- Rep_lifted_boolean_algebra xf f) \<squnion> up_filter z)

goal (1 subgoal):
 1. (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f) \<and> (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f)
[PROOF STEP]
by (simp add: triple_def triple.pairs_def)
[PROOF STATE]
proof (state)
this:
(- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f) \<and> (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>f. (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f) \<and> (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f)

goal (1 subgoal):
 1. ba_iso (ba_iso_inv xf) = xf
[PROOF STEP]
have "regular (Abs_lifted_pair (\<lambda>f . (?rf f,Rep_phi f (-?rf f))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))
[PROOF STEP]
have "--Abs_lifted_pair (\<lambda>f . (?rf f,Rep_phi f (-?rf f))) = -Abs_lifted_pair (\<lambda>f . triple.pairs_uminus (Rep_phi f) (?rf f,Rep_phi f (-?rf f)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - - Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))) = - Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<forall>f. (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f) \<and> (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f)

goal (1 subgoal):
 1. - - Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))) = - Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)))
[PROOF STEP]
by (simp add: eq_onp_same_args uminus_lifted_pair.abs_eq)
[PROOF STATE]
proof (state)
this:
- - Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))) = - Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)))

goal (1 subgoal):
 1. regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- - Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))) = - Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)))

goal (1 subgoal):
 1. regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))
[PROOF STEP]
have "... = -Abs_lifted_pair (\<lambda>f . (-?rf f,Rep_phi f (?rf f)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))) = - Abs_lifted_pair (\<lambda>f. (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f)))
[PROOF STEP]
by (metis (no_types, lifting) simp_phi triple_def triple.pairs_uminus.simps)
[PROOF STATE]
proof (state)
this:
- Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))) = - Abs_lifted_pair (\<lambda>f. (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f)))

goal (1 subgoal):
 1. regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))) = - Abs_lifted_pair (\<lambda>f. (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f)))

goal (1 subgoal):
 1. regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . triple.pairs_uminus (Rep_phi f) (-?rf f,Rep_phi f (?rf f)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - Abs_lifted_pair (\<lambda>f. (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f))) = Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f)))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<forall>f. (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f) \<and> (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f)

goal (1 subgoal):
 1. - Abs_lifted_pair (\<lambda>f. (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f))) = Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f)))
[PROOF STEP]
by (simp add: eq_onp_same_args uminus_lifted_pair.abs_eq)
[PROOF STATE]
proof (state)
this:
- Abs_lifted_pair (\<lambda>f. (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f))) = Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f)))

goal (1 subgoal):
 1. regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- Abs_lifted_pair (\<lambda>f. (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f))) = Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f)))

goal (1 subgoal):
 1. regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . (?rf f,Rep_phi f (-?rf f)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f))) = Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)))
[PROOF STEP]
by (metis (no_types, lifting) simp_phi triple_def triple.pairs_uminus.simps double_compl)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f))) = Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)))

goal (1 subgoal):
 1. regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
- - Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))) = Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
- - Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))) = Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)))

goal (1 subgoal):
 1. regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))

goal (1 subgoal):
 1. ba_iso (ba_iso_inv xf) = xf
[PROOF STEP]
hence "in_p_image (Abs_lifted_pair (\<lambda>f . (?rf f,Rep_phi f (-?rf f))))"
[PROOF STATE]
proof (prove)
using this:
regular (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))

goal (1 subgoal):
 1. in_p_image (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
in_p_image (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))

goal (1 subgoal):
 1. ba_iso (ba_iso_inv xf) = xf
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
in_p_image (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))

goal (1 subgoal):
 1. ba_iso (ba_iso_inv xf) = xf
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
in_p_image (Abs_lifted_pair (\<lambda>f. (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f))))
\<forall>f. (- Rep_lifted_boolean_algebra xf f, Rep_phi f (Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f) \<and> (Rep_lifted_boolean_algebra xf f, Rep_phi f (- Rep_lifted_boolean_algebra xf f)) \<in> triple.pairs (Rep_phi f)

goal (1 subgoal):
 1. ba_iso (ba_iso_inv xf) = xf
[PROOF STEP]
by (simp add: Rep_lifted_boolean_algebra_inverse Abs_lifted_pair_inverse Abs_regular_inverse)
[PROOF STATE]
proof (state)
this:
ba_iso (ba_iso_inv xf) = xf

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ba_iso:
  "boolean_algebra_isomorphism ba_iso"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((bounded_lattice_homomorphism ba_iso \<and> uminus_homomorphism ba_iso) \<and> bij ba_iso) \<and> minus_homomorphism ba_iso
[PROOF STEP]
proof (intro conjI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. sup_homomorphism ba_iso
 2. inf_homomorphism ba_iso
 3. top_homomorphism ba_iso
 4. bot_homomorphism ba_iso
 5. uminus_homomorphism ba_iso
 6. bij ba_iso
 7. minus_homomorphism ba_iso
[PROOF STEP]
show "Abs_lifted_boolean_algebra (\<lambda>f . fst (Rep_lifted_pair (Rep_regular bot) f)) = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bot_homomorphism ba_iso
[PROOF STEP]
by (simp add: bot_lifted_boolean_algebra_def bot_regular.rep_eq bot_lifted_pair.rep_eq)
[PROOF STATE]
proof (state)
this:
bot_homomorphism ba_iso

goal (6 subgoals):
 1. sup_homomorphism ba_iso
 2. inf_homomorphism ba_iso
 3. top_homomorphism ba_iso
 4. uminus_homomorphism ba_iso
 5. bij ba_iso
 6. minus_homomorphism ba_iso
[PROOF STEP]
show "Abs_lifted_boolean_algebra (\<lambda>f . fst (Rep_lifted_pair (Rep_regular top) f)) = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. top_homomorphism ba_iso
[PROOF STEP]
by (simp add: top_lifted_boolean_algebra_def top_regular.rep_eq top_lifted_pair.rep_eq)
[PROOF STATE]
proof (state)
this:
top_homomorphism ba_iso

goal (5 subgoals):
 1. sup_homomorphism ba_iso
 2. inf_homomorphism ba_iso
 3. uminus_homomorphism ba_iso
 4. bij ba_iso
 5. minus_homomorphism ba_iso
[PROOF STEP]
show "\<forall>pf qf . Abs_lifted_boolean_algebra (\<lambda>f::('a,'b) phi . fst (Rep_lifted_pair (Rep_regular (pf \<squnion> qf)) f)) = Abs_lifted_boolean_algebra (\<lambda>f . fst (Rep_lifted_pair (Rep_regular pf) f)) \<squnion> Abs_lifted_boolean_algebra (\<lambda>f . fst (Rep_lifted_pair (Rep_regular qf) f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_homomorphism ba_iso
[PROOF STEP]
proof (intro allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pf qf. ba_iso (pf \<squnion> qf) = ba_iso pf \<squnion> ba_iso qf
[PROOF STEP]
fix pf qf :: "('a,'b) lifted_pair regular"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pf qf. ba_iso (pf \<squnion> qf) = ba_iso pf \<squnion> ba_iso qf
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pf qf. ba_iso (pf \<squnion> qf) = ba_iso pf \<squnion> ba_iso qf
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pf qf. ba_iso (pf \<squnion> qf) = ba_iso pf \<squnion> ba_iso qf
[PROOF STEP]
obtain x y z w where 1: "(x,y) = Rep_lifted_pair (Rep_regular pf) f \<and> (z,w) = Rep_lifted_pair (Rep_regular qf) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y z w. (x, y) = Rep_lifted_pair (Rep_regular pf) f \<and> (z, w) = Rep_lifted_pair (Rep_regular qf) f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. (\<And>x y z w. (x, y) = Rep_lifted_pair (Rep_regular pf) f \<and> (z, w) = Rep_lifted_pair (Rep_regular qf) f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(x, y) = Rep_lifted_pair (Rep_regular pf) f \<and> (z, w) = Rep_lifted_pair (Rep_regular qf) f

goal (1 subgoal):
 1. \<And>pf qf. ba_iso (pf \<squnion> qf) = ba_iso pf \<squnion> ba_iso qf
[PROOF STEP]
have "triple (Rep_phi f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple (Rep_phi f)
[PROOF STEP]
by (simp add: triple_def)
[PROOF STATE]
proof (state)
this:
triple (Rep_phi f)

goal (1 subgoal):
 1. \<And>pf qf. ba_iso (pf \<squnion> qf) = ba_iso pf \<squnion> ba_iso qf
[PROOF STEP]
hence "fst (triple.pairs_sup (x,y) (z,w)) = fst (x,y) \<squnion> fst (z,w)"
[PROOF STATE]
proof (prove)
using this:
triple (Rep_phi f)

goal (1 subgoal):
 1. fst (triple.pairs_sup (x, y) (z, w)) = fst (x, y) \<squnion> fst (z, w)
[PROOF STEP]
using triple.pairs_sup.simps
[PROOF STATE]
proof (prove)
using this:
triple (Rep_phi f)
triple ?phi \<Longrightarrow> triple.pairs_sup (?x, ?y) (?z, ?w) = (?x \<squnion> ?z, ?y \<sqinter> ?w)

goal (1 subgoal):
 1. fst (triple.pairs_sup (x, y) (z, w)) = fst (x, y) \<squnion> fst (z, w)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
fst (triple.pairs_sup (x, y) (z, w)) = fst (x, y) \<squnion> fst (z, w)

goal (1 subgoal):
 1. \<And>pf qf. ba_iso (pf \<squnion> qf) = ba_iso pf \<squnion> ba_iso qf
[PROOF STEP]
hence "fst (triple.pairs_sup (Rep_lifted_pair (Rep_regular pf) f) (Rep_lifted_pair (Rep_regular qf) f)) = fst (Rep_lifted_pair (Rep_regular pf) f) \<squnion> fst (Rep_lifted_pair (Rep_regular qf) f)"
[PROOF STATE]
proof (prove)
using this:
fst (triple.pairs_sup (x, y) (z, w)) = fst (x, y) \<squnion> fst (z, w)

goal (1 subgoal):
 1. fst (triple.pairs_sup (Rep_lifted_pair (Rep_regular pf) f) (Rep_lifted_pair (Rep_regular qf) f)) = fst (Rep_lifted_pair (Rep_regular pf) f) \<squnion> fst (Rep_lifted_pair (Rep_regular qf) f)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
fst (triple.pairs_sup (x, y) (z, w)) = fst (x, y) \<squnion> fst (z, w)
(x, y) = Rep_lifted_pair (Rep_regular pf) f \<and> (z, w) = Rep_lifted_pair (Rep_regular qf) f

goal (1 subgoal):
 1. fst (triple.pairs_sup (Rep_lifted_pair (Rep_regular pf) f) (Rep_lifted_pair (Rep_regular qf) f)) = fst (Rep_lifted_pair (Rep_regular pf) f) \<squnion> fst (Rep_lifted_pair (Rep_regular qf) f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst (triple.pairs_sup (Rep_lifted_pair (Rep_regular pf) f) (Rep_lifted_pair (Rep_regular qf) f)) = fst (Rep_lifted_pair (Rep_regular pf) f) \<squnion> fst (Rep_lifted_pair (Rep_regular qf) f)

goal (1 subgoal):
 1. \<And>pf qf. ba_iso (pf \<squnion> qf) = ba_iso pf \<squnion> ba_iso qf
[PROOF STEP]
hence "fst (Rep_lifted_pair (Rep_regular (pf \<squnion> qf)) f) = fst (Rep_lifted_pair (Rep_regular pf) f) \<squnion> fst (Rep_lifted_pair (Rep_regular qf) f)"
[PROOF STATE]
proof (prove)
using this:
fst (triple.pairs_sup (Rep_lifted_pair (Rep_regular pf) f) (Rep_lifted_pair (Rep_regular qf) f)) = fst (Rep_lifted_pair (Rep_regular pf) f) \<squnion> fst (Rep_lifted_pair (Rep_regular qf) f)

goal (1 subgoal):
 1. fst (Rep_lifted_pair (Rep_regular (pf \<squnion> qf)) f) = fst (Rep_lifted_pair (Rep_regular pf) f) \<squnion> fst (Rep_lifted_pair (Rep_regular qf) f)
[PROOF STEP]
by (unfold sup_regular.rep_eq sup_lifted_pair.rep_eq) simp
[PROOF STATE]
proof (state)
this:
fst (Rep_lifted_pair (Rep_regular (pf \<squnion> qf)) f) = fst (Rep_lifted_pair (Rep_regular pf) f) \<squnion> fst (Rep_lifted_pair (Rep_regular qf) f)

goal (1 subgoal):
 1. \<And>pf qf. ba_iso (pf \<squnion> qf) = ba_iso pf \<squnion> ba_iso qf
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
fst (Rep_lifted_pair (Rep_regular (pf \<squnion> qf)) ?f4) = fst (Rep_lifted_pair (Rep_regular pf) ?f4) \<squnion> fst (Rep_lifted_pair (Rep_regular qf) ?f4)

goal (1 subgoal):
 1. \<And>pf qf. ba_iso (pf \<squnion> qf) = ba_iso pf \<squnion> ba_iso qf
[PROOF STEP]
thus "Abs_lifted_boolean_algebra (\<lambda>f . fst (Rep_lifted_pair (Rep_regular (pf \<squnion> qf)) f)) = Abs_lifted_boolean_algebra (\<lambda>f . fst (Rep_lifted_pair (Rep_regular pf) f)) \<squnion> Abs_lifted_boolean_algebra (\<lambda>f . fst (Rep_lifted_pair (Rep_regular qf) f))"
[PROOF STATE]
proof (prove)
using this:
fst (Rep_lifted_pair (Rep_regular (pf \<squnion> qf)) ?f4) = fst (Rep_lifted_pair (Rep_regular pf) ?f4) \<squnion> fst (Rep_lifted_pair (Rep_regular qf) ?f4)

goal (1 subgoal):
 1. ba_iso (pf \<squnion> qf) = ba_iso pf \<squnion> ba_iso qf
[PROOF STEP]
by (simp add: eq_onp_same_args sup_lifted_boolean_algebra.abs_eq sup_regular.rep_eq sup_lifted_boolean_algebra.rep_eq)
[PROOF STATE]
proof (state)
this:
ba_iso (pf \<squnion> qf) = ba_iso pf \<squnion> ba_iso qf

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

goal (4 subgoals):
 1. inf_homomorphism ba_iso
 2. uminus_homomorphism ba_iso
 3. bij ba_iso
 4. minus_homomorphism ba_iso
[PROOF STEP]
show 1: "\<forall>pf qf . Abs_lifted_boolean_algebra (\<lambda>f::('a,'b) phi . fst (Rep_lifted_pair (Rep_regular (pf \<sqinter> qf)) f)) = Abs_lifted_boolean_algebra (\<lambda>f . fst (Rep_lifted_pair (Rep_regular pf) f)) \<sqinter> Abs_lifted_boolean_algebra (\<lambda>f . fst (Rep_lifted_pair (Rep_regular qf) f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inf_homomorphism ba_iso
[PROOF STEP]
proof (intro allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pf qf. ba_iso (pf \<sqinter> qf) = ba_iso pf \<sqinter> ba_iso qf
[PROOF STEP]
fix pf qf :: "('a,'b) lifted_pair regular"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pf qf. ba_iso (pf \<sqinter> qf) = ba_iso pf \<sqinter> ba_iso qf
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pf qf. ba_iso (pf \<sqinter> qf) = ba_iso pf \<sqinter> ba_iso qf
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pf qf. ba_iso (pf \<sqinter> qf) = ba_iso pf \<sqinter> ba_iso qf
[PROOF STEP]
obtain x y z w where 1: "(x,y) = Rep_lifted_pair (Rep_regular pf) f \<and> (z,w) = Rep_lifted_pair (Rep_regular qf) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y z w. (x, y) = Rep_lifted_pair (Rep_regular pf) f \<and> (z, w) = Rep_lifted_pair (Rep_regular qf) f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

goal (1 subgoal):
 1. (\<And>x y z w. (x, y) = Rep_lifted_pair (Rep_regular pf) f \<and> (z, w) = Rep_lifted_pair (Rep_regular qf) f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(x, y) = Rep_lifted_pair (Rep_regular pf) f \<and> (z, w) = Rep_lifted_pair (Rep_regular qf) f

goal (1 subgoal):
 1. \<And>pf qf. ba_iso (pf \<sqinter> qf) = ba_iso pf \<sqinter> ba_iso qf
[PROOF STEP]
have "triple (Rep_phi f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple (Rep_phi f)
[PROOF STEP]
by (simp add: triple_def)
[PROOF STATE]
proof (state)
this:
triple (Rep_phi f)

goal (1 subgoal):
 1. \<And>pf qf. ba_iso (pf \<sqinter> qf) = ba_iso pf \<sqinter> ba_iso qf
[PROOF STEP]
hence "fst (triple.pairs_inf (x,y) (z,w)) = fst (x,y) \<sqinter> fst (z,w)"
[PROOF STATE]
proof (prove)
using this:
triple (Rep_phi f)

goal (1 subgoal):
 1. fst (triple.pairs_inf (x, y) (z, w)) = fst (x, y) \<sqinter> fst (z, w)
[PROOF STEP]
using triple.pairs_inf.simps
[PROOF STATE]
proof (prove)
using this:
triple (Rep_phi f)
triple ?phi \<Longrightarrow> triple.pairs_inf (?x, ?y) (?z, ?w) = (?x \<sqinter> ?z, ?y \<squnion> ?w)

goal (1 subgoal):
 1. fst (triple.pairs_inf (x, y) (z, w)) = fst (x, y) \<sqinter> fst (z, w)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
fst (triple.pairs_inf (x, y) (z, w)) = fst (x, y) \<sqinter> fst (z, w)

goal (1 subgoal):
 1. \<And>pf qf. ba_iso (pf \<sqinter> qf) = ba_iso pf \<sqinter> ba_iso qf
[PROOF STEP]
hence "fst (triple.pairs_inf (Rep_lifted_pair (Rep_regular pf) f) (Rep_lifted_pair (Rep_regular qf) f)) = fst (Rep_lifted_pair (Rep_regular pf) f) \<sqinter> fst (Rep_lifted_pair (Rep_regular qf) f)"
[PROOF STATE]
proof (prove)
using this:
fst (triple.pairs_inf (x, y) (z, w)) = fst (x, y) \<sqinter> fst (z, w)

goal (1 subgoal):
 1. fst (triple.pairs_inf (Rep_lifted_pair (Rep_regular pf) f) (Rep_lifted_pair (Rep_regular qf) f)) = fst (Rep_lifted_pair (Rep_regular pf) f) \<sqinter> fst (Rep_lifted_pair (Rep_regular qf) f)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
fst (triple.pairs_inf (x, y) (z, w)) = fst (x, y) \<sqinter> fst (z, w)
(x, y) = Rep_lifted_pair (Rep_regular pf) f \<and> (z, w) = Rep_lifted_pair (Rep_regular qf) f

goal (1 subgoal):
 1. fst (triple.pairs_inf (Rep_lifted_pair (Rep_regular pf) f) (Rep_lifted_pair (Rep_regular qf) f)) = fst (Rep_lifted_pair (Rep_regular pf) f) \<sqinter> fst (Rep_lifted_pair (Rep_regular qf) f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst (triple.pairs_inf (Rep_lifted_pair (Rep_regular pf) f) (Rep_lifted_pair (Rep_regular qf) f)) = fst (Rep_lifted_pair (Rep_regular pf) f) \<sqinter> fst (Rep_lifted_pair (Rep_regular qf) f)

goal (1 subgoal):
 1. \<And>pf qf. ba_iso (pf \<sqinter> qf) = ba_iso pf \<sqinter> ba_iso qf
[PROOF STEP]
hence "fst (Rep_lifted_pair (Rep_regular (pf \<sqinter> qf)) f) = fst (Rep_lifted_pair (Rep_regular pf) f) \<sqinter> fst (Rep_lifted_pair (Rep_regular qf) f)"
[PROOF STATE]
proof (prove)
using this:
fst (triple.pairs_inf (Rep_lifted_pair (Rep_regular pf) f) (Rep_lifted_pair (Rep_regular qf) f)) = fst (Rep_lifted_pair (Rep_regular pf) f) \<sqinter> fst (Rep_lifted_pair (Rep_regular qf) f)

goal (1 subgoal):
 1. fst (Rep_lifted_pair (Rep_regular (pf \<sqinter> qf)) f) = fst (Rep_lifted_pair (Rep_regular pf) f) \<sqinter> fst (Rep_lifted_pair (Rep_regular qf) f)
[PROOF STEP]
by (unfold inf_regular.rep_eq inf_lifted_pair.rep_eq) simp
[PROOF STATE]
proof (state)
this:
fst (Rep_lifted_pair (Rep_regular (pf \<sqinter> qf)) f) = fst (Rep_lifted_pair (Rep_regular pf) f) \<sqinter> fst (Rep_lifted_pair (Rep_regular qf) f)

goal (1 subgoal):
 1. \<And>pf qf. ba_iso (pf \<sqinter> qf) = ba_iso pf \<sqinter> ba_iso qf
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
fst (Rep_lifted_pair (Rep_regular (pf \<sqinter> qf)) ?f4) = fst (Rep_lifted_pair (Rep_regular pf) ?f4) \<sqinter> fst (Rep_lifted_pair (Rep_regular qf) ?f4)

goal (1 subgoal):
 1. \<And>pf qf. ba_iso (pf \<sqinter> qf) = ba_iso pf \<sqinter> ba_iso qf
[PROOF STEP]
thus "Abs_lifted_boolean_algebra (\<lambda>f . fst (Rep_lifted_pair (Rep_regular (pf \<sqinter> qf)) f)) = Abs_lifted_boolean_algebra (\<lambda>f . fst (Rep_lifted_pair (Rep_regular pf) f)) \<sqinter> Abs_lifted_boolean_algebra (\<lambda>f . fst (Rep_lifted_pair (Rep_regular qf) f))"
[PROOF STATE]
proof (prove)
using this:
fst (Rep_lifted_pair (Rep_regular (pf \<sqinter> qf)) ?f4) = fst (Rep_lifted_pair (Rep_regular pf) ?f4) \<sqinter> fst (Rep_lifted_pair (Rep_regular qf) ?f4)

goal (1 subgoal):
 1. ba_iso (pf \<sqinter> qf) = ba_iso pf \<sqinter> ba_iso qf
[PROOF STEP]
by (simp add: eq_onp_same_args inf_lifted_boolean_algebra.abs_eq inf_regular.rep_eq inf_lifted_boolean_algebra.rep_eq)
[PROOF STATE]
proof (state)
this:
ba_iso (pf \<sqinter> qf) = ba_iso pf \<sqinter> ba_iso qf

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

goal (3 subgoals):
 1. uminus_homomorphism ba_iso
 2. bij ba_iso
 3. minus_homomorphism ba_iso
[PROOF STEP]
show "\<forall>pf . Abs_lifted_boolean_algebra (\<lambda>f::('a,'b) phi . fst (Rep_lifted_pair (Rep_regular (-pf)) f)) = -Abs_lifted_boolean_algebra (\<lambda>f . fst (Rep_lifted_pair (Rep_regular pf) f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. uminus_homomorphism ba_iso
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pf. ba_iso (- pf) = - ba_iso pf
[PROOF STEP]
fix pf :: "('a,'b) lifted_pair regular"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pf. ba_iso (- pf) = - ba_iso pf
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pf. ba_iso (- pf) = - ba_iso pf
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pf. ba_iso (- pf) = - ba_iso pf
[PROOF STEP]
obtain x y where 1: "(x,y) = Rep_lifted_pair (Rep_regular pf) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. (x, y) = Rep_lifted_pair (Rep_regular pf) f \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using prod.collapse
[PROOF STATE]
proof (prove)
using this:
(fst ?prod, snd ?prod) = ?prod

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

goal (1 subgoal):
 1. \<And>pf. ba_iso (- pf) = - ba_iso pf
[PROOF STEP]
have "triple (Rep_phi f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple (Rep_phi f)
[PROOF STEP]
by (simp add: triple_def)
[PROOF STATE]
proof (state)
this:
triple (Rep_phi f)

goal (1 subgoal):
 1. \<And>pf. ba_iso (- pf) = - ba_iso pf
[PROOF STEP]
hence "fst (triple.pairs_uminus (Rep_phi f) (x,y)) = -fst (x,y)"
[PROOF STATE]
proof (prove)
using this:
triple (Rep_phi f)

goal (1 subgoal):
 1. fst (triple.pairs_uminus (Rep_phi f) (x, y)) = - fst (x, y)
[PROOF STEP]
using triple.pairs_uminus.simps
[PROOF STATE]
proof (prove)
using this:
triple (Rep_phi f)
triple ?phi \<Longrightarrow> triple.pairs_uminus ?phi (?x, ?y) = (- ?x, ?phi ?x)

goal (1 subgoal):
 1. fst (triple.pairs_uminus (Rep_phi f) (x, y)) = - fst (x, y)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
fst (triple.pairs_uminus (Rep_phi f) (x, y)) = - fst (x, y)

goal (1 subgoal):
 1. \<And>pf. ba_iso (- pf) = - ba_iso pf
[PROOF STEP]
hence "fst (triple.pairs_uminus (Rep_phi f) (Rep_lifted_pair (Rep_regular pf) f)) = -fst (Rep_lifted_pair (Rep_regular pf) f)"
[PROOF STATE]
proof (prove)
using this:
fst (triple.pairs_uminus (Rep_phi f) (x, y)) = - fst (x, y)

goal (1 subgoal):
 1. fst (triple.pairs_uminus (Rep_phi f) (Rep_lifted_pair (Rep_regular pf) f)) = - fst (Rep_lifted_pair (Rep_regular pf) f)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
fst (triple.pairs_uminus (Rep_phi f) (x, y)) = - fst (x, y)
(x, y) = Rep_lifted_pair (Rep_regular pf) f

goal (1 subgoal):
 1. fst (triple.pairs_uminus (Rep_phi f) (Rep_lifted_pair (Rep_regular pf) f)) = - fst (Rep_lifted_pair (Rep_regular pf) f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fst (triple.pairs_uminus (Rep_phi f) (Rep_lifted_pair (Rep_regular pf) f)) = - fst (Rep_lifted_pair (Rep_regular pf) f)

goal (1 subgoal):
 1. \<And>pf. ba_iso (- pf) = - ba_iso pf
[PROOF STEP]
hence "fst (Rep_lifted_pair (Rep_regular (-pf)) f) = -fst (Rep_lifted_pair (Rep_regular pf) f)"
[PROOF STATE]
proof (prove)
using this:
fst (triple.pairs_uminus (Rep_phi f) (Rep_lifted_pair (Rep_regular pf) f)) = - fst (Rep_lifted_pair (Rep_regular pf) f)

goal (1 subgoal):
 1. fst (Rep_lifted_pair (Rep_regular (- pf)) f) = - fst (Rep_lifted_pair (Rep_regular pf) f)
[PROOF STEP]
by (unfold uminus_regular.rep_eq uminus_lifted_pair.rep_eq) simp
[PROOF STATE]
proof (state)
this:
fst (Rep_lifted_pair (Rep_regular (- pf)) f) = - fst (Rep_lifted_pair (Rep_regular pf) f)

goal (1 subgoal):
 1. \<And>pf. ba_iso (- pf) = - ba_iso pf
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
fst (Rep_lifted_pair (Rep_regular (- pf)) ?f4) = - fst (Rep_lifted_pair (Rep_regular pf) ?f4)

goal (1 subgoal):
 1. \<And>pf. ba_iso (- pf) = - ba_iso pf
[PROOF STEP]
thus "Abs_lifted_boolean_algebra (\<lambda>f . fst (Rep_lifted_pair (Rep_regular (-pf)) f)) = -Abs_lifted_boolean_algebra (\<lambda>f . fst (Rep_lifted_pair (Rep_regular pf) f))"
[PROOF STATE]
proof (prove)
using this:
fst (Rep_lifted_pair (Rep_regular (- pf)) ?f4) = - fst (Rep_lifted_pair (Rep_regular pf) ?f4)

goal (1 subgoal):
 1. ba_iso (- pf) = - ba_iso pf
[PROOF STEP]
by (simp add: eq_onp_same_args uminus_lifted_boolean_algebra.abs_eq uminus_regular.rep_eq uminus_lifted_boolean_algebra.rep_eq)
[PROOF STATE]
proof (state)
this:
ba_iso (- pf) = - ba_iso pf

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

goal (2 subgoals):
 1. bij ba_iso
 2. minus_homomorphism ba_iso
[PROOF STEP]
thus "\<forall>pf qf . Abs_lifted_boolean_algebra (\<lambda>f::('a,'b) phi . fst (Rep_lifted_pair (Rep_regular (pf - qf)) f)) = Abs_lifted_boolean_algebra (\<lambda>f . fst (Rep_lifted_pair (Rep_regular pf) f)) - Abs_lifted_boolean_algebra (\<lambda>f . fst (Rep_lifted_pair (Rep_regular qf) f))"
[PROOF STATE]
proof (prove)
using this:
uminus_homomorphism ba_iso

goal (1 subgoal):
 1. minus_homomorphism ba_iso
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
uminus_homomorphism ba_iso
inf_homomorphism ba_iso

goal (1 subgoal):
 1. minus_homomorphism ba_iso
[PROOF STEP]
by (simp add: diff_eq)
[PROOF STATE]
proof (state)
this:
minus_homomorphism ba_iso

goal (1 subgoal):
 1. bij ba_iso
[PROOF STEP]
show "bij ba_iso"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij ba_iso
[PROOF STEP]
by (rule invertible_bij[where g=ba_iso_inv]) (simp_all add: ba_iso_left_invertible ba_iso_right_invertible)
[PROOF STATE]
proof (state)
this:
bij ba_iso

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma get_dense_char:
  "Rep_lifted_pair (Rep_dense pf) f = (top,up_filter (get_dense pf f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense pf) f = (top, up_filter (get_dense pf f))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense pf) f = (top, up_filter (get_dense pf f))
[PROOF STEP]
obtain x y where 1: "(x,y) = Rep_lifted_pair (Rep_dense pf) f \<and> (x,y) \<in> triple.pairs (Rep_phi f) \<and> triple.pairs_uminus (Rep_phi f) (x,y) = triple.pairs_bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. (x, y) = Rep_lifted_pair (Rep_dense pf) f \<and> (x, y) \<in> triple.pairs (Rep_phi f) \<and> triple.pairs_uminus (Rep_phi f) (x, y) = (bot, Filters.filter.Abs_filter UNIV) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis bot_lifted_pair.rep_eq prod.collapse simp_dense simp_lifted_pair uminus_lifted_pair.rep_eq)
[PROOF STATE]
proof (state)
this:
(x, y) = Rep_lifted_pair (Rep_dense pf) f \<and> (x, y) \<in> triple.pairs (Rep_phi f) \<and> triple.pairs_uminus (Rep_phi f) (x, y) = (bot, Filters.filter.Abs_filter UNIV)

goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense pf) f = (top, up_filter (get_dense pf f))
[PROOF STEP]
hence 2: "x = top"
[PROOF STATE]
proof (prove)
using this:
(x, y) = Rep_lifted_pair (Rep_dense pf) f \<and> (x, y) \<in> triple.pairs (Rep_phi f) \<and> triple.pairs_uminus (Rep_phi f) (x, y) = (bot, Filters.filter.Abs_filter UNIV)

goal (1 subgoal):
 1. x = top
[PROOF STEP]
by (simp add: triple.intro triple.pairs_uminus.simps dense_pp)
[PROOF STATE]
proof (state)
this:
x = top

goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense pf) f = (top, up_filter (get_dense pf f))
[PROOF STEP]
have "triple (Rep_phi f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple (Rep_phi f)
[PROOF STEP]
by (simp add: triple_def)
[PROOF STATE]
proof (state)
this:
triple (Rep_phi f)

goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense pf) f = (top, up_filter (get_dense pf f))
[PROOF STEP]
hence "\<exists>z. y = Rep_phi f (-x) \<squnion> up_filter z"
[PROOF STATE]
proof (prove)
using this:
triple (Rep_phi f)

goal (1 subgoal):
 1. \<exists>z. y = Rep_phi f (- x) \<squnion> up_filter z
[PROOF STEP]
using 1 triple.pairs_def
[PROOF STATE]
proof (prove)
using this:
triple (Rep_phi f)
(x, y) = Rep_lifted_pair (Rep_dense pf) f \<and> (x, y) \<in> triple.pairs (Rep_phi f) \<and> triple.pairs_uminus (Rep_phi f) (x, y) = (bot, Filters.filter.Abs_filter UNIV)
triple ?phi \<Longrightarrow> triple.pairs ?phi = {(x, y). \<exists>z. y = ?phi (- x) \<squnion> up_filter z}

goal (1 subgoal):
 1. \<exists>z. y = Rep_phi f (- x) \<squnion> up_filter z
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>z. y = Rep_phi f (- x) \<squnion> up_filter z

goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense pf) f = (top, up_filter (get_dense pf f))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>z. y = Rep_phi f (- x) \<squnion> up_filter z
[PROOF STEP]
obtain z where "y = up_filter z"
[PROOF STATE]
proof (prove)
using this:
\<exists>z. y = Rep_phi f (- x) \<squnion> up_filter z

goal (1 subgoal):
 1. (\<And>z. y = up_filter z \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
\<exists>z. y = Rep_phi f (- x) \<squnion> up_filter z
x = top

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

goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense pf) f = (top, up_filter (get_dense pf f))
[PROOF STEP]
hence "Rep_lifted_pair (Rep_dense pf) f = (top,up_filter z)"
[PROOF STATE]
proof (prove)
using this:
y = up_filter z

goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense pf) f = (top, up_filter z)
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
y = up_filter z
(x, y) = Rep_lifted_pair (Rep_dense pf) f \<and> (x, y) \<in> triple.pairs (Rep_phi f) \<and> triple.pairs_uminus (Rep_phi f) (x, y) = (bot, Filters.filter.Abs_filter UNIV)
x = top

goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense pf) f = (top, up_filter z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Rep_lifted_pair (Rep_dense pf) f = (top, up_filter z)

goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense pf) f = (top, up_filter (get_dense pf f))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Rep_lifted_pair (Rep_dense pf) f = (top, up_filter z)

goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense pf) f = (top, up_filter (get_dense pf f))
[PROOF STEP]
by (metis (mono_tags, lifting) tfl_some get_dense.simps)
[PROOF STATE]
proof (state)
this:
Rep_lifted_pair (Rep_dense pf) f = (top, up_filter (get_dense pf f))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dl_iso_inv_lifted_pair:
  "(top,up_filter (Rep_lifted_distrib_lattice_top xf f)) \<in> triple.pairs (Rep_phi f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (top, up_filter (Rep_lifted_distrib_lattice_top xf f)) \<in> triple.pairs (Rep_phi f)
[PROOF STEP]
by (metis (no_types, opaque_lifting) compl_bot_eq double_compl simp_phi sup_bot.left_neutral triple.sa_iso_pair triple_def)


[STATEMENT]
lemma dl_iso_inv_dense:
  "dense (Abs_lifted_pair (\<lambda>f . (top,up_filter (Rep_lifted_distrib_lattice_top xf f))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))))
[PROOF STEP]
have "\<forall>f . triple.pairs_uminus (Rep_phi f) (top,up_filter (Rep_lifted_distrib_lattice_top xf f)) = triple.pairs_bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f. triple.pairs_uminus (Rep_phi f) (top, up_filter (Rep_lifted_distrib_lattice_top xf f)) = (bot, Filters.filter.Abs_filter UNIV)
[PROOF STEP]
by (simp add: top_filter.abs_eq triple.pairs_uminus.simps triple_def)
[PROOF STATE]
proof (state)
this:
\<forall>f. triple.pairs_uminus (Rep_phi f) (top, up_filter (Rep_lifted_distrib_lattice_top xf f)) = (bot, Filters.filter.Abs_filter UNIV)

goal (1 subgoal):
 1. dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))))
[PROOF STEP]
hence "bot = -Abs_lifted_pair (\<lambda>f . (top,up_filter (Rep_lifted_distrib_lattice_top xf f)))"
[PROOF STATE]
proof (prove)
using this:
\<forall>f. triple.pairs_uminus (Rep_phi f) (top, up_filter (Rep_lifted_distrib_lattice_top xf f)) = (bot, Filters.filter.Abs_filter UNIV)

goal (1 subgoal):
 1. bot = - Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f)))
[PROOF STEP]
by (simp add: eq_onp_def uminus_lifted_pair.abs_eq dl_iso_inv_lifted_pair bot_lifted_pair_def)
[PROOF STATE]
proof (state)
this:
bot = - Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f)))

goal (1 subgoal):
 1. dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
bot = - Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f)))

goal (1 subgoal):
 1. dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dl_iso_left_invertible:
  "dl_iso_inv (dl_iso pf) = pf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dl_iso_inv (dl_iso pf) = pf
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dl_iso_inv (dl_iso pf) = pf
[PROOF STEP]
have "dl_iso_inv (dl_iso pf) = Abs_dense (Abs_lifted_pair (\<lambda>f . (top,up_filter (get_dense pf f))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dl_iso_inv (dl_iso pf) = Abs_dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (get_dense pf f))))
[PROOF STEP]
by (metis Abs_lifted_distrib_lattice_top_inverse UNIV_I UNIV_def)
[PROOF STATE]
proof (state)
this:
dl_iso_inv (dl_iso pf) = Abs_dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (get_dense pf f))))

goal (1 subgoal):
 1. dl_iso_inv (dl_iso pf) = pf
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dl_iso_inv (dl_iso pf) = Abs_dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (get_dense pf f))))

goal (1 subgoal):
 1. dl_iso_inv (dl_iso pf) = pf
[PROOF STEP]
have "... = Abs_dense (Abs_lifted_pair (Rep_lifted_pair (Rep_dense pf)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (get_dense pf f)))) = Abs_dense (Abs_lifted_pair (Rep_lifted_pair (Rep_dense pf)))
[PROOF STEP]
by (metis get_dense_char)
[PROOF STATE]
proof (state)
this:
Abs_dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (get_dense pf f)))) = Abs_dense (Abs_lifted_pair (Rep_lifted_pair (Rep_dense pf)))

goal (1 subgoal):
 1. dl_iso_inv (dl_iso pf) = pf
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (get_dense pf f)))) = Abs_dense (Abs_lifted_pair (Rep_lifted_pair (Rep_dense pf)))

goal (1 subgoal):
 1. dl_iso_inv (dl_iso pf) = pf
[PROOF STEP]
have "... = pf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_dense (Abs_lifted_pair (Rep_lifted_pair (Rep_dense pf))) = pf
[PROOF STEP]
by (simp add: Rep_dense_inverse Rep_lifted_pair_inverse)
[PROOF STATE]
proof (state)
this:
Abs_dense (Abs_lifted_pair (Rep_lifted_pair (Rep_dense pf))) = pf

goal (1 subgoal):
 1. dl_iso_inv (dl_iso pf) = pf
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dl_iso_inv (dl_iso pf) = pf
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dl_iso_inv (dl_iso pf) = pf

goal (1 subgoal):
 1. dl_iso_inv (dl_iso pf) = pf
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
dl_iso_inv (dl_iso pf) = pf

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dl_iso_right_invertible:
  "dl_iso (dl_iso_inv xf) = xf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dl_iso (dl_iso_inv xf) = xf
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dl_iso (dl_iso_inv xf) = xf
[PROOF STEP]
let ?rf = "Rep_lifted_distrib_lattice_top xf"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dl_iso (dl_iso_inv xf) = xf
[PROOF STEP]
let ?pf = "Abs_dense (Abs_lifted_pair (\<lambda>f . (top,up_filter (?rf f))))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dl_iso (dl_iso_inv xf) = xf
[PROOF STEP]
have 1: "\<forall>f . (top,up_filter (?rf f)) \<in> triple.pairs (Rep_phi f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f)) \<in> triple.pairs (Rep_phi f)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f)) \<in> triple.pairs (Rep_phi f)
[PROOF STEP]
fix f :: "('a,'b) phi"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f)) \<in> triple.pairs (Rep_phi f)
[PROOF STEP]
have "triple (Rep_phi f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple (Rep_phi f)
[PROOF STEP]
by (simp add: triple_def)
[PROOF STATE]
proof (state)
this:
triple (Rep_phi f)

goal (1 subgoal):
 1. \<And>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f)) \<in> triple.pairs (Rep_phi f)
[PROOF STEP]
thus "(top,up_filter (?rf f)) \<in> triple.pairs (Rep_phi f)"
[PROOF STATE]
proof (prove)
using this:
triple (Rep_phi f)

goal (1 subgoal):
 1. (top, up_filter (Rep_lifted_distrib_lattice_top xf f)) \<in> triple.pairs (Rep_phi f)
[PROOF STEP]
using triple.pairs_def
[PROOF STATE]
proof (prove)
using this:
triple (Rep_phi f)
triple ?phi \<Longrightarrow> triple.pairs ?phi = {(x, y). \<exists>z. y = ?phi (- x) \<squnion> up_filter z}

goal (1 subgoal):
 1. (top, up_filter (Rep_lifted_distrib_lattice_top xf f)) \<in> triple.pairs (Rep_phi f)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
(top, up_filter (Rep_lifted_distrib_lattice_top xf f)) \<in> triple.pairs (Rep_phi f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f)) \<in> triple.pairs (Rep_phi f)

goal (1 subgoal):
 1. dl_iso (dl_iso_inv xf) = xf
[PROOF STEP]
have 2: "dense (Abs_lifted_pair (\<lambda>f . (top,up_filter (?rf f))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))))
[PROOF STEP]
have "-Abs_lifted_pair (\<lambda>f . (top,up_filter (?rf f))) = Abs_lifted_pair (\<lambda>f . triple.pairs_uminus (Rep_phi f) (top,up_filter (?rf f)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))) = Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (top, up_filter (Rep_lifted_distrib_lattice_top xf f)))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<forall>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f)) \<in> triple.pairs (Rep_phi f)

goal (1 subgoal):
 1. - Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))) = Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (top, up_filter (Rep_lifted_distrib_lattice_top xf f)))
[PROOF STEP]
by (simp add: eq_onp_same_args uminus_lifted_pair.abs_eq)
[PROOF STATE]
proof (state)
this:
- Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))) = Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (top, up_filter (Rep_lifted_distrib_lattice_top xf f)))

goal (1 subgoal):
 1. dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))) = Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (top, up_filter (Rep_lifted_distrib_lattice_top xf f)))

goal (1 subgoal):
 1. dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))))
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . (bot,Rep_phi f top))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (top, up_filter (Rep_lifted_distrib_lattice_top xf f))) = Abs_lifted_pair (\<lambda>f. (bot, Rep_phi f top))
[PROOF STEP]
by (simp add: triple.pairs_uminus.simps triple_def)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (top, up_filter (Rep_lifted_distrib_lattice_top xf f))) = Abs_lifted_pair (\<lambda>f. (bot, Rep_phi f top))

goal (1 subgoal):
 1. dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. triple.pairs_uminus (Rep_phi f) (top, up_filter (Rep_lifted_distrib_lattice_top xf f))) = Abs_lifted_pair (\<lambda>f. (bot, Rep_phi f top))

goal (1 subgoal):
 1. dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))))
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>f . triple.pairs_bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. (bot, Rep_phi f top)) = Abs_lifted_pair (\<lambda>f. (bot, Filters.filter.Abs_filter UNIV))
[PROOF STEP]
by (metis (no_types, opaque_lifting) simp_phi triple.phi_top triple_def)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. (bot, Rep_phi f top)) = Abs_lifted_pair (\<lambda>f. (bot, Filters.filter.Abs_filter UNIV))

goal (1 subgoal):
 1. dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. (bot, Rep_phi f top)) = Abs_lifted_pair (\<lambda>f. (bot, Filters.filter.Abs_filter UNIV))

goal (1 subgoal):
 1. dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))))
[PROOF STEP]
have "... = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>f. (bot, Filters.filter.Abs_filter UNIV)) = bot
[PROOF STEP]
by (simp add: bot_lifted_pair_def)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>f. (bot, Filters.filter.Abs_filter UNIV)) = bot

goal (1 subgoal):
 1. dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))))

goal (1 subgoal):
 1. dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))))

goal (1 subgoal):
 1. dl_iso (dl_iso_inv xf) = xf
[PROOF STEP]
have "get_dense ?pf = ?rf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get_dense (dl_iso_inv xf) = Rep_lifted_distrib_lattice_top xf
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. get_dense (dl_iso_inv xf) x = Rep_lifted_distrib_lattice_top xf x
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. get_dense (dl_iso_inv xf) x = Rep_lifted_distrib_lattice_top xf x
[PROOF STEP]
have "(top,up_filter (get_dense ?pf f)) = Rep_lifted_pair (Rep_dense ?pf) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (top, up_filter (get_dense (dl_iso_inv xf) f)) = Rep_lifted_pair (Rep_dense (dl_iso_inv xf)) f
[PROOF STEP]
by (metis get_dense_char)
[PROOF STATE]
proof (state)
this:
(top, up_filter (get_dense (dl_iso_inv xf) f)) = Rep_lifted_pair (Rep_dense (dl_iso_inv xf)) f

goal (1 subgoal):
 1. \<And>x. get_dense (dl_iso_inv xf) x = Rep_lifted_distrib_lattice_top xf x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(top, up_filter (get_dense (dl_iso_inv xf) f)) = Rep_lifted_pair (Rep_dense (dl_iso_inv xf)) f

goal (1 subgoal):
 1. \<And>x. get_dense (dl_iso_inv xf) x = Rep_lifted_distrib_lattice_top xf x
[PROOF STEP]
have "... = Rep_lifted_pair (Abs_lifted_pair (\<lambda>f . (top,up_filter (?rf f)))) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense (dl_iso_inv xf)) f = Rep_lifted_pair (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f)))) f
[PROOF STEP]
using Abs_dense_inverse 2
[PROOF STATE]
proof (prove)
using this:
?y \<in> dense_elements \<Longrightarrow> Rep_dense (Abs_dense ?y) = ?y
dense (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f))))

goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense (dl_iso_inv xf)) f = Rep_lifted_pair (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f)))) f
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Rep_lifted_pair (Rep_dense (dl_iso_inv xf)) f = Rep_lifted_pair (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f)))) f

goal (1 subgoal):
 1. \<And>x. get_dense (dl_iso_inv xf) x = Rep_lifted_distrib_lattice_top xf x
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Rep_lifted_pair (Rep_dense (dl_iso_inv xf)) f = Rep_lifted_pair (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f)))) f

goal (1 subgoal):
 1. \<And>x. get_dense (dl_iso_inv xf) x = Rep_lifted_distrib_lattice_top xf x
[PROOF STEP]
have "... = (top,up_filter (?rf f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_lifted_pair (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f)))) f = (top, up_filter (Rep_lifted_distrib_lattice_top xf f))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
\<forall>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f)) \<in> triple.pairs (Rep_phi f)

goal (1 subgoal):
 1. Rep_lifted_pair (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f)))) f = (top, up_filter (Rep_lifted_distrib_lattice_top xf f))
[PROOF STEP]
by (simp add: Abs_lifted_pair_inverse)
[PROOF STATE]
proof (state)
this:
Rep_lifted_pair (Abs_lifted_pair (\<lambda>f. (top, up_filter (Rep_lifted_distrib_lattice_top xf f)))) f = (top, up_filter (Rep_lifted_distrib_lattice_top xf f))

goal (1 subgoal):
 1. \<And>x. get_dense (dl_iso_inv xf) x = Rep_lifted_distrib_lattice_top xf x
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(top, up_filter (get_dense (dl_iso_inv xf) f)) = (top, up_filter (Rep_lifted_distrib_lattice_top xf f))
[PROOF STEP]
show "get_dense ?pf f = ?rf f"
[PROOF STATE]
proof (prove)
using this:
(top, up_filter (get_dense (dl_iso_inv xf) f)) = (top, up_filter (Rep_lifted_distrib_lattice_top xf f))

goal (1 subgoal):
 1. get_dense (dl_iso_inv xf) f = Rep_lifted_distrib_lattice_top xf f
[PROOF STEP]
using up_filter_injective
[PROOF STATE]
proof (prove)
using this:
(top, up_filter (get_dense (dl_iso_inv xf) f)) = (top, up_filter (Rep_lifted_distrib_lattice_top xf f))
up_filter ?x = up_filter ?y \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. get_dense (dl_iso_inv xf) f = Rep_lifted_distrib_lattice_top xf f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
get_dense (dl_iso_inv xf) f = Rep_lifted_distrib_lattice_top xf f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
get_dense (dl_iso_inv xf) = Rep_lifted_distrib_lattice_top xf

goal (1 subgoal):
 1. dl_iso (dl_iso_inv xf) = xf
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
get_dense (dl_iso_inv xf) = Rep_lifted_distrib_lattice_top xf

goal (1 subgoal):
 1. dl_iso (dl_iso_inv xf) = xf
[PROOF STEP]
by (simp add: Rep_lifted_distrib_lattice_top_inverse)
[PROOF STATE]
proof (state)
this:
dl_iso (dl_iso_inv xf) = xf

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dl_iso:
  "bounded_lattice_top_isomorphism dl_iso"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bounded_lattice_top_isomorphism dl_iso
[PROOF STEP]
proof (intro conjI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. sup_homomorphism dl_iso
 2. inf_homomorphism dl_iso
 3. top_homomorphism dl_iso
 4. bij dl_iso
[PROOF STEP]
have "get_dense top = (\<lambda>f::('a,'b) phi . top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get_dense top = (\<lambda>f. top)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. get_dense top f = top
[PROOF STEP]
fix f :: "('a,'b) phi"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. get_dense top f = top
[PROOF STEP]
have "Rep_lifted_pair (Rep_dense top) f = (top,Abs_filter {top})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense top) f = (top, Filters.filter.Abs_filter {top})
[PROOF STEP]
by (simp add: top_dense.rep_eq top_lifted_pair.rep_eq)
[PROOF STATE]
proof (state)
this:
Rep_lifted_pair (Rep_dense top) f = (top, Filters.filter.Abs_filter {top})

goal (1 subgoal):
 1. \<And>f. get_dense top f = top
[PROOF STEP]
hence "up_filter (get_dense top f) = Abs_filter {top}"
[PROOF STATE]
proof (prove)
using this:
Rep_lifted_pair (Rep_dense top) f = (top, Filters.filter.Abs_filter {top})

goal (1 subgoal):
 1. up_filter (get_dense top f) = Filters.filter.Abs_filter {top}
[PROOF STEP]
by (metis prod.inject get_dense_char)
[PROOF STATE]
proof (state)
this:
up_filter (get_dense top f) = Filters.filter.Abs_filter {top}

goal (1 subgoal):
 1. \<And>f. get_dense top f = top
[PROOF STEP]
hence "Rep_filter (up_filter (get_dense top f)) = {top}"
[PROOF STATE]
proof (prove)
using this:
up_filter (get_dense top f) = Filters.filter.Abs_filter {top}

goal (1 subgoal):
 1. Filters.filter.Rep_filter (up_filter (get_dense top f)) = {top}
[PROOF STEP]
by (metis bot_filter.abs_eq bot_filter.rep_eq)
[PROOF STATE]
proof (state)
this:
Filters.filter.Rep_filter (up_filter (get_dense top f)) = {top}

goal (1 subgoal):
 1. \<And>f. get_dense top f = top
[PROOF STEP]
thus "get_dense top f = top"
[PROOF STATE]
proof (prove)
using this:
Filters.filter.Rep_filter (up_filter (get_dense top f)) = {top}

goal (1 subgoal):
 1. get_dense top f = top
[PROOF STEP]
by (metis self_in_upset singletonD Abs_filter_inverse mem_Collect_eq up_filter)
[PROOF STATE]
proof (state)
this:
get_dense top f = top

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
get_dense top = (\<lambda>f. top)

goal (4 subgoals):
 1. sup_homomorphism dl_iso
 2. inf_homomorphism dl_iso
 3. top_homomorphism dl_iso
 4. bij dl_iso
[PROOF STEP]
thus "Abs_lifted_distrib_lattice_top (get_dense top::('a,'b) phi \<Rightarrow> 'b) = top"
[PROOF STATE]
proof (prove)
using this:
get_dense top = (\<lambda>f. top)

goal (1 subgoal):
 1. top_homomorphism dl_iso
[PROOF STEP]
by (metis top_lifted_distrib_lattice_top_def)
[PROOF STATE]
proof (state)
this:
top_homomorphism dl_iso

goal (3 subgoals):
 1. sup_homomorphism dl_iso
 2. inf_homomorphism dl_iso
 3. bij dl_iso
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. sup_homomorphism dl_iso
 2. inf_homomorphism dl_iso
 3. bij dl_iso
[PROOF STEP]
show "\<forall>pf qf :: ('a,'b) lifted_pair dense . Abs_lifted_distrib_lattice_top (get_dense (pf \<squnion> qf)) = Abs_lifted_distrib_lattice_top (get_dense pf) \<squnion> Abs_lifted_distrib_lattice_top (get_dense qf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_homomorphism dl_iso
[PROOF STEP]
proof (intro allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pf qf. dl_iso (pf \<squnion> qf) = dl_iso pf \<squnion> dl_iso qf
[PROOF STEP]
fix pf qf :: "('a,'b) lifted_pair dense"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pf qf. dl_iso (pf \<squnion> qf) = dl_iso pf \<squnion> dl_iso qf
[PROOF STEP]
have 1: "Abs_lifted_distrib_lattice_top (get_dense pf) \<squnion> Abs_lifted_distrib_lattice_top (get_dense qf) = Abs_lifted_distrib_lattice_top (\<lambda>f . get_dense pf f \<squnion> get_dense qf f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dl_iso pf \<squnion> dl_iso qf = Abs_lifted_distrib_lattice_top (\<lambda>f. get_dense pf f \<squnion> get_dense qf f)
[PROOF STEP]
by (simp add: eq_onp_same_args sup_lifted_distrib_lattice_top.abs_eq)
[PROOF STATE]
proof (state)
this:
dl_iso pf \<squnion> dl_iso qf = Abs_lifted_distrib_lattice_top (\<lambda>f. get_dense pf f \<squnion> get_dense qf f)

goal (1 subgoal):
 1. \<And>pf qf. dl_iso (pf \<squnion> qf) = dl_iso pf \<squnion> dl_iso qf
[PROOF STEP]
have "(\<lambda>f . get_dense (pf \<squnion> qf) f) = (\<lambda>f . get_dense pf f \<squnion> get_dense qf f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get_dense (pf \<squnion> qf) = (\<lambda>f. get_dense pf f \<squnion> get_dense qf f)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. get_dense (pf \<squnion> qf) f = get_dense pf f \<squnion> get_dense qf f
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. get_dense (pf \<squnion> qf) f = get_dense pf f \<squnion> get_dense qf f
[PROOF STEP]
have "(top,up_filter (get_dense (pf \<squnion> qf) f)) = Rep_lifted_pair (Rep_dense (pf \<squnion> qf)) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (top, up_filter (get_dense (pf \<squnion> qf) f)) = Rep_lifted_pair (Rep_dense (pf \<squnion> qf)) f
[PROOF STEP]
by (metis get_dense_char)
[PROOF STATE]
proof (state)
this:
(top, up_filter (get_dense (pf \<squnion> qf) f)) = Rep_lifted_pair (Rep_dense (pf \<squnion> qf)) f

goal (1 subgoal):
 1. \<And>f. get_dense (pf \<squnion> qf) f = get_dense pf f \<squnion> get_dense qf f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(top, up_filter (get_dense (pf \<squnion> qf) f)) = Rep_lifted_pair (Rep_dense (pf \<squnion> qf)) f

goal (1 subgoal):
 1. \<And>f. get_dense (pf \<squnion> qf) f = get_dense pf f \<squnion> get_dense qf f
[PROOF STEP]
have "... = triple.pairs_sup (Rep_lifted_pair (Rep_dense pf) f) (Rep_lifted_pair (Rep_dense qf) f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense (pf \<squnion> qf)) f = triple.pairs_sup (Rep_lifted_pair (Rep_dense pf) f) (Rep_lifted_pair (Rep_dense qf) f)
[PROOF STEP]
by (simp add: sup_lifted_pair.rep_eq sup_dense.rep_eq)
[PROOF STATE]
proof (state)
this:
Rep_lifted_pair (Rep_dense (pf \<squnion> qf)) f = triple.pairs_sup (Rep_lifted_pair (Rep_dense pf) f) (Rep_lifted_pair (Rep_dense qf) f)

goal (1 subgoal):
 1. \<And>f. get_dense (pf \<squnion> qf) f = get_dense pf f \<squnion> get_dense qf f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Rep_lifted_pair (Rep_dense (pf \<squnion> qf)) f = triple.pairs_sup (Rep_lifted_pair (Rep_dense pf) f) (Rep_lifted_pair (Rep_dense qf) f)

goal (1 subgoal):
 1. \<And>f. get_dense (pf \<squnion> qf) f = get_dense pf f \<squnion> get_dense qf f
[PROOF STEP]
have "... = triple.pairs_sup (top,up_filter (get_dense pf f)) (top,up_filter (get_dense qf f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple.pairs_sup (Rep_lifted_pair (Rep_dense pf) f) (Rep_lifted_pair (Rep_dense qf) f) = triple.pairs_sup (top, up_filter (get_dense pf f)) (top, up_filter (get_dense qf f))
[PROOF STEP]
by (metis get_dense_char)
[PROOF STATE]
proof (state)
this:
triple.pairs_sup (Rep_lifted_pair (Rep_dense pf) f) (Rep_lifted_pair (Rep_dense qf) f) = triple.pairs_sup (top, up_filter (get_dense pf f)) (top, up_filter (get_dense qf f))

goal (1 subgoal):
 1. \<And>f. get_dense (pf \<squnion> qf) f = get_dense pf f \<squnion> get_dense qf f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
triple.pairs_sup (Rep_lifted_pair (Rep_dense pf) f) (Rep_lifted_pair (Rep_dense qf) f) = triple.pairs_sup (top, up_filter (get_dense pf f)) (top, up_filter (get_dense qf f))

goal (1 subgoal):
 1. \<And>f. get_dense (pf \<squnion> qf) f = get_dense pf f \<squnion> get_dense qf f
[PROOF STEP]
have "... = (top,up_filter (get_dense pf f) \<sqinter> up_filter (get_dense qf f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple.pairs_sup (top, up_filter (get_dense pf f)) (top, up_filter (get_dense qf f)) = (top, up_filter (get_dense pf f) \<sqinter> up_filter (get_dense qf f))
[PROOF STEP]
by (metis (no_types, lifting) calculation prod.simps(1) simp_phi triple.pairs_sup.simps triple_def)
[PROOF STATE]
proof (state)
this:
triple.pairs_sup (top, up_filter (get_dense pf f)) (top, up_filter (get_dense qf f)) = (top, up_filter (get_dense pf f) \<sqinter> up_filter (get_dense qf f))

goal (1 subgoal):
 1. \<And>f. get_dense (pf \<squnion> qf) f = get_dense pf f \<squnion> get_dense qf f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
triple.pairs_sup (top, up_filter (get_dense pf f)) (top, up_filter (get_dense qf f)) = (top, up_filter (get_dense pf f) \<sqinter> up_filter (get_dense qf f))

goal (1 subgoal):
 1. \<And>f. get_dense (pf \<squnion> qf) f = get_dense pf f \<squnion> get_dense qf f
[PROOF STEP]
have "... = (top,up_filter (get_dense pf f \<squnion> get_dense qf f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (top, up_filter (get_dense pf f) \<sqinter> up_filter (get_dense qf f)) = (top, up_filter (get_dense pf f \<squnion> get_dense qf f))
[PROOF STEP]
by (metis up_filter_dist_sup)
[PROOF STATE]
proof (state)
this:
(top, up_filter (get_dense pf f) \<sqinter> up_filter (get_dense qf f)) = (top, up_filter (get_dense pf f \<squnion> get_dense qf f))

goal (1 subgoal):
 1. \<And>f. get_dense (pf \<squnion> qf) f = get_dense pf f \<squnion> get_dense qf f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(top, up_filter (get_dense (pf \<squnion> qf) f)) = (top, up_filter (get_dense pf f \<squnion> get_dense qf f))
[PROOF STEP]
show "get_dense (pf \<squnion> qf) f = get_dense pf f \<squnion> get_dense qf f"
[PROOF STATE]
proof (prove)
using this:
(top, up_filter (get_dense (pf \<squnion> qf) f)) = (top, up_filter (get_dense pf f \<squnion> get_dense qf f))

goal (1 subgoal):
 1. get_dense (pf \<squnion> qf) f = get_dense pf f \<squnion> get_dense qf f
[PROOF STEP]
using up_filter_injective
[PROOF STATE]
proof (prove)
using this:
(top, up_filter (get_dense (pf \<squnion> qf) f)) = (top, up_filter (get_dense pf f \<squnion> get_dense qf f))
up_filter ?x = up_filter ?y \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. get_dense (pf \<squnion> qf) f = get_dense pf f \<squnion> get_dense qf f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
get_dense (pf \<squnion> qf) f = get_dense pf f \<squnion> get_dense qf f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
get_dense (pf \<squnion> qf) = (\<lambda>f. get_dense pf f \<squnion> get_dense qf f)

goal (1 subgoal):
 1. \<And>pf qf. dl_iso (pf \<squnion> qf) = dl_iso pf \<squnion> dl_iso qf
[PROOF STEP]
thus "Abs_lifted_distrib_lattice_top (get_dense (pf \<squnion> qf)) = Abs_lifted_distrib_lattice_top (get_dense pf) \<squnion> Abs_lifted_distrib_lattice_top (get_dense qf)"
[PROOF STATE]
proof (prove)
using this:
get_dense (pf \<squnion> qf) = (\<lambda>f. get_dense pf f \<squnion> get_dense qf f)

goal (1 subgoal):
 1. dl_iso (pf \<squnion> qf) = dl_iso pf \<squnion> dl_iso qf
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
get_dense (pf \<squnion> qf) = (\<lambda>f. get_dense pf f \<squnion> get_dense qf f)
dl_iso pf \<squnion> dl_iso qf = Abs_lifted_distrib_lattice_top (\<lambda>f. get_dense pf f \<squnion> get_dense qf f)

goal (1 subgoal):
 1. dl_iso (pf \<squnion> qf) = dl_iso pf \<squnion> dl_iso qf
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
dl_iso (pf \<squnion> qf) = dl_iso pf \<squnion> dl_iso qf

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

goal (2 subgoals):
 1. inf_homomorphism dl_iso
 2. bij dl_iso
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. inf_homomorphism dl_iso
 2. bij dl_iso
[PROOF STEP]
show "\<forall>pf qf :: ('a,'b) lifted_pair dense . Abs_lifted_distrib_lattice_top (get_dense (pf \<sqinter> qf)) = Abs_lifted_distrib_lattice_top (get_dense pf) \<sqinter> Abs_lifted_distrib_lattice_top (get_dense qf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inf_homomorphism dl_iso
[PROOF STEP]
proof (intro allI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pf qf. dl_iso (pf \<sqinter> qf) = dl_iso pf \<sqinter> dl_iso qf
[PROOF STEP]
fix pf qf :: "('a,'b) lifted_pair dense"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>pf qf. dl_iso (pf \<sqinter> qf) = dl_iso pf \<sqinter> dl_iso qf
[PROOF STEP]
have 1: "Abs_lifted_distrib_lattice_top (get_dense pf) \<sqinter> Abs_lifted_distrib_lattice_top (get_dense qf) = Abs_lifted_distrib_lattice_top (\<lambda>f . get_dense pf f \<sqinter> get_dense qf f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dl_iso pf \<sqinter> dl_iso qf = Abs_lifted_distrib_lattice_top (\<lambda>f. get_dense pf f \<sqinter> get_dense qf f)
[PROOF STEP]
by (simp add: eq_onp_same_args inf_lifted_distrib_lattice_top.abs_eq)
[PROOF STATE]
proof (state)
this:
dl_iso pf \<sqinter> dl_iso qf = Abs_lifted_distrib_lattice_top (\<lambda>f. get_dense pf f \<sqinter> get_dense qf f)

goal (1 subgoal):
 1. \<And>pf qf. dl_iso (pf \<sqinter> qf) = dl_iso pf \<sqinter> dl_iso qf
[PROOF STEP]
have "(\<lambda>f . get_dense (pf \<sqinter> qf) f) = (\<lambda>f . get_dense pf f \<sqinter> get_dense qf f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get_dense (pf \<sqinter> qf) = (\<lambda>f. get_dense pf f \<sqinter> get_dense qf f)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. get_dense (pf \<sqinter> qf) f = get_dense pf f \<sqinter> get_dense qf f
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. get_dense (pf \<sqinter> qf) f = get_dense pf f \<sqinter> get_dense qf f
[PROOF STEP]
have "(top,up_filter (get_dense (pf \<sqinter> qf) f)) = Rep_lifted_pair (Rep_dense (pf \<sqinter> qf)) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (top, up_filter (get_dense (pf \<sqinter> qf) f)) = Rep_lifted_pair (Rep_dense (pf \<sqinter> qf)) f
[PROOF STEP]
by (metis get_dense_char)
[PROOF STATE]
proof (state)
this:
(top, up_filter (get_dense (pf \<sqinter> qf) f)) = Rep_lifted_pair (Rep_dense (pf \<sqinter> qf)) f

goal (1 subgoal):
 1. \<And>f. get_dense (pf \<sqinter> qf) f = get_dense pf f \<sqinter> get_dense qf f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(top, up_filter (get_dense (pf \<sqinter> qf) f)) = Rep_lifted_pair (Rep_dense (pf \<sqinter> qf)) f

goal (1 subgoal):
 1. \<And>f. get_dense (pf \<sqinter> qf) f = get_dense pf f \<sqinter> get_dense qf f
[PROOF STEP]
have "... = triple.pairs_inf (Rep_lifted_pair (Rep_dense pf) f) (Rep_lifted_pair (Rep_dense qf) f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense (pf \<sqinter> qf)) f = triple.pairs_inf (Rep_lifted_pair (Rep_dense pf) f) (Rep_lifted_pair (Rep_dense qf) f)
[PROOF STEP]
by (simp add: inf_lifted_pair.rep_eq inf_dense.rep_eq)
[PROOF STATE]
proof (state)
this:
Rep_lifted_pair (Rep_dense (pf \<sqinter> qf)) f = triple.pairs_inf (Rep_lifted_pair (Rep_dense pf) f) (Rep_lifted_pair (Rep_dense qf) f)

goal (1 subgoal):
 1. \<And>f. get_dense (pf \<sqinter> qf) f = get_dense pf f \<sqinter> get_dense qf f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Rep_lifted_pair (Rep_dense (pf \<sqinter> qf)) f = triple.pairs_inf (Rep_lifted_pair (Rep_dense pf) f) (Rep_lifted_pair (Rep_dense qf) f)

goal (1 subgoal):
 1. \<And>f. get_dense (pf \<sqinter> qf) f = get_dense pf f \<sqinter> get_dense qf f
[PROOF STEP]
have "... = triple.pairs_inf (top,up_filter (get_dense pf f)) (top,up_filter (get_dense qf f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple.pairs_inf (Rep_lifted_pair (Rep_dense pf) f) (Rep_lifted_pair (Rep_dense qf) f) = triple.pairs_inf (top, up_filter (get_dense pf f)) (top, up_filter (get_dense qf f))
[PROOF STEP]
by (metis get_dense_char)
[PROOF STATE]
proof (state)
this:
triple.pairs_inf (Rep_lifted_pair (Rep_dense pf) f) (Rep_lifted_pair (Rep_dense qf) f) = triple.pairs_inf (top, up_filter (get_dense pf f)) (top, up_filter (get_dense qf f))

goal (1 subgoal):
 1. \<And>f. get_dense (pf \<sqinter> qf) f = get_dense pf f \<sqinter> get_dense qf f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
triple.pairs_inf (Rep_lifted_pair (Rep_dense pf) f) (Rep_lifted_pair (Rep_dense qf) f) = triple.pairs_inf (top, up_filter (get_dense pf f)) (top, up_filter (get_dense qf f))

goal (1 subgoal):
 1. \<And>f. get_dense (pf \<sqinter> qf) f = get_dense pf f \<sqinter> get_dense qf f
[PROOF STEP]
have "... = (top,up_filter (get_dense pf f) \<squnion> up_filter (get_dense qf f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple.pairs_inf (top, up_filter (get_dense pf f)) (top, up_filter (get_dense qf f)) = (top, up_filter (get_dense pf f) \<squnion> up_filter (get_dense qf f))
[PROOF STEP]
by (metis (no_types, lifting) calculation prod.simps(1) simp_phi triple.pairs_inf.simps triple_def)
[PROOF STATE]
proof (state)
this:
triple.pairs_inf (top, up_filter (get_dense pf f)) (top, up_filter (get_dense qf f)) = (top, up_filter (get_dense pf f) \<squnion> up_filter (get_dense qf f))

goal (1 subgoal):
 1. \<And>f. get_dense (pf \<sqinter> qf) f = get_dense pf f \<sqinter> get_dense qf f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
triple.pairs_inf (top, up_filter (get_dense pf f)) (top, up_filter (get_dense qf f)) = (top, up_filter (get_dense pf f) \<squnion> up_filter (get_dense qf f))

goal (1 subgoal):
 1. \<And>f. get_dense (pf \<sqinter> qf) f = get_dense pf f \<sqinter> get_dense qf f
[PROOF STEP]
have "... = (top,up_filter (get_dense pf f \<sqinter> get_dense qf f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (top, up_filter (get_dense pf f) \<squnion> up_filter (get_dense qf f)) = (top, up_filter (get_dense pf f \<sqinter> get_dense qf f))
[PROOF STEP]
by (metis up_filter_dist_inf)
[PROOF STATE]
proof (state)
this:
(top, up_filter (get_dense pf f) \<squnion> up_filter (get_dense qf f)) = (top, up_filter (get_dense pf f \<sqinter> get_dense qf f))

goal (1 subgoal):
 1. \<And>f. get_dense (pf \<sqinter> qf) f = get_dense pf f \<sqinter> get_dense qf f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(top, up_filter (get_dense (pf \<sqinter> qf) f)) = (top, up_filter (get_dense pf f \<sqinter> get_dense qf f))
[PROOF STEP]
show "get_dense (pf \<sqinter> qf) f = get_dense pf f \<sqinter> get_dense qf f"
[PROOF STATE]
proof (prove)
using this:
(top, up_filter (get_dense (pf \<sqinter> qf) f)) = (top, up_filter (get_dense pf f \<sqinter> get_dense qf f))

goal (1 subgoal):
 1. get_dense (pf \<sqinter> qf) f = get_dense pf f \<sqinter> get_dense qf f
[PROOF STEP]
using up_filter_injective
[PROOF STATE]
proof (prove)
using this:
(top, up_filter (get_dense (pf \<sqinter> qf) f)) = (top, up_filter (get_dense pf f \<sqinter> get_dense qf f))
up_filter ?x = up_filter ?y \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. get_dense (pf \<sqinter> qf) f = get_dense pf f \<sqinter> get_dense qf f
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
get_dense (pf \<sqinter> qf) f = get_dense pf f \<sqinter> get_dense qf f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
get_dense (pf \<sqinter> qf) = (\<lambda>f. get_dense pf f \<sqinter> get_dense qf f)

goal (1 subgoal):
 1. \<And>pf qf. dl_iso (pf \<sqinter> qf) = dl_iso pf \<sqinter> dl_iso qf
[PROOF STEP]
thus "Abs_lifted_distrib_lattice_top (get_dense (pf \<sqinter> qf)) = Abs_lifted_distrib_lattice_top (get_dense pf) \<sqinter> Abs_lifted_distrib_lattice_top (get_dense qf)"
[PROOF STATE]
proof (prove)
using this:
get_dense (pf \<sqinter> qf) = (\<lambda>f. get_dense pf f \<sqinter> get_dense qf f)

goal (1 subgoal):
 1. dl_iso (pf \<sqinter> qf) = dl_iso pf \<sqinter> dl_iso qf
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
get_dense (pf \<sqinter> qf) = (\<lambda>f. get_dense pf f \<sqinter> get_dense qf f)
dl_iso pf \<sqinter> dl_iso qf = Abs_lifted_distrib_lattice_top (\<lambda>f. get_dense pf f \<sqinter> get_dense qf f)

goal (1 subgoal):
 1. dl_iso (pf \<sqinter> qf) = dl_iso pf \<sqinter> dl_iso qf
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
dl_iso (pf \<sqinter> qf) = dl_iso pf \<sqinter> dl_iso qf

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

goal (1 subgoal):
 1. bij dl_iso
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. bij dl_iso
[PROOF STEP]
show "bij dl_iso"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij dl_iso
[PROOF STEP]
by (rule invertible_bij[where g=dl_iso_inv]) (simp_all add: dl_iso_left_invertible dl_iso_right_invertible)
[PROOF STATE]
proof (state)
this:
bij dl_iso

goal:
No subgoals!
[PROOF STEP]
qed