--- a/src/HOL/Real/HahnBanach/VectorSpace.thy Sun Jul 16 21:00:32 2000 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Mon Jul 17 13:58:18 2000 +0200
@@ -15,24 +15,11 @@
element $\zero$ is defined. *}
consts
- prod :: "[real, 'a] => 'a" (infixr "'(*')" 70)
- zero :: 'a ("00")
+ prod :: "[real, 'a::{plus, minus, zero}] => 'a" (infixr "'(*')" 70)
syntax (symbols)
- prod :: "[real, 'a] => 'a" (infixr "\<prod>" 70)
- zero :: 'a ("\<zero>")
-
-(* text {* The unary and binary minus can be considered as
-abbreviations: *}
-*)
+ prod :: "[real, 'a] => 'a" (infixr "\<cdot>" 70)
-(***
-constdefs
- negate :: "'a => 'a" ("- _" [100] 100)
- "- x == (- #1) ( * ) x"
- diff :: "'a => 'a => 'a" (infixl "-" 68)
- "x - y == x + - y";
-***)
subsection {* Vector space laws *}
@@ -47,43 +34,43 @@
*}
constdefs
- is_vectorspace :: "('a::{plus,minus}) set => bool"
- "is_vectorspace V == V ~= {}
- & (ALL x:V. ALL y:V. ALL z:V. ALL a b.
- x + y : V
- & a (*) x : V
- & (x + y) + z = x + (y + z)
- & x + y = y + x
- & x - x = 00
- & 00 + x = x
- & a (*) (x + y) = a (*) x + a (*) y
- & (a + b) (*) x = a (*) x + b (*) x
- & (a * b) (*) x = a (*) b (*) x
- & #1 (*) x = x
- & - x = (- #1) (*) x
- & x - y = x + - y)"
+ is_vectorspace :: "('a::{plus, minus, zero}) set => bool"
+ "is_vectorspace V == V \<noteq> {}
+ \<and> (\<forall>x \<in> V. \<forall>y \<in> V. \<forall>z \<in> V. \<forall>a b.
+ x + y \<in> V
+ \<and> a \<cdot> x \<in> V
+ \<and> (x + y) + z = x + (y + z)
+ \<and> x + y = y + x
+ \<and> x - x = 0
+ \<and> 0 + x = x
+ \<and> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y
+ \<and> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x
+ \<and> (a * b) \<cdot> x = a \<cdot> b \<cdot> x
+ \<and> #1 \<cdot> x = x
+ \<and> - x = (- #1) \<cdot> x
+ \<and> x - y = x + - y)"
text_raw {* \medskip *}
text {* The corresponding introduction rule is:*}
lemma vsI [intro]:
- "[| 00:V;
- ALL x:V. ALL y:V. x + y : V;
- ALL x:V. ALL a. a (*) x : V;
- ALL x:V. ALL y:V. ALL z:V. (x + y) + z = x + (y + z);
- ALL x:V. ALL y:V. x + y = y + x;
- ALL x:V. x - x = 00;
- ALL x:V. 00 + x = x;
- ALL x:V. ALL y:V. ALL a. a (*) (x + y) = a (*) x + a (*) y;
- ALL x:V. ALL a b. (a + b) (*) x = a (*) x + b (*) x;
- ALL x:V. ALL a b. (a * b) (*) x = a (*) b (*) x;
- ALL x:V. #1 (*) x = x;
- ALL x:V. - x = (- #1) (*) x;
- ALL x:V. ALL y:V. x - y = x + - y |] ==> is_vectorspace V"
+ "[| 0 \<in> V;
+ \<forall>x \<in> V. \<forall>y \<in> V. x + y \<in> V;
+ \<forall>x \<in> V. \<forall>a. a \<cdot> x \<in> V;
+ \<forall>x \<in> V. \<forall>y \<in> V. \<forall>z \<in> V. (x + y) + z = x + (y + z);
+ \<forall>x \<in> V. \<forall>y \<in> V. x + y = y + x;
+ \<forall>x \<in> V. x - x = 0;
+ \<forall>x \<in> V. 0 + x = x;
+ \<forall>x \<in> V. \<forall>y \<in> V. \<forall>a. a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y;
+ \<forall>x \<in> V. \<forall>a b. (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x;
+ \<forall>x \<in> V. \<forall>a b. (a * b) \<cdot> x = a \<cdot> b \<cdot> x;
+ \<forall>x \<in> V. #1 \<cdot> x = x;
+ \<forall>x \<in> V. - x = (- #1) \<cdot> x;
+ \<forall>x \<in> V. \<forall>y \<in> V. x - y = x + - y |] ==> is_vectorspace V"
proof (unfold is_vectorspace_def, intro conjI ballI allI)
fix x y z
- assume "x:V" "y:V" "z:V"
- "ALL x:V. ALL y:V. ALL z:V. x + y + z = x + (y + z)"
+ assume "x \<in> V" "y \<in> V" "z \<in> V"
+ "\<forall>x \<in> V. \<forall>y \<in> V. \<forall>z \<in> V. x + y + z = x + (y + z)"
thus "x + y + z = x + (y + z)" by (elim bspec[elimify])
qed force+
@@ -91,58 +78,58 @@
text {* The corresponding destruction rules are: *}
lemma negate_eq1:
- "[| is_vectorspace V; x:V |] ==> - x = (- #1) (*) x"
+ "[| is_vectorspace V; x \<in> V |] ==> - x = (- #1) \<cdot> x"
by (unfold is_vectorspace_def) simp
lemma diff_eq1:
- "[| is_vectorspace V; x:V; y:V |] ==> x - y = x + - y"
+ "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x - y = x + - y"
by (unfold is_vectorspace_def) simp
lemma negate_eq2:
- "[| is_vectorspace V; x:V |] ==> (- #1) (*) x = - x"
+ "[| is_vectorspace V; x \<in> V |] ==> (- #1) \<cdot> x = - x"
by (unfold is_vectorspace_def) simp
lemma negate_eq2a:
- "[| is_vectorspace V; x:V |] ==> #-1 (*) x = - x"
+ "[| is_vectorspace V; x \<in> V |] ==> #-1 \<cdot> x = - x"
by (unfold is_vectorspace_def) simp
lemma diff_eq2:
- "[| is_vectorspace V; x:V; y:V |] ==> x + - y = x - y"
+ "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x + - y = x - y"
by (unfold is_vectorspace_def) simp
-lemma vs_not_empty [intro??]: "is_vectorspace V ==> (V ~= {})"
+lemma vs_not_empty [intro??]: "is_vectorspace V ==> (V \<noteq> {})"
by (unfold is_vectorspace_def) simp
lemma vs_add_closed [simp, intro??]:
- "[| is_vectorspace V; x:V; y:V |] ==> x + y : V"
+ "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x + y \<in> V"
by (unfold is_vectorspace_def) simp
lemma vs_mult_closed [simp, intro??]:
- "[| is_vectorspace V; x:V |] ==> a (*) x : V"
+ "[| is_vectorspace V; x \<in> V |] ==> a \<cdot> x \<in> V"
by (unfold is_vectorspace_def) simp
lemma vs_diff_closed [simp, intro??]:
- "[| is_vectorspace V; x:V; y:V |] ==> x - y : V"
+ "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x - y \<in> V"
by (simp add: diff_eq1 negate_eq1)
lemma vs_neg_closed [simp, intro??]:
- "[| is_vectorspace V; x:V |] ==> - x : V"
+ "[| is_vectorspace V; x \<in> V |] ==> - x \<in> V"
by (simp add: negate_eq1)
lemma vs_add_assoc [simp]:
- "[| is_vectorspace V; x:V; y:V; z:V |]
+ "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |]
==> (x + y) + z = x + (y + z)"
by (unfold is_vectorspace_def) fast
lemma vs_add_commute [simp]:
- "[| is_vectorspace V; x:V; y:V |] ==> y + x = x + y"
+ "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> y + x = x + y"
by (unfold is_vectorspace_def) simp
lemma vs_add_left_commute [simp]:
- "[| is_vectorspace V; x:V; y:V; z:V |]
+ "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |]
==> x + (y + z) = y + (x + z)"
proof -
- assume "is_vectorspace V" "x:V" "y:V" "z:V"
+ assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
hence "x + (y + z) = (x + y) + z"
by (simp only: vs_add_assoc)
also have "... = (y + x) + z" by (simp! only: vs_add_commute)
@@ -153,78 +140,78 @@
theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute
lemma vs_diff_self [simp]:
- "[| is_vectorspace V; x:V |] ==> x - x = 00"
+ "[| is_vectorspace V; x \<in> V |] ==> x - x = 0"
by (unfold is_vectorspace_def) simp
text {* The existence of the zero element of a vector space
follows from the non-emptiness of carrier set. *}
-lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> 00:V"
+lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> 0 \<in> V"
proof -
assume "is_vectorspace V"
- have "V ~= {}" ..
- hence "EX x. x:V" by force
+ have "V \<noteq> {}" ..
+ hence "\<exists>x. x \<in> V" by force
thus ?thesis
proof
- fix x assume "x:V"
- have "00 = x - x" by (simp!)
- also have "... : V" by (simp! only: vs_diff_closed)
+ fix x assume "x \<in> V"
+ have "0 = x - x" by (simp!)
+ also have "... \<in> V" by (simp! only: vs_diff_closed)
finally show ?thesis .
qed
qed
lemma vs_add_zero_left [simp]:
- "[| is_vectorspace V; x:V |] ==> 00 + x = x"
+ "[| is_vectorspace V; x \<in> V |] ==> 0 + x = x"
by (unfold is_vectorspace_def) simp
lemma vs_add_zero_right [simp]:
- "[| is_vectorspace V; x:V |] ==> x + 00 = x"
+ "[| is_vectorspace V; x \<in> V |] ==> x + 0 = x"
proof -
- assume "is_vectorspace V" "x:V"
- hence "x + 00 = 00 + x" by simp
+ assume "is_vectorspace V" "x \<in> V"
+ hence "x + 0 = 0 + x" by simp
also have "... = x" by (simp!)
finally show ?thesis .
qed
lemma vs_add_mult_distrib1:
- "[| is_vectorspace V; x:V; y:V |]
- ==> a (*) (x + y) = a (*) x + a (*) y"
+ "[| is_vectorspace V; x \<in> V; y \<in> V |]
+ ==> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y"
by (unfold is_vectorspace_def) simp
lemma vs_add_mult_distrib2:
- "[| is_vectorspace V; x:V |]
- ==> (a + b) (*) x = a (*) x + b (*) x"
+ "[| is_vectorspace V; x \<in> V |]
+ ==> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x"
by (unfold is_vectorspace_def) simp
lemma vs_mult_assoc:
- "[| is_vectorspace V; x:V |] ==> (a * b) (*) x = a (*) (b (*) x)"
+ "[| is_vectorspace V; x \<in> V |] ==> (a * b) \<cdot> x = a \<cdot> (b \<cdot> x)"
by (unfold is_vectorspace_def) simp
lemma vs_mult_assoc2 [simp]:
- "[| is_vectorspace V; x:V |] ==> a (*) b (*) x = (a * b) (*) x"
+ "[| is_vectorspace V; x \<in> V |] ==> a \<cdot> b \<cdot> x = (a * b) \<cdot> x"
by (simp only: vs_mult_assoc)
lemma vs_mult_1 [simp]:
- "[| is_vectorspace V; x:V |] ==> #1 (*) x = x"
+ "[| is_vectorspace V; x \<in> V |] ==> #1 \<cdot> x = x"
by (unfold is_vectorspace_def) simp
lemma vs_diff_mult_distrib1:
- "[| is_vectorspace V; x:V; y:V |]
- ==> a (*) (x - y) = a (*) x - a (*) y"
+ "[| is_vectorspace V; x \<in> V; y \<in> V |]
+ ==> a \<cdot> (x - y) = a \<cdot> x - a \<cdot> y"
by (simp add: diff_eq1 negate_eq1 vs_add_mult_distrib1)
lemma vs_diff_mult_distrib2:
- "[| is_vectorspace V; x:V |]
- ==> (a - b) (*) x = a (*) x - (b (*) x)"
+ "[| is_vectorspace V; x \<in> V |]
+ ==> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)"
proof -
- assume "is_vectorspace V" "x:V"
- have " (a - b) (*) x = (a + - b) (*) x"
+ assume "is_vectorspace V" "x \<in> V"
+ have " (a - b) \<cdot> x = (a + - b) \<cdot> x"
by (unfold real_diff_def, simp)
- also have "... = a (*) x + (- b) (*) x"
+ also have "... = a \<cdot> x + (- b) \<cdot> x"
by (rule vs_add_mult_distrib2)
- also have "... = a (*) x + - (b (*) x)"
+ also have "... = a \<cdot> x + - (b \<cdot> x)"
by (simp! add: negate_eq1)
- also have "... = a (*) x - (b (*) x)"
+ also have "... = a \<cdot> x - (b \<cdot> x)"
by (simp! add: diff_eq1)
finally show ?thesis .
qed
@@ -234,40 +221,40 @@
text{* Further derived laws: *}
lemma vs_mult_zero_left [simp]:
- "[| is_vectorspace V; x:V |] ==> #0 (*) x = 00"
+ "[| is_vectorspace V; x \<in> V |] ==> #0 \<cdot> x = 0"
proof -
- assume "is_vectorspace V" "x:V"
- have "#0 (*) x = (#1 - #1) (*) x" by simp
- also have "... = (#1 + - #1) (*) x" by simp
- also have "... = #1 (*) x + (- #1) (*) x"
+ assume "is_vectorspace V" "x \<in> V"
+ have "#0 \<cdot> x = (#1 - #1) \<cdot> x" by simp
+ also have "... = (#1 + - #1) \<cdot> x" by simp
+ also have "... = #1 \<cdot> x + (- #1) \<cdot> x"
by (rule vs_add_mult_distrib2)
- also have "... = x + (- #1) (*) x" by (simp!)
+ also have "... = x + (- #1) \<cdot> x" by (simp!)
also have "... = x + - x" by (simp! add: negate_eq2a)
also have "... = x - x" by (simp! add: diff_eq2)
- also have "... = 00" by (simp!)
+ also have "... = 0" by (simp!)
finally show ?thesis .
qed
lemma vs_mult_zero_right [simp]:
- "[| is_vectorspace (V:: 'a::{plus, minus} set) |]
- ==> a (*) 00 = (00::'a)"
+ "[| is_vectorspace (V:: 'a::{plus, minus, zero} set) |]
+ ==> a \<cdot> 0 = (0::'a)"
proof -
assume "is_vectorspace V"
- have "a (*) 00 = a (*) (00 - (00::'a))" by (simp!)
- also have "... = a (*) 00 - a (*) 00"
+ have "a \<cdot> 0 = a \<cdot> (0 - (0::'a))" by (simp!)
+ also have "... = a \<cdot> 0 - a \<cdot> 0"
by (rule vs_diff_mult_distrib1) (simp!)+
- also have "... = 00" by (simp!)
+ also have "... = 0" by (simp!)
finally show ?thesis .
qed
lemma vs_minus_mult_cancel [simp]:
- "[| is_vectorspace V; x:V |] ==> (- a) (*) - x = a (*) x"
+ "[| is_vectorspace V; x \<in> V |] ==> (- a) \<cdot> - x = a \<cdot> x"
by (simp add: negate_eq1)
lemma vs_add_minus_left_eq_diff:
- "[| is_vectorspace V; x:V; y:V |] ==> - x + y = y - x"
+ "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> - x + y = y - x"
proof -
- assume "is_vectorspace V" "x:V" "y:V"
+ assume "is_vectorspace V" "x \<in> V" "y \<in> V"
have "- x + y = y + - x"
by (simp! add: vs_add_commute [RS sym, of V "- x"])
also have "... = y - x" by (simp! add: diff_eq1)
@@ -275,63 +262,63 @@
qed
lemma vs_add_minus [simp]:
- "[| is_vectorspace V; x:V |] ==> x + - x = 00"
+ "[| is_vectorspace V; x \<in> V |] ==> x + - x = 0"
by (simp! add: diff_eq2)
lemma vs_add_minus_left [simp]:
- "[| is_vectorspace V; x:V |] ==> - x + x = 00"
+ "[| is_vectorspace V; x \<in> V |] ==> - x + x = 0"
by (simp! add: diff_eq2)
lemma vs_minus_minus [simp]:
- "[| is_vectorspace V; x:V |] ==> - (- x) = x"
+ "[| is_vectorspace V; x \<in> V |] ==> - (- x) = x"
by (simp add: negate_eq1)
lemma vs_minus_zero [simp]:
- "is_vectorspace (V::'a::{minus, plus} set) ==> - (00::'a) = 00"
+ "is_vectorspace (V::'a::{plus, minus, zero} set) ==> - (0::'a) = 0"
by (simp add: negate_eq1)
lemma vs_minus_zero_iff [simp]:
- "[| is_vectorspace V; x:V |] ==> (- x = 00) = (x = 00)"
+ "[| is_vectorspace V; x \<in> V |] ==> (- x = 0) = (x = 0)"
(concl is "?L = ?R")
proof -
- assume "is_vectorspace V" "x:V"
+ assume "is_vectorspace V" "x \<in> V"
show "?L = ?R"
proof
have "x = - (- x)" by (rule vs_minus_minus [RS sym])
also assume ?L
- also have "- ... = 00" by (rule vs_minus_zero)
+ also have "- ... = 0" by (rule vs_minus_zero)
finally show ?R .
qed (simp!)
qed
lemma vs_add_minus_cancel [simp]:
- "[| is_vectorspace V; x:V; y:V |] ==> x + (- x + y) = y"
+ "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x + (- x + y) = y"
by (simp add: vs_add_assoc [RS sym] del: vs_add_commute)
lemma vs_minus_add_cancel [simp]:
- "[| is_vectorspace V; x:V; y:V |] ==> - x + (x + y) = y"
+ "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> - x + (x + y) = y"
by (simp add: vs_add_assoc [RS sym] del: vs_add_commute)
lemma vs_minus_add_distrib [simp]:
- "[| is_vectorspace V; x:V; y:V |]
+ "[| is_vectorspace V; x \<in> V; y \<in> V |]
==> - (x + y) = - x + - y"
by (simp add: negate_eq1 vs_add_mult_distrib1)
lemma vs_diff_zero [simp]:
- "[| is_vectorspace V; x:V |] ==> x - 00 = x"
+ "[| is_vectorspace V; x \<in> V |] ==> x - 0 = x"
by (simp add: diff_eq1)
lemma vs_diff_zero_right [simp]:
- "[| is_vectorspace V; x:V |] ==> 00 - x = - x"
+ "[| is_vectorspace V; x \<in> V |] ==> 0 - x = - x"
by (simp add:diff_eq1)
lemma vs_add_left_cancel:
- "[| is_vectorspace V; x:V; y:V; z:V |]
+ "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |]
==> (x + y = x + z) = (y = z)"
(concl is "?L = ?R")
proof
- assume "is_vectorspace V" "x:V" "y:V" "z:V"
- have "y = 00 + y" by (simp!)
+ assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
+ have "y = 0 + y" by (simp!)
also have "... = - x + x + y" by (simp!)
also have "... = - x + (x + y)"
by (simp! only: vs_add_assoc vs_neg_closed)
@@ -343,68 +330,67 @@
qed force
lemma vs_add_right_cancel:
- "[| is_vectorspace V; x:V; y:V; z:V |]
+ "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |]
==> (y + x = z + x) = (y = z)"
by (simp only: vs_add_commute vs_add_left_cancel)
lemma vs_add_assoc_cong:
- "[| is_vectorspace V; x:V; y:V; x':V; y':V; z:V |]
+ "[| is_vectorspace V; x \<in> V; y \<in> V; x' \<in> V; y' \<in> V; z \<in> V |]
==> x + y = x' + y' ==> x + (y + z) = x' + (y' + z)"
by (simp only: vs_add_assoc [RS sym])
lemma vs_mult_left_commute:
- "[| is_vectorspace V; x:V; y:V; z:V |]
- ==> x (*) y (*) z = y (*) x (*) z"
+ "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |]
+ ==> x \<cdot> y \<cdot> z = y \<cdot> x \<cdot> z"
by (simp add: real_mult_commute)
-lemma vs_mult_zero_uniq :
- "[| is_vectorspace V; x:V; a (*) x = 00; x ~= 00 |] ==> a = #0"
+lemma vs_mult_zero_uniq:
+ "[| is_vectorspace V; x \<in> V; a \<cdot> x = 0; x \<noteq> 0 |] ==> a = #0"
proof (rule classical)
- assume "is_vectorspace V" "x:V" "a (*) x = 00" "x ~= 00"
- assume "a ~= #0"
- have "x = (rinv a * a) (*) x" by (simp!)
- also have "... = rinv a (*) (a (*) x)" by (rule vs_mult_assoc)
- also have "... = rinv a (*) 00" by (simp!)
- also have "... = 00" by (simp!)
- finally have "x = 00" .
+ assume "is_vectorspace V" "x \<in> V" "a \<cdot> x = 0" "x \<noteq> 0"
+ assume "a \<noteq> #0"
+ have "x = (rinv a * a) \<cdot> x" by (simp!)
+ also have "... = rinv a \<cdot> (a \<cdot> x)" by (rule vs_mult_assoc)
+ also have "... = rinv a \<cdot> 0" by (simp!)
+ also have "... = 0" by (simp!)
+ finally have "x = 0" .
thus "a = #0" by contradiction
qed
lemma vs_mult_left_cancel:
- "[| is_vectorspace V; x:V; y:V; a ~= #0 |] ==>
- (a (*) x = a (*) y) = (x = y)"
+ "[| is_vectorspace V; x \<in> V; y \<in> V; a \<noteq> #0 |] ==>
+ (a \<cdot> x = a \<cdot> y) = (x = y)"
(concl is "?L = ?R")
proof
- assume "is_vectorspace V" "x:V" "y:V" "a ~= #0"
- have "x = #1 (*) x" by (simp!)
- also have "... = (rinv a * a) (*) x" by (simp!)
- also have "... = rinv a (*) (a (*) x)"
+ assume "is_vectorspace V" "x \<in> V" "y \<in> V" "a \<noteq> #0"
+ have "x = #1 \<cdot> x" by (simp!)
+ also have "... = (rinv a * a) \<cdot> x" by (simp!)
+ also have "... = rinv a \<cdot> (a \<cdot> x)"
by (simp! only: vs_mult_assoc)
also assume ?L
- also have "rinv a (*) ... = y" by (simp!)
+ also have "rinv a \<cdot> ... = y" by (simp!)
finally show ?R .
qed simp
lemma vs_mult_right_cancel: (*** forward ***)
- "[| is_vectorspace V; x:V; x ~= 00 |]
- ==> (a (*) x = b (*) x) = (a = b)" (concl is "?L = ?R")
+ "[| is_vectorspace V; x \<in> V; x \<noteq> 0 |]
+ ==> (a \<cdot> x = b \<cdot> x) = (a = b)" (concl is "?L = ?R")
proof
- assume "is_vectorspace V" "x:V" "x ~= 00"
- have "(a - b) (*) x = a (*) x - b (*) x"
+ assume "is_vectorspace V" "x \<in> V" "x \<noteq> 0"
+ have "(a - b) \<cdot> x = a \<cdot> x - b \<cdot> x"
by (simp! add: vs_diff_mult_distrib2)
- also assume ?L hence "a (*) x - b (*) x = 00" by (simp!)
- finally have "(a - b) (*) x = 00" .
+ also assume ?L hence "a \<cdot> x - b \<cdot> x = 0" by (simp!)
+ finally have "(a - b) \<cdot> x = 0" .
hence "a - b = #0" by (simp! add: vs_mult_zero_uniq)
thus "a = b" by (rule real_add_minus_eq)
qed simp (***
-backward :
lemma vs_mult_right_cancel:
- "[| is_vectorspace V; x:V; x ~= 00 |] ==>
+ "[| is_vectorspace V; x:V; x \<noteq> 0 |] ==>
(a ( * ) x = b ( * ) x) = (a = b)"
(concl is "?L = ?R");
proof;
- assume "is_vectorspace V" "x:V" "x ~= 00";
+ assume "is_vectorspace V" "x:V" "x \<noteq> 0";
assume l: ?L;
show "a = b";
proof (rule real_add_minus_eq);
@@ -412,8 +398,8 @@
proof (rule vs_mult_zero_uniq);
have "(a - b) ( * ) x = a ( * ) x - b ( * ) x";
by (simp! add: vs_diff_mult_distrib2);
- also; from l; have "a ( * ) x - b ( * ) x = 00"; by (simp!);
- finally; show "(a - b) ( * ) x = 00"; .;
+ also; from l; have "a ( * ) x - b ( * ) x = 0"; by (simp!);
+ finally; show "(a - b) ( * ) x = 0"; .;
qed;
qed;
next;
@@ -423,11 +409,11 @@
**)
lemma vs_eq_diff_eq:
- "[| is_vectorspace V; x:V; y:V; z:V |] ==>
+ "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] ==>
(x = z - y) = (x + y = z)"
(concl is "?L = ?R" )
proof -
- assume vs: "is_vectorspace V" "x:V" "y:V" "z:V"
+ assume vs: "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
show "?L = ?R"
proof
assume ?L
@@ -435,7 +421,7 @@
also have "... = z + - y + y" by (simp! add: diff_eq1)
also have "... = z + (- y + y)"
by (rule vs_add_assoc) (simp!)+
- also from vs have "... = z + 00"
+ also from vs have "... = z + 0"
by (simp only: vs_add_minus_left)
also from vs have "... = z" by (simp only: vs_add_zero_right)
finally show ?R .
@@ -452,32 +438,32 @@
qed
lemma vs_add_minus_eq_minus:
- "[| is_vectorspace V; x:V; y:V; x + y = 00 |] ==> x = - y"
+ "[| is_vectorspace V; x \<in> V; y \<in> V; x + y = 0 |] ==> x = - y"
proof -
- assume "is_vectorspace V" "x:V" "y:V"
+ assume "is_vectorspace V" "x \<in> V" "y \<in> V"
have "x = (- y + y) + x" by (simp!)
also have "... = - y + (x + y)" by (simp!)
- also assume "x + y = 00"
- also have "- y + 00 = - y" by (simp!)
+ also assume "x + y = 0"
+ also have "- y + 0 = - y" by (simp!)
finally show "x = - y" .
qed
lemma vs_add_minus_eq:
- "[| is_vectorspace V; x:V; y:V; x - y = 00 |] ==> x = y"
+ "[| is_vectorspace V; x \<in> V; y \<in> V; x - y = 0 |] ==> x = y"
proof -
- assume "is_vectorspace V" "x:V" "y:V" "x - y = 00"
- assume "x - y = 00"
- hence e: "x + - y = 00" by (simp! add: diff_eq1)
+ assume "is_vectorspace V" "x \<in> V" "y \<in> V" "x - y = 0"
+ assume "x - y = 0"
+ hence e: "x + - y = 0" by (simp! add: diff_eq1)
with _ _ _ have "x = - (- y)"
by (rule vs_add_minus_eq_minus) (simp!)+
thus "x = y" by (simp!)
qed
lemma vs_add_diff_swap:
- "[| is_vectorspace V; a:V; b:V; c:V; d:V; a + b = c + d |]
+ "[| is_vectorspace V; a \<in> V; b \<in> V; c \<in> V; d \<in> V; a + b = c + d |]
==> a - c = d - b"
proof -
- assume vs: "is_vectorspace V" "a:V" "b:V" "c:V" "d:V"
+ assume vs: "is_vectorspace V" "a \<in> V" "b \<in> V" "c \<in> V" "d \<in> V"
and eq: "a + b = c + d"
have "- c + (a + b) = - c + (c + d)"
by (simp! add: vs_add_left_cancel)
@@ -487,16 +473,16 @@
by (simp add: vs_add_ac diff_eq1)
also from eq have "... = d + - b"
by (simp! add: vs_add_right_cancel)
- also have "... = d - b" by (simp! add : diff_eq2)
+ also have "... = d - b" by (simp! add: diff_eq2)
finally show "a - c = d - b" .
qed
lemma vs_add_cancel_21:
- "[| is_vectorspace V; x:V; y:V; z:V; u:V |]
+ "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V; u \<in> V |]
==> (x + (y + z) = y + u) = ((x + z) = u)"
(concl is "?L = ?R")
proof -
- assume "is_vectorspace V" "x:V" "y:V""z:V" "u:V"
+ assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V" "u \<in> V"
show "?L = ?R"
proof
have "x + z = - y + y + (x + z)" by (simp!)
@@ -510,20 +496,20 @@
qed
lemma vs_add_cancel_end:
- "[| is_vectorspace V; x:V; y:V; z:V |]
+ "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |]
==> (x + (y + z) = y) = (x = - z)"
(concl is "?L = ?R" )
proof -
- assume "is_vectorspace V" "x:V" "y:V" "z:V"
+ assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
show "?L = ?R"
proof
assume l: ?L
- have "x + z = 00"
+ have "x + z = 0"
proof (rule vs_add_left_cancel [RS iffD1])
have "y + (x + z) = x + (y + z)" by (simp!)
also note l
- also have "y = y + 00" by (simp!)
- finally show "y + (x + z) = y + 00" .
+ also have "y = y + 0" by (simp!)
+ finally show "y + (x + z) = y + 0" .
qed (simp!)+
thus "x = - z" by (simp! add: vs_add_minus_eq_minus)
next