moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
authorwenzelm
Wed Aug 17 13:14:20 2011 +0200 (2011-08-17)
changeset 44236b73b7832b384
parent 44235 85e9dad3c187
child 44237 2a2040c9d898
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);
src/HOL/IsaMakefile
src/HOL/Library/Library.thy
src/HOL/Library/Nested_Environment.thy
src/HOL/Unix/Nested_Environment.thy
src/HOL/Unix/Unix.thy
     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