1 (* Title: HOL/Real/HahnBanach/LinearSpace.thy |
|
2 ID: $Id$ |
|
3 Author: Gertrud Bauer, TU Munich |
|
4 *) |
|
5 |
|
6 header {* Linear Spaces *}; |
|
7 |
|
8 theory LinearSpace = Bounds + Aux:; |
|
9 |
|
10 subsection {* Signature *}; |
|
11 |
|
12 consts |
|
13 sum :: "['a, 'a] => 'a" (infixl "[+]" 65) |
|
14 prod :: "[real, 'a] => 'a" (infixr "[*]" 70) |
|
15 zero :: 'a ("<0>"); |
|
16 |
|
17 constdefs |
|
18 negate :: "'a => 'a" ("[-] _" [100] 100) |
|
19 "[-] x == (- 1r) [*] x" |
|
20 diff :: "'a => 'a => 'a" (infixl "[-]" 68) |
|
21 "x [-] y == x [+] [-] y"; |
|
22 |
|
23 subsection {* Vector space laws *} |
|
24 (*** |
|
25 constdefs |
|
26 is_vectorspace :: "'a set => bool" |
|
27 "is_vectorspace V == V ~= {} |
|
28 & (ALL x: V. ALL a. a [*] x: V) |
|
29 & (ALL x: V. ALL y: V. x [+] y = y [+] x) |
|
30 & (ALL x: V. ALL y: V. ALL z: V. x [+] y [+] z = x [+] (y [+] z)) |
|
31 & (ALL x: V. ALL y: V. x [+] y: V) |
|
32 & (ALL x: V. x [-] x = <0>) |
|
33 & (ALL x: V. <0> [+] x = x) |
|
34 & (ALL x: V. ALL y: V. ALL a. a [*] (x [+] y) = a [*] x [+] a [*] y) |
|
35 & (ALL x: V. ALL a b. (a + b) [*] x = a [*] x [+] b [*] x) |
|
36 & (ALL x: V. ALL a b. (a * b) [*] x = a [*] b [*] x) |
|
37 & (ALL x: V. 1r [*] x = x)"; |
|
38 ***) |
|
39 constdefs |
|
40 is_vectorspace :: "'a set => bool" |
|
41 "is_vectorspace V == V ~= {} |
|
42 & (ALL x:V. ALL y:V. ALL z:V. ALL a b. |
|
43 x [+] y: V |
|
44 & a [*] x: V |
|
45 & x [+] y [+] z = x [+] (y [+] z) |
|
46 & x [+] y = y [+] x |
|
47 & x [-] x = <0> |
|
48 & <0> [+] x = x |
|
49 & a [*] (x [+] y) = a [*] x [+] a [*] y |
|
50 & (a + b) [*] x = a [*] x [+] b [*] x |
|
51 & (a * b) [*] x = a [*] b [*] x |
|
52 & 1r [*] x = x)"; |
|
53 |
|
54 lemma vsI [intro]: |
|
55 "[| <0>:V; \ |
|
56 ALL x: V. ALL y: V. x [+] y: V; |
|
57 ALL x: V. ALL a. a [*] x: V; |
|
58 ALL x: V. ALL y: V. ALL z: V. x [+] y [+] z = x [+] (y [+] z); |
|
59 ALL x: V. ALL y: V. x [+] y = y [+] x; |
|
60 ALL x: V. x [-] x = <0>; |
|
61 ALL x: V. <0> [+] x = x; |
|
62 ALL x: V. ALL y: V. ALL a. a [*] (x [+] y) = a [*] x [+] a [*] y; |
|
63 ALL x: V. ALL a b. (a + b) [*] x = a [*] x [+] b [*] x; |
|
64 ALL x: V. ALL a b. (a * b) [*] x = a [*] b [*] x; \ |
|
65 ALL x: V. 1r [*] x = x |] ==> is_vectorspace V"; |
|
66 proof (unfold is_vectorspace_def, intro conjI ballI allI); |
|
67 fix x y z; assume "x:V" "y:V" "z:V"; |
|
68 assume "ALL x: V. ALL y: V. ALL z: V. x [+] y [+] z = x [+] (y [+] z)"; |
|
69 thus "x [+] y [+] z = x [+] (y [+] z)"; by (elim bspec[elimify]); |
|
70 qed force+; |
|
71 |
|
72 lemma vs_not_empty [intro !!]: "is_vectorspace V ==> (V ~= {})"; |
|
73 by (unfold is_vectorspace_def) simp; |
|
74 |
|
75 lemma vs_add_closed [simp, intro!!]: |
|
76 "[| is_vectorspace V; x: V; y: V|] ==> x [+] y: V"; |
|
77 by (unfold is_vectorspace_def) simp; |
|
78 |
|
79 lemma vs_mult_closed [simp, intro!!]: |
|
80 "[| is_vectorspace V; x: V |] ==> a [*] x: V"; |
|
81 by (unfold is_vectorspace_def) simp; |
|
82 |
|
83 lemma vs_diff_closed [simp, intro!!]: |
|
84 "[| is_vectorspace V; x: V; y: V|] ==> x [-] y: V"; |
|
85 by (unfold diff_def negate_def) simp; |
|
86 |
|
87 lemma vs_neg_closed [simp, intro!!]: |
|
88 "[| is_vectorspace V; x: V |] ==> [-] x: V"; |
|
89 by (unfold negate_def) simp; |
|
90 |
|
91 lemma vs_add_assoc [simp]: |
|
92 "[| is_vectorspace V; x: V; y: V; z: V|] |
|
93 ==> x [+] y [+] z = x [+] (y [+] z)"; |
|
94 by (unfold is_vectorspace_def) fast; |
|
95 |
|
96 lemma vs_add_commute [simp]: |
|
97 "[| is_vectorspace V; x:V; y:V |] ==> y [+] x = x [+] y"; |
|
98 by (unfold is_vectorspace_def) simp; |
|
99 |
|
100 lemma vs_add_left_commute [simp]: |
|
101 "[| is_vectorspace V; x:V; y:V; z:V |] |
|
102 ==> x [+] (y [+] z) = y [+] (x [+] z)"; |
|
103 proof -; |
|
104 assume "is_vectorspace V" "x:V" "y:V" "z:V"; |
|
105 hence "x [+] (y [+] z) = (x [+] y) [+] z"; |
|
106 by (simp only: vs_add_assoc); |
|
107 also; have "... = (y [+] x) [+] z"; by (simp! only: vs_add_commute); |
|
108 also; have "... = y [+] (x [+] z)"; by (simp! only: vs_add_assoc); |
|
109 finally; show ?thesis; .; |
|
110 qed; |
|
111 |
|
112 theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute; |
|
113 |
|
114 lemma vs_diff_self [simp]: |
|
115 "[| is_vectorspace V; x:V |] ==> x [-] x = <0>"; |
|
116 by (unfold is_vectorspace_def) simp; |
|
117 |
|
118 lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> <0>:V"; |
|
119 proof -; |
|
120 assume "is_vectorspace V"; |
|
121 have "V ~= {}"; ..; |
|
122 hence "EX x. x:V"; by force; |
|
123 thus ?thesis; |
|
124 proof; |
|
125 fix x; assume "x:V"; |
|
126 have "<0> = x [-] x"; by (simp!); |
|
127 also; have "... : V"; by (simp! only: vs_diff_closed); |
|
128 finally; show ?thesis; .; |
|
129 qed; |
|
130 qed; |
|
131 |
|
132 lemma vs_add_zero_left [simp]: |
|
133 "[| is_vectorspace V; x:V |] ==> <0> [+] x = x"; |
|
134 by (unfold is_vectorspace_def) simp; |
|
135 |
|
136 lemma vs_add_zero_right [simp]: |
|
137 "[| is_vectorspace V; x:V |] ==> x [+] <0> = x"; |
|
138 proof -; |
|
139 assume "is_vectorspace V" "x:V"; |
|
140 hence "x [+] <0> = <0> [+] x"; by simp; |
|
141 also; have "... = x"; by (simp!); |
|
142 finally; show ?thesis; .; |
|
143 qed; |
|
144 |
|
145 lemma vs_add_mult_distrib1: |
|
146 "[| is_vectorspace V; x:V; y:V |] |
|
147 ==> a [*] (x [+] y) = a [*] x [+] a [*] y"; |
|
148 by (unfold is_vectorspace_def) simp; |
|
149 |
|
150 lemma vs_add_mult_distrib2: |
|
151 "[| is_vectorspace V; x:V |] ==> (a + b) [*] x = a [*] x [+] b [*] x"; |
|
152 by (unfold is_vectorspace_def) simp; |
|
153 |
|
154 lemma vs_mult_assoc: |
|
155 "[| is_vectorspace V; x:V |] ==> (a * b) [*] x = a [*] (b [*] x)"; |
|
156 by (unfold is_vectorspace_def) simp; |
|
157 |
|
158 lemma vs_mult_assoc2 [simp]: |
|
159 "[| is_vectorspace V; x:V |] ==> a [*] b [*] x = (a * b) [*] x"; |
|
160 by (simp only: vs_mult_assoc); |
|
161 |
|
162 lemma vs_mult_1 [simp]: |
|
163 "[| is_vectorspace V; x:V |] ==> 1r [*] x = x"; |
|
164 by (unfold is_vectorspace_def) simp; |
|
165 |
|
166 lemma vs_diff_mult_distrib1: |
|
167 "[| is_vectorspace V; x:V; y:V |] |
|
168 ==> a [*] (x [-] y) = a [*] x [-] a [*] y"; |
|
169 by (simp add: diff_def negate_def vs_add_mult_distrib1); |
|
170 |
|
171 lemma vs_minus_eq: "[| is_vectorspace V; x:V |] |
|
172 ==> - b [*] x = [-] (b [*] x)"; |
|
173 by (simp add: negate_def); |
|
174 |
|
175 lemma vs_diff_mult_distrib2: |
|
176 "[| is_vectorspace V; x:V |] |
|
177 ==> (a - b) [*] x = a [*] x [-] (b [*] x)"; |
|
178 proof -; |
|
179 assume "is_vectorspace V" "x:V"; |
|
180 have " (a - b) [*] x = (a + - b ) [*] x"; |
|
181 by (unfold real_diff_def, simp); |
|
182 also; have "... = a [*] x [+] (- b) [*] x"; |
|
183 by (rule vs_add_mult_distrib2); |
|
184 also; have "... = a [*] x [+] [-] (b [*] x)"; |
|
185 by (simp! add: vs_minus_eq); |
|
186 also; have "... = a [*] x [-] (b [*] x)"; by (unfold diff_def, simp); |
|
187 finally; show ?thesis; .; |
|
188 qed; |
|
189 |
|
190 lemma vs_mult_zero_left [simp]: |
|
191 "[| is_vectorspace V; x: V|] ==> 0r [*] x = <0>"; |
|
192 proof -; |
|
193 assume "is_vectorspace V" "x:V"; |
|
194 have "0r [*] x = (1r - 1r) [*] x"; by (simp only: real_diff_self); |
|
195 also; have "... = (1r + - 1r) [*] x"; by simp; |
|
196 also; have "... = 1r [*] x [+] (- 1r) [*] x"; |
|
197 by (rule vs_add_mult_distrib2); |
|
198 also; have "... = x [+] (- 1r) [*] x"; by (simp!); |
|
199 also; have "... = x [+] [-] x"; by (fold negate_def) simp; |
|
200 also; have "... = x [-] x"; by (fold diff_def) simp; |
|
201 also; have "... = <0>"; by (simp!); |
|
202 finally; show ?thesis; .; |
|
203 qed; |
|
204 |
|
205 lemma vs_mult_zero_right [simp]: |
|
206 "[| is_vectorspace (V:: 'a set) |] ==> a [*] <0> = (<0>::'a)"; |
|
207 proof -; |
|
208 assume "is_vectorspace V"; |
|
209 have "a [*] <0> = a [*] (<0> [-] (<0>::'a))"; by (simp!); |
|
210 also; have "... = a [*] <0> [-] a [*] <0>"; |
|
211 by (rule vs_diff_mult_distrib1) (simp!)+; |
|
212 also; have "... = <0>"; by (simp!); |
|
213 finally; show ?thesis; .; |
|
214 qed; |
|
215 |
|
216 lemma vs_minus_mult_cancel [simp]: |
|
217 "[| is_vectorspace V; x:V |] ==> (- a) [*] [-] x = a [*] x"; |
|
218 by (unfold negate_def) simp; |
|
219 |
|
220 lemma vs_add_minus_left_eq_diff: |
|
221 "[| is_vectorspace V; x:V; y:V |] ==> [-] x [+] y = y [-] x"; |
|
222 proof -; |
|
223 assume "is_vectorspace V" "x:V" "y:V"; |
|
224 have "[-] x [+] y = y [+] [-] x"; |
|
225 by (simp! add: vs_add_commute [RS sym, of V "[-] x"]); |
|
226 also; have "... = y [-] x"; by (unfold diff_def) simp; |
|
227 finally; show ?thesis; .; |
|
228 qed; |
|
229 |
|
230 lemma vs_add_minus [simp]: |
|
231 "[| is_vectorspace V; x:V|] ==> x [+] [-] x = <0>"; |
|
232 by (fold diff_def) simp; |
|
233 |
|
234 lemma vs_add_minus_left [simp]: |
|
235 "[| is_vectorspace V; x:V |] ==> [-] x [+] x = <0>"; |
|
236 by (fold diff_def) simp; |
|
237 |
|
238 lemma vs_minus_minus [simp]: |
|
239 "[| is_vectorspace V; x:V|] ==> [-] [-] x = x"; |
|
240 by (unfold negate_def) simp; |
|
241 |
|
242 lemma vs_minus_zero [simp]: |
|
243 "[| is_vectorspace (V::'a set)|] ==> [-] (<0>::'a) = <0>"; |
|
244 by (unfold negate_def) simp; |
|
245 |
|
246 lemma vs_minus_zero_iff [simp]: |
|
247 "[| is_vectorspace V; x:V|] ==> ([-] x = <0>) = (x = <0>)" |
|
248 (concl is "?L = ?R"); |
|
249 proof -; |
|
250 assume vs: "is_vectorspace V" "x:V"; |
|
251 show "?L = ?R"; |
|
252 proof; |
|
253 assume l: ?L; |
|
254 have "x = [-] [-] x"; by (rule vs_minus_minus [RS sym]); |
|
255 also; have "... = [-] <0>"; by (simp only: l); |
|
256 also; have "... = <0>"; by (rule vs_minus_zero); |
|
257 finally; show ?R; .; |
|
258 next; |
|
259 assume ?R; |
|
260 with vs; show ?L; by simp; |
|
261 qed; |
|
262 qed; |
|
263 |
|
264 lemma vs_add_minus_cancel [simp]: |
|
265 "[| is_vectorspace V; x:V; y:V|] ==> x [+] ([-] x [+] y) = y"; |
|
266 by (simp add: vs_add_assoc [RS sym] del: vs_add_commute); |
|
267 |
|
268 lemma vs_minus_add_cancel [simp]: |
|
269 "[| is_vectorspace V; x:V; y:V |] ==> [-] x [+] (x [+] y) = y"; |
|
270 by (simp add: vs_add_assoc [RS sym] del: vs_add_commute); |
|
271 |
|
272 lemma vs_minus_add_distrib [simp]: |
|
273 "[| is_vectorspace V; x:V; y:V|] |
|
274 ==> [-] (x [+] y) = [-] x [+] [-] y"; |
|
275 by (unfold negate_def, simp add: vs_add_mult_distrib1); |
|
276 |
|
277 lemma vs_diff_zero [simp]: |
|
278 "[| is_vectorspace V; x:V |] ==> x [-] <0> = x"; |
|
279 by (unfold diff_def) simp; |
|
280 |
|
281 lemma vs_diff_zero_right [simp]: |
|
282 "[| is_vectorspace V; x:V |] ==> <0> [-] x = [-] x"; |
|
283 by (unfold diff_def) simp; |
|
284 |
|
285 lemma vs_add_left_cancel: |
|
286 "[| is_vectorspace V; x:V; y:V; z:V|] |
|
287 ==> (x [+] y = x [+] z) = (y = z)" |
|
288 (concl is "?L = ?R"); |
|
289 proof; |
|
290 assume "is_vectorspace V" "x:V" "y:V" "z:V"; |
|
291 assume l: ?L; |
|
292 have "y = <0> [+] y"; by (simp!); |
|
293 also; have "... = [-] x [+] x [+] y"; by (simp!); |
|
294 also; have "... = [-] x [+] (x [+] y)"; |
|
295 by (simp! only: vs_add_assoc vs_neg_closed); |
|
296 also; have "... = [-] x [+] (x [+] z)"; by (simp only: l); |
|
297 also; have "... = [-] x [+] x [+] z"; |
|
298 by (rule vs_add_assoc [RS sym]) (simp!)+; |
|
299 also; have "... = z"; by (simp!); |
|
300 finally; show ?R;.; |
|
301 next; |
|
302 assume ?R; |
|
303 thus ?L; by force; |
|
304 qed; |
|
305 |
|
306 lemma vs_add_right_cancel: |
|
307 "[| is_vectorspace V; x:V; y:V; z:V |] |
|
308 ==> (y [+] x = z [+] x) = (y = z)"; |
|
309 by (simp only: vs_add_commute vs_add_left_cancel); |
|
310 |
|
311 lemma vs_add_assoc_cong [tag FIXME simp]: |
|
312 "[| is_vectorspace V; x:V; y:V; x':V; y':V; z:V |] |
|
313 ==> x [+] y = x' [+] y' ==> x [+] (y [+] z) = x' [+] (y' [+] z)"; |
|
314 by (simp del: vs_add_commute vs_add_assoc add: vs_add_assoc [RS sym]); |
|
315 |
|
316 lemma vs_mult_left_commute: |
|
317 "[| is_vectorspace V; x:V; y:V; z:V |] |
|
318 ==> x [*] y [*] z = y [*] x [*] z"; |
|
319 by (simp add: real_mult_commute); |
|
320 |
|
321 lemma vs_mult_zero_uniq : |
|
322 "[| is_vectorspace V; x:V; a [*] x = <0>; x ~= <0> |] ==> a = 0r"; |
|
323 proof (rule classical); |
|
324 assume "is_vectorspace V" "x:V" "a [*] x = <0>" "x ~= <0>"; |
|
325 assume "a ~= 0r"; |
|
326 have "x = (rinv a * a) [*] x"; by (simp!); |
|
327 also; have "... = (rinv a) [*] (a [*] x)"; by (rule vs_mult_assoc); |
|
328 also; have "... = (rinv a) [*] <0>"; by (simp!); |
|
329 also; have "... = <0>"; by (simp!); |
|
330 finally; have "x = <0>"; .; |
|
331 thus "a = 0r"; by contradiction; |
|
332 qed; |
|
333 |
|
334 lemma vs_mult_left_cancel: |
|
335 "[| is_vectorspace V; x:V; y:V; a ~= 0r |] ==> |
|
336 (a [*] x = a [*] y) = (x = y)" |
|
337 (concl is "?L = ?R"); |
|
338 proof; |
|
339 assume "is_vectorspace V" "x:V" "y:V" "a ~= 0r"; |
|
340 assume l: ?L; |
|
341 have "x = 1r [*] x"; by (simp!); |
|
342 also; have "... = (rinv a * a) [*] x"; by (simp!); |
|
343 also; have "... = rinv a [*] (a [*] x)"; |
|
344 by (simp! only: vs_mult_assoc); |
|
345 also; have "... = rinv a [*] (a [*] y)"; by (simp only: l); |
|
346 also; have "... = y"; by (simp!); |
|
347 finally; show ?R;.; |
|
348 next; |
|
349 assume ?R; |
|
350 thus ?L; by simp; |
|
351 qed; |
|
352 |
|
353 lemma vs_mult_right_cancel: (*** forward ***) |
|
354 "[| is_vectorspace V; x:V; x ~= <0> |] ==> (a [*] x = b [*] x) = (a = b)" |
|
355 (concl is "?L = ?R"); |
|
356 proof; |
|
357 assume "is_vectorspace V" "x:V" "x ~= <0>"; |
|
358 assume l: ?L; |
|
359 have "(a - b) [*] x = a [*] x [-] b [*] x"; by (simp! add: vs_diff_mult_distrib2); |
|
360 also; from l; have "a [*] x [-] b [*] x = <0>"; by (simp!); |
|
361 finally; have "(a - b) [*] x = <0>"; .; |
|
362 hence "a - b = 0r"; by (simp! add: vs_mult_zero_uniq); |
|
363 thus "a = b"; by (rule real_add_minus_eq); |
|
364 next; |
|
365 assume ?R; |
|
366 thus ?L; by simp; |
|
367 qed; (*** backward : |
|
368 lemma vs_mult_right_cancel: |
|
369 "[| is_vectorspace V; x:V; x ~= <0> |] ==> (a [*] x = b [*] x) = (a = b)" |
|
370 (concl is "?L = ?R"); |
|
371 proof; |
|
372 assume "is_vectorspace V" "x:V" "x ~= <0>"; |
|
373 assume l: ?L; |
|
374 show "a = b"; |
|
375 proof (rule real_add_minus_eq); |
|
376 show "a - b = 0r"; |
|
377 proof (rule vs_mult_zero_uniq); |
|
378 have "(a - b) [*] x = a [*] x [-] b [*] x"; by (simp! add: vs_diff_mult_distrib2); |
|
379 also; from l; have "a [*] x [-] b [*] x = <0>"; by (simp!); |
|
380 finally; show "(a - b) [*] x = <0>"; .; |
|
381 qed; |
|
382 qed; |
|
383 next; |
|
384 assume ?R; |
|
385 thus ?L; by simp; |
|
386 qed; |
|
387 **) |
|
388 |
|
389 lemma vs_eq_diff_eq: |
|
390 "[| is_vectorspace V; x:V; y:V; z:V |] ==> |
|
391 (x = z [-] y) = (x [+] y = z)" |
|
392 (concl is "?L = ?R" ); |
|
393 proof -; |
|
394 assume vs: "is_vectorspace V" "x:V" "y:V" "z:V"; |
|
395 show "?L = ?R"; |
|
396 proof; |
|
397 assume l: ?L; |
|
398 have "x [+] y = z [-] y [+] y"; by (simp add: l); |
|
399 also; have "... = z [+] [-] y [+] y"; by (unfold diff_def) simp; |
|
400 also; have "... = z [+] ([-] y [+] y)"; |
|
401 by (rule vs_add_assoc) (simp!)+; |
|
402 also; from vs; have "... = z [+] <0>"; |
|
403 by (simp only: vs_add_minus_left); |
|
404 also; from vs; have "... = z"; by (simp only: vs_add_zero_right); |
|
405 finally; show ?R;.; |
|
406 next; |
|
407 assume r: ?R; |
|
408 have "z [-] y = (x [+] y) [-] y"; by (simp only: r); |
|
409 also; from vs; have "... = x [+] y [+] [-] y"; |
|
410 by (unfold diff_def) simp; |
|
411 also; have "... = x [+] (y [+] [-] y)"; |
|
412 by (rule vs_add_assoc) (simp!)+; |
|
413 also; have "... = x"; by (simp!); |
|
414 finally; show ?L; by (rule sym); |
|
415 qed; |
|
416 qed; |
|
417 |
|
418 lemma vs_add_minus_eq_minus: |
|
419 "[| is_vectorspace V; x:V; y:V; <0> = x [+] y|] ==> y = [-] x"; |
|
420 proof -; |
|
421 assume vs: "is_vectorspace V" "x:V" "y:V"; |
|
422 assume "<0> = x [+] y"; |
|
423 have "[-] x = [-] x [+] <0>"; by (simp!); |
|
424 also; have "... = [-] x [+] (x [+] y)"; by (simp!); |
|
425 also; have "... = [-] x [+] x [+] y"; |
|
426 by (rule vs_add_assoc [RS sym]) (simp!)+; |
|
427 also; have "... = (x [+] [-] x) [+] y"; by (simp!); |
|
428 also; have "... = y"; by (simp!); |
|
429 finally; show ?thesis; by (rule sym); |
|
430 qed; |
|
431 |
|
432 lemma vs_add_minus_eq: |
|
433 "[| is_vectorspace V; x:V; y:V; x [-] y = <0> |] ==> x = y"; |
|
434 proof -; |
|
435 assume "is_vectorspace V" "x:V" "y:V" "x [-] y = <0>"; |
|
436 have "x [+] [-] y = x [-] y"; by (unfold diff_def, simp); |
|
437 also; have "... = <0>"; .; |
|
438 finally; have e: "<0> = x [+] [-] y"; by (rule sym); |
|
439 have "x = [-] [-] x"; by (simp!); |
|
440 also; have "[-] x = [-] y"; |
|
441 by (rule vs_add_minus_eq_minus [RS sym]) (simp! add: e)+; |
|
442 also; have "[-] ... = y"; by (simp!); |
|
443 finally; show "x = y"; .; |
|
444 qed; |
|
445 |
|
446 lemma vs_add_diff_swap: |
|
447 "[| is_vectorspace V; a:V; b:V; c:V; d:V; a [+] b = c [+] d|] |
|
448 ==> a [-] c = d [-] b"; |
|
449 proof -; |
|
450 assume vs: "is_vectorspace V" "a:V" "b:V" "c:V" "d:V" |
|
451 and eq: "a [+] b = c [+] d"; |
|
452 have "[-] c [+] (a [+] b) = [-] c [+] (c [+] d)"; |
|
453 by (simp! add: vs_add_left_cancel); |
|
454 also; have "... = d"; by (rule vs_minus_add_cancel); |
|
455 finally; have eq: "[-] c [+] (a [+] b) = d"; .; |
|
456 from vs; have "a [-] c = ([-] c [+] (a [+] b)) [+] [-] b"; |
|
457 by (simp add: vs_add_ac diff_def); |
|
458 also; from eq; have "... = d [+] [-] b"; |
|
459 by (simp! add: vs_add_right_cancel); |
|
460 also; have "... = d [-] b"; by (simp add : diff_def); |
|
461 finally; show "a [-] c = d [-] b"; .; |
|
462 qed; |
|
463 |
|
464 lemma vs_add_cancel_21: |
|
465 "[| is_vectorspace V; x:V; y:V; z:V; u:V|] |
|
466 ==> (x [+] (y [+] z) = y [+] u) = ((x [+] z) = u)" |
|
467 (concl is "?L = ?R" ); |
|
468 proof -; |
|
469 assume vs: "is_vectorspace V" "x:V" "y:V""z:V" "u:V"; |
|
470 show "?L = ?R"; |
|
471 proof; |
|
472 assume l: ?L; |
|
473 have "u = <0> [+] u"; by (simp!); |
|
474 also; have "... = [-] y [+] y [+] u"; by (simp!); |
|
475 also; have "... = [-] y [+] (y [+] u)"; |
|
476 by (rule vs_add_assoc) (simp!)+; |
|
477 also; have "... = [-] y [+] (x [+] (y [+] z))"; by (simp only: l); |
|
478 also; have "... = [-] y [+] (y [+] (x [+] z))"; by (simp!); |
|
479 also; have "... = [-] y [+] y [+] (x [+] z)"; |
|
480 by (rule vs_add_assoc [RS sym]) (simp!)+; |
|
481 also; have "... = (x [+] z)"; by (simp!); |
|
482 finally; show ?R; by (rule sym); |
|
483 next; |
|
484 assume r: ?R; |
|
485 have "x [+] (y [+] z) = y [+] (x [+] z)"; |
|
486 by (simp! only: vs_add_left_commute [of V x]); |
|
487 also; have "... = y [+] u"; by (simp only: r); |
|
488 finally; show ?L; .; |
|
489 qed; |
|
490 qed; |
|
491 |
|
492 lemma vs_add_cancel_end: |
|
493 "[| is_vectorspace V; x:V; y:V; z:V |] |
|
494 ==> (x [+] (y [+] z) = y) = (x = [-] z)" |
|
495 (concl is "?L = ?R" ); |
|
496 proof -; |
|
497 assume vs: "is_vectorspace V" "x:V" "y:V" "z:V"; |
|
498 show "?L = ?R"; |
|
499 proof; |
|
500 assume l: ?L; |
|
501 have "<0> = x [+] z"; |
|
502 proof (rule vs_add_left_cancel [RS iffD1]); |
|
503 have "y [+] <0> = y"; by (simp! only: vs_add_zero_right); |
|
504 also; have "... = x [+] (y [+] z)"; by (simp only: l); |
|
505 also; have "... = y [+] (x [+] z)"; |
|
506 by (simp! only: vs_add_left_commute); |
|
507 finally; show "y [+] <0> = y [+] (x [+] z)"; .; |
|
508 qed (simp!)+; |
|
509 hence "z = [-] x"; by (simp! only: vs_add_minus_eq_minus); |
|
510 then; show ?R; by (simp!); |
|
511 next; |
|
512 assume r: ?R; |
|
513 have "x [+] (y [+] z) = [-] z [+] (y [+] z)"; by (simp only: r); |
|
514 also; have "... = y [+] ([-] z [+] z)"; |
|
515 by (simp! only: vs_add_left_commute); |
|
516 also; have "... = y [+] <0>"; by (simp!); |
|
517 also; have "... = y"; by (simp!); |
|
518 finally; show ?L; .; |
|
519 qed; |
|
520 qed; |
|
521 |
|
522 lemma it: "[| x = y; x' = y'|] ==> x [+] x' = y [+] y'"; |
|
523 by simp; |
|
524 |
|
525 end; |
|