author wenzelm Sun Dec 20 13:56:02 2015 +0100 (2015-12-20) changeset 61879 e4f9d8f094fe parent 61878 fa4dbb82732f child 61880 ff4d33058566 child 61883 c0f34fe6aa61
tuned whitespace;
     1.1 --- a/src/HOL/Hahn_Banach/Function_Norm.thy	Sun Dec 20 13:11:47 2015 +0100
1.2 +++ b/src/HOL/Hahn_Banach/Function_Norm.thy	Sun Dec 20 13:56:02 2015 +0100
1.3 @@ -11,8 +11,8 @@
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> is \<^emph>\<open>continuous\<close>,
1.8 -  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>, iff
1.10 +  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 @@ -52,20 +52,20 @@
1.15    \<open>\<parallel>f\<parallel> = \<sup>x \<noteq> 0. \<bar>f x\<bar> / \<parallel>x\<parallel>\<close>
1.16    \end{center}
1.17
1.18 -  For the case \<open>V = {0}\<close> the supremum would be taken from an empty set.
1.19 -  Since \<open>\<real>\<close> is unbounded, there would be no supremum. To avoid this
1.20 -  situation it must be guaranteed that there is an element in this set. This
1.21 -  element must be \<open>{} \<ge> 0\<close> so that \<open>fn_norm\<close> has the norm properties.
1.22 -  Furthermore it does not have to change the norm in all other cases, so it
1.23 -  must be \<open>0\<close>, as all other elements are \<open>{} \<ge> 0\<close>.
1.24 +  For the case \<open>V = {0}\<close> the supremum would be taken from an empty set. Since
1.25 +  \<open>\<real>\<close> is unbounded, there would be no supremum. To avoid this situation it
1.26 +  must be guaranteed that there is an element in this set. This element must
1.27 +  be \<open>{} \<ge> 0\<close> so that \<open>fn_norm\<close> has the norm properties. Furthermore it does
1.28 +  not have to change the norm in all other cases, so it must be \<open>0\<close>, as all
1.29 +  other elements are \<open>{} \<ge> 0\<close>.
1.30
1.31    Thus we define the set \<open>B\<close> where the supremum is taken from as follows:
1.32    \begin{center}
1.33    \<open>{0} \<union> {\<bar>f x\<bar> / \<parallel>x\<parallel>. x \<noteq> 0 \<and> x \<in> F}\<close>
1.34    \end{center}
1.35
1.36 -  \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the supremum exists
1.37 -  (otherwise it is undefined).
1.38 +  \<open>fn_norm\<close> is equal to the supremum of \<open>B\<close>, if the supremum exists (otherwise
1.39 +  it is undefined).
1.40  \<close>
1.41
1.42  locale fn_norm =

     2.1 --- a/src/HOL/Hahn_Banach/Function_Order.thy	Sun Dec 20 13:11:47 2015 +0100
