src/HOL/Real/HahnBanach/VectorSpace.thy
author wenzelm
Sun Jul 23 12:01:05 2000 +0200 (2000-07-23)
changeset 9408 d3d56e1d2ec1
parent 9379 21cfeae6659d
child 9503 3324cbbecef8
permissions -rw-r--r--
classical atts now intro! / intro / intro?;
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@9035
     8
theory VectorSpace = Bounds + Aux:
wenzelm@7917
     9
wenzelm@9035
    10
subsection {* Signature *}
wenzelm@7917
    11
wenzelm@7927
    12
text {* For the definition of real vector spaces a type $\alpha$
bauerg@9379
    13
of the sort $\{ \idt{plus}, \idt{minus}, \idt{zero}\}$ is considered, on which a
bauerg@9379
    14
real scalar multiplication $\mult$ is defined. *}
wenzelm@7917
    15
wenzelm@7917
    16
consts
bauerg@9379
    17
  prod  :: "[real, 'a::{plus, minus, zero}] => 'a"     (infixr "'(*')" 70)
wenzelm@7917
    18
wenzelm@7917
    19
syntax (symbols)
bauerg@9379
    20
  prod  :: "[real, 'a] => 'a"                          (infixr "\\<cdot>" 70)
wenzelm@7917
    21
wenzelm@7917
    22
wenzelm@9035
    23
subsection {* Vector space laws *}
wenzelm@7917
    24
wenzelm@7927
    25
text {* A \emph{vector space} is a non-empty set $V$ of elements from
wenzelm@7927
    26
  $\alpha$ with the following vector space laws: The set $V$ is closed
wenzelm@7927
    27
  under addition and scalar multiplication, addition is associative
wenzelm@7927
    28
  and commutative; $\minus x$ is the inverse of $x$ w.~r.~t.~addition
bauerg@9379
    29
  and $0$ is the neutral element of addition.  Addition and
wenzelm@7927
    30
  multiplication are distributive; scalar multiplication is
wenzelm@7978
    31
  associative and the real number $1$ is the neutral element of scalar
wenzelm@7927
    32
  multiplication.
wenzelm@9035
    33
*}
wenzelm@7917
    34
wenzelm@7917
    35
constdefs
bauerg@9374
    36
  is_vectorspace :: "('a::{plus, minus, zero}) set => bool"
bauerg@9379
    37
  "is_vectorspace V == V \\<noteq> {}
