[STATEMENT]
lemma (in constants) veval'_shadows:
  assumes "\<Gamma> \<turnstile>\<^sub>v t \<down> v" "not_shadows_vconsts_env \<Gamma>" "\<not> shadows_consts t"
  shows "not_shadows_vconsts v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_shadows_vconsts v
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v t \<down> v
not_shadows_vconsts_env \<Gamma>
\<not> shadows_consts t

goal (1 subgoal):
 1. not_shadows_vconsts v
[PROOF STEP]
proof induction
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sconst name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Svar name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 3. \<And>\<Gamma> cs. \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sabs cs)\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t cs \<Gamma>' u u' env uu_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vabs cs \<Gamma>'; \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts t\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vabs cs \<Gamma>'); \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts u\<rbrakk> \<Longrightarrow> not_shadows_vconsts u'; vfind_match cs u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>not_shadows_vconsts_env (\<Gamma>' ++\<^sub>f env); \<not> shadows_consts rhs\<rbrakk> \<Longrightarrow> not_shadows_vconsts val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (t $\<^sub>s u)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 5. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts t\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts u\<rbrakk> \<Longrightarrow> not_shadows_vconsts u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>not_shadows_vconsts_env (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); \<not> shadows_consts rhs\<rbrakk> \<Longrightarrow> not_shadows_vconsts val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (t $\<^sub>s u)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 6. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (not_shadows_vconsts_env \<Gamma> \<longrightarrow> \<not> shadows_consts x1 \<longrightarrow> not_shadows_vconsts x2)) ts us; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (name $$ ts)\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vconstr name us)
[PROOF STEP]
case comb
[PROOF STATE]
proof (state)
this:
\<Gamma>_ \<turnstile>\<^sub>v t_ \<down> Vabs cs_ \<Gamma>'_
\<Gamma>_ \<turnstile>\<^sub>v u_ \<down> u'_
vfind_match cs_ u'_ = Some (env_, uu_, rhs_)
\<Gamma>'_ ++\<^sub>f env_ \<turnstile>\<^sub>v rhs_ \<down> val_
\<lbrakk>not_shadows_vconsts_env \<Gamma>_; \<not> shadows_consts t_\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vabs cs_ \<Gamma>'_)
\<lbrakk>not_shadows_vconsts_env \<Gamma>_; \<not> shadows_consts u_\<rbrakk> \<Longrightarrow> not_shadows_vconsts u'_
\<lbrakk>not_shadows_vconsts_env (\<Gamma>'_ ++\<^sub>f env_); \<not> shadows_consts rhs_\<rbrakk> \<Longrightarrow> not_shadows_vconsts val_
not_shadows_vconsts_env \<Gamma>_
\<not> shadows_consts (t_ $\<^sub>s u_)

goal (6 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sconst name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Svar name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 3. \<And>\<Gamma> cs. \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sabs cs)\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t cs \<Gamma>' u u' env uu_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vabs cs \<Gamma>'; \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts t\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vabs cs \<Gamma>'); \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts u\<rbrakk> \<Longrightarrow> not_shadows_vconsts u'; vfind_match cs u' = Some (env, uu_, rhs); \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>not_shadows_vconsts_env (\<Gamma>' ++\<^sub>f env); \<not> shadows_consts rhs\<rbrakk> \<Longrightarrow> not_shadows_vconsts val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (t $\<^sub>s u)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 5. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts t\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts u\<rbrakk> \<Longrightarrow> not_shadows_vconsts u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>not_shadows_vconsts_env (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); \<not> shadows_consts rhs\<rbrakk> \<Longrightarrow> not_shadows_vconsts val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (t $\<^sub>s u)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 6. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (not_shadows_vconsts_env \<Gamma> \<longrightarrow> \<not> shadows_consts x1 \<longrightarrow> not_shadows_vconsts x2)) ts us; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (name $$ ts)\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vconstr name us)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_shadows_vconsts val_
[PROOF STEP]
apply (rule comb)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. not_shadows_vconsts_env (\<Gamma>'_ ++\<^sub>f env_)
 2. \<not> shadows_consts rhs_
[PROOF STEP]
using comb
[PROOF STATE]
proof (prove)
using this:
\<Gamma>_ \<turnstile>\<^sub>v t_ \<down> Vabs cs_ \<Gamma>'_
\<Gamma>_ \<turnstile>\<^sub>v u_ \<down> u'_
vfind_match cs_ u'_ = Some (env_, uu_, rhs_)
\<Gamma>'_ ++\<^sub>f env_ \<turnstile>\<^sub>v rhs_ \<down> val_
\<lbrakk>not_shadows_vconsts_env \<Gamma>_; \<not> shadows_consts t_\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vabs cs_ \<Gamma>'_)
\<lbrakk>not_shadows_vconsts_env \<Gamma>_; \<not> shadows_consts u_\<rbrakk> \<Longrightarrow> not_shadows_vconsts u'_
\<lbrakk>not_shadows_vconsts_env (\<Gamma>'_ ++\<^sub>f env_); \<not> shadows_consts rhs_\<rbrakk> \<Longrightarrow> not_shadows_vconsts val_
not_shadows_vconsts_env \<Gamma>_
\<not> shadows_consts (t_ $\<^sub>s u_)

goal (2 subgoals):
 1. not_shadows_vconsts_env (\<Gamma>'_ ++\<^sub>f env_)
 2. \<not> shadows_consts rhs_
[PROOF STEP]
by (auto simp: list_all_iff dest: vfind_match_elem intro: not_shadows_vconsts.vmatch_env)
[PROOF STATE]
proof (state)
this:
not_shadows_vconsts val_

goal (5 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sconst name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Svar name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 3. \<And>\<Gamma> cs. \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sabs cs)\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts t\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts u\<rbrakk> \<Longrightarrow> not_shadows_vconsts u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>not_shadows_vconsts_env (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); \<not> shadows_consts rhs\<rbrakk> \<Longrightarrow> not_shadows_vconsts val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (t $\<^sub>s u)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 5. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (not_shadows_vconsts_env \<Gamma> \<longrightarrow> \<not> shadows_consts x1 \<longrightarrow> not_shadows_vconsts x2)) ts us; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (name $$ ts)\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vconstr name us)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sconst name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Svar name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 3. \<And>\<Gamma> cs. \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sabs cs)\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts t\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts u\<rbrakk> \<Longrightarrow> not_shadows_vconsts u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>not_shadows_vconsts_env (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); \<not> shadows_consts rhs\<rbrakk> \<Longrightarrow> not_shadows_vconsts val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (t $\<^sub>s u)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 5. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (not_shadows_vconsts_env \<Gamma> \<longrightarrow> \<not> shadows_consts x1 \<longrightarrow> not_shadows_vconsts x2)) ts us; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (name $$ ts)\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vconstr name us)
[PROOF STEP]
case (rec_comb \<Gamma> t css name \<Gamma>' cs u u' env pat rhs val)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'
fmlookup css name = Some cs
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts t\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vrecabs css name \<Gamma>')
\<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts u\<rbrakk> \<Longrightarrow> not_shadows_vconsts u'
\<lbrakk>not_shadows_vconsts_env (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); \<not> shadows_consts rhs\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
not_shadows_vconsts_env \<Gamma>
\<not> shadows_consts (t $\<^sub>s u)

