src/HOL/Real/HahnBanach/VectorSpace.thy

intro/elim/dest attributes: changed ! / !! flags to ? / ??;

(*  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}\}$ is considered, on which a
real scalar multiplication $\mult$, and a zero 
element $\zero$ is defined. *};

consts
  prod  :: "[real, 'a] => 'a"                       (infixr "<*>" 70)
  zero  :: 'a                                       ("<0>");

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

(* text {* The unary and binary minus can be considered as 
abbreviations: *};
*)

(***
constdefs 
  negate :: "'a => 'a"                           ("- _" [100] 100)
  "- x == (- 1r) <*> x"
  diff :: "'a => 'a => 'a"                       (infixl "-" 68)
  "x - y == x + - y";
***)

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 $\zero$ 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}) set => bool"
  "is_vectorspace V == V ~= {} 
   & (ALL x:V. ALL y:V. ALL z:V. ALL a b.
        x + y : V                                 
      & a <*> x : V                                 
      & (x + y) + z = x + (y + z)             
      & x + y = y + x                           
      & x - x = <0>                               
      & <0> + x = x                               
      & a <*> (x + y) = a <*> x + a <*> y       
      & (a + b) <*> x = a <*> x + b <*> x         
      & (a * b) <*> x = a <*> b <*> x               
      & 1r <*> x = x
      & - x = (- 1r) <*> x
      & x - y = x + - y)";                             

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

lemma vsI [intro]:
  "[| <0>:V; 
  ALL x:V. ALL y:V. x + y : V; 
  ALL x:V. ALL a. a <*> x : V;  
  ALL x:V. ALL y:V. ALL z:V. (x + y) + z = x + (y + z);
  ALL x:V. ALL y:V. x + y = y + x;
  ALL x:V. x - x = <0>;
  ALL x:V. <0> + x = x;
  ALL x:V. ALL y:V. ALL a. a <*> (x + y) = a <*> x + a <*> y;
  ALL x:V. ALL a b. (a + b) <*> x = a <*> x + b <*> x;
  ALL x:V. ALL a b. (a * b) <*> x = a <*> b <*> x; 
  ALL x:V. 1r <*> x = x; 
  ALL x:V. - x = (- 1r) <*> x; 
  ALL x:V. ALL y:V. x - y = x + - y |] ==> is_vectorspace V";
proof (unfold is_vectorspace_def, intro conjI ballI allI);
  fix x y z; 
  assume "x:V" "y:V" "z:V"
    "ALL x:V. ALL y:V. ALL z:V. x + y + z = x + (y + z)";
  thus "x + y + z =  x + (y + z)"; by (elim bspec[elimify]);
qed force+;

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

lemma negate_eq1: 
  "[| is_vectorspace V; x:V |] ==> - x = (- 1r) <*> x";
  by (unfold is_vectorspace_def) simp;

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

lemma negate_eq2: 
  "[| is_vectorspace V; x:V |] ==> (- 1r) <*> x = - x";
  by (unfold is_vectorspace_def) simp;

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

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

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

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

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

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

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

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

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

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

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

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

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

lemma vs_mult_1 [simp]: 
  "[| is_vectorspace V; x:V |] ==> 1r <*> x = x"; 
  by (unfold is_vectorspace_def) simp;

lemma vs_diff_mult_distrib1: 
  "[| is_vectorspace V; x:V; y:V |] 
  ==> a <*> (x - y) = a <*> x - a <*> y";
  by (simp add: diff_eq1 negate_eq1 vs_add_mult_distrib1);

lemma vs_diff_mult_distrib2: 
  "[| is_vectorspace V; x:V |] 
  ==> (a - b) <*> x = a <*> x - (b <*> x)";
proof -;
  assume "is_vectorspace V" "x:V";
  have " (a - b) <*> x = (a + - b ) <*> x"; 
    by (unfold real_diff_def, simp);
  also; have "... = a <*> x + (- b) <*> x"; 
    by (rule vs_add_mult_distrib2);
  also; have "... = a <*> x + - (b <*> x)"; 
    by (simp! add: negate_eq1);
  also; have "... = a <*> x - (b <*> 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:V |] ==> 0r <*> x = <0>";
proof -;
  assume "is_vectorspace V" "x:V";
  have  "0r <*> x = (1r - 1r) <*> x"; by (simp only: real_diff_self);
  also; have "... = (1r + - 1r) <*> x"; by simp;
  also; have "... =  1r <*> x + (- 1r) <*> x"; 
    by (rule vs_add_mult_distrib2);
  also; have "... = x + (- 1r) <*> x"; by (simp!);
  also; have "... = x + - x"; by (simp! add: negate_eq2);;
  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} set) |] 
  ==> a <*> <0> = (<0>::'a)";
proof -;
  assume "is_vectorspace V";
  have "a <*> <0> = a <*> (<0> - (<0>::'a))"; by (simp!);
  also; have "... =  a <*> <0> - a <*> <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:V |] ==> (- a) <*> - x = a <*> x";
  by (simp add: negate_eq1);

lemma vs_add_minus_left_eq_diff: 
  "[| is_vectorspace V; x:V; y:V |] ==> - x + y = y - x";
proof -; 
  assume "is_vectorspace V" "x:V" "y:V";
  have "- x + y = y + - x"; 
    by (simp! add: vs_add_commute [RS sym, of V "- x"]);
  also; have "... = y - x"; by (simp! add: diff_eq1);
  finally; show ?thesis; .;
qed;

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

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

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

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

lemma vs_minus_zero_iff [simp]:
  "[| is_vectorspace V; x:V |] ==> (- x = <0>) = (x = <0>)" 
  (concl is "?L = ?R");
proof -;
  assume "is_vectorspace V" "x:V";
  show "?L = ?R";
  proof;
    have "x = - (- x)"; by (rule vs_minus_minus [RS sym]);
    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:V; y: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:V; y: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:V; y:V |] 
  ==> - (x + y) = - x + - y";
  by (simp add: negate_eq1 vs_add_mult_distrib1);

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

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

