author wenzelm Mon, 25 Oct 1999 19:24:43 +0200 changeset 7927 b50446a33c16 parent 7926 9c20924de52c child 7928 06a11f8cf573
update by Gertrud Bauer;
 src/HOL/Real/HahnBanach/FunctionNorm.thy file | annotate | diff | comparison | revisions src/HOL/Real/HahnBanach/FunctionOrder.thy file | annotate | diff | comparison | revisions src/HOL/Real/HahnBanach/HahnBanach.thy file | annotate | diff | comparison | revisions src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy file | annotate | diff | comparison | revisions src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy file | annotate | diff | comparison | revisions src/HOL/Real/HahnBanach/NormedSpace.thy file | annotate | diff | comparison | revisions src/HOL/Real/HahnBanach/README.html file | annotate | diff | comparison | revisions src/HOL/Real/HahnBanach/ROOT.ML file | annotate | diff | comparison | revisions src/HOL/Real/HahnBanach/Subspace.thy file | annotate | diff | comparison | revisions src/HOL/Real/HahnBanach/VectorSpace.thy file | annotate | diff | comparison | revisions src/HOL/Real/HahnBanach/ZornLemma.thy file | annotate | diff | comparison | revisions src/HOL/Real/HahnBanach/document/notation.tex file | annotate | diff | comparison | revisions src/HOL/Real/HahnBanach/document/root.bib file | annotate | diff | comparison | revisions src/HOL/Real/HahnBanach/document/root.tex file | annotate | diff | comparison | revisions
--- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Mon Oct 25 19:24:43 1999 +0200
@@ -12,7 +12,7 @@
text{* A linearform $f$ on a normed vector space $(V, \norm{\cdot})$
is \emph{continous}, iff it is bounded, i.~e.
$\exists\ap c\in R.\ap \forall\ap x\in V.\ap -|f\ap x| \leq c \cdot \norm x.$
+|f\ap x| \leq c \cdot \norm x\]
In our application no other functions than linearforms are considered,
so we can define continous linearforms as follows:
*};
@@ -48,15 +48,15 @@
is called the \emph{norm} of $f$.

For the non-trivial vector space $V$ the norm can be defined as
-$\fnorm {f} =\sup_{x\neq\zero}\frac{|f\ap x|}{\norm x}.$
+$\fnorm {f} =\sup_{x\neq\zero}\frac{|f\ap x|}{\norm x}$

-For the case that the vector space $V$ contains only the zero vector
-set, the set $B$ this supremum is taken from would be empty, and any
-real number is a supremum of $B$. So it must be guarateed that there
-is an element in $B$. This element must be greater or equal $0$ so
-that $\idt{function{\dsh}norm}$ has the norm properties. Furthermore
-it does not have to change the norm in all other cases, so it must be
-$0$, as all other elements of $B$ are greater or equal $0$.
+For the case that the vector space $V$ contains only the $\zero$
+vector, the set $B$ this supremum is taken from would be empty, and
+any real number is a supremum of $B$. So it must be guarateed that
+there is an element in $B$. This element must be ${} \ge 0$ so that
+$\idt{function{\dsh}norm}$ has the norm properties. Furthermore it
+does not have to change the norm in all other cases, so it must be
+$0$, as all other elements of $B$ are ${} \ge 0$.

Thus $B$ is defined as follows.
*};
@@ -250,7 +250,7 @@

txt{* The proof is by case analysis on $x$. *};

-  show "?thesis";
+  show ?thesis;
proof (rule case_split);

txt {* For the case $x = \zero$ the thesis follows
--- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Mon Oct 25 19:24:43 1999 +0200
@@ -12,11 +12,11 @@

text{* We define the \emph{graph} of a (real) function $f$ with the
domain $F$ as the set
-\begin{matharray}{l}
-\{(x, f\ap x). \ap x:F\}.
-\end{matharray}
+$+\{(x, f\ap x). \ap x:F\} +$
So we are modelling partial functions by specifying the domain and
-the mapping function. We use the notion 'function' also for the graph
+the mapping function. We use the notion function'' also for the graph
of a function.
*};

--- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Mon Oct 25 19:24:43 1999 +0200
@@ -10,7 +10,7 @@

text {*
We present the proof of two different versions of the Hahn-Banach
-  Theorem, closely following \cite{Heuser:1986}.
+  Theorem, closely following \cite[\S36]{Heuser:1986}.
*};

subsection {* The case of general linear spaces *};
@@ -49,7 +49,7 @@
the union of all functions in the chain is again a norm preserving
function. (The union is an upper bound for all elements.
It is even the least upper bound, because every upper bound of $M$
-  is also an upper bound for $\cup\; c$.) *};
+  is also an upper bound for $\Union c$.) *};

