Theory WellTypeRT

(*  Title:      JinjaDCI/J/WellTypeRT.thy

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

    Based on the Jinja theory J/WellTypeRT.thy by Tobias Nipkow
*)

section ‹ Runtime Well-typedness ›

theory WellTypeRT
imports WellType
begin

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

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

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

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

| WTrtVar:
  "E V = Some T  ⟹
  P,E,h,sh ⊢ Var V : T"

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

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

| WTrtLAss:
  "⟦ E V = Some T;  P,E,h,sh ⊢ e : T';  P ⊢ T' ≤ T ⟧
   ⟹ P,E,h,sh ⊢ V:=e : Void"

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

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

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

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

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

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

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

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

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

| WTrtBlock:
  "P,E(V↦T),h,sh ⊢ e : T'  ⟹
  P,E,h,sh ⊢ {V:T; e} : T'"

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

| WTrtCond:
  "⟦ P,E,h,sh ⊢ e : Boolean;  P,E,h,sh ⊢ e⇩1:T⇩1;  P,E,h,sh ⊢ 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 ⊢ if (e) e⇩1 else e⇩2 : T"

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

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

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

| WTrtInit:
  "⟦ P,E,h,sh ⊢ 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 ⊢ INIT C (Cs, b) ← e : T"

| WTrtRI:
  "⟦ P,E,h,sh ⊢ e : T; P,E,h,sh ⊢ 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 ⊢ RI(C, e);Cs ← e' : T'"

― ‹well-typed expression lists›

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

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

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

lemmas WTrt_induct = WTrt_WTrts.induct [split_format (complete)]
  and WTrt_inducts = WTrt_WTrts.inducts [split_format (complete)]
(*>*)


subsection‹Easy consequences›

lemma [iff]: "(P,E,h,sh ⊢ [] [:] Ts) = (Ts = [])"
(*<*)by(rule iffI) (auto elim: WTrts.cases)(*>*)

lemma [iff]: "(P,E,h,sh ⊢ e#es [:] T#Ts) = (P,E,h,sh ⊢ e : T ∧ P,E,h,sh ⊢ es [:] Ts)"
(*<*)by(rule iffI) (auto elim: WTrts.cases)(*>*)

