(* Title: HOL/Hahn_Banach/Vector_Space.thy
Author: Gertrud Bauer, TU Munich
*)
section \Vector spaces\
theory Vector_Space
imports Complex_Main Bounds
begin
subsection \Signature\
text \
For the definition of real vector spaces a type @{typ 'a} of the sort
\{plus, minus, zero}\ is considered, on which a real scalar multiplication
\\\ is declared.
\
consts
prod :: "real \ 'a::{plus,minus,zero} \ 'a" (infixr "\" 70)
subsection \Vector space laws\
text \
A \<^emph>\vector space\ is a non-empty set \V\ of elements from @{typ 'a} with the
following vector space laws: The set \V\ is closed under addition and scalar
multiplication, addition is associative and commutative; \- x\ is the
inverse of \x\ wrt.\ 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.
\
locale vectorspace =
fixes V
assumes non_empty [iff, intro?]: "V \ {}"
and add_closed [iff]: "x \ V \ y \ V \ x + y \ V"
and mult_closed [iff]: "x \ V \ a \ x \ V"
and add_assoc: "x \ V \ y \ V \ z \ V \ (x + y) + z = x + (y + z)"
and add_commute: "x \ V \ y \ V \ x + y = y + x"
and diff_self [simp]: "x \ V \ x - x = 0"
and add_zero_left [simp]: "x \ V \ 0 + x = x"
and add_mult_distrib1: "x \ V \ y \ V \ a \ (x + y) = a \ x + a \ y"
and add_mult_distrib2: "x \ V \ (a + b) \ x = a \ x + b \ x"
and mult_assoc: "x \ V \ (a * b) \ x = a \ (b \ x)"
and mult_1 [simp]: "x \ V \ 1 \ x = x"
and negate_eq1: "x \ V \ - x = (- 1) \ x"
and diff_eq1: "x \ V \ y \ V \ x - y = x + - y"
begin
lemma negate_eq2: "x \ V \ (- 1) \ x = - x"
by (rule negate_eq1 [symmetric])
lemma negate_eq2a: "x \ V \ -1 \ x = - x"
by (simp add: negate_eq1)
lemma diff_eq2: "x \ V \ y \ V \ x + - y = x - y"
by (rule diff_eq1 [symmetric])
lemma diff_closed [iff]: "x \ V \ y \ V \ x - y \ V"
by (simp add: diff_eq1 negate_eq1)
lemma neg_closed [iff]: "x \ V \ - x \ V"
by (simp add: negate_eq1)
lemma add_left_commute:
"x \ V \ y \ V \ z \ V \ x + (y + z) = y + (x + z)"
proof -
assume xyz: "x \ V" "y \ V" "z \ V"
then have "x + (y + z) = (x + y) + z"
by (simp only: add_assoc)
also from xyz have "\ = (y + x) + z" by (simp only: add_commute)
also from xyz have "\ = y + (x + z)" by (simp only: add_assoc)
finally show ?thesis .
qed
lemmas add_ac = add_assoc add_commute add_left_commute
text \
The existence of the zero element of a vector space follows from the
non-emptiness of carrier set.
\
lemma zero [iff]: "0 \ V"
proof -
from non_empty obtain x where x: "x \ V" by blast
then have "0 = x - x" by (rule diff_self [symmetric])
also from x x have "\ \ V" by (rule diff_closed)
finally show ?thesis .
qed
lemma add_zero_right [simp]: "x \ V \ x + 0 = x"
proof -
assume x: "x \ V"
from this and zero have "x + 0 = 0 + x" by (rule add_commute)
also from x have "\ = x" by (rule add_zero_left)
finally show ?thesis .
qed
lemma mult_assoc2: "x \ V \ a \ b \ x = (a * b) \ x"
by (simp only: mult_assoc)
lemma diff_mult_distrib1: "x \ V \ y \ V \ a \ (x - y) = a \ x - a \ y"
by (simp add: diff_eq1 negate_eq1 add_mult_distrib1 mult_assoc2)
lemma diff_mult_distrib2: "x \ V \ (a - b) \ x = a \ x - (b \ x)"
proof -
assume x: "x \ V"
have " (a - b) \ x = (a + - b) \ x"
by simp
also from x have "\ = a \ x + (- b) \ x"
by (rule add_mult_distrib2)
also from x have "\ = a \ x + - (b \ x)"
by (simp add: negate_eq1 mult_assoc2)
also from x have "\ = a \ x - (b \ x)"
by (simp add: diff_eq1)
finally show ?thesis .
qed
lemmas distrib =
add_mult_distrib1 add_mult_distrib2
diff_mult_distrib1 diff_mult_distrib2
text \\<^medskip> Further derived laws:\
lemma mult_zero_left [simp]: "x \ V \ 0 \ x = 0"
proof -
assume x: "x \ V"
have "0 \ x = (1 - 1) \ x" by simp
also have "\ = (1 + - 1) \ x" by simp
also from x have "\ = 1 \ x + (- 1) \ x"
by (rule add_mult_distrib2)
also from x have "\ = x + (- 1) \ x" by simp
also from x have "\ = x + - x" by (simp add: negate_eq2a)
also from x have "\ = x - x" by (simp add: diff_eq2)
also from x have "\ = 0" by simp
finally show ?thesis .
qed
lemma mult_zero_right [simp]: "a \ 0 = (0::'a)"
proof -
have "a \ 0 = a \ (0 - (0::'a))" by simp
also have "\ = a \ 0 - a \ 0"
by (rule diff_mult_distrib1) simp_all
also have "\ = 0" by simp
finally show ?thesis .
qed
lemma minus_mult_cancel [simp]: "x \ V \ (- a) \ - x = a \ x"
by (simp add: negate_eq1 mult_assoc2)
lemma add_minus_left_eq_diff: "x \ V \ y \ V \ - x + y = y - x"
proof -
assume xy: "x \ V" "y \ V"
then have "- x + y = y + - x" by (simp add: add_commute)
also from xy have "\ = y - x" by (simp add: diff_eq1)
finally show ?thesis .
qed
lemma add_minus [simp]: "x \ V \ x + - x = 0"
by (simp add: diff_eq2)
lemma add_minus_left [simp]: "x \ V \ - x + x = 0"
by (simp add: diff_eq2 add_commute)
lemma minus_minus [simp]: "x \ V \ - (- x) = x"
by (simp add: negate_eq1 mult_assoc2)
lemma minus_zero [simp]: "- (0::'a) = 0"
by (simp add: negate_eq1)
lemma minus_zero_iff [simp]:
assumes x: "x \ V"
shows "(- x = 0) = (x = 0)"
proof
from x have "x = - (- x)" by simp
also assume "- x = 0"
also have "- \ = 0" by (rule minus_zero)
finally show "x = 0" .
next
assume "x = 0"
then show "- x = 0" by simp
qed
lemma add_minus_cancel [simp]: "x \ V \ y \ V \ x + (- x + y) = y"
by (simp add: add_assoc [symmetric])
lemma minus_add_cancel [simp]: "x \ V \ y \ V \ - x + (x + y) = y"
by (simp add: add_assoc [symmetric])
lemma minus_add_distrib [simp]: "x \ V \ y \ V \ - (x + y) = - x + - y"
by (simp add: negate_eq1 add_mult_distrib1)
lemma diff_zero [simp]: "x \ V \ x - 0 = x"
by (simp add: diff_eq1)
lemma diff_zero_right [simp]: "x \ V \ 0 - x = - x"
by (simp add: diff_eq1)
lemma add_left_cancel:
assumes x: "x \ V" and y: "y \ V" and z: "z \ V"
shows "(x + y = x + z) = (y = z)"
proof
from y have "y = 0 + y" by simp
also from x y have "\ = (- x + x) + y" by simp
also from x y have "\ = - x + (x + y)" by (simp add: add.assoc)
also assume "x + y = x + z"
also from x z have "- x + (x + z) = - x + x + z" by (simp add: add.assoc)
also from x z have "\ = z" by simp
finally show "y = z" .
next
assume "y = z"
then show "x + y = x + z" by (simp only:)
qed
lemma add_right_cancel:
"x \ V \ y \ V \ z \ V \ (y + x = z + x) = (y = z)"
by (simp only: add_commute add_left_cancel)
lemma add_assoc_cong:
"x \ V \ y \ V \ x' \ V \ y' \ V \ z \ V
\ x + y = x' + y' \ x + (y + z) = x' + (y' + z)"
by (simp only: add_assoc [symmetric])
lemma mult_left_commute: "x \ V \ a \ b \ x = b \ a \ x"
by (simp add: mult.commute mult_assoc2)
lemma mult_zero_uniq:
assumes x: "x \ V" "x \ 0" and ax: "a \ x = 0"
shows "a = 0"
proof (rule classical)
assume a: "a \ 0"
from x a have "x = (inverse a * a) \ x" by simp
also from \x \ V\ have "\ = inverse a \ (a \ x)" by (rule mult_assoc)
also from ax have "\ = inverse a \ 0" by simp
also have "\ = 0" by simp
finally have "x = 0" .
with \x \