author  nipkow 
Mon, 13 Sep 2010 11:13:15 +0200  
changeset 39302  d7728f65b353 
parent 39198  f967a16dfcdd 
child 39380  5a2662c1e44a 
permissions  rwrr 
31459  1 
(* Author: Florian Haftmann, TU Muenchen *) 
29708  2 

3 
header {* An abstract view on maps for code generation. *} 

4 

5 
theory Mapping 

35157  6 
imports Main 
29708  7 
begin 
8 

9 
subsection {* Type definition and primitive operations *} 

10 

37700
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

11 
typedef (open) ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set" 
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

12 
morphisms lookup Mapping .. 
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

13 

bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

14 
lemma lookup_Mapping [simp]: 
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

15 
"lookup (Mapping f) = f" 
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

16 
by (rule Mapping_inverse) rule 
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

17 

bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

18 
lemma Mapping_lookup [simp]: 
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

19 
"Mapping (lookup m) = m" 
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

20 
by (fact lookup_inverse) 
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

21 

bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

22 
declare lookup_inject [simp] 
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

23 

bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

24 
lemma Mapping_inject [simp]: 
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

25 
"Mapping f = Mapping g \<longleftrightarrow> f = g" 
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

26 
by (simp add: Mapping_inject) 
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

27 

bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

28 
lemma mapping_eqI: 
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

29 
assumes "lookup m = lookup n" 
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

30 
shows "m = n" 
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

31 
using assms by simp 
29708  32 

35157  33 
definition empty :: "('a, 'b) mapping" where 
34 
"empty = Mapping (\<lambda>_. None)" 

29708  35 

37700
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

36 
definition update :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where 
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

37 
"update k v m = Mapping ((lookup m)(k \<mapsto> v))" 
29708  38 

37700
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

39 
definition delete :: "'a \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where 
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

40 
"delete k m = Mapping ((lookup m)(k := None))" 
29708  41 

42 

43 
subsection {* Derived operations *} 

44 

35157  45 
definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set" where 
46 
"keys m = dom (lookup m)" 

29708  47 

35194  48 
definition ordered_keys :: "('a\<Colon>linorder, 'b) mapping \<Rightarrow> 'a list" where 
37052  49 
"ordered_keys m = (if finite (keys m) then sorted_list_of_set (keys m) else [])" 
35194  50 

35157  51 
definition is_empty :: "('a, 'b) mapping \<Rightarrow> bool" where 
37052  52 
"is_empty m \<longleftrightarrow> keys m = {}" 
35157  53 

54 
definition size :: "('a, 'b) mapping \<Rightarrow> nat" where 

37052  55 
"size m = (if finite (keys m) then card (keys m) else 0)" 
35157  56 

57 
definition replace :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where 

37052  58 
"replace k v m = (if k \<in> keys m then update k v m else m)" 
29814  59 

37026
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

60 
definition default :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where 
37052  61 
"default k v m = (if k \<in> keys m then m else update k v m)" 
37026
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

62 

7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

63 
definition map_entry :: "'a \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where 
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

64 
"map_entry k f m = (case lookup m k of None \<Rightarrow> m 
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

65 
 Some v \<Rightarrow> update k (f v) m)" 
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

66 

7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

67 
definition map_default :: "'a \<Rightarrow> 'b \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where 
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

68 
"map_default k v f m = map_entry k f (default k v m)" 
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

69 

35157  70 
definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping" where 
71 
"tabulate ks f = Mapping (map_of (map (\<lambda>k. (k, f k)) ks))" 

29708  72 

35157  73 
definition bulkload :: "'a list \<Rightarrow> (nat, 'a) mapping" where 
74 
"bulkload xs = Mapping (\<lambda>k. if k < length xs then Some (xs ! k) else None)" 

29826  75 

29708  76 

77 
subsection {* Properties *} 

78 

37052  79 
lemma keys_is_none_lookup [code_inline]: 
80 
"k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))" 

81 
by (auto simp add: keys_def is_none_def) 

82 

29708  83 
lemma lookup_empty [simp]: 
84 
"lookup empty = Map.empty" 

85 
by (simp add: empty_def) 

86 

87 
lemma lookup_update [simp]: 

88 
"lookup (update k v m) = (lookup m) (k \<mapsto> v)" 

37700
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

89 
by (simp add: update_def) 
29708  90 

35157  91 
lemma lookup_delete [simp]: 
92 
"lookup (delete k m) = (lookup m) (k := None)" 

37700
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

93 
by (simp add: delete_def) 
29708  94 

37026
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

95 
lemma lookup_map_entry [simp]: 
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

96 
"lookup (map_entry k f m) = (lookup m) (k := Option.map f (lookup m k))" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

97 
by (cases "lookup m k") (simp_all add: map_entry_def fun_eq_iff) 
37026
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

98 

35157  99 
lemma lookup_tabulate [simp]: 
29708  100 
"lookup (tabulate ks f) = (Some o f) ` set ks" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

101 
by (induct ks) (auto simp add: tabulate_def restrict_map_def fun_eq_iff) 
29708  102 

