summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Hahn_Banach/Vector_Space.thy

author | blanchet |

Thu Jan 16 16:33:19 2014 +0100 (2014-01-16) | |

changeset 55018 | 2a526bd279ed |

parent 54230 | b1d955791529 |

child 57512 | cc97b347b301 |

permissions | -rw-r--r-- |

moved 'Zorn' into 'Main', since it's a BNF dependency

1 (* Title: HOL/Hahn_Banach/Vector_Space.thy

2 Author: Gertrud Bauer, TU Munich

3 *)

5 header {* Vector spaces *}

7 theory Vector_Space

8 imports Complex_Main Bounds

9 begin

11 subsection {* Signature *}

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 *}

19 consts

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

22 notation (xsymbols)

23 prod (infixr "\<cdot>" 70)

24 notation (HTML output)

25 prod (infixr "\<cdot>" 70)

28 subsection {* Vector space laws *}

30 text {*

31 A \emph{vector space} is a non-empty 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

37 multiplication is associative and the real number @{text "1"} is

38 the neutral element of scalar multiplication.

39 *}

41 locale vectorspace =

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

56 begin

58 lemma negate_eq2: "x \<in> V \<Longrightarrow> (- 1) \<cdot> x = - x"

59 by (rule negate_eq1 [symmetric])

61 lemma negate_eq2a: "x \<in> V \<Longrightarrow> -1 \<cdot> x = - x"

62 by (simp add: negate_eq1)

64 lemma diff_eq2: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + - y = x - y"

65 by (rule diff_eq1 [symmetric])

67 lemma diff_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y \<in> V"

68 by (simp add: diff_eq1 negate_eq1)

70 lemma neg_closed [iff]: "x \<in> V \<Longrightarrow> - x \<in> V"

71 by (simp add: negate_eq1)

73 lemma add_left_commute: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)"

74 proof -

75 assume xyz: "x \<in> V" "y \<in> V" "z \<in> V"

76 then have "x + (y + z) = (x + y) + z"

77 by (simp only: add_assoc)

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)

80 finally show ?thesis .

81 qed

83 theorems add_ac = add_assoc add_commute add_left_commute

86 text {* The existence of the zero element of a vector space

87 follows from the non-emptiness of carrier set. *}

89 lemma zero [iff]: "0 \<in> V"

90 proof -

91 from non_empty obtain x where x: "x \<in> V" by blast

92 then have "0 = x - x" by (rule diff_self [symmetric])

93 also from x x have "\<dots> \<in> V" by (rule diff_closed)

94 finally show ?thesis .

95 qed

97 lemma add_zero_right [simp]: "x \<in> V \<Longrightarrow> x + 0 = x"

98 proof -

99 assume x: "x \<in> V"

100 from this and zero have "x + 0 = 0 + x" by (rule add_commute)

101 also from x have "\<dots> = x" by (rule add_zero_left)

102 finally show ?thesis .

103 qed

105 lemma mult_assoc2: "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = (a * b) \<cdot> x"

106 by (simp only: mult_assoc)

108 lemma diff_mult_distrib1: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<cdot> (x - y) = a \<cdot> x - a \<cdot> y"

109 by (simp add: diff_eq1 negate_eq1 add_mult_distrib1 mult_assoc2)

111 lemma diff_mult_distrib2: "x \<in> V \<Longrightarrow> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)"

112 proof -

113 assume x: "x \<in> V"

114 have " (a - b) \<cdot> x = (a + - b) \<cdot> x"

115 by simp

116 also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x"

117 by (rule add_mult_distrib2)

118 also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)"

119 by (simp add: negate_eq1 mult_assoc2)

120 also from x have "\<dots> = a \<cdot> x - (b \<cdot> x)"

121 by (simp add: diff_eq1)

122 finally show ?thesis .

123 qed

125 lemmas distrib =

126 add_mult_distrib1 add_mult_distrib2

127 diff_mult_distrib1 diff_mult_distrib2

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

132 lemma mult_zero_left [simp]: "x \<in> V \<Longrightarrow> 0 \<cdot> x = 0"

133 proof -

134 assume x: "x \<in> V"

135 have "0 \<cdot> x = (1 - 1) \<cdot> x" by simp

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

