author | wenzelm |

Fri Jan 19 23:53:07 2001 +0100 (2001-01-19) | |

changeset 10943 | 3a610d34eb9e |

parent 10942 | 6bbc41330b68 |

child 10944 | 710ddb9e8b5e |

added HOL/Library/Nested_Environment.thy;

src/HOL/IsaMakefile | file | annotate | diff | revisions | |

src/HOL/Library/Library.thy | file | annotate | diff | revisions | |

src/HOL/Library/Nested_Environment.thy | file | annotate | diff | revisions |

1.1 --- a/src/HOL/IsaMakefile Fri Jan 19 23:28:50 2001 +0100 1.2 +++ b/src/HOL/IsaMakefile Fri Jan 19 23:53:07 2001 +0100 1.3 @@ -179,7 +179,7 @@ 1.4 $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \ 1.5 Library/Library.thy Library/List_Prefix.thy Library/Multiset.thy \ 1.6 Library/Quotient.thy Library/Ring_and_Field.thy Library/README.html \ 1.7 - Library/Rational_Numbers.thy Library/ROOT.ML \ 1.8 + Library/Nested_Environment.thy Library/Rational_Numbers.thy Library/ROOT.ML \ 1.9 Library/While_Combinator.thy Library/While_Combinator_Example.thy 1.10 @$(ISATOOL) usedir $(OUT)/HOL Library 1.11

2.1 --- a/src/HOL/Library/Library.thy Fri Jan 19 23:28:50 2001 +0100 2.2 +++ b/src/HOL/Library/Library.thy Fri Jan 19 23:53:07 2001 +0100 2.3 @@ -4,6 +4,7 @@ 2.4 Ring_and_Field + 2.5 Rational_Numbers + 2.6 List_Prefix + 2.7 + Nested_Environment + 2.8 Accessible_Part + 2.9 Multiset + 2.10 While_Combinator + While_Combinator_Example:

