[STATEMENT]
lemma is_iso_arr_is_iso_dghm:
  assumes "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>"
    and "\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>"
    and "\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> = dghm_id \<BB>"
  shows "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
proof(intro is_iso_dghmI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 2. v11 (\<FF>\<lparr>ObjMap\<rparr>)
 3. v11 (\<FF>\<lparr>ArrMap\<rparr>)
 4. \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>
 5. \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
interpret L: is_dghm \<alpha> \<BB> \<AA> \<GG>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 2. v11 (\<FF>\<lparr>ObjMap\<rparr>)
 3. v11 (\<FF>\<lparr>ArrMap\<rparr>)
 4. \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>
 5. \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
interpret R: is_dghm \<alpha> \<AA> \<BB> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 2. v11 (\<FF>\<lparr>ObjMap\<rparr>)
 3. v11 (\<FF>\<lparr>ArrMap\<rparr>)
 4. \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>
 5. \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
show "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (4 subgoals):
 1. v11 (\<FF>\<lparr>ObjMap\<rparr>)
 2. v11 (\<FF>\<lparr>ArrMap\<rparr>)
 3. \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>
 4. \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
show "v11 (\<FF>\<lparr>ObjMap\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v11 (\<FF>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
proof(rule R.ObjMap.vsv_valeq_v11I)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; y \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; \<FF>\<lparr>ObjMap\<rparr>\<lparr>x\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>y\<rparr>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; y \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; \<FF>\<lparr>ObjMap\<rparr>\<lparr>x\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>y\<rparr>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume prems[simp]:
      "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" "b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" "\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; y \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; \<FF>\<lparr>ObjMap\<rparr>\<lparr>x\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>y\<rparr>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
from assms(1,2)
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
have "(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
by (simp add: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; y \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; \<FF>\<lparr>ObjMap\<rparr>\<lparr>x\<rparr> = \<FF>\<lparr>ObjMap\<rparr>\<lparr>y\<rparr>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
show "a = b"
[PROOF STATE]
proof (prove)
using this:
(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>

goal (1 subgoal):
 1. a = b
[PROOF STEP]
by (simp add: assms(3) dghm_id_components)
[PROOF STATE]
proof (state)
this:
a = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v11 (\<FF>\<lparr>ObjMap\<rparr>)

goal (3 subgoals):
 1. v11 (\<FF>\<lparr>ArrMap\<rparr>)
 2. \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>
 3. \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
show "v11 (\<FF>\<lparr>ArrMap\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v11 (\<FF>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
proof(rule R.ArrMap.vsv_valeq_v11I)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; y \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; \<FF>\<lparr>ArrMap\<rparr>\<lparr>x\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>y\<rparr>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; y \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; \<FF>\<lparr>ArrMap\<rparr>\<lparr>x\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>y\<rparr>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
assume prems[simp]:
      "a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>" "b \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>" "\<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>b\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
b \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
\<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>b\<rparr>

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; y \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; \<FF>\<lparr>ArrMap\<rparr>\<lparr>x\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>y\<rparr>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
b \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
\<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
have "\<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
b \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
\<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>b\<rparr>

goal (1 subgoal):
 1. \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
\<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; y \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; \<FF>\<lparr>ArrMap\<rparr>\<lparr>x\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>y\<rparr>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
with R.dghm_ArrMap_vsv L.dghm_ArrMap_vsv R.dghm_ArrMap_vrange
[PROOF STATE]
proof (chain)
picking this:
vsv (\<FF>\<lparr>ArrMap\<rparr>)
vsv (\<GG>\<lparr>ArrMap\<rparr>)
\<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
\<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
have
      "(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>b\<rparr>"
[PROOF STATE]
proof (prove)
using this:
vsv (\<FF>\<lparr>ArrMap\<rparr>)
vsv (\<GG>\<lparr>ArrMap\<rparr>)
\<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
\<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
unfolding dghm_comp_components
[PROOF STATE]
proof (prove)
using this:
vsv (\<FF>\<lparr>ArrMap\<rparr>)
vsv (\<GG>\<lparr>ArrMap\<rparr>)
\<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
\<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<GG>\<lparr>ArrMap\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr>)\<lparr>a\<rparr> = (\<GG>\<lparr>ArrMap\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr>)\<lparr>b\<rparr>
[PROOF STEP]
by (simp add: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>b\<rparr>

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; y \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>; \<FF>\<lparr>ArrMap\<rparr>\<lparr>x\<rparr> = \<FF>\<lparr>ArrMap\<rparr>\<lparr>y\<rparr>\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
show "a = b"
[PROOF STATE]
proof (prove)
using this:
(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>b\<rparr>

goal (1 subgoal):
 1. a = b
[PROOF STEP]
by (simp add: assms(3) dghm_id_components)
[PROOF STATE]
proof (state)
this:
a = b

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
v11 (\<FF>\<lparr>ArrMap\<rparr>)

goal (2 subgoals):
 1. \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>
 2. \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
show "\<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
proof(intro vsubset_antisym vsubsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
 2. \<And>x. x \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
from R.dghm_ObjMap_vrange
[PROOF STATE]
proof (chain)
picking this:
\<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
show "a \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) \<Longrightarrow> a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>" for a
[PROOF STATE]
proof (prove)
using this:
\<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) \<Longrightarrow> a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) \<Longrightarrow> ?a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
assume prems: "a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
have a_def[symmetric]: "(\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = a"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = a
[PROOF STEP]
unfolding assms(4) dghm_id_components
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. vid_on (\<BB>\<lparr>Obj\<rparr>)\<lparr>a\<rparr> = a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a = (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
show "a \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
by (subst a_def)
        (
          cs_concl cs_shallow
            cs_intro: V_cs_intros dg_cs_intros cs_simp: dg_cs_simps
        )
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
show "\<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
proof(intro vsubset_antisym vsubsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
 2. \<And>x. x \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
from R.dghm_ArrMap_vrange
[PROOF STATE]
proof (chain)
picking this:
\<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
show "a \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) \<Longrightarrow> a \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>" for a
[PROOF STATE]
proof (prove)
using this:
\<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) \<Longrightarrow> a \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) \<Longrightarrow> ?a \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
assume prems: "a \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
have a_def[symmetric]: "(\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = a"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = a
[PROOF STEP]
unfolding assms(4) dghm_id_components
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. vid_on (\<BB>\<lparr>Arr\<rparr>)\<lparr>a\<rparr> = a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
a = (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr> \<Longrightarrow> x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
a = (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "a \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
a = (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
by (subst a_def)
        (
          cs_concl cs_shallow
            cs_intro: V_cs_intros dg_cs_intros cs_simp: dg_cs_simps
        )
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = \<BB>\<lparr>Arr\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_iso_dghm_is_iso_arr:
  assumes "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>"
  shows [dghm_cs_intros]: "inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>"
    and [dghm_cs_simps]: "inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>"
    and [dghm_cs_simps]: "\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> = dghm_id \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA> &&& inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA> &&& \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> = dghm_id \<BB>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>
 2. inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>
 3. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> = dghm_id \<BB>
[PROOF STEP]
let ?\<GG> = \<open>inv_dghm \<FF>\<close>
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>
 2. inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>
 3. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> = dghm_id \<BB>
[PROOF STEP]
interpret is_iso_dghm \<alpha> \<AA> \<BB> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>
 2. inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>
 3. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> = dghm_id \<BB>
[PROOF STEP]
show \<GG>: "?\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
proof(intro is_iso_dghmI is_dghmI, unfold dghm_cs_simps)
[PROOF STATE]
proof (state)
goal (17 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (inv_dghm \<FF>)
 3. digraph \<alpha> \<BB>
 4. digraph \<alpha> \<AA>
 5. vcard (inv_dghm \<FF>) = 4\<^sub>\<nat>
 6. \<FF>\<lparr>HomCod\<rparr> = \<BB>
 7. \<FF>\<lparr>HomDom\<rparr> = \<AA>
 8. vsv (inv_dghm \<FF>\<lparr>ObjMap\<rparr>)
 9. vsv (inv_dghm \<FF>\<lparr>ArrMap\<rparr>)
 10. \<BB>\<lparr>Obj\<rparr> = \<BB>\<lparr>Obj\<rparr>
A total of 17 subgoals...
[PROOF STEP]
show "vfsequence (inv_dghm \<FF>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (inv_dghm \<FF>)
[PROOF STEP]
unfolding inv_dghm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [(\<FF>\<lparr>ObjMap\<rparr>)\<inverse>\<^sub>\<circ>, (\<FF>\<lparr>ArrMap\<rparr>)\<inverse>\<^sub>\<circ>, \<FF>\<lparr>HomCod\<rparr>, \<FF>\<lparr>HomDom\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vfsequence (inv_dghm \<FF>)

goal (16 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<BB>
 3. digraph \<alpha> \<AA>
 4. vcard (inv_dghm \<FF>) = 4\<^sub>\<nat>
 5. \<FF>\<lparr>HomCod\<rparr> = \<BB>
 6. \<FF>\<lparr>HomDom\<rparr> = \<AA>
 7. vsv (inv_dghm \<FF>\<lparr>ObjMap\<rparr>)
 8. vsv (inv_dghm \<FF>\<lparr>ArrMap\<rparr>)
 9. \<BB>\<lparr>Obj\<rparr> = \<BB>\<lparr>Obj\<rparr>
 10. \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
A total of 16 subgoals...
[PROOF STEP]
show "vcard (inv_dghm \<FF>) = 4\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (inv_dghm \<FF>) = 4\<^sub>\<nat>
[PROOF STEP]
unfolding inv_dghm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [(\<FF>\<lparr>ObjMap\<rparr>)\<inverse>\<^sub>\<circ>, (\<FF>\<lparr>ArrMap\<rparr>)\<inverse>\<^sub>\<circ>, \<FF>\<lparr>HomCod\<rparr>, \<FF>\<lparr>HomDom\<rparr>]\<^sub>\<circ> = 4\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (inv_dghm \<FF>) = 4\<^sub>\<nat>

goal (15 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<BB>
 3. digraph \<alpha> \<AA>
 4. \<FF>\<lparr>HomCod\<rparr> = \<BB>
 5. \<FF>\<lparr>HomDom\<rparr> = \<AA>
 6. vsv (inv_dghm \<FF>\<lparr>ObjMap\<rparr>)
 7. vsv (inv_dghm \<FF>\<lparr>ArrMap\<rparr>)
 8. \<BB>\<lparr>Obj\<rparr> = \<BB>\<lparr>Obj\<rparr>
 9. \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
 10. \<BB>\<lparr>Arr\<rparr> = \<BB>\<lparr>Arr\<rparr>
A total of 15 subgoals...
[PROOF STEP]
show "inv_dghm \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : inv_dghm \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> inv_dghm \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>"
      if "f : a \<mapsto>\<^bsub>\<BB>\<^esub> b" for a b f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_dghm \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : inv_dghm \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> inv_dghm \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<BB>\<^esub> b

goal (1 subgoal):
 1. inv_dghm \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : inv_dghm \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> inv_dghm \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
by
        (
          intro iso_dghm_HomDom_is_arr_conv,
          use nothing in \<open>unfold inv_dghm_components\<close>
        )
        (
          cs_concl
            cs_simp: V_cs_simps dghm_cs_simps dg_cs_simps
            cs_intro: dg_cs_intros V_cs_intros
        )+
[PROOF STATE]
proof (state)
this:
?f : ?a \<mapsto>\<^bsub>\<BB>\<^esub> ?b \<Longrightarrow> inv_dghm \<FF>\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr> : inv_dghm \<FF>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr> \<mapsto>\<^bsub>\<AA>\<^esub> inv_dghm \<FF>\<lparr>ObjMap\<rparr>\<lparr>?b\<rparr>

goal (14 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<BB>
 3. digraph \<alpha> \<AA>
 4. \<FF>\<lparr>HomCod\<rparr> = \<BB>
 5. \<FF>\<lparr>HomDom\<rparr> = \<AA>
 6. vsv (inv_dghm \<FF>\<lparr>ObjMap\<rparr>)
 7. vsv (inv_dghm \<FF>\<lparr>ArrMap\<rparr>)
 8. \<BB>\<lparr>Obj\<rparr> = \<BB>\<lparr>Obj\<rparr>
 9. \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
 10. \<BB>\<lparr>Arr\<rparr> = \<BB>\<lparr>Arr\<rparr>
A total of 14 subgoals...
[PROOF STEP]
qed
    (
      cs_concl cs_shallow
        cs_simp: dg_cs_simps
        cs_intro: dg_cs_intros V_cs_intros dghm_cs_intros
    )+
[PROOF STATE]
proof (state)
this:
inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>

goal (2 subgoals):
 1. inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>
 2. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> = dghm_id \<BB>
[PROOF STEP]
show "inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>
[PROOF STEP]
proof(rule dghm_eqI[of \<alpha> \<AA> \<AA> _ \<AA> \<AA>])
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
 2. dghm_id \<AA> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
 3. (inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = dghm_id \<AA>\<lparr>ObjMap\<rparr>
 4. (inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = dghm_id \<AA>\<lparr>ArrMap\<rparr>
 5. \<AA> = \<AA>
 6. \<AA> = \<AA>
[PROOF STEP]
show "(inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = dghm_id \<AA>\<lparr>ObjMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = dghm_id \<AA>\<lparr>ObjMap\<rparr>
[PROOF STEP]
unfolding inv_dghm_components dghm_comp_components dghm_id_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<FF>\<lparr>ObjMap\<rparr>)\<inverse>\<^sub>\<circ> \<circ>\<^sub>\<circ> \<FF>\<lparr>ObjMap\<rparr> = vid_on (\<AA>\<lparr>Obj\<rparr>)
[PROOF STEP]
by (rule ObjMap.v11_vcomp_vconverse)
[PROOF STATE]
proof (state)
this:
(inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = dghm_id \<AA>\<lparr>ObjMap\<rparr>

goal (5 subgoals):
 1. inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
 2. dghm_id \<AA> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
 3. (inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = dghm_id \<AA>\<lparr>ArrMap\<rparr>
 4. \<AA> = \<AA>
 5. \<AA> = \<AA>
[PROOF STEP]
show "(inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = dghm_id \<AA>\<lparr>ArrMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = dghm_id \<AA>\<lparr>ArrMap\<rparr>
[PROOF STEP]
unfolding inv_dghm_components dghm_comp_components dghm_id_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<FF>\<lparr>ArrMap\<rparr>)\<inverse>\<^sub>\<circ> \<circ>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> = vid_on (\<AA>\<lparr>Arr\<rparr>)
[PROOF STEP]
by (rule ArrMap.v11_vcomp_vconverse)
[PROOF STATE]
proof (state)
this:
(inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = dghm_id \<AA>\<lparr>ArrMap\<rparr>

goal (4 subgoals):
 1. inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
 2. dghm_id \<AA> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
 3. \<AA> = \<AA>
 4. \<AA> = \<AA>
[PROOF STEP]
qed (use \<GG> in \<open>cs_concl cs_intro: dghm_cs_intros\<close>)
[PROOF STATE]
proof (state)
this:
inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>

goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> = dghm_id \<BB>
[PROOF STEP]
show "\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> = dghm_id \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> = dghm_id \<BB>
[PROOF STEP]
proof(rule dghm_eqI[of \<alpha> \<BB> \<BB> _ \<BB> \<BB>])
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 2. dghm_id \<BB> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 3. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF>)\<lparr>ObjMap\<rparr> = dghm_id \<BB>\<lparr>ObjMap\<rparr>
 4. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF>)\<lparr>ArrMap\<rparr> = dghm_id \<BB>\<lparr>ArrMap\<rparr>
 5. \<BB> = \<BB>
 6. \<BB> = \<BB>
[PROOF STEP]
show "(\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF>)\<lparr>ObjMap\<rparr> = dghm_id \<BB>\<lparr>ObjMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF>)\<lparr>ObjMap\<rparr> = dghm_id \<BB>\<lparr>ObjMap\<rparr>
[PROOF STEP]
unfolding inv_dghm_components dghm_comp_components dghm_id_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF>\<lparr>ObjMap\<rparr> \<circ>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>)\<inverse>\<^sub>\<circ> = vid_on (\<BB>\<lparr>Obj\<rparr>)
[PROOF STEP]
by (rule ObjMap.v11_vcomp_vconverse')
[PROOF STATE]
proof (state)
this:
(\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF>)\<lparr>ObjMap\<rparr> = dghm_id \<BB>\<lparr>ObjMap\<rparr>

goal (5 subgoals):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 2. dghm_id \<BB> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 3. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF>)\<lparr>ArrMap\<rparr> = dghm_id \<BB>\<lparr>ArrMap\<rparr>
 4. \<BB> = \<BB>
 5. \<BB> = \<BB>
[PROOF STEP]
show "(\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF>)\<lparr>ArrMap\<rparr> = dghm_id \<BB>\<lparr>ArrMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF>)\<lparr>ArrMap\<rparr> = dghm_id \<BB>\<lparr>ArrMap\<rparr>
[PROOF STEP]
unfolding inv_dghm_components dghm_comp_components dghm_id_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF>\<lparr>ArrMap\<rparr> \<circ>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>)\<inverse>\<^sub>\<circ> = vid_on (\<BB>\<lparr>Arr\<rparr>)
[PROOF STEP]
by (rule ArrMap.v11_vcomp_vconverse')
[PROOF STATE]
proof (state)
this:
(\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF>)\<lparr>ArrMap\<rparr> = dghm_id \<BB>\<lparr>ArrMap\<rparr>

goal (4 subgoals):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 2. dghm_id \<BB> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 3. \<BB> = \<BB>
 4. \<BB> = \<BB>
[PROOF STEP]
qed (use \<GG> in \<open>cs_concl cs_intro: dghm_cs_intros\<close>)
[PROOF STATE]
proof (state)
this:
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> = dghm_id \<BB>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_iso_dghm) iso_inv_dghm_ObjMap_dghm_ObjMap_app[dghm_cs_simps]:
  assumes "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
  shows "inv_dghm \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr> = a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_dghm \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr> = a
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv_dghm \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr> = a
[PROOF STEP]
from is_iso_dghm_is_iso_arr[OF is_iso_dghm_axioms]
[PROOF STATE]
proof (chain)
picking this:
inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>
inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> = dghm_id \<BB>
[PROOF STEP]
have
    "(inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = dghm_id \<AA>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>
inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> = dghm_id \<BB>

goal (1 subgoal):
 1. (inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = dghm_id \<AA>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = dghm_id \<AA>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>

goal (1 subgoal):
 1. inv_dghm \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr> = a
[PROOF STEP]
from this assms
[PROOF STATE]
proof (chain)
picking this:
(inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = dghm_id \<AA>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = dghm_id \<AA>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. inv_dghm \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr> = a
[PROOF STEP]
by
      (
        cs_prems cs_shallow
          cs_simp: dg_cs_simps cs_intro: dg_cs_intros dghm_cs_intros
      )
[PROOF STATE]
proof (state)
this:
inv_dghm \<FF>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr> = a

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_iso_dghm) iso_inv_dghm_ArrMap_dghm_ArrMap_app[dghm_cs_simps]:
  assumes "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
  shows "inv_dghm \<FF>\<lparr>ArrMap\<rparr>\<lparr>\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr> = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inv_dghm \<FF>\<lparr>ArrMap\<rparr>\<lparr>\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr> = f
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. inv_dghm \<FF>\<lparr>ArrMap\<rparr>\<lparr>\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr> = f
[PROOF STEP]
from is_iso_dghm_is_iso_arr[OF is_iso_dghm_axioms]
[PROOF STATE]
proof (chain)
picking this:
inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>
inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> = dghm_id \<BB>
[PROOF STEP]
have
    "(inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = dghm_id \<AA>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>"
[PROOF STATE]
proof (prove)
using this:
inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>
inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = dghm_id \<AA>
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M inv_dghm \<FF> = dghm_id \<BB>

goal (1 subgoal):
 1. (inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = dghm_id \<AA>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = dghm_id \<AA>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>

goal (1 subgoal):
 1. inv_dghm \<FF>\<lparr>ArrMap\<rparr>\<lparr>\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr> = f
[PROOF STEP]
from this assms
[PROOF STATE]
proof (chain)
picking this:
(inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = dghm_id \<AA>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(inv_dghm \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = dghm_id \<AA>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. inv_dghm \<FF>\<lparr>ArrMap\<rparr>\<lparr>\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr> = f
[PROOF STEP]
by
      (
        cs_prems cs_shallow
          cs_simp: dg_cs_simps cs_intro: dg_cs_intros dghm_cs_intros
      )
[PROOF STATE]
proof (state)
this:
inv_dghm \<FF>\<lparr>ArrMap\<rparr>\<lparr>\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr> = f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iso_digraphI':
  assumes "\<exists>\<FF>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
using assms iso_digraph.intro
[PROOF STATE]
proof (prove)
using this:
\<exists>\<FF>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
\<exists>\<FF>. \<FF> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>?\<alpha>\<^esub> ?\<BB> \<Longrightarrow> ?\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>

goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by auto


[STATEMENT]
lemma iso_digraphI:
  assumes "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
unfolding iso_digraph_def
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<exists>\<FF>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by auto


[STATEMENT]
lemma iso_digraphD[dest]:
  assumes "\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<exists>\<FF>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>\<FF>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<exists>\<FF>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
unfolding iso_digraph_def
[PROOF STATE]
proof (prove)
using this:
\<exists>\<FF>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<exists>\<FF>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by simp_all


[STATEMENT]
lemma iso_digraphE[elim]:
  assumes "\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
  obtains \<FF> where "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<FF>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. (\<And>\<FF>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma iso_digraph_refl:
  assumes "digraph \<alpha> \<AA>"
  shows "\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
proof(rule iso_digraphI[of _ _ _ \<open>dghm_id \<AA>\<close>])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dghm_id \<AA> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
interpret digraph \<alpha> \<AA>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<alpha> \<AA>
[PROOF STEP]
by (rule assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dghm_id \<AA> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show "dghm_id \<AA> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_id \<AA> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule dg_dghm_id_is_iso_dghm)
[PROOF STATE]
proof (state)
this:
dghm_id \<AA> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iso_digraph_sym[sym]:
  assumes "\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<BB> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<BB> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
interpret iso_digraph \<alpha> \<AA> \<BB>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<BB> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
from iso_digraph_is_iso_dghm
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<FF>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
obtain \<FF> where "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
using this:
\<exists>\<FF>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. (\<And>\<FF>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<BB> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
have "inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (simp add: is_iso_dghm_is_iso_arr(1))
[PROOF STATE]
proof (state)
this:
inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. \<BB> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inv_dghm \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. \<BB> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: dghm_cs_intros iso_digraphI)
[PROOF STATE]
proof (state)
this:
\<BB> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma iso_digraph_trans[trans]:
  assumes "\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>" and "\<BB> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>"
  shows "\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret L: iso_digraph \<alpha> \<AA> \<BB>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret R: iso_digraph \<alpha> \<BB> \<CC>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<BB> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
from L.iso_digraph_is_iso_dghm R.iso_digraph_is_iso_dghm
[PROOF STATE]
proof (chain)
picking this:
\<exists>\<FF>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
\<exists>\<FF>. \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<exists>\<FF>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<BB>
\<exists>\<FF>. \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^sub>.\<^sub>i\<^sub>s\<^sub>o\<^bsub>\<alpha>\<^esub> \<CC>

goal (1 subgoal):
 1. \<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (meson dghm_comp_is_iso_dghm iso_digraph.intro)
[PROOF STATE]
proof (state)
this:
\<AA> \<approx>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma count_wc_queries_empty [simp]: "count_wc_queries {} sorter = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_wc_queries {} sorter = 0
[PROOF STEP]
by (simp add: count_wc_queries_def)


[STATEMENT]
lemma count_wc_queries_aux:
  assumes "\<And>R. R \<in> Rs \<Longrightarrow> sorter = sorter' R" "Rs \<subseteq> Rs'" "finite Rs'"
  shows   "count_wc_queries Rs sorter \<le> Max ((\<lambda>R. count_queries R (sorter' R)) ` Rs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_wc_queries Rs sorter \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))
[PROOF STEP]
proof (cases "Rs = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> count_wc_queries Rs sorter \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))
 2. Rs \<noteq> {} \<Longrightarrow> count_wc_queries Rs sorter \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Rs \<noteq> {}

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> count_wc_queries Rs sorter \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))
 2. Rs \<noteq> {} \<Longrightarrow> count_wc_queries Rs sorter \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))
[PROOF STEP]
hence "count_wc_queries Rs sorter = Max ((\<lambda>R. count_queries R sorter) ` Rs)"
[PROOF STATE]
proof (prove)
using this:
Rs \<noteq> {}

goal (1 subgoal):
 1. count_wc_queries Rs sorter = (MAX R\<in>Rs. count_queries R sorter)
[PROOF STEP]
by (simp add: count_wc_queries_def)
[PROOF STATE]
proof (state)
this:
count_wc_queries Rs sorter = (MAX R\<in>Rs. count_queries R sorter)

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> count_wc_queries Rs sorter \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))
 2. Rs \<noteq> {} \<Longrightarrow> count_wc_queries Rs sorter \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
count_wc_queries Rs sorter = (MAX R\<in>Rs. count_queries R sorter)

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> count_wc_queries Rs sorter \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))
 2. Rs \<noteq> {} \<Longrightarrow> count_wc_queries Rs sorter \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))
[PROOF STEP]
have "(\<lambda>R. count_queries R sorter) ` Rs = (\<lambda>R. count_queries R (sorter' R)) ` Rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>R. count_queries R sorter) ` Rs = (\<lambda>R. count_queries R (sorter' R)) ` Rs
[PROOF STEP]
by (intro image_cong refl) (simp_all add: assms)
[PROOF STATE]
proof (state)
this:
(\<lambda>R. count_queries R sorter) ` Rs = (\<lambda>R. count_queries R (sorter' R)) ` Rs

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> count_wc_queries Rs sorter \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))
 2. Rs \<noteq> {} \<Longrightarrow> count_wc_queries Rs sorter \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>R. count_queries R sorter) ` Rs = (\<lambda>R. count_queries R (sorter' R)) ` Rs

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> count_wc_queries Rs sorter \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))
 2. Rs \<noteq> {} \<Longrightarrow> count_wc_queries Rs sorter \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))
