author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44703  f2bfe19239bc 
child 49679  835d55b4fc8c 
permissions  rwrr 
44236
b73b7832b384
moved theory Nested_Environment to HOLUnix (a bit too specific for HOLLibrary);
wenzelm
parents:
38857
diff
changeset

1 
(* Title: HOL/Unix/Nested_Environment.thy 
10943  2 
Author: Markus Wenzel, TU Muenchen 
3 
*) 

4 

14706  5 
header {* Nested environments *} 
10943  6 

15131  7 
theory Nested_Environment 
30663
0b6aff7451b2
Main is (Complex_Main) base entry point in library theories
haftmann
parents:
28562
diff
changeset

8 
imports Main 
15131  9 
begin 
10943  10 

11 
text {* 

44703  12 
Consider a partial function @{term [source] "e :: 'a \<Rightarrow> 'b option"}; 
10943  13 
this may be understood as an \emph{environment} mapping indexes 
14 
@{typ 'a} to optional entry values @{typ 'b} (cf.\ the basic theory 

10948  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. 

10943  20 
*} 
21 

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

23 
Val 'a 

44703  24 
 Env 'b "'c \<Rightarrow> ('a, 'b, 'c) env option" 
10943  25 

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 
*} 

34 

35 

36 
subsection {* The lookup operation *} 

37 

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 
*} 

45 

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

44601  48 
where 
34941  49 
"lookup (Val a) xs = (if xs = [] then Some (Val a) else None)" 
50 
 "lookup (Env b es) xs = 

51 
(case xs of 

44703  52 
[] \<Rightarrow> Some (Env b es) 
53 
 y # ys \<Rightarrow> lookup_option (es y) ys)" 

34941  54 
 "lookup_option None xs = None" 
55 
 "lookup_option (Some e) xs = lookup e xs" 

10943  56 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
34941
diff
changeset

57 
hide_const lookup_option 
10943  58 

59 
text {* 

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

61 
the following equalities. 

62 
*} 

63 

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

65 
by (cases e) simp_all 

66 

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

68 
by simp 

69 

70 
theorem lookup_env_cons: 

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

72 
(case es x of 

44703  73 
None \<Rightarrow> None 
74 
 Some e \<Rightarrow> lookup e xs)" 

10943  75 
by (cases "es x") simp_all 
76 

34941  77 
lemmas lookup_lookup_option.simps [simp del] 
10943  78 
and lookup_simps [simp] = lookup_nil lookup_val_cons lookup_env_cons 
79 

80 
theorem lookup_eq: 

81 
"lookup env xs = 

82 
(case xs of 

44703  83 
[] \<Rightarrow> Some env 
84 
 x # xs \<Rightarrow> 

10943  85 
(case env of 
44703  86 
Val a \<Rightarrow> None 
87 
 Env b es \<Rightarrow> 

10943  88 
(case es x of 
44703  89 
None \<Rightarrow> None 
90 
 Some e \<Rightarrow> lookup e xs)))" 

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

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 
*} 

99 

100 
theorem lookup_append_none: 

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

23394  103 
using assms 
20503  104 
proof (induct xs arbitrary: env) 
18153  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 

10943  114 
next 
18153  115 
case (Env b es) 
116 
show ?thesis 

117 
proof (cases "es x") 

118 
case None 

119 
with Env show ?thesis by simp 

10943  120 
next 
18153  121 
case (Some e) 
122 
note es = `es x = Some e` 

10943  123 
show ?thesis 
18153  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 

10943  128 
next 
18153  129 
case Some 
130 
with Env es have False using Cons.prems by simp 

131 
then show ?thesis .. 

10943  132 
qed 
133 
qed 

18153  134 
qed 
10943  135 
qed 
136 

137 
theorem lookup_append_some: 

18153  138 
assumes "lookup env xs = Some e" 
139 
shows "lookup env (xs @ ys) = lookup e ys" 

23394  140 
using assms 
20503  141 
proof (induct xs arbitrary: env e) 
18153  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 .. 

10943  153 
next 
18153  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 .. 

10943  160 
next 
18153  161 
case (Some e') 
162 
note es = `es x = Some e'` 

10943  163 
show ?thesis 
18153  164 
proof (cases "lookup e' xs") 
165 
case None 

166 
with asm Env es have False by simp 

167 
then show ?thesis .. 

10943  168 
next 
18153  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 

10943  174 
qed 
175 
qed 

18153  176 
qed 
10943  177 
qed 
178 

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 
*} 

185 

186 
theorem lookup_some_append: 

18153  187 
assumes "lookup env (xs @ ys) = Some e" 
188 
shows "\<exists>e. lookup env xs = Some e" 

