[STATEMENT]
lemma eval\<^sub>1_preserves_unmod:
  "\<lbrakk> P \<turnstile>\<^sub>1 \<langle>e,(h,ls)\<rangle> \<Rightarrow> \<langle>e',(h',ls')\<rangle>; unmod e i; i < size ls \<rbrakk>
  \<Longrightarrow> ls ! i = ls' ! i"
and "\<lbrakk> P \<turnstile>\<^sub>1 \<langle>es,(h,ls)\<rangle> [\<Rightarrow>] \<langle>es',(h',ls')\<rangle>; unmods es i; i < size ls \<rbrakk>
      \<Longrightarrow> ls ! i = ls' ! i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>P \<turnstile>\<^sub>1 \<langle>e,(h, ls)\<rangle> \<Rightarrow> \<langle>e',(h', ls')\<rangle>; unmod e i; i < length ls\<rbrakk> \<Longrightarrow> ls ! i = ls' ! i) &&& (\<lbrakk>P \<turnstile>\<^sub>1 \<langle>es,(h, ls)\<rangle> [\<Rightarrow>] \<langle>es',(h', ls')\<rangle>; unmods es i; i < length ls\<rbrakk> \<Longrightarrow> ls ! i = ls' ! i)
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>P \<turnstile>\<^sub>1 \<langle>e,(h, ls)\<rangle> \<Rightarrow> \<langle>e',(h', ls')\<rangle>; unmod e i; i < length ls\<rbrakk> \<Longrightarrow> ls ! i = ls' ! i) &&& (\<lbrakk>P \<turnstile>\<^sub>1 \<langle>es,(h, ls)\<rangle> [\<Rightarrow>] \<langle>es',(h', ls')\<rangle>; unmods es i; i < length ls\<rbrakk> \<Longrightarrow> ls ! i = ls' ! i)
[PROOF STEP]
proof(induct rule:eval\<^sub>1_evals\<^sub>1_inducts)
[PROOF STATE]
proof (state)
goal (43 subgoals):
 1. \<And>h a C FDTs h' l. \<lbrakk>new_Addr h = \<lfloor>a\<rfloor>; P \<turnstile> C has_fields FDTs; h' = h(a \<mapsto> (C, init_fields FDTs)); unmod (new C) i; i < length l\<rbrakk> \<Longrightarrow> l ! i = l ! i
 2. \<And>h C l. \<lbrakk>new_Addr h = None; unmod (new C) i; i < length l\<rbrakk> \<Longrightarrow> l ! i = l ! i
 3. \<And>e a b aa h l D fs C. \<lbrakk>P \<turnstile>\<^sub>1 \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>addr aa,(h, l)\<rangle>; \<lbrakk>unmod e i; i < length b\<rbrakk> \<Longrightarrow> b ! i = l ! i; h aa = \<lfloor>(D, fs)\<rfloor>; P \<turnstile> D \<preceq>\<^sup>* C; unmod (Cast C e) i; i < length b\<rbrakk> \<Longrightarrow> b ! i = l ! i
 4. \<And>e a b aa ba C. \<lbrakk>P \<turnstile>\<^sub>1 \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>null,(aa, ba)\<rangle>; \<lbrakk>unmod e i; i < length b\<rbrakk> \<Longrightarrow> b ! i = ba ! i; unmod (Cast C e) i; i < length b\<rbrakk> \<Longrightarrow> b ! i = ba ! i
 5. \<And>e a b aa h l D fs C. \<lbrakk>P \<turnstile>\<^sub>1 \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>addr aa,(h, l)\<rangle>; \<lbrakk>unmod e i; i < length b\<rbrakk> \<Longrightarrow> b ! i = l ! i; h aa = \<lfloor>(D, fs)\<rfloor>; (D, C) \<notin> (subcls1 P)\<^sup>*; unmod (Cast C e) i; i < length b\<rbrakk> \<Longrightarrow> b ! i = l ! i
 6. \<And>e a b e' aa ba C. \<lbrakk>P \<turnstile>\<^sub>1 \<langle>e,(a, b)\<rangle> \<Rightarrow> \<langle>throw e',(aa, ba)\<rangle>; \<lbrakk>unmod e i; i < length b\<rbrakk> \<Longrightarrow> b ! i = ba ! i; unmod (Cast C e) i; i < length b\<rbrakk> \<Longrightarrow> b ! i = ba ! i
 7. \<And>v a b. \<lbrakk>unmod (Val v) i; i < length b\<rbrakk> \<Longrightarrow> b ! i = b ! i
 8. \<And>e\<^sub>1 a b v\<^sub>1 aa ba e\<^sub>2 v\<^sub>2 ab bb bop v. \<lbrakk>P \<turnstile>\<^sub>1 \<langle>e\<^sub>1,(a, b)\<rangle> \<Rightarrow> \<langle>Val v\<^sub>1,(aa, ba)\<rangle>; \<lbrakk>unmod e\<^sub>1 i; i < length b\<rbrakk> \<Longrightarrow> b ! i = ba ! i; P \<turnstile>\<^sub>1 \<langle>e\<^sub>2,(aa, ba)\<rangle> \<Rightarrow> \<langle>Val v\<^sub>2,(ab, bb)\<rangle>; \<lbrakk>unmod e\<^sub>2 i; i < length ba\<rbrakk> \<Longrightarrow> ba ! i = bb ! i; binop (bop, v\<^sub>1, v\<^sub>2) = \<lfloor>v\<rfloor>; unmod (e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2) i; i < length b\<rbrakk> \<Longrightarrow> b ! i = bb ! i
 9. \<And>e\<^sub>1 a b e aa ba bop e\<^sub>2. \<lbrakk>P \<turnstile>\<^sub>1 \<langle>e\<^sub>1,(a, b)\<rangle> \<Rightarrow> \<langle>throw e,(aa, ba)\<rangle>; \<lbrakk>unmod e\<^sub>1 i; i < length b\<rbrakk> \<Longrightarrow> b ! i = ba ! i; unmod (e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2) i; i < length b\<rbrakk> \<Longrightarrow> b ! i = ba ! i
 10. \<And>e\<^sub>1 a b v\<^sub>1 aa ba e\<^sub>2 e ab bb bop. \<lbrakk>P \<turnstile>\<^sub>1 \<langle>e\<^sub>1,(a, b)\<rangle> \<Rightarrow> \<langle>Val v\<^sub>1,(aa, ba)\<rangle>; \<lbrakk>unmod e\<^sub>1 i; i < length b\<rbrakk> \<Longrightarrow> b ! i = ba ! i; P \<turnstile>\<^sub>1 \<langle>e\<^sub>2,(aa, ba)\<rangle> \<Rightarrow> \<langle>throw e,(ab, bb)\<rangle>; \<lbrakk>unmod e\<^sub>2 i; i < length ba\<rbrakk> \<Longrightarrow> ba ! i = bb ! i; unmod (e\<^sub>1 \<guillemotleft>bop\<guillemotright> e\<^sub>2) i; i < length b\<rbrakk> \<Longrightarrow> b ! i = bb ! i
