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

src/HOL/Real/HahnBanach/Linearform.thy

author | bauerg |

Mon Jul 17 13:58:18 2000 +0200 (2000-07-17) | |

changeset 9374 | 153853af318b |

parent 9035 | 371f023d3dbd |

child 9408 | d3d56e1d2ec1 |

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

- xsymbols for

\<noteq> \<notin> \<in> \<exists> \<forall>

\<and> \<inter> \<union> \<Union>

- vector space type of {plus, minus, zero}, overload 0 in vector space

- syntax |.| and ||.||

\<noteq> \<notin> \<in> \<exists> \<forall>

\<and> \<inter> \<union> \<Union>

- vector space type of {plus, minus, zero}, overload 0 in vector space

- syntax |.| and ||.||

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::{plus, minus, zero} set, 'a => real] => bool"

15 "is_linearform V f ==

16 (\<forall>x \<in> V. \<forall>y \<in> V. f (x + y) = f x + f y) \<and>

17 (\<forall>x \<in> V. \<forall>a. f (a \<cdot> x) = a * (f x))"

19 lemma is_linearformI [intro]:

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

21 !! x c. x \<in> V ==> f (c \<cdot> 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 \<in> V; y \<in> 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 \<in> V |] ==> f (a \<cdot> 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 \<in> V|]

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

36 proof -

37 assume "is_linearform V f" "is_vectorspace V" "x \<in> V"

38 have "f (- x) = f ((- #1) \<cdot> x)" by (simp! add: negate_eq1)

39 also have "... = (- #1) * (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 \<in> V; y \<in> V |]

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

47 proof -

48 assume "is_vectorspace V" "is_linearform V f" "x \<in> V" "y \<in> 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 0 = #0"

60 proof -

61 assume "is_vectorspace V" "is_linearform V f"

62 have "f 0 = f (0 - 0)" by (simp!)

63 also have "... = f 0 - f 0"

64 by (rule linearform_diff) (simp!)+

65 also have "... = #0" by simp

66 finally show "f 0 = #0" .

67 qed

69 end