src/HOL/Real/HahnBanach/VectorSpace.thy

corrected errors;

(*  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 $\alpha$
of the sort $\{ \idt{plus}, \idt{minus}, \idt{zero}\}$ is considered, on which a
real scalar multiplication $\mult$ is defined. *}

consts
  prod  :: "[real, 'a::{plus, minus, zero}] => 'a"     (infixr "'(*')" 70)

syntax (symbols)
  prod  :: "[real, 'a] => 'a"                          (infixr "\<cdot>" 70)


subsection {* Vector space laws *}

text {* A \emph{vector space} is a non-empty set $V$ of elements from
  $\alpha$ with the following vector space laws: The set $V$ is closed
  under addition and scalar multiplication, addition is associative
  and commutative; $\minus x$ is the inverse of $x$ w.~r.~t.~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.
*}

constdefs
  is_vectorspace :: "('a::{plus, minus, zero}) set => bool"
  "is_vectorspace V == 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_raw {* \medskip *}
text {* The corresponding introduction rule is:*}

lemma vsI [intro]:
  "[| 0 \<in> V; 
  \<forall>x \<in> V. \<forall>y \<in> V. x + y \<in> V; 
  \<forall>x \<in> V. \<forall>a. a \<cdot> x \<in> V;  
  \<forall>x \<in> V. \<forall>y \<in> V. \<forall>z \<in> V. (x + y) + z = x + (y + z);
  \<forall>x \<in> V. \<forall>y \<in> V. x + y = y + x;
  \<forall>x \<in> V. x - x = 0;
  \<forall>x \<in> V. 0 + x = x;
  \<forall>x \<in> V. \<forall>y \<in> V. \<forall>a. a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y;
  \<forall>x \<in> V. \<forall>a b. (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x;
  \<forall>x \<in> V. \<forall>a b. (a * b) \<cdot> x = a \<cdot> b \<cdot> x; 
  \<forall>x \<in> V. #1 \<cdot> x = x; 
  \<forall>x \<in> V. - x = (- #1) \<cdot> x; 
  \<forall>x \<in> V. \<forall>y \<in> V. x - y = x + - y |] ==> is_vectorspace V"
proof (unfold is_vectorspace_def, intro conjI ballI allI)
  fix x y z 
  assume "x \<in> V" "y \<in> V" "z \<in> V"
    "\<forall>x \<in> V. \<forall>y \<in> V. \<forall>z \<in> V. x + y + z = x + (y + z)"
  thus "x + y + z =  x + (y + z)" by blast
qed force+

text_raw {* \medskip *}
text {* The corresponding destruction rules are: *}

lemma negate_eq1: 
  "[| is_vectorspace V; x \<in> V |] ==> - x = (- #1) \<cdot> x"
  by (unfold is_vectorspace_def) simp

lemma diff_eq1: 
  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x - y = x + - y"
  by (unfold is_vectorspace_def) simp 

lemma negate_eq2: 
  "[| is_vectorspace V; x \<in> V |] ==> (- #1) \<cdot> x = - x"
  by (unfold is_vectorspace_def) simp

lemma negate_eq2a: 
  "[| is_vectorspace V; x \<in> V |] ==> #-1 \<cdot> x = - x"
  by (unfold is_vectorspace_def) simp

lemma diff_eq2: 
  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x + - y = x - y"
  by (unfold is_vectorspace_def) simp  

lemma vs_not_empty [intro?]: "is_vectorspace V ==> (V \<noteq> {})" 
  by (unfold is_vectorspace_def) simp
 
lemma vs_add_closed [simp, intro?]: 
  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x + y \<in> V" 
  by (unfold is_vectorspace_def) simp

lemma vs_mult_closed [simp, intro?]: 
  "[| is_vectorspace V; x \<in> V |] ==> a \<cdot> x \<in> V" 
  by (unfold is_vectorspace_def) simp

lemma vs_diff_closed [simp, intro?]: 
 "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> x - y \<in> V"
  by (simp add: diff_eq1 negate_eq1)

lemma vs_neg_closed  [simp, intro?]: 
  "[| is_vectorspace V; x \<in> V |] ==> - x \<in> V"
  by (simp add: negate_eq1)

lemma vs_add_assoc [simp]:  
  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |]
   ==> (x + y) + z = x + (y + z)"
  by (unfold is_vectorspace_def) fast

lemma vs_add_commute [simp]: 
  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> y + x = x + y"
  by (unfold is_vectorspace_def) simp

lemma vs_add_left_commute [simp]:
  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] 
  ==> 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; x \<in> V |] ==>  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 ==> 0 \<in> V"
proof - 
  assume "is_vectorspace V"
  have "V \<noteq> {}" ..
  hence "\<exists>x. x \<in> V" by force
  thus ?thesis 
  proof 
    fix x assume "x \<in> V" 
    have "0 = x - x" by (simp!)
    also have "... \<in> V" by (simp! only: vs_diff_closed)
    finally show ?thesis .
  qed
qed

lemma vs_add_zero_left [simp]: 
  "[| is_vectorspace V; x \<in> V |] ==>  0 + x = x"
  by (unfold is_vectorspace_def) simp

