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.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.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.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.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.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.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.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;