author | wenzelm |
Tue, 21 Sep 1999 17:31:20 +0200 | |
changeset 7566 | c5a3f980a7af |
parent 7535 | 599d3414b51d |
child 7567 | 62384a807775 |
permissions | -rw-r--r-- |
7566 | 1 |
(* Title: HOL/Real/HahnBanach/Subspace.thy |
2 |
ID: $Id$ |
|
3 |
Author: Gertrud Bauer, TU Munich |
|
4 |
*) |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
5 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
6 |
theory Subspace = LinearSpace:; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
7 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
8 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
9 |
section {* subspaces *}; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
10 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
11 |
constdefs |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
12 |
is_subspace :: "['a set, 'a set] => bool" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
13 |
"is_subspace U V == <0>:U & U <= V |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
14 |
& (ALL x:U. ALL y:U. ALL a. x [+] y : U |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
15 |
& a [*] x : U)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
16 |
|
7566 | 17 |
lemma subspaceI [intro]: |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
18 |
"[| <0>:U; U <= V; ALL x:U. ALL y:U. (x [+] y : U); ALL x:U. ALL a. a [*] x : U |] |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
19 |
\ ==> is_subspace U V"; |
7566 | 20 |
by (unfold is_subspace_def) (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
21 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
22 |
lemma "is_subspace U V ==> U ~= {}"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
23 |
by (unfold is_subspace_def) force; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
24 |
|
7566 | 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"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
32 |
by (unfold is_subspace_def) force; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
33 |
|
7566 | 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!); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
36 |
|
7566 | 37 |
lemma subspace_mult_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> a [*] x: U"; |
38 |
by (unfold is_subspace_def) (simp!); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
39 |
|
7566 | 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!); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
42 |
|
7566 | 43 |
lemma subspace_neg_closed [simp, intro!!]: "[| is_subspace U V; x: U |] ==> [-] x: U"; |
44 |
by (unfold negate_def) (simp!); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
45 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
46 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
47 |
theorem subspace_vs [intro!!]: |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
48 |
"[| is_subspace U V; is_vectorspace V |] ==> is_vectorspace U"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
49 |
proof -; |
7566 | 50 |
assume "is_subspace U V"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
51 |
assume "is_vectorspace V"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
52 |
assume "is_subspace U V"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
53 |
show ?thesis; |
7566 | 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)+; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
59 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
60 |
|
7566 | 61 |
lemma subspace_refl [intro]: "is_vectorspace V ==> is_subspace V V"; |
62 |
proof; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
63 |
assume "is_vectorspace V"; |
7566 | 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!); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
68 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
69 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
70 |
lemma subspace_trans: "[| is_subspace U V; is_subspace V W |] ==> is_subspace U W"; |
7566 | 71 |
proof; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
72 |
assume "is_subspace U V" "is_subspace V W"; |
7566 | 73 |
show "<0> : U"; ..; |
74 |
have "U <= V"; ..; |
|
75 |
also; have "V <= W"; ..; |
|
76 |
finally; show "U <= W"; .; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
77 |
show "ALL x:U. ALL y:U. x [+] y : U"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
78 |
proof (intro ballI); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
79 |
fix x y; assume "x:U" "y:U"; |
7566 | 80 |
show "x [+] y : U"; by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
81 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
82 |
show "ALL x:U. ALL a. a [*] x : U"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
83 |
proof (intro ballI allI); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
84 |
fix x a; assume "x:U"; |
7566 | 85 |
show "a [*] x : U"; by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
86 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
87 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
88 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
89 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
90 |
section {* linear closure *}; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
91 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
92 |
constdefs |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
93 |
lin :: "'a => 'a set" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
94 |
"lin x == {y. ? a. y = a [*] x}"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
95 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
96 |
lemma linD: "x : lin v = (? a::real. x = a [*] v)"; |
7566 | 97 |
by (unfold lin_def) force; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
98 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
99 |
lemma x_lin_x: "[| is_vectorspace V; x:V |] ==> x:lin x"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
100 |
proof (unfold lin_def, intro CollectI exI); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
101 |
assume "is_vectorspace V" "x:V"; |
7566 | 102 |
show "x = 1r [*] x"; by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
103 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
104 |
|
7566 | 105 |
lemma lin_subspace [intro!!]: "[| is_vectorspace V; x:V |] ==> is_subspace (lin x) V"; |
106 |
proof; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
107 |
assume "is_vectorspace V" "x:V"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
108 |
show "<0> : lin x"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
109 |
proof (unfold lin_def, intro CollectI exI); |
7566 | 110 |
show "<0> = 0r [*] x"; by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
111 |
qed; |
7566 | 112 |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
113 |
show "lin x <= V"; |
7566 | 114 |
proof (unfold lin_def, intro subsetI, elim CollectE exE); |
115 |
fix xa a; assume "xa = a [*] x"; |
|
116 |
show "xa:V"; by (simp!); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
117 |
qed; |
7566 | 118 |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
119 |
show "ALL x1 : lin x. ALL x2 : lin x. x1 [+] x2 : lin x"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
120 |
proof (intro ballI); |
7566 | 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 !? *) |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
124 |
fix a1 a2; assume "x1 = a1 [*] x" "x2 = a2 [*] x"; |
7566 | 125 |
show "x1 [+] x2 = (a1 + a2) [*] x"; by (simp! add: vs_add_mult_distrib2); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
126 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
127 |
qed; |
7566 | 128 |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
129 |
show "ALL xa:lin x. ALL a. a [*] xa : lin x"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
130 |
proof (intro ballI allI); |
7566 | 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); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
134 |
fix a1; assume "x1 = a1 [*] x"; |
7566 | 135 |
show "a [*] x1 = (a * a1) [*] x"; by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
136 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
137 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
138 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
139 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
140 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
141 |
lemma lin_vs [intro!!]: "[| is_vectorspace V; x:V |] ==> is_vectorspace (lin x)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
142 |
proof (rule subspace_vs); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
143 |
assume "is_vectorspace V" "x:V"; |
7566 | 144 |
show "is_subspace (lin x) V"; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
145 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
146 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
147 |
section {* sum of two vectorspaces *}; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
148 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
149 |
constdefs |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
150 |
vectorspace_sum :: "['a set, 'a set] => 'a set" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
151 |
"vectorspace_sum U V == {x. ? u:U. ? v:V. x = u [+] v}"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
152 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
153 |
lemma vs_sumD: "x:vectorspace_sum U V = (? u:U. ? v:V. x = u [+] v)"; |
7566 | 154 |
by (unfold vectorspace_sum_def) (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
155 |
|
7566 | 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"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
159 |
by (unfold vectorspace_sum_def, intro CollectI bexI); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
160 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
161 |
lemma subspace_vs_sum1 [intro!!]: |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
162 |
"[| is_vectorspace U; is_vectorspace V |] ==> is_subspace U (vectorspace_sum U V)"; |
7566 | 163 |
proof; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
164 |
assume "is_vectorspace U" "is_vectorspace V"; |
7566 | 165 |
show "<0> : U"; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
166 |
show "U <= vectorspace_sum U V"; |
7566 | 167 |
proof (intro subsetI vs_sumI); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
168 |
fix x; assume "x:U"; |
7566 | 169 |
show "x = x [+] <0>"; by (simp!); |
170 |
show "<0> : V"; by (simp!); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
171 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
172 |
show "ALL x:U. ALL y:U. x [+] y : U"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
173 |
proof (intro ballI); |
7566 | 174 |
fix x y; assume "x:U" "y:U"; show "x [+] y : U"; by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
175 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
176 |
show "ALL x:U. ALL a. a [*] x : U"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
177 |
proof (intro ballI allI); |
7566 | 178 |
fix x a; assume "x:U"; show "a [*] x : U"; by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
179 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
180 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
181 |
|
7566 | 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"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
187 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
188 |
show "<0> : vectorspace_sum U V"; |
7566 | 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 |
||
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
196 |
show "vectorspace_sum U V <= E"; |
7566 | 197 |
proof (intro subsetI, elim vs_sumE bexE); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
198 |
fix x u v; assume "u : U" "v : V" "x = u [+] v"; |
7566 | 199 |
show "x:E"; by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
200 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
201 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
202 |
show "ALL x:vectorspace_sum U V. ALL y:vectorspace_sum U V. x [+] y : vectorspace_sum U V"; |
7566 | 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; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
212 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
213 |
show "ALL x:vectorspace_sum U V. ALL a. a [*] x : vectorspace_sum U V"; |
7566 | 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; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
222 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
223 |
|
7566 | 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; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
231 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
232 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
233 |
section {* special case: direct sum of a vectorspace and a linear closure of a vector *}; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
234 |
|
7566 | 235 |
lemma decomp4: "[| is_vectorspace E; is_subspace H E; y1 : H; y2 : H; x0 ~: H; x0 :E; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
236 |
x0 ~= <0>; y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0 |] |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
237 |
==> y1 = y2 & a1 = a2"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
238 |
proof; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
239 |
assume "is_vectorspace E" "is_subspace H E" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
240 |
"y1 : H" "y2 : H" "x0 ~: H" "x0 : E" "x0 ~= <0>" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
241 |
"y1 [+] a1 [*] x0 = y2 [+] a2 [*] x0"; |
7566 | 242 |
have h: "is_vectorspace H"; ..; |
243 |
have "y1 [-] y2 = a2 [*] x0 [-] a1 [*] x0"; |
|
244 |
by (simp! add: vs_add_diff_swap); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
245 |
also; have "... = (a2 - a1) [*] x0"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
246 |
by (rule vs_diff_mult_distrib2 [RS sym]); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
247 |
finally; have eq: "y1 [-] y2 = (a2 - a1) [*] x0"; .; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
248 |
|
7566 | 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; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
253 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
254 |
have int: "H Int (lin x0) = {<0>}"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
255 |
proof; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
256 |
show "H Int lin x0 <= {<0>}"; |
7566 | 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; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
274 |
qed; |
7566 | 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"; ..; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
279 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
280 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
281 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
282 |
from h; show "y1 = y2"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
283 |
proof (rule vs_add_minus_eq); |
7566 | 284 |
show "y1 [-] y2 = <0>"; |
285 |
by (rule Int_singletonD [OF int y y']); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
286 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
287 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
288 |
show "a1 = a2"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
289 |
proof (rule real_add_minus_eq [RS sym]); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
290 |
show "a2 - a1 = 0r"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
291 |
proof (rule vs_mult_zero_uniq); |
7566 | 292 |
show "(a2 - a1) [*] x0 = <0>"; by (rule Int_singletonD [OF int x' x]); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
293 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
294 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
295 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
296 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
297 |
|
7566 | 298 |
lemma decomp1: |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
299 |
"[| is_vectorspace E; is_subspace H E; t:H; x0~:H; x0:E; x0 ~= <0> |] |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
300 |
==> (@ (y, a). t = y [+] a [*] x0 & y : H) = (t, 0r)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
301 |
proof (rule, unfold split_paired_all); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
302 |
assume "is_vectorspace E" "is_subspace H E" "t:H" "x0~:H" "x0:E" "x0 ~= <0>"; |
7566 | 303 |
have h: "is_vectorspace H"; ..; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
304 |
fix y a; presume t1: "t = y [+] a [*] x0" and "y : H"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
305 |
have "y = t & a = 0r"; |
7566 | 306 |
by (rule decomp4) (assumption+, (simp!)); |
307 |
thus "(y, a) = (t, 0r)"; by (simp!); |
|
308 |
qed (simp!)+; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
309 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
310 |
|
7566 | 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> |] |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
316 |
==> h0 x = h y + a * xi"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
317 |
proof -; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
318 |
assume "h0 = (%x. let (y, a) = @ (y, a). (x = y [+] a [*] x0 & y:H) |
7566 | 319 |
in (h y) + a * xi)"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
320 |
assume "x = y [+] a [*] x0"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
321 |
assume "is_vectorspace E" "is_subspace H E" "y:H" "x0 ~: H" "x0:E" "x0 ~= <0>"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
322 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
323 |
have "x : vectorspace_sum H (lin x0)"; |
7566 | 324 |
by (simp! add: vectorspace_sum_def lin_def, intro bexI exI conjI) force+; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
325 |
have "EX! xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
326 |
proof; |
7566 | 327 |
show "EX xa. ((%(y, a). x = y [+] a [*] x0 & y:H) xa)"; |
328 |
by (force!); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
329 |
next; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
330 |
fix xa ya; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
331 |
assume "(%(y,a). x = y [+] a [*] x0 & y : H) xa" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
332 |
"(%(y,a). x = y [+] a [*] x0 & y : H) ya"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
333 |
show "xa = ya"; ; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
334 |
proof -; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
335 |
show "fst xa = fst ya & snd xa = snd ya ==> xa = ya"; |
7566 | 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!); |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
339 |
from x y; show "fst xa = fst ya & snd xa = snd ya"; |
7566 | 340 |
by (elim conjE) (rule decomp4, (simp!)+); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
341 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
342 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
343 |
hence eq: "(@ (y, a). (x = y [+] a [*] x0 & y:H)) = (y, a)"; |
7566 | 344 |
by (rule select1_equality) (force!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
345 |
thus "h0 x = h y + a * xi"; |
7566 | 346 |
by (simp! add: Let_def); |
347 |
qed; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
348 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
349 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
350 |
end; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
351 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
352 |