author  wenzelm 
Tue, 15 Jul 2008 19:39:37 +0200  
changeset 27612  d3eb431db035 
parent 27611  2c01c0bdb385 
child 29234  60f7fb56f8cd 
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 

27612  8 
theory Linearform 
9 
imports VectorSpace 

10 
begin 

7917  11 

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

14 
that is additive and multiplicative. 

15 
*} 

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

16 

13515  17 
locale linearform = var V + var f + 
25762  18 
constrains V :: "'a\<Colon>{minus, plus, zero, uminus} set" 
13515  19 
assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y" 
20 
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

21 

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

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

23 

13547  24 
lemma (in linearform) neg [iff]: 
27611  25 
assumes "vectorspace V" 
13547  26 
shows "x \<in> V \<Longrightarrow> f ( x) =  f x" 
10687  27 
proof  
27611  28 
interpret vectorspace [V] by fact 
13515  29 
assume x: "x \<in> V" 
27612  30 
then have "f ( x) = f (( 1) \<cdot> x)" by (simp add: negate_eq1) 
31 
also from x have "\<dots> = ( 1) * (f x)" by (rule mult) 

32 
also from x have "\<dots> =  (f x)" by simp 

9035  33 
finally show ?thesis . 
34 
qed 

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

35 

13547  36 
lemma (in linearform) diff [iff]: 
27611  37 
assumes "vectorspace V" 
13547  38 
shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x  y) = f x  f y" 
9035  39 
proof  
27611  40 
interpret vectorspace [V] by fact 
13515  41 
assume x: "x \<in> V" and y: "y \<in> V" 
27612  42 
then have "x  y = x +  y" by (rule diff_eq1) 
43 
also have "f \<dots> = f x + f ( y)" by (rule add) (simp_all add: x y) 

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

47 

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

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

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

60 

10687  61 
end 