# Theory BigStep

```(*  Title:      JinjaDCI/J/BigStep.thy

Author:     Tobias Nipkow, Susannah Mansky
Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC

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

section ‹ Big Step Semantics ›

theory BigStep imports Expr State WWellForm begin

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

New:
"⟦ sh C = Some (sfs, Done); new_Addr h = Some a;
P ⊢ C has_fields FDTs; h' = h(a↦blank P C) ⟧
⟹ P ⊢ ⟨new C,(h,l,sh)⟩ ⇒ ⟨addr a,(h',l,sh)⟩"

| NewFail:
"⟦ sh C = Some (sfs, Done); new_Addr h = None; is_class P C ⟧ ⟹
P ⊢ ⟨new C, (h,l,sh)⟩ ⇒ ⟨THROW OutOfMemory,(h,l,sh)⟩"

| NewInit:
"⟦ ∄sfs. sh C = Some (sfs, Done); P ⊢ ⟨INIT C ([C],False) ← unit,(h,l,sh)⟩ ⇒ ⟨Val v',(h',l',sh')⟩;
new_Addr h' = Some a; P ⊢ C has_fields FDTs; h'' = h'(a↦blank P C) ⟧
⟹ P ⊢ ⟨new C,(h,l,sh)⟩ ⇒ ⟨addr a,(h'',l',sh')⟩"

| NewInitOOM:
"⟦ ∄sfs. sh C = Some (sfs, Done); P ⊢ ⟨INIT C ([C],False) ← unit,(h,l,sh)⟩ ⇒ ⟨Val v',(h',l',sh')⟩;
new_Addr h' = None; is_class P C ⟧
⟹ P ⊢ ⟨new C,(h,l,sh)⟩ ⇒ ⟨THROW OutOfMemory,(h',l',sh')⟩"

| NewInitThrow:
"⟦ ∄sfs. sh C = Some (sfs, Done); P ⊢ ⟨INIT C ([C],False) ← unit,(h,l,sh)⟩ ⇒ ⟨throw a,s'⟩;
is_class P C ⟧
⟹ P ⊢ ⟨new C,(h,l,sh)⟩ ⇒ ⟨throw a,s'⟩"

| Cast:
"⟦ P ⊢ ⟨e,s⇩0⟩ ⇒ ⟨addr a,(h,l,sh)⟩; h a = Some(D,fs); P ⊢ D ≼⇧* C ⟧
⟹ P ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨addr a,(h,l,sh)⟩"

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

| CastFail:
"⟦ P ⊢ ⟨e,s⇩0⟩⇒ ⟨addr a,(h,l,sh)⟩; h a = Some(D,fs); ¬ P ⊢ D ≼⇧* C ⟧
⟹ P ⊢ ⟨Cast C e,s⇩0⟩ ⇒ ⟨THROW ClassCast,(h,l,sh)⟩"

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

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

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

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

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

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

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

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

| FAcc:
"⟦ P ⊢ ⟨e,s⇩0⟩ ⇒ ⟨addr a,(h,l,sh)⟩; h a = Some(C,fs);
P ⊢ C has F,NonStatic:t in D;
fs(F,D) = Some v ⟧
⟹ P ⊢ ⟨e∙F{D},s⇩0⟩ ⇒ ⟨Val v,(h,l,sh)⟩"

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

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

| FAccNone:
"⟦ P ⊢ ⟨e,s⇩0⟩ ⇒ ⟨addr a,(h,l,sh)⟩; h a = Some(C,fs);
¬(∃b t. P ⊢ C has F,b:t in D) ⟧
⟹ P ⊢ ⟨e∙F{D},s⇩0⟩ ⇒ ⟨THROW NoSuchFieldError,(h,l,sh)⟩"

| FAccStatic:
"⟦ P ⊢ ⟨e,s⇩0⟩ ⇒ ⟨addr a,(h,l,sh)⟩; h a = Some(C,fs);
P ⊢ C has F,Static:t in D ⟧
⟹ P ⊢ ⟨e∙F{D},s⇩0⟩ ⇒ ⟨THROW IncompatibleClassChangeError,(h,l,sh)⟩"

| SFAcc:
"⟦ P ⊢ C has F,Static:t in D;
sh D = Some (sfs,Done);
sfs F = Some v ⟧
⟹ P ⊢ ⟨C∙⇩sF{D},(h,l,sh)⟩ ⇒ ⟨Val v,(h,l,sh)⟩"

| SFAccInit:
"⟦ P ⊢ C has F,Static:t in D;
∄sfs. sh D = Some (sfs,Done); P ⊢ ⟨INIT D ([D],False) ← unit,(h,l,sh)⟩ ⇒ ⟨Val v',(h',l',sh')⟩;
sh' D = Some (sfs,i);
sfs F = Some v ⟧
⟹ P ⊢ ⟨C∙⇩sF{D},(h,l,sh)⟩ ⇒ ⟨Val v,(h',l',sh')⟩"

| SFAccInitThrow:
"⟦ P ⊢ C has F,Static:t in D;
∄sfs. sh D = Some (sfs,Done); P ⊢ ⟨INIT D ([D],False) ← unit,(h,l,sh)⟩ ⇒ ⟨throw a,s'⟩ ⟧
⟹ P ⊢ ⟨C∙⇩sF{D},(h,l,sh)⟩ ⇒ ⟨throw a,s'⟩"

| SFAccNone:
"⟦ ¬(∃b t. P ⊢ C has F,b:t in D) ⟧
⟹ P ⊢ ⟨C∙⇩sF{D},s⟩ ⇒ ⟨THROW NoSuchFieldError,s⟩"

| SFAccNonStatic:
"⟦ P ⊢ C has F,NonStatic:t in D ⟧
⟹ P ⊢ ⟨C∙⇩sF{D},s⟩ ⇒ ⟨THROW IncompatibleClassChangeError,s⟩"

| FAss:
"⟦ P ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨addr a,s⇩1⟩; P ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨Val v,(h⇩2,l⇩2,sh⇩2)⟩;
h⇩2 a = Some(C,fs); P ⊢ C has F,NonStatic:t in D;
fs' = fs((F,D)↦v); h⇩2' = h⇩2(a↦(C,fs')) ⟧
⟹ P ⊢ ⟨e⇩1∙F{D}:=e⇩2,s⇩0⟩ ⇒ ⟨unit,(h⇩2',l⇩2,sh⇩2)⟩"

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

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

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

| FAssNone:
"⟦ P ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨addr a,s⇩1⟩; P ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨Val v,(h⇩2,l⇩2,sh⇩2)⟩;
h⇩2 a = Some(C,fs); ¬(∃b t. P ⊢ C has F,b:t in D) ⟧
⟹ P ⊢ ⟨e⇩1∙F{D}:=e⇩2,s⇩0⟩ ⇒ ⟨THROW NoSuchFieldError,(h⇩2,l⇩2,sh⇩2)⟩"

| FAssStatic:
"⟦ P ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨addr a,s⇩1⟩; P ⊢ ⟨e⇩2,s⇩1⟩ ⇒ ⟨Val v,(h⇩2,l⇩2,sh⇩2)⟩;
h⇩2 a = Some(C,fs); P ⊢ C has F,Static:t in D ⟧
⟹ P ⊢ ⟨e⇩1∙F{D}:=e⇩2,s⇩0⟩ ⇒ ⟨THROW IncompatibleClassChangeError,(h⇩2,l⇩2,sh⇩2)⟩"

| SFAss:
"⟦ P ⊢ ⟨e⇩2,s⇩0⟩ ⇒ ⟨Val v,(h⇩1,l⇩1,sh⇩1)⟩;
P ⊢ C has F,Static:t in D;
sh⇩1 D = Some(sfs,Done); sfs' = sfs(F↦v); sh⇩1' = sh⇩1(D↦(sfs',Done)) ⟧
⟹ P ⊢ ⟨C∙⇩sF{D}:=e⇩2,s⇩0⟩ ⇒ ⟨unit,(h⇩1,l⇩1,sh⇩1')⟩"

| SFAssInit:
"⟦ P ⊢ ⟨e⇩2,s⇩0⟩ ⇒ ⟨Val v,(h⇩1,l⇩1,sh⇩1)⟩;
P ⊢ C has F,Static:t in D;
∄sfs. sh⇩1 D = Some(sfs,Done); P ⊢ ⟨INIT D ([D],False) ← unit,(h⇩1,l⇩1,sh⇩1)⟩ ⇒ ⟨Val v',(h',l',sh')⟩;
sh' D = Some(sfs,i);
sfs' = sfs(F↦v); sh'' = sh'(D↦(sfs',i)) ⟧
⟹ P ⊢ ⟨C∙⇩sF{D}:=e⇩2,s⇩0⟩ ⇒ ⟨unit,(h',l',sh'')⟩"

| SFAssInitThrow:
"⟦ P ⊢ ⟨e⇩2,s⇩0⟩ ⇒ ⟨Val v,(h⇩1,l⇩1,sh⇩1)⟩;
P ⊢ C has F,Static:t in D;
∄sfs. sh⇩1 D = Some(sfs,Done); P ⊢ ⟨INIT D ([D],False) ← unit,(h⇩1,l⇩1,sh⇩1)⟩ ⇒ ⟨throw a,s'⟩ ⟧
⟹ P ⊢ ⟨C∙⇩sF{D}:=e⇩2,s⇩0⟩ ⇒ ⟨throw a,s'⟩"

| SFAssThrow:
"P ⊢ ⟨e⇩2,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩
⟹ P ⊢ ⟨C∙⇩sF{D}:=e⇩2,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"

| SFAssNone:
"⟦ P ⊢ ⟨e⇩2,s⇩0⟩ ⇒ ⟨Val v,(h⇩2,l⇩2,sh⇩2)⟩;
¬(∃b t. P ⊢ C has F,b:t in D) ⟧
⟹ P ⊢ ⟨C∙⇩sF{D}:=e⇩2,s⇩0⟩ ⇒ ⟨THROW NoSuchFieldError,(h⇩2,l⇩2,sh⇩2)⟩"

| SFAssNonStatic:
"⟦ P ⊢ ⟨e⇩2,s⇩0⟩ ⇒ ⟨Val v,(h⇩2,l⇩2,sh⇩2)⟩;
P ⊢ C has F,NonStatic:t in D ⟧
⟹ P ⊢ ⟨C∙⇩sF{D}:=e⇩2,s⇩0⟩ ⇒ ⟨THROW IncompatibleClassChangeError,(h⇩2,l⇩2,sh⇩2)⟩"

| CallObjThrow:
"P ⊢ ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P ⊢ ⟨e∙M(ps),s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

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

| CallNull:
"⟦ P ⊢ ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩;  P ⊢ ⟨ps,s⇩1⟩ [⇒] ⟨map Val vs,s⇩2⟩ ⟧
⟹ P ⊢ ⟨e∙M(ps),s⇩0⟩ ⇒ ⟨THROW NullPointer,s⇩2⟩"

| CallNone:
"⟦ P ⊢ ⟨e,s⇩0⟩ ⇒ ⟨addr a,s⇩1⟩;  P ⊢ ⟨ps,s⇩1⟩ [⇒] ⟨map Val vs,(h⇩2,l⇩2,sh⇩2)⟩;
h⇩2 a = Some(C,fs); ¬(∃b Ts T m D. P ⊢ C sees M,b:Ts→T = m in D) ⟧
⟹ P ⊢ ⟨e∙M(ps),s⇩0⟩ ⇒ ⟨THROW NoSuchMethodError,(h⇩2,l⇩2,sh⇩2)⟩"

| CallStatic:
"⟦ P ⊢ ⟨e,s⇩0⟩ ⇒ ⟨addr a,s⇩1⟩;  P ⊢ ⟨ps,s⇩1⟩ [⇒] ⟨map Val vs,(h⇩2,l⇩2,sh⇩2)⟩;
h⇩2 a = Some(C,fs); P ⊢ C sees M,Static:Ts→T = m in D ⟧
⟹ P ⊢ ⟨e∙M(ps),s⇩0⟩ ⇒ ⟨THROW IncompatibleClassChangeError,(h⇩2,l⇩2,sh⇩2)⟩"

| Call:
"⟦ P ⊢ ⟨e,s⇩0⟩ ⇒ ⟨addr a,s⇩1⟩;  P ⊢ ⟨ps,s⇩1⟩ [⇒] ⟨map Val vs,(h⇩2,l⇩2,sh⇩2)⟩;
h⇩2 a = Some(C,fs); P ⊢ C sees M,NonStatic:Ts→T = (pns,body) in D;
length vs = length pns;  l⇩2' = [this↦Addr a, pns[↦]vs];
P ⊢ ⟨body,(h⇩2,l⇩2',sh⇩2)⟩ ⇒ ⟨e',(h⇩3,l⇩3,sh⇩3)⟩ ⟧
⟹ P ⊢ ⟨e∙M(ps),s⇩0⟩ ⇒ ⟨e',(h⇩3,l⇩2,sh⇩3)⟩"

| SCallParamsThrow:
"⟦ P ⊢ ⟨es,s⇩0⟩ [⇒] ⟨map Val vs @ throw ex # es',s⇩2⟩ ⟧
⟹ P ⊢ ⟨C∙⇩sM(es),s⇩0⟩ ⇒ ⟨throw ex,s⇩2⟩"

| SCallNone:
"⟦ P ⊢ ⟨ps,s⇩0⟩ [⇒] ⟨map Val vs,s⇩2⟩;
¬(∃b Ts T m D. P ⊢ C sees M,b:Ts→T = m in D) ⟧
⟹ P ⊢ ⟨C∙⇩sM(ps),s⇩0⟩ ⇒ ⟨THROW NoSuchMethodError,s⇩2⟩"

| SCallNonStatic:
"⟦ P ⊢ ⟨ps,s⇩0⟩ [⇒] ⟨map Val vs,s⇩2⟩;
P ⊢ C sees M,NonStatic:Ts→T = m in D ⟧
⟹ P ⊢ ⟨C∙⇩sM(ps),s⇩0⟩ ⇒ ⟨THROW IncompatibleClassChangeError,s⇩2⟩"

| SCallInitThrow:
"⟦ P ⊢ ⟨ps,s⇩0⟩ [⇒] ⟨map Val vs,(h⇩1,l⇩1,sh⇩1)⟩;
P ⊢ C sees M,Static:Ts→T = (pns,body) in D;
∄sfs. sh⇩1 D = Some(sfs,Done); M ≠ clinit;
P ⊢ ⟨INIT D ([D],False) ← unit,(h⇩1,l⇩1,sh⇩1)⟩ ⇒ ⟨throw a,s'⟩ ⟧
⟹ P ⊢ ⟨C∙⇩sM(ps),s⇩0⟩ ⇒ ⟨throw a,s'⟩"

| SCallInit:
"⟦ P ⊢ ⟨ps,s⇩0⟩ [⇒] ⟨map Val vs,(h⇩1,l⇩1,sh⇩1)⟩;
P ⊢ C sees M,Static:Ts→T = (pns,body) in D;
∄sfs. sh⇩1 D = Some(sfs,Done); M ≠ clinit;
P ⊢ ⟨INIT D ([D],False) ← unit,(h⇩1,l⇩1,sh⇩1)⟩ ⇒ ⟨Val v',(h⇩2,l⇩2,sh⇩2)⟩;
length vs = length pns;  l⇩2' = [pns[↦]vs];
P ⊢ ⟨body,(h⇩2,l⇩2',sh⇩2)⟩ ⇒ ⟨e',(h⇩3,l⇩3,sh⇩3)⟩ ⟧
⟹ P ⊢ ⟨C∙⇩sM(ps),s⇩0⟩ ⇒ ⟨e',(h⇩3,l⇩2,sh⇩3)⟩"

| SCall:
"⟦ P ⊢ ⟨ps,s⇩0⟩ [⇒] ⟨map Val vs,(h⇩2,l⇩2,sh⇩2)⟩;
P ⊢ C sees M,Static:Ts→T = (pns,body) in D;
sh⇩2 D = Some(sfs,Done) ∨ (M = clinit ∧ sh⇩2 D = Some(sfs,Processing));
length vs = length pns;  l⇩2' = [pns[↦]vs];
P ⊢ ⟨body,(h⇩2,l⇩2',sh⇩2)⟩ ⇒ ⟨e',(h⇩3,l⇩3,sh⇩3)⟩ ⟧
⟹ P ⊢ ⟨C∙⇩sM(ps),s⇩0⟩ ⇒ ⟨e',(h⇩3,l⇩2,sh⇩3)⟩"

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

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

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

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

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

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

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

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

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

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

| Throw:
"P ⊢ ⟨e,s⇩0⟩ ⇒ ⟨addr a,s⇩1⟩ ⟹
P ⊢ ⟨throw e,s⇩0⟩ ⇒ ⟨Throw a,s⇩1⟩"

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

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

| Try:
"P ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val v⇩1,s⇩1⟩ ⟹
P ⊢ ⟨try e⇩1 catch(C V) e⇩2,s⇩0⟩ ⇒ ⟨Val v⇩1,s⇩1⟩"

| TryCatch:
"⟦ P ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Throw a,(h⇩1,l⇩1,sh⇩1)⟩;  h⇩1 a = Some(D,fs);  P ⊢ D ≼⇧* C;
P ⊢ ⟨e⇩2,(h⇩1,l⇩1(V↦Addr a),sh⇩1)⟩ ⇒ ⟨e⇩2',(h⇩2,l⇩2,sh⇩2)⟩ ⟧
⟹ P ⊢ ⟨try e⇩1 catch(C V) e⇩2,s⇩0⟩ ⇒ ⟨e⇩2',(h⇩2,l⇩2(V:=l⇩1 V),sh⇩2)⟩"

| TryThrow:
"⟦ P ⊢ ⟨e⇩1,s⇩0⟩ ⇒ ⟨Throw a,(h⇩1,l⇩1,sh⇩1)⟩;  h⇩1 a = Some(D,fs);  ¬ P ⊢ D ≼⇧* C ⟧
⟹ P ⊢ ⟨try e⇩1 catch(C V) e⇩2,s⇩0⟩ ⇒ ⟨Throw a,(h⇩1,l⇩1,sh⇩1)⟩"

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

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

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

― ‹ init rules ›

| InitFinal:
"P ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩ ⟹ P ⊢ ⟨INIT C (Nil,b) ← e,s⟩ ⇒ ⟨e',s'⟩"

| InitNone:
"⟦ sh C = None; P ⊢ ⟨INIT C' (C#Cs,False) ← e,(h,l,sh(C ↦ (sblank P C, Prepared)))⟩ ⇒ ⟨e',s'⟩ ⟧
⟹ P ⊢ ⟨INIT C' (C#Cs,False) ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩"

| InitDone:
"⟦ sh C = Some(sfs,Done); P ⊢ ⟨INIT C' (Cs,True) ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩ ⟧
⟹ P ⊢ ⟨INIT C' (C#Cs,False) ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩"

| InitProcessing:
"⟦ sh C = Some(sfs,Processing); P ⊢ ⟨INIT C' (Cs,True) ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩ ⟧
⟹ P ⊢ ⟨INIT C' (C#Cs,False) ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩"

― ‹ note that @{text RI} will mark all classes in the list Cs with the Error flag ›
| InitError:
"⟦ sh C = Some(sfs,Error);
P ⊢ ⟨RI (C, THROW NoClassDefFoundError);Cs ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩ ⟧
⟹ P ⊢ ⟨INIT C' (C#Cs,False) ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩"

| InitObject:
"⟦ sh C = Some(sfs,Prepared);
C = Object;
sh' = sh(C ↦ (sfs,Processing));
P ⊢ ⟨INIT C' (C#Cs,True) ← e,(h,l,sh')⟩ ⇒ ⟨e',s'⟩ ⟧
⟹ P ⊢ ⟨INIT C' (C#Cs,False) ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩"

| InitNonObject:
"⟦ sh C = Some(sfs,Prepared);
C ≠ Object;
class P C = Some (D,r);
sh' = sh(C ↦ (sfs,Processing));
P ⊢ ⟨INIT C' (D#C#Cs,False) ← e,(h,l,sh')⟩ ⇒ ⟨e',s'⟩ ⟧
⟹ P ⊢ ⟨INIT C' (C#Cs,False) ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩"

| InitRInit:
"P ⊢ ⟨RI (C,C∙⇩sclinit([]));Cs ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩
⟹ P ⊢ ⟨INIT C' (C#Cs,True) ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩"

| RInit:
"⟦ P ⊢ ⟨e',s⟩ ⇒ ⟨Val v, (h',l',sh')⟩;
sh' C = Some(sfs, i); sh'' = sh'(C ↦ (sfs, Done));
C' = last(C#Cs);
P ⊢ ⟨INIT C' (Cs,True) ← e, (h',l',sh'')⟩ ⇒ ⟨e⇩1,s⇩1⟩ ⟧
⟹ P ⊢ ⟨RI (C,e');Cs ← e,s⟩ ⇒ ⟨e⇩1,s⇩1⟩"

| RInitInitFail:
"⟦ P ⊢ ⟨e',s⟩ ⇒ ⟨throw a, (h',l',sh')⟩;
sh' C = Some(sfs, i); sh'' = sh'(C ↦ (sfs, Error));
P ⊢ ⟨RI (D,throw a);Cs ← e, (h',l',sh'')⟩ ⇒ ⟨e⇩1,s⇩1⟩ ⟧
⟹ P ⊢ ⟨RI (C,e');D#Cs ← e,s⟩ ⇒ ⟨e⇩1,s⇩1⟩"

| RInitFailFinal:
"⟦ P ⊢ ⟨e',s⟩ ⇒ ⟨throw a, (h',l',sh')⟩;
sh' C = Some(sfs, i); sh'' = sh'(C ↦ (sfs, Error)) ⟧
⟹ P ⊢ ⟨RI (C,e');Nil ← e,s⟩ ⇒ ⟨throw a, (h',l',sh'')⟩"

(*<*)
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 ⊢ ⟨new C,s⟩ ⇒ ⟨e',s'⟩"
"P ⊢ ⟨Cast C e,s⟩ ⇒ ⟨e',s'⟩"
"P ⊢ ⟨Val v,s⟩ ⇒ ⟨e',s'⟩"
"P ⊢ ⟨e⇩1 «bop» e⇩2,s⟩ ⇒ ⟨e',s'⟩"
"P ⊢ ⟨Var v,s⟩ ⇒ ⟨e',s'⟩"
"P ⊢ ⟨V:=e,s⟩ ⇒ ⟨e',s'⟩"
"P ⊢ ⟨e∙F{D},s⟩ ⇒ ⟨e',s'⟩"
"P ⊢ ⟨C∙⇩sF{D},s⟩ ⇒ ⟨e',s'⟩"
"P ⊢ ⟨e⇩1∙F{D}:=e⇩2,s⟩ ⇒ ⟨e',s'⟩"
"P ⊢ ⟨C∙⇩sF{D}:=e⇩2,s⟩ ⇒ ⟨e',s'⟩"
"P ⊢ ⟨e∙M(es),s⟩ ⇒ ⟨e',s'⟩"
"P ⊢ ⟨C∙⇩sM(es),s⟩ ⇒ ⟨e',s'⟩"
"P ⊢ ⟨{V:T;e⇩1},s⟩ ⇒ ⟨e',s'⟩"
"P ⊢ ⟨e⇩1;;e⇩2,s⟩ ⇒ ⟨e',s'⟩"
"P ⊢ ⟨if (e) e⇩1 else e⇩2,s⟩ ⇒ ⟨e',s'⟩"
"P ⊢ ⟨while (b) c,s⟩ ⇒ ⟨e',s'⟩"
"P ⊢ ⟨throw e,s⟩ ⇒ ⟨e',s'⟩"
"P ⊢ ⟨try e⇩1 catch(C V) e⇩2,s⟩ ⇒ ⟨e',s'⟩"
"P ⊢ ⟨INIT C (Cs,b) ← e,s⟩ ⇒ ⟨e',s'⟩"
"P ⊢ ⟨RI (C,e);Cs ← e⇩0,s⟩ ⇒ ⟨e',s'⟩"

inductive_cases evals_cases [cases set]:
"P ⊢ ⟨[],s⟩ [⇒] ⟨e',s'⟩"
"P ⊢ ⟨e#es,s⟩ [⇒] ⟨e',s'⟩"
(*>*)

subsection "Final expressions"

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

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

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

lemma eval_final_same: "⟦ P ⊢ ⟨e,s⟩ ⇒ ⟨e',s'⟩; final e ⟧ ⟹ e = e' ∧ s = s'"
(*<*)by(auto elim!: finalE eval_cases)(*>*)

lemma eval_finalsId:
assumes finals: "finals es" shows "P ⊢ ⟨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 ⊢ ⟨es,s⟩ [⇒] ⟨es,s⟩"
and finals: "finals (e # es)" by fact+
show "P ⊢ ⟨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 ⊢ ⟨Val v,s⟩ ⇒ ⟨Val v,s⟩" by (simp add: eval_finalId)
moreover from finals e have "P ⊢ ⟨es,s⟩ [⇒] ⟨es,s⟩" by(fast intro:hyp)
ultimately have "P ⊢ ⟨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 ⊢ ⟨Throw a,s⟩ ⇒ ⟨Throw a,s⟩" by (simp add: eval_finalId)
hence "P ⊢ ⟨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 evals_finals_same:
assumes finals: "finals es"
shows "P ⊢ ⟨es,s⟩ [⇒] ⟨es',s'⟩ ⟹ es = es' ∧ s = s'"
using finals
proof (induct es arbitrary: es' type: list)
case Nil then show ?case using evals_cases(1) by blast
next
case (Cons e es)
have IH: "⋀es'. P ⊢ ⟨es,s⟩ [⇒] ⟨es',s'⟩ ⟹ finals es ⟹ es = es' ∧ s = s'"
and step: "P ⊢ ⟨e # es,s⟩ [⇒] ⟨es',s'⟩" and finals: "finals (e # es)" by fact+
then obtain e' es'' where es': "es' = e'#es''" by (meson Cons.prems(1) evals_cases(2))
have fe: "final e" using finals not_finals_ConsI by auto
show ?case
proof(rule evals_cases(2)[OF step])
fix v s⇩1 es1 assume es1: "es' = Val v # es1"
and estep: "P ⊢ ⟨e,s⟩ ⇒ ⟨Val v,s⇩1⟩" and esstep: "P ⊢ ⟨es,s⇩1⟩ [⇒] ⟨es1,s'⟩"
then have "e = Val v" using eval_final_same fe by auto
then have "finals es" using es' not_finals_ConsI2 finals by blast
then show ?thesis using es' IH estep esstep es1 eval_final_same fe by blast
next
fix e' assume es1: "es' = throw e' # es" and estep: "P ⊢ ⟨e,s⟩ ⇒ ⟨throw e',s'⟩"
then have "e = throw e'" using eval_final_same fe by auto
then show ?thesis using es' estep es1 eval_final_same fe by blast
qed
qed
(*>*)

subsection "Property preservation"

lemma evals_length: "P ⊢ ⟨es,s⟩ [⇒] ⟨es',s'⟩ ⟹ length es = length es'"
by(induct es arbitrary:es' s s', auto elim: evals_cases)

corollary evals_empty: "P ⊢ ⟨es,s⟩ [⇒] ⟨es',s'⟩ ⟹ (es = []) = (es' = [])"
by(drule evals_length, fastforce)

(****)

theorem eval_hext: "P ⊢ ⟨e,(h,l,sh)⟩ ⇒ ⟨e',(h',l',sh')⟩ ⟹ h ⊴ h'"
and evals_hext:  "P ⊢ ⟨es,(h,l,sh)⟩ [⇒] ⟨es',(h',l',sh')⟩ ⟹ h ⊴ h'"
(*<*)
proof (induct rule: eval_evals_inducts)
case New thus ?case
by(fastforce intro!: hext_new intro:LeastI simp:new_Addr_def
split:if_split_asm simp del:fun_upd_apply)
next
case NewInit thus ?case
by (meson hext_new hext_trans new_Addr_SomeD)
next
case FAss thus ?case
by(auto simp:sym[THEN hext_upd_obj] simp del:fun_upd_apply
elim!: hext_trans)
qed (auto elim!: hext_trans)
(*>*)

lemma eval_lcl_incr: "P ⊢ ⟨e,(h⇩0,l⇩0,sh⇩0)⟩ ⇒ ⟨e',(h⇩1,l⇩1,sh⇩1)⟩ ⟹ dom l⇩0 ⊆ dom l⇩1"
and evals_lcl_incr: "P ⊢ ⟨es,(h⇩0,l⇩0,sh⇩0)⟩ [⇒] ⟨es',(h⇩1,l⇩1,sh⇩1)⟩ ⟹ dom l⇩0 ⊆ dom l⇩1"
(*<*)
proof (induct rule: eval_evals_inducts)
case BinOp show ?case by(rule subset_trans)(rule BinOp.hyps)+
next
case Call thus ?case
by(simp del: fun_upd_apply)
next
case Seq show ?case by(rule subset_trans)(rule Seq.hyps)+
next
case CondT show ?case by(rule subset_trans)(rule CondT.hyps)+
next
case CondF show ?case by(rule subset_trans)(rule CondF.hyps)+
next
case WhileT thus ?case by(blast)
next
case TryCatch thus ?case by(clarsimp simp:dom_def split:if_split_asm) blast
next
case Cons show ?case by(rule subset_trans)(rule Cons.hyps)+
next
case Block thus ?case by(auto simp del:fun_upd_apply)
qed auto
(*>*)

lemma
shows init_ri_same_loc: "P ⊢ ⟨e,(h,l,sh)⟩ ⇒ ⟨e',(h',l',sh')⟩
⟹ (⋀C Cs b M a. e = INIT C (Cs,b) ← unit ∨ e = C∙⇩sM([]) ∨ e = RI (C,Throw a) ; Cs ← unit
∨ e = RI (C,C∙⇩sclinit([])) ; Cs ← unit
⟹ l = l')"
and "P ⊢ ⟨es,(h,l,sh)⟩ [⇒] ⟨es',(h',l',sh')⟩ ⟹ True"
proof(induct rule: eval_evals_inducts)
case (RInitInitFail e h l sh a')
then show ?case using eval_final[of _ _ _ "throw a'"]
by(fastforce dest: eval_final_same[of _ "Throw a"])
next
case RInitFailFinal then show ?case by(auto dest: eval_final_same)
qed(auto dest: evals_cases eval_cases(17) eval_final_same)

lemma init_same_loc: "P ⊢ ⟨INIT C (Cs,b) ← unit,(h,l,sh)⟩ ⇒ ⟨e',(h',l',sh')⟩ ⟹ l = l'"

(****)

lemma assumes wf: "wwf_J_prog P"
shows eval_proc_pres': "P ⊢ ⟨e,(h,l,sh)⟩ ⇒ ⟨e',(h',l',sh')⟩
⟹ not_init C e ⟹ ∃sfs. sh C = ⌊(sfs, Processing)⌋ ⟹ ∃sfs'. sh' C = ⌊(sfs', Processing)⌋"
and evals_proc_pres': "P ⊢ ⟨es,(h,l,sh)⟩ [⇒] ⟨es',(h',l',sh')⟩
⟹ not_inits C es ⟹ ∃sfs. sh C = ⌊(sfs, Processing)⌋ ⟹ ∃sfs'. sh' C = ⌊(sfs', Processing)⌋"
(*<*)
proof(induct rule:eval_evals_inducts)
case Call then show ?case using sees_wwf_nsub_RI[OF wf Call.hyps(6)] nsub_RI_not_init by auto
next
case (SCallInit ps h l sh vs h⇩1 l⇩1 sh⇩1 C' M Ts T pns body D v' h⇩2 l⇩2 sh⇩2 l⇩2' e' h⇩3 l⇩3 sh⇩3)
then show ?case
using SCallInit sees_wwf_nsub_RI[OF wf SCallInit.hyps(3)] nsub_RI_not_init[of body] by auto
next
case SCall then show ?case using sees_wwf_nsub_RI[OF wf SCall.hyps(3)] nsub_RI_not_init by auto
next
case (InitNone sh C1 C' Cs h l e' a a b) then show ?case by(cases "C = C1") auto
next
case (InitDone sh C sfs C' Cs h l e' a a b) then show ?case by(cases Cs, auto)
next
case (InitProcessing sh C sfs C' Cs h l e' a a b) then show ?case by(cases Cs, auto)
next
case (InitError sh C1 sfs Cs h l e' a a b C') then show ?case by(cases "C = C1") auto
next
case (InitObject sh C1 sfs sh' C' Cs h l e' a a b) then show ?case by(cases "C = C1") auto
next
case (InitNonObject sh C1 sfs D a b sh' C' Cs h l e' a a b)
then show ?case by(cases "C = C1") auto
next
case (RInit e a a b v h' l' sh' C sfs i sh'' C' Cs e⇩1 a a b) then show ?case by(cases Cs, auto)
next
case (RInitInitFail e h l sh a h' l' sh' C1 sfs i sh'' D Cs e⇩1 h1 l1 sh1)
then show ?case using eval_final by fastforce
qed(auto)

(************************************************)

subsection‹Init Elimination rules›

lemma init_NilE:
assumes init: "P ⊢ ⟨INIT C (Nil,b) ← unit,s⟩ ⇒ ⟨e',s'⟩"
shows "e' = unit ∧ s' = s"
proof(rule eval_cases(19)[OF init]) ― ‹ Init › qed(auto dest: eval_final_same)

lemma init_ProcessingE:
assumes shC: "sh C = ⌊(sfs, Processing)⌋"
and init: "P ⊢ ⟨INIT C ([C],False) ← unit,(h,l,sh)⟩ ⇒ ⟨e',s'⟩"
shows "e' = unit ∧ s' = (h,l,sh)"
proof(rule eval_cases(19)[OF init]) ― ‹ Init ›
fix sha Ca sfs Cs ha la
assume "(h, l, sh) = (ha, la, sha)" and "sha Ca = ⌊(sfs, Processing)⌋"
and "P ⊢ ⟨INIT C (Cs,True) ← unit,(ha, la, sha)⟩ ⇒ ⟨e',s'⟩" and "[C] = Ca # Cs"
then show ?thesis using init_NilE by simp
next
fix sha sfs Cs ha la
assume "(h, l, sh) = (ha, la, sha)" and "sha Object = ⌊(sfs, Prepared)⌋"
and "[C] = Object # Cs"
then show ?thesis using shC by clarsimp
qed(auto simp: assms)

lemma rinit_throwE:
"P ⊢ ⟨RI (C,throw e) ; Cs ← e⇩0,s⟩ ⇒ ⟨e',s'⟩
⟹ ∃a s⇩t. e' = throw a ∧ P ⊢ ⟨throw e,s⟩ ⇒ ⟨throw a,s⇩t⟩"
proof(induct Cs arbitrary: C e s)
case Nil
then show ?case
proof(rule eval_cases(20)) ― ‹ RI ›
fix v h' l' sh' assume "P ⊢ ⟨throw e,s⟩ ⇒ ⟨Val v,(h', l', sh')⟩"
then show ?case using eval_cases(17) by blast
qed(auto)
next
case (Cons C' Cs')
show ?case using Cons.prems(1)
proof(rule eval_cases(20)) ― ‹ RI ›
fix v h' l' sh' assume "P ⊢ ⟨throw e,s⟩ ⇒ ⟨Val v,(h', l', sh')⟩"
then show ?case using eval_cases(17) by blast
next
fix a h' l' sh' sfs i D Cs''
assume e''step: "P ⊢ ⟨throw e,s⟩ ⇒ ⟨throw a,(h', l', sh')⟩"
and shC: "sh' C = ⌊(sfs, i)⌋"
and riD: "P ⊢ ⟨RI (D,throw a) ; Cs'' ← e⇩0,(h', l', sh'(C ↦ (sfs, Error)))⟩ ⇒ ⟨e',s'⟩"
and "C' # Cs' = D # Cs''"
then show ?thesis using Cons.hyps eval_final eval_final_same by blast
qed(simp)
qed

lemma rinit_ValE:
assumes ri: "P ⊢ ⟨RI (C,e) ; Cs ← unit,s⟩ ⇒ ⟨Val v',s'⟩"
shows "∃v'' s''. P ⊢ ⟨e,s⟩ ⇒ ⟨Val v'',s''⟩"
proof(rule eval_cases(20)[OF ri]) ― ‹ RI ›
fix a h' l' sh' sfs i D Cs'
assume "P ⊢ ⟨RI (D,throw a) ; Cs' ← unit,(h', l', sh'(C ↦ (sfs, Error)))⟩ ⇒ ⟨Val v',s'⟩"
then show ?thesis using rinit_throwE by blast
qed(auto)

subsection "Some specific evaluations"

lemma lass_val_of_eval:
"⟦ lass_val_of e = ⌊a⌋; P ⊢ ⟨e,(h, l, sh)⟩ ⇒ ⟨e',(h', l', sh')⟩ ⟧
⟹ e' = unit ∧ h' = h ∧ l' = l(fst a↦snd a) ∧ sh' = sh"
by(drule lass_val_of_spec, auto elim: eval.cases)

lemma eval_throw_nonVal:
assumes eval: "P ⊢ ⟨e,s⟩ ⇒ ⟨throw a,s'⟩"
shows "val_of e = None"
proof(cases "val_of e")
case (Some v) show ?thesis using eval by(auto simp: val_of_spec[OF Some] intro: eval.cases)
qed(simp)

lemma eval_throw_nonLAss:
assumes eval: "P ⊢ ⟨e,s⟩ ⇒ ⟨throw a,s'⟩"
shows "lass_val_of e = None"
proof(cases "lass_val_of e")
case (Some v) show ?thesis using eval by(auto simp: lass_val_of_spec[OF Some] intro: eval.cases)
qed(simp)

end
```