[STATEMENT]
lemma phi_iso_filter:
  "filter ((\<lambda>qf::('a::non_trivial_boolean_algebra,'b::distrib_lattice_top) lifted_pair dense . Rep_lifted_distrib_lattice_top (dl_iso qf) f) ` Rep_filter (stone_phi pf))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ord_class.filter ((\<lambda>qf. Rep_lifted_distrib_lattice_top (dl_iso qf) f) ` Filters.filter.Rep_filter (stone_phi pf))
[PROOF STEP]
proof (rule filter_map_filter)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. mono (\<lambda>qf. Rep_lifted_distrib_lattice_top (dl_iso qf) f)
 2. \<forall>x y. Rep_lifted_distrib_lattice_top (dl_iso x) f \<le> y \<longrightarrow> (\<exists>z\<ge>x. y = Rep_lifted_distrib_lattice_top (dl_iso z) f)
[PROOF STEP]
show "mono (\<lambda>qf::('a::non_trivial_boolean_algebra,'b::distrib_lattice_top) lifted_pair dense . Rep_lifted_distrib_lattice_top (dl_iso qf) f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mono (\<lambda>qf. Rep_lifted_distrib_lattice_top (dl_iso qf) f)
[PROOF STEP]
by (metis (no_types, lifting) mono_def dl_iso le_iff_sup sup_lifted_distrib_lattice_top.rep_eq)
[PROOF STATE]
proof (state)
this:
mono (\<lambda>qf. Rep_lifted_distrib_lattice_top (dl_iso qf) f)

goal (1 subgoal):
 1. \<forall>x y. Rep_lifted_distrib_lattice_top (dl_iso x) f \<le> y \<longrightarrow> (\<exists>z\<ge>x. y = Rep_lifted_distrib_lattice_top (dl_iso z) f)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x y. Rep_lifted_distrib_lattice_top (dl_iso x) f \<le> y \<longrightarrow> (\<exists>z\<ge>x. y = Rep_lifted_distrib_lattice_top (dl_iso z) f)
[PROOF STEP]
show "\<forall>qf y . Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<longrightarrow> (\<exists>rf . qf \<le> rf \<and> y = Rep_lifted_distrib_lattice_top (dl_iso rf) f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<longrightarrow> (\<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f)
[PROOF STEP]
proof (intro allI, rule impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
fix qf :: "('a,'b) lifted_pair dense"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
fix y :: 'b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
assume 1: "Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y"
[PROOF STATE]
proof (state)
this:
Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
let ?rf = "Abs_dense (Abs_lifted_pair (\<lambda>g . if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g))"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
have 2: "\<forall>g . (if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g) \<in> triple.pairs (Rep_phi g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>g. (if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g) \<in> triple.pairs (Rep_phi g)
[PROOF STEP]
by (metis Abs_lifted_distrib_lattice_top_inverse dl_iso_inv_lifted_pair mem_Collect_eq simp_lifted_pair)
[PROOF STATE]
proof (state)
this:
\<forall>g. (if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g) \<in> triple.pairs (Rep_phi g)

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
hence "-Abs_lifted_pair (\<lambda>g . if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g) = Abs_lifted_pair (\<lambda>g . triple.pairs_uminus (Rep_phi g) (if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g))"
[PROOF STATE]
proof (prove)
using this:
\<forall>g. (if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g) \<in> triple.pairs (Rep_phi g)

goal (1 subgoal):
 1. - Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g) = Abs_lifted_pair (\<lambda>g. triple.pairs_uminus (Rep_phi g) (if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))
[PROOF STEP]
by (simp add: eq_onp_def uminus_lifted_pair.abs_eq)
[PROOF STATE]
proof (state)
this:
- Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g) = Abs_lifted_pair (\<lambda>g. triple.pairs_uminus (Rep_phi g) (if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g) = Abs_lifted_pair (\<lambda>g. triple.pairs_uminus (Rep_phi g) (if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>g . if g = f then triple.pairs_uminus (Rep_phi g) (top,up_filter y) else triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_dense qf) g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>g. triple.pairs_uminus (Rep_phi g) (if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) = Abs_lifted_pair (\<lambda>g. if g = f then triple.pairs_uminus (Rep_phi g) (top, up_filter y) else triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_dense qf) g))
[PROOF STEP]
by (simp add: if_distrib)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>g. triple.pairs_uminus (Rep_phi g) (if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) = Abs_lifted_pair (\<lambda>g. if g = f then triple.pairs_uminus (Rep_phi g) (top, up_filter y) else triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_dense qf) g))

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>g. triple.pairs_uminus (Rep_phi g) (if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) = Abs_lifted_pair (\<lambda>g. if g = f then triple.pairs_uminus (Rep_phi g) (top, up_filter y) else triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_dense qf) g))

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>g . if g = f then (bot,top) else triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_dense qf) g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>g. if g = f then triple.pairs_uminus (Rep_phi g) (top, up_filter y) else triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_dense qf) g)) = Abs_lifted_pair (\<lambda>g. if g = f then (bot, top) else triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_dense qf) g))
[PROOF STEP]
by (subst triple.pairs_uminus.simps, simp add: triple_def, metis compl_top_eq simp_phi)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>g. if g = f then triple.pairs_uminus (Rep_phi g) (top, up_filter y) else triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_dense qf) g)) = Abs_lifted_pair (\<lambda>g. if g = f then (bot, top) else triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_dense qf) g))

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>g. if g = f then triple.pairs_uminus (Rep_phi g) (top, up_filter y) else triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_dense qf) g)) = Abs_lifted_pair (\<lambda>g. if g = f then (bot, top) else triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_dense qf) g))

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>g . if g = f then (bot,top) else (bot,top))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>g. if g = f then (bot, top) else triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_dense qf) g)) = Abs_lifted_pair (\<lambda>g. if g = f then (bot, top) else (bot, top))
[PROOF STEP]
by (metis bot_lifted_pair.rep_eq simp_dense top_filter.abs_eq uminus_lifted_pair.rep_eq)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>g. if g = f then (bot, top) else triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_dense qf) g)) = Abs_lifted_pair (\<lambda>g. if g = f then (bot, top) else (bot, top))

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>g. if g = f then (bot, top) else triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_dense qf) g)) = Abs_lifted_pair (\<lambda>g. if g = f then (bot, top) else (bot, top))

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
have "... = bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>g. if g = f then (bot, top) else (bot, top)) = bot
[PROOF STEP]
by (simp add: bot_lifted_pair.abs_eq top_filter.abs_eq)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>g. if g = f then (bot, top) else (bot, top)) = bot

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))
[PROOF STEP]
have 3: "Abs_lifted_pair (\<lambda>g . if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g) \<in> dense_elements"
[PROOF STATE]
proof (prove)
using this:
dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))

goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g) \<in> dense_elements
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g) \<in> dense_elements

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
hence "(top,up_filter (get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g . if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) f)) = Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g . if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) f"
[PROOF STATE]
proof (prove)
using this:
Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g) \<in> dense_elements

goal (1 subgoal):
 1. (top, up_filter (get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) f)) = Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) f
[PROOF STEP]
by (metis (mono_tags, lifting) get_dense_char)
[PROOF STATE]
proof (state)
this:
(top, up_filter (get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) f)) = Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) f

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(top, up_filter (get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) f)) = Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) f

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
have "... = Rep_lifted_pair (Abs_lifted_pair (\<lambda>g . if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) f = Rep_lifted_pair (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) f
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g) \<in> dense_elements

goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) f = Rep_lifted_pair (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) f
[PROOF STEP]
by (simp add: Abs_dense_inverse)
[PROOF STATE]
proof (state)
this:
Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) f = Rep_lifted_pair (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) f

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) f = Rep_lifted_pair (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) f

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
have "... = (top,up_filter y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_lifted_pair (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) f = (top, up_filter y)
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
\<forall>g. (if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g) \<in> triple.pairs (Rep_phi g)

goal (1 subgoal):
 1. Rep_lifted_pair (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) f = (top, up_filter y)
[PROOF STEP]
by (simp add: Abs_lifted_pair_inverse)
[PROOF STATE]
proof (state)
this:
Rep_lifted_pair (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) f = (top, up_filter y)

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(top, up_filter (get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) f)) = (top, up_filter y)
[PROOF STEP]
have "get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g . if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) f = y"
[PROOF STATE]
proof (prove)
using this:
(top, up_filter (get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) f)) = (top, up_filter y)

goal (1 subgoal):
 1. get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) f = y
[PROOF STEP]
using up_filter_injective
[PROOF STATE]
proof (prove)
using this:
(top, up_filter (get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) f)) = (top, up_filter y)
up_filter ?x = up_filter ?y \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) f = y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) f = y

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
hence 4: "Rep_lifted_distrib_lattice_top (dl_iso ?rf) f = y"
[PROOF STATE]
proof (prove)
using this:
get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) f = y

goal (1 subgoal):
 1. Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) f = y
[PROOF STEP]
by (simp add: Abs_lifted_distrib_lattice_top_inverse)
[PROOF STATE]
proof (state)
this:
Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) f = y

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) f = y

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
fix g
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
have "Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso ?rf) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g
[PROOF STEP]
proof (cases "g = f")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. g = f \<Longrightarrow> Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g
 2. g \<noteq> f \<Longrightarrow> Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g
[PROOF STEP]
assume "g = f"
[PROOF STATE]
proof (state)
this:
g = f

goal (2 subgoals):
 1. g = f \<Longrightarrow> Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g
 2. g \<noteq> f \<Longrightarrow> Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
g = f

goal (1 subgoal):
 1. Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g
[PROOF STEP]
using 1 4
[PROOF STATE]
proof (prove)
using this:
g = f
Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y
Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) f = y

goal (1 subgoal):
 1. Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g

goal (1 subgoal):
 1. g \<noteq> f \<Longrightarrow> Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g \<noteq> f \<Longrightarrow> Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g
[PROOF STEP]
assume 5: "g \<noteq> f"
[PROOF STATE]
proof (state)
this:
g \<noteq> f

goal (1 subgoal):
 1. g \<noteq> f \<Longrightarrow> Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g
[PROOF STEP]
have "(top,up_filter (get_dense ?rf g)) = Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g . if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (top, up_filter (get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) g)) = Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g
[PROOF STEP]
by (metis (mono_tags, lifting) get_dense_char)
[PROOF STATE]
proof (state)
this:
(top, up_filter (get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) g)) = Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g

goal (1 subgoal):
 1. g \<noteq> f \<Longrightarrow> Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(top, up_filter (get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) g)) = Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g

goal (1 subgoal):
 1. g \<noteq> f \<Longrightarrow> Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g
[PROOF STEP]
have "... = Rep_lifted_pair (Abs_lifted_pair (\<lambda>g . if g = f then (top,up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g = Rep_lifted_pair (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) g
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g) \<in> dense_elements

goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g = Rep_lifted_pair (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) g
[PROOF STEP]
by (simp add: Abs_dense_inverse)
[PROOF STATE]
proof (state)
this:
Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g = Rep_lifted_pair (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) g

goal (1 subgoal):
 1. g \<noteq> f \<Longrightarrow> Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g = Rep_lifted_pair (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) g

goal (1 subgoal):
 1. g \<noteq> f \<Longrightarrow> Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g
[PROOF STEP]
have "... = Rep_lifted_pair (Rep_dense qf) g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_lifted_pair (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) g = Rep_lifted_pair (Rep_dense qf) g
[PROOF STEP]
using 2 5
[PROOF STATE]
proof (prove)
using this:
\<forall>g. (if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g) \<in> triple.pairs (Rep_phi g)
g \<noteq> f

goal (1 subgoal):
 1. Rep_lifted_pair (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) g = Rep_lifted_pair (Rep_dense qf) g
[PROOF STEP]
by (simp add: Abs_lifted_pair_inverse)
[PROOF STATE]
proof (state)
this:
Rep_lifted_pair (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) g = Rep_lifted_pair (Rep_dense qf) g

goal (1 subgoal):
 1. g \<noteq> f \<Longrightarrow> Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Rep_lifted_pair (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)) g = Rep_lifted_pair (Rep_dense qf) g

goal (1 subgoal):
 1. g \<noteq> f \<Longrightarrow> Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g
[PROOF STEP]
have "... = (top,up_filter (get_dense qf g))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense qf) g = (top, up_filter (get_dense qf g))
[PROOF STEP]
using get_dense_char
[PROOF STATE]
proof (prove)
using this:
Rep_lifted_pair (Rep_dense ?pf) ?f = (top, up_filter (get_dense ?pf ?f))

goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense qf) g = (top, up_filter (get_dense qf g))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Rep_lifted_pair (Rep_dense qf) g = (top, up_filter (get_dense qf g))

goal (1 subgoal):
 1. g \<noteq> f \<Longrightarrow> Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(top, up_filter (get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) g)) = (top, up_filter (get_dense qf g))
[PROOF STEP]
have "get_dense ?rf g = get_dense qf g"
[PROOF STATE]
proof (prove)
using this:
(top, up_filter (get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) g)) = (top, up_filter (get_dense qf g))

goal (1 subgoal):
 1. get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) g = get_dense qf g
[PROOF STEP]
using up_filter_injective
[PROOF STATE]
proof (prove)
using this:
(top, up_filter (get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) g)) = (top, up_filter (get_dense qf g))
up_filter ?x = up_filter ?y \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) g = get_dense qf g
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) g = get_dense qf g

goal (1 subgoal):
 1. g \<noteq> f \<Longrightarrow> Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g
[PROOF STEP]
thus "Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso ?rf) g"
[PROOF STATE]
proof (prove)
using this:
get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))) g = get_dense qf g

goal (1 subgoal):
 1. Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g
[PROOF STEP]
by (simp add: Abs_lifted_distrib_lattice_top_inverse)
[PROOF STATE]
proof (state)
this:
Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Rep_lifted_distrib_lattice_top (dl_iso qf) g \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) g

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
Rep_lifted_distrib_lattice_top (dl_iso qf) ?g2 \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) ?g2

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
hence "Rep_lifted_distrib_lattice_top (dl_iso qf) \<le> Rep_lifted_distrib_lattice_top (dl_iso ?rf)"
[PROOF STATE]
proof (prove)
using this:
Rep_lifted_distrib_lattice_top (dl_iso qf) ?g2 \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) ?g2

goal (1 subgoal):
 1. Rep_lifted_distrib_lattice_top (dl_iso qf) \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))))
[PROOF STEP]
by (simp add: le_funI)
[PROOF STATE]
proof (state)
this:
Rep_lifted_distrib_lattice_top (dl_iso qf) \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))))

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
hence 6: "dl_iso qf \<le> dl_iso ?rf"
[PROOF STATE]
proof (prove)
using this:
Rep_lifted_distrib_lattice_top (dl_iso qf) \<le> Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))))

goal (1 subgoal):
 1. dl_iso qf \<le> dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))
