header {* \isaheader{Objects and the Heap} *}
theory Objects imports Value begin
subsection{* Objects and Arrays *}
types
fields = "vname × cname \<rightharpoonup> val" -- "field name, defining class, value"
datatype heapobj
= Obj cname fields -- "class instance with class name and fields"
| Arr ty "val list" -- "element type and list of each cell's content"
consts
obj_ty :: "heapobj => ty"
primrec
"obj_ty (Obj c f) = Class c"
"obj_ty (Arr t e) = Array t"
fun is_Arr :: "heapobj => bool" where
"is_Arr (Obj C fs) = False"
| "is_Arr (Arr T el) = True"
lemma is_Arr_conv:
"is_Arr arrobj = (∃T el. arrobj = Arr T el)"
by(cases arrobj, auto)
lemma is_ArrE:
"[| is_Arr arrobj; !!T el. arrobj = Arr T el ==> thesis |] ==> thesis"
"[| ¬ is_Arr arrobj; !!C fs. arrobj = Obj C fs ==> thesis |] ==> thesis"
by(cases arrobj, auto)+
definition init_fields :: "((vname × cname) × ty) list => fields"
where "init_fields ≡ map_of o map (λ(F,T). (F,default_val T))"
definition
-- "a new, blank object with default values in all fields:"
blank :: "'m prog => cname => heapobj"
where
"blank P C ≡ Obj C (init_fields (fields P C))"
lemma blank_obj: "∃c f. blank P C = Obj c f"
by(simp add: blank_def)
lemma obj_ty_blank [iff]: "obj_ty (blank P C) = Class C"
by (simp add: blank_def)
subsection{* Heap *}
types heap = "addr \<rightharpoonup> heapobj"
translations
"heap" <= (type) "nat => heapobj option"
fun the_obj :: "heapobj => cname × fields" where
"the_obj (Obj C fs) = (C, fs)"
fun the_arr :: "heapobj => ty × val list" where
"the_arr (Arr T el) = (T, el)"
abbreviation
cname_of :: "heap => addr => cname" where
"cname_of hp a == fst (the_obj (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"
definition hext :: "heap => heap => bool" ("_ \<unlhd> _" [51,51] 50)
where
"h \<unlhd> h' ≡ (∀a C fs. h a = ⌊Obj C fs⌋ --> (∃fs'. h' a = ⌊Obj C fs'⌋))
∧ (∀a T e. h a = ⌊Arr T e⌋ --> (∃e'. h' a = ⌊Arr T e'⌋ ∧ length e' = length e))"
consts
typeof_h :: "heap => val => ty option" ("typeof_")
primrec
"typeofh Unit = Some Void"
"typeofh Null = Some NT"
"typeofh (Bool b) = Some Boolean"
"typeofh (Intg i) = Some Integer"
"typeofh (Addr a) = (case h a of None => None
| Some ho => (case ho of Obj C fs => ⌊Class C⌋
| Arr t e => ⌊Array t⌋))"
lemma new_Addr_SomeD:
"new_Addr h = Some a ==> h a = None"
by(fastsimp simp add:new_Addr_def split:if_splits intro:someI)
lemma [simp]: "(typeofh v = Some Boolean) = (∃b. v = Bool b)"
by(cases v, auto split:heapobj.split)
lemma [simp]: "(typeofh v = Some Integer) = (∃i. v = Intg i)"
by(cases v, auto split: heapobj.split)
lemma [simp]: "(typeofh v = Some NT) = (v = Null)"
by(cases v, auto split:heapobj.split)
lemma [simp]: "(typeofh v = Some(Class C)) = (∃a fs. v = Addr a ∧ h a = Some(Obj C fs))"
by(cases v, auto split:heapobj.split)
lemma [simp]: "(typeofh v = Some(Array T)) = (∃a e. v = Addr a ∧ h a = Some(Arr T e))"
by(cases v, auto split:heapobj.split)
lemma [simp]: "h a = Some(Obj C fs) ==> typeof(h(a\<mapsto>(Obj C fs'))) v = typeofh v"
by(induct v) (auto simp:fun_upd_apply)
lemma [simp]: "h a = Some(Arr t e) ==> typeof(h(a\<mapsto>(Arr t e'))) v = typeofh v"
by(induct v) (auto simp:fun_upd_apply)
text{* For literal values the first parameter of @{term typeof} can be
set to @{term empty} because they do not contain addresses: *}
consts
typeof :: "val => ty option"
translations
"typeof v" == "typeof_h (CONST empty) v"
lemma typeof_lit_typeof:
"typeof v = Some T ==> typeofh v = Some T"
by(cases v) auto
lemma typeof_lit_is_type:
"typeof v = Some T ==> is_type P T"
by (induct v) (auto)
lemma typeof_NoneD [simp,dest]:
"typeof v = Some x ==> ¬is_Addr v"
by (cases v) auto
definition cast_ok :: "'m prog => ty => heap => val => bool" where
"cast_ok P T h v ≡ ∃U. typeofh v = ⌊U⌋ ∧ P \<turnstile> U ≤ T"
section {* Heap extension @{text"\<unlhd>"} *}
lemma hextI:
"[|∀a C fs. h a = Some(Obj C fs) --> (∃fs'. h' a = Some(Obj C fs'));
∀a T e. h a = Some(Arr T e) --> (∃e'. h' a = Some(Arr T e') ∧ length e' = length e) |]
==> h \<unlhd> h'"
apply (unfold hext_def)
apply auto
done
lemma hext_objD: "[| h \<unlhd> h'; h a = Some(Obj C fs) |] ==> ∃fs'. h' a = Some(Obj C fs')"
apply (unfold hext_def)
apply (force)
done
lemma hext_arrD: "[| h \<unlhd> h'; h a = Some(Arr T e) |] ==> ∃e'. h' a = Some(Arr T e') ∧ length e' = length e"
apply(unfold hext_def)
apply blast
done
lemma hext_objarrD: "[| h \<unlhd> h'; h a = Some v |] ==> ∃w. h' a = Some w"
apply(case_tac v)
by(auto dest: hext_objD hext_arrD)
lemma hext_refl [iff]: "h \<unlhd> h"
apply (rule hextI)
apply (fast)
apply (fast)
done
lemma hext_new [simp]: "h a = None ==> h \<unlhd> h(a\<mapsto>x)"
apply (rule hextI)
apply (auto simp:fun_upd_apply)
done
lemma hext_trans: "[| h \<unlhd> h'; h' \<unlhd> h'' |] ==> h \<unlhd> h''"
apply (rule hextI)
apply (fast dest: hext_objD)
apply (fastsimp dest: hext_arrD)
done
lemma hext_upd_obj: "h a = Some (Obj C fs) ==> h \<unlhd> h(a\<mapsto>(Obj C fs'))"
apply (rule hextI)
apply (auto simp:fun_upd_apply)
done
lemma hext_upd_arr: "[| h a = Some (Arr T e); length e = length e' |] ==> h \<unlhd> h(a\<mapsto>(Arr T e'))"
apply(rule hextI)
apply (auto simp:fun_upd_apply)
done
lemma hext_typeof_mono: "[| h \<unlhd> h'; typeofh v = Some T |] ==> typeofh' v = Some T"
proof (cases v)
case(Addr a)
assume hexth: "h \<unlhd> h'" and thT: "typeofh v = ⌊T⌋" and vIi: "v = Addr a"
from hexth have hextobj: "∀a C fs. h a = ⌊Obj C fs⌋ --> (∃fs'. h' a = ⌊Obj C fs'⌋)" by (simp add: hext_def)
from hexth have hextarr: "∀a T s e. h a = ⌊Arr T e⌋ --> (∃e'. h' a = ⌊Arr T e'⌋ ∧ length e' = length e)"
by (simp add: hext_def)
show "typeofh' v = Some T"
proof (cases "h a")
case None
with vIi have "typeofh v = None" by (simp split:heapobj.split)
with thT have False by simp
thus ?thesis by simp
next
case (Some ho)
show "typeofh' v = Some T"
proof (cases ho)
case (Obj C fs)
with hextobj Some have exfsh':"∃fs'. h' a = ⌊Obj C fs'⌋" by simp
then obtain fs' where "h' a = ⌊Obj C fs'⌋" by clarify
with vIi Some Obj thT show ?thesis by simp
next
case (Arr T e)
with hextarr Some have "∃e'. h' a = ⌊Arr T e'⌋ ∧ length e' = length e" by simp
then obtain e' where "h' a = ⌊Arr T e'⌋" "length e' = length e" by clarify
with vIi Some Arr thT show ?thesis by simp
qed
qed
qed(simp_all)
lemma map_typeof_hext_mono:
"[| map typeofh vs = map Some Ts; hext h h' |] ==> map typeofh' vs = map Some Ts"
apply(induct vs arbitrary: Ts)
apply(auto simp add: Cons_eq_map_conv intro: hext_typeof_mono)
done
lemma hext_None: "[| hext h h'; h' a = None |] ==> h a = None"
by(cases "h a", auto dest: hext_objarrD)
lemma hext_new_Addr:
assumes "hext h h'"
and "new_Addr h' = ⌊a'⌋"
obtains a where "new_Addr h = ⌊a⌋"
using prems
apply(auto dest!: hext_None simp add: new_Addr_def split: split_if_asm)
apply(fastsimp)
done
lemma hext_typeof_eq:
"[| hext h h'; h a = ⌊v⌋ |] ==> typeofh (Addr a) = typeofh' (Addr a)"
apply(cases v, auto dest: hext_objD hext_arrD)
apply(auto simp: hext_def)
apply(erule_tac x="a" in allE, fastsimp)
apply(erule_tac x="a" in allE, fastsimp)
done
lemma type_of_hext_type_of:
"[| typeofh w = ⌊T⌋; hext h h' |] ==> typeofh' w = ⌊T⌋"
apply(cases w, auto)
apply(case_tac a, auto dest: hext_objarrD)
apply(case_tac a, auto)
apply(case_tac aa, auto dest: hext_objD hext_arrD)+
done
end