goal (5 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sconst name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Svar name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 3. \<And>\<Gamma> cs. \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sabs cs)\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts t\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts u\<rbrakk> \<Longrightarrow> not_shadows_vconsts u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>not_shadows_vconsts_env (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); \<not> shadows_consts rhs\<rbrakk> \<Longrightarrow> not_shadows_vconsts val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (t $\<^sub>s u)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 5. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (not_shadows_vconsts_env \<Gamma> \<longrightarrow> \<not> shadows_consts x1 \<longrightarrow> not_shadows_vconsts x2)) ts us; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (name $$ ts)\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vconstr name us)
[PROOF STEP]
have "(pat, rhs) \<in> set cs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (pat, rhs) \<in> set cs
[PROOF STEP]
by (rule vfind_match_elem) fact
[PROOF STATE]
proof (state)
this:
(pat, rhs) \<in> set cs

goal (5 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sconst name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Svar name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 3. \<And>\<Gamma> cs. \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sabs cs)\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vabs cs \<Gamma>)
 4. \<And>\<Gamma> t css name \<Gamma>' cs u u' env uv_ rhs val. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'; \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts t\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vrecabs css name \<Gamma>'); fmlookup css name = Some cs; \<Gamma> \<turnstile>\<^sub>v u \<down> u'; \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts u\<rbrakk> \<Longrightarrow> not_shadows_vconsts u'; vfind_match cs u' = Some (env, uv_, rhs); \<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val; \<lbrakk>not_shadows_vconsts_env (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); \<not> shadows_consts rhs\<rbrakk> \<Longrightarrow> not_shadows_vconsts val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (t $\<^sub>s u)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 5. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (not_shadows_vconsts_env \<Gamma> \<longrightarrow> \<not> shadows_consts x1 \<longrightarrow> not_shadows_vconsts x2)) ts us; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (name $$ ts)\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vconstr name us)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_shadows_vconsts val
