Theory WellTypeRT

(*  Title:       CoreC++
    Author:      Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

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

section ‹Runtime Well-typedness›

theory WellTypeRT imports WellType begin


subsection ‹Run time types›

primrec typeof_h :: "prog ⇒ heap ⇒ val ⇒ ty option" (‹_ ⊢ typeof⇘_⇙›) where
  "P ⊢ typeof⇘h⇙ Unit     = Some Void"
| "P ⊢ typeof⇘h⇙ Null     = Some NT"
| "P ⊢ typeof⇘h⇙ (Bool b) = Some Boolean"
| "P ⊢ typeof⇘h⇙ (Intg i) = Some Integer"
| "P ⊢ typeof⇘h⇙ (Ref r)  = (case h (the_addr (Ref r)) of None ⇒ None 
                            | Some(C,S) ⇒ (if Subobjs P C (the_path(Ref r)) then
                                   Some(Class(last(the_path(Ref r))))
                                            else None))"


lemma type_eq_type: "typeof v = Some T ⟹ P ⊢ typeof⇘h⇙ v = Some T"
by(induct v)auto

lemma typeof_Void [simp]: "P ⊢ typeof⇘h⇙ v = Some Void ⟹ v = Unit"
by(induct v,auto split:if_split_asm)

lemma typeof_NT [simp]: "P ⊢ typeof⇘h⇙ v = Some NT ⟹ v = Null"
by(induct v,auto split:if_split_asm)

lemma typeof_Boolean [simp]: "P ⊢ typeof⇘h⇙ v = Some Boolean ⟹ ∃b. v = Bool b"
by(induct v,auto split:if_split_asm)

lemma typeof_Integer [simp]: "P ⊢ typeof⇘h⇙ v = Some Integer ⟹ ∃i. v = Intg i"
by(induct v,auto split:if_split_asm)

lemma typeof_Class_Subo: 
"P ⊢ typeof⇘h⇙ v = Some (Class C) ⟹ 
∃a Cs D S. v = Ref(a,Cs) ∧ h a = Some(D,S) ∧ Subobjs P D Cs ∧ last Cs = C"
by(induct v,auto split:if_split_asm)

subsection ‹The rules›

inductive
  WTrt :: "[prog,env,heap,expr,     ty     ] ⇒ bool"
        (‹_,_,_ ⊢ _ : _›   [51,51,51]50)
  and WTrts :: "[prog,env,heap,expr list,ty list] ⇒ bool"
        (‹_,_,_ ⊢ _ [:] _› [51,51,51]50)
  for P :: prog
where
  
  WTrtNew:
  "is_class P C  ⟹ 
  P,E,h ⊢ new C : Class C"

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

| WTrtStaticCast:
  "⟦ P,E,h ⊢ e : T; is_refT T; is_class P C ⟧
  ⟹ P,E,h ⊢ ⦇C⦈e : Class C"

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

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

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

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

| WTrtFAcc:
"⟦P,E,h ⊢ e : Class C; Cs ≠ []; P ⊢ C has least F:T via Cs ⟧
  ⟹ P,E,h ⊢ e∙F{Cs} : T"

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

| WTrtFAss:
"⟦P,E,h ⊢ e⇩1 : Class C; Cs ≠ [];
  P ⊢ C has least F:T via Cs; P,E,h ⊢ e⇩2 : T'; P ⊢ T' ≤ T ⟧
  ⟹ P,E,h ⊢ e⇩1∙F{Cs}:=e⇩2 : T"

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

| WTrtCall:
  "⟦ P,E,h ⊢ e : Class C;  P ⊢ C has least M = (Ts,T,m) via Cs;
     P,E,h ⊢ es [:] Ts'; P ⊢ Ts' [≤] Ts ⟧
  ⟹ P,E,h ⊢ e∙M(es) : T" 

| WTrtStaticCall:
  "⟦ P,E,h ⊢ e : Class C'; P ⊢ Path C' to C unique;
     P ⊢ C has least M = (Ts,T,m) via Cs; 
     P,E,h ⊢ es [:] Ts'; P ⊢ Ts' [≤] Ts ⟧
  ⟹ P,E,h ⊢ e∙(C::)M(es) : T"

