Theory BigStep

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

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

section ‹Big Step Semantics›

theory BigStep
imports Syntax State
begin


subsection ‹The rules›

inductive
  eval :: "prog ⇒ env ⇒ expr ⇒ state ⇒ expr ⇒ state ⇒ bool"
          ("_,_ ⊢ ((1⟨_,/_⟩) ⇒/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  and evals :: "prog ⇒ env ⇒ expr list ⇒ state ⇒ expr list ⇒ state ⇒ bool"
           ("_,_ ⊢ ((1⟨_,/_⟩) [⇒]/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  for P :: prog
where

  New:
  "⟦ 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)⟩"

| NewFail:
  "new_Addr h = None ⟹
  P,E ⊢ ⟨new C, (h,l)⟩ ⇒ ⟨THROW OutOfMemory,(h,l)⟩"

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

| StaticDownCast:
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a,Cs@[C]@Cs'),s⇩1⟩
   ⟹ P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒ ⟨ref (a,Cs@[C]),s⇩1⟩"

| StaticCastNull:
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩ ⟹
  P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩"

| StaticCastFail:
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a,Cs),s⇩1⟩; ¬ P ⊢ (last Cs) ≼⇧* C; C ∉ set Cs ⟧
  ⟹ P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒ ⟨THROW ClassCast,s⇩1⟩"

| StaticCastThrow:
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
  P,E ⊢ ⟨⦇C⦈e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

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

| StaticDownDynCast:
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a,Cs@[C]@Cs'),s⇩1⟩
   ⟹ P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨ref (a,Cs@[C]),s⇩1⟩"

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

| DynCastNull:
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩ ⟹
  P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩"

| DynCastFail: (* fourth premise not necessary for type proof but for determinism *)
  "⟦ P,E ⊢ ⟨e,s⇩0⟩⇒ ⟨ref (a,Cs),(h,l)⟩; h a = Some(D,S); ¬ P ⊢ Path D to C unique;
    ¬ P ⊢ Path last Cs to C unique; C ∉ set Cs ⟧
  ⟹ P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨null,(h,l)⟩"

| DynCastThrow:
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
  P,E ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

| Val:
  "P,E ⊢ ⟨Val v,s⟩ ⇒ ⟨Val v,s⟩"

| BinOp:
  "⟦ P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val v⇩1,s⇩1⟩; P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨Val v⇩2,s⇩2⟩; 
    binop(bop,v⇩1,v⇩2) = Some v ⟧
  ⟹ P,E ⊢ ⟨e⇩1 «bop» e⇩2,s⇩0⟩⇒⟨Val v,s⇩2⟩"

| BinOpThrow1:
  "P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨throw e,s⇩1⟩ ⟹
  P,E ⊢ ⟨e⇩1 «bop» e⇩2, s⇩0⟩ ⇒ ⟨throw e,s⇩1⟩"

| BinOpThrow2:
  "⟦ P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val v⇩1,s⇩1⟩; P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨throw e,s⇩2⟩ ⟧
  ⟹ P,E ⊢ ⟨e⇩1 «bop» e⇩2,s⇩0⟩ ⇒ ⟨throw e,s⇩2⟩"

| Var:
  "l V = Some v ⟹
  P,E ⊢ ⟨Var V,(h,l)⟩ ⇒ ⟨Val v,(h,l)⟩"

| LAss:
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨Val v,(h,l)⟩; E V = Some T;
     P ⊢ T casts v to v'; l' = l(V↦v') ⟧
  ⟹ P,E ⊢ ⟨V:=e,s⇩0⟩ ⇒ ⟨Val v',(h,l')⟩"

| LAssThrow:
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
  P,E ⊢ ⟨V:=e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

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

| FAccNull:
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩ ⟹
  P,E ⊢ ⟨e∙F{Cs},s⇩0⟩ ⇒ ⟨THROW NullPointer,s⇩1⟩" 

| FAccThrow:
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
  P,E ⊢ ⟨e∙F{Cs},s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

| FAss:
  "⟦ P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨ref (a,Cs'),s⇩1⟩; P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨Val v,(h⇩2,l⇩2)⟩;
     h⇩2 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; fs' = fs(F↦v'); 
     S' = S - {(Ds,fs)} ∪ {(Ds,fs')}; h⇩2' = h⇩2(a↦(D,S'))⟧
  ⟹ P,E ⊢ ⟨e⇩1∙F{Cs}:=e⇩2,s⇩0⟩ ⇒ ⟨Val v',(h⇩2',l⇩2)⟩"

| FAssNull:
  "⟦ P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨null,s⇩1⟩;  P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨Val v,s⇩2⟩ ⟧ ⟹
  P,E ⊢ ⟨e⇩1∙F{Cs}:=e⇩2,s⇩0⟩ ⇒ ⟨THROW NullPointer,s⇩2⟩" 

