author  haftmann 
Tue, 19 May 2009 16:54:55 +0200  
changeset 31205  98370b26c2ce 
parent 31203  5c8fb4fd67e0 
child 31870  5274d3d0a6f2 
permissions  rwrr 
26170  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 

31203
5c8fb4fd67e0
moved Code_Index, Random and Quickcheck before Main
haftmann
parents:
29822
diff
changeset

9 
imports Heap_Monad 
26170  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 
definition 

36 
upd :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a\<Colon>heap array Heap" 

37 
where 

38 
[code del]: "upd i x a = (do len \<leftarrow> length a; 

39 
(if i < len 

26719  40 
then Heap_Monad.heap (\<lambda>h. (a, Heap.upd a i x h)) 
41 
else raise (''array update: index out of range'')) 

26170  42 
done)" 
43 

44 
lemma upd_return: 

45 
"upd i x a \<guillemotright> return a = upd i x a" 

26719  46 
proof (rule Heap_eqI) 
47 
fix h 

48 
obtain len h' where "Heap_Monad.execute (Array.length a) h = (len, h')" 

49 
by (cases "Heap_Monad.execute (Array.length a) h") 

50 
then show "Heap_Monad.execute (upd i x a \<guillemotright> return a) h = Heap_Monad.execute (upd i x a) h" 

28145  51 
by (auto simp add: upd_def bindM_def split: sum.split) 
26719  52 
qed 
26170  53 

54 

55 
subsection {* Derivates *} 

56 

57 
definition 

58 
map_entry :: "nat \<Rightarrow> ('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" 

59 
where 

60 
"map_entry i f a = (do 

61 
x \<leftarrow> nth a i; 

62 
upd i (f x) a 

63 
done)" 

64 

65 
definition 

66 
swap :: "nat \<Rightarrow> 'a \<Rightarrow> 'a\<Colon>heap array \<Rightarrow> 'a Heap" 

67 
where 

68 
"swap i x a = (do 

69 
y \<leftarrow> nth a i; 

70 
upd i x a; 

27596  71 
return y 
26170  72 
done)" 
73 

74 
definition 

75 
make :: "nat \<Rightarrow> (nat \<Rightarrow> 'a\<Colon>heap) \<Rightarrow> 'a array Heap" 

76 
where 

77 
"make n f = of_list (map f [0 ..< n])" 

78 

79 
definition 

80 
freeze :: "'a\<Colon>heap array \<Rightarrow> 'a list Heap" 

81 
where 

82 
"freeze a = (do 

83 
n \<leftarrow> length a; 

84 
mapM (nth a) [0..<n] 

85 
done)" 

86 

27656
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset

87 
definition 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset

88 
map :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset

89 
where 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset

90 
"map f a = (do 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset

91 
n \<leftarrow> length a; 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset

92 
mapM (\<lambda>n. map_entry n f a) [0..<n]; 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset

93 
return a 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset

94 
done)" 
d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset

95 

d4f6e64ee7cc
added verification framework for the HeapMonad and quicksort as example for this framework
bulwahn
parents:
27596
diff
changeset

96 
hide (open) const new map  {* avoid clashed with some popular names *} 
26170  97 

98 

99 
subsection {* Properties *} 

100 

28562  101 
lemma array_make [code]: 
26170  102 
"Array.new n x = make n (\<lambda>_. x)" 
103 
by (induct n) (simp_all add: make_def new_def Heap_Monad.heap_def 

104 
monad_simp array_of_list_replicate [symmetric] 

105 
map_replicate_trivial replicate_append_same 

106 
of_list_def) 

107 

28562  108 
lemma array_of_list_make [code]: 
26170  109 
"of_list xs = make (List.length xs) (\<lambda>n. xs ! n)" 
110 
unfolding make_def map_nth .. 

111 

26182  112 

113 
subsection {* Code generator setup *} 

114 

115 
subsubsection {* Logical intermediate layer *} 

116 

117 
definition new' where 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

118 
[code del]: "new' = Array.new o Code_Numeral.nat_of" 
26182  119 
hide (open) const new' 
28562  120 
lemma [code]: 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

