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

src/HOL/Real/HahnBanach/VectorSpace.thy

changeset 27612 | d3eb431db035 |

parent 23378 | 1d138d6bb461 |

child 29234 | 60f7fb56f8cd |

1.1 --- a/src/HOL/Real/HahnBanach/VectorSpace.thy Tue Jul 15 16:50:09 2008 +0200 1.2 +++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Tue Jul 15 19:39:37 2008 +0200 1.3 @@ -5,7 +5,9 @@ 1.4 1.5 header {* Vector spaces *} 1.6 1.7 -theory VectorSpace imports Real Bounds Zorn begin 1.8 +theory VectorSpace 1.9 +imports Real Bounds Zorn 1.10 +begin 1.11 1.12 subsection {* Signature *} 1.13 1.14 @@ -71,10 +73,10 @@ 1.15 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> x + (y + z) = y + (x + z)" 1.16 proof - 1.17 assume xyz: "x \<in> V" "y \<in> V" "z \<in> V" 1.18 - hence "x + (y + z) = (x + y) + z" 1.19 + then have "x + (y + z) = (x + y) + z" 1.20 by (simp only: add_assoc) 1.21 - also from xyz have "... = (y + x) + z" by (simp only: add_commute) 1.22 - also from xyz have "... = y + (x + z)" by (simp only: add_assoc) 1.23 + also from xyz have "\<dots> = (y + x) + z" by (simp only: add_commute) 1.24 + also from xyz have "\<dots> = y + (x + z)" by (simp only: add_assoc) 1.25 finally show ?thesis . 1.26 qed 1.27 1.28 @@ -89,7 +91,7 @@ 1.29 proof - 1.30 from non_empty obtain x where x: "x \<in> V" by blast 1.31 then have "0 = x - x" by (rule diff_self [symmetric]) 1.32 - also from x x have "... \<in> V" by (rule diff_closed) 1.33 + also from x x have "\<dots> \<in> V" by (rule diff_closed) 1.34 finally show ?thesis . 1.35 qed 1.36 1.37 @@ -98,7 +100,7 @@ 1.38 proof - 1.39 assume x: "x \<in> V" 1.40 from this and zero have "x + 0 = 0 + x" by (rule add_commute) 1.41 - also from x have "... = x" by (rule add_zero_left) 1.42 + also from x have "\<dots> = x" by (rule add_zero_left) 1.43 finally show ?thesis . 1.44 qed 1.45 1.46 @@ -116,11 +118,11 @@ 1.47 assume x: "x \<in> V" 1.48 have " (a - b) \<cdot> x = (a + - b) \<cdot> x" 1.49 by (simp add: real_diff_def) 1.50 - also from x have "... = a \<cdot> x + (- b) \<cdot> x" 1.51 + also from x have "\<dots> = a \<cdot> x + (- b) \<cdot> x" 1.52 by (rule add_mult_distrib2) 1.53 - also from x have "... = a \<cdot> x + - (b \<cdot> x)" 1.54 + also from x have "\<dots> = a \<cdot> x + - (b \<cdot> x)" 1.55 by (simp add: negate_eq1 mult_assoc2) 1.56 - also from x have "... = a \<cdot> x - (b \<cdot> x)" 1.57 + also from x have "\<dots> = a \<cdot> x - (b \<cdot> x)" 1.58 by (simp add: diff_eq1) 1.59 finally show ?thesis . 1.60 qed 1.61 @@ -137,13 +139,13 @@ 1.62 proof - 1.63 assume x: "x \<in> V" 1.64 have "0 \<cdot> x = (1 - 1) \<cdot> x" by simp 1.65 - also have "... = (1 + - 1) \<cdot> x" by simp 1.66 - also from x have "... = 1 \<cdot> x + (- 1) \<cdot> x" 1.67 + also have "\<dots> = (1 + - 1) \<cdot> x" by simp 1.68 + also from x have "\<dots> = 1 \<cdot> x + (- 1) \<cdot> x" 1.69 by (rule add_mult_distrib2) 1.70 - also from x have "... = x + (- 1) \<cdot> x" by simp 1.71 - also from x have "... = x + - x" by (simp add: negate_eq2a) 1.72 - also from x have "... = x - x" by (simp add: diff_eq2) 1.73 - also from x have "... = 0" by simp 1.74 + also from x have "\<dots> = x + (- 1) \<cdot> x" by simp 1.75 + also from x have "\<dots> = x + - x" by (simp add: negate_eq2a) 1.76 + also from x have "\<dots> = x - x" by (simp add: diff_eq2) 1.77 + also from x have "\<dots> = 0" by simp 1.78 finally show ?thesis . 1.79 qed 1.80 1.81 @@ -151,9 +153,9 @@ 1.82 "a \<cdot> 0 = (0::'a)" 1.83 proof - 1.84 have "a \<cdot> 0 = a \<cdot> (0 - (0::'a))" by simp 1.85 - also have "... = a \<cdot> 0 - a \<cdot> 0" 1.86 + also have "\<dots> = a \<cdot> 0 - a \<cdot> 0" 1.87 by (rule diff_mult_distrib1) simp_all 1.88 - also have "... = 0" by simp 1.89 + also have "\<dots> = 0" by simp 1.90 finally show ?thesis . 1.91 qed 1.92 1.93 @@ -165,8 +167,8 @@ 1.94 "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + y = y - x" 1.95 proof - 1.96 assume xy: "x \<in> V" "y \<in> V" 1.97 - hence "- x + y = y + - x" by (simp add: add_commute) 1.98 - also from xy have "... = y - x" by (simp add: diff_eq1) 1.99 + then have "- x + y = y + - x" by (simp add: add_commute) 1.100 + also from xy have "\<dots> = y - x" by (simp add: diff_eq1) 1.101 finally show ?thesis . 1.102 qed 1.103 1.104 @@ -193,7 +195,7 @@ 1.105 { 1.106 from x have "x = - (- x)" by (simp add: minus_minus) 1.107 also assume "- x = 0" 1.108 - also have "- ... = 0" by (rule minus_zero) 1.109 + also have "- \<dots> = 0" by (rule minus_zero) 1.110 finally show "x = 0" . 1.111 next 1.112 assume "x = 0" 1.113 @@ -227,13 +229,13 @@ 1.114 assume x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V" 1.115 { 1.116 from y have "y = 0 + y" by simp 1.117 - also from x y have "... = (- x + x) + y" by simp 1.118 - also from x y have "... = - x + (x + y)" 1.119 + also from x y have "\<dots> = (- x + x) + y" by simp 1.120 + also from x y have "\<dots> = - x + (x + y)" 1.121 by (simp add: add_assoc neg_closed) 1.122 also assume "x + y = x + z" 1.123 also from x z have "- x + (x + z) = - x + x + z" 1.124 by (simp add: add_assoc [symmetric] neg_closed) 1.125 - also from x z have "... = z" by simp 1.126 + also from x z have "\<dots> = z" by simp 1.127 finally show "y = z" . 1.128 next 1.129 assume "y = z" 1.130 @@ -260,9 +262,9 @@ 1.131 assume a: "a \<noteq> 0" 1.132 assume x: "x \<in> V" "x \<noteq> 0" and ax: "a \<cdot> x = 0" 1.133 from x a have "x = (inverse a * a) \<cdot> x" by simp 1.134 - also from `x \<in> V` have "... = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc) 1.135 - also from ax have "... = inverse a \<cdot> 0" by simp 1.136 - also have "... = 0" by simp 1.137 + also from `x \<in> V` have "\<dots> = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc) 1.138 + also from ax have "\<dots> = inverse a \<cdot> 0" by simp 1.139 + also have "\<dots> = 0" by simp 1.140 finally have "x = 0" . 1.141 with `x \<noteq> 0` show "a = 0" by contradiction 1.142 qed 1.143 @@ -272,11 +274,11 @@ 1.144 proof 1.145 assume x: "x \<in> V" and y: "y \<in> V" and a: "a \<noteq> 0" 1.146 from x have "x = 1 \<cdot> x" by simp 1.147 - also from a have "... = (inverse a * a) \<cdot> x" by simp 1.148 - also from x have "... = inverse a \<cdot> (a \<cdot> x)" 1.149 + also from a have "\<dots> = (inverse a * a) \<cdot> x" by simp 1.150 + also from x have "\<dots> = inverse a \<cdot> (a \<cdot> x)" 1.151 by (simp only: mult_assoc) 1.152 also assume "a \<cdot> x = a \<cdot> y" 1.153 - also from a y have "inverse a \<cdot> ... = y" 1.154 + also from a y have "inverse a \<cdot> \<dots> = y" 1.155 by (simp add: mult_assoc2) 1.156 finally show "x = y" . 1.157 next 1.158 @@ -295,7 +297,7 @@ 1.159 with x have "a \<cdot> x - b \<cdot> x = 0" by simp 1.160 finally have "(a - b) \<cdot> x = 0" . 1.161 with x neq have "a - b = 0" by (rule mult_zero_uniq) 1.162 - thus "a = b" by simp 1.163 + then show "a = b" by simp 1.164 next 1.165 assume "a = b" 1.166 then show "a \<cdot> x = b \<cdot> x" by (simp only:) 1.167 @@ -308,24 +310,24 @@ 1.168 assume x: "x \<in> V" and y: "y \<in> V" and z: "z \<in> V" 1.169 { 1.170 assume "x = z - y" 1.171 - hence "x + y = z - y + y" by simp 1.172 - also from y z have "... = z + - y + y" 1.173 + then have "x + y = z - y + y" by simp 1.174 + also from y z have "\<dots> = z + - y + y" 1.175 by (simp add: diff_eq1) 1.176 - also have "... = z + (- y + y)" 1.177 + also have "\<dots> = z + (- y + y)" 1.178 by (rule add_assoc) (simp_all add: y z) 1.179 - also from y z have "... = z + 0" 1.180 + also from y z have "\<dots> = z + 0" 1.181 by (simp only: add_minus_left) 1.182 - also from z have "... = z" 1.183 + also from z have "\<dots> = z" 1.184 by (simp only: add_zero_right) 1.185 finally show "x + y = z" . 1.186 next 1.187 assume "x + y = z" 1.188 - hence "z - y = (x + y) - y" by simp 1.189 - also from x y have "... = x + y + - y" 1.190 + then have "z - y = (x + y) - y" by simp 1.191 + also from x y have "\<dots> = x + y + - y" 1.192 by (simp add: diff_eq1) 1.193 - also have "... = x + (y + - y)" 1.194 + also have "\<dots> = x + (y + - y)" 1.195 by (rule add_assoc) (simp_all add: x y) 1.196 - also from x y have "... = x" by simp 1.197 + also from x y have "\<dots> = x" by simp 1.198 finally show "x = z - y" .. 1.199 } 1.200 qed 1.201 @@ -335,7 +337,7 @@ 1.202 proof - 1.203 assume x: "x \<in> V" and y: "y \<in> V" 1.204 from x y have "x = (- y + y) + x" by simp 1.205 - also from x y have "... = - y + (x + y)" by (simp add: add_ac) 1.206 + also from x y have "\<dots> = - y + (x + y)" by (simp add: add_ac) 1.207 also assume "x + y = 0" 1.208 also from y have "- y + 0 = - y" by simp 1.209 finally show "x = - y" . 1.210 @@ -360,13 +362,13 @@ 1.211 and eq: "a + b = c + d" 1.212 then have "- c + (a + b) = - c + (c + d)" 1.213 by (simp add: add_left_cancel) 1.214 - also have "... = d" using `c \<in> V` `d \<in> V` by (rule minus_add_cancel) 1.215 + also have "\<dots> = d" using `c \<in> V` `d \<in> V` by (rule minus_add_cancel) 1.216 finally have eq: "- c + (a + b) = d" . 1.217 from vs have "a - c = (- c + (a + b)) + - b" 1.218 by (simp add: add_ac diff_eq1) 1.219 - also from vs eq have "... = d + - b" 1.220 + also from vs eq have "\<dots> = d + - b" 1.221 by (simp add: add_right_cancel) 1.222 - also from vs have "... = d - b" by (simp add: diff_eq2) 1.223 + also from vs have "\<dots> = d - b" by (simp add: diff_eq2) 1.224 finally show "a - c = d - b" . 1.225 qed 1.226 1.227 @@ -377,7 +379,7 @@ 1.228 assume vs: "x \<in> V" "y \<in> V" "z \<in> V" "u \<in> V" 1.229 { 1.230 from vs have "x + z = - y + y + (x + z)" by simp 1.231 - also have "... = - y + (y + (x + z))" 1.232 + also have "\<dots> = - y + (y + (x + z))" 1.233 by (rule add_assoc) (simp_all add: vs) 1.234 also from vs have "y + (x + z) = x + (y + z)" 1.235 by (simp add: add_ac) 1.236 @@ -404,10 +406,10 @@ 1.237 with vs show "x = - z" by (simp add: add_minus_eq_minus) 1.238 next 1.239 assume eq: "x = - z" 1.240 - hence "x + (y + z) = - z + (y + z)" by simp 1.241 - also have "... = y + (- z + z)" 1.242 + then have "x + (y + z) = - z + (y + z)" by simp 1.243 + also have "\<dots> = y + (- z + z)" 1.244 by (rule add_left_commute) (simp_all add: vs) 1.245 - also from vs have "... = y" by simp 1.246 + also from vs have "\<dots> = y" by simp 1.247 finally show "x + (y + z) = y" . 1.248 } 1.249 qed