author wenzelm Mon Nov 02 11:43:02 2015 +0100 (2015-11-02) changeset 61540 f92bf6674699 parent 61539 a29295dac1ca child 61541 846c72206207
tuned document;
     1.1 --- a/src/HOL/Hahn_Banach/Function_Norm.thy	Mon Nov 02 11:10:28 2015 +0100
1.2 +++ b/src/HOL/Hahn_Banach/Function_Norm.thy	Mon Nov 02 11:43:02 2015 +0100
1.3 @@ -11,14 +11,13 @@
1.4  subsection \<open>Continuous linear forms\<close>
1.5
1.6  text \<open>
1.7 -  A linear form \<open>f\<close> on a normed vector space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close>
1.8 -  is \<^emph>\<open>continuous\<close>, iff it is bounded, i.e.
1.9 +  A linear form \<open>f\<close> on a normed vector space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> is \<^emph>\<open>continuous\<close>,
1.10 +  iff it is bounded, i.e.
1.11    \begin{center}
1.12    \<open>\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
1.13    \end{center}
1.14 -  In our application no other functions than linear forms are
1.15 -  considered, so we can define continuous linear forms as bounded
1.16 -  linear forms:
1.17 +  In our application no other functions than linear forms are considered, so
1.18 +  we can define continuous linear forms as bounded linear forms:
1.19  \<close>
1.20
1.21  locale continuous = linearform +
1.22 @@ -48,28 +47,25 @@
1.23    \end{center}
1.24    is called the \<^emph>\<open>norm\<close> of \<open>f\<close>.
1.25
1.26 -  For non-trivial vector spaces \<open>V \<noteq> {0}\<close> the norm can be
1.27 -  defined as
1.28 +  For non-trivial vector spaces \<open>V \<noteq> {0}\<close> the norm can be defined as
1.29    \begin{center}
1.30    \<open>\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>\<close>
1.31    \end{center}
1.32
1.33 -  For the case \<open>V = {0}\<close> the supremum would be taken from an
1.34 -  empty set. Since \<open>\<real>\<close> is unbounded, there would be no supremum.
1.35 -  To avoid this situation it must be guaranteed that there is an
1.36 -  element in this set. This element must be \<open>{} \<ge> 0\<close> so that
1.37 -  \<open>fn_norm\<close> has the norm properties. Furthermore it does not
1.38 -  have to change the norm in all other cases, so it must be \<open>0\<close>,
1.39 -  as all other elements are \<open>{} \<ge> 0\<close>.
1.40 +  For the case \<open>V = {0}\<close> the supremum would be taken from an empty set.
1.41 +  Since \<open>\<real>\<close> is unbounded, there would be no supremum. To avoid this
1.42 +  situation it must be guaranteed that there is an element in this set. This
1.43 +  element must be \<open>{} \<ge> 0\<close> so that \<open>fn_norm\<close> has the norm properties.
1.44 +  Furthermore it does not have to change the norm in all other cases, so it
1.45 +  must be \<open>0\<close>, as all other elements are \<open>{} \<ge> 0\<close>.
1.46
1.47 -  Thus we define the set \<open>B\<close> where the supremum is taken from as
1.48 -  follows:
1.49 +  Thus we define the set \<open>B\<close> where the supremum is taken from as follows:
1.50    \begin{center}
1.51    \<open>{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}\<close>
1.52    \end{center}
1.53
1.54 -  \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the
1.55 -  supremum exists (otherwise it is undefined).
1.56 +  \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the supremum exists
1.57 +  (otherwise it is undefined).
1.58  \<close>
1.59
1.60  locale fn_norm =
1.61 @@ -84,8 +80,8 @@
1.62    by (simp add: B_def)
1.63
1.64  text \<open>
1.65 -  The following lemma states that every continuous linear form on a
1.66 -  normed space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> has a function norm.
1.67 +  The following lemma states that every continuous linear form on a normed
1.68 +  space \<open>(V, \<parallel>\<cdot>\<parallel>)\<close> has a function norm.
1.69  \<close>
1.70
1.71  lemma (in normed_vectorspace_with_fn_norm) fn_norm_works:
1.72 @@ -108,9 +104,9 @@
1.73        txt \<open>We know that \<open>f\<close> is bounded by some value \<open>c\<close>.\<close>
1.74        from bounded obtain c where c: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * \<parallel>x\<parallel>" ..
1.75
1.76 -      txt \<open>To prove the thesis, we have to show that there is some
1.77 -        \<open>b\<close>, such that \<open>y \<le> b\<close> for all \<open>y \<in>
1.78 -        B\<close>. Due to the definition of \<open>B\<close> there are two cases.\<close>
1.79 +      txt \<open>To prove the thesis, we have to show that there is some \<open>b\<close>, such
1.80 +        that \<open>y \<le> b\<close> for all \<open>y \<in> B\<close>. Due to the definition of \<open>B\<close> there are
1.81 +        two cases.\<close>
1.82
1.83        def b \<equiv> "max c 0"
1.84        have "\<forall>y \<in> B V f. y \<le> b"
1.85 @@ -237,8 +233,8 @@
1.86
1.87  text \<open>
1.88    \<^medskip>
1.89 -  The function norm is the least positive real number for
1.90 -  which the following inequation holds:
1.91 +  The function norm is the least positive real number for which the
1.92 +  following inequality holds:
1.93    \begin{center}
1.94      \<open>\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
1.95    \end{center}

     2.1 --- a/src/HOL/Hahn_Banach/Function_Order.thy	Mon Nov 02 11:10:28 2015 +0100
