--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Tue Sep 30 15:10:26 2003 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Tue Sep 30 15:10:59 2003 +0200
@@ -339,10 +339,11 @@
have FE: "F \<unlhd> E" .
have F: "vectorspace F" ..
have linearform: "linearform F f" .
- have F_norm: "normed_vectorspace F norm" ..
+ have F_norm: "normed_vectorspace F norm"
+ by (rule subspace_normed_vs [OF _ _ _ norm.intro])
have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
by (rule normed_vectorspace.fn_norm_ge_zero
- [OF F_norm, folded B_def fn_norm_def])
+ [OF F_norm _ continuous.intro, folded B_def fn_norm_def])
txt {* We define a function @{text p} on @{text E} as follows:
@{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} *}
@@ -394,7 +395,7 @@
fix x assume "x \<in> F"
show "\<bar>f x\<bar> \<le> p x"
by (unfold p_def) (rule normed_vectorspace.fn_norm_le_cong
- [OF F_norm, folded B_def fn_norm_def])
+ [OF F_norm _ continuous.intro, folded B_def fn_norm_def])
qed
txt {* Using the fact that @{text p} is a seminorm and @{text f} is bounded
@@ -443,7 +444,7 @@
with b show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
by (simp only: p_def)
qed
- from continuous.axioms [OF g_cont] this ge_zero
+ from linearformE 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])
@@ -456,7 +457,7 @@
fix x assume x: "x \<in> F"
from a have "g x = f x" ..
hence "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
- also from continuous.axioms [OF g_cont]
+ also from linearformE g_cont
have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
proof (rule fn_norm_le_cong [of g, folded B_def fn_norm_def])
from FE x show "x \<in> E" ..
@@ -464,8 +465,10 @@
finally show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" .
qed
show "0 \<le> \<parallel>g\<parallel>\<hyphen>E"
- using continuous.axioms [OF g_cont]
+ using linearformE g_cont
by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
+ next
+ show "continuous F norm f" by (rule continuous.intro)
qed
qed
with linearformE a g_cont show ?thesis by blast