# HG changeset patch
# User wenzelm
# Date 1445269536 -7200
# Node ID 3590367b0ce97d26a8be407048075886f8ff1eeb
# Parent  0cc8016cc1959860cb1d7a497b4a8baa6a46f088
tuned document;

diff -r 0cc8016cc195 -r 3590367b0ce9 src/HOL/Hahn_Banach/Function_Norm.thy
--- a/src/HOL/Hahn_Banach/Function_Norm.thy	Mon Oct 19 17:19:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/Function_Norm.thy	Mon Oct 19 17:45:36 2015 +0200
@@ -12,7 +12,7 @@
 
 text \<open>
   A linear form @{text f} on a normed vector space @{text "(V, \<parallel>\<cdot>\<parallel>)"}
-  is \emph{continuous}, iff it is bounded, i.e.
+  is \<^emph>\<open>continuous\<close>, iff it is bounded, i.e.
   \begin{center}
   @{text "\<exists>c \<in> R. \<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
   \end{center}
@@ -46,7 +46,7 @@
   \begin{center}
   @{text "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
   \end{center}
-  is called the \emph{norm} of @{text f}.
+  is called the \<^emph>\<open>norm\<close> of @{text f}.
 
   For non-trivial vector spaces @{text "V \<noteq> {0}"} the norm can be
   defined as
@@ -194,7 +194,8 @@
 qed
 
 text \<open>
-  \medskip The fundamental property of function norms is:
+  \<^medskip>
+  The fundamental property of function norms is:
   \begin{center}
   @{text "\<bar>f x\<bar> \<le> \<parallel>f\<parallel> \<cdot> \<parallel>x\<parallel>"}
   \end{center}
@@ -235,7 +236,8 @@
 qed
 
 text \<open>
-  \medskip The function norm is the least positive real number for
+  \<^medskip>
+  The function norm is the least positive real number for
   which the following inequation holds:
   \begin{center}
     @{text "\<bar>f x\<bar> \<le> c \<cdot> \<parallel>x\<parallel>"}
diff -r 0cc8016cc195 -r 3590367b0ce9 src/HOL/Hahn_Banach/Function_Order.thy
--- a/src/HOL/Hahn_Banach/Function_Order.thy	Mon Oct 19 17:19:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/Function_Order.thy	Mon Oct 19 17:45:36 2015 +0200
@@ -11,7 +11,7 @@
 subsection \<open>The graph of a function\<close>
 
 text \<open>
-  We define the \emph{graph} of a (real) function @{text f} with
+  We define the \<^emph>\<open>graph\<close> of a (real) function @{text f} with
   domain @{text F} as the set
   \begin{center}
   @{text "{(x, f x). x \<in> F}"}
diff -r 0cc8016cc195 -r 3590367b0ce9 src/HOL/Hahn_Banach/Hahn_Banach.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach.thy	Mon Oct 19 17:19:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach.thy	Mon Oct 19 17:45:36 2015 +0200
@@ -15,42 +15,36 @@
 
 subsection \<open>The Hahn-Banach Theorem for vector spaces\<close>
 
+paragraph \<open>Hahn-Banach Theorem.\<close>
 text \<open>
-  \textbf{Hahn-Banach Theorem.} Let @{text F} be a subspace of a real
-  vector space @{text E}, let @{text p} be a semi-norm on @{text E},
-  and @{text f} be a linear form defined on @{text F} such that @{text
-  f} is bounded by @{text p}, i.e.  @{text "\<forall>x \<in> F. f x \<le> p x"}.  Then
-  @{text f} can be extended to a linear form @{text h} on @{text E}
-  such that @{text h} is norm-preserving, i.e. @{text h} is also
-  bounded by @{text p}.
+  Let @{text F} be a subspace of a real vector space @{text E}, let @{text
+  p} be a semi-norm on @{text E}, and @{text f} be a linear form defined on
+  @{text F} such that @{text f} is bounded by @{text p}, i.e. @{text "\<forall>x \<in>
+  F. f x \<le> p x"}. Then @{text f} can be extended to a linear form @{text h}
+  on @{text E} such that @{text h} is norm-preserving, i.e. @{text h} is
+  also bounded by @{text p}.
+\<close>
 
-  \bigskip
-  \textbf{Proof Sketch.}
-  \begin{enumerate}
-
-  \item Define @{text M} as the set of norm-preserving extensions of
+paragraph \<open>Proof Sketch.\<close>
+text \<open>
+  \<^enum> Define @{text M} as the set of norm-preserving extensions of
   @{text f} to subspaces of @{text E}. The linear forms in @{text M}
   are ordered by domain extension.
 
-  \item We show that every non-empty chain in @{text M} has an upper
+  \<^enum> We show that every non-empty chain in @{text M} has an upper
   bound in @{text M}.
 
-  \item With Zorn's Lemma we conclude that there is a maximal function
+  \<^enum> With Zorn's Lemma we conclude that there is a maximal function
   @{text g} in @{text M}.
 
-  \item The domain @{text H} of @{text g} is the whole space @{text
+  \<^enum> The domain @{text H} of @{text g} is the whole space @{text
   E}, as shown by classical contradiction:
 
-  \begin{itemize}
+    \<^item> Assuming @{text g} is not defined on whole @{text E}, it can
+    still be extended in a norm-preserving way to a super-space @{text
+    H'} of @{text H}.
 
-  \item Assuming @{text g} is not defined on whole @{text E}, it can
-  still be extended in a norm-preserving way to a super-space @{text
-  H'} of @{text H}.
-
-  \item Thus @{text g} can not be maximal. Contradiction!
-
-  \end{itemize}
-  \end{enumerate}
+    \<^item> Thus @{text g} can not be maximal. Contradiction!
 \<close>
 
 theorem Hahn_Banach:
@@ -60,7 +54,7 @@
   shows "\<exists>h. linearform E h \<and> (\<forall>x \<in> F. h x = f x) \<and> (\<forall>x \<in> E. h x \<le> p x)"
     -- \<open>Let @{text E} be a vector space, @{text F} a subspace of @{text E}, @{text p} a seminorm on @{text E},\<close>
     -- \<open>and @{text f} a linear form on @{text F} such that @{text f} is bounded by @{text p},\<close>
-    -- \<open>then @{text f} can be extended to a linear form @{text h} on @{text E} in a norm-preserving way. \skp\<close>
+    -- \<open>then @{text f} can be extended to a linear form @{text h} on @{text E} in a norm-preserving way. \<^smallskip>\<close>
 proof -
   interpret vectorspace E by fact
   interpret subspace F E by fact
@@ -104,7 +98,7 @@
     qed
   }
   then have "\<exists>g \<in> M. \<forall>x \<in> M. g \<subseteq> x \<longrightarrow> x = g"
-  -- \<open>With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \skp\<close>
+  -- \<open>With Zorn's Lemma we can conclude that there is a maximal element in @{text M}. \<^smallskip>\<close>
   proof (rule Zorn's_Lemma)
       -- \<open>We show that @{text M} is non-empty:\<close>
     show "graph F f \<in> M"
@@ -127,16 +121,16 @@
     and hp: "\<forall>x \<in> H. h x \<le> p x" unfolding M_def ..
       -- \<open>@{text g} is a norm-preserving extension of @{text f}, in other words:\<close>
       -- \<open>@{text g} is the graph of some linear form @{text h} defined on a subspace @{text H} of @{text E},\<close>
-      -- \<open>and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \skp\<close>
+      -- \<open>and @{text h} is an extension of @{text f} that is again bounded by @{text p}. \<^smallskip>\<close>
   from HE E have H: "vectorspace H"
     by (rule subspace.vectorspace)
 
   have HE_eq: "H = E"
-    -- \<open>We show that @{text h} is defined on whole @{text E} by classical contradiction. \skp\<close>
+    -- \<open>We show that @{text h} is defined on whole @{text E} by classical contradiction. \<^smallskip>\<close>
   proof (rule classical)
     assume neq: "H \<noteq> E"
       -- \<open>Assume @{text h} is not defined on whole @{text E}. Then show that @{text h} can be extended\<close>
-      -- \<open>in a norm-preserving way to a function @{text h'} with the graph @{text g'}. \skp\<close>
+      -- \<open>in a norm-preserving way to a function @{text h'} with the graph @{text g'}. \<^smallskip>\<close>
     have "\<exists>g' \<in> M. g \<subseteq> g' \<and> g \<noteq> g'"
     proof -
       from HE have "H \<subseteq> E" ..
@@ -152,7 +146,7 @@
       qed
 
       def H' \<equiv> "H + lin x'"
-        -- \<open>Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \skp\<close>
+        -- \<open>Define @{text H'} as the direct sum of @{text H} and the linear closure of @{text x'}. \<^smallskip>\<close>
       have HH': "H \<unlhd> H'"
       proof (unfold H'_def)
         from x'E have "vectorspace (lin x')" ..
@@ -164,7 +158,7 @@
           \<and> xi \<le> p (y + x') - h y"
         -- \<open>Pick a real number @{text \<xi>} that fulfills certain inequations; this will\<close>
         -- \<open>be used to establish that @{text h'} is a norm-preserving extension of @{text h}.
-           \label{ex-xi-use}\skp\<close>
+           \label{ex-xi-use}\<^smallskip>\<close>
       proof -
         from H have "\<exists>xi. \<forall>y \<in> H. - p (y + x') - h y \<le> xi
             \<and> xi \<le> p (y + x') - h y"
@@ -191,10 +185,10 @@
 
       def h' \<equiv> "\<lambda>x. let (y, a) =
           SOME (y, a). x = y + a \<cdot> x' \<and> y \<in> H in h y + a * xi"
-        -- \<open>Define the extension @{text h'} of @{text h} to @{text H'} using @{text \<xi>}. \skp\<close>
+        -- \<open>Define the extension @{text h'} of @{text h} to @{text H'} using @{text \<xi>}. \<^smallskip>\<close>
 
       have "g \<subseteq> graph H' h' \<and> g \<noteq> graph H' h'"
-        -- \<open>@{text h'} is an extension of @{text h} \dots \skp\<close>
+        -- \<open>@{text h'} is an extension of @{text h} \dots \<^smallskip>\<close>
       proof
         show "g \<subseteq> graph H' h'"
         proof -
@@ -231,7 +225,7 @@
         qed
       qed
       moreover have "graph H' h' \<in> M"
-        -- \<open>and @{text h'} is norm-preserving. \skp\<close>
+        -- \<open>and @{text h'} is norm-preserving. \<^smallskip>\<close>
       proof (unfold M_def)
         show "graph H' h' \<in> norm_pres_extensions E p F f"
         proof (rule norm_pres_extensionI2)
@@ -279,7 +273,7 @@
       ultimately show ?thesis ..
     qed
     then have "\<not> (\<forall>x \<in> M. g \<subseteq> x \<longrightarrow> g = x)" by simp
-      -- \<open>So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \skp\<close>
+      -- \<open>So the graph @{text g} of @{text h} cannot be maximal. Contradiction! \<^smallskip>\<close>
     with gx show "H = E" by contradiction
   qed
 
diff -r 0cc8016cc195 -r 3590367b0ce9 src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Mon Oct 19 17:19:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Ext_Lemmas.thy	Mon Oct 19 17:45:36 2015 +0200
@@ -24,7 +24,8 @@
   Subsequently we show some properties of this extension @{text h'} of
   @{text h}.
 
-  \medskip This lemma will be used to show the existence of a linear
+  \<^medskip>
+  This lemma will be used to show the existence of a linear
   extension of @{text f} (see page \pageref{ex-xi-use}). It is a
   consequence of the completeness of @{text \<real>}. To show
   \begin{center}
@@ -84,7 +85,8 @@
 qed
 
 text \<open>
-  \medskip The function @{text h'} is defined as a @{text "h' x = h y
+  \<^medskip>
+  The function @{text h'} is defined as a @{text "h' x = h y
   + a \<cdot> \<xi>"} where @{text "x = y + a \<cdot> \<xi>"} is a linear extension of
   @{text h} to @{text H'}.
 \<close>
@@ -190,7 +192,9 @@
   qed
 qed
 
-text \<open>\medskip The linear extension @{text h'} of @{text h}
+text \<open>
+  \<^medskip>
+  The linear extension @{text h'} of @{text h}
   is bounded by the seminorm @{text p}.\<close>
 
 lemma h'_norm_pres:
diff -r 0cc8016cc195 -r 3590367b0ce9 src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Mon Oct 19 17:19:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Mon Oct 19 17:45:36 2015 +0200
@@ -18,11 +18,13 @@
   graph H h"}.  We will show some properties about the limit function
   @{text h}, i.e.\ the supremum of the chain @{text c}.
 
-  \medskip Let @{text c} be a chain of norm-preserving extensions of
+  \<^medskip>
+  Let @{text c} be a chain of norm-preserving extensions of
   the function @{text f} and let @{text "graph H h"} be the supremum
   of @{text c}.  Every element in @{text H} is member of one of the
   elements of the chain.
 \<close>
+
 lemmas [dest?] = chainsD
 lemmas chainsE2 [elim?] = chainsD2 [elim_format]
 
@@ -54,7 +56,8 @@
 qed
 
 text \<open>
-  \medskip Let @{text c} be a chain of norm-preserving extensions of
+  \<^medskip>
+  Let @{text c} be a chain of norm-preserving extensions of
   the function @{text f} and let @{text "graph H h"} be the supremum
   of @{text c}.  Every element in the domain @{text H} of the supremum
   function is member of the domain @{text H'} of some function @{text
@@ -82,7 +85,8 @@
 qed
 
 text \<open>
-  \medskip Any two elements @{text x} and @{text y} in the domain
+  \<^medskip>
+  Any two elements @{text x} and @{text y} in the domain
   @{text H} of the supremum function @{text h} are both in the domain
   @{text H'} of some function @{text h'}, such that @{text h} extends
   @{text h'}.
@@ -154,7 +158,8 @@
 qed
 
 text \<open>
-  \medskip The relation induced by the graph of the supremum of a
+  \<^medskip>
+  The relation induced by the graph of the supremum of a
   chain @{text c} is definite, i.~e.~t is the graph of a function.
 \<close>
 
@@ -204,7 +209,8 @@
 qed
 
 text \<open>
-  \medskip The limit function @{text h} is linear. Every element
+  \<^medskip>
+  The limit function @{text h} is linear. Every element
   @{text x} in the domain of @{text h} is in the domain of a function
   @{text h'} in the chain of norm preserving extensions.  Furthermore,
   @{text h} is an extension of @{text h'} so the function values of
@@ -259,7 +265,8 @@
 qed
 
 text \<open>
-  \medskip The limit of a non-empty chain of norm preserving
+  \<^medskip>
+  The limit of a non-empty chain of norm preserving
   extensions of @{text f} is an extension of @{text f}, since every
   element of the chain is an extension of @{text f} and the supremum
   is an extension for every element of the chain.
@@ -285,7 +292,8 @@
 qed
 
 text \<open>
-  \medskip The domain @{text H} of the limit function is a superspace
+  \<^medskip>
+  The domain @{text H} of the limit function is a superspace
   of @{text F}, since @{text F} is a subset of @{text H}. The
   existence of the @{text 0} element in @{text F} and the closure
   properties follow from the fact that @{text F} is a vector space.
@@ -310,7 +318,8 @@
 qed
 
 text \<open>
-  \medskip The domain @{text H} of the limit function is a subspace of
+  \<^medskip>
+  The domain @{text H} of the limit function is a subspace of
   @{text E}.
 \<close>
 
@@ -366,7 +375,8 @@
 qed
 
 text \<open>
-  \medskip The limit function is bounded by the norm @{text p} as
+  \<^medskip>
+  The limit function is bounded by the norm @{text p} as
   well, since all elements in the chain are bounded by @{text p}.
 \<close>
 
@@ -387,7 +397,8 @@
 qed
 
 text \<open>
-  \medskip The following lemma is a property of linear forms on real
+  \<^medskip>
+  The following lemma is a property of linear forms on real
   vector spaces. It will be used for the lemma @{text abs_Hahn_Banach}
   (see page \pageref{abs-Hahn_Banach}). \label{abs-ineq-iff} For real
   vector spaces the following inequations are equivalent:
diff -r 0cc8016cc195 -r 3590367b0ce9 src/HOL/Hahn_Banach/Linearform.thy
--- a/src/HOL/Hahn_Banach/Linearform.thy	Mon Oct 19 17:19:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/Linearform.thy	Mon Oct 19 17:45:36 2015 +0200
@@ -9,7 +9,7 @@
 begin
 
 text \<open>
-  A \emph{linear form} is a function on a vector space into the reals
+  A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals
   that is additive and multiplicative.
 \<close>
 
diff -r 0cc8016cc195 -r 3590367b0ce9 src/HOL/Hahn_Banach/Normed_Space.thy
--- a/src/HOL/Hahn_Banach/Normed_Space.thy	Mon Oct 19 17:19:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/Normed_Space.thy	Mon Oct 19 17:45:36 2015 +0200
@@ -11,7 +11,7 @@
 subsection \<open>Quasinorms\<close>
 
 text \<open>
-  A \emph{seminorm} @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space
+  A \<^emph>\<open>seminorm\<close> @{text "\<parallel>\<cdot>\<parallel>"} is a function on a real vector space
   into the reals that has the following properties: it is positive
   definite, absolute homogeneous and subadditive.
 \<close>
@@ -57,7 +57,7 @@
 subsection \<open>Norms\<close>
 
 text \<open>
-  A \emph{norm} @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the
+  A \<^emph>\<open>norm\<close> @{text "\<parallel>\<cdot>\<parallel>"} is a seminorm that maps only the
   @{text 0} vector to @{text 0}.
 \<close>
 
@@ -68,8 +68,8 @@
 subsection \<open>Normed vector spaces\<close>
 
 text \<open>
-  A vector space together with a norm is called a \emph{normed
-  space}.
+  A vector space together with a norm is called a \<^emph>\<open>normed
+  space\<close>.
 \<close>
 
 locale normed_vectorspace = vectorspace + norm
diff -r 0cc8016cc195 -r 3590367b0ce9 src/HOL/Hahn_Banach/Subspace.thy
--- a/src/HOL/Hahn_Banach/Subspace.thy	Mon Oct 19 17:19:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/Subspace.thy	Mon Oct 19 17:45:36 2015 +0200
@@ -12,7 +12,7 @@
 
 text \<open>
   A non-empty subset @{text U} of a vector space @{text V} is a
-  \emph{subspace} of @{text V}, iff @{text U} is closed under addition
+  \<^emph>\<open>subspace\<close> of @{text V}, iff @{text U} is closed under addition
   and scalar multiplication.
 \<close>
 
@@ -50,7 +50,8 @@
 qed
 
 text \<open>
-  \medskip Similar as for linear spaces, the existence of the zero
+  \<^medskip>
+  Similar as for linear spaces, the existence of the zero
   element in every subspace follows from the non-emptiness of the
   carrier set and by vector space laws.
 \<close>
@@ -76,7 +77,7 @@
   from x show ?thesis by (simp add: negate_eq1)
 qed
 
-text \<open>\medskip Further derived laws: every subspace is a vector space.\<close>
+text \<open>\<^medskip> Further derived laws: every subspace is a vector space.\<close>
 
 lemma (in subspace) vectorspace [iff]:
   assumes "vectorspace V"
@@ -139,7 +140,7 @@
 subsection \<open>Linear closure\<close>
 
 text \<open>
-  The \emph{linear closure} of a vector @{text x} is the set of all
+  The \<^emph>\<open>linear closure\<close> of a vector @{text x} is the set of all
   scalar multiples of @{text x}.
 \<close>
 
@@ -226,7 +227,7 @@
 subsection \<open>Sum of two vectorspaces\<close>
 
 text \<open>
-  The \emph{sum} of two vectorspaces @{text U} and @{text V} is the
+  The \<^emph>\<open>sum\<close> of two vectorspaces @{text U} and @{text V} is the
   set of all sums of elements from @{text U} and @{text V}.
 \<close>
 
@@ -328,7 +329,7 @@
 subsection \<open>Direct sums\<close>
 
 text \<open>
-  The sum of @{text U} and @{text V} is called \emph{direct}, iff the
+  The sum of @{text U} and @{text V} is called \<^emph>\<open>direct\<close>, iff the
   zero element is the only common element of @{text U} and @{text
   V}. For every element @{text x} of the direct sum of @{text U} and
   @{text V} the decomposition in @{text "x = u + v"} with
diff -r 0cc8016cc195 -r 3590367b0ce9 src/HOL/Hahn_Banach/Vector_Space.thy
--- a/src/HOL/Hahn_Banach/Vector_Space.thy	Mon Oct 19 17:19:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/Vector_Space.thy	Mon Oct 19 17:45:36 2015 +0200
@@ -23,7 +23,7 @@
 subsection \<open>Vector space laws\<close>
 
 text \<open>
-  A \emph{vector space} is a non-empty set @{text V} of elements from
+  A \<^emph>\<open>vector space\<close> is a non-empty set @{text V} of elements from
   @{typ 'a} with the following vector space laws: The set @{text V} is
   closed under addition and scalar multiplication, addition is
   associative and commutative; @{text "- x"} is the inverse of @{text
@@ -122,7 +122,7 @@
   diff_mult_distrib1 diff_mult_distrib2
 
 
-text \<open>\medskip Further derived laws:\<close>
+text \<open>\<^medskip> Further derived laws:\<close>
 
 lemma mult_zero_left [simp]: "x \<in> V \<Longrightarrow> 0 \<cdot> x = 0"
 proof -
diff -r 0cc8016cc195 -r 3590367b0ce9 src/HOL/Hahn_Banach/document/root.tex
--- a/src/HOL/Hahn_Banach/document/root.tex	Mon Oct 19 17:19:53 2015 +0200
+++ b/src/HOL/Hahn_Banach/document/root.tex	Mon Oct 19 17:45:36 2015 +0200
@@ -8,7 +8,6 @@
 \urlstyle{rm}
 
 \newcommand{\isasymsup}{\isamath{\sup\,}}
-\newcommand{\skp}{\smallskip}
 
 
 \begin{document}