[STATEMENT]
lemma prefix_and_fewer_gholes_implies_equal_gmctxt:
  "C \<le> D \<Longrightarrow> ghole_poss C \<subseteq> ghole_poss D \<Longrightarrow> C = D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C \<le> D; ghole_poss C \<subseteq> ghole_poss D\<rbrakk> \<Longrightarrow> C = D
[PROOF STEP]
proof (induct C D rule: less_eq_gmctxt_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>u. ghole_poss GMHole \<subseteq> ghole_poss u \<Longrightarrow> GMHole = u
 2. \<And>cs ds f. \<lbrakk>length cs = length ds; \<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i; \<And>i. \<lbrakk>i < length cs; ghole_poss (cs ! i) \<subseteq> ghole_poss (ds ! i)\<rbrakk> \<Longrightarrow> cs ! i = ds ! i; ghole_poss (GMFun f cs) \<subseteq> ghole_poss (GMFun f ds)\<rbrakk> \<Longrightarrow> GMFun f cs = GMFun f ds
[PROOF STEP]
case (1 D)
[PROOF STATE]
proof (state)
this:
ghole_poss GMHole \<subseteq> ghole_poss D

goal (2 subgoals):
 1. \<And>u. ghole_poss GMHole \<subseteq> ghole_poss u \<Longrightarrow> GMHole = u
 2. \<And>cs ds f. \<lbrakk>length cs = length ds; \<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i; \<And>i. \<lbrakk>i < length cs; ghole_poss (cs ! i) \<subseteq> ghole_poss (ds ! i)\<rbrakk> \<Longrightarrow> cs ! i = ds ! i; ghole_poss (GMFun f cs) \<subseteq> ghole_poss (GMFun f ds)\<rbrakk> \<Longrightarrow> GMFun f cs = GMFun f ds
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ghole_poss GMHole \<subseteq> ghole_poss D
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ghole_poss GMHole \<subseteq> ghole_poss D

goal (1 subgoal):
 1. GMHole = D
[PROOF STEP]
by (cases D) auto
[PROOF STATE]
proof (state)
this:
GMHole = D

goal (1 subgoal):
 1. \<And>cs ds f. \<lbrakk>length cs = length ds; \<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i; \<And>i. \<lbrakk>i < length cs; ghole_poss (cs ! i) \<subseteq> ghole_poss (ds ! i)\<rbrakk> \<Longrightarrow> cs ! i = ds ! i; ghole_poss (GMFun f cs) \<subseteq> ghole_poss (GMFun f ds)\<rbrakk> \<Longrightarrow> GMFun f cs = GMFun f ds
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cs ds f. \<lbrakk>length cs = length ds; \<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i; \<And>i. \<lbrakk>i < length cs; ghole_poss (cs ! i) \<subseteq> ghole_poss (ds ! i)\<rbrakk> \<Longrightarrow> cs ! i = ds ! i; ghole_poss (GMFun f cs) \<subseteq> ghole_poss (GMFun f ds)\<rbrakk> \<Longrightarrow> GMFun f cs = GMFun f ds
[PROOF STEP]
case (2 Cs Ds f)
[PROOF STATE]
proof (state)
this:
length Cs = length Ds
?i < length Cs \<Longrightarrow> Cs ! ?i \<le> Ds ! ?i
\<lbrakk>?i < length Cs; ghole_poss (Cs ! ?i) \<subseteq> ghole_poss (Ds ! ?i)\<rbrakk> \<Longrightarrow> Cs ! ?i = Ds ! ?i
ghole_poss (GMFun f Cs) \<subseteq> ghole_poss (GMFun f Ds)

goal (1 subgoal):
 1. \<And>cs ds f. \<lbrakk>length cs = length ds; \<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i; \<And>i. \<lbrakk>i < length cs; ghole_poss (cs ! i) \<subseteq> ghole_poss (ds ! i)\<rbrakk> \<Longrightarrow> cs ! i = ds ! i; ghole_poss (GMFun f cs) \<subseteq> ghole_poss (GMFun f ds)\<rbrakk> \<Longrightarrow> GMFun f cs = GMFun f ds
[PROOF STEP]
have "i < length Ds \<Longrightarrow> ghole_poss (Cs ! i) \<subseteq> ghole_poss (Ds ! i)" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length Ds \<Longrightarrow> ghole_poss (Cs ! i) \<subseteq> ghole_poss (Ds ! i)
[PROOF STEP]
using 2(1,4)
[PROOF STATE]
proof (prove)
using this:
length Cs = length Ds
ghole_poss (GMFun f Cs) \<subseteq> ghole_poss (GMFun f Ds)

goal (1 subgoal):
 1. i < length Ds \<Longrightarrow> ghole_poss (Cs ! i) \<subseteq> ghole_poss (Ds ! i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i < length Ds \<Longrightarrow> ghole_poss (Cs ! ?i) \<subseteq> ghole_poss (Ds ! ?i)

goal (1 subgoal):
 1. \<And>cs ds f. \<lbrakk>length cs = length ds; \<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i; \<And>i. \<lbrakk>i < length cs; ghole_poss (cs ! i) \<subseteq> ghole_poss (ds ! i)\<rbrakk> \<Longrightarrow> cs ! i = ds ! i; ghole_poss (GMFun f cs) \<subseteq> ghole_poss (GMFun f ds)\<rbrakk> \<Longrightarrow> GMFun f cs = GMFun f ds
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?i < length Ds \<Longrightarrow> ghole_poss (Cs ! ?i) \<subseteq> ghole_poss (Ds ! ?i)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?i < length Ds \<Longrightarrow> ghole_poss (Cs ! ?i) \<subseteq> ghole_poss (Ds ! ?i)

goal (1 subgoal):
 1. GMFun f Cs = GMFun f Ds
[PROOF STEP]
using 2
[PROOF STATE]
proof (prove)
using this:
?i < length Ds \<Longrightarrow> ghole_poss (Cs ! ?i) \<subseteq> ghole_poss (Ds ! ?i)
length Cs = length Ds
?i < length Cs \<Longrightarrow> Cs ! ?i \<le> Ds ! ?i
\<lbrakk>?i < length Cs; ghole_poss (Cs ! ?i) \<subseteq> ghole_poss (Ds ! ?i)\<rbrakk> \<Longrightarrow> Cs ! ?i = Ds ! ?i
ghole_poss (GMFun f Cs) \<subseteq> ghole_poss (GMFun f Ds)

goal (1 subgoal):
 1. GMFun f Cs = GMFun f Ds
[PROOF STEP]
by (auto intro!: nth_equalityI)
[PROOF STATE]
proof (state)
this:
GMFun f Cs = GMFun f Ds

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma set_sup_gmctxt_args_split:
  "length Cs = length Ds \<Longrightarrow> set (sup_gmctxt_args (GMFun f Cs) (GMFun f Ds)) =
     (\<Union> i \<in> {0..< length Ds}. set (sup_gmctxt_args (Cs ! i) (Ds ! i)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length Cs = length Ds \<Longrightarrow> set (sup_gmctxt_args (GMFun f Cs) (GMFun f Ds)) = (\<Union>i\<in>{0..<length Ds}. set (sup_gmctxt_args (Cs ! i) (Ds ! i)))
[PROOF STEP]
by (auto simp: atLeast0LessThan in_set_zip)
    (metis length_map map_fst_zip nth_mem nth_zip)


[STATEMENT]
lemma gmctxt_closing_trans:
  "gmctxt_closing C D \<Longrightarrow> gmctxt_closing D E \<Longrightarrow> gmctxt_closing C E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>gmctxt_closing C D; gmctxt_closing D E\<rbrakk> \<Longrightarrow> gmctxt_closing C E
[PROOF STEP]
unfolding gmctxt_closing_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>less_eq_gmctxt C D \<and> ghole_poss D \<subseteq> ghole_poss C; less_eq_gmctxt D E \<and> ghole_poss E \<subseteq> ghole_poss D\<rbrakk> \<Longrightarrow> less_eq_gmctxt C E \<and> ghole_poss E \<subseteq> ghole_poss C
[PROOF STEP]
using less_eq_gmctxt_prime
[PROOF STATE]
proof (prove)
using this:
(?C \<le> ?D) = less_eq_gmctxt ?C ?D

goal (1 subgoal):
 1. \<lbrakk>less_eq_gmctxt C D \<and> ghole_poss D \<subseteq> ghole_poss C; less_eq_gmctxt D E \<and> ghole_poss E \<subseteq> ghole_poss D\<rbrakk> \<Longrightarrow> less_eq_gmctxt C E \<and> ghole_poss E \<subseteq> ghole_poss C
[PROOF STEP]
by (metis (full_types) order_trans)


[STATEMENT]
lemma gmctxt_closing_sup_args_ghole_or_gterm:
  assumes "gmctxt_closing C D"
  shows "\<forall> E \<in> set (sup_gmctxt_args C D). E = GMHole \<or> num_gholes E = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>E\<in>set (sup_gmctxt_args C D). E = GMHole \<or> num_gholes E = 0
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
gmctxt_closing C D

goal (1 subgoal):
 1. \<forall>E\<in>set (sup_gmctxt_args C D). E = GMHole \<or> num_gholes E = 0
[PROOF STEP]
unfolding gmctxt_closing_def
[PROOF STATE]
proof (prove)
using this:
less_eq_gmctxt C D \<and> ghole_poss D \<subseteq> ghole_poss C

goal (1 subgoal):
 1. \<forall>E\<in>set (sup_gmctxt_args C D). E = GMHole \<or> num_gholes E = 0
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. less_eq_gmctxt C D \<and> ghole_poss D \<subseteq> ghole_poss C \<Longrightarrow> \<forall>E\<in>set (sup_gmctxt_args C D). E = GMHole \<or> num_gholes E = 0
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
gmctxt_closing C D
[PROOF STEP]
have "C \<le> D" "ghole_poss D \<subseteq> ghole_poss C"
[PROOF STATE]
proof (prove)
using this:
gmctxt_closing C D

goal (1 subgoal):
 1. C \<le> D &&& ghole_poss D \<subseteq> ghole_poss C
[PROOF STEP]
unfolding gmctxt_closing_def
[PROOF STATE]
proof (prove)
using this:
less_eq_gmctxt C D \<and> ghole_poss D \<subseteq> ghole_poss C

goal (1 subgoal):
 1. C \<le> D &&& ghole_poss D \<subseteq> ghole_poss C
[PROOF STEP]
by (auto simp: less_eq_gmctxt_prime)
[PROOF STATE]
proof (state)
this:
C \<le> D
ghole_poss D \<subseteq> ghole_poss C

goal (1 subgoal):
 1. less_eq_gmctxt C D \<and> ghole_poss D \<subseteq> ghole_poss C \<Longrightarrow> \<forall>E\<in>set (sup_gmctxt_args C D). E = GMHole \<or> num_gholes E = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<le> D
ghole_poss D \<subseteq> ghole_poss C
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
C \<le> D
ghole_poss D \<subseteq> ghole_poss C

goal (1 subgoal):
 1. \<forall>E\<in>set (sup_gmctxt_args C D). E = GMHole \<or> num_gholes E = 0
[PROOF STEP]
proof (induct rule: less_eq_gmctxt_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>u. ghole_poss u \<subseteq> ghole_poss GMHole \<Longrightarrow> \<forall>E\<in>set (sup_gmctxt_args GMHole u). E = GMHole \<or> num_gholes E = 0
 2. \<And>cs ds f. \<lbrakk>length cs = length ds; \<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i; \<And>i. \<lbrakk>i < length cs; ghole_poss (ds ! i) \<subseteq> ghole_poss (cs ! i)\<rbrakk> \<Longrightarrow> \<forall>E\<in>set (sup_gmctxt_args (cs ! i) (ds ! i)). E = GMHole \<or> num_gholes E = 0; ghole_poss (GMFun f ds) \<subseteq> ghole_poss (GMFun f cs)\<rbrakk> \<Longrightarrow> \<forall>E\<in>set (sup_gmctxt_args (GMFun f cs) (GMFun f ds)). E = GMHole \<or> num_gholes E = 0
[PROOF STEP]
case (1 D)
[PROOF STATE]
proof (state)
this:
ghole_poss D \<subseteq> ghole_poss GMHole

goal (2 subgoals):
 1. \<And>u. ghole_poss u \<subseteq> ghole_poss GMHole \<Longrightarrow> \<forall>E\<in>set (sup_gmctxt_args GMHole u). E = GMHole \<or> num_gholes E = 0
 2. \<And>cs ds f. \<lbrakk>length cs = length ds; \<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i; \<And>i. \<lbrakk>i < length cs; ghole_poss (ds ! i) \<subseteq> ghole_poss (cs ! i)\<rbrakk> \<Longrightarrow> \<forall>E\<in>set (sup_gmctxt_args (cs ! i) (ds ! i)). E = GMHole \<or> num_gholes E = 0; ghole_poss (GMFun f ds) \<subseteq> ghole_poss (GMFun f cs)\<rbrakk> \<Longrightarrow> \<forall>E\<in>set (sup_gmctxt_args (GMFun f cs) (GMFun f ds)). E = GMHole \<or> num_gholes E = 0
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ghole_poss D \<subseteq> ghole_poss GMHole
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ghole_poss D \<subseteq> ghole_poss GMHole

goal (1 subgoal):
 1. \<forall>E\<in>set (sup_gmctxt_args GMHole D). E = GMHole \<or> num_gholes E = 0
[PROOF STEP]
by (cases D) (auto simp: in_set_conv_nth intro!: ghole_poss_num_gholes_zero, blast)
[PROOF STATE]
proof (state)
this:
\<forall>E\<in>set (sup_gmctxt_args GMHole D). E = GMHole \<or> num_gholes E = 0

goal (1 subgoal):
 1. \<And>cs ds f. \<lbrakk>length cs = length ds; \<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i; \<And>i. \<lbrakk>i < length cs; ghole_poss (ds ! i) \<subseteq> ghole_poss (cs ! i)\<rbrakk> \<Longrightarrow> \<forall>E\<in>set (sup_gmctxt_args (cs ! i) (ds ! i)). E = GMHole \<or> num_gholes E = 0; ghole_poss (GMFun f ds) \<subseteq> ghole_poss (GMFun f cs)\<rbrakk> \<Longrightarrow> \<forall>E\<in>set (sup_gmctxt_args (GMFun f cs) (GMFun f ds)). E = GMHole \<or> num_gholes E = 0
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cs ds f. \<lbrakk>length cs = length ds; \<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i; \<And>i. \<lbrakk>i < length cs; ghole_poss (ds ! i) \<subseteq> ghole_poss (cs ! i)\<rbrakk> \<Longrightarrow> \<forall>E\<in>set (sup_gmctxt_args (cs ! i) (ds ! i)). E = GMHole \<or> num_gholes E = 0; ghole_poss (GMFun f ds) \<subseteq> ghole_poss (GMFun f cs)\<rbrakk> \<Longrightarrow> \<forall>E\<in>set (sup_gmctxt_args (GMFun f cs) (GMFun f ds)). E = GMHole \<or> num_gholes E = 0
[PROOF STEP]
case (2 cs ds f)
[PROOF STATE]
proof (state)
this:
length cs = length ds
?i < length cs \<Longrightarrow> cs ! ?i \<le> ds ! ?i
\<lbrakk>?i < length cs; ghole_poss (ds ! ?i) \<subseteq> ghole_poss (cs ! ?i)\<rbrakk> \<Longrightarrow> \<forall>E\<in>set (sup_gmctxt_args (cs ! ?i) (ds ! ?i)). E = GMHole \<or> num_gholes E = 0
ghole_poss (GMFun f ds) \<subseteq> ghole_poss (GMFun f cs)

goal (1 subgoal):
 1. \<And>cs ds f. \<lbrakk>length cs = length ds; \<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i; \<And>i. \<lbrakk>i < length cs; ghole_poss (ds ! i) \<subseteq> ghole_poss (cs ! i)\<rbrakk> \<Longrightarrow> \<forall>E\<in>set (sup_gmctxt_args (cs ! i) (ds ! i)). E = GMHole \<or> num_gholes E = 0; ghole_poss (GMFun f ds) \<subseteq> ghole_poss (GMFun f cs)\<rbrakk> \<Longrightarrow> \<forall>E\<in>set (sup_gmctxt_args (GMFun f cs) (GMFun f ds)). E = GMHole \<or> num_gholes E = 0
[PROOF STEP]
note IS = this
[PROOF STATE]
proof (state)
this:
length cs = length ds
?i < length cs \<Longrightarrow> cs ! ?i \<le> ds ! ?i
\<lbrakk>?i < length cs; ghole_poss (ds ! ?i) \<subseteq> ghole_poss (cs ! ?i)\<rbrakk> \<Longrightarrow> \<forall>E\<in>set (sup_gmctxt_args (cs ! ?i) (ds ! ?i)). E = GMHole \<or> num_gholes E = 0
ghole_poss (GMFun f ds) \<subseteq> ghole_poss (GMFun f cs)

goal (1 subgoal):
 1. \<And>cs ds f. \<lbrakk>length cs = length ds; \<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i; \<And>i. \<lbrakk>i < length cs; ghole_poss (ds ! i) \<subseteq> ghole_poss (cs ! i)\<rbrakk> \<Longrightarrow> \<forall>E\<in>set (sup_gmctxt_args (cs ! i) (ds ! i)). E = GMHole \<or> num_gholes E = 0; ghole_poss (GMFun f ds) \<subseteq> ghole_poss (GMFun f cs)\<rbrakk> \<Longrightarrow> \<forall>E\<in>set (sup_gmctxt_args (GMFun f cs) (GMFun f ds)). E = GMHole \<or> num_gholes E = 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>E\<in>set (sup_gmctxt_args (GMFun f cs) (GMFun f ds)). E = GMHole \<or> num_gholes E = 0
[PROOF STEP]
using IS set_sup_gmctxt_args_split[OF IS(1)]
[PROOF STATE]
proof (prove)
using this:
length cs = length ds
?i < length cs \<Longrightarrow> cs ! ?i \<le> ds ! ?i
\<lbrakk>?i < length cs; ghole_poss (ds ! ?i) \<subseteq> ghole_poss (cs ! ?i)\<rbrakk> \<Longrightarrow> \<forall>E\<in>set (sup_gmctxt_args (cs ! ?i) (ds ! ?i)). E = GMHole \<or> num_gholes E = 0
ghole_poss (GMFun f ds) \<subseteq> ghole_poss (GMFun f cs)
set (sup_gmctxt_args (GMFun ?f cs) (GMFun ?f ds)) = (\<Union>i\<in>{0..<length ds}. set (sup_gmctxt_args (cs ! i) (ds ! i)))

goal (1 subgoal):
 1. \<forall>E\<in>set (sup_gmctxt_args (GMFun f cs) (GMFun f ds)). E = GMHole \<or> num_gholes E = 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>E\<in>set (sup_gmctxt_args (GMFun f cs) (GMFun f ds)). E = GMHole \<or> num_gholes E = 0

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>E\<in>set (sup_gmctxt_args C D). E = GMHole \<or> num_gholes E = 0

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inv_imples_ghole_poss_subseteq:
  "C \<le> D \<Longrightarrow> \<forall> E \<in> set (sup_gmctxt_args C D). E = GMHole \<or> num_gholes E = 0 \<Longrightarrow> ghole_poss D \<subseteq> ghole_poss C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C \<le> D; \<forall>E\<in>set (sup_gmctxt_args C D). E = GMHole \<or> num_gholes E = 0\<rbrakk> \<Longrightarrow> ghole_poss D \<subseteq> ghole_poss C
[PROOF STEP]
proof (induct rule: less_eq_gmctxt_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>u. \<forall>E\<in>set (sup_gmctxt_args GMHole u). E = GMHole \<or> num_gholes E = 0 \<Longrightarrow> ghole_poss u \<subseteq> ghole_poss GMHole
 2. \<And>cs ds f. \<lbrakk>length cs = length ds; \<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i; \<And>i. \<lbrakk>i < length cs; \<forall>E\<in>set (sup_gmctxt_args (cs ! i) (ds ! i)). E = GMHole \<or> num_gholes E = 0\<rbrakk> \<Longrightarrow> ghole_poss (ds ! i) \<subseteq> ghole_poss (cs ! i); \<forall>E\<in>set (sup_gmctxt_args (GMFun f cs) (GMFun f ds)). E = GMHole \<or> num_gholes E = 0\<rbrakk> \<Longrightarrow> ghole_poss (GMFun f ds) \<subseteq> ghole_poss (GMFun f cs)
[PROOF STEP]
case (1 D)
[PROOF STATE]
proof (state)
this:
\<forall>E\<in>set (sup_gmctxt_args GMHole D). E = GMHole \<or> num_gholes E = 0

goal (2 subgoals):
 1. \<And>u. \<forall>E\<in>set (sup_gmctxt_args GMHole u). E = GMHole \<or> num_gholes E = 0 \<Longrightarrow> ghole_poss u \<subseteq> ghole_poss GMHole
 2. \<And>cs ds f. \<lbrakk>length cs = length ds; \<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i; \<And>i. \<lbrakk>i < length cs; \<forall>E\<in>set (sup_gmctxt_args (cs ! i) (ds ! i)). E = GMHole \<or> num_gholes E = 0\<rbrakk> \<Longrightarrow> ghole_poss (ds ! i) \<subseteq> ghole_poss (cs ! i); \<forall>E\<in>set (sup_gmctxt_args (GMFun f cs) (GMFun f ds)). E = GMHole \<or> num_gholes E = 0\<rbrakk> \<Longrightarrow> ghole_poss (GMFun f ds) \<subseteq> ghole_poss (GMFun f cs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>E\<in>set (sup_gmctxt_args GMHole D). E = GMHole \<or> num_gholes E = 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>E\<in>set (sup_gmctxt_args GMHole D). E = GMHole \<or> num_gholes E = 0

goal (1 subgoal):
 1. ghole_poss D \<subseteq> ghole_poss GMHole
[PROOF STEP]
by (cases D) (auto simp: num_gholes_zero_ghole_poss)
[PROOF STATE]
proof (state)
this:
ghole_poss D \<subseteq> ghole_poss GMHole

goal (1 subgoal):
 1. \<And>cs ds f. \<lbrakk>length cs = length ds; \<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i; \<And>i. \<lbrakk>i < length cs; \<forall>E\<in>set (sup_gmctxt_args (cs ! i) (ds ! i)). E = GMHole \<or> num_gholes E = 0\<rbrakk> \<Longrightarrow> ghole_poss (ds ! i) \<subseteq> ghole_poss (cs ! i); \<forall>E\<in>set (sup_gmctxt_args (GMFun f cs) (GMFun f ds)). E = GMHole \<or> num_gholes E = 0\<rbrakk> \<Longrightarrow> ghole_poss (GMFun f ds) \<subseteq> ghole_poss (GMFun f cs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>cs ds f. \<lbrakk>length cs = length ds; \<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i; \<And>i. \<lbrakk>i < length cs; \<forall>E\<in>set (sup_gmctxt_args (cs ! i) (ds ! i)). E = GMHole \<or> num_gholes E = 0\<rbrakk> \<Longrightarrow> ghole_poss (ds ! i) \<subseteq> ghole_poss (cs ! i); \<forall>E\<in>set (sup_gmctxt_args (GMFun f cs) (GMFun f ds)). E = GMHole \<or> num_gholes E = 0\<rbrakk> \<Longrightarrow> ghole_poss (GMFun f ds) \<subseteq> ghole_poss (GMFun f cs)
[PROOF STEP]
case (2 cs ds f)
[PROOF STATE]
proof (state)
this:
length cs = length ds
?i < length cs \<Longrightarrow> cs ! ?i \<le> ds ! ?i
\<lbrakk>?i < length cs; \<forall>E\<in>set (sup_gmctxt_args (cs ! ?i) (ds ! ?i)). E = GMHole \<or> num_gholes E = 0\<rbrakk> \<Longrightarrow> ghole_poss (ds ! ?i) \<subseteq> ghole_poss (cs ! ?i)
\<forall>E\<in>set (sup_gmctxt_args (GMFun f cs) (GMFun f ds)). E = GMHole \<or> num_gholes E = 0

goal (1 subgoal):
 1. \<And>cs ds f. \<lbrakk>length cs = length ds; \<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i; \<And>i. \<lbrakk>i < length cs; \<forall>E\<in>set (sup_gmctxt_args (cs ! i) (ds ! i)). E = GMHole \<or> num_gholes E = 0\<rbrakk> \<Longrightarrow> ghole_poss (ds ! i) \<subseteq> ghole_poss (cs ! i); \<forall>E\<in>set (sup_gmctxt_args (GMFun f cs) (GMFun f ds)). E = GMHole \<or> num_gholes E = 0\<rbrakk> \<Longrightarrow> ghole_poss (GMFun f ds) \<subseteq> ghole_poss (GMFun f cs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
length cs = length ds
?i < length cs \<Longrightarrow> cs ! ?i \<le> ds ! ?i
\<lbrakk>?i < length cs; \<forall>E\<in>set (sup_gmctxt_args (cs ! ?i) (ds ! ?i)). E = GMHole \<or> num_gholes E = 0\<rbrakk> \<Longrightarrow> ghole_poss (ds ! ?i) \<subseteq> ghole_poss (cs ! ?i)
\<forall>E\<in>set (sup_gmctxt_args (GMFun f cs) (GMFun f ds)). E = GMHole \<or> num_gholes E = 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
length cs = length ds
?i < length cs \<Longrightarrow> cs ! ?i \<le> ds ! ?i
\<lbrakk>?i < length cs; \<forall>E\<in>set (sup_gmctxt_args (cs ! ?i) (ds ! ?i)). E = GMHole \<or> num_gholes E = 0\<rbrakk> \<Longrightarrow> ghole_poss (ds ! ?i) \<subseteq> ghole_poss (cs ! ?i)
\<forall>E\<in>set (sup_gmctxt_args (GMFun f cs) (GMFun f ds)). E = GMHole \<or> num_gholes E = 0

goal (1 subgoal):
 1. ghole_poss (GMFun f ds) \<subseteq> ghole_poss (GMFun f cs)
[PROOF STEP]
using set_sup_gmctxt_args_split[OF 2(1)]
[PROOF STATE]
proof (prove)
using this:
length cs = length ds
?i < length cs \<Longrightarrow> cs ! ?i \<le> ds ! ?i
\<lbrakk>?i < length cs; \<forall>E\<in>set (sup_gmctxt_args (cs ! ?i) (ds ! ?i)). E = GMHole \<or> num_gholes E = 0\<rbrakk> \<Longrightarrow> ghole_poss (ds ! ?i) \<subseteq> ghole_poss (cs ! ?i)
\<forall>E\<in>set (sup_gmctxt_args (GMFun f cs) (GMFun f ds)). E = GMHole \<or> num_gholes E = 0
set (sup_gmctxt_args (GMFun ?f cs) (GMFun ?f ds)) = (\<Union>i\<in>{0..<length ds}. set (sup_gmctxt_args (cs ! i) (ds ! i)))

goal (1 subgoal):
 1. ghole_poss (GMFun f ds) \<subseteq> ghole_poss (GMFun f cs)
[PROOF STEP]
by auto (metis (no_types, lifting) fst_conv in_set_zip snd_conv subsetD)
[PROOF STATE]
proof (state)
this:
ghole_poss (GMFun f ds) \<subseteq> ghole_poss (GMFun f cs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fill_gholes_gmctxt_ghole_poss_subseteq:
  assumes "num_gholes C = length Ds" "\<forall> i < length Ds. Ds ! i = GMHole \<or> num_gholes (Ds ! i) = 0"
  shows "ghole_poss (fill_gholes_gmctxt C Ds) \<subseteq> ghole_poss C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ghole_poss (fill_gholes_gmctxt C Ds) \<subseteq> ghole_poss C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
num_gholes C = length Ds
\<forall>i<length Ds. Ds ! i = GMHole \<or> num_gholes (Ds ! i) = 0

goal (1 subgoal):
 1. ghole_poss (fill_gholes_gmctxt C Ds) \<subseteq> ghole_poss C
[PROOF STEP]
proof (induct rule: fill_gholes_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<forall>i<length [x]. [x] ! i = GMHole \<or> num_gholes ([x] ! i) = 0 \<Longrightarrow> ghole_poss (fill_gholes_gmctxt GMHole [x]) \<subseteq> ghole_poss GMHole
 2. \<And>f Cs xs. \<lbrakk>sum_list (map num_gholes Cs) = length xs; \<And>i. \<lbrakk>i < length Cs; \<forall>ia<length (partition_gholes xs Cs ! i). partition_gholes xs Cs ! i ! ia = GMHole \<or> num_gholes (partition_gholes xs Cs ! i ! ia) = 0\<rbrakk> \<Longrightarrow> ghole_poss (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) \<subseteq> ghole_poss (Cs ! i); \<forall>i<length (concat (partition_gholes xs Cs)). concat (partition_gholes xs Cs) ! i = GMHole \<or> num_gholes (concat (partition_gholes xs Cs) ! i) = 0\<rbrakk> \<Longrightarrow> ghole_poss (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) \<subseteq> ghole_poss (GMFun f Cs)
[PROOF STEP]
case (GMFun f Cs xs)
[PROOF STATE]
proof (state)
this:
sum_list (map num_gholes Cs) = length xs
\<lbrakk>?i < length Cs; \<forall>i<length (partition_gholes xs Cs ! ?i). partition_gholes xs Cs ! ?i ! i = GMHole \<or> num_gholes (partition_gholes xs Cs ! ?i ! i) = 0\<rbrakk> \<Longrightarrow> ghole_poss (fill_gholes_gmctxt (Cs ! ?i) (partition_gholes xs Cs ! ?i)) \<subseteq> ghole_poss (Cs ! ?i)
\<forall>i<length (concat (partition_gholes xs Cs)). concat (partition_gholes xs Cs) ! i = GMHole \<or> num_gholes (concat (partition_gholes xs Cs) ! i) = 0

goal (2 subgoals):
 1. \<And>x. \<forall>i<length [x]. [x] ! i = GMHole \<or> num_gholes ([x] ! i) = 0 \<Longrightarrow> ghole_poss (fill_gholes_gmctxt GMHole [x]) \<subseteq> ghole_poss GMHole
 2. \<And>f Cs xs. \<lbrakk>sum_list (map num_gholes Cs) = length xs; \<And>i. \<lbrakk>i < length Cs; \<forall>ia<length (partition_gholes xs Cs ! i). partition_gholes xs Cs ! i ! ia = GMHole \<or> num_gholes (partition_gholes xs Cs ! i ! ia) = 0\<rbrakk> \<Longrightarrow> ghole_poss (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) \<subseteq> ghole_poss (Cs ! i); \<forall>i<length (concat (partition_gholes xs Cs)). concat (partition_gholes xs Cs) ! i = GMHole \<or> num_gholes (concat (partition_gholes xs Cs) ! i) = 0\<rbrakk> \<Longrightarrow> ghole_poss (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) \<subseteq> ghole_poss (GMFun f Cs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sum_list (map num_gholes Cs) = length xs
\<lbrakk>?i < length Cs; \<forall>i<length (partition_gholes xs Cs ! ?i). partition_gholes xs Cs ! ?i ! i = GMHole \<or> num_gholes (partition_gholes xs Cs ! ?i ! i) = 0\<rbrakk> \<Longrightarrow> ghole_poss (fill_gholes_gmctxt (Cs ! ?i) (partition_gholes xs Cs ! ?i)) \<subseteq> ghole_poss (Cs ! ?i)
\<forall>i<length (concat (partition_gholes xs Cs)). concat (partition_gholes xs Cs) ! i = GMHole \<or> num_gholes (concat (partition_gholes xs Cs) ! i) = 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sum_list (map num_gholes Cs) = length xs
\<lbrakk>?i < length Cs; \<forall>i<length (partition_gholes xs Cs ! ?i). partition_gholes xs Cs ! ?i ! i = GMHole \<or> num_gholes (partition_gholes xs Cs ! ?i ! i) = 0\<rbrakk> \<Longrightarrow> ghole_poss (fill_gholes_gmctxt (Cs ! ?i) (partition_gholes xs Cs ! ?i)) \<subseteq> ghole_poss (Cs ! ?i)
\<forall>i<length (concat (partition_gholes xs Cs)). concat (partition_gholes xs Cs) ! i = GMHole \<or> num_gholes (concat (partition_gholes xs Cs) ! i) = 0

goal (1 subgoal):
 1. ghole_poss (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) \<subseteq> ghole_poss (GMFun f Cs)
[PROOF STEP]
unfolding partition_holes_fill_gholes_gmctxt_conv'
[PROOF STATE]
proof (prove)
using this:
sum_list (map num_gholes Cs) = length xs
\<lbrakk>?i < length Cs; \<forall>i<length (partition_gholes xs Cs ! ?i). partition_gholes xs Cs ! ?i ! i = GMHole \<or> num_gholes (partition_gholes xs Cs ! ?i ! i) = 0\<rbrakk> \<Longrightarrow> ghole_poss (fill_gholes_gmctxt (Cs ! ?i) (partition_gholes xs Cs ! ?i)) \<subseteq> ghole_poss (Cs ! ?i)
\<forall>i<length (concat (partition_gholes xs Cs)). concat (partition_gholes xs Cs) ! i = GMHole \<or> num_gholes (concat (partition_gholes xs Cs) ! i) = 0

goal (1 subgoal):
 1. ghole_poss (GMFun f (map2 fill_gholes_gmctxt Cs (partition_gholes (concat (partition_gholes xs Cs)) Cs))) \<subseteq> ghole_poss (GMFun f Cs)
[PROOF STEP]
by auto (metis (no_types, lifting) length_map length_partition_by_nth partition_by_nth_nth(1, 2) subsetD)
[PROOF STATE]
proof (state)
this:
ghole_poss (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) \<subseteq> ghole_poss (GMFun f Cs)

goal (1 subgoal):
 1. \<And>x. \<forall>i<length [x]. [x] ! i = GMHole \<or> num_gholes ([x] ! i) = 0 \<Longrightarrow> ghole_poss (fill_gholes_gmctxt GMHole [x]) \<subseteq> ghole_poss GMHole
[PROOF STEP]
qed (auto simp: num_gholes_zero_ghole_poss)


[STATEMENT]
lemma ghole_poss_not_in_poss_gmctxt:
  assumes "p \<in> ghole_poss C"
  shows "p \<notin> poss_gmctxt C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<notin> poss_gmctxt C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p \<in> ghole_poss C

goal (1 subgoal):
 1. p \<notin> poss_gmctxt C
[PROOF STEP]
by (induct C arbitrary: p) auto


[STATEMENT]
lemma comp_gmctxt_inf_ghole_poss_cases:
  assumes "(C, D) \<in> comp_gmctxt" "p \<in> ghole_poss (C \<sqinter> D)"
  shows "p \<in> ghole_poss C \<and> p \<in> ghole_poss D \<or>
    p \<in> ghole_poss C \<and> p \<in> poss_gmctxt D \<or>
    p \<in> ghole_poss D \<and> p \<in> poss_gmctxt C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> ghole_poss C \<and> p \<in> ghole_poss D \<or> p \<in> ghole_poss C \<and> p \<in> poss_gmctxt D \<or> p \<in> ghole_poss D \<and> p \<in> poss_gmctxt C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(C, D) \<in> comp_gmctxt
p \<in> ghole_poss (C \<sqinter> D)

goal (1 subgoal):
 1. p \<in> ghole_poss C \<and> p \<in> ghole_poss D \<or> p \<in> ghole_poss C \<and> p \<in> poss_gmctxt D \<or> p \<in> ghole_poss D \<and> p \<in> poss_gmctxt C
[PROOF STEP]
proof (induct arbitrary: p)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>D p. p \<in> ghole_poss (GMHole \<sqinter> D) \<Longrightarrow> p \<in> ghole_poss GMHole \<and> p \<in> ghole_poss D \<or> p \<in> ghole_poss GMHole \<and> p \<in> poss_gmctxt D \<or> p \<in> ghole_poss D \<and> p \<in> poss_gmctxt GMHole
 2. \<And>C p. p \<in> ghole_poss (C \<sqinter> GMHole) \<Longrightarrow> p \<in> ghole_poss C \<and> p \<in> ghole_poss GMHole \<or> p \<in> ghole_poss C \<and> p \<in> poss_gmctxt GMHole \<or> p \<in> ghole_poss GMHole \<and> p \<in> poss_gmctxt C
 3. \<And>f g Cs Ds p. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> (\<forall>x. x \<in> ghole_poss (Cs ! i \<sqinter> Ds ! i) \<longrightarrow> x \<in> ghole_poss (Cs ! i) \<and> x \<in> ghole_poss (Ds ! i) \<or> x \<in> ghole_poss (Cs ! i) \<and> x \<in> poss_gmctxt (Ds ! i) \<or> x \<in> ghole_poss (Ds ! i) \<and> x \<in> poss_gmctxt (Cs ! i)); p \<in> ghole_poss (GMFun f Cs \<sqinter> GMFun g Ds)\<rbrakk> \<Longrightarrow> p \<in> ghole_poss (GMFun f Cs) \<and> p \<in> ghole_poss (GMFun g Ds) \<or> p \<in> ghole_poss (GMFun f Cs) \<and> p \<in> poss_gmctxt (GMFun g Ds) \<or> p \<in> ghole_poss (GMFun g Ds) \<and> p \<in> poss_gmctxt (GMFun f Cs)
[PROOF STEP]
case (GMHole1 D)
[PROOF STATE]
proof (state)
this:
p \<in> ghole_poss (GMHole \<sqinter> D)

goal (3 subgoals):
 1. \<And>D p. p \<in> ghole_poss (GMHole \<sqinter> D) \<Longrightarrow> p \<in> ghole_poss GMHole \<and> p \<in> ghole_poss D \<or> p \<in> ghole_poss GMHole \<and> p \<in> poss_gmctxt D \<or> p \<in> ghole_poss D \<and> p \<in> poss_gmctxt GMHole
 2. \<And>C p. p \<in> ghole_poss (C \<sqinter> GMHole) \<Longrightarrow> p \<in> ghole_poss C \<and> p \<in> ghole_poss GMHole \<or> p \<in> ghole_poss C \<and> p \<in> poss_gmctxt GMHole \<or> p \<in> ghole_poss GMHole \<and> p \<in> poss_gmctxt C
 3. \<And>f g Cs Ds p. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> (\<forall>x. x \<in> ghole_poss (Cs ! i \<sqinter> Ds ! i) \<longrightarrow> x \<in> ghole_poss (Cs ! i) \<and> x \<in> ghole_poss (Ds ! i) \<or> x \<in> ghole_poss (Cs ! i) \<and> x \<in> poss_gmctxt (Ds ! i) \<or> x \<in> ghole_poss (Ds ! i) \<and> x \<in> poss_gmctxt (Cs ! i)); p \<in> ghole_poss (GMFun f Cs \<sqinter> GMFun g Ds)\<rbrakk> \<Longrightarrow> p \<in> ghole_poss (GMFun f Cs) \<and> p \<in> ghole_poss (GMFun g Ds) \<or> p \<in> ghole_poss (GMFun f Cs) \<and> p \<in> poss_gmctxt (GMFun g Ds) \<or> p \<in> ghole_poss (GMFun g Ds) \<and> p \<in> poss_gmctxt (GMFun f Cs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> ghole_poss (GMHole \<sqinter> D)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p \<in> ghole_poss (GMHole \<sqinter> D)

goal (1 subgoal):
 1. p \<in> ghole_poss GMHole \<and> p \<in> ghole_poss D \<or> p \<in> ghole_poss GMHole \<and> p \<in> poss_gmctxt D \<or> p \<in> ghole_poss D \<and> p \<in> poss_gmctxt GMHole
[PROOF STEP]
by (cases D) auto
[PROOF STATE]
proof (state)
this:
p \<in> ghole_poss GMHole \<and> p \<in> ghole_poss D \<or> p \<in> ghole_poss GMHole \<and> p \<in> poss_gmctxt D \<or> p \<in> ghole_poss D \<and> p \<in> poss_gmctxt GMHole

goal (2 subgoals):
 1. \<And>C p. p \<in> ghole_poss (C \<sqinter> GMHole) \<Longrightarrow> p \<in> ghole_poss C \<and> p \<in> ghole_poss GMHole \<or> p \<in> ghole_poss C \<and> p \<in> poss_gmctxt GMHole \<or> p \<in> ghole_poss GMHole \<and> p \<in> poss_gmctxt C
 2. \<And>f g Cs Ds p. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> (\<forall>x. x \<in> ghole_poss (Cs ! i \<sqinter> Ds ! i) \<longrightarrow> x \<in> ghole_poss (Cs ! i) \<and> x \<in> ghole_poss (Ds ! i) \<or> x \<in> ghole_poss (Cs ! i) \<and> x \<in> poss_gmctxt (Ds ! i) \<or> x \<in> ghole_poss (Ds ! i) \<and> x \<in> poss_gmctxt (Cs ! i)); p \<in> ghole_poss (GMFun f Cs \<sqinter> GMFun g Ds)\<rbrakk> \<Longrightarrow> p \<in> ghole_poss (GMFun f Cs) \<and> p \<in> ghole_poss (GMFun g Ds) \<or> p \<in> ghole_poss (GMFun f Cs) \<and> p \<in> poss_gmctxt (GMFun g Ds) \<or> p \<in> ghole_poss (GMFun g Ds) \<and> p \<in> poss_gmctxt (GMFun f Cs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>C p. p \<in> ghole_poss (C \<sqinter> GMHole) \<Longrightarrow> p \<in> ghole_poss C \<and> p \<in> ghole_poss GMHole \<or> p \<in> ghole_poss C \<and> p \<in> poss_gmctxt GMHole \<or> p \<in> ghole_poss GMHole \<and> p \<in> poss_gmctxt C
 2. \<And>f g Cs Ds p. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> (\<forall>x. x \<in> ghole_poss (Cs ! i \<sqinter> Ds ! i) \<longrightarrow> x \<in> ghole_poss (Cs ! i) \<and> x \<in> ghole_poss (Ds ! i) \<or> x \<in> ghole_poss (Cs ! i) \<and> x \<in> poss_gmctxt (Ds ! i) \<or> x \<in> ghole_poss (Ds ! i) \<and> x \<in> poss_gmctxt (Cs ! i)); p \<in> ghole_poss (GMFun f Cs \<sqinter> GMFun g Ds)\<rbrakk> \<Longrightarrow> p \<in> ghole_poss (GMFun f Cs) \<and> p \<in> ghole_poss (GMFun g Ds) \<or> p \<in> ghole_poss (GMFun f Cs) \<and> p \<in> poss_gmctxt (GMFun g Ds) \<or> p \<in> ghole_poss (GMFun g Ds) \<and> p \<in> poss_gmctxt (GMFun f Cs)
[PROOF STEP]
case (GMHole2 C)
[PROOF STATE]
proof (state)
this:
p \<in> ghole_poss (C \<sqinter> GMHole)

goal (2 subgoals):
 1. \<And>C p. p \<in> ghole_poss (C \<sqinter> GMHole) \<Longrightarrow> p \<in> ghole_poss C \<and> p \<in> ghole_poss GMHole \<or> p \<in> ghole_poss C \<and> p \<in> poss_gmctxt GMHole \<or> p \<in> ghole_poss GMHole \<and> p \<in> poss_gmctxt C
 2. \<And>f g Cs Ds p. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> (\<forall>x. x \<in> ghole_poss (Cs ! i \<sqinter> Ds ! i) \<longrightarrow> x \<in> ghole_poss (Cs ! i) \<and> x \<in> ghole_poss (Ds ! i) \<or> x \<in> ghole_poss (Cs ! i) \<and> x \<in> poss_gmctxt (Ds ! i) \<or> x \<in> ghole_poss (Ds ! i) \<and> x \<in> poss_gmctxt (Cs ! i)); p \<in> ghole_poss (GMFun f Cs \<sqinter> GMFun g Ds)\<rbrakk> \<Longrightarrow> p \<in> ghole_poss (GMFun f Cs) \<and> p \<in> ghole_poss (GMFun g Ds) \<or> p \<in> ghole_poss (GMFun f Cs) \<and> p \<in> poss_gmctxt (GMFun g Ds) \<or> p \<in> ghole_poss (GMFun g Ds) \<and> p \<in> poss_gmctxt (GMFun f Cs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> ghole_poss (C \<sqinter> GMHole)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p \<in> ghole_poss (C \<sqinter> GMHole)

goal (1 subgoal):
 1. p \<in> ghole_poss C \<and> p \<in> ghole_poss GMHole \<or> p \<in> ghole_poss C \<and> p \<in> poss_gmctxt GMHole \<or> p \<in> ghole_poss GMHole \<and> p \<in> poss_gmctxt C
[PROOF STEP]
by (cases C) auto
[PROOF STATE]
proof (state)
this:
p \<in> ghole_poss C \<and> p \<in> ghole_poss GMHole \<or> p \<in> ghole_poss C \<and> p \<in> poss_gmctxt GMHole \<or> p \<in> ghole_poss GMHole \<and> p \<in> poss_gmctxt C

goal (1 subgoal):
 1. \<And>f g Cs Ds p. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> (\<forall>x. x \<in> ghole_poss (Cs ! i \<sqinter> Ds ! i) \<longrightarrow> x \<in> ghole_poss (Cs ! i) \<and> x \<in> ghole_poss (Ds ! i) \<or> x \<in> ghole_poss (Cs ! i) \<and> x \<in> poss_gmctxt (Ds ! i) \<or> x \<in> ghole_poss (Ds ! i) \<and> x \<in> poss_gmctxt (Cs ! i)); p \<in> ghole_poss (GMFun f Cs \<sqinter> GMFun g Ds)\<rbrakk> \<Longrightarrow> p \<in> ghole_poss (GMFun f Cs) \<and> p \<in> ghole_poss (GMFun g Ds) \<or> p \<in> ghole_poss (GMFun f Cs) \<and> p \<in> poss_gmctxt (GMFun g Ds) \<or> p \<in> ghole_poss (GMFun g Ds) \<and> p \<in> poss_gmctxt (GMFun f Cs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f g Cs Ds p. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> (\<forall>x. x \<in> ghole_poss (Cs ! i \<sqinter> Ds ! i) \<longrightarrow> x \<in> ghole_poss (Cs ! i) \<and> x \<in> ghole_poss (Ds ! i) \<or> x \<in> ghole_poss (Cs ! i) \<and> x \<in> poss_gmctxt (Ds ! i) \<or> x \<in> ghole_poss (Ds ! i) \<and> x \<in> poss_gmctxt (Cs ! i)); p \<in> ghole_poss (GMFun f Cs \<sqinter> GMFun g Ds)\<rbrakk> \<Longrightarrow> p \<in> ghole_poss (GMFun f Cs) \<and> p \<in> ghole_poss (GMFun g Ds) \<or> p \<in> ghole_poss (GMFun f Cs) \<and> p \<in> poss_gmctxt (GMFun g Ds) \<or> p \<in> ghole_poss (GMFun g Ds) \<and> p \<in> poss_gmctxt (GMFun f Cs)
[PROOF STEP]
case (GMFun f g Cs Ds)
[PROOF STATE]
proof (state)
this:
f = g
length Cs = length Ds
\<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> (\<forall>x. x \<in> ghole_poss (Cs ! i \<sqinter> Ds ! i) \<longrightarrow> x \<in> ghole_poss (Cs ! i) \<and> x \<in> ghole_poss (Ds ! i) \<or> x \<in> ghole_poss (Cs ! i) \<and> x \<in> poss_gmctxt (Ds ! i) \<or> x \<in> ghole_poss (Ds ! i) \<and> x \<in> poss_gmctxt (Cs ! i))
p \<in> ghole_poss (GMFun f Cs \<sqinter> GMFun g Ds)

goal (1 subgoal):
 1. \<And>f g Cs Ds p. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> (\<forall>x. x \<in> ghole_poss (Cs ! i \<sqinter> Ds ! i) \<longrightarrow> x \<in> ghole_poss (Cs ! i) \<and> x \<in> ghole_poss (Ds ! i) \<or> x \<in> ghole_poss (Cs ! i) \<and> x \<in> poss_gmctxt (Ds ! i) \<or> x \<in> ghole_poss (Ds ! i) \<and> x \<in> poss_gmctxt (Cs ! i)); p \<in> ghole_poss (GMFun f Cs \<sqinter> GMFun g Ds)\<rbrakk> \<Longrightarrow> p \<in> ghole_poss (GMFun f Cs) \<and> p \<in> ghole_poss (GMFun g Ds) \<or> p \<in> ghole_poss (GMFun f Cs) \<and> p \<in> poss_gmctxt (GMFun g Ds) \<or> p \<in> ghole_poss (GMFun g Ds) \<and> p \<in> poss_gmctxt (GMFun f Cs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f = g
length Cs = length Ds
\<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> (\<forall>x. x \<in> ghole_poss (Cs ! i \<sqinter> Ds ! i) \<longrightarrow> x \<in> ghole_poss (Cs ! i) \<and> x \<in> ghole_poss (Ds ! i) \<or> x \<in> ghole_poss (Cs ! i) \<and> x \<in> poss_gmctxt (Ds ! i) \<or> x \<in> ghole_poss (Ds ! i) \<and> x \<in> poss_gmctxt (Cs ! i))
p \<in> ghole_poss (GMFun f Cs \<sqinter> GMFun g Ds)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
f = g
length Cs = length Ds
\<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> (\<forall>x. x \<in> ghole_poss (Cs ! i \<sqinter> Ds ! i) \<longrightarrow> x \<in> ghole_poss (Cs ! i) \<and> x \<in> ghole_poss (Ds ! i) \<or> x \<in> ghole_poss (Cs ! i) \<and> x \<in> poss_gmctxt (Ds ! i) \<or> x \<in> ghole_poss (Ds ! i) \<and> x \<in> poss_gmctxt (Cs ! i))
p \<in> ghole_poss (GMFun f Cs \<sqinter> GMFun g Ds)

goal (1 subgoal):
 1. p \<in> ghole_poss (GMFun f Cs) \<and> p \<in> ghole_poss (GMFun g Ds) \<or> p \<in> ghole_poss (GMFun f Cs) \<and> p \<in> poss_gmctxt (GMFun g Ds) \<or> p \<in> ghole_poss (GMFun g Ds) \<and> p \<in> poss_gmctxt (GMFun f Cs)
[PROOF STEP]
by (auto simp: atLeast0LessThan) blast+
[PROOF STATE]
proof (state)
this:
p \<in> ghole_poss (GMFun f Cs) \<and> p \<in> ghole_poss (GMFun g Ds) \<or> p \<in> ghole_poss (GMFun f Cs) \<and> p \<in> poss_gmctxt (GMFun g Ds) \<or> p \<in> ghole_poss (GMFun g Ds) \<and> p \<in> poss_gmctxt (GMFun f Cs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma length_ghole_poss_list_num_gholes:
  "num_gholes C = length (ghole_poss_list C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes C = length (ghole_poss_list C)
[PROOF STEP]
by (induct C) (auto simp: length_concat intro: nth_sum_listI)


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

goal (2 subgoals):
 1. distinct (ghole_poss_list GMHole)
 2. \<And>x1 x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> distinct (ghole_poss_list x2a)) \<Longrightarrow> distinct (ghole_poss_list (GMFun x1 x2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x2a \<in> set Cs \<Longrightarrow> distinct (ghole_poss_list ?x2a)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?x2a \<in> set Cs \<Longrightarrow> distinct (ghole_poss_list ?x2a)

goal (1 subgoal):
 1. distinct (ghole_poss_list (GMFun f Cs))
[PROOF STEP]
proof (induct Cs rule: rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<And>x2a. x2a \<in> set [] \<Longrightarrow> distinct (ghole_poss_list x2a)) \<Longrightarrow> distinct (ghole_poss_list (GMFun f []))
 2. \<And>x xs. \<lbrakk>(\<And>x2a. x2a \<in> set xs \<Longrightarrow> distinct (ghole_poss_list x2a)) \<Longrightarrow> distinct (ghole_poss_list (GMFun f xs)); \<And>x2a. x2a \<in> set (xs @ [x]) \<Longrightarrow> distinct (ghole_poss_list x2a)\<rbrakk> \<Longrightarrow> distinct (ghole_poss_list (GMFun f (xs @ [x])))
[PROOF STEP]
case (snoc x xs)
[PROOF STATE]
proof (state)
this:
(\<And>x2a. x2a \<in> set xs \<Longrightarrow> distinct (ghole_poss_list x2a)) \<Longrightarrow> distinct (ghole_poss_list (GMFun f xs))
?x2a \<in> set (xs @ [x]) \<Longrightarrow> distinct (ghole_poss_list ?x2a)

goal (2 subgoals):
 1. (\<And>x2a. x2a \<in> set [] \<Longrightarrow> distinct (ghole_poss_list x2a)) \<Longrightarrow> distinct (ghole_poss_list (GMFun f []))
 2. \<And>x xs. \<lbrakk>(\<And>x2a. x2a \<in> set xs \<Longrightarrow> distinct (ghole_poss_list x2a)) \<Longrightarrow> distinct (ghole_poss_list (GMFun f xs)); \<And>x2a. x2a \<in> set (xs @ [x]) \<Longrightarrow> distinct (ghole_poss_list x2a)\<rbrakk> \<Longrightarrow> distinct (ghole_poss_list (GMFun f (xs @ [x])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<And>x2a. x2a \<in> set xs \<Longrightarrow> distinct (ghole_poss_list x2a)) \<Longrightarrow> distinct (ghole_poss_list (GMFun f xs))
?x2a \<in> set (xs @ [x]) \<Longrightarrow> distinct (ghole_poss_list ?x2a)
[PROOF STEP]
have "distinct (ghole_poss_list (GMFun f xs))" "distinct (ghole_poss_list x)"
[PROOF STATE]
proof (prove)
using this:
(\<And>x2a. x2a \<in> set xs \<Longrightarrow> distinct (ghole_poss_list x2a)) \<Longrightarrow> distinct (ghole_poss_list (GMFun f xs))
?x2a \<in> set (xs @ [x]) \<Longrightarrow> distinct (ghole_poss_list ?x2a)

goal (1 subgoal):
 1. distinct (ghole_poss_list (GMFun f xs)) &&& distinct (ghole_poss_list x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (ghole_poss_list (GMFun f xs))
distinct (ghole_poss_list x)

goal (2 subgoals):
 1. (\<And>x2a. x2a \<in> set [] \<Longrightarrow> distinct (ghole_poss_list x2a)) \<Longrightarrow> distinct (ghole_poss_list (GMFun f []))
 2. \<And>x xs. \<lbrakk>(\<And>x2a. x2a \<in> set xs \<Longrightarrow> distinct (ghole_poss_list x2a)) \<Longrightarrow> distinct (ghole_poss_list (GMFun f xs)); \<And>x2a. x2a \<in> set (xs @ [x]) \<Longrightarrow> distinct (ghole_poss_list x2a)\<rbrakk> \<Longrightarrow> distinct (ghole_poss_list (GMFun f (xs @ [x])))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct (ghole_poss_list (GMFun f xs))
distinct (ghole_poss_list x)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
distinct (ghole_poss_list (GMFun f xs))
distinct (ghole_poss_list x)

goal (1 subgoal):
 1. distinct (ghole_poss_list (GMFun f (xs @ [x])))
[PROOF STEP]
using snoc
[PROOF STATE]
proof (prove)
using this:
distinct (ghole_poss_list (GMFun f xs))
distinct (ghole_poss_list x)
(\<And>x2a. x2a \<in> set xs \<Longrightarrow> distinct (ghole_poss_list x2a)) \<Longrightarrow> distinct (ghole_poss_list (GMFun f xs))
?x2a \<in> set (xs @ [x]) \<Longrightarrow> distinct (ghole_poss_list ?x2a)

goal (1 subgoal):
 1. distinct (ghole_poss_list (GMFun f (xs @ [x])))
[PROOF STEP]
by (auto simp add: map_cons_presv_distinct dest: set_zip_leftD)
[PROOF STATE]
proof (state)
this:
distinct (ghole_poss_list (GMFun f (xs @ [x])))

goal (1 subgoal):
 1. (\<And>x2a. x2a \<in> set [] \<Longrightarrow> distinct (ghole_poss_list x2a)) \<Longrightarrow> distinct (ghole_poss_list (GMFun f []))
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
distinct (ghole_poss_list (GMFun f Cs))

goal (1 subgoal):
 1. distinct (ghole_poss_list GMHole)
[PROOF STEP]
qed auto


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

goal (2 subgoals):
 1. ghole_poss GMHole = set (ghole_poss_list GMHole)
 2. \<And>x1 x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> ghole_poss x2a = set (ghole_poss_list x2a)) \<Longrightarrow> ghole_poss (GMFun x1 x2) = set (ghole_poss_list (GMFun x1 x2))
[PROOF STEP]
note IS = GMFun[OF nth_mem]
[PROOF STATE]
proof (state)
this:
?n1 < length Cs \<Longrightarrow> ghole_poss (Cs ! ?n1) = set (ghole_poss_list (Cs ! ?n1))

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

goal (2 subgoals):
 1. ghole_poss GMHole = set (ghole_poss_list GMHole)
 2. \<And>x1 x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> ghole_poss x2a = set (ghole_poss_list x2a)) \<Longrightarrow> ghole_poss (GMFun x1 x2) = set (ghole_poss_list (GMFun x1 x2))
[PROOF STEP]
fix p
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ghole_poss GMHole = set (ghole_poss_list GMHole)
 2. \<And>x1 x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> ghole_poss x2a = set (ghole_poss_list x2a)) \<Longrightarrow> ghole_poss (GMFun x1 x2) = set (ghole_poss_list (GMFun x1 x2))
[PROOF STEP]
assume "p \<in> ghole_poss (GMFun f Cs)"
[PROOF STATE]
proof (state)
this:
p \<in> ghole_poss (GMFun f Cs)

goal (2 subgoals):
 1. ghole_poss GMHole = set (ghole_poss_list GMHole)
 2. \<And>x1 x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> ghole_poss x2a = set (ghole_poss_list x2a)) \<Longrightarrow> ghole_poss (GMFun x1 x2) = set (ghole_poss_list (GMFun x1 x2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p \<in> ghole_poss (GMFun f Cs)
[PROOF STEP]
obtain i ps where w: "p = i # ps" "i < length Cs"
      "ps \<in> ghole_poss (Cs ! i)"
[PROOF STATE]
proof (prove)
using this:
p \<in> ghole_poss (GMFun f Cs)

goal (1 subgoal):
 1. (\<And>i ps. \<lbrakk>p = i # ps; i < length Cs; ps \<in> ghole_poss (Cs ! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = i # ps
i < length Cs
ps \<in> ghole_poss (Cs ! i)

goal (2 subgoals):
 1. ghole_poss GMHole = set (ghole_poss_list GMHole)
 2. \<And>x1 x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> ghole_poss x2a = set (ghole_poss_list x2a)) \<Longrightarrow> ghole_poss (GMFun x1 x2) = set (ghole_poss_list (GMFun x1 x2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = i # ps
i < length Cs
ps \<in> ghole_poss (Cs ! i)
[PROOF STEP]
have "(i, Cs ! i) \<in> set (zip [0..<length Cs] Cs)"
[PROOF STATE]
proof (prove)
using this:
p = i # ps
i < length Cs
ps \<in> ghole_poss (Cs ! i)

goal (1 subgoal):
 1. (i, Cs ! i) \<in> set (zip [0..<length Cs] Cs)
[PROOF STEP]
by (force simp: in_set_zip)
[PROOF STATE]
proof (state)
this:
(i, Cs ! i) \<in> set (zip [0..<length Cs] Cs)

goal (2 subgoals):
 1. ghole_poss GMHole = set (ghole_poss_list GMHole)
 2. \<And>x1 x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> ghole_poss x2a = set (ghole_poss_list x2a)) \<Longrightarrow> ghole_poss (GMFun x1 x2) = set (ghole_poss_list (GMFun x1 x2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(i, Cs ! i) \<in> set (zip [0..<length Cs] Cs)
[PROOF STEP]
have "p \<in> set (ghole_poss_list (GMFun f Cs))"
[PROOF STATE]
proof (prove)
using this:
(i, Cs ! i) \<in> set (zip [0..<length Cs] Cs)

goal (1 subgoal):
 1. p \<in> set (ghole_poss_list (GMFun f Cs))
[PROOF STEP]
using IS[of i] w
[PROOF STATE]
proof (prove)
using this:
(i, Cs ! i) \<in> set (zip [0..<length Cs] Cs)
i < length Cs \<Longrightarrow> ghole_poss (Cs ! i) = set (ghole_poss_list (Cs ! i))
p = i # ps
i < length Cs
ps \<in> ghole_poss (Cs ! i)

goal (1 subgoal):
 1. p \<in> set (ghole_poss_list (GMFun f Cs))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p \<in> set (ghole_poss_list (GMFun f Cs))

goal (2 subgoals):
 1. ghole_poss GMHole = set (ghole_poss_list GMHole)
 2. \<And>x1 x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> ghole_poss x2a = set (ghole_poss_list x2a)) \<Longrightarrow> ghole_poss (GMFun x1 x2) = set (ghole_poss_list (GMFun x1 x2))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?p2 \<in> ghole_poss (GMFun f Cs) \<Longrightarrow> ?p2 \<in> set (ghole_poss_list (GMFun f Cs))

goal (2 subgoals):
 1. ghole_poss GMHole = set (ghole_poss_list GMHole)
 2. \<And>x1 x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> ghole_poss x2a = set (ghole_poss_list x2a)) \<Longrightarrow> ghole_poss (GMFun x1 x2) = set (ghole_poss_list (GMFun x1 x2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?p2 \<in> ghole_poss (GMFun f Cs) \<Longrightarrow> ?p2 \<in> set (ghole_poss_list (GMFun f Cs))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?p2 \<in> ghole_poss (GMFun f Cs) \<Longrightarrow> ?p2 \<in> set (ghole_poss_list (GMFun f Cs))

goal (1 subgoal):
 1. ghole_poss (GMFun f Cs) = set (ghole_poss_list (GMFun f Cs))
[PROOF STEP]
using IS
[PROOF STATE]
proof (prove)
using this:
?p2 \<in> ghole_poss (GMFun f Cs) \<Longrightarrow> ?p2 \<in> set (ghole_poss_list (GMFun f Cs))
?n1 < length Cs \<Longrightarrow> ghole_poss (Cs ! ?n1) = set (ghole_poss_list (Cs ! ?n1))

goal (1 subgoal):
 1. ghole_poss (GMFun f Cs) = set (ghole_poss_list (GMFun f Cs))
[PROOF STEP]
by (auto simp: in_set_zip)
[PROOF STATE]
proof (state)
this:
ghole_poss (GMFun f Cs) = set (ghole_poss_list (GMFun f Cs))

goal (1 subgoal):
 1. ghole_poss GMHole = set (ghole_poss_list GMHole)
[PROOF STEP]
qed auto


[STATEMENT]
lemma card_ghole_poss_num_gholes:
  "card (ghole_poss C) = num_gholes C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (ghole_poss C) = num_gholes C
[PROOF STEP]
unfolding ghole_poss_ghole_poss_list_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (set (ghole_poss_list C)) = num_gholes C
[PROOF STEP]
unfolding length_ghole_poss_list_num_gholes
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card (set (ghole_poss_list C)) = length (ghole_poss_list C)
[PROOF STEP]
using ghole_poss_list_distict
[PROOF STATE]
proof (prove)
using this:
distinct (ghole_poss_list ?C)

goal (1 subgoal):
 1. card (set (ghole_poss_list C)) = length (ghole_poss_list C)
[PROOF STEP]
using distinct_card
[PROOF STATE]
proof (prove)
using this:
distinct (ghole_poss_list ?C)
distinct ?xs \<Longrightarrow> card (set ?xs) = length ?xs

goal (1 subgoal):
 1. card (set (ghole_poss_list C)) = length (ghole_poss_list C)
[PROOF STEP]
by blast


[STATEMENT]
lemma subgm_at_hole_poss [simp]:
  "p \<in> ghole_poss C \<Longrightarrow> subgm_at C p = GMHole"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> ghole_poss C \<Longrightarrow> subgm_at C p = GMHole
[PROOF STEP]
by (induct C arbitrary: p) auto


[STATEMENT]
lemma subgm_at_mctxt_of_term:
  "p \<in> gposs t \<Longrightarrow> subgm_at (gmctxt_of_gterm t) p = gmctxt_of_gterm (gsubt_at t p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> gposs t \<Longrightarrow> subgm_at (gmctxt_of_gterm t) p = gmctxt_of_gterm (gsubt_at t p)
[PROOF STEP]
by (induct t arbitrary: p) auto


[STATEMENT]
lemma num_gholes_subgm_at:
  assumes "p \<in> poss_gmctxt C"
  shows "num_gholes (subgm_at C p) = ghole_num_at_pos p C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes (subgm_at C p) = ghole_num_at_pos p C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
p \<in> poss_gmctxt C

goal (1 subgoal):
 1. num_gholes (subgm_at C p) = ghole_num_at_pos p C
[PROOF STEP]
by (induct C arbitrary: p) auto


[STATEMENT]
lemma gmctxt_subtgm_at_fill_args_empty_pos [simp]:
  assumes "num_gholes C = length ts"
  shows "gmctxt_subtgm_at_fill_args [] C ts = ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gmctxt_subtgm_at_fill_args [] C ts = ts
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
num_gholes C = length ts

goal (1 subgoal):
 1. gmctxt_subtgm_at_fill_args [] C ts = ts
[PROOF STEP]
by (auto simp: gmctxt_subtgm_at_fill_args_def)


[STATEMENT]
lemma ghole_num_at_pos_fill_args_length:
  assumes "p \<in> poss_gmctxt C" "num_gholes C = length ts"
  shows "ghole_num_at_pos p C = length (gmctxt_subtgm_at_fill_args p C ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ghole_num_at_pos p C = length (gmctxt_subtgm_at_fill_args p C ts)
[PROOF STEP]
using ghole_num_bef_at_pos_num_gholes_less_eq[OF assms(1)] assms(2)
[PROOF STATE]
proof (prove)
using this:
ghole_num_bef_pos p C + ghole_num_at_pos p C \<le> num_gholes C
num_gholes C = length ts

goal (1 subgoal):
 1. ghole_num_at_pos p C = length (gmctxt_subtgm_at_fill_args p C ts)
[PROOF STEP]
by (auto simp: gmctxt_subtgm_at_fill_args_def)


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

goal (1 subgoal):
 1. ghole_num_bef_pos p C < length ts \<and> gsubt_at t p = ts ! ghole_num_bef_pos p C
[PROOF STEP]
proof (induct arbitrary: p rule: eq_gfill_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t p. p \<in> ghole_poss GMHole \<Longrightarrow> ghole_num_bef_pos p GMHole < length [t] \<and> gsubt_at t p = [t] ! ghole_num_bef_pos p GMHole
 2. \<And>f ss Cs ts p. \<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. x \<in> ghole_poss (Cs ! i) \<longrightarrow> ghole_num_bef_pos x (Cs ! i) < length (partition_gholes ts Cs ! i) \<and> gsubt_at (ss ! i) x = partition_gholes ts Cs ! i ! ghole_num_bef_pos x (Cs ! i)); p \<in> ghole_poss (GMFun f Cs)\<rbrakk> \<Longrightarrow> ghole_num_bef_pos p (GMFun f Cs) < length ts \<and> gsubt_at (GFun f ss) p = ts ! ghole_num_bef_pos p (GMFun f Cs)
[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. x \<in> ghole_poss (Cs ! i) \<longrightarrow> ghole_num_bef_pos x (Cs ! i) < length (partition_gholes ts Cs ! i) \<and> gsubt_at (ss ! i) x = partition_gholes ts Cs ! i ! ghole_num_bef_pos x (Cs ! i))
p \<in> ghole_poss (GMFun f Cs)

goal (2 subgoals):
 1. \<And>t p. p \<in> ghole_poss GMHole \<Longrightarrow> ghole_num_bef_pos p GMHole < length [t] \<and> gsubt_at t p = [t] ! ghole_num_bef_pos p GMHole
 2. \<And>f ss Cs ts p. \<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. x \<in> ghole_poss (Cs ! i) \<longrightarrow> ghole_num_bef_pos x (Cs ! i) < length (partition_gholes ts Cs ! i) \<and> gsubt_at (ss ! i) x = partition_gholes ts Cs ! i ! ghole_num_bef_pos x (Cs ! i)); p \<in> ghole_poss (GMFun f Cs)\<rbrakk> \<Longrightarrow> ghole_num_bef_pos p (GMFun f Cs) < length ts \<and> gsubt_at (GFun f ss) p = ts ! ghole_num_bef_pos p (GMFun f Cs)
[PROOF STEP]
let ?ts = "partition_gholes ts Cs"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t p. p \<in> ghole_poss GMHole \<Longrightarrow> ghole_num_bef_pos p GMHole < length [t] \<and> gsubt_at t p = [t] ! ghole_num_bef_pos p GMHole
 2. \<And>f ss Cs ts p. \<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. x \<in> ghole_poss (Cs ! i) \<longrightarrow> ghole_num_bef_pos x (Cs ! i) < length (partition_gholes ts Cs ! i) \<and> gsubt_at (ss ! i) x = partition_gholes ts Cs ! i ! ghole_num_bef_pos x (Cs ! i)); p \<in> ghole_poss (GMFun f Cs)\<rbrakk> \<Longrightarrow> ghole_num_bef_pos p (GMFun f Cs) < length ts \<and> gsubt_at (GFun f ss) p = ts ! ghole_num_bef_pos p (GMFun f Cs)
[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. x \<in> ghole_poss (Cs ! i) \<longrightarrow> ghole_num_bef_pos x (Cs ! i) < length (partition_gholes ts Cs ! i) \<and> gsubt_at (ss ! i) x = partition_gholes ts Cs ! i ! ghole_num_bef_pos x (Cs ! i))
p \<in> ghole_poss (GMFun f Cs)
[PROOF STEP]
obtain i and q where [simp]: "p = i # q"
    and "i < length ss" and "q \<in> ghole_poss (Cs ! i)"
[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. x \<in> ghole_poss (Cs ! i) \<longrightarrow> ghole_num_bef_pos x (Cs ! i) < length (partition_gholes ts Cs ! i) \<and> gsubt_at (ss ! i) x = partition_gholes ts Cs ! i ! ghole_num_bef_pos x (Cs ! i))
p \<in> ghole_poss (GMFun f Cs)

goal (1 subgoal):
 1. (\<And>i q. \<lbrakk>p = i # q; i < length ss; q \<in> ghole_poss (Cs ! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = i # q
i < length ss
q \<in> ghole_poss (Cs ! i)

goal (2 subgoals):
 1. \<And>t p. p \<in> ghole_poss GMHole \<Longrightarrow> ghole_num_bef_pos p GMHole < length [t] \<and> gsubt_at t p = [t] ! ghole_num_bef_pos p GMHole
 2. \<And>f ss Cs ts p. \<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. x \<in> ghole_poss (Cs ! i) \<longrightarrow> ghole_num_bef_pos x (Cs ! i) < length (partition_gholes ts Cs ! i) \<and> gsubt_at (ss ! i) x = partition_gholes ts Cs ! i ! ghole_num_bef_pos x (Cs ! i)); p \<in> ghole_poss (GMFun f Cs)\<rbrakk> \<Longrightarrow> ghole_num_bef_pos p (GMFun f Cs) < length ts \<and> gsubt_at (GFun f ss) p = ts ! ghole_num_bef_pos p (GMFun f Cs)
[PROOF STEP]
with GMFun.hyps
[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. x \<in> ghole_poss (Cs ! i) \<longrightarrow> ghole_num_bef_pos x (Cs ! i) < length (partition_gholes ts Cs ! i) \<and> gsubt_at (ss ! i) x = partition_gholes ts Cs ! i ! ghole_num_bef_pos x (Cs ! i))
p = i # q
i < length ss
q \<in> ghole_poss (Cs ! i)
[PROOF STEP]
have "ss ! i =\<^sub>G\<^sub>f (Cs ! i, ?ts ! i)"
    and j: "ghole_num_bef_pos q (Cs ! i) < length (?ts ! i)" (is "?j < length _")
    and *: "?ts ! i ! ghole_num_bef_pos q (Cs ! i) = gsubt_at (ss ! i) q"
[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. x \<in> ghole_poss (Cs ! i) \<longrightarrow> ghole_num_bef_pos x (Cs ! i) < length (partition_gholes ts Cs ! i) \<and> gsubt_at (ss ! i) x = partition_gholes ts Cs ! i ! ghole_num_bef_pos x (Cs ! i))
p = i # q
i < length ss
q \<in> ghole_poss (Cs ! i)

goal (1 subgoal):
 1. ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i) &&& ghole_num_bef_pos q (Cs ! i) < length (partition_gholes ts Cs ! i) &&& partition_gholes ts Cs ! i ! ghole_num_bef_pos q (Cs ! i) = gsubt_at (ss ! i) q
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ss ! i =\<^sub>G\<^sub>f (Cs ! i, partition_gholes ts Cs ! i)
ghole_num_bef_pos q (Cs ! i) < length (partition_gholes ts Cs ! i)
partition_gholes ts Cs ! i ! ghole_num_bef_pos q (Cs ! i) = gsubt_at (ss ! i) q

goal (2 subgoals):
 1. \<And>t p. p \<in> ghole_poss GMHole \<Longrightarrow> ghole_num_bef_pos p GMHole < length [t] \<and> gsubt_at t p = [t] ! ghole_num_bef_pos p GMHole
 2. \<And>f ss Cs ts p. \<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. x \<in> ghole_poss (Cs ! i) \<longrightarrow> ghole_num_bef_pos x (Cs ! i) < length (partition_gholes ts Cs ! i) \<and> gsubt_at (ss ! i) x = partition_gholes ts Cs ! i ! ghole_num_bef_pos x (Cs ! i)); p \<in> ghole_poss (GMFun f Cs)\<rbrakk> \<Longrightarrow> ghole_num_bef_pos p (GMFun f Cs) < length ts \<and> gsubt_at (GFun f ss) p = ts ! ghole_num_bef_pos p (GMFun f Cs)
[PROOF STEP]
let ?k = "sum_list (map length (take i ?ts)) + ?j"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t p. p \<in> ghole_poss GMHole \<Longrightarrow> ghole_num_bef_pos p GMHole < length [t] \<and> gsubt_at t p = [t] ! ghole_num_bef_pos p GMHole
 2. \<And>f ss Cs ts p. \<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. x \<in> ghole_poss (Cs ! i) \<longrightarrow> ghole_num_bef_pos x (Cs ! i) < length (partition_gholes ts Cs ! i) \<and> gsubt_at (ss ! i) x = partition_gholes ts Cs ! i ! ghole_num_bef_pos x (Cs ! i)); p \<in> ghole_poss (GMFun f Cs)\<rbrakk> \<Longrightarrow> ghole_num_bef_pos p (GMFun f Cs) < length ts \<and> gsubt_at (GFun f ss) p = ts ! ghole_num_bef_pos p (GMFun f Cs)
[PROOF STEP]
have "i < length ?ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length (partition_gholes ts Cs)
[PROOF STEP]
using \<open>i < length ss\<close> and GMFun
[PROOF STATE]
proof (prove)
using this:
i < length ss
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. x \<in> ghole_poss (Cs ! i) \<longrightarrow> ghole_num_bef_pos x (Cs ! i) < length (partition_gholes ts Cs ! i) \<and> gsubt_at (ss ! i) x = partition_gholes ts Cs ! i ! ghole_num_bef_pos x (Cs ! i))
p \<in> ghole_poss (GMFun f Cs)

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

goal (2 subgoals):
 1. \<And>t p. p \<in> ghole_poss GMHole \<Longrightarrow> ghole_num_bef_pos p GMHole < length [t] \<and> gsubt_at t p = [t] ! ghole_num_bef_pos p GMHole
 2. \<And>f ss Cs ts p. \<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. x \<in> ghole_poss (Cs ! i) \<longrightarrow> ghole_num_bef_pos x (Cs ! i) < length (partition_gholes ts Cs ! i) \<and> gsubt_at (ss ! i) x = partition_gholes ts Cs ! i ! ghole_num_bef_pos x (Cs ! i)); p \<in> ghole_poss (GMFun f Cs)\<rbrakk> \<Longrightarrow> ghole_num_bef_pos p (GMFun f Cs) < length ts \<and> gsubt_at (GFun f ss) p = ts ! ghole_num_bef_pos p (GMFun f Cs)
[PROOF STEP]
with partition_by_nth_nth_old [OF this j] and GMFun and concat_nth_length [OF this j]
[PROOF STATE]
proof (chain)
picking this:
sum_list (map num_gholes Cs) = length ts \<Longrightarrow> partition_gholes ts Cs ! i ! ghole_num_bef_pos q (Cs ! i) = ts ! (sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i))
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. x \<in> ghole_poss (Cs ! i) \<longrightarrow> ghole_num_bef_pos x (Cs ! i) < length (partition_gholes ts Cs ! i) \<and> gsubt_at (ss ! i) x = partition_gholes ts Cs ! i ! ghole_num_bef_pos x (Cs ! i))
p \<in> ghole_poss (GMFun f Cs)
sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i) < length (concat (partition_gholes ts Cs))
i < length (partition_gholes ts Cs)
[PROOF STEP]
have "?ts ! i ! ?j = ts ! ?k" and "?k < length ts"
[PROOF STATE]
proof (prove)
using this:
sum_list (map num_gholes Cs) = length ts \<Longrightarrow> partition_gholes ts Cs ! i ! ghole_num_bef_pos q (Cs ! i) = ts ! (sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i))
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. x \<in> ghole_poss (Cs ! i) \<longrightarrow> ghole_num_bef_pos x (Cs ! i) < length (partition_gholes ts Cs ! i) \<and> gsubt_at (ss ! i) x = partition_gholes ts Cs ! i ! ghole_num_bef_pos x (Cs ! i))
p \<in> ghole_poss (GMFun f Cs)
sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i) < length (concat (partition_gholes ts Cs))
i < length (partition_gholes ts Cs)

goal (1 subgoal):
 1. partition_gholes ts Cs ! i ! ghole_num_bef_pos q (Cs ! i) = ts ! (sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i)) &&& sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i) < length ts
[PROOF STEP]
by (auto)
[PROOF STATE]
proof (state)
this:
partition_gholes ts Cs ! i ! ghole_num_bef_pos q (Cs ! i) = ts ! (sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i))
sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i) < length ts

goal (2 subgoals):
 1. \<And>t p. p \<in> ghole_poss GMHole \<Longrightarrow> ghole_num_bef_pos p GMHole < length [t] \<and> gsubt_at t p = [t] ! ghole_num_bef_pos p GMHole
 2. \<And>f ss Cs ts p. \<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. x \<in> ghole_poss (Cs ! i) \<longrightarrow> ghole_num_bef_pos x (Cs ! i) < length (partition_gholes ts Cs ! i) \<and> gsubt_at (ss ! i) x = partition_gholes ts Cs ! i ! ghole_num_bef_pos x (Cs ! i)); p \<in> ghole_poss (GMFun f Cs)\<rbrakk> \<Longrightarrow> ghole_num_bef_pos p (GMFun f Cs) < length ts \<and> gsubt_at (GFun f ss) p = ts ! ghole_num_bef_pos p (GMFun f Cs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
partition_gholes ts Cs ! i ! ghole_num_bef_pos q (Cs ! i) = ts ! (sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i))
sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i) < length ts

goal (2 subgoals):
 1. \<And>t p. p \<in> ghole_poss GMHole \<Longrightarrow> ghole_num_bef_pos p GMHole < length [t] \<and> gsubt_at t p = [t] ! ghole_num_bef_pos p GMHole
 2. \<And>f ss Cs ts p. \<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. x \<in> ghole_poss (Cs ! i) \<longrightarrow> ghole_num_bef_pos x (Cs ! i) < length (partition_gholes ts Cs ! i) \<and> gsubt_at (ss ! i) x = partition_gholes ts Cs ! i ! ghole_num_bef_pos x (Cs ! i)); p \<in> ghole_poss (GMFun f Cs)\<rbrakk> \<Longrightarrow> ghole_num_bef_pos p (GMFun f Cs) < length ts \<and> gsubt_at (GFun f ss) p = ts ! ghole_num_bef_pos p (GMFun f Cs)
[PROOF STEP]
with *
[PROOF STATE]
proof (chain)
picking this:
partition_gholes ts Cs ! i ! ghole_num_bef_pos q (Cs ! i) = gsubt_at (ss ! i) q
partition_gholes ts Cs ! i ! ghole_num_bef_pos q (Cs ! i) = ts ! (sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i))
sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i) < length ts
[PROOF STEP]
have "ts ! ?k = gsubt_at (GFun f ss) p"
[PROOF STATE]
proof (prove)
using this:
partition_gholes ts Cs ! i ! ghole_num_bef_pos q (Cs ! i) = gsubt_at (ss ! i) q
partition_gholes ts Cs ! i ! ghole_num_bef_pos q (Cs ! i) = ts ! (sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i))
sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i) < length ts