lemma vs_add_zero_right [simp]: 
  "[| is_vectorspace V; x \<in> V |] ==>  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; x \<in> V; y \<in> V |] 
  ==> a \<cdot> (x + y) = a \<cdot> x + a \<cdot> y"
  by (unfold is_vectorspace_def) simp

lemma vs_add_mult_distrib2: 
  "[| is_vectorspace V; x \<in> V |] 
  ==> (a + b) \<cdot> x = a \<cdot> x + b \<cdot> x" 
  by (unfold is_vectorspace_def) simp

lemma vs_mult_assoc: 
  "[| is_vectorspace V; x \<in> V |] ==> (a * b) \<cdot> x = a \<cdot> (b \<cdot> x)"
  by (unfold is_vectorspace_def) simp

lemma vs_mult_assoc2 [simp]: 
 "[| is_vectorspace V; x \<in> V |] ==> a \<cdot> b \<cdot> x = (a * b) \<cdot> x"
  by (simp only: vs_mult_assoc)

lemma vs_mult_1 [simp]: 
  "[| is_vectorspace V; x \<in> V |] ==> #1 \<cdot> x = x" 
  by (unfold is_vectorspace_def) simp

lemma vs_diff_mult_distrib1: 
  "[| is_vectorspace V; x \<in> V; y \<in> V |] 
  ==> 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; x \<in> V |] 
  ==> (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_raw {* \paragraph {Further derived laws.} *}*)
text_raw {* \medskip *}
text{* Further derived laws: *}

lemma vs_mult_zero_left [simp]: 
  "[| is_vectorspace V; x \<in> V |] ==> #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) |] 
  ==> 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; x \<in> V |] ==> (- a) \<cdot> - x = a \<cdot> x"
  by (simp add: negate_eq1)

lemma vs_add_minus_left_eq_diff: 
  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> - 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; x \<in> V |] ==> x + - x = 0"
  by (simp! add: diff_eq2)

lemma vs_add_minus_left [simp]: 
  "[| is_vectorspace V; x \<in> V |] ==> - x + x = 0"
  by (simp! add: diff_eq2)

lemma vs_minus_minus [simp]: 
  "[| is_vectorspace V; x \<in> V |] ==> - (- x) = x"
  by (simp add: negate_eq1)

lemma vs_minus_zero [simp]: 
  "is_vectorspace (V::'a::{plus, minus, zero} set) ==> - (0::'a) = 0" 
  by (simp add: negate_eq1)

lemma vs_minus_zero_iff [simp]:
  "[| is_vectorspace V; x \<in> V |] ==> (- 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; x \<in> V; y \<in> V |] ==> x + (- x + y) = y" 
  by (simp add: vs_add_assoc [symmetric] del: vs_add_commute) 

lemma vs_minus_add_cancel [simp]: 
  "[| is_vectorspace V; x \<in> V; y \<in> V |] ==> - x + (x + y) = y" 
  by (simp add: vs_add_assoc [symmetric] del: vs_add_commute) 

lemma vs_minus_add_distrib [simp]:  
  "[| is_vectorspace V; x \<in> V; y \<in> V |] 
  ==> - (x + y) = - x + - y"
  by (simp add: negate_eq1 vs_add_mult_distrib1)

lemma vs_diff_zero [simp]: 
  "[| is_vectorspace V; x \<in> V |] ==> x - 0 = x"
  by (simp add: diff_eq1)  

lemma vs_diff_zero_right [simp]: 
  "[| is_vectorspace V; x \<in> V |] ==> 0 - x = - x"
  by (simp add:diff_eq1)

lemma vs_add_left_cancel:
  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] 
   ==> (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 force

lemma vs_add_right_cancel: 
  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] 
  ==> (y + x = z + x) = (y = z)"  
  by (simp only: vs_add_commute vs_add_left_cancel)

lemma vs_add_assoc_cong: 
  "[| is_vectorspace V; x \<in> V; y \<in> V; x' \<in> V; y' \<in> V; z \<in> V |] 
  ==> x + y = x' + y' ==> x + (y + z) = x' + (y' + z)"
  by (simp only: vs_add_assoc [symmetric]) 

lemma vs_mult_left_commute: 
  "[| is_vectorspace V; x \<in> V; y \<in> V; z \<in> V |] 
  ==> x \<cdot> y \<cdot> z = y \<cdot> x \<cdot> z"  
  by (simp add: real_mult_commute)

lemma vs_mult_zero_uniq:
  "[| is_vectorspace V; x \<in> V; x \<noteq> 0; a \<cdot> x = 0 |] ==> 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; x \<in> V; y \<in> V; a \<noteq> #0 |] ==> 
  (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; x \<in> V; x \<noteq> 0 |] 
  ==> (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; x \<in> V; y \<in> V; z \<in> V |] ==> 
  (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; x \<in> V; y \<in> V; x + y = 0 |] ==> 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; x \<in> V; y \<in> V; x - y = 0 |] ==> 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; a \<in> V; b \<in> V; c \<in> V; d \<in> V; a + b = c + d |] 
  ==> 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; x \<in> V; y \<in> V; z \<in> V; u \<in> V |] 
  ==> (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; x \<in> V; y \<in> V; z \<in> V |] 
  ==> (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