[STATEMENT]
lemma fill_gholes_ghole_poss:
  assumes "t =\<^sub>G\<^sub>f (C, ts)" and "i < length ts"
  shows "gsubt_at t (ghole_poss_list C ! i) = ts ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gsubt_at t (ghole_poss_list C ! i) = ts ! i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t =\<^sub>G\<^sub>f (C, ts)
i < length ts

goal (1 subgoal):
 1. gsubt_at t (ghole_poss_list C ! i) = ts ! i
[PROOF STEP]
proof (induct arbitrary: i rule: eq_gfill_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t i. i < length [t] \<Longrightarrow> gsubt_at t (ghole_poss_list GMHole ! i) = [t] ! i
 2. \<And>f ss Cs ts i. \<lbrakk>length Cs = length ss; sum_list (map num_gholes Cs) = length ts; \<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i) \<and> (\<forall>x<length (partition_gholes ts Cs ! i). gsubt_at (ss ! i) (ghole_poss_list (Cs ! i) ! x) = partition_gholes ts Cs ! i ! x); i < length ts\<rbrakk> \<Longrightarrow> gsubt_at (GFun f ss) (ghole_poss_list (GMFun f Cs) ! i) = ts ! i
[PROOF STEP]
case (GMFun f ss Cs ts)
[PROOF STATE]
proof (state)
this:
length Cs = length ss
sum_list (map num_gholes Cs) = length ts
\<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i) \<and> (\<forall>x<length (partition_gholes ts Cs ! i). gsubt_at (ss ! i) (ghole_poss_list (Cs ! i) ! x) = partition_gholes ts Cs ! i ! x)
i < length ts

goal (2 subgoals):
 1. \<And>t i. i < length [t] \<Longrightarrow> gsubt_at t (ghole_poss_list GMHole ! i) = [t] ! i
 2. \<And>f ss Cs ts i. \<lbrakk>length Cs = length ss; sum_list (map num_gholes Cs) = length ts; \<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i) \<and> (\<forall>x<length (partition_gholes ts Cs ! i). gsubt_at (ss ! i) (ghole_poss_list (Cs ! i) ! x) = partition_gholes ts Cs ! i ! x); i < length ts\<rbrakk> \<Longrightarrow> gsubt_at (GFun f ss) (ghole_poss_list (GMFun f Cs) ! i) = ts ! i
[PROOF STEP]
have *: "length (concat (poss_rec ghole_poss_list Cs)) = num_gholes (GMFun f Cs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (concat (poss_rec ghole_poss_list Cs)) = num_gholes (GMFun f Cs)
[PROOF STEP]
using GMFun(1, 2, 4)
[PROOF STATE]
proof (prove)
using this:
length Cs = length ss
sum_list (map num_gholes Cs) = length ts
i < length ts

goal (1 subgoal):
 1. length (concat (poss_rec ghole_poss_list Cs)) = num_gholes (GMFun f Cs)
[PROOF STEP]
unfolding length_ghole_poss_list_num_gholes[of "GMFun f Cs", symmetric, unfolded ghole_poss_list.simps]
[PROOF STATE]
proof (prove)
using this:
length Cs = length ss
sum_list (map num_gholes Cs) = length ts
i < length ts

goal (1 subgoal):
 1. num_gholes (GMFun f Cs) = num_gholes (GMFun f Cs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length (concat (poss_rec ghole_poss_list Cs)) = num_gholes (GMFun f Cs)

goal (2 subgoals):
 1. \<And>t i. i < length [t] \<Longrightarrow> gsubt_at t (ghole_poss_list GMHole ! i) = [t] ! i
 2. \<And>f ss Cs ts i. \<lbrakk>length Cs = length ss; sum_list (map num_gholes Cs) = length ts; \<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i) \<and> (\<forall>x<length (partition_gholes ts Cs ! i). gsubt_at (ss ! i) (ghole_poss_list (Cs ! i) ! x) = partition_gholes ts Cs ! i ! x); i < length ts\<rbrakk> \<Longrightarrow> gsubt_at (GFun f ss) (ghole_poss_list (GMFun f Cs) ! i) = ts ! i
[PROOF STEP]
from GMFun
[PROOF STATE]
proof (chain)
picking this:
length Cs = length ss
sum_list (map num_gholes Cs) = length ts
\<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i) \<and> (\<forall>x<length (partition_gholes ts Cs ! i). gsubt_at (ss ! i) (ghole_poss_list (Cs ! i) ! x) = partition_gholes ts Cs ! i ! x)
i < length ts
[PROOF STEP]
have b: "i < length (concat (partition_gholes ts Cs))"
[PROOF STATE]
proof (prove)
using this:
length Cs = length ss
sum_list (map num_gholes Cs) = length ts
\<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i) \<and> (\<forall>x<length (partition_gholes ts Cs ! i). gsubt_at (ss ! i) (ghole_poss_list (Cs ! i) ! x) = partition_gholes ts Cs ! i ! x)
i < length ts

goal (1 subgoal):
 1. i < length (concat (partition_gholes ts Cs))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < length (concat (partition_gholes ts Cs))

goal (2 subgoals):
 1. \<And>t i. i < length [t] \<Longrightarrow> gsubt_at t (ghole_poss_list GMHole ! i) = [t] ! i
 2. \<And>f ss Cs ts i. \<lbrakk>length Cs = length ss; sum_list (map num_gholes Cs) = length ts; \<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i) \<and> (\<forall>x<length (partition_gholes ts Cs ! i). gsubt_at (ss ! i) (ghole_poss_list (Cs ! i) ! x) = partition_gholes ts Cs ! i ! x); i < length ts\<rbrakk> \<Longrightarrow> gsubt_at (GFun f ss) (ghole_poss_list (GMFun f Cs) ! i) = ts ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length (concat (partition_gholes ts Cs))
[PROOF STEP]
have ts: "ts ! i = (\<lambda> (j, k). partition_gholes ts Cs ! j ! k) (concat_index_split (0, i) (partition_gholes ts Cs))"
[PROOF STATE]
proof (prove)
using this:
i < length (concat (partition_gholes ts Cs))

goal (1 subgoal):
 1. ts ! i = (case concat_index_split (0, i) (partition_gholes ts Cs) of (j, k) \<Rightarrow> partition_gholes ts Cs ! j ! k)
[PROOF STEP]
by (metis GMFun.hyps(2) concat_index_split_sound concat_partition_by)
[PROOF STATE]
proof (state)
this:
ts ! i = (case concat_index_split (0, i) (partition_gholes ts Cs) of (j, k) \<Rightarrow> partition_gholes ts Cs ! j ! k)

goal (2 subgoals):
 1. \<And>t i. i < length [t] \<Longrightarrow> gsubt_at t (ghole_poss_list GMHole ! i) = [t] ! i
 2. \<And>f ss Cs ts i. \<lbrakk>length Cs = length ss; sum_list (map num_gholes Cs) = length ts; \<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i) \<and> (\<forall>x<length (partition_gholes ts Cs ! i). gsubt_at (ss ! i) (ghole_poss_list (Cs ! i) ! x) = partition_gholes ts Cs ! i ! x); i < length ts\<rbrakk> \<Longrightarrow> gsubt_at (GFun f ss) (ghole_poss_list (GMFun f Cs) ! i) = ts ! i
[PROOF STEP]
obtain o_idx i_idx where csp: "concat_index_split (0, i) (partition_gholes ts Cs) = (o_idx, i_idx)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>o_idx i_idx. concat_index_split (0, i) (partition_gholes ts Cs) = (o_idx, i_idx) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using old.prod.exhaust
[PROOF STATE]
proof (prove)
using this:
(\<And>a b. ?y = (a, b) \<Longrightarrow> ?P) \<Longrightarrow> ?P

goal (1 subgoal):
 1. (\<And>o_idx i_idx. concat_index_split (0, i) (partition_gholes ts Cs) = (o_idx, i_idx) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
concat_index_split (0, i) (partition_gholes ts Cs) = (o_idx, i_idx)

goal (2 subgoals):
 1. \<And>t i. i < length [t] \<Longrightarrow> gsubt_at t (ghole_poss_list GMHole ! i) = [t] ! i
 2. \<And>f ss Cs ts i. \<lbrakk>length Cs = length ss; sum_list (map num_gholes Cs) = length ts; \<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i) \<and> (\<forall>x<length (partition_gholes ts Cs ! i). gsubt_at (ss ! i) (ghole_poss_list (Cs ! i) ! x) = partition_gholes ts Cs ! i ! x); i < length ts\<rbrakk> \<Longrightarrow> gsubt_at (GFun f ss) (ghole_poss_list (GMFun f Cs) ! i) = ts ! i
[PROOF STEP]
have idx: "o_idx < length Cs" "i_idx < length (partition_gholes ts Cs ! o_idx)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. o_idx < length Cs &&& i_idx < length (partition_gholes ts Cs ! o_idx)
[PROOF STEP]
using concat_index_split_sound_bounds[OF b csp]
[PROOF STATE]
proof (prove)
using this:
o_idx < length (partition_gholes ts Cs)
i_idx < length (partition_gholes ts Cs ! o_idx)

goal (1 subgoal):
 1. o_idx < length Cs &&& i_idx < length (partition_gholes ts Cs ! o_idx)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
o_idx < length Cs
i_idx < length (partition_gholes ts Cs ! o_idx)

goal (2 subgoals):
 1. \<And>t i. i < length [t] \<Longrightarrow> gsubt_at t (ghole_poss_list GMHole ! i) = [t] ! i
 2. \<And>f ss Cs ts i. \<lbrakk>length Cs = length ss; sum_list (map num_gholes Cs) = length ts; \<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i) \<and> (\<forall>x<length (partition_gholes ts Cs ! i). gsubt_at (ss ! i) (ghole_poss_list (Cs ! i) ! x) = partition_gholes ts Cs ! i ! x); i < length ts\<rbrakk> \<Longrightarrow> gsubt_at (GFun f ss) (ghole_poss_list (GMFun f Cs) ! i) = ts ! i
[PROOF STEP]
have "concat_index_split (0, i) (poss_rec ghole_poss_list Cs) = (o_idx, i_idx)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concat_index_split (0, i) (poss_rec ghole_poss_list Cs) = (o_idx, i_idx)
[PROOF STEP]
using GMFun(1, 2, 4) *
[PROOF STATE]
proof (prove)
using this:
length Cs = length ss
sum_list (map num_gholes Cs) = length ts
i < length ts
length (concat (poss_rec ghole_poss_list Cs)) = num_gholes (GMFun f Cs)

goal (1 subgoal):
 1. concat_index_split (0, i) (poss_rec ghole_poss_list Cs) = (o_idx, i_idx)
[PROOF STEP]
unfolding csp[symmetric]
[PROOF STATE]
proof (prove)
using this:
length Cs = length ss
sum_list (map num_gholes Cs) = length ts
i < length ts
length (concat (poss_rec ghole_poss_list Cs)) = num_gholes (GMFun f Cs)

goal (1 subgoal):
 1. concat_index_split (0, i) (poss_rec ghole_poss_list Cs) = concat_index_split (0, i) (partition_gholes ts Cs)
[PROOF STEP]
by (intro concat_index_split_unique, unfold *)
       (auto, simp add: length_ghole_poss_list_num_gholes length_partition_gholes_nth)
[PROOF STATE]
proof (state)
this:
concat_index_split (0, i) (poss_rec ghole_poss_list Cs) = (o_idx, i_idx)

goal (2 subgoals):
 1. \<And>t i. i < length [t] \<Longrightarrow> gsubt_at t (ghole_poss_list GMHole ! i) = [t] ! i
 2. \<And>f ss Cs ts i. \<lbrakk>length Cs = length ss; sum_list (map num_gholes Cs) = length ts; \<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i) \<and> (\<forall>x<length (partition_gholes ts Cs ! i). gsubt_at (ss ! i) (ghole_poss_list (Cs ! i) ! x) = partition_gholes ts Cs ! i ! x); i < length ts\<rbrakk> \<Longrightarrow> gsubt_at (GFun f ss) (ghole_poss_list (GMFun f Cs) ! i) = ts ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
concat_index_split (0, i) (poss_rec ghole_poss_list Cs) = (o_idx, i_idx)
[PROOF STEP]
have gp: "ghole_poss_list (GMFun f Cs) ! i = poss_rec ghole_poss_list Cs ! o_idx ! i_idx"
[PROOF STATE]
proof (prove)
using this:
concat_index_split (0, i) (poss_rec ghole_poss_list Cs) = (o_idx, i_idx)

goal (1 subgoal):
 1. ghole_poss_list (GMFun f Cs) ! i = poss_rec ghole_poss_list Cs ! o_idx ! i_idx