goal (1 subgoal):
 1. ts ! (sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i)) = gsubt_at (GFun f ss) p
[PROOF STEP]
using \<open>i < length ss\<close>
[PROOF STATE]
proof (prove)
using this:
partition_gholes ts Cs ! i ! ghole_num_bef_pos q (Cs ! i) = gsubt_at (ss ! i) q
partition_gholes ts Cs ! i ! ghole_num_bef_pos q (Cs ! i) = ts ! (sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i))
sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i) < length ts
i < length ss

goal (1 subgoal):
 1. ts ! (sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i)) = gsubt_at (GFun f ss) p
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ts ! (sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i)) = gsubt_at (GFun f ss) p

goal (2 subgoals):
 1. \<And>t p. p \<in> ghole_poss GMHole \<Longrightarrow> ghole_num_bef_pos p GMHole < length [t] \<and> gsubt_at t p = [t] ! ghole_num_bef_pos p GMHole
 2. \<And>f ss Cs ts p. \<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. x \<in> ghole_poss (Cs ! i) \<longrightarrow> ghole_num_bef_pos x (Cs ! i) < length (partition_gholes ts Cs ! i) \<and> gsubt_at (ss ! i) x = partition_gholes ts Cs ! i ! ghole_num_bef_pos x (Cs ! i)); p \<in> ghole_poss (GMFun f Cs)\<rbrakk> \<Longrightarrow> ghole_num_bef_pos p (GMFun f Cs) < length ts \<and> gsubt_at (GFun f ss) p = ts ! ghole_num_bef_pos p (GMFun f Cs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
partition_gholes ts Cs ! i ! ghole_num_bef_pos q (Cs ! i) = ts ! (sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i))
sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i) < length ts
ts ! (sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i)) = gsubt_at (GFun f ss) p
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
partition_gholes ts Cs ! i ! ghole_num_bef_pos q (Cs ! i) = ts ! (sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i))
sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i) < length ts
ts ! (sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i)) = gsubt_at (GFun f ss) p

