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