[PROOF STEP]
have "Max \<dots> \<le> Max ((\<lambda>R. count_queries R (sorter' R)) ` Rs')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (MAX R\<in>Rs. count_queries R (sorter' R)) \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
Rs \<noteq> {}

goal (1 subgoal):
 1. (MAX R\<in>Rs. count_queries R (sorter' R)) \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))
[PROOF STEP]
by (intro Max_mono assms image_mono finite_imageI) auto
[PROOF STATE]
proof (state)
this:
(MAX R\<in>Rs. count_queries R (sorter' R)) \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> count_wc_queries Rs sorter \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))
 2. Rs \<noteq> {} \<Longrightarrow> count_wc_queries Rs sorter \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
count_wc_queries Rs sorter \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
count_wc_queries Rs sorter \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))

goal (1 subgoal):
 1. count_wc_queries Rs sorter \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
count_wc_queries Rs sorter \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))

goal (1 subgoal):
 1. Rs = {} \<Longrightarrow> count_wc_queries Rs sorter \<le> (MAX R\<in>Rs'. count_queries R (sorter' R))
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma card_range_eval_sorter:
  assumes "finite Rs"
  shows   "card ((\<lambda>R. eval_sorter R e) ` Rs) \<le> 2 ^ count_wc_queries Rs e"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ((\<lambda>R. eval_sorter R e) ` Rs) \<le> 2 ^ count_wc_queries Rs e
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite Rs

goal (1 subgoal):
 1. card ((\<lambda>R. eval_sorter R e) ` Rs) \<le> 2 ^ count_wc_queries Rs e
