1 (* Title: HOL/Library/Nested_Environment.thy |
|
2 Author: Markus Wenzel, TU Muenchen |
|
3 *) |
|
4 |
|
5 header {* Nested environments *} |
|
6 |
|
7 theory Nested_Environment |
|
8 imports Main |
|
9 begin |
|
10 |
|
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 *} |
|
21 |
|
22 datatype ('a, 'b, 'c) env = |
|
23 Val 'a |
|
24 | Env 'b "'c => ('a, 'b, 'c) env option" |
|
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 |
|
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" |
|
56 |
|
57 hide_const lookup_option |
|
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 |
|
73 None => None |
|
74 | Some e => lookup e xs)" |
|
75 by (cases "es x") simp_all |
|
76 |
|
77 lemmas lookup_lookup_option.simps [simp del] |
|
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 |
|
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) |
|
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: |
|
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 |
|
136 |
|
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 |
|
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: |
|
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 |
|
195 |
|
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 *} |
|
201 |
|
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 |
|
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 |
|
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))" |
|
264 |
|
265 hide_const update_option |
|
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 |
|
289 None => None |
|
290 | Some e => Some (update (y # ys) opt e))))" |
|
291 by (cases "es x") simp_all |
|
292 |
|
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 |
|
296 |
|
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) |
|
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: |
|
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 |
|
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: |
|
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 |
|
414 |
|
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 |
|
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: |
|
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 |
|
520 |
|
521 text {* Environments and code generation *} |
|
522 |
|
523 lemma [code, code del]: |
|
524 "(HOL.equal :: (_, _, _) env \<Rightarrow> _) = HOL.equal" .. |
|
525 |
|
526 lemma equal_env_code [code]: |
|
527 fixes x y :: "'a\<Colon>equal" |
|
528 and f g :: "'c\<Colon>{equal, finite} \<Rightarrow> ('b\<Colon>equal, 'a, 'c) env option" |
|
529 shows "HOL.equal (Env x f) (Env y g) \<longleftrightarrow> |
|
530 HOL.equal x y \<and> (\<forall>z\<in>UNIV. case f z |
|
531 of None \<Rightarrow> (case g z |
|
532 of None \<Rightarrow> True | Some _ \<Rightarrow> False) |
|
533 | Some a \<Rightarrow> (case g z |
|
534 of None \<Rightarrow> False | Some b \<Rightarrow> HOL.equal a b))" (is ?env) |
|
535 and "HOL.equal (Val a) (Val b) \<longleftrightarrow> HOL.equal a b" |
|
536 and "HOL.equal (Val a) (Env y g) \<longleftrightarrow> False" |
|
537 and "HOL.equal (Env x f) (Val b) \<longleftrightarrow> False" |
|
538 proof (unfold equal) |
|
539 have "f = g \<longleftrightarrow> (\<forall>z. case f z |
|
540 of None \<Rightarrow> (case g z |
|
541 of None \<Rightarrow> True | Some _ \<Rightarrow> False) |
|
542 | Some a \<Rightarrow> (case g z |
|
543 of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" (is "?lhs = ?rhs") |
|
544 proof |
|
545 assume ?lhs |
|
546 then show ?rhs by (auto split: option.splits) |
|
547 next |
|
548 assume assm: ?rhs (is "\<forall>z. ?prop z") |
|
549 show ?lhs |
|
550 proof |
|
551 fix z |
|
552 from assm have "?prop z" .. |
|
553 then show "f z = g z" by (auto split: option.splits) |
|
554 qed |
|
555 qed |
|
556 then show "Env x f = Env y g \<longleftrightarrow> |
|
557 x = y \<and> (\<forall>z\<in>UNIV. case f z |
|
558 of None \<Rightarrow> (case g z |
|
559 of None \<Rightarrow> True | Some _ \<Rightarrow> False) |
|
560 | Some a \<Rightarrow> (case g z |
|
561 of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp |
|
562 qed simp_all |
|
563 |
|
564 lemma [code nbe]: |
|
565 "HOL.equal (x :: (_, _, _) env) x \<longleftrightarrow> True" |
|
566 by (fact equal_refl) |
|
567 |
|
568 lemma [code, code del]: |
|
569 "(Code_Evaluation.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Evaluation.term_of" .. |
|
570 |
|
571 end |
|