A total of 43 subgoals...
[PROOF STEP]
qed(auto dest!:eval\<^sub>1_preserves_len evals\<^sub>1_preserves_len split:if_split_asm)


[STATEMENT]
lemma LAss_lem:
  "\<lbrakk>x \<in> set xs; size xs \<le> size ys \<rbrakk>
  \<Longrightarrow> m\<^sub>1 \<subseteq>\<^sub>m m\<^sub>2(xs[\<mapsto>]ys) \<Longrightarrow> m\<^sub>1(x\<mapsto>y) \<subseteq>\<^sub>m m\<^sub>2(xs[\<mapsto>]ys[last_index xs x := y])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set xs; length xs \<le> length ys; m\<^sub>1 \<subseteq>\<^sub>m m\<^sub>2(xs [\<mapsto>] ys)\<rbrakk> \<Longrightarrow> m\<^sub>1(x \<mapsto> y) \<subseteq>\<^sub>m m\<^sub>2(xs [\<mapsto>] ys[last_index xs x := y])
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set xs; length xs \<le> length ys; m\<^sub>1 \<subseteq>\<^sub>m m\<^sub>2(xs [\<mapsto>] ys)\<rbrakk> \<Longrightarrow> m\<^sub>1(x \<mapsto> y) \<subseteq>\<^sub>m m\<^sub>2(xs [\<mapsto>] ys[last_index xs x := y])
[PROOF STEP]
by(simp add:map_le_def fun_upds_apply eq_sym_conv)


[STATEMENT]
lemma Block_lem:
fixes l :: "'a \<rightharpoonup> 'b"
assumes 0: "l \<subseteq>\<^sub>m [Vs [\<mapsto>] ls]"
    and 1: "l' \<subseteq>\<^sub>m [Vs [\<mapsto>] ls', V\<mapsto>v]"
    and hidden: "V \<in> set Vs \<Longrightarrow> ls ! last_index Vs V = ls' ! last_index Vs V"
    and size: "size ls = size ls'"    "size Vs < size ls'"
shows "l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
(*<*)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
have "l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls', V\<mapsto>v](V := l V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls', V \<mapsto> v](V := l V)
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
l' \<subseteq>\<^sub>m [Vs [\<mapsto>] ls', V \<mapsto> v]

goal (1 subgoal):
 1. l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls', V \<mapsto> v](V := l V)
[PROOF STEP]
by(rule map_le_upd)
[PROOF STATE]
proof (state)
this:
l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls', V \<mapsto> v](V := l V)

goal (1 subgoal):
 1. l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls', V \<mapsto> v](V := l V)

goal (1 subgoal):
 1. l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
have "\<dots> = [Vs [\<mapsto>] ls'](V := l V)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [Vs [\<mapsto>] ls', V \<mapsto> v](V := l V) = [Vs [\<mapsto>] ls'](V := l V)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[Vs [\<mapsto>] ls', V \<mapsto> v](V := l V) = [Vs [\<mapsto>] ls'](V := l V)