2.2 +++ b/src/HOL/Hahn_Banach/Function_Order.thy	Mon Nov 02 11:43:02 2015 +0100
2.3 @@ -70,8 +70,8 @@
2.4    where "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))"
2.5
2.6  text \<open>
2.7 -  The following lemma states that \<open>g\<close> is the graph of a function
2.8 -  if the relation induced by \<open>g\<close> is unique.
2.9 +  The following lemma states that \<open>g\<close> is the graph of a function if the
2.10 +  relation induced by \<open>g\<close> is unique.
2.11  \<close>
2.12
2.13  lemma graph_domain_funct:
2.14 @@ -93,9 +93,9 @@
2.15  subsection \<open>Norm-preserving extensions of a function\<close>
2.16
2.17  text \<open>
2.18 -  Given a linear form \<open>f\<close> on the space \<open>F\<close> and a seminorm
2.19 -  \<open>p\<close> on \<open>E\<close>. The set of all linear extensions of \<open>f\<close>, to superspaces \<open>H\<close> of \<open>F\<close>, which are bounded by
2.20 -  \<open>p\<close>, is defined as follows.
2.21 +  Given a linear form \<open>f\<close> on the space \<open>F\<close> and a seminorm \<open>p\<close> on \<open>E\<close>. The
2.22 +  set of all linear extensions of \<open>f\<close>, to superspaces \<open>H\<close> of \<open>F\<close>, which are
2.23 +  bounded by \<open>p\<close>, is defined as follows.
2.24  \<close>
2.25
2.26  definition

     3.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Mon Nov 02 11:10:28 2015 +0100
