src/HOL/Imperative_HOL/Array.thy
changeset 37796 08bd610b2583
parent 37787 30dc3abf4a58
child 37797 96551d6b1414
     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 11:38:04 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Tue Jul 13 12:01:34 2010 +0200
     1.3 @@ -35,9 +35,8 @@
     1.4    length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where
     1.5    "length a h = List.length (get_array a h)"
     1.6    
     1.7 -definition (*FIXME update*)
     1.8 -  change :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
     1.9 -  "change a i x h = set_array a ((get_array a h)[i:=x]) h"
    1.10 +definition update :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
    1.11 +  "update a i x h = set_array a ((get_array a h)[i:=x]) h"
    1.12  
    1.13  definition (*FIXME noteq*)
    1.14    noteq_arrs :: "'a\<Colon>heap array \<Rightarrow> 'b\<Colon>heap array \<Rightarrow> bool" (infix "=!!=" 70) where
    1.15 @@ -64,15 +63,15 @@
    1.16  
    1.17  definition upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap" where
    1.18    [code del]: "upd i x a = Heap_Monad.guard (\<lambda>h. i < length a h)
    1.19 -    (\<lambda>h. (a, change a i x h))"
    1.20 +    (\<lambda>h. (a, update a i x h))"
    1.21  
    1.22  definition map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" where
    1.23    [code del]: "map_entry i f a = Heap_Monad.guard (\<lambda>h. i < length a h)
    1.24 -    (\<lambda>h. (a, change a i (f (get_array a h ! i)) h))"
    1.25 +    (\<lambda>h. (a, update a i (f (get_array a h ! i)) h))"
    1.26  
    1.27  definition swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap" where
    1.28    [code del]: "swap i x a = Heap_Monad.guard (\<lambda>h. i < length a h)
    1.29 -    (\<lambda>h. (get_array a h ! i, change a i x h))"
    1.30 +    (\<lambda>h. (get_array a h ! i, update a i x h))"
    1.31  
    1.32  definition freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" where
    1.33    [code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get_array a h)"
    1.34 @@ -109,27 +108,27 @@
    1.35    "r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)"
    1.36    by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def)
    1.37  
    1.38 -lemma get_array_change_eq [simp]:
    1.39 -  "get_array a (change a i v h) = (get_array a h) [i := v]"
    1.40 -  by (simp add: change_def)
    1.41 +lemma get_array_update_eq [simp]:
    1.42 +  "get_array a (update a i v h) = (get_array a h) [i := v]"
    1.43 +  by (simp add: update_def)
    1.44  
    1.45 -lemma nth_change_array_neq_array [simp]:
    1.46 -  "a =!!= b \<Longrightarrow> get_array a (change b j v h) ! i = get_array a h ! i"
    1.47 -  by (simp add: change_def noteq_arrs_def)
    1.48 +lemma nth_update_array_neq_array [simp]:
    1.49 +  "a =!!= b \<Longrightarrow> get_array a (update b j v h) ! i = get_array a h ! i"
    1.50 +  by (simp add: update_def noteq_arrs_def)
    1.51  
    1.52 -lemma get_arry_array_change_elem_neqIndex [simp]:
    1.53 -  "i \<noteq> j \<Longrightarrow> get_array a (change a j v h) ! i = get_array a h ! i"
    1.54 +lemma get_arry_array_update_elem_neqIndex [simp]:
    1.55 +  "i \<noteq> j \<Longrightarrow> get_array a (update a j v h) ! i = get_array a h ! i"
    1.56    by simp
    1.57  
    1.58 -lemma length_change [simp]: 
    1.59 -  "length a (change b i v h) = length a h"
    1.60 -  by (simp add: change_def length_def set_array_def get_array_def)
    1.61 +lemma length_update [simp]: 
    1.62 +  "length a (update b i v h) = length a h"
    1.63 +  by (simp add: update_def length_def set_array_def get_array_def)
    1.64  
    1.65 -lemma change_swap_neqArray:
    1.66 +lemma update_swap_neqArray:
    1.67    "a =!!= a' \<Longrightarrow> 
    1.68 -  change a i v (change a' i' v' h) 
    1.69 -  = change a' i' v' (change a i v h)"
    1.70 -apply (unfold change_def)
    1.71 +  update a i v (update a' i' v' h) 
    1.72 +  = update a' i' v' (update a i v h)"
    1.73 +apply (unfold update_def)
    1.74  apply simp
    1.75  apply (subst array_set_set_swap, assumption)
    1.76  apply (subst array_get_set_neq)
    1.77 @@ -137,9 +136,9 @@
    1.78  apply (simp)
    1.79  done
    1.80  
    1.81 -lemma change_swap_neqIndex:
    1.82 -  "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> change a i v (change a i' v' h) = change a i' v' (change a i v h)"
    1.83 -  by (auto simp add: change_def array_set_set_swap list_update_swap)
    1.84 +lemma update_swap_neqIndex:
    1.85 +  "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> update a i v (update a i' v' h) = update a i' v' (update a i v h)"
    1.86 +  by (auto simp add: update_def array_set_set_swap list_update_swap)
    1.87  
    1.88  lemma get_array_init_array_list:
    1.89    "get_array (fst (array ls h)) (snd (array ls' h)) = ls'"
    1.90 @@ -151,9 +150,9 @@
    1.91         = snd (array new_ls h)"
    1.92    by (simp add: Let_def split_def array_def)
    1.93  
    1.94 -lemma array_present_change [simp]: 
    1.95 -  "array_present a (change b i v h) = array_present a h"
    1.96 -  by (simp add: change_def array_present_def set_array_def get_array_def)
    1.97 +lemma array_present_update [simp]: 
    1.98 +  "array_present a (update b i v h) = array_present a h"
    1.99 +  by (simp add: update_def array_present_def set_array_def get_array_def)
   1.100  
   1.101  lemma array_present_array [simp]:
   1.102    "array_present (fst (array xs h)) (snd (array xs h))"
   1.103 @@ -264,7 +263,7 @@
   1.104  
   1.105  lemma execute_upd [execute_simps]:
   1.106    "i < length a h \<Longrightarrow>
   1.107 -    execute (upd i x a) h = Some (a, change a i x h)"
   1.108 +    execute (upd i x a) h = Some (a, update a i x h)"
   1.109    "i \<ge> length a h \<Longrightarrow> execute (upd i x a) h = None"
   1.110    by (simp_all add: upd_def execute_simps)
   1.111  
   1.112 @@ -273,20 +272,20 @@
   1.113    by (auto intro: success_intros simp add: upd_def)
   1.114  
   1.115  lemma crel_updI [crel_intros]:
   1.116 -  assumes "i < length a h" "h' = change a i v h"
   1.117 +  assumes "i < length a h" "h' = update a i v h"
   1.118    shows "crel (upd i v a) h h' a"
   1.119    by (rule crelI) (insert assms, simp add: execute_simps)
   1.120  
   1.121  lemma crel_updE [crel_elims]:
   1.122    assumes "crel (upd i v a) h h' r"
   1.123 -  obtains "r = a" "h' = change a i v h" "i < length a h"
   1.124 +  obtains "r = a" "h' = update a i v h" "i < length a h"
   1.125    using assms by (rule crelE)
   1.126      (erule successE, cases "i < length a h", simp_all add: execute_simps)
   1.127  
   1.128  lemma execute_map_entry [execute_simps]:
   1.129    "i < length a h \<Longrightarrow>
   1.130     execute (map_entry i f a) h =
   1.131 -      Some (a, change a i (f (get_array a h ! i)) h)"
   1.132 +      Some (a, update a i (f (get_array a h ! i)) h)"
   1.133    "i \<ge> length a h \<Longrightarrow> execute (map_entry i f a) h = None"
   1.134    by (simp_all add: map_entry_def execute_simps)
   1.135  
   1.136 @@ -295,20 +294,20 @@
   1.137    by (auto intro: success_intros simp add: map_entry_def)
   1.138  
   1.139  lemma crel_map_entryI [crel_intros]:
   1.140 -  assumes "i < length a h" "h' = change a i (f (get_array a h ! i)) h" "r = a"
   1.141 +  assumes "i < length a h" "h' = update a i (f (get_array a h ! i)) h" "r = a"
   1.142    shows "crel (map_entry i f a) h h' r"
   1.143    by (rule crelI) (insert assms, simp add: execute_simps)
   1.144  
   1.145  lemma crel_map_entryE [crel_elims]:
   1.146    assumes "crel (map_entry i f a) h h' r"
   1.147 -  obtains "r = a" "h' = change a i (f (get_array a h ! i)) h" "i < length a h"
   1.148 +  obtains "r = a" "h' = update a i (f (get_array a h ! i)) h" "i < length a h"
   1.149    using assms by (rule crelE)
   1.150      (erule successE, cases "i < length a h", simp_all add: execute_simps)
   1.151  
   1.152  lemma execute_swap [execute_simps]:
   1.153    "i < length a h \<Longrightarrow>
   1.154     execute (swap i x a) h =
   1.155 -      Some (get_array a h ! i, change a i x h)"
   1.156 +      Some (get_array a h ! i, update a i x h)"
   1.157    "i \<ge> length a h \<Longrightarrow> execute (swap i x a) h = None"
   1.158    by (simp_all add: swap_def execute_simps)
   1.159  
   1.160 @@ -317,13 +316,13 @@
   1.161    by (auto intro: success_intros simp add: swap_def)
   1.162  
   1.163  lemma crel_swapI [crel_intros]:
   1.164 -  assumes "i < length a h" "h' = change a i x h" "r = get_array a h ! i"
   1.165 +  assumes "i < length a h" "h' = update a i x h" "r = get_array a h ! i"
   1.166    shows "crel (swap i x a) h h' r"
   1.167    by (rule crelI) (insert assms, simp add: execute_simps)
   1.168  
   1.169  lemma crel_swapE [crel_elims]:
   1.170    assumes "crel (swap i x a) h h' r"
   1.171 -  obtains "r = get_array a h ! i" "h' = change a i x h" "i < length a h"
   1.172 +  obtains "r = get_array a h ! i" "h' = update a i x h" "i < length a h"
   1.173    using assms by (rule crelE)
   1.174      (erule successE, cases "i < length a h", simp_all add: execute_simps)
   1.175  
   1.176 @@ -357,7 +356,7 @@
   1.177    "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)"
   1.178    by (rule Heap_eqI) (simp add: map_nth execute_simps)
   1.179  
   1.180 -hide_const (open) new
   1.181 +hide_const (open) update new of_list make len nth upd map_entry swap freeze
   1.182  
   1.183  
   1.184  subsection {* Code generator setup *}
   1.185 @@ -407,24 +406,24 @@
   1.186    by (simp add: upd'_def upd_return)
   1.187  
   1.188  lemma [code]:
   1.189 -  "map_entry i f a = (do
   1.190 -     x \<leftarrow> nth a i;
   1.191 -     upd i (f x) a
   1.192 +  "Array.map_entry i f a = (do
   1.193 +     x \<leftarrow> Array.nth a i;
   1.194 +     Array.upd i (f x) a
   1.195     done)"
   1.196    by (rule Heap_eqI) (simp add: bind_def guard_def map_entry_def execute_simps)
   1.197  
   1.198  lemma [code]:
   1.199 -  "swap i x a = (do
   1.200 -     y \<leftarrow> nth a i;
   1.201 -     upd i x a;
   1.202 +  "Array.swap i x a = (do
   1.203 +     y \<leftarrow> Array.nth a i;
   1.204 +     Array.upd i x a;
   1.205       return y
   1.206     done)"
   1.207    by (rule Heap_eqI) (simp add: bind_def guard_def swap_def execute_simps)
   1.208  
   1.209  lemma [code]:
   1.210 -  "freeze a = (do
   1.211 -     n \<leftarrow> len a;
   1.212 -     Heap_Monad.fold_map (\<lambda>i. nth a i) [0..<n]
   1.213 +  "Array.freeze a = (do
   1.214 +     n \<leftarrow> Array.len a;
   1.215 +     Heap_Monad.fold_map (\<lambda>i. Array.nth a i) [0..<n]
   1.216     done)"
   1.217  proof (rule Heap_eqI)
   1.218    fix h
   1.219 @@ -441,12 +440,12 @@
   1.220      apply (simp add: length_def map_nth)
   1.221      done
   1.222    then have "execute (do
   1.223 -      n \<leftarrow> len a;
   1.224 +      n \<leftarrow> Array.len a;
   1.225        Heap_Monad.fold_map (Array.nth a) [0..<n]
   1.226      done) h = Some (get_array a h, h)"
   1.227      by (auto intro: execute_bind_eq_SomeI simp add: execute_simps)
   1.228 -  then show "execute (freeze a) h = execute (do
   1.229 -      n \<leftarrow> len a;
   1.230 +  then show "execute (Array.freeze a) h = execute (do
   1.231 +      n \<leftarrow> Array.len a;
   1.232        Heap_Monad.fold_map (Array.nth a) [0..<n]
   1.233      done) h" by (simp add: execute_simps)
   1.234  qed