have "!! c. [| c : chain M; EX x. x:c |] ==> Union c : M";
proof -;
@@ -91,7 +91,7 @@
qed;
qed;

-  txt {* According to Zorn's Lemma there exists
+  txt {* According to Zorn's Lemma there is
a maximal norm-preserving extension $g\in M$. *};

with aM; have bex_g: "EX g:M. ALL x:M. g <= x --> g = x";
@@ -283,7 +283,7 @@
thus ?thesis; ..;
qed;

-  txt {* We have shown, that $h$ can still be extended to
+  txt {* We have shown that $h$ can still be extended to
some $h_0$, in contradiction to the assumption that
$h$ is a maximal element. *};

@@ -293,7 +293,7 @@
qed;

-txt{* It follows $H = E$ and the thesis can be shown. *};
+txt{* It follows $H = E$, and the thesis can be shown. *};

show "is_linearform E h & (ALL x:F. h x = f x)
& (ALL x:E. h x <= p x)";
@@ -372,8 +372,8 @@

txt{* We define the function $p$ on $E$ as follows:
\begin{matharray}{l}
-  p\ap x = \fnorm f * \norm x\\
-  % p\ap x = \fnorm f * \fnorm x.\\
+  p\ap x = \fnorm f \cdot \norm x\\
+  % p\ap x = \fnorm f \cdot \fnorm x\\
\end{matharray}
*};

@@ -408,7 +408,7 @@
finally; show ?thesis; .;
qed;

-    txt{* Furthermore $p$ obeys the triangle inequation: *};
+    txt{* Furthermore, $p$ obeys the triangle inequation: *};

show "p (x + y) <= p x + p y";
proof -;
@@ -478,7 +478,7 @@
a solution
for the inequation
\begin{matharray}{l}
-        \forall\ap x\in E.\ap |g\ap x| \leq c * \norm x.
+        \forall\ap x\in E.\ap |g\ap x| \leq c \cdot \norm x
\end{matharray} *};

have "ALL x:E. rabs (g x) <= function_norm F norm f * norm x";
--- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Mon Oct 25 19:24:43 1999 +0200
@@ -3,7 +3,7 @@
Author:     Gertrud Bauer, TU Munich
*)

-header {* Extending a non-ma\-xi\-mal function *};
+header {* Extending a non-maximal function *};

theory HahnBanachExtLemmas = FunctionNorm:;

@@ -30,7 +30,7 @@
\end{matharray}
it suffices to show that
\begin{matharray}{l}
-\forall u\in F. \ap\forall v\in F. \ap a\ap u \leq b \ap v.
+\forall u\in F. \ap\forall v\in F. \ap a\ap u \leq b \ap v
\end{matharray}
*};

@@ -84,7 +84,7 @@
show ?thesis;
proof (intro exI conjI ballI);

-      txt {* For all $y\in F$ is $a\ap y \leq \xi$. *};
+      txt {* For all $y\in F$ holds $a\ap y \leq \xi$. *};

fix y; assume y: "y:F";
show "a y <= xi";
@@ -93,7 +93,7 @@
qed (force!);
next;

-      txt {* For all $y\in F$ is $\xi\leq b\ap y$. *};
+      txt {* For all $y\in F$ holds $\xi\leq b\ap y$. *};

fix y; assume "y:F";
show "xi <= b y";
@@ -115,8 +115,8 @@
qed;
qed;

-text{* The function $h_0$ is defined as a linear extension of $h$
-to $H_0$. $h_0$ is linear. *};
+text{* The function $h_0$ is defined as a canonical linear extension
+of $h$ to $H_0$. *};

lemma h0_lf:
"[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H
@@ -142,7 +142,7 @@
fix x1 x2; assume x1: "x1 : H0" and x2: "x2 : H0";

