[STATEMENT]
lemma is_acc_suffix[simp]: "is_acc (suffix i r) \<longleftrightarrow> is_acc r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_acc (suffix i r) = is_acc r
[PROOF STEP]
unfolding is_acc_def suffix_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>A\<in>F. \<exists>\<^sub>\<infinity>ia. r (i + ia) \<in> A) = (\<forall>A\<in>F. \<exists>\<^sub>\<infinity>i. r i \<in> A)
[PROOF STEP]
apply (clarsimp simp: INFM_nat)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>A\<in>F. \<forall>m. \<exists>ia>m. r (i + ia) \<in> A) = (\<forall>A\<in>F. \<forall>m. \<exists>i>m. r i \<in> A)
[PROOF STEP]
apply (rule iffI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>A\<in>F. \<forall>m. \<exists>ia>m. r (i + ia) \<in> A \<Longrightarrow> \<forall>A\<in>F. \<forall>m. \<exists>i>m. r i \<in> A
 2. \<forall>A\<in>F. \<forall>m. \<exists>i>m. r i \<in> A \<Longrightarrow> \<forall>A\<in>F. \<forall>m. \<exists>ia>m. r (i + ia) \<in> A
[PROOF STEP]
apply (metis trans_less_add2)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A\<in>F. \<forall>m. \<exists>i>m. r i \<in> A \<Longrightarrow> \<forall>A\<in>F. \<forall>m. \<exists>ia>m. r (i + ia) \<in> A
[PROOF STEP]
by (metis add_lessD1 less_imp_add_positive nat_add_left_cancel_less)


[STATEMENT]
lemma finite_V_Fe:
    assumes "finite V" "A \<in> F"
    shows "finite A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite V
A \<in> F

goal (1 subgoal):
 1. finite A
[PROOF STEP]
by (metis Pow_iff infinite_super rev_subsetD F_ss)


[STATEMENT]
lemma G'_gb_fields: "gbg_F G' = { f`A | A. A\<in>F }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gbg_F G' = {f ` A |A. A \<in> F}
[PROOF STEP]
unfolding gb_rename_ecnv_def fr_rename_ext_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gbg_F \<lparr>g_V = f ` V, g_E = rename_E f E, g_V0 = f ` V0, gbg_F = {f ` A |A. A \<in> F}, \<dots> = ecnv G\<rparr> = {f ` A |A. A \<in> F}
[PROOF STEP]
by simp


[STATEMENT]
lemma acc_sim1: "is_acc r \<Longrightarrow> G'.is_acc (f o r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_acc r \<Longrightarrow> G'.is_acc (f \<circ> r)
[PROOF STEP]
unfolding is_acc_def G'.is_acc_def G'_gb_fields
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>A\<in>F. \<exists>\<^sub>\<infinity>i. r i \<in> A \<Longrightarrow> \<forall>A\<in>{f ` A |A. A \<in> F}. \<exists>\<^sub>\<infinity>i. (f \<circ> r) i \<in> A
[PROOF STEP]
by (fastforce intro: imageI simp: INFM_nat)


[STATEMENT]
lemma acc_sim2:
    assumes "G'.is_acc r" shows "is_acc (fi o r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_acc (fi \<circ> r)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_acc (fi \<circ> r)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
G'.is_acc r
[PROOF STEP]
have 1: "\<And>A m. A \<in> gbg_F G \<Longrightarrow> \<exists>i>m. r i \<in> f`A"
[PROOF STATE]
proof (prove)
using this:
G'.is_acc r

goal (1 subgoal):
 1. \<And>A m. A \<in> F \<Longrightarrow> \<exists>i>m. r i \<in> f ` A
[PROOF STEP]
unfolding G'.is_acc_def G'_gb_fields
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>{f ` A |A. A \<in> F}. \<exists>\<^sub>\<infinity>i. r i \<in> A

goal (1 subgoal):
 1. \<And>A m. A \<in> F \<Longrightarrow> \<exists>i>m. r i \<in> f ` A
[PROOF STEP]
by (auto simp: INFM_nat)
[PROOF STATE]
proof (state)
this:
?A \<in> F \<Longrightarrow> \<exists>i>?m. r i \<in> f ` ?A

goal (1 subgoal):
 1. is_acc (fi \<circ> r)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?A \<in> F \<Longrightarrow> \<exists>i>?m. r i \<in> f ` ?A

goal (1 subgoal):
 1. is_acc (fi \<circ> r)
[PROOF STEP]
fix A m
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_acc (fi \<circ> r)
[PROOF STEP]
assume 2: "A \<in> gbg_F G"
[PROOF STATE]
proof (state)
this:
A \<in> F

goal (1 subgoal):
 1. is_acc (fi \<circ> r)
[PROOF STEP]
from 1[OF this, of m]
[PROOF STATE]
proof (chain)
picking this:
\<exists>i>m. r i \<in> f ` A
[PROOF STEP]
have "\<exists>i>m. fi (r i) \<in> A"
[PROOF STATE]
proof (prove)
using this:
\<exists>i>m. r i \<in> f ` A

goal (1 subgoal):
 1. \<exists>i>m. fi (r i) \<in> A
[PROOF STEP]
using F_ss
[PROOF STATE]
proof (prove)
using this:
\<exists>i>m. r i \<in> f ` A
F \<subseteq> Pow V

goal (1 subgoal):
 1. \<exists>i>m. fi (r i) \<in> A
[PROOF STEP]
apply clarsimp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i x. \<lbrakk>F \<subseteq> Pow V; m < i; r i = f x; x \<in> A\<rbrakk> \<Longrightarrow> \<exists>i>m. fi (r i) \<in> A
[PROOF STEP]
by (metis Pow_iff 2 fi_f in_mono)
[PROOF STATE]
proof (state)
this:
\<exists>i>m. fi (r i) \<in> A

goal (1 subgoal):
 1. is_acc (fi \<circ> r)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?A2 \<in> F \<Longrightarrow> \<exists>i>?m2. fi (r i) \<in> ?A2

goal (1 subgoal):
 1. is_acc (fi \<circ> r)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
?A2 \<in> F \<Longrightarrow> \<exists>i>?m2. fi (r i) \<in> ?A2

goal (1 subgoal):
 1. is_acc (fi \<circ> r)
[PROOF STEP]
unfolding is_acc_def
[PROOF STATE]
proof (prove)
using this:
?A2 \<in> F \<Longrightarrow> \<exists>i>?m2. fi (r i) \<in> ?A2

goal (1 subgoal):
 1. \<forall>A\<in>F. \<exists>\<^sub>\<infinity>i. (fi \<circ> r) i \<in> A
[PROOF STEP]
by (auto simp: INFM_nat)
[PROOF STATE]
proof (state)
this:
is_acc (fi \<circ> r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma acc_run_sim1: "is_acc_run r \<Longrightarrow> G'.is_acc_run (f o r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_acc_run r \<Longrightarrow> G'.is_acc_run (f \<circ> r)
[PROOF STEP]
using acc_sim1 run_sim1
[PROOF STATE]
proof (prove)
using this:
is_acc ?r \<Longrightarrow> G'.is_acc (f \<circ> ?r)
is_run ?r \<Longrightarrow> G'.is_run (f \<circ> ?r)

goal (1 subgoal):
 1. is_acc_run r \<Longrightarrow> G'.is_acc_run (f \<circ> r)
[PROOF STEP]
unfolding G'.is_acc_run_def is_acc_run_def
[PROOF STATE]
proof (prove)
using this:
is_acc ?r \<Longrightarrow> G'.is_acc (f \<circ> ?r)
is_run ?r \<Longrightarrow> G'.is_run (f \<circ> ?r)

goal (1 subgoal):
 1. is_run r \<and> is_acc r \<Longrightarrow> G'.is_run (f \<circ> r) \<and> G'.is_acc (f \<circ> r)
[PROOF STEP]
by auto


[STATEMENT]
lemma acc_run_sim2: "G'.is_acc_run r \<Longrightarrow> is_acc_run (fi o r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G'.is_acc_run r \<Longrightarrow> is_acc_run (fi \<circ> r)
[PROOF STEP]
using acc_sim2 run_sim2
[PROOF STATE]
proof (prove)
using this:
G'.is_acc ?r \<Longrightarrow> is_acc (fi \<circ> ?r)
G'.is_run ?r \<Longrightarrow> is_run (fi \<circ> ?r)

goal (1 subgoal):
 1. G'.is_acc_run r \<Longrightarrow> is_acc_run (fi \<circ> r)
[PROOF STEP]
unfolding G'.is_acc_run_def is_acc_run_def
[PROOF STATE]
proof (prove)
using this:
G'.is_acc ?r \<Longrightarrow> is_acc (fi \<circ> ?r)
G'.is_run ?r \<Longrightarrow> is_run (fi \<circ> ?r)

goal (1 subgoal):
 1. G'.is_run r \<and> G'.is_acc r \<Longrightarrow> is_run (fi \<circ> r) \<and> is_acc (fi \<circ> r)
[PROOF STEP]
by auto


[STATEMENT]
lemma is_gba: "gba G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gba G
[PROOF STEP]
by unfold_locales


[STATEMENT]
lemma acceptI[intro?]: "\<lbrakk>is_acc_run r; \<And>i. L (r i) (w i)\<rbrakk> \<Longrightarrow> accept w"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_acc_run r; \<And>i. L (r i) (w i)\<rbrakk> \<Longrightarrow> accept w
[PROOF STEP]
by (auto simp: accept_def)


[STATEMENT]
lemma langI[intro?]: "accept w \<Longrightarrow> w\<in>lang"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. accept w \<Longrightarrow> w \<in> lang
[PROOF STEP]
by (auto simp: lang_def)


[STATEMENT]
lemma G'_gba_fields: "gba_L G' = (\<lambda>q l.
    if q\<in>f`V then L (fi q) l else False)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gba_L G' = (\<lambda>q l. if q \<in> f ` V then L (fi q) l else False)
[PROOF STEP]
unfolding gb_rename_ecnv_def gba_rename_ecnv_def fr_rename_ext_def fi_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gba_L \<lparr>g_V = f ` V, g_E = rename_E f E, g_V0 = f ` V0, gbg_F = {f ` A |A. A \<in> F}, gba_L = \<lambda>q l. if q \<in> f ` V then L (the_inv_into V f q) l else False, \<dots> = ecnv G\<rparr> = (\<lambda>q l. if q \<in> f ` V then L (the_inv_into V f q) l else False)
[PROOF STEP]
by simp


[STATEMENT]
lemma L_sim1: "\<lbrakk>range r \<subseteq> V; L (r i) l\<rbrakk> \<Longrightarrow> G'.L (f (r i)) l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range r \<subseteq> V; L (r i) l\<rbrakk> \<Longrightarrow> G'.L (f (r i)) l
[PROOF STEP]
by (auto simp: G'_gba_fields fi_def[symmetric] fi_f
      dest: inj_onD[OF INJ]
      dest!: rev_subsetD[OF rangeI[of _ i]])


[STATEMENT]
lemma L_sim2: "\<lbrakk> range r \<subseteq> f`V; G'.L (r i) l \<rbrakk> \<Longrightarrow> L (fi (r i)) l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range r \<subseteq> f ` V; G'.L (r i) l\<rbrakk> \<Longrightarrow> L (fi (r i)) l
[PROOF STEP]
by (auto
      simp: G'_gba_fields fi_def[symmetric] f_fi
      dest!: rev_subsetD[OF rangeI[of _ i]])


[STATEMENT]
lemma accept_eq[simp]: "G'.accept = accept"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G'.accept = accept
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. G'.accept x = accept x
[PROOF STEP]
unfolding accept_def G'.accept_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<exists>r. G'.is_acc_run r \<and> (\<forall>i. G'.L (r i) (x i))) = (\<exists>r. is_acc_run r \<and> (\<forall>i. L (r i) (x i)))
[PROOF STEP]
proof safe
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x r. \<lbrakk>G'.is_acc_run r; \<forall>i. G'.L (r i) (x i)\<rbrakk> \<Longrightarrow> \<exists>r. is_acc_run r \<and> (\<forall>i. L (r i) (x i))
 2. \<And>x r. \<lbrakk>is_acc_run r; \<forall>i. L (r i) (x i)\<rbrakk> \<Longrightarrow> \<exists>r. G'.is_acc_run r \<and> (\<forall>i. G'.L (r i) (x i))
[PROOF STEP]
fix w r
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x r. \<lbrakk>G'.is_acc_run r; \<forall>i. G'.L (r i) (x i)\<rbrakk> \<Longrightarrow> \<exists>r. is_acc_run r \<and> (\<forall>i. L (r i) (x i))
 2. \<And>x r. \<lbrakk>is_acc_run r; \<forall>i. L (r i) (x i)\<rbrakk> \<Longrightarrow> \<exists>r. G'.is_acc_run r \<and> (\<forall>i. G'.L (r i) (x i))
[PROOF STEP]
assume R: "G'.is_acc_run r"
[PROOF STATE]
proof (state)
this:
G'.is_acc_run r

goal (2 subgoals):
 1. \<And>x r. \<lbrakk>G'.is_acc_run r; \<forall>i. G'.L (r i) (x i)\<rbrakk> \<Longrightarrow> \<exists>r. is_acc_run r \<and> (\<forall>i. L (r i) (x i))
 2. \<And>x r. \<lbrakk>is_acc_run r; \<forall>i. L (r i) (x i)\<rbrakk> \<Longrightarrow> \<exists>r. G'.is_acc_run r \<and> (\<forall>i. G'.L (r i) (x i))
[PROOF STEP]
assume L: "\<forall>i. G'.L (r i) (w i)"
[PROOF STATE]
proof (state)
this:
\<forall>i. G'.L (r i) (w i)

goal (2 subgoals):
 1. \<And>x r. \<lbrakk>G'.is_acc_run r; \<forall>i. G'.L (r i) (x i)\<rbrakk> \<Longrightarrow> \<exists>r. is_acc_run r \<and> (\<forall>i. L (r i) (x i))
 2. \<And>x r. \<lbrakk>is_acc_run r; \<forall>i. L (r i) (x i)\<rbrakk> \<Longrightarrow> \<exists>r. G'.is_acc_run r \<and> (\<forall>i. G'.L (r i) (x i))
[PROOF STEP]
from R
[PROOF STATE]
proof (chain)
picking this:
G'.is_acc_run r
[PROOF STEP]
have RAN: "range r \<subseteq> f`V"
[PROOF STATE]
proof (prove)
using this:
G'.is_acc_run r

goal (1 subgoal):
 1. range r \<subseteq> f ` V
[PROOF STEP]
using G'.run_reachable[OF G'.acc_run_run[OF R]] G'.reachable_V
[PROOF STATE]
proof (prove)
using this:
G'.is_acc_run r
range r \<subseteq> G'.reachable
G'.reachable \<subseteq> G'.V

goal (1 subgoal):
 1. range r \<subseteq> f ` V
[PROOF STEP]
unfolding G'_fields
[PROOF STATE]
proof (prove)
using this:
G'.is_acc_run r
range r \<subseteq> (rename_E f E)\<^sup>* `` f ` V0
(rename_E f E)\<^sup>* `` f ` V0 \<subseteq> f ` V

goal (1 subgoal):
 1. range r \<subseteq> f ` V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
range r \<subseteq> f ` V

goal (2 subgoals):
 1. \<And>x r. \<lbrakk>G'.is_acc_run r; \<forall>i. G'.L (r i) (x i)\<rbrakk> \<Longrightarrow> \<exists>r. is_acc_run r \<and> (\<forall>i. L (r i) (x i))
 2. \<And>x r. \<lbrakk>is_acc_run r; \<forall>i. L (r i) (x i)\<rbrakk> \<Longrightarrow> \<exists>r. G'.is_acc_run r \<and> (\<forall>i. G'.L (r i) (x i))
[PROOF STEP]
from L
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. G'.L (r i) (w i)
[PROOF STEP]
show "\<exists>r. is_acc_run r \<and> (\<forall>i. L (r i) (w i))"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. G'.L (r i) (w i)

goal (1 subgoal):
 1. \<exists>r. is_acc_run r \<and> (\<forall>i. L (r i) (w i))
[PROOF STEP]
using acc_run_sim2[OF R] L_sim2[OF RAN]
[PROOF STATE]
proof (prove)
using this:
\<forall>i. G'.L (r i) (w i)
is_acc_run (fi \<circ> r)
G'.L (r ?i) ?l \<Longrightarrow> L (fi (r ?i)) ?l

goal (1 subgoal):
 1. \<exists>r. is_acc_run r \<and> (\<forall>i. L (r i) (w i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r. is_acc_run r \<and> (\<forall>i. L (r i) (w i))

goal (1 subgoal):
 1. \<And>x r. \<lbrakk>is_acc_run r; \<forall>i. L (r i) (x i)\<rbrakk> \<Longrightarrow> \<exists>r. G'.is_acc_run r \<and> (\<forall>i. G'.L (r i) (x i))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x r. \<lbrakk>is_acc_run r; \<forall>i. L (r i) (x i)\<rbrakk> \<Longrightarrow> \<exists>r. G'.is_acc_run r \<and> (\<forall>i. G'.L (r i) (x i))
[PROOF STEP]
fix w r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x r. \<lbrakk>is_acc_run r; \<forall>i. L (r i) (x i)\<rbrakk> \<Longrightarrow> \<exists>r. G'.is_acc_run r \<and> (\<forall>i. G'.L (r i) (x i))
[PROOF STEP]
assume R: "is_acc_run r"
[PROOF STATE]
proof (state)
this:
is_acc_run r

goal (1 subgoal):
 1. \<And>x r. \<lbrakk>is_acc_run r; \<forall>i. L (r i) (x i)\<rbrakk> \<Longrightarrow> \<exists>r. G'.is_acc_run r \<and> (\<forall>i. G'.L (r i) (x i))
[PROOF STEP]
assume L: "\<forall>i. L (r i) (w i)"
[PROOF STATE]
proof (state)
this:
\<forall>i. L (r i) (w i)

goal (1 subgoal):
 1. \<And>x r. \<lbrakk>is_acc_run r; \<forall>i. L (r i) (x i)\<rbrakk> \<Longrightarrow> \<exists>r. G'.is_acc_run r \<and> (\<forall>i. G'.L (r i) (x i))
[PROOF STEP]
from R
[PROOF STATE]
proof (chain)
picking this:
is_acc_run r
[PROOF STEP]
have RAN: "range r \<subseteq> V"
[PROOF STATE]
proof (prove)
using this:
is_acc_run r

goal (1 subgoal):
 1. range r \<subseteq> V
[PROOF STEP]
using run_reachable[OF acc_run_run[OF R]] reachable_V
[PROOF STATE]
proof (prove)
using this:
is_acc_run r
range r \<subseteq> reachable
reachable \<subseteq> V

goal (1 subgoal):
 1. range r \<subseteq> V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
range r \<subseteq> V

goal (1 subgoal):
 1. \<And>x r. \<lbrakk>is_acc_run r; \<forall>i. L (r i) (x i)\<rbrakk> \<Longrightarrow> \<exists>r. G'.is_acc_run r \<and> (\<forall>i. G'.L (r i) (x i))
[PROOF STEP]
from L
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. L (r i) (w i)
[PROOF STEP]
show "\<exists>r.
        G'.is_acc_run r
      \<and> (\<forall>i. G'.L (r i) (w i))"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. L (r i) (w i)

goal (1 subgoal):
 1. \<exists>r. G'.is_acc_run r \<and> (\<forall>i. G'.L (r i) (w i))
[PROOF STEP]
using acc_run_sim1[OF R] L_sim1[OF RAN]
[PROOF STATE]
proof (prove)
using this:
\<forall>i. L (r i) (w i)
G'.is_acc_run (f \<circ> r)
L (r ?i) ?l \<Longrightarrow> G'.L (f (r ?i)) ?l

goal (1 subgoal):
 1. \<exists>r. G'.is_acc_run r \<and> (\<forall>i. G'.L (r i) (w i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>r. G'.is_acc_run r \<and> (\<forall>i. G'.L (r i) (w i))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lang_eq[simp]: "G'.lang = lang"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G'.lang = lang
[PROOF STEP]
unfolding G'.lang_def lang_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Collect G'.accept = Collect accept
[PROOF STEP]
by simp


[STATEMENT]
lemma finite_G'_V:
    assumes "finite V"
    shows "finite G'.V"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite G'.V
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite V

goal (1 subgoal):
 1. finite G'.V
[PROOF STEP]
by (auto simp add: G'_gba_fields G'_fields split: if_split_asm)


[STATEMENT]
lemma gba_rename_correct:
  fixes G :: "('v,'l,'m) gba_rec_scheme"
  assumes "gba G"
  assumes INJ: "inj_on f (g_V G)"
  defines "G' \<equiv> gba_rename f G"
  shows "gba G'"
  and "finite (g_V G) \<Longrightarrow> finite (g_V G')"
  and "gba.accept G' = gba.accept G"
  and "gba.lang G' = gba.lang G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (gba G' &&& (finite (g_V G) \<Longrightarrow> finite (g_V G'))) &&& gba.accept G' = gba.accept G &&& gba.lang G' = gba.lang G
[PROOF STEP]
unfolding G'_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (gba (gba_rename f G) &&& (finite (g_V G) \<Longrightarrow> finite (g_V (gba_rename f G)))) &&& gba.accept (gba_rename f G) = gba.accept G &&& gba.lang (gba_rename f G) = gba.lang G
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. gba (gba_rename f G)
 2. finite (g_V G) \<Longrightarrow> finite (g_V (gba_rename f G))
 3. gba.accept (gba_rename f G) = gba.accept G
 4. gba.lang (gba_rename f G) = gba.lang G
[PROOF STEP]
let ?G' = "gba_rename f G"
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. gba (gba_rename f G)
 2. finite (g_V G) \<Longrightarrow> finite (g_V (gba_rename f G))
 3. gba.accept (gba_rename f G) = gba.accept G
 4. gba.lang (gba_rename f G) = gba.lang G
[PROOF STEP]
interpret gba G
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gba G
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. gba (gba_rename f G)
 2. finite V \<Longrightarrow> finite (g_V (gba_rename f G))
 3. gba.accept (gba_rename f G) = accept
 4. gba.lang (gba_rename f G) = lang
[PROOF STEP]
from INJ
[PROOF STATE]
proof (chain)
picking this:
inj_on f V
[PROOF STEP]
interpret gba_rename_precond G f "\<lambda>_. ()"
[PROOF STATE]
proof (prove)
using this:
inj_on f V

goal (1 subgoal):
 1. gba_rename_precond G f
[PROOF STEP]
by unfold_locales simp_all
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. gba G'
 2. finite V \<Longrightarrow> finite G'.V
 3. G'.accept = accept
 4. G'.lang = lang
[PROOF STEP]
show "gba ?G'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gba G'
[PROOF STEP]
by (rule G'.is_gba)
[PROOF STATE]
proof (state)
this:
gba G'

goal (3 subgoals):
 1. finite V \<Longrightarrow> finite G'.V
 2. G'.accept = accept
 3. G'.lang = lang
[PROOF STEP]
show "finite (g_V G) \<Longrightarrow> finite (g_V ?G')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite V \<Longrightarrow> finite G'.V
[PROOF STEP]
by (fact finite_G'_V)
[PROOF STATE]
proof (state)
this:
finite V \<Longrightarrow> finite G'.V

goal (2 subgoals):
 1. G'.accept = accept
 2. G'.lang = lang
[PROOF STEP]
show "G'.accept = accept"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G'.accept = accept
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
G'.accept = accept

goal (1 subgoal):
 1. G'.lang = lang
[PROOF STEP]
show "G'.lang = lang"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G'.lang = lang
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
G'.lang = lang

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_b_graph: "b_graph G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b_graph G
[PROOF STEP]
by unfold_locales


[STATEMENT]
lemma to_gbg_alt:
    "gbg.V T m = V"
    "gbg.E T m = E"
    "gbg.V0 T m = V0"
    "gbg.F T m = (if F=UNIV then {} else {F})"
    "gbg.is_run T m = is_run"
    "gbg.is_acc T m = is_acc"
    "gbg.is_acc_run T m = is_acc_run"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g_V (to_gbg_ext m) = V &&& g_E (to_gbg_ext m) = E &&& g_V0 (to_gbg_ext m) = V0) &&& (gbg_F (to_gbg_ext m) = (if F = UNIV then {} else {F}) &&& graph_defs.is_run (to_gbg_ext m) = is_run) &&& gb_graph.is_acc (to_gbg_ext m) = is_acc &&& gb_graph.is_acc_run (to_gbg_ext m) = is_acc_run
[PROOF STEP]
unfolding is_run_def[abs_def] gbg.is_run_def[abs_def]
      is_acc_def[abs_def] gbg.is_acc_def[abs_def]
      is_acc_run_def[abs_def] gbg.is_acc_run_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (g_V (to_gbg_ext m) = V &&& g_E (to_gbg_ext m) = E &&& g_V0 (to_gbg_ext m) = V0) &&& (gbg_F (to_gbg_ext m) = (if F = UNIV then {} else {F}) &&& (\<lambda>r. r 0 \<in> g_V0 (to_gbg_ext m) \<and> ipath (g_E (to_gbg_ext m)) r) = (\<lambda>r. r 0 \<in> V0 \<and> ipath E r)) &&& (\<lambda>r. \<forall>A\<in>gbg_F (to_gbg_ext m). \<exists>\<^sub>\<infinity>i. r i \<in> A) = (\<lambda>r. \<exists>\<^sub>\<infinity>i. r i \<in> F) &&& (\<lambda>r. (r 0 \<in> g_V0 (to_gbg_ext m) \<and> ipath (g_E (to_gbg_ext m)) r) \<and> (\<forall>A\<in>gbg_F (to_gbg_ext m). \<exists>\<^sub>\<infinity>i. r i \<in> A)) = (\<lambda>r. (r 0 \<in> V0 \<and> ipath E r) \<and> (\<exists>\<^sub>\<infinity>i. r i \<in> F))
[PROOF STEP]
by (auto simp: to_gbg_ext_def)


[STATEMENT]
lemma is_ba: "ba G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ba G
[PROOF STEP]
by unfold_locales


[STATEMENT]
lemma ba_acc_simps[simp]: "gba.L T m = L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gba_L (to_gba_ext m) = L
[PROOF STEP]
by (simp add: to_gbg_ext_def)


[STATEMENT]
lemma to_gba_alt_accept:
    "gba.accept T m = accept"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Automata.gba.accept (to_gba_ext m) = accept
[PROOF STEP]
apply (intro ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. Automata.gba.accept (to_gba_ext m) x = accept x
[PROOF STEP]
unfolding accept_def gba.accept_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<exists>r. gb_graph.is_acc_run (to_gba_ext m) r \<and> (\<forall>i. gba_L (to_gba_ext m) (r i) (x i))) = (\<exists>r. is_acc_run r \<and> (\<forall>i. L (r i) (x i)))
[PROOF STEP]
apply (simp_all add: to_gbg_alt)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma to_gba_alt_lang:
    "gba.lang T m = lang"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Automata.gba.lang (to_gba_ext m) = lang
[PROOF STEP]
unfolding lang_def gba.lang_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Collect (Automata.gba.accept (to_gba_ext m)) = Collect accept
[PROOF STEP]
apply (simp_all add: to_gba_alt_accept)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma acc_boundI[simp, intro]: "x\<in>acc q \<Longrightarrow> x<num_acc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> acc q \<Longrightarrow> x < num_acc
[PROOF STEP]
using acc_bound
[PROOF STATE]
proof (prove)
using this:
\<Union> (range acc) \<subseteq> {0..<num_acc}

goal (1 subgoal):
 1. x \<in> acc q \<Longrightarrow> x < num_acc
[PROOF STEP]
by fastforce


[STATEMENT]
lemma to_gbg_alt1:
    "gbg.E T m = E"
    "gbg.V0 T m = V0"
    "gbg.F T m = F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g_E (to_gbg_ext m) = E &&& g_V0 (to_gbg_ext m) = V0 &&& gbg_F (to_gbg_ext m) = F
[PROOF STEP]
by (simp_all add: to_gbg_ext_def)


[STATEMENT]
lemma F_fin[simp,intro!]: "finite F"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite F
[PROOF STEP]
unfolding F_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {accn i |i. i < num_acc}
[PROOF STEP]
by auto


[STATEMENT]
lemma is_run_gbg:
    "gbg.is_run T m = is_run"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph_defs.is_run (to_gbg_ext m) = is_run
[PROOF STEP]
unfolding is_run_def[abs_def] is_acc_run_def[abs_def]
      gbg.is_run_def[abs_def] gbg.is_acc_run_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>r. r 0 \<in> g_V0 (to_gbg_ext m) \<and> ipath (g_E (to_gbg_ext m)) r) = (\<lambda>r. r 0 \<in> V0 \<and> ipath E r)
[PROOF STEP]
by (simp_all add: to_gbg_ext_def)


[STATEMENT]
lemma is_acc_gbg:
    "gbg.is_acc T m = is_acc"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gb_graph.is_acc (to_gbg_ext m) = is_acc
[PROOF STEP]
apply (intro ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. gb_graph.is_acc (to_gbg_ext m) x = is_acc x
[PROOF STEP]
unfolding gbg.is_acc_def is_acc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<forall>A\<in>gbg_F (to_gbg_ext m). \<exists>\<^sub>\<infinity>i. x i \<in> A) = (\<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc (x i))
[PROOF STEP]
apply (simp add: to_gbg_alt1 is_run_gbg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<forall>A\<in>F. \<exists>\<^sub>\<infinity>i. x i \<in> A) = (\<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc (x i))
[PROOF STEP]
unfolding F_def accn_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<forall>A\<in>{{q. i \<in> acc q} |i. i < num_acc}. \<exists>\<^sub>\<infinity>i. x i \<in> A) = (\<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc (x i))
[PROOF STEP]
apply (blast intro: INFM_mono)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma is_acc_run_gbg:
    "gbg.is_acc_run T m = is_acc_run"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gb_graph.is_acc_run (to_gbg_ext m) = is_acc_run
[PROOF STEP]
apply (intro ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. gb_graph.is_acc_run (to_gbg_ext m) x = is_acc_run x
[PROOF STEP]
unfolding gbg.is_acc_run_def is_acc_run_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (graph_defs.is_run (to_gbg_ext m) x \<and> gb_graph.is_acc (to_gbg_ext m) x) = (is_run x \<and> is_acc x)
[PROOF STEP]
by (simp_all add: to_gbg_alt1 is_run_gbg is_acc_gbg)


[STATEMENT]
lemma acc_limit_alt:
    assumes FIN: "finite (range r)"
    shows "is_acc r \<longleftrightarrow> (\<forall>n<num_acc. limit r \<inter> accn n \<noteq> {})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_acc r = (\<forall>n<num_acc. limit r \<inter> accn n \<noteq> {})
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. is_acc r \<Longrightarrow> \<forall>n<num_acc. limit r \<inter> accn n \<noteq> {}
 2. \<forall>n<num_acc. limit r \<inter> accn n \<noteq> {} \<Longrightarrow> is_acc r
[PROOF STEP]
assume "\<forall>n<num_acc. limit r \<inter> accn n \<noteq> {}"
[PROOF STATE]
proof (state)
this:
\<forall>n<num_acc. limit r \<inter> accn n \<noteq> {}

goal (2 subgoals):
 1. is_acc r \<Longrightarrow> \<forall>n<num_acc. limit r \<inter> accn n \<noteq> {}
 2. \<forall>n<num_acc. limit r \<inter> accn n \<noteq> {} \<Longrightarrow> is_acc r
[PROOF STEP]
thus "is_acc r"
[PROOF STATE]
proof (prove)
using this:
\<forall>n<num_acc. limit r \<inter> accn n \<noteq> {}

goal (1 subgoal):
 1. is_acc r
[PROOF STEP]
unfolding is_acc_def accn_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n<num_acc. limit r \<inter> {q. n \<in> acc q} \<noteq> {}

goal (1 subgoal):
 1. \<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc (r i)
[PROOF STEP]
by (auto dest!: limit_inter_INF)
[PROOF STATE]
proof (state)
this:
is_acc r

goal (1 subgoal):
 1. is_acc r \<Longrightarrow> \<forall>n<num_acc. limit r \<inter> accn n \<noteq> {}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. is_acc r \<Longrightarrow> \<forall>n<num_acc. limit r \<inter> accn n \<noteq> {}
[PROOF STEP]
from FIN
[PROOF STATE]
proof (chain)
picking this:
finite (range r)
[PROOF STEP]
have FIN': "\<And>A. finite (A \<inter> range r)"
[PROOF STATE]
proof (prove)
using this:
finite (range r)

goal (1 subgoal):
 1. \<And>A. finite (A \<inter> range r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite (?A1 \<inter> range r)

goal (1 subgoal):
 1. is_acc r \<Longrightarrow> \<forall>n<num_acc. limit r \<inter> accn n \<noteq> {}
[PROOF STEP]
assume "is_acc r"
[PROOF STATE]
proof (state)
this:
is_acc r

goal (1 subgoal):
 1. is_acc r \<Longrightarrow> \<forall>n<num_acc. limit r \<inter> accn n \<noteq> {}
[PROOF STEP]
hence "\<forall>n<num_acc. limit r \<inter> (accn n \<inter> range r) \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
is_acc r

goal (1 subgoal):
 1. \<forall>n<num_acc. limit r \<inter> (accn n \<inter> range r) \<noteq> {}
[PROOF STEP]
unfolding is_acc_def accn_def
[PROOF STATE]
proof (prove)
using this:
\<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc (r i)

goal (1 subgoal):
 1. \<forall>n<num_acc. limit r \<inter> ({q. n \<in> acc q} \<inter> range r) \<noteq> {}
[PROOF STEP]
by (auto simp: fin_ex_inf_eq_limit[OF FIN', symmetric])
[PROOF STATE]
proof (state)
this:
\<forall>n<num_acc. limit r \<inter> (accn n \<inter> range r) \<noteq> {}

goal (1 subgoal):
 1. is_acc r \<Longrightarrow> \<forall>n<num_acc. limit r \<inter> accn n \<noteq> {}
[PROOF STEP]
thus "\<forall>n<num_acc. limit r \<inter> accn n \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
\<forall>n<num_acc. limit r \<inter> (accn n \<inter> range r) \<noteq> {}

goal (1 subgoal):
 1. \<forall>n<num_acc. limit r \<inter> accn n \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n<num_acc. limit r \<inter> accn n \<noteq> {}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma acc_limit_alt':
    "finite (range r) \<Longrightarrow> is_acc r \<longleftrightarrow> (\<Union>(acc ` limit r) = {0..<num_acc})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (range r) \<Longrightarrow> is_acc r = (\<Union> (acc ` limit r) = {0..<num_acc})
[PROOF STEP]
unfolding acc_limit_alt
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (range r) \<Longrightarrow> (\<forall>n<num_acc. limit r \<inter> accn n \<noteq> {}) = (\<Union> (acc ` limit r) = {0..<num_acc})
[PROOF STEP]
by (auto simp: accn_def)


