[STATEMENT]
lemma poss_simps [simp]:
  "ghole_poss (GMFun f Cs) = {i # p | i p. i < length Cs \<and> p \<in> ghole_poss (Cs ! i)}"
  "poss_gmctxt (GMFun f Cs) = {[]} \<union> {i # p | i p. i < length Cs \<and> p \<in> poss_gmctxt (Cs ! i)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ghole_poss (GMFun f Cs) = {i # p |i p. i < length Cs \<and> p \<in> ghole_poss (Cs ! i)} &&& poss_gmctxt (GMFun f Cs) = {[]} \<union> {i # p |i p. i < length Cs \<and> p \<in> poss_gmctxt (Cs ! i)}
[PROOF STEP]
by auto


[STATEMENT]
lemma num_gholes_o_gmctxt_of_gterm [simp]:
  "num_gholes \<circ> gmctxt_of_gterm = (\<lambda>x. 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes \<circ> gmctxt_of_gterm = (\<lambda>x. 0)
[PROOF STEP]
by (rule ext, induct_tac x) simp_all


[STATEMENT]
lemma mctxt_of_term_term_of_mctxt_id [simp]:
  "num_gholes C = 0 \<Longrightarrow> gmctxt_of_gterm (gterm_of_gmctxt C) = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes C = 0 \<Longrightarrow> gmctxt_of_gterm (gterm_of_gmctxt C) = C
[PROOF STEP]
by (induct C) (simp_all add: map_idI)


[STATEMENT]
lemma num_holes_mctxt_of_term [simp]:
  "num_gholes (gmctxt_of_gterm t) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes (gmctxt_of_gterm t) = 0
[PROOF STEP]
by (induct t) simp_all


[STATEMENT]
lemma num_gholes_gmctxt_of_mctxt [simp]:
  "ground_mctxt C \<Longrightarrow> num_gholes (gmctxt_of_mctxt C) = num_holes C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground_mctxt C \<Longrightarrow> num_gholes (gmctxt_of_mctxt C) = num_holes C
[PROOF STEP]
by (induct C) (auto intro: nth_sum_listI)


[STATEMENT]
lemma num_holes_mctxt_of_gmctxt [simp]:
  "num_holes (mctxt_of_gmctxt C) = num_gholes C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_holes (mctxt_of_gmctxt C) = num_gholes C
[PROOF STEP]
by (induct C) (auto intro: nth_sum_listI)


[STATEMENT]
lemma num_holes_mctxt_of_gmctxt_fun_comp [simp]:
  "num_holes \<circ> mctxt_of_gmctxt = num_gholes"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_holes \<circ> mctxt_of_gmctxt = num_gholes
[PROOF STEP]
by (auto simp: comp_def)


[STATEMENT]
lemma gmctxt_of_gctxt_num_gholes [simp]:
  "num_gholes (gmctxt_of_gctxt C) = Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes (gmctxt_of_gctxt C) = Suc 0
[PROOF STEP]
by (induct C) auto


[STATEMENT]
lemma ground_mctxt_list_num_gholes_gmctxt_of_mctxt_conv [simp]:
  "\<forall>x\<in>set Cs. ground_mctxt x \<Longrightarrow> map (num_gholes \<circ> gmctxt_of_mctxt) Cs = map num_holes Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set Cs. ground_mctxt x \<Longrightarrow> map (num_gholes \<circ> gmctxt_of_mctxt) Cs = map num_holes Cs
[PROOF STEP]
by auto


[STATEMENT]
lemma num_gholes_map_gmctxt [simp]:
  "num_gholes (map_gmctxt f C) = num_gholes C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes (map_gmctxt f C) = num_gholes C
[PROOF STEP]
by (induct C)  (auto simp: comp_def, metis (no_types, lifting) map_eq_conv)


[STATEMENT]
lemma map_num_gholes_map_gmctxt [simp]:
  "map (num_gholes \<circ> map_gmctxt f) Cs = map num_gholes Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (num_gholes \<circ> map_gmctxt f) Cs = map num_gholes Cs
[PROOF STEP]
by (induct Cs) auto


[STATEMENT]
lemma gterm_of_gmctxt_gmctxt_of_gterm_id [simp]:
  "gterm_of_gmctxt (gmctxt_of_gterm t) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gterm_of_gmctxt (gmctxt_of_gterm t) = t
[PROOF STEP]
by (induct t) (simp_all add: map_idI)


[STATEMENT]
lemma no_gholes_gmctxt_of_gterm_gterm_of_gmctxt_id [simp]:
  "num_gholes C = 0 \<Longrightarrow> gmctxt_of_gterm (gterm_of_gmctxt C) = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes C = 0 \<Longrightarrow> gmctxt_of_gterm (gterm_of_gmctxt C) = C
[PROOF STEP]
by (induct C) (auto simp: comp_def intro: nth_equalityI)


[STATEMENT]
lemma no_gholes_term_of_gterm_gterm_of_gmctxt [simp]:
  "num_gholes C = 0 \<Longrightarrow> term_of_gterm (gterm_of_gmctxt C) = term_of_gmctxt C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes C = 0 \<Longrightarrow> term_of_gterm (gterm_of_gmctxt C) = term_of_gmctxt C
[PROOF STEP]
by (induct C) (auto simp: comp_def intro: nth_equalityI)


[STATEMENT]
lemma no_gholes_term_of_mctxt_mctxt_of_gmctxt [simp]:
  "num_gholes C = 0 \<Longrightarrow> term_of_mctxt (mctxt_of_gmctxt C) = term_of_gmctxt C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes C = 0 \<Longrightarrow> term_of_mctxt (mctxt_of_gmctxt C) = term_of_gmctxt C
[PROOF STEP]
by (induct C) (auto simp: comp_def intro: nth_equalityI)


[STATEMENT]
lemma nthWhile_gmctxt_of_gctxt [simp]:
  "length (takeWhile (\<lambda>C. num_gholes C = 0) (map gmctxt_of_gterm ss @ gmctxt_of_gctxt C # ts)) = length ss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (takeWhile (\<lambda>C. num_gholes C = 0) (map gmctxt_of_gterm ss @ gmctxt_of_gctxt C # ts)) = length ss
[PROOF STEP]
by (induct ss) auto


[STATEMENT]
lemma sum_list_nthWhile_length [simp]:
  "sum_list (map num_gholes Cs) = Suc 0 \<Longrightarrow> length (takeWhile (\<lambda>C. num_gholes C = 0) Cs) < length Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map num_gholes Cs) = Suc 0 \<Longrightarrow> length (takeWhile (\<lambda>C. num_gholes C = 0) Cs) < length Cs
[PROOF STEP]
by (induct Cs) auto


[STATEMENT]
lemma gctxt_of_gmctxt_gmctxt_of_gctxt [simp]:
  "gctxt_of_gmctxt (gmctxt_of_gctxt C) = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gctxt_of_gmctxt (gmctxt_of_gctxt C) = C
[PROOF STEP]
by (induct C) (auto simp: Let_def comp_def nth_append)


[STATEMENT]
lemma gmctxt_of_gctxt_GMHole_Hole:
  "gmctxt_of_gctxt C = GMHole \<Longrightarrow> C = \<box>\<^sub>G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gmctxt_of_gctxt C = GMHole \<Longrightarrow> C = \<box>\<^sub>G
[PROOF STEP]
by (metis gctxt_of_gmctxt.simps(1) gctxt_of_gmctxt_gmctxt_of_gctxt)


[STATEMENT]
lemma gmctxt_of_gctxt_gctxt_of_gmctxt:
  "num_gholes C = Suc 0 \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt C) = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes C = Suc 0 \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt C) = C
[PROOF STEP]
proof (induct C)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. num_gholes GMHole = Suc 0 \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt GMHole) = GMHole
 2. \<And>x1 x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; num_gholes x2a = Suc 0\<rbrakk> \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt x2a) = x2a; num_gholes (GMFun x1 x2) = Suc 0\<rbrakk> \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt (GMFun x1 x2)) = GMFun x1 x2
[PROOF STEP]
case (GMFun f Cs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set Cs; num_gholes ?x2a = Suc 0\<rbrakk> \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt ?x2a) = ?x2a
num_gholes (GMFun f Cs) = Suc 0

goal (2 subgoals):
 1. num_gholes GMHole = Suc 0 \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt GMHole) = GMHole
 2. \<And>x1 x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; num_gholes x2a = Suc 0\<rbrakk> \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt x2a) = x2a; num_gholes (GMFun x1 x2) = Suc 0\<rbrakk> \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt (GMFun x1 x2)) = GMFun x1 x2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x2a \<in> set Cs; num_gholes ?x2a = Suc 0\<rbrakk> \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt ?x2a) = ?x2a
num_gholes (GMFun f Cs) = Suc 0
[PROOF STEP]
obtain i where nth: "i < length Cs" "i = length (takeWhile (\<lambda>C. num_gholes C = 0) Cs)"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set Cs; num_gholes ?x2a = Suc 0\<rbrakk> \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt ?x2a) = ?x2a
num_gholes (GMFun f Cs) = Suc 0

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < length Cs; i = length (takeWhile (\<lambda>C. num_gholes C = 0) Cs)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using sum_list_nthWhile_length
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set Cs; num_gholes ?x2a = Suc 0\<rbrakk> \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt ?x2a) = ?x2a
num_gholes (GMFun f Cs) = Suc 0
sum_list (map num_gholes ?Cs) = Suc 0 \<Longrightarrow> length (takeWhile (\<lambda>C. num_gholes C = 0) ?Cs) < length ?Cs

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < length Cs; i = length (takeWhile (\<lambda>C. num_gholes C = 0) Cs)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length Cs
i = length (takeWhile (\<lambda>C. num_gholes C = 0) Cs)

goal (2 subgoals):
 1. num_gholes GMHole = Suc 0 \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt GMHole) = GMHole
 2. \<And>x1 x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; num_gholes x2a = Suc 0\<rbrakk> \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt x2a) = x2a; num_gholes (GMFun x1 x2) = Suc 0\<rbrakk> \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt (GMFun x1 x2)) = GMFun x1 x2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length Cs
i = length (takeWhile (\<lambda>C. num_gholes C = 0) Cs)
[PROOF STEP]
have "0 < num_gholes (Cs ! i)"
[PROOF STATE]
proof (prove)
using this:
i < length Cs
i = length (takeWhile (\<lambda>C. num_gholes C = 0) Cs)

goal (1 subgoal):
 1. 0 < num_gholes (Cs ! i)
[PROOF STEP]
unfolding nth(2)
[PROOF STATE]
proof (prove)
using this:
length (takeWhile (\<lambda>C. num_gholes C = 0) Cs) < length Cs
length (takeWhile (\<lambda>C. num_gholes C = 0) Cs) = length (takeWhile (\<lambda>C. num_gholes C = 0) Cs)

goal (1 subgoal):
 1. 0 < num_gholes (Cs ! length (takeWhile (\<lambda>C. num_gholes C = 0) Cs))
[PROOF STEP]
using nth_length_takeWhile
[PROOF STATE]
proof (prove)
using this:
length (takeWhile (\<lambda>C. num_gholes C = 0) Cs) < length Cs
length (takeWhile (\<lambda>C. num_gholes C = 0) Cs) = length (takeWhile (\<lambda>C. num_gholes C = 0) Cs)
length (takeWhile ?P ?xs) < length ?xs \<Longrightarrow> \<not> ?P (?xs ! length (takeWhile ?P ?xs))

goal (1 subgoal):
 1. 0 < num_gholes (Cs ! length (takeWhile (\<lambda>C. num_gholes C = 0) Cs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < num_gholes (Cs ! i)

goal (2 subgoals):
 1. num_gholes GMHole = Suc 0 \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt GMHole) = GMHole
 2. \<And>x1 x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; num_gholes x2a = Suc 0\<rbrakk> \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt x2a) = x2a; num_gholes (GMFun x1 x2) = Suc 0\<rbrakk> \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt (GMFun x1 x2)) = GMFun x1 x2
