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.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.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.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.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.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.122      also assume "x + y = x + z"
1.123      also from x z have "- x + (x + z) = - x + x + z"
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.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.176 -    also have "... = z + (- y + y)"
1.177 +    also have "\<dots> = z + (- y + y)"
1.179 -    also from y z have "... = z + 0"
1.180 +    also from y z have "\<dots> = z + 0"
1.182 -    also from z have "... = z"
1.183 +    also from z have "\<dots> = z"
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.193 -    also have "... = x + (y + - y)"
1.194 +    also have "\<dots> = x + (y + - 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.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.219 -  also from vs eq have "...  = d + - b"
1.220 +  also from vs eq have "\<dots>  = d + - b"
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.234      also from vs have "y + (x + z) = x + (y + z)"
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)"