62 [code del]: "nth a i = Heap_Monad.guard (\<lambda>h. i < length a h) |
61 [code del]: "nth a i = Heap_Monad.guard (\<lambda>h. i < length a h) |
63 (\<lambda>h. (get_array a h ! i, h))" |
62 (\<lambda>h. (get_array a h ! i, h))" |
64 |
63 |
65 definition upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap" where |
64 definition upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap" where |
66 [code del]: "upd i x a = Heap_Monad.guard (\<lambda>h. i < length a h) |
65 [code del]: "upd i x a = Heap_Monad.guard (\<lambda>h. i < length a h) |
67 (\<lambda>h. (a, change a i x h))" |
66 (\<lambda>h. (a, update a i x h))" |
68 |
67 |
69 definition map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" where |
68 definition map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" where |
70 [code del]: "map_entry i f a = Heap_Monad.guard (\<lambda>h. i < length a h) |
69 [code del]: "map_entry i f a = Heap_Monad.guard (\<lambda>h. i < length a h) |
71 (\<lambda>h. (a, change a i (f (get_array a h ! i)) h))" |
70 (\<lambda>h. (a, update a i (f (get_array a h ! i)) h))" |
72 |
71 |
73 definition swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap" where |
72 definition swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap" where |
74 [code del]: "swap i x a = Heap_Monad.guard (\<lambda>h. i < length a h) |
73 [code del]: "swap i x a = Heap_Monad.guard (\<lambda>h. i < length a h) |
75 (\<lambda>h. (get_array a h ! i, change a i x h))" |
74 (\<lambda>h. (get_array a h ! i, update a i x h))" |
76 |
75 |
77 definition freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" where |
76 definition freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" where |
78 [code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get_array a h)" |
77 [code del]: "freeze a = Heap_Monad.tap (\<lambda>h. get_array a h)" |
79 |
78 |
80 |
79 |
107 |
106 |
108 lemma array_set_set_swap: |
107 lemma array_set_set_swap: |
109 "r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)" |
108 "r =!!= r' \<Longrightarrow> set_array r x (set_array r' x' h) = set_array r' x' (set_array r x h)" |
110 by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def) |
109 by (simp add: Let_def expand_fun_eq noteq_arrs_def set_array_def) |
111 |
110 |
112 lemma get_array_change_eq [simp]: |
111 lemma get_array_update_eq [simp]: |
113 "get_array a (change a i v h) = (get_array a h) [i := v]" |
112 "get_array a (update a i v h) = (get_array a h) [i := v]" |
114 by (simp add: change_def) |
113 by (simp add: update_def) |
115 |
114 |
116 lemma nth_change_array_neq_array [simp]: |
115 lemma nth_update_array_neq_array [simp]: |
117 "a =!!= b \<Longrightarrow> get_array a (change b j v h) ! i = get_array a h ! i" |
116 "a =!!= b \<Longrightarrow> get_array a (update b j v h) ! i = get_array a h ! i" |
118 by (simp add: change_def noteq_arrs_def) |
117 by (simp add: update_def noteq_arrs_def) |
119 |
118 |
120 lemma get_arry_array_change_elem_neqIndex [simp]: |
119 lemma get_arry_array_update_elem_neqIndex [simp]: |
121 "i \<noteq> j \<Longrightarrow> get_array a (change a j v h) ! i = get_array a h ! i" |
120 "i \<noteq> j \<Longrightarrow> get_array a (update a j v h) ! i = get_array a h ! i" |
122 by simp |
121 by simp |
123 |
122 |
124 lemma length_change [simp]: |
123 lemma length_update [simp]: |
125 "length a (change b i v h) = length a h" |
124 "length a (update b i v h) = length a h" |
126 by (simp add: change_def length_def set_array_def get_array_def) |
125 by (simp add: update_def length_def set_array_def get_array_def) |
127 |
126 |
128 lemma change_swap_neqArray: |
127 lemma update_swap_neqArray: |
129 "a =!!= a' \<Longrightarrow> |
128 "a =!!= a' \<Longrightarrow> |
130 change a i v (change a' i' v' h) |
129 update a i v (update a' i' v' h) |
131 = change a' i' v' (change a i v h)" |
130 = update a' i' v' (update a i v h)" |
132 apply (unfold change_def) |
131 apply (unfold update_def) |
133 apply simp |
132 apply simp |
134 apply (subst array_set_set_swap, assumption) |
133 apply (subst array_set_set_swap, assumption) |
135 apply (subst array_get_set_neq) |
134 apply (subst array_get_set_neq) |
136 apply (erule noteq_arrs_sym) |
135 apply (erule noteq_arrs_sym) |
137 apply (simp) |
136 apply (simp) |
138 done |
137 done |
139 |
138 |
140 lemma change_swap_neqIndex: |
139 lemma update_swap_neqIndex: |
141 "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> change a i v (change a i' v' h) = change a i' v' (change a i v h)" |
140 "\<lbrakk> i \<noteq> i' \<rbrakk> \<Longrightarrow> update a i v (update a i' v' h) = update a i' v' (update a i v h)" |
142 by (auto simp add: change_def array_set_set_swap list_update_swap) |
141 by (auto simp add: update_def array_set_set_swap list_update_swap) |
143 |
142 |
144 lemma get_array_init_array_list: |
143 lemma get_array_init_array_list: |
145 "get_array (fst (array ls h)) (snd (array ls' h)) = ls'" |
144 "get_array (fst (array ls h)) (snd (array ls' h)) = ls'" |
146 by (simp add: Let_def split_def array_def) |
145 by (simp add: Let_def split_def array_def) |
147 |
146 |
262 using assms by (rule crelE) |
261 using assms by (rule crelE) |
263 (erule successE, cases "i < length a h", simp_all add: execute_simps) |
262 (erule successE, cases "i < length a h", simp_all add: execute_simps) |
264 |
263 |
265 lemma execute_upd [execute_simps]: |
264 lemma execute_upd [execute_simps]: |
266 "i < length a h \<Longrightarrow> |
265 "i < length a h \<Longrightarrow> |
267 execute (upd i x a) h = Some (a, change a i x h)" |
266 execute (upd i x a) h = Some (a, update a i x h)" |
268 "i \<ge> length a h \<Longrightarrow> execute (upd i x a) h = None" |
267 "i \<ge> length a h \<Longrightarrow> execute (upd i x a) h = None" |
269 by (simp_all add: upd_def execute_simps) |
268 by (simp_all add: upd_def execute_simps) |
270 |
269 |
271 lemma success_updI [success_intros]: |
270 lemma success_updI [success_intros]: |
272 "i < length a h \<Longrightarrow> success (upd i x a) h" |
271 "i < length a h \<Longrightarrow> success (upd i x a) h" |
273 by (auto intro: success_intros simp add: upd_def) |
272 by (auto intro: success_intros simp add: upd_def) |
274 |
273 |
275 lemma crel_updI [crel_intros]: |
274 lemma crel_updI [crel_intros]: |
276 assumes "i < length a h" "h' = change a i v h" |
275 assumes "i < length a h" "h' = update a i v h" |
277 shows "crel (upd i v a) h h' a" |
276 shows "crel (upd i v a) h h' a" |
278 by (rule crelI) (insert assms, simp add: execute_simps) |
277 by (rule crelI) (insert assms, simp add: execute_simps) |
279 |
278 |
280 lemma crel_updE [crel_elims]: |
279 lemma crel_updE [crel_elims]: |
281 assumes "crel (upd i v a) h h' r" |
280 assumes "crel (upd i v a) h h' r" |
282 obtains "r = a" "h' = change a i v h" "i < length a h" |
281 obtains "r = a" "h' = update a i v h" "i < length a h" |
283 using assms by (rule crelE) |
282 using assms by (rule crelE) |
284 (erule successE, cases "i < length a h", simp_all add: execute_simps) |
283 (erule successE, cases "i < length a h", simp_all add: execute_simps) |
285 |
284 |
286 lemma execute_map_entry [execute_simps]: |
285 lemma execute_map_entry [execute_simps]: |
287 "i < length a h \<Longrightarrow> |
286 "i < length a h \<Longrightarrow> |
288 execute (map_entry i f a) h = |
287 execute (map_entry i f a) h = |
289 Some (a, change a i (f (get_array a h ! i)) h)" |
288 Some (a, update a i (f (get_array a h ! i)) h)" |
290 "i \<ge> length a h \<Longrightarrow> execute (map_entry i f a) h = None" |
289 "i \<ge> length a h \<Longrightarrow> execute (map_entry i f a) h = None" |
291 by (simp_all add: map_entry_def execute_simps) |
290 by (simp_all add: map_entry_def execute_simps) |
292 |
291 |
293 lemma success_map_entryI [success_intros]: |
292 lemma success_map_entryI [success_intros]: |
294 "i < length a h \<Longrightarrow> success (map_entry i f a) h" |
293 "i < length a h \<Longrightarrow> success (map_entry i f a) h" |
295 by (auto intro: success_intros simp add: map_entry_def) |
294 by (auto intro: success_intros simp add: map_entry_def) |
296 |
295 |
297 lemma crel_map_entryI [crel_intros]: |
296 lemma crel_map_entryI [crel_intros]: |
298 assumes "i < length a h" "h' = change a i (f (get_array a h ! i)) h" "r = a" |
297 assumes "i < length a h" "h' = update a i (f (get_array a h ! i)) h" "r = a" |
299 shows "crel (map_entry i f a) h h' r" |
298 shows "crel (map_entry i f a) h h' r" |
300 by (rule crelI) (insert assms, simp add: execute_simps) |
299 by (rule crelI) (insert assms, simp add: execute_simps) |
301 |
300 |
302 lemma crel_map_entryE [crel_elims]: |
301 lemma crel_map_entryE [crel_elims]: |
303 assumes "crel (map_entry i f a) h h' r" |
302 assumes "crel (map_entry i f a) h h' r" |
304 obtains "r = a" "h' = change a i (f (get_array a h ! i)) h" "i < length a h" |
303 obtains "r = a" "h' = update a i (f (get_array a h ! i)) h" "i < length a h" |
305 using assms by (rule crelE) |
304 using assms by (rule crelE) |
306 (erule successE, cases "i < length a h", simp_all add: execute_simps) |
305 (erule successE, cases "i < length a h", simp_all add: execute_simps) |
307 |
306 |
308 lemma execute_swap [execute_simps]: |
307 lemma execute_swap [execute_simps]: |
309 "i < length a h \<Longrightarrow> |
308 "i < length a h \<Longrightarrow> |
310 execute (swap i x a) h = |
309 execute (swap i x a) h = |
311 Some (get_array a h ! i, change a i x h)" |
310 Some (get_array a h ! i, update a i x h)" |
312 "i \<ge> length a h \<Longrightarrow> execute (swap i x a) h = None" |
311 "i \<ge> length a h \<Longrightarrow> execute (swap i x a) h = None" |
313 by (simp_all add: swap_def execute_simps) |
312 by (simp_all add: swap_def execute_simps) |
314 |
313 |
315 lemma success_swapI [success_intros]: |
314 lemma success_swapI [success_intros]: |
316 "i < length a h \<Longrightarrow> success (swap i x a) h" |
315 "i < length a h \<Longrightarrow> success (swap i x a) h" |
317 by (auto intro: success_intros simp add: swap_def) |
316 by (auto intro: success_intros simp add: swap_def) |
318 |
317 |
319 lemma crel_swapI [crel_intros]: |
318 lemma crel_swapI [crel_intros]: |
320 assumes "i < length a h" "h' = change a i x h" "r = get_array a h ! i" |
319 assumes "i < length a h" "h' = update a i x h" "r = get_array a h ! i" |
321 shows "crel (swap i x a) h h' r" |
320 shows "crel (swap i x a) h h' r" |
322 by (rule crelI) (insert assms, simp add: execute_simps) |
321 by (rule crelI) (insert assms, simp add: execute_simps) |
323 |
322 |
324 lemma crel_swapE [crel_elims]: |
323 lemma crel_swapE [crel_elims]: |
325 assumes "crel (swap i x a) h h' r" |
324 assumes "crel (swap i x a) h h' r" |
326 obtains "r = get_array a h ! i" "h' = change a i x h" "i < length a h" |
325 obtains "r = get_array a h ! i" "h' = update a i x h" "i < length a h" |
327 using assms by (rule crelE) |
326 using assms by (rule crelE) |
328 (erule successE, cases "i < length a h", simp_all add: execute_simps) |
327 (erule successE, cases "i < length a h", simp_all add: execute_simps) |
329 |
328 |
330 lemma execute_freeze [execute_simps]: |
329 lemma execute_freeze [execute_simps]: |
331 "execute (freeze a) h = Some (get_array a h, h)" |
330 "execute (freeze a) h = Some (get_array a h, h)" |
439 apply (subst execute_fold_map_unchanged_heap) |
438 apply (subst execute_fold_map_unchanged_heap) |
440 apply (simp_all add: nth_def guard_def *) |
439 apply (simp_all add: nth_def guard_def *) |
441 apply (simp add: length_def map_nth) |
440 apply (simp add: length_def map_nth) |
442 done |
441 done |
443 then have "execute (do |
442 then have "execute (do |
444 n \<leftarrow> len a; |
443 n \<leftarrow> Array.len a; |
445 Heap_Monad.fold_map (Array.nth a) [0..<n] |
444 Heap_Monad.fold_map (Array.nth a) [0..<n] |
446 done) h = Some (get_array a h, h)" |
445 done) h = Some (get_array a h, h)" |
447 by (auto intro: execute_bind_eq_SomeI simp add: execute_simps) |
446 by (auto intro: execute_bind_eq_SomeI simp add: execute_simps) |
448 then show "execute (freeze a) h = execute (do |
447 then show "execute (Array.freeze a) h = execute (do |
449 n \<leftarrow> len a; |
448 n \<leftarrow> Array.len a; |
450 Heap_Monad.fold_map (Array.nth a) [0..<n] |
449 Heap_Monad.fold_map (Array.nth a) [0..<n] |
451 done) h" by (simp add: execute_simps) |
450 done) h" by (simp add: execute_simps) |
452 qed |
451 qed |
453 |
452 |
454 hide_const (open) new' of_list' make' len' nth' upd' |
453 hide_const (open) new' of_list' make' len' nth' upd' |