[PROOF STEP]
from nth(1) this
[PROOF STATE]
proof (chain)
picking this:
i < length Cs
0 < num_gholes (Cs ! i)
[PROOF STEP]
have num: "num_gholes (Cs ! i) = Suc 0"
[PROOF STATE]
proof (prove)
using this:
i < length Cs
0 < num_gholes (Cs ! i)

goal (1 subgoal):
 1. num_gholes (Cs ! i) = Suc 0
[PROOF STEP]
using GMFun(2)
[PROOF STATE]
proof (prove)
using this:
i < length Cs
0 < num_gholes (Cs ! i)
num_gholes (GMFun f Cs) = Suc 0

goal (1 subgoal):
 1. num_gholes (Cs ! i) = Suc 0
[PROOF STEP]
by (auto elim!: sum_list_1_E)
[PROOF STATE]
proof (state)
this:
num_gholes (Cs ! i) = Suc 0

goal (2 subgoals):
 1. num_gholes GMHole = Suc 0 \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt GMHole) = GMHole
 2. \<And>x1 x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; num_gholes x2a = Suc 0\<rbrakk> \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt x2a) = x2a; num_gholes (GMFun x1 x2) = Suc 0\<rbrakk> \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt (GMFun x1 x2)) = GMFun x1 x2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
num_gholes (Cs ! i) = Suc 0
[PROOF STEP]
have [simp]: "map (gmctxt_of_gterm \<circ> gterm_of_gmctxt) (drop (Suc i) Cs) = drop (Suc i) Cs"
[PROOF STATE]
proof (prove)
using this:
num_gholes (Cs ! i) = Suc 0

goal (1 subgoal):
 1. map (gmctxt_of_gterm \<circ> gterm_of_gmctxt) (drop (Suc i) Cs) = drop (Suc i) Cs
[PROOF STEP]
using GMFun(2) nth(1)
[PROOF STATE]
proof (prove)
using this:
num_gholes (Cs ! i) = Suc 0
num_gholes (GMFun f Cs) = Suc 0
i < length Cs

goal (1 subgoal):
 1. map (gmctxt_of_gterm \<circ> gterm_of_gmctxt) (drop (Suc i) Cs) = drop (Suc i) Cs
[PROOF STEP]
by (auto elim!: sum_list_1_E simp: comp_def intro!: nth_equalityI)
     (metis add.commute add_Suc_right lessI less_diff_conv no_gholes_gmctxt_of_gterm_gterm_of_gmctxt_id not_add_less1)
[PROOF STATE]
proof (state)
this:
map (gmctxt_of_gterm \<circ> gterm_of_gmctxt) (drop (Suc i) Cs) = drop (Suc i) Cs

goal (2 subgoals):
 1. num_gholes GMHole = Suc 0 \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt GMHole) = GMHole
 2. \<And>x1 x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; num_gholes x2a = Suc 0\<rbrakk> \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt x2a) = x2a; num_gholes (GMFun x1 x2) = Suc 0\<rbrakk> \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt (GMFun x1 x2)) = GMFun x1 x2
[PROOF STEP]
have [simp]: "map (gmctxt_of_gterm \<circ> gterm_of_gmctxt) (take i Cs) = take i Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (gmctxt_of_gterm \<circ> gterm_of_gmctxt) (take i Cs) = take i Cs
[PROOF STEP]
using nth(1)
[PROOF STATE]
proof (prove)
using this:
i < length Cs

goal (1 subgoal):
 1. map (gmctxt_of_gterm \<circ> gterm_of_gmctxt) (take i Cs) = take i Cs
[PROOF STEP]
unfolding nth(2)
[PROOF STATE]
proof (prove)
using this:
length (takeWhile (\<lambda>C. num_gholes C = 0) Cs) < length Cs

goal (1 subgoal):
 1. map (gmctxt_of_gterm \<circ> gterm_of_gmctxt) (take (length (takeWhile (\<lambda>C. num_gholes C = 0) Cs)) Cs) = take (length (takeWhile (\<lambda>C. num_gholes C = 0) Cs)) Cs
[PROOF STEP]
by (induct Cs) auto
[PROOF STATE]
proof (state)
this:
map (gmctxt_of_gterm \<circ> gterm_of_gmctxt) (take i Cs) = take i Cs

goal (2 subgoals):
 1. num_gholes GMHole = Suc 0 \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt GMHole) = GMHole
 2. \<And>x1 x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; num_gholes x2a = Suc 0\<rbrakk> \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt x2a) = x2a; num_gholes (GMFun x1 x2) = Suc 0\<rbrakk> \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt (GMFun x1 x2)) = GMFun x1 x2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gmctxt_of_gctxt (gctxt_of_gmctxt (GMFun f Cs)) = GMFun f Cs
[PROOF STEP]
using id_take_nth_drop[OF nth(1)]
[PROOF STATE]
proof (prove)
using this:
Cs = take i Cs @ Cs ! i # drop (Suc i) Cs

goal (1 subgoal):
 1. gmctxt_of_gctxt (gctxt_of_gmctxt (GMFun f Cs)) = GMFun f Cs
[PROOF STEP]
by (auto simp: Let_def GMFun(1)[OF nth_mem[OF nth(1)] num] simp flip: nth(2))
[PROOF STATE]
proof (state)
this:
gmctxt_of_gctxt (gctxt_of_gmctxt (GMFun f Cs)) = GMFun f Cs

goal (1 subgoal):
 1. num_gholes GMHole = Suc 0 \<Longrightarrow> gmctxt_of_gctxt (gctxt_of_gmctxt GMHole) = GMHole
[PROOF STEP]
qed auto


[STATEMENT]
lemma inj_gmctxt_of_gctxt: "inj gmctxt_of_gctxt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj gmctxt_of_gctxt
[PROOF STEP]
unfolding inj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x y. gmctxt_of_gctxt x = gmctxt_of_gctxt y \<longrightarrow> x = y
[PROOF STEP]
by (metis gctxt_of_gmctxt_gmctxt_of_gctxt)


[STATEMENT]
lemma inj_gctxt_of_gmctxt_on_single_hole:
  "inj_on gctxt_of_gmctxt (Collect (\<lambda> C. num_gholes C = Suc 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on gctxt_of_gmctxt {C. num_gholes C = Suc 0}
[PROOF STEP]
by (metis (mono_tags, lifting) gmctxt_of_gctxt_gctxt_of_gmctxt inj_onI mem_Collect_eq)


[STATEMENT]
lemma gctxt_of_gmctxt_hole_dest:
  "num_gholes C = Suc 0 \<Longrightarrow> gctxt_of_gmctxt C = \<box>\<^sub>G \<Longrightarrow> C = GMHole"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>num_gholes C = Suc 0; gctxt_of_gmctxt C = \<box>\<^sub>G\<rbrakk> \<Longrightarrow> C = GMHole
[PROOF STEP]
by (cases C) (auto simp: Let_def split!: if_splits)


[STATEMENT]
lemma mctxt_of_gmctxt_inv [simp]:
  "gmctxt_of_mctxt (mctxt_of_gmctxt C) = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gmctxt_of_mctxt (mctxt_of_gmctxt C) = C
[PROOF STEP]
by (induct C) (simp_all add: map_idI)


[STATEMENT]
lemma ground_mctxt_of_gmctxt [simp]:
  "ground_mctxt (mctxt_of_gmctxt C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground_mctxt (mctxt_of_gmctxt C)
[PROOF STEP]
by (induct C) auto


[STATEMENT]
lemma ground_mctxt_of_gmctxt' [simp]:
  "mctxt_of_gmctxt C = MFun f D \<Longrightarrow> ground_mctxt (MFun f D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mctxt_of_gmctxt C = MFun f D \<Longrightarrow> ground_mctxt (MFun f D)
[PROOF STEP]
by (induct C) auto


[STATEMENT]
lemma gmctxt_of_mctxt_inv [simp]:
  "ground_mctxt C \<Longrightarrow> mctxt_of_gmctxt (gmctxt_of_mctxt C) = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground_mctxt C \<Longrightarrow> mctxt_of_gmctxt (gmctxt_of_mctxt C) = C
[PROOF STEP]
by (induct C) (auto 0 0 intro!: nth_equalityI)


[STATEMENT]
lemma ground_mctxt_of_gmctxtD:
  "ground_mctxt C \<Longrightarrow> \<exists> D. C = mctxt_of_gmctxt D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground_mctxt C \<Longrightarrow> \<exists>D. C = mctxt_of_gmctxt D
[PROOF STEP]
by (metis gmctxt_of_mctxt_inv)


[STATEMENT]
lemma inj_mctxt_of_gmctxt: "inj_on mctxt_of_gmctxt X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on mctxt_of_gmctxt X
[PROOF STEP]
by (metis inj_on_def mctxt_of_gmctxt_inv)


[STATEMENT]
lemma inj_gmctxt_of_mctxt_ground:
  "inj_on gmctxt_of_mctxt (Collect ground_mctxt)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on gmctxt_of_mctxt (Collect ground_mctxt)
[PROOF STEP]
using gmctxt_of_mctxt_inv inj_on_def
[PROOF STATE]
proof (prove)
using this:
ground_mctxt ?C \<Longrightarrow> mctxt_of_gmctxt (gmctxt_of_mctxt ?C) = ?C
inj_on ?f ?A = (\<forall>x\<in>?A. \<forall>y\<in>?A. ?f x = ?f y \<longrightarrow> x = y)

goal (1 subgoal):
 1. inj_on gmctxt_of_mctxt (Collect ground_mctxt)
[PROOF STEP]
by force


[STATEMENT]
lemma map_gmctxt_comp [simp]:
  "map_gmctxt f (map_gmctxt g C) = map_gmctxt (f \<circ> g) C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_gmctxt f (map_gmctxt g C) = map_gmctxt (f \<circ> g) C
[PROOF STEP]
by (induct C) auto


[STATEMENT]
lemma map_mctxt_of_gmctxt:
  "map_mctxt f (mctxt_of_gmctxt C) = mctxt_of_gmctxt (map_gmctxt f C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Multihole_Context.map_mctxt f (mctxt_of_gmctxt C) = mctxt_of_gmctxt (map_gmctxt f C)
[PROOF STEP]
by (induct C) auto


[STATEMENT]
lemma map_gmctxt_of_mctxt:
  "ground_mctxt C \<Longrightarrow> map_gmctxt f (gmctxt_of_mctxt C) = gmctxt_of_mctxt (map_mctxt f C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground_mctxt C \<Longrightarrow> map_gmctxt f (gmctxt_of_mctxt C) = gmctxt_of_mctxt (Multihole_Context.map_mctxt f C)
[PROOF STEP]
by (induct C) auto


[STATEMENT]
lemma map_gmctxt_nempty [simp]:
  "C \<noteq> GMHole \<Longrightarrow> map_gmctxt f C \<noteq> GMHole"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<noteq> GMHole \<Longrightarrow> map_gmctxt f C \<noteq> GMHole
[PROOF STEP]
by (cases C) auto


[STATEMENT]
lemma vars_mctxt_of_gmctxt [simp]:
  "vars_mctxt (mctxt_of_gmctxt C) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars_mctxt (mctxt_of_gmctxt C) = {}
[PROOF STEP]
by (induct C) auto


[STATEMENT]
lemma vars_mctxt_of_gmctxt_subseteq [simp]:
  "vars_mctxt (mctxt_of_gmctxt C) \<subseteq> Q \<longleftrightarrow> True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (vars_mctxt (mctxt_of_gmctxt C) \<subseteq> Q) = True
[PROOF STEP]
by auto


[STATEMENT]
lemma eqgfE:
  assumes "t =\<^sub>G\<^sub>f (D, ss)" shows "t = fill_gholes D ss" "num_gholes D = length ss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t = fill_gholes D ss &&& num_gholes D = length ss
[PROOF STEP]
using assms[unfolded eq_gfill.simps]
[PROOF STATE]
proof (prove)
using this:
\<exists>ta Da ssa. t = ta \<and> (D, ss) = (Da, ssa) \<and> ta = fill_gholes Da ssa \<and> num_gholes Da = length ssa

goal (1 subgoal):
 1. t = fill_gholes D ss &&& num_gholes D = length ss
[PROOF STEP]
by auto


