[STATEMENT]
lemma split_vars_ground_vars:
  assumes "ground_mctxt C" and "num_holes C = length xs"
  shows "split_vars (fill_holes C (map Var xs)) = (C, xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. split_vars (fill_holes C (map Var xs)) = (C, xs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ground_mctxt C
num_holes C = length xs

goal (1 subgoal):
 1. split_vars (fill_holes C (map Var xs)) = (C, xs)
[PROOF STEP]
proof (induct C arbitrary: xs)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>xs. \<lbrakk>ground_mctxt MHole; num_holes MHole = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes MHole (map Var xs)) = (MHole, xs)
 3. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
case (MHole xs)
[PROOF STATE]
proof (state)
this:
ground_mctxt MHole
num_holes MHole = length xs

goal (3 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>xs. \<lbrakk>ground_mctxt MHole; num_holes MHole = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes MHole (map Var xs)) = (MHole, xs)
 3. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ground_mctxt MHole
num_holes MHole = length xs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ground_mctxt MHole
num_holes MHole = length xs

goal (1 subgoal):
 1. split_vars (fill_holes MHole (map Var xs)) = (MHole, xs)
[PROOF STEP]
by (cases xs, auto)
[PROOF STATE]
proof (state)
this:
split_vars (fill_holes MHole (map Var xs)) = (MHole, xs)

goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
case (MFun f Cs xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set Cs; ground_mctxt ?x2a; num_holes ?x2a = length ?xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes ?x2a (map Var ?xs)) = (?x2a, ?xs)
ground_mctxt (MFun f Cs)
num_holes (MFun f Cs) = length xs

goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
have "fill_holes (MFun f Cs) (map Var xs) =\<^sub>f (MFun f Cs, map Var xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_holes (MFun f Cs) (map Var xs) =\<^sub>f (MFun f Cs, map Var xs)
[PROOF STEP]
by (rule eqfI, insert MFun(3), auto)
[PROOF STATE]
proof (state)
this:
fill_holes (MFun f Cs) (map Var xs) =\<^sub>f (MFun f Cs, map Var xs)

goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
from eqf_MFunE[OF this]
[PROOF STATE]
proof (chain)
picking this:
(\<And>ts sss. \<lbrakk>fill_holes (MFun f Cs) (map Var xs) = Fun f ts; length ts = length Cs; length sss = length Cs; \<And>i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>f (Cs ! i, sss ! i); map Var xs = concat sss\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain ts xss where fh: "fill_holes (MFun f Cs) (map Var xs) = Fun f ts"
    and lent: "length ts = length Cs"
    and lenx: "length xss = length Cs"
    and args: "\<And>i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>f (Cs ! i, xss ! i)"
    and id: "map Var xs = concat xss"
[PROOF STATE]
proof (prove)
using this:
(\<And>ts sss. \<lbrakk>fill_holes (MFun f Cs) (map Var xs) = Fun f ts; length ts = length Cs; length sss = length Cs; \<And>i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>f (Cs ! i, sss ! i); map Var xs = concat sss\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>ts xss. \<lbrakk>fill_holes (MFun f Cs) (map Var xs) = Fun f ts; length ts = length Cs; length xss = length Cs; \<And>i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>f (Cs ! i, xss ! i); map Var xs = concat xss\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fill_holes (MFun f Cs) (map Var xs) = Fun f ts
length ts = length Cs
length xss = length Cs
?i < length Cs \<Longrightarrow> ts ! ?i =\<^sub>f (Cs ! ?i, xss ! ?i)
map Var xs = concat xss

goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
from arg_cong[OF id, of "map the_Var"]
[PROOF STATE]
proof (chain)
picking this:
map the_Var (map Var xs) = map the_Var (concat xss)
[PROOF STEP]
have id2: "xs = concat (map (map the_Var) xss)"
[PROOF STATE]
proof (prove)
using this:
map the_Var (map Var xs) = map the_Var (concat xss)

goal (1 subgoal):
 1. xs = concat (map (map the_Var) xss)
[PROOF STEP]
by (metis map_concat length_map map_nth_eq_conv term.sel(1))
[PROOF STATE]
proof (state)
this:
xs = concat (map (map the_Var) xss)

goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
xs = concat (map (map the_Var) xss)

goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
assume i: "i < length Cs"
[PROOF STATE]
proof (state)
this:
i < length Cs

goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length Cs
[PROOF STEP]
have mem: "Cs ! i \<in> set Cs"
[PROOF STATE]
proof (prove)
using this:
i < length Cs

goal (1 subgoal):
 1. Cs ! i \<in> set Cs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Cs ! i \<in> set Cs

goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
with MFun(2)
[PROOF STATE]
proof (chain)
picking this:
ground_mctxt (MFun f Cs)
Cs ! i \<in> set Cs
[PROOF STEP]
have ground: "ground_mctxt (Cs ! i)"
[PROOF STATE]
proof (prove)
using this:
ground_mctxt (MFun f Cs)
Cs ! i \<in> set Cs

goal (1 subgoal):
 1. ground_mctxt (Cs ! i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ground_mctxt (Cs ! i)

goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
have "map Var (map the_Var (xss ! i)) = map id (xss ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map Var (map the_Var (xss ! i)) = map id (xss ! i)
[PROOF STEP]
unfolding map_map o_def map_eq_conv
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set (xss ! i). Var (the_Var x) = id x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set (xss ! i) \<Longrightarrow> Var (the_Var x) = id x
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> set (xss ! i) \<Longrightarrow> Var (the_Var x) = id x
[PROOF STEP]
assume "x \<in> set (xss ! i)"
[PROOF STATE]
proof (state)
this:
x \<in> set (xss ! i)

goal (1 subgoal):
 1. \<And>x. x \<in> set (xss ! i) \<Longrightarrow> Var (the_Var x) = id x
[PROOF STEP]
with lenx i
[PROOF STATE]
proof (chain)
picking this:
length xss = length Cs
i < length Cs
x \<in> set (xss ! i)
[PROOF STEP]
have "x \<in> set (concat xss)"
[PROOF STATE]
proof (prove)
using this:
length xss = length Cs
i < length Cs
x \<in> set (xss ! i)

goal (1 subgoal):
 1. x \<in> set (concat xss)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
x \<in> set (concat xss)

goal (1 subgoal):
 1. \<And>x. x \<in> set (xss ! i) \<Longrightarrow> Var (the_Var x) = id x
[PROOF STEP]
from this[unfolded id[symmetric]]
[PROOF STATE]
proof (chain)
picking this:
x \<in> set (map Var xs)
[PROOF STEP]
show "Var (the_Var x) = id x"
[PROOF STATE]
proof (prove)
using this:
x \<in> set (map Var xs)

goal (1 subgoal):
 1. Var (the_Var x) = id x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Var (the_Var x) = id x

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
map Var (map the_Var (xss ! i)) = map id (xss ! i)

goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
map Var (map the_Var (xss ! i)) = map id (xss ! i)
[PROOF STEP]
have idxss: "map Var (map the_Var (xss ! i)) = xss ! i"
[PROOF STATE]
proof (prove)
using this:
map Var (map the_Var (xss ! i)) = map id (xss ! i)

goal (1 subgoal):
 1. map Var (map the_Var (xss ! i)) = xss ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map Var (map the_Var (xss ! i)) = xss ! i

goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
note rec = eqfE[OF args[OF i]]
[PROOF STATE]
proof (state)
this:
ts ! i = fill_holes (Cs ! i) (xss ! i)
num_holes (Cs ! i) = length (xss ! i)

goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
note IH = MFun(1)[OF mem ground, of "map the_Var (xss ! i)", unfolded rec(2) idxss rec(1)[symmetric]]
[PROOF STATE]
proof (state)
this:
length (xss ! i) = length (map the_Var (xss ! i)) \<Longrightarrow> split_vars (ts ! i) = (Cs ! i, map the_Var (xss ! i))

goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
from IH
[PROOF STATE]
proof (chain)
picking this:
length (xss ! i) = length (map the_Var (xss ! i)) \<Longrightarrow> split_vars (ts ! i) = (Cs ! i, map the_Var (xss ! i))
[PROOF STEP]
have "split_vars (ts ! i) = (Cs ! i, map the_Var (xss ! i))"
[PROOF STATE]
proof (prove)
using this:
length (xss ! i) = length (map the_Var (xss ! i)) \<Longrightarrow> split_vars (ts ! i) = (Cs ! i, map the_Var (xss ! i))

goal (1 subgoal):
 1. split_vars (ts ! i) = (Cs ! i, map the_Var (xss ! i))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
split_vars (ts ! i) = (Cs ! i, map the_Var (xss ! i))

goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
note this idxss
[PROOF STATE]
proof (state)
this:
split_vars (ts ! i) = (Cs ! i, map the_Var (xss ! i))
map Var (map the_Var (xss ! i)) = xss ! i

goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i2 < length Cs \<Longrightarrow> split_vars (ts ! ?i2) = (Cs ! ?i2, map the_Var (xss ! ?i2))
?i2 < length Cs \<Longrightarrow> map Var (map the_Var (xss ! ?i2)) = xss ! ?i2

goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
note IH = this
[PROOF STATE]
proof (state)
this:
?i2 < length Cs \<Longrightarrow> split_vars (ts ! ?i2) = (Cs ! ?i2, map the_Var (xss ! ?i2))
?i2 < length Cs \<Longrightarrow> map Var (map the_Var (xss ! ?i2)) = xss ! ?i2

goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
have "?case = (map fst (map split_vars ts) = Cs \<and> concat (map snd (map split_vars ts)) = concat (map (map the_Var) xss))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (split_vars (fill_holes (MFun f Cs) (map Var xs)) = (MFun f Cs, xs)) = (map fst (map split_vars ts) = Cs \<and> concat (map snd (map split_vars ts)) = concat (map (map the_Var) xss))
[PROOF STEP]
unfolding fh
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (split_vars (Fun f ts) = (MFun f Cs, xs)) = (map fst (map split_vars ts) = Cs \<and> concat (map snd (map split_vars ts)) = concat (map (map the_Var) xss))
[PROOF STEP]
unfolding id2
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (split_vars (Fun f ts) = (MFun f Cs, concat (map (map the_Var) xss))) = (map fst (map split_vars ts) = Cs \<and> concat (map snd (map split_vars ts)) = concat (map (map the_Var) xss))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(split_vars (fill_holes (MFun f Cs) (map Var xs)) = (MFun f Cs, xs)) = (map fst (map split_vars ts) = Cs \<and> concat (map snd (map split_vars ts)) = concat (map (map the_Var) xss))

goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(split_vars (fill_holes (MFun f Cs) (map Var xs)) = (MFun f Cs, xs)) = (map fst (map split_vars ts) = Cs \<and> concat (map snd (map split_vars ts)) = concat (map (map the_Var) xss))

goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
have "\<dots>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map fst (map split_vars ts) = Cs \<and> concat (map snd (map split_vars ts)) = concat (map (map the_Var) xss)
[PROOF STEP]
proof (rule conjI[OF nth_equalityI arg_cong[of _ _ concat, OF nth_equalityI, rule_format]], unfold length_map lent lenx)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. length Cs = length Cs
 2. \<And>i. i < length Cs \<Longrightarrow> map fst (map split_vars ts) ! i = Cs ! i
 3. length Cs = length Cs
 4. \<And>i. i < length Cs \<Longrightarrow> map snd (map split_vars ts) ! i = map (map the_Var) xss ! i
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. length Cs = length Cs
 2. \<And>i. i < length Cs \<Longrightarrow> map fst (map split_vars ts) ! i = Cs ! i
 3. length Cs = length Cs
 4. \<And>i. i < length Cs \<Longrightarrow> map snd (map split_vars ts) ! i = map (map the_Var) xss ! i
[PROOF STEP]
assume i: "i < length Cs"
[PROOF STATE]
proof (state)
this:
i < length Cs

goal (4 subgoals):
 1. length Cs = length Cs
 2. \<And>i. i < length Cs \<Longrightarrow> map fst (map split_vars ts) ! i = Cs ! i
 3. length Cs = length Cs
 4. \<And>i. i < length Cs \<Longrightarrow> map snd (map split_vars ts) ! i = map (map the_Var) xss ! i
[PROOF STEP]
with arg_cong[OF IH(2)[OF this], of "map the_Var"]
      IH[OF this]
[PROOF STATE]
proof (chain)
picking this:
map the_Var (map Var (map the_Var (xss ! i))) = map the_Var (xss ! i)
split_vars (ts ! i) = (Cs ! i, map the_Var (xss ! i))
map Var (map the_Var (xss ! i)) = xss ! i
i < length Cs
[PROOF STEP]
show "map snd (map split_vars ts) ! i = map (map the_Var) xss ! i"
[PROOF STATE]
proof (prove)
using this:
map the_Var (map Var (map the_Var (xss ! i))) = map the_Var (xss ! i)
split_vars (ts ! i) = (Cs ! i, map the_Var (xss ! i))
map Var (map the_Var (xss ! i)) = xss ! i
i < length Cs

goal (1 subgoal):
 1. map snd (map split_vars ts) ! i = map (map the_Var) xss ! i
[PROOF STEP]
using lent lenx
[PROOF STATE]
proof (prove)
using this:
map the_Var (map Var (map the_Var (xss ! i))) = map the_Var (xss ! i)
split_vars (ts ! i) = (Cs ! i, map the_Var (xss ! i))
map Var (map the_Var (xss ! i)) = xss ! i
i < length Cs
length ts = length Cs
length xss = length Cs

goal (1 subgoal):
 1. map snd (map split_vars ts) ! i = map (map the_Var) xss ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map snd (map split_vars ts) ! i = map (map the_Var) xss ! i

goal (3 subgoals):
 1. length Cs = length Cs
 2. \<And>i. i < length Cs \<Longrightarrow> map fst (map split_vars ts) ! i = Cs ! i
 3. length Cs = length Cs
[PROOF STEP]
qed (insert IH lent, auto)
[PROOF STATE]
proof (state)
this:
map fst (map split_vars ts) = Cs \<and> concat (map snd (map split_vars ts)) = concat (map (map the_Var) xss)

goal (2 subgoals):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
 2. \<And>x1a x2 xs. \<lbrakk>\<And>x2a xs. \<lbrakk>x2a \<in> set x2; ground_mctxt x2a; num_holes x2a = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes x2a (map Var xs)) = (x2a, xs); ground_mctxt (MFun x1a x2); num_holes (MFun x1a x2) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MFun x1a x2) (map Var xs)) = (MFun x1a x2, xs)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
