author  wenzelm 
Wed, 29 Sep 1999 16:41:52 +0200  
changeset 7656  2f18c0ffc348 
parent 7566  c5a3f980a7af 
child 7808  fd019ac3485f 
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 

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

6 
theory Linearform = LinearSpace:; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

7 

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

8 
section {* linearforms *}; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

9 

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

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

11 
is_linearform :: "['a set, 'a => real] => bool" 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

12 
"is_linearform V f == 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

13 
(ALL x: V. ALL y: V. f (x [+] y) = f x + f y) & 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

14 
(ALL x: V. ALL a. f (a [*] x) = a * (f x))"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

15 

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

16 
lemma is_linearformI [intro]: "[ !! x y. [ x : V; y : V ] ==> f (x [+] y) = f x + f y; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

17 
!! x c. x : V ==> f (c [*] x) = c * f x ] 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

18 
==> is_linearform V f"; 
7566  19 
by (unfold is_linearform_def) force; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

20 

7566  21 
lemma linearform_add_linear [intro!!]: 
22 
"[ is_linearform V f; x:V; y:V ] ==> f (x [+] y) = f x + f y"; 

23 
by (unfold is_linearform_def) auto; 

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

24 

7566  25 
lemma linearform_mult_linear [intro!!]: 
26 
"[ is_linearform V f; x:V ] ==> f (a [*] x) = a * (f x)"; 

27 
by (unfold is_linearform_def) auto; 

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

28 

7566  29 
lemma linearform_neg_linear [intro!!]: 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

30 
"[ is_vectorspace V; is_linearform V f; x:V] ==> f ([] x) =  f x"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

32 
assume "is_linearform V f" "is_vectorspace V" "x:V"; 
7566  33 
have "f ([] x) = f (( 1r) [*] x)"; by (simp! add: vs_mult_minus_1); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

34 
also; have "... = ( 1r) * (f x)"; by (rule linearform_mult_linear); 
7566  35 
also; have "... =  (f x)"; by (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

36 
finally; show ?thesis; .; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

38 

7566  39 
lemma linearform_diff_linear [intro!!]: 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

40 
"[ is_vectorspace V; is_linearform V f; x:V; y:V ] ==> f (x [] y) = f x  f y"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

42 
assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V"; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

43 
have "f (x [] y) = f (x [+] [] y)"; by (simp only: diff_def); 
7566  44 
also; have "... = f x + f ([] y)"; by (rule linearform_add_linear) (simp!)+; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

45 
also; have "f ([] y) =  f y"; by (rule linearform_neg_linear); 
7566  46 
finally; show "f (x [] y) = f x  f y"; by (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

48 

7656  49 
lemma linearform_zero [intro!!, simp]: "[ is_vectorspace V; is_linearform V f ] ==> f <0> = 0r"; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

51 
assume "is_vectorspace V" "is_linearform V f"; 
7566  52 
have "f <0> = f (<0> [] <0>)"; by (simp!); 
53 
also; have "... = f <0>  f <0>"; by (rule linearform_diff_linear) (simp!)+; 

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

54 
also; have "... = 0r"; by simp; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

55 
finally; show "f <0> = 0r"; .; 
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

57 

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

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

59 