src/HOL/Hahn_Banach/Linearform.thy
 author haftmann Fri Nov 01 18:51:14 2013 +0100 (2013-11-01) changeset 54230 b1d955791529 parent 31795 be3e1cc5005c child 58744 c434e37f290e permissions -rw-r--r--
more simplification rules on unary and binary minus
     1 (*  Title:      HOL/Hahn_Banach/Linearform.thy

     2     Author:     Gertrud Bauer, TU Munich

     3 *)

     4

     5 header {* Linearforms *}

     6

     7 theory Linearform

     8 imports Vector_Space

     9 begin

    10

    11 text {*

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

    13   that is additive and multiplicative.

    14 *}

    15

    16 locale linearform =

    17   fixes V :: "'a\<Colon>{minus, plus, zero, uminus} set" and f

    18   assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"

    19     and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x"

    20

    21 declare linearform.intro [intro?]

    22

    23 lemma (in linearform) neg [iff]:

    24   assumes "vectorspace V"

    25   shows "x \<in> V \<Longrightarrow> f (- x) = - f x"

    26 proof -

    27   interpret vectorspace V by fact

    28   assume x: "x \<in> V"

    29   then have "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)

    30   also from x have "\<dots> = (- 1) * (f x)" by (rule mult)

    31   also from x have "\<dots> = - (f x)" by simp

    32   finally show ?thesis .

    33 qed

    34

    35 lemma (in linearform) diff [iff]:

    36   assumes "vectorspace V"

    37   shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y"

    38 proof -

    39   interpret vectorspace V by fact

    40   assume x: "x \<in> V" and y: "y \<in> V"

    41   then have "x - y = x + - y" by (rule diff_eq1)

    42   also have "f \<dots> = f x + f (- y)" by (rule add) (simp_all add: x y)

    43   also have "f (- y) = - f y" using vectorspace V y by (rule neg)

    44   finally show ?thesis by simp

    45 qed

    46

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

    48

    49 lemma (in linearform) zero [iff]:

    50   assumes "vectorspace V"

    51   shows "f 0 = 0"

    52 proof -

    53   interpret vectorspace V by fact

    54   have "f 0 = f (0 - 0)" by simp

    55   also have "\<dots> = f 0 - f 0" using vectorspace V by (rule diff) simp_all

    56   also have "\<dots> = 0" by simp

    57   finally show ?thesis .

    58 qed

    59

    60 end