[PROOF STEP]
by (simp add: "*" GMFun.hyps(2) GMFun.prems concat_index_split_less_length_concat(4))
[PROOF STATE]
proof (state)
this:
ghole_poss_list (GMFun f Cs) ! i = poss_rec ghole_poss_list Cs ! o_idx ! i_idx

goal (2 subgoals):
 1. \<And>t i. i < length [t] \<Longrightarrow> gsubt_at t (ghole_poss_list GMHole ! i) = [t] ! i
 2. \<And>f ss Cs ts i. \<lbrakk>length Cs = length ss; sum_list (map num_gholes Cs) = length ts; \<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i) \<and> (\<forall>x<length (partition_gholes ts Cs ! i). gsubt_at (ss ! i) (ghole_poss_list (Cs ! i) ! x) = partition_gholes ts Cs ! i ! x); i < length ts\<rbrakk> \<Longrightarrow> gsubt_at (GFun f ss) (ghole_poss_list (GMFun f Cs) ! i) = ts ! i
[PROOF STEP]
from idx GMFun
[PROOF STATE]
proof (chain)
picking this:
o_idx < length Cs
i_idx < length (partition_gholes ts Cs ! o_idx)
length Cs = length ss
sum_list (map num_gholes Cs) = length ts
\<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i) \<and> (\<forall>x<length (partition_gholes ts Cs ! i). gsubt_at (ss ! i) (ghole_poss_list (Cs ! i) ! x) = partition_gholes ts Cs ! i ! x)
i < length ts
[PROOF STEP]
have r: "o_idx < length (zip [0..<length ss] Cs)"
[PROOF STATE]
proof (prove)
using this:
o_idx < length Cs
i_idx < length (partition_gholes ts Cs ! o_idx)
length Cs = length ss
sum_list (map num_gholes Cs) = length ts
\<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i) \<and> (\<forall>x<length (partition_gholes ts Cs ! i). gsubt_at (ss ! i) (ghole_poss_list (Cs ! i) ! x) = partition_gholes ts Cs ! i ! x)
i < length ts

goal (1 subgoal):
 1. o_idx < length (zip [0..<length ss] Cs)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
o_idx < length (zip [0..<length ss] Cs)

goal (2 subgoals):
 1. \<And>t i. i < length [t] \<Longrightarrow> gsubt_at t (ghole_poss_list GMHole ! i) = [t] ! i
 2. \<And>f ss Cs ts i. \<lbrakk>length Cs = length ss; sum_list (map num_gholes Cs) = length ts; \<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i) \<and> (\<forall>x<length (partition_gholes ts Cs ! i). gsubt_at (ss ! i) (ghole_poss_list (Cs ! i) ! x) = partition_gholes ts Cs ! i ! x); i < length ts\<rbrakk> \<Longrightarrow> gsubt_at (GFun f ss) (ghole_poss_list (GMFun f Cs) ! i) = ts ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
o_idx < length (zip [0..<length ss] Cs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
o_idx < length (zip [0..<length ss] Cs)

goal (1 subgoal):
 1. gsubt_at (GFun f ss) (ghole_poss_list (GMFun f Cs) ! i) = ts ! i
[PROOF STEP]
using GMFun idx
[PROOF STATE]
proof (prove)
using this:
o_idx < length (zip [0..<length ss] Cs)
length Cs = length ss
sum_list (map num_gholes Cs) = length ts
\<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i) \<and> (\<forall>x<length (partition_gholes ts Cs ! i). gsubt_at (ss ! i) (ghole_poss_list (Cs ! i) ! x) = partition_gholes ts Cs ! i ! x)
i < length ts
o_idx < length Cs
i_idx < length (partition_gholes ts Cs ! o_idx)

goal (1 subgoal):
 1. gsubt_at (GFun f ss) (ghole_poss_list (GMFun f Cs) ! i) = ts ! i
[PROOF STEP]
unfolding ts csp gp
[PROOF STATE]
proof (prove)
using this:
o_idx < length (zip [0..<length ss] Cs)
length Cs = length ss
sum_list (map num_gholes Cs) = length ts
\<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i) \<and> (\<forall>x<length (partition_gholes ts Cs ! i). gsubt_at (ss ! i) (ghole_poss_list (Cs ! i) ! x) = partition_gholes ts Cs ! i ! x)
i < length ts
o_idx < length Cs
i_idx < length (partition_gholes ts Cs ! o_idx)

goal (1 subgoal):
 1. gsubt_at (GFun f ss) (poss_rec ghole_poss_list Cs ! o_idx ! i_idx) = (case (o_idx, i_idx) of (j, x) \<Rightarrow> partition_gholes ts Cs ! j ! x)
[PROOF STEP]
by (auto simp: nth_map[OF r] length_ghole_poss_list_num_gholes length_partition_gholes_nth split: prod.splits)
[PROOF STATE]
proof (state)
this:
gsubt_at (GFun f ss) (ghole_poss_list (GMFun f Cs) ! i) = ts ! i

goal (1 subgoal):
 1. \<And>t i. i < length [t] \<Longrightarrow> gsubt_at t (ghole_poss_list GMHole ! i) = [t] ! i
[PROOF STEP]
qed auto


[STATEMENT]
lemma length_unfill_gholes [simp]:
  assumes "C \<le> gmctxt_of_gterm t"
  shows "length (unfill_gholes C t) = num_gholes C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (unfill_gholes C t) = num_gholes C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
C \<le> gmctxt_of_gterm t

goal (1 subgoal):
 1. length (unfill_gholes C t) = num_gholes C
