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