author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46867  0883804b67bb 
child 54230  b1d955791529 
permissions  rwrr 
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 

9035  5 
header {* Vector spaces *} 
7917  6 

31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29252
diff
changeset

7 
theory Vector_Space 
44887  8 
imports Complex_Main Bounds "~~/src/HOL/Library/Zorn" 
27612  9 
begin 
7917  10 

9035  11 
subsection {* Signature *} 
7917  12 

10687  13 
text {* 
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. 

17 
*} 

7917  18 

19 
consts 

10687  20 
prod :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a" (infixr "'(*')" 70) 
7917  21 

21210  22 
notation (xsymbols) 
19736  23 
prod (infixr "\<cdot>" 70) 
21210  24 
notation (HTML output) 
19736  25 
prod (infixr "\<cdot>" 70) 
7917  26 

27 

9035  28 
subsection {* Vector space laws *} 
7917  29 

10687  30 
text {* 
31 
A \emph{vector space} is a nonempty set @{text V} of elements from 

32 
@{typ 'a} with the following vector space laws: The set @{text V} is 

33 
closed under addition and scalar multiplication, addition is 

34 
associative and commutative; @{text " x"} is the inverse of @{text 

35 
x} w.~r.~t.~addition and @{text 0} is the neutral element of 

36 
addition. Addition and multiplication are distributive; scalar 

12018
ec054019c910
Numerals and simprocs for types real and hypreal. The abstract
paulson
parents:
11704
diff
changeset

37 
multiplication is associative and the real number @{text "1"} is 
10687  38 
the neutral element of scalar multiplication. 
9035  39 
*} 
7917  40 

46867
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

41 
locale vectorspace = 
0883804b67bb
modernized locale expression, with some fluctuation of arguments;
wenzelm
parents:
44887
diff
changeset

42 
fixes V 
13515  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" 

44887  56 
begin 
7917  57 

44887  58 
lemma negate_eq2: "x \<in> V \<Longrightarrow> ( 1) \<cdot> x =  x" 
13515  59 
by (rule negate_eq1 [symmetric]) 
9013
9dd0274f76af
Updated files to remove 0r and 1r from theorems in descendant theories
fleuriot
parents:
8703
diff
changeset

60 

44887  61 
lemma negate_eq2a: "x \<in> V \<Longrightarrow> 1 \<cdot> x =  x" 
13515  62 
by (simp add: negate_eq1) 
7917  63 

44887  64 
lemma diff_eq2: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x +  y = x  y" 
13515  65 
by (rule diff_eq1 [symmetric]) 
7917  66 

44887  67 
lemma diff_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x  y \<in> V" 
9035  68 
by (simp add: diff_eq1 negate_eq1) 
7917  69 

44887  70 
lemma neg_closed [iff]: "x \<in> V \<Longrightarrow>  x \<in> V" 
9035  71 
by (simp add: negate_eq1) 
7917  72 

44887  73 
lemma add_left_commute: "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" 
27612  76 
then have "x + (y + z) = (x + y) + z" 
13515  77 
by (simp only: add_assoc) 
27612  78 
also from xyz have "\<dots> = (y + x) + z" by (simp only: add_commute) 
79 
also from xyz have "\<dots> = y + (x + z)" by (simp only: add_assoc) 

9035  80 
finally show ?thesis . 
81 
qed 

7917  82 

44887  83 
theorems add_ac = add_assoc add_commute add_left_commute 
7917  84 

85 

7978  86 
text {* The existence of the zero element of a vector space 
13515  87 
follows from the nonemptiness of carrier set. *} 
7917  88 

44887  89 
lemma zero [iff]: "0 \<in> V" 
10687  90 
proof  
13515  91 
from non_empty obtain x where x: "x \<in> V" by blast 
92 
then have "0 = x  x" by (rule diff_self [symmetric]) 

27612  93 
also from x x have "\<dots> \<in> V" by (rule diff_closed) 
11472  94 
finally show ?thesis . 
9035  95 
qed 
7917  96 

44887  97 
lemma add_zero_right [simp]: "x \<in> V \<Longrightarrow> x + 0 = x" 
9035  98 
proof  
13515  99 
assume x: "x \<in> V" 
100 
from this and zero have "x + 0 = 0 + x" by (rule add_commute) 

27612  101 
also from x have "\<dots> = x" by (rule add_zero_left) 
9035  102 
finally show ?thesis . 
103 
qed 

7917  104 

44887  105 
lemma mult_assoc2: "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = (a * b) \<cdot> x" 
13515  106 
by (simp only: mult_assoc) 
7917  107 

44887  108 
lemma diff_mult_distrib1: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<cdot> (x  y) = a \<cdot> x  a \<cdot> y" 
13515  109 
by (simp add: diff_eq1 negate_eq1 add_mult_distrib1 mult_assoc2) 
7917  110 

44887  111 
lemma diff_mult_distrib2: "x \<in> V \<Longrightarrow> (a  b) \<cdot> x = a \<cdot> x  (b \<cdot> x)" 
9035  112 
proof  
13515  113 
assume x: "x \<in> V" 
10687  114 
have " (a  b) \<cdot> x = (a +  b) \<cdot> x" 
37887  115 
by (simp add: diff_minus) 
27612  116 
also from x have "\<dots> = a \<cdot> x + ( b) \<cdot> x" 
13515  117 
by (rule add_mult_distrib2) 
27612  118 
also from x have "\<dots> = a \<cdot> x +  (b \<cdot> x)" 
13515  119 
by (simp add: negate_eq1 mult_assoc2) 
27612  120 
also from x have "\<dots> = a \<cdot> x  (b \<cdot> x)" 
13515  121 
by (simp add: diff_eq1) 
9035  122 
finally show ?thesis . 
123 
qed 

7917  124 

44887  125 
lemmas distrib = 
13515  126 
add_mult_distrib1 add_mult_distrib2 
127 
diff_mult_distrib1 diff_mult_distrib2 

128 

10687  129 

130 
text {* \medskip Further derived laws: *} 

7917  131 

44887  132 
lemma mult_zero_left [simp]: "x \<in> V \<Longrightarrow> 0 \<cdot> x = 0" 
9035  133 
proof  
13515  134 
assume x: "x \<in> V" 
135 
have "0 \<cdot> x = (1  1) \<cdot> x" by simp 

27612  136 
also have "\<dots> = (1 +  1) \<cdot> x" by simp 
137 
also from x have "\<dots> = 1 \<cdot> x + ( 1) \<cdot> x" 

13515  138 
by (rule add_mult_distrib2) 
27612  139 
also from x have "\<dots> = x + ( 1) \<cdot> x" by simp 
140 
also from x have "\<dots> = x +  x" by (simp add: negate_eq2a) 

141 
also from x have "\<dots> = x  x" by (simp add: diff_eq2) 

142 
also from x have "\<dots> = 0" by simp 

9035  143 
finally show ?thesis . 
144 
qed 

7917  145 

44887  146 
lemma mult_zero_right [simp]: "a \<cdot> 0 = (0::'a)" 
9035  147 
proof  
13515  148 
have "a \<cdot> 0 = a \<cdot> (0  (0::'a))" by simp 
27612  149 
also have "\<dots> = a \<cdot> 0  a \<cdot> 0" 
13515  150 
by (rule diff_mult_distrib1) simp_all 
27612  151 
also have "\<dots> = 0" by simp 
9035  152 
finally show ?thesis . 
153 
qed 

7917  154 

44887  155 
lemma minus_mult_cancel [simp]: "x \<in> V \<Longrightarrow> ( a) \<cdot>  x = a \<cdot> x" 
13515  156 
by (simp add: negate_eq1 mult_assoc2) 
7917  157 

44887  158 
lemma add_minus_left_eq_diff: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow>  x + y = y  x" 
10687  159 
proof  
13515  160 
assume xy: "x \<in> V" "y \<in> V" 
27612  161 
then have " x + y = y +  x" by (simp add: add_commute) 
162 
also from xy have "\<dots> = y  x" by (simp add: diff_eq1) 

9035  163 
finally show ?thesis . 
164 
qed 

7917  165 

44887  166 
lemma add_minus [simp]: "x \<in> V \<Longrightarrow> x +  x = 0" 
13515  167 
by (simp add: diff_eq2) 
7917  168 

44887  169 
lemma add_minus_left [simp]: "x \<in> V \<Longrightarrow>  x + x = 0" 
13515  170 
by (simp add: diff_eq2 add_commute) 
7917  171 

44887  172 
lemma minus_minus [simp]: "x \<in> V \<Longrightarrow>  ( x) = x" 
13515  173 
by (simp add: negate_eq1 mult_assoc2) 
174 

44887  175 
lemma minus_zero [simp]: " (0::'a) = 0" 
9035  176 
by (simp add: negate_eq1) 
7917  177 

44887  178 
lemma minus_zero_iff [simp]: 
179 
assumes x: "x \<in> V" 

180 
shows "( x = 0) = (x = 0)" 

13515  181 
proof 
44887  182 
from x have "x =  ( x)" by simp 
183 
also assume " x = 0" 

184 
also have " \<dots> = 0" by (rule minus_zero) 

185 
finally show "x = 0" . 

186 
next 

187 
assume "x = 0" 

188 
then show " x = 0" by simp 

9035  189 
qed 
7917  190 

44887  191 
lemma add_minus_cancel [simp]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + ( x + y) = y" 
192 
by (simp add: add_assoc [symmetric]) 

7917  193 

44887  194 
lemma minus_add_cancel [simp]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow>  x + (x + y) = y" 
195 
by (simp add: add_assoc [symmetric]) 

7917  196 

44887  197 
lemma minus_add_distrib [simp]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow>  (x + y) =  x +  y" 
13515  198 
by (simp add: negate_eq1 add_mult_distrib1) 
7917  199 

44887  200 
lemma diff_zero [simp]: "x \<in> V \<Longrightarrow> x  0 = x" 
13515  201 
by (simp add: diff_eq1) 
202 

44887  203 
lemma diff_zero_right [simp]: "x \<in> V \<Longrightarrow> 0  x =  x" 
10687  204 
by (simp add: diff_eq1) 
7917  205 

44887  206 
lemma add_left_cancel: 
207 
assumes x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V" 

208 
shows "(x + y = x + z) = (y = z)" 

9035  209 
proof 
44887  210 
from y have "y = 0 + y" by simp 
211 
also from x y have "\<dots> = ( x + x) + y" by simp 

212 
also from x y have "\<dots> =  x + (x + y)" by (simp add: add_assoc) 

213 
also assume "x + y = x + z" 

214 
also from x z have " x + (x + z) =  x + x + z" by (simp add: add_assoc) 

215 
also from x z have "\<dots> = z" by simp 

216 
finally show "y = z" . 

217 
next 

218 
assume "y = z" 

219 
then show "x + y = x + z" by (simp only:) 

13515  220 
qed 
7917  221 

44887  222 
lemma add_right_cancel: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)" 
13515  223 
by (simp only: add_commute add_left_cancel) 
7917  224 

