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

  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
  "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⇘hv = 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  e1 : T1;  P,E,h,sh  e2 : T2 
   P,E,h,sh  e1 «Eq» e2 : Boolean"

| WTrtBinOpAdd:
  " P,E,h,sh  e1 : Integer;  P,E,h,sh  e2 : Integer 
   P,E,h,sh  e1 «Add» e2 : 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  eF{D} : T"

| WTrtFAccNT:
  "P,E,h,sh  e : NT 
  P,E,h,sh  eF{D} : T"

| WTrtSFAcc:
  " P  C has F,Static:T in D  
  P,E,h,sh  CsF{D} : T"

| WTrtFAss:
  " P,E,h,sh  e1 : Class C;  P  C has F,NonStatic:T in D; P,E,h,sh  e2 : T2;  P  T2  T 
   P,E,h,sh  e1F{D}:=e2 : Void"

| WTrtFAssNT:
  " P,E,h,sh  e1:NT; P,E,h,sh  e2 : T2 
   P,E,h,sh  e1F{D}:=e2 : Void"

| WTrtSFAss:
  " P,E,h,sh  e2 : T2; P  C has F,Static:T in D; P  T2  T 
   P,E,h,sh  CsF{D}:=e2 : 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  eM(es) : T"

| WTrtCallNT:
  " P,E,h,sh  e : NT; P,E,h,sh  es [:] Ts 
   P,E,h,sh  eM(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  CsM(es) : T"

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

| WTrtSeq:
  " P,E,h,sh  e1:T1;  P,E,h,sh  e2:T2 
   P,E,h,sh  e1;;e2 : T2"

| WTrtCond:
  " P,E,h,sh  e : Boolean;  P,E,h,sh  e1:T1;  P,E,h,sh  e2:T2;
     P  T1  T2  P  T2  T1; P  T1  T2  T = T2; P  T2  T1  T = T1 
   P,E,h,sh  if (e) e1 else e2 : 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 : Tr; is_refT Tr  
  P,E,h,sh  throw e : T"

| WTrtTry:
  " P,E,h,sh  e1 : T1;  P,E(V  Class C),h,sh  e2 : T2; P  T1  T2 
   P,E,h,sh  try e1 catch(C V) e2 : T2"

| 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]
  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  es1 @ es2 [:] Ts) =
  (Ts1 Ts2. Ts = Ts1 @ Ts2  P,E,h,sh  es1 [:] Ts1 & P,E,h,sh  es2[:]Ts2)"
proof(induct es1)
  case (Cons a list)
  let ?lhs = "λTs. (U Us. Ts = U # Us  P,E,h,sh  a : U 
        (Ts1 Ts2. Us = Ts1 @ Ts2  P,E,h,sh  list [:] Ts1  P,E,h,sh  es2 [:] Ts2))"
  let ?rhs = "λTs. (Ts1 Ts2. Ts = Ts1 @ Ts2 
        (U Us. Ts1 = U # Us  P,E,h,sh  a : U  P,E,h,sh  list [:] Us)  P,E,h,sh  es2 [:] Ts2)"
  { 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⇘hv = 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  e1;;e2 : T2 = (T1. P,E,h,sh  e1:T1  P,E,h,sh  e2:T2)"
(*<*)proof(rule iffI) qed (auto elim: WTrt.cases)(*>*)

lemma [iff]: "P,E,h,sh  {V:T; e} : T'  =  (P,E(VT),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) e1 else e2 : T"
  "P,E,h,sh  while(e) c : T"
  "P,E,h,sh  throw e : T"
  "P,E,h,sh  try e1 catch(C V) e2 : T"
  "P,E,h,sh  Cast D e : T"
  "P,E,h,sh  eF{D} : T"
  "P,E,h,sh  CsF{D} : T"
  "P,E,h,sh  eF{D} := v : T"
  "P,E,h,sh  CsF{D} := v : T"
  "P,E,h,sh  e1 «bop» e2 : T"
  "P,E,h,sh  new C : T"
  "P,E,h,sh  eM{D}(es) : T"
  "P,E,h,sh  CsM{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)
  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)
  case WTFAcc
  then show ?case by(fastforce simp: WTrtFAcc has_visible_field)
  case WTSFAcc
  then show ?case by(fastforce simp: WTrtSFAcc has_visible_field)
  case WTFAss
  then show ?case by(fastforce simp: WTrtFAss dest: has_visible_field)
  case WTSFAss
  then show ?case by(fastforce simp: WTrtSFAss dest: has_visible_field)
qed(fastforce intro: WTrt_WTrts.intros)+