Theory State
section "Program State"
theory State imports TypeRel begin
definition body :: "cname × mname => stmt" where
"body ≡ λ(C,m). bdy (the (method C m))"
text ‹Locations, i.e.\ abstract references to objects›
typedecl loc
datatype val
= Null
| Addr loc
type_synonym fields
= "(fname ⇀ val)"
type_synonym
obj = "cname × fields"
translations
(type) "fields" ↽ (type) "fname => val option"
(type) "obj" ↽ (type) "cname × fields"
definition init_vars :: "('a ⇀ 'b) => ('a ⇀ val)" where
"init_vars m == map_option (λT. Null) o m"
text ‹private:›
type_synonym heap = "loc ⇀ obj"
type_synonym locals = "vname ⇀ val"
text ‹private:›
record state
= heap :: heap
locals :: locals
translations
(type) "heap" ↽ (type) "loc => obj option"
(type) "locals" ↽ (type) "vname => val option"
(type) "state" ↽ (type) "(|heap :: heap, locals :: locals|)"
definition del_locs :: "state => state" where
"del_locs s ≡ s (| locals := Map.empty |)"
definition init_locs :: "cname => mname => state => state" where
"init_locs C m s ≡ s (| locals := locals s ++
init_vars (map_of (lcl (the (method C m)))) |)"
text ‹The first parameter of \<^term>‹set_locs› is of type \<^typ>‹state›
rather than \<^typ>‹locals› in order to keep \<^typ>‹locals› private.›
definition set_locs :: "state => state => state" where
"set_locs s s' ≡ s' (| locals := locals s |)"
definition get_local :: "state => vname => val" ("_<_>" [99,0] 99) where
"get_local s x ≡ the (locals s x)"
definition get_obj :: "state => loc => obj" where
"get_obj s a ≡ the (heap s a)"
definition obj_class :: "state => loc => cname" where
"obj_class s a ≡ fst (get_obj s a)"
definition get_field :: "state => loc => fname => val" where
"get_field s a f ≡ the (snd (get_obj s a) f)"
definition hupd :: "loc => obj => state => state" ("hupd'(_↦_')" [10,10] 1000) where
"hupd a obj s ≡ s (| heap := ((heap s)(a↦obj))|)"
definition lupd :: "vname => val => state => state" ("lupd'(_↦_')" [10,10] 1000) where
"lupd x v s ≡ s (| locals := ((locals s)(x↦v ))|)"
definition new_obj :: "loc => cname => state => state" where
"new_obj a C ≡ hupd(a↦(C,init_vars (field C)))"
definition upd_obj :: "loc => fname => val => state => state" where
"upd_obj a f v s ≡ let (C,fs) = the (heap s a) in hupd(a↦(C,fs(f↦v))) s"
definition new_Addr :: "state => val" where
"new_Addr s == SOME v. (∃a. v = Addr a ∧ (heap s) a = None) | v = Null"
subsection "Properties not used in the meta theory"
lemma locals_upd_id [simp]: "s⦇locals := locals s⦈ = s"
by simp
lemma lupd_get_local_same [simp]: "lupd(x↦v) s<x> = v"
by (simp add: lupd_def get_local_def)
lemma lupd_get_local_other [simp]: "x ≠ y ⟹ lupd(x↦v) s<y> = s<y>"
apply (drule not_sym)
by (simp add: lupd_def get_local_def)
lemma get_field_lupd [simp]:
"get_field (lupd(x↦y) s) a f = get_field s a f"
by (simp add: lupd_def get_field_def get_obj_def)
lemma get_field_set_locs [simp]:
"get_field (set_locs l s) a f = get_field s a f"
by (simp add: lupd_def get_field_def set_locs_def get_obj_def)
lemma get_field_del_locs [simp]:
"get_field (del_locs s) a f = get_field s a f"
by (simp add: lupd_def get_field_def del_locs_def get_obj_def)
lemma new_obj_get_local [simp]: "new_obj a C s <x> = s<x>"
by (simp add: new_obj_def hupd_def get_local_def)
lemma heap_lupd [simp]: "heap (lupd(x↦y) s) = heap s"
by (simp add: lupd_def)
lemma heap_hupd_same [simp]: "heap (hupd(a↦obj) s) a = Some obj"
by (simp add: hupd_def)
lemma heap_hupd_other [simp]: "aa ≠ a ⟹ heap (hupd(aa↦obj) s) a = heap s a"
apply (drule not_sym)
by (simp add: hupd_def)
lemma hupd_hupd [simp]: "hupd(a↦obj) (hupd(a↦obj') s) = hupd(a↦obj) s"
by (simp add: hupd_def)
lemma heap_del_locs [simp]: "heap (del_locs s) = heap s"
by (simp add: del_locs_def)
lemma heap_set_locs [simp]: "heap (set_locs l s) = heap s"
by (simp add: set_locs_def)
lemma hupd_lupd [simp]:
"hupd(a↦obj) (lupd(x↦y) s) = lupd(x↦y) (hupd(a↦obj) s)"
by (simp add: hupd_def lupd_def)
lemma hupd_del_locs [simp]:
"hupd(a↦obj) (del_locs s) = del_locs (hupd(a↦obj) s)"
by (simp add: hupd_def del_locs_def)
lemma new_obj_lupd [simp]:
"new_obj a C (lupd(x↦y) s) = lupd(x↦y) (new_obj a C s)"
by (simp add: new_obj_def)
lemma new_obj_del_locs [simp]:
"new_obj a C (del_locs s) = del_locs (new_obj a C s)"
by (simp add: new_obj_def)
lemma upd_obj_lupd [simp]:
"upd_obj a f v (lupd(x↦y) s) = lupd(x↦y) (upd_obj a f v s)"
by (simp add: upd_obj_def Let_def split_beta)
lemma upd_obj_del_locs [simp]:
"upd_obj a f v (del_locs s) = del_locs (upd_obj a f v s)"
by (simp add: upd_obj_def Let_def split_beta)
lemma get_field_hupd_same [simp]:
"get_field (hupd(a↦(C, fs)) s) a = the ∘ fs"
apply (rule ext)
by (simp add: get_field_def get_obj_def)
lemma get_field_hupd_other [simp]:
"aa ≠ a ⟹ get_field (hupd(aa↦obj) s) a = get_field s a"
apply (rule ext)
by (simp add: get_field_def get_obj_def)
lemma new_AddrD:
"new_Addr s = v ⟹ (∃a. v = Addr a ∧ heap s a = None) | v = Null"
apply (unfold new_Addr_def)
apply (erule subst)
apply (rule someI)
apply (rule disjI2)
apply (rule HOL.refl)
done
end