137 also from x have "\<dots> = 1 \<cdot> x + (- 1) \<cdot> x"

138 by (rule add_mult_distrib2)

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

143 finally show ?thesis .

144 qed

146 lemma mult_zero_right [simp]: "a \<cdot> 0 = (0::'a)"

147 proof -

148 have "a \<cdot> 0 = a \<cdot> (0 - (0::'a))" by simp

149 also have "\<dots> = a \<cdot> 0 - a \<cdot> 0"

150 by (rule diff_mult_distrib1) simp_all

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

152 finally show ?thesis .

153 qed

155 lemma minus_mult_cancel [simp]: "x \<in> V \<Longrightarrow> (- a) \<cdot> - x = a \<cdot> x"

156 by (simp add: negate_eq1 mult_assoc2)

158 lemma add_minus_left_eq_diff: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + y = y - x"

159 proof -

160 assume xy: "x \<in> V" "y \<in> V"

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)

163 finally show ?thesis .

164 qed

166 lemma add_minus [simp]: "x \<in> V \<Longrightarrow> x + - x = 0"

167 by (simp add: diff_eq2)

169 lemma add_minus_left [simp]: "x \<in> V \<Longrightarrow> - x + x = 0"

170 by (simp add: diff_eq2 add_commute)

172 lemma minus_minus [simp]: "x \<in> V \<Longrightarrow> - (- x) = x"

173 by (simp add: negate_eq1 mult_assoc2)

175 lemma minus_zero [simp]: "- (0::'a) = 0"

176 by (simp add: negate_eq1)

178 lemma minus_zero_iff [simp]:

179 assumes x: "x \<in> V"

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

181 proof

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

189 qed

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])

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])

197 lemma minus_add_distrib [simp]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - (x + y) = - x + - y"

198 by (simp add: negate_eq1 add_mult_distrib1)

200 lemma diff_zero [simp]: "x \<in> V \<Longrightarrow> x - 0 = x"

201 by (simp add: diff_eq1)

203 lemma diff_zero_right [simp]: "x \<in> V \<Longrightarrow> 0 - x = - x"

204 by (simp add: diff_eq1)

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)"

209 proof

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:)

220 qed

222 lemma add_right_cancel: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)"

223 by (simp only: add_commute add_left_cancel)

225 lemma add_assoc_cong:

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])

230 lemma mult_left_commute: "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = b \<cdot> a \<cdot> x"

231 by (simp add: mult_commute mult_assoc2)

233 lemma mult_zero_uniq:

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

235 shows "a = 0"

236 proof (rule classical)

237 assume a: "a \<noteq> 0"

238 from x a have "x = (inverse a * a) \<cdot> x" by simp

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

242 finally have "x = 0" .

243 with `x \<noteq> 0` show "a = 0" by contradiction

244 qed

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)"

249 proof

250 from x have "x = 1 \<cdot> x" by simp

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)"

253 by (simp only: mult_assoc)

254 also assume "a \<cdot> x = a \<cdot> y"

255 also from a y have "inverse a \<cdot> \<dots> = y"

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

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)"

266 proof

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:)

277 qed

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)"

282 proof

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" ..

303 qed

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"

308 proof -

309 from x y have "x = (- y + y) + x" by simp

310 also from x y have "\<dots> = - y + (x + y)" by (simp add: add_ac)

311 also note xy

312 also from y have "- y + 0 = - y" by simp

313 finally show "x = - y" .

314 qed

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"

319 proof -

320 from x y xy have eq: "x + - y = 0" by (simp add: diff_eq1)

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

324 qed

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"

330 proof -

331 from assms have "- c + (a + b) = - c + (c + d)"

332 by (simp add: add_left_cancel)

333 also have "\<dots> = d" using `c \<in> V` `d \<in> V` by (rule minus_add_cancel)

334 finally have eq: "- c + (a + b) = d" .

335 from vs have "a - c = (- c + (a + b)) + - b"

336 by (simp add: add_ac diff_eq1)

337 also from vs eq have "\<dots> = d + - b"

338 by (simp add: add_right_cancel)

339 also from vs have "\<dots> = d - b" by (simp add: diff_eq2)

340 finally show "a - c = d - b" .

341 qed

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)"

346 proof

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])

359 qed

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)"

364 proof

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" .

375 qed

377 end

379 end