equal
deleted
inserted
replaced
214 lemma update_change [code]: |
214 lemma update_change [code]: |
215 "r := e = change (\<lambda>_. e) r \<guillemotright> return ()" |
215 "r := e = change (\<lambda>_. e) r \<guillemotright> return ()" |
216 by (rule Heap_eqI) (simp add: change_def lookup_chain) |
216 by (rule Heap_eqI) (simp add: change_def lookup_chain) |
217 |
217 |
218 |
218 |
219 text {* Non-interaction between imperative array and imperative references *} |
219 text {* Non-interaction between imperative arrays and imperative references *} |
220 |
220 |
221 lemma array_get_set [simp]: |
221 lemma array_get_set [simp]: |
222 "Array.get (set r v h) = Array.get h" |
222 "Array.get (set r v h) = Array.get h" |
223 by (simp add: Array.get_def set_def fun_eq_iff) |
223 by (simp add: Array.get_def set_def fun_eq_iff) |
224 |
224 |
261 hide_const (open) present get set alloc noteq lookup update change |
261 hide_const (open) present get set alloc noteq lookup update change |
262 |
262 |
263 |
263 |
264 subsection {* Code generator setup *} |
264 subsection {* Code generator setup *} |
265 |
265 |
266 text {* Intermediate operation avoids invariance problem in @{text Scala} (similiar to value restriction) *} |
266 text {* Intermediate operation avoids invariance problem in @{text Scala} (similar to value restriction) *} |
267 |
267 |
268 definition ref' where |
268 definition ref' where |
269 [code del]: "ref' = ref" |
269 [code del]: "ref' = ref" |
270 |
270 |
271 lemma [code]: |
271 lemma [code]: |