src/HOL/Hahn_Banach/Linearform.thy
author wenzelm
Mon Nov 02 11:43:02 2015 +0100 (2015-11-02)
changeset 61540 f92bf6674699
parent 61539 a29295dac1ca
permissions -rw-r--r--
tuned document;
wenzelm@31795
     1
(*  Title:      HOL/Hahn_Banach/Linearform.thy
wenzelm@7566
     2
    Author:     Gertrud Bauer, TU Munich
wenzelm@7566
     3
*)
wenzelm@7535
     4
wenzelm@58889
     5
section \<open>Linearforms\<close>
wenzelm@7535
     6
wenzelm@27612
     7
theory Linearform
wenzelm@31795
     8
imports Vector_Space
wenzelm@27612
     9
begin
wenzelm@7917
    10
wenzelm@58744
    11
text \<open>
wenzelm@61540
    12
  A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals that is
wenzelm@61540
    13
  additive and multiplicative.
wenzelm@58744
    14
\<close>
wenzelm@7535
    15
ballarin@29234
    16
locale linearform =
wenzelm@61076
    17
  fixes V :: "'a::{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@58744
    43
  also have "f (- y) = - f y" using \<open>vectorspace V\<close> y by (rule neg)
wenzelm@13515
    44
  finally show ?thesis by simp
wenzelm@9035
    45
qed
wenzelm@7535
    46
wenzelm@61539
    47
text \<open>Every linear form yields \<open>0\<close> for the \<open>0\<close> vector.\<close>
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@58744
    55
  also have "\<dots> = f 0 - f 0" using \<open>vectorspace V\<close> 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