author  wenzelm 
Fri, 12 Oct 2012 18:58:20 +0200  
changeset 49834  b27bbb021df1 
parent 45231  d85a2fdc586c 
child 49929  70300f1b6835 
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 

49834  11 
typedef ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set" 
37700
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 
lemma Mapping_inject [simp]: 
bd90378b8171
refrain from using datatype declaration  opens chance for quickcheck later on
haftmann
parents:
37299
diff
changeset

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

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

25 

39380
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset

26 
lemma mapping_eq_iff: 
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset

27 
"m = n \<longleftrightarrow> lookup m = lookup n" 
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset

28 
by (simp add: lookup_inject) 
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset

29 

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

30 
lemma mapping_eqI: 
39380
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset

31 
"lookup m = lookup n \<Longrightarrow> m = n" 
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset

32 
by (simp add: mapping_eq_iff) 
29708  33 

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

29708  36 

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

37 
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

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

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

40 
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

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

43 

40605  44 
subsection {* Functorial structure *} 
45 

46 
definition map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('c, 'd) mapping" where 

47 
"map f g m = Mapping (Option.map g \<circ> lookup m \<circ> f)" 

48 

49 
lemma lookup_map [simp]: 

50 
"lookup (map f g m) = Option.map g \<circ> lookup m \<circ> f" 

51 
by (simp add: map_def) 

52 

41505
6d19301074cf
"enriched_type" replaces less specific "type_lifting"
haftmann
parents:
41372
diff
changeset

53 
enriched_type map: map 
41372  54 
by (simp_all add: mapping_eq_iff fun_eq_iff Option.map.compositionality Option.map.id) 
40605  55 

56 

29708  57 
subsection {* Derived operations *} 
58 

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

29708  61 

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

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

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

37052  69 
"size m = (if finite (keys m) then card (keys m) else 0)" 
35157  70 

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

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

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

74 
definition default :: "'a \<Rightarrow> 'b \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where 
37052  75 
"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

76 

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

77 
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

78 
"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

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

80 

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

81 
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

82 
"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

83 

35157  84 
definition tabulate :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping" where 
40605  85 
"tabulate ks f = Mapping (map_of (List.map (\<lambda>k. (k, f k)) ks))" 
29708  86 

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

29826  89 

29708  90 

91 
subsection {* Properties *} 

92 

45231
d85a2fdc586c
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
bulwahn
parents:
41505
diff
changeset

93 
lemma keys_is_none_lookup [code_unfold]: 
37052  94 
"k \<in> keys m \<longleftrightarrow> \<not> (Option.is_none (lookup m k))" 
95 
by (auto simp add: keys_def is_none_def) 

96 

29708  97 
lemma lookup_empty [simp]: 
98 
"lookup empty = Map.empty" 

99 
by (simp add: empty_def) 

100 

101 
lemma lookup_update [simp]: 

102 
"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

103 
by (simp add: update_def) 
29708  104 

35157  105 
lemma lookup_delete [simp]: 
106 
"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

107 
by (simp add: delete_def) 
29708  108 

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

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

110 
"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

111 
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

112 

35157  113 
lemma lookup_tabulate [simp]: 
29708  114 
"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

115 
by (induct ks) (auto simp add: tabulate_def restrict_map_def fun_eq_iff) 
29708  116 

35157  117 
lemma lookup_bulkload [simp]: 
29826  118 
"lookup (bulkload xs) = (\<lambda>k. if k < length xs then Some (xs ! k) else None)" 
35157  119 
by (simp add: bulkload_def) 
29826  120 

29708  121 
lemma update_update: 
122 
"update k v (update k w m) = update k v m" 

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

35157  124 
by (rule mapping_eqI, simp add: fun_upd_twist)+ 
29708  125 

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

128 
by (rule mapping_eqI) simp 

29708  129 

130 
lemma delete_update: 

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

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

35157  133 
by (rule mapping_eqI, simp add: fun_upd_twist)+ 
29708  134 

35157  135 
lemma delete_empty [simp]: 
136 
"delete k empty = empty" 

137 
by (rule mapping_eqI) simp 

29708  138 

35157  139 
lemma replace_update: 
37052  140 
"k \<notin> keys m \<Longrightarrow> replace k v m = m" 
141 
"k \<in> keys m \<Longrightarrow> replace k v m = update k v m" 

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

29708  143 

144 
lemma size_empty [simp]: 

145 
"size empty = 0" 

37052  146 
by (simp add: size_def keys_def) 
29708  147 

148 
lemma size_update: 

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

