src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
changeset 31795 be3e1cc5005c
parent 29252 ea97aa6aeba2
child 32960 69916a850301
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Wed Jun 24 21:46:54 2009 +0200
     1.3 @@ -0,0 +1,445 @@
     1.4 +(*  Title:      HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
     1.5 +    Author:     Gertrud Bauer, TU Munich
     1.6 +*)
     1.7 +
     1.8 +header {* The supremum w.r.t.~the function order *}
     1.9 +
    1.10 +theory Hahn_Banach_Sup_Lemmas
    1.11 +imports Function_Norm Zorn_Lemma
    1.12 +begin
    1.13 +
    1.14 +text {*
    1.15 +  This section contains some lemmas that will be used in the proof of
    1.16 +  the Hahn-Banach Theorem.  In this section the following context is
    1.17 +  presumed.  Let @{text E} be a real vector space with a seminorm
    1.18 +  @{text p} on @{text E}.  @{text F} is a subspace of @{text E} and
    1.19 +  @{text f} a linear form on @{text F}. We consider a chain @{text c}
    1.20 +  of norm-preserving extensions of @{text f}, such that @{text "\<Union>c =
    1.21 +  graph H h"}.  We will show some properties about the limit function
    1.22 +  @{text h}, i.e.\ the supremum of the chain @{text c}.
    1.23 +
    1.24 +  \medskip Let @{text c} be a chain of norm-preserving extensions of
    1.25 +  the function @{text f} and let @{text "graph H h"} be the supremum
    1.26 +  of @{text c}.  Every element in @{text H} is member of one of the
    1.27 +  elements of the chain.
    1.28 +*}
    1.29 +lemmas [dest?] = chainD
    1.30 +lemmas chainE2 [elim?] = chainD2 [elim_format, standard]
    1.31 +
    1.32 +lemma some_H'h't:
    1.33 +  assumes M: "M = norm_pres_extensions E p F f"
    1.34 +    and cM: "c \<in> chain M"
    1.35 +    and u: "graph H h = \<Union>c"
    1.36 +    and x: "x \<in> H"
    1.37 +  shows "\<exists>H' h'. graph H' h' \<in> c
    1.38 +    \<and> (x, h x) \<in> graph H' h'
    1.39 +    \<and> linearform H' h' \<and> H' \<unlhd> E
    1.40 +    \<and> F \<unlhd> H' \<and> graph F f \<subseteq> graph H' h'
    1.41 +    \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
    1.42 +proof -
    1.43 +  from x have "(x, h x) \<in> graph H h" ..
    1.44 +  also from u have "\<dots> = \<Union>c" .
    1.45 +  finally obtain g where gc: "g \<in> c" and gh: "(x, h x) \<in> g" by blast
    1.46 +
    1.47 +  from cM have "c \<subseteq> M" ..
    1.48 +  with gc have "g \<in> M" ..
    1.49 +  also from M have "\<dots> = norm_pres_extensions E p F f" .
    1.50 +  finally obtain H' and h' where g: "g = graph H' h'"
    1.51 +    and * : "linearform H' h'"  "H' \<unlhd> E"  "F \<unlhd> H'"
    1.52 +      "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x" ..
    1.53 +
    1.54 +  from gc and g have "graph H' h' \<in> c" by (simp only:)
    1.55 +  moreover from gh and g have "(x, h x) \<in> graph H' h'" by (simp only:)
    1.56 +  ultimately show ?thesis using * by blast
    1.57 +qed
    1.58 +
    1.59 +text {*
    1.60 +  \medskip Let @{text c} be a chain of norm-preserving extensions of
    1.61 +  the function @{text f} and let @{text "graph H h"} be the supremum
    1.62 +  of @{text c}.  Every element in the domain @{text H} of the supremum
    1.63 +  function is member of the domain @{text H'} of some function @{text
    1.64 +  h'}, such that @{text h} extends @{text h'}.
    1.65 +*}
    1.66 +
    1.67 +lemma some_H'h':
    1.68 +  assumes M: "M = norm_pres_extensions E p F f"
    1.69 +    and cM: "c \<in> chain M"
    1.70 +    and u: "graph H h = \<Union>c"
    1.71 +    and x: "x \<in> H"
    1.72 +  shows "\<exists>H' h'. x \<in> H' \<and> graph H' h' \<subseteq> graph H h
    1.73 +    \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H'
    1.74 +    \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
    1.75 +proof -
    1.76 +  from M cM u x obtain H' h' where
    1.77 +      x_hx: "(x, h x) \<in> graph H' h'"
    1.78 +    and c: "graph H' h' \<in> c"
    1.79 +    and * : "linearform H' h'"  "H' \<unlhd> E"  "F \<unlhd> H'"
    1.80 +      "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x"
    1.81 +    by (rule some_H'h't [elim_format]) blast
    1.82 +  from x_hx have "x \<in> H'" ..
    1.83 +  moreover from cM u c have "graph H' h' \<subseteq> graph H h"
    1.84 +    by (simp only: chain_ball_Union_upper)
    1.85 +  ultimately show ?thesis using * by blast
    1.86 +qed
    1.87 +
    1.88 +text {*
    1.89 +  \medskip Any two elements @{text x} and @{text y} in the domain
    1.90 +  @{text H} of the supremum function @{text h} are both in the domain
    1.91 +  @{text H'} of some function @{text h'}, such that @{text h} extends
    1.92 +  @{text h'}.
    1.93 +*}
    1.94 +
    1.95 +lemma some_H'h'2:
    1.96 +  assumes M: "M = norm_pres_extensions E p F f"
    1.97 +    and cM: "c \<in> chain M"
    1.98 +    and u: "graph H h = \<Union>c"
    1.99 +    and x: "x \<in> H"
   1.100 +    and y: "y \<in> H"
   1.101 +  shows "\<exists>H' h'. x \<in> H' \<and> y \<in> H'
   1.102 +    \<and> graph H' h' \<subseteq> graph H h
   1.103 +    \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H'
   1.104 +    \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
   1.105 +proof -
   1.106 +  txt {* @{text y} is in the domain @{text H''} of some function @{text h''},
   1.107 +  such that @{text h} extends @{text h''}. *}
   1.108 +
   1.109 +  from M cM u and y obtain H' h' where
   1.110 +      y_hy: "(y, h y) \<in> graph H' h'"
   1.111 +    and c': "graph H' h' \<in> c"
   1.112 +    and * :
   1.113 +      "linearform H' h'"  "H' \<unlhd> E"  "F \<unlhd> H'"
   1.114 +      "graph F f \<subseteq> graph H' h'"  "\<forall>x \<in> H'. h' x \<le> p x"
   1.115 +    by (rule some_H'h't [elim_format]) blast
   1.116 +
   1.117 +  txt {* @{text x} is in the domain @{text H'} of some function @{text h'},
   1.118 +    such that @{text h} extends @{text h'}. *}
   1.119 +
   1.120 +  from M cM u and x obtain H'' h'' where
   1.121 +      x_hx: "(x, h x) \<in> graph H'' h''"
   1.122 +    and c'': "graph H'' h'' \<in> c"
   1.123 +    and ** :
   1.124 +      "linearform H'' h''"  "H'' \<unlhd> E"  "F \<unlhd> H''"
   1.125 +      "graph F f \<subseteq> graph H'' h''"  "\<forall>x \<in> H''. h'' x \<le> p x"
   1.126 +    by (rule some_H'h't [elim_format]) blast
   1.127 +
   1.128 +  txt {* Since both @{text h'} and @{text h''} are elements of the chain,
   1.129 +    @{text h''} is an extension of @{text h'} or vice versa. Thus both
   1.130 +    @{text x} and @{text y} are contained in the greater
   1.131 +    one. \label{cases1}*}
   1.132 +
   1.133 +  from cM c'' c' have "graph H'' h'' \<subseteq> graph H' h' \<or> graph H' h' \<subseteq> graph H'' h''"
   1.134 +    (is "?case1 \<or> ?case2") ..
   1.135 +  then show ?thesis
   1.136 +  proof
   1.137 +    assume ?case1
   1.138 +    have "(x, h x) \<in> graph H'' h''" by fact
   1.139 +    also have "\<dots> \<subseteq> graph H' h'" by fact
   1.140 +    finally have xh:"(x, h x) \<in> graph H' h'" .
   1.141 +    then have "x \<in> H'" ..
   1.142 +    moreover from y_hy have "y \<in> H'" ..
   1.143 +    moreover from cM u and c' have "graph H' h' \<subseteq> graph H h"
   1.144 +      by (simp only: chain_ball_Union_upper)
   1.145 +    ultimately show ?thesis using * by blast
   1.146 +  next
   1.147 +    assume ?case2
   1.148 +    from x_hx have "x \<in> H''" ..
   1.149 +    moreover {
   1.150 +      have "(y, h y) \<in> graph H' h'" by (rule y_hy)
   1.151 +      also have "\<dots> \<subseteq> graph H'' h''" by fact
   1.152 +      finally have "(y, h y) \<in> graph H'' h''" .
   1.153 +    } then have "y \<in> H''" ..
   1.154 +    moreover from cM u and c'' have "graph H'' h'' \<subseteq> graph H h"
   1.155 +      by (simp only: chain_ball_Union_upper)
   1.156 +    ultimately show ?thesis using ** by blast
   1.157 +  qed
   1.158 +qed
   1.159 +
   1.160 +text {*
   1.161 +  \medskip The relation induced by the graph of the supremum of a
   1.162 +  chain @{text c} is definite, i.~e.~t is the graph of a function.
   1.163 +*}
   1.164 +
   1.165 +lemma sup_definite:
   1.166 +  assumes M_def: "M \<equiv> norm_pres_extensions E p F f"
   1.167 +    and cM: "c \<in> chain M"
   1.168 +    and xy: "(x, y) \<in> \<Union>c"
   1.169 +    and xz: "(x, z) \<in> \<Union>c"
   1.170 +  shows "z = y"
   1.171 +proof -
   1.172 +  from cM have c: "c \<subseteq> M" ..
   1.173 +  from xy obtain G1 where xy': "(x, y) \<in> G1" and G1: "G1 \<in> c" ..
   1.174 +  from xz obtain G2 where xz': "(x, z) \<in> G2" and G2: "G2 \<in> c" ..
   1.175 +
   1.176 +  from G1 c have "G1 \<in> M" ..
   1.177 +  then obtain H1 h1 where G1_rep: "G1 = graph H1 h1"
   1.178 +    unfolding M_def by blast
   1.179 +
   1.180 +  from G2 c have "G2 \<in> M" ..
   1.181 +  then obtain H2 h2 where G2_rep: "G2 = graph H2 h2"
   1.182 +    unfolding M_def by blast
   1.183 +
   1.184 +  txt {* @{text "G\<^sub>1"} is contained in @{text "G\<^sub>2"}
   1.185 +    or vice versa, since both @{text "G\<^sub>1"} and @{text
   1.186 +    "G\<^sub>2"} are members of @{text c}. \label{cases2}*}
   1.187 +
   1.188 +  from cM G1 G2 have "G1 \<subseteq> G2 \<or> G2 \<subseteq> G1" (is "?case1 \<or> ?case2") ..
   1.189 +  then show ?thesis
   1.190 +  proof
   1.191 +    assume ?case1
   1.192 +    with xy' G2_rep have "(x, y) \<in> graph H2 h2" by blast
   1.193 +    then have "y = h2 x" ..
   1.194 +    also
   1.195 +    from xz' G2_rep have "(x, z) \<in> graph H2 h2" by (simp only:)
   1.196 +    then have "z = h2 x" ..
   1.197 +    finally show ?thesis .
   1.198 +  next
   1.199 +    assume ?case2
   1.200 +    with xz' G1_rep have "(x, z) \<in> graph H1 h1" by blast
   1.201 +    then have "z = h1 x" ..
   1.202 +    also
   1.203 +    from xy' G1_rep have "(x, y) \<in> graph H1 h1" by (simp only:)
   1.204 +    then have "y = h1 x" ..
   1.205 +    finally show ?thesis ..
   1.206 +  qed
   1.207 +qed
   1.208 +
   1.209 +text {*
   1.210 +  \medskip The limit function @{text h} is linear. Every element
   1.211 +  @{text x} in the domain of @{text h} is in the domain of a function
   1.212 +  @{text h'} in the chain of norm preserving extensions.  Furthermore,
   1.213 +  @{text h} is an extension of @{text h'} so the function values of
   1.214 +  @{text x} are identical for @{text h'} and @{text h}.  Finally, the
   1.215 +  function @{text h'} is linear by construction of @{text M}.
   1.216 +*}
   1.217 +
   1.218 +lemma sup_lf:
   1.219 +  assumes M: "M = norm_pres_extensions E p F f"
   1.220 +    and cM: "c \<in> chain M"
   1.221 +    and u: "graph H h = \<Union>c"
   1.222 +  shows "linearform H h"
   1.223 +proof
   1.224 +  fix x y assume x: "x \<in> H" and y: "y \<in> H"
   1.225 +  with M cM u obtain H' h' where
   1.226 +        x': "x \<in> H'" and y': "y \<in> H'"
   1.227 +      and b: "graph H' h' \<subseteq> graph H h"
   1.228 +      and linearform: "linearform H' h'"
   1.229 +      and subspace: "H' \<unlhd> E"
   1.230 +    by (rule some_H'h'2 [elim_format]) blast
   1.231 +
   1.232 +  show "h (x + y) = h x + h y"
   1.233 +  proof -
   1.234 +    from linearform x' y' have "h' (x + y) = h' x + h' y"
   1.235 +      by (rule linearform.add)
   1.236 +    also from b x' have "h' x = h x" ..
   1.237 +    also from b y' have "h' y = h y" ..
   1.238 +    also from subspace x' y' have "x + y \<in> H'"
   1.239 +      by (rule subspace.add_closed)
   1.240 +    with b have "h' (x + y) = h (x + y)" ..
   1.241 +    finally show ?thesis .
   1.242 +  qed
   1.243 +next
   1.244 +  fix x a assume x: "x \<in> H"
   1.245 +  with M cM u obtain H' h' where
   1.246 +        x': "x \<in> H'"
   1.247 +      and b: "graph H' h' \<subseteq> graph H h"
   1.248 +      and linearform: "linearform H' h'"
   1.249 +      and subspace: "H' \<unlhd> E"
   1.250 +    by (rule some_H'h' [elim_format]) blast
   1.251 +
   1.252 +  show "h (a \<cdot> x) = a * h x"
   1.253 +  proof -
   1.254 +    from linearform x' have "h' (a \<cdot> x) = a * h' x"
   1.255 +      by (rule linearform.mult)
   1.256 +    also from b x' have "h' x = h x" ..
   1.257 +    also from subspace x' have "a \<cdot> x \<in> H'"
   1.258 +      by (rule subspace.mult_closed)
   1.259 +    with b have "h' (a \<cdot> x) = h (a \<cdot> x)" ..
   1.260 +    finally show ?thesis .
   1.261 +  qed
   1.262 +qed
   1.263 +
   1.264 +text {*
   1.265 +  \medskip The limit of a non-empty chain of norm preserving
   1.266 +  extensions of @{text f} is an extension of @{text f}, since every
   1.267 +  element of the chain is an extension of @{text f} and the supremum
   1.268 +  is an extension for every element of the chain.
   1.269 +*}
   1.270 +
   1.271 +lemma sup_ext:
   1.272 +  assumes graph: "graph H h = \<Union>c"
   1.273 +    and M: "M = norm_pres_extensions E p F f"
   1.274 +    and cM: "c \<in> chain M"
   1.275 +    and ex: "\<exists>x. x \<in> c"
   1.276 +  shows "graph F f \<subseteq> graph H h"
   1.277 +proof -
   1.278 +  from ex obtain x where xc: "x \<in> c" ..
   1.279 +  from cM have "c \<subseteq> M" ..
   1.280 +  with xc have "x \<in> M" ..
   1.281 +  with M have "x \<in> norm_pres_extensions E p F f"
   1.282 +    by (simp only:)
   1.283 +  then obtain G g where "x = graph G g" and "graph F f \<subseteq> graph G g" ..
   1.284 +  then have "graph F f \<subseteq> x" by (simp only:)
   1.285 +  also from xc have "\<dots> \<subseteq> \<Union>c" by blast
   1.286 +  also from graph have "\<dots> = graph H h" ..
   1.287 +  finally show ?thesis .
   1.288 +qed
   1.289 +
   1.290 +text {*
   1.291 +  \medskip The domain @{text H} of the limit function is a superspace
   1.292 +  of @{text F}, since @{text F} is a subset of @{text H}. The
   1.293 +  existence of the @{text 0} element in @{text F} and the closure
   1.294 +  properties follow from the fact that @{text F} is a vector space.
   1.295 +*}
   1.296 +
   1.297 +lemma sup_supF:
   1.298 +  assumes graph: "graph H h = \<Union>c"
   1.299 +    and M: "M = norm_pres_extensions E p F f"
   1.300 +    and cM: "c \<in> chain M"
   1.301 +    and ex: "\<exists>x. x \<in> c"
   1.302 +    and FE: "F \<unlhd> E"
   1.303 +  shows "F \<unlhd> H"
   1.304 +proof
   1.305 +  from FE show "F \<noteq> {}" by (rule subspace.non_empty)
   1.306 +  from graph M cM ex have "graph F f \<subseteq> graph H h" by (rule sup_ext)
   1.307 +  then show "F \<subseteq> H" ..
   1.308 +  fix x y assume "x \<in> F" and "y \<in> F"
   1.309 +  with FE show "x + y \<in> F" by (rule subspace.add_closed)
   1.310 +next
   1.311 +  fix x a assume "x \<in> F"
   1.312 +  with FE show "a \<cdot> x \<in> F" by (rule subspace.mult_closed)
   1.313 +qed
   1.314 +
   1.315 +text {*
   1.316 +  \medskip The domain @{text H} of the limit function is a subspace of
   1.317 +  @{text E}.
   1.318 +*}
   1.319 +
   1.320 +lemma sup_subE:
   1.321 +  assumes graph: "graph H h = \<Union>c"
   1.322 +    and M: "M = norm_pres_extensions E p F f"
   1.323 +    and cM: "c \<in> chain M"
   1.324 +    and ex: "\<exists>x. x \<in> c"
   1.325 +    and FE: "F \<unlhd> E"
   1.326 +    and E: "vectorspace E"
   1.327 +  shows "H \<unlhd> E"
   1.328 +proof
   1.329 +  show "H \<noteq> {}"
   1.330 +  proof -
   1.331 +    from FE E have "0 \<in> F" by (rule subspace.zero)
   1.332 +    also from graph M cM ex FE have "F \<unlhd> H" by (rule sup_supF)
   1.333 +    then have "F \<subseteq> H" ..
   1.334 +    finally show ?thesis by blast
   1.335 +  qed
   1.336 +  show "H \<subseteq> E"
   1.337 +  proof
   1.338 +    fix x assume "x \<in> H"
   1.339 +    with M cM graph
   1.340 +    obtain H' h' where x: "x \<in> H'" and H'E: "H' \<unlhd> E"
   1.341 +      by (rule some_H'h' [elim_format]) blast
   1.342 +    from H'E have "H' \<subseteq> E" ..
   1.343 +    with x show "x \<in> E" ..
   1.344 +  qed
   1.345 +  fix x y assume x: "x \<in> H" and y: "y \<in> H"
   1.346 +  show "x + y \<in> H"
   1.347 +  proof -
   1.348 +    from M cM graph x y obtain H' h' where
   1.349 +          x': "x \<in> H'" and y': "y \<in> H'" and H'E: "H' \<unlhd> E"
   1.350 +        and graphs: "graph H' h' \<subseteq> graph H h"
   1.351 +      by (rule some_H'h'2 [elim_format]) blast
   1.352 +    from H'E x' y' have "x + y \<in> H'"
   1.353 +      by (rule subspace.add_closed)
   1.354 +    also from graphs have "H' \<subseteq> H" ..
   1.355 +    finally show ?thesis .
   1.356 +  qed
   1.357 +next
   1.358 +  fix x a assume x: "x \<in> H"
   1.359 +  show "a \<cdot> x \<in> H"
   1.360 +  proof -
   1.361 +    from M cM graph x
   1.362 +    obtain H' h' where x': "x \<in> H'" and H'E: "H' \<unlhd> E"
   1.363 +        and graphs: "graph H' h' \<subseteq> graph H h"
   1.364 +      by (rule some_H'h' [elim_format]) blast
   1.365 +    from H'E x' have "a \<cdot> x \<in> H'" by (rule subspace.mult_closed)
   1.366 +    also from graphs have "H' \<subseteq> H" ..
   1.367 +    finally show ?thesis .
   1.368 +  qed
   1.369 +qed
   1.370 +
   1.371 +text {*
   1.372 +  \medskip The limit function is bounded by the norm @{text p} as
   1.373 +  well, since all elements in the chain are bounded by @{text p}.
   1.374 +*}
   1.375 +
   1.376 +lemma sup_norm_pres:
   1.377 +  assumes graph: "graph H h = \<Union>c"
   1.378 +    and M: "M = norm_pres_extensions E p F f"
   1.379 +    and cM: "c \<in> chain M"
   1.380 +  shows "\<forall>x \<in> H. h x \<le> p x"
   1.381 +proof
   1.382 +  fix x assume "x \<in> H"
   1.383 +  with M cM graph obtain H' h' where x': "x \<in> H'"
   1.384 +      and graphs: "graph H' h' \<subseteq> graph H h"
   1.385 +      and a: "\<forall>x \<in> H'. h' x \<le> p x"
   1.386 +    by (rule some_H'h' [elim_format]) blast
   1.387 +  from graphs x' have [symmetric]: "h' x = h x" ..
   1.388 +  also from a x' have "h' x \<le> p x " ..
   1.389 +  finally show "h x \<le> p x" .
   1.390 +qed
   1.391 +
   1.392 +text {*
   1.393 +  \medskip The following lemma is a property of linear forms on real
   1.394 +  vector spaces. It will be used for the lemma @{text abs_Hahn_Banach}
   1.395 +  (see page \pageref{abs-Hahn_Banach}). \label{abs-ineq-iff} For real
   1.396 +  vector spaces the following inequations are equivalent:
   1.397 +  \begin{center}
   1.398 +  \begin{tabular}{lll}
   1.399 +  @{text "\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x"} & and &
   1.400 +  @{text "\<forall>x \<in> H. h x \<le> p x"} \\
   1.401 +  \end{tabular}
   1.402 +  \end{center}
   1.403 +*}
   1.404 +
   1.405 +lemma abs_ineq_iff:
   1.406 +  assumes "subspace H E" and "vectorspace E" and "seminorm E p"
   1.407 +    and "linearform H h"
   1.408 +  shows "(\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x) = (\<forall>x \<in> H. h x \<le> p x)" (is "?L = ?R")
   1.409 +proof
   1.410 +  interpret subspace H E by fact
   1.411 +  interpret vectorspace E by fact
   1.412 +  interpret seminorm E p by fact
   1.413 +  interpret linearform H h by fact
   1.414 +  have H: "vectorspace H" using `vectorspace E` ..
   1.415 +  {
   1.416 +    assume l: ?L
   1.417 +    show ?R
   1.418 +    proof
   1.419 +      fix x assume x: "x \<in> H"
   1.420 +      have "h x \<le> \<bar>h x\<bar>" by arith
   1.421 +      also from l x have "\<dots> \<le> p x" ..
   1.422 +      finally show "h x \<le> p x" .
   1.423 +    qed
   1.424 +  next
   1.425 +    assume r: ?R
   1.426 +    show ?L
   1.427 +    proof
   1.428 +      fix x assume x: "x \<in> H"
   1.429 +      show "\<And>a b :: real. - a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> \<bar>b\<bar> \<le> a"
   1.430 +        by arith
   1.431 +      from `linearform H h` and H x
   1.432 +      have "- h x = h (- x)" by (rule linearform.neg [symmetric])
   1.433 +      also
   1.434 +      from H x have "- x \<in> H" by (rule vectorspace.neg_closed)
   1.435 +      with r have "h (- x) \<le> p (- x)" ..
   1.436 +      also have "\<dots> = p x"
   1.437 +	using `seminorm E p` `vectorspace E`
   1.438 +      proof (rule seminorm.minus)
   1.439 +        from x show "x \<in> E" ..
   1.440 +      qed
   1.441 +      finally have "- h x \<le> p x" .
   1.442 +      then show "- p x \<le> h x" by simp
   1.443 +      from r x show "h x \<le> p x" ..
   1.444 +    qed
   1.445 +  }
   1.446 +qed
   1.447 +
   1.448 +end