44887  225 
lemma add_assoc_cong: 
13515  226 
"x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x' \<in> V \<Longrightarrow> y' \<in> V \<Longrightarrow> z \<in> V 
227 
\<Longrightarrow> x + y = x' + y' \<Longrightarrow> x + (y + z) = x' + (y' + z)" 

228 
by (simp only: add_assoc [symmetric]) 

7917  229 

44887  230 
lemma mult_left_commute: "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = b \<cdot> a \<cdot> x" 
36778
739a9379e29b
avoid using realspecific versions of generic lemmas
huffman
parents:
31795
diff
changeset

231 
by (simp add: mult_commute mult_assoc2) 
7917  232 

44887  233 
lemma mult_zero_uniq: 
234 
assumes x: "x \<in> V" "x \<noteq> 0" and ax: "a \<cdot> x = 0" 

235 
shows "a = 0" 

9035  236 
proof (rule classical) 
13515  237 
assume a: "a \<noteq> 0" 
238 
from x a have "x = (inverse a * a) \<cdot> x" by simp 

27612  239 
also from `x \<in> V` have "\<dots> = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc) 
240 
also from ax have "\<dots> = inverse a \<cdot> 0" by simp 

241 
also have "\<dots> = 0" by simp 

9374  242 
finally have "x = 0" . 
23378  243 
with `x \<noteq> 0` show "a = 0" by contradiction 
9035  244 
qed 
7917  245 

