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

goal (1 subgoal):
 1. unfill_holes C t = map ((|_) t) (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> unfill_holes (MVar x) t = map ((|_) t) (hole_poss_list (MVar x))
 2. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> unfill_holes MHole t = map ((|_) t) (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> unfill_holes x2a t = map ((|_) t) (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> unfill_holes (MFun x1a x2) t = map ((|_) t) (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> unfill_holes (MVar x) t = map ((|_) t) (hole_poss_list (MVar x))
 2. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> unfill_holes MHole t = map ((|_) t) (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> unfill_holes x2a t = map ((|_) t) (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> unfill_holes (MFun x1a x2) t = map ((|_) t) (hole_poss_list (MFun x1a x2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
MVar x \<le> mctxt_of_term t
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
MVar x \<le> mctxt_of_term t

goal (1 subgoal):
 1. unfill_holes (MVar x) t = map ((|_) t) (hole_poss_list (MVar x))
[PROOF STEP]
by (cases t) (auto elim: less_eq_mctxt_MVarE1)
[PROOF STATE]
proof (state)
this:
unfill_holes (MVar x) t = map ((|_) t) (hole_poss_list (MVar x))

goal (2 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> unfill_holes MHole t = map ((|_) t) (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> unfill_holes x2a t = map ((|_) t) (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> unfill_holes (MFun x1a x2) t = map ((|_) t) (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> unfill_holes MHole t = map ((|_) t) (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> unfill_holes x2a t = map ((|_) t) (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> unfill_holes (MFun x1a x2) t = map ((|_) t) (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> unfill_holes ?x2a ?t = map ((|_) ?t) (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> unfill_holes MHole t = map ((|_) t) (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> unfill_holes x2a t = map ((|_) t) (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> unfill_holes (MFun x1a x2) t = map ((|_) t) (hole_poss_list (MFun x1a x2))
[PROOF STEP]
from MFun(2)
[PROOF STATE]
proof (chain)
picking this:
MFun f ts \<le> mctxt_of_term t
[PROOF STEP]
obtain ss where [simp]: "t = Fun f ss" and l: "length ts = length ss"
[PROOF STATE]
proof (prove)
using this:
MFun f ts \<le> mctxt_of_term t

goal (1 subgoal):
 1. (\<And>ss. \<lbrakk>t = Fun f ss; length ts = length ss\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases t) (auto elim: less_eq_mctxt_MFunE1)
[PROOF STATE]
proof (state)
this:
t = Fun f ss
length ts = length ss

goal (2 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> unfill_holes MHole t = map ((|_) t) (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> unfill_holes x2a t = map ((|_) t) (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> unfill_holes (MFun x1a x2) t = map ((|_) t) (hole_poss_list (MFun x1a x2))
[PROOF STEP]
let ?ts = "map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> unfill_holes MHole t = map ((|_) t) (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> unfill_holes x2a t = map ((|_) t) (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> unfill_holes (MFun x1a x2) t = map ((|_) t) (hole_poss_list (MFun x1a x2))
[PROOF STEP]
let ?ss = "map (\<lambda> x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> unfill_holes MHole t = map ((|_) t) (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> unfill_holes x2a t = map ((|_) t) (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> unfill_holes (MFun x1a x2) t = map ((|_) t) (hole_poss_list (MFun x1a x2))
[PROOF STEP]
have eq_l [simp]: "length (concat ?ts) = length (concat ?ss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (concat (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts])) = length (concat (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)))
[PROOF STEP]
using MFun
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set ts; ?x2a \<le> mctxt_of_term ?t\<rbrakk> \<Longrightarrow> unfill_holes ?x2a ?t = map ((|_) ?t) (hole_poss_list ?x2a)
MFun f ts \<le> mctxt_of_term t

goal (1 subgoal):
 1. length (concat (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts])) = length (concat (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)))
[PROOF STEP]
by (auto simp: length_concat comp_def elim!: less_eq_mctxt_MFunE1 split!: prod.splits intro!: nth_sum_listI)
[PROOF STATE]
proof (state)
this:
length (concat (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts])) = length (concat (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)))

goal (2 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> unfill_holes MHole t = map ((|_) t) (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> unfill_holes x2a t = map ((|_) t) (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> unfill_holes (MFun x1a x2) t = map ((|_) t) (hole_poss_list (MFun x1a x2))
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
length (concat (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts])) = length (concat (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)))

goal (2 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> unfill_holes MHole t = map ((|_) t) (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> unfill_holes x2a t = map ((|_) t) (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> unfill_holes (MFun x1a x2) t = map ((|_) t) (hole_poss_list (MFun x1a x2))
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> unfill_holes MHole t = map ((|_) t) (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> unfill_holes x2a t = map ((|_) t) (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> unfill_holes (MFun x1a x2) t = map ((|_) t) (hole_poss_list (MFun x1a x2))
[PROOF STEP]
assume ass: "i < length (concat ?ts)"
[PROOF STATE]
proof (state)
this:
i < length (concat (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]))

goal (2 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> unfill_holes MHole t = map ((|_) t) (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> unfill_holes x2a t = map ((|_) t) (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> unfill_holes (MFun x1a x2) t = map ((|_) t) (hole_poss_list (MFun x1a x2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length (concat (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]))
[PROOF STEP]
have lss: "i < length (concat ?ss)"
[PROOF STATE]
proof (prove)
using this:
i < length (concat (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]))

goal (1 subgoal):
 1. i < length (concat (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
i < length (concat (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)))

goal (2 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> unfill_holes MHole t = map ((|_) t) (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> unfill_holes x2a t = map ((|_) t) (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> unfill_holes (MFun x1a x2) t = map ((|_) t) (hole_poss_list (MFun x1a x2))
[PROOF STEP]
obtain m n where [simp]: "concat_index_split (0, i) ?ts = (m, n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m n. concat_index_split (0, i) (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) = (m, n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
concat_index_split (0, i) (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) = (m, n)

goal (2 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> unfill_holes MHole t = map ((|_) t) (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> unfill_holes x2a t = map ((|_) t) (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> unfill_holes (MFun x1a x2) t = map ((|_) t) (hole_poss_list (MFun x1a x2))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
concat_index_split (0, i) (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) = (m, n)
[PROOF STEP]
have [simp]: "concat_index_split (0, i) ?ss = (m, n)"
[PROOF STATE]
proof (prove)
using this:
concat_index_split (0, i) (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) = (m, n)

goal (1 subgoal):
 1. concat_index_split (0, i) (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)) = (m, n)
[PROOF STEP]
using concat_index_split_unique[OF ass, of ?ss 0] MFun(2)
[PROOF STATE]
proof (prove)
using this:
concat_index_split (0, i) (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) = (m, n)
\<lbrakk>length (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) = length (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)); \<forall>i<length (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]). length (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts] ! i) = length (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts) ! i)\<rbrakk> \<Longrightarrow> concat_index_split (0, i) (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) = concat_index_split (0, i) (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts))
MFun f ts \<le> mctxt_of_term t

goal (1 subgoal):
 1. concat_index_split (0, i) (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)) = (m, n)
[PROOF STEP]
by (auto simp: unfill_holles_hole_poss_list_length[of "ts ! i" "ss ! i" for i]
       simp del: length_unfill_holes elim!: less_eq_mctxt_MFunE1)
[PROOF STATE]
proof (state)
this:
concat_index_split (0, i) (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)) = (m, n)

goal (2 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> unfill_holes MHole t = map ((|_) t) (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> unfill_holes x2a t = map ((|_) t) (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> unfill_holes (MFun x1a x2) t = map ((|_) t) (hole_poss_list (MFun x1a x2))
[PROOF STEP]
from concat_index_split_less_length_concat(2-)[OF ass ] concat_index_split_less_length_concat(2-)[OF lss]
[PROOF STATE]
proof (chain)
picking this:
concat_index_split (0, i) (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) = (?m, ?n) \<Longrightarrow> ?m < length (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts])
concat_index_split (0, i) (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) = (?m, ?n) \<Longrightarrow> ?n < length (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts] ! ?m)
concat_index_split (0, i) (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) = (?m, ?n) \<Longrightarrow> concat (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) ! i = map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts] ! ?m ! ?n
concat_index_split (0, i) (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)) = (?m, ?n) \<Longrightarrow> ?m < length (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts))
concat_index_split (0, i) (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)) = (?m, ?n) \<Longrightarrow> ?n < length (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts) ! ?m)
concat_index_split (0, i) (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)) = (?m, ?n) \<Longrightarrow> concat (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)) ! i = map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts) ! ?m ! ?n
[PROOF STEP]
have "concat ?ts ! i = concat ?ss! i"
[PROOF STATE]
proof (prove)
using this:
concat_index_split (0, i) (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) = (?m, ?n) \<Longrightarrow> ?m < length (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts])
concat_index_split (0, i) (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) = (?m, ?n) \<Longrightarrow> ?n < length (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts] ! ?m)
concat_index_split (0, i) (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) = (?m, ?n) \<Longrightarrow> concat (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) ! i = map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts] ! ?m ! ?n
concat_index_split (0, i) (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)) = (?m, ?n) \<Longrightarrow> ?m < length (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts))
concat_index_split (0, i) (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)) = (?m, ?n) \<Longrightarrow> ?n < length (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts) ! ?m)
concat_index_split (0, i) (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)) = (?m, ?n) \<Longrightarrow> concat (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)) ! i = map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts) ! ?m ! ?n

goal (1 subgoal):
 1. concat (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) ! i = concat (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)) ! i
[PROOF STEP]
using MFun(1)[OF nth_mem, of m "ss ! m"] MFun(2)
[PROOF STATE]
proof (prove)
using this:
concat_index_split (0, i) (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) = (?m, ?n) \<Longrightarrow> ?m < length (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts])
concat_index_split (0, i) (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) = (?m, ?n) \<Longrightarrow> ?n < length (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts] ! ?m)
concat_index_split (0, i) (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) = (?m, ?n) \<Longrightarrow> concat (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) ! i = map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts] ! ?m ! ?n
concat_index_split (0, i) (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)) = (?m, ?n) \<Longrightarrow> ?m < length (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts))
concat_index_split (0, i) (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)) = (?m, ?n) \<Longrightarrow> ?n < length (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts) ! ?m)
concat_index_split (0, i) (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)) = (?m, ?n) \<Longrightarrow> concat (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)) ! i = map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts) ! ?m ! ?n
\<lbrakk>m < length ts; ts ! m \<le> mctxt_of_term (ss ! m)\<rbrakk> \<Longrightarrow> unfill_holes (ts ! m) (ss ! m) = map ((|_) (ss ! m)) (hole_poss_list (ts ! m))
MFun f ts \<le> mctxt_of_term t

goal (1 subgoal):
 1. concat (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) ! i = concat (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)) ! i
[PROOF STEP]
by (auto elim!: less_eq_mctxt_MFunE1)
[PROOF STATE]
proof (state)
this:
concat (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) ! i = concat (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)) ! i