| WTrtCallNT:
  "⟦P,E,h ⊢ e : NT; P,E,h ⊢ es [:] Ts⟧ ⟹ P,E,h ⊢ Call e Copt M es : T"

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

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

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

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

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


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

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




declare
  WTrt_WTrts.intros[intro!]
  WTrtNil[iff]
declare
  WTrtFAcc[rule del] WTrtFAccNT[rule del]
  WTrtFAss[rule del] WTrtFAssNT[rule del]
  WTrtCall[rule del] WTrtCallNT[rule del]

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


subsection‹Easy consequences›

inductive_simps [iff]:
  "P,E,h ⊢ [] [:] Ts"
  "P,E,h ⊢ e#es [:] T#Ts"
  "P,E,h ⊢ (e#es) [:] Ts"
  "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; e} : T'"


lemma [simp]: "∀Ts. (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)"

apply(induct_tac es⇩1)
 apply simp
apply clarsimp
apply(erule thin_rl)
apply (rule iffI)
 apply clarsimp
 apply(rule exI)+
 apply(rule conjI)
  prefer 2 apply blast
 apply simp
apply fastforce
done



inductive_cases WTrt_elim_cases[elim!]:
  "P,E,h ⊢ new C : T"
  "P,E,h ⊢ Cast C e : T"
  "P,E,h ⊢ ⦇C⦈e : T"
  "P,E,h ⊢ e⇩1 «bop» e⇩2 : T"
  "P,E,h ⊢ V:=e : T"
  "P,E,h ⊢ e∙F{Cs} : T"
  "P,E,h ⊢ e∙F{Cs} := v : T"
  "P,E,h ⊢ e∙M(es) : T"
  "P,E,h ⊢ e∙(C::)M(es) : 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"


subsection‹Some interesting lemmas›


lemma WTrts_Val[simp]:
 "⋀Ts. (P,E,h ⊢ map Val vs [:] Ts) = (map (λv. (P ⊢ typeof⇘h⇙) v) vs = map Some Ts)"

apply(induct vs)
 apply fastforce
apply(case_tac Ts)
 apply simp
apply simp
done



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


lemma WTrt_env_mono:
  "P,E,h ⊢ e : T ⟹ (⋀E'. E ⊆⇩m E' ⟹ P,E',h ⊢ e : T)" and
  "P,E,h ⊢ es [:] Ts ⟹ (⋀E'. E ⊆⇩m E' ⟹ P,E',h ⊢ es [:] Ts)"

apply(induct rule: WTrt_inducts)
apply(simp add: WTrtNew)
apply(fastforce simp: WTrtDynCast)
apply(fastforce simp: WTrtStaticCast)
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(fastforce simp: WTrtFAcc)
apply(simp add: WTrtFAccNT)
apply(fastforce simp: WTrtFAss)
apply(fastforce simp: WTrtFAssNT)
apply(fastforce simp: WTrtCall)
apply(fastforce simp: WTrtStaticCall)
apply(fastforce simp: WTrtCallNT)
apply(fastforce simp: map_le_def)
apply(fastforce)
apply(fastforce simp: WTrtCond)
apply(fastforce simp: WTrtWhile)
apply(fastforce simp: WTrtThrow)
apply(simp add: WTrtNil)
apply(simp add: WTrtCons)
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"

proof(induct rule: WT_WTs_inducts)
  case WTVal thus ?case by (fastforce dest:type_eq_type)
next
  case WTBinOp thus ?case by (fastforce split:bop.splits)
next
  case WTFAcc thus ?case
    by(fastforce intro!:WTrtFAcc dest:Subobjs_nonempty 
                  simp:LeastFieldDecl_def FieldDecls_def)
next
  case WTFAss thus ?case
    by(fastforce intro!:WTrtFAss dest:Subobjs_nonempty
                  simp:LeastFieldDecl_def FieldDecls_def)
next
  case WTCall thus ?case by (fastforce intro:WTrtCall)
qed (auto simp del:fun_upd_apply)


end