# HG changeset patch
# User wenzelm
# Date 1313579660 -7200
# Node ID b73b7832b3843fce2949412a521ad11a797a7f21
# Parent  85e9dad3c187c3a0a26850cd0c35662904409abd
moved theory Nested_Environment to HOL-Unix (a bit too specific for HOL-Library);

diff -r 85e9dad3c187 -r b73b7832b384 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Aug 17 10:03:58 2011 +0200
+++ b/src/HOL/IsaMakefile	Wed Aug 17 13:14:20 2011 +0200
@@ -437,39 +437,35 @@
   Library/Code_Char_ord.thy Library/Code_Integer.thy			\
   Library/Code_Natural.thy Library/Code_Prolog.thy			\
   Tools/Predicate_Compile/code_prolog.ML Library/ContNotDenum.thy	\
-  Library/Cset.thy Library/Cset_Monad.thy 				\
-  Library/Continuity.thy Library/Convex.thy Library/Countable.thy	\
-  Library/Diagonalize.thy Library/Dlist.thy Library/Dlist_Cset.thy 	\
-  Library/Efficient_Nat.thy Library/Eval_Witness.thy 			\
-  Library/Executable_Set.thy Library/Extended_Real.thy			\
-  Library/Extended_Nat.thy Library/Float.thy				\
+  Library/Cset.thy Library/Cset_Monad.thy Library/Continuity.thy	\
+  Library/Convex.thy Library/Countable.thy Library/Diagonalize.thy	\
+  Library/Dlist.thy Library/Dlist_Cset.thy Library/Efficient_Nat.thy	\
+  Library/Eval_Witness.thy Library/Executable_Set.thy			\
+  Library/Extended_Real.thy Library/Extended_Nat.thy Library/Float.thy	\
   Library/Formal_Power_Series.thy Library/Fraction_Field.thy		\
   Library/FrechetDeriv.thy Library/Cset.thy Library/FuncSet.thy		\
-  Library/Function_Algebras.thy Library/Fundamental_Theorem_Algebra.thy	\
-  Library/Glbs.thy Library/Indicator_Function.thy			\
-  Library/Infinite_Set.thy Library/Inner_Product.thy			\
-  Library/Kleene_Algebra.thy Library/LaTeXsugar.thy			\
-  Library/Lattice_Algebras.thy Library/Lattice_Syntax.thy		\
-  Library/Library.thy Library/List_Cset.thy Library/List_Prefix.thy	\
-  Library/List_lexord.thy Library/Mapping.thy Library/Monad_Syntax.thy	\
-  Library/More_List.thy Library/More_Set.thy Library/Multiset.thy	\
-  Library/Nat_Bijection.thy Library/Nested_Environment.thy		\
-  Library/Numeral_Type.thy Library/Old_Recdef.thy 			\
-  Library/OptionalSugar.thy						\
-  Library/Order_Relation.thy Library/Permutation.thy			\
-  Library/Permutations.thy Library/Poly_Deriv.thy			\
-  Library/Polynomial.thy Library/Predicate_Compile_Quickcheck.thy	\
-  Library/Preorder.thy Library/Product_Vector.thy			\
-  Library/Product_ord.thy Library/Product_plus.thy			\
-  Library/Product_Lattice.thy						\
-  Library/Quickcheck_Types.thy						\
-  Library/Quotient_List.thy Library/Quotient_Option.thy			\
-  Library/Quotient_Product.thy Library/Quotient_Sum.thy			\
-  Library/Quotient_Syntax.thy Library/Quotient_Type.thy			\
-  Library/RBT.thy Library/RBT_Impl.thy Library/RBT_Mapping.thy 		\
-  Library/README.html 							\
-  Library/Set_Algebras.thy Library/State_Monad.thy Library/Ramsey.thy	\
-  Library/Reflection.thy 			 			\
+  Library/Function_Algebras.thy						\
+  Library/Fundamental_Theorem_Algebra.thy Library/Glbs.thy		\
+  Library/Indicator_Function.thy Library/Infinite_Set.thy		\
+  Library/Inner_Product.thy Library/Kleene_Algebra.thy			\
+  Library/LaTeXsugar.thy Library/Lattice_Algebras.thy			\
+  Library/Lattice_Syntax.thy Library/Library.thy Library/List_Cset.thy	\
+  Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy	\
+  Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy	\
+  Library/Multiset.thy Library/Nat_Bijection.thy			\
+  Library/Numeral_Type.thy Library/Old_Recdef.thy			\
+  Library/OptionalSugar.thy Library/Order_Relation.thy			\
+  Library/Permutation.thy Library/Permutations.thy			\
+  Library/Poly_Deriv.thy Library/Polynomial.thy				\
+  Library/Predicate_Compile_Quickcheck.thy Library/Preorder.thy		\
+  Library/Product_Vector.thy Library/Product_ord.thy			\
+  Library/Product_plus.thy Library/Product_Lattice.thy			\
+  Library/Quickcheck_Types.thy Library/Quotient_List.thy		\
+  Library/Quotient_Option.thy Library/Quotient_Product.thy		\
+  Library/Quotient_Sum.thy Library/Quotient_Syntax.thy			\
+  Library/Quotient_Type.thy Library/RBT.thy Library/RBT_Impl.thy	\
+  Library/RBT_Mapping.thy Library/README.html Library/Set_Algebras.thy	\
+  Library/State_Monad.thy Library/Ramsey.thy Library/Reflection.thy	\
   Library/Sublist_Order.thy Library/Sum_of_Squares.thy			\
   Library/Sum_of_Squares/sos_wrapper.ML					\
   Library/Sum_of_Squares/sum_of_squares.ML				\
