Theory WellTypeRT

(*  Title:      JinjaThreads/J/WellTypeRT.thy
    Author:     Tobias Nipkow, Andreas Lochbihler
*)

section ‹Runtime Well-typedness›

theory WellTypeRT
imports 
  WellType
  JHeap
begin

context J_heap_base begin

inductive WTrt :: "'addr J_prog  'heap  env  'addr expr  ty  bool"
  and WTrts :: "'addr J_prog  'heap  env  'addr expr list  ty list  bool"
  for P :: "'addr J_prog" and h :: "'heap"
  where

  WTrtNew:
    "is_class P C   WTrt P h E (new C) (Class C)"

| WTrtNewArray:
    " WTrt P h E e Integer; is_type P (T⌊⌉) 
     WTrt P h E (newA Te) (T⌊⌉)"

| WTrtCast:
    " WTrt P h E e T; is_type P U   WTrt P h E (Cast U e) U"

| WTrtInstanceOf:
    " WTrt P h E e T; is_type P U   WTrt P h E (e instanceof U) Boolean"

| WTrtVal:
    "typeof⇘hv = Some T  WTrt P h E (Val v) T"

| WTrtVar:
    "E V = Some T   WTrt P h E (Var V) T"

| WTrtBinOp:
    " WTrt P h E e1 T1; WTrt P h E e2 T2; P  T1«bop»T2 : T 
   WTrt P h E (e1 «bop» e2) T"

| WTrtLAss:
    " E V = Some T; WTrt P h E e T'; P  T'  T 
      WTrt P h E (V:=e) Void"

| WTrtAAcc:
    " WTrt P h E a (T⌊⌉); WTrt P h E i Integer 
     WTrt P h E (ai) T"

| WTrtAAccNT:
    " WTrt P h E a NT; WTrt P h E i Integer 
     WTrt P h E (ai) T"

| WTrtAAss:
    "  WTrt P h E a (T⌊⌉); WTrt P h E i Integer; WTrt P h E e T' 
     WTrt P h E (ai := e) Void"

| WTrtAAssNT:
    "  WTrt P h E a NT; WTrt P h E i Integer; WTrt P h E e T' 
     WTrt P h E (ai := e) Void"

| WTrtALength:
  "WTrt P h E a (T⌊⌉)  WTrt P h E (a∙length) Integer"

| WTrtALengthNT:
  "WTrt P h E a NT  WTrt P h E (a∙length) T"

| WTrtFAcc:
    " WTrt P h E e U; class_type_of' U = C; P  C has F:T (fm) in D  
    WTrt P h E (eF{D}) T"

| WTrtFAccNT:
    "WTrt P h E e NT  WTrt P h E (eF{D}) T"

| WTrtFAss:
    " WTrt P h E e1 U; class_type_of' U = C;  P  C has F:T (fm) in D; WTrt P h E e2 T2;  P  T2  T 
     WTrt P h E (e1F{D}:=e2) Void"

| WTrtFAssNT:
    " WTrt P h E e1 NT; WTrt P h E e2 T2 
     WTrt P h E (e1F{D}:=e2) Void"

| WTrtCAS:
  " WTrt P h E e1 U; class_type_of' U = C; P  C has F:T (fm) in D; volatile fm;
     WTrt P h E e2 T2; P  T2  T; WTrt P h E e3 T3; P  T3  T 
   WTrt P h E (e1∙compareAndSwap(DF, e2, e3)) Boolean"

| WTrtCASNT:
  " WTrt P h E e1 NT; WTrt P h E e2 T2; WTrt P h E e3 T3 
   WTrt P h E (e1∙compareAndSwap(DF, e2, e3)) Boolean"

| WTrtCall:
    " WTrt P h E e U; class_type_of' U = C; P  C sees M:Ts  T = meth in D;
       WTrts P h E es Ts'; P  Ts' [≤] Ts 
     WTrt P h E (eM(es)) T"

| WTrtCallNT:
    " WTrt P h E e NT; WTrts P h E es Ts 
     WTrt P h E (eM(es)) T"

| WTrtBlock:
    " WTrt P h (E(VT)) e T'; case vo of None  True | v  T'. typeof⇘hv = T'  P  T'  T 
   WTrt P h E {V:T=vo; e} T'"

