[STATEMENT]
lemma fill_gholes_gmctxt_fill_gholes:
  assumes len_ds: "length Ds = num_gholes C"
    and nh: "num_gholes (fill_gholes_gmctxt C Ds) = length ss"
  shows "fill_gholes (fill_gholes_gmctxt C Ds) ss =
  fill_gholes C [fill_gholes (Ds ! i) (partition_gholes ss Ds ! i). i \<leftarrow> [0 ..< num_gholes C]]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_gholes (fill_gholes_gmctxt C Ds) ss = fill_gholes C (map (\<lambda>i. fill_gholes (Ds ! i) (partition_gholes ss Ds ! i)) [0..<num_gholes C])
[PROOF STEP]
using assms(1)[symmetric] assms(2)
[PROOF STATE]
proof (prove)
using this:
num_gholes C = length Ds
num_gholes (fill_gholes_gmctxt C Ds) = length ss

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

goal (2 subgoals):
 1. \<And>x ss. num_gholes (fill_gholes_gmctxt GMHole [x]) = length ss \<Longrightarrow> fill_gholes (fill_gholes_gmctxt GMHole [x]) ss = fill_gholes GMHole (map (\<lambda>i. fill_gholes ([x] ! i) (partition_gholes ss [x] ! i)) [0..<num_gholes GMHole])
 2. \<And>f Cs xs ss. \<lbrakk>sum_list (map num_gholes Cs) = length xs; \<And>i ss. \<lbrakk>i < length Cs; num_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) ss = fill_gholes (Cs ! i) (map (\<lambda>ia. fill_gholes (partition_gholes xs Cs ! i ! ia) (partition_gholes ss (partition_gholes xs Cs ! i) ! ia)) [0..<num_gholes (Cs ! i)]); num_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) ss = fill_gholes (GMFun f Cs) (map (\<lambda>i. fill_gholes (concat (partition_gholes xs Cs) ! i) (partition_gholes ss (concat (partition_gholes xs Cs)) ! i)) [0..<num_gholes (GMFun f Cs)])
[PROOF STEP]
define qs where "qs = map (\<lambda>i. fill_gholes_gmctxt (Cs ! i) (partition_gholes ds Cs ! i)) [0..<length Cs]"
[PROOF STATE]
proof (state)
this:
qs = map (\<lambda>i. fill_gholes_gmctxt (Cs ! i) (partition_gholes ds Cs ! i)) [0..<length Cs]

goal (2 subgoals):
 1. \<And>x ss. num_gholes (fill_gholes_gmctxt GMHole [x]) = length ss \<Longrightarrow> fill_gholes (fill_gholes_gmctxt GMHole [x]) ss = fill_gholes GMHole (map (\<lambda>i. fill_gholes ([x] ! i) (partition_gholes ss [x] ! i)) [0..<num_gholes GMHole])
 2. \<And>f Cs xs ss. \<lbrakk>sum_list (map num_gholes Cs) = length xs; \<And>i ss. \<lbrakk>i < length Cs; num_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) ss = fill_gholes (Cs ! i) (map (\<lambda>ia. fill_gholes (partition_gholes xs Cs ! i ! ia) (partition_gholes ss (partition_gholes xs Cs ! i) ! ia)) [0..<num_gholes (Cs ! i)]); num_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) ss = fill_gholes (GMFun f Cs) (map (\<lambda>i. fill_gholes (concat (partition_gholes xs Cs) ! i) (partition_gholes ss (concat (partition_gholes xs Cs)) ! i)) [0..<num_gholes (GMFun f Cs)])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
qs = map (\<lambda>i. fill_gholes_gmctxt (Cs ! i) (partition_gholes ds Cs ! i)) [0..<length Cs]
[PROOF STEP]
have qs: "\<And>i. i < length Cs \<Longrightarrow> fill_gholes_gmctxt (Cs ! i) (partition_gholes ds Cs ! i) = qs ! i"
    "length qs = length Cs"
[PROOF STATE]
proof (prove)
using this:
qs = map (\<lambda>i. fill_gholes_gmctxt (Cs ! i) (partition_gholes ds Cs ! i)) [0..<length Cs]

goal (1 subgoal):
 1. (\<And>i. i < length Cs \<Longrightarrow> fill_gholes_gmctxt (Cs ! i) (partition_gholes ds Cs ! i) = qs ! i) &&& length qs = length Cs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?i < length Cs \<Longrightarrow> fill_gholes_gmctxt (Cs ! ?i) (partition_gholes ds Cs ! ?i) = qs ! ?i
length qs = length Cs

goal (2 subgoals):
 1. \<And>x ss. num_gholes (fill_gholes_gmctxt GMHole [x]) = length ss \<Longrightarrow> fill_gholes (fill_gholes_gmctxt GMHole [x]) ss = fill_gholes GMHole (map (\<lambda>i. fill_gholes ([x] ! i) (partition_gholes ss [x] ! i)) [0..<num_gholes GMHole])
 2. \<And>f Cs xs ss. \<lbrakk>sum_list (map num_gholes Cs) = length xs; \<And>i ss. \<lbrakk>i < length Cs; num_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) ss = fill_gholes (Cs ! i) (map (\<lambda>ia. fill_gholes (partition_gholes xs Cs ! i ! ia) (partition_gholes ss (partition_gholes xs Cs ! i) ! ia)) [0..<num_gholes (Cs ! i)]); num_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) ss = fill_gholes (GMFun f Cs) (map (\<lambda>i. fill_gholes (concat (partition_gholes xs Cs) ! i) (partition_gholes ss (concat (partition_gholes xs Cs)) ! i)) [0..<num_gholes (GMFun f Cs)])
[PROOF STEP]
define zs where "zs = map (\<lambda>i. fill_gholes (ds ! i) (partition_gholes ss ds ! i)) [0..<length ds]"
[PROOF STATE]
proof (state)
this:
zs = map (\<lambda>i. fill_gholes (ds ! i) (partition_gholes ss ds ! i)) [0..<length ds]

goal (2 subgoals):
 1. \<And>x ss. num_gholes (fill_gholes_gmctxt GMHole [x]) = length ss \<Longrightarrow> fill_gholes (fill_gholes_gmctxt GMHole [x]) ss = fill_gholes GMHole (map (\<lambda>i. fill_gholes ([x] ! i) (partition_gholes ss [x] ! i)) [0..<num_gholes GMHole])
 2. \<And>f Cs xs ss. \<lbrakk>sum_list (map num_gholes Cs) = length xs; \<And>i ss. \<lbrakk>i < length Cs; num_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) ss = fill_gholes (Cs ! i) (map (\<lambda>ia. fill_gholes (partition_gholes xs Cs ! i ! ia) (partition_gholes ss (partition_gholes xs Cs ! i) ! ia)) [0..<num_gholes (Cs ! i)]); num_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) ss = fill_gholes (GMFun f Cs) (map (\<lambda>i. fill_gholes (concat (partition_gholes xs Cs) ! i) (partition_gholes ss (concat (partition_gholes xs Cs)) ! i)) [0..<num_gholes (GMFun f Cs)])
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
zs = map (\<lambda>i. fill_gholes (ds ! i) (partition_gholes ss ds ! i)) [0..<length ds]

goal (2 subgoals):
 1. \<And>x ss. num_gholes (fill_gholes_gmctxt GMHole [x]) = length ss \<Longrightarrow> fill_gholes (fill_gholes_gmctxt GMHole [x]) ss = fill_gholes GMHole (map (\<lambda>i. fill_gholes ([x] ! i) (partition_gholes ss [x] ! i)) [0..<num_gholes GMHole])
 2. \<And>f Cs xs ss. \<lbrakk>sum_list (map num_gholes Cs) = length xs; \<And>i ss. \<lbrakk>i < length Cs; num_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) ss = fill_gholes (Cs ! i) (map (\<lambda>ia. fill_gholes (partition_gholes xs Cs ! i ! ia) (partition_gholes ss (partition_gholes xs Cs ! i) ! ia)) [0..<num_gholes (Cs ! i)]); num_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) ss = fill_gholes (GMFun f Cs) (map (\<lambda>i. fill_gholes (concat (partition_gholes xs Cs) ! i) (partition_gholes ss (concat (partition_gholes xs Cs)) ! i)) [0..<num_gholes (GMFun f Cs)])
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x ss. num_gholes (fill_gholes_gmctxt GMHole [x]) = length ss \<Longrightarrow> fill_gholes (fill_gholes_gmctxt GMHole [x]) ss = fill_gholes GMHole (map (\<lambda>i. fill_gholes ([x] ! i) (partition_gholes ss [x] ! i)) [0..<num_gholes GMHole])
 2. \<And>f Cs xs ss. \<lbrakk>sum_list (map num_gholes Cs) = length xs; \<And>i ss. \<lbrakk>i < length Cs; num_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) ss = fill_gholes (Cs ! i) (map (\<lambda>ia. fill_gholes (partition_gholes xs Cs ! i ! ia) (partition_gholes ss (partition_gholes xs Cs ! i) ! ia)) [0..<num_gholes (Cs ! i)]); num_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) ss = fill_gholes (GMFun f Cs) (map (\<lambda>i. fill_gholes (concat (partition_gholes xs Cs) ! i) (partition_gholes ss (concat (partition_gholes xs Cs)) ! i)) [0..<num_gholes (GMFun f Cs)])
[PROOF STEP]
assume i: "i < length Cs"
[PROOF STATE]
proof (state)
this:
i < length Cs

goal (2 subgoals):
 1. \<And>x ss. num_gholes (fill_gholes_gmctxt GMHole [x]) = length ss \<Longrightarrow> fill_gholes (fill_gholes_gmctxt GMHole [x]) ss = fill_gholes GMHole (map (\<lambda>i. fill_gholes ([x] ! i) (partition_gholes ss [x] ! i)) [0..<num_gholes GMHole])
 2. \<And>f Cs xs ss. \<lbrakk>sum_list (map num_gholes Cs) = length xs; \<And>i ss. \<lbrakk>i < length Cs; num_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) ss = fill_gholes (Cs ! i) (map (\<lambda>ia. fill_gholes (partition_gholes xs Cs ! i ! ia) (partition_gholes ss (partition_gholes xs Cs ! i) ! ia)) [0..<num_gholes (Cs ! i)]); num_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) ss = fill_gholes (GMFun f Cs) (map (\<lambda>i. fill_gholes (concat (partition_gholes xs Cs) ! i) (partition_gholes ss (concat (partition_gholes xs Cs)) ! i)) [0..<num_gholes (GMFun f Cs)])
[PROOF STEP]
from GMFun(1)
[PROOF STATE]
proof (chain)
picking this:
sum_list (map num_gholes Cs) = length ds
[PROOF STEP]
have *: "map length (partition_gholes ds Cs) = map num_gholes Cs"
[PROOF STATE]
proof (prove)
using this:
sum_list (map num_gholes Cs) = length ds

goal (1 subgoal):
 1. map length (partition_gholes ds Cs) = map num_gholes Cs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map length (partition_gholes ds Cs) = map num_gholes Cs

goal (2 subgoals):
 1. \<And>x ss. num_gholes (fill_gholes_gmctxt GMHole [x]) = length ss \<Longrightarrow> fill_gholes (fill_gholes_gmctxt GMHole [x]) ss = fill_gholes GMHole (map (\<lambda>i. fill_gholes ([x] ! i) (partition_gholes ss [x] ! i)) [0..<num_gholes GMHole])
 2. \<And>f Cs xs ss. \<lbrakk>sum_list (map num_gholes Cs) = length xs; \<And>i ss. \<lbrakk>i < length Cs; num_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) ss = fill_gholes (Cs ! i) (map (\<lambda>ia. fill_gholes (partition_gholes xs Cs ! i ! ia) (partition_gholes ss (partition_gholes xs Cs ! i) ! ia)) [0..<num_gholes (Cs ! i)]); num_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) ss = fill_gholes (GMFun f Cs) (map (\<lambda>i. fill_gholes (concat (partition_gholes xs Cs) ! i) (partition_gholes ss (concat (partition_gholes xs Cs)) ! i)) [0..<num_gholes (GMFun f Cs)])