[PROOF STEP]
proof (induct C t rule: unfill_gholes.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. GMHole \<le> gmctxt_of_gterm t \<Longrightarrow> length (unfill_gholes GMHole t) = num_gholes GMHole
 2. \<And>g Cs f ts. \<lbrakk>\<And>x. \<lbrakk>f = g \<and> length ts = length Cs; x \<in> set [0..<length ts]; Cs ! x \<le> gmctxt_of_gterm (ts ! x)\<rbrakk> \<Longrightarrow> length (unfill_gholes (Cs ! x) (ts ! x)) = num_gholes (Cs ! x); GMFun g Cs \<le> gmctxt_of_gterm (GFun f ts)\<rbrakk> \<Longrightarrow> length (unfill_gholes (GMFun g Cs) (GFun f ts)) = num_gholes (GMFun g Cs)
[PROOF STEP]
case (2 f Cs g ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>g = f \<and> length ts = length Cs; ?x \<in> set [0..<length ts]; Cs ! ?x \<le> gmctxt_of_gterm (ts ! ?x)\<rbrakk> \<Longrightarrow> length (unfill_gholes (Cs ! ?x) (ts ! ?x)) = num_gholes (Cs ! ?x)
GMFun f Cs \<le> gmctxt_of_gterm (GFun g ts)

goal (2 subgoals):
 1. \<And>t. GMHole \<le> gmctxt_of_gterm t \<Longrightarrow> length (unfill_gholes GMHole t) = num_gholes GMHole
 2. \<And>g Cs f ts. \<lbrakk>\<And>x. \<lbrakk>f = g \<and> length ts = length Cs; x \<in> set [0..<length ts]; Cs ! x \<le> gmctxt_of_gterm (ts ! x)\<rbrakk> \<Longrightarrow> length (unfill_gholes (Cs ! x) (ts ! x)) = num_gholes (Cs ! x); GMFun g Cs \<le> gmctxt_of_gterm (GFun f ts)\<rbrakk> \<Longrightarrow> length (unfill_gholes (GMFun g Cs) (GFun f ts)) = num_gholes (GMFun g Cs)
[PROOF STEP]
with 2(1)[OF _ nth_mem] 2(2)
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>g = f \<and> length ts = length Cs; ?n1 < length [0..<length ts]; Cs ! ([0..<length ts] ! ?n1) \<le> gmctxt_of_gterm (ts ! ([0..<length ts] ! ?n1))\<rbrakk> \<Longrightarrow> length (unfill_gholes (Cs ! ([0..<length ts] ! ?n1)) (ts ! ([0..<length ts] ! ?n1))) = num_gholes (Cs ! ([0..<length ts] ! ?n1))
GMFun f Cs \<le> gmctxt_of_gterm (GFun g ts)
\<lbrakk>g = f \<and> length ts = length Cs; ?x \<in> set [0..<length ts]; Cs ! ?x \<le> gmctxt_of_gterm (ts ! ?x)\<rbrakk> \<Longrightarrow> length (unfill_gholes (Cs ! ?x) (ts ! ?x)) = num_gholes (Cs ! ?x)
GMFun f Cs \<le> gmctxt_of_gterm (GFun g ts)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>g = f \<and> length ts = length Cs; ?n1 < length [0..<length ts]; Cs ! ([0..<length ts] ! ?n1) \<le> gmctxt_of_gterm (ts ! ([0..<length ts] ! ?n1))\<rbrakk> \<Longrightarrow> length (unfill_gholes (Cs ! ([0..<length ts] ! ?n1)) (ts ! ([0..<length ts] ! ?n1))) = num_gholes (Cs ! ([0..<length ts] ! ?n1))
GMFun f Cs \<le> gmctxt_of_gterm (GFun g ts)
\<lbrakk>g = f \<and> length ts = length Cs; ?x \<in> set [0..<length ts]; Cs ! ?x \<le> gmctxt_of_gterm (ts ! ?x)\<rbrakk> \<Longrightarrow> length (unfill_gholes (Cs ! ?x) (ts ! ?x)) = num_gholes (Cs ! ?x)
GMFun f Cs \<le> gmctxt_of_gterm (GFun g ts)

goal (1 subgoal):
 1. length (unfill_gholes (GMFun f Cs) (GFun g ts)) = num_gholes (GMFun f Cs)
[PROOF STEP]
by (auto simp: less_eq_gmctxt_def length_concat
      intro!: cong[of sum_list, OF refl] nth_equalityI elim!: nth_equalityE)
[PROOF STATE]
proof (state)
this:
length (unfill_gholes (GMFun f Cs) (GFun g ts)) = num_gholes (GMFun f Cs)

goal (1 subgoal):
 1. \<And>t. GMHole \<le> gmctxt_of_gterm t \<Longrightarrow> length (unfill_gholes GMHole t) = num_gholes GMHole
[PROOF STEP]
qed auto


[STATEMENT]
lemma fill_gholes_arbitrary:
  assumes lCs: "length Cs = length ts"
    and lss: "length ss = length ts"
    and rec: "\<And> i. i < length ts \<Longrightarrow> num_gholes (Cs ! i) = length (ss ! i) \<and> f (Cs ! i) (ss ! i) = ts ! i"
  shows "map (\<lambda>i. f (Cs ! i) (partition_gholes (concat ss) Cs ! i)) [0 ..< length Cs] = ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. f (Cs ! i) (partition_gholes (concat ss) Cs ! i)) [0..<length Cs] = ts
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. map (\<lambda>i. f (Cs ! i) (partition_gholes (concat ss) Cs ! i)) [0..<length Cs] = ts
[PROOF STEP]
have "sum_list (map num_gholes Cs) = length (concat ss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map num_gholes Cs) = length (concat ss)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length Cs = length ts
length ss = length ts
?i < length ts \<Longrightarrow> num_gholes (Cs ! ?i) = length (ss ! ?i) \<and> f (Cs ! ?i) (ss ! ?i) = ts ! ?i

goal (1 subgoal):
 1. sum_list (map num_gholes Cs) = length (concat ss)
[PROOF STEP]
by (auto simp: length_concat map_nth_eq_conv intro: arg_cong[of _ _ "sum_list"])
[PROOF STATE]
proof (state)
this:
sum_list (map num_gholes Cs) = length (concat ss)

goal (1 subgoal):
 1. map (\<lambda>i. f (Cs ! i) (partition_gholes (concat ss) Cs ! i)) [0..<length Cs] = ts
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
sum_list (map num_gholes Cs) = length (concat ss)

goal (1 subgoal):
 1. map (\<lambda>i. f (Cs ! i) (partition_gholes (concat ss) Cs ! i)) [0..<length Cs] = ts
[PROOF STEP]
have "partition_gholes (concat ss) Cs = ss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_gholes (concat ss) Cs = ss
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length Cs = length ts
length ss = length ts
?i < length ts \<Longrightarrow> num_gholes (Cs ! ?i) = length (ss ! ?i) \<and> f (Cs ! ?i) (ss ! ?i) = ts ! ?i

goal (1 subgoal):
 1. partition_gholes (concat ss) Cs = ss
[PROOF STEP]
by (auto intro: partition_by_concat_id)
[PROOF STATE]
proof (state)
this:
partition_gholes (concat ss) Cs = ss

goal (1 subgoal):
 1. map (\<lambda>i. f (Cs ! i) (partition_gholes (concat ss) Cs ! i)) [0..<length Cs] = ts
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
sum_list (map num_gholes Cs) = length (concat ss)
partition_gholes (concat ss) Cs = ss
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
sum_list (map num_gholes Cs) = length (concat ss)
partition_gholes (concat ss) Cs = ss

goal (1 subgoal):
 1. map (\<lambda>i. f (Cs ! i) (partition_gholes (concat ss) Cs ! i)) [0..<length Cs] = ts
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sum_list (map num_gholes Cs) = length (concat ss)
partition_gholes (concat ss) Cs = ss
length Cs = length ts
length ss = length ts
?i < length ts \<Longrightarrow> num_gholes (Cs ! ?i) = length (ss ! ?i) \<and> f (Cs ! ?i) (ss ! ?i) = ts ! ?i

goal (1 subgoal):
 1. map (\<lambda>i. f (Cs ! i) (partition_gholes (concat ss) Cs ! i)) [0..<length Cs] = ts
[PROOF STEP]
by (auto intro: nth_equalityI)
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. f (Cs ! i) (partition_gholes (concat ss) Cs ! i)) [0..<length Cs] = ts

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fill_unfill_gholes:
  assumes "C \<le> gmctxt_of_gterm t"
  shows "fill_gholes C (unfill_gholes C t) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_gholes C (unfill_gholes C t) = t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
C \<le> gmctxt_of_gterm t

goal (1 subgoal):
 1. fill_gholes C (unfill_gholes C t) = t
[PROOF STEP]
proof (induct C t rule: unfill_gholes.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. GMHole \<le> gmctxt_of_gterm t \<Longrightarrow> fill_gholes GMHole (unfill_gholes GMHole t) = t
 2. \<And>g Cs f ts. \<lbrakk>\<And>x. \<lbrakk>f = g \<and> length ts = length Cs; x \<in> set [0..<length ts]; Cs ! x \<le> gmctxt_of_gterm (ts ! x)\<rbrakk> \<Longrightarrow> fill_gholes (Cs ! x) (unfill_gholes (Cs ! x) (ts ! x)) = ts ! x; GMFun g Cs \<le> gmctxt_of_gterm (GFun f ts)\<rbrakk> \<Longrightarrow> fill_gholes (GMFun g Cs) (unfill_gholes (GMFun g Cs) (GFun f ts)) = GFun f ts
[PROOF STEP]
case (2 f Cs g ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>g = f \<and> length ts = length Cs; ?x \<in> set [0..<length ts]; Cs ! ?x \<le> gmctxt_of_gterm (ts ! ?x)\<rbrakk> \<Longrightarrow> fill_gholes (Cs ! ?x) (unfill_gholes (Cs ! ?x) (ts ! ?x)) = ts ! ?x
GMFun f Cs \<le> gmctxt_of_gterm (GFun g ts)

goal (2 subgoals):
 1. \<And>t. GMHole \<le> gmctxt_of_gterm t \<Longrightarrow> fill_gholes GMHole (unfill_gholes GMHole t) = t
 2. \<And>g Cs f ts. \<lbrakk>\<And>x. \<lbrakk>f = g \<and> length ts = length Cs; x \<in> set [0..<length ts]; Cs ! x \<le> gmctxt_of_gterm (ts ! x)\<rbrakk> \<Longrightarrow> fill_gholes (Cs ! x) (unfill_gholes (Cs ! x) (ts ! x)) = ts ! x; GMFun g Cs \<le> gmctxt_of_gterm (GFun f ts)\<rbrakk> \<Longrightarrow> fill_gholes (GMFun g Cs) (unfill_gholes (GMFun g Cs) (GFun f ts)) = GFun f ts
[PROOF STEP]
with 2(1)[OF _ nth_mem] 2(2)
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>g = f \<and> length ts = length Cs; ?n1 < length [0..<length ts]; Cs ! ([0..<length ts] ! ?n1) \<le> gmctxt_of_gterm (ts ! ([0..<length ts] ! ?n1))\<rbrakk> \<Longrightarrow> fill_gholes (Cs ! ([0..<length ts] ! ?n1)) (unfill_gholes (Cs ! ([0..<length ts] ! ?n1)) (ts ! ([0..<length ts] ! ?n1))) = ts ! ([0..<length ts] ! ?n1)
GMFun f Cs \<le> gmctxt_of_gterm (GFun g ts)
\<lbrakk>g = f \<and> length ts = length Cs; ?x \<in> set [0..<length ts]; Cs ! ?x \<le> gmctxt_of_gterm (ts ! ?x)\<rbrakk> \<Longrightarrow> fill_gholes (Cs ! ?x) (unfill_gholes (Cs ! ?x) (ts ! ?x)) = ts ! ?x
GMFun f Cs \<le> gmctxt_of_gterm (GFun g ts)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>g = f \<and> length ts = length Cs; ?n1 < length [0..<length ts]; Cs ! ([0..<length ts] ! ?n1) \<le> gmctxt_of_gterm (ts ! ([0..<length ts] ! ?n1))\<rbrakk> \<Longrightarrow> fill_gholes (Cs ! ([0..<length ts] ! ?n1)) (unfill_gholes (Cs ! ([0..<length ts] ! ?n1)) (ts ! ([0..<length ts] ! ?n1))) = ts ! ([0..<length ts] ! ?n1)
GMFun f Cs \<le> gmctxt_of_gterm (GFun g ts)
\<lbrakk>g = f \<and> length ts = length Cs; ?x \<in> set [0..<length ts]; Cs ! ?x \<le> gmctxt_of_gterm (ts ! ?x)\<rbrakk> \<Longrightarrow> fill_gholes (Cs ! ?x) (unfill_gholes (Cs ! ?x) (ts ! ?x)) = ts ! ?x
GMFun f Cs \<le> gmctxt_of_gterm (GFun g ts)

goal (1 subgoal):
 1. fill_gholes (GMFun f Cs) (unfill_gholes (GMFun f Cs) (GFun g ts)) = GFun g ts
[PROOF STEP]
by (auto simp: less_eq_gmctxt_def unfill_gholes_conv intro!: fill_gholes_arbitrary elim!: nth_equalityE)
[PROOF STATE]
proof (state)
this:
fill_gholes (GMFun f Cs) (unfill_gholes (GMFun f Cs) (GFun g ts)) = GFun g ts

goal (1 subgoal):
 1. \<And>t. GMHole \<le> gmctxt_of_gterm t \<Longrightarrow> fill_gholes GMHole (unfill_gholes GMHole t) = t
[PROOF STEP]
qed (auto split: if_splits)


[STATEMENT]
lemma funas_gmctxt_of_mctxt [simp]:
  "ground_mctxt C \<Longrightarrow> funas_gmctxt (gmctxt_of_mctxt C) = funas_mctxt C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground_mctxt C \<Longrightarrow> funas_gmctxt (gmctxt_of_mctxt C) = funas_mctxt C
[PROOF STEP]
by (induct C) (auto simp: funas_gterm_gterm_of_term)


[STATEMENT]
lemma funas_mctxt_of_gmctxt_conv:
  "funas_mctxt (mctxt_of_gmctxt C) = funas_gmctxt C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_mctxt (mctxt_of_gmctxt C) = funas_gmctxt C
[PROOF STEP]
by (induct C) (auto simp flip: funas_gterm_gterm_of_term)


[STATEMENT]
lemma funas_gterm_ctxt_apply [simp]:
  assumes "num_gholes C = length ss"
  shows "funas_gterm (fill_gholes C ss) = funas_gmctxt C \<union> \<Union> (set (map funas_gterm ss))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_gterm (fill_gholes C ss) = funas_gmctxt C \<union> \<Union> (set (map funas_gterm ss))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
num_gholes C = length ss

goal (1 subgoal):
 1. funas_gterm (fill_gholes C ss) = funas_gmctxt C \<union> \<Union> (set (map funas_gterm ss))
[PROOF STEP]
proof (induct rule: fill_gholes_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. funas_gterm (fill_gholes GMHole [x]) = funas_gmctxt GMHole \<union> \<Union> (set (map funas_gterm [x]))
 2. \<And>f Cs xs. \<lbrakk>sum_list (map num_gholes Cs) = length xs; \<And>i. i < length Cs \<Longrightarrow> funas_gterm (fill_gholes (Cs ! i) (partition_gholes xs Cs ! i)) = funas_gmctxt (Cs ! i) \<union> \<Union> (set (map funas_gterm (partition_gholes xs Cs ! i)))\<rbrakk> \<Longrightarrow> funas_gterm (fill_gholes (GMFun f Cs) (concat (partition_gholes xs Cs))) = funas_gmctxt (GMFun f Cs) \<union> \<Union> (set (map funas_gterm (concat (partition_gholes xs Cs))))
[PROOF STEP]
case (GMFun f Cs ss)
[PROOF STATE]
proof (state)
this:
sum_list (map num_gholes Cs) = length ss
?i < length Cs \<Longrightarrow> funas_gterm (fill_gholes (Cs ! ?i) (partition_gholes ss Cs ! ?i)) = funas_gmctxt (Cs ! ?i) \<union> \<Union> (set (map funas_gterm (partition_gholes ss Cs ! ?i)))

goal (2 subgoals):
 1. \<And>x. funas_gterm (fill_gholes GMHole [x]) = funas_gmctxt GMHole \<union> \<Union> (set (map funas_gterm [x]))
 2. \<And>f Cs xs. \<lbrakk>sum_list (map num_gholes Cs) = length xs; \<And>i. i < length Cs \<Longrightarrow> funas_gterm (fill_gholes (Cs ! i) (partition_gholes xs Cs ! i)) = funas_gmctxt (Cs ! i) \<union> \<Union> (set (map funas_gterm (partition_gholes xs Cs ! i)))\<rbrakk> \<Longrightarrow> funas_gterm (fill_gholes (GMFun f Cs) (concat (partition_gholes xs Cs))) = funas_gmctxt (GMFun f Cs) \<union> \<Union> (set (map funas_gterm (concat (partition_gholes xs Cs))))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_gterm (fill_gholes (GMFun f Cs) (concat (partition_gholes ss Cs))) = funas_gmctxt (GMFun f Cs) \<union> \<Union> (set (map funas_gterm (concat (partition_gholes ss Cs))))
[PROOF STEP]
using GMFun partition_gholes_subseteq[OF GMFun(1)]
[PROOF STATE]
proof (prove)
using this:
sum_list (map num_gholes Cs) = length ss
?i < length Cs \<Longrightarrow> funas_gterm (fill_gholes (Cs ! ?i) (partition_gholes ss Cs ! ?i)) = funas_gmctxt (Cs ! ?i) \<union> \<Union> (set (map funas_gterm (partition_gholes ss Cs ! ?i)))
\<lbrakk>?i < length Cs; ?x \<in> set (partition_gholes ss Cs ! ?i)\<rbrakk> \<Longrightarrow> ?x \<in> set ss

goal (1 subgoal):
 1. funas_gterm (fill_gholes (GMFun f Cs) (concat (partition_gholes ss Cs))) = funas_gmctxt (GMFun f Cs) \<union> \<Union> (set (map funas_gterm (concat (partition_gholes ss Cs))))
[PROOF STEP]
by (auto simp add: Un_Union_image simp del: map_partition_by_nth)
[PROOF STATE]
proof (state)
this:
funas_gterm (fill_gholes (GMFun f Cs) (concat (partition_gholes ss Cs))) = funas_gmctxt (GMFun f Cs) \<union> \<Union> (set (map funas_gterm (concat (partition_gholes ss Cs))))

goal (1 subgoal):
 1. \<And>x. funas_gterm (fill_gholes GMHole [x]) = funas_gmctxt GMHole \<union> \<Union> (set (map funas_gterm [x]))
[PROOF STEP]
qed simp


[STATEMENT]
lemma funas_gmctxt_gmctxt_of_gterm [simp]:
  "funas_gmctxt (gmctxt_of_gterm s) = funas_gterm s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_gmctxt (gmctxt_of_gterm s) = funas_gterm s
[PROOF STEP]
by (induct s) auto


[STATEMENT]
lemma funas_gmctxt_replicate_GMHole [simp]:
  "funas_gmctxt (GMFun f (replicate n GMHole)) = {(f, n)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_gmctxt (GMFun f (replicate n GMHole)) = {(f, n)}
[PROOF STEP]
by auto


[STATEMENT]
lemma funas_gmctxt_gmctxt_of_gctxt [simp]:
  "funas_gmctxt (gmctxt_of_gctxt C) = funas_gctxt C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_gmctxt (gmctxt_of_gctxt C) = funas_gctxt C
[PROOF STEP]
by (induct C) auto


[STATEMENT]
lemma funas_gmctxt_fill_gholes_gmctxt [simp]:
  assumes "num_gholes C = length Ds"
  shows "funas_gmctxt (fill_gholes_gmctxt C Ds) = funas_gmctxt C \<union> \<Union>(set (map funas_gmctxt Ds))"
  (is "?f C Ds = ?g C Ds")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_gmctxt (fill_gholes_gmctxt C Ds) = funas_gmctxt C \<union> \<Union> (set (map funas_gmctxt Ds))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
num_gholes C = length Ds

goal (1 subgoal):
 1. funas_gmctxt (fill_gholes_gmctxt C Ds) = funas_gmctxt C \<union> \<Union> (set (map funas_gmctxt Ds))
[PROOF STEP]
proof (induct C arbitrary: Ds)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Ds. num_gholes GMHole = length Ds \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt GMHole Ds) = funas_gmctxt GMHole \<union> \<Union> (set (map funas_gmctxt Ds))
 2. \<And>x1 x2 Ds. \<lbrakk>\<And>x2a Ds. \<lbrakk>x2a \<in> set x2; num_gholes x2a = length Ds\<rbrakk> \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt x2a Ds) = funas_gmctxt x2a \<union> \<Union> (set (map funas_gmctxt Ds)); num_gholes (GMFun x1 x2) = length Ds\<rbrakk> \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt (GMFun x1 x2) Ds) = funas_gmctxt (GMFun x1 x2) \<union> \<Union> (set (map funas_gmctxt Ds))
[PROOF STEP]
case GMHole
[PROOF STATE]
proof (state)
this:
num_gholes GMHole = length Ds

goal (2 subgoals):
 1. \<And>Ds. num_gholes GMHole = length Ds \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt GMHole Ds) = funas_gmctxt GMHole \<union> \<Union> (set (map funas_gmctxt Ds))
 2. \<And>x1 x2 Ds. \<lbrakk>\<And>x2a Ds. \<lbrakk>x2a \<in> set x2; num_gholes x2a = length Ds\<rbrakk> \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt x2a Ds) = funas_gmctxt x2a \<union> \<Union> (set (map funas_gmctxt Ds)); num_gholes (GMFun x1 x2) = length Ds\<rbrakk> \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt (GMFun x1 x2) Ds) = funas_gmctxt (GMFun x1 x2) \<union> \<Union> (set (map funas_gmctxt Ds))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
