author | wenzelm |

Wed Aug 17 13:14:20 2011 +0200 (2011-08-17) | |

changeset 44236 | b73b7832b384 |

parent 44235 | 85e9dad3c187 |

child 44237 | 2a2040c9d898 |

moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);

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

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

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

1.1 --- a/src/HOL/IsaMakefile Wed Aug 17 10:03:58 2011 +0200 1.2 +++ b/src/HOL/IsaMakefile Wed Aug 17 13:14:20 2011 +0200 1.3 @@ -437,39 +437,35 @@ 1.4 Library/Code_Char_ord.thy Library/Code_Integer.thy \ 1.5 Library/Code_Natural.thy Library/Code_Prolog.thy \ 1.6 Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy \ 1.7 - Library/Cset.thy Library/Cset_Monad.thy \ 1.8 - Library/Continuity.thy Library/Convex.thy Library/Countable.thy \ 1.9 - Library/Diagonalize.thy Library/Dlist.thy Library/Dlist_Cset.thy \ 1.10 - Library/Efficient_Nat.thy Library/Eval_Witness.thy \ 1.11 - Library/Executable_Set.thy Library/Extended_Real.thy \ 1.12 - Library/Extended_Nat.thy Library/Float.thy \ 1.13 + Library/Cset.thy Library/Cset_Monad.thy Library/Continuity.thy \ 1.14 + Library/Convex.thy Library/Countable.thy Library/Diagonalize.thy \ 1.15 + Library/Dlist.thy Library/Dlist_Cset.thy Library/Efficient_Nat.thy \ 1.16 + Library/Eval_Witness.thy Library/Executable_Set.thy \ 1.17 + Library/Extended_Real.thy Library/Extended_Nat.thy Library/Float.thy \ 1.18 Library/Formal_Power_Series.thy Library/Fraction_Field.thy \ 1.19 Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy \ 1.20 - Library/Function_Algebras.thy Library/Fundamental_Theorem_Algebra.thy \ 1.21 - Library/Glbs.thy Library/Indicator_Function.thy \ 1.22 - Library/Infinite_Set.thy Library/Inner_Product.thy \ 1.23 - Library/Kleene_Algebra.thy Library/LaTeXsugar.thy \ 1.24 - Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy \ 1.25 - Library/Library.thy Library/List_Cset.thy Library/List_Prefix.thy \ 1.26 - Library/List_lexord.thy Library/Mapping.thy Library/Monad_Syntax.thy \ 1.27 - Library/More_List.thy Library/More_Set.thy Library/Multiset.thy \ 1.28 - Library/Nat_Bijection.thy Library/Nested_Environment.thy \ 1.29 - Library/Numeral_Type.thy Library/Old_Recdef.thy \ 1.30 - Library/OptionalSugar.thy \ 1.31 - Library/Order_Relation.thy Library/Permutation.thy \ 1.32 - Library/Permutations.thy Library/Poly_Deriv.thy \ 1.33 - Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy \ 1.34 - Library/Preorder.thy Library/Product_Vector.thy \ 1.35 - Library/Product_ord.thy Library/Product_plus.thy \ 1.36 - Library/Product_Lattice.thy \ 1.37 - Library/Quickcheck_Types.thy \ 1.38 - Library/Quotient_List.thy Library/Quotient_Option.thy \ 1.39 - Library/Quotient_Product.thy Library/Quotient_Sum.thy \ 1.40 - Library/Quotient_Syntax.thy Library/Quotient_Type.thy \ 1.41 - Library/RBT.thy Library/RBT_Impl.thy Library/RBT_Mapping.thy \ 1.42 - Library/README.html \ 1.43 - Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy \ 1.44 - Library/Reflection.thy \ 1.45 + Library/Function_Algebras.thy \ 1.46 + Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy \ 1.47 + Library/Indicator_Function.thy Library/Infinite_Set.thy \ 1.48 + Library/Inner_Product.thy Library/Kleene_Algebra.thy \ 1.49 + Library/LaTeXsugar.thy Library/Lattice_Algebras.thy \ 1.50 + Library/Lattice_Syntax.thy Library/Library.thy Library/List_Cset.thy \ 1.51 + Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy \ 1.52 + Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy \ 1.53 + Library/Multiset.thy Library/Nat_Bijection.thy \ 1.54 + Library/Numeral_Type.thy Library/Old_Recdef.thy \ 1.55 + Library/OptionalSugar.thy Library/Order_Relation.thy \ 1.56 + Library/Permutation.thy Library/Permutations.thy \ 1.57 + Library/Poly_Deriv.thy Library/Polynomial.thy \ 1.58 + Library/Predicate_Compile_Quickcheck.thy Library/Preorder.thy \ 1.59 + Library/Product_Vector.thy Library/Product_ord.thy \ 1.60 + Library/Product_plus.thy Library/Product_Lattice.thy \ 1.61 + Library/Quickcheck_Types.thy Library/Quotient_List.thy \ 1.62 + Library/Quotient_Option.thy Library/Quotient_Product.thy \ 1.63 + Library/Quotient_Sum.thy Library/Quotient_Syntax.thy \ 1.64 + Library/Quotient_Type.thy Library/RBT.thy Library/RBT_Impl.thy \ 1.65 + Library/RBT_Mapping.thy Library/README.html Library/Set_Algebras.thy \ 1.66 + Library/State_Monad.thy Library/Ramsey.thy Library/Reflection.thy \ 1.67 Library/Sublist_Order.thy Library/Sum_of_Squares.thy \ 1.68 Library/Sum_of_Squares/sos_wrapper.ML \ 1.69 Library/Sum_of_Squares/sum_of_squares.ML \ 1.70 @@ -830,9 +826,9 @@ 1.71 1.72 HOL-Unix: HOL $(LOG)/HOL-Unix.gz 1.73 1.74 -$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy \ 1.75 - Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy \ 1.76 - Unix/document/root.bib Unix/document/root.tex 1.77 +$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/List_Prefix.thy Unix/ROOT.ML \ 1.78 + Unix/Nested_Environment.thy Unix/Unix.thy Unix/document/root.bib \ 1.79 + Unix/document/root.tex 1.80 @$(ISABELLE_TOOL) usedir -m no_brackets -m no_type_brackets $(OUT)/HOL Unix 1.81 1.82