[PROOF STEP]
have **: "length ss = sum_list (map sum_list (partition_gholes (map num_gholes ds) Cs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ss = sum_list (map sum_list (partition_gholes (map num_gholes ds) Cs))
[PROOF STEP]
using GMFun(1) GMFun(3)[symmetric] num_gholes_fill_gholes_gmctxt[of "GMFun f Cs" ds]
[PROOF STATE]
proof (prove)
using this:
sum_list (map num_gholes Cs) = length ds
length ss = num_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes ds Cs)))
num_gholes (GMFun f Cs) = length ds \<Longrightarrow> num_gholes (fill_gholes_gmctxt (GMFun f Cs) ds) = sum_list (map num_gholes ds)

goal (1 subgoal):
 1. length ss = sum_list (map sum_list (partition_gholes (map num_gholes ds) Cs))
[PROOF STEP]
by (auto simp: comp_def map_map_partition_by[symmetric])
[PROOF STATE]
proof (state)
this:
length ss = sum_list (map sum_list (partition_gholes (map num_gholes ds) Cs))

goal (2 subgoals):
 1. \<And>x ss. num_gholes (fill_gholes_gmctxt GMHole [x]) = length ss \<Longrightarrow> fill_gholes (fill_gholes_gmctxt GMHole [x]) ss = fill_gholes GMHole (map (\<lambda>i. fill_gholes ([x] ! i) (partition_gholes ss [x] ! i)) [0..<num_gholes GMHole])
 2. \<And>f Cs xs ss. \<lbrakk>sum_list (map num_gholes Cs) = length xs; \<And>i ss. \<lbrakk>i < length Cs; num_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) ss = fill_gholes (Cs ! i) (map (\<lambda>ia. fill_gholes (partition_gholes xs Cs ! i ! ia) (partition_gholes ss (partition_gholes xs Cs ! i) ! ia)) [0..<num_gholes (Cs ! i)]); num_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) ss = fill_gholes (GMFun f Cs) (map (\<lambda>i. fill_gholes (concat (partition_gholes xs Cs) ! i) (partition_gholes ss (concat (partition_gholes xs Cs)) ! i)) [0..<num_gholes (GMFun f Cs)])
[PROOF STEP]
have "partition_by (partition_by ss
        (map (\<lambda>i. num_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes ds Cs ! i))) [0..<length Cs]) ! i)
        (partition_gholes (map num_gholes ds) Cs ! i) = partition_gholes (partition_gholes ss ds) Cs ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_by (partition_by ss (map (\<lambda>i. num_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes ds Cs ! i))) [0..<length Cs]) ! i) (partition_gholes (map num_gholes ds) Cs ! i) = partition_gholes (partition_gholes ss ds) Cs ! i
[PROOF STEP]
using i GMFun(1) GMFun(3) partition_by_partition_by[OF **]
[PROOF STATE]
proof (prove)
using this:
i < length Cs
sum_list (map num_gholes Cs) = length ds
num_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes ds Cs))) = length ss
partition_by (partition_by ss (concat (partition_gholes (map num_gholes ds) Cs))) (map length (partition_gholes (map num_gholes ds) Cs)) = map (\<lambda>i. partition_by (partition_by ss (map sum_list (partition_gholes (map num_gholes ds) Cs)) ! i) (partition_gholes (map num_gholes ds) Cs ! i)) [0..<length (partition_gholes (map num_gholes ds) Cs)]

goal (1 subgoal):
 1. partition_by (partition_by ss (map (\<lambda>i. num_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes ds Cs ! i))) [0..<length Cs]) ! i) (partition_gholes (map num_gholes ds) Cs ! i) = partition_gholes (partition_gholes ss ds) Cs ! i
[PROOF STEP]
by (auto simp: comp_def num_gholes_fill_gholes_gmctxt length_partition_by_nth
        intro!: arg_cong[of _ _ "\<lambda>x. partition_by (partition_by ss x ! _) _"] nth_equalityI)
[PROOF STATE]
proof (state)
this:
partition_by (partition_by ss (map (\<lambda>i. num_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes ds Cs ! i))) [0..<length Cs]) ! i) (partition_gholes (map num_gholes ds) Cs ! i) = partition_gholes (partition_gholes ss ds) Cs ! i

goal (2 subgoals):
 1. \<And>x ss. num_gholes (fill_gholes_gmctxt GMHole [x]) = length ss \<Longrightarrow> fill_gholes (fill_gholes_gmctxt GMHole [x]) ss = fill_gholes GMHole (map (\<lambda>i. fill_gholes ([x] ! i) (partition_gholes ss [x] ! i)) [0..<num_gholes GMHole])
 2. \<And>f Cs xs ss. \<lbrakk>sum_list (map num_gholes Cs) = length xs; \<And>i ss. \<lbrakk>i < length Cs; num_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) ss = fill_gholes (Cs ! i) (map (\<lambda>ia. fill_gholes (partition_gholes xs Cs ! i ! ia) (partition_gholes ss (partition_gholes xs Cs ! i) ! ia)) [0..<num_gholes (Cs ! i)]); num_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) ss = fill_gholes (GMFun f Cs) (map (\<lambda>i. fill_gholes (concat (partition_gholes xs Cs) ! i) (partition_gholes ss (concat (partition_gholes xs Cs)) ! i)) [0..<num_gholes (GMFun f Cs)])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
partition_by (partition_by ss (map (\<lambda>i. num_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes ds Cs ! i))) [0..<length Cs]) ! i) (partition_gholes (map num_gholes ds) Cs ! i) = partition_gholes (partition_gholes ss ds) Cs ! i
[PROOF STEP]
have "map (\<lambda>j. fill_gholes (partition_gholes ds Cs ! i ! j)
        (partition_gholes (partition_gholes ss qs ! i)
        (partition_gholes ds Cs ! i) ! j)) [0..<num_gholes (Cs ! i)] =
        partition_gholes zs Cs ! i"
[PROOF STATE]
proof (prove)
using this:
partition_by (partition_by ss (map (\<lambda>i. num_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes ds Cs ! i))) [0..<length Cs]) ! i) (partition_gholes (map num_gholes ds) Cs ! i) = partition_gholes (partition_gholes ss ds) Cs ! i

goal (1 subgoal):
 1. map (\<lambda>j. fill_gholes (partition_gholes ds Cs ! i ! j) (partition_gholes (partition_gholes ss qs ! i) (partition_gholes ds Cs ! i) ! j)) [0..<num_gholes (Cs ! i)] = partition_gholes zs Cs ! i
[PROOF STEP]
using GMFun(1,3)
[PROOF STATE]
proof (prove)
using this:
partition_by (partition_by ss (map (\<lambda>i. num_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes ds Cs ! i))) [0..<length Cs]) ! i) (partition_gholes (map num_gholes ds) Cs ! i) = partition_gholes (partition_gholes ss ds) Cs ! i
sum_list (map num_gholes Cs) = length ds
num_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes ds Cs))) = length ss

goal (1 subgoal):
 1. map (\<lambda>j. fill_gholes (partition_gholes ds Cs ! i ! j) (partition_gholes (partition_gholes ss qs ! i) (partition_gholes ds Cs ! i) ! j)) [0..<num_gholes (Cs ! i)] = partition_gholes zs Cs ! i
[PROOF STEP]
by (auto simp: length_partition_by_nth zs_def qs_def i comp_def partition_by_nth_nth intro: nth_equalityI)
[PROOF STATE]
proof (state)
this:
map (\<lambda>j. fill_gholes (partition_gholes ds Cs ! i ! j) (partition_gholes (partition_gholes ss qs ! i) (partition_gholes ds Cs ! i) ! j)) [0..<num_gholes (Cs ! i)] = partition_gholes zs Cs ! i

goal (2 subgoals):
 1. \<And>x ss. num_gholes (fill_gholes_gmctxt GMHole [x]) = length ss \<Longrightarrow> fill_gholes (fill_gholes_gmctxt GMHole [x]) ss = fill_gholes GMHole (map (\<lambda>i. fill_gholes ([x] ! i) (partition_gholes ss [x] ! i)) [0..<num_gholes GMHole])
 2. \<And>f Cs xs ss. \<lbrakk>sum_list (map num_gholes Cs) = length xs; \<And>i ss. \<lbrakk>i < length Cs; num_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (Cs ! i) (partition_gholes xs Cs ! i)) ss = fill_gholes (Cs ! i) (map (\<lambda>ia. fill_gholes (partition_gholes xs Cs ! i ! ia) (partition_gholes ss (partition_gholes xs Cs ! i) ! ia)) [0..<num_gholes (Cs ! i)]); num_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) = length ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes xs Cs))) ss = fill_gholes (GMFun f Cs) (map (\<lambda>i. fill_gholes (concat (partition_gholes xs Cs) ! i) (partition_gholes ss (concat (partition_gholes xs Cs)) ! i)) [0..<num_gholes (GMFun f Cs)])
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i2 < length Cs \<Longrightarrow> map (\<lambda>j. fill_gholes (partition_gholes ds Cs ! ?i2 ! j) (partition_gholes (partition_gholes ss qs ! ?i2) (partition_gholes ds Cs ! ?i2) ! j)) [0..<num_gholes (Cs ! ?i2)] = partition_gholes zs Cs ! ?i2

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

goal (1 subgoal):
 1. fill_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes ds Cs))) ss = fill_gholes (GMFun f Cs) (map (\<lambda>i. fill_gholes (concat (partition_gholes ds Cs) ! i) (partition_gholes ss (concat (partition_gholes ds Cs)) ! i)) [0..<num_gholes (GMFun f Cs)])
[PROOF STEP]
using GMFun
[PROOF STATE]
proof (prove)
using this:
?i2 < length Cs \<Longrightarrow> map (\<lambda>j. fill_gholes (partition_gholes ds Cs ! ?i2 ! j) (partition_gholes (partition_gholes ss qs ! ?i2) (partition_gholes ds Cs ! ?i2) ! j)) [0..<num_gholes (Cs ! ?i2)] = partition_gholes zs Cs ! ?i2
sum_list (map num_gholes Cs) = length ds
\<lbrakk>?i < length Cs; num_gholes (fill_gholes_gmctxt (Cs ! ?i) (partition_gholes ds Cs ! ?i)) = length ?ss\<rbrakk> \<Longrightarrow> fill_gholes (fill_gholes_gmctxt (Cs ! ?i) (partition_gholes ds Cs ! ?i)) ?ss = fill_gholes (Cs ! ?i) (map (\<lambda>i. fill_gholes (partition_gholes ds Cs ! ?i ! i) (partition_gholes ?ss (partition_gholes ds Cs ! ?i) ! i)) [0..<num_gholes (Cs ! ?i)])
num_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes ds Cs))) = length ss

goal (1 subgoal):
 1. fill_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes ds Cs))) ss = fill_gholes (GMFun f Cs) (map (\<lambda>i. fill_gholes (concat (partition_gholes ds Cs) ! i) (partition_gholes ss (concat (partition_gholes ds Cs)) ! i)) [0..<num_gholes (GMFun f Cs)])
[PROOF STEP]
by (simp add: qs_def [symmetric] qs zs_def [symmetric] length_partition_by_nth)
[PROOF STATE]
proof (state)
this:
fill_gholes (fill_gholes_gmctxt (GMFun f Cs) (concat (partition_gholes ds Cs))) ss = fill_gholes (GMFun f Cs) (map (\<lambda>i. fill_gholes (concat (partition_gholes ds Cs) ! i) (partition_gholes ss (concat (partition_gholes ds Cs)) ! i)) [0..<num_gholes (GMFun f Cs)])

goal (1 subgoal):
 1. \<And>x ss. num_gholes (fill_gholes_gmctxt GMHole [x]) = length ss \<Longrightarrow> fill_gholes (fill_gholes_gmctxt GMHole [x]) ss = fill_gholes GMHole (map (\<lambda>i. fill_gholes ([x] ! i) (partition_gholes ss [x] ! i)) [0..<num_gholes GMHole])
[PROOF STEP]
qed auto