[STATEMENT]
lemma eqgf_GMHoleE:
  assumes "t =\<^sub>G\<^sub>f (GMHole, ss)" shows "ss = [t]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ss = [t]
[PROOF STEP]
using eqgfE[OF assms]
[PROOF STATE]
proof (prove)
using this:
t = fill_gholes GMHole ss
num_gholes GMHole = length ss

goal (1 subgoal):
 1. ss = [t]
[PROOF STEP]
by (cases ss) auto


[STATEMENT]
lemma eqgf_GMFunE:
  assumes "s =\<^sub>G\<^sub>f (GMFun f Cs, ss)"
  obtains ts sss where "s = GFun f ts" "length ts = length Cs" "length sss = length Cs"
  "\<And> i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>G\<^sub>f (Cs ! i, sss ! i)" "ss = concat sss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ts sss. \<lbrakk>s = GFun f ts; length ts = length Cs; length sss = length Cs; \<And>i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>G\<^sub>f (Cs ! i, sss ! i); ss = concat sss\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>ts sss. \<lbrakk>s = GFun f ts; length ts = length Cs; length sss = length Cs; \<And>i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>G\<^sub>f (Cs ! i, sss ! i); ss = concat sss\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from eqgfE[OF assms]
[PROOF STATE]
proof (chain)
picking this:
s = fill_gholes (GMFun f Cs) ss
num_gholes (GMFun f Cs) = length ss
[PROOF STEP]
have fh: "s = fill_gholes (GMFun f Cs) ss"
    and nh: "sum_list (map num_gholes Cs) = length ss"
[PROOF STATE]
proof (prove)
using this:
s = fill_gholes (GMFun f Cs) ss
num_gholes (GMFun f Cs) = length ss

goal (1 subgoal):
 1. s = fill_gholes (GMFun f Cs) ss &&& sum_list (map num_gholes Cs) = length ss
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
s = fill_gholes (GMFun f Cs) ss
sum_list (map num_gholes Cs) = length ss

