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