Quelle  BigStep.thy

(*  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₀⟩ ==> ⟨addr a,(h,l,sh)⟩; h a = Some(D,fs); P ⊨ D ⪯^* C ]
  ==> P ⊨ ⟨Cast C e,s₀⟩ ==> ⟨addr a,(h,l,sh)⟩"

| CastNull:
  "P ⊨ ⟨e,s₀⟩ ==> ⟨null,s₁⟩ ==>
  P ⊨ ⟨Cast C e,s₀⟩ ==> ⟨null,s₁⟩"

| CastFail:
  "[ P ⊨ ⟨e,s₀⟩==> ⟨addr a,(h,l,sh)⟩; h a = Some(D,fs); ¬ P ⊨ D ⪯^* C ]
  ==> P ⊨ ⟨Cast C e,s₀⟩ ==> ⟨THROW ClassCast,(h,l,sh)⟩"

| CastThrow:
  "P ⊨ ⟨e,s₀⟩ ==> ⟨throw e',s₁⟩ ==>
  P ⊨ ⟨Cast C e,s₀⟩ ==> ⟨throw e',s₁⟩"

| Val:
  "P ⊨ ⟨Val v,s⟩ ==> ⟨Val v,s⟩"

| BinOp:
  "[ P ⊨ ⟨e₁,s₀⟩ ==> ⟨Val v₁,s₁⟩; P ⊨ ⟨e₂,s₁⟩ ==> ⟨Val v₂,s₂⟩; binop(bop,v₁,v₂) = Some v ]
  ==> P ⊨ ⟨e₁ «bop¬ e₂,s₀⟩ ==> ⟨Val v,s₂⟩"

| BinOpThrow1:
  "P ⊨ ⟨e₁,s₀⟩ ==> ⟨throw e,s₁⟩ ==>
  P ⊨ ⟨e₁ «bop¬ e₂, s₀⟩ ==> ⟨throw e,s₁⟩"

| BinOpThrow2:
  "[ P ⊨ ⟨e₁,s₀⟩ ==> ⟨Val v₁,s₁⟩; P ⊨ ⟨e₂,s₁⟩ ==> ⟨throw e,s₂⟩ ]
  ==> P ⊨ ⟨e₁ «bop¬ e₂,s₀⟩ ==> ⟨throw e,s₂⟩"

| Var:
  "l V = Some v ==>
  P ⊨ ⟨Var V,(h,l,sh)⟩ ==> ⟨Val v,(h,l,sh)⟩"

