author wenzelm Wed, 16 Jan 2013 21:50:39 +0100 changeset 50918 3b6417e9f73e parent 50917 9459f59cff09 child 50919 cc03437a1f80
tuned proofs;
--- 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 -
--- 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])