# 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 expr⇩1 = "nat exp"
type_synonym J⇩1_prog = "expr⇩1 prog"
type_synonym state⇩1 = "heap × (val list) × sheap"

definition hp⇩1 :: "state⇩1 ⇒ heap"
where
"hp⇩1  ≡  fst"
definition lcl⇩1 :: "state⇩1 ⇒ val list"
where
"lcl⇩1  ≡  fst ∘ snd"
definition shp⇩1 :: "state⇩1 ⇒ sheap"
where
"shp⇩1  ≡  snd ∘ snd"

(*<*)
declare hp⇩1_def[simp] lcl⇩1_def[simp] shp⇩1_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(e⇩1 «bop» e⇩2) = max (max_vars e⇩1) (max_vars e⇩2)"
| "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 e⇩1 F D e⇩2) = max (max_vars e⇩1) (max_vars e⇩2)"
| "max_vars(SFAss C F D e⇩2) = max_vars e⇩2"
| "max_vars(e∙M(es)) = max (max_vars e) (max_varss es)"
| "max_vars({V:T; e}) = max_vars e + 1"
| "max_vars(e⇩1;;e⇩2) = max (max_vars e⇩1) (max_vars e⇩2)"
| "max_vars(if (e) e⇩1 else e⇩2) =
max (max_vars e) (max (max_vars e⇩1) (max_vars e⇩2))"
| "max_vars(while (b) e) = max (max_vars b) (max_vars e)"
| "max_vars(throw e) = max_vars e"
| "max_vars(try e⇩1 catch(C V) e⇩2) = max (max_vars e⇩1) (max_vars e⇩2 + 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')"

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

New⇩1:
"⟦ 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)⟩"
| NewFail⇩1:
"⟦ sh C = Some (sfs, Done); new_Addr h = None ⟧ ⟹
P ⊢⇩1 ⟨new C, (h,l,sh)⟩ ⇒ ⟨THROW OutOfMemory,(h,l,sh)⟩"
| NewInit⇩1:
"⟦ ∄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')⟩"
| NewInitOOM⇩1:
"⟦ ∄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')⟩"
| NewInitThrow⇩1:
"⟦ ∄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'⟩"

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

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

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

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

