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

src/HOL/Library/Nested_Environment.thy

author | wenzelm |

Thu Oct 16 22:44:24 2008 +0200 (2008-10-16) | |

changeset 28615 | 4c8fa015ec7f |

parent 28562 | 4e74209f113e |

child 30663 | 0b6aff7451b2 |

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

explicit SORT_CONSTRAINT for proofs depending implicitly on certain sorts;

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 imports Plain "~~/src/HOL/List" "~~/src/HOL/Code_Eval"

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 assumes "lookup env xs = None"

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

106 using assms

107 proof (induct xs arbitrary: env)

108 case Nil

109 then have False by simp

110 then show ?case ..

111 next

112 case (Cons x xs)

113 show ?case

114 proof (cases env)

115 case Val

116 then show ?thesis by simp

117 next

118 case (Env b es)

119 show ?thesis

120 proof (cases "es x")

121 case None

122 with Env show ?thesis by simp

123 next

124 case (Some e)

125 note es = `es x = Some e`

126 show ?thesis

127 proof (cases "lookup e xs")

128 case None

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

130 with Env Some show ?thesis by simp

131 next

132 case Some

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

134 then show ?thesis ..

135 qed

136 qed

137 qed

138 qed

140 theorem lookup_append_some:

141 assumes "lookup env xs = Some e"

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

143 using assms

144 proof (induct xs arbitrary: env e)

145 case Nil

146 then have "env = e" by simp

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

148 next

149 case (Cons x xs)

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

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

152 proof (cases env)

153 case (Val a)

154 with asm have False by simp

155 then show ?thesis ..

156 next

157 case (Env b es)

158 show ?thesis

159 proof (cases "es x")

160 case None

161 with asm Env have False by simp

162 then show ?thesis ..

163 next

164 case (Some e')

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

166 show ?thesis

167 proof (cases "lookup e' xs")

168 case None

169 with asm Env es have False by simp

170 then show ?thesis ..

171 next

172 case Some

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

174 by simp

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

176 with Env es show ?thesis by simp

177 qed

178 qed

179 qed

180 qed

182 text {*

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

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

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

186 [source] lookup_append_none} above.

187 *}

189 theorem lookup_some_append:

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

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

192 proof -

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

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

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

196 then show ?thesis by (simp)

197 qed

199 text {*

200 The subsequent statement describes in more detail how a successful

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

202 at any upper position.

203 *}

205 theorem lookup_some_upper:

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

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

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

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

210 lookup env' ys = Some e"

211 using assms

212 proof (induct xs arbitrary: env e)

213 case Nil

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

215 by simp

216 then obtain b' es' env' where

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

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

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

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

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

222 with es' look' show ?case by blast

223 next

224 case (Cons x xs)

225 from Cons.prems

226 obtain b' es' env' where

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

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

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

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

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

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

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

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

235 by blast

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

237 by simp

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

239 qed

242 subsection {* The update operation *}

244 text {*

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

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

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

248 environment is left unchanged.

249 *}

251 consts

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

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

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

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

257 primrec (update)

258 "update xs opt (Val a) =

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

260 else Val a)"

261 "update xs opt (Env b es) =

