# Theory SmallStep

```(*  Title:       CoreC++
Author:      Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

Based on the Jinja theory J/SmallStep.thy by Tobias Nipkow
*)

section ‹Small Step Semantics›

theory SmallStep imports Syntax State begin

subsection ‹Some pre-definitions›

fun blocks :: "vname list × ty list × val list × expr ⇒ expr"
where
blocks_Cons:"blocks(V#Vs, T#Ts, v#vs, e) = {V:T := Val v; blocks(Vs,Ts,vs,e)}" |
blocks_Nil: "blocks([],[],[],e) = e"

lemma blocks_old_induct:
fixes P :: "vname list ⇒ ty list ⇒ val list ⇒ expr ⇒ bool"
shows
"⟦⋀aj ak al. P [] [] (aj # ak) al; ⋀ad ae a b. P [] (ad # ae) a b;
⋀V Vs a b. P (V # Vs) [] a b; ⋀V Vs T Ts aw. P (V # Vs) (T # Ts) [] aw;
⋀V Vs T Ts v vs e. P Vs Ts vs e ⟹ P (V # Vs) (T # Ts) (v # vs) e; ⋀e. P [] [] [] e⟧
⟹ P u v w x"
by (induction_schema) (pat_completeness, lexicographic_order)

lemma [simp]:
"⟦ size vs = size Vs; size Ts = size Vs ⟧ ⟹ fv(blocks(Vs,Ts,vs,e)) = fv e - set Vs"

apply(induct rule:blocks_old_induct)
apply simp_all
apply blast
done

definition assigned :: "vname ⇒ expr ⇒ bool" where
"assigned V e  ≡  ∃v e'. e = (V:= Val v;; e')"

subsection ‹The rules›

inductive_set
red  :: "prog ⇒ (env × (expr × state) × (expr × state)) set"
and reds  :: "prog ⇒ (env × (expr list × state) × (expr list × state)) set"
and red' :: "prog ⇒ env ⇒ expr ⇒ state ⇒ expr ⇒ state ⇒ bool"
("_,_ ⊢ ((1⟨_,/_⟩) →/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
and reds' :: "prog ⇒ env ⇒ expr list ⇒ state ⇒ expr list ⇒ state ⇒ bool"
("_,_ ⊢ ((1⟨_,/_⟩) [→]/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
for P :: prog
where

"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ≡ (E,(e,s), e',s') ∈ red P"
| "P,E ⊢ ⟨es,s⟩ [→] ⟨es',s'⟩ ≡ (E,(es,s), es',s') ∈ reds P"

| RedNew:
"⟦ new_Addr h = Some a; h' = h(a↦(C,Collect (init_obj P C))) ⟧
⟹ P,E ⊢ ⟨new C, (h,l)⟩ → ⟨ref (a,[C]), (h',l)⟩"

| RedNewFail:
P,E ⊢ ⟨new C, (h,l)⟩ → ⟨THROW OutOfMemory, (h,l)⟩"

| StaticCastRed:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨⦇C⦈e, s⟩ → ⟨⦇C⦈e', s'⟩"

| RedStaticCastNull:
"P,E ⊢ ⟨⦇C⦈null, s⟩ → ⟨null,s⟩"

| RedStaticUpCast:
"⟦ P ⊢ Path last Cs to C via Cs'; Ds = Cs@⇩pCs' ⟧
⟹ P,E ⊢ ⟨⦇C⦈(ref (a,Cs)), s⟩ → ⟨ref (a,Ds), s⟩"

| RedStaticDownCast:
"P,E ⊢ ⟨⦇C⦈(ref (a,Cs@[C]@Cs')), s⟩ → ⟨ref (a,Cs@[C]), s⟩"

| RedStaticCastFail:
"⟦C ∉ set Cs; ¬ P ⊢ (last Cs) ≼⇧* C⟧
⟹ P,E ⊢ ⟨⦇C⦈(ref (a,Cs)), s⟩ → ⟨THROW ClassCast, s⟩"

| DynCastRed:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨Cast C e, s⟩ → ⟨Cast C e', s'⟩"

| RedDynCastNull:
"P,E ⊢ ⟨Cast C null, s⟩ → ⟨null,s⟩"

| RedStaticUpDynCast: (* path uniqueness not necessary for type proof but for determinism *)
"⟦ P ⊢ Path last Cs to C unique; P ⊢ Path last Cs to C via Cs'; Ds = Cs@⇩pCs' ⟧
⟹ P,E ⊢ ⟨Cast C(ref(a,Cs)),s⟩ → ⟨ref(a,Ds),s⟩"

| RedStaticDownDynCast:
"P,E ⊢ ⟨Cast C (ref (a,Cs@[C]@Cs')), s⟩ → ⟨ref (a,Cs@[C]), s⟩"

| RedDynCast:(* path uniqueness not necessary for type proof but for determinism *)
"⟦ hp s a = Some(D,S); P ⊢ Path D to C via Cs';
P ⊢ Path D to C unique ⟧
⟹ P,E ⊢ ⟨Cast C (ref (a,Cs)), s⟩ → ⟨ref (a,Cs'), s⟩"

| RedDynCastFail:(* third premise not necessary for type proof but for determinism *)
"⟦hp s a = Some(D,S); ¬ P ⊢ Path D to C unique;
¬ P ⊢ Path last Cs to C unique; C ∉ set Cs ⟧
⟹ P,E ⊢ ⟨Cast C (ref (a,Cs)), s⟩ → ⟨null, s⟩"

| BinOpRed1:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨e «bop» e⇩2, s⟩ → ⟨e' «bop» e⇩2, s'⟩"

| BinOpRed2:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨(Val v⇩1) «bop» e, s⟩ → ⟨(Val v⇩1) «bop» e', s'⟩"

| RedBinOp:
"binop(bop,v⇩1,v⇩2) = Some v ⟹
P,E ⊢ ⟨(Val v⇩1) «bop» (Val v⇩2), s⟩ → ⟨Val v,s⟩"

| RedVar:
"lcl s V = Some v ⟹
P,E ⊢ ⟨Var V,s⟩ → ⟨Val v,s⟩"

| LAssRed:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨V:=e,s⟩ → ⟨V:=e',s'⟩"

| RedLAss:
"⟦E V = Some T; P ⊢ T casts v to v'⟧ ⟹
P,E ⊢ ⟨V:=(Val v),(h,l)⟩ → ⟨Val v',(h,l(V↦v'))⟩"

| FAccRed:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨e∙F{Cs}, s⟩ → ⟨e'∙F{Cs}, s'⟩"

| RedFAcc:
"⟦ hp s a = Some(D,S); Ds = Cs'@⇩pCs; (Ds,fs) ∈ S; fs F = Some v ⟧
⟹ P,E ⊢ ⟨(ref (a,Cs'))∙F{Cs}, s⟩ → ⟨Val v,s⟩"

| RedFAccNull:
"P,E ⊢ ⟨null∙F{Cs}, s⟩ → ⟨THROW NullPointer, s⟩"

| FAssRed1:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨e∙F{Cs}:=e⇩2, s⟩ → ⟨e'∙F{Cs}:=e⇩2, s'⟩"

| FAssRed2:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨Val v∙F{Cs}:=e, s⟩ → ⟨Val v∙F{Cs}:=e', s'⟩"

| RedFAss:
"⟦h a = Some(D,S); P ⊢ (last Cs') has least F:T via Cs;
P ⊢ T casts v to v'; Ds = Cs'@⇩pCs; (Ds,fs) ∈ S⟧ ⟹
P,E ⊢ ⟨(ref (a,Cs'))∙F{Cs}:=(Val v), (h,l)⟩ → ⟨Val v', (h(a ↦ (D,insert (Ds,fs(F↦v')) (S - {(Ds,fs)}))),l)⟩"

| RedFAssNull:
"P,E ⊢ ⟨null∙F{Cs}:=Val v, s⟩ → ⟨THROW NullPointer, s⟩"

| CallObj:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨Call e Copt M es,s⟩ → ⟨Call e' Copt M es,s'⟩"

| CallParams:
"P,E ⊢ ⟨es,s⟩ [→] ⟨es',s'⟩ ⟹
P,E ⊢ ⟨Call (Val v) Copt M es,s⟩ → ⟨Call (Val v) Copt M es',s'⟩"

| RedCall:
"⟦ hp s a = Some(C,S); P ⊢ last Cs has least M = (Ts',T',pns',body') via Ds;
P ⊢ (C,Cs@⇩pDs) selects M = (Ts,T,pns,body) via Cs';
size vs = size pns; size Ts = size pns;
bs = blocks(this#pns,Class(last Cs')#Ts,Ref(a,Cs')#vs,body);
new_body = (case T' of Class D ⇒ ⦇D⦈bs | _ ⇒ bs)⟧
⟹ P,E ⊢ ⟨(ref (a,Cs))∙M(map Val vs), s⟩ → ⟨new_body, s⟩"

| RedStaticCall:
"⟦ P ⊢ Path (last Cs) to C unique; P ⊢ Path (last Cs) to C via Cs'';
P ⊢ C has least M = (Ts,T,pns,body) via Cs'; Ds = (Cs@⇩pCs'')@⇩pCs';
size vs = size pns; size Ts = size pns ⟧
⟹ P,E ⊢ ⟨(ref (a,Cs))∙(C::)M(map Val vs), s⟩ →
⟨blocks(this#pns,Class(last Ds)#Ts,Ref(a,Ds)#vs,body), s⟩"

| RedCallNull:
"P,E ⊢ ⟨Call null Copt M (map Val vs),s⟩ → ⟨THROW NullPointer,s⟩"

| BlockRedNone:
"⟦ P,E(V ↦ T) ⊢ ⟨e, (h,l(V:=None))⟩ → ⟨e', (h',l')⟩; l' V = None; ¬ assigned V e ⟧
⟹ P,E ⊢ ⟨{V:T; e}, (h,l)⟩ → ⟨{V:T; e'}, (h',l'(V := l V))⟩"

| BlockRedSome:
"⟦ P,E(V ↦ T) ⊢ ⟨e, (h,l(V:=None))⟩ → ⟨e', (h',l')⟩; l' V = Some v;
¬ assigned V e ⟧
⟹ P,E ⊢ ⟨{V:T; e}, (h,l)⟩ → ⟨{V:T := Val v; e'}, (h',l'(V := l V))⟩"

| InitBlockRed:
"⟦ P,E(V ↦ T) ⊢ ⟨e, (h,l(V↦v'))⟩ → ⟨e', (h',l')⟩; l' V = Some v'';
P ⊢ T casts v to v' ⟧
⟹ P,E ⊢ ⟨{V:T := Val v; e}, (h,l)⟩ → ⟨{V:T := Val v''; e'}, (h',l'(V := l V))⟩"

| RedBlock:
"P,E ⊢ ⟨{V:T; Val u}, s⟩ → ⟨Val u, s⟩"

| RedInitBlock:
"P ⊢ T casts v to v' ⟹ P,E ⊢ ⟨{V:T := Val v; Val u}, s⟩ → ⟨Val u, s⟩"

| SeqRed:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨e;;e⇩2, s⟩ → ⟨e';;e⇩2, s'⟩"

| RedSeq:
"P,E ⊢ ⟨(Val v);;e⇩2, s⟩ → ⟨e⇩2, s⟩"

| CondRed:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨if (e) e⇩1 else e⇩2, s⟩ → ⟨if (e') e⇩1 else e⇩2, s'⟩"

| RedCondT:
"P,E ⊢ ⟨if (true) e⇩1 else e⇩2, s⟩ → ⟨e⇩1, s⟩"

| RedCondF:
"P,E ⊢ ⟨if (false) e⇩1 else e⇩2, s⟩ → ⟨e⇩2, s⟩"

| RedWhile:
"P,E ⊢ ⟨while(b) c, s⟩ → ⟨if(b) (c;;while(b) c) else unit, s⟩"

| ThrowRed:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨throw e, s⟩ → ⟨throw e', s'⟩"

| RedThrowNull:
"P,E ⊢ ⟨throw null, s⟩ → ⟨THROW NullPointer, s⟩"

| ListRed1:
"P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹
P,E ⊢ ⟨e#es,s⟩ [→] ⟨e'#es,s'⟩"

| ListRed2:
"P,E ⊢ ⟨es,s⟩ [→] ⟨es',s'⟩ ⟹
P,E ⊢ ⟨Val v # es,s⟩ [→] ⟨Val v # es',s'⟩"

― ‹Exception propagation›

| DynCastThrow: "P,E ⊢ ⟨Cast C (Throw r), s⟩ → ⟨Throw r, s⟩"
| StaticCastThrow: "P,E ⊢ ⟨⦇C⦈(Throw r), s⟩ → ⟨Throw r, s⟩"
| BinOpThrow1: "P,E ⊢ ⟨(Throw r) «bop» e⇩2, s⟩ → ⟨Throw r, s⟩"
| BinOpThrow2: "P,E ⊢ ⟨(Val v⇩1) «bop» (Throw r), s⟩ → ⟨Throw r, s⟩"
| LAssThrow: "P,E ⊢ ⟨V:=(Throw r), s⟩ → ⟨Throw r, s⟩"
| FAccThrow: "P,E ⊢ ⟨(Throw r)∙F{Cs}, s⟩ → ⟨Throw r, s⟩"
| FAssThrow1: "P,E ⊢ ⟨(Throw r)∙F{Cs}:=e⇩2, s⟩ → ⟨Throw r,s⟩"
| FAssThrow2: "P,E ⊢ ⟨Val v∙F{Cs}:=(Throw r), s⟩ → ⟨Throw r, s⟩"
| CallThrowObj: "P,E ⊢ ⟨Call (Throw r) Copt M es, s⟩ → ⟨Throw r, s⟩"
| CallThrowParams: "⟦ es = map Val vs @ Throw r # es' ⟧
⟹ P,E ⊢ ⟨Call (Val v) Copt M es, s⟩ → ⟨Throw r, s⟩"
| BlockThrow: "P,E ⊢ ⟨{V:T; Throw r}, s⟩ → ⟨Throw r, s⟩"
| InitBlockThrow: "P ⊢ T casts v to v'
⟹ P,E ⊢ ⟨{V:T := Val v; Throw r}, s⟩ → ⟨Throw r, s⟩"
| SeqThrow: "P,E ⊢ ⟨(Throw r);;e⇩2, s⟩ → ⟨Throw r, s⟩"
| CondThrow: "P,E ⊢ ⟨if (Throw r) e⇩1 else e⇩2, s⟩ → ⟨Throw r, s⟩"
| ThrowThrow: "P,E ⊢ ⟨throw(Throw r), s⟩ → ⟨Throw r, s⟩"

lemmas red_reds_induct = red_reds.induct [split_format (complete)]
and red_reds_inducts = red_reds.inducts [split_format (complete)]

inductive_cases [elim!]:
"P,E ⊢ ⟨V:=e,s⟩ → ⟨e',s'⟩"
"P,E ⊢ ⟨e1;;e2,s⟩ → ⟨e',s'⟩"

declare Cons_eq_map_conv [iff]

lemma "P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩ ⟹ True"
and reds_length:"P,E ⊢ ⟨es,s⟩ [→] ⟨es',s'⟩ ⟹ length es = length es'"
by (induct rule: red_reds.inducts) auto

subsection‹The reflexive transitive closure›

definition Red :: "prog ⇒ env ⇒ ((expr × state) × (expr × state)) set"
where "Red P E = {((e,s),e',s'). P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩}"

definition Reds :: "prog ⇒ env ⇒ ((expr list × state) × (expr list × state)) set"
where "Reds P E = {((es,s),es',s'). P,E ⊢ ⟨es,s⟩ [→] ⟨es',s'⟩}"

lemma[simp]: "((e,s),e',s') ∈ Red P E = P,E ⊢ ⟨e,s⟩ → ⟨e',s'⟩"

lemma[simp]: "((es,s),es',s') ∈ Reds P E = P,E ⊢ ⟨es,s⟩ [→] ⟨es',s'⟩"

abbreviation
Step :: "prog ⇒ env ⇒ expr ⇒ state ⇒ expr ⇒ state ⇒ bool"
("_,_ ⊢ ((1⟨_,/_⟩) →*/ (1⟨_,/_⟩))" [51,0,0,0,0] 81) where
"P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩ ≡ ((e,s), e',s') ∈ (Red P E)⇧*"

abbreviation
Steps :: "prog ⇒ env ⇒ expr list ⇒ state ⇒ expr list ⇒ state ⇒ bool"
("_,_ ⊢ ((1⟨_,/_⟩) [→]*/ (1⟨_,/_⟩))" [51,0,0,0,0] 81) where
"P,E ⊢ ⟨es,s⟩ [→]* ⟨es',s'⟩ ≡ ((es,s), es',s') ∈ (Reds P E)⇧*"

lemma converse_rtrancl_induct_red[consumes 1]:
assumes "P,E ⊢ ⟨e,(h,l)⟩ →* ⟨e',(h',l')⟩"
and "⋀e h l. R e h l e h l"
and "⋀e⇩0 h⇩0 l⇩0 e⇩1 h⇩1 l⇩1 e' h' l'.
⟦ P,E ⊢ ⟨e⇩0,(h⇩0,l⇩0)⟩ → ⟨e⇩1,(h⇩1,l⇩1)⟩; R e⇩1 h⇩1 l⇩1 e' h' l' ⟧ ⟹ R e⇩0 h⇩0 l⇩0 e' h' l'"
shows "R e h l e' h' l'"

proof -
{ fix s s'
assume reds: "P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩"
and base: "⋀e s. R e (hp s) (lcl s) e (hp s) (lcl s)"
and IH: "⋀e⇩0 s⇩0 e⇩1 s⇩1 e' s'.
⟦ P,E ⊢ ⟨e⇩0,s⇩0⟩ → ⟨e⇩1,s⇩1⟩; R e⇩1 (hp s⇩1) (lcl s⇩1) e' (hp s') (lcl s') ⟧
⟹ R e⇩0 (hp s⇩0) (lcl s⇩0) e' (hp s') (lcl s')"
from reds have "R e (hp s) (lcl s) e' (hp s') (lcl s')"
proof (induct rule:converse_rtrancl_induct2)
case refl show ?case by(rule base)
next
case (step e⇩0 s⇩0 e s)
have Red:"((e⇩0,s⇩0),e,s) ∈ Red P E"
and R:"R e (hp s) (lcl s) e' (hp s') (lcl s')" by fact+
from IH[OF Red[simplified] R] show ?case .
qed
}
with assms show ?thesis by fastforce
qed

lemma steps_length:"P,E ⊢ ⟨es,s⟩ [→]* ⟨es',s'⟩ ⟹ length es = length es'"
by(induct rule:rtrancl_induct2,auto intro:reds_length)

subsection‹Some easy lemmas›

lemma [iff]: "¬ P,E ⊢ ⟨[],s⟩ [→] ⟨es',s'⟩"
by(blast elim: reds.cases)

lemma [iff]: "¬ P,E ⊢ ⟨Val v,s⟩ → ⟨e',s'⟩"
by(fastforce elim: red.cases)

lemma [iff]: "¬ P,E ⊢ ⟨Throw r,s⟩ → ⟨e',s'⟩"
by(fastforce elim: red.cases)

lemma red_lcl_incr: "P,E ⊢ ⟨e,(h⇩0,l⇩0)⟩ → ⟨e',(h⇩1,l⇩1)⟩ ⟹ dom l⇩0 ⊆ dom l⇩1"
and "P,E ⊢ ⟨es,(h⇩0,l⇩0)⟩ [→] ⟨es',(h⇩1,l⇩1)⟩ ⟹ dom l⇩0 ⊆ dom l⇩1"
by (induct rule: red_reds_inducts) (auto simp del:fun_upd_apply)

lemma red_lcl_add: "P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩ ⟹ (⋀l⇩0. P,E ⊢ ⟨e,(h,l⇩0++l)⟩ → ⟨e',(h',l⇩0++l')⟩)"
and "P,E ⊢ ⟨es,(h,l)⟩ [→] ⟨es',(h',l')⟩ ⟹ (⋀l⇩0. P,E ⊢ ⟨es,(h,l⇩0++l)⟩ [→] ⟨es',(h',l⇩0++l')⟩)"

proof (induct rule:red_reds_inducts)
case RedLAss thus ?case by(auto intro:red_reds.intros simp del:fun_upd_apply)
next
case RedStaticDownCast thus ?case by(fastforce intro:red_reds.intros)
next
case RedStaticUpDynCast thus ?case by(fastforce intro:red_reds.intros)
next
case RedStaticDownDynCast thus ?case by(fastforce intro:red_reds.intros)
next
case RedDynCast thus ?case by(fastforce intro:red_reds.intros)
next
case RedDynCastFail thus ?case by(fastforce intro:red_reds.intros)
next
case RedFAcc thus ?case by(fastforce intro:red_reds.intros)
next
case RedFAss thus ?case by (fastforce intro:red_reds.intros)
next
case RedCall thus ?case by (fastforce intro!:red_reds.RedCall)
next
case RedStaticCall thus ?case by(fastforce intro:red_reds.intros)
next
case (InitBlockRed E V T e h l v' e' h' l' v'' v l⇩0)
have IH: "⋀l⇩0. P,E(V ↦ T) ⊢ ⟨e,(h, l⇩0 ++ l(V ↦ v'))⟩ → ⟨e',(h', l⇩0 ++ l')⟩"
and l'V: "l' V = Some v''" and casts:"P ⊢ T casts v to v'" by fact+
from IH have IH': "P,E(V ↦ T) ⊢ ⟨e,(h, (l⇩0 ++ l)(V ↦ v'))⟩ → ⟨e',(h',l⇩0 ++ l')⟩"
by simp
have "(l⇩0 ++ l')(V := (l⇩0 ++ l) V) = l⇩0 ++ l'(V := l V)"
with red_reds.InitBlockRed[OF IH' _ casts] l'V show ?case
by(simp del:fun_upd_apply)
next
case (BlockRedNone E V T e h l e' h' l' l⇩0)
have IH: "⋀l⇩0. P,E(V ↦ T) ⊢ ⟨e,(h, l⇩0 ++ l(V := None))⟩ → ⟨e',(h', l⇩0 ++ l')⟩"
and l'V: "l' V = None" and unass: "¬ assigned V e" by fact+
have "l⇩0(V := None) ++ l(V := None) = (l⇩0 ++ l)(V := None)"
hence IH': "P,E(V ↦ T) ⊢ ⟨e,(h, (l⇩0++l)(V := None))⟩ → ⟨e',(h', l⇩0(V := None) ++ l')⟩"
using IH[of "l⇩0(V := None)"] by simp
have "(l⇩0(V := None) ++ l')(V := (l⇩0 ++ l) V) = l⇩0 ++ l'(V := l V)"
with red_reds.BlockRedNone[OF IH' _ unass] l'V show ?case
next
case (BlockRedSome E V T e h l e' h' l' v l⇩0)
have IH: "⋀l⇩0. P,E(V ↦ T) ⊢ ⟨e,(h, l⇩0 ++ l(V := None))⟩ → ⟨e',(h', l⇩0 ++ l')⟩"
and l'V: "l' V = Some v" and unass: "¬ assigned V e" by fact+
have "l⇩0(V := None) ++ l(V := None) = (l⇩0 ++ l)(V := None)"
hence IH': "P,E(V ↦ T) ⊢ ⟨e,(h, (l⇩0++l)(V := None))⟩ → ⟨e',(h', l⇩0(V := None) ++ l')⟩"
using IH[of "l⇩0(V := None)"] by simp
have "(l⇩0(V := None) ++ l')(V := (l⇩0 ++ l) V) = l⇩0 ++ l'(V := l V)"
with red_reds.BlockRedSome[OF IH' _ unass] l'V show ?case
next

assumes "P,E ⊢ ⟨e,(h,l)⟩ →* ⟨e',(h',l')⟩" shows "P,E ⊢ ⟨e,(h,l⇩0++l)⟩ →* ⟨e',(h',l⇩0++l')⟩"
using assms
proof(induct rule:converse_rtrancl_induct_red)
case 1 thus ?case by simp
next
case 2 thus ?case
by(auto dest: red_lcl_add intro: converse_rtrancl_into_rtrancl simp:Red_def)
qed

lemma
red_preserves_obj:"⟦P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩; h a = Some(D,S)⟧
⟹ ∃S'. h' a = Some(D,S')"
and reds_preserves_obj:"⟦P,E ⊢ ⟨es,(h,l)⟩ [→] ⟨es',(h',l')⟩; h a = Some(D,S)⟧
⟹ ∃S'. h' a = Some(D,S')"