[STATEMENT]
lemma fill_gholes_gmctxt_sound:
  assumes len_ds: "length Ds = num_gholes C"
  and len_sss: "length sss = num_gholes C"
  and len_ts: "length ts = num_gholes C"
  and insts: "\<And> i. i < length Ds \<Longrightarrow> ts ! i =\<^sub>G\<^sub>f (Ds ! i, sss ! i)"
  shows "fill_gholes C ts =\<^sub>G\<^sub>f (fill_gholes_gmctxt C Ds, concat sss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_gholes C ts =\<^sub>G\<^sub>f (fill_gholes_gmctxt C Ds, concat sss)
[PROOF STEP]
proof (rule eqfI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fill_gholes C ts = fill_gholes (fill_gholes_gmctxt C Ds) (concat sss)
 2. num_gholes (fill_gholes_gmctxt C Ds) = length (concat sss)
[PROOF STEP]
note l_nh_i = eqgfE(2)[OF insts]
[PROOF STATE]
proof (state)
this:
?i1 < length Ds \<Longrightarrow> num_gholes (Ds ! ?i1) = length (sss ! ?i1)

goal (2 subgoals):
 1. fill_gholes C ts = fill_gholes (fill_gholes_gmctxt C Ds) (concat sss)
 2. num_gholes (fill_gholes_gmctxt C Ds) = length (concat sss)
[PROOF STEP]
from len_ds len_sss
[PROOF STATE]
proof (chain)
picking this:
length Ds = num_gholes C
length sss = num_gholes C
[PROOF STEP]
have concat_sss: "partition_gholes (concat sss) Ds = sss"
[PROOF STATE]
proof (prove)
using this:
length Ds = num_gholes C
length sss = num_gholes C

goal (1 subgoal):
 1. partition_gholes (concat sss) Ds = sss
[PROOF STEP]
by (metis l_nh_i length_map map_nth_eq_conv partition_by_concat_id)
[PROOF STATE]
proof (state)
this:
partition_gholes (concat sss) Ds = sss

goal (2 subgoals):
 1. fill_gholes C ts = fill_gholes (fill_gholes_gmctxt C Ds) (concat sss)
 2. num_gholes (fill_gholes_gmctxt C Ds) = length (concat sss)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
partition_gholes (concat sss) Ds = sss
[PROOF STEP]
show nh: "num_gholes (fill_gholes_gmctxt C Ds) = length (concat sss)"
[PROOF STATE]
proof (prove)
using this:
partition_gholes (concat sss) Ds = sss

goal (1 subgoal):
 1. num_gholes (fill_gholes_gmctxt C Ds) = length (concat sss)
[PROOF STEP]
unfolding num_gholes_fill_gholes_gmctxt [OF len_ds [symmetric]] length_concat
[PROOF STATE]
proof (prove)
using this:
partition_gholes (concat sss) Ds = sss

goal (1 subgoal):
 1. sum_list (map num_gholes Ds) = sum_list (map length sss)
[PROOF STEP]
by (metis l_nh_i len_ds len_sss nth_map_conv)
[PROOF STATE]
proof (state)
this:
num_gholes (fill_gholes_gmctxt C Ds) = length (concat sss)

goal (1 subgoal):
 1. fill_gholes C ts = fill_gholes (fill_gholes_gmctxt C Ds) (concat sss)
[PROOF STEP]
have ts: "ts = [fill_gholes (Ds ! i) (partition_gholes (concat sss) Ds ! i) . i \<leftarrow> [0..<num_gholes C]]" (is "_ = ?fhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts = map (\<lambda>i. fill_gholes (Ds ! i) (partition_gholes (concat sss) Ds ! i)) [0..<num_gholes C]
[PROOF STEP]
proof (rule nth_equalityI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. length ts = length (map (\<lambda>i. fill_gholes (Ds ! i) (partition_gholes (concat sss) Ds ! i)) [0..<num_gholes C])
 2. \<And>i. i < length ts \<Longrightarrow> ts ! i = map (\<lambda>i. fill_gholes (Ds ! i) (partition_gholes (concat sss) Ds ! i)) [0..<num_gholes C] ! i
[PROOF STEP]
show l_fhs: "length ts = length ?fhs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ts = length (map (\<lambda>i. fill_gholes (Ds ! i) (partition_gholes (concat sss) Ds ! i)) [0..<num_gholes C])
[PROOF STEP]
unfolding length_map
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ts = length [0..<num_gholes C]
[PROOF STEP]
by (metis diff_zero len_ts length_upt)
[PROOF STATE]
proof (state)
this:
length ts = length (map (\<lambda>i. fill_gholes (Ds ! i) (partition_gholes (concat sss) Ds ! i)) [0..<num_gholes C])

goal (1 subgoal):
 1. \<And>i. i < length ts \<Longrightarrow> ts ! i = map (\<lambda>i. fill_gholes (Ds ! i) (partition_gholes (concat sss) Ds ! i)) [0..<num_gholes C] ! i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < length ts \<Longrightarrow> ts ! i = map (\<lambda>i. fill_gholes (Ds ! i) (partition_gholes (concat sss) Ds ! i)) [0..<num_gholes C] ! i
[PROOF STEP]
assume i: "i < length ts"
[PROOF STATE]
proof (state)
this:
i < length ts

goal (1 subgoal):
 1. \<And>i. i < length ts \<Longrightarrow> ts ! i = map (\<lambda>i. fill_gholes (Ds ! i) (partition_gholes (concat sss) Ds ! i)) [0..<num_gholes C] ! i
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length ts
[PROOF STEP]
have i': "i < length [0..<num_gholes C]"
[PROOF STATE]
proof (prove)
using this:
i < length ts

goal (1 subgoal):
 1. i < length [0..<num_gholes C]
[PROOF STEP]
by (metis diff_zero len_ts length_upt)
[PROOF STATE]
proof (state)
this:
i < length [0..<num_gholes C]

goal (1 subgoal):
 1. \<And>i. i < length ts \<Longrightarrow> ts ! i = map (\<lambda>i. fill_gholes (Ds ! i) (partition_gholes (concat sss) Ds ! i)) [0..<num_gholes C] ! i
[PROOF STEP]
show "ts!i = ?fhs ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts ! i = map (\<lambda>i. fill_gholes (Ds ! i) (partition_gholes (concat sss) Ds ! i)) [0..<num_gholes C] ! i
[PROOF STEP]
unfolding nth_map[OF i']
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ts ! i = fill_gholes (Ds ! ([0..<num_gholes C] ! i)) (partition_gholes (concat sss) Ds ! ([0..<num_gholes C] ! i))
[PROOF STEP]
using eqgfE(1)[OF insts[unfolded len_ds, OF i[unfolded len_ts]]]
[PROOF STATE]
proof (prove)
using this:
ts ! i = fill_gholes (Ds ! i) (sss ! i)

goal (1 subgoal):
 1. ts ! i = fill_gholes (Ds ! ([0..<num_gholes C] ! i)) (partition_gholes (concat sss) Ds ! ([0..<num_gholes C] ! i))
[PROOF STEP]
by (metis concat_sss i' len_ds len_sss map_nth nth_map)
[PROOF STATE]
proof (state)
this:
ts ! i = map (\<lambda>i. fill_gholes (Ds ! i) (partition_gholes (concat sss) Ds ! i)) [0..<num_gholes C] ! i

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
ts = map (\<lambda>i. fill_gholes (Ds ! i) (partition_gholes (concat sss) Ds ! i)) [0..<num_gholes C]

goal (1 subgoal):
 1. fill_gholes C ts = fill_gholes (fill_gholes_gmctxt C Ds) (concat sss)
[PROOF STEP]
note ts = this
[PROOF STATE]
proof (state)
this:
ts = map (\<lambda>i. fill_gholes (Ds ! i) (partition_gholes (concat sss) Ds ! i)) [0..<num_gholes C]

goal (1 subgoal):
 1. fill_gholes C ts = fill_gholes (fill_gholes_gmctxt C Ds) (concat sss)
[PROOF STEP]
show "fill_gholes C ts = fill_gholes (fill_gholes_gmctxt C Ds) (concat sss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_gholes C ts = fill_gholes (fill_gholes_gmctxt C Ds) (concat sss)
[PROOF STEP]
unfolding fill_gholes_gmctxt_fill_gholes[OF len_ds nh] ts
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_gholes C (map (\<lambda>i. fill_gholes (Ds ! i) (partition_gholes (concat sss) Ds ! i)) [0..<num_gholes C]) = fill_gholes C (map (\<lambda>i. fill_gholes (Ds ! i) (partition_gholes (concat sss) Ds ! i)) [0..<num_gholes C])
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
fill_gholes C ts = fill_gholes (fill_gholes_gmctxt C Ds) (concat sss)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inf_gmctxt_idem [simp]:
  "(C :: 'f gmctxt) \<sqinter> C = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<sqinter> C = C
[PROOF STEP]
by (induct C) (auto simp: zip_same_conv_map intro: map_idI)


[STATEMENT]
lemma inf_gmctxt_GMHole2 [simp]:
  "C \<sqinter> GMHole = GMHole"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<sqinter> GMHole = GMHole
[PROOF STEP]
by (induct C) simp_all


[STATEMENT]
lemma inf_gmctxt_comm [ac_simps]:
  "(C :: 'f gmctxt) \<sqinter> D = D \<sqinter> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<sqinter> D = D \<sqinter> C
[PROOF STEP]
by (induct C D rule: inf_gmctxt.induct) (fastforce simp: in_set_conv_nth intro!: nth_equalityI)+


[STATEMENT]
lemma inf_gmctxt_assoc [ac_simps]:
  fixes C :: "'f gmctxt"
  shows "C \<sqinter> D \<sqinter> E = C \<sqinter> (D \<sqinter> E)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<sqinter> D \<sqinter> E = C \<sqinter> (D \<sqinter> E)
[PROOF STEP]
apply (induct C D arbitrary: E rule: inf_gmctxt.induct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>D E. GMHole \<sqinter> D \<sqinter> E = GMHole \<sqinter> (D \<sqinter> E)
 2. \<And>v va E. GMFun v va \<sqinter> GMHole \<sqinter> E = GMFun v va \<sqinter> (GMHole \<sqinter> E)
 3. \<And>f Cs g Ds E. (\<And>x xa y E. \<lbrakk>f = g \<and> length Cs = length Ds; x \<in> set (zip Cs Ds); (xa, y) = x\<rbrakk> \<Longrightarrow> xa \<sqinter> y \<sqinter> E = xa \<sqinter> (y \<sqinter> E)) \<Longrightarrow> GMFun f Cs \<sqinter> GMFun g Ds \<sqinter> E = GMFun f Cs \<sqinter> (GMFun g Ds \<sqinter> E)
[PROOF STEP]
apply (auto)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Cs g Ds E. \<lbrakk>\<And>a b xa E. \<lbrakk>(a, b) \<in> set (zip Cs Ds); xa = a\<rbrakk> \<Longrightarrow> a \<sqinter> b \<sqinter> E = a \<sqinter> (b \<sqinter> E); length Cs = length Ds\<rbrakk> \<Longrightarrow> GMFun g (map2 (\<sqinter>) Cs Ds) \<sqinter> E = GMFun g Cs \<sqinter> (GMFun g Ds \<sqinter> E)
 2. \<And>f Cs g Ds E. f \<noteq> g \<Longrightarrow> GMHole = GMFun f Cs \<sqinter> (GMFun g Ds \<sqinter> E)
 3. \<And>f Cs g Ds E. length Cs \<noteq> length Ds \<Longrightarrow> GMHole = GMFun f Cs \<sqinter> (GMFun g Ds \<sqinter> E)
[PROOF STEP]
apply (case_tac E, auto)+
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Cs Ds x22. \<lbrakk>\<And>a b xa E. \<lbrakk>(a, b) \<in> set (zip Cs Ds); xa = a\<rbrakk> \<Longrightarrow> a \<sqinter> b \<sqinter> E = a \<sqinter> (b \<sqinter> E); length Cs = length x22; length Ds = length x22\<rbrakk> \<Longrightarrow> map2 (\<sqinter>) (map2 (\<sqinter>) Cs Ds) x22 = map2 (\<sqinter>) Cs (map2 (\<sqinter>) Ds x22)
 2. \<And>f Cs g Ds E. f \<noteq> g \<Longrightarrow> GMHole = GMFun f Cs \<sqinter> (GMFun g Ds \<sqinter> E)
 3. \<And>f Cs g Ds E. length Cs \<noteq> length Ds \<Longrightarrow> GMHole = GMFun f Cs \<sqinter> (GMFun g Ds \<sqinter> E)
[PROOF STEP]
apply (fastforce simp: in_set_conv_nth intro!: nth_equalityI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>f Cs g Ds E. f \<noteq> g \<Longrightarrow> GMHole = GMFun f Cs \<sqinter> (GMFun g Ds \<sqinter> E)
 2. \<And>f Cs g Ds E. length Cs \<noteq> length Ds \<Longrightarrow> GMHole = GMFun f Cs \<sqinter> (GMFun g Ds \<sqinter> E)
[PROOF STEP]
apply (case_tac E, auto)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma less_eq_gmctxt_prime: "C \<le> D \<longleftrightarrow> less_eq_gmctxt C D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C \<le> D) = less_eq_gmctxt C D
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. C \<le> D \<Longrightarrow> less_eq_gmctxt C D
 2. less_eq_gmctxt C D \<Longrightarrow> C \<le> D
[PROOF STEP]
assume "less_eq_gmctxt C D"
[PROOF STATE]
proof (state)
this:
less_eq_gmctxt C D

goal (2 subgoals):
 1. C \<le> D \<Longrightarrow> less_eq_gmctxt C D
 2. less_eq_gmctxt C D \<Longrightarrow> C \<le> D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
less_eq_gmctxt C D
[PROOF STEP]
show "C \<le> D"
[PROOF STATE]
proof (prove)
using this:
less_eq_gmctxt C D

goal (1 subgoal):
 1. C \<le> D
[PROOF STEP]
by (induct C D rule: less_eq_gmctxt.induct) (auto simp: less_eq_gmctxt_def intro: nth_equalityI)
[PROOF STATE]
proof (state)
this:
C \<le> D

goal (1 subgoal):
 1. C \<le> D \<Longrightarrow> less_eq_gmctxt C D
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C \<le> D \<Longrightarrow> less_eq_gmctxt C D
[PROOF STEP]
assume "C \<le> D"
[PROOF STATE]
proof (state)
this:
C \<le> D

goal (1 subgoal):
 1. C \<le> D \<Longrightarrow> less_eq_gmctxt C D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<le> D
[PROOF STEP]
show "less_eq_gmctxt C D"
[PROOF STATE]
proof (prove)
using this:
C \<le> D

goal (1 subgoal):
 1. less_eq_gmctxt C D
[PROOF STEP]
unfolding less_eq_gmctxt_def
[PROOF STATE]
proof (prove)
using this:
C \<sqinter> D = C

goal (1 subgoal):
 1. less_eq_gmctxt C D
[PROOF STEP]
by (induct C D rule: inf_gmctxt.induct)
     (auto split: if_splits simp: set_zip intro!: less_eq_gmctxt.intros nth_equalityI elim!: nth_equalityE, metis)
[PROOF STATE]
proof (state)
this:
less_eq_gmctxt C D

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma  less_eq_gmctxt_Hole:
  "less_eq_gmctxt C GMHole \<Longrightarrow> C = GMHole"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. less_eq_gmctxt C GMHole \<Longrightarrow> C = GMHole
[PROOF STEP]
using less_eq_gmctxt.cases
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>less_eq_gmctxt ?a1.0 ?a2.0; \<And>u. \<lbrakk>?a1.0 = GMHole; ?a2.0 = u\<rbrakk> \<Longrightarrow> ?P; \<And>cs ds f. \<lbrakk>?a1.0 = GMFun f cs; ?a2.0 = GMFun f ds; length cs = length ds; \<And>i. i < length cs \<Longrightarrow> less_eq_gmctxt (cs ! i) (ds ! i)\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. less_eq_gmctxt C GMHole \<Longrightarrow> C = GMHole
[PROOF STEP]
by blast


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

goal (2 subgoals):
 1. \<And>D. 0 < num_gholes GMHole \<Longrightarrow> 0 < num_gholes (GMHole \<sqinter> D)
 2. \<And>x1 x2 D. \<lbrakk>\<And>x2a D. \<lbrakk>x2a \<in> set x2; 0 < num_gholes x2a\<rbrakk> \<Longrightarrow> 0 < num_gholes (x2a \<sqinter> D); 0 < num_gholes (GMFun x1 x2)\<rbrakk> \<Longrightarrow> 0 < num_gholes (GMFun x1 x2 \<sqinter> D)
[PROOF STEP]
from GMFun(2)
[PROOF STATE]
proof (chain)
picking this:
0 < num_gholes (GMFun f Cs)
[PROOF STEP]
obtain i where wit: "i < length Cs" "0 < num_gholes (Cs ! i)"
[PROOF STATE]
proof (prove)
using this:
0 < num_gholes (GMFun f Cs)

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < length Cs; 0 < num_gholes (Cs ! i)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto, metis (mono_tags, lifting) in_set_conv_nth length_map map_nth_eq_conv not_less sum_list_nonpos)
[PROOF STATE]
proof (state)
this:
i < length Cs
0 < num_gholes (Cs ! i)

goal (2 subgoals):
 1. \<And>D. 0 < num_gholes GMHole \<Longrightarrow> 0 < num_gholes (GMHole \<sqinter> D)
 2. \<And>x1 x2 D. \<lbrakk>\<And>x2a D. \<lbrakk>x2a \<in> set x2; 0 < num_gholes x2a\<rbrakk> \<Longrightarrow> 0 < num_gholes (x2a \<sqinter> D); 0 < num_gholes (GMFun x1 x2)\<rbrakk> \<Longrightarrow> 0 < num_gholes (GMFun x1 x2 \<sqinter> D)
[PROOF STEP]
note IS = GMFun(1)[OF nth_mem, OF wit]
[PROOF STATE]
proof (state)
this:
0 < num_gholes (Cs ! i \<sqinter> ?D)

goal (2 subgoals):
 1. \<And>D. 0 < num_gholes GMHole \<Longrightarrow> 0 < num_gholes (GMHole \<sqinter> D)
 2. \<And>x1 x2 D. \<lbrakk>\<And>x2a D. \<lbrakk>x2a \<in> set x2; 0 < num_gholes x2a\<rbrakk> \<Longrightarrow> 0 < num_gholes (x2a \<sqinter> D); 0 < num_gholes (GMFun x1 x2)\<rbrakk> \<Longrightarrow> 0 < num_gholes (GMFun x1 x2 \<sqinter> D)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < num_gholes (GMFun f Cs \<sqinter> D)
[PROOF STEP]
proof (cases D)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. D = GMHole \<Longrightarrow> 0 < num_gholes (GMFun f Cs \<sqinter> D)
 2. \<And>x21 x22. D = GMFun x21 x22 \<Longrightarrow> 0 < num_gholes (GMFun f Cs \<sqinter> D)
[PROOF STEP]
case [simp]: (GMFun g Ds)
[PROOF STATE]
proof (state)
this:
D = GMFun g Ds

goal (2 subgoals):
 1. D = GMHole \<Longrightarrow> 0 < num_gholes (GMFun f Cs \<sqinter> D)
 2. \<And>x21 x22. D = GMFun x21 x22 \<Longrightarrow> 0 < num_gholes (GMFun f Cs \<sqinter> D)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
D = GMFun g Ds

goal (2 subgoals):
 1. D = GMHole \<Longrightarrow> 0 < num_gholes (GMFun f Cs \<sqinter> D)
 2. \<And>x21 x22. D = GMFun x21 x22 \<Longrightarrow> 0 < num_gholes (GMFun f Cs \<sqinter> D)
[PROOF STEP]
assume "f = g" "length Cs = length Ds"
[PROOF STATE]
proof (state)
this:
f = g
length Cs = length Ds

goal (2 subgoals):
 1. D = GMHole \<Longrightarrow> 0 < num_gholes (GMFun f Cs \<sqinter> D)
 2. \<And>x21 x22. D = GMFun x21 x22 \<Longrightarrow> 0 < num_gholes (GMFun f Cs \<sqinter> D)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f = g
length Cs = length Ds
[PROOF STEP]
have "0 < num_gholes (Cs ! i \<sqinter> Ds ! i)"
[PROOF STATE]
proof (prove)
using this:
f = g
length Cs = length Ds

goal (1 subgoal):
 1. 0 < num_gholes (Cs ! i \<sqinter> Ds ! i)
[PROOF STEP]
using IS[of "Ds ! i"]
[PROOF STATE]
proof (prove)
using this:
f = g
length Cs = length Ds
0 < num_gholes (Cs ! i \<sqinter> Ds ! i)

goal (1 subgoal):
 1. 0 < num_gholes (Cs ! i \<sqinter> Ds ! i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
0 < num_gholes (Cs ! i \<sqinter> Ds ! i)

goal (2 subgoals):
 1. D = GMHole \<Longrightarrow> 0 < num_gholes (GMFun f Cs \<sqinter> D)
 2. \<And>x21 x22. D = GMFun x21 x22 \<Longrightarrow> 0 < num_gholes (GMFun f Cs \<sqinter> D)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<lbrakk>f = g; length Cs = length Ds\<rbrakk> \<Longrightarrow> 0 < num_gholes (Cs ! i \<sqinter> Ds ! i)

goal (2 subgoals):
 1. D = GMHole \<Longrightarrow> 0 < num_gholes (GMFun f Cs \<sqinter> D)
 2. \<And>x21 x22. D = GMFun x21 x22 \<Longrightarrow> 0 < num_gholes (GMFun f Cs \<sqinter> D)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>f = g; length Cs = length Ds\<rbrakk> \<Longrightarrow> 0 < num_gholes (Cs ! i \<sqinter> Ds ! i)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>f = g; length Cs = length Ds\<rbrakk> \<Longrightarrow> 0 < num_gholes (Cs ! i \<sqinter> Ds ! i)

goal (1 subgoal):
 1. 0 < num_gholes (GMFun f Cs \<sqinter> D)
[PROOF STEP]
using wit(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>f = g; length Cs = length Ds\<rbrakk> \<Longrightarrow> 0 < num_gholes (Cs ! i \<sqinter> Ds ! i)
i < length Cs

goal (1 subgoal):
 1. 0 < num_gholes (GMFun f Cs \<sqinter> D)
[PROOF STEP]
by (auto simp:  split!: prod.splits)
         (smt (verit, del_insts) length_map length_zip map_nth_eq_conv min_less_iff_conj not_gr0 nth_mem nth_zip o_apply prod.simps(2) sum_list_eq_0_iff)
[PROOF STATE]
proof (state)
this:
0 < num_gholes (GMFun f Cs \<sqinter> D)

goal (1 subgoal):
 1. D = GMHole \<Longrightarrow> 0 < num_gholes (GMFun f Cs \<sqinter> D)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
0 < num_gholes (GMFun f Cs \<sqinter> D)

goal (1 subgoal):
 1. \<And>D. 0 < num_gholes GMHole \<Longrightarrow> 0 < num_gholes (GMHole \<sqinter> D)
[PROOF STEP]
qed auto


[STATEMENT]
lemma sup_gmctxt_idem [simp]:
  fixes C :: "'f gmctxt"
  shows "C \<squnion> C = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<squnion> C = C
[PROOF STEP]
by (induct C) (auto simp: zip_same_conv_map intro: map_idI)


[STATEMENT]
lemma sup_gmctxt_MHole [simp]: "C \<squnion> GMHole = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<squnion> GMHole = C
[PROOF STEP]
by (induct C) simp_all


[STATEMENT]
lemma sup_gmctxt_comm [ac_simps]:
  fixes C :: "'f gmctxt"
  shows "C \<squnion> D = D \<squnion> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<squnion> D = D \<squnion> C
[PROOF STEP]
by (induct C D rule: sup_gmctxt.induct) (fastforce simp: in_set_conv_nth intro!: nth_equalityI)+


[STATEMENT]
lemma comp_gmctxt_refl:
  "(C, C) \<in> comp_gmctxt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C, C) \<in> comp_gmctxt
[PROOF STEP]
by (induct C) auto


[STATEMENT]
lemma comp_gmctxt_sym:
  assumes "(C, D) \<in> comp_gmctxt"
  shows "(D, C) \<in> comp_gmctxt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (D, C) \<in> comp_gmctxt
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(C, D) \<in> comp_gmctxt

goal (1 subgoal):
 1. (D, C) \<in> comp_gmctxt
[PROOF STEP]
by (induct) auto


[STATEMENT]
lemma sup_gmctxt_assoc [ac_simps]:
  assumes "(C, D) \<in> comp_gmctxt" and "(D, E) \<in> comp_gmctxt"
  shows "C \<squnion> D \<squnion> E = C \<squnion> (D \<squnion> E)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<squnion> D \<squnion> E = C \<squnion> (D \<squnion> E)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(C, D) \<in> comp_gmctxt
(D, E) \<in> comp_gmctxt

goal (1 subgoal):
 1. C \<squnion> D \<squnion> E = C \<squnion> (D \<squnion> E)
[PROOF STEP]
by (induct C D arbitrary: E) (auto elim!: comp_gmctxt.cases intro!: nth_equalityI)


[STATEMENT]
lemma sup_gmctxt_ge1 [simp]:
  assumes "(C, D) \<in> comp_gmctxt"
  shows "C \<le> C \<squnion> D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<le> C \<squnion> D
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(C, D) \<in> comp_gmctxt

goal (1 subgoal):
 1. C \<le> C \<squnion> D
[PROOF STEP]
by (induct C D) (auto simp: less_eq_gmctxt_def intro: nth_equalityI)


[STATEMENT]
lemma sup_gmctxt_ge2 [simp]:
  assumes "(C, D) \<in> comp_gmctxt"
  shows "D \<le> C \<squnion> D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D \<le> C \<squnion> D
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(C, D) \<in> comp_gmctxt

goal (1 subgoal):
 1. D \<le> C \<squnion> D
[PROOF STEP]
by (induct) (auto simp: less_eq_gmctxt_def intro: nth_equalityI)


[STATEMENT]
lemma sup_gmctxt_least:
  assumes "(D, E) \<in> comp_gmctxt"
    and "D \<le> C" and "E \<le> C"
  shows "D \<squnion> E \<le> C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. D \<squnion> E \<le> C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(D, E) \<in> comp_gmctxt
D \<le> C
E \<le> C

goal (1 subgoal):
 1. D \<squnion> E \<le> C
[PROOF STEP]
apply (induct arbitrary: C)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>D C. \<lbrakk>GMHole \<le> C; D \<le> C\<rbrakk> \<Longrightarrow> GMHole \<squnion> D \<le> C
 2. \<And>C Ca. \<lbrakk>C \<le> Ca; GMHole \<le> Ca\<rbrakk> \<Longrightarrow> C \<squnion> GMHole \<le> Ca
 3. \<And>f g Cs Ds C. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> (\<forall>x\<ge>Cs ! i. Ds ! i \<le> x \<longrightarrow> Cs ! i \<squnion> Ds ! i \<le> x); GMFun f Cs \<le> C; GMFun g Ds \<le> C\<rbrakk> \<Longrightarrow> GMFun f Cs \<squnion> GMFun g Ds \<le> C
[PROOF STEP]
apply (auto simp: less_eq_gmctxt_def elim!: inf_gmctxt.elims intro!: nth_equalityI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>Csa Csb Dsb i. \<lbrakk>length Csa = length Dsb; \<forall>i<length Dsb. (Csa ! i, Csb ! i) \<in> comp_gmctxt \<and> (\<forall>x. Csa ! i \<sqinter> x = Csa ! i \<longrightarrow> Csb ! i \<sqinter> x = Csb ! i \<longrightarrow> (Csa ! i \<squnion> Csb ! i) \<sqinter> x = Csa ! i \<squnion> Csb ! i); Csa = map2 (\<sqinter>) Csa Dsb; Csb = map2 (\<sqinter>) Csb Dsb; length Csb = length Dsb; i < length Dsb\<rbrakk> \<Longrightarrow> (Csa ! i \<squnion> Csb ! i) \<sqinter> Dsb ! i = Csa ! i \<squnion> Csb ! i
 2. \<And>Csa fb Csb gb Dsb. \<lbrakk>length Csa = length Csb; \<forall>i<length Csb. (Csa ! i, Csb ! i) \<in> comp_gmctxt \<and> (\<forall>x. Csa ! i \<sqinter> x = Csa ! i \<longrightarrow> Csb ! i \<sqinter> x = Csb ! i \<longrightarrow> (Csa ! i \<squnion> Csb ! i) \<sqinter> x = Csa ! i \<squnion> Csb ! i); GMFun fb Csa = (if fb = gb \<and> length Csb = length Dsb then GMFun fb (map2 (\<sqinter>) Csa Dsb) else GMHole); GMFun fb Csb = (if fb = gb \<and> length Csb = length Dsb then GMFun fb (map2 (\<sqinter>) Csb Dsb) else GMHole)\<rbrakk> \<Longrightarrow> fb = gb
 3. \<And>Csa fb Csb gb Dsb. \<lbrakk>length Csa = length Csb; \<forall>i<length Csb. (Csa ! i, Csb ! i) \<in> comp_gmctxt \<and> (\<forall>x. Csa ! i \<sqinter> x = Csa ! i \<longrightarrow> Csb ! i \<sqinter> x = Csb ! i \<longrightarrow> (Csa ! i \<squnion> Csb ! i) \<sqinter> x = Csa ! i \<squnion> Csb ! i); GMFun fb Csa = (if fb = gb \<and> length Csb = length Dsb then GMFun fb (map2 (\<sqinter>) Csa Dsb) else GMHole); GMFun fb Csb = (if fb = gb \<and> length Csb = length Dsb then GMFun fb (map2 (\<sqinter>) Csb Dsb) else GMHole)\<rbrakk> \<Longrightarrow> length Csb = length Dsb
[PROOF STEP]
apply (metis (erased, lifting) length_map nth_map nth_zip split_conv)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>Csa fb Csb gb Dsb. \<lbrakk>length Csa = length Csb; \<forall>i<length Csb. (Csa ! i, Csb ! i) \<in> comp_gmctxt \<and> (\<forall>x. Csa ! i \<sqinter> x = Csa ! i \<longrightarrow> Csb ! i \<sqinter> x = Csb ! i \<longrightarrow> (Csa ! i \<squnion> Csb ! i) \<sqinter> x = Csa ! i \<squnion> Csb ! i); GMFun fb Csa = (if fb = gb \<and> length Csb = length Dsb then GMFun fb (map2 (\<sqinter>) Csa Dsb) else GMHole); GMFun fb Csb = (if fb = gb \<and> length Csb = length Dsb then GMFun fb (map2 (\<sqinter>) Csb Dsb) else GMHole)\<rbrakk> \<Longrightarrow> fb = gb
 2. \<And>Csa fb Csb gb Dsb. \<lbrakk>length Csa = length Csb; \<forall>i<length Csb. (Csa ! i, Csb ! i) \<in> comp_gmctxt \<and> (\<forall>x. Csa ! i \<sqinter> x = Csa ! i \<longrightarrow> Csb ! i \<sqinter> x = Csb ! i \<longrightarrow> (Csa ! i \<squnion> Csb ! i) \<sqinter> x = Csa ! i \<squnion> Csb ! i); GMFun fb Csa = (if fb = gb \<and> length Csb = length Dsb then GMFun fb (map2 (\<sqinter>) Csa Dsb) else GMHole); GMFun fb Csb = (if fb = gb \<and> length Csb = length Dsb then GMFun fb (map2 (\<sqinter>) Csb Dsb) else GMHole)\<rbrakk> \<Longrightarrow> length Csb = length Dsb
[PROOF STEP]
apply (case_tac "fb = gb \<and> length Csb = length Dsb", simp_all)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma sup_gmctxt_args_MHole2 [simp]:
  "sup_gmctxt_args C GMHole = replicate (num_gholes C) GMHole"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sup_gmctxt_args C GMHole = replicate (num_gholes C) GMHole
[PROOF STEP]
by (cases C) simp_all


[STATEMENT]
lemma num_gholes_sup_gmctxt_args:
  assumes "(C, D) \<in> comp_gmctxt"
  shows "num_gholes C = length (sup_gmctxt_args C D)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes C = length (sup_gmctxt_args C D)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(C, D) \<in> comp_gmctxt

goal (1 subgoal):
 1. num_gholes C = length (sup_gmctxt_args C D)
[PROOF STEP]
by (induct) (auto simp: length_concat intro!: arg_cong [of _ _ sum_list] nth_equalityI)


[STATEMENT]
lemma sup_gmctxt_sup_gmctxt_args:
  assumes "(C, D) \<in> comp_gmctxt"
  shows "fill_gholes_gmctxt C (sup_gmctxt_args C D) = C \<squnion> D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_gholes_gmctxt C (sup_gmctxt_args C D) = C \<squnion> D
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(C, D) \<in> comp_gmctxt

goal (1 subgoal):
 1. fill_gholes_gmctxt C (sup_gmctxt_args C D) = C \<squnion> D
[PROOF STEP]
proof (induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>D. fill_gholes_gmctxt GMHole (sup_gmctxt_args GMHole D) = GMHole \<squnion> D
 2. \<And>C. fill_gholes_gmctxt C (sup_gmctxt_args C GMHole) = C \<squnion> GMHole
 3. \<And>f g Cs Ds. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f Cs) (sup_gmctxt_args (GMFun f Cs) (GMFun g Ds)) = GMFun f Cs \<squnion> GMFun g Ds
[PROOF STEP]
note fill_gholes_gmctxt.simps [simp del]
[PROOF STATE]
proof (state)
this:
fill_gholes_gmctxt GMHole [] = GMHole
fill_gholes_gmctxt GMHole [?t] = ?t
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])

goal (3 subgoals):
 1. \<And>D. fill_gholes_gmctxt GMHole (sup_gmctxt_args GMHole D) = GMHole \<squnion> D
 2. \<And>C. fill_gholes_gmctxt C (sup_gmctxt_args C GMHole) = C \<squnion> GMHole
 3. \<And>f g Cs Ds. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f Cs) (sup_gmctxt_args (GMFun f Cs) (GMFun g Ds)) = GMFun f Cs \<squnion> GMFun g Ds
[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> fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i

goal (3 subgoals):
 1. \<And>D. fill_gholes_gmctxt GMHole (sup_gmctxt_args GMHole D) = GMHole \<squnion> D
 2. \<And>C. fill_gholes_gmctxt C (sup_gmctxt_args C GMHole) = C \<squnion> GMHole
 3. \<And>f g Cs Ds. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f Cs) (sup_gmctxt_args (GMFun f Cs) (GMFun g Ds)) = GMFun f Cs \<squnion> GMFun g Ds
[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> fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i
[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> fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i

goal (1 subgoal):
 1. fill_gholes_gmctxt (GMFun f Cs) (sup_gmctxt_args (GMFun f Cs) (GMFun g Ds)) = GMFun f Cs \<squnion> GMFun g Ds
[PROOF STEP]
proof (cases "f = g \<and> length Cs = length Ds")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i; f = g \<and> length Cs = length Ds\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f Cs) (sup_gmctxt_args (GMFun f Cs) (GMFun g Ds)) = GMFun f Cs \<squnion> GMFun g Ds
 2. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i; \<not> (f = g \<and> length Cs = length Ds)\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f Cs) (sup_gmctxt_args (GMFun f Cs) (GMFun g Ds)) = GMFun f Cs \<squnion> GMFun g Ds
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
f = g \<and> length Cs = length Ds

goal (2 subgoals):
 1. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i; f = g \<and> length Cs = length Ds\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f Cs) (sup_gmctxt_args (GMFun f Cs) (GMFun g Ds)) = GMFun f Cs \<squnion> GMFun g Ds
 2. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i; \<not> (f = g \<and> length Cs = length Ds)\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f Cs) (sup_gmctxt_args (GMFun f Cs) (GMFun g Ds)) = GMFun f Cs \<squnion> GMFun g Ds
[PROOF STEP]
with GMFun
[PROOF STATE]
proof (chain)
picking this:
f = g
length Cs = length Ds
\<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i
f = g \<and> length Cs = length Ds
[PROOF STEP]
have "\<forall>i < length Cs.
      fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i"
      and *: "\<forall>i < length Cs. (Cs ! i, Ds ! i) \<in> comp_gmctxt"
[PROOF STATE]
proof (prove)
using this:
f = g
length Cs = length Ds
\<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i
f = g \<and> length Cs = length Ds

goal (1 subgoal):
 1. \<forall>i<length Cs. fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i &&& \<forall>i<length Cs. (Cs ! i, Ds ! i) \<in> comp_gmctxt
[PROOF STEP]
by (force simp: set_zip)+
[PROOF STATE]
proof (state)
this:
\<forall>i<length Cs. fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i
\<forall>i<length Cs. (Cs ! i, Ds ! i) \<in> comp_gmctxt

goal (2 subgoals):
 1. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i; f = g \<and> length Cs = length Ds\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f Cs) (sup_gmctxt_args (GMFun f Cs) (GMFun g Ds)) = GMFun f Cs \<squnion> GMFun g Ds
 2. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i; \<not> (f = g \<and> length Cs = length Ds)\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f Cs) (sup_gmctxt_args (GMFun f Cs) (GMFun g Ds)) = GMFun f Cs \<squnion> GMFun g Ds
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<forall>i<length Cs. fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i
\<forall>i<length Cs. (Cs ! i, Ds ! i) \<in> comp_gmctxt

goal (2 subgoals):
 1. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i; f = g \<and> length Cs = length Ds\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f Cs) (sup_gmctxt_args (GMFun f Cs) (GMFun g Ds)) = GMFun f Cs \<squnion> GMFun g Ds
 2. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i; \<not> (f = g \<and> length Cs = length Ds)\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f Cs) (sup_gmctxt_args (GMFun f Cs) (GMFun g Ds)) = GMFun f Cs \<squnion> GMFun g Ds
