50 "locals" \<leftharpoondown> (type)"vname => val option" |
50 "locals" \<leftharpoondown> (type)"vname => val option" |
51 "state" \<leftharpoondown> (type)"(|heap :: heap, locals :: locals|)" |
51 "state" \<leftharpoondown> (type)"(|heap :: heap, locals :: locals|)" |
52 |
52 |
53 constdefs |
53 constdefs |
54 |
54 |
55 reset_locs :: "state => state" |
55 del_locs :: "state => state" |
56 "reset_locs s \<equiv> s (| locals := empty |)" |
56 "del_locs s \<equiv> s (| locals := empty |)" |
57 |
57 |
58 init_locs :: "cname => mname => state => state" |
58 init_locs :: "cname => mname => state => state" |
59 "init_locs C m s \<equiv> s (| locals := locals s ++ |
59 "init_locs C m s \<equiv> s (| locals := locals s ++ |
60 init_vars (map_of (lcl (the (method C m)))) |)" |
60 init_vars (map_of (lcl (the (method C m)))) |)" |
61 |
61 |
120 lemma get_field_set_locs [simp]: |
120 lemma get_field_set_locs [simp]: |
121 "get_field (set_locs l s) a f = get_field s a f" |
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) |
122 by (simp add: lupd_def get_field_def set_locs_def get_obj_def) |
123 |
123 |
124 lemma get_field_set_locs [simp]: |
124 lemma get_field_set_locs [simp]: |
125 "get_field (reset_locs s) a f = get_field s a f" |
125 "get_field (del_locs s) a f = get_field s a f" |
126 by (simp add: lupd_def get_field_def reset_locs_def get_obj_def) |
126 by (simp add: lupd_def get_field_def del_locs_def get_obj_def) |
127 |
127 |
128 lemma new_obj_get_local [simp]: "new_obj a C s <x> = s<x>" |
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) |
129 by (simp add: new_obj_def hupd_def get_local_def) |
130 |
130 |
131 lemma heap_lupd [simp]: "heap (lupd(x\<mapsto>y) s) = heap s" |
131 lemma heap_lupd [simp]: "heap (lupd(x\<mapsto>y) s) = heap s" |
139 by (simp add: hupd_def) |
139 by (simp add: hupd_def) |
140 |
140 |
141 lemma hupd_hupd [simp]: "hupd(a\<mapsto>obj) (hupd(a\<mapsto>obj') s) = hupd(a\<mapsto>obj) s" |
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) |
142 by (simp add: hupd_def) |
143 |
143 |
144 lemma heap_reset_locs [simp]: "heap (reset_locs s) = heap s" |
144 lemma heap_del_locs [simp]: "heap (del_locs s) = heap s" |
145 by (simp add: reset_locs_def) |
145 by (simp add: del_locs_def) |
146 |
146 |
147 lemma heap_set_locs [simp]: "heap (set_locs l s) = heap s" |
147 lemma heap_set_locs [simp]: "heap (set_locs l s) = heap s" |
148 by (simp add: set_locs_def) |
148 by (simp add: set_locs_def) |
149 |
149 |
150 lemma hupd_lupd [simp]: |
150 lemma hupd_lupd [simp]: |
151 "hupd(a\<mapsto>obj) (lupd(x\<mapsto>y) s) = lupd(x\<mapsto>y) (hupd(a\<mapsto>obj) s)" |
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) |
152 by (simp add: hupd_def lupd_def) |
153 |
153 |
154 lemma hupd_reset_locs [simp]: |
154 lemma hupd_del_locs [simp]: |
155 "hupd(a\<mapsto>obj) (reset_locs s) = reset_locs (hupd(a\<mapsto>obj) s)" |
155 "hupd(a\<mapsto>obj) (del_locs s) = del_locs (hupd(a\<mapsto>obj) s)" |
156 by (simp add: hupd_def reset_locs_def) |
156 by (simp add: hupd_def del_locs_def) |
157 |
157 |
158 lemma new_obj_lupd [simp]: |
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)" |
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) |
160 by (simp add: new_obj_def) |
161 |
161 |
162 lemma new_obj_reset_locs [simp]: |
162 lemma new_obj_del_locs [simp]: |
163 "new_obj a C (reset_locs s) = reset_locs (new_obj a C s)" |
163 "new_obj a C (del_locs s) = del_locs (new_obj a C s)" |
164 by (simp add: new_obj_def) |
164 by (simp add: new_obj_def) |
165 |
165 |
166 lemma upd_obj_lupd [simp]: |
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)" |
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) |
168 by (simp add: upd_obj_def Let_def split_beta) |
169 |
169 |
170 lemma upd_obj_reset_locs [simp]: |
170 lemma upd_obj_del_locs [simp]: |
171 "upd_obj a f v (reset_locs s) = reset_locs (upd_obj a f v s)" |
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) |
172 by (simp add: upd_obj_def Let_def split_beta) |
173 |
173 |
174 lemma get_field_hupd_same [simp]: |
174 lemma get_field_hupd_same [simp]: |
175 "get_field (hupd(a\<mapsto>(C, fs)) s) a = the \<circ> fs" |
175 "get_field (hupd(a\<mapsto>(C, fs)) s) a = the \<circ> fs" |
176 apply (rule ext) |
176 apply (rule ext) |