num_gholes GMHole = length Ds
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
num_gholes GMHole = length Ds

goal (1 subgoal):
 1. funas_gmctxt (fill_gholes_gmctxt GMHole Ds) = funas_gmctxt GMHole \<union> \<Union> (set (map funas_gmctxt Ds))
[PROOF STEP]
by (cases Ds) simp_all
[PROOF STATE]
proof (state)
this:
funas_gmctxt (fill_gholes_gmctxt GMHole Ds) = funas_gmctxt GMHole \<union> \<Union> (set (map funas_gmctxt Ds))

goal (1 subgoal):
 1. \<And>x1 x2 Ds. \<lbrakk>\<And>x2a Ds. \<lbrakk>x2a \<in> set x2; num_gholes x2a = length Ds\<rbrakk> \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt x2a Ds) = funas_gmctxt x2a \<union> \<Union> (set (map funas_gmctxt Ds)); num_gholes (GMFun x1 x2) = length Ds\<rbrakk> \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt (GMFun x1 x2) Ds) = funas_gmctxt (GMFun x1 x2) \<union> \<Union> (set (map funas_gmctxt Ds))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 Ds. \<lbrakk>\<And>x2a Ds. \<lbrakk>x2a \<in> set x2; num_gholes x2a = length Ds\<rbrakk> \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt x2a Ds) = funas_gmctxt x2a \<union> \<Union> (set (map funas_gmctxt Ds)); num_gholes (GMFun x1 x2) = length Ds\<rbrakk> \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt (GMFun x1 x2) Ds) = funas_gmctxt (GMFun x1 x2) \<union> \<Union> (set (map funas_gmctxt Ds))
[PROOF STEP]
case (GMFun f Cs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set Cs; num_gholes ?x2a = length ?Ds\<rbrakk> \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt ?x2a ?Ds) = funas_gmctxt ?x2a \<union> \<Union> (set (map funas_gmctxt ?Ds))
num_gholes (GMFun f Cs) = length Ds

goal (1 subgoal):
 1. \<And>x1 x2 Ds. \<lbrakk>\<And>x2a Ds. \<lbrakk>x2a \<in> set x2; num_gholes x2a = length Ds\<rbrakk> \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt x2a Ds) = funas_gmctxt x2a \<union> \<Union> (set (map funas_gmctxt Ds)); num_gholes (GMFun x1 x2) = length Ds\<rbrakk> \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt (GMFun x1 x2) Ds) = funas_gmctxt (GMFun x1 x2) \<union> \<Union> (set (map funas_gmctxt Ds))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x2a \<in> set Cs; num_gholes ?x2a = length ?Ds\<rbrakk> \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt ?x2a ?Ds) = funas_gmctxt ?x2a \<union> \<Union> (set (map funas_gmctxt ?Ds))
num_gholes (GMFun f Cs) = length Ds
[PROOF STEP]
have num_gholes: "sum_list (map num_gholes Cs) = length Ds"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set Cs; num_gholes ?x2a = length ?Ds\<rbrakk> \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt ?x2a ?Ds) = funas_gmctxt ?x2a \<union> \<Union> (set (map funas_gmctxt ?Ds))
num_gholes (GMFun f Cs) = length Ds

goal (1 subgoal):
 1. sum_list (map num_gholes Cs) = length Ds
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum_list (map num_gholes Cs) = length Ds

goal (1 subgoal):
 1. \<And>x1 x2 Ds. \<lbrakk>\<And>x2a Ds. \<lbrakk>x2a \<in> set x2; num_gholes x2a = length Ds\<rbrakk> \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt x2a Ds) = funas_gmctxt x2a \<union> \<Union> (set (map funas_gmctxt Ds)); num_gholes (GMFun x1 x2) = length Ds\<rbrakk> \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt (GMFun x1 x2) Ds) = funas_gmctxt (GMFun x1 x2) \<union> \<Union> (set (map funas_gmctxt Ds))
[PROOF STEP]
let ?ys = "partition_gholes Ds Cs"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 x2 Ds. \<lbrakk>\<And>x2a Ds. \<lbrakk>x2a \<in> set x2; num_gholes x2a = length Ds\<rbrakk> \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt x2a Ds) = funas_gmctxt x2a \<union> \<Union> (set (map funas_gmctxt Ds)); num_gholes (GMFun x1 x2) = length Ds\<rbrakk> \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt (GMFun x1 x2) Ds) = funas_gmctxt (GMFun x1 x2) \<union> \<Union> (set (map funas_gmctxt Ds))
[PROOF STEP]
have "\<And>i. i < length Cs \<Longrightarrow> ?f (Cs ! i) (?ys ! i) = ?g (Cs ! i) (?ys ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length Cs \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt (Cs ! i) (partition_gholes Ds Cs ! i)) = funas_gmctxt (Cs ! i) \<union> \<Union> (set (map funas_gmctxt (partition_gholes Ds Cs ! i)))
[PROOF STEP]
by (simp add: GMFun.hyps length_partition_by_nth num_gholes)
[PROOF STATE]
proof (state)
this:
?i < length Cs \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt (Cs ! ?i) (partition_gholes Ds Cs ! ?i)) = funas_gmctxt (Cs ! ?i) \<union> \<Union> (set (map funas_gmctxt (partition_gholes Ds Cs ! ?i)))

goal (1 subgoal):
 1. \<And>x1 x2 Ds. \<lbrakk>\<And>x2a Ds. \<lbrakk>x2a \<in> set x2; num_gholes x2a = length Ds\<rbrakk> \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt x2a Ds) = funas_gmctxt x2a \<union> \<Union> (set (map funas_gmctxt Ds)); num_gholes (GMFun x1 x2) = length Ds\<rbrakk> \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt (GMFun x1 x2) Ds) = funas_gmctxt (GMFun x1 x2) \<union> \<Union> (set (map funas_gmctxt Ds))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?i < length Cs \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt (Cs ! ?i) (partition_gholes Ds Cs ! ?i)) = funas_gmctxt (Cs ! ?i) \<union> \<Union> (set (map funas_gmctxt (partition_gholes Ds Cs ! ?i)))
[PROOF STEP]
have "(\<Union>i \<in> {0 ..< length Cs}. ?f (Cs ! i) (?ys ! i)) =
    (\<Union>i \<in> {0 ..< length Cs}. ?g (Cs ! i) (?ys ! i))"
[PROOF STATE]
proof (prove)
using this:
?i < length Cs \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt (Cs ! ?i) (partition_gholes Ds Cs ! ?i)) = funas_gmctxt (Cs ! ?i) \<union> \<Union> (set (map funas_gmctxt (partition_gholes Ds Cs ! ?i)))

goal (1 subgoal):
 1. (\<Union>i\<in>{0..<length Cs}. funas_gmctxt (fill_gholes_gmctxt (Cs ! i) (partition_gholes Ds Cs ! i))) = (\<Union>i\<in>{0..<length Cs}. funas_gmctxt (Cs ! i) \<union> \<Union> (set (map funas_gmctxt (partition_gholes Ds Cs ! i))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Union>i\<in>{0..<length Cs}. funas_gmctxt (fill_gholes_gmctxt (Cs ! i) (partition_gholes Ds Cs ! i))) = (\<Union>i\<in>{0..<length Cs}. funas_gmctxt (Cs ! i) \<union> \<Union> (set (map funas_gmctxt (partition_gholes Ds Cs ! i))))

goal (1 subgoal):
 1. \<And>x1 x2 Ds. \<lbrakk>\<And>x2a Ds. \<lbrakk>x2a \<in> set x2; num_gholes x2a = length Ds\<rbrakk> \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt x2a Ds) = funas_gmctxt x2a \<union> \<Union> (set (map funas_gmctxt Ds)); num_gholes (GMFun x1 x2) = length Ds\<rbrakk> \<Longrightarrow> funas_gmctxt (fill_gholes_gmctxt (GMFun x1 x2) Ds) = funas_gmctxt (GMFun x1 x2) \<union> \<Union> (set (map funas_gmctxt Ds))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Union>i\<in>{0..<length Cs}. funas_gmctxt (fill_gholes_gmctxt (Cs ! i) (partition_gholes Ds Cs ! i))) = (\<Union>i\<in>{0..<length Cs}. funas_gmctxt (Cs ! i) \<union> \<Union> (set (map funas_gmctxt (partition_gholes Ds Cs ! i))))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Union>i\<in>{0..<length Cs}. funas_gmctxt (fill_gholes_gmctxt (Cs ! i) (partition_gholes Ds Cs ! i))) = (\<Union>i\<in>{0..<length Cs}. funas_gmctxt (Cs ! i) \<union> \<Union> (set (map funas_gmctxt (partition_gholes Ds Cs ! i))))

goal (1 subgoal):
 1. funas_gmctxt (fill_gholes_gmctxt (GMFun f Cs) Ds) = funas_gmctxt (GMFun f Cs) \<union> \<Union> (set (map funas_gmctxt Ds))
[PROOF STEP]
using num_gholes
[PROOF STATE]
proof (prove)
using this:
(\<Union>i\<in>{0..<length Cs}. funas_gmctxt (fill_gholes_gmctxt (Cs ! i) (partition_gholes Ds Cs ! i))) = (\<Union>i\<in>{0..<length Cs}. funas_gmctxt (Cs ! i) \<union> \<Union> (set (map funas_gmctxt (partition_gholes Ds Cs ! i))))
sum_list (map num_gholes Cs) = length Ds

goal (1 subgoal):
 1. funas_gmctxt (fill_gholes_gmctxt (GMFun f Cs) Ds) = funas_gmctxt (GMFun f Cs) \<union> \<Union> (set (map funas_gmctxt Ds))
[PROOF STEP]
unfolding partition_holes_fill_holes_mctxt_conv
[PROOF STATE]
proof (prove)
using this:
(\<Union>i\<in>{0..<length Cs}. funas_gmctxt (fill_gholes_gmctxt (Cs ! i) (partition_gholes Ds Cs ! i))) = (\<Union>i\<in>{0..<length Cs}. funas_gmctxt (Cs ! i) \<union> \<Union> (set (map funas_gmctxt (partition_gholes Ds Cs ! i))))
sum_list (map num_gholes Cs) = length Ds

goal (1 subgoal):
 1. funas_gmctxt (fill_gholes_gmctxt (GMFun f Cs) Ds) = funas_gmctxt (GMFun f Cs) \<union> \<Union> (set (map funas_gmctxt Ds))
