--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Real/HahnBanach/VectorSpace.thy Fri Oct 22 20:14:31 1999 +0200
@@ -0,0 +1,537 @@
+(* 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$ is
+considered, on which the operations addition and real scalar
+multiplication are defined, and which has an zero element.*};
+
+consts
+(***
+ sum :: "['a, 'a] => 'a" (infixl "+" 65)
+***)
+ 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 $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 a vector space
+follows from the non-emptyness of the vector space. *};
+
+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;
\ No newline at end of file