1 (* Title: HOL/Unix/Nested_Environment.thy
2 Author: Markus Wenzel, TU Muenchen
5 header {* Nested environments *}
7 theory Nested_Environment
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.
22 datatype ('a, 'b, 'c) env =
24 | Env 'b "'c => ('a, 'b, 'c) env option"
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.
36 subsection {* The lookup operation *}
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
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 =
53 | y # ys => lookup_option (es y) ys)"
54 | "lookup_option None xs = None"
55 | "lookup_option (Some e) xs = lookup e xs"
57 hide_const lookup_option
60 \medskip The characteristic cases of @{term lookup} are expressed by
61 the following equalities.
64 theorem lookup_nil: "lookup e [] = Some e"
67 theorem lookup_val_cons: "lookup (Val a) (x # xs) = None"
70 theorem lookup_env_cons:
71 "lookup (Env b es) (x # xs) =
74 | Some e => lookup e xs)"
75 by (cases "es x") simp_all
77 lemmas lookup_lookup_option.simps [simp del]
78 and lookup_simps [simp] = lookup_nil lookup_val_cons lookup_env_cons
90 | Some e => lookup e xs)))"
91 by (simp split: list.split env.split)
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
100 theorem lookup_append_none:
101 assumes "lookup env xs = None"
102 shows "lookup env (xs @ ys) = None"
104 proof (induct xs arbitrary: env)
106 then have False by simp
113 then show ?thesis by simp
119 with Env show ?thesis by simp
122 note es = `es x = Some e`
124 proof (cases "lookup e xs")
126 then have "lookup e (xs @ ys) = None" by (rule Cons.hyps)
127 with Env Some show ?thesis by simp
130 with Env es have False using Cons.prems by simp
137 theorem lookup_append_some:
138 assumes "lookup env xs = Some e"
139 shows "lookup env (xs @ ys) = lookup e ys"
141 proof (induct xs arbitrary: env e)
143 then have "env = e" by simp
144 then show "lookup env ([] @ ys) = lookup e ys" by simp
147 note asm = `lookup env (x # xs) = Some e`
148 show "lookup env ((x # xs) @ ys) = lookup e ys"
151 with asm have False by simp
158 with asm Env have False by simp
162 note es = `es x = Some e'`
164 proof (cases "lookup e' xs")
166 with asm Env es have False by simp
170 with asm Env es have "lookup e' xs = Some e"
172 then have "lookup e' (xs @ ys) = lookup e ys" by (rule Cons.hyps)
173 with Env es show ?thesis by simp
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.
186 theorem lookup_some_append:
187 assumes "lookup env (xs @ ys) = Some e"
188 shows "\<exists>e. lookup env xs = Some e"
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)
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.
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"
209 proof (induct xs arbitrary: env e)
211 from Nil.prems have "lookup env (y # ys) = Some e"
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
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"
233 from env es' upper' have "lookup env (x # xs) = Some (Env b'' es'')"
235 with es'' look'' show ?case by blast
239 subsection {* The update operation *}
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.
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)
256 | "update xs opt (Env b es) =
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))"
265 hide_const update_option
268 \medskip The characteristic cases of @{term update} are expressed by
269 the following equalities.
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"
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) =
290 | Some e => Some (update (y # ys) opt e))))"
291 by (cases "es x") simp_all
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
309 [] => Env b (es (x := opt))
314 | Some e => Some (update (y # ys) opt e)))))))"
315 by (simp split: list.split env.split option.split)
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.
323 theorem lookup_update_some:
324 assumes "lookup env xs = Some e"
325 shows "lookup (update xs (Some env') env) xs = Some env'"
327 proof (induct xs arbitrary: env e)
329 then have "env = e" by simp
330 then show ?case by simp
334 and asm = `lookup env (x # xs) = Some e`
338 with asm have False by simp
345 with asm Env have False by simp
349 note es = `es x = Some e'`
353 with Env show ?thesis by simp
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
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.
372 theorem update_append_none:
373 assumes "lookup env xs = None"
374 shows "update (xs @ y # ys) opt env = env"
376 proof (induct xs arbitrary: env)
378 then have False by simp
383 and asm = `lookup env (x # xs) = None`
384 show "update ((x # xs) @ y # ys) opt env = env"
387 then show ?thesis by simp
393 note es = `es x = None`
395 by (cases xs) (simp_all add: es Env fun_upd_idem_iff)
398 note es = `es x = Some e`
402 with asm Env Some have False by simp
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)
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)"
419 proof (induct xs arbitrary: env e)
421 then have "env = e" by simp
422 then show ?case by simp
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)"
431 with asm have False by simp
438 with asm Env have False by simp
442 note es = `es x = Some e'`
446 with asm Env es have "e = e'" by simp
447 with Env es Nil show ?thesis by simp
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
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
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)
475 then show ?thesis by simp
481 with neq Env show ?thesis by simp
484 with neq Env show ?thesis by simp
493 then show ?thesis by simp
502 with Env Nil show ?thesis by simp
505 with neq hyp and Env Nil show ?thesis by simp
512 with Env Cons show ?thesis by simp
515 with neq hyp and Env Cons show ?thesis by simp
522 subsection {* Code generation *}
524 lemma [code, code del]:
525 "(HOL.equal :: (_, _, _) env \<Rightarrow> _) = HOL.equal" ..
527 lemma equal_env_code [code]:
528 fixes x y :: "'a\<Colon>equal"
529 and f g :: "'c\<Colon>{equal, finite} \<Rightarrow> ('b\<Colon>equal, 'a, 'c) env option"
531 "HOL.equal (Env x f) (Env y g) \<longleftrightarrow>
532 HOL.equal x y \<and> (\<forall>z \<in> UNIV.
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)
536 and "HOL.equal (Val a) (Val b) \<longleftrightarrow> HOL.equal a b"
537 and "HOL.equal (Val a) (Env y g) \<longleftrightarrow> False"
538 and "HOL.equal (Env x f) (Val b) \<longleftrightarrow> False"
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")
546 then show ?rhs by (auto split: option.splits)
548 assume ?rhs (is "\<forall>z. ?prop z")
552 from `?rhs` have "?prop z" ..
553 then show "f z = g z" by (auto split: option.splits)
556 then show "Env x f = Env y g \<longleftrightarrow>
557 x = y \<and> (\<forall>z\<in>UNIV.
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
564 "HOL.equal (x :: (_, _, _) env) x \<longleftrightarrow> True"
567 lemma [code, code del]:
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" ..