[PROOF STEP]
by (simp add: le_funD less_eq_lifted_distrib_lattice_top.rep_eq)
[PROOF STATE]
proof (state)
this:
dl_iso qf \<le> dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
hence "qf \<le> ?rf"
[PROOF STATE]
proof (prove)
using this:
dl_iso qf \<le> dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))

goal (1 subgoal):
 1. qf \<le> Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))
[PROOF STEP]
by (metis (no_types, lifting) dl_iso sup_isomorphism_ord_isomorphism)
[PROOF STATE]
proof (state)
this:
qf \<le> Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))

goal (1 subgoal):
 1. \<And>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<Longrightarrow> \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
thus "\<exists>rf . qf \<le> rf \<and> y = Rep_lifted_distrib_lattice_top (dl_iso rf) f"
[PROOF STATE]
proof (prove)
using this:
qf \<le> Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))

goal (1 subgoal):
 1. \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
qf \<le> Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g))
Rep_lifted_distrib_lattice_top (dl_iso (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter y) else Rep_lifted_pair (Rep_dense qf) g)))) f = y

goal (1 subgoal):
 1. \<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>qf y. Rep_lifted_distrib_lattice_top (dl_iso qf) f \<le> y \<longrightarrow> (\<exists>rf\<ge>qf. y = Rep_lifted_distrib_lattice_top (dl_iso rf) f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma phi_iso:
  "Rep_phi f (Rep_lifted_boolean_algebra (ba_iso pf) f) = filter_map (\<lambda>qf::('a::non_trivial_boolean_algebra,'b::distrib_lattice_top) lifted_pair dense . Rep_lifted_distrib_lattice_top (dl_iso qf) f) (stone_phi pf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_phi f (Rep_lifted_boolean_algebra (ba_iso pf) f) = filter_map (\<lambda>qf. Rep_lifted_distrib_lattice_top (dl_iso qf) f) (stone_phi pf)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Rep_phi f (Rep_lifted_boolean_algebra (ba_iso pf) f) = filter_map (\<lambda>qf. Rep_lifted_distrib_lattice_top (dl_iso qf) f) (stone_phi pf)
[PROOF STEP]
let ?r = "Rep_phi f"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Rep_phi f (Rep_lifted_boolean_algebra (ba_iso pf) f) = filter_map (\<lambda>qf. Rep_lifted_distrib_lattice_top (dl_iso qf) f) (stone_phi pf)
[PROOF STEP]
let ?ppf = "\<lambda>g . triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Rep_phi f (Rep_lifted_boolean_algebra (ba_iso pf) f) = filter_map (\<lambda>qf. Rep_lifted_distrib_lattice_top (dl_iso qf) f) (stone_phi pf)
[PROOF STEP]
have 1: "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. Rep_phi f (Rep_lifted_boolean_algebra (ba_iso pf) f) = filter_map (\<lambda>qf. Rep_lifted_distrib_lattice_top (dl_iso qf) f) (stone_phi pf)
[PROOF STEP]
have 2: "Rep_filter (?r (fst (Rep_lifted_pair (Rep_regular pf) f))) \<subseteq> { z . \<exists>qf . -Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<subseteq> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
obtain x where 3: "x = fst (Rep_lifted_pair (Rep_regular pf) f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x = fst (Rep_lifted_pair (Rep_regular pf) f) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = fst (Rep_lifted_pair (Rep_regular pf) f)

goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
assume "z \<in> Rep_filter (?r (fst (Rep_lifted_pair (Rep_regular pf) f)))"
[PROOF STATE]
proof (state)
this:
z \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))

goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
hence "\<up>z \<subseteq> Rep_filter (?r x)"
[PROOF STATE]
proof (prove)
using this:
z \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))

goal (1 subgoal):
 1. \<up>z \<subseteq> Filters.filter.Rep_filter (Rep_phi f x)
[PROOF STEP]
using 3 filter_def
[PROOF STATE]
proof (prove)
using this:
z \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))
x = fst (Rep_lifted_pair (Rep_regular pf) f)
ord_class.filter ?F \<equiv> ?F \<noteq> {} \<and> (\<forall>x\<in>?F. \<forall>y\<in>?F. \<exists>z\<in>?F. z \<le> x \<and> z \<le> y) \<and> is_up_set ?F

goal (1 subgoal):
 1. \<up>z \<subseteq> Filters.filter.Rep_filter (Rep_phi f x)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<up>z \<subseteq> Filters.filter.Rep_filter (Rep_phi f x)

goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
hence 4: "up_filter z \<le> ?r x"
[PROOF STATE]
proof (prove)
using this:
\<up>z \<subseteq> Filters.filter.Rep_filter (Rep_phi f x)

goal (1 subgoal):
 1. up_filter z \<le> Rep_phi f x
[PROOF STEP]
by (metis Rep_filter_cases Rep_filter_inverse less_eq_filter.rep_eq mem_Collect_eq up_filter)
[PROOF STATE]
proof (state)
this:
up_filter z \<le> Rep_phi f x

goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
have 5: "\<forall>g . ?ppf g \<in> triple.pairs (Rep_phi g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>g. triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g) \<in> triple.pairs (Rep_phi g)
[PROOF STEP]
by (metis (no_types) simp_lifted_pair uminus_lifted_pair.rep_eq)
[PROOF STATE]
proof (state)
this:
\<forall>g. triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g) \<in> triple.pairs (Rep_phi g)

goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
let ?zf = "\<lambda>g . if g = f then (top,up_filter z) else triple.pairs_top"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
have 6: "\<forall>g . ?zf g \<in> triple.pairs (Rep_phi g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>g. (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})) \<in> triple.pairs (Rep_phi g)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>g. (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})) \<in> triple.pairs (Rep_phi g)
[PROOF STEP]
fix g :: "('a,'b) phi"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>g. (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})) \<in> triple.pairs (Rep_phi g)
[PROOF STEP]
have "triple (Rep_phi g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple (Rep_phi g)
[PROOF STEP]
by (simp add: triple_def)
[PROOF STATE]
proof (state)
this:
triple (Rep_phi g)

goal (1 subgoal):
 1. \<And>g. (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})) \<in> triple.pairs (Rep_phi g)
[PROOF STEP]
hence "(top,up_filter z) \<in> triple.pairs (Rep_phi g)"
[PROOF STATE]
proof (prove)
using this:
triple (Rep_phi g)

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

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

goal (1 subgoal):
 1. \<And>g. (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})) \<in> triple.pairs (Rep_phi g)
[PROOF STEP]
thus "?zf g \<in> triple.pairs (Rep_phi g)"
[PROOF STATE]
proof (prove)
using this:
(top, up_filter z) \<in> triple.pairs (Rep_phi g)

goal (1 subgoal):
 1. (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})) \<in> triple.pairs (Rep_phi g)
[PROOF STEP]
by (metis simp_lifted_pair top_lifted_pair.rep_eq)
[PROOF STATE]
proof (state)
this:
(if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})) \<in> triple.pairs (Rep_phi g)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>g. (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})) \<in> triple.pairs (Rep_phi g)

goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
hence "-Abs_lifted_pair ?zf = Abs_lifted_pair (\<lambda>g . triple.pairs_uminus (Rep_phi g) (?zf g))"
[PROOF STATE]
proof (prove)
using this:
\<forall>g. (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})) \<in> triple.pairs (Rep_phi g)

goal (1 subgoal):
 1. - Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})) = Abs_lifted_pair (\<lambda>g. triple.pairs_uminus (Rep_phi g) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})))
[PROOF STEP]
by (subst uminus_lifted_pair.abs_eq) (simp_all add: eq_onp_same_args)
[PROOF STATE]
proof (state)
this:
- Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})) = Abs_lifted_pair (\<lambda>g. triple.pairs_uminus (Rep_phi g) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})))

goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
- Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})) = Abs_lifted_pair (\<lambda>g. triple.pairs_uminus (Rep_phi g) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})))

goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>g . if g = f then triple.pairs_uminus (Rep_phi g) (top,up_filter z) else triple.pairs_uminus (Rep_phi g) triple.pairs_top)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>g. triple.pairs_uminus (Rep_phi g) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))) = Abs_lifted_pair (\<lambda>g. if g = f then triple.pairs_uminus (Rep_phi g) (top, up_filter z) else triple.pairs_uminus (Rep_phi g) (top, Filters.filter.Abs_filter {top}))
[PROOF STEP]
by (rule arg_cong[where f=Abs_lifted_pair]) auto
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>g. triple.pairs_uminus (Rep_phi g) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))) = Abs_lifted_pair (\<lambda>g. if g = f then triple.pairs_uminus (Rep_phi g) (top, up_filter z) else triple.pairs_uminus (Rep_phi g) (top, Filters.filter.Abs_filter {top}))

goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>g. triple.pairs_uminus (Rep_phi g) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))) = Abs_lifted_pair (\<lambda>g. if g = f then triple.pairs_uminus (Rep_phi g) (top, up_filter z) else triple.pairs_uminus (Rep_phi g) (top, Filters.filter.Abs_filter {top}))

goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
have "... = Abs_lifted_pair (\<lambda>g . triple.pairs_bot)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>g. if g = f then triple.pairs_uminus (Rep_phi g) (top, up_filter z) else triple.pairs_uminus (Rep_phi g) (top, Filters.filter.Abs_filter {top})) = Abs_lifted_pair (\<lambda>g. (bot, Filters.filter.Abs_filter UNIV))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
triple (Rep_phi f)

goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>g. if g = f then triple.pairs_uminus (Rep_phi g) (top, up_filter z) else triple.pairs_uminus (Rep_phi g) (top, Filters.filter.Abs_filter {top})) = Abs_lifted_pair (\<lambda>g. (bot, Filters.filter.Abs_filter UNIV))
[PROOF STEP]
by (metis bot_lifted_pair.rep_eq dense_closed_top top_lifted_pair.rep_eq triple.pairs_uminus.simps uminus_lifted_pair.rep_eq)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>g. if g = f then triple.pairs_uminus (Rep_phi g) (top, up_filter z) else triple.pairs_uminus (Rep_phi g) (top, Filters.filter.Abs_filter {top})) = Abs_lifted_pair (\<lambda>g. (bot, Filters.filter.Abs_filter UNIV))

goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
- Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})) = Abs_lifted_pair (\<lambda>g. (bot, Filters.filter.Abs_filter UNIV))
[PROOF STEP]
have 7: "Abs_lifted_pair ?zf \<in> dense_elements"
[PROOF STATE]
proof (prove)
using this:
- Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})) = Abs_lifted_pair (\<lambda>g. (bot, Filters.filter.Abs_filter UNIV))

goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})) \<in> dense_elements
[PROOF STEP]
by (simp add: bot_lifted_pair.abs_eq)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})) \<in> dense_elements

goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
let ?qf = "Abs_dense (Abs_lifted_pair ?zf)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
have "\<forall>g . triple.pairs_less_eq (?ppf g) (?zf g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>g. triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>g. triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
[PROOF STEP]
fix g
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>g. triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
[PROOF STEP]
show "triple.pairs_less_eq (?ppf g) (?zf g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
[PROOF STEP]
proof (cases "g = f")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. g = f \<Longrightarrow> triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
 2. g \<noteq> f \<Longrightarrow> triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
[PROOF STEP]
assume 8: "g = f"
[PROOF STATE]
proof (state)
this:
g = f

goal (2 subgoals):
 1. g = f \<Longrightarrow> triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
 2. g \<noteq> f \<Longrightarrow> triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
[PROOF STEP]
hence 9: "?ppf g = (-x,?r x)"
[PROOF STATE]
proof (prove)
using this:
g = f

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

goal (1 subgoal):
 1. triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g) = (- x, Rep_phi f x)
[PROOF STEP]
by (metis prod.collapse triple.pairs_uminus.simps)
[PROOF STATE]
proof (state)
this:
triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g) = (- x, Rep_phi f x)

goal (2 subgoals):
 1. g = f \<Longrightarrow> triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
 2. g \<noteq> f \<Longrightarrow> triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
[PROOF STEP]
have "triple.pairs_less_eq (-x,?r x) (top,up_filter z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple.pairs_less_eq (- x, Rep_phi f x) (top, up_filter z)
[PROOF STEP]
using 1 4
[PROOF STATE]
proof (prove)
using this:
triple (Rep_phi f)
up_filter z \<le> Rep_phi f x

goal (1 subgoal):
 1. triple.pairs_less_eq (- x, Rep_phi f x) (top, up_filter z)
[PROOF STEP]
by (meson inf.bot_least triple.pairs_less_eq.simps)
[PROOF STATE]
proof (state)
this:
triple.pairs_less_eq (- x, Rep_phi f x) (top, up_filter z)

goal (2 subgoals):
 1. g = f \<Longrightarrow> triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
 2. g \<noteq> f \<Longrightarrow> triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
triple.pairs_less_eq (- x, Rep_phi f x) (top, up_filter z)

goal (1 subgoal):
 1. triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
[PROOF STEP]
using 8 9
[PROOF STATE]
proof (prove)
using this:
triple.pairs_less_eq (- x, Rep_phi f x) (top, up_filter z)
g = f
triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g) = (- x, Rep_phi f x)

goal (1 subgoal):
 1. triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))

goal (1 subgoal):
 1. g \<noteq> f \<Longrightarrow> triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. g \<noteq> f \<Longrightarrow> triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
[PROOF STEP]
assume 10: "g \<noteq> f"
[PROOF STATE]
proof (state)
this:
g \<noteq> f

goal (1 subgoal):
 1. g \<noteq> f \<Longrightarrow> triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
[PROOF STEP]
have "triple.pairs_less_eq (?ppf g) triple.pairs_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (top, Filters.filter.Abs_filter {top})
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
triple (Rep_phi f)

goal (1 subgoal):
 1. triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (top, Filters.filter.Abs_filter {top})
[PROOF STEP]
by (metis (no_types, opaque_lifting) bot.extremum top_greatest prod.collapse triple_def triple.pairs_less_eq.simps triple.phi_bot)
[PROOF STATE]
proof (state)
this:
triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (top, Filters.filter.Abs_filter {top})

goal (1 subgoal):
 1. g \<noteq> f \<Longrightarrow> triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (top, Filters.filter.Abs_filter {top})

goal (1 subgoal):
 1. triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
[PROOF STEP]
using 10
[PROOF STATE]
proof (prove)
using this:
triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (top, Filters.filter.Abs_filter {top})
g \<noteq> f

goal (1 subgoal):
 1. triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>g. triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))

goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
hence "Abs_lifted_pair ?ppf \<le> Abs_lifted_pair ?zf"
[PROOF STATE]
proof (prove)
using this:
\<forall>g. triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))

goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>g. triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) \<le> Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
[PROOF STEP]
using 5 6
[PROOF STATE]
proof (prove)
using this:
\<forall>g. triple.pairs_less_eq (triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
\<forall>g. triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g) \<in> triple.pairs (Rep_phi g)
\<forall>g. (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})) \<in> triple.pairs (Rep_phi g)

