src/HOL/Library/Heap.thy
changeset 26300 03def556e26e
parent 26170 66e6b967ccf1
child 26586 a2255b130fd9
equal deleted inserted replaced
26299:2f387f5c0f52 26300:03def556e26e
   412   by (simp add: get_ref_def set_array_def upd_def)
   412   by (simp add: get_ref_def set_array_def upd_def)
   413 
   413 
   414 lemma new_ref_upd: "fst (ref v (upd a i v' h)) = fst (ref v h)"
   414 lemma new_ref_upd: "fst (ref v (upd a i v' h)) = fst (ref v h)"
   415   by (simp add: set_array_def get_array_def Let_def ref_new_set upd_def ref_def  new_ref_def)
   415   by (simp add: set_array_def get_array_def Let_def ref_new_set upd_def ref_def  new_ref_def)
   416 
   416 
   417 (*not actually true ???
   417 text {*not actually true ???*}
   418 lemma upd_set_ref_swap: "upd a i v (set_ref r v' h) = set_ref r v' (upd a i v h)"
   418 lemma upd_set_ref_swap: "upd a i v (set_ref r v' h) = set_ref r v' (upd a i v h)"
   419 apply (case_tac a)
   419 apply (case_tac a)
   420 apply (simp add: Let_def upd_def)
   420 apply (simp add: Let_def upd_def)
   421 apply auto
   421 apply auto
   422 done*)
   422 oops
   423 
   423 
   424 lemma length_new_ref[simp]: 
   424 lemma length_new_ref[simp]: 
   425   "length a (snd (ref v h)) = length a h"
   425   "length a (snd (ref v h)) = length a h"
   426   by (simp add: get_array_def set_ref_def length_def new_ref_def ref_def Let_def)
   426   by (simp add: get_array_def set_ref_def length_def new_ref_def ref_def Let_def)
   427 
   427 
   428 lemma get_array_new_ref [simp]: 
   428 lemma get_array_new_ref [simp]: 
   429   "get_array a (snd (ref v h)) = get_array a h"
   429   "get_array a (snd (ref v h)) = get_array a h"
   430   by (simp add: new_ref_def ref_def set_ref_def get_array_def Let_def)
   430   by (simp add: new_ref_def ref_def set_ref_def get_array_def Let_def)
   431 
   431 
   432 lemma get_array_new_ref [simp]:
       
   433   "get_array a (snd (ref v h)) ! i = get_array a h ! i"
       
   434   by (simp add: get_array_def new_ref_def ref_def set_ref_def Let_def)
       
   435 
       
   436 lemma ref_present_upd [simp]: 
   432 lemma ref_present_upd [simp]: 
   437   "ref_present r (upd a i v h) = ref_present r h"
   433   "ref_present r (upd a i v h) = ref_present r h"
   438   by (simp add: upd_def ref_present_def set_array_def get_array_def)
   434   by (simp add: upd_def ref_present_def set_array_def get_array_def)
   439 
   435 
   440 lemma array_present_set_ref [simp]:
   436 lemma array_present_set_ref [simp]: