# Theory WellTypeRT

```(*  Title:      Jinja/J/WellTypeRT.thy

Author:     Tobias Nipkow
*)

section ‹Runtime Well-typedness›

theory WellTypeRT
imports WellType
begin

inductive
WTrt :: "J_prog ⇒ heap ⇒ env ⇒ expr ⇒ ty ⇒ bool"
and WTrts :: "J_prog ⇒ heap ⇒ env ⇒ expr list ⇒ ty list ⇒ bool"
and WTrt2 :: "[J_prog,env,heap,expr,ty] ⇒ bool"
("_,_,_ ⊢ _ : _"   [51,51,51]50)
and WTrts2 :: "[J_prog,env,heap,expr list, ty list] ⇒ bool"
("_,_,_ ⊢ _ [:] _" [51,51,51]50)
for P :: J_prog and h :: heap
where

"P,E,h ⊢ e : T ≡ WTrt P h E e T"
| "P,E,h ⊢ es[:]Ts ≡ WTrts P h E es Ts"

| WTrtNew:
"is_class P C  ⟹
P,E,h ⊢ new C : Class C"

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

| WTrtVal:
"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"
*)
| WTrtBinOpEq:
"⟦ P,E,h ⊢ e⇩1 : T⇩1;  P,E,h ⊢ e⇩2 : T⇩2 ⟧
⟹ P,E,h ⊢ e⇩1 «Eq» e⇩2 : Boolean"

"⟦ P,E,h ⊢ e⇩1 : Integer;  P,E,h ⊢ e⇩2 : Integer ⟧
⟹ P,E,h ⊢ e⇩1 «Add» e⇩2 : Integer"

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

| WTrtFAcc:
"⟦ P,E,h ⊢ e : Class C; P ⊢ C has F:T in D ⟧ ⟹
P,E,h ⊢ e∙F{D} : T"

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

| WTrtFAss:
"⟦ P,E,h ⊢ e⇩1 : Class C;  P ⊢ C has F:T in D; P,E,h ⊢ e⇩2 : T⇩2;  P ⊢ T⇩2 ≤ T ⟧
⟹ P,E,h ⊢ e⇩1∙F{D}:=e⇩2 : Void"

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

| WTrtCall:
"⟦ P,E,h ⊢ e : Class C; P ⊢ C sees M:Ts → T = (pns,body) in D;
P,E,h ⊢ es [:] Ts'; P ⊢ Ts' [≤] Ts ⟧
⟹ P,E,h ⊢ e∙M(es) : T"

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

| WTrtBlock:
"P,E(V↦T),h ⊢ e : 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⇩1;  P,E,h ⊢ e⇩2:T⇩2;
P ⊢ T⇩1 ≤ T⇩2 ∨ P ⊢ T⇩2 ≤ T⇩1; P ⊢ T⇩1 ≤ T⇩2 ⟶ T = T⇩2; P ⊢ T⇩2 ≤ T⇩1 ⟶ T = T⇩1 ⟧
⟹ 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⇩r; is_refT T⇩r ⟧ ⟹
P,E,h ⊢ throw e : T"

| WTrtTry:
"⟦ P,E,h ⊢ e⇩1 : T⇩1;  P,E(V ↦ Class C),h ⊢ e⇩2 : T⇩2; P ⊢ T⇩1 ≤ T⇩2 ⟧
⟹ P,E,h ⊢ try e⇩1 catch(C V) e⇩2 : T⇩2"

― ‹well-typed expression lists›

| 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›

lemma [iff]: "(P,E,h ⊢ [] [:] Ts) = (Ts = [])"
(*<*)by(rule iffI) (auto elim: WTrts.cases)(*>*)

lemma [iff]: "(P,E,h ⊢ e#es [:] T#Ts) = (P,E,h ⊢ e : T ∧ P,E,h ⊢ es [:] Ts)"
(*<*)by(rule iffI) (auto elim: WTrts.cases)(*>*)

lemma [iff]: "(P,E,h ⊢ (e#es) [:] Ts) =
(∃U Us. Ts = U#Us ∧ P,E,h ⊢ e : U ∧ P,E,h ⊢ es [:] Us)"
(*<*)by(rule iffI) (auto elim: WTrts.cases)(*>*)

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)"
(*<*)
proof(induct es⇩1)
case (Cons a list)
let ?lhs = "λTs. (∃U Us. Ts = U # Us ∧ P,E,h ⊢ a : U ∧
(∃Ts⇩1 Ts⇩2. Us = Ts⇩1 @ Ts⇩2 ∧ P,E,h ⊢ list [:] Ts⇩1 ∧ P,E,h ⊢ es⇩2 [:] Ts⇩2))"
let ?rhs = "λTs. (∃Ts⇩1 Ts⇩2. Ts = Ts⇩1 @ Ts⇩2 ∧
(∃U Us. Ts⇩1 = U # Us ∧ P,E,h ⊢ a : U ∧ P,E,h ⊢ list [:] Us) ∧ P,E,h ⊢ es⇩2 [:] Ts⇩2)"
{ fix Ts assume "?lhs Ts"
then have "?rhs Ts" by (auto intro: Cons_eq_appendI)
}
moreover {
fix Ts assume "?rhs Ts"
then have "?lhs Ts" by fastforce
}
ultimately have "⋀Ts. ?lhs Ts = ?rhs Ts" by(rule iffI)
then show ?case by (clarsimp simp: Cons)
qed simp
(*>*)

lemma [iff]: "P,E,h ⊢ Val v : T = (typeof⇘h⇙ v = Some T)"
(*<*)proof(rule iffI) qed (auto elim: WTrt.cases)(*>*)

lemma [iff]: "P,E,h ⊢ Var v : T = (E v = Some T)"
(*<*)proof(rule iffI) qed (auto elim: WTrt.cases)(*>*)

lemma [iff]: "P,E,h ⊢ e⇩1;;e⇩2 : T⇩2 = (∃T⇩1. P,E,h ⊢ e⇩1:T⇩1 ∧ P,E,h ⊢ e⇩2:T⇩2)"
(*<*)proof(rule iffI) qed (auto elim: WTrt.cases)(*>*)

lemma [iff]: "P,E,h ⊢ {V:T; e} : T'  =  (P,E(V↦T),h ⊢ e : T')"
(*<*)proof(rule iffI) qed (auto elim: WTrt.cases)(*>*)

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

subsection‹Some interesting lemmas›

lemma WTrts_Val[simp]:
"⋀Ts. (P,E,h ⊢ map Val vs [:] Ts) = (map (typeof⇘h⇙) vs = map Some Ts)"
(*<*)
proof(induct vs)
case (Cons a vs)
then show ?case by(case_tac Ts; simp)
qed simp
(*>*)

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)"
(*<*)
proof(induct rule: WTrt_inducts)
case WTrtVar then show ?case by(simp add: map_le_def dom_def)
next
case WTrtLAss then show ?case by(force simp:map_le_def)
qed(fastforce intro: WTrt_WTrts.intros)+
(*>*)

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"
(*<*)
proof(induct rule: WTrt_inducts)
case WTrtVal then show ?case by(simp add: hext_typeof_mono)
qed(fastforce intro: WTrt_WTrts.intros)+
(*>*)

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 then show ?case by(fastforce dest: typeof_lit_typeof)
next
case WTFAcc
then show ?case by(fastforce simp: WTrtFAcc has_visible_field)
next
case WTFAss
then show ?case by(fastforce simp: WTrtFAss dest: has_visible_field)
qed(fastforce intro: WTrt_WTrts.intros)+
(*>*)

end
```