author wenzelm Thu Aug 29 16:08:30 2002 +0200 (2002-08-29) changeset 13547 bf399f3bd7dc parent 13546 f76237c2be75 child 13548 36cb5fb8188c
tuned;
     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.41            also from x'E uE vE have "\<dots> = (v + x') - (u + x')"
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.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.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.11 -  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> \<parallel>x - y\<parallel> \<le> \<parallel>x\<parallel> + \<parallel>y\<parallel>"
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.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.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"