src/HOL/Real/HahnBanach/Linearform.thy
author wenzelm
Sat Dec 16 21:41:51 2000 +0100 (2000-12-16)
changeset 10687 c186279eecea
parent 9408 d3d56e1d2ec1
child 11701 3d51fbf81c17
permissions -rw-r--r--
tuned HOL/Real/HahnBanach;
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@10687
    10
text {*
wenzelm@10687
    11
  A \emph{linear form} is a function on a vector space into the reals
wenzelm@10687
    12
  that is additive and multiplicative.
wenzelm@10687
    13
*}
wenzelm@7535
    14
wenzelm@7535
    15
constdefs
wenzelm@10687
    16
  is_linearform :: "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
wenzelm@10687
    17
  "is_linearform V f \<equiv>
bauerg@9374
    18
      (\<forall>x \<in> V. \<forall>y \<in> V. f (x + y) = f x + f y) \<and>
wenzelm@10687
    19
      (\<forall>x \<in> V. \<forall>a. f (a \<cdot> x) = a * (f x))"
wenzelm@7535
    20
wenzelm@10687
    21
lemma is_linearformI [intro]:
wenzelm@10687
    22
  "(\<And>x y. x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y) \<Longrightarrow>
wenzelm@10687
    23
    (\<And>x c. x \<in> V \<Longrightarrow> f (c \<cdot> x) = c * f x)
wenzelm@10687
    24
 \<Longrightarrow> is_linearform V f"
wenzelm@10687
    25
 by (unfold is_linearform_def) blast
wenzelm@7535
    26
wenzelm@10687
    27
lemma linearform_add [intro?]:
wenzelm@10687
    28
  "is_linearform V f \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
wenzelm@10687
    29
  by (unfold is_linearform_def) blast
wenzelm@7535
    30
wenzelm@10687
    31
lemma linearform_mult [intro?]:
wenzelm@10687
    32
  "is_linearform V f \<Longrightarrow> x \<in> V \<Longrightarrow>  f (a \<cdot> x) = a * (f x)"
wenzelm@10687
    33
  by (unfold is_linearform_def) blast
wenzelm@7535
    34
wenzelm@9408
    35
lemma linearform_neg [intro?]:
wenzelm@10687
    36
  "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> x \<in> V
wenzelm@10687
    37
  \<Longrightarrow> f (- x) = - f x"
wenzelm@10687
    38
proof -
wenzelm@10687
    39
  assume "is_linearform V f"  "is_vectorspace V"  "x \<in> V"
bauerg@9374
    40
  have "f (- x) = f ((- #1) \<cdot> x)" by (simp! add: negate_eq1)
wenzelm@9035
    41
  also have "... = (- #1) * (f x)" by (rule linearform_mult)
wenzelm@9035
    42
  also have "... = - (f x)" by (simp!)
wenzelm@9035
    43
  finally show ?thesis .
wenzelm@9035
    44
qed
wenzelm@7535
    45
wenzelm@10687
    46
lemma linearform_diff [intro?]:
wenzelm@10687
    47
  "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V
wenzelm@10687
    48
  \<Longrightarrow> f (x - y) = f x - f y"
wenzelm@9035
    49
proof -
wenzelm@10687
    50
  assume "is_vectorspace V"  "is_linearform V f"  "x \<in> V"  "y \<in> V"
wenzelm@9035
    51
  have "f (x - y) = f (x + - y)" by (simp! only: diff_eq1)
wenzelm@10687
    52
  also have "... = f x + f (- y)"
wenzelm@9035
    53
    by (rule linearform_add) (simp!)+
wenzelm@9035
    54
  also have "f (- y) = - f y" by (rule linearform_neg)
wenzelm@9035
    55
  finally show "f (x - y) = f x - f y" by (simp!)
wenzelm@9035
    56
qed
wenzelm@7535
    57
wenzelm@10687
    58
text {* Every linear form yields @{text 0} for the @{text 0} vector. *}
wenzelm@7917
    59
wenzelm@10687
    60
lemma linearform_zero [intro?, simp]:
wenzelm@10687
    61
  "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> f 0 = #0"
wenzelm@10687
    62
proof -
wenzelm@10687
    63
  assume "is_vectorspace V"  "is_linearform V f"
bauerg@9374
    64
  have "f 0 = f (0 - 0)" by (simp!)
wenzelm@10687
    65
  also have "... = f 0 - f 0"
wenzelm@9035
    66
    by (rule linearform_diff) (simp!)+
wenzelm@9035
    67
  also have "... = #0" by simp
bauerg@9374
    68
  finally show "f 0 = #0" .
wenzelm@10687
    69
qed
wenzelm@7535
    70
wenzelm@10687
    71
end