hide_const; update replaces change
authorhaftmann
Tue Jul 13 12:01:34 2010 +0200 (2010-07-13 ago)
changeset 3779608bd610b2583
parent 37788 261c61fabc98
child 37797 96551d6b1414
hide_const; update replaces change
src/HOL/Imperative_HOL/Array.thy
src/HOL/Imperative_HOL/Ref.thy
src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy
src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy
src/HOL/Imperative_HOL/ex/SatChecker.thy
src/HOL/Imperative_HOL/ex/Subarray.thy
     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
     2.1 --- a/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 11:38:04 2010 +0200
     2.2 +++ b/src/HOL/Imperative_HOL/Ref.thy	Tue Jul 13 12:01:34 2010 +0200
     2.3 @@ -150,7 +150,7 @@
     2.4  
     2.5  lemma crel_refE [crel_elims]:
     2.6    assumes "crel (ref v) h h' r"
     2.7 -  obtains "Ref.get h' r = v" and "Ref.present h' r" and "\<not> Ref.present h r"
     2.8 +  obtains "get h' r = v" and "present h' r" and "\<not> present h r"
     2.9    using assms by (rule crelE) (simp add: execute_simps)
    2.10  
    2.11  lemma execute_lookup [execute_simps]:
    2.12 @@ -162,13 +162,13 @@
    2.13    by (auto intro: success_intros  simp add: lookup_def)
    2.14  
    2.15  lemma crel_lookupI [crel_intros]:
    2.16 -  assumes "h' = h" "x = Ref.get h r"
    2.17 +  assumes "h' = h" "x = get h r"
    2.18    shows "crel (!r) h h' x"
    2.19    by (rule crelI) (insert assms, simp add: execute_simps)
    2.20  
    2.21  lemma crel_lookupE [crel_elims]:
    2.22    assumes "crel (!r) h h' x"
    2.23 -  obtains "h' = h" "x = Ref.get h r"
    2.24 +  obtains "h' = h" "x = get h r"
    2.25    using assms by (rule crelE) (simp add: execute_simps)
    2.26  
    2.27  lemma execute_update [execute_simps]:
    2.28 @@ -180,13 +180,13 @@
    2.29    by (auto intro: success_intros  simp add: update_def)
    2.30  
    2.31  lemma crel_updateI [crel_intros]:
    2.32 -  assumes "h' = Ref.set r v h"
    2.33 +  assumes "h' = set r v h"
    2.34    shows "crel (r := v) h h' x"
    2.35    by (rule crelI) (insert assms, simp add: execute_simps)
    2.36  
    2.37  lemma crel_updateE [crel_elims]:
    2.38    assumes "crel (r' := v) h h' r"
    2.39 -  obtains "h' = Ref.set r' v h"
    2.40 +  obtains "h' = set r' v h"
    2.41    using assms by (rule crelE) (simp add: execute_simps)
    2.42  
    2.43  lemma execute_change [execute_simps]:
    2.44 @@ -198,13 +198,13 @@
    2.45    by (auto intro!: success_intros crel_intros simp add: change_def)
    2.46  
    2.47  lemma crel_changeI [crel_intros]: 
    2.48 -  assumes "h' = Ref.set r (f (Ref.get h r)) h" "x = f (Ref.get h r)"
    2.49 -  shows "crel (Ref.change f r) h h' x"
    2.50 +  assumes "h' = set r (f (get h r)) h" "x = f (get h r)"
    2.51 +  shows "crel (change f r) h h' x"
    2.52    by (rule crelI) (insert assms, simp add: execute_simps)  
    2.53  
    2.54  lemma crel_changeE [crel_elims]:
    2.55 -  assumes "crel (Ref.change f r') h h' r"
    2.56 -  obtains "h' = Ref.set r' (f (Ref.get h r')) h" "r = f (Ref.get h r')"
    2.57 +  assumes "crel (change f r') h h' r"
    2.58 +  obtains "h' = set r' (f (get h r')) h" "r = f (get h r')"
    2.59    using assms by (rule crelE) (simp add: execute_simps)
    2.60  
    2.61  lemma lookup_chain:
    2.62 @@ -226,17 +226,17 @@
    2.63    "get_array a (set r v h) ! i = get_array a h ! i"
    2.64    by simp
    2.65  
    2.66 -lemma get_change [simp]:
    2.67 -  "get (Array.change a i v h) r  = get h r"
    2.68 -  by (simp add: get_def Array.change_def set_array_def)
    2.69 +lemma get_update [simp]:
    2.70 +  "get (Array.update a i v h) r  = get h r"
    2.71 +  by (simp add: get_def Array.update_def set_array_def)
    2.72  
    2.73 -lemma alloc_change:
    2.74 -  "fst (alloc v (Array.change a i v' h)) = fst (alloc v h)"
    2.75 -  by (simp add: Array.change_def get_array_def set_array_def alloc_def Let_def)
    2.76 +lemma alloc_update:
    2.77 +  "fst (alloc v (Array.update a i v' h)) = fst (alloc v h)"
    2.78 +  by (simp add: Array.update_def get_array_def set_array_def alloc_def Let_def)
    2.79  
    2.80 -lemma change_set_swap:
    2.81 -  "Array.change a i v (set r v' h) = set r v' (Array.change a i v h)"
    2.82 -  by (simp add: Array.change_def get_array_def set_array_def set_def)
    2.83 +lemma update_set_swap:
    2.84 +  "Array.update a i v (set r v' h) = set r v' (Array.update a i v h)"
    2.85 +  by (simp add: Array.update_def get_array_def set_array_def set_def)
    2.86  
    2.87  lemma length_alloc [simp]: 
    2.88    "Array.length a (snd (alloc v h)) = Array.length a h"
    2.89 @@ -246,9 +246,9 @@
    2.90    "get_array a (snd (alloc v h)) = get_array a h"
    2.91    by (simp add: get_array_def alloc_def set_def Let_def)
    2.92  
    2.93 -lemma present_change [simp]: 
    2.94 -  "present (Array.change a i v h) = present h"
    2.95 -  by (simp add: Array.change_def set_array_def expand_fun_eq present_def)
    2.96 +lemma present_update [simp]: 
    2.97 +  "present (Array.update a i v h) = present h"
    2.98 +  by (simp add: Array.update_def set_array_def expand_fun_eq present_def)
    2.99  
   2.100  lemma array_present_set [simp]:
   2.101    "array_present a (set r v h) = array_present a h"
   2.102 @@ -262,7 +262,7 @@
   2.103    "set_array a xs (set r x' h) = set r x' (set_array a xs h)"
   2.104    by (simp add: set_array_def set_def)
   2.105  
   2.106 -hide_const (open) present get set alloc lookup update change
   2.107 +hide_const (open) present get set alloc noteq lookup update change
   2.108  
   2.109  
   2.110  subsection {* Code generator setup *}
     3.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 11:38:04 2010 +0200
     3.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Quicksort.thy	Tue Jul 13 12:01:34 2010 +0200
     3.3 @@ -14,17 +14,17 @@
     3.4  where
     3.5    "swap arr i j = (
     3.6       do
     3.7 -       x \<leftarrow> nth arr i;
     3.8 -       y \<leftarrow> nth arr j;
     3.9 -       upd i y arr;
    3.10 -       upd j x arr;
    3.11 +       x \<leftarrow> Array.nth arr i;
    3.12 +       y \<leftarrow> Array.nth arr j;
    3.13 +       Array.upd i y arr;
    3.14 +       Array.upd j x arr;
    3.15         return ()
    3.16       done)"
    3.17  
    3.18  lemma crel_swapI [crel_intros]:
    3.19    assumes "i < Array.length a h" "j < Array.length a h"
    3.20      "x = get_array a h ! i" "y = get_array a h ! j"
    3.21 -    "h' = Array.change a j x (Array.change a i y h)"
    3.22 +    "h' = Array.update a j x (Array.update a i y h)"
    3.23    shows "crel (swap a i j) h h' r"
    3.24    unfolding swap_def using assms by (auto intro!: crel_intros)
    3.25  
    3.26 @@ -41,7 +41,7 @@
    3.27    "part1 a left right p = (
    3.28       if (right \<le> left) then return right
    3.29       else (do
    3.30 -       v \<leftarrow> nth a left;
    3.31 +       v \<leftarrow> Array.nth a left;
    3.32         (if (v \<le> p) then (part1 a (left + 1) right p)
    3.33                      else (do swap a left right;
    3.34    part1 a left (right - 1) p done))
    3.35 @@ -228,9 +228,9 @@
    3.36  fun partition :: "nat array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat Heap"
    3.37  where
    3.38    "partition a left right = (do
    3.39 -     pivot \<leftarrow> nth a right;
    3.40 +     pivot \<leftarrow> Array.nth a right;
    3.41       middle \<leftarrow> part1 a left (right - 1) pivot;
    3.42 -     v \<leftarrow> nth a middle;
    3.43 +     v \<leftarrow> Array.nth a middle;
    3.44       m \<leftarrow> return (if (v \<le> pivot) then (middle + 1) else middle);
    3.45       swap a m right;
    3.46       return m
    3.47 @@ -294,8 +294,8 @@
    3.48           else middle)"
    3.49      unfolding partition.simps
    3.50      by (elim crel_bindE crel_returnE crel_nthE crel_ifE crel_updE) simp
    3.51 -  from swap have h'_def: "h' = Array.change a r (get_array a h1 ! rs)
    3.52 -    (Array.change a rs (get_array a h1 ! r) h1)"
    3.53 +  from swap have h'_def: "h' = Array.update a r (get_array a h1 ! rs)
    3.54 +    (Array.update a rs (get_array a h1 ! r) h1)"
    3.55      unfolding swap_def
    3.56      by (elim crel_bindE crel_returnE crel_nthE crel_updE) simp
    3.57    from swap have in_bounds: "r < Array.length a h1 \<and> rs < Array.length a h1"
    3.58 @@ -326,7 +326,7 @@
    3.59        with part_partitions[OF part] right_remains True
    3.60        have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
    3.61        with i_props h'_def in_bounds have "get_array a h' ! i \<le> get_array a h' ! rs"
    3.62 -        unfolding Array.change_def Array.length_def by simp
    3.63 +        unfolding Array.update_def Array.length_def by simp
    3.64      }
    3.65      moreover
    3.66      {
    3.67 @@ -352,7 +352,7 @@
    3.68            by fastsimp
    3.69          with i_is True rs_equals right_remains h'_def
    3.70          show ?thesis using in_bounds
    3.71 -          unfolding Array.change_def Array.length_def
    3.72 +          unfolding Array.update_def Array.length_def
    3.73            by auto
    3.74        qed
    3.75      }
    3.76 @@ -368,7 +368,7 @@
    3.77        from part_partitions[OF part] rs_equals right_remains i_is_left
    3.78        have "get_array a h1 ! i \<le> get_array a h' ! rs" by fastsimp
    3.79        with i_props h'_def have "get_array a h' ! i \<le> get_array a h' ! rs"
    3.80 -        unfolding Array.change_def by simp
    3.81 +        unfolding Array.update_def by simp
    3.82      }
    3.83      moreover
    3.84      {
    3.85 @@ -388,7 +388,7 @@
    3.86          assume i_is: "i = r"
    3.87          from i_is False rs_equals right_remains h'_def
    3.88          show ?thesis using in_bounds
    3.89 -          unfolding Array.change_def Array.length_def
    3.90 +          unfolding Array.update_def Array.length_def
    3.91            by auto
    3.92        qed
    3.93      }
    3.94 @@ -646,7 +646,7 @@
    3.95  subsection {* Example *}
    3.96  
    3.97  definition "qsort a = do
    3.98 -    k \<leftarrow> len a;
    3.99 +    k \<leftarrow> Array.len a;
   3.100      quicksort a 0 (k - 1);
   3.101      return a
   3.102    done"
     4.1 --- a/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 11:38:04 2010 +0200
     4.2 +++ b/src/HOL/Imperative_HOL/ex/Imperative_Reverse.thy	Tue Jul 13 12:01:34 2010 +0200
     4.3 @@ -8,14 +8,12 @@
     4.4  imports Imperative_HOL Subarray
     4.5  begin
     4.6  
     4.7 -hide_const (open) swap rev
     4.8 -
     4.9  fun swap :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> unit Heap" where
    4.10    "swap a i j = (do
    4.11 -     x \<leftarrow> nth a i;
    4.12 -     y \<leftarrow> nth a j;
    4.13 -     upd i y a;
    4.14 -     upd j x a;
    4.15 +     x \<leftarrow> Array.nth a i;
    4.16 +     y \<leftarrow> Array.nth a j;
    4.17 +     Array.upd i y a;
    4.18 +     Array.upd j x a;
    4.19       return ()
    4.20     done)"
    4.21  
     5.1 --- a/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Jul 13 11:38:04 2010 +0200
     5.2 +++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy	Tue Jul 13 12:01:34 2010 +0200
     5.3 @@ -127,21 +127,21 @@
     5.4  unfolding array_ran_def Array.length_def by simp
     5.5  
     5.6  lemma array_ran_upd_array_Some:
     5.7 -  assumes "cl \<in> array_ran a (Array.change a i (Some b) h)"
     5.8 +  assumes "cl \<in> array_ran a (Array.update a i (Some b) h)"
     5.9    shows "cl \<in> array_ran a h \<or> cl = b"
    5.10  proof -
    5.11    have "set (get_array a h[i := Some b]) \<subseteq> insert (Some b) (set (get_array a h))" by (rule set_update_subset_insert)
    5.12    with assms show ?thesis 
    5.13 -    unfolding array_ran_def Array.change_def by fastsimp
    5.14 +    unfolding array_ran_def Array.update_def by fastsimp
    5.15  qed
    5.16  
    5.17  lemma array_ran_upd_array_None:
    5.18 -  assumes "cl \<in> array_ran a (Array.change a i None h)"
    5.19 +  assumes "cl \<in> array_ran a (Array.update a i None h)"
    5.20    shows "cl \<in> array_ran a h"
    5.21  proof -
    5.22    have "set (get_array a h[i := None]) \<subseteq> insert None (set (get_array a h))" by (rule set_update_subset_insert)
    5.23    with assms show ?thesis
    5.24 -    unfolding array_ran_def Array.change_def by auto
    5.25 +    unfolding array_ran_def Array.update_def by auto
    5.26  qed
    5.27  
    5.28  definition correctArray :: "Clause list \<Rightarrow> Clause option array \<Rightarrow> heap \<Rightarrow> bool"
    5.29 @@ -152,7 +152,7 @@
    5.30  lemma correctArray_update:
    5.31    assumes "correctArray rcs a h"
    5.32    assumes "correctClause rcs c" "sorted c" "distinct c"
    5.33 -  shows "correctArray rcs a (Array.change a i (Some c) h)"
    5.34 +  shows "correctArray rcs a (Array.update a i (Some c) h)"
    5.35    using assms
    5.36    unfolding correctArray_def
    5.37    by (auto dest:array_ran_upd_array_Some)
    5.38 @@ -413,7 +413,7 @@
    5.39  definition get_clause :: "Clause option array \<Rightarrow> ClauseId \<Rightarrow> Clause Heap"
    5.40  where
    5.41    "get_clause a i = 
    5.42 -       (do c \<leftarrow> nth a i;
    5.43 +       (do c \<leftarrow> Array.nth a i;
    5.44             (case c of None \<Rightarrow> raise (''Clause not found'')
    5.45                      | Some x \<Rightarrow> return x)
    5.46          done)"
    5.47 @@ -440,11 +440,11 @@
    5.48    (do
    5.49       cli \<leftarrow> get_clause a i;
    5.50       result \<leftarrow> foldM (res_thm2 a) rs cli;
    5.51 -     upd saveTo (Some result) a; 
    5.52 +     Array.upd saveTo (Some result) a; 
    5.53       return rcs
    5.54     done)"
    5.55 -| "doProofStep2 a (Delete cid) rcs = (do upd cid None a; return rcs done)"
    5.56 -| "doProofStep2 a (Root cid clause) rcs = (do upd cid (Some (remdups (sort clause))) a; return (clause # rcs) done)"
    5.57 +| "doProofStep2 a (Delete cid) rcs = (do Array.upd cid None a; return rcs done)"
    5.58 +| "doProofStep2 a (Root cid clause) rcs = (do Array.upd cid (Some (remdups (sort clause))) a; return (clause # rcs) done)"
    5.59  | "doProofStep2 a (Xstep cid1 cid2) rcs = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''"
    5.60  | "doProofStep2 a (ProofDone b) rcs = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''"
    5.61  
     6.1 --- a/src/HOL/Imperative_HOL/ex/Subarray.thy	Tue Jul 13 11:38:04 2010 +0200
     6.2 +++ b/src/HOL/Imperative_HOL/ex/Subarray.thy	Tue Jul 13 12:01:34 2010 +0200
     6.3 @@ -11,20 +11,20 @@
     6.4  definition subarray :: "nat \<Rightarrow> nat \<Rightarrow> ('a::heap) array \<Rightarrow> heap \<Rightarrow> 'a list" where
     6.5    "subarray n m a h \<equiv> sublist' n m (get_array a h)"
     6.6  
     6.7 -lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Array.change a i v h) = subarray n m a h"
     6.8 -apply (simp add: subarray_def Array.change_def)
     6.9 +lemma subarray_upd: "i \<ge> m \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h"
    6.10 +apply (simp add: subarray_def Array.update_def)
    6.11  apply (simp add: sublist'_update1)
    6.12  done
    6.13  
    6.14 -lemma subarray_upd2: " i < n  \<Longrightarrow> subarray n m a (Array.change a i v h) = subarray n m a h"
    6.15 -apply (simp add: subarray_def Array.change_def)
    6.16 +lemma subarray_upd2: " i < n  \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h"
    6.17 +apply (simp add: subarray_def Array.update_def)
    6.18  apply (subst sublist'_update2)
    6.19  apply fastsimp
    6.20  apply simp
    6.21  done
    6.22  
    6.23 -lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Array.change a i v h) = subarray n m a h[i - n := v]"
    6.24 -unfolding subarray_def Array.change_def
    6.25 +lemma subarray_upd3: "\<lbrakk> n \<le> i; i < m\<rbrakk> \<Longrightarrow> subarray n m a (Array.update a i v h) = subarray n m a h[i - n := v]"
    6.26 +unfolding subarray_def Array.update_def
    6.27  by (simp add: sublist'_update3)
    6.28  
    6.29  lemma subarray_Nil: "n \<ge> m \<Longrightarrow> subarray n m a h = []"