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