[PROOF STEP]
by (simp add: UN_Un_distrib UN_upt_len_conv [of _ _ "\<lambda>x. \<Union>(set x)"] UN_set_partition_by_map)
[PROOF STATE]
proof (state)
this:
funas_gmctxt (fill_gholes_gmctxt (GMFun f Cs) Ds) = funas_gmctxt (GMFun f Cs) \<union> \<Union> (set (map funas_gmctxt Ds))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma funas_supremum:
  "C \<le> D \<Longrightarrow> funas_gmctxt D = funas_gmctxt C \<union> \<Union> (set (map funas_gmctxt (sup_gmctxt_args C D)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<le> D \<Longrightarrow> funas_gmctxt D = funas_gmctxt C \<union> \<Union> (set (map funas_gmctxt (sup_gmctxt_args C D)))
[PROOF STEP]
using fill_gholes_gmctxt_sup_mctxt_args[of C]
[PROOF STATE]
proof (prove)
using this:
num_gholes C = length ?Ds \<Longrightarrow> sup_gmctxt_args C (fill_gholes_gmctxt C ?Ds) = ?Ds

goal (1 subgoal):
 1. C \<le> D \<Longrightarrow> funas_gmctxt D = funas_gmctxt C \<union> \<Union> (set (map funas_gmctxt (sup_gmctxt_args C D)))
[PROOF STEP]
by (auto simp: fill_gholes_gmctxt_sup_mctxt_args[of C] elim!: less_eq_to_sup_mctxt_args[of C D])


[STATEMENT]
lemma funas_gctxt_gctxt_of_gmctxt [simp]:
  "num_gholes D = Suc 0 \<Longrightarrow> funas_gctxt (gctxt_of_gmctxt D) = funas_gmctxt D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes D = Suc 0 \<Longrightarrow> funas_gctxt (gctxt_of_gmctxt D) = funas_gmctxt D
[PROOF STEP]
by (metis One_nat_def funas_gmctxt_gmctxt_of_gctxt gmctxt_of_gctxt_gctxt_of_gmctxt)


[STATEMENT]
lemma less_sup_gmctxt_args_funas_gmctxt:
  "C \<le> D \<Longrightarrow> funas_gmctxt C \<subseteq> \<F> \<Longrightarrow> \<forall> Ds \<in> set (sup_gmctxt_args C D). funas_gmctxt Ds \<subseteq> \<F> \<Longrightarrow> funas_gmctxt D \<subseteq> \<F>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C \<le> D; funas_gmctxt C \<subseteq> \<F>; \<forall>Ds\<in>set (sup_gmctxt_args C D). funas_gmctxt Ds \<subseteq> \<F>\<rbrakk> \<Longrightarrow> funas_gmctxt D \<subseteq> \<F>
[PROOF STEP]
using funas_supremum[of C D]
[PROOF STATE]
proof (prove)
using this:
C \<le> D \<Longrightarrow> funas_gmctxt D = funas_gmctxt C \<union> \<Union> (set (map funas_gmctxt (sup_gmctxt_args C D)))

goal (1 subgoal):
 1. \<lbrakk>C \<le> D; funas_gmctxt C \<subseteq> \<F>; \<forall>Ds\<in>set (sup_gmctxt_args C D). funas_gmctxt Ds \<subseteq> \<F>\<rbrakk> \<Longrightarrow> funas_gmctxt D \<subseteq> \<F>
[PROOF STEP]
by auto


[STATEMENT]
lemma funas_gmctxt_poss_gmctxt_subgm_at_funas:
  assumes "funas_gmctxt C \<subseteq> \<F>"  "p \<in> poss_gmctxt C"
  shows "funas_gmctxt (subgm_at C p) \<subseteq> \<F>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_gmctxt (subgm_at C p) \<subseteq> \<F>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
funas_gmctxt C \<subseteq> \<F>
p \<in> poss_gmctxt C

goal (1 subgoal):
 1. funas_gmctxt (subgm_at C p) \<subseteq> \<F>