3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 3.2 +++ b/src/HOL/Library/Nested_Environment.thy Fri Jan 19 23:53:07 2001 +0100 3.3 @@ -0,0 +1,550 @@ 3.4 +(* Title: HOL/Library/Nested_Environment.thy 3.5 + ID: $Id$ 3.6 + Author: Markus Wenzel, TU Muenchen 3.7 + License: GPL (GNU GENERAL PUBLIC LICENSE) 3.8 +*) 3.9 + 3.10 +header {* 3.11 + \title{Nested environments} 3.12 + \author{Markus Wenzel} 3.13 +*} 3.14 + 3.15 +theory Nested_Environment = Main: 3.16 + 3.17 +text {* 3.18 + Consider a partial function @{term [source] "e :: 'a => 'b option"}; 3.19 + this may be understood as an \emph{environment} mapping indexes 3.20 + @{typ 'a} to optional entry values @{typ 'b} (cf.\ the basic theory 3.21 + @{text 3.22 + Map}\footnote{\url{http://isabelle.in.tum.de/library/HOL/Map.html}} 3.23 + of Isabelle/HOL). This basic idea is easily generalized to that of 3.24 + a \emph{nested environment}, where entries may be either basic 3.25 + values or again proper environments. Then each entry is accessed by 3.26 + a \emph{path}, i.e.\ a list of indexes leading to its position 3.27 + within the structure. 3.28 +*} 3.29 + 3.30 +datatype ('a, 'b, 'c) env = 3.31 + Val 'a 3.32 + | Env 'b "'c => ('a, 'b, 'c) env option" 3.33 + 3.34 +text {* 3.35 + \medskip In the type @{typ "('a, 'b, 'c) env"} the parameter @{typ 3.36 + 'a} refers to basic values (occurring in terminal positions), type 3.37 + @{typ 'b} to values associated with proper (inner) environments, and 3.38 + type @{typ 'c} with the index type for branching. Note that there 3.39 + is no restriction on any of these types. In particular, arbitrary 3.40 + branching may yield rather large (transfinite) tree structures. 3.41 +*} 3.42 + 3.43 + 3.44 +subsection {* The lookup operation *} 3.45 + 3.46 +text {* 3.47 + Lookup in nested environments works by following a given path of 3.48 + index elements, leading to an optional result (a terminal value or 3.49 + nested environment). A \emph{defined position} within a nested 3.50 + environment is one where @{term lookup} at its path does not yield 3.51 + @{term None}. 3.52 +*} 3.53 + 3.54 +consts 3.55 + lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option" 3.56 + lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option" 3.57 + 3.58 +primrec (lookup) 3.59 + "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)" 3.60 + "lookup (Env b es) xs = 3.61 + (case xs of 3.62 + [] => Some (Env b es) 3.63 + | y # ys => lookup_option (es y) ys)" 3.64 + "lookup_option None xs = None" 3.65 + "lookup_option (Some e) xs = lookup e xs" 3.66 + 3.67 +hide const lookup_option 3.68 + 3.69 +text {* 3.70 + \medskip The characteristic cases of @{term lookup} are expressed by 3.71 + the following equalities. 3.72 +*} 3.73 + 3.74 +theorem lookup_nil: "lookup e [] = Some e" 3.75 + by (cases e) simp_all 3.76 + 3.77 +theorem lookup_val_cons: "lookup (Val a) (x # xs) = None" 3.78 + by simp 3.79 + 3.80 +theorem lookup_env_cons: 3.81 + "lookup (Env b es) (x # xs) = 3.82 + (case es x of 3.83 + None => None 3.84 + | Some e => lookup e xs)" 3.85 + by (cases "es x") simp_all 3.86 + 3.87 +lemmas lookup.simps [simp del] 3.88 + and lookup_simps [simp] = lookup_nil lookup_val_cons lookup_env_cons 3.89 + 3.90 +theorem lookup_eq: 3.91 + "lookup env xs = 3.92 + (case xs of 3.93 + [] => Some env 3.94 + | x # xs => 3.95 + (case env of 3.96 + Val a => None 3.97 + | Env b es => 3.98 + (case es x of 3.99 + None => None 3.100 + | Some e => lookup e xs)))" 3.101 + by (simp split: list.split env.split) 3.102 + 3.103 +text {* 3.104 + \medskip Displaced @{term lookup} operations, relative to a certain 3.105 + base path prefix, may be reduced as follows. There are two cases, 3.106 + depending whether the environment actually extends far enough to 3.107 + follow the base path. 3.108 +*} 3.109 + 3.110 +theorem lookup_append_none: 3.111 + "!!env. lookup env xs = None ==> lookup env (xs @ ys) = None" 3.112 + (is "PROP ?P xs") 3.113 +proof (induct xs) 3.114 + fix env :: "('a, 'b, 'c) env" 3.115 + { 3.116 + assume "lookup env [] = None" 3.117 + hence False by simp 3.118 + thus "lookup env ([] @ ys) = None" .. 3.119 + next 3.120 + fix x xs 3.121 + assume hyp: "PROP ?P xs" 3.122 + assume asm: "lookup env (x # xs) = None" 3.123 + show "lookup env ((x # xs) @ ys) = None" 3.124 + proof (cases env) 3.125 + case Val 3.126 + thus ?thesis by simp 3.127 + next 3.128 + fix b es assume env: "env = Env b es" 3.129 + show ?thesis 3.130 + proof (cases "es x") 3.131 + assume "es x = None" 3.132 + with env show ?thesis by simp 3.133 + next 3.134 + fix e assume es: "es x = Some e" 3.135 + show ?thesis 3.136 + proof (cases "lookup e xs") 3.137 + case None 3.138 + hence "lookup e (xs @ ys) = None" by (rule hyp) 3.139 + with env es show ?thesis by simp 3.140 + next 3.141 + case Some 3.142 + with asm env es have False by simp 3.143 + thus ?thesis .. 3.144 + qed 3.145 + qed 3.146 + qed 3.147 + } 3.148 +qed 3.149 + 3.150 +theorem lookup_append_some: 3.151 + "!!env e. lookup env xs = Some e ==> lookup env (xs @ ys) = lookup e ys" 3.152 + (is "PROP ?P xs") 3.153 +proof (induct xs) 3.154 + fix env e :: "('a, 'b, 'c) env" 3.155 + { 3.156 + assume "lookup env [] = Some e" 3.157 + hence "env = e" by simp 3.158 + thus "lookup env ([] @ ys) = lookup e ys" by simp 3.159 + next 3.160 + fix x xs 3.161 + assume hyp: "PROP ?P xs" 3.162 + assume asm: "lookup env (x # xs) = Some e" 3.163 + show "lookup env ((x # xs) @ ys) = lookup e ys" 3.164 + proof (cases env) 3.165 + fix a assume "env = Val a" 3.166 + with asm have False by simp 3.167 + thus ?thesis .. 3.168 + next 3.169 + fix b es assume env: "env = Env b es" 3.170 + show ?thesis 3.171 + proof (cases "es x") 3.172 + assume "es x = None" 3.173 + with asm env have False by simp 3.174 + thus ?thesis .. 3.175 + next 3.176 + fix e' assume es: "es x = Some e'" 3.177 + show ?thesis 3.178 + proof (cases "lookup e' xs") 3.179 + case None 3.180 + with asm env es have False by simp 3.181 + thus ?thesis .. 3.182 + next 3.183 + case Some 3.184 + with asm env es have "lookup e' xs = Some e" 3.185 + by simp 3.186 + hence "lookup e' (xs @ ys) = lookup e ys" by (rule hyp) 3.187 + with env es show ?thesis by simp 3.188 + qed 3.189 + qed 3.190 + qed 3.191 + } 3.192 +qed 3.193 + 3.194 +text {* 3.195 + \medskip Successful @{term lookup} deeper down an environment 3.196 + structure means we are able to peek further up as well. Note that 3.197 + this is basically just the contrapositive statement of @{thm 3.198 + [source] lookup_append_none} above. 3.199 +*} 3.200 + 3.201 +theorem lookup_some_append: 3.202 + "lookup env (xs @ ys) = Some e ==> \<exists>e. lookup env xs = Some e" 3.203 +proof - 3.204 + assume "lookup env (xs @ ys) = Some e" 3.205 + hence "lookup env (xs @ ys) \<noteq> None" by simp 3.206 + hence "lookup env xs \<noteq> None" 3.207 + by (rule contrapos_nn) (simp only: lookup_append_none) 3.208 + thus ?thesis by simp 3.209 +qed 3.210 + 3.211 +text {* 3.212 + The subsequent statement describes in more detail how a successful 3.213 + @{term lookup} with a non-empty path results in a certain situation 3.214 + at any upper position. 3.215 +*} 3.216 + 3.217 +theorem lookup_some_upper: "!!env e. 3.218 + lookup env (xs @ y # ys) = Some e ==> 3.219 + \<exists>b' es' env'. 3.220 + lookup env xs = Some (Env b' es') \<and> 3.221 + es' y = Some env' \<and> 3.222 + lookup env' ys = Some e" 3.223 + (is "PROP ?P xs" is "!!env e. ?A env e xs ==> ?C env e xs") 3.224 +proof (induct ?P xs) 3.225 + fix env e 3.226 + let ?A = "?A env e" and ?C = "?C env e" 3.227 + { 3.228 + assume "?A []" 3.229 + hence "lookup env (y # ys) = Some e" by simp 3.230 + then obtain b' es' env' where 3.231 + env: "env = Env b' es'" 3.232 + and es': "es' y = Some env'" 3.233 + and look': "lookup env' ys = Some e" 3.234 + by (auto simp add: lookup_eq split: option.splits env.splits) 3.235 + from env have "lookup env [] = Some (Env b' es')" by simp 3.236 + with es' look' show "?C []" by blast 3.237 + next 3.238 + fix x xs 3.239 + assume hyp: "PROP ?P xs" 3.240 + assume "?A (x # xs)" 3.241 + then obtain b' es' env' where 3.242 + env: "env = Env b' es'" 3.243 + and es': "es' x = Some env'" 3.244 + and look': "lookup env' (xs @ y # ys) = Some e" 3.245 + by (auto simp add: lookup_eq split: option.splits env.splits) 3.246 + from hyp [OF look'] obtain b'' es'' env'' where 3.247 + upper': "lookup env' xs = Some (Env b'' es'')" 3.248 + and es'': "es'' y = Some env''" 3.249 + and look'': "lookup env'' ys = Some e" 3.250 + by blast 3.251 + from env es' upper' have "lookup env (x # xs) = Some (Env b'' es'')" 3.252 + by simp 3.253 + with es'' look'' show "?C (x # xs)" by blast 3.254 + } 3.255 +qed 3.256 + 3.257 + 3.258 +subsection {* The update operation *} 3.259 + 3.260 +text {* 3.261 + Update at a certain position in a nested environment may either 3.262 + delete an existing entry, or overwrite an existing one. Note that 3.263 + update at undefined positions is simple absorbed, i.e.\ the 3.264 + environment is left unchanged. 3.265 +*} 3.266 + 3.267 +consts 3.268 + update :: "'c list => ('a, 'b, 'c) env option 3.269 + => ('a, 'b, 'c) env => ('a, 'b, 'c) env" 3.270 + update_option :: "'c list => ('a, 'b, 'c) env option 3.271 + => ('a, 'b, 'c) env option => ('a, 'b, 'c) env option" 3.272 + 3.273 +primrec (update) 3.274 + "update xs opt (Val a) = 3.275 + (if xs = [] then (case opt of None => Val a | Some e => e) 3.276 + else Val a)" 3.277 + "update xs opt (Env b es) = 3.278 + (case xs of 3.279 + [] => (case opt of None => Env b es | Some e => e) 3.280 + | y # ys => Env b (es (y := update_option ys opt (es y))))" 3.281 + "update_option xs opt None = 3.282 + (if xs = [] then opt else None)" 3.283 + "update_option xs opt (Some e) = 3.284 + (if xs = [] then opt else Some (update xs opt e))" 3.285 + 3.286 +hide const update_option 3.287 + 3.288 +text {* 3.289 + \medskip The characteristic cases of @{term update} are expressed by 3.290 + the following equalities. 3.291 +*} 3.292 + 3.293 +theorem update_nil_none: "update [] None env = env" 3.294 + by (cases env) simp_all 3.295 + 3.296 +theorem update_nil_some: "update [] (Some e) env = e" 3.297 + by (cases env) simp_all 3.298 + 3.299 +theorem update_cons_val: "update (x # xs) opt (Val a) = Val a" 3.300 + by simp 3.301 + 3.302 +theorem update_cons_nil_env: 3.303 + "update [x] opt (Env b es) = Env b (es (x := opt))" 3.304 + by (cases "es x") simp_all 3.305 + 3.306 +theorem update_cons_cons_env: 3.307 + "update (x # y # ys) opt (Env b es) = 3.308 + Env b (es (x := 3.309 + (case es x of 3.310 + None => None 3.311 + | Some e => Some (update (y # ys) opt e))))" 3.312 + by (cases "es x") simp_all 3.313 + 3.314 +lemmas update.simps [simp del] 3.315 + and update_simps [simp] = update_nil_none update_nil_some 3.316 + update_cons_val update_cons_nil_env update_cons_cons_env 3.317 + 3.318 +lemma update_eq: 3.319 + "update xs opt env = 3.320 + (case xs of 3.321 + [] => 3.322 + (case opt of 3.323 + None => env 3.324 + | Some e => e) 3.325 + | x # xs => 3.326 + (case env of 3.327 + Val a => Val a 3.328 + | Env b es => 3.329 + (case xs of 3.330 + [] => Env b (es (x := opt)) 3.331 + | y # ys => 3.332 + Env b (es (x := 3.333 + (case es x of 3.334 + None => None 3.335 + | Some e => Some (update (y # ys) opt e)))))))" 3.336 + by (simp split: list.split env.split option.split) 3.337 + 3.338 +text {* 3.339 + \medskip The most basic correspondence of @{term lookup} and @{term 3.340 + update} states that after @{term update} at a defined position, 3.341 + subsequent @{term lookup} operations would yield the new value. 3.342 +*} 3.343 + 3.344 +theorem lookup_update_some: 3.345 + "!!env e. lookup env xs = Some e ==> 3.346 + lookup (update xs (Some env') env) xs = Some env'" 3.347 + (is "PROP ?P xs") 3.348 +proof (induct xs) 3.349 + fix env e :: "('a, 'b, 'c) env" 3.350 + { 3.351 + assume "lookup env [] = Some e" 3.352 + hence "env = e" by simp 3.353 + thus "lookup (update [] (Some env') env) [] = Some env'" 3.354 + by simp 3.355 + next 3.356 + fix x xs 3.357 + assume hyp: "PROP ?P xs" 3.358 + assume asm: "lookup env (x # xs) = Some e" 3.359 + show "lookup (update (x # xs) (Some env') env) (x # xs) = Some env'" 3.360 + proof (cases env) 3.361 + fix a assume "env = Val a" 3.362 + with asm have False by simp 3.363 + thus ?thesis .. 3.364 + next 3.365 + fix b es assume env: "env = Env b es" 3.366 + show ?thesis 3.367 + proof (cases "es x") 3.368 + assume "es x = None" 3.369 + with asm env have False by simp 3.370 + thus ?thesis .. 3.371 + next 3.372 + fix e' assume es: "es x = Some e'" 3.373 + show ?thesis 3.374 + proof (cases xs) 3.375 + assume "xs = []" 3.376 + with env show ?thesis by simp 3.377 + next 3.378 + fix x' xs' assume xs: "xs = x' # xs'" 3.379 + from asm env es have "lookup e' xs = Some e" by simp 3.380 + hence "lookup (update xs (Some env') e') xs = Some env'" by (rule hyp) 3.381 + with env es xs show ?thesis by simp 3.382 + qed 3.383 + qed 3.384 + qed 3.385 + } 3.386 +qed 3.387 + 3.388 +text {* 3.389 + \medskip The properties of displaced @{term update} operations are 3.390 + analogous to those of @{term lookup} above. There are two cases: 3.391 + below an undefined position @{term update} is absorbed altogether, 3.392 + and below a defined positions @{term update} affects subsequent 3.393 + @{term lookup} operations in the obvious way. 3.394 +*} 3.395 + 3.396 +theorem update_append_none: 3.397 + "!!env. lookup env xs = None ==> update (xs @ y # ys) opt env = env" 3.398 + (is "PROP ?P xs") 3.399 +proof (induct xs) 3.400 + fix env :: "('a, 'b, 'c) env" 3.401 + { 3.402 + assume "lookup env [] = None" 3.403 + hence False by simp 3.404 + thus "update ([] @ y # ys) opt env = env" .. 3.405 + next 3.406 + fix x xs 3.407 + assume hyp: "PROP ?P xs" 3.408 + assume asm: "lookup env (x # xs) = None" 3.409 + show "update ((x # xs) @ y # ys) opt env = env" 3.410 + proof (cases env) 3.411 + fix a assume "env = Val a" 3.412 + thus ?thesis by simp 3.413 + next 3.414 + fix b es assume env: "env = Env b es" 3.415 + show ?thesis 3.416 + proof (cases "es x") 3.417 + assume es: "es x = None" 3.418 + show ?thesis 3.419 + by (cases xs) (simp_all add: es env fun_upd_idem_iff) 3.420 + next 3.421 + fix e assume es: "es x = Some e" 3.422 + show ?thesis 3.423 + proof (cases xs) 3.424 + assume "xs = []" 3.425 + with asm env es have False by simp 3.426 + thus ?thesis .. 3.427 + next 3.428 + fix x' xs' assume xs: "xs = x' # xs'" 3.429 + from asm env es have "lookup e xs = None" by simp 3.430 + hence "update (xs @ y # ys) opt e = e" by (rule hyp) 3.431 + with env es xs show "update ((x # xs) @ y # ys) opt env = env" 3.432 + by (simp add: fun_upd_idem_iff) 3.433 + qed 3.434 + qed 3.435 + qed 3.436 + } 3.437 +qed 3.438 + 3.439 +theorem update_append_some: 3.440 + "!!env e. lookup env xs = Some e ==> 3.441 + lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)" 3.442 + (is "PROP ?P xs") 3.443 +proof (induct xs) 3.444 + fix env e :: "('a, 'b, 'c) env" 3.445 + { 3.446 + assume "lookup env [] = Some e" 3.447 + hence "env = e" by simp 3.448 + thus "lookup (update ([] @ y # ys) opt env) [] = Some (update (y # ys) opt e)" 3.449 + by simp 3.450 + next 3.451 + fix x xs 3.452 + assume hyp: "PROP ?P xs" 3.453 + assume asm: "lookup env (x # xs) = Some e" 3.454 + show "lookup (update ((x # xs) @ y # ys) opt env) (x # xs) 3.455 + = Some (update (y # ys) opt e)" 3.456 + proof (cases env) 3.457 + fix a assume "env = Val a" 3.458 + with asm have False by simp 3.459 + thus ?thesis .. 3.460 + next 3.461 + fix b es assume env: "env = Env b es" 3.462 + show ?thesis 3.463 + proof (cases "es x") 3.464 + assume "es x = None" 3.465 + with asm env have False by simp 3.466 + thus ?thesis .. 3.467 + next 3.468 + fix e' assume es: "es x = Some e'" 3.469 + show ?thesis 3.470 + proof (cases xs) 3.471 + assume xs: "xs = []" 3.472 + from asm env es xs have "e = e'" by simp 3.473 + with env es xs show ?thesis by simp 3.474 + next 3.475 + fix x' xs' assume xs: "xs = x' # xs'" 3.476 + from asm env es have "lookup e' xs = Some e" by simp 3.477 + hence "lookup (update (xs @ y # ys) opt e') xs = 3.478 + Some (update (y # ys) opt e)" by (rule hyp) 3.479 + with env es xs show ?thesis by simp 3.480 + qed 3.481 + qed 3.482 + qed 3.483 + } 3.484 +qed 3.485 + 3.486 +text {* 3.487 + \medskip Apparently, @{term update} does not affect the result of 3.488 + subsequent @{term lookup} operations at independent positions, i.e.\ 3.489 + in case that the paths for @{term update} and @{term lookup} fork at 3.490 + a certain point. 3.491 +*} 3.492 + 3.493 +theorem lookup_update_other: 3.494 + "!!env. y \<noteq> (z::'c) ==> lookup (update (xs @ z # zs) opt env) (xs @ y # ys) = 3.495 + lookup env (xs @ y # ys)" 3.496 + (is "PROP ?P xs") 3.497 +proof (induct xs) 3.498 + fix env :: "('a, 'b, 'c) env" 3.499 + assume neq: "y \<noteq> z" 3.500 + { 3.501 + show "lookup (update ([] @ z # zs) opt env) ([] @ y # ys) = 3.502 + lookup env ([] @ y # ys)" 3.503 + proof (cases env) 3.504 + case Val 3.505 + thus ?thesis by simp 3.506 + next 3.507 + case Env 3.508 + show ?thesis 3.509 + proof (cases zs) 3.510 + case Nil 3.511 + with neq Env show ?thesis by simp 3.512 + next 3.513 + case Cons 3.514 + with neq Env show ?thesis by simp 3.515 + qed 3.516 + qed 3.517 + next 3.518 + fix x xs 3.519 + assume hyp: "PROP ?P xs" 3.520 + show "lookup (update ((x # xs) @ z # zs) opt env) ((x # xs) @ y # ys) = 3.521 + lookup env ((x # xs) @ y # ys)" 3.522 + proof (cases env) 3.523 + case Val 3.524 + thus ?thesis by simp 3.525 + next 3.526 + fix y es assume env: "env = Env y es" 3.527 + show ?thesis 3.528 + proof (cases xs) 3.529 + assume xs: "xs = []" 3.530 + show ?thesis 3.531 + proof (cases "es x") 3.532 + case None 3.533 + with env xs show ?thesis by simp 3.534 + next 3.535 + case Some 3.536 + with hyp env xs and neq show ?thesis by simp 3.537 + qed 3.538 + next 3.539 + fix x' xs' assume xs: "xs = x' # xs'" 3.540 + show ?thesis 3.541 + proof (cases "es x") 3.542 + case None 3.543 + with env xs show ?thesis by simp 3.544 + next 3.545 + case Some 3.546 + with hyp env xs neq show ?thesis by simp 3.547 + qed 3.548 + qed 3.549 + qed 3.550 + } 3.551 +qed 3.552 + 3.553 +end