author  nipkow 
Thu, 13 Apr 2000 15:01:50 +0200  
changeset 8703  816d8f6513be 
parent 8203  2fcc6017cb72 
child 9013  9dd0274f76af 
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 

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

7 

7917  8 
theory Linearform = VectorSpace:; 
9 

7978  10 
text{* A \emph{linear form} is a function on a vector 
11 
space into the reals that is additive and multiplicative. *}; 

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

12 

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

13 
constdefs 
7917  14 
is_linearform :: "['a::{minus, plus} set, 'a => real] => bool" 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

15 
"is_linearform V f == 
7917  16 
(ALL x: V. ALL y: V. f (x + y) = f x + f y) & 
8703  17 
(ALL x: V. ALL a. f (a (*) x) = a * (f x))"; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

18 

7808  19 
lemma is_linearformI [intro]: 
7917  20 
"[ !! x y. [ x : V; y : V ] ==> f (x + y) = f x + f y; 
8703  21 
!! x c. x : V ==> f (c (*) x) = c * f x ] 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

24 

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset

25 
lemma linearform_add [intro??]: 
7917  26 
"[ is_linearform V f; x:V; y:V ] ==> f (x + y) = f x + f y"; 
27 
by (unfold is_linearform_def) fast; 

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

28 

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset

29 
lemma linearform_mult [intro??]: 
8703  30 
"[ is_linearform V f; x:V ] ==> f (a (*) x) = a * (f x)"; 
7917  31 
by (unfold is_linearform_def) fast; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

32 

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset

33 
lemma linearform_neg [intro??]: 
7917  34 
"[ is_vectorspace V; is_linearform V f; x:V] 
35 
==> f ( x) =  f x"; 

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

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

37 
assume "is_linearform V f" "is_vectorspace V" "x:V"; 
8703  38 
have "f ( x) = f (( 1r) (*) x)"; by (simp! add: negate_eq1); 
7978  39 
also; have "... = ( 1r) * (f x)"; by (rule linearform_mult); 
7566  40 
also; have "... =  (f x)"; by (simp!); 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

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

43 

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset

44 
lemma linearform_diff [intro??]: 
7808  45 
"[ is_vectorspace V; is_linearform V f; x:V; y:V ] 
7917  46 
==> f (x  y) = f x  f y"; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

48 
assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V"; 
7917  49 
have "f (x  y) = f (x +  y)"; by (simp! only: diff_eq1); 
50 
also; have "... = f x + f ( y)"; 

7978  51 
by (rule linearform_add) (simp!)+; 
52 
also; have "f ( y) =  f y"; by (rule linearform_neg); 

7917  53 
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

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

55 

7978  56 
text{* Every linear form yields $0$ for the $\zero$ vector.*}; 
7917  57 

8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset

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

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

61 
assume "is_vectorspace V" "is_linearform V f"; 
8703  62 
have "f 00 = f (00  00)"; by (simp!); 
63 
also; have "... = f 00  f 00"; 

7978  64 
by (rule linearform_diff) (simp!)+; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

65 
also; have "... = 0r"; by simp; 
8703  66 
finally; show "f 00 = 0r"; .; 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

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

68 

7808  69 
end; 