Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Vector_Space.thy Sprache: Isabelle

Original von: Isabelle^©

(*  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.19 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.