goal (1 subgoal):
 1. (\<And>ts sss. \<lbrakk>s = GFun f ts; length ts = length Cs; length sss = length Cs; \<And>i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>G\<^sub>f (Cs ! i, sss ! i); ss = concat sss\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from fh
[PROOF STATE]
proof (chain)
picking this:
s = fill_gholes (GMFun f Cs) ss
[PROOF STEP]
obtain ts where s: "s = GFun f ts"
[PROOF STATE]
proof (prove)
using this:
s = fill_gholes (GMFun f Cs) ss

goal (1 subgoal):
 1. (\<And>ts. s = GFun f ts \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases s, auto)
[PROOF STATE]
proof (state)
this:
s = GFun f ts

goal (1 subgoal):
 1. (\<And>ts sss. \<lbrakk>s = GFun f ts; length ts = length Cs; length sss = length Cs; \<And>i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>G\<^sub>f (Cs ! i, sss ! i); ss = concat sss\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from fh[unfolded s]
[PROOF STATE]
proof (chain)
picking this:
GFun f ts = fill_gholes (GMFun f Cs) ss
[PROOF STEP]
have ts: "ts = map (\<lambda>i. fill_gholes (Cs ! i) (partition_gholes ss Cs ! i)) [0..<length Cs]"
    (is "_ = map (?f Cs ss) _")
[PROOF STATE]
proof (prove)
using this:
GFun f ts = fill_gholes (GMFun f Cs) ss

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

goal (1 subgoal):
 1. (\<And>ts sss. \<lbrakk>s = GFun f ts; length ts = length Cs; length sss = length Cs; \<And>i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>G\<^sub>f (Cs ! i, sss ! i); ss = concat sss\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
let ?sss = "partition_gholes ss Cs"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>ts sss. \<lbrakk>s = GFun f ts; length ts = length Cs; length sss = length Cs; \<And>i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>G\<^sub>f (Cs ! i, sss ! i); ss = concat sss\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from nh
[PROOF STATE]
proof (chain)
picking this:
sum_list (map num_gholes Cs) = length ss
[PROOF STEP]
have *: "length ?sss = length Cs"
    "\<And>i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>G\<^sub>f (Cs ! i, ?sss ! i)" "ss = concat ?sss"
[PROOF STATE]
proof (prove)
using this:
sum_list (map num_gholes Cs) = length ss

goal (1 subgoal):
 1. length (partition_gholes ss Cs) = length Cs &&& (\<And>i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ss Cs ! i)) &&& ss = concat (partition_gholes ss Cs)
[PROOF STEP]
by (auto simp: ts length_partition_by_nth)
[PROOF STATE]
proof (state)
this:
length (partition_gholes ss Cs) = length Cs
?i < length Cs \<Longrightarrow> ts ! ?i =\<^sub>G\<^sub>f (Cs ! ?i, partition_gholes ss Cs ! ?i)
ss = concat (partition_gholes ss Cs)

goal (1 subgoal):
 1. (\<And>ts sss. \<lbrakk>s = GFun f ts; length ts = length Cs; length sss = length Cs; \<And>i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>G\<^sub>f (Cs ! i, sss ! i); ss = concat sss\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have len: "length ts = length Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ts = length Cs
[PROOF STEP]
unfolding ts
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map (\<lambda>i. fill_gholes (Cs ! i) (partition_gholes ss Cs ! i)) [0..<length Cs]) = length Cs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length ts = length Cs

goal (1 subgoal):
 1. (\<And>ts sss. \<lbrakk>s = GFun f ts; length ts = length Cs; length sss = length Cs; \<And>i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>G\<^sub>f (Cs ! i, sss ! i); ss = concat sss\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume ass: "\<And>ts sss. s = GFun f ts \<Longrightarrow>
              length ts = length Cs \<Longrightarrow>
              length sss = length Cs \<Longrightarrow> (\<And>i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>G\<^sub>f (Cs ! i, sss ! i)) \<Longrightarrow> ss = concat sss \<Longrightarrow> thesis"
[PROOF STATE]
proof (state)
this:
\<lbrakk>s = GFun f ?ts; length ?ts = length Cs; length ?sss = length Cs; \<And>i. i < length Cs \<Longrightarrow> ?ts ! i =\<^sub>G\<^sub>f (Cs ! i, ?sss ! i); ss = concat ?sss\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. (\<And>ts sss. \<lbrakk>s = GFun f ts; length ts = length Cs; length sss = length Cs; \<And>i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>G\<^sub>f (Cs ! i, sss ! i); ss = concat sss\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
show thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule ass[OF s len *])
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partition_holes_subseteq [simp]:
  assumes "sum_list (map num_holes Cs) = length xs" "i < length Cs"
    and "x \<in> set (partition_holes xs Cs ! i)"
  shows "x \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set xs
[PROOF STEP]
using assms partition_by_nth_nth_elem length_partition_by_nth
[PROOF STATE]
proof (prove)
using this:
sum_list (map num_holes Cs) = length xs
i < length Cs
x \<in> set (partition_holes xs Cs ! i)
\<lbrakk>sum_list ?ys = length ?xs; ?i < length ?ys; ?j < ?ys ! ?i\<rbrakk> \<Longrightarrow> partition_by ?xs ?ys ! ?i ! ?j \<in> set ?xs
\<lbrakk>sum_list ?ys = length ?xs; ?i < length ?ys\<rbrakk> \<Longrightarrow> length (partition_by ?xs ?ys ! ?i) = ?ys ! ?i

goal (1 subgoal):
 1. x \<in> set xs
[PROOF STEP]
by (auto simp: in_set_conv_nth) fastforce


[STATEMENT]
lemma partition_gholes_subseteq [simp]:
  assumes "sum_list (map num_gholes Cs) = length xs" "i < length Cs"
    and "x \<in> set (partition_gholes xs Cs ! i)"
  shows "x \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set xs
[PROOF STEP]
using assms partition_by_nth_nth_elem length_partition_by_nth
[PROOF STATE]
proof (prove)
using this:
sum_list (map num_gholes Cs) = length xs
i < length Cs
x \<in> set (partition_gholes xs Cs ! i)
\<lbrakk>sum_list ?ys = length ?xs; ?i < length ?ys; ?j < ?ys ! ?i\<rbrakk> \<Longrightarrow> partition_by ?xs ?ys ! ?i ! ?j \<in> set ?xs
\<lbrakk>sum_list ?ys = length ?xs; ?i < length ?ys\<rbrakk> \<Longrightarrow> length (partition_by ?xs ?ys ! ?i) = ?ys ! ?i

goal (1 subgoal):
 1. x \<in> set xs
[PROOF STEP]
by (auto simp: in_set_conv_nth) fastforce


[STATEMENT]
lemma list_elem_to_partition_nth [elim]:
  assumes "sum_list (map num_gholes Cs) = length xs" "x \<in> set xs"
  obtains i where "i < length Cs" "x \<in> set (partition_gholes xs Cs ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < length Cs; x \<in> set (partition_gholes xs Cs ! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sum_list (map num_gholes Cs) = length xs
x \<in> set xs

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < length Cs; x \<in> set (partition_gholes xs Cs ! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis concat_partition_by in_set_idx length_map length_partition_by nth_concat_split nth_mem)


[STATEMENT]
lemma partition_holes_fill_gholes_conv':
  "fill_gholes (GMFun f Cs) ts =
    GFun f (map (case_prod fill_gholes) (zip Cs (partition_gholes ts Cs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_gholes (GMFun f Cs) ts = GFun f (map2 fill_gholes Cs (partition_gholes ts Cs))
[PROOF STEP]
unfolding zip_nth_conv [of Cs "partition_gholes ts Cs", simplified]
    and partition_holes_fill_holes_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_gholes (GMFun f Cs) ts = GFun f (map (\<lambda>(x, y). fill_gholes x y) (map (\<lambda>i. (Cs ! i, partition_gholes ts Cs ! i)) [0..<length Cs]))
[PROOF STEP]
by simp


[STATEMENT]
lemma unfill_gholes_conv:
  assumes "length Cs = length ts"
  shows "unfill_gholes (GMFun f Cs) (GFun f ts) =
    concat (map (case_prod unfill_gholes) (zip Cs ts))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unfill_gholes (GMFun f Cs) (GFun f ts) = concat (map2 unfill_gholes Cs ts)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length Cs = length ts

goal (1 subgoal):
 1. unfill_gholes (GMFun f Cs) (GFun f ts) = concat (map2 unfill_gholes Cs ts)
[PROOF STEP]
by (auto simp: zip_nth_conv [of Cs ts, simplified] comp_def)


[STATEMENT]
lemma partition_holes_fill_gholes_gmctxt_conv:
  "fill_gholes_gmctxt (GMFun f Cs) ts =
    GMFun f [fill_gholes_gmctxt (Cs ! i) (partition_gholes ts Cs ! i). i \<leftarrow> [0 ..< length Cs]]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_gholes_gmctxt (GMFun f Cs) ts = GMFun f (map (\<lambda>i. fill_gholes_gmctxt (Cs ! i) (partition_gholes ts Cs ! i)) [0..<length Cs])
[PROOF STEP]
by (simp add: partition_by_nth take_map)


[STATEMENT]
lemma partition_holes_fill_gholes_gmctxt_conv':
  "fill_gholes_gmctxt (GMFun f Cs) ts =
    GMFun f (map (case_prod fill_gholes_gmctxt) (zip Cs (partition_gholes ts Cs)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_gholes_gmctxt (GMFun f Cs) ts = GMFun f (map2 fill_gholes_gmctxt Cs (partition_gholes ts Cs))
[PROOF STEP]
unfolding zip_nth_conv [of Cs "partition_gholes ts Cs", simplified]
    and partition_holes_fill_gholes_gmctxt_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. GMFun f (map (\<lambda>i. fill_gholes_gmctxt (Cs ! i) (partition_gholes ts Cs ! i)) [0..<length Cs]) = GMFun f (map (\<lambda>(x, y). fill_gholes_gmctxt x y) (map (\<lambda>i. (Cs ! i, partition_gholes ts Cs ! i)) [0..<length Cs]))
[PROOF STEP]
by simp


[STATEMENT]
lemma fill_gholes_no_holes [simp]:
  "num_gholes C = 0 \<Longrightarrow> fill_gholes C [] = gterm_of_gmctxt C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes C = 0 \<Longrightarrow> fill_gholes C [] = gterm_of_gmctxt C
[PROOF STEP]
by (induct C) (auto simp: partition_holes_fill_gholes_conv'
    simp del: fill_gholes.simps intro: nth_equalityI)


[STATEMENT]
lemma fill_gholes_gmctxt_no_holes [simp]:
  "num_gholes C = 0 \<Longrightarrow> fill_gholes_gmctxt C [] = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes C = 0 \<Longrightarrow> fill_gholes_gmctxt C [] = C
[PROOF STEP]
by (induct C) (auto intro: nth_equalityI)


[STATEMENT]
lemma eqgf_GMFunI:
  assumes "\<And> i. i < length Cs \<Longrightarrow> ss ! i =\<^sub>G\<^sub>f (Cs ! i, ts ! i)"
    and "length Cs = length ss" "length ss = length ts"
  shows "GFun f ss =\<^sub>G\<^sub>f (GMFun f Cs, concat ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. GFun f ss =\<^sub>G\<^sub>f (GMFun f Cs, concat ts)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?i < length Cs \<Longrightarrow> ss ! ?i =\<^sub>G\<^sub>f (Cs ! ?i, ts ! ?i)
length Cs = length ss
length ss = length ts

goal (1 subgoal):
 1. GFun f ss =\<^sub>G\<^sub>f (GMFun f Cs, concat ts)
[PROOF STEP]
apply (auto simp del: fill_gholes.simps
    simp: partition_holes_fill_gholes_conv' intro!: eq_gfill.intros nth_equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>i. \<lbrakk>\<And>i. i < length ts \<Longrightarrow> ss ! i =\<^sub>G\<^sub>f (Cs ! i, ts ! i); length Cs = length ts; length ss = length ts; i < length ts\<rbrakk> \<Longrightarrow> ss ! i = fill_gholes (Cs ! i) (partition_gholes (concat ts) Cs ! i)
 2. \<lbrakk>\<And>i. i < length ts \<Longrightarrow> ss ! i =\<^sub>G\<^sub>f (Cs ! i, ts ! i); length Cs = length ts; length ss = length ts\<rbrakk> \<Longrightarrow> sum_list (map num_gholes Cs) = length (concat ts)
[PROOF STEP]
apply (metis eqgfE length_map map_nth_eq_conv partition_by_concat_id)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>i. i < length ts \<Longrightarrow> ss ! i =\<^sub>G\<^sub>f (Cs ! i, ts ! i); length Cs = length ts; length ss = length ts\<rbrakk> \<Longrightarrow> sum_list (map num_gholes Cs) = length (concat ts)
[PROOF STEP]
by (metis eqgfE(2) length_concat nth_map_conv)


[STATEMENT]
lemma length_partition_gholes_nth:
  assumes "sum_list (map num_gholes cs) = length ts"
    and "i < length cs"
  shows "length (partition_gholes ts cs ! i) = num_gholes (cs ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (partition_gholes ts cs ! i) = num_gholes (cs ! i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sum_list (map num_gholes cs) = length ts
i < length cs

goal (1 subgoal):
 1. length (partition_gholes ts cs ! i) = num_gholes (cs ! i)
[PROOF STEP]
by (simp add: length_partition_by_nth)


[STATEMENT]
lemma fill_gholes_induct2[consumes 2, case_names GMHole GMFun]:
  fixes P :: "'f gmctxt \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> bool"
  assumes len1: "num_gholes C = length xs" and len2: "num_gholes C = length ys"
  and Hole: "\<And>x y. P GMHole [x] [y]"
  and Fun: "\<And>f Cs xs ys.  sum_list (map num_gholes Cs) = length xs \<Longrightarrow>
    sum_list (map num_gholes Cs) = length ys \<Longrightarrow>
    (\<And>i. i < length Cs \<Longrightarrow> P (Cs ! i) (partition_gholes xs Cs ! i) (partition_gholes ys Cs ! i)) \<Longrightarrow>
    P (GMFun f Cs) (concat (partition_gholes xs Cs)) (concat (partition_gholes ys Cs))"
  shows "P C xs ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P C xs ys
[PROOF STEP]
proof (insert len1 len2, induct C arbitrary: xs ys)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs ys. \<lbrakk>num_gholes GMHole = length xs; num_gholes GMHole = length ys\<rbrakk> \<Longrightarrow> P GMHole xs ys
 2. \<And>x1 x2 xs ys. \<lbrakk>\<And>x2a xs ys. \<lbrakk>x2a \<in> set x2; num_gholes x2a = length xs; num_gholes x2a = length ys\<rbrakk> \<Longrightarrow> P x2a xs ys; num_gholes (GMFun x1 x2) = length xs; num_gholes (GMFun x1 x2) = length ys\<rbrakk> \<Longrightarrow> P (GMFun x1 x2) xs ys
[PROOF STEP]
case GMHole
[PROOF STATE]
proof (state)
this:
num_gholes GMHole = length xs
num_gholes GMHole = length ys

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

goal (1 subgoal):
 1. P GMHole xs ys
[PROOF STEP]
using Hole
[PROOF STATE]
proof (prove)
using this:
num_gholes GMHole = length xs
num_gholes GMHole = length ys
P GMHole [?x] [?y]

goal (1 subgoal):
 1. P GMHole xs ys
[PROOF STEP]
by (cases xs; cases ys) auto
[PROOF STATE]
proof (state)
this:
P GMHole xs ys

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

goal (1 subgoal):
 1. \<And>x1 x2 xs ys. \<lbrakk>\<And>x2a xs ys. \<lbrakk>x2a \<in> set x2; num_gholes x2a = length xs; num_gholes x2a = length ys\<rbrakk> \<Longrightarrow> P x2a xs ys; num_gholes (GMFun x1 x2) = length xs; num_gholes (GMFun x1 x2) = length ys\<rbrakk> \<Longrightarrow> P (GMFun x1 x2) xs ys
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x2a \<in> set Cs; num_gholes ?x2a = length ?xs; num_gholes ?x2a = length ?ys\<rbrakk> \<Longrightarrow> P ?x2a ?xs ?ys
num_gholes (GMFun f Cs) = length xs
num_gholes (GMFun f Cs) = length ys
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set Cs; num_gholes ?x2a = length ?xs; num_gholes ?x2a = length ?ys\<rbrakk> \<Longrightarrow> P ?x2a ?xs ?ys
num_gholes (GMFun f Cs) = length xs
num_gholes (GMFun f Cs) = length ys

goal (1 subgoal):
 1. P (GMFun f Cs) xs ys
[PROOF STEP]
using Fun[of Cs xs ys f]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set Cs; num_gholes ?x2a = length ?xs; num_gholes ?x2a = length ?ys\<rbrakk> \<Longrightarrow> P ?x2a ?xs ?ys
num_gholes (GMFun f Cs) = length xs
num_gholes (GMFun f Cs) = length ys
\<lbrakk>sum_list (map num_gholes Cs) = length xs; sum_list (map num_gholes Cs) = length ys; \<And>i. i < length Cs \<Longrightarrow> P (Cs ! i) (partition_gholes xs Cs ! i) (partition_gholes ys Cs ! i)\<rbrakk> \<Longrightarrow> P (GMFun f Cs) (concat (partition_gholes xs Cs)) (concat (partition_gholes ys Cs))

goal (1 subgoal):
 1. P (GMFun f Cs) xs ys
[PROOF STEP]
by (auto simp: length_partition_by_nth)
[PROOF STATE]
proof (state)
this:
P (GMFun f Cs) xs ys

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fill_gholes_induct[consumes 1, case_names GMHole GMFun]:
  fixes P :: "'f gmctxt \<Rightarrow> 'a list \<Rightarrow> bool"
  assumes len: "num_gholes C = length xs"
    and Hole: "\<And>x. P GMHole [x]"
    and Fun: "\<And>f Cs xs. sum_list (map num_gholes Cs) = length xs \<Longrightarrow>
      (\<And>i. i < length Cs \<Longrightarrow> P (Cs ! i) (partition_gholes xs Cs ! i)) \<Longrightarrow>
      P (GMFun f Cs) (concat (partition_gholes xs Cs))"
  shows "P C xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P C xs
[PROOF STEP]
using fill_gholes_induct2[of C xs xs "\<lambda> C xs _. P C xs"] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>num_gholes C = length xs; num_gholes C = length xs; \<And>x y. P GMHole [x]; \<And>f Cs xs ys. \<lbrakk>sum_list (map num_gholes Cs) = length xs; sum_list (map num_gholes Cs) = length ys; \<And>i. i < length Cs \<Longrightarrow> P (Cs ! i) (partition_gholes xs Cs ! i)\<rbrakk> \<Longrightarrow> P (GMFun f Cs) (concat (partition_gholes xs Cs))\<rbrakk> \<Longrightarrow> P C xs
num_gholes C = length xs
P GMHole [?x]
\<lbrakk>sum_list (map num_gholes ?Cs) = length ?xs; \<And>i. i < length ?Cs \<Longrightarrow> P (?Cs ! i) (partition_gholes ?xs ?Cs ! i)\<rbrakk> \<Longrightarrow> P (GMFun ?f ?Cs) (concat (partition_gholes ?xs ?Cs))

goal (1 subgoal):
 1. P C xs
[PROOF STEP]
by simp


[STATEMENT]
lemma eq_gfill_induct [consumes 1, case_names GMHole GMFun]:
  assumes "t =\<^sub>G\<^sub>f (C, ts)"
    and "\<And>t. P t GMHole [t]"
    and "\<And>f ss Cs ts. \<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>
        P (ss ! i) (Cs ! i) (partition_gholes ts Cs ! i)\<rbrakk>
      \<Longrightarrow> P (GFun f ss) (GMFun f Cs) ts"
  shows "P t C ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P t C ts
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
t =\<^sub>G\<^sub>f (C, ts)

goal (1 subgoal):
 1. P t C ts
[PROOF STEP]
proof (induct t arbitrary: C ts)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2a C ts. \<lbrakk>\<And>x2aa C ts. \<lbrakk>x2aa \<in> set x2a; x2aa =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P x2aa C ts; GFun x1a x2a =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P (GFun x1a x2a) C ts
[PROOF STEP]
case (GFun f ss)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2aa \<in> set ss; ?x2aa =\<^sub>G\<^sub>f (?C, ?ts)\<rbrakk> \<Longrightarrow> P ?x2aa ?C ?ts
GFun f ss =\<^sub>G\<^sub>f (C, ts)

goal (1 subgoal):
 1. \<And>x1a x2a C ts. \<lbrakk>\<And>x2aa C ts. \<lbrakk>x2aa \<in> set x2a; x2aa =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P x2aa C ts; GFun x1a x2a =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P (GFun x1a x2a) C ts
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2aa \<in> set ss; ?x2aa =\<^sub>G\<^sub>f (?C, ?ts)\<rbrakk> \<Longrightarrow> P ?x2aa ?C ?ts
GFun f ss =\<^sub>G\<^sub>f (C, ts)

goal (1 subgoal):
 1. \<And>x1a x2a C ts. \<lbrakk>\<And>x2aa C ts. \<lbrakk>x2aa \<in> set x2a; x2aa =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P x2aa C ts; GFun x1a x2a =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P (GFun x1a x2a) C ts
[PROOF STEP]
assume "C = GMHole" and "ts = [GFun f ss]"
[PROOF STATE]
proof (state)
this:
C = GMHole
ts = [GFun f ss]

goal (1 subgoal):
 1. \<And>x1a x2a C ts. \<lbrakk>\<And>x2aa C ts. \<lbrakk>x2aa \<in> set x2a; x2aa =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P x2aa C ts; GFun x1a x2a =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P (GFun x1a x2a) C ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C = GMHole
ts = [GFun f ss]
[PROOF STEP]
have ?case
[PROOF STATE]
proof (prove)
using this:
C = GMHole
ts = [GFun f ss]

goal (1 subgoal):
 1. P (GFun f ss) C ts
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
C = GMHole
ts = [GFun f ss]
P ?t GMHole [?t]

goal (1 subgoal):
 1. P (GFun f ss) C ts
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P (GFun f ss) C ts

goal (1 subgoal):
 1. \<And>x1a x2a C ts. \<lbrakk>\<And>x2aa C ts. \<lbrakk>x2aa \<in> set x2a; x2aa =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P x2aa C ts; GFun x1a x2a =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P (GFun x1a x2a) C ts
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>C = GMHole; ts = [GFun f ss]\<rbrakk> \<Longrightarrow> P (GFun f ss) C ts

goal (1 subgoal):
 1. \<And>x1a x2a C ts. \<lbrakk>\<And>x2aa C ts. \<lbrakk>x2aa \<in> set x2a; x2aa =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P x2aa C ts; GFun x1a x2a =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P (GFun x1a x2a) C ts
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>C = GMHole; ts = [GFun f ss]\<rbrakk> \<Longrightarrow> P (GFun f ss) C ts

goal (1 subgoal):
 1. \<And>x1a x2a C ts. \<lbrakk>\<And>x2aa C ts. \<lbrakk>x2aa \<in> set x2a; x2aa =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P x2aa C ts; GFun x1a x2a =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P (GFun x1a x2a) C ts
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
\<lbrakk>C = GMHole; ts = [GFun f ss]\<rbrakk> \<Longrightarrow> P (GFun f ss) C ts

goal (1 subgoal):
 1. \<And>x1a x2a C ts. \<lbrakk>\<And>x2aa C ts. \<lbrakk>x2aa \<in> set x2a; x2aa =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P x2aa C ts; GFun x1a x2a =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P (GFun x1a x2a) C ts
[PROOF STEP]
fix Cs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2a C ts. \<lbrakk>\<And>x2aa C ts. \<lbrakk>x2aa \<in> set x2a; x2aa =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P x2aa C ts; GFun x1a x2a =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P (GFun x1a x2a) C ts
[PROOF STEP]
assume C: "C = GMFun f Cs" and "sum_list (map num_gholes Cs) = length ts"
      and "length Cs = length ss"
      and "GFun f ss = fill_gholes (GMFun f Cs) ts"
[PROOF STATE]
proof (state)
this:
C = GMFun f Cs
sum_list (map num_gholes Cs) = length ts
length Cs = length ss
GFun f ss = fill_gholes (GMFun f Cs) ts

goal (1 subgoal):
 1. \<And>x1a x2a C ts. \<lbrakk>\<And>x2aa C ts. \<lbrakk>x2aa \<in> set x2a; x2aa =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P x2aa C ts; GFun x1a x2a =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P (GFun x1a x2a) C ts
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
C = GMFun f Cs
sum_list (map num_gholes Cs) = length ts
length Cs = length ss
GFun f ss = fill_gholes (GMFun f Cs) ts

goal (1 subgoal):
 1. \<And>x1a x2a C ts. \<lbrakk>\<And>x2aa C ts. \<lbrakk>x2aa \<in> set x2a; x2aa =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P x2aa C ts; GFun x1a x2a =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P (GFun x1a x2a) C ts
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C = GMFun f Cs
sum_list (map num_gholes Cs) = length ts
length Cs = length ss
GFun f ss = fill_gholes (GMFun f Cs) ts
[PROOF STEP]
have "\<forall>i < length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i)"
[PROOF STATE]
proof (prove)
using this:
C = GMFun f Cs
sum_list (map num_gholes Cs) = length ts
length Cs = length ss
GFun f ss = fill_gholes (GMFun f Cs) ts

goal (1 subgoal):
 1. \<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i)
[PROOF STEP]
by (auto simp del: fill_gholes.simps
         simp: partition_holes_fill_gholes_conv' length_partition_gholes_nth  intro!: eq_gfill.intros)
[PROOF STATE]
proof (state)
this:
\<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i)

goal (1 subgoal):
 1. \<And>x1a x2a C ts. \<lbrakk>\<And>x2aa C ts. \<lbrakk>x2aa \<in> set x2a; x2aa =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P x2aa C ts; GFun x1a x2a =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P (GFun x1a x2a) C ts
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i)

goal (1 subgoal):
 1. \<And>x1a x2a C ts. \<lbrakk>\<And>x2aa C ts. \<lbrakk>x2aa \<in> set x2a; x2aa =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P x2aa C ts; GFun x1a x2a =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P (GFun x1a x2a) C ts
[PROOF STEP]
have "\<forall>i < length ss. P (ss ! i) (Cs ! i) (partition_gholes ts Cs ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<length ss. P (ss ! i) (Cs ! i) (partition_gholes ts Cs ! i)
[PROOF STEP]
using GFun calculation(5) nth_mem
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2aa \<in> set ss; ?x2aa =\<^sub>G\<^sub>f (?C, ?ts)\<rbrakk> \<Longrightarrow> P ?x2aa ?C ?ts
GFun f ss =\<^sub>G\<^sub>f (C, ts)
\<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i)
?n < length ?xs \<Longrightarrow> ?xs ! ?n \<in> set ?xs

goal (1 subgoal):
 1. \<forall>i<length ss. P (ss ! i) (Cs ! i) (partition_gholes ts Cs ! i)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>i<length ss. P (ss ! i) (Cs ! i) (partition_gholes ts Cs ! i)

goal (1 subgoal):
 1. \<And>x1a x2a C ts. \<lbrakk>\<And>x2aa C ts. \<lbrakk>x2aa \<in> set x2a; x2aa =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P x2aa C ts; GFun x1a x2a =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P (GFun x1a x2a) C ts
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
C = GMFun f Cs
sum_list (map num_gholes Cs) = length ts
length Cs = length ss
GFun f ss = fill_gholes (GMFun f Cs) ts
\<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i)
\<forall>i<length ss. P (ss ! i) (Cs ! i) (partition_gholes ts Cs ! i)
[PROOF STEP]
have ?case
[PROOF STATE]
proof (prove)
using this:
C = GMFun f Cs
sum_list (map num_gholes Cs) = length ts
length Cs = length ss
GFun f ss = fill_gholes (GMFun f Cs) ts
\<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i)
\<forall>i<length ss. P (ss ! i) (Cs ! i) (partition_gholes ts Cs ! i)

goal (1 subgoal):
 1. P (GFun f ss) C ts
[PROOF STEP]
using assms(3)[of Cs ss ts f]
[PROOF STATE]
proof (prove)
using this:
C = GMFun f Cs
sum_list (map num_gholes Cs) = length ts
length Cs = length ss
GFun f ss = fill_gholes (GMFun f Cs) ts
\<forall>i<length ss. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i)
\<forall>i<length ss. P (ss ! i) (Cs ! i) (partition_gholes ts Cs ! 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> P (ss ! i) (Cs ! i) (partition_gholes ts Cs ! i)\<rbrakk> \<Longrightarrow> P (GFun f ss) (GMFun f Cs) ts

goal (1 subgoal):
 1. P (GFun f ss) C ts
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
P (GFun f ss) C ts

goal (1 subgoal):
 1. \<And>x1a x2a C ts. \<lbrakk>\<And>x2aa C ts. \<lbrakk>x2aa \<in> set x2a; x2aa =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P x2aa C ts; GFun x1a x2a =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P (GFun x1a x2a) C ts
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>C = GMFun f ?Cs2; sum_list (map num_gholes ?Cs2) = length ts; length ?Cs2 = length ss; GFun f ss = fill_gholes (GMFun f ?Cs2) ts\<rbrakk> \<Longrightarrow> P (GFun f ss) C ts

goal (1 subgoal):
 1. \<And>x1a x2a C ts. \<lbrakk>\<And>x2aa C ts. \<lbrakk>x2aa \<in> set x2a; x2aa =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P x2aa C ts; GFun x1a x2a =\<^sub>G\<^sub>f (C, ts)\<rbrakk> \<Longrightarrow> P (GFun x1a x2a) C ts
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>C = GMHole; ts = [GFun f ss]\<rbrakk> \<Longrightarrow> P (GFun f ss) C ts
\<lbrakk>C = GMFun f ?Cs2; sum_list (map num_gholes ?Cs2) = length ts; length ?Cs2 = length ss; GFun f ss = fill_gholes (GMFun f ?Cs2) ts\<rbrakk> \<Longrightarrow> P (GFun f ss) C ts
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>C = GMHole; ts = [GFun f ss]\<rbrakk> \<Longrightarrow> P (GFun f ss) C ts
\<lbrakk>C = GMFun f ?Cs2; sum_list (map num_gholes ?Cs2) = length ts; length ?Cs2 = length ss; GFun f ss = fill_gholes (GMFun f ?Cs2) ts\<rbrakk> \<Longrightarrow> P (GFun f ss) C ts

goal (1 subgoal):
 1. P (GFun f ss) C ts
[PROOF STEP]
using GFun
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>C = GMHole; ts = [GFun f ss]\<rbrakk> \<Longrightarrow> P (GFun f ss) C ts
\<lbrakk>C = GMFun f ?Cs2; sum_list (map num_gholes ?Cs2) = length ts; length ?Cs2 = length ss; GFun f ss = fill_gholes (GMFun f ?Cs2) ts\<rbrakk> \<Longrightarrow> P (GFun f ss) C ts
\<lbrakk>?x2aa \<in> set ss; ?x2aa =\<^sub>G\<^sub>f (?C, ?ts)\<rbrakk> \<Longrightarrow> P ?x2aa ?C ?ts
GFun f ss =\<^sub>G\<^sub>f (C, ts)

goal (1 subgoal):
 1. P (GFun f ss) C ts
[PROOF STEP]
by (elim eq_gfill.cases) (auto simp del: fill_gholes.simps,
      metis GFun.prems eqgf_GMFunE eqgf_GMHoleE gterm.inject num_gholes.elims)
[PROOF STATE]
proof (state)
this:
P (GFun f ss) C ts

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nempty_ground_mctxt_gmctxt [simp]:
  "C \<noteq> MHole \<Longrightarrow> ground_mctxt C \<Longrightarrow> gmctxt_of_mctxt C \<noteq> GMHole"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C \<noteq> MHole; ground_mctxt C\<rbrakk> \<Longrightarrow> gmctxt_of_mctxt C \<noteq> GMHole
[PROOF STEP]
by (induct C) auto


[STATEMENT]
lemma mctxt_of_gmctxt_fill_holes [simp]:
  assumes "num_gholes C = length ss"
  shows "gterm_of_term (fill_holes (mctxt_of_gmctxt C) (map term_of_gterm ss)) = fill_gholes C ss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gterm_of_term (fill_holes (mctxt_of_gmctxt C) (map term_of_gterm ss)) = fill_gholes C ss
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
num_gholes C = length ss

goal (1 subgoal):
 1. gterm_of_term (fill_holes (mctxt_of_gmctxt C) (map term_of_gterm ss)) = fill_gholes C ss
[PROOF STEP]
by (induct rule: fill_gholes_induct) auto


[STATEMENT]
lemma mctxt_of_gmctxt_terms_fill_holes:
  assumes "num_gholes C = length ss"
  shows "gterm_of_term (fill_holes (mctxt_of_gmctxt C) ss) = fill_gholes C (map gterm_of_term ss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gterm_of_term (fill_holes (mctxt_of_gmctxt C) ss) = fill_gholes C (map gterm_of_term ss)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
num_gholes C = length ss

goal (1 subgoal):
 1. gterm_of_term (fill_holes (mctxt_of_gmctxt C) ss) = fill_gholes C (map gterm_of_term ss)
[PROOF STEP]
by (induct rule: fill_gholes_induct) auto


[STATEMENT]
lemma ground_gmctxt_of_mctxt_gterm_fill_holes:
  assumes "num_holes C = length ss" and "ground_mctxt C"
  shows "term_of_gterm (fill_gholes (gmctxt_of_mctxt C) ss) = fill_holes C (map term_of_gterm ss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. term_of_gterm (fill_gholes (gmctxt_of_mctxt C) ss) = fill_holes C (map term_of_gterm ss)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
num_holes C = length ss
ground_mctxt C

goal (1 subgoal):
 1. term_of_gterm (fill_gholes (gmctxt_of_mctxt C) ss) = fill_holes C (map term_of_gterm ss)
[PROOF STEP]
by (induct rule: fill_holes_induct)
   (auto simp: comp_def, metis (no_types, lifting) map_eq_conv num_gholes_gmctxt_of_mctxt)


[STATEMENT]
lemma  ground_gmctxt_of_gterm_of_term:
  assumes "num_holes C = length ss" and "ground_mctxt C"
  shows "gterm_of_term (fill_holes C (map term_of_gterm ss)) = fill_gholes (gmctxt_of_mctxt C) ss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gterm_of_term (fill_holes C (map term_of_gterm ss)) = fill_gholes (gmctxt_of_mctxt C) ss
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
num_holes C = length ss
ground_mctxt C

goal (1 subgoal):
 1. gterm_of_term (fill_holes C (map term_of_gterm ss)) = fill_gholes (gmctxt_of_mctxt C) ss
[PROOF STEP]
by (induct rule: fill_holes_induct)
   (auto simp: comp_def, metis (no_types, lifting) map_eq_conv num_gholes_gmctxt_of_mctxt)


[STATEMENT]
lemma ground_gmctxt_of_mctxt_fill_holes [simp]:
  assumes "num_holes C = length ss" and "ground_mctxt C" "\<forall> s \<in> set ss. ground s"
  shows "term_of_gterm (fill_gholes (gmctxt_of_mctxt C) (map gterm_of_term ss)) = fill_holes C ss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. term_of_gterm (fill_gholes (gmctxt_of_mctxt C) (map gterm_of_term ss)) = fill_holes C ss
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
num_holes C = length ss
ground_mctxt C
\<forall>s\<in>set ss. ground s

goal (1 subgoal):
 1. term_of_gterm (fill_gholes (gmctxt_of_mctxt C) (map gterm_of_term ss)) = fill_holes C ss
[PROOF STEP]
by (induct rule: fill_holes_induct) auto


[STATEMENT]
lemma fill_holes_mctxt_of_gmctxt_to_fill_gholes:
  assumes "num_gholes C = length ss"
  shows "fill_holes (mctxt_of_gmctxt C) (map term_of_gterm ss) = term_of_gterm (fill_gholes C ss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_holes (mctxt_of_gmctxt C) (map term_of_gterm ss) = term_of_gterm (fill_gholes C ss)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
num_gholes C = length ss

goal (1 subgoal):
 1. fill_holes (mctxt_of_gmctxt C) (map term_of_gterm ss) = term_of_gterm (fill_gholes C ss)
[PROOF STEP]
by (metis ground_gmctxt_of_mctxt_gterm_fill_holes ground_mctxt_of_gmctxt mctxt_of_gmctxt_inv num_holes_mctxt_of_gmctxt)


[STATEMENT]
lemma fill_gholes_gmctxt_of_gterm [simp]:
  "fill_gholes (gmctxt_of_gterm s) [] = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_gholes (gmctxt_of_gterm s) [] = s
[PROOF STEP]
by (induct s) (auto simp add: map_nth_eq_conv)


[STATEMENT]
lemma fill_gholes_GMHole [simp]:
  "length ss = Suc 0 \<Longrightarrow> fill_gholes GMHole ss = ss ! 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ss = Suc 0 \<Longrightarrow> fill_gholes GMHole ss = ss ! 0
[PROOF STEP]
by (cases ss) auto


[STATEMENT]
lemma apply_gctxt_fill_gholes:
  "C\<langle>s\<rangle>\<^sub>G = fill_gholes (gmctxt_of_gctxt C) [s]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C\<langle>s\<rangle>\<^sub>G = fill_gholes (gmctxt_of_gctxt C) [s]
[PROOF STEP]
by (induct C) (auto simp: partition_holes_fill_gholes_conv'
    simp del: fill_gholes.simps intro!: nth_equalityI)


[STATEMENT]
lemma fill_gholes_apply_gctxt:
  "num_gholes C = Suc 0 \<Longrightarrow> fill_gholes C [s] = (gctxt_of_gmctxt C)\<langle>s\<rangle>\<^sub>G"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes C = Suc 0 \<Longrightarrow> fill_gholes C [s] = (gctxt_of_gmctxt C)\<langle>s\<rangle>\<^sub>G
[PROOF STEP]
by (simp add: apply_gctxt_fill_gholes gmctxt_of_gctxt_gctxt_of_gmctxt)


[STATEMENT]
lemma ctxt_of_gctxt_gctxt_of_gmctxt_apply:
  "num_gholes C = Suc 0 \<Longrightarrow> fill_holes (mctxt_of_gmctxt C) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt C))\<langle>s\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes C = Suc 0 \<Longrightarrow> fill_holes (mctxt_of_gmctxt C) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt C))\<langle>s\<rangle>
[PROOF STEP]
proof (induct C)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. num_gholes GMHole = Suc 0 \<Longrightarrow> fill_holes (mctxt_of_gmctxt GMHole) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt GMHole))\<langle>s\<rangle>
 2. \<And>x1 x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; num_gholes x2a = Suc 0\<rbrakk> \<Longrightarrow> fill_holes (mctxt_of_gmctxt x2a) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt x2a))\<langle>s\<rangle>; num_gholes (GMFun x1 x2) = Suc 0\<rbrakk> \<Longrightarrow> fill_holes (mctxt_of_gmctxt (GMFun x1 x2)) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt (GMFun x1 x2)))\<langle>s\<rangle>