[PROOF STEP]
have "partition_gholes (concat (map (case_prod sup_gmctxt_args) (zip Cs Ds)))
      Cs = map (case_prod sup_gmctxt_args) (zip Cs Ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_gholes (concat (map2 sup_gmctxt_args Cs Ds)) Cs = map2 sup_gmctxt_args Cs Ds
[PROOF STEP]
using True and *
[PROOF STATE]
proof (prove)
using this:
f = g \<and> length Cs = length Ds
\<forall>i<length Cs. (Cs ! i, Ds ! i) \<in> comp_gmctxt

goal (1 subgoal):
 1. partition_gholes (concat (map2 sup_gmctxt_args Cs Ds)) Cs = map2 sup_gmctxt_args Cs Ds
[PROOF STEP]
by (intro partition_by_concat_id) (auto simp: num_gholes_sup_gmctxt_args)
[PROOF STATE]
proof (state)
this:
partition_gholes (concat (map2 sup_gmctxt_args Cs Ds)) Cs = map2 sup_gmctxt_args Cs Ds

goal (2 subgoals):
 1. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i; f = g \<and> length Cs = length Ds\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f Cs) (sup_gmctxt_args (GMFun f Cs) (GMFun g Ds)) = GMFun f Cs \<squnion> GMFun g Ds
 2. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i; \<not> (f = g \<and> length Cs = length Ds)\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f Cs) (sup_gmctxt_args (GMFun f Cs) (GMFun g Ds)) = GMFun f Cs \<squnion> GMFun g Ds
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<forall>i<length Cs. fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i
\<forall>i<length Cs. (Cs ! i, Ds ! i) \<in> comp_gmctxt
partition_gholes (concat (map2 sup_gmctxt_args Cs Ds)) Cs = map2 sup_gmctxt_args Cs Ds
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length Cs. fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i
\<forall>i<length Cs. (Cs ! i, Ds ! i) \<in> comp_gmctxt
partition_gholes (concat (map2 sup_gmctxt_args Cs Ds)) Cs = map2 sup_gmctxt_args Cs Ds

