[STATEMENT]
lemma perIT_concat:" perInsTrans s t \<Longrightarrow> perInsTrans t u \<Longrightarrow> perInsTrans s u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>perInsTrans s t; perInsTrans t u\<rbrakk> \<Longrightarrow> perInsTrans s u
[PROOF STEP]
by (induction s t rule: perInsTrans.induct) (simp add: perInsTrans.intros)+


[STATEMENT]
lemma assumes "invar_vebt t n " shows
  "perInsTrans (vebt_buildup n) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. perInsTrans (vebt_buildup n) t
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. perInsTrans (vebt_buildup n) t
[PROOF STEP]
have "finite A \<Longrightarrow>invar_vebt s n \<Longrightarrow>set_vebt' s = B \<Longrightarrow> B\<subseteq> A \<Longrightarrow> perInsTrans (vebt_buildup n) s" for s A B
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s
[PROOF STEP]
proof (induction "card B" arbitrary: s B)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>B s. \<lbrakk>0 = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s
 2. \<And>x B s. \<lbrakk>\<And>B s. \<lbrakk>x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s; Suc x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
0 = card B
finite A
invar_vebt s n
set_vebt' s = B
B \<subseteq> A

goal (2 subgoals):
 1. \<And>B s. \<lbrakk>0 = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s
 2. \<And>x B s. \<lbrakk>\<And>B s. \<lbrakk>x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s; Suc x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 = card B
finite A
invar_vebt s n
set_vebt' s = B
B \<subseteq> A
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 = card B
finite A
invar_vebt s n
set_vebt' s = B
B \<subseteq> A

goal (1 subgoal):
 1. perInsTrans (vebt_buildup n) s
[PROOF STEP]
by (metis buildup_gives_empty buildup_gives_valid card_eq_0_iff deg_not_0 perInsTrans.intros(1) set_vebt_finite uniquetree)
[PROOF STATE]
proof (state)
this:
perInsTrans (vebt_buildup n) s

goal (1 subgoal):
 1. \<And>x B s. \<lbrakk>\<And>B s. \<lbrakk>x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s; Suc x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x B s. \<lbrakk>\<And>B s. \<lbrakk>x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s; Suc x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s
[PROOF STEP]
case (Suc car)
[PROOF STATE]
proof (state)
this:
\<lbrakk>car = card ?B; finite A; invar_vebt ?s n; set_vebt' ?s = ?B; ?B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) ?s
Suc car = card B
finite A
invar_vebt s n
set_vebt' s = B
B \<subseteq> A

goal (1 subgoal):
 1. \<And>x B s. \<lbrakk>\<And>B s. \<lbrakk>x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s; Suc x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s
[PROOF STEP]
hence "finite B"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>car = card ?B; finite A; invar_vebt ?s n; set_vebt' ?s = ?B; ?B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) ?s
Suc car = card B
finite A
invar_vebt s n
set_vebt' s = B
B \<subseteq> A

goal (1 subgoal):
 1. finite B
[PROOF STEP]
by (meson rev_finite_subset)
[PROOF STATE]
proof (state)
this:
finite B

goal (1 subgoal):
 1. \<And>x B s. \<lbrakk>\<And>B s. \<lbrakk>x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s; Suc x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s
[PROOF STEP]
obtain x b where "B = insert x b \<and> x \<notin> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x b. B = insert x b \<and> x \<notin> b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis Suc.hyps(2) card_Suc_eq)
[PROOF STATE]
proof (state)
this:
B = insert x b \<and> x \<notin> b

goal (1 subgoal):
 1. \<And>x B s. \<lbrakk>\<And>B s. \<lbrakk>x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s; Suc x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s
[PROOF STEP]
have "set_vebt' (vebt_delete s x) = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set_vebt' (vebt_delete s x) = b
[PROOF STEP]
using Suc.prems(2) Suc.prems(3) \<open>B = insert x b \<and> x \<notin> b\<close> delete_correct'
[PROOF STATE]
proof (prove)
using this:
invar_vebt s n
set_vebt' s = B
B = insert x b \<and> x \<notin> b
invar_vebt ?t ?n \<Longrightarrow> set_vebt' (vebt_delete ?t ?x) = set_vebt' ?t - {?x}

goal (1 subgoal):
 1. set_vebt' (vebt_delete s x) = b
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
set_vebt' (vebt_delete s x) = b

goal (1 subgoal):
 1. \<And>x B s. \<lbrakk>\<And>B s. \<lbrakk>x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s; Suc x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
set_vebt' (vebt_delete s x) = b

goal (1 subgoal):
 1. \<And>x B s. \<lbrakk>\<And>B s. \<lbrakk>x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s; Suc x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s
[PROOF STEP]
hence "perInsTrans (vebt_buildup n) (vebt_delete s x)"
[PROOF STATE]
proof (prove)
using this:
set_vebt' (vebt_delete s x) = b

goal (1 subgoal):
 1. perInsTrans (vebt_buildup n) (vebt_delete s x)
[PROOF STEP]
by (metis Suc.hyps(1) Suc.hyps(2) Suc.prems(1) Suc.prems(2) Suc.prems(4) \<open>B = insert x b \<and> x \<notin> b\<close> \<open>finite B\<close> card_insert_disjoint delete_pres_valid finite_insert nat.inject subset_insertI subset_trans)
[PROOF STATE]
proof (state)
this:
perInsTrans (vebt_buildup n) (vebt_delete s x)

goal (1 subgoal):
 1. \<And>x B s. \<lbrakk>\<And>B s. \<lbrakk>x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s; Suc x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s
[PROOF STEP]
hence "set_vebt' (vebt_insert (vebt_delete s x) x) = set_vebt' s"
[PROOF STATE]
proof (prove)
using this:
perInsTrans (vebt_buildup n) (vebt_delete s x)

goal (1 subgoal):
 1. set_vebt' (vebt_insert (vebt_delete s x) x) = set_vebt' s
[PROOF STEP]
by (metis Diff_insert_absorb Suc.prems(2) Suc.prems(3) Un_insert_right \<open>B = insert x b \<and> x \<notin> b\<close> boolean_algebra_cancel.sup0 delete_pres_valid delete_correct' insertI1 insert_corr mem_Collect_eq member_bound set_vebt'_def)
[PROOF STATE]
proof (state)
this:
set_vebt' (vebt_insert (vebt_delete s x) x) = set_vebt' s

goal (1 subgoal):
 1. \<And>x B s. \<lbrakk>\<And>B s. \<lbrakk>x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s; Suc x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s