split_vars (fill_holes (MFun f Cs) (map Var xs)) = (MFun f Cs, xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
split_vars (fill_holes (MFun f Cs) (map Var xs)) = (MFun f Cs, xs)

goal (1 subgoal):
 1. split_vars (fill_holes (MFun f Cs) (map Var xs)) = (MFun f Cs, xs)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
split_vars (fill_holes (MFun f Cs) (map Var xs)) = (MFun f Cs, xs)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>ground_mctxt (MVar x); num_holes (MVar x) = length xs\<rbrakk> \<Longrightarrow> split_vars (fill_holes (MVar x) (map Var xs)) = (MVar x, xs)
[PROOF STEP]
qed auto


[STATEMENT]
lemma split_vars_vars_term_list: "snd (split_vars t) = vars_term_list t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. snd (split_vars t) = vars_term_list t
[PROOF STEP]
proof (induct t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. snd (split_vars (Var x)) = vars_term_list (Var x)
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> snd (split_vars x2a) = vars_term_list x2a) \<Longrightarrow> snd (split_vars (Fun x1a x2)) = vars_term_list (Fun x1a x2)
[PROOF STEP]
case (Fun f ts)
[PROOF STATE]
proof (state)
this:
?x2a \<in> set ts \<Longrightarrow> snd (split_vars ?x2a) = vars_term_list ?x2a

goal (2 subgoals):
 1. \<And>x. snd (split_vars (Var x)) = vars_term_list (Var x)
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> snd (split_vars x2a) = vars_term_list x2a) \<Longrightarrow> snd (split_vars (Fun x1a x2)) = vars_term_list (Fun x1a x2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x2a \<in> set ts \<Longrightarrow> snd (split_vars ?x2a) = vars_term_list ?x2a
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?x2a \<in> set ts \<Longrightarrow> snd (split_vars ?x2a) = vars_term_list ?x2a

goal (1 subgoal):
 1. snd (split_vars (Fun f ts)) = vars_term_list (Fun f ts)
[PROOF STEP]
by (auto simp: vars_term_list.simps o_def, induct ts, auto)
[PROOF STATE]
proof (state)
this:
snd (split_vars (Fun f ts)) = vars_term_list (Fun f ts)

goal (1 subgoal):
 1. \<And>x. snd (split_vars (Var x)) = vars_term_list (Var x)
[PROOF STEP]
qed (auto simp: vars_term_list.simps)


[STATEMENT]
lemma split_vars_num_holes: "num_holes (fst (split_vars t)) = length (snd (split_vars t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_holes (fst (split_vars t)) = length (snd (split_vars t))
[PROOF STEP]
proof (induct t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. num_holes (fst (split_vars (Var x))) = length (snd (split_vars (Var x)))
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> num_holes (fst (split_vars x2a)) = length (snd (split_vars x2a))) \<Longrightarrow> num_holes (fst (split_vars (Fun x1a x2))) = length (snd (split_vars (Fun x1a x2)))
[PROOF STEP]
case (Fun f ts)
[PROOF STATE]
proof (state)
this:
?x2a \<in> set ts \<Longrightarrow> num_holes (fst (split_vars ?x2a)) = length (snd (split_vars ?x2a))

goal (2 subgoals):
 1. \<And>x. num_holes (fst (split_vars (Var x))) = length (snd (split_vars (Var x)))
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> num_holes (fst (split_vars x2a)) = length (snd (split_vars x2a))) \<Longrightarrow> num_holes (fst (split_vars (Fun x1a x2))) = length (snd (split_vars (Fun x1a x2)))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?x2a \<in> set ts \<Longrightarrow> num_holes (fst (split_vars ?x2a)) = length (snd (split_vars ?x2a))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
?x2a \<in> set ts \<Longrightarrow> num_holes (fst (split_vars ?x2a)) = length (snd (split_vars ?x2a))