goal (1 subgoal):
 1. fill_gholes_gmctxt (GMFun f Cs) (sup_gmctxt_args (GMFun f Cs) (GMFun g Ds)) = GMFun f Cs \<squnion> GMFun g Ds
[PROOF STEP]
using * and True
[PROOF STATE]
proof (prove)
using this:
\<forall>i<length Cs. fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i
\<forall>i<length Cs. (Cs ! i, Ds ! i) \<in> comp_gmctxt
partition_gholes (concat (map2 sup_gmctxt_args Cs Ds)) Cs = map2 sup_gmctxt_args Cs Ds
\<forall>i<length Cs. (Cs ! i, Ds ! i) \<in> comp_gmctxt
f = g \<and> length Cs = length Ds

goal (1 subgoal):
 1. fill_gholes_gmctxt (GMFun f Cs) (sup_gmctxt_args (GMFun f Cs) (GMFun g Ds)) = GMFun f Cs \<squnion> GMFun g Ds
[PROOF STEP]
by (auto simp: partition_holes_fill_gholes_gmctxt_conv intro!: nth_equalityI)
[PROOF STATE]
proof (state)
this:
fill_gholes_gmctxt (GMFun f Cs) (sup_gmctxt_args (GMFun f Cs) (GMFun g Ds)) = GMFun f Cs \<squnion> GMFun g Ds

