Quelle  J1.thy

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

definition hp₁ :: "state₁ ==> heap"
where
  "hp₁ ≡ fst"
definition lcl₁ :: "state₁ ==> val list"
where
  "lcl₁ ≡ fst ∘ snd"
definition shp₁ :: "state₁ ==> sheap"
where
  "shp₁ ≡ snd ∘ snd"

(*<*)
declare hp₁_def[simp] lcl₁_def[simp] shp₁_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₁ «bop¬ e₂) = max (max_vars e₁) (max_vars e₂)"
| "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₁ F D e₂) = max (max_vars e₁) (max_vars e₂)"
| "max_vars(SFAss C F D e₂) = max_vars e₂"
| "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(e₁;;e₂) = max (max_vars e₁) (max_vars e₂)"
| "max_vars(if (e) e₁ else e₂) =
   max (max_vars e) (max (max_vars e₁) (max_vars e₂))"
| "max_vars(while (b) e) = max (max_vars b) (max_vars e)"
| "max_vars(throw e) = max_vars e"
| "max_vars(try e₁ catch(C V) e₂) = max (max_vars e₁) (max_vars e₂ + 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
  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 ] ==>
  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₂⟩"
| BinOpThrow₁₁:
  "P ⊨₁ ⟨e₁,s₀⟩ ==> ⟨throw e,s₁⟩ ==>
  P ⊨₁ ⟨e₁ «bop¬ e₂, s₀⟩ ==> ⟨throw e,s₁⟩"
| BinOpThrow₂₁:
  "[ P ⊨₁ ⟨e₁,s₀⟩ ==> ⟨Val v₁,s₁⟩; P ⊨₁ ⟨e₂,s₁⟩ ==> ⟨throw e,s₂⟩ ]
  ==> P ⊨₁ ⟨e₁ «bop¬ e₂,s₀⟩ ==> ⟨throw e,s₂⟩"

| Var₁:
  "[ ls!i = v; i < size ls ] ==>
  P ⊨₁ ⟨Var i,(h,ls,sh)⟩ ==> ⟨Val v,(h,ls,sh)⟩"

| LAss₁:
  "[ P ⊨₁ ⟨e,s₀⟩ ==> ⟨Val v,(h,ls,sh)⟩; i < size ls; ls' = ls[i := v] ]
  ==> P ⊨₁ ⟨i:= e,s₀⟩ ==> ⟨unit,(h,ls',sh)⟩"
| LAssThrow₁:
  "P ⊨₁ ⟨e,s₀⟩ ==> ⟨throw e',s₁⟩ ==>
  P ⊨₁ ⟨i:= e,s₀⟩ ==> ⟨throw e',s₁⟩"

| FAcc₁:
  "[ P ⊨₁ ⟨e,s₀⟩ ==> ⟨addr a,(h,ls,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,ls,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,ls,sh)⟩; h a = Some(C,fs);
    ¬(∃b t. P ⊨ C has F,b:t in D) ]
  ==> P ⊨₁ ⟨e∙F{D},s₀⟩ ==> ⟨THROW NoSuchFieldError,(h,ls,sh)⟩"
| FAccStatic₁:
  "[ P ⊨₁ ⟨e,s₀⟩ ==> ⟨addr a,(h,ls,sh)⟩; h a = Some(C,fs);
    P ⊨ C has F,Static:t in D ]
  ==> P ⊨₁ ⟨e∙F{D},s₀⟩ ==> ⟨THROW IncompatibleClassChangeError,(h,ls,sh)⟩"

| SFAcc₁:
  "[ P ⊨ C has F,Static:t in D;
     sh D = Some (sfs,Done);
     sfs F = Some v ]
  ==> P ⊨₁ ⟨C∙_sF{D},(h,ls,sh)⟩ ==> ⟨Val v,(h,ls,sh)⟩"
