--- a/src/HOL/Real/HahnBanach/VectorSpace.thy Mon Jul 17 15:06:08 2000 +0200
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Mon Jul 17 18:17:54 2000 +0200
@@ -10,15 +10,14 @@
subsection {* Signature *}
text {* For the definition of real vector spaces a type $\alpha$
-of the sort $\{ \idt{plus}, \idt{minus}\}$ is considered, on which a
-real scalar multiplication $\mult$, and a zero
-element $\zero$ is defined. *}
+of the sort $\{ \idt{plus}, \idt{minus}, \idt{zero}\}$ is considered, on which a
+real scalar multiplication $\mult$ is defined. *}
consts
- prod :: "[real, 'a::{plus, minus, zero}] => 'a" (infixr "'(*')" 70)
+ prod :: "[real, 'a::{plus, minus, zero}] => 'a" (infixr "'(*')" 70)
syntax (symbols)
- prod :: "[real, 'a] => 'a" (infixr "\<cdot>" 70)
+ prod :: "[real, 'a] => 'a" (infixr "\\<cdot>" 70)
subsection {* Vector space laws *}
@@ -27,7 +26,7 @@
$\alpha$ with the following vector space laws: The set $V$ is closed
under addition and scalar multiplication, addition is associative
and commutative; $\minus x$ is the inverse of $x$ w.~r.~t.~addition
- and $\zero$ is the neutral element of addition. Addition and
+ and $0$ is the neutral element of addition. Addition and
multiplication are distributive; scalar multiplication is
associative and the real number $1$ is the neutral element of scalar
multiplication.
@@ -35,42 +34,42 @@
constdefs
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)"
+ "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]:
- "[| 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"
+ "[| 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 \<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)"
+ 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+
@@ -78,58 +77,58 @@
text {* The corresponding destruction rules are: *}
lemma negate_eq1:
- "[| is_vectorspace V; x \<in> V |] ==> - x = (- #1) \<cdot> x"
+ "[| is_vectorspace V; x \\<in> V |] ==> - x = (- #1) \\<cdot> x"
by (unfold is_vectorspace_def) simp
lemma diff_eq1:
- "[| is_vectorspace V; x \<in> V; y \<in> 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 \<in> V |] ==> (- #1) \<cdot> 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 \<in> V |] ==> #-1 \<cdot> 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 \<in> V; y \<in> 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 \<noteq> {})"
+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 \<in> V; y \<in> V |] ==> x + y \<in> 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 \<in> V |] ==> a \<cdot> x \<in> 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 \<in> V; y \<in> V |] ==> x - y \<in> 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 \<in> V |] ==> - x \<in> V"
+ "[| is_vectorspace V; x \\<in> V |] ==> - x \\<in> V"
by (simp add: negate_eq1)
lemma vs_add_assoc [simp]:
- "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> 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 \<in> V; y \<in> 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 \<in> V; y \<in> V; z \<in> 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 \<in> V" "y \<in> V" "z \<in> 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)
@@ -140,78 +139,78 @@
theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute
lemma vs_diff_self [simp]:
- "[| is_vectorspace V; x \<in> V |] ==> x - x = 0"
+ "[| 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 ==> 0 \<in> V"
+lemma zero_in_vs [simp, intro]: "is_vectorspace V ==> 0 \\<in> V"
proof -
assume "is_vectorspace V"
- have "V \<noteq> {}" ..
- hence "\<exists>x. x \<in> V" by force
+ have "V \\<noteq> {}" ..
+ hence "\\<exists>x. x \\<in> V" by force
thus ?thesis
proof
- fix x assume "x \<in> V"
+ fix x assume "x \\<in> V"
have "0 = x - x" by (simp!)
- also have "... \<in> V" by (simp! only: vs_diff_closed)
+ 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 \<in> V |] ==> 0 + 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 \<in> V |] ==> x + 0 = x"
+ "[| is_vectorspace V; x \\<in> V |] ==> x + 0 = x"
proof -
- assume "is_vectorspace V" "x \<in> V"
+ 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 \<in> V; y \<in> V |]
- ==> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> 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 \<in> V |]
- ==> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> 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 \<in> V |] ==> (a * b) \<cdot> x = a \<cdot> (b \<cdot> 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 \<in> V |] ==> a \<cdot> b \<cdot> x = (a * b) \<cdot> 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 \<in> V |] ==> #1 \<cdot> 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 \<in> V; y \<in> V |]
- ==> a \<cdot> (x - y) = a \<cdot> x - a \<cdot> 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 \<in> V |]
- ==> (a - b) \<cdot> x = a \<cdot> x - (b \<cdot> x)"
+ "[| is_vectorspace V; x \\<in> V |]
+ ==> (a - b) \\<cdot> x = a \\<cdot> x - (b \\<cdot> x)"
proof -
- assume "is_vectorspace V" "x \<in> V"
- have " (a - b) \<cdot> x = (a + - b) \<cdot> 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 \<cdot> x + (- b) \<cdot> x"
+ also have "... = a \\<cdot> x + (- b) \\<cdot> x"
by (rule vs_add_mult_distrib2)
- also have "... = a \<cdot> x + - (b \<cdot> x)"
+ also have "... = a \\<cdot> x + - (b \\<cdot> x)"
by (simp! add: negate_eq1)
- also have "... = a \<cdot> x - (b \<cdot> x)"
+ also have "... = a \\<cdot> x - (b \\<cdot> x)"
by (simp! add: diff_eq1)
finally show ?thesis .
qed
@@ -221,14 +220,14 @@
text{* Further derived laws: *}
lemma vs_mult_zero_left [simp]:
- "[| is_vectorspace V; x \<in> V |] ==> #0 \<cdot> x = 0"
+ "[| is_vectorspace V; x \\<in> V |] ==> #0 \\<cdot> x = 0"
proof -
- 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"
+ 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) \<cdot> 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 "... = 0" by (simp!)
@@ -237,40 +236,40 @@
lemma vs_mult_zero_right [simp]:
"[| is_vectorspace (V:: 'a::{plus, minus, zero} set) |]
- ==> a \<cdot> 0 = (0::'a)"
+ ==> a \\<cdot> 0 = (0::'a)"
proof -
assume "is_vectorspace V"
- have "a \<cdot> 0 = a \<cdot> (0 - (0::'a))" by (simp!)
- also have "... = a \<cdot> 0 - a \<cdot> 0"
+ 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 "... = 0" by (simp!)
finally show ?thesis .
qed
lemma vs_minus_mult_cancel [simp]:
- "[| is_vectorspace V; x \<in> V |] ==> (- a) \<cdot> - x = a \<cdot> 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 \<in> V; y \<in> V |] ==> - x + y = y - x"
+ "[| is_vectorspace V; x \\<in> V; y \\<in> V |] ==> - x + y = y - x"
proof -
- 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"])
+ assume "is_vectorspace V" "x \\<in> V" "y \\<in> V"
+ hence "- x + y = y + - x"
+ by (simp add: vs_add_commute)
also have "... = y - x" by (simp! add: diff_eq1)
finally show ?thesis .
qed
lemma vs_add_minus [simp]:
- "[| is_vectorspace V; x \<in> V |] ==> x + - x = 0"
+ "[| is_vectorspace V; x \\<in> V |] ==> x + - x = 0"
by (simp! add: diff_eq2)
lemma vs_add_minus_left [simp]:
- "[| is_vectorspace V; x \<in> V |] ==> - x + x = 0"
+ "[| is_vectorspace V; x \\<in> V |] ==> - x + x = 0"
by (simp! add: diff_eq2)
lemma vs_minus_minus [simp]:
- "[| is_vectorspace V; x \<in> V |] ==> - (- x) = x"
+ "[| is_vectorspace V; x \\<in> V |] ==> - (- x) = x"
by (simp add: negate_eq1)
lemma vs_minus_zero [simp]:
@@ -278,13 +277,13 @@
by (simp add: negate_eq1)
lemma vs_minus_zero_iff [simp]:
- "[| is_vectorspace V; x \<in> V |] ==> (- x = 0) = (x = 0)"
+ "[| is_vectorspace V; x \\<in> V |] ==> (- x = 0) = (x = 0)"
(concl is "?L = ?R")
proof -
- assume "is_vectorspace V" "x \<in> V"
+ assume "is_vectorspace V" "x \\<in> V"
show "?L = ?R"
proof
- have "x = - (- x)" by (rule vs_minus_minus [RS sym])
+ have "x = - (- x)" by (simp! add: vs_minus_minus)
also assume ?L
also have "- ... = 0" by (rule vs_minus_zero)
finally show ?R .
@@ -292,105 +291,105 @@
qed
lemma vs_add_minus_cancel [simp]:
- "[| is_vectorspace V; x \<in> V; y \<in> 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 \<in> V; y \<in> 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 \<in> V; y \<in> 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 \<in> V |] ==> x - 0 = 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 \<in> V |] ==> 0 - 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 \<in> V; y \<in> V; z \<in> 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 \<in> V" "y \<in> V" "z \<in> V"
+ 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)
- also assume ?L
- also have "- x + ... = - x + x + z"
- by (rule vs_add_assoc [RS sym]) (simp!)+
+ also assume "x + y = x + z"
+ also have "- x + (x + z) = - x + x + z"
+ by (simp! only: vs_add_assoc[RS sym] vs_neg_closed)
also have "... = z" by (simp!)
finally show ?R .
qed force
lemma vs_add_right_cancel:
- "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> 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 \<in> V; y \<in> V; x' \<in> V; y' \<in> V; z \<in> 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 \<in> V; y \<in> V; z \<in> V |]
- ==> x \<cdot> y \<cdot> z = y \<cdot> x \<cdot> 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 \<in> V; a \<cdot> x = 0; x \<noteq> 0 |] ==> a = #0"
+ "[| is_vectorspace V; x \\<in> V; a \\<cdot> x = 0; x \\<noteq> 0 |] ==> a = #0"
proof (rule classical)
- 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!)
+ 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 \<in> V; y \<in> V; a \<noteq> #0 |] ==>
- (a \<cdot> x = a \<cdot> 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 \<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)"
+ 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 \<cdot> ... = 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 \<in> V; x \<noteq> 0 |]
- ==> (a \<cdot> x = b \<cdot> 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 \<in> V" "x \<noteq> 0"
- have "(a - b) \<cdot> x = a \<cdot> x - b \<cdot> 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 \<cdot> x - b \<cdot> x = 0" by (simp!)
- finally have "(a - b) \<cdot> x = 0" .
+ 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 (***
lemma vs_mult_right_cancel:
- "[| is_vectorspace V; x:V; x \<noteq> 0 |] ==>
+ "[| 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 \<noteq> 0";
+ assume "is_vectorspace V" "x:V" "x \\<noteq> 0";
assume l: ?L;
show "a = b";
proof (rule real_add_minus_eq);
@@ -409,11 +408,11 @@
**)
lemma vs_eq_diff_eq:
- "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> 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 \<in> V" "y \<in> V" "z \<in> V"
+ assume vs: "is_vectorspace V" "x \\<in> V" "y \\<in> V" "z \\<in> V"
show "?L = ?R"
proof
assume ?L
@@ -438,9 +437,9 @@
qed
lemma vs_add_minus_eq_minus:
- "[| is_vectorspace V; x \<in> V; y \<in> V; x + y = 0 |] ==> x = - y"
+ "[| is_vectorspace V; x \\<in> V; y \\<in> V; x + y = 0 |] ==> x = - y"
proof -
- assume "is_vectorspace V" "x \<in> V" "y \<in> 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 = 0"
@@ -449,9 +448,9 @@
qed
lemma vs_add_minus_eq:
- "[| is_vectorspace V; x \<in> V; y \<in> V; x - y = 0 |] ==> x = y"
+ "[| is_vectorspace V; x \\<in> V; y \\<in> V; x - y = 0 |] ==> x = y"
proof -
- assume "is_vectorspace V" "x \<in> V" "y \<in> V" "x - y = 0"
+ 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)"
@@ -460,10 +459,10 @@
qed
lemma vs_add_diff_swap:
- "[| is_vectorspace V; a \<in> V; b \<in> V; c \<in> V; d \<in> 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 \<in> V" "b \<in> V" "c \<in> V" "d \<in> 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)
@@ -478,11 +477,11 @@
qed
lemma vs_add_cancel_21:
- "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V; u \<in> 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 \<in> V" "y \<in> V" "z \<in> V" "u \<in> 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!)
@@ -496,11 +495,11 @@
qed
lemma vs_add_cancel_end:
- "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> 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 \<in> V" "y \<in> V" "z \<in> V"
+ assume "is_vectorspace V" "x \\<in> V" "y \\<in> V" "z \\<in> V"
show "?L = ?R"
proof
assume l: ?L