goal (1 subgoal):
 1. \<lbrakk>f = g; length Cs = length Ds; \<forall>i<length Ds. (Cs ! i, Ds ! i) \<in> comp_gmctxt \<and> fill_gholes_gmctxt (Cs ! i) (sup_gmctxt_args (Cs ! i) (Ds ! i)) = Cs ! i \<squnion> Ds ! i; \<not> (f = g \<and> length Cs = length Ds)\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f Cs) (sup_gmctxt_args (GMFun f Cs) (GMFun g Ds)) = GMFun f Cs \<squnion> GMFun g Ds
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
fill_gholes_gmctxt (GMFun f Cs) (sup_gmctxt_args (GMFun f Cs) (GMFun g Ds)) = GMFun f Cs \<squnion> GMFun g Ds

goal (2 subgoals):
 1. \<And>D. fill_gholes_gmctxt GMHole (sup_gmctxt_args GMHole D) = GMHole \<squnion> D
 2. \<And>C. fill_gholes_gmctxt C (sup_gmctxt_args C GMHole) = C \<squnion> GMHole
[PROOF STEP]
qed auto


[STATEMENT]
lemma eqgf_comp_gmctxt:
  assumes "s =\<^sub>G\<^sub>f (C, ss)" and "s =\<^sub>G\<^sub>f (D, ts)"
  shows "(C, D) \<in> comp_gmctxt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C, D) \<in> comp_gmctxt
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s =\<^sub>G\<^sub>f (C, ss)
s =\<^sub>G\<^sub>f (D, ts)

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

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

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

goal (1 subgoal):
 1. \<And>x1a x2a C D ss ts. \<lbrakk>\<And>x2aa C D ss ts. \<lbrakk>x2aa \<in> set x2a; x2aa =\<^sub>G\<^sub>f (C, ss); x2aa =\<^sub>G\<^sub>f (D, ts)\<rbrakk> \<Longrightarrow> (C, D) \<in> comp_gmctxt; GFun x1a x2a =\<^sub>G\<^sub>f (C, ss); GFun x1a x2a =\<^sub>G\<^sub>f (D, ts)\<rbrakk> \<Longrightarrow> (C, D) \<in> comp_gmctxt
