update by Gertrud Bauer;
authorwenzelm
Mon Oct 25 19:24:43 1999 +0200 (1999-10-25)
changeset 7927b50446a33c16
parent 7926 9c20924de52c
child 7928 06a11f8cf573
update by Gertrud Bauer;
src/HOL/Real/HahnBanach/FunctionNorm.thy
src/HOL/Real/HahnBanach/FunctionOrder.thy
src/HOL/Real/HahnBanach/HahnBanach.thy
src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy
src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy
src/HOL/Real/HahnBanach/NormedSpace.thy
src/HOL/Real/HahnBanach/README.html
src/HOL/Real/HahnBanach/ROOT.ML
src/HOL/Real/HahnBanach/Subspace.thy
src/HOL/Real/HahnBanach/VectorSpace.thy
src/HOL/Real/HahnBanach/ZornLemma.thy
src/HOL/Real/HahnBanach/document/notation.tex
src/HOL/Real/HahnBanach/document/root.bib
src/HOL/Real/HahnBanach/document/root.tex
     1.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Mon Oct 25 19:24:31 1999 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Mon Oct 25 19:24:43 1999 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4  text{* A linearform $f$ on a normed vector space $(V, \norm{\cdot})$
     1.5  is \emph{continous}, iff it is bounded, i.~e.
     1.6  \[\exists\ap c\in R.\ap \forall\ap x\in V.\ap 
     1.7 -|f\ap x| \leq c \cdot \norm x.\]
     1.8 +|f\ap x| \leq c \cdot \norm x\]
     1.9  In our application no other functions than linearforms are considered,
    1.10  so we can define continous linearforms as follows:
    1.11  *};
    1.12 @@ -48,15 +48,15 @@
    1.13  is called the \emph{norm} of $f$.
    1.14  
    1.15  For the non-trivial vector space $V$ the norm can be defined as 
    1.16 -\[\fnorm {f} =\sup_{x\neq\zero}\frac{|f\ap x|}{\norm x}. \] 
    1.17 +\[\fnorm {f} =\sup_{x\neq\zero}\frac{|f\ap x|}{\norm x} \] 
    1.18  
    1.19 -For the case that the vector space $V$ contains only the zero vector 
    1.20 -set, the set $B$ this supremum is taken from would be empty, and any 
    1.21 -real number is a supremum of $B$. So it must be guarateed that there 
    1.22 -is an element in $B$. This element must be greater or equal $0$ so 
    1.23 -that $\idt{function{\dsh}norm}$ has the norm properties. Furthermore 
    1.24 -it does not have to change the norm in all other cases, so it must be
    1.25 -$0$, as all other elements of $B$ are greater or equal $0$.
    1.26 +For the case that the vector space $V$ contains only the $\zero$
    1.27 +vector, the set $B$ this supremum is taken from would be empty, and
    1.28 +any real number is a supremum of $B$. So it must be guarateed that
    1.29 +there is an element in $B$. This element must be ${} \ge 0$ so that
    1.30 +$\idt{function{\dsh}norm}$ has the norm properties. Furthermore it
    1.31 +does not have to change the norm in all other cases, so it must be
    1.32 +$0$, as all other elements of $B$ are ${} \ge 0$.
    1.33  
    1.34  Thus $B$ is defined as follows.
    1.35  *};
    1.36 @@ -250,7 +250,7 @@
    1.37  
    1.38   txt{* The proof is by case analysis on $x$. *};
    1.39   
    1.40 -  show "?thesis";
    1.41 +  show ?thesis;
    1.42    proof (rule case_split);
    1.43  
    1.44      txt {* For the case $x = \zero$ the thesis follows
     2.1 --- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Mon Oct 25 19:24:31 1999 +0200
     2.2 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Mon Oct 25 19:24:43 1999 +0200
     2.3 @@ -12,11 +12,11 @@
     2.4  
     2.5  text{* We define the \emph{graph} of a (real) function $f$ with the 
     2.6  domain $F$ as the set 
     2.7 -\begin{matharray}{l}
     2.8 -\{(x, f\ap x). \ap x:F\}.
     2.9 -\end{matharray}
    2.10 +\[
    2.11 +\{(x, f\ap x). \ap x:F\}
    2.12 +\]
    2.13  So we are modelling partial functions by specifying the domain and 
    2.14 -the mapping function. We use the notion 'function' also for the graph
    2.15 +the mapping function. We use the notion ``function'' also for the graph
    2.16  of a function. 
    2.17  *};
    2.18  
     3.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Mon Oct 25 19:24:31 1999 +0200
     3.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Mon Oct 25 19:24:43 1999 +0200
     3.3 @@ -10,7 +10,7 @@
     3.4  
     3.5  text {*
     3.6    We present the proof of two different versions of the Hahn-Banach 
     3.7 -  Theorem, closely following \cite{Heuser:1986}.
     3.8 +  Theorem, closely following \cite[\S36]{Heuser:1986}.
     3.9  *};
    3.10  
    3.11  subsection {* The case of general linear spaces *};
    3.12 @@ -49,7 +49,7 @@
    3.13    the union of all functions in the chain is again a norm preserving
    3.14    function. (The union is an upper bound for all elements. 
    3.15    It is even the least upper bound, because every upper bound of $M$
    3.16 -  is also an upper bound for $\cup\; c$.) *};
    3.17 +  is also an upper bound for $\Union c$.) *};
    3.18  
    3.19    have "!! c. [| c : chain M; EX x. x:c |] ==> Union c : M";  
    3.20    proof -;
    3.21 @@ -91,7 +91,7 @@
    3.22      qed;
    3.23    qed;
    3.24   
    3.25 -  txt {* According to Zorn's Lemma there exists 
    3.26 +  txt {* According to Zorn's Lemma there is
    3.27    a maximal norm-preserving extension $g\in M$. *};
    3.28    
    3.29    with aM; have bex_g: "EX g:M. ALL x:M. g <= x --> g = x";
    3.30 @@ -283,7 +283,7 @@
    3.31      thus ?thesis; ..;
    3.32    qed;
    3.33  
    3.34 -  txt {* We have shown, that $h$ can still be extended to 
    3.35 +  txt {* We have shown that $h$ can still be extended to 
    3.36    some $h_0$, in contradiction to the assumption that 
    3.37    $h$ is a maximal element. *};
    3.38  
    3.39 @@ -293,7 +293,7 @@
    3.40    thus ?thesis; by contradiction;
    3.41  qed; 
    3.42  
    3.43 -txt{* It follows $H = E$ and the thesis can be shown. *};
    3.44 +txt{* It follows $H = E$, and the thesis can be shown. *};
    3.45  
    3.46  show "is_linearform E h & (ALL x:F. h x = f x) 
    3.47       & (ALL x:E. h x <= p x)";
    3.48 @@ -372,8 +372,8 @@
    3.49  
    3.50    txt{* We define the function $p$ on $E$ as follows:
    3.51    \begin{matharray}{l}
    3.52 -  p\ap x = \fnorm f * \norm x\\
    3.53 -  % p\ap x = \fnorm f * \fnorm x.\\
    3.54 +  p\ap x = \fnorm f \cdot \norm x\\
    3.55 +  % p\ap x = \fnorm f \cdot \fnorm x\\
    3.56    \end{matharray}
    3.57    *};
    3.58  
    3.59 @@ -408,7 +408,7 @@
    3.60        finally; show ?thesis; .;
    3.61      qed;
    3.62  
    3.63 -    txt{* Furthermore $p$ obeys the triangle inequation: *};
    3.64 +    txt{* Furthermore, $p$ obeys the triangle inequation: *};
    3.65  
    3.66      show "p (x + y) <= p x + p y";
    3.67      proof -;
    3.68 @@ -478,7 +478,7 @@
    3.69          a solution
    3.70          for the inequation 
    3.71          \begin{matharray}{l}
    3.72 -        \forall\ap x\in E.\ap |g\ap x| \leq c * \norm x.
    3.73 +        \forall\ap x\in E.\ap |g\ap x| \leq c \cdot \norm x
    3.74          \end{matharray} *};
    3.75  
    3.76          have "ALL x:E. rabs (g x) <= function_norm F norm f * norm x";
     4.1 --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Mon Oct 25 19:24:31 1999 +0200
     4.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Mon Oct 25 19:24:43 1999 +0200
     4.3 @@ -3,7 +3,7 @@
     4.4      Author:     Gertrud Bauer, TU Munich
     4.5  *)
     4.6  
     4.7 -header {* Extending a non-ma\-xi\-mal function *};
     4.8 +header {* Extending a non-maximal function *};
     4.9  
    4.10  theory HahnBanachExtLemmas = FunctionNorm:;
    4.11  
    4.12 @@ -30,7 +30,7 @@
    4.13  \end{matharray}
    4.14  it suffices to show that 
    4.15  \begin{matharray}{l}
    4.16 -\forall u\in F. \ap\forall v\in F. \ap a\ap u \leq b \ap v.
    4.17 +\forall u\in F. \ap\forall v\in F. \ap a\ap u \leq b \ap v
    4.18  \end{matharray}
    4.19  *};
    4.20  
    4.21 @@ -84,7 +84,7 @@
    4.22      show ?thesis;
    4.23      proof (intro exI conjI ballI); 
    4.24     
    4.25 -      txt {* For all $y\in F$ is $a\ap y \leq \xi$. *};
    4.26 +      txt {* For all $y\in F$ holds $a\ap y \leq \xi$. *};
    4.27       
    4.28        fix y; assume y: "y:F";
    4.29        show "a y <= xi";    
    4.30 @@ -93,7 +93,7 @@
    4.31        qed (force!);
    4.32      next;
    4.33  
    4.34 -      txt {* For all $y\in F$ is $\xi\leq b\ap y$. *};
    4.35 +      txt {* For all $y\in F$ holds $\xi\leq b\ap y$. *};
    4.36  
    4.37        fix y; assume "y:F";
    4.38        show "xi <= b y";  
    4.39 @@ -115,8 +115,8 @@
    4.40    qed;
    4.41  qed;
    4.42  
    4.43 -text{* The function $h_0$ is defined as a linear extension of $h$
    4.44 -to $H_0$. $h_0$ is linear. *};
    4.45 +text{* The function $h_0$ is defined as a canonical linear extension
    4.46 +of $h$ to $H_0$. *};
    4.47  
    4.48  lemma h0_lf: 
    4.49    "[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
    4.50 @@ -142,7 +142,7 @@
    4.51      fix x1 x2; assume x1: "x1 : H0" and x2: "x2 : H0"; 
    4.52  
    4.53      txt{* We now have to show that $h_0$ is linear 
    4.54 -    w.~r.~t.~addition, i.~e.~
    4.55 +    w.~r.~t.~addition, i.~e.\
    4.56      $h_0 \ap (x_1\plus x_2) = h_0\ap x_1 + h_0\ap x_2$
    4.57      for $x_1, x_2\in H$. *}; 
    4.58  
    4.59 @@ -192,8 +192,8 @@
    4.60   
    4.61      txt{* We further have to show that $h_0$ is linear 
    4.62      w.~r.~t.~scalar multiplication, 
    4.63 -    i.~e.~ $c\in real$ $h_0\ap (c \mult x_1) = c \cdot h_0\ap x_1$
    4.64 -    for $x\in H$ and real $c$. 
    4.65 +    i.~e.\ $h_0\ap (c \mult x_1) = c \cdot h_0\ap x_1$
    4.66 +    for $x\in H$ and any real number $c$. 
    4.67      *}; 
    4.68  
    4.69    next;  
    4.70 @@ -268,7 +268,7 @@
    4.71        by (rule h0_definite);
    4.72  
    4.73      txt{* Now we show  
    4.74 -    $h\ap y + a * xi\leq  p\ap (y\plus a \mult x_0)$ 
    4.75 +    $h\ap y + a \cdot xi\leq  p\ap (y\plus a \mult x_0)$ 
    4.76      by case analysis on $a$. *};
    4.77  
    4.78      also; have "... <= p (y + a <*> x0)";
    4.79 @@ -278,7 +278,7 @@
    4.80        with vs y a; show ?thesis; by simp;
    4.81  
    4.82      txt {* In the case $a < 0$ we use $a_1$ with $y$ taken as
    4.83 -    $\frac{y}{a}$. *};
    4.84 +    $y/a$. *};
    4.85  
    4.86      next;
    4.87        assume lz: "a < 0r"; hence nz: "a ~= 0r"; by simp;
    4.88 @@ -308,7 +308,7 @@
    4.89        thus ?thesis; by simp;
    4.90  
    4.91        txt {* In the case $a > 0$ we use $a_2$ with $y$ taken
    4.92 -      as $\frac{y}{a}$. *};
    4.93 +      as $y/a$. *};
    4.94      next; 
    4.95        assume gz: "0r < a"; hence nz: "a ~= 0r"; by simp;
    4.96        have "xi <= p (rinv a <*> y + x0) - h (rinv a <*> y)";
     5.1 --- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Mon Oct 25 19:24:31 1999 +0200
     5.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Mon Oct 25 19:24:43 1999 +0200
     5.3 @@ -15,7 +15,7 @@
     5.4  Let $E$ be a real vector space with a quasinorm $q$ on $E$. 
     5.5  $F$ is a subspace of $E$ and $f$ a linearform on $F$. We 
     5.6  consider a chain $c$ of norm preserving extensions of $f$, such that
     5.7 -$\cup\; c = \idt{graph}\ap H\ap h$. 
     5.8 +$\Union c = \idt{graph}\ap H\ap h$. 
     5.9  We will show some properties about the limit function $h$, 
    5.10  i.~e.~the supremum of the chain $c$.
    5.11  *}; 
    5.12 @@ -348,8 +348,8 @@
    5.13    thus ?thesis;
    5.14    proof (elim UnionE chainE2);
    5.15  
    5.16 -    txt{* Since both $(x, y) \in \cup\; c$ and $(x, z) \in cup c$
    5.17 -    they are menbers of some graphs $G_1$ and $G_2$, resp.~, such that
    5.18 +    txt{* Since both $(x, y) \in \Union c$ and $(x, z) \in \Union c$
    5.19 +    they are members of some graphs $G_1$ and $G_2$, resp., such that
    5.20      both $G_1$ and $G_2$ are members of $c$*};
    5.21  
    5.22      fix G1 G2; assume
    5.23 @@ -390,13 +390,11 @@
    5.24    qed;
    5.25  qed;
    5.26  
    5.27 -text{* The limit function $h$ is linear: Every element $x$
    5.28 -in the domain of $h$ is in the domain of 
    5.29 -a function $h'$ in the chain of norm preserving extensions.
    5.30 -Futher $h$ is an extension of $h'$ so the value
    5.31 -of $x$ are identical for $h'$ and $h$.
    5.32 -Finally, the function $h'$ is linear by construction of $M$.
    5.33 -*};
    5.34 +text{* The limit function $h$ is linear: every element $x$ in the
    5.35 +domain of $h$ is in the domain of a function $h'$ in the chain of norm
    5.36 +preserving extensions.  Furthermore, $h$ is an extension of $h'$ so
    5.37 +the value of $x$ are identical for $h'$ and $h$.  Finally, the
    5.38 +function $h'$ is linear by construction of $M$.  *};
    5.39  
    5.40  lemma sup_lf: 
    5.41    "[| M = norm_pres_extensions E p F f; c: chain M; 
    5.42 @@ -439,7 +437,7 @@
    5.43        by (rule some_H'h');
    5.44  
    5.45      txt{* We have to show that h is linear w.~r.~t. 
    5.46 -    skalar multiplication. *};
    5.47 +    scalar multiplication. *};
    5.48  
    5.49      thus "h (a <*> x) = a * h x";
    5.50      proof (elim exE conjE);
    5.51 @@ -494,10 +492,10 @@
    5.52    qed;
    5.53  qed;
    5.54  
    5.55 -text{* The domain $H$ of the limit function is a superspace
    5.56 -of $F$, since $F$ is a subset of $H$. The existence of 
    5.57 -the $\zero$ element in $F$ and the closeness properties
    5.58 -follow from the fact that $F$ is a vectorspace. *};
    5.59 +text{* The domain $H$ of the limit function is a superspace of $F$,
    5.60 +since $F$ is a subset of $H$. The existence of the $\zero$ element in
    5.61 +$F$ and the closure properties follow from the fact that $F$ is a
    5.62 +vectorspace. *};
    5.63  
    5.64  lemma sup_supF: 
    5.65    "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c;
    5.66 @@ -528,7 +526,7 @@
    5.67    qed;
    5.68  qed;
    5.69  
    5.70 -text{* The domain $H$ of the limt function is a subspace
    5.71 +text{* The domain $H$ of the limit function is a subspace
    5.72  of $E$. *};
    5.73  
    5.74  lemma sup_subE: 
    5.75 @@ -588,7 +586,7 @@
    5.76        qed;
    5.77      qed;      
    5.78  
    5.79 -    txt{* $H$ is closed under skalar multiplication. *};
    5.80 +    txt{* $H$ is closed under scalar multiplication. *};
    5.81  
    5.82      show "ALL x:H. ALL a. a <*> x : H"; 
    5.83      proof (intro ballI allI); 
    5.84 @@ -610,8 +608,8 @@
    5.85    qed;
    5.86  qed;
    5.87  
    5.88 -text {* The limit functon is bounded by 
    5.89 -the norm $p$ as well, simce all elements in the chain are norm preserving.
    5.90 +text {* The limit function is bounded by 
    5.91 +the norm $p$ as well, since all elements in the chain are norm preserving.
    5.92  *};
    5.93  
    5.94  lemma sup_norm_pres: 
     6.1 --- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Mon Oct 25 19:24:31 1999 +0200
     6.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Mon Oct 25 19:24:43 1999 +0200
     6.3 @@ -72,7 +72,8 @@
     6.4  
     6.5  subsection {* Norms *};
     6.6  
     6.7 -text{* A \emph{norm} $\norm{\cdot}$ is a quasinorm that maps only $\zero$ to $0$. *};
     6.8 +text{* A \emph{norm} $\norm{\cdot}$ is a quasinorm that maps only the
     6.9 +$\zero$ vector to $0$. *};
    6.10  
    6.11  constdefs
    6.12    is_norm :: "['a::{minus, plus} set, 'a => real] => bool"
     7.1 --- a/src/HOL/Real/HahnBanach/README.html	Mon Oct 25 19:24:31 1999 +0200
     7.2 +++ b/src/HOL/Real/HahnBanach/README.html	Mon Oct 25 19:24:43 1999 +0200
     7.3 @@ -1,6 +1,6 @@
     7.4  <HTML><HEAD><TITLE>HOL/Real/HahnBanach/README</TITLE></HEAD><BODY>
     7.5  
     7.6 -<H3> The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).</H3>
     7.7 +<H3> The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar).</H3>
     7.8  
     7.9  Author:     Gertrud Bauer, Technische Universit&auml;t M&uuml;nchen<P>
    7.10  
     8.1 --- a/src/HOL/Real/HahnBanach/ROOT.ML	Mon Oct 25 19:24:31 1999 +0200
     8.2 +++ b/src/HOL/Real/HahnBanach/ROOT.ML	Mon Oct 25 19:24:43 1999 +0200
     8.3 @@ -2,7 +2,7 @@
     8.4      ID:         $Id$
     8.5      Author:     Gertrud Bauer, TU Munich
     8.6  
     8.7 -The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).
     8.8 +The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
     8.9  *)
    8.10  
    8.11  time_use_thy "Bounds";
     9.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Mon Oct 25 19:24:31 1999 +0200
     9.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Mon Oct 25 19:24:43 1999 +0200
     9.3 @@ -213,9 +213,8 @@
     9.4  instance set :: (plus) plus; by intro_classes;
     9.5  
     9.6  defs vs_sum_def:
     9.7 -  "U + V == {x. EX u:U. EX v:V. x = u + v}";
     9.8 +  "U + V == {x. EX u:U. EX v:V. x = u + v}";(***  
     9.9  
    9.10 -(***
    9.11  constdefs 
    9.12    vs_sum :: 
    9.13    "['a::{minus, plus} set, 'a set] => 'a set"         (infixl "+" 65)
    9.14 @@ -318,7 +317,7 @@
    9.15  text {* The sum of $U$ and $V$ is called \emph{direct}, iff the zero 
    9.16  element is the only common element of $U$ and $V$. For every element
    9.17  $x$ of the direct sum of $U$ and $V$ the decomposition in
    9.18 -$x = u + v$ with $u:U$ and $v:V$ is unique.*}; 
    9.19 +$x = u + v$ with $u \in U$ and $v \in V$ is unique.*}; 
    9.20  
    9.21  lemma decomp: 
    9.22    "[| is_vectorspace E; is_subspace U E; is_subspace V E; 
    9.23 @@ -352,7 +351,7 @@
    9.24  text {* An application of the previous lemma will be used in the 
    9.25  proof of the Hahn-Banach theorem: for an element $y + a \mult x_0$ 
    9.26  of the direct sum of a vectorspace $H$ and the linear closure of 
    9.27 -$x_0$ the components $y:H$ and $a$ are unique. *}; 
    9.28 +$x_0$ the components $y \in H$ and $a$ are unique. *}; 
    9.29  
    9.30  lemma decomp_H0: 
    9.31    "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; 
    9.32 @@ -426,7 +425,7 @@
    9.33  
    9.34  text {* The components $y\in H$ and $a$ in $y \plus a \mult x_0$ 
    9.35  are unique, so the function $h_0$ defined by 
    9.36 -$h_0 (y \plus a \mult x_0) = h y + a * xi$ is definite. *};
    9.37 +$h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *};
    9.38  
    9.39  lemma h0_definite:
    9.40    "[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
    10.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Mon Oct 25 19:24:31 1999 +0200
    10.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Mon Oct 25 19:24:43 1999 +0200
    10.3 @@ -9,9 +9,10 @@
    10.4  
    10.5  subsection {* Signature *};
    10.6  
    10.7 -text {* For the definition of real vector spaces a type $\alpha$ is 
    10.8 -considered, on which the operations addition and real scalar
    10.9 -multiplication are defined, and which has an zero element.*};
   10.10 +text {* For the definition of real vector spaces a type $\alpha$
   10.11 +of the sort $\idt{plus}, \idt{minus}$ is considered, on which a
   10.12 +real scalar multiplication $\mult$ is defined, and which has an zero 
   10.13 +element $\zero$.*};
   10.14  
   10.15  consts
   10.16  (***
   10.17 @@ -24,8 +25,9 @@
   10.18    prod  :: "[real, 'a] => 'a"                       (infixr "\<prod>" 70)
   10.19    zero  :: 'a                                       ("\<zero>");
   10.20  
   10.21 -text {* The unary and binary minus can be considered as 
   10.22 +(* text {* The unary and binary minus can be considered as 
   10.23  abbreviations: *};
   10.24 +*)
   10.25  
   10.26  (***
   10.27  constdefs 
   10.28 @@ -37,15 +39,14 @@
   10.29  
   10.30  subsection {* Vector space laws *};
   10.31  
   10.32 -text {* A \emph{vector space} is a non-empty set $V$ of elements 
   10.33 -from $\alpha$ with the following vector space laws: 
   10.34 -The set $V$ is closed under addition and scalar multiplication, 
   10.35 -addition is associative and  commutative. $\minus x$ is the inverse
   10.36 -of $x$ w.~r.~t.~addition and $\zero$ is the neutral element of 
   10.37 -addition. 
   10.38 -Addition and multiplication are distributive. 
   10.39 -Scalar multiplication is associative and the real $1$ is the neutral 
   10.40 -element of scalar multiplication.
   10.41 +text {* A \emph{vector space} is a non-empty set $V$ of elements from
   10.42 +  $\alpha$ with the following vector space laws: The set $V$ is closed
   10.43 +  under addition and scalar multiplication, addition is associative
   10.44 +  and commutative; $\minus x$ is the inverse of $x$ w.~r.~t.~addition
   10.45 +  and $\zero$ is the neutral element of addition.  Addition and
   10.46 +  multiplication are distributive; scalar multiplication is
   10.47 +  associative and the real $1$ is the neutral element of scalar
   10.48 +  multiplication.
   10.49  *};
   10.50  
   10.51  constdefs
    11.1 --- a/src/HOL/Real/HahnBanach/ZornLemma.thy	Mon Oct 25 19:24:31 1999 +0200
    11.2 +++ b/src/HOL/Real/HahnBanach/ZornLemma.thy	Mon Oct 25 19:24:43 1999 +0200
    11.3 @@ -13,8 +13,8 @@
    11.4  In our application $S$ is a set of sets, ordered by set inclusion. Since 
    11.5  the union of a chain of sets is an upperbound for all elements of the 
    11.6  chain, the conditions of Zorn's lemma can be modified:
    11.7 -If $S$ is non-empty, it suffices to show that for every non-empty 
    11.8 -chain $c$ in $S$ the union of $c$ also lies in $S$:
    11.9 +if $S$ is non-empty, it suffices to show that for every non-empty 
   11.10 +chain $c$ in $S$ the union of $c$ also lies in $S$.
   11.11  *};
   11.12  
   11.13  theorem Zorn's_Lemma: 
   11.14 @@ -35,7 +35,7 @@
   11.15        assume "c={}"; 
   11.16        with aS; show ?thesis; by fast;
   11.17  
   11.18 -      txt{* If $c$ is non-empty, then $\cup\; c$ 
   11.19 +      txt{* If $c$ is non-empty, then $\Union c$ 
   11.20        is an upperbound of $c$, that lies in $S$. *};
   11.21  
   11.22      next;
    12.1 --- a/src/HOL/Real/HahnBanach/document/notation.tex	Mon Oct 25 19:24:31 1999 +0200
    12.2 +++ b/src/HOL/Real/HahnBanach/document/notation.tex	Mon Oct 25 19:24:43 1999 +0200
    12.3 @@ -2,7 +2,7 @@
    12.4  \renewcommand{\isamarkupheader}[1]{\section{#1}}
    12.5  \newcommand{\isasymbollambda}{${\mathtt{\lambda}}$}
    12.6  
    12.7 -\parindent 0pt \parskip 0.5ex
    12.8 +
    12.9  
   12.10  \newcommand{\name}[1]{\textsf{#1}}
   12.11  
   12.12 @@ -34,16 +34,17 @@
   12.13  \newcommand{\Le}{\le}
   12.14  \newcommand{\Lt}{\lt}
   12.15  \newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
   12.16 -\newcommand{\ap}{\mathbin{\!}}
   12.17 +\newcommand{\ap}{\mathbin{}}
   12.18 +\newcommand{\Union}{\bigcup}
   12.19  
   12.20  
   12.21 -\newcommand{\norm}[1]{\|\, #1\,\|}
   12.22 -\newcommand{\fnorm}[1]{\|\, #1\,\|}
   12.23 -\newcommand{\zero}{{\mathord{\mathbf {0}}}}
   12.24 -\newcommand{\plus}{{\mathbin{\;\mathtt {+}\;}}}
   12.25 -\newcommand{\minus}{{\mathbin{\;\mathtt {-}\;}}}
   12.26 -\newcommand{\mult}{{\mathbin{\;\mathbf {\odot}\;}}}
   12.27 -\newcommand{\1}{{\mathord{\mathrm{1}}}}
   12.28 +\newcommand{\norm}[1]{\left\|#1\right\|}
   12.29 +\newcommand{\fnorm}[1]{\left\|#1\right\|}
   12.30 +\newcommand{\zero}{\mathord{\mathbf 0}}
   12.31 +\newcommand{\plus}{\mathbin{\mathbf +}}
   12.32 +\newcommand{\minus}{\mathbin{\mathbf -}}
   12.33 +\newcommand{\mult}{\mathbin{\mathbf\odot}}
   12.34 +\newcommand{\1}{\mathord{\mathrm{1}}}
   12.35  %\newcommand{\zero}{{\mathord{\small\sl\tt {<0>}}}}
   12.36  %\newcommand{\plus}{{\mathbin{\;\small\sl\tt {[+]}\;}}}
   12.37  %\newcommand{\minus}{{\mathbin{\;\small\sl\tt {[-]}\;}}}
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/src/HOL/Real/HahnBanach/document/root.bib	Mon Oct 25 19:24:43 1999 +0200
    13.3 @@ -0,0 +1,27 @@
    13.4 +
    13.5 +@Book{Heuser:1986,
    13.6 +  author = 	 {H. Heuser},
    13.7 +  title = 	 {Funktionalanalysis: Theorie und Anwendung},
    13.8 +  publisher = 	 {Teubner},
    13.9 +  year = 	 1986
   13.10 +}
   13.11 +
   13.12 +@InCollection{Narici:1996,
   13.13 +  author = 	 {L. Narici and E. Beckenstein},
   13.14 +  title = 	 {The {Hahn-Banach Theorem}: The Life and Times},
   13.15 +  booktitle = 	 {Topology Atlas},
   13.16 +  publisher =	 {York University, Toronto, Ontario, Canada},
   13.17 +  year =	 1996,
   13.18 +  note =	 {\url{http://at.yorku.ca/topology/preprint.htm} and
   13.19 +                  \url{http://at.yorku.ca/p/a/a/a/16.htm}}
   13.20 +}
   13.21 +
   13.22 +@Article{Nowak:1993,
   13.23 +  author =       {B. Nowak and A. Trybulec},
   13.24 +  title =	 {{Hahn-Banach} Theorem},
   13.25 +  journal =      {Journal of Formalized Mathematics},
   13.26 +  year =         {1993},
   13.27 +  volume =       {5},
   13.28 +  institution =  {University of Bialystok},
   13.29 +  note =         {\url{http://mizar.uwb.edu.pl/JFM/Vol5/hahnban.html}}
   13.30 +}
    14.1 --- a/src/HOL/Real/HahnBanach/document/root.tex	Mon Oct 25 19:24:31 1999 +0200
    14.2 +++ b/src/HOL/Real/HahnBanach/document/root.tex	Mon Oct 25 19:24:43 1999 +0200
    14.3 @@ -12,32 +12,42 @@
    14.4  \pagestyle{headings}
    14.5  \pagenumbering{arabic}
    14.6  
    14.7 -\title{The Hahn-Banach Theorem for Real Vectorspaces}
    14.8 +\title{The Hahn-Banach Theorem for Real Vector Spaces}
    14.9  \author{Gertrud Bauer}
   14.10  \maketitle
   14.11  
   14.12  \begin{abstract}
   14.13 -The Hahn-Banach theorem is one of the most important theorems
   14.14 -of functional analysis. We present the fully formal proof of two versions of
   14.15 -the theorem, one for general linear spaces and one for normed spaces
   14.16 -as a corollary of the first. 
   14.17 -
   14.18 -The first part contains the definition of basic notions of
   14.19 -linear algebra, such as vector spaces, subspaces, normed spaces,
   14.20 -continous linearforms, norm of functions and an order on
   14.21 -functions by domain extension.
   14.22 -
   14.23 -The second part contains some lemmas about the supremum w.r.t. the
   14.24 -function order and the extension of a non-maximal function, 
   14.25 -which are needed for the proof of the main theorem.
   14.26 -
   14.27 -The third part is the proof of the theorem in its two different versions.
   14.28 -
   14.29 +  The Hahn-Banach theorem is one of the most fundamental results in functional
   14.30 +  analysis. We present a fully formal proof of two versions of the theorem,
   14.31 +  one for general linear spaces and another for normed spaces.  This
   14.32 +  development is based on simply-typed classical set-theory, as provided by
   14.33 +  Isabelle/HOL.
   14.34  \end{abstract}
   14.35  
   14.36 +
   14.37  \tableofcontents
   14.38 +\parindent 0pt \parskip 0.5ex
   14.39 +
   14.40 +\clearpage
   14.41 +\section{Preface}
   14.42  
   14.43 -\part {Basic notions}
   14.44 +This is a fully formal proof of the Hahn-Banach theorem. It closely follows
   14.45 +the informal presentation given in the textbook \cite[\S 36]{Heuser:1986}.
   14.46 +Another formal proof of the same theorem has been done in Mizar
   14.47 +\cite{Nowak:1993}.  A general overview of the relevance and history of the
   14.48 +Hahn-Banach theorem is given in \cite{Narici:1996}.
   14.49 +
   14.50 +\medskip The document is structured as follows.  The first part contains
   14.51 +definitions of basic notions of linear algebra: vector spaces, subspaces,
   14.52 +normed spaces, continuous linearforms, norm of functions and an order on
   14.53 +functions by domain extension.  The second part contains some lemmas about the
   14.54 +supremum (w.r.t.\ the function order) and extension of non-maximal functions.
   14.55 +With these preliminaries, the main proof of the theorem (in its two versions)
   14.56 +is conducted in the third part.
   14.57 +
   14.58 +
   14.59 +\clearpage
   14.60 +\part {Basic Notions}
   14.61  
   14.62  \input{Bounds.tex}
   14.63  \input{Aux.tex}
   14.64 @@ -49,15 +59,17 @@
   14.65  \input{FunctionNorm.tex}
   14.66  \input{ZornLemma.tex}
   14.67  
   14.68 -\part {Lemmas for the proof}
   14.69 +\clearpage
   14.70 +\part {Lemmas for the Proof}
   14.71  
   14.72  \input{HahnBanachSupLemmas.tex}
   14.73  \input{HahnBanachExtLemmas.tex}
   14.74  
   14.75 -\part {The proof}
   14.76 +\clearpage
   14.77 +\part {The Main Proof}
   14.78  
   14.79  \input{HahnBanach.tex}
   14.80  \bibliographystyle{abbrv}
   14.81 -\bibliography{bib}
   14.82 +\bibliography{root}
   14.83  
   14.84  \end{document}