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