[PROOF STEP]
have ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C, D) \<in> comp_gmctxt
[PROOF STEP]
proof (unfold *, intro comp_gmctxt.GMFun [OF refl **] allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < length Ds \<Longrightarrow> (Cs ! i, Ds ! i) \<in> comp_gmctxt
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < length Ds \<Longrightarrow> (Cs ! i, Ds ! i) \<in> comp_gmctxt
[PROOF STEP]
assume "i < length Ds"
[PROOF STATE]
proof (state)
this:
i < length Ds

goal (1 subgoal):
 1. \<And>i. i < length Ds \<Longrightarrow> (Cs ! i, Ds ! i) \<in> comp_gmctxt
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length Ds
[PROOF STEP]
show "(Cs ! i, Ds ! i) \<in> comp_gmctxt"
[PROOF STATE]
proof (prove)
using this:
i < length Ds

goal (1 subgoal):
 1. (Cs ! i, Ds ! i) \<in> comp_gmctxt
[PROOF STEP]
using GFun
[PROOF STATE]
proof (prove)
using this:
i < length Ds
\<lbrakk>?x2aa \<in> set ss; ?x2aa =\<^sub>G\<^sub>f (?C, ?ss); ?x2aa =\<^sub>G\<^sub>f (?D, ?ts)\<rbrakk> \<Longrightarrow> (?C, ?D) \<in> comp_gmctxt
GFun f ss =\<^sub>G\<^sub>f (C, us)
GFun f ss =\<^sub>G\<^sub>f (D, vs)

goal (1 subgoal):
 1. (Cs ! i, Ds ! i) \<in> comp_gmctxt
[PROOF STEP]
by (auto simp: * ** elim!: eqgf_GMFunE) (metis nth_mem)
[PROOF STATE]
proof (state)
this:
(Cs ! i, Ds ! i) \<in> comp_gmctxt

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(C, D) \<in> comp_gmctxt

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

goal (1 subgoal):
 1. \<And>x1a x2a C D ss ts. \<lbrakk>\<And>x2aa C D ss ts. \<lbrakk>x2aa \<in> set x2a; x2aa =\<^sub>G\<^sub>f (C, ss); x2aa =\<^sub>G\<^sub>f (D, ts)\<rbrakk> \<Longrightarrow> (C, D) \<in> comp_gmctxt; GFun x1a x2a =\<^sub>G\<^sub>f (C, ss); GFun x1a x2a =\<^sub>G\<^sub>f (D, ts)\<rbrakk> \<Longrightarrow> (C, D) \<in> comp_gmctxt
[PROOF STEP]
from GFun.prems this
[PROOF STATE]
proof (chain)
picking this:
GFun f ss =\<^sub>G\<^sub>f (C, us)
GFun f ss =\<^sub>G\<^sub>f (D, vs)
\<lbrakk>C = GMFun f ?Cs2; D = GMFun f ?Ds2; length ?Cs2 = length ?Ds2\<rbrakk> \<Longrightarrow> (C, D) \<in> comp_gmctxt
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
GFun f ss =\<^sub>G\<^sub>f (C, us)
GFun f ss =\<^sub>G\<^sub>f (D, vs)
\<lbrakk>C = GMFun f ?Cs2; D = GMFun f ?Ds2; length ?Cs2 = length ?Ds2\<rbrakk> \<Longrightarrow> (C, D) \<in> comp_gmctxt

goal (1 subgoal):
 1. (C, D) \<in> comp_gmctxt
[PROOF STEP]
by (cases C D rule: gmctxt.exhaust [case_product gmctxt.exhaust])
    (auto simp: eq_gfill.simps dest: map_eq_imp_length_eq)
[PROOF STATE]
proof (state)
this:
(C, D) \<in> comp_gmctxt

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqgf_less_eq [simp]:
  assumes "s =\<^sub>G\<^sub>f (C, ss)"
  shows "C \<le> gmctxt_of_gterm s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<le> gmctxt_of_gterm s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
s =\<^sub>G\<^sub>f (C, ss)

goal (1 subgoal):
 1. C \<le> gmctxt_of_gterm s
[PROOF STEP]
by (induct rule: eq_gfill_induct) (auto simp: less_eq_gmctxt_prime)


[STATEMENT]
lemma less_eq_comp_gmctxt [simp]:
  "C \<le> D \<Longrightarrow> (C, D) \<in> comp_gmctxt"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<le> D \<Longrightarrow> (C, D) \<in> comp_gmctxt
[PROOF STEP]
by (induct rule: less_eq_gmctxt_induct) auto


[STATEMENT]
lemma gmctxt_less_eq_sup:
  "(C :: 'f gmctxt) \<le> D \<Longrightarrow> C \<squnion> D = D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<le> D \<Longrightarrow> C \<squnion> D = D
[PROOF STEP]
by (induct rule: less_eq_gmctxt_induct) (auto intro: nth_equalityI)


[STATEMENT]
lemma fill_gholes_gmctxt_less_eq:
  assumes "num_gholes C = length Ds"
  shows "C \<le> fill_gholes_gmctxt C Ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<le> fill_gholes_gmctxt C Ds
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
num_gholes C = length Ds

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

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

goal (1 subgoal):
 1. GMFun f Cs \<le> fill_gholes_gmctxt (GMFun f Cs) Ds
[PROOF STEP]
unfolding partition_holes_fill_gholes_gmctxt_conv'
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?n1 < length Cs; num_gholes (Cs ! ?n1) = length ?Ds\<rbrakk> \<Longrightarrow> Cs ! ?n1 \<le> fill_gholes_gmctxt (Cs ! ?n1) ?Ds
num_gholes (GMFun f Cs) = length Ds

goal (1 subgoal):
 1. GMFun f Cs \<le> GMFun f (map2 fill_gholes_gmctxt Cs (partition_gholes Ds Cs))
[PROOF STEP]
by (intro less_eq_gmctxt_intros) (auto simp: length_partition_by_nth)
[PROOF STATE]
proof (state)
this:
GMFun f Cs \<le> fill_gholes_gmctxt (GMFun f Cs) Ds

goal (1 subgoal):
 1. \<And>Ds. num_gholes GMHole = length Ds \<Longrightarrow> GMHole \<le> fill_gholes_gmctxt GMHole Ds
[PROOF STEP]
qed simp


[STATEMENT]
lemma less_eq_to_sup_mctxt_args [elim]:
  assumes "C \<le> D"
  obtains Ds where "num_gholes C = length Ds" "D = fill_gholes_gmctxt C Ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>Ds. \<lbrakk>num_gholes C = length Ds; D = fill_gholes_gmctxt C Ds\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms gmctxt_less_eq_sup[OF assms]
[PROOF STATE]
proof (prove)
using this:
C \<le> D
C \<squnion> D = D

goal (1 subgoal):
 1. (\<And>Ds. \<lbrakk>num_gholes C = length Ds; D = fill_gholes_gmctxt C Ds\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using sup_gmctxt_sup_gmctxt_args[OF less_eq_comp_gmctxt[OF assms]]
[PROOF STATE]
proof (prove)
using this:
C \<le> D
C \<squnion> D = D
fill_gholes_gmctxt C (sup_gmctxt_args C D) = C \<squnion> D

goal (1 subgoal):
 1. (\<And>Ds. \<lbrakk>num_gholes C = length Ds; D = fill_gholes_gmctxt C Ds\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using less_eq_comp_gmctxt num_gholes_sup_gmctxt_args
[PROOF STATE]
proof (prove)
using this:
C \<le> D
C \<squnion> D = D
fill_gholes_gmctxt C (sup_gmctxt_args C D) = C \<squnion> D
?C \<le> ?D \<Longrightarrow> (?C, ?D) \<in> comp_gmctxt
(?C, ?D) \<in> comp_gmctxt \<Longrightarrow> num_gholes ?C = length (sup_gmctxt_args ?C ?D)

goal (1 subgoal):
 1. (\<And>Ds. \<lbrakk>num_gholes C = length Ds; D = fill_gholes_gmctxt C Ds\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by force


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

goal (1 subgoal):
 1. sup_gmctxt_args C (fill_gholes_gmctxt C Ds) = Ds
[PROOF STEP]
proof (induct C arbitrary: Ds)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Ds. num_gholes GMHole = length Ds \<Longrightarrow> sup_gmctxt_args GMHole (fill_gholes_gmctxt GMHole Ds) = Ds
 2. \<And>x1 x2 Ds. \<lbrakk>\<And>x2a Ds. \<lbrakk>x2a \<in> set x2; num_gholes x2a = length Ds\<rbrakk> \<Longrightarrow> sup_gmctxt_args x2a (fill_gholes_gmctxt x2a Ds) = Ds; num_gholes (GMFun x1 x2) = length Ds\<rbrakk> \<Longrightarrow> sup_gmctxt_args (GMFun x1 x2) (fill_gholes_gmctxt (GMFun x1 x2) Ds) = 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> sup_gmctxt_args GMHole (fill_gholes_gmctxt GMHole Ds) = Ds
 2. \<And>x1 x2 Ds. \<lbrakk>\<And>x2a Ds. \<lbrakk>x2a \<in> set x2; num_gholes x2a = length Ds\<rbrakk> \<Longrightarrow> sup_gmctxt_args x2a (fill_gholes_gmctxt x2a Ds) = Ds; num_gholes (GMFun x1 x2) = length Ds\<rbrakk> \<Longrightarrow> sup_gmctxt_args (GMFun x1 x2) (fill_gholes_gmctxt (GMFun x1 x2) Ds) = 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. sup_gmctxt_args GMHole (fill_gholes_gmctxt GMHole Ds) = Ds
[PROOF STEP]
by (cases Ds) auto
[PROOF STATE]
proof (state)
this:
sup_gmctxt_args GMHole (fill_gholes_gmctxt GMHole Ds) = 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> sup_gmctxt_args x2a (fill_gholes_gmctxt x2a Ds) = Ds; num_gholes (GMFun x1 x2) = length Ds\<rbrakk> \<Longrightarrow> sup_gmctxt_args (GMFun x1 x2) (fill_gholes_gmctxt (GMFun x1 x2) Ds) = 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> sup_gmctxt_args x2a (fill_gholes_gmctxt x2a Ds) = Ds; num_gholes (GMFun x1 x2) = length Ds\<rbrakk> \<Longrightarrow> sup_gmctxt_args (GMFun x1 x2) (fill_gholes_gmctxt (GMFun x1 x2) Ds) = Ds
[PROOF STEP]
case (GMFun f Cs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set Cs; num_gholes ?x2a = length ?Ds\<rbrakk> \<Longrightarrow> sup_gmctxt_args ?x2a (fill_gholes_gmctxt ?x2a ?Ds) = ?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> sup_gmctxt_args x2a (fill_gholes_gmctxt x2a Ds) = Ds; num_gholes (GMFun x1 x2) = length Ds\<rbrakk> \<Longrightarrow> sup_gmctxt_args (GMFun x1 x2) (fill_gholes_gmctxt (GMFun x1 x2) Ds) = Ds
[PROOF STEP]
have "map2 sup_gmctxt_args Cs (map2 fill_gholes_gmctxt Cs (partition_gholes Ds Cs)) = partition_gholes Ds Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map2 sup_gmctxt_args Cs (map2 fill_gholes_gmctxt Cs (partition_gholes Ds Cs)) = partition_gholes Ds Cs
[PROOF STEP]
using GMFun(1)[OF nth_mem] GMFun(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?n1 < length Cs; num_gholes (Cs ! ?n1) = length ?Ds\<rbrakk> \<Longrightarrow> sup_gmctxt_args (Cs ! ?n1) (fill_gholes_gmctxt (Cs ! ?n1) ?Ds) = ?Ds
num_gholes (GMFun f Cs) = length Ds

goal (1 subgoal):
 1. map2 sup_gmctxt_args Cs (map2 fill_gholes_gmctxt Cs (partition_gholes Ds Cs)) = partition_gholes Ds Cs
[PROOF STEP]
by (auto simp: length_partition_by_nth intro!: nth_equalityI)
[PROOF STATE]
proof (state)
this:
map2 sup_gmctxt_args Cs (map2 fill_gholes_gmctxt Cs (partition_gholes Ds Cs)) = partition_gholes Ds Cs

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

goal (1 subgoal):
 1. sup_gmctxt_args (GMFun f Cs) (fill_gholes_gmctxt (GMFun f Cs) Ds) = Ds
[PROOF STEP]
using GMFun(1)[OF nth_mem] GMFun(2)
[PROOF STATE]
proof (prove)
using this:
map2 sup_gmctxt_args Cs (map2 fill_gholes_gmctxt Cs (partition_gholes Ds Cs)) = partition_gholes Ds Cs
\<lbrakk>?n1 < length Cs; num_gholes (Cs ! ?n1) = length ?Ds\<rbrakk> \<Longrightarrow> sup_gmctxt_args (Cs ! ?n1) (fill_gholes_gmctxt (Cs ! ?n1) ?Ds) = ?Ds
num_gholes (GMFun f Cs) = length Ds

goal (1 subgoal):
 1. sup_gmctxt_args (GMFun f Cs) (fill_gholes_gmctxt (GMFun f Cs) Ds) = Ds
[PROOF STEP]
unfolding partition_holes_fill_gholes_gmctxt_conv'
[PROOF STATE]
proof (prove)
using this:
map2 sup_gmctxt_args Cs (map2 fill_gholes_gmctxt Cs (partition_gholes Ds Cs)) = partition_gholes Ds Cs
\<lbrakk>?n1 < length Cs; num_gholes (Cs ! ?n1) = length ?Ds\<rbrakk> \<Longrightarrow> sup_gmctxt_args (Cs ! ?n1) (fill_gholes_gmctxt (Cs ! ?n1) ?Ds) = ?Ds
num_gholes (GMFun f Cs) = length Ds

goal (1 subgoal):
 1. sup_gmctxt_args (GMFun f Cs) (GMFun f (map2 fill_gholes_gmctxt Cs (partition_gholes Ds Cs))) = Ds
[PROOF STEP]
using concat_partition_by[of "map num_gholes Cs" Ds]
[PROOF STATE]
proof (prove)
using this:
map2 sup_gmctxt_args Cs (map2 fill_gholes_gmctxt Cs (partition_gholes Ds Cs)) = partition_gholes Ds Cs
\<lbrakk>?n1 < length Cs; num_gholes (Cs ! ?n1) = length ?Ds\<rbrakk> \<Longrightarrow> sup_gmctxt_args (Cs ! ?n1) (fill_gholes_gmctxt (Cs ! ?n1) ?Ds) = ?Ds
num_gholes (GMFun f Cs) = length Ds
sum_list (map num_gholes Cs) = length Ds \<Longrightarrow> concat (partition_gholes Ds Cs) = Ds

goal (1 subgoal):
 1. sup_gmctxt_args (GMFun f Cs) (GMFun f (map2 fill_gholes_gmctxt Cs (partition_gholes Ds Cs))) = Ds
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sup_gmctxt_args (GMFun f Cs) (fill_gholes_gmctxt (GMFun f Cs) Ds) = Ds

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map2_fill_gholes_gmctxt_id [simp]:
  assumes "\<And> i. i < length Ds \<Longrightarrow> num_gholes (Ds ! i) = 0"
  shows "map2 fill_gholes_gmctxt Ds (replicate (length Ds) []) = Ds"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map2 fill_gholes_gmctxt Ds (replicate (length Ds) []) = Ds
[PROOF STEP]
using assms fill_gholes_gmctxt_no_holes[of "Ds ! i" for i]
[PROOF STATE]
proof (prove)
using this:
?i < length Ds \<Longrightarrow> num_gholes (Ds ! ?i) = 0
num_gholes (Ds ! ?i2) = 0 \<Longrightarrow> fill_gholes_gmctxt (Ds ! ?i2) [] = Ds ! ?i2

goal (1 subgoal):
 1. map2 fill_gholes_gmctxt Ds (replicate (length Ds) []) = Ds
[PROOF STEP]
by (auto simp: map_nth_eq_conv)


[STATEMENT]
lemma fill_gholes_gmctxt_GMFun_replicate_append [simp]:
  assumes "length Cs = n" and "\<And> t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0"
  shows "fill_gholes_gmctxt (GMFun f ((replicate n GMHole) @ Ds)) Cs = GMFun f (Cs @ Ds)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_gholes_gmctxt (GMFun f (replicate n GMHole @ Ds)) Cs = GMFun f (Cs @ Ds)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length Cs = n
?t \<in> set Ds \<Longrightarrow> num_gholes ?t = 0

goal (1 subgoal):
 1. fill_gholes_gmctxt (GMFun f (replicate n GMHole @ Ds)) Cs = GMFun f (Cs @ Ds)
[PROOF STEP]
proof (induct n arbitrary: Cs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Cs. \<lbrakk>length Cs = 0; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f (replicate 0 GMHole @ Ds)) Cs = GMFun f (Cs @ Ds)
 2. \<And>n Cs. \<lbrakk>\<And>Cs. \<lbrakk>length Cs = n; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f (replicate n GMHole @ Ds)) Cs = GMFun f (Cs @ Ds); length Cs = Suc n; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f (replicate (Suc n) GMHole @ Ds)) Cs = GMFun f (Cs @ Ds)
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
length Cs = 0
?t \<in> set Ds \<Longrightarrow> num_gholes ?t = 0

goal (2 subgoals):
 1. \<And>Cs. \<lbrakk>length Cs = 0; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f (replicate 0 GMHole @ Ds)) Cs = GMFun f (Cs @ Ds)
 2. \<And>n Cs. \<lbrakk>\<And>Cs. \<lbrakk>length Cs = n; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f (replicate n GMHole @ Ds)) Cs = GMFun f (Cs @ Ds); length Cs = Suc n; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f (replicate (Suc n) GMHole @ Ds)) Cs = GMFun f (Cs @ Ds)
[PROOF STEP]
note [simp] = 0(1)
[PROOF STATE]
proof (state)
this:
length Cs = 0

goal (2 subgoals):
 1. \<And>Cs. \<lbrakk>length Cs = 0; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f (replicate 0 GMHole @ Ds)) Cs = GMFun f (Cs @ Ds)
 2. \<And>n Cs. \<lbrakk>\<And>Cs. \<lbrakk>length Cs = n; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f (replicate n GMHole @ Ds)) Cs = GMFun f (Cs @ Ds); length Cs = Suc n; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f (replicate (Suc n) GMHole @ Ds)) Cs = GMFun f (Cs @ Ds)
