1.1 --- a/src/HOL/Unix/Nested_Environment.thy	Thu Aug 18 15:39:00 2011 +0200
     1.2 +++ b/src/HOL/Unix/Nested_Environment.thy	Thu Aug 18 15:51:34 2011 +0200
     1.3 @@ -518,7 +518,8 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 -text {* Environments and code generation *}
     1.8 +
     1.9 +subsection {* Code generation *}
    1.10  
    1.11  lemma [code, code del]:
    1.12    "(HOL.equal :: (_, _, _) env \<Rightarrow> _) = HOL.equal" ..
    1.13 @@ -526,39 +527,37 @@
    1.14  lemma equal_env_code [code]:
    1.15    fixes x y :: "'a\<Colon>equal"
    1.16      and f g :: "'c\<Colon>{equal, finite} \<Rightarrow> ('b\<Colon>equal, 'a, 'c) env option"
    1.17 -  shows "HOL.equal (Env x f) (Env y g) \<longleftrightarrow>
    1.18 -  HOL.equal x y \<and> (\<forall>z\<in>UNIV. case f z
    1.19 -   of None \<Rightarrow> (case g z
    1.20 -        of None \<Rightarrow> True | Some _ \<Rightarrow> False)
    1.21 -    | Some a \<Rightarrow> (case g z
    1.22 -        of None \<Rightarrow> False | Some b \<Rightarrow> HOL.equal a b))" (is ?env)
    1.23 +  shows
    1.24 +    "HOL.equal (Env x f) (Env y g) \<longleftrightarrow>
    1.25 +      HOL.equal x y \<and> (\<forall>z \<in> UNIV.
    1.26 +        case f z of
    1.27 +          None \<Rightarrow> (case g z of None \<Rightarrow> True | Some _ \<Rightarrow> False)
    1.28 +        | Some a \<Rightarrow> (case g z of None \<Rightarrow> False | Some b \<Rightarrow> HOL.equal a b))" (is ?env)
    1.29      and "HOL.equal (Val a) (Val b) \<longleftrightarrow> HOL.equal a b"
    1.30      and "HOL.equal (Val a) (Env y g) \<longleftrightarrow> False"
    1.31      and "HOL.equal (Env x f) (Val b) \<longleftrightarrow> False"
    1.32  proof (unfold equal)
    1.33 -  have "f = g \<longleftrightarrow> (\<forall>z. case f z
    1.34 -   of None \<Rightarrow> (case g z
    1.35 -        of None \<Rightarrow> True | Some _ \<Rightarrow> False)
    1.36 -    | Some a \<Rightarrow> (case g z
    1.37 -        of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" (is "?lhs = ?rhs")
    1.38 +  have "f = g \<longleftrightarrow>
    1.39 +    (\<forall>z. case f z of
    1.40 +      None \<Rightarrow> (case g z of None \<Rightarrow> True | Some _ \<Rightarrow> False)
    1.41 +    | Some a \<Rightarrow> (case g z of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" (is "?lhs = ?rhs")
    1.42    proof
    1.43      assume ?lhs
    1.44      then show ?rhs by (auto split: option.splits)
    1.45    next
    1.46 -    assume assm: ?rhs (is "\<forall>z. ?prop z")
    1.47 +    assume ?rhs (is "\<forall>z. ?prop z")
    1.48      show ?lhs
    1.49      proof
    1.50        fix z
    1.51 -      from assm have "?prop z" ..
    1.52 +      from `?rhs` have "?prop z" ..
    1.53        then show "f z = g z" by (auto split: option.splits)
    1.54      qed
    1.55    qed
    1.56    then show "Env x f = Env y g \<longleftrightarrow>
    1.57 -    x = y \<and> (\<forall>z\<in>UNIV. case f z
    1.58 -     of None \<Rightarrow> (case g z
    1.59 -          of None \<Rightarrow> True | Some _ \<Rightarrow> False)
    1.60 -      | Some a \<Rightarrow> (case g z
    1.61 -          of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
    1.62 +    x = y \<and> (\<forall>z\<in>UNIV.
    1.63 +      case f z of
    1.64 +        None \<Rightarrow> (case g z of None \<Rightarrow> True | Some _ \<Rightarrow> False)
    1.65 +      | Some a \<Rightarrow> (case g z of None \<Rightarrow> False | Some b \<Rightarrow> a = b))" by simp
    1.66  qed simp_all
    1.67  
    1.68  lemma [code nbe]:
    1.69 @@ -566,6 +565,8 @@
    1.70    by (fact equal_refl)
    1.71  
    1.72  lemma [code, code del]:
    1.73 -  "(Code_Evaluation.term_of :: ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) = Code_Evaluation.term_of" ..
    1.74 +  "(Code_Evaluation.term_of ::
    1.75 +    ('a::{term_of, type}, 'b::{term_of, type}, 'c::{term_of, type}) env \<Rightarrow> term) =
    1.76 +      Code_Evaluation.term_of" ..
    1.77  
    1.78  end