Theory J1WellForm

(*  Title:      JinjaDCI/Compiler/J1WellForm.thy

    Author:     Tobias Nipkow, Susannah Mansky
    Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC

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

section ‹ Well-Formedness of Intermediate Language ›

theory J1WellForm
imports "../J/JWellForm" J1
begin

subsection "Well-Typedness"

type_synonym 
  env⇩1  = "ty list"   ― ‹type environment indexed by variable number›

inductive
  WT⇩1 :: "[J⇩1_prog,env⇩1, expr⇩1     , ty     ] ⇒ bool"
         (‹(_,_ ⊢⇩1/ _ :: _)›   [51,51,51]50)
  and WTs⇩1 :: "[J⇩1_prog,env⇩1, expr⇩1 list, ty list] ⇒ bool"
         (‹(_,_ ⊢⇩1/ _ [::] _)› [51,51,51]50)
  for P :: J⇩1_prog
where
  
  WTNew⇩1:
  "is_class P C  ⟹
  P,E ⊢⇩1 new C :: Class C"

| WTCast⇩1:
  "⟦ P,E ⊢⇩1 e :: Class D;  is_class P C;  P ⊢ C ≼⇧* D ∨ P ⊢ D ≼⇧* C ⟧
  ⟹ P,E ⊢⇩1 Cast C e :: Class C"

| WTVal⇩1:
  "typeof v = Some T ⟹
  P,E ⊢⇩1 Val v :: T"

| WTVar⇩1:
  "⟦ E!i = T; i < size E ⟧
  ⟹ P,E ⊢⇩1 Var i :: T"

| WTBinOp⇩1:
  "⟦ P,E ⊢⇩1 e⇩1 :: T⇩1;  P,E ⊢⇩1 e⇩2 :: T⇩2;
     case bop of Eq ⇒ (P ⊢ T⇩1 ≤ T⇩2 ∨ P ⊢ T⇩2 ≤ T⇩1) ∧ T = Boolean
               | Add ⇒ T⇩1 = Integer ∧ T⇩2 = Integer ∧ T = Integer ⟧
  ⟹ P,E ⊢⇩1 e⇩1 «bop» e⇩2 :: T"

| WTLAss⇩1:
  "⟦ E!i = T;  i < size E; P,E ⊢⇩1 e :: T';  P ⊢ T' ≤ T ⟧
  ⟹ P,E ⊢⇩1 i:=e :: Void"

| WTFAcc⇩1:
  "⟦ P,E ⊢⇩1 e :: Class C;  P ⊢ C sees F,NonStatic:T in D ⟧
  ⟹ P,E ⊢⇩1 e∙F{D} :: T"

| WTSFAcc⇩1:
  "⟦ P ⊢ C sees F,Static:T in D ⟧
  ⟹ P,E ⊢⇩1 C∙⇩sF{D} :: T"

| WTFAss⇩1:
  "⟦ P,E ⊢⇩1 e⇩1 :: Class C;  P ⊢ C sees F,NonStatic:T in D;  P,E ⊢⇩1 e⇩2 :: T';  P ⊢ T' ≤ T ⟧
  ⟹ P,E ⊢⇩1 e⇩1∙F{D} := e⇩2 :: Void"

| WTSFAss⇩1:
  "⟦  P ⊢ C sees F,Static:T in D;  P,E ⊢⇩1 e⇩2 :: T';  P ⊢ T' ≤ T ⟧
  ⟹ P,E ⊢⇩1 C∙⇩sF{D}:=e⇩2 :: Void"

| WTCall⇩1:
  "⟦ P,E ⊢⇩1 e :: Class C; P ⊢ C sees M,NonStatic:Ts' → T = m in D;
    P,E ⊢⇩1 es [::] Ts;  P ⊢ Ts [≤] Ts' ⟧
  ⟹ P,E ⊢⇩1 e∙M(es) :: T"

| WTSCall⇩1:
  "⟦ P ⊢ C sees M,Static:Ts → T = m in D;
     P,E ⊢⇩1 es [::] Ts';  P ⊢ Ts' [≤] Ts; M ≠ clinit ⟧
  ⟹ P,E ⊢⇩1 C∙⇩sM(es) :: T"

| WTBlock⇩1:
  "⟦ is_type P T; P,E@[T] ⊢⇩1 e::T' ⟧
  ⟹  P,E ⊢⇩1 {i:T; e} :: T'"

| WTSeq⇩1:
  "⟦ P,E ⊢⇩1 e⇩1::T⇩1;  P,E ⊢⇩1 e⇩2::T⇩2 ⟧
  ⟹  P,E ⊢⇩1 e⇩1;;e⇩2 :: T⇩2"

| WTCond⇩1:
  "⟦ P,E ⊢⇩1 e :: Boolean;  P,E ⊢⇩1 e⇩1::T⇩1;  P,E ⊢⇩1 e⇩2::T⇩2;
    P ⊢ T⇩1 ≤ T⇩2 ∨ P ⊢ T⇩2 ≤ T⇩1;  P ⊢ T⇩1 ≤ T⇩2 ⟶ T = T⇩2; P ⊢ T⇩2 ≤ T⇩1 ⟶ T = T⇩1 ⟧
  ⟹ P,E ⊢⇩1 if (e) e⇩1 else e⇩2 :: T"

| WTWhile⇩1:
  "⟦ P,E ⊢⇩1 e :: Boolean;  P,E ⊢⇩1 c::T ⟧
  ⟹ P,E ⊢⇩1 while (e) c :: Void"

| WTThrow⇩1:
  "P,E ⊢⇩1 e :: Class C  ⟹
  P,E ⊢⇩1 throw e :: Void"

| WTTry⇩1:
  "⟦ P,E ⊢⇩1 e⇩1 :: T;  P,E@[Class C] ⊢⇩1 e⇩2 :: T; is_class P C ⟧
  ⟹ P,E ⊢⇩1 try e⇩1 catch(C i) e⇩2 :: T"

| WTNil⇩1:
  "P,E ⊢⇩1 [] [::] []"

| WTCons⇩1:
  "⟦ P,E ⊢⇩1 e :: T; P,E ⊢⇩1 es [::] Ts ⟧
  ⟹  P,E ⊢⇩1 e#es [::] T#Ts"

(*<*)
declare  WT⇩1_WTs⇩1.intros[intro!]
declare WTNil⇩1[iff]

lemmas WT⇩1_WTs⇩1_induct = WT⇩1_WTs⇩1.induct [split_format (complete)]
  and WT⇩1_WTs⇩1_inducts = WT⇩1_WTs⇩1.inducts [split_format (complete)]

inductive_cases eee[elim!]:
  "P,E ⊢⇩1 Val v :: T"
  "P,E ⊢⇩1 Var i :: T"
  "P,E ⊢⇩1 Cast D e :: T"
  "P,E ⊢⇩1 i:=e :: T"
  "P,E ⊢⇩1 {i:U; e} :: T"
  "P,E ⊢⇩1 e⇩1;;e⇩2 :: T"
  "P,E ⊢⇩1 if (e) e⇩1 else e⇩2 :: T"
  "P,E ⊢⇩1 while (e) c :: T"
  "P,E ⊢⇩1 throw e :: T"
  "P,E ⊢⇩1 try e⇩1 catch(C i) e⇩2 :: T"
  "P,E ⊢⇩1 e∙F{D} :: T"
  "P,E ⊢⇩1 C∙⇩sF{D} :: T"
  "P,E ⊢⇩1 e⇩1∙F{D}:=e⇩2 :: T"
  "P,E ⊢⇩1 C∙⇩sF{D}:=e⇩2 :: T"
  "P,E ⊢⇩1 e⇩1 «bop» e⇩2 :: T"
  "P,E ⊢⇩1 new C :: T"
  "P,E ⊢⇩1 e∙M(es) :: T"
  "P,E ⊢⇩1 C∙⇩sM(es) :: T"
  "P,E ⊢⇩1 [] [::] Ts"
  "P,E ⊢⇩1 e#es [::] Ts"
(*>*)

lemma init_nWT⇩1 [simp]:"¬P,E ⊢⇩1 INIT C (Cs,b) ← e :: T"
 by(auto elim:WT⇩1.cases)
lemma rinit_nWT⇩1 [simp]:"¬P,E ⊢⇩1 RI(C,e);Cs ← e' :: T"
 by(auto elim:WT⇩1.cases)

lemma WTs⇩1_same_size: "⋀Ts. P,E ⊢⇩1 es [::] Ts ⟹ size es = size Ts"
(*<*)by (induct es type:list) auto(*>*)


lemma WT⇩1_unique:
  "P,E ⊢⇩1 e :: T⇩1 ⟹ (⋀T⇩2. P,E ⊢⇩1 e :: T⇩2 ⟹ T⇩1 = T⇩2)" and
  WTs⇩1_unique: "P,E ⊢⇩1 es [::] Ts⇩1 ⟹ (⋀Ts⇩2. P,E ⊢⇩1 es [::] Ts⇩2 ⟹ Ts⇩1 = Ts⇩2)"
(*<*)
proof(induct rule:WT⇩1_WTs⇩1.inducts)
  case WTVal⇩1 then show ?case by clarsimp
next
  case (WTBinOp⇩1 E e⇩1 T⇩1 e⇩2 T⇩2 bop T)
  then show ?case by(case_tac bop) force+
next
  case WTFAcc⇩1 then show ?case
    by (blast dest:sees_field_idemp sees_field_fun)
next
  case WTSFAcc⇩1 then show ?case by (blast dest:sees_field_fun)
next
  case WTSFAss⇩1 then show ?case by (blast dest:sees_field_fun)
next
  case WTCall⇩1 then show ?case
    by (blast dest:sees_method_idemp sees_method_fun)
next
  case WTSCall⇩1 then show ?case by (blast dest:sees_method_fun)
qed blast+
(*>*)


lemma assumes wf: "wf_prog p P"
shows WT⇩1_is_type: "P,E ⊢⇩1 e :: T ⟹ set E ⊆ types P ⟹ is_type P T"
and "P,E ⊢⇩1 es [::] Ts ⟹ True"
(*<*)
proof(induct rule:WT⇩1_WTs⇩1.inducts)
  case WTVal⇩1 then show ?case by (simp add:typeof_lit_is_type)
next
  case WTVar⇩1 then show ?case by (blast intro:nth_mem)
next
  case WTBinOp⇩1 then show ?case by (simp split:bop.splits)
next
  case WTFAcc⇩1 then show ?case
    by (simp add:sees_field_is_type[OF _ wf])
next
  case WTSFAcc⇩1 then show ?case
    by (simp add:sees_field_is_type[OF _ wf])
next
  case WTCall⇩1 then show ?case
    by (fastforce dest!: sees_wf_mdecl[OF wf] simp:wf_mdecl_def)
next
  case WTSCall⇩1 then show ?case
    by (fastforce dest!: sees_wf_mdecl[OF wf] simp:wf_mdecl_def)
next
  case WTCond⇩1 then show ?case by blast
qed simp+
(*>*)

lemma WT⇩1_nsub_RI: "P,E ⊢⇩1 e :: T ⟹ ¬sub_RI e"
 and WTs⇩1_nsub_RIs: "P,E ⊢⇩1 es [::] Ts ⟹ ¬sub_RIs es"
proof(induct rule: WT⇩1_WTs⇩1.inducts) qed(simp_all)

subsection‹ Runtime Well-Typedness ›

inductive
  WTrt⇩1 :: "J⇩1_prog ⇒ heap ⇒ sheap ⇒ env⇩1 ⇒ expr⇩1 ⇒ ty ⇒ bool"
  and WTrts⇩1 :: "J⇩1_prog ⇒ heap ⇒ sheap ⇒ env⇩1 ⇒ expr⇩1 list ⇒ ty list ⇒ bool"
  and WTrt2⇩1 :: "[J⇩1_prog,env⇩1,heap,sheap,expr⇩1,ty] ⇒ bool"
        (‹_,_,_,_ ⊢⇩1 _ : _›   [51,51,51,51]50)
  and WTrts2⇩1 :: "[J⇩1_prog,env⇩1,heap,sheap,expr⇩1 list, ty list] ⇒ bool"
        (‹_,_,_,_ ⊢⇩1 _ [:] _› [51,51,51,51]50)
  for P :: J⇩1_prog and h :: heap and sh :: sheap
where
  
  "P,E,h,sh ⊢⇩1 e : T ≡ WTrt⇩1 P h sh E e T"
| "P,E,h,sh ⊢⇩1 es[:]Ts ≡ WTrts⇩1 P h sh E es Ts"

| WTrtNew⇩1:
  "is_class P C  ⟹
  P,E,h,sh ⊢⇩1 new C : Class C"

| WTrtCast⇩1:
  "⟦ P,E,h,sh ⊢⇩1 e : T; is_refT T; is_class P C ⟧
  ⟹ P,E,h,sh ⊢⇩1 Cast C e : Class C"

| WTrtVal⇩1:
  "typeof⇘h⇙ v = Some T ⟹
  P,E,h,sh ⊢⇩1 Val v : T"

| WTrtVar⇩1:
  "⟦ E!i = T; i < size E ⟧  ⟹
  P,E,h,sh ⊢⇩1 Var i : T"

| WTrtBinOpEq⇩1:
  "⟦ P,E,h,sh ⊢⇩1 e⇩1 : T⇩1;  P,E,h,sh ⊢⇩1 e⇩2 : T⇩2 ⟧
  ⟹ P,E,h,sh ⊢⇩1 e⇩1 «Eq» e⇩2 : Boolean"

| WTrtBinOpAdd⇩1:
  "⟦ P,E,h,sh ⊢⇩1 e⇩1 : Integer;  P,E,h,sh ⊢⇩1 e⇩2 : Integer ⟧
  ⟹ P,E,h,sh ⊢⇩1 e⇩1 «Add» e⇩2 : Integer"

| WTrtLAss⇩1:
  "⟦ E!i = T; i < size E; P,E,h,sh ⊢⇩1 e : T';  P ⊢ T' ≤ T ⟧
   ⟹ P,E,h,sh ⊢⇩1 i:=e : Void"

| WTrtFAcc⇩1:
  "⟦ P,E,h,sh ⊢⇩1 e : Class C; P ⊢ C has F,NonStatic:T in D ⟧ ⟹
  P,E,h,sh ⊢⇩1 e∙F{D} : T"

| WTrtFAccNT⇩1:
  "P,E,h,sh ⊢⇩1 e : NT ⟹
  P,E,h,sh ⊢⇩1 e∙F{D} : T"

| WTrtSFAcc⇩1:
  "⟦ P ⊢ C has F,Static:T in D ⟧ ⟹
  P,E,h,sh ⊢⇩1 C∙⇩sF{D} : T"

| WTrtFAss⇩1:
  "⟦ P,E,h,sh ⊢⇩1 e⇩1 : Class C;  P ⊢ C has F,NonStatic:T in D; P,E,h,sh ⊢⇩1 e⇩2 : T⇩2;  P ⊢ T⇩2 ≤ T ⟧
  ⟹ P,E,h,sh ⊢⇩1 e⇩1∙F{D}:=e⇩2 : Void"

| WTrtFAssNT⇩1:
  "⟦ P,E,h,sh ⊢⇩1 e⇩1:NT; P,E,h,sh ⊢⇩1 e⇩2 : T⇩2 ⟧
  ⟹ P,E,h,sh ⊢⇩1 e⇩1∙F{D}:=e⇩2 : Void"

| WTrtSFAss⇩1:
  "⟦ P,E,h,sh ⊢⇩1 e⇩2 : T⇩2; P ⊢ C has F,Static:T in D; P ⊢ T⇩2 ≤ T ⟧
  ⟹ P,E,h,sh ⊢⇩1 C∙⇩sF{D}:=e⇩2 : Void"

| WTrtCall⇩1:
  "⟦ P,E,h,sh ⊢⇩1 e : Class C; P ⊢ C sees M,NonStatic:Ts → T = m in D;
     P,E,h,sh ⊢⇩1 es [:] Ts'; P ⊢ Ts' [≤] Ts ⟧
  ⟹ P,E,h,sh ⊢⇩1 e∙M(es) : T"

| WTrtCallNT⇩1:
  "⟦ P,E,h,sh ⊢⇩1 e : NT; P,E,h,sh ⊢⇩1 es [:] Ts ⟧
  ⟹ P,E,h,sh ⊢⇩1 e∙M(es) : T"

| WTrtSCall⇩1:
  "⟦ P ⊢ C sees M,Static:Ts → T = m in D;
     P,E,h,sh ⊢⇩1 es [:] Ts'; P ⊢ Ts' [≤] Ts;
     M = clinit ⟶ sh D = ⌊(sfs,Processing)⌋ ∧ es = map Val vs ⟧
  ⟹ P,E,h,sh ⊢⇩1 C∙⇩sM(es) : T"

| WTrtBlock⇩1:
  "P,E@[T],h,sh ⊢⇩1 e : T'  ⟹
  P,E,h,sh ⊢⇩1 {i:T; e} : T'"

| WTrtSeq⇩1:
  "⟦ P,E,h,sh ⊢⇩1 e⇩1:T⇩1;  P,E,h,sh ⊢⇩1 e⇩2:T⇩2 ⟧
  ⟹ P,E,h,sh ⊢⇩1 e⇩1;;e⇩2 : T⇩2"

| WTrtCond⇩1:
  "⟦ P,E,h,sh ⊢⇩1 e : Boolean;  P,E,h,sh ⊢⇩1 e⇩1:T⇩1;  P,E,h,sh ⊢⇩1 e⇩2:T⇩2;
     P ⊢ T⇩1 ≤ T⇩2 ∨ P ⊢ T⇩2 ≤ T⇩1; P ⊢ T⇩1 ≤ T⇩2 ⟶ T = T⇩2; P ⊢ T⇩2 ≤ T⇩1 ⟶ T = T⇩1 ⟧
  ⟹ P,E,h,sh ⊢⇩1 if (e) e⇩1 else e⇩2 : T"

| WTrtWhile⇩1:
  "⟦ P,E,h,sh ⊢⇩1 e : Boolean;  P,E,h,sh ⊢⇩1 c:T ⟧
  ⟹  P,E,h,sh ⊢⇩1 while(e) c : Void"

| WTrtThrow⇩1:
  "⟦ P,E,h,sh ⊢⇩1 e : T⇩r; is_refT T⇩r ⟧ ⟹
  P,E,h,sh ⊢⇩1 throw e : T"

| WTrtTry⇩1:
  "⟦ P,E,h,sh ⊢⇩1 e⇩1 : T⇩1;  P,E@[Class C],h,sh ⊢⇩1 e⇩2 : T⇩2; P ⊢ T⇩1 ≤ T⇩2 ⟧
  ⟹ P,E,h,sh ⊢⇩1 try e⇩1 catch(C i) e⇩2 : T⇩2"

| WTrtInit⇩1:
  "⟦ P,E,h,sh ⊢⇩1 e : T; ∀C' ∈ set (C#Cs). is_class P C'; ¬sub_RI e;
     ∀C' ∈ set (tl Cs). ∃sfs. sh C' = ⌊(sfs,Processing)⌋;
     b ⟶ (∀C' ∈ set Cs. ∃sfs. sh C' = ⌊(sfs,Processing)⌋);
     distinct Cs; supercls_lst P Cs ⟧
  ⟹ P,E,h,sh ⊢⇩1 INIT C (Cs, b) ← e : T"

| WTrtRI⇩1:
  "⟦ P,E,h,sh ⊢⇩1 e : T; P,E,h,sh ⊢⇩1 e' : T'; ∀C' ∈ set (C#Cs). is_class P C'; ¬sub_RI e';
     ∀C' ∈ set (C#Cs). not_init C' e;
     ∀C' ∈ set Cs. ∃sfs. sh C' = ⌊(sfs,Processing)⌋;
     ∃sfs. sh C = ⌊(sfs, Processing)⌋ ∨ (sh C = ⌊(sfs, Error)⌋ ∧ e = THROW NoClassDefFoundError);
     distinct (C#Cs); supercls_lst P (C#Cs) ⟧
  ⟹ P,E,h,sh ⊢⇩1 RI(C, e);Cs ← e' : T'"

― ‹well-typed expression lists›

| WTrtNil⇩1:
  "P,E,h,sh ⊢⇩1 [] [:] []"

| WTrtCons⇩1:
  "⟦ P,E,h,sh ⊢⇩1 e : T;  P,E,h,sh ⊢⇩1 es [:] Ts ⟧
  ⟹  P,E,h,sh ⊢⇩1 e#es [:] T#Ts"

(*<*)
declare WTrt⇩1_WTrts⇩1.intros[intro!] WTrtNil⇩1[iff]
declare
  WTrtFAcc⇩1[rule del] WTrtFAccNT⇩1[rule del] WTrtSFAcc⇩1[rule del]
  WTrtFAss⇩1[rule del] WTrtFAssNT⇩1[rule del] WTrtSFAss⇩1[rule del]
  WTrtCall⇩1[rule del] WTrtCallNT⇩1[rule del] WTrtSCall⇩1[rule del]

lemmas WTrt⇩1_induct = WTrt⇩1_WTrts⇩1.induct [split_format (complete)]
  and WTrt⇩1_inducts = WTrt⇩1_WTrts⇩1.inducts [split_format (complete)]
(*>*)

(*<*)
inductive_cases WTrt⇩1_elim_cases[elim!]:
  "P,E,h,sh ⊢⇩1 Val v : T"
  "P,E,h,sh ⊢⇩1 Var i : T"
  "P,E,h,sh ⊢⇩1 v :=e : T"
  "P,E,h,sh ⊢⇩1 {i:U; e} : T"
  "P,E,h,sh ⊢⇩1 e⇩1;;e⇩2 : T⇩2"
  "P,E,h,sh ⊢⇩1 if (e) e⇩1 else e⇩2 : T"
  "P,E,h,sh ⊢⇩1 while(e) c : T"
  "P,E,h,sh ⊢⇩1 throw e : T"
  "P,E,h,sh ⊢⇩1 try e⇩1 catch(C V) e⇩2 : T"
  "P,E,h,sh ⊢⇩1 Cast D e : T"
  "P,E,h,sh ⊢⇩1 e∙F{D} : T"
  "P,E,h,sh ⊢⇩1 C∙⇩sF{D} : T"
  "P,E,h,sh ⊢⇩1 e∙F{D} := v : T"
  "P,E,h,sh ⊢⇩1 C∙⇩sF{D} := v : T"
  "P,E,h,sh ⊢⇩1 e⇩1 «bop» e⇩2 : T"
  "P,E,h,sh ⊢⇩1 new C : T"
  "P,E,h,sh ⊢⇩1 e∙M{D}(es) : T"
  "P,E,h,sh ⊢⇩1 C∙⇩sM{D}(es) : T"
  "P,E,h,sh ⊢⇩1 INIT C (Cs,b) ← e : T"
  "P,E,h,sh ⊢⇩1 RI(C,e);Cs ← e' : T"
  "P,E,h,sh ⊢⇩1 [] [:] Ts"
  "P,E,h,sh ⊢⇩1 e#es [:] Ts"
(*>*)

lemma WT⇩1_implies_WTrt⇩1: "P,E ⊢⇩1 e :: T ⟹ P,E,h,sh ⊢⇩1 e : T"
and WTs⇩1_implies_WTrts⇩1: "P,E ⊢⇩1 es [::] Ts ⟹ P,E,h,sh ⊢⇩1 es [:] Ts"
(*<*)
proof(induct rule: WT⇩1_WTs⇩1_inducts)
  case WTVal⇩1 then show ?case by (fastforce dest:typeof_lit_typeof)
next
  case (WTBinOp⇩1 E e⇩1 T⇩1 e⇩2 T⇩2 bop T)
  then show ?case by (case_tac bop) fastforce+
next
  case WTFAcc⇩1 then show ?case
    by (fastforce simp: WTrtFAcc⇩1 has_visible_field)
next
  case WTSFAcc⇩1 then show ?case
    by (fastforce simp: WTrtSFAcc⇩1 has_visible_field)
next
  case WTFAss⇩1 then show ?case by (meson WTrtFAss⇩1 has_visible_field)
next
  case WTSFAss⇩1 then show ?case by (meson WTrtSFAss⇩1 has_visible_field)
next
  case WTCall⇩1 then show ?case by (fastforce simp: WTrtCall⇩1)
next
  case WTSCall⇩1 then show ?case by (fastforce simp: WTrtSCall⇩1)
qed fastforce+
(*>*)

subsection‹ Well-formedness›

― ‹Indices in blocks increase by 1›

primrec ℬ :: "expr⇩1 ⇒ nat ⇒ bool"
  and ℬs :: "expr⇩1 list ⇒ nat ⇒ bool" where
"ℬ (new C) i = True" |
"ℬ (Cast C e) i = ℬ e i" |
"ℬ (Val v) i = True" |
"ℬ (e⇩1 «bop» e⇩2) i = (ℬ e⇩1 i ∧ ℬ e⇩2 i)" |
"ℬ (Var j) i = True" |
"ℬ (e∙F{D}) i = ℬ e i" |
"ℬ (C∙⇩sF{D}) i = True" |
"ℬ (j:=e) i = ℬ e i" |
"ℬ (e⇩1∙F{D} := e⇩2) i = (ℬ e⇩1 i ∧ ℬ e⇩2 i)" |
"ℬ (C∙⇩sF{D} := e⇩2) i = ℬ e⇩2 i" |
"ℬ (e∙M(es)) i = (ℬ e i ∧ ℬs es i)" |
"ℬ (C∙⇩sM(es)) i = ℬs es i" |
"ℬ ({j:T ; e}) i = (i = j ∧ ℬ e (i+1))" |
"ℬ (e⇩1;;e⇩2) i = (ℬ e⇩1 i ∧ ℬ e⇩2 i)" |
"ℬ (if (e) e⇩1 else e⇩2) i = (ℬ e i ∧ ℬ e⇩1 i ∧ ℬ e⇩2 i)" |
"ℬ (throw e) i = ℬ e i" |
"ℬ (while (e) c) i = (ℬ e i ∧ ℬ c i)" |
"ℬ (try e⇩1 catch(C j) e⇩2) i = (ℬ e⇩1 i ∧ i=j ∧ ℬ e⇩2 (i+1))" |
"ℬ (INIT C (Cs,b) ← e) i = ℬ e i" |
"ℬ (RI(C,e);Cs ← e') i = (ℬ e i ∧ ℬ e' i)" |

"ℬs [] i = True" |
"ℬs (e#es) i = (ℬ e i ∧ ℬs es i)"


definition wf_J⇩1_mdecl :: "J⇩1_prog ⇒ cname ⇒ expr⇩1 mdecl ⇒ bool"
where
  "wf_J⇩1_mdecl P C  ≡  λ(M,b,Ts,T,body).
    ¬sub_RI body ∧
 (case b of
    NonStatic ⇒
        (∃T'. P,Class C#Ts ⊢⇩1 body :: T' ∧ P ⊢ T' ≤ T) ∧
        𝒟 body ⌊{..size Ts}⌋ ∧ ℬ body (size Ts + 1)
  | Static ⇒ (∃T'. P,Ts ⊢⇩1 body :: T' ∧ P ⊢ T' ≤ T) ∧
        𝒟 body ⌊{..<size Ts}⌋ ∧ ℬ body (size Ts))"

lemma wf_J⇩1_mdecl_NonStatic[simp]:
  "wf_J⇩1_mdecl P C (M,NonStatic,Ts,T,body) ≡
    (¬sub_RI body ∧
    (∃T'. P,Class C#Ts ⊢⇩1 body :: T' ∧ P ⊢ T' ≤ T) ∧
     𝒟 body ⌊{..size Ts}⌋ ∧ ℬ body (size Ts + 1))"
(*<*)by (simp add:wf_J⇩1_mdecl_def)(*>*)

lemma wf_J⇩1_mdecl_Static[simp]:
  "wf_J⇩1_mdecl P C (M,Static,Ts,T,body) ≡
    (¬sub_RI body ∧
    (∃T'. P,Ts ⊢⇩1 body :: T' ∧ P ⊢ T' ≤ T) ∧
     𝒟 body ⌊{..<size Ts}⌋ ∧ ℬ body (size Ts))"
(*<*)by (simp add:wf_J⇩1_mdecl_def)(*>*)

abbreviation "wf_J⇩1_prog == wf_prog wf_J⇩1_mdecl"

lemma sees_wf⇩1_nsub_RI:
assumes wf: "wf_J⇩1_prog P" and cM: "P ⊢ C sees M,b : Ts→T = body in D"
shows "¬sub_RI body"
using sees_wf_mdecl[OF wf cM] by(simp add: wf_J⇩1_mdecl_def wf_mdecl_def)

lemma wf⇩1_types_clinit:
assumes wf:"wf_prog wf_md P" and ex: "class P C = Some a" and proc: "sh C = ⌊(sfs, Processing)⌋"
shows "P,E,h,sh ⊢⇩1 C∙⇩sclinit([]) : Void"
proof -
  from ex obtain D fs ms where "a = (D,fs,ms)" by(cases a)
  then have sP: "(C, D, fs, ms) ∈ set P" using ex map_of_SomeD[of P C a] by(simp add: class_def)
  then have "wf_clinit ms" using assms by(unfold wf_prog_def wf_cdecl_def, auto)
  then obtain m where sm: "(clinit, Static, [], Void, m) ∈ set ms"
    by(unfold wf_clinit_def) auto
  then have "P ⊢ C sees clinit,Static:[] → Void = m in C"
    using mdecl_visible[OF wf sP sm] by simp
  then show ?thesis using WTrtSCall⇩1 proc by blast
qed


lemma assumes wf: "wf_J⇩1_prog P"
shows eval⇩1_proc_pres: "P ⊢⇩1 ⟨e,(h,l,sh)⟩ ⇒ ⟨e',(h',l',sh')⟩
  ⟹ not_init C e ⟹ ∃sfs. sh C = ⌊(sfs, Processing)⌋ ⟹ ∃sfs'. sh' C = ⌊(sfs', Processing)⌋"
  and evals⇩1_proc_pres: "P ⊢⇩1 ⟨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⇩1_evals⇩1_inducts)
  case Call⇩1 then show ?case using sees_wf⇩1_nsub_RI[OF wf Call⇩1.hyps(6)] nsub_RI_not_init by auto
next
  case (SCallInit⇩1 ps h l sh vs h⇩1 l⇩1 sh⇩1 C' M Ts T body D v' h⇩2 l⇩2 sh⇩2 l⇩2' e' h⇩3 l⇩3 sh⇩3)
  then show ?case
    using SCallInit⇩1 sees_wf⇩1_nsub_RI[OF wf SCallInit⇩1.hyps(3)] nsub_RI_not_init[of body] by auto
next
  case SCall⇩1 then show ?case using sees_wf⇩1_nsub_RI[OF wf SCall⇩1.hyps(3)] nsub_RI_not_init by auto
next
  case (InitNone⇩1 sh C1 C' Cs h l e' a a b) then show ?case by(cases "C = C1") auto
next
  case (InitDone⇩1 sh C sfs C' Cs h l e' a a b) then show ?case by(cases Cs, auto)
next
  case (InitProcessing⇩1 sh C sfs C' Cs h l e' a a b) then show ?case by(cases Cs, auto)
next
  case (InitError⇩1 sh C1 sfs Cs h l e' a a b C') then show ?case by(cases "C = C1") auto
next
  case (InitObject⇩1 sh C1 sfs sh' C' Cs h l e' a a b) then show ?case by(cases "C = C1") auto
next
  case (InitNonObject⇩1 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⇩1 e a a b v h' l' sh' C sfs i sh'' C' Cs e⇩1 a a b) then show ?case by(cases Cs, auto)
next
  case (RInitInitFail⇩1 e h l sh a h' l' sh' C1 sfs i sh'' D Cs e⇩1 h1 l1 sh1)
  then show ?case using eval⇩1_final by fastforce
qed(auto)
(*>*)

lemma clinit⇩1_proc_pres:
  "⟦ wf_J⇩1_prog P; P ⊢⇩1 ⟨C⇩0∙⇩sclinit([]),(h,l,sh)⟩ ⇒ ⟨e',(h',l',sh')⟩;
     sh C' = ⌊(sfs,Processing)⌋ ⟧
  ⟹ ∃sfs. sh' C' = ⌊(sfs,Processing)⌋"
 by(auto dest: eval⇩1_proc_pres)

end