--- a/src/HOL/Real/HahnBanach/VectorSpace.thy Sat Dec 16 21:41:14 2000 +0100
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Sat Dec 16 21:41:51 2000 +0100
@@ -9,127 +9,124 @@
subsection {* Signature *}
-text {* For the definition of real vector spaces a type $\alpha$
-of the sort $\{ \idt{plus}, \idt{minus}, \idt{zero}\}$ is considered, on which a
-real scalar multiplication $\mult$ is defined. *}
+text {*
+ For the definition of real vector spaces a type @{typ 'a} of the
+ sort @{text "{plus, minus, zero}"} is considered, on which a real
+ scalar multiplication @{text \<cdot>} is declared.
+*}
consts
- prod :: "[real, 'a::{plus, minus, zero}] => 'a" (infixr "'(*')" 70)
+ prod :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a" (infixr "'(*')" 70)
syntax (symbols)
- prod :: "[real, 'a] => 'a" (infixr "\<cdot>" 70)
+ prod :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "\<cdot>" 70)
subsection {* Vector space laws *}
-text {* A \emph{vector space} is a non-empty set $V$ of elements from
- $\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 $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.
+text {*
+ A \emph{vector space} is a non-empty set @{text V} of elements from
+ @{typ 'a} with the following vector space laws: The set @{text V} is
+ closed under addition and scalar multiplication, addition is
+ associative and commutative; @{text "- x"} is the inverse of @{text
+ x} w.~r.~t.~addition and @{text 0} is the neutral element of
+ addition. Addition and multiplication are distributive; scalar
+ multiplication is associative and the real number @{text "#1"} is
+ the neutral element of scalar multiplication.
*}
constdefs
- is_vectorspace :: "('a::{plus, minus, zero}) set => bool"
- "is_vectorspace V == V \<noteq> {}
+ is_vectorspace :: "('a::{plus, minus, zero}) set \<Rightarrow> bool"
+ "is_vectorspace V \<equiv> 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
+ 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)"
+ \<and> x - y = x + - y)"
-text_raw {* \medskip *}
-text {* The corresponding introduction rule is:*}
+
+text {* \medskip 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"
-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)"
- thus "x + y + z = x + (y + z)" by blast
-qed force+
+ "0 \<in> V \<Longrightarrow>
+ \<forall>x \<in> V. \<forall>y \<in> V. x + y \<in> V \<Longrightarrow>
+ \<forall>x \<in> V. \<forall>a. a \<cdot> x \<in> V \<Longrightarrow>
+ \<forall>x \<in> V. \<forall>y \<in> V. \<forall>z \<in> V. (x + y) + z = x + (y + z) \<Longrightarrow>
+ \<forall>x \<in> V. \<forall>y \<in> V. x + y = y + x \<Longrightarrow>
+ \<forall>x \<in> V. x - x = 0 \<Longrightarrow>
+ \<forall>x \<in> V. 0 + x = x \<Longrightarrow>
+ \<forall>x \<in> V. \<forall>y \<in> V. \<forall>a. a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y \<Longrightarrow>
+ \<forall>x \<in> V. \<forall>a b. (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x \<Longrightarrow>
+ \<forall>x \<in> V. \<forall>a b. (a * b) \<cdot> x = a \<cdot> b \<cdot> x \<Longrightarrow>
+ \<forall>x \<in> V. #1 \<cdot> x = x \<Longrightarrow>
+ \<forall>x \<in> V. - x = (- #1) \<cdot> x \<Longrightarrow>
+ \<forall>x \<in> V. \<forall>y \<in> V. x - y = x + - y \<Longrightarrow> is_vectorspace V"
+ by (unfold is_vectorspace_def) auto
-text_raw {* \medskip *}
-text {* The corresponding destruction rules are: *}
+text {* \medskip The corresponding destruction rules are: *}
-lemma negate_eq1:
- "[| is_vectorspace V; x \<in> V |] ==> - x = (- #1) \<cdot> x"
+lemma negate_eq1:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> - x = (- #1) \<cdot> x"
+ by (unfold is_vectorspace_def) simp
+
+lemma diff_eq1:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y = x + - y"
by (unfold is_vectorspace_def) simp
-lemma diff_eq1:
- "[| 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 \<Longrightarrow> x \<in> V \<Longrightarrow> (- #1) \<cdot> x = - x"
+ by (unfold is_vectorspace_def) simp
-lemma negate_eq2:
- "[| is_vectorspace V; x \<in> V |] ==> (- #1) \<cdot> x = - x"
+lemma negate_eq2a:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> #-1 \<cdot> x = - x"
by (unfold is_vectorspace_def) simp
-lemma negate_eq2a:
- "[| is_vectorspace V; x \<in> V |] ==> #-1 \<cdot> x = - x"
+lemma diff_eq2:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + - y = x - y"
+ by (unfold is_vectorspace_def) simp
+
+lemma vs_not_empty [intro?]: "is_vectorspace V \<Longrightarrow> (V \<noteq> {})"
by (unfold is_vectorspace_def) simp
-lemma diff_eq2:
- "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x + - y = x - y"
- by (unfold is_vectorspace_def) simp
+lemma vs_add_closed [simp, intro?]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y \<in> V"
+ by (unfold is_vectorspace_def) simp
-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"
+lemma vs_mult_closed [simp, intro?]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> a \<cdot> x \<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"
- 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"
+lemma vs_diff_closed [simp, intro?]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> 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"
+lemma vs_neg_closed [simp, intro?]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> - 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 |]
- ==> (x + y) + z = x + (y + z)"
- by (unfold is_vectorspace_def) fast
+lemma vs_add_assoc [simp]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V
+ \<Longrightarrow> (x + y) + z = x + (y + z)"
+ by (unfold is_vectorspace_def) blast
-lemma vs_add_commute [simp]:
- "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> y + x = x + y"
- by (unfold is_vectorspace_def) simp
+lemma vs_add_commute [simp]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> y + x = x + y"
+ by (unfold is_vectorspace_def) blast
lemma vs_add_left_commute [simp]:
- "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |]
- ==> x + (y + z) = y + (x + z)"
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V
+ \<Longrightarrow> x + (y + z) = y + (x + z)"
proof -
- assume "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
- hence "x + (y + z) = (x + y) + z"
+ 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)
also have "... = y + (x + z)" by (simp! only: vs_add_assoc)
@@ -138,94 +135,93 @@
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"
+lemma vs_diff_self [simp]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> 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"
-proof -
+lemma zero_in_vs [simp, intro]: "is_vectorspace V \<Longrightarrow> 0 \<in> V"
+proof -
assume "is_vectorspace V"
have "V \<noteq> {}" ..
- hence "\<exists>x. x \<in> V" by force
- thus ?thesis
- proof
- fix x assume "x \<in> V"
+ hence "\<exists>x. x \<in> V" by blast
+ thus ?thesis
+ proof
+ 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 \<in> V |] ==> 0 + x = x"
+lemma vs_add_zero_left [simp]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> 0 + x = x"
by (unfold is_vectorspace_def) simp
-lemma vs_add_zero_right [simp]:
- "[| is_vectorspace V; x \<in> V |] ==> x + 0 = x"
+lemma vs_add_zero_right [simp]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> 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"
+lemma vs_add_mult_distrib1:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V
+ \<Longrightarrow> 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"
+lemma vs_add_mult_distrib2:
+ "is_vectorspace V \<Longrightarrow> x \<in> V
+ \<Longrightarrow> (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)"
+lemma vs_mult_assoc:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> (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"
+lemma vs_mult_assoc2 [simp]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> 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"
+lemma vs_mult_1 [simp]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> #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"
+lemma vs_diff_mult_distrib1:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V
+ \<Longrightarrow> 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)"
+lemma vs_diff_mult_distrib2:
+ "is_vectorspace V \<Longrightarrow> x \<in> V
+ \<Longrightarrow> (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
-(*text_raw {* \paragraph {Further derived laws.} *}*)
-text_raw {* \medskip *}
-text{* Further derived laws: *}
+
+text {* \medskip Further derived laws: *}
-lemma vs_mult_zero_left [simp]:
- "[| is_vectorspace V; x \<in> V |] ==> #0 \<cdot> x = 0"
+lemma vs_mult_zero_left [simp]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> #0 \<cdot> x = 0"
proof -
- assume "is_vectorspace V" "x \<in> V"
+ 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"
+ 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 + - x" by (simp! add: negate_eq2a)
@@ -234,9 +230,9 @@
finally show ?thesis .
qed
-lemma vs_mult_zero_right [simp]:
- "[| is_vectorspace (V:: 'a::{plus, minus, zero} set) |]
- ==> a \<cdot> 0 = (0::'a)"
+lemma vs_mult_zero_right [simp]:
+ "is_vectorspace (V:: 'a::{plus, minus, zero} set)
+ \<Longrightarrow> a \<cdot> 0 = (0::'a)"
proof -
assume "is_vectorspace V"
have "a \<cdot> 0 = a \<cdot> (0 - (0::'a))" by (simp!)
@@ -246,41 +242,41 @@
finally show ?thesis .
qed
-lemma vs_minus_mult_cancel [simp]:
- "[| is_vectorspace V; x \<in> V |] ==> (- a) \<cdot> - x = a \<cdot> x"
+lemma vs_minus_mult_cancel [simp]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> (- 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"
-proof -
- assume "is_vectorspace V" "x \<in> V" "y \<in> V"
- hence "- x + y = y + - x"
+lemma vs_add_minus_left_eq_diff:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + y = y - x"
+proof -
+ 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"
+lemma vs_add_minus [simp]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> x + - x = 0"
by (simp! add: diff_eq2)
-lemma vs_add_minus_left [simp]:
- "[| is_vectorspace V; x \<in> V |] ==> - x + x = 0"
+lemma vs_add_minus_left [simp]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> - x + x = 0"
by (simp! add: diff_eq2)
-lemma vs_minus_minus [simp]:
- "[| is_vectorspace V; x \<in> V |] ==> - (- x) = x"
+lemma vs_minus_minus [simp]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> - (- x) = x"
by (simp add: negate_eq1)
-lemma vs_minus_zero [simp]:
- "is_vectorspace (V::'a::{plus, minus, zero} set) ==> - (0::'a) = 0"
+lemma vs_minus_zero [simp]:
+ "is_vectorspace (V::'a::{plus, minus, zero} set) \<Longrightarrow> - (0::'a) = 0"
by (simp add: negate_eq1)
lemma vs_minus_zero_iff [simp]:
- "[| is_vectorspace V; x \<in> V |] ==> (- x = 0) = (x = 0)"
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> (- 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 (simp! add: vs_minus_minus)
@@ -290,81 +286,81 @@
qed (simp!)
qed
-lemma vs_add_minus_cancel [simp]:
- "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x + (- x + y) = y"
- by (simp add: vs_add_assoc [symmetric] del: vs_add_commute)
+lemma vs_add_minus_cancel [simp]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + (- x + y) = y"
+ by (simp add: vs_add_assoc [symmetric] del: vs_add_commute)
-lemma vs_minus_add_cancel [simp]:
- "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> - x + (x + y) = y"
- by (simp add: vs_add_assoc [symmetric] del: vs_add_commute)
+lemma vs_minus_add_cancel [simp]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> - x + (x + y) = y"
+ by (simp add: vs_add_assoc [symmetric] del: vs_add_commute)
-lemma vs_minus_add_distrib [simp]:
- "[| is_vectorspace V; x \<in> V; y \<in> V |]
- ==> - (x + y) = - x + - y"
+lemma vs_minus_add_distrib [simp]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V
+ \<Longrightarrow> - (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"
- by (simp add: diff_eq1)
+lemma vs_diff_zero [simp]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> x - 0 = x"
+ by (simp add: diff_eq1)
-lemma vs_diff_zero_right [simp]:
- "[| is_vectorspace V; x \<in> V |] ==> 0 - x = - x"
+lemma vs_diff_zero_right [simp]:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> 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 |]
- ==> (x + y = x + z) = (y = z)"
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V
+ \<Longrightarrow> (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)"
+ also have "... = - x + (x + y)"
by (simp! only: vs_add_assoc vs_neg_closed)
also assume "x + y = x + z"
- also have "- x + (x + z) = - x + x + z"
+ also have "- x + (x + z) = - x + x + z"
by (simp! only: vs_add_assoc [symmetric] vs_neg_closed)
also have "... = z" by (simp!)
finally show ?R .
-qed force
+qed blast
-lemma vs_add_right_cancel:
- "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |]
- ==> (y + x = z + x) = (y = z)"
+lemma vs_add_right_cancel:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V
+ \<Longrightarrow> (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 |]
- ==> x + y = x' + y' ==> x + (y + z) = x' + (y' + z)"
- by (simp only: vs_add_assoc [symmetric])
+lemma vs_add_assoc_cong:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x' \<in> V \<Longrightarrow> y' \<in> V \<Longrightarrow> z \<in> V
+ \<Longrightarrow> x + y = x' + y' \<Longrightarrow> x + (y + z) = x' + (y' + z)"
+ by (simp only: vs_add_assoc [symmetric])
-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"
+lemma vs_mult_left_commute:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V
+ \<Longrightarrow> 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; x \<noteq> 0; a \<cdot> x = 0 |] ==> a = 0"
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> a \<cdot> x = 0 \<Longrightarrow> a = 0"
proof (rule classical)
- assume "is_vectorspace V" "x \<in> V" "a \<cdot> x = 0" "x \<noteq> 0"
+ assume "is_vectorspace V" "x \<in> V" "a \<cdot> x = 0" "x \<noteq> 0"
assume "a \<noteq> 0"
have "x = (inverse a * a) \<cdot> x" by (simp!)
also have "... = inverse a \<cdot> (a \<cdot> x)" by (rule vs_mult_assoc)
also have "... = inverse a \<cdot> 0" by (simp!)
also have "... = 0" by (simp!)
finally have "x = 0" .
- thus "a = 0" by contradiction
+ thus "a = 0" by contradiction
qed
-lemma vs_mult_left_cancel:
- "[| is_vectorspace V; x \<in> V; y \<in> V; a \<noteq> #0 |] ==>
+lemma vs_mult_left_cancel:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> a \<noteq> #0 \<Longrightarrow>
(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"
+ assume "is_vectorspace V" "x \<in> V" "y \<in> V" "a \<noteq> #0"
have "x = #1 \<cdot> x" by (simp!)
also have "... = (inverse a * a) \<cdot> x" by (simp!)
- also have "... = inverse a \<cdot> (a \<cdot> x)"
+ also have "... = inverse a \<cdot> (a \<cdot> x)"
by (simp! only: vs_mult_assoc)
also assume ?L
also have "inverse a \<cdot> ... = y" by (simp!)
@@ -372,51 +368,51 @@
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 \<Longrightarrow> x \<in> V \<Longrightarrow> x \<noteq> 0
+ \<Longrightarrow> (a \<cdot> x = b \<cdot> x) = (a = b)" (concl is "?L = ?R")
proof
- assume v: "is_vectorspace V" "x \<in> V" "x \<noteq> 0"
- have "(a - b) \<cdot> x = a \<cdot> x - b \<cdot> x"
+ assume v: "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" .
- from v this have "a - b = 0" by (rule vs_mult_zero_uniq)
+ from v this have "a - b = 0" by (rule vs_mult_zero_uniq)
thus "a = b" by simp
-qed simp
+qed simp
-lemma vs_eq_diff_eq:
- "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] ==>
+lemma vs_eq_diff_eq:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow>
(x = z - y) = (x + y = z)"
- (concl is "?L = ?R" )
+ (concl is "?L = ?R" )
proof -
- assume vs: "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
- show "?L = ?R"
+ assume vs: "is_vectorspace V" "x \<in> V" "y \<in> V" "z \<in> V"
+ show "?L = ?R"
proof
assume ?L
hence "x + y = z - y + y" by simp
also have "... = z + - y + y" by (simp! add: diff_eq1)
- also have "... = z + (- y + y)"
+ also have "... = z + (- y + y)"
by (rule vs_add_assoc) (simp!)+
- also from vs have "... = z + 0"
+ 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 .
next
assume ?R
hence "z - y = (x + y) - y" by simp
- also from vs have "... = x + y + - y"
+ also from vs have "... = x + y + - y"
by (simp add: diff_eq1)
- also have "... = x + (y + - y)"
+ also have "... = x + (y + - y)"
by (rule vs_add_assoc) (simp!)+
also have "... = x" by (simp!)
finally show ?L by (rule sym)
qed
qed
-lemma vs_add_minus_eq_minus:
- "[| is_vectorspace V; x \<in> V; y \<in> V; x + y = 0 |] ==> x = - y"
+lemma vs_add_minus_eq_minus:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + y = 0 \<Longrightarrow> 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"
@@ -424,41 +420,41 @@
finally show "x = - y" .
qed
-lemma vs_add_minus_eq:
- "[| is_vectorspace V; x \<in> V; y \<in> V; x - y = 0 |] ==> x = y"
+lemma vs_add_minus_eq:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x - y = 0 \<Longrightarrow> 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)"
+ 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 \<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"
+ "is_vectorspace V \<Longrightarrow> a \<in> V \<Longrightarrow> b \<in> V \<Longrightarrow> c \<in> V \<Longrightarrow> d \<in> V \<Longrightarrow> a + b = c + d
+ \<Longrightarrow> a - c = d - b"
+proof -
+ 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)"
+ have "- c + (a + b) = - c + (c + d)"
by (simp! add: vs_add_left_cancel)
also have "... = d" by (rule vs_minus_add_cancel)
finally have eq: "- c + (a + b) = d" .
- from vs have "a - c = (- c + (a + b)) + - b"
+ from vs have "a - c = (- c + (a + b)) + - b"
by (simp add: vs_add_ac diff_eq1)
- also from eq have "... = d + - b"
+ also from eq have "... = d + - b"
by (simp! add: vs_add_right_cancel)
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 \<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"
+lemma vs_add_cancel_21:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V \<Longrightarrow> u \<in> V
+ \<Longrightarrow> (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"
show "?L = ?R"
proof
have "x + z = - y + y + (x + z)" by (simp!)
@@ -471,16 +467,16 @@
qed (simp! only: vs_add_left_commute [of V x])
qed
-lemma vs_add_cancel_end:
- "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |]
- ==> (x + (y + z) = y) = (x = - z)"
+lemma vs_add_cancel_end:
+ "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> z \<in> V
+ \<Longrightarrow> (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
- have "x + z = 0"
+ have "x + z = 0"
proof (rule vs_add_left_cancel [THEN iffD1])
have "y + (x + z) = x + (y + z)" by (simp!)
also note l
@@ -490,12 +486,12 @@
thus "x = - z" by (simp! add: vs_add_minus_eq_minus)
next
assume r: ?R
- hence "x + (y + z) = - z + (y + z)" by simp
- also have "... = y + (- z + z)"
+ hence "x + (y + z) = - z + (y + z)" by simp
+ also have "... = y + (- z + z)"
by (simp! only: vs_add_left_commute)
also have "... = y" by (simp!)
finally show ?L .
qed
qed
-end
\ No newline at end of file
+end