goal (1 subgoal):
 1. Abs_lifted_pair (\<lambda>g. triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) \<le> Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
[PROOF STEP]
by (subst less_eq_lifted_pair.abs_eq) (simp_all add: eq_onp_same_args)
[PROOF STATE]
proof (state)
this:
Abs_lifted_pair (\<lambda>g. triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) \<le> Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))

goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
hence 11: "-Rep_regular pf \<le> Rep_dense ?qf"
[PROOF STATE]
proof (prove)
using this:
Abs_lifted_pair (\<lambda>g. triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) \<le> Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))

goal (1 subgoal):
 1. - Rep_regular pf \<le> Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))))
[PROOF STEP]
using 7
[PROOF STATE]
proof (prove)
using this:
Abs_lifted_pair (\<lambda>g. triple.pairs_uminus (Rep_phi g) (Rep_lifted_pair (Rep_regular pf) g)) \<le> Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))
Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})) \<in> dense_elements

goal (1 subgoal):
 1. - Rep_regular pf \<le> Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))))
[PROOF STEP]
by (simp add: uminus_lifted_pair_def Abs_dense_inverse)
[PROOF STATE]
proof (state)
this:
- Rep_regular pf \<le> Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))))

goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
have "(top,up_filter (get_dense ?qf f)) = Rep_lifted_pair (Rep_dense ?qf) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (top, up_filter (get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})))) f)) = Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))))) f
[PROOF STEP]
by (metis get_dense_char)
[PROOF STATE]
proof (state)
this:
(top, up_filter (get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})))) f)) = Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))))) f

goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(top, up_filter (get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})))) f)) = Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))))) f

goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
have "... = (top,up_filter z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))))) f = (top, up_filter z)
[PROOF STEP]
using 6 7 Abs_dense_inverse Abs_lifted_pair_inverse
[PROOF STATE]
proof (prove)
using this:
\<forall>g. (if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})) \<in> triple.pairs (Rep_phi g)
Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})) \<in> dense_elements
?y \<in> dense_elements \<Longrightarrow> Rep_dense (Abs_dense ?y) = ?y
?y \<in> {pf. \<forall>f. pf f \<in> triple.pairs (Rep_phi f)} \<Longrightarrow> Rep_lifted_pair (Abs_lifted_pair ?y) = ?y

goal (1 subgoal):
 1. Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))))) f = (top, up_filter z)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Rep_lifted_pair (Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))))) f = (top, up_filter z)

goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(top, up_filter (get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})))) f)) = (top, up_filter z)
[PROOF STEP]
have "z = get_dense ?qf f"
[PROOF STATE]
proof (prove)
using this:
(top, up_filter (get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})))) f)) = (top, up_filter z)

goal (1 subgoal):
 1. z = get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})))) f
[PROOF STEP]
using up_filter_injective
[PROOF STATE]
proof (prove)
using this:
(top, up_filter (get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})))) f)) = (top, up_filter z)
up_filter ?x = up_filter ?y \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. z = get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})))) f
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
z = get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})))) f

goal (1 subgoal):
 1. \<And>x. x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<Longrightarrow> x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
thus "z \<in> { z . \<exists>qf . -Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f }"
[PROOF STATE]
proof (prove)
using this:
z = get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})))) f

goal (1 subgoal):
 1. z \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
using 11
[PROOF STATE]
proof (prove)
using this:
z = get_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top})))) f
- Rep_regular pf \<le> Rep_dense (Abs_dense (Abs_lifted_pair (\<lambda>g. if g = f then (top, up_filter z) else (top, Filters.filter.Abs_filter {top}))))

goal (1 subgoal):
 1. z \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
z \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<subseteq> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}

goal (1 subgoal):
 1. Rep_phi f (Rep_lifted_boolean_algebra (ba_iso pf) f) = filter_map (\<lambda>qf. Rep_lifted_distrib_lattice_top (dl_iso qf) f) (stone_phi pf)
[PROOF STEP]
have 12: "Rep_filter (?r (fst (Rep_lifted_pair (Rep_regular pf) f))) \<supseteq> { z . \<exists>qf . -Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f} \<subseteq> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f} \<Longrightarrow> x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f} \<Longrightarrow> x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))
[PROOF STEP]
assume "z \<in> { z . \<exists>qf . -Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f }"
[PROOF STATE]
proof (state)
this:
z \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}

goal (1 subgoal):
 1. \<And>x. x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f} \<Longrightarrow> x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))
[PROOF STEP]
hence "\<exists>qf . -Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f"
[PROOF STATE]
proof (prove)
using this:
z \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}

goal (1 subgoal):
 1. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f

goal (1 subgoal):
 1. \<And>x. x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f} \<Longrightarrow> x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))
[PROOF STEP]
hence "triple.pairs_less_eq (Rep_lifted_pair (-Rep_regular pf) f) (top,up_filter z)"
[PROOF STATE]
proof (prove)
using this:
\<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f

goal (1 subgoal):
 1. triple.pairs_less_eq (Rep_lifted_pair (- Rep_regular pf) f) (top, up_filter z)
[PROOF STEP]
by (metis less_eq_lifted_pair.rep_eq get_dense_char)
[PROOF STATE]
proof (state)
this:
triple.pairs_less_eq (Rep_lifted_pair (- Rep_regular pf) f) (top, up_filter z)

goal (1 subgoal):
 1. \<And>x. x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f} \<Longrightarrow> x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))
[PROOF STEP]
hence "up_filter z \<le> snd (Rep_lifted_pair (-Rep_regular pf) f)"
[PROOF STATE]
proof (prove)
using this:
triple.pairs_less_eq (Rep_lifted_pair (- Rep_regular pf) f) (top, up_filter z)

goal (1 subgoal):
 1. up_filter z \<le> snd (Rep_lifted_pair (- Rep_regular pf) f)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
triple.pairs_less_eq (Rep_lifted_pair (- Rep_regular pf) f) (top, up_filter z)
triple (Rep_phi f)

goal (1 subgoal):
 1. up_filter z \<le> snd (Rep_lifted_pair (- Rep_regular pf) f)
[PROOF STEP]
by (metis (no_types, opaque_lifting) prod.collapse triple.pairs_less_eq.simps)
[PROOF STATE]
proof (state)
this:
up_filter z \<le> snd (Rep_lifted_pair (- Rep_regular pf) f)

goal (1 subgoal):
 1. \<And>x. x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f} \<Longrightarrow> x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
up_filter z \<le> snd (Rep_lifted_pair (- Rep_regular pf) f)

goal (1 subgoal):
 1. \<And>x. x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f} \<Longrightarrow> x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))
[PROOF STEP]
have "... = snd (?ppf f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (Rep_lifted_pair (- Rep_regular pf) f) = snd (triple.pairs_uminus (Rep_phi f) (Rep_lifted_pair (Rep_regular pf) f))
[PROOF STEP]
by (metis uminus_lifted_pair.rep_eq)
[PROOF STATE]
proof (state)
this:
snd (Rep_lifted_pair (- Rep_regular pf) f) = snd (triple.pairs_uminus (Rep_phi f) (Rep_lifted_pair (Rep_regular pf) f))

goal (1 subgoal):
 1. \<And>x. x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f} \<Longrightarrow> x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
snd (Rep_lifted_pair (- Rep_regular pf) f) = snd (triple.pairs_uminus (Rep_phi f) (Rep_lifted_pair (Rep_regular pf) f))

goal (1 subgoal):
 1. \<And>x. x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f} \<Longrightarrow> x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))