[PROOF STEP]
case (GMFun f Cs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set Cs; num_gholes ?x2a = Suc 0\<rbrakk> \<Longrightarrow> fill_holes (mctxt_of_gmctxt ?x2a) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt ?x2a))\<langle>s\<rangle>
num_gholes (GMFun f Cs) = Suc 0

goal (2 subgoals):
 1. num_gholes GMHole = Suc 0 \<Longrightarrow> fill_holes (mctxt_of_gmctxt GMHole) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt GMHole))\<langle>s\<rangle>
 2. \<And>x1 x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; num_gholes x2a = Suc 0\<rbrakk> \<Longrightarrow> fill_holes (mctxt_of_gmctxt x2a) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt x2a))\<langle>s\<rangle>; num_gholes (GMFun x1 x2) = Suc 0\<rbrakk> \<Longrightarrow> fill_holes (mctxt_of_gmctxt (GMFun x1 x2)) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt (GMFun x1 x2)))\<langle>s\<rangle>
[PROOF STEP]
obtain i where split: "i < length Cs" "num_gholes (Cs ! i) = Suc 0"
    "\<forall> j < length Cs. j \<noteq> i \<longrightarrow> num_gholes (Cs ! j) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < length Cs; num_gholes (Cs ! i) = Suc 0; \<forall>j<length Cs. j \<noteq> i \<longrightarrow> num_gholes (Cs ! j) = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using GMFun(2)
