Theory Objects

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

   Based on the Jinja theory Common/Objects.thy by Tobias Nipkow 
*)

section ‹Objects and the Heap›

theory Objects imports SubObj begin


subsection‹Objects›

type_synonym
  subo = "(path × (vname ⇀ val))"     ― ‹subobjects realized on the heap›
type_synonym
  obj  = "cname × subo set"            ― ‹mdc and subobject›


definition init_class_fieldmap :: "prog ⇒ cname ⇒ (vname ⇀ val)" where
  "init_class_fieldmap P C ≡ 
     map_of (map (λ(F,T).(F,default_val T)) (fst(snd(the(class P C)))) )"

inductive
  init_obj :: "prog ⇒ cname ⇒ (path × (vname ⇀ val)) ⇒ bool"
  for P :: prog and C :: cname
where
  "Subobjs P C Cs ⟹ init_obj P C (Cs,init_class_fieldmap P (last Cs))"


lemma init_obj_nonempty: "init_obj P C (Cs,fs) ⟹ Cs ≠ []"
by (fastforce elim:init_obj.cases dest:Subobjs_nonempty)

lemma init_obj_no_Ref: 
"⟦init_obj P C (Cs,fs);  fs F = Some(Ref(a',Cs'))⟧ ⟹ False"
by (fastforce elim:init_obj.cases default_val_no_Ref 
                  simp:init_class_fieldmap_def map_of_map)

lemma SubobjsSet_init_objSet:
  "{Cs. Subobjs P C Cs} = {Cs. ∃vmap. init_obj P C (Cs,vmap)}"
by ( fastforce intro:init_obj.intros elim:init_obj.cases)


definition obj_ty :: "obj ⇒ ty" where
  "obj_ty obj  ≡  Class (fst obj)"


 ― ‹a new, blank object with default values in all fields:›
definition blank :: "prog ⇒ cname ⇒ obj" where
  "blank P C  ≡ (C, Collect (init_obj P C))"


lemma [simp]: "obj_ty (C,S) = Class C"
  by (simp add: obj_ty_def)

subsection‹Heap›

type_synonym heap  = "addr ⇀ obj"

abbreviation
  cname_of :: "heap ⇒ addr ⇒ cname" where
  "cname_of hp a == fst (the (hp a))"

definition new_Addr :: "heap ⇒ addr option" where
  "new_Addr h  ≡  if ∃a. h a = None then Some(SOME a. h a = None) else None"

lemma new_Addr_SomeD:
  "new_Addr h = Some a ⟹ h a = None"
 by(fastforce simp add:new_Addr_def split:if_splits intro:someI)


end