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