[PROOF STEP]
proof (induct C arbitrary: p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p. \<lbrakk>funas_gmctxt GMHole \<subseteq> \<F>; p \<in> poss_gmctxt GMHole\<rbrakk> \<Longrightarrow> funas_gmctxt (subgm_at GMHole p) \<subseteq> \<F>
 2. \<And>x1 x2 p. \<lbrakk>\<And>x2a p. \<lbrakk>x2a \<in> set x2; funas_gmctxt x2a \<subseteq> \<F>; p \<in> poss_gmctxt x2a\<rbrakk> \<Longrightarrow> funas_gmctxt (subgm_at x2a p) \<subseteq> \<F>; funas_gmctxt (GMFun x1 x2) \<subseteq> \<F>; p \<in> poss_gmctxt (GMFun x1 x2)\<rbrakk> \<Longrightarrow> funas_gmctxt (subgm_at (GMFun x1 x2) p) \<subseteq> \<F>
[PROOF STEP]
case (GMFun f Cs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set Cs; funas_gmctxt ?x2a \<subseteq> \<F>; ?p \<in> poss_gmctxt ?x2a\<rbrakk> \<Longrightarrow> funas_gmctxt (subgm_at ?x2a ?p) \<subseteq> \<F>
funas_gmctxt (GMFun f Cs) \<subseteq> \<F>
p \<in> poss_gmctxt (GMFun f Cs)

goal (2 subgoals):
 1. \<And>p. \<lbrakk>funas_gmctxt GMHole \<subseteq> \<F>; p \<in> poss_gmctxt GMHole\<rbrakk> \<Longrightarrow> funas_gmctxt (subgm_at GMHole p) \<subseteq> \<F>
 2. \<And>x1 x2 p. \<lbrakk>\<And>x2a p. \<lbrakk>x2a \<in> set x2; funas_gmctxt x2a \<subseteq> \<F>; p \<in> poss_gmctxt x2a\<rbrakk> \<Longrightarrow> funas_gmctxt (subgm_at x2a p) \<subseteq> \<F>; funas_gmctxt (GMFun x1 x2) \<subseteq> \<F>; p \<in> poss_gmctxt (GMFun x1 x2)\<rbrakk> \<Longrightarrow> funas_gmctxt (subgm_at (GMFun x1 x2) p) \<subseteq> \<F>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x2a \<in> set Cs; funas_gmctxt ?x2a \<subseteq> \<F>; ?p \<in> poss_gmctxt ?x2a\<rbrakk> \<Longrightarrow> funas_gmctxt (subgm_at ?x2a ?p) \<subseteq> \<F>
funas_gmctxt (GMFun f Cs) \<subseteq> \<F>
p \<in> poss_gmctxt (GMFun f Cs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set Cs; funas_gmctxt ?x2a \<subseteq> \<F>; ?p \<in> poss_gmctxt ?x2a\<rbrakk> \<Longrightarrow> funas_gmctxt (subgm_at ?x2a ?p) \<subseteq> \<F>
funas_gmctxt (GMFun f Cs) \<subseteq> \<F>
p \<in> poss_gmctxt (GMFun f Cs)

goal (1 subgoal):
 1. funas_gmctxt (subgm_at (GMFun f Cs) p) \<subseteq> \<F>
[PROOF STEP]
by (auto, blast) (metis SUP_le_iff nth_mem subsetD)
[PROOF STATE]
proof (state)
this:
funas_gmctxt (subgm_at (GMFun f Cs) p) \<subseteq> \<F>

goal (1 subgoal):
 1. \<And>p. \<lbrakk>funas_gmctxt GMHole \<subseteq> \<F>; p \<in> poss_gmctxt GMHole\<rbrakk> \<Longrightarrow> funas_gmctxt (subgm_at GMHole p) \<subseteq> \<F>
[PROOF STEP]
qed auto


[STATEMENT]
lemma inf_funas_gmctxt_subset1:
  "funas_gmctxt (C \<sqinter> D) \<subseteq> funas_gmctxt C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_gmctxt (C \<sqinter> D) \<subseteq> funas_gmctxt C
[PROOF STEP]
using funas_supremum[of C "C \<sqinter> D"]
[PROOF STATE]
proof (prove)
using this:
C \<le> C \<sqinter> D \<Longrightarrow> funas_gmctxt (C \<sqinter> D) = funas_gmctxt C \<union> \<Union> (set (map funas_gmctxt (sup_gmctxt_args C (C \<sqinter> D))))

goal (1 subgoal):
 1. funas_gmctxt (C \<sqinter> D) \<subseteq> funas_gmctxt C
[PROOF STEP]
by (metis funas_supremum inf_le1 le_sup_iff order_refl)


[STATEMENT]
lemma inf_funas_gmctxt_subset2:
  "funas_gmctxt (C \<sqinter> D) \<subseteq> funas_gmctxt D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_gmctxt (C \<sqinter> D) \<subseteq> funas_gmctxt D
[PROOF STEP]
using funas_supremum[of D "C \<sqinter> D"]
[PROOF STATE]
proof (prove)
using this:
D \<le> C \<sqinter> D \<Longrightarrow> funas_gmctxt (C \<sqinter> D) = funas_gmctxt D \<union> \<Union> (set (map funas_gmctxt (sup_gmctxt_args D (C \<sqinter> D))))

goal (1 subgoal):
 1. funas_gmctxt (C \<sqinter> D) \<subseteq> funas_gmctxt D
[PROOF STEP]
by (metis funas_supremum inf_le2 le_sup_iff order_refl)


[STATEMENT]
lemma cs_abs_rep[simp]: "cs_rep (cs_abs f) = f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_rep (cs_abs f) = f
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. cs_rep (cs_abs f) x = f x
[PROOF STEP]
show "cs_rep (cs_abs f) x = f x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_rep (cs_abs f) x = f x
[PROOF STEP]
unfolding cs_lr_def cs_st_def cs_rep_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (map_option fst \<circ> f, f -` Some ` snd -` {True}) of (g, P) \<Rightarrow> \<lambda>p. map_option (\<lambda>k. (k, p \<in> P)) (g p)) x = f x
[PROOF STEP]
by (cases "f x") (force+)
[PROOF STATE]
proof (state)
this:
cs_rep (cs_abs f) ?x = f ?x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cs_rep_lr[simp]: "cs_lr (cs_rep (g, P)) = g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_lr (cs_rep (g, P)) = g
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. cs_lr (cs_rep (g, P)) x = g x
[PROOF STEP]
show "cs_lr (cs_rep (g, P)) x = g x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_lr (cs_rep (g, P)) x = g x
[PROOF STEP]
unfolding cs_rep_def cs_lr_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (map_option fst \<circ>\<circ>\<circ> case_prod) (\<lambda>g P p. map_option (\<lambda>k. (k, p \<in> P)) (g p)) (g, P) x = g x
[PROOF STEP]
by (cases "g x") (auto)
[PROOF STATE]
proof (state)
this:
cs_lr (cs_rep (g, P)) ?x = g ?x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cs_rep_st[simp]: "cs_st (cs_rep (g, P)) = P \<inter> dom g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_st (cs_rep (g, P)) = P \<inter> dom g
[PROOF STEP]
unfolding cs_rep_def cs_st_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (g, P) of (g, P) \<Rightarrow> \<lambda>p. map_option (\<lambda>k. (k, p \<in> P)) (g p)) -` Some ` snd -` {True} = P \<inter> dom g
[PROOF STEP]
by force


[STATEMENT]
lemma cs_lr_dom[simp]: "dom (cs_lr f) = dom f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (cs_lr f) = dom f
[PROOF STEP]
unfolding cs_lr_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (map_option fst \<circ> f) = dom f
[PROOF STEP]
by simp


[STATEMENT]
lemma cs_lr_apply[simp]:
    assumes "p \<in> dom f"
    shows "the (cs_lr f p) = fst (the (f p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (cs_lr f p) = fst (the (f p))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p \<in> dom f

goal (1 subgoal):
 1. the (cs_lr f p) = fst (the (f p))
[PROOF STEP]
unfolding cs_lr_def
[PROOF STATE]
proof (prove)
using this:
p \<in> dom f

goal (1 subgoal):
 1. the ((map_option fst \<circ> f) p) = fst (the (f p))
[PROOF STEP]
by auto


[STATEMENT]
lemma cs_rep_dom[simp]: "dom (cs_rep (g, P)) = dom g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (cs_rep (g, P)) = dom g
[PROOF STEP]
unfolding cs_rep_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (case (g, P) of (g, P) \<Rightarrow> \<lambda>p. map_option (\<lambda>k. (k, p \<in> P)) (g p)) = dom g
[PROOF STEP]
by auto


[STATEMENT]
lemma cs_rep_apply[simp]:
    assumes "p \<in> dom f"
    shows "fst (the (cs_rep (f, P) p)) = the (f p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (the (cs_rep (f, P) p)) = the (f p)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p \<in> dom f

goal (1 subgoal):
 1. fst (the (cs_rep (f, P) p)) = the (f p)
[PROOF STEP]
unfolding cs_rep_def
[PROOF STATE]
proof (prove)
using this:
p \<in> dom f

goal (1 subgoal):
 1. fst (the ((case (f, P) of (g, P) \<Rightarrow> \<lambda>p. map_option (\<lambda>k. (k, p \<in> P)) (g p)) p)) = the (f p)
[PROOF STEP]
by auto


[STATEMENT]
lemma refresh_1_apply[simp]: "fst (the (refresh_1 f p)) = fst (the (f p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (the (refresh_1 f p)) = fst (the (f p))
[PROOF STEP]
unfolding refresh_1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (the ((if True \<in> snd ` ran f then f else map_option (apsnd \<top>) \<circ> f) p)) = fst (the (f p))
[PROOF STEP]
by (cases "f p") (auto)


[STATEMENT]
lemma refresh_1_cs_st[simp]: "cs_st (refresh_1 f) = (if cs_st f = {} then dom f else cs_st f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_st (refresh_1 f) = (if cs_st f = {} then dom f else cs_st f)
[PROOF STEP]
unfolding refresh_1_def cs_st_def ran_def image_def vimage_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. (if True \<in> {y. \<exists>x\<in>{b. \<exists>a. f a = Some b}. y = snd x} then f else map_option (apsnd \<top>) \<circ> f) x \<in> {y. \<exists>x\<in>{x. snd x \<in> {True}}. y = Some x}} = (if {x. f x \<in> {y. \<exists>x\<in>{x. snd x \<in> {True}}. y = Some x}} = {} then dom f else {x. f x \<in> {y. \<exists>x\<in>{x. snd x \<in> {True}}. y = Some x}})
[PROOF STEP]
by auto


[STATEMENT]
lemma complement_succ_1_abs:
    assumes "g \<in> complement_succ_1 A a f"
    shows "cs_abs g \<in> complement_succ A a (cs_abs f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_abs g \<in> complement_succ A a (cs_abs f)
[PROOF STEP]
unfolding complement_succ_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_abs g \<in> (case cs_abs f of (f, P) \<Rightarrow> {(g, st_succ A a g P) |g. g \<in> lr_succ A a f})
[PROOF STEP]
proof (simp, rule)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cs_st g = st_succ A a (cs_lr g) (cs_st f)
 2. cs_lr g \<in> lr_succ A a (cs_lr f)
[PROOF STEP]
have 1:
      "dom g = \<Union>((transition A a) ` (dom f))"
      "\<forall> p \<in> dom f. \<forall> q \<in> transition A a p. fst (the (g q)) \<le> fst (the (f p))"
      "\<forall> p \<in> dom g. accepting A p \<longrightarrow> even (fst (the (g p)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom g = \<Union> (transition A a ` dom f) &&& \<forall>p\<in>dom f. \<forall>q\<in>transition A a p. fst (the (g q)) \<le> fst (the (f p)) &&& \<forall>p\<in>dom g. accepting A p \<longrightarrow> even (fst (the (g p)))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
g \<in> complement_succ_1 A a f

goal (1 subgoal):
 1. dom g = \<Union> (transition A a ` dom f) &&& \<forall>p\<in>dom f. \<forall>q\<in>transition A a p. fst (the (g q)) \<le> fst (the (f p)) &&& \<forall>p\<in>dom g. accepting A p \<longrightarrow> even (fst (the (g p)))
[PROOF STEP]
unfolding complement_succ_1_def ranks_1_def
[PROOF STATE]
proof (prove)
using this:
g \<in> ((\<lambda>f. {g. dom g = \<Union> (transition A a ` dom f) \<and> (\<forall>p\<in>dom f. \<forall>q\<in>transition A a p. fst (the (g q)) \<le> fst (the (f p))) \<and> (\<forall>q\<in>dom g. accepting A q \<longrightarrow> even (fst (the (g q)))) \<and> cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}}) \<circ> refresh_1) f

goal (1 subgoal):
 1. dom g = \<Union> (transition A a ` dom f) &&& \<forall>p\<in>dom f. \<forall>q\<in>transition A a p. fst (the (g q)) \<le> fst (the (f p)) &&& \<forall>p\<in>dom g. accepting A p \<longrightarrow> even (fst (the (g p)))
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
dom g = \<Union> (transition A a ` dom f)
\<forall>p\<in>dom f. \<forall>q\<in>transition A a p. fst (the (g q)) \<le> fst (the (f p))
\<forall>p\<in>dom g. accepting A p \<longrightarrow> even (fst (the (g p)))

goal (2 subgoals):
 1. cs_st g = st_succ A a (cs_lr g) (cs_st f)
 2. cs_lr g \<in> lr_succ A a (cs_lr f)
[PROOF STEP]
show "cs_lr g \<in> lr_succ A a (cs_lr f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_lr g \<in> lr_succ A a (cs_lr f)
[PROOF STEP]
unfolding lr_succ_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_lr g \<in> {g. dom g = \<Union> (transition A a ` dom (cs_lr f)) \<and> (\<forall>p\<in>dom (cs_lr f). \<forall>q\<in>transition A a p. the (g q) \<le> the (cs_lr f p)) \<and> (\<forall>q\<in>dom g. accepting A q \<longrightarrow> even (the (g q)))}
[PROOF STEP]
proof (intro CollectI conjI ballI impI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. dom (cs_lr g) = \<Union> (transition A a ` dom (cs_lr f))
 2. \<And>p q. \<lbrakk>p \<in> dom (cs_lr f); q \<in> transition A a p\<rbrakk> \<Longrightarrow> the (cs_lr g q) \<le> the (cs_lr f p)
 3. \<And>q. \<lbrakk>q \<in> dom (cs_lr g); accepting A q\<rbrakk> \<Longrightarrow> even (the (cs_lr g q))
[PROOF STEP]
show "dom (cs_lr g) = \<Union> (transition A a ` dom (cs_lr f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (cs_lr g) = \<Union> (transition A a ` dom (cs_lr f))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
dom g = \<Union> (transition A a ` dom f)
\<forall>p\<in>dom f. \<forall>q\<in>transition A a p. fst (the (g q)) \<le> fst (the (f p))
\<forall>p\<in>dom g. accepting A p \<longrightarrow> even (fst (the (g p)))

goal (1 subgoal):
 1. dom (cs_lr g) = \<Union> (transition A a ` dom (cs_lr f))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dom (cs_lr g) = \<Union> (transition A a ` dom (cs_lr f))

goal (2 subgoals):
 1. \<And>p q. \<lbrakk>p \<in> dom (cs_lr f); q \<in> transition A a p\<rbrakk> \<Longrightarrow> the (cs_lr g q) \<le> the (cs_lr f p)
 2. \<And>q. \<lbrakk>q \<in> dom (cs_lr g); accepting A q\<rbrakk> \<Longrightarrow> even (the (cs_lr g q))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p q. \<lbrakk>p \<in> dom (cs_lr f); q \<in> transition A a p\<rbrakk> \<Longrightarrow> the (cs_lr g q) \<le> the (cs_lr f p)
 2. \<And>q. \<lbrakk>q \<in> dom (cs_lr g); accepting A q\<rbrakk> \<Longrightarrow> even (the (cs_lr g q))
[PROOF STEP]
fix p q
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p q. \<lbrakk>p \<in> dom (cs_lr f); q \<in> transition A a p\<rbrakk> \<Longrightarrow> the (cs_lr g q) \<le> the (cs_lr f p)
 2. \<And>q. \<lbrakk>q \<in> dom (cs_lr g); accepting A q\<rbrakk> \<Longrightarrow> even (the (cs_lr g q))
[PROOF STEP]
assume 2: "p \<in> dom (cs_lr f)" "q \<in> transition A a p"
[PROOF STATE]
proof (state)
this:
p \<in> dom (cs_lr f)
q \<in> transition A a p

goal (2 subgoals):
 1. \<And>p q. \<lbrakk>p \<in> dom (cs_lr f); q \<in> transition A a p\<rbrakk> \<Longrightarrow> the (cs_lr g q) \<le> the (cs_lr f p)
 2. \<And>q. \<lbrakk>q \<in> dom (cs_lr g); accepting A q\<rbrakk> \<Longrightarrow> even (the (cs_lr g q))
[PROOF STEP]
have 3: "q \<in> dom (cs_lr g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<in> dom (cs_lr g)
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
dom g = \<Union> (transition A a ` dom f)
\<forall>p\<in>dom f. \<forall>q\<in>transition A a p. fst (the (g q)) \<le> fst (the (f p))
\<forall>p\<in>dom g. accepting A p \<longrightarrow> even (fst (the (g p)))
p \<in> dom (cs_lr f)
q \<in> transition A a p

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

goal (2 subgoals):
 1. \<And>p q. \<lbrakk>p \<in> dom (cs_lr f); q \<in> transition A a p\<rbrakk> \<Longrightarrow> the (cs_lr g q) \<le> the (cs_lr f p)
 2. \<And>q. \<lbrakk>q \<in> dom (cs_lr g); accepting A q\<rbrakk> \<Longrightarrow> even (the (cs_lr g q))
[PROOF STEP]
show "the (cs_lr g q) \<le> the (cs_lr f p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (cs_lr g q) \<le> the (cs_lr f p)
[PROOF STEP]
using 1 2 3
[PROOF STATE]
proof (prove)
using this:
dom g = \<Union> (transition A a ` dom f)
\<forall>p\<in>dom f. \<forall>q\<in>transition A a p. fst (the (g q)) \<le> fst (the (f p))
\<forall>p\<in>dom g. accepting A p \<longrightarrow> even (fst (the (g p)))
p \<in> dom (cs_lr f)
q \<in> transition A a p
q \<in> dom (cs_lr g)

goal (1 subgoal):
 1. the (cs_lr g q) \<le> the (cs_lr f p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
the (cs_lr g q) \<le> the (cs_lr f p)

goal (1 subgoal):
 1. \<And>q. \<lbrakk>q \<in> dom (cs_lr g); accepting A q\<rbrakk> \<Longrightarrow> even (the (cs_lr g q))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>q \<in> dom (cs_lr g); accepting A q\<rbrakk> \<Longrightarrow> even (the (cs_lr g q))
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>q. \<lbrakk>q \<in> dom (cs_lr g); accepting A q\<rbrakk> \<Longrightarrow> even (the (cs_lr g q))
[PROOF STEP]
assume 2: "p \<in> dom (cs_lr g)" "accepting A p"
[PROOF STATE]
proof (state)
this:
p \<in> dom (cs_lr g)
accepting A p

goal (1 subgoal):
 1. \<And>q. \<lbrakk>q \<in> dom (cs_lr g); accepting A q\<rbrakk> \<Longrightarrow> even (the (cs_lr g q))
[PROOF STEP]
show "even (the (cs_lr g p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. even (the (cs_lr g p))
[PROOF STEP]
using 1 2
[PROOF STATE]
proof (prove)
using this:
dom g = \<Union> (transition A a ` dom f)
\<forall>p\<in>dom f. \<forall>q\<in>transition A a p. fst (the (g q)) \<le> fst (the (f p))
\<forall>p\<in>dom g. accepting A p \<longrightarrow> even (fst (the (g p)))
p \<in> dom (cs_lr g)
accepting A p

goal (1 subgoal):
 1. even (the (cs_lr g p))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
even (the (cs_lr g p))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cs_lr g \<in> lr_succ A a (cs_lr f)

goal (1 subgoal):
 1. cs_st g = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
have 2: "cs_st g = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 f)). even (fst (the (g q)))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_st g = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 f)). even (fst (the (g q)))}
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
g \<in> complement_succ_1 A a f

goal (1 subgoal):
 1. cs_st g = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 f)). even (fst (the (g q)))}
