6 |
6 |
7 theory Array |
7 theory Array |
8 imports Heap_Monad |
8 imports Heap_Monad |
9 begin |
9 begin |
10 |
10 |
|
11 subsection {* Primitive layer *} |
|
12 |
|
13 definition |
|
14 array_present :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> bool" where |
|
15 "array_present a h \<longleftrightarrow> addr_of_array a < lim h" |
|
16 |
|
17 definition |
|
18 get_array :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> 'a list" where |
|
19 "get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))" |
|
20 |
|
21 definition |
|
22 set_array :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where |
|
23 "set_array a x = |
|
24 arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))" |
|
25 |
|
26 definition array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where |
|
27 "array xs h = (let |
|
28 l = lim h; |
|
29 r = Array l; |
|
30 h'' = set_array r xs (h\<lparr>lim := l + 1\<rparr>) |
|
31 in (r, h''))" |
|
32 |
|
33 definition length :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> nat" where |
|
34 "length a h = List.length (get_array a h)" |
|
35 |
|
36 definition change :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where |
|
37 "change a i x h = set_array a ((get_array a h)[i:=x]) h" |
|
38 |
|
39 text {* Properties of imperative arrays *} |
|
40 |
|
41 text {* FIXME: Does there exist a "canonical" array axiomatisation in |
|
42 the literature? *} |
|
43 |
|
44 definition noteq_arrs :: "('a\<Colon>heap) array \<Rightarrow> ('b\<Colon>heap) array \<Rightarrow> bool" (infix "=!!=" 70) where |
|
45 "r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s" |
|
46 |
|
47 lemma noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a" |
|
48 and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'" |
|
49 unfolding noteq_arrs_def by auto |
|
50 |
|
51 lemma noteq_arrs_irrefl: "r =!!= r \<Longrightarrow> False" |
|
52 unfolding noteq_arrs_def by auto |
|
53 |
|
54 lemma present_new_arr: "array_present a h \<Longrightarrow> a =!!= fst (array xs h)" |
|
55 by (simp add: array_present_def noteq_arrs_def array_def Let_def) |
|
56 |
|
57 lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x" |
|
58 by (simp add: get_array_def set_array_def o_def) |
|
59 |
|
60 lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h" |
|
61 by (simp add: noteq_arrs_def get_array_def set_array_def) |
|
62 |
|
63 lemma set_array_same [simp]: |
|
64 "set_array r x (set_array r y h) = set_array r x h" |
|
65 by (simp add: set_array_def) |
|
66 |
|
67 lemma array_set_set_swap: |
|
68 "r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)" |
|
69 by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def) |
|
70 |
|
71 lemma get_array_change_eq [simp]: |
|
72 "get_array a (change a i v h) = (get_array a h) [i := v]" |
|
73 by (simp add: change_def) |
|
74 |
|
75 lemma nth_change_array_neq_array [simp]: |
|
76 "a =!!= b \<Longrightarrow> get_array a (change b j v h) ! i = get_array a h ! i" |
|
77 by (simp add: change_def noteq_arrs_def) |
|
78 |
|
79 lemma get_arry_array_change_elem_neqIndex [simp]: |
|
80 "i \<noteq> j \<Longrightarrow> get_array a (change a j v h) ! i = get_array a h ! i" |
|
81 by simp |
|
82 |
|
83 lemma length_change [simp]: |
|
84 "length a (change b i v h) = length a h" |
|
85 by (simp add: change_def length_def set_array_def get_array_def) |
|
86 |
|
87 lemma change_swap_neqArray: |
|
88 "a =!!= a' \<Longrightarrow> |
|
89 change a i v (change a' i' v' h) |
|
90 = change a' i' v' (change a i v h)" |
|
91 apply (unfold change_def) |
|
92 apply simp |
|
93 apply (subst array_set_set_swap, assumption) |
|
94 apply (subst array_get_set_neq) |
|
95 apply (erule noteq_arrs_sym) |
|
96 apply (simp) |
|
97 done |
|
98 |
|
99 lemma change_swap_neqIndex: |
|
100 "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> change a i v (change a i' v' h) = change a i' v' (change a i v h)" |
|
101 by (auto simp add: change_def array_set_set_swap list_update_swap) |
|
102 |
|
103 lemma get_array_init_array_list: |
|
104 "get_array (fst (array ls h)) (snd (array ls' h)) = ls'" |
|
105 by (simp add: Let_def split_def array_def) |
|
106 |
|
107 lemma set_array: |
|
108 "set_array (fst (array ls h)) |
|
109 new_ls (snd (array ls h)) |
|
110 = snd (array new_ls h)" |
|
111 by (simp add: Let_def split_def array_def) |
|
112 |
|
113 lemma array_present_change [simp]: |
|
114 "array_present a (change b i v h) = array_present a h" |
|
115 by (simp add: change_def array_present_def set_array_def get_array_def) |
|
116 |
|
117 |
|
118 |
11 subsection {* Primitives *} |
119 subsection {* Primitives *} |
12 |
120 |
13 definition |
121 definition |
14 new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where |
122 new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where |
15 [code del]: "new n x = Heap_Monad.heap (Heap.array (replicate n x))" |
123 [code del]: "new n x = Heap_Monad.heap (Array.array (replicate n x))" |
16 |
124 |
17 definition |
125 definition |
18 of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where |
126 of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where |
19 [code del]: "of_list xs = Heap_Monad.heap (Heap.array xs)" |
127 [code del]: "of_list xs = Heap_Monad.heap (Array.array xs)" |
20 |
128 |
21 definition |
129 definition |
22 length :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where |
130 len :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where |
23 [code del]: "length arr = Heap_Monad.heap (\<lambda>h. (Heap.length arr h, h))" |
131 [code del]: "len arr = Heap_Monad.heap (\<lambda>h. (Array.length arr h, h))" |
24 |
132 |
25 definition |
133 definition |
26 nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap" |
134 nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap" |
27 where |
135 where |
28 [code del]: "nth a i = (do len \<leftarrow> length a; |
136 [code del]: "nth a i = (do len \<leftarrow> len a; |
29 (if i < len |
137 (if i < len |
30 then Heap_Monad.heap (\<lambda>h. (get_array a h ! i, h)) |
138 then Heap_Monad.heap (\<lambda>h. (get_array a h ! i, h)) |
31 else raise ''array lookup: index out of range'') |
139 else raise ''array lookup: index out of range'') |
32 done)" |
140 done)" |
33 |
141 |
34 definition |
142 definition |
35 upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap" |
143 upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap" |
36 where |
144 where |
37 [code del]: "upd i x a = (do len \<leftarrow> length a; |
145 [code del]: "upd i x a = (do len \<leftarrow> len a; |
38 (if i < len |
146 (if i < len |
39 then Heap_Monad.heap (\<lambda>h. (a, Heap.upd a i x h)) |
147 then Heap_Monad.heap (\<lambda>h. (a, change a i x h)) |
40 else raise ''array update: index out of range'') |
148 else raise ''array update: index out of range'') |
41 done)" |
149 done)" |
42 |
150 |
43 lemma upd_return: |
151 lemma upd_return: |
44 "upd i x a \<guillemotright> return a = upd i x a" |
152 "upd i x a \<guillemotright> return a = upd i x a" |
123 hide_const (open) make' |
230 hide_const (open) make' |
124 lemma [code]: |
231 lemma [code]: |
125 "Array.make n f = Array.make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)" |
232 "Array.make n f = Array.make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)" |
126 by (simp add: make'_def o_def) |
233 by (simp add: make'_def o_def) |
127 |
234 |
128 definition length' where |
235 definition len' where |
129 [code del]: "length' a = Array.length a \<guillemotright>= (\<lambda>n. return (Code_Numeral.of_nat n))" |
236 [code del]: "len' a = Array.len a \<guillemotright>= (\<lambda>n. return (Code_Numeral.of_nat n))" |
130 hide_const (open) length' |
237 hide_const (open) len' |
131 lemma [code]: |
238 lemma [code]: |
132 "Array.length a = Array.length' a \<guillemotright>= (\<lambda>i. return (Code_Numeral.nat_of i))" |
239 "Array.len a = Array.len' a \<guillemotright>= (\<lambda>i. return (Code_Numeral.nat_of i))" |
133 by (simp add: length'_def) |
240 by (simp add: len'_def) |
134 |
241 |
135 definition nth' where |
242 definition nth' where |
136 [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of" |
243 [code del]: "nth' a = Array.nth a o Code_Numeral.nat_of" |
137 hide_const (open) nth' |
244 hide_const (open) nth' |
138 lemma [code]: |
245 lemma [code]: |
152 code_type array (SML "_/ array") |
259 code_type array (SML "_/ array") |
153 code_const Array (SML "raise/ (Fail/ \"bare Array\")") |
260 code_const Array (SML "raise/ (Fail/ \"bare Array\")") |
154 code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))") |
261 code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))") |
155 code_const Array.of_list' (SML "(fn/ ()/ =>/ Array.fromList/ _)") |
262 code_const Array.of_list' (SML "(fn/ ()/ =>/ Array.fromList/ _)") |
156 code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))") |
263 code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))") |
157 code_const Array.length' (SML "(fn/ ()/ =>/ Array.length/ _)") |
264 code_const Array.len' (SML "(fn/ ()/ =>/ Array.length/ _)") |
158 code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))") |
265 code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))") |
159 code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))") |
266 code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))") |
160 |
267 |
161 code_reserved SML Array |
268 code_reserved SML Array |
162 |
269 |