8 imports Heap_Monad |
8 imports Heap_Monad |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Primitives *} |
11 subsection {* Primitives *} |
12 |
12 |
13 definition (*FIXME present *) |
13 definition present :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> bool" where |
14 array_present :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> bool" where |
14 "present h a \<longleftrightarrow> addr_of_array a < lim h" |
15 "array_present h a \<longleftrightarrow> addr_of_array a < lim h" |
|
16 |
15 |
17 definition (*FIXME get :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a list" where*) |
16 definition (*FIXME get :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a list" where*) |
18 get_array :: "'a\<Colon>heap array \<Rightarrow> heap \<Rightarrow> 'a list" where |
17 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))" |
18 "get_array a h = map from_nat (arrays h (TYPEREP('a)) (addr_of_array a))" |
20 |
19 |
21 definition (*FIXME set*) |
20 definition set :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where |
22 set_array :: "'a\<Colon>heap array \<Rightarrow> 'a list \<Rightarrow> heap \<Rightarrow> heap" where |
21 "set a x = arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))" |
23 "set_array a x = |
22 |
24 arrays_update (\<lambda>h. h(TYPEREP('a) := ((h(TYPEREP('a))) (addr_of_array a:=map to_nat x))))" |
23 definition alloc :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where |
25 |
24 "alloc xs h = (let |
26 definition (*FIXME alloc*) |
|
27 array :: "'a list \<Rightarrow> heap \<Rightarrow> 'a\<Colon>heap array \<times> heap" where |
|
28 "array xs h = (let |
|
29 l = lim h; |
25 l = lim h; |
30 r = Array l; |
26 r = Array l; |
31 h'' = set_array r xs (h\<lparr>lim := l + 1\<rparr>) |
27 h'' = set r xs (h\<lparr>lim := l + 1\<rparr>) |
32 in (r, h''))" |
28 in (r, h''))" |
33 |
29 |
34 definition length :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> nat" where |
30 definition length :: "heap \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> nat" where |
35 "length h a = List.length (get_array a h)" |
31 "length h a = List.length (get_array a h)" |
36 |
32 |
37 definition update :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where |
33 definition update :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> heap \<Rightarrow> heap" where |
38 "update a i x h = set_array a ((get_array a h)[i:=x]) h" |
34 "update a i x h = set a ((get_array a h)[i:=x]) h" |
39 |
35 |
40 definition (*FIXME noteq*) |
36 definition noteq :: "'a\<Colon>heap array \<Rightarrow> 'b\<Colon>heap array \<Rightarrow> bool" (infix "=!!=" 70) where |
41 noteq_arrs :: "'a\<Colon>heap array \<Rightarrow> 'b\<Colon>heap array \<Rightarrow> bool" (infix "=!!=" 70) where |
|
42 "r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s" |
37 "r =!!= s \<longleftrightarrow> TYPEREP('a) \<noteq> TYPEREP('b) \<or> addr_of_array r \<noteq> addr_of_array s" |
43 |
38 |
44 |
39 |
45 subsection {* Monad operations *} |
40 subsection {* Monad operations *} |
46 |
41 |
47 definition new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where |
42 definition new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where |
48 [code del]: "new n x = Heap_Monad.heap (array (replicate n x))" |
43 [code del]: "new n x = Heap_Monad.heap (alloc (replicate n x))" |
49 |
44 |
50 definition of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where |
45 definition of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where |
51 [code del]: "of_list xs = Heap_Monad.heap (array xs)" |
46 [code del]: "of_list xs = Heap_Monad.heap (alloc xs)" |
52 |
47 |
53 definition make :: "nat \<Rightarrow> (nat \<Rightarrow> 'a\<Colon>heap) \<Rightarrow> 'a array Heap" where |
48 definition make :: "nat \<Rightarrow> (nat \<Rightarrow> 'a\<Colon>heap) \<Rightarrow> 'a array Heap" where |
54 [code del]: "make n f = Heap_Monad.heap (array (map f [0 ..< n]))" |
49 [code del]: "make n f = Heap_Monad.heap (alloc (map f [0 ..< n]))" |
55 |
50 |
56 definition len :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where |
51 definition len :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where |
57 [code del]: "len a = Heap_Monad.tap (\<lambda>h. length h a)" |
52 [code del]: "len a = Heap_Monad.tap (\<lambda>h. length h a)" |
58 |
53 |
59 definition nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap" where |
54 definition nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap" where |
83 |
78 |
84 text {* Primitives *} |
79 text {* Primitives *} |
85 |
80 |
86 lemma noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a" |
81 lemma noteq_arrs_sym: "a =!!= b \<Longrightarrow> b =!!= a" |
87 and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'" |
82 and unequal_arrs [simp]: "a \<noteq> a' \<longleftrightarrow> a =!!= a'" |
88 unfolding noteq_arrs_def by auto |
83 unfolding noteq_def by auto |
89 |
84 |
90 lemma noteq_arrs_irrefl: "r =!!= r \<Longrightarrow> False" |
85 lemma noteq_arrs_irrefl: "r =!!= r \<Longrightarrow> False" |
91 unfolding noteq_arrs_def by auto |
86 unfolding noteq_def by auto |
92 |
87 |
93 lemma present_new_arr: "array_present h a \<Longrightarrow> a =!!= fst (array xs h)" |
88 lemma present_new_arr: "present h a \<Longrightarrow> a =!!= fst (alloc xs h)" |
94 by (simp add: array_present_def noteq_arrs_def array_def Let_def) |
89 by (simp add: present_def noteq_def alloc_def Let_def) |
95 |
90 |
96 lemma array_get_set_eq [simp]: "get_array r (set_array r x h) = x" |
91 lemma array_get_set_eq [simp]: "get_array r (set r x h) = x" |
97 by (simp add: get_array_def set_array_def o_def) |
92 by (simp add: get_array_def set_def o_def) |
98 |
93 |
99 lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set_array s x h) = get_array r h" |
94 lemma array_get_set_neq [simp]: "r =!!= s \<Longrightarrow> get_array r (set s x h) = get_array r h" |
100 by (simp add: noteq_arrs_def get_array_def set_array_def) |
95 by (simp add: noteq_def get_array_def set_def) |
101 |
96 |
102 lemma set_array_same [simp]: |
97 lemma set_array_same [simp]: |
103 "set_array r x (set_array r y h) = set_array r x h" |
98 "set r x (set r y h) = set r x h" |
104 by (simp add: set_array_def) |
99 by (simp add: set_def) |
105 |
100 |
106 lemma array_set_set_swap: |
101 lemma array_set_set_swap: |
107 "r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)" |
102 "r =!!= r' \<Longrightarrow> set r x (set r' x' h) = set r' x' (set r x h)" |
108 by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def) |
103 by (simp add: Let_def expand_fun_eq noteq_def set_def) |
109 |
104 |
110 lemma get_array_update_eq [simp]: |
105 lemma get_array_update_eq [simp]: |
111 "get_array a (update a i v h) = (get_array a h) [i := v]" |
106 "get_array a (update a i v h) = (get_array a h) [i := v]" |
112 by (simp add: update_def) |
107 by (simp add: update_def) |
113 |
108 |
114 lemma nth_update_array_neq_array [simp]: |
109 lemma nth_update_array_neq_array [simp]: |
115 "a =!!= b \<Longrightarrow> get_array a (update b j v h) ! i = get_array a h ! i" |
110 "a =!!= b \<Longrightarrow> get_array a (update b j v h) ! i = get_array a h ! i" |
116 by (simp add: update_def noteq_arrs_def) |
111 by (simp add: update_def noteq_def) |
117 |
112 |
118 lemma get_arry_array_update_elem_neqIndex [simp]: |
113 lemma get_arry_array_update_elem_neqIndex [simp]: |
119 "i \<noteq> j \<Longrightarrow> get_array a (update a j v h) ! i = get_array a h ! i" |
114 "i \<noteq> j \<Longrightarrow> get_array a (update a j v h) ! i = get_array a h ! i" |
120 by simp |
115 by simp |
121 |
116 |
122 lemma length_update [simp]: |
117 lemma length_update [simp]: |
123 "length (update b i v h) = length h" |
118 "length (update b i v h) = length h" |
124 by (simp add: update_def length_def set_array_def get_array_def expand_fun_eq) |
119 by (simp add: update_def length_def set_def get_array_def expand_fun_eq) |
125 |
120 |
126 lemma update_swap_neqArray: |
121 lemma update_swap_neqArray: |
127 "a =!!= a' \<Longrightarrow> |
122 "a =!!= a' \<Longrightarrow> |
128 update a i v (update a' i' v' h) |
123 update a i v (update a' i' v' h) |
129 = update a' i' v' (update a i v h)" |
124 = update a' i' v' (update a i v h)" |
138 lemma update_swap_neqIndex: |
133 lemma update_swap_neqIndex: |
139 "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> update a i v (update a i' v' h) = update a i' v' (update a i v h)" |
134 "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> update a i v (update a i' v' h) = update a i' v' (update a i v h)" |
140 by (auto simp add: update_def array_set_set_swap list_update_swap) |
135 by (auto simp add: update_def array_set_set_swap list_update_swap) |
141 |
136 |
142 lemma get_array_init_array_list: |
137 lemma get_array_init_array_list: |
143 "get_array (fst (array ls h)) (snd (array ls' h)) = ls'" |
138 "get_array (fst (alloc ls h)) (snd (alloc ls' h)) = ls'" |
144 by (simp add: Let_def split_def array_def) |
139 by (simp add: Let_def split_def alloc_def) |
145 |
140 |
146 lemma set_array: |
141 lemma set_array: |
147 "set_array (fst (array ls h)) |
142 "set (fst (alloc ls h)) |
148 new_ls (snd (array ls h)) |
143 new_ls (snd (alloc ls h)) |
149 = snd (array new_ls h)" |
144 = snd (alloc new_ls h)" |
150 by (simp add: Let_def split_def array_def) |
145 by (simp add: Let_def split_def alloc_def) |
151 |
146 |
152 lemma array_present_update [simp]: |
147 lemma array_present_update [simp]: |
153 "array_present (update b i v h) = array_present h" |
148 "present (update b i v h) = present h" |
154 by (simp add: update_def array_present_def set_array_def get_array_def expand_fun_eq) |
149 by (simp add: update_def present_def set_def get_array_def expand_fun_eq) |
155 |
150 |
156 lemma array_present_array [simp]: |
151 lemma array_present_array [simp]: |
157 "array_present (snd (array xs h)) (fst (array xs h))" |
152 "present (snd (alloc xs h)) (fst (alloc xs h))" |
158 by (simp add: array_present_def array_def set_array_def Let_def) |
153 by (simp add: present_def alloc_def set_def Let_def) |
159 |
154 |
160 lemma not_array_present_array [simp]: |
155 lemma not_array_present_array [simp]: |
161 "\<not> array_present h (fst (array xs h))" |
156 "\<not> present h (fst (alloc xs h))" |
162 by (simp add: array_present_def array_def Let_def) |
157 by (simp add: present_def alloc_def Let_def) |
163 |
158 |
164 |
159 |
165 text {* Monad operations *} |
160 text {* Monad operations *} |
166 |
161 |
167 lemma execute_new [execute_simps]: |
162 lemma execute_new [execute_simps]: |
168 "execute (new n x) h = Some (array (replicate n x) h)" |
163 "execute (new n x) h = Some (alloc (replicate n x) h)" |
169 by (simp add: new_def execute_simps) |
164 by (simp add: new_def execute_simps) |
170 |
165 |
171 lemma success_newI [success_intros]: |
166 lemma success_newI [success_intros]: |
172 "success (new n x) h" |
167 "success (new n x) h" |
173 by (auto intro: success_intros simp add: new_def) |
168 by (auto intro: success_intros simp add: new_def) |
174 |
169 |
175 lemma crel_newI [crel_intros]: |
170 lemma crel_newI [crel_intros]: |
176 assumes "(a, h') = array (replicate n x) h" |
171 assumes "(a, h') = alloc (replicate n x) h" |
177 shows "crel (new n x) h h' a" |
172 shows "crel (new n x) h h' a" |
178 by (rule crelI) (simp add: assms execute_simps) |
173 by (rule crelI) (simp add: assms execute_simps) |
179 |
174 |
180 lemma crel_newE [crel_elims]: |
175 lemma crel_newE [crel_elims]: |
181 assumes "crel (new n x) h h' r" |
176 assumes "crel (new n x) h h' r" |
182 obtains "r = fst (array (replicate n x) h)" "h' = snd (array (replicate n x) h)" |
177 obtains "r = fst (alloc (replicate n x) h)" "h' = snd (alloc (replicate n x) h)" |
183 "get_array r h' = replicate n x" "array_present h' r" "\<not> array_present h r" |
178 "get_array r h' = replicate n x" "present h' r" "\<not> present h r" |
184 using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps) |
179 using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps) |
185 |
180 |
186 lemma execute_of_list [execute_simps]: |
181 lemma execute_of_list [execute_simps]: |
187 "execute (of_list xs) h = Some (array xs h)" |
182 "execute (of_list xs) h = Some (alloc xs h)" |
188 by (simp add: of_list_def execute_simps) |
183 by (simp add: of_list_def execute_simps) |
189 |
184 |
190 lemma success_of_listI [success_intros]: |
185 lemma success_of_listI [success_intros]: |
191 "success (of_list xs) h" |
186 "success (of_list xs) h" |
192 by (auto intro: success_intros simp add: of_list_def) |
187 by (auto intro: success_intros simp add: of_list_def) |
193 |
188 |
194 lemma crel_of_listI [crel_intros]: |
189 lemma crel_of_listI [crel_intros]: |
195 assumes "(a, h') = array xs h" |
190 assumes "(a, h') = alloc xs h" |
196 shows "crel (of_list xs) h h' a" |
191 shows "crel (of_list xs) h h' a" |
197 by (rule crelI) (simp add: assms execute_simps) |
192 by (rule crelI) (simp add: assms execute_simps) |
198 |
193 |
199 lemma crel_of_listE [crel_elims]: |
194 lemma crel_of_listE [crel_elims]: |
200 assumes "crel (of_list xs) h h' r" |
195 assumes "crel (of_list xs) h h' r" |
201 obtains "r = fst (array xs h)" "h' = snd (array xs h)" |
196 obtains "r = fst (alloc xs h)" "h' = snd (alloc xs h)" |
202 "get_array r h' = xs" "array_present h' r" "\<not> array_present h r" |
197 "get_array r h' = xs" "present h' r" "\<not> present h r" |
203 using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps) |
198 using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps) |
204 |
199 |
205 lemma execute_make [execute_simps]: |
200 lemma execute_make [execute_simps]: |
206 "execute (make n f) h = Some (array (map f [0 ..< n]) h)" |
201 "execute (make n f) h = Some (alloc (map f [0 ..< n]) h)" |
207 by (simp add: make_def execute_simps) |
202 by (simp add: make_def execute_simps) |
208 |
203 |
209 lemma success_makeI [success_intros]: |
204 lemma success_makeI [success_intros]: |
210 "success (make n f) h" |
205 "success (make n f) h" |
211 by (auto intro: success_intros simp add: make_def) |
206 by (auto intro: success_intros simp add: make_def) |
212 |
207 |
213 lemma crel_makeI [crel_intros]: |
208 lemma crel_makeI [crel_intros]: |
214 assumes "(a, h') = array (map f [0 ..< n]) h" |
209 assumes "(a, h') = alloc (map f [0 ..< n]) h" |
215 shows "crel (make n f) h h' a" |
210 shows "crel (make n f) h h' a" |
216 by (rule crelI) (simp add: assms execute_simps) |
211 by (rule crelI) (simp add: assms execute_simps) |
217 |
212 |
218 lemma crel_makeE [crel_elims]: |
213 lemma crel_makeE [crel_elims]: |
219 assumes "crel (make n f) h h' r" |
214 assumes "crel (make n f) h h' r" |
220 obtains "r = fst (array (map f [0 ..< n]) h)" "h' = snd (array (map f [0 ..< n]) h)" |
215 obtains "r = fst (alloc (map f [0 ..< n]) h)" "h' = snd (alloc (map f [0 ..< n]) h)" |
221 "get_array r h' = map f [0 ..< n]" "array_present h' r" "\<not> array_present h r" |
216 "get_array r h' = map f [0 ..< n]" "present h' r" "\<not> present h r" |
222 using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps) |
217 using assms by (rule crelE) (simp add: get_array_init_array_list execute_simps) |
223 |
218 |
224 lemma execute_len [execute_simps]: |
219 lemma execute_len [execute_simps]: |
225 "execute (len a) h = Some (length h a, h)" |
220 "execute (len a) h = Some (length h a, h)" |
226 by (simp add: len_def execute_simps) |
221 by (simp add: len_def execute_simps) |