121 
"Array.new = Array.new' o Code_Numeral.of_nat" 
26182  122 
by (simp add: new'_def o_def) 
123 

124 
definition of_list' where 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

125 
[code del]: "of_list' i xs = Array.of_list (take (Code_Numeral.nat_of i) xs)" 
26182  126 
hide (open) const of_list' 
28562  127 
lemma [code]: 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

128 
"Array.of_list xs = Array.of_list' (Code_Numeral.of_nat (List.length xs)) xs" 
26182  129 
by (simp add: of_list'_def) 
130 

131 
definition make' where 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

132 
[code del]: "make' i f = Array.make (Code_Numeral.nat_of i) (f o Code_Numeral.of_nat)" 
26182  133 
hide (open) const make' 
28562  134 
lemma [code]: 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

135 
"Array.make n f = Array.make' (Code_Numeral.of_nat n) (f o Code_Numeral.nat_of)" 
26182  136 
by (simp add: make'_def o_def) 
137 

138 
definition length' where 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

139 
[code del]: "length' = Array.length \<guillemotright>== liftM Code_Numeral.of_nat" 
26182  140 
hide (open) const length' 
28562  141 
lemma [code]: 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

142 
"Array.length = Array.length' \<guillemotright>== liftM Code_Numeral.nat_of" 
26182  143 
by (simp add: length'_def monad_simp', 
144 
simp add: liftM_def comp_def monad_simp, 

145 
simp add: monad_simp') 

146 

147 
definition nth' where 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

148 
[code del]: "nth' a = Array.nth a o Code_Numeral.nat_of" 
26182  149 
hide (open) const nth' 
28562  150 
lemma [code]: 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

151 
"Array.nth a n = Array.nth' a (Code_Numeral.of_nat n)" 
26182  152 
by (simp add: nth'_def) 
153 

154 
definition upd' where 

31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

155 
[code del]: "upd' a i x = Array.upd (Code_Numeral.nat_of i) x a \<guillemotright> return ()" 
26182  156 
hide (open) const upd' 
28562  157 
lemma [code]: 
31205
98370b26c2ce
String.literal replaces message_string, code_numeral replaces (code_)index
haftmann
parents:
31203
diff
changeset

158 
"Array.upd i x a = Array.upd' a (Code_Numeral.of_nat i) x \<guillemotright> return a" 
26743  159 
by (simp add: upd'_def monad_simp upd_return) 
26182  160 

161 

162 
subsubsection {* SML *} 

163 

164 
code_type array (SML "_/ array") 

165 
code_const Array (SML "raise/ (Fail/ \"bare Array\")") 

26752  166 
code_const Array.new' (SML "(fn/ ()/ =>/ Array.array/ ((_),/ (_)))") 
167 
code_const Array.of_list (SML "(fn/ ()/ =>/ Array.fromList/ _)") 

168 
code_const Array.make' (SML "(fn/ ()/ =>/ Array.tabulate/ ((_),/ (_)))") 

169 
code_const Array.length' (SML "(fn/ ()/ =>/ Array.length/ _)") 

170 
code_const Array.nth' (SML "(fn/ ()/ =>/ Array.sub/ ((_),/ (_)))") 

171 
code_const Array.upd' (SML "(fn/ ()/ =>/ Array.update/ ((_),/ (_),/ (_)))") 

26182  172 

173 
code_reserved SML Array 

174 

175 

176 
subsubsection {* OCaml *} 

177 

178 
code_type array (OCaml "_/ array") 

179 
code_const Array (OCaml "failwith/ \"bare Array\"") 

27673  180 
code_const Array.new' (OCaml "(fun/ ()/ >/ Array.make/ _/ _)") 
181 
code_const Array.of_list (OCaml "(fun/ ()/ >/ Array.of'_list/ _)") 

182 
code_const Array.make' (OCaml "(fun/ ()/ >/ Array.init/ _/ _)") 

183 
code_const Array.length' (OCaml "(fun/ ()/ >/ Array.length/ _)") 

184 
code_const Array.nth' (OCaml "(fun/ ()/ >/ Array.get/ _/ _)") 

185 
code_const Array.upd' (OCaml "(fun/ ()/ >/ Array.set/ _/ _/ _)") 

26182  186 

187 
code_reserved OCaml Array 

188 

189 

190 
subsubsection {* Haskell *} 

191 

29793  192 
code_type array (Haskell "Heap.STArray/ Heap.RealWorld/ _") 
26182  193 
code_const Array (Haskell "error/ \"bare Array\"") 
29793  194 
code_const Array.new' (Haskell "Heap.newArray/ (0,/ _)") 
195 
code_const Array.of_list' (Haskell "Heap.newListArray/ (0,/ _)") 

196 
code_const Array.length' (Haskell "Heap.lengthArray") 

197 
code_const Array.nth' (Haskell "Heap.readArray") 

198 
code_const Array.upd' (Haskell "Heap.writeArray") 

26182  199 

26170  200 
end 