[PROOF STEP]
have "... = ?r (fst (Rep_lifted_pair (Rep_regular pf) f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (triple.pairs_uminus (Rep_phi f) (Rep_lifted_pair (Rep_regular pf) f)) = Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
triple (Rep_phi f)

goal (1 subgoal):
 1. snd (triple.pairs_uminus (Rep_phi f) (Rep_lifted_pair (Rep_regular pf) f)) = Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))
[PROOF STEP]
by (metis (no_types) prod.collapse prod.inject triple.pairs_uminus.simps)
[PROOF STATE]
proof (state)
this:
snd (triple.pairs_uminus (Rep_phi f) (Rep_lifted_pair (Rep_regular pf) f)) = Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))

goal (1 subgoal):
 1. \<And>x. x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f} \<Longrightarrow> x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
up_filter z \<le> Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))
[PROOF STEP]
have "Rep_filter (up_filter z) \<subseteq> Rep_filter (?r (fst (Rep_lifted_pair (Rep_regular pf) f)))"
[PROOF STATE]
proof (prove)
using this:
up_filter z \<le> Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))

goal (1 subgoal):
 1. Filters.filter.Rep_filter (up_filter z) \<subseteq> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))
[PROOF STEP]
by (simp add: less_eq_filter.rep_eq)
[PROOF STATE]
proof (state)
this:
Filters.filter.Rep_filter (up_filter z) \<subseteq> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))

goal (1 subgoal):
 1. \<And>x. x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f} \<Longrightarrow> x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))
[PROOF STEP]
hence "\<up>z \<subseteq> Rep_filter (?r (fst (Rep_lifted_pair (Rep_regular pf) f)))"
[PROOF STATE]
proof (prove)
using this:
Filters.filter.Rep_filter (up_filter z) \<subseteq> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))

goal (1 subgoal):
 1. \<up>z \<subseteq> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))
[PROOF STEP]
by (metis Abs_filter_inverse mem_Collect_eq up_filter)
[PROOF STATE]
proof (state)
this:
\<up>z \<subseteq> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))

goal (1 subgoal):
 1. \<And>x. x \<in> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f} \<Longrightarrow> x \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))
[PROOF STEP]
thus "z \<in> Rep_filter (?r (fst (Rep_lifted_pair (Rep_regular pf) f)))"
[PROOF STATE]
proof (prove)
using this:
\<up>z \<subseteq> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))

goal (1 subgoal):
 1. z \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
z \<in> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f} \<subseteq> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))

goal (1 subgoal):
 1. Rep_phi f (Rep_lifted_boolean_algebra (ba_iso pf) f) = filter_map (\<lambda>qf. Rep_lifted_distrib_lattice_top (dl_iso qf) f) (stone_phi pf)
[PROOF STEP]
have 13: "\<forall>qf\<in>Rep_filter (stone_phi pf) . Rep_lifted_distrib_lattice_top (Abs_lifted_distrib_lattice_top (get_dense qf)) f = get_dense qf f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>qf\<in>Filters.filter.Rep_filter (stone_phi pf). Rep_lifted_distrib_lattice_top (dl_iso qf) f = get_dense qf f
[PROOF STEP]
by (metis Abs_lifted_distrib_lattice_top_inverse UNIV_I UNIV_def)
[PROOF STATE]
proof (state)
this:
\<forall>qf\<in>Filters.filter.Rep_filter (stone_phi pf). Rep_lifted_distrib_lattice_top (dl_iso qf) f = get_dense qf f

goal (1 subgoal):
 1. Rep_phi f (Rep_lifted_boolean_algebra (ba_iso pf) f) = filter_map (\<lambda>qf. Rep_lifted_distrib_lattice_top (dl_iso qf) f) (stone_phi pf)
[PROOF STEP]
have "Rep_filter (?r (fst (Rep_lifted_pair (Rep_regular pf) f))) = { z . \<exists>qf\<in>stone_phi_base pf . z = get_dense qf f }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) = {z. \<exists>qf\<in>stone_phi_base pf. z = get_dense qf f}
[PROOF STEP]
using 2 12
[PROOF STATE]
proof (prove)
using this:
Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) \<subseteq> {z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f}
{z. \<exists>qf. - Rep_regular pf \<le> Rep_dense qf \<and> z = get_dense qf f} \<subseteq> Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)))

goal (1 subgoal):
 1. Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) = {z. \<exists>qf\<in>stone_phi_base pf. z = get_dense qf f}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) = {z. \<exists>qf\<in>stone_phi_base pf. z = get_dense qf f}

goal (1 subgoal):
 1. Rep_phi f (Rep_lifted_boolean_algebra (ba_iso pf) f) = filter_map (\<lambda>qf. Rep_lifted_distrib_lattice_top (dl_iso qf) f) (stone_phi pf)
[PROOF STEP]
hence "?r (fst (Rep_lifted_pair (Rep_regular pf) f)) = Abs_filter { z . \<exists>qf\<in>stone_phi_base pf . z = get_dense qf f }"
[PROOF STATE]
proof (prove)
using this:
Filters.filter.Rep_filter (Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f))) = {z. \<exists>qf\<in>stone_phi_base pf. z = get_dense qf f}

goal (1 subgoal):
 1. Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)) = Filters.filter.Abs_filter {z. \<exists>qf\<in>stone_phi_base pf. z = get_dense qf f}
[PROOF STEP]
by (metis Rep_filter_inverse)
[PROOF STATE]
proof (state)
this:
Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)) = Filters.filter.Abs_filter {z. \<exists>qf\<in>stone_phi_base pf. z = get_dense qf f}

goal (1 subgoal):
 1. Rep_phi f (Rep_lifted_boolean_algebra (ba_iso pf) f) = filter_map (\<lambda>qf. Rep_lifted_distrib_lattice_top (dl_iso qf) f) (stone_phi pf)
[PROOF STEP]
hence "?r (Rep_lifted_boolean_algebra (ba_iso pf) f) = Abs_filter { z . \<exists>qf\<in>Rep_filter (stone_phi pf) . z = Rep_lifted_distrib_lattice_top (dl_iso qf) f }"
[PROOF STATE]
proof (prove)
using this:
Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)) = Filters.filter.Abs_filter {z. \<exists>qf\<in>stone_phi_base pf. z = get_dense qf f}

goal (1 subgoal):
 1. Rep_phi f (Rep_lifted_boolean_algebra (ba_iso pf) f) = Filters.filter.Abs_filter {z. \<exists>qf\<in>Filters.filter.Rep_filter (stone_phi pf). z = Rep_lifted_distrib_lattice_top (dl_iso qf) f}
[PROOF STEP]
using 13
[PROOF STATE]
proof (prove)
using this:
Rep_phi f (fst (Rep_lifted_pair (Rep_regular pf) f)) = Filters.filter.Abs_filter {z. \<exists>qf\<in>stone_phi_base pf. z = get_dense qf f}
\<forall>qf\<in>Filters.filter.Rep_filter (stone_phi pf). Rep_lifted_distrib_lattice_top (dl_iso qf) f = get_dense qf f

goal (1 subgoal):
 1. Rep_phi f (Rep_lifted_boolean_algebra (ba_iso pf) f) = Filters.filter.Abs_filter {z. \<exists>qf\<in>Filters.filter.Rep_filter (stone_phi pf). z = Rep_lifted_distrib_lattice_top (dl_iso qf) f}
[PROOF STEP]
by (simp add: Abs_filter_inverse stone_phi_base_filter stone_phi_def Abs_lifted_boolean_algebra_inverse)
[PROOF STATE]
proof (state)
this:
Rep_phi f (Rep_lifted_boolean_algebra (ba_iso pf) f) = Filters.filter.Abs_filter {z. \<exists>qf\<in>Filters.filter.Rep_filter (stone_phi pf). z = Rep_lifted_distrib_lattice_top (dl_iso qf) f}

