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

src/HOL/Library/Nested_Environment.thy

author | huffman |

Thu Jun 11 09:03:24 2009 -0700 (2009-06-11) | |

changeset 31563 | ded2364d14d4 |

parent 30663 | 0b6aff7451b2 |

child 32657 | 5f13912245ff |

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

cleaned up some proofs

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

2 Author: Markus Wenzel, TU Muenchen

3 *)

5 header {* Nested environments *}

7 theory Nested_Environment

8 imports Main

9 begin

11 text {*

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

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

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

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

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

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

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

19 position within the structure.

20 *}

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

23 Val 'a

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

26 text {*

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

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

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

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

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

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

33 *}

36 subsection {* The lookup operation *}

38 text {*

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

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

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

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

43 @{term None}.

44 *}

46 consts

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

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

50 primrec (lookup)

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

52 "lookup (Env b es) xs =

53 (case xs of

54 [] => Some (Env b es)

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

56 "lookup_option None xs = None"

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

59 hide const lookup_option

61 text {*

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

63 the following equalities.

64 *}

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

67 by (cases e) simp_all

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

70 by simp

72 theorem lookup_env_cons:

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

74 (case es x of

75 None => None

76 | Some e => lookup e xs)"

77 by (cases "es x") simp_all

79 lemmas lookup.simps [simp del]

80 and lookup_simps [simp] = lookup_nil lookup_val_cons lookup_env_cons

82 theorem lookup_eq:

83 "lookup env xs =

84 (case xs of

85 [] => Some env

86 | x # xs =>

87 (case env of

88 Val a => None

89 | Env b es =>

90 (case es x of

91 None => None

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

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

95 text {*

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

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

98 depending whether the environment actually extends far enough to

99 follow the base path.

100 *}

102 theorem lookup_append_none:

103 assumes "lookup env xs = None"

104 shows "lookup env (xs @ ys) = None"

105 using assms

106 proof (induct xs arbitrary: env)

107 case Nil

108 then have False by simp

109 then show ?case ..

110 next

111 case (Cons x xs)

112 show ?case

113 proof (cases env)

114 case Val

115 then show ?thesis by simp

116 next

117 case (Env b es)

118 show ?thesis

119 proof (cases "es x")

120 case None

121 with Env show ?thesis by simp

122 next

123 case (Some e)

124 note es = `es x = Some e`

125 show ?thesis

126 proof (cases "lookup e xs")

127 case None

128 then have "lookup e (xs @ ys) = None" by (rule Cons.hyps)

129 with Env Some show ?thesis by simp

130 next

131 case Some

132 with Env es have False using Cons.prems by simp

133 then show ?thesis ..

134 qed

135 qed

136 qed

137 qed

139 theorem lookup_append_some:

140 assumes "lookup env xs = Some e"

141 shows "lookup env (xs @ ys) = lookup e ys"

142 using assms

143 proof (induct xs arbitrary: env e)

144 case Nil

145 then have "env = e" by simp

146 then show "lookup env ([] @ ys) = lookup e ys" by simp

147 next

148 case (Cons x xs)

149 note asm = `lookup env (x # xs) = Some e`

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

151 proof (cases env)

152 case (Val a)

153 with asm have False by simp

154 then show ?thesis ..

155 next

156 case (Env b es)

157 show ?thesis

158 proof (cases "es x")

159 case None

160 with asm Env have False by simp

161 then show ?thesis ..

162 next

163 case (Some e')

164 note es = `es x = Some e'`

165 show ?thesis

166 proof (cases "lookup e' xs")

167 case None

168 with asm Env es have False by simp

169 then show ?thesis ..

170 next

171 case Some

172 with asm Env es have "lookup e' xs = Some e"

173 by simp

174 then have "lookup e' (xs @ ys) = lookup e ys" by (rule Cons.hyps)

175 with Env es show ?thesis by simp

176 qed

177 qed

178 qed

179 qed

181 text {*

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

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

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

185 [source] lookup_append_none} above.

186 *}

188 theorem lookup_some_append:

189 assumes "lookup env (xs @ ys) = Some e"

190 shows "\<exists>e. lookup env xs = Some e"

191 proof -

192 from assms have "lookup env (xs @ ys) \<noteq> None" by simp

193 then have "lookup env xs \<noteq> None"

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

195 then show ?thesis by (simp)

196 qed

198 text {*

199 The subsequent statement describes in more detail how a successful

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

201 at any upper position.

202 *}

204 theorem lookup_some_upper:

205 assumes "lookup env (xs @ y # ys) = Some e"

206 shows "\<exists>b' es' env'.

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

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

209 lookup env' ys = Some e"

210 using assms

211 proof (induct xs arbitrary: env e)

212 case Nil

213 from Nil.prems have "lookup env (y # ys) = Some e"

214 by simp

215 then obtain b' es' env' where

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

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

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

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

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

221 with es' look' show ?case by blast

222 next

223 case (Cons x xs)

224 from Cons.prems

225 obtain b' es' env' where

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

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

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

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

230 from Cons.hyps [OF look'] obtain b'' es'' env'' where

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

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

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

234 by blast

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

236 by simp

237 with es'' look'' show ?case by blast

238 qed

241 subsection {* The update operation *}

243 text {*

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

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

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

247 environment is left unchanged.

248 *}

250 consts

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

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

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

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

256 primrec (update)

257 "update xs opt (Val a) =

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

259 else Val a)"

260 "update xs opt (Env b es) =

261 (case xs of

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

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

264 "update_option xs opt None =

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

266 "update_option xs opt (Some e) =

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

269 hide const update_option

271 text {*

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

273 the following equalities.

274 *}

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

277 by (cases env) simp_all

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

280 by (cases env) simp_all

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

283 by simp

285 theorem update_cons_nil_env:

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

287 by (cases "es x") simp_all

289 theorem update_cons_cons_env:

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

291 Env b (es (x :=

292 (case es x of

293 None => None

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

295 by (cases "es x") simp_all

297 lemmas update.simps [simp del]

298 and update_simps [simp] = update_nil_none update_nil_some

299 update_cons_val update_cons_nil_env update_cons_cons_env

301 lemma update_eq:

302 "update xs opt env =

303 (case xs of

304 [] =>

305 (case opt of

306 None => env

307 | Some e => e)

308 | x # xs =>

309 (case env of

310 Val a => Val a

311 | Env b es =>

312 (case xs of

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

314 | y # ys =>

315 Env b (es (x :=

316 (case es x of

317 None => None

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

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

321 text {*

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

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

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

325 *}

327 theorem lookup_update_some:

328 assumes "lookup env xs = Some e"

329 shows "lookup (update xs (Some env') env) xs = Some env'"

330 using assms

331 proof (induct xs arbitrary: env e)

332 case Nil

333 then have "env = e" by simp

334 then show ?case by simp

335 next

336 case (Cons x xs)

337 note hyp = Cons.hyps

338 and asm = `lookup env (x # xs) = Some e`

339 show ?case

340 proof (cases env)

341 case (Val a)

342 with asm have False by simp

343 then show ?thesis ..

344 next

345 case (Env b es)

346 show ?thesis

347 proof (cases "es x")

348 case None

349 with asm Env have False by simp

350 then show ?thesis ..

351 next

352 case (Some e')

353 note es = `es x = Some e'`

354 show ?thesis

355 proof (cases xs)

356 case Nil

357 with Env show ?thesis by simp

358 next

359 case (Cons x' xs')

360 from asm Env es have "lookup e' xs = Some e" by simp

361 then have "lookup (update xs (Some env') e') xs = Some env'" by (rule hyp)

362 with Env es Cons show ?thesis by simp

363 qed

364 qed

365 qed

366 qed

368 text {*

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

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

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

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

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

374 *}

376 theorem update_append_none:

377 assumes "lookup env xs = None"

378 shows "update (xs @ y # ys) opt env = env"

379 using assms

380 proof (induct xs arbitrary: env)

381 case Nil

382 then have False by simp

383 then show ?case ..

384 next

385 case (Cons x xs)

386 note hyp = Cons.hyps

387 and asm = `lookup env (x # xs) = None`

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

389 proof (cases env)

390 case (Val a)

391 then show ?thesis by simp

392 next

393 case (Env b es)

394 show ?thesis

395 proof (cases "es x")

396 case None

397 note es = `es x = None`

398 show ?thesis

399 by (cases xs) (simp_all add: es Env fun_upd_idem_iff)

400 next

401 case (Some e)

402 note es = `es x = Some e`

403 show ?thesis

404 proof (cases xs)

405 case Nil

406 with asm Env Some have False by simp

407 then show ?thesis ..

408 next

409 case (Cons x' xs')

410 from asm Env es have "lookup e xs = None" by simp

411 then have "update (xs @ y # ys) opt e = e" by (rule hyp)

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

413 by (simp add: fun_upd_idem_iff)

414 qed

415 qed

416 qed

417 qed

419 theorem update_append_some:

420 assumes "lookup env xs = Some e"

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

422 using assms

423 proof (induct xs arbitrary: env e)

424 case Nil

425 then have "env = e" by simp

426 then show ?case by simp

427 next

428 case (Cons x xs)

429 note hyp = Cons.hyps

430 and asm = `lookup env (x # xs) = Some e`

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

432 Some (update (y # ys) opt e)"

433 proof (cases env)

434 case (Val a)

435 with asm have False by simp

436 then show ?thesis ..

437 next

438 case (Env b es)

439 show ?thesis

440 proof (cases "es x")

441 case None

442 with asm Env have False by simp

443 then show ?thesis ..

444 next

445 case (Some e')

446 note es = `es x = Some e'`

447 show ?thesis

448 proof (cases xs)

449 case Nil

450 with asm Env es have "e = e'" by simp

451 with Env es Nil show ?thesis by simp

452 next

453 case (Cons x' xs')

454 from asm Env es have "lookup e' xs = Some e" by simp

455 then have "lookup (update (xs @ y # ys) opt e') xs =

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

457 with Env es Cons show ?thesis by simp

458 qed

459 qed

460 qed

461 qed

463 text {*

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

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

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

467 a certain point.

468 *}

470 theorem lookup_update_other:

471 assumes neq: "y \<noteq> (z::'c)"

472 shows "lookup (update (xs @ z # zs) opt env) (xs @ y # ys) =

473 lookup env (xs @ y # ys)"

474 proof (induct xs arbitrary: env)

475 case Nil

476 show ?case

477 proof (cases env)

478 case Val

479 then show ?thesis by simp

480 next

481 case Env

482 show ?thesis

483 proof (cases zs)

484 case Nil

485 with neq Env show ?thesis by simp

486 next

487 case Cons

488 with neq Env show ?thesis by simp

489 qed

490 qed

491 next

492 case (Cons x xs)

493 note hyp = Cons.hyps

494 show ?case

495 proof (cases env)

496 case Val

497 then show ?thesis by simp

498 next

499 case (Env y es)

500 show ?thesis

501 proof (cases xs)

502 case Nil

503 show ?thesis

504 proof (cases "es x")

505 case None

506 with Env Nil show ?thesis by simp

507 next

508 case Some

509 with neq hyp and Env Nil show ?thesis by simp

510 qed

511 next

512 case (Cons x' xs')

513 show ?thesis

514 proof (cases "es x")

515 case None

516 with Env Cons show ?thesis by simp

517 next

518 case Some

519 with neq hyp and Env Cons show ?thesis by simp

520 qed

521 qed

522 qed

523 qed

525 text {* Environments and code generation *}

527 lemma [code, code del]:

528 fixes e1 e2 :: "('b\<Colon>eq, 'a\<Colon>eq, 'c\<Colon>eq) env"

529 shows "eq_class.eq e1 e2 \<longleftrightarrow> eq_class.eq e1 e2" ..

531 lemma eq_env_code [code]:

532 fixes x y :: "'a\<Colon>eq"

533 and f g :: "'c\<Colon>{eq, finite} \<Rightarrow> ('b\<Colon>eq, 'a, 'c) env option"

534 shows "eq_class.eq (Env x f) (Env y g) \<longleftrightarrow>

535 eq_class.eq x y \<and> (\<forall>z\<in>UNIV. case f z

536 of None \<Rightarrow> (case g z

537 of None \<Rightarrow> True | Some _ \<Rightarrow> False)

538 | Some a \<Rightarrow> (case g z

539 of None \<Rightarrow> False | Some b \<Rightarrow> eq_class.eq a b))" (is ?env)

540 and "eq_class.eq (Val a) (Val b) \<longleftrightarrow> eq_class.eq a b"

541 and "eq_class.eq (Val a) (Env y g) \<longleftrightarrow> False"

542 and "eq_class.eq (Env x f) (Val b) \<longleftrightarrow> False"

543 proof (unfold eq)

544 have "f = g \<longleftrightarrow> (\<forall>z. case f z

545 of None \<Rightarrow> (case g z

546 of None \<Rightarrow> True | Some _ \<Rightarrow> False)

547 | Some a \<Rightarrow> (case g z

548 of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" (is "?lhs = ?rhs")

549 proof

550 assume ?lhs

551 then show ?rhs by (auto split: option.splits)

552 next

553 assume assm: ?rhs (is "\<forall>z. ?prop z")

554 show ?lhs

555 proof

556 fix z

557 from assm have "?prop z" ..

558 then show "f z = g z" by (auto split: option.splits)

559 qed

560 qed

561 then show "Env x f = Env y g \<longleftrightarrow>

562 x = y \<and> (\<forall>z\<in>UNIV. case f z

563 of None \<Rightarrow> (case g z

564 of None \<Rightarrow> True | Some _ \<Rightarrow> False)

565 | Some a \<Rightarrow> (case g z

566 of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp

567 qed simp_all

569 lemma [code, code del]:

570 "(Code_Eval.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Eval.term_of" ..

572 end