src/HOL/Real/HahnBanach/Subspace.thy
author wenzelm
Wed Sep 29 16:41:52 1999 +0200 (1999-09-29)
changeset 7656 2f18c0ffc348
parent 7567 62384a807775
child 7808 fd019ac3485f
permissions -rw-r--r--
update from Gertrud;
     1 (*  Title:      HOL/Real/HahnBanach/Subspace.thy
     2     ID:         $Id$
     3     Author:     Gertrud Bauer, TU Munich
     4 *)
     5 
     6 theory Subspace = LinearSpace:;
     7 
     8 
     9 section {* subspaces *};
    10 
    11 constdefs
    12   is_subspace ::  "['a set, 'a set] => bool"
    13   "is_subspace U V ==  <0>:U  & U <= V 
    14      &  (ALL x:U. ALL y:U. ALL a. x [+] y : U                          
    15                        & a [*] x : U)";                            
    16 
    17 lemma subspaceI [intro]: 
    18   "[| <0>:U; U <= V; ALL x:U. ALL y:U. (x [+] y : U); ALL x:U. ALL a. a [*] x : U |]
    19   \ ==> is_subspace U V";
    20   by (unfold is_subspace_def) simp;
    21 
    22 lemma "is_subspace U V ==> U ~= {}";
    23   by (unfold is_subspace_def) force;
    24 
    25 lemma zero_in_subspace [intro !!]: "is_subspace U V ==> <0>:U";
    26   by (unfold is_subspace_def) simp;;
    27 
    28 lemma subspace_subset [intro !!]: "is_subspace U V ==> U <= V";
    29   by (unfold is_subspace_def) simp;
    30 
    31 lemma subspace_subsetD [simp, intro!!]: "[| is_subspace U V; x:U |]==> x:V";
    32   by (unfold is_subspace_def) force;
    33 
    34 lemma subspace_add_closed [simp, intro!!]: "[| is_subspace U V; x: U; y: U |] ==> x [+] y: U";
    35   by (unfold is_subspace_def) simp;
    36 
    37 lemma subspace_mult_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> a [*] x: U";
    38   by (unfold is_subspace_def) simp;
    39 
    40 lemma subspace_diff_closed [simp, intro!!]: "[| is_subspace U V; x: U; y: U |] ==> x [-] y: U";
    41   by (unfold diff_def negate_def) simp;
    42 
    43 lemma subspace_neg_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> [-] x: U";
    44  by (unfold negate_def) simp;
    45 
    46 
    47 theorem subspace_vs [intro!!]:
    48   "[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U";
    49 proof -;
    50   assume "is_subspace U V" "is_vectorspace V";
    51   show ?thesis;
    52   proof; 
    53     show "<0>:U"; ..;
    54     show "ALL x:U. ALL a. a [*] x : U"; by (simp!);
    55     show "ALL x:U. ALL y:U. x [+] y : U"; by (simp!);
    56   qed (simp! add: vs_add_mult_distrib1 vs_add_mult_distrib2)+;
    57 qed;
    58 
    59 lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V";
    60 proof; 
    61   assume "is_vectorspace V";
    62   show "<0> : V"; ..;
    63   show "V <= V"; ..;
    64   show "ALL x:V. ALL y:V. x [+] y : V"; by (simp!);
    65   show "ALL x:V. ALL a. a [*] x : V"; by (simp!);
    66 qed;
    67 
    68 lemma subspace_trans: "[| is_subspace U V; is_subspace V W |] ==> is_subspace U W";
    69 proof; 
    70   assume "is_subspace U V" "is_subspace V W";
    71   show "<0> : U"; ..;
    72 
    73   have "U <= V"; ..;
    74   also; have "V <= W"; ..;
    75   finally; show "U <= W"; .;
    76 
    77   show "ALL x:U. ALL y:U. x [+] y : U"; 
    78   proof (intro ballI);
    79     fix x y; assume "x:U" "y:U";
    80     show "x [+] y : U"; by (simp!);
    81   qed;
    82 
    83   show "ALL x:U. ALL a. a [*] x : U";
    84   proof (intro ballI allI);
    85     fix x a; assume "x:U";
    86     show "a [*] x : U"; by (simp!);
    87   qed;
    88 qed;
    89 
    90 
    91 section {* linear closure *};
    92 
    93 constdefs
    94   lin :: "'a => 'a set"
    95   "lin x == {y. ? a. y = a [*] x}";
    96 
    97 lemma linD: "x : lin v = (? a::real. x = a [*] v)";
    98   by (unfold lin_def) force;
    99 
   100 lemma linI [intro!!]: "a [*] x0 : lin x0";
   101   by (unfold lin_def) force;
   102 
   103 lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x:lin x";
   104 proof (unfold lin_def, intro CollectI exI);
   105   assume "is_vectorspace V" "x:V";
   106   show "x = 1r [*] x"; by (simp!);
   107 qed;
   108 
   109 lemma lin_subspace [intro!!]: "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V";
   110 proof;
   111   assume "is_vectorspace V" "x:V";
   112   show "<0> : lin x"; 
   113   proof (unfold lin_def, intro CollectI exI);
   114     show "<0> = 0r [*] x"; by (simp!);
   115   qed;
   116 
   117   show "lin x <= V";
   118   proof (unfold lin_def, intro subsetI, elim CollectE exE); 
   119     fix xa a; assume "xa = a [*] x"; 
   120     show "xa:V"; by (simp!);
   121   qed;
   122 
   123   show "ALL x1 : lin x. ALL x2 : lin x. x1 [+] x2 : lin x"; 
   124   proof (intro ballI);
   125     fix x1 x2; assume "x1 : lin x" "x2 : lin x"; 
   126     thus "x1 [+] x2 : lin x";
   127     proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
   128       fix a1 a2; assume "x1 = a1 [*] x" "x2 = a2 [*] x";
   129       show "x1 [+] x2 = (a1 + a2) [*] x"; by (simp! add: vs_add_mult_distrib2);
   130     qed;
   131   qed;
   132 
   133   show "ALL xa:lin x. ALL a. a [*] xa : lin x"; 
   134   proof (intro ballI allI);
   135     fix x1 a; assume "x1 : lin x"; 
   136     thus "a [*] x1 : lin x";
   137     proof (unfold lin_def, elim CollectE exE, intro CollectI exI);
   138       fix a1; assume "x1 = a1 [*] x";
   139       show "a [*] x1 = (a * a1) [*] x"; by (simp!);
   140     qed;
   141   qed; 
   142 qed;
   143 
   144 
   145 lemma lin_vs [intro!!]: "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)";
   146 proof (rule subspace_vs);
   147   assume "is_vectorspace V" "x:V";
   148   show "is_subspace (lin x) V"; ..;
   149 qed;
   150 
   151 section {* sum of two vectorspaces *};
   152 
   153 constdefs 
   154   vectorspace_sum :: "['a set, 'a set] => 'a set"
   155   "vectorspace_sum U V == {x. ? u:U. ? v:V. x = u [+] v}";
   156 
   157 lemma vs_sumD: "x:vectorspace_sum U V = (? u:U. ? v:V. x = u [+] v)";
   158   by (unfold vectorspace_sum_def) simp;
   159 
   160 lemmas vs_sumE = vs_sumD [RS iffD1, elimify];
   161 
   162 lemma vs_sumI [intro!!]: "[| x: U; y:V; (t::'a) = x [+] y |] ==> (t::'a) : vectorspace_sum U V";
   163   by (unfold vectorspace_sum_def, intro CollectI bexI); 
   164 
   165 lemma subspace_vs_sum1 [intro!!]: 
   166   "[| is_vectorspace U; is_vectorspace V |] ==> is_subspace U (vectorspace_sum U V)";
   167 proof; 
   168   assume "is_vectorspace U" "is_vectorspace V";
   169   show "<0> : U"; ..;
   170   show "U <= vectorspace_sum U V";
   171   proof (intro subsetI vs_sumI);
   172   fix x; assume "x:U";
   173     show "x = x [+] <0>"; by (simp!);
   174     show "<0> : V"; by (simp!);
   175   qed;
   176   show "ALL x:U. ALL y:U. x [+] y : U"; 
   177   proof (intro ballI);
   178     fix x y; assume "x:U" "y:U"; show "x [+] y : U"; by (simp!);
   179   qed;
   180   show "ALL x:U. ALL a. a [*] x : U"; 
   181   proof (intro ballI allI);
   182     fix x a; assume "x:U"; show "a [*] x : U"; by (simp!);
   183   qed;
   184 qed;
   185 
   186 lemma vs_sum_subspace [intro!!]: 
   187   "[| is_subspace U E; is_subspace V E; is_vectorspace E |] 
   188   ==> is_subspace (vectorspace_sum U V) E";
   189 proof; 
   190   assume "is_subspace U E" "is_subspace V E" and e: "is_vectorspace E";
   191 
   192   show "<0> : vectorspace_sum U V";
   193   proof (intro vs_sumI);
   194     show "<0> : U"; ..;
   195     show "<0> : V"; ..;
   196     show "(<0>::'a) = <0> [+] <0>"; by (simp!);
   197   qed;
   198   
   199   show "vectorspace_sum U V <= E";
   200   proof (intro subsetI, elim vs_sumE bexE);
   201     fix x u v; assume "u : U" "v : V" "x = u [+] v";
   202     show "x:E"; by (simp!);
   203   qed;
   204   
   205   show "ALL x:vectorspace_sum U V. ALL y:vectorspace_sum U V. x [+] y : vectorspace_sum U V";
   206   proof (intro ballI);
   207     fix x y; assume "x:vectorspace_sum U V" "y:vectorspace_sum U V";
   208     thus "x [+] y : vectorspace_sum U V";
   209     proof (elim vs_sumE bexE, intro vs_sumI);
   210       fix ux vx uy vy; 
   211       assume "ux : U" "vx : V" "x = ux [+] vx" "uy : U" "vy : V" "y = uy [+] vy";
   212       show "x [+] y = (ux [+] uy) [+] (vx [+] vy)"; by (simp!);
   213     qed (simp!)+;
   214   qed;
   215 
   216   show "ALL x:vectorspace_sum U V. ALL a. a [*] x : vectorspace_sum U V";
   217   proof (intro ballI allI);
   218     fix x a; assume "x:vectorspace_sum U V";
   219     thus "a [*] x : vectorspace_sum U V";
   220     proof (elim vs_sumE bexE, intro vs_sumI);
   221       fix a x u v; assume "u : U" "v : V" "x = u [+] v";
   222       show "a [*] x = (a [*] u) [+] (a [*] v)"; by (simp! add: vs_add_mult_distrib1);
   223     qed (simp!)+;
   224   qed;
   225 qed;
   226 
   227 lemma vs_sum_vs [intro!!]: 
   228   "[| is_subspace U E; is_subspace V E; is_vectorspace E |] 
   229   ==> is_vectorspace (vectorspace_sum U V)";
   230 proof (rule subspace_vs);
   231   assume "is_subspace U E" "is_subspace V E" "is_vectorspace E";
   232   show "is_subspace (vectorspace_sum U V) E"; ..;
   233 qed;
   234 
   235 
   236 section {* special case: direct sum of a vectorspace and a linear closure of a vector *};
   237 
   238 lemma decomp: "[| is_vectorspace E; is_subspace U E; is_subspace V E; U Int V = {<0>}; 
   239   u1:U; u2:U; v1:V; v2:V; u1 [+] v1 = u2 [+] v2 |] 
   240   ==> u1 = u2 & v1 = v2"; 
   241 proof; 
   242   assume "is_vectorspace E" "is_subspace U E" "is_subspace V E"  "U Int V = {<0>}" 
   243          "u1:U" "u2:U" "v1:V" "v2:V" "u1 [+] v1 = u2 [+] v2"; 
   244   have eq: "u1 [-] u2 = v2 [-] v1"; by (simp! add: vs_add_diff_swap);
   245   have u: "u1 [-] u2 : U"; by (simp!); with eq; have v': "v2 [-] v1 : U"; by simp; 
   246   have v: "v2 [-] v1 : V"; by (simp!); with eq; have u': "u1 [-] u2 : V"; by simp;
   247   
   248   show "u1 = u2";
   249   proof (rule vs_add_minus_eq);
   250     show "u1 [-] u2 = <0>"; by (rule Int_singletonD [OF _ u u']); 
   251   qed (rule);
   252 
   253   show "v1 = v2";
   254   proof (rule vs_add_minus_eq [RS sym]);
   255     show "v2 [-] v1 = <0>"; by (rule Int_singletonD [OF _ v' v]); 
   256   qed (rule);
   257 qed;
   258 
   259 lemma decomp4: "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; x0 ~: H; x0 :E; 
   260   x0 ~= <0>; y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0 |]
   261   ==> y1 = y2 & a1 = a2";
   262 proof;
   263   assume "is_vectorspace E" and h: "is_subspace H E"
   264      and "y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= <0>" 
   265          "y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0";
   266 
   267   have c: "y1 = y2 & a1 [*] x0 = a2 [*] x0";
   268   proof (rule decomp); 
   269     show "a1 [*] x0 : lin x0"; ..; 
   270     show "a2 [*] x0 : lin x0"; ..;
   271     show "H Int (lin x0) = {<0>}"; 
   272     proof;
   273       show "H Int lin x0 <= {<0>}"; 
   274       proof (intro subsetI, elim IntE, rule singleton_iff[RS iffD2]);
   275         fix x; assume "x:H" "x:lin x0"; 
   276         thus "x = <0>";
   277         proof (unfold lin_def, elim CollectE exE);
   278           fix a; assume "x = a [*] x0";
   279           show ?thesis;
   280           proof (rule case_split [of "a = 0r"]);
   281             assume "a = 0r"; show ?thesis; by (simp!);
   282           next;
   283             assume "a ~= 0r"; 
   284             from h; have "(rinv a) [*] a [*] x0 : H"; by (rule subspace_mult_closed) (simp!);
   285             also; have "(rinv a) [*] a [*] x0 = x0"; by (simp!);
   286             finally; have "x0 : H"; .;
   287             thus ?thesis; by contradiction;
   288           qed;
   289        qed;
   290       qed;
   291       show "{<0>} <= H Int lin x0";
   292       proof (intro subsetI, elim singletonE, intro IntI, simp+);
   293         show "<0> : H"; ..;
   294         from lin_vs; show "<0> : lin x0"; ..;
   295       qed;
   296     qed;
   297     show "is_subspace (lin x0) E"; ..;
   298   qed;
   299   
   300   from c; show "y1 = y2"; by simp;
   301   
   302   show  "a1 = a2"; 
   303   proof (rule vs_mult_right_cancel [RS iffD1]);
   304     from c; show "a1 [*] x0 = a2 [*] x0"; by simp; 
   305   qed;
   306 qed;
   307 
   308 lemma decomp1: 
   309   "[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E; x0 ~= <0> |] 
   310   ==> (@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)";
   311 proof (rule, unfold split_paired_all);
   312   assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E" "x0 ~= <0>";
   313   have h: "is_vectorspace H"; ..;
   314   fix y a; presume t1: "t = y [+] a [*] x0" and "y : H";
   315   have "y = t & a = 0r"; 
   316     by (rule decomp4) (assumption | (simp!))+; 
   317   thus "(y, a) = (t, 0r)"; by (simp!);
   318 qed (simp!)+;
   319 
   320 lemma decomp3:
   321   "[| h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
   322                 in (h y) + a * xi);
   323       x = y [+] a [*] x0; 
   324       is_vectorspace E; is_subspace H E; y:H; x0 ~: H; x0:E; x0 ~= <0> |]
   325   ==> h0 x = h y + a * xi";
   326 proof -;  
   327   assume "h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) 
   328                     in (h y) + a * xi)"
   329          "x = y [+] a [*] x0"
   330          "is_vectorspace E" "is_subspace H E" "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>";
   331 
   332   have "x : vectorspace_sum H (lin x0)"; 
   333     by (simp! add: vectorspace_sum_def lin_def, intro bexI exI conjI) force+;
   334   have "EX! xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)"; 
   335   proof%%;
   336     show "EX xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)";
   337       by (force!);
   338   next;
   339     fix xa ya;
   340     assume "(%(y,a). x = y [+] a [*] x0 & y : H) xa"
   341            "(%(y,a). x = y [+] a [*] x0 & y : H) ya";
   342     show "xa = ya"; ;
   343     proof -;
   344       show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; 
   345         by (rule Pair_fst_snd_eq [RS iffD2]);
   346       have x: "x = (fst xa) [+] (snd xa) [*] x0 & (fst xa) : H"; by (force!);
   347       have y: "x = (fst ya) [+] (snd ya) [*] x0 & (fst ya) : H"; by (force!);
   348       from x y; show "fst xa = fst ya & snd xa = snd ya"; by (elim conjE) (rule decomp4, (simp!)+);
   349     qed;
   350   qed;
   351   hence eq: "(@ (y, a). (x = y [+] a [*] x0 & y:H)) = (y, a)"; by (rule select1_equality) (force!);
   352   thus "h0 x = h y + a * xi"; by (simp! add: Let_def);
   353 qed;
   354 
   355 end;
   356 
   357