goal (1 subgoal):
 1. num_holes (fst (split_vars (Fun f ts))) = length (snd (split_vars (Fun f ts)))
[PROOF STEP]
by (induct ts, auto)
[PROOF STATE]
proof (state)
this:
num_holes (fst (split_vars (Fun f ts))) = length (snd (split_vars (Fun f ts)))

goal (1 subgoal):
 1. \<And>x. num_holes (fst (split_vars (Var x))) = length (snd (split_vars (Var x)))
[PROOF STEP]
qed simp


[STATEMENT]
lemma ground_eq_fill: "t =\<^sub>f (C,ss) \<Longrightarrow> ground t = (ground_mctxt C \<and> (\<forall> s \<in> set ss. ground s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t =\<^sub>f (C, ss) \<Longrightarrow> ground t = (ground_mctxt C \<and> (\<forall>s\<in>set ss. ground s))
[PROOF STEP]
proof (induct C arbitrary: t ss)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x t ss. t =\<^sub>f (MVar x, ss) \<Longrightarrow> ground t = (ground_mctxt (MVar x) \<and> Ball (set ss) ground)
 2. \<And>t ss. t =\<^sub>f (MHole, ss) \<Longrightarrow> ground t = (ground_mctxt MHole \<and> Ball (set ss) ground)
 3. \<And>x1a x2 t ss. \<lbrakk>\<And>x2a t ss. \<lbrakk>x2a \<in> set x2; t =\<^sub>f (x2a, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt x2a \<and> Ball (set ss) ground); t =\<^sub>f (MFun x1a x2, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt (MFun x1a x2) \<and> Ball (set ss) ground)
[PROOF STEP]
case (MVar x)
[PROOF STATE]
proof (state)
this:
t =\<^sub>f (MVar x, ss)

goal (3 subgoals):
 1. \<And>x t ss. t =\<^sub>f (MVar x, ss) \<Longrightarrow> ground t = (ground_mctxt (MVar x) \<and> Ball (set ss) ground)
 2. \<And>t ss. t =\<^sub>f (MHole, ss) \<Longrightarrow> ground t = (ground_mctxt MHole \<and> Ball (set ss) ground)
 3. \<And>x1a x2 t ss. \<lbrakk>\<And>x2a t ss. \<lbrakk>x2a \<in> set x2; t =\<^sub>f (x2a, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt x2a \<and> Ball (set ss) ground); t =\<^sub>f (MFun x1a x2, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt (MFun x1a x2) \<and> Ball (set ss) ground)
[PROOF STEP]
from eqfE[OF this]
[PROOF STATE]
proof (chain)
picking this:
t = fill_holes (MVar x) ss
num_holes (MVar x) = length ss
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
t = fill_holes (MVar x) ss
num_holes (MVar x) = length ss

