1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/Hahn_Banach/Vector_Space.thy Wed Jun 24 21:46:54 2009 +0200
1.3 @@ -0,0 +1,418 @@
1.4 +(* Title: HOL/Hahn_Banach/Vector_Space.thy
1.5 + Author: Gertrud Bauer, TU Munich
1.6 +*)
1.7 +
1.8 +header {* Vector spaces *}
1.9 +
1.10 +theory Vector_Space
1.11 +imports Real Bounds Zorn
1.12 +begin
1.13 +
1.14 +subsection {* Signature *}
1.15 +
1.16 +text {*
1.17 + For the definition of real vector spaces a type @{typ 'a} of the
1.18 + sort @{text "{plus, minus, zero}"} is considered, on which a real
1.19 + scalar multiplication @{text \<cdot>} is declared.
1.20 +*}
1.21 +
1.22 +consts
1.23 + prod :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a" (infixr "'(*')" 70)
1.24 +
1.25 +notation (xsymbols)
1.26 + prod (infixr "\<cdot>" 70)
1.27 +notation (HTML output)
1.28 + prod (infixr "\<cdot>" 70)
1.29 +
1.30 +
1.31 +subsection {* Vector space laws *}
1.32 +
1.33 +text {*
1.34 + A \emph{vector space} is a non-empty set @{text V} of elements from
1.35 + @{typ 'a} with the following vector space laws: The set @{text V} is
1.36 + closed under addition and scalar multiplication, addition is
1.37 + associative and commutative; @{text "- x"} is the inverse of @{text
1.38 + x} w.~r.~t.~addition and @{text 0} is the neutral element of
1.39 + addition. Addition and multiplication are distributive; scalar
1.40 + multiplication is associative and the real number @{text "1"} is
1.41 + the neutral element of scalar multiplication.
1.42 +*}
1.43 +
1.44 +locale var_V = fixes V
1.45 +
1.46 +locale vectorspace = var_V +
1.47 + assumes non_empty [iff, intro?]: "V \<noteq> {}"
1.48 + and add_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y \<in> V"
1.49 + and mult_closed [iff]: "x \<in> V \<Longrightarrow> a \<cdot> x \<in> V"
1.50 + and add_assoc: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x + y) + z = x + (y + z)"
1.51 + and add_commute: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y = y + x"
1.52 + and diff_self [simp]: "x \<in> V \<Longrightarrow> x - x = 0"
1.53 + and add_zero_left [simp]: "x \<in> V \<Longrightarrow> 0 + x = x"
1.54 + and add_mult_distrib1: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y"
1.55 + and add_mult_distrib2: "x \<in> V \<Longrightarrow> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x"
1.56 + and mult_assoc: "x \<in> V \<Longrightarrow> (a * b) \<cdot> x = a \<cdot> (b \<cdot> x)"
1.57 + and mult_1 [simp]: "x \<in> V \<Longrightarrow> 1 \<cdot> x = x"
1.58 + and negate_eq1: "x \<in> V \<Longrightarrow> - x = (- 1) \<cdot> x"
1.59 + and diff_eq1: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y = x + - y"
1.60 +
1.61 +lemma (in vectorspace) negate_eq2: "x \<in> V \<Longrightarrow> (- 1) \<cdot> x = - x"
1.62 + by (rule negate_eq1 [symmetric])
1.63 +
1.64 +lemma (in vectorspace) negate_eq2a: "x \<in> V \<Longrightarrow> -1 \<cdot> x = - x"
1.65 + by (simp add: negate_eq1)
1.66 +
1.67 +lemma (in vectorspace) diff_eq2: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + - y = x - y"
1.68 + by (rule diff_eq1 [symmetric])
1.69 +
1.70 +lemma (in vectorspace) diff_closed [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y \<in> V"
1.71 + by (simp add: diff_eq1 negate_eq1)
1.72 +
1.73 +lemma (in vectorspace) neg_closed [iff]: "x \<in> V \<Longrightarrow> - x \<in> V"
1.74 + by (simp add: negate_eq1)
1.75 +
1.76 +lemma (in vectorspace) add_left_commute:
1.77 + "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)"
1.78 +proof -
1.79 + assume xyz: "x \<in> V" "y \<in> V" "z \<in> V"
1.80 + then have "x + (y + z) = (x + y) + z"
1.81 + by (simp only: add_assoc)
1.82 + also from xyz have "\<dots> = (y + x) + z" by (simp only: add_commute)
1.83 + also from xyz have "\<dots> = y + (x + z)" by (simp only: add_assoc)
1.84 + finally show ?thesis .
1.85 +qed
1.86 +
1.87 +theorems (in vectorspace) add_ac =
1.88 + add_assoc add_commute add_left_commute
1.89 +
1.90 +
1.91 +text {* The existence of the zero element of a vector space
1.92 + follows from the non-emptiness of carrier set. *}
1.93 +
1.94 +lemma (in vectorspace) zero [iff]: "0 \<in> V"
1.95 +proof -
1.96 + from non_empty obtain x where x: "x \<in> V" by blast
1.97 + then have "0 = x - x" by (rule diff_self [symmetric])
1.98 + also from x x have "\<dots> \<in> V" by (rule diff_closed)
1.99 + finally show ?thesis .
1.100 +qed
1.101 +
1.102 +lemma (in vectorspace) add_zero_right [simp]:
1.103 + "x \<in> V \<Longrightarrow> x + 0 = x"
1.104 +proof -
1.105 + assume x: "x \<in> V"
1.106 + from this and zero have "x + 0 = 0 + x" by (rule add_commute)
1.107 + also from x have "\<dots> = x" by (rule add_zero_left)
1.108 + finally show ?thesis .
1.109 +qed
1.110 +
1.111 +lemma (in vectorspace) mult_assoc2:
1.112 + "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = (a * b) \<cdot> x"
1.113 + by (simp only: mult_assoc)
1.114 +
1.115 +lemma (in vectorspace) diff_mult_distrib1:
1.116 + "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<cdot> (x - y) = a \<cdot> x - a \<cdot> y"
1.117 + by (simp add: diff_eq1 negate_eq1 add_mult_distrib1 mult_assoc2)
1.118 +
1.119 +lemma (in vectorspace) diff_mult_distrib2:
1.120 + "x \<in> V \<Longrightarrow> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)"
1.121 +proof -
1.122 + assume x: "x \<in> V"
1.123 + have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
1.124 + by (simp add: real_diff_def)
1.125 + also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x"
1.126 + by (rule add_mult_distrib2)
1.127 + also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)"
1.128 + by (simp add: negate_eq1 mult_assoc2)
1.129 + also from x have "\<dots> = a \<cdot> x - (b \<cdot> x)"
1.130 + by (simp add: diff_eq1)
1.131 + finally show ?thesis .
1.132 +qed
1.133 +
1.134 +lemmas (in vectorspace) distrib =
1.135 + add_mult_distrib1 add_mult_distrib2
1.136 + diff_mult_distrib1 diff_mult_distrib2
1.137 +
1.138 +
1.139 +text {* \medskip Further derived laws: *}
1.140 +
1.141 +lemma (in vectorspace) mult_zero_left [simp]:
1.142 + "x \<in> V \<Longrightarrow> 0 \<cdot> x = 0"
1.143 +proof -
1.144 + assume x: "x \<in> V"
1.145 + have "0 \<cdot> x = (1 - 1) \<cdot> x" by simp
1.146 + also have "\<dots> = (1 + - 1) \<cdot> x" by simp
1.147 + also from x have "\<dots> = 1 \<cdot> x + (- 1) \<cdot> x"
1.148 + by (rule add_mult_distrib2)
1.149 + also from x have "\<dots> = x + (- 1) \<cdot> x" by simp
1.150 + also from x have "\<dots> = x + - x" by (simp add: negate_eq2a)
1.151 + also from x have "\<dots> = x - x" by (simp add: diff_eq2)
1.152 + also from x have "\<dots> = 0" by simp
1.153 + finally show ?thesis .
1.154 +qed
1.155 +
1.156 +lemma (in vectorspace) mult_zero_right [simp]:
1.157 + "a \<cdot> 0 = (0::'a)"
1.158 +proof -
1.159 + have "a \<cdot> 0 = a \<cdot> (0 - (0::'a))" by simp
1.160 + also have "\<dots> = a \<cdot> 0 - a \<cdot> 0"
1.161 + by (rule diff_mult_distrib1) simp_all
1.162 + also have "\<dots> = 0" by simp
1.163 + finally show ?thesis .
1.164 +qed
1.165 +
1.166 +lemma (in vectorspace) minus_mult_cancel [simp]:
1.167 + "x \<in> V \<Longrightarrow> (- a) \<cdot> - x = a \<cdot> x"
1.168 + by (simp add: negate_eq1 mult_assoc2)
1.169 +
1.170 +lemma (in vectorspace) add_minus_left_eq_diff:
1.171 + "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + y = y - x"
1.172 +proof -
1.173 + assume xy: "x \<in> V" "y \<in> V"
1.174 + then have "- x + y = y + - x" by (simp add: add_commute)
1.175 + also from xy have "\<dots> = y - x" by (simp add: diff_eq1)
1.176 + finally show ?thesis .
1.177 +qed
1.178 +
1.179 +lemma (in vectorspace) add_minus [simp]:
1.180 + "x \<in> V \<Longrightarrow> x + - x = 0"
1.181 + by (simp add: diff_eq2)
1.182 +
1.183 +lemma (in vectorspace) add_minus_left [simp]:
1.184 + "x \<in> V \<Longrightarrow> - x + x = 0"
1.185 + by (simp add: diff_eq2 add_commute)
1.186 +
1.187 +lemma (in vectorspace) minus_minus [simp]:
1.188 + "x \<in> V \<Longrightarrow> - (- x) = x"
1.189 + by (simp add: negate_eq1 mult_assoc2)
1.190 +
1.191 +lemma (in vectorspace) minus_zero [simp]:
1.192 + "- (0::'a) = 0"
1.193 + by (simp add: negate_eq1)
1.194 +
1.195 +lemma (in vectorspace) minus_zero_iff [simp]:
1.196 + "x \<in> V \<Longrightarrow> (- x = 0) = (x = 0)"
1.197 +proof
1.198 + assume x: "x \<in> V"
1.199 + {
1.200 + from x have "x = - (- x)" by (simp add: minus_minus)
1.201 + also assume "- x = 0"
1.202 + also have "- \<dots> = 0" by (rule minus_zero)
1.203 + finally show "x = 0" .
1.204 + next
1.205 + assume "x = 0"
1.206 + then show "- x = 0" by simp
1.207 + }
1.208 +qed
1.209 +
1.210 +lemma (in vectorspace) add_minus_cancel [simp]:
1.211 + "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + (- x + y) = y"
1.212 + by (simp add: add_assoc [symmetric] del: add_commute)
1.213 +
1.214 +lemma (in vectorspace) minus_add_cancel [simp]:
1.215 + "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + (x + y) = y"
1.216 + by (simp add: add_assoc [symmetric] del: add_commute)
1.217 +
1.218 +lemma (in vectorspace) minus_add_distrib [simp]:
1.219 + "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - (x + y) = - x + - y"
1.220 + by (simp add: negate_eq1 add_mult_distrib1)
1.221 +
1.222 +lemma (in vectorspace) diff_zero [simp]:
1.223 + "x \<in> V \<Longrightarrow> x - 0 = x"
1.224 + by (simp add: diff_eq1)
1.225 +
1.226 +lemma (in vectorspace) diff_zero_right [simp]:
1.227 + "x \<in> V \<Longrightarrow> 0 - x = - x"
1.228 + by (simp add: diff_eq1)
1.229 +
1.230 +lemma (in vectorspace) add_left_cancel:
1.231 + "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x + y = x + z) = (y = z)"
1.232 +proof
1.233 + assume x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V"
1.234 + {
1.235 + from y have "y = 0 + y" by simp
1.236 + also from x y have "\<dots> = (- x + x) + y" by simp
1.237 + also from x y have "\<dots> = - x + (x + y)"
1.238 + by (simp add: add_assoc neg_closed)
1.239 + also assume "x + y = x + z"
1.240 + also from x z have "- x + (x + z) = - x + x + z"
1.241 + by (simp add: add_assoc [symmetric] neg_closed)
1.242 + also from x z have "\<dots> = z" by simp
1.243 + finally show "y = z" .
1.244 + next
1.245 + assume "y = z"
1.246 + then show "x + y = x + z" by (simp only:)
1.247 + }
1.248 +qed
1.249 +
1.250 +lemma (in vectorspace) add_right_cancel:
1.251 + "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (y + x = z + x) = (y = z)"
1.252 + by (simp only: add_commute add_left_cancel)
1.253 +
1.254 +lemma (in vectorspace) add_assoc_cong:
1.255 + "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x' \<in> V \<Longrightarrow> y' \<in> V \<Longrightarrow> z \<in> V
1.256 + \<Longrightarrow> x + y = x' + y' \<Longrightarrow> x + (y + z) = x' + (y' + z)"
1.257 + by (simp only: add_assoc [symmetric])
1.258 +
1.259 +lemma (in vectorspace) mult_left_commute:
1.260 + "x \<in> V \<Longrightarrow> a \<cdot> b \<cdot> x = b \<cdot> a \<cdot> x"
1.261 + by (simp add: real_mult_commute mult_assoc2)
1.262 +
1.263 +lemma (in vectorspace) mult_zero_uniq:
1.264 + "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> a \<cdot> x = 0 \<Longrightarrow> a = 0"
1.265 +proof (rule classical)
1.266 + assume a: "a \<noteq> 0"
1.267 + assume x: "x \<in> V" "x \<noteq> 0" and ax: "a \<cdot> x = 0"
1.268 + from x a have "x = (inverse a * a) \<cdot> x" by simp
1.269 + also from `x \<in> V` have "\<dots> = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc)
1.270 + also from ax have "\<dots> = inverse a \<cdot> 0" by simp
1.271 + also have "\<dots> = 0" by simp
1.272 + finally have "x = 0" .
1.273 + with `x \<noteq> 0` show "a = 0" by contradiction
1.274 +qed
1.275 +
1.276 +lemma (in vectorspace) mult_left_cancel:
1.277 + "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> (a \<cdot> x = a \<cdot> y) = (x = y)"
1.278 +proof
1.279 + assume x: "x \<in> V" and y: "y \<in> V" and a: "a \<noteq> 0"
1.280 + from x have "x = 1 \<cdot> x" by simp
1.281 + also from a have "\<dots> = (inverse a * a) \<cdot> x" by simp
1.282 + also from x have "\<dots> = inverse a \<cdot> (a \<cdot> x)"
1.283 + by (simp only: mult_assoc)
1.284 + also assume "a \<cdot> x = a \<cdot> y"
1.285 + also from a y have "inverse a \<cdot> \<dots> = y"
1.286 + by (simp add: mult_assoc2)
1.287 + finally show "x = y" .
1.288 +next
1.289 + assume "x = y"
1.290 + then show "a \<cdot> x = a \<cdot> y" by (simp only:)
1.291 +qed
1.292 +
1.293 +lemma (in vectorspace) mult_right_cancel:
1.294 + "x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> (a \<cdot> x = b \<cdot> x) = (a = b)"
1.295 +proof
1.296 + assume x: "x \<in> V" and neq: "x \<noteq> 0"
1.297 + {
1.298 + from x have "(a - b) \<cdot> x = a \<cdot> x - b \<cdot> x"
1.299 + by (simp add: diff_mult_distrib2)
1.300 + also assume "a \<cdot> x = b \<cdot> x"
1.301 + with x have "a \<cdot> x - b \<cdot> x = 0" by simp
1.302 + finally have "(a - b) \<cdot> x = 0" .
1.303 + with x neq have "a - b = 0" by (rule mult_zero_uniq)
1.304 + then show "a = b" by simp
1.305 + next
1.306 + assume "a = b"
1.307 + then show "a \<cdot> x = b \<cdot> x" by (simp only:)
1.308 + }
1.309 +qed
1.310 +
1.311 +lemma (in vectorspace) eq_diff_eq:
1.312 + "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x = z - y) = (x + y = z)"
1.313 +proof
1.314 + assume x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V"
1.315 + {
1.316 + assume "x = z - y"
1.317 + then have "x + y = z - y + y" by simp
1.318 + also from y z have "\<dots> = z + - y + y"
1.319 + by (simp add: diff_eq1)
1.320 + also have "\<dots> = z + (- y + y)"
1.321 + by (rule add_assoc) (simp_all add: y z)
1.322 + also from y z have "\<dots> = z + 0"
1.323 + by (simp only: add_minus_left)
1.324 + also from z have "\<dots> = z"
1.325 + by (simp only: add_zero_right)
1.326 + finally show "x + y = z" .
1.327 + next
1.328 + assume "x + y = z"
1.329 + then have "z - y = (x + y) - y" by simp
1.330 + also from x y have "\<dots> = x + y + - y"
1.331 + by (simp add: diff_eq1)
1.332 + also have "\<dots> = x + (y + - y)"
1.333 + by (rule add_assoc) (simp_all add: x y)
1.334 + also from x y have "\<dots> = x" by simp
1.335 + finally show "x = z - y" ..
1.336 + }
1.337 +qed
1.338 +
1.339 +lemma (in vectorspace) add_minus_eq_minus:
1.340 + "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y = 0 \<Longrightarrow> x = - y"
1.341 +proof -
1.342 + assume x: "x \<in> V" and y: "y \<in> V"
1.343 + from x y have "x = (- y + y) + x" by simp
1.344 + also from x y have "\<dots> = - y + (x + y)" by (simp add: add_ac)
1.345 + also assume "x + y = 0"
1.346 + also from y have "- y + 0 = - y" by simp
1.347 + finally show "x = - y" .
1.348 +qed
1.349 +
1.350 +lemma (in vectorspace) add_minus_eq:
1.351 + "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y = 0 \<Longrightarrow> x = y"
1.352 +proof -
1.353 + assume x: "x \<in> V" and y: "y \<in> V"
1.354 + assume "x - y = 0"
1.355 + with x y have eq: "x + - y = 0" by (simp add: diff_eq1)
1.356 + with _ _ have "x = - (- y)"
1.357 + by (rule add_minus_eq_minus) (simp_all add: x y)
1.358 + with x y show "x = y" by simp
1.359 +qed
1.360 +
1.361 +lemma (in vectorspace) add_diff_swap:
1.362 + "a \<in> V \<Longrightarrow> b \<in> V \<Longrightarrow> c \<in> V \<Longrightarrow> d \<in> V \<Longrightarrow> a + b = c + d
1.363 + \<Longrightarrow> a - c = d - b"
1.364 +proof -
1.365 + assume vs: "a \<in> V" "b \<in> V" "c \<in> V" "d \<in> V"
1.366 + and eq: "a + b = c + d"
1.367 + then have "- c + (a + b) = - c + (c + d)"
1.368 + by (simp add: add_left_cancel)
1.369 + also have "\<dots> = d" using `c \<in> V` `d \<in> V` by (rule minus_add_cancel)
1.370 + finally have eq: "- c + (a + b) = d" .
1.371 + from vs have "a - c = (- c + (a + b)) + - b"
1.372 + by (simp add: add_ac diff_eq1)
1.373 + also from vs eq have "\<dots> = d + - b"
1.374 + by (simp add: add_right_cancel)
1.375 + also from vs have "\<dots> = d - b" by (simp add: diff_eq2)
1.376 + finally show "a - c = d - b" .
1.377 +qed
1.378 +
1.379 +lemma (in vectorspace) vs_add_cancel_21:
1.380 + "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> u \<in> V
1.381 + \<Longrightarrow> (x + (y + z) = y + u) = (x + z = u)"
1.382 +proof
1.383 + assume vs: "x \<in> V" "y \<in> V" "z \<in> V" "u \<in> V"
1.384 + {
1.385 + from vs have "x + z = - y + y + (x + z)" by simp
1.386 + also have "\<dots> = - y + (y + (x + z))"
1.387 + by (rule add_assoc) (simp_all add: vs)
1.388 + also from vs have "y + (x + z) = x + (y + z)"
1.389 + by (simp add: add_ac)
1.390 + also assume "x + (y + z) = y + u"
1.391 + also from vs have "- y + (y + u) = u" by simp
1.392 + finally show "x + z = u" .
1.393 + next
1.394 + assume "x + z = u"
1.395 + with vs show "x + (y + z) = y + u"
1.396 + by (simp only: add_left_commute [of x])
1.397 + }
1.398 +qed
1.399 +
1.400 +lemma (in vectorspace) add_cancel_end:
1.401 + "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> (x + (y + z) = y) = (x = - z)"
1.402 +proof
1.403 + assume vs: "x \<in> V" "y \<in> V" "z \<in> V"
1.404 + {
1.405 + assume "x + (y + z) = y"
1.406 + with vs have "(x + z) + y = 0 + y"
1.407 + by (simp add: add_ac)
1.408 + with vs have "x + z = 0"
1.409 + by (simp only: add_right_cancel add_closed zero)
1.410 + with vs show "x = - z" by (simp add: add_minus_eq_minus)
1.411 + next
1.412 + assume eq: "x = - z"
1.413 + then have "x + (y + z) = - z + (y + z)" by simp
1.414 + also have "\<dots> = y + (- z + z)"
1.415 + by (rule add_left_commute) (simp_all add: vs)
1.416 + also from vs have "\<dots> = y" by simp
1.417 + finally show "x + (y + z) = y" .
1.418 + }
1.419 +qed
1.420 +
1.421 +end