10943
|
1 |
(* Title: HOL/Library/Nested_Environment.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Markus Wenzel, TU Muenchen
|
|
4 |
*)
|
|
5 |
|
14706
|
6 |
header {* Nested environments *}
|
10943
|
7 |
|
15131
|
8 |
theory Nested_Environment
|
15140
|
9 |
imports Main
|
15131
|
10 |
begin
|
10943
|
11 |
|
|
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
|
10948
|
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.
|
10943
|
21 |
*}
|
|
22 |
|
|
23 |
datatype ('a, 'b, 'c) env =
|
|
24 |
Val 'a
|
|
25 |
| Env 'b "'c => ('a, 'b, 'c) env option"
|
|
26 |
|
|
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 |
*}
|
|
35 |
|
|
36 |
|
|
37 |
subsection {* The lookup operation *}
|
|
38 |
|
|
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 |
*}
|
|
46 |
|
|
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"
|
|
50 |
|
|
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"
|
|
59 |
|
|
60 |
hide const lookup_option
|
|
61 |
|
|
62 |
text {*
|
|
63 |
\medskip The characteristic cases of @{term lookup} are expressed by
|
|
64 |
the following equalities.
|
|
65 |
*}
|
|
66 |
|
|
67 |
theorem lookup_nil: "lookup e [] = Some e"
|
|
68 |
by (cases e) simp_all
|
|
69 |
|
|
70 |
theorem lookup_val_cons: "lookup (Val a) (x # xs) = None"
|
|
71 |
by simp
|
|
72 |
|
|
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
|
|
79 |
|
|
80 |
lemmas lookup.simps [simp del]
|
|
81 |
and lookup_simps [simp] = lookup_nil lookup_val_cons lookup_env_cons
|
|
82 |
|
|
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)
|
|
95 |
|
|
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 |
*}
|
|
102 |
|
|
103 |
theorem lookup_append_none:
|
18153
|
104 |
assumes "lookup env xs = None"
|
|
105 |
shows "lookup env (xs @ ys) = None"
|
|
106 |
using prems
|
|
107 |
proof (induct xs fixing: 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
|
10943
|
117 |
next
|
18153
|
118 |
case (Env b es)
|
|
119 |
show ?thesis
|
|
120 |
proof (cases "es x")
|
|
121 |
case None
|
|
122 |
with Env show ?thesis by simp
|
10943
|
123 |
next
|
18153
|
124 |
case (Some e)
|
|
125 |
note es = `es x = Some e`
|
10943
|
126 |
show ?thesis
|
18153
|
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
|
10943
|
131 |
next
|
18153
|
132 |
case Some
|
|
133 |
with Env es have False using Cons.prems by simp
|
|
134 |
then show ?thesis ..
|
10943
|
135 |
qed
|
|
136 |
qed
|
18153
|
137 |
qed
|
10943
|
138 |
qed
|
|
139 |
|
|
140 |
theorem lookup_append_some:
|
18153
|
141 |
assumes "lookup env xs = Some e"
|
|
142 |
shows "lookup env (xs @ ys) = lookup e ys"
|
|
143 |
using prems
|
|
144 |
proof (induct xs fixing: 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 ..
|
10943
|
156 |
next
|
18153
|
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 ..
|
10943
|
163 |
next
|
18153
|
164 |
case (Some e')
|
|
165 |
note es = `es x = Some e'`
|
10943
|
166 |
show ?thesis
|
18153
|
167 |
proof (cases "lookup e' xs")
|
|
168 |
case None
|
|
169 |
with asm Env es have False by simp
|
|
170 |
then show ?thesis ..
|
10943
|
171 |
next
|
18153
|
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
|
10943
|
177 |
qed
|
|
178 |
qed
|
18153
|
179 |
qed
|
10943
|
180 |
qed
|
|
181 |
|
|
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 |
*}
|
|
188 |
|
|
189 |
theorem lookup_some_append:
|
18153
|
190 |
assumes "lookup env (xs @ ys) = Some e"
|
|
191 |
shows "\<exists>e. lookup env xs = Some e"
|
10943
|
192 |
proof -
|
18153
|
193 |
from prems have "lookup env (xs @ ys) \<noteq> None" by simp
|
|
194 |
then have "lookup env xs \<noteq> None"
|
10943
|
195 |
by (rule contrapos_nn) (simp only: lookup_append_none)
|
18153
|
196 |
then show ?thesis by simp
|
10943
|
197 |
qed
|
|
198 |
|
|
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 |
*}
|
|
204 |
|
18153
|
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 prems
|
|
212 |
proof (induct xs fixing: 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
|
10943
|
239 |
qed
|
|
240 |
|
|
241 |
|
|
242 |
subsection {* The update operation *}
|
|
243 |
|
|
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 |
*}
|
|
250 |
|
|
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"
|
|
256 |
|
|
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))"
|
|
269 |
|
|
270 |
hide const update_option
|
|
271 |
|
|
272 |
text {*
|
|
273 |
\medskip The characteristic cases of @{term update} are expressed by
|
|
274 |
the following equalities.
|
|
275 |
*}
|
|
276 |
|
|
277 |
theorem update_nil_none: "update [] None env = env"
|
|
278 |
by (cases env) simp_all
|
|
279 |
|
|
280 |
theorem update_nil_some: "update [] (Some e) env = e"
|
|
281 |
by (cases env) simp_all
|
|
282 |
|
|
283 |
theorem update_cons_val: "update (x # xs) opt (Val a) = Val a"
|
|
284 |
by simp
|
|
285 |
|
|
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
|
|
289 |
|
|
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
|
|
297 |
|
|
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
|
|
301 |
|
|
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)
|
|
321 |
|
|
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 |
*}
|
|
327 |
|
|
328 |
theorem lookup_update_some:
|
18153
|
329 |
assumes "lookup env xs = Some e"
|
|
330 |
shows "lookup (update xs (Some env') env) xs = Some env'"
|
|
331 |
using prems
|
|
332 |
proof (induct xs fixing: 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 ..
|
10943
|
345 |
next
|
18153
|
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 ..
|
10943
|
352 |
next
|
18153
|
353 |
case (Some e')
|
|
354 |
note es = `es x = Some e'`
|
10943
|
355 |
show ?thesis
|
18153
|
356 |
proof (cases xs)
|
|
357 |
case Nil
|
|
358 |
with Env show ?thesis by simp
|
10943
|
359 |
next
|
18153
|
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
|
10943
|
364 |
qed
|
|
365 |
qed
|
18153
|
366 |
qed
|
10943
|
367 |
qed
|
|
368 |
|
|
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 |
*}
|
|
376 |
|
|
377 |
theorem update_append_none:
|
18153
|
378 |
assumes "lookup env xs = None"
|
|
379 |
shows "update (xs @ y # ys) opt env = env"
|
|
380 |
using prems
|
|
381 |
proof (induct xs fixing: 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
|
10943
|
393 |
next
|
18153
|
394 |
case (Env b es)
|
|
395 |
show ?thesis
|
|
396 |
proof (cases "es x")
|
|
397 |
case None
|
|
398 |
note es = `es x = None`
|
10943
|
399 |
show ?thesis
|
18153
|
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 ..
|
10943
|
409 |
next
|
18153
|
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)
|
10943
|
415 |
qed
|
|
416 |
qed
|
18153
|
417 |
qed
|
10943
|
418 |
qed
|
|
419 |
|
|
420 |
theorem update_append_some:
|
18153
|
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 prems
|
|
424 |
proof (induct xs fixing: 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 ..
|
10943
|
438 |
next
|
18153
|
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 ..
|
10943
|
445 |
next
|
18153
|
446 |
case (Some e')
|
|
447 |
note es = `es x = Some e'`
|
10943
|
448 |
show ?thesis
|
18153
|
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
|
10943
|
453 |
next
|
18153
|
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
|
10943
|
459 |
qed
|
|
460 |
qed
|
18153
|
461 |
qed
|
10943
|
462 |
qed
|
|
463 |
|
|
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 |
*}
|
|
470 |
|
|
471 |
theorem lookup_update_other:
|
18153
|
472 |
assumes neq: "y \<noteq> (z::'c)"
|
|
473 |
shows "lookup (update (xs @ z # zs) opt env) (xs @ y # ys) =
|
10943
|
474 |
lookup env (xs @ y # ys)"
|
18153
|
475 |
proof (induct xs fixing: 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
|
10943
|
487 |
next
|
18153
|
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
|
10943
|
504 |
show ?thesis
|
18153
|
505 |
proof (cases "es x")
|
|
506 |
case None
|
|
507 |
with Env Nil show ?thesis by simp
|
10943
|
508 |
next
|
18153
|
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
|
10943
|
521 |
qed
|
|
522 |
qed
|
18153
|
523 |
qed
|
10943
|
524 |
qed
|
|
525 |
|
|
526 |
end
|