Theory WellTypeRT
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