35157  103 
lemma lookup_bulkload [simp]: 
29826  104 
"lookup (bulkload xs) = (\<lambda>k. if k < length xs then Some (xs ! k) else None)" 
35157  105 
by (simp add: bulkload_def) 
29826  106 

29708  107 
lemma update_update: 
108 
"update k v (update k w m) = update k v m" 

109 
"k \<noteq> l \<Longrightarrow> update k v (update l w m) = update l w (update k v m)" 

35157  110 
by (rule mapping_eqI, simp add: fun_upd_twist)+ 
29708  111 

35157  112 
lemma update_delete [simp]: 
113 
"update k v (delete k m) = update k v m" 

114 
by (rule mapping_eqI) simp 

29708  115 

116 
lemma delete_update: 

117 
"delete k (update k v m) = delete k m" 

118 
"k \<noteq> l \<Longrightarrow> delete k (update l v m) = update l v (delete k m)" 

35157  119 
by (rule mapping_eqI, simp add: fun_upd_twist)+ 
29708  120 

35157  121 
lemma delete_empty [simp]: 
122 
"delete k empty = empty" 

123 
by (rule mapping_eqI) simp 

29708  124 

35157  125 
lemma replace_update: 
37052  126 
"k \<notin> keys m \<Longrightarrow> replace k v m = m" 
127 
"k \<in> keys m \<Longrightarrow> replace k v m = update k v m" 

128 
by (rule mapping_eqI) (auto simp add: replace_def fun_upd_twist)+ 

29708  129 

130 
lemma size_empty [simp]: 

131 
"size empty = 0" 

37052  132 
by (simp add: size_def keys_def) 
29708  133 

134 
lemma size_update: 

37052  135 
"finite (keys m) \<Longrightarrow> size (update k v m) = 
136 
(if k \<in> keys m then size m else Suc (size m))" 

137 
by (auto simp add: size_def insert_dom keys_def) 

29708  138 

139 
lemma size_delete: 

37052  140 
"size (delete k m) = (if k \<in> keys m then size m  1 else size m)" 
141 
by (simp add: size_def keys_def) 

29708  142 

37052  143 
lemma size_tabulate [simp]: 
29708  144 
"size (tabulate ks f) = length (remdups ks)" 
37052  145 
by (simp add: size_def distinct_card [of "remdups ks", symmetric] comp_def keys_def) 
29708  146 

29831  147 
lemma bulkload_tabulate: 
29826  148 
"bulkload xs = tabulate [0..<length xs] (nth xs)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

149 
by (rule mapping_eqI) (simp add: fun_eq_iff) 
29826  150 

37052  151 
lemma is_empty_empty: (*FIXME*) 
152 
"is_empty m \<longleftrightarrow> m = Mapping Map.empty" 

153 
by (cases m) (simp add: is_empty_def keys_def) 

154 

155 
lemma is_empty_empty' [simp]: 

156 
"is_empty empty" 

157 
by (simp add: is_empty_empty empty_def) 

158 

159 
lemma is_empty_update [simp]: 

160 
"\<not> is_empty (update k v m)" 

37700
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

161 
by (simp add: is_empty_empty update_def) 
37052  162 

163 
lemma is_empty_delete: 

164 
"is_empty (delete k m) \<longleftrightarrow> is_empty m \<or> keys m = {k}" 

37700
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

165 
by (auto simp add: delete_def is_empty_def keys_def simp del: dom_eq_empty_conv) 
37052  166 

167 
lemma is_empty_replace [simp]: 

168 
"is_empty (replace k v m) \<longleftrightarrow> is_empty m" 

169 
by (auto simp add: replace_def) (simp add: is_empty_def) 

170 

171 
lemma is_empty_default [simp]: 

172 
"\<not> is_empty (default k v m)" 

173 
by (auto simp add: default_def) (simp add: is_empty_def) 

174 

175 
lemma is_empty_map_entry [simp]: 

176 
"is_empty (map_entry k f m) \<longleftrightarrow> is_empty m" 

177 
by (cases "lookup m k") 

178 
(auto simp add: map_entry_def, simp add: is_empty_empty) 

179 

180 
lemma is_empty_map_default [simp]: 

181 
"\<not> is_empty (map_default k v f m)" 

182 
by (simp add: map_default_def) 

183 

184 
lemma keys_empty [simp]: 

185 
"keys empty = {}" 

186 
by (simp add: keys_def) 

187 

188 
lemma keys_update [simp]: 

189 
"keys (update k v m) = insert k (keys m)" 

190 
by (simp add: keys_def) 

191 

192 
lemma keys_delete [simp]: 

193 
"keys (delete k m) = keys m  {k}" 

194 
by (simp add: keys_def) 

195 

196 
lemma keys_replace [simp]: 

197 
"keys (replace k v m) = keys m" 

198 
by (auto simp add: keys_def replace_def) 

199 

200 
lemma keys_default [simp]: 

201 
"keys (default k v m) = insert k (keys m)" 

202 
by (auto simp add: keys_def default_def) 

203 

