src/HOL/NanoJava/State.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/NanoJava/State.thy	Sat Jun 16 20:06:42 2001 +0200
@@ -0,0 +1,111 @@
+(*  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