src/HOL/Imperative_HOL/Array.thy
 changeset 37719 271ecd4fb9f9 parent 37716 24bb91462892 child 37752 d0a384c84d69
```     1.1 --- a/src/HOL/Imperative_HOL/Array.thy	Mon Jul 05 15:36:37 2010 +0200
1.2 +++ b/src/HOL/Imperative_HOL/Array.thy	Mon Jul 05 16:46:23 2010 +0200
1.3 @@ -8,24 +8,132 @@
1.5  begin
1.6
1.7 +subsection {* Primitive layer *}
1.8 +
1.9 +definition
1.10 +  array_present :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> bool" where
1.11 +  "array_present a h \<longleftrightarrow> addr_of_array a < lim h"
1.12 +
1.13 +definition
1.14 +  get_array :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> 'a list" where
1.15 +  "get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))"
1.16 +
1.17 +definition
1.18 +  set_array :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where
1.19 +  "set_array a x =
1.20 +  arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))"
1.21 +
1.22 +definition array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where
1.23 +  "array xs h = (let
1.24 +     l = lim h;
1.25 +     r = Array l;
1.26 +     h'' = set_array r xs (h\<lparr>lim := l + 1\<rparr>)
1.27 +   in (r, h''))"
1.28 +
1.29 +definition length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where
1.30 +  "length a h = List.length (get_array a h)"
1.31 +
1.32 +definition change :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where
1.33 +  "change a i x h = set_array a ((get_array a h)[i:=x]) h"
1.34 +
1.35 +text {* Properties of imperative arrays *}
1.36 +
1.37 +text {* FIXME: Does there exist a "canonical" array axiomatisation in
1.38 +the literature?  *}
1.39 +
1.40 +definition noteq_arrs :: "('a\<Colon>heap) array \<Rightarrow> ('b\<Colon>heap) array \<Rightarrow> bool" (infix "=!!=" 70) where
1.41 +  "r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s"
1.42 +
1.43 +lemma noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a"
1.44 +  and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'"
1.45 +  unfolding noteq_arrs_def by auto
1.46 +
1.47 +lemma noteq_arrs_irrefl: "r =!!= r \<Longrightarrow> False"
1.48 +  unfolding noteq_arrs_def by auto
1.49 +
1.50 +lemma present_new_arr: "array_present a h \<Longrightarrow> a =!!= fst (array xs h)"
1.51 +  by (simp add: array_present_def noteq_arrs_def array_def Let_def)
1.52 +
1.53 +lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x"
1.54 +  by (simp add: get_array_def set_array_def o_def)
1.55 +
1.56 +lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h"
1.57 +  by (simp add: noteq_arrs_def get_array_def set_array_def)
1.58 +
1.59 +lemma set_array_same [simp]:
1.60 +  "set_array r x (set_array r y h) = set_array r x h"
1.61 +  by (simp add: set_array_def)
1.62 +
1.63 +lemma array_set_set_swap:
1.64 +  "r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)"
1.65 +  by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def)
1.66 +
1.67 +lemma get_array_change_eq [simp]:
1.68 +  "get_array a (change a i v h) = (get_array a h) [i := v]"
1.69 +  by (simp add: change_def)
1.70 +
1.71 +lemma nth_change_array_neq_array [simp]:
1.72 +  "a =!!= b \<Longrightarrow> get_array a (change b j v h) ! i = get_array a h ! i"
1.73 +  by (simp add: change_def noteq_arrs_def)
1.74 +
1.75 +lemma get_arry_array_change_elem_neqIndex [simp]:
1.76 +  "i \<noteq> j \<Longrightarrow> get_array a (change a j v h) ! i = get_array a h ! i"
1.77 +  by simp
1.78 +
1.79 +lemma length_change [simp]:
1.80 +  "length a (change b i v h) = length a h"
1.81 +  by (simp add: change_def length_def set_array_def get_array_def)
1.82 +
1.83 +lemma change_swap_neqArray:
1.84 +  "a =!!= a' \<Longrightarrow>
1.85 +  change a i v (change a' i' v' h)
1.86 +  = change a' i' v' (change a i v h)"
1.87 +apply (unfold change_def)
1.88 +apply simp
1.89 +apply (subst array_set_set_swap, assumption)
1.90 +apply (subst array_get_set_neq)
1.91 +apply (erule noteq_arrs_sym)
1.92 +apply (simp)
1.93 +done
1.94 +
1.95 +lemma change_swap_neqIndex:
1.96 +  "\<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.97 +  by (auto simp add: change_def array_set_set_swap list_update_swap)
1.98 +
1.99 +lemma get_array_init_array_list:
1.100 +  "get_array (fst (array ls h)) (snd (array ls' h)) = ls'"
1.101 +  by (simp add: Let_def split_def array_def)
1.102 +
1.103 +lemma set_array:
1.104 +  "set_array (fst (array ls h))
1.105 +     new_ls (snd (array ls h))
1.106 +       = snd (array new_ls h)"
1.107 +  by (simp add: Let_def split_def array_def)
1.108 +
1.109 +lemma array_present_change [simp]:
1.110 +  "array_present a (change b i v h) = array_present a h"
1.111 +  by (simp add: change_def array_present_def set_array_def get_array_def)
1.112 +
1.113 +
1.114 +
1.115  subsection {* Primitives *}
1.116
1.117  definition
1.118    new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where
1.119 -  [code del]: "new n x = Heap_Monad.heap (Heap.array (replicate n x))"
1.120 +  [code del]: "new n x = Heap_Monad.heap (Array.array (replicate n x))"
1.121
1.122  definition
1.123    of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where
1.124 -  [code del]: "of_list xs = Heap_Monad.heap (Heap.array xs)"
1.125 +  [code del]: "of_list xs = Heap_Monad.heap (Array.array xs)"
1.126
1.127  definition
1.128 -  length :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
1.129 -  [code del]: "length arr = Heap_Monad.heap (\<lambda>h. (Heap.length arr h, h))"
1.130 +  len :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where
1.131 +  [code del]: "len arr = Heap_Monad.heap (\<lambda>h. (Array.length arr h, h))"
1.132
1.133  definition
1.134    nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap"
1.135  where
1.136 -  [code del]: "nth a i = (do len \<leftarrow> length a;
1.137 +  [code del]: "nth a i = (do len \<leftarrow> len a;
1.138                   (if i < len
1.139                       then Heap_Monad.heap (\<lambda>h. (get_array a h ! i, h))
1.140                       else raise ''array lookup: index out of range'')
1.141 @@ -34,9 +142,9 @@
1.142  definition
1.143    upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap"
1.144  where
1.145 -  [code del]: "upd i x a = (do len \<leftarrow> length a;
1.146 +  [code del]: "upd i x a = (do len \<leftarrow> len a;
1.147                        (if i < len
1.148 -                           then Heap_Monad.heap (\<lambda>h. (a, Heap.upd a i x h))
1.149 +                           then Heap_Monad.heap (\<lambda>h. (a, change a i x h))
1.150                             else raise ''array update: index out of range'')
1.151                     done)"
1.152
1.153 @@ -73,7 +181,7 @@
1.154    freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap"
1.155  where
1.156    "freeze a = (do
1.157 -     n \<leftarrow> length a;
1.158 +     n \<leftarrow> len a;
1.159       mapM (nth a) [0..<n]
1.160     done)"
1.161
1.162 @@ -81,12 +189,11 @@
1.163     map :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap"
1.164  where
1.165    "map f a = (do
1.166 -     n \<leftarrow> length a;
1.167 +     n \<leftarrow> len a;
1.168       mapM (\<lambda>n. map_entry n f a) [0..<n];
1.169       return a
1.170     done)"
1.171
1.172 -hide_const (open) new map -- {* avoid clashed with some popular names *}
1.173
1.174
1.175  subsection {* Properties *}
1.176 @@ -125,12 +232,12 @@
1.177    "Array.make n f = Array.make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)"
1.178    by (simp add: make'_def o_def)
1.179
1.180 -definition length' where
1.181 -  [code del]: "length' a = Array.length a \<guillemotright>= (\<lambda>n. return (Code_Numeral.of_nat n))"
1.182 -hide_const (open) length'
1.183 +definition len' where
1.184 +  [code del]: "len' a = Array.len a \<guillemotright>= (\<lambda>n. return (Code_Numeral.of_nat n))"
1.185 +hide_const (open) len'
1.186  lemma [code]:
1.187 -  "Array.length a = Array.length' a \<guillemotright>= (\<lambda>i. return (Code_Numeral.nat_of i))"
1.188 -  by (simp add: length'_def)
1.189 +  "Array.len a = Array.len' a \<guillemotright>= (\<lambda>i. return (Code_Numeral.nat_of i))"
1.190 +  by (simp add: len'_def)
1.191
1.192  definition nth' where
1.193    [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of"
1.194 @@ -154,7 +261,7 @@
1.195  code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))")
1.196  code_const Array.of_list' (SML "(fn/ ()/ =>/ Array.fromList/ _)")
1.197  code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))")
1.198 -code_const Array.length' (SML "(fn/ ()/ =>/ Array.length/ _)")
1.199 +code_const Array.len' (SML "(fn/ ()/ =>/ Array.length/ _)")
1.200  code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))")
1.201  code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))")
1.202
1.203 @@ -167,7 +274,7 @@
1.204  code_const Array (OCaml "failwith/ \"bare Array\"")
1.205  code_const Array.new' (OCaml "(fun/ ()/ ->/ Array.make/ (Big'_int.int'_of'_big'_int/ _)/ _)")
1.206  code_const Array.of_list' (OCaml "(fun/ ()/ ->/ Array.of'_list/ _)")
1.207 -code_const Array.length' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
1.208 +code_const Array.len' (OCaml "(fun/ ()/ ->/ Big'_int.big'_int'_of'_int/ (Array.length/ _))")
1.209  code_const Array.nth' (OCaml "(fun/ ()/ ->/ Array.get/ _/ (Big'_int.int'_of'_big'_int/ _))")
1.210  code_const Array.upd' (OCaml "(fun/ ()/ ->/ Array.set/ _/ (Big'_int.int'_of'_big'_int/ _)/ _)")
1.211
1.212 @@ -180,8 +287,10 @@
1.213  code_const Array (Haskell "error/ \"bare Array\"")
1.214  code_const Array.new' (Haskell "Heap.newArray/ (0,/ _)")
1.215  code_const Array.of_list' (Haskell "Heap.newListArray/ (0,/ _)")