goal (1 subgoal):
 1. Rep_phi f (Rep_lifted_boolean_algebra (ba_iso pf) f) = filter_map (\<lambda>qf. Rep_lifted_distrib_lattice_top (dl_iso qf) f) (stone_phi pf)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Rep_phi f (Rep_lifted_boolean_algebra (ba_iso pf) f) = Filters.filter.Abs_filter {z. \<exists>qf\<in>Filters.filter.Rep_filter (stone_phi pf). z = Rep_lifted_distrib_lattice_top (dl_iso qf) f}

goal (1 subgoal):
 1. Rep_phi f (Rep_lifted_boolean_algebra (ba_iso pf) f) = filter_map (\<lambda>qf. Rep_lifted_distrib_lattice_top (dl_iso qf) f) (stone_phi pf)
[PROOF STEP]
by (simp add: image_def)
[PROOF STATE]
proof (state)
this:
Rep_phi f (Rep_lifted_boolean_algebra (ba_iso pf) f) = filter_map (\<lambda>qf. Rep_lifted_distrib_lattice_top (dl_iso qf) f) (stone_phi pf)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Sigma_transfer[transfer_rule]:
  assumes [transfer_rule]: "right_total A"
  shows
    "(rel_set A ===> (A ===> rel_set B) ===> rel_set (rel_prod A B))
      Sigma Sigma"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set A ===> (A ===> rel_set B) ===> rel_set (rel_prod A B)) Sigma Sigma
[PROOF STEP]
unfolding Sigma_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (rel_set A ===> (A ===> rel_set B) ===> rel_set (rel_prod A B)) (\<lambda>A B. \<Union>x\<in>A. \<Union>y\<in>B x. {(x, y)}) (\<lambda>A B. \<Union>x\<in>A. \<Union>y\<in>B x. {(x, y)})
[PROOF STEP]
by transfer_prover


[STATEMENT]
lemma insert_body_set_ins [simp]:
  shows  "set (insert_body xs e) = insert e (set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (insert_body xs e) = insert e (set xs)
[PROOF STEP]
by (induction xs, auto)


[STATEMENT]
lemma insert_rga_set_ins:
  assumes "i \<in> set xs"
  shows "set (insert_rga xs (oid, Some i)) = insert oid (set xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (insert_rga xs (oid, Some i)) = insert oid (set xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<in> set xs

goal (1 subgoal):
 1. set (insert_rga xs (oid, Some i)) = insert oid (set xs)
[PROOF STEP]
by (induction xs, auto)


[STATEMENT]
lemma insert_body_commutes:
  shows "insert_body (insert_body xs e1) e2 = insert_body (insert_body xs e2) e1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_body (insert_body xs e1) e2 = insert_body (insert_body xs e2) e1
[PROOF STEP]
by (induction xs, auto)


[STATEMENT]
lemma insert_rga_insert_body_commute:
  assumes "i2 \<noteq> Some e1"
  shows "insert_rga (insert_body xs e1) (e2, i2) = insert_body (insert_rga xs (e2, i2)) e1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_rga (insert_body xs e1) (e2, i2) = insert_body (insert_rga xs (e2, i2)) e1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i2 \<noteq> Some e1

goal (1 subgoal):
 1. insert_rga (insert_body xs e1) (e2, i2) = insert_body (insert_rga xs (e2, i2)) e1
[PROOF STEP]
by (induction xs; cases i2) (auto simp add: insert_body_commutes)


