src/HOL/NanoJava/State.thy

added NanoJava

(*  Title:      HOL/NanoJava/State.thy
    ID:         $Id$
    Author:     David von Oheimb
    Copyright   2001 Technische Universitaet Muenchen
*)

header "Program State"

theory State = TypeRel:

constdefs

  body :: "cname => mname => stmt"
 "body C m \<equiv> bdy (the (method C m))"

text {* locations, i.e.\ abstract references to objects *}
typedecl loc 
arities  loc :: "term"

datatype val
  = Null        (* null reference *)
  | Addr loc    (* address, i.e. location of object *)

types	fields
	= "(vnam \<leadsto> val)"

        obj = "cname \<times> fields"

translations

  "fields" \<leftharpoondown> (type)"vnam \<Rightarrow> val option"
  "obj"    \<leftharpoondown> (type)"cname \<times> fields"

constdefs

  init_vars:: "('a \<leadsto> 'b) => ('a \<leadsto> val)"
 "init_vars m == option_map (\<lambda>T. Null) o m"
  
text {* private *}
types	heap   = "loc   \<leadsto> obj"
        locals = "vname \<leadsto> val"	

text {* private *}
record  state
	= heap   :: heap
          locals :: locals

translations

  "heap"   \<leftharpoondown> (type)"loc   => obj option"
  "locals" \<leftharpoondown> (type)"vname => val option"
  "state" \<leftharpoondown> (type)"(|heap :: heap, locals :: locals|)"

constdefs

  init_locs     :: "cname => mname => state => state"
 "init_locs C m s \<equiv> s (| locals:=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.*}
constdefs
  set_locs  :: "state => state => state"
 "set_locs s s' \<equiv> s' (| locals := locals s |)"

  get_local     :: "state => vname => val" ("_<_>" [99,0] 99)
 "get_local s x  \<equiv> the (locals s x)"

(* local function: *)
  get_obj       :: "state => loc => obj"
 "get_obj s a \<equiv> the (heap s a)"

  obj_class     :: "state => loc => cname"
 "obj_class s a \<equiv> fst (get_obj s a)"

  get_field     :: "state => loc => vnam => val"
 "get_field s a f \<equiv> the (snd (get_obj s a) f)"

constdefs

(* local function: *)
  hupd       :: "loc \<Rightarrow> obj \<Rightarrow> state \<Rightarrow> state"   ("hupd'(_|->_')" [10,10] 1000)
 "hupd a obj s \<equiv> s (| heap   := ((heap   s)(a\<mapsto>obj))|)"

  lupd       :: "vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" ("lupd'(_|->_')" [10,10] 1000)
 "lupd x v s   \<equiv> s (| locals := ((locals s)(x\<mapsto>v  ))|)"

syntax (xsymbols)
  hupd       :: "loc \<Rightarrow> obj \<Rightarrow> state \<Rightarrow> state"   ("hupd'(_\<mapsto>_')" [10,10] 1000)
  lupd       :: "vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" ("lupd'(_\<mapsto>_')" [10,10] 1000)

constdefs

  new_obj    :: "loc \<Rightarrow> cname \<Rightarrow> state \<Rightarrow> state"
 "new_obj a C   \<equiv> hupd(a\<mapsto>(C,init_vars (field C)))"

  upd_obj    :: "loc \<Rightarrow> vnam \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state"
 "upd_obj a f v s \<equiv> let (C,fs) = the (heap s a) in hupd(a\<mapsto>(C,fs(f\<mapsto>v))) s"

  new_Addr	:: "state => val"
 "new_Addr s == SOME v. (\<exists>a. v = Addr a \<and> (heap s) a = None) | v = Null"

lemma new_AddrD: 
"new_Addr s = v \<Longrightarrow> (\<exists>a. v = Addr a \<and> 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