[STATEMENT]
lemma is_igba: "igba G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igba G
[PROOF STEP]
by unfold_locales


[STATEMENT]
lemma to_gba_alt_L:
    "gba.L T m = L"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gba_L (to_gba_ext m) = L
[PROOF STEP]
by (auto simp: to_gbg_ext_def)


[STATEMENT]
lemma accept_gba_alt: "gba.accept T m = accept"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Automata.gba.accept (to_gba_ext m) = accept
[PROOF STEP]
apply (intro ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. Automata.gba.accept (to_gba_ext m) x = accept x
[PROOF STEP]
unfolding accept_def gba.accept_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. (\<exists>r. gb_graph.is_acc_run (to_gba_ext m) r \<and> (\<forall>i. gba_L (to_gba_ext m) (r i) (x i))) = (\<exists>r. is_acc_run r \<and> (\<forall>i. L (r i) (x i)))
[PROOF STEP]
apply (simp add: to_gbg_alt to_gba_alt_L)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma lang_gba_alt: "gba.lang T m = lang"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Automata.gba.lang (to_gba_ext m) = lang
[PROOF STEP]
unfolding lang_def gba.lang_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Collect (Automata.gba.accept (to_gba_ext m)) = Collect accept
[PROOF STEP]
apply (simp add: accept_gba_alt)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma F_to_idx_correct:
  shows "F_to_idx F \<le> SPEC (\<lambda>(num_acc,acc). F = { {q. i\<in>acc q} | i. i<num_acc }
    \<and> \<Union>(range acc) \<subseteq> {0..<num_acc})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F_to_idx F \<le> SPEC (\<lambda>(num_acc, acc). F = {{q. i \<in> acc q} |i. i < num_acc} \<and> \<Union> (range acc) \<subseteq> {0..<num_acc})