| SFAccInit₁:
  "[ P ⊨ C has F,Static:t in D;
     ∄sfs. sh D = Some (sfs,Done); P ⊨₁ ⟨INIT D ([D],False) ← unit,(h,ls,sh)⟩ ==> ⟨Val v',(h',ls',sh')⟩;
     sh' D = Some (sfs,i);
     sfs F = Some v ]
  ==> P ⊨₁ ⟨C∙_sF{D},(h,ls,sh)⟩ ==> ⟨Val v,(h',ls',sh')⟩"
| SFAccInitThrow₁:
  "[ P ⊨ C has F,Static:t in D;
     ∄sfs. sh D = Some (sfs,Done); P ⊨₁ ⟨INIT D ([D],False) ← unit,(h,ls,sh)⟩ ==> ⟨throw a,s'⟩ ]
  ==> P ⊨₁ ⟨C∙_sF{D},(h,ls,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₂⟩"
| FAssThrow₁₁:
  "P ⊨₁ ⟨e₁,s₀⟩ ==> ⟨throw e',s₁⟩ ==>
  P ⊨₁ ⟨e₁∙F{D}:=e₂,s₀⟩ ==> ⟨throw e',s₁⟩"
| FAssThrow₂₁:
  "[ 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(es),s₀⟩ ==> ⟨throw e',s₁⟩"
| CallNull₁:
  "[ P ⊨₁ ⟨e,s₀⟩ ==> ⟨null,s₁⟩; P ⊨₁ ⟨es,s₁⟩ [==>] ⟨map Val vs,s₂⟩ ]
  ==> P ⊨₁ ⟨e∙M(es),s₀⟩ ==> ⟨THROW NullPointer,s₂⟩"
| Call₁:
  "[ P ⊨₁ ⟨e,s₀⟩ ==> ⟨addr a,s₁⟩; P ⊨₁ ⟨es,s₁⟩ [==>] ⟨map Val vs,(h₂,ls₂,sh₂)⟩;
    h₂ a = Some(C,fs); P ⊨ C sees M,NonStatic:Ts→T = body in D;
    size vs = size Ts; ls₂' = (Addr a) # vs @ replicate (max_vars body) undefined;
    P ⊨₁ ⟨body,(h₂,ls₂',sh₂)⟩ ==> ⟨e',(h₃,ls₃,sh₃)⟩ ]
  ==> P ⊨₁ ⟨e∙M(es),s₀⟩ ==> ⟨e',(h₃,ls₂,sh₃)⟩"
| CallParamsThrow₁:
  "[ P ⊨₁ ⟨e,s₀⟩ ==> ⟨Val v,s₁⟩; P ⊨₁ ⟨es,s₁⟩ [==>] ⟨es',s₂⟩;
     es' = map Val vs @ throw ex # es₂ ]
   ==> P ⊨₁ ⟨e∙M(es),s₀⟩ ==> ⟨throw ex,s₂⟩"
| CallNone₁:
  "[ P ⊨₁ ⟨e,s₀⟩ ==> ⟨addr a,s₁⟩; P ⊨₁ ⟨ps,s₁⟩ [==>] ⟨map Val vs,(h₂,ls₂,sh₂)⟩;
     h₂ a = Some(C,fs); ¬(∃b Ts T body D. P ⊨ C sees M,b:Ts→T = body in D) ]
  ==> P ⊨₁ ⟨e∙M(ps),s₀⟩ ==> ⟨THROW NoSuchMethodError,(h₂,ls₂,sh₂)⟩"
| CallStatic₁:
  "[ P ⊨₁ ⟨e,s₀⟩ ==> ⟨addr a,s₁⟩; P ⊨₁ ⟨ps,s₁⟩ [==>] ⟨map Val vs,(h₂,ls₂,sh₂)⟩;
     h₂ a = Some(C,fs); P ⊨ C sees M,Static:Ts→T = body in D ]
  ==> P ⊨₁ ⟨e∙M(ps),s₀⟩ ==> ⟨THROW IncompatibleClassChangeError,(h₂,ls₂,sh₂)⟩"

| SCallParamsThrow₁:
  "[ P ⊨₁ ⟨es,s₀⟩ [==>] ⟨es',s₂⟩; es' = map Val vs @ throw ex # es₂ ]
   ==> P ⊨₁ ⟨C∙_sM(es),s₀⟩ ==> ⟨throw ex,s₂⟩"
| SCallNone₁:
  "[ P ⊨₁ ⟨ps,s₀⟩ [==>] ⟨map Val vs,s₂⟩;
     ¬(∃b Ts T body D. P ⊨ C sees M,b:Ts→T = body 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 = body in D ]
  ==> P ⊨₁ ⟨C∙_sM(ps),s₀⟩ ==> ⟨THROW IncompatibleClassChangeError,s₂⟩"
| SCallInitThrow₁:
  "[ P ⊨₁ ⟨ps,s₀⟩ [==>] ⟨map Val vs,(h₁,ls₁,sh₁)⟩;
     P ⊨ C sees M,Static:Ts→T = body in D;
     ∄sfs. sh₁ D = Some(sfs,Done); M ≠ clinit;
     P ⊨₁ ⟨INIT D ([D],False) ← unit,(h₁,ls₁,sh₁)⟩ ==> ⟨throw a,s'⟩ ]
  ==> P ⊨₁ ⟨C∙_sM(ps),s₀⟩ ==> ⟨throw a,s'⟩"
| SCallInit₁:
  "[ P ⊨₁ ⟨ps,s₀⟩ [==>] ⟨map Val vs,(h₁,ls₁,sh₁)⟩;
     P ⊨ C sees M,Static:Ts→T = body in D;
     ∄sfs. sh₁ D = Some(sfs,Done); M ≠ clinit;
     P ⊨₁ ⟨INIT D ([D],False) ← unit,(h₁,ls₁,sh₁)⟩ ==> ⟨Val v',(h₂,ls₂,sh₂)⟩;
     size vs = size Ts; ls₂' = vs @ replicate (max_vars body) undefined;
     P ⊨₁ ⟨body,(h₂,ls₂',sh₂)⟩ ==> ⟨e',(h₃,ls₃,sh₃)⟩ ]
  ==> P ⊨₁ ⟨C∙_sM(ps),s₀⟩ ==> ⟨e',(h₃,ls₂,sh₃)⟩"
