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