summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Real/HahnBanach/Linearform.thy

author | nipkow |

Thu Apr 13 15:01:50 2000 +0200 (2000-04-13) | |

changeset 8703 | 816d8f6513be |

parent 8203 | 2fcc6017cb72 |

child 9013 | 9dd0274f76af |

permissions | -rw-r--r-- |

Times -> <*>

** -> <*lex*>

** -> <*lex*>

1 (* Title: HOL/Real/HahnBanach/Linearform.thy

2 ID: $Id$

3 Author: Gertrud Bauer, TU Munich

4 *)

6 header {* Linearforms *};

8 theory Linearform = VectorSpace:;

10 text{* A \emph{linear form} is a function on a vector

11 space into the reals that is additive and multiplicative. *};

13 constdefs

14 is_linearform :: "['a::{minus, plus} set, 'a => real] => bool"

15 "is_linearform V f ==

16 (ALL x: V. ALL y: V. f (x + y) = f x + f y) &

17 (ALL x: V. ALL a. f (a (*) x) = a * (f x))";

19 lemma is_linearformI [intro]:

20 "[| !! x y. [| x : V; y : V |] ==> f (x + y) = f x + f y;

21 !! x c. x : V ==> f (c (*) x) = c * f x |]

22 ==> is_linearform V f";

23 by (unfold is_linearform_def) force;

25 lemma linearform_add [intro??]:

26 "[| is_linearform V f; x:V; y:V |] ==> f (x + y) = f x + f y";

27 by (unfold is_linearform_def) fast;

29 lemma linearform_mult [intro??]:

30 "[| is_linearform V f; x:V |] ==> f (a (*) x) = a * (f x)";

31 by (unfold is_linearform_def) fast;

33 lemma linearform_neg [intro??]:

34 "[| is_vectorspace V; is_linearform V f; x:V|]

35 ==> f (- x) = - f x";

36 proof -;

37 assume "is_linearform V f" "is_vectorspace V" "x:V";

38 have "f (- x) = f ((- 1r) (*) x)"; by (simp! add: negate_eq1);

39 also; have "... = (- 1r) * (f x)"; by (rule linearform_mult);

40 also; have "... = - (f x)"; by (simp!);

41 finally; show ?thesis; .;

42 qed;

44 lemma linearform_diff [intro??]:

45 "[| is_vectorspace V; is_linearform V f; x:V; y:V |]

46 ==> f (x - y) = f x - f y";

47 proof -;

48 assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V";

49 have "f (x - y) = f (x + - y)"; by (simp! only: diff_eq1);

50 also; have "... = f x + f (- y)";

51 by (rule linearform_add) (simp!)+;

52 also; have "f (- y) = - f y"; by (rule linearform_neg);

53 finally; show "f (x - y) = f x - f y"; by (simp!);

54 qed;

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

58 lemma linearform_zero [intro??, simp]:

59 "[| is_vectorspace V; is_linearform V f |] ==> f 00 = 0r";

60 proof -;

61 assume "is_vectorspace V" "is_linearform V f";

62 have "f 00 = f (00 - 00)"; by (simp!);

63 also; have "... = f 00 - f 00";

64 by (rule linearform_diff) (simp!)+;

65 also; have "... = 0r"; by simp;

66 finally; show "f 00 = 0r"; .;

67 qed;

69 end;