author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 31795  be3e1cc5005c 
child 58744  c434e37f290e 
permissions  rwrr 
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29252
diff
changeset

1 
(* Title: HOL/Hahn_Banach/Linearform.thy 
7566  2 
Author: Gertrud Bauer, TU Munich 
3 
*) 

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

4 

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

6 

27612  7 
theory Linearform 
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29252
diff
changeset

8 
imports Vector_Space 
27612  9 
begin 
7917  10 

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

13 
that is additive and multiplicative. 

14 
*} 

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

15 

29234  16 
locale linearform = 
17 
fixes V :: "'a\<Colon>{minus, plus, zero, uminus} set" and f 

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

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

20 

14254
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13547
diff
changeset

21 
declare linearform.intro [intro?] 
342634f38451
Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents:
13547
diff
changeset

22 

13547  23 
lemma (in linearform) neg [iff]: 
27611  24 
assumes "vectorspace V" 
13547  25 
shows "x \<in> V \<Longrightarrow> f ( x) =  f x" 
10687  26 
proof  
29234  27 
interpret vectorspace V by fact 
13515  28 
assume x: "x \<in> V" 
27612  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 

9035  32 
finally show ?thesis . 
33 
qed 

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

34 

13547  35 
lemma (in linearform) diff [iff]: 
27611  36 
assumes "vectorspace V" 
13547  37 
shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x  y) = f x  f y" 
9035  38 
proof  
29234  39 
interpret vectorspace V by fact 
13515  40 
assume x: "x \<in> V" and y: "y \<in> V" 
27612  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) 

23378  43 
also have "f ( y) =  f y" using `vectorspace V` y by (rule neg) 
13515  44 
finally show ?thesis by simp 
9035  45 
qed 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

46 

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

13547  49 
lemma (in linearform) zero [iff]: 
27611  50 
assumes "vectorspace V" 
13547  51 
shows "f 0 = 0" 
10687  52 
proof  
29234  53 
interpret vectorspace V by fact 
13515  54 
have "f 0 = f (0  0)" by simp 
23378  55 
also have "\<dots> = f 0  f 0" using `vectorspace V` by (rule diff) simp_all 
13515  56 
also have "\<dots> = 0" by simp 
57 
finally show ?thesis . 

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

59 

10687  60 
end 