goal (1 subgoal):
 1. ground t = (ground_mctxt (MVar x) \<and> (\<forall>a\<in>set ss. ground a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ground t = (ground_mctxt (MVar x) \<and> (\<forall>a\<in>set ss. ground a))

goal (2 subgoals):
 1. \<And>t ss. t =\<^sub>f (MHole, ss) \<Longrightarrow> ground t = (ground_mctxt MHole \<and> Ball (set ss) ground)
 2. \<And>x1a x2 t ss. \<lbrakk>\<And>x2a t ss. \<lbrakk>x2a \<in> set x2; t =\<^sub>f (x2a, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt x2a \<and> Ball (set ss) ground); t =\<^sub>f (MFun x1a x2, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt (MFun x1a x2) \<and> Ball (set ss) ground)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t ss. t =\<^sub>f (MHole, ss) \<Longrightarrow> ground t = (ground_mctxt MHole \<and> Ball (set ss) ground)
 2. \<And>x1a x2 t ss. \<lbrakk>\<And>x2a t ss. \<lbrakk>x2a \<in> set x2; t =\<^sub>f (x2a, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt x2a \<and> Ball (set ss) ground); t =\<^sub>f (MFun x1a x2, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt (MFun x1a x2) \<and> Ball (set ss) ground)
[PROOF STEP]
case (MHole t ss)
[PROOF STATE]
proof (state)
this:
t =\<^sub>f (MHole, ss)

goal (2 subgoals):
 1. \<And>t ss. t =\<^sub>f (MHole, ss) \<Longrightarrow> ground t = (ground_mctxt MHole \<and> Ball (set ss) ground)
 2. \<And>x1a x2 t ss. \<lbrakk>\<And>x2a t ss. \<lbrakk>x2a \<in> set x2; t =\<^sub>f (x2a, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt x2a \<and> Ball (set ss) ground); t =\<^sub>f (MFun x1a x2, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt (MFun x1a x2) \<and> Ball (set ss) ground)
[PROOF STEP]
from eqfE[OF this]
[PROOF STATE]
proof (chain)
picking this:
t = fill_holes MHole ss
num_holes MHole = length ss
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
t = fill_holes MHole ss
num_holes MHole = length ss

goal (1 subgoal):
 1. ground t = (ground_mctxt MHole \<and> (\<forall>a\<in>set ss. ground a))
[PROOF STEP]
by (cases ss, auto)
[PROOF STATE]
proof (state)
this:
ground t = (ground_mctxt MHole \<and> (\<forall>a\<in>set ss. ground a))

goal (1 subgoal):
 1. \<And>x1a x2 t ss. \<lbrakk>\<And>x2a t ss. \<lbrakk>x2a \<in> set x2; t =\<^sub>f (x2a, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt x2a \<and> Ball (set ss) ground); t =\<^sub>f (MFun x1a x2, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt (MFun x1a x2) \<and> Ball (set ss) ground)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2 t ss. \<lbrakk>\<And>x2a t ss. \<lbrakk>x2a \<in> set x2; t =\<^sub>f (x2a, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt x2a \<and> Ball (set ss) ground); t =\<^sub>f (MFun x1a x2, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt (MFun x1a x2) \<and> Ball (set ss) ground)
[PROOF STEP]
case (MFun f Cs s ss)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set Cs; ?t =\<^sub>f (?x2a, ?ss)\<rbrakk> \<Longrightarrow> ground ?t = (ground_mctxt ?x2a \<and> (\<forall>a\<in>set ?ss. ground a))
s =\<^sub>f (MFun f Cs, ss)

goal (1 subgoal):
 1. \<And>x1a x2 t ss. \<lbrakk>\<And>x2a t ss. \<lbrakk>x2a \<in> set x2; t =\<^sub>f (x2a, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt x2a \<and> Ball (set ss) ground); t =\<^sub>f (MFun x1a x2, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt (MFun x1a x2) \<and> Ball (set ss) ground)
[PROOF STEP]
from eqf_MFunE[OF MFun(2)]
[PROOF STATE]
proof (chain)
picking this:
(\<And>ts sss. \<lbrakk>s = Fun f ts; length ts = length Cs; length sss = length Cs; \<And>i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>f (Cs ! i, sss ! i); ss = concat sss\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain ts sss where s: "s = Fun f ts" and len: "length ts = length Cs" "length sss = length Cs"
    and IH: "\<And> i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>f (Cs ! i, sss ! i)" and ss: "ss = concat sss"
[PROOF STATE]
proof (prove)
using this:
(\<And>ts sss. \<lbrakk>s = Fun f ts; length ts = length Cs; length sss = length Cs; \<And>i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>f (Cs ! i, sss ! i); ss = concat sss\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

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

goal (1 subgoal):
 1. \<And>x1a x2 t ss. \<lbrakk>\<And>x2a t ss. \<lbrakk>x2a \<in> set x2; t =\<^sub>f (x2a, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt x2a \<and> Ball (set ss) ground); t =\<^sub>f (MFun x1a x2, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt (MFun x1a x2) \<and> Ball (set ss) ground)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
s = Fun f ts
length ts = length Cs
length sss = length Cs
?i < length Cs \<Longrightarrow> ts ! ?i =\<^sub>f (Cs ! ?i, sss ! ?i)
ss = concat sss

goal (1 subgoal):
 1. \<And>x1a x2 t ss. \<lbrakk>\<And>x2a t ss. \<lbrakk>x2a \<in> set x2; t =\<^sub>f (x2a, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt x2a \<and> Ball (set ss) ground); t =\<^sub>f (MFun x1a x2, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt (MFun x1a x2) \<and> Ball (set ss) ground)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2 t ss. \<lbrakk>\<And>x2a t ss. \<lbrakk>x2a \<in> set x2; t =\<^sub>f (x2a, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt x2a \<and> Ball (set ss) ground); t =\<^sub>f (MFun x1a x2, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt (MFun x1a x2) \<and> Ball (set ss) ground)
[PROOF STEP]
assume i: "i < length Cs"
[PROOF STATE]
proof (state)
this:
i < length Cs

goal (1 subgoal):
 1. \<And>x1a x2 t ss. \<lbrakk>\<And>x2a t ss. \<lbrakk>x2a \<in> set x2; t =\<^sub>f (x2a, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt x2a \<and> Ball (set ss) ground); t =\<^sub>f (MFun x1a x2, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt (MFun x1a x2) \<and> Ball (set ss) ground)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length Cs
[PROOF STEP]
have "Cs ! i \<in> set Cs"
[PROOF STATE]
proof (prove)
using this:
i < length Cs

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

goal (1 subgoal):
 1. \<And>x1a x2 t ss. \<lbrakk>\<And>x2a t ss. \<lbrakk>x2a \<in> set x2; t =\<^sub>f (x2a, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt x2a \<and> Ball (set ss) ground); t =\<^sub>f (MFun x1a x2, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt (MFun x1a x2) \<and> Ball (set ss) ground)
[PROOF STEP]
from MFun(1)[OF this IH[OF i]]
[PROOF STATE]
proof (chain)
picking this:
ground (ts ! i) = (ground_mctxt (Cs ! i) \<and> (\<forall>a\<in>set (sss ! i). ground a))
[PROOF STEP]
have "ground (ts ! i) = (ground_mctxt (Cs ! i) \<and> (\<forall>a\<in>set (sss ! i). ground a))"
[PROOF STATE]
proof (prove)
using this:
ground (ts ! i) = (ground_mctxt (Cs ! i) \<and> (\<forall>a\<in>set (sss ! i). ground a))

goal (1 subgoal):
 1. ground (ts ! i) = (ground_mctxt (Cs ! i) \<and> (\<forall>a\<in>set (sss ! i). ground a))
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
ground (ts ! i) = (ground_mctxt (Cs ! i) \<and> (\<forall>a\<in>set (sss ! i). ground a))

goal (1 subgoal):
 1. \<And>x1a x2 t ss. \<lbrakk>\<And>x2a t ss. \<lbrakk>x2a \<in> set x2; t =\<^sub>f (x2a, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt x2a \<and> Ball (set ss) ground); t =\<^sub>f (MFun x1a x2, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt (MFun x1a x2) \<and> Ball (set ss) ground)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i2 < length Cs \<Longrightarrow> ground (ts ! ?i2) = (ground_mctxt (Cs ! ?i2) \<and> (\<forall>a\<in>set (sss ! ?i2). ground a))

goal (1 subgoal):
 1. \<And>x1a x2 t ss. \<lbrakk>\<And>x2a t ss. \<lbrakk>x2a \<in> set x2; t =\<^sub>f (x2a, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt x2a \<and> Ball (set ss) ground); t =\<^sub>f (MFun x1a x2, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt (MFun x1a x2) \<and> Ball (set ss) ground)
[PROOF STEP]
note IH = this
[PROOF STATE]
proof (state)
this:
?i2 < length Cs \<Longrightarrow> ground (ts ! ?i2) = (ground_mctxt (Cs ! ?i2) \<and> (\<forall>a\<in>set (sss ! ?i2). ground a))

goal (1 subgoal):
 1. \<And>x1a x2 t ss. \<lbrakk>\<And>x2a t ss. \<lbrakk>x2a \<in> set x2; t =\<^sub>f (x2a, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt x2a \<and> Ball (set ss) ground); t =\<^sub>f (MFun x1a x2, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt (MFun x1a x2) \<and> Ball (set ss) ground)
[PROOF STEP]
note conv = set_conv_nth
[PROOF STATE]
proof (state)
this:
set ?xs = {?xs ! i |i. i < length ?xs}

goal (1 subgoal):
 1. \<And>x1a x2 t ss. \<lbrakk>\<And>x2a t ss. \<lbrakk>x2a \<in> set x2; t =\<^sub>f (x2a, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt x2a \<and> Ball (set ss) ground); t =\<^sub>f (MFun x1a x2, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt (MFun x1a x2) \<and> Ball (set ss) ground)
[PROOF STEP]
have "?case = ((\<forall>x\<in>set ts. ground x) = ((\<forall>x\<in>set Cs. ground_mctxt x) \<and> (\<forall>a\<in>set sss. \<forall>x\<in>set a. ground x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ground s = (ground_mctxt (MFun f Cs) \<and> (\<forall>a\<in>set ss. ground a))) = ((\<forall>x\<in>set ts. ground x) = ((\<forall>x\<in>set Cs. ground_mctxt x) \<and> (\<forall>a\<in>set sss. \<forall>x\<in>set a. ground x)))
[PROOF STEP]
unfolding s ss
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ground (Fun f ts) = (ground_mctxt (MFun f Cs) \<and> (\<forall>a\<in>set (concat sss). ground a))) = ((\<forall>x\<in>set ts. ground x) = ((\<forall>x\<in>set Cs. ground_mctxt x) \<and> (\<forall>a\<in>set sss. \<forall>x\<in>set a. ground x)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(ground s = (ground_mctxt (MFun f Cs) \<and> (\<forall>a\<in>set ss. ground a))) = ((\<forall>x\<in>set ts. ground x) = ((\<forall>x\<in>set Cs. ground_mctxt x) \<and> (\<forall>a\<in>set sss. \<forall>x\<in>set a. ground x)))

goal (1 subgoal):
 1. \<And>x1a x2 t ss. \<lbrakk>\<And>x2a t ss. \<lbrakk>x2a \<in> set x2; t =\<^sub>f (x2a, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt x2a \<and> Ball (set ss) ground); t =\<^sub>f (MFun x1a x2, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt (MFun x1a x2) \<and> Ball (set ss) ground)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(ground s = (ground_mctxt (MFun f Cs) \<and> (\<forall>a\<in>set ss. ground a))) = ((\<forall>x\<in>set ts. ground x) = ((\<forall>x\<in>set Cs. ground_mctxt x) \<and> (\<forall>a\<in>set sss. \<forall>x\<in>set a. ground x)))

goal (1 subgoal):
 1. \<And>x1a x2 t ss. \<lbrakk>\<And>x2a t ss. \<lbrakk>x2a \<in> set x2; t =\<^sub>f (x2a, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt x2a \<and> Ball (set ss) ground); t =\<^sub>f (MFun x1a x2, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt (MFun x1a x2) \<and> Ball (set ss) ground)
[PROOF STEP]
have "..."
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>set ts. ground x) = ((\<forall>x\<in>set Cs. ground_mctxt x) \<and> (\<forall>a\<in>set sss. \<forall>x\<in>set a. ground x))
[PROOF STEP]
unfolding conv[of ts] conv[of Cs] conv[of sss] len
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>{ts ! i |i. i < length Cs}. ground x) = ((\<forall>x\<in>{Cs ! i |i. i < length Cs}. ground_mctxt x) \<and> (\<forall>a\<in>{sss ! i |i. i < length Cs}. \<forall>x\<in>set a. ground x))
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
?i2 < length Cs \<Longrightarrow> ground (ts ! ?i2) = (ground_mctxt (Cs ! ?i2) \<and> (\<forall>a\<in>set (sss ! ?i2). ground a))

goal (1 subgoal):
 1. (\<forall>x\<in>{ts ! i |i. i < length Cs}. ground x) = ((\<forall>x\<in>{Cs ! i |i. i < length Cs}. ground_mctxt x) \<and> (\<forall>a\<in>{sss ! i |i. i < length Cs}. \<forall>x\<in>set a. ground x))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>set ts. ground x) = ((\<forall>x\<in>set Cs. ground_mctxt x) \<and> (\<forall>a\<in>set sss. \<forall>x\<in>set a. ground x))

goal (1 subgoal):
 1. \<And>x1a x2 t ss. \<lbrakk>\<And>x2a t ss. \<lbrakk>x2a \<in> set x2; t =\<^sub>f (x2a, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt x2a \<and> Ball (set ss) ground); t =\<^sub>f (MFun x1a x2, ss)\<rbrakk> \<Longrightarrow> ground t = (ground_mctxt (MFun x1a x2) \<and> Ball (set ss) ground)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(ground s = (ground_mctxt (MFun f Cs) \<and> (\<forall>a\<in>set ss. ground a))) = (((\<forall>x\<in>set Cs. ground_mctxt x) \<and> (\<forall>a\<in>set sss. \<forall>x\<in>set a. ground x)) = ((\<forall>x\<in>set Cs. ground_mctxt x) \<and> (\<forall>a\<in>set sss. \<forall>x\<in>set a. ground x)))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(ground s = (ground_mctxt (MFun f Cs) \<and> (\<forall>a\<in>set ss. ground a))) = (((\<forall>x\<in>set Cs. ground_mctxt x) \<and> (\<forall>a\<in>set sss. \<forall>x\<in>set a. ground x)) = ((\<forall>x\<in>set Cs. ground_mctxt x) \<and> (\<forall>a\<in>set sss. \<forall>x\<in>set a. ground x)))

goal (1 subgoal):
 1. ground s = (ground_mctxt (MFun f Cs) \<and> (\<forall>a\<in>set ss. ground a))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ground s = (ground_mctxt (MFun f Cs) \<and> (\<forall>a\<in>set ss. ground a))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ground_fill_holes:
  assumes nh: "num_holes C = length ss"
  shows "ground (fill_holes C ss) = (ground_mctxt C \<and> (\<forall> s \<in> set ss. ground s))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground (fill_holes C ss) = (ground_mctxt C \<and> (\<forall>s\<in>set ss. ground s))
[PROOF STEP]
by (rule ground_eq_fill[OF eqfI[OF refl nh]])


[STATEMENT]
lemma split_vars_ground' [simp]:
  "ground_mctxt (fst (split_vars t))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ground_mctxt (fst (split_vars t))
[PROOF STEP]
by (induct t) auto


[STATEMENT]
lemma split_vars_funas_mctxt [simp]:
  "funas_mctxt (fst (split_vars t)) = funas_term t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_mctxt (fst (split_vars t)) = funas_term t
[PROOF STEP]
by (induct t) auto


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

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

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

goal (1 subgoal):
 1. C \<le> D \<Longrightarrow> less_eq_mctxt' C D
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. C \<le> D \<Longrightarrow> less_eq_mctxt' 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_mctxt' C D
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
C \<le> D
[PROOF STEP]
show "less_eq_mctxt' C D"
[PROOF STATE]
proof (prove)
using this:
C \<le> D

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma less_eq_mctxt_MHoleE2:
  assumes "C \<le> MHole"
  obtains (MHole) "C = MHole"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (C = MHole \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
C \<le> MHole

goal (1 subgoal):
 1. (C = MHole \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding less_eq_mctxt_prime
[PROOF STATE]
proof (prove)
using this:
less_eq_mctxt' C MHole

goal (1 subgoal):
 1. (C = MHole \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases C, auto)


[STATEMENT]
lemma less_eq_mctxt_MVarE2:
  assumes "C \<le> MVar v"
  obtains (MHole) "C = MHole" | (MVar) "C = MVar v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C = MHole \<Longrightarrow> thesis; C = MVar v \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
C \<le> MVar v

goal (1 subgoal):
 1. \<lbrakk>C = MHole \<Longrightarrow> thesis; C = MVar v \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding less_eq_mctxt_prime
[PROOF STATE]
proof (prove)
using this:
less_eq_mctxt' C (MVar v)

goal (1 subgoal):
 1. \<lbrakk>C = MHole \<Longrightarrow> thesis; C = MVar v \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (cases C) auto


[STATEMENT]
lemma less_eq_mctxt_MFunE2:
  assumes "C \<le> MFun f ds"
  obtains (MHole) "C = MHole"
    | (MFun) cs where "C = MFun f cs" "length cs = length ds" "\<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>C = MHole \<Longrightarrow> thesis; \<And>cs. \<lbrakk>C = MFun f cs; length cs = length ds; \<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
C \<le> MFun f ds

goal (1 subgoal):
 1. \<lbrakk>C = MHole \<Longrightarrow> thesis; \<And>cs. \<lbrakk>C = MFun f cs; length cs = length ds; \<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding less_eq_mctxt_prime
[PROOF STATE]
proof (prove)
using this:
less_eq_mctxt' C (MFun f ds)

goal (1 subgoal):
 1. \<lbrakk>C = MHole \<Longrightarrow> thesis; \<And>cs. \<lbrakk>C = MFun f cs; length cs = length ds; \<And>i. i < length cs \<Longrightarrow> less_eq_mctxt' (cs ! i) (ds ! i)\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (cases C) auto


[STATEMENT]
lemma less_eq_mctxt_MVarE1:
  assumes "MVar v \<le> D"
  obtains (MVar) "D = MVar v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (D = MVar v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
MVar v \<le> D

goal (1 subgoal):
 1. (D = MVar v \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases D) (auto elim: less_eq_mctxtE2)


[STATEMENT]
lemma MHole_Bot [simp]: "MHole \<le> D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. MHole \<le> D
[PROOF STEP]
by (simp add: less_eq_mctxt_intros(1))


[STATEMENT]
lemma less_eq_mctxt_MFunE1:
  assumes "MFun f cs \<le> D"
  obtains (MFun) ds where "D = MFun f ds" "length cs = length ds" "\<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>ds. \<lbrakk>D = MFun f ds; length cs = length ds; \<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
MFun f cs \<le> D

goal (1 subgoal):
 1. (\<And>ds. \<lbrakk>D = MFun f ds; length cs = length ds; \<And>i. i < length cs \<Longrightarrow> cs ! i \<le> ds ! i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases D) (auto elim: less_eq_mctxtE2)


[STATEMENT]
lemma length_unfill_holes [simp]:
  assumes "C \<le> mctxt_of_term t"
  shows "length (unfill_holes C t) = num_holes C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (unfill_holes C t) = num_holes C
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
C \<le> mctxt_of_term t

goal (1 subgoal):
 1. length (unfill_holes C t) = num_holes C
[PROOF STEP]
proof (induct C t rule: unfill_holes.induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> length (unfill_holes MHole t) = num_holes MHole
 2. \<And>w v. MVar w \<le> mctxt_of_term (Var v) \<Longrightarrow> length (unfill_holes (MVar w) (Var v)) = num_holes (MVar w)
 3. \<And>g Cs f ts. \<lbrakk>\<And>x. \<lbrakk>f = g \<and> length ts = length Cs; x \<in> set [0..<length ts]; Cs ! x \<le> mctxt_of_term (ts ! x)\<rbrakk> \<Longrightarrow> length (unfill_holes (Cs ! x) (ts ! x)) = num_holes (Cs ! x); MFun g Cs \<le> mctxt_of_term (Fun f ts)\<rbrakk> \<Longrightarrow> length (unfill_holes (MFun g Cs) (Fun f ts)) = num_holes (MFun g Cs)
 4. \<And>v va vb. MVar v \<le> mctxt_of_term (Fun va vb) \<Longrightarrow> length (unfill_holes (MVar v) (Fun va vb)) = num_holes (MVar v)
 5. \<And>v va vb. MFun v va \<le> mctxt_of_term (Var vb) \<Longrightarrow> length (unfill_holes (MFun v va) (Var vb)) = num_holes (MFun v va)
[PROOF STEP]
case (3 f Cs g ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>g = f \<and> length ts = length Cs; ?x \<in> set [0..<length ts]; Cs ! ?x \<le> mctxt_of_term (ts ! ?x)\<rbrakk> \<Longrightarrow> length (unfill_holes (Cs ! ?x) (ts ! ?x)) = num_holes (Cs ! ?x)
MFun f Cs \<le> mctxt_of_term (Fun g ts)

goal (5 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> length (unfill_holes MHole t) = num_holes MHole
 2. \<And>w v. MVar w \<le> mctxt_of_term (Var v) \<Longrightarrow> length (unfill_holes (MVar w) (Var v)) = num_holes (MVar w)
 3. \<And>g Cs f ts. \<lbrakk>\<And>x. \<lbrakk>f = g \<and> length ts = length Cs; x \<in> set [0..<length ts]; Cs ! x \<le> mctxt_of_term (ts ! x)\<rbrakk> \<Longrightarrow> length (unfill_holes (Cs ! x) (ts ! x)) = num_holes (Cs ! x); MFun g Cs \<le> mctxt_of_term (Fun f ts)\<rbrakk> \<Longrightarrow> length (unfill_holes (MFun g Cs) (Fun f ts)) = num_holes (MFun g Cs)
 4. \<And>v va vb. MVar v \<le> mctxt_of_term (Fun va vb) \<Longrightarrow> length (unfill_holes (MVar v) (Fun va vb)) = num_holes (MVar v)
 5. \<And>v va vb. MFun v va \<le> mctxt_of_term (Var vb) \<Longrightarrow> length (unfill_holes (MFun v va) (Var vb)) = num_holes (MFun v va)
[PROOF STEP]
with 3(1)[OF _ nth_mem] 3(2)
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>g = f \<and> length ts = length Cs; ?n1 < length [0..<length ts]; Cs ! ([0..<length ts] ! ?n1) \<le> mctxt_of_term (ts ! ([0..<length ts] ! ?n1))\<rbrakk> \<Longrightarrow> length (unfill_holes (Cs ! ([0..<length ts] ! ?n1)) (ts ! ([0..<length ts] ! ?n1))) = num_holes (Cs ! ([0..<length ts] ! ?n1))
MFun f Cs \<le> mctxt_of_term (Fun g ts)
\<lbrakk>g = f \<and> length ts = length Cs; ?x \<in> set [0..<length ts]; Cs ! ?x \<le> mctxt_of_term (ts ! ?x)\<rbrakk> \<Longrightarrow> length (unfill_holes (Cs ! ?x) (ts ! ?x)) = num_holes (Cs ! ?x)
MFun f Cs \<le> mctxt_of_term (Fun g ts)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>g = f \<and> length ts = length Cs; ?n1 < length [0..<length ts]; Cs ! ([0..<length ts] ! ?n1) \<le> mctxt_of_term (ts ! ([0..<length ts] ! ?n1))\<rbrakk> \<Longrightarrow> length (unfill_holes (Cs ! ([0..<length ts] ! ?n1)) (ts ! ([0..<length ts] ! ?n1))) = num_holes (Cs ! ([0..<length ts] ! ?n1))
MFun f Cs \<le> mctxt_of_term (Fun g ts)
\<lbrakk>g = f \<and> length ts = length Cs; ?x \<in> set [0..<length ts]; Cs ! ?x \<le> mctxt_of_term (ts ! ?x)\<rbrakk> \<Longrightarrow> length (unfill_holes (Cs ! ?x) (ts ! ?x)) = num_holes (Cs ! ?x)
MFun f Cs \<le> mctxt_of_term (Fun g ts)

goal (1 subgoal):
 1. length (unfill_holes (MFun f Cs) (Fun g ts)) = num_holes (MFun f Cs)
[PROOF STEP]
by (auto simp: less_eq_mctxt_def length_concat
      intro!: cong[of sum_list, OF refl] nth_equalityI elim!: nth_equalityE)
[PROOF STATE]
proof (state)
this:
length (unfill_holes (MFun f Cs) (Fun g ts)) = num_holes (MFun f Cs)

goal (4 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> length (unfill_holes MHole t) = num_holes MHole
 2. \<And>w v. MVar w \<le> mctxt_of_term (Var v) \<Longrightarrow> length (unfill_holes (MVar w) (Var v)) = num_holes (MVar w)
 3. \<And>v va vb. MVar v \<le> mctxt_of_term (Fun va vb) \<Longrightarrow> length (unfill_holes (MVar v) (Fun va vb)) = num_holes (MVar v)
 4. \<And>v va vb. MFun v va \<le> mctxt_of_term (Var vb) \<Longrightarrow> length (unfill_holes (MFun v va) (Var vb)) = num_holes (MFun v va)
[PROOF STEP]
qed (auto simp: less_eq_mctxt_def)


[STATEMENT]
lemma map_vars_mctxt_id [simp]:
  "map_vars_mctxt (\<lambda> x. x) C = C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_vars_mctxt (\<lambda>x. x) C = C
[PROOF STEP]
by (induct C, auto intro: nth_equalityI)


[STATEMENT]
lemma split_vars_eqf_subst_map_vars_term:
  "t \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars t)), map \<sigma> (snd (split_vars t)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars t)), map \<sigma> (snd (split_vars t)))
[PROOF STEP]
proof (induct t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. Var x \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars (Var x))), map \<sigma> (snd (split_vars (Var x))))
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> x2a \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars x2a)), map \<sigma> (snd (split_vars x2a)))) \<Longrightarrow> Fun x1a x2 \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars (Fun x1a x2))), map \<sigma> (snd (split_vars (Fun x1a x2))))
[PROOF STEP]
case (Fun f ts)
[PROOF STATE]
proof (state)
this:
?x2a \<in> set ts \<Longrightarrow> ?x2a \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars ?x2a)), map \<sigma> (snd (split_vars ?x2a)))

