(*  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 [RS sym] 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 [RS sym] 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 [RS sym] 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 [RS sym]) 

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; a \\<cdot> x = 0; x \\<noteq> 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 = (rinv a * a) \\<cdot> x" by (simp!)

  also have "... = rinv a \\<cdot> (a \\<cdot> x)" by (rule vs_mult_assoc)

  also have "... = rinv 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 "... = (rinv a * a) \\<cdot> x" by (simp!)

  also have "... = rinv a \\<cdot> (a \\<cdot> x)" 

    by (simp! only: vs_mult_assoc)

  also assume ?L

  also have "rinv 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 "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" . 

  hence "a - b = #0" by (simp! add: vs_mult_zero_uniq)

  thus "a = b" by (rule real_add_minus_eq)

qed simp (*** 

lemma vs_mult_right_cancel: 

  "[| is_vectorspace V; x:V; x \\<noteq> 0 |] ==>  

  (a ( * ) x = b ( * ) x) = (a = b)"

  (concl is "?L = ?R");

proof;

  assume "is_vectorspace V" "x:V" "x \\<noteq> 0";

  assume l: ?L; 

  show "a = b"; 

  proof (rule real_add_minus_eq);

    show "a - b = (#0::real)"; 

    proof (rule vs_mult_zero_uniq);

      have "(a - b) ( * ) x = a ( * ) x - b ( * ) x";

        by (simp! add: vs_diff_mult_distrib2);

      also; from l; have "a ( * ) x - b ( * ) x = 0"; by (simp!);

      finally; show "(a - b) ( * ) x  = 0"; .; 

    qed;

  qed;

next;

  assume ?R;

  thus ?L; by simp;

qed;

**)

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 [RS 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