goal (1 subgoal):
 1. ghole_num_bef_pos p (GMFun f Cs) < length ts \<and> gsubt_at (GFun f ss) p = ts ! ghole_num_bef_pos p (GMFun f Cs)
[PROOF STEP]
using GMFun.hyps(2)
[PROOF STATE]
proof (prove)
using this:
partition_gholes ts Cs ! i ! ghole_num_bef_pos q (Cs ! i) = ts ! (sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i))
sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i) < length ts
ts ! (sum_list (map length (take i (partition_gholes ts Cs))) + ghole_num_bef_pos q (Cs ! i)) = gsubt_at (GFun f ss) p
sum_list (map num_gholes Cs) = length ts

goal (1 subgoal):
 1. ghole_num_bef_pos p (GMFun f Cs) < length ts \<and> gsubt_at (GFun f ss) p = ts ! ghole_num_bef_pos p (GMFun f Cs)
[PROOF STEP]
by (auto simp: take_map [symmetric])
[PROOF STATE]
proof (state)
this:
ghole_num_bef_pos p (GMFun f Cs) < length ts \<and> gsubt_at (GFun f ss) p = ts ! ghole_num_bef_pos p (GMFun f Cs)

goal (1 subgoal):
 1. \<And>t p. p \<in> ghole_poss GMHole \<Longrightarrow> ghole_num_bef_pos p GMHole < length [t] \<and> gsubt_at t p = [t] ! ghole_num_bef_pos p GMHole