[PROOF STEP]
unfolding F_to_idx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SPEC (\<lambda>Flist. distinct Flist \<and> set Flist = F) \<bind> (\<lambda>Flist. let num_acc = length Flist; acc = \<lambda>v. {i. i < num_acc \<and> v \<in> Flist ! i} in RETURN (num_acc, acc)) \<le> SPEC (\<lambda>(num_acc, acc). F = {{q. i \<in> acc q} |i. i < num_acc} \<and> \<Union> (range acc) \<subseteq> {0..<num_acc})
[PROOF STEP]
apply (refine_rcg refine_vcg)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x x1 x2. \<lbrakk>distinct x \<and> set x = F; (length x, \<lambda>v. {i. i < length x \<and> v \<in> x ! i}) = (x1, x2)\<rbrakk> \<Longrightarrow> F = {{q. i \<in> x2 q} |i. i < x1}
 2. \<And>x x1 x2. \<lbrakk>distinct x \<and> set x = F; (length x, \<lambda>v. {i. i < length x \<and> v \<in> x ! i}) = (x1, x2)\<rbrakk> \<Longrightarrow> \<Union> (range x2) \<subseteq> {0..<x1}
[PROOF STEP]
apply (clarsimp dest!: sym[where t=F])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>distinct x; F = set x\<rbrakk> \<Longrightarrow> set x = {{q. i < length x \<and> q \<in> x ! i} |i. i < length x}
 2. \<And>x x1 x2. \<lbrakk>distinct x \<and> set x = F; (length x, \<lambda>v. {i. i < length x \<and> v \<in> x ! i}) = (x1, x2)\<rbrakk> \<Longrightarrow> \<Union> (range x2) \<subseteq> {0..<x1}
