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,s0⟩ ⇒ ⟨addr a,(h,l,sh)⟩; h a = Some(D,fs); P ⊢ D ≼* C ⟧
  ⟹ P ⊢ ⟨Cast C e,s0⟩ ⇒ ⟨addr a,(h,l,sh)⟩"

| CastNull:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨null,s1⟩ ⟹
  P ⊢ ⟨Cast C e,s0⟩ ⇒ ⟨null,s1⟩"

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

| CastThrow:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢ ⟨Cast C e,s0⟩ ⇒ ⟨throw e',s1⟩"

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

| BinOp:
  "⟦ P ⊢ ⟨e1,s0⟩ ⇒ ⟨Val v1,s1⟩; P ⊢ ⟨e2,s1⟩ ⇒ ⟨Val v2,s2⟩; binop(bop,v1,v2) = Some v ⟧
  ⟹ P ⊢ ⟨e1 «bop» e2,s0⟩ ⇒ ⟨Val v,s2⟩"

| BinOpThrow1:
  "P ⊢ ⟨e1,s0⟩ ⇒ ⟨throw e,s1⟩ ⟹
  P ⊢ ⟨e1 «bop» e2, s0⟩ ⇒ ⟨throw e,s1⟩"

| BinOpThrow2:
  "⟦ P ⊢ ⟨e1,s0⟩ ⇒ ⟨Val v1,s1⟩; P ⊢ ⟨e2,s1⟩ ⇒ ⟨throw e,s2⟩ ⟧
  ⟹ P ⊢ ⟨e1 «bop» e2,s0⟩ ⇒ ⟨throw e,s2⟩"

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

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

| LAssThrow:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢ ⟨V:=e,s0⟩ ⇒ ⟨throw e',s1⟩"

| FAcc:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨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},s0⟩ ⇒ ⟨Val v,(h,l,sh)⟩"

| FAccNull:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨null,s1⟩ ⟹
  P ⊢ ⟨e∙F{D},s0⟩ ⇒ ⟨THROW NullPointer,s1⟩"

| FAccThrow:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢ ⟨e∙F{D},s0⟩ ⇒ ⟨throw e',s1⟩"

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

