[STATEMENT]
lemma subst_v_eval_v[simp]:
  fixes v::v and v'::v
  assumes "i \<lbrakk> v \<rbrakk> ~  s" and "i \<lbrakk> (v'[x::=v]\<^sub>v\<^sub>v) \<rbrakk> ~ s'"
  shows "(i ( x \<mapsto> s )) \<lbrakk> v' \<rbrakk> ~ s'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> v' \<rbrakk> ~ s'
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> v'[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> v' \<rbrakk> ~ s'
[PROOF STEP]
proof(nominal_induct v' arbitrary: s' rule:v.strong_induct)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>xa s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ xa ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ s'
 2. \<And>xa s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ xa ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ s'
 3. \<And>x1a x2a s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x1a[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x1a \<rbrakk> ~ s' ; \<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x2a[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x2a \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s'
 4. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x3[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_cons x1a x2a x3)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 5. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x4[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_consp x1a x2a x3 x4)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
case (V_lit x)
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> [ x ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'

goal (5 subgoals):
 1. \<And>xa s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ xa ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ s'
 2. \<And>xa s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ xa ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ s'
 3. \<And>x1a x2a s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x1a[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x1a \<rbrakk> ~ s' ; \<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x2a[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x2a \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s'
 4. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x3[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_cons x1a x2a x3)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 5. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x4[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_consp x1a x2a x3 x4)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> [ x ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> [ x ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
using subst_vv.simps
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> [ x ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'
[ ?l ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>v = [ ?l ]\<^sup>v
[ ?y ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>v = (if ?x = ?y then ?v else [ ?y ]\<^sup>v)
(V_cons ?tyid ?c ?v')[?x::=?v]\<^sub>v\<^sub>v = V_cons ?tyid ?c ?v'[?x::=?v]\<^sub>v\<^sub>v
(V_consp ?tyid ?c ?b ?v')[?x::=?v]\<^sub>v\<^sub>v = V_consp ?tyid ?c ?b ?v'[?x::=?v]\<^sub>v\<^sub>v
[ ?v1.0 , ?v2.0 ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>v = [ ?v1.0[?x::=?v]\<^sub>v\<^sub>v , ?v2.0[?x::=?v]\<^sub>v\<^sub>v ]\<^sup>v

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
by (metis eval_v_elims(1) eval_v_litI)
[PROOF STATE]
proof (state)
this:
i(x \<mapsto> s) \<lbrakk> [ x ]\<^sup>v \<rbrakk> ~ s'

goal (4 subgoals):
 1. \<And>xa s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ xa ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ s'
 2. \<And>x1a x2a s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x1a[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x1a \<rbrakk> ~ s' ; \<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x2a[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x2a \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s'
 3. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x3[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_cons x1a x2a x3)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 4. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x4[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_consp x1a x2a x3 x4)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>xa s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ xa ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ s'
 2. \<And>x1a x2a s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x1a[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x1a \<rbrakk> ~ s' ; \<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x2a[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x2a \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s'
 3. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x3[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_cons x1a x2a x3)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 4. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x4[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_consp x1a x2a x3 x4)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
case (V_var x')
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> [ x' ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'

goal (4 subgoals):
 1. \<And>xa s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ xa ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ xa ]\<^sup>v \<rbrakk> ~ s'
 2. \<And>x1a x2a s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x1a[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x1a \<rbrakk> ~ s' ; \<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x2a[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x2a \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s'
 3. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x3[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_cons x1a x2a x3)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 4. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x4[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_consp x1a x2a x3 x4)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> [ x' ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> [ x' ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> [ x' ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
proof(cases "x=x'")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ x' ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' ; x = x'\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x' ]\<^sup>v \<rbrakk> ~ s'
 2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ x' ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' ; x \<noteq> x'\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x' ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
x = x'

goal (2 subgoals):
 1. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ x' ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' ; x = x'\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x' ]\<^sup>v \<rbrakk> ~ s'
 2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ x' ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' ; x \<noteq> x'\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x' ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
hence "(V_var x')[x::=v]\<^sub>v\<^sub>v = v"
[PROOF STATE]
proof (prove)
using this:
x = x'

goal (1 subgoal):
 1. [ x' ]\<^sup>v[x::=v]\<^sub>v\<^sub>v = v
[PROOF STEP]
using subst_vv.simps
[PROOF STATE]
proof (prove)
using this:
x = x'
[ ?l ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>v = [ ?l ]\<^sup>v
[ ?y ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>v = (if ?x = ?y then ?v else [ ?y ]\<^sup>v)
(V_cons ?tyid ?c ?v')[?x::=?v]\<^sub>v\<^sub>v = V_cons ?tyid ?c ?v'[?x::=?v]\<^sub>v\<^sub>v
(V_consp ?tyid ?c ?b ?v')[?x::=?v]\<^sub>v\<^sub>v = V_consp ?tyid ?c ?b ?v'[?x::=?v]\<^sub>v\<^sub>v
[ ?v1.0 , ?v2.0 ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>v = [ ?v1.0[?x::=?v]\<^sub>v\<^sub>v , ?v2.0[?x::=?v]\<^sub>v\<^sub>v ]\<^sup>v

goal (1 subgoal):
 1. [ x' ]\<^sup>v[x::=v]\<^sub>v\<^sub>v = v
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
[ x' ]\<^sup>v[x::=v]\<^sub>v\<^sub>v = v

goal (2 subgoals):
 1. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ x' ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' ; x = x'\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x' ]\<^sup>v \<rbrakk> ~ s'
 2. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ x' ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' ; x \<noteq> x'\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x' ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[ x' ]\<^sup>v[x::=v]\<^sub>v\<^sub>v = v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
[ x' ]\<^sup>v[x::=v]\<^sub>v\<^sub>v = v

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> [ x' ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
using V_var eval_v_elims eval_v_varI eval_v_uniqueness True
[PROOF STATE]
proof (prove)
using this:
[ x' ]\<^sup>v[x::=v]\<^sub>v\<^sub>v = v
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> [ x' ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
Some ?sv = ?i ?x \<Longrightarrow> ?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?sv
\<lbrakk>?i \<lbrakk> ?v \<rbrakk> ~ ?s ; ?i \<lbrakk> ?v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?s = ?s'
x = x'

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> [ x' ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
by (simp add: eval_v.eval_v_varI)
[PROOF STATE]
proof (state)
this:
i(x \<mapsto> s) \<lbrakk> [ x' ]\<^sup>v \<rbrakk> ~ s'

goal (1 subgoal):
 1. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ x' ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' ; x \<noteq> x'\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x' ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ x' ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' ; x \<noteq> x'\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x' ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
x \<noteq> x'

goal (1 subgoal):
 1. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ x' ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' ; x \<noteq> x'\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x' ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
hence "atom x \<sharp> (V_var x')"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> x'

goal (1 subgoal):
 1. atom x \<sharp> [ x' ]\<^sup>v
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
atom x \<sharp> [ x' ]\<^sup>v

goal (1 subgoal):
 1. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ x' ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' ; x \<noteq> x'\<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x' ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
atom x \<sharp> [ x' ]\<^sup>v
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> [ x' ]\<^sup>v

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> [ x' ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
using eval_v_i_upd False V_var
[PROOF STATE]
proof (prove)
using this:
atom x \<sharp> [ x' ]\<^sup>v
\<lbrakk>atom ?x \<sharp> ?v; ?i \<lbrakk> ?v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> ?i(?x \<mapsto> ?s) \<lbrakk> ?v \<rbrakk> ~ ?s'
x \<noteq> x'
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> [ x' ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> [ x' ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
i(x \<mapsto> s) \<lbrakk> [ x' ]\<^sup>v \<rbrakk> ~ s'

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
i(x \<mapsto> s) \<lbrakk> [ x' ]\<^sup>v \<rbrakk> ~ s'

goal (3 subgoals):
 1. \<And>x1a x2a s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x1a[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x1a \<rbrakk> ~ s' ; \<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x2a[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x2a \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s'
 2. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x3[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_cons x1a x2a x3)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 3. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x4[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_consp x1a x2a x3 x4)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x1a x2a s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x1a[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x1a \<rbrakk> ~ s' ; \<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x2a[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x2a \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s'
 2. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x3[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_cons x1a x2a x3)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 3. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x4[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_consp x1a x2a x3 x4)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
case (V_pair v1 v2)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v2[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ ?s'
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> [ v1 , v2 ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'

goal (3 subgoals):
 1. \<And>x1a x2a s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x1a[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x1a \<rbrakk> ~ s' ; \<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x2a[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x2a \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s'
 2. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x3[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_cons x1a x2a x3)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 3. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x4[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_consp x1a x2a x3 x4)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v2[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ ?s'
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> [ v1 , v2 ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'
[PROOF STEP]
obtain s1 and s2 where *:"eval_v i (v1[x::=v]\<^sub>v\<^sub>v) s1 \<and> eval_v i (v2[x::=v]\<^sub>v\<^sub>v) s2 \<and> s' = SPair s1 s2"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v2[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ ?s'
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> [ v1 , v2 ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'

goal (1 subgoal):
 1. (\<And>s1 s2. i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s1  \<and> i \<lbrakk> v2[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s2  \<and> s' = SPair s1 s2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using V_pair eval_v_elims subst_vv.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v2[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ ?s'
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> [ v1 , v2 ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v2[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ ?s'
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> [ v1 , v2 ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
[ ?l ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>v = [ ?l ]\<^sup>v
[ ?y ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>v = (if ?x = ?y then ?v else [ ?y ]\<^sup>v)
(V_cons ?tyid ?c ?v')[?x::=?v]\<^sub>v\<^sub>v = V_cons ?tyid ?c ?v'[?x::=?v]\<^sub>v\<^sub>v
(V_consp ?tyid ?c ?b ?v')[?x::=?v]\<^sub>v\<^sub>v = V_consp ?tyid ?c ?b ?v'[?x::=?v]\<^sub>v\<^sub>v
[ ?v1.0 , ?v2.0 ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>v = [ ?v1.0[?x::=?v]\<^sub>v\<^sub>v , ?v2.0[?x::=?v]\<^sub>v\<^sub>v ]\<^sup>v

goal (1 subgoal):
 1. (\<And>s1 s2. i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s1  \<and> i \<lbrakk> v2[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s2  \<and> s' = SPair s1 s2 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s1  \<and> i \<lbrakk> v2[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s2  \<and> s' = SPair s1 s2

goal (3 subgoals):
 1. \<And>x1a x2a s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x1a[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x1a \<rbrakk> ~ s' ; \<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x2a[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x2a \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s'
 2. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x3[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_cons x1a x2a x3)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 3. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x4[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_consp x1a x2a x3 x4)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
hence "(i ( x \<mapsto> s )) \<lbrakk> v1 \<rbrakk> ~ s1 \<and> (i ( x \<mapsto> s )) \<lbrakk> v2 \<rbrakk> ~ s2"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s1  \<and> i \<lbrakk> v2[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s2  \<and> s' = SPair s1 s2

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ s2
[PROOF STEP]
using V_pair
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s1  \<and> i \<lbrakk> v2[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s2  \<and> s' = SPair s1 s2
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v2[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ ?s'
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> [ v1 , v2 ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ s2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ s2

goal (3 subgoals):
 1. \<And>x1a x2a s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x1a[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x1a \<rbrakk> ~ s' ; \<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x2a[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x2a \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> [ x1a , x2a ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> [ x1a , x2a ]\<^sup>v \<rbrakk> ~ s'
 2. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x3[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_cons x1a x2a x3)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 3. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x4[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_consp x1a x2a x3 x4)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
thus  ?case
[PROOF STATE]
proof (prove)
using this:
i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ s2

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
using eval_v_pairI subst_vv.simps * V_pair
[PROOF STATE]
proof (prove)
using this:
i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1  \<and> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ s2
\<lbrakk>?i \<lbrakk> ?v1.0 \<rbrakk> ~ ?s1.0 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ ?s2.0 \<rbrakk> \<Longrightarrow> ?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ SPair ?s1.0 ?s2.0
[ ?l ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>v = [ ?l ]\<^sup>v
[ ?y ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>v = (if ?x = ?y then ?v else [ ?y ]\<^sup>v)
(V_cons ?tyid ?c ?v')[?x::=?v]\<^sub>v\<^sub>v = V_cons ?tyid ?c ?v'[?x::=?v]\<^sub>v\<^sub>v
(V_consp ?tyid ?c ?b ?v')[?x::=?v]\<^sub>v\<^sub>v = V_consp ?tyid ?c ?b ?v'[?x::=?v]\<^sub>v\<^sub>v
[ ?v1.0 , ?v2.0 ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>v = [ ?v1.0[?x::=?v]\<^sub>v\<^sub>v , ?v2.0[?x::=?v]\<^sub>v\<^sub>v ]\<^sup>v
i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s1  \<and> i \<lbrakk> v2[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s2  \<and> s' = SPair s1 s2
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v2[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v2 \<rbrakk> ~ ?s'
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> [ v1 , v2 ]\<^sup>v[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i(x \<mapsto> s) \<lbrakk> [ v1 , v2 ]\<^sup>v \<rbrakk> ~ s'

goal (2 subgoals):
 1. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x3[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_cons x1a x2a x3)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 2. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x4[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_consp x1a x2a x3 x4)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x3[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_cons x1a x2a x3)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 2. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x4[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_consp x1a x2a x3 x4)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
case (V_cons tyid dc v1)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> (V_cons tyid dc v1)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'

goal (2 subgoals):
 1. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x3[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_cons x1a x2a x3)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 2. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x4[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_consp x1a x2a x3 x4)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> (V_cons tyid dc v1)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'
[PROOF STEP]
obtain s1 where "eval_v i (v1[x::=v]\<^sub>v\<^sub>v) s1"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> (V_cons tyid dc v1)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'

goal (1 subgoal):
 1. (\<And>s1. i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s1  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_elims subst_vv.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> (V_cons tyid dc v1)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
[ ?l ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>v = [ ?l ]\<^sup>v
[ ?y ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>v = (if ?x = ?y then ?v else [ ?y ]\<^sup>v)
(V_cons ?tyid ?c ?v')[?x::=?v]\<^sub>v\<^sub>v = V_cons ?tyid ?c ?v'[?x::=?v]\<^sub>v\<^sub>v
(V_consp ?tyid ?c ?b ?v')[?x::=?v]\<^sub>v\<^sub>v = V_consp ?tyid ?c ?b ?v'[?x::=?v]\<^sub>v\<^sub>v
[ ?v1.0 , ?v2.0 ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>v = [ ?v1.0[?x::=?v]\<^sub>v\<^sub>v , ?v2.0[?x::=?v]\<^sub>v\<^sub>v ]\<^sup>v

goal (1 subgoal):
 1. (\<And>s1. i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s1  \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s1

goal (2 subgoals):
 1. \<And>x1a x2a x3 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x3[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x3 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_cons x1a x2a x3)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_cons x1a x2a x3 \<rbrakk> ~ s'
 2. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x4[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_consp x1a x2a x3 x4)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s1

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s'
[PROOF STEP]
using eval_v_consI V_cons
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s1
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ SCons ?tyid ?dc ?s
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> (V_cons tyid dc v1)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s'
[PROOF STEP]
by (metis eval_v_elims subst_vv.simps)
[PROOF STATE]
proof (state)
this:
i(x \<mapsto> s) \<lbrakk> V_cons tyid dc v1 \<rbrakk> ~ s'

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x4[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_consp x1a x2a x3 x4)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x4[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_consp x1a x2a x3 x4)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
case (V_consp tyid dc b1 v1)
[PROOF STATE]
proof (state)
this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> (V_consp tyid dc b1 v1)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x4[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_consp x1a x2a x3 x4)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> (V_consp tyid dc b1 v1)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'
[PROOF STEP]
obtain s1 where *:"eval_v i (v1[x::=v]\<^sub>v\<^sub>v) s1 \<and> s' = SConsp tyid dc b1 s1"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> (V_consp tyid dc b1 v1)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'

goal (1 subgoal):
 1. (\<And>s1. i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s1  \<and> s' = SConsp tyid dc b1 s1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using eval_v_elims subst_vv.simps
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> (V_consp tyid dc b1 v1)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'
\<lbrakk>?i \<lbrakk> [ ?l ]\<^sup>v \<rbrakk> ~ ?s ; ?s = \<lbrakk> ?l \<rbrakk>  \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?x ]\<^sup>v \<rbrakk> ~ ?s ; Some ?s = ?i ?x \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> [ ?v1.0 , ?v2.0 ]\<^sup>v \<rbrakk> ~ ?s ; \<And>s1 s2. \<lbrakk>?s = SPair s1 s2; ?i \<lbrakk> ?v1.0 \<rbrakk> ~ s1 ; ?i \<lbrakk> ?v2.0 \<rbrakk> ~ s2 \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_cons ?tyid ?dc ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SCons ?tyid ?dc s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
\<lbrakk>?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ ?s ; \<And>s. \<lbrakk>?s = SConsp ?tyid ?dc ?b s; ?i \<lbrakk> ?v \<rbrakk> ~ s \<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
[ ?l ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>v = [ ?l ]\<^sup>v
[ ?y ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>v = (if ?x = ?y then ?v else [ ?y ]\<^sup>v)
(V_cons ?tyid ?c ?v')[?x::=?v]\<^sub>v\<^sub>v = V_cons ?tyid ?c ?v'[?x::=?v]\<^sub>v\<^sub>v
(V_consp ?tyid ?c ?b ?v')[?x::=?v]\<^sub>v\<^sub>v = V_consp ?tyid ?c ?b ?v'[?x::=?v]\<^sub>v\<^sub>v
[ ?v1.0 , ?v2.0 ]\<^sup>v[?x::=?v]\<^sub>v\<^sub>v = [ ?v1.0[?x::=?v]\<^sub>v\<^sub>v , ?v2.0[?x::=?v]\<^sub>v\<^sub>v ]\<^sup>v

goal (1 subgoal):
 1. (\<And>s1. i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s1  \<and> s' = SConsp tyid dc b1 s1 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s1  \<and> s' = SConsp tyid dc b1 s1

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x4[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_consp x1a x2a x3 x4)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
hence "i ( x \<mapsto> s ) \<lbrakk> v1 \<rbrakk> ~ s1"
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s1  \<and> s' = SConsp tyid dc b1 s1

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1
[PROOF STEP]
using V_consp
[PROOF STATE]
proof (prove)
using this:
i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s1  \<and> s' = SConsp tyid dc b1 s1
\<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ ?s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ ?s'
i \<lbrakk> v \<rbrakk> ~ s
i \<lbrakk> (V_consp tyid dc b1 v1)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s'

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1

goal (1 subgoal):
 1. \<And>x1a x2a x3 x4 s'. \<lbrakk>\<And>s'. \<lbrakk>i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> x4[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> x4 \<rbrakk> ~ s' ; i \<lbrakk> v \<rbrakk> ~ s ; i \<lbrakk> (V_consp x1a x2a x3 x4)[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s' \<rbrakk> \<Longrightarrow> i(x \<mapsto> s) \<lbrakk> V_consp x1a x2a x3 x4 \<rbrakk> ~ s'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s'
[PROOF STEP]
using * eval_v_conspI
[PROOF STATE]
proof (prove)
using this:
i(x \<mapsto> s) \<lbrakk> v1 \<rbrakk> ~ s1
i \<lbrakk> v1[x::=v]\<^sub>v\<^sub>v \<rbrakk> ~ s1  \<and> s' = SConsp tyid dc b1 s1
?i \<lbrakk> ?v \<rbrakk> ~ ?s  \<Longrightarrow> ?i \<lbrakk> V_consp ?tyid ?dc ?b ?v \<rbrakk> ~ SConsp ?tyid ?dc ?b ?s

goal (1 subgoal):
 1. i(x \<mapsto> s) \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s'
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
i(x \<mapsto> s) \<lbrakk> V_consp tyid dc b1 v1 \<rbrakk> ~ s'

goal:
No subgoals!
[PROOF STEP]
qed