1(* Title: HOL/Hahn_Banach/Linearform.thy 2 Author: Gertrud Bauer, TU Munich 3*) 4 5section \<open>Linearforms\<close> 6 7theory Linearform 8imports Vector_Space 9begin 10 11text \<open> 12 A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals that is 13 additive and multiplicative. 14\<close> 15 16locale linearform = 17 fixes V :: "'a::{minus, plus, zero, uminus} set" and f 18 assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y" 19 and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x" 20 21declare linearform.intro [intro?] 22 23lemma (in linearform) neg [iff]: 24 assumes "vectorspace V" 25 shows "x \<in> V \<Longrightarrow> f (- x) = - f x" 26proof - 27 interpret vectorspace V by fact 28 assume x: "x \<in> V" 29 then have "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1) 30 also from x have "\<dots> = (- 1) * (f x)" by (rule mult) 31 also from x have "\<dots> = - (f x)" by simp 32 finally show ?thesis . 33qed 34 35lemma (in linearform) diff [iff]: 36 assumes "vectorspace V" 37 shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y" 38proof - 39 interpret vectorspace V by fact 40 assume x: "x \<in> V" and y: "y \<in> V" 41 then have "x - y = x + - y" by (rule diff_eq1) 42 also have "f \<dots> = f x + f (- y)" by (rule add) (simp_all add: x y) 43 also have "f (- y) = - f y" using \<open>vectorspace V\<close> y by (rule neg) 44 finally show ?thesis by simp 45qed 46 47text \<open>Every linear form yields \<open>0\<close> for the \<open>0\<close> vector.\<close> 48 49lemma (in linearform) zero [iff]: 50 assumes "vectorspace V" 51 shows "f 0 = 0" 52proof - 53 interpret vectorspace V by fact 54 have "f 0 = f (0 - 0)" by simp 55 also have "\<dots> = f 0 - f 0" using \<open>vectorspace V\<close> by (rule diff) simp_all 56 also have "\<dots> = 0" by simp 57 finally show ?thesis . 58qed 59 60end 61