2.2 +++ b/src/HOL/Hahn_Banach/Function_Order.thy	Sun Dec 20 13:56:02 2015 +0100
2.3 @@ -11,14 +11,12 @@
2.4  subsection \<open>The graph of a function\<close>
2.5
2.6  text \<open>
2.7 -  We define the \<^emph>\<open>graph\<close> of a (real) function \<open>f\<close> with
2.8 -  domain \<open>F\<close> as the set
2.9 +  We define the \<^emph>\<open>graph\<close> of a (real) function \<open>f\<close> with domain \<open>F\<close> as the set
2.10    \begin{center}
2.11    \<open>{(x, f x). x \<in> F}\<close>
2.12    \end{center}
2.13 -  So we are modeling partial functions by specifying the domain and
2.14 -  the mapping function. We use the term function'' also for its
2.15 -  graph.
2.16 +  So we are modeling partial functions by specifying the domain and the
2.17 +  mapping function. We use the term function'' also for its graph.
2.18  \<close>
2.19
2.20  type_synonym 'a graph = "('a \<times> real) set"
2.21 @@ -41,8 +39,8 @@
2.22  subsection \<open>Functions ordered by domain extension\<close>
2.23
2.24  text \<open>
2.25 -  A function \<open>h'\<close> is an extension of \<open>h\<close>, iff the graph of
2.26 -  \<open>h\<close> is a subset of the graph of \<open>h'\<close>.
2.27 +  A function \<open>h'\<close> is an extension of \<open>h\<close>, iff the graph of \<open>h\<close> is a subset of
2.28 +  the graph of \<open>h'\<close>.
2.29  \<close>
2.30
2.31  lemma graph_extI:
2.32 @@ -93,8 +91,8 @@
2.33  subsection \<open>Norm-preserving extensions of a function\<close>
2.34
2.35  text \<open>
2.36 -  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.37 -  set of all linear extensions of \<open>f\<close>, to superspaces \<open>H\<close> of \<open>F\<close>, which are
2.38 +  Given a linear form \<open>f\<close> on the space \<open>F\<close> and a seminorm \<open>p\<close> on \<open>E\<close>. The set
2.39 +  of all linear extensions of \<open>f\<close>, to superspaces \<open>H\<close> of \<open>F\<close>, which are
2.40    bounded by \<open>p\<close>, is defined as follows.
2.41  \<close>
2.42

     3.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sun Dec 20 13:11:47 2015 +0100