3.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Mon Nov 02 11:43:02 2015 +0100
3.3 @@ -9,37 +9,36 @@
3.4  begin
3.5
3.6  text \<open>
3.7 -  We present the proof of two different versions of the Hahn-Banach
3.8 -  Theorem, closely following @{cite \<open>\S36\<close> "Heuser:1986"}.
3.9 +  We present the proof of two different versions of the Hahn-Banach Theorem,
3.10 +  closely following @{cite \<open>\S36\<close> "Heuser:1986"}.
3.11  \<close>
3.12
3.13 +
3.14  subsection \<open>The Hahn-Banach Theorem for vector spaces\<close>
3.15
3.16  paragraph \<open>Hahn-Banach Theorem.\<close>
3.17  text \<open>
3.18 -  Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm on \<open>E\<close>, and \<open>f\<close> be a linear form defined on
3.19 -  \<open>F\<close> such that \<open>f\<close> is bounded by \<open>p\<close>, i.e. \<open>\<forall>x \<in>
3.20 -  F. f x \<le> p x\<close>. Then \<open>f\<close> can be extended to a linear form \<open>h\<close>
3.21 -  on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is
3.22 -  also bounded by \<open>p\<close>.
3.23 -\<close>
3.24 +  Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm
3.25 +  on \<open>E\<close>, and \<open>f\<close> be a linear form defined on \<open>F\<close> such that \<open>f\<close> is bounded
3.26 +  by \<open>p\<close>, i.e. \<open>\<forall>x \<in> F. f x \<le> p x\<close>. Then \<open>f\<close> can be extended to a linear
3.27 +  form \<open>h\<close> on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is also bounded
3.28 +  by \<open>p\<close>. \<close>
3.29
3.30  paragraph \<open>Proof Sketch.\<close>
3.31  text \<open>
3.32 -  \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of
3.33 -  \<open>f\<close> to subspaces of \<open>E\<close>. The linear forms in \<open>M\<close>
3.34 -  are ordered by domain extension.
3.35 +  \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of \<open>f\<close> to subspaces
3.36 +  of \<open>E\<close>. The linear forms in \<open>M\<close> are ordered by domain extension.
3.37
3.38 -  \<^enum> We show that every non-empty chain in \<open>M\<close> has an upper
3.39 -  bound in \<open>M\<close>.
3.40 +  \<^enum> We show that every non-empty chain in \<open>M\<close> has an upper bound in \<open>M\<close>.
3.41
3.42 -  \<^enum> With Zorn's Lemma we conclude that there is a maximal function
3.43 -  \<open>g\<close> in \<open>M\<close>.
3.44 +  \<^enum> With Zorn's Lemma we conclude that there is a maximal function \<open>g\<close> in
3.45 +  \<open>M\<close>.
3.46
3.47 -  \<^enum> The domain \<open>H\<close> of \<open>g\<close> is the whole space \<open>E\<close>, as shown by classical contradiction:
3.48 +  \<^enum> The domain \<open>H\<close> of \<open>g\<close> is the whole space \<open>E\<close>, as shown by classical
3.50
3.51 -    \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can
3.52 -    still be extended in a norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>.
3.53 +    \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can still be extended in
3.54 +    a norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>.
3.55
3.56      \<^item> Thus \<open>g\<close> can not be maximal. Contradiction!
3.57  \<close>
3.58 @@ -153,7 +152,7 @@
3.59        obtain xi where
3.60          xi: "\<forall>y \<in> H. - p (y + x') - h y \<le> xi
3.61            \<and> xi \<le> p (y + x') - h y"
3.62 -        -- \<open>Pick a real number \<open>\<xi>\<close> that fulfills certain inequations; this will\<close>
3.63 +        -- \<open>Pick a real number \<open>\<xi>\<close> that fulfills certain inequality; this will\<close>
3.64          -- \<open>be used to establish that \<open>h'\<close> is a norm-preserving extension of \<open>h\<close>.
3.65             \label{ex-xi-use}\<^smallskip>\<close>
3.66        proof -
3.67 @@ -292,10 +291,10 @@
3.68
3.69  text \<open>
3.70    The following alternative formulation of the Hahn-Banach
3.71 -  Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear
3.72 -  form \<open>f\<close> and a seminorm \<open>p\<close> the following inequations
3.73 -  are equivalent:\footnote{This was shown in lemma @{thm [source]
3.74 -  abs_ineq_iff} (see page \pageref{abs-ineq-iff}).}
3.75 +  Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear form
3.76 +  \<open>f\<close> and a seminorm \<open>p\<close> the following inequality are
3.77 +  equivalent:\footnote{This was shown in lemma @{thm [source] abs_ineq_iff}
3.78 +  (see page \pageref{abs-ineq-iff}).}
3.79    \begin{center}
3.80    \begin{tabular}{lll}
3.81    \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &
3.82 @@ -336,9 +335,9 @@
3.83  subsection \<open>The Hahn-Banach Theorem for normed spaces\<close>
3.84
3.85  text \<open>
3.86 -  Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a
3.87 -  norm space \<open>E\<close>, can be extended to a continuous linear form
3.88 -  \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> = \<parallel>g\<parallel>\<close>.
3.89 +  Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a norm space \<open>E\<close>,
3.90 +  can be extended to a continuous linear form \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> =
3.91 +  \<parallel>g\<parallel>\<close>.
3.92  \<close>
3.93
3.94  theorem norm_Hahn_Banach:
3.95 @@ -420,10 +419,10 @@
3.96           OF F_norm, folded B_def fn_norm_def])
3.97    qed
3.98
3.99 -  txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded
3.100 -    by \<open>p\<close> we can apply the Hahn-Banach Theorem for real vector
3.101 -    spaces. So \<open>f\<close> can be extended in a norm-preserving way to
3.102 -    some function \<open>g\<close> on the whole vector space \<open>E\<close>.\<close>
3.103 +  txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded by \<open>p\<close> we
3.104 +    can apply the Hahn-Banach Theorem for real vector spaces. So \<open>f\<close> can be
3.105 +    extended in a norm-preserving way to some function \<open>g\<close> on the whole
3.106 +    vector space \<open>E\<close>.\<close>
3.107
3.108    with E FE linearform q obtain g where
3.109        linearformE: "linearform E g"
3.110 @@ -445,19 +444,20 @@
3.111    have "\<parallel>g\<parallel>\<hyphen>E = \<parallel>f\<parallel>\<hyphen>F"
3.112    proof (rule order_antisym)
3.113      txt \<open>
3.114 -      First we show \<open>\<parallel>g\<parallel> \<le> \<parallel>f\<parallel>\<close>.  The function norm \<open>\<parallel>g\<parallel>\<close> is defined as the smallest \<open>c \<in> \<real>\<close> such that
3.115 +      First we show \<open>\<parallel>g\<parallel> \<le> \<parallel>f\<parallel>\<close>. The function norm \<open>\<parallel>g\<parallel>\<close> is defined as the
3.116 +      smallest \<open>c \<in> \<real>\<close> such that
3.117        \begin{center}
3.118        \begin{tabular}{l}
3.119        \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>\<close>
3.120        \end{tabular}
3.121        \end{center}
3.122 -      \noindent Furthermore holds
3.123 +      \<^noindent> Furthermore holds
3.124        \begin{center}
3.125        \begin{tabular}{l}
3.126        \<open>\<forall>x \<in> E. \<bar>g x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>\<close>
3.127        \end{tabular}
3.128        \end{center}
3.129 -\<close>
3.130 +    \<close>
3.131
3.132      from g_cont _ ge_zero
3.133      show "\<parallel>g\<parallel>\<hyphen>E \<le> \<parallel>f\<parallel>\<hyphen>F"

     4.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Mon Nov 02 11:10:28 2015 +0100