262 (case xs of

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

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

265 "update_option xs opt None =

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

267 "update_option xs opt (Some e) =

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

270 hide const update_option

272 text {*

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

274 the following equalities.

275 *}

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

278 by (cases env) simp_all

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

281 by (cases env) simp_all

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

284 by simp

286 theorem update_cons_nil_env:

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

288 by (cases "es x") simp_all

290 theorem update_cons_cons_env:

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

292 Env b (es (x :=

293 (case es x of

294 None => None

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

296 by (cases "es x") simp_all

298 lemmas update.simps [simp del]

299 and update_simps [simp] = update_nil_none update_nil_some

300 update_cons_val update_cons_nil_env update_cons_cons_env

302 lemma update_eq:

303 "update xs opt env =

304 (case xs of

305 [] =>

306 (case opt of

307 None => env

308 | Some e => e)

309 | x # xs =>

310 (case env of

311 Val a => Val a

312 | Env b es =>

313 (case xs of

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

315 | y # ys =>

316 Env b (es (x :=

317 (case es x of

318 None => None

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

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

322 text {*

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

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

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

326 *}

328 theorem lookup_update_some:

329 assumes "lookup env xs = Some e"

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

331 using assms

332 proof (induct xs arbitrary: env e)

333 case Nil

334 then have "env = e" by simp

335 then show ?case by simp

336 next

337 case (Cons x xs)

338 note hyp = Cons.hyps

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

340 show ?case

341 proof (cases env)

342 case (Val a)

343 with asm have False by simp

344 then show ?thesis ..

345 next

346 case (Env b es)

347 show ?thesis

348 proof (cases "es x")

349 case None

350 with asm Env have False by simp

351 then show ?thesis ..

352 next

353 case (Some e')

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

355 show ?thesis

356 proof (cases xs)

357 case Nil

358 with Env show ?thesis by simp

359 next

360 case (Cons x' xs')

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

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

363 with Env es Cons show ?thesis by simp

364 qed

365 qed

366 qed

367 qed

369 text {*

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

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

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

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

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

375 *}

377 theorem update_append_none:

378 assumes "lookup env xs = None"

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

380 using assms

381 proof (induct xs arbitrary: env)

382 case Nil

383 then have False by simp

384 then show ?case ..

385 next

386 case (Cons x xs)

387 note hyp = Cons.hyps

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

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

390 proof (cases env)

391 case (Val a)

392 then show ?thesis by simp

393 next

394 case (Env b es)

395 show ?thesis

396 proof (cases "es x")

397 case None

398 note es = `es x = None`

399 show ?thesis

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

401 next

402 case (Some e)

403 note es = `es x = Some e`

404 show ?thesis

405 proof (cases xs)

406 case Nil

407 with asm Env Some have False by simp

408 then show ?thesis ..

409 next

410 case (Cons x' xs')

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

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

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

414 by (simp add: fun_upd_idem_iff)

415 qed

416 qed

417 qed

418 qed

420 theorem update_append_some:

421 assumes "lookup env xs = Some e"

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

423 using assms

424 proof (induct xs arbitrary: env e)

425 case Nil

426 then have "env = e" by simp

427 then show ?case by simp

428 next

429 case (Cons x xs)

430 note hyp = Cons.hyps

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

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

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

434 proof (cases env)

435 case (Val a)

436 with asm have False by simp

437 then show ?thesis ..

438 next

439 case (Env b es)

440 show ?thesis

441 proof (cases "es x")

442 case None

443 with asm Env have False by simp

444 then show ?thesis ..

445 next

446 case (Some e')

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

448 show ?thesis

449 proof (cases xs)

450 case Nil

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

452 with Env es Nil show ?thesis by simp

453 next

454 case (Cons x' xs')

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

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

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

458 with Env es Cons show ?thesis by simp

459 qed

460 qed

461 qed

462 qed

464 text {*

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

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

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

468 a certain point.

469 *}

471 theorem lookup_update_other:

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

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

474 lookup env (xs @ y # ys)"

475 proof (induct xs arbitrary: env)

476 case Nil

477 show ?case

478 proof (cases env)

479 case Val

480 then show ?thesis by simp

481 next

482 case Env

483 show ?thesis

484 proof (cases zs)

485 case Nil

486 with neq Env show ?thesis by simp

487 next

488 case Cons

489 with neq Env show ?thesis by simp

490 qed

491 qed

492 next

493 case (Cons x xs)

494 note hyp = Cons.hyps

495 show ?case

496 proof (cases env)

497 case Val

498 then show ?thesis by simp

499 next

500 case (Env y es)

501 show ?thesis

502 proof (cases xs)

503 case Nil

504 show ?thesis

505 proof (cases "es x")

506 case None

507 with Env Nil show ?thesis by simp

508 next

509 case Some

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

511 qed

512 next

513 case (Cons x' xs')

514 show ?thesis

515 proof (cases "es x")

516 case None

517 with Env Cons show ?thesis by simp

518 next

519 case Some

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

521 qed

522 qed

523 qed

524 qed

526 text {* Environments and code generation *}

528 lemma [code, code del]:

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

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

532 lemma eq_env_code [code]:

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

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

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

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

537 of None \<Rightarrow> (case g z

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

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

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

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

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

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

544 proof (unfold eq)

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

546 of None \<Rightarrow> (case g z

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

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

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

550 proof

551 assume ?lhs

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

553 next

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

555 show ?lhs

556 proof

557 fix z

558 from assm have "?prop z" ..

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

560 qed

561 qed

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

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

564 of None \<Rightarrow> (case g z

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

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

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

568 qed simp_all

570 lemma [code, code del]:

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

573 end