[PROOF STEP]
apply (intro equalityI subsetI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x xa. \<lbrakk>distinct x; F = set x; xa \<in> set x\<rbrakk> \<Longrightarrow> xa \<in> {{q. i < length x \<and> q \<in> x ! i} |i. i < length x}
 2. \<And>x xa. \<lbrakk>distinct x; F = set x; xa \<in> {{q. i < length x \<and> q \<in> x ! i} |i. i < length x}\<rbrakk> \<Longrightarrow> xa \<in> set x
 3. \<And>x x1 x2. \<lbrakk>distinct x \<and> set x = F; (length x, \<lambda>v. {i. i < length x \<and> v \<in> x ! i}) = (x1, x2)\<rbrakk> \<Longrightarrow> \<Union> (range x2) \<subseteq> {0..<x1}
[PROOF STEP]
apply (auto simp: in_set_conv_nth) [2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x x1 x2. \<lbrakk>distinct x \<and> set x = F; (length x, \<lambda>v. {i. i < length x \<and> v \<in> x ! i}) = (x1, x2)\<rbrakk> \<Longrightarrow> \<Union> (range x2) \<subseteq> {0..<x1}
[PROOF STEP]
apply auto []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mk_acc_impl_correct:
  assumes F: "(Flist',Flist)\<in>Id"
  assumes FIN: "\<forall>A\<in>set Flist. finite A"
  shows "mk_acc_impl Flist' \<le> \<Down>Id (RETURN (\<lambda>v. {i . i<length Flist \<and> v\<in>Flist!i}))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_acc_impl Flist' \<le> \<Down> Id (RETURN (\<lambda>v. {i. i < length Flist \<and> v \<in> Flist ! i}))
[PROOF STEP]
using F
[PROOF STATE]
proof (prove)
using this:
(Flist', Flist) \<in> Id

goal (1 subgoal):
 1. mk_acc_impl Flist' \<le> \<Down> Id (RETURN (\<lambda>v. {i. i < length Flist \<and> v \<in> Flist ! i}))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Flist' = Flist \<Longrightarrow> mk_acc_impl Flist \<le> RETURN (\<lambda>v. {i. i < length Flist \<and> v \<in> Flist ! i})
[PROOF STEP]
unfolding mk_acc_impl_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Flist' = Flist \<Longrightarrow> (let acc = Map.empty in nfoldli Flist (\<lambda>_. True) (\<lambda>A (i, acc). FOREACH\<^bsup>\<lambda>it acc'. acc' = (\<lambda>v. if v \<in> A - it then Some (insert i (the_default {} (acc v))) else acc v)\<^esup> A (\<lambda>v acc. RETURN (acc(v \<mapsto> insert i (the_default {} (acc v))))) acc \<bind> (\<lambda>acc. RETURN (Suc i, acc))) (0, acc) \<bind> (\<lambda>(uu_, acc). RETURN (\<lambda>x. the_default {} (acc x)))) \<le> RETURN (\<lambda>v. {i. i < length Flist \<and> v \<in> Flist ! i})
[PROOF STEP]
apply (refine_rcg
    nfoldli_rule[where
      I="\<lambda>l1 l2 (i,res). i=length l1
        \<and> the_default {} o res = (\<lambda>v. {j . j<i \<and> v\<in>Flist!j})"
    ]
    refine_vcg
  )
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>x1 x2. \<lbrakk>Flist' = Flist; (0, Map.empty) = (x1, x2)\<rbrakk> \<Longrightarrow> x1 = length []
 2. \<And>x1 x2. \<lbrakk>Flist' = Flist; (0, Map.empty) = (x1, x2)\<rbrakk> \<Longrightarrow> the_default {} \<circ> x2 = (\<lambda>v. {j. j < x1 \<and> v \<in> Flist ! j})
 3. \<And>x l1 l2 \<sigma> a b. \<lbrakk>Flist' = Flist; Flist = l1 @ x # l2; case \<sigma> of (i, res) \<Rightarrow> i = length l1 \<and> the_default {} \<circ> res = (\<lambda>v. {j. j < i \<and> v \<in> Flist ! j}); True; \<sigma> = (a, b)\<rbrakk> \<Longrightarrow> finite x
 4. \<And>x l1 l2 \<sigma> a b. \<lbrakk>Flist' = Flist; Flist = l1 @ x # l2; case \<sigma> of (i, res) \<Rightarrow> i = length l1 \<and> the_default {} \<circ> res = (\<lambda>v. {j. j < i \<and> v \<in> Flist ! j}); True; \<sigma> = (a, b)\<rbrakk> \<Longrightarrow> b = (\<lambda>v. if v \<in> x - x then Some (insert a (the_default {} (b v))) else b v)
 5. \<And>x l1 l2 \<sigma> a b xa it \<sigma>'. \<lbrakk>Flist' = Flist; Flist = l1 @ x # l2; case \<sigma> of (i, res) \<Rightarrow> i = length l1 \<and> the_default {} \<circ> res = (\<lambda>v. {j. j < i \<and> v \<in> Flist ! j}); True; \<sigma> = (a, b); xa \<in> it; it \<subseteq> x; \<sigma>' = (\<lambda>v. if v \<in> x - it then Some (insert a (the_default {} (b v))) else b v)\<rbrakk> \<Longrightarrow> \<sigma>'(xa \<mapsto> insert a (the_default {} (\<sigma>' xa))) = (\<lambda>v. if v \<in> x - (it - {xa}) then Some (insert a (the_default {} (b v))) else b v)
 6. \<And>x l1 l2 \<sigma> a b \<sigma>' x1 x2. \<lbrakk>Flist' = Flist; Flist = l1 @ x # l2; case \<sigma> of (i, res) \<Rightarrow> i = length l1 \<and> the_default {} \<circ> res = (\<lambda>v. {j. j < i \<and> v \<in> Flist ! j}); True; \<sigma> = (a, b); \<sigma>' = (\<lambda>v. if v \<in> x - {} then Some (insert a (the_default {} (b v))) else b v); (Suc a, \<sigma>') = (x1, x2)\<rbrakk> \<Longrightarrow> x1 = length (l1 @ [x])
 7. \<And>x l1 l2 \<sigma> a b \<sigma>' x1 x2. \<lbrakk>Flist' = Flist; Flist = l1 @ x # l2; case \<sigma> of (i, res) \<Rightarrow> i = length l1 \<and> the_default {} \<circ> res = (\<lambda>v. {j. j < i \<and> v \<in> Flist ! j}); True; \<sigma> = (a, b); \<sigma>' = (\<lambda>v. if v \<in> x - {} then Some (insert a (the_default {} (b v))) else b v); (Suc a, \<sigma>') = (x1, x2)\<rbrakk> \<Longrightarrow> the_default {} \<circ> x2 = (\<lambda>v. {j. j < x1 \<and> v \<in> Flist ! j})
 8. \<And>l1 l2 \<sigma> a b. \<lbrakk>Flist' = Flist; Flist = l1 @ l2; case \<sigma> of (i, res) \<Rightarrow> i = length l1 \<and> the_default {} \<circ> res = (\<lambda>v. {j. j < i \<and> v \<in> Flist ! j}); \<not> True; \<sigma> = (a, b)\<rbrakk> \<Longrightarrow> (\<lambda>v. {i. i < length Flist \<and> v \<in> Flist ! i}) = (\<lambda>x. the_default {} (b x))
 9. \<And>\<sigma> a b. \<lbrakk>Flist' = Flist; case \<sigma> of (i, res) \<Rightarrow> i = length Flist \<and> the_default {} \<circ> res = (\<lambda>v. {j. j < i \<and> v \<in> Flist ! j}); True; \<sigma> = (a, b)\<rbrakk> \<Longrightarrow> (\<lambda>v. {i. i < length Flist \<and> v \<in> Flist ! i}) = (\<lambda>x. the_default {} (b x))
[PROOF STEP]
using FIN
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>set Flist. finite A

goal (9 subgoals):
 1. \<And>x1 x2. \<lbrakk>Flist' = Flist; (0, Map.empty) = (x1, x2)\<rbrakk> \<Longrightarrow> x1 = length []
 2. \<And>x1 x2. \<lbrakk>Flist' = Flist; (0, Map.empty) = (x1, x2)\<rbrakk> \<Longrightarrow> the_default {} \<circ> x2 = (\<lambda>v. {j. j < x1 \<and> v \<in> Flist ! j})
 3. \<And>x l1 l2 \<sigma> a b. \<lbrakk>Flist' = Flist; Flist = l1 @ x # l2; case \<sigma> of (i, res) \<Rightarrow> i = length l1 \<and> the_default {} \<circ> res = (\<lambda>v. {j. j < i \<and> v \<in> Flist ! j}); True; \<sigma> = (a, b)\<rbrakk> \<Longrightarrow> finite x
 4. \<And>x l1 l2 \<sigma> a b. \<lbrakk>Flist' = Flist; Flist = l1 @ x # l2; case \<sigma> of (i, res) \<Rightarrow> i = length l1 \<and> the_default {} \<circ> res = (\<lambda>v. {j. j < i \<and> v \<in> Flist ! j}); True; \<sigma> = (a, b)\<rbrakk> \<Longrightarrow> b = (\<lambda>v. if v \<in> x - x then Some (insert a (the_default {} (b v))) else b v)
 5. \<And>x l1 l2 \<sigma> a b xa it \<sigma>'. \<lbrakk>Flist' = Flist; Flist = l1 @ x # l2; case \<sigma> of (i, res) \<Rightarrow> i = length l1 \<and> the_default {} \<circ> res = (\<lambda>v. {j. j < i \<and> v \<in> Flist ! j}); True; \<sigma> = (a, b); xa \<in> it; it \<subseteq> x; \<sigma>' = (\<lambda>v. if v \<in> x - it then Some (insert a (the_default {} (b v))) else b v)\<rbrakk> \<Longrightarrow> \<sigma>'(xa \<mapsto> insert a (the_default {} (\<sigma>' xa))) = (\<lambda>v. if v \<in> x - (it - {xa}) then Some (insert a (the_default {} (b v))) else b v)
 6. \<And>x l1 l2 \<sigma> a b \<sigma>' x1 x2. \<lbrakk>Flist' = Flist; Flist = l1 @ x # l2; case \<sigma> of (i, res) \<Rightarrow> i = length l1 \<and> the_default {} \<circ> res = (\<lambda>v. {j. j < i \<and> v \<in> Flist ! j}); True; \<sigma> = (a, b); \<sigma>' = (\<lambda>v. if v \<in> x - {} then Some (insert a (the_default {} (b v))) else b v); (Suc a, \<sigma>') = (x1, x2)\<rbrakk> \<Longrightarrow> x1 = length (l1 @ [x])
 7. \<And>x l1 l2 \<sigma> a b \<sigma>' x1 x2. \<lbrakk>Flist' = Flist; Flist = l1 @ x # l2; case \<sigma> of (i, res) \<Rightarrow> i = length l1 \<and> the_default {} \<circ> res = (\<lambda>v. {j. j < i \<and> v \<in> Flist ! j}); True; \<sigma> = (a, b); \<sigma>' = (\<lambda>v. if v \<in> x - {} then Some (insert a (the_default {} (b v))) else b v); (Suc a, \<sigma>') = (x1, x2)\<rbrakk> \<Longrightarrow> the_default {} \<circ> x2 = (\<lambda>v. {j. j < x1 \<and> v \<in> Flist ! j})
 8. \<And>l1 l2 \<sigma> a b. \<lbrakk>Flist' = Flist; Flist = l1 @ l2; case \<sigma> of (i, res) \<Rightarrow> i = length l1 \<and> the_default {} \<circ> res = (\<lambda>v. {j. j < i \<and> v \<in> Flist ! j}); \<not> True; \<sigma> = (a, b)\<rbrakk> \<Longrightarrow> (\<lambda>v. {i. i < length Flist \<and> v \<in> Flist ! i}) = (\<lambda>x. the_default {} (b x))
 9. \<And>\<sigma> a b. \<lbrakk>Flist' = Flist; case \<sigma> of (i, res) \<Rightarrow> i = length Flist \<and> the_default {} \<circ> res = (\<lambda>v. {j. j < i \<and> v \<in> Flist ! j}); True; \<sigma> = (a, b)\<rbrakk> \<Longrightarrow> (\<lambda>v. {i. i < length Flist \<and> v \<in> Flist ! i}) = (\<lambda>x. the_default {} (b x))
[PROOF STEP]
apply (simp_all)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1. \<lbrakk>Flist' = Flist; x1 = 0; \<forall>x\<in>set Flist. finite x\<rbrakk> \<Longrightarrow> the_default {} \<circ> Map.empty = (\<lambda>v. {})
 2. \<And>x l1 l2 \<sigma> b xa it \<sigma>'. \<lbrakk>Flist' = l1 @ x # l2; Flist = l1 @ x # l2; the_default {} \<circ> b = (\<lambda>v. {j. j < length l1 \<and> v \<in> (l1 @ x # l2) ! j}); \<sigma> = (length l1, b); xa \<in> it; it \<subseteq> x; \<sigma>' = (\<lambda>v. if v \<in> x \<and> v \<notin> it then Some (insert (length l1) (the_default {} (b v))) else b v); finite x \<and> (\<forall>x\<in>set l1 \<union> set l2. finite x)\<rbrakk> \<Longrightarrow> (\<lambda>v. if v \<in> x \<and> v \<notin> it then Some (insert (length l1) (the_default {} (b v))) else b v)(xa \<mapsto> insert (length l1) (the_default {} (b xa))) = (\<lambda>v. if v \<in> x \<and> (v \<in> it \<longrightarrow> v = xa) then Some (insert (length l1) (the_default {} (b v))) else b v)
 3. \<And>x l1 l2 \<sigma> b \<sigma>' x1. \<lbrakk>Flist' = l1 @ x # l2; Flist = l1 @ x # l2; the_default {} \<circ> b = (\<lambda>v. {j. j < length l1 \<and> v \<in> (l1 @ x # l2) ! j}); \<sigma> = (length l1, b); \<sigma>' = (\<lambda>v. if v \<in> x then Some (insert (length l1) (the_default {} (b v))) else b v); Suc (length l1) = x1; finite x \<and> (\<forall>x\<in>set l1 \<union> set l2. finite x)\<rbrakk> \<Longrightarrow> the_default {} \<circ> (\<lambda>v. if v \<in> x then Some (insert (length l1) (the_default {} (b v))) else b v) = (\<lambda>v. {j. j < x1 \<and> v \<in> (l1 @ x # l2) ! j})
 4. \<And>\<sigma> b. \<lbrakk>Flist' = Flist; the_default {} \<circ> b = (\<lambda>v. {j. j < length Flist \<and> v \<in> Flist ! j}); \<sigma> = (length Flist, b); \<forall>x\<in>set Flist. finite x\<rbrakk> \<Longrightarrow> (\<lambda>v. {i. i < length Flist \<and> v \<in> Flist ! i}) = (\<lambda>x. the_default {} (b x))
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1 v. \<lbrakk>Flist' = Flist; x1 = 0; \<forall>x\<in>set Flist. finite x\<rbrakk> \<Longrightarrow> (the_default {} \<circ> Map.empty) v = {}
 2. \<And>x l1 l2 \<sigma> b xa it \<sigma>'. \<lbrakk>Flist' = l1 @ x # l2; Flist = l1 @ x # l2; the_default {} \<circ> b = (\<lambda>v. {j. j < length l1 \<and> v \<in> (l1 @ x # l2) ! j}); \<sigma> = (length l1, b); xa \<in> it; it \<subseteq> x; \<sigma>' = (\<lambda>v. if v \<in> x \<and> v \<notin> it then Some (insert (length l1) (the_default {} (b v))) else b v); finite x \<and> (\<forall>x\<in>set l1 \<union> set l2. finite x)\<rbrakk> \<Longrightarrow> (\<lambda>v. if v \<in> x \<and> v \<notin> it then Some (insert (length l1) (the_default {} (b v))) else b v)(xa \<mapsto> insert (length l1) (the_default {} (b xa))) = (\<lambda>v. if v \<in> x \<and> (v \<in> it \<longrightarrow> v = xa) then Some (insert (length l1) (the_default {} (b v))) else b v)
 3. \<And>x l1 l2 \<sigma> b \<sigma>' x1. \<lbrakk>Flist' = l1 @ x # l2; Flist = l1 @ x # l2; the_default {} \<circ> b = (\<lambda>v. {j. j < length l1 \<and> v \<in> (l1 @ x # l2) ! j}); \<sigma> = (length l1, b); \<sigma>' = (\<lambda>v. if v \<in> x then Some (insert (length l1) (the_default {} (b v))) else b v); Suc (length l1) = x1; finite x \<and> (\<forall>x\<in>set l1 \<union> set l2. finite x)\<rbrakk> \<Longrightarrow> the_default {} \<circ> (\<lambda>v. if v \<in> x then Some (insert (length l1) (the_default {} (b v))) else b v) = (\<lambda>v. {j. j < x1 \<and> v \<in> (l1 @ x # l2) ! j})
 4. \<And>\<sigma> b. \<lbrakk>Flist' = Flist; the_default {} \<circ> b = (\<lambda>v. {j. j < length Flist \<and> v \<in> Flist ! j}); \<sigma> = (length Flist, b); \<forall>x\<in>set Flist. finite x\<rbrakk> \<Longrightarrow> (\<lambda>v. {i. i < length Flist \<and> v \<in> Flist ! i}) = (\<lambda>x. the_default {} (b x))
[PROOF STEP]
apply auto []
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x l1 l2 \<sigma> b xa it \<sigma>'. \<lbrakk>Flist' = l1 @ x # l2; Flist = l1 @ x # l2; the_default {} \<circ> b = (\<lambda>v. {j. j < length l1 \<and> v \<in> (l1 @ x # l2) ! j}); \<sigma> = (length l1, b); xa \<in> it; it \<subseteq> x; \<sigma>' = (\<lambda>v. if v \<in> x \<and> v \<notin> it then Some (insert (length l1) (the_default {} (b v))) else b v); finite x \<and> (\<forall>x\<in>set l1 \<union> set l2. finite x)\<rbrakk> \<Longrightarrow> (\<lambda>v. if v \<in> x \<and> v \<notin> it then Some (insert (length l1) (the_default {} (b v))) else b v)(xa \<mapsto> insert (length l1) (the_default {} (b xa))) = (\<lambda>v. if v \<in> x \<and> (v \<in> it \<longrightarrow> v = xa) then Some (insert (length l1) (the_default {} (b v))) else b v)
 2. \<And>x l1 l2 \<sigma> b \<sigma>' x1. \<lbrakk>Flist' = l1 @ x # l2; Flist = l1 @ x # l2; the_default {} \<circ> b = (\<lambda>v. {j. j < length l1 \<and> v \<in> (l1 @ x # l2) ! j}); \<sigma> = (length l1, b); \<sigma>' = (\<lambda>v. if v \<in> x then Some (insert (length l1) (the_default {} (b v))) else b v); Suc (length l1) = x1; finite x \<and> (\<forall>x\<in>set l1 \<union> set l2. finite x)\<rbrakk> \<Longrightarrow> the_default {} \<circ> (\<lambda>v. if v \<in> x then Some (insert (length l1) (the_default {} (b v))) else b v) = (\<lambda>v. {j. j < x1 \<and> v \<in> (l1 @ x # l2) ! j})
 3. \<And>\<sigma> b. \<lbrakk>Flist' = Flist; the_default {} \<circ> b = (\<lambda>v. {j. j < length Flist \<and> v \<in> Flist ! j}); \<sigma> = (length Flist, b); \<forall>x\<in>set Flist. finite x\<rbrakk> \<Longrightarrow> (\<lambda>v. {i. i < length Flist \<and> v \<in> Flist ! i}) = (\<lambda>x. the_default {} (b x))
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x l1 l2 \<sigma> b xa it \<sigma>' v. \<lbrakk>Flist' = l1 @ x # l2; Flist = l1 @ x # l2; the_default {} \<circ> b = (\<lambda>v. {j. j < length l1 \<and> v \<in> (l1 @ x # l2) ! j}); \<sigma> = (length l1, b); xa \<in> it; it \<subseteq> x; \<sigma>' = (\<lambda>v. if v \<in> x \<and> v \<notin> it then Some (insert (length l1) (the_default {} (b v))) else b v); finite x \<and> (\<forall>x\<in>set l1 \<union> set l2. finite x)\<rbrakk> \<Longrightarrow> ((\<lambda>v. if v \<in> x \<and> v \<notin> it then Some (insert (length l1) (the_default {} (b v))) else b v)(xa \<mapsto> insert (length l1) (the_default {} (b xa)))) v = (if v \<in> x \<and> (v \<in> it \<longrightarrow> v = xa) then Some (insert (length l1) (the_default {} (b v))) else b v)
 2. \<And>x l1 l2 \<sigma> b \<sigma>' x1. \<lbrakk>Flist' = l1 @ x # l2; Flist = l1 @ x # l2; the_default {} \<circ> b = (\<lambda>v. {j. j < length l1 \<and> v \<in> (l1 @ x # l2) ! j}); \<sigma> = (length l1, b); \<sigma>' = (\<lambda>v. if v \<in> x then Some (insert (length l1) (the_default {} (b v))) else b v); Suc (length l1) = x1; finite x \<and> (\<forall>x\<in>set l1 \<union> set l2. finite x)\<rbrakk> \<Longrightarrow> the_default {} \<circ> (\<lambda>v. if v \<in> x then Some (insert (length l1) (the_default {} (b v))) else b v) = (\<lambda>v. {j. j < x1 \<and> v \<in> (l1 @ x # l2) ! j})
 3. \<And>\<sigma> b. \<lbrakk>Flist' = Flist; the_default {} \<circ> b = (\<lambda>v. {j. j < length Flist \<and> v \<in> Flist ! j}); \<sigma> = (length Flist, b); \<forall>x\<in>set Flist. finite x\<rbrakk> \<Longrightarrow> (\<lambda>v. {i. i < length Flist \<and> v \<in> Flist ! i}) = (\<lambda>x. the_default {} (b x))
[PROOF STEP]
apply (auto split: if_split_asm simp: nth_append nth_Cons') []
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x l1 l2 \<sigma> b \<sigma>' x1. \<lbrakk>Flist' = l1 @ x # l2; Flist = l1 @ x # l2; the_default {} \<circ> b = (\<lambda>v. {j. j < length l1 \<and> v \<in> (l1 @ x # l2) ! j}); \<sigma> = (length l1, b); \<sigma>' = (\<lambda>v. if v \<in> x then Some (insert (length l1) (the_default {} (b v))) else b v); Suc (length l1) = x1; finite x \<and> (\<forall>x\<in>set l1 \<union> set l2. finite x)\<rbrakk> \<Longrightarrow> the_default {} \<circ> (\<lambda>v. if v \<in> x then Some (insert (length l1) (the_default {} (b v))) else b v) = (\<lambda>v. {j. j < x1 \<and> v \<in> (l1 @ x # l2) ! j})
 2. \<And>\<sigma> b. \<lbrakk>Flist' = Flist; the_default {} \<circ> b = (\<lambda>v. {j. j < length Flist \<and> v \<in> Flist ! j}); \<sigma> = (length Flist, b); \<forall>x\<in>set Flist. finite x\<rbrakk> \<Longrightarrow> (\<lambda>v. {i. i < length Flist \<and> v \<in> Flist ! i}) = (\<lambda>x. the_default {} (b x))
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x l1 l2 \<sigma> b \<sigma>' x1 v. \<lbrakk>Flist' = l1 @ x # l2; Flist = l1 @ x # l2; the_default {} \<circ> b = (\<lambda>v. {j. j < length l1 \<and> v \<in> (l1 @ x # l2) ! j}); \<sigma> = (length l1, b); \<sigma>' = (\<lambda>v. if v \<in> x then Some (insert (length l1) (the_default {} (b v))) else b v); Suc (length l1) = x1; finite x \<and> (\<forall>x\<in>set l1 \<union> set l2. finite x)\<rbrakk> \<Longrightarrow> (the_default {} \<circ> (\<lambda>v. if v \<in> x then Some (insert (length l1) (the_default {} (b v))) else b v)) v = {j. j < x1 \<and> v \<in> (l1 @ x # l2) ! j}
 2. \<And>\<sigma> b. \<lbrakk>Flist' = Flist; the_default {} \<circ> b = (\<lambda>v. {j. j < length Flist \<and> v \<in> Flist ! j}); \<sigma> = (length Flist, b); \<forall>x\<in>set Flist. finite x\<rbrakk> \<Longrightarrow> (\<lambda>v. {i. i < length Flist \<and> v \<in> Flist ! i}) = (\<lambda>x. the_default {} (b x))
[PROOF STEP]
apply (auto split: if_split_asm simp: nth_append nth_Cons'
    fun_comp_eq_conv) []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> b. \<lbrakk>Flist' = Flist; the_default {} \<circ> b = (\<lambda>v. {j. j < length Flist \<and> v \<in> Flist ! j}); \<sigma> = (length Flist, b); \<forall>x\<in>set Flist. finite x\<rbrakk> \<Longrightarrow> (\<lambda>v. {i. i < length Flist \<and> v \<in> Flist ! i}) = (\<lambda>x. the_default {} (b x))
[PROOF STEP]
apply (rule ext)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> b v. \<lbrakk>Flist' = Flist; the_default {} \<circ> b = (\<lambda>v. {j. j < length Flist \<and> v \<in> Flist ! j}); \<sigma> = (length Flist, b); \<forall>x\<in>set Flist. finite x\<rbrakk> \<Longrightarrow> {i. i < length Flist \<and> v \<in> Flist ! i} = the_default {} (b v)
[PROOF STEP]
apply (auto simp: fun_comp_eq_conv) []
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma F_to_idx_refine:
  assumes FIN: "\<forall>A\<in>F. finite A"
  shows "F_to_idx_impl F \<le> \<Down>Id (F_to_idx F)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F_to_idx_impl F \<le> \<Down> Id (F_to_idx F)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>F. finite A

goal (1 subgoal):
 1. F_to_idx_impl F \<le> \<Down> Id (F_to_idx F)
[PROOF STEP]
unfolding F_to_idx_impl_def F_to_idx_def
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>F. finite A

goal (1 subgoal):
 1. SPEC (\<lambda>Flist. distinct Flist \<and> set Flist = F) \<bind> (\<lambda>Flist. let num_acc = length Flist in mk_acc_impl Flist \<bind> (\<lambda>acc. RETURN (num_acc, acc))) \<le> \<Down> Id (SPEC (\<lambda>Flist. distinct Flist \<and> set Flist = F) \<bind> (\<lambda>Flist. let num_acc = length Flist; acc = \<lambda>v. {i. i < num_acc \<and> v \<in> Flist ! i} in RETURN (num_acc, acc)))
[PROOF STEP]
apply (refine_rcg bind_Let_refine2[OF mk_acc_impl_correct])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Flist Flista. \<lbrakk>\<forall>A\<in>F. finite A; (Flist, Flista) \<in> Id; Flist \<in> {Flist. distinct Flist \<and> set Flist = F}; Flista \<in> {Flist. distinct Flist \<and> set Flist = F}\<rbrakk> \<Longrightarrow> \<forall>A\<in>set Flista. finite A
 2. \<And>Flist Flista acc. \<lbrakk>\<forall>A\<in>F. finite A; (Flist, Flista) \<in> Id; Flist \<in> {Flist. distinct Flist \<and> set Flist = F}; Flista \<in> {Flist. distinct Flist \<and> set Flist = F}; inres (mk_acc_impl Flist) acc; (acc, \<lambda>v. {i. i < length Flista \<and> v \<in> Flista ! i}) \<in> Id\<rbrakk> \<Longrightarrow> ((length Flist, acc), length Flista, \<lambda>v. {i. i < length Flista \<and> v \<in> Flista ! i}) \<in> Id
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma (in gb_graph) gbg_to_idx_ext_correct:
  assumes [simp, intro]: "\<And> A. A \<in> F \<Longrightarrow> finite A"
  shows "gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'.
    igb_graph.is_acc_run G' = is_acc_run
  \<and> g_V G' = V
  \<and> g_E G' = E
  \<and> g_V0 G' = V0
  \<and> igb_graph_rec.more G' = ecnv G
  \<and> igb_graph G'
)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
note F_to_idx_refine[of F]
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>F. finite A \<Longrightarrow> F_to_idx_impl F \<le> \<Down> Id (F_to_idx F)

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<forall>A\<in>F. finite A \<Longrightarrow> F_to_idx_impl F \<le> \<Down> Id (F_to_idx F)

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
note F_to_idx_correct
[PROOF STATE]
proof (state)
this:
F_to_idx ?F \<le> SPEC (\<lambda>(num_acc, acc). ?F = {{q. i \<in> acc q} |i. i < num_acc} \<and> \<Union> (range acc) \<subseteq> {0..<num_acc})

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<forall>A\<in>F. finite A \<Longrightarrow> F_to_idx_impl F \<le> SPEC (\<lambda>(num_acc, acc). F = {{q. i \<in> acc q} |i. i < num_acc} \<and> \<Union> (range acc) \<subseteq> {0..<num_acc})
[PROOF STEP]
have R: "F_to_idx_impl F
    \<le> SPEC (\<lambda>(num_acc, acc). F = {{q. i \<in> acc q} |i. i < num_acc}
      \<and> \<Union>(range acc) \<subseteq> {0..<num_acc})"
[PROOF STATE]
proof (prove)
using this:
\<forall>A\<in>F. finite A \<Longrightarrow> F_to_idx_impl F \<le> SPEC (\<lambda>(num_acc, acc). F = {{q. i \<in> acc q} |i. i < num_acc} \<and> \<Union> (range acc) \<subseteq> {0..<num_acc})

goal (1 subgoal):
 1. F_to_idx_impl F \<le> SPEC (\<lambda>(num_acc, acc). F = {{q. i \<in> acc q} |i. i < num_acc} \<and> \<Union> (range acc) \<subseteq> {0..<num_acc})
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
F_to_idx_impl F \<le> SPEC (\<lambda>(num_acc, acc). F = {{q. i \<in> acc q} |i. i < num_acc} \<and> \<Union> (range acc) \<subseteq> {0..<num_acc})

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
have eq_conjI: "\<And>a b c. (b\<longleftrightarrow>c) \<Longrightarrow> (a&b \<longleftrightarrow> a&c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. b = c \<Longrightarrow> (a \<and> b) = (a \<and> c)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?b = ?c \<Longrightarrow> (?a \<and> ?b) = (?a \<and> ?c)

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?b = ?c \<Longrightarrow> (?a \<and> ?b) = (?a \<and> ?c)

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
fix acc :: "'Q \<Rightarrow> nat set" and num_acc r
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
have "(\<forall>A. (\<exists>i. A = {q. i \<in> acc q} \<and> i < num_acc) \<longrightarrow> (limit r \<inter> A \<noteq> {}))
      \<longleftrightarrow> (\<forall>i<num_acc. \<exists>q\<in>limit r. i\<in>acc q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>A. (\<exists>i. A = {q. i \<in> acc q} \<and> i < num_acc) \<longrightarrow> limit r \<inter> A \<noteq> {}) = (\<forall>i<num_acc. \<exists>q\<in>limit r. i \<in> acc q)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<forall>A. (\<exists>i. A = {q. i \<in> acc q} \<and> i < num_acc) \<longrightarrow> limit r \<inter> A \<noteq> {}) = (\<forall>i<num_acc. \<exists>q\<in>limit r. i \<in> acc q)

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(\<forall>A. (\<exists>i. A = {q. i \<in> ?acc2 q} \<and> i < ?num_acc2) \<longrightarrow> limit ?r2 \<inter> A \<noteq> {}) = (\<forall>i<?num_acc2. \<exists>q\<in>limit ?r2. i \<in> ?acc2 q)

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
note aux1=this
[PROOF STATE]
proof (state)
this:
(\<forall>A. (\<exists>i. A = {q. i \<in> ?acc2 q} \<and> i < ?num_acc2) \<longrightarrow> limit ?r2 \<inter> A \<noteq> {}) = (\<forall>i<?num_acc2. \<exists>q\<in>limit ?r2. i \<in> ?acc2 q)

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(\<forall>A. (\<exists>i. A = {q. i \<in> ?acc2 q} \<and> i < ?num_acc2) \<longrightarrow> limit ?r2 \<inter> A \<noteq> {}) = (\<forall>i<?num_acc2. \<exists>q\<in>limit ?r2. i \<in> ?acc2 q)

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
fix acc :: "'Q \<Rightarrow> nat set" and num_acc i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
assume FE: "F = {{q. i \<in> acc q} |i. i < num_acc}"
[PROOF STATE]
proof (state)
this:
F = {{q. i \<in> acc q} |i. i < num_acc}

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
assume INR: "(\<Union>x. acc x) \<subseteq> {0..<num_acc}"
[PROOF STATE]
proof (state)
this:
\<Union> (range acc) \<subseteq> {0..<num_acc}

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
have "finite {q. i \<in> acc q}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite {q. i \<in> acc q}
[PROOF STEP]
proof (cases "i<num_acc")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. i < num_acc \<Longrightarrow> finite {q. i \<in> acc q}
 2. \<not> i < num_acc \<Longrightarrow> finite {q. i \<in> acc q}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
i < num_acc

goal (2 subgoals):
 1. i < num_acc \<Longrightarrow> finite {q. i \<in> acc q}
 2. \<not> i < num_acc \<Longrightarrow> finite {q. i \<in> acc q}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
i < num_acc

goal (1 subgoal):
 1. finite {q. i \<in> acc q}
[PROOF STEP]
using FE
[PROOF STATE]
proof (prove)
using this:
i < num_acc
F = {{q. i \<in> acc q} |i. i < num_acc}

goal (1 subgoal):
 1. finite {q. i \<in> acc q}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
finite {q. i \<in> acc q}

goal (1 subgoal):
 1. \<not> i < num_acc \<Longrightarrow> finite {q. i \<in> acc q}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> i < num_acc \<Longrightarrow> finite {q. i \<in> acc q}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> i < num_acc

goal (1 subgoal):
 1. \<not> i < num_acc \<Longrightarrow> finite {q. i \<in> acc q}
[PROOF STEP]
hence "{q. i \<in> acc q} = {}"
[PROOF STATE]
proof (prove)
using this:
\<not> i < num_acc

goal (1 subgoal):
 1. {q. i \<in> acc q} = {}
[PROOF STEP]
using INR
[PROOF STATE]
proof (prove)
using this:
\<not> i < num_acc
\<Union> (range acc) \<subseteq> {0..<num_acc}

goal (1 subgoal):
 1. {q. i \<in> acc q} = {}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
{q. i \<in> acc q} = {}

goal (1 subgoal):
 1. \<not> i < num_acc \<Longrightarrow> finite {q. i \<in> acc q}
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
{q. i \<in> acc q} = {}

goal (1 subgoal):
 1. finite {q. i \<in> acc q}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
finite {q. i \<in> acc q}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
finite {q. i \<in> acc q}

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>F = {{q. i \<in> ?acc2 q} |i. i < ?num_acc2}; \<Union> (range ?acc2) \<subseteq> {0..<?num_acc2}\<rbrakk> \<Longrightarrow> finite {q. ?i2 \<in> ?acc2 q}

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
note aux2=this
[PROOF STATE]
proof (state)
this:
\<lbrakk>F = {{q. i \<in> ?acc2 q} |i. i < ?num_acc2}; \<Union> (range ?acc2) \<subseteq> {0..<?num_acc2}\<rbrakk> \<Longrightarrow> finite {q. ?i2 \<in> ?acc2 q}

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>F = {{q. i \<in> ?acc2 q} |i. i < ?num_acc2}; \<Union> (range ?acc2) \<subseteq> {0..<?num_acc2}\<rbrakk> \<Longrightarrow> finite {q. ?i2 \<in> ?acc2 q}

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
fix acc :: "'Q \<Rightarrow> nat set" and num_acc q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
assume FE: "F = {{q. i \<in> acc q} |i. i < num_acc}"
      and INR: "(\<Union>x. acc x) \<subseteq> {0..<num_acc}"
      and "acc q \<noteq> {}"
[PROOF STATE]
proof (state)
this:
F = {{q. i \<in> acc q} |i. i < num_acc}
\<Union> (range acc) \<subseteq> {0..<num_acc}
acc q \<noteq> {}

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
F = {{q. i \<in> acc q} |i. i < num_acc}
\<Union> (range acc) \<subseteq> {0..<num_acc}
acc q \<noteq> {}
[PROOF STEP]
obtain i where "i\<in>acc q"
[PROOF STATE]
proof (prove)
using this:
F = {{q. i \<in> acc q} |i. i < num_acc}
\<Union> (range acc) \<subseteq> {0..<num_acc}
acc q \<noteq> {}

goal (1 subgoal):
 1. (\<And>i. i \<in> acc q \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i \<in> acc q

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
i \<in> acc q

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
with INR
[PROOF STATE]
proof (chain)
picking this:
\<Union> (range acc) \<subseteq> {0..<num_acc}
i \<in> acc q
[PROOF STEP]
have "i<num_acc"
[PROOF STATE]
proof (prove)
using this:
\<Union> (range acc) \<subseteq> {0..<num_acc}
i \<in> acc q

goal (1 subgoal):
 1. i < num_acc
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
i < num_acc

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
i \<in> acc q
i < num_acc
[PROOF STEP]
have "q\<in>\<Union>F"
[PROOF STATE]
proof (prove)
using this:
i \<in> acc q
i < num_acc

goal (1 subgoal):
 1. q \<in> \<Union> F
[PROOF STEP]
by (auto simp: FE)
[PROOF STATE]
proof (state)
this:
q \<in> \<Union> F

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
with F_ss
[PROOF STATE]
proof (chain)
picking this:
F \<subseteq> Pow V
q \<in> \<Union> F
[PROOF STEP]
have "q\<in>V"
[PROOF STATE]
proof (prove)
using this:
F \<subseteq> Pow V
q \<in> \<Union> F

goal (1 subgoal):
 1. q \<in> V
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
q \<in> V

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>F = {{q. i \<in> ?acc2 q} |i. i < ?num_acc2}; \<Union> (range ?acc2) \<subseteq> {0..<?num_acc2}; ?acc2 ?q2 \<noteq> {}\<rbrakk> \<Longrightarrow> ?q2 \<in> V

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
note aux3=this
[PROOF STATE]
proof (state)
this:
\<lbrakk>F = {{q. i \<in> ?acc2 q} |i. i < ?num_acc2}; \<Union> (range ?acc2) \<subseteq> {0..<?num_acc2}; ?acc2 ?q2 \<noteq> {}\<rbrakk> \<Longrightarrow> ?q2 \<in> V

goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
unfolding gbg_to_idx_ext_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. F_to_idx_impl F \<bind> (\<lambda>(num_acc, acc). RETURN \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr>) \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')
[PROOF STEP]
apply (refine_rcg order_trans[OF R] refine_vcg)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x a b. \<lbrakk>case x of (num_acc, acc) \<Rightarrow> F = {{q. i \<in> acc q} |i. i < num_acc} \<and> \<Union> (range acc) \<subseteq> {0..<num_acc}; x = (a, b)\<rbrakk> \<Longrightarrow> igb_graph.is_acc_run \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = a, igbg_acc = b, \<dots> = ecnv G\<rparr> = is_acc_run
 2. \<And>x a b. \<lbrakk>case x of (num_acc, acc) \<Rightarrow> F = {{q. i \<in> acc q} |i. i < num_acc} \<and> \<Union> (range acc) \<subseteq> {0..<num_acc}; x = (a, b)\<rbrakk> \<Longrightarrow> g_V \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = a, igbg_acc = b, \<dots> = ecnv G\<rparr> = V
 3. \<And>x a b. \<lbrakk>case x of (num_acc, acc) \<Rightarrow> F = {{q. i \<in> acc q} |i. i < num_acc} \<and> \<Union> (range acc) \<subseteq> {0..<num_acc}; x = (a, b)\<rbrakk> \<Longrightarrow> g_E \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = a, igbg_acc = b, \<dots> = ecnv G\<rparr> = E
 4. \<And>x a b. \<lbrakk>case x of (num_acc, acc) \<Rightarrow> F = {{q. i \<in> acc q} |i. i < num_acc} \<and> \<Union> (range acc) \<subseteq> {0..<num_acc}; x = (a, b)\<rbrakk> \<Longrightarrow> g_V0 \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = a, igbg_acc = b, \<dots> = ecnv G\<rparr> = V0
 5. \<And>x a b. \<lbrakk>case x of (num_acc, acc) \<Rightarrow> F = {{q. i \<in> acc q} |i. i < num_acc} \<and> \<Union> (range acc) \<subseteq> {0..<num_acc}; x = (a, b)\<rbrakk> \<Longrightarrow> igb_graph_rec.more \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = a, igbg_acc = b, \<dots> = ecnv G\<rparr> = ecnv G
 6. \<And>x a b. \<lbrakk>case x of (num_acc, acc) \<Rightarrow> F = {{q. i \<in> acc q} |i. i < num_acc} \<and> \<Union> (range acc) \<subseteq> {0..<num_acc}; x = (a, b)\<rbrakk> \<Longrightarrow> igb_graph \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = a, igbg_acc = b, \<dots> = ecnv G\<rparr>
[PROOF STEP]
proof clarsimp_all
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>F = {{q. i \<in> ba q} |i. i < aa}; \<Union> (range ba) \<subseteq> {0..<aa}\<rbrakk> \<Longrightarrow> igb_graph.is_acc_run \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = aa, igbg_acc = ba, \<dots> = ecnv G\<rparr> = is_acc_run
 2. \<And>aa ba. \<lbrakk>F = {{q. i \<in> ba q} |i. i < aa}; \<Union> (range ba) \<subseteq> {0..<aa}\<rbrakk> \<Longrightarrow> igb_graph \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = aa, igbg_acc = ba, \<dots> = ecnv G\<rparr>
[PROOF STEP]
fix acc and num_acc :: nat
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>F = {{q. i \<in> ba q} |i. i < aa}; \<Union> (range ba) \<subseteq> {0..<aa}\<rbrakk> \<Longrightarrow> igb_graph.is_acc_run \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = aa, igbg_acc = ba, \<dots> = ecnv G\<rparr> = is_acc_run
 2. \<And>aa ba. \<lbrakk>F = {{q. i \<in> ba q} |i. i < aa}; \<Union> (range ba) \<subseteq> {0..<aa}\<rbrakk> \<Longrightarrow> igb_graph \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = aa, igbg_acc = ba, \<dots> = ecnv G\<rparr>
[PROOF STEP]
assume FE[simp]: "F = {{q. i \<in> acc q} |i. i < num_acc}"
      and BOUND: "(\<Union>x. acc x) \<subseteq> {0..<num_acc}"
[PROOF STATE]
proof (state)
this:
F = {{q. i \<in> acc q} |i. i < num_acc}
\<Union> (range acc) \<subseteq> {0..<num_acc}

goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>F = {{q. i \<in> ba q} |i. i < aa}; \<Union> (range ba) \<subseteq> {0..<aa}\<rbrakk> \<Longrightarrow> igb_graph.is_acc_run \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = aa, igbg_acc = ba, \<dots> = ecnv G\<rparr> = is_acc_run
 2. \<And>aa ba. \<lbrakk>F = {{q. i \<in> ba q} |i. i < aa}; \<Union> (range ba) \<subseteq> {0..<aa}\<rbrakk> \<Longrightarrow> igb_graph \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = aa, igbg_acc = ba, \<dots> = ecnv G\<rparr>
[PROOF STEP]
let ?G' = "\<lparr>
      g_V = V,
      g_E = E,
      g_V0 = V0,
      igbg_num_acc = num_acc,
      igbg_acc = acc,
      \<dots> = ecnv G\<rparr>"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>F = {{q. i \<in> ba q} |i. i < aa}; \<Union> (range ba) \<subseteq> {0..<aa}\<rbrakk> \<Longrightarrow> igb_graph.is_acc_run \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = aa, igbg_acc = ba, \<dots> = ecnv G\<rparr> = is_acc_run
 2. \<And>aa ba. \<lbrakk>F = {{q. i \<in> ba q} |i. i < aa}; \<Union> (range ba) \<subseteq> {0..<aa}\<rbrakk> \<Longrightarrow> igb_graph \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = aa, igbg_acc = ba, \<dots> = ecnv G\<rparr>
[PROOF STEP]
interpret G': igb_graph ?G'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igb_graph \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr>
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. g_V0 \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr> \<subseteq> g_V \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr>
 2. g_E \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr> \<subseteq> g_V \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr> \<times> g_V \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr>
 3. \<Union> (range (igbg_acc \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr>)) \<subseteq> {0..<igbg_num_acc \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr>}
 4. \<And>q. igbg_acc \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr> q \<noteq> {} \<Longrightarrow> q \<in> g_V \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr>
[PROOF STEP]
using V0_ss E_ss
[PROOF STATE]
proof (prove)
using this:
V0 \<subseteq> V
E \<subseteq> V \<times> V

goal (4 subgoals):
 1. g_V0 \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr> \<subseteq> g_V \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr>
 2. g_E \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr> \<subseteq> g_V \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr> \<times> g_V \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr>
 3. \<Union> (range (igbg_acc \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr>)) \<subseteq> {0..<igbg_num_acc \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr>}
 4. \<And>q. igbg_acc \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr> q \<noteq> {} \<Longrightarrow> q \<in> g_V \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr>
[PROOF STEP]
apply (auto simp add: aux2 aux3 BOUND)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>aa ba. \<lbrakk>F = {{q. i \<in> ba q} |i. i < aa}; \<Union> (range ba) \<subseteq> {0..<aa}\<rbrakk> \<Longrightarrow> igb_graph.is_acc_run \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = aa, igbg_acc = ba, \<dots> = ecnv G\<rparr> = is_acc_run
 2. \<And>aa ba. \<lbrakk>F = {{q. i \<in> ba q} |i. i < aa}; \<Union> (range ba) \<subseteq> {0..<aa}\<rbrakk> \<Longrightarrow> igb_graph \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = aa, igbg_acc = ba, \<dots> = ecnv G\<rparr>
[PROOF STEP]
show "igb_graph ?G'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igb_graph \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr>
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
this:
igb_graph \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = num_acc, igbg_acc = acc, \<dots> = ecnv G\<rparr>

goal (1 subgoal):
 1. \<And>aa ba. \<lbrakk>F = {{q. i \<in> ba q} |i. i < aa}; \<Union> (range ba) \<subseteq> {0..<aa}\<rbrakk> \<Longrightarrow> igb_graph.is_acc_run \<lparr>g_V = V, g_E = E, g_V0 = V0, igbg_num_acc = aa, igbg_acc = ba, \<dots> = ecnv G\<rparr> = is_acc_run
[PROOF STEP]
show "G'.is_acc_run = is_acc_run"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. G'.is_acc_run = is_acc_run
[PROOF STEP]
unfolding G'.is_acc_run_def[abs_def] is_acc_run_def[abs_def]
        G'.is_run_def[abs_def] is_run_def[abs_def]
        G'.is_acc_def[abs_def] is_acc_def[abs_def]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>r. (r 0 \<in> G'.V0 \<and> ipath G'.E r) \<and> (\<forall>n<G'.num_acc. \<exists>\<^sub>\<infinity>i. n \<in> G'.acc (r i))) = (\<lambda>r. (r 0 \<in> V0 \<and> ipath E r) \<and> (\<forall>A\<in>F. \<exists>\<^sub>\<infinity>i. r i \<in> A))
[PROOF STEP]
apply (clarsimp intro!: ext eq_conjI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r. (\<forall>n<num_acc. \<exists>\<^sub>\<infinity>i. n \<in> acc (r i)) = (\<forall>A. (\<exists>i. A = {q. i \<in> acc q} \<and> i < num_acc) \<longrightarrow> (\<exists>\<^sub>\<infinity>i. r i \<in> A))
[PROOF STEP]
apply auto []
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>r n. \<lbrakk>\<forall>A. (\<exists>i. A = {q. i \<in> acc q} \<and> i < num_acc) \<longrightarrow> (\<exists>\<^sub>\<infinity>i. r i \<in> A); n < num_acc\<rbrakk> \<Longrightarrow> \<exists>\<^sub>\<infinity>i. n \<in> acc (r i)
[PROOF STEP]
apply (metis (lifting, no_types) INFM_mono mem_Collect_eq)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
G'.is_acc_run = is_acc_run

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
gbg_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ecnv G \<and> igb_graph G')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in gba) gba_to_idx_ext_correct:
  assumes [simp, intro]: "\<And> A. A \<in> F \<Longrightarrow> finite A"
  shows "gba_to_idx_ext ecnv G \<le>
    SPEC (\<lambda>G'.
    igba.accept G' = accept
  \<and> g_V G' = V
  \<and> g_E G' = E
  \<and> g_V0 G' = V0
  \<and> igba_rec.more G' = ecnv G
  \<and> igba G')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gba_to_idx_ext ecnv G \<le> SPEC (\<lambda>G'. igba.accept G' = accept \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igba_rec.more G' = ecnv G \<and> igba G')
[PROOF STEP]
apply (rule order_trans[OF gbg_to_idx_ext_correct])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>A. A \<in> F \<Longrightarrow> finite A
 2. SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ti_Lcnv ecnv G \<and> igb_graph G') \<le> SPEC (\<lambda>G'. igba.accept G' = accept \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igba_rec.more G' = ecnv G \<and> igba G')
[PROOF STEP]
apply (rule, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SPEC (\<lambda>G'. igb_graph.is_acc_run G' = is_acc_run \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igb_graph_rec.more G' = ti_Lcnv ecnv G \<and> igb_graph G') \<le> SPEC (\<lambda>G'. igba.accept G' = accept \<and> g_V G' = V \<and> g_E G' = E \<and> g_V0 G' = V0 \<and> igba_rec.more G' = ecnv G \<and> igba G')
[PROOF STEP]
apply (rule SPEC_rule)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. igb_graph.is_acc_run x = is_acc_run \<and> g_V x = V \<and> g_E x = E \<and> g_V0 x = V0 \<and> igb_graph_rec.more x = ti_Lcnv ecnv G \<and> igb_graph x \<Longrightarrow> igba.accept x = accept \<and> g_V x = V \<and> g_E x = E \<and> g_V0 x = V0 \<and> igba_rec.more x = ecnv G \<and> igba x
[PROOF STEP]
apply (elim conjE, intro conjI)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> igba.accept x = accept
 2. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_V x = V
 3. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_E x = E
 4. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_V0 x = V0
 5. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> igba_rec.more x = ecnv G
 6. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> igba x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> igba.accept x = accept
 2. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_V x = V
 3. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_E x = E
 4. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_V0 x = V0
 5. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> igba_rec.more x = ecnv G
 6. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> igba x
[PROOF STEP]
fix G'
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> igba.accept x = accept
 2. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_V x = V
 3. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_E x = E
 4. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_V0 x = V0
 5. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> igba_rec.more x = ecnv G
 6. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> igba x
[PROOF STEP]
assume
    ARUN: "igb_graph.is_acc_run G' = is_acc_run"
    and MORE: "igb_graph_rec.more G' = ti_Lcnv ecnv G"
    and LOC: "igb_graph G'"
    and FIELDS: "g_V G' = V" "g_E G' = E" "g_V0 G' = V0"
[PROOF STATE]
proof (state)
this:
igb_graph.is_acc_run G' = is_acc_run
igb_graph_rec.more G' = ti_Lcnv ecnv G
igb_graph G'
g_V G' = V
g_E G' = E
g_V0 G' = V0

goal (6 subgoals):
 1. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> igba.accept x = accept
 2. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_V x = V
 3. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_E x = E
 4. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_V0 x = V0
 5. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> igba_rec.more x = ecnv G
 6. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> igba x
[PROOF STEP]
from LOC
[PROOF STATE]
proof (chain)
picking this:
igb_graph G'
[PROOF STEP]
interpret igb: igb_graph G'
[PROOF STATE]
proof (prove)
using this:
igb_graph G'

goal (1 subgoal):
 1. igb_graph G'
[PROOF STEP]
.
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> igba.accept x = accept
 2. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_V x = V
 3. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_E x = E
 4. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_V0 x = V0
 5. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> igba_rec.more x = ecnv G
 6. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> igba x
[PROOF STEP]
interpret igb: igba G'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igba G'
[PROOF STEP]
apply unfold_locales
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q l. igba_L G' q l \<Longrightarrow> q \<in> igb.V
[PROOF STEP]
using MORE FIELDS L_ss
[PROOF STATE]
proof (prove)
using this:
igb_graph_rec.more G' = ti_Lcnv ecnv G
igb.V = V
igb.E = E
igb.V0 = V0
L ?q ?l \<Longrightarrow> ?q \<in> V

goal (1 subgoal):
 1. \<And>q l. igba_L G' q l \<Longrightarrow> q \<in> igb.V
[PROOF STEP]
unfolding ti_Lcnv_def
[PROOF STATE]
proof (prove)
using this:
igb_graph_rec.more G' = \<lparr>igba_L = L, \<dots> = ecnv G\<rparr>
igb.V = V
igb.E = E
igb.V0 = V0
L ?q ?l \<Longrightarrow> ?q \<in> V

goal (1 subgoal):
 1. \<And>q l. igba_L G' q l \<Longrightarrow> q \<in> igb.V
[PROOF STEP]
apply (cases G')
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>q l g_V g_E g_V0 igbg_num_acc igbg_acc igba_La morea. \<lbrakk>igba_L G' q l; igb_graph_rec.more G' = \<lparr>igba_L = L, \<dots> = ecnv G\<rparr>; igb.V = V; igb.E = E; igb.V0 = V0; \<And>q l. L q l \<Longrightarrow> q \<in> V; G' = \<lparr>g_V = g_V, g_E = g_E, g_V0 = g_V0, igbg_num_acc = igbg_num_acc, igbg_acc = igbg_acc, igba_L = igba_La, \<dots> = morea\<rparr>\<rbrakk> \<Longrightarrow> q \<in> igb.V
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> igba.accept x = accept
 2. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_V x = V
 3. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_E x = E
 4. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_V0 x = V0
 5. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> igba_rec.more x = ecnv G
 6. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> igba x
[PROOF STEP]
show "igba.accept G' = accept" and "igba_rec.more G' = ecnv G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igb.accept = accept &&& igba_rec.more G' = ecnv G
[PROOF STEP]
using ARUN MORE
[PROOF STATE]
proof (prove)
using this:
igb.is_acc_run = is_acc_run
igb_graph_rec.more G' = ti_Lcnv ecnv G

goal (1 subgoal):
 1. igb.accept = accept &&& igba_rec.more G' = ecnv G
[PROOF STEP]
unfolding accept_def[abs_def] igb.accept_def[abs_def] ti_Lcnv_def
[PROOF STATE]
proof (prove)
using this:
igb.is_acc_run = is_acc_run
igb_graph_rec.more G' = \<lparr>igba_L = L, \<dots> = ecnv G\<rparr>

goal (1 subgoal):
 1. (\<lambda>w. \<exists>r. igb.is_acc_run r \<and> (\<forall>i. igb.L (r i) (w i))) = (\<lambda>w. \<exists>r. is_acc_run r \<and> (\<forall>i. L (r i) (w i))) &&& igba_rec.more G' = ecnv G
[PROOF STEP]
apply (cases G', (auto) []) +
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
igb.accept = accept
igba_rec.more G' = ecnv G

goal (4 subgoals):
 1. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_V x = V
 2. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_E x = E
 3. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_V0 x = V0
 4. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> igba x
[PROOF STEP]
show "igba G'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. igba G'
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
this:
igba G'

goal (3 subgoals):
 1. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_V x = V
 2. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_E x = E
 3. \<And>x. \<lbrakk>igb_graph.is_acc_run x = is_acc_run; g_V x = V; g_E x = E; g_V0 x = V0; igb_graph_rec.more x = ti_Lcnv ecnv G; igb_graph x\<rbrakk> \<Longrightarrow> g_V0 x = V0
[PROOF STEP]
qed


[STATEMENT]
lemma degen_more[simp]: "b_graph_rec.more (degeneralize_ext ecnv) = ecnv G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b_graph_rec.more (degeneralize_ext ecnv) = ecnv G
[PROOF STEP]
unfolding degeneralize_ext_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b_graph_rec.more (if num_acc = 0 then \<lparr>g_V = V \<times> {0}, g_E = {((q, 0), q', 0) |q q'. (q, q') \<in> E}, g_V0 = V0 \<times> {0}, bg_F = V \<times> {0}, \<dots> = ecnv G\<rparr> else \<lparr>g_V = V \<times> {0..<num_acc}, g_E = {((q, i), q', i') |i i' q q'. i < num_acc \<and> (q, q') \<in> E \<and> i' = (if i \<in> acc q then (i + 1) mod num_acc else i)}, g_V0 = V0 \<times> {0}, bg_F = {(q, 0) |q. 0 \<in> acc q}, \<dots> = ecnv G\<rparr>) = ecnv G
[PROOF STEP]
by auto