| LAss:
  "[ P ⊨ ⟨e,s₀⟩ ==> ⟨Val v,(h,l,sh)⟩; l' = l(V↦v) ]
  ==> P ⊨ ⟨V:=e,s₀⟩ ==> ⟨unit,(h,l',sh)⟩"

| LAssThrow:
  "P ⊨ ⟨e,s₀⟩ ==> ⟨throw e',s₁⟩ ==>
  P ⊨ ⟨V:=e,s₀⟩ ==> ⟨throw e',s₁⟩"

| FAcc:
  "[ P ⊨ ⟨e,s₀⟩ ==> ⟨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₀⟩ ==> ⟨Val v,(h,l,sh)⟩"

| FAccNull:
  "P ⊨ ⟨e,s₀⟩ ==> ⟨null,s₁⟩ ==>
  P ⊨ ⟨e∙F{D},s₀⟩ ==> ⟨THROW NullPointer,s₁⟩"

| FAccThrow:
  "P ⊨ ⟨e,s₀⟩ ==> ⟨throw e',s₁⟩ ==>
  P ⊨ ⟨e∙F{D},s₀⟩ ==> ⟨throw e',s₁⟩"

| FAccNone:
  "[ P ⊨ ⟨e,s₀⟩ ==> ⟨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₀⟩ ==> ⟨THROW NoSuchFieldError,(h,l,sh)⟩"

| FAccStatic:
  "[ P ⊨ ⟨e,s₀⟩ ==> ⟨addr a,(h,l,sh)⟩; h a = Some(C,fs);
    P ⊨ C has F,Static:t in D ]
  ==> P ⊨ ⟨e∙F{D},s₀⟩ ==> ⟨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₁,s₀⟩ ==> ⟨addr a,s₁⟩; P ⊨ ⟨e₂,s₁⟩ ==> ⟨Val v,(h₂,l₂,sh₂)⟩;
     h₂ a = Some(C,fs); P ⊨ C has F,NonStatic:t in D;
     fs' = fs((F,D)↦v); h₂' = h₂(a↦(C,fs')) ]
  ==> P ⊨ ⟨e₁∙F{D}:=e₂,s₀⟩ ==> ⟨unit,(h₂',l₂,sh₂)⟩"

| FAssNull:
  "[ P ⊨ ⟨e₁,s₀⟩ ==> ⟨null,s₁⟩; P ⊨ ⟨e₂,s₁⟩ ==> ⟨Val v,s₂⟩ ] ==>
  P ⊨ ⟨e₁∙F{D}:=e₂,s₀⟩ ==> ⟨THROW NullPointer,s₂⟩"

| FAssThrow1:
  "P ⊨ ⟨e₁,s₀⟩ ==> ⟨throw e',s₁⟩ ==>
  P ⊨ ⟨e₁∙F{D}:=e₂,s₀⟩ ==> ⟨throw e',s₁⟩"

| FAssThrow2:
  "[ P ⊨ ⟨e₁,s₀⟩ ==> ⟨Val v,s₁⟩; P ⊨ ⟨e₂,s₁⟩ ==> ⟨throw e',s₂⟩ ]
  ==> P ⊨ ⟨e₁∙F{D}:=e₂,s₀⟩ ==> ⟨throw e',s₂⟩"

| FAssNone:
  "[ P ⊨ ⟨e₁,s₀⟩ ==> ⟨addr a,s₁⟩; P ⊨ ⟨e₂,s₁⟩ ==> ⟨Val v,(h₂,l₂,sh₂)⟩;
     h₂ a = Some(C,fs); ¬(∃b t. P ⊨ C has F,b:t in D) ]
  ==> P ⊨ ⟨e₁∙F{D}:=e₂,s₀⟩ ==> ⟨THROW NoSuchFieldError,(h₂,l₂,sh₂)⟩"

| FAssStatic:
  "[ P ⊨ ⟨e₁,s₀⟩ ==> ⟨addr a,s₁⟩; P ⊨ ⟨e₂,s₁⟩ ==> ⟨Val v,(h₂,l₂,sh₂)⟩;
     h₂ a = Some(C,fs); P ⊨ C has F,Static:t in D ]
  ==> P ⊨ ⟨e₁∙F{D}:=e₂,s₀⟩ ==> ⟨THROW IncompatibleClassChangeError,(h₂,l₂,sh₂)⟩"

| SFAss:
  "[ P ⊨ ⟨e₂,s₀⟩ ==> ⟨Val v,(h₁,l₁,sh₁)⟩;
     P ⊨ C has F,Static:t in D;
     sh₁ D = Some(sfs,Done); sfs' = sfs(F↦v); sh₁' = sh₁(D↦(sfs',Done)) ]
  ==> P ⊨ ⟨C∙_sF{D}:=e₂,s₀⟩ ==> ⟨unit,(h₁,l₁,sh₁')⟩"

| SFAssInit:
  "[ P ⊨ ⟨e₂,s₀⟩ ==> ⟨Val v,(h₁,l₁,sh₁)⟩;
     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' = sfs(F↦v); sh'' = sh'(D↦(sfs',i)) ]
  ==> P ⊨ ⟨C∙_sF{D}:=e₂,s₀⟩ ==> ⟨unit,(h',l',sh'')⟩"

| SFAssInitThrow:
  "[ P ⊨ ⟨e₂,s₀⟩ ==> ⟨Val v,(h₁,l₁,sh₁)⟩;
     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}:=e₂,s₀⟩ ==> ⟨throw a,s'⟩"

| SFAssThrow:
  "P ⊨ ⟨e₂,s₀⟩ ==> ⟨throw e',s₂⟩
  ==> P ⊨ ⟨C∙_sF{D}:=e₂,s₀⟩ ==> ⟨throw e',s₂⟩"

| SFAssNone:
  "[ P ⊨ ⟨e₂,s₀⟩ ==> ⟨Val v,(h₂,l₂,sh₂)⟩;
    ¬(∃b t. P ⊨ C has F,b:t in D) ]
  ==> P ⊨ ⟨C∙_sF{D}:=e₂,s₀⟩ ==> ⟨THROW NoSuchFieldError,(h₂,l₂,sh₂)⟩"

| SFAssNonStatic:
  "[ P ⊨ ⟨e₂,s₀⟩ ==> ⟨Val v,(h₂,l₂,sh₂)⟩;
    P ⊨ C has F,NonStatic:t in D ]
  ==> P ⊨ ⟨C∙_sF{D}:=e₂,s₀⟩ ==> ⟨THROW IncompatibleClassChangeError,(h₂,l₂,sh₂)⟩"

| CallObjThrow:
  "P ⊨ ⟨e,s₀⟩ ==> ⟨throw e',s₁⟩ ==>
  P ⊨ ⟨e∙M(ps),s₀⟩ ==> ⟨throw e',s₁⟩"

| CallParamsThrow:
  "[ P ⊨ ⟨e,s₀⟩ ==> ⟨Val v,s₁⟩; P ⊨ ⟨es,s₁⟩ [==>] ⟨map Val vs @ throw ex # es',s₂⟩ ]
   ==> P ⊨ ⟨e∙M(es),s₀⟩ ==> ⟨throw ex,s₂⟩"

| CallNull:
  "[ P ⊨ ⟨e,s₀⟩ ==> ⟨null,s₁⟩; P ⊨ ⟨ps,s₁⟩ [==>] ⟨map Val vs,s₂⟩ ]
  ==> P ⊨ ⟨e∙M(ps),s₀⟩ ==> ⟨THROW NullPointer,s₂⟩"

| CallNone:
  "[ P ⊨ ⟨e,s₀⟩ ==> ⟨addr a,s₁⟩; P ⊨ ⟨ps,s₁⟩ [==>] ⟨map Val vs,(h₂,l₂,sh₂)⟩;
     h₂ a = Some(C,fs); ¬(∃b Ts T m D. P ⊨ C sees M,b:Ts→T = m in D) ]
  ==> P ⊨ ⟨e∙M(ps),s₀⟩ ==> ⟨THROW NoSuchMethodError,(h₂,l₂,sh₂)⟩"

| CallStatic:
  "[ P ⊨ ⟨e,s₀⟩ ==> ⟨addr a,s₁⟩; P ⊨ ⟨ps,s₁⟩ [==>] ⟨map Val vs,(h₂,l₂,sh₂)⟩;
     h₂ a = Some(C,fs); P ⊨ C sees M,Static:Ts→T = m in D ]
  ==> P ⊨ ⟨e∙M(ps),s₀⟩ ==> ⟨THROW IncompatibleClassChangeError,(h₂,l₂,sh₂)⟩"

| Call:
  "[ P ⊨ ⟨e,s₀⟩ ==> ⟨addr a,s₁⟩; P ⊨ ⟨ps,s₁⟩ [==>] ⟨map Val vs,(h₂,l₂,sh₂)⟩;
     h₂ a = Some(C,fs); P ⊨ C sees M,NonStatic:Ts→T = (pns,body) in D;
     length vs = length pns; l₂' = [this↦Addr a, pns[↦]vs];
     P ⊨ ⟨body,(h₂,l₂',sh₂)⟩ ==> ⟨e',(h₃,l₃,sh₃)⟩ ]
  ==> P ⊨ ⟨e∙M(ps),s₀⟩ ==> ⟨e',(h₃,l₂,sh₃)⟩"

| SCallParamsThrow:
  "[ P ⊨ ⟨es,s₀⟩ [==>] ⟨map Val vs @ throw ex # es',s₂⟩ ]
   ==> P ⊨ ⟨C∙_sM(es),s₀⟩ ==> ⟨throw ex,s₂⟩"

| SCallNone:
  "[ P ⊨ ⟨ps,s₀⟩ [==>] ⟨map Val vs,s₂⟩;
     ¬(∃b Ts T m D. P ⊨ C sees M,b:Ts→T = m in D) ]
  ==> P ⊨ ⟨C∙_sM(ps),s₀⟩ ==> ⟨THROW NoSuchMethodError,s₂⟩"

