summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Nested_Environment.thy

author | kleing |

Mon Jun 21 10:25:57 2004 +0200 (2004-06-21) | |

changeset 14981 | e73f8140af78 |

parent 14706 | 71590b7733b7 |

child 15131 | c69542757a4d |

permissions | -rw-r--r-- |

Merged in license change from Isabelle2004

1 (* Title: HOL/Library/Nested_Environment.thy

2 ID: $Id$

3 Author: Markus Wenzel, TU Muenchen

4 *)

6 header {* Nested environments *}

8 theory Nested_Environment = Main:

10 text {*

11 Consider a partial function @{term [source] "e :: 'a => 'b option"};

12 this may be understood as an \emph{environment} mapping indexes

13 @{typ 'a} to optional entry values @{typ 'b} (cf.\ the basic theory

14 @{text Map} of Isabelle/HOL). This basic idea is easily generalized

15 to that of a \emph{nested environment}, where entries may be either

16 basic values or again proper environments. Then each entry is

17 accessed by a \emph{path}, i.e.\ a list of indexes leading to its

18 position within the structure.

19 *}

21 datatype ('a, 'b, 'c) env =

22 Val 'a

23 | Env 'b "'c => ('a, 'b, 'c) env option"

25 text {*

26 \medskip In the type @{typ "('a, 'b, 'c) env"} the parameter @{typ

27 'a} refers to basic values (occurring in terminal positions), type

28 @{typ 'b} to values associated with proper (inner) environments, and

29 type @{typ 'c} with the index type for branching. Note that there

30 is no restriction on any of these types. In particular, arbitrary

31 branching may yield rather large (transfinite) tree structures.

32 *}

35 subsection {* The lookup operation *}

37 text {*

38 Lookup in nested environments works by following a given path of

39 index elements, leading to an optional result (a terminal value or

40 nested environment). A \emph{defined position} within a nested

41 environment is one where @{term lookup} at its path does not yield

42 @{term None}.

43 *}

45 consts

46 lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"

47 lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option"

49 primrec (lookup)

50 "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"

51 "lookup (Env b es) xs =

52 (case xs of

53 [] => Some (Env b es)

54 | y # ys => lookup_option (es y) ys)"

55 "lookup_option None xs = None"

56 "lookup_option (Some e) xs = lookup e xs"

58 hide const lookup_option

60 text {*

61 \medskip The characteristic cases of @{term lookup} are expressed by

62 the following equalities.

63 *}

65 theorem lookup_nil: "lookup e [] = Some e"

66 by (cases e) simp_all

68 theorem lookup_val_cons: "lookup (Val a) (x # xs) = None"

69 by simp

71 theorem lookup_env_cons:

72 "lookup (Env b es) (x # xs) =

73 (case es x of

74 None => None

75 | Some e => lookup e xs)"

76 by (cases "es x") simp_all

78 lemmas lookup.simps [simp del]

79 and lookup_simps [simp] = lookup_nil lookup_val_cons lookup_env_cons

81 theorem lookup_eq:

82 "lookup env xs =

83 (case xs of

84 [] => Some env

85 | x # xs =>

86 (case env of

87 Val a => None

88 | Env b es =>

89 (case es x of

90 None => None

91 | Some e => lookup e xs)))"

92 by (simp split: list.split env.split)

94 text {*

95 \medskip Displaced @{term lookup} operations, relative to a certain

96 base path prefix, may be reduced as follows. There are two cases,

97 depending whether the environment actually extends far enough to

98 follow the base path.

99 *}

101 theorem lookup_append_none:

102 "!!env. lookup env xs = None ==> lookup env (xs @ ys) = None"

103 (is "PROP ?P xs")

104 proof (induct xs)

105 fix env :: "('a, 'b, 'c) env"

106 {

107 assume "lookup env [] = None"

108 hence False by simp

109 thus "lookup env ([] @ ys) = None" ..

110 next

111 fix x xs

112 assume hyp: "PROP ?P xs"

113 assume asm: "lookup env (x # xs) = None"

114 show "lookup env ((x # xs) @ ys) = None"

115 proof (cases env)

116 case Val

117 thus ?thesis by simp

118 next

119 fix b es assume env: "env = Env b es"

120 show ?thesis

121 proof (cases "es x")

122 assume "es x = None"

123 with env show ?thesis by simp

124 next

125 fix e assume es: "es x = Some e"

126 show ?thesis

127 proof (cases "lookup e xs")

128 case None

129 hence "lookup e (xs @ ys) = None" by (rule hyp)

130 with env es show ?thesis by simp

131 next

132 case Some

133 with asm env es have False by simp

134 thus ?thesis ..

135 qed

136 qed

137 qed

138 }

139 qed

141 theorem lookup_append_some:

142 "!!env e. lookup env xs = Some e ==> lookup env (xs @ ys) = lookup e ys"

143 (is "PROP ?P xs")

144 proof (induct xs)

145 fix env e :: "('a, 'b, 'c) env"

146 {

147 assume "lookup env [] = Some e"

148 hence "env = e" by simp

149 thus "lookup env ([] @ ys) = lookup e ys" by simp

150 next

151 fix x xs

152 assume hyp: "PROP ?P xs"

153 assume asm: "lookup env (x # xs) = Some e"

154 show "lookup env ((x # xs) @ ys) = lookup e ys"

155 proof (cases env)

156 fix a assume "env = Val a"

157 with asm have False by simp

158 thus ?thesis ..

159 next

160 fix b es assume env: "env = Env b es"

161 show ?thesis

162 proof (cases "es x")

163 assume "es x = None"

164 with asm env have False by simp

165 thus ?thesis ..

166 next

167 fix e' assume es: "es x = Some e'"

168 show ?thesis

169 proof (cases "lookup e' xs")

170 case None

171 with asm env es have False by simp

172 thus ?thesis ..

173 next

174 case Some

175 with asm env es have "lookup e' xs = Some e"

176 by simp

177 hence "lookup e' (xs @ ys) = lookup e ys" by (rule hyp)

178 with env es show ?thesis by simp

179 qed

180 qed

181 qed

182 }

183 qed

185 text {*

186 \medskip Successful @{term lookup} deeper down an environment

187 structure means we are able to peek further up as well. Note that

188 this is basically just the contrapositive statement of @{thm

189 [source] lookup_append_none} above.

190 *}

192 theorem lookup_some_append:

193 "lookup env (xs @ ys) = Some e ==> \<exists>e. lookup env xs = Some e"

194 proof -

195 assume "lookup env (xs @ ys) = Some e"

196 hence "lookup env (xs @ ys) \<noteq> None" by simp

197 hence "lookup env xs \<noteq> None"

198 by (rule contrapos_nn) (simp only: lookup_append_none)

199 thus ?thesis by simp

200 qed

202 text {*

203 The subsequent statement describes in more detail how a successful

204 @{term lookup} with a non-empty path results in a certain situation

205 at any upper position.

206 *}

208 theorem lookup_some_upper: "!!env e.

209 lookup env (xs @ y # ys) = Some e ==>

210 \<exists>b' es' env'.

211 lookup env xs = Some (Env b' es') \<and>

212 es' y = Some env' \<and>

213 lookup env' ys = Some e"

214 (is "PROP ?P xs" is "!!env e. ?A env e xs ==> ?C env e xs")

215 proof (induct xs)

216 fix env e let ?A = "?A env e" and ?C = "?C env e"

217 {

218 assume "?A []"

219 hence "lookup env (y # ys) = Some e" by simp

220 then obtain b' es' env' where

221 env: "env = Env b' es'" and

222 es': "es' y = Some env'" and

223 look': "lookup env' ys = Some e"

224 by (auto simp add: lookup_eq split: option.splits env.splits)

225 from env have "lookup env [] = Some (Env b' es')" by simp

226 with es' look' show "?C []" by blast

227 next

228 fix x xs

229 assume hyp: "PROP ?P xs"

230 assume "?A (x # xs)"

231 then obtain b' es' env' where

232 env: "env = Env b' es'" and

233 es': "es' x = Some env'" and

234 look': "lookup env' (xs @ y # ys) = Some e"

235 by (auto simp add: lookup_eq split: option.splits env.splits)

236 from hyp [OF look'] obtain b'' es'' env'' where

237 upper': "lookup env' xs = Some (Env b'' es'')" and

238 es'': "es'' y = Some env''" and

239 look'': "lookup env'' ys = Some e"

240 by blast

241 from env es' upper' have "lookup env (x # xs) = Some (Env b'' es'')"

242 by simp

243 with es'' look'' show "?C (x # xs)" by blast

244 }

245 qed

248 subsection {* The update operation *}

250 text {*

251 Update at a certain position in a nested environment may either

252 delete an existing entry, or overwrite an existing one. Note that

253 update at undefined positions is simple absorbed, i.e.\ the

254 environment is left unchanged.

255 *}

257 consts

258 update :: "'c list => ('a, 'b, 'c) env option

259 => ('a, 'b, 'c) env => ('a, 'b, 'c) env"

260 update_option :: "'c list => ('a, 'b, 'c) env option

261 => ('a, 'b, 'c) env option => ('a, 'b, 'c) env option"

263 primrec (update)

264 "update xs opt (Val a) =

265 (if xs = [] then (case opt of None => Val a | Some e => e)

266 else Val a)"

267 "update xs opt (Env b es) =

268 (case xs of

269 [] => (case opt of None => Env b es | Some e => e)

270 | y # ys => Env b (es (y := update_option ys opt (es y))))"

271 "update_option xs opt None =

272 (if xs = [] then opt else None)"

273 "update_option xs opt (Some e) =

274 (if xs = [] then opt else Some (update xs opt e))"

276 hide const update_option

278 text {*

279 \medskip The characteristic cases of @{term update} are expressed by

280 the following equalities.

281 *}

283 theorem update_nil_none: "update [] None env = env"

284 by (cases env) simp_all

286 theorem update_nil_some: "update [] (Some e) env = e"

287 by (cases env) simp_all

289 theorem update_cons_val: "update (x # xs) opt (Val a) = Val a"

290 by simp

292 theorem update_cons_nil_env:

293 "update [x] opt (Env b es) = Env b (es (x := opt))"

294 by (cases "es x") simp_all

296 theorem update_cons_cons_env:

297 "update (x # y # ys) opt (Env b es) =

298 Env b (es (x :=

299 (case es x of

300 None => None

301 | Some e => Some (update (y # ys) opt e))))"

302 by (cases "es x") simp_all

304 lemmas update.simps [simp del]

305 and update_simps [simp] = update_nil_none update_nil_some

306 update_cons_val update_cons_nil_env update_cons_cons_env

308 lemma update_eq:

309 "update xs opt env =

310 (case xs of

311 [] =>

312 (case opt of

313 None => env

314 | Some e => e)

315 | x # xs =>

316 (case env of

317 Val a => Val a

318 | Env b es =>

319 (case xs of

320 [] => Env b (es (x := opt))

321 | y # ys =>

322 Env b (es (x :=

323 (case es x of

324 None => None

325 | Some e => Some (update (y # ys) opt e)))))))"

326 by (simp split: list.split env.split option.split)

328 text {*

329 \medskip The most basic correspondence of @{term lookup} and @{term

330 update} states that after @{term update} at a defined position,

331 subsequent @{term lookup} operations would yield the new value.

332 *}

334 theorem lookup_update_some:

335 "!!env e. lookup env xs = Some e ==>

336 lookup (update xs (Some env') env) xs = Some env'"

337 (is "PROP ?P xs")

338 proof (induct xs)

339 fix env e :: "('a, 'b, 'c) env"

340 {

341 assume "lookup env [] = Some e"

342 hence "env = e" by simp

343 thus "lookup (update [] (Some env') env) [] = Some env'"

344 by simp

345 next

346 fix x xs

347 assume hyp: "PROP ?P xs"

348 assume asm: "lookup env (x # xs) = Some e"

349 show "lookup (update (x # xs) (Some env') env) (x # xs) = Some env'"

350 proof (cases env)

351 fix a assume "env = Val a"

352 with asm have False by simp

353 thus ?thesis ..

354 next

355 fix b es assume env: "env = Env b es"

356 show ?thesis

357 proof (cases "es x")

358 assume "es x = None"

359 with asm env have False by simp

360 thus ?thesis ..

361 next

362 fix e' assume es: "es x = Some e'"

363 show ?thesis

364 proof (cases xs)

365 assume "xs = []"

366 with env show ?thesis by simp

367 next

368 fix x' xs' assume xs: "xs = x' # xs'"

369 from asm env es have "lookup e' xs = Some e" by simp

370 hence "lookup (update xs (Some env') e') xs = Some env'" by (rule hyp)

371 with env es xs show ?thesis by simp

372 qed

373 qed

374 qed

375 }

376 qed

378 text {*

379 \medskip The properties of displaced @{term update} operations are

380 analogous to those of @{term lookup} above. There are two cases:

381 below an undefined position @{term update} is absorbed altogether,

382 and below a defined positions @{term update} affects subsequent

383 @{term lookup} operations in the obvious way.

384 *}

386 theorem update_append_none:

387 "!!env. lookup env xs = None ==> update (xs @ y # ys) opt env = env"

388 (is "PROP ?P xs")

389 proof (induct xs)

390 fix env :: "('a, 'b, 'c) env"

391 {

392 assume "lookup env [] = None"

393 hence False by simp

394 thus "update ([] @ y # ys) opt env = env" ..

395 next

396 fix x xs

397 assume hyp: "PROP ?P xs"

398 assume asm: "lookup env (x # xs) = None"

399 show "update ((x # xs) @ y # ys) opt env = env"

400 proof (cases env)

401 fix a assume "env = Val a"

402 thus ?thesis by simp

403 next

404 fix b es assume env: "env = Env b es"

405 show ?thesis

406 proof (cases "es x")

407 assume es: "es x = None"

408 show ?thesis

409 by (cases xs) (simp_all add: es env fun_upd_idem_iff)

410 next

411 fix e assume es: "es x = Some e"

412 show ?thesis

413 proof (cases xs)

414 assume "xs = []"

415 with asm env es have False by simp

416 thus ?thesis ..

417 next

418 fix x' xs' assume xs: "xs = x' # xs'"

419 from asm env es have "lookup e xs = None" by simp

420 hence "update (xs @ y # ys) opt e = e" by (rule hyp)

421 with env es xs show "update ((x # xs) @ y # ys) opt env = env"

422 by (simp add: fun_upd_idem_iff)

423 qed

424 qed

425 qed

426 }

427 qed

429 theorem update_append_some:

430 "!!env e. lookup env xs = Some e ==>

431 lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)"

432 (is "PROP ?P xs")

433 proof (induct xs)

434 fix env e :: "('a, 'b, 'c) env"

435 {

436 assume "lookup env [] = Some e"

437 hence "env = e" by simp

438 thus "lookup (update ([] @ y # ys) opt env) [] = Some (update (y # ys) opt e)"

439 by simp

440 next

441 fix x xs

442 assume hyp: "PROP ?P xs"

443 assume asm: "lookup env (x # xs) = Some e"

444 show "lookup (update ((x # xs) @ y # ys) opt env) (x # xs)

445 = Some (update (y # ys) opt e)"

446 proof (cases env)

447 fix a assume "env = Val a"

448 with asm have False by simp

449 thus ?thesis ..

450 next

451 fix b es assume env: "env = Env b es"

452 show ?thesis

453 proof (cases "es x")

454 assume "es x = None"

455 with asm env have False by simp

456 thus ?thesis ..

457 next

458 fix e' assume es: "es x = Some e'"

459 show ?thesis

460 proof (cases xs)

461 assume xs: "xs = []"

462 from asm env es xs have "e = e'" by simp

463 with env es xs show ?thesis by simp

464 next

465 fix x' xs' assume xs: "xs = x' # xs'"

466 from asm env es have "lookup e' xs = Some e" by simp

467 hence "lookup (update (xs @ y # ys) opt e') xs =

468 Some (update (y # ys) opt e)" by (rule hyp)

469 with env es xs show ?thesis by simp

470 qed

471 qed

472 qed

473 }

474 qed

476 text {*

477 \medskip Apparently, @{term update} does not affect the result of

478 subsequent @{term lookup} operations at independent positions, i.e.\

479 in case that the paths for @{term update} and @{term lookup} fork at

480 a certain point.

481 *}

483 theorem lookup_update_other:

484 "!!env. y \<noteq> (z::'c) ==> lookup (update (xs @ z # zs) opt env) (xs @ y # ys) =

485 lookup env (xs @ y # ys)"

486 (is "PROP ?P xs")

487 proof (induct xs)

488 fix env :: "('a, 'b, 'c) env"

489 assume neq: "y \<noteq> z"

490 {

491 show "lookup (update ([] @ z # zs) opt env) ([] @ y # ys) =

492 lookup env ([] @ y # ys)"

493 proof (cases env)

494 case Val

495 thus ?thesis by simp

496 next

497 case Env

498 show ?thesis

499 proof (cases zs)

500 case Nil

501 with neq Env show ?thesis by simp

502 next

503 case Cons

504 with neq Env show ?thesis by simp

505 qed

506 qed

507 next

508 fix x xs

509 assume hyp: "PROP ?P xs"

510 show "lookup (update ((x # xs) @ z # zs) opt env) ((x # xs) @ y # ys) =

511 lookup env ((x # xs) @ y # ys)"

512 proof (cases env)

513 case Val

514 thus ?thesis by simp

515 next

516 fix y es assume env: "env = Env y es"

517 show ?thesis

518 proof (cases xs)

519 assume xs: "xs = []"

520 show ?thesis

521 proof (cases "es x")

522 case None

523 with env xs show ?thesis by simp

524 next

525 case Some

526 with hyp env xs and neq show ?thesis by simp

527 qed

528 next

529 fix x' xs' assume xs: "xs = x' # xs'"

530 show ?thesis

531 proof (cases "es x")

532 case None

533 with env xs show ?thesis by simp

534 next

535 case Some

536 with hyp env xs neq show ?thesis by simp

537 qed

538 qed

539 qed

540 }

541 qed

543 end