tuned;
authorwenzelm
Thu Aug 29 16:08:30 2002 +0200 (2002-08-29)
changeset 13547bf399f3bd7dc
parent 13546 f76237c2be75
child 13548 36cb5fb8188c
tuned;
src/HOL/Real/HahnBanach/FunctionNorm.thy
src/HOL/Real/HahnBanach/HahnBanach.thy
src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
src/HOL/Real/HahnBanach/Linearform.thy
src/HOL/Real/HahnBanach/NormedSpace.thy
src/HOL/Real/HahnBanach/Subspace.thy
     1.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Thu Aug 29 11:15:36 2002 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Thu Aug 29 16:08:30 2002 +0200
     1.3 @@ -53,9 +53,9 @@
     1.4    empty set. Since @{text \<real>} is unbounded, there would be no supremum.
     1.5    To avoid this situation it must be guaranteed that there is an
     1.6    element in this set. This element must be @{text "{} \<ge> 0"} so that
     1.7 -  @{text function_norm} has the norm properties. Furthermore
     1.8 -  it does not have to change the norm in all other cases, so it must
     1.9 -  be @{text 0}, as all other elements are @{text "{} \<ge> 0"}.
    1.10 +  @{text fn_norm} has the norm properties. Furthermore it does not
    1.11 +  have to change the norm in all other cases, so it must be @{text 0},
    1.12 +  as all other elements are @{text "{} \<ge> 0"}.
    1.13  
    1.14    Thus we define the set @{text B} where the supremum is taken from as
    1.15    follows:
    1.16 @@ -63,31 +63,25 @@
    1.17    @{text "{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}"}
    1.18    \end{center}
    1.19  
    1.20 -  @{text function_norm} is equal to the supremum of @{text B}, if the
    1.21 +  @{text fn_norm} is equal to the supremum of @{text B}, if the
    1.22    supremum exists (otherwise it is undefined).
    1.23  *}
    1.24  
    1.25 -locale function_norm = norm_syntax +
    1.26 -  fixes B
    1.27 -  defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
    1.28 -  fixes function_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
    1.29 +locale fn_norm = norm_syntax +
    1.30 +  fixes B defines "B V f \<equiv> {0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel> | x. x \<noteq> 0 \<and> x \<in> V}"
    1.31 +  fixes fn_norm ("\<parallel>_\<parallel>\<hyphen>_" [0, 1000] 999)
    1.32    defines "\<parallel>f\<parallel>\<hyphen>V \<equiv> \<Squnion>(B V f)"
    1.33  
    1.34 -lemma (in function_norm) B_not_empty [intro]: "0 \<in> B V f"
    1.35 -  by (unfold B_def) simp
    1.36 -
    1.37 -locale (open) functional_vectorspace =
    1.38 -    normed_vectorspace + function_norm +
    1.39 -  fixes cont
    1.40 -  defines "cont f \<equiv> continuous V norm f"
    1.41 +lemma (in fn_norm) B_not_empty [intro]: "0 \<in> B V f"
    1.42 +  by (simp add: B_def)
    1.43  
    1.44  text {*
    1.45    The following lemma states that every continuous linear form on a
    1.46    normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.
    1.47  *}
    1.48  
    1.49 -lemma (in functional_vectorspace) function_norm_works:
    1.50 -  includes continuous
    1.51 +lemma (in normed_vectorspace) fn_norm_works:   (* FIXME bug with "(in fn_norm)" !? *)
    1.52 +  includes fn_norm + continuous
    1.53    shows "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
    1.54  proof -
    1.55    txt {* The existence of the supremum is shown using the
    1.56 @@ -148,38 +142,40 @@
    1.57        thus ?thesis ..
    1.58      qed
    1.59    qed
    1.60 -  then show ?thesis
    1.61 -    by (unfold function_norm_def) (rule the_lubI_ex)
    1.62 +  then show ?thesis by (unfold fn_norm_def) (rule the_lubI_ex)
    1.63  qed
    1.64  
    1.65 -lemma (in functional_vectorspace) function_norm_ub [intro?]:
    1.66 -  includes continuous
    1.67 +lemma (in normed_vectorspace) fn_norm_ub [iff?]:
    1.68 +  includes fn_norm + continuous
    1.69    assumes b: "b \<in> B V f"
    1.70    shows "b \<le> \<parallel>f\<parallel>\<hyphen>V"
    1.71  proof -
    1.72 -  have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" by (rule function_norm_works)
    1.73 +  have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
    1.74 +    by (unfold B_def fn_norm_def) (rule fn_norm_works)
    1.75    from this and b show ?thesis ..
    1.76  qed
    1.77  
    1.78 -lemma (in functional_vectorspace) function_norm_least' [intro?]:
    1.79 -  includes continuous
    1.80 +lemma (in normed_vectorspace) fn_norm_leastB:
    1.81 +  includes fn_norm + continuous
    1.82    assumes b: "\<And>b. b \<in> B V f \<Longrightarrow> b \<le> y"
    1.83    shows "\<parallel>f\<parallel>\<hyphen>V \<le> y"
    1.84  proof -
    1.85 -  have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" by (rule function_norm_works)
    1.86 +  have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
    1.87 +    by (unfold B_def fn_norm_def) (rule fn_norm_works)
    1.88    from this and b show ?thesis ..
    1.89  qed
    1.90  
    1.91  text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
    1.92  
    1.93 -lemma (in functional_vectorspace) function_norm_ge_zero [iff]:
    1.94 -  includes continuous
    1.95 +lemma (in normed_vectorspace) fn_norm_ge_zero [iff]:
    1.96 +  includes fn_norm + continuous
    1.97    shows "0 \<le> \<parallel>f\<parallel>\<hyphen>V"
    1.98  proof -
    1.99    txt {* The function norm is defined as the supremum of @{text B}.
   1.100      So it is @{text "\<ge> 0"} if all elements in @{text B} are @{text "\<ge>
   1.101      0"}, provided the supremum exists and @{text B} is not empty. *}
   1.102 -  have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)" by (rule function_norm_works)
   1.103 +  have "lub (B V f) (\<parallel>f\<parallel>\<hyphen>V)"
   1.104 +    by (unfold B_def fn_norm_def) (rule fn_norm_works)
   1.105    moreover have "0 \<in> B V f" ..
   1.106    ultimately show ?thesis ..
   1.107  qed
   1.108 @@ -191,8 +187,8 @@
   1.109    \end{center}
   1.110  *}
   1.111  
   1.112 -lemma (in functional_vectorspace) function_norm_le_cong:
   1.113 -  includes continuous + vectorspace_linearform
   1.114 +lemma (in normed_vectorspace) fn_norm_le_cong:
   1.115 +  includes fn_norm + continuous + linearform
   1.116    assumes x: "x \<in> V"
   1.117    shows "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
   1.118  proof cases
   1.119 @@ -202,7 +198,7 @@
   1.120    also have "\<bar>\<dots>\<bar> = 0" by simp
   1.121    also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
   1.122    proof (rule real_le_mult_order1a)
   1.123 -    show "0 \<le> \<parallel>f\<parallel>\<hyphen>V" ..
   1.124 +    show "0 \<le> \<parallel>f\<parallel>\<hyphen>V" by (unfold B_def fn_norm_def) rule
   1.125      show "0 \<le> norm x" ..
   1.126    qed
   1.127    finally show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>" .
   1.128 @@ -213,11 +209,10 @@
   1.129    also have "\<dots> \<le>  \<parallel>f\<parallel>\<hyphen>V * \<parallel>x\<parallel>"
   1.130    proof (rule real_mult_le_le_mono2)
   1.131      from x show "0 \<le> \<parallel>x\<parallel>" ..
   1.132 -    show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
   1.133 -    proof
   1.134 -      from x and neq show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
   1.135 -        by (auto simp add: B_def real_divide_def)
   1.136 -    qed
   1.137 +    from x and neq have "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<in> B V f"
   1.138 +      by (auto simp add: B_def real_divide_def)
   1.139 +    then show "\<bar>f x\<bar> * inverse \<parallel>x\<parallel> \<le> \<parallel>f\<parallel>\<hyphen>V"
   1.140 +      by (unfold B_def fn_norm_def) (rule fn_norm_ub)
   1.141    qed
   1.142    finally show ?thesis .
   1.143  qed
   1.144 @@ -230,11 +225,11 @@
   1.145    \end{center}
   1.146  *}
   1.147  
   1.148 -lemma (in functional_vectorspace) function_norm_least [intro?]:
   1.149 -  includes continuous
   1.150 +lemma (in normed_vectorspace) fn_norm_least [intro?]:
   1.151 +  includes fn_norm + continuous
   1.152    assumes ineq: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" and ge: "0 \<le> c"
   1.153    shows "\<parallel>f\<parallel>\<hyphen>V \<le> c"
   1.154 -proof (rule function_norm_least')
   1.155 +proof (rule fn_norm_leastB [folded B_def fn_norm_def])
   1.156    fix b assume b: "b \<in> B V f"
   1.157    show "b \<le> c"
   1.158    proof cases
   1.159 @@ -261,9 +256,4 @@
   1.160    qed
   1.161  qed
   1.162  
   1.163 -lemmas [iff?] =
   1.164 -  functional_vectorspace.function_norm_ge_zero
   1.165 -  functional_vectorspace.function_norm_le_cong
   1.166 -  functional_vectorspace.function_norm_least
   1.167 -
   1.168  end
     2.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Aug 29 11:15:36 2002 +0200
     2.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Thu Aug 29 16:08:30 2002 +0200
     2.3 @@ -53,8 +53,7 @@
     2.4  *}
     2.5  
     2.6  theorem HahnBanach:
     2.7 -  includes vectorspace E + subvectorspace F E +
     2.8 -    seminorm_vectorspace E p + linearform F f
     2.9 +  includes vectorspace E + subspace F E + seminorm E p + linearform F f
    2.10    assumes fp: "\<forall>x \<in> F. f x \<le> p x"
    2.11    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)"
    2.12      -- {* Let @{text E} be a vector space, @{text F} a subspace of @{text E}, @{text p} a seminorm on @{text E}, *}
    2.13 @@ -63,6 +62,7 @@
    2.14  proof -
    2.15    def M \<equiv> "norm_pres_extensions E p F f"
    2.16    hence M: "M = \<dots>" by (simp only:)
    2.17 +  have E: "vectorspace E" .
    2.18    have F: "vectorspace F" ..
    2.19    {
    2.20      fix c assume cM: "c \<in> chain M" and ex: "\<exists>x. x \<in> c"
    2.21 @@ -121,7 +121,7 @@
    2.22        -- {* @{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E}, *}
    2.23        -- {* and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \skp *}
    2.24    from HE have H: "vectorspace H"
    2.25 -    by (rule subvectorspace.vectorspace)
    2.26 +    by (rule subspace.vectorspace)
    2.27  
    2.28    have HE_eq: "H = E"
    2.29      -- {* We show that @{text h} is defined on whole @{text E} by classical contradiction. \skp *}
    2.30 @@ -164,7 +164,7 @@
    2.31            fix u v assume u: "u \<in> H" and v: "v \<in> H"
    2.32            with HE have uE: "u \<in> E" and vE: "v \<in> E" by auto
    2.33            from H u v linearform have "h v - h u = h (v - u)"
    2.34 -            by (simp add: vectorspace_linearform.diff)
    2.35 +            by (simp add: linearform.diff)
    2.36            also from hp and H u v have "\<dots> \<le> p (v - u)"
    2.37              by (simp only: vectorspace.diff_closed)
    2.38            also from x'E uE vE have "v - u = x' + - x' + v + - u"
    2.39 @@ -173,11 +173,10 @@
    2.40              by (simp add: add_ac)
    2.41            also from x'E uE vE have "\<dots> = (v + x') - (u + x')"
    2.42              by (simp add: diff_eq1)
    2.43 -          also from x'E uE vE have "p \<dots> \<le> p (v + x') + p (u + x')"
    2.44 +          also from x'E uE vE E have "p \<dots> \<le> p (v + x') + p (u + x')"
    2.45              by (simp add: diff_subadditive)
    2.46            finally have "h v - h u \<le> p (v + x') + p (u + x')" .
    2.47 -          then show "- p (u + x') - h u \<le> p (v + x') - h v"
    2.48 -            by simp
    2.49 +          then show "- p (u + x') - h u \<le> p (v + x') - h v" by simp
    2.50          qed
    2.51          then show ?thesis ..
    2.52        qed
    2.53 @@ -298,8 +297,7 @@
    2.54  *}
    2.55  
    2.56  theorem abs_HahnBanach:
    2.57 -  includes vectorspace E + subvectorspace F E +
    2.58 -    linearform F f + seminorm_vectorspace E p
    2.59 +  includes vectorspace E + subspace F E + linearform F f + seminorm E p
    2.60    assumes fp: "\<forall>x \<in> F. \<bar>f x\<bar> \<le> p x"
    2.61    shows "\<exists>g. linearform E g
    2.62      \<and> (\<forall>x \<in> F. g x = f x)
    2.63 @@ -330,8 +328,7 @@
    2.64  *}
    2.65  
    2.66  theorem norm_HahnBanach:
    2.67 -  includes functional_vectorspace E + subvectorspace F E +
    2.68 -    linearform F f + continuous F norm f
    2.69 +  includes normed_vectorspace E + subspace F E + linearform F f + fn_norm + continuous F norm f
    2.70    shows "\<exists>g. linearform E g
    2.71       \<and> continuous E norm g
    2.72       \<and> (\<forall>x \<in> F. g x = f x)
    2.73 @@ -343,6 +340,9 @@
    2.74    have F: "vectorspace F" ..
    2.75    have linearform: "linearform F f" .
    2.76    have F_norm: "normed_vectorspace F norm" ..
    2.77 +  have ge_zero: "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
    2.78 +    by (rule normed_vectorspace.fn_norm_ge_zero
    2.79 +      [OF F_norm, folded B_def fn_norm_def])
    2.80  
    2.81    txt {* We define a function @{text p} on @{text E} as follows:
    2.82      @{text "p x = \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"} *}
    2.83 @@ -356,9 +356,7 @@
    2.84      txt {* @{text p} is positive definite: *}
    2.85      show "0 \<le> p x"
    2.86      proof (unfold p_def, rule real_le_mult_order1a)
    2.87 -      show "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
    2.88 -        apply (unfold function_norm_def B_def)
    2.89 -        using normed_vectorspace.axioms [OF F_norm] ..
    2.90 +      show "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
    2.91        from x show "0 \<le> \<parallel>x\<parallel>" ..
    2.92      qed
    2.93  
    2.94 @@ -366,14 +364,10 @@
    2.95  
    2.96      show "p (a \<cdot> x) = \<bar>a\<bar> * p x"
    2.97      proof -
    2.98 -      have "p (a \<cdot> x) = \<parallel>f\<parallel>\<hyphen>F * \<parallel>a \<cdot> x\<parallel>"
    2.99 -        by (simp only: p_def)
   2.100 -      also from x have "\<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
   2.101 -        by (rule abs_homogenous)
   2.102 -      also have "\<parallel>f\<parallel>\<hyphen>F * (\<bar>a\<bar> * \<parallel>x\<parallel>) = \<bar>a\<bar> * (\<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>)"
   2.103 -        by simp
   2.104 -      also have "\<dots> = \<bar>a\<bar> * p x"
   2.105 -        by (simp only: p_def)
   2.106 +      have "p (a \<cdot> x) = \<parallel>f\<parallel>\<hyphen>F * \<parallel>a \<cdot> x\<parallel>" by (simp only: p_def)
   2.107 +      also from x have "\<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>" by (rule abs_homogenous)
   2.108 +      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
   2.109 +      also have "\<dots> = \<bar>a\<bar> * p x" by (simp only: p_def)
   2.110        finally show ?thesis .
   2.111      qed
   2.112  
   2.113 @@ -381,19 +375,14 @@
   2.114  
   2.115      show "p (x + y) \<le> p x + p y"
   2.116      proof -
   2.117 -      have "p (x + y) = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x + y\<parallel>"
   2.118 -        by (simp only: p_def)
   2.119 +      have "p (x + y) = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x + y\<parallel>" by (simp only: p_def)
   2.120        also have "\<dots> \<le> \<parallel>f\<parallel>\<hyphen>F * (\<parallel>x\<parallel> + \<parallel>y\<parallel>)"
   2.121        proof (rule real_mult_le_le_mono1a)
   2.122 -        show "0 \<le> \<parallel>f\<parallel>\<hyphen>F"
   2.123 -          apply (unfold function_norm_def B_def)
   2.124 -          using normed_vectorspace.axioms [OF F_norm] ..  (* FIXME *)
   2.125 +        show "0 \<le> \<parallel>f\<parallel>\<hyphen>F" by (rule ge_zero)
   2.126          from x y show "\<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>" ..
   2.127        qed
   2.128 -      also have "\<dots> = \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel> + \<parallel>f\<parallel>\<hyphen>F * \<parallel>y\<parallel>"
   2.129 -        by (simp only: real_add_mult_distrib2)
   2.130 -      also have "\<dots> = p x + p y"
   2.131 -        by (simp only: p_def)
   2.132 +      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)
   2.133 +      also have "\<dots> = p x + p y" by (simp only: p_def)
   2.134        finally show ?thesis .
   2.135      qed
   2.136    qed
   2.137 @@ -404,8 +393,8 @@
   2.138    proof
   2.139      fix x assume "x \<in> F"
   2.140      show "\<bar>f x\<bar> \<le> p x"
   2.141 -      apply (unfold p_def function_norm_def B_def)
   2.142 -      using normed_vectorspace.axioms [OF F_norm] .. (* FIXME *)
   2.143 +      by (unfold p_def) (rule normed_vectorspace.fn_norm_le_cong
   2.144 +        [OF F_norm, folded B_def fn_norm_def])
   2.145    qed
   2.146  
   2.147    txt {* Using the fact that @{text p} is a seminorm and @{text f} is bounded
   2.148 @@ -454,45 +443,32 @@
   2.149        with b show "\<bar>g x\<bar> \<le> \<parallel>f\<parallel>\<hyphen>F * \<parallel>x\<parallel>"
   2.150          by (simp only: p_def)
   2.151      qed
   2.152 +    from continuous.axioms [OF g_cont] this ge_zero
   2.153      show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"
   2.154 -      apply (unfold function_norm_def B_def)
   2.155 -      apply rule
   2.156 -      apply (rule normed_vectorspace.axioms [OF E_norm])+
   2.157 -      apply (rule continuous.axioms [OF g_cont])+
   2.158 -      apply (rule b [unfolded p_def function_norm_def B_def])
   2.159 -      using normed_vectorspace.axioms [OF F_norm] ..  (* FIXME *)
   2.160 +      by (rule fn_norm_least [of g, folded B_def fn_norm_def])
   2.161  
   2.162      txt {* The other direction is achieved by a similar argument. *}
   2.163  
   2.164 -    have ** : "\<forall>x \<in> F. \<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
   2.165 -    proof
   2.166 -      fix x assume x: "x \<in> F"
   2.167 -      from a have "g x = f x" ..
   2.168 -      hence "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
   2.169 -      also have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
   2.170 -        apply (unfold function_norm_def B_def)
   2.171 -        apply rule
   2.172 -        apply (rule normed_vectorspace.axioms [OF E_norm])+
   2.173 -        apply (rule continuous.axioms [OF g_cont])+
   2.174 -      proof -
   2.175 -        from FE x show "x \<in> E" ..
   2.176 +    show "\<parallel>f\<parallel>\<hyphen>F \<le> \<parallel>g\<parallel>\<hyphen>E"
   2.177 +    proof (rule normed_vectorspace.fn_norm_least [OF F_norm, folded B_def fn_norm_def])
   2.178 +      show "\<forall>x \<in> F. \<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
   2.179 +      proof
   2.180 +	fix x assume x: "x \<in> F"
   2.181 +	from a have "g x = f x" ..
   2.182 +	hence "\<bar>f x\<bar> = \<bar>g x\<bar>" by (simp only:)
   2.183 +	also from continuous.axioms [OF g_cont]
   2.184 +	have "\<dots> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>"
   2.185 +	proof (rule fn_norm_le_cong [of g, folded B_def fn_norm_def])
   2.186 +	  from FE x show "x \<in> E" ..
   2.187 +	qed
   2.188 +	finally show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" .
   2.189        qed
   2.190 -      finally show "\<bar>f x\<bar> \<le> \<parallel>g\<parallel>\<hyphen>E * \<parallel>x\<parallel>" .
   2.191 +      show "0 \<le> \<parallel>g\<parallel>\<hyphen>E"
   2.192 +	using continuous.axioms [OF g_cont]
   2.193 +	by (rule fn_norm_ge_zero [of g, folded B_def fn_norm_def])
   2.194      qed
   2.195 -    show "\<parallel>f\<parallel>\<hyphen>F \<le> \<parallel>g\<parallel>\<hyphen>E"
   2.196 -      apply (unfold function_norm_def B_def)
   2.197 -      apply rule
   2.198 -      apply (rule normed_vectorspace.axioms [OF F_norm])+
   2.199 -      apply assumption+
   2.200 -      apply (rule ** [unfolded function_norm_def B_def])
   2.201 -      apply rule
   2.202 -      apply assumption+
   2.203 -      apply (rule continuous.axioms [OF g_cont])+
   2.204 -      done  (* FIXME *)
   2.205    qed
   2.206 -
   2.207 -  with linearformE a g_cont show ?thesis
   2.208 -    by blast
   2.209 +  with linearformE a g_cont show ?thesis by blast
   2.210  qed
   2.211  
   2.212  end
     3.1 --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Aug 29 11:15:36 2002 +0200
     3.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Thu Aug 29 16:08:30 2002 +0200
     3.3 @@ -190,8 +190,7 @@
     3.4        SOME (y, a). x = y + a \<cdot> x0 \<and> y \<in> H in h y + a * xi"
     3.5      and H'_def: "H' \<equiv> H + lin x0"
     3.6      and x0: "x0 \<notin> H"  "x0 \<in> E"  "x0 \<noteq> 0"
     3.7 -  includes vectorspace E + subvectorspace H E +
     3.8 -    seminorm E p + linearform H h
     3.9 +  includes vectorspace E + subspace H E + seminorm E p + linearform H h
    3.10    assumes a: "\<forall>y \<in> H. h y \<le> p y"
    3.11      and a': "\<forall>y \<in> H. - p (y + x0) - h y \<le> xi \<and> xi \<le> p (y + x0) - h y"
    3.12    shows "\<forall>x \<in> H'. h' x \<le> p x"
     4.1 --- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Thu Aug 29 11:15:36 2002 +0200
     4.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Thu Aug 29 16:08:30 2002 +0200
     4.3 @@ -322,7 +322,7 @@
     4.4  proof
     4.5    show "H \<noteq> {}"
     4.6    proof -
     4.7 -    from FE E have "0 \<in> F" by (rule subvectorspace.zero)
     4.8 +    from FE E have "0 \<in> F" by (rule subspace.zero)
     4.9      also from graph M cM ex FE have "F \<unlhd> H" by (rule sup_supF)
    4.10      then have "F \<subseteq> H" ..
    4.11      finally show ?thesis by blast
    4.12 @@ -397,10 +397,10 @@
    4.13  *}
    4.14  
    4.15  lemma abs_ineq_iff:
    4.16 -  includes subvectorspace H E + seminorm E p + linearform H h
    4.17 +  includes subspace H E + vectorspace E + seminorm E p + linearform H h
    4.18    shows "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" (is "?L = ?R")
    4.19  proof
    4.20 -  have h: "vectorspace H" by (rule vectorspace)
    4.21 +  have H: "vectorspace H" ..
    4.22    {
    4.23      assume l: ?L
    4.24      show ?R
    4.25 @@ -420,12 +420,13 @@
    4.26        show "- p x \<le> h x"
    4.27        proof (rule real_minus_le)
    4.28          have "linearform H h" .
    4.29 -        from h this x have "- h x = h (- x)"
    4.30 -          by (rule vectorspace_linearform.neg [symmetric])
    4.31 -        also from r x have "\<dots> \<le> p (- x)" by simp
    4.32 +        from this H x have "- h x = h (- x)" by (rule linearform.neg [symmetric])
    4.33 +        also
    4.34 +	from H x have "- x \<in> H" by (rule vectorspace.neg_closed)
    4.35 +	with r have "h (- x) \<le> p (- x)" ..
    4.36          also have "\<dots> = p x"
    4.37 -        proof (rule seminorm_vectorspace.minus)
    4.38 -          show "x \<in> E" ..
    4.39 +        proof (rule seminorm.minus)
    4.40 +          from x show "x \<in> E" ..
    4.41          qed
    4.42          finally show "- h x \<le> p x" .
    4.43        qed
     5.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Thu Aug 29 11:15:36 2002 +0200
     5.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Thu Aug 29 16:08:30 2002 +0200
     5.3 @@ -16,11 +16,9 @@
     5.4    assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
     5.5      and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x"
     5.6  
     5.7 -locale (open) vectorspace_linearform =
     5.8 -  vectorspace + linearform
     5.9 -
    5.10 -lemma (in vectorspace_linearform) neg [iff]:
    5.11 -  "x \<in> V \<Longrightarrow> f (- x) = - f x"
    5.12 +lemma (in linearform) neg [iff]:
    5.13 +  includes vectorspace
    5.14 +  shows "x \<in> V \<Longrightarrow> f (- x) = - f x"
    5.15  proof -
    5.16    assume x: "x \<in> V"
    5.17    hence "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
    5.18 @@ -29,21 +27,22 @@
    5.19    finally show ?thesis .
    5.20  qed
    5.21  
    5.22 -lemma (in vectorspace_linearform) diff [iff]:
    5.23 -  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y"
    5.24 +lemma (in linearform) diff [iff]:
    5.25 +  includes vectorspace
    5.26 +  shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y"
    5.27  proof -
    5.28    assume x: "x \<in> V" and y: "y \<in> V"
    5.29    hence "x - y = x + - y" by (rule diff_eq1)
    5.30 -  also have "f ... = f x + f (- y)"
    5.31 -    by (rule add) (simp_all add: x y)
    5.32 -  also from y have "f (- y) = - f y" by (rule neg)
    5.33 +  also have "f ... = f x + f (- y)" by (rule add) (simp_all add: x y)
    5.34 +  also from _ y have "f (- y) = - f y" by (rule neg)
    5.35    finally show ?thesis by simp
    5.36  qed
    5.37  
    5.38  text {* Every linear form yields @{text 0} for the @{text 0} vector. *}
    5.39  
    5.40 -lemma (in vectorspace_linearform) linearform_zero [iff]:
    5.41 -  "f 0 = 0"
    5.42 +lemma (in linearform) zero [iff]:
    5.43 +  includes vectorspace
    5.44 +  shows "f 0 = 0"
    5.45  proof -
    5.46    have "f 0 = f (0 - 0)" by simp
    5.47    also have "\<dots> = f 0 - f 0" by (rule diff) simp_all
     6.1 --- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Thu Aug 29 11:15:36 2002 +0200
     6.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Thu Aug 29 16:08:30 2002 +0200
     6.3 @@ -23,11 +23,9 @@
     6.4      and abs_homogenous [iff?]: "x \<in> V \<Longrightarrow> \<parallel>a \<cdot> x\<parallel> = \<bar>a\<bar> * \<parallel>x\<parallel>"
     6.5      and subadditive [iff?]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x + y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
     6.6  
     6.7 -locale (open) seminorm_vectorspace =
     6.8 -  seminorm + vectorspace
     6.9 -
    6.10 -lemma (in seminorm_vectorspace) diff_subadditive:
    6.11 -  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
    6.12 +lemma (in seminorm) diff_subadditive:
    6.13 +  includes vectorspace
    6.14 +  shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
    6.15  proof -
    6.16    assume x: "x \<in> V" and y: "y \<in> V"
    6.17    hence "x - y = x + - 1 \<cdot> y"
    6.18 @@ -40,8 +38,9 @@
    6.19    finally show ?thesis .
    6.20  qed
    6.21  
    6.22 -lemma (in seminorm_vectorspace) minus:
    6.23 -  "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
    6.24 +lemma (in seminorm) minus:
    6.25 +  includes vectorspace
    6.26 +  shows "x \<in> V \<Longrightarrow> \<parallel>- x\<parallel> = \<parallel>x\<parallel>"
    6.27  proof -
    6.28    assume x: "x \<in> V"
    6.29    hence "- x = - 1 \<cdot> x" by (simp only: negate_eq1)
    6.30 @@ -70,7 +69,7 @@
    6.31    space}.
    6.32  *}
    6.33  
    6.34 -locale normed_vectorspace = vectorspace + seminorm_vectorspace + norm
    6.35 +locale normed_vectorspace = vectorspace + norm
    6.36  
    6.37  lemma (in normed_vectorspace) gt_zero [intro?]:
    6.38    "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> 0 < \<parallel>x\<parallel>"
    6.39 @@ -91,7 +90,7 @@
    6.40  *}
    6.41  
    6.42  lemma subspace_normed_vs [intro?]:
    6.43 -  includes subvectorspace F E + normed_vectorspace E
    6.44 +  includes subspace F E + normed_vectorspace E
    6.45    shows "normed_vectorspace F norm"
    6.46  proof
    6.47    show "vectorspace F" by (rule vectorspace)
     7.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Thu Aug 29 11:15:36 2002 +0200
     7.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Thu Aug 29 16:08:30 2002 +0200
     7.3 @@ -37,12 +37,9 @@
     7.4  lemma rev_subspaceD [elim?]: "x \<in> U \<Longrightarrow> U \<unlhd> V \<Longrightarrow> x \<in> V"
     7.5    by (rule subspace.subsetD)
     7.6  
     7.7 -
     7.8 -locale (open) subvectorspace =
     7.9 -  subspace + vectorspace
    7.10 -
    7.11 -lemma (in subvectorspace) diff_closed [iff]:
    7.12 -    "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x - y \<in> U"
    7.13 +lemma (in subspace) diff_closed [iff]:
    7.14 +  includes vectorspace
    7.15 +  shows "x \<in> U \<Longrightarrow> y \<in> U \<Longrightarrow> x - y \<in> U"
    7.16    by (simp add: diff_eq1 negate_eq1)
    7.17  
    7.18  
    7.19 @@ -52,7 +49,9 @@
    7.20    carrier set and by vector space laws.
    7.21  *}
    7.22  
    7.23 -lemma (in subvectorspace) zero [intro]: "0 \<in> U"
    7.24 +lemma (in subspace) zero [intro]:
    7.25 +  includes vectorspace
    7.26 +  shows "0 \<in> U"
    7.27  proof -
    7.28    have "U \<noteq> {}" by (rule U_V.non_empty)
    7.29    then obtain x where x: "x \<in> U" by blast
    7.30 @@ -61,14 +60,17 @@
    7.31    finally show ?thesis .
    7.32  qed
    7.33  
    7.34 -lemma (in subvectorspace) neg_closed [iff]: "x \<in> U \<Longrightarrow> - x \<in> U"
    7.35 +lemma (in subspace) neg_closed [iff]:
    7.36 +  includes vectorspace
    7.37 +  shows "x \<in> U \<Longrightarrow> - x \<in> U"
    7.38    by (simp add: negate_eq1)
    7.39  
    7.40  
    7.41  text {* \medskip Further derived laws: every subspace is a vector space. *}
    7.42  
    7.43 -lemma (in subvectorspace) vectorspace [iff]:
    7.44 -  "vectorspace U"
    7.45 +lemma (in subspace) vectorspace [iff]:
    7.46 +  includes vectorspace
    7.47 +  shows "vectorspace U"
    7.48  proof
    7.49    show "U \<noteq> {}" ..
    7.50    fix x y z assume x: "x \<in> U" and y: "y \<in> U" and z: "z \<in> U"
    7.51 @@ -195,7 +197,7 @@
    7.52  
    7.53  lemma (in vectorspace) lin_vectorspace [intro]:
    7.54      "x \<in> V \<Longrightarrow> vectorspace (lin x)"
    7.55 -  by (rule subvectorspace.vectorspace) (rule lin_subspace)
    7.56 +  by (rule subspace.vectorspace) (rule lin_subspace)
    7.57  
    7.58  
    7.59  subsection {* Sum of two vectorspaces *}
    7.60 @@ -244,7 +246,7 @@
    7.61  text {* The sum of two subspaces is again a subspace. *}
    7.62  
    7.63  lemma sum_subspace [intro?]:
    7.64 -  includes subvectorspace U E + subvectorspace V E
    7.65 +  includes subspace U E + vectorspace E + subspace V E
    7.66    shows "U + V \<unlhd> E"
    7.67  proof
    7.68    have "0 \<in> U + V"
    7.69 @@ -289,7 +291,7 @@
    7.70  
    7.71  lemma sum_vs [intro?]:
    7.72      "U \<unlhd> E \<Longrightarrow> V \<unlhd> E \<Longrightarrow> vectorspace E \<Longrightarrow> vectorspace (U + V)"
    7.73 -  by (rule subvectorspace.vectorspace) (rule sum_subspace)
    7.74 +  by (rule subspace.vectorspace) (rule sum_subspace)
    7.75  
    7.76  
    7.77  subsection {* Direct sums *}
    7.78 @@ -310,8 +312,8 @@
    7.79      and sum: "u1 + v1 = u2 + v2"
    7.80    shows "u1 = u2 \<and> v1 = v2"
    7.81  proof
    7.82 -  have U: "vectorspace U" by (rule subvectorspace.vectorspace)
    7.83 -  have V: "vectorspace V" by (rule subvectorspace.vectorspace)
    7.84 +  have U: "vectorspace U" by (rule subspace.vectorspace)
    7.85 +  have V: "vectorspace V" by (rule subspace.vectorspace)
    7.86    from u1 u2 v1 v2 and sum have eq: "u1 - u2 = v2 - v1"
    7.87      by (simp add: add_diff_swap)
    7.88    from u1 u2 have u: "u1 - u2 \<in> U"
    7.89 @@ -345,7 +347,7 @@
    7.90  *}
    7.91  
    7.92  lemma decomp_H':
    7.93 -  includes vectorspace E + subvectorspace H E
    7.94 +  includes vectorspace E + subspace H E
    7.95    assumes y1: "y1 \<in> H" and y2: "y2 \<in> H"
    7.96      and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
    7.97      and eq: "y1 + a1 \<cdot> x' = y2 + a2 \<cdot> x'"
    7.98 @@ -397,7 +399,7 @@
    7.99  *}
   7.100  
   7.101  lemma decomp_H'_H:
   7.102 -  includes vectorspace E + subvectorspace H E
   7.103 +  includes vectorspace E + subspace H E
   7.104    assumes t: "t \<in> H"
   7.105      and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
   7.106    shows "(SOME (y, a). t = y + a \<cdot> x' \<and> y \<in> H) = (t, 0)"
   7.107 @@ -424,7 +426,7 @@
   7.108      "h' \<equiv> (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a \<cdot> x' \<and> y \<in> H)
   7.109                  in (h y) + a * xi)"
   7.110      and x: "x = y + a \<cdot> x'"
   7.111 -  includes vectorspace E + subvectorspace H E
   7.112 +  includes vectorspace E + subspace H E
   7.113    assumes y: "y \<in> H"
   7.114      and x': "x' \<notin> H"  "x' \<in> E"  "x' \<noteq> 0"
   7.115    shows "h' x = h y + a * xi"