goal (2 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> unfill_holes MHole t = map ((|_) t) (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> unfill_holes x2a t = map ((|_) t) (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> unfill_holes (MFun x1a x2) t = map ((|_) t) (hole_poss_list (MFun x1a x2))
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i2 < length (concat (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts])) \<Longrightarrow> concat (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) ! ?i2 = concat (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)) ! ?i2

goal (2 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> unfill_holes MHole t = map ((|_) t) (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> unfill_holes x2a t = map ((|_) t) (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> unfill_holes (MFun x1a x2) t = map ((|_) t) (hole_poss_list (MFun x1a x2))
[PROOF STEP]
note nth = this
[PROOF STATE]
proof (state)
this:
?i2 < length (concat (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts])) \<Longrightarrow> concat (map (\<lambda>i. unfill_holes (ts ! i) (ss ! i)) [0..<length ts]) ! ?i2 = concat (map (\<lambda>x. map ((|_) (Fun f ss)) (case x of (x, y) \<Rightarrow> map ((#) x) (hole_poss_list y))) (zip [0..<length ts] ts)) ! ?i2

goal (2 subgoals):
 1. \<And>t. MHole \<le> mctxt_of_term t \<Longrightarrow> unfill_holes MHole t = map ((|_) t) (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> unfill_holes x2a t = map ((|_) t) (hole_poss_list x2a); MFun x1a x2 \<le> mctxt_of_term t\<rbrakk> \<Longrightarrow> unfill_holes (MFun x1a x2) t = map ((|_) t) (hole_poss_list (MFun x1a x2))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unfill_holes (MFun f ts) t = map ((|_) t) (hole_poss_list (MFun f ts))
[PROOF STEP]
using MFun
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set ts; ?x2a \<le> mctxt_of_term ?t\<rbrakk> \<Longrightarrow> unfill_holes ?x2a ?t = map ((|_) ?t) (hole_poss_list ?x2a)
MFun f ts \<le> mctxt_of_term t

goal (1 subgoal):
 1. unfill_holes (MFun f ts) t = map ((|_) t) (hole_poss_list (MFun f ts))
[PROOF STEP]
by (auto simp: comp_def map_concat length_concat
        elim!: less_eq_mctxt_MFunE1 split!: prod.splits
        intro!: nth_equalityI nth_sum_listI nth)
[PROOF STATE]
proof (state)
this:
unfill_holes (MFun f ts) t = map ((|_) t) (hole_poss_list (MFun f ts))

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


[STATEMENT]
lemma hole_poss_split_varposs_list_length [simp]:
  "length (hole_poss_list (fst (split_vars t))) = length (varposs_list t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (hole_poss_list (fst (split_vars t))) = length (varposs_list t)
[PROOF STEP]
by (induct t)(auto simp: length_concat comp_def intro!: nth_sum_listI)


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

goal (2 subgoals):
 1. \<And>x. hole_poss_list (fst (split_vars (Var x))) = varposs_list (Var x)
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> hole_poss_list (fst (split_vars x2a)) = varposs_list x2a) \<Longrightarrow> hole_poss_list (fst (split_vars (Fun x1a x2))) = varposs_list (Fun x1a x2)
[PROOF STEP]
let ?ts = "poss_args hole_poss_list (map (fst \<circ> split_vars) ts)"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. hole_poss_list (fst (split_vars (Var x))) = varposs_list (Var x)
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> hole_poss_list (fst (split_vars x2a)) = varposs_list x2a) \<Longrightarrow> hole_poss_list (fst (split_vars (Fun x1a x2))) = varposs_list (Fun x1a x2)
[PROOF STEP]
let ?ss = "poss_args varposs_list ts"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. hole_poss_list (fst (split_vars (Var x))) = varposs_list (Var x)
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> hole_poss_list (fst (split_vars x2a)) = varposs_list x2a) \<Longrightarrow> hole_poss_list (fst (split_vars (Fun x1a x2))) = varposs_list (Fun x1a x2)
[PROOF STEP]
have len: "length (concat ?ts) = length (concat ?ss)" "length ?ts = length ?ss"
    "\<forall> i < length ?ts. length (?ts ! i) = length (?ss ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. length (concat (poss_args hole_poss_list (map (fst \<circ> split_vars) ts))) = length (concat (poss_args varposs_list ts)) &&& length (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)) = length (poss_args varposs_list ts) &&& \<forall>i<length (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)). length (poss_args hole_poss_list (map (fst \<circ> split_vars) ts) ! i) = length (poss_args varposs_list ts ! i)
[PROOF STEP]
by (auto intro: eq_length_concat_nth)
[PROOF STATE]
proof (state)
this:
length (concat (poss_args hole_poss_list (map (fst \<circ> split_vars) ts))) = length (concat (poss_args varposs_list ts))
length (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)) = length (poss_args varposs_list ts)
\<forall>i<length (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)). length (poss_args hole_poss_list (map (fst \<circ> split_vars) ts) ! i) = length (poss_args varposs_list ts ! i)

goal (2 subgoals):
 1. \<And>x. hole_poss_list (fst (split_vars (Var x))) = varposs_list (Var x)
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> hole_poss_list (fst (split_vars x2a)) = varposs_list x2a) \<Longrightarrow> hole_poss_list (fst (split_vars (Fun x1a x2))) = varposs_list (Fun x1a x2)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
length (concat (poss_args hole_poss_list (map (fst \<circ> split_vars) ts))) = length (concat (poss_args varposs_list ts))
length (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)) = length (poss_args varposs_list ts)
\<forall>i<length (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)). length (poss_args hole_poss_list (map (fst \<circ> split_vars) ts) ! i) = length (poss_args varposs_list ts ! i)

goal (2 subgoals):
 1. \<And>x. hole_poss_list (fst (split_vars (Var x))) = varposs_list (Var x)
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> hole_poss_list (fst (split_vars x2a)) = varposs_list x2a) \<Longrightarrow> hole_poss_list (fst (split_vars (Fun x1a x2))) = varposs_list (Fun x1a x2)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. hole_poss_list (fst (split_vars (Var x))) = varposs_list (Var x)
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> hole_poss_list (fst (split_vars x2a)) = varposs_list x2a) \<Longrightarrow> hole_poss_list (fst (split_vars (Fun x1a x2))) = varposs_list (Fun x1a x2)
[PROOF STEP]
assume ass: "i < length (concat ?ts)"
[PROOF STATE]
proof (state)
this:
i < length (concat (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)))

goal (2 subgoals):
 1. \<And>x. hole_poss_list (fst (split_vars (Var x))) = varposs_list (Var x)
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> hole_poss_list (fst (split_vars x2a)) = varposs_list x2a) \<Longrightarrow> hole_poss_list (fst (split_vars (Fun x1a x2))) = varposs_list (Fun x1a x2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i < length (concat (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)))
[PROOF STEP]
have lss: "i < length (concat ?ss)"
[PROOF STATE]
proof (prove)
using this:
i < length (concat (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)))

goal (1 subgoal):
 1. i < length (concat (poss_args varposs_list ts))
[PROOF STEP]
using len
[PROOF STATE]
proof (prove)
using this:
i < length (concat (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)))
length (concat (poss_args hole_poss_list (map (fst \<circ> split_vars) ts))) = length (concat (poss_args varposs_list ts))
length (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)) = length (poss_args varposs_list ts)
\<forall>i<length (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)). length (poss_args hole_poss_list (map (fst \<circ> split_vars) ts) ! i) = length (poss_args varposs_list ts ! i)

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

goal (2 subgoals):
 1. \<And>x. hole_poss_list (fst (split_vars (Var x))) = varposs_list (Var x)
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> hole_poss_list (fst (split_vars x2a)) = varposs_list x2a) \<Longrightarrow> hole_poss_list (fst (split_vars (Fun x1a x2))) = varposs_list (Fun x1a x2)
[PROOF STEP]
obtain m n where int: "concat_index_split (0, i) ?ts = (m, n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m n. concat_index_split (0, i) (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)) = (m, n) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
concat_index_split (0, i) (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)) = (m, n)

goal (2 subgoals):
 1. \<And>x. hole_poss_list (fst (split_vars (Var x))) = varposs_list (Var x)
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> hole_poss_list (fst (split_vars x2a)) = varposs_list x2a) \<Longrightarrow> hole_poss_list (fst (split_vars (Fun x1a x2))) = varposs_list (Fun x1a x2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
concat_index_split (0, i) (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)) = (m, n)
[PROOF STEP]
have [simp]: "concat_index_split (0, i) ?ss = (m, n)"
[PROOF STATE]
proof (prove)
using this:
concat_index_split (0, i) (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)) = (m, n)

goal (1 subgoal):
 1. concat_index_split (0, i) (poss_args varposs_list ts) = (m, n)
[PROOF STEP]
using concat_index_split_unique[OF ass len(2-)]
[PROOF STATE]
proof (prove)
using this:
concat_index_split (0, i) (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)) = (m, n)
concat_index_split (?n, i) (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)) = concat_index_split (?n, i) (poss_args varposs_list ts)

goal (1 subgoal):
 1. concat_index_split (0, i) (poss_args varposs_list ts) = (m, n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
concat_index_split (0, i) (poss_args varposs_list ts) = (m, n)

goal (2 subgoals):
 1. \<And>x. hole_poss_list (fst (split_vars (Var x))) = varposs_list (Var x)
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> hole_poss_list (fst (split_vars x2a)) = varposs_list x2a) \<Longrightarrow> hole_poss_list (fst (split_vars (Fun x1a x2))) = varposs_list (Fun x1a x2)
[PROOF STEP]
from concat_index_split_less_length_concat(2-)[OF ass int] concat_index_split_less_length_concat(2-)[OF lss]
[PROOF STATE]
proof (chain)
picking this:
m < length (poss_args hole_poss_list (map (fst \<circ> split_vars) ts))
n < length (poss_args hole_poss_list (map (fst \<circ> split_vars) ts) ! m)
concat (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)) ! i = poss_args hole_poss_list (map (fst \<circ> split_vars) ts) ! m ! n
concat_index_split (0, i) (poss_args varposs_list ts) = (?m, ?n) \<Longrightarrow> ?m < length (poss_args varposs_list ts)
concat_index_split (0, i) (poss_args varposs_list ts) = (?m, ?n) \<Longrightarrow> ?n < length (poss_args varposs_list ts ! ?m)
concat_index_split (0, i) (poss_args varposs_list ts) = (?m, ?n) \<Longrightarrow> concat (poss_args varposs_list ts) ! i = poss_args varposs_list ts ! ?m ! ?n
[PROOF STEP]
have "concat ?ts ! i = concat ?ss! i"
[PROOF STATE]
proof (prove)
using this:
m < length (poss_args hole_poss_list (map (fst \<circ> split_vars) ts))
n < length (poss_args hole_poss_list (map (fst \<circ> split_vars) ts) ! m)
concat (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)) ! i = poss_args hole_poss_list (map (fst \<circ> split_vars) ts) ! m ! n
concat_index_split (0, i) (poss_args varposs_list ts) = (?m, ?n) \<Longrightarrow> ?m < length (poss_args varposs_list ts)
concat_index_split (0, i) (poss_args varposs_list ts) = (?m, ?n) \<Longrightarrow> ?n < length (poss_args varposs_list ts ! ?m)
concat_index_split (0, i) (poss_args varposs_list ts) = (?m, ?n) \<Longrightarrow> concat (poss_args varposs_list ts) ! i = poss_args varposs_list ts ! ?m ! ?n

goal (1 subgoal):
 1. concat (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)) ! i = concat (poss_args varposs_list ts) ! i
[PROOF STEP]
using Fun[OF nth_mem, of m]
[PROOF STATE]
proof (prove)
using this:
m < length (poss_args hole_poss_list (map (fst \<circ> split_vars) ts))
n < length (poss_args hole_poss_list (map (fst \<circ> split_vars) ts) ! m)
concat (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)) ! i = poss_args hole_poss_list (map (fst \<circ> split_vars) ts) ! m ! n
concat_index_split (0, i) (poss_args varposs_list ts) = (?m, ?n) \<Longrightarrow> ?m < length (poss_args varposs_list ts)
concat_index_split (0, i) (poss_args varposs_list ts) = (?m, ?n) \<Longrightarrow> ?n < length (poss_args varposs_list ts ! ?m)
concat_index_split (0, i) (poss_args varposs_list ts) = (?m, ?n) \<Longrightarrow> concat (poss_args varposs_list ts) ! i = poss_args varposs_list ts ! ?m ! ?n
m < length ts \<Longrightarrow> hole_poss_list (fst (split_vars (ts ! m))) = varposs_list (ts ! m)