| SCall₁:
  "[ P ⊨₁ ⟨ps,s₀⟩ [==>] ⟨map Val vs,(h₂,ls₂,sh₂)⟩;
     P ⊨ C sees M,Static:Ts→T = body in D;
     sh₂ D = Some(sfs,Done) ∨ (M = clinit ∧ sh₂ D = ⌊(sfs, Processing)⌋);
     size vs = size Ts; ls₂' = vs @ replicate (max_vars body) undefined;
     P ⊨₁ ⟨body,(h₂,ls₂',sh₂)⟩ ==> ⟨e',(h₃,ls₃,sh₃)⟩ ]
  ==> P ⊨₁ ⟨C∙_sM(ps),s₀⟩ ==> ⟨e',(h₃,ls₂,sh₃)⟩"

| Block₁:
  "P ⊨₁ ⟨e,s₀⟩ ==> ⟨e',s₁⟩ ==> P ⊨₁ ⟨Block i T e,s₀⟩ ==> ⟨e',s₁⟩"

| 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 i) e₂,s₀⟩ ==> ⟨Val v₁,s₁⟩"
| TryCatch₁:
  "[ P ⊨₁ ⟨e₁,s₀⟩ ==> ⟨Throw a,(h₁,ls₁,sh₁)⟩;
    h₁ a = Some(D,fs); P ⊨ D ⪯^* C; i < length ls₁;
    P ⊨₁ ⟨e₂,(h₁,ls₁[i:=Addr a],sh₁)⟩ ==> ⟨e₂',(h₂,ls₂,sh₂)⟩ ]
  ==> P ⊨₁ ⟨try e₁ catch(C i) e₂,s₀⟩ ==> ⟨e₂',(h₂,ls₂,sh₂)⟩"
| TryThrow₁:
  "[ P ⊨₁ ⟨e₁,s₀⟩ ==> ⟨Throw a,(h₁,ls₁,sh₁)⟩; h₁ a = Some(D,fs); ¬ P ⊨ D ⪯^* C ]
  ==> P ⊨₁ ⟨try e₁ catch(C i) e₂,s₀⟩ ==> ⟨Throw a,(h₁,ls₁,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'⟩"
| 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'⟩"
(*>*) 


lemma eval₁_final: "P ⊨₁ ⟨e,s⟩ ==> ⟨e',s'⟩ ==> final e'"
 and evals₁_final: "P ⊨₁ ⟨es,s⟩ [==>] ⟨es',s'⟩ ==> finals es'"
(*<*)by(induct rule:eval\<^sub>1_evals\<^sub>1.inducts, simp_all)(*>*)


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

subsection "Property preservation"

lemma eval₁_preserves_len:
  "P ⊨₁ ⟨e₀,(h₀,ls₀,sh₀)⟩ ==> ⟨e₁,(h₁,ls₁,sh₁)⟩ ==> length ls₀ = length ls₁"
and evals₁_preserves_len:
  "P ⊨₁ ⟨es₀,(h₀,ls₀,sh₀)⟩ [==>] ⟨es₁,(h₁,ls₁,sh₁)⟩ ==> length ls₀ = length ls₁"
(*<*)by (induct rule:eval\<^sub>1_evals\<^sub>1_inducts, simp_all)(*>*)


lemma evals₁_preserves_elen:
  "∧es' s s'. P ⊨₁ ⟨es,s⟩ [==>] ⟨es',s'⟩ ==> length es = length es'"
(*<*)by(induct es type:list) (auto elim:evals\<^sub>1.cases)(*>*)


lemma clinit₁_loc_pres:
 "P ⊨₁ ⟨C₀∙_sclinit([]),(h,l,sh)⟩ ==> ⟨e',(h',l',sh')⟩ ==> l = l'"
 by(auto elim!: eval₁_cases(12) evals₁_cases(1))

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)


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)
(*>*)

subsection "Initialization"

lemma rinit₁_throw:
 "P₁ ⊨₁ ⟨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₁_cases(20)) qed(auto elim: eval₁_cases)
next
  case (Cons C Cs) show ?case using Cons.prems
  proof(induct rule: eval₁_cases(20))
    case RInit₁: 1
    then show ?case using Cons.hyps by(auto elim: eval₁_cases)
  next
    case RInitInitFail₁: 2
    then show ?case using Cons.hyps eval₁_final_same final_def by blast
  next
    case RInitFailFinal₁: 3 then show ?case by simp
  qed
qed

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

end