44887  246 
lemma mult_left_cancel: 
247 
assumes x: "x \<in> V" and y: "y \<in> V" and a: "a \<noteq> 0" 

248 
shows "(a \<cdot> x = a \<cdot> y) = (x = y)" 

9035  249 
proof 
13515  250 
from x have "x = 1 \<cdot> x" by simp 
27612  251 
also from a have "\<dots> = (inverse a * a) \<cdot> x" by simp 
252 
also from x have "\<dots> = inverse a \<cdot> (a \<cdot> x)" 

13515  253 
by (simp only: mult_assoc) 
254 
also assume "a \<cdot> x = a \<cdot> y" 

27612  255 
also from a y have "inverse a \<cdot> \<dots> = y" 
13515  256 
by (simp add: mult_assoc2) 
257 
finally show "x = y" . 

258 
next 

259 
assume "x = y" 

260 
then show "a \<cdot> x = a \<cdot> y" by (simp only:) 

261 
qed 

7917  262 

44887  263 
lemma mult_right_cancel: 
264 
assumes x: "x \<in> V" and neq: "x \<noteq> 0" 

265 
shows "(a \<cdot> x = b \<cdot> x) = (a = b)" 

9035  266 
proof 
44887  267 
from x have "(a  b) \<cdot> x = a \<cdot> x  b \<cdot> x" 
268 
by (simp add: diff_mult_distrib2) 

