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