10943  189 
proof  
23394  190 
from assms have "lookup env (xs @ ys) \<noteq> None" by simp 
18153  191 
then have "lookup env xs \<noteq> None" 
10943  192 
by (rule contrapos_nn) (simp only: lookup_append_none) 
18576  193 
then show ?thesis by (simp) 
10943  194 
qed 
195 

196 
text {* 

197 
The subsequent statement describes in more detail how a successful 

198 
@{term lookup} with a nonempty path results in a certain situation 

199 
at any upper position. 

200 
*} 

201 

18153  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" 

23394  208 
using assms 
20503  209 
proof (induct xs arbitrary: env e) 
18153  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 

10943  236 
qed 
237 

238 

239 
subsection {* The update operation *} 

240 

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 
*} 

247 

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

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

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

44601  252 
where 
253 
"update xs opt (Val a) = 

44703  254 
(if xs = [] then (case opt of None \<Rightarrow> Val a  Some e \<Rightarrow> e) 
44601  255 
else Val a)" 
256 
 "update xs opt (Env b es) = 

257 
(case xs of 

44703  258 
[] \<Rightarrow> (case opt of None \<Rightarrow> Env b es  Some e \<Rightarrow> e) 
259 
 y # ys \<Rightarrow> Env b (es (y := update_option ys opt (es y))))" 

44601  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))" 

10943  264 

36176
3fe7e97ccca8
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact'  frees some popular keywords;
wenzelm
parents:
34941
diff
changeset

265 
hide_const update_option 
10943  266 

267 
text {* 

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

269 
the following equalities. 

270 
*} 

271 

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

273 
by (cases env) simp_all 

274 

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

276 
by (cases env) simp_all 

277 

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

279 
by simp 

280 

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 

284 

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 

