src/HOL/NanoJava/State.thy
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 16417 9bc16273c2d4
child 30235 58d147683393
permissions -rw-r--r--
avoid rebinding of existing facts;
     1 (*  Title:      HOL/NanoJava/State.thy
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4     Copyright   2001 Technische Universitaet Muenchen
     5 *)
     6 
     7 header "Program State"
     8 
     9 theory State imports TypeRel begin
    10 
    11 constdefs
    12 
    13   body :: "cname \<times> mname => stmt"
    14  "body \<equiv> \<lambda>(C,m). bdy (the (method C m))"
    15 
    16 text {* Locations, i.e.\ abstract references to objects *}
    17 typedecl loc 
    18 
    19 datatype val
    20   = Null        --{* null reference *}
    21   | Addr loc    --{* address, i.e. location of object *}
    22 
    23 types	fields
    24 	= "(fname \<rightharpoonup> val)"
    25 
    26         obj = "cname \<times> fields"
    27 
    28 translations
    29 
    30   "fields" \<leftharpoondown> (type)"fname => val option"
    31   "obj"    \<leftharpoondown> (type)"cname \<times> fields"
    32 
    33 constdefs
    34 
    35   init_vars:: "('a \<rightharpoonup> 'b) => ('a \<rightharpoonup> val)"
    36  "init_vars m == option_map (\<lambda>T. Null) o m"
    37   
    38 text {* private: *}
    39 types	heap   = "loc   \<rightharpoonup> obj"
    40         locals = "vname \<rightharpoonup> val"	
    41 
    42 text {* private: *}
    43 record  state
    44 	= heap   :: heap
    45           locals :: locals
    46 
    47 translations
    48 
    49   "heap"   \<leftharpoondown> (type)"loc   => obj option"
    50   "locals" \<leftharpoondown> (type)"vname => val option"
    51   "state" \<leftharpoondown> (type)"(|heap :: heap, locals :: locals|)"
    52 
    53 constdefs
    54 
    55   del_locs     :: "state => state"
    56  "del_locs s \<equiv> s (| locals := empty |)"
    57 
    58   init_locs     :: "cname => mname => state => state"
    59  "init_locs C m s \<equiv> s (| locals := locals s ++ 
    60                          init_vars (map_of (lcl (the (method C m)))) |)"
    61 
    62 text {* The first parameter of @{term set_locs} is of type @{typ state} 
    63         rather than @{typ locals} in order to keep @{typ locals} private.*}
    64 constdefs
    65   set_locs  :: "state => state => state"
    66  "set_locs s s' \<equiv> s' (| locals := locals s |)"
    67 
    68   get_local     :: "state => vname => val" ("_<_>" [99,0] 99)
    69  "get_local s x  \<equiv> the (locals s x)"
    70 
    71 --{* local function: *}
    72   get_obj       :: "state => loc => obj"
    73  "get_obj s a \<equiv> the (heap s a)"
    74 
    75   obj_class     :: "state => loc => cname"
    76  "obj_class s a \<equiv> fst (get_obj s a)"
    77 
    78   get_field     :: "state => loc => fname => val"
    79  "get_field s a f \<equiv> the (snd (get_obj s a) f)"
    80 
    81 --{* local function: *}
    82   hupd       :: "loc => obj => state => state"   ("hupd'(_|->_')" [10,10] 1000)
    83  "hupd a obj s \<equiv> s (| heap   := ((heap   s)(a\<mapsto>obj))|)"
    84 
    85   lupd       :: "vname => val => state => state" ("lupd'(_|->_')" [10,10] 1000)
    86  "lupd x v s   \<equiv> s (| locals := ((locals s)(x\<mapsto>v  ))|)"
    87 
    88 syntax (xsymbols)
    89   hupd       :: "loc => obj => state => state"   ("hupd'(_\<mapsto>_')" [10,10] 1000)
    90   lupd       :: "vname => val => state => state" ("lupd'(_\<mapsto>_')" [10,10] 1000)
    91 
    92 constdefs
    93 
    94   new_obj    :: "loc => cname => state => state"
    95  "new_obj a C   \<equiv> hupd(a\<mapsto>(C,init_vars (field C)))"
    96 
    97   upd_obj    :: "loc => fname => val => state => state"
    98  "upd_obj a f v s \<equiv> let (C,fs) = the (heap s a) in hupd(a\<mapsto>(C,fs(f\<mapsto>v))) s"
    99 
   100   new_Addr	:: "state => val"
   101  "new_Addr s == SOME v. (\<exists>a. v = Addr a \<and> (heap s) a = None) | v = Null"
   102 
   103 
   104 subsection "Properties not used in the meta theory"
   105 
   106 lemma locals_upd_id [simp]: "s\<lparr>locals := locals s\<rparr> = s" 
   107 by simp
   108 
   109 lemma lupd_get_local_same [simp]: "lupd(x\<mapsto>v) s<x> = v"
   110 by (simp add: lupd_def get_local_def)
   111 
   112 lemma lupd_get_local_other [simp]: "x \<noteq> y \<Longrightarrow> lupd(x\<mapsto>v) s<y> = s<y>"
   113 apply (drule not_sym)
   114 by (simp add: lupd_def get_local_def)
   115 
   116 lemma get_field_lupd [simp]:
   117   "get_field (lupd(x\<mapsto>y) s) a f = get_field s a f"
   118 by (simp add: lupd_def get_field_def get_obj_def)
   119 
   120 lemma get_field_set_locs [simp]:
   121   "get_field (set_locs l s) a f = get_field s a f"
   122 by (simp add: lupd_def get_field_def set_locs_def get_obj_def)
   123 
   124 lemma get_field_del_locs [simp]:
   125   "get_field (del_locs s) a f = get_field s a f"
   126 by (simp add: lupd_def get_field_def del_locs_def get_obj_def)
   127 
   128 lemma new_obj_get_local [simp]: "new_obj a C s <x> = s<x>"
   129 by (simp add: new_obj_def hupd_def get_local_def)
   130 
   131 lemma heap_lupd [simp]: "heap (lupd(x\<mapsto>y) s) = heap s"
   132 by (simp add: lupd_def)
   133 
   134 lemma heap_hupd_same [simp]: "heap (hupd(a\<mapsto>obj) s) a = Some obj"
   135 by (simp add: hupd_def)
   136 
   137 lemma heap_hupd_other [simp]: "aa \<noteq> a  \<Longrightarrow> heap (hupd(aa\<mapsto>obj) s) a = heap s a"
   138 apply (drule not_sym)
   139 by (simp add: hupd_def)
   140 
   141 lemma hupd_hupd [simp]: "hupd(a\<mapsto>obj) (hupd(a\<mapsto>obj') s) = hupd(a\<mapsto>obj) s"
   142 by (simp add: hupd_def)
   143 
   144 lemma heap_del_locs [simp]: "heap (del_locs s) = heap s"
   145 by (simp add: del_locs_def)
   146 
   147 lemma heap_set_locs [simp]: "heap (set_locs l s) = heap s"
   148 by (simp add: set_locs_def)
   149 
   150 lemma hupd_lupd [simp]: 
   151   "hupd(a\<mapsto>obj) (lupd(x\<mapsto>y) s) = lupd(x\<mapsto>y) (hupd(a\<mapsto>obj) s)"
   152 by (simp add: hupd_def lupd_def)
   153 
   154 lemma hupd_del_locs [simp]: 
   155   "hupd(a\<mapsto>obj) (del_locs s) = del_locs (hupd(a\<mapsto>obj) s)"
   156 by (simp add: hupd_def del_locs_def)
   157 
   158 lemma new_obj_lupd [simp]: 
   159   "new_obj a C (lupd(x\<mapsto>y) s) = lupd(x\<mapsto>y) (new_obj a C s)"
   160 by (simp add: new_obj_def)
   161 
   162 lemma new_obj_del_locs [simp]: 
   163   "new_obj a C (del_locs s) = del_locs (new_obj a C s)"
   164 by (simp add: new_obj_def)
   165 
   166 lemma upd_obj_lupd [simp]: 
   167   "upd_obj a f v (lupd(x\<mapsto>y) s) = lupd(x\<mapsto>y) (upd_obj a f v s)"
   168 by (simp add: upd_obj_def Let_def split_beta)
   169 
   170 lemma upd_obj_del_locs [simp]: 
   171   "upd_obj a f v (del_locs s) = del_locs (upd_obj a f v s)"
   172 by (simp add: upd_obj_def Let_def split_beta)
   173 
   174 lemma get_field_hupd_same [simp]:
   175  "get_field (hupd(a\<mapsto>(C, fs)) s) a = the \<circ> fs"
   176 apply (rule ext)
   177 by (simp add: get_field_def get_obj_def)
   178 
   179 lemma get_field_hupd_other [simp]:
   180  "aa \<noteq> a  \<Longrightarrow> get_field (hupd(aa\<mapsto>obj) s) a = get_field s a"
   181 apply (rule ext)
   182 by (simp add: get_field_def get_obj_def)
   183 
   184 lemma new_AddrD: 
   185 "new_Addr s = v \<Longrightarrow> (\<exists>a. v = Addr a \<and> heap s a = None) | v = Null"
   186 apply (unfold new_Addr_def)
   187 apply (erule subst)
   188 apply (rule someI)
   189 apply (rule disjI2)
   190 apply (rule HOL.refl)
   191 done
   192 
   193 end