src/HOL/NanoJava/State.thy

 constdefs
 
   body :: "cname \<times> mname => stmt"
  "body \<equiv> \<lambda>(C,m). bdy (the (method C m))"
 
-text {* locations, i.e.\ abstract references to objects *}
+text {* Locations, i.e.\ abstract references to objects *}
 typedecl loc 
 
 datatype val
   = Null        --{* null reference *}
   | Addr loc    --{* address, i.e. location of object *}

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

 
   reset_locs     :: "state => state"
  "reset_locs s \<equiv> s (| locals := empty |)"
 
   init_locs     :: "cname => mname => state => state"
- "init_locs C m s \<equiv> s (| locals:=init_vars (map_of (lcl (the (method C m)))) |)"
+ "init_locs C m s \<equiv> s (| locals := locals s ++ 
+                         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"

  "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"
 
+
+subsection "Properties not used in the meta theory"
+
+lemma locals_upd_id [simp]: "s\<lparr>locals := locals s\<rparr> = s" 
+by simp
+
+lemma lupd_get_local_same [simp]: "lupd(x\<mapsto>v) s<x> = v"
+by (simp add: lupd_def get_local_def)
+
+lemma lupd_get_local_other [simp]: "x \<noteq> y \<Longrightarrow> lupd(x\<mapsto>v) s<y> = s<y>"
+apply (drule not_sym)
+by (simp add: lupd_def get_local_def)
+
+lemma get_field_lupd [simp]:
+  "get_field (lupd(x\<mapsto>y) s) a f = get_field s a f"
+by (simp add: lupd_def get_field_def get_obj_def)
+
+lemma get_field_set_locs [simp]:
+  "get_field (set_locs l s) a f = get_field s a f"
+by (simp add: lupd_def get_field_def set_locs_def get_obj_def)
+
+lemma get_field_set_locs [simp]:
+  "get_field (reset_locs s) a f = get_field s a f"
+by (simp add: lupd_def get_field_def reset_locs_def get_obj_def)
+
+lemma new_obj_get_local [simp]: "new_obj a C s <x> = s<x>"
+by (simp add: new_obj_def hupd_def get_local_def)
+
+lemma heap_lupd [simp]: "heap (lupd(x\<mapsto>y) s) = heap s"
+by (simp add: lupd_def)
+
+lemma heap_hupd_same [simp]: "heap (hupd(a\<mapsto>obj) s) a = Some obj"
+by (simp add: hupd_def)
+
+lemma heap_hupd_other [simp]: "aa \<noteq> a  \<Longrightarrow> heap (hupd(aa\<mapsto>obj) s) a = heap s a"
+apply (drule not_sym)
+by (simp add: hupd_def)
+
+lemma hupd_hupd [simp]: "hupd(a\<mapsto>obj) (hupd(a\<mapsto>obj') s) = hupd(a\<mapsto>obj) s"
+by (simp add: hupd_def)
+
+lemma heap_reset_locs [simp]: "heap (reset_locs s) = heap s"
+by (simp add: reset_locs_def)
+
+lemma heap_set_locs [simp]: "heap (set_locs l s) = heap s"
+by (simp add: set_locs_def)
+
+lemma hupd_lupd [simp]: 
+  "hupd(a\<mapsto>obj) (lupd(x\<mapsto>y) s) = lupd(x\<mapsto>y) (hupd(a\<mapsto>obj) s)"
+by (simp add: hupd_def lupd_def)
+
+lemma hupd_reset_locs [simp]: 
+  "hupd(a\<mapsto>obj) (reset_locs s) = reset_locs (hupd(a\<mapsto>obj) s)"
+by (simp add: hupd_def reset_locs_def)
+
+lemma new_obj_lupd [simp]: 
+  "new_obj a C (lupd(x\<mapsto>y) s) = lupd(x\<mapsto>y) (new_obj a C s)"
+by (simp add: new_obj_def)
+
+lemma new_obj_reset_locs [simp]: 
+  "new_obj a C (reset_locs s) = reset_locs (new_obj a C s)"
+by (simp add: new_obj_def)
+
+lemma upd_obj_lupd [simp]: 
+  "upd_obj a f v (lupd(x\<mapsto>y) s) = lupd(x\<mapsto>y) (upd_obj a f v s)"
+by (simp add: upd_obj_def Let_def split_beta)
+
+lemma upd_obj_reset_locs [simp]: 
+  "upd_obj a f v (reset_locs s) = reset_locs (upd_obj a f v s)"
+by (simp add: upd_obj_def Let_def split_beta)
+
+lemma get_field_hupd_same [simp]:
+ "get_field (hupd(a\<mapsto>(C, fs)) s) a = the \<circ> fs"
+apply (rule ext)
+by (simp add: get_field_def get_obj_def)
+
+lemma get_field_hupd_other [simp]:
+ "aa \<noteq> a  \<Longrightarrow> get_field (hupd(aa\<mapsto>obj) s) a = get_field s a"
+apply (rule ext)
+by (simp add: get_field_def get_obj_def)
+
 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)