[PROOF STEP]
proof (induction e arbitrary: Rs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x Rs. finite Rs \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Return x)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Return x)
 2. \<And>x1a x2 x3 Rs. \<lbrakk>\<And>x3a Rs. \<lbrakk>x3a \<in> range x3; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R x3a) ` Rs) \<le> 2 ^ count_wc_queries Rs x3a; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query x1a x2 x3)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query x1a x2 x3)
[PROOF STEP]
case (Return xs Rs)
[PROOF STATE]
proof (state)
this:
finite Rs

goal (2 subgoals):
 1. \<And>x Rs. finite Rs \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Return x)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Return x)
 2. \<And>x1a x2 x3 Rs. \<lbrakk>\<And>x3a Rs. \<lbrakk>x3a \<in> range x3; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R x3a) ` Rs) \<le> 2 ^ count_wc_queries Rs x3a; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query x1a x2 x3)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query x1a x2 x3)
[PROOF STEP]
have *: "(\<lambda>R. eval_sorter R (Return xs)) ` Rs = (if Rs = {} then {} else {xs})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>R. eval_sorter R (Return xs)) ` Rs = (if Rs = {} then {} else {xs})
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<lambda>R. eval_sorter R (Return xs)) ` Rs = (if Rs = {} then {} else {xs})

goal (2 subgoals):
 1. \<And>x Rs. finite Rs \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Return x)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Return x)
 2. \<And>x1a x2 x3 Rs. \<lbrakk>\<And>x3a Rs. \<lbrakk>x3a \<in> range x3; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R x3a) ` Rs) \<le> 2 ^ count_wc_queries Rs x3a; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query x1a x2 x3)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query x1a x2 x3)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ((\<lambda>R. eval_sorter R (Return xs)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Return xs)
[PROOF STEP]
by (subst *) auto
[PROOF STATE]
proof (state)
this:
card ((\<lambda>R. eval_sorter R (Return xs)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Return xs)

goal (1 subgoal):
 1. \<And>x1a x2 x3 Rs. \<lbrakk>\<And>x3a Rs. \<lbrakk>x3a \<in> range x3; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R x3a) ` Rs) \<le> 2 ^ count_wc_queries Rs x3a; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query x1a x2 x3)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query x1a x2 x3)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2 x3 Rs. \<lbrakk>\<And>x3a Rs. \<lbrakk>x3a \<in> range x3; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R x3a) ` Rs) \<le> 2 ^ count_wc_queries Rs x3a; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query x1a x2 x3)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query x1a x2 x3)
