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