|
1 (* Title: HOL/Real/HahnBanach/VectorSpace.thy |
|
2 ID: $Id$ |
|
3 Author: Gertrud Bauer, TU Munich |
|
4 *) |
|
5 |
|
6 header {* Vector spaces *} |
|
7 |
|
8 theory VectorSpace |
|
9 imports Real Bounds Zorn |
|
10 begin |
|
11 |
|
12 subsection {* Signature *} |
|
13 |
|
14 text {* |
|
15 For the definition of real vector spaces a type @{typ 'a} of the |
|
16 sort @{text "{plus, minus, zero}"} is considered, on which a real |
|
17 scalar multiplication @{text \<cdot>} is declared. |
|
18 *} |
|
19 |
|
20 consts |
|
21 prod :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a" (infixr "'(*')" 70) |
|
22 |
|
23 notation (xsymbols) |
|
24 prod (infixr "\<cdot>" 70) |
|
25 notation (HTML output) |
|
26 prod (infixr "\<cdot>" 70) |
|
27 |
|
28 |
|
29 subsection {* Vector space laws *} |
|
30 |
|
31 text {* |
|
32 A \emph{vector space} is a non-empty set @{text V} of elements from |
|
33 @{typ 'a} with the following vector space laws: The set @{text V} is |
|
34 closed under addition and scalar multiplication, addition is |
|
35 associative and commutative; @{text "- x"} is the inverse of @{text |
|
36 x} w.~r.~t.~addition and @{text 0} is the neutral element of |
|
37 addition. Addition and multiplication are distributive; scalar |
|
38 multiplication is associative and the real number @{text "1"} is |
|
39 the neutral element of scalar multiplication. |
|
40 *} |
|
41 |
|
42 locale var_V = fixes V |
|
43 |
|
44 locale vectorspace = var_V + |
|
45 assumes non_empty [iff, intro?]: "V \<noteq> {}" |
|
46 and add_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y \<in> V" |
|
47 and mult_closed [iff]: "x \<in> V \<Longrightarrow> a \<cdot> x \<in> V" |
|
48 and add_assoc: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x + y) + z = x + (y + z)" |
|
49 and add_commute: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y = y + x" |
|
50 and diff_self [simp]: "x \<in> V \<Longrightarrow> x - x = 0" |
|
51 and add_zero_left [simp]: "x \<in> V \<Longrightarrow> 0 + x = x" |
|
52 and add_mult_distrib1: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y" |
|
53 and add_mult_distrib2: "x \<in> V \<Longrightarrow> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x" |
|
54 and mult_assoc: "x \<in> V \<Longrightarrow> (a * b) \<cdot> x = a \<cdot> (b \<cdot> x)" |
|
55 and mult_1 [simp]: "x \<in> V \<Longrightarrow> 1 \<cdot> x = x" |
|
56 and negate_eq1: "x \<in> V \<Longrightarrow> - x = (- 1) \<cdot> x" |
|
57 and diff_eq1: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y = x + - y" |
|
58 |
|
59 lemma (in vectorspace) negate_eq2: "x \<in> V \<Longrightarrow> (- 1) \<cdot> x = - x" |
|
60 by (rule negate_eq1 [symmetric]) |
|
61 |
|
62 lemma (in vectorspace) negate_eq2a: "x \<in> V \<Longrightarrow> -1 \<cdot> x = - x" |
|
63 by (simp add: negate_eq1) |
|
64 |
|
65 lemma (in vectorspace) diff_eq2: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + - y = x - y" |
|
66 by (rule diff_eq1 [symmetric]) |
|
67 |
|
68 lemma (in vectorspace) diff_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y \<in> V" |
|
69 by (simp add: diff_eq1 negate_eq1) |
|
70 |
|
71 lemma (in vectorspace) neg_closed [iff]: "x \<in> V \<Longrightarrow> - x \<in> V" |
|
72 by (simp add: negate_eq1) |
|
73 |
|
74 lemma (in vectorspace) add_left_commute: |
|
75 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)" |
|
76 proof - |
|
77 assume xyz: "x \<in> V" "y \<in> V" "z \<in> V" |
|
78 then have "x + (y + z) = (x + y) + z" |
|
79 by (simp only: add_assoc) |
|
80 also from xyz have "\<dots> = (y + x) + z" by (simp only: add_commute) |
|
81 also from xyz have "\<dots> = y + (x + z)" by (simp only: add_assoc) |
|
82 finally show ?thesis . |
|
83 qed |
|
84 |
|
85 theorems (in vectorspace) add_ac = |
|
86 add_assoc add_commute add_left_commute |
|
87 |
|
88 |
|
89 text {* The existence of the zero element of a vector space |
|
90 follows from the non-emptiness of carrier set. *} |
|
91 |
|
92 lemma (in vectorspace) zero [iff]: "0 \<in> V" |
|
93 proof - |
|
94 from non_empty obtain x where x: "x \<in> V" by blast |
|
95 then have "0 = x - x" by (rule diff_self [symmetric]) |
|
96 also from x x have "\<dots> \<in> V" by (rule diff_closed) |
|
97 finally show ?thesis . |
|
98 qed |
|
99 |
|
100 lemma (in vectorspace) add_zero_right [simp]: |
|
101 "x \<in> V \<Longrightarrow> x + 0 = x" |
|
102 proof - |
|
103 assume x: "x \<in> V" |
|
104 from this and zero have "x + 0 = 0 + x" by (rule add_commute) |
|
105 also from x have "\<dots> = x" by (rule add_zero_left) |
|
106 finally show ?thesis . |
|
107 qed |
|
108 |
|
109 lemma (in vectorspace) mult_assoc2: |
|
110 "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = (a * b) \<cdot> x" |
|
111 by (simp only: mult_assoc) |
|
112 |
|
113 lemma (in vectorspace) diff_mult_distrib1: |
|
114 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<cdot> (x - y) = a \<cdot> x - a \<cdot> y" |
|
115 by (simp add: diff_eq1 negate_eq1 add_mult_distrib1 mult_assoc2) |
|
116 |
|
117 lemma (in vectorspace) diff_mult_distrib2: |
|
118 "x \<in> V \<Longrightarrow> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)" |
|
119 proof - |
|
120 assume x: "x \<in> V" |
|
121 have " (a - b) \<cdot> x = (a + - b) \<cdot> x" |
|
122 by (simp add: real_diff_def) |
|
123 also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x" |
|
124 by (rule add_mult_distrib2) |
|
125 also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)" |
|
126 by (simp add: negate_eq1 mult_assoc2) |
|
127 also from x have "\<dots> = a \<cdot> x - (b \<cdot> x)" |
|
128 by (simp add: diff_eq1) |
|
129 finally show ?thesis . |
|
130 qed |
|
131 |
|
132 lemmas (in vectorspace) distrib = |
|
133 add_mult_distrib1 add_mult_distrib2 |
|
134 diff_mult_distrib1 diff_mult_distrib2 |
|
135 |
|
136 |
|
137 text {* \medskip Further derived laws: *} |
|
138 |
|
139 lemma (in vectorspace) mult_zero_left [simp]: |
|
140 "x \<in> V \<Longrightarrow> 0 \<cdot> x = 0" |
|
141 proof - |
|
142 assume x: "x \<in> V" |
|
143 have "0 \<cdot> x = (1 - 1) \<cdot> x" by simp |
|
144 also have "\<dots> = (1 + - 1) \<cdot> x" by simp |
|
145 also from x have "\<dots> = 1 \<cdot> x + (- 1) \<cdot> x" |
|
146 by (rule add_mult_distrib2) |
|
147 also from x have "\<dots> = x + (- 1) \<cdot> x" by simp |
|
148 also from x have "\<dots> = x + - x" by (simp add: negate_eq2a) |
|
149 also from x have "\<dots> = x - x" by (simp add: diff_eq2) |
|
150 also from x have "\<dots> = 0" by simp |
|
151 finally show ?thesis . |
|
152 qed |
|
153 |
|
154 lemma (in vectorspace) mult_zero_right [simp]: |
|
155 "a \<cdot> 0 = (0::'a)" |
|
156 proof - |
|
157 have "a \<cdot> 0 = a \<cdot> (0 - (0::'a))" by simp |
|
158 also have "\<dots> = a \<cdot> 0 - a \<cdot> 0" |
|
159 by (rule diff_mult_distrib1) simp_all |
|
160 also have "\<dots> = 0" by simp |
|
161 finally show ?thesis . |
|
162 qed |
|
163 |
|
164 lemma (in vectorspace) minus_mult_cancel [simp]: |
|
165 "x \<in> V \<Longrightarrow> (- a) \<cdot> - x = a \<cdot> x" |
|
166 by (simp add: negate_eq1 mult_assoc2) |
|
167 |
|
168 lemma (in vectorspace) add_minus_left_eq_diff: |
|
169 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + y = y - x" |
|
170 proof - |
|
171 assume xy: "x \<in> V" "y \<in> V" |
|
172 then have "- x + y = y + - x" by (simp add: add_commute) |
|
173 also from xy have "\<dots> = y - x" by (simp add: diff_eq1) |
|
174 finally show ?thesis . |
|
175 qed |
|
176 |
|
177 lemma (in vectorspace) add_minus [simp]: |
|
178 "x \<in> V \<Longrightarrow> x + - x = 0" |
|
179 by (simp add: diff_eq2) |
|
180 |
|
181 lemma (in vectorspace) add_minus_left [simp]: |
|
182 "x \<in> V \<Longrightarrow> - x + x = 0" |
|
183 by (simp add: diff_eq2 add_commute) |
|
184 |
|
185 lemma (in vectorspace) minus_minus [simp]: |
|
186 "x \<in> V \<Longrightarrow> - (- x) = x" |
|
187 by (simp add: negate_eq1 mult_assoc2) |
|
188 |
|
189 lemma (in vectorspace) minus_zero [simp]: |
|
190 "- (0::'a) = 0" |
|
191 by (simp add: negate_eq1) |
|
192 |
|
193 lemma (in vectorspace) minus_zero_iff [simp]: |
|
194 "x \<in> V \<Longrightarrow> (- x = 0) = (x = 0)" |
|
195 proof |
|
196 assume x: "x \<in> V" |
|
197 { |
|
198 from x have "x = - (- x)" by (simp add: minus_minus) |
|
199 also assume "- x = 0" |
|
200 also have "- \<dots> = 0" by (rule minus_zero) |
|
201 finally show "x = 0" . |
|
202 next |
|
203 assume "x = 0" |
|
204 then show "- x = 0" by simp |
|
205 } |
|
206 qed |
|
207 |
|
208 lemma (in vectorspace) add_minus_cancel [simp]: |
|
209 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + (- x + y) = y" |
|
210 by (simp add: add_assoc [symmetric] del: add_commute) |
|
211 |
|
212 lemma (in vectorspace) minus_add_cancel [simp]: |
|
213 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + (x + y) = y" |
|
214 by (simp add: add_assoc [symmetric] del: add_commute) |
|
215 |
|
216 lemma (in vectorspace) minus_add_distrib [simp]: |
|
217 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - (x + y) = - x + - y" |
|
218 by (simp add: negate_eq1 add_mult_distrib1) |
|
219 |
|
220 lemma (in vectorspace) diff_zero [simp]: |
|
221 "x \<in> V \<Longrightarrow> x - 0 = x" |
|
222 by (simp add: diff_eq1) |
|
223 |
|
224 lemma (in vectorspace) diff_zero_right [simp]: |
|
225 "x \<in> V \<Longrightarrow> 0 - x = - x" |
|
226 by (simp add: diff_eq1) |
|
227 |
|
228 lemma (in vectorspace) add_left_cancel: |
|
229 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x + y = x + z) = (y = z)" |
|
230 proof |
|
231 assume x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V" |
|
232 { |
|
233 from y have "y = 0 + y" by simp |
|
234 also from x y have "\<dots> = (- x + x) + y" by simp |
|
235 also from x y have "\<dots> = - x + (x + y)" |
|
236 by (simp add: add_assoc neg_closed) |
|
237 also assume "x + y = x + z" |
|
238 also from x z have "- x + (x + z) = - x + x + z" |
|
239 by (simp add: add_assoc [symmetric] neg_closed) |
|
240 also from x z have "\<dots> = z" by simp |
|
241 finally show "y = z" . |
|
242 next |
|
243 assume "y = z" |
|
244 then show "x + y = x + z" by (simp only:) |
|
245 } |
|
246 qed |
|
247 |
|
248 lemma (in vectorspace) add_right_cancel: |
|
249 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)" |
|
250 by (simp only: add_commute add_left_cancel) |
|
251 |
|
252 lemma (in vectorspace) add_assoc_cong: |
|
253 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x' \<in> V \<Longrightarrow> y' \<in> V \<Longrightarrow> z \<in> V |
|
254 \<Longrightarrow> x + y = x' + y' \<Longrightarrow> x + (y + z) = x' + (y' + z)" |
|
255 by (simp only: add_assoc [symmetric]) |
|
256 |
|
257 lemma (in vectorspace) mult_left_commute: |
|
258 "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = b \<cdot> a \<cdot> x" |
|
259 by (simp add: real_mult_commute mult_assoc2) |
|
260 |
|
261 lemma (in vectorspace) mult_zero_uniq: |
|
262 "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> a \<cdot> x = 0 \<Longrightarrow> a = 0" |
|
263 proof (rule classical) |
|
264 assume a: "a \<noteq> 0" |
|
265 assume x: "x \<in> V" "x \<noteq> 0" and ax: "a \<cdot> x = 0" |
|
266 from x a have "x = (inverse a * a) \<cdot> x" by simp |
|
267 also from `x \<in> V` have "\<dots> = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc) |
|
268 also from ax have "\<dots> = inverse a \<cdot> 0" by simp |
|
269 also have "\<dots> = 0" by simp |
|
270 finally have "x = 0" . |
|
271 with `x \<noteq> 0` show "a = 0" by contradiction |
|
272 qed |
|
273 |
|
274 lemma (in vectorspace) mult_left_cancel: |
|
275 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (a \<cdot> x = a \<cdot> y) = (x = y)" |
|
276 proof |
|
277 assume x: "x \<in> V" and y: "y \<in> V" and a: "a \<noteq> 0" |
|
278 from x have "x = 1 \<cdot> x" by simp |
|
279 also from a have "\<dots> = (inverse a * a) \<cdot> x" by simp |
|
280 also from x have "\<dots> = inverse a \<cdot> (a \<cdot> x)" |
|
281 by (simp only: mult_assoc) |
|
282 also assume "a \<cdot> x = a \<cdot> y" |
|
283 also from a y have "inverse a \<cdot> \<dots> = y" |
|
284 by (simp add: mult_assoc2) |
|
285 finally show "x = y" . |
|
286 next |
|
287 assume "x = y" |
|
288 then show "a \<cdot> x = a \<cdot> y" by (simp only:) |
|
289 qed |
|
290 |
|
291 lemma (in vectorspace) mult_right_cancel: |
|
292 "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> (a \<cdot> x = b \<cdot> x) = (a = b)" |
|
293 proof |
|
294 assume x: "x \<in> V" and neq: "x \<noteq> 0" |
|
295 { |
|
296 from x have "(a - b) \<cdot> x = a \<cdot> x - b \<cdot> x" |
|
297 by (simp add: diff_mult_distrib2) |
|
298 also assume "a \<cdot> x = b \<cdot> x" |
|
299 with x have "a \<cdot> x - b \<cdot> x = 0" by simp |
|
300 finally have "(a - b) \<cdot> x = 0" . |
|
301 with x neq have "a - b = 0" by (rule mult_zero_uniq) |
|
302 then show "a = b" by simp |
|
303 next |
|
304 assume "a = b" |
|
305 then show "a \<cdot> x = b \<cdot> x" by (simp only:) |
|
306 } |
|
307 qed |
|
308 |
|
309 lemma (in vectorspace) eq_diff_eq: |
|
310 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x = z - y) = (x + y = z)" |
|
311 proof |
|
312 assume x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V" |
|
313 { |
|
314 assume "x = z - y" |
|
315 then have "x + y = z - y + y" by simp |
|
316 also from y z have "\<dots> = z + - y + y" |
|
317 by (simp add: diff_eq1) |
|
318 also have "\<dots> = z + (- y + y)" |
|
319 by (rule add_assoc) (simp_all add: y z) |
|
320 also from y z have "\<dots> = z + 0" |
|
321 by (simp only: add_minus_left) |
|
322 also from z have "\<dots> = z" |
|
323 by (simp only: add_zero_right) |
|
324 finally show "x + y = z" . |
|
325 next |
|
326 assume "x + y = z" |
|
327 then have "z - y = (x + y) - y" by simp |
|
328 also from x y have "\<dots> = x + y + - y" |
|
329 by (simp add: diff_eq1) |
|
330 also have "\<dots> = x + (y + - y)" |
|
331 by (rule add_assoc) (simp_all add: x y) |
|
332 also from x y have "\<dots> = x" by simp |
|
333 finally show "x = z - y" .. |
|
334 } |
|
335 qed |
|
336 |
|
337 lemma (in vectorspace) add_minus_eq_minus: |
|
338 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y = 0 \<Longrightarrow> x = - y" |
|
339 proof - |
|
340 assume x: "x \<in> V" and y: "y \<in> V" |
|
341 from x y have "x = (- y + y) + x" by simp |
|
342 also from x y have "\<dots> = - y + (x + y)" by (simp add: add_ac) |
|
343 also assume "x + y = 0" |
|
344 also from y have "- y + 0 = - y" by simp |
|
345 finally show "x = - y" . |
|
346 qed |
|
347 |
|
348 lemma (in vectorspace) add_minus_eq: |
|
349 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y = 0 \<Longrightarrow> x = y" |
|
350 proof - |
|
351 assume x: "x \<in> V" and y: "y \<in> V" |
|
352 assume "x - y = 0" |
|
353 with x y have eq: "x + - y = 0" by (simp add: diff_eq1) |
|
354 with _ _ have "x = - (- y)" |
|
355 by (rule add_minus_eq_minus) (simp_all add: x y) |
|
356 with x y show "x = y" by simp |
|
357 qed |
|
358 |
|
359 lemma (in vectorspace) add_diff_swap: |
|
360 "a \<in> V \<Longrightarrow> b \<in> V \<Longrightarrow> c \<in> V \<Longrightarrow> d \<in> V \<Longrightarrow> a + b = c + d |
|
361 \<Longrightarrow> a - c = d - b" |
|
362 proof - |
|
363 assume vs: "a \<in> V" "b \<in> V" "c \<in> V" "d \<in> V" |
|
364 and eq: "a + b = c + d" |
|
365 then have "- c + (a + b) = - c + (c + d)" |
|
366 by (simp add: add_left_cancel) |
|
367 also have "\<dots> = d" using `c \<in> V` `d \<in> V` by (rule minus_add_cancel) |
|
368 finally have eq: "- c + (a + b) = d" . |
|
369 from vs have "a - c = (- c + (a + b)) + - b" |
|
370 by (simp add: add_ac diff_eq1) |
|
371 also from vs eq have "\<dots> = d + - b" |
|
372 by (simp add: add_right_cancel) |
|
373 also from vs have "\<dots> = d - b" by (simp add: diff_eq2) |
|
374 finally show "a - c = d - b" . |
|
375 qed |
|
376 |
|
377 lemma (in vectorspace) vs_add_cancel_21: |
|
378 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> u \<in> V |
|
379 \<Longrightarrow> (x + (y + z) = y + u) = (x + z = u)" |
|
380 proof |
|
381 assume vs: "x \<in> V" "y \<in> V" "z \<in> V" "u \<in> V" |
|
382 { |
|
383 from vs have "x + z = - y + y + (x + z)" by simp |
|
384 also have "\<dots> = - y + (y + (x + z))" |
|
385 by (rule add_assoc) (simp_all add: vs) |
|
386 also from vs have "y + (x + z) = x + (y + z)" |
|
387 by (simp add: add_ac) |
|
388 also assume "x + (y + z) = y + u" |
|
389 also from vs have "- y + (y + u) = u" by simp |
|
390 finally show "x + z = u" . |
|
391 next |
|
392 assume "x + z = u" |
|
393 with vs show "x + (y + z) = y + u" |
|
394 by (simp only: add_left_commute [of x]) |
|
395 } |
|
396 qed |
|
397 |
|
398 lemma (in vectorspace) add_cancel_end: |
|
399 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x + (y + z) = y) = (x = - z)" |
|
400 proof |
|
401 assume vs: "x \<in> V" "y \<in> V" "z \<in> V" |
|
402 { |
|
403 assume "x + (y + z) = y" |
|
404 with vs have "(x + z) + y = 0 + y" |
|
405 by (simp add: add_ac) |
|
406 with vs have "x + z = 0" |
|
407 by (simp only: add_right_cancel add_closed zero) |
|
408 with vs show "x = - z" by (simp add: add_minus_eq_minus) |
|
409 next |
|
410 assume eq: "x = - z" |
|
411 then have "x + (y + z) = - z + (y + z)" by simp |
|
412 also have "\<dots> = y + (- z + z)" |
|
413 by (rule add_left_commute) (simp_all add: vs) |
|
414 also from vs have "\<dots> = y" by simp |
|
415 finally show "x + (y + z) = y" . |
|
416 } |
|
417 qed |
|
418 |
|
419 end |