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

src/HOL/Hahn_Banach/Vector_Space.thy

author | wenzelm |

Sat Jan 05 17:24:33 2019 +0100 (10 months ago) | |

changeset 69597 | ff784d5a5bfb |

parent 61879 | e4f9d8f094fe |

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

isabelle update -u control_cartouches;

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

2 Author: Gertrud Bauer, TU Munich

3 *)

5 section \<open>Vector spaces\<close>

7 theory Vector_Space

8 imports Complex_Main Bounds

9 begin

11 subsection \<open>Signature\<close>

13 text \<open>

14 For the definition of real vector spaces a type \<^typ>\<open>'a\<close> of the sort

15 \<open>{plus, minus, zero}\<close> is considered, on which a real scalar multiplication

16 \<open>\<cdot>\<close> is declared.

17 \<close>

19 consts

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

23 subsection \<open>Vector space laws\<close>

25 text \<open>

26 A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from \<^typ>\<open>'a\<close> with the

27 following vector space laws: The set \<open>V\<close> is closed under addition and scalar

28 multiplication, addition is associative and commutative; \<open>- x\<close> is the

29 inverse of \<open>x\<close> wrt.\ addition and \<open>0\<close> is the neutral element of addition.

30 Addition and multiplication are distributive; scalar multiplication is

31 associative and the real number \<open>1\<close> is the neutral element of scalar

32 multiplication.

33 \<close>

35 locale vectorspace =

36 fixes V

37 assumes non_empty [iff, intro?]: "V \<noteq> {}"

38 and add_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y \<in> V"

39 and mult_closed [iff]: "x \<in> V \<Longrightarrow> a \<cdot> x \<in> V"

40 and add_assoc: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x + y) + z = x + (y + z)"

41 and add_commute: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y = y + x"

42 and diff_self [simp]: "x \<in> V \<Longrightarrow> x - x = 0"

43 and add_zero_left [simp]: "x \<in> V \<Longrightarrow> 0 + x = x"

44 and add_mult_distrib1: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y"

45 and add_mult_distrib2: "x \<in> V \<Longrightarrow> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x"

46 and mult_assoc: "x \<in> V \<Longrightarrow> (a * b) \<cdot> x = a \<cdot> (b \<cdot> x)"

47 and mult_1 [simp]: "x \<in> V \<Longrightarrow> 1 \<cdot> x = x"

48 and negate_eq1: "x \<in> V \<Longrightarrow> - x = (- 1) \<cdot> x"

49 and diff_eq1: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y = x + - y"

50 begin

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

53 by (rule negate_eq1 [symmetric])

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

56 by (simp add: negate_eq1)

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

59 by (rule diff_eq1 [symmetric])

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

62 by (simp add: diff_eq1 negate_eq1)

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

65 by (simp add: negate_eq1)

67 lemma add_left_commute:

68 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)"

69 proof -

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

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

72 by (simp only: add_assoc)

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)

75 finally show ?thesis .

76 qed

78 lemmas add_ac = add_assoc add_commute add_left_commute

81 text \<open>

82 The existence of the zero element of a vector space follows from the

83 non-emptiness of carrier set.

84 \<close>

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

87 proof -

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

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

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

91 finally show ?thesis .

92 qed

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

95 proof -

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

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

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

99 finally show ?thesis .

100 qed

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

103 by (simp only: mult_assoc)

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

106 by (simp add: diff_eq1 negate_eq1 add_mult_distrib1 mult_assoc2)

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

109 proof -

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

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

112 by simp

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

114 by (rule add_mult_distrib2)

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

116 by (simp add: negate_eq1 mult_assoc2)

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

118 by (simp add: diff_eq1)

119 finally show ?thesis .

120 qed

122 lemmas distrib =

123 add_mult_distrib1 add_mult_distrib2

124 diff_mult_distrib1 diff_mult_distrib2

127 text \<open>\<^medskip> Further derived laws:\<close>

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

130 proof -

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

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

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

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

135 by (rule add_mult_distrib2)

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

137 also from x have "\<dots> = x + - x" by (simp add: negate_eq2a)

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

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

140 finally show ?thesis .

141 qed

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

144 proof -

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

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

147 by (rule diff_mult_distrib1) simp_all

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

149 finally show ?thesis .

150 qed

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

153 by (simp add: negate_eq1 mult_assoc2)

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

156 proof -

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

158 then have "- x + y = y + - x" by (simp add: add_commute)

159 also from xy have "\<dots> = y - x" by (simp add: diff_eq1)

160 finally show ?thesis .

161 qed

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

164 by (simp add: diff_eq2)

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

167 by (simp add: diff_eq2 add_commute)

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

170 by (simp add: negate_eq1 mult_assoc2)

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

173 by (simp add: negate_eq1)

175 lemma minus_zero_iff [simp]:

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

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

178 proof

179 from x have "x = - (- x)" by simp

180 also assume "- x = 0"

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

182 finally show "x = 0" .

183 next

184 assume "x = 0"