[PROOF STEP]
unfolding complement_succ_1_def ranks_1_def
[PROOF STATE]
proof (prove)
using this:
g \<in> ((\<lambda>f. {g. dom g = \<Union> (transition A a ` dom f) \<and> (\<forall>p\<in>dom f. \<forall>q\<in>transition A a p. fst (the (g q)) \<le> fst (the (f p))) \<and> (\<forall>q\<in>dom g. accepting A q \<longrightarrow> even (fst (the (g q)))) \<and> cs_st g = {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))}}) \<circ> refresh_1) f

goal (1 subgoal):
 1. cs_st g = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 f)). even (fst (the (g q)))}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cs_st g = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 f)). even (fst (the (g q)))}

goal (1 subgoal):
 1. cs_st g = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
show "cs_st g = st_succ A a (cs_lr g) (cs_st f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_st g = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
proof (cases "cs_st f = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cs_st f = {} \<Longrightarrow> cs_st g = st_succ A a (cs_lr g) (cs_st f)
 2. cs_st f \<noteq> {} \<Longrightarrow> cs_st g = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
cs_st f = {}

goal (2 subgoals):
 1. cs_st f = {} \<Longrightarrow> cs_st g = st_succ A a (cs_lr g) (cs_st f)
 2. cs_st f \<noteq> {} \<Longrightarrow> cs_st g = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
have 3: "the (cs_lr g q) = fst (the (g q))" if "q \<in> \<Union>((transition A a) ` (dom f))" for q
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (cs_lr g q) = fst (the (g q))
[PROOF STEP]
using that 1(1)
[PROOF STATE]
proof (prove)
using this:
q \<in> \<Union> (transition A a ` dom f)
dom g = \<Union> (transition A a ` dom f)

goal (1 subgoal):
 1. the (cs_lr g q) = fst (the (g q))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?q \<in> \<Union> (transition A a ` dom f) \<Longrightarrow> the (cs_lr g ?q) = fst (the (g ?q))

goal (2 subgoals):
 1. cs_st f = {} \<Longrightarrow> cs_st g = st_succ A a (cs_lr g) (cs_st f)
 2. cs_st f \<noteq> {} \<Longrightarrow> cs_st g = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_st g = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
using 2 3
[PROOF STATE]
proof (prove)
using this:
cs_st g = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 f)). even (fst (the (g q)))}
?q \<in> \<Union> (transition A a ` dom f) \<Longrightarrow> the (cs_lr g ?q) = fst (the (g ?q))

goal (1 subgoal):
 1. cs_st g = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
unfolding st_succ_def refresh_1_cs_st True cs_lr_dom 1(1)
[PROOF STATE]
proof (prove)
using this:
cs_st g = {q \<in> \<Union> (transition A a ` (if {} = {} then dom f else {})). even (fst (the (g q)))}
?q \<in> \<Union> (transition A a ` dom f) \<Longrightarrow> the (cs_lr g ?q) = fst (the (g ?q))

goal (1 subgoal):
 1. cs_st g = {q \<in> if {} = {} then \<Union> (transition A a ` dom f) else \<Union> (transition A a ` {}). even (the (cs_lr g q))}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
cs_st g = st_succ A a (cs_lr g) (cs_st f)

goal (1 subgoal):
 1. cs_st f \<noteq> {} \<Longrightarrow> cs_st g = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. cs_st f \<noteq> {} \<Longrightarrow> cs_st g = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
cs_st f \<noteq> {}

goal (1 subgoal):
 1. cs_st f \<noteq> {} \<Longrightarrow> cs_st g = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
have 3: "the (cs_lr g q) = fst (the (g q))" if "q \<in> \<Union>((transition A a) ` (cs_st f))" for q
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the (cs_lr g q) = fst (the (g q))
[PROOF STEP]
using that 1(1)
[PROOF STATE]
proof (prove)
using this:
q \<in> \<Union> (transition A a ` cs_st f)
dom g = \<Union> (transition A a ` dom f)

goal (1 subgoal):
 1. the (cs_lr g q) = fst (the (g q))
[PROOF STEP]
by
          (auto intro!: cs_lr_apply)
          (metis IntE UN_iff cs_abs_rep cs_lr_dom cs_rep_st domD prod.collapse)
[PROOF STATE]
proof (state)
this:
?q \<in> \<Union> (transition A a ` cs_st f) \<Longrightarrow> the (cs_lr g ?q) = fst (the (g ?q))

goal (1 subgoal):
 1. cs_st f \<noteq> {} \<Longrightarrow> cs_st g = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
have "cs_st g = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 f)). even (fst (the (g q)))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_st g = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 f)). even (fst (the (g q)))}
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
cs_st g = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 f)). even (fst (the (g q)))}

goal (1 subgoal):
 1. cs_st g = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 f)). even (fst (the (g q)))}
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
cs_st g = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 f)). even (fst (the (g q)))}

goal (1 subgoal):
 1. cs_st f \<noteq> {} \<Longrightarrow> cs_st g = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cs_st g = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 f)). even (fst (the (g q)))}

goal (1 subgoal):
 1. cs_st f \<noteq> {} \<Longrightarrow> cs_st g = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
have "cs_st (refresh_1 f) = cs_st f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_st (refresh_1 f) = cs_st f
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
cs_st f \<noteq> {}

goal (1 subgoal):
 1. cs_st (refresh_1 f) = cs_st f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cs_st (refresh_1 f) = cs_st f

goal (1 subgoal):
 1. cs_st f \<noteq> {} \<Longrightarrow> cs_st g = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cs_st (refresh_1 f) = cs_st f

goal (1 subgoal):
 1. cs_st f \<noteq> {} \<Longrightarrow> cs_st g = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
have "{q \<in> \<Union>((transition A a) ` (cs_st f)). even (fst (the (g q)))} =
        {q \<in> \<Union>((transition A a) ` (cs_st f)). even (the (cs_lr g q))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))} = {q \<in> \<Union> (transition A a ` cs_st f). even (the (cs_lr g q))}
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
?q \<in> \<Union> (transition A a ` cs_st f) \<Longrightarrow> the (cs_lr g ?q) = fst (the (g ?q))

goal (1 subgoal):
 1. {q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))} = {q \<in> \<Union> (transition A a ` cs_st f). even (the (cs_lr g q))}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
{q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))} = {q \<in> \<Union> (transition A a ` cs_st f). even (the (cs_lr g q))}

goal (1 subgoal):
 1. cs_st f \<noteq> {} \<Longrightarrow> cs_st g = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{q \<in> \<Union> (transition A a ` cs_st f). even (fst (the (g q)))} = {q \<in> \<Union> (transition A a ` cs_st f). even (the (cs_lr g q))}

goal (1 subgoal):
 1. cs_st f \<noteq> {} \<Longrightarrow> cs_st g = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
have "\<dots> = st_succ A a (cs_lr g) (cs_st f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {q \<in> \<Union> (transition A a ` cs_st f). even (the (cs_lr g q))} = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
unfolding st_succ_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {q \<in> \<Union> (transition A a ` cs_st f). even (the (cs_lr g q))} = {q \<in> if cs_st f = {} then dom (cs_lr g) else \<Union> (transition A a ` cs_st f). even (the (cs_lr g q))}
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
cs_st f \<noteq> {}

goal (1 subgoal):
 1. {q \<in> \<Union> (transition A a ` cs_st f). even (the (cs_lr g q))} = {q \<in> if cs_st f = {} then dom (cs_lr g) else \<Union> (transition A a ` cs_st f). even (the (cs_lr g q))}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
{q \<in> \<Union> (transition A a ` cs_st f). even (the (cs_lr g q))} = st_succ A a (cs_lr g) (cs_st f)

goal (1 subgoal):
 1. cs_st f \<noteq> {} \<Longrightarrow> cs_st g = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cs_st g = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cs_st g = st_succ A a (cs_lr g) (cs_st f)

goal (1 subgoal):
 1. cs_st g = st_succ A a (cs_lr g) (cs_st f)
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
cs_st g = st_succ A a (cs_lr g) (cs_st f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cs_st g = st_succ A a (cs_lr g) (cs_st f)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma complement_succ_1_rep:
    assumes "P \<subseteq> dom f" "(g, Q) \<in> complement_succ A a (f, P)"
    shows "cs_rep (g, Q) \<in> complement_succ_1 A a (cs_rep (f, P))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_rep (g, Q) \<in> complement_succ_1 A a (cs_rep (f, P))
[PROOF STEP]
unfolding complement_succ_1_def ranks_1_def comp_apply
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_rep (g, Q) \<in> {g. dom g = \<Union> (transition A a ` dom (refresh_1 (cs_rep (f, P)))) \<and> (\<forall>p\<in>dom (refresh_1 (cs_rep (f, P))). \<forall>q\<in>transition A a p. fst (the (g q)) \<le> fst (the (refresh_1 (cs_rep (f, P)) p))) \<and> (\<forall>q\<in>dom g. accepting A q \<longrightarrow> even (fst (the (g q)))) \<and> cs_st g = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (g q)))}}
[PROOF STEP]
proof (intro CollectI conjI ballI impI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. dom (cs_rep (g, Q)) = \<Union> (transition A a ` dom (refresh_1 (cs_rep (f, P))))
 2. \<And>p q. \<lbrakk>p \<in> dom (refresh_1 (cs_rep (f, P))); q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (cs_rep (g, Q) q)) \<le> fst (the (refresh_1 (cs_rep (f, P)) p))
 3. \<And>q. \<lbrakk>q \<in> dom (cs_rep (g, Q)); accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (cs_rep (g, Q) q)))
 4. cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
have 1:
      "dom g = \<Union>((transition A a) ` (dom f))"
      "\<forall> p \<in> dom f. \<forall> q \<in> transition A a p. the (g q) \<le> the (f p)"
      "\<forall> p \<in> dom g. accepting A p \<longrightarrow> even (the (g p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom g = \<Union> (transition A a ` dom f) &&& \<forall>p\<in>dom f. \<forall>q\<in>transition A a p. the (g q) \<le> the (f p) &&& \<forall>p\<in>dom g. accepting A p \<longrightarrow> even (the (g p))
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(g, Q) \<in> complement_succ A a (f, P)

goal (1 subgoal):
 1. dom g = \<Union> (transition A a ` dom f) &&& \<forall>p\<in>dom f. \<forall>q\<in>transition A a p. the (g q) \<le> the (f p) &&& \<forall>p\<in>dom g. accepting A p \<longrightarrow> even (the (g p))
[PROOF STEP]
unfolding complement_succ_def lr_succ_def
[PROOF STATE]
proof (prove)
using this:
(g, Q) \<in> (case (f, P) of (f, P) \<Rightarrow> {(g, st_succ A a g P) |g. g \<in> {g. dom g = \<Union> (transition A a ` dom f) \<and> (\<forall>p\<in>dom f. \<forall>q\<in>transition A a p. the (g q) \<le> the (f p)) \<and> (\<forall>q\<in>dom g. accepting A q \<longrightarrow> even (the (g q)))}})

goal (1 subgoal):
 1. dom g = \<Union> (transition A a ` dom f) &&& \<forall>p\<in>dom f. \<forall>q\<in>transition A a p. the (g q) \<le> the (f p) &&& \<forall>p\<in>dom g. accepting A p \<longrightarrow> even (the (g p))
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
dom g = \<Union> (transition A a ` dom f)
\<forall>p\<in>dom f. \<forall>q\<in>transition A a p. the (g q) \<le> the (f p)
\<forall>p\<in>dom g. accepting A p \<longrightarrow> even (the (g p))

goal (4 subgoals):
 1. dom (cs_rep (g, Q)) = \<Union> (transition A a ` dom (refresh_1 (cs_rep (f, P))))
 2. \<And>p q. \<lbrakk>p \<in> dom (refresh_1 (cs_rep (f, P))); q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (cs_rep (g, Q) q)) \<le> fst (the (refresh_1 (cs_rep (f, P)) p))
 3. \<And>q. \<lbrakk>q \<in> dom (cs_rep (g, Q)); accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (cs_rep (g, Q) q)))
 4. cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
have 2: "Q = {q \<in> if P = {} then dom g else \<Union>((transition A a) ` P). even (the (g q))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q = {q \<in> if P = {} then dom g else \<Union> (transition A a ` P). even (the (g q))}
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
(g, Q) \<in> complement_succ A a (f, P)

goal (1 subgoal):
 1. Q = {q \<in> if P = {} then dom g else \<Union> (transition A a ` P). even (the (g q))}
