src/HOL/Real/HahnBanach/Linearform.thy
author wenzelm
Fri Oct 22 20:14:31 1999 +0200 (1999-10-22)
changeset 7917 5e5b9813cce7
parent 7808 fd019ac3485f
child 7978 1b99ee57d131
permissions -rw-r--r--
HahnBanach update by Gertrud Bauer;
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@7808
     6
header {* Linearforms *};
wenzelm@7535
     7
wenzelm@7917
     8
theory Linearform = VectorSpace:;
wenzelm@7917
     9
wenzelm@7917
    10
text{* A \emph{linearform} is a function on a vector
wenzelm@7917
    11
space into the reals that is linear w.~r.~t.~addition and skalar
wenzelm@7917
    12
multiplikation. *};
wenzelm@7535
    13
wenzelm@7535
    14
constdefs
wenzelm@7917
    15
  is_linearform :: "['a::{minus, plus} set, 'a => real] => bool" 
wenzelm@7535
    16
  "is_linearform V f == 
wenzelm@7917
    17
      (ALL x: V. ALL y: V. f (x + y) = f x + f y) &
wenzelm@7917
    18
      (ALL x: V. ALL a. f (a <*> x) = a * (f x))"; 
wenzelm@7535
    19
wenzelm@7808
    20
lemma is_linearformI [intro]: 
wenzelm@7917
    21
  "[| !! x y. [| x : V; y : V |] ==> f (x + y) = f x + f y;
wenzelm@7917
    22
    !! x c. x : V ==> f (c <*> x) = c * f x |]
wenzelm@7535
    23
 ==> is_linearform V f";
wenzelm@7566
    24
 by (unfold is_linearform_def) force;
wenzelm@7535
    25
wenzelm@7566
    26
lemma linearform_add_linear [intro!!]: 
wenzelm@7917
    27
  "[| is_linearform V f; x:V; y:V |] ==> f (x + y) = f x + f y";
wenzelm@7917
    28
  by (unfold is_linearform_def) fast;
wenzelm@7535
    29
wenzelm@7566
    30
lemma linearform_mult_linear [intro!!]: 
wenzelm@7917
    31
  "[| is_linearform V f; x:V |] ==>  f (a <*> x) = a * (f x)"; 
wenzelm@7917
    32
  by (unfold is_linearform_def) fast;
wenzelm@7535
    33
wenzelm@7566
    34
lemma linearform_neg_linear [intro!!]:
wenzelm@7917
    35
  "[|  is_vectorspace V; is_linearform V f; x:V|] 
wenzelm@7917
    36
  ==> f (- x) = - f x";
wenzelm@7535
    37
proof -; 
wenzelm@7535
    38
  assume "is_linearform V f" "is_vectorspace V" "x:V"; 
wenzelm@7917
    39
  have "f (- x) = f ((- 1r) <*> x)"; by (simp! add: negate_eq1);
wenzelm@7535
    40
  also; have "... = (- 1r) * (f x)"; by (rule linearform_mult_linear);
wenzelm@7566
    41
  also; have "... = - (f x)"; by (simp!);
wenzelm@7535
    42
  finally; show ?thesis; .;
wenzelm@7535
    43
qed;
wenzelm@7535
    44
wenzelm@7566
    45
lemma linearform_diff_linear [intro!!]: 
wenzelm@7808
    46
  "[| is_vectorspace V; is_linearform V f; x:V; y:V |] 
wenzelm@7917
    47
  ==> f (x - y) = f x - f y";  
wenzelm@7535
    48
proof -;
wenzelm@7535
    49
  assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V";
wenzelm@7917
    50
  have "f (x - y) = f (x + - y)"; by (simp! only: diff_eq1);
wenzelm@7917
    51
  also; have "... = f x + f (- y)"; 
wenzelm@7808
    52
    by (rule linearform_add_linear) (simp!)+;
wenzelm@7917
    53
  also; have "f (- y) = - f y"; by (rule linearform_neg_linear);
wenzelm@7917
    54
  finally; show "f (x - y) = f x - f y"; by (simp!);
wenzelm@7535
    55
qed;
wenzelm@7535
    56
wenzelm@7917
    57
text{* Every linearform yields $0$ for the $\zero$ vector.*};
wenzelm@7917
    58
wenzelm@7808
    59
lemma linearform_zero [intro!!, simp]: 
wenzelm@7808
    60
  "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; 
wenzelm@7535
    61
proof -; 
wenzelm@7535
    62
  assume "is_vectorspace V" "is_linearform V f";
wenzelm@7917
    63
  have "f <0> = f (<0> - <0>)"; by (simp!);
wenzelm@7808
    64
  also; have "... = f <0> - f <0>"; 
wenzelm@7808
    65
    by (rule linearform_diff_linear) (simp!)+;
wenzelm@7535
    66
  also; have "... = 0r"; by simp;
wenzelm@7535
    67
  finally; show "f <0> = 0r"; .;
wenzelm@7535
    68
qed; 
wenzelm@7535
    69
wenzelm@7808
    70
end;