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

src/HOL/Real/HahnBanach/Linearform.thy

author | wenzelm |

Wed Sep 29 16:41:52 1999 +0200 (1999-09-29) | |

changeset 7656 | 2f18c0ffc348 |

parent 7566 | c5a3f980a7af |

child 7808 | fd019ac3485f |

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 theory Linearform = LinearSpace:;

8 section {* linearforms *};

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]: "[| !! x y. [| x : V; y : V |] ==> f (x [+] y) = f x + f y;

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

18 ==> is_linearform V f";

19 by (unfold is_linearform_def) force;

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;

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;

29 lemma linearform_neg_linear [intro!!]:

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

31 proof -;

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

33 have "f ([-] x) = f ((- 1r) [*] x)"; by (simp! add: vs_mult_minus_1);

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

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

36 finally; show ?thesis; .;

37 qed;

39 lemma linearform_diff_linear [intro!!]:

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

41 proof -;

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

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

44 also; have "... = f x + f ([-] y)"; by (rule linearform_add_linear) (simp!)+;

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

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

47 qed;

49 lemma linearform_zero [intro!!, simp]: "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r";

50 proof -;

51 assume "is_vectorspace V" "is_linearform V f";

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

53 also; have "... = f <0> - f <0>"; by (rule linearform_diff_linear) (simp!)+;

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

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

56 qed;

58 end;