[PROOF STEP]
qed auto


[STATEMENT]
lemma poss_gmctxt_fill_gholes_split:
  assumes "t =\<^sub>G\<^sub>f (C, ts)" and "p \<in> poss_gmctxt C"
  shows "gsubt_at t p =\<^sub>G\<^sub>f (subgm_at C p , gmctxt_subtgm_at_fill_args p C ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gsubt_at t p =\<^sub>G\<^sub>f (subgm_at C p, gmctxt_subtgm_at_fill_args p C ts)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
t =\<^sub>G\<^sub>f (C, ts)
p \<in> poss_gmctxt C

goal (1 subgoal):
 1. gsubt_at t p =\<^sub>G\<^sub>f (subgm_at C p, gmctxt_subtgm_at_fill_args p C ts)
[PROOF STEP]
proof (induct arbitrary: p rule: eq_gfill_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t p. p \<in> poss_gmctxt GMHole \<Longrightarrow> gsubt_at t p =\<^sub>G\<^sub>f (subgm_at GMHole p, gmctxt_subtgm_at_fill_args p GMHole [t])
 2. \<And>f ss Cs ts p. \<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. x \<in> poss_gmctxt (Cs ! i) \<longrightarrow> gsubt_at (ss ! i) x =\<^sub>G\<^sub>f (subgm_at (Cs ! i) x, gmctxt_subtgm_at_fill_args x (Cs ! i) (partition_gholes ts Cs ! i))); p \<in> poss_gmctxt (GMFun f Cs)\<rbrakk> \<Longrightarrow> gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)
