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

src/HOL/Unix/Nested_Environment.thy

author | wenzelm |

Mon Dec 21 21:48:36 2015 +0100 (2015-12-21) | |

changeset 61893 | 4121cc8479f8 |

parent 58889 | 5b7a9633cfa8 |

child 66148 | 5e60c2d0a1f1 |

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

misc tuning and modernization;

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

2 Author: Markus Wenzel, TU Muenchen

3 *)

5 section \<open>Nested environments\<close>

7 theory Nested_Environment

8 imports Main

9 begin

11 text \<open>

12 Consider a partial function @{term [source] "e :: 'a \<Rightarrow> 'b option"}; this may

13 be understood as an \<^emph>\<open>environment\<close> mapping indexes @{typ 'a} to optional

14 entry values @{typ 'b} (cf.\ the basic theory \<open>Map\<close> of Isabelle/HOL). This

15 basic idea is easily generalized to that of a \<^emph>\<open>nested environment\<close>, where

16 entries may be either basic values or again proper environments. Then each

17 entry is accessed by a \<^emph>\<open>path\<close>, i.e.\ a list of indexes leading to its

18 position within the structure.

19 \<close>

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

22 Val 'a

23 | Env 'b "'c \<Rightarrow> ('a, 'b, 'c) env option"

25 text \<open>

26 \<^medskip>

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

28 basic values (occurring in terminal positions), type @{typ 'b} to values

29 associated with proper (inner) environments, and type @{typ 'c} with the

30 index type for branching. Note that there is no restriction on any of these

31 types. In particular, arbitrary branching may yield rather large

32 (transfinite) tree structures.

33 \<close>

36 subsection \<open>The lookup operation\<close>

38 text \<open>

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

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

41 environment). A \<^emph>\<open>defined position\<close> within a nested environment is one where

42 @{term lookup} at its path does not yield @{term None}.

43 \<close>

45 primrec lookup :: "('a, 'b, 'c) env \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"

46 and lookup_option :: "('a, 'b, 'c) env option \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"

47 where

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

49 | "lookup (Env b es) xs =

50 (case xs of

51 [] \<Rightarrow> Some (Env b es)

52 | y # ys \<Rightarrow> lookup_option (es y) ys)"

53 | "lookup_option None xs = None"

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

56 hide_const lookup_option

58 text \<open>

59 \<^medskip>

60 The characteristic cases of @{term lookup} are expressed by the following

61 equalities.

62 \<close>

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 \<Rightarrow> None

74 | Some e \<Rightarrow> lookup e xs)"

75 by (cases "es x") simp_all

77 lemmas lookup.simps [simp del] 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 [] \<Rightarrow> Some env

84 | x # xs \<Rightarrow>

85 (case env of

86 Val a \<Rightarrow> None

87 | Env b es \<Rightarrow>

88 (case es x of

89 None \<Rightarrow> None

90 | Some e \<Rightarrow> lookup e xs)))"

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

93 text \<open>

94 \<^medskip>

95 Displaced @{term lookup} operations, relative to a certain base path prefix,

96 may be reduced as follows. There are two cases, depending whether the

97 environment actually extends far enough to follow the base path.

98 \<close>

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 = \<open>es x = Some e\<close>

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 = \<open>lookup env (x # xs) = Some e\<close>

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 = \<open>es x = Some e'\<close>

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 \<open>

180 \<^medskip>

181 Successful @{term lookup} deeper down an environment structure means we are

182 able to peek further up as well. Note that this is basically just the

183 contrapositive statement of @{thm [source] lookup_append_none} above.

184 \<close>

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 \<open>

197 The subsequent statement describes in more detail how a successful @{term

198 lookup} with a non-empty path results in a certain situation at any upper

199 position.

200 \<close>

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 \<open>The update operation\<close>

241 text \<open>

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

243 existing entry, or overwrite an existing one. Note that update at undefined

244 positions is simple absorbed, i.e.\ the environment is left unchanged.

245 \<close>

247 primrec update :: "'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow>

248 ('a, 'b, 'c) env \<Rightarrow> ('a, 'b, 'c) env"

249 and update_option :: "'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow>

250 ('a, 'b, 'c) env option \<Rightarrow> ('a, 'b, 'c) env option"

251 where

252 "update xs opt (Val a) =

253 (if xs = [] then (case opt of None \<Rightarrow> Val a | Some e \<Rightarrow> e)

254 else Val a)"

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

256 (case xs of

257 [] \<Rightarrow> (case opt of None \<Rightarrow> Env b es | Some e \<Rightarrow> e)

258 | y # ys \<Rightarrow> Env b (es (y := update_option ys opt (es y))))"

259 | "update_option xs opt None =

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

261 | "update_option xs opt (Some e) =

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

264 hide_const update_option

266 text \<open>

267 \<^medskip>

268 The characteristic cases of @{term update} are expressed by the following

269 equalities.

270 \<close>

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 \<Rightarrow> None

290 | Some e \<Rightarrow> Some (update (y # ys) opt e))))"

291 by (cases "es x") simp_all

293 lemmas update.simps [simp del] 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 [] \<Rightarrow>

301 (case opt of

302 None \<Rightarrow> env

303 | Some e \<Rightarrow> e)

304 | x # xs \<Rightarrow>

305 (case env of

306 Val a \<Rightarrow> Val a

307 | Env b es \<Rightarrow>

308 (case xs of

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

310 | y # ys \<Rightarrow>

311 Env b (es (x :=

312 (case es x of

313 None \<Rightarrow> None

314 | Some e \<Rightarrow> Some (update (y # ys) opt e)))))))"

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

317 text \<open>

318 \<^medskip>

319 The most basic correspondence of @{term lookup} and @{term update} states

320 that after @{term update} at a defined position, subsequent @{term lookup}

321 operations would yield the new value.

322 \<close>

324 theorem lookup_update_some:

325 assumes "lookup env xs = Some e"

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

327 using assms

328 proof (induct xs arbitrary: env e)

329 case Nil

330 then have "env = e" by simp

331 then show ?case by simp

332 next

333 case (Cons x xs)

334 note hyp = Cons.hyps

335 and asm = \<open>lookup env (x # xs) = Some e\<close>

336 show ?case

337 proof (cases env)

338 case (Val a)

339 with asm have False by simp

340 then show ?thesis ..

341 next

342 case (Env b es)

343 show ?thesis

344 proof (cases "es x")

345 case None

346 with asm Env have False by simp

347 then show ?thesis ..

348 next

349 case (Some e')

350 note es = \<open>es x = Some e'\<close>

351 show ?thesis

352 proof (cases xs)

353 case Nil

354 with Env show ?thesis by simp

355 next

356 case (Cons x' xs')

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

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

359 with Env es Cons show ?thesis by simp

360 qed

361 qed

362 qed

363 qed

365 text \<open>

366 \<^medskip>

367 The properties of displaced @{term update} operations are analogous to those

368 of @{term lookup} above. There are two cases: below an undefined position

369 @{term update} is absorbed altogether, and below a defined positions @{term

370 update} affects subsequent @{term lookup} operations in the obvious way.

371 \<close>

373 theorem update_append_none:

374 assumes "lookup env xs = None"

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

376 using assms

377 proof (induct xs arbitrary: env)

378 case Nil

379 then have False by simp

380 then show ?case ..

381 next

382 case (Cons x xs)

383 note hyp = Cons.hyps

384 and asm = \<open>lookup env (x # xs) = None\<close>

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

386 proof (cases env)

387 case (Val a)

388 then show ?thesis by simp

389 next

390 case (Env b es)

391 show ?thesis

392 proof (cases "es x")

393 case None

394 note es = \<open>es x = None\<close>

395 show ?thesis

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

397 next

398 case (Some e)

399 note es = \<open>es x = Some e\<close>

400 show ?thesis

401 proof (cases xs)

402 case Nil

403 with asm Env Some have False by simp

404 then show ?thesis ..

405 next

406 case (Cons x' xs')

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

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

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

410 by (simp add: fun_upd_idem_iff)

411 qed

412 qed

413 qed

414 qed

416 theorem update_append_some:

417 assumes "lookup env xs = Some e"

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

419 using assms

420 proof (induct xs arbitrary: env e)

421 case Nil

422 then have "env = e" by simp

423 then show ?case by simp

424 next

425 case (Cons x xs)

426 note hyp = Cons.hyps

427 and asm = \<open>lookup env (x # xs) = Some e\<close>

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

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

430 proof (cases env)

431 case (Val a)

432 with asm have False by simp

433 then show ?thesis ..

434 next

435 case (Env b es)

436 show ?thesis

437 proof (cases "es x")

438 case None

439 with asm Env have False by simp

440 then show ?thesis ..

441 next

442 case (Some e')

443 note es = \<open>es x = Some e'\<close>

444 show ?thesis

445 proof (cases xs)

446 case Nil

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

448 with Env es Nil show ?thesis by simp

449 next

450 case (Cons x' xs')

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

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

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

454 with Env es Cons show ?thesis by simp

455 qed

456 qed

457 qed

458 qed

460 text \<open>

461 \<^medskip>

462 Apparently, @{term update} does not affect the result of subsequent @{term

463 lookup} operations at independent positions, i.e.\ in case that the paths

464 for @{term update} and @{term lookup} fork at a certain point.

465 \<close>

467 theorem lookup_update_other:

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

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

470 lookup env (xs @ y # ys)"

471 proof (induct xs arbitrary: env)

472 case Nil

473 show ?case

474 proof (cases env)

475 case Val

476 then show ?thesis by simp

477 next

478 case Env

479 show ?thesis

480 proof (cases zs)

481 case Nil

482 with neq Env show ?thesis by simp

483 next

484 case Cons

485 with neq Env show ?thesis by simp

486 qed

487 qed

488 next

489 case (Cons x xs)

490 note hyp = Cons.hyps

491 show ?case

492 proof (cases env)

493 case Val

494 then show ?thesis by simp

495 next

496 case (Env y es)

497 show ?thesis

498 proof (cases xs)

499 case Nil

500 show ?thesis

501 proof (cases "es x")

502 case None

503 with Env Nil show ?thesis by simp

504 next

505 case Some

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

507 qed

508 next

509 case (Cons x' xs')

510 show ?thesis

511 proof (cases "es x")

512 case None

513 with Env Cons show ?thesis by simp

514 next

515 case Some

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

517 qed

518 qed

519 qed

520 qed

523 subsection \<open>Code generation\<close>

525 lemma [code, code del]:

526 "(HOL.equal :: (_, _, _) env \<Rightarrow> _) = HOL.equal" ..

528 lemma equal_env_code [code]:

529 fixes x y :: "'a::equal"

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

531 shows

532 "HOL.equal (Env x f) (Env y g) \<longleftrightarrow>

533 HOL.equal x y \<and> (\<forall>z \<in> UNIV.

534 case f z of

535 None \<Rightarrow> (case g z of None \<Rightarrow> True | Some _ \<Rightarrow> False)

536 | Some a \<Rightarrow> (case g z of None \<Rightarrow> False | Some b \<Rightarrow> HOL.equal a b))" (is ?env)

537 and "HOL.equal (Val a) (Val b) \<longleftrightarrow> HOL.equal a b"

538 and "HOL.equal (Val a) (Env y g) \<longleftrightarrow> False"

539 and "HOL.equal (Env x f) (Val b) \<longleftrightarrow> False"

540 proof (unfold equal)

541 have "f = g \<longleftrightarrow>

542 (\<forall>z. case f z of

543 None \<Rightarrow> (case g z of None \<Rightarrow> True | Some _ \<Rightarrow> False)

544 | Some a \<Rightarrow> (case g z 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 ?rhs (is "\<forall>z. ?prop z")

550 show ?lhs

551 proof

552 fix z

553 from \<open>?rhs\<close> 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.

559 case f z of

560 None \<Rightarrow> (case g z of None \<Rightarrow> True | Some _ \<Rightarrow> False)

561 | Some a \<Rightarrow> (case g z of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp

562 qed simp_all

564 lemma [code nbe]: "HOL.equal (x :: (_, _, _) env) x \<longleftrightarrow> True"

565 by (fact equal_refl)

567 end