|
(* Title: HOL/Hahn_Banach/Vector_Space.thy
Author: Gertrud Bauer, TU Munich
*)
section \<open>Vector spaces\<close>
theory Vector_Space
imports Complex_Main Bounds
begin
subsection \<open>Signature\<close>
text \<open>
For the definition of real vector spaces a type \<^typ>\<open>'a\<close> of the sort
\<open>{plus, minus, zero}\<close> is considered, on which a real scalar multiplication
\<open>\<cdot>\<close> is declared.
\<close>
consts
prod :: "real \ 'a::{plus,minus,zero} \ 'a" (infixr "\" 70)
subsection \<open>Vector space laws\<close>
text \<open>
A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from \<^typ>\<open>'a\<close> with the
following vector space laws: The set \<open>V\<close> is closed under addition and scalar
multiplication, addition is associative and commutative; \<open>- x\<close> is the
inverse of \<open>x\<close> wrt.\ addition and \<open>0\<close> is the neutral element of addition.
Addition and multiplication are distributive; scalar multiplication is
associative and the real number \<open>1\<close> is the neutral element of scalar
multiplication.
\<close>
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 \<open>
The existence of the zero element of a vector space follows from the
non-emptiness of carrier set.
\<close>
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 \<open>\<^medskip> Further derived laws:\<close>
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
\<Longrightarrow> x + y = x' + y' \<Longrightarrow> 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 \<open>x \<in> V\<close> have "\<dots> = inverse a \<cdot> (a \<cdot> x)" by (rule mult_assoc)
also from ax have "\ = inverse a \ 0" by simp
also have "\ = 0" by simp
finally have "x = 0" .
with \<open>x \<noteq> 0\<close> 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 \ V"
shows "(x = z - y) = (x + y = z)"
proof
assume "x = z - y"
then have "x + y = z - y + y" by simp
also from y z have "\ = z + - y + y"
by (simp add: diff_eq1)
also have "\ = z + (- y + y)"
by (rule add_assoc) (simp_all add: y z)
also from y z have "\ = z + 0"
by (simp only: add_minus_left)
also from z have "\ = z"
by (simp only: add_zero_right)
finally show "x + y = z" .
next
assume "x + y = z"
then have "z - y = (x + y) - y" by simp
also from x y have "\ = x + y + - y"
by (simp add: diff_eq1)
also have "\ = x + (y + - y)"
by (rule add_assoc) (simp_all add: x y)
also from x y have "\ = x" by simp
finally show "x = z - y" ..
qed
lemma add_minus_eq_minus:
assumes x: "x \ V" and y: "y \ V" and xy: "x + y = 0"
shows "x = - y"
proof -
from x y have "x = (- y + y) + x" by simp
also from x y have "\ = - y + (x + y)" by (simp add: add_ac)
also note xy
also from y have "- y + 0 = - y" by simp
finally show "x = - y" .
qed
lemma add_minus_eq:
assumes x: "x \ V" and y: "y \ V" and xy: "x - y = 0"
shows "x = y"
proof -
from x y xy have eq: "x + - y = 0" by (simp add: diff_eq1)
with _ _ have "x = - (- y)"
by (rule add_minus_eq_minus) (simp_all add: x y)
with x y show "x = y" by simp
qed
lemma add_diff_swap:
assumes vs: "a \ V" "b \ V" "c \ V" "d \ V"
and eq: "a + b = c + d"
shows "a - c = d - b"
proof -
from assms have "- c + (a + b) = - c + (c + d)"
by (simp add: add_left_cancel)
also have "\ = d" using \c \ V\ \d \ V\ by (rule minus_add_cancel)
finally have eq: "- c + (a + b) = d" .
from vs have "a - c = (- c + (a + b)) + - b"
by (simp add: add_ac diff_eq1)
also from vs eq have "\ = d + - b"
by (simp add: add_right_cancel)
also from vs have "\ = d - b" by (simp add: diff_eq2)
finally show "a - c = d - b" .
qed
lemma vs_add_cancel_21:
assumes vs: "x \ V" "y \ V" "z \ V" "u \ V"
shows "(x + (y + z) = y + u) = (x + z = u)"
proof
from vs have "x + z = - y + y + (x + z)" by simp
also have "\ = - y + (y + (x + z))"
by (rule add_assoc) (simp_all add: vs)
also from vs have "y + (x + z) = x + (y + z)"
by (simp add: add_ac)
also assume "x + (y + z) = y + u"
also from vs have "- y + (y + u) = u" by simp
finally show "x + z = u" .
next
assume "x + z = u"
with vs show "x + (y + z) = y + u"
by (simp only: add_left_commute [of x])
qed
lemma add_cancel_end:
assumes vs: "x \ V" "y \ V" "z \ V"
shows "(x + (y + z) = y) = (x = - z)"
proof
assume "x + (y + z) = y"
with vs have "(x + z) + y = 0 + y" by (simp add: add_ac)
with vs have "x + z = 0" by (simp only: add_right_cancel add_closed zero)
with vs show "x = - z" by (simp add: add_minus_eq_minus)
next
assume eq: "x = - z"
then have "x + (y + z) = - z + (y + z)" by simp
also have "\ = y + (- z + z)" by (rule add_left_commute) (simp_all add: vs)
also from vs have "\ = y" by simp
finally show "x + (y + z) = y" .
qed
end
end
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