[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. x \<in> poss_gmctxt (Cs ! i) \<longrightarrow> gsubt_at (ss ! i) x =\<^sub>G\<^sub>f (subgm_at (Cs ! i) x, gmctxt_subtgm_at_fill_args x (Cs ! i) (partition_gholes ts Cs ! i)))
p \<in> poss_gmctxt (GMFun f Cs)

goal (2 subgoals):
 1. \<And>t p. p \<in> poss_gmctxt GMHole \<Longrightarrow> gsubt_at t p =\<^sub>G\<^sub>f (subgm_at GMHole p, gmctxt_subtgm_at_fill_args p GMHole [t])
 2. \<And>f ss Cs ts p. \<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. x \<in> poss_gmctxt (Cs ! i) \<longrightarrow> gsubt_at (ss ! i) x =\<^sub>G\<^sub>f (subgm_at (Cs ! i) x, gmctxt_subtgm_at_fill_args x (Cs ! i) (partition_gholes ts Cs ! i))); p \<in> poss_gmctxt (GMFun f Cs)\<rbrakk> \<Longrightarrow> gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)
[PROOF STEP]
let ?ts = "partition_gholes ts Cs"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t p. p \<in> poss_gmctxt GMHole \<Longrightarrow> gsubt_at t p =\<^sub>G\<^sub>f (subgm_at GMHole p, gmctxt_subtgm_at_fill_args p GMHole [t])
 2. \<And>f ss Cs ts p. \<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. x \<in> poss_gmctxt (Cs ! i) \<longrightarrow> gsubt_at (ss ! i) x =\<^sub>G\<^sub>f (subgm_at (Cs ! i) x, gmctxt_subtgm_at_fill_args x (Cs ! i) (partition_gholes ts Cs ! i))); p \<in> poss_gmctxt (GMFun f Cs)\<rbrakk> \<Longrightarrow> gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)
