src/HOL/Real/HahnBanach/VectorSpace.thy

tuned;

(*  Title:      HOL/Real/HahnBanach/VectorSpace.thy
    ID:         $Id$
    Author:     Gertrud Bauer, TU Munich
*)

header {* Vector spaces *}

theory VectorSpace = Bounds + Aux:

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 \<cdot>} is declared.
*}

consts
  prod  :: "real \<Rightarrow> 'a::{plus, minus, zero} \<Rightarrow> 'a"     (infixr "'(*')" 70)

syntax (xsymbols)
  prod  :: "real \<Rightarrow> 'a \<Rightarrow> 'a"                          (infixr "\<cdot>" 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.
*}

constdefs
  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
      \<and> 1 \<cdot> x = x
      \<and> - x = (- 1) \<cdot> x
      \<and> x - y = x + - y)"


text {* \medskip The corresponding introduction rule is:*}

lemma vsI [intro]:
  "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 {* \medskip The corresponding destruction rules are: *}

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 negate_eq2:
  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> (- 1) \<cdot> x = - x"
  by (unfold is_vectorspace_def) simp

lemma negate_eq2a:
  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> -1 \<cdot> x = - x"
  by (unfold is_vectorspace_def) simp

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 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_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_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 \<Longrightarrow> x \<in> V \<Longrightarrow> - x \<in> V"
  by (simp add: negate_eq1)

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 \<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 \<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"
    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)
  finally show ?thesis .
qed

theorems vs_add_ac = vs_add_assoc vs_add_commute vs_add_left_commute

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 \<Longrightarrow> 0 \<in> V"
proof -
  assume "is_vectorspace V"
  have "V \<noteq> {}" ..
  then obtain x where "x \<in> V" by blast
  have "0 = x - x" by (simp!)
  also have "... \<in> V" by (simp! only: vs_diff_closed)
  finally show ?thesis .
qed

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 \<Longrightarrow> x \<in> V \<Longrightarrow>  x + 0 = x"
proof -
  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 \<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 \<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 \<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 \<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 \<Longrightarrow> x \<in> V \<Longrightarrow> 1 \<cdot> x = x"
  by (unfold is_vectorspace_def) simp

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 \<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"
    by (unfold real_diff_def, simp)
  also have "... = a \<cdot> x + (- b) \<cdot> x"
    by (rule vs_add_mult_distrib2)
  also have "... = a \<cdot> x + - (b \<cdot> x)"
    by (simp! add: negate_eq1)
  also have "... = a \<cdot> x - (b \<cdot> x)"
    by (simp! add: diff_eq1)
  finally show ?thesis .
qed


text {* \medskip Further derived laws: *}

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"
  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"
    by (rule vs_add_mult_distrib2)
  also have "... = x + (- 1) \<cdot> x" by (simp!)
  also have "... = x + - x" by (simp! add: negate_eq2a)
  also have "... = x - x" by (simp! add: diff_eq2)
  also have "... = 0" by (simp!)
  finally show ?thesis .
qed

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!)
  also have "... =  a \<cdot> 0 - a \<cdot> 0"
     by (rule vs_diff_mult_distrib1) (simp!)+
  also have "... = 0" by (simp!)
  finally show ?thesis .
qed

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 \<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 \<Longrightarrow> x \<in> V \<Longrightarrow> x + - x = 0"
  by (simp! add: diff_eq2)

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 \<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) \<Longrightarrow> - (0::'a) = 0"
  by (simp add: negate_eq1)

lemma vs_minus_zero_iff [simp]:
  "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> (- x = 0) = (x = 0)"
  (concl is "?L = ?R")
proof -
  assume "is_vectorspace V"  "x \<in> V"
  show "?L = ?R"
  proof
    have "x = - (- x)" by (simp! add: vs_minus_minus)
    also assume ?L
    also have "- ... = 0" by (rule vs_minus_zero)
    finally show ?R .
  qed (simp!)
qed

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 \<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 \<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 \<Longrightarrow> x \<in> V \<Longrightarrow> x - 0 = x"
  by (simp add: diff_eq1)

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 \<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"
  have "y = 0 + y" by (simp!)
  also have "... = - x + x + y" by (simp!)
  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"
    by (simp! only: vs_add_assoc [symmetric] vs_neg_closed)
  also have "... = z" by (simp!)
  finally show ?R .
qed blast

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 \<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 \<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 \<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 "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
qed

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"
  have "x = 1 \<cdot> x" by (simp!)
  also have "... = (inverse a * a) \<cdot> x" by (simp!)
  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!)
  finally show ?R .
qed simp

lemma vs_mult_right_cancel: (*** forward ***)
  "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"
    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)
  thus "a = b" by simp
qed simp

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" )
proof -
  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)"
      by (rule vs_add_assoc) (simp!)+
    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"
      by (simp add: diff_eq1)
    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 \<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"
  have "x = (- y + y) + x" by (simp!)
  also have "... = - y + (x + y)" by (simp!)
  also assume "x + y = 0"
  also have "- y + 0 = - y" by (simp!)
  finally show "x = - y" .
qed

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 "x - y = 0"
  hence e: "x + - y = 0" by (simp! add: diff_eq1)
  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 \<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)"
    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"
    by (simp add: vs_add_ac diff_eq1)
  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 \<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!)
    also have "... = - y + (y + (x + z))"
      by (rule vs_add_assoc) (simp!)+
    also have "y + (x + z) = x + (y + z)" by (simp!)
    also assume ?L
    also have "- y + (y + u) = u" by (simp!)
    finally show ?R .
  qed (simp! only: vs_add_left_commute [of V x])
qed

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"
  show "?L = ?R"
  proof
    assume l: ?L
    have "x + z = 0"
    proof (rule vs_add_left_cancel [THEN iffD1])
      have "y + (x + z) = x + (y + z)" by (simp!)
      also note l
      also have "y = y + 0" by (simp!)
      finally show "y + (x + z) = y + 0" .
    qed (simp!)+
    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)"
      by (simp! only: vs_add_left_commute)
    also have "... = y"  by (simp!)
    finally show ?L .
  qed
qed

end