Theory Objects

(*  Title:       CoreC++
    Author:      Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at>

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

section ‹Objects and the Heap›

theory Objects imports SubObj begin


  subo = "(path × (vname  val))"     ― ‹subobjects realized on the heap›
  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)))) )"

  init_obj :: "prog  cname  (path × (vname  val))  bool"
  for P :: prog and C :: cname
  "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)


type_synonym heap  = "addr  obj"

  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)