3.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Sun Dec 20 13:56:02 2015 +0100
3.3 @@ -18,28 +18,26 @@
3.4
3.5  paragraph \<open>Hahn-Banach Theorem.\<close>
3.6  text \<open>
3.7 -  Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm
3.8 -  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.9 -  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.10 -  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.11 -  by \<open>p\<close>.
3.12 +  Let \<open>F\<close> be a subspace of a real vector space \<open>E\<close>, let \<open>p\<close> be a semi-norm on
3.13 +  \<open>E\<close>, and \<open>f\<close> be a linear form defined on \<open>F\<close> such that \<open>f\<close> is bounded by
3.14 +  \<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 form \<open>h\<close>
3.15 +  on \<open>E\<close> such that \<open>h\<close> is norm-preserving, i.e. \<open>h\<close> is also bounded by \<open>p\<close>.
3.16  \<close>
3.17
3.18  paragraph \<open>Proof Sketch.\<close>
3.19  text \<open>
3.20 -  \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of \<open>f\<close> to subspaces
3.21 -  of \<open>E\<close>. The linear forms in \<open>M\<close> are ordered by domain extension.
3.22 +  \<^enum> Define \<open>M\<close> as the set of norm-preserving extensions of \<open>f\<close> to subspaces of
3.23 +  \<open>E\<close>. The linear forms in \<open>M\<close> are ordered by domain extension.
3.24
3.25    \<^enum> We show that every non-empty chain in \<open>M\<close> has an upper bound in \<open>M\<close>.
3.26
3.27 -  \<^enum> With Zorn's Lemma we conclude that there is a maximal function \<open>g\<close> in
3.28 -  \<open>M\<close>.
3.29 +  \<^enum> With Zorn's Lemma we conclude that there is a maximal function \<open>g\<close> in \<open>M\<close>.
3.30
3.31    \<^enum> The domain \<open>H\<close> of \<open>g\<close> is the whole space \<open>E\<close>, as shown by classical
3.32    contradiction:
3.33
3.34 -    \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can still be extended in
3.35 -    a norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>.
3.36 +    \<^item> Assuming \<open>g\<close> is not defined on whole \<open>E\<close>, it can still be extended in a
3.37 +    norm-preserving way to a super-space \<open>H'\<close> of \<open>H\<close>.
3.38
3.39      \<^item> Thus \<open>g\<close> can not be maximal. Contradiction!
3.40  \<close>
3.41 @@ -292,14 +290,13 @@
3.42
3.43  text \<open>
3.44    The following alternative formulation of the Hahn-Banach
3.45 -  Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear form
3.46 -  \<open>f\<close> and a seminorm \<open>p\<close> the following inequality are
3.47 -  equivalent:\footnote{This was shown in lemma @{thm [source] abs_ineq_iff}
3.48 -  (see page \pageref{abs-ineq-iff}).}
3.49 +  Theorem\label{abs-Hahn-Banach} uses the fact that for a real linear form \<open>f\<close>
3.50 +  and a seminorm \<open>p\<close> the following inequality are equivalent:\footnote{This
3.51 +  was shown in lemma @{thm [source] abs_ineq_iff} (see page
3.52 +  \pageref{abs-ineq-iff}).}
3.53    \begin{center}
3.54    \begin{tabular}{lll}
3.55 -  \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &
3.56 -  \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\
3.57 +  \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and & \<open>\<forall>x \<in> H. h x \<le> p x\<close> \\
3.58    \end{tabular}
3.59    \end{center}
3.60  \<close>
3.61 @@ -336,9 +333,8 @@
3.62  subsection \<open>The Hahn-Banach Theorem for normed spaces\<close>
3.63
3.64  text \<open>
3.65 -  Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a norm space \<open>E\<close>,
3.66 -  can be extended to a continuous linear form \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> =
3.67 -  \<parallel>g\<parallel>\<close>.
3.68 +  Every continuous linear form \<open>f\<close> on a subspace \<open>F\<close> of a norm space \<open>E\<close>, can
3.69 +  be extended to a continuous linear form \<open>g\<close> on \<open>E\<close> such that \<open>\<parallel>f\<parallel> = \<parallel>g\<parallel>\<close>.
3.70  \<close>
3.71
3.72  theorem norm_Hahn_Banach:
3.73 @@ -420,10 +416,10 @@
3.74           OF F_norm, folded B_def fn_norm_def])
3.75    qed
3.76
3.77 -  txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded by \<open>p\<close> we
3.78 -    can apply the Hahn-Banach Theorem for real vector spaces. So \<open>f\<close> can be
3.79 -    extended in a norm-preserving way to some function \<open>g\<close> on the whole
3.80 -    vector space \<open>E\<close>.\<close>
3.81 +  txt \<open>Using the fact that \<open>p\<close> is a seminorm and \<open>f\<close> is bounded by \<open>p\<close> we can
3.82 +    apply the Hahn-Banach Theorem for real vector spaces. So \<open>f\<close> can be
3.83 +    extended in a norm-preserving way to some function \<open>g\<close> on the whole vector
3.84 +    space \<open>E\<close>.\<close>
3.85
3.86    with E FE linearform q obtain g where
3.87        linearformE: "linearform E g"

     4.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Sun Dec 20 13:11:47 2015 +0100
4.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Sun Dec 20 13:56:02 2015 +0100
4.3 @@ -9,14 +9,13 @@
4.4  begin
4.5
4.6  text \<open>
4.7 -  In this section the following context is presumed. Let \<open>E\<close> be a real
4.8 -  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.9 -  a linear function on \<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>
4.11 -  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.12 -  = 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.13 -  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.14 -  for a certain \<open>\<xi>\<close>.
4.15 +  In this section the following context is presumed. Let \<open>E\<close> be a real vector
4.16 +  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
4.17 +  function on \<open>F\<close>. We consider a subspace \<open>H\<close> of \<open>E\<close> that is a superspace of
4.18 +  \<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 an
4.19 +  element in \<open>E - H\<close>. \<open>H\<close> is extended to the direct sum \<open>H' = H + lin x\<^sub>0\<close>, so
4.20 +  for any \<open>x \<in> H'\<close> the decomposition of \<open>x = y + a \<cdot> x\<close> with \<open>y \<in> H\<close> is
4.21 +  unique. \<open>h'\<close> is defined on \<open>H'\<close> by \<open>h' x = h y + a \<cdot> \<xi>\<close> for a certain \<open>\<xi>\<close>.
4.22
4.23    Subsequently we show some properties of this extension \<open>h'\<close> of \<open>h\<close>.
4.24
4.25 @@ -82,8 +81,8 @@
4.26
4.27  text \<open>
4.28    \<^medskip>
4.29 -  The function \<open>h'\<close> is defined as a \<open>h' x = h y + a \<cdot> \<xi>\<close> where
4.30 -  \<open>x = y + a \<cdot> \<xi>\<close> is a linear extension of \<open>h\<close> to \<open>H'\<close>.
4.31 +  The function \<open>h'\<close> is defined as a \<open>h' x = h y + a \<cdot> \<xi>\<close> where \<open>x = y + a \<cdot> \<xi>\<close>
4.32 +  is a linear extension of \<open>h\<close> to \<open>H'\<close>.
4.33  \<close>
4.34
4.35  lemma h'_lf:

     5.1 --- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sun Dec 20 13:11:47 2015 +0100
