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