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

src/HOL/Library/Nested_Environment.thy

author | nipkow |

Mon Aug 16 14:22:27 2004 +0200 (2004-08-16) | |

changeset 15131 | c69542757a4d |

parent 14981 | e73f8140af78 |

child 15140 | 322485b816ac |

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

New theory header syntax.

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

9 import Main

10 begin

12 text {*

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

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

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

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

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

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

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

20 position within the structure.

21 *}

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

24 Val 'a

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

27 text {*

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

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

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

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

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

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

34 *}

37 subsection {* The lookup operation *}

39 text {*

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

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

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

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

44 @{term None}.

45 *}

47 consts

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

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

51 primrec (lookup)

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

53 "lookup (Env b es) xs =

54 (case xs of

55 [] => Some (Env b es)

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

57 "lookup_option None xs = None"

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

60 hide const lookup_option

62 text {*

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

64 the following equalities.

65 *}

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

68 by (cases e) simp_all

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

71 by simp

73 theorem lookup_env_cons:

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

75 (case es x of

76 None => None

77 | Some e => lookup e xs)"

78 by (cases "es x") simp_all

80 lemmas lookup.simps [simp del]

81 and lookup_simps [simp] = lookup_nil lookup_val_cons lookup_env_cons

83 theorem lookup_eq:

84 "lookup env xs =

85 (case xs of

86 [] => Some env

87 | x # xs =>

88 (case env of

89 Val a => None

90 | Env b es =>

91 (case es x of

92 None => None

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

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

96 text {*

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

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

99 depending whether the environment actually extends far enough to

100 follow the base path.

101 *}

103 theorem lookup_append_none:

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

105 (is "PROP ?P xs")

106 proof (induct xs)

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

108 {

109 assume "lookup env [] = None"

110 hence False by simp

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

112 next

113 fix x xs

114 assume hyp: "PROP ?P xs"

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

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

117 proof (cases env)

118 case Val

119 thus ?thesis by simp

120 next

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

122 show ?thesis

123 proof (cases "es x")

124 assume "es x = None"

125 with env show ?thesis by simp

126 next

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

128 show ?thesis

129 proof (cases "lookup e xs")

130 case None

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

132 with env es show ?thesis by simp

133 next

134 case Some

135 with asm env es have False by simp

136 thus ?thesis ..

137 qed

138 qed

139 qed

140 }

141 qed

143 theorem lookup_append_some:

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

145 (is "PROP ?P xs")

146 proof (induct xs)

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

148 {

149 assume "lookup env [] = Some e"

150 hence "env = e" by simp

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

152 next

153 fix x xs

154 assume hyp: "PROP ?P xs"

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

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

157 proof (cases env)

158 fix a assume "env = Val a"

159 with asm have False by simp

160 thus ?thesis ..

161 next

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

163 show ?thesis

164 proof (cases "es x")

165 assume "es x = None"

166 with asm env have False by simp

167 thus ?thesis ..

168 next

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

170 show ?thesis

171 proof (cases "lookup e' xs")

172 case None

173 with asm env es have False by simp

174 thus ?thesis ..

175 next

176 case Some

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

178 by simp

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

180 with env es show ?thesis by simp

181 qed

182 qed

183 qed

184 }

185 qed

187 text {*

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

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

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

191 [source] lookup_append_none} above.

192 *}

194 theorem lookup_some_append:

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

196 proof -

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

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

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

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

201 thus ?thesis by simp

202 qed

204 text {*

205 The subsequent statement describes in more detail how a successful

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

207 at any upper position.

208 *}

210 theorem lookup_some_upper: "!!env e.

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

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

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

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

215 lookup env' ys = Some e"

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

217 proof (induct xs)

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

219 {

220 assume "?A []"

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

222 then obtain b' es' env' where

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

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

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

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

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

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

229 next

230 fix x xs

231 assume hyp: "PROP ?P xs"

232 assume "?A (x # xs)"

233 then obtain b' es' env' where

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

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

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

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

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

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

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

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

242 by blast

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

244 by simp

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

246 }

247 qed

250 subsection {* The update operation *}

252 text {*

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

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

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

256 environment is left unchanged.

257 *}

259 consts

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

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

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

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

265 primrec (update)

266 "update xs opt (Val a) =

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

268 else Val a)"

269 "update xs opt (Env b es) =

270 (case xs of

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

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

273 "update_option xs opt None =

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

275 "update_option xs opt (Some e) =

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

278 hide const update_option

280 text {*

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

282 the following equalities.

283 *}

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

286 by (cases env) simp_all

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

289 by (cases env) simp_all

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

292 by simp

294 theorem update_cons_nil_env:

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

296 by (cases "es x") simp_all

298 theorem update_cons_cons_env:

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

300 Env b (es (x :=

301 (case es x of

302 None => None

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

304 by (cases "es x") simp_all

306 lemmas update.simps [simp del]

307 and update_simps [simp] = update_nil_none update_nil_some

308 update_cons_val update_cons_nil_env update_cons_cons_env

310 lemma update_eq:

311 "update xs opt env =

312 (case xs of

313 [] =>

314 (case opt of

315 None => env

316 | Some e => e)

317 | x # xs =>

318 (case env of

319 Val a => Val a

320 | Env b es =>

321 (case xs of

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

323 | y # ys =>

324 Env b (es (x :=

325 (case es x of

326 None => None

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

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

330 text {*

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

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

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

334 *}

336 theorem lookup_update_some:

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

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

339 (is "PROP ?P xs")

340 proof (induct xs)

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

342 {

343 assume "lookup env [] = Some e"

344 hence "env = e" by simp

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

346 by simp

347 next

348 fix x xs

349 assume hyp: "PROP ?P xs"

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

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

352 proof (cases env)

353 fix a assume "env = Val a"

354 with asm have False by simp

355 thus ?thesis ..

356 next

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

358 show ?thesis

359 proof (cases "es x")

360 assume "es x = None"

361 with asm env have False by simp

362 thus ?thesis ..

363 next

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

365 show ?thesis

366 proof (cases xs)

367 assume "xs = []"

368 with env show ?thesis by simp

369 next

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

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

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

373 with env es xs show ?thesis by simp

374 qed

375 qed

376 qed

377 }

378 qed

380 text {*

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

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

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

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

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

386 *}

388 theorem update_append_none:

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

390 (is "PROP ?P xs")

391 proof (induct xs)

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

393 {

394 assume "lookup env [] = None"

395 hence False by simp

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

397 next

398 fix x xs

399 assume hyp: "PROP ?P xs"

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

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

402 proof (cases env)

403 fix a assume "env = Val a"

404 thus ?thesis by simp

405 next

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

407 show ?thesis

408 proof (cases "es x")

409 assume es: "es x = None"

410 show ?thesis

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

412 next

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

414 show ?thesis

415 proof (cases xs)

416 assume "xs = []"

417 with asm env es have False by simp

418 thus ?thesis ..

419 next

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

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

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

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

424 by (simp add: fun_upd_idem_iff)

425 qed

426 qed

427 qed

428 }

429 qed

431 theorem update_append_some:

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

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

434 (is "PROP ?P xs")

435 proof (induct xs)

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

437 {

438 assume "lookup env [] = Some e"

439 hence "env = e" by simp

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

441 by simp

442 next

443 fix x xs

444 assume hyp: "PROP ?P xs"

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

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

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

448 proof (cases env)

449 fix a assume "env = Val a"

450 with asm have False by simp

451 thus ?thesis ..

452 next

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

454 show ?thesis

455 proof (cases "es x")

456 assume "es x = None"

457 with asm env have False by simp

458 thus ?thesis ..

459 next

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

461 show ?thesis

462 proof (cases xs)

463 assume xs: "xs = []"

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

465 with env es xs show ?thesis by simp

466 next

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

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

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

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

471 with env es xs show ?thesis by simp

472 qed

473 qed

474 qed

475 }

476 qed

478 text {*

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

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

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

482 a certain point.

483 *}

485 theorem lookup_update_other:

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

487 lookup env (xs @ y # ys)"

488 (is "PROP ?P xs")

489 proof (induct xs)

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

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

492 {

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

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

495 proof (cases env)

496 case Val

497 thus ?thesis by simp

498 next

499 case Env

500 show ?thesis

501 proof (cases zs)

502 case Nil

503 with neq Env show ?thesis by simp

504 next

505 case Cons

506 with neq Env show ?thesis by simp

507 qed

508 qed

509 next

510 fix x xs

511 assume hyp: "PROP ?P xs"

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

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

514 proof (cases env)

515 case Val

516 thus ?thesis by simp

517 next

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

519 show ?thesis

520 proof (cases xs)

521 assume xs: "xs = []"

522 show ?thesis

523 proof (cases "es x")

524 case None

525 with env xs show ?thesis by simp

526 next

527 case Some

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

529 qed

530 next

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

532 show ?thesis

533 proof (cases "es x")

534 case None

535 with env xs show ?thesis by simp

536 next

537 case Some

538 with hyp env xs neq show ?thesis by simp

539 qed

540 qed

541 qed

542 }

543 qed

545 end