src/HOL/Real/HahnBanach/Subspace.thy
author wenzelm
Mon Oct 25 19:24:43 1999 +0200 (1999-10-25)
changeset 7927 b50446a33c16
parent 7917 5e5b9813cce7
child 7978 1b99ee57d131
permissions -rw-r--r--
update by Gertrud Bauer;
     1 (*  Title:      HOL/Real/HahnBanach/Subspace.thy
     2     ID:         $Id$
     3     Author:     Gertrud Bauer, TU Munich
     4 *)
     5 
     6 
     7 header {* Subspaces *};
     8 
     9 theory Subspace = VectorSpace:;
    10 
    11 
    12 subsection {* Definition *};
    13 
    14 text {* A non-empty subset $U$ of a vector space $V$ is a 
    15 \emph{subspace} of $V$, iff $U$ is closed under addition and 
    16 scalar multiplication. *};
    17 
    18 constdefs 
    19   is_subspace ::  "['a::{minus, plus} set, 'a set] => bool"
    20   "is_subspace U V ==  U ~= {}  & U <= V 
    21      &  (ALL x:U. ALL y:U. ALL a. x + y : U & a <*> x : U)";
    22 
    23 lemma subspaceI [intro]: 
    24   "[| <0>:U; U <= V; ALL x:U. ALL y:U. (x + y : U); 
    25   ALL x:U. ALL a. a <*> x : U |]
    26   ==> is_subspace U V";
    27 proof (unfold is_subspace_def, intro conjI); 
    28   assume "<0>:U"; thus "U ~= {}"; by fast;
    29 qed (simp+);
    30 
    31 lemma subspace_not_empty [intro!!]: "is_subspace U V ==> U ~= {}";
    32   by (unfold is_subspace_def) simp; 
    33 
    34 lemma subspace_subset [intro !!]: "is_subspace U V ==> U <= V";
    35   by (unfold is_subspace_def) simp;
    36 
    37 lemma subspace_subsetD [simp, intro!!]: 
    38   "[| is_subspace U V; x:U |]==> x:V";
    39   by (unfold is_subspace_def) force;
    40 
    41 lemma subspace_add_closed [simp, intro!!]: 
    42   "[| is_subspace U V; x: U; y: U |] ==> x + y : U";
    43   by (unfold is_subspace_def) simp;
    44 
    45 lemma subspace_mult_closed [simp, intro!!]: 
    46   "[| is_subspace U V; x: U |] ==> a <*> x: U";
    47   by (unfold is_subspace_def) simp;
    48 
    49 lemma subspace_diff_closed [simp, intro!!]: 
    50   "[| is_subspace U V; is_vectorspace V; x: U; y: U |] 
    51   ==> x - y: U";
    52   by (simp! add: diff_eq1 negate_eq1);
    53 
    54 text {* Similar as for linear spaces, the existence of the 
    55 zero element in every subspace follws from the non-emptyness 
    56 of the subspace and vector space laws.*};
    57 
    58 lemma zero_in_subspace [intro !!]:
    59   "[| is_subspace U V; is_vectorspace V |] ==> <0>:U";
    60 proof -; 
    61   assume "is_subspace U V" and v: "is_vectorspace V";
    62   have "U ~= {}"; ..;
    63   hence "EX x. x:U"; by force;
    64   thus ?thesis; 
    65   proof; 
    66     fix x; assume u: "x:U"; 
    67     hence "x:V"; by (simp!);
    68     with v; have "<0> = x - x"; by (simp!);
    69     also; have "... : U"; by (rule subspace_diff_closed);
    70     finally; show ?thesis; .;
    71   qed;
    72 qed;
    73 
    74 lemma subspace_neg_closed [simp, intro!!]: 
    75   "[| is_subspace U V; is_vectorspace V; x: U |] ==> - x: U";
    76   by (simp add: negate_eq1);
    77 
    78 text_raw {* \medskip *};
    79 text {* Further derived laws: Every subspace is a vector space. *};
    80 
    81 lemma subspace_vs [intro!!]:
    82   "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U";
    83 proof -;
    84   assume "is_subspace U V" "is_vectorspace V";
    85   show ?thesis;
    86   proof; 
    87     show "<0>:U"; ..;
    88     show "ALL x:U. ALL a. a <*> x : U"; by (simp!);
    89     show "ALL x:U. ALL y:U. x + y : U"; by (simp!);
    90     show "ALL x:U. - x = -1r <*> x"; by (simp! add: negate_eq1);
    91     show "ALL x:U. ALL y:U. x - y =  x + - y"; 
    92       by (simp! add: diff_eq1);
    93   qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+;
    94 qed;
    95 
    96 text {* The subspace relation is reflexive. *};
    97 
    98 lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V";
    99 proof; 
   100   assume "is_vectorspace V";
   101   show "<0> : V"; ..;
   102   show "V <= V"; ..;
   103   show "ALL x:V. ALL y:V. x + y : V"; by (simp!);
   104   show "ALL x:V. ALL a. a <*> x : V"; by (simp!);
   105 qed;
   106 
   107 text {* The subspace relation is transitive. *};
   108 
   109 lemma subspace_trans: 
   110   "[| is_subspace U V; is_vectorspace V; is_subspace V W |] 
   111   ==> is_subspace U W";
   112 proof; 
   113   assume "is_subspace U V" "is_subspace V W" "is_vectorspace V";
   114   show "<0> : U"; ..;
   115 
   116   have "U <= V"; ..;
   117   also; have "V <= W"; ..;
   118   finally; show "U <= W"; .;
   119 
   120   show "ALL x:U. ALL y:U. x + y : U"; 
   121   proof (intro ballI);
   122     fix x y; assume "x:U" "y:U";
   123     show "x + y : U"; by (simp!);
   124   qed;
   125 
   126   show "ALL x:U. ALL a. a <*> x : U";
   127   proof (intro ballI allI);
   128     fix x a; assume "x:U";
   129     show "a <*> x : U"; by (simp!);
   130   qed;
   131 qed;
   132 
   133 
   134 
   135 subsection {* Linear closure *};
   136 
   137 text {* The \emph{linear closure} of a vector $x$ is the set of all 
   138 multiples of $x$. *};
   139 
   140 constdefs
   141   lin :: "'a => 'a set"
   142   "lin x == {y. EX a. y = a <*> x}";
   143 
   144 lemma linD: "x : lin v = (EX a::real. x = a <*> v)";
   145   by (unfold lin_def) force;
   146 
   147 lemma linI [intro!!]: "a <*> x0 : lin x0";
   148   by (unfold lin_def) force;
   149 
   150 text {* Every vector is contained in its linear closure. *};
   151 
   152 lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x:lin x";
   153 proof (unfold lin_def, intro CollectI exI);
   154   assume "is_vectorspace V" "x:V";
   155   show "x = 1r <*> x"; by (simp!);
   156 qed;
   157 
   158 text {* Any linear closure is a subspace. *};
   159 
   160 lemma lin_subspace [intro!!]: 
   161   "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V";
   162 proof;
   163   assume "is_vectorspace V" "x:V";
   164   show "<0> : lin x"; 
   165   proof (unfold lin_def, intro CollectI exI);
   166     show "<0> = 0r <*> x"; by (simp!);
   167   qed;
   168 
   169   show "lin x <= V";
   170   proof (unfold lin_def, intro subsetI, elim CollectE exE); 
   171     fix xa a; assume "xa = a <*> x"; 
   172     show "xa:V"; by (simp!);
   173   qed;
   174 
   175   show "ALL x1 : lin x. ALL x2 : lin x. x1 + x2 : lin x"; 
   176   proof (intro ballI);
   177     fix x1 x2; assume "x1 : lin x" "x2 : lin x"; 
   178     thus "x1 + x2 : lin x";
   179     proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
   180       fix a1 a2; assume "x1 = a1 <*> x" "x2 = a2 <*> x";
   181       show "x1 + x2 = (a1 + a2) <*> x"; 
   182         by (simp! add: vs_add_mult_distrib2);
   183     qed;
   184   qed;
   185 
   186   show "ALL xa:lin x. ALL a. a <*> xa : lin x"; 
   187   proof (intro ballI allI);
   188     fix x1 a; assume "x1 : lin x"; 
   189     thus "a <*> x1 : lin x";
   190     proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
   191       fix a1; assume "x1 = a1 <*> x";
   192       show "a <*> x1 = (a * a1) <*> x"; by (simp!);
   193     qed;
   194   qed; 
   195 qed;
   196 
   197 text {* Any linear closure is a vector space. *};
   198 
   199 lemma lin_vs [intro!!]: 
   200   "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)";
   201 proof (rule subspace_vs);
   202   assume "is_vectorspace V" "x:V";
   203   show "is_subspace (lin x) V"; ..;
   204 qed;
   205 
   206 
   207 
   208 subsection {* Sum of two vectorspaces *};
   209 
   210 text {* The \emph{sum} of two vectorspaces $U$ and $V$ is the set of
   211 all sums of elements from $U$ and $V$. *};
   212 
   213 instance set :: (plus) plus; by intro_classes;
   214 
   215 defs vs_sum_def:
   216   "U + V == {x. EX u:U. EX v:V. x = u + v}";(***  
   217 
   218 constdefs 
   219   vs_sum :: 
   220   "['a::{minus, plus} set, 'a set] => 'a set"         (infixl "+" 65)
   221   "vs_sum U V == {x. EX u:U. EX v:V. x = u + v}";
   222 ***)
   223 
   224 lemma vs_sumD: 
   225   "x: U + V = (EX u:U. EX v:V. x = u + v)";
   226   by (unfold vs_sum_def) simp;
   227 
   228 lemmas vs_sumE = vs_sumD [RS iffD1, elimify];
   229 
   230 lemma vs_sumI [intro!!]: 
   231   "[| x:U; y:V; t= x + y |] ==> t : U + V";
   232   by (unfold vs_sum_def, intro CollectI bexI); 
   233 
   234 text{* $U$ is a subspace of $U + V$. *};
   235 
   236 lemma subspace_vs_sum1 [intro!!]: 
   237   "[| is_vectorspace U; is_vectorspace V |]
   238   ==> is_subspace U (U + V)";
   239 proof; 
   240   assume "is_vectorspace U" "is_vectorspace V";
   241   show "<0> : U"; ..;
   242   show "U <= U + V";
   243   proof (intro subsetI vs_sumI);
   244   fix x; assume "x:U";
   245     show "x = x + <0>"; by (simp!);
   246     show "<0> : V"; by (simp!);
   247   qed;
   248   show "ALL x:U. ALL y:U. x + y : U"; 
   249   proof (intro ballI);
   250     fix x y; assume "x:U" "y:U"; show "x + y : U"; by (simp!);
   251   qed;
   252   show "ALL x:U. ALL a. a <*> x : U"; 
   253   proof (intro ballI allI);
   254     fix x a; assume "x:U"; show "a <*> x : U"; by (simp!);
   255   qed;
   256 qed;
   257 
   258 text{* The sum of two subspaces is again a subspace.*};
   259 
   260 lemma vs_sum_subspace [intro!!]: 
   261   "[| is_subspace U E; is_subspace V E; is_vectorspace E |] 
   262   ==> is_subspace (U + V) E";
   263 proof; 
   264   assume "is_subspace U E" "is_subspace V E" "is_vectorspace E";
   265   show "<0> : U + V";
   266   proof (intro vs_sumI);
   267     show "<0> : U"; ..;
   268     show "<0> : V"; ..;
   269     show "(<0>::'a) = <0> + <0>"; by (simp!);
   270   qed;
   271   
   272   show "U + V <= E";
   273   proof (intro subsetI, elim vs_sumE bexE);
   274     fix x u v; assume "u : U" "v : V" "x = u + v";
   275     show "x:E"; by (simp!);
   276   qed;
   277   
   278   show "ALL x: U + V. ALL y: U + V. x + y : U + V";
   279   proof (intro ballI);
   280     fix x y; assume "x : U + V" "y : U + V";
   281     thus "x + y : U + V";
   282     proof (elim vs_sumE bexE, intro vs_sumI);
   283       fix ux vx uy vy; 
   284       assume "ux : U" "vx : V" "x = ux + vx" 
   285 	and "uy : U" "vy : V" "y = uy + vy";
   286       show "x + y = (ux + uy) + (vx + vy)"; by (simp!);
   287     qed (simp!)+;
   288   qed;
   289 
   290   show "ALL x: U + V. ALL a. a <*> x : U + V";
   291   proof (intro ballI allI);
   292     fix x a; assume "x : U + V";
   293     thus "a <*> x : U + V";
   294     proof (elim vs_sumE bexE, intro vs_sumI);
   295       fix a x u v; assume "u : U" "v : V" "x = u + v";
   296       show "a <*> x = (a <*> u) + (a <*> v)"; 
   297         by (simp! add: vs_add_mult_distrib1);
   298     qed (simp!)+;
   299   qed;
   300 qed;
   301 
   302 text{* The sum of two subspaces is a vectorspace. *};
   303 
   304 lemma vs_sum_vs [intro!!]: 
   305   "[| is_subspace U E; is_subspace V E; is_vectorspace E |] 
   306   ==> is_vectorspace (U + V)";
   307 proof (rule subspace_vs);
   308   assume "is_subspace U E" "is_subspace V E" "is_vectorspace E";
   309   show "is_subspace (U + V) E"; ..;
   310 qed;
   311 
   312 
   313 
   314 subsection {* Direct sums *};
   315 
   316 
   317 text {* The sum of $U$ and $V$ is called \emph{direct}, iff the zero 
   318 element is the only common element of $U$ and $V$. For every element
   319 $x$ of the direct sum of $U$ and $V$ the decomposition in
   320 $x = u + v$ with $u \in U$ and $v \in V$ is unique.*}; 
   321 
   322 lemma decomp: 
   323   "[| is_vectorspace E; is_subspace U E; is_subspace V E; 
   324   U Int V = {<0>}; u1:U; u2:U; v1:V; v2:V; u1 + v1 = u2 + v2 |] 
   325   ==> u1 = u2 & v1 = v2"; 
   326 proof; 
   327   assume "is_vectorspace E" "is_subspace U E" "is_subspace V E"  
   328     "U Int V = {<0>}" "u1:U" "u2:U" "v1:V" "v2:V" 
   329     "u1 + v1 = u2 + v2"; 
   330   have eq: "u1 - u2 = v2 - v1"; by (simp! add: vs_add_diff_swap);
   331   have u: "u1 - u2 : U"; by (simp!); 
   332   with eq; have v': "v2 - v1 : U"; by simp; 
   333   have v: "v2 - v1 : V"; by (simp!); 
   334   with eq; have u': "u1 - u2 : V"; by simp;
   335   
   336   show "u1 = u2";
   337   proof (rule vs_add_minus_eq);
   338     show "u1 - u2 = <0>"; by (rule Int_singletonD [OF _ u u']); 
   339     show "u1 : E"; ..;
   340     show "u2 : E"; ..;
   341   qed;
   342 
   343   show "v1 = v2";
   344   proof (rule vs_add_minus_eq [RS sym]);
   345     show "v2 - v1 = <0>"; by (rule Int_singletonD [OF _ v' v]);
   346     show "v1 : E"; ..;
   347     show "v2 : E"; ..;
   348   qed;
   349 qed;
   350 
   351 text {* An application of the previous lemma will be used in the 
   352 proof of the Hahn-Banach theorem: for an element $y + a \mult x_0$ 
   353 of the direct sum of a vectorspace $H$ and the linear closure of 
   354 $x_0$ the components $y \in H$ and $a$ are unique. *}; 
   355 
   356 lemma decomp_H0: 
   357   "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; 
   358   x0 ~: H; x0 : E; x0 ~= <0>; y1 + a1 <*> x0 = y2 + a2 <*> x0 |]
   359   ==> y1 = y2 & a1 = a2";
   360 proof;
   361   assume "is_vectorspace E" and h: "is_subspace H E"
   362      and "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= <0>" 
   363          "y1 + a1 <*> x0 = y2 + a2 <*> x0";
   364 
   365   have c: "y1 = y2 & a1 <*> x0 = a2 <*> x0";
   366   proof (rule decomp); 
   367     show "a1 <*> x0 : lin x0"; ..; 
   368     show "a2 <*> x0 : lin x0"; ..;
   369     show "H Int (lin x0) = {<0>}"; 
   370     proof;
   371       show "H Int lin x0 <= {<0>}"; 
   372       proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]);
   373         fix x; assume "x:H" "x:lin x0"; 
   374         thus "x = <0>";
   375         proof (unfold lin_def, elim CollectE exE);
   376           fix a; assume "x = a <*> x0";
   377           show ?thesis;
   378           proof (rule case_split);
   379             assume "a = 0r"; show ?thesis; by (simp!);
   380           next;
   381             assume "a ~= 0r"; 
   382             from h; have "rinv a <*> a <*> x0 : H"; 
   383               by (rule subspace_mult_closed) (simp!);
   384             also; have "rinv a <*> a <*> x0 = x0"; by (simp!);
   385             finally; have "x0 : H"; .;
   386             thus ?thesis; by contradiction;
   387           qed;
   388        qed;
   389       qed;
   390       show "{<0>} <= H Int lin x0";
   391       proof (intro subsetI, elim singletonE, intro IntI, simp+);
   392         show "<0> : H"; ..;
   393         from lin_vs; show "<0> : lin x0"; ..;
   394       qed;
   395     qed;
   396     show "is_subspace (lin x0) E"; ..;
   397   qed;
   398   
   399   from c; show "y1 = y2"; by simp;
   400   
   401   show  "a1 = a2"; 
   402   proof (rule vs_mult_right_cancel [RS iffD1]);
   403     from c; show "a1 <*> x0 = a2 <*> x0"; by simp;
   404   qed;
   405 qed;
   406 
   407 text {* Since for an element $y + a \mult x_0$ of the direct sum 
   408 of a vectorspace $H$ and the linear closure of $x_0$ the components
   409 $y\in H$ and $a$ are unique, follows from $y\in H$ the fact that 
   410 $a = 0$.*}; 
   411 
   412 lemma decomp_H0_H: 
   413   "[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E;
   414   x0 ~= <0> |] 
   415   ==> (SOME (y, a). t = y + a <*> x0 & y : H) = (t, 0r)";
   416 proof (rule, unfold split_paired_all);
   417   assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E"
   418     "x0 ~= <0>";
   419   have h: "is_vectorspace H"; ..;
   420   fix y a; presume t1: "t = y + a <*> x0" and "y : H";
   421   have "y = t & a = 0r"; 
   422     by (rule decomp_H0) (assumption | (simp!))+;
   423   thus "(y, a) = (t, 0r)"; by (simp!);
   424 qed (simp!)+;
   425 
   426 text {* The components $y\in H$ and $a$ in $y \plus a \mult x_0$ 
   427 are unique, so the function $h_0$ defined by 
   428 $h_0 (y \plus a \mult x_0) = h y + a \cdot \xi$ is definite. *};
   429 
   430 lemma h0_definite:
   431   "[| h0 = (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
   432                 in (h y) + a * xi);
   433   x = y + a <*> x0; is_vectorspace E; is_subspace H E;
   434   y:H; x0 ~: H; x0:E; x0 ~= <0> |]
   435   ==> h0 x = h y + a * xi";
   436 proof -;  
   437   assume 
   438     "h0 = (\<lambda>x. let (y, a) = SOME (y, a). (x = y + a <*> x0 & y:H)
   439                in (h y) + a * xi)"
   440     "x = y + a <*> x0" "is_vectorspace E" "is_subspace H E"
   441     "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
   442   have "x : H + (lin x0)"; 
   443     by (simp! add: vs_sum_def lin_def) force+;
   444   have "EX! xa. ((\<lambda>(y, a). x = y + a <*> x0 & y:H) xa)"; 
   445   proof;
   446     show "EX xa. ((%(y, a). x = y + a <*> x0 & y:H) xa)";
   447       by (force!);
   448   next;
   449     fix xa ya;
   450     assume "(%(y,a). x = y + a <*> x0 & y : H) xa"
   451            "(%(y,a). x = y + a <*> x0 & y : H) ya";
   452     show "xa = ya"; ;
   453     proof -;
   454       show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; 
   455         by (rule Pair_fst_snd_eq [RS iffD2]);
   456       have x: "x = (fst xa) + (snd xa) <*> x0 & (fst xa) : H"; 
   457         by (force!);
   458       have y: "x = (fst ya) + (snd ya) <*> x0 & (fst ya) : H"; 
   459         by (force!);
   460       from x y; show "fst xa = fst ya & snd xa = snd ya"; 
   461         by (elim conjE) (rule decomp_H0, (simp!)+);
   462     qed;
   463   qed;
   464   hence eq: "(SOME (y, a). (x = y + a <*> x0 & y:H)) = (y, a)"; 
   465     by (rule select1_equality) (force!);
   466   thus "h0 x = h y + a * xi"; by (simp! add: Let_def);
   467 qed;
   468 
   469 end;