| LAss⇩1:
"⟦ P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨Val v,(h,ls,sh)⟩; i < size ls; ls' = ls[i := v] ⟧
⟹ P ⊢⇩1 ⟨i:= e,s⇩0⟩ ⇒ ⟨unit,(h,ls',sh)⟩"
| LAssThrow⇩1:
"P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P ⊢⇩1 ⟨i:= e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"

| FAcc⇩1:
"⟦ P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨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},s⇩0⟩ ⇒ ⟨Val v,(h,ls,sh)⟩"
| FAccNull⇩1:
"P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩ ⟹
P ⊢⇩1 ⟨e∙F{D},s⇩0⟩ ⇒ ⟨THROW NullPointer,s⇩1⟩"
| FAccThrow⇩1:
"P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P ⊢⇩1 ⟨e∙F{D},s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"
| FAccNone⇩1:
"⟦ P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨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},s⇩0⟩ ⇒ ⟨THROW NoSuchFieldError,(h,ls,sh)⟩"
| FAccStatic⇩1:
"⟦ P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨addr a,(h,ls,sh)⟩; h a = Some(C,fs);
P ⊢ C has F,Static:t in D ⟧
⟹ P ⊢⇩1 ⟨e∙F{D},s⇩0⟩ ⇒ ⟨THROW IncompatibleClassChangeError,(h,ls,sh)⟩"

| SFAcc⇩1:
"⟦ 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)⟩"
| SFAccInit⇩1:
"⟦ 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')⟩"
| SFAccInitThrow⇩1:
"⟦ 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'⟩"
| SFAccNone⇩1:
"⟦ ¬(∃b t. P ⊢ C has F,b:t in D) ⟧
⟹ P ⊢⇩1 ⟨C∙⇩sF{D},s⟩ ⇒ ⟨THROW NoSuchFieldError,s⟩"
| SFAccNonStatic⇩1:
"⟦ P ⊢ C has F,NonStatic:t in D ⟧
⟹ P ⊢⇩1 ⟨C∙⇩sF{D},s⟩ ⇒ ⟨THROW IncompatibleClassChangeError,s⟩"

| FAss⇩1:
"⟦ P ⊢⇩1 ⟨e⇩1,s⇩0⟩ ⇒ ⟨addr a,s⇩1⟩; P ⊢⇩1 ⟨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 ⊢⇩1 ⟨e⇩1∙F{D}:=e⇩2,s⇩0⟩ ⇒ ⟨unit,(h⇩2',l⇩2,sh⇩2)⟩"
| FAssNull⇩1:
"⟦ P ⊢⇩1 ⟨e⇩1,s⇩0⟩ ⇒ ⟨null,s⇩1⟩;  P ⊢⇩1 ⟨e⇩2,s⇩1⟩ ⇒ ⟨Val v,s⇩2⟩ ⟧ ⟹
P ⊢⇩1 ⟨e⇩1∙F{D}:=e⇩2,s⇩0⟩ ⇒ ⟨THROW NullPointer,s⇩2⟩"
| FAssThrow⇩1⇩1:
"P ⊢⇩1 ⟨e⇩1,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P ⊢⇩1 ⟨e⇩1∙F{D}:=e⇩2,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"
| FAssThrow⇩2⇩1:
"⟦ P ⊢⇩1 ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val v,s⇩1⟩; P ⊢⇩1 ⟨e⇩2,s⇩1⟩ ⇒ ⟨throw e',s⇩2⟩ ⟧
⟹ P ⊢⇩1 ⟨e⇩1∙F{D}:=e⇩2,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
| FAssNone⇩1:
"⟦ P ⊢⇩1 ⟨e⇩1,s⇩0⟩ ⇒ ⟨addr a,s⇩1⟩; P ⊢⇩1 ⟨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 ⊢⇩1 ⟨e⇩1∙F{D}:=e⇩2,s⇩0⟩ ⇒ ⟨THROW NoSuchFieldError,(h⇩2,l⇩2,sh⇩2)⟩"
| FAssStatic⇩1:
"⟦ P ⊢⇩1 ⟨e⇩1,s⇩0⟩ ⇒ ⟨addr a,s⇩1⟩; P ⊢⇩1 ⟨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 ⊢⇩1 ⟨e⇩1∙F{D}:=e⇩2,s⇩0⟩ ⇒ ⟨THROW IncompatibleClassChangeError,(h⇩2,l⇩2,sh⇩2)⟩"

| SFAss⇩1:
"⟦ P ⊢⇩1 ⟨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 ⊢⇩1 ⟨C∙⇩sF{D}:=e⇩2,s⇩0⟩ ⇒ ⟨unit,(h⇩1,l⇩1,sh⇩1')⟩"
| SFAssInit⇩1:
"⟦ P ⊢⇩1 ⟨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 ⊢⇩1 ⟨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 ⊢⇩1 ⟨C∙⇩sF{D}:=e⇩2,s⇩0⟩ ⇒ ⟨unit,(h',l',sh'')⟩"
| SFAssInitThrow⇩1:
"⟦ P ⊢⇩1 ⟨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 ⊢⇩1 ⟨INIT D ([D],False) ← unit,(h⇩1,l⇩1,sh⇩1)⟩ ⇒ ⟨throw a,s'⟩ ⟧
⟹ P ⊢⇩1 ⟨C∙⇩sF{D}:=e⇩2,s⇩0⟩ ⇒ ⟨throw a,s'⟩"
| SFAssThrow⇩1:
"P ⊢⇩1 ⟨e⇩2,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩
⟹ P ⊢⇩1 ⟨C∙⇩sF{D}:=e⇩2,s⇩0⟩ ⇒ ⟨throw e',s⇩2⟩"
| SFAssNone⇩1:
"⟦ P ⊢⇩1 ⟨e⇩2,s⇩0⟩ ⇒ ⟨Val v,(h⇩2,l⇩2,sh⇩2)⟩;
¬(∃b t. P ⊢ C has F,b:t in D) ⟧
⟹ P ⊢⇩1 ⟨C∙⇩sF{D}:=e⇩2,s⇩0⟩ ⇒ ⟨THROW NoSuchFieldError,(h⇩2,l⇩2,sh⇩2)⟩"
| SFAssNonStatic⇩1:
"⟦ P ⊢⇩1 ⟨e⇩2,s⇩0⟩ ⇒ ⟨Val v,(h⇩2,l⇩2,sh⇩2)⟩;
P ⊢ C has F,NonStatic:t in D ⟧
⟹ P ⊢⇩1 ⟨C∙⇩sF{D}:=e⇩2,s⇩0⟩ ⇒ ⟨THROW IncompatibleClassChangeError,(h⇩2,l⇩2,sh⇩2)⟩"

| CallObjThrow⇩1:
"P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩ ⟹
P ⊢⇩1 ⟨e∙M(es),s⇩0⟩ ⇒ ⟨throw e',s⇩1⟩"
| CallNull⇩1:
"⟦ P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨null,s⇩1⟩; P ⊢⇩1 ⟨es,s⇩1⟩ [⇒] ⟨map Val vs,s⇩2⟩ ⟧
⟹ P ⊢⇩1 ⟨e∙M(es),s⇩0⟩ ⇒ ⟨THROW NullPointer,s⇩2⟩"
| Call⇩1:
"⟦ P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨addr a,s⇩1⟩; P ⊢⇩1 ⟨es,s⇩1⟩ [⇒] ⟨map Val vs,(h⇩2,ls⇩2,sh⇩2)⟩;
h⇩2 a = Some(C,fs); P ⊢ C sees M,NonStatic:Ts→T = body in D;
size vs = size Ts; ls⇩2' = (Addr a) # vs @ replicate (max_vars body) undefined;
P ⊢⇩1 ⟨body,(h⇩2,ls⇩2',sh⇩2)⟩ ⇒ ⟨e',(h⇩3,ls⇩3,sh⇩3)⟩ ⟧
⟹ P ⊢⇩1 ⟨e∙M(es),s⇩0⟩ ⇒ ⟨e',(h⇩3,ls⇩2,sh⇩3)⟩"
| CallParamsThrow⇩1:
"⟦ P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨Val v,s⇩1⟩; P ⊢⇩1 ⟨es,s⇩1⟩ [⇒] ⟨es',s⇩2⟩;
es' = map Val vs @ throw ex # es⇩2 ⟧
⟹ P ⊢⇩1 ⟨e∙M(es),s⇩0⟩ ⇒ ⟨throw ex,s⇩2⟩"
| CallNone⇩1:
"⟦ P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨addr a,s⇩1⟩;  P ⊢⇩1 ⟨ps,s⇩1⟩ [⇒] ⟨map Val vs,(h⇩2,ls⇩2,sh⇩2)⟩;
h⇩2 a = Some(C,fs); ¬(∃b Ts T body D. P ⊢ C sees M,b:Ts→T = body in D) ⟧
⟹ P ⊢⇩1 ⟨e∙M(ps),s⇩0⟩ ⇒ ⟨THROW NoSuchMethodError,(h⇩2,ls⇩2,sh⇩2)⟩"
| CallStatic⇩1:
"⟦ P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨addr a,s⇩1⟩;  P ⊢⇩1 ⟨ps,s⇩1⟩ [⇒] ⟨map Val vs,(h⇩2,ls⇩2,sh⇩2)⟩;
h⇩2 a = Some(C,fs); P ⊢ C sees M,Static:Ts→T = body in D ⟧
⟹ P ⊢⇩1 ⟨e∙M(ps),s⇩0⟩ ⇒ ⟨THROW IncompatibleClassChangeError,(h⇩2,ls⇩2,sh⇩2)⟩"

| SCallParamsThrow⇩1:
"⟦ P ⊢⇩1 ⟨es,s⇩0⟩ [⇒] ⟨es',s⇩2⟩; es' = map Val vs @ throw ex # es⇩2 ⟧
⟹ P ⊢⇩1 ⟨C∙⇩sM(es),s⇩0⟩ ⇒ ⟨throw ex,s⇩2⟩"
| SCallNone⇩1:
"⟦ P ⊢⇩1 ⟨ps,s⇩0⟩ [⇒] ⟨map Val vs,s⇩2⟩;
¬(∃b Ts T body D. P ⊢ C sees M,b:Ts→T = body in D) ⟧
⟹ P ⊢⇩1 ⟨C∙⇩sM(ps),s⇩0⟩ ⇒ ⟨THROW NoSuchMethodError,s⇩2⟩"
| SCallNonStatic⇩1:
"⟦ P ⊢⇩1 ⟨ps,s⇩0⟩ [⇒] ⟨map Val vs,s⇩2⟩;
P ⊢ C sees M,NonStatic:Ts→T = body in D ⟧
⟹ P ⊢⇩1 ⟨C∙⇩sM(ps),s⇩0⟩ ⇒ ⟨THROW IncompatibleClassChangeError,s⇩2⟩"
| SCallInitThrow⇩1:
"⟦ P ⊢⇩1 ⟨ps,s⇩0⟩ [⇒] ⟨map Val vs,(h⇩1,ls⇩1,sh⇩1)⟩;
P ⊢ C sees M,Static:Ts→T = body in D;
∄sfs. sh⇩1 D = Some(sfs,Done); M ≠ clinit;
P ⊢⇩1 ⟨INIT D ([D],False) ← unit,(h⇩1,ls⇩1,sh⇩1)⟩ ⇒ ⟨throw a,s'⟩ ⟧
⟹ P ⊢⇩1 ⟨C∙⇩sM(ps),s⇩0⟩ ⇒ ⟨throw a,s'⟩"
| SCallInit⇩1:
"⟦ P ⊢⇩1 ⟨ps,s⇩0⟩ [⇒] ⟨map Val vs,(h⇩1,ls⇩1,sh⇩1)⟩;
P ⊢ C sees M,Static:Ts→T = body in D;
∄sfs. sh⇩1 D = Some(sfs,Done); M ≠ clinit;
P ⊢⇩1 ⟨INIT D ([D],False) ← unit,(h⇩1,ls⇩1,sh⇩1)⟩ ⇒ ⟨Val v',(h⇩2,ls⇩2,sh⇩2)⟩;
size vs = size Ts; ls⇩2' = vs @ replicate (max_vars body) undefined;
P ⊢⇩1 ⟨body,(h⇩2,ls⇩2',sh⇩2)⟩ ⇒ ⟨e',(h⇩3,ls⇩3,sh⇩3)⟩ ⟧
⟹ P ⊢⇩1 ⟨C∙⇩sM(ps),s⇩0⟩ ⇒ ⟨e',(h⇩3,ls⇩2,sh⇩3)⟩"
| SCall⇩1:
"⟦ P ⊢⇩1 ⟨ps,s⇩0⟩ [⇒] ⟨map Val vs,(h⇩2,ls⇩2,sh⇩2)⟩;
P ⊢ C sees M,Static:Ts→T = body in D;
sh⇩2 D = Some(sfs,Done) ∨ (M = clinit ∧ sh⇩2 D = ⌊(sfs, Processing)⌋);
size vs = size Ts; ls⇩2' = vs @ replicate (max_vars body) undefined;
P ⊢⇩1 ⟨body,(h⇩2,ls⇩2',sh⇩2)⟩ ⇒ ⟨e',(h⇩3,ls⇩3,sh⇩3)⟩ ⟧
⟹ P ⊢⇩1 ⟨C∙⇩sM(ps),s⇩0⟩ ⇒ ⟨e',(h⇩3,ls⇩2,sh⇩3)⟩"

| Block⇩1:
"P ⊢⇩1 ⟨e,s⇩0⟩ ⇒ ⟨e',s⇩1⟩ ⟹ P ⊢⇩1 ⟨Block i T e,s⇩0⟩ ⇒ ⟨e',s⇩1⟩"

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

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

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

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

| Try⇩1:
"P ⊢⇩1 ⟨e⇩1,s⇩0⟩ ⇒ ⟨Val v⇩1,s⇩1⟩ ⟹
P ⊢⇩1 ⟨try e⇩1 catch(C i) e⇩2,s⇩0⟩ ⇒ ⟨Val v⇩1,s⇩1⟩"
| TryCatch⇩1:
"⟦ P ⊢⇩1 ⟨e⇩1,s⇩0⟩ ⇒ ⟨Throw a,(h⇩1,ls⇩1,sh⇩1)⟩;
h⇩1 a = Some(D,fs); P ⊢ D ≼⇧* C; i < length ls⇩1;
P ⊢⇩1 ⟨e⇩2,(h⇩1,ls⇩1[i:=Addr a],sh⇩1)⟩ ⇒ ⟨e⇩2',(h⇩2,ls⇩2,sh⇩2)⟩ ⟧
⟹ P ⊢⇩1 ⟨try e⇩1 catch(C i) e⇩2,s⇩0⟩ ⇒ ⟨e⇩2',(h⇩2,ls⇩2,sh⇩2)⟩"
| TryThrow⇩1:
"⟦ P ⊢⇩1 ⟨e⇩1,s⇩0⟩ ⇒ ⟨Throw a,(h⇩1,ls⇩1,sh⇩1)⟩; h⇩1 a = Some(D,fs); ¬ P ⊢ D ≼⇧* C ⟧
⟹ P ⊢⇩1 ⟨try e⇩1 catch(C i) e⇩2,s⇩0⟩ ⇒ ⟨Throw a,(h⇩1,ls⇩1,sh⇩1)⟩"

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

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

― ‹ init rules ›

| InitFinal⇩1:
"P ⊢⇩1 ⟨e,s⟩ ⇒ ⟨e',s'⟩ ⟹ P ⊢⇩1 ⟨INIT C (Nil,b) ← e,s⟩ ⇒ ⟨e',s'⟩"
| InitNone⇩1:
"⟦ 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'⟩"
| InitDone⇩1:
"⟦ 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'⟩"
| InitProcessing⇩1:
"⟦ 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'⟩"
| InitError⇩1:
"⟦ 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'⟩"
| InitObject⇩1:
"⟦ 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'⟩"
| InitNonObject⇩1:
"⟦ 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'⟩"
| InitRInit⇩1:
"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'⟩"

| RInit⇩1:
"⟦ 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'')⟩ ⇒ ⟨e⇩1,s⇩1⟩ ⟧
⟹ P ⊢⇩1 ⟨RI (C,e);Cs ← e',s⟩ ⇒ ⟨e⇩1,s⇩1⟩"
| RInitInitFail⇩1:
"⟦ 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'')⟩ ⇒ ⟨e⇩1,s⇩1⟩ ⟧
⟹ P ⊢⇩1 ⟨RI (C,e);D#Cs ← e',s⟩ ⇒ ⟨e⇩1,s⇩1⟩"
| RInitFailFinal⇩1:
"⟦ 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 eval⇩1_evals⇩1_induct = eval⇩1_evals⇩1.induct [split_format (complete)]
and eval⇩1_evals⇩1_inducts = eval⇩1_evals⇩1.inducts [split_format (complete)]
(*>*)

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

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

lemma eval⇩1_final: "P ⊢⇩1 ⟨e,s⟩ ⇒ ⟨e',s'⟩ ⟹ final e'"
and evals⇩1_final: "P ⊢⇩1 ⟨es,s⟩ [⇒] ⟨es',s'⟩ ⟹ finals es'"
(*<*)by(induct rule:eval⇩1_evals⇩1.inducts, simp_all)(*>*)

lemma eval⇩1_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 eval⇩1_cases(3) by blast
next
fix a assume "e = Throw a"
then show ?thesis using eval
by (metis eval⇩1_cases(3,17) exp.distinct(101) exp.inject(3) val.distinct(13))
qed
(*>*)

subsection "Property preservation"

lemma eval⇩1_preserves_len:
"P ⊢⇩1 ⟨e⇩0,(h⇩0,ls⇩0,sh⇩0)⟩ ⇒ ⟨e⇩1,(h⇩1,ls⇩1,sh⇩1)⟩ ⟹ length ls⇩0 = length ls⇩1"
and evals⇩1_preserves_len:
"P ⊢⇩1 ⟨es⇩0,(h⇩0,ls⇩0,sh⇩0)⟩ [⇒] ⟨es⇩1,(h⇩1,ls⇩1,sh⇩1)⟩ ⟹ length ls⇩0 = length ls⇩1"
(*<*)by (induct rule:eval⇩1_evals⇩1_inducts, simp_all)(*>*)

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

lemma clinit⇩1_loc_pres:
"P ⊢⇩1 ⟨C⇩0∙⇩sclinit([]),(h,l,sh)⟩ ⇒ ⟨e',(h',l',sh')⟩ ⟹ l = l'"
by(auto elim!: eval⇩1_cases(12) evals⇩1_cases(1))

lemma
shows init⇩1_ri⇩1_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: eval⇩1_evals⇩1_inducts)
case (RInitInitFail⇩1 e h l sh a')
then show ?case using eval⇩1_final[of _ _ _ "throw a'"]
by(fastforce dest: eval⇩1_final_same[of _ "Throw a"])
next
case RInitFailFinal⇩1 then show ?case by(auto dest: eval⇩1_final_same)
qed(auto dest: evals⇩1_cases eval⇩1_cases(17) eval⇩1_final_same)

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

theorem eval⇩1_hext: "P ⊢⇩1 ⟨e,(h,l,sh)⟩ ⇒ ⟨e',(h',l',sh')⟩ ⟹ h ⊴ h'"
and evals⇩1_hext:  "P ⊢⇩1 ⟨es,(h,l,sh)⟩ [⇒] ⟨es',(h',l',sh')⟩ ⟹ h ⊴ h'"
(*<*)
proof (induct rule: eval⇩1_evals⇩1_inducts)
case New⇩1 thus ?case
split:if_split_asm simp del:fun_upd_apply)
next
case NewInit⇩1 thus ?case
next
case FAss⇩1 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 rinit⇩1_throw:
"P⇩1 ⊢⇩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 eval⇩1_cases(20)) qed(auto elim: eval⇩1_cases)
next
case (Cons C Cs) show ?case using Cons.prems
proof(induct rule: eval⇩1_cases(20))
case RInit⇩1: 1
then show ?case using Cons.hyps by(auto elim: eval⇩1_cases)
next
case RInitInitFail⇩1: 2
then show ?case using Cons.hyps eval⇩1_final_same final_def by blast
next
case RInitFailFinal⇩1: 3 then show ?case by simp
qed
qed

lemma rinit⇩1_throwE:
"P ⊢⇩1 ⟨RI (C,throw e) ; Cs ← e⇩0,s⟩ ⇒ ⟨e',s'⟩
⟹ ∃a s⇩t. e' = throw a ∧ P ⊢⇩1 ⟨throw e,s⟩ ⇒ ⟨throw a,s⇩t⟩"
proof(induct Cs arbitrary: C e s)
case Nil
then show ?case
proof(rule eval⇩1_cases(20)) ― ‹ RI ›
fix v h' l' sh' assume "P ⊢⇩1 ⟨throw e,s⟩ ⇒ ⟨Val v,(h', l', sh')⟩"
then show ?case using eval⇩1_cases(17) by blast
qed(auto)
next
case (Cons C' Cs')
show ?case using Cons.prems(1)
proof(rule eval⇩1_cases(20)) ― ‹ RI ›
fix v h' l' sh' assume "P ⊢⇩1 ⟨throw e,s⟩ ⇒ ⟨Val v,(h', l', sh')⟩"
then show ?case using eval⇩1_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'' ← e⇩0,(h', l', sh'(C ↦ (sfs, Error)))⟩ ⇒ ⟨e',s'⟩"
and "C' # Cs' = D # Cs''"
then show ?thesis using Cons.hyps eval⇩1_final eval⇩1_final_same by blast
qed(simp)
qed

end