goal (1 subgoal):
 1. concat (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)) ! i = concat (poss_args varposs_list ts) ! i
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
concat (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)) ! i = concat (poss_args varposs_list ts) ! i

goal (2 subgoals):
 1. \<And>x. hole_poss_list (fst (split_vars (Var x))) = varposs_list (Var x)
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> hole_poss_list (fst (split_vars x2a)) = varposs_list x2a) \<Longrightarrow> hole_poss_list (fst (split_vars (Fun x1a x2))) = varposs_list (Fun x1a x2)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i2 < length (concat (poss_args hole_poss_list (map (fst \<circ> split_vars) ts))) \<Longrightarrow> concat (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)) ! ?i2 = concat (poss_args varposs_list ts) ! ?i2

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

goal (1 subgoal):
 1. hole_poss_list (fst (split_vars (Fun f ts))) = varposs_list (Fun f ts)
[PROOF STEP]
using len
[PROOF STATE]
proof (prove)
using this:
?i2 < length (concat (poss_args hole_poss_list (map (fst \<circ> split_vars) ts))) \<Longrightarrow> concat (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)) ! ?i2 = concat (poss_args varposs_list ts) ! ?i2
length (concat (poss_args hole_poss_list (map (fst \<circ> split_vars) ts))) = length (concat (poss_args varposs_list ts))
length (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)) = length (poss_args varposs_list ts)
\<forall>i<length (poss_args hole_poss_list (map (fst \<circ> split_vars) ts)). length (poss_args hole_poss_list (map (fst \<circ> split_vars) ts) ! i) = length (poss_args varposs_list ts ! i)

goal (1 subgoal):
 1. hole_poss_list (fst (split_vars (Fun f ts))) = varposs_list (Fun f ts)
[PROOF STEP]
by (auto intro: nth_equalityI)
[PROOF STATE]
proof (state)
this:
hole_poss_list (fst (split_vars (Fun f ts))) = varposs_list (Fun f ts)

goal (1 subgoal):
 1. \<And>x. hole_poss_list (fst (split_vars (Var x))) = varposs_list (Var x)
[PROOF STEP]
qed auto


[STATEMENT]
lemma funas_term_fill_holes_iff: "num_holes C = length ts \<Longrightarrow>
   g \<in> funas_term (fill_holes C ts) \<longleftrightarrow> g \<in> funas_mctxt C \<or> (\<exists>t \<in> set ts. g \<in> funas_term t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. num_holes C = length ts \<Longrightarrow> (g \<in> funas_term (fill_holes C ts)) = (g \<in> funas_mctxt C \<or> (\<exists>t\<in>set ts. g \<in> funas_term t))
[PROOF STEP]
proof (induct C ts rule: fill_holes_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. (g \<in> funas_term (fill_holes MHole [x])) = (g \<in> funas_mctxt MHole \<or> (\<exists>t\<in>set [x]. g \<in> funas_term t))
 2. \<And>v. (g \<in> funas_term (fill_holes (MVar v) [])) = (g \<in> funas_mctxt (MVar v) \<or> (\<exists>t\<in>set []. g \<in> funas_term t))
 3. \<And>f Cs xs. \<lbrakk>sum_list (map num_holes Cs) = length xs; \<And>i. i < length Cs \<Longrightarrow> (g \<in> funas_term (fill_holes (Cs ! i) (partition_holes xs Cs ! i))) = (g \<in> funas_mctxt (Cs ! i) \<or> (\<exists>t\<in>set (partition_holes xs Cs ! i). g \<in> funas_term t))\<rbrakk> \<Longrightarrow> (g \<in> funas_term (fill_holes (MFun f Cs) (concat (partition_holes xs Cs)))) = (g \<in> funas_mctxt (MFun f Cs) \<or> (\<exists>t\<in>set (concat (partition_holes xs Cs)). g \<in> funas_term t))
[PROOF STEP]
case (MFun f Cs ts)
[PROOF STATE]
proof (state)
this:
sum_list (map num_holes Cs) = length ts
?i < length Cs \<Longrightarrow> (g \<in> funas_term (fill_holes (Cs ! ?i) (partition_holes ts Cs ! ?i))) = (g \<in> funas_mctxt (Cs ! ?i) \<or> (\<exists>t\<in>set (partition_holes ts Cs ! ?i). g \<in> funas_term t))

goal (3 subgoals):
 1. \<And>x. (g \<in> funas_term (fill_holes MHole [x])) = (g \<in> funas_mctxt MHole \<or> (\<exists>t\<in>set [x]. g \<in> funas_term t))
 2. \<And>v. (g \<in> funas_term (fill_holes (MVar v) [])) = (g \<in> funas_mctxt (MVar v) \<or> (\<exists>t\<in>set []. g \<in> funas_term t))
 3. \<And>f Cs xs. \<lbrakk>sum_list (map num_holes Cs) = length xs; \<And>i. i < length Cs \<Longrightarrow> (g \<in> funas_term (fill_holes (Cs ! i) (partition_holes xs Cs ! i))) = (g \<in> funas_mctxt (Cs ! i) \<or> (\<exists>t\<in>set (partition_holes xs Cs ! i). g \<in> funas_term t))\<rbrakk> \<Longrightarrow> (g \<in> funas_term (fill_holes (MFun f Cs) (concat (partition_holes xs Cs)))) = (g \<in> funas_mctxt (MFun f Cs) \<or> (\<exists>t\<in>set (concat (partition_holes xs Cs)). g \<in> funas_term t))
[PROOF STEP]
have "(\<exists>i < length Cs. g \<in> funas_term (fill_holes (Cs ! i) (partition_holes (concat (partition_holes ts Cs)) Cs ! i)))
    \<longleftrightarrow> (\<exists>C \<in> set Cs. g \<in> funas_mctxt C) \<or> (\<exists>us \<in> set (partition_holes ts Cs). \<exists>t \<in> set us. g \<in> funas_term t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>i<length Cs. g \<in> funas_term (fill_holes (Cs ! i) (partition_holes (concat (partition_holes ts Cs)) Cs ! i))) = ((\<exists>C\<in>set Cs. g \<in> funas_mctxt C) \<or> (\<exists>us\<in>set (partition_holes ts Cs). \<exists>t\<in>set us. g \<in> funas_term t))
[PROOF STEP]
using MFun
[PROOF STATE]
proof (prove)
using this:
sum_list (map num_holes Cs) = length ts
?i < length Cs \<Longrightarrow> (g \<in> funas_term (fill_holes (Cs ! ?i) (partition_holes ts Cs ! ?i))) = (g \<in> funas_mctxt (Cs ! ?i) \<or> (\<exists>t\<in>set (partition_holes ts Cs ! ?i). g \<in> funas_term t))

goal (1 subgoal):
 1. (\<exists>i<length Cs. g \<in> funas_term (fill_holes (Cs ! i) (partition_holes (concat (partition_holes ts Cs)) Cs ! i))) = ((\<exists>C\<in>set Cs. g \<in> funas_mctxt C) \<or> (\<exists>us\<in>set (partition_holes ts Cs). \<exists>t\<in>set us. g \<in> funas_term t))
[PROOF STEP]
by (auto simp: ex_set_conv_ex_nth) blast
[PROOF STATE]
proof (state)
this:
(\<exists>i<length Cs. g \<in> funas_term (fill_holes (Cs ! i) (partition_holes (concat (partition_holes ts Cs)) Cs ! i))) = ((\<exists>C\<in>set Cs. g \<in> funas_mctxt C) \<or> (\<exists>us\<in>set (partition_holes ts Cs). \<exists>t\<in>set us. g \<in> funas_term t))

goal (3 subgoals):
 1. \<And>x. (g \<in> funas_term (fill_holes MHole [x])) = (g \<in> funas_mctxt MHole \<or> (\<exists>t\<in>set [x]. g \<in> funas_term t))
 2. \<And>v. (g \<in> funas_term (fill_holes (MVar v) [])) = (g \<in> funas_mctxt (MVar v) \<or> (\<exists>t\<in>set []. g \<in> funas_term t))
 3. \<And>f Cs xs. \<lbrakk>sum_list (map num_holes Cs) = length xs; \<And>i. i < length Cs \<Longrightarrow> (g \<in> funas_term (fill_holes (Cs ! i) (partition_holes xs Cs ! i))) = (g \<in> funas_mctxt (Cs ! i) \<or> (\<exists>t\<in>set (partition_holes xs Cs ! i). g \<in> funas_term t))\<rbrakk> \<Longrightarrow> (g \<in> funas_term (fill_holes (MFun f Cs) (concat (partition_holes xs Cs)))) = (g \<in> funas_mctxt (MFun f Cs) \<or> (\<exists>t\<in>set (concat (partition_holes xs Cs)). g \<in> funas_term t))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<exists>i<length Cs. g \<in> funas_term (fill_holes (Cs ! i) (partition_holes (concat (partition_holes ts Cs)) Cs ! i))) = ((\<exists>C\<in>set Cs. g \<in> funas_mctxt C) \<or> (\<exists>us\<in>set (partition_holes ts Cs). \<exists>t\<in>set us. g \<in> funas_term t))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<exists>i<length Cs. g \<in> funas_term (fill_holes (Cs ! i) (partition_holes (concat (partition_holes ts Cs)) Cs ! i))) = ((\<exists>C\<in>set Cs. g \<in> funas_mctxt C) \<or> (\<exists>us\<in>set (partition_holes ts Cs). \<exists>t\<in>set us. g \<in> funas_term t))

goal (1 subgoal):
 1. (g \<in> funas_term (fill_holes (MFun f Cs) (concat (partition_holes ts Cs)))) = (g \<in> funas_mctxt (MFun f Cs) \<or> (\<exists>t\<in>set (concat (partition_holes ts Cs)). g \<in> funas_term t))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(g \<in> funas_term (fill_holes (MFun f Cs) (concat (partition_holes ts Cs)))) = (g \<in> funas_mctxt (MFun f Cs) \<or> (\<exists>t\<in>set (concat (partition_holes ts Cs)). g \<in> funas_term t))

goal (2 subgoals):
 1. \<And>x. (g \<in> funas_term (fill_holes MHole [x])) = (g \<in> funas_mctxt MHole \<or> (\<exists>t\<in>set [x]. g \<in> funas_term t))
 2. \<And>v. (g \<in> funas_term (fill_holes (MVar v) [])) = (g \<in> funas_mctxt (MVar v) \<or> (\<exists>t\<in>set []. g \<in> funas_term t))
[PROOF STEP]
qed auto


[STATEMENT]
lemma vars_term_fill_holes [simp]:
  "num_holes C = length ts \<Longrightarrow> ground_mctxt C \<Longrightarrow>
    vars_term (fill_holes C ts) = \<Union>(vars_term ` set ts)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>num_holes C = length ts; ground_mctxt C\<rbrakk> \<Longrightarrow> vars_term (fill_holes C ts) = \<Union> (vars_term ` set ts)
[PROOF STEP]
proof (induct C arbitrary: ts)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x ts. \<lbrakk>num_holes (MVar x) = length ts; ground_mctxt (MVar x)\<rbrakk> \<Longrightarrow> vars_term (fill_holes (MVar x) ts) = \<Union> (vars_term ` set ts)
 2. \<And>ts. \<lbrakk>num_holes MHole = length ts; ground_mctxt MHole\<rbrakk> \<Longrightarrow> vars_term (fill_holes MHole ts) = \<Union> (vars_term ` set ts)
 3. \<And>x1a x2 ts. \<lbrakk>\<And>x2a ts. \<lbrakk>x2a \<in> set x2; num_holes x2a = length ts; ground_mctxt x2a\<rbrakk> \<Longrightarrow> vars_term (fill_holes x2a ts) = \<Union> (vars_term ` set ts); num_holes (MFun x1a x2) = length ts; ground_mctxt (MFun x1a x2)\<rbrakk> \<Longrightarrow> vars_term (fill_holes (MFun x1a x2) ts) = \<Union> (vars_term ` set ts)
