Theory SmallStep

(*  Title:       CoreC++
    ID:          $Id: SmallStep.thy,v 1.15 2007-07-19 21:23:09 makarius Exp $
    Author:      Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

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


header {* \isaheader{Small Step Semantics} *}

theory SmallStep imports Syntax State begin


section {* Some pre-definitions *}

consts blocks :: "vname list × ty list × val list × expr => expr"
recdef blocks "measure(λ(Vs,Ts,vs,e). size Vs)"
 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 [simp]:
  "[| size vs = size Vs; size Ts = size Vs |] ==> fv(blocks(Vs,Ts,vs,e)) = fv e - set Vs"

apply(induct rule:blocks.induct)
apply simp_all
apply blast
done



constdefs
  assigned :: "vname => expr => bool"
  "assigned V e  ≡  ∃v e'. e = (V:= Val v;; e')"


section {* 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"
          ("_,_ \<turnstile> ((1⟨_,/_⟩) ->/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  and reds' :: "prog => env => expr list => state => expr list => state => bool"
          ("_,_ \<turnstile> ((1⟨_,/_⟩) [->]/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  for P :: prog
where

  "P,E \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ≡ (E,(e,s), e',s') ∈ red P"
| "P,E \<turnstile> ⟨es,s⟩ [->] ⟨es',s'⟩ ≡ (E,(es,s), es',s') ∈ reds P"

| RedNew:
  "[| new_Addr h = Some a; h' = h(a\<mapsto>(C,Collect (init_obj P C))) |]
  ==> P,E \<turnstile> ⟨new C, (h,l)⟩ -> ⟨ref (a,[C]), (h',l)⟩"

| RedNewFail:
  "new_Addr h = None ==>
  P,E \<turnstile> ⟨new C, (h,l)⟩ -> ⟨THROW OutOfMemory, (h,l)⟩"

| StaticCastRed:
  "P,E \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P,E \<turnstile> ⟨(|C|)),e, s⟩ -> ⟨(|C|)),e', s'⟩"

| RedStaticCastNull:
  "P,E \<turnstile> ⟨(|C|)),null, s⟩ -> ⟨null,s⟩"

| RedStaticUpCast:
  "[| P \<turnstile> Path last Cs to C via Cs'; Ds = Cs@pCs' |]
  ==> P,E \<turnstile> ⟨(|C|)),(ref (a,Cs)), s⟩ -> ⟨ref (a,Ds), s⟩"

| RedStaticDownCast:
  "P,E \<turnstile> ⟨(|C|)),(ref (a,Cs@[C]@Cs')), s⟩ -> ⟨ref (a,Cs@[C]), s⟩"

| RedStaticCastFail:
  "[|C ∉ set Cs; ¬ P \<turnstile> (last Cs) \<preceq>* C|]
  ==> P,E \<turnstile> ⟨(|C|)),(ref (a,Cs)), s⟩ -> ⟨THROW ClassCast, s⟩"

| DynCastRed:
  "P,E \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P,E \<turnstile> ⟨Cast C e, s⟩ -> ⟨Cast C e', s'⟩"

| RedDynCastNull:
  "P,E \<turnstile> ⟨Cast C null, s⟩ -> ⟨null,s⟩"

| RedStaticUpDynCast: (* path uniqueness not necessary for type proof but for determinism *)
  "[| P \<turnstile> Path last Cs to C unique; P \<turnstile> Path last Cs to C via Cs'; Ds = Cs@pCs' |]
  ==> P,E \<turnstile> ⟨Cast C(ref(a,Cs)),s⟩ -> ⟨ref(a,Ds),s⟩"

| RedStaticDownDynCast:
  "P,E \<turnstile> ⟨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 \<turnstile> Path D to C via Cs';
    P \<turnstile> Path D to C unique |]
  ==> P,E \<turnstile> ⟨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 \<turnstile> Path D to C unique;
    ¬ P \<turnstile> Path last Cs to C unique; C ∉ set Cs |]
  ==> P,E \<turnstile> ⟨Cast C (ref (a,Cs)), s⟩ -> ⟨null, s⟩"

| BinOpRed1:
  "P,E \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P,E \<turnstile> ⟨e «bop» e2, s⟩ -> ⟨e' «bop» e2, s'⟩"

| BinOpRed2:
  "P,E \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P,E \<turnstile> ⟨(Val v1) «bop» e, s⟩ -> ⟨(Val v1) «bop» e', s'⟩"

| RedBinOp:
  "binop(bop,v1,v2) = Some v ==>
  P,E \<turnstile> ⟨(Val v1) «bop» (Val v2), s⟩ -> ⟨Val v,s⟩"

| RedVar:
  "lcl s V = Some v ==>
  P,E \<turnstile> ⟨Var V,s⟩ -> ⟨Val v,s⟩"

| LAssRed:
  "P,E \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P,E \<turnstile> ⟨V:=e,s⟩ -> ⟨V:=e',s'⟩"

| RedLAss:
  "[|E V = Some T; P \<turnstile> T casts v to v'|] ==> 
  P,E \<turnstile> ⟨V:=(Val v),(h,l)⟩ -> ⟨Val v',(h,l(V\<mapsto>v'))⟩"

