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