| SCallNonStatic:
  "[ P ⊨ ⟨ps,s₀⟩ [==>] ⟨map Val vs,s₂⟩;
     P ⊨ C sees M,NonStatic:Ts→T = m in D ]
  ==> P ⊨ ⟨C∙_sM(ps),s₀⟩ ==> ⟨THROW IncompatibleClassChangeError,s₂⟩"

| SCallInitThrow:
  "[ P ⊨ ⟨ps,s₀⟩ [==>] ⟨map Val vs,(h₁,l₁,sh₁)⟩;
     P ⊨ C sees M,Static:Ts→T = (pns,body) in D;
     ∄sfs. sh₁ D = Some(sfs,Done); M ≠ clinit;
     P ⊨ ⟨INIT D ([D],False) ← unit,(h₁,l₁,sh₁)⟩ ==> ⟨throw a,s'⟩ ]
  ==> P ⊨ ⟨C∙_sM(ps),s₀⟩ ==> ⟨throw a,s'⟩"

| SCallInit:
  "[ P ⊨ ⟨ps,s₀⟩ [==>] ⟨map Val vs,(h₁,l₁,sh₁)⟩;
     P ⊨ C sees M,Static:Ts→T = (pns,body) in D;
     ∄sfs. sh₁ D = Some(sfs,Done); M ≠ clinit;
     P ⊨ ⟨INIT D ([D],False) ← unit,(h₁,l₁,sh₁)⟩ ==> ⟨Val v',(h₂,l₂,sh₂)⟩;
     length vs = length pns; l₂' = [pns[↦]vs];
     P ⊨ ⟨body,(h₂,l₂',sh₂)⟩ ==> ⟨e',(h₃,l₃,sh₃)⟩ ]
  ==> P ⊨ ⟨C∙_sM(ps),s₀⟩ ==> ⟨e',(h₃,l₂,sh₃)⟩"