[PROOF STEP]
proof (rule rec_comb)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. not_shadows_vconsts_env (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)
 2. \<not> shadows_consts rhs
[PROOF STEP]
show "not_shadows_vconsts_env (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_shadows_vconsts_env (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)
[PROOF STEP]
proof (intro fmpred_add)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. not_shadows_vconsts_env \<Gamma>'
 2. not_shadows_vconsts_env (mk_rec_env css \<Gamma>')
 3. not_shadows_vconsts_env env
[PROOF STEP]
show "not_shadows_vconsts_env env"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_shadows_vconsts_env env
[PROOF STEP]
using rec_comb
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'
fmlookup css name = Some cs
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts t\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vrecabs css name \<Gamma>')
\<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts u\<rbrakk> \<Longrightarrow> not_shadows_vconsts u'
\<lbrakk>not_shadows_vconsts_env (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); \<not> shadows_consts rhs\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
not_shadows_vconsts_env \<Gamma>
\<not> shadows_consts (t $\<^sub>s u)

goal (1 subgoal):
 1. not_shadows_vconsts_env env
[PROOF STEP]
by (auto dest: vfind_match_elem intro: not_shadows_vconsts.vmatch_env)
[PROOF STATE]
proof (state)
this:
not_shadows_vconsts_env env

goal (2 subgoals):
 1. not_shadows_vconsts_env \<Gamma>'
 2. not_shadows_vconsts_env (mk_rec_env css \<Gamma>')
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. not_shadows_vconsts_env \<Gamma>'
 2. not_shadows_vconsts_env (mk_rec_env css \<Gamma>')
[PROOF STEP]
show "not_shadows_vconsts_env (mk_rec_env css \<Gamma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_shadows_vconsts_env (mk_rec_env css \<Gamma>')
[PROOF STEP]
unfolding mk_rec_env_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_shadows_vconsts_env (fmmap_keys (\<lambda>name cs. Vrecabs css name \<Gamma>') css)
[PROOF STEP]
using rec_comb
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'
fmlookup css name = Some cs
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts t\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vrecabs css name \<Gamma>')
\<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts u\<rbrakk> \<Longrightarrow> not_shadows_vconsts u'
\<lbrakk>not_shadows_vconsts_env (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); \<not> shadows_consts rhs\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
not_shadows_vconsts_env \<Gamma>
\<not> shadows_consts (t $\<^sub>s u)

goal (1 subgoal):
 1. not_shadows_vconsts_env (fmmap_keys (\<lambda>name cs. Vrecabs css name \<Gamma>') css)
[PROOF STEP]
by (auto intro: fmdomI)
[PROOF STATE]
proof (state)
this:
not_shadows_vconsts_env (mk_rec_env css \<Gamma>')

goal (1 subgoal):
 1. not_shadows_vconsts_env \<Gamma>'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. not_shadows_vconsts_env \<Gamma>'
[PROOF STEP]
show "not_shadows_vconsts_env \<Gamma>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_shadows_vconsts_env \<Gamma>'
[PROOF STEP]
using rec_comb
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'
fmlookup css name = Some cs
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts t\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vrecabs css name \<Gamma>')
\<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts u\<rbrakk> \<Longrightarrow> not_shadows_vconsts u'
\<lbrakk>not_shadows_vconsts_env (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); \<not> shadows_consts rhs\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
not_shadows_vconsts_env \<Gamma>
\<not> shadows_consts (t $\<^sub>s u)

goal (1 subgoal):
 1. not_shadows_vconsts_env \<Gamma>'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
not_shadows_vconsts_env \<Gamma>'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
not_shadows_vconsts_env (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env)

goal (1 subgoal):
 1. \<not> shadows_consts rhs
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> shadows_consts rhs
[PROOF STEP]
have "not_shadows_vconsts (Vrecabs css name \<Gamma>')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. not_shadows_vconsts (Vrecabs css name \<Gamma>')
[PROOF STEP]
using rec_comb
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'
fmlookup css name = Some cs
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts t\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vrecabs css name \<Gamma>')
\<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts u\<rbrakk> \<Longrightarrow> not_shadows_vconsts u'
\<lbrakk>not_shadows_vconsts_env (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); \<not> shadows_consts rhs\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
not_shadows_vconsts_env \<Gamma>
\<not> shadows_consts (t $\<^sub>s u)

goal (1 subgoal):
 1. not_shadows_vconsts (Vrecabs css name \<Gamma>')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
not_shadows_vconsts (Vrecabs css name \<Gamma>')

goal (1 subgoal):
 1. \<not> shadows_consts rhs
[PROOF STEP]
thus "\<not> shadows_consts rhs"
[PROOF STATE]
proof (prove)
using this:
not_shadows_vconsts (Vrecabs css name \<Gamma>')

goal (1 subgoal):
 1. \<not> shadows_consts rhs
[PROOF STEP]
using \<open>(pat, rhs) \<in> set cs\<close> rec_comb
[PROOF STATE]
proof (prove)
using this:
not_shadows_vconsts (Vrecabs css name \<Gamma>')
(pat, rhs) \<in> set cs
\<Gamma> \<turnstile>\<^sub>v t \<down> Vrecabs css name \<Gamma>'
fmlookup css name = Some cs
\<Gamma> \<turnstile>\<^sub>v u \<down> u'
vfind_match cs u' = Some (env, pat, rhs)
\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env \<turnstile>\<^sub>v rhs \<down> val
\<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts t\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vrecabs css name \<Gamma>')
\<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts u\<rbrakk> \<Longrightarrow> not_shadows_vconsts u'
\<lbrakk>not_shadows_vconsts_env (\<Gamma>' ++\<^sub>f mk_rec_env css \<Gamma>' ++\<^sub>f env); \<not> shadows_consts rhs\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
not_shadows_vconsts_env \<Gamma>
\<not> shadows_consts (t $\<^sub>s u)

goal (1 subgoal):
 1. \<not> shadows_consts rhs
[PROOF STEP]
by (auto simp: list_all_iff)
[PROOF STATE]
proof (state)
this:
\<not> shadows_consts rhs

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
not_shadows_vconsts val

goal (4 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sconst name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Svar name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 3. \<And>\<Gamma> cs. \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sabs cs)\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vabs cs \<Gamma>)
 4. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (not_shadows_vconsts_env \<Gamma> \<longrightarrow> \<not> shadows_consts x1 \<longrightarrow> not_shadows_vconsts x2)) ts us; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (name $$ ts)\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vconstr name us)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sconst name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Svar name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 3. \<And>\<Gamma> cs. \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sabs cs)\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vabs cs \<Gamma>)
 4. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (not_shadows_vconsts_env \<Gamma> \<longrightarrow> \<not> shadows_consts x1 \<longrightarrow> not_shadows_vconsts x2)) ts us; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (name $$ ts)\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vconstr name us)
[PROOF STEP]
case (constr name \<Gamma> ts us)
[PROOF STATE]
proof (state)
this:
name |\<in>| C
list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (not_shadows_vconsts_env \<Gamma> \<longrightarrow> \<not> shadows_consts x1 \<longrightarrow> not_shadows_vconsts x2)) ts us
not_shadows_vconsts_env \<Gamma>
\<not> shadows_consts (name $$ ts)

goal (4 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sconst name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Svar name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 3. \<And>\<Gamma> cs. \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sabs cs)\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vabs cs \<Gamma>)
 4. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (not_shadows_vconsts_env \<Gamma> \<longrightarrow> \<not> shadows_consts x1 \<longrightarrow> not_shadows_vconsts x2)) ts us; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (name $$ ts)\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vconstr name us)
[PROOF STEP]
have "list_all (not_shadows_vconsts) us"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. list_all not_shadows_vconsts us
[PROOF STEP]
using \<open>list_all2 _ _ _\<close> \<open>\<not> shadows_consts (name $$ ts)\<close>
[PROOF STATE]
proof (prove)
using this:
list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (not_shadows_vconsts_env \<Gamma> \<longrightarrow> \<not> shadows_consts x1 \<longrightarrow> not_shadows_vconsts x2)) ts us
\<not> shadows_consts (name $$ ts)