4.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Mon Nov 02 11:43:02 2015 +0100
4.3 @@ -9,29 +9,27 @@
4.4  begin
4.5
4.6  text \<open>
4.7 -  In this section the following context is presumed.  Let \<open>E\<close> be
4.8 -  a real vector space with a seminorm \<open>q\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of \<open>E\<close> and \<open>f\<close> a linear function on
4.9 -  \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a
4.10 -  superspace of \<open>F\<close> and a linear form \<open>h\<close> on \<open>H\<close>. \<open>H\<close> is a not equal to \<open>E\<close> and \<open>x\<^sub>0\<close> is
4.11 -  an element in \<open>E - H\<close>.  \<open>H\<close> is extended to the direct
4.12 -  sum \<open>H' = H + lin x\<^sub>0\<close>, so for any \<open>x \<in> H'\<close>
4.13 -  the decomposition of \<open>x = y + a \<cdot> x\<close> with \<open>y \<in> H\<close> is
4.14 -  unique. \<open>h'\<close> is defined on \<open>H'\<close> by \<open>h' x = h y +
4.15 -  a \<cdot> \<xi>\<close> for a certain \<open>\<xi>\<close>.
4.16 +  In this section the following context is presumed. Let \<open>E\<close> be a real
4.17 +  vector space with a seminorm \<open>q\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of \<open>E\<close> and \<open>f\<close>
4.18 +  a linear function on \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a
4.19 +  superspace of \<open>F\<close> and a linear form \<open>h\<close> on \<open>H\<close>. \<open>H\<close> is a not equal to \<open>E\<close>
4.20 +  and \<open>x\<^sub>0\<close> is an element in \<open>E - H\<close>. \<open>H\<close> is extended to the direct sum \<open>H'
4.21 +  = H + lin x\<^sub>0\<close>, so for any \<open>x \<in> H'\<close> the decomposition of \<open>x = y + a \<cdot> x\<close>
4.22 +  with \<open>y \<in> H\<close> is unique. \<open>h'\<close> is defined on \<open>H'\<close> by \<open>h' x = h y + a \<cdot> \<xi>\<close>
4.23 +  for a certain \<open>\<xi>\<close>.
4.24
4.25 -  Subsequently we show some properties of this extension \<open>h'\<close> of
4.26 -  \<open>h\<close>.
4.27 +  Subsequently we show some properties of this extension \<open>h'\<close> of \<open>h\<close>.
4.28
4.29    \<^medskip>
4.30 -  This lemma will be used to show the existence of a linear
4.31 -  extension of \<open>f\<close> (see page \pageref{ex-xi-use}). It is a
4.32 -  consequence of the completeness of \<open>\<real>\<close>. To show
4.33 +  This lemma will be used to show the existence of a linear extension of \<open>f\<close>
4.34 +  (see page \pageref{ex-xi-use}). It is a consequence of the completeness of
4.35 +  \<open>\<real>\<close>. To show
4.36    \begin{center}
4.37    \begin{tabular}{l}
4.38    \<open>\<exists>\<xi>. \<forall>y \<in> F. a y \<le> \<xi> \<and> \<xi> \<le> b y\<close>
4.39    \end{tabular}
4.40    \end{center}
4.41 -  \noindent it suffices to show that
4.42 +  \<^noindent> it suffices to show that
4.43    \begin{center}
4.44    \begin{tabular}{l}
4.45    \<open>\<forall>u \<in> F. \<forall>v \<in> F. a u \<le> b v\<close>
4.46 @@ -84,9 +82,8 @@
4.47
4.48  text \<open>
4.49    \<^medskip>
4.50 -  The function \<open>h'\<close> is defined as a \<open>h' x = h y
4.51 -  + a \<cdot> \<xi>\<close> where \<open>x = y + a \<cdot> \<xi>\<close> is a linear extension of
4.52 -  \<open>h\<close> to \<open>H'\<close>.
4.53 +  The function \<open>h'\<close> is defined as a \<open>h' x = h y + a \<cdot> \<xi>\<close> where
4.54 +  \<open>x = y + a \<cdot> \<xi>\<close> is a linear extension of \<open>h\<close> to \<open>H'\<close>.
4.55  \<close>
4.56
4.57  lemma h'_lf:
4.58 @@ -192,8 +189,8 @@
4.59
4.60  text \<open>
4.61    \<^medskip>
4.62 -  The linear extension \<open>h'\<close> of \<open>h\<close>
4.63 -  is bounded by the seminorm \<open>p\<close>.\<close>
4.64 +  The linear extension \<open>h'\<close> of \<open>h\<close> is bounded by the seminorm \<open>p\<close>.
4.65 +\<close>
4.66
4.67  lemma h'_norm_pres:
4.68    assumes h'_def: "h' \<equiv> \<lambda>x. let (y, a) =

     5.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Mon Nov 02 11:10:28 2015 +0100
