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

src/HOL/Real/HahnBanach/Linearform.thy

author | wenzelm |

Fri Oct 08 16:40:27 1999 +0200 (1999-10-08) | |

changeset 7808 | fd019ac3485f |

parent 7656 | 2f18c0ffc348 |

child 7917 | 5e5b9813cce7 |

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

update from Gertrud;

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

2 ID: $Id$

3 Author: Gertrud Bauer, TU Munich

4 *)

6 header {* Linearforms *};

8 theory Linearform = LinearSpace:;

10 constdefs

11 is_linearform :: "['a set, 'a => real] => bool"

12 "is_linearform V f ==

13 (ALL x: V. ALL y: V. f (x [+] y) = f x + f y) &

14 (ALL x: V. ALL a. f (a [*] x) = a * (f x))";

16 lemma is_linearformI [intro]:

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

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

19 ==> is_linearform V f";

20 by (unfold is_linearform_def) force;

22 lemma linearform_add_linear [intro!!]:

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

24 by (unfold is_linearform_def) auto;

26 lemma linearform_mult_linear [intro!!]:

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

28 by (unfold is_linearform_def) auto;

30 lemma linearform_neg_linear [intro!!]:

31 "[| is_vectorspace V; is_linearform V f; x:V|] ==> f ([-] x) = - f x";

32 proof -;

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

34 have "f ([-] x) = f ((- 1r) [*] x)"; by (unfold negate_def) simp;

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

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

37 finally; show ?thesis; .;

38 qed;

40 lemma linearform_diff_linear [intro!!]:

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

42 ==> f (x [-] y) = f x - f y";

43 proof -;

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

45 have "f (x [-] y) = f (x [+] [-] y)"; by (simp only: diff_def);

46 also; have "... = f x + f ([-] y)";

47 by (rule linearform_add_linear) (simp!)+;

48 also; have "f ([-] y) = - f y"; by (rule linearform_neg_linear);

49 finally; show "f (x [-] y) = f x - f y"; by (simp!);

50 qed;

52 lemma linearform_zero [intro!!, simp]:

53 "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r";

54 proof -;

55 assume "is_vectorspace V" "is_linearform V f";

56 have "f <0> = f (<0> [-] <0>)"; by (simp!);

57 also; have "... = f <0> - f <0>";

58 by (rule linearform_diff_linear) (simp!)+;

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

60 finally; show "f <0> = 0r"; .;

61 qed;

63 end;