2.1 --- a/src/HOL/Library/Library.thy Wed Aug 17 10:03:58 2011 +0200 2.2 +++ b/src/HOL/Library/Library.thy Wed Aug 17 13:14:20 2011 +0200 2.3 @@ -37,7 +37,6 @@ 2.4 Monad_Syntax 2.5 More_List 2.6 Multiset 2.7 - Nested_Environment 2.8 Numeral_Type 2.9 Old_Recdef 2.10 OptionalSugar

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

4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000 4.2 +++ b/src/HOL/Unix/Nested_Environment.thy Wed Aug 17 13:14:20 2011 +0200 4.3 @@ -0,0 +1,571 @@ 4.4 +(* Title: HOL/Unix/Nested_Environment.thy 4.5 + Author: Markus Wenzel, TU Muenchen 4.6 +*) 4.7 + 4.8 +header {* Nested environments *} 4.9 + 4.10 +theory Nested_Environment 4.11 +imports Main 4.12 +begin 4.13 + 4.14 +text {* 4.15 + Consider a partial function @{term [source] "e :: 'a => 'b option"}; 4.16 + this may be understood as an \emph{environment} mapping indexes 4.17 + @{typ 'a} to optional entry values @{typ 'b} (cf.\ the basic theory 4.18 + @{text Map} of Isabelle/HOL). This basic idea is easily generalized 4.19 + to that of a \emph{nested environment}, where entries may be either 4.20 + basic values or again proper environments. Then each entry is 4.21 + accessed by a \emph{path}, i.e.\ a list of indexes leading to its 4.22 + position within the structure. 4.23 +*} 4.24 + 4.25 +datatype ('a, 'b, 'c) env = 4.26 + Val 'a 4.27 + | Env 'b "'c => ('a, 'b, 'c) env option" 4.28 + 4.29 +text {* 4.30 + \medskip In the type @{typ "('a, 'b, 'c) env"} the parameter @{typ 4.31 + 'a} refers to basic values (occurring in terminal positions), type 4.32 + @{typ 'b} to values associated with proper (inner) environments, and 4.33 + type @{typ 'c} with the index type for branching. Note that there 4.34 + is no restriction on any of these types. In particular, arbitrary 4.35 + branching may yield rather large (transfinite) tree structures. 4.36 +*} 4.37 + 4.38 + 4.39 +subsection {* The lookup operation *} 4.40 + 4.41 +text {* 4.42 + Lookup in nested environments works by following a given path of 4.43 + index elements, leading to an optional result (a terminal value or 4.44 + nested environment). A \emph{defined position} within a nested 4.45 + environment is one where @{term lookup} at its path does not yield 4.46 + @{term None}. 4.47 +*} 4.48 + 4.49 +primrec 4.50 + lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option" 4.51 + and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option" where 4.52 + "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)" 4.53 + | "lookup (Env b es) xs = 4.54 + (case xs of 4.55 + [] => Some (Env b es) 4.56 + | y # ys => lookup_option (es y) ys)" 4.57 + | "lookup_option None xs = None" 4.58 + | "lookup_option (Some e) xs = lookup e xs" 4.59 + 4.60 +hide_const lookup_option 4.61 + 4.62 +text {* 4.63 + \medskip The characteristic cases of @{term lookup} are expressed by 4.64 + the following equalities. 4.65 +*} 4.66 + 4.67 +theorem lookup_nil: "lookup e [] = Some e" 4.68 + by (cases e) simp_all 4.69 + 4.70 +theorem lookup_val_cons: "lookup (Val a) (x # xs) = None" 4.71 + by simp 4.72 + 4.73 +theorem lookup_env_cons: 4.74 + "lookup (Env b es) (x # xs) = 4.75 + (case es x of 4.76 + None => None 4.77 + | Some e => lookup e xs)" 4.78 + by (cases "es x") simp_all 4.79 + 4.80 +lemmas lookup_lookup_option.simps [simp del] 4.81 + and lookup_simps [simp] = lookup_nil lookup_val_cons lookup_env_cons 4.82 + 4.83 +theorem lookup_eq: 4.84 + "lookup env xs = 4.85 + (case xs of 4.86 + [] => Some env 4.87 + | x # xs => 4.88 + (case env of 4.89 + Val a => None 4.90 + | Env b es => 4.91 + (case es x of 4.92 + None => None 4.93 + | Some e => lookup e xs)))" 4.94 + by (simp split: list.split env.split) 4.95 + 4.96 +text {* 4.97 + \medskip Displaced @{term lookup} operations, relative to a certain 4.98 + base path prefix, may be reduced as follows. There are two cases, 4.99 + depending whether the environment actually extends far enough to 4.100 + follow the base path. 4.101 +*} 4.102 + 4.103 +theorem lookup_append_none: 4.104 + assumes "lookup env xs = None" 4.105 + shows "lookup env (xs @ ys) = None" 4.106 + using assms 4.107 +proof (induct xs arbitrary: env) 4.108 + case Nil 4.109 + then have False by simp 4.110 + then show ?case .. 4.111 +next 4.112 + case (Cons x xs) 4.113 + show ?case 4.114 + proof (cases env) 4.115 + case Val 4.116 + then show ?thesis by simp 4.117 + next 4.118 + case (Env b es) 4.119 + show ?thesis 4.120 + proof (cases "es x") 4.121 + case None 4.122 + with Env show ?thesis by simp 4.123 + next 4.124 + case (Some e) 4.125 + note es = `es x = Some e` 4.126 + show ?thesis 4.127 + proof (cases "lookup e xs") 4.128 + case None 4.129 + then have "lookup e (xs @ ys) = None" by (rule Cons.hyps) 4.130 + with Env Some show ?thesis by simp 4.131 + next 4.132 + case Some 4.133 + with Env es have False using Cons.prems by simp 4.134 + then show ?thesis .. 4.135 + qed 4.136 + qed 4.137 + qed 4.138 +qed 4.139 + 4.140 +theorem lookup_append_some: 4.141 + assumes "lookup env xs = Some e" 4.142 + shows "lookup env (xs @ ys) = lookup e ys" 4.143 + using assms 4.144 +proof (induct xs arbitrary: env e) 4.145 + case Nil 4.146 + then have "env = e" by simp 4.147 + then show "lookup env ([] @ ys) = lookup e ys" by simp 4.148 +next 4.149 + case (Cons x xs) 4.150 + note asm = `lookup env (x # xs) = Some e` 4.151 + show "lookup env ((x # xs) @ ys) = lookup e ys" 4.152 + proof (cases env) 4.153 + case (Val a) 4.154 + with asm have False by simp 4.155 + then show ?thesis .. 4.156 + next 4.157 + case (Env b es) 4.158 + show ?thesis 4.159 + proof (cases "es x") 4.160 + case None 4.161 + with asm Env have False by simp 4.162 + then show ?thesis .. 4.163 + next 4.164 + case (Some e') 4.165 + note es = `es x = Some e'` 4.166 + show ?thesis 4.167 + proof (cases "lookup e' xs") 4.168 + case None 4.169 + with asm Env es have False by simp 4.170 + then show ?thesis .. 4.171 + next 4.172 + case Some 4.173 + with asm Env es have "lookup e' xs = Some e" 4.174 + by simp 4.175 + then have "lookup e' (xs @ ys) = lookup e ys" by (rule Cons.hyps) 4.176 + with Env es show ?thesis by simp 4.177 + qed 4.178 + qed 4.179 + qed 4.180 +qed 4.181 + 4.182 +text {* 4.183 + \medskip Successful @{term lookup} deeper down an environment 4.184 + structure means we are able to peek further up as well. Note that 4.185 + this is basically just the contrapositive statement of @{thm 4.186 + [source] lookup_append_none} above. 4.187 +*} 4.188 + 4.189 +theorem lookup_some_append: 4.190 + assumes "lookup env (xs @ ys) = Some e" 4.191 + shows "\<exists>e. lookup env xs = Some e" 4.192 +proof - 4.193 + from assms have "lookup env (xs @ ys) \<noteq> None" by simp 4.194 + then have "lookup env xs \<noteq> None" 4.195 + by (rule contrapos_nn) (simp only: lookup_append_none) 4.196 + then show ?thesis by (simp) 4.197 +qed 4.198 + 4.199 +text {* 4.200 + The subsequent statement describes in more detail how a successful 4.201 + @{term lookup} with a non-empty path results in a certain situation 4.202 + at any upper position. 4.203 +*} 4.204 + 4.205 +theorem lookup_some_upper: 4.206 + assumes "lookup env (xs @ y # ys) = Some e" 4.207 + shows "\<exists>b' es' env'. 4.208 + lookup env xs = Some (Env b' es') \<and> 4.209 + es' y = Some env' \<and> 4.210 + lookup env' ys = Some e" 4.211 + using assms 4.212 +proof (induct xs arbitrary: env e) 4.213 + case Nil 4.214 + from Nil.prems have "lookup env (y # ys) = Some e" 4.215 + by simp 4.216 + then obtain b' es' env' where 4.217 + env: "env = Env b' es'" and 4.218 + es': "es' y = Some env'" and 4.219 + look': "lookup env' ys = Some e" 4.220 + by (auto simp add: lookup_eq split: option.splits env.splits) 4.221 + from env have "lookup env [] = Some (Env b' es')" by simp 4.222 + with es' look' show ?case by blast 4.223 +next 4.224 + case (Cons x xs) 4.225 + from Cons.prems 4.226 + obtain b' es' env' where 4.227 + env: "env = Env b' es'" and 4.228 + es': "es' x = Some env'" and 4.229 + look': "lookup env' (xs @ y # ys) = Some e" 4.230 + by (auto simp add: lookup_eq split: option.splits env.splits) 4.231 + from Cons.hyps [OF look'] obtain b'' es'' env'' where 4.232 + upper': "lookup env' xs = Some (Env b'' es'')" and 4.233 + es'': "es'' y = Some env''" and 4.234 + look'': "lookup env'' ys = Some e" 4.235 + by blast 4.236 + from env es' upper' have "lookup env (x # xs) = Some (Env b'' es'')" 4.237 + by simp 4.238 + with es'' look'' show ?case by blast 4.239 +qed 4.240 + 4.241 + 4.242 +subsection {* The update operation *} 4.243 + 4.244 +text {* 4.245 + Update at a certain position in a nested environment may either 4.246 + delete an existing entry, or overwrite an existing one. Note that 4.247 + update at undefined positions is simple absorbed, i.e.\ the 4.248 + environment is left unchanged. 4.249 +*} 4.250 + 4.251 +primrec 4.252 + update :: "'c list => ('a, 'b, 'c) env option 4.253 + => ('a, 'b, 'c) env => ('a, 'b, 'c) env" 4.254 + and update_option :: "'c list => ('a, 'b, 'c) env option 4.255 + => ('a, 'b, 'c) env option => ('a, 'b, 'c) env option" where 4.256 + "update xs opt (Val a) = 4.257 + (if xs = [] then (case opt of None => Val a | Some e => e) 4.258 + else Val a)" 4.259 + | "update xs opt (Env b es) = 4.260 + (case xs of 4.261 + [] => (case opt of None => Env b es | Some e => e) 4.262 + | y # ys => Env b (es (y := update_option ys opt (es y))))" 4.263 + | "update_option xs opt None = 4.264 + (if xs = [] then opt else None)" 4.265 + | "update_option xs opt (Some e) = 4.266 + (if xs = [] then opt else Some (update xs opt e))" 4.267 + 4.268 +hide_const update_option 4.269 + 4.270 +text {* 4.271 + \medskip The characteristic cases of @{term update} are expressed by 4.272 + the following equalities. 4.273 +*} 4.274 + 4.275 +theorem update_nil_none: "update [] None env = env" 4.276 + by (cases env) simp_all 4.277 + 4.278 +theorem update_nil_some: "update [] (Some e) env = e" 4.279 + by (cases env) simp_all 4.280 + 4.281 +theorem update_cons_val: "update (x # xs) opt (Val a) = Val a" 4.282 + by simp 4.283 + 4.284 +theorem update_cons_nil_env: 4.285 + "update [x] opt (Env b es) = Env b (es (x := opt))" 4.286 + by (cases "es x") simp_all 4.287 + 4.288 +theorem update_cons_cons_env: 4.289 + "update (x # y # ys) opt (Env b es) = 4.290 + Env b (es (x := 4.291 + (case es x of 4.292 + None => None 4.293 + | Some e => Some (update (y # ys) opt e))))" 4.294 + by (cases "es x") simp_all 4.295 + 4.296 +lemmas update_update_option.simps [simp del] 4.297 + and update_simps [simp] = update_nil_none update_nil_some 4.298 + update_cons_val update_cons_nil_env update_cons_cons_env 4.299 + 4.300 +lemma update_eq: 4.301 + "update xs opt env = 4.302 + (case xs of 4.303 + [] => 4.304 + (case opt of 4.305 + None => env 4.306 + | Some e => e) 4.307 + | x # xs => 4.308 + (case env of 4.309 + Val a => Val a 4.310 + | Env b es => 4.311 + (case xs of 4.312 + [] => Env b (es (x := opt)) 4.313 + | y # ys => 4.314 + Env b (es (x := 4.315 + (case es x of 4.316 + None => None 4.317 + | Some e => Some (update (y # ys) opt e)))))))" 4.318 + by (simp split: list.split env.split option.split) 4.319 + 4.320 +text {* 4.321 + \medskip The most basic correspondence of @{term lookup} and @{term 4.322 + update} states that after @{term update} at a defined position, 4.323 + subsequent @{term lookup} operations would yield the new value. 4.324 +*} 4.325 + 4.326 +theorem lookup_update_some: 4.327 + assumes "lookup env xs = Some e" 4.328 + shows "lookup (update xs (Some env') env) xs = Some env'" 4.329 + using assms 4.330 +proof (induct xs arbitrary: env e) 4.331 + case Nil 4.332 + then have "env = e" by simp 4.333 + then show ?case by simp 4.334 +next 4.335 + case (Cons x xs) 4.336 + note hyp = Cons.hyps 4.337 + and asm = `lookup env (x # xs) = Some e` 4.338 + show ?case 4.339 + proof (cases env) 4.340 + case (Val a) 4.341 + with asm have False by simp 4.342 + then show ?thesis .. 4.343 + next 4.344 + case (Env b es) 4.345 + show ?thesis 4.346 + proof (cases "es x") 4.347 + case None 4.348 + with asm Env have False by simp 4.349 + then show ?thesis .. 4.350 + next 4.351 + case (Some e') 4.352 + note es = `es x = Some e'` 4.353 + show ?thesis 4.354 + proof (cases xs) 4.355 + case Nil 4.356 + with Env show ?thesis by simp 4.357 + next 4.358 + case (Cons x' xs') 4.359 + from asm Env es have "lookup e' xs = Some e" by simp 4.360 + then have "lookup (update xs (Some env') e') xs = Some env'" by (rule hyp) 4.361 + with Env es Cons show ?thesis by simp 4.362 + qed 4.363 + qed 4.364 + qed 4.365 +qed 4.366 + 4.367 +text {* 4.368 + \medskip The properties of displaced @{term update} operations are 4.369 + analogous to those of @{term lookup} above. There are two cases: 4.370 + below an undefined position @{term update} is absorbed altogether, 4.371 + and below a defined positions @{term update} affects subsequent 4.372 + @{term lookup} operations in the obvious way. 4.373 +*} 4.374 + 4.375 +theorem update_append_none: 4.376 + assumes "lookup env xs = None" 4.377 + shows "update (xs @ y # ys) opt env = env" 4.378 + using assms 4.379 +proof (induct xs arbitrary: env) 4.380 + case Nil 4.381 + then have False by simp 4.382 + then show ?case .. 4.383 +next 4.384 + case (Cons x xs) 4.385 + note hyp = Cons.hyps 4.386 + and asm = `lookup env (x # xs) = None` 4.387 + show "update ((x # xs) @ y # ys) opt env = env" 4.388 + proof (cases env) 4.389 + case (Val a) 4.390 + then show ?thesis by simp 4.391 + next 4.392 + case (Env b es) 4.393 + show ?thesis 4.394 + proof (cases "es x") 4.395 + case None 4.396 + note es = `es x = None` 4.397 + show ?thesis 4.398 + by (cases xs) (simp_all add: es Env fun_upd_idem_iff) 4.399 + next 4.400 + case (Some e) 4.401 + note es = `es x = Some e` 4.402 + show ?thesis 4.403 + proof (cases xs) 4.404 + case Nil 4.405 + with asm Env Some have False by simp 4.406 + then show ?thesis .. 4.407 + next 4.408 + case (Cons x' xs') 4.409 + from asm Env es have "lookup e xs = None" by simp 4.410 + then have "update (xs @ y # ys) opt e = e" by (rule hyp) 4.411 + with Env es Cons show "update ((x # xs) @ y # ys) opt env = env" 4.412 + by (simp add: fun_upd_idem_iff) 4.413 + qed 4.414 + qed 4.415 + qed 4.416 +qed 4.417 + 4.418 +theorem update_append_some: 4.419 + assumes "lookup env xs = Some e" 4.420 + shows "lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)" 4.421 + using assms 4.422 +proof (induct xs arbitrary: env e) 4.423 + case Nil 4.424 + then have "env = e" by simp 4.425 + then show ?case by simp 4.426 +next 4.427 + case (Cons x xs) 4.428 + note hyp = Cons.hyps 4.429 + and asm = `lookup env (x # xs) = Some e` 4.430 + show "lookup (update ((x # xs) @ y # ys) opt env) (x # xs) = 4.431 + Some (update (y # ys) opt e)" 4.432 + proof (cases env) 4.433 + case (Val a) 4.434 + with asm have False by simp 4.435 + then show ?thesis .. 4.436 + next 4.437 + case (Env b es) 4.438 + show ?thesis 4.439 + proof (cases "es x") 4.440 + case None 4.441 + with asm Env have False by simp 4.442 + then show ?thesis .. 4.443 + next 4.444 + case (Some e') 4.445 + note es = `es x = Some e'` 4.446 + show ?thesis 4.447 + proof (cases xs) 4.448 + case Nil 4.449 + with asm Env es have "e = e'" by simp 4.450 + with Env es Nil show ?thesis by simp 4.451 + next 4.452 + case (Cons x' xs') 4.453 + from asm Env es have "lookup e' xs = Some e" by simp 4.454 + then have "lookup (update (xs @ y # ys) opt e') xs = 4.455 + Some (update (y # ys) opt e)" by (rule hyp) 4.456 + with Env es Cons show ?thesis by simp 4.457 + qed 4.458 + qed 4.459 + qed 4.460 +qed 4.461 + 4.462 +text {* 4.463 + \medskip Apparently, @{term update} does not affect the result of 4.464 + subsequent @{term lookup} operations at independent positions, i.e.\ 4.465 + in case that the paths for @{term update} and @{term lookup} fork at 4.466 + a certain point. 4.467 +*} 4.468 + 4.469 +theorem lookup_update_other: 4.470 + assumes neq: "y \<noteq> (z::'c)" 4.471 + shows "lookup (update (xs @ z # zs) opt env) (xs @ y # ys) = 4.472 + lookup env (xs @ y # ys)" 4.473 +proof (induct xs arbitrary: env) 4.474 + case Nil 4.475 + show ?case 4.476 + proof (cases env) 4.477 + case Val 4.478 + then show ?thesis by simp 4.479 + next 4.480 + case Env 4.481 + show ?thesis 4.482 + proof (cases zs) 4.483 + case Nil 4.484 + with neq Env show ?thesis by simp 4.485 + next 4.486 + case Cons 4.487 + with neq Env show ?thesis by simp 4.488 + qed 4.489 + qed 4.490 +next 4.491 + case (Cons x xs) 4.492 + note hyp = Cons.hyps 4.493 + show ?case 4.494 + proof (cases env) 4.495 + case Val 4.496 + then show ?thesis by simp 4.497 + next 4.498 + case (Env y es) 4.499 + show ?thesis 4.500 + proof (cases xs) 4.501 + case Nil 4.502 + show ?thesis 4.503 + proof (cases "es x") 4.504 + case None 4.505 + with Env Nil show ?thesis by simp 4.506 + next 4.507 + case Some 4.508 + with neq hyp and Env Nil show ?thesis by simp 4.509 + qed 4.510 + next 4.511 + case (Cons x' xs') 4.512 + show ?thesis 4.513 + proof (cases "es x") 4.514 + case None 4.515 + with Env Cons show ?thesis by simp 4.516 + next 4.517 + case Some 4.518 + with neq hyp and Env Cons show ?thesis by simp 4.519 + qed 4.520 + qed 4.521 + qed 4.522 +qed 4.523 + 4.524 +text {* Environments and code generation *} 4.525 + 4.526 +lemma [code, code del]: 4.527 + "(HOL.equal :: (_, _, _) env \<Rightarrow> _) = HOL.equal" .. 4.528 + 4.529 +lemma equal_env_code [code]: 4.530 + fixes x y :: "'a\<Colon>equal" 4.531 + and f g :: "'c\<Colon>{equal, finite} \<Rightarrow> ('b\<Colon>equal, 'a, 'c) env option" 4.532 + shows "HOL.equal (Env x f) (Env y g) \<longleftrightarrow> 4.533 + HOL.equal x y \<and> (\<forall>z\<in>UNIV. case f z 4.534 + of None \<Rightarrow> (case g z 4.535 + of None \<Rightarrow> True | Some _ \<Rightarrow> False) 4.536 + | Some a \<Rightarrow> (case g z 4.537 + of None \<Rightarrow> False | Some b \<Rightarrow> HOL.equal a b))" (is ?env) 4.538 + and "HOL.equal (Val a) (Val b) \<longleftrightarrow> HOL.equal a b" 4.539 + and "HOL.equal (Val a) (Env y g) \<longleftrightarrow> False" 4.540 + and "HOL.equal (Env x f) (Val b) \<longleftrightarrow> False" 4.541 +proof (unfold equal) 4.542 + have "f = g \<longleftrightarrow> (\<forall>z. case f z 4.543 + of None \<Rightarrow> (case g z 4.544 + of None \<Rightarrow> True | Some _ \<Rightarrow> False) 4.545 + | Some a \<Rightarrow> (case g z 4.546 + of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" (is "?lhs = ?rhs") 4.547 + proof 4.548 + assume ?lhs 4.549 + then show ?rhs by (auto split: option.splits) 4.550 + next 4.551 + assume assm: ?rhs (is "\<forall>z. ?prop z") 4.552 + show ?lhs 4.553 + proof 4.554 + fix z 4.555 + from assm have "?prop z" .. 4.556 + then show "f z = g z" by (auto split: option.splits) 4.557 + qed 4.558 + qed 4.559 + then show "Env x f = Env y g \<longleftrightarrow> 4.560 + x = y \<and> (\<forall>z\<in>UNIV. case f z 4.561 + of None \<Rightarrow> (case g z 4.562 + of None \<Rightarrow> True | Some _ \<Rightarrow> False) 4.563 + | Some a \<Rightarrow> (case g z 4.564 + of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp 4.565 +qed simp_all 4.566 + 4.567 +lemma [code nbe]: 4.568 + "HOL.equal (x :: (_, _, _) env) x \<longleftrightarrow> True" 4.569 + by (fact equal_refl) 4.570 + 4.571 +lemma [code, code del]: 4.572 + "(Code_Evaluation.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Evaluation.term_of" .. 4.573 + 4.574 +end

5.1 --- a/src/HOL/Unix/Unix.thy Wed Aug 17 10:03:58 2011 +0200 5.2 +++ b/src/HOL/Unix/Unix.thy Wed Aug 17 13:14:20 2011 +0200 5.3 @@ -6,8 +6,7 @@ 5.4 5.5 theory Unix 5.6 imports 5.7 - Main 5.8 - "~~/src/HOL/Library/Nested_Environment" 5.9 + Nested_Environment 5.10 "~~/src/HOL/Library/List_Prefix" 5.11 begin 5.12