269 
also assume "a \<cdot> x = b \<cdot> x" 

270 
with x have "a \<cdot> x  b \<cdot> x = 0" by simp 

271 
finally have "(a  b) \<cdot> x = 0" . 

272 
with x neq have "a  b = 0" by (rule mult_zero_uniq) 

273 
then show "a = b" by simp 

274 
next 

275 
assume "a = b" 

276 
then show "a \<cdot> x = b \<cdot> x" by (simp only:) 

13515  277 
qed 
7917  278 

44887  279 
lemma eq_diff_eq: 
280 
assumes x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V" 

281 
shows "(x = z  y) = (x + y = z)" 

13515  282 
proof 
44887  283 
assume "x = z  y" 
284 
then have "x + y = z  y + y" by simp 

285 
also from y z have "\<dots> = z +  y + y" 

286 
by (simp add: diff_eq1) 

287 
also have "\<dots> = z + ( y + y)" 

288 
by (rule add_assoc) (simp_all add: y z) 

289 
also from y z have "\<dots> = z + 0" 

290 
by (simp only: add_minus_left) 

291 
also from z have "\<dots> = z" 

292 
by (simp only: add_zero_right) 

293 
finally show "x + y = z" . 

294 
next 

295 
assume "x + y = z" 

296 
then have "z  y = (x + y)  y" by simp 

297 
also from x y have "\<dots> = x + y +  y" 

298 
by (simp add: diff_eq1) 

299 
also have "\<dots> = x + (y +  y)" 

300 
by (rule add_assoc) (simp_all add: x y) 

301 
also from x y have "\<dots> = x" by simp 

302 
finally show "x = z  y" .. 

9035  303 
qed 
7917  304 