@@ -830,9 +826,9 @@
 
 HOL-Unix: HOL $(LOG)/HOL-Unix.gz
 
-$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy		\
-  Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy			\
-  Unix/document/root.bib Unix/document/root.tex
+$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/List_Prefix.thy Unix/ROOT.ML	\
+  Unix/Nested_Environment.thy Unix/Unix.thy Unix/document/root.bib	\
+  Unix/document/root.tex
 	@$(ISABELLE_TOOL) usedir -m no_brackets -m no_type_brackets $(OUT)/HOL Unix
 
 
diff -r 85e9dad3c187 -r b73b7832b384 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Wed Aug 17 10:03:58 2011 +0200
+++ b/src/HOL/Library/Library.thy	Wed Aug 17 13:14:20 2011 +0200
@@ -37,7 +37,6 @@
   Monad_Syntax
   More_List
   Multiset
-  Nested_Environment
   Numeral_Type
   Old_Recdef
   OptionalSugar
diff -r 85e9dad3c187 -r b73b7832b384 src/HOL/Library/Nested_Environment.thy
--- a/src/HOL/Library/Nested_Environment.thy	Wed Aug 17 10:03:58 2011 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,571 +0,0 @@
-(*  Title:      HOL/Library/Nested_Environment.thy
-    Author:     Markus Wenzel, TU Muenchen
-*)
-
-header {* Nested environments *}
-
-theory Nested_Environment
-imports Main
-begin
-
-text {*
-  Consider a partial function @{term [source] "e :: 'a => 'b option"};
-  this may be understood as an \emph{environment} mapping indexes
-  @{typ 'a} to optional entry values @{typ 'b} (cf.\ the basic theory
-  @{text Map} of Isabelle/HOL).  This basic idea is easily generalized
-  to that of a \emph{nested environment}, where entries may be either
-  basic values or again proper environments.  Then each entry is
-  accessed by a \emph{path}, i.e.\ a list of indexes leading to its
-  position within the structure.
-*}
-
-datatype ('a, 'b, 'c) env =
-    Val 'a
-  | Env 'b  "'c => ('a, 'b, 'c) env option"
-
-text {*
-  \medskip In the type @{typ "('a, 'b, 'c) env"} the parameter @{typ
-  'a} refers to basic values (occurring in terminal positions), type
-  @{typ 'b} to values associated with proper (inner) environments, and
-  type @{typ 'c} with the index type for branching.  Note that there
-  is no restriction on any of these types.  In particular, arbitrary
-  branching may yield rather large (transfinite) tree structures.
-*}
-
-
-subsection {* The lookup operation *}
-
-text {*
-  Lookup in nested environments works by following a given path of
-  index elements, leading to an optional result (a terminal value or
-  nested environment).  A \emph{defined position} within a nested
-  environment is one where @{term lookup} at its path does not yield
-  @{term None}.
-*}
-
-primrec
-  lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
-  and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option" where
-    "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
-  | "lookup (Env b es) xs =
-      (case xs of
-        [] => Some (Env b es)
-      | y # ys => lookup_option (es y) ys)"
-  | "lookup_option None xs = None"
-  | "lookup_option (Some e) xs = lookup e xs"
-
-hide_const lookup_option
-
-text {*
-  \medskip The characteristic cases of @{term lookup} are expressed by
-  the following equalities.
-*}
-
-theorem lookup_nil: "lookup e [] = Some e"
-  by (cases e) simp_all
-
-theorem lookup_val_cons: "lookup (Val a) (x # xs) = None"
-  by simp
-
-theorem lookup_env_cons:
-  "lookup (Env b es) (x # xs) =
-    (case es x of
-      None => None
-    | Some e => lookup e xs)"
-  by (cases "es x") simp_all
-
-lemmas lookup_lookup_option.simps [simp del]
-  and lookup_simps [simp] = lookup_nil lookup_val_cons lookup_env_cons
-
-theorem lookup_eq:
-  "lookup env xs =
-    (case xs of
-      [] => Some env
-    | x # xs =>
-      (case env of
-        Val a => None
-      | Env b es =>
-          (case es x of
-            None => None
-          | Some e => lookup e xs)))"
-  by (simp split: list.split env.split)
-
-text {*
-  \medskip Displaced @{term lookup} operations, relative to a certain
-  base path prefix, may be reduced as follows.  There are two cases,
-  depending whether the environment actually extends far enough to
-  follow the base path.
-*}
-
-theorem lookup_append_none:
-  assumes "lookup env xs = None"
-  shows "lookup env (xs @ ys) = None"
-  using assms
-proof (induct xs arbitrary: env)
-  case Nil
-  then have False by simp
-  then show ?case ..
-next
-  case (Cons x xs)
-  show ?case
-  proof (cases env)
-    case Val
-    then show ?thesis by simp
-  next
-    case (Env b es)
-    show ?thesis
-    proof (cases "es x")
-      case None
-      with Env show ?thesis by simp
-    next
-      case (Some e)
-      note es = `es x = Some e`
-      show ?thesis
-      proof (cases "lookup e xs")
-        case None
-        then have "lookup e (xs @ ys) = None" by (rule Cons.hyps)
-        with Env Some show ?thesis by simp
-      next
-        case Some
-        with Env es have False using Cons.prems by simp
-        then show ?thesis ..
-      qed
-    qed
-  qed
-qed
-
-theorem lookup_append_some:
-  assumes "lookup env xs = Some e"
-  shows "lookup env (xs @ ys) = lookup e ys"
-  using assms
-proof (induct xs arbitrary: env e)
-  case Nil
-  then have "env = e" by simp
-  then show "lookup env ([] @ ys) = lookup e ys" by simp
-next
-  case (Cons x xs)
-  note asm = `lookup env (x # xs) = Some e`
-  show "lookup env ((x # xs) @ ys) = lookup e ys"
-  proof (cases env)
-    case (Val a)
-    with asm have False by simp
-    then show ?thesis ..
-  next
-    case (Env b es)
-    show ?thesis
-    proof (cases "es x")
-      case None
-      with asm Env have False by simp
-      then show ?thesis ..
-    next
-      case (Some e')
-      note es = `es x = Some e'`
-      show ?thesis
-      proof (cases "lookup e' xs")
-        case None
-        with asm Env es have False by simp
-        then show ?thesis ..
-      next
-        case Some
-        with asm Env es have "lookup e' xs = Some e"
-          by simp
-        then have "lookup e' (xs @ ys) = lookup e ys" by (rule Cons.hyps)
-        with Env es show ?thesis by simp
-      qed
-    qed
-  qed
-qed
-
-text {*
-  \medskip Successful @{term lookup} deeper down an environment
-  structure means we are able to peek further up as well.  Note that
-  this is basically just the contrapositive statement of @{thm
-  [source] lookup_append_none} above.
-*}
-
-theorem lookup_some_append:
-  assumes "lookup env (xs @ ys) = Some e"
-  shows "\<exists>e. lookup env xs = Some e"
-proof -
-  from assms have "lookup env (xs @ ys) \<noteq> None" by simp
-  then have "lookup env xs \<noteq> None"
-    by (rule contrapos_nn) (simp only: lookup_append_none)
-  then show ?thesis by (simp)
-qed
-
-text {*
-  The subsequent statement describes in more detail how a successful
-  @{term lookup} with a non-empty path results in a certain situation
-  at any upper position.
-*}
-
-theorem lookup_some_upper:
-  assumes "lookup env (xs @ y # ys) = Some e"
-  shows "\<exists>b' es' env'.
-    lookup env xs = Some (Env b' es') \<and>
-    es' y = Some env' \<and>
-    lookup env' ys = Some e"
-  using assms
-proof (induct xs arbitrary: env e)
-  case Nil
-  from Nil.prems have "lookup env (y # ys) = Some e"
-    by simp
-  then obtain b' es' env' where
-      env: "env = Env b' es'" and
-      es': "es' y = Some env'" and
-      look': "lookup env' ys = Some e"
-    by (auto simp add: lookup_eq split: option.splits env.splits)
-  from env have "lookup env [] = Some (Env b' es')" by simp
-  with es' look' show ?case by blast
-next
-  case (Cons x xs)
-  from Cons.prems
-  obtain b' es' env' where
-      env: "env = Env b' es'" and
-      es': "es' x = Some env'" and
-      look': "lookup env' (xs @ y # ys) = Some e"
-    by (auto simp add: lookup_eq split: option.splits env.splits)
-  from Cons.hyps [OF look'] obtain b'' es'' env'' where
-      upper': "lookup env' xs = Some (Env b'' es'')" and
-      es'': "es'' y = Some env''" and
-      look'': "lookup env'' ys = Some e"
-    by blast
-  from env es' upper' have "lookup env (x # xs) = Some (Env b'' es'')"
-    by simp
-  with es'' look'' show ?case by blast
-qed
-
-
-subsection {* The update operation *}
-
-text {*
-  Update at a certain position in a nested environment may either
-  delete an existing entry, or overwrite an existing one.  Note that
-  update at undefined positions is simple absorbed, i.e.\ the
-  environment is left unchanged.
-*}
-
-primrec
-  update :: "'c list => ('a, 'b, 'c) env option
-    => ('a, 'b, 'c) env => ('a, 'b, 'c) env"
-  and update_option :: "'c list => ('a, 'b, 'c) env option
-    => ('a, 'b, 'c) env option => ('a, 'b, 'c) env option" where
-    "update xs opt (Val a) =
-      (if xs = [] then (case opt of None => Val a | Some e => e)
-      else Val a)"
-  | "update xs opt (Env b es) =
-      (case xs of
-        [] => (case opt of None => Env b es | Some e => e)
-      | y # ys => Env b (es (y := update_option ys opt (es y))))"
-  | "update_option xs opt None =
-      (if xs = [] then opt else None)"
-  | "update_option xs opt (Some e) =
-      (if xs = [] then opt else Some (update xs opt e))"
-
-hide_const update_option
-
-text {*
-  \medskip The characteristic cases of @{term update} are expressed by
-  the following equalities.
-*}
-
-theorem update_nil_none: "update [] None env = env"
-  by (cases env) simp_all
-
-theorem update_nil_some: "update [] (Some e) env = e"
-  by (cases env) simp_all
-
-theorem update_cons_val: "update (x # xs) opt (Val a) = Val a"
-  by simp
-
-theorem update_cons_nil_env:
-    "update [x] opt (Env b es) = Env b (es (x := opt))"
-  by (cases "es x") simp_all
-
-theorem update_cons_cons_env:
-  "update (x # y # ys) opt (Env b es) =
-    Env b (es (x :=
-      (case es x of
-        None => None
-      | Some e => Some (update (y # ys) opt e))))"
-  by (cases "es x") simp_all
-
-lemmas update_update_option.simps [simp del]
-  and update_simps [simp] = update_nil_none update_nil_some
-    update_cons_val update_cons_nil_env update_cons_cons_env
-
-lemma update_eq:
-  "update xs opt env =
-    (case xs of
-      [] =>
-        (case opt of
-          None => env
-        | Some e => e)
-    | x # xs =>
-        (case env of
-          Val a => Val a
-        | Env b es =>
-            (case xs of
-              [] => Env b (es (x := opt))
-            | y # ys =>
-                Env b (es (x :=
-                  (case es x of
-                    None => None
-                  | Some e => Some (update (y # ys) opt e)))))))"
-  by (simp split: list.split env.split option.split)
-
-text {*
-  \medskip The most basic correspondence of @{term lookup} and @{term
-  update} states that after @{term update} at a defined position,
-  subsequent @{term lookup} operations would yield the new value.
-*}
-
-theorem lookup_update_some:
-  assumes "lookup env xs = Some e"
-  shows "lookup (update xs (Some env') env) xs = Some env'"
-  using assms
-proof (induct xs arbitrary: env e)
-  case Nil
-  then have "env = e" by simp
-  then show ?case by simp
-next
-  case (Cons x xs)
-  note hyp = Cons.hyps
-    and asm = `lookup env (x # xs) = Some e`
-  show ?case
-  proof (cases env)
-    case (Val a)
-    with asm have False by simp
-    then show ?thesis ..
-  next
-    case (Env b es)
-    show ?thesis
-    proof (cases "es x")
-      case None
-      with asm Env have False by simp
-      then show ?thesis ..
-    next
-      case (Some e')
-      note es = `es x = Some e'`
-      show ?thesis
-      proof (cases xs)
-        case Nil
-        with Env show ?thesis by simp
-      next
-        case (Cons x' xs')
-        from asm Env es have "lookup e' xs = Some e" by simp
-        then have "lookup (update xs (Some env') e') xs = Some env'" by (rule hyp)
-        with Env es Cons show ?thesis by simp
-      qed
-    qed
-  qed
-qed
-
-text {*
-  \medskip The properties of displaced @{term update} operations are
-  analogous to those of @{term lookup} above.  There are two cases:
-  below an undefined position @{term update} is absorbed altogether,
-  and below a defined positions @{term update} affects subsequent
-  @{term lookup} operations in the obvious way.
-*}
-
-theorem update_append_none:
-  assumes "lookup env xs = None"
-  shows "update (xs @ y # ys) opt env = env"
-  using assms
-proof (induct xs arbitrary: env)
-  case Nil
-  then have False by simp
-  then show ?case ..
-next
-  case (Cons x xs)
-  note hyp = Cons.hyps
-    and asm = `lookup env (x # xs) = None`
-  show "update ((x # xs) @ y # ys) opt env = env"
-  proof (cases env)
-    case (Val a)
-    then show ?thesis by simp
-  next
-    case (Env b es)
-    show ?thesis
-    proof (cases "es x")
-      case None
-      note es = `es x = None`
-      show ?thesis
-        by (cases xs) (simp_all add: es Env fun_upd_idem_iff)
-    next
-      case (Some e)
-      note es = `es x = Some e`
-      show ?thesis
-      proof (cases xs)
-        case Nil
-        with asm Env Some have False by simp
-        then show ?thesis ..
-      next
-        case (Cons x' xs')
-        from asm Env es have "lookup e xs = None" by simp
-        then have "update (xs @ y # ys) opt e = e" by (rule hyp)
-        with Env es Cons show "update ((x # xs) @ y # ys) opt env = env"
-          by (simp add: fun_upd_idem_iff)
-      qed
-    qed
-  qed
-qed
-
-theorem update_append_some:
-  assumes "lookup env xs = Some e"
-  shows "lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)"
-  using assms
-proof (induct xs arbitrary: env e)
-  case Nil
-  then have "env = e" by simp
-  then show ?case by simp
-next
-  case (Cons x xs)
-  note hyp = Cons.hyps
-    and asm = `lookup env (x # xs) = Some e`
-  show "lookup (update ((x # xs) @ y # ys) opt env) (x # xs) =
-      Some (update (y # ys) opt e)"
-  proof (cases env)
-    case (Val a)
-    with asm have False by simp
-    then show ?thesis ..
-  next
-    case (Env b es)
-    show ?thesis
-    proof (cases "es x")
-      case None
-      with asm Env have False by simp
-      then show ?thesis ..
-    next
-      case (Some e')
-      note es = `es x = Some e'`
-      show ?thesis
-      proof (cases xs)
-        case Nil
-        with asm Env es have "e = e'" by simp
-        with Env es Nil show ?thesis by simp
-      next
-        case (Cons x' xs')
-        from asm Env es have "lookup e' xs = Some e" by simp
-        then have "lookup (update (xs @ y # ys) opt e') xs =
-          Some (update (y # ys) opt e)" by (rule hyp)
-        with Env es Cons show ?thesis by simp
-      qed
-    qed
-  qed
-qed
-
-text {*
-  \medskip Apparently, @{term update} does not affect the result of
-  subsequent @{term lookup} operations at independent positions, i.e.\
-  in case that the paths for @{term update} and @{term lookup} fork at
-  a certain point.
-*}
-
-theorem lookup_update_other:
-  assumes neq: "y \<noteq> (z::'c)"
-  shows "lookup (update (xs @ z # zs) opt env) (xs @ y # ys) =
-    lookup env (xs @ y # ys)"
-proof (induct xs arbitrary: env)
-  case Nil
-  show ?case
-  proof (cases env)
-    case Val
-    then show ?thesis by simp
-  next
-    case Env
-    show ?thesis
-    proof (cases zs)
-      case Nil
-      with neq Env show ?thesis by simp
-    next
-      case Cons
-      with neq Env show ?thesis by simp
-    qed
-  qed
-next
-  case (Cons x xs)
-  note hyp = Cons.hyps
-  show ?case
-  proof (cases env)
-    case Val
-    then show ?thesis by simp
-  next
-    case (Env y es)
-    show ?thesis
-    proof (cases xs)
-      case Nil
-      show ?thesis
-      proof (cases "es x")
-        case None
-        with Env Nil show ?thesis by simp
-      next
-        case Some
-        with neq hyp and Env Nil show ?thesis by simp
-      qed
-    next
-      case (Cons x' xs')
-      show ?thesis
-      proof (cases "es x")
-        case None
-        with Env Cons show ?thesis by simp
-      next
-        case Some
-        with neq hyp and Env Cons show ?thesis by simp
-      qed
-    qed
-  qed
-qed
-
-text {* Environments and code generation *}
-
-lemma [code, code del]:
-  "(HOL.equal :: (_, _, _) env \<Rightarrow> _) = HOL.equal" ..
-
-lemma equal_env_code [code]:
-  fixes x y :: "'a\<Colon>equal"
-    and f g :: "'c\<Colon>{equal, finite} \<Rightarrow> ('b\<Colon>equal, 'a, 'c) env option"
-  shows "HOL.equal (Env x f) (Env y g) \<longleftrightarrow>
-  HOL.equal x y \<and> (\<forall>z\<in>UNIV. case f z
-   of None \<Rightarrow> (case g z
-        of None \<Rightarrow> True | Some _ \<Rightarrow> False)
-    | Some a \<Rightarrow> (case g z
-        of None \<Rightarrow> False | Some b \<Rightarrow> HOL.equal a b))" (is ?env)
-    and "HOL.equal (Val a) (Val b) \<longleftrightarrow> HOL.equal a b"
-    and "HOL.equal (Val a) (Env y g) \<longleftrightarrow> False"
-    and "HOL.equal (Env x f) (Val b) \<longleftrightarrow> False"
-proof (unfold equal)
-  have "f = g \<longleftrightarrow> (\<forall>z. case f z
-   of None \<Rightarrow> (case g z
-        of None \<Rightarrow> True | Some _ \<Rightarrow> False)
-    | Some a \<Rightarrow> (case g z
-        of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" (is "?lhs = ?rhs")
-  proof
-    assume ?lhs
-    then show ?rhs by (auto split: option.splits)
-  next
-    assume assm: ?rhs (is "\<forall>z. ?prop z")
-    show ?lhs 
-    proof
-      fix z
-      from assm have "?prop z" ..
-      then show "f z = g z" by (auto split: option.splits)
-    qed
-  qed
-  then show "Env x f = Env y g \<longleftrightarrow>
-    x = y \<and> (\<forall>z\<in>UNIV. case f z
-     of None \<Rightarrow> (case g z
-          of None \<Rightarrow> True | Some _ \<Rightarrow> False)
-      | Some a \<Rightarrow> (case g z
-          of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
-qed simp_all
-
-lemma [code nbe]:
-  "HOL.equal (x :: (_, _, _) env) x \<longleftrightarrow> True"
-  by (fact equal_refl)
-
-lemma [code, code del]:
-  "(Code_Evaluation.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Evaluation.term_of" ..
-
-end
diff -r 85e9dad3c187 -r b73b7832b384 src/HOL/Unix/Nested_Environment.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Unix/Nested_Environment.thy	Wed Aug 17 13:14:20 2011 +0200
@@ -0,0 +1,571 @@
+(*  Title:      HOL/Unix/Nested_Environment.thy
+    Author:     Markus Wenzel, TU Muenchen
+*)
+
+header {* Nested environments *}
+
+theory Nested_Environment
+imports Main
+begin
+
+text {*
+  Consider a partial function @{term [source] "e :: 'a => 'b option"};
+  this may be understood as an \emph{environment} mapping indexes
+  @{typ 'a} to optional entry values @{typ 'b} (cf.\ the basic theory
+  @{text Map} of Isabelle/HOL).  This basic idea is easily generalized
+  to that of a \emph{nested environment}, where entries may be either
+  basic values or again proper environments.  Then each entry is
+  accessed by a \emph{path}, i.e.\ a list of indexes leading to its
+  position within the structure.
+*}
+
+datatype ('a, 'b, 'c) env =
+    Val 'a
+  | Env 'b  "'c => ('a, 'b, 'c) env option"
+
+text {*
+  \medskip In the type @{typ "('a, 'b, 'c) env"} the parameter @{typ
+  'a} refers to basic values (occurring in terminal positions), type
+  @{typ 'b} to values associated with proper (inner) environments, and
+  type @{typ 'c} with the index type for branching.  Note that there
+  is no restriction on any of these types.  In particular, arbitrary
+  branching may yield rather large (transfinite) tree structures.
+*}
+
+
+subsection {* The lookup operation *}
+
+text {*
+  Lookup in nested environments works by following a given path of
+  index elements, leading to an optional result (a terminal value or
+  nested environment).  A \emph{defined position} within a nested
+  environment is one where @{term lookup} at its path does not yield
+  @{term None}.
+*}
+
+primrec
+  lookup :: "('a, 'b, 'c) env => 'c list => ('a, 'b, 'c) env option"
+  and lookup_option :: "('a, 'b, 'c) env option => 'c list => ('a, 'b, 'c) env option" where
+    "lookup (Val a) xs = (if xs = [] then Some (Val a) else None)"
+  | "lookup (Env b es) xs =
+      (case xs of
+        [] => Some (Env b es)
+      | y # ys => lookup_option (es y) ys)"
+  | "lookup_option None xs = None"
+  | "lookup_option (Some e) xs = lookup e xs"
+
+hide_const lookup_option
+
+text {*
+  \medskip The characteristic cases of @{term lookup} are expressed by
+  the following equalities.
+*}
+
+theorem lookup_nil: "lookup e [] = Some e"
+  by (cases e) simp_all
+
+theorem lookup_val_cons: "lookup (Val a) (x # xs) = None"
+  by simp
+
+theorem lookup_env_cons:
+  "lookup (Env b es) (x # xs) =
+    (case es x of
+      None => None
+    | Some e => lookup e xs)"
+  by (cases "es x") simp_all
+
+lemmas lookup_lookup_option.simps [simp del]
+  and lookup_simps [simp] = lookup_nil lookup_val_cons lookup_env_cons
+
+theorem lookup_eq:
+  "lookup env xs =
+    (case xs of
+      [] => Some env
+    | x # xs =>
+      (case env of
+        Val a => None
+      | Env b es =>
+          (case es x of
+            None => None
+          | Some e => lookup e xs)))"
+  by (simp split: list.split env.split)
+
+text {*
+  \medskip Displaced @{term lookup} operations, relative to a certain
+  base path prefix, may be reduced as follows.  There are two cases,
+  depending whether the environment actually extends far enough to
+  follow the base path.
+*}
+
+theorem lookup_append_none:
+  assumes "lookup env xs = None"
+  shows "lookup env (xs @ ys) = None"
+  using assms
+proof (induct xs arbitrary: env)
+  case Nil
+  then have False by simp
+  then show ?case ..
+next
+  case (Cons x xs)
+  show ?case
+  proof (cases env)
+    case Val
+    then show ?thesis by simp
+  next
+    case (Env b es)
+    show ?thesis
+    proof (cases "es x")
+      case None
+      with Env show ?thesis by simp
+    next
+      case (Some e)
+      note es = `es x = Some e`
+      show ?thesis
+      proof (cases "lookup e xs")
+        case None
+        then have "lookup e (xs @ ys) = None" by (rule Cons.hyps)
+        with Env Some show ?thesis by simp
+      next
+        case Some
+        with Env es have False using Cons.prems by simp
+        then show ?thesis ..
+      qed
+    qed
+  qed
+qed
+
+theorem lookup_append_some:
+  assumes "lookup env xs = Some e"
+  shows "lookup env (xs @ ys) = lookup e ys"
+  using assms
+proof (induct xs arbitrary: env e)
+  case Nil
+  then have "env = e" by simp
+  then show "lookup env ([] @ ys) = lookup e ys" by simp
+next
+  case (Cons x xs)
+  note asm = `lookup env (x # xs) = Some e`
+  show "lookup env ((x # xs) @ ys) = lookup e ys"
+  proof (cases env)
+    case (Val a)
+    with asm have False by simp
+    then show ?thesis ..
+  next
+    case (Env b es)
+    show ?thesis
+    proof (cases "es x")
+      case None
+      with asm Env have False by simp
+      then show ?thesis ..
+    next
+      case (Some e')
+      note es = `es x = Some e'`
+      show ?thesis
+      proof (cases "lookup e' xs")
+        case None
+        with asm Env es have False by simp
+        then show ?thesis ..
+      next
+        case Some
+        with asm Env es have "lookup e' xs = Some e"
+          by simp
+        then have "lookup e' (xs @ ys) = lookup e ys" by (rule Cons.hyps)
+        with Env es show ?thesis by simp
+      qed
+    qed
+  qed
+qed
+
+text {*
+  \medskip Successful @{term lookup} deeper down an environment
+  structure means we are able to peek further up as well.  Note that
+  this is basically just the contrapositive statement of @{thm
+  [source] lookup_append_none} above.
+*}
+
+theorem lookup_some_append:
+  assumes "lookup env (xs @ ys) = Some e"
+  shows "\<exists>e. lookup env xs = Some e"
+proof -
+  from assms have "lookup env (xs @ ys) \<noteq> None" by simp
+  then have "lookup env xs \<noteq> None"
+    by (rule contrapos_nn) (simp only: lookup_append_none)
+  then show ?thesis by (simp)
+qed
+
+text {*
+  The subsequent statement describes in more detail how a successful
+  @{term lookup} with a non-empty path results in a certain situation
+  at any upper position.
+*}
+
+theorem lookup_some_upper:
+  assumes "lookup env (xs @ y # ys) = Some e"
+  shows "\<exists>b' es' env'.
+    lookup env xs = Some (Env b' es') \<and>
+    es' y = Some env' \<and>
+    lookup env' ys = Some e"
+  using assms
+proof (induct xs arbitrary: env e)
+  case Nil
+  from Nil.prems have "lookup env (y # ys) = Some e"
+    by simp
+  then obtain b' es' env' where
+      env: "env = Env b' es'" and
+      es': "es' y = Some env'" and
+      look': "lookup env' ys = Some e"
+    by (auto simp add: lookup_eq split: option.splits env.splits)
+  from env have "lookup env [] = Some (Env b' es')" by simp
+  with es' look' show ?case by blast
+next
+  case (Cons x xs)
+  from Cons.prems
+  obtain b' es' env' where
+      env: "env = Env b' es'" and
+      es': "es' x = Some env'" and
+      look': "lookup env' (xs @ y # ys) = Some e"
+    by (auto simp add: lookup_eq split: option.splits env.splits)
+  from Cons.hyps [OF look'] obtain b'' es'' env'' where
+      upper': "lookup env' xs = Some (Env b'' es'')" and
+      es'': "es'' y = Some env''" and
+      look'': "lookup env'' ys = Some e"
+    by blast
+  from env es' upper' have "lookup env (x # xs) = Some (Env b'' es'')"
+    by simp
+  with es'' look'' show ?case by blast
+qed
+
+
+subsection {* The update operation *}
+
+text {*
+  Update at a certain position in a nested environment may either
+  delete an existing entry, or overwrite an existing one.  Note that
+  update at undefined positions is simple absorbed, i.e.\ the
+  environment is left unchanged.
+*}
+
+primrec
+  update :: "'c list => ('a, 'b, 'c) env option
+    => ('a, 'b, 'c) env => ('a, 'b, 'c) env"
+  and update_option :: "'c list => ('a, 'b, 'c) env option
+    => ('a, 'b, 'c) env option => ('a, 'b, 'c) env option" where
+    "update xs opt (Val a) =
+      (if xs = [] then (case opt of None => Val a | Some e => e)
+      else Val a)"
+  | "update xs opt (Env b es) =
+      (case xs of
+        [] => (case opt of None => Env b es | Some e => e)
+      | y # ys => Env b (es (y := update_option ys opt (es y))))"
+  | "update_option xs opt None =
+      (if xs = [] then opt else None)"
+  | "update_option xs opt (Some e) =
+      (if xs = [] then opt else Some (update xs opt e))"
+
+hide_const update_option
+
+text {*
+  \medskip The characteristic cases of @{term update} are expressed by
+  the following equalities.
+*}
+
+theorem update_nil_none: "update [] None env = env"
+  by (cases env) simp_all
+
+theorem update_nil_some: "update [] (Some e) env = e"
+  by (cases env) simp_all
+
+theorem update_cons_val: "update (x # xs) opt (Val a) = Val a"
+  by simp
+
+theorem update_cons_nil_env:
+    "update [x] opt (Env b es) = Env b (es (x := opt))"
+  by (cases "es x") simp_all
+
+theorem update_cons_cons_env:
+  "update (x # y # ys) opt (Env b es) =
+    Env b (es (x :=
+      (case es x of
+        None => None
+      | Some e => Some (update (y # ys) opt e))))"
+  by (cases "es x") simp_all
+
+lemmas update_update_option.simps [simp del]
+  and update_simps [simp] = update_nil_none update_nil_some
+    update_cons_val update_cons_nil_env update_cons_cons_env
+
+lemma update_eq:
+  "update xs opt env =
+    (case xs of
+      [] =>
+        (case opt of
+          None => env
+        | Some e => e)
+    | x # xs =>
+        (case env of
+          Val a => Val a
+        | Env b es =>
+            (case xs of
+              [] => Env b (es (x := opt))
+            | y # ys =>
+                Env b (es (x :=
+                  (case es x of
+                    None => None
+                  | Some e => Some (update (y # ys) opt e)))))))"
+  by (simp split: list.split env.split option.split)
+
+text {*
+  \medskip The most basic correspondence of @{term lookup} and @{term
+  update} states that after @{term update} at a defined position,
+  subsequent @{term lookup} operations would yield the new value.
+*}
+
+theorem lookup_update_some:
+  assumes "lookup env xs = Some e"
+  shows "lookup (update xs (Some env') env) xs = Some env'"
+  using assms
+proof (induct xs arbitrary: env e)
+  case Nil
+  then have "env = e" by simp
+  then show ?case by simp
+next
+  case (Cons x xs)
+  note hyp = Cons.hyps
+    and asm = `lookup env (x # xs) = Some e`
+  show ?case
+  proof (cases env)
+    case (Val a)
+    with asm have False by simp
+    then show ?thesis ..
+  next
+    case (Env b es)
+    show ?thesis
+    proof (cases "es x")
+      case None
+      with asm Env have False by simp
+      then show ?thesis ..
+    next
+      case (Some e')
+      note es = `es x = Some e'`
+      show ?thesis
+      proof (cases xs)
+        case Nil
+        with Env show ?thesis by simp
+      next
+        case (Cons x' xs')
+        from asm Env es have "lookup e' xs = Some e" by simp
+        then have "lookup (update xs (Some env') e') xs = Some env'" by (rule hyp)
+        with Env es Cons show ?thesis by simp
+      qed
+    qed
+  qed
+qed
+
+text {*
+  \medskip The properties of displaced @{term update} operations are
+  analogous to those of @{term lookup} above.  There are two cases:
+  below an undefined position @{term update} is absorbed altogether,
+  and below a defined positions @{term update} affects subsequent
+  @{term lookup} operations in the obvious way.
+*}
+
+theorem update_append_none:
+  assumes "lookup env xs = None"
+  shows "update (xs @ y # ys) opt env = env"
+  using assms
+proof (induct xs arbitrary: env)
+  case Nil
+  then have False by simp
+  then show ?case ..
+next
+  case (Cons x xs)
+  note hyp = Cons.hyps
+    and asm = `lookup env (x # xs) = None`
+  show "update ((x # xs) @ y # ys) opt env = env"
+  proof (cases env)
+    case (Val a)
+    then show ?thesis by simp
+  next
+    case (Env b es)
+    show ?thesis
+    proof (cases "es x")
+      case None
+      note es = `es x = None`
+      show ?thesis
+        by (cases xs) (simp_all add: es Env fun_upd_idem_iff)
+    next
+      case (Some e)
+      note es = `es x = Some e`
+      show ?thesis
+      proof (cases xs)
+        case Nil
+        with asm Env Some have False by simp
+        then show ?thesis ..
+      next
+        case (Cons x' xs')
+        from asm Env es have "lookup e xs = None" by simp
+        then have "update (xs @ y # ys) opt e = e" by (rule hyp)
+        with Env es Cons show "update ((x # xs) @ y # ys) opt env = env"
+          by (simp add: fun_upd_idem_iff)
+      qed
+    qed
+  qed
+qed
+
+theorem update_append_some:
+  assumes "lookup env xs = Some e"
+  shows "lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)"
+  using assms
+proof (induct xs arbitrary: env e)
+  case Nil
+  then have "env = e" by simp
+  then show ?case by simp
+next
+  case (Cons x xs)
+  note hyp = Cons.hyps
+    and asm = `lookup env (x # xs) = Some e`
+  show "lookup (update ((x # xs) @ y # ys) opt env) (x # xs) =
+      Some (update (y # ys) opt e)"
+  proof (cases env)
+    case (Val a)
+    with asm have False by simp
+    then show ?thesis ..
+  next
+    case (Env b es)
+    show ?thesis
+    proof (cases "es x")
+      case None
+      with asm Env have False by simp
+      then show ?thesis ..
+    next
+      case (Some e')
+      note es = `es x = Some e'`
+      show ?thesis
+      proof (cases xs)
+        case Nil
+        with asm Env es have "e = e'" by simp
+        with Env es Nil show ?thesis by simp
+      next
+        case (Cons x' xs')
+        from asm Env es have "lookup e' xs = Some e" by simp
+        then have "lookup (update (xs @ y # ys) opt e') xs =
+          Some (update (y # ys) opt e)" by (rule hyp)
+        with Env es Cons show ?thesis by simp
+      qed
+    qed
+  qed
+qed
+
+text {*
+  \medskip Apparently, @{term update} does not affect the result of
+  subsequent @{term lookup} operations at independent positions, i.e.\
+  in case that the paths for @{term update} and @{term lookup} fork at
+  a certain point.
+*}
+
+theorem lookup_update_other:
+  assumes neq: "y \<noteq> (z::'c)"
+  shows "lookup (update (xs @ z # zs) opt env) (xs @ y # ys) =
+    lookup env (xs @ y # ys)"
+proof (induct xs arbitrary: env)
+  case Nil
+  show ?case
+  proof (cases env)
+    case Val
+    then show ?thesis by simp
+  next
+    case Env
+    show ?thesis
+    proof (cases zs)
+      case Nil
+      with neq Env show ?thesis by simp
+    next
+      case Cons
+      with neq Env show ?thesis by simp
+    qed
+  qed
+next
+  case (Cons x xs)
+  note hyp = Cons.hyps
+  show ?case
+  proof (cases env)
+    case Val
+    then show ?thesis by simp
+  next
+    case (Env y es)
+    show ?thesis
+    proof (cases xs)
+      case Nil
+      show ?thesis
+      proof (cases "es x")
+        case None
+        with Env Nil show ?thesis by simp
+      next
+        case Some
+        with neq hyp and Env Nil show ?thesis by simp
+      qed
+    next
+      case (Cons x' xs')
+      show ?thesis
+      proof (cases "es x")
+        case None
+        with Env Cons show ?thesis by simp
+      next
+        case Some
+        with neq hyp and Env Cons show ?thesis by simp
+      qed
+    qed
+  qed
+qed
+
+text {* Environments and code generation *}
+
+lemma [code, code del]:
+  "(HOL.equal :: (_, _, _) env \<Rightarrow> _) = HOL.equal" ..
+
+lemma equal_env_code [code]:
+  fixes x y :: "'a\<Colon>equal"
+    and f g :: "'c\<Colon>{equal, finite} \<Rightarrow> ('b\<Colon>equal, 'a, 'c) env option"
+  shows "HOL.equal (Env x f) (Env y g) \<longleftrightarrow>
+  HOL.equal x y \<and> (\<forall>z\<in>UNIV. case f z
+   of None \<Rightarrow> (case g z
+        of None \<Rightarrow> True | Some _ \<Rightarrow> False)
+    | Some a \<Rightarrow> (case g z
+        of None \<Rightarrow> False | Some b \<Rightarrow> HOL.equal a b))" (is ?env)
+    and "HOL.equal (Val a) (Val b) \<longleftrightarrow> HOL.equal a b"
+    and "HOL.equal (Val a) (Env y g) \<longleftrightarrow> False"
+    and "HOL.equal (Env x f) (Val b) \<longleftrightarrow> False"
+proof (unfold equal)
+  have "f = g \<longleftrightarrow> (\<forall>z. case f z
+   of None \<Rightarrow> (case g z
+        of None \<Rightarrow> True | Some _ \<Rightarrow> False)
+    | Some a \<Rightarrow> (case g z
+        of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" (is "?lhs = ?rhs")
+  proof
+    assume ?lhs
+    then show ?rhs by (auto split: option.splits)
+  next
+    assume assm: ?rhs (is "\<forall>z. ?prop z")
+    show ?lhs
+    proof
+      fix z
+      from assm have "?prop z" ..
+      then show "f z = g z" by (auto split: option.splits)
+    qed
+  qed
+  then show "Env x f = Env y g \<longleftrightarrow>
+    x = y \<and> (\<forall>z\<in>UNIV. case f z
+     of None \<Rightarrow> (case g z
+          of None \<Rightarrow> True | Some _ \<Rightarrow> False)
+      | Some a \<Rightarrow> (case g z
+          of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
+qed simp_all
+
+lemma [code nbe]:
+  "HOL.equal (x :: (_, _, _) env) x \<longleftrightarrow> True"
+  by (fact equal_refl)
+
+lemma [code, code del]:
+  "(Code_Evaluation.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Evaluation.term_of" ..
+
+end
diff -r 85e9dad3c187 -r b73b7832b384 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Wed Aug 17 10:03:58 2011 +0200
+++ b/src/HOL/Unix/Unix.thy	Wed Aug 17 13:14:20 2011 +0200
@@ -6,8 +6,7 @@
 
 theory Unix
 imports
-  Main
-  "~~/src/HOL/Library/Nested_Environment"
+  Nested_Environment
   "~~/src/HOL/Library/List_Prefix"
 begin