moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
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