5.2 +++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sun Dec 20 13:56:02 2015 +0100
5.3 @@ -10,17 +10,16 @@
5.4
5.5  text \<open>
5.6    This section contains some lemmas that will be used in the proof of the
5.7 -  Hahn-Banach Theorem. In this section the following context is presumed.
5.8 -  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.9 -  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.10 -  norm-preserving extensions of \<open>f\<close>, such that \<open>\<Union>c = graph H h\<close>. We will
5.11 -  show some properties about the limit function \<open>h\<close>, i.e.\ the supremum of
5.12 -  the chain \<open>c\<close>.
5.13 +  Hahn-Banach Theorem. In this section the following context is presumed. Let
5.14 +  \<open>E\<close> be a real vector space with a seminorm \<open>p\<close> on \<open>E\<close>. \<open>F\<close> is a subspace of
5.15 +  \<open>E\<close> and \<open>f\<close> a linear form on \<open>F\<close>. We consider a chain \<open>c\<close> of norm-preserving
5.16 +  extensions of \<open>f\<close>, such that \<open>\<Union>c = graph H h\<close>. We will show some properties
5.17 +  about the limit function \<open>h\<close>, i.e.\ the supremum of the chain \<open>c\<close>.
5.18
5.19    \<^medskip>
5.20 -  Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and
5.21 -  let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in \<open>H\<close> is member of
5.22 -  one of the elements of the chain.
5.23 +  Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and let
5.24 +  \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in \<open>H\<close> is member of one of
5.25 +  the elements of the chain.
5.26  \<close>
5.27
5.28  lemmas [dest?] = chainsD
5.29 @@ -55,10 +54,10 @@
5.30
5.31  text \<open>
5.32    \<^medskip>
5.33 -  Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and
5.34 -  let \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in the domain \<open>H\<close> of
5.35 -  the supremum function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>,
5.36 -  such that \<open>h\<close> extends \<open>h'\<close>.
5.37 +  Let \<open>c\<close> be a chain of norm-preserving extensions of the function \<open>f\<close> and let
5.38 +  \<open>graph H h\<close> be the supremum of \<open>c\<close>. Every element in the domain \<open>H\<close> of the
5.39 +  supremum function is member of the domain \<open>H'\<close> of some function \<open>h'\<close>, such
5.40 +  that \<open>h\<close> extends \<open>h'\<close>.
5.41  \<close>
5.42
5.43  lemma some_H'h':
5.44 @@ -83,9 +82,9 @@
5.45
5.46  text \<open>
5.47    \<^medskip>
5.48 -  Any two elements \<open>x\<close> and \<open>y\<close> in the domain \<open>H\<close> of the supremum function
5.49 -  \<open>h\<close> are both in the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close>
5.50 -  extends \<open>h'\<close>.
5.51 +  Any two elements \<open>x\<close> and \<open>y\<close> in the domain \<open>H\<close> of the supremum function \<open>h\<close>
5.52 +  are both in the domain \<open>H'\<close> of some function \<open>h'\<close>, such that \<open>h\<close> extends
5.53 +  \<open>h'\<close>.
5.54  \<close>
5.55
5.56  lemma some_H'h'2:
5.57 @@ -99,8 +98,8 @@
5.58      \<and> linearform H' h' \<and> H' \<unlhd> E \<and> F \<unlhd> H'
5.59      \<and> graph F f \<subseteq> graph H' h' \<and> (\<forall>x \<in> H'. h' x \<le> p x)"
5.60  proof -
5.61 -  txt \<open>\<open>y\<close> is in the domain \<open>H''\<close> of some function \<open>h''\<close>,
5.62 -  such that \<open>h\<close> extends \<open>h''\<close>.\<close>
5.63 +  txt \<open>\<open>y\<close> is in the domain \<open>H''\<close> of some function \<open>h''\<close>, such that \<open>h\<close>
5.64 +    extends \<open>h''\<close>.\<close>
5.65
5.66    from M cM u and y obtain H' h' where
5.67        y_hy: "(y, h y) \<in> graph H' h'"
5.68 @@ -121,10 +120,9 @@
5.69        "graph F f \<subseteq> graph H'' h''"  "\<forall>x \<in> H''. h'' x \<le> p x"
5.70      by (rule some_H'h't [elim_format]) blast
5.71
5.72 -  txt \<open>Since both \<open>h'\<close> and \<open>h''\<close> are elements of the chain,
5.73 -    \<open>h''\<close> is an extension of \<open>h'\<close> or vice versa. Thus both
5.74 -    \<open>x\<close> and \<open>y\<close> are contained in the greater
5.75 -    one. \label{cases1}\<close>
5.76 +  txt \<open>Since both \<open>h'\<close> and \<open>h''\<close> are elements of the chain, \<open>h''\<close> is an
5.77 +    extension of \<open>h'\<close> or vice versa. Thus both \<open>x\<close> and \<open>y\<close> are contained in
5.78 +    the greater one. \label{cases1}\<close>
5.79
5.80    from cM c'' c' consider "graph H'' h'' \<subseteq> graph H' h'" | "graph H' h' \<subseteq> graph H'' h''"
5.81      by (blast dest: chainsD)
5.82 @@ -205,11 +203,11 @@
5.83
5.84  text \<open>
5.85    \<^medskip>
5.86 -  The limit function \<open>h\<close> is linear. Every element \<open>x\<close> in the domain of \<open>h\<close>
5.87 -  is in the domain of a function \<open>h'\<close> in the chain of norm preserving
5.88 -  extensions. Furthermore, \<open>h\<close> is an extension of \<open>h'\<close> so the function
5.89 -  values of \<open>x\<close> are identical for \<open>h'\<close> and \<open>h\<close>. Finally, the function \<open>h'\<close>
5.90 -  is linear by construction of \<open>M\<close>.
5.91 +  The limit function \<open>h\<close> is linear. Every element \<open>x\<close> in the domain of \<open>h\<close> is
5.92 +  in the domain of a function \<open>h'\<close> in the chain of norm preserving extensions.
5.93 +  Furthermore, \<open>h\<close> is an extension of \<open>h'\<close> so the function values of \<open>x\<close> are
5.94 +  identical for \<open>h'\<close> and \<open>h\<close>. Finally, the function \<open>h'\<close> is linear by
5.95 +  construction of \<open>M\<close>.
5.96  \<close>
5.97
5.98  lemma sup_lf:
5.99 @@ -286,8 +284,8 @@
5.100
5.101  text \<open>
5.102    \<^medskip>
5.103 -  The domain \<open>H\<close> of the limit function is a superspace of \<open>F\<close>, since \<open>F\<close> is
5.104 -  a subset of \<open>H\<close>. The existence of the \<open>0\<close> element in \<open>F\<close> and the closure
5.105 +  The domain \<open>H\<close> of the limit function is a superspace of \<open>F\<close>, since \<open>F\<close> is a
5.106 +  subset of \<open>H\<close>. The existence of the \<open>0\<close> element in \<open>F\<close> and the closure
5.107    properties follow from the fact that \<open>F\<close> is a vector space.
5.108  \<close>
5.109
5.110 @@ -367,8 +365,8 @@
5.111
5.112  text \<open>
5.113    \<^medskip>
5.114 -  The limit function is bounded by the norm \<open>p\<close> as well, since all elements
5.115 -  in the chain are bounded by \<open>p\<close>.
5.116 +  The limit function is bounded by the norm \<open>p\<close> as well, since all elements in
5.117 +  the chain are bounded by \<open>p\<close>.
5.118  \<close>
5.119
5.120  lemma sup_norm_pres:
5.121 @@ -389,10 +387,10 @@
5.122
5.123  text \<open>
5.124    \<^medskip>
5.125 -  The following lemma is a property of linear forms on real vector spaces.
5.126 -  It will be used for the lemma \<open>abs_Hahn_Banach\<close> (see page
5.127 -  \pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces
5.128 -  the following inequality are equivalent:
5.129 +  The following lemma is a property of linear forms on real vector spaces. It
5.130 +  will be used for the lemma \<open>abs_Hahn_Banach\<close> (see page
5.131 +  \pageref{abs-Hahn-Banach}). \label{abs-ineq-iff} For real vector spaces the
5.132 +  following inequality are equivalent:
5.133    \begin{center}
5.134    \begin{tabular}{lll}
5.135    \<open>\<forall>x \<in> H. \<bar>h x\<bar> \<le> p x\<close> & and &

     6.1 --- a/src/HOL/Hahn_Banach/Normed_Space.thy	Sun Dec 20 13:11:47 2015 +0100
6.2 +++ b/src/HOL/Hahn_Banach/Normed_Space.thy	Sun Dec 20 13:56:02 2015 +0100
6.3 @@ -11,9 +11,9 @@
6.4  subsection \<open>Quasinorms\<close>
6.5
6.6  text \<open>
6.7 -  A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space into the reals
6.8 -  that has the following properties: it is positive definite, absolute
6.9 -  homogeneous and subadditive.
6.10 +  A \<^emph>\<open>seminorm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a function on a real vector space into the reals that
6.11 +  has the following properties: it is positive definite, absolute homogeneous
6.12 +  and subadditive.
6.13  \<close>
6.14
6.15  locale seminorm =
6.16 @@ -57,8 +57,7 @@
6.17  subsection \<open>Norms\<close>
6.18
6.19  text \<open>
6.20 -  A \<^emph>\<open>norm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a seminorm that maps only the
6.21 -  \<open>0\<close> vector to \<open>0\<close>.
6.22 +  A \<^emph>\<open>norm\<close> \<open>\<parallel>\<cdot>\<parallel>\<close> is a seminorm that maps only the \<open>0\<close> vector to \<open>0\<close>.
6.23  \<close>
6.24
6.25  locale norm = seminorm +
6.26 @@ -68,8 +67,7 @@
6.27  subsection \<open>Normed vector spaces\<close>
6.28
6.29  text \<open>
6.30 -  A vector space together with a norm is called a \<^emph>\<open>normed
6.31 -  space\<close>.
6.32 +  A vector space together with a norm is called a \<^emph>\<open>normed space\<close>.
6.33  \<close>
6.34
6.35  locale normed_vectorspace = vectorspace + norm

     7.1 --- a/src/HOL/Hahn_Banach/Subspace.thy	Sun Dec 20 13:11:47 2015 +0100
7.2 +++ b/src/HOL/Hahn_Banach/Subspace.thy	Sun Dec 20 13:56:02 2015 +0100
7.3 @@ -139,8 +139,8 @@
7.4  subsection \<open>Linear closure\<close>
7.5
7.6  text \<open>
7.7 -  The \<^emph>\<open>linear closure\<close> of a vector \<open>x\<close> is the set of all scalar multiples
7.8 -  of \<open>x\<close>.
7.9 +  The \<^emph>\<open>linear closure\<close> of a vector \<open>x\<close> is the set of all scalar multiples of
7.10 +  \<open>x\<close>.
7.11  \<close>
7.12
7.13  definition lin :: "('a::{minus,plus,zero}) \<Rightarrow> 'a set"
7.14 @@ -318,7 +318,7 @@
7.15    qed
7.16  qed
7.17
7.18 -text\<open>The sum of two subspaces is a vectorspace.\<close>
7.19 +text \<open>The sum of two subspaces is a vectorspace.\<close>
7.20
7.21  lemma sum_vs [intro?]:
7.22      "U \<unlhd> E \<Longrightarrow> V \<unlhd> E \<Longrightarrow> vectorspace E \<Longrightarrow> vectorspace (U + V)"
7.23 @@ -328,10 +328,10 @@
7.24  subsection \<open>Direct sums\<close>
7.25
7.26  text \<open>
7.27 -  The sum of \<open>U\<close> and \<open>V\<close> is called \<^emph>\<open>direct\<close>, iff the zero element is the
7.28 -  only common element of \<open>U\<close> and \<open>V\<close>. For every element \<open>x\<close> of the direct
7.29 -  sum of \<open>U\<close> and \<open>V\<close> the decomposition in \<open>x = u + v\<close> with \<open>u \<in> U\<close> and
7.30 -  \<open>v \<in> V\<close> is unique.
7.31 +  The sum of \<open>U\<close> and \<open>V\<close> is called \<^emph>\<open>direct\<close>, iff the zero element is the only
7.32 +  common element of \<open>U\<close> and \<open>V\<close>. For every element \<open>x\<close> of the direct sum of
7.33 +  \<open>U\<close> and \<open>V\<close> the decomposition in \<open>x = u + v\<close> with \<open>u \<in> U\<close> and \<open>v \<in> V\<close> is
7.34 +  unique.
7.35  \<close>
7.36
7.37  lemma decomp:
7.38 @@ -434,8 +434,8 @@
7.39
7.40  text \<open>
7.41    Since for any element \<open>y + a \<cdot> x'\<close> of the direct sum of a vectorspace \<open>H\<close>
7.42 -  and the linear closure of \<open>x'\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are unique,
7.43 -  it follows from \<open>y \<in> H\<close> that \<open>a = 0\<close>.
7.44 +  and the linear closure of \<open>x'\<close> the components \<open>y \<in> H\<close> and \<open>a\<close> are unique, it
7.45 +  follows from \<open>y \<in> H\<close> that \<open>a = 0\<close>.
7.46  \<close>
7.47
7.48  lemma decomp_H'_H:

     8.1 --- a/src/HOL/Hahn_Banach/Vector_Space.thy	Sun Dec 20 13:11:47 2015 +0100
8.2 +++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Sun Dec 20 13:56:02 2015 +0100
8.3 @@ -23,13 +23,13 @@
8.4  subsection \<open>Vector space laws\<close>
8.5
8.6  text \<open>
8.7 -  A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from @{typ 'a} with
8.8 -  the following vector space laws: The set \<open>V\<close> is closed under addition and
8.9 -  scalar multiplication, addition is associative and commutative; \<open>- x\<close> is
8.10 -  the inverse of \<open>x\<close> wrt.\ addition and \<open>0\<close> is the neutral element of
8.11 -  addition. Addition and multiplication are distributive; scalar
8.12 -  multiplication is associative and the real number \<open>1\<close> is the neutral
8.13 -  element of scalar multiplication.
8.14 +  A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from @{typ 'a} with the
8.15 +  following vector space laws: The set \<open>V\<close> is closed under addition and scalar
8.16 +  multiplication, addition is associative and commutative; \<open>- x\<close> is the
8.17 +  inverse of \<open>x\<close> wrt.\ addition and \<open>0\<close> is the neutral element of addition.
8.18 +  Addition and multiplication are distributive; scalar multiplication is
8.19 +  associative and the real number \<open>1\<close> is the neutral element of scalar
8.20 +  multiplication.
8.21  \<close>
8.22
8.23  locale vectorspace =
8.24 @@ -78,8 +78,10 @@
8.25  lemmas add_ac = add_assoc add_commute add_left_commute
8.26
8.27
8.28 -text \<open>The existence of the zero element of a vector space follows from the
8.29 -  non-emptiness of carrier set.\<close>
8.30 +text \<open>
8.31 +  The existence of the zero element of a vector space follows from the
8.32 +  non-emptiness of carrier set.
8.33 +\<close>
8.34
8.35  lemma zero [iff]: "0 \<in> V"
8.36  proof -

     9.1 --- a/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Sun Dec 20 13:11:47 2015 +0100
9.2 +++ b/src/HOL/Hahn_Banach/Zorn_Lemma.thy	Sun Dec 20 13:56:02 2015 +0100
9.3 @@ -9,13 +9,13 @@
9.4  begin
9.5
9.6  text \<open>
9.7 -  Zorn's Lemmas states: if every linear ordered subset of an ordered
9.8 -  set \<open>S\<close> has an upper bound in \<open>S\<close>, then there exists a
9.9 -  maximal element in \<open>S\<close>.  In our application, \<open>S\<close> is a
9.10 -  set of sets ordered by set inclusion. Since the union of a chain of
9.11 -  sets is an upper bound for all elements of the chain, the conditions
9.12 -  of Zorn's lemma can be modified: if \<open>S\<close> is non-empty, it
9.13 -  suffices to show that for every non-empty chain \<open>c\<close> in \<open>S\<close> the union of \<open>c\<close> also lies in \<open>S\<close>.
9.14 +  Zorn's Lemmas states: if every linear ordered subset of an ordered set \<open>S\<close>
9.15 +  has an upper bound in \<open>S\<close>, then there exists a maximal element in \<open>S\<close>. In
9.16 +  our application, \<open>S\<close> is a set of sets ordered by set inclusion. Since the
9.17 +  union of a chain of sets is an upper bound for all elements of the chain,
9.18 +  the conditions of Zorn's lemma can be modified: if \<open>S\<close> is non-empty, it
9.19 +  suffices to show that for every non-empty chain \<open>c\<close> in \<open>S\<close> the union of \<open>c\<close>
9.20 +  also lies in \<open>S\<close>.
9.21  \<close>
9.22
9.23  theorem Zorn's_Lemma:
9.24 @@ -28,16 +28,14 @@
9.25      fix c assume "c \<in> chains S"
9.26      show "\<exists>y \<in> S. \<forall>z \<in> c. z \<subseteq> y"
9.27      proof cases
9.28 -
9.29 -      txt \<open>If \<open>c\<close> is an empty chain, then every element in
9.30 -        \<open>S\<close> is an upper bound of \<open>c\<close>.\<close>
9.31 +      txt \<open>If \<open>c\<close> is an empty chain, then every element in \<open>S\<close> is an upper
9.32 +        bound of \<open>c\<close>.\<close>
9.33
9.34        assume "c = {}"
9.35        with aS show ?thesis by fast
9.36
9.37 -      txt \<open>If \<open>c\<close> is non-empty, then \<open>\<Union>c\<close> is an upper
9.38 -        bound of \<open>c\<close>, lying in \<open>S\<close>.\<close>
9.39 -
9.40 +      txt \<open>If \<open>c\<close> is non-empty, then \<open>\<Union>c\<close> is an upper bound of \<open>c\<close>, lying in
9.41 +        \<open>S\<close>.\<close>
9.42      next
9.43        assume "c \<noteq> {}"
9.44        show ?thesis