lemma [iff]: "(P,E,h,sh ⊢ (e#es) [:] Ts) =
  (∃U Us. Ts = U#Us ∧ P,E,h,sh ⊢ e : U ∧ P,E,h,sh ⊢ es [:] Us)"
(*<*)by(rule iffI) (auto elim: WTrts.cases)(*>*)

lemma [simp]: "∀Ts. (P,E,h,sh ⊢ es⇩1 @ es⇩2 [:] Ts) =
  (∃Ts⇩1 Ts⇩2. Ts = Ts⇩1 @ Ts⇩2 ∧ P,E,h,sh ⊢ es⇩1 [:] Ts⇩1 & P,E,h,sh ⊢ es⇩2[:]Ts⇩2)"
(*<*)
proof(induct es⇩1)
  case (Cons a list)
  let ?lhs = "λTs. (∃U Us. Ts = U # Us ∧ P,E,h,sh ⊢ a : U ∧
        (∃Ts⇩1 Ts⇩2. Us = Ts⇩1 @ Ts⇩2 ∧ P,E,h,sh ⊢ list [:] Ts⇩1 ∧ P,E,h,sh ⊢ es⇩2 [:] Ts⇩2))"
  let ?rhs = "λTs. (∃Ts⇩1 Ts⇩2. Ts = Ts⇩1 @ Ts⇩2 ∧
        (∃U Us. Ts⇩1 = U # Us ∧ P,E,h,sh ⊢ a : U ∧ P,E,h,sh ⊢ list [:] Us) ∧ P,E,h,sh ⊢ es⇩2 [:] Ts⇩2)"
  { fix Ts assume "?lhs Ts"
    then have "?rhs Ts" by (auto intro: Cons_eq_appendI)
  }
  moreover {
    fix Ts assume "?rhs Ts"
    then have "?lhs Ts" by fastforce
  }
  ultimately have "⋀Ts. ?lhs Ts = ?rhs Ts" by(rule iffI)
  then show ?case by (clarsimp simp: Cons)
qed simp
(*>*)

lemma [iff]: "P,E,h,sh ⊢ Val v : T = (typeof⇘h⇙ v = Some T)"
(*<*)proof(rule iffI) qed (auto elim: WTrt.cases)(*>*)

lemma [iff]: "P,E,h,sh ⊢ Var v : T = (E v = Some T)"
(*<*)proof(rule iffI) qed (auto elim: WTrt.cases)(*>*)

lemma [iff]: "P,E,h,sh ⊢ e⇩1;;e⇩2 : T⇩2 = (∃T⇩1. P,E,h,sh ⊢ e⇩1:T⇩1 ∧ P,E,h,sh ⊢ e⇩2:T⇩2)"
(*<*)proof(rule iffI) qed (auto elim: WTrt.cases)(*>*)

lemma [iff]: "P,E,h,sh ⊢ {V:T; e} : T'  =  (P,E(V↦T),h,sh ⊢ e : T')"
(*<*)proof(rule iffI) qed (auto elim: WTrt.cases)(*>*)

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

subsection‹Some interesting lemmas›

lemma WTrts_Val[simp]:
 "⋀Ts. (P,E,h,sh ⊢ map Val vs [:] Ts) = (map (typeof⇘h⇙) vs = map Some Ts)"
(*<*)
proof(induct vs)
  case (Cons a vs)
  then show ?case by(case_tac Ts; simp)
qed simp
(*>*)


lemma WTrts_same_length: "⋀Ts. P,E,h,sh ⊢ es [:] Ts ⟹ length es = length Ts"
(*<*)by(induct es type:list)auto(*>*)


lemma WTrt_env_mono:
  "P,E,h,sh ⊢ e : T ⟹ (⋀E'. E ⊆⇩m E' ⟹ P,E',h,sh ⊢ e : T)" and
  "P,E,h,sh ⊢ es [:] Ts ⟹ (⋀E'. E ⊆⇩m E' ⟹ P,E',h,sh ⊢ es [:] Ts)"
(*<*)
proof(induct rule: WTrt_inducts)
  case WTrtVar then show ?case by(simp add: map_le_def dom_def)
next
  case WTrtLAss then show ?case by(force simp:map_le_def)
qed(fastforce intro: WTrt_WTrts.intros)+
(*>*)


lemma WTrt_hext_mono: "P,E,h,sh ⊢ e : T ⟹ h ⊴ h' ⟹ P,E,h',sh ⊢ e : T"
and WTrts_hext_mono: "P,E,h,sh ⊢ es [:] Ts ⟹ h ⊴ h' ⟹ P,E,h',sh ⊢ es [:] Ts"
(*<*)
proof(induct rule: WTrt_inducts)
  case WTrtVal then show ?case by(simp add: hext_typeof_mono)
qed(fastforce intro: WTrt_WTrts.intros)+
(*>*)

lemma WTrt_shext_mono: "P,E,h,sh ⊢ e : T ⟹ sh ⊴⇩s sh' ⟹ ¬sub_RI e ⟹ P,E,h,sh' ⊢ e : T"
and WTrts_shext_mono: "P,E,h,sh ⊢ es [:] Ts ⟹ sh ⊴⇩s sh' ⟹ ¬sub_RIs es ⟹ P,E,h,sh' ⊢ es [:] Ts"
(*<*)
by(induct rule: WTrt_inducts)
  (auto simp add: WTrt_WTrts.intros)
(*>*)

lemma WTrt_hext_shext_mono: "P,E,h,sh ⊢ e : T
   ⟹ h ⊴ h' ⟹ sh ⊴⇩s sh' ⟹ ¬sub_RI e ⟹ P,E,h',sh' ⊢ e : T"
 by(auto intro: WTrt_hext_mono WTrt_shext_mono)

lemma WTrts_hext_shext_mono: "P,E,h,sh ⊢ es [:] Ts
   ⟹ h ⊴ h' ⟹ sh ⊴⇩s sh' ⟹ ¬sub_RIs es ⟹ P,E,h',sh' ⊢ es [:] Ts"
 by(auto intro: WTrts_hext_mono WTrts_shext_mono)


lemma WT_implies_WTrt: "P,E ⊢ e :: T ⟹ P,E,h,sh ⊢ e : T"
and WTs_implies_WTrts: "P,E ⊢ es [::] Ts ⟹ P,E,h,sh ⊢ es [:] Ts"
(*<*)
proof(induct rule: WT_WTs_inducts)
  case WTVal then show ?case by(fastforce dest: typeof_lit_typeof)
next
  case WTFAcc
  then show ?case by(fastforce simp: WTrtFAcc has_visible_field)
next
  case WTSFAcc
  then show ?case by(fastforce simp: WTrtSFAcc has_visible_field)
next
  case WTFAss
  then show ?case by(fastforce simp: WTrtFAss dest: has_visible_field)
next
  case WTSFAss
  then show ?case by(fastforce simp: WTrtSFAss dest: has_visible_field)
qed(fastforce intro: WTrt_WTrts.intros)+
(*>*)

end