[STATEMENT]
lemma insert_rga_None_commutes:
  assumes "i2 \<noteq> Some e1"
  shows "insert_rga (insert_rga xs (e1, None)) (e2, i2  ) =
         insert_rga (insert_rga xs (e2, i2  )) (e1, None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_rga (insert_rga xs (e1, None)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, None)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i2 \<noteq> Some e1

goal (1 subgoal):
 1. insert_rga (insert_rga xs (e1, None)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, None)
[PROOF STEP]
by (induction xs; cases i2) (auto simp add: insert_body_commutes)


[STATEMENT]
lemma insert_rga_nonexistent:
  assumes "i \<notin> set xs"
  shows "insert_rga xs (e, Some i) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_rga xs (e, Some i) = xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<notin> set xs

goal (1 subgoal):
 1. insert_rga xs (e, Some i) = xs
[PROOF STEP]
by (induction xs, auto)


[STATEMENT]
lemma insert_rga_Some_commutes:
  assumes "i1 \<in> set xs" and "i2 \<in> set xs"
    and "e1 \<noteq> i2" and "e2 \<noteq> i1"
  shows "insert_rga (insert_rga xs (e1, Some i1)) (e2, Some i2) =
         insert_rga (insert_rga xs (e2, Some i2)) (e1, Some i1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_rga (insert_rga xs (e1, Some i1)) (e2, Some i2) = insert_rga (insert_rga xs (e2, Some i2)) (e1, Some i1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i1 \<in> set xs
i2 \<in> set xs
e1 \<noteq> i2
e2 \<noteq> i1

goal (1 subgoal):
 1. insert_rga (insert_rga xs (e1, Some i1)) (e2, Some i2) = insert_rga (insert_rga xs (e2, Some i2)) (e1, Some i1)
[PROOF STEP]
proof (induction xs, simp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>i1 \<in> set xs; i2 \<in> set xs; e1 \<noteq> i2; e2 \<noteq> i1\<rbrakk> \<Longrightarrow> insert_rga (insert_rga xs (e1, Some i1)) (e2, Some i2) = insert_rga (insert_rga xs (e2, Some i2)) (e1, Some i1); i1 \<in> set (a # xs); i2 \<in> set (a # xs); e1 \<noteq> i2; e2 \<noteq> i1\<rbrakk> \<Longrightarrow> insert_rga (insert_rga (a # xs) (e1, Some i1)) (e2, Some i2) = insert_rga (insert_rga (a # xs) (e2, Some i2)) (e1, Some i1)
[PROOF STEP]
case (Cons a xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i1 \<in> set xs; i2 \<in> set xs; e1 \<noteq> i2; e2 \<noteq> i1\<rbrakk> \<Longrightarrow> insert_rga (insert_rga xs (e1, Some i1)) (e2, Some i2) = insert_rga (insert_rga xs (e2, Some i2)) (e1, Some i1)
i1 \<in> set (a # xs)
i2 \<in> set (a # xs)
e1 \<noteq> i2
e2 \<noteq> i1

goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrakk>i1 \<in> set xs; i2 \<in> set xs; e1 \<noteq> i2; e2 \<noteq> i1\<rbrakk> \<Longrightarrow> insert_rga (insert_rga xs (e1, Some i1)) (e2, Some i2) = insert_rga (insert_rga xs (e2, Some i2)) (e1, Some i1); i1 \<in> set (a # xs); i2 \<in> set (a # xs); e1 \<noteq> i2; e2 \<noteq> i1\<rbrakk> \<Longrightarrow> insert_rga (insert_rga (a # xs) (e1, Some i1)) (e2, Some i2) = insert_rga (insert_rga (a # xs) (e2, Some i2)) (e1, Some i1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i1 \<in> set xs; i2 \<in> set xs; e1 \<noteq> i2; e2 \<noteq> i1\<rbrakk> \<Longrightarrow> insert_rga (insert_rga xs (e1, Some i1)) (e2, Some i2) = insert_rga (insert_rga xs (e2, Some i2)) (e1, Some i1)
i1 \<in> set (a # xs)
i2 \<in> set (a # xs)
e1 \<noteq> i2
e2 \<noteq> i1
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i1 \<in> set xs; i2 \<in> set xs; e1 \<noteq> i2; e2 \<noteq> i1\<rbrakk> \<Longrightarrow> insert_rga (insert_rga xs (e1, Some i1)) (e2, Some i2) = insert_rga (insert_rga xs (e2, Some i2)) (e1, Some i1)
i1 \<in> set (a # xs)
i2 \<in> set (a # xs)
e1 \<noteq> i2
e2 \<noteq> i1

goal (1 subgoal):
 1. insert_rga (insert_rga (a # xs) (e1, Some i1)) (e2, Some i2) = insert_rga (insert_rga (a # xs) (e2, Some i2)) (e1, Some i1)
[PROOF STEP]
by (cases "a = i1"; cases "a = i2";
        auto simp add: insert_body_commutes insert_rga_insert_body_commute)
[PROOF STATE]
proof (state)
this:
insert_rga (insert_rga (a # xs) (e1, Some i1)) (e2, Some i2) = insert_rga (insert_rga (a # xs) (e2, Some i2)) (e1, Some i1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma insert_rga_commutes:
  assumes "i2 \<noteq> Some e1" and "i1 \<noteq> Some e2"
  shows "insert_rga (insert_rga xs (e1, i1)) (e2, i2) =
         insert_rga (insert_rga xs (e2, i2)) (e1, i1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
proof(cases i1)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i1 = None \<Longrightarrow> insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
 2. \<And>a. i1 = Some a \<Longrightarrow> insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
i1 = None

goal (2 subgoals):
 1. i1 = None \<Longrightarrow> insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
 2. \<And>a. i1 = Some a \<Longrightarrow> insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i1 = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i1 = None

goal (1 subgoal):
 1. insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
using assms(1) insert_rga_None_commutes
[PROOF STATE]
proof (prove)
using this:
i1 = None
i2 \<noteq> Some e1
?i2.0 \<noteq> Some ?e1.0 \<Longrightarrow> insert_rga (insert_rga ?xs (?e1.0, None)) (?e2.0, ?i2.0) = insert_rga (insert_rga ?xs (?e2.0, ?i2.0)) (?e1.0, None)

goal (1 subgoal):
 1. insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
by (cases i2, fastforce, blast)
[PROOF STATE]
proof (state)
this:
insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)

goal (1 subgoal):
 1. \<And>a. i1 = Some a \<Longrightarrow> insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. i1 = Some a \<Longrightarrow> insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
case some_r1: (Some r1)
[PROOF STATE]
proof (state)
this:
i1 = Some r1

goal (1 subgoal):
 1. \<And>a. i1 = Some a \<Longrightarrow> insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i1 = Some r1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i1 = Some r1

goal (1 subgoal):
 1. insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
proof(cases i2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>i1 = Some r1; i2 = None\<rbrakk> \<Longrightarrow> insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
 2. \<And>a. \<lbrakk>i1 = Some r1; i2 = Some a\<rbrakk> \<Longrightarrow> insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
i2 = None

goal (2 subgoals):
 1. \<lbrakk>i1 = Some r1; i2 = None\<rbrakk> \<Longrightarrow> insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
 2. \<And>a. \<lbrakk>i1 = Some r1; i2 = Some a\<rbrakk> \<Longrightarrow> insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i2 = None
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i2 = None

goal (1 subgoal):
 1. insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
using assms(2) insert_rga_None_commutes
[PROOF STATE]
proof (prove)
using this:
i2 = None
i1 \<noteq> Some e2
?i2.0 \<noteq> Some ?e1.0 \<Longrightarrow> insert_rga (insert_rga ?xs (?e1.0, None)) (?e2.0, ?i2.0) = insert_rga (insert_rga ?xs (?e2.0, ?i2.0)) (?e1.0, None)

goal (1 subgoal):
 1. insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)

goal (1 subgoal):
 1. \<And>a. \<lbrakk>i1 = Some r1; i2 = Some a\<rbrakk> \<Longrightarrow> insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>i1 = Some r1; i2 = Some a\<rbrakk> \<Longrightarrow> insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
case some_r2: (Some r2)
[PROOF STATE]
proof (state)
this:
i2 = Some r2

goal (1 subgoal):
 1. \<And>a. \<lbrakk>i1 = Some r1; i2 = Some a\<rbrakk> \<Longrightarrow> insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i2 = Some r2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
i2 = Some r2

goal (1 subgoal):
 1. insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
proof(cases "r1 \<in> set xs \<and> r2 \<in> set xs")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>i2 = Some r2; r1 \<in> set xs \<and> r2 \<in> set xs\<rbrakk> \<Longrightarrow> insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
 2. \<lbrakk>i2 = Some r2; \<not> (r1 \<in> set xs \<and> r2 \<in> set xs)\<rbrakk> \<Longrightarrow> insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
r1 \<in> set xs \<and> r2 \<in> set xs

goal (2 subgoals):
 1. \<lbrakk>i2 = Some r2; r1 \<in> set xs \<and> r2 \<in> set xs\<rbrakk> \<Longrightarrow> insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
 2. \<lbrakk>i2 = Some r2; \<not> (r1 \<in> set xs \<and> r2 \<in> set xs)\<rbrakk> \<Longrightarrow> insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
r1 \<in> set xs \<and> r2 \<in> set xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
r1 \<in> set xs \<and> r2 \<in> set xs

goal (1 subgoal):
 1. insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
using assms some_r1 some_r2
[PROOF STATE]
proof (prove)
using this:
r1 \<in> set xs \<and> r2 \<in> set xs
i2 \<noteq> Some e1
i1 \<noteq> Some e2
i1 = Some r1
i2 = Some r2

goal (1 subgoal):
 1. insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
by (simp add: insert_rga_Some_commutes)
[PROOF STATE]
proof (state)
this:
insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)

goal (1 subgoal):
 1. \<lbrakk>i2 = Some r2; \<not> (r1 \<in> set xs \<and> r2 \<in> set xs)\<rbrakk> \<Longrightarrow> insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>i2 = Some r2; \<not> (r1 \<in> set xs \<and> r2 \<in> set xs)\<rbrakk> \<Longrightarrow> insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> (r1 \<in> set xs \<and> r2 \<in> set xs)

goal (1 subgoal):
 1. \<lbrakk>i2 = Some r2; \<not> (r1 \<in> set xs \<and> r2 \<in> set xs)\<rbrakk> \<Longrightarrow> insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> (r1 \<in> set xs \<and> r2 \<in> set xs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> (r1 \<in> set xs \<and> r2 \<in> set xs)

goal (1 subgoal):
 1. insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
using assms some_r1 some_r2
[PROOF STATE]
proof (prove)
using this:
\<not> (r1 \<in> set xs \<and> r2 \<in> set xs)
i2 \<noteq> Some e1
i1 \<noteq> Some e2
i1 = Some r1
i2 = Some r2

goal (1 subgoal):
 1. insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)
[PROOF STEP]
by (metis insert_iff insert_rga_nonexistent insert_rga_set_ins)
[PROOF STATE]
proof (state)
this:
insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
insert_rga (insert_rga xs (e1, i1)) (e2, i2) = insert_rga (insert_rga xs (e2, i2)) (e1, i1)

goal:
No subgoals!
[PROOF STEP]
qed