| FAssThrow1:
  "P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
  P,E ⊢ ⟨e⇩1∙F{Cs}:=e⇩2,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

| FAssThrow2:
  "⟦ P,E ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val v,s⇩1⟩; P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨throw e',s⇩2⟩ ⟧
  ⟹ P,E ⊢ ⟨e⇩1∙F{Cs}:=e⇩2,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"

| CallObjThrow:
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
  P,E ⊢ ⟨Call e Copt M es,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

| CallParamsThrow:
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨Val v,s⇩1⟩; P,E ⊢ ⟨es,s⇩1⟩ [⇒] ⟨map Val vs @ throw ex # es',s⇩2⟩ ⟧
   ⟹ P,E ⊢ ⟨Call e Copt M es,s⇩0⟩ ⇒ ⟨throw ex,s⇩2⟩"

| Call:
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a,Cs),s⇩1⟩;  P,E ⊢ ⟨ps,s⇩1⟩ [⇒] ⟨map Val vs,(h⇩2,l⇩2)⟩;
     h⇩2 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'; length vs = length pns; 
     P ⊢ Ts Casts vs to vs'; l⇩2' = [this↦Ref (a,Cs'), pns[↦]vs'];
     new_body = (case T' of Class D ⇒ ⦇D⦈body   | _  ⇒ body);  
     P,E(this↦Class(last Cs'), pns[↦]Ts) ⊢ ⟨new_body,(h⇩2,l⇩2')⟩ ⇒ ⟨e',(h⇩3,l⇩3)⟩ ⟧
  ⟹ P,E ⊢ ⟨e∙M(ps),s⇩0⟩ ⇒ ⟨e',(h⇩3,l⇩2)⟩"

| StaticCall:
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref (a,Cs),s⇩1⟩;  P,E ⊢ ⟨ps,s⇩1⟩ [⇒] ⟨map Val vs,(h⇩2,l⇩2)⟩;
     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';
     length vs = length pns; P ⊢ Ts Casts vs to vs'; 
     l⇩2' = [this↦Ref (a,Ds), pns[↦]vs'];
     P,E(this↦Class(last Ds), pns[↦]Ts) ⊢ ⟨body,(h⇩2,l⇩2')⟩ ⇒ ⟨e',(h⇩3,l⇩3)⟩ ⟧
  ⟹ P,E ⊢ ⟨e∙(C::)M(ps),s⇩0⟩ ⇒ ⟨e',(h⇩3,l⇩2)⟩"

| CallNull:
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩;  P,E ⊢ ⟨es,s⇩1⟩ [⇒] ⟨map Val vs,s⇩2⟩ ⟧
  ⟹ P,E ⊢ ⟨Call e Copt M es,s⇩0⟩ ⇒ ⟨THROW NullPointer,s⇩2⟩"

| Block:
  "⟦P,E(V ↦ T) ⊢ ⟨e⇩0,(h⇩0,l⇩0(V:=None))⟩ ⇒ ⟨e⇩1,(h⇩1,l⇩1)⟩ ⟧ ⟹
  P,E ⊢ ⟨{V:T; e⇩0},(h⇩0,l⇩0)⟩ ⇒ ⟨e⇩1,(h⇩1,l⇩1(V:=l⇩0 V))⟩"

| Seq:
  "⟦ P,E ⊢ ⟨e⇩0,s⇩0⟩ ⇒ ⟨Val v,s⇩1⟩; P,E ⊢ ⟨e⇩1,s⇩1⟩ ⇒ ⟨e⇩2,s⇩2⟩ ⟧
  ⟹ P,E ⊢ ⟨e⇩0;;e⇩1,s⇩0⟩ ⇒ ⟨e⇩2,s⇩2⟩"

| SeqThrow:
  "P,E ⊢ ⟨e⇩0,s⇩0⟩ ⇒ ⟨throw e,s⇩1⟩ ⟹
  P,E ⊢ ⟨e⇩0;;e⇩1,s⇩0⟩⇒⟨throw e,s⇩1⟩"

| CondT:
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨true,s⇩1⟩; P,E ⊢ ⟨e⇩1,s⇩1⟩ ⇒ ⟨e',s⇩2⟩ ⟧
  ⟹ P,E ⊢ ⟨if (e) e⇩1 else e⇩2,s⇩0⟩ ⇒ ⟨e',s⇩2⟩"

| CondF:
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨false,s⇩1⟩; P,E ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨e',s⇩2⟩ ⟧
  ⟹ P,E ⊢ ⟨if (e) e⇩1 else e⇩2,s⇩0⟩ ⇒ ⟨e',s⇩2⟩"

| CondThrow:
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
  P,E ⊢ ⟨if (e) e⇩1 else e⇩2, s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

| WhileF:
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨false,s⇩1⟩ ⟹
  P,E ⊢ ⟨while (e) c,s⇩0⟩ ⇒ ⟨unit,s⇩1⟩"

| WhileT:
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨true,s⇩1⟩; P,E ⊢ ⟨c,s⇩1⟩ ⇒ ⟨Val v⇩1,s⇩2⟩; 
     P,E ⊢ ⟨while (e) c,s⇩2⟩ ⇒ ⟨e⇩3,s⇩3⟩ ⟧
  ⟹ P,E ⊢ ⟨while (e) c,s⇩0⟩ ⇒ ⟨e⇩3,s⇩3⟩"

| WhileCondThrow:
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ throw e',s⇩1⟩ ⟹
  P,E ⊢ ⟨while (e) c,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

| WhileBodyThrow:
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨true,s⇩1⟩; P,E ⊢ ⟨c,s⇩1⟩ ⇒ ⟨throw e',s⇩2⟩⟧
  ⟹ P,E ⊢ ⟨while (e) c,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"

| Throw:
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨ref r,s⇩1⟩ ⟹
  P,E ⊢ ⟨throw e,s⇩0⟩ ⇒ ⟨Throw r,s⇩1⟩"

| ThrowNull:
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩ ⟹
  P,E ⊢ ⟨throw e,s⇩0⟩ ⇒ ⟨THROW NullPointer,s⇩1⟩"

| ThrowThrow:
  "P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
  P,E ⊢ ⟨throw e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

| Nil:
  "P,E ⊢ ⟨[],s⟩ [⇒] ⟨[],s⟩"

| Cons:
  "⟦ P,E ⊢ ⟨e,s⇩0⟩ ⇒ ⟨Val v,s⇩1⟩; P,E ⊢ ⟨es,s⇩1⟩ [⇒] ⟨es',s⇩2⟩ ⟧
  ⟹ P,E ⊢ ⟨e#es,s⇩0⟩ [⇒] ⟨Val v # es',s⇩2⟩"

| ConsThrow:
  "P,E ⊢ ⟨e, s⇩0⟩ ⇒ ⟨throw e', s⇩1⟩ ⟹
  P,E ⊢ ⟨e#es, s⇩0⟩ [⇒] ⟨throw e' # es, s⇩1⟩"

lemmas eval_evals_induct = eval_evals.induct [split_format (complete)]
  and eval_evals_inducts = eval_evals.inducts [split_format (complete)]

inductive_cases eval_cases [cases set]:
 "P,E ⊢ ⟨new C,s⟩ ⇒ ⟨e',s'⟩"
 "P,E ⊢ ⟨Cast C e,s⟩ ⇒ ⟨e',s'⟩"
 "P,E ⊢ ⟨⦇C⦈e,s⟩ ⇒ ⟨e',s'⟩"
 "P,E ⊢ ⟨Val v,s⟩ ⇒ ⟨e',s'⟩"
 "P,E ⊢ ⟨e⇩1 «bop» e⇩2,s⟩ ⇒ ⟨e',s'⟩"
 "P,E ⊢ ⟨Var V,s⟩ ⇒ ⟨e',s'⟩"
 "P,E ⊢ ⟨V:=e,s⟩ ⇒ ⟨e',s'⟩"
 "P,E ⊢ ⟨e∙F{Cs},s⟩ ⇒ ⟨e',s'⟩"
 "P,E ⊢ ⟨e⇩1∙F{Cs}:=e⇩2,s⟩ ⇒ ⟨e',s'⟩"
 "P,E ⊢ ⟨e∙M(es),s⟩ ⇒ ⟨e',s'⟩"
 "P,E ⊢ ⟨e∙(C::)M(es),s⟩ ⇒ ⟨e',s'⟩"
 "P,E ⊢ ⟨{V:T;e⇩1},s⟩ ⇒ ⟨e',s'⟩"
 "P,E ⊢ ⟨e⇩1;;e⇩2,s⟩ ⇒ ⟨e',s'⟩"
 "P,E ⊢ ⟨if (e) e⇩1 else e⇩2,s⟩ ⇒ ⟨e',s'⟩"
 "P,E ⊢ ⟨while (b) c,s⟩ ⇒ ⟨e',s'⟩"
 "P,E ⊢ ⟨throw e,s⟩ ⇒ ⟨e',s'⟩"
  
inductive_cases evals_cases [cases set]:
 "P,E ⊢ ⟨[],s⟩ [⇒] ⟨e',s'⟩"
 "P,E ⊢ ⟨e#es,s⟩ [⇒] ⟨e',s'⟩"



subsection ‹Final expressions›

definition final :: "expr ⇒ bool" where
  "final e  ≡  (∃v. e = Val v) ∨ (∃r. e = Throw r)"

definition finals:: "expr list ⇒ bool" where
  "finals es  ≡  (∃vs. es = map Val vs) ∨ (∃vs r es'. es = map Val vs @ Throw r # es')"

lemma [simp]: "final(Val v)"
by(simp add:final_def)

lemma [simp]: "final(throw e) = (∃r. e = ref r)"
by(simp add:final_def)

lemma finalE: "⟦ final e;  ⋀v. e = Val v ⟹ Q;  ⋀r. e = Throw r ⟹ Q ⟧ ⟹ Q"
by(auto simp:final_def)

lemma [iff]: "finals []"
by(simp add:finals_def)

lemma [iff]: "finals (Val v # es) = finals es"

apply(clarsimp simp add:finals_def)
apply(rule iffI)
 apply(erule disjE)
  apply simp
 apply(rule disjI2)
 apply clarsimp
 apply(case_tac vs)
  apply simp
 apply fastforce
apply(erule disjE)
 apply (rule disjI1)
 apply clarsimp
apply(rule disjI2)
apply clarsimp
apply(rule_tac x = "v#vs" in exI)
apply simp
done


lemma finals_app_map[iff]: "finals (map Val vs @ es) = finals es"
by(induct_tac vs, auto)

lemma [iff]: "finals (map Val vs)"
using finals_app_map[of vs "[]"]by(simp)

lemma [iff]: "finals (throw e # es) = (∃r. e = ref r)"

apply(simp add:finals_def)
apply(rule iffI)
 apply clarsimp
 apply(case_tac vs)
  apply simp
 apply fastforce
apply fastforce
done


lemma not_finals_ConsI: "¬ final e ⟹ ¬ finals(e#es)"
 
apply(auto simp add:finals_def final_def)
apply(case_tac vs)
apply auto
done


lemma eval_final: "P,E ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩ ⟹ final e'"
 and evals_final: "P,E ⊢ ⟨es,s⟩ [⇒] ⟨es',s'⟩ ⟹ finals es'"
by(induct rule:eval_evals.inducts, simp_all)


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


text‹Only used later, in the small to big translation, but is already a
good sanity check:›

lemma eval_finalId:  "final e ⟹ P,E ⊢ ⟨e,s⟩ ⇒ ⟨e,s⟩"
by (erule finalE) (fastforce intro: eval_evals.intros)+


lemma eval_finalsId:
assumes finals: "finals es" shows "P,E ⊢ ⟨es,s⟩ [⇒] ⟨es,s⟩"

  using finals
proof (induct es type: list)
  case Nil show ?case by (rule eval_evals.intros)
next
  case (Cons e es)
  have hyp: "finals es ⟹ P,E ⊢ ⟨es,s⟩ [⇒] ⟨es,s⟩"
   and finals: "finals (e # es)" by fact+
  show "P,E ⊢ ⟨e # es,s⟩ [⇒] ⟨e # es,s⟩"
  proof cases
    assume "final e"
    thus ?thesis
    proof (cases rule: finalE)
      fix v assume e: "e = Val v"
      have "P,E ⊢ ⟨Val v,s⟩ ⇒ ⟨Val v,s⟩" by (simp add: eval_finalId)
      moreover from finals e have "P,E ⊢ ⟨es,s⟩ [⇒] ⟨es,s⟩" by(fast intro:hyp)
      ultimately have "P,E ⊢ ⟨Val v#es,s⟩ [⇒] ⟨Val v#es,s⟩"
        by (rule eval_evals.intros)
      with e show ?thesis by simp
    next
      fix a assume e: "e = Throw a"
      have "P,E ⊢ ⟨Throw a,s⟩ ⇒ ⟨Throw a,s⟩" by (simp add: eval_finalId)
      hence "P,E ⊢ ⟨Throw a#es,s⟩ [⇒] ⟨Throw a#es,s⟩" by (rule eval_evals.intros)
      with e show ?thesis by simp
    qed
  next
    assume "¬ final e"
    with not_finals_ConsI finals have False by blast
    thus ?thesis ..
  qed
qed


lemma
eval_preserves_obj:"P,E ⊢ ⟨e,(h,l)⟩ ⇒ ⟨e',(h',l')⟩ ⟹ (⋀S. h a = Some(D,S) 
  ⟹ ∃S'. h' a = Some(D,S'))"
and evals_preserves_obj:"P,E ⊢ ⟨es,(h,l)⟩ [⇒] ⟨es',(h',l')⟩ 
⟹ (⋀S. h a = Some(D,S) ⟹ ∃S'. h' a = Some(D,S'))"
by(induct rule:eval_evals_inducts)(fastforce dest:new_Addr_SomeD)+

end