| SCall:
  "[ P ⊨ ⟨ps,s₀⟩ [==>] ⟨map Val vs,(h₂,l₂,sh₂)⟩;
     P ⊨ C sees M,Static:Ts→T = (pns,body) in D;
     sh₂ D = Some(sfs,Done) ∨ (M = clinit ∧ sh₂ D = Some(sfs,Processing));
     length vs = length pns; l₂' = [pns[↦]vs];
     P ⊨ ⟨body,(h₂,l₂',sh₂)⟩ ==> ⟨e',(h₃,l₃,sh₃)⟩ ]
  ==> P ⊨ ⟨C∙_sM(ps),s₀⟩ ==> ⟨e',(h₃,l₂,sh₃)⟩"

| Block:
  "P ⊨ ⟨e₀,(h₀,l₀(V:=None),sh₀)⟩ ==> ⟨e₁,(h₁,l₁,sh₁)⟩ ==>
  P ⊨ ⟨{V:T; e₀},(h₀,l₀,sh₀)⟩ ==> ⟨e₁,(h₁,l₁(V:=l₀ V),sh₁)⟩"

| Seq:
  "[ P ⊨ ⟨e₀,s₀⟩ ==> ⟨Val v,s₁⟩; P ⊨ ⟨e₁,s₁⟩ ==> ⟨e₂,s₂⟩ ]
  ==> P ⊨ ⟨e₀;;e₁,s₀⟩ ==> ⟨e₂,s₂⟩"

