src/HOL/Hahn_Banach/Linearform.thy
 author hoelzl Thu Sep 02 10:14:32 2010 +0200 (2010-09-02) changeset 39072 1030b1a166ef parent 31795 be3e1cc5005c child 58744 c434e37f290e permissions -rw-r--r--
 wenzelm@31795  1 (* Title: HOL/Hahn_Banach/Linearform.thy  wenzelm@7566  2  Author: Gertrud Bauer, TU Munich  wenzelm@7566  3 *)  wenzelm@7535  4 wenzelm@9035  5 header {* Linearforms *}  wenzelm@7535  6 wenzelm@27612  7 theory Linearform  wenzelm@31795  8 imports Vector_Space  wenzelm@27612  9 begin  wenzelm@7917  10 wenzelm@10687  11 text {*  wenzelm@10687  12  A \emph{linear form} is a function on a vector space into the reals  wenzelm@10687  13  that is additive and multiplicative.  wenzelm@10687  14 *}  wenzelm@7535  15 ballarin@29234  16 locale linearform =  ballarin@29234  17  fixes V :: "'a\{minus, plus, zero, uminus} set" and f  wenzelm@13515  18  assumes add [iff]: "x \ V \ y \ V \ f (x + y) = f x + f y"  wenzelm@13515  19  and mult [iff]: "x \ V \ f (a \ x) = a * f x"  wenzelm@7535  20 ballarin@14254  21 declare linearform.intro [intro?]  ballarin@14254  22 wenzelm@13547  23 lemma (in linearform) neg [iff]:  ballarin@27611  24  assumes "vectorspace V"  wenzelm@13547  25  shows "x \ V \ f (- x) = - f x"  wenzelm@10687  26 proof -  ballarin@29234  27  interpret vectorspace V by fact  wenzelm@13515  28  assume x: "x \ V"  wenzelm@27612  29  then have "f (- x) = f ((- 1) \ x)" by (simp add: negate_eq1)  wenzelm@27612  30  also from x have "\ = (- 1) * (f x)" by (rule mult)  wenzelm@27612  31  also from x have "\ = - (f x)" by simp  wenzelm@9035  32  finally show ?thesis .  wenzelm@9035  33 qed  wenzelm@7535  34 wenzelm@13547  35 lemma (in linearform) diff [iff]:  ballarin@27611  36  assumes "vectorspace V"  wenzelm@13547  37  shows "x \ V \ y \ V \ f (x - y) = f x - f y"  wenzelm@9035  38 proof -  ballarin@29234  39  interpret vectorspace V by fact  wenzelm@13515  40  assume x: "x \ V" and y: "y \ V"  wenzelm@27612  41  then have "x - y = x + - y" by (rule diff_eq1)  wenzelm@27612  42  also have "f \ = f x + f (- y)" by (rule add) (simp_all add: x y)  wenzelm@23378  43  also have "f (- y) = - f y" using vectorspace V y by (rule neg)  wenzelm@13515  44  finally show ?thesis by simp  wenzelm@9035  45 qed  wenzelm@7535  46 wenzelm@10687  47 text {* Every linear form yields @{text 0} for the @{text 0} vector. *}  wenzelm@7917  48 wenzelm@13547  49 lemma (in linearform) zero [iff]:  ballarin@27611  50  assumes "vectorspace V"  wenzelm@13547  51  shows "f 0 = 0"  wenzelm@10687  52 proof -  ballarin@29234  53  interpret vectorspace V by fact  wenzelm@13515  54  have "f 0 = f (0 - 0)" by simp  wenzelm@23378  55  also have "\ = f 0 - f 0" using vectorspace V by (rule diff) simp_all  wenzelm@13515  56  also have "\ = 0" by simp  wenzelm@13515  57  finally show ?thesis .  wenzelm@10687  58 qed  wenzelm@7535  59 wenzelm@10687  60 end