src/HOL/Real/HahnBanach/Linearform.thy
author fleuriot
Thu Jun 01 11:22:27 2000 +0200 (2000-06-01)
changeset 9013 9dd0274f76af
parent 8703 816d8f6513be
child 9035 371f023d3dbd
permissions -rw-r--r--
Updated files to remove 0r and 1r from theorems in descendant theories
of RealBin. Some new theorems added.
     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 ((- (#1::real)) (*) 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;
    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 00 = (#0::real)"; 
    60 proof -; 
    61   assume "is_vectorspace V" "is_linearform V f";
    62   have "f 00 = f (00 - 00)"; by (simp!);
    63   also; have "... = f 00 - f 00"; 
    64     by (rule linearform_diff) (simp!)+;
    65   also; have "... = (#0::real)"; by simp;
    66   finally; show "f 00 = (#0::real)"; .;
    67 qed; 
    68 
    69 end;