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

src/HOL/Library/Nested_Environment.thy

author | wenzelm |

Thu Feb 11 23:00:22 2010 +0100 (2010-02-11) | |

changeset 35115 | 446c5063e4fd |

parent 34941 | 156925dd67af |

child 36176 | 3fe7e97ccca8 |

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

modernized translations;

formal markup of @{syntax_const} and @{const_syntax};

minor tuning;

formal markup of @{syntax_const} and @{const_syntax};

minor tuning;

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 primrec

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

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

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

50 | "lookup (Env b es) xs =

51 (case xs of

52 [] => Some (Env b es)

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

54 | "lookup_option None xs = None"

55 | "lookup_option (Some e) xs = lookup e xs"

57 hide const lookup_option

59 text {*

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

61 the following equalities.

62 *}

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

65 by (cases e) simp_all

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

68 by simp

70 theorem lookup_env_cons:

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

72 (case es x of

73 None => None

74 | Some e => lookup e xs)"

75 by (cases "es x") simp_all

77 lemmas lookup_lookup_option.simps [simp del]

78 and lookup_simps [simp] = lookup_nil lookup_val_cons lookup_env_cons

80 theorem lookup_eq:

81 "lookup env xs =

82 (case xs of

83 [] => Some env

84 | x # xs =>

85 (case env of

86 Val a => None

87 | Env b es =>

88 (case es x of

89 None => None

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

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

93 text {*

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

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

96 depending whether the environment actually extends far enough to

97 follow the base path.

98 *}

100 theorem lookup_append_none:

101 assumes "lookup env xs = None"

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

103 using assms

104 proof (induct xs arbitrary: env)

105 case Nil

106 then have False by simp

107 then show ?case ..

108 next

109 case (Cons x xs)

110 show ?case

111 proof (cases env)

112 case Val

113 then show ?thesis by simp

114 next

115 case (Env b es)

116 show ?thesis

117 proof (cases "es x")

118 case None

119 with Env show ?thesis by simp

120 next

121 case (Some e)

122 note es = `es x = Some e`

123 show ?thesis

124 proof (cases "lookup e xs")

125 case None

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

127 with Env Some show ?thesis by simp

128 next

129 case Some

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

131 then show ?thesis ..

132 qed

133 qed

134 qed

135 qed

137 theorem lookup_append_some:

138 assumes "lookup env xs = Some e"

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

140 using assms

141 proof (induct xs arbitrary: env e)

142 case Nil

143 then have "env = e" by simp

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

145 next

146 case (Cons x xs)

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

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

149 proof (cases env)

150 case (Val a)

151 with asm have False by simp

152 then show ?thesis ..

153 next

154 case (Env b es)

155 show ?thesis

156 proof (cases "es x")

157 case None

158 with asm Env have False by simp

159 then show ?thesis ..

160 next

161 case (Some e')

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

163 show ?thesis

164 proof (cases "lookup e' xs")

165 case None

166 with asm Env es have False by simp

167 then show ?thesis ..

168 next

169 case Some

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

171 by simp

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

173 with Env es show ?thesis by simp

174 qed

175 qed

176 qed

177 qed

179 text {*

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

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

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

183 [source] lookup_append_none} above.

184 *}

186 theorem lookup_some_append:

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

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

189 proof -

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

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

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

193 then show ?thesis by (simp)

194 qed

196 text {*

197 The subsequent statement describes in more detail how a successful

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

199 at any upper position.

200 *}

202 theorem lookup_some_upper:

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

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

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

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

207 lookup env' ys = Some e"

208 using assms

209 proof (induct xs arbitrary: env e)

210 case Nil

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

212 by simp

213 then obtain b' es' env' where

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

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

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

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

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

219 with es' look' show ?case by blast

220 next

221 case (Cons x xs)

222 from Cons.prems

223 obtain b' es' env' where

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

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

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

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

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

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

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

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

232 by blast

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

234 by simp

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

236 qed

239 subsection {* The update operation *}

241 text {*

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

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

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

245 environment is left unchanged.

246 *}

248 primrec

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

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

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

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

253 "update xs opt (Val a) =

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

255 else Val a)"

256 | "update xs opt (Env b es) =

257 (case xs of

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

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

260 | "update_option xs opt None =

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

262 | "update_option xs opt (Some e) =

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

265 hide const update_option

267 text {*

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

269 the following equalities.

270 *}

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

273 by (cases env) simp_all

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

276 by (cases env) simp_all

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

279 by simp

281 theorem update_cons_nil_env:

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

283 by (cases "es x") simp_all

285 theorem update_cons_cons_env:

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

287 Env b (es (x :=

288 (case es x of

289 None => None

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

291 by (cases "es x") simp_all

293 lemmas update_update_option.simps [simp del]

294 and update_simps [simp] = update_nil_none update_nil_some

295 update_cons_val update_cons_nil_env update_cons_cons_env

297 lemma update_eq:

298 "update xs opt env =

299 (case xs of

300 [] =>

301 (case opt of

302 None => env

303 | Some e => e)

304 | x # xs =>

305 (case env of

306 Val a => Val a

307 | Env b es =>

308 (case xs of

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

310 | y # ys =>

311 Env b (es (x :=

312 (case es x of

313 None => None

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

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

317 text {*

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

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

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

321 *}

323 theorem lookup_update_some:

324 assumes "lookup env xs = Some e"

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

326 using assms

327 proof (induct xs arbitrary: env e)

328 case Nil

329 then have "env = e" by simp

330 then show ?case by simp

331 next

332 case (Cons x xs)

333 note hyp = Cons.hyps

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

335 show ?case

336 proof (cases env)

337 case (Val a)

338 with asm have False by simp

339 then show ?thesis ..

340 next

341 case (Env b es)

342 show ?thesis

343 proof (cases "es x")

344 case None

345 with asm Env have False by simp

346 then show ?thesis ..

347 next

348 case (Some e')

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

350 show ?thesis

351 proof (cases xs)

352 case Nil

353 with Env show ?thesis by simp

354 next

355 case (Cons x' xs')

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

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

358 with Env es Cons show ?thesis by simp

359 qed

360 qed

361 qed

362 qed

364 text {*

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

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

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

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

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

370 *}

372 theorem update_append_none:

373 assumes "lookup env xs = None"

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

375 using assms

376 proof (induct xs arbitrary: env)

377 case Nil

378 then have False by simp

379 then show ?case ..

380 next

381 case (Cons x xs)

382 note hyp = Cons.hyps

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

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

385 proof (cases env)

386 case (Val a)

387 then show ?thesis by simp

388 next

389 case (Env b es)

390 show ?thesis

391 proof (cases "es x")

392 case None

393 note es = `es x = None`

394 show ?thesis

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

396 next

397 case (Some e)

398 note es = `es x = Some e`

399 show ?thesis

400 proof (cases xs)

401 case Nil

402 with asm Env Some have False by simp

403 then show ?thesis ..

404 next

405 case (Cons x' xs')

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

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

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

409 by (simp add: fun_upd_idem_iff)

410 qed

411 qed

412 qed

413 qed

415 theorem update_append_some:

416 assumes "lookup env xs = Some e"

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

418 using assms

419 proof (induct xs arbitrary: env e)

420 case Nil

421 then have "env = e" by simp

422 then show ?case by simp

423 next

424 case (Cons x xs)

425 note hyp = Cons.hyps

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

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

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

429 proof (cases env)

430 case (Val a)

431 with asm have False by simp

432 then show ?thesis ..

433 next

434 case (Env b es)

435 show ?thesis

436 proof (cases "es x")

437 case None

438 with asm Env have False by simp

439 then show ?thesis ..

440 next

441 case (Some e')

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

443 show ?thesis

444 proof (cases xs)

445 case Nil

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

447 with Env es Nil show ?thesis by simp

448 next

449 case (Cons x' xs')

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

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

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

453 with Env es Cons show ?thesis by simp

454 qed

455 qed

456 qed

457 qed

459 text {*

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

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

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

463 a certain point.

464 *}

466 theorem lookup_update_other:

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

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

469 lookup env (xs @ y # ys)"

470 proof (induct xs arbitrary: env)

471 case Nil

472 show ?case

473 proof (cases env)

474 case Val

475 then show ?thesis by simp

476 next

477 case Env

478 show ?thesis

479 proof (cases zs)

480 case Nil

481 with neq Env show ?thesis by simp

482 next

483 case Cons

484 with neq Env show ?thesis by simp

485 qed

486 qed

487 next

488 case (Cons x xs)

489 note hyp = Cons.hyps

490 show ?case

491 proof (cases env)

492 case Val

493 then show ?thesis by simp

494 next

495 case (Env y es)

496 show ?thesis

497 proof (cases xs)

498 case Nil

499 show ?thesis

500 proof (cases "es x")

501 case None

502 with Env Nil show ?thesis by simp

503 next

504 case Some

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

506 qed

507 next

508 case (Cons x' xs')

509 show ?thesis

510 proof (cases "es x")

511 case None

512 with Env Cons show ?thesis by simp

513 next

514 case Some

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

516 qed

517 qed

518 qed

519 qed

521 text {* Environments and code generation *}

523 lemma [code, code del]:

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

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

527 lemma eq_env_code [code]:

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

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

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

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

532 of None \<Rightarrow> (case g z

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

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

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

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

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

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

539 proof (unfold eq)

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

541 of None \<Rightarrow> (case g z

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

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

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

545 proof

546 assume ?lhs

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

548 next

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

550 show ?lhs

551 proof

552 fix z

553 from assm have "?prop z" ..

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

555 qed

556 qed

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

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

559 of None \<Rightarrow> (case g z

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

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

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

563 qed simp_all

565 lemma [code, code del]:

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

568 end