bauerg@9379
    38
   \\<and> (\\<forall>x \\<in> V. \\<forall>y \\<in> V. \\<forall>z \\<in> V. \\<forall>a b.
bauerg@9379
    39
        x + y \\<in> V                                 
bauerg@9379
    40
      \\<and> a \\<cdot> x \\<in> V                                 
bauerg@9379
    41
      \\<and> (x + y) + z = x + (y + z)             
bauerg@9379
    42
      \\<and> x + y = y + x                           
bauerg@9379
    43
      \\<and> x - x = 0                               
bauerg@9379
    44
      \\<and> 0 + x = x                               
bauerg@9379
    45
      \\<and> a \\<cdot> (x + y) = a \\<cdot> x + a \\<cdot> y       
bauerg@9379
    46
      \\<and> (a + b) \\<cdot> x = a \\<cdot> x + b \\<cdot> x         
bauerg@9379
    47
      \\<and> (a * b) \\<cdot> x = a \\<cdot> b \\<cdot> x               
bauerg@9379
    48
      \\<and> #1 \\<cdot> x = x
bauerg@9379
    49
      \\<and> - x = (- #1) \\<cdot> x
bauerg@9379
    50
      \\<and> x - y = x + - y)"                             
wenzelm@7917
    51
wenzelm@9035
    52
text_raw {* \medskip *}
wenzelm@9035
    53
text {* The corresponding introduction rule is:*}
wenzelm@7917
    54
wenzelm@7917
    55
lemma vsI [intro]:
bauerg@9379
    56
  "[| 0 \\<in> V; 
bauerg@9379
    57
  \\<forall>x \\<in> V. \\<forall>y \\<in> V. x + y \\<in> V; 
bauerg@9379
    58
  \\<forall>x \\<in> V. \\<forall>a. a \\<cdot> x \\<in> V;  
bauerg@9379
    59
  \\<forall>x \\<in> V. \\<forall>y \\<in> V. \\<forall>z \\<in> V. (x + y) + z = x + (y + z);
bauerg@9379
    60
  \\<forall>x \\<in> V. \\<forall>y \\<in> V. x + y = y + x;
bauerg@9379
    61
  \\<forall>x \\<in> V. x - x = 0;
bauerg@9379
    62
  \\<forall>x \\<in> V. 0 + x = x;
bauerg@9379
    63
  \\<forall>x \\<in> V. \\<forall>y \\<in> V. \\<forall>a. a \\<cdot> (x + y) = a \\<cdot> x + a \\<cdot> y;
bauerg@9379
    64
  \\<forall>x \\<in> V. \\<forall>a b. (a + b) \\<cdot> x = a \\<cdot> x + b \\<cdot> x;
bauerg@9379
    65
  \\<forall>x \\<in> V. \\<forall>a b. (a * b) \\<cdot> x = a \\<cdot> b \\<cdot> x; 
bauerg@9379
    66
  \\<forall>x \\<in> V. #1 \\<cdot> x = x; 
bauerg@9379
    67
  \\<forall>x \\<in> V. - x = (- #1) \\<cdot> x; 
bauerg@9379
    68
  \\<forall>x \\<in> V. \\<forall>y \\<in> V. x - y = x + - y |] ==> is_vectorspace V"
wenzelm@9035
    69
proof (unfold is_vectorspace_def, intro conjI ballI allI)
wenzelm@9035
    70
  fix x y z 
bauerg@9379
    71
  assume "x \\<in> V" "y \\<in> V" "z \\<in> V"
bauerg@9379
    72
    "\\<forall>x \\<in> V. \\<forall>y \\<in> V. \\<forall>z \\<in> V. x + y + z = x + (y + z)"
wenzelm@9408
    73
  thus "x + y + z =  x + (y + z)" by blast
wenzelm@9035
    74
qed force+
wenzelm@7917
    75
wenzelm@9035
    76
text_raw {* \medskip *}
wenzelm@9035
    77
text {* The corresponding destruction rules are: *}
wenzelm@7917
    78
wenzelm@7917
    79
lemma negate_eq1: 
bauerg@9379
    80
  "[| is_vectorspace V; x \\<in> V |] ==> - x = (- #1) \\<cdot> x"
wenzelm@9035
    81
  by (unfold is_vectorspace_def) simp
wenzelm@7917
    82
wenzelm@7917
    83
lemma diff_eq1: 
bauerg@9379
    84
  "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x - y = x + - y"
wenzelm@9035
    85
  by (unfold is_vectorspace_def) simp 
wenzelm@7917
    86
wenzelm@7917
    87
lemma negate_eq2: 
bauerg@9379
    88
  "[| is_vectorspace V; x \\<in> V |] ==> (- #1) \\<cdot> x = - x"
wenzelm@9035
    89
  by (unfold is_vectorspace_def) simp
fleuriot@9013
    90
fleuriot@9013
    91
lemma negate_eq2a: 
bauerg@9379
    92
  "[| is_vectorspace V; x \\<in> V |] ==> #-1 \\<cdot> x = - x"
wenzelm@9035
    93
  by (unfold is_vectorspace_def) simp
wenzelm@7917
    94
wenzelm@7917
    95
lemma diff_eq2: 
bauerg@9379
    96
  "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x + - y = x - y"
wenzelm@9035
    97
  by (unfold is_vectorspace_def) simp  
wenzelm@7917
    98
wenzelm@9408
    99
lemma vs_not_empty [intro?]: "is_vectorspace V ==> (V \\<noteq> {})" 
wenzelm@9035
   100
  by (unfold is_vectorspace_def) simp
wenzelm@7917
   101
 
wenzelm@9408
   102
lemma vs_add_closed [simp, intro?]: 
bauerg@9379
   103
  "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x + y \\<in> V" 
wenzelm@9035
   104
  by (unfold is_vectorspace_def) simp
wenzelm@7917
   105
wenzelm@9408
   106
lemma vs_mult_closed [simp, intro?]: 
bauerg@9379
   107
  "[| is_vectorspace V; x \\<in> V |] ==> a \\<cdot> x \\<in> V" 
wenzelm@9035
   108
  by (unfold is_vectorspace_def) simp
wenzelm@7917
   109
wenzelm@9408
   110
lemma vs_diff_closed [simp, intro?]: 
bauerg@9379
   111
 "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x - y \\<in> V"
wenzelm@9035
   112
  by (simp add: diff_eq1 negate_eq1)
wenzelm@7917
   113
wenzelm@9408
   114
lemma vs_neg_closed  [simp, intro?]: 
bauerg@9379
   115
  "[| is_vectorspace V; x \\<in> V |] ==> - x \\<in> V"
wenzelm@9035
   116
  by (simp add: negate_eq1)
wenzelm@7917
   117
wenzelm@7917
   118
lemma vs_add_assoc [simp]:  
bauerg@9379
   119
  "[| is_vectorspace V; x \\<in> V; y \\<in> V; z \\<in> V |]
wenzelm@9035
   120
   ==> (x + y) + z = x + (y + z)"
wenzelm@9035
   121
  by (unfold is_vectorspace_def) fast
wenzelm@7917
   122
wenzelm@7917
   123
lemma vs_add_commute [simp]: 
bauerg@9379
   124
  "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> y + x = x + y"
wenzelm@9035
   125
  by (unfold is_vectorspace_def) simp
wenzelm@7917
   126
wenzelm@7917
   127
lemma vs_add_left_commute [simp]:
bauerg@9379
   128
  "[| is_vectorspace V; x \\<in> V; y \\<in> V; z \\<in> V |] 
wenzelm@9035
   129
  ==> x + (y + z) = y + (x + z)"
wenzelm@9035
   130
proof -
bauerg@9379
   131
  assume "is_vectorspace V" "x \\<in> V" "y \\<in> V" "z \\<in> V"
wenzelm@9035
   132
  hence "x + (y + z) = (x + y) + z" 
wenzelm@9035
   133
    by (simp only: vs_add_assoc)
wenzelm@9035
   134
  also have "... = (y + x) + z" by (simp! only: vs_add_commute)
wenzelm@9035
   135
  also have "... = y + (x + z)" by (simp! only: vs_add_assoc)
wenzelm@9035
   136
  finally show ?thesis .
wenzelm@9035
   137
qed
wenzelm@7917
   138
wenzelm@9035
   139
theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute
wenzelm@7917
   140
wenzelm@7917
   141
lemma vs_diff_self [simp]: 
bauerg@9379
   142
  "[| is_vectorspace V; x \\<in> V |] ==>  x - x = 0" 
wenzelm@9035
   143
  by (unfold is_vectorspace_def) simp
wenzelm@7917
   144
wenzelm@7978
   145
text {* The existence of the zero element of a vector space
wenzelm@9035
   146
follows from the non-emptiness of carrier set. *}
wenzelm@7917
   147
bauerg@9379
   148
lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> 0 \\<in> V"
wenzelm@9035
   149
proof - 
wenzelm@9035
   150
  assume "is_vectorspace V"
bauerg@9379
   151
  have "V \\<noteq> {}" ..
bauerg@9379
   152
  hence "\\<exists>x. x \\<in> V" by force
wenzelm@9035
   153
  thus ?thesis 
wenzelm@9035
   154
  proof 
bauerg@9379
   155
    fix x assume "x \\<in> V" 
bauerg@9374
   156
    have "0 = x - x" by (simp!)
bauerg@9379
   157
    also have "... \\<in> V" by (simp! only: vs_diff_closed)
wenzelm@9035
   158
    finally show ?thesis .
wenzelm@9035
   159
  qed
wenzelm@9035
   160
qed
wenzelm@7917
   161
wenzelm@7917
   162
lemma vs_add_zero_left [simp]: 
bauerg@9379
   163
  "[| is_vectorspace V; x \\<in> V |] ==>  0 + x = x"
wenzelm@9035
   164
  by (unfold is_vectorspace_def) simp
wenzelm@7917
   165
wenzelm@7917
   166
lemma vs_add_zero_right [simp]: 
bauerg@9379
   167
  "[| is_vectorspace V; x \\<in> V |] ==>  x + 0 = x"
wenzelm@9035
   168
proof -
bauerg@9379
   169
  assume "is_vectorspace V" "x \\<in> V"
bauerg@9374
   170
  hence "x + 0 = 0 + x" by simp
wenzelm@9035
   171
  also have "... = x" by (simp!)
wenzelm@9035
   172
  finally show ?thesis .
wenzelm@9035
   173
qed
wenzelm@7917
   174
wenzelm@7917
   175
lemma vs_add_mult_distrib1: 
bauerg@9379
   176
  "[| is_vectorspace V; x \\<in> V; y \\<in> V |] 
bauerg@9379
   177
  ==> a \\<cdot> (x + y) = a \\<cdot> x + a \\<cdot> y"
wenzelm@9035
   178
  by (unfold is_vectorspace_def) simp
wenzelm@7917
   179
wenzelm@7917
   180
lemma vs_add_mult_distrib2: 
bauerg@9379
   181
  "[| is_vectorspace V; x \\<in> V |] 
bauerg@9379
   182
  ==> (a + b) \\<cdot> x = a \\<cdot> x + b \\<cdot> x" 
wenzelm@9035
   183
  by (unfold is_vectorspace_def) simp
wenzelm@7917
   184
wenzelm@7917
   185
lemma vs_mult_assoc: 
bauerg@9379
   186
  "[| is_vectorspace V; x \\<in> V |] ==> (a * b) \\<cdot> x = a \\<cdot> (b \\<cdot> x)"
wenzelm@9035
   187
  by (unfold is_vectorspace_def) simp
wenzelm@7917
   188
wenzelm@7917
   189
lemma vs_mult_assoc2 [simp]: 
bauerg@9379
   190
 "[| is_vectorspace V; x \\<in> V |] ==> a \\<cdot> b \\<cdot> x = (a * b) \\<cdot> x"
wenzelm@9035
   191
  by (simp only: vs_mult_assoc)
wenzelm@7917
   192
wenzelm@7917
   193
lemma vs_mult_1 [simp]: 
bauerg@9379
   194
  "[| is_vectorspace V; x \\<in> V |] ==> #1 \\<cdot> x = x" 
wenzelm@9035
   195
  by (unfold is_vectorspace_def) simp
wenzelm@7917
   196
wenzelm@7917
   197
lemma vs_diff_mult_distrib1: 
bauerg@9379
   198
  "[| is_vectorspace V; x \\<in> V; y \\<in> V |] 
bauerg@9379
   199
  ==> a \\<cdot> (x - y) = a \\<cdot> x - a \\<cdot> y"
wenzelm@9035
   200
  by (simp add: diff_eq1 negate_eq1 vs_add_mult_distrib1)
wenzelm@7917
   201
wenzelm@7917
   202
lemma vs_diff_mult_distrib2: 
bauerg@9379
   203
  "[| is_vectorspace V; x \\<in> V |] 
bauerg@9379
   204
  ==> (a - b) \\<cdot> x = a \\<cdot> x - (b \\<cdot> x)"
wenzelm@9035
   205
proof -
bauerg@9379
   206
  assume "is_vectorspace V" "x \\<in> V"
bauerg@9379
   207
  have " (a - b) \\<cdot> x = (a + - b) \\<cdot> x" 
wenzelm@9035
   208
    by (unfold real_diff_def, simp)
bauerg@9379
   209
  also have "... = a \\<cdot> x + (- b) \\<cdot> x" 
wenzelm@9035
   210
    by (rule vs_add_mult_distrib2)
bauerg@9379
   211
  also have "... = a \\<cdot> x + - (b \\<cdot> x)" 
wenzelm@9035
   212
    by (simp! add: negate_eq1)
bauerg@9379
   213
  also have "... = a \\<cdot> x - (b \\<cdot> x)" 
wenzelm@9035
   214
    by (simp! add: diff_eq1)
wenzelm@9035
   215
  finally show ?thesis .
wenzelm@9035
   216
qed
wenzelm@7917
   217
wenzelm@9035
   218
(*text_raw {* \paragraph {Further derived laws.} *}*)
wenzelm@9035
   219
text_raw {* \medskip *}
wenzelm@9035
   220
text{* Further derived laws: *}
wenzelm@7917
   221
wenzelm@7917
   222
lemma vs_mult_zero_left [simp]: 
bauerg@9379
   223
  "[| is_vectorspace V; x \\<in> V |] ==> #0 \\<cdot> x = 0"
wenzelm@9035
   224
proof -
bauerg@9379
   225
  assume "is_vectorspace V" "x \\<in> V"
bauerg@9379
   226
  have  "#0 \\<cdot> x = (#1 - #1) \\<cdot> x" by simp
bauerg@9379
   227
  also have "... = (#1 + - #1) \\<cdot> x" by simp
bauerg@9379
   228
  also have "... =  #1 \\<cdot> x + (- #1) \\<cdot> x" 
wenzelm@9035
   229
    by (rule vs_add_mult_distrib2)
bauerg@9379
   230
  also have "... = x + (- #1) \\<cdot> x" by (simp!)
wenzelm@9035
   231
  also have "... = x + - x" by (simp! add: negate_eq2a)
wenzelm@9035
   232
  also have "... = x - x" by (simp! add: diff_eq2)
bauerg@9374
   233
  also have "... = 0" by (simp!)
wenzelm@9035
   234
  finally show ?thesis .
wenzelm@9035
   235
qed
wenzelm@7917
   236
wenzelm@7917
   237
lemma vs_mult_zero_right [simp]: 
bauerg@9374
   238
  "[| is_vectorspace (V:: 'a::{plus, minus, zero} set) |] 
bauerg@9379
   239
  ==> a \\<cdot> 0 = (0::'a)"
wenzelm@9035
   240
proof -
wenzelm@9035
   241
  assume "is_vectorspace V"
bauerg@9379
   242
  have "a \\<cdot> 0 = a \\<cdot> (0 - (0::'a))" by (simp!)
bauerg@9379
   243
  also have "... =  a \\<cdot> 0 - a \\<cdot> 0"
wenzelm@9035
   244
     by (rule vs_diff_mult_distrib1) (simp!)+
bauerg@9374
   245
  also have "... = 0" by (simp!)
wenzelm@9035
   246
  finally show ?thesis .
wenzelm@9035
   247
qed
wenzelm@7917
   248
wenzelm@7917
   249
lemma vs_minus_mult_cancel [simp]:  
bauerg@9379
   250
  "[| is_vectorspace V; x \\<in> V |] ==> (- a) \\<cdot> - x = a \\<cdot> x"
wenzelm@9035
   251
  by (simp add: negate_eq1)
wenzelm@7917
   252
wenzelm@7917
   253
lemma vs_add_minus_left_eq_diff: 
bauerg@9379
   254
  "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> - x + y = y - x"
wenzelm@9035
   255
proof - 
bauerg@9379
   256
  assume "is_vectorspace V" "x \\<in> V" "y \\<in> V"
bauerg@9379
   257
  hence "- x + y = y + - x" 
bauerg@9379
   258
    by (simp add: vs_add_commute)
wenzelm@9035
   259
  also have "... = y - x" by (simp! add: diff_eq1)
wenzelm@9035
   260
  finally show ?thesis .
wenzelm@9035
   261
qed
wenzelm@7917
   262
wenzelm@7917
   263
lemma vs_add_minus [simp]: 
bauerg@9379
   264
  "[| is_vectorspace V; x \\<in> V |] ==> x + - x = 0"
wenzelm@9035
   265
  by (simp! add: diff_eq2)
wenzelm@7917
   266
wenzelm@7917
   267
lemma vs_add_minus_left [simp]: 
bauerg@9379
   268
  "[| is_vectorspace V; x \\<in> V |] ==> - x + x = 0"
wenzelm@9035
   269
  by (simp! add: diff_eq2)
wenzelm@7917
   270
wenzelm@7917
   271
lemma vs_minus_minus [simp]: 
bauerg@9379
   272
  "[| is_vectorspace V; x \\<in> V |] ==> - (- x) = x"
wenzelm@9035
   273
  by (simp add: negate_eq1)
wenzelm@7917
   274
wenzelm@7917
   275
lemma vs_minus_zero [simp]: 
bauerg@9374
   276
  "is_vectorspace (V::'a::{plus, minus, zero} set) ==> - (0::'a) = 0" 
wenzelm@9035
   277
  by (simp add: negate_eq1)
wenzelm@7917
   278
wenzelm@7917
   279
lemma vs_minus_zero_iff [simp]:
bauerg@9379
   280
  "[| is_vectorspace V; x \\<in> V |] ==> (- x = 0) = (x = 0)" 
wenzelm@9035
   281
  (concl is "?L = ?R")
wenzelm@9035
   282
proof -
bauerg@9379
   283
  assume "is_vectorspace V" "x \\<in> V"
wenzelm@9035
   284
  show "?L = ?R"
wenzelm@9035
   285
  proof
bauerg@9379
   286
    have "x = - (- x)" by (simp! add: vs_minus_minus)
wenzelm@9035
   287
    also assume ?L
bauerg@9374
   288
    also have "- ... = 0" by (rule vs_minus_zero)
wenzelm@9035
   289
    finally show ?R .
wenzelm@9035
   290
  qed (simp!)
wenzelm@9035
   291
qed
wenzelm@7917
   292
wenzelm@7917
   293
lemma vs_add_minus_cancel [simp]:  
bauerg@9379
   294
  "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> x + (- x + y) = y" 
wenzelm@9035
   295
  by (simp add: vs_add_assoc [RS sym] del: vs_add_commute) 
wenzelm@7917
   296
wenzelm@7917
   297
lemma vs_minus_add_cancel [simp]: 
bauerg@9379
   298
  "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> - x + (x + y) = y" 
wenzelm@9035
   299
  by (simp add: vs_add_assoc [RS sym] del: vs_add_commute) 
wenzelm@7917
   300
wenzelm@7917
   301
lemma vs_minus_add_distrib [simp]:  
bauerg@9379
   302
  "[| is_vectorspace V; x \\<in> V; y \\<in> V |] 
wenzelm@9035
   303
  ==> - (x + y) = - x + - y"
wenzelm@9035
   304
  by (simp add: negate_eq1 vs_add_mult_distrib1)
wenzelm@7917
   305
wenzelm@7917
   306
lemma vs_diff_zero [simp]: 
bauerg@9379
   307
  "[| is_vectorspace V; x \\<in> V |] ==> x - 0 = x"
wenzelm@9035
   308
  by (simp add: diff_eq1)  
wenzelm@7917
   309
wenzelm@7917
   310
lemma vs_diff_zero_right [simp]: 
bauerg@9379
   311
  "[| is_vectorspace V; x \\<in> V |] ==> 0 - x = - x"
wenzelm@9035
   312
  by (simp add:diff_eq1)
wenzelm@7917
   313
wenzelm@7917
   314
lemma vs_add_left_cancel:
bauerg@9379
   315
  "[| is_vectorspace V; x \\<in> V; y \\<in> V; z \\<in> V |] 
wenzelm@7917
   316
   ==> (x + y = x + z) = (y = z)"  
wenzelm@9035
   317
  (concl is "?L = ?R")
wenzelm@9035
   318
proof
bauerg@9379
   319
  assume "is_vectorspace V" "x \\<in> V" "y \\<in> V" "z \\<in> V"
bauerg@9374
   320
  have "y = 0 + y" by (simp!)
wenzelm@9035
   321
  also have "... = - x + x + y" by (simp!)
wenzelm@9035
   322
  also have "... = - x + (x + y)" 
wenzelm@9035
   323
    by (simp! only: vs_add_assoc vs_neg_closed)
bauerg@9379
   324
  also assume "x + y = x + z"
bauerg@9379
   325
  also have "- x + (x + z) = - x + x + z" 
wenzelm@9408
   326
    by (simp! only: vs_add_assoc [RS sym] vs_neg_closed)
wenzelm@9035
   327
  also have "... = z" by (simp!)
wenzelm@9035
   328
  finally show ?R .
wenzelm@9035
   329
qed force
wenzelm@7917
   330
wenzelm@7917
   331
lemma vs_add_right_cancel: 
bauerg@9379
   332
  "[| is_vectorspace V; x \\<in> V; y \\<in> V; z \\<in> V |] 
wenzelm@9035
   333
  ==> (y + x = z + x) = (y = z)"  
wenzelm@9035
   334
  by (simp only: vs_add_commute vs_add_left_cancel)
wenzelm@7917
   335
wenzelm@7917
   336
lemma vs_add_assoc_cong: 
bauerg@9379
   337
  "[| is_vectorspace V; x \\<in> V; y \\<in> V; x' \\<in> V; y' \\<in> V; z \\<in> V |] 
wenzelm@9035
   338
  ==> x + y = x' + y' ==> x + (y + z) = x' + (y' + z)"
wenzelm@9035
   339
  by (simp only: vs_add_assoc [RS sym]) 
wenzelm@7917
   340
wenzelm@7917
   341
lemma vs_mult_left_commute: 
bauerg@9379
   342
  "[| is_vectorspace V; x \\<in> V; y \\<in> V; z \\<in> V |] 
bauerg@9379
   343
  ==> x \\<cdot> y \\<cdot> z = y \\<cdot> x \\<cdot> z"  
wenzelm@9035
   344
  by (simp add: real_mult_commute)
wenzelm@7917
   345
bauerg@9374
   346
lemma vs_mult_zero_uniq:
bauerg@9379
   347
  "[| is_vectorspace V; x \\<in> V; a \\<cdot> x = 0; x \\<noteq> 0 |] ==> a = #0"
wenzelm@9035
   348
proof (rule classical)
bauerg@9379
   349
  assume "is_vectorspace V" "x \\<in> V" "a \\<cdot> x = 0" "x \\<noteq> 0"
bauerg@9379
   350
  assume "a \\<noteq> #0"
bauerg@9379
   351
  have "x = (rinv a * a) \\<cdot> x" by (simp!)
bauerg@9379
   352
  also have "... = rinv a \\<cdot> (a \\<cdot> x)" by (rule vs_mult_assoc)
bauerg@9379
   353
  also have "... = rinv a \\<cdot> 0" by (simp!)
bauerg@9374
   354
  also have "... = 0" by (simp!)
bauerg@9374
   355
  finally have "x = 0" .
wenzelm@9035
   356
  thus "a = #0" by contradiction 
wenzelm@9035
   357
qed
wenzelm@7917
   358
wenzelm@7917
   359
lemma vs_mult_left_cancel: 
bauerg@9379
   360
  "[| is_vectorspace V; x \\<in> V; y \\<in> V; a \\<noteq> #0 |] ==> 
bauerg@9379
   361
  (a \\<cdot> x = a \\<cdot> y) = (x = y)"
wenzelm@9035
   362
  (concl is "?L = ?R")
wenzelm@9035
   363
proof
bauerg@9379
   364
  assume "is_vectorspace V" "x \\<in> V" "y \\<in> V" "a \\<noteq> #0"
bauerg@9379
   365
  have "x = #1 \\<cdot> x" by (simp!)
bauerg@9379
   366
  also have "... = (rinv a * a) \\<cdot> x" by (simp!)
bauerg@9379
   367
  also have "... = rinv a \\<cdot> (a \\<cdot> x)" 
wenzelm@9035
   368
    by (simp! only: vs_mult_assoc)
wenzelm@9035
   369
  also assume ?L
bauerg@9379
   370
  also have "rinv a \\<cdot> ... = y" by (simp!)
wenzelm@9035
   371
  finally show ?R .
wenzelm@9035
   372
qed simp
wenzelm@7917
   373
wenzelm@7917
   374
lemma vs_mult_right_cancel: (*** forward ***)
bauerg@9379
   375
  "[| is_vectorspace V; x \\<in> V; x \\<noteq> 0 |] 
bauerg@9379
   376
  ==> (a \\<cdot> x = b \\<cdot> x) = (a = b)" (concl is "?L = ?R")
wenzelm@9035
   377
proof
bauerg@9379
   378
  assume "is_vectorspace V" "x \\<in> V" "x \\<noteq> 0"
bauerg@9379
   379
  have "(a - b) \\<cdot> x = a \\<cdot> x - b \\<cdot> x" 
wenzelm@9035
   380
    by (simp! add: vs_diff_mult_distrib2)
bauerg@9379
   381
  also assume ?L hence "a \\<cdot> x - b \\<cdot> x = 0" by (simp!)
bauerg@9379
   382
  finally have "(a - b) \\<cdot> x = 0" . 
wenzelm@9035
   383
  hence "a - b = #0" by (simp! add: vs_mult_zero_uniq)
wenzelm@9035
   384
  thus "a = b" by (rule real_add_minus_eq)
wenzelm@9035
   385
qed simp (*** 
wenzelm@7917
   386
wenzelm@7917
   387
lemma vs_mult_right_cancel: 
bauerg@9379
   388
  "[| is_vectorspace V; x:V; x \\<noteq> 0 |] ==>  
nipkow@8703
   389
  (a ( * ) x = b ( * ) x) = (a = b)"
wenzelm@7917
   390
  (concl is "?L = ?R");
wenzelm@7917
   391
proof;
bauerg@9379
   392
  assume "is_vectorspace V" "x:V" "x \\<noteq> 0";
wenzelm@7917
   393
  assume l: ?L; 
wenzelm@7917
   394
  show "a = b"; 
wenzelm@7917
   395
  proof (rule real_add_minus_eq);
fleuriot@9013
   396
    show "a - b = (#0::real)"; 
wenzelm@7917
   397
    proof (rule vs_mult_zero_uniq);
nipkow@8703
   398
      have "(a - b) ( * ) x = a ( * ) x - b ( * ) x";
wenzelm@7917
   399
        by (simp! add: vs_diff_mult_distrib2);
bauerg@9374
   400
      also; from l; have "a ( * ) x - b ( * ) x = 0"; by (simp!);
bauerg@9374
   401
      finally; show "(a - b) ( * ) x  = 0"; .; 
wenzelm@7917
   402
    qed;
wenzelm@7917
   403
  qed;
wenzelm@7917
   404
next;
wenzelm@7917
   405
  assume ?R;
wenzelm@7917
   406
  thus ?L; by simp;
wenzelm@7917
   407
qed;
wenzelm@7917
   408
**)
wenzelm@7917
   409
wenzelm@7917
   410
lemma vs_eq_diff_eq: 
bauerg@9379
   411
  "[| is_vectorspace V; x \\<in> V; y \\<in> V; z \\<in> V |] ==> 
wenzelm@7917
   412
  (x = z - y) = (x + y = z)"
wenzelm@9035
   413
  (concl is "?L = ?R" )  
wenzelm@9035
   414
proof -
bauerg@9379
   415
  assume vs: "is_vectorspace V" "x \\<in> V" "y \\<in> V" "z \\<in> V"
wenzelm@9035
   416
  show "?L = ?R"   
wenzelm@9035
   417
  proof
wenzelm@9035
   418
    assume ?L
wenzelm@9035
   419
    hence "x + y = z - y + y" by simp
wenzelm@9035
   420
    also have "... = z + - y + y" by (simp! add: diff_eq1)
wenzelm@9035
   421
    also have "... = z + (- y + y)" 
wenzelm@9035
   422
      by (rule vs_add_assoc) (simp!)+
bauerg@9374
   423
    also from vs have "... = z + 0" 
wenzelm@9035
   424
      by (simp only: vs_add_minus_left)
wenzelm@9035
   425
    also from vs have "... = z" by (simp only: vs_add_zero_right)
wenzelm@9035
   426
    finally show ?R .
wenzelm@9035
   427
  next
wenzelm@9035
   428
    assume ?R
wenzelm@9035
   429
    hence "z - y = (x + y) - y" by simp
wenzelm@9035
   430
    also from vs have "... = x + y + - y" 
wenzelm@9035
   431
      by (simp add: diff_eq1)
wenzelm@9035
   432
    also have "... = x + (y + - y)" 
wenzelm@9035
   433
      by (rule vs_add_assoc) (simp!)+
wenzelm@9035
   434
    also have "... = x" by (simp!)
wenzelm@9035
   435
    finally show ?L by (rule sym)
wenzelm@9035
   436
  qed
wenzelm@9035
   437
qed
wenzelm@7917
   438
wenzelm@7917
   439
lemma vs_add_minus_eq_minus: 
bauerg@9379
   440
  "[| is_vectorspace V; x \\<in> V; y \\<in> V; x + y = 0 |] ==> x = - y" 
wenzelm@9035
   441
proof -
bauerg@9379
   442
  assume "is_vectorspace V" "x \\<in> V" "y \\<in> V" 
wenzelm@9035
   443
  have "x = (- y + y) + x" by (simp!)
wenzelm@9035
   444
  also have "... = - y + (x + y)" by (simp!)
bauerg@9374
   445
  also assume "x + y = 0"
bauerg@9374
   446
  also have "- y + 0 = - y" by (simp!)
wenzelm@9035
   447
  finally show "x = - y" .
wenzelm@9035
   448
qed
wenzelm@7917
   449
wenzelm@7917
   450
lemma vs_add_minus_eq: 
bauerg@9379
   451
  "[| is_vectorspace V; x \\<in> V; y \\<in> V; x - y = 0 |] ==> x = y" 
wenzelm@9035
   452
proof -
bauerg@9379
   453
  assume "is_vectorspace V" "x \\<in> V" "y \\<in> V" "x - y = 0"
bauerg@9374
   454
  assume "x - y = 0"
bauerg@9374
   455
  hence e: "x + - y = 0" by (simp! add: diff_eq1)
wenzelm@9035
   456
  with _ _ _ have "x = - (- y)" 
wenzelm@9035
   457
    by (rule vs_add_minus_eq_minus) (simp!)+
wenzelm@9035
   458
  thus "x = y" by (simp!)
wenzelm@9035
   459
qed
wenzelm@7917
   460
wenzelm@7917
   461
lemma vs_add_diff_swap:
bauerg@9379
   462
  "[| is_vectorspace V; a \\<in> V; b \\<in> V; c \\<in> V; d \\<in> V; a + b = c + d |] 
wenzelm@9035
   463
  ==> a - c = d - b"
wenzelm@9035
   464
proof - 
bauerg@9379
   465
  assume vs: "is_vectorspace V" "a \\<in> V" "b \\<in> V" "c \\<in> V" "d \\<in> V" 
wenzelm@9035
   466
    and eq: "a + b = c + d"
wenzelm@9035
   467
  have "- c + (a + b) = - c + (c + d)" 
wenzelm@9035
   468
    by (simp! add: vs_add_left_cancel)
wenzelm@9035
   469
  also have "... = d" by (rule vs_minus_add_cancel)
wenzelm@9035
   470
  finally have eq: "- c + (a + b) = d" .
wenzelm@9035
   471
  from vs have "a - c = (- c + (a + b)) + - b" 
wenzelm@9035
   472
    by (simp add: vs_add_ac diff_eq1)
wenzelm@9035
   473
  also from eq have "...  = d + - b" 
wenzelm@9035
   474
    by (simp! add: vs_add_right_cancel)
bauerg@9374
   475
  also have "... = d - b" by (simp! add: diff_eq2)
wenzelm@9035
   476
  finally show "a - c = d - b" .
wenzelm@9035
   477
qed
wenzelm@7917
   478
wenzelm@7917
   479
lemma vs_add_cancel_21: 
bauerg@9379
   480
  "[| is_vectorspace V; x \\<in> V; y \\<in> V; z \\<in> V; u \\<in> V |] 
wenzelm@7917
   481
  ==> (x + (y + z) = y + u) = ((x + z) = u)"
wenzelm@9035
   482
  (concl is "?L = ?R") 
wenzelm@9035
   483
proof - 
bauerg@9379
   484
  assume "is_vectorspace V" "x \\<in> V" "y \\<in> V" "z \\<in> V" "u \\<in> V"
wenzelm@9035
   485
  show "?L = ?R"
wenzelm@9035
   486
  proof
wenzelm@9035
   487
    have "x + z = - y + y + (x + z)" by (simp!)
wenzelm@9035
   488
    also have "... = - y + (y + (x + z))"
wenzelm@9035
   489
      by (rule vs_add_assoc) (simp!)+
wenzelm@9035
   490
    also have "y + (x + z) = x + (y + z)" by (simp!)
wenzelm@9035
   491
    also assume ?L
wenzelm@9035
   492
    also have "- y + (y + u) = u" by (simp!)
wenzelm@9035
   493
    finally show ?R .
wenzelm@9035
   494
  qed (simp! only: vs_add_left_commute [of V x])
wenzelm@9035
   495
qed
wenzelm@7917
   496
wenzelm@7917
   497
lemma vs_add_cancel_end: 
bauerg@9379
   498
  "[| is_vectorspace V; x \\<in> V; y \\<in> V; z \\<in> V |] 
wenzelm@7917
   499
  ==> (x + (y + z) = y) = (x = - z)"
wenzelm@9035
   500
  (concl is "?L = ?R" )
wenzelm@9035
   501
proof -
bauerg@9379
   502
  assume "is_vectorspace V" "x \\<in> V" "y \\<in> V" "z \\<in> V"
wenzelm@9035
   503
  show "?L = ?R"
wenzelm@9035
   504
  proof
wenzelm@9035
   505
    assume l: ?L
bauerg@9374
   506
    have "x + z = 0" 
wenzelm@9035
   507
    proof (rule vs_add_left_cancel [RS iffD1])
wenzelm@9035
   508
      have "y + (x + z) = x + (y + z)" by (simp!)
wenzelm@9035
   509
      also note l
bauerg@9374
   510
      also have "y = y + 0" by (simp!)
bauerg@9374
   511
      finally show "y + (x + z) = y + 0" .
wenzelm@9035
   512
    qed (simp!)+
wenzelm@9035
   513
    thus "x = - z" by (simp! add: vs_add_minus_eq_minus)
wenzelm@9035
   514
  next
wenzelm@9035
   515
    assume r: ?R
wenzelm@9035
   516
    hence "x + (y + z) = - z + (y + z)" by simp 
wenzelm@9035
   517
    also have "... = y + (- z + z)" 
wenzelm@9035
   518
      by (simp! only: vs_add_left_commute)
wenzelm@9035
   519
    also have "... = y"  by (simp!)
wenzelm@9035
   520
    finally show ?L .
wenzelm@9035
   521
  qed
wenzelm@9035
   522
qed
wenzelm@7917
   523
wenzelm@9035
   524
end