[PROOF STEP]
unfolding complement_succ_def st_succ_def
[PROOF STATE]
proof (prove)
using this:
(g, Q) \<in> (case (f, P) of (f, P) \<Rightarrow> {(g, {q \<in> if P = {} then dom g else \<Union> (transition A a ` P). even (the (g q))}) |g. g \<in> lr_succ A a f})

goal (1 subgoal):
 1. Q = {q \<in> if P = {} then dom g else \<Union> (transition A a ` P). even (the (g q))}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Q = {q \<in> if P = {} then dom g else \<Union> (transition A a ` P). even (the (g q))}

goal (4 subgoals):
 1. dom (cs_rep (g, Q)) = \<Union> (transition A a ` dom (refresh_1 (cs_rep (f, P))))
 2. \<And>p q. \<lbrakk>p \<in> dom (refresh_1 (cs_rep (f, P))); q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (cs_rep (g, Q) q)) \<le> fst (the (refresh_1 (cs_rep (f, P)) p))
 3. \<And>q. \<lbrakk>q \<in> dom (cs_rep (g, Q)); accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (cs_rep (g, Q) q)))
 4. cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
have 3: "Q \<subseteq> dom g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<subseteq> dom g
[PROOF STEP]
unfolding 2 1(1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {q \<in> if P = {} then \<Union> (transition A a ` dom f) else \<Union> (transition A a ` P). even (the (g q))} \<subseteq> \<Union> (transition A a ` dom f)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
P \<subseteq> dom f

goal (1 subgoal):
 1. {q \<in> if P = {} then \<Union> (transition A a ` dom f) else \<Union> (transition A a ` P). even (the (g q))} \<subseteq> \<Union> (transition A a ` dom f)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Q \<subseteq> dom g

goal (4 subgoals):
 1. dom (cs_rep (g, Q)) = \<Union> (transition A a ` dom (refresh_1 (cs_rep (f, P))))
 2. \<And>p q. \<lbrakk>p \<in> dom (refresh_1 (cs_rep (f, P))); q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (cs_rep (g, Q) q)) \<le> fst (the (refresh_1 (cs_rep (f, P)) p))
 3. \<And>q. \<lbrakk>q \<in> dom (cs_rep (g, Q)); accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (cs_rep (g, Q) q)))
 4. cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
show "dom (cs_rep (g, Q)) = \<Union> (transition A a ` dom (refresh_1 (cs_rep (f, P))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom (cs_rep (g, Q)) = \<Union> (transition A a ` dom (refresh_1 (cs_rep (f, P))))
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
dom g = \<Union> (transition A a ` dom f)
\<forall>p\<in>dom f. \<forall>q\<in>transition A a p. the (g q) \<le> the (f p)
\<forall>p\<in>dom g. accepting A p \<longrightarrow> even (the (g p))

goal (1 subgoal):
 1. dom (cs_rep (g, Q)) = \<Union> (transition A a ` dom (refresh_1 (cs_rep (f, P))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dom (cs_rep (g, Q)) = \<Union> (transition A a ` dom (refresh_1 (cs_rep (f, P))))

goal (3 subgoals):
 1. \<And>p q. \<lbrakk>p \<in> dom (refresh_1 (cs_rep (f, P))); q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (cs_rep (g, Q) q)) \<le> fst (the (refresh_1 (cs_rep (f, P)) p))
 2. \<And>q. \<lbrakk>q \<in> dom (cs_rep (g, Q)); accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (cs_rep (g, Q) q)))
 3. cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
show "\<And> p q. p \<in> dom (refresh_1 (cs_rep (f, P))) \<Longrightarrow> q \<in> transition A a p \<Longrightarrow>
      fst (the (cs_rep (g, Q) q)) \<le> fst (the (refresh_1 (cs_rep (f, P)) p))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p q. \<lbrakk>p \<in> dom (refresh_1 (cs_rep (f, P))); q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (cs_rep (g, Q) q)) \<le> fst (the (refresh_1 (cs_rep (f, P)) p))
[PROOF STEP]
using 1(1, 2)
[PROOF STATE]
proof (prove)
using this:
dom g = \<Union> (transition A a ` dom f)
\<forall>p\<in>dom f. \<forall>q\<in>transition A a p. the (g q) \<le> the (f p)

goal (1 subgoal):
 1. \<And>p q. \<lbrakk>p \<in> dom (refresh_1 (cs_rep (f, P))); q \<in> transition A a p\<rbrakk> \<Longrightarrow> fst (the (cs_rep (g, Q) q)) \<le> fst (the (refresh_1 (cs_rep (f, P)) p))
[PROOF STEP]
by (auto) (metis UN_I cs_rep_apply domI option.sel)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?p \<in> dom (refresh_1 (cs_rep (f, P))); ?q \<in> transition A a ?p\<rbrakk> \<Longrightarrow> fst (the (cs_rep (g, Q) ?q)) \<le> fst (the (refresh_1 (cs_rep (f, P)) ?p))

goal (2 subgoals):
 1. \<And>q. \<lbrakk>q \<in> dom (cs_rep (g, Q)); accepting A q\<rbrakk> \<Longrightarrow> even (fst (the (cs_rep (g, Q) q)))
 2. cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
show "\<And> p. p \<in> dom (cs_rep (g, Q)) \<Longrightarrow> accepting A p \<Longrightarrow> even (fst (the (cs_rep (g, Q) p)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrakk>p \<in> dom (cs_rep (g, Q)); accepting A p\<rbrakk> \<Longrightarrow> even (fst (the (cs_rep (g, Q) p)))
[PROOF STEP]
using 1(1, 3)
[PROOF STATE]
proof (prove)
using this:
dom g = \<Union> (transition A a ` dom f)
\<forall>p\<in>dom g. accepting A p \<longrightarrow> even (the (g p))

goal (1 subgoal):
 1. \<And>p. \<lbrakk>p \<in> dom (cs_rep (g, Q)); accepting A p\<rbrakk> \<Longrightarrow> even (fst (the (cs_rep (g, Q) p)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?p \<in> dom (cs_rep (g, Q)); accepting A ?p\<rbrakk> \<Longrightarrow> even (fst (the (cs_rep (g, Q) ?p)))

goal (1 subgoal):
 1. cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
show "cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))).
      even (fst (the (cs_rep (g, Q) q)))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
proof (cases "P = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. P = {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
 2. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
P = {}

goal (2 subgoals):
 1. P = {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
 2. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
have "cs_st (cs_rep (g, Q)) = Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_st (cs_rep (g, Q)) = Q
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
Q \<subseteq> dom g

goal (1 subgoal):
 1. cs_st (cs_rep (g, Q)) = Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs_st (cs_rep (g, Q)) = Q

goal (2 subgoals):
 1. P = {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
 2. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cs_st (cs_rep (g, Q)) = Q

goal (2 subgoals):
 1. P = {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
 2. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
have "\<dots> = {q \<in> dom g. even (the (g q))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q = {q \<in> dom g. even (the (g q))}
[PROOF STEP]
unfolding 2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {q \<in> if P = {} then dom g else \<Union> (transition A a ` P). even (the (g q))} = {q \<in> dom g. even (the (g q))}
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
P = {}

goal (1 subgoal):
 1. {q \<in> if P = {} then dom g else \<Union> (transition A a ` P). even (the (g q))} = {q \<in> dom g. even (the (g q))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Q = {q \<in> dom g. even (the (g q))}

goal (2 subgoals):
 1. P = {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
 2. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Q = {q \<in> dom g. even (the (g q))}

goal (2 subgoals):
 1. P = {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
 2. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
have "\<dots> = {q \<in> dom g. even (fst (the (cs_rep (g, Q) q)))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {q \<in> dom g. even (the (g q))} = {q \<in> dom g. even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
using cs_rep_apply
[PROOF STATE]
proof (prove)
using this:
?p \<in> dom ?f \<Longrightarrow> fst (the (cs_rep (?f, ?P) ?p)) = the (?f ?p)

goal (1 subgoal):
 1. {q \<in> dom g. even (the (g q))} = {q \<in> dom g. even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
{q \<in> dom g. even (the (g q))} = {q \<in> dom g. even (fst (the (cs_rep (g, Q) q)))}

goal (2 subgoals):
 1. P = {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
 2. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{q \<in> dom g. even (the (g q))} = {q \<in> dom g. even (fst (the (cs_rep (g, Q) q)))}

goal (2 subgoals):
 1. P = {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
 2. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
have "dom g = \<Union>((transition A a) ` (dom f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom g = \<Union> (transition A a ` dom f)
[PROOF STEP]
using 1(1)
[PROOF STATE]
proof (prove)
using this:
dom g = \<Union> (transition A a ` dom f)

goal (1 subgoal):
 1. dom g = \<Union> (transition A a ` dom f)
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
dom g = \<Union> (transition A a ` dom f)

goal (2 subgoals):
 1. P = {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
 2. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
dom g = \<Union> (transition A a ` dom f)

goal (2 subgoals):
 1. P = {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
 2. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
have "dom f = cs_st (refresh_1 (cs_rep (f, P)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dom f = cs_st (refresh_1 (cs_rep (f, P)))
[PROOF STEP]
using True
[PROOF STATE]
proof (prove)
using this:
P = {}

goal (1 subgoal):
 1. dom f = cs_st (refresh_1 (cs_rep (f, P)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
dom f = cs_st (refresh_1 (cs_rep (f, P)))

goal (2 subgoals):
 1. P = {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
 2. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}

goal (1 subgoal):
 1. cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
by this
[PROOF STATE]
proof (state)
this:
cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}

goal (1 subgoal):
 1. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
P \<noteq> {}

goal (1 subgoal):
 1. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
have 4: "fst (the (cs_rep (g, Q) q)) = the (g q)" if "q \<in> \<Union>((transition A a) ` P)" for q
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst (the (cs_rep (g, Q) q)) = the (g q)
[PROOF STEP]
using 1(1) that assms(1)
[PROOF STATE]
proof (prove)
using this:
dom g = \<Union> (transition A a ` dom f)
q \<in> \<Union> (transition A a ` P)
P \<subseteq> dom f

goal (1 subgoal):
 1. fst (the (cs_rep (g, Q) q)) = the (g q)
[PROOF STEP]
by (fast intro: cs_rep_apply)
[PROOF STATE]
proof (state)
this:
?q \<in> \<Union> (transition A a ` P) \<Longrightarrow> fst (the (cs_rep (g, Q) ?q)) = the (g ?q)

goal (1 subgoal):
 1. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
have "cs_st (cs_rep (g, Q)) = Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cs_st (cs_rep (g, Q)) = Q
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
Q \<subseteq> dom g

goal (1 subgoal):
 1. cs_st (cs_rep (g, Q)) = Q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
cs_st (cs_rep (g, Q)) = Q

goal (1 subgoal):
 1. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
cs_st (cs_rep (g, Q)) = Q

goal (1 subgoal):
 1. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
have "\<dots> = {q \<in> \<Union>((transition A a) ` P). even (the (g q))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q = {q \<in> \<Union> (transition A a ` P). even (the (g q))}
[PROOF STEP]
unfolding 2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {q \<in> if P = {} then dom g else \<Union> (transition A a ` P). even (the (g q))} = {q \<in> \<Union> (transition A a ` P). even (the (g q))}
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
P \<noteq> {}

goal (1 subgoal):
 1. {q \<in> if P = {} then dom g else \<Union> (transition A a ` P). even (the (g q))} = {q \<in> \<Union> (transition A a ` P). even (the (g q))}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Q = {q \<in> \<Union> (transition A a ` P). even (the (g q))}

goal (1 subgoal):
 1. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Q = {q \<in> \<Union> (transition A a ` P). even (the (g q))}

goal (1 subgoal):
 1. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
have "\<dots> = {q \<in> \<Union>((transition A a) ` P). even (fst (the (cs_rep (g, Q) q)))}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {q \<in> \<Union> (transition A a ` P). even (the (g q))} = {q \<in> \<Union> (transition A a ` P). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
using 4
[PROOF STATE]
proof (prove)
using this:
?q \<in> \<Union> (transition A a ` P) \<Longrightarrow> fst (the (cs_rep (g, Q) ?q)) = the (g ?q)

goal (1 subgoal):
 1. {q \<in> \<Union> (transition A a ` P). even (the (g q))} = {q \<in> \<Union> (transition A a ` P). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
{q \<in> \<Union> (transition A a ` P). even (the (g q))} = {q \<in> \<Union> (transition A a ` P). even (fst (the (cs_rep (g, Q) q)))}

goal (1 subgoal):
 1. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
{q \<in> \<Union> (transition A a ` P). even (the (g q))} = {q \<in> \<Union> (transition A a ` P). even (fst (the (cs_rep (g, Q) q)))}

goal (1 subgoal):
 1. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
have "P = (cs_st (refresh_1 (cs_rep (f, P))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P = cs_st (refresh_1 (cs_rep (f, P)))
[PROOF STEP]
using assms(1) False
[PROOF STATE]
proof (prove)
using this:
P \<subseteq> dom f
P \<noteq> {}

goal (1 subgoal):
 1. P = cs_st (refresh_1 (cs_rep (f, P)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P = cs_st (refresh_1 (cs_rep (f, P)))

goal (1 subgoal):
 1. P \<noteq> {} \<Longrightarrow> cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}

goal (1 subgoal):
 1. cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
cs_st (cs_rep (g, Q)) = {q \<in> \<Union> (transition A a ` cs_st (refresh_1 (cs_rep (f, P)))). even (fst (the (cs_rep (g, Q) q)))}

goal:
No subgoals!
[PROOF STEP]
qed