Theory Objects

(*  Title:      HOL/MicroJava/J/State.thy
    ID:         $Id: Objects.thy,v 1.4 2006-11-17 01:28:44 makarius Exp $
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen
*)

header {* \isaheader{Objects and the Heap} *}

theory Objects imports TypeRel Value begin

subsection{* Objects *}

types 
  fields = "vname × cname \<rightharpoonup> val"  -- "field name, defining class, value"
  obj = "cname × fields"    -- "class instance with class name and fields"

constdefs
  obj_ty  :: "obj => ty"
  "obj_ty obj  ≡  Class (fst obj)"

  init_fields :: "((vname × cname) × ty) list => fields"
  "init_fields  ≡  map_of o map (λ(F,T). (F,default_val T))"
  
  -- "a new, blank object with default values in all fields:"
  blank :: "'m prog => cname => obj"
  "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 *}

types heap  = "addr \<rightharpoonup> obj"

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

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

  cast_ok :: "'m prog => cname => heap => val => bool"
  "cast_ok P C h v  ≡  v = Null ∨ P \<turnstile> cname_of h (the_Addr v) \<preceq>* C"

  hext :: "heap => heap => bool" ("_ \<unlhd> _" [51,51] 50)
  "h \<unlhd> h'  ≡  ∀a C fs. h a = Some(C,fs) --> (∃fs'. h' a = Some(C,fs'))"

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(C,fs) => Some(Class C))"

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(induct v) auto(*>*)

lemma [simp]: "(typeofh v = Some Integer) = (∃i. v = Intg i)"
(*<*)by(cases v) auto(*>*)

lemma [simp]: "(typeofh v = Some NT) = (v = Null)"
 (*<*)by(cases v) auto(*>*)

lemma [simp]: "(typeofh 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\<mapsto>(C,fs'))) 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: *}

abbreviation
  typeof :: "val => ty option" where
  "typeof v == typeof_h 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 simp:is_type_def)(*>*)


section {* Heap extension @{text"\<unlhd>"} *}

lemma hextI: "∀a C fs. h a = Some(C,fs) --> (∃fs'. h' a = Some(C,fs')) ==> h \<unlhd> h'"
(*<*)
apply (unfold hext_def)
apply auto
done
(*>*)

lemma hext_objD: "[| h \<unlhd> h'; h a = Some(C,fs) |] ==> ∃fs'. h' a = Some(C,fs')"
(*<*)
apply (unfold hext_def)
apply (force)
done
(*>*)

lemma hext_refl [iff]: "h \<unlhd> h"
(*<*)
apply (rule hextI)
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)
done
(*>*)

lemma hext_upd_obj: "h a = Some (C,fs) ==> h \<unlhd> h(a\<mapsto>(C,fs'))"
(*<*)
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"
(*<*)
apply(cases v)
    apply simp
   apply simp
  apply simp
 apply simp
apply(fastsimp simp:hext_def)
done
(*>*)


end