204 
lemma keys_map_entry [simp]: 

205 
"keys (map_entry k f m) = keys m" 

206 
by (auto simp add: keys_def) 

207 

208 
lemma keys_map_default [simp]: 

209 
"keys (map_default k v f m) = insert k (keys m)" 

210 
by (simp add: map_default_def) 

211 

212 
lemma keys_tabulate [simp]: 

37026
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

213 
"keys (tabulate ks f) = set ks" 
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

214 
by (simp add: tabulate_def keys_def map_of_map_restrict o_def) 
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

215 

37052  216 
lemma keys_bulkload [simp]: 
37026
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

217 
"keys (bulkload xs) = {0..<length xs}" 
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

218 
by (simp add: keys_tabulate bulkload_tabulate) 
7e8979a155ae
operations default, map_entry, map_default; more lemmas
haftmann
parents:
36176
diff
changeset

219 

37052  220 
lemma distinct_ordered_keys [simp]: 
221 
"distinct (ordered_keys m)" 

222 
by (simp add: ordered_keys_def) 

223 

224 
lemma ordered_keys_infinite [simp]: 

225 
"\<not> finite (keys m) \<Longrightarrow> ordered_keys m = []" 

226 
by (simp add: ordered_keys_def) 

227 

228 
lemma ordered_keys_empty [simp]: 

229 
"ordered_keys empty = []" 

230 
by (simp add: ordered_keys_def) 

231 

232 
lemma ordered_keys_update [simp]: 

233 
"k \<in> keys m \<Longrightarrow> ordered_keys (update k v m) = ordered_keys m" 

234 
"finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (update k v m) = insort k (ordered_keys m)" 

235 
by (simp_all add: ordered_keys_def) (auto simp only: sorted_list_of_set_insert [symmetric] insert_absorb) 

236 

237 
lemma ordered_keys_delete [simp]: 

238 
"ordered_keys (delete k m) = remove1 k (ordered_keys m)" 

239 
proof (cases "finite (keys m)") 

240 
case False then show ?thesis by simp 

241 
next 

242 
case True note fin = True 

243 
show ?thesis 

244 
proof (cases "k \<in> keys m") 

245 
case False with fin have "k \<notin> set (sorted_list_of_set (keys m))" by simp 

246 
with False show ?thesis by (simp add: ordered_keys_def remove1_idem) 

247 
next 

248 
case True with fin show ?thesis by (simp add: ordered_keys_def sorted_list_of_set_remove) 

249 
qed 

250 
qed 

251 

252 
lemma ordered_keys_replace [simp]: 

253 
"ordered_keys (replace k v m) = ordered_keys m" 

254 
by (simp add: replace_def) 

255 

256 
lemma ordered_keys_default [simp]: 

257 
"k \<in> keys m \<Longrightarrow> ordered_keys (default k v m) = ordered_keys m" 

258 
"finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (default k v m) = insort k (ordered_keys m)" 

259 
by (simp_all add: default_def) 

260 

261 
lemma ordered_keys_map_entry [simp]: 

262 
"ordered_keys (map_entry k f m) = ordered_keys m" 

263 
by (simp add: ordered_keys_def) 

264 

265 
lemma ordered_keys_map_default [simp]: 

266 
"k \<in> keys m \<Longrightarrow> ordered_keys (map_default k v f m) = ordered_keys m" 

267 
"finite (keys m) \<Longrightarrow> k \<notin> keys m \<Longrightarrow> ordered_keys (map_default k v f m) = insort k (ordered_keys m)" 

268 
by (simp_all add: map_default_def) 

269 

270 
lemma ordered_keys_tabulate [simp]: 

271 
"ordered_keys (tabulate ks f) = sort (remdups ks)" 

272 
by (simp add: ordered_keys_def sorted_list_of_set_sort_remdups) 

273 

274 
lemma ordered_keys_bulkload [simp]: 

275 
"ordered_keys (bulkload ks) = [0..<length ks]" 

276 
by (simp add: ordered_keys_def) 

36110  277 

31459  278 

37700
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

279 
subsection {* Code generator setup *} 
31459  280 

37701
411717732710
explicit code_datatype declaration prevents multiple instantiations later on
haftmann
parents:
37700
diff
changeset

281 
code_datatype empty update 
411717732710
explicit code_datatype declaration prevents multiple instantiations later on
haftmann
parents:
37700
diff
changeset

282 

38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37701
diff
changeset

283 
instantiation mapping :: (type, type) equal 
37700
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

284 
begin 
31459  285 

37700
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

286 
definition [code del]: 
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37701
diff
changeset

287 
"HOL.equal m n \<longleftrightarrow> lookup m = lookup n" 
31459  288 

37700
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

289 
instance proof 
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
37701
diff
changeset

290 
qed (simp add: equal_mapping_def) 
31459  291 

37700
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

292 
end 
31459  293 

35157  294 

37299  295 
hide_const (open) empty is_empty lookup update delete ordered_keys keys size 
296 
replace default map_entry map_default tabulate bulkload 

35157  297 

29708  298 
end 