[PROOF STATE]
proof (prove)
using this:
num_gholes (GMFun f Cs) = Suc 0

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < length Cs; num_gholes (Cs ! i) = Suc 0; \<forall>j<length Cs. j \<noteq> i \<longrightarrow> num_gholes (Cs ! j) = 0\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length Cs
num_gholes (Cs ! i) = Suc 0
\<forall>j<length Cs. j \<noteq> i \<longrightarrow> num_gholes (Cs ! j) = 0

goal (2 subgoals):
 1. num_gholes GMHole = Suc 0 \<Longrightarrow> fill_holes (mctxt_of_gmctxt GMHole) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt GMHole))\<langle>s\<rangle>
 2. \<And>x1 x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; num_gholes x2a = Suc 0\<rbrakk> \<Longrightarrow> fill_holes (mctxt_of_gmctxt x2a) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt x2a))\<langle>s\<rangle>; num_gholes (GMFun x1 x2) = Suc 0\<rbrakk> \<Longrightarrow> fill_holes (mctxt_of_gmctxt (GMFun x1 x2)) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt (GMFun x1 x2)))\<langle>s\<rangle>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length Cs
num_gholes (Cs ! i) = Suc 0
\<forall>j<length Cs. j \<noteq> i \<longrightarrow> num_gholes (Cs ! j) = 0
[PROOF STEP]
have [simp]: "sum_list (take i (map num_gholes Cs)) = 0"
[PROOF STATE]
proof (prove)
using this:
i < length Cs
num_gholes (Cs ! i) = Suc 0
\<forall>j<length Cs. j \<noteq> i \<longrightarrow> num_gholes (Cs ! j) = 0

goal (1 subgoal):
 1. sum_list (take i (map num_gholes Cs)) = 0
[PROOF STEP]
by (auto simp: sum_list_eq_0_iff dest: set_take_nth)
[PROOF STATE]
proof (state)
this:
sum_list (take i (map num_gholes Cs)) = 0

goal (2 subgoals):
 1. num_gholes GMHole = Suc 0 \<Longrightarrow> fill_holes (mctxt_of_gmctxt GMHole) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt GMHole))\<langle>s\<rangle>
 2. \<And>x1 x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; num_gholes x2a = Suc 0\<rbrakk> \<Longrightarrow> fill_holes (mctxt_of_gmctxt x2a) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt x2a))\<langle>s\<rangle>; num_gholes (GMFun x1 x2) = Suc 0\<rbrakk> \<Longrightarrow> fill_holes (mctxt_of_gmctxt (GMFun x1 x2)) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt (GMFun x1 x2)))\<langle>s\<rangle>
[PROOF STEP]
from split
[PROOF STATE]
proof (chain)
picking this:
i < length Cs
num_gholes (Cs ! i) = Suc 0
\<forall>j<length Cs. j \<noteq> i \<longrightarrow> num_gholes (Cs ! j) = 0
[PROOF STEP]
have [simp]: "j < length Cs \<Longrightarrow> j \<noteq> i \<Longrightarrow>
     fill_holes (mctxt_of_gmctxt (Cs ! j)) [] = term_of_mctxt (mctxt_of_gmctxt (Cs ! j))" for j
[PROOF STATE]
proof (prove)
using this:
i < length Cs
num_gholes (Cs ! i) = Suc 0
\<forall>j<length Cs. j \<noteq> i \<longrightarrow> num_gholes (Cs ! j) = 0

goal (1 subgoal):
 1. \<lbrakk>j < length Cs; j \<noteq> i\<rbrakk> \<Longrightarrow> fill_holes (mctxt_of_gmctxt (Cs ! j)) [] = term_of_mctxt (mctxt_of_gmctxt (Cs ! j))
[PROOF STEP]
by (intro fill_holes_term_of_mctxt) auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>?j1 < length Cs; ?j1 \<noteq> i\<rbrakk> \<Longrightarrow> fill_holes (mctxt_of_gmctxt (Cs ! ?j1)) [] = term_of_mctxt (mctxt_of_gmctxt (Cs ! ?j1))

goal (2 subgoals):
 1. num_gholes GMHole = Suc 0 \<Longrightarrow> fill_holes (mctxt_of_gmctxt GMHole) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt GMHole))\<langle>s\<rangle>
 2. \<And>x1 x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; num_gholes x2a = Suc 0\<rbrakk> \<Longrightarrow> fill_holes (mctxt_of_gmctxt x2a) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt x2a))\<langle>s\<rangle>; num_gholes (GMFun x1 x2) = Suc 0\<rbrakk> \<Longrightarrow> fill_holes (mctxt_of_gmctxt (GMFun x1 x2)) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt (GMFun x1 x2)))\<langle>s\<rangle>
[PROOF STEP]
from split
[PROOF STATE]
proof (chain)
picking this:
i < length Cs
num_gholes (Cs ! i) = Suc 0
\<forall>j<length Cs. j \<noteq> i \<longrightarrow> num_gholes (Cs ! j) = 0
[PROOF STEP]
have [simp]: "gctxt_of_gmctxt (GMFun f Cs) =
    GMore f (map gterm_of_gmctxt (take i Cs)) (gctxt_of_gmctxt (Cs ! i)) (map gterm_of_gmctxt (drop (Suc i) Cs))"
[PROOF STATE]
proof (prove)
using this:
i < length Cs
num_gholes (Cs ! i) = Suc 0
\<forall>j<length Cs. j \<noteq> i \<longrightarrow> num_gholes (Cs ! j) = 0