[PROOF STEP]
case MHole
[PROOF STATE]
proof (state)
this:
num_holes MHole = length ts
ground_mctxt MHole

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

goal (1 subgoal):
 1. vars_term (fill_holes MHole ts) = \<Union> (vars_term ` set ts)
[PROOF STEP]
by (cases ts) simp_all
[PROOF STATE]
proof (state)
this:
vars_term (fill_holes MHole ts) = \<Union> (vars_term ` set ts)

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

goal (2 subgoals):
 1. \<And>x ts. \<lbrakk>num_holes (MVar x) = length ts; ground_mctxt (MVar x)\<rbrakk> \<Longrightarrow> vars_term (fill_holes (MVar x) ts) = \<Union> (vars_term ` set ts)
 2. \<And>x1a x2 ts. \<lbrakk>\<And>x2a ts. \<lbrakk>x2a \<in> set x2; num_holes x2a = length ts; ground_mctxt x2a\<rbrakk> \<Longrightarrow> vars_term (fill_holes x2a ts) = \<Union> (vars_term ` set ts); num_holes (MFun x1a x2) = length ts; ground_mctxt (MFun x1a x2)\<rbrakk> \<Longrightarrow> vars_term (fill_holes (MFun x1a x2) ts) = \<Union> (vars_term ` set ts)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x2a \<in> set Cs; num_holes ?x2a = length ?ts; ground_mctxt ?x2a\<rbrakk> \<Longrightarrow> vars_term (fill_holes ?x2a ?ts) = \<Union> (vars_term ` set ?ts)
num_holes (MFun f Cs) = length ts
ground_mctxt (MFun f Cs)
[PROOF STEP]
have *: "length (partition_holes ts Cs) = length Cs"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set Cs; num_holes ?x2a = length ?ts; ground_mctxt ?x2a\<rbrakk> \<Longrightarrow> vars_term (fill_holes ?x2a ?ts) = \<Union> (vars_term ` set ?ts)
num_holes (MFun f Cs) = length ts
ground_mctxt (MFun f Cs)

goal (1 subgoal):
 1. length (partition_holes ts Cs) = length Cs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length (partition_holes ts Cs) = length Cs

goal (2 subgoals):
 1. \<And>x ts. \<lbrakk>num_holes (MVar x) = length ts; ground_mctxt (MVar x)\<rbrakk> \<Longrightarrow> vars_term (fill_holes (MVar x) ts) = \<Union> (vars_term ` set ts)
 2. \<And>x1a x2 ts. \<lbrakk>\<And>x2a ts. \<lbrakk>x2a \<in> set x2; num_holes x2a = length ts; ground_mctxt x2a\<rbrakk> \<Longrightarrow> vars_term (fill_holes x2a ts) = \<Union> (vars_term ` set ts); num_holes (MFun x1a x2) = length ts; ground_mctxt (MFun x1a x2)\<rbrakk> \<Longrightarrow> vars_term (fill_holes (MFun x1a x2) ts) = \<Union> (vars_term ` set ts)
[PROOF STEP]
let ?f = "\<lambda>x. \<Union>y \<in> set x. vars_term y"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x ts. \<lbrakk>num_holes (MVar x) = length ts; ground_mctxt (MVar x)\<rbrakk> \<Longrightarrow> vars_term (fill_holes (MVar x) ts) = \<Union> (vars_term ` set ts)
 2. \<And>x1a x2 ts. \<lbrakk>\<And>x2a ts. \<lbrakk>x2a \<in> set x2; num_holes x2a = length ts; ground_mctxt x2a\<rbrakk> \<Longrightarrow> vars_term (fill_holes x2a ts) = \<Union> (vars_term ` set ts); num_holes (MFun x1a x2) = length ts; ground_mctxt (MFun x1a x2)\<rbrakk> \<Longrightarrow> vars_term (fill_holes (MFun x1a x2) ts) = \<Union> (vars_term ` set ts)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vars_term (fill_holes (MFun f Cs) ts) = \<Union> (vars_term ` set ts)
[PROOF STEP]
using MFun
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set Cs; num_holes ?x2a = length ?ts; ground_mctxt ?x2a\<rbrakk> \<Longrightarrow> vars_term (fill_holes ?x2a ?ts) = \<Union> (vars_term ` set ?ts)
num_holes (MFun f Cs) = length ts
ground_mctxt (MFun f Cs)

goal (1 subgoal):
 1. vars_term (fill_holes (MFun f Cs) ts) = \<Union> (vars_term ` set ts)
[PROOF STEP]
unfolding partition_holes_fill_holes_conv
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set Cs; num_holes ?x2a = length ?ts; ground_mctxt ?x2a\<rbrakk> \<Longrightarrow> vars_term (fill_holes ?x2a ?ts) = \<Union> (vars_term ` set ?ts)
num_holes (MFun f Cs) = length ts
ground_mctxt (MFun f Cs)

goal (1 subgoal):
 1. vars_term (Fun f (map (\<lambda>i. fill_holes (Cs ! i) (partition_holes ts Cs ! i)) [0..<length Cs])) = \<Union> (vars_term ` set ts)
[PROOF STEP]
by (simp add: UN_upt_len_conv [OF *, of ?f] UN_set_partition_by)
[PROOF STATE]
proof (state)
this:
vars_term (fill_holes (MFun f Cs) ts) = \<Union> (vars_term ` set ts)

goal (1 subgoal):
 1. \<And>x ts. \<lbrakk>num_holes (MVar x) = length ts; ground_mctxt (MVar x)\<rbrakk> \<Longrightarrow> vars_term (fill_holes (MVar x) ts) = \<Union> (vars_term ` set ts)
[PROOF STEP]
qed simp


[STATEMENT]
lemma funas_mctxt_fill_holes [simp]:
  assumes "num_holes C = length ts"
  shows "funas_term (fill_holes C ts) = funas_mctxt C \<union> \<Union>(set (map funas_term ts))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_term (fill_holes C ts) = funas_mctxt C \<union> \<Union> (set (map funas_term ts))
[PROOF STEP]
using funas_term_fill_holes_iff[OF assms]
[PROOF STATE]
proof (prove)
using this:
(?g \<in> funas_term (fill_holes C ts)) = (?g \<in> funas_mctxt C \<or> (\<exists>t\<in>set ts. ?g \<in> funas_term t))

goal (1 subgoal):
 1. funas_term (fill_holes C ts) = funas_mctxt C \<union> \<Union> (set (map funas_term ts))
[PROOF STEP]
by auto


[STATEMENT]
lemma funas_mctxt_fill_holes_mctxt [simp]:
  assumes "num_holes C = length Ds"
  shows "funas_mctxt (fill_holes_mctxt C Ds) = funas_mctxt C \<union> \<Union>(set (map funas_mctxt Ds))"
  (is "?f C Ds = ?g C Ds")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. funas_mctxt (fill_holes_mctxt C Ds) = funas_mctxt C \<union> \<Union> (set (map funas_mctxt Ds))
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
num_holes C = length Ds

goal (1 subgoal):
 1. funas_mctxt (fill_holes_mctxt C Ds) = funas_mctxt C \<union> \<Union> (set (map funas_mctxt Ds))
[PROOF STEP]
proof (induct C arbitrary: Ds)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x Ds. num_holes (MVar x) = length Ds \<Longrightarrow> funas_mctxt (fill_holes_mctxt (MVar x) Ds) = funas_mctxt (MVar x) \<union> \<Union> (set (map funas_mctxt Ds))
 2. \<And>Ds. num_holes MHole = length Ds \<Longrightarrow> funas_mctxt (fill_holes_mctxt MHole Ds) = funas_mctxt MHole \<union> \<Union> (set (map funas_mctxt Ds))
 3. \<And>x1a x2 Ds. \<lbrakk>\<And>x2a Ds. \<lbrakk>x2a \<in> set x2; num_holes x2a = length Ds\<rbrakk> \<Longrightarrow> funas_mctxt (fill_holes_mctxt x2a Ds) = funas_mctxt x2a \<union> \<Union> (set (map funas_mctxt Ds)); num_holes (MFun x1a x2) = length Ds\<rbrakk> \<Longrightarrow> funas_mctxt (fill_holes_mctxt (MFun x1a x2) Ds) = funas_mctxt (MFun x1a x2) \<union> \<Union> (set (map funas_mctxt Ds))
[PROOF STEP]
case MHole
[PROOF STATE]
proof (state)
this:
num_holes MHole = length Ds

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

goal (1 subgoal):
 1. funas_mctxt (fill_holes_mctxt MHole Ds) = funas_mctxt MHole \<union> \<Union> (set (map funas_mctxt Ds))
[PROOF STEP]
by (cases Ds) simp_all
[PROOF STATE]
proof (state)
this:
funas_mctxt (fill_holes_mctxt MHole Ds) = funas_mctxt MHole \<union> \<Union> (set (map funas_mctxt Ds))

goal (2 subgoals):
 1. \<And>x Ds. num_holes (MVar x) = length Ds \<Longrightarrow> funas_mctxt (fill_holes_mctxt (MVar x) Ds) = funas_mctxt (MVar x) \<union> \<Union> (set (map funas_mctxt Ds))
 2. \<And>x1a x2 Ds. \<lbrakk>\<And>x2a Ds. \<lbrakk>x2a \<in> set x2; num_holes x2a = length Ds\<rbrakk> \<Longrightarrow> funas_mctxt (fill_holes_mctxt x2a Ds) = funas_mctxt x2a \<union> \<Union> (set (map funas_mctxt Ds)); num_holes (MFun x1a x2) = length Ds\<rbrakk> \<Longrightarrow> funas_mctxt (fill_holes_mctxt (MFun x1a x2) Ds) = funas_mctxt (MFun x1a x2) \<union> \<Union> (set (map funas_mctxt Ds))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x Ds. num_holes (MVar x) = length Ds \<Longrightarrow> funas_mctxt (fill_holes_mctxt (MVar x) Ds) = funas_mctxt (MVar x) \<union> \<Union> (set (map funas_mctxt Ds))
 2. \<And>x1a x2 Ds. \<lbrakk>\<And>x2a Ds. \<lbrakk>x2a \<in> set x2; num_holes x2a = length Ds\<rbrakk> \<Longrightarrow> funas_mctxt (fill_holes_mctxt x2a Ds) = funas_mctxt x2a \<union> \<Union> (set (map funas_mctxt Ds)); num_holes (MFun x1a x2) = length Ds\<rbrakk> \<Longrightarrow> funas_mctxt (fill_holes_mctxt (MFun x1a x2) Ds) = funas_mctxt (MFun x1a x2) \<union> \<Union> (set (map funas_mctxt Ds))
