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