[PROOF STEP]
case (Query a b f Rs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x3a \<in> range f; finite ?Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R ?x3a) ` ?Rs) \<le> 2 ^ count_wc_queries ?Rs ?x3a
finite Rs

goal (1 subgoal):
 1. \<And>x1a x2 x3 Rs. \<lbrakk>\<And>x3a Rs. \<lbrakk>x3a \<in> range x3; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R x3a) ` Rs) \<le> 2 ^ count_wc_queries Rs x3a; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query x1a x2 x3)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query x1a x2 x3)
[PROOF STEP]
have "f True \<in> range f" "f False \<in> range f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f True \<in> range f &&& f False \<in> range f
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
f True \<in> range f
f False \<in> range f

goal (1 subgoal):
 1. \<And>x1a x2 x3 Rs. \<lbrakk>\<And>x3a Rs. \<lbrakk>x3a \<in> range x3; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R x3a) ` Rs) \<le> 2 ^ count_wc_queries Rs x3a; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query x1a x2 x3)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query x1a x2 x3)
[PROOF STEP]
note IH = this [THEN Query.IH]
[PROOF STATE]
proof (state)
this:
finite ?Rs \<Longrightarrow> card ((\<lambda>R. eval_sorter R (f True)) ` ?Rs) \<le> 2 ^ count_wc_queries ?Rs (f True)
finite ?Rs \<Longrightarrow> card ((\<lambda>R. eval_sorter R (f False)) ` ?Rs) \<le> 2 ^ count_wc_queries ?Rs (f False)

goal (1 subgoal):
 1. \<And>x1a x2 x3 Rs. \<lbrakk>\<And>x3a Rs. \<lbrakk>x3a \<in> range x3; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R x3a) ` Rs) \<le> 2 ^ count_wc_queries Rs x3a; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query x1a x2 x3)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query x1a x2 x3)
[PROOF STEP]
let ?Rs1 = "{R\<in>Rs. (a, b) \<in> R}" and ?Rs2 = "{R\<in>Rs. (a, b) \<notin> R}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2 x3 Rs. \<lbrakk>\<And>x3a Rs. \<lbrakk>x3a \<in> range x3; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R x3a) ` Rs) \<le> 2 ^ count_wc_queries Rs x3a; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query x1a x2 x3)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query x1a x2 x3)
[PROOF STEP]
let ?A = "(\<lambda>R. eval_sorter R (f True)) ` ?Rs1" and ?B = "(\<lambda>R. eval_sorter R (f False)) ` ?Rs2"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2 x3 Rs. \<lbrakk>\<And>x3a Rs. \<lbrakk>x3a \<in> range x3; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R x3a) ` Rs) \<le> 2 ^ count_wc_queries Rs x3a; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query x1a x2 x3)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query x1a x2 x3)
[PROOF STEP]
from Query.prems
[PROOF STATE]
proof (chain)
picking this:
finite Rs
[PROOF STEP]
have fin: "finite ?Rs1" "finite ?Rs2"
[PROOF STATE]
proof (prove)
using this:
finite Rs

goal (1 subgoal):
 1. finite {R \<in> Rs. (a, b) \<in> R} &&& finite {R \<in> Rs. (a, b) \<notin> R}
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
finite {R \<in> Rs. (a, b) \<in> R}
finite {R \<in> Rs. (a, b) \<notin> R}

goal (1 subgoal):
 1. \<And>x1a x2 x3 Rs. \<lbrakk>\<And>x3a Rs. \<lbrakk>x3a \<in> range x3; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R x3a) ` Rs) \<le> 2 ^ count_wc_queries Rs x3a; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query x1a x2 x3)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query x1a x2 x3)