| SeqThrow:
  "P ⊨ ⟨e₀,s₀⟩ ==> ⟨throw e,s₁⟩ ==>
  P ⊨ ⟨e₀;;e₁,s₀⟩ ==> ⟨throw e,s₁⟩"

| CondT:
  "[ P ⊨ ⟨e,s₀⟩ ==> ⟨true,s₁⟩; P ⊨ ⟨e₁,s₁⟩ ==> ⟨e',s₂⟩ ]
  ==> P ⊨ ⟨if (e) e₁ else e₂,s₀⟩ ==> ⟨e',s₂⟩"

| CondF:
  "[ P ⊨ ⟨e,s₀⟩ ==> ⟨false,s₁⟩; P ⊨ ⟨e₂,s₁⟩ ==> ⟨e',s₂⟩ ]
  ==> P ⊨ ⟨if (e) e₁ else e₂,s₀⟩ ==> ⟨e',s₂⟩"

| CondThrow:
  "P ⊨ ⟨e,s₀⟩ ==> ⟨throw e',s₁⟩ ==>
  P ⊨ ⟨if (e) e₁ else e₂, s₀⟩ ==> ⟨throw e',s₁⟩"

| WhileF:
  "P ⊨ ⟨e,s₀⟩ ==> ⟨false,s₁⟩ ==>
  P ⊨ ⟨while (e) c,s₀⟩ ==> ⟨unit,s₁⟩"

| WhileT:
  "[ P ⊨ ⟨e,s₀⟩ ==> ⟨true,s₁⟩; P ⊨ ⟨c,s₁⟩ ==> ⟨Val v₁,s₂⟩; P ⊨ ⟨while (e) c,s₂⟩ ==> ⟨e₃,s₃⟩ ]
  ==> P ⊨ ⟨while (e) c,s₀⟩ ==> ⟨e₃,s₃⟩"

| WhileCondThrow:
  "P ⊨ ⟨e,s₀⟩ ==> ⟨throw e',s₁⟩ ==>
  P ⊨ ⟨while (e) c,s₀⟩ ==> ⟨throw e',s₁⟩"

| WhileBodyThrow:
  "[ P ⊨ ⟨e,s₀⟩ ==> ⟨true,s₁⟩; P ⊨ ⟨c,s₁⟩ ==> ⟨throw e',s₂⟩]
  ==> P ⊨ ⟨while (e) c,s₀⟩ ==> ⟨throw e',s₂⟩"

| Throw:
  "P ⊨ ⟨e,s₀⟩ ==> ⟨addr a,s₁⟩ ==>
  P ⊨ ⟨throw e,s₀⟩ ==> ⟨Throw a,s₁⟩"

| ThrowNull:
  "P ⊨ ⟨e,s₀⟩ ==> ⟨null,s₁⟩ ==>
  P ⊨ ⟨throw e,s₀⟩ ==> ⟨THROW NullPointer,s₁⟩"

| ThrowThrow:
  "P ⊨ ⟨e,s₀⟩ ==> ⟨throw e',s₁⟩ ==>
  P ⊨ ⟨throw e,s₀⟩ ==> ⟨throw e',s₁⟩"

| Try:
  "P ⊨ ⟨e₁,s₀⟩ ==> ⟨Val v₁,s₁⟩ ==>
  P ⊨ ⟨try e₁ catch(C V) e₂,s₀⟩ ==> ⟨Val v₁,s₁⟩"

