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