--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy Thu Aug 29 11:15:36 2002 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy Thu Aug 29 16:08:30 2002 +0200
@@ -53,9 +53,9 @@
empty set. Since @{text \<real>} is unbounded, there would be no supremum.
To avoid this situation it must be guaranteed that there is an
element in this set. This element must be @{text "{} \<ge> 0"} so that
- @{text function_norm} has the norm properties. Furthermore
- it does not have to change the norm in all other cases, so it must
- be @{text 0}, as all other elements are @{text "{} \<ge> 0"}.
+ @{text fn_norm} has the norm properties. Furthermore it does not
+ have to change the norm in all other cases, so it must be @{text 0},
+ as all other elements are @{text "{} \<ge> 0"}.
Thus we define the set @{text B} where the supremum is taken from as
follows:
@@ -63,31 +63,25 @@
@{text "{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}"}
\end{center}
- @{text function_norm} is equal to the supremum of @{text B}, if the
+ @{text fn_norm} is equal to the supremum of @{text B}, if the
supremum exists (otherwise it is undefined).
*}
-locale function_norm = norm_syntax +
- fixes B
- defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
- fixes function_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
+locale fn_norm = norm_syntax +
+ fixes B defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
+ fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
-lemma (in function_norm) B_not_empty [intro]: "0 \<in> B V f"
- by (unfold B_def) simp
-
-locale (open) functional_vectorspace =
- normed_vectorspace + function_norm +
- fixes cont
- defines "cont f \<equiv> continuous V norm f"
+lemma (in fn_norm) B_not_empty [intro]: "0 \<in> B V f"
+ by (simp add: B_def)
text {*
The following lemma states that every continuous linear form on a
normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
*}
-lemma (in functional_vectorspace) function_norm_works:
- includes continuous
+lemma (in normed_vectorspace) fn_norm_works: (* FIXME bug with "(in fn_norm)" !? *)
+ includes fn_norm + continuous
shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
proof -
txt {* The existence of the supremum is shown using the
@@ -148,38 +142,40 @@
thus ?thesis ..
qed
qed
- then show ?thesis
- by (unfold function_norm_def) (rule the_lubI_ex)
+ then show ?thesis by (unfold fn_norm_def) (rule the_lubI_ex)
qed
-lemma (in functional_vectorspace) function_norm_ub [intro?]:
- includes continuous
+lemma (in normed_vectorspace) fn_norm_ub [iff?]:
+ includes fn_norm + continuous
assumes b: "b \<in> B V f"
shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
proof -
- have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" by (rule function_norm_works)
+ have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
+ by (unfold B_def fn_norm_def) (rule fn_norm_works)
from this and b show ?thesis ..
qed
-lemma (in functional_vectorspace) function_norm_least' [intro?]:
- includes continuous
+lemma (in normed_vectorspace) fn_norm_leastB:
+ includes fn_norm + continuous
assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
proof -
- have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" by (rule function_norm_works)
+ have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
+ by (unfold B_def fn_norm_def) (rule fn_norm_works)
from this and b show ?thesis ..
qed
text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
-lemma (in functional_vectorspace) function_norm_ge_zero [iff]:
- includes continuous
+lemma (in normed_vectorspace) fn_norm_ge_zero [iff]:
+ includes fn_norm + continuous
shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
proof -
txt {* The function norm is defined as the supremum of @{text B}.
So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
0"}, provided the supremum exists and @{text B} is not empty. *}
- have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" by (rule function_norm_works)
+ have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
+ by (unfold B_def fn_norm_def) (rule fn_norm_works)
moreover have "0 \<in> B V f" ..
ultimately show ?thesis ..
qed
@@ -191,8 +187,8 @@
\end{center}
*}
-lemma (in functional_vectorspace) function_norm_le_cong:
- includes continuous + vectorspace_linearform
+lemma (in normed_vectorspace) fn_norm_le_cong:
+ includes fn_norm + continuous + linearform
assumes x: "x \<in> V"
shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
proof cases
@@ -202,7 +198,7 @@
also have "\<bar>\<dots>\<bar> = 0" by simp
also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
proof (rule real_le_mult_order1a)
- show "0 \<le> \<parallel>f\<parallel>\<hyphen>V" ..
+ show "0 \<le> \<parallel>f\<parallel>\<hyphen>V" by (unfold B_def fn_norm_def) rule
show "0 \<le> norm x" ..
qed
finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
@@ -213,11 +209,10 @@
also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
proof (rule real_mult_le_le_mono2)
from x show "0 \<le> \<parallel>x\<parallel>" ..
- show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
- proof
- from x and neq show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
- by (auto simp add: B_def real_divide_def)
- qed
+ from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
+ by (auto simp add: B_def real_divide_def)
+ then show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
+ by (unfold B_def fn_norm_def) (rule fn_norm_ub)
qed
finally show ?thesis .
qed
@@ -230,11 +225,11 @@
\end{center}
*}
-lemma (in functional_vectorspace) function_norm_least [intro?]:
- includes continuous
+lemma (in normed_vectorspace) fn_norm_least [intro?]:
+ includes fn_norm + continuous
assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
-proof (rule function_norm_least')
+proof (rule fn_norm_leastB [folded B_def fn_norm_def])
fix b assume b: "b \<in> B V f"
show "b \<le> c"
proof cases
@@ -261,9 +256,4 @@
qed
qed
-lemmas [iff?] =
- functional_vectorspace.function_norm_ge_zero
- functional_vectorspace.function_norm_le_cong
- functional_vectorspace.function_norm_least
-
end
--- a/src/HOL/Real/HahnBanach/HahnBanach.thy Thu Aug 29 11:15:36 2002 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy Thu Aug 29 16:08:30 2002 +0200
@@ -53,8 +53,7 @@
*}
theorem HahnBanach:
- includes vectorspace E + subvectorspace F E +
- seminorm_vectorspace E p + linearform F f
+ includes vectorspace E + subspace F E + seminorm E p + linearform F f
assumes fp: "\<forall>x \<in> F. f x \<le> p x"
shows "\<exists>h. linearform E h \<and> (\<forall>x \<in> F. h x = f x) \<and> (\<forall>x \<in> E. h x \<le> p x)"
-- {* Let @{text E} be a vector space, @{text F} a subspace of @{text E}, @{text p} a seminorm on @{text E}, *}
@@ -63,6 +62,7 @@
proof -
def M \<equiv> "norm_pres_extensions E p F f"
hence M: "M = \<dots>" by (simp only:)
+ have E: "vectorspace E" .
have F: "vectorspace F" ..
{
fix c assume cM: "c \<in> chain M" and ex: "\<exists>x. x \<in> c"
@@ -121,7 +121,7 @@
-- {* @{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E}, *}
-- {* and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \skp *}
from HE have H: "vectorspace H"
- by (rule subvectorspace.vectorspace)
+ by (rule subspace.vectorspace)
have HE_eq: "H = E"
-- {* We show that @{text h} is defined on whole @{text E} by classical contradiction. \skp *}
@@ -164,7 +164,7 @@
fix u v assume u: "u \<in> H" and v: "v \<in> H"
with HE have uE: "u \<in> E" and vE: "v \<in> E" by auto
from H u v linearform have "h v - h u = h (v - u)"
- by (simp add: vectorspace_linearform.diff)
+ by (simp add: linearform.diff)
also from hp and H u v have "\<dots> \<le> p (v - u)"
by (simp only: vectorspace.diff_closed)
also from x'E uE vE have "v - u = x' + - x' + v + - u"
@@ -173,11 +173,10 @@
by (simp add: add_ac)
also from x'E uE vE have "\<dots> = (v + x') - (u + x')"
by (simp add: diff_eq1)
- also from x'E uE vE have "p \<dots> \<le> p (v + x') + p (u + x')"
+ also from x'E uE vE E have "p \<dots> \<le> p (v + x') + p (u + x')"
by (simp add: diff_subadditive)
finally have "h v - h u \<le> p (v + x') + p (u + x')" .
- then show "- p (u + x') - h u \<le> p (v + x') - h v"
- by simp
+ then show "- p (u + x') - h u \<le> p (v + x') - h v" by simp
qed
then show ?thesis ..
qed
@@ -298,8 +297,7 @@
*}
theorem abs_HahnBanach:
- includes vectorspace E + subvectorspace F E +
- linearform F f + seminorm_vectorspace E p
+ includes vectorspace E + subspace F E + linearform F f + seminorm E p
assumes fp: "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
shows "\<exists>g. linearform E g
\<and> (\<forall>x \<in> F. g x = f x)
@@ -330,8 +328,7 @@
*}
theorem norm_HahnBanach:
- includes functional_vectorspace E + subvectorspace F E +
- linearform F f + continuous F norm f
+ includes normed_vectorspace E + subspace F E + linearform F f + fn_norm + continuous F norm f
shows "\<exists>g. linearform E g
\<and> continuous E norm g
\<and> (\<forall>x \<in> F. g x = f x)
@@ -343,6 +340,9 @@
have F: "vectorspace F" ..
have linearform: "linearform F f" .
have F_norm: "normed_vectorspace F norm" ..
+ 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])
txt {* We define a function @{text p} on @{text E} as follows:
@{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} *}
@@ -356,9 +356,7 @@
txt {* @{text p} is positive definite: *}
show "0 \<le> p x"
proof (unfold p_def, rule real_le_mult_order1a)
- show "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
- apply (unfold function_norm_def B_def)
- using normed_vectorspace.axioms [OF F_norm] ..
+ show "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
from x show "0 \<le> \<parallel>x\<parallel>" ..
qed
@@ -366,14 +364,10 @@
show "p (a \<cdot> x) = \<bar>a\<bar> * p x"
proof -
- have "p (a \<cdot> x) = \<parallel>f\<parallel>\<hyphen>F * \<parallel>a \<cdot> x\<parallel>"
- by (simp only: p_def)
- also from x have "\<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
- by (rule abs_homogenous)
- also have "\<parallel>f\<parallel>\<hyphen>F * (\<bar>a\<bar> * \<parallel>x\<parallel>) = \<bar>a\<bar> * (\<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>)"
- by simp
- also have "\<dots> = \<bar>a\<bar> * p x"
- by (simp only: p_def)
+ have "p (a \<cdot> x) = \<parallel>f\<parallel>\<hyphen>F * \<parallel>a \<cdot> x\<parallel>" by (simp only: p_def)
+ also from x have "\<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>" by (rule abs_homogenous)
+ also have "\<parallel>f\<parallel>\<hyphen>F * (\<bar>a\<bar> * \<parallel>x\<parallel>) = \<bar>a\<bar> * (\<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>)" by simp
+ also have "\<dots> = \<bar>a\<bar> * p x" by (simp only: p_def)
finally show ?thesis .
qed
@@ -381,19 +375,14 @@
show "p (x + y) \<le> p x + p y"
proof -
- have "p (x + y) = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x + y\<parallel>"
- by (simp only: p_def)
+ have "p (x + y) = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x + y\<parallel>" by (simp only: p_def)
also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>F * (\<parallel>x\<parallel> + \<parallel>y\<parallel>)"
proof (rule real_mult_le_le_mono1a)
- show "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
- apply (unfold function_norm_def B_def)
- using normed_vectorspace.axioms [OF F_norm] .. (* FIXME *)
+ show "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
from x y show "\<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>" ..
qed
- also have "\<dots> = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel> + \<parallel>f\<parallel>\<hyphen>F * \<parallel>y\<parallel>"
- by (simp only: real_add_mult_distrib2)
- also have "\<dots> = p x + p y"
- by (simp only: p_def)
+ also have "\<dots> = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel> + \<parallel>f\<parallel>\<hyphen>F * \<parallel>y\<parallel>" by (simp only: real_add_mult_distrib2)
+ also have "\<dots> = p x + p y" by (simp only: p_def)
finally show ?thesis .
qed
qed
@@ -404,8 +393,8 @@
proof
fix x assume "x \<in> F"
show "\<bar>f x\<bar> \<le> p x"
- apply (unfold p_def function_norm_def B_def)
- using normed_vectorspace.axioms [OF F_norm] .. (* FIXME *)
+ by (unfold p_def) (rule normed_vectorspace.fn_norm_le_cong
+ [OF F_norm, folded B_def fn_norm_def])
qed
txt {* Using the fact that @{text p} is a seminorm and @{text f} is bounded
@@ -454,45 +443,32 @@
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
show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"
- apply (unfold function_norm_def B_def)
- apply rule
- apply (rule normed_vectorspace.axioms [OF E_norm])+
- apply (rule continuous.axioms [OF g_cont])+
- apply (rule b [unfolded p_def function_norm_def B_def])
- using normed_vectorspace.axioms [OF F_norm] .. (* FIXME *)
+ by (rule fn_norm_least [of g, folded B_def fn_norm_def])
txt {* The other direction is achieved by a similar argument. *}
- have ** : "\<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"
- from a have "g x = f x" ..
- hence "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
- also have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
- apply (unfold function_norm_def B_def)
- apply rule
- apply (rule normed_vectorspace.axioms [OF E_norm])+
- apply (rule continuous.axioms [OF g_cont])+
- proof -
- from FE x show "x \<in> E" ..
+ show "\<parallel>f\<parallel>\<hyphen>F \<le> \<parallel>g\<parallel>\<hyphen>E"
+ proof (rule normed_vectorspace.fn_norm_least [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"
+ 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]
+ 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" ..
+ qed
+ finally show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" .
qed
- finally show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" .
+ show "0 \<le> \<parallel>g\<parallel>\<hyphen>E"
+ using continuous.axioms [OF g_cont]
+ by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
qed
- show "\<parallel>f\<parallel>\<hyphen>F \<le> \<parallel>g\<parallel>\<hyphen>E"
- apply (unfold function_norm_def B_def)
- apply rule
- apply (rule normed_vectorspace.axioms [OF F_norm])+
- apply assumption+
- apply (rule ** [unfolded function_norm_def B_def])
- apply rule
- apply assumption+
- apply (rule continuous.axioms [OF g_cont])+
- done (* FIXME *)
qed
-
- with linearformE a g_cont show ?thesis
- by blast
+ with linearformE a g_cont show ?thesis by blast
qed
end
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Thu Aug 29 11:15:36 2002 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy Thu Aug 29 16:08:30 2002 +0200
@@ -190,8 +190,7 @@
SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
and H'_def: "H' \<equiv> H + lin x0"
and x0: "x0 \<notin> H" "x0 \<in> E" "x0 \<noteq> 0"
- includes vectorspace E + subvectorspace H E +
- seminorm E p + linearform H h
+ includes vectorspace E + subspace H E + seminorm E p + linearform H h
assumes a: "\<forall>y \<in> H. h y \<le> p y"
and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y"
shows "\<forall>x \<in> H'. h' x \<le> p x"
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Thu Aug 29 11:15:36 2002 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy Thu Aug 29 16:08:30 2002 +0200
@@ -322,7 +322,7 @@
proof
show "H \<noteq> {}"
proof -
- from FE E have "0 \<in> F" by (rule subvectorspace.zero)
+ from FE E have "0 \<in> F" by (rule subspace.zero)
also from graph M cM ex FE have "F \<unlhd> H" by (rule sup_supF)
then have "F \<subseteq> H" ..
finally show ?thesis by blast
@@ -397,10 +397,10 @@
*}
lemma abs_ineq_iff:
- includes subvectorspace H E + seminorm E p + linearform H h
+ includes subspace H E + vectorspace E + seminorm E p + linearform H h
shows "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" (is "?L = ?R")
proof
- have h: "vectorspace H" by (rule vectorspace)
+ have H: "vectorspace H" ..
{
assume l: ?L
show ?R
@@ -420,12 +420,13 @@
show "- p x \<le> h x"
proof (rule real_minus_le)
have "linearform H h" .
- from h this x have "- h x = h (- x)"
- by (rule vectorspace_linearform.neg [symmetric])
- also from r x have "\<dots> \<le> p (- x)" by simp
+ from this H x have "- h x = h (- x)" by (rule linearform.neg [symmetric])
+ also
+ from H x have "- x \<in> H" by (rule vectorspace.neg_closed)
+ with r have "h (- x) \<le> p (- x)" ..
also have "\<dots> = p x"
- proof (rule seminorm_vectorspace.minus)
- show "x \<in> E" ..
+ proof (rule seminorm.minus)
+ from x show "x \<in> E" ..
qed
finally show "- h x \<le> p x" .
qed
--- a/src/HOL/Real/HahnBanach/Linearform.thy Thu Aug 29 11:15:36 2002 +0200
+++ b/src/HOL/Real/HahnBanach/Linearform.thy Thu Aug 29 16:08:30 2002 +0200
@@ -16,11 +16,9 @@
assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x"
-locale (open) vectorspace_linearform =
- vectorspace + linearform
-
-lemma (in vectorspace_linearform) neg [iff]:
- "x \<in> V \<Longrightarrow> f (- x) = - f x"
+lemma (in linearform) neg [iff]:
+ includes vectorspace
+ shows "x \<in> V \<Longrightarrow> f (- x) = - f x"
proof -
assume x: "x \<in> V"
hence "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
@@ -29,21 +27,22 @@
finally show ?thesis .
qed
-lemma (in vectorspace_linearform) diff [iff]:
- "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y"
+lemma (in linearform) diff [iff]:
+ includes vectorspace
+ shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y"
proof -
assume x: "x \<in> V" and y: "y \<in> V"
hence "x - y = x + - y" by (rule diff_eq1)
- also have "f ... = f x + f (- y)"
- by (rule add) (simp_all add: x y)
- also from y have "f (- y) = - f y" by (rule neg)
+ also have "f ... = f x + f (- y)" by (rule add) (simp_all add: x y)
+ also from _ y have "f (- y) = - f y" by (rule neg)
finally show ?thesis by simp
qed
text {* Every linear form yields @{text 0} for the @{text 0} vector. *}
-lemma (in vectorspace_linearform) linearform_zero [iff]:
- "f 0 = 0"
+lemma (in linearform) zero [iff]:
+ includes vectorspace
+ shows "f 0 = 0"
proof -
have "f 0 = f (0 - 0)" by simp
also have "\<dots> = f 0 - f 0" by (rule diff) simp_all
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy Thu Aug 29 11:15:36 2002 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy Thu Aug 29 16:08:30 2002 +0200
@@ -23,11 +23,9 @@
and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
-locale (open) seminorm_vectorspace =
- seminorm + vectorspace
-
-lemma (in seminorm_vectorspace) diff_subadditive:
- "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
+lemma (in seminorm) diff_subadditive:
+ includes vectorspace
+ shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
proof -
assume x: "x \<in> V" and y: "y \<in> V"
hence "x - y = x + - 1 \<cdot> y"
@@ -40,8 +38,9 @@
finally show ?thesis .
qed
-lemma (in seminorm_vectorspace) minus:
- "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
+lemma (in seminorm) minus:
+ includes vectorspace
+ shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
proof -
assume x: "x \<in> V"
hence "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
@@ -70,7 +69,7 @@
space}.
*}
-locale normed_vectorspace = vectorspace + seminorm_vectorspace + norm
+locale normed_vectorspace = vectorspace + norm
lemma (in normed_vectorspace) gt_zero [intro?]:
"x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> 0 < \<parallel>x\<parallel>"
@@ -91,7 +90,7 @@
*}
lemma subspace_normed_vs [intro?]:
- includes subvectorspace F E + normed_vectorspace E
+ includes subspace F E + normed_vectorspace E
shows "normed_vectorspace F norm"
proof
show "vectorspace F" by (rule vectorspace)
--- a/src/HOL/Real/HahnBanach/Subspace.thy Thu Aug 29 11:15:36 2002 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy Thu Aug 29 16:08:30 2002 +0200
@@ -37,12 +37,9 @@
lemma rev_subspaceD [elim?]: "x \<in> U \<Longrightarrow> U \<unlhd> V \<Longrightarrow> x \<in> V"
by (rule subspace.subsetD)
-
-locale (open) subvectorspace =
- subspace + vectorspace
-
-lemma (in subvectorspace) diff_closed [iff]:
- "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x - y \<in> U"
+lemma (in subspace) diff_closed [iff]:
+ includes vectorspace
+ shows "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x - y \<in> U"
by (simp add: diff_eq1 negate_eq1)
@@ -52,7 +49,9 @@
carrier set and by vector space laws.
*}
-lemma (in subvectorspace) zero [intro]: "0 \<in> U"
+lemma (in subspace) zero [intro]:
+ includes vectorspace
+ shows "0 \<in> U"
proof -
have "U \<noteq> {}" by (rule U_V.non_empty)
then obtain x where x: "x \<in> U" by blast
@@ -61,14 +60,17 @@
finally show ?thesis .
qed
-lemma (in subvectorspace) neg_closed [iff]: "x \<in> U \<Longrightarrow> - x \<in> U"
+lemma (in subspace) neg_closed [iff]:
+ includes vectorspace
+ shows "x \<in> U \<Longrightarrow> - x \<in> U"
by (simp add: negate_eq1)
text {* \medskip Further derived laws: every subspace is a vector space. *}
-lemma (in subvectorspace) vectorspace [iff]:
- "vectorspace U"
+lemma (in subspace) vectorspace [iff]:
+ includes vectorspace
+ shows "vectorspace U"
proof
show "U \<noteq> {}" ..
fix x y z assume x: "x \<in> U" and y: "y \<in> U" and z: "z \<in> U"
@@ -195,7 +197,7 @@
lemma (in vectorspace) lin_vectorspace [intro]:
"x \<in> V \<Longrightarrow> vectorspace (lin x)"
- by (rule subvectorspace.vectorspace) (rule lin_subspace)
+ by (rule subspace.vectorspace) (rule lin_subspace)
subsection {* Sum of two vectorspaces *}
@@ -244,7 +246,7 @@
text {* The sum of two subspaces is again a subspace. *}
lemma sum_subspace [intro?]:
- includes subvectorspace U E + subvectorspace V E
+ includes subspace U E + vectorspace E + subspace V E
shows "U + V \<unlhd> E"
proof
have "0 \<in> U + V"
@@ -289,7 +291,7 @@
lemma sum_vs [intro?]:
"U \<unlhd> E \<Longrightarrow> V \<unlhd> E \<Longrightarrow> vectorspace E \<Longrightarrow> vectorspace (U + V)"
- by (rule subvectorspace.vectorspace) (rule sum_subspace)
+ by (rule subspace.vectorspace) (rule sum_subspace)
subsection {* Direct sums *}
@@ -310,8 +312,8 @@
and sum: "u1 + v1 = u2 + v2"
shows "u1 = u2 \<and> v1 = v2"
proof
- have U: "vectorspace U" by (rule subvectorspace.vectorspace)
- have V: "vectorspace V" by (rule subvectorspace.vectorspace)
+ have U: "vectorspace U" by (rule subspace.vectorspace)
+ have V: "vectorspace V" by (rule subspace.vectorspace)
from u1 u2 v1 v2 and sum have eq: "u1 - u2 = v2 - v1"
by (simp add: add_diff_swap)
from u1 u2 have u: "u1 - u2 \<in> U"
@@ -345,7 +347,7 @@
*}
lemma decomp_H':
- includes vectorspace E + subvectorspace H E
+ includes vectorspace E + subspace H E
assumes y1: "y1 \<in> H" and y2: "y2 \<in> H"
and x': "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0"
and eq: "y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'"
@@ -397,7 +399,7 @@
*}
lemma decomp_H'_H:
- includes vectorspace E + subvectorspace H E
+ includes vectorspace E + subspace H E
assumes t: "t \<in> H"
and x': "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0"
shows "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
@@ -424,7 +426,7 @@
"h' \<equiv> (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)
in (h y) + a * xi)"
and x: "x = y + a \<cdot> x'"
- includes vectorspace E + subvectorspace H E
+ includes vectorspace E + subspace H E
assumes y: "y \<in> H"
and x': "x' \<notin> H" "x' \<in> E" "x' \<noteq> 0"
shows "h' x = h y + a * xi"