goal (1 subgoal):
 1. list_all not_shadows_vconsts us
[PROOF STEP]
proof (induction ts us rule: list.rel_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<not> shadows_consts (name $$ []) \<Longrightarrow> list_all not_shadows_vconsts []
 2. \<And>a21 a22 b21 b22. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v a21 \<down> b21 \<and> (not_shadows_vconsts_env \<Gamma> \<longrightarrow> \<not> shadows_consts a21 \<longrightarrow> not_shadows_vconsts b21); \<not> shadows_consts (name $$ a22) \<Longrightarrow> list_all not_shadows_vconsts b22; \<not> shadows_consts (name $$ (a21 # a22))\<rbrakk> \<Longrightarrow> list_all not_shadows_vconsts (b21 # b22)
[PROOF STEP]
case (Cons v vs u us)
[PROOF STATE]
proof (state)
this:
\<Gamma> \<turnstile>\<^sub>v v \<down> u \<and> (not_shadows_vconsts_env \<Gamma> \<longrightarrow> \<not> shadows_consts v \<longrightarrow> not_shadows_vconsts u)
\<not> shadows_consts (name $$ vs) \<Longrightarrow> list_all not_shadows_vconsts us
\<not> shadows_consts (name $$ (v # vs))

goal (2 subgoals):
 1. \<not> shadows_consts (name $$ []) \<Longrightarrow> list_all not_shadows_vconsts []
 2. \<And>a21 a22 b21 b22. \<lbrakk>\<Gamma> \<turnstile>\<^sub>v a21 \<down> b21 \<and> (not_shadows_vconsts_env \<Gamma> \<longrightarrow> \<not> shadows_consts a21 \<longrightarrow> not_shadows_vconsts b21); \<not> shadows_consts (name $$ a22) \<Longrightarrow> list_all not_shadows_vconsts b22; \<not> shadows_consts (name $$ (a21 # a22))\<rbrakk> \<Longrightarrow> list_all not_shadows_vconsts (b21 # b22)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v v \<down> u \<and> (not_shadows_vconsts_env \<Gamma> \<longrightarrow> \<not> shadows_consts v \<longrightarrow> not_shadows_vconsts u)
\<not> shadows_consts (name $$ vs) \<Longrightarrow> list_all not_shadows_vconsts us
\<not> shadows_consts (name $$ (v # vs))

goal (1 subgoal):
 1. list_all not_shadows_vconsts (u # us)
[PROOF STEP]
using constr
[PROOF STATE]
proof (prove)
using this:
\<Gamma> \<turnstile>\<^sub>v v \<down> u \<and> (not_shadows_vconsts_env \<Gamma> \<longrightarrow> \<not> shadows_consts v \<longrightarrow> not_shadows_vconsts u)
\<not> shadows_consts (name $$ vs) \<Longrightarrow> list_all not_shadows_vconsts us
\<not> shadows_consts (name $$ (v # vs))
name |\<in>| C
list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (not_shadows_vconsts_env \<Gamma> \<longrightarrow> \<not> shadows_consts x1 \<longrightarrow> not_shadows_vconsts x2)) ts us__
not_shadows_vconsts_env \<Gamma>
\<not> shadows_consts (name $$ ts)

goal (1 subgoal):
 1. list_all not_shadows_vconsts (u # us)
[PROOF STEP]
by (auto simp: shadows.list_comb app_sterm_def)
[PROOF STATE]
proof (state)
this:
list_all not_shadows_vconsts (u # us)

goal (1 subgoal):
 1. \<not> shadows_consts (name $$ []) \<Longrightarrow> list_all not_shadows_vconsts []
[PROOF STEP]
qed simp
[PROOF STATE]
proof (state)
this:
list_all not_shadows_vconsts us

goal (4 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sconst name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Svar name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 3. \<And>\<Gamma> cs. \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sabs cs)\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vabs cs \<Gamma>)
 4. \<And>name \<Gamma> ts us. \<lbrakk>name |\<in>| C; list_all2 (\<lambda>x1 x2. \<Gamma> \<turnstile>\<^sub>v x1 \<down> x2 \<and> (not_shadows_vconsts_env \<Gamma> \<longrightarrow> \<not> shadows_consts x1 \<longrightarrow> not_shadows_vconsts x2)) ts us; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (name $$ ts)\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vconstr name us)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
list_all not_shadows_vconsts us

goal (1 subgoal):
 1. not_shadows_vconsts (Vconstr name us)
[PROOF STEP]
by (simp add: list_all_iff)
[PROOF STATE]
proof (state)
this:
not_shadows_vconsts (Vconstr name us)

goal (3 subgoals):
 1. \<And>name \<Gamma> val. \<lbrakk>name |\<notin>| C; fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sconst name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 2. \<And>\<Gamma> name val. \<lbrakk>fmlookup \<Gamma> name = Some val; not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Svar name)\<rbrakk> \<Longrightarrow> not_shadows_vconsts val
 3. \<And>\<Gamma> cs. \<lbrakk>not_shadows_vconsts_env \<Gamma>; \<not> shadows_consts (Sabs cs)\<rbrakk> \<Longrightarrow> not_shadows_vconsts (Vabs cs \<Gamma>)
[PROOF STEP]
qed (auto simp: list_all_iff list_ex_iff)