author  webertj 
Fri, 11 Apr 2003 23:11:13 +0200  
changeset 13908  4bdfa9f77254 
parent 13890  90611b4e0054 
child 13909  a5247a49c85e 
permissions  rwrr 
3981  1 
(* Title: HOL/Map.thy 
2 
ID: $Id$ 

3 
Author: Tobias Nipkow, based on a theory by David von Oheimb 

13908  4 
Copyright 19972003 TU Muenchen 
3981  5 

6 
The datatype of `maps' (written ~=>); strongly resembles maps in VDM. 

7 
*) 

8 

13908  9 
theory Map = List: 
3981  10 

13908  11 
types ('a,'b) "~=>" = "'a => 'b option" (infixr 0) 
3981  12 

13 
consts 

5300  14 
chg_map :: "('b => 'b) => 'a => ('a ~=> 'b) => ('a ~=> 'b)" 
3981  15 
override:: "('a ~=> 'b) => ('a ~=> 'b) => ('a ~=> 'b)" (infixl "++" 100) 
5300  16 
dom :: "('a ~=> 'b) => 'a set" 
17 
ran :: "('a ~=> 'b) => 'b set" 

18 
map_of :: "('a * 'b)list => 'a ~=> 'b" 

19 
map_upds:: "('a ~=> 'b) => 'a list => 'b list => 

20 
('a ~=> 'b)" ("_/'(_[>]_/')" [900,0,0]900) 

21 
syntax 

13890  22 
empty :: "'a ~=> 'b" 
5300  23 
map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)" 
24 
("_/'(_/>_')" [900,0,0]900) 

3981  25 

12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
10137
diff
changeset

26 
syntax (xsymbols) 
13908  27 
"~=>" :: "[type, type] => type" (infixr "\<leadsto>" 0) 
5300  28 
map_upd :: "('a ~=> 'b) => 'a => 'b => ('a ~=> 'b)" 
13908  29 
("_/'(_/\<mapsto>/_')" [900,0,0]900) 
5300  30 
map_upds :: "('a ~=> 'b) => 'a list => 'b list => ('a ~=> 'b)" 
13908  31 
("_/'(_/[\<mapsto>]/_')" [900,0,0]900) 
5300  32 

33 
translations 

13890  34 
"empty" => "_K None" 
35 
"empty" <= "%x. None" 

5300  36 

37 
"m(a>b)" == "m(a:=Some b)" 

3981  38 

39 
defs 

40 

13908  41 
chg_map_def: "chg_map f a m == case m a of None => m  Some b => m(a>f b)" 
3981  42 

13908  43 
override_def: "m1++m2 == %x. case m2 x of None => m1 x  Some y => Some y" 
3981  44 

13908  45 
dom_def: "dom(m) == {a. m a ~= None}" 
46 
ran_def: "ran(m) == {b. ? a. m a = Some b}" 

3981  47 

5183  48 
primrec 
49 
"map_of [] = empty" 

5300  50 
"map_of (p#ps) = (map_of ps)(fst p > snd p)" 
51 

52 
primrec "t([] [>]bs) = t" 

53 
"t(a#as[>]bs) = t(a>hd bs)(as[>]tl bs)" 

3981  54 

13908  55 

56 
section "empty" 

57 

58 
lemma empty_upd_none: "empty(x := None) = empty" 

59 
apply (rule ext) 

60 
apply (simp (no_asm)) 

61 
done 

62 
declare empty_upd_none [simp] 

63 

64 
(* FIXME: what is this sum_case nonsense?? *) 

65 
lemma sum_case_empty_empty: "sum_case empty empty = empty" 

66 
apply (rule ext) 

67 
apply (simp (no_asm) split add: sum.split) 

68 
done 

69 
declare sum_case_empty_empty [simp] 

70 

71 

72 
section "map_upd" 

73 

74 
lemma map_upd_triv: "t k = Some x ==> t(k>x) = t" 

75 
apply (rule ext) 

76 
apply (simp (no_asm_simp)) 

77 
done 

78 

79 
lemma map_upd_nonempty: "t(k>x) ~= empty" 

80 
apply safe 

81 
apply (drule_tac x = "k" in fun_cong) 

82 
apply (simp (no_asm_use)) 

83 
done 

84 
declare map_upd_nonempty [simp] 

85 

86 
lemma finite_range_updI: "finite (range f) ==> finite (range (f(a>b)))" 

87 
apply (unfold image_def) 

88 
apply (simp (no_asm_use) add: full_SetCompr_eq) 

89 
apply (rule finite_subset) 

90 
prefer 2 apply (assumption) 

91 
apply auto 

92 
done 

93 

94 

95 
(* FIXME: what is this sum_case nonsense?? *) 

96 
section "sum_case and empty/map_upd" 

97 

98 
lemma sum_case_map_upd_empty: "sum_case (m(k>y)) empty = (sum_case m empty)(Inl k>y)" 

99 
apply (rule ext) 

100 
apply (simp (no_asm) split add: sum.split) 

101 
done 

102 
declare sum_case_map_upd_empty [simp] 

103 

104 
lemma sum_case_empty_map_upd: "sum_case empty (m(k>y)) = (sum_case empty m)(Inr k>y)" 

105 
apply (rule ext) 

106 
apply (simp (no_asm) split add: sum.split) 

107 
done 

108 
declare sum_case_empty_map_upd [simp] 

109 

110 
lemma sum_case_map_upd_map_upd: "sum_case (m1(k1>y1)) (m2(k2>y2)) = (sum_case (m1(k1>y1)) m2)(Inr k2>y2)" 

111 
apply (rule ext) 

112 
apply (simp (no_asm) split add: sum.split) 

113 
done 

114 
declare sum_case_map_upd_map_upd [simp] 

115 

116 

117 
section "map_upds" 

118 

119 
lemma map_upds_twist [rule_format (no_asm)]: "a ~: set as > (!m bs. (m(a>b)(as[>]bs)) = (m(as[>]bs)(a>b)))" 

120 
apply (induct_tac "as") 

121 
apply (auto simp del: fun_upd_apply) 

122 
apply (drule spec)+ 

123 
apply (rotate_tac 1) 

124 
apply (erule subst) 

125 
apply (erule fun_upd_twist [THEN subst]) 

126 
apply (rule refl) 

127 
done 

128 
declare map_upds_twist [simp] 

129 

130 

131 
section "chg_map" 

132 

133 
lemma chg_map_new: "m a = None ==> chg_map f a m = m" 

134 
apply (unfold chg_map_def) 

135 
apply auto 

136 
done 

137 

138 
lemma chg_map_upd: "m a = Some b ==> chg_map f a m = m(a>f b)" 

139 
apply (unfold chg_map_def) 

140 
apply auto 

141 
done 

142 

143 
declare chg_map_new [simp] chg_map_upd [simp] 

144 

145 

146 
section "map_of" 

147 

148 
lemma map_of_SomeD [rule_format (no_asm)]: "map_of xs k = Some y > (k,y):set xs" 

149 
apply (induct_tac "xs") 

150 
apply auto 

151 
done 

152 

153 
lemma map_of_mapk_SomeI [rule_format (no_asm)]: "inj f ==> map_of t k = Some x > 

154 
map_of (map (split (%k. Pair (f k))) t) (f k) = Some x" 

155 
apply (induct_tac "t") 

156 
apply (auto simp add: inj_eq) 

157 
done 

158 

159 
lemma weak_map_of_SomeI [rule_format (no_asm)]: "(k, x) : set l > (? x. map_of l k = Some x)" 

160 
apply (induct_tac "l") 

161 
apply auto 

162 
done 

163 

164 
lemma map_of_filter_in: 

165 
"[ map_of xs k = Some z; P k z ] ==> map_of (filter (split P) xs) k = Some z" 

166 
apply (rule mp) 

167 
prefer 2 apply (assumption) 

168 
apply (erule thin_rl) 

169 
apply (induct_tac "xs") 

170 
apply auto 

171 
done 

172 

173 
lemma finite_range_map_of: "finite (range (map_of l))" 

174 
apply (induct_tac "l") 

175 
apply (simp_all (no_asm) add: image_constant) 

176 
apply (rule finite_subset) 

177 
prefer 2 apply (assumption) 

178 
apply auto 

179 
done 

180 

181 
lemma map_of_map: "map_of (map (%(a,b). (a,f b)) xs) x = option_map f (map_of xs x)" 

182 
apply (induct_tac "xs") 

183 
apply auto 

184 
done 

185 

186 

187 
section "option_map related" 

188 

189 
lemma option_map_o_empty: "option_map f o empty = empty" 

190 
apply (rule ext) 

191 
apply (simp (no_asm)) 

192 
done 

193 

194 
lemma option_map_o_map_upd: "option_map f o m(a>b) = (option_map f o m)(a>f b)" 

195 
apply (rule ext) 

196 
apply (simp (no_asm)) 

197 
done 

198 

199 
declare option_map_o_empty [simp] option_map_o_map_upd [simp] 

200 

201 

202 
section "++" 

203 

204 
lemma override_empty: "m ++ empty = m" 

205 
apply (unfold override_def) 

206 
apply (simp (no_asm)) 

207 
done 

208 
declare override_empty [simp] 

209 

210 
lemma empty_override: "empty ++ m = m" 

211 
apply (unfold override_def) 

212 
apply (rule ext) 

213 
apply (simp split add: option.split) 

214 
done 

215 
declare empty_override [simp] 

216 

217 
lemma override_Some_iff [rule_format (no_asm)]: 

218 
"((m ++ n) k = Some x) = (n k = Some x  n k = None & m k = Some x)" 

219 
apply (unfold override_def) 

220 
apply (simp (no_asm) split add: option.split) 

221 
done 

222 

223 
lemmas override_SomeD = override_Some_iff [THEN iffD1, standard] 

224 
declare override_SomeD [dest!] 

225 

226 
lemma override_find_right: "!!xx. n k = Some xx ==> (m ++ n) k = Some xx" 

227 
apply (subst override_Some_iff) 

228 
apply fast 

229 
done 

230 
declare override_find_right [simp] 

231 

232 
lemma override_None: "((m ++ n) k = None) = (n k = None & m k = None)" 

233 
apply (unfold override_def) 

234 
apply (simp (no_asm) split add: option.split) 

235 
done 

236 
declare override_None [iff] 

237 

238 
lemma override_upd: "f ++ g(x>y) = (f ++ g)(x>y)" 

239 
apply (unfold override_def) 

240 
apply (rule ext) 

241 
apply auto 

242 
done 

243 
declare override_upd [simp] 

244 

245 
lemma map_of_override: "map_of ys ++ map_of xs = map_of (xs@ys)" 

246 
apply (unfold override_def) 

247 
apply (rule sym) 

248 
apply (induct_tac "xs") 

249 
apply (simp (no_asm)) 

250 
apply (rule ext) 

251 
apply (simp (no_asm_simp) split add: option.split) 

252 
done 

253 
declare map_of_override [simp] 

254 

255 
declare fun_upd_apply [simp del] 

256 
lemma finite_range_map_of_override: "finite (range f) ==> finite (range (f ++ map_of l))" 

257 
apply (induct_tac "l") 

258 
apply auto 

259 
apply (erule finite_range_updI) 

260 
done 

261 
declare fun_upd_apply [simp] 

262 

263 

264 
section "dom" 

265 

266 
lemma domI: "m a = Some b ==> a : dom m" 

267 
apply (unfold dom_def) 

268 
apply auto 

269 
done 

270 

271 
lemma domD: "a : dom m ==> ? b. m a = Some b" 

272 
apply (unfold dom_def) 

273 
apply auto 

274 
done 

275 

276 
lemma domIff: "(a : dom m) = (m a ~= None)" 

277 
apply (unfold dom_def) 

278 
apply auto 

279 
done 

280 
declare domIff [iff] 

281 
declare domIff [simp del] 

282 

283 
lemma dom_empty: "dom empty = {}" 

284 
apply (unfold dom_def) 

285 
apply (simp (no_asm)) 

286 
done 

287 
declare dom_empty [simp] 

288 

289 
lemma dom_map_upd: "dom(m(a>b)) = insert a (dom m)" 

290 
apply (unfold dom_def) 

291 
apply (simp (no_asm)) 

292 
apply blast 

293 
done 

294 
declare dom_map_upd [simp] 

295 

296 
lemma finite_dom_map_of: "finite (dom (map_of l))" 

297 
apply (unfold dom_def) 

298 
apply (induct_tac "l") 

299 
apply (auto simp add: insert_Collect [symmetric]) 

300 
done 

301 

302 
lemma dom_override: "dom(m++n) = dom n Un dom m" 

303 
apply (unfold dom_def) 

304 
apply auto 

305 
done 

306 
declare dom_override [simp] 

307 

308 
section "ran" 

309 

310 
lemma ran_empty: "ran empty = {}" 

311 
apply (unfold ran_def) 

312 
apply (simp (no_asm)) 

313 
done 

314 
declare ran_empty [simp] 

315 

316 
lemma ran_empty': "ran (%u. None) = {}" 

317 
apply (unfold ran_def) 

318 
apply auto 

319 
done 

320 
declare ran_empty' [simp] 

321 

322 
lemma ran_map_upd: "m a = None ==> ran(m(a>b)) = insert b (ran m)" 

323 
apply (unfold ran_def) 

324 
apply auto 

325 
apply (subgoal_tac "~ (aa = a) ") 

326 
apply auto 

327 
done 

328 
declare ran_map_upd [simp] 

329 

3981  330 
end 