| FAccRed:
  "P,E \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P,E \<turnstile> ⟨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 \<turnstile> ⟨(ref (a,Cs'))•F{Cs}, s⟩ -> ⟨Val v,s⟩"

| RedFAccNull:
  "P,E \<turnstile> ⟨null•F{Cs}, s⟩ -> ⟨THROW NullPointer, s⟩"

| FAssRed1:
  "P,E \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P,E \<turnstile> ⟨e•F{Cs}:=e2, s⟩ -> ⟨e'•F{Cs}:=e2, s'⟩"

| FAssRed2:
  "P,E \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
   P,E \<turnstile> ⟨Val v•F{Cs}:=e, s⟩ -> ⟨Val v•F{Cs}:=e', s'⟩"

| RedFAss:
"[|h a = Some(D,S); P \<turnstile> (last Cs') has least F:T via Cs;
  P \<turnstile> T casts v to v'; Ds = Cs'@pCs; (Ds,fs) ∈ S|] ==>
  P,E \<turnstile> ⟨(ref (a,Cs'))•F{Cs}:=(Val v), (h,l)⟩ -> ⟨Val v', (h(a \<mapsto> (D,insert (Ds,fs(F\<mapsto>v')) (S - {(Ds,fs)}))),l)⟩"

| RedFAssNull:
  "P,E \<turnstile> ⟨null•F{Cs}:=Val v, s⟩ -> ⟨THROW NullPointer, s⟩"

| CallObj:
  "P,E \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P,E \<turnstile> ⟨Call e Copt M es,s⟩ -> ⟨Call e' Copt M es,s'⟩"

| CallParams:
  "P,E \<turnstile> ⟨es,s⟩ [->] ⟨es',s'⟩ ==>
   P,E \<turnstile> ⟨Call (Val v) Copt M es,s⟩ -> ⟨Call (Val v) Copt M es',s'⟩"

| RedCall:
  "[| hp s a = Some(C,S); P \<turnstile> last Cs has least M = (Ts',T',pns',body') via Ds;
    P \<turnstile> (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 \<turnstile> ⟨(ref (a,Cs))•M(map Val vs), s⟩ -> ⟨new_body, s⟩"

| RedStaticCall:
  "[| P \<turnstile> Path (last Cs) to C unique; P \<turnstile> Path (last Cs) to C via Cs'';
    P \<turnstile> C has least M = (Ts,T,pns,body) via Cs'; Ds = (Cs@pCs'')@pCs';
    size vs = size pns; size Ts = size pns |]
  ==> P,E \<turnstile> ⟨(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 \<turnstile> ⟨Call null Copt M (map Val vs),s⟩ -> ⟨THROW NullPointer,s⟩"

| BlockRedNone:
  "[| P,E(V \<mapsto> T) \<turnstile> ⟨e, (h,l(V:=None))⟩ -> ⟨e', (h',l')⟩; l' V = None; ¬ assigned V e |]
  ==> P,E \<turnstile> ⟨{V:T; e}, (h,l)⟩ -> ⟨{V:T; e'}, (h',l'(V := l V))⟩"

| BlockRedSome:
  "[| P,E(V \<mapsto> T) \<turnstile> ⟨e, (h,l(V:=None))⟩ -> ⟨e', (h',l')⟩; l' V = Some v;
     ¬ assigned V e |]
  ==> P,E \<turnstile> ⟨{V:T; e}, (h,l)⟩ -> ⟨{V:T := Val v; e'}, (h',l'(V := l V))⟩"

| InitBlockRed:
  "[| P,E(V \<mapsto> T) \<turnstile> ⟨e, (h,l(V\<mapsto>v'))⟩ -> ⟨e', (h',l')⟩; l' V = Some v''; 
     P \<turnstile> T casts v to v' |]
  ==> P,E \<turnstile> ⟨{V:T := Val v; e}, (h,l)⟩ -> ⟨{V:T := Val v''; e'}, (h',l'(V := l V))⟩"

| RedBlock:
  "P,E \<turnstile> ⟨{V:T; Val u}, s⟩ -> ⟨Val u, s⟩"

| RedInitBlock:
  "P \<turnstile> T casts v to v' ==> P,E \<turnstile> ⟨{V:T := Val v; Val u}, s⟩ -> ⟨Val u, s⟩"

| SeqRed:
  "P,E \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P,E \<turnstile> ⟨e;;e2, s⟩ -> ⟨e';;e2, s'⟩"

| RedSeq:
  "P,E \<turnstile> ⟨(Val v);;e2, s⟩ -> ⟨e2, s⟩"

| CondRed:
  "P,E \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P,E \<turnstile> ⟨if (e) e1 else e2, s⟩ -> ⟨if (e') e1 else e2, s'⟩"

| RedCondT:
  "P,E \<turnstile> ⟨if (true) e1 else e2, s⟩ -> ⟨e1, s⟩"

| RedCondF:
  "P,E \<turnstile> ⟨if (false) e1 else e2, s⟩ -> ⟨e2, s⟩"

| RedWhile:
  "P,E \<turnstile> ⟨while(b) c, s⟩ -> ⟨if(b) (c;;while(b) c) else unit, s⟩"

| ThrowRed:
  "P,E \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P,E \<turnstile> ⟨throw e, s⟩ -> ⟨throw e', s'⟩"

| RedThrowNull:
  "P,E \<turnstile> ⟨throw null, s⟩ -> ⟨THROW NullPointer, s⟩"

| ListRed1:
  "P,E \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==>
  P,E \<turnstile> ⟨e#es,s⟩ [->] ⟨e'#es,s'⟩"

| ListRed2:
  "P,E \<turnstile> ⟨es,s⟩ [->] ⟨es',s'⟩ ==>
  P,E \<turnstile> ⟨Val v # es,s⟩ [->] ⟨Val v # es',s'⟩"

-- "Exception propagation"

| DynCastThrow: "P,E \<turnstile> ⟨Cast C (Throw r), s⟩ -> ⟨Throw r, s⟩"
| StaticCastThrow: "P,E \<turnstile> ⟨(|C|)),(Throw r), s⟩ -> ⟨Throw r, s⟩"
| BinOpThrow1: "P,E \<turnstile> ⟨(Throw r) «bop» e2, s⟩ -> ⟨Throw r, s⟩"
| BinOpThrow2: "P,E \<turnstile> ⟨(Val v1) «bop» (Throw r), s⟩ -> ⟨Throw r, s⟩"
| LAssThrow: "P,E \<turnstile> ⟨V:=(Throw r), s⟩ -> ⟨Throw r, s⟩"
| FAccThrow: "P,E \<turnstile> ⟨(Throw r)•F{Cs}, s⟩ -> ⟨Throw r, s⟩"
| FAssThrow1: "P,E \<turnstile> ⟨(Throw r)•F{Cs}:=e2, s⟩ -> ⟨Throw r,s⟩"
| FAssThrow2: "P,E \<turnstile> ⟨Val v•F{Cs}:=(Throw r), s⟩ -> ⟨Throw r, s⟩"
| CallThrowObj: "P,E \<turnstile> ⟨Call (Throw r) Copt M es, s⟩ -> ⟨Throw r, s⟩"
| CallThrowParams: "[| es = map Val vs @ Throw r # es' |] 
  ==> P,E \<turnstile> ⟨Call (Val v) Copt M es, s⟩ -> ⟨Throw r, s⟩"
| BlockThrow: "P,E \<turnstile> ⟨{V:T; Throw r}, s⟩ -> ⟨Throw r, s⟩"
| InitBlockThrow: "P \<turnstile> T casts v to v' 
  ==> P,E \<turnstile> ⟨{V:T := Val v; Throw r}, s⟩ -> ⟨Throw r, s⟩"
| SeqThrow: "P,E \<turnstile> ⟨(Throw r);;e2, s⟩ -> ⟨Throw r, s⟩"
| CondThrow: "P,E \<turnstile> ⟨if (Throw r) e1 else e2, s⟩ -> ⟨Throw r, s⟩"
| ThrowThrow: "P,E \<turnstile> ⟨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 \<turnstile> ⟨V:=e,s⟩ -> ⟨e',s'⟩"
 "P,E \<turnstile> ⟨e1;;e2,s⟩ -> ⟨e',s'⟩"

declare Cons_eq_map_conv [iff]

lemma "P,E \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩ ==> True"
and reds_length:"P,E \<turnstile> ⟨es,s⟩ [->] ⟨es',s'⟩ ==> length es = length es'"
by (induct rule: red_reds.inducts) auto


section{* The reflexive transitive closure *}

consts
  Red ::  "prog => env => ((expr      × state) × (expr      × state)) set"
  Reds :: "prog => env => ((expr list × state) × (expr list × state)) set"

defs
  Red_def: "Red P E ≡  {((e,s),e',s'). P,E \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩}"
  Reds_def:"Reds P E ≡ {((es,s),es',s'). P,E \<turnstile> ⟨es,s⟩ [->] ⟨es',s'⟩}"

lemma[simp]: "((e,s),e',s') ∈ Red P E = P,E \<turnstile> ⟨e,s⟩ -> ⟨e',s'⟩"
by (simp add:Red_def)

lemma[simp]: "((es,s),es',s') ∈ Reds P E = P,E \<turnstile> ⟨es,s⟩ [->] ⟨es',s'⟩"
by (simp add:Reds_def)



abbreviation
  Step :: "prog => env => expr => state => expr => state => bool"
          ("_,_ \<turnstile> ((1⟨_,/_⟩) ->*/ (1⟨_,/_⟩))" [51,0,0,0,0] 81) where
  "P,E \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ≡ ((e,s), e',s') ∈ (Red P E)*"

abbreviation
  Steps :: "prog => env => expr list => state => expr list => state => bool"
          ("_,_ \<turnstile> ((1⟨_,/_⟩) [->]*/ (1⟨_,/_⟩))" [51,0,0,0,0] 81) where
  "P,E \<turnstile> ⟨es,s⟩ [->]* ⟨es',s'⟩ ≡ ((es,s), es',s') ∈ (Reds P E)*"


lemma converse_rtrancl_induct_red[consumes 1]:
assumes "P,E \<turnstile> ⟨e,(h,l)⟩ ->* ⟨e',(h',l')⟩"
and "!!e h l. R e h l e h l"
and "!!e0 h0 l0 e1 h1 l1 e' h' l'.
       [| P,E \<turnstile> ⟨e0,(h0,l0)⟩ -> ⟨e1,(h1,l1)⟩; R e1 h1 l1 e' h' l' |] ==> R e0 h0 l0 e' h' l'"
shows "R e h l e' h' l'"

proof -
  { fix s s'
    assume reds: "P,E \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩"
       and base: "!!e s. R e (hp s) (lcl s) e (hp s) (lcl s)"
       and IH: "!!e0 s0 e1 s1 e' s'.
           [| P,E \<turnstile> ⟨e0,s0⟩ -> ⟨e1,s1⟩; R e1 (hp s1) (lcl s1) e' (hp s') (lcl s') |]
           ==> R e0 (hp s0) (lcl s0) 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 e0 s0 e s)
      have Red:"((e0,s0),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 prems show ?thesis by fastsimp
qed



lemma steps_length:"P,E \<turnstile> ⟨es,s⟩ [->]* ⟨es',s'⟩ ==> length es = length es'"
by(induct rule:rtrancl_induct2,auto intro:reds_length)


section{*Some easy lemmas*}

lemma [iff]: "¬ P,E \<turnstile> ⟨[],s⟩ [->] ⟨es',s'⟩"
by(blast elim: reds.cases)

lemma [iff]: "¬ P,E \<turnstile> ⟨Val v,s⟩ -> ⟨e',s'⟩"
by(fastsimp elim: red.cases)

lemma [iff]: "¬ P,E \<turnstile> ⟨Throw r,s⟩ -> ⟨e',s'⟩"
by(fastsimp elim: red.cases)


lemma red_lcl_incr: "P,E \<turnstile> ⟨e,(h0,l0)⟩ -> ⟨e',(h1,l1)⟩ ==> dom l0 ⊆ dom l1"
and "P,E \<turnstile> ⟨es,(h0,l0)⟩ [->] ⟨es',(h1,l1)⟩ ==> dom l0 ⊆ dom l1"
by (induct rule: red_reds_inducts) (auto simp del:fun_upd_apply)


lemma red_lcl_add: "P,E \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',(h',l')⟩ ==> (!!l0. P,E \<turnstile> ⟨e,(h,l0++l)⟩ -> ⟨e',(h',l0++l')⟩)"
and "P,E \<turnstile> ⟨es,(h,l)⟩ [->] ⟨es',(h',l')⟩ ==> (!!l0. P,E \<turnstile> ⟨es,(h,l0++l)⟩ [->] ⟨es',(h',l0++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(fastsimp intro:red_reds.intros)
next
  case RedStaticUpDynCast thus ?case by(fastsimp intro:red_reds.intros)
next
  case RedStaticDownDynCast thus ?case by(fastsimp intro:red_reds.intros)
next
  case RedDynCast thus ?case by(fastsimp intro:red_reds.intros)
next
  case RedDynCastFail thus ?case by(fastsimp intro:red_reds.intros)
next
  case RedFAcc thus ?case by(fastsimp intro:red_reds.intros)
next
  case RedFAss thus ?case by (fastsimp intro:red_reds.intros)
next
  case RedCall thus ?case by (fastsimp intro!:red_reds.RedCall)
next
  case RedStaticCall thus ?case by(fastsimp intro:red_reds.intros)
next
  case (InitBlockRed E V T e h l v' e' h' l' v'' v l0)
  have IH: "!!l0. P,E(V \<mapsto> T) \<turnstile> ⟨e,(h, l0 ++ l(V \<mapsto> v'))⟩ -> ⟨e',(h', l0 ++ l')⟩"
    and l'V: "l' V = Some v''" and casts:"P \<turnstile> T casts v to v'" by fact+
  from IH have IH': "P,E(V \<mapsto> T) \<turnstile> ⟨e,(h, (l0 ++ l)(V \<mapsto> v'))⟩ -> ⟨e',(h',l0 ++ l')⟩"
    by simp
  have "(l0 ++ l')(V := (l0 ++ l) V) = l0 ++ l'(V := l V)"
    by(rule ext)(simp add:map_add_def)
  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' l0)
  have IH: "!!l0. P,E(V \<mapsto> T) \<turnstile> ⟨e,(h, l0 ++ l(V := None))⟩ -> ⟨e',(h', l0 ++ l')⟩"
    and l'V: "l' V = None" and unass: "¬ assigned V e" by fact+
  have "l0(V := None) ++ l(V := None) = (l0 ++ l)(V := None)"
    by(simp add:expand_fun_eq map_add_def)
  hence IH': "P,E(V \<mapsto> T) \<turnstile> ⟨e,(h, (l0++l)(V := None))⟩ -> ⟨e',(h', l0(V := None) ++ l')⟩"
    using IH[of "l0(V := None)"] by simp
  have "(l0(V := None) ++ l')(V := (l0 ++ l) V) = l0 ++ l'(V := l V)"
    by(simp add:expand_fun_eq map_add_def)
  with red_reds.BlockRedNone[OF IH' _ unass] l'V show ?case
    by(simp add: map_add_def)
next
  case (BlockRedSome E V T e h l e' h' l' v l0)
  have IH: "!!l0. P,E(V \<mapsto> T) \<turnstile> ⟨e,(h, l0 ++ l(V := None))⟩ -> ⟨e',(h', l0 ++ l')⟩"
    and l'V: "l' V = Some v" and unass: "¬ assigned V e" by fact+
  have "l0(V := None) ++ l(V := None) = (l0 ++ l)(V := None)"
    by(simp add:expand_fun_eq map_add_def)
  hence IH': "P,E(V \<mapsto> T) \<turnstile> ⟨e,(h, (l0++l)(V := None))⟩ -> ⟨e',(h', l0(V := None) ++ l')⟩"
    using IH[of "l0(V := None)"] by simp
  have "(l0(V := None) ++ l')(V := (l0 ++ l) V) = l0 ++ l'(V := l V)"
    by(simp add:expand_fun_eq map_add_def)
  with red_reds.BlockRedSome[OF IH' _ unass] l'V show ?case
    by(simp add:map_add_def)
next
qed (simp_all add:red_reds.intros)



lemma Red_lcl_add:
assumes "P,E \<turnstile> ⟨e,(h,l)⟩ ->* ⟨e',(h',l')⟩" shows "P,E \<turnstile> ⟨e,(h,l0++l)⟩ ->* ⟨e',(h',l0++l')⟩"

using prems
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 \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',(h',l')⟩; h a = Some(D,S)|] 
  ==> ∃S'. h' a = Some(D,S')"
and reds_preserves_obj:"[|P,E \<turnstile> ⟨es,(h,l)⟩ [->] ⟨es',(h',l')⟩; h a = Some(D,S)|] 
  ==> ∃S'. h' a = Some(D,S')"
by (induct rule:red_reds_inducts) (auto dest:new_Addr_SomeD)

end