1(* Title: HOL/Hahn_Banach/Vector_Space.thy 2 Author: Gertrud Bauer, TU Munich 3*) 4 5section \<open>Vector spaces\<close> 6 7theory Vector_Space 8imports Complex_Main Bounds 9begin 10 11subsection \<open>Signature\<close> 12 13text \<open> 14 For the definition of real vector spaces a type @{typ 'a} 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> 18 19consts 20 prod :: "real \<Rightarrow> 'a::{plus,minus,zero} \<Rightarrow> 'a" (infixr "\<cdot>" 70) 21 22 23subsection \<open>Vector space laws\<close> 24 25text \<open> 26 A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from @{typ 'a} 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> 34 35locale 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" 50begin 51 52lemma negate_eq2: "x \<in> V \<Longrightarrow> (- 1) \<cdot> x = - x" 53 by (rule negate_eq1 [symmetric]) 54 55lemma negate_eq2a: "x \<in> V \<Longrightarrow> -1 \<cdot> x = - x" 56 by (simp add: negate_eq1) 57 58lemma diff_eq2: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + - y = x - y" 59 by (rule diff_eq1 [symmetric]) 60 61lemma diff_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y \<in> V" 62 by (simp add: diff_eq1 negate_eq1) 63 64lemma neg_closed [iff]: "x \<in> V \<Longrightarrow> - x \<in> V" 65 by (simp add: negate_eq1) 66 67lemma add_left_commute: 68 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)" 69proof - 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 . 76qed 77 78lemmas add_ac = add_assoc add_commute add_left_commute 79 80 81text \<open> 82 The existence of the zero element of a vector space follows from the 83 non-emptiness of carrier set. 84\<close> 85 86lemma zero [iff]: "0 \<in> V" 87proof - 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 . 92qed 93 94lemma add_zero_right [simp]: "x \<in> V \<Longrightarrow> x + 0 = x" 95proof - 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 . 100qed 101 102lemma mult_assoc2: "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = (a * b) \<cdot> x" 103 by (simp only: mult_assoc) 104 105lemma 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) 107 108lemma diff_mult_distrib2: "x \<in> V \<Longrightarrow> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)" 109proof - 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 . 120qed 121 122lemmas distrib = 123 add_mult_distrib1 add_mult_distrib2 124 diff_mult_distrib1 diff_mult_distrib2 125 126 127text \<open>\<^medskip> Further derived laws:\<close> 128 129lemma mult_zero_left [simp]: "x \<in> V \<Longrightarrow> 0 \<cdot> x = 0" 130proof - 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 . 141qed 142 143lemma mult_zero_right [simp]: "a \<cdot> 0 = (0::'a)" 144proof - 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 . 150qed 151 152lemma minus_mult_cancel [simp]: "x \<in> V \<Longrightarrow> (- a) \<cdot> - x = a \<cdot> x" 153 by (simp add: negate_eq1 mult_assoc2) 154 155lemma add_minus_left_eq_diff: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + y = y - x" 156proof - 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 . 161qed 162 163lemma add_minus [simp]: "x \<in> V \<Longrightarrow> x + - x = 0" 164 by (simp add: diff_eq2) 165 166lemma add_minus_left [simp]: "x \<in> V \<Longrightarrow> - x + x = 0" 167 by (simp add: diff_eq2 add_commute) 168 169lemma minus_minus [simp]: "x \<in> V \<Longrightarrow> - (- x) = x" 170 by (simp add: negate_eq1 mult_assoc2) 171 172lemma minus_zero [simp]: "- (0::'a) = 0" 173 by (simp add: negate_eq1) 174 175lemma minus_zero_iff [simp]: 176 assumes x: "x \<in> V" 177 shows "(- x = 0) = (x = 0)" 178proof 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" . 183next 184 assume "x = 0" 185 then show "- x = 0" by simp 186qed 187 188lemma add_minus_cancel [simp]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + (- x + y) = y" 189 by (simp add: add_assoc [symmetric]) 190 191lemma minus_add_cancel [simp]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + (x + y) = y" 192 by (simp add: add_assoc [symmetric]) 193 194lemma 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) 196 197lemma diff_zero [simp]: "x \<in> V \<Longrightarrow> x - 0 = x" 198 by (simp add: diff_eq1) 199 200lemma diff_zero_right [simp]: "x \<in> V \<Longrightarrow> 0 - x = - x" 201 by (simp add: diff_eq1) 202 203lemma 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)" 206proof 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" . 214next 215 assume "y = z" 216 then show "x + y = x + z" by (simp only:) 217qed 218 219lemma 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) 222 223lemma 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]) 227 228lemma 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) 230 231lemma mult_zero_uniq: 232 assumes x: "x \<in> V" "x \<noteq> 0" and ax: "a \<cdot> x = 0" 233 shows "a = 0" 234proof (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 242qed 243 244lemma 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)" 247proof 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" . 256next 257 assume "x = y" 258 then show "a \<cdot> x = a \<cdot> y" by (simp only:) 259qed 260 261lemma mult_right_cancel: 262 assumes x: "x \<in> V" and neq: "x \<noteq> 0" 263 shows "(a \<cdot> x = b \<cdot> x) = (a = b)" 264proof 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 272next 273 assume "a = b" 274 then show "a \<cdot> x = b \<cdot> x" by (simp only:) 275qed 276 277lemma 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)" 280proof 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" . 292next 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" .. 301qed 302 303lemma add_minus_eq_minus: 304 assumes x: "x \<in> V" and y: "y \<in> V" and xy: "x + y = 0" 305 shows "x = - y" 306proof - 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" . 312qed 313 314lemma add_minus_eq: 315 assumes x: "x \<in> V" and y: "y \<in> V" and xy: "x - y = 0" 316 shows "x = y" 317proof - 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 322qed 323 324lemma 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" 328proof - 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" . 339qed 340 341lemma 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)" 344proof 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" . 353next 354 assume "x + z = u" 355 with vs show "x + (y + z) = y + u" 356 by (simp only: add_left_commute [of x]) 357qed 358 359lemma add_cancel_end: 360 assumes vs: "x \<in> V" "y \<in> V" "z \<in> V" 361 shows "(x + (y + z) = y) = (x = - z)" 362proof 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) 367next 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" . 373qed 374 375end 376 377end 378