src/HOL/Hahn_Banach/Linearform.thy
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 31795 be3e1cc5005c
child 58744 c434e37f290e
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
     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