(* Title: HOL/Hahn_Banach/Vector_Space.thy
Author: Gertrud Bauer, TU Munich
*)
header {* 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 @{text "{plus, minus, zero}"} is considered, on which a real
scalar multiplication @{text \} is declared.
*}
consts
prod :: "real \ 'a::{plus, minus, zero} \ 'a" (infixr "'(*')" 70)
notation (xsymbols)
prod (infixr "\" 70)
notation (HTML output)
prod (infixr "\" 70)
subsection {* Vector space laws *}
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.
*}
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
theorems 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 \ 0` show "a = 0" by contradiction
qed
lemma mult_left_cancel:
assumes x: "x \ V" and y: "y \ V" and a: "a \ 0"
shows "(a \ x = a \ y) = (x = y)"
proof
from x have "x = 1 \ x" by simp
also from a have "\ = (inverse a * a) \ x" by simp
also from x have "\ = inverse a \ (a \ x)"
by (simp only: mult_assoc)
also assume "a \ x = a \ y"
also from a y have "inverse a \ \ = y"
by (simp add: mult_assoc2)
finally show "x = y" .
next
assume "x = y"
then show "a \ x = a \ y" by (simp only:)
qed
lemma mult_right_cancel:
assumes x: "x \ V" and neq: "x \ 0"
shows "(a \ x = b \ x) = (a = b)"
proof
from x have "(a - b) \ x = a \ x - b \ x"
by (simp add: diff_mult_distrib2)
also assume "a \ x = b \ x"
with x have "a \ x - b \ x = 0" by simp
finally have "(a - b) \ x = 0" .
with x neq have "a - b = 0" by (rule mult_zero_uniq)
then show "a = b" by simp
next
assume "a = b"
then show "a \ x = b \ x" by (simp only:)
qed
lemma eq_diff_eq:
assumes x: "x \ V" and y: "y \ V" and z: "z \