src/HOL/Real/HahnBanach/Linearform.thy
author paulson
Fri Nov 02 17:55:24 2001 +0100 (2001-11-02)
changeset 12018 ec054019c910
parent 11701 3d51fbf81c17
child 13515 a6a7025fd7e8
permissions -rw-r--r--
Numerals and simprocs for types real and hypreal. The abstract
constants 0, 1 and binary numerals work harmoniously.
     1 (*  Title:      HOL/Real/HahnBanach/Linearform.thy
     2     ID:         $Id$
     3     Author:     Gertrud Bauer, TU Munich
     4 *)
     5 
     6 header {* Linearforms *}
     7 
     8 theory Linearform = VectorSpace:
     9 
    10 text {*
    11   A \emph{linear form} is a function on a vector space into the reals
    12   that is additive and multiplicative.
    13 *}
    14 
    15 constdefs
    16   is_linearform :: "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
    17   "is_linearform V f \<equiv>
    18       (\<forall>x \<in> V. \<forall>y \<in> V. f (x + y) = f x + f y) \<and>
    19       (\<forall>x \<in> V. \<forall>a. f (a \<cdot> x) = a * (f x))"
    20 
    21 lemma is_linearformI [intro]:
    22   "(\<And>x y. x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y) \<Longrightarrow>
    23     (\<And>x c. x \<in> V \<Longrightarrow> f (c \<cdot> x) = c * f x)
    24  \<Longrightarrow> is_linearform V f"
    25  by (unfold is_linearform_def) blast
    26 
    27 lemma linearform_add [intro?]:
    28   "is_linearform V f \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
    29   by (unfold is_linearform_def) blast
    30 
    31 lemma linearform_mult [intro?]:
    32   "is_linearform V f \<Longrightarrow> x \<in> V \<Longrightarrow>  f (a \<cdot> x) = a * (f x)"
    33   by (unfold is_linearform_def) blast
    34 
    35 lemma linearform_neg [intro?]:
    36   "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> x \<in> V
    37   \<Longrightarrow> f (- x) = - f x"
    38 proof -
    39   assume "is_linearform V f"  "is_vectorspace V"  "x \<in> V"
    40   have "f (- x) = f ((- 1) \<cdot> x)" by (simp! add: negate_eq1)
    41   also have "... = (- 1) * (f x)" by (rule linearform_mult)
    42   also have "... = - (f x)" by (simp!)
    43   finally show ?thesis .
    44 qed
    45 
    46 lemma linearform_diff [intro?]:
    47   "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V
    48   \<Longrightarrow> f (x - y) = f x - f y"
    49 proof -
    50   assume "is_vectorspace V"  "is_linearform V f"  "x \<in> V"  "y \<in> V"
    51   have "f (x - y) = f (x + - y)" by (simp! only: diff_eq1)
    52   also have "... = f x + f (- y)"
    53     by (rule linearform_add) (simp!)+
    54   also have "f (- y) = - f y" by (rule linearform_neg)
    55   finally show "f (x - y) = f x - f y" by (simp!)
    56 qed
    57 
    58 text {* Every linear form yields @{text 0} for the @{text 0} vector. *}
    59 
    60 lemma linearform_zero [intro?, simp]:
    61   "is_vectorspace V \<Longrightarrow> is_linearform V f \<Longrightarrow> f 0 = 0"
    62 proof -
    63   assume "is_vectorspace V"  "is_linearform V f"
    64   have "f 0 = f (0 - 0)" by (simp!)
    65   also have "... = f 0 - f 0"
    66     by (rule linearform_diff) (simp!)+
    67   also have "... = 0" by simp
    68   finally show "f 0 = 0" .
    69 qed
    70 
    71 end