equal
deleted
inserted
replaced
229 |
229 |
230 text {* FIXME: Does there exist a "canonical" array axiomatisation in |
230 text {* FIXME: Does there exist a "canonical" array axiomatisation in |
231 the literature? *} |
231 the literature? *} |
232 |
232 |
233 lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x" |
233 lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x" |
234 by (simp add: get_array_def set_array_def) |
234 by (simp add: get_array_def set_array_def o_def) |
235 |
235 |
236 lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h" |
236 lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h" |
237 by (simp add: noteq_arrs_def get_array_def set_array_def) |
237 by (simp add: noteq_arrs_def get_array_def set_array_def) |
238 |
238 |
239 lemma set_array_same [simp]: |
239 lemma set_array_same [simp]: |