txt{* We now have to show that $h_0$ is linear
$h_0 \ap (x_1\plus x_2) = h_0\ap x_1 + h_0\ap x_2$
for $x_1, x_2\in H$. *};

@@ -192,8 +192,8 @@

txt{* We further have to show that $h_0$ is linear
w.~r.~t.~scalar multiplication,
-    i.~e.~ $c\in real$ $h_0\ap (c \mult x_1) = c \cdot h_0\ap x_1$
-    for $x\in H$ and real $c$.
+    i.~e.\ $h_0\ap (c \mult x_1) = c \cdot h_0\ap x_1$
+    for $x\in H$ and any real number $c$.
*};

next;
@@ -268,7 +268,7 @@
by (rule h0_definite);

txt{* Now we show
-    $h\ap y + a * xi\leq p\ap (y\plus a \mult x_0)$
+    $h\ap y + a \cdot xi\leq p\ap (y\plus a \mult x_0)$
by case analysis on $a$. *};

also; have "... <= p (y + a <*> x0)";
@@ -278,7 +278,7 @@
with vs y a; show ?thesis; by simp;

txt {* In the case $a < 0$ we use $a_1$ with $y$ taken as
-    $\frac{y}{a}$. *};
+    $y/a$. *};

next;
assume lz: "a < 0r"; hence nz: "a ~= 0r"; by simp;
@@ -308,7 +308,7 @@
thus ?thesis; by simp;

txt {* In the case $a > 0$ we use $a_2$ with $y$ taken
-      as $\frac{y}{a}$. *};
+      as $y/a$. *};
next;
assume gz: "0r < a"; hence nz: "a ~= 0r"; by simp;
have "xi <= p (rinv a <*> y + x0) - h (rinv a <*> y)";
--- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Mon Oct 25 19:24:43 1999 +0200
@@ -15,7 +15,7 @@
Let $E$ be a real vector space with a quasinorm $q$ on $E$.
$F$ is a subspace of $E$ and $f$ a linearform on $F$. We
consider a chain $c$ of norm preserving extensions of $f$, such that
-$\cup\; c = \idt{graph}\ap H\ap h$.
+$\Union c = \idt{graph}\ap H\ap h$.
We will show some properties about the limit function $h$,
i.~e.~the supremum of the chain $c$.
*};
@@ -348,8 +348,8 @@
thus ?thesis;
proof (elim UnionE chainE2);

