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'"
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]



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
    by(fastforce 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 ⊢ ⟨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
    by(fastforce intro!: hext_new intro:someI simp:new_Addr_def
                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 (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 ⊢ 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(simp add: WTrtNew)
apply(fastforce intro: WTrtDynCast)
apply(fastforce intro: WTrtStaticCast)
apply(fastforce simp: WTrtVal dest:hext_typeof_mono)
apply(simp add: WTrtVar)
apply(fastforce simp add: WTrtBinOp)
apply(fastforce simp add: WTrtLAss)
apply(fastforce simp: WTrtFAcc del:WTrt_WTrts.intros WTrt_elim_cases)
apply(simp add: WTrtFAccNT)
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)
apply(fastforce simp add: WTrtSeq)
apply(fastforce simp add: WTrtCond)
apply(fastforce simp add: WTrtWhile)
apply(fastforce simp add: WTrtThrow)
apply(simp add: WTrtNil)
apply(simp add: WTrtCons)
done




end