src/HOL/Hahn_Banach/Linearform.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 31795 be3e1cc5005c
child 58744 c434e37f290e
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
wenzelm@31795
     1
(*  Title:      HOL/Hahn_Banach/Linearform.thy
wenzelm@7566
     2
    Author:     Gertrud Bauer, TU Munich
wenzelm@7566
     3
*)
wenzelm@7535
     4
wenzelm@9035
     5
header {* Linearforms *}
wenzelm@7535
     6
wenzelm@27612
     7
theory Linearform
wenzelm@31795
     8
imports Vector_Space
wenzelm@27612
     9
begin
wenzelm@7917
    10
wenzelm@10687
    11
text {*
wenzelm@10687
    12
  A \emph{linear form} is a function on a vector space into the reals
wenzelm@10687
    13
  that is additive and multiplicative.
wenzelm@10687
    14
*}
wenzelm@7535
    15
ballarin@29234
    16
locale linearform =
ballarin@29234
    17
  fixes V :: "'a\<Colon>{minus, plus, zero, uminus} set" and f
wenzelm@13515
    18
  assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
wenzelm@13515
    19
    and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x"
wenzelm@7535
    20
ballarin@14254
    21
declare linearform.intro [intro?]
ballarin@14254
    22
wenzelm@13547
    23
lemma (in linearform) neg [iff]:
ballarin@27611
    24
  assumes "vectorspace V"
wenzelm@13547
    25
  shows "x \<in> V \<Longrightarrow> f (- x) = - f x"
wenzelm@10687
    26
proof -
ballarin@29234
    27
  interpret vectorspace V by fact
wenzelm@13515
    28
  assume x: "x \<in> V"
wenzelm@27612
    29
  then have "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
wenzelm@27612
    30
  also from x have "\<dots> = (- 1) * (f x)" by (rule mult)
wenzelm@27612
    31
  also from x have "\<dots> = - (f x)" by simp
wenzelm@9035
    32
  finally show ?thesis .
wenzelm@9035
    33
qed
wenzelm@7535
    34
wenzelm@13547
    35
lemma (in linearform) diff [iff]:
ballarin@27611
    36
  assumes "vectorspace V"
wenzelm@13547
    37
  shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y"
wenzelm@9035
    38
proof -
ballarin@29234
    39
  interpret vectorspace V by fact
wenzelm@13515
    40
  assume x: "x \<in> V" and y: "y \<in> V"
wenzelm@27612
    41
  then have "x - y = x + - y" by (rule diff_eq1)
wenzelm@27612
    42
  also have "f \<dots> = f x + f (- y)" by (rule add) (simp_all add: x y)
wenzelm@23378
    43
  also have "f (- y) = - f y" using `vectorspace V` y by (rule neg)
wenzelm@13515
    44
  finally show ?thesis by simp
wenzelm@9035
    45
qed
wenzelm@7535
    46
wenzelm@10687
    47
text {* Every linear form yields @{text 0} for the @{text 0} vector. *}
wenzelm@7917
    48
wenzelm@13547
    49
lemma (in linearform) zero [iff]:
ballarin@27611
    50
  assumes "vectorspace V"
wenzelm@13547
    51
  shows "f 0 = 0"
wenzelm@10687
    52
proof -
ballarin@29234
    53
  interpret vectorspace V by fact
wenzelm@13515
    54
  have "f 0 = f (0 - 0)" by simp
wenzelm@23378
    55
  also have "\<dots> = f 0 - f 0" using `vectorspace V` by (rule diff) simp_all
wenzelm@13515
    56
  also have "\<dots> = 0" by simp
wenzelm@13515
    57
  finally show ?thesis .
wenzelm@10687
    58
qed
wenzelm@7535
    59
wenzelm@10687
    60
end