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 ||.||
     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::{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))" 
    18 
    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
    24 
    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
    28 
    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
    32 
    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
    43 
    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
    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 = #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 
    68 
    69 end