185 then show "- x = 0" by simp

186 qed

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

189 by (simp add: add_assoc [symmetric])

191 lemma minus_add_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_distrib [simp]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - (x + y) = - x + - y"

195 by (simp add: negate_eq1 add_mult_distrib1)

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

198 by (simp add: diff_eq1)

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

201 by (simp add: diff_eq1)

203 lemma add_left_cancel:

204 assumes x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V"

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

206 proof

207 from y have "y = 0 + y" by simp

208 also from x y have "\<dots> = (- x + x) + y" by simp

209 also from x y have "\<dots> = - x + (x + y)" by (simp add: add.assoc)

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

211 also from x z have "- x + (x + z) = - x + x + z" by (simp add: add.assoc)

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

213 finally show "y = z" .

214 next

215 assume "y = z"

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

217 qed

219 lemma add_right_cancel:

220 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)"

221 by (simp only: add_commute add_left_cancel)

223 lemma add_assoc_cong:

224 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x' \<in> V \<Longrightarrow> y' \<in> V \<Longrightarrow> z \<in> V

225 \<Longrightarrow> x + y = x' + y' \<Longrightarrow> x + (y + z) = x' + (y' + z)"

226 by (simp only: add_assoc [symmetric])

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

229 by (simp add: mult.commute mult_assoc2)

231 lemma mult_zero_uniq:

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

233 shows "a = 0"

234 proof (rule classical)

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

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

237 also from \<open>x \<in> V\<close> have "\<dots> = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc)

238 also from ax have "\<dots> = inverse a \<cdot> 0" by simp

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

240 finally have "x = 0" .

241 with \<open>x \<noteq> 0\<close> show "a = 0" by contradiction

242 qed

244 lemma mult_left_cancel:

245 assumes x: "x \<in> V" and y: "y \<in> V" and a: "a \<noteq> 0"

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

247 proof

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

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

250 also from x have "\<dots> = inverse a \<cdot> (a \<cdot> x)"

251 by (simp only: mult_assoc)

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

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

254 by (simp add: mult_assoc2)

255 finally show "x = y" .

256 next

257 assume "x = y"

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

259 qed

261 lemma mult_right_cancel:

262 assumes x: "x \<in> V" and neq: "x \<noteq> 0"

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

264 proof

265 from x have "(a - b) \<cdot> x = a \<cdot> x - b \<cdot> x"

266 by (simp add: diff_mult_distrib2)

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

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

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

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

271 then show "a = b" by simp

272 next

273 assume "a = b"

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

275 qed

277 lemma eq_diff_eq:

278 assumes x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V"

279 shows "(x = z - y) = (x + y = z)"

280 proof

281 assume "x = z - y"

282 then have "x + y = z - y + y" by simp

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

284 by (simp add: diff_eq1)

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

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

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

288 by (simp only: add_minus_left)

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

290 by (simp only: add_zero_right)

291 finally show "x + y = z" .

292 next

293 assume "x + y = z"

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

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

296 by (simp add: diff_eq1)

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

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

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

300 finally show "x = z - y" ..

301 qed

303 lemma add_minus_eq_minus:

304 assumes x: "x \<in> V" and y: "y \<in> V" and xy: "x + y = 0"

305 shows "x = - y"

306 proof -

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

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

309 also note xy

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

311 finally show "x = - y" .

312 qed

314 lemma add_minus_eq:

315 assumes x: "x \<in> V" and y: "y \<in> V" and xy: "x - y = 0"

316 shows "x = y"

317 proof -

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

319 with _ _ have "x = - (- y)"

320 by (rule add_minus_eq_minus) (simp_all add: x y)

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

322 qed

324 lemma add_diff_swap:

325 assumes vs: "a \<in> V" "b \<in> V" "c \<in> V" "d \<in> V"

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

327 shows "a - c = d - b"

328 proof -

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

330 by (simp add: add_left_cancel)

331 also have "\<dots> = d" using \<open>c \<in> V\<close> \<open>d \<in> V\<close> by (rule minus_add_cancel)

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

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

334 by (simp add: add_ac diff_eq1)

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

336 by (simp add: add_right_cancel)

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

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

339 qed

341 lemma vs_add_cancel_21:

342 assumes vs: "x \<in> V" "y \<in> V" "z \<in> V" "u \<in> V"

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

344 proof

345 from vs have "x + z = - y + y + (x + z)" by simp

346 also have "\<dots> = - y + (y + (x + z))"

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

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

349 by (simp add: add_ac)

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

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

352 finally show "x + z = u" .

353 next

354 assume "x + z = u"

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

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

357 qed

359 lemma add_cancel_end:

360 assumes vs: "x \<in> V" "y \<in> V" "z \<in> V"

361 shows "(x + (y + z) = y) = (x = - z)"

362 proof

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

364 with vs have "(x + z) + y = 0 + y" by (simp add: add_ac)

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

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

367 next

368 assume eq: "x = - z"

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

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

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

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

373 qed

375 end

377 end