[PROOF STEP]
have *: "(\<lambda>R. eval_sorter R (Query a b f)) ` Rs \<subseteq> ?A \<union> ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>R. eval_sorter R (Query a b f)) ` Rs \<subseteq> (\<lambda>R. eval_sorter R (f True)) ` {R \<in> Rs. (a, b) \<in> R} \<union> (\<lambda>R. eval_sorter R (f False)) ` {R \<in> Rs. (a, b) \<notin> R}
[PROOF STEP]
proof (intro subsetI, elim imageE, goal_cases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x R. \<lbrakk>x = eval_sorter R (Query a b f); R \<in> Rs\<rbrakk> \<Longrightarrow> x \<in> (\<lambda>R. eval_sorter R (f True)) ` {R \<in> Rs. (a, b) \<in> R} \<union> (\<lambda>R. eval_sorter R (f False)) ` {R \<in> Rs. (a, b) \<notin> R}
[PROOF STEP]
case (1 xs R)
[PROOF STATE]
proof (state)
this:
xs = eval_sorter R (Query a b f)
R \<in> Rs

goal (1 subgoal):
 1. \<And>x R. \<lbrakk>x = eval_sorter R (Query a b f); R \<in> Rs\<rbrakk> \<Longrightarrow> x \<in> (\<lambda>R. eval_sorter R (f True)) ` {R \<in> Rs. (a, b) \<in> R} \<union> (\<lambda>R. eval_sorter R (f False)) ` {R \<in> Rs. (a, b) \<notin> R}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
xs = eval_sorter R (Query a b f)
R \<in> Rs

goal (1 subgoal):
 1. xs \<in> (\<lambda>R. eval_sorter R (f True)) ` {R \<in> Rs. (a, b) \<in> R} \<union> (\<lambda>R. eval_sorter R (f False)) ` {R \<in> Rs. (a, b) \<notin> R}
[PROOF STEP]
by (cases "(a,b) \<in> R") auto
[PROOF STATE]
proof (state)
this:
xs \<in> (\<lambda>R. eval_sorter R (f True)) ` {R \<in> Rs. (a, b) \<in> R} \<union> (\<lambda>R. eval_sorter R (f False)) ` {R \<in> Rs. (a, b) \<notin> R}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>R. eval_sorter R (Query a b f)) ` Rs \<subseteq> (\<lambda>R. eval_sorter R (f True)) ` {R \<in> Rs. (a, b) \<in> R} \<union> (\<lambda>R. eval_sorter R (f False)) ` {R \<in> Rs. (a, b) \<notin> R}

goal (1 subgoal):
 1. \<And>x1a x2 x3 Rs. \<lbrakk>\<And>x3a Rs. \<lbrakk>x3a \<in> range x3; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R x3a) ` Rs) \<le> 2 ^ count_wc_queries Rs x3a; finite Rs\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query x1a x2 x3)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query x1a x2 x3)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
proof (cases "Rs = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
 2. Rs \<noteq> {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Rs \<noteq> {}

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
 2. Rs \<noteq> {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
have "card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> card (?A \<union> ?B)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> card ((\<lambda>R. eval_sorter R (f True)) ` {R \<in> Rs. (a, b) \<in> R} \<union> (\<lambda>R. eval_sorter R (f False)) ` {R \<in> Rs. (a, b) \<notin> R})
[PROOF STEP]
by (intro card_mono finite_UnI finite_imageI fin *)
[PROOF STATE]
proof (state)
this:
card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> card ((\<lambda>R. eval_sorter R (f True)) ` {R \<in> Rs. (a, b) \<in> R} \<union> (\<lambda>R. eval_sorter R (f False)) ` {R \<in> Rs. (a, b) \<notin> R})

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
 2. Rs \<noteq> {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> card ((\<lambda>R. eval_sorter R (f True)) ` {R \<in> Rs. (a, b) \<in> R} \<union> (\<lambda>R. eval_sorter R (f False)) ` {R \<in> Rs. (a, b) \<notin> R})

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
 2. Rs \<noteq> {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
have "\<dots> \<le> card ?A + card ?B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ((\<lambda>R. eval_sorter R (f True)) ` {R \<in> Rs. (a, b) \<in> R} \<union> (\<lambda>R. eval_sorter R (f False)) ` {R \<in> Rs. (a, b) \<notin> R}) \<le> card ((\<lambda>R. eval_sorter R (f True)) ` {R \<in> Rs. (a, b) \<in> R}) + card ((\<lambda>R. eval_sorter R (f False)) ` {R \<in> Rs. (a, b) \<notin> R})
[PROOF STEP]
by (rule card_Un_le)
[PROOF STATE]
proof (state)
this:
card ((\<lambda>R. eval_sorter R (f True)) ` {R \<in> Rs. (a, b) \<in> R} \<union> (\<lambda>R. eval_sorter R (f False)) ` {R \<in> Rs. (a, b) \<notin> R}) \<le> card ((\<lambda>R. eval_sorter R (f True)) ` {R \<in> Rs. (a, b) \<in> R}) + card ((\<lambda>R. eval_sorter R (f False)) ` {R \<in> Rs. (a, b) \<notin> R})

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
 2. Rs \<noteq> {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card ((\<lambda>R. eval_sorter R (f True)) ` {R \<in> Rs. (a, b) \<in> R} \<union> (\<lambda>R. eval_sorter R (f False)) ` {R \<in> Rs. (a, b) \<notin> R}) \<le> card ((\<lambda>R. eval_sorter R (f True)) ` {R \<in> Rs. (a, b) \<in> R}) + card ((\<lambda>R. eval_sorter R (f False)) ` {R \<in> Rs. (a, b) \<notin> R})

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
 2. Rs \<noteq> {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
have "\<dots> \<le> 2 ^ count_wc_queries ?Rs1 (f True) + 2 ^ count_wc_queries ?Rs2 (f False)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card ((\<lambda>R. eval_sorter R (f True)) ` {R \<in> Rs. (a, b) \<in> R}) + card ((\<lambda>R. eval_sorter R (f False)) ` {R \<in> Rs. (a, b) \<notin> R}) \<le> 2 ^ count_wc_queries {R \<in> Rs. (a, b) \<in> R} (f True) + 2 ^ count_wc_queries {R \<in> Rs. (a, b) \<notin> R} (f False)
[PROOF STEP]
by (intro add_mono IH fin)
[PROOF STATE]
proof (state)
this:
card ((\<lambda>R. eval_sorter R (f True)) ` {R \<in> Rs. (a, b) \<in> R}) + card ((\<lambda>R. eval_sorter R (f False)) ` {R \<in> Rs. (a, b) \<notin> R}) \<le> 2 ^ count_wc_queries {R \<in> Rs. (a, b) \<in> R} (f True) + 2 ^ count_wc_queries {R \<in> Rs. (a, b) \<notin> R} (f False)

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
 2. Rs \<noteq> {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
card ((\<lambda>R. eval_sorter R (f True)) ` {R \<in> Rs. (a, b) \<in> R}) + card ((\<lambda>R. eval_sorter R (f False)) ` {R \<in> Rs. (a, b) \<notin> R}) \<le> 2 ^ count_wc_queries {R \<in> Rs. (a, b) \<in> R} (f True) + 2 ^ count_wc_queries {R \<in> Rs. (a, b) \<notin> R} (f False)

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
 2. Rs \<noteq> {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
have "count_wc_queries ?Rs1 (f True) \<le> Max ((\<lambda>R. count_queries R (f ((a,b)\<in>R))) ` Rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_wc_queries {R \<in> Rs. (a, b) \<in> R} (f True) \<le> (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R)))
[PROOF STEP]
by (intro count_wc_queries_aux Query.prems) auto
[PROOF STATE]
proof (state)
this:
count_wc_queries {R \<in> Rs. (a, b) \<in> R} (f True) \<le> (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R)))

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
 2. Rs \<noteq> {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
count_wc_queries {R \<in> Rs. (a, b) \<in> R} (f True) \<le> (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R)))

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
 2. Rs \<noteq> {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
have "count_wc_queries ?Rs2 (f False) \<le> Max ((\<lambda>R. count_queries R (f ((a,b)\<in>R))) ` Rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_wc_queries {R \<in> Rs. (a, b) \<notin> R} (f False) \<le> (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R)))
[PROOF STEP]
by (intro count_wc_queries_aux Query.prems) auto
[PROOF STATE]
proof (state)
this:
count_wc_queries {R \<in> Rs. (a, b) \<notin> R} (f False) \<le> (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R)))

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
 2. Rs \<noteq> {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
count_wc_queries {R \<in> Rs. (a, b) \<notin> R} (f False) \<le> (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R)))

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
 2. Rs \<noteq> {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
have "2 ^ \<dots> + 2 ^ \<dots> = (2 ^ Suc \<dots> :: nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R))) + 2 ^ (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R))) = 2 ^ Suc (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R))) + 2 ^ (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R))) = 2 ^ Suc (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R)))

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
 2. Rs \<noteq> {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 ^ (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R))) + 2 ^ (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R))) = 2 ^ Suc (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R)))

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
 2. Rs \<noteq> {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
have "Suc (Max ((\<lambda>R. count_queries R (f ((a,b)\<in>R))) ` Rs)) =
                 Max (Suc ` ((\<lambda>R. count_queries R (f ((a,b)\<in>R))) ` Rs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R))) = Max (Suc ` (\<lambda>R. count_queries R (f ((a, b) \<in> R))) ` Rs)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
