header {* \isaheader{Heap Extension} *}
theory HeapExtension imports Progress begin
section {* The Heap Extension *}
constdefs
hext :: "heap => heap => bool" ("_ \<unlhd> _" [51,51] 50)
"h \<unlhd> h' ≡ ∀a C S. h a = Some(C,S) --> (∃S'. h' a = Some(C,S'))"
lemma hextI: "∀a C S. h a = Some(C,S) --> (∃S'. h' a = Some(C,S')) ==> h \<unlhd> h'"
apply (unfold hext_def)
apply auto
done
lemma hext_objD: "[| h \<unlhd> h'; h a = Some(C,S) |] ==> ∃S'. h' a = Some(C,S')"
apply (unfold hext_def)
apply (force)
done
lemma hext_refl [iff]: "h \<unlhd> h"
apply (rule hextI)
apply (fast)
done
lemma hext_new [simp]: "h a = None ==> h \<unlhd> h(a\<mapsto>x)"
apply (rule hextI)
apply (auto simp:fun_upd_apply)
done
lemma hext_trans: "[| h \<unlhd> h'; h' \<unlhd> h'' |] ==> h \<unlhd> h''"
apply (rule hextI)
apply (fast dest: hext_objD)
done
lemma hext_upd_obj: "h a = Some (C,S) ==> h \<unlhd> h(a\<mapsto>(C,S'))"
apply (rule hextI)
apply (auto simp:fun_upd_apply)
done
section {* @{text"\<unlhd>"} and preallocated *}
lemma preallocated_hext:
"[| preallocated h; h \<unlhd> h' |] ==> preallocated h'"
by (simp add: preallocated_def hext_def)
lemmas preallocated_upd_obj = preallocated_hext [OF _ hext_upd_obj]
lemmas preallocated_new = preallocated_hext [OF _ hext_new]
section {* @{text"\<unlhd>"} in Small- and BigStep *}
lemma red_hext_incr: "P,E \<turnstile> ⟨e,(h,l)⟩ -> ⟨e',(h',l')⟩ ==> h \<unlhd> h'"
and reds_hext_incr: "P,E \<turnstile> ⟨es,(h,l)⟩ [->] ⟨es',(h',l')⟩ ==> h \<unlhd> h'"
proof(induct rule:red_reds_inducts)
case RedNew thus ?case
by(fastsimp dest:new_Addr_SomeD simp:hext_def split:if_splits)
next
case RedFAss thus ?case by(simp add:hext_def split:if_splits)
qed simp_all
lemma step_hext_incr: "P,E \<turnstile> ⟨e,s⟩ ->* ⟨e',s'⟩ ==> hp s \<unlhd> hp s'"
proof(induct rule:converse_rtrancl_induct2)
case refl thus ?case by(rule hext_refl)
next
case (step e s e'' s'')
have Red:"((e, s), e'', s'') ∈ Red P E"
and hext:"hp s'' \<unlhd> hp s'" by fact+
from Red have "P,E \<turnstile> ⟨e,s⟩ -> ⟨e'',s''⟩" by simp
hence "hp s \<unlhd> hp s''"
by(cases s,cases s'')(auto dest:red_hext_incr)
with hext show ?case by-(rule hext_trans)
qed
lemma steps_hext_incr: "P,E \<turnstile> ⟨es,s⟩ [->]* ⟨es',s'⟩ ==> hp s \<unlhd> hp s'"
proof(induct rule:converse_rtrancl_induct2)
case refl thus ?case by(rule hext_refl)
next
case (step es s es'' s'')
have Reds:"((es, s), es'', s'') ∈ Reds P E"
and hext:"hp s'' \<unlhd> hp s'" by fact+
from Reds have "P,E \<turnstile> ⟨es,s⟩ [->] ⟨es'',s''⟩" by simp
hence "hp s \<unlhd> hp s''"
by(cases s,cases s'',auto dest:reds_hext_incr)
with hext show ?case by-(rule hext_trans)
qed
lemma eval_hext: "P,E \<turnstile> ⟨e,(h,l)⟩ => ⟨e',(h',l')⟩ ==> h \<unlhd> h'"
and evals_hext: "P,E \<turnstile> ⟨es,(h,l)⟩ [=>] ⟨es',(h',l')⟩ ==> h \<unlhd> h'"
proof (induct rule:eval_evals_inducts)
case New thus ?case
by(fastsimp intro!: hext_new intro:someI simp:new_Addr_def
split:split_if_asm simp del:fun_upd_apply)
next
case FAss thus ?case
by(auto simp:sym[THEN hext_upd_obj] simp del:fun_upd_apply
elim!: hext_trans)
qed (auto elim!: hext_trans)
section {* @{text"\<unlhd>"} and conformance *}
lemma conf_hext: "h \<unlhd> h' ==> P,h \<turnstile> v :≤ T ==> P,h' \<turnstile> v :≤ T"
by(cases T)(induct v,auto dest: hext_objD split:split_if_asm)+
lemma confs_hext: "P,h \<turnstile> vs [:≤] Ts ==> h \<unlhd> h' ==> P,h' \<turnstile> vs [:≤] Ts"
by (erule list_all2_mono, erule conf_hext, assumption)
lemma fconf_hext: "[| P,h \<turnstile> fs (:≤) E; h \<unlhd> h' |] ==> P,h' \<turnstile> fs (:≤) E"
apply (unfold fconf_def)
apply (fast elim: conf_hext)
done
lemmas fconf_upd_obj = fconf_hext [OF _ hext_upd_obj]
lemmas fconf_new = fconf_hext [OF _ hext_new]
lemma oconf_hext: "P,h \<turnstile> obj \<surd> ==> h \<unlhd> h' ==> P,h' \<turnstile> obj \<surd>"
apply (auto simp:oconf_def)
apply (erule allE)
apply (erule_tac x="Cs" in allE)
apply (erule_tac x="fs'" in allE)
apply (fastsimp elim:fconf_hext)
done
lemmas oconf_new = oconf_hext [OF _ hext_new]
lemmas oconf_upd_obj = oconf_hext [OF _ hext_upd_obj]
lemma hconf_new: "[| P \<turnstile> h \<surd>; h a = None; P,h \<turnstile> obj \<surd> |] ==> P \<turnstile> h(a\<mapsto>obj) \<surd>"
by (unfold hconf_def) (auto intro: oconf_new preallocated_new)
lemma "[|P \<turnstile> h \<surd>; h' = h(a \<mapsto> (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P|]
==> P \<turnstile> h' \<surd>"
apply (simp add:hconf_def oconf_def)
apply auto
apply (rule_tac x="init_class_fieldmap P (last Cs)" in exI)
apply (rule init_obj.intros)
apply assumption
apply (erule init_obj.cases)
apply clarsimp
apply (erule init_obj.cases)
apply clarsimp
apply (erule_tac x="a" in allE)
apply clarsimp
apply (erule init_obj.cases)
apply simp
apply (erule_tac x="a" in allE)
apply clarsimp
apply (erule init_obj.cases)
apply clarsimp
apply (drule Subobj_last_isClass)
apply simp
apply (auto simp:is_class_def)
apply (rule fconf_init_fields)
apply auto
apply (erule_tac x="aa" in allE)
apply (erule_tac x="aaa" in allE)
apply (erule_tac x="b" in allE)
apply clarsimp
apply (rotate_tac -1)
apply (erule_tac x="Cs" in allE)
apply (erule_tac x="fs'" in allE)
apply clarsimp thm fconf_new
apply (erule fconf_new)
apply simp
apply (rule preallocated_new)
apply simp_all
done
lemma hconf_upd_obj:
"[| P \<turnstile> h\<surd>; h a = Some(C,S); P,h \<turnstile> (C,S')\<surd> |] ==> P \<turnstile> h(a\<mapsto>(C,S'))\<surd>"
by (unfold hconf_def) (auto intro: oconf_upd_obj preallocated_upd_obj)
lemma lconf_hext: "[| P,h \<turnstile> l (:≤)w E; h \<unlhd> h' |] ==> P,h' \<turnstile> l (:≤)w E"
apply (unfold lconf_def)
apply (fast elim: conf_hext)
done
section {* @{text"\<unlhd>"} in the runtime type system *}
lemma hext_typeof_mono: "[| h \<unlhd> h'; P \<turnstile> typeofh v = Some T |] ==> P \<turnstile> typeofh' v = Some T"
apply(cases v)
apply simp
apply simp
apply simp
apply simp
apply(fastsimp simp:hext_def)
done
lemma WTrt_hext_mono: "P,E,h \<turnstile> e : T ==> (!!h'. h \<unlhd> h' ==> P,E,h' \<turnstile> e : T)"
and WTrts_hext_mono: "P,E,h \<turnstile> es [:] Ts ==> (!!h'. h \<unlhd> h' ==> P,E,h' \<turnstile> es [:] Ts)"
apply(induct rule: WTrt_inducts)
apply(simp add: WTrtNew)
apply(fastsimp intro: WTrtDynCast)
apply(fastsimp intro: WTrtStaticCast)
apply(fastsimp simp: WTrtVal dest:hext_typeof_mono)
apply(simp add: WTrtVar)
apply(fastsimp simp add: WTrtBinOp)
apply(fastsimp simp add: WTrtLAss)
apply(fastsimp simp: WTrtFAcc del:WTrt_WTrts.intros WTrt_elim_cases)
apply(simp add: WTrtFAccNT)
apply(fastsimp simp: WTrtFAss del:WTrt_WTrts.intros WTrt_elim_cases)
apply(fastsimp simp: WTrtFAssNT del:WTrt_WTrts.intros WTrt_elim_cases)
apply(fastsimp simp: WTrtCall del:WTrt_WTrts.intros WTrt_elim_cases)
apply(fastsimp simp: WTrtStaticCall del:WTrt_WTrts.intros WTrt_elim_cases)
apply(fastsimp simp: WTrtCallNT del:WTrt_WTrts.intros WTrt_elim_cases)
apply(fastsimp)
apply(fastsimp simp add: WTrtSeq)
apply(fastsimp simp add: WTrtCond)
apply(fastsimp simp add: WTrtWhile)
apply(fastsimp simp add: WTrtThrow)
apply(simp add: WTrtNil)
apply(simp add: WTrtCons)
done
end