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