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