[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. x \<in> poss_gmctxt (Cs ! i) \<longrightarrow> gsubt_at (ss ! i) x =\<^sub>G\<^sub>f (subgm_at (Cs ! i) x, gmctxt_subtgm_at_fill_args x (Cs ! i) (partition_gholes ts Cs ! i)))
p \<in> poss_gmctxt (GMFun f Cs)
[PROOF STEP]
have "\<And> i. i < length Cs \<Longrightarrow> ss ! i =\<^sub>G\<^sub>f (Cs ! i, ?ts ! i)"
[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. x \<in> poss_gmctxt (Cs ! i) \<longrightarrow> gsubt_at (ss ! i) x =\<^sub>G\<^sub>f (subgm_at (Cs ! i) x, gmctxt_subtgm_at_fill_args x (Cs ! i) (partition_gholes ts Cs ! i)))
p \<in> poss_gmctxt (GMFun f Cs)

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

goal (2 subgoals):
 1. \<And>t p. p \<in> poss_gmctxt GMHole \<Longrightarrow> gsubt_at t p =\<^sub>G\<^sub>f (subgm_at GMHole p, gmctxt_subtgm_at_fill_args p GMHole [t])
 2. \<And>f ss Cs ts p. \<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. x \<in> poss_gmctxt (Cs ! i) \<longrightarrow> gsubt_at (ss ! i) x =\<^sub>G\<^sub>f (subgm_at (Cs ! i) x, gmctxt_subtgm_at_fill_args x (Cs ! i) (partition_gholes ts Cs ! i))); p \<in> poss_gmctxt (GMFun f Cs)\<rbrakk> \<Longrightarrow> gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)
