src/HOL/Real/HahnBanach/Linearform.thy
 author haftmann Wed Jan 02 15:14:02 2008 +0100 (2008-01-02) changeset 25762 c03e9d04b3e4 parent 23378 1d138d6bb461 child 27611 2c01c0bdb385 permissions -rw-r--r--
splitted class uminus from class minus
 wenzelm@7566  1 (* Title: HOL/Real/HahnBanach/Linearform.thy  wenzelm@7566  2  ID: $Id$  wenzelm@7566  3  Author: Gertrud Bauer, TU Munich  wenzelm@7566  4 *)  wenzelm@7535  5 wenzelm@9035  6 header {* Linearforms *}  wenzelm@7535  7 haftmann@16417  8 theory Linearform imports VectorSpace begin  wenzelm@7917  9 wenzelm@10687  10 text {*  wenzelm@10687  11  A \emph{linear form} is a function on a vector space into the reals  wenzelm@10687  12  that is additive and multiplicative.  wenzelm@10687  13 *}  wenzelm@7535  14 wenzelm@13515  15 locale linearform = var V + var f +  haftmann@25762  16  constrains V :: "'a\{minus, plus, zero, uminus} set"  wenzelm@13515  17  assumes add [iff]: "x \ V \ y \ V \ f (x + y) = f x + f y"  wenzelm@13515  18  and mult [iff]: "x \ V \ f (a \ x) = a * f x"  wenzelm@7535  19 ballarin@14254  20 declare linearform.intro [intro?]  ballarin@14254  21 wenzelm@13547  22 lemma (in linearform) neg [iff]:  wenzelm@13547  23  includes vectorspace  wenzelm@13547  24  shows "x \ V \ f (- x) = - f x"  wenzelm@10687  25 proof -  wenzelm@13515  26  assume x: "x \ V"  wenzelm@13515  27  hence "f (- x) = f ((- 1) \ x)" by (simp add: negate_eq1)  wenzelm@13515  28  also from x have "... = (- 1) * (f x)" by (rule mult)  wenzelm@13515  29  also from x have "... = - (f x)" by simp  wenzelm@9035  30  finally show ?thesis .  wenzelm@9035  31 qed  wenzelm@7535  32 wenzelm@13547  33 lemma (in linearform) diff [iff]:  wenzelm@13547  34  includes vectorspace  wenzelm@13547  35  shows "x \ V \ y \ V \ f (x - y) = f x - f y"  wenzelm@9035  36 proof -  wenzelm@13515  37  assume x: "x \ V" and y: "y \ V"  wenzelm@13515  38  hence "x - y = x + - y" by (rule diff_eq1)  wenzelm@13547  39  also have "f ... = f x + f (- y)" by (rule add) (simp_all add: x y)  wenzelm@23378  40  also have "f (- y) = - f y" using vectorspace V y by (rule neg)  wenzelm@13515  41  finally show ?thesis by simp  wenzelm@9035  42 qed  wenzelm@7535  43 wenzelm@10687  44 text {* Every linear form yields @{text 0} for the @{text 0} vector. *}  wenzelm@7917  45 wenzelm@13547  46 lemma (in linearform) zero [iff]:  wenzelm@13547  47  includes vectorspace  wenzelm@13547  48  shows "f 0 = 0"  wenzelm@10687  49 proof -  wenzelm@13515  50  have "f 0 = f (0 - 0)" by simp  wenzelm@23378  51  also have "\ = f 0 - f 0" using vectorspace V by (rule diff) simp_all  wenzelm@13515  52  also have "\ = 0" by simp  wenzelm@13515  53  finally show ?thesis .  wenzelm@10687  54 qed  wenzelm@7535  55 wenzelm@10687  56 end