src/HOL/Hahn_Banach/Vector_Space.thy
 author wenzelm Tue Oct 21 10:58:19 2014 +0200 (2014-10-21) changeset 58744 c434e37f290e parent 57512 cc97b347b301 child 58745 5d452cf4bce7 permissions -rw-r--r--
update_cartouches;
 wenzelm@31795  1 (* Title: HOL/Hahn_Banach/Vector_Space.thy  wenzelm@7917  2  Author: Gertrud Bauer, TU Munich  wenzelm@7917  3 *)  wenzelm@7917  4 wenzelm@58744  5 header \Vector spaces\  wenzelm@7917  6 wenzelm@31795  7 theory Vector_Space  blanchet@55018  8 imports Complex_Main Bounds  wenzelm@27612  9 begin  wenzelm@7917  10 wenzelm@58744  11 subsection \Signature\  wenzelm@7917  12 wenzelm@58744  13 text \  wenzelm@10687  14  For the definition of real vector spaces a type @{typ 'a} of the  wenzelm@10687  15  sort @{text "{plus, minus, zero}"} is considered, on which a real  wenzelm@10687  16  scalar multiplication @{text \} is declared.  wenzelm@58744  17 \  wenzelm@7917  18 wenzelm@7917  19 consts  wenzelm@10687  20  prod :: "real \ 'a::{plus, minus, zero} \ 'a" (infixr "'(*')" 70)  wenzelm@7917  21 wenzelm@21210  22 notation (xsymbols)  wenzelm@19736  23  prod (infixr "\" 70)  wenzelm@21210  24 notation (HTML output)  wenzelm@19736  25  prod (infixr "\" 70)  wenzelm@7917  26 wenzelm@7917  27 wenzelm@58744  28 subsection \Vector space laws\  wenzelm@7917  29 wenzelm@58744  30 text \  wenzelm@10687  31  A \emph{vector space} is a non-empty set @{text V} of elements from  wenzelm@10687  32  @{typ 'a} with the following vector space laws: The set @{text V} is  wenzelm@10687  33  closed under addition and scalar multiplication, addition is  wenzelm@10687  34  associative and commutative; @{text "- x"} is the inverse of @{text  wenzelm@10687  35  x} w.~r.~t.~addition and @{text 0} is the neutral element of  wenzelm@10687  36  addition. Addition and multiplication are distributive; scalar  paulson@12018  37  multiplication is associative and the real number @{text "1"} is  wenzelm@10687  38  the neutral element of scalar multiplication.  wenzelm@58744  39 \  wenzelm@7917  40 wenzelm@46867  41 locale vectorspace =  wenzelm@46867  42  fixes V  wenzelm@13515  43  assumes non_empty [iff, intro?]: "V \ {}"  wenzelm@13515  44  and add_closed [iff]: "x \ V \ y \ V \ x + y \ V"  wenzelm@13515  45  and mult_closed [iff]: "x \ V \ a \ x \ V"  wenzelm@13515  46  and add_assoc: "x \ V \ y \ V \ z \ V \ (x + y) + z = x + (y + z)"  wenzelm@13515  47  and add_commute: "x \ V \ y \ V \ x + y = y + x"  wenzelm@13515  48  and diff_self [simp]: "x \ V \ x - x = 0"  wenzelm@13515  49  and add_zero_left [simp]: "x \ V \ 0 + x = x"  wenzelm@13515  50  and add_mult_distrib1: "x \ V \ y \ V \ a \ (x + y) = a \ x + a \ y"  wenzelm@13515  51  and add_mult_distrib2: "x \ V \ (a + b) \ x = a \ x + b \ x"  wenzelm@13515  52  and mult_assoc: "x \ V \ (a * b) \ x = a \ (b \ x)"  wenzelm@13515  53  and mult_1 [simp]: "x \ V \ 1 \ x = x"  wenzelm@13515  54  and negate_eq1: "x \ V \ - x = (- 1) \ x"  wenzelm@13515  55  and diff_eq1: "x \ V \ y \ V \ x - y = x + - y"  wenzelm@44887  56 begin  wenzelm@7917  57 wenzelm@44887  58 lemma negate_eq2: "x \ V \ (- 1) \ x = - x"  wenzelm@13515  59  by (rule negate_eq1 [symmetric])  fleuriot@9013  60 wenzelm@44887  61 lemma negate_eq2a: "x \ V \ -1 \ x = - x"  wenzelm@13515  62  by (simp add: negate_eq1)  wenzelm@7917  63 wenzelm@44887  64 lemma diff_eq2: "x \ V \ y \ V \ x + - y = x - y"  wenzelm@13515  65  by (rule diff_eq1 [symmetric])  wenzelm@7917  66 wenzelm@44887  67 lemma diff_closed [iff]: "x \ V \ y \ V \ x - y \ V"  wenzelm@9035  68  by (simp add: diff_eq1 negate_eq1)  wenzelm@7917  69 wenzelm@44887  70 lemma neg_closed [iff]: "x \ V \ - x \ V"  wenzelm@9035  71  by (simp add: negate_eq1)  wenzelm@7917  72 wenzelm@44887  73 lemma add_left_commute: "x \ V \ y \ V \ z \ V \ x + (y + z) = y + (x + z)"  wenzelm@9035  74 proof -  wenzelm@13515  75  assume xyz: "x \ V" "y \ V" "z \ V"  wenzelm@27612  76  then have "x + (y + z) = (x + y) + z"  wenzelm@13515  77  by (simp only: add_assoc)  wenzelm@27612  78  also from xyz have "\ = (y + x) + z" by (simp only: add_commute)  wenzelm@27612  79  also from xyz have "\ = y + (x + z)" by (simp only: add_assoc)  wenzelm@9035  80  finally show ?thesis .  wenzelm@9035  81 qed  wenzelm@7917  82 wenzelm@44887  83 theorems add_ac = add_assoc add_commute add_left_commute  wenzelm@7917  84 wenzelm@7917  85 wenzelm@58744  86 text \The existence of the zero element of a vector space  wenzelm@58744  87  follows from the non-emptiness of carrier set.\  wenzelm@7917  88 wenzelm@44887  89 lemma zero [iff]: "0 \ V"  wenzelm@10687  90 proof -  wenzelm@13515  91  from non_empty obtain x where x: "x \ V" by blast  wenzelm@13515  92  then have "0 = x - x" by (rule diff_self [symmetric])  wenzelm@27612  93  also from x x have "\ \ V" by (rule diff_closed)  wenzelm@11472  94  finally show ?thesis .  wenzelm@9035  95 qed  wenzelm@7917  96 wenzelm@44887  97 lemma add_zero_right [simp]: "x \ V \ x + 0 = x"  wenzelm@9035  98 proof -  wenzelm@13515  99  assume x: "x \ V"  wenzelm@13515  100  from this and zero have "x + 0 = 0 + x" by (rule add_commute)  wenzelm@27612  101  also from x have "\ = x" by (rule add_zero_left)  wenzelm@9035  102  finally show ?thesis .  wenzelm@9035  103 qed  wenzelm@7917  104 wenzelm@44887  105 lemma mult_assoc2: "x \ V \ a \ b \ x = (a * b) \ x"  wenzelm@13515  106  by (simp only: mult_assoc)  wenzelm@7917  107 wenzelm@44887  108 lemma diff_mult_distrib1: "x \ V \ y \ V \ a \ (x - y) = a \ x - a \ y"  wenzelm@13515  109  by (simp add: diff_eq1 negate_eq1 add_mult_distrib1 mult_assoc2)  wenzelm@7917  110 wenzelm@44887  111 lemma diff_mult_distrib2: "x \ V \ (a - b) \ x = a \ x - (b \ x)"  wenzelm@9035  112 proof -  wenzelm@13515  113  assume x: "x \ V"  wenzelm@10687  114  have " (a - b) \ x = (a + - b) \ x"  haftmann@54230  115  by simp  wenzelm@27612  116  also from x have "\ = a \ x + (- b) \ x"  wenzelm@13515  117  by (rule add_mult_distrib2)  wenzelm@27612  118  also from x have "\ = a \ x + - (b \ x)"  wenzelm@13515  119  by (simp add: negate_eq1 mult_assoc2)  wenzelm@27612  120  also from x have "\ = a \ x - (b \ x)"  wenzelm@13515  121  by (simp add: diff_eq1)  wenzelm@9035  122  finally show ?thesis .  wenzelm@9035  123 qed  wenzelm@7917  124 wenzelm@44887  125 lemmas distrib =  wenzelm@13515  126  add_mult_distrib1 add_mult_distrib2  wenzelm@13515  127  diff_mult_distrib1 diff_mult_distrib2  wenzelm@13515  128 wenzelm@10687  129 wenzelm@58744  130 text \\medskip Further derived laws:\  wenzelm@7917  131 wenzelm@44887  132 lemma mult_zero_left [simp]: "x \ V \ 0 \ x = 0"  wenzelm@9035  133 proof -  wenzelm@13515  134  assume x: "x \ V"  wenzelm@13515  135  have "0 \ x = (1 - 1) \ x" by simp  wenzelm@27612  136  also have "\ = (1 + - 1) \ x" by simp  wenzelm@27612  137  also from x have "\ = 1 \ x + (- 1) \ x"  wenzelm@13515  138  by (rule add_mult_distrib2)  wenzelm@27612  139  also from x have "\ = x + (- 1) \ x" by simp  wenzelm@27612  140  also from x have "\ = x + - x" by (simp add: negate_eq2a)  wenzelm@27612  141  also from x have "\ = x - x" by (simp add: diff_eq2)  wenzelm@27612  142  also from x have "\ = 0" by simp  wenzelm@9035  143  finally show ?thesis .  wenzelm@9035  144 qed  wenzelm@7917  145 wenzelm@44887  146 lemma mult_zero_right [simp]: "a \ 0 = (0::'a)"  wenzelm@9035  147 proof -  wenzelm@13515  148  have "a \ 0 = a \ (0 - (0::'a))" by simp  wenzelm@27612  149  also have "\ = a \ 0 - a \ 0"  wenzelm@13515  150  by (rule diff_mult_distrib1) simp_all  wenzelm@27612  151  also have "\ = 0" by simp  wenzelm@9035  152  finally show ?thesis .  wenzelm@9035  153 qed  wenzelm@7917  154 wenzelm@44887  155 lemma minus_mult_cancel [simp]: "x \ V \ (- a) \ - x = a \ x"  wenzelm@13515  156  by (simp add: negate_eq1 mult_assoc2)  wenzelm@7917  157 wenzelm@44887  158 lemma add_minus_left_eq_diff: "x \ V \ y \ V \ - x + y = y - x"  wenzelm@10687  159 proof -  wenzelm@13515  160  assume xy: "x \ V" "y \ V"  wenzelm@27612  161  then have "- x + y = y + - x" by (simp add: add_commute)  wenzelm@27612  162  also from xy have "\ = y - x" by (simp add: diff_eq1)  wenzelm@9035  163  finally show ?thesis .  wenzelm@9035  164 qed  wenzelm@7917  165 wenzelm@44887  166 lemma add_minus [simp]: "x \ V \ x + - x = 0"  wenzelm@13515  167  by (simp add: diff_eq2)  wenzelm@7917  168 wenzelm@44887  169 lemma add_minus_left [simp]: "x \ V \ - x + x = 0"  wenzelm@13515  170  by (simp add: diff_eq2 add_commute)  wenzelm@7917  171 wenzelm@44887  172 lemma minus_minus [simp]: "x \ V \ - (- x) = x"  wenzelm@13515  173  by (simp add: negate_eq1 mult_assoc2)  wenzelm@13515  174 wenzelm@44887  175 lemma minus_zero [simp]: "- (0::'a) = 0"  wenzelm@9035  176  by (simp add: negate_eq1)  wenzelm@7917  177 wenzelm@44887  178 lemma minus_zero_iff [simp]:  wenzelm@44887  179  assumes x: "x \ V"  wenzelm@44887  180  shows "(- x = 0) = (x = 0)"  wenzelm@13515  181 proof  wenzelm@44887  182  from x have "x = - (- x)" by simp  wenzelm@44887  183  also assume "- x = 0"  wenzelm@44887  184  also have "- \ = 0" by (rule minus_zero)  wenzelm@44887  185  finally show "x = 0" .  wenzelm@44887  186 next  wenzelm@44887  187  assume "x = 0"  wenzelm@44887  188  then show "- x = 0" by simp  wenzelm@9035  189 qed  wenzelm@7917  190 wenzelm@44887  191 lemma add_minus_cancel [simp]: "x \ V \ y \ V \ x + (- x + y) = y"  wenzelm@44887  192  by (simp add: add_assoc [symmetric])  wenzelm@7917  193 wenzelm@44887  194 lemma minus_add_cancel [simp]: "x \ V \ y \ V \ - x + (x + y) = y"  wenzelm@44887  195  by (simp add: add_assoc [symmetric])  wenzelm@7917  196 wenzelm@44887  197 lemma minus_add_distrib [simp]: "x \ V \ y \ V \ - (x + y) = - x + - y"  wenzelm@13515  198  by (simp add: negate_eq1 add_mult_distrib1)  wenzelm@7917  199 wenzelm@44887  200 lemma diff_zero [simp]: "x \ V \ x - 0 = x"  wenzelm@13515  201  by (simp add: diff_eq1)  wenzelm@13515  202 wenzelm@44887  203 lemma diff_zero_right [simp]: "x \ V \ 0 - x = - x"  wenzelm@10687  204  by (simp add: diff_eq1)  wenzelm@7917  205 wenzelm@44887  206 lemma add_left_cancel:  wenzelm@44887  207  assumes x: "x \ V" and y: "y \ V" and z: "z \ V"  wenzelm@44887  208  shows "(x + y = x + z) = (y = z)"  wenzelm@9035  209 proof  wenzelm@44887  210  from y have "y = 0 + y" by simp  wenzelm@44887  211  also from x y have "\ = (- x + x) + y" by simp  haftmann@57512  212  also from x y have "\ = - x + (x + y)" by (simp add: add.assoc)  wenzelm@44887  213  also assume "x + y = x + z"  haftmann@57512  214  also from x z have "- x + (x + z) = - x + x + z" by (simp add: add.assoc)  wenzelm@44887  215  also from x z have "\ = z" by simp  wenzelm@44887  216  finally show "y = z" .  wenzelm@44887  217 next  wenzelm@44887  218  assume "y = z"  wenzelm@44887  219  then show "x + y = x + z" by (simp only:)  wenzelm@13515  220 qed  wenzelm@7917  221 wenzelm@44887  222 lemma add_right_cancel: "x \ V \ y \ V \ z \ V \ (y + x = z + x) = (y = z)"  wenzelm@13515  223  by (simp only: add_commute add_left_cancel)  wenzelm@7917  224 wenzelm@44887  225 lemma add_assoc_cong:  wenzelm@13515  226  "x \ V \ y \ V \ x' \ V \ y' \ V \ z \ V  wenzelm@13515  227  \ x + y = x' + y' \ x + (y + z) = x' + (y' + z)"  wenzelm@13515  228  by (simp only: add_assoc [symmetric])  wenzelm@7917  229 wenzelm@44887  230 lemma mult_left_commute: "x \ V \ a \ b \ x = b \ a \ x"  haftmann@57512  231  by (simp add: mult.commute mult_assoc2)  wenzelm@7917  232 wenzelm@44887  233 lemma mult_zero_uniq:  wenzelm@44887  234  assumes x: "x \ V" "x \ 0" and ax: "a \ x = 0"  wenzelm@44887  235  shows "a = 0"  wenzelm@9035  236 proof (rule classical)  wenzelm@13515  237  assume a: "a \ 0"  wenzelm@13515  238  from x a have "x = (inverse a * a) \ x" by simp  wenzelm@58744  239  also from \x \ V\ have "\ = inverse a \ (a \ x)" by (rule mult_assoc)  wenzelm@27612  240  also from ax have "\ = inverse a \ 0" by simp  wenzelm@27612  241  also have "\ = 0" by simp  bauerg@9374  242  finally have "x = 0" .  wenzelm@58744  243  with \x \ 0\ show "a = 0" by contradiction  wenzelm@9035  244 qed  wenzelm@7917  245 wenzelm@44887  246 lemma mult_left_cancel:  wenzelm@44887  247  assumes x: "x \ V" and y: "y \ V" and a: "a \ 0"  wenzelm@44887  248  shows "(a \ x = a \ y) = (x = y)"  wenzelm@9035  249 proof  wenzelm@13515  250  from x have "x = 1 \ x" by simp  wenzelm@27612  251  also from a have "\ = (inverse a * a) \ x" by simp  wenzelm@27612  252  also from x have "\ = inverse a \ (a \ x)"  wenzelm@13515  253  by (simp only: mult_assoc)  wenzelm@13515  254  also assume "a \ x = a \ y"  wenzelm@27612  255  also from a y have "inverse a \ \ = y"  wenzelm@13515  256  by (simp add: mult_assoc2)  wenzelm@13515  257  finally show "x = y" .  wenzelm@13515  258 next  wenzelm@13515  259  assume "x = y"  wenzelm@13515  260  then show "a \ x = a \ y" by (simp only:)  wenzelm@13515  261 qed  wenzelm@7917  262 wenzelm@44887  263 lemma mult_right_cancel:  wenzelm@44887  264  assumes x: "x \ V" and neq: "x \ 0"  wenzelm@44887  265  shows "(a \ x = b \ x) = (a = b)"  wenzelm@9035  266 proof  wenzelm@44887  267  from x have "(a - b) \ x = a \ x - b \ x"  wenzelm@44887  268  by (simp add: diff_mult_distrib2)  wenzelm@44887  269  also assume "a \ x = b \ x"  wenzelm@44887  270  with x have "a \ x - b \ x = 0" by simp  wenzelm@44887  271  finally have "(a - b) \ x = 0" .  wenzelm@44887  272  with x neq have "a - b = 0" by (rule mult_zero_uniq)  wenzelm@44887  273  then show "a = b" by simp  wenzelm@44887  274 next  wenzelm@44887  275  assume "a = b"  wenzelm@44887  276  then show "a \ x = b \ x" by (simp only:)  wenzelm@13515  277 qed  wenzelm@7917  278 wenzelm@44887  279 lemma eq_diff_eq:  wenzelm@44887  280  assumes x: "x \ V" and y: "y \ V" and z: "z \ V"  wenzelm@44887  281  shows "(x = z - y) = (x + y = z)"  wenzelm@13515  282 proof  wenzelm@44887  283  assume "x = z - y"  wenzelm@44887  284  then have "x + y = z - y + y" by simp  wenzelm@44887  285  also from y z have "\ = z + - y + y"  wenzelm@44887  286  by (simp add: diff_eq1)  wenzelm@44887  287  also have "\ = z + (- y + y)"  wenzelm@44887  288  by (rule add_assoc) (simp_all add: y z)  wenzelm@44887  289  also from y z have "\ = z + 0"  wenzelm@44887  290  by (simp only: add_minus_left)  wenzelm@44887  291  also from z have "\ = z"  wenzelm@44887  292  by (simp only: add_zero_right)  wenzelm@44887  293  finally show "x + y = z" .  wenzelm@44887  294 next  wenzelm@44887  295  assume "x + y = z"  wenzelm@44887  296  then have "z - y = (x + y) - y" by simp  wenzelm@44887  297  also from x y have "\ = x + y + - y"  wenzelm@44887  298  by (simp add: diff_eq1)  wenzelm@44887  299  also have "\ = x + (y + - y)"  wenzelm@44887  300  by (rule add_assoc) (simp_all add: x y)  wenzelm@44887  301  also from x y have "\ = x" by simp  wenzelm@44887  302  finally show "x = z - y" ..  wenzelm@9035  303 qed  wenzelm@7917  304 wenzelm@44887  305 lemma add_minus_eq_minus:  wenzelm@44887  306  assumes x: "x \ V" and y: "y \ V" and xy: "x + y = 0"  wenzelm@44887  307  shows "x = - y"  wenzelm@9035  308 proof -  wenzelm@13515  309  from x y have "x = (- y + y) + x" by simp  wenzelm@27612  310  also from x y have "\ = - y + (x + y)" by (simp add: add_ac)  wenzelm@44887  311  also note xy  wenzelm@13515  312  also from y have "- y + 0 = - y" by simp  wenzelm@9035  313  finally show "x = - y" .  wenzelm@9035  314 qed  wenzelm@7917  315 wenzelm@44887  316 lemma add_minus_eq:  wenzelm@44887  317  assumes x: "x \ V" and y: "y \ V" and xy: "x - y = 0"  wenzelm@44887  318  shows "x = y"  wenzelm@9035  319 proof -  wenzelm@44887  320  from x y xy have eq: "x + - y = 0" by (simp add: diff_eq1)  wenzelm@13515  321  with _ _ have "x = - (- y)"  wenzelm@13515  322  by (rule add_minus_eq_minus) (simp_all add: x y)  wenzelm@13515  323  with x y show "x = y" by simp  wenzelm@9035  324 qed  wenzelm@7917  325 wenzelm@44887  326 lemma add_diff_swap:  wenzelm@44887  327  assumes vs: "a \ V" "b \ V" "c \ V" "d \ V"  wenzelm@44887  328  and eq: "a + b = c + d"  wenzelm@44887  329  shows "a - c = d - b"  wenzelm@10687  330 proof -  wenzelm@44887  331  from assms have "- c + (a + b) = - c + (c + d)"  wenzelm@13515  332  by (simp add: add_left_cancel)  wenzelm@58744  333  also have "\ = d" using \c \ V\ \d \ V\ by (rule minus_add_cancel)  wenzelm@9035  334  finally have eq: "- c + (a + b) = d" .  wenzelm@10687  335  from vs have "a - c = (- c + (a + b)) + - b"  wenzelm@13515  336  by (simp add: add_ac diff_eq1)  wenzelm@27612  337  also from vs eq have "\ = d + - b"  wenzelm@13515  338  by (simp add: add_right_cancel)  wenzelm@27612  339  also from vs have "\ = d - b" by (simp add: diff_eq2)  wenzelm@9035  340  finally show "a - c = d - b" .  wenzelm@9035  341 qed  wenzelm@7917  342 wenzelm@44887  343 lemma vs_add_cancel_21:  wenzelm@44887  344  assumes vs: "x \ V" "y \ V" "z \ V" "u \ V"  wenzelm@44887  345  shows "(x + (y + z) = y + u) = (x + z = u)"  wenzelm@13515  346 proof  wenzelm@44887  347  from vs have "x + z = - y + y + (x + z)" by simp  wenzelm@44887  348  also have "\ = - y + (y + (x + z))"  wenzelm@44887  349  by (rule add_assoc) (simp_all add: vs)  wenzelm@44887  350  also from vs have "y + (x + z) = x + (y + z)"  wenzelm@44887  351  by (simp add: add_ac)  wenzelm@44887  352  also assume "x + (y + z) = y + u"  wenzelm@44887  353  also from vs have "- y + (y + u) = u" by simp  wenzelm@44887  354  finally show "x + z = u" .  wenzelm@44887  355 next  wenzelm@44887  356  assume "x + z = u"  wenzelm@44887  357  with vs show "x + (y + z) = y + u"  wenzelm@44887  358  by (simp only: add_left_commute [of x])  wenzelm@9035  359 qed  wenzelm@7917  360 wenzelm@44887  361 lemma add_cancel_end:  wenzelm@44887  362  assumes vs: "x \ V" "y \ V" "z \ V"  wenzelm@44887  363  shows "(x + (y + z) = y) = (x = - z)"  wenzelm@13515  364 proof  wenzelm@44887  365  assume "x + (y + z) = y"  wenzelm@44887  366  with vs have "(x + z) + y = 0 + y" by (simp add: add_ac)  wenzelm@44887  367  with vs have "x + z = 0" by (simp only: add_right_cancel add_closed zero)  wenzelm@44887  368  with vs show "x = - z" by (simp add: add_minus_eq_minus)  wenzelm@44887  369 next  wenzelm@44887  370  assume eq: "x = - z"  wenzelm@44887  371  then have "x + (y + z) = - z + (y + z)" by simp  wenzelm@44887  372  also have "\ = y + (- z + z)" by (rule add_left_commute) (simp_all add: vs)  wenzelm@44887  373  also from vs have "\ = y" by simp  wenzelm@44887  374  finally show "x + (y + z) = y" .  wenzelm@9035  375 qed  wenzelm@7917  376 wenzelm@10687  377 end  wenzelm@44887  378 wenzelm@44887  379 end  wenzelm@44887  380