| WTrtSynchronized:
    " WTrt P h E o' T; is_refT T; WTrt P h E e T' 
     WTrt P h E (sync(o') e) T'"

| WTrtInSynchronized:
    " WTrt P h E (addr a) T; WTrt P h E e T' 
     WTrt P h E (insync(a) e) T'"

| WTrtSeq:
    " WTrt P h E e1 T1; WTrt P h E e2 T2 
     WTrt P h E (e1;;e2) T2"

| WTrtCond:
    " WTrt P h E e Boolean; WTrt P h E e1 T1; WTrt P h E e2 T2; P  lub(T1, T2) = T 
     WTrt P h E (if (e) e1 else e2) T"

| WTrtWhile:
    " WTrt P h E e Boolean; WTrt P h E c T 
     WTrt P h E (while(e) c) Void"

| WTrtThrow:
    " WTrt P h E e T; P  T  Class Throwable 
     WTrt P h E (throw e) T'"

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

| WTrtNil: "WTrts P h E [] []"

| WTrtCons: " WTrt P h E e T; WTrts P h E es Ts   WTrts P h E (e # es) (T # Ts)"

abbreviation
  WTrt_syntax :: "'addr J_prog  env  'heap  'addr expr  ty  bool" ("_,_,_  _ : _"   [51,51,51]50)
where
  "P,E,h  e : T  WTrt P h E e T"

abbreviation
  WTrts_syntax :: "'addr J_prog  env  'heap  'addr expr list  ty list  bool" ("_,_,_  _ [:] _"   [51,51,51]50)
where
  "P,E,h  es [:] Ts  WTrts P h E es Ts"

lemmas [intro!] =
  WTrtNew WTrtNewArray WTrtCast WTrtInstanceOf WTrtVal WTrtVar WTrtBinOp WTrtLAss
  WTrtBlock WTrtSynchronized WTrtInSynchronized WTrtSeq WTrtCond WTrtWhile
  WTrtThrow WTrtTry WTrtNil WTrtCons

lemmas [intro] =
  WTrtFAcc WTrtFAccNT WTrtFAss WTrtFAssNT WTrtCall WTrtCallNT
  WTrtAAcc WTrtAAccNT WTrtAAss WTrtAAssNT WTrtALength WTrtALengthNT 

subsection‹Easy consequences›

inductive_simps WTrts_iffs [iff]:
  "P,E,h  [] [:] Ts"
  "P,E,h  e#es [:] T#Ts"
  "P,E,h  (e#es) [:] Ts"

lemma WTrts_conv_list_all2: "P,E,h  es [:] Ts = list_all2 (WTrt P h E) es Ts"
by(induct es arbitrary: Ts)(auto simp add: list_all2_Cons1 elim: WTrts.cases)

lemma [simp]: "(P,E,h  es1 @ es2 [:] Ts) =
  (Ts1 Ts2. Ts = Ts1 @ Ts2  P,E,h  es1 [:] Ts1 & P,E,h  es2[:]Ts2)"
by(auto simp add: WTrts_conv_list_all2 list_all2_append1 dest: list_all2_lengthD[symmetric])

inductive_simps WTrt_iffs [iff]:
  "P,E,h  Val v : T"
  "P,E,h  Var v : T"
  "P,E,h  e1;;e2 : T2"
  "P,E,h  {V:T=vo; e} : T'"

inductive_cases WTrt_elim_cases[elim!]:
  "P,E,h  newA Ti : U"
  "P,E,h  v :=e : T"
  "P,E,h  if (e) e1 else e2 : T"
  "P,E,h  while(e) c : T"
  "P,E,h  throw e : T"
  "P,E,h  try e1 catch(C V) e2 : T"
  "P,E,h  Cast D e : T"
  "P,E,h  e instanceof U : T"
  "P,E,h  ai : T"
  "P,E,h  ai := e : T"
  "P,E,h  a∙length : T"
  "P,E,h  eF{D} : T"
  "P,E,h  eF{D} := v : T"
  "P,E,h  e∙compareAndSwap(DF, e2, e3) : T"
  "P,E,h  e1 «bop» e2 : T"
  "P,E,h  new C : T"
  "P,E,h  eM(es) : T"
  "P,E,h  sync(o') e : T"
  "P,E,h  insync(a) e : T"

subsection‹Some interesting lemmas›

lemma WTrts_Val[simp]:
 "P,E,h  map Val vs [:] Ts  map (typeof⇘h) vs = map Some Ts"
by(induct vs arbitrary: Ts) auto

lemma WTrt_env_mono: "P,E,h  e : T  (E'. E m E'  P,E',h  e : T)"
  and WTrts_env_mono: "P,E,h  es [:] Ts  (E'. E m E'  P,E',h  es [:] Ts)"
apply(induct rule: WTrt_WTrts.inducts)
apply(simp add: WTrtNew)
apply(fastforce simp: WTrtNewArray)
apply(fastforce simp: WTrtCast)
apply(fastforce simp: WTrtInstanceOf)
apply(fastforce simp: WTrtVal)
apply(simp add: WTrtVar map_le_def dom_def)
apply(fastforce simp add: WTrtBinOp)
apply(force simp: map_le_def)
apply(force simp: WTrtAAcc)
apply(force simp: WTrtAAccNT)
apply(rule WTrtAAss, fastforce, blast, blast)
apply(fastforce)
apply(rule WTrtALength, blast)
apply(blast)
apply(fastforce simp: WTrtFAcc)
apply(simp add: WTrtFAccNT)
apply(fastforce simp: WTrtFAss)
apply(fastforce simp: WTrtFAssNT)
apply(fastforce simp: WTrtCAS)
apply(fastforce simp: WTrtCASNT)
apply(fastforce simp: WTrtCall)
apply(fastforce simp: WTrtCallNT)
apply(fastforce simp: map_le_def)
apply(fastforce)
apply(fastforce)
apply(fastforce)
apply(fastforce)
apply(fastforce simp: WTrtSeq)
apply(fastforce simp: WTrtCond)
apply(fastforce simp: WTrtWhile)
apply(fastforce simp: WTrtThrow)
apply(auto simp: WTrtTry map_le_def dom_def)
done

lemma WT_implies_WTrt: "P,E  e :: T  P,E,h  e : T"
  and WTs_implies_WTrts: "P,E  es [::] Ts  P,E,h  es [:] Ts"
apply(induct rule: WT_WTs.inducts)
apply fast
apply fast
apply fast
apply fast
apply(fastforce dest:typeof_lit_typeof)
apply(simp)
apply(fastforce intro: WT_binop_WTrt_binop)
apply(fastforce)
apply(erule WTrtAAcc)
apply(assumption)
apply(erule WTrtAAss)
apply(assumption)+
apply(erule WTrtALength)
apply(fastforce intro: has_visible_field)
apply(fastforce simp: WTrtFAss dest: has_visible_field)
apply(fastforce simp: WTrtCAS dest: has_visible_field)
apply(fastforce simp: WTrtCall)
apply(clarsimp simp del: fun_upd_apply, blast intro: typeof_lit_typeof)
apply(fastforce)+
done

lemma wt_blocks:
 "E.  length Vs = length Ts; length vs = length Ts  
       (P,E,h  blocks Vs Ts vs e : T) =
       (P,E(Vs[↦]Ts),h  e:T  (Ts'. map (typeof⇘h) vs = map Some Ts'  P  Ts' [≤] Ts))"
apply(induct Vs Ts vs e rule:blocks.induct)
apply (force)
apply simp_all
done

end

context J_heap begin

lemma WTrt_hext_mono: "P,E,h  e : T  h  h'  P,E,h'  e : T"
  and WTrts_hext_mono: "P,E,h  es [:] Ts  h  h'  P,E,h'  es [:] Ts"
apply(induct rule: WTrt_WTrts.inducts)
apply(simp add: WTrtNew)
apply(fastforce simp: WTrtNewArray)
apply(fastforce simp: WTrtCast)
apply(fastforce simp: WTrtInstanceOf)
apply(fastforce simp: WTrtVal dest:hext_typeof_mono)
apply(simp add: WTrtVar)
apply(fastforce simp add: WTrtBinOp)
apply(fastforce simp add: WTrtLAss)
apply fastforce
apply fastforce
apply fastforce
apply fastforce
apply fastforce
apply fastforce
apply(fast)
apply(simp add: WTrtFAccNT)
apply(fastforce simp: WTrtFAss del:WTrt_WTrts.intros WTrt_elim_cases)
apply(fastforce simp: WTrtFAssNT)
apply(fastforce simp: WTrtCAS)
apply(fastforce simp: WTrtCASNT)
apply(fastforce simp: WTrtCall)
apply(fastforce simp: WTrtCallNT)
apply(fastforce intro: hext_typeof_mono)
apply fastforce+
done

end

end