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