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.6  lemma (in seminorm) diff_subadditive:
     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