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);
2 theory Subspace = LinearSpace:;
5 section {* subspaces *};
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)";
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;
18 lemma "is_subspace U V ==> U ~= {}";
19   by (unfold is_subspace_def) force;
21 lemma zero_in_subspace: "is_subspace U V ==> <0>:U";
22   by (unfold is_subspace_def) force;
24 lemma subspace_subset: "is_subspace U V ==> U <= V";
25   by (unfold is_subspace_def) fast;
27 lemma subspace_subset2 [simp]: "[| is_subspace U V; x:U |]==> x:V";
28   by (unfold is_subspace_def) fast;
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;
33 lemma subspace_mult_closed [simp]: "[| is_subspace U V; x: U |] ==> a [*] x: U";
34   by (unfold is_subspace_def) asm_simp;
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;
39 lemma subspace_neg_closed [simp]: "[| is_subspace U V; x: U |] ==> [-] x: U";
40  by (unfold negate_def) asm_simp;
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;
54 next;
55   assume "is_subspace U V";
56   show "U <= V"; by (rule subspace_subset);
57 qed;
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;
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;
85 section {* linear closure *};
87 constdefs
88   lin :: "'a => 'a set"
89   "lin x == {y. ? a. y = a [*] x}";
91 lemma linD: "x : lin v = (? a::real. x = a [*] v)";
92   by (unfold lin_def) fast;
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;
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;
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;
136 section {* sum of two vectorspaces *};
138 constdefs
139   vectorspace_sum :: "['a set, 'a set] => 'a set"
140   "vectorspace_sum U V == {x. ? u:U. ? v:V. x = u [+] v}";
142 lemma vs_sumD: "x:vectorspace_sum U V = (? u:U. ? v:V. x = u [+] v)";
143   by (unfold vectorspace_sum_def) fast;
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);
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;
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";
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);
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;
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+;
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;
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]);
202 section {* special case: direct sum of a vectorspace and a linear closure of a vector *};
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";
215   also; have "... = (a2 - a1) [*] x0";
216     by (rule vs_diff_mult_distrib2 [RS sym]);
217   finally; have eq: "y1 [-] y2 = (a2 - a1) [*] x0"; .;
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);
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"; .;
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;
249   from h; show "y1 = y2";
251     show "y1 [-] y2 = <0>";
252       by (rule Int_singeltonD [OF int y y']);
253   qed;
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;
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+;
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>";
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";