1.1 --- a/src/HOL/Real/HahnBanach/Linearform.thy Tue Dec 30 08:18:54 2008 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,60 +0,0 @@
1.4 -(* Title: HOL/Real/HahnBanach/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 VectorSpace
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