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