src/HOL/Real/HahnBanach/Linearform.thy
author bauerg
Mon Jul 17 13:58:18 2000 +0200 (2000-07-17)
changeset 9374 153853af318b
parent 9035 371f023d3dbd
child 9408 d3d56e1d2ec1
permissions -rw-r--r--
- xsymbols for
\<noteq> \<notin> \<in> \<exists> \<forall>
\<and> \<inter> \<union> \<Union>
- vector space type of {plus, minus, zero}, overload 0 in vector space
- syntax |.| and ||.||
wenzelm@7566
     1
(*  Title:      HOL/Real/HahnBanach/Linearform.thy
wenzelm@7566
     2
    ID:         $Id$
wenzelm@7566
     3
    Author:     Gertrud Bauer, TU Munich
wenzelm@7566
     4
*)
wenzelm@7535
     5
wenzelm@9035
     6
header {* Linearforms *}
wenzelm@7535
     7
wenzelm@9035
     8
theory Linearform = VectorSpace:
wenzelm@7917
     9
wenzelm@7978
    10
text{* A \emph{linear form} is a function on a vector
wenzelm@9035
    11
space into the reals that is additive and multiplicative. *}
wenzelm@7535
    12
wenzelm@7535
    13
constdefs
bauerg@9374
    14
  is_linearform :: "['a::{plus, minus, zero} set, 'a => real] => bool" 
wenzelm@7535
    15
  "is_linearform V f == 
bauerg@9374
    16
      (\<forall>x \<in> V. \<forall>y \<in> V. f (x + y) = f x + f y) \<and>
bauerg@9374
    17
      (\<forall>x \<in> V. \<forall>a. f (a \<cdot> x) = a * (f x))" 
wenzelm@7535
    18
wenzelm@7808
    19
lemma is_linearformI [intro]: 
bauerg@9374
    20
  "[| !! x y. [| x \<in> V; y \<in> V |] ==> f (x + y) = f x + f y;
bauerg@9374
    21
    !! x c. x \<in> V ==> f (c \<cdot> x) = c * f x |]
wenzelm@9035
    22
 ==> is_linearform V f"
wenzelm@9035
    23
 by (unfold is_linearform_def) force
wenzelm@7535
    24
wenzelm@8203
    25
lemma linearform_add [intro??]: 
bauerg@9374
    26
  "[| is_linearform V f; x \<in> V; y \<in> V |] ==> f (x + y) = f x + f y"
wenzelm@9035
    27
  by (unfold is_linearform_def) fast
wenzelm@7535
    28
wenzelm@8203
    29
lemma linearform_mult [intro??]: 
bauerg@9374
    30
  "[| is_linearform V f; x \<in> V |] ==>  f (a \<cdot> x) = a * (f x)" 
wenzelm@9035
    31
  by (unfold is_linearform_def) fast
wenzelm@7535
    32
wenzelm@8203
    33
lemma linearform_neg [intro??]:
bauerg@9374
    34
  "[|  is_vectorspace V; is_linearform V f; x \<in> V|] 
wenzelm@9035
    35
  ==> f (- x) = - f x"
wenzelm@9035
    36
proof - 
bauerg@9374
    37
  assume "is_linearform V f" "is_vectorspace V" "x \<in> V"
bauerg@9374
    38
  have "f (- x) = f ((- #1) \<cdot> x)" by (simp! add: negate_eq1)
wenzelm@9035
    39
  also have "... = (- #1) * (f x)" by (rule linearform_mult)
wenzelm@9035
    40
  also have "... = - (f x)" by (simp!)
wenzelm@9035
    41
  finally show ?thesis .
wenzelm@9035
    42
qed
wenzelm@7535
    43
wenzelm@8203
    44
lemma linearform_diff [intro??]: 
bauerg@9374
    45
  "[| is_vectorspace V; is_linearform V f; x \<in> V; y \<in> V |] 
wenzelm@9035
    46
  ==> f (x - y) = f x - f y"  
wenzelm@9035
    47
proof -
bauerg@9374
    48
  assume "is_vectorspace V" "is_linearform V f" "x \<in> V" "y \<in> V"
wenzelm@9035
    49
  have "f (x - y) = f (x + - y)" by (simp! only: diff_eq1)
wenzelm@9035
    50
  also have "... = f x + f (- y)" 
wenzelm@9035
    51
    by (rule linearform_add) (simp!)+
wenzelm@9035
    52
  also have "f (- y) = - f y" by (rule linearform_neg)
wenzelm@9035
    53
  finally show "f (x - y) = f x - f y" by (simp!)
wenzelm@9035
    54
qed
wenzelm@7535
    55
wenzelm@9035
    56
text{* Every linear form yields $0$ for the $\zero$ vector.*}
wenzelm@7917
    57
wenzelm@8203
    58
lemma linearform_zero [intro??, simp]: 
bauerg@9374
    59
  "[| is_vectorspace V; is_linearform V f |] ==> f 0 = #0"
wenzelm@9035
    60
proof - 
wenzelm@9035
    61
  assume "is_vectorspace V" "is_linearform V f"
bauerg@9374
    62
  have "f 0 = f (0 - 0)" by (simp!)
bauerg@9374
    63
  also have "... = f 0 - f 0" 
wenzelm@9035
    64
    by (rule linearform_diff) (simp!)+
wenzelm@9035
    65
  also have "... = #0" by simp
bauerg@9374
    66
  finally show "f 0 = #0" .
wenzelm@9035
    67
qed 
wenzelm@7535
    68
wenzelm@9035
    69
end