goal (1 subgoal):
 1. gctxt_of_gmctxt (GMFun f Cs) = GMore f (map gterm_of_gmctxt (take i Cs)) (gctxt_of_gmctxt (Cs ! i)) (map gterm_of_gmctxt (drop (Suc i) Cs))
[PROOF STEP]
using nth_length_takeWhile GMFun(2) sum_list_nthWhile_length
[PROOF STATE]
proof (prove)
using this:
i < length Cs
num_gholes (Cs ! i) = Suc 0
\<forall>j<length Cs. j \<noteq> i \<longrightarrow> num_gholes (Cs ! j) = 0
length (takeWhile ?P ?xs) < length ?xs \<Longrightarrow> \<not> ?P (?xs ! length (takeWhile ?P ?xs))
num_gholes (GMFun f Cs) = Suc 0
sum_list (map num_gholes ?Cs) = Suc 0 \<Longrightarrow> length (takeWhile (\<lambda>C. num_gholes C = 0) ?Cs) < length ?Cs

goal (1 subgoal):
 1. gctxt_of_gmctxt (GMFun f Cs) = GMore f (map gterm_of_gmctxt (take i Cs)) (gctxt_of_gmctxt (Cs ! i)) (map gterm_of_gmctxt (drop (Suc i) Cs))
[PROOF STEP]
by (auto simp: Let_def)
[PROOF STATE]
proof (state)
this:
gctxt_of_gmctxt (GMFun f Cs) = GMore f (map gterm_of_gmctxt (take i Cs)) (gctxt_of_gmctxt (Cs ! i)) (map gterm_of_gmctxt (drop (Suc i) Cs))

goal (2 subgoals):
 1. num_gholes GMHole = Suc 0 \<Longrightarrow> fill_holes (mctxt_of_gmctxt GMHole) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt GMHole))\<langle>s\<rangle>
 2. \<And>x1 x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; num_gholes x2a = Suc 0\<rbrakk> \<Longrightarrow> fill_holes (mctxt_of_gmctxt x2a) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt x2a))\<langle>s\<rangle>; num_gholes (GMFun x1 x2) = Suc 0\<rbrakk> \<Longrightarrow> fill_holes (mctxt_of_gmctxt (GMFun x1 x2)) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt (GMFun x1 x2)))\<langle>s\<rangle>
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_holes (mctxt_of_gmctxt (GMFun f Cs)) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt (GMFun f Cs)))\<langle>s\<rangle>
[PROOF STEP]
using GMFun(1)[OF nth_mem[OF split(1)] split(2)] split
[PROOF STATE]
proof (prove)
using this:
fill_holes (mctxt_of_gmctxt (Cs ! i)) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt (Cs ! i)))\<langle>s\<rangle>
i < length Cs
num_gholes (Cs ! i) = Suc 0
\<forall>j<length Cs. j \<noteq> i \<longrightarrow> num_gholes (Cs ! j) = 0

goal (1 subgoal):
 1. fill_holes (mctxt_of_gmctxt (GMFun f Cs)) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt (GMFun f Cs)))\<langle>s\<rangle>
[PROOF STEP]
by (auto simp: min_def nth_append_Cons partition_by_nth simp del: gctxt_of_gmctxt.simps intro!: nth_equalityI)
[PROOF STATE]
proof (state)
this:
fill_holes (mctxt_of_gmctxt (GMFun f Cs)) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt (GMFun f Cs)))\<langle>s\<rangle>

goal (1 subgoal):
 1. num_gholes GMHole = Suc 0 \<Longrightarrow> fill_holes (mctxt_of_gmctxt GMHole) [s] = (ctxt_of_gctxt (gctxt_of_gmctxt GMHole))\<langle>s\<rangle>
[PROOF STEP]
qed auto


[STATEMENT]
lemma fill_gholes_replicate [simp]:
  "n = length ss \<Longrightarrow> fill_gholes (GMFun f (replicate n GMHole)) ss = GFun f ss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = length ss \<Longrightarrow> fill_gholes (GMFun f (replicate n GMHole)) ss = GFun f ss
[PROOF STEP]
unfolding partition_holes_fill_gholes_conv'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = length ss \<Longrightarrow> GFun f (map2 fill_gholes (replicate n GMHole) (partition_gholes ss (replicate n GMHole))) = GFun f ss
[PROOF STEP]
by (induct ss arbitrary: n) auto


[STATEMENT]
lemma fill_gholes_gmctxt_replicate_MHole [simp]:
  "fill_gholes_gmctxt C (replicate (num_gholes C) GMHole) = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_gholes_gmctxt C (replicate (num_gholes C) GMHole) = C
[PROOF STEP]
proof (induct C)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fill_gholes_gmctxt GMHole (replicate (num_gholes GMHole) GMHole) = GMHole
 2. \<And>x1 x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> fill_gholes_gmctxt x2a (replicate (num_gholes x2a) GMHole) = x2a) \<Longrightarrow> fill_gholes_gmctxt (GMFun x1 x2) (replicate (num_gholes (GMFun x1 x2)) GMHole) = GMFun x1 x2
[PROOF STEP]
case (GMFun f Cs)
[PROOF STATE]
proof (state)
this:
?x2a \<in> set Cs \<Longrightarrow> fill_gholes_gmctxt ?x2a (replicate (num_gholes ?x2a) GMHole) = ?x2a

goal (2 subgoals):
 1. fill_gholes_gmctxt GMHole (replicate (num_gholes GMHole) GMHole) = GMHole
 2. \<And>x1 x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> fill_gholes_gmctxt x2a (replicate (num_gholes x2a) GMHole) = x2a) \<Longrightarrow> fill_gholes_gmctxt (GMFun x1 x2) (replicate (num_gholes (GMFun x1 x2)) GMHole) = GMFun x1 x2
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
?x2a \<in> set Cs \<Longrightarrow> fill_gholes_gmctxt ?x2a (replicate (num_gholes ?x2a) GMHole) = ?x2a

goal (2 subgoals):
 1. fill_gholes_gmctxt GMHole (replicate (num_gholes GMHole) GMHole) = GMHole
 2. \<And>x1 x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> fill_gholes_gmctxt x2a (replicate (num_gholes x2a) GMHole) = x2a) \<Longrightarrow> fill_gholes_gmctxt (GMFun x1 x2) (replicate (num_gholes (GMFun x1 x2)) GMHole) = GMFun x1 x2
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fill_gholes_gmctxt GMHole (replicate (num_gholes GMHole) GMHole) = GMHole
 2. \<And>x1 x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> fill_gholes_gmctxt x2a (replicate (num_gholes x2a) GMHole) = x2a) \<Longrightarrow> fill_gholes_gmctxt (GMFun x1 x2) (replicate (num_gholes (GMFun x1 x2)) GMHole) = GMFun x1 x2
[PROOF STEP]
assume "i < length Cs"
[PROOF STATE]
proof (state)
this:
i < length Cs

goal (2 subgoals):
 1. fill_gholes_gmctxt GMHole (replicate (num_gholes GMHole) GMHole) = GMHole
 2. \<And>x1 x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> fill_gholes_gmctxt x2a (replicate (num_gholes x2a) GMHole) = x2a) \<Longrightarrow> fill_gholes_gmctxt (GMFun x1 x2) (replicate (num_gholes (GMFun x1 x2)) GMHole) = GMFun x1 x2
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length Cs
[PROOF STEP]
have "partition_gholes (replicate (sum_list (map num_gholes Cs)) GMHole) Cs ! i =
        replicate (num_gholes (Cs ! i)) GMHole"
[PROOF STATE]
proof (prove)
using this:
i < length Cs

goal (1 subgoal):
 1. partition_gholes (replicate (sum_list (map num_gholes Cs)) GMHole) Cs ! i = replicate (num_gholes (Cs ! i)) GMHole
[PROOF STEP]
using partition_by_nth_nth[of "map num_gholes Cs" "replicate (sum_list (map num_gholes Cs)) MHole"]
[PROOF STATE]
proof (prove)
using this:
i < length Cs
\<lbrakk>sum_list (map num_gholes Cs) = length (replicate (sum_list (map num_gholes Cs)) MHole); ?i < length (map num_gholes Cs); ?j < map num_gholes Cs ! ?i\<rbrakk> \<Longrightarrow> partition_gholes (replicate (sum_list (map num_gholes Cs)) MHole) Cs ! ?i ! ?j = replicate (sum_list (map num_gholes Cs)) MHole ! partition_by_idx (length (replicate (sum_list (map num_gholes Cs)) MHole)) (map num_gholes Cs) ?i ?j
\<lbrakk>sum_list (map num_gholes Cs) = length (replicate (sum_list (map num_gholes Cs)) MHole); ?i < length (map num_gholes Cs); ?j < map num_gholes Cs ! ?i\<rbrakk> \<Longrightarrow> partition_by_idx (length (replicate (sum_list (map num_gholes Cs)) MHole)) (map num_gholes Cs) ?i ?j < length (replicate (sum_list (map num_gholes Cs)) MHole)

goal (1 subgoal):
 1. partition_gholes (replicate (sum_list (map num_gholes Cs)) GMHole) Cs ! i = replicate (num_gholes (Cs ! i)) GMHole
[PROOF STEP]
by (auto simp: length_partition_by_nth partition_by_nth_nth intro!: nth_equalityI)
[PROOF STATE]
proof (state)
this:
partition_gholes (replicate (sum_list (map num_gholes Cs)) GMHole) Cs ! i = replicate (num_gholes (Cs ! i)) GMHole

goal (2 subgoals):
 1. fill_gholes_gmctxt GMHole (replicate (num_gholes GMHole) GMHole) = GMHole
 2. \<And>x1 x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> fill_gholes_gmctxt x2a (replicate (num_gholes x2a) GMHole) = x2a) \<Longrightarrow> fill_gholes_gmctxt (GMFun x1 x2) (replicate (num_gholes (GMFun x1 x2)) GMHole) = GMFun x1 x2
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i4 < length Cs \<Longrightarrow> partition_gholes (replicate (sum_list (map num_gholes Cs)) GMHole) Cs ! ?i4 = replicate (num_gholes (Cs ! ?i4)) GMHole

goal (2 subgoals):
 1. fill_gholes_gmctxt GMHole (replicate (num_gholes GMHole) GMHole) = GMHole
 2. \<And>x1 x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> fill_gholes_gmctxt x2a (replicate (num_gholes x2a) GMHole) = x2a) \<Longrightarrow> fill_gholes_gmctxt (GMFun x1 x2) (replicate (num_gholes (GMFun x1 x2)) GMHole) = GMFun x1 x2
[PROOF STEP]
note * = this
[PROOF STATE]
proof (state)
this:
?i4 < length Cs \<Longrightarrow> partition_gholes (replicate (sum_list (map num_gholes Cs)) GMHole) Cs ! ?i4 = replicate (num_gholes (Cs ! ?i4)) GMHole

goal (2 subgoals):
 1. fill_gholes_gmctxt GMHole (replicate (num_gholes GMHole) GMHole) = GMHole
 2. \<And>x1 x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> fill_gholes_gmctxt x2a (replicate (num_gholes x2a) GMHole) = x2a) \<Longrightarrow> fill_gholes_gmctxt (GMFun x1 x2) (replicate (num_gholes (GMFun x1 x2)) GMHole) = GMFun x1 x2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_gholes_gmctxt (GMFun f Cs) (replicate (num_gholes (GMFun f Cs)) GMHole) = GMFun f Cs
[PROOF STEP]
using GMFun[OF nth_mem]
[PROOF STATE]
proof (prove)
using this:
?n1 < length Cs \<Longrightarrow> fill_gholes_gmctxt (Cs ! ?n1) (replicate (num_gholes (Cs ! ?n1)) GMHole) = Cs ! ?n1

goal (1 subgoal):
 1. fill_gholes_gmctxt (GMFun f Cs) (replicate (num_gholes (GMFun f Cs)) GMHole) = GMFun f Cs
[PROOF STEP]
by (auto simp: * intro!: nth_equalityI)
[PROOF STATE]
proof (state)
this:
fill_gholes_gmctxt (GMFun f Cs) (replicate (num_gholes (GMFun f Cs)) GMHole) = GMFun f Cs

goal (1 subgoal):
 1. fill_gholes_gmctxt GMHole (replicate (num_gholes GMHole) GMHole) = GMHole
[PROOF STEP]
qed auto


[STATEMENT]
lemma fill_gholes_gmctxt_GMFun_replicate_length [simp]:
  "fill_gholes_gmctxt (GMFun f (replicate (length Cs) GMHole)) Cs = GMFun f Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_gholes_gmctxt (GMFun f (replicate (length Cs) GMHole)) Cs = GMFun f Cs
[PROOF STEP]
unfolding partition_holes_fill_gholes_gmctxt_conv'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. GMFun f (map2 fill_gholes_gmctxt (replicate (length Cs) GMHole) (partition_gholes Cs (replicate (length Cs) GMHole))) = GMFun f Cs
[PROOF STEP]
by (induct Cs) simp_all


[STATEMENT]
lemma fill_gholes_gmctxt_MFun:
  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>
      fill_gholes_gmctxt (Cs ! i) (ss ! i) = ts ! i"
  shows "fill_gholes_gmctxt (GMFun f Cs) (concat ss) = GMFun f ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_gholes_gmctxt (GMFun f Cs) (concat ss) = GMFun f ts
[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> fill_gholes_gmctxt (Cs ! ?i) (ss ! ?i) = ts ! ?i

goal (1 subgoal):
 1. fill_gholes_gmctxt (GMFun f Cs) (concat ss) = GMFun f ts
[PROOF STEP]
unfolding fill_gholes_gmctxt.simps gmctxt.simps
[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> fill_gholes_gmctxt (Cs ! ?i) (ss ! ?i) = ts ! ?i

goal (1 subgoal):
 1. f = f \<and> map (\<lambda>i. fill_gholes_gmctxt (Cs ! i) (partition_gholes (concat ss) Cs ! i)) [0..<length Cs] = ts
[PROOF STEP]
by (auto intro!: nth_equalityI)
    (metis length_map map_nth_eq_conv partition_by_concat_id)


[STATEMENT]
lemma fill_gholes_gmctxt_nHole [simp]:
  "C \<noteq> GMHole \<Longrightarrow> num_gholes C = length Ds \<Longrightarrow> fill_gholes_gmctxt C Ds \<noteq> GMHole"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C \<noteq> GMHole; num_gholes C = length Ds\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt C Ds \<noteq> GMHole
[PROOF STEP]
using fill_gholes_gmctxt.elims
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>fill_gholes_gmctxt ?x ?xa = ?y; \<lbrakk>?x = GMHole; ?xa = []; ?y = GMHole\<rbrakk> \<Longrightarrow> ?P; \<And>t. \<lbrakk>?x = GMHole; ?xa = [t]; ?y = t\<rbrakk> \<Longrightarrow> ?P; \<And>f cs ts. \<lbrakk>?x = GMFun f cs; ?xa = ts; ?y = GMFun f (map (\<lambda>i. fill_gholes_gmctxt (cs ! i) (partition_gholes ts cs ! i)) [0..<length cs])\<rbrakk> \<Longrightarrow> ?P; \<And>v vb vc. \<lbrakk>?x = GMHole; ?xa = v # vb # vc; ?y = undefined\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<lbrakk>C \<noteq> GMHole; num_gholes C = length Ds\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt C Ds \<noteq> GMHole
[PROOF STEP]
by blast


[STATEMENT]
lemma num_gholes_fill_gholes_gmctxt [simp]:
  assumes "num_gholes C = length Ds"
  shows "num_gholes (fill_gholes_gmctxt C Ds) = sum_list (map num_gholes Ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes (fill_gholes_gmctxt C Ds) = sum_list (map num_gholes Ds)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
num_gholes C = length Ds

goal (1 subgoal):
 1. num_gholes (fill_gholes_gmctxt C Ds) = sum_list (map num_gholes Ds)
[PROOF STEP]
proof (induct C arbitrary: Ds)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Ds. num_gholes GMHole = length Ds \<Longrightarrow> num_gholes (fill_gholes_gmctxt GMHole Ds) = sum_list (map num_gholes Ds)
 2. \<And>x1 x2 Ds. \<lbrakk>\<And>x2a Ds. \<lbrakk>x2a \<in> set x2; num_gholes x2a = length Ds\<rbrakk> \<Longrightarrow> num_gholes (fill_gholes_gmctxt x2a Ds) = sum_list (map num_gholes Ds); num_gholes (GMFun x1 x2) = length Ds\<rbrakk> \<Longrightarrow> num_gholes (fill_gholes_gmctxt (GMFun x1 x2) Ds) = sum_list (map num_gholes 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> num_gholes (fill_gholes_gmctxt GMHole Ds) = sum_list (map num_gholes Ds)
 2. \<And>x1 x2 Ds. \<lbrakk>\<And>x2a Ds. \<lbrakk>x2a \<in> set x2; num_gholes x2a = length Ds\<rbrakk> \<Longrightarrow> num_gholes (fill_gholes_gmctxt x2a Ds) = sum_list (map num_gholes Ds); num_gholes (GMFun x1 x2) = length Ds\<rbrakk> \<Longrightarrow> num_gholes (fill_gholes_gmctxt (GMFun x1 x2) Ds) = sum_list (map num_gholes 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. num_gholes (fill_gholes_gmctxt GMHole Ds) = sum_list (map num_gholes Ds)
[PROOF STEP]
by (cases Ds) simp_all
[PROOF STATE]
proof (state)
this:
num_gholes (fill_gholes_gmctxt GMHole Ds) = sum_list (map num_gholes 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> num_gholes (fill_gholes_gmctxt x2a Ds) = sum_list (map num_gholes Ds); num_gholes (GMFun x1 x2) = length Ds\<rbrakk> \<Longrightarrow> num_gholes (fill_gholes_gmctxt (GMFun x1 x2) Ds) = sum_list (map num_gholes 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> num_gholes (fill_gholes_gmctxt x2a Ds) = sum_list (map num_gholes Ds); num_gholes (GMFun x1 x2) = length Ds\<rbrakk> \<Longrightarrow> num_gholes (fill_gholes_gmctxt (GMFun x1 x2) Ds) = sum_list (map num_gholes Ds)
[PROOF STEP]
case (GMFun f Cs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set Cs; num_gholes ?x2a = length ?Ds\<rbrakk> \<Longrightarrow> num_gholes (fill_gholes_gmctxt ?x2a ?Ds) = sum_list (map num_gholes ?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> num_gholes (fill_gholes_gmctxt x2a Ds) = sum_list (map num_gholes Ds); num_gholes (GMFun x1 x2) = length Ds\<rbrakk> \<Longrightarrow> num_gholes (fill_gholes_gmctxt (GMFun x1 x2) Ds) = sum_list (map num_gholes Ds)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x2a \<in> set Cs; num_gholes ?x2a = length ?Ds\<rbrakk> \<Longrightarrow> num_gholes (fill_gholes_gmctxt ?x2a ?Ds) = sum_list (map num_gholes ?Ds)
num_gholes (GMFun f Cs) = length Ds
[PROOF STEP]
have *: "map (num_gholes \<circ> (\<lambda>i. fill_gholes_gmctxt (Cs ! i) (partition_gholes Ds Cs ! i))) [0..<length Cs] =
    map (\<lambda>i. sum_list (map num_gholes (partition_gholes Ds Cs ! i))) [0 ..< length Cs]"
    and "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> num_gholes (fill_gholes_gmctxt ?x2a ?Ds) = sum_list (map num_gholes ?Ds)
num_gholes (GMFun f Cs) = length Ds

goal (1 subgoal):
 1. map (num_gholes \<circ> (\<lambda>i. fill_gholes_gmctxt (Cs ! i) (partition_gholes Ds Cs ! i))) [0..<length Cs] = map (\<lambda>i. sum_list (map num_gholes (partition_gholes Ds Cs ! i))) [0..<length Cs] &&& sum_list (map num_gholes Cs) = length Ds
[PROOF STEP]
by (auto simp add: length_partition_by_nth)
[PROOF STATE]
proof (state)
this:
map (num_gholes \<circ> (\<lambda>i. fill_gholes_gmctxt (Cs ! i) (partition_gholes Ds Cs ! i))) [0..<length Cs] = map (\<lambda>i. sum_list (map num_gholes (partition_gholes Ds Cs ! i))) [0..<length Cs]
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> num_gholes (fill_gholes_gmctxt x2a Ds) = sum_list (map num_gholes Ds); num_gholes (GMFun x1 x2) = length Ds\<rbrakk> \<Longrightarrow> num_gholes (fill_gholes_gmctxt (GMFun x1 x2) Ds) = sum_list (map num_gholes Ds)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map (num_gholes \<circ> (\<lambda>i. fill_gholes_gmctxt (Cs ! i) (partition_gholes Ds Cs ! i))) [0..<length Cs] = map (\<lambda>i. sum_list (map num_gholes (partition_gholes Ds Cs ! i))) [0..<length Cs]
sum_list (map num_gholes Cs) = length Ds
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
map (num_gholes \<circ> (\<lambda>i. fill_gholes_gmctxt (Cs ! i) (partition_gholes Ds Cs ! i))) [0..<length Cs] = map (\<lambda>i. sum_list (map num_gholes (partition_gholes Ds Cs ! i))) [0..<length Cs]
sum_list (map num_gholes Cs) = length Ds

goal (1 subgoal):
 1. num_gholes (fill_gholes_gmctxt (GMFun f Cs) Ds) = sum_list (map num_gholes Ds)
[PROOF STEP]
using map_upt_len_conv [of "\<lambda>x. sum_list (map num_gholes x)" "partition_gholes Ds Cs"]
[PROOF STATE]
proof (prove)
using this:
map (num_gholes \<circ> (\<lambda>i. fill_gholes_gmctxt (Cs ! i) (partition_gholes Ds Cs ! i))) [0..<length Cs] = map (\<lambda>i. sum_list (map num_gholes (partition_gholes Ds Cs ! i))) [0..<length Cs]
sum_list (map num_gholes Cs) = length Ds
map (\<lambda>i. sum_list (map num_gholes (partition_gholes Ds Cs ! i))) [0..<length (partition_gholes Ds Cs)] = map (\<lambda>x. sum_list (map num_gholes x)) (partition_gholes Ds Cs)

goal (1 subgoal):
 1. num_gholes (fill_gholes_gmctxt (GMFun f Cs) Ds) = sum_list (map num_gholes Ds)
[PROOF STEP]
unfolding partition_holes_fill_holes_mctxt_conv
[PROOF STATE]
proof (prove)
using this:
map (num_gholes \<circ> (\<lambda>i. fill_gholes_gmctxt (Cs ! i) (partition_gholes Ds Cs ! i))) [0..<length Cs] = map (\<lambda>i. sum_list (map num_gholes (partition_gholes Ds Cs ! i))) [0..<length Cs]
sum_list (map num_gholes Cs) = length Ds
map (\<lambda>i. sum_list (map num_gholes (partition_gholes Ds Cs ! i))) [0..<length (partition_gholes Ds Cs)] = map (\<lambda>x. sum_list (map num_gholes x)) (partition_gholes Ds Cs)

goal (1 subgoal):
 1. num_gholes (fill_gholes_gmctxt (GMFun f Cs) Ds) = sum_list (map num_gholes Ds)
[PROOF STEP]
by (simp add: *)
[PROOF STATE]
proof (state)
this:
num_gholes (fill_gholes_gmctxt (GMFun f Cs) Ds) = sum_list (map num_gholes Ds)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma num_gholes_greater0_fill_gholes_gmctxt [intro!]:
  assumes "num_gholes C = length Ds"
    and "\<exists> D \<in> set Ds. 0 < num_gholes D"
  shows "0 < sum_list (map num_gholes Ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < sum_list (map num_gholes Ds)
[PROOF STEP]
using assms gr_zeroI
[PROOF STATE]
proof (prove)
using this:
num_gholes C = length Ds
\<exists>D\<in>set Ds. 0 < num_gholes D
(?n = (0::?'a) \<Longrightarrow> False) \<Longrightarrow> (0::?'a) < ?n

goal (1 subgoal):
 1. 0 < sum_list (map num_gholes Ds)
[PROOF STEP]
by force