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