151 
by (auto simp add: size_def insert_dom keys_def) 

29708  152 

153 
lemma size_delete: 

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

29708  156 

37052  157 
lemma size_tabulate [simp]: 
29708  158 
"size (tabulate ks f) = length (remdups ks)" 
37052  159 
by (simp add: size_def distinct_card [of "remdups ks", symmetric] comp_def keys_def) 
29708  160 

29831  161 
lemma bulkload_tabulate: 
29826  162 
"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

163 
by (rule mapping_eqI) (simp add: fun_eq_iff) 
29826  164 

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

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

168 

169 
lemma is_empty_empty' [simp]: 

170 
"is_empty empty" 

171 
by (simp add: is_empty_empty empty_def) 

172 

173 
lemma is_empty_update [simp]: 

174 
"\<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

175 
by (simp add: is_empty_empty update_def) 
37052  176 

177 
lemma is_empty_delete: 

178 
"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

179 
by (auto simp add: delete_def is_empty_def keys_def simp del: dom_eq_empty_conv) 
37052  180 

181 
lemma is_empty_replace [simp]: 

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

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

184 

185 
lemma is_empty_default [simp]: 

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

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

188 

189 
lemma is_empty_map_entry [simp]: 

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

191 
by (cases "lookup m k") 

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

193 

194 
lemma is_empty_map_default [simp]: 

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

196 
by (simp add: map_default_def) 

197 

198 
lemma keys_empty [simp]: 

199 
"keys empty = {}" 

200 
by (simp add: keys_def) 

201 

202 
lemma keys_update [simp]: 

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

204 
by (simp add: keys_def) 

205 

206 
lemma keys_delete [simp]: 

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

208 
by (simp add: keys_def) 

209 

210 
lemma keys_replace [simp]: 

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

212 
by (auto simp add: keys_def replace_def) 

213 

214 
lemma keys_default [simp]: 

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

216 
by (auto simp add: keys_def default_def) 

217 

218 
lemma keys_map_entry [simp]: 

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

220 
by (auto simp add: keys_def) 

221 

222 
lemma keys_map_default [simp]: 

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

224 
by (simp add: map_default_def) 

225 

226 
lemma keys_tabulate [simp]: 

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

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

228 
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

229 

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

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

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

233 

37052  234 
lemma distinct_ordered_keys [simp]: 
235 
"distinct (ordered_keys m)" 

236 
by (simp add: ordered_keys_def) 

237 

238 
lemma ordered_keys_infinite [simp]: 

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

240 
by (simp add: ordered_keys_def) 

241 

242 
lemma ordered_keys_empty [simp]: 

243 
"ordered_keys empty = []" 

244 
by (simp add: ordered_keys_def) 

245 

246 
lemma ordered_keys_update [simp]: 

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

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

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

250 

251 
lemma ordered_keys_delete [simp]: 

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

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

254 
case False then show ?thesis by simp 

255 
next 

256 
case True note fin = True 

257 
show ?thesis 

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

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

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

261 
next 

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

263 
qed 

264 
qed 

265 

266 
lemma ordered_keys_replace [simp]: 

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

268 
by (simp add: replace_def) 

269 

270 
lemma ordered_keys_default [simp]: 

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

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

273 
by (simp_all add: default_def) 

274 

275 
lemma ordered_keys_map_entry [simp]: 

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

277 
by (simp add: ordered_keys_def) 

278 

279 
lemma ordered_keys_map_default [simp]: 

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

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

282 
by (simp_all add: map_default_def) 

283 

284 
lemma ordered_keys_tabulate [simp]: 

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

286 
by (simp add: ordered_keys_def sorted_list_of_set_sort_remdups) 

287 

288 
lemma ordered_keys_bulkload [simp]: 

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

290 
by (simp add: ordered_keys_def) 

36110  291 

31459  292 

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

293 
subsection {* Code generator setup *} 
31459  294 

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

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

296 

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

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

298 
begin 
31459  299 

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

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

301 
"HOL.equal m n \<longleftrightarrow> lookup m = lookup n" 
31459  302 

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

303 
instance proof 
39380
5a2662c1e44a
established emerging canonical names *_eqI and *_eq_iff
haftmann
parents:
39302
diff
changeset

304 
qed (simp add: equal_mapping_def mapping_eq_iff) 
31459  305 

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

306 
end 
31459  307 

35157  308 

37299  309 
hide_const (open) empty is_empty lookup update delete ordered_keys keys size 
40605  310 
replace default map_entry map_default tabulate bulkload map 
35157  311 

29708  312 
end 