Theory Objects
section ‹Objects and the Heap›
theory Objects imports TypeRel Value begin
subsection‹Objects›
type_synonym
fields = "vname × cname ⇀ val"
type_synonym
obj = "cname × fields"
definition obj_ty :: "obj ⇒ ty"
where
"obj_ty obj ≡ Class (fst obj)"
definition init_fields :: "((vname × cname) × ty) list ⇒ fields"
where
"init_fields ≡ map_of ∘ map (λ(F,T). (F,default_val T))"
definition blank :: "'m prog ⇒ cname ⇒ obj"
where
"blank P C ≡ (C,init_fields (fields P C))"
lemma [simp]: "obj_ty (C,fs) = 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(LEAST a. h a = None) else None"
definition cast_ok :: "'m prog ⇒ cname ⇒ heap ⇒ val ⇒ bool"
where
"cast_ok P C h v ≡ v = Null ∨ P ⊢ cname_of h (the_Addr v) ≼⇧* C"
definition hext :: "heap ⇒ heap ⇒ bool" ("_ ⊴ _" [51,51] 50)
where
"h ⊴ h' ≡ ∀a C fs. h a = Some(C,fs) ⟶ (∃fs'. h' a = Some(C,fs'))"
primrec typeof_h :: "heap ⇒ val ⇒ ty option" ("typeof⇘_⇙")
where
"typeof⇘h⇙ Unit = Some Void"
| "typeof⇘h⇙ Null = Some NT"
| "typeof⇘h⇙ (Bool b) = Some Boolean"
| "typeof⇘h⇙ (Intg i) = Some Integer"
| "typeof⇘h⇙ (Addr a) = (case h a of None ⇒ None | Some(C,fs) ⇒ Some(Class C))"
lemma new_Addr_SomeD:
"new_Addr h = Some a ⟹ h a = None"
by(fastforce simp add:new_Addr_def split:if_splits intro:LeastI)
lemma [simp]: "(typeof⇘h⇙ v = Some Boolean) = (∃b. v = Bool b)"
by(induct v) auto
lemma [simp]: "(typeof⇘h⇙ v = Some Integer) = (∃i. v = Intg i)"
by(cases v) auto
lemma [simp]: "(typeof⇘h⇙ v = Some NT) = (v = Null)"
by(cases v) auto
lemma [simp]: "(typeof⇘h⇙ v = Some(Class C)) = (∃a fs. v = Addr a ∧ h a = Some(C,fs))"
by(cases v) auto
lemma [simp]: "h a = Some(C,fs) ⟹ typeof⇘(h(a↦(C,fs')))⇙ v = typeof⇘h⇙ v"
by(induct v) (auto simp:fun_upd_apply)
text‹For literal values the first parameter of @{term typeof} can be
set to @{term Map.empty} because they do not contain addresses:›
abbreviation
typeof :: "val ⇒ ty option" where
"typeof v == typeof_h Map.empty v"
lemma typeof_lit_typeof:
"typeof v = Some T ⟹ typeof⇘h⇙ v = Some T"
by(cases v) auto
lemma typeof_lit_is_type:
"typeof v = Some T ⟹ is_type P T"
by (induct v) (auto simp:is_type_def)
subsection ‹Heap extension ‹⊴››
lemma hextI: "∀a C fs. h a = Some(C,fs) ⟶ (∃fs'. h' a = Some(C,fs')) ⟹ h ⊴ h'"
by(auto simp: hext_def)
lemma hext_objD: "⟦ h ⊴ h'; h a = Some(C,fs) ⟧ ⟹ ∃fs'. h' a = Some(C,fs')"
by(auto simp: hext_def)
lemma hext_refl [iff]: "h ⊴ h"
by (rule hextI) fast
lemma hext_new [simp]: "h a = None ⟹ h ⊴ h(a↦x)"
by (rule hextI) (auto simp:fun_upd_apply)
lemma hext_trans: "⟦ h ⊴ h'; h' ⊴ h'' ⟧ ⟹ h ⊴ h''"
by (rule hextI) (fast dest: hext_objD)
lemma hext_upd_obj: "h a = Some (C,fs) ⟹ h ⊴ h(a↦(C,fs'))"
by (rule hextI) (auto simp:fun_upd_apply)
lemma hext_typeof_mono: "⟦ h ⊴ h'; typeof⇘h⇙ v = Some T ⟧ ⟹ typeof⇘h'⇙ v = Some T"
proof(cases v)
case Addr assume "h ⊴ h'" and "typeof⇘h⇙ v = ⌊T⌋"
then show ?thesis using Addr by(fastforce simp:hext_def)
qed simp_all
text ‹Code generator setup for @{term "new_Addr"}›
definition gen_new_Addr :: "heap ⇒ addr ⇒ addr option"
where "gen_new_Addr h n ≡ if ∃a. a ≥ n ∧ h a = None then Some(LEAST a. a ≥ n ∧ h a = None) else None"
lemma new_Addr_code_code [code]:
"new_Addr h = gen_new_Addr h 0"
by(simp add: new_Addr_def gen_new_Addr_def split del: if_split cong: if_cong)
lemma gen_new_Addr_code [code]:
"gen_new_Addr h n = (if h n = None then Some n else gen_new_Addr h (Suc n))"
apply(simp add: gen_new_Addr_def)
apply(rule impI)
apply(rule conjI)
apply safe[1]
apply(fastforce intro: Least_equality)
apply(rule arg_cong[where f=Least])
apply(rule ext)
apply(case_tac "n = ac")
apply simp
apply(auto)[1]
apply clarify
apply(subgoal_tac "a = n")
apply simp
apply(rule Least_equality)
apply auto[2]
apply(rule ccontr)
apply(erule_tac x="a" in allE)
apply simp
done
end