src/HOL/Imperative_HOL/Ref.thy
changeset 37805 0f797d586ce5
parent 37804 0145e59c1f6c
child 37806 a7679be14442
     1.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 16:00:56 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 16:12:40 2010 +0200
     1.3 @@ -219,15 +219,11 @@
     1.4  text {* Non-interaction between imperative array and imperative references *}
     1.5  
     1.6  lemma get_array_set [simp]:
     1.7 -  "get_array a (set r v h) = get_array a h"
     1.8 -  by (simp add: get_array_def set_def)
     1.9 -
    1.10 -lemma nth_set [simp]:
    1.11 -  "get_array a (set r v h) ! i = get_array a h ! i"
    1.12 -  by simp
    1.13 +  "get_array (set r v h) = get_array h"
    1.14 +  by (simp add: get_array_def set_def expand_fun_eq)
    1.15  
    1.16  lemma get_update [simp]:
    1.17 -  "get (Array.update a i v h) r  = get h r"
    1.18 +  "get (Array.update a i v h) r = get h r"
    1.19    by (simp add: get_def Array.update_def Array.set_def)
    1.20  
    1.21  lemma alloc_update:
    1.22 @@ -243,8 +239,8 @@
    1.23    by (simp add: Array.length_def get_array_def alloc_def set_def Let_def)
    1.24  
    1.25  lemma get_array_alloc [simp]: 
    1.26 -  "get_array a (snd (alloc v h)) = get_array a h"
    1.27 -  by (simp add: get_array_def alloc_def set_def Let_def)
    1.28 +  "get_array (snd (alloc v h)) = get_array h"
    1.29 +  by (simp add: get_array_def alloc_def set_def Let_def expand_fun_eq)
    1.30  
    1.31  lemma present_update [simp]: 
    1.32    "present (Array.update a i v h) = present h"