[PROOF STEP]
case (MFun f Cs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x2a \<in> set Cs; num_holes ?x2a = length ?Ds\<rbrakk> \<Longrightarrow> funas_mctxt (fill_holes_mctxt ?x2a ?Ds) = funas_mctxt ?x2a \<union> \<Union> (set (map funas_mctxt ?Ds))
num_holes (MFun f Cs) = length Ds

goal (2 subgoals):
 1. \<And>x Ds. num_holes (MVar x) = length Ds \<Longrightarrow> funas_mctxt (fill_holes_mctxt (MVar x) Ds) = funas_mctxt (MVar x) \<union> \<Union> (set (map funas_mctxt Ds))
 2. \<And>x1a x2 Ds. \<lbrakk>\<And>x2a Ds. \<lbrakk>x2a \<in> set x2; num_holes x2a = length Ds\<rbrakk> \<Longrightarrow> funas_mctxt (fill_holes_mctxt x2a Ds) = funas_mctxt x2a \<union> \<Union> (set (map funas_mctxt Ds)); num_holes (MFun x1a x2) = length Ds\<rbrakk> \<Longrightarrow> funas_mctxt (fill_holes_mctxt (MFun x1a x2) Ds) = funas_mctxt (MFun x1a x2) \<union> \<Union> (set (map funas_mctxt Ds))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x2a \<in> set Cs; num_holes ?x2a = length ?Ds\<rbrakk> \<Longrightarrow> funas_mctxt (fill_holes_mctxt ?x2a ?Ds) = funas_mctxt ?x2a \<union> \<Union> (set (map funas_mctxt ?Ds))
num_holes (MFun f Cs) = length Ds
[PROOF STEP]
have num_holes: "sum_list (map num_holes Cs) = length Ds"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set Cs; num_holes ?x2a = length ?Ds\<rbrakk> \<Longrightarrow> funas_mctxt (fill_holes_mctxt ?x2a ?Ds) = funas_mctxt ?x2a \<union> \<Union> (set (map funas_mctxt ?Ds))
num_holes (MFun f Cs) = length Ds

goal (1 subgoal):
 1. sum_list (map num_holes Cs) = length Ds
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
sum_list (map num_holes Cs) = length Ds

goal (2 subgoals):
 1. \<And>x Ds. num_holes (MVar x) = length Ds \<Longrightarrow> funas_mctxt (fill_holes_mctxt (MVar x) Ds) = funas_mctxt (MVar x) \<union> \<Union> (set (map funas_mctxt Ds))
 2. \<And>x1a x2 Ds. \<lbrakk>\<And>x2a Ds. \<lbrakk>x2a \<in> set x2; num_holes x2a = length Ds\<rbrakk> \<Longrightarrow> funas_mctxt (fill_holes_mctxt x2a Ds) = funas_mctxt x2a \<union> \<Union> (set (map funas_mctxt Ds)); num_holes (MFun x1a x2) = length Ds\<rbrakk> \<Longrightarrow> funas_mctxt (fill_holes_mctxt (MFun x1a x2) Ds) = funas_mctxt (MFun x1a x2) \<union> \<Union> (set (map funas_mctxt Ds))
[PROOF STEP]
let ?ys = "partition_holes Ds Cs"
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x Ds. num_holes (MVar x) = length Ds \<Longrightarrow> funas_mctxt (fill_holes_mctxt (MVar x) Ds) = funas_mctxt (MVar x) \<union> \<Union> (set (map funas_mctxt Ds))
 2. \<And>x1a x2 Ds. \<lbrakk>\<And>x2a Ds. \<lbrakk>x2a \<in> set x2; num_holes x2a = length Ds\<rbrakk> \<Longrightarrow> funas_mctxt (fill_holes_mctxt x2a Ds) = funas_mctxt x2a \<union> \<Union> (set (map funas_mctxt Ds)); num_holes (MFun x1a x2) = length Ds\<rbrakk> \<Longrightarrow> funas_mctxt (fill_holes_mctxt (MFun x1a x2) Ds) = funas_mctxt (MFun x1a x2) \<union> \<Union> (set (map funas_mctxt Ds))
[PROOF STEP]
have "\<And>i. i < length Cs \<Longrightarrow> ?f (Cs ! i) (?ys ! i) = ?g (Cs ! i) (?ys ! i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < length Cs \<Longrightarrow> funas_mctxt (fill_holes_mctxt (Cs ! i) (partition_holes Ds Cs ! i)) = funas_mctxt (Cs ! i) \<union> \<Union> (set (map funas_mctxt (partition_holes Ds Cs ! i)))
[PROOF STEP]
using MFun
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x2a \<in> set Cs; num_holes ?x2a = length ?Ds\<rbrakk> \<Longrightarrow> funas_mctxt (fill_holes_mctxt ?x2a ?Ds) = funas_mctxt ?x2a \<union> \<Union> (set (map funas_mctxt ?Ds))
num_holes (MFun f Cs) = length Ds

goal (1 subgoal):
 1. \<And>i. i < length Cs \<Longrightarrow> funas_mctxt (fill_holes_mctxt (Cs ! i) (partition_holes Ds Cs ! i)) = funas_mctxt (Cs ! i) \<union> \<Union> (set (map funas_mctxt (partition_holes Ds Cs ! i)))
[PROOF STEP]
by (metis nth_mem num_holes.simps(3) length_partition_holes_nth)
[PROOF STATE]
proof (state)
this:
?i < length Cs \<Longrightarrow> funas_mctxt (fill_holes_mctxt (Cs ! ?i) (partition_holes Ds Cs ! ?i)) = funas_mctxt (Cs ! ?i) \<union> \<Union> (set (map funas_mctxt (partition_holes Ds Cs ! ?i)))

goal (2 subgoals):
 1. \<And>x Ds. num_holes (MVar x) = length Ds \<Longrightarrow> funas_mctxt (fill_holes_mctxt (MVar x) Ds) = funas_mctxt (MVar x) \<union> \<Union> (set (map funas_mctxt Ds))
 2. \<And>x1a x2 Ds. \<lbrakk>\<And>x2a Ds. \<lbrakk>x2a \<in> set x2; num_holes x2a = length Ds\<rbrakk> \<Longrightarrow> funas_mctxt (fill_holes_mctxt x2a Ds) = funas_mctxt x2a \<union> \<Union> (set (map funas_mctxt Ds)); num_holes (MFun x1a x2) = length Ds\<rbrakk> \<Longrightarrow> funas_mctxt (fill_holes_mctxt (MFun x1a x2) Ds) = funas_mctxt (MFun x1a x2) \<union> \<Union> (set (map funas_mctxt Ds))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
?i < length Cs \<Longrightarrow> funas_mctxt (fill_holes_mctxt (Cs ! ?i) (partition_holes Ds Cs ! ?i)) = funas_mctxt (Cs ! ?i) \<union> \<Union> (set (map funas_mctxt (partition_holes Ds Cs ! ?i)))
[PROOF STEP]
have "(\<Union>i \<in> {0 ..< length Cs}. ?f (Cs ! i) (?ys ! i)) =
    (\<Union>i \<in> {0 ..< length Cs}. ?g (Cs ! i) (?ys ! i))"
[PROOF STATE]
proof (prove)
using this:
?i < length Cs \<Longrightarrow> funas_mctxt (fill_holes_mctxt (Cs ! ?i) (partition_holes Ds Cs ! ?i)) = funas_mctxt (Cs ! ?i) \<union> \<Union> (set (map funas_mctxt (partition_holes Ds Cs ! ?i)))

goal (1 subgoal):
 1. (\<Union>i\<in>{0..<length Cs}. funas_mctxt (fill_holes_mctxt (Cs ! i) (partition_holes Ds Cs ! i))) = (\<Union>i\<in>{0..<length Cs}. funas_mctxt (Cs ! i) \<union> \<Union> (set (map funas_mctxt (partition_holes Ds Cs ! i))))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(\<Union>i\<in>{0..<length Cs}. funas_mctxt (fill_holes_mctxt (Cs ! i) (partition_holes Ds Cs ! i))) = (\<Union>i\<in>{0..<length Cs}. funas_mctxt (Cs ! i) \<union> \<Union> (set (map funas_mctxt (partition_holes Ds Cs ! i))))

goal (2 subgoals):
 1. \<And>x Ds. num_holes (MVar x) = length Ds \<Longrightarrow> funas_mctxt (fill_holes_mctxt (MVar x) Ds) = funas_mctxt (MVar x) \<union> \<Union> (set (map funas_mctxt Ds))
 2. \<And>x1a x2 Ds. \<lbrakk>\<And>x2a Ds. \<lbrakk>x2a \<in> set x2; num_holes x2a = length Ds\<rbrakk> \<Longrightarrow> funas_mctxt (fill_holes_mctxt x2a Ds) = funas_mctxt x2a \<union> \<Union> (set (map funas_mctxt Ds)); num_holes (MFun x1a x2) = length Ds\<rbrakk> \<Longrightarrow> funas_mctxt (fill_holes_mctxt (MFun x1a x2) Ds) = funas_mctxt (MFun x1a x2) \<union> \<Union> (set (map funas_mctxt Ds))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(\<Union>i\<in>{0..<length Cs}. funas_mctxt (fill_holes_mctxt (Cs ! i) (partition_holes Ds Cs ! i))) = (\<Union>i\<in>{0..<length Cs}. funas_mctxt (Cs ! i) \<union> \<Union> (set (map funas_mctxt (partition_holes Ds Cs ! i))))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Union>i\<in>{0..<length Cs}. funas_mctxt (fill_holes_mctxt (Cs ! i) (partition_holes Ds Cs ! i))) = (\<Union>i\<in>{0..<length Cs}. funas_mctxt (Cs ! i) \<union> \<Union> (set (map funas_mctxt (partition_holes Ds Cs ! i))))

goal (1 subgoal):
 1. funas_mctxt (fill_holes_mctxt (MFun f Cs) Ds) = funas_mctxt (MFun f Cs) \<union> \<Union> (set (map funas_mctxt Ds))
[PROOF STEP]
using num_holes
[PROOF STATE]
proof (prove)
using this:
(\<Union>i\<in>{0..<length Cs}. funas_mctxt (fill_holes_mctxt (Cs ! i) (partition_holes Ds Cs ! i))) = (\<Union>i\<in>{0..<length Cs}. funas_mctxt (Cs ! i) \<union> \<Union> (set (map funas_mctxt (partition_holes Ds Cs ! i))))
sum_list (map num_holes Cs) = length Ds

goal (1 subgoal):
 1. funas_mctxt (fill_holes_mctxt (MFun f Cs) Ds) = funas_mctxt (MFun f Cs) \<union> \<Union> (set (map funas_mctxt Ds))
[PROOF STEP]
unfolding partition_holes_fill_holes_mctxt_conv
[PROOF STATE]
proof (prove)
using this:
(\<Union>i\<in>{0..<length Cs}. funas_mctxt (fill_holes_mctxt (Cs ! i) (partition_holes Ds Cs ! i))) = (\<Union>i\<in>{0..<length Cs}. funas_mctxt (Cs ! i) \<union> \<Union> (set (map funas_mctxt (partition_holes Ds Cs ! i))))
sum_list (map num_holes Cs) = length Ds

goal (1 subgoal):
 1. funas_mctxt (MFun f (map (\<lambda>i. fill_holes_mctxt (Cs ! i) (partition_holes Ds Cs ! i)) [0..<length Cs])) = funas_mctxt (MFun f Cs) \<union> \<Union> (set (map funas_mctxt Ds))
[PROOF STEP]
by (simp add: UN_Un_distrib UN_upt_len_conv [of _ _ "\<lambda>x. \<Union>(set x)"] UN_set_partition_by_map)
[PROOF STATE]
proof (state)
this:
funas_mctxt (fill_holes_mctxt (MFun f Cs) Ds) = funas_mctxt (MFun f Cs) \<union> \<Union> (set (map funas_mctxt Ds))

goal (1 subgoal):
 1. \<And>x Ds. num_holes (MVar x) = length Ds \<Longrightarrow> funas_mctxt (fill_holes_mctxt (MVar x) Ds) = funas_mctxt (MVar x) \<union> \<Union> (set (map funas_mctxt Ds))
[PROOF STEP]
qed simp


[STATEMENT]
lemma append_singl_rev: "a # as = [a] @ as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a # as = [a] @ as
[PROOF STEP]
by simp


[STATEMENT]
lemma list_pair_induct[case_names Nil Cons]:
assumes "P []" and "\<And>a b list. P list \<Longrightarrow> P ((a,b) # list)"
shows "P lista"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P lista
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
P []
P ?list \<Longrightarrow> P ((?a, ?b) # ?list)

goal (1 subgoal):
 1. P lista
[PROOF STEP]
by (induction lista) auto


[STATEMENT]
lemma list_pair_case[elim, case_names Nil Cons]:
assumes "xs = [] \<Longrightarrow> P" and "\<And>a b list. xs = (a,b) # list \<Longrightarrow> P"
shows "P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs = [] \<Longrightarrow> P
xs = (?a, ?b) # ?list \<Longrightarrow> P

goal (1 subgoal):
 1. P
[PROOF STEP]
by(cases xs, auto)


[STATEMENT]
lemma asList:
assumes "finite A" shows "distinct (asList A) \<and> set (asList A) = A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (asList A) \<and> set (asList A) = A
[PROOF STEP]
unfolding asList_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (SOME as. distinct as \<and> set as = A) \<and> set (SOME as. distinct as \<and> set as = A) = A
[PROOF STEP]
by (rule someI_ex) (metis assms finite_distinct_list)


[STATEMENT]
lemma map_sdrop[simp]: "sdrop 0 = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sdrop 0 = id
[PROOF STEP]
by (auto intro: ext)


[STATEMENT]
lemma stl_o_sdrop[simp]: "stl o sdrop n = sdrop (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. stl \<circ> sdrop n = sdrop (Suc n)
[PROOF STEP]
by (auto intro: ext)


[STATEMENT]
lemma sdrop_o_stl[simp]: "sdrop n o stl = sdrop (Suc n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sdrop n \<circ> stl = sdrop (Suc n)
[PROOF STEP]
by (auto intro: ext)


[STATEMENT]
lemma hd_stake[simp]: "i > 0 \<Longrightarrow> hd (stake i \<pi>) = shd \<pi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < i \<Longrightarrow> hd (stake i \<pi>) = shd \<pi>
[PROOF STEP]
by (cases i) auto


[STATEMENT]
lemma mdl2mdl_wf:
  fixes phi :: "('a, 't :: timestamp) Preliminaries.formula"
  shows "wf_fmla (mdl2mdl phi)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_fmla (mdl2mdl phi)
[PROOF STEP]
by (induction phi rule: mdl2mdl_embed.induct(1)[where ?Q="\<lambda>r. wf_regex (Times (embed r) (Symbol (Bool True))) \<and> (\<forall>phi \<in> atms (embed r). wf_fmla phi)"]) auto


[STATEMENT]
lemma embed'_cong[fundef_cong]: "(\<And>phi. phi \<in> atms r \<Longrightarrow> f phi = f' phi) \<Longrightarrow> embed' f r = embed' f' r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>phi. phi \<in> atms r \<Longrightarrow> f phi = f' phi) \<Longrightarrow> embed' f r = embed' f' r
[PROOF STEP]
by (induction r) auto


[STATEMENT]
lemma mdl2mdl_equivalent:
  fixes phi :: "('a, 't :: timestamp) Preliminaries.formula"
  shows "\<And>i. sat (mdl2mdl phi) i \<longleftrightarrow> rvsat phi i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. sat (mdl2mdl phi) i = rvsat phi i
[PROOF STEP]
by (induction phi rule: mdl2mdl_embed.induct(1)[where ?Q="\<lambda>r. match (embed r) = rvmatch r"]) (auto split: nat.splits)


[STATEMENT]
lemma mdlstar2mdl:
  fixes phi :: "('a, 't :: timestamp) Preliminaries.formula"
  shows "wf_fmla (mdl2mdl phi)" "\<And>i. sat (mdl2mdl phi) i \<longleftrightarrow> rvsat phi i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wf_fmla (mdl2mdl phi) &&& (\<And>i. sat (mdl2mdl phi) i = rvsat phi i)
[PROOF STEP]
apply (rule mdl2mdl_wf)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. sat (mdl2mdl phi) i = rvsat phi i
[PROOF STEP]
apply (rule mdl2mdl_equivalent)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma rvmatch_embed':
  assumes "\<And>phi i. phi \<in> atms r \<Longrightarrow> rvsat (mdl2mdl' phi) i \<longleftrightarrow> sat phi i"
  shows "rvmatch (embed' mdl2mdl' r) = match r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rvmatch (embed' mdl2mdl' r) = match r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