lemma vs_add_left_cancel:
  "[| is_vectorspace V; x:V; y:V; z:V |] 
   ==> (x + y = x + z) = (y = z)"  
  (concl is "?L = ?R");
proof;
  assume "is_vectorspace V" "x:V" "y:V" "z: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 ?L; 
  also; have "- x + ... = - x + x + z"; 
    by (rule vs_add_assoc [RS sym]) (simp!)+;
  also; have "... = z"; by (simp!);
  finally; show ?R; .;
qed force;

lemma vs_add_right_cancel: 
  "[| is_vectorspace V; x:V; y:V; z: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:V; y:V; x':V; y':V; z: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:V; y:V; z:V |] 
  ==> x <*> y <*> z = y <*> x <*> z";  
  by (simp add: real_mult_commute);

lemma vs_mult_zero_uniq :
  "[| is_vectorspace V; x:V; a <*> x = <0>; x ~= <0> |] ==> a = 0r";
proof (rule classical);
  assume "is_vectorspace V" "x:V" "a <*> x = <0>" "x ~= <0>";
  assume "a ~= 0r";
  have "x = (rinv a * a) <*> x"; by (simp!);
  also; have "... = rinv a <*> (a <*> x)"; by (rule vs_mult_assoc);
  also; have "... = rinv a <*> <0>"; by (simp!);
  also; have "... = <0>"; by (simp!);
  finally; have "x = <0>"; .;
  thus "a = 0r"; by contradiction; 
qed;

lemma vs_mult_left_cancel: 
  "[| is_vectorspace V; x:V; y:V; a ~= 0r |] ==> 
  (a <*> x = a <*> y) = (x = y)"
  (concl is "?L = ?R");
proof;
  assume "is_vectorspace V" "x:V" "y:V" "a ~= 0r";
  have "x = 1r <*> x"; by (simp!);
  also; have "... = (rinv a * a) <*> x"; by (simp!);
  also; have "... = rinv a <*> (a <*> x)"; 
    by (simp! only: vs_mult_assoc);
  also; assume ?L;
  also; have "rinv a <*> ... = y"; by (simp!);
  finally; show ?R; .;
qed simp;

lemma vs_mult_right_cancel: (*** forward ***)
  "[| is_vectorspace V; x:V; x ~= <0> |] 
  ==> (a <*> x = b <*> x) = (a = b)" (concl is "?L = ?R");
proof;
  assume "is_vectorspace V" "x:V" "x ~= <0>";
  have "(a - b) <*> x = a <*> x - b <*> x"; 
    by (simp! add: vs_diff_mult_distrib2);
  also; assume ?L; hence "a <*> x - b <*> x = <0>"; by (simp!);
  finally; have "(a - b) <*> x = <0>"; .; 
  hence "a - b = 0r"; by (simp! add: vs_mult_zero_uniq);
  thus "a = b"; by (rule real_add_minus_eq);
qed simp; (*** 

backward :
lemma vs_mult_right_cancel: 
  "[| is_vectorspace V; x:V; x ~= <0> |] ==>  
  (a <*> x = b <*> x) = (a = b)"
  (concl is "?L = ?R");
proof;
  assume "is_vectorspace V" "x:V" "x ~= <0>";
  assume l: ?L; 
  show "a = b"; 
  proof (rule real_add_minus_eq);
    show "a - b = 0r"; 
    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:V; y:V; z:V |] ==> 
  (x = z - y) = (x + y = z)"
  (concl is "?L = ?R" );  
proof -;
  assume vs: "is_vectorspace V" "x:V" "y:V" "z: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:V; y:V; x + y = <0> |] ==> x = - y"; 
proof -;
  assume "is_vectorspace V" "x:V" "y: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:V; y:V; x - y = <0> |] ==> x = y"; 
proof -;
  assume "is_vectorspace V" "x:V" "y: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:V; b:V; c:V; d:V; a + b = c + d |] 
  ==> a - c = d - b";
proof -; 
  assume vs: "is_vectorspace V" "a:V" "b:V" "c:V" "d: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:V; y:V; z:V; u:V |] 
  ==> (x + (y + z) = y + u) = ((x + z) = u)"
  (concl is "?L = ?R"); 
proof -; 
  assume "is_vectorspace V" "x:V" "y:V""z:V" "u: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:V; y:V; z:V |] 
  ==> (x + (y + z) = y) = (x = - z)"
  (concl is "?L = ?R" );
proof -;
  assume "is_vectorspace V" "x:V" "y:V" "z: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;