src/HOL/Real/HahnBanach/Subspace.thy
changeset 7917 5e5b9813cce7
parent 7808 fd019ac3485f
child 7927 b50446a33c16
     1.1 --- a/src/HOL/Real/HahnBanach/Subspace.thy	Fri Oct 22 18:41:00 1999 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Subspace.thy	Fri Oct 22 20:14:31 1999 +0200
     1.3 @@ -6,28 +6,30 @@
     1.4  
     1.5  header {* Subspaces *};
     1.6  
     1.7 -theory Subspace = LinearSpace:;
     1.8 +theory Subspace = VectorSpace:;
     1.9  
    1.10  
    1.11 -subsection {* Subspaces *};
    1.12 +subsection {* Definition *};
    1.13  
    1.14 -constdefs
    1.15 -  is_subspace ::  "['a set, 'a set] => bool"
    1.16 -  "is_subspace U V ==  <0>:U  & U <= V 
    1.17 -     &  (ALL x:U. ALL y:U. ALL a. x [+] y : U                          
    1.18 -                       & a [*] x : U)";                            
    1.19 +text {* A non-empty subset $U$ of a vector space $V$ is a 
    1.20 +\emph{subspace} of $V$, iff $U$ is closed under addition and 
    1.21 +scalar multiplication. *};
    1.22 +
    1.23 +constdefs 
    1.24 +  is_subspace ::  "['a::{minus, plus} set, 'a set] => bool"
    1.25 +  "is_subspace U V ==  U ~= {}  & U <= V 
    1.26 +     &  (ALL x:U. ALL y:U. ALL a. x + y : U & a <*> x : U)";
    1.27  
    1.28  lemma subspaceI [intro]: 
    1.29 -  "[| <0>:U; U <= V; ALL x:U. ALL y:U. (x [+] y : U); 
    1.30 -  ALL x:U. ALL a. a [*] x : U |]
    1.31 +  "[| <0>:U; U <= V; ALL x:U. ALL y:U. (x + y : U); 
    1.32 +  ALL x:U. ALL a. a <*> x : U |]
    1.33    ==> is_subspace U V";
    1.34 -  by (unfold is_subspace_def) simp;
    1.35 +proof (unfold is_subspace_def, intro conjI); 
    1.36 +  assume "<0>:U"; thus "U ~= {}"; by fast;
    1.37 +qed (simp+);
    1.38  
    1.39 -lemma "is_subspace U V ==> U ~= {}";
    1.40 -  by (unfold is_subspace_def) force;
    1.41 -
    1.42 -lemma zero_in_subspace [intro !!]: "is_subspace U V ==> <0>:U";
    1.43 -  by (unfold is_subspace_def) simp;;
    1.44 +lemma subspace_not_empty [intro!!]: "is_subspace U V ==> U ~= {}";
    1.45 +  by (unfold is_subspace_def) simp; 
    1.46  
    1.47  lemma subspace_subset [intro !!]: "is_subspace U V ==> U <= V";
    1.48    by (unfold is_subspace_def) simp;
    1.49 @@ -37,20 +39,44 @@
    1.50    by (unfold is_subspace_def) force;
    1.51  
    1.52  lemma subspace_add_closed [simp, intro!!]: 
    1.53 -  "[| is_subspace U V; x: U; y: U |] ==> x [+] y: U";
    1.54 +  "[| is_subspace U V; x: U; y: U |] ==> x + y : U";
    1.55    by (unfold is_subspace_def) simp;
    1.56  
    1.57  lemma subspace_mult_closed [simp, intro!!]: 
    1.58 -  "[| is_subspace U V; x: U |] ==> a [*] x: U";
    1.59 +  "[| is_subspace U V; x: U |] ==> a <*> x: U";
    1.60    by (unfold is_subspace_def) simp;
    1.61  
    1.62  lemma subspace_diff_closed [simp, intro!!]: 
    1.63 -  "[| is_subspace U V; x: U; y: U |] ==> x [-] y: U";
    1.64 -  by (unfold diff_def negate_def) simp;
    1.65 +  "[| is_subspace U V; is_vectorspace V; x: U; y: U |] 
    1.66 +  ==> x - y: U";
    1.67 +  by (simp! add: diff_eq1 negate_eq1);
    1.68 +
    1.69 +text {* Similar as for linear spaces, the existence of the 
    1.70 +zero element in every subspace follws from the non-emptyness 
    1.71 +of the subspace and vector space laws.*};
    1.72 +
    1.73 +lemma zero_in_subspace [intro !!]:
    1.74 +  "[| is_subspace U V; is_vectorspace V |] ==> <0>:U";
    1.75 +proof -; 
    1.76 +  assume "is_subspace U V" and v: "is_vectorspace V";
    1.77 +  have "U ~= {}"; ..;
    1.78 +  hence "EX x. x:U"; by force;
    1.79 +  thus ?thesis; 
    1.80 +  proof; 
    1.81 +    fix x; assume u: "x:U"; 
    1.82 +    hence "x:V"; by (simp!);
    1.83 +    with v; have "<0> = x - x"; by (simp!);
    1.84 +    also; have "... : U"; by (rule subspace_diff_closed);
    1.85 +    finally; show ?thesis; .;
    1.86 +  qed;
    1.87 +qed;
    1.88  
    1.89  lemma subspace_neg_closed [simp, intro!!]: 
    1.90 -  "[| is_subspace U V; x: U |] ==> [-] x: U";
    1.91 -  by (unfold negate_def) simp;
    1.92 +  "[| is_subspace U V; is_vectorspace V; x: U |] ==> - x: U";
    1.93 +  by (simp add: negate_eq1);
    1.94 +
    1.95 +text_raw {* \medskip *};
    1.96 +text {* Further derived laws: Every subspace is a vector space. *};
    1.97  
    1.98  lemma subspace_vs [intro!!]:
    1.99    "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U";
   1.100 @@ -59,40 +85,48 @@
   1.101    show ?thesis;
   1.102    proof; 
   1.103      show "<0>:U"; ..;
   1.104 -    show "ALL x:U. ALL a. a [*] x : U"; by (simp!);
   1.105 -    show "ALL x:U. ALL y:U. x [+] y : U"; by (simp!);
   1.106 +    show "ALL x:U. ALL a. a <*> x : U"; by (simp!);
   1.107 +    show "ALL x:U. ALL y:U. x + y : U"; by (simp!);
   1.108 +    show "ALL x:U. - x = -1r <*> x"; by (simp! add: negate_eq1);
   1.109 +    show "ALL x:U. ALL y:U. x - y =  x + - y"; 
   1.110 +      by (simp! add: diff_eq1);
   1.111    qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+;
   1.112  qed;
   1.113  
   1.114 +text {* The subspace relation is reflexive. *};
   1.115 +
   1.116  lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V";
   1.117  proof; 
   1.118    assume "is_vectorspace V";
   1.119    show "<0> : V"; ..;
   1.120    show "V <= V"; ..;
   1.121 -  show "ALL x:V. ALL y:V. x [+] y : V"; by (simp!);
   1.122 -  show "ALL x:V. ALL a. a [*] x : V"; by (simp!);
   1.123 +  show "ALL x:V. ALL y:V. x + y : V"; by (simp!);
   1.124 +  show "ALL x:V. ALL a. a <*> x : V"; by (simp!);
   1.125  qed;
   1.126  
   1.127 +text {* The subspace relation is transitive. *};
   1.128 +
   1.129  lemma subspace_trans: 
   1.130 -  "[| is_subspace U V; is_subspace V W |] ==> is_subspace U W";
   1.131 +  "[| is_subspace U V; is_vectorspace V; is_subspace V W |] 
   1.132 +  ==> is_subspace U W";
   1.133  proof; 
   1.134 -  assume "is_subspace U V" "is_subspace V W";
   1.135 +  assume "is_subspace U V" "is_subspace V W" "is_vectorspace V";
   1.136    show "<0> : U"; ..;
   1.137  
   1.138    have "U <= V"; ..;
   1.139    also; have "V <= W"; ..;
   1.140    finally; show "U <= W"; .;
   1.141  
   1.142 -  show "ALL x:U. ALL y:U. x [+] y : U"; 
   1.143 +  show "ALL x:U. ALL y:U. x + y : U"; 
   1.144    proof (intro ballI);
   1.145      fix x y; assume "x:U" "y:U";
   1.146 -    show "x [+] y : U"; by (simp!);
   1.147 +    show "x + y : U"; by (simp!);
   1.148    qed;
   1.149  
   1.150 -  show "ALL x:U. ALL a. a [*] x : U";
   1.151 +  show "ALL x:U. ALL a. a <*> x : U";
   1.152    proof (intro ballI allI);
   1.153      fix x a; assume "x:U";
   1.154 -    show "a [*] x : U"; by (simp!);
   1.155 +    show "a <*> x : U"; by (simp!);
   1.156    qed;
   1.157  qed;
   1.158  
   1.159 @@ -100,60 +134,68 @@
   1.160  
   1.161  subsection {* Linear closure *};
   1.162  
   1.163 +text {* The \emph{linear closure} of a vector $x$ is the set of all 
   1.164 +multiples of $x$. *};
   1.165  
   1.166  constdefs
   1.167    lin :: "'a => 'a set"
   1.168 -  "lin x == {y. ? a. y = a [*] x}";
   1.169 +  "lin x == {y. EX a. y = a <*> x}";
   1.170  
   1.171 -lemma linD: "x : lin v = (? a::real. x = a [*] v)";
   1.172 +lemma linD: "x : lin v = (EX a::real. x = a <*> v)";
   1.173    by (unfold lin_def) force;
   1.174  
   1.175 -lemma linI [intro!!]: "a [*] x0 : lin x0";
   1.176 +lemma linI [intro!!]: "a <*> x0 : lin x0";
   1.177    by (unfold lin_def) force;
   1.178  
   1.179 +text {* Every vector is contained in its linear closure. *};
   1.180 +
   1.181  lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x:lin x";
   1.182  proof (unfold lin_def, intro CollectI exI);
   1.183    assume "is_vectorspace V" "x:V";
   1.184 -  show "x = 1r [*] x"; by (simp!);
   1.185 +  show "x = 1r <*> x"; by (simp!);
   1.186  qed;
   1.187  
   1.188 +text {* Any linear closure is a subspace. *};
   1.189 +
   1.190  lemma lin_subspace [intro!!]: 
   1.191    "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V";
   1.192  proof;
   1.193    assume "is_vectorspace V" "x:V";
   1.194    show "<0> : lin x"; 
   1.195    proof (unfold lin_def, intro CollectI exI);
   1.196 -    show "<0> = 0r [*] x"; by (simp!);
   1.197 +    show "<0> = 0r <*> x"; by (simp!);
   1.198    qed;
   1.199  
   1.200    show "lin x <= V";
   1.201    proof (unfold lin_def, intro subsetI, elim CollectE exE); 
   1.202 -    fix xa a; assume "xa = a [*] x"; 
   1.203 +    fix xa a; assume "xa = a <*> x"; 
   1.204      show "xa:V"; by (simp!);
   1.205    qed;
   1.206  
   1.207 -  show "ALL x1 : lin x. ALL x2 : lin x. x1 [+] x2 : lin x"; 
   1.208 +  show "ALL x1 : lin x. ALL x2 : lin x. x1 + x2 : lin x"; 
   1.209    proof (intro ballI);
   1.210      fix x1 x2; assume "x1 : lin x" "x2 : lin x"; 
   1.211 -    thus "x1 [+] x2 : lin x";
   1.212 +    thus "x1 + x2 : lin x";
   1.213      proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
   1.214 -      fix a1 a2; assume "x1 = a1 [*] x" "x2 = a2 [*] x";
   1.215 -      show "x1 [+] x2 = (a1 + a2) [*] x"; 
   1.216 +      fix a1 a2; assume "x1 = a1 <*> x" "x2 = a2 <*> x";
   1.217 +      show "x1 + x2 = (a1 + a2) <*> x"; 
   1.218          by (simp! add: vs_add_mult_distrib2);
   1.219      qed;
   1.220    qed;
   1.221  
   1.222 -  show "ALL xa:lin x. ALL a. a [*] xa : lin x"; 
   1.223 +  show "ALL xa:lin x. ALL a. a <*> xa : lin x"; 
   1.224    proof (intro ballI allI);
   1.225      fix x1 a; assume "x1 : lin x"; 
   1.226 -    thus "a [*] x1 : lin x";
   1.227 +    thus "a <*> x1 : lin x";
   1.228      proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
   1.229 -      fix a1; assume "x1 = a1 [*] x";
   1.230 -      show "a [*] x1 = (a * a1) [*] x"; by (simp!);
   1.231 +      fix a1; assume "x1 = a1 <*> x";
   1.232 +      show "a <*> x1 = (a * a1) <*> x"; by (simp!);
   1.233      qed;
   1.234    qed; 
   1.235  qed;
   1.236  
   1.237 +text {* Any linear closure is a vector space. *};
   1.238 +
   1.239  lemma lin_vs [intro!!]: 
   1.240    "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)";
   1.241  proof (rule subspace_vs);
   1.242 @@ -165,139 +207,166 @@
   1.243  
   1.244  subsection {* Sum of two vectorspaces *};
   1.245  
   1.246 +text {* The \emph{sum} of two vectorspaces $U$ and $V$ is the set of
   1.247 +all sums of elements from $U$ and $V$. *};
   1.248  
   1.249 +instance set :: (plus) plus; by intro_classes;
   1.250 +
   1.251 +defs vs_sum_def:
   1.252 +  "U + V == {x. EX u:U. EX v:V. x = u + v}";
   1.253 +
   1.254 +(***
   1.255  constdefs 
   1.256 -  vectorspace_sum :: "['a set, 'a set] => 'a set"
   1.257 -  "vectorspace_sum U V == {x. ? u:U. ? v:V. x = u [+] v}";
   1.258 +  vs_sum :: 
   1.259 +  "['a::{minus, plus} set, 'a set] => 'a set"         (infixl "+" 65)
   1.260 +  "vs_sum U V == {x. EX u:U. EX v:V. x = u + v}";
   1.261 +***)
   1.262  
   1.263 -lemma vs_sumD: "x:vectorspace_sum U V = (? u:U. ? v:V. x = u [+] v)";
   1.264 -  by (unfold vectorspace_sum_def) simp;
   1.265 +lemma vs_sumD: 
   1.266 +  "x: U + V = (EX u:U. EX v:V. x = u + v)";
   1.267 +  by (unfold vs_sum_def) simp;
   1.268  
   1.269  lemmas vs_sumE = vs_sumD [RS iffD1, elimify];
   1.270  
   1.271  lemma vs_sumI [intro!!]: 
   1.272 -  "[| x: U; y:V; (t::'a) = x [+] y |] 
   1.273 -  ==> (t::'a) : vectorspace_sum U V";
   1.274 -  by (unfold vectorspace_sum_def, intro CollectI bexI); 
   1.275 +  "[| x:U; y:V; t= x + y |] ==> t : U + V";
   1.276 +  by (unfold vs_sum_def, intro CollectI bexI); 
   1.277 +
   1.278 +text{* $U$ is a subspace of $U + V$. *};
   1.279  
   1.280  lemma subspace_vs_sum1 [intro!!]: 
   1.281 -  "[| is_vectorspace U; is_vectorspace V |] 
   1.282 -  ==> is_subspace U (vectorspace_sum U V)";
   1.283 +  "[| is_vectorspace U; is_vectorspace V |]
   1.284 +  ==> is_subspace U (U + V)";
   1.285  proof; 
   1.286    assume "is_vectorspace U" "is_vectorspace V";
   1.287    show "<0> : U"; ..;
   1.288 -  show "U <= vectorspace_sum U V";
   1.289 +  show "U <= U + V";
   1.290    proof (intro subsetI vs_sumI);
   1.291    fix x; assume "x:U";
   1.292 -    show "x = x [+] <0>"; by (simp!);
   1.293 +    show "x = x + <0>"; by (simp!);
   1.294      show "<0> : V"; by (simp!);
   1.295    qed;
   1.296 -  show "ALL x:U. ALL y:U. x [+] y : U"; 
   1.297 +  show "ALL x:U. ALL y:U. x + y : U"; 
   1.298    proof (intro ballI);
   1.299 -    fix x y; assume "x:U" "y:U"; show "x [+] y : U"; by (simp!);
   1.300 +    fix x y; assume "x:U" "y:U"; show "x + y : U"; by (simp!);
   1.301    qed;
   1.302 -  show "ALL x:U. ALL a. a [*] x : U"; 
   1.303 +  show "ALL x:U. ALL a. a <*> x : U"; 
   1.304    proof (intro ballI allI);
   1.305 -    fix x a; assume "x:U"; show "a [*] x : U"; by (simp!);
   1.306 +    fix x a; assume "x:U"; show "a <*> x : U"; by (simp!);
   1.307    qed;
   1.308  qed;
   1.309  
   1.310 +text{* The sum of two subspaces is again a subspace.*};
   1.311 +
   1.312  lemma vs_sum_subspace [intro!!]: 
   1.313    "[| is_subspace U E; is_subspace V E; is_vectorspace E |] 
   1.314 -  ==> is_subspace (vectorspace_sum U V) E";
   1.315 +  ==> is_subspace (U + V) E";
   1.316  proof; 
   1.317 -  assume "is_subspace U E" "is_subspace V E" and e: "is_vectorspace E";
   1.318 -  show "<0> : vectorspace_sum U V";
   1.319 +  assume "is_subspace U E" "is_subspace V E" "is_vectorspace E";
   1.320 +  show "<0> : U + V";
   1.321    proof (intro vs_sumI);
   1.322      show "<0> : U"; ..;
   1.323      show "<0> : V"; ..;
   1.324 -    show "(<0>::'a) = <0> [+] <0>"; by (simp!);
   1.325 +    show "(<0>::'a) = <0> + <0>"; by (simp!);
   1.326    qed;
   1.327    
   1.328 -  show "vectorspace_sum U V <= E";
   1.329 +  show "U + V <= E";
   1.330    proof (intro subsetI, elim vs_sumE bexE);
   1.331 -    fix x u v; assume "u : U" "v : V" "x = u [+] v";
   1.332 +    fix x u v; assume "u : U" "v : V" "x = u + v";
   1.333      show "x:E"; by (simp!);
   1.334    qed;
   1.335    
   1.336 -  show "ALL x:vectorspace_sum U V. ALL y:vectorspace_sum U V. 
   1.337 -        x [+] y : vectorspace_sum U V";
   1.338 +  show "ALL x: U + V. ALL y: U + V. x + y : U + V";
   1.339    proof (intro ballI);
   1.340 -    fix x y; assume "x:vectorspace_sum U V" "y:vectorspace_sum U V";
   1.341 -    thus "x [+] y : vectorspace_sum U V";
   1.342 +    fix x y; assume "x : U + V" "y : U + V";
   1.343 +    thus "x + y : U + V";
   1.344      proof (elim vs_sumE bexE, intro vs_sumI);
   1.345        fix ux vx uy vy; 
   1.346 -      assume "ux : U" "vx : V" "x = ux [+] vx" "uy : U" "vy : V" 
   1.347 -             "y = uy [+] vy";
   1.348 -      show "x [+] y = (ux [+] uy) [+] (vx [+] vy)"; by (simp!);
   1.349 +      assume "ux : U" "vx : V" "x = ux + vx" 
   1.350 +	and "uy : U" "vy : V" "y = uy + vy";
   1.351 +      show "x + y = (ux + uy) + (vx + vy)"; by (simp!);
   1.352      qed (simp!)+;
   1.353    qed;
   1.354  
   1.355 -  show "ALL x:vectorspace_sum U V. ALL a. 
   1.356 -        a [*] x : vectorspace_sum U V";
   1.357 +  show "ALL x: U + V. ALL a. a <*> x : U + V";
   1.358    proof (intro ballI allI);
   1.359 -    fix x a; assume "x:vectorspace_sum U V";
   1.360 -    thus "a [*] x : vectorspace_sum U V";
   1.361 +    fix x a; assume "x : U + V";
   1.362 +    thus "a <*> x : U + V";
   1.363      proof (elim vs_sumE bexE, intro vs_sumI);
   1.364 -      fix a x u v; assume "u : U" "v : V" "x = u [+] v";
   1.365 -      show "a [*] x = (a [*] u) [+] (a [*] v)"; 
   1.366 +      fix a x u v; assume "u : U" "v : V" "x = u + v";
   1.367 +      show "a <*> x = (a <*> u) + (a <*> v)"; 
   1.368          by (simp! add: vs_add_mult_distrib1);
   1.369      qed (simp!)+;
   1.370    qed;
   1.371  qed;
   1.372  
   1.373 +text{* The sum of two subspaces is a vectorspace. *};
   1.374 +
   1.375  lemma vs_sum_vs [intro!!]: 
   1.376    "[| is_subspace U E; is_subspace V E; is_vectorspace E |] 
   1.377 -  ==> is_vectorspace (vectorspace_sum U V)";
   1.378 +  ==> is_vectorspace (U + V)";
   1.379  proof (rule subspace_vs);
   1.380    assume "is_subspace U E" "is_subspace V E" "is_vectorspace E";
   1.381 -  show "is_subspace (vectorspace_sum U V) E"; ..;
   1.382 +  show "is_subspace (U + V) E"; ..;
   1.383  qed;
   1.384  
   1.385  
   1.386  
   1.387 -subsection {* A special case *}
   1.388 +subsection {* Direct sums *};
   1.389  
   1.390  
   1.391 -text {* direct sum of a vectorspace and a linear closure of a vector 
   1.392 -*};
   1.393 +text {* The sum of $U$ and $V$ is called \emph{direct}, iff the zero 
   1.394 +element is the only common element of $U$ and $V$. For every element
   1.395 +$x$ of the direct sum of $U$ and $V$ the decomposition in
   1.396 +$x = u + v$ with $u:U$ and $v:V$ is unique.*}; 
   1.397  
   1.398 -lemma decomp: "[| is_vectorspace E; is_subspace U E; is_subspace V E; 
   1.399 -  U Int V = {<0>}; u1:U; u2:U; v1:V; v2:V; u1 [+] v1 = u2 [+] v2 |] 
   1.400 +lemma decomp: 
   1.401 +  "[| is_vectorspace E; is_subspace U E; is_subspace V E; 
   1.402 +  U Int V = {<0>}; u1:U; u2:U; v1:V; v2:V; u1 + v1 = u2 + v2 |] 
   1.403    ==> u1 = u2 & v1 = v2"; 
   1.404  proof; 
   1.405    assume "is_vectorspace E" "is_subspace U E" "is_subspace V E"  
   1.406      "U Int V = {<0>}" "u1:U" "u2:U" "v1:V" "v2:V" 
   1.407 -    "u1 [+] v1 = u2 [+] v2"; 
   1.408 -  have eq: "u1 [-] u2 = v2 [-] v1"; by (simp! add: vs_add_diff_swap);
   1.409 -  have u: "u1 [-] u2 : U"; by (simp!); 
   1.410 -  with eq; have v': "v2 [-] v1 : U"; by simp; 
   1.411 -  have v: "v2 [-] v1 : V"; by (simp!); 
   1.412 -  with eq; have u': "u1 [-] u2 : V"; by simp;
   1.413 +    "u1 + v1 = u2 + v2"; 
   1.414 +  have eq: "u1 - u2 = v2 - v1"; by (simp! add: vs_add_diff_swap);
   1.415 +  have u: "u1 - u2 : U"; by (simp!); 
   1.416 +  with eq; have v': "v2 - v1 : U"; by simp; 
   1.417 +  have v: "v2 - v1 : V"; by (simp!); 
   1.418 +  with eq; have u': "u1 - u2 : V"; by simp;
   1.419    
   1.420    show "u1 = u2";
   1.421    proof (rule vs_add_minus_eq);
   1.422 -    show "u1 [-] u2 = <0>"; by (rule Int_singletonD [OF _ u u']); 
   1.423 -  qed (rule);
   1.424 +    show "u1 - u2 = <0>"; by (rule Int_singletonD [OF _ u u']); 
   1.425 +    show "u1 : E"; ..;
   1.426 +    show "u2 : E"; ..;
   1.427 +  qed;
   1.428  
   1.429    show "v1 = v2";
   1.430    proof (rule vs_add_minus_eq [RS sym]);
   1.431 -    show "v2 [-] v1 = <0>"; by (rule Int_singletonD [OF _ v' v]); 
   1.432 -  qed (rule);
   1.433 +    show "v2 - v1 = <0>"; by (rule Int_singletonD [OF _ v' v]);
   1.434 +    show "v1 : E"; ..;
   1.435 +    show "v2 : E"; ..;
   1.436 +  qed;
   1.437  qed;
   1.438  
   1.439 -lemma decomp4: "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; 
   1.440 -  x0 ~: H; x0 :E; x0 ~= <0>; y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0 |]
   1.441 +text {* An application of the previous lemma will be used in the 
   1.442 +proof of the Hahn-Banach theorem: for an element $y + a \mult x_0$ 
   1.443 +of the direct sum of a vectorspace $H$ and the linear closure of 
   1.444 +$x_0$ the components $y:H$ and $a$ are unique. *}; 
   1.445 +
   1.446 +lemma decomp_H0: 
   1.447 +  "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; 
   1.448 +  x0 ~: H; x0 : E; x0 ~= <0>; y1 + a1 <*> x0 = y2 + a2 <*> x0 |]
   1.449    ==> y1 = y2 & a1 = a2";
   1.450  proof;
   1.451    assume "is_vectorspace E" and h: "is_subspace H E"
   1.452       and "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= <0>" 
   1.453 -         "y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0";
   1.454 +         "y1 + a1 <*> x0 = y2 + a2 <*> x0";
   1.455  
   1.456 -  have c: "y1 = y2 & a1 [*] x0 = a2 [*] x0";
   1.457 +  have c: "y1 = y2 & a1 <*> x0 = a2 <*> x0";
   1.458    proof (rule decomp); 
   1.459 -    show "a1 [*] x0 : lin x0"; ..; 
   1.460 -    show "a2 [*] x0 : lin x0"; ..;
   1.461 +    show "a1 <*> x0 : lin x0"; ..; 
   1.462 +    show "a2 <*> x0 : lin x0"; ..;
   1.463      show "H Int (lin x0) = {<0>}"; 
   1.464      proof;
   1.465        show "H Int lin x0 <= {<0>}"; 
   1.466 @@ -305,15 +374,15 @@
   1.467          fix x; assume "x:H" "x:lin x0"; 
   1.468          thus "x = <0>";
   1.469          proof (unfold lin_def, elim CollectE exE);
   1.470 -          fix a; assume "x = a [*] x0";
   1.471 +          fix a; assume "x = a <*> x0";
   1.472            show ?thesis;
   1.473 -          proof (rule case_split [of "a = 0r"]);
   1.474 +          proof (rule case_split);
   1.475              assume "a = 0r"; show ?thesis; by (simp!);
   1.476            next;
   1.477              assume "a ~= 0r"; 
   1.478 -            from h; have "(rinv a) [*] a [*] x0 : H"; 
   1.479 +            from h; have "rinv a <*> a <*> x0 : H"; 
   1.480                by (rule subspace_mult_closed) (simp!);
   1.481 -            also; have "(rinv a) [*] a [*] x0 = x0"; by (simp!);
   1.482 +            also; have "rinv a <*> a <*> x0 = x0"; by (simp!);
   1.483              finally; have "x0 : H"; .;
   1.484              thus ?thesis; by contradiction;
   1.485            qed;
   1.486 @@ -332,58 +401,68 @@
   1.487    
   1.488    show  "a1 = a2"; 
   1.489    proof (rule vs_mult_right_cancel [RS iffD1]);
   1.490 -    from c; show "a1 [*] x0 = a2 [*] x0"; by simp; 
   1.491 +    from c; show "a1 <*> x0 = a2 <*> x0"; by simp;
   1.492    qed;
   1.493  qed;
   1.494  
   1.495 -lemma decomp1: 
   1.496 -  "[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E; x0 ~= <0> |]
   1.497 -  ==> (@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)";
   1.498 +text {* Since for an element $y + a \mult x_0$ of the direct sum 
   1.499 +of a vectorspace $H$ and the linear closure of $x_0$ the components
   1.500 +$y\in H$ and $a$ are unique, follows from $y\in H$ the fact that 
   1.501 +$a = 0$.*}; 
   1.502 +
   1.503 +lemma decomp_H0_H: 
   1.504 +  "[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E;
   1.505 +  x0 ~= <0> |] 
   1.506 +  ==> (SOME (y, a). t = y + a <*> x0 & y : H) = (t, 0r)";
   1.507  proof (rule, unfold split_paired_all);
   1.508 -  assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E" 
   1.509 +  assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E"
   1.510      "x0 ~= <0>";
   1.511    have h: "is_vectorspace H"; ..;
   1.512 -  fix y a; presume t1: "t = y [+] a [*] x0" and "y : H";
   1.513 +  fix y a; presume t1: "t = y + a <*> x0" and "y : H";
   1.514    have "y = t & a = 0r"; 
   1.515 -    by (rule decomp4) (assumption | (simp!))+; 
   1.516 +    by (rule decomp_H0) (assumption | (simp!))+;
   1.517    thus "(y, a) = (t, 0r)"; by (simp!);
   1.518  qed (simp!)+;
   1.519  
   1.520 -lemma decomp3:
   1.521 -  "[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
   1.522 +text {* The components $y\in H$ and $a$ in $y \plus a \mult x_0$ 
   1.523 +are unique, so the function $h_0$ defined by 
   1.524 +$h_0 (y \plus a \mult x_0) = h y + a * xi$ is definite. *};
   1.525 +
   1.526 +lemma h0_definite:
   1.527 +  "[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
   1.528                  in (h y) + a * xi);
   1.529 -  x = y [+] a [*] x0; is_vectorspace E; is_subspace H E;    
   1.530 +  x = y + a <*> x0; is_vectorspace E; is_subspace H E;
   1.531    y:H; x0 ~: H; x0:E; x0 ~= <0> |]
   1.532    ==> h0 x = h y + a * xi";
   1.533  proof -;  
   1.534 -  assume "h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
   1.535 -                    in (h y) + a * xi)"
   1.536 -         "x = y [+] a [*] x0" "is_vectorspace E" "is_subspace H E" 
   1.537 -         "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
   1.538 -  have "x : vectorspace_sum H (lin x0)"; 
   1.539 -    by (simp! add: vectorspace_sum_def lin_def, intro bexI exI conjI) 
   1.540 -       force+;
   1.541 -  have "EX! xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)"; 
   1.542 -  proof%%;
   1.543 -    show "EX xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)";
   1.544 +  assume 
   1.545 +    "h0 = (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
   1.546 +               in (h y) + a * xi)"
   1.547 +    "x = y + a <*> x0" "is_vectorspace E" "is_subspace H E"
   1.548 +    "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
   1.549 +  have "x : H + (lin x0)"; 
   1.550 +    by (simp! add: vs_sum_def lin_def) force+;
   1.551 +  have "EX! xa. ((\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)"; 
   1.552 +  proof;
   1.553 +    show "EX xa. ((%(y, a). x = y + a <*> x0 & y:H) xa)";
   1.554        by (force!);
   1.555    next;
   1.556      fix xa ya;
   1.557 -    assume "(%(y,a). x = y [+] a [*] x0 & y : H) xa"
   1.558 -           "(%(y,a). x = y [+] a [*] x0 & y : H) ya";
   1.559 +    assume "(%(y,a). x = y + a <*> x0 & y : H) xa"
   1.560 +           "(%(y,a). x = y + a <*> x0 & y : H) ya";
   1.561      show "xa = ya"; ;
   1.562      proof -;
   1.563        show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; 
   1.564          by (rule Pair_fst_snd_eq [RS iffD2]);
   1.565 -      have x: "x = (fst xa) [+] (snd xa) [*] x0 & (fst xa) : H"; 
   1.566 +      have x: "x = (fst xa) + (snd xa) <*> x0 & (fst xa) : H"; 
   1.567          by (force!);
   1.568 -      have y: "x = (fst ya) [+] (snd ya) [*] x0 & (fst ya) : H"; 
   1.569 +      have y: "x = (fst ya) + (snd ya) <*> x0 & (fst ya) : H"; 
   1.570          by (force!);
   1.571        from x y; show "fst xa = fst ya & snd xa = snd ya"; 
   1.572 -        by (elim conjE) (rule decomp4, (simp!)+);
   1.573 +        by (elim conjE) (rule decomp_H0, (simp!)+);
   1.574      qed;
   1.575    qed;
   1.576 -  hence eq: "(@ (y, a). (x = y [+] a [*] x0 & y:H)) = (y, a)"; 
   1.577 +  hence eq: "(SOME (y, a). (x = y + a <*> x0 & y:H)) = (y, a)"; 
   1.578      by (rule select1_equality) (force!);
   1.579    thus "h0 x = h y + a * xi"; by (simp! add: Let_def);
   1.580  qed;