5.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Mon Nov 02 11:43:02 2015 +0100
5.3 @@ -2,27 +2,25 @@
5.4      Author:     Gertrud Bauer, TU Munich
5.5  *)
5.6
5.7 -section \<open>The supremum w.r.t.~the function order\<close>
5.8 +section \<open>The supremum wrt.\ the function order\<close>
5.9
5.10  theory Hahn_Banach_Sup_Lemmas
5.11  imports Function_Norm Zorn_Lemma
5.12  begin
5.13
5.14  text \<open>
5.15 -  This section contains some lemmas that will be used in the proof of
5.16 -  the Hahn-Banach Theorem.  In this section the following context is
5.17 -  presumed.  Let \<open>E\<close> be a real vector space with a seminorm
5.18 -  \<open>p\<close> on \<open>E\<close>.  \<open>F\<close> is a subspace of \<open>E\<close> and
5.19 -  \<open>f\<close> a linear form on \<open>F\<close>. We consider a chain \<open>c\<close>
5.20 -  of norm-preserving extensions of \<open>f\<close>, such that \<open>\<Union>c =
5.21 -  graph H h\<close>.  We will show some properties about the limit function
5.22 -  \<open>h\<close>, i.e.\ the supremum of the chain \<open>c\<close>.
5.23 +  This section contains some lemmas that will be used in the proof of the
5.24 +  Hahn-Banach Theorem. In this section the following context is presumed.
5.25 +  Let \<open>E\<close> be a real vector space with a seminorm \<open>p\<close> on \<open>E\<close>. \<open>F\<close> is a
5.26 +  subspace of \<open>E\<close> and \<open>f\<close> a linear form on \<open>F\<close>. We consider a chain \<open>c\<close> of
5.27 +  norm-preserving extensions of \<open>f\<close>, such that \<open>\<Union>c = graph H h\<close>. We will
5.28 +  show some properties about the limit function \<open>h\<close>, i.e.\ the supremum of
5.29 +  the chain \<open>c\<close>.
5.30
5.31    \<^medskip>
5.32 -  Let \<open>c\<close> be a chain of norm-preserving extensions of
5.33 -  the function \<open>f\<close> and let \<open>graph H h\<close> be the supremum
5.34 -  of \<open>c\<close>.  Every element in \<open>H\<close> is member of one of the
5.35 -  elements of the chain.
5.36 +  Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and
5.37 +  let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in \<open>H\<close> is member of
5.38 +  one of the elements of the chain.
5.39  \<close>
5.40
5.41  lemmas [dest?] = chainsD
5.42 @@ -57,10 +55,10 @@
5.43
5.44  text \<open>
5.45    \<^medskip>
5.46 -  Let \<open>c\<close> be a chain of norm-preserving extensions of
5.47 -  the function \<open>f\<close> and let \<open>graph H h\<close> be the supremum
5.48 -  of \<open>c\<close>.  Every element in the domain \<open>H\<close> of the supremum
5.49 -  function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close> extends \<open>h'\<close>.
5.50 +  Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and
5.51 +  let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in the domain \<open>H\<close> of
5.52 +  the supremum function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>,
5.53 +  such that \<open>h\<close> extends \<open>h'\<close>.
5.54  \<close>
5.55
5.56  lemma some_H'h':
5.57 @@ -85,10 +83,9 @@
5.58
5.59  text \<open>
5.60    \<^medskip>
5.61 -  Any two elements \<open>x\<close> and \<open>y\<close> in the domain
5.62 -  \<open>H\<close> of the supremum function \<open>h\<close> are both in the domain
5.63 -  \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close> extends
5.64 -  \<open>h'\<close>.
5.65 +  Any two elements \<open>x\<close> and \<open>y\<close> in the domain \<open>H\<close> of the supremum function
5.66 +  \<open>h\<close> are both in the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close>
5.67 +  extends \<open>h'\<close>.
5.68  \<close>
5.69
5.70  lemma some_H'h'2:
5.71 @@ -158,8 +155,8 @@
5.72
5.73  text \<open>
5.74    \<^medskip>
5.75 -  The relation induced by the graph of the supremum of a
5.76 -  chain \<open>c\<close> is definite, i.~e.~t is the graph of a function.
5.77 +  The relation induced by the graph of the supremum of a chain \<open>c\<close> is
5.78 +  definite, i.e.\ it is the graph of a function.
5.79  \<close>
5.80
5.81  lemma sup_definite:
5.82 @@ -181,8 +178,8 @@
5.83    then obtain H2 h2 where G2_rep: "G2 = graph H2 h2"
5.84      unfolding M_def by blast
5.85
5.86 -  txt \<open>\<open>G\<^sub>1\<close> is contained in \<open>G\<^sub>2\<close>
5.87 -    or vice versa, since both \<open>G\<^sub>1\<close> and \<open>G\<^sub>2\<close> are members of \<open>c\<close>. \label{cases2}\<close>
5.88 +  txt \<open>\<open>G\<^sub>1\<close> is contained in \<open>G\<^sub>2\<close> or vice versa, since both \<open>G\<^sub>1\<close> and \<open>G\<^sub>2\<close>
5.89 +    are members of \<open>c\<close>. \label{cases2}\<close>
5.90
5.91    from cM G1 G2 consider "G1 \<subseteq> G2" | "G2 \<subseteq> G1"
5.92      by (blast dest: chainsD)
5.93 @@ -208,12 +205,11 @@
5.94
5.95  text \<open>
5.96    \<^medskip>
5.97 -  The limit function \<open>h\<close> is linear. Every element
5.98 -  \<open>x\<close> in the domain of \<open>h\<close> is in the domain of a function
5.99 -  \<open>h'\<close> in the chain of norm preserving extensions.  Furthermore,
5.100 -  \<open>h\<close> is an extension of \<open>h'\<close> so the function values of
5.101 -  \<open>x\<close> are identical for \<open>h'\<close> and \<open>h\<close>.  Finally, the
5.102 -  function \<open>h'\<close> is linear by construction of \<open>M\<close>.
5.103 +  The limit function \<open>h\<close> is linear. Every element \<open>x\<close> in the domain of \<open>h\<close>
5.104 +  is in the domain of a function \<open>h'\<close> in the chain of norm preserving
5.105 +  extensions. Furthermore, \<open>h\<close> is an extension of \<open>h'\<close> so the function
5.106 +  values of \<open>x\<close> are identical for \<open>h'\<close> and \<open>h\<close>. Finally, the function \<open>h'\<close>
5.107 +  is linear by construction of \<open>M\<close>.
5.108  \<close>
5.109
5.110  lemma sup_lf:
5.111 @@ -264,10 +260,9 @@
5.112
5.113  text \<open>
5.114    \<^medskip>
5.115 -  The limit of a non-empty chain of norm preserving
5.116 -  extensions of \<open>f\<close> is an extension of \<open>f\<close>, since every
5.117 -  element of the chain is an extension of \<open>f\<close> and the supremum
5.118 -  is an extension for every element of the chain.
5.119 +  The limit of a non-empty chain of norm preserving extensions of \<open>f\<close> is an
5.120 +  extension of \<open>f\<close>, since every element of the chain is an extension of \<open>f\<close>
5.121 +  and the supremum is an extension for every element of the chain.
5.122  \<close>
5.123
5.124  lemma sup_ext:
5.125 @@ -291,9 +286,8 @@
5.126
5.127  text \<open>
5.128    \<^medskip>
5.129 -  The domain \<open>H\<close> of the limit function is a superspace
5.130 -  of \<open>F\<close>, since \<open>F\<close> is a subset of \<open>H\<close>. The
5.131 -  existence of the \<open>0\<close> element in \<open>F\<close> and the closure
5.132 +  The domain \<open>H\<close> of the limit function is a superspace of \<open>F\<close>, since \<open>F\<close> is
5.133 +  a subset of \<open>H\<close>. The existence of the \<open>0\<close> element in \<open>F\<close> and the closure
5.134    properties follow from the fact that \<open>F\<close> is a vector space.
5.135  \<close>
5.136
5.137 @@ -317,8 +311,7 @@
5.138
5.139  text \<open>
5.140    \<^medskip>
5.141 -  The domain \<open>H\<close> of the limit function is a subspace of
5.142 -  \<open>E\<close>.
5.143 +  The domain \<open>H\<close> of the limit function is a subspace of \<open>E\<close>.
5.144  \<close>
5.145
5.146  lemma sup_subE:
5.147 @@ -374,8 +367,8 @@
5.148
5.149  text \<open>
5.150    \<^medskip>
5.151 -  The limit function is bounded by the norm \<open>p\<close> as
5.152 -  well, since all elements in the chain are bounded by \<open>p\<close>.
5.153 +  The limit function is bounded by the norm \<open>p\<close> as well, since all elements
5.154 +  in the chain are bounded by \<open>p\<close>.
5.155  \<close>
5.156
5.157  lemma sup_norm_pres:
5.158 @@ -396,10 +389,10 @@
5.159
5.160  text \<open>
5.161    \<^medskip>
5.162 -  The following lemma is a property of linear forms on real
5.163 -  vector spaces. It will be used for the lemma \<open>abs_Hahn_Banach\<close>
5.164 -  (see page \pageref{abs-Hahn_Banach}). \label{abs-ineq-iff} For real
5.165 -  vector spaces the following inequations are equivalent:
5.166 +  The following lemma is a property of linear forms on real vector spaces.
5.167 +  It will be used for the lemma \<open>abs_Hahn_Banach\<close> (see page
5.168 +  \pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces
5.169 +  the following inequality are equivalent:
5.170    \begin{center}
5.171    \begin{tabular}{lll}
5.172    \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &

     6.1 --- a/src/HOL/Hahn_Banach/Linearform.thy	Mon Nov 02 11:10:28 2015 +0100
6.2 +++ b/src/HOL/Hahn_Banach/Linearform.thy	Mon Nov 02 11:43:02 2015 +0100
6.3 @@ -9,8 +9,8 @@
6.4  begin
6.5
6.6  text \<open>
6.7 -  A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals
6.8 -  that is additive and multiplicative.
6.9 +  A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals that is
6.10 +  additive and multiplicative.
6.11  \<close>
6.12
6.13  locale linearform =

     7.1 --- a/src/HOL/Hahn_Banach/Normed_Space.thy	Mon Nov 02 11:10:28 2015 +0100
7.2 +++ b/src/HOL/Hahn_Banach/Normed_Space.thy	Mon Nov 02 11:43:02 2015 +0100
7.3 @@ -11,9 +11,9 @@
7.4  subsection \<open>Quasinorms\<close>
7.5
7.6  text \<open>
7.7 -  A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space
7.8 -  into the reals that has the following properties: it is positive
7.9 -  definite, absolute homogeneous and subadditive.
7.10 +  A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space into the reals
7.11 +  that has the following properties: it is positive definite, absolute
7.12 +  homogeneous and subadditive.
7.13  \<close>
7.14
7.15  locale seminorm =

     8.1 --- a/src/HOL/Hahn_Banach/Subspace.thy	Mon Nov 02 11:10:28 2015 +0100
8.2 +++ b/src/HOL/Hahn_Banach/Subspace.thy	Mon Nov 02 11:43:02 2015 +0100
8.3 @@ -11,9 +11,8 @@
8.4  subsection \<open>Definition\<close>
8.5
8.6  text \<open>
8.7 -  A non-empty subset \<open>U\<close> of a vector space \<open>V\<close> is a
8.8 -  \<^emph>\<open>subspace\<close> of \<open>V\<close>, iff \<open>U\<close> is closed under addition
8.9 -  and scalar multiplication.
8.10 +  A non-empty subset \<open>U\<close> of a vector space \<open>V\<close> is a \<^emph>\<open>subspace\<close> of \<open>V\<close>, iff
8.11 +  \<open>U\<close> is closed under addition and scalar multiplication.
8.12  \<close>
8.13
8.14  locale subspace =
8.15 @@ -51,9 +50,9 @@
8.16
8.17  text \<open>
8.18    \<^medskip>
8.19 -  Similar as for linear spaces, the existence of the zero
8.20 -  element in every subspace follows from the non-emptiness of the
8.21 -  carrier set and by vector space laws.
8.22 +  Similar as for linear spaces, the existence of the zero element in every
8.23 +  subspace follows from the non-emptiness of the carrier set and by vector
8.24 +  space laws.
8.25  \<close>
8.26
8.27  lemma (in subspace) zero [intro]:
8.28 @@ -140,8 +139,8 @@
8.29  subsection \<open>Linear closure\<close>
8.30
8.31  text \<open>
8.32 -  The \<^emph>\<open>linear closure\<close> of a vector \<open>x\<close> is the set of all
8.33 -  scalar multiples of \<open>x\<close>.
8.34 +  The \<^emph>\<open>linear closure\<close> of a vector \<open>x\<close> is the set of all scalar multiples
8.35 +  of \<open>x\<close>.
8.36  \<close>
8.37
8.38  definition lin :: "('a::{minus,plus,zero}) \<Rightarrow> 'a set"
8.39 @@ -227,8 +226,8 @@
8.40  subsection \<open>Sum of two vectorspaces\<close>
8.41
8.42  text \<open>
8.43 -  The \<^emph>\<open>sum\<close> of two vectorspaces \<open>U\<close> and \<open>V\<close> is the
8.44 -  set of all sums of elements from \<open>U\<close> and \<open>V\<close>.
8.45 +  The \<^emph>\<open>sum\<close> of two vectorspaces \<open>U\<close> and \<open>V\<close> is the set of all sums of
8.46 +  elements from \<open>U\<close> and \<open>V\<close>.
8.47  \<close>
8.48
8.49  lemma sum_def: "U + V = {u + v | u v. u \<in> U \<and> v \<in> V}"
8.50 @@ -329,10 +328,10 @@
8.51  subsection \<open>Direct sums\<close>
8.52
8.53  text \<open>
8.54 -  The sum of \<open>U\<close> and \<open>V\<close> is called \<^emph>\<open>direct\<close>, iff the
8.55 -  zero element is the only common element of \<open>U\<close> and \<open>V\<close>. For every element \<open>x\<close> of the direct sum of \<open>U\<close> and
8.56 -  \<open>V\<close> the decomposition in \<open>x = u + v\<close> with
8.57 -  \<open>u \<in> U\<close> and \<open>v \<in> V\<close> is unique.
8.58 +  The sum of \<open>U\<close> and \<open>V\<close> is called \<^emph>\<open>direct\<close>, iff the zero element is the
8.59 +  only common element of \<open>U\<close> and \<open>V\<close>. For every element \<open>x\<close> of the direct
8.60 +  sum of \<open>U\<close> and \<open>V\<close> the decomposition in \<open>x = u + v\<close> with \<open>u \<in> U\<close> and
8.61 +  \<open>v \<in> V\<close> is unique.
8.62  \<close>
8.63
8.64  lemma decomp:
8.65 @@ -377,12 +376,10 @@
8.66  qed
8.67
8.68  text \<open>
8.69 -  An application of the previous lemma will be used in the proof of
8.70 -  the Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any
8.71 -  element \<open>y + a \<cdot> x\<^sub>0\<close> of the direct sum of a
8.72 -  vectorspace \<open>H\<close> and the linear closure of \<open>x\<^sub>0\<close>
8.73 -  the components \<open>y \<in> H\<close> and \<open>a\<close> are uniquely
8.74 -  determined.
8.75 +  An application of the previous lemma will be used in the proof of the
8.76 +  Hahn-Banach Theorem (see page \pageref{decomp-H-use}): for any element
8.77 +  \<open>y + a \<cdot> x\<^sub>0\<close> of the direct sum of a vectorspace \<open>H\<close> and the linear closure
8.78 +  of \<open>x\<^sub>0\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are uniquely determined.
8.79  \<close>
8.80
8.81  lemma decomp_H':
8.82 @@ -436,10 +433,9 @@
8.83  qed
8.84
8.85  text \<open>
8.86 -  Since for any element \<open>y + a \<cdot> x'\<close> of the direct sum of a
8.87 -  vectorspace \<open>H\<close> and the linear closure of \<open>x'\<close> the
8.88 -  components \<open>y \<in> H\<close> and \<open>a\<close> are unique, it follows from
8.89 -  \<open>y \<in> H\<close> that \<open>a = 0\<close>.
8.90 +  Since for any element \<open>y + a \<cdot> x'\<close> of the direct sum of a vectorspace \<open>H\<close>
8.91 +  and the linear closure of \<open>x'\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are unique,
8.92 +  it follows from \<open>y \<in> H\<close> that \<open>a = 0\<close>.
8.93  \<close>
8.94
8.95  lemma decomp_H'_H:
8.96 @@ -464,9 +460,8 @@
8.97  qed
8.98
8.99  text \<open>
8.100 -  The components \<open>y \<in> H\<close> and \<open>a\<close> in \<open>y + a \<cdot> x'\<close>
8.101 -  are unique, so the function \<open>h'\<close> defined by
8.102 -  \<open>h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>\<close> is definite.
8.103 +  The components \<open>y \<in> H\<close> and \<open>a\<close> in \<open>y + a \<cdot> x'\<close> are unique, so the function
8.104 +  \<open>h'\<close> defined by \<open>h' (y + a \<cdot> x') = h y + a \<cdot> \<xi>\<close> is definite.
8.105  \<close>
8.106
8.107  lemma h'_definite:

     9.1 --- a/src/HOL/Hahn_Banach/Vector_Space.thy	Mon Nov 02 11:10:28 2015 +0100
9.2 +++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Mon Nov 02 11:43:02 2015 +0100
9.3 @@ -11,9 +11,9 @@
9.4  subsection \<open>Signature\<close>
9.5
9.6  text \<open>
9.7 -  For the definition of real vector spaces a type @{typ 'a} of the
9.8 -  sort \<open>{plus, minus, zero}\<close> is considered, on which a real
9.9 -  scalar multiplication \<open>\<cdot>\<close> is declared.
9.10 +  For the definition of real vector spaces a type @{typ 'a} of the sort
9.11 +  \<open>{plus, minus, zero}\<close> is considered, on which a real scalar multiplication
9.12 +  \<open>\<cdot>\<close> is declared.
9.13  \<close>
9.14
9.15  consts
9.16 @@ -23,13 +23,13 @@
9.17  subsection \<open>Vector space laws\<close>
9.18
9.19  text \<open>
9.20 -  A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from
9.21 -  @{typ 'a} with the following vector space laws: The set \<open>V\<close> is
9.22 -  closed under addition and scalar multiplication, addition is
9.23 -  associative and commutative; \<open>- x\<close> is the inverse of \<open>x\<close> w.~r.~t.~addition and \<open>0\<close> is the neutral element of
9.24 -  addition.  Addition and multiplication are distributive; scalar
9.25 -  multiplication is associative and the real number \<open>1\<close> is
9.26 -  the neutral element of scalar multiplication.
9.27 +  A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from @{typ 'a} with
9.28 +  the following vector space laws: The set \<open>V\<close> is closed under addition and
9.29 +  scalar multiplication, addition is associative and commutative; \<open>- x\<close> is
9.30 +  the inverse of \<open>x\<close> wrt.\ addition and \<open>0\<close> is the neutral element of
9.31 +  addition. Addition and multiplication are distributive; scalar
9.32 +  multiplication is associative and the real number \<open>1\<close> is the neutral
9.33 +  element of scalar multiplication.
9.34  \<close>
9.35
9.36  locale vectorspace =
9.37 @@ -64,7 +64,8 @@
9.38  lemma neg_closed [iff]: "x \<in> V \<Longrightarrow> - x \<in> V"
9.39    by (simp add: negate_eq1)
9.40
9.41 -lemma add_left_commute: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)"
9.43 +  "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)"
9.44  proof -
9.45    assume xyz: "x \<in> V"  "y \<in> V"  "z \<in> V"
9.46    then have "x + (y + z) = (x + y) + z"
9.47 @@ -77,8 +78,8 @@
9.49
9.50
9.51 -text \<open>The existence of the zero element of a vector space
9.52 -  follows from the non-emptiness of carrier set.\<close>
9.53 +text \<open>The existence of the zero element of a vector space follows from the
9.54 +  non-emptiness of carrier set.\<close>
9.55
9.56  lemma zero [iff]: "0 \<in> V"
9.57  proof -
9.58 @@ -213,7 +214,8 @@
9.59    then show "x + y = x + z" by (simp only:)
9.60  qed
9.61
9.62 -lemma add_right_cancel: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)"
9.64 +    "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)"
9.66
9.68 @@ -371,4 +373,3 @@
9.69  end
9.70
9.71  end
9.72 -

    10.1 --- a/src/HOL/Hahn_Banach/document/root.tex	Mon Nov 02 11:10:28 2015 +0100
10.2 +++ b/src/HOL/Hahn_Banach/document/root.tex	Mon Nov 02 11:43:02 2015 +0100
10.3 @@ -16,7 +16,7 @@
10.4  \pagenumbering{arabic}
10.5
10.6  \title{The Hahn-Banach Theorem \\ for Real Vector Spaces}
10.7 -\author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}}
10.8 +\author{Gertrud Bauer}
10.9  \maketitle
10.10
10.11  \begin{abstract}