src/HOL/Real/HahnBanach/NormedSpace.thy
 changeset 27611 2c01c0bdb385 parent 25762 c03e9d04b3e4 child 27612 d3eb431db035
```     1.1 --- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Tue Jul 15 16:02:10 2008 +0200
1.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Tue Jul 15 16:50:09 2008 +0200
1.3 @@ -27,9 +27,10 @@
1.4  declare seminorm.intro [intro?]
1.5
1.7 -  includes vectorspace
1.8 +  assumes "vectorspace V"
1.9    shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
1.10  proof -
1.11 +  interpret vectorspace [V] by fact
1.12    assume x: "x \<in> V" and y: "y \<in> V"
1.13    hence "x - y = x + - 1 \<cdot> y"
1.14      by (simp add: diff_eq2 negate_eq2a)
1.15 @@ -42,9 +43,10 @@
1.16  qed
1.17
1.18  lemma (in seminorm) minus:
1.19 -  includes vectorspace
1.20 +  assumes "vectorspace V"
1.21    shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
1.22  proof -
1.23 +  interpret vectorspace [V] by fact
1.24    assume x: "x \<in> V"
1.25    hence "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
1.26    also from x have "\<parallel>\<dots>\<parallel> = \<bar>- 1\<bar> * \<parallel>x\<parallel>"
1.27 @@ -95,14 +97,19 @@
1.28  *}
1.29
1.30  lemma subspace_normed_vs [intro?]:
1.31 -  includes subspace F E + normed_vectorspace E
1.32 +  fixes F E norm
1.33 +  assumes "subspace F E" "normed_vectorspace E norm"
1.34    shows "normed_vectorspace F norm"
1.35 -proof
1.36 -  show "vectorspace F" by (rule vectorspace) unfold_locales
1.37 -next
1.38 -  have "NormedSpace.norm E norm" by unfold_locales
1.39 -  with subset show "NormedSpace.norm F norm"
1.40 -    by (simp add: norm_def seminorm_def norm_axioms_def)
1.41 +proof -
1.42 +  interpret subspace [F E] by fact
1.43 +  interpret normed_vectorspace [E norm] by fact
1.44 +  show ?thesis proof
1.45 +    show "vectorspace F" by (rule vectorspace) unfold_locales
1.46 +  next
1.47 +    have "NormedSpace.norm E norm" by unfold_locales
1.48 +    with subset show "NormedSpace.norm F norm"
1.49 +      by (simp add: norm_def seminorm_def norm_axioms_def)
1.50 +  qed
1.51  qed
1.52
1.53  end
```