# 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:
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)"

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

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

lemma [iff]: "finals []"

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

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(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(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'))"