Rs \<noteq> {}

goal (1 subgoal):
 1. Suc (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R))) = Max (Suc ` (\<lambda>R. count_queries R (f ((a, b) \<in> R))) ` Rs)
[PROOF STEP]
by (intro mono_Max_commute finite_imageI Query.prems) (auto simp: incseq_def)
[PROOF STATE]
proof (state)
this:
Suc (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R))) = Max (Suc ` (\<lambda>R. count_queries R (f ((a, b) \<in> R))) ` Rs)

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
 2. Rs \<noteq> {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Suc (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R))) = Max (Suc ` (\<lambda>R. count_queries R (f ((a, b) \<in> R))) ` Rs)

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
 2. Rs \<noteq> {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
have "Suc ` ((\<lambda>R. count_queries R (f ((a,b)\<in>R))) ` Rs) =
                 (\<lambda>R. Suc (count_queries R (f ((a,b)\<in>R)))) ` Rs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc ` (\<lambda>R. count_queries R (f ((a, b) \<in> R))) ` Rs = (\<lambda>R. Suc (count_queries R (f ((a, b) \<in> R)))) ` Rs
[PROOF STEP]
by (simp add: image_image)
[PROOF STATE]
proof (state)
this:
Suc ` (\<lambda>R. count_queries R (f ((a, b) \<in> R))) ` Rs = (\<lambda>R. Suc (count_queries R (f ((a, b) \<in> R)))) ` Rs

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
 2. Rs \<noteq> {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Suc ` (\<lambda>R. count_queries R (f ((a, b) \<in> R))) ` Rs = (\<lambda>R. Suc (count_queries R (f ((a, b) \<in> R)))) ` Rs

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
 2. Rs \<noteq> {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
have "Max \<dots> = count_wc_queries Rs (Query a b f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (MAX R\<in>Rs. Suc (count_queries R (f ((a, b) \<in> R)))) = count_wc_queries Rs (Query a b f)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
Rs \<noteq> {}

goal (1 subgoal):
 1. (MAX R\<in>Rs. Suc (count_queries R (f ((a, b) \<in> R)))) = count_wc_queries Rs (Query a b f)
[PROOF STEP]
by (auto simp add: count_wc_queries_def)
[PROOF STATE]
proof (state)
this:
(MAX R\<in>Rs. Suc (count_queries R (f ((a, b) \<in> R)))) = count_wc_queries Rs (Query a b f)

goal (2 subgoals):
 1. Rs = {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
 2. Rs \<noteq> {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> 2 ^ x + 2 ^ count_wc_queries {R \<in> Rs. (a, b) \<notin> R} (f False) \<le> 2 ^ y + 2 ^ count_wc_queries {R \<in> Rs. (a, b) \<notin> R} (f False); \<And>x y. x \<le> y \<Longrightarrow> 2 ^ (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R))) + 2 ^ x \<le> 2 ^ (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R))) + 2 ^ y\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>x y. x \<le> y \<Longrightarrow> 2 ^ x + 2 ^ count_wc_queries {R \<in> Rs. (a, b) \<notin> R} (f False) \<le> 2 ^ y + 2 ^ count_wc_queries {R \<in> Rs. (a, b) \<notin> R} (f False); \<And>x y. x \<le> y \<Longrightarrow> 2 ^ (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R))) + 2 ^ x \<le> 2 ^ (MAX R\<in>Rs. count_queries R (f ((a, b) \<in> R))) + 2 ^ y\<rbrakk> \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)

goal (1 subgoal):
 1. card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
by - simp_all
[PROOF STATE]
proof (state)
this:
card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)

goal (1 subgoal):
 1. Rs = {} \<Longrightarrow> card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)