-    txt{* Since both $(x, y) \in \cup\; c$ and $(x, z) \in cup c$
-    they are menbers of some graphs $G_1$ and $G_2$, resp.~, such that
+    txt{* Since both $(x, y) \in \Union c$ and $(x, z) \in \Union c$
+    they are members of some graphs $G_1$ and $G_2$, resp., such that
both $G_1$ and $G_2$ are members of $c$*};

fix G1 G2; assume
@@ -390,13 +390,11 @@
qed;
qed;

-text{* The limit function $h$ is linear: Every element $x$
-in the domain of $h$ is in the domain of
-a function $h'$ in the chain of norm preserving extensions.
-Futher $h$ is an extension of $h'$ so the value
-of $x$ are identical for $h'$ and $h$.
-Finally, the function $h'$ is linear by construction of $M$.
-*};
+text{* The limit function $h$ is linear: every element $x$ in the
+domain of $h$ is in the domain of a function $h'$ in the chain of norm
+preserving extensions.  Furthermore, $h$ is an extension of $h'$ so
+the value of $x$ are identical for $h'$ and $h$.  Finally, the
+function $h'$ is linear by construction of $M$.  *};

lemma sup_lf:
"[| M = norm_pres_extensions E p F f; c: chain M;
@@ -439,7 +437,7 @@
by (rule some_H'h');

txt{* We have to show that h is linear w.~r.~t.
-    skalar multiplication. *};
+    scalar multiplication. *};

thus "h (a <*> x) = a * h x";
proof (elim exE conjE);
@@ -494,10 +492,10 @@
qed;
qed;

-text{* The domain $H$ of the limit function is a superspace
-of $F$, since $F$ is a subset of $H$. The existence of
-the $\zero$ element in $F$ and the closeness properties
-follow from the fact that $F$ is a vectorspace. *};
+text{* The domain $H$ of the limit function is a superspace of $F$,
+since $F$ is a subset of $H$. The existence of the $\zero$ element in
+$F$ and the closure properties follow from the fact that $F$ is a
+vectorspace. *};

lemma sup_supF:
"[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c;
@@ -528,7 +526,7 @@
qed;
qed;

-text{* The domain $H$ of the limt function is a subspace
+text{* The domain $H$ of the limit function is a subspace
of $E$. *};

lemma sup_subE:
@@ -588,7 +586,7 @@
qed;
qed;

-    txt{* $H$ is closed under skalar multiplication. *};
+    txt{* $H$ is closed under scalar multiplication. *};

show "ALL x:H. ALL a. a <*> x : H";
proof (intro ballI allI);
@@ -610,8 +608,8 @@
qed;
qed;

-text {* The limit functon is bounded by
-the norm $p$ as well, simce all elements in the chain are norm preserving.
+text {* The limit function is bounded by
+the norm $p$ as well, since all elements in the chain are norm preserving.
*};

lemma sup_norm_pres: 
--- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Mon Oct 25 19:24:43 1999 +0200
@@ -72,7 +72,8 @@

subsection {* Norms *};

-text{* A \emph{norm} $\norm{\cdot}$ is a quasinorm that maps only $\zero$ to $0$. *};
+text{* A \emph{norm} $\norm{\cdot}$ is a quasinorm that maps only the
+$\zero$ vector to $0$. *};

constdefs
is_norm :: "['a::{minus, plus} set, 'a => real] => bool"
--- a/src/HOL/Real/HahnBanach/README.html	Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/README.html	Mon Oct 25 19:24:43 1999 +0200
@@ -1,6 +1,6 @@

-<H3> The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).</H3>
+<H3> The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar).</H3>

Author:     Gertrud Bauer, Technische Universit&auml;t M&uuml;nchen<P>

--- a/src/HOL/Real/HahnBanach/ROOT.ML	Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/ROOT.ML	Mon Oct 25 19:24:43 1999 +0200
@@ -2,7 +2,7 @@
ID:         $Id$
Author:     Gertrud Bauer, TU Munich

-The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).
+The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
*)

time_use_thy "Bounds";
--- a/src/HOL/Real/HahnBanach/Subspace.thy	Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/Subspace.thy	Mon Oct 25 19:24:43 1999 +0200
@@ -213,9 +213,8 @@
instance set :: (plus) plus; by intro_classes;

defs vs_sum_def:
-  "U + V == {x. EX u:U. EX v:V. x = u + v}";
+  "U + V == {x. EX u:U. EX v:V. x = u + v}";(***

-(***
constdefs
vs_sum ::
"['a::{minus, plus} set, 'a set] => 'a set"         (infixl "+" 65)
@@ -318,7 +317,7 @@
text {* The sum of $U$ and $V$ is called \emph{direct}, iff the zero
element is the only common element of $U$ and $V$. For every element
$x$ of the direct sum of $U$ and $V$ the decomposition in
-$x = u + v$ with $u:U$ and $v:V$ is unique.*};
+$x = u + v$ with $u \in U$ and $v \in V$ is unique.*};

lemma decomp:
"[| is_vectorspace E; is_subspace U E; is_subspace V E;
@@ -352,7 +351,7 @@
text {* An application of the previous lemma will be used in the
proof of the Hahn-Banach theorem: for an element $y + a \mult x_0$
of the direct sum of a vectorspace $H$ and the linear closure of
-$x_0$ the components $y:H$ and $a$ are unique. *};
+$x_0$ the components $y \in H$ and $a$ are unique. *};

lemma decomp_H0:
"[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H;
@@ -426,7 +425,7 @@

text {* The components $y\in H$ and $a$ in $y \plus a \mult x_0$
are unique, so the function $h_0$ defined by
-$h_0 (y \plus a \mult x_0) = h y + a * xi$ is definite. *};
+$h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *};

lemma h0_definite:
"[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
--- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Mon Oct 25 19:24:43 1999 +0200
@@ -9,9 +9,10 @@

subsection {* Signature *};

-text {* For the definition of real vector spaces a type $\alpha$ is
-considered, on which the operations addition and real scalar
-multiplication are defined, and which has an zero element.*};
+text {* For the definition of real vector spaces a type $\alpha$
+of the sort $\idt{plus}, \idt{minus}$ is considered, on which a
+real scalar multiplication $\mult$ is defined, and which has an zero
+element $\zero$.*};

