src/HOL/Real/HahnBanach/Linearform.thy
 author wenzelm Fri Oct 05 21:52:39 2001 +0200 (2001-10-05) changeset 11701 3d51fbf81c17 parent 10687 c186279eecea child 12018 ec054019c910 permissions -rw-r--r--
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
"num" syntax (still with "#"), Numeral0, Numeral1;
     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 {*

    11   A \emph{linear form} is a function on a vector space into the reals

    12   that is additive and multiplicative.

    13 *}

    14

    15 constdefs

    16   is_linearform :: "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"

    17   "is_linearform V f \<equiv>

    18       (\<forall>x \<in> V. \<forall>y \<in> V. f (x + y) = f x + f y) \<and>

    19       (\<forall>x \<in> V. \<forall>a. f (a \<cdot> x) = a * (f x))"

    20

    21 lemma is_linearformI [intro]:

    22   "(\<And>x y. x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y) \<Longrightarrow>

    23     (\<And>x c. x \<in> V \<Longrightarrow> f (c \<cdot> x) = c * f x)

    24  \<Longrightarrow> is_linearform V f"

    25  by (unfold is_linearform_def) blast

    26

    27 lemma linearform_add [intro?]:

    28   "is_linearform V f \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"

    29   by (unfold is_linearform_def) blast

    30

    31 lemma linearform_mult [intro?]:

    32   "is_linearform V f \<Longrightarrow> x \<in> V \<Longrightarrow>  f (a \<cdot> x) = a * (f x)"

    33   by (unfold is_linearform_def) blast

    34

    35 lemma linearform_neg [intro?]:

    36   "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> x \<in> V

    37   \<Longrightarrow> f (- x) = - f x"

    38 proof -

    39   assume "is_linearform V f"  "is_vectorspace V"  "x \<in> V"

    40   have "f (- x) = f ((- Numeral1) \<cdot> x)" by (simp! add: negate_eq1)

    41   also have "... = (- Numeral1) * (f x)" by (rule linearform_mult)

    42   also have "... = - (f x)" by (simp!)

    43   finally show ?thesis .

    44 qed

    45

    46 lemma linearform_diff [intro?]:

    47   "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V

    48   \<Longrightarrow> f (x - y) = f x - f y"

    49 proof -

    50   assume "is_vectorspace V"  "is_linearform V f"  "x \<in> V"  "y \<in> V"

    51   have "f (x - y) = f (x + - y)" by (simp! only: diff_eq1)

    52   also have "... = f x + f (- y)"

    53     by (rule linearform_add) (simp!)+

    54   also have "f (- y) = - f y" by (rule linearform_neg)

    55   finally show "f (x - y) = f x - f y" by (simp!)

    56 qed

    57

    58 text {* Every linear form yields @{text 0} for the @{text 0} vector. *}

    59

    60 lemma linearform_zero [intro?, simp]:

    61   "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> f 0 = Numeral0"

    62 proof -

    63   assume "is_vectorspace V"  "is_linearform V f"

    64   have "f 0 = f (0 - 0)" by (simp!)

    65   also have "... = f 0 - f 0"

    66     by (rule linearform_diff) (simp!)+

    67   also have "... = Numeral0" by simp

    68   finally show "f 0 = Numeral0" .

    69 qed

    70

    71 end