?phi \<in> atms r \<Longrightarrow> rvsat (mdl2mdl' ?phi) ?i = sat ?phi ?i

goal (1 subgoal):
 1. rvmatch (embed' mdl2mdl' r) = match r
[PROOF STEP]
by (induction r) auto


[STATEMENT]
lemma mdl2mdlstar:
  fixes phi :: "('a, 't :: timestamp) formula"
  assumes "wf_fmla phi"
  shows "\<And>i. rvsat (mdl2mdl' phi) i \<longleftrightarrow> sat phi i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. rvsat (mdl2mdl' phi) i = sat phi i
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
wf_fmla phi

goal (1 subgoal):
 1. \<And>i. rvsat (mdl2mdl' phi) i = sat phi i
[PROOF STEP]
apply (induction phi rule: mdl2mdl'.induct)
[PROOF STATE]
proof (prove)
goal (10 subgoals):
 1. \<And>b i. wf_fmla (Bool b) \<Longrightarrow> rvsat (mdl2mdl' (Bool b)) i = sat (Bool b) i
 2. \<And>a i. wf_fmla (Atom a) \<Longrightarrow> rvsat (mdl2mdl' (Atom a)) i = sat (Atom a) i
 3. \<And>phi i. \<lbrakk>\<And>i. wf_fmla phi \<Longrightarrow> rvsat (mdl2mdl' phi) i = sat phi i; wf_fmla (Neg phi)\<rbrakk> \<Longrightarrow> rvsat (mdl2mdl' (Neg phi)) i = sat (Neg phi) i
 4. \<And>f phi psi i. \<lbrakk>\<And>i. wf_fmla phi \<Longrightarrow> rvsat (mdl2mdl' phi) i = sat phi i; \<And>i. wf_fmla psi \<Longrightarrow> rvsat (mdl2mdl' psi) i = sat psi i; wf_fmla (Bin f phi psi)\<rbrakk> \<Longrightarrow> rvsat (mdl2mdl' (Bin f phi psi)) i = sat (Bin f phi psi) i
 5. \<And>I phi i. \<lbrakk>\<And>i. wf_fmla phi \<Longrightarrow> rvsat (mdl2mdl' phi) i = sat phi i; wf_fmla (Prev I phi)\<rbrakk> \<Longrightarrow> rvsat (mdl2mdl' (Prev I phi)) i = sat (Prev I phi) i
 6. \<And>I phi i. \<lbrakk>\<And>i. wf_fmla phi \<Longrightarrow> rvsat (mdl2mdl' phi) i = sat phi i; wf_fmla (Next I phi)\<rbrakk> \<Longrightarrow> rvsat (mdl2mdl' (Next I phi)) i = sat (Next I phi) i
 7. \<And>phi I psi i. \<lbrakk>\<And>i. wf_fmla phi \<Longrightarrow> rvsat (mdl2mdl' phi) i = sat phi i; \<And>i. wf_fmla psi \<Longrightarrow> rvsat (mdl2mdl' psi) i = sat psi i; wf_fmla (Since phi I psi)\<rbrakk> \<Longrightarrow> rvsat (mdl2mdl' (Since phi I psi)) i = sat (Since phi I psi) i
 8. \<And>phi I psi i. \<lbrakk>\<And>i. wf_fmla phi \<Longrightarrow> rvsat (mdl2mdl' phi) i = sat phi i; \<And>i. wf_fmla psi \<Longrightarrow> rvsat (mdl2mdl' psi) i = sat psi i; wf_fmla (Until phi I psi)\<rbrakk> \<Longrightarrow> rvsat (mdl2mdl' (Until phi I psi)) i = sat (Until phi I psi) i
 9. \<And>I r i. \<lbrakk>\<And>phi i. \<lbrakk>phi \<in> atms (rderive r); wf_fmla phi\<rbrakk> \<Longrightarrow> rvsat (mdl2mdl' phi) i = sat phi i; wf_fmla (MatchP I r)\<rbrakk> \<Longrightarrow> rvsat (mdl2mdl' (MatchP I r)) i = sat (MatchP I r) i
 10. \<And>I r i. \<lbrakk>\<And>phi i. \<lbrakk>phi \<in> atms (rderive r); wf_fmla phi\<rbrakk> \<Longrightarrow> rvsat (mdl2mdl' phi) i = sat phi i; wf_fmla (MatchF I r)\<rbrakk> \<Longrightarrow> rvsat (mdl2mdl' (MatchF I r)) i = sat (MatchF I r) i
[PROOF STEP]
apply (auto split: nat.splits)[8]
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>I r i. \<lbrakk>\<And>phi i. \<lbrakk>phi \<in> atms (rderive r); wf_fmla phi\<rbrakk> \<Longrightarrow> rvsat (mdl2mdl' phi) i = sat phi i; wf_fmla (MatchP I r)\<rbrakk> \<Longrightarrow> rvsat (mdl2mdl' (MatchP I r)) i = sat (MatchP I r) i
 2. \<And>I r i. \<lbrakk>\<And>phi i. \<lbrakk>phi \<in> atms (rderive r); wf_fmla phi\<rbrakk> \<Longrightarrow> rvsat (mdl2mdl' phi) i = sat phi i; wf_fmla (MatchF I r)\<rbrakk> \<Longrightarrow> rvsat (mdl2mdl' (MatchF I r)) i = sat (MatchF I r) i
[PROOF STEP]
subgoal for I r i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>phi i. \<lbrakk>phi \<in> atms (rderive r); wf_fmla phi\<rbrakk> \<Longrightarrow> rvsat (mdl2mdl' phi) i = sat phi i; wf_fmla (MatchP I r)\<rbrakk> \<Longrightarrow> rvsat (mdl2mdl' (MatchP I r)) i = sat (MatchP I r) i
[PROOF STEP]
by auto (metis atms_rderive match_rderive rvmatch_embed' wf_fmla.simps(1))+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>I r i. \<lbrakk>\<And>phi i. \<lbrakk>phi \<in> atms (rderive r); wf_fmla phi\<rbrakk> \<Longrightarrow> rvsat (mdl2mdl' phi) i = sat phi i; wf_fmla (MatchF I r)\<rbrakk> \<Longrightarrow> rvsat (mdl2mdl' (MatchF I r)) i = sat (MatchF I r) i
[PROOF STEP]
subgoal for I r i
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>phi i. \<lbrakk>phi \<in> atms (rderive r); wf_fmla phi\<rbrakk> \<Longrightarrow> rvsat (mdl2mdl' phi) i = sat phi i; wf_fmla (MatchF I r)\<rbrakk> \<Longrightarrow> rvsat (mdl2mdl' (MatchF I r)) i = sat (MatchF I r) i
[PROOF STEP]
by auto (metis atms_rderive match_rderive rvmatch_embed' wf_fmla.simps(1))+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma noteq_sym: "a =!!= b \<Longrightarrow> b =!!= a"
  and unequal [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a =!!= b \<Longrightarrow> b =!!= a) &&& (a \<noteq> a') = a =!!= a'
[PROOF STEP]
unfolding noteq_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array a \<noteq> addr_of_array b \<Longrightarrow> TYPEREP('b) \<noteq> TYPEREP('a) \<or> addr_of_array b \<noteq> addr_of_array a) &&& (a \<noteq> a') = (TYPEREP('a) \<noteq> TYPEREP('a) \<or> addr_of_array a \<noteq> addr_of_array a')
[PROOF STEP]
by auto


[STATEMENT]
lemma noteq_irrefl: "r =!!= r \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r =!!= r \<Longrightarrow> False
[PROOF STEP]
unfolding noteq_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. TYPEREP('a) \<noteq> TYPEREP('a) \<or> addr_of_array r \<noteq> addr_of_array r \<Longrightarrow> False
[PROOF STEP]
by auto


[STATEMENT]
lemma present_alloc_noteq: "present h a \<Longrightarrow> a =!!= fst (alloc xs h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. present h a \<Longrightarrow> a =!!= fst (alloc xs h)
[PROOF STEP]
by (simp add: present_def noteq_def alloc_def Let_def)


[STATEMENT]
lemma get_set_eq [simp]: "get (set r x h) r = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get (Array_Time.set r x h) r = x
[PROOF STEP]
by (simp add: get_def set_def o_def)


[STATEMENT]
lemma get_set_neq [simp]: "r =!!= s \<Longrightarrow> get (set s x h) r = get h r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r =!!= s \<Longrightarrow> get (Array_Time.set s x h) r = get h r
[PROOF STEP]
by (simp add: noteq_def get_def set_def)


[STATEMENT]
lemma set_same [simp]:
  "set r x (set r y h) = set r x h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array_Time.set r x (Array_Time.set r y h) = Array_Time.set r x h
[PROOF STEP]
by (simp add: set_def)


[STATEMENT]
lemma set_set_swap:
  "r =!!= r' \<Longrightarrow> set r x (set r' x' h) = set r' x' (set r x h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r =!!= r' \<Longrightarrow> Array_Time.set r x (Array_Time.set r' x' h) = Array_Time.set r' x' (Array_Time.set r x h)
[PROOF STEP]
by (simp add: Let_def fun_eq_iff noteq_def set_def)


[STATEMENT]
lemma get_update_eq [simp]:
  "get (update a i v h) a = (get h a) [i := v]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get (update a i v h) a = (get h a)[i := v]
[PROOF STEP]
by (simp add: update_def)


[STATEMENT]
lemma nth_update_neq [simp]:
  "a =!!= b \<Longrightarrow> get (update b j v h) a ! i = get h a ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a =!!= b \<Longrightarrow> get (update b j v h) a ! i = get h a ! i
[PROOF STEP]
by (simp add: update_def noteq_def)


[STATEMENT]
lemma get_update_elem_neqIndex [simp]:
  "i \<noteq> j \<Longrightarrow> get (update a j v h) a ! i = get h a ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<noteq> j \<Longrightarrow> get (update a j v h) a ! i = get h a ! i
[PROOF STEP]
by simp


[STATEMENT]
lemma length_update [simp]:
  "length (update b i v h) = length h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array_Time.length (update b i v h) = Array_Time.length h
[PROOF STEP]
by (simp add: update_def length_def set_def get_def fun_eq_iff)


[STATEMENT]
lemma update_swap_neq:
  "a =!!= a' \<Longrightarrow>
  update a i v (update a' i' v' h)
  = update a' i' v' (update a i v h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a =!!= a' \<Longrightarrow> update a i v (update a' i' v' h) = update a' i' v' (update a i v h)
[PROOF STEP]
apply (unfold update_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a =!!= a' \<Longrightarrow> Array_Time.set a ((get (Array_Time.set a' ((get h a')[i' := v']) h) a)[i := v]) (Array_Time.set a' ((get h a')[i' := v']) h) = Array_Time.set a' ((get (Array_Time.set a ((get h a)[i := v]) h) a')[i' := v']) (Array_Time.set a ((get h a)[i := v]) h)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a =!!= a' \<Longrightarrow> Array_Time.set a ((get h a)[i := v]) (Array_Time.set a' ((get h a')[i' := v']) h) = Array_Time.set a' ((get (Array_Time.set a ((get h a)[i := v]) h) a')[i' := v']) (Array_Time.set a ((get h a)[i := v]) h)
[PROOF STEP]
apply (subst set_set_swap, assumption)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a =!!= a' \<Longrightarrow> Array_Time.set a' ((get h a')[i' := v']) (Array_Time.set a ((get h a)[i := v]) h) = Array_Time.set a' ((get (Array_Time.set a ((get h a)[i := v]) h) a')[i' := v']) (Array_Time.set a ((get h a)[i := v]) h)
[PROOF STEP]
apply (subst get_set_neq)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. a =!!= a' \<Longrightarrow> a' =!!= a
 2. a =!!= a' \<Longrightarrow> Array_Time.set a' ((get h a')[i' := v']) (Array_Time.set a ((get h a)[i := v]) h) = Array_Time.set a' ((get h a')[i' := v']) (Array_Time.set a ((get h a)[i := v]) h)
[PROOF STEP]
apply (erule noteq_sym)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a =!!= a' \<Longrightarrow> Array_Time.set a' ((get h a')[i' := v']) (Array_Time.set a ((get h a)[i := v]) h) = Array_Time.set a' ((get h a')[i' := v']) (Array_Time.set a ((get h a)[i := v]) h)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma update_swap_neqIndex:
  "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> update a i v (update a i' v' h) = update a i' v' (update a i v h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i \<noteq> i' \<Longrightarrow> update a i v (update a i' v' h) = update a i' v' (update a i v h)
[PROOF STEP]
by (auto simp add: update_def set_set_swap list_update_swap)


[STATEMENT]
lemma get_alloc:
  "get (snd (alloc xs h)) (fst (alloc ys h)) = xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get (snd (alloc xs h)) (fst (alloc ys h)) = xs
[PROOF STEP]
by (simp add: Let_def split_def alloc_def)


[STATEMENT]
lemma length_alloc:
  "length (snd (alloc (xs :: 'a::heap list) h)) (fst (alloc (ys :: 'a list) h)) = List.length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array_Time.length (snd (alloc xs h)) (fst (alloc ys h)) = List.length xs
[PROOF STEP]
by (simp add: Array_Time.length_def get_alloc)


[STATEMENT]
lemma set:
  "set (fst (alloc ls h))
     new_ls (snd (alloc ls h))
       = snd (alloc new_ls h)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Array_Time.set (fst (alloc ls h)) new_ls (snd (alloc ls h)) = snd (alloc new_ls h)
[PROOF STEP]
by (simp add: Let_def split_def alloc_def)


[STATEMENT]
lemma present_update [simp]:
  "present (update b i v h) = present h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. present (update b i v h) = present h
[PROOF STEP]
by (simp add: update_def present_def set_def get_def fun_eq_iff)


[STATEMENT]
lemma present_alloc [simp]:
  "present (snd (alloc xs h)) (fst (alloc xs h))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. present (snd (alloc xs h)) (fst (alloc xs h))
[PROOF STEP]
by (simp add: present_def alloc_def set_def Let_def)


[STATEMENT]
lemma not_present_alloc [simp]:
  "\<not> present h (fst (alloc xs h))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> present h (fst (alloc xs h))
[PROOF STEP]
by (simp add: present_def alloc_def Let_def)


[STATEMENT]
lemma execute_new [execute_simps]:
  "execute (new n x) h = Some (let (r,h') = alloc (replicate n x) h in (r,h',n+1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execute (new n x) h = Some (let (r, h') = alloc (replicate n x) h in (r, h', n + 1))
[PROOF STEP]
by (simp add: new_def execute_simps)


[STATEMENT]
lemma success_newI [success_intros]:
  "success (new n x) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. success (new n x) h
[PROOF STEP]
by (auto intro: success_intros simp add: new_def)


[STATEMENT]
lemma effect_newI [effect_intros]:
  assumes "(a, h') = alloc (replicate n x) h"
  shows "effect (new n x) h h' a (n+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. effect (new n x) h h' a (n + 1)
[PROOF STEP]
apply (rule effectI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execute (new n x) h = Some (a, h', n + 1)
[PROOF STEP]
apply (simp add: assms execute_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case alloc (replicate n x) h of (r, h') \<Rightarrow> (r, h', Suc n)) = (a, h', Suc n)
[PROOF STEP]
by (metis assms case_prod_conv)


[STATEMENT]
lemma effect_newE [effect_elims]:
  assumes "effect (new n x) h h' r n'"
  obtains "r = fst (alloc (replicate n x) h)" "h' = snd (alloc (replicate n x) h)"
    "get h' r = replicate n x" "present h' r" "\<not> present h r" "n+1=n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>r = fst (alloc (replicate n x) h); h' = snd (alloc (replicate n x) h); get h' r = replicate n x; present h' r; \<not> present h r; n + 1 = n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect (new n x) h h' r n'

goal (1 subgoal):
 1. (\<lbrakk>r = fst (alloc (replicate n x) h); h' = snd (alloc (replicate n x) h); get h' r = replicate n x; present h' r; \<not> present h r; n + 1 = n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (rule effectE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>r = fst (alloc (replicate n x) h); h' = snd (alloc (replicate n x) h); get h' r = replicate n x; present h' r; \<not> present h r; n + 1 = n'\<rbrakk> \<Longrightarrow> thesis; r = fst (the (execute (new n x) h)); h' = fst (snd (the (execute (new n x) h))); n' = snd (snd (the (execute (new n x) h))); success (new n x) h\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using  case_prod_beta get_alloc execute_new
[PROOF STATE]
proof (prove)
using this:
(case ?p of (x, xa) \<Rightarrow> ?f x xa) = ?f (fst ?p) (snd ?p)
get (snd (alloc ?xs ?h)) (fst (alloc ?ys ?h)) = ?xs
execute (new ?n ?x) ?h = Some (let (r, h') = alloc (replicate ?n ?x) ?h in (r, h', ?n + 1))

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>r = fst (alloc (replicate n x) h); h' = snd (alloc (replicate n x) h); get h' r = replicate n x; present h' r; \<not> present h r; n + 1 = n'\<rbrakk> \<Longrightarrow> thesis; r = fst (the (execute (new n x) h)); h' = fst (snd (the (execute (new n x) h))); n' = snd (snd (the (execute (new n x) h))); success (new n x) h\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (metis (mono_tags, lifting) fst_conv not_present_alloc option.sel present_alloc sndI)


[STATEMENT]
lemma execute_of_list [execute_simps]:
  "execute (of_list xs) h = Some (let (r,h') = alloc xs h in (r,h',1 + List.length xs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execute (of_list xs) h = Some (let (r, h') = alloc xs h in (r, h', 1 + List.length xs))
[PROOF STEP]
by (simp add: of_list_def execute_simps)


[STATEMENT]
lemma success_of_listI [success_intros]:
  "success (of_list xs) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. success (of_list xs) h
[PROOF STEP]
by (auto intro: success_intros simp add: of_list_def)


[STATEMENT]
lemma effect_of_listI [effect_intros]:
  assumes "(a, h') = alloc xs h"
  shows "effect (of_list xs) h h' a (1 + List.length xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. effect (of_list xs) h h' a (1 + List.length xs)
[PROOF STEP]
by (rule effectI, simp add: assms execute_simps, metis assms case_prod_conv)


[STATEMENT]
lemma effect_of_listE [effect_elims]:
  assumes "effect (of_list xs) h h' r n'"
  obtains "r = fst (alloc xs h)" "h' = snd (alloc xs h)"
    "get h' r = xs" "present h' r" "\<not> present h r" "n' = 1 + List.length xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>r = fst (alloc xs h); h' = snd (alloc xs h); get h' r = xs; present h' r; \<not> present h r; n' = 1 + List.length xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect (of_list xs) h h' r n'

goal (1 subgoal):
 1. (\<lbrakk>r = fst (alloc xs h); h' = snd (alloc xs h); get h' r = xs; present h' r; \<not> present h r; n' = 1 + List.length xs\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (rule effectE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>r = fst (alloc xs h); h' = snd (alloc xs h); get h' r = xs; present h' r; \<not> present h r; n' = 1 + List.length xs\<rbrakk> \<Longrightarrow> thesis; r = fst (the (execute (of_list xs) h)); h' = fst (snd (the (execute (of_list xs) h))); n' = snd (snd (the (execute (of_list xs) h))); success (of_list xs) h\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
apply (simp add: get_alloc  execute_of_list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>fst (case alloc xs h of (r, h') \<Rightarrow> (r, h', Suc (List.length xs))) = fst (alloc xs h); fst (snd (case alloc xs h of (r, h') \<Rightarrow> (r, h', Suc (List.length xs)))) = snd (alloc xs h); snd (snd (case alloc xs h of (r, h') \<Rightarrow> (r, h', Suc (List.length xs)))) = Suc (List.length xs)\<rbrakk> \<Longrightarrow> thesis; r = fst (case alloc xs h of (r, h') \<Rightarrow> (r, h', Suc (List.length xs))); h' = fst (snd (case alloc xs h of (r, h') \<Rightarrow> (r, h', Suc (List.length xs)))); n' = snd (snd (case alloc xs h of (r, h') \<Rightarrow> (r, h', Suc (List.length xs)))); success (of_list xs) h\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (simp add: case_prod_unfold)


[STATEMENT]
lemma execute_make [execute_simps]:
  "execute (make n f) h = Some (let (r,h') = alloc (map f [0 ..< n]) h in (r,h',n+1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execute (Array_Time.make n f) h = Some (let (r, h') = alloc (map f [0..<n]) h in (r, h', n + 1))
[PROOF STEP]
by (simp add: make_def execute_simps)


[STATEMENT]
lemma success_makeI [success_intros]:
  "success (make n f) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. success (Array_Time.make n f) h
[PROOF STEP]
by (auto intro: success_intros simp add: make_def)


[STATEMENT]
lemma effect_makeI [effect_intros]:
  assumes "(a, h') = alloc (map f [0 ..< n]) h"
  shows "effect (make n f) h h' a (n+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. effect (Array_Time.make n f) h h' a (n + 1)
[PROOF STEP]
by (rule effectI) (simp add: assms execute_simps, metis assms case_prod_conv)


[STATEMENT]
lemma effect_makeE [effect_elims]:
  assumes "effect (make n f) h h' r n'"
  obtains "r = fst (alloc (map f [0 ..< n]) h)" "h' = snd (alloc (map f [0 ..< n]) h)"
    "get h' r = map f [0 ..< n]" "present h' r" "\<not> present h r" "n+1=n'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>r = fst (alloc (map f [0..<n]) h); h' = snd (alloc (map f [0..<n]) h); get h' r = map f [0..<n]; present h' r; \<not> present h r; n + 1 = n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect (Array_Time.make n f) h h' r n'

goal (1 subgoal):
 1. (\<lbrakk>r = fst (alloc (map f [0..<n]) h); h' = snd (alloc (map f [0..<n]) h); get h' r = map f [0..<n]; present h' r; \<not> present h r; n + 1 = n'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
apply (rule effectE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>r = fst (alloc (map f [0..<n]) h); h' = snd (alloc (map f [0..<n]) h); get h' r = map f [0..<n]; present h' r; \<not> present h r; n + 1 = n'\<rbrakk> \<Longrightarrow> thesis; r = fst (the (execute (Array_Time.make n f) h)); h' = fst (snd (the (execute (Array_Time.make n f) h))); n' = snd (snd (the (execute (Array_Time.make n f) h))); success (Array_Time.make n f) h\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using get_alloc
[PROOF STATE]
proof (prove)
using this:
get (snd (alloc ?xs ?h)) (fst (alloc ?ys ?h)) = ?xs

goal (1 subgoal):
 1. \<lbrakk>\<lbrakk>r = fst (alloc (map f [0..<n]) h); h' = snd (alloc (map f [0..<n]) h); get h' r = map f [0..<n]; present h' r; \<not> present h r; n + 1 = n'\<rbrakk> \<Longrightarrow> thesis; r = fst (the (execute (Array_Time.make n f) h)); h' = fst (snd (the (execute (Array_Time.make n f) h))); n' = snd (snd (the (execute (Array_Time.make n f) h))); success (Array_Time.make n f) h\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by (metis (mono_tags, opaque_lifting) effectE effect_makeI not_present_alloc present_alloc prod.collapse)


[STATEMENT]
lemma execute_len [execute_simps]:
  "execute (len a) h = Some (length h a, h, 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. execute (len a) h = Some (Array_Time.length h a, h, 1)
[PROOF STEP]
by (simp add: len_def execute_simps)


[STATEMENT]
lemma success_lenI [success_intros]:
  "success (len a) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. success (len a) h
[PROOF STEP]
by (auto intro: success_intros simp add: len_def)


[STATEMENT]
lemma effect_lengthI [effect_intros]:
  assumes "h' = h" "r = length h a" "n=1"
  shows "effect (len a) h h' r n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. effect (len a) h h' r n
[PROOF STEP]
by (rule effectI) (simp add: assms execute_simps)


[STATEMENT]
lemma effect_lengthE [effect_elims]:
  assumes "effect (len a) h h' r n"
  obtains "r = length h' a" "h' = h" "n=1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>r = Array_Time.length h' a; h' = h; n = 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect (len a) h h' r n

goal (1 subgoal):
 1. (\<lbrakk>r = Array_Time.length h' a; h' = h; n = 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule effectE) (simp add: execute_simps)


[STATEMENT]
lemma execute_nth [execute_simps]:
  "i < length h a \<Longrightarrow>
    execute (nth a i) h = Some (get h a ! i, h,1)"
  "i \<ge> length h a \<Longrightarrow> execute (nth a i) h = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i < Array_Time.length h a \<Longrightarrow> execute (Array_Time.nth a i) h = Some (get h a ! i, h, 1)) &&& (Array_Time.length h a \<le> i \<Longrightarrow> execute (Array_Time.nth a i) h = None)
[PROOF STEP]
by (simp_all add: nth_def execute_simps)


[STATEMENT]
lemma success_nthI [success_intros]:
  "i < length h a \<Longrightarrow> success (nth a i) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < Array_Time.length h a \<Longrightarrow> success (Array_Time.nth a i) h
[PROOF STEP]
by (auto intro: success_intros simp add: nth_def)


[STATEMENT]
lemma effect_nthI [effect_intros]:
  assumes "i < length h a" "h' = h" "r = get h a ! i" "n=1"
  shows "effect (nth a i) h h' r n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. effect (Array_Time.nth a i) h h' r n
[PROOF STEP]
by (rule effectI) (insert assms, simp add: execute_simps)


[STATEMENT]
lemma effect_nthE [effect_elims]:
  assumes "effect (nth a i) h h' r n"
  obtains "i < length h a" "r = get h a ! i" "h' = h" "n=1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>i < Array_Time.length h a; r = get h a ! i; h' = h; n = 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect (Array_Time.nth a i) h h' r n

goal (1 subgoal):
 1. (\<lbrakk>i < Array_Time.length h a; r = get h a ! i; h' = h; n = 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE)


[STATEMENT]
lemma execute_upd [execute_simps]:
  "i < length h a \<Longrightarrow>
    execute (upd i x a) h = Some (a, update a i x h, 1)"
  "i \<ge> length h a \<Longrightarrow> execute (upd i x a) h = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i < Array_Time.length h a \<Longrightarrow> execute (upd i x a) h = Some (a, update a i x h, 1)) &&& (Array_Time.length h a \<le> i \<Longrightarrow> execute (upd i x a) h = None)
[PROOF STEP]
by (simp_all add: upd_def execute_simps)


[STATEMENT]
lemma success_updI [success_intros]:
  "i < length h a \<Longrightarrow> success (upd i x a) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < Array_Time.length h a \<Longrightarrow> success (upd i x a) h
[PROOF STEP]
by (auto intro: success_intros simp add: upd_def)


[STATEMENT]
lemma effect_updI [effect_intros]:
  assumes "i < length h a" "h' = update a i v h" "n=1"
  shows "effect (upd i v a) h h' a n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. effect (upd i v a) h h' a n
[PROOF STEP]
by (rule effectI) (insert assms, simp add: execute_simps)


[STATEMENT]
lemma effect_updE [effect_elims]:
  assumes "effect (upd i v a) h h' r n"
  obtains "r = a" "h' = update a i v h" "i < length h a" "n=1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>r = a; h' = update a i v h; i < Array_Time.length h a; n = 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect (upd i v a) h h' r n

goal (1 subgoal):
 1. (\<lbrakk>r = a; h' = update a i v h; i < Array_Time.length h a; n = 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE)


[STATEMENT]
lemma execute_map_entry [execute_simps]:
  "i < length h a \<Longrightarrow>
   execute (map_entry i f a) h =
      Some (a, update a i (f (get h a ! i)) h, 2)"
  "i \<ge> length h a \<Longrightarrow> execute (map_entry i f a) h = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i < Array_Time.length h a \<Longrightarrow> execute (map_entry i f a) h = Some (a, update a i (f (get h a ! i)) h, 2)) &&& (Array_Time.length h a \<le> i \<Longrightarrow> execute (map_entry i f a) h = None)
[PROOF STEP]
by (simp_all add: map_entry_def execute_simps)


[STATEMENT]
lemma success_map_entryI [success_intros]:
  "i < length h a \<Longrightarrow> success (map_entry i f a) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < Array_Time.length h a \<Longrightarrow> success (map_entry i f a) h
[PROOF STEP]
by (auto intro: success_intros simp add: map_entry_def)


[STATEMENT]
lemma effect_map_entryI [effect_intros]:
  assumes "i < length h a" "h' = update a i (f (get h a ! i)) h" "r = a" "n=2"
  shows "effect (map_entry i f a) h h' r n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. effect (map_entry i f a) h h' r n
[PROOF STEP]
by (rule effectI) (insert assms, simp add: execute_simps)


[STATEMENT]
lemma effect_map_entryE [effect_elims]:
  assumes "effect (map_entry i f a) h h' r n"
  obtains "r = a" "h' = update a i (f (get h a ! i)) h" "i < length h a" "n=2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>r = a; h' = update a i (f (get h a ! i)) h; i < Array_Time.length h a; n = 2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
effect (map_entry i f a) h h' r n

goal (1 subgoal):
 1. (\<lbrakk>r = a; h' = update a i (f (get h a ! i)) h; i < Array_Time.length h a; n = 2\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule effectE) (cases "i < length h a", auto simp: execute_simps elim: successE)


[STATEMENT]
lemma execute_swap [execute_simps]:
  "i < length h a \<Longrightarrow>
   execute (swap i x a) h =
      Some (get h a ! i, update a i x h, 2)"
  "i \<ge> length h a \<Longrightarrow> execute (swap i x a) h = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (i < Array_Time.length h a \<Longrightarrow> execute (swap i x a) h = Some (get h a ! i, update a i x h, 2)) &&& (Array_Time.length h a \<le> i \<Longrightarrow> execute (swap i x a) h = None)
[PROOF STEP]
by (simp_all add: swap_def execute_simps)


[STATEMENT]
lemma success_swapI [success_intros]:
  "i < length h a \<Longrightarrow> success (swap i x a) h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < Array_Time.length h a \<Longrightarrow> success (swap i x a) h
[PROOF STEP]
by (auto intro: success_intros simp add: swap_def)


[STATEMENT]
lemma effect_swapI [effect_intros]:
  assumes "i < length h a" "h' = update a i x h" "r = get h a ! i" "n=2"
  shows "effect (swap i x a) h h' r n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. effect (swap i x a) h h' r n
[PROOF STEP]
by (rule effectI) (insert assms, simp add: execute_simps)