goal (2 subgoals):
 1. \<And>x. Var x \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars (Var x))), map \<sigma> (snd (split_vars (Var x))))
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> x2a \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars x2a)), map \<sigma> (snd (split_vars x2a)))) \<Longrightarrow> Fun x1a x2 \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars (Fun x1a x2))), map \<sigma> (snd (split_vars (Fun x1a x2))))
[PROOF STEP]
have "?case = (Fun f (map (\<lambda>t. t \<cdot> \<sigma>) ts)
    =\<^sub>f (MFun f (map (map_vars_mctxt vw \<circ> (fst \<circ> split_vars)) ts), concat (map (map \<sigma> \<circ> (snd \<circ> split_vars)) ts)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Fun f ts \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars (Fun f ts))), map \<sigma> (snd (split_vars (Fun f ts))))) = (Fun f (map (\<lambda>t. t \<cdot> \<sigma>) ts) =\<^sub>f (MFun f (map (map_vars_mctxt vw \<circ> (fst \<circ> split_vars)) ts), concat (map (map \<sigma> \<circ> (snd \<circ> split_vars)) ts)))
[PROOF STEP]
by (simp add: map_concat)
[PROOF STATE]
proof (state)
this:
(Fun f ts \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars (Fun f ts))), map \<sigma> (snd (split_vars (Fun f ts))))) = (Fun f (map (\<lambda>t. t \<cdot> \<sigma>) ts) =\<^sub>f (MFun f (map (map_vars_mctxt vw \<circ> (fst \<circ> split_vars)) ts), concat (map (map \<sigma> \<circ> (snd \<circ> split_vars)) ts)))