consts
(***
@@ -24,8 +25,9 @@
prod  :: "[real, 'a] => 'a"                       (infixr "\<prod>" 70)
zero  :: 'a                                       ("\<zero>");

-text {* The unary and binary minus can be considered as
+(* text {* The unary and binary minus can be considered as
abbreviations: *};
+*)

(***
constdefs
@@ -37,15 +39,14 @@

subsection {* Vector space laws *};

-text {* A \emph{vector space} is a non-empty set $V$ of elements
-from $\alpha$ with the following vector space laws:
-The set $V$ is closed under addition and scalar multiplication,
-addition is associative and  commutative. $\minus x$ is the inverse
-of $x$ w.~r.~t.~addition and $\zero$ is the neutral element of
-Scalar multiplication is associative and the real $1$ is the neutral
-element of scalar multiplication.
+text {* A \emph{vector space} is a non-empty set $V$ of elements from
+  $\alpha$ with the following vector space laws: The set $V$ is closed
+  and commutative; $\minus x$ is the inverse of $x$ w.~r.~t.~addition
+  and $\zero$ is the neutral element of addition.  Addition and
+  multiplication are distributive; scalar multiplication is
+  associative and the real $1$ is the neutral element of scalar
+  multiplication.
*};

constdefs
--- a/src/HOL/Real/HahnBanach/ZornLemma.thy	Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/ZornLemma.thy	Mon Oct 25 19:24:43 1999 +0200
@@ -13,8 +13,8 @@
In our application $S$ is a set of sets, ordered by set inclusion. Since
the union of a chain of sets is an upperbound for all elements of the
chain, the conditions of Zorn's lemma can be modified:
-If $S$ is non-empty, it suffices to show that for every non-empty
-chain $c$ in $S$ the union of $c$ also lies in $S$:
+if $S$ is non-empty, it suffices to show that for every non-empty
+chain $c$ in $S$ the union of $c$ also lies in $S$.
*};

theorem Zorn's_Lemma:
@@ -35,7 +35,7 @@
assume "c={}";
with aS; show ?thesis; by fast;

-      txt{* If $c$ is non-empty, then $\cup\; c$
+      txt{* If $c$ is non-empty, then $\Union c$
is an upperbound of $c$, that lies in $S$. *};

next;
--- a/src/HOL/Real/HahnBanach/document/notation.tex	Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/document/notation.tex	Mon Oct 25 19:24:43 1999 +0200
@@ -2,7 +2,7 @@
\newcommand{\isasymbollambda}{${\mathtt{\lambda}}$}

-\parindent 0pt \parskip 0.5ex
+

\newcommand{\name}[1]{\textsf{#1}}

@@ -34,16 +34,17 @@
\newcommand{\Le}{\le}
\newcommand{\Lt}{\lt}
\newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
-\newcommand{\ap}{\mathbin{\!}}
+\newcommand{\ap}{\mathbin{}}
+\newcommand{\Union}{\bigcup}

-\newcommand{\norm}[1]{\|\, #1\,\|}
-\newcommand{\fnorm}[1]{\|\, #1\,\|}
-\newcommand{\zero}{{\mathord{\mathbf {0}}}}
-\newcommand{\plus}{{\mathbin{\;\mathtt {+}\;}}}
-\newcommand{\minus}{{\mathbin{\;\mathtt {-}\;}}}
-\newcommand{\mult}{{\mathbin{\;\mathbf {\odot}\;}}}
-\newcommand{\1}{{\mathord{\mathrm{1}}}}
+\newcommand{\norm}[1]{\left\|#1\right\|}
+\newcommand{\fnorm}[1]{\left\|#1\right\|}
+\newcommand{\zero}{\mathord{\mathbf 0}}
+\newcommand{\plus}{\mathbin{\mathbf +}}
+\newcommand{\minus}{\mathbin{\mathbf -}}
+\newcommand{\mult}{\mathbin{\mathbf\odot}}
+\newcommand{\1}{\mathord{\mathrm{1}}}
%\newcommand{\zero}{{\mathord{\small\sl\tt {<0>}}}}
%\newcommand{\plus}{{\mathbin{\;\small\sl\tt {[+]}\;}}}
%\newcommand{\minus}{{\mathbin{\;\small\sl\tt {[-]}\;}}}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/document/root.bib	Mon Oct 25 19:24:43 1999 +0200
@@ -0,0 +1,27 @@
+
+@Book{Heuser:1986,
+  author = 	 {H. Heuser},
+  title = 	 {Funktionalanalysis: Theorie und Anwendung},
+  publisher = 	 {Teubner},
+  year = 	 1986
+}
+
+@InCollection{Narici:1996,
+  author = 	 {L. Narici and E. Beckenstein},
+  title = 	 {The {Hahn-Banach Theorem}: The Life and Times},
+  booktitle = 	 {Topology Atlas},
+  publisher =	 {York University, Toronto, Ontario, Canada},
+  year =	 1996,
+  note =	 {\url{http://at.yorku.ca/topology/preprint.htm} and
+                  \url{http://at.yorku.ca/p/a/a/a/16.htm}}
+}
+
+@Article{Nowak:1993,
+  author =       {B. Nowak and A. Trybulec},
+  title =	 {{Hahn-Banach} Theorem},
+  journal =      {Journal of Formalized Mathematics},
+  year =         {1993},
+  volume =       {5},
+  institution =  {University of Bialystok},
+  note =         {\url{http://mizar.uwb.edu.pl/JFM/Vol5/hahnban.html}}
+}
--- a/src/HOL/Real/HahnBanach/document/root.tex	Mon Oct 25 19:24:31 1999 +0200
+++ b/src/HOL/Real/HahnBanach/document/root.tex	Mon Oct 25 19:24:43 1999 +0200
@@ -12,32 +12,42 @@
\pagenumbering{arabic}

-\title{The Hahn-Banach Theorem for Real Vectorspaces}
+\title{The Hahn-Banach Theorem for Real Vector Spaces}
\author{Gertrud Bauer}
\maketitle

\begin{abstract}
-The Hahn-Banach theorem is one of the most important theorems
-of functional analysis. We present the fully formal proof of two versions of
-the theorem, one for general linear spaces and one for normed spaces
-as a corollary of the first.
-
-The first part contains the definition of basic notions of
-linear algebra, such as vector spaces, subspaces, normed spaces,
-continous linearforms, norm of functions and an order on
-functions by domain extension.
-
-The second part contains some lemmas about the supremum w.r.t. the
-function order and the extension of a non-maximal function,
-which are needed for the proof of the main theorem.
-
-The third part is the proof of the theorem in its two different versions.
-
+  The Hahn-Banach theorem is one of the most fundamental results in functional
+  analysis. We present a fully formal proof of two versions of the theorem,
+  one for general linear spaces and another for normed spaces.  This
+  development is based on simply-typed classical set-theory, as provided by
+  Isabelle/HOL.
\end{abstract}

+
\tableofcontents
+\parindent 0pt \parskip 0.5ex
+
+\clearpage
+\section{Preface}

-\part {Basic notions}
+This is a fully formal proof of the Hahn-Banach theorem. It closely follows
+the informal presentation given in the textbook \cite[\S 36]{Heuser:1986}.
+Another formal proof of the same theorem has been done in Mizar
+\cite{Nowak:1993}.  A general overview of the relevance and history of the
+Hahn-Banach theorem is given in \cite{Narici:1996}.
+
+\medskip The document is structured as follows.  The first part contains
+definitions of basic notions of linear algebra: vector spaces, subspaces,
+normed spaces, continuous linearforms, norm of functions and an order on
+functions by domain extension.  The second part contains some lemmas about the
+supremum (w.r.t.\ the function order) and extension of non-maximal functions.
+With these preliminaries, the main proof of the theorem (in its two versions)
+is conducted in the third part.
+
+
+\clearpage
+\part {Basic Notions}

\input{Bounds.tex}
\input{Aux.tex}
@@ -49,15 +59,17 @@
\input{FunctionNorm.tex}
\input{ZornLemma.tex}

-\part {Lemmas for the proof}
+\clearpage
+\part {Lemmas for the Proof}

\input{HahnBanachSupLemmas.tex}
\input{HahnBanachExtLemmas.tex}

-\part {The proof}
+\clearpage
+\part {The Main Proof}

\input{HahnBanach.tex}
\bibliographystyle{abbrv}
-\bibliography{bib}
+\bibliography{root}

\end{document}