[PROOF STEP]
have "invar_vebt (vebt_insert (vebt_delete s x) x) n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invar_vebt (vebt_insert (vebt_delete s x) x) n
[PROOF STEP]
by (metis Suc.prems(2) Suc.prems(3) \<open>B = insert x b \<and> x \<notin> b\<close> delete_pres_valid insertI1 mem_Collect_eq member_bound set_vebt'_def valid_pres_insert)
[PROOF STATE]
proof (state)
this:
invar_vebt (vebt_insert (vebt_delete s x) x) n

goal (1 subgoal):
 1. \<And>x B s. \<lbrakk>\<And>B s. \<lbrakk>x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s; Suc x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
invar_vebt (vebt_insert (vebt_delete s x) x) n

goal (1 subgoal):
 1. \<And>x B s. \<lbrakk>\<And>B s. \<lbrakk>x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s; Suc x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s
[PROOF STEP]
hence "vebt_insert (vebt_delete s x) x = s"
[PROOF STATE]
proof (prove)
using this:
invar_vebt (vebt_insert (vebt_delete s x) x) n

goal (1 subgoal):
 1. vebt_insert (vebt_delete s x) x = s
[PROOF STEP]
using Suc.prems(2) \<open>set_vebt' (VEBT_Insert.vebt_insert (vebt_delete s x) x) = set_vebt' s\<close> uniquetree
[PROOF STATE]
proof (prove)
using this:
invar_vebt (vebt_insert (vebt_delete s x) x) n
invar_vebt s n
set_vebt' (vebt_insert (vebt_delete s x) x) = set_vebt' s
\<lbrakk>invar_vebt ?t ?n; invar_vebt ?s ?n; set_vebt' ?t = set_vebt' ?s\<rbrakk> \<Longrightarrow> ?s = ?t

goal (1 subgoal):
 1. vebt_insert (vebt_delete s x) x = s
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
vebt_insert (vebt_delete s x) x = s

goal (1 subgoal):
 1. \<And>x B s. \<lbrakk>\<And>B s. \<lbrakk>x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s; Suc x = card B; finite A; invar_vebt s n; set_vebt' s = B; B \<subseteq> A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) s
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
set_vebt' (vebt_delete s x) = b
invar_vebt (vebt_insert (vebt_delete s x) x) n
vebt_insert (vebt_delete s x) x = s
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
set_vebt' (vebt_delete s x) = b
invar_vebt (vebt_insert (vebt_delete s x) x) n
vebt_insert (vebt_delete s x) x = s

goal (1 subgoal):
 1. perInsTrans (vebt_buildup n) s
[PROOF STEP]
by (metis \<open>perInsTrans (vebt_buildup n) (vebt_delete s x)\<close> perIT_concat perInsTrans.intros(1) perInsTrans.intros(2))
[PROOF STATE]
proof (state)
this:
perInsTrans (vebt_buildup n) s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<lbrakk>finite ?A; invar_vebt ?s n; set_vebt' ?s = ?B; ?B \<subseteq> ?A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) ?s

goal (1 subgoal):
 1. perInsTrans (vebt_buildup n) t
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>finite ?A; invar_vebt ?s n; set_vebt' ?s = ?B; ?B \<subseteq> ?A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) ?s
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>finite ?A; invar_vebt ?s n; set_vebt' ?s = ?B; ?B \<subseteq> ?A\<rbrakk> \<Longrightarrow> perInsTrans (vebt_buildup n) ?s

goal (1 subgoal):
 1. perInsTrans (vebt_buildup n) t
[PROOF STEP]
by (meson assms equalityD1 set_vebt_finite)
[PROOF STATE]
proof (state)
this:
perInsTrans (vebt_buildup n) t

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ahm_invar_impl_of [simp, intro]: "ArrayHashMap_Impl.ahm_invar (impl_of hm)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ArrayHashMap_Impl.ahm_invar (impl_of hm)
[PROOF STEP]
using impl_of[of hm]
[PROOF STATE]
proof (prove)
using this:
impl_of hm \<in> {hm. ArrayHashMap_Impl.ahm_invar hm}

goal (1 subgoal):
 1. ArrayHashMap_Impl.ahm_invar (impl_of hm)
[PROOF STEP]
by simp


[STATEMENT]
lemma HashMap_impl_of [code abstype]: "HashMap (impl_of t) = t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. HashMap (impl_of t) = t
[PROOF STEP]
by(rule impl_of_inverse)


[STATEMENT]
lemma impl_of_ahm_empty [code abstract]:
  "impl_of ahm_empty_const = ArrayHashMap_Impl.ahm_empty ()"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. impl_of ahm_empty_const = ArrayHashMap_Impl.ahm_empty ()
[PROOF STEP]
by(simp add: ahm_empty_const_def HashMap_inverse)


[STATEMENT]
lemma impl_of_ahm_update [code abstract]:
  "impl_of (ahm_update k v hm) = ArrayHashMap_Impl.ahm_update k v (impl_of hm)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. impl_of (ahm_update k v hm) = ArrayHashMap_Impl.ahm_update k v (impl_of hm)
[PROOF STEP]
by(simp add: ahm_update_def HashMap_inverse ahm_update_correct)


[STATEMENT]
lemma impl_of_ahm_delete [code abstract]:
  "impl_of (ahm_delete k hm) = ArrayHashMap_Impl.ahm_delete k (impl_of hm)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. impl_of (ahm_delete k hm) = ArrayHashMap_Impl.ahm_delete k (impl_of hm)
[PROOF STEP]
by(simp add: ahm_delete_def HashMap_inverse ahm_delete_correct)


[STATEMENT]
lemma finite_dom_ahm_\<alpha>[simp]: "finite (dom (ahm_\<alpha> hm))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (dom (ahm_\<alpha> hm))
[PROOF STEP]
by (simp add: ahm_\<alpha>_def finite_dom_ahm_\<alpha>)


[STATEMENT]
lemma ahm_empty_correct[simp]: "ahm_\<alpha> (ahm_empty ()) = Map.empty"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ahm_\<alpha> (ahm_empty ()) = Map.empty
[PROOF STEP]
by(simp add: ahm_\<alpha>_def ahm_empty_def ahm_empty_const_def HashMap_inverse)


[STATEMENT]
lemma ahm_lookup_correct[simp]: "ahm_lookup k m = ahm_\<alpha> m k"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ahm_lookup k m = ahm_\<alpha> m k
[PROOF STEP]
by (simp add: ahm_lookup_def ArrayHashMap_Impl.ahm_lookup_def ahm_\<alpha>_def)


[STATEMENT]
lemma ahm_update_correct[simp]: "ahm_\<alpha> (ahm_update k v hm) = (ahm_\<alpha> hm)(k \<mapsto> v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ahm_\<alpha> (ahm_update k v hm) = ahm_\<alpha> hm(k \<mapsto> v)
[PROOF STEP]
by (simp add: ahm_\<alpha>_def ahm_update_def ahm_update_correct HashMap_inverse)


[STATEMENT]
lemma ahm_delete_correct[simp]:
  "ahm_\<alpha> (ahm_delete k hm) = (ahm_\<alpha> hm) |` (- {k})"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ahm_\<alpha> (ahm_delete k hm) = ahm_\<alpha> hm |` (- {k})
[PROOF STEP]
by (simp add: ahm_\<alpha>_def ahm_delete_def HashMap_inverse ahm_delete_correct)


[STATEMENT]
lemma ahm_iteratei_impl[simp]: "map_iterator (ahm_iteratei m) (ahm_\<alpha> m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_iterator (ahm_iteratei m) (ahm_\<alpha> m)
[PROOF STEP]
unfolding ahm_iteratei_def ahm_\<alpha>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map_iterator (ArrayHashMap_Impl.ahm_iteratei (impl_of m)) (ArrayHashMap_Impl.ahm_\<alpha> (impl_of m))
[PROOF STEP]
apply (rule ahm_iteratei_correct)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ArrayHashMap_Impl.ahm_invar (impl_of m)
[PROOF STEP]
by simp


[STATEMENT]
lemma pi_ahm[proper_it]:
  "proper_it' ahm_iteratei ahm_iteratei"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it' ahm_iteratei ahm_iteratei
[PROOF STEP]
unfolding ahm_iteratei_def[abs_def]
    ArrayHashMap_Impl.ahm_iteratei_def ArrayHashMap_Impl.ahm_iteratei_aux_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. proper_it' (\<lambda>hm. rec_hashmap (\<lambda>a n. rec_array (\<lambda>xs. foldli (concat xs)) a) (impl_of hm)) (\<lambda>hm. rec_hashmap (\<lambda>a n. rec_array (\<lambda>xs. foldli (concat xs)) a) (impl_of hm))
[PROOF STEP]
apply (rule proper_it'I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s. proper_it (rec_hashmap (\<lambda>a n. rec_array (\<lambda>xs. foldli (concat xs)) a) (impl_of s)) (rec_hashmap (\<lambda>a n. rec_array (\<lambda>xs. foldli (concat xs)) a) (impl_of s))
[PROOF STEP]
apply (case_tac "impl_of s")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2. impl_of s = ArrayHashMap_Impl.hashmap.HashMap x1 x2 \<Longrightarrow> proper_it (rec_hashmap (\<lambda>a n. rec_array (\<lambda>xs. foldli (concat xs)) a) (impl_of s)) (rec_hashmap (\<lambda>a n. rec_array (\<lambda>xs. foldli (concat xs)) a) (impl_of s))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s x1 x2. impl_of s = ArrayHashMap_Impl.hashmap.HashMap x1 x2 \<Longrightarrow> proper_it (case x1 of Array xs \<Rightarrow> foldli (concat xs)) (case x1 of Array xs \<Rightarrow> foldli (concat xs))
[PROOF STEP]
apply (rename_tac array nat)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s array nat. impl_of s = ArrayHashMap_Impl.hashmap.HashMap array nat \<Longrightarrow> proper_it (case array of Array xs \<Rightarrow> foldli (concat xs)) (case array of Array xs \<Rightarrow> foldli (concat xs))
[PROOF STEP]
apply (case_tac array)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s array nat x. \<lbrakk>impl_of s = ArrayHashMap_Impl.hashmap.HashMap array nat; array = Array x\<rbrakk> \<Longrightarrow> proper_it (case array of Array xs \<Rightarrow> foldli (concat xs)) (case array of Array xs \<Rightarrow> foldli (concat xs))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s array nat x. \<lbrakk>impl_of s = ArrayHashMap_Impl.hashmap.HashMap (Array x) nat; array = Array x\<rbrakk> \<Longrightarrow> proper_it (foldli (concat x)) (foldli (concat x))
[PROOF STEP]
by (intro icf_proper_iteratorI)


[STATEMENT]
lemma concat_nth:
  assumes "m < length xs" and "n < length (xs ! m)"
    and "i = sum_list (map length (take m xs)) + n"
  shows "concat xs ! i = xs ! m ! n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concat xs ! i = xs ! m ! n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m < length xs
n < length (xs ! m)
i = sum_list (map length (take m xs)) + n

goal (1 subgoal):
 1. concat xs ! i = xs ! m ! n
[PROOF STEP]
proof (induct xs arbitrary: m n i)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m n i. \<lbrakk>m < length []; n < length ([] ! m); i = sum_list (map length (take m [])) + n\<rbrakk> \<Longrightarrow> concat [] ! i = [] ! m ! n
 2. \<And>a xs m n i. \<lbrakk>\<And>m n i. \<lbrakk>m < length xs; n < length (xs ! m); i = sum_list (map length (take m xs)) + n\<rbrakk> \<Longrightarrow> concat xs ! i = xs ! m ! n; m < length (a # xs); n < length ((a # xs) ! m); i = sum_list (map length (take m (a # xs))) + n\<rbrakk> \<Longrightarrow> concat (a # xs) ! i = (a # xs) ! m ! n
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?m < length xs; ?n < length (xs ! ?m); ?i = sum_list (map length (take ?m xs)) + ?n\<rbrakk> \<Longrightarrow> concat xs ! ?i = xs ! ?m ! ?n
m < length (x # xs)
n < length ((x # xs) ! m)
i = sum_list (map length (take m (x # xs))) + n

goal (2 subgoals):
 1. \<And>m n i. \<lbrakk>m < length []; n < length ([] ! m); i = sum_list (map length (take m [])) + n\<rbrakk> \<Longrightarrow> concat [] ! i = [] ! m ! n
 2. \<And>a xs m n i. \<lbrakk>\<And>m n i. \<lbrakk>m < length xs; n < length (xs ! m); i = sum_list (map length (take m xs)) + n\<rbrakk> \<Longrightarrow> concat xs ! i = xs ! m ! n; m < length (a # xs); n < length ((a # xs) ! m); i = sum_list (map length (take m (a # xs))) + n\<rbrakk> \<Longrightarrow> concat (a # xs) ! i = (a # xs) ! m ! n
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. concat (x # xs) ! i = (x # xs) ! m ! n
[PROOF STEP]
proof (cases m)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. m = 0 \<Longrightarrow> concat (x # xs) ! i = (x # xs) ! m ! n
 2. \<And>nat. m = Suc nat \<Longrightarrow> concat (x # xs) ! i = (x # xs) ! m ! n
[PROOF STEP]
case 0
[PROOF STATE]
proof (state)
this:
m = 0

goal (2 subgoals):
 1. m = 0 \<Longrightarrow> concat (x # xs) ! i = (x # xs) ! m ! n
 2. \<And>nat. m = Suc nat \<Longrightarrow> concat (x # xs) ! i = (x # xs) ! m ! n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m = 0
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
m = 0

goal (1 subgoal):
 1. concat (x # xs) ! i = (x # xs) ! m ! n
[PROOF STEP]
using Cons
[PROOF STATE]
proof (prove)
using this:
m = 0
\<lbrakk>?m < length xs; ?n < length (xs ! ?m); ?i = sum_list (map length (take ?m xs)) + ?n\<rbrakk> \<Longrightarrow> concat xs ! ?i = xs ! ?m ! ?n
m < length (x # xs)
n < length ((x # xs) ! m)
i = sum_list (map length (take m (x # xs))) + n

goal (1 subgoal):
 1. concat (x # xs) ! i = (x # xs) ! m ! n
[PROOF STEP]
by (simp add: nth_append)
[PROOF STATE]
proof (state)
this:
concat (x # xs) ! i = (x # xs) ! m ! n

goal (1 subgoal):
 1. \<And>nat. m = Suc nat \<Longrightarrow> concat (x # xs) ! i = (x # xs) ! m ! n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>nat. m = Suc nat \<Longrightarrow> concat (x # xs) ! i = (x # xs) ! m ! n
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
m = Suc k

goal (1 subgoal):
 1. \<And>nat. m = Suc nat \<Longrightarrow> concat (x # xs) ! i = (x # xs) ! m ! n
[PROOF STEP]
with Cons(1) [of k n "i - length x"] and Cons(2-)
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>k < length xs; n < length (xs ! k); i - length x = sum_list (map length (take k xs)) + n\<rbrakk> \<Longrightarrow> concat xs ! (i - length x) = xs ! k ! n
m < length (x # xs)
n < length ((x # xs) ! m)
i = sum_list (map length (take m (x # xs))) + n
m = Suc k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>k < length xs; n < length (xs ! k); i - length x = sum_list (map length (take k xs)) + n\<rbrakk> \<Longrightarrow> concat xs ! (i - length x) = xs ! k ! n
m < length (x # xs)
n < length ((x # xs) ! m)
i = sum_list (map length (take m (x # xs))) + n
m = Suc k

goal (1 subgoal):
 1. concat (x # xs) ! i = (x # xs) ! m ! n
[PROOF STEP]
by (simp_all add: nth_append)
[PROOF STATE]
proof (state)
this:
concat (x # xs) ! i = (x # xs) ! m ! n

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
concat (x # xs) ! i = (x # xs) ! m ! n

goal (1 subgoal):
 1. \<And>m n i. \<lbrakk>m < length []; n < length ([] ! m); i = sum_list (map length (take m [])) + n\<rbrakk> \<Longrightarrow> concat [] ! i = [] ! m ! n
[PROOF STEP]
qed simp


[STATEMENT]
lemma sum_list_take_eq:
  fixes xs :: "nat list"
  shows "k < i \<Longrightarrow> i < length xs \<Longrightarrow> sum_list (take i xs) =
    sum_list (take k xs) + xs ! k + sum_list (take (i - Suc k) (drop (Suc k) xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>k < i; i < length xs\<rbrakk> \<Longrightarrow> sum_list (take i xs) = sum_list (take k xs) + xs ! k + sum_list (take (i - Suc k) (drop (Suc k) xs))
[PROOF STEP]
by (subst id_take_nth_drop [of k]) (auto simp: min_def drop_take)


[STATEMENT]
lemma partition_by_map0_append [simp]:
  "partition_by xs (map (\<lambda>x. 0) ys @ zs) = replicate (length ys) [] @ partition_by xs zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_by xs (map (\<lambda>x. 0) ys @ zs) = replicate (length ys) [] @ partition_by xs zs
[PROOF STEP]
by (induct ys) simp_all


[STATEMENT]
lemma concat_partition_by [simp]:
  "sum_list ys = length xs \<Longrightarrow> concat (partition_by xs ys) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list ys = length xs \<Longrightarrow> concat (partition_by xs ys) = xs
[PROOF STEP]
by (induct ys arbitrary: xs) simp_all


[STATEMENT]
lemma partition_by_nth_nth_old:
  assumes "i < length (partition_by xs ys)"
    and "j < length (partition_by xs ys ! i)"
    and "sum_list ys = length xs"
  shows "partition_by xs ys ! i ! j = xs ! (sum_list (map length (take i (partition_by xs ys))) + j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_by xs ys ! i ! j = xs ! (sum_list (map length (take i (partition_by xs ys))) + j)
[PROOF STEP]
using concat_nth [OF assms(1, 2) refl]
[PROOF STATE]
proof (prove)
using this:
concat (partition_by xs ys) ! (sum_list (map length (take i (partition_by xs ys))) + j) = partition_by xs ys ! i ! j

goal (1 subgoal):
 1. partition_by xs ys ! i ! j = xs ! (sum_list (map length (take i (partition_by xs ys))) + j)
[PROOF STEP]
unfolding concat_partition_by [OF assms(3)]
[PROOF STATE]
proof (prove)
using this:
xs ! (sum_list (map length (take i (partition_by xs ys))) + j) = partition_by xs ys ! i ! j

goal (1 subgoal):
 1. partition_by xs ys ! i ! j = xs ! (sum_list (map length (take i (partition_by xs ys))) + j)
[PROOF STEP]
by simp


[STATEMENT]
lemma map_map_partition_by:
  "map (map f) (partition_by xs ys) = partition_by (map f xs) ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (map f) (partition_by xs ys) = partition_by (map f xs) ys
[PROOF STEP]
by (induct ys arbitrary: xs) (auto simp: take_map drop_map)


[STATEMENT]
lemma length_partition_by [simp]:
  "length (partition_by xs ys) = length ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (partition_by xs ys) = length ys
[PROOF STEP]
by (induct ys arbitrary: xs) simp_all


[STATEMENT]
lemma partition_by_Nil [simp]:
  "partition_by [] ys = replicate (length ys) []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_by [] ys = replicate (length ys) []
[PROOF STEP]
by (induct ys) simp_all


[STATEMENT]
lemma partition_by_concat_id [simp]:
  assumes "length xss = length ys"
    and "\<And>i. i < length ys \<Longrightarrow> length (xss ! i) = ys ! i"
  shows "partition_by (concat xss) ys = xss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_by (concat xss) ys = xss
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
length xss = length ys
?i < length ys \<Longrightarrow> length (xss ! ?i) = ys ! ?i

goal (1 subgoal):
 1. partition_by (concat xss) ys = xss
[PROOF STEP]
by (induct ys arbitrary: xss) (simp, case_tac xss, simp, fastforce)


[STATEMENT]
lemma partition_by_nth:
  "i < length ys \<Longrightarrow> partition_by xs ys ! i = take (ys ! i) (drop (sum_list (take i ys)) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length ys \<Longrightarrow> partition_by xs ys ! i = take (ys ! i) (drop (sum_list (take i ys)) xs)
[PROOF STEP]
by (induct ys arbitrary: xs i) (simp, case_tac i, simp_all add: ac_simps)


[STATEMENT]
lemma partition_by_nth_less:
  assumes "k < i" and "i < length zs"
    and "length xs = sum_list (take i zs) + j"
  shows "partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) xs)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) xs)
[PROOF STEP]
have "partition_by (xs @ y # ys) zs ! k =
    take (zs ! k) (drop (sum_list (take k zs)) (xs @ y # ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) (xs @ y # ys))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k < i
i < length zs
length xs = sum_list (take i zs) + j

goal (1 subgoal):
 1. partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) (xs @ y # ys))
[PROOF STEP]
by (auto simp: partition_by_nth)
[PROOF STATE]
proof (state)
this:
partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) (xs @ y # ys))

goal (1 subgoal):
 1. partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) xs)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) (xs @ y # ys))

goal (1 subgoal):
 1. partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) xs)
[PROOF STEP]
have "zs ! k + sum_list (take k zs) \<le> length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zs ! k + sum_list (take k zs) \<le> length xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
k < i
i < length zs
length xs = sum_list (take i zs) + j

goal (1 subgoal):
 1. zs ! k + sum_list (take k zs) \<le> length xs
[PROOF STEP]
by (simp add: sum_list_take_eq)
[PROOF STATE]
proof (state)
this:
zs ! k + sum_list (take k zs) \<le> length xs

goal (1 subgoal):
 1. partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) xs)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) (xs @ y # ys))
zs ! k + sum_list (take k zs) \<le> length xs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) (xs @ y # ys))
zs ! k + sum_list (take k zs) \<le> length xs

goal (1 subgoal):
 1. partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) xs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) xs)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partition_by_nth_greater:
  assumes "i < k" and "k < length zs" and "j < zs ! i"
    and "length xs = sum_list (take i zs) + j"
  shows "partition_by (xs @ y # ys) zs ! k =
    take (zs ! k) (drop (sum_list (take k zs) - 1) (xs @ ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs) - 1) (xs @ ys))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs) - 1) (xs @ ys))
[PROOF STEP]
have "partition_by (xs @ y # ys) zs ! k =
    take (zs ! k) (drop (sum_list (take k zs)) (xs @ y # ys))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) (xs @ y # ys))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < k
k < length zs
j < zs ! i
length xs = sum_list (take i zs) + j

goal (1 subgoal):
 1. partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) (xs @ y # ys))
[PROOF STEP]
by (auto simp: partition_by_nth)
[PROOF STATE]
proof (state)
this:
partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) (xs @ y # ys))

goal (1 subgoal):
 1. partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs) - 1) (xs @ ys))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) (xs @ y # ys))

goal (1 subgoal):
 1. partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs) - 1) (xs @ ys))
[PROOF STEP]
have "sum_list (take k zs) > length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs < sum_list (take k zs)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i < k
k < length zs
j < zs ! i
length xs = sum_list (take i zs) + j

goal (1 subgoal):
 1. length xs < sum_list (take k zs)
[PROOF STEP]
by (auto simp: sum_list_take_eq)
[PROOF STATE]
proof (state)
this:
length xs < sum_list (take k zs)

goal (1 subgoal):
 1. partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs) - 1) (xs @ ys))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) (xs @ y # ys))
length xs < sum_list (take k zs)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs)) (xs @ y # ys))
length xs < sum_list (take k zs)

goal (1 subgoal):
 1. partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs) - 1) (xs @ ys))
[PROOF STEP]
by (auto) (metis Suc_diff_Suc drop_Suc_Cons)
[PROOF STATE]
proof (state)
this:
partition_by (xs @ y # ys) zs ! k = take (zs ! k) (drop (sum_list (take k zs) - 1) (xs @ ys))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma length_partition_by_nth:
  "sum_list ys = length xs \<Longrightarrow> i < length ys \<Longrightarrow> length (partition_by xs ys ! i) = ys ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sum_list ys = length xs; i < length ys\<rbrakk> \<Longrightarrow> length (partition_by xs ys ! i) = ys ! i
[PROOF STEP]
by (induct ys arbitrary: xs i; case_tac i) auto


[STATEMENT]
lemma partition_by_nth_nth_elem:
  assumes "sum_list ys = length xs" "i < length ys" "j < ys ! i"
  shows "partition_by xs ys ! i ! j \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_by xs ys ! i ! j \<in> set xs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. partition_by xs ys ! i ! j \<in> set xs
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
sum_list ys = length xs
i < length ys
j < ys ! i
[PROOF STEP]
have "j < length (partition_by xs ys ! i)"
[PROOF STATE]
proof (prove)
using this:
sum_list ys = length xs
i < length ys
j < ys ! i

goal (1 subgoal):
 1. j < length (partition_by xs ys ! i)
[PROOF STEP]
by (simp only: length_partition_by_nth)
[PROOF STATE]
proof (state)
this:
j < length (partition_by xs ys ! i)

goal (1 subgoal):
 1. partition_by xs ys ! i ! j \<in> set xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
j < length (partition_by xs ys ! i)
[PROOF STEP]
have "partition_by xs ys ! i ! j \<in> set (partition_by xs ys ! i)"
[PROOF STATE]
proof (prove)
using this:
j < length (partition_by xs ys ! i)

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

goal (1 subgoal):
 1. partition_by xs ys ! i ! j \<in> set xs
[PROOF STEP]
with assms(2)
[PROOF STATE]
proof (chain)
picking this:
i < length ys
partition_by xs ys ! i ! j \<in> set (partition_by xs ys ! i)
[PROOF STEP]
have "partition_by xs ys ! i ! j \<in> set (concat (partition_by xs ys))"
[PROOF STATE]
proof (prove)
using this:
i < length ys
partition_by xs ys ! i ! j \<in> set (partition_by xs ys ! i)

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

goal (1 subgoal):
 1. partition_by xs ys ! i ! j \<in> set xs
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
partition_by xs ys ! i ! j \<in> set (concat (partition_by xs ys))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
partition_by xs ys ! i ! j \<in> set (concat (partition_by xs ys))

goal (1 subgoal):
 1. partition_by xs ys ! i ! j \<in> set xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
partition_by xs ys ! i ! j \<in> set (concat (partition_by xs ys))
sum_list ys = length xs
i < length ys
j < ys ! i

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partition_by_nth_nth:
  assumes "sum_list ys = length xs" "i < length ys" "j < ys ! i"
  shows "partition_by xs ys ! i ! j = xs ! partition_by_idx (length xs) ys i j"
        "partition_by_idx (length xs) ys i j < length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_by xs ys ! i ! j = xs ! partition_by_idx (length xs) ys i j &&& partition_by_idx (length xs) ys i j < length xs
[PROOF STEP]
unfolding partition_by_idx_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_by xs ys ! i ! j = xs ! (partition_by [0..<length xs] ys ! i ! j) &&& partition_by [0..<length xs] ys ! i ! j < length xs
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. partition_by xs ys ! i ! j = xs ! (partition_by [0..<length xs] ys ! i ! j)
 2. partition_by [0..<length xs] ys ! i ! j < length xs
[PROOF STEP]
let ?n = "partition_by [0..<length xs] ys ! i ! j"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. partition_by xs ys ! i ! j = xs ! (partition_by [0..<length xs] ys ! i ! j)
 2. partition_by [0..<length xs] ys ! i ! j < length xs
[PROOF STEP]
show "?n < length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_by [0..<length xs] ys ! i ! j < length xs
[PROOF STEP]
using partition_by_nth_nth_elem[OF _ assms(2,3), of "[0..<length xs]"] assms(1)
[PROOF STATE]
proof (prove)
using this:
sum_list ys = length [0..<length xs] \<Longrightarrow> partition_by [0..<length xs] ys ! i ! j \<in> set [0..<length xs]
sum_list ys = length xs

goal (1 subgoal):
 1. partition_by [0..<length xs] ys ! i ! j < length xs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
partition_by [0..<length xs] ys ! i ! j < length xs

goal (1 subgoal):
 1. partition_by xs ys ! i ! j = xs ! (partition_by [0..<length xs] ys ! i ! j)
[PROOF STEP]
have li: "i < length (partition_by [0..<length xs] ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length (partition_by [0..<length xs] ys)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
i < length ys

goal (1 subgoal):
 1. i < length (partition_by [0..<length xs] ys)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
i < length (partition_by [0..<length xs] ys)

goal (1 subgoal):
 1. partition_by xs ys ! i ! j = xs ! (partition_by [0..<length xs] ys ! i ! j)
[PROOF STEP]
have lj: "j < length (partition_by [0..<length xs] ys ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j < length (partition_by [0..<length xs] ys ! i)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
sum_list ys = length xs
i < length ys
j < ys ! i

goal (1 subgoal):
 1. j < length (partition_by [0..<length xs] ys ! i)
[PROOF STEP]
by (simp add: length_partition_by_nth)
[PROOF STATE]
proof (state)
this:
j < length (partition_by [0..<length xs] ys ! i)

goal (1 subgoal):
 1. partition_by xs ys ! i ! j = xs ! (partition_by [0..<length xs] ys ! i ! j)
[PROOF STEP]
have "partition_by (map ((!) xs) [0..<length xs]) ys ! i ! j = xs ! ?n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_by (map ((!) xs) [0..<length xs]) ys ! i ! j = xs ! (partition_by [0..<length xs] ys ! i ! j)
[PROOF STEP]
by (simp only: map_map_partition_by[symmetric] nth_map[OF li] nth_map[OF lj])
[PROOF STATE]
proof (state)
this:
partition_by (map ((!) xs) [0..<length xs]) ys ! i ! j = xs ! (partition_by [0..<length xs] ys ! i ! j)

goal (1 subgoal):
 1. partition_by xs ys ! i ! j = xs ! (partition_by [0..<length xs] ys ! i ! j)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
partition_by (map ((!) xs) [0..<length xs]) ys ! i ! j = xs ! (partition_by [0..<length xs] ys ! i ! j)
[PROOF STEP]
show "partition_by xs ys ! i ! j = xs ! ?n"
[PROOF STATE]
proof (prove)
using this:
partition_by (map ((!) xs) [0..<length xs]) ys ! i ! j = xs ! (partition_by [0..<length xs] ys ! i ! j)

goal (1 subgoal):
 1. partition_by xs ys ! i ! j = xs ! (partition_by [0..<length xs] ys ! i ! j)
[PROOF STEP]
by (simp add: map_nth)
[PROOF STATE]
proof (state)
this:
partition_by xs ys ! i ! j = xs ! (partition_by [0..<length xs] ys ! i ! j)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_length_partition_by [simp]:
  "sum_list ys = length xs \<Longrightarrow> map length (partition_by xs ys) = ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list ys = length xs \<Longrightarrow> map length (partition_by xs ys) = ys
[PROOF STEP]
by (intro nth_equalityI, auto simp: length_partition_by_nth)


[STATEMENT]
lemma map_partition_by_nth [simp]:
  "i < length ys \<Longrightarrow> map f (partition_by xs ys ! i) = partition_by (map f xs) ys ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < length ys \<Longrightarrow> map f (partition_by xs ys ! i) = partition_by (map f xs) ys ! i
[PROOF STEP]
by (induct ys arbitrary: i xs) (simp, case_tac i, simp_all add: take_map drop_map)


[STATEMENT]
lemma sum_list_partition_by [simp]:
  "sum_list ys = length xs \<Longrightarrow>
    sum_list (map (\<lambda>x. sum_list (map f x)) (partition_by xs ys)) = sum_list (map f xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list ys = length xs \<Longrightarrow> (\<Sum>x\<leftarrow>partition_by xs ys. sum_list (map f x)) = sum_list (map f xs)
[PROOF STEP]
by (induct ys arbitrary: xs) (simp_all, metis append_take_drop_id sum_list_append map_append)


[STATEMENT]
lemma partition_by_map_conv:
  "partition_by xs ys = map (\<lambda>i. take (ys ! i) (drop (sum_list (take i ys)) xs)) [0 ..< length ys]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_by xs ys = map (\<lambda>i. take (ys ! i) (drop (sum_list (take i ys)) xs)) [0..<length ys]
[PROOF STEP]
by (rule nth_equalityI) (simp_all add: partition_by_nth)


[STATEMENT]
lemma UN_set_partition_by_map:
  "sum_list ys = length xs \<Longrightarrow> (\<Union>x\<in>set (partition_by (map f xs) ys). \<Union> (set x)) = \<Union>(set (map f xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list ys = length xs \<Longrightarrow> (\<Union>x\<in>set (partition_by (map f xs) ys). \<Union> (set x)) = \<Union> (set (map f xs))
[PROOF STEP]
by (induct ys arbitrary: xs)
     (simp_all add: drop_map take_map, metis UN_Un append_take_drop_id set_append)


[STATEMENT]
lemma UN_set_partition_by:
  "sum_list ys = length xs \<Longrightarrow> (\<Union>zs \<in> set (partition_by xs ys). \<Union>x \<in> set zs. f x) = (\<Union>x \<in> set xs. f x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list ys = length xs \<Longrightarrow> (\<Union>zs\<in>set (partition_by xs ys). \<Union> (f ` set zs)) = \<Union> (f ` set xs)
[PROOF STEP]
by (induct ys arbitrary: xs) (simp_all, metis UN_Un append_take_drop_id set_append)


[STATEMENT]
lemma Ball_atLeast0LessThan_partition_by_conv:
  "(\<forall>i\<in>{0..<length ys}. \<forall>x\<in>set (partition_by xs ys ! i). P x) =
    (\<forall>x \<in> \<Union>(set (map set (partition_by xs ys))). P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>i\<in>{0..<length ys}. \<forall>x\<in>set (partition_by xs ys ! i). P x) = (\<forall>x\<in>\<Union> (set (map set (partition_by xs ys))). P x)
[PROOF STEP]
by auto (metis atLeast0LessThan in_set_conv_nth length_partition_by lessThan_iff)


[STATEMENT]
lemma Ball_set_partition_by:
  "sum_list ys = length xs \<Longrightarrow>
  (\<forall>x \<in> set (partition_by xs ys). \<forall>y \<in> set x. P y) = (\<forall>x \<in> set xs. P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list ys = length xs \<Longrightarrow> (\<forall>x\<in>set (partition_by xs ys). \<forall>y\<in>set x. P y) = (\<forall>x\<in>set xs. P x)
[PROOF STEP]
proof (induct ys arbitrary: xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>xs. sum_list [] = length xs \<Longrightarrow> (\<forall>x\<in>set (partition_by xs []). Ball (set x) P) = Ball (set xs) P
 2. \<And>a ys xs. \<lbrakk>\<And>xs. sum_list ys = length xs \<Longrightarrow> (\<forall>x\<in>set (partition_by xs ys). Ball (set x) P) = Ball (set xs) P; sum_list (a # ys) = length xs\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (partition_by xs (a # ys)). Ball (set x) P) = Ball (set xs) P
[PROOF STEP]
case (Cons y ys)
[PROOF STATE]
proof (state)
this:
sum_list ys = length ?xs \<Longrightarrow> (\<forall>x\<in>set (partition_by ?xs ys). \<forall>a\<in>set x. P a) = (\<forall>a\<in>set ?xs. P a)
sum_list (y # ys) = length xs

goal (2 subgoals):
 1. \<And>xs. sum_list [] = length xs \<Longrightarrow> (\<forall>x\<in>set (partition_by xs []). Ball (set x) P) = Ball (set xs) P
 2. \<And>a ys xs. \<lbrakk>\<And>xs. sum_list ys = length xs \<Longrightarrow> (\<forall>x\<in>set (partition_by xs ys). Ball (set x) P) = Ball (set xs) P; sum_list (a # ys) = length xs\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (partition_by xs (a # ys)). Ball (set x) P) = Ball (set xs) P
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sum_list ys = length ?xs \<Longrightarrow> (\<forall>x\<in>set (partition_by ?xs ys). \<forall>a\<in>set x. P a) = (\<forall>a\<in>set ?xs. P a)
sum_list (y # ys) = length xs
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
sum_list ys = length ?xs \<Longrightarrow> (\<forall>x\<in>set (partition_by ?xs ys). \<forall>a\<in>set x. P a) = (\<forall>a\<in>set ?xs. P a)
sum_list (y # ys) = length xs

goal (1 subgoal):
 1. (\<forall>x\<in>set (partition_by xs (y # ys)). \<forall>a\<in>set x. P a) = (\<forall>a\<in>set xs. P a)
[PROOF STEP]
apply (subst (2) append_take_drop_id [of y xs, symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>xs. sum_list ys = length xs \<Longrightarrow> (\<forall>x\<in>set (partition_by xs ys). \<forall>a\<in>set x. P a) = (\<forall>a\<in>set xs. P a); sum_list (y # ys) = length xs\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (partition_by xs (y # ys)). Ball (set x) P) = Ball (set (take y xs @ drop y xs)) P
[PROOF STEP]
apply (simp only: set_append)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>xs. sum_list ys = length xs \<Longrightarrow> (\<forall>x\<in>set (partition_by xs ys). \<forall>a\<in>set x. P a) = (\<forall>a\<in>set xs. P a); sum_list (y # ys) = length xs\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set (partition_by xs (y # ys)). Ball (set x) P) = Ball (set (take y xs) \<union> set (drop y xs)) P
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(\<forall>x\<in>set (partition_by xs (y # ys)). \<forall>a\<in>set x. P a) = (\<forall>a\<in>set xs. P a)

goal (1 subgoal):
 1. \<And>xs. sum_list [] = length xs \<Longrightarrow> (\<forall>x\<in>set (partition_by xs []). Ball (set x) P) = Ball (set xs) P
[PROOF STEP]
qed simp


[STATEMENT]
lemma partition_by_append2:
  "partition_by xs (ys @ zs) = partition_by (take (sum_list ys) xs) ys @ partition_by (drop (sum_list ys) xs) zs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_by xs (ys @ zs) = partition_by (take (sum_list ys) xs) ys @ partition_by (drop (sum_list ys) xs) zs
[PROOF STEP]
by (induct ys arbitrary: xs) (auto simp: drop_take ac_simps split: split_min)


[STATEMENT]
lemma partition_by_concat2:
  "partition_by xs (concat ys) =
   concat (map (\<lambda>i . partition_by (partition_by xs (map sum_list ys) ! i) (ys ! i)) [0..<length ys])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_by xs (concat ys) = concat (map (\<lambda>i. partition_by (partition_by xs (map sum_list ys) ! i) (ys ! i)) [0..<length ys])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. partition_by xs (concat ys) = concat (map (\<lambda>i. partition_by (partition_by xs (map sum_list ys) ! i) (ys ! i)) [0..<length ys])
[PROOF STEP]
have *: "map (\<lambda>i . partition_by (partition_by xs (map sum_list ys) ! i) (ys ! i)) [0..<length ys] =
    map (\<lambda>(x,y). partition_by x y) (zip (partition_by xs (map sum_list ys)) ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map (\<lambda>i. partition_by (partition_by xs (map sum_list ys) ! i) (ys ! i)) [0..<length ys] = map2 partition_by (partition_by xs (map sum_list ys)) ys
[PROOF STEP]
using zip_nth_conv[of "partition_by xs (map sum_list ys)" ys]
[PROOF STATE]
proof (prove)
using this:
length (partition_by xs (map sum_list ys)) = length ys \<Longrightarrow> zip (partition_by xs (map sum_list ys)) ys = map (\<lambda>i. (partition_by xs (map sum_list ys) ! i, ys ! i)) [0..<length ys]

goal (1 subgoal):
 1. map (\<lambda>i. partition_by (partition_by xs (map sum_list ys) ! i) (ys ! i)) [0..<length ys] = map2 partition_by (partition_by xs (map sum_list ys)) ys
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
map (\<lambda>i. partition_by (partition_by xs (map sum_list ys) ! i) (ys ! i)) [0..<length ys] = map2 partition_by (partition_by xs (map sum_list ys)) ys

goal (1 subgoal):
 1. partition_by xs (concat ys) = concat (map (\<lambda>i. partition_by (partition_by xs (map sum_list ys) ! i) (ys ! i)) [0..<length ys])
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_by xs (concat ys) = concat (map (\<lambda>i. partition_by (partition_by xs (map sum_list ys) ! i) (ys ! i)) [0..<length ys])
[PROOF STEP]
unfolding *
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. partition_by xs (concat ys) = concat (map2 partition_by (partition_by xs (map sum_list ys)) ys)
[PROOF STEP]
by (induct ys arbitrary: xs) (auto simp: partition_by_append2)
[PROOF STATE]
proof (state)
this:
partition_by xs (concat ys) = concat (map (\<lambda>i. partition_by (partition_by xs (map sum_list ys) ! i) (ys ! i)) [0..<length ys])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma partition_by_partition_by:
  "length xs = sum_list (map sum_list ys) \<Longrightarrow>
   partition_by (partition_by xs (concat ys)) (map length ys) =
   map (\<lambda>i. partition_by (partition_by xs (map sum_list ys) ! i) (ys ! i)) [0..<length ys]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length xs = sum_list (map sum_list ys) \<Longrightarrow> partition_by (partition_by xs (concat ys)) (map length ys) = map (\<lambda>i. partition_by (partition_by xs (map sum_list ys) ! i) (ys ! i)) [0..<length ys]
[PROOF STEP]
by (auto simp: partition_by_concat2 intro: partition_by_concat_id)


[STATEMENT]
lemma inf_mctxt_idem [simp]:
  fixes C :: "('f, 'v) mctxt"
  shows "C \<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_mctxt_MHole2 [simp]:
  "C \<sqinter> MHole = MHole"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. C \<sqinter> MHole = MHole
[PROOF STEP]
by (induct C) simp_all


[STATEMENT]
lemma inf_mctxt_comm [ac_simps]:
  "(C :: ('f, 'v) mctxt) \<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_mctxt.induct) (fastforce simp: in_set_conv_nth intro!: nth_equalityI)+


[STATEMENT]
lemma inf_mctxt_assoc [ac_simps]:
  fixes C :: "('f, 'v) mctxt"
  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_mctxt.induct)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>D E. MHole \<sqinter> D \<sqinter> E = MHole \<sqinter> (D \<sqinter> E)
 2. \<And>v E. MVar v \<sqinter> MHole \<sqinter> E = MVar v \<sqinter> (MHole \<sqinter> E)
 3. \<And>v va E. MFun v va \<sqinter> MHole \<sqinter> E = MFun v va \<sqinter> (MHole \<sqinter> E)
 4. \<And>x y E. MVar x \<sqinter> MVar y \<sqinter> E = MVar x \<sqinter> (MVar y \<sqinter> E)
 5. \<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> MFun f Cs \<sqinter> MFun g Ds \<sqinter> E = MFun f Cs \<sqinter> (MFun g Ds \<sqinter> E)
 6. \<And>v va vb E. MVar v \<sqinter> MFun va vb \<sqinter> E = MVar v \<sqinter> (MFun va vb \<sqinter> E)
 7. \<And>v va vb E. MFun v va \<sqinter> MVar vb \<sqinter> E = MFun v va \<sqinter> (MVar vb \<sqinter> E)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>y E. MVar y \<sqinter> E = MVar y \<sqinter> (MVar y \<sqinter> E)
 2. \<And>x y E. x \<noteq> y \<Longrightarrow> MHole = MVar x \<sqinter> (MVar y \<sqinter> E)
 3. \<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> MFun g (map2 (\<sqinter>) Cs Ds) \<sqinter> E = MFun g Cs \<sqinter> (MFun g Ds \<sqinter> E)
 4. \<And>f Cs g Ds E. f \<noteq> g \<Longrightarrow> MHole = MFun f Cs \<sqinter> (MFun g Ds \<sqinter> E)
 5. \<And>f Cs g Ds E. length Cs \<noteq> length Ds \<Longrightarrow> MHole = MFun f Cs \<sqinter> (MFun g Ds \<sqinter> E)
 6. \<And>v va vb E. MHole = MVar v \<sqinter> (MFun va vb \<sqinter> E)
 7. \<And>v va vb E. MHole = MFun v va \<sqinter> (MVar vb \<sqinter> E)
[PROOF STEP]
apply (case_tac E, auto)+
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>Cs Ds x32. \<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 x32; length Ds = length x32\<rbrakk> \<Longrightarrow> map2 (\<sqinter>) (map2 (\<sqinter>) Cs Ds) x32 = map2 (\<sqinter>) Cs (map2 (\<sqinter>) Ds x32)
 2. \<And>f Cs g Ds E. f \<noteq> g \<Longrightarrow> MHole = MFun f Cs \<sqinter> (MFun g Ds \<sqinter> E)
 3. \<And>f Cs g Ds E. length Cs \<noteq> length Ds \<Longrightarrow> MHole = MFun f Cs \<sqinter> (MFun g Ds \<sqinter> E)
 4. \<And>v va vb E. MHole = MVar v \<sqinter> (MFun va vb \<sqinter> E)
 5. \<And>v va vb E. MHole = MFun v va \<sqinter> (MVar vb \<sqinter> E)
[PROOF STEP]
apply (fastforce simp: in_set_conv_nth intro!: nth_equalityI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>f Cs g Ds E. f \<noteq> g \<Longrightarrow> MHole = MFun f Cs \<sqinter> (MFun g Ds \<sqinter> E)
 2. \<And>f Cs g Ds E. length Cs \<noteq> length Ds \<Longrightarrow> MHole = MFun f Cs \<sqinter> (MFun g Ds \<sqinter> E)
 3. \<And>v va vb E. MHole = MVar v \<sqinter> (MFun va vb \<sqinter> E)
 4. \<And>v va vb E. MHole = MFun v va \<sqinter> (MVar vb \<sqinter> E)
[PROOF STEP]
apply (case_tac E, auto)+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma partition_holes_fill_holes_conv:
  "fill_holes (MFun f cs) ts =
    Fun f [fill_holes (cs ! i) (partition_holes ts cs ! i). i \<leftarrow> [0 ..< length cs]]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_holes (MFun f cs) ts = Fun f (map (\<lambda>i. fill_holes (cs ! i) (partition_holes ts cs ! i)) [0..<length cs])
[PROOF STEP]
by (simp add: partition_by_nth take_map)


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


[STATEMENT]
lemma fill_holes_induct2[consumes 2, case_names MHole MVar MFun]:
  fixes P :: "('f,'v) mctxt \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> bool"
  assumes len1: "num_holes C = length xs" and len2: "num_holes C = length ys"
  and Hole: "\<And>x y. P MHole [x] [y]"
  and Var: "\<And>v. P (MVar v) [] []"
  and Fun: "\<And>f Cs xs ys.  sum_list (map num_holes Cs) = length xs \<Longrightarrow>
    sum_list (map num_holes Cs) = length ys \<Longrightarrow>
    (\<And>i. i < length Cs \<Longrightarrow> P (Cs ! i) (partition_holes xs Cs ! i) (partition_holes ys Cs ! i)) \<Longrightarrow>
    P (MFun f Cs) (concat (partition_holes xs Cs)) (concat (partition_holes ys Cs))"
  shows "P C xs ys"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P C xs ys
[PROOF STEP]
proof (insert len1 len2, induct C arbitrary: xs ys)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xs ys. \<lbrakk>num_holes (MVar x) = length xs; num_holes (MVar x) = length ys\<rbrakk> \<Longrightarrow> P (MVar x) xs ys
 2. \<And>xs ys. \<lbrakk>num_holes MHole = length xs; num_holes MHole = length ys\<rbrakk> \<Longrightarrow> P MHole xs ys
 3. \<And>x1a x2 xs ys. \<lbrakk>\<And>x2a xs ys. \<lbrakk>x2a \<in> set x2; num_holes x2a = length xs; num_holes x2a = length ys\<rbrakk> \<Longrightarrow> P x2a xs ys; num_holes (MFun x1a x2) = length xs; num_holes (MFun x1a x2) = length ys\<rbrakk> \<Longrightarrow> P (MFun x1a x2) xs ys
[PROOF STEP]
case MHole
[PROOF STATE]
proof (state)
this:
num_holes MHole = length xs
num_holes MHole = length ys

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

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

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

goal (2 subgoals):
 1. \<And>x xs ys. \<lbrakk>num_holes (MVar x) = length xs; num_holes (MVar x) = length ys\<rbrakk> \<Longrightarrow> P (MVar x) xs ys
 2. \<And>x1a x2 xs ys. \<lbrakk>\<And>x2a xs ys. \<lbrakk>x2a \<in> set x2; num_holes x2a = length xs; num_holes x2a = length ys\<rbrakk> \<Longrightarrow> P x2a xs ys; num_holes (MFun x1a x2) = length xs; num_holes (MFun x1a x2) = length ys\<rbrakk> \<Longrightarrow> P (MFun x1a x2) xs ys
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x xs ys. \<lbrakk>num_holes (MVar x) = length xs; num_holes (MVar x) = length ys\<rbrakk> \<Longrightarrow> P (MVar x) xs ys
 2. \<And>x1a x2 xs ys. \<lbrakk>\<And>x2a xs ys. \<lbrakk>x2a \<in> set x2; num_holes x2a = length xs; num_holes x2a = length ys\<rbrakk> \<Longrightarrow> P x2a xs ys; num_holes (MFun x1a x2) = length xs; num_holes (MFun x1a x2) = length ys\<rbrakk> \<Longrightarrow> P (MFun x1a x2) xs ys
[PROOF STEP]
case (MVar v)
[PROOF STATE]
proof (state)
this:
num_holes (MVar v) = length xs
num_holes (MVar v) = length ys

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

goal (1 subgoal):
 1. P (MVar v) xs ys
[PROOF STEP]
using Var
[PROOF STATE]
proof (prove)
using this:
num_holes (MVar v) = length xs
num_holes (MVar v) = length ys
P (MVar ?v) [] []

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fill_holes_induct[consumes 1, case_names MHole MVar MFun]:
  fixes P :: "('f,'v) mctxt \<Rightarrow> 'a list \<Rightarrow> bool"
  assumes len: "num_holes C = length xs"
  and Hole: "\<And>x. P MHole [x]"
  and Var: "\<And>v. P (MVar v) []"
  and Fun: "\<And>f Cs xs. sum_list (map num_holes Cs) = length xs \<Longrightarrow>
    (\<And>i. i < length Cs \<Longrightarrow> P (Cs ! i) (partition_holes xs Cs ! i)) \<Longrightarrow>
    P (MFun f Cs) (concat (partition_holes xs Cs))"
  shows "P C xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P C xs
[PROOF STEP]
using fill_holes_induct2[of C xs xs "\<lambda> C xs _. P C xs"] assms
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>num_holes C = length xs; num_holes C = length xs; \<And>x y. P MHole [x]; \<And>v. P (MVar v) []; \<And>f Cs xs ys. \<lbrakk>sum_list (map num_holes Cs) = length xs; sum_list (map num_holes Cs) = length ys; \<And>i. i < length Cs \<Longrightarrow> P (Cs ! i) (partition_holes xs Cs ! i)\<rbrakk> \<Longrightarrow> P (MFun f Cs) (concat (partition_holes xs Cs))\<rbrakk> \<Longrightarrow> P C xs
num_holes C = length xs
P MHole [?x]
P (MVar ?v) []
\<lbrakk>sum_list (map num_holes ?Cs) = length ?xs; \<And>i. i < length ?Cs \<Longrightarrow> P (?Cs ! i) (partition_holes ?xs ?Cs ! i)\<rbrakk> \<Longrightarrow> P (MFun ?f ?Cs) (concat (partition_holes ?xs ?Cs))

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


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

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


[STATEMENT]
lemma fill_holes_term_of_mctxt:
  "num_holes C = 0 \<Longrightarrow> fill_holes C [] = term_of_mctxt C"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_holes C = 0 \<Longrightarrow> fill_holes C [] = term_of_mctxt C
[PROOF STEP]
by (induct C) (auto simp add: map_eq_nth_conv)


[STATEMENT]
lemma fill_holes_MHole:
  "length ts = Suc 0 \<Longrightarrow> ts ! 0 = u \<Longrightarrow> fill_holes MHole ts = u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length ts = Suc 0; ts ! 0 = u\<rbrakk> \<Longrightarrow> fill_holes MHole ts = u
[PROOF STEP]
by (cases ts) simp_all


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

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

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fill_holes_MFun:
  assumes lCs: "length Cs = length ts"
    and lss: "length ss = length ts"
    and rec: "\<And> i. i < length ts \<Longrightarrow> num_holes (Cs ! i) = length (ss ! i) \<and> fill_holes (Cs ! i) (ss ! i) = ts ! i"
  shows "fill_holes (MFun f Cs) (concat ss) = Fun f ts"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fill_holes (MFun f Cs) (concat ss) = Fun f ts
[PROOF STEP]
unfolding fill_holes.simps term.simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f = f \<and> map (\<lambda>i. fill_holes (Cs ! i) (partition_holes (concat ss) Cs ! i)) [0..<length Cs] = ts
[PROOF STEP]
by (rule conjI[OF refl], rule fill_holes_arbitrary[OF lCs lss rec])


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

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


[STATEMENT]
lemma eqf_MFunE:
  assumes "s =\<^sub>f (MFun f Cs,ss)"
  obtains ts sss where "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"
[PROOF STATE]
proof (prove)
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]
proof -
[PROOF STATE]
proof (state)
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]
from eqfE[OF assms]
[PROOF STATE]
proof (chain)
picking this:
s = fill_holes (MFun f Cs) ss
num_holes (MFun f Cs) = length ss
[PROOF STEP]
have fh: "s = fill_holes (MFun f Cs) ss"
    and nh: "sum_list (map num_holes Cs) = length ss"
[PROOF STATE]
proof (prove)
using this:
s = fill_holes (MFun f Cs) ss
num_holes (MFun f Cs) = length ss

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

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]
from fh
[PROOF STATE]
proof (chain)
picking this:
s = fill_holes (MFun f Cs) ss
[PROOF STEP]
obtain ts where s: "s = Fun f ts"
[PROOF STATE]
proof (prove)
using this:
s = fill_holes (MFun f Cs) ss

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

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]
from fh[unfolded s]
[PROOF STATE]
proof (chain)
picking this:
Fun f ts = fill_holes (MFun f Cs) ss
[PROOF STEP]
have ts: "ts = map (\<lambda>i. fill_holes (Cs ! i) (partition_holes ss Cs ! i)) [0..<length Cs]"
    (is "_ = map (?f Cs ss) _")
[PROOF STATE]
proof (prove)
using this:
Fun f ts = fill_holes (MFun f Cs) ss

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

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]
let ?sss = "partition_holes ss Cs"
[PROOF STATE]
proof (state)
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]
from nh
[PROOF STATE]
proof (chain)
picking this:
sum_list (map num_holes Cs) = length ss
[PROOF STEP]
have *: "length ?sss = length Cs" "\<And>i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>f (Cs ! i, ?sss ! i)" "ss = concat ?sss"
[PROOF STATE]
proof (prove)
using this:
sum_list (map num_holes Cs) = length ss

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

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]
have len: "length ts = length Cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length ts = length Cs
[PROOF STEP]
unfolding ts
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (map (\<lambda>i. fill_holes (Cs ! i) (partition_holes ss Cs ! i)) [0..<length Cs]) = length Cs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
length ts = length Cs

goal (1 subgoal):
 1. (\<And>ts sss. \<lbrakk>s = 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]
assume ass: "\<And>ts sss. s = Fun f ts \<Longrightarrow>
              length ts = length Cs \<Longrightarrow>
              length sss = length Cs \<Longrightarrow> (\<And>i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>f (Cs ! i, sss ! i)) \<Longrightarrow> ss = concat sss \<Longrightarrow> thesis"
[PROOF STATE]
proof (state)
this:
\<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

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]
show thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. thesis
[PROOF STEP]
by (rule ass[OF s len *])
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eqf_MFunI:
  assumes "length sss = length Cs"
    and "length ts = length Cs"
    and"\<And> i. i < length Cs \<Longrightarrow> ts ! i =\<^sub>f (Cs ! i, sss ! i)"
  shows "Fun f ts =\<^sub>f (MFun f Cs, concat sss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fun f ts =\<^sub>f (MFun f Cs, concat sss)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Fun f ts = fill_holes (MFun f Cs) (concat sss)
 2. num_holes (MFun f Cs) = length (concat sss)
[PROOF STEP]
have "num_holes (MFun f Cs) = sum_list (map num_holes Cs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_holes (MFun f Cs) = sum_list (map num_holes Cs)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
num_holes (MFun f Cs) = sum_list (map num_holes Cs)

goal (2 subgoals):
 1. Fun f ts = fill_holes (MFun f Cs) (concat sss)
 2. num_holes (MFun f Cs) = length (concat sss)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
num_holes (MFun f Cs) = sum_list (map num_holes Cs)

goal (2 subgoals):
 1. Fun f ts = fill_holes (MFun f Cs) (concat sss)
 2. num_holes (MFun f Cs) = length (concat sss)
[PROOF STEP]
have "map num_holes Cs = map length sss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map num_holes Cs = map length sss
[PROOF STEP]
by (rule nth_equalityI, insert assms eqfE[OF assms(3)], auto)
[PROOF STATE]
proof (state)
this:
map num_holes Cs = map length sss

goal (2 subgoals):
 1. Fun f ts = fill_holes (MFun f Cs) (concat sss)
 2. num_holes (MFun f Cs) = length (concat sss)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
map num_holes Cs = map length sss

goal (2 subgoals):
 1. Fun f ts = fill_holes (MFun f Cs) (concat sss)
 2. num_holes (MFun f Cs) = length (concat sss)
[PROOF STEP]
have "sum_list (\<dots>) = length (concat sss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map length sss) = length (concat sss)
[PROOF STEP]
unfolding length_concat
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map length sss) = sum_list (map length sss)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
sum_list (map length sss) = length (concat sss)

goal (2 subgoals):
 1. Fun f ts = fill_holes (MFun f Cs) (concat sss)
 2. num_holes (MFun f Cs) = length (concat sss)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
num_holes (MFun f Cs) = length (concat sss)
[PROOF STEP]
show "num_holes (MFun f Cs) = length (concat sss)"
[PROOF STATE]
proof (prove)
using this:
num_holes (MFun f Cs) = length (concat sss)

goal (1 subgoal):
 1. num_holes (MFun f Cs) = length (concat sss)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
num_holes (MFun f Cs) = length (concat sss)

goal (1 subgoal):
 1. Fun f ts = fill_holes (MFun f Cs) (concat sss)
[PROOF STEP]
show "Fun f ts = fill_holes (MFun f Cs) (concat sss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Fun f ts = fill_holes (MFun f Cs) (concat sss)
[PROOF STEP]
by (rule fill_holes_MFun[symmetric], insert assms(1,2) eqfE[OF assms(3)], auto)
[PROOF STATE]
proof (state)
this:
Fun f ts = fill_holes (MFun f Cs) (concat sss)

goal:
No subgoals!
[PROOF STEP]
qed