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 T⌊e⌉) (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⇘h⇙ v = 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 (a⌊i⌉) T"

| WTrtAAccNT:
    "⟦ WTrt P h E a NT; WTrt P h E i Integer ⟧
    ⟹ WTrt P h E (a⌊i⌉) T"

| WTrtAAss:
    "⟦  WTrt P h E a (T⌊⌉); WTrt P h E i Integer; WTrt P h E e T' ⟧
    ⟹ WTrt P h E (a⌊i⌉ := 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 (a⌊i⌉ := 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 (e∙F{D}) T"

| WTrtFAccNT:
    "WTrt P h E e NT ⟹ WTrt P h E (e∙F{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 (e1∙F{D}:=e2) Void"

| WTrtFAssNT:
    "⟦ WTrt P h E e1 NT; WTrt P h E e2 T2 ⟧
    ⟹ WTrt P h E (e1∙F{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(D∙F, 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(D∙F, 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 (e∙M(es)) T"

| WTrtCallNT:
    "⟦ WTrt P h E e NT; WTrts P h E es Ts ⟧
    ⟹ WTrt P h E (e∙M(es)) T"

| WTrtBlock:
    "⟦ WTrt P h (E(V↦T)) e T'; case vo of None ⇒ True | ⌊v⌋ ⇒ ∃T'. typeof⇘h⇙ v = ⌊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 ⊢ es⇩1 @ es⇩2 [:] Ts) =
  (∃Ts⇩1 Ts⇩2. Ts = Ts⇩1 @ Ts⇩2 ∧ P,E,h ⊢ es⇩1 [:] Ts⇩1 & P,E,h ⊢ es⇩2[:]Ts⇩2)"
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 ⊢ e⇩1;;e⇩2 : T⇩2"
  "P,E,h ⊢ {V:T=vo; e} : T'"

inductive_cases WTrt_elim_cases[elim!]:
  "P,E,h ⊢ newA T⌊i⌉ : U"
  "P,E,h ⊢ v :=e : T"
  "P,E,h ⊢ if (e) e⇩1 else e⇩2 : T"
  "P,E,h ⊢ while(e) c : T"
  "P,E,h ⊢ throw e : T"
  "P,E,h ⊢ try e⇩1 catch(C V) e⇩2 : T"
  "P,E,h ⊢ Cast D e : T"
  "P,E,h ⊢ e instanceof U : T"
  "P,E,h ⊢ a⌊i⌉ : T"
  "P,E,h ⊢ a⌊i⌉ := e : T"
  "P,E,h ⊢ a∙length : T"
  "P,E,h ⊢ e∙F{D} : T"
  "P,E,h ⊢ e∙F{D} := v : T"
  "P,E,h ⊢ e∙compareAndSwap(D∙F, e2, e3) : T"
  "P,E,h ⊢ e⇩1 «bop» e⇩2 : T"
  "P,E,h ⊢ new C : T"
  "P,E,h ⊢ e∙M(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