44703  289 
None \<Rightarrow> None 
290 
 Some e \<Rightarrow> Some (update (y # ys) opt e))))" 

10943  291 
by (cases "es x") simp_all 
292 

34941  293 
lemmas update_update_option.simps [simp del] 
10943  294 
and update_simps [simp] = update_nil_none update_nil_some 
295 
update_cons_val update_cons_nil_env update_cons_cons_env 

296 

297 
lemma update_eq: 

298 
"update xs opt env = 

299 
(case xs of 

44703  300 
[] \<Rightarrow> 
10943  301 
(case opt of 
44703  302 
None \<Rightarrow> env 
303 
 Some e \<Rightarrow> e) 

304 
 x # xs \<Rightarrow> 

10943  305 
(case env of 
44703  306 
Val a \<Rightarrow> Val a 
307 
 Env b es \<Rightarrow> 

10943  308 
(case xs of 
44703  309 
[] \<Rightarrow> Env b (es (x := opt)) 
310 
 y # ys \<Rightarrow> 

10943  311 
Env b (es (x := 
312 
(case es x of 

44703  313 
None \<Rightarrow> None 
314 
 Some e \<Rightarrow> Some (update (y # ys) opt e)))))))" 

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

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 
*} 

322 

323 
theorem lookup_update_some: 

18153  324 
assumes "lookup env xs = Some e" 
325 
shows "lookup (update xs (Some env') env) xs = Some env'" 

23394  326 
using assms 
20503  327 
proof (induct xs arbitrary: env e) 
18153  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 .. 

10943  340 
next 
18153  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 .. 

10943  347 
next 
18153  348 
case (Some e') 
349 
note es = `es x = Some e'` 

10943  350 
show ?thesis 
18153  351 
proof (cases xs) 
352 
case Nil 

353 
with Env show ?thesis by simp 

10943  354 
next 
18153  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 

10943  359 
qed 
360 
qed 

18153  361 
qed 
10943  362 
qed 
363 

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 
*} 

371 

372 
theorem update_append_none: 

18153  373 
assumes "lookup env xs = None" 
374 
shows "update (xs @ y # ys) opt env = env" 

23394  375 
using assms 
20503  376 
proof (induct xs arbitrary: env) 
18153  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 

10943  388 
next 
18153  389 
case (Env b es) 
390 
show ?thesis 

391 
proof (cases "es x") 

392 
case None 

393 
note es = `es x = None` 

10943  394 
show ?thesis 
18153  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 .. 

10943  404 
next 
18153  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) 

10943  410 
qed 
411 
qed 

18153  412 
qed 
10943  413 
qed 
414 

415 
theorem update_append_some: 

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

23394  418 
using assms 
20503  419 
proof (induct xs arbitrary: env e) 
18153  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 .. 

10943  433 
next 
18153  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 .. 

10943  440 
next 
18153  441 
case (Some e') 
442 
note es = `es x = Some e'` 

10943  443 
show ?thesis 
18153  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 

10943  448 
next 
18153  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 

10943  454 
qed 
455 
qed 

18153  456 
qed 
10943  457 
qed 
458 

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 
*} 

465 

466 
theorem lookup_update_other: 

18153  467 
assumes neq: "y \<noteq> (z::'c)" 
468 
shows "lookup (update (xs @ z # zs) opt env) (xs @ y # ys) = 

10943  469 
lookup env (xs @ y # ys)" 
20503  470 
proof (induct xs arbitrary: env) 
18153  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 

10943  482 
next 
18153  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 

10943  499 
show ?thesis 
18153  500 
proof (cases "es x") 
501 
case None 

502 
with Env Nil show ?thesis by simp 

10943  503 
next 
18153  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 

10943  516 
qed 
517 
qed 

18153  518 
qed 
10943  519 
qed 
520 

44267  521 

522 
subsection {* Code generation *} 

24433
4a405457e9d6
added explicit equation for equality of nested environments
haftmann
parents:
23394
diff
changeset

523 

28562  524 
lemma [code, code del]: 
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36176
diff
changeset

525 
"(HOL.equal :: (_, _, _) env \<Rightarrow> _) = HOL.equal" .. 
24433
4a405457e9d6
added explicit equation for equality of nested environments
haftmann
parents:
23394
diff
changeset

526 

38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36176
diff
changeset

527 
lemma equal_env_code [code]: 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36176
diff
changeset

528 
fixes x y :: "'a\<Colon>equal" 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36176
diff
changeset

529 
and f g :: "'c\<Colon>{equal, finite} \<Rightarrow> ('b\<Colon>equal, 'a, 'c) env option" 
44267  530 
shows 
531 
"HOL.equal (Env x f) (Env y g) \<longleftrightarrow> 

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

533 
case f z of 

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

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

38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36176
diff
changeset

536 
and "HOL.equal (Val a) (Val b) \<longleftrightarrow> HOL.equal a b" 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36176
diff
changeset

537 
and "HOL.equal (Val a) (Env y g) \<longleftrightarrow> False" 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36176
diff
changeset

538 
and "HOL.equal (Env x f) (Val b) \<longleftrightarrow> False" 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36176
diff
changeset

539 
proof (unfold equal) 
44267  540 
have "f = g \<longleftrightarrow> 
541 
(\<forall>z. case f z of 

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

543 
 Some a \<Rightarrow> (case g z of None \<Rightarrow> False  Some b \<Rightarrow> a = b))" (is "?lhs = ?rhs") 

24433
4a405457e9d6
added explicit equation for equality of nested environments
haftmann
parents:
23394
diff
changeset

544 
proof 
4a405457e9d6
added explicit equation for equality of nested environments
haftmann
parents:
23394
diff
changeset

545 
assume ?lhs 
4a405457e9d6
added explicit equation for equality of nested environments
haftmann
parents:
23394
diff
changeset

546 
then show ?rhs by (auto split: option.splits) 
4a405457e9d6
added explicit equation for equality of nested environments
haftmann
parents:
23394
diff
changeset

547 
next 
44267  548 
assume ?rhs (is "\<forall>z. ?prop z") 
44236
b73b7832b384
moved theory Nested_Environment to HOLUnix (a bit too specific for HOLLibrary);
wenzelm
parents:
38857
diff
changeset

549 
show ?lhs 
24433
4a405457e9d6
added explicit equation for equality of nested environments
haftmann
parents:
23394
diff
changeset

550 
proof 
4a405457e9d6
added explicit equation for equality of nested environments
haftmann
parents:
23394
diff
changeset

551 
fix z 
44267  552 
from `?rhs` have "?prop z" .. 
24433
4a405457e9d6
added explicit equation for equality of nested environments
haftmann
parents:
23394
diff
changeset

553 
then show "f z = g z" by (auto split: option.splits) 
4a405457e9d6
added explicit equation for equality of nested environments
haftmann
parents:
23394
diff
changeset

554 
qed 
4a405457e9d6
added explicit equation for equality of nested environments
haftmann
parents:
23394
diff
changeset

555 
qed 
26513  556 
then show "Env x f = Env y g \<longleftrightarrow> 
44267  557 
x = y \<and> (\<forall>z\<in>UNIV. 
558 
case f z of 

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

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

24433
4a405457e9d6
added explicit equation for equality of nested environments
haftmann
parents:
23394
diff
changeset

561 
qed simp_all 
4a405457e9d6
added explicit equation for equality of nested environments
haftmann
parents:
23394
diff
changeset

562 

38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36176
diff
changeset

563 
lemma [code nbe]: 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36176
diff
changeset

564 
"HOL.equal (x :: (_, _, _) env) x \<longleftrightarrow> True" 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36176
diff
changeset

565 
by (fact equal_refl) 
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
36176
diff
changeset

566 

28562  567 
lemma [code, code del]: 
44267  568 
"(Code_Evaluation.term_of :: 
569 
('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = 

570 
Code_Evaluation.term_of" .. 

28228  571 

10943  572 
end 