1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Hahn_Banach/Linearform.thy	Wed Jun 24 21:46:54 2009 +0200
     1.3 @@ -0,0 +1,60 @@
     1.4 +(*  Title:      HOL/Hahn_Banach/Linearform.thy
     1.5 +    Author:     Gertrud Bauer, TU Munich
     1.6 +*)
     1.7 +
     1.8 +header {* Linearforms *}
     1.9 +
    1.10 +theory Linearform
    1.11 +imports Vector_Space
    1.12 +begin
    1.13 +
    1.14 +text {*
    1.15 +  A \emph{linear form} is a function on a vector space into the reals
    1.16 +  that is additive and multiplicative.
    1.17 +*}
    1.18 +
    1.19 +locale linearform =
    1.20 +  fixes V :: "'a\<Colon>{minus, plus, zero, uminus} set" and f
    1.21 +  assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
    1.22 +    and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x"
    1.23 +
    1.24 +declare linearform.intro [intro?]
    1.25 +
    1.26 +lemma (in linearform) neg [iff]:
    1.27 +  assumes "vectorspace V"
    1.28 +  shows "x \<in> V \<Longrightarrow> f (- x) = - f x"
    1.29 +proof -
    1.30 +  interpret vectorspace V by fact
    1.31 +  assume x: "x \<in> V"
    1.32 +  then have "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
    1.33 +  also from x have "\<dots> = (- 1) * (f x)" by (rule mult)
    1.34 +  also from x have "\<dots> = - (f x)" by simp
    1.35 +  finally show ?thesis .
    1.36 +qed
    1.37 +
    1.38 +lemma (in linearform) diff [iff]:
    1.39 +  assumes "vectorspace V"
    1.40 +  shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y"
    1.41 +proof -
    1.42 +  interpret vectorspace V by fact
    1.43 +  assume x: "x \<in> V" and y: "y \<in> V"
    1.44 +  then have "x - y = x + - y" by (rule diff_eq1)
    1.45 +  also have "f \<dots> = f x + f (- y)" by (rule add) (simp_all add: x y)
    1.46 +  also have "f (- y) = - f y" using `vectorspace V` y by (rule neg)
    1.47 +  finally show ?thesis by simp
    1.48 +qed
    1.49 +
    1.50 +text {* Every linear form yields @{text 0} for the @{text 0} vector. *}
    1.51 +
    1.52 +lemma (in linearform) zero [iff]:
    1.53 +  assumes "vectorspace V"
    1.54 +  shows "f 0 = 0"
    1.55 +proof -
    1.56 +  interpret vectorspace V by fact
    1.57 +  have "f 0 = f (0 - 0)" by simp
    1.58 +  also have "\<dots> = f 0 - f 0" using `vectorspace V` by (rule diff) simp_all
    1.59 +  also have "\<dots> = 0" by simp
    1.60 +  finally show ?thesis .
    1.61 +qed
    1.62 +
    1.63 +end