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 *)
     5 
     6 header {* Linearforms *};
     7 
     8 theory Linearform = LinearSpace:;
     9 
    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))"; 
    15 
    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;
    21 
    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;
    25 
    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;
    29 
    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;
    39 
    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;
    51 
    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; 
    62 
    63 end;