tuned whitespace;
authorwenzelm
Sun Dec 20 13:56:02 2015 +0100 (2015-12-20)
changeset 61879e4f9d8f094fe
parent 61878 fa4dbb82732f
child 61880 ff4d33058566
child 61883 c0f34fe6aa61
tuned whitespace;
src/HOL/Hahn_Banach/Function_Norm.thy
src/HOL/Hahn_Banach/Function_Order.thy
src/HOL/Hahn_Banach/Hahn_Banach.thy
src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
src/HOL/Hahn_Banach/Normed_Space.thy
src/HOL/Hahn_Banach/Subspace.thy
src/HOL/Hahn_Banach/Vector_Space.thy
src/HOL/Hahn_Banach/Zorn_Lemma.thy
     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