|
1 (* Title: HOL/Library/Array.thy |
|
2 ID: $Id$ |
|
3 Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Monadic arrays *} |
|
7 |
|
8 theory Array |
|
9 imports Heap_Monad |
|
10 begin |
|
11 |
|
12 subsection {* Primitives *} |
|
13 |
|
14 definition |
|
15 new :: "nat \<Rightarrow> 'a\<Colon>heap \<Rightarrow> 'a array Heap" where |
|
16 [code del]: "new n x = Heap_Monad.heap (Heap.array n x)" |
|
17 |
|
18 definition |
|
19 of_list :: "'a\<Colon>heap list \<Rightarrow> 'a array Heap" where |
|
20 [code del]: "of_list xs = Heap_Monad.heap (Heap.array_of_list xs)" |
|
21 |
|
22 definition |
|
23 length :: "'a\<Colon>heap array \<Rightarrow> nat Heap" where |
|
24 [code del]: "length arr = Heap_Monad.heap (\<lambda>h. (Heap.length arr h, h))" |
|
25 |
|
26 definition |
|
27 nth :: "'a\<Colon>heap array \<Rightarrow> nat \<Rightarrow> 'a Heap" |
|
28 where |
|
29 [code del]: "nth a i = (do len \<leftarrow> length a; |
|
30 (if i < len |
|
31 then Heap_Monad.heap (\<lambda>h. (get_array a h ! i, h)) |
|
32 else raise (''array lookup: index out of range'')) |
|
33 done)" |
|
34 |
|
35 -- {* FIXME adjustion for List theory *} |
|
36 no_syntax |
|
37 nth :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!" 100) |
|
38 |
|
39 abbreviation |
|
40 nth_list :: "'a list \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!" 100) |
|
41 where |
|
42 "nth_list \<equiv> List.nth" |
|
43 |
|
44 definition |
|
45 upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap" |
|
46 where |
|
47 [code del]: "upd i x a = (do len \<leftarrow> length a; |
|
48 (if i < len |
|
49 then Heap_Monad.heap (\<lambda>h. ((), Heap.upd a i x h)) |
|
50 else raise (''array update: index out of range'')); |
|
51 return a |
|
52 done)" |
|
53 |
|
54 lemma upd_return: |
|
55 "upd i x a \<guillemotright> return a = upd i x a" |
|
56 unfolding upd_def by (simp add: monad_simp) |
|
57 |
|
58 |
|
59 subsection {* Derivates *} |
|
60 |
|
61 definition |
|
62 map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" |
|
63 where |
|
64 "map_entry i f a = (do |
|
65 x \<leftarrow> nth a i; |
|
66 upd i (f x) a |
|
67 done)" |
|
68 |
|
69 definition |
|
70 swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap" |
|
71 where |
|
72 "swap i x a = (do |
|
73 y \<leftarrow> nth a i; |
|
74 upd i x a; |
|
75 return x |
|
76 done)" |
|
77 |
|
78 definition |
|
79 make :: "nat \<Rightarrow> (nat \<Rightarrow> 'a\<Colon>heap) \<Rightarrow> 'a array Heap" |
|
80 where |
|
81 "make n f = of_list (map f [0 ..< n])" |
|
82 |
|
83 definition |
|
84 freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" |
|
85 where |
|
86 "freeze a = (do |
|
87 n \<leftarrow> length a; |
|
88 mapM (nth a) [0..<n] |
|
89 done)" |
|
90 |
|
91 definition |
|
92 map :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" |
|
93 where |
|
94 "map f a = (do |
|
95 n \<leftarrow> length a; |
|
96 foldM (\<lambda>n. map_entry n f) [0..<n] a |
|
97 done)" |
|
98 |
|
99 hide (open) const new map -- {* avoid clashed with some popular names *} |
|
100 |
|
101 |
|
102 subsection {* Converting arrays to lists *} |
|
103 |
|
104 primrec list_of_aux :: "nat \<Rightarrow> ('a\<Colon>heap) array \<Rightarrow> 'a list \<Rightarrow> 'a list Heap" where |
|
105 "list_of_aux 0 a xs = return xs" |
|
106 | "list_of_aux (Suc n) a xs = (do |
|
107 x \<leftarrow> Array.nth a n; |
|
108 list_of_aux n a (x#xs) |
|
109 done)" |
|
110 |
|
111 definition list_of :: "('a\<Colon>heap) array \<Rightarrow> 'a list Heap" where |
|
112 "list_of a = (do n \<leftarrow> Array.length a; |
|
113 list_of_aux n a [] |
|
114 done)" |
|
115 |
|
116 |
|
117 subsection {* Properties *} |
|
118 |
|
119 lemma array_make [code func]: |
|
120 "Array.new n x = make n (\<lambda>_. x)" |
|
121 by (induct n) (simp_all add: make_def new_def Heap_Monad.heap_def |
|
122 monad_simp array_of_list_replicate [symmetric] |
|
123 map_replicate_trivial replicate_append_same |
|
124 of_list_def) |
|
125 |
|
126 lemma array_of_list_make [code func]: |
|
127 "of_list xs = make (List.length xs) (\<lambda>n. xs ! n)" |
|
128 unfolding make_def map_nth .. |
|
129 |
|
130 end |