# HG changeset patch
# User wenzelm
# Date 1313675494 -7200
# Node ID d4d48d75aac3fbe2ca6fce728aaa6f0e1e62fea7
# Parent  d9c7bf932eabc23f08a2645267670f888880739f
tuned document;
tuned proofs;

diff -r d9c7bf932eab -r d4d48d75aac3 src/HOL/Unix/Nested_Environment.thy
--- a/src/HOL/Unix/Nested_Environment.thy	Thu Aug 18 15:39:00 2011 +0200
+++ b/src/HOL/Unix/Nested_Environment.thy	Thu Aug 18 15:51:34 2011 +0200
@@ -518,7 +518,8 @@
   qed
 qed
 
-text {* Environments and code generation *}
+
+subsection {* Code generation *}
 
 lemma [code, code del]:
   "(HOL.equal :: (_, _, _) env \<Rightarrow> _) = HOL.equal" ..
@@ -526,39 +527,37 @@
 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)
+  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")
+  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")
+    assume ?rhs (is "\<forall>z. ?prop z")
     show ?lhs
     proof
       fix z
-      from assm have "?prop z" ..
+      from `?rhs` 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
+    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]:
@@ -566,6 +565,8 @@
   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" ..
+  "(Code_Evaluation.term_of ::
+    ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) =
+      Code_Evaluation.term_of" ..
 
 end