[PROOF STEP]
have "i < length Ds \<Longrightarrow> num_gholes (Ds ! i) = 0" for i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length Ds \<Longrightarrow> num_gholes (Ds ! i) = 0
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
length Cs = 0
?t \<in> set Ds \<Longrightarrow> num_gholes ?t = 0

goal (1 subgoal):
 1. i < length Ds \<Longrightarrow> num_gholes (Ds ! i) = 0
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
?i < length Ds \<Longrightarrow> num_gholes (Ds ! ?i) = 0

goal (2 subgoals):
 1. \<And>Cs. \<lbrakk>length Cs = 0; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f (replicate 0 GMHole @ Ds)) Cs = GMFun f (Cs @ Ds)
 2. \<And>n Cs. \<lbrakk>\<And>Cs. \<lbrakk>length Cs = n; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f (replicate n GMHole @ Ds)) Cs = GMFun f (Cs @ Ds); length Cs = Suc n; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f (replicate (Suc n) GMHole @ Ds)) Cs = GMFun f (Cs @ Ds)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?i < length Ds \<Longrightarrow> num_gholes (Ds ! ?i) = 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?i < length Ds \<Longrightarrow> num_gholes (Ds ! ?i) = 0

goal (1 subgoal):
 1. fill_gholes_gmctxt (GMFun f (replicate 0 GMHole @ Ds)) Cs = GMFun f (Cs @ Ds)
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
?i < length Ds \<Longrightarrow> num_gholes (Ds ! ?i) = 0
length Cs = 0
?t \<in> set Ds \<Longrightarrow> num_gholes ?t = 0

goal (1 subgoal):
 1. fill_gholes_gmctxt (GMFun f (replicate 0 GMHole @ Ds)) Cs = GMFun f (Cs @ Ds)
[PROOF STEP]
unfolding partition_holes_fill_gholes_gmctxt_conv'
[PROOF STATE]
proof (prove)
using this:
?i < length Ds \<Longrightarrow> num_gholes (Ds ! ?i) = 0
length Cs = 0
?t \<in> set Ds \<Longrightarrow> num_gholes ?t = 0

goal (1 subgoal):
 1. GMFun f (map2 fill_gholes_gmctxt (replicate 0 GMHole @ Ds) (partition_gholes Cs (replicate 0 GMHole @ Ds))) = GMFun f (Cs @ Ds)
[PROOF STEP]
by (cases Cs) auto
[PROOF STATE]
proof (state)
this:
fill_gholes_gmctxt (GMFun f (replicate 0 GMHole @ Ds)) Cs = GMFun f (Cs @ Ds)

goal (1 subgoal):
 1. \<And>n Cs. \<lbrakk>\<And>Cs. \<lbrakk>length Cs = n; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f (replicate n GMHole @ Ds)) Cs = GMFun f (Cs @ Ds); length Cs = Suc n; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f (replicate (Suc n) GMHole @ Ds)) Cs = GMFun f (Cs @ Ds)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>n Cs. \<lbrakk>\<And>Cs. \<lbrakk>length Cs = n; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f (replicate n GMHole @ Ds)) Cs = GMFun f (Cs @ Ds); length Cs = Suc n; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f (replicate (Suc n) GMHole @ Ds)) Cs = GMFun f (Cs @ Ds)
[PROOF STEP]
case (Suc n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>length ?Cs = n; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f (replicate n GMHole @ Ds)) ?Cs = GMFun f (?Cs @ Ds)
length Cs = Suc n
?t \<in> set Ds \<Longrightarrow> num_gholes ?t = 0

goal (1 subgoal):
 1. \<And>n Cs. \<lbrakk>\<And>Cs. \<lbrakk>length Cs = n; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f (replicate n GMHole @ Ds)) Cs = GMFun f (Cs @ Ds); length Cs = Suc n; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f (replicate (Suc n) GMHole @ Ds)) Cs = GMFun f (Cs @ Ds)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>length ?Cs = n; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f (replicate n GMHole @ Ds)) ?Cs = GMFun f (?Cs @ Ds)
length Cs = Suc n
?t \<in> set Ds \<Longrightarrow> num_gholes ?t = 0
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length ?Cs = n; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> fill_gholes_gmctxt (GMFun f (replicate n GMHole @ Ds)) ?Cs = GMFun f (?Cs @ Ds)
length Cs = Suc n
?t \<in> set Ds \<Longrightarrow> num_gholes ?t = 0

goal (1 subgoal):
 1. fill_gholes_gmctxt (GMFun f (replicate (Suc n) GMHole @ Ds)) Cs = GMFun f (Cs @ Ds)
[PROOF STEP]
unfolding partition_holes_fill_gholes_gmctxt_conv'
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>length ?Cs = n; \<And>t. t \<in> set Ds \<Longrightarrow> num_gholes t = 0\<rbrakk> \<Longrightarrow> GMFun f (map2 fill_gholes_gmctxt (replicate n GMHole @ Ds) (partition_gholes ?Cs (replicate n GMHole @ Ds))) = GMFun f (?Cs @ Ds)
length Cs = Suc n
?t \<in> set Ds \<Longrightarrow> num_gholes ?t = 0

goal (1 subgoal):
 1. GMFun f (map2 fill_gholes_gmctxt (replicate (Suc n) GMHole @ Ds) (partition_gholes Cs (replicate (Suc n) GMHole @ Ds))) = GMFun f (Cs @ Ds)
[PROOF STEP]
by (simp add: Cons_nth_drop_Suc take_Suc_conv_app_nth)
[PROOF STATE]
proof (state)
this:
fill_gholes_gmctxt (GMFun f (replicate (Suc n) GMHole @ Ds)) Cs = GMFun f (Cs @ Ds)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma finite_ghole_poss:
  "finite (ghole_poss C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (ghole_poss C)
[PROOF STEP]
by (induct C) auto


[STATEMENT]
lemma ghole_poss_simp [simp]:
  "ghole_poss (GMFun f cs) = {i # p | i p. i < length cs \<and> p \<in> ghole_poss (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)}
[PROOF STEP]
by auto


[STATEMENT]
lemma num_gholes_zero_ghole_poss:
  "num_gholes D = 0 \<Longrightarrow> ghole_poss D = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes D = 0 \<Longrightarrow> ghole_poss D = {}
[PROOF STEP]
by (induct D) auto


[STATEMENT]
lemma ghole_poss_num_gholes_zero:
  "ghole_poss D = {} \<Longrightarrow> num_gholes D = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ghole_poss D = {} \<Longrightarrow> num_gholes D = 0
[PROOF STEP]
proof (induct D)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. ghole_poss GMHole = {} \<Longrightarrow> num_gholes GMHole = 0
 2. \<And>x1 x2. \<lbrakk>\<And>x2a. \<lbrakk>x2a \<in> set x2; ghole_poss x2a = {}\<rbrakk> \<Longrightarrow> num_gholes x2a = 0; ghole_poss (GMFun x1 x2) = {}\<rbrakk> \<Longrightarrow> num_gholes (GMFun x1 x2) = 0
[PROOF STEP]
case (GMFun f Ds)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set Ds; ghole_poss ?x2a = {}\<rbrakk> \<Longrightarrow> num_gholes ?x2a = 0
ghole_poss (GMFun f Ds) = {}

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

goal (1 subgoal):
 1. num_gholes (GMFun f Ds) = 0
[PROOF STEP]
by (simp, metis Collect_empty_eq Collect_mem_eq in_set_idx)
[PROOF STATE]
proof (state)
this:
num_gholes (GMFun f Ds) = 0

goal (1 subgoal):
 1. ghole_poss GMHole = {} \<Longrightarrow> num_gholes GMHole = 0
[PROOF STEP]
qed simp


[STATEMENT]
lemma num_ghloes_nzero_ghole_poss_nempty:
  "num_gholes D \<noteq> 0 \<Longrightarrow> ghole_poss D \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_gholes D \<noteq> 0 \<Longrightarrow> ghole_poss D \<noteq> {}
[PROOF STEP]
by (induct D) (auto simp: in_set_conv_nth, fastforce)


[STATEMENT]
lemma ghole_poss_epsE [elim]:
  "ghole_poss D = {[]} \<Longrightarrow> D = GMHole"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ghole_poss D = {[]} \<Longrightarrow> D = GMHole
[PROOF STEP]
by (induct D) auto


[STATEMENT]
lemma ghole_poss_gmctxt_of_gterm [simp]:
  "ghole_poss (gmctxt_of_gterm t) = {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ghole_poss (gmctxt_of_gterm t) = {}
[PROOF STEP]
by (induct t) auto


[STATEMENT]
lemma ghole_poss_subseteq_args [simp]:
  assumes "ghole_poss (GMFun f Ds) \<subseteq> ghole_poss (GMFun g Cs)"
  shows "\<forall> i < min (length Ds) (length Cs). ghole_poss (Ds ! i) \<subseteq> ghole_poss (Cs ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i<min (length Ds) (length Cs). ghole_poss (Ds ! i) \<subseteq> ghole_poss (Cs ! i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ghole_poss (GMFun f Ds) \<subseteq> ghole_poss (GMFun g Cs)

goal (1 subgoal):
 1. \<forall>i<min (length Ds) (length Cs). ghole_poss (Ds ! i) \<subseteq> ghole_poss (Cs ! i)
[PROOF STEP]
by auto


[STATEMENT]
lemma factor_ghole_pos_by_prefix:
  assumes "C \<le> D" "p \<in> ghole_poss D"
  obtains q where "q \<le>\<^sub>p p" "q \<in> ghole_poss C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>q. \<lbrakk>q \<le>\<^sub>p p; q \<in> ghole_poss C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
C \<le> D
p \<in> ghole_poss D

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>q \<le>\<^sub>p p; q \<in> ghole_poss C\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (induct C D arbitrary: p thesis rule: less_eq_gmctxt_induct)
     (auto, metis position_less_eq_Cons)