# HG changeset patch
# User wenzelm
# Date 1358369439 -3600
# Node ID 3b6417e9f73e225a49e86e6c41b1903a7faf8275
# Parent  9459f59cff0941bda98790ff3ca9afae392dc07b
tuned proofs;

diff -r 9459f59cff09 -r 3b6417e9f73e src/HOL/Hahn_Banach/Function_Norm.thy
--- a/src/HOL/Hahn_Banach/Function_Norm.thy	Wed Jan 16 21:49:56 2013 +0100
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy	Wed Jan 16 21:50:39 2013 +0100
@@ -244,7 +244,7 @@
 
 lemma (in normed_vectorspace_with_fn_norm) fn_norm_least [intro?]:
   assumes "continuous V f norm"
-  assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
+  assumes ineq: "\<And>x. x \<in> V \<Longrightarrow> \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
   shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
 proof -
   interpret continuous V f norm by fact
@@ -265,7 +265,7 @@
       proof (rule mult_right_mono)
         have "0 < \<parallel>x\<parallel>" using x x_neq ..
         then show "0 \<le> inverse \<parallel>x\<parallel>" by simp
-        from ineq and x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
+        from x show "\<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" by (rule ineq)
       qed
       also have "\<dots> = c"
       proof -
diff -r 9459f59cff09 -r 3b6417e9f73e src/HOL/Hahn_Banach/Hahn_Banach.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Wed Jan 16 21:49:56 2013 +0100
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Wed Jan 16 21:50:39 2013 +0100
@@ -469,15 +469,13 @@
       \end{center}
     *}
 
-    have "\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
+    from g_cont _ ge_zero
+    show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"
     proof
       fix x assume "x \<in> E"
       with b show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
         by (simp only: p_def)
     qed
-    from g_cont this ge_zero
-    show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"
-      by (rule fn_norm_least [of g, folded B_def fn_norm_def])
 
     txt {* The other direction is achieved by a similar argument. *}
 
@@ -485,9 +483,9 @@
     proof (rule normed_vectorspace_with_fn_norm.fn_norm_least
         [OF normed_vectorspace_with_fn_norm.intro,
          OF F_norm, folded B_def fn_norm_def])
-      show "\<forall>x \<in> F. \<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
-      proof
-        fix x assume x: "x \<in> F"
+      fix x assume x: "x \<in> F"
+      show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
+      proof -
         from a x have "g x = f x" ..
         then have "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
         also from g_cont
@@ -495,8 +493,9 @@
         proof (rule fn_norm_le_cong [OF _ linearformE, folded B_def fn_norm_def])
           from FE x show "x \<in> E" ..
         qed
-        finally show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" .
+        finally show ?thesis .
       qed
+    next
       show "0 \<le> \<parallel>g\<parallel>\<hyphen>E"
         using g_cont
         by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])