goal (1 subgoal):
 1. l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
[Vs [\<mapsto>] ls', V \<mapsto> v](V := l V) = [Vs [\<mapsto>] ls'](V := l V)

goal (1 subgoal):
 1. l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
have "\<dots> \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
proof (cases "l V")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. l V = None \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
 2. \<And>a. l V = \<lfloor>a\<rfloor> \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
case None
[PROOF STATE]
proof (state)
this:
l V = None

goal (2 subgoals):
 1. l V = None \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
 2. \<And>a. l V = \<lfloor>a\<rfloor> \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
l V = None

goal (1 subgoal):
 1. [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']

goal (1 subgoal):
 1. \<And>a. l V = \<lfloor>a\<rfloor> \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. l V = \<lfloor>a\<rfloor> \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
case (Some w)
[PROOF STATE]
proof (state)
this:
l V = \<lfloor>w\<rfloor>

goal (1 subgoal):
 1. \<And>a. l V = \<lfloor>a\<rfloor> \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
hence "[Vs [\<mapsto>] ls] V = Some w"
[PROOF STATE]
proof (prove)
using this:
l V = \<lfloor>w\<rfloor>

goal (1 subgoal):
 1. [Vs [\<mapsto>] ls] V = \<lfloor>w\<rfloor>
[PROOF STEP]
using 0
[PROOF STATE]
proof (prove)
using this:
l V = \<lfloor>w\<rfloor>
l \<subseteq>\<^sub>m [Vs [\<mapsto>] ls]

goal (1 subgoal):
 1. [Vs [\<mapsto>] ls] V = \<lfloor>w\<rfloor>
[PROOF STEP]
by(force simp add: map_le_def split:if_splits)
[PROOF STATE]
proof (state)
this:
[Vs [\<mapsto>] ls] V = \<lfloor>w\<rfloor>

goal (1 subgoal):
 1. \<And>a. l V = \<lfloor>a\<rfloor> \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
hence VinVs: "V \<in> set Vs" and w: "w = ls ! last_index Vs V"
[PROOF STATE]
proof (prove)
using this:
[Vs [\<mapsto>] ls] V = \<lfloor>w\<rfloor>

goal (1 subgoal):
 1. V \<in> set Vs &&& w = ls ! last_index Vs V
[PROOF STEP]
using size
[PROOF STATE]
proof (prove)
using this:
[Vs [\<mapsto>] ls] V = \<lfloor>w\<rfloor>
length ls = length ls'
length Vs < length ls'

goal (1 subgoal):
 1. V \<in> set Vs &&& w = ls ! last_index Vs V
[PROOF STEP]
by(auto simp add:fun_upds_apply split:if_splits)
[PROOF STATE]
proof (state)
this:
V \<in> set Vs
w = ls ! last_index Vs V

goal (1 subgoal):
 1. \<And>a. l V = \<lfloor>a\<rfloor> \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
hence "w = ls' ! last_index Vs V"
[PROOF STATE]
proof (prove)
using this:
V \<in> set Vs
w = ls ! last_index Vs V

goal (1 subgoal):
 1. w = ls' ! last_index Vs V
[PROOF STEP]
using hidden[OF VinVs]
[PROOF STATE]
proof (prove)
using this:
V \<in> set Vs
w = ls ! last_index Vs V
ls ! last_index Vs V = ls' ! last_index Vs V

goal (1 subgoal):
 1. w = ls' ! last_index Vs V
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
w = ls' ! last_index Vs V

goal (1 subgoal):
 1. \<And>a. l V = \<lfloor>a\<rfloor> \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
hence "[Vs [\<mapsto>] ls'](V := l V) = [Vs [\<mapsto>] ls']"
[PROOF STATE]
proof (prove)
using this:
w = ls' ! last_index Vs V

goal (1 subgoal):
 1. [Vs [\<mapsto>] ls'](V := l V) = [Vs [\<mapsto>] ls']
[PROOF STEP]
using Some size VinVs
[PROOF STATE]
proof (prove)
using this:
w = ls' ! last_index Vs V
l V = \<lfloor>w\<rfloor>
length ls = length ls'
length Vs < length ls'
V \<in> set Vs

goal (1 subgoal):
 1. [Vs [\<mapsto>] ls'](V := l V) = [Vs [\<mapsto>] ls']
[PROOF STEP]
by(simp add: map_upds_upd_conv_last_index)
[PROOF STATE]
proof (state)
this:
[Vs [\<mapsto>] ls'](V := l V) = [Vs [\<mapsto>] ls']

goal (1 subgoal):
 1. \<And>a. l V = \<lfloor>a\<rfloor> \<Longrightarrow> [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
[Vs [\<mapsto>] ls'](V := l V) = [Vs [\<mapsto>] ls']

goal (1 subgoal):
 1. [Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[Vs [\<mapsto>] ls'](V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']

goal (1 subgoal):
 1. l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']

goal (1 subgoal):
 1. l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
l'(V := l V) \<subseteq>\<^sub>m [Vs [\<mapsto>] ls']

goal:
No subgoals!
[PROOF STEP]
qed