Theory J1

(*  Title:      JinjaDCI/Compiler/J1.thy
    Author:     Tobias Nipkow, Susannah Mansky
    Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC

    Based on the Jinja theory Compiler/J1.thy by Tobias Nipkow
*)

chapter ‹ Compilation \label{cha:comp} ›

section ‹ An Intermediate Language ›

theory J1 imports "../J/BigStep" begin

type_synonym expr1 = "nat exp"
type_synonym J1_prog = "expr1 prog"
type_synonym state1 = "heap × (val list) × sheap"

definition hp1 :: "state1 ⇒ heap"
where
  "hp1  ≡  fst"
definition lcl1 :: "state1 ⇒ val list"
where
  "lcl1  ≡  fst ∘ snd"
definition shp1 :: "state1 ⇒ sheap"
where
  "shp1  ≡  snd ∘ snd"

(*<*)
declare hp1_def[simp] lcl1_def[simp] shp1_def[simp]
(*>*)

primrec
  max_vars :: "'a exp ⇒ nat"
  and max_varss :: "'a exp list ⇒ nat"
where
  "max_vars(new C) = 0"
| "max_vars(Cast C e) = max_vars e"
| "max_vars(Val v) = 0"
| "max_vars(e1 «bop» e2) = max (max_vars e1) (max_vars e2)"
| "max_vars(Var V) = 0"
| "max_vars(V:=e) = max_vars e"
| "max_vars(e∙F{D}) = max_vars e"
| "max_vars(C∙sF{D}) = 0"
| "max_vars(FAss e1 F D e2) = max (max_vars e1) (max_vars e2)"
| "max_vars(SFAss C F D e2) = max_vars e2"
| "max_vars(e∙M(es)) = max (max_vars e) (max_varss es)"
| "max_vars(C∙sM(es)) = max_varss es"
| "max_vars({V:T; e}) = max_vars e + 1"
| "max_vars(e1;;e2) = max (max_vars e1) (max_vars e2)"
| "max_vars(if (e) e1 else e2) =
   max (max_vars e) (max (max_vars e1) (max_vars e2))"
| "max_vars(while (b) e) = max (max_vars b) (max_vars e)"
| "max_vars(throw e) = max_vars e"
| "max_vars(try e1 catch(C V) e2) = max (max_vars e1) (max_vars e2 + 1)"
| "max_vars(INIT C (Cs,b) ← e) = max_vars e"
| "max_vars(RI(C,e);Cs ← e') = max (max_vars e) (max_vars e')"

| "max_varss [] = 0"
| "max_varss (e#es) = max (max_vars e) (max_varss es)"