goal (2 subgoals):
 1. \<And>x. Var x \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars (Var x))), map \<sigma> (snd (split_vars (Var x))))
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> x2a \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars x2a)), map \<sigma> (snd (split_vars x2a)))) \<Longrightarrow> Fun x1a x2 \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars (Fun x1a x2))), map \<sigma> (snd (split_vars (Fun x1a x2))))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(Fun f ts \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars (Fun f ts))), map \<sigma> (snd (split_vars (Fun f ts))))) = (Fun f (map (\<lambda>t. t \<cdot> \<sigma>) ts) =\<^sub>f (MFun f (map (map_vars_mctxt vw \<circ> (fst \<circ> split_vars)) ts), concat (map (map \<sigma> \<circ> (snd \<circ> split_vars)) ts)))

goal (2 subgoals):
 1. \<And>x. Var x \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars (Var x))), map \<sigma> (snd (split_vars (Var x))))
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> x2a \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars x2a)), map \<sigma> (snd (split_vars x2a)))) \<Longrightarrow> Fun x1a x2 \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars (Fun x1a x2))), map \<sigma> (snd (split_vars (Fun x1a x2))))
[PROOF STEP]
have "..."
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fun f (map (\<lambda>t. t \<cdot> \<sigma>) ts) =\<^sub>f (MFun f (map (map_vars_mctxt vw \<circ> (fst \<circ> split_vars)) ts), concat (map (map \<sigma> \<circ> (snd \<circ> split_vars)) ts))
[PROOF STEP]
proof (rule eqf_MFunI, simp, simp, unfold length_map)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < length ts \<Longrightarrow> map (\<lambda>t. t \<cdot> \<sigma>) ts ! i =\<^sub>f (map (map_vars_mctxt vw \<circ> (fst \<circ> split_vars)) ts ! i, map (map \<sigma> \<circ> (snd \<circ> split_vars)) ts ! i)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i < length ts \<Longrightarrow> map (\<lambda>t. t \<cdot> \<sigma>) ts ! i =\<^sub>f (map (map_vars_mctxt vw \<circ> (fst \<circ> split_vars)) ts ! i, map (map \<sigma> \<circ> (snd \<circ> split_vars)) ts ! 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> map (\<lambda>t. t \<cdot> \<sigma>) ts ! i =\<^sub>f (map (map_vars_mctxt vw \<circ> (fst \<circ> split_vars)) ts ! i, map (map \<sigma> \<circ> (snd \<circ> split_vars)) ts ! i)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length ts
[PROOF STEP]
have mem: "ts ! i \<in> set ts"
[PROOF STATE]
proof (prove)
using this:
i < length ts

goal (1 subgoal):
 1. ts ! i \<in> set ts
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ts ! i \<in> set ts

goal (1 subgoal):
 1. \<And>i. i < length ts \<Longrightarrow> map (\<lambda>t. t \<cdot> \<sigma>) ts ! i =\<^sub>f (map (map_vars_mctxt vw \<circ> (fst \<circ> split_vars)) ts ! i, map (map \<sigma> \<circ> (snd \<circ> split_vars)) ts ! i)
[PROOF STEP]
show "map (\<lambda>t. t \<cdot> \<sigma>) ts ! i =\<^sub>f (map (map_vars_mctxt vw \<circ> (fst \<circ> split_vars)) ts ! i, map (map \<sigma> \<circ> (snd \<circ> split_vars)) ts ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>t. t \<cdot> \<sigma>) ts ! i =\<^sub>f (map (map_vars_mctxt vw \<circ> (fst \<circ> split_vars)) ts ! i, map (map \<sigma> \<circ> (snd \<circ> split_vars)) ts ! i)
[PROOF STEP]
using Fun[OF mem] i
[PROOF STATE]
proof (prove)
using this:
ts ! i \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars (ts ! i))), map \<sigma> (snd (split_vars (ts ! i))))
i < length ts