| FAccStatic:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨addr a,(h,l,sh)⟩; h a = Some(C,fs);
    P ⊢ C has F,Static:t in D ⟧
  ⟹ P ⊢ ⟨e∙F{D},s0⟩ ⇒ ⟨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 ⊢ ⟨e1,s0⟩ ⇒ ⟨addr a,s1⟩; P ⊢ ⟨e2,s1⟩ ⇒ ⟨Val v,(h2,l2,sh2)⟩;
     h2 a = Some(C,fs); P ⊢ C has F,NonStatic:t in D;
     fs' = fs((F,D)↦v); h2' = h2(a↦(C,fs')) ⟧
  ⟹ P ⊢ ⟨e1∙F{D}:=e2,s0⟩ ⇒ ⟨unit,(h2',l2,sh2)⟩"

| FAssNull:
  "⟦ P ⊢ ⟨e1,s0⟩ ⇒ ⟨null,s1⟩;  P ⊢ ⟨e2,s1⟩ ⇒ ⟨Val v,s2⟩ ⟧ ⟹
  P ⊢ ⟨e1∙F{D}:=e2,s0⟩ ⇒ ⟨THROW NullPointer,s2⟩"

| FAssThrow1:
  "P ⊢ ⟨e1,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢ ⟨e1∙F{D}:=e2,s0⟩ ⇒ ⟨throw e',s1⟩"

| FAssThrow2:
  "⟦ P ⊢ ⟨e1,s0⟩ ⇒ ⟨Val v,s1⟩; P ⊢ ⟨e2,s1⟩ ⇒ ⟨throw e',s2⟩ ⟧
  ⟹ P ⊢ ⟨e1∙F{D}:=e2,s0⟩ ⇒ ⟨throw e',s2⟩"

| FAssNone:
  "⟦ P ⊢ ⟨e1,s0⟩ ⇒ ⟨addr a,s1⟩; P ⊢ ⟨e2,s1⟩ ⇒ ⟨Val v,(h2,l2,sh2)⟩;
     h2 a = Some(C,fs); ¬(∃b t. P ⊢ C has F,b:t in D) ⟧
  ⟹ P ⊢ ⟨e1∙F{D}:=e2,s0⟩ ⇒ ⟨THROW NoSuchFieldError,(h2,l2,sh2)⟩"

| FAssStatic:
  "⟦ P ⊢ ⟨e1,s0⟩ ⇒ ⟨addr a,s1⟩; P ⊢ ⟨e2,s1⟩ ⇒ ⟨Val v,(h2,l2,sh2)⟩;
     h2 a = Some(C,fs); P ⊢ C has F,Static:t in D ⟧
  ⟹ P ⊢ ⟨e1∙F{D}:=e2,s0⟩ ⇒ ⟨THROW IncompatibleClassChangeError,(h2,l2,sh2)⟩"

| SFAss:
  "⟦ P ⊢ ⟨e2,s0⟩ ⇒ ⟨Val v,(h1,l1,sh1)⟩;
     P ⊢ C has F,Static:t in D;
     sh1 D = Some(sfs,Done); sfs' = sfs(F↦v); sh1' = sh1(D↦(sfs',Done)) ⟧
  ⟹ P ⊢ ⟨C∙sF{D}:=e2,s0⟩ ⇒ ⟨unit,(h1,l1,sh1')⟩"

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

| SFAssInitThrow:
  "⟦ P ⊢ ⟨e2,s0⟩ ⇒ ⟨Val v,(h1,l1,sh1)⟩;
     P ⊢ C has F,Static:t in D;
     ∄sfs. sh1 D = Some(sfs,Done); P ⊢ ⟨INIT D ([D],False) ← unit,(h1,l1,sh1)⟩ ⇒ ⟨throw a,s'⟩ ⟧
  ⟹ P ⊢ ⟨C∙sF{D}:=e2,s0⟩ ⇒ ⟨throw a,s'⟩"

| SFAssThrow:
  "P ⊢ ⟨e2,s0⟩ ⇒ ⟨throw e',s2⟩
  ⟹ P ⊢ ⟨C∙sF{D}:=e2,s0⟩ ⇒ ⟨throw e',s2⟩"

| SFAssNone:
  "⟦ P ⊢ ⟨e2,s0⟩ ⇒ ⟨Val v,(h2,l2,sh2)⟩;
    ¬(∃b t. P ⊢ C has F,b:t in D) ⟧
  ⟹ P ⊢ ⟨C∙sF{D}:=e2,s0⟩ ⇒ ⟨THROW NoSuchFieldError,(h2,l2,sh2)⟩"

| SFAssNonStatic:
  "⟦ P ⊢ ⟨e2,s0⟩ ⇒ ⟨Val v,(h2,l2,sh2)⟩;
    P ⊢ C has F,NonStatic:t in D ⟧
  ⟹ P ⊢ ⟨C∙sF{D}:=e2,s0⟩ ⇒ ⟨THROW IncompatibleClassChangeError,(h2,l2,sh2)⟩"

| CallObjThrow:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢ ⟨e∙M(ps),s0⟩ ⇒ ⟨throw e',s1⟩"

| CallParamsThrow:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨Val v,s1⟩; P ⊢ ⟨es,s1⟩ [⇒] ⟨map Val vs @ throw ex # es',s2⟩ ⟧
   ⟹ P ⊢ ⟨e∙M(es),s0⟩ ⇒ ⟨throw ex,s2⟩"

| CallNull:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨null,s1⟩;  P ⊢ ⟨ps,s1⟩ [⇒] ⟨map Val vs,s2⟩ ⟧
  ⟹ P ⊢ ⟨e∙M(ps),s0⟩ ⇒ ⟨THROW NullPointer,s2⟩"

| CallNone:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨addr a,s1⟩;  P ⊢ ⟨ps,s1⟩ [⇒] ⟨map Val vs,(h2,l2,sh2)⟩;
     h2 a = Some(C,fs); ¬(∃b Ts T m D. P ⊢ C sees M,b:Ts→T = m in D) ⟧
  ⟹ P ⊢ ⟨e∙M(ps),s0⟩ ⇒ ⟨THROW NoSuchMethodError,(h2,l2,sh2)⟩"

| CallStatic:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨addr a,s1⟩;  P ⊢ ⟨ps,s1⟩ [⇒] ⟨map Val vs,(h2,l2,sh2)⟩;
     h2 a = Some(C,fs); P ⊢ C sees M,Static:Ts→T = m in D ⟧
  ⟹ P ⊢ ⟨e∙M(ps),s0⟩ ⇒ ⟨THROW IncompatibleClassChangeError,(h2,l2,sh2)⟩"

| Call:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨addr a,s1⟩;  P ⊢ ⟨ps,s1⟩ [⇒] ⟨map Val vs,(h2,l2,sh2)⟩;
     h2 a = Some(C,fs); P ⊢ C sees M,NonStatic:Ts→T = (pns,body) in D;
     length vs = length pns;  l2' = [this↦Addr a, pns[↦]vs];
     P ⊢ ⟨body,(h2,l2',sh2)⟩ ⇒ ⟨e',(h3,l3,sh3)⟩ ⟧
  ⟹ P ⊢ ⟨e∙M(ps),s0⟩ ⇒ ⟨e',(h3,l2,sh3)⟩"

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

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

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

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

| SCallInit:
  "⟦ P ⊢ ⟨ps,s0⟩ [⇒] ⟨map Val vs,(h1,l1,sh1)⟩;
     P ⊢ C sees M,Static:Ts→T = (pns,body) in D;
     ∄sfs. sh1 D = Some(sfs,Done); M ≠ clinit;
     P ⊢ ⟨INIT D ([D],False) ← unit,(h1,l1,sh1)⟩ ⇒ ⟨Val v',(h2,l2,sh2)⟩;
     length vs = length pns;  l2' = [pns[↦]vs];
     P ⊢ ⟨body,(h2,l2',sh2)⟩ ⇒ ⟨e',(h3,l3,sh3)⟩ ⟧
  ⟹ P ⊢ ⟨C∙sM(ps),s0⟩ ⇒ ⟨e',(h3,l2,sh3)⟩"

| SCall:
  "⟦ P ⊢ ⟨ps,s0⟩ [⇒] ⟨map Val vs,(h2,l2,sh2)⟩;
     P ⊢ C sees M,Static:Ts→T = (pns,body) in D;
     sh2 D = Some(sfs,Done) ∨ (M = clinit ∧ sh2 D = Some(sfs,Processing));
     length vs = length pns;  l2' = [pns[↦]vs];
     P ⊢ ⟨body,(h2,l2',sh2)⟩ ⇒ ⟨e',(h3,l3,sh3)⟩ ⟧
  ⟹ P ⊢ ⟨C∙sM(ps),s0⟩ ⇒ ⟨e',(h3,l2,sh3)⟩"

| Block:
  "P ⊢ ⟨e0,(h0,l0(V:=None),sh0)⟩ ⇒ ⟨e1,(h1,l1,sh1)⟩ ⟹
  P ⊢ ⟨{V:T; e0},(h0,l0,sh0)⟩ ⇒ ⟨e1,(h1,l1(V:=l0 V),sh1)⟩"

| Seq:
  "⟦ P ⊢ ⟨e0,s0⟩ ⇒ ⟨Val v,s1⟩; P ⊢ ⟨e1,s1⟩ ⇒ ⟨e2,s2⟩ ⟧
  ⟹ P ⊢ ⟨e0;;e1,s0⟩ ⇒ ⟨e2,s2⟩"

| SeqThrow:
  "P ⊢ ⟨e0,s0⟩ ⇒ ⟨throw e,s1⟩ ⟹
  P ⊢ ⟨e0;;e1,s0⟩ ⇒ ⟨throw e,s1⟩"

| CondT:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨true,s1⟩; P ⊢ ⟨e1,s1⟩ ⇒ ⟨e',s2⟩ ⟧
  ⟹ P ⊢ ⟨if (e) e1 else e2,s0⟩ ⇒ ⟨e',s2⟩"

| CondF:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨false,s1⟩; P ⊢ ⟨e2,s1⟩ ⇒ ⟨e',s2⟩ ⟧
  ⟹ P ⊢ ⟨if (e) e1 else e2,s0⟩ ⇒ ⟨e',s2⟩"

| CondThrow:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢ ⟨if (e) e1 else e2, s0⟩ ⇒ ⟨throw e',s1⟩"

| WhileF:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨false,s1⟩ ⟹
  P ⊢ ⟨while (e) c,s0⟩ ⇒ ⟨unit,s1⟩"

| WhileT:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨true,s1⟩; P ⊢ ⟨c,s1⟩ ⇒ ⟨Val v1,s2⟩; P ⊢ ⟨while (e) c,s2⟩ ⇒ ⟨e3,s3⟩ ⟧
  ⟹ P ⊢ ⟨while (e) c,s0⟩ ⇒ ⟨e3,s3⟩"

| WhileCondThrow:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢ ⟨while (e) c,s0⟩ ⇒ ⟨throw e',s1⟩"

| WhileBodyThrow:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨true,s1⟩; P ⊢ ⟨c,s1⟩ ⇒ ⟨throw e',s2⟩⟧
  ⟹ P ⊢ ⟨while (e) c,s0⟩ ⇒ ⟨throw e',s2⟩"

| Throw:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨addr a,s1⟩ ⟹
  P ⊢ ⟨throw e,s0⟩ ⇒ ⟨Throw a,s1⟩"

| ThrowNull:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨null,s1⟩ ⟹
  P ⊢ ⟨throw e,s0⟩ ⇒ ⟨THROW NullPointer,s1⟩"

| ThrowThrow:
  "P ⊢ ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢ ⟨throw e,s0⟩ ⇒ ⟨throw e',s1⟩"

| Try:
  "P ⊢ ⟨e1,s0⟩ ⇒ ⟨Val v1,s1⟩ ⟹
  P ⊢ ⟨try e1 catch(C V) e2,s0⟩ ⇒ ⟨Val v1,s1⟩"

| TryCatch:
  "⟦ P ⊢ ⟨e1,s0⟩ ⇒ ⟨Throw a,(h1,l1,sh1)⟩;  h1 a = Some(D,fs);  P ⊢ D ≼* C;
     P ⊢ ⟨e2,(h1,l1(V↦Addr a),sh1)⟩ ⇒ ⟨e2',(h2,l2,sh2)⟩ ⟧
  ⟹ P ⊢ ⟨try e1 catch(C V) e2,s0⟩ ⇒ ⟨e2',(h2,l2(V:=l1 V),sh2)⟩"

| TryThrow:
  "⟦ P ⊢ ⟨e1,s0⟩ ⇒ ⟨Throw a,(h1,l1,sh1)⟩;  h1 a = Some(D,fs);  ¬ P ⊢ D ≼* C ⟧
  ⟹ P ⊢ ⟨try e1 catch(C V) e2,s0⟩ ⇒ ⟨Throw a,(h1,l1,sh1)⟩"

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

| Cons:
  "⟦ P ⊢ ⟨e,s0⟩ ⇒ ⟨Val v,s1⟩; P ⊢ ⟨es,s1⟩ [⇒] ⟨es',s2⟩ ⟧
  ⟹ P ⊢ ⟨e#es,s0⟩ [⇒] ⟨Val v # es',s2⟩"

| ConsThrow:
  "P ⊢ ⟨e, s0⟩ ⇒ ⟨throw e', s1⟩ ⟹
  P ⊢ ⟨e#es, s0⟩ [⇒] ⟨throw e' # es, s1⟩"

― ‹ 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'')⟩ ⇒ ⟨e1,s1⟩ ⟧
  ⟹ P ⊢ ⟨RI (C,e');Cs ← e,s⟩ ⇒ ⟨e1,s1⟩"

| 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'')⟩ ⇒ ⟨e1,s1⟩ ⟧
  ⟹ P ⊢ ⟨RI (C,e');D#Cs ← e,s⟩ ⇒ ⟨e1,s1⟩"

| 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 ⊢ ⟨e1 «bop» e2,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 ⊢ ⟨e1∙F{D}:=e2,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨C∙sF{D}:=e2,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨e∙M(es),s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨C∙sM(es),s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨{V:T;e1},s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨e1;;e2,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨if (e) e1 else e2,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨while (b) c,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨throw e,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨try e1 catch(C V) e2,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨INIT C (Cs,b) ← e,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢ ⟨RI (C,e);Cs ← e0,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 s1 es1 assume es1: "es' = Val v # es1"
      and estep: "P ⊢ ⟨e,s⟩ ⇒ ⟨Val v,s1⟩" and esstep: "P ⊢ ⟨es,s1⟩ [⇒] ⟨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,(h0,l0,sh0)⟩ ⇒ ⟨e',(h1,l1,sh1)⟩ ⟹ dom l0 ⊆ dom l1"
 and evals_lcl_incr: "P ⊢ ⟨es,(h0,l0,sh0)⟩ [⇒] ⟨es',(h1,l1,sh1)⟩ ⟹ dom l0 ⊆ dom l1"
(*<*)
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'"
 by(simp add: init_ri_same_loc)

(****)

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 h1 l1 sh1 C' M Ts T pns body D v' h2 l2 sh2 l2' e' h3 l3 sh3)
  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 e1 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 e1 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 ← e0,s⟩ ⇒ ⟨e',s'⟩
   ⟹ ∃a st. e' = throw a ∧ P ⊢ ⟨throw e,s⟩ ⇒ ⟨throw a,st⟩"
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'' ← e0,(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