44887  305 
lemma add_minus_eq_minus: 
306 
assumes x: "x \<in> V" and y: "y \<in> V" and xy: "x + y = 0" 

307 
shows "x =  y" 

9035  308 
proof  
13515  309 
from x y have "x = ( y + y) + x" by simp 
27612  310 
also from x y have "\<dots> =  y + (x + y)" by (simp add: add_ac) 
44887  311 
also note xy 
13515  312 
also from y have " y + 0 =  y" by simp 
9035  313 
finally show "x =  y" . 
314 
qed 

7917  315 

44887  316 
lemma add_minus_eq: 
317 
assumes x: "x \<in> V" and y: "y \<in> V" and xy: "x  y = 0" 

318 
shows "x = y" 

9035  319 
proof  
44887  320 
from x y xy have eq: "x +  y = 0" by (simp add: diff_eq1) 
13515  321 
with _ _ have "x =  ( y)" 
322 
by (rule add_minus_eq_minus) (simp_all add: x y) 

323 
with x y show "x = y" by simp 

9035  324 
qed 
7917  325 

44887  326 
lemma add_diff_swap: 
327 
assumes vs: "a \<in> V" "b \<in> V" "c \<in> V" "d \<in> V" 

328 
and eq: "a + b = c + d" 

329 
shows "a  c = d  b" 

10687  330 
proof  
44887  331 
from assms have " c + (a + b) =  c + (c + d)" 
13515  332 
by (simp add: add_left_cancel) 
27612  333 
also have "\<dots> = d" using `c \<in> V` `d \<in> V` by (rule minus_add_cancel) 
9035  334 
finally have eq: " c + (a + b) = d" . 
10687  335 
from vs have "a  c = ( c + (a + b)) +  b" 
13515  336 
by (simp add: add_ac diff_eq1) 
27612  337 
also from vs eq have "\<dots> = d +  b" 
13515  338 
by (simp add: add_right_cancel) 
27612  339 
also from vs have "\<dots> = d  b" by (simp add: diff_eq2) 
9035  340 
finally show "a  c = d  b" . 
341 
qed 

7917  342 

44887  343 
lemma vs_add_cancel_21: 
344 
assumes vs: "x \<in> V" "y \<in> V" "z \<in> V" "u \<in> V" 

345 
shows "(x + (y + z) = y + u) = (x + z = u)" 

13515  346 
proof 
44887  347 
from vs have "x + z =  y + y + (x + z)" by simp 
348 
also have "\<dots> =  y + (y + (x + z))" 

349 
by (rule add_assoc) (simp_all add: vs) 

350 
also from vs have "y + (x + z) = x + (y + z)" 

351 
by (simp add: add_ac) 

352 
also assume "x + (y + z) = y + u" 

353 
also from vs have " y + (y + u) = u" by simp 

354 
finally show "x + z = u" . 

355 
next 

356 
assume "x + z = u" 

357 
with vs show "x + (y + z) = y + u" 

358 
by (simp only: add_left_commute [of x]) 

9035  359 
qed 
7917  360 

44887  361 
lemma add_cancel_end: 
362 
assumes vs: "x \<in> V" "y \<in> V" "z \<in> V" 

363 
shows "(x + (y + z) = y) = (x =  z)" 

13515  364 
proof 
44887  365 
assume "x + (y + z) = y" 
366 
with vs have "(x + z) + y = 0 + y" by (simp add: add_ac) 

367 
with vs have "x + z = 0" by (simp only: add_right_cancel add_closed zero) 

368 
with vs show "x =  z" by (simp add: add_minus_eq_minus) 

369 
next 

370 
assume eq: "x =  z" 

371 
then have "x + (y + z) =  z + (y + z)" by simp 

372 
also have "\<dots> = y + ( z + z)" by (rule add_left_commute) (simp_all add: vs) 

373 
also from vs have "\<dots> = y" by simp 

374 
finally show "x + (y + z) = y" . 

9035  375 
qed 
7917  376 

10687  377 
end 
44887  378 

379 
end 

380 