1 (* Title: HOL/Real/HahnBanach/VectorSpace.thy
3 Author: Gertrud Bauer, TU Munich
6 header {* Vector spaces *}
8 theory VectorSpace = Aux:
10 subsection {* Signature *}
13 For the definition of real vector spaces a type @{typ 'a} of the
14 sort @{text "{plus, minus, zero}"} is considered, on which a real
15 scalar multiplication @{text \<cdot>} is declared.
19 prod :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a" (infixr "'(*')" 70)
22 prod :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<cdot>" 70)
24 prod :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<cdot>" 70)
27 subsection {* Vector space laws *}
30 A \emph{vector space} is a non-empty set @{text V} of elements from
31 @{typ 'a} with the following vector space laws: The set @{text V} is
32 closed under addition and scalar multiplication, addition is
33 associative and commutative; @{text "- x"} is the inverse of @{text
34 x} w.~r.~t.~addition and @{text 0} is the neutral element of
35 addition. Addition and multiplication are distributive; scalar
36 multiplication is associative and the real number @{text "1"} is
37 the neutral element of scalar multiplication.
40 locale vectorspace = var V +
41 assumes non_empty [iff, intro?]: "V \<noteq> {}"
42 and add_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y \<in> V"
43 and mult_closed [iff]: "x \<in> V \<Longrightarrow> a \<cdot> x \<in> V"
44 and add_assoc: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x + y) + z = x + (y + z)"
45 and add_commute: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y = y + x"
46 and diff_self [simp]: "x \<in> V \<Longrightarrow> x - x = 0"
47 and add_zero_left [simp]: "x \<in> V \<Longrightarrow> 0 + x = x"
48 and add_mult_distrib1: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y"
49 and add_mult_distrib2: "x \<in> V \<Longrightarrow> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x"
50 and mult_assoc: "x \<in> V \<Longrightarrow> (a * b) \<cdot> x = a \<cdot> (b \<cdot> x)"
51 and mult_1 [simp]: "x \<in> V \<Longrightarrow> 1 \<cdot> x = x"
52 and negate_eq1: "x \<in> V \<Longrightarrow> - x = (- 1) \<cdot> x"
53 and diff_eq1: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y = x + - y"
55 lemma (in vectorspace) negate_eq2: "x \<in> V \<Longrightarrow> (- 1) \<cdot> x = - x"
56 by (rule negate_eq1 [symmetric])
58 lemma (in vectorspace) negate_eq2a: "x \<in> V \<Longrightarrow> -1 \<cdot> x = - x"
59 by (simp add: negate_eq1)
61 lemma (in vectorspace) diff_eq2: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + - y = x - y"
62 by (rule diff_eq1 [symmetric])
64 lemma (in vectorspace) diff_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y \<in> V"
65 by (simp add: diff_eq1 negate_eq1)
67 lemma (in vectorspace) neg_closed [iff]: "x \<in> V \<Longrightarrow> - x \<in> V"
68 by (simp add: negate_eq1)
70 lemma (in vectorspace) add_left_commute:
71 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)"
73 assume xyz: "x \<in> V" "y \<in> V" "z \<in> V"
74 hence "x + (y + z) = (x + y) + z"
75 by (simp only: add_assoc)
76 also from xyz have "... = (y + x) + z" by (simp only: add_commute)
77 also from xyz have "... = y + (x + z)" by (simp only: add_assoc)
78 finally show ?thesis .
81 theorems (in vectorspace) add_ac =
82 add_assoc add_commute add_left_commute
85 text {* The existence of the zero element of a vector space
86 follows from the non-emptiness of carrier set. *}
88 lemma (in vectorspace) zero [iff]: "0 \<in> V"
90 from non_empty obtain x where x: "x \<in> V" by blast
91 then have "0 = x - x" by (rule diff_self [symmetric])
92 also from x have "... \<in> V" by (rule diff_closed)
93 finally show ?thesis .
96 lemma (in vectorspace) add_zero_right [simp]:
97 "x \<in> V \<Longrightarrow> x + 0 = x"
100 from this and zero have "x + 0 = 0 + x" by (rule add_commute)
101 also from x have "... = x" by (rule add_zero_left)
102 finally show ?thesis .
105 lemma (in vectorspace) mult_assoc2:
106 "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = (a * b) \<cdot> x"
107 by (simp only: mult_assoc)
109 lemma (in vectorspace) diff_mult_distrib1:
110 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<cdot> (x - y) = a \<cdot> x - a \<cdot> y"
111 by (simp add: diff_eq1 negate_eq1 add_mult_distrib1 mult_assoc2)
113 lemma (in vectorspace) diff_mult_distrib2:
114 "x \<in> V \<Longrightarrow> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)"
116 assume x: "x \<in> V"
117 have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
118 by (simp add: real_diff_def)
119 also have "... = a \<cdot> x + (- b) \<cdot> x"
120 by (rule add_mult_distrib2)
121 also from x have "... = a \<cdot> x + - (b \<cdot> x)"
122 by (simp add: negate_eq1 mult_assoc2)
123 also from x have "... = a \<cdot> x - (b \<cdot> x)"
124 by (simp add: diff_eq1)
125 finally show ?thesis .
128 lemmas (in vectorspace) distrib =
129 add_mult_distrib1 add_mult_distrib2
130 diff_mult_distrib1 diff_mult_distrib2
133 text {* \medskip Further derived laws: *}
135 lemma (in vectorspace) mult_zero_left [simp]:
136 "x \<in> V \<Longrightarrow> 0 \<cdot> x = 0"
138 assume x: "x \<in> V"
139 have "0 \<cdot> x = (1 - 1) \<cdot> x" by simp
140 also have "... = (1 + - 1) \<cdot> x" by simp
141 also have "... = 1 \<cdot> x + (- 1) \<cdot> x"
142 by (rule add_mult_distrib2)
143 also from x have "... = x + (- 1) \<cdot> x" by simp
144 also from x have "... = x + - x" by (simp add: negate_eq2a)
145 also from x have "... = x - x" by (simp add: diff_eq2)
146 also from x have "... = 0" by simp
147 finally show ?thesis .
150 lemma (in vectorspace) mult_zero_right [simp]:
151 "a \<cdot> 0 = (0::'a)"
153 have "a \<cdot> 0 = a \<cdot> (0 - (0::'a))" by simp
154 also have "... = a \<cdot> 0 - a \<cdot> 0"
155 by (rule diff_mult_distrib1) simp_all
156 also have "... = 0" by simp
157 finally show ?thesis .
160 lemma (in vectorspace) minus_mult_cancel [simp]:
161 "x \<in> V \<Longrightarrow> (- a) \<cdot> - x = a \<cdot> x"
162 by (simp add: negate_eq1 mult_assoc2)
164 lemma (in vectorspace) add_minus_left_eq_diff:
165 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + y = y - x"
167 assume xy: "x \<in> V" "y \<in> V"
168 hence "- x + y = y + - x" by (simp add: add_commute)
169 also from xy have "... = y - x" by (simp add: diff_eq1)
170 finally show ?thesis .
173 lemma (in vectorspace) add_minus [simp]:
174 "x \<in> V \<Longrightarrow> x + - x = 0"
175 by (simp add: diff_eq2)
177 lemma (in vectorspace) add_minus_left [simp]:
178 "x \<in> V \<Longrightarrow> - x + x = 0"
179 by (simp add: diff_eq2 add_commute)
181 lemma (in vectorspace) minus_minus [simp]:
182 "x \<in> V \<Longrightarrow> - (- x) = x"
183 by (simp add: negate_eq1 mult_assoc2)
185 lemma (in vectorspace) minus_zero [simp]:
187 by (simp add: negate_eq1)
189 lemma (in vectorspace) minus_zero_iff [simp]:
190 "x \<in> V \<Longrightarrow> (- x = 0) = (x = 0)"
192 assume x: "x \<in> V"
194 from x have "x = - (- x)" by (simp add: minus_minus)
195 also assume "- x = 0"
196 also have "- ... = 0" by (rule minus_zero)
197 finally show "x = 0" .
200 then show "- x = 0" by simp
204 lemma (in vectorspace) add_minus_cancel [simp]:
205 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + (- x + y) = y"
206 by (simp add: add_assoc [symmetric] del: add_commute)
208 lemma (in vectorspace) minus_add_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)
212 lemma (in vectorspace) minus_add_distrib [simp]:
213 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - (x + y) = - x + - y"
214 by (simp add: negate_eq1 add_mult_distrib1)
216 lemma (in vectorspace) diff_zero [simp]:
217 "x \<in> V \<Longrightarrow> x - 0 = x"
218 by (simp add: diff_eq1)
220 lemma (in vectorspace) diff_zero_right [simp]:
221 "x \<in> V \<Longrightarrow> 0 - x = - x"
222 by (simp add: diff_eq1)
224 lemma (in vectorspace) add_left_cancel:
225 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x + y = x + z) = (y = z)"
227 assume x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V"
229 from y have "y = 0 + y" by simp
230 also from x y have "... = (- x + x) + y" by simp
231 also from x y have "... = - x + (x + y)"
232 by (simp add: add_assoc neg_closed)
233 also assume "x + y = x + z"
234 also from x z have "- x + (x + z) = - x + x + z"
235 by (simp add: add_assoc [symmetric] neg_closed)
236 also from x z have "... = z" by simp
237 finally show "y = z" .
240 then show "x + y = x + z" by (simp only:)
244 lemma (in vectorspace) add_right_cancel:
245 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)"
246 by (simp only: add_commute add_left_cancel)
248 lemma (in vectorspace) add_assoc_cong:
249 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x' \<in> V \<Longrightarrow> y' \<in> V \<Longrightarrow> z \<in> V
250 \<Longrightarrow> x + y = x' + y' \<Longrightarrow> x + (y + z) = x' + (y' + z)"
251 by (simp only: add_assoc [symmetric])
253 lemma (in vectorspace) mult_left_commute:
254 "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = b \<cdot> a \<cdot> x"
255 by (simp add: real_mult_commute mult_assoc2)
257 lemma (in vectorspace) mult_zero_uniq:
258 "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> a \<cdot> x = 0 \<Longrightarrow> a = 0"
259 proof (rule classical)
260 assume a: "a \<noteq> 0"
261 assume x: "x \<in> V" "x \<noteq> 0" and ax: "a \<cdot> x = 0"
262 from x a have "x = (inverse a * a) \<cdot> x" by simp
263 also have "... = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc)
264 also from ax have "... = inverse a \<cdot> 0" by simp
265 also have "... = 0" by simp
266 finally have "x = 0" .
267 thus "a = 0" by contradiction
270 lemma (in vectorspace) mult_left_cancel:
271 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (a \<cdot> x = a \<cdot> y) = (x = y)"
273 assume x: "x \<in> V" and y: "y \<in> V" and a: "a \<noteq> 0"
274 from x have "x = 1 \<cdot> x" by simp
275 also from a have "... = (inverse a * a) \<cdot> x" by simp
276 also from x have "... = inverse a \<cdot> (a \<cdot> x)"
277 by (simp only: mult_assoc)
278 also assume "a \<cdot> x = a \<cdot> y"
279 also from a y have "inverse a \<cdot> ... = y"
280 by (simp add: mult_assoc2)
281 finally show "x = y" .
284 then show "a \<cdot> x = a \<cdot> y" by (simp only:)
287 lemma (in vectorspace) mult_right_cancel:
288 "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> (a \<cdot> x = b \<cdot> x) = (a = b)"
290 assume x: "x \<in> V" and neq: "x \<noteq> 0"
292 from x have "(a - b) \<cdot> x = a \<cdot> x - b \<cdot> x"
293 by (simp add: diff_mult_distrib2)
294 also assume "a \<cdot> x = b \<cdot> x"
295 with x have "a \<cdot> x - b \<cdot> x = 0" by simp
296 finally have "(a - b) \<cdot> x = 0" .
297 with x neq have "a - b = 0" by (rule mult_zero_uniq)
301 then show "a \<cdot> x = b \<cdot> x" by (simp only:)
305 lemma (in vectorspace) eq_diff_eq:
306 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x = z - y) = (x + y = z)"
308 assume x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V"
311 hence "x + y = z - y + y" by simp
312 also from y z have "... = z + - y + y"
313 by (simp add: diff_eq1)
314 also have "... = z + (- y + y)"
315 by (rule add_assoc) (simp_all add: y z)
316 also from y z have "... = z + 0"
317 by (simp only: add_minus_left)
318 also from z have "... = z"
319 by (simp only: add_zero_right)
320 finally show "x + y = z" .
323 hence "z - y = (x + y) - y" by simp
324 also from x y have "... = x + y + - y"
325 by (simp add: diff_eq1)
326 also have "... = x + (y + - y)"
327 by (rule add_assoc) (simp_all add: x y)
328 also from x y have "... = x" by simp
329 finally show "x = z - y" ..
333 lemma (in vectorspace) add_minus_eq_minus:
334 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y = 0 \<Longrightarrow> x = - y"
336 assume x: "x \<in> V" and y: "y \<in> V"
337 from x y have "x = (- y + y) + x" by simp
338 also from x y have "... = - y + (x + y)" by (simp add: add_ac)
339 also assume "x + y = 0"
340 also from y have "- y + 0 = - y" by simp
341 finally show "x = - y" .
344 lemma (in vectorspace) add_minus_eq:
345 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y = 0 \<Longrightarrow> x = y"
347 assume x: "x \<in> V" and y: "y \<in> V"
349 with x y have eq: "x + - y = 0" by (simp add: diff_eq1)
350 with _ _ have "x = - (- y)"
351 by (rule add_minus_eq_minus) (simp_all add: x y)
352 with x y show "x = y" by simp
355 lemma (in vectorspace) add_diff_swap:
356 "a \<in> V \<Longrightarrow> b \<in> V \<Longrightarrow> c \<in> V \<Longrightarrow> d \<in> V \<Longrightarrow> a + b = c + d
357 \<Longrightarrow> a - c = d - b"
359 assume vs: "a \<in> V" "b \<in> V" "c \<in> V" "d \<in> V"
360 and eq: "a + b = c + d"
361 then have "- c + (a + b) = - c + (c + d)"
362 by (simp add: add_left_cancel)
363 also have "... = d" by (rule minus_add_cancel)
364 finally have eq: "- c + (a + b) = d" .
365 from vs have "a - c = (- c + (a + b)) + - b"
366 by (simp add: add_ac diff_eq1)
367 also from vs eq have "... = d + - b"
368 by (simp add: add_right_cancel)
369 also from vs have "... = d - b" by (simp add: diff_eq2)
370 finally show "a - c = d - b" .
373 lemma (in vectorspace) vs_add_cancel_21:
374 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> u \<in> V
375 \<Longrightarrow> (x + (y + z) = y + u) = (x + z = u)"
377 assume vs: "x \<in> V" "y \<in> V" "z \<in> V" "u \<in> V"
379 from vs have "x + z = - y + y + (x + z)" by simp
380 also have "... = - y + (y + (x + z))"
381 by (rule add_assoc) (simp_all add: vs)
382 also from vs have "y + (x + z) = x + (y + z)"
383 by (simp add: add_ac)
384 also assume "x + (y + z) = y + u"
385 also from vs have "- y + (y + u) = u" by simp
386 finally show "x + z = u" .
389 with vs show "x + (y + z) = y + u"
390 by (simp only: add_left_commute [of x])
394 lemma (in vectorspace) add_cancel_end:
395 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x + (y + z) = y) = (x = - z)"
397 assume vs: "x \<in> V" "y \<in> V" "z \<in> V"
399 assume "x + (y + z) = y"
400 with vs have "(x + z) + y = 0 + y"
401 by (simp add: add_ac)
402 with vs have "x + z = 0"
403 by (simp only: add_right_cancel add_closed zero)
404 with vs show "x = - z" by (simp add: add_minus_eq_minus)
407 hence "x + (y + z) = - z + (y + z)" by simp
408 also have "... = y + (- z + z)"
409 by (rule add_left_commute) (simp_all add: vs)
410 also from vs have "... = y" by simp
411 finally show "x + (y + z) = y" .