src/HOL/Real/HahnBanach/Linearform.thy
 author wenzelm Thu Aug 22 20:49:43 2002 +0200 (2002-08-22) changeset 13515 a6a7025fd7e8 parent 12018 ec054019c910 child 13547 bf399f3bd7dc permissions -rw-r--r--
updated to use locales (still some rough edges);
1 (*  Title:      HOL/Real/HahnBanach/Linearform.thy
2     ID:         $Id$
3     Author:     Gertrud Bauer, TU Munich
4 *)
8 theory Linearform = VectorSpace:
10 text {*
11   A \emph{linear form} is a function on a vector space into the reals
12   that is additive and multiplicative.
13 *}
15 locale linearform = var V + var f +
16   assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
17     and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x"
19 locale (open) vectorspace_linearform =
20   vectorspace + linearform
22 lemma (in vectorspace_linearform) neg [iff]:
23   "x \<in> V \<Longrightarrow> f (- x) = - f x"
24 proof -
25   assume x: "x \<in> V"
26   hence "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
27   also from x have "... = (- 1) * (f x)" by (rule mult)
28   also from x have "... = - (f x)" by simp
29   finally show ?thesis .
30 qed
32 lemma (in vectorspace_linearform) diff [iff]:
33   "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y"
34 proof -
35   assume x: "x \<in> V" and y: "y \<in> V"
36   hence "x - y = x + - y" by (rule diff_eq1)
37   also have "f ... = f x + f (- y)"