inductive
  eval1 :: "J1_prog ⇒ expr1 ⇒ state1 ⇒ expr1 ⇒ state1 ⇒ bool"
          ("_ ⊢1 ((1⟨_,/_⟩) ⇒/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  and evals1 :: "J1_prog ⇒ expr1 list ⇒ state1 ⇒ expr1 list ⇒ state1 ⇒ bool"
           ("_ ⊢1 ((1⟨_,/_⟩) [⇒]/ (1⟨_,/_⟩))" [51,0,0,0,0] 81)
  for P :: J1_prog
where

  New1:
  "⟦ sh C = Some (sfs, Done); new_Addr h = Some a;
     P ⊢ C has_fields FDTs; h' = h(a↦blank P C) ⟧
  ⟹ P ⊢1 ⟨new C,(h,l,sh)⟩ ⇒ ⟨addr a,(h',l,sh)⟩"
| NewFail1:
  "⟦ sh C = Some (sfs, Done); new_Addr h = None ⟧ ⟹
  P ⊢1 ⟨new C, (h,l,sh)⟩ ⇒ ⟨THROW OutOfMemory,(h,l,sh)⟩"
| NewInit1:
  "⟦ ∄sfs. sh C = Some (sfs, Done); P ⊢1 ⟨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 ⊢1 ⟨new C,(h,l,sh)⟩ ⇒ ⟨addr a,(h'',l',sh')⟩"
| NewInitOOM1:
  "⟦ ∄sfs. sh C = Some (sfs, Done); P ⊢1 ⟨INIT C ([C],False) ← unit,(h,l,sh)⟩ ⇒ ⟨Val v',(h',l',sh')⟩;
     new_Addr h' = None; is_class P C ⟧
  ⟹ P ⊢1 ⟨new C,(h,l,sh)⟩ ⇒ ⟨THROW OutOfMemory,(h',l',sh')⟩"
| NewInitThrow1:
  "⟦ ∄sfs. sh C = Some (sfs, Done); P ⊢1 ⟨INIT C ([C],False) ← unit,(h,l,sh)⟩ ⇒ ⟨throw a,s'⟩;
     is_class P C ⟧
  ⟹ P ⊢1 ⟨new C,(h,l,sh)⟩ ⇒ ⟨throw a,s'⟩"

| Cast1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨addr a,(h,l,sh)⟩; h a = Some(D,fs); P ⊢ D ≼* C ⟧
  ⟹ P ⊢1 ⟨Cast C e,s0⟩ ⇒ ⟨addr a,(h,l,sh)⟩"
| CastNull1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨null,s1⟩ ⟹
  P ⊢1 ⟨Cast C e,s0⟩ ⇒ ⟨null,s1⟩"
| CastFail1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨addr a,(h,l,sh)⟩; h a = Some(D,fs); ¬ P ⊢ D ≼* C ⟧
  ⟹ P ⊢1 ⟨Cast C e,s0⟩ ⇒ ⟨THROW ClassCast,(h,l,sh)⟩"
| CastThrow1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢1 ⟨Cast C e,s0⟩ ⇒ ⟨throw e',s1⟩"

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

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

| Var1:
  "⟦ ls!i = v; i < size ls ⟧ ⟹
  P ⊢1 ⟨Var i,(h,ls,sh)⟩ ⇒ ⟨Val v,(h,ls,sh)⟩"

| LAss1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨Val v,(h,ls,sh)⟩; i < size ls; ls' = ls[i := v] ⟧
  ⟹ P ⊢1 ⟨i:= e,s0⟩ ⇒ ⟨unit,(h,ls',sh)⟩"
| LAssThrow1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢1 ⟨i:= e,s0⟩ ⇒ ⟨throw e',s1⟩"

| FAcc1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨addr a,(h,ls,sh)⟩; h a = Some(C,fs);
     P ⊢ C has F,NonStatic:t in D;
     fs(F,D) = Some v ⟧
  ⟹ P ⊢1 ⟨e∙F{D},s0⟩ ⇒ ⟨Val v,(h,ls,sh)⟩"
| FAccNull1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨null,s1⟩ ⟹
  P ⊢1 ⟨e∙F{D},s0⟩ ⇒ ⟨THROW NullPointer,s1⟩"
| FAccThrow1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢1 ⟨e∙F{D},s0⟩ ⇒ ⟨throw e',s1⟩"
| FAccNone1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨addr a,(h,ls,sh)⟩; h a = Some(C,fs);
    ¬(∃b t. P ⊢ C has F,b:t in D) ⟧
  ⟹ P ⊢1 ⟨e∙F{D},s0⟩ ⇒ ⟨THROW NoSuchFieldError,(h,ls,sh)⟩"
| FAccStatic1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨addr a,(h,ls,sh)⟩; h a = Some(C,fs);
    P ⊢ C has F,Static:t in D ⟧
  ⟹ P ⊢1 ⟨e∙F{D},s0⟩ ⇒ ⟨THROW IncompatibleClassChangeError,(h,ls,sh)⟩"

| SFAcc1:
  "⟦ P ⊢ C has F,Static:t in D;
     sh D = Some (sfs,Done);
     sfs F = Some v ⟧
  ⟹ P ⊢1 ⟨C∙sF{D},(h,ls,sh)⟩ ⇒ ⟨Val v,(h,ls,sh)⟩"
| SFAccInit1:
  "⟦ P ⊢ C has F,Static:t in D;
     ∄sfs. sh D = Some (sfs,Done); P ⊢1 ⟨INIT D ([D],False) ← unit,(h,ls,sh)⟩ ⇒ ⟨Val v',(h',ls',sh')⟩;
     sh' D = Some (sfs,i);
     sfs F = Some v ⟧
  ⟹ P ⊢1 ⟨C∙sF{D},(h,ls,sh)⟩ ⇒ ⟨Val v,(h',ls',sh')⟩"
| SFAccInitThrow1:
  "⟦ P ⊢ C has F,Static:t in D;
     ∄sfs. sh D = Some (sfs,Done); P ⊢1 ⟨INIT D ([D],False) ← unit,(h,ls,sh)⟩ ⇒ ⟨throw a,s'⟩ ⟧
  ⟹ P ⊢1 ⟨C∙sF{D},(h,ls,sh)⟩ ⇒ ⟨throw a,s'⟩"
| SFAccNone1:
  "⟦ ¬(∃b t. P ⊢ C has F,b:t in D) ⟧
  ⟹ P ⊢1 ⟨C∙sF{D},s⟩ ⇒ ⟨THROW NoSuchFieldError,s⟩"
| SFAccNonStatic1:
  "⟦ P ⊢ C has F,NonStatic:t in D ⟧
  ⟹ P ⊢1 ⟨C∙sF{D},s⟩ ⇒ ⟨THROW IncompatibleClassChangeError,s⟩"


| FAss1:
  "⟦ P ⊢1 ⟨e1,s0⟩ ⇒ ⟨addr a,s1⟩; P ⊢1 ⟨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 ⊢1 ⟨e1∙F{D}:=e2,s0⟩ ⇒ ⟨unit,(h2',l2,sh2)⟩"
| FAssNull1:
  "⟦ P ⊢1 ⟨e1,s0⟩ ⇒ ⟨null,s1⟩;  P ⊢1 ⟨e2,s1⟩ ⇒ ⟨Val v,s2⟩ ⟧ ⟹
  P ⊢1 ⟨e1∙F{D}:=e2,s0⟩ ⇒ ⟨THROW NullPointer,s2⟩"
| FAssThrow11:
  "P ⊢1 ⟨e1,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢1 ⟨e1∙F{D}:=e2,s0⟩ ⇒ ⟨throw e',s1⟩"
| FAssThrow21:
  "⟦ P ⊢1 ⟨e1,s0⟩ ⇒ ⟨Val v,s1⟩; P ⊢1 ⟨e2,s1⟩ ⇒ ⟨throw e',s2⟩ ⟧
  ⟹ P ⊢1 ⟨e1∙F{D}:=e2,s0⟩ ⇒ ⟨throw e',s2⟩"
| FAssNone1:
  "⟦ P ⊢1 ⟨e1,s0⟩ ⇒ ⟨addr a,s1⟩; P ⊢1 ⟨e2,s1⟩ ⇒ ⟨Val v,(h2,l2,sh2)⟩;
     h2 a = Some(C,fs); ¬(∃b t. P ⊢ C has F,b:t in D) ⟧
  ⟹ P ⊢1 ⟨e1∙F{D}:=e2,s0⟩ ⇒ ⟨THROW NoSuchFieldError,(h2,l2,sh2)⟩"
| FAssStatic1:
  "⟦ P ⊢1 ⟨e1,s0⟩ ⇒ ⟨addr a,s1⟩; P ⊢1 ⟨e2,s1⟩ ⇒ ⟨Val v,(h2,l2,sh2)⟩;
     h2 a = Some(C,fs); P ⊢ C has F,Static:t in D ⟧
  ⟹ P ⊢1 ⟨e1∙F{D}:=e2,s0⟩ ⇒ ⟨THROW IncompatibleClassChangeError,(h2,l2,sh2)⟩"

| SFAss1:
  "⟦ P ⊢1 ⟨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 ⊢1 ⟨C∙sF{D}:=e2,s0⟩ ⇒ ⟨unit,(h1,l1,sh1')⟩"
| SFAssInit1:
  "⟦ P ⊢1 ⟨e2,s0⟩ ⇒ ⟨Val v,(h1,l1,sh1)⟩;
     P ⊢ C has F,Static:t in D;
     ∄sfs. sh1 D = Some(sfs,Done); P ⊢1 ⟨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 ⊢1 ⟨C∙sF{D}:=e2,s0⟩ ⇒ ⟨unit,(h',l',sh'')⟩"
| SFAssInitThrow1:
  "⟦ P ⊢1 ⟨e2,s0⟩ ⇒ ⟨Val v,(h1,l1,sh1)⟩;
     P ⊢ C has F,Static:t in D;
     ∄sfs. sh1 D = Some(sfs,Done); P ⊢1 ⟨INIT D ([D],False) ← unit,(h1,l1,sh1)⟩ ⇒ ⟨throw a,s'⟩ ⟧
  ⟹ P ⊢1 ⟨C∙sF{D}:=e2,s0⟩ ⇒ ⟨throw a,s'⟩"
| SFAssThrow1:
  "P ⊢1 ⟨e2,s0⟩ ⇒ ⟨throw e',s2⟩
  ⟹ P ⊢1 ⟨C∙sF{D}:=e2,s0⟩ ⇒ ⟨throw e',s2⟩"
| SFAssNone1:
  "⟦ P ⊢1 ⟨e2,s0⟩ ⇒ ⟨Val v,(h2,l2,sh2)⟩;
    ¬(∃b t. P ⊢ C has F,b:t in D) ⟧
  ⟹ P ⊢1 ⟨C∙sF{D}:=e2,s0⟩ ⇒ ⟨THROW NoSuchFieldError,(h2,l2,sh2)⟩"
| SFAssNonStatic1:
  "⟦ P ⊢1 ⟨e2,s0⟩ ⇒ ⟨Val v,(h2,l2,sh2)⟩;
    P ⊢ C has F,NonStatic:t in D ⟧
  ⟹ P ⊢1 ⟨C∙sF{D}:=e2,s0⟩ ⇒ ⟨THROW IncompatibleClassChangeError,(h2,l2,sh2)⟩"

| CallObjThrow1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢1 ⟨e∙M(es),s0⟩ ⇒ ⟨throw e',s1⟩"
| CallNull1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨null,s1⟩; P ⊢1 ⟨es,s1⟩ [⇒] ⟨map Val vs,s2⟩ ⟧
  ⟹ P ⊢1 ⟨e∙M(es),s0⟩ ⇒ ⟨THROW NullPointer,s2⟩"
| Call1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨addr a,s1⟩; P ⊢1 ⟨es,s1⟩ [⇒] ⟨map Val vs,(h2,ls2,sh2)⟩;
    h2 a = Some(C,fs); P ⊢ C sees M,NonStatic:Ts→T = body in D;
    size vs = size Ts; ls2' = (Addr a) # vs @ replicate (max_vars body) undefined;
    P ⊢1 ⟨body,(h2,ls2',sh2)⟩ ⇒ ⟨e',(h3,ls3,sh3)⟩ ⟧
  ⟹ P ⊢1 ⟨e∙M(es),s0⟩ ⇒ ⟨e',(h3,ls2,sh3)⟩"
| CallParamsThrow1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨Val v,s1⟩; P ⊢1 ⟨es,s1⟩ [⇒] ⟨es',s2⟩;
     es' = map Val vs @ throw ex # es2 ⟧
   ⟹ P ⊢1 ⟨e∙M(es),s0⟩ ⇒ ⟨throw ex,s2⟩"
| CallNone1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨addr a,s1⟩;  P ⊢1 ⟨ps,s1⟩ [⇒] ⟨map Val vs,(h2,ls2,sh2)⟩;
     h2 a = Some(C,fs); ¬(∃b Ts T body D. P ⊢ C sees M,b:Ts→T = body in D) ⟧
  ⟹ P ⊢1 ⟨e∙M(ps),s0⟩ ⇒ ⟨THROW NoSuchMethodError,(h2,ls2,sh2)⟩"
| CallStatic1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨addr a,s1⟩;  P ⊢1 ⟨ps,s1⟩ [⇒] ⟨map Val vs,(h2,ls2,sh2)⟩;
     h2 a = Some(C,fs); P ⊢ C sees M,Static:Ts→T = body in D ⟧
  ⟹ P ⊢1 ⟨e∙M(ps),s0⟩ ⇒ ⟨THROW IncompatibleClassChangeError,(h2,ls2,sh2)⟩"

| SCallParamsThrow1:
  "⟦ P ⊢1 ⟨es,s0⟩ [⇒] ⟨es',s2⟩; es' = map Val vs @ throw ex # es2 ⟧
   ⟹ P ⊢1 ⟨C∙sM(es),s0⟩ ⇒ ⟨throw ex,s2⟩"
| SCallNone1:
  "⟦ P ⊢1 ⟨ps,s0⟩ [⇒] ⟨map Val vs,s2⟩;
     ¬(∃b Ts T body D. P ⊢ C sees M,b:Ts→T = body in D) ⟧
  ⟹ P ⊢1 ⟨C∙sM(ps),s0⟩ ⇒ ⟨THROW NoSuchMethodError,s2⟩"
| SCallNonStatic1:
  "⟦ P ⊢1 ⟨ps,s0⟩ [⇒] ⟨map Val vs,s2⟩;
     P ⊢ C sees M,NonStatic:Ts→T = body in D ⟧
  ⟹ P ⊢1 ⟨C∙sM(ps),s0⟩ ⇒ ⟨THROW IncompatibleClassChangeError,s2⟩"
| SCallInitThrow1:
  "⟦ P ⊢1 ⟨ps,s0⟩ [⇒] ⟨map Val vs,(h1,ls1,sh1)⟩;
     P ⊢ C sees M,Static:Ts→T = body in D;
     ∄sfs. sh1 D = Some(sfs,Done); M ≠ clinit;
     P ⊢1 ⟨INIT D ([D],False) ← unit,(h1,ls1,sh1)⟩ ⇒ ⟨throw a,s'⟩ ⟧
  ⟹ P ⊢1 ⟨C∙sM(ps),s0⟩ ⇒ ⟨throw a,s'⟩"
| SCallInit1:
  "⟦ P ⊢1 ⟨ps,s0⟩ [⇒] ⟨map Val vs,(h1,ls1,sh1)⟩;
     P ⊢ C sees M,Static:Ts→T = body in D;
     ∄sfs. sh1 D = Some(sfs,Done); M ≠ clinit;
     P ⊢1 ⟨INIT D ([D],False) ← unit,(h1,ls1,sh1)⟩ ⇒ ⟨Val v',(h2,ls2,sh2)⟩;
     size vs = size Ts; ls2' = vs @ replicate (max_vars body) undefined;
     P ⊢1 ⟨body,(h2,ls2',sh2)⟩ ⇒ ⟨e',(h3,ls3,sh3)⟩ ⟧
  ⟹ P ⊢1 ⟨C∙sM(ps),s0⟩ ⇒ ⟨e',(h3,ls2,sh3)⟩"
| SCall1:
  "⟦ P ⊢1 ⟨ps,s0⟩ [⇒] ⟨map Val vs,(h2,ls2,sh2)⟩;
     P ⊢ C sees M,Static:Ts→T = body in D;
     sh2 D = Some(sfs,Done) ∨ (M = clinit ∧ sh2 D = ⌊(sfs, Processing)⌋);
     size vs = size Ts; ls2' = vs @ replicate (max_vars body) undefined;
     P ⊢1 ⟨body,(h2,ls2',sh2)⟩ ⇒ ⟨e',(h3,ls3,sh3)⟩ ⟧
  ⟹ P ⊢1 ⟨C∙sM(ps),s0⟩ ⇒ ⟨e',(h3,ls2,sh3)⟩"

| Block1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨e',s1⟩ ⟹ P ⊢1 ⟨Block i T e,s0⟩ ⇒ ⟨e',s1⟩"

| Seq1:
  "⟦ P ⊢1 ⟨e0,s0⟩ ⇒ ⟨Val v,s1⟩; P ⊢1 ⟨e1,s1⟩ ⇒ ⟨e2,s2⟩ ⟧
  ⟹ P ⊢1 ⟨e0;;e1,s0⟩ ⇒ ⟨e2,s2⟩"
| SeqThrow1:
  "P ⊢1 ⟨e0,s0⟩ ⇒ ⟨throw e,s1⟩ ⟹
  P ⊢1 ⟨e0;;e1,s0⟩ ⇒ ⟨throw e,s1⟩"

| CondT1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨true,s1⟩; P ⊢1 ⟨e1,s1⟩ ⇒ ⟨e',s2⟩ ⟧
  ⟹ P ⊢1 ⟨if (e) e1 else e2,s0⟩ ⇒ ⟨e',s2⟩"
| CondF1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨false,s1⟩; P ⊢1 ⟨e2,s1⟩ ⇒ ⟨e',s2⟩ ⟧
  ⟹ P ⊢1 ⟨if (e) e1 else e2,s0⟩ ⇒ ⟨e',s2⟩"
| CondThrow1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢1 ⟨if (e) e1 else e2, s0⟩ ⇒ ⟨throw e',s1⟩"

| WhileF1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨false,s1⟩ ⟹
  P ⊢1 ⟨while (e) c,s0⟩ ⇒ ⟨unit,s1⟩"
| WhileT1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨true,s1⟩; P ⊢1 ⟨c,s1⟩ ⇒ ⟨Val v1,s2⟩;
    P ⊢1 ⟨while (e) c,s2⟩ ⇒ ⟨e3,s3⟩ ⟧
  ⟹ P ⊢1 ⟨while (e) c,s0⟩ ⇒ ⟨e3,s3⟩"
| WhileCondThrow1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢1 ⟨while (e) c,s0⟩ ⇒ ⟨throw e',s1⟩"
| WhileBodyThrow1:
  "⟦ P ⊢1 ⟨e,s0⟩ ⇒ ⟨true,s1⟩; P ⊢1 ⟨c,s1⟩ ⇒ ⟨throw e',s2⟩⟧
  ⟹ P ⊢1 ⟨while (e) c,s0⟩ ⇒ ⟨throw e',s2⟩"

| Throw1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨addr a,s1⟩ ⟹
  P ⊢1 ⟨throw e,s0⟩ ⇒ ⟨Throw a,s1⟩"
| ThrowNull1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨null,s1⟩ ⟹
  P ⊢1 ⟨throw e,s0⟩ ⇒ ⟨THROW NullPointer,s1⟩"
| ThrowThrow1:
  "P ⊢1 ⟨e,s0⟩ ⇒ ⟨throw e',s1⟩ ⟹
  P ⊢1 ⟨throw e,s0⟩ ⇒ ⟨throw e',s1⟩"

| Try1:
  "P ⊢1 ⟨e1,s0⟩ ⇒ ⟨Val v1,s1⟩ ⟹
  P ⊢1 ⟨try e1 catch(C i) e2,s0⟩ ⇒ ⟨Val v1,s1⟩"
| TryCatch1:
  "⟦ P ⊢1 ⟨e1,s0⟩ ⇒ ⟨Throw a,(h1,ls1,sh1)⟩;
    h1 a = Some(D,fs); P ⊢ D ≼* C; i < length ls1;
    P ⊢1 ⟨e2,(h1,ls1[i:=Addr a],sh1)⟩ ⇒ ⟨e2',(h2,ls2,sh2)⟩ ⟧
  ⟹ P ⊢1 ⟨try e1 catch(C i) e2,s0⟩ ⇒ ⟨e2',(h2,ls2,sh2)⟩"
| TryThrow1:
  "⟦ P ⊢1 ⟨e1,s0⟩ ⇒ ⟨Throw a,(h1,ls1,sh1)⟩; h1 a = Some(D,fs); ¬ P ⊢ D ≼* C ⟧
  ⟹ P ⊢1 ⟨try e1 catch(C i) e2,s0⟩ ⇒ ⟨Throw a,(h1,ls1,sh1)⟩"

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

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

― ‹ init rules ›

| InitFinal1:
  "P ⊢1 ⟨e,s⟩ ⇒ ⟨e',s'⟩ ⟹ P ⊢1 ⟨INIT C (Nil,b) ← e,s⟩ ⇒ ⟨e',s'⟩"
| InitNone1:
  "⟦ sh C = None; P ⊢1 ⟨INIT C' (C#Cs,False) ← e,(h,l,sh(C ↦ (sblank P C, Prepared)))⟩ ⇒ ⟨e',s'⟩ ⟧
  ⟹ P ⊢1 ⟨INIT C' (C#Cs,False) ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩"
| InitDone1:
  "⟦ sh C = Some(sfs,Done); P ⊢1 ⟨INIT C' (Cs,True) ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩ ⟧
  ⟹ P ⊢1 ⟨INIT C' (C#Cs,False) ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩"
| InitProcessing1:
  "⟦ sh C = Some(sfs,Processing); P ⊢1 ⟨INIT C' (Cs,True) ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩ ⟧
  ⟹ P ⊢1 ⟨INIT C' (C#Cs,False) ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩"
| InitError1:
  "⟦ sh C = Some(sfs,Error);
     P ⊢1 ⟨RI (C, THROW NoClassDefFoundError);Cs ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩ ⟧
  ⟹ P ⊢1 ⟨INIT C' (C#Cs,False) ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩"
| InitObject1:
  "⟦ sh C = Some(sfs,Prepared);
     C = Object;
     sh' = sh(C ↦ (sfs,Processing));
     P ⊢1 ⟨INIT C' (C#Cs,True) ← e,(h,l,sh')⟩ ⇒ ⟨e',s'⟩ ⟧
  ⟹ P ⊢1 ⟨INIT C' (C#Cs,False) ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩"
| InitNonObject1:
  "⟦ sh C = Some(sfs,Prepared);
     C ≠ Object;
     class P C = Some (D,r);
     sh' = sh(C ↦ (sfs,Processing));
     P ⊢1 ⟨INIT C' (D#C#Cs,False) ← e,(h,l,sh')⟩ ⇒ ⟨e',s'⟩ ⟧
  ⟹ P ⊢1 ⟨INIT C' (C#Cs,False) ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩"
| InitRInit1:
  "P ⊢1 ⟨RI (C,C∙sclinit([]));Cs ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩
  ⟹ P ⊢1 ⟨INIT C' (C#Cs,True) ← e,(h,l,sh)⟩ ⇒ ⟨e',s'⟩"

| RInit1:
  "⟦ P ⊢1 ⟨e,s⟩ ⇒ ⟨Val v, (h',l',sh')⟩;
     sh' C = Some(sfs, i); sh'' = sh'(C ↦ (sfs, Done));
     C' = last(C#Cs);
     P ⊢1 ⟨INIT C' (Cs,True) ← e', (h',l',sh'')⟩ ⇒ ⟨e1,s1⟩ ⟧
  ⟹ P ⊢1 ⟨RI (C,e);Cs ← e',s⟩ ⇒ ⟨e1,s1⟩"
| RInitInitFail1:
  "⟦ P ⊢1 ⟨e,s⟩ ⇒ ⟨throw a, (h',l',sh')⟩;
     sh' C = Some(sfs, i); sh'' = sh'(C ↦ (sfs, Error));
     P ⊢1 ⟨RI (D,throw a);Cs ← e', (h',l',sh'')⟩ ⇒ ⟨e1,s1⟩ ⟧
  ⟹ P ⊢1 ⟨RI (C,e);D#Cs ← e',s⟩ ⇒ ⟨e1,s1⟩"
| RInitFailFinal1:
  "⟦ P ⊢1 ⟨e,s⟩ ⇒ ⟨throw a, (h',l',sh')⟩;
     sh' C = Some(sfs, i); sh'' = sh'(C ↦ (sfs, Error)) ⟧
  ⟹ P ⊢1 ⟨RI (C,e);Nil ← e',s⟩ ⇒ ⟨throw a, (h',l',sh'')⟩"


(*<*)
lemmas eval1_evals1_induct = eval1_evals1.induct [split_format (complete)]
  and eval1_evals1_inducts = eval1_evals1.inducts [split_format (complete)]
(*>*)


inductive_cases eval1_cases [cases set]:
 "P ⊢1 ⟨new C,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢1 ⟨Cast C e,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢1 ⟨Val v,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢1 ⟨e1 «bop» e2,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢1 ⟨Var v,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢1 ⟨V:=e,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢1 ⟨e∙F{D},s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢1 ⟨C∙sF{D},s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢1 ⟨e1∙F{D}:=e2,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢1 ⟨C∙sF{D}:=e2,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢1 ⟨e∙M(es),s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢1 ⟨C∙sM(es),s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢1 ⟨{V:T;e1},s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢1 ⟨e1;;e2,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢1 ⟨if (e) e1 else e2,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢1 ⟨while (b) c,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢1 ⟨throw e,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢1 ⟨try e1 catch(C V) e2,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢1 ⟨INIT C (Cs,b) ← e,s⟩ ⇒ ⟨e',s'⟩"
 "P ⊢1 ⟨RI (C,e);Cs ← e0,s⟩ ⇒ ⟨e',s'⟩"
 
inductive_cases evals1_cases [cases set]:
 "P ⊢1 ⟨[],s⟩ [⇒] ⟨e',s'⟩"
 "P ⊢1 ⟨e#es,s⟩ [⇒] ⟨e',s'⟩"
(*>*) 


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


lemma eval1_final_same:
assumes eval: "P ⊢1 ⟨e,s⟩ ⇒ ⟨e',s'⟩" shows "final e ⟹ e = e' ∧ s = s'"
(*<*)
proof(erule finalE)
  fix v assume Val: "e = Val v"
  then show ?thesis using eval eval1_cases(3) by blast
next
  fix a assume "e = Throw a"
  then show ?thesis using eval
    by (metis eval1_cases(3,17) exp.distinct(101) exp.inject(3) val.distinct(13))
qed
(*>*)

subsection "Property preservation"

lemma eval1_preserves_len:
  "P ⊢1 ⟨e0,(h0,ls0,sh0)⟩ ⇒ ⟨e1,(h1,ls1,sh1)⟩ ⟹ length ls0 = length ls1"
and evals1_preserves_len:
  "P ⊢1 ⟨es0,(h0,ls0,sh0)⟩ [⇒] ⟨es1,(h1,ls1,sh1)⟩ ⟹ length ls0 = length ls1"
(*<*)by (induct rule:eval1_evals1_inducts, simp_all)(*>*)


lemma evals1_preserves_elen:
  "⋀es' s s'. P ⊢1 ⟨es,s⟩ [⇒] ⟨es',s'⟩ ⟹ length es = length es'"
(*<*)by(induct es type:list) (auto elim:evals1.cases)(*>*)


lemma clinit1_loc_pres:
 "P ⊢1 ⟨C0∙sclinit([]),(h,l,sh)⟩ ⇒ ⟨e',(h',l',sh')⟩ ⟹ l = l'"
 by(auto elim!: eval1_cases(12) evals1_cases(1))

lemma
shows init1_ri1_same_loc: "P ⊢1 ⟨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 ⊢1 ⟨es,(h,l,sh)⟩ [⇒] ⟨es',(h',l',sh')⟩ ⟹ True"
proof(induct rule: eval1_evals1_inducts)
  case (RInitInitFail1 e h l sh a')
  then show ?case using eval1_final[of _ _ _ "throw a'"]
     by(fastforce dest: eval1_final_same[of _ "Throw a"])
next
  case RInitFailFinal1 then show ?case by(auto dest: eval1_final_same)
qed(auto dest: evals1_cases eval1_cases(17) eval1_final_same)

lemma init1_same_loc: "P ⊢1 ⟨INIT C (Cs,b) ← unit,(h,l,sh)⟩ ⇒ ⟨e',(h',l',sh')⟩ ⟹ l = l'"
 by(simp add: init1_ri1_same_loc)


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

subsection "Initialization"

lemma rinit1_throw:
 "P1 ⊢1 ⟨RI (D,Throw xa) ; Cs ← e,(h, l, sh)⟩ ⇒ ⟨e',(h', l', sh')⟩
    ⟹ e' = Throw xa"
proof(induct Cs arbitrary: D h l sh h' l' sh')
  case Nil then show ?case
  proof(rule eval1_cases(20)) qed(auto elim: eval1_cases)
next
  case (Cons C Cs) show ?case using Cons.prems
  proof(induct rule: eval1_cases(20))
    case RInit1: 1
    then show ?case using Cons.hyps by(auto elim: eval1_cases)
  next
    case RInitInitFail1: 2
    then show ?case using Cons.hyps eval1_final_same final_def by blast
  next
    case RInitFailFinal1: 3 then show ?case by simp
  qed
qed

lemma rinit1_throwE:
"P ⊢1 ⟨RI (C,throw e) ; Cs ← e0,s⟩ ⇒ ⟨e',s'⟩
   ⟹ ∃a st. e' = throw a ∧ P ⊢1 ⟨throw e,s⟩ ⇒ ⟨throw a,st⟩"
proof(induct Cs arbitrary: C e s)
  case Nil
  then show ?case
  proof(rule eval1_cases(20)) ― ‹ RI ›
    fix v h' l' sh' assume "P ⊢1 ⟨throw e,s⟩ ⇒ ⟨Val v,(h', l', sh')⟩"
    then show ?case using eval1_cases(17) by blast
  qed(auto)
next
  case (Cons C' Cs')
  show ?case using Cons.prems(1)
  proof(rule eval1_cases(20)) ― ‹ RI ›
    fix v h' l' sh' assume "P ⊢1 ⟨throw e,s⟩ ⇒ ⟨Val v,(h', l', sh')⟩"
    then show ?case using eval1_cases(17) by blast
  next
    fix a h' l' sh' sfs i D Cs''
    assume e''step: "P ⊢1 ⟨throw e,s⟩ ⇒ ⟨throw a,(h', l', sh')⟩"
       and shC: "sh' C = ⌊(sfs, i)⌋"
       and riD: "P ⊢1 ⟨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 eval1_final eval1_final_same by blast
  qed(simp)
qed

end