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