header {* \isaheader{Runtime Well-typedness} *}
theory WellTypeRT imports WellType begin
section {* Run time types *}
consts
typeof_h :: "prog => heap => val => ty option" ("_ \<turnstile> typeof_")
primrec
"P \<turnstile> typeofh Unit = Some Void"
"P \<turnstile> typeofh Null = Some NT"
"P \<turnstile> typeofh (Bool b) = Some Boolean"
"P \<turnstile> typeofh (Intg i) = Some Integer"
"P \<turnstile> typeofh (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 \<turnstile> typeofh v = Some T"
by(induct v)auto
lemma typeof_Void [simp]: "P \<turnstile> typeofh v = Some Void ==> v = Unit"
by(induct v,auto split:split_if_asm)
lemma typeof_NT [simp]: "P \<turnstile> typeofh v = Some NT ==> v = Null"
by(induct v,auto split:split_if_asm)
lemma typeof_Boolean [simp]: "P \<turnstile> typeofh v = Some Boolean ==> ∃b. v = Bool b"
by(induct v,auto split:split_if_asm)
lemma typeof_Integer [simp]: "P \<turnstile> typeofh v = Some Integer ==> ∃i. v = Intg i"
by(induct v,auto split:split_if_asm)
lemma typeof_Class_Subo:
"P \<turnstile> typeofh 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:split_if_asm)
section {* The rules *}
inductive
WTrt :: "[prog,env,heap,expr, ty ] => bool"
("_,_,_ \<turnstile> _ : _" [51,51,51]50)
and WTrts :: "[prog,env,heap,expr list,ty list] => bool"
("_,_,_ \<turnstile> _ [:] _" [51,51,51]50)
for P :: prog
where
WTrtNew:
"is_class P C ==>
P,E,h \<turnstile> new C : Class C"
| WTrtDynCast:
"[| P,E,h \<turnstile> e : T; is_refT T; is_class P C |]
==> P,E,h \<turnstile> Cast C e : Class C"
| WTrtStaticCast:
"[| P,E,h \<turnstile> e : T; is_refT T; is_class P C |]
==> P,E,h \<turnstile> (|C|)),e : Class C"
| WTrtVal:
"P \<turnstile> typeofh v = Some T ==>
P,E,h \<turnstile> Val v : T"
| WTrtVar:
"E V = Some T ==>
P,E,h \<turnstile> Var V : T"
| WTrtBinOp:
"[| P,E,h \<turnstile> e1 : T1; P,E,h \<turnstile> e2 : T2;
case bop of Eq => T = Boolean
| Add => T1 = Integer ∧ T2 = Integer ∧ T = Integer |]
==> P,E,h \<turnstile> e1 «bop» e2 : T"
| WTrtLAss:
"[| E V = Some T; P,E,h \<turnstile> e : T'; P \<turnstile> T' ≤ T |]
==> P,E,h \<turnstile> V:=e : T"
| WTrtFAcc:
"[|P,E,h \<turnstile> e : Class C; Cs ≠ []; P \<turnstile> C has least F:T via Cs |]
==> P,E,h \<turnstile> e•F{Cs} : T"
| WTrtFAccNT:
"P,E,h \<turnstile> e : NT ==> P,E,h \<turnstile> e•F{Cs} : T"
| WTrtFAss:
"[|P,E,h \<turnstile> e1 : Class C; Cs ≠ [];
P \<turnstile> C has least F:T via Cs; P,E,h \<turnstile> e2 : T'; P \<turnstile> T' ≤ T |]
==> P,E,h \<turnstile> e1•F{Cs}:=e2 : T"
| WTrtFAssNT:
"[| P,E,h \<turnstile> e1 : NT; P,E,h \<turnstile> e2 : T'; P \<turnstile> T' ≤ T |]
==> P,E,h \<turnstile> e1•F{Cs}:=e2 : T"
| WTrtCall:
"[| P,E,h \<turnstile> e : Class C; P \<turnstile> C has least M = (Ts,T,m) via Cs;
P,E,h \<turnstile> es [:] Ts'; P \<turnstile> Ts' [≤] Ts |]
==> P,E,h \<turnstile> e•M(es) : T"
| WTrtStaticCall:
"[| P,E,h \<turnstile> e : Class C'; P \<turnstile> Path C' to C unique;
P \<turnstile> C has least M = (Ts,T,m) via Cs;
P,E,h \<turnstile> es [:] Ts'; P \<turnstile> Ts' [≤] Ts |]
==> P,E,h \<turnstile> e•(C::)M(es) : T"
| WTrtCallNT:
"[|P,E,h \<turnstile> e : NT; P,E,h \<turnstile> es [:] Ts|] ==> P,E,h \<turnstile> Call e Copt M es : T"
| WTrtBlock:
"[|P,E(V\<mapsto>T),h \<turnstile> e : T'; is_type P T|] ==>
P,E,h \<turnstile> {V:T; e} : T'"
| WTrtSeq:
"[| P,E,h \<turnstile> e1 : T1; P,E,h \<turnstile> e2 : T2 |] ==> P,E,h \<turnstile> e1;;e2 : T2"
| WTrtCond:
"[| P,E,h \<turnstile> e : Boolean; P,E,h \<turnstile> e1 : T; P,E,h \<turnstile> e2 : T |]
==> P,E,h \<turnstile> if (e) e1 else e2 : T"
| WTrtWhile:
"[| P,E,h \<turnstile> e : Boolean; P,E,h \<turnstile> c : T |]
==> P,E,h \<turnstile> while(e) c : Void"
| WTrtThrow:
"[|P,E,h \<turnstile> e : T'; is_refT T'|]
==> P,E,h \<turnstile> throw e : T"
| WTrtNil:
"P,E,h \<turnstile> [] [:] []"
| WTrtCons:
"[| P,E,h \<turnstile> e : T; P,E,h \<turnstile> es [:] Ts |] ==> P,E,h \<turnstile> 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)]
section{*Easy consequences*}
lemma [iff]: "(P,E,h \<turnstile> [] [:] Ts) = (Ts = [])"
apply(rule iffI)
apply (auto elim: WTrts.cases)
done
lemma [iff]: "(P,E,h \<turnstile> e#es [:] T#Ts) = (P,E,h \<turnstile> e : T ∧ P,E,h \<turnstile> es [:] Ts)"
apply(rule iffI)
apply (auto elim: WTrts.cases)
done
lemma [iff]: "(P,E,h \<turnstile> (e#es) [:] Ts) =
(∃U Us. Ts = U#Us ∧ P,E,h \<turnstile> e : U ∧ P,E,h \<turnstile> es [:] Us)"
apply(rule iffI)
apply (auto elim: WTrts.cases)
done
lemma [simp]: "∀Ts. (P,E,h \<turnstile> es1 @ es2 [:] Ts) =
(∃Ts1 Ts2. Ts = Ts1 @ Ts2 ∧ P,E,h \<turnstile> es1 [:] Ts1 & P,E,h \<turnstile> es2 [:] Ts2)"
apply(induct_tac es1)
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 fastsimp
done
lemma [iff]: "P,E,h \<turnstile> Val v : T = (P \<turnstile> typeofh v = Some T)"
apply(rule iffI)
apply (auto elim: WTrt.cases)
done
lemma [iff]: "P,E,h \<turnstile> Var V : T = (E V = Some T)"
apply(rule iffI)
apply (auto elim: WTrt.cases)
done
lemma [iff]: "P,E,h \<turnstile> e1;;e2 : T2 = (∃T1. P,E,h \<turnstile> e1:T1 ∧ P,E,h \<turnstile> e2:T2)"
apply(rule iffI)
apply (auto elim: WTrt.cases)
done
lemma [iff]: "P,E,h \<turnstile> {V:T; e} : T' = (P,E(V\<mapsto>T),h \<turnstile> e : T' ∧ is_type P T)"
apply(rule iffI)
apply (auto elim: WTrt.cases)
done
inductive_cases WTrt_elim_cases[elim!]:
"P,E,h \<turnstile> new C : T"
"P,E,h \<turnstile> Cast C e : T"
"P,E,h \<turnstile> (|C|)),e : T"
"P,E,h \<turnstile> e1 «bop» e2 : T"
"P,E,h \<turnstile> V:=e : T"
"P,E,h \<turnstile> e•F{Cs} : T"
"P,E,h \<turnstile> e•F{Cs} := v : T"
"P,E,h \<turnstile> e•M(es) : T"
"P,E,h \<turnstile> e•(C::)M(es) : T"
"P,E,h \<turnstile> if (e) e1 else e2 : T"
"P,E,h \<turnstile> while(e) c : T"
"P,E,h \<turnstile> throw e : T"
section{*Some interesting lemmas*}
lemma WTrts_Val[simp]:
"!!Ts. (P,E,h \<turnstile> map Val vs [:] Ts) = (map (λv. (P \<turnstile> typeofh) v) vs = map Some Ts)"
apply(induct vs)
apply fastsimp
apply(case_tac Ts)
apply simp
apply simp
done
lemma WTrts_same_length: "!!Ts. P,E,h \<turnstile> es [:] Ts ==> length es = length Ts"
by(induct es type:list)auto
lemma WTrt_env_mono:
"P,E,h \<turnstile> e : T ==> (!!E'. E ⊆m E' ==> P,E',h \<turnstile> e : T)" and
"P,E,h \<turnstile> es [:] Ts ==> (!!E'. E ⊆m E' ==> P,E',h \<turnstile> es [:] Ts)"
apply(induct rule: WTrt_inducts)
apply(simp add: WTrtNew)
apply(fastsimp simp: WTrtDynCast)
apply(fastsimp simp: WTrtStaticCast)
apply(fastsimp simp: WTrtVal)
apply(simp add: WTrtVar map_le_def dom_def)
apply(fastsimp simp add: WTrtBinOp)
apply (force simp:map_le_def)
apply(fastsimp simp: WTrtFAcc)
apply(simp add: WTrtFAccNT)
apply(fastsimp simp: WTrtFAss)
apply(fastsimp simp: WTrtFAssNT)
apply(fastsimp simp: WTrtCall)
apply(fastsimp simp: WTrtStaticCall)
apply(fastsimp simp: WTrtCallNT)
apply(fastsimp simp: map_le_def)
apply(fastsimp)
apply(fastsimp simp: WTrtCond)
apply(fastsimp simp: WTrtWhile)
apply(fastsimp simp: WTrtThrow)
apply(simp add: WTrtNil)
apply(simp add: WTrtCons)
done
lemma WT_implies_WTrt: "P,E \<turnstile> e :: T ==> P,E,h \<turnstile> e : T"
and WTs_implies_WTrts: "P,E \<turnstile> es [::] Ts ==> P,E,h \<turnstile> es [:] Ts"
proof(induct rule: WT_WTs_inducts)
case WTVal thus ?case by (fastsimp dest:type_eq_type)
next
case WTBinOp thus ?case by (fastsimp split:bop.splits)
next
case WTFAcc thus ?case
by(fastsimp intro!:WTrtFAcc dest:Subobjs_nonempty
simp:LeastFieldDecl_def FieldDecls_def)
next
case WTFAss thus ?case
by(fastsimp intro!:WTrtFAss dest:Subobjs_nonempty
simp:LeastFieldDecl_def FieldDecls_def)
next
case WTCall thus ?case by (fastsimp intro:WTrtCall)
qed (auto simp del:fun_upd_apply)
end