[PROOF STEP]
qed simp_all
[PROOF STATE]
proof (state)
this:
card ((\<lambda>R. eval_sorter R (Query a b f)) ` Rs) \<le> 2 ^ count_wc_queries Rs (Query a b f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ln_fact_bigo: "(\<lambda>n. ln (fact n) - (ln (2 * pi * n) / 2 + n * ln n - n)) \<in> O(\<lambda>n. 1 / n)"
  and asymp_equiv_ln_fact [asymp_equiv_intros]: "(\<lambda>n. ln (fact n)) \<sim>[at_top] (\<lambda>n. n * ln n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. ln (fact n) - (ln (2 * pi * real n) / 2 + real n * ln (real n) - real n)) \<in> O(\<lambda>x. 1 / real x) &&& (\<lambda>n. ln (fact n)) \<sim>[sequentially] (\<lambda>n. real n * ln (real n))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>n. ln (fact n) - (ln (2 * pi * real n) / 2 + real n * ln (real n) - real n)) \<in> O(\<lambda>x. 1 / real x)
 2. (\<lambda>n. ln (fact n)) \<sim>[sequentially] (\<lambda>n. real n * ln (real n))
[PROOF STEP]
include asymp_equiv_notation
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<lambda>n. ln (fact n) - (ln (2 * pi * real n) / 2 + real n * ln (real n) - real n)) \<in> O(\<lambda>x. 1 / real x)
 2. (\<lambda>n. ln (fact n)) \<sim>[sequentially] (\<lambda>n. real n * ln (real n))
[PROOF STEP]
define f where "f = (\<lambda>n. ln (2 * pi * real n) / 2 + real n * ln (real n) - real n)"
[PROOF STATE]
proof (state)
this:
f = (\<lambda>n. ln (2 * pi * real n) / 2 + real n * ln (real n) - real n)

goal (2 subgoals):
 1. (\<lambda>n. ln (fact n) - (ln (2 * pi * real n) / 2 + real n * ln (real n) - real n)) \<in> O(\<lambda>x. 1 / real x)
 2. (\<lambda>n. ln (fact n)) \<sim>[sequentially] (\<lambda>n. real n * ln (real n))
[PROOF STEP]
have "eventually (\<lambda>n. ln (fact n) - f n \<in> {0..1/(12*real n)}) at_top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. ln (fact n) - f n \<in> {0..1 / (12 * real n)}
[PROOF STEP]
using eventually_gt_at_top[of "1::nat"]
[PROOF STATE]
proof (prove)
using this:
eventually ((<) 1) sequentially

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. ln (fact n) - f n \<in> {0..1 / (12 * real n)}
[PROOF STEP]
proof eventually_elim
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n. 1 < n \<Longrightarrow> ln (fact n) - f n \<in> {0..1 / (12 * real n)}
[PROOF STEP]
case (elim n)
[PROOF STATE]
proof (state)
this:
1 < n

goal (1 subgoal):
 1. \<And>n. 1 < n \<Longrightarrow> ln (fact n) - f n \<in> {0..1 / (12 * real n)}
[PROOF STEP]
with ln_fact_bounds[of n]
[PROOF STATE]
proof (chain)
picking this:
0 < n \<Longrightarrow> ln (2 * pi * real n) / 2 + real n * ln (real n) - real n \<le> ln (fact n)
0 < n \<Longrightarrow> ln (fact n) \<le> ln (2 * pi * real n) / 2 + real n * ln (real n) - real n + 1 / (12 * real n)
1 < n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 < n \<Longrightarrow> ln (2 * pi * real n) / 2 + real n * ln (real n) - real n \<le> ln (fact n)
0 < n \<Longrightarrow> ln (fact n) \<le> ln (2 * pi * real n) / 2 + real n * ln (real n) - real n + 1 / (12 * real n)
1 < n

goal (1 subgoal):
 1. ln (fact n) - f n \<in> {0..1 / (12 * real n)}
[PROOF STEP]
by (simp add: f_def)
[PROOF STATE]
proof (state)
this:
ln (fact n) - f n \<in> {0..1 / (12 * real n)}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. ln (fact n) - f n \<in> {0..1 / (12 * real n)}

goal (2 subgoals):
 1. (\<lambda>n. ln (fact n) - (ln (2 * pi * real n) / 2 + real n * ln (real n) - real n)) \<in> O(\<lambda>x. 1 / real x)
 2. (\<lambda>n. ln (fact n)) \<sim>[sequentially] (\<lambda>n. real n * ln (real n))
[PROOF STEP]
hence "eventually (\<lambda>n. norm (ln (fact n) - f n) \<le> (1/12) * norm (1 / real n)) at_top"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. ln (fact n) - f n \<in> {0..1 / (12 * real n)}

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. norm (ln (fact n) - f n) \<le> 1 / 12 * norm (1 / real n)
[PROOF STEP]
using eventually_gt_at_top[of "0::nat"]
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. ln (fact n) - f n \<in> {0..1 / (12 * real n)}
eventually ((<) 0) sequentially

goal (1 subgoal):
 1. \<forall>\<^sub>F n in sequentially. norm (ln (fact n) - f n) \<le> 1 / 12 * norm (1 / real n)
[PROOF STEP]
by eventually_elim (simp_all add: field_simps)
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F n in sequentially. norm (ln (fact n) - f n) \<le> 1 / 12 * norm (1 / real n)

goal (2 subgoals):
 1. (\<lambda>n. ln (fact n) - (ln (2 * pi * real n) / 2 + real n * ln (real n) - real n)) \<in> O(\<lambda>x. 1 / real x)
 2. (\<lambda>n. ln (fact n)) \<sim>[sequentially] (\<lambda>n. real n * ln (real n))
[PROOF STEP]
thus "(\<lambda>n. ln (fact n) - f n) \<in> O(\<lambda>n. 1 / real n)"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. norm (ln (fact n) - f n) \<le> 1 / 12 * norm (1 / real n)

goal (1 subgoal):
 1. (\<lambda>n. ln (fact n) - f n) \<in> O(\<lambda>n. 1 / real n)
[PROOF STEP]
using bigoI[of "\<lambda>n. ln (fact n) - f n" "1/12" "\<lambda>n. 1 / real n"]
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F n in sequentially. norm (ln (fact n) - f n) \<le> 1 / 12 * norm (1 / real n)
\<forall>\<^sub>F x in ?F. norm (ln (fact x) - f x) \<le> 1 / 12 * norm (1 / real x) \<Longrightarrow> (\<lambda>n. ln (fact n) - f n) \<in> O[?F](\<lambda>n. 1 / real n)

goal (1 subgoal):
 1. (\<lambda>n. ln (fact n) - f n) \<in> O(\<lambda>n. 1 / real n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>n. ln (fact n) - f n) \<in> O(\<lambda>n. 1 / real n)

goal (1 subgoal):
 1. (\<lambda>n. ln (fact n)) \<sim>[sequentially] (\<lambda>n. real n * ln (real n))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>n. ln (fact n) - f n) \<in> O(\<lambda>n. 1 / real n)

goal (1 subgoal):
 1. (\<lambda>n. ln (fact n)) \<sim>[sequentially] (\<lambda>n. real n * ln (real n))
[PROOF STEP]
have "(\<lambda>n. 1 / real n) \<in> o(f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. 1 / real n) \<in> o(f)
[PROOF STEP]
unfolding f_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. 1 / real n) \<in> o(\<lambda>n. ln (2 * pi * real n) / 2 + real n * ln (real n) - real n)
[PROOF STEP]
by (intro smallo_real_nat_transfer) simp
[PROOF STATE]
proof (state)
this:
(\<lambda>n. 1 / real n) \<in> o(f)

goal (1 subgoal):
 1. (\<lambda>n. ln (fact n)) \<sim>[sequentially] (\<lambda>n. real n * ln (real n))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. ln (fact n) - f n) \<in> o(f)
[PROOF STEP]
have "(\<lambda>n. f n + (ln (fact n) - f n)) \<sim> f"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. ln (fact n) - f n) \<in> o(f)

goal (1 subgoal):
 1. (\<lambda>n. f n + (ln (fact n) - f n)) \<sim>[sequentially] f
[PROOF STEP]
by (subst asymp_equiv_add_right) simp_all
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f n + (ln (fact n) - f n)) \<sim>[sequentially] f

goal (1 subgoal):
 1. (\<lambda>n. ln (fact n)) \<sim>[sequentially] (\<lambda>n. real n * ln (real n))
[PROOF STEP]
hence "(\<lambda>n. ln (fact n)) \<sim> f"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. f n + (ln (fact n) - f n)) \<sim>[sequentially] f

goal (1 subgoal):
 1. (\<lambda>n. ln (fact n)) \<sim>[sequentially] f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<lambda>n. ln (fact n)) \<sim>[sequentially] f

goal (1 subgoal):
 1. (\<lambda>n. ln (fact n)) \<sim>[sequentially] (\<lambda>n. real n * ln (real n))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>n. ln (fact n)) \<sim>[sequentially] f

goal (1 subgoal):
 1. (\<lambda>n. ln (fact n)) \<sim>[sequentially] (\<lambda>n. real n * ln (real n))
[PROOF STEP]
have "f \<sim> (\<lambda>n. n * ln n + (ln (2*pi*n)/2 - n))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f \<sim>[sequentially] (\<lambda>x. real x * ln (real x) + (ln (2 * pi * real x) / 2 - real x))
[PROOF STEP]
by (simp add: f_def algebra_simps)
[PROOF STATE]
proof (state)
this:
f \<sim>[sequentially] (\<lambda>x. real x * ln (real x) + (ln (2 * pi * real x) / 2 - real x))

goal (1 subgoal):
 1. (\<lambda>n. ln (fact n)) \<sim>[sequentially] (\<lambda>n. real n * ln (real n))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f \<sim>[sequentially] (\<lambda>x. real x * ln (real x) + (ln (2 * pi * real x) / 2 - real x))

goal (1 subgoal):
 1. (\<lambda>n. ln (fact n)) \<sim>[sequentially] (\<lambda>n. real n * ln (real n))
[PROOF STEP]
have "\<dots> \<sim> (\<lambda>n. n * ln n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. real x * ln (real x) + (ln (2 * pi * real x) / 2 - real x)) \<sim>[sequentially] (\<lambda>x. real x * ln (real x))
[PROOF STEP]
by (subst asymp_equiv_add_right) auto
[PROOF STATE]
proof (state)
this:
(\<lambda>x. real x * ln (real x) + (ln (2 * pi * real x) / 2 - real x)) \<sim>[sequentially] (\<lambda>x. real x * ln (real x))

goal (1 subgoal):
 1. (\<lambda>n. ln (fact n)) \<sim>[sequentially] (\<lambda>n. real n * ln (real n))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<And>c d. c \<sim>[sequentially] d \<Longrightarrow> c \<sim>[sequentially] d; \<And>c d. c \<sim>[sequentially] d \<Longrightarrow> c \<sim>[sequentially] d\<rbrakk> \<Longrightarrow> (\<lambda>n. ln (fact n)) \<sim>[sequentially] (\<lambda>a. real a * ln (real a))
[PROOF STEP]
show "(\<lambda>n. ln (fact n)) \<sim> (\<lambda>n. n * ln n)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<And>c d. c \<sim>[sequentially] d \<Longrightarrow> c \<sim>[sequentially] d; \<And>c d. c \<sim>[sequentially] d \<Longrightarrow> c \<sim>[sequentially] d\<rbrakk> \<Longrightarrow> (\<lambda>n. ln (fact n)) \<sim>[sequentially] (\<lambda>a. real a * ln (real a))

goal (1 subgoal):
 1. (\<lambda>n. ln (fact n)) \<sim>[sequentially] (\<lambda>n. real n * ln (real n))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>n. ln (fact n)) \<sim>[sequentially] (\<lambda>n. real n * ln (real n))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma trans_trel:
  "\<lbrakk> (\<sigma>, P) \<rightarrow>\<^sub>u (\<rho>, Q); (\<rho>, Q) \<rightarrow>\<^sub>u (\<phi>, R) \<rbrakk> \<Longrightarrow> (\<sigma>, P) \<rightarrow>\<^sub>u (\<phi>, R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, P) \<rightarrow>\<^sub>u (\<rho>, Q); (\<rho>, Q) \<rightarrow>\<^sub>u (\<phi>, R)\<rbrakk> \<Longrightarrow> (\<sigma>, P) \<rightarrow>\<^sub>u (\<phi>, R)
[PROOF STEP]
by auto


[STATEMENT]
lemma skip_trel: "(\<sigma>, II) \<rightarrow>\<^sub>u (\<sigma>, II)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, II) \<rightarrow>\<^sub>u (\<sigma>, II)
[PROOF STEP]
by simp


[STATEMENT]
lemma assigns_trel: "(\<sigma>, \<langle>\<rho>\<rangle>\<^sub>a) \<rightarrow>\<^sub>u (\<rho> \<circ> \<sigma>, II)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, \<langle>\<rho>\<rangle>\<^sub>a) \<rightarrow>\<^sub>u (\<rho> \<circ> \<sigma>, II)
[PROOF STEP]
by (simp add: assigns_comp)


[STATEMENT]
lemma assign_trel:
  "(\<sigma>, x := v) \<rightarrow>\<^sub>u (\<sigma>(&x \<mapsto>\<^sub>s \<sigma> \<dagger> v), II)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, x := v) \<rightarrow>\<^sub>u (\<sigma>(&x \<mapsto>\<^sub>s \<sigma> \<dagger> v), II)
[PROOF STEP]
by (simp add: assigns_comp usubst)


[STATEMENT]
lemma seq_trel:
  assumes "(\<sigma>, P) \<rightarrow>\<^sub>u (\<rho>, Q)"
  shows "(\<sigma>, P ;; R) \<rightarrow>\<^sub>u (\<rho>, Q ;; R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, P ;; R) \<rightarrow>\<^sub>u (\<rho>, Q ;; R)
[PROOF STEP]
by (metis (no_types, lifting) assms order_refl seqr_assoc seqr_mono trel.simps)


[STATEMENT]
lemma seq_skip_trel:
  "(\<sigma>, II ;; P) \<rightarrow>\<^sub>u (\<sigma>, P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, II ;; P) \<rightarrow>\<^sub>u (\<sigma>, P)
[PROOF STEP]
by simp


[STATEMENT]
lemma nondet_left_trel:
  "(\<sigma>, P \<sqinter> Q) \<rightarrow>\<^sub>u (\<sigma>, P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, P \<sqinter> Q) \<rightarrow>\<^sub>u (\<sigma>, P)
[PROOF STEP]
by (metis (no_types, opaque_lifting) disj_comm disj_upred_def semilattice_sup_class.sup.absorb_iff1 semilattice_sup_class.sup.left_idem seqr_or_distr trel.simps)


[STATEMENT]
lemma nondet_right_trel:
  "(\<sigma>, P \<sqinter> Q) \<rightarrow>\<^sub>u (\<sigma>, Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, P \<sqinter> Q) \<rightarrow>\<^sub>u (\<sigma>, Q)
[PROOF STEP]
by (simp add: seqr_mono)


[STATEMENT]
lemma rcond_true_trel:
  assumes "\<sigma> \<dagger> b = true"
  shows "(\<sigma>, P \<triangleleft> b \<triangleright>\<^sub>r Q) \<rightarrow>\<^sub>u (\<sigma>, P)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, P \<triangleleft> b \<triangleright>\<^sub>r Q) \<rightarrow>\<^sub>u (\<sigma>, P)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<dagger> b = true

goal (1 subgoal):
 1. (\<sigma>, P \<triangleleft> b \<triangleright>\<^sub>r Q) \<rightarrow>\<^sub>u (\<sigma>, P)
[PROOF STEP]
by (simp add: assigns_r_comp usubst alpha cond_unit_T)


[STATEMENT]
lemma rcond_false_trel:
  assumes "\<sigma> \<dagger> b = false"
  shows "(\<sigma>, P \<triangleleft> b \<triangleright>\<^sub>r Q) \<rightarrow>\<^sub>u (\<sigma>, Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, P \<triangleleft> b \<triangleright>\<^sub>r Q) \<rightarrow>\<^sub>u (\<sigma>, Q)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<sigma> \<dagger> b = false

goal (1 subgoal):
 1. (\<sigma>, P \<triangleleft> b \<triangleright>\<^sub>r Q) \<rightarrow>\<^sub>u (\<sigma>, Q)
[PROOF STEP]
by (simp add: assigns_r_comp usubst alpha cond_unit_F)


[STATEMENT]
lemma while_true_trel:
  assumes "\<sigma> \<dagger> b = true"
  shows "(\<sigma>, while b do P od) \<rightarrow>\<^sub>u (\<sigma>, P ;; while b do P od)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, while\<^sup>\<top> b do P od) \<rightarrow>\<^sub>u (\<sigma>, P ;; while\<^sup>\<top> b do P od)
[PROOF STEP]
by (metis assms rcond_true_trel while_unfold)


[STATEMENT]
lemma while_false_trel:
  assumes "\<sigma> \<dagger> b = false"
  shows "(\<sigma>, while b do P od) \<rightarrow>\<^sub>u (\<sigma>, II)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, while\<^sup>\<top> b do P od) \<rightarrow>\<^sub>u (\<sigma>, II)
[PROOF STEP]
by (metis assms rcond_false_trel while_unfold)


[STATEMENT]
theorem hoare_opsem_link:
  "\<lbrace>p\<rbrace>Q\<lbrace>r\<rbrace>\<^sub>u = (\<forall> \<sigma>\<^sub>0 \<sigma>\<^sub>1. `\<sigma>\<^sub>0 \<dagger> p` \<and> (\<sigma>\<^sub>0, Q) \<rightarrow>\<^sub>u (\<sigma>\<^sub>1, II) \<longrightarrow> `\<sigma>\<^sub>1 \<dagger> r`)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrace>p\<rbrace> Q \<lbrace>r\<rbrace>\<^sub>u = (\<forall>\<sigma>\<^sub>0 \<sigma>\<^sub>1. `\<sigma>\<^sub>0 \<dagger> p` \<and> (\<sigma>\<^sub>0, Q) \<rightarrow>\<^sub>u (\<sigma>\<^sub>1, II) \<longrightarrow> `\<sigma>\<^sub>1 \<dagger> r`)
[PROOF STEP]
apply (rel_auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>\<sigma>\<^sub>0 \<sigma>\<^sub>1. (\<forall>b. \<lbrakk>p\<rbrakk>\<^sub>e (\<sigma>\<^sub>0 b)) \<and> (\<forall>a. \<lbrakk>Q\<rbrakk>\<^sub>e (\<sigma>\<^sub>0 a, \<sigma>\<^sub>1 a)) \<longrightarrow> (\<forall>b. \<lbrakk>r\<rbrakk>\<^sub>e (\<sigma>\<^sub>1 b)); \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); \<lbrakk>p\<rbrakk>\<^sub>e a\<rbrakk> \<Longrightarrow> \<lbrakk>r\<rbrakk>\<^sub>e b
[PROOF STEP]
apply (rename_tac a b)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>\<sigma>\<^sub>0 \<sigma>\<^sub>1. (\<forall>b. \<lbrakk>p\<rbrakk>\<^sub>e (\<sigma>\<^sub>0 b)) \<and> (\<forall>a. \<lbrakk>Q\<rbrakk>\<^sub>e (\<sigma>\<^sub>0 a, \<sigma>\<^sub>1 a)) \<longrightarrow> (\<forall>b. \<lbrakk>r\<rbrakk>\<^sub>e (\<sigma>\<^sub>1 b)); \<lbrakk>Q\<rbrakk>\<^sub>e (a, b); \<lbrakk>p\<rbrakk>\<^sub>e a\<rbrakk> \<Longrightarrow> \<lbrakk>r\<rbrakk>\<^sub>e b
[PROOF STEP]
apply (drule_tac x="\<lambda> _. a" in spec, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<lbrakk>Q\<rbrakk>\<^sub>e (a, b); \<lbrakk>p\<rbrakk>\<^sub>e a; \<forall>\<sigma>\<^sub>1. (\<forall>aa. \<lbrakk>Q\<rbrakk>\<^sub>e (a, \<sigma>\<^sub>1 aa)) \<longrightarrow> (\<forall>b. \<lbrakk>r\<rbrakk>\<^sub>e (\<sigma>\<^sub>1 b))\<rbrakk> \<Longrightarrow> \<lbrakk>r\<rbrakk>\<^sub>e b
[PROOF STEP]
apply (drule_tac x="\<lambda> _. b" in spec, simp)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma node_ptr_kinds_M_eq:
  assumes "|h \<turnstile> object_ptr_kinds_M|\<^sub>r = |h' \<turnstile> object_ptr_kinds_M|\<^sub>r"
  shows "|h \<turnstile> node_ptr_kinds_M|\<^sub>r = |h' \<turnstile> node_ptr_kinds_M|\<^sub>r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. |h \<turnstile> node_ptr_kinds_M|\<^sub>r = |h' \<turnstile> node_ptr_kinds_M|\<^sub>r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
|h \<turnstile> object_ptr_kinds_M|\<^sub>r = |h' \<turnstile> object_ptr_kinds_M|\<^sub>r

goal (1 subgoal):
 1. |h \<turnstile> node_ptr_kinds_M|\<^sub>r = |h' \<turnstile> node_ptr_kinds_M|\<^sub>r
[PROOF STEP]
by(auto simp add: node_ptr_kinds_M_defs object_ptr_kinds_M_defs node_ptr_kinds_def)