author  wenzelm 
Thu, 29 Aug 2002 16:08:30 +0200  
changeset 13547  bf399f3bd7dc 
parent 13515  a6a7025fd7e8 
child 14254  342634f38451 
permissions  rwrr 
7566  1 
(* Title: HOL/Real/HahnBanach/Linearform.thy 
2 
ID: $Id$ 

3 
Author: Gertrud Bauer, TU Munich 

4 
*) 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

5 

9035  6 
header {* Linearforms *} 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

7 

9035  8 
theory Linearform = VectorSpace: 
7917  9 

10687  10 
text {* 
11 
A \emph{linear form} is a function on a vector space into the reals 

12 
that is additive and multiplicative. 

13 
*} 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

14 

13515  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" 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

18 

13547  19 
lemma (in linearform) neg [iff]: 
20 
includes vectorspace 

21 
shows "x \<in> V \<Longrightarrow> f ( x) =  f x" 

10687  22 
proof  
13515  23 
assume x: "x \<in> V" 
24 
hence "f ( x) = f (( 1) \<cdot> x)" by (simp add: negate_eq1) 

25 
also from x have "... = ( 1) * (f x)" by (rule mult) 

26 
also from x have "... =  (f x)" by simp 

9035  27 
finally show ?thesis . 
28 
qed 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

29 

13547  30 
lemma (in linearform) diff [iff]: 
31 
includes vectorspace 

32 
shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x  y) = f x  f y" 

9035  33 
proof  
13515  34 
assume x: "x \<in> V" and y: "y \<in> V" 
35 
hence "x  y = x +  y" by (rule diff_eq1) 

13547  36 
also have "f ... = f x + f ( y)" by (rule add) (simp_all add: x y) 
37 
also from _ y have "f ( y) =  f y" by (rule neg) 

13515  38 
finally show ?thesis by simp 
9035  39 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

40 

10687  41 
text {* Every linear form yields @{text 0} for the @{text 0} vector. *} 
7917  42 

13547  43 
lemma (in linearform) zero [iff]: 
44 
includes vectorspace 

45 
shows "f 0 = 0" 

10687  46 
proof  
13515  47 
have "f 0 = f (0  0)" by simp 
48 
also have "\<dots> = f 0  f 0" by (rule diff) simp_all 

49 
also have "\<dots> = 0" by simp 

50 
finally show ?thesis . 

10687  51 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

52 

10687  53 
end 