# 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(fastforce simp: WTrtDynCast)
apply(fastforce simp: WTrtStaticCast)
apply(fastforce simp: WTrtVal)
apply (force simp:map_le_def)
apply(fastforce simp: WTrtFAcc)
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)
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
```