added explicit equation for equality of nested environments

--- a/src/HOL/Library/Nested_Environment.thy	Mon Aug 27 08:31:01 2007 +0200
+++ b/src/HOL/Library/Nested_Environment.thy	Mon Aug 27 11:34:14 2007 +0200
@@ -523,4 +523,43 @@
   qed
 qed
 
+text {* Equality of environments for code generation *}
+
+lemma [code func, code func del]:
+  fixes e1 e2 :: "('b\<Colon>eq, 'a\<Colon>eq, 'c\<Colon>eq) env"
+  shows "e1 = e2 \<longleftrightarrow> e1 = e2" ..
+
+lemma eq_env_code [code func]:
+  fixes x y :: "'a\<Colon>eq"
+    and f g :: "'c\<Colon>{eq, finite} \<Rightarrow> ('b\<Colon>eq, 'a, 'c) env option"
+  shows "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))" (is ?env)
+    and "Val a = Val b \<longleftrightarrow> a = b"
+    and "Val a = Env y g \<longleftrightarrow> False"
+    and "Env x f = Val b \<longleftrightarrow> False"
+proof -
+  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 by simp
+qed simp_all
+
 end

--- a/src/HOL/ex/ExecutableContent.thy	Mon Aug 27 08:31:01 2007 +0200
+++ b/src/HOL/ex/ExecutableContent.thy	Mon Aug 27 11:34:14 2007 +0200
@@ -19,7 +19,7 @@
   List_Prefix
   Nat_Infinity
   NatPair
-  (*Nested_Environment*)
+  Nested_Environment
   Permutation
   Primes
   Product_ord