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