goal (1 subgoal):
 1. map (\<lambda>t. t \<cdot> \<sigma>) ts ! i =\<^sub>f (map (map_vars_mctxt vw \<circ> (fst \<circ> split_vars)) ts ! i, map (map \<sigma> \<circ> (snd \<circ> split_vars)) ts ! i)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (\<lambda>t. t \<cdot> \<sigma>) ts ! i =\<^sub>f (map (map_vars_mctxt vw \<circ> (fst \<circ> split_vars)) ts ! i, map (map \<sigma> \<circ> (snd \<circ> split_vars)) ts ! i)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Fun f (map (\<lambda>t. t \<cdot> \<sigma>) ts) =\<^sub>f (MFun f (map (map_vars_mctxt vw \<circ> (fst \<circ> split_vars)) ts), concat (map (map \<sigma> \<circ> (snd \<circ> split_vars)) ts))

goal (2 subgoals):
 1. \<And>x. Var x \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars (Var x))), map \<sigma> (snd (split_vars (Var x))))
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> x2a \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars x2a)), map \<sigma> (snd (split_vars x2a)))) \<Longrightarrow> Fun x1a x2 \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars (Fun x1a x2))), map \<sigma> (snd (split_vars (Fun x1a x2))))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Fun f ts \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars (Fun f ts))), map \<sigma> (snd (split_vars (Fun f ts))))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Fun f ts \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars (Fun f ts))), map \<sigma> (snd (split_vars (Fun f ts))))

goal (1 subgoal):
 1. Fun f ts \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars (Fun f ts))), map \<sigma> (snd (split_vars (Fun f ts))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Fun f ts \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars (Fun f ts))), map \<sigma> (snd (split_vars (Fun f ts))))

goal (1 subgoal):
 1. \<And>x. Var x \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt vw (fst (split_vars (Var x))), map \<sigma> (snd (split_vars (Var x))))
[PROOF STEP]
qed auto


[STATEMENT]
lemma split_vars_eqf_subst: "t \<cdot> \<sigma> =\<^sub>f (fst (split_vars t), (map \<sigma> (snd (split_vars t))))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. t \<cdot> \<sigma> =\<^sub>f (fst (split_vars t), map \<sigma> (snd (split_vars t)))
[PROOF STEP]
using split_vars_eqf_subst_map_vars_term[of t \<sigma> "\<lambda> x. x"]
[PROOF STATE]
proof (prove)
using this:
t \<cdot> \<sigma> =\<^sub>f (map_vars_mctxt (\<lambda>x. x) (fst (split_vars t)), map \<sigma> (snd (split_vars t)))

goal (1 subgoal):
 1. t \<cdot> \<sigma> =\<^sub>f (fst (split_vars t), map \<sigma> (snd (split_vars t)))
[PROOF STEP]
by simp


[STATEMENT]
lemma split_vars_fill_holes:
  assumes "C = fst (split_vars s)" and "ss = map Var (snd (split_vars s))"
  shows "fill_holes C ss = s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_holes C ss = s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
C = fst (split_vars s)
ss = map Var (snd (split_vars s))

goal (1 subgoal):
 1. fill_holes C ss = s
[PROOF STEP]
by (metis eqfE(1) split_vars_eqf_subst subst_apply_term_empty)


[STATEMENT]
lemma fill_unfill_holes:
  assumes "C \<le> mctxt_of_term t"
  shows "fill_holes C (unfill_holes C t) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_holes C (unfill_holes C t) = t
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
C \<le> mctxt_of_term t

goal (1 subgoal):
 1. fill_holes C (unfill_holes C t) = t
