final update by Gertrud Bauer;
authorwenzelm
Fri Oct 29 20:18:34 1999 +0200 (1999-10-29)
changeset 79781b99ee57d131
parent 7977 67bfcd3a433c
child 7979 bd9b0151c932
final update by Gertrud Bauer;
src/HOL/Real/HahnBanach/Aux.thy
src/HOL/Real/HahnBanach/Bounds.thy
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/Linearform.thy
src/HOL/Real/HahnBanach/NormedSpace.thy
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/bbb.sty
src/HOL/Real/HahnBanach/document/notation.tex
src/HOL/Real/HahnBanach/document/root.tex
     1.1 --- a/src/HOL/Real/HahnBanach/Aux.thy	Fri Oct 29 19:24:20 1999 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Aux.thy	Fri Oct 29 20:18:34 1999 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4  lemmas chainE2 = chainD2 [elimify];
     1.5  
     1.6  text_raw {* \medskip *};
     1.7 -text{* Lemmas about sets: *};
     1.8 +text{* Lemmas about sets. *};
     1.9  
    1.10  lemma Int_singletonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v";
    1.11    by (fast elim: equalityE);
    1.12 @@ -24,7 +24,7 @@
    1.13   by (force simp add: psubset_eq);
    1.14  
    1.15  text_raw {* \medskip *};
    1.16 -text{* Some lemmas about orders: *};
    1.17 +text{* Some lemmas about orders. *};
    1.18  
    1.19  lemma lt_imp_not_eq: "x < (y::'a::order) ==> x ~= y"; 
    1.20    by (rule order_less_le[RS iffD1, RS conjunct2]);
     2.1 --- a/src/HOL/Real/HahnBanach/Bounds.thy	Fri Oct 29 19:24:20 1999 +0200
     2.2 +++ b/src/HOL/Real/HahnBanach/Bounds.thy	Fri Oct 29 20:18:34 1999 +0200
     2.3 @@ -71,10 +71,12 @@
     2.4  
     2.5  text_raw {* \end{comment} *};
     2.6  
     2.7 -text {* A supremum of an ordered set $B$ w.~r.~t.~$A$ 
     2.8 -is defined as a least upperbound of $B$, which lies in $A$.
     2.9 -The definition of the supremum is based on the
    2.10 -existing definition (see HOL/Real/Lubs.thy).*};
    2.11 +text {*
    2.12 + A supremum\footnote{The definition of the supremum is based on one in
    2.13 + \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Lubs.html}}  of
    2.14 + an ordered set $B$ w.~r.~t.~$A$ is defined as a least upper bound of
    2.15 + $B$, which lies in $A$.
    2.16 +*};
    2.17     
    2.18  text{* If a supremum exists, then $\idt{Sup}\ap A\ap B$
    2.19  is equal to the supremum. *};
    2.20 @@ -114,13 +116,13 @@
    2.21  text_raw {* \end{comment} *};
    2.22  ;
    2.23  
    2.24 -text{* The supremum of $B$ is less than every upper bound
    2.25 +text{* The supremum of $B$ is less than any upper bound
    2.26  of $B$.*};
    2.27  
    2.28  lemma sup_le_ub: "isUb A B y ==> is_Sup A B s ==> s <= y";
    2.29    by (unfold is_Sup_def, rule isLub_le_isUb);
    2.30  
    2.31 -text {* The supremum $B$ is an upperbound for $B$. *};
    2.32 +text {* The supremum $B$ is an upper bound for $B$. *};
    2.33  
    2.34  lemma sup_ub: "y:B ==> is_Sup A B s ==> y <= s";
    2.35    by (unfold is_Sup_def, rule isLubD2);
     3.1 --- a/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri Oct 29 19:24:20 1999 +0200
     3.2 +++ b/src/HOL/Real/HahnBanach/FunctionNorm.thy	Fri Oct 29 20:18:34 1999 +0200
     3.3 @@ -7,110 +7,113 @@
     3.4  
     3.5  theory FunctionNorm = NormedSpace + FunctionOrder:;
     3.6  
     3.7 -subsection {* Continous linearforms*};
     3.8 +subsection {* Continuous linear forms*};
     3.9  
    3.10 -text{* A linearform $f$ on a normed vector space $(V, \norm{\cdot})$
    3.11 -is \emph{continous}, iff it is bounded, i.~e.
    3.12 -\[\exists\ap c\in R.\ap \forall\ap x\in V.\ap 
    3.13 -|f\ap x| \leq c \cdot \norm x\]
    3.14 -In our application no other functions than linearforms are considered,
    3.15 -so we can define continous linearforms as follows:
    3.16 +text{* A linear form $f$ on a normed vector space $(V, \norm{\cdot})$
    3.17 +is \emph{continuous}, iff it is bounded, i.~e.
    3.18 +\[\Ex {c\in R}{\All {x\in V} {|f\ap x| \leq c \cdot \norm x}}\]
    3.19 +In our application no other functions than linear forms are considered,
    3.20 +so we can define continuous linear forms as bounded linear forms:
    3.21  *};
    3.22  
    3.23  constdefs
    3.24 -  is_continous ::
    3.25 +  is_continuous ::
    3.26    "['a::{minus, plus} set, 'a => real, 'a => real] => bool" 
    3.27 -  "is_continous V norm f == 
    3.28 +  "is_continuous V norm f == 
    3.29      is_linearform V f & (EX c. ALL x:V. rabs (f x) <= c * norm x)";
    3.30  
    3.31 -lemma continousI [intro]: 
    3.32 +lemma continuousI [intro]: 
    3.33    "[| is_linearform V f; !! x. x:V ==> rabs (f x) <= c * norm x |] 
    3.34 -  ==> is_continous V norm f";
    3.35 -proof (unfold is_continous_def, intro exI conjI ballI);
    3.36 +  ==> is_continuous V norm f";
    3.37 +proof (unfold is_continuous_def, intro exI conjI ballI);
    3.38    assume r: "!! x. x:V ==> rabs (f x) <= c * norm x"; 
    3.39    fix x; assume "x:V"; show "rabs (f x) <= c * norm x"; by (rule r);
    3.40  qed;
    3.41    
    3.42 -lemma continous_linearform [intro!!]: 
    3.43 -  "is_continous V norm f ==> is_linearform V f";
    3.44 -  by (unfold is_continous_def) force;
    3.45 +lemma continuous_linearform [intro!!]: 
    3.46 +  "is_continuous V norm f ==> is_linearform V f";
    3.47 +  by (unfold is_continuous_def) force;
    3.48  
    3.49 -lemma continous_bounded [intro!!]:
    3.50 -  "is_continous V norm f 
    3.51 +lemma continuous_bounded [intro!!]:
    3.52 +  "is_continuous V norm f 
    3.53    ==> EX c. ALL x:V. rabs (f x) <= c * norm x";
    3.54 -  by (unfold is_continous_def) force;
    3.55 +  by (unfold is_continuous_def) force;
    3.56  
    3.57 -subsection{* The norm of a linearform *};
    3.58 +subsection{* The norm of a linear form *};
    3.59  
    3.60  
    3.61  text{* The least real number $c$ for which holds
    3.62 -\[\forall\ap x\in V.\ap |f\ap x| \leq c \cdot \norm x\]
    3.63 +\[\All {x\in V}{|f\ap x| \leq c \cdot \norm x}\]
    3.64  is called the \emph{norm} of $f$.
    3.65  
    3.66 -For the non-trivial vector space $V$ the norm can be defined as 
    3.67 +For non-trivial vector spaces $V \neq \{\zero\}$ the norm can be defined as 
    3.68  \[\fnorm {f} =\sup_{x\neq\zero}\frac{|f\ap x|}{\norm x} \] 
    3.69  
    3.70 -For the case that the vector space $V$ contains only the $\zero$
    3.71 -vector, the set $B$ this supremum is taken from would be empty, and
    3.72 -any real number is a supremum of $B$. So it must be guarateed that
    3.73 -there is an element in $B$. This element must be ${} \ge 0$ so that
    3.74 +For the case $V = \{\zero\}$ the supremum would be taken from an
    3.75 +empty set. Since $\bbbR$ is unbounded, there would be no supremum.  To
    3.76 +avoid this situation it must be guaranteed that there is an element in
    3.77 +this set. This element must be ${} \ge 0$ so that
    3.78  $\idt{function{\dsh}norm}$ has the norm properties. Furthermore it
    3.79  does not have to change the norm in all other cases, so it must be
    3.80 -$0$, as all other elements of $B$ are ${} \ge 0$.
    3.81 +$0$, as all other elements of are ${} \ge 0$.
    3.82  
    3.83 -Thus $B$ is defined as follows.
    3.84 +Thus we define the set $B$ the supremum is taken from as
    3.85 +\[
    3.86 +\{ 0 \} \Un \left\{ \frac{|f\ap x|}{\norm x} \dt x\neq \zero \And x\in F\right\}
    3.87 + \]
    3.88  *};
    3.89  
    3.90  constdefs
    3.91    B :: "[ 'a set, 'a => real, 'a => real ] => real set"
    3.92    "B V norm f == 
    3.93 -  {z. z = 0r | (EX x:V. x ~= <0> & z = rabs (f x) * rinv (norm x))}";
    3.94 -
    3.95 -text{* $\idt{function{\dsh}norm}$ is equal to the supremum of $B$, 
    3.96 -if there exists a supremum. *};
    3.97 +  {0r} \Un {rabs (f x) * rinv (norm x) | x. x ~= <0> & x:V}";
    3.98  
    3.99 -constdefs 
   3.100 -  function_norm :: " ['a set, 'a => real, 'a => real] => real"
   3.101 -  "function_norm V norm f == Sup UNIV (B V norm f)";
   3.102 -
   3.103 -text{* $\idt{is{\dsh}function{\dsh}norm}$ also guarantees that there 
   3.104 -is a funciton norm .*};
   3.105 +text{* $n$ is the function norm of $f$, iff 
   3.106 +$n$ is the supremum of $B$. 
   3.107 +*};
   3.108  
   3.109  constdefs 
   3.110    is_function_norm :: 
   3.111    " ['a set, 'a => real, 'a => real] => real => bool"
   3.112    "is_function_norm V norm f fn == is_Sup UNIV (B V norm f) fn";
   3.113  
   3.114 +text{* $\idt{function{\dsh}norm}$ is equal to the supremum of $B$, 
   3.115 +if the supremum exists. Otherwise it is undefined. *};
   3.116 +
   3.117 +constdefs 
   3.118 +  function_norm :: " ['a set, 'a => real, 'a => real] => real"
   3.119 +  "function_norm V norm f == Sup UNIV (B V norm f)";
   3.120 +
   3.121  lemma B_not_empty: "0r : B V norm f";
   3.122    by (unfold B_def, force);
   3.123  
   3.124 -text {* The following lemma states every continous linearform on a 
   3.125 -normed space $(V, \norm{\cdot})$ has a function norm. *};
   3.126 +text {* The following lemma states that every continuous linear form
   3.127 +on a normed space $(V, \norm{\cdot})$ has a function norm. *};
   3.128  
   3.129  lemma ex_fnorm [intro!!]: 
   3.130 -  "[| is_normed_vectorspace V norm; is_continous V norm f|]
   3.131 +  "[| is_normed_vectorspace V norm; is_continuous V norm f|]
   3.132       ==> is_function_norm V norm f (function_norm V norm f)"; 
   3.133  proof (unfold function_norm_def is_function_norm_def 
   3.134 -  is_continous_def Sup_def, elim conjE, rule selectI2EX);
   3.135 +  is_continuous_def Sup_def, elim conjE, rule selectI2EX);
   3.136    assume "is_normed_vectorspace V norm";
   3.137    assume "is_linearform V f" 
   3.138    and e: "EX c. ALL x:V. rabs (f x) <= c * norm x";
   3.139  
   3.140    txt {* The existence of the supremum is shown using the 
   3.141    completeness of the reals. Completeness means, that
   3.142 -  for every non-empty and bounded set of reals there exists a 
   3.143 +  every non-empty bounded set of reals has a 
   3.144    supremum. *};
   3.145    show  "EX a. is_Sup UNIV (B V norm f) a"; 
   3.146    proof (unfold is_Sup_def, rule reals_complete);
   3.147  
   3.148 -    txt {* First we have to show that $B$ is non-empty. *}; 
   3.149 +    txt {* First we have to show that $B$ is non-empty: *}; 
   3.150  
   3.151      show "EX X. X : B V norm f"; 
   3.152      proof (intro exI);
   3.153        show "0r : (B V norm f)"; by (unfold B_def, force);
   3.154      qed;
   3.155  
   3.156 -    txt {* Then we have to show that $B$ is bounded. *};
   3.157 +    txt {* Then we have to show that $B$ is bounded: *};
   3.158  
   3.159      from e; show "EX Y. isUb UNIV (B V norm f) Y";
   3.160      proof;
   3.161 @@ -122,19 +125,18 @@
   3.162  
   3.163        show "?thesis";
   3.164        proof (intro exI isUbI setleI ballI, unfold B_def, 
   3.165 -	elim CollectE disjE bexE conjE);
   3.166 +	elim UnE CollectE exE conjE singletonE);
   3.167  
   3.168          txt{* To proof the thesis, we have to show that there is 
   3.169 -        some constant b, which is greater than every $y$ in $B$. 
   3.170 +        some constant $b$, such that $y \leq b$ for all $y\in B$. 
   3.171          Due to the definition of $B$ there are two cases for
   3.172 -        $y\in B$. If $y = 0$ then $y$ is less than 
   3.173 -        $\idt{max}\ap c\ap 0$: *};
   3.174 +        $y\in B$. If $y = 0$ then $y \leq idt{max}\ap c\ap 0$: *};
   3.175  
   3.176  	fix y; assume "y = 0r";
   3.177          show "y <= b"; by (simp! add: le_max2);
   3.178  
   3.179          txt{* The second case is 
   3.180 -        $y = \frac{|f\ap x|}{\norm x}$ for some 
   3.181 +        $y = {|f\ap x|}/{\norm x}$ for some 
   3.182          $x\in V$ with $x \neq \zero$. *};
   3.183  
   3.184        next;
   3.185 @@ -186,13 +188,13 @@
   3.186    qed;
   3.187  qed;
   3.188  
   3.189 -text {* The norm of a continous function is always $\geq 0$. *};
   3.190 +text {* The norm of a continuous function is always $\geq 0$. *};
   3.191  
   3.192  lemma fnorm_ge_zero [intro!!]: 
   3.193 -  "[| is_continous V norm f; is_normed_vectorspace V norm|]
   3.194 +  "[| is_continuous V norm f; is_normed_vectorspace V norm|]
   3.195     ==> 0r <= function_norm V norm f";
   3.196  proof -;
   3.197 -  assume c: "is_continous V norm f" 
   3.198 +  assume c: "is_continuous V norm f" 
   3.199       and n: "is_normed_vectorspace V norm";
   3.200  
   3.201    txt {* The function norm is defined as the supremum of $B$. 
   3.202 @@ -202,9 +204,9 @@
   3.203    show ?thesis; 
   3.204    proof (unfold function_norm_def, rule sup_ub1);
   3.205      show "ALL x:(B V norm f). 0r <= x"; 
   3.206 -    proof (intro ballI, unfold B_def, 
   3.207 -           elim CollectE bexE conjE disjE);
   3.208 -      fix x r; 
   3.209 +    proof (intro ballI, unfold B_def,
   3.210 +           elim UnE singletonE CollectE exE conjE); 
   3.211 +      fix x r;
   3.212        assume "x : V" "x ~= <0>" 
   3.213          and r: "r = rabs (f x) * rinv (norm x)";
   3.214  
   3.215 @@ -218,33 +220,33 @@
   3.216            qed;
   3.217          qed; ***)
   3.218        with ge; show "0r <= r";
   3.219 -       by (simp only: r,rule real_le_mult_order);
   3.220 +       by (simp only: r, rule real_le_mult_order);
   3.221      qed (simp!);
   3.222  
   3.223 -    txt {* Since $f$ is continous the function norm exists. *};
   3.224 +    txt {* Since $f$ is continuous the function norm exists: *};
   3.225  
   3.226      have "is_function_norm V norm f (function_norm V norm f)"; ..;
   3.227      thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"; 
   3.228 -      by (unfold is_function_norm_def, unfold function_norm_def);
   3.229 +      by (unfold is_function_norm_def function_norm_def);
   3.230  
   3.231 -    txt {* $B$ is non-empty by construction. *};
   3.232 +    txt {* $B$ is non-empty by construction: *};
   3.233  
   3.234      show "0r : B V norm f"; by (rule B_not_empty);
   3.235    qed;
   3.236  qed;
   3.237    
   3.238 -text{* The basic property of function norms is: 
   3.239 +text{* \medskip The fundamental property of function norms is: 
   3.240  \begin{matharray}{l}
   3.241  | f\ap x | \leq {\fnorm {f}} \cdot {\norm x}  
   3.242  \end{matharray}
   3.243  *};
   3.244  
   3.245  lemma norm_fx_le_norm_f_norm_x: 
   3.246 -  "[| is_normed_vectorspace V norm; x:V; is_continous V norm f |] 
   3.247 -    ==> rabs (f x) <= (function_norm V norm f) * norm x"; 
   3.248 +  "[| is_normed_vectorspace V norm; x:V; is_continuous V norm f |] 
   3.249 +    ==> rabs (f x) <= function_norm V norm f * norm x"; 
   3.250  proof -; 
   3.251    assume "is_normed_vectorspace V norm" "x:V" 
   3.252 -  and c: "is_continous V norm f";
   3.253 +  and c: "is_continuous V norm f";
   3.254    have v: "is_vectorspace V"; ..;
   3.255    assume "x:V";
   3.256  
   3.257 @@ -259,7 +261,7 @@
   3.258  
   3.259      assume "x = <0>";
   3.260      have "rabs (f x) = rabs (f <0>)"; by (simp!);
   3.261 -    also; from v continous_linearform; have "f <0> = 0r"; ..;
   3.262 +    also; from v continuous_linearform; have "f <0> = 0r"; ..;
   3.263      also; note rabs_zero;
   3.264      also; have "0r <= function_norm V norm f * norm x";
   3.265      proof (rule real_le_mult_order);
   3.266 @@ -286,11 +288,11 @@
   3.267        show "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))";
   3.268           by (simp! add: is_function_norm_def function_norm_def);
   3.269        show "rabs (f x) * rinv (norm x) : B V norm f"; 
   3.270 -        by (unfold B_def, intro CollectI disjI2 bexI [of _ x]
   3.271 +        by (unfold B_def, intro UnI2 CollectI exI [of _ x]
   3.272              conjI, simp);
   3.273      qed;
   3.274  
   3.275 -    txt {* The thesis follows by a short calculation: *};
   3.276 +    txt {* The thesis now follows by a short calculation: *};
   3.277  
   3.278      have "rabs (f x) = rabs (f x) * 1r"; by (simp!);
   3.279      also; from nz; have "1r = rinv (norm x) * norm x"; 
   3.280 @@ -305,21 +307,20 @@
   3.281    qed;
   3.282  qed;
   3.283  
   3.284 -text{* The function norm is the least positive real number for 
   3.285 -which the inequation
   3.286 +text{* \medskip The function norm is the least positive real number for 
   3.287 +which the following inequation holds:
   3.288  \begin{matharray}{l}
   3.289  | f\ap x | \leq c \cdot {\norm x}  
   3.290  \end{matharray} 
   3.291 -holds.
   3.292  *};
   3.293  
   3.294  lemma fnorm_le_ub: 
   3.295 -  "[| is_normed_vectorspace V norm; is_continous V norm f;
   3.296 +  "[| is_normed_vectorspace V norm; is_continuous V norm f;
   3.297       ALL x:V. rabs (f x) <= c * norm x; 0r <= c |]
   3.298    ==> function_norm V norm f <= c";
   3.299  proof (unfold function_norm_def);
   3.300    assume "is_normed_vectorspace V norm"; 
   3.301 -  assume c: "is_continous V norm f";
   3.302 +  assume c: "is_continuous V norm f";
   3.303    assume fb: "ALL x:V. rabs (f x) <= c * norm x"
   3.304           and "0r <= c";
   3.305  
   3.306 @@ -342,7 +343,7 @@
   3.307      proof (intro isUbI setleI ballI);
   3.308        fix y; assume "y: B V norm f";
   3.309        thus le: "y <= c";
   3.310 -      proof (unfold B_def, elim CollectE disjE bexE conjE);
   3.311 +      proof (unfold B_def, elim UnE CollectE exE conjE singletonE);
   3.312  
   3.313         txt {* The first case for $y\in B$ is $y=0$. *};
   3.314  
   3.315 @@ -350,7 +351,7 @@
   3.316          show "y <= c"; by (force!);
   3.317  
   3.318          txt{* The second case is 
   3.319 -        $y = \frac{|f\ap x|}{\norm x}$ for some 
   3.320 +        $y = {|f\ap x|}/{\norm x}$ for some 
   3.321          $x\in V$ with $x \neq \zero$. *};  
   3.322  
   3.323        next;
     4.1 --- a/src/HOL/Real/HahnBanach/FunctionOrder.thy	Fri Oct 29 19:24:20 1999 +0200
     4.2 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Fri Oct 29 20:18:34 1999 +0200
     4.3 @@ -3,29 +3,26 @@
     4.4      Author:     Gertrud Bauer, TU Munich
     4.5  *)
     4.6  
     4.7 -header {* An Order on functions *};
     4.8 +header {* An order on functions *};
     4.9  
    4.10  theory FunctionOrder = Subspace + Linearform:;
    4.11  
    4.12 -
    4.13  subsection {* The graph of a function *};
    4.14  
    4.15 -text{* We define the \emph{graph} of a (real) function $f$ with the 
    4.16 +text{* We define the \emph{graph} of a (real) function $f$ with
    4.17  domain $F$ as the set 
    4.18  \[
    4.19  \{(x, f\ap x). \ap x:F\}
    4.20  \]
    4.21 -So we are modelling partial functions by specifying the domain and 
    4.22 -the mapping function. We use the notion ``function'' also for the graph
    4.23 -of a function. 
    4.24 +So we are modeling partial functions by specifying the domain and 
    4.25 +the mapping function. We use the term ``function'' also for its graph.
    4.26  *};
    4.27  
    4.28 -types 'a graph = "('a::{minus, plus} * real) set";
    4.29 +types 'a graph = "('a * real) set";
    4.30  
    4.31  constdefs
    4.32    graph :: "['a set, 'a => real] => 'a graph "
    4.33 -  "graph F f == {p. EX x. p = (x, f x) & x:F}"; (* 
    4.34 -   == {(x, f x). x:F} *)
    4.35 +  "graph F f == {(x, f x) | x. x:F}"; 
    4.36  
    4.37  lemma graphI [intro!!]: "x:F ==> (x, f x) : graph F f";
    4.38    by (unfold graph_def, intro CollectI exI) force;
    4.39 @@ -41,7 +38,7 @@
    4.40  
    4.41  subsection {* Functions ordered by domain extension *};
    4.42  
    4.43 -text{* The function $h'$ is an extension of $h$, iff the graph of 
    4.44 +text{* A function $h'$ is an extension of $h$, iff the graph of 
    4.45  $h$ is a subset of the graph of $h'$.*};
    4.46  
    4.47  lemma graph_extI: 
    4.48 @@ -83,7 +80,7 @@
    4.49  lemma graph_domain_funct: 
    4.50    "(!!x y z. (x, y):g ==> (x, z):g ==> z = y) 
    4.51    ==> graph (domain g) (funct g) = g";
    4.52 -proof (unfold domain_def, unfold funct_def, unfold graph_def, auto);
    4.53 +proof (unfold domain_def funct_def graph_def, auto);
    4.54    fix a b; assume "(a, b) : g";
    4.55    show "(a, SOME y. (a, y) : g) : g"; by (rule selectI2);
    4.56    show "EX y. (a, y) : g"; ..;
    4.57 @@ -96,9 +93,9 @@
    4.58  
    4.59  
    4.60  
    4.61 -subsection {* Norm preserving extensions of a function *};
    4.62 +subsection {* Norm-preserving extensions of a function *};
    4.63  
    4.64 -text {* Given a function $f$ on the space $F$ and a quasinorm $p$ on 
    4.65 +text {* Given a linear form $f$ on the space $F$ and a seminorm $p$ on 
    4.66  $E$. The set of all linear extensions of $f$, to superspaces $H$ of 
    4.67  $F$, which are bounded by $p$, is defined as follows. *};
    4.68  
     5.1 --- a/src/HOL/Real/HahnBanach/HahnBanach.thy	Fri Oct 29 19:24:20 1999 +0200
     5.2 +++ b/src/HOL/Real/HahnBanach/HahnBanach.thy	Fri Oct 29 20:18:34 1999 +0200
     5.3 @@ -1,6 +1,6 @@
     5.4  (*  Title:      HOL/Real/HahnBanach/HahnBanach.thy
     5.5      ID:         $Id$
     5.6 -    Author:     Gertrud Baueer, TU Munich
     5.7 +    Author:     Gertrud Bauer, TU Munich
     5.8  *)
     5.9  
    5.10  header {* The Hahn-Banach Theorem *};
    5.11 @@ -15,18 +15,19 @@
    5.12  
    5.13  subsection {* The case of general linear spaces *};
    5.14  
    5.15 -text  {* Every linearform $f$ on a subspace $F$ of $E$, which is 
    5.16 - bounded by some  quasinorm $q$ on $E$, can be extended 
    5.17 - to a function on $E$ in a norm preseving way. *};
    5.18 +text  {* Let $f$ be a linear form $f$ defined on a subspace $F$ 
    5.19 + of a norm vector space $E$. If $f$ is  
    5.20 + bounded by some seminorm $q$ on $E$, it can be extended 
    5.21 + to a function on $E$ in a norm-preserving way. *};
    5.22  
    5.23  theorem HahnBanach: 
    5.24 -  "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; 
    5.25 +  "[| is_vectorspace E; is_subspace F E; is_seminorm E p; 
    5.26    is_linearform F f; ALL x:F. f x <= p x |]
    5.27    ==> EX h. is_linearform E h
    5.28            & (ALL x:F. h x = f x)
    5.29            & (ALL x:E. h x <= p x)";
    5.30  proof -;
    5.31 -  assume "is_vectorspace E" "is_subspace F E" "is_quasinorm E p"
    5.32 +  assume "is_vectorspace E" "is_subspace F E" "is_seminorm E p"
    5.33           "is_linearform F f" "ALL x:F. f x <= p x";
    5.34    
    5.35    txt{* We define $M$ to be the set of all linear extensions 
    5.36 @@ -42,19 +43,18 @@
    5.37      thus "is_subspace F F"; ..;
    5.38    qed (blast!)+;
    5.39  
    5.40 -  subsubsect {* Existence of a limit function of the norm preserving
    5.41 +  subsubsect {* Existence of a limit function the norm-preserving
    5.42    extensions *}; 
    5.43  
    5.44 -  txt {* For every non-empty chain of norm preserving functions
    5.45 -  the union of all functions in the chain is again a norm preserving
    5.46 -  function. (The union is an upper bound for all elements. 
    5.47 +  txt {* For every non-empty chain of norm-preserving extensions
    5.48 +  the union of all functions in the chain is again a norm-preserving
    5.49 +  extension. (The union is an upper bound for all elements. 
    5.50    It is even the least upper bound, because every upper bound of $M$
    5.51    is also an upper bound for $\Union c$.) *};
    5.52  
    5.53 -  have "!! c. [| c : chain M; EX x. x:c |] ==> Union c : M";  
    5.54 -  proof -;
    5.55 +  {{;
    5.56      fix c; assume "c:chain M" "EX x. x:c";
    5.57 -    show "Union c : M";
    5.58 +    have "Union c : M";
    5.59  
    5.60      proof (unfold M_def, rule norm_pres_extensionI);
    5.61        show "EX (H::'a set) h::'a => real. graph H h = Union c
    5.62 @@ -67,29 +67,25 @@
    5.63          let ?H = "domain (Union c)";
    5.64          let ?h = "funct (Union c)";
    5.65  
    5.66 -        show a [simp]: "graph ?H ?h = Union c"; 
    5.67 +        show a: "graph ?H ?h = Union c"; 
    5.68          proof (rule graph_domain_funct);
    5.69            fix x y z; assume "(x, y) : Union c" "(x, z) : Union c";
    5.70            show "z = y"; by (rule sup_definite);
    5.71          qed;
    5.72              
    5.73 -        show "is_linearform ?H ?h"; 
    5.74 +        show "is_linearform ?H ?h";  
    5.75            by (simp! add: sup_lf a);
    5.76 -
    5.77          show "is_subspace ?H E"; 
    5.78            by (rule sup_subE, rule a) (simp!)+;
    5.79 - 
    5.80          show "is_subspace F ?H"; 
    5.81            by (rule sup_supF, rule a) (simp!)+;
    5.82 -
    5.83          show "graph F f <= graph ?H ?h"; 
    5.84            by (rule sup_ext, rule a) (simp!)+;
    5.85 -
    5.86          show "ALL x::'a:?H. ?h x <= p x"; 
    5.87            by (rule sup_norm_pres, rule a) (simp!)+;
    5.88        qed;
    5.89      qed;
    5.90 -  qed;
    5.91 +  }};
    5.92   
    5.93    txt {* According to Zorn's Lemma there is
    5.94    a maximal norm-preserving extension $g\in M$. *};
    5.95 @@ -120,19 +116,18 @@
    5.96        have h: "is_vectorspace H"; ..;
    5.97        have f: "is_vectorspace F"; ..;
    5.98  
    5.99 -subsubsect {* The domain of the limit function. *};
   5.100 +subsubsect {* The domain of the limit function *};
   5.101  
   5.102  have eq: "H = E"; 
   5.103  proof (rule classical);
   5.104  
   5.105 -txt {* Assume the domain of the supremum is not $E$. *};
   5.106 +txt {* Assume that the domain of the supremum is not $E$, *};
   5.107  ;
   5.108    assume "H ~= E";
   5.109    have "H <= E"; ..;
   5.110    hence "H < E"; ..;
   5.111   
   5.112 -  txt{* Then there exists an element $x_0$ in 
   5.113 -  the difference of $E$ and $H$. *};
   5.114 +  txt{* then there exists an element $x_0$ in $E \ H$: *};
   5.115  
   5.116    hence "EX x0:E. x0~:H"; 
   5.117      by (rule set_less_imp_diff_not_empty);
   5.118 @@ -153,16 +148,16 @@
   5.119      qed blast;
   5.120  
   5.121      txt {* Define $H_0$ as the (direct) sum of H and the 
   5.122 -    linear closure of $x_0$.*};
   5.123 +    linear closure of $x_0$. \label{ex-xi-use}*};
   5.124  
   5.125      def H0 == "H + lin x0";
   5.126  
   5.127 -    from h; have xi: "EX xi. (ALL y:H. - p (y + x0) - h y <= xi)
   5.128 -                     & (ALL y:H. xi <= p (y + x0) - h y)";
   5.129 +    from h; have xi: "EX xi. ALL y:H. - p (y + x0) - h y <= xi 
   5.130 +                                    & xi <= p (y + x0) - h y";
   5.131      proof (rule ex_xi);
   5.132        fix u v; assume "u:H" "v:H";
   5.133        from h; have "h v - h u = h (v - u)";
   5.134 -         by (simp! add: linearform_diff_linear);
   5.135 +         by (simp! add: linearform_diff);
   5.136        also; from h_bound; have "... <= p (v - u)";
   5.137          by (simp!);
   5.138        also; have "v - u = x0 + - x0 + v + - u";
   5.139 @@ -172,7 +167,7 @@
   5.140        also; have "... = (v + x0) - (u + x0)";
   5.141          by (simp! add: diff_eq1);
   5.142        also; have "p ... <= p (v + x0) + p (u + x0)";
   5.143 -         by (rule quasinorm_diff_triangle_ineq) (simp!)+;
   5.144 +         by (rule seminorm_diff_subadditive) (simp!)+;
   5.145        finally; have "h v - h u <= p (v + x0) + p (u + x0)"; .;
   5.146  
   5.147        thus "- p (u + x0) - h u <= p (v + x0) - h v";
   5.148 @@ -182,13 +177,14 @@
   5.149                 & graph H0 h0 : M"; 
   5.150      proof (elim exE, intro exI conjI);
   5.151        fix xi; 
   5.152 -      assume a: "(ALL y:H. - p (y + x0) - h y <= xi) 
   5.153 -               & (ALL y:H. xi <= p (y + x0) - h y)";
   5.154 +      assume a: "ALL y:H. - p (y + x0) - h y <= xi 
   5.155 +                        & xi <= p (y + x0) - h y";
   5.156       
   5.157 -      txt {* Define $h_0$ as the linear extension of $h$ on $H_0$:*};  
   5.158 +      txt {* Define $h_0$ as the canonical linear extension 
   5.159 +      of $h$ on $H_0$:*};  
   5.160  
   5.161        def h0 ==
   5.162 -          "\<lambda>x. let (y,a) = SOME (y, a). (x = y + a <*> x0 & y:H)
   5.163 +          "\<lambda>x. let (y,a) = SOME (y, a). x = y + a <*> x0 & y:H
   5.164                 in (h y) + a * xi";
   5.165  
   5.166        txt {* We get that the graph of $h_0$ extend that of
   5.167 @@ -230,15 +226,13 @@
   5.168        qed;
   5.169        thus "g ~= graph H0 h0"; by (simp!);
   5.170  
   5.171 -      txt {* Furthermore  $h_0$ is a norm preserving extension 
   5.172 +      txt {* Furthermore  $h_0$ is a norm-preserving extension 
   5.173       of $f$. *};
   5.174  
   5.175        have "graph H0 h0 : norm_pres_extensions E p F f";
   5.176        proof (rule norm_pres_extensionI2);
   5.177 -
   5.178          show "is_linearform H0 h0";
   5.179            by (rule h0_lf, rule x0) (simp!)+;
   5.180 -
   5.181          show "is_subspace H0 E";
   5.182            by (unfold H0_def, rule vs_sum_subspace, 
   5.183               rule lin_subspace);
   5.184 @@ -314,23 +308,24 @@
   5.185  
   5.186  subsection  {* An alternative formulation of the theorem *};
   5.187  
   5.188 -text {* The following alternative formulation of the 
   5.189 -Hahn-Banach Theorem uses the fact that for
   5.190 -real numbers the following inequations are equivalent:
   5.191 +text {* The following alternative formulation of the Hahn-Banach
   5.192 +Theorem\label{rabs-HahnBanach} uses the fact that for real numbers the
   5.193 +following inequations are equivalent:\footnote{This was shown in lemma
   5.194 +$\idt{rabs{\dsh}ineq{\dsh}iff}$ (see page \pageref{rabs-ineq-iff}).}
   5.195  \begin{matharray}{ll}
   5.196  \forall x\in H.\ap |h\ap x|\leq p\ap x& {\rm and}\\
   5.197  \forall x\in H.\ap h\ap x\leq p\ap x\\
   5.198  \end{matharray}
   5.199 -(This was shown in lemma $\idt{rabs{\dsh}ineq}$.) *};
   5.200 +*};
   5.201  
   5.202  theorem rabs_HahnBanach:
   5.203 -  "[| is_vectorspace E; is_subspace F E; is_quasinorm E p; 
   5.204 +  "[| is_vectorspace E; is_subspace F E; is_seminorm E p; 
   5.205    is_linearform F f; ALL x:F. rabs (f x) <= p x |]
   5.206    ==> EX g. is_linearform E g
   5.207            & (ALL x:F. g x = f x)
   5.208            & (ALL x:E. rabs (g x) <= p x)";
   5.209  proof -; 
   5.210 -  assume e: "is_vectorspace E" "is_subspace F E" "is_quasinorm E p" 
   5.211 +  assume e: "is_vectorspace E" "is_subspace F E" "is_seminorm E p" 
   5.212              "is_linearform F f"  "ALL x:F. rabs (f x) <= p x";
   5.213    have "ALL x:F. f x <= p x"; 
   5.214      by (rule rabs_ineq_iff [RS iffD1]);
   5.215 @@ -352,36 +347,35 @@
   5.216  
   5.217  subsection {* The Hahn-Banach Theorem for normed spaces *};
   5.218  
   5.219 -text  {* Every continous linear function $f$ on a subspace of $E$, 
   5.220 -  can be extended to a continous function on $E$ with the same 
   5.221 -  function norm. *};
   5.222 +text {* Every continuous linear form $f$ on a subspace $F$ of a
   5.223 +norm space $E$, can be extended to a continuous linear form $g$ on
   5.224 +$E$ such that $\fnorm{f} = \fnorm {g}$. *};
   5.225  
   5.226  theorem norm_HahnBanach:
   5.227    "[| is_normed_vectorspace E norm; is_subspace F E; 
   5.228 -  is_linearform F f; is_continous F norm f |] 
   5.229 +  is_linearform F f; is_continuous F norm f |] 
   5.230    ==> EX g. is_linearform E g
   5.231 -         & is_continous E norm g 
   5.232 +         & is_continuous E norm g 
   5.233           & (ALL x:F. g x = f x) 
   5.234           & function_norm E norm g = function_norm F norm f";
   5.235  proof -;
   5.236    assume e_norm: "is_normed_vectorspace E norm";
   5.237    assume f: "is_subspace F E" "is_linearform F f";
   5.238 -  assume f_cont: "is_continous F norm f";
   5.239 +  assume f_cont: "is_continuous F norm f";
   5.240    have e: "is_vectorspace E"; ..;
   5.241    with _; have f_norm: "is_normed_vectorspace F norm"; ..;
   5.242  
   5.243    txt{* We define the function $p$ on $E$ as follows:
   5.244    \begin{matharray}{l}
   5.245 -  p\ap x = \fnorm f \cdot \norm x\\
   5.246 -  % p\ap x = \fnorm f \cdot \fnorm x\\
   5.247 +  p \ap x = \fnorm f \cdot \norm x\\
   5.248    \end{matharray}
   5.249    *};
   5.250  
   5.251    def p == "\<lambda>x. function_norm F norm f * norm x";
   5.252    
   5.253 -  txt{* $p$ is a quasinorm on $E$: *};
   5.254 +  txt{* $p$ is a seminorm on $E$: *};
   5.255  
   5.256 -  have q: "is_quasinorm E p";
   5.257 +  have q: "is_seminorm E p";
   5.258    proof;
   5.259      fix x y a; assume "x:E" "y:E";
   5.260  
   5.261 @@ -393,14 +387,14 @@
   5.262        show "0r <= norm x"; ..;
   5.263      qed;
   5.264  
   5.265 -    txt{* $p$ is multiplicative: *};
   5.266 +    txt{* $p$ is absolutely homogenous: *};
   5.267  
   5.268      show "p (a <*> x) = rabs a * p x";
   5.269      proof -; 
   5.270        have "p (a <*> x) = function_norm F norm f * norm (a <*> x)";
   5.271          by (simp!);
   5.272        also; have "norm (a <*> x) = rabs a * norm x"; 
   5.273 -        by (rule normed_vs_norm_mult_distrib);
   5.274 +        by (rule normed_vs_norm_rabs_homogenous);
   5.275        also; have "function_norm F norm f * (rabs a * norm x) 
   5.276          = rabs a * (function_norm F norm f * norm x)";
   5.277          by (simp! only: real_mult_left_commute);
   5.278 @@ -408,7 +402,7 @@
   5.279        finally; show ?thesis; .;
   5.280      qed;
   5.281  
   5.282 -    txt{* Furthermore, $p$ obeys the triangle inequation: *};
   5.283 +    txt{* Furthermore, $p$ is subadditive: *};
   5.284  
   5.285      show "p (x + y) <= p x + p y";
   5.286      proof -;
   5.287 @@ -436,10 +430,10 @@
   5.288         by (simp! add: norm_fx_le_norm_f_norm_x);
   5.289    qed;
   5.290  
   5.291 -  txt{* Using the facts that $p$ is a quasinorm and 
   5.292 -  $f$ is bounded we can apply the Hahn-Banach Theorem for real
   5.293 -  vector spaces. 
   5.294 -  So $f$ can be extended in a norm preserving way to some function
   5.295 +  txt{* Using the fact that $p$ is a seminorm and 
   5.296 +  $f$ is bounded by $q$ we can apply the Hahn-Banach Theorem 
   5.297 +  for real vector spaces. 
   5.298 +  So $f$ can be extended in a norm-preserving way to some function
   5.299    $g$ on the whole vector space $E$. *};
   5.300  
   5.301    with e f q; 
   5.302 @@ -451,36 +445,43 @@
   5.303    proof (elim exE conjE); 
   5.304      fix g;
   5.305      assume "is_linearform E g" and a: "ALL x:F. g x = f x" 
   5.306 -       and "ALL x:E. rabs (g x) <= p x";
   5.307 +       and b: "ALL x:E. rabs (g x) <= p x";
   5.308  
   5.309      show "EX g. is_linearform E g 
   5.310 -            & is_continous E norm g 
   5.311 +            & is_continuous E norm g 
   5.312              & (ALL x:F. g x = f x) 
   5.313              & function_norm E norm g = function_norm F norm f";
   5.314      proof (intro exI conjI);
   5.315  
   5.316 -    txt{* To complete the proof, we show that this function
   5.317 -    $g$ is also continous and has the same function norm as
   5.318 -    $f$. *};
   5.319 +    txt{* We futhermore have to show that 
   5.320 +    $g$ is also continuous: *};
   5.321  
   5.322 -      show g_cont: "is_continous E norm g";
   5.323 +      show g_cont: "is_continuous E norm g";
   5.324        proof;
   5.325          fix x; assume "x:E";
   5.326 +        from b [RS bspec, OF this]; 
   5.327          show "rabs (g x) <= function_norm F norm f * norm x";
   5.328 -          by (rule bspec [of _ _ x], (simp!));
   5.329 +          by (unfold p_def);
   5.330        qed; 
   5.331  
   5.332 +      txt {* To complete the proof, we show that 
   5.333 +      $\fnorm g = \fnorm f$. *};
   5.334 +
   5.335        show "function_norm E norm g = function_norm F norm f"
   5.336          (is "?L = ?R");
   5.337        proof (rule order_antisym);
   5.338  
   5.339 -        txt{* $\idt{function{\dsh}norm}\ap F\ap \idt{norm}\ap f$ is 
   5.340 -        a solution
   5.341 -        for the inequation 
   5.342 +        txt{* First we show $\fnorm g \leq \fnorm f$.  The function norm
   5.343 +        $\fnorm g$ is defined as the smallest $c\in\bbbR$ such that
   5.344          \begin{matharray}{l}
   5.345 -        \forall\ap x\in E.\ap |g\ap x| \leq c \cdot \norm x
   5.346 -        \end{matharray} *};
   5.347 -
   5.348 +        \All {x\in E} {|g\ap x| \leq c \cdot \norm x}
   5.349 +        \end{matharray}
   5.350 +        Furthermore holds
   5.351 +        \begin{matharray}{l}
   5.352 +        \All {x\in E} {|g\ap x| \leq \fnorm f \cdot \norm x}
   5.353 +        \end{matharray}
   5.354 +        *};
   5.355 + 
   5.356          have "ALL x:E. rabs (g x) <= function_norm F norm f * norm x";
   5.357          proof;
   5.358            fix x; assume "x:E"; 
   5.359 @@ -488,12 +489,7 @@
   5.360              by (simp!);
   5.361          qed;
   5.362  
   5.363 -        txt{* Since
   5.364 -         $\idt{function{\dsh}norm}\ap E\ap \idt{norm}\ap g$
   5.365 -        is the smallest solution for this inequation, we have: *};
   5.366 -
   5.367 -        with _ g_cont;
   5.368 -        show "?L <= ?R";
   5.369 +        with _ g_cont; show "?L <= ?R";
   5.370          proof (rule fnorm_le_ub);
   5.371            from f_cont f_norm; show "0r <= function_norm F norm f"; ..;
   5.372          qed;
     6.1 --- a/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Fri Oct 29 19:24:20 1999 +0200
     6.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachExtLemmas.thy	Fri Oct 29 20:18:34 1999 +0200
     6.3 @@ -3,88 +3,89 @@
     6.4      Author:     Gertrud Bauer, TU Munich
     6.5  *)
     6.6  
     6.7 -header {* Extending a non-maximal function *};
     6.8 +header {* Extending non-maximal functions *};
     6.9  
    6.10  theory HahnBanachExtLemmas = FunctionNorm:;
    6.11  
    6.12  text{* In this section the following context is presumed.
    6.13  Let $E$ be a real vector space with a 
    6.14 -quasinorm $q$ on $E$. $F$ is a subspace of $E$ and $f$ a linear 
    6.15 +seminorm $q$ on $E$. $F$ is a subspace of $E$ and $f$ a linear 
    6.16  function on $F$. We consider a subspace $H$ of $E$ that is a 
    6.17 -superspace of $F$ and a linearform $h$ on $H$. $H$ is a not equal 
    6.18 +superspace of $F$ and a linear form $h$ on $H$. $H$ is a not equal 
    6.19  to $E$ and $x_0$ is an element in $E \backslash H$.
    6.20  $H$ is extended to the direct sum  $H_0 = H + \idt{lin}\ap x_0$, so for
    6.21  any $x\in H_0$ the decomposition of $x = y + a \mult x$ 
    6.22  with $y\in H$ is unique. $h_0$ is defined on $H_0$ by  
    6.23 -$h_0 x = h y + a \cdot \xi$ for some $\xi$.
    6.24 +$h_0\ap x = h\ap y + a \cdot \xi$ for a certain $\xi$.
    6.25  
    6.26  Subsequently we show some properties of this extension $h_0$ of $h$.
    6.27  *}; 
    6.28  
    6.29  
    6.30 -text {* This lemma will be used to show the existence of a linear 
    6.31 -extension of $f$. It is a conclusion of the completenesss of the 
    6.32 -reals. To show 
    6.33 +text {* This lemma will be used to show the existence of a linear
    6.34 +extension of $f$ (see page \pageref{ex-xi-use}). 
    6.35 +It is a consequence
    6.36 +of the completeness of $\bbbR$. To show 
    6.37  \begin{matharray}{l}
    6.38 -\exists \xi. \ap (\forall y\in F.\ap a\ap y \leq \xi) \land (\forall y\in F.\ap xi \leq b\ap y)
    6.39 -\end{matharray}
    6.40 +\Ex{\xi}{\All {y\in F}{a\ap y \leq \xi \land \xi \leq b\ap y}}
    6.41 +\end{matharray} 
    6.42  it suffices to show that 
    6.43 -\begin{matharray}{l}
    6.44 -\forall u\in F. \ap\forall v\in F. \ap a\ap u \leq b \ap v
    6.45 -\end{matharray}
    6.46 -*};
    6.47 +\begin{matharray}{l} \All
    6.48 +{u\in F}{\All {v\in F}{a\ap u \leq b \ap v}} 
    6.49 +\end{matharray} *};
    6.50  
    6.51  lemma ex_xi: 
    6.52    "[| is_vectorspace F; !! u v. [| u:F; v:F |] ==> a u <= b v |]
    6.53 -  ==> EX (xi::real). (ALL y:F. a y <= xi) & (ALL y:F. xi <= b y)"; 
    6.54 +  ==> EX (xi::real). ALL y:F. a y <= xi & xi <= b y"; 
    6.55  proof -;
    6.56    assume vs: "is_vectorspace F";
    6.57    assume r: "(!! u v. [| u:F; v:F |] ==> a u <= (b v::real))";
    6.58  
    6.59    txt {* From the completeness of the reals follows:
    6.60    The set $S = \{a\ap u.\ap u\in F\}$ has a supremum, if
    6.61 -  it is non-empty and if it has an upperbound. *};
    6.62 +  it is non-empty and has an upper bound. *};
    6.63  
    6.64 -  let ?S = "{s::real. EX u:F. s = a u}";
    6.65 +  let ?S = "{a u :: real | u. u:F}";
    6.66  
    6.67    have "EX xi. isLub UNIV ?S xi";  
    6.68    proof (rule reals_complete);
    6.69    
    6.70 -    txt {* The set $S$ is non-empty, since $a\ap\zero \in S$ *};
    6.71 +    txt {* The set $S$ is non-empty, since $a\ap\zero \in S$: *};
    6.72  
    6.73      from vs; have "a <0> : ?S"; by force;
    6.74      thus "EX X. X : ?S"; ..;
    6.75  
    6.76 -    txt {* $b\ap \zero$ is an upperboud of $S$. *};
    6.77 +    txt {* $b\ap \zero$ is an upper bound of $S$: *};
    6.78  
    6.79      show "EX Y. isUb UNIV ?S Y"; 
    6.80      proof; 
    6.81        show "isUb UNIV ?S (b <0>)";
    6.82        proof (intro isUbI setleI ballI);
    6.83 +        show "b <0> : UNIV"; ..;
    6.84 +      next;
    6.85  
    6.86 -        txt {* Every element $y\in S$ is less than $b\ap \zero$ *};  
    6.87 +        txt {* Every element $y\in S$ is less than $b\ap \zero$: *};
    6.88  
    6.89          fix y; assume y: "y : ?S"; 
    6.90 -        from y; have "EX u:F. y = a u"; ..;
    6.91 +        from y; have "EX u:F. y = a u"; by fast;
    6.92          thus "y <= b <0>"; 
    6.93          proof;
    6.94 -          fix u; assume "u:F"; assume "y = a u";
    6.95 +          fix u; assume "u:F"; 
    6.96 +          assume "y = a u";
    6.97            also; have "a u <= b <0>"; by (rule r) (simp!)+;
    6.98            finally; show ?thesis; .;
    6.99          qed;
   6.100 -      next;
   6.101 -        show "b <0> : UNIV"; by simp;
   6.102        qed;
   6.103      qed;
   6.104    qed;
   6.105  
   6.106 -  thus "EX xi. (ALL y:F. a y <= xi) & (ALL y:F. xi <= b y)"; 
   6.107 +  thus "EX xi. ALL y:F. a y <= xi & xi <= b y"; 
   6.108    proof (elim exE);
   6.109      fix xi; assume "isLub UNIV ?S xi"; 
   6.110      show ?thesis;
   6.111      proof (intro exI conjI ballI); 
   6.112     
   6.113 -      txt {* For all $y\in F$ holds $a\ap y \leq \xi$. *};
   6.114 +      txt {* For all $y\in F$ holds $a\ap y \leq \xi$: *};
   6.115       
   6.116        fix y; assume y: "y:F";
   6.117        show "a y <= xi";    
   6.118 @@ -93,16 +94,16 @@
   6.119        qed (force!);
   6.120      next;
   6.121  
   6.122 -      txt {* For all $y\in F$ holds $\xi\leq b\ap y$. *};
   6.123 +      txt {* For all $y\in F$ holds $\xi\leq b\ap y$: *};
   6.124  
   6.125        fix y; assume "y:F";
   6.126        show "xi <= b y";  
   6.127        proof (intro isLub_le_isUb isUbI setleI);
   6.128 -        show "b y : UNIV"; by simp;
   6.129 +        show "b y : UNIV"; ..;
   6.130          show "ALL ya : ?S. ya <= b y"; 
   6.131          proof;
   6.132            fix au; assume au: "au : ?S ";
   6.133 -          hence "EX u:F. au = a u"; ..;
   6.134 +          hence "EX u:F. au = a u"; by fast;
   6.135            thus "au <= b y";
   6.136            proof;
   6.137              fix u; assume "u:F"; assume "au = a u";  
   6.138 @@ -115,25 +116,26 @@
   6.139    qed;
   6.140  qed;
   6.141  
   6.142 -text{* The function $h_0$ is defined as a canonical linear extension
   6.143 -of $h$ to $H_0$. *};
   6.144 +text{* The function $h_0$ is defined as a
   6.145 +$h_0\ap x = h\ap y + a\cdot \xi$ where $x = y + a\prod \xi$
   6.146 +is a linear extension of $h$ to $H_0$. *};
   6.147  
   6.148  lemma h0_lf: 
   6.149 -  "[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
   6.150 +  "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
   6.151                  in h y + a * xi);
   6.152 -  H0 = H + lin x0; is_subspace H E; is_linearform H h; x0 ~: H; 
   6.153 +  H0 == H + lin x0; is_subspace H E; is_linearform H h; x0 ~: H; 
   6.154    x0 : E; x0 ~= <0>; is_vectorspace E |]
   6.155    ==> is_linearform H0 h0";
   6.156  proof -;
   6.157    assume h0_def: 
   6.158 -    "h0 = (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
   6.159 +    "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
   6.160                 in h y + a * xi)"
   6.161 -      and H0_def: "H0 = H + lin x0" 
   6.162 -      and vs: "is_subspace H E" "is_linearform H h" "x0 ~: H"
   6.163 -        "x0 ~= <0>" "x0 : E" "is_vectorspace E";
   6.164 +    and H0_def: "H0 == H + lin x0" 
   6.165 +    and vs: "is_subspace H E" "is_linearform H h" "x0 ~: H"
   6.166 +      "x0 ~= <0>" "x0 : E" "is_vectorspace E";
   6.167  
   6.168    have h0: "is_vectorspace H0"; 
   6.169 -  proof (simp only: H0_def, rule vs_sum_vs);
   6.170 +  proof (unfold H0_def, rule vs_sum_vs);
   6.171      show "is_subspace (lin x0) E"; ..;
   6.172    qed; 
   6.173  
   6.174 @@ -141,8 +143,7 @@
   6.175    proof;
   6.176      fix x1 x2; assume x1: "x1 : H0" and x2: "x2 : H0"; 
   6.177  
   6.178 -    txt{* We now have to show that $h_0$ is linear 
   6.179 -    w.~r.~t.~addition, i.~e.\
   6.180 +    txt{* We now have to show that $h_0$ is additive, i.~e.\
   6.181      $h_0 \ap (x_1\plus x_2) = h_0\ap x_1 + h_0\ap x_2$
   6.182      for $x_1, x_2\in H$. *}; 
   6.183  
   6.184 @@ -150,13 +151,13 @@
   6.185        by (rule vs_add_closed, rule h0); 
   6.186      from x1; 
   6.187      have ex_x1: "EX y1 a1. x1 = y1 + a1 <*> x0  & y1 : H"; 
   6.188 -      by (simp add: H0_def vs_sum_def lin_def) blast;
   6.189 +      by (unfold H0_def vs_sum_def lin_def) fast;
   6.190      from x2; 
   6.191      have ex_x2: "EX y2 a2. x2 = y2 + a2 <*> x0 & y2 : H"; 
   6.192 -      by (simp add: H0_def vs_sum_def lin_def) blast;
   6.193 +      by (unfold H0_def vs_sum_def lin_def) fast;
   6.194      from x1x2; 
   6.195      have ex_x1x2: "EX y a. x1 + x2 = y + a <*> x0 & y : H";
   6.196 -      by (simp add: H0_def vs_sum_def lin_def) force;
   6.197 +      by (unfold H0_def vs_sum_def lin_def) fast;
   6.198  
   6.199      from ex_x1 ex_x2 ex_x1x2;
   6.200      show "h0 (x1 + x2) = h0 x1 + h0 x2";
   6.201 @@ -167,7 +168,7 @@
   6.202           and y: "x1 + x2 = y + a <*> x0"   and y':  "y  : H"; 
   6.203  
   6.204        have ya: "y1 + y2 = y & a1 + a2 = a"; 
   6.205 -      proof (rule decomp_H0); 
   6.206 +      proof (rule decomp_H0);  txt{*\label{decomp-H0-use}*}; 
   6.207          show "y1 + y2 + (a1 + a2) <*> x0 = y + a <*> x0"; 
   6.208            by (simp! add: vs_add_mult_distrib2 [of E]);
   6.209          show "y1 + y2 : H"; ..;
   6.210 @@ -179,7 +180,7 @@
   6.211          by (simp add: ya);
   6.212        also; from vs y1' y2'; 
   6.213        have "... = h y1 + h y2 + a1 * xi + a2 * xi"; 
   6.214 -	by (simp add: linearform_add_linear [of H] 
   6.215 +	by (simp add: linearform_add [of H] 
   6.216                        real_add_mult_distrib);
   6.217        also; have "... = (h y1 + a1 * xi) + (h y2 + a2 * xi)"; 
   6.218          by simp;
   6.219 @@ -190,24 +191,23 @@
   6.220        finally; show ?thesis; .;
   6.221      qed;
   6.222   
   6.223 -    txt{* We further have to show that $h_0$ is linear 
   6.224 -    w.~r.~t.~scalar multiplication, 
   6.225 +    txt{* We further have to show that $h_0$ is multiplicative, 
   6.226      i.~e.\ $h_0\ap (c \mult x_1) = c \cdot h_0\ap x_1$
   6.227 -    for $x\in H$ and any real number $c$. 
   6.228 +    for $x\in H$ and $c\in \bbbR$. 
   6.229      *}; 
   6.230  
   6.231    next;  
   6.232      fix c x1; assume x1: "x1 : H0";    
   6.233      have ax1: "c <*> x1 : H0";
   6.234        by (rule vs_mult_closed, rule h0);
   6.235 -    from x1; have ex_x1: "EX y1 a1. x1 = y1 + a1 <*> x0 & y1 : H";
   6.236 -      by (simp add: H0_def vs_sum_def lin_def) fast;
   6.237      from x1; have ex_x: "!! x. x: H0 
   6.238                          ==> EX y a. x = y + a <*> x0 & y : H";
   6.239 -      by (simp add: H0_def vs_sum_def lin_def) fast;
   6.240 -    note ex_ax1 = ex_x [of "c <*> x1", OF ax1];
   6.241 +      by (unfold H0_def vs_sum_def lin_def) fast;
   6.242  
   6.243 -    with ex_x1; show "h0 (c <*> x1) = c * (h0 x1)";  
   6.244 +    from x1; have ex_x1: "EX y1 a1. x1 = y1 + a1 <*> x0 & y1 : H";
   6.245 +      by (unfold H0_def vs_sum_def lin_def) fast;
   6.246 +    with ex_x [of "c <*> x1", OF ax1];
   6.247 +    show "h0 (c <*> x1) = c * (h0 x1)";  
   6.248      proof (elim exE conjE);
   6.249        fix y1 y a1 a; 
   6.250        assume y1: "x1 = y1 + a1 <*> x0"       and y1': "y1 : H"
   6.251 @@ -225,7 +225,7 @@
   6.252        also; have "... = h (c <*> y1) + (c * a1) * xi";
   6.253          by (simp add: ya);
   6.254        also; from vs y1'; have "... = c * h y1 + c * a1 * xi"; 
   6.255 -	by (simp add: linearform_mult_linear [of H]);
   6.256 +	by (simp add: linearform_mult [of H]);
   6.257        also; from vs y1'; have "... = c * (h y1 + a1 * xi)"; 
   6.258  	by (simp add: real_add_mult_distrib2 real_mult_assoc);
   6.259        also; have "h y1 + a1 * xi = h0 x1"; 
   6.260 @@ -235,30 +235,31 @@
   6.261    qed;
   6.262  qed;
   6.263  
   6.264 -text{* $h_0$ is bounded by the quasinorm $p$. *};
   6.265 +text{* The linear extension $h_0$ of $h$
   6.266 +is bounded by the seminorm $p$. *};
   6.267  
   6.268  lemma h0_norm_pres:
   6.269 -  "[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
   6.270 +  "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
   6.271                  in h y + a * xi);
   6.272 -  H0 = H + lin x0; x0 ~: H; x0 : E; x0 ~= <0>; is_vectorspace E; 
   6.273 -  is_subspace H E; is_quasinorm E p; is_linearform H h; 
   6.274 +  H0 == H + lin x0; x0 ~: H; x0 : E; x0 ~= <0>; is_vectorspace E; 
   6.275 +  is_subspace H E; is_seminorm E p; is_linearform H h; 
   6.276    ALL y:H. h y <= p y; (ALL y:H. - p (y + x0) - h y <= xi) 
   6.277    & (ALL y:H. xi <= p (y + x0) - h y) |]
   6.278     ==> ALL x:H0. h0 x <= p x"; 
   6.279  proof; 
   6.280    assume h0_def: 
   6.281 -    "h0 = (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
   6.282 +    "h0 == (\<lambda>x. let (y, a) = SOME (y, a). x = y + a <*> x0 & y:H 
   6.283                 in (h y) + a * xi)"
   6.284 -    and H0_def: "H0 = H + lin x0" 
   6.285 +    and H0_def: "H0 == H + lin x0" 
   6.286      and vs: "x0 ~: H" "x0 : E" "x0 ~= <0>" "is_vectorspace E" 
   6.287 -            "is_subspace H E" "is_quasinorm E p" "is_linearform H h" 
   6.288 -    and a:      " ALL y:H. h y <= p y";
   6.289 -  presume a1: "ALL y:H. - p (y + x0) - h y <= xi";
   6.290 -  presume a2: "ALL y:H. xi <= p (y + x0) - h y";
   6.291 +            "is_subspace H E" "is_seminorm E p" "is_linearform H h" 
   6.292 +    and a: "ALL y:H. h y <= p y";
   6.293 +  presume a1: "ALL ya:H. - p (ya + x0) - h ya <= xi";
   6.294 +  presume a2: "ALL ya:H. xi <= p (ya + x0) - h ya";
   6.295    fix x; assume "x : H0"; 
   6.296    have ex_x: 
   6.297      "!! x. x : H0 ==> EX y a. x = y + a <*> x0 & y : H";
   6.298 -    by (simp add: H0_def vs_sum_def lin_def) fast;
   6.299 +    by (unfold H0_def vs_sum_def lin_def) fast;
   6.300    have "EX y a. x = y + a <*> x0 & y : H";
   6.301      by (rule ex_x);
   6.302    thus "h0 x <= p x";
   6.303 @@ -268,7 +269,7 @@
   6.304        by (rule h0_definite);
   6.305  
   6.306      txt{* Now we show  
   6.307 -    $h\ap y + a \cdot xi\leq  p\ap (y\plus a \mult x_0)$ 
   6.308 +    $h\ap y + a \cdot \xi\leq  p\ap (y\plus a \mult x_0)$ 
   6.309      by case analysis on $a$. *};
   6.310  
   6.311      also; have "... <= p (y + a <*> x0)";
   6.312 @@ -277,17 +278,17 @@
   6.313        assume z: "a = 0r"; 
   6.314        with vs y a; show ?thesis; by simp;
   6.315  
   6.316 -    txt {* In the case $a < 0$ we use $a_1$ with $y$ taken as
   6.317 -    $y/a$. *};
   6.318 +    txt {* In the case $a < 0$, we use $a_1$ with $\idt{ya}$ 
   6.319 +    taken as $y/a$: *};
   6.320  
   6.321      next;
   6.322        assume lz: "a < 0r"; hence nz: "a ~= 0r"; by simp;
   6.323        from a1; 
   6.324        have "- p (rinv a <*> y + x0) - h (rinv a <*> y) <= xi";
   6.325 -        by (rule bspec)(simp!);
   6.326 - 
   6.327 -      txt {* The thesis now follows by a short calculation. *};      
   6.328 +        by (rule bspec) (simp!);
   6.329  
   6.330 +      txt {* The thesis for this case now follows by a short  
   6.331 +      calculation. *};      
   6.332        hence "a * xi 
   6.333              <= a * (- p (rinv a <*> y + x0) - h (rinv a <*> y))";
   6.334          by (rule real_mult_less_le_anti [OF lz]);
   6.335 @@ -296,25 +297,28 @@
   6.336          by (rule real_mult_diff_distrib);
   6.337        also; from lz vs y; have "- a * (p (rinv a <*> y + x0)) 
   6.338                                 = p (a <*> (rinv a <*> y + x0))";
   6.339 -        by (simp add: quasinorm_mult_distrib rabs_minus_eqI2);
   6.340 +        by (simp add: seminorm_rabs_homogenous rabs_minus_eqI2);
   6.341        also; from nz vs y; have "... = p (y + a <*> x0)";
   6.342          by (simp add: vs_add_mult_distrib1);
   6.343        also; from nz vs y; have "a * (h (rinv a <*> y)) =  h y";
   6.344 -        by (simp add: linearform_mult_linear [RS sym]);
   6.345 +        by (simp add: linearform_mult [RS sym]);
   6.346        finally; have "a * xi <= p (y + a <*> x0) - h y"; .;
   6.347  
   6.348        hence "h y + a * xi <= h y + p (y + a <*> x0) - h y";
   6.349          by (simp add: real_add_left_cancel_le);
   6.350        thus ?thesis; by simp;
   6.351  
   6.352 -      txt {* In the case $a > 0$ we use $a_2$ with $y$ taken
   6.353 -      as $y/a$. *};
   6.354 +      txt {* In the case $a > 0$, we use $a_2$ with $\idt{ya}$ 
   6.355 +      taken as $y/a$: *};
   6.356 +
   6.357      next; 
   6.358        assume gz: "0r < a"; hence nz: "a ~= 0r"; by simp;
   6.359 +      from a2;
   6.360        have "xi <= p (rinv a <*> y + x0) - h (rinv a <*> y)";
   6.361 -        by (rule bspec [OF a2]) (simp!);
   6.362 +        by (rule bspec) (simp!);
   6.363  
   6.364 -      txt {* The thesis follows by a short calculation. *};
   6.365 +      txt {* The thesis for this case follows by a short
   6.366 +      calculation: *};
   6.367  
   6.368        with gz; have "a * xi 
   6.369              <= a * (p (rinv a <*> y + x0) - h (rinv a <*> y))";
   6.370 @@ -325,12 +329,12 @@
   6.371        also; from gz vs y; 
   6.372        have "a * p (rinv a <*> y + x0) 
   6.373             = p (a <*> (rinv a <*> y + x0))";
   6.374 -        by (simp add: quasinorm_mult_distrib rabs_eqI2);
   6.375 +        by (simp add: seminorm_rabs_homogenous rabs_eqI2);
   6.376        also; from nz vs y; 
   6.377        have "... = p (y + a <*> x0)";
   6.378          by (simp add: vs_add_mult_distrib1);
   6.379        also; from nz vs y; have "a * h (rinv a <*> y) = h y";
   6.380 -        by (simp add: linearform_mult_linear [RS sym]); 
   6.381 +        by (simp add: linearform_mult [RS sym]); 
   6.382        finally; have "a * xi <= p (y + a <*> x0) - h y"; .;
   6.383   
   6.384        hence "h y + a * xi <= h y + (p (y + a <*> x0) - h y)";
   6.385 @@ -342,5 +346,4 @@
   6.386    qed;
   6.387  qed blast+; 
   6.388  
   6.389 -
   6.390  end;
   6.391 \ No newline at end of file
     7.1 --- a/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Fri Oct 29 19:24:20 1999 +0200
     7.2 +++ b/src/HOL/Real/HahnBanach/HahnBanachSupLemmas.thy	Fri Oct 29 20:18:34 1999 +0200
     7.3 @@ -10,20 +10,20 @@
     7.4  
     7.5  
     7.6  text{* This section contains some lemmas that will be used in the
     7.7 -proof of the Hahn-Banach theorem.
     7.8 +proof of the Hahn-Banach Theorem.
     7.9  In this section the following context is presumed. 
    7.10 -Let $E$ be a real vector space with a quasinorm $q$ on $E$. 
    7.11 -$F$ is a subspace of $E$ and $f$ a linearform on $F$. We 
    7.12 -consider a chain $c$ of norm preserving extensions of $f$, such that
    7.13 +Let $E$ be a real vector space with a seminorm $q$ on $E$. 
    7.14 +$F$ is a subspace of $E$ and $f$ a linear form on $F$. We 
    7.15 +consider a chain $c$ of norm-preserving extensions of $f$, such that
    7.16  $\Union c = \idt{graph}\ap H\ap h$. 
    7.17  We will show some properties about the limit function $h$, 
    7.18 -i.~e.~the supremum of the chain $c$.
    7.19 +i.e.\ the supremum of the chain $c$.
    7.20  *}; 
    7.21  
    7.22  (***
    7.23  lemma some_H'h't:
    7.24    "[| M = norm_pres_extensions E p F f; c: chain M; 
    7.25 -  graph H h = Union c; x:H|]
    7.26 +  graph H h = Union c; x:H |]
    7.27     ==> EX H' h' t. t : graph H h & t = (x, h x) & graph H' h':c 
    7.28         & t:graph H' h' & is_linearform H' h' & is_subspace H' E 
    7.29         & is_subspace F H' & graph F f <= graph H' h' 
    7.30 @@ -60,14 +60,14 @@
    7.31  qed;
    7.32  ***)
    7.33  
    7.34 -text{* Let $c$ be a chain of norm preserving extensions of the 
    7.35 +text{* Let $c$ be a chain of norm-preserving extensions of the 
    7.36  function $f$ and let $\idt{graph}\ap H\ap h$ be the supremum of $c$. 
    7.37  Every element in $H$ is member of
    7.38  one of the elements of the chain. *};
    7.39  
    7.40  lemma some_H'h't:
    7.41    "[| M = norm_pres_extensions E p F f; c: chain M; 
    7.42 -  graph H h = Union c; x:H|]
    7.43 +  graph H h = Union c; x:H |]
    7.44     ==> EX H' h'. graph H' h' : c & (x, h x) : graph H' h' 
    7.45         & is_linearform H' h' & is_subspace H' E 
    7.46         & is_subspace F H' & graph F f <= graph H' h' 
    7.47 @@ -109,7 +109,7 @@
    7.48  qed;
    7.49  
    7.50  
    7.51 -text{*  Let $c$ be a chain of norm preserving extensions of the
    7.52 +text{*  Let $c$ be a chain of norm-preserving extensions of the
    7.53  function $f$ and let $\idt{graph}\ap H\ap h$ be the supremum of $c$. 
    7.54  Every element in the domain $H$ of the supremum function is member of
    7.55  the domain $H'$ of some function $h'$, such that $h$ extends $h'$.
    7.56 @@ -117,7 +117,7 @@
    7.57  
    7.58  lemma some_H'h': 
    7.59    "[| M = norm_pres_extensions E p F f; c: chain M; 
    7.60 -  graph H h = Union c; x:H|] 
    7.61 +  graph H h = Union c; x:H |] 
    7.62    ==> EX H' h'. x:H' & graph H' h' <= graph H h 
    7.63        & is_linearform H' h' & is_subspace H' E & is_subspace F H'
    7.64        & graph F f <= graph H' h' & (ALL x:H'. h' x <= p x)"; 
    7.65 @@ -147,7 +147,7 @@
    7.66  (***
    7.67  lemma some_H'h': 
    7.68    "[| M = norm_pres_extensions E p F f; c: chain M; 
    7.69 -  graph H h = Union c; x:H|] 
    7.70 +  graph H h = Union c; x:H |] 
    7.71    ==> EX H' h'. x:H' & graph H' h' <= graph H h 
    7.72        & is_linearform H' h' & is_subspace H' E & is_subspace F H'
    7.73        & graph F f <= graph H' h' & (ALL x:H'. h' x <= p x)"; 
    7.74 @@ -185,7 +185,7 @@
    7.75  
    7.76  
    7.77  text{* Any two elements $x$ and $y$ in the domain $H$ of the 
    7.78 -supremum function $h$ lie both in the domain $H'$ of some function 
    7.79 +supremum function $h$ are both in the domain $H'$ of some function 
    7.80  $h'$, such that $h$ extends $h'$. *};
    7.81  
    7.82  lemma some_H'h'2: 
    7.83 @@ -265,7 +265,7 @@
    7.84  (***
    7.85  lemma some_H'h'2: 
    7.86    "[| M = norm_pres_extensions E p F f; c: chain M; 
    7.87 -  graph H h = Union c;  x:H; y:H|] 
    7.88 +  graph H h = Union c;  x:H; y:H |] 
    7.89    ==> EX H' h'. x:H' & y:H' & graph H' h' <= graph H h 
    7.90        & is_linearform H' h' & is_subspace H' E & is_subspace F H' 
    7.91        & graph F f <= graph H' h' & (ALL x:H'. h' x <= p x)"; 
    7.92 @@ -350,7 +350,7 @@
    7.93  
    7.94      txt{* Since both $(x, y) \in \Union c$ and $(x, z) \in \Union c$
    7.95      they are members of some graphs $G_1$ and $G_2$, resp., such that
    7.96 -    both $G_1$ and $G_2$ are members of $c$*};
    7.97 +    both $G_1$ and $G_2$ are members of $c$.*};
    7.98  
    7.99      fix G1 G2; assume
   7.100        "(x, y) : G1" "G1 : c" "(x, z) : G2" "G2 : c" "c <= M";
   7.101 @@ -366,8 +366,8 @@
   7.102        fix H1 h1 H2 h2; 
   7.103        assume "graph H1 h1 = G1" "graph H2 h2 = G2";
   7.104  
   7.105 -      txt{* Since both h $G_1$ and $G_2$ are members of $c$, 
   7.106 -      $G_1$ is contained in $G_2$ or vice versa. *};
   7.107 +      txt{* $G_1$ is contained in $G_2$ or vice versa, 
   7.108 +      since both $G_1$ and $G_2$ are members of $c$. *};
   7.109  
   7.110        have "G1 <= G2 | G2 <= G1" (is "?case1 | ?case2"); ..;
   7.111        thus ?thesis;
   7.112 @@ -390,10 +390,10 @@
   7.113    qed;
   7.114  qed;
   7.115  
   7.116 -text{* The limit function $h$ is linear: every element $x$ in the
   7.117 +text{* The limit function $h$ is linear. Every element $x$ in the
   7.118  domain of $h$ is in the domain of a function $h'$ in the chain of norm
   7.119  preserving extensions.  Furthermore, $h$ is an extension of $h'$ so
   7.120 -the value of $x$ are identical for $h'$ and $h$.  Finally, the
   7.121 +the function values of $x$ are identical for $h'$ and $h$.  Finally, the
   7.122  function $h'$ is linear by construction of $M$.  *};
   7.123  
   7.124  lemma sup_lf: 
   7.125 @@ -412,8 +412,7 @@
   7.126              & (ALL x:H'. h' x <= p x)";
   7.127        by (rule some_H'h'2);
   7.128  
   7.129 -    txt {* We have to show that h is linear w.~r.~t. 
   7.130 -    addition. *};
   7.131 +    txt {* We have to show that $h$ is additive. *};
   7.132  
   7.133      thus "h (x + y) = h x + h y"; 
   7.134      proof (elim exE conjE);
   7.135 @@ -421,7 +420,7 @@
   7.136          and b: "graph H' h' <= graph H h" 
   7.137          and "is_linearform H' h'" "is_subspace H' E";
   7.138        have "h' (x + y) = h' x + h' y"; 
   7.139 -        by (rule linearform_add_linear);
   7.140 +        by (rule linearform_add);
   7.141        also; have "h' x = h x"; ..;
   7.142        also; have "h' y = h y"; ..;
   7.143        also; have "x + y : H'"; ..;
   7.144 @@ -436,8 +435,7 @@
   7.145              & (ALL x:H'. h' x <= p x)";
   7.146        by (rule some_H'h');
   7.147  
   7.148 -    txt{* We have to show that h is linear w.~r.~t. 
   7.149 -    scalar multiplication. *};
   7.150 +    txt{* We have to show that $h$ is multiplicative. *};
   7.151  
   7.152      thus "h (a <*> x) = a * h x";
   7.153      proof (elim exE conjE);
   7.154 @@ -445,7 +443,7 @@
   7.155          and b: "graph H' h' <= graph H h" 
   7.156          and "is_linearform H' h'" "is_subspace H' E";
   7.157        have "h' (a <*> x) = a * h' x"; 
   7.158 -        by (rule linearform_mult_linear);
   7.159 +        by (rule linearform_mult);
   7.160        also; have "h' x = h x"; ..;
   7.161        also; have "a <*> x : H'"; ..;
   7.162        with b; have "h' (a <*> x) = h (a <*> x)"; ..;
   7.163 @@ -462,7 +460,7 @@
   7.164  
   7.165  lemma sup_ext:
   7.166    "[| M = norm_pres_extensions E p F f; c: chain M; EX x. x:c; 
   7.167 -  graph H h = Union c|] ==> graph F f <= graph H h";
   7.168 +  graph H h = Union c |] ==> graph F f <= graph H h";
   7.169  proof -;
   7.170    assume "M = norm_pres_extensions E p F f" "c: chain M" 
   7.171           "graph H h = Union c";
   7.172 @@ -484,9 +482,11 @@
   7.173  
   7.174      thus ?thesis; 
   7.175      proof (elim exE conjE); 
   7.176 -      fix G g; assume "graph G g = x" "graph F f <= graph G g";
   7.177 -      have "graph F f <= graph G g"; .;
   7.178 -      also; have "graph G g <= graph H h"; by (simp!, fast);
   7.179 +      fix G g; assume "graph F f <= graph G g";
   7.180 +      also; assume "graph G g = x";
   7.181 +      also; have "... : c"; .;
   7.182 +      hence "x <= Union c"; by fast;
   7.183 +      also; have [RS sym]: "graph H h = Union c"; .;
   7.184        finally; show ?thesis; .;
   7.185      qed;
   7.186    qed;
   7.187 @@ -539,15 +539,15 @@
   7.188    show ?thesis; 
   7.189    proof;
   7.190   
   7.191 -    txt {* The $\zero$ element lies in $H$, as $F$ is a subset 
   7.192 -    of $H$. *};
   7.193 +    txt {* The $\zero$ element is in $H$, as $F$ is a subset 
   7.194 +    of $H$: *};
   7.195  
   7.196      have "<0> : F"; ..;
   7.197      also; have "is_subspace F H"; by (rule sup_supF); 
   7.198      hence "F <= H"; ..;
   7.199      finally; show "<0> : H"; .;
   7.200  
   7.201 -    txt{* $H$ is a subset of $E$. *};
   7.202 +    txt{* $H$ is a subset of $E$: *};
   7.203  
   7.204      show "H <= E"; 
   7.205      proof;
   7.206 @@ -565,7 +565,7 @@
   7.207        qed;
   7.208      qed;
   7.209  
   7.210 -    txt{* $H$ is closed under addition. *};
   7.211 +    txt{* $H$ is closed under addition: *};
   7.212  
   7.213      show "ALL x:H. ALL y:H. x + y : H"; 
   7.214      proof (intro ballI); 
   7.215 @@ -586,7 +586,7 @@
   7.216        qed;
   7.217      qed;      
   7.218  
   7.219 -    txt{* $H$ is closed under scalar multiplication. *};
   7.220 +    txt{* $H$ is closed under scalar multiplication: *};
   7.221  
   7.222      show "ALL x:H. ALL a. a <*> x : H"; 
   7.223      proof (intro ballI allI); 
   7.224 @@ -609,7 +609,8 @@
   7.225  qed;
   7.226  
   7.227  text {* The limit function is bounded by 
   7.228 -the norm $p$ as well, since all elements in the chain are norm preserving.
   7.229 +the norm $p$ as well, since all elements in the chain are
   7.230 +bounded by $p$.
   7.231  *};
   7.232  
   7.233  lemma sup_norm_pres: 
   7.234 @@ -635,10 +636,10 @@
   7.235  qed;
   7.236  
   7.237  
   7.238 -text_raw{* \medskip *}
   7.239 -text{* The following lemma is a property of real linearforms on 
   7.240 +text{* \medskip The following lemma is a property of linearforms on 
   7.241  real vector spaces. It will be used for the lemma 
   7.242 -$\idt{rabs{\dsh}HahnBanach}$.
   7.243 +$\idt{rabs{\dsh}HahnBanach}$ (see page \pageref{rabs-HahnBanach}).
   7.244 +\label{rabs-ineq-iff}
   7.245  For real vector spaces the following inequations are equivalent:
   7.246  \begin{matharray}{ll} 
   7.247  \forall x\in H.\ap |h\ap x|\leq p\ap x& {\rm and}\\ 
   7.248 @@ -647,12 +648,12 @@
   7.249  *};
   7.250  
   7.251  lemma rabs_ineq_iff: 
   7.252 -  "[| is_subspace H E; is_vectorspace E; is_quasinorm E p; 
   7.253 +  "[| is_subspace H E; is_vectorspace E; is_seminorm E p; 
   7.254    is_linearform H h |] 
   7.255    ==> (ALL x:H. rabs (h x) <= p x) = (ALL x:H. h x <= p x)" 
   7.256    (concl is "?L = ?R");
   7.257  proof -;
   7.258 -  assume "is_subspace H E" "is_vectorspace E" "is_quasinorm E p" 
   7.259 +  assume "is_subspace H E" "is_vectorspace E" "is_seminorm E p" 
   7.260           "is_linearform H h";
   7.261    have h: "is_vectorspace H"; ..;
   7.262    show ?thesis;
   7.263 @@ -675,10 +676,10 @@
   7.264        show "- p x <= h x";
   7.265        proof (rule real_minus_le);
   7.266  	from h; have "- h x = h (- x)"; 
   7.267 -          by (rule linearform_neg_linear [RS sym]);
   7.268 +          by (rule linearform_neg [RS sym]);
   7.269  	also; from r; have "... <= p (- x)"; by (simp!);
   7.270  	also; have "... = p x"; 
   7.271 -          by (rule quasinorm_minus, rule subspace_subsetD);
   7.272 +          by (rule seminorm_minus, rule subspace_subsetD);
   7.273  	finally; show "- h x <= p x"; .; 
   7.274        qed;
   7.275        from r; show "h x <= p x"; ..; 
     8.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy	Fri Oct 29 19:24:20 1999 +0200
     8.2 +++ b/src/HOL/Real/HahnBanach/Linearform.thy	Fri Oct 29 20:18:34 1999 +0200
     8.3 @@ -7,9 +7,8 @@
     8.4  
     8.5  theory Linearform = VectorSpace:;
     8.6  
     8.7 -text{* A \emph{linearform} is a function on a vector
     8.8 -space into the reals that is linear w.~r.~t.~addition and skalar
     8.9 -multiplikation. *};
    8.10 +text{* A \emph{linear form} is a function on a vector
    8.11 +space into the reals that is additive and multiplicative. *};
    8.12  
    8.13  constdefs
    8.14    is_linearform :: "['a::{minus, plus} set, 'a => real] => bool" 
    8.15 @@ -23,38 +22,38 @@
    8.16   ==> is_linearform V f";
    8.17   by (unfold is_linearform_def) force;
    8.18  
    8.19 -lemma linearform_add_linear [intro!!]: 
    8.20 +lemma linearform_add [intro!!]: 
    8.21    "[| is_linearform V f; x:V; y:V |] ==> f (x + y) = f x + f y";
    8.22    by (unfold is_linearform_def) fast;
    8.23  
    8.24 -lemma linearform_mult_linear [intro!!]: 
    8.25 +lemma linearform_mult [intro!!]: 
    8.26    "[| is_linearform V f; x:V |] ==>  f (a <*> x) = a * (f x)"; 
    8.27    by (unfold is_linearform_def) fast;
    8.28  
    8.29 -lemma linearform_neg_linear [intro!!]:
    8.30 +lemma linearform_neg [intro!!]:
    8.31    "[|  is_vectorspace V; is_linearform V f; x:V|] 
    8.32    ==> f (- x) = - f x";
    8.33  proof -; 
    8.34    assume "is_linearform V f" "is_vectorspace V" "x:V"; 
    8.35    have "f (- x) = f ((- 1r) <*> x)"; by (simp! add: negate_eq1);
    8.36 -  also; have "... = (- 1r) * (f x)"; by (rule linearform_mult_linear);
    8.37 +  also; have "... = (- 1r) * (f x)"; by (rule linearform_mult);
    8.38    also; have "... = - (f x)"; by (simp!);
    8.39    finally; show ?thesis; .;
    8.40  qed;
    8.41  
    8.42 -lemma linearform_diff_linear [intro!!]: 
    8.43 +lemma linearform_diff [intro!!]: 
    8.44    "[| is_vectorspace V; is_linearform V f; x:V; y:V |] 
    8.45    ==> f (x - y) = f x - f y";  
    8.46  proof -;
    8.47    assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V";
    8.48    have "f (x - y) = f (x + - y)"; by (simp! only: diff_eq1);
    8.49    also; have "... = f x + f (- y)"; 
    8.50 -    by (rule linearform_add_linear) (simp!)+;
    8.51 -  also; have "f (- y) = - f y"; by (rule linearform_neg_linear);
    8.52 +    by (rule linearform_add) (simp!)+;
    8.53 +  also; have "f (- y) = - f y"; by (rule linearform_neg);
    8.54    finally; show "f (x - y) = f x - f y"; by (simp!);
    8.55  qed;
    8.56  
    8.57 -text{* Every linearform yields $0$ for the $\zero$ vector.*};
    8.58 +text{* Every linear form yields $0$ for the $\zero$ vector.*};
    8.59  
    8.60  lemma linearform_zero [intro!!, simp]: 
    8.61    "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; 
    8.62 @@ -62,7 +61,7 @@
    8.63    assume "is_vectorspace V" "is_linearform V f";
    8.64    have "f <0> = f (<0> - <0>)"; by (simp!);
    8.65    also; have "... = f <0> - f <0>"; 
    8.66 -    by (rule linearform_diff_linear) (simp!)+;
    8.67 +    by (rule linearform_diff) (simp!)+;
    8.68    also; have "... = 0r"; by simp;
    8.69    finally; show "f <0> = 0r"; .;
    8.70  qed; 
     9.1 --- a/src/HOL/Real/HahnBanach/NormedSpace.thy	Fri Oct 29 19:24:20 1999 +0200
     9.2 +++ b/src/HOL/Real/HahnBanach/NormedSpace.thy	Fri Oct 29 20:18:34 1999 +0200
     9.3 @@ -11,60 +11,61 @@
     9.4  
     9.5  subsection {* Quasinorms *};
     9.6  
     9.7 -text{* A \emph{quasinorm} $\norm{\cdot}$ is a  function on a real vector space into the reals 
     9.8 -that has the following properties: *};
     9.9 +text{* A \emph{seminorm} $\norm{\cdot}$ is a function on a real vector
    9.10 +space into the reals that has the following properties: It is positive
    9.11 +definite, absolute homogenous and subadditive.  *};
    9.12  
    9.13  constdefs
    9.14 -  is_quasinorm :: "['a::{plus, minus} set, 'a => real] => bool"
    9.15 -  "is_quasinorm V norm == ALL x: V. ALL y:V. ALL a. 
    9.16 +  is_seminorm :: "['a::{plus, minus} set, 'a => real] => bool"
    9.17 +  "is_seminorm V norm == ALL x: V. ALL y:V. ALL a. 
    9.18          0r <= norm x 
    9.19        & norm (a <*> x) = (rabs a) * (norm x)
    9.20        & norm (x + y) <= norm x + norm y";
    9.21  
    9.22 -lemma is_quasinormI [intro]: 
    9.23 -  "[| !! x y a. [| x:V; y:V|] ==>  0r <= norm x;
    9.24 +lemma is_seminormI [intro]: 
    9.25 +  "[| !! x y a. [| x:V; y:V|] ==> 0r <= norm x;
    9.26    !! x a. x:V ==> norm (a <*> x) = (rabs a) * (norm x);
    9.27    !! x y. [|x:V; y:V |] ==> norm (x + y) <= norm x + norm y |] 
    9.28 -  ==> is_quasinorm V norm";
    9.29 -  by (unfold is_quasinorm_def, force);
    9.30 +  ==> is_seminorm V norm";
    9.31 +  by (unfold is_seminorm_def, force);
    9.32  
    9.33 -lemma quasinorm_ge_zero [intro!!]:
    9.34 -  "[| is_quasinorm V norm; x:V |] ==> 0r <= norm x";
    9.35 -  by (unfold is_quasinorm_def, force);
    9.36 +lemma seminorm_ge_zero [intro!!]:
    9.37 +  "[| is_seminorm V norm; x:V |] ==> 0r <= norm x";
    9.38 +  by (unfold is_seminorm_def, force);
    9.39  
    9.40 -lemma quasinorm_mult_distrib: 
    9.41 -  "[| is_quasinorm V norm; x:V |] 
    9.42 +lemma seminorm_rabs_homogenous: 
    9.43 +  "[| is_seminorm V norm; x:V |] 
    9.44    ==> norm (a <*> x) = (rabs a) * (norm x)";
    9.45 -  by (unfold is_quasinorm_def, force);
    9.46 +  by (unfold is_seminorm_def, force);
    9.47  
    9.48 -lemma quasinorm_triangle_ineq: 
    9.49 -  "[| is_quasinorm V norm; x:V; y:V |] 
    9.50 +lemma seminorm_subadditive: 
    9.51 +  "[| is_seminorm V norm; x:V; y:V |] 
    9.52    ==> norm (x + y) <= norm x + norm y";
    9.53 -  by (unfold is_quasinorm_def, force);
    9.54 +  by (unfold is_seminorm_def, force);
    9.55  
    9.56 -lemma quasinorm_diff_triangle_ineq: 
    9.57 -  "[| is_quasinorm V norm; x:V; y:V; is_vectorspace V |] 
    9.58 +lemma seminorm_diff_subadditive: 
    9.59 +  "[| is_seminorm V norm; x:V; y:V; is_vectorspace V |] 
    9.60    ==> norm (x - y) <= norm x + norm y";
    9.61  proof -;
    9.62 -  assume "is_quasinorm V norm" "x:V" "y:V" "is_vectorspace V";
    9.63 +  assume "is_seminorm V norm" "x:V" "y:V" "is_vectorspace V";
    9.64    have "norm (x - y) = norm (x + - 1r <*> y)";  
    9.65      by (simp! add: diff_eq2 negate_eq2);
    9.66    also; have "... <= norm x + norm  (- 1r <*> y)"; 
    9.67 -    by (simp! add: quasinorm_triangle_ineq);
    9.68 +    by (simp! add: seminorm_subadditive);
    9.69    also; have "norm (- 1r <*> y) = rabs (- 1r) * norm y"; 
    9.70 -    by (rule quasinorm_mult_distrib);
    9.71 +    by (rule seminorm_rabs_homogenous);
    9.72    also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one);
    9.73    finally; show "norm (x - y) <= norm x + norm y"; by simp;
    9.74  qed;
    9.75  
    9.76 -lemma quasinorm_minus: 
    9.77 -  "[| is_quasinorm V norm; x:V; is_vectorspace V |] 
    9.78 +lemma seminorm_minus: 
    9.79 +  "[| is_seminorm V norm; x:V; is_vectorspace V |] 
    9.80    ==> norm (- x) = norm x";
    9.81  proof -;
    9.82 -  assume "is_quasinorm V norm" "x:V" "is_vectorspace V";
    9.83 -  have "norm (- x) = norm (-1r <*> x)"; by (simp! only: negate_eq1);
    9.84 -  also; have "... = rabs (-1r) * norm x"; 
    9.85 -    by (rule quasinorm_mult_distrib);
    9.86 +  assume "is_seminorm V norm" "x:V" "is_vectorspace V";
    9.87 +  have "norm (- x) = norm (- 1r <*> x)"; by (simp! only: negate_eq1);
    9.88 +  also; have "... = rabs (- 1r) * norm x"; 
    9.89 +    by (rule seminorm_rabs_homogenous);
    9.90    also; have "rabs (- 1r) = 1r"; by (rule rabs_minus_one);
    9.91    finally; show "norm (- x) = norm x"; by simp;
    9.92  qed;
    9.93 @@ -72,20 +73,20 @@
    9.94  
    9.95  subsection {* Norms *};
    9.96  
    9.97 -text{* A \emph{norm} $\norm{\cdot}$ is a quasinorm that maps only the
    9.98 +text{* A \emph{norm} $\norm{\cdot}$ is a seminorm that maps only the
    9.99  $\zero$ vector to $0$. *};
   9.100  
   9.101  constdefs
   9.102    is_norm :: "['a::{minus, plus} set, 'a => real] => bool"
   9.103 -  "is_norm V norm == ALL x: V.  is_quasinorm V norm 
   9.104 +  "is_norm V norm == ALL x: V.  is_seminorm V norm 
   9.105        & (norm x = 0r) = (x = <0>)";
   9.106  
   9.107  lemma is_normI [intro]: 
   9.108 -  "ALL x: V.  is_quasinorm V norm  & (norm x = 0r) = (x = <0>) 
   9.109 +  "ALL x: V.  is_seminorm V norm  & (norm x = 0r) = (x = <0>) 
   9.110    ==> is_norm V norm"; by (simp only: is_norm_def);
   9.111  
   9.112 -lemma norm_is_quasinorm [intro!!]: 
   9.113 -  "[| is_norm V norm; x:V |] ==> is_quasinorm V norm";
   9.114 +lemma norm_is_seminorm [intro!!]: 
   9.115 +  "[| is_norm V norm; x:V |] ==> is_seminorm V norm";
   9.116    by (unfold is_norm_def, force);
   9.117  
   9.118  lemma norm_zero_iff: 
   9.119 @@ -94,7 +95,7 @@
   9.120  
   9.121  lemma norm_ge_zero [intro!!]:
   9.122    "[|is_norm V norm; x:V |] ==> 0r <= norm x";
   9.123 -  by (unfold is_norm_def is_quasinorm_def, force);
   9.124 +  by (unfold is_norm_def is_seminorm_def, force);
   9.125  
   9.126  
   9.127  subsection {* Normed vector spaces *};
   9.128 @@ -141,16 +142,16 @@
   9.129    finally; show "0r < norm x"; .;
   9.130  qed;
   9.131  
   9.132 -lemma normed_vs_norm_mult_distrib [intro!!]: 
   9.133 +lemma normed_vs_norm_rabs_homogenous [intro!!]: 
   9.134    "[| is_normed_vectorspace V norm; x:V |] 
   9.135    ==> norm (a <*> x) = (rabs a) * (norm x)";
   9.136 -  by (rule quasinorm_mult_distrib, rule norm_is_quasinorm, 
   9.137 +  by (rule seminorm_rabs_homogenous, rule norm_is_seminorm, 
   9.138        rule normed_vs_norm);
   9.139  
   9.140 -lemma normed_vs_norm_triangle_ineq [intro!!]: 
   9.141 +lemma normed_vs_norm_subadditive [intro!!]: 
   9.142    "[| is_normed_vectorspace V norm; x:V; y:V |] 
   9.143    ==> norm (x + y) <= norm x + norm y";
   9.144 -  by (rule quasinorm_triangle_ineq, rule norm_is_quasinorm, 
   9.145 +  by (rule seminorm_subadditive, rule norm_is_seminorm, 
   9.146       rule normed_vs_norm);
   9.147  
   9.148  text{* Any subspace of a normed vector space is again a 
   9.149 @@ -165,7 +166,7 @@
   9.150    show "is_vectorspace F"; ..;
   9.151    show "is_norm F norm"; 
   9.152    proof (intro is_normI ballI conjI);
   9.153 -    show "is_quasinorm F norm"; 
   9.154 +    show "is_seminorm F norm"; 
   9.155      proof;
   9.156        fix x y a; presume "x : E";
   9.157        show "0r <= norm x"; ..;
    10.1 --- a/src/HOL/Real/HahnBanach/ROOT.ML	Fri Oct 29 19:24:20 1999 +0200
    10.2 +++ b/src/HOL/Real/HahnBanach/ROOT.ML	Fri Oct 29 20:18:34 1999 +0200
    10.3 @@ -5,5 +5,4 @@
    10.4  The Hahn-Banach theorem for real vector spaces (Isabelle/Isar).
    10.5  *)
    10.6  
    10.7 -time_use_thy "Bounds";
    10.8  time_use_thy "HahnBanach";
    11.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Fri Oct 29 19:24:20 1999 +0200
    11.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Fri Oct 29 20:18:34 1999 +0200
    11.3 @@ -17,15 +17,15 @@
    11.4  
    11.5  constdefs 
    11.6    is_subspace ::  "['a::{minus, plus} set, 'a set] => bool"
    11.7 -  "is_subspace U V ==  U ~= {}  & U <= V 
    11.8 -     &  (ALL x:U. ALL y:U. ALL a. x + y : U & a <*> x : U)";
    11.9 +  "is_subspace U V == U ~= {} & U <= V 
   11.10 +     & (ALL x:U. ALL y:U. ALL a. x + y : U & a <*> x : U)";
   11.11  
   11.12  lemma subspaceI [intro]: 
   11.13 -  "[| <0>:U; U <= V; ALL x:U. ALL y:U. (x + y : U); 
   11.14 +  "[| <0> : U; U <= V; ALL x:U. ALL y:U. (x + y : U); 
   11.15    ALL x:U. ALL a. a <*> x : U |]
   11.16    ==> is_subspace U V";
   11.17  proof (unfold is_subspace_def, intro conjI); 
   11.18 -  assume "<0>:U"; thus "U ~= {}"; by fast;
   11.19 +  assume "<0> : U"; thus "U ~= {}"; by fast;
   11.20  qed (simp+);
   11.21  
   11.22  lemma subspace_not_empty [intro!!]: "is_subspace U V ==> U ~= {}";
   11.23 @@ -35,28 +35,28 @@
   11.24    by (unfold is_subspace_def) simp;
   11.25  
   11.26  lemma subspace_subsetD [simp, intro!!]: 
   11.27 -  "[| is_subspace U V; x:U |]==> x:V";
   11.28 +  "[| is_subspace U V; x:U |] ==> x:V";
   11.29    by (unfold is_subspace_def) force;
   11.30  
   11.31  lemma subspace_add_closed [simp, intro!!]: 
   11.32 -  "[| is_subspace U V; x: U; y: U |] ==> x + y : U";
   11.33 +  "[| is_subspace U V; x:U; y:U |] ==> x + y : U";
   11.34    by (unfold is_subspace_def) simp;
   11.35  
   11.36  lemma subspace_mult_closed [simp, intro!!]: 
   11.37 -  "[| is_subspace U V; x: U |] ==> a <*> x: U";
   11.38 +  "[| is_subspace U V; x:U |] ==> a <*> x : U";
   11.39    by (unfold is_subspace_def) simp;
   11.40  
   11.41  lemma subspace_diff_closed [simp, intro!!]: 
   11.42 -  "[| is_subspace U V; is_vectorspace V; x: U; y: U |] 
   11.43 -  ==> x - y: U";
   11.44 +  "[| is_subspace U V; is_vectorspace V; x:U; y:U |] 
   11.45 +  ==> x - y : U";
   11.46    by (simp! add: diff_eq1 negate_eq1);
   11.47  
   11.48  text {* Similar as for linear spaces, the existence of the 
   11.49 -zero element in every subspace follws from the non-emptyness 
   11.50 -of the subspace and vector space laws.*};
   11.51 +zero element in every subspace follows from the non-emptiness 
   11.52 +of the carrier set and by vector space laws.*};
   11.53  
   11.54  lemma zero_in_subspace [intro !!]:
   11.55 -  "[| is_subspace U V; is_vectorspace V |] ==> <0>:U";
   11.56 +  "[| is_subspace U V; is_vectorspace V |] ==> <0> : U";
   11.57  proof -; 
   11.58    assume "is_subspace U V" and v: "is_vectorspace V";
   11.59    have "U ~= {}"; ..;
   11.60 @@ -72,11 +72,11 @@
   11.61  qed;
   11.62  
   11.63  lemma subspace_neg_closed [simp, intro!!]: 
   11.64 -  "[| is_subspace U V; is_vectorspace V; x: U |] ==> - x: U";
   11.65 +  "[| is_subspace U V; is_vectorspace V; x:U |] ==> - x : U";
   11.66    by (simp add: negate_eq1);
   11.67  
   11.68  text_raw {* \medskip *};
   11.69 -text {* Further derived laws: Every subspace is a vector space. *};
   11.70 +text {* Further derived laws: every subspace is a vector space. *};
   11.71  
   11.72  lemma subspace_vs [intro!!]:
   11.73    "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U";
   11.74 @@ -84,7 +84,7 @@
   11.75    assume "is_subspace U V" "is_vectorspace V";
   11.76    show ?thesis;
   11.77    proof; 
   11.78 -    show "<0>:U"; ..;
   11.79 +    show "<0> : U"; ..;
   11.80      show "ALL x:U. ALL a. a <*> x : U"; by (simp!);
   11.81      show "ALL x:U. ALL y:U. x + y : U"; by (simp!);
   11.82      show "ALL x:U. - x = -1r <*> x"; by (simp! add: negate_eq1);
   11.83 @@ -134,26 +134,26 @@
   11.84  
   11.85  subsection {* Linear closure *};
   11.86  
   11.87 -text {* The \emph{linear closure} of a vector $x$ is the set of all 
   11.88 -multiples of $x$. *};
   11.89 +text {* The \emph{linear closure} of a vector $x$ is the set of all
   11.90 +scalar multiples of $x$. *};
   11.91  
   11.92  constdefs
   11.93    lin :: "'a => 'a set"
   11.94 -  "lin x == {y. EX a. y = a <*> x}";
   11.95 +  "lin x == {a <*> x | a. True}"; 
   11.96  
   11.97  lemma linD: "x : lin v = (EX a::real. x = a <*> v)";
   11.98 -  by (unfold lin_def) force;
   11.99 +  by (unfold lin_def) fast;
  11.100  
  11.101  lemma linI [intro!!]: "a <*> x0 : lin x0";
  11.102 -  by (unfold lin_def) force;
  11.103 +  by (unfold lin_def) fast;
  11.104  
  11.105  text {* Every vector is contained in its linear closure. *};
  11.106  
  11.107 -lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x:lin x";
  11.108 -proof (unfold lin_def, intro CollectI exI);
  11.109 +lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x : lin x";
  11.110 +proof (unfold lin_def, intro CollectI exI conjI);
  11.111    assume "is_vectorspace V" "x:V";
  11.112    show "x = 1r <*> x"; by (simp!);
  11.113 -qed;
  11.114 +qed simp;
  11.115  
  11.116  text {* Any linear closure is a subspace. *};
  11.117  
  11.118 @@ -162,12 +162,12 @@
  11.119  proof;
  11.120    assume "is_vectorspace V" "x:V";
  11.121    show "<0> : lin x"; 
  11.122 -  proof (unfold lin_def, intro CollectI exI);
  11.123 +  proof (unfold lin_def, intro CollectI exI conjI);
  11.124      show "<0> = 0r <*> x"; by (simp!);
  11.125 -  qed;
  11.126 +  qed simp;
  11.127  
  11.128    show "lin x <= V";
  11.129 -  proof (unfold lin_def, intro subsetI, elim CollectE exE); 
  11.130 +  proof (unfold lin_def, intro subsetI, elim CollectE exE conjE); 
  11.131      fix xa a; assume "xa = a <*> x"; 
  11.132      show "xa:V"; by (simp!);
  11.133    qed;
  11.134 @@ -176,21 +176,23 @@
  11.135    proof (intro ballI);
  11.136      fix x1 x2; assume "x1 : lin x" "x2 : lin x"; 
  11.137      thus "x1 + x2 : lin x";
  11.138 -    proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
  11.139 +    proof (unfold lin_def, elim CollectE exE conjE, 
  11.140 +      intro CollectI exI conjI);
  11.141        fix a1 a2; assume "x1 = a1 <*> x" "x2 = a2 <*> x";
  11.142        show "x1 + x2 = (a1 + a2) <*> x"; 
  11.143          by (simp! add: vs_add_mult_distrib2);
  11.144 -    qed;
  11.145 +    qed simp;
  11.146    qed;
  11.147  
  11.148    show "ALL xa:lin x. ALL a. a <*> xa : lin x"; 
  11.149    proof (intro ballI allI);
  11.150      fix x1 a; assume "x1 : lin x"; 
  11.151      thus "a <*> x1 : lin x";
  11.152 -    proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
  11.153 +    proof (unfold lin_def, elim CollectE exE conjE,
  11.154 +      intro CollectI exI conjI);
  11.155        fix a1; assume "x1 = a1 <*> x";
  11.156        show "a <*> x1 = (a * a1) <*> x"; by (simp!);
  11.157 -    qed;
  11.158 +    qed simp;
  11.159    qed; 
  11.160  qed;
  11.161  
  11.162 @@ -213,7 +215,7 @@
  11.163  instance set :: (plus) plus; by intro_classes;
  11.164  
  11.165  defs vs_sum_def:
  11.166 -  "U + V == {x. EX u:U. EX v:V. x = u + v}";(***  
  11.167 +  "U + V == {u + v | u v. u:U & v:V}"; (***
  11.168  
  11.169  constdefs 
  11.170    vs_sum :: 
  11.171 @@ -223,13 +225,13 @@
  11.172  
  11.173  lemma vs_sumD: 
  11.174    "x: U + V = (EX u:U. EX v:V. x = u + v)";
  11.175 -  by (unfold vs_sum_def) simp;
  11.176 +    by (unfold vs_sum_def) fast;
  11.177  
  11.178  lemmas vs_sumE = vs_sumD [RS iffD1, elimify];
  11.179  
  11.180  lemma vs_sumI [intro!!]: 
  11.181    "[| x:U; y:V; t= x + y |] ==> t : U + V";
  11.182 -  by (unfold vs_sum_def, intro CollectI bexI); 
  11.183 +  by (unfold vs_sum_def) fast;
  11.184  
  11.185  text{* $U$ is a subspace of $U + V$. *};
  11.186  
  11.187 @@ -287,7 +289,7 @@
  11.188      qed (simp!)+;
  11.189    qed;
  11.190  
  11.191 -  show "ALL x: U + V. ALL a. a <*> x : U + V";
  11.192 +  show "ALL x : U + V. ALL a. a <*> x : U + V";
  11.193    proof (intro ballI allI);
  11.194      fix x a; assume "x : U + V";
  11.195      thus "a <*> x : U + V";
  11.196 @@ -348,10 +350,11 @@
  11.197    qed;
  11.198  qed;
  11.199  
  11.200 -text {* An application of the previous lemma will be used in the 
  11.201 -proof of the Hahn-Banach theorem: for an element $y + a \mult x_0$ 
  11.202 -of the direct sum of a vectorspace $H$ and the linear closure of 
  11.203 -$x_0$ the components $y \in H$ and $a$ are unique. *}; 
  11.204 +text {* An application of the previous lemma will be used in the proof
  11.205 +of the Hahn-Banach Theorem (see page \pageref{decomp-H0-use}): for any
  11.206 +element $y + a \mult x_0$ of the direct sum of a vectorspace $H$ and
  11.207 +the linear closure of $x_0$ the components $y \in H$ and $a$ are
  11.208 +uniquely determined. *};
  11.209  
  11.210  lemma decomp_H0: 
  11.211    "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; 
  11.212 @@ -370,9 +373,9 @@
  11.213      proof;
  11.214        show "H Int lin x0 <= {<0>}"; 
  11.215        proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]);
  11.216 -        fix x; assume "x:H" "x:lin x0"; 
  11.217 +        fix x; assume "x:H" "x : lin x0"; 
  11.218          thus "x = <0>";
  11.219 -        proof (unfold lin_def, elim CollectE exE);
  11.220 +        proof (unfold lin_def, elim CollectE exE conjE);
  11.221            fix a; assume "x = a <*> x0";
  11.222            show ?thesis;
  11.223            proof (rule case_split);
  11.224 @@ -388,8 +391,9 @@
  11.225         qed;
  11.226        qed;
  11.227        show "{<0>} <= H Int lin x0";
  11.228 -      proof (intro subsetI, elim singletonE, intro IntI, simp+);
  11.229 -        show "<0> : H"; ..;
  11.230 +      proof (intro subsetI, elim singletonE, intro IntI, 
  11.231 +        (simp only:)+);
  11.232 +        show "<0>:H"; ..;
  11.233          from lin_vs; show "<0> : lin x0"; ..;
  11.234        qed;
  11.235      qed;
  11.236 @@ -404,20 +408,20 @@
  11.237    qed;
  11.238  qed;
  11.239  
  11.240 -text {* Since for an element $y + a \mult x_0$ of the direct sum 
  11.241 +text {* Since for any element $y + a \mult x_0$ of the direct sum 
  11.242  of a vectorspace $H$ and the linear closure of $x_0$ the components
  11.243 -$y\in H$ and $a$ are unique, follows from $y\in H$ the fact that 
  11.244 +$y\in H$ and $a$ are unique, it follows from $y\in H$ that 
  11.245  $a = 0$.*}; 
  11.246  
  11.247  lemma decomp_H0_H: 
  11.248 -  "[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E;
  11.249 +  "[| is_vectorspace E; is_subspace H E; t:H; x0 ~: H; x0:E;
  11.250    x0 ~= <0> |] 
  11.251    ==> (SOME (y, a). t = y + a <*> x0 & y : H) = (t, 0r)";
  11.252  proof (rule, unfold split_paired_all);
  11.253 -  assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E"
  11.254 +  assume "is_vectorspace E" "is_subspace H E" "t:H" "x0 ~: H" "x0:E"
  11.255      "x0 ~= <0>";
  11.256    have h: "is_vectorspace H"; ..;
  11.257 -  fix y a; presume t1: "t = y + a <*> x0" and "y : H";
  11.258 +  fix y a; presume t1: "t = y + a <*> x0" and "y:H";
  11.259    have "y = t & a = 0r"; 
  11.260      by (rule decomp_H0) (assumption | (simp!))+;
  11.261    thus "(y, a) = (t, 0r)"; by (simp!);
  11.262 @@ -428,14 +432,14 @@
  11.263  $h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *};
  11.264  
  11.265  lemma h0_definite:
  11.266 -  "[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
  11.267 +  "[| h0 == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
  11.268                  in (h y) + a * xi);
  11.269    x = y + a <*> x0; is_vectorspace E; is_subspace H E;
  11.270    y:H; x0 ~: H; x0:E; x0 ~= <0> |]
  11.271    ==> h0 x = h y + a * xi";
  11.272  proof -;  
  11.273    assume 
  11.274 -    "h0 = (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
  11.275 +    "h0 == (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
  11.276                 in (h y) + a * xi)"
  11.277      "x = y + a <*> x0" "is_vectorspace E" "is_subspace H E"
  11.278      "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
  11.279 @@ -443,25 +447,25 @@
  11.280      by (simp! add: vs_sum_def lin_def) force+;
  11.281    have "EX! xa. ((\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)"; 
  11.282    proof;
  11.283 -    show "EX xa. ((%(y, a). x = y + a <*> x0 & y:H) xa)";
  11.284 +    show "EX xa. ((\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)";
  11.285        by (force!);
  11.286    next;
  11.287      fix xa ya;
  11.288 -    assume "(%(y,a). x = y + a <*> x0 & y : H) xa"
  11.289 -           "(%(y,a). x = y + a <*> x0 & y : H) ya";
  11.290 +    assume "(\<lambda>(y,a). x = y + a <*> x0 & y : H) xa"
  11.291 +           "(\<lambda>(y,a). x = y + a <*> x0 & y : H) ya";
  11.292      show "xa = ya"; ;
  11.293      proof -;
  11.294        show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; 
  11.295          by (rule Pair_fst_snd_eq [RS iffD2]);
  11.296 -      have x: "x = (fst xa) + (snd xa) <*> x0 & (fst xa) : H"; 
  11.297 +      have x: "x = fst xa + snd xa <*> x0 & fst xa : H"; 
  11.298          by (force!);
  11.299 -      have y: "x = (fst ya) + (snd ya) <*> x0 & (fst ya) : H"; 
  11.300 +      have y: "x = fst ya + snd ya <*> x0 & fst ya : H"; 
  11.301          by (force!);
  11.302        from x y; show "fst xa = fst ya & snd xa = snd ya"; 
  11.303          by (elim conjE) (rule decomp_H0, (simp!)+);
  11.304      qed;
  11.305    qed;
  11.306 -  hence eq: "(SOME (y, a). (x = y + a <*> x0 & y:H)) = (y, a)"; 
  11.307 +  hence eq: "(SOME (y, a). x = y + a <*> x0 & y:H) = (y, a)"; 
  11.308      by (rule select1_equality) (force!);
  11.309    thus "h0 x = h y + a * xi"; by (simp! add: Let_def);
  11.310  qed;
    12.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy	Fri Oct 29 19:24:20 1999 +0200
    12.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy	Fri Oct 29 20:18:34 1999 +0200
    12.3 @@ -10,14 +10,11 @@
    12.4  subsection {* Signature *};
    12.5  
    12.6  text {* For the definition of real vector spaces a type $\alpha$
    12.7 -of the sort $\idt{plus}, \idt{minus}$ is considered, on which a
    12.8 -real scalar multiplication $\mult$ is defined, and which has an zero 
    12.9 -element $\zero$.*};
   12.10 +of the sort $\{ \idt{plus}, \idt{minus}\}$ is considered, on which a
   12.11 +real scalar multiplication $\mult$, and a zero 
   12.12 +element $\zero$ is defined. *};
   12.13  
   12.14  consts
   12.15 -(***
   12.16 -  sum	:: "['a, 'a] => 'a"                         (infixl "+" 65)
   12.17 -***)
   12.18    prod  :: "[real, 'a] => 'a"                       (infixr "<*>" 70)
   12.19    zero  :: 'a                                       ("<0>");
   12.20  
   12.21 @@ -45,7 +42,7 @@
   12.22    and commutative; $\minus x$ is the inverse of $x$ w.~r.~t.~addition
   12.23    and $\zero$ is the neutral element of addition.  Addition and
   12.24    multiplication are distributive; scalar multiplication is
   12.25 -  associative and the real $1$ is the neutral element of scalar
   12.26 +  associative and the real number $1$ is the neutral element of scalar
   12.27    multiplication.
   12.28  *};
   12.29  
   12.30 @@ -55,7 +52,7 @@
   12.31     & (ALL x:V. ALL y:V. ALL z:V. ALL a b.
   12.32          x + y : V                                 
   12.33        & a <*> x : V                                 
   12.34 -      & x + y + z = x + (y + z)             
   12.35 +      & (x + y) + z = x + (y + z)             
   12.36        & x + y = y + x                           
   12.37        & x - x = <0>                               
   12.38        & <0> + x = x                               
   12.39 @@ -72,8 +69,8 @@
   12.40  lemma vsI [intro]:
   12.41    "[| <0>:V; 
   12.42    ALL x:V. ALL y:V. x + y : V; 
   12.43 -  ALL x:V. ALL a. a <*> x : V;    
   12.44 -  ALL x:V. ALL y:V. ALL z:V. x + y + z = x + (y + z);
   12.45 +  ALL x:V. ALL a. a <*> x : V;  
   12.46 +  ALL x:V. ALL y:V. ALL z:V. (x + y) + z = x + (y + z);
   12.47    ALL x:V. ALL y:V. x + y = y + x;
   12.48    ALL x:V. x - x = <0>;
   12.49    ALL x:V. <0> + x = x;
   12.50 @@ -82,7 +79,7 @@
   12.51    ALL x:V. ALL a b. (a * b) <*> x = a <*> b <*> x; 
   12.52    ALL x:V. 1r <*> x = x; 
   12.53    ALL x:V. - x = (- 1r) <*> x; 
   12.54 -  ALL x:V. ALL y:V. x - y = x + - y|] ==> is_vectorspace V";
   12.55 +  ALL x:V. ALL y:V. x - y = x + - y |] ==> is_vectorspace V";
   12.56  proof (unfold is_vectorspace_def, intro conjI ballI allI);
   12.57    fix x y z; 
   12.58    assume "x:V" "y:V" "z:V"
   12.59 @@ -113,7 +110,7 @@
   12.60    by (unfold is_vectorspace_def) simp;
   12.61   
   12.62  lemma vs_add_closed [simp, intro!!]: 
   12.63 -  "[| is_vectorspace V; x:V; y:V|] ==> x + y : V"; 
   12.64 +  "[| is_vectorspace V; x:V; y:V |] ==> x + y : V"; 
   12.65    by (unfold is_vectorspace_def) simp;
   12.66  
   12.67  lemma vs_mult_closed [simp, intro!!]: 
   12.68 @@ -121,7 +118,7 @@
   12.69    by (unfold is_vectorspace_def) simp;
   12.70  
   12.71  lemma vs_diff_closed [simp, intro!!]: 
   12.72 - "[| is_vectorspace V; x:V; y:V|] ==> x - y : V";
   12.73 + "[| is_vectorspace V; x:V; y:V |] ==> x - y : V";
   12.74    by (simp add: diff_eq1 negate_eq1);
   12.75  
   12.76  lemma vs_neg_closed  [simp, intro!!]: 
   12.77 @@ -129,8 +126,8 @@
   12.78    by (simp add: negate_eq1);
   12.79  
   12.80  lemma vs_add_assoc [simp]:  
   12.81 -  "[| is_vectorspace V; x:V; y:V; z:V|]
   12.82 -   ==> x + y + z = x + (y + z)";
   12.83 +  "[| is_vectorspace V; x:V; y:V; z:V |]
   12.84 +   ==> (x + y) + z = x + (y + z)";
   12.85    by (unfold is_vectorspace_def) fast;
   12.86  
   12.87  lemma vs_add_commute [simp]: 
   12.88 @@ -155,8 +152,8 @@
   12.89    "[| is_vectorspace V; x:V |] ==>  x - x = <0>"; 
   12.90    by (unfold is_vectorspace_def) simp;
   12.91  
   12.92 -text {* The existence of the zero element a vector space
   12.93 -follows from the non-emptyness of the vector space. *};
   12.94 +text {* The existence of the zero element of a vector space
   12.95 +follows from the non-emptiness of carrier set. *};
   12.96  
   12.97  lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> <0>:V";
   12.98  proof -; 
   12.99 @@ -228,12 +225,12 @@
  12.100    finally; show ?thesis; .;
  12.101  qed;
  12.102  
  12.103 -(*text_raw {* \paragraph {Further derived laws:} *};*)
  12.104 +(*text_raw {* \paragraph {Further derived laws.} *};*)
  12.105  text_raw {* \medskip *};
  12.106  text{* Further derived laws: *};
  12.107  
  12.108  lemma vs_mult_zero_left [simp]: 
  12.109 -  "[| is_vectorspace V; x:V|] ==> 0r <*> x = <0>";
  12.110 +  "[| is_vectorspace V; x:V |] ==> 0r <*> x = <0>";
  12.111  proof -;
  12.112    assume "is_vectorspace V" "x:V";
  12.113    have  "0r <*> x = (1r - 1r) <*> x"; by (simp only: real_diff_self);
  12.114 @@ -304,11 +301,11 @@
  12.115  qed;
  12.116  
  12.117  lemma vs_add_minus_cancel [simp]:  
  12.118 -  "[| is_vectorspace V; x:V; y:V |] ==>  x + (- x + y) = y"; 
  12.119 +  "[| is_vectorspace V; x:V; y:V |] ==> x + (- x + y) = y"; 
  12.120    by (simp add: vs_add_assoc [RS sym] del: vs_add_commute); 
  12.121  
  12.122  lemma vs_minus_add_cancel [simp]: 
  12.123 -  "[| is_vectorspace V; x:V; y:V |] ==>  - x + (x + y) = y"; 
  12.124 +  "[| is_vectorspace V; x:V; y:V |] ==> - x + (x + y) = y"; 
  12.125    by (simp add: vs_add_assoc [RS sym] del: vs_add_commute); 
  12.126  
  12.127  lemma vs_minus_add_distrib [simp]:  
  12.128 @@ -325,7 +322,7 @@
  12.129    by (simp add:diff_eq1);
  12.130  
  12.131  lemma vs_add_left_cancel:
  12.132 -  "[| is_vectorspace V; x:V; y:V; z:V|] 
  12.133 +  "[| is_vectorspace V; x:V; y:V; z:V |] 
  12.134     ==> (x + y = x + z) = (y = z)"  
  12.135    (concl is "?L = ?R");
  12.136  proof;
  12.137 @@ -338,7 +335,7 @@
  12.138    also; have "- x + ... = - x + x + z"; 
  12.139      by (rule vs_add_assoc [RS sym]) (simp!)+;
  12.140    also; have "... = z"; by (simp!);
  12.141 -  finally; show ?R;.;
  12.142 +  finally; show ?R; .;
  12.143  qed force;
  12.144  
  12.145  lemma vs_add_right_cancel: 
  12.146 @@ -381,7 +378,7 @@
  12.147      by (simp! only: vs_mult_assoc);
  12.148    also; assume ?L;
  12.149    also; have "rinv a <*> ... = y"; by (simp!);
  12.150 -  finally; show ?R;.;
  12.151 +  finally; show ?R; .;
  12.152  qed simp;
  12.153  
  12.154  lemma vs_mult_right_cancel: (*** forward ***)
  12.155 @@ -437,7 +434,7 @@
  12.156      also; from vs; have "... = z + <0>"; 
  12.157        by (simp only: vs_add_minus_left);
  12.158      also; from vs; have "... = z"; by (simp only: vs_add_zero_right);
  12.159 -    finally; show ?R;.;
  12.160 +    finally; show ?R; .;
  12.161    next;
  12.162      assume ?R;
  12.163      hence "z - y = (x + y) - y"; by simp;
  12.164 @@ -451,7 +448,7 @@
  12.165  qed;
  12.166  
  12.167  lemma vs_add_minus_eq_minus: 
  12.168 -  "[| is_vectorspace V; x:V; y:V; x + y = <0>|] ==> x = - y"; 
  12.169 +  "[| is_vectorspace V; x:V; y:V; x + y = <0> |] ==> x = - y"; 
  12.170  proof -;
  12.171    assume "is_vectorspace V" "x:V" "y:V"; 
  12.172    have "x = (- y + y) + x"; by (simp!);
  12.173 @@ -473,11 +470,11 @@
  12.174  qed;
  12.175  
  12.176  lemma vs_add_diff_swap:
  12.177 -  "[| is_vectorspace V; a:V; b:V; c:V; d:V; a + b = c + d|] 
  12.178 +  "[| is_vectorspace V; a:V; b:V; c:V; d:V; a + b = c + d |] 
  12.179    ==> a - c = d - b";
  12.180  proof -; 
  12.181    assume vs: "is_vectorspace V" "a:V" "b:V" "c:V" "d:V" 
  12.182 -  and eq: "a + b = c + d";
  12.183 +    and eq: "a + b = c + d";
  12.184    have "- c + (a + b) = - c + (c + d)"; 
  12.185      by (simp! add: vs_add_left_cancel);
  12.186    also; have "... = d"; by (rule vs_minus_add_cancel);
  12.187 @@ -491,9 +488,9 @@
  12.188  qed;
  12.189  
  12.190  lemma vs_add_cancel_21: 
  12.191 -  "[| is_vectorspace V; x:V; y:V; z:V; u:V|] 
  12.192 +  "[| is_vectorspace V; x:V; y:V; z:V; u:V |] 
  12.193    ==> (x + (y + z) = y + u) = ((x + z) = u)"
  12.194 -  (concl is "?L = ?R" ); 
  12.195 +  (concl is "?L = ?R"); 
  12.196  proof -; 
  12.197    assume "is_vectorspace V" "x:V" "y:V""z:V" "u:V";
  12.198    show "?L = ?R";
    13.1 --- a/src/HOL/Real/HahnBanach/ZornLemma.thy	Fri Oct 29 19:24:20 1999 +0200
    13.2 +++ b/src/HOL/Real/HahnBanach/ZornLemma.thy	Fri Oct 29 20:18:34 1999 +0200
    13.3 @@ -8,10 +8,10 @@
    13.4  theory ZornLemma = Aux + Zorn:;
    13.5  
    13.6  text{* 
    13.7 -Zorn's Lemmas says: if every linear ordered subset of an ordered set 
    13.8 +Zorn's Lemmas states: if every linear ordered subset of an ordered set 
    13.9  $S$ has an upper bound in $S$, then there exists a maximal element in $S$.
   13.10 -In our application $S$ is a set of sets, ordered by set inclusion. Since 
   13.11 -the union of a chain of sets is an upperbound for all elements of the 
   13.12 +In our application, $S$ is a set of sets ordered by set inclusion. Since 
   13.13 +the union of a chain of sets is an upper bound for all elements of the 
   13.14  chain, the conditions of Zorn's lemma can be modified:
   13.15  if $S$ is non-empty, it suffices to show that for every non-empty 
   13.16  chain $c$ in $S$ the union of $c$ also lies in $S$.
   13.17 @@ -21,6 +21,8 @@
   13.18    "a:S ==> (!!c. c: chain S ==> EX x. x:c ==> Union c : S) 
   13.19    ==>  EX y: S. ALL z: S. y <= z --> y = z";
   13.20  proof (rule Zorn_Lemma2);
   13.21 +  txt_raw{* \footnote{See
   13.22 +  \url{http://isabelle.in.tum.de/library/HOL/HOL-Real/Zorn.html}}*};
   13.23    assume aS: "a:S";
   13.24    assume r: "!!c. c: chain S ==> EX x. x:c ==> Union c : S";
   13.25    show "ALL c:chain S. EX y:S. ALL z:c. z <= y";
   13.26 @@ -30,13 +32,13 @@
   13.27      proof (rule case_split);
   13.28   
   13.29        txt{* If $c$ is an empty chain, then every element
   13.30 -      in $S$ is an upperbound of $c$. *};
   13.31 +      in $S$ is an upper bound of $c$. *};
   13.32  
   13.33        assume "c={}"; 
   13.34        with aS; show ?thesis; by fast;
   13.35  
   13.36        txt{* If $c$ is non-empty, then $\Union c$ 
   13.37 -      is an upperbound of $c$, that lies in $S$. *};
   13.38 +      is an upper bound of $c$, lying in $S$. *};
   13.39  
   13.40      next;
   13.41        assume c: "c~={}";
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/src/HOL/Real/HahnBanach/document/bbb.sty	Fri Oct 29 20:18:34 1999 +0200
    14.3 @@ -0,0 +1,25 @@
    14.4 +% bbb.sty  10-Nov-1991, 27-Mar-1994
    14.5 +%
    14.6 +% blackboard-bold symbols: B C D E F G H I J K L M N O P Q R T U Z
    14.7 +%
    14.8 +
    14.9 +\def\bbbB{{{\rm I}\mkern-3.8mu{\rm B}}}
   14.10 +\def\bbbC{{{\rm C}\mkern-15mu{\phantom{\rm t}\vrule}\mkern9mu}}
   14.11 +\def\bbbD{{{\rm I}\mkern-3.8mu{\rm D}}}
   14.12 +\def\bbbE{{{\rm I}\mkern-3.8mu{\rm E}}}
   14.13 +\def\bbbF{{{\rm I}\mkern-3.8mu{\rm F}}}
   14.14 +\def\bbbG{{{\rm G}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
   14.15 +\def\bbbH{{{\rm I}\mkern-3.8mu{\rm H}}}
   14.16 +\def\bbbI{{{\rm I}\mkern-12mu{\phantom{\rm t}\vrule}\mkern6mu}}
   14.17 +\def\bbbJ{{{\rm J}\mkern-12mu{\phantom{\rm t}\vrule}\mkern6mu}}
   14.18 +\def\bbbK{{{\rm I}\mkern-3.8mu{\rm K}}}
   14.19 +\def\bbbL{{{\rm I}\mkern-3.8mu{\rm L}}}
   14.20 +\def\bbbM{{{\rm I}\mkern-3.8mu{\rm M}}}
   14.21 +\def\bbbN{{{\rm I}\mkern-3.8mu{\rm N}}}
   14.22 +\def\bbbO{{{\rm O}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
   14.23 +\def\bbbP{{{\rm I}\mkern-3.8mu{\rm P}}}
   14.24 +\def\bbbQ{{{\rm Q}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
   14.25 +\def\bbbR{{{\rm I}\mkern-3.8mu{\rm R}}}
   14.26 +\def\bbbT{{{\rm T}\mkern-16mu{\phantom{\rm t}\vrule}\mkern10mu}}
   14.27 +\def\bbbU{{{\rm U}\mkern-15mu{\phantom{\rm t}\vrule}\mkern9mu}}
   14.28 +\def\bbbZ{{{\sf Z}\mkern-7.5mu{\sf Z}}}
    15.1 --- a/src/HOL/Real/HahnBanach/document/notation.tex	Fri Oct 29 19:24:20 1999 +0200
    15.2 +++ b/src/HOL/Real/HahnBanach/document/notation.tex	Fri Oct 29 20:18:34 1999 +0200
    15.3 @@ -1,11 +1,10 @@
    15.4  
    15.5  \renewcommand{\isamarkupheader}[1]{\section{#1}}
    15.6 -\newcommand{\isasymbollambda}{${\mathtt{\lambda}}$}
    15.7 -
    15.8 +\newcommand{\isasymlambda}{${\mathtt{\lambda}}$}
    15.9 +\newcommand{\isasymprod}{\emph{$\mult$}}
   15.10 +\newcommand{\isasymzero}{\emph{$\zero$}}
   15.11  
   15.12  
   15.13 -\newcommand{\name}[1]{\textsf{#1}}
   15.14 -
   15.15  \newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
   15.16  \newcommand{\var}[1]{{?\!#1}}
   15.17  \DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
   15.18 @@ -13,30 +12,22 @@
   15.19  
   15.20  \newenvironment{matharray}[1]{\[\begin{array}{#1}}{\end{array}\]}
   15.21  
   15.22 -\newcommand{\ty}{{\mathbin{:\,}}}
   15.23  \newcommand{\To}{\to}
   15.24  \newcommand{\dt}{{\mathpunct.}}
   15.25 -\newcommand{\all}[1]{\forall #1\dt\;}
   15.26 -\newcommand{\ex}[1]{\exists #1\dt\;}
   15.27 -\newcommand{\EX}[1]{\exists #1\dt\;}
   15.28 -\newcommand{\eps}[1]{\epsilon\; #1}
   15.29 -%\newcommand{\Forall}{\mathop\bigwedge}
   15.30 +\newcommand{\Ex}[1]{\exists #1\dt\;}
   15.31  \newcommand{\Forall}{\forall}
   15.32  \newcommand{\All}[1]{\Forall #1\dt\;}
   15.33 -\newcommand{\ALL}[1]{\Forall #1\dt\;}
   15.34 -\newcommand{\Eps}[1]{\Epsilon #1\dt\;}
   15.35  \newcommand{\Eq}{\mathbin{\,\equiv\,}}
   15.36 -\newcommand{\True}{\name{true}}
   15.37 -\newcommand{\False}{\name{false}}
   15.38  \newcommand{\Impl}{\Rightarrow}
   15.39  \newcommand{\And}{\;\land\;}
   15.40  \newcommand{\Or}{\;\lor\;}
   15.41  \newcommand{\Le}{\le}
   15.42  \newcommand{\Lt}{\lt}
   15.43  \newcommand{\lam}[1]{\mathop{\lambda} #1\dt\;}
   15.44 -\newcommand{\ap}{\mathbin{}}
   15.45 +\newcommand{\ap}{\mathpalette{\mathbin{\!}}{\mathbin{\!}}{\mathbin{}}{\mathbin{}}}
   15.46  \newcommand{\Union}{\bigcup}
   15.47 -
   15.48 +\newcommand{\Un}{\cup}
   15.49 +\newcommand{\Int}{\cap}
   15.50  
   15.51  \newcommand{\norm}[1]{\left\|#1\right\|}
   15.52  \newcommand{\fnorm}[1]{\left\|#1\right\|}
   15.53 @@ -44,20 +35,8 @@
   15.54  \newcommand{\plus}{\mathbin{\mathbf +}}
   15.55  \newcommand{\minus}{\mathbin{\mathbf -}}
   15.56  \newcommand{\mult}{\mathbin{\mathbf\odot}}
   15.57 -\newcommand{\1}{\mathord{\mathrm{1}}}
   15.58 -%\newcommand{\zero}{{\mathord{\small\sl\tt {<0>}}}}
   15.59 -%\newcommand{\plus}{{\mathbin{\;\small\sl\tt {[+]}\;}}}
   15.60 -%\newcommand{\minus}{{\mathbin{\;\small\sl\tt {[-]}\;}}}
   15.61 -%\newcommand{\mult}{{\mathbin{\;\small\sl\tt {[*]}\;}}}
   15.62 -%\newcommand{\1}{{\mathord{\mathrb{1}}}}
   15.63 -\newcommand{\fl}{{\mathord{\bf\underline{\phantom{i}}}}}
   15.64 -\renewcommand{\times}{\;{\mathbin{\cdot}}\;}
   15.65 -\newcommand{\qed}{\hfill~$\Box$}
   15.66  
   15.67 -\newcommand{\isasymbolprod}{$\mult$}
   15.68 -\newcommand{\isasymbolzero}{$\zero$}
   15.69 -
   15.70 -%%% Local Variables: 
   15.71 +%%% Local Variables:
   15.72  %%% mode: latex
   15.73  %%% TeX-master: "root"
   15.74 -%%% End: 
   15.75 +%%% End:
    16.1 --- a/src/HOL/Real/HahnBanach/document/root.tex	Fri Oct 29 19:24:20 1999 +0200
    16.2 +++ b/src/HOL/Real/HahnBanach/document/root.tex	Fri Oct 29 20:18:34 1999 +0200
    16.3 @@ -4,6 +4,7 @@
    16.4  \usepackage{comment}
    16.5  \usepackage{latexsym,theorem}
    16.6  \usepackage{isabelle,pdfsetup} %last one!
    16.7 +\usepackage{bbb}
    16.8  
    16.9  \input{notation}
   16.10  
   16.11 @@ -13,11 +14,13 @@
   16.12  \pagenumbering{arabic}
   16.13  
   16.14  \title{The Hahn-Banach Theorem for Real Vector Spaces}
   16.15 -\author{Gertrud Bauer}
   16.16 +
   16.17 +\author{Gertrud Bauer \\ \url{http://www.in.tum.de/~bauerg/}}
   16.18 +\maketitle
   16.19  \maketitle
   16.20  
   16.21  \begin{abstract}
   16.22 -  The Hahn-Banach theorem is one of the most fundamental results in functional
   16.23 +  The Hahn-Banach Theorem is one of the most fundamental results in functional
   16.24    analysis. We present a fully formal proof of two versions of the theorem,
   16.25    one for general linear spaces and another for normed spaces.  This
   16.26    development is based on simply-typed classical set-theory, as provided by
   16.27 @@ -31,11 +34,11 @@
   16.28  \clearpage
   16.29  \section{Preface}
   16.30  
   16.31 -This is a fully formal proof of the Hahn-Banach theorem. It closely follows
   16.32 +This is a fully formal proof of the Hahn-Banach Theorem. It closely follows
   16.33  the informal presentation given in the textbook \cite[\S 36]{Heuser:1986}.
   16.34  Another formal proof of the same theorem has been done in Mizar
   16.35  \cite{Nowak:1993}.  A general overview of the relevance and history of the
   16.36 -Hahn-Banach theorem is given in \cite{Narici:1996}.
   16.37 +Hahn-Banach Theorem is given in \cite{Narici:1996}.
   16.38  
   16.39  \medskip The document is structured as follows.  The first part contains
   16.40  definitions of basic notions of linear algebra: vector spaces, subspaces,