# Theory HeapExtension

```(*  Title:       CoreC++
Author:      Daniel Wasserrab
Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>

Based on extracts from the Jinja theories:
Common/Objects.thy by David von Oheimb
Common/Conform.thy by David von Oheimb and Tobias Nipkow
Common/Exceptions.thy by Gerwin Klein and Martin Strecker
J/BigStep.thy by Tobias Nipkow
J/SmallStep.thy by Tobias Nipkow
J/WellTypeRT.thy by Tobias Nipkow
*)

section ‹Heap Extension›

theory HeapExtension
imports Progress
begin

subsection ‹The Heap Extension›

definition hext :: "heap ⇒ heap ⇒ bool" ("_ ⊴ _" [51,51] 50) where
"h ⊴ 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 ⊴ h'"

apply (unfold hext_def)
apply auto
done

lemma hext_objD: "⟦ h ⊴ h'; h a = Some(C,S) ⟧ ⟹ ∃S'. h' a = Some(C,S')"

apply (unfold hext_def)
apply (force)
done

lemma hext_refl [iff]: "h ⊴ h"

apply (rule hextI)
apply (fast)
done

lemma hext_new [simp]: "h a = None ⟹ h ⊴ h(a↦x)"

apply (rule hextI)
apply (auto simp:fun_upd_apply)
done

lemma hext_trans: "⟦ h ⊴ h'; h' ⊴ h'' ⟧ ⟹ h ⊴ h''"

apply (rule hextI)
apply (fast dest: hext_objD)
done

lemma hext_upd_obj: "h a = Some (C,S) ⟹ h ⊴ h(a↦(C,S'))"

apply (rule hextI)
apply (auto simp:fun_upd_apply)
done

subsection ‹‹⊴› and preallocated›

lemma preallocated_hext:
"⟦ preallocated h; h ⊴ h' ⟧ ⟹ preallocated h'"

lemmas preallocated_upd_obj = preallocated_hext [OF _ hext_upd_obj]
lemmas preallocated_new  = preallocated_hext [OF _ hext_new]

subsection ‹‹⊴› in Small- and BigStep›

lemma red_hext_incr: "P,E ⊢ ⟨e,(h,l)⟩ → ⟨e',(h',l')⟩  ⟹ h ⊴ h'"
and reds_hext_incr: "P,E ⊢ ⟨es,(h,l)⟩ [→] ⟨es',(h',l')⟩  ⟹ h ⊴ h'"

proof(induct rule:red_reds_inducts)
case RedNew thus ?case
next
case RedFAss thus ?case by(simp add:hext_def split:if_splits)
qed simp_all

lemma step_hext_incr: "P,E ⊢ ⟨e,s⟩ →* ⟨e',s'⟩  ⟹ hp s ⊴ 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'' ⊴ hp s'" by fact+
from Red have "P,E ⊢ ⟨e,s⟩ → ⟨e'',s''⟩" by simp
hence "hp s ⊴ 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 ⊢ ⟨es,s⟩ [→]* ⟨es',s'⟩  ⟹ hp s ⊴ 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'' ⊴ hp s'" by fact+
from Reds have "P,E ⊢ ⟨es,s⟩ [→] ⟨es'',s''⟩" by simp
hence "hp s ⊴ 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 ⊢ ⟨e,(h,l)⟩ ⇒ ⟨e',(h',l')⟩ ⟹ h ⊴ h'"
and evals_hext:  "P,E ⊢ ⟨es,(h,l)⟩ [⇒] ⟨es',(h',l')⟩ ⟹ h ⊴ h'"

proof (induct rule:eval_evals_inducts)
case New thus ?case
split:if_split_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)

subsection ‹‹⊴› and conformance›

lemma conf_hext: "h ⊴ h' ⟹ P,h ⊢ v :≤ T ⟹ P,h' ⊢ v :≤ T"
by(cases T)(induct v,auto dest: hext_objD split:if_split_asm)+

lemma confs_hext: "P,h ⊢ vs [:≤] Ts ⟹ h ⊴ h' ⟹ P,h' ⊢ vs [:≤] Ts"
by (erule list_all2_mono, erule conf_hext, assumption)

lemma fconf_hext: "⟦ P,h ⊢ fs (:≤) E; h ⊴ h' ⟧ ⟹ P,h' ⊢ 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 ⊢ obj √ ⟹ h ⊴ h' ⟹ P,h' ⊢ obj √"

apply (auto simp:oconf_def)
apply (erule allE)
apply (erule_tac x="Cs" in allE)
apply (erule_tac x="fs'" in allE)
apply (fastforce 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 ⊢ h √; h a = None; P,h ⊢ obj √ ⟧ ⟹ P ⊢ h(a↦obj) √"
by (unfold hconf_def) (auto intro: oconf_new preallocated_new)

lemma "⟦P ⊢ h √; h' = h(a ↦ (C, Collect (init_obj P C))); h a = None; wf_prog wf_md P⟧
⟹ P ⊢ h' √"
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 ⊢ h√; h a = Some(C,S); P,h ⊢ (C,S')√ ⟧ ⟹ P ⊢ h(a↦(C,S'))√"
by (unfold hconf_def) (auto intro: oconf_upd_obj preallocated_upd_obj)

lemma lconf_hext: "⟦ P,h ⊢ l (:≤)⇩w E; h ⊴ h' ⟧ ⟹ P,h' ⊢ l (:≤)⇩w E"

apply (unfold lconf_def)
apply  (fast elim: conf_hext)
done

subsection ‹‹⊴› in the runtime type system›

lemma hext_typeof_mono: "⟦ h ⊴ h'; P ⊢ typeof⇘h⇙ v = Some T ⟧ ⟹ P ⊢ typeof⇘h'⇙ v = Some T"

apply(cases v)
apply simp
apply simp
apply simp
apply simp
apply(fastforce simp:hext_def)
done

lemma WTrt_hext_mono: "P,E,h ⊢ e : T ⟹ (⋀h'. h ⊴ h' ⟹ P,E,h' ⊢ e : T)"
and WTrts_hext_mono: "P,E,h ⊢ es [:] Ts ⟹ (⋀h'. h ⊴ h' ⟹ P,E,h' ⊢ es [:] Ts)"

apply(induct rule: WTrt_inducts)
apply(fastforce intro: WTrtDynCast)
apply(fastforce intro: WTrtStaticCast)
apply(fastforce simp: WTrtVal dest:hext_typeof_mono)
apply(fastforce simp: WTrtFAcc del:WTrt_WTrts.intros WTrt_elim_cases)
apply(fastforce simp: WTrtFAss del:WTrt_WTrts.intros WTrt_elim_cases)
apply(fastforce simp: WTrtFAssNT del:WTrt_WTrts.intros WTrt_elim_cases)
apply(fastforce simp: WTrtCall del:WTrt_WTrts.intros WTrt_elim_cases)
apply(fastforce simp: WTrtStaticCall del:WTrt_WTrts.intros WTrt_elim_cases)
apply(fastforce simp: WTrtCallNT del:WTrt_WTrts.intros WTrt_elim_cases)
apply(fastforce)
done

end
```