[PROOF STEP]
proof (induct C t rule: unfill_holes.induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> fill_holes MHole (unfill_holes MHole t) = t
 2. \<And>w v. MVar w \<le> mctxt_of_term (Var v) \<Longrightarrow> fill_holes (MVar w) (unfill_holes (MVar w) (Var v)) = Var v
 3. \<And>g Cs f ts. \<lbrakk>\<And>x. \<lbrakk>f = g \<and> length ts = length Cs; x \<in> set [0..<length ts]; Cs ! x \<le> mctxt_of_term (ts ! x)\<rbrakk> \<Longrightarrow> fill_holes (Cs ! x) (unfill_holes (Cs ! x) (ts ! x)) = ts ! x; MFun g Cs \<le> mctxt_of_term (Fun f ts)\<rbrakk> \<Longrightarrow> fill_holes (MFun g Cs) (unfill_holes (MFun g Cs) (Fun f ts)) = Fun f ts
 4. \<And>v va vb. MVar v \<le> mctxt_of_term (Fun va vb) \<Longrightarrow> fill_holes (MVar v) (unfill_holes (MVar v) (Fun va vb)) = Fun va vb
 5. \<And>v va vb. MFun v va \<le> mctxt_of_term (Var vb) \<Longrightarrow> fill_holes (MFun v va) (unfill_holes (MFun v va) (Var vb)) = Var vb
[PROOF STEP]
case (3 f Cs g ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>g = f \<and> length ts = length Cs; ?x \<in> set [0..<length ts]; Cs ! ?x \<le> mctxt_of_term (ts ! ?x)\<rbrakk> \<Longrightarrow> fill_holes (Cs ! ?x) (unfill_holes (Cs ! ?x) (ts ! ?x)) = ts ! ?x
MFun f Cs \<le> mctxt_of_term (Fun g ts)

goal (5 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> fill_holes MHole (unfill_holes MHole t) = t
 2. \<And>w v. MVar w \<le> mctxt_of_term (Var v) \<Longrightarrow> fill_holes (MVar w) (unfill_holes (MVar w) (Var v)) = Var v
 3. \<And>g Cs f ts. \<lbrakk>\<And>x. \<lbrakk>f = g \<and> length ts = length Cs; x \<in> set [0..<length ts]; Cs ! x \<le> mctxt_of_term (ts ! x)\<rbrakk> \<Longrightarrow> fill_holes (Cs ! x) (unfill_holes (Cs ! x) (ts ! x)) = ts ! x; MFun g Cs \<le> mctxt_of_term (Fun f ts)\<rbrakk> \<Longrightarrow> fill_holes (MFun g Cs) (unfill_holes (MFun g Cs) (Fun f ts)) = Fun f ts
 4. \<And>v va vb. MVar v \<le> mctxt_of_term (Fun va vb) \<Longrightarrow> fill_holes (MVar v) (unfill_holes (MVar v) (Fun va vb)) = Fun va vb
 5. \<And>v va vb. MFun v va \<le> mctxt_of_term (Var vb) \<Longrightarrow> fill_holes (MFun v va) (unfill_holes (MFun v va) (Var vb)) = Var vb
[PROOF STEP]
with 3(1)[OF _ nth_mem] 3(2)
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>g = f \<and> length ts = length Cs; ?n1 < length [0..<length ts]; Cs ! ([0..<length ts] ! ?n1) \<le> mctxt_of_term (ts ! ([0..<length ts] ! ?n1))\<rbrakk> \<Longrightarrow> fill_holes (Cs ! ([0..<length ts] ! ?n1)) (unfill_holes (Cs ! ([0..<length ts] ! ?n1)) (ts ! ([0..<length ts] ! ?n1))) = ts ! ([0..<length ts] ! ?n1)
MFun f Cs \<le> mctxt_of_term (Fun g ts)
\<lbrakk>g = f \<and> length ts = length Cs; ?x \<in> set [0..<length ts]; Cs ! ?x \<le> mctxt_of_term (ts ! ?x)\<rbrakk> \<Longrightarrow> fill_holes (Cs ! ?x) (unfill_holes (Cs ! ?x) (ts ! ?x)) = ts ! ?x
MFun f Cs \<le> mctxt_of_term (Fun g ts)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>g = f \<and> length ts = length Cs; ?n1 < length [0..<length ts]; Cs ! ([0..<length ts] ! ?n1) \<le> mctxt_of_term (ts ! ([0..<length ts] ! ?n1))\<rbrakk> \<Longrightarrow> fill_holes (Cs ! ([0..<length ts] ! ?n1)) (unfill_holes (Cs ! ([0..<length ts] ! ?n1)) (ts ! ([0..<length ts] ! ?n1))) = ts ! ([0..<length ts] ! ?n1)
MFun f Cs \<le> mctxt_of_term (Fun g ts)
\<lbrakk>g = f \<and> length ts = length Cs; ?x \<in> set [0..<length ts]; Cs ! ?x \<le> mctxt_of_term (ts ! ?x)\<rbrakk> \<Longrightarrow> fill_holes (Cs ! ?x) (unfill_holes (Cs ! ?x) (ts ! ?x)) = ts ! ?x
MFun f Cs \<le> mctxt_of_term (Fun g ts)

goal (1 subgoal):
 1. fill_holes (MFun f Cs) (unfill_holes (MFun f Cs) (Fun g ts)) = Fun g ts
[PROOF STEP]
by (auto simp: less_eq_mctxt_def intro!: fill_holes_arbitrary elim!: nth_equalityE)
[PROOF STATE]
proof (state)
this:
fill_holes (MFun f Cs) (unfill_holes (MFun f Cs) (Fun g ts)) = Fun g ts

goal (4 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> fill_holes MHole (unfill_holes MHole t) = t
 2. \<And>w v. MVar w \<le> mctxt_of_term (Var v) \<Longrightarrow> fill_holes (MVar w) (unfill_holes (MVar w) (Var v)) = Var v
 3. \<And>v va vb. MVar v \<le> mctxt_of_term (Fun va vb) \<Longrightarrow> fill_holes (MVar v) (unfill_holes (MVar v) (Fun va vb)) = Fun va vb
 4. \<And>v va vb. MFun v va \<le> mctxt_of_term (Var vb) \<Longrightarrow> fill_holes (MFun v va) (unfill_holes (MFun v va) (Var vb)) = Var vb
[PROOF STEP]
qed (auto simp: less_eq_mctxt_def split: if_splits)


[STATEMENT]
lemma hole_poss_list_length:
  "length (hole_poss_list D) = num_holes D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (hole_poss_list D) = num_holes D
[PROOF STEP]
by (induct D) (auto simp: length_concat intro!: nth_sum_listI)


[STATEMENT]
lemma unfill_holles_hole_poss_list_length:
  assumes "C \<le> mctxt_of_term t"
  shows "length (unfill_holes C t) = length (hole_poss_list C)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (unfill_holes C t) = length (hole_poss_list C)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
C \<le> mctxt_of_term t

goal (1 subgoal):
 1. length (unfill_holes C t) = length (hole_poss_list C)
[PROOF STEP]
proof (induct C arbitrary: t)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x t. MVar x \<le> mctxt_of_term t \<Longrightarrow> length (unfill_holes (MVar x) t) = length (hole_poss_list (MVar x))
 2. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> length (unfill_holes MHole t) = length (hole_poss_list MHole)
 3. \<And>x1a x2 t. \<lbrakk>\<And>x2a t. \<lbrakk>x2a \<in> set x2; x2a \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> length (unfill_holes x2a t) = length (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> length (unfill_holes (MFun x1a x2) t) = length (hole_poss_list (MFun x1a x2))
[PROOF STEP]
case (MVar x)
[PROOF STATE]
proof (state)
this:
MVar x \<le> mctxt_of_term t

goal (3 subgoals):
 1. \<And>x t. MVar x \<le> mctxt_of_term t \<Longrightarrow> length (unfill_holes (MVar x) t) = length (hole_poss_list (MVar x))
 2. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> length (unfill_holes MHole t) = length (hole_poss_list MHole)
 3. \<And>x1a x2 t. \<lbrakk>\<And>x2a t. \<lbrakk>x2a \<in> set x2; x2a \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> length (unfill_holes x2a t) = length (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> length (unfill_holes (MFun x1a x2) t) = length (hole_poss_list (MFun x1a x2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
MVar x \<le> mctxt_of_term t
[PROOF STEP]
have [simp]: "t = Var x"
[PROOF STATE]
proof (prove)
using this:
MVar x \<le> mctxt_of_term t

goal (1 subgoal):
 1. t = Var x
[PROOF STEP]
by (cases t) (auto dest: less_eq_mctxt_MVarE1)
[PROOF STATE]
proof (state)
this:
t = Var x

goal (3 subgoals):
 1. \<And>x t. MVar x \<le> mctxt_of_term t \<Longrightarrow> length (unfill_holes (MVar x) t) = length (hole_poss_list (MVar x))
 2. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> length (unfill_holes MHole t) = length (hole_poss_list MHole)
 3. \<And>x1a x2 t. \<lbrakk>\<And>x2a t. \<lbrakk>x2a \<in> set x2; x2a \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> length (unfill_holes x2a t) = length (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> length (unfill_holes (MFun x1a x2) t) = length (hole_poss_list (MFun x1a x2))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (unfill_holes (MVar x) t) = length (hole_poss_list (MVar x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (unfill_holes (MVar x) t) = length (hole_poss_list (MVar x))

goal (2 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> length (unfill_holes MHole t) = length (hole_poss_list MHole)
 2. \<And>x1a x2 t. \<lbrakk>\<And>x2a t. \<lbrakk>x2a \<in> set x2; x2a \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> length (unfill_holes x2a t) = length (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> length (unfill_holes (MFun x1a x2) t) = length (hole_poss_list (MFun x1a x2))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> length (unfill_holes MHole t) = length (hole_poss_list MHole)
 2. \<And>x1a x2 t. \<lbrakk>\<And>x2a t. \<lbrakk>x2a \<in> set x2; x2a \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> length (unfill_holes x2a t) = length (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> length (unfill_holes (MFun x1a x2) t) = length (hole_poss_list (MFun x1a x2))
[PROOF STEP]
case (MFun f ts)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set ts; ?x2a \<le> mctxt_of_term ?t\<rbrakk> \<Longrightarrow> length (unfill_holes ?x2a ?t) = length (hole_poss_list ?x2a)
MFun f ts \<le> mctxt_of_term t

goal (2 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> length (unfill_holes MHole t) = length (hole_poss_list MHole)
 2. \<And>x1a x2 t. \<lbrakk>\<And>x2a t. \<lbrakk>x2a \<in> set x2; x2a \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> length (unfill_holes x2a t) = length (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> length (unfill_holes (MFun x1a x2) t) = length (hole_poss_list (MFun x1a x2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x2a \<in> set ts; ?x2a \<le> mctxt_of_term ?t\<rbrakk> \<Longrightarrow> length (unfill_holes ?x2a ?t) = length (hole_poss_list ?x2a)
MFun f ts \<le> mctxt_of_term t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set ts; ?x2a \<le> mctxt_of_term ?t\<rbrakk> \<Longrightarrow> length (unfill_holes ?x2a ?t) = length (hole_poss_list ?x2a)
MFun f ts \<le> mctxt_of_term t

goal (1 subgoal):
 1. length (unfill_holes (MFun f ts) t) = length (hole_poss_list (MFun f ts))
[PROOF STEP]
by (cases t) (auto simp: length_concat comp_def
      elim!: less_eq_mctxt_MFunE1 less_eq_mctxt_MVarE1 intro!: nth_sum_listI)
[PROOF STATE]
proof (state)
this:
length (unfill_holes (MFun f ts) t) = length (hole_poss_list (MFun f ts))

goal (1 subgoal):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> length (unfill_holes MHole t) = length (hole_poss_list MHole)
[PROOF STEP]
qed auto