[PROOF STEP]
proof (cases p)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = [] \<Longrightarrow> gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)
 2. \<And>a list. p = a # list \<Longrightarrow> gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
p = []

goal (2 subgoals):
 1. p = [] \<Longrightarrow> gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)
 2. \<And>a list. p = a # list \<Longrightarrow> gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = []
[PROOF STEP]
have "GFun f ss =\<^sub>G\<^sub>f (GMFun f Cs, concat ?ts)"
[PROOF STATE]
proof (prove)
using this:
p = []

goal (1 subgoal):
 1. GFun f ss =\<^sub>G\<^sub>f (GMFun f Cs, concat (partition_gholes ts Cs))
[PROOF STEP]
using GMFun
[PROOF STATE]
proof (prove)
using this:
p = []
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. x \<in> poss_gmctxt (Cs ! i) \<longrightarrow> gsubt_at (ss ! i) x =\<^sub>G\<^sub>f (subgm_at (Cs ! i) x, gmctxt_subtgm_at_fill_args x (Cs ! i) (partition_gholes ts Cs ! i)))
p \<in> poss_gmctxt (GMFun f Cs)

goal (1 subgoal):
 1. GFun f ss =\<^sub>G\<^sub>f (GMFun f Cs, concat (partition_gholes ts Cs))