| TryCatch:
  "[ P ⊨ ⟨e₁,s₀⟩ ==> ⟨Throw a,(h₁,l₁,sh₁)⟩; h₁ a = Some(D,fs); P ⊨ D ⪯^* C;
     P ⊨ ⟨e₂,(h₁,l₁(V↦Addr a),sh₁)⟩ ==> ⟨e₂',(h₂,l₂,sh₂)⟩ ]
  ==> P ⊨ ⟨try e₁ catch(C V) e₂,s₀⟩ ==> ⟨e₂',(h₂,l₂(V:=l₁ V),sh₂)⟩"

| TryThrow:
  "[ P ⊨ ⟨e₁,s₀⟩ ==> ⟨Throw a,(h₁,l₁,sh₁)⟩; h₁ a = Some(D,fs); ¬ P ⊨ D ⪯^* C ]
  ==> P ⊨ ⟨try e₁ catch(C V) e₂,s₀⟩ ==> ⟨Throw a,(h₁,l₁,sh₁)⟩"

| Nil:
  "P ⊨ ⟨[],s⟩ [==>] ⟨[],s⟩"

| Cons:
  "[ P ⊨ ⟨e,s₀⟩ ==> ⟨Val v,s₁⟩; P ⊨ ⟨es,s₁⟩ [==>] ⟨es',s₂⟩ ]
  ==> P ⊨ ⟨e#es,s₀⟩ [==>] ⟨Val v # es',s₂⟩"

| ConsThrow:
  "P ⊨ ⟨e, s₀⟩ ==> ⟨throw e', s₁⟩ ==>
  P ⊨ ⟨e#es, s₀⟩ [==>] ⟨throw e' # es, s₁⟩"

― ‹ 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₁,s₁⟩ ]
  ==> P ⊨ ⟨RI (C,e');Cs ← e,s⟩ ==> ⟨e₁,s₁⟩"

| 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₁,s₁⟩ ]
  ==> P ⊨ ⟨RI (C,e');D#Cs ← e,s⟩ ==> ⟨e₁,s₁⟩"

| 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₁ «bop¬ e₂,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₁∙F{D}:=e₂,s⟩ ==> ⟨e',s'⟩"
 "P ⊨ ⟨C∙_sF{D}:=e₂,s⟩ ==> ⟨e',s'⟩"
 "P ⊨ ⟨e∙M(es),s⟩ ==> ⟨e',s'⟩"
 "P ⊨ ⟨C∙_sM(es),s⟩ ==> ⟨e',s'⟩"
 "P ⊨ ⟨{V:T;e₁},s⟩ ==> ⟨e',s'⟩"
 "P ⊨ ⟨e₁;;e₂,s⟩ ==> ⟨e',s'⟩"
 "P ⊨ ⟨if (e) e₁ else e₂,s⟩ ==> ⟨e',s'⟩"
 "P ⊨ ⟨while (b) c,s⟩ ==> ⟨e',s'⟩"
 "P ⊨ ⟨throw e,s⟩ ==> ⟨e',s'⟩"
 "P ⊨ ⟨try e₁ catch(C V) e₂,s⟩ ==> ⟨e',s'⟩"
 "P ⊨ ⟨INIT C (Cs,b) ← e,s⟩ ==> ⟨e',s'⟩"
 "P ⊨ ⟨RI (C,e);Cs ← e₀,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
  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₁ es1 assume es1: "es' = Val v # es1"
      and estep: "P ⊨ ⟨e,s⟩ ==> ⟨Val v,s₁⟩" and esstep: "P ⊨ ⟨es,s₁⟩ [==>] ⟨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₀,l₀,sh₀)⟩ ==> ⟨e',(h₁,l₁,sh₁)⟩ ==> dom l₀ ⊆ dom l₁"
 and evals_lcl_incr: "P ⊨ ⟨es,(h₀,l₀,sh₀)⟩ [==>] ⟨es',(h₁,l₁,sh₁)⟩ ==> dom l₀ ⊆ dom l₁"
(*<*)
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 h₁ l₁ sh₁ C' M Ts T pns body D v' h₂ l₂ sh₂ l₂' e' h₃ l₃ sh₃)
  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₁ 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₁ 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₀,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₀,(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