header {* \isaheader{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"
for P :: "J_prog" and h :: "heap"
where
WTrtNew:
"is_class P C ==> WTrt P h E (new C) (Class C)"
| WTrtNewArray:
"[| WTrt P h E e Integer; is_type P T |]
==> WTrt P h E (newA T⌊e⌉) (T⌊⌉)"
| WTrtCast:
"[| WTrt P h E e T; is_type P U |] ==> WTrt P h E (Cast U e) U"
| WTrtVal:
"typeofh v = Some T ==> WTrt P h E (Val v) T"
| WTrtVar:
"E V = Some T ==> WTrt P h E (Var V) T"
| WTrtBinOp:
"[| WTrt P h E e1 T1; WTrt P h E e2 T2; P \<turnstile> T1«bop»T2 : T |]
==> WTrt P h E (e1 «bop» e2) T"
| WTrtLAss:
"[| E V = Some T; WTrt P h E e T'; P \<turnstile> T' ≤ T |]
==> WTrt P h E (V:=e) Void"
| WTrtAAcc:
"[| WTrt P h E a (T⌊⌉); WTrt P h E i Integer |]
==> WTrt P h E (a⌊i⌉) T"
| WTrtAAccNT:
"[| WTrt P h E a NT; WTrt P h E i Integer |]
==> WTrt P h E (a⌊i⌉) T"
| WTrtAAss:
"[| WTrt P h E a (T⌊⌉); WTrt P h E i Integer; WTrt P h E e T' |]
==> WTrt P h E (a⌊i⌉ := e) Void"
| WTrtAAssNT:
"[| WTrt P h E a NT; WTrt P h E i Integer; WTrt P h E e T' |]
==> WTrt P h E (a⌊i⌉ := e) Void"
| WTrtALength:
"WTrt P h E a (T⌊⌉) ==> WTrt P h E (a•length) Integer"
| WTrtALengthNT:
"WTrt P h E a NT ==> WTrt P h E (a•length) T"
| WTrtFAcc:
"[| WTrt P h E e (Class C); P \<turnstile> C has F:T in D |] ==>
WTrt P h E (e•F{D}) T"
| WTrtFAccNT:
"WTrt P h E e NT ==> WTrt P h E (e•F{D}) T"
| WTrtFAss:
"[| WTrt P h E e1 (Class C); P \<turnstile> C has F:T in D; WTrt P h E e2 T2; P \<turnstile> T2 ≤ T |]
==> WTrt P h E (e1•F{D}:=e2) Void"
| WTrtFAssNT:
"[| WTrt P h E e1 NT; WTrt P h E e2 T2 |]
==> WTrt P h E (e1•F{D}:=e2) Void"
| WTrtCall:
"[| WTrt P h E e (Class C); ¬ is_external_call P (Class C) M; P \<turnstile> C sees M:Ts -> T = (pns,body) in D;
WTrts P h E es Ts'; P \<turnstile> Ts' [≤] Ts |]
==> WTrt P h E (e•M(es)) T"
| WTrtCallNT:
"[| WTrt P h E e NT; WTrts P h E es Ts |]
==> WTrt P h E (e•M(es)) T"
| WTrtCallExternal:
"[| WTrt P h E e T; WTrts P h E es Ts; P \<turnstile> T•M(Ts) :: U |]
==> WTrt P h E (e•M(es)) U"
| WTrtBlock:
"[| WTrt P h (E(V\<mapsto>T)) e T'; case vo of None => True | ⌊v⌋ => ∃T'. typeofh v = ⌊T'⌋ ∧ P \<turnstile> T' ≤ T |]
==> WTrt P h E {V:T=vo; e} T'"
| WTrtSynchronized:
"[| WTrt P h E o' T; is_refT T; T ≠ NT; WTrt P h E e T' |]
==> WTrt P h E (sync(o') e) T'"
| WTrtSynchronizedNT:
"[| WTrt P h E o' NT; WTrt P h E e T |]
==> WTrt P h E (sync(o') e) T'"
| WTrtInSynchronized:
"[| WTrt P h E (addr a) T; WTrt P h E e T' |]
==> WTrt P h E (insync(a) e) T'"
| WTrtSeq:
"[| WTrt P h E e1 T1; WTrt P h E e2 T2 |]
==> WTrt P h E (e1;;e2) T2"
| WTrtCond:
"[| WTrt P h E e Boolean; WTrt P h E e1 T1; WTrt P h E e2 T2;
P \<turnstile> T1 ≤ T2 ∨ P \<turnstile> T2 ≤ T1; P \<turnstile> T1 ≤ T2 --> T = T2; P \<turnstile> T2 ≤ T1 --> T = T1 |]
==> WTrt P h E (if (e) e1 else e2) T"
| WTrtWhile:
"[| WTrt P h E e Boolean; WTrt P h E c T |]
==> WTrt P h E (while(e) c) Void"
| WTrtThrow:
"[| WTrt P h E e T; P \<turnstile> T ≤ Class Throwable |]
==> WTrt P h E (throw e) T'"
| WTrtTry:
"[| WTrt P h E e1 T1; WTrt P h (E(V \<mapsto> Class C)) e2 T2; P \<turnstile> T1 ≤ T2 |]
==> WTrt P h E (try e1 catch(C V) e2) T2"
| WTrtNil: "WTrts P h E [] []"
| WTrtCons: "[| WTrt P h E e T; WTrts P h E es Ts |] ==> WTrts P h E (e # es) (T # Ts)"
abbreviation
WTrt_syntax :: "J_prog => env => heap => expr => ty => bool" ("_,_,_ \<turnstile> _ : _" [51,51,51]50)
where
"P,E,h \<turnstile> e : T ≡ WTrt P h E e T"
abbreviation
WTrts_syntax :: "J_prog => env => heap => expr list => ty list => bool" ("_,_,_ \<turnstile> _ [:] _" [51,51,51]50)
where
"P,E,h \<turnstile> es [:] Ts ≡ WTrts P h E es Ts"
declare WTrt_WTrts.intros[intro!]
declare
WTrtFAcc[rule del] WTrtFAccNT[rule del]
WTrtFAss[rule del] WTrtFAssNT[rule del]
WTrtCall[rule del] WTrtCallNT[rule del]
WTrtCallExternal[rule del]
WTrtAAcc[rule del, intro] WTrtAAccNT[rule del, intro]
WTrtAAss[rule del, intro] WTrtAAssNT[rule del, intro]
WTrtALength[rule del, intro] WTrtALengthNT[rule del, intro]
WTrtSynchronized[rule del, intro] WTrtSynchronizedNT[rule del, intro]
subsection{*Easy consequences*}
lemma [iff]: "(P,E,h \<turnstile> [] [:] Ts) = (Ts = [])"
by (auto elim: WTrts.cases)
lemma [iff]: "(P,E,h \<turnstile> e#es [:] T#Ts) = (P,E,h \<turnstile> e : T ∧ P,E,h \<turnstile> es [:] Ts)"
by (auto elim: WTrts.cases)
lemma WTrts_conv_list_all2: "P,E,h \<turnstile> es [:] Ts = list_all2 (WTrt P h E) es Ts"
by(induct es arbitrary: Ts)(auto simp add: list_all2_Cons1 elim: WTrts.cases)
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)"
by(auto simp add: WTrts_conv_list_all2 list_all2_Cons1)
lemma [simp]: "(P,E,h \<turnstile> es1 @ es2 [:] Ts) =
(∃Ts1 Ts2. Ts = Ts1 @ Ts2 ∧ P,E,h \<turnstile> es1 [:] Ts1 & P,E,h \<turnstile> es2[:]Ts2)"
by(auto simp add: WTrts_conv_list_all2 list_all2_append1 dest: list_all2_lengthD[symmetric])
lemma [iff]: "P,E,h \<turnstile> Val v : T = (typeofh v = Some T)"
proof
assume "P,E,h \<turnstile> Val v : T"
thus "typeofh v = Some T" by - (erule WTrt.cases, auto)
next
assume "typeofh v = ⌊T⌋"
thus "P,E,h \<turnstile> Val v : T" by - (rule WTrtVal)
qed
lemma [iff]: "P,E,h \<turnstile> Var v : T = (E v = Some T)"
by (auto elim: WTrt.cases)
lemma [iff]: "P,E,h \<turnstile> e1;;e2 : T2 = (∃T1. P,E,h \<turnstile> e1:T1 ∧ P,E,h \<turnstile> e2:T2)"
by (auto elim: WTrt.cases)
lemma [iff]: "P,E,h \<turnstile> {V:T=vo; e} : T' = (P,E(V\<mapsto>T),h \<turnstile> e : T' ∧ (case vo of None => True | ⌊v⌋ => ∃T'. typeofh v = ⌊T'⌋ ∧ P \<turnstile> T' ≤ T))"
by (auto elim: WTrt.cases)
inductive_cases WTrt_elim_cases[elim!]:
"P,E,h \<turnstile> newA T⌊i⌉ : U"
"P,E,h \<turnstile> v :=e : 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"
"P,E,h \<turnstile> try e1 catch(C V) e2 : T"
"P,E,h \<turnstile> Cast D e : T"
"P,E,h \<turnstile> a⌊i⌉ : T"
"P,E,h \<turnstile> a⌊i⌉ := e : T"
"P,E,h \<turnstile> a•length : T"
"P,E,h \<turnstile> e•F{D} : T"
"P,E,h \<turnstile> e•F{D} := v : T"
"P,E,h \<turnstile> e1 «bop» e2 : T"
"P,E,h \<turnstile> new C : T"
"P,E,h \<turnstile> e•M(es) : T"
"P,E,h \<turnstile> sync(o') e : T"
"P,E,h \<turnstile> insync(a) e : T"
subsection{*Some interesting lemmas*}
lemma WTrts_Val[simp]:
"P,E,h \<turnstile> map Val vs [:] Ts <-> map (typeofh) vs = map Some Ts"
apply(induct vs arbitrary: Ts)
apply simp
apply(case_tac Ts)
apply simp
apply simp
done
lemma WTrt_env_mono: "P,E,h \<turnstile> e : T ==> (!!E'. E ⊆m E' ==> P,E',h \<turnstile> e : T)"
and WTrts_env_mono: "P,E,h \<turnstile> es [:] Ts ==> (!!E'. E ⊆m E' ==> P,E',h \<turnstile> es [:] Ts)"
apply(induct rule: WTrt_WTrts.inducts)
apply(simp add: WTrtNew)
apply(fastsimp simp: WTrtNewArray)
apply(fastsimp simp: WTrtCast)
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(force simp: WTrtAAcc)
apply(force simp: WTrtAAccNT)
apply(rule WTrtAAss, fastsimp, blast, blast)
apply(fastsimp)
apply(rule WTrtALength, blast)
apply(blast)
apply(fastsimp simp: WTrtFAcc)
apply(simp add: WTrtFAccNT)
apply(fastsimp simp: WTrtFAss)
apply(fastsimp simp: WTrtFAssNT)
apply(fastsimp simp: WTrtCall)
apply(fastsimp simp: WTrtCallNT)
apply(fastsimp intro: WTrtCallExternal)
apply(fastsimp simp: map_le_def)
apply(rule WTrtSynchronized)
apply(blast)
apply(assumption)
apply(fastsimp)
apply(fastsimp intro: WTrtInSynchronized)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp simp: WTrtSeq)
apply(fastsimp simp: WTrtCond)
apply(fastsimp simp: WTrtWhile)
apply(fastsimp simp: WTrtThrow)
apply(auto simp: WTrtTry map_le_def dom_def)
done
lemma WTrt_hext_mono: "P,E,h \<turnstile> e : T ==> h \<unlhd> h' ==> P,E,h' \<turnstile> e : T"
and WTrts_hext_mono: "P,E,h \<turnstile> es [:] Ts ==> h \<unlhd> h' ==> P,E,h' \<turnstile> es [:] Ts"
apply(induct rule: WTrt_WTrts.inducts)
apply(simp add: WTrtNew)
apply(fastsimp simp: WTrtNewArray)
apply(fastsimp simp: WTrtCast)
apply(fastsimp simp: WTrtVal dest:hext_typeof_mono)
apply(simp add: WTrtVar)
apply(fastsimp simp add: WTrtBinOp)
apply(fastsimp simp add: WTrtLAss)
apply(rule WTrtAAcc)
apply(simp)
apply(simp)
apply(rule WTrtAAccNT)
apply(simp)
apply(simp)
apply(rule WTrtAAss)
apply(simp)
apply(simp)
apply(simp)
apply(simp)
apply(rule WTrtAAssNT)
apply(simp)
apply(simp)
apply(simp)
apply(rule WTrtALength, blast)
apply(rule WTrtALengthNT, blast)
apply(fast intro: WTrtFAcc)
apply(simp add: WTrtFAccNT)
apply(fastsimp simp: WTrtFAss del:WTrt_WTrts.intros WTrt_elim_cases)
apply(fastsimp simp: WTrtFAssNT)
apply(fastsimp simp: WTrtCall)
apply(fastsimp simp: WTrtCallNT)
apply(fastsimp intro: WTrtCallExternal)
apply(fastsimp intro: hext_typeof_mono)
apply(rule WTrtSynchronized)
apply(blast)
apply(assumption)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp intro: WTrtInSynchronized)
apply(fastsimp simp add: WTrtSeq)
apply(fastsimp simp add: WTrtCond)
apply(fastsimp simp add: WTrtWhile)
apply(fastsimp simp add: WTrtThrow)
apply(fastsimp simp: WTrtTry)
apply(fastsimp)+
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"
apply(induct rule: WT_WTs.inducts)
apply fast
apply fast
apply fast
apply(fastsimp dest:typeof_lit_typeof)
apply(simp)
apply(fastsimp intro: WT_binop_WTrt_binop)
apply(fastsimp)
apply(erule WTrtAAcc)
apply(assumption)
apply(erule WTrtAAss)
apply(assumption)+
apply(erule WTrtALength)
apply(fastsimp simp: WTrtFAcc has_visible_field)
apply(fastsimp simp: WTrtFAss dest: has_visible_field)
apply(fastsimp simp: WTrtCall)
apply(fastsimp intro: WTrtCallExternal)
apply(clarsimp simp del: fun_upd_apply, blast intro: typeof_lit_typeof)
apply(erule WTrtSynchronized)
apply(assumption)+
apply(fastsimp)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp)
apply(fastsimp)
done
end