[PROOF STEP]
by (intro eqgf_GMFunI) (auto simp del: fill_gholes.simps)
[PROOF STATE]
proof (state)
this:
GFun f ss =\<^sub>G\<^sub>f (GMFun f Cs, concat (partition_gholes ts Cs))

goal (2 subgoals):
 1. p = [] \<Longrightarrow> gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)
 2. \<And>a list. p = a # list \<Longrightarrow> gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
GFun f ss =\<^sub>G\<^sub>f (GMFun f Cs, concat (partition_gholes ts Cs))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
GFun f ss =\<^sub>G\<^sub>f (GMFun f Cs, concat (partition_gholes ts Cs))

goal (1 subgoal):
 1. gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)
[PROOF STEP]
using GMFun
[PROOF STATE]
proof (prove)
using this:
GFun f ss =\<^sub>G\<^sub>f (GMFun f Cs, concat (partition_gholes ts 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. x \<in> poss_gmctxt (Cs ! i) \<longrightarrow> gsubt_at (ss ! i) x =\<^sub>G\<^sub>f (subgm_at (Cs ! i) x, gmctxt_subtgm_at_fill_args x (Cs ! i) (partition_gholes ts Cs ! i)))
p \<in> poss_gmctxt (GMFun f Cs)

goal (1 subgoal):
 1. gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)
[PROOF STEP]
unfolding Nil
[PROOF STATE]
proof (prove)
using this:
GFun f ss =\<^sub>G\<^sub>f (GMFun f Cs, concat (partition_gholes ts 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. x \<in> poss_gmctxt (Cs ! i) \<longrightarrow> gsubt_at (ss ! i) x =\<^sub>G\<^sub>f (subgm_at (Cs ! i) x, gmctxt_subtgm_at_fill_args x (Cs ! i) (partition_gholes ts Cs ! i)))
[] \<in> poss_gmctxt (GMFun f Cs)

goal (1 subgoal):
 1. gsubt_at (GFun f ss) [] =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) [], gmctxt_subtgm_at_fill_args [] (GMFun f Cs) ts)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)

goal (1 subgoal):
 1. \<And>a list. p = a # list \<Longrightarrow> gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a list. p = a # list \<Longrightarrow> gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)
[PROOF STEP]
case (Cons i q)
[PROOF STATE]
proof (state)
this:
p = i # q

goal (1 subgoal):
 1. \<And>a list. p = a # list \<Longrightarrow> gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = i # q
[PROOF STEP]
have "ghole_num_at_pos q (Cs ! i) \<le> num_gholes (Cs ! i) - ghole_num_bef_pos q (Cs ! i)"
[PROOF STATE]
proof (prove)
using this:
p = i # q

goal (1 subgoal):
 1. ghole_num_at_pos q (Cs ! i) \<le> num_gholes (Cs ! i) - ghole_num_bef_pos q (Cs ! i)
[PROOF STEP]
using GMFun(1, 2, 4) ghole_num_bef_at_pos_num_gholes_less_eq[of q "Cs ! i"]
[PROOF STATE]
proof (prove)
using this:
p = i # q
length Cs = length ss
sum_list (map num_gholes Cs) = length ts
p \<in> poss_gmctxt (GMFun f Cs)
q \<in> poss_gmctxt (Cs ! i) \<Longrightarrow> ghole_num_bef_pos q (Cs ! i) + ghole_num_at_pos q (Cs ! i) \<le> num_gholes (Cs ! i)

goal (1 subgoal):
 1. ghole_num_at_pos q (Cs ! i) \<le> num_gholes (Cs ! i) - ghole_num_bef_pos q (Cs ! i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ghole_num_at_pos q (Cs ! i) \<le> num_gholes (Cs ! i) - ghole_num_bef_pos q (Cs ! i)

goal (1 subgoal):
 1. \<And>a list. p = a # list \<Longrightarrow> gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ghole_num_at_pos q (Cs ! i) \<le> num_gholes (Cs ! i) - ghole_num_bef_pos q (Cs ! i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
ghole_num_at_pos q (Cs ! i) \<le> num_gholes (Cs ! i) - ghole_num_bef_pos q (Cs ! i)

goal (1 subgoal):
 1. gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)
[PROOF STEP]
using GMFun
[PROOF STATE]
proof (prove)
using this:
ghole_num_at_pos q (Cs ! i) \<le> num_gholes (Cs ! i) - ghole_num_bef_pos q (Cs ! i)
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. x \<in> poss_gmctxt (Cs ! i) \<longrightarrow> gsubt_at (ss ! i) x =\<^sub>G\<^sub>f (subgm_at (Cs ! i) x, gmctxt_subtgm_at_fill_args x (Cs ! i) (partition_gholes ts Cs ! i)))
p \<in> poss_gmctxt (GMFun f Cs)

goal (1 subgoal):
 1. gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)
[PROOF STEP]
by (auto simp: Cons add.commute gmctxt_subtgm_at_fill_args_def partition_by_nth drop_take take_map min_def split!: if_splits)
[PROOF STATE]
proof (state)
this:
gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
gsubt_at (GFun f ss) p =\<^sub>G\<^sub>f (subgm_at (GMFun f Cs) p, gmctxt_subtgm_at_fill_args p (GMFun f Cs) ts)

goal (1 subgoal):
 1. \<And>t p. p \<in> poss_gmctxt GMHole \<Longrightarrow> gsubt_at t p =\<^sub>G\<^sub>f (subgm_at GMHole p, gmctxt_subtgm_at_fill_args p GMHole [t])
[PROOF STEP]
qed auto