src/HOL/Real/HahnBanach/Linearform.thy
 author wenzelm Mon Feb 07 18:38:51 2000 +0100 (2000-02-07) changeset 8203 2fcc6017cb72 parent 7978 1b99ee57d131 child 8703 816d8f6513be permissions -rw-r--r--
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
     1 (*  Title:      HOL/Real/HahnBanach/Linearform.thy

     2     ID:         $Id$

     3     Author:     Gertrud Bauer, TU Munich

     4 *)

     5

     6 header {* Linearforms *};

     7

     8 theory Linearform = VectorSpace:;

     9

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

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

    12

    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))";

    18

    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;

    24

    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;

    28

    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;

    32

    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;

    43

    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;

    55

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

    57

    58 lemma linearform_zero [intro??, simp]:

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

    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 "... = 0r"; by simp;

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

    67 qed;

    68

    69 end;