src/HOL/Real/HahnBanach/Linearform.thy
author wenzelm
Fri Sep 10 17:28:51 1999 +0200 (1999-09-10)
changeset 7535 599d3414b51d
child 7566 c5a3f980a7af
permissions -rw-r--r--
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
(by Gertrud Bauer, TU Munich);
wenzelm@7535
     1
wenzelm@7535
     2
theory Linearform = LinearSpace:;
wenzelm@7535
     3
wenzelm@7535
     4
section {* linearforms *};
wenzelm@7535
     5
wenzelm@7535
     6
constdefs
wenzelm@7535
     7
  is_linearform :: "['a set, 'a => real] => bool" 
wenzelm@7535
     8
  "is_linearform V f == 
wenzelm@7535
     9
      (ALL x: V. ALL y: V. f (x [+] y) = f x + f y) &
wenzelm@7535
    10
      (ALL x: V. ALL a. f (a [*] x) = a * (f x))"; 
wenzelm@7535
    11
wenzelm@7535
    12
lemma is_linearformI [intro]: "[| !! x y. [| x : V; y : V |] ==> f (x [+] y) = f x + f y;
wenzelm@7535
    13
    !! x c. x : V ==> f (c [*] x) = c * f x |]
wenzelm@7535
    14
 ==> is_linearform V f";
wenzelm@7535
    15
 by (unfold is_linearform_def, force);
wenzelm@7535
    16
wenzelm@7535
    17
lemma linearform_add_linear: "[| is_linearform V f; x:V; y:V |] ==> f (x [+] y) = f x + f y";
wenzelm@7535
    18
 by (unfold is_linearform_def, auto);
wenzelm@7535
    19
wenzelm@7535
    20
lemma linearform_mult_linear: "[| is_linearform V f; x:V |] ==>  f (a [*] x) = a * (f x)"; 
wenzelm@7535
    21
 by (unfold is_linearform_def, auto);
wenzelm@7535
    22
wenzelm@7535
    23
lemma linearform_neg_linear:
wenzelm@7535
    24
  "[|  is_vectorspace V; is_linearform V f; x:V|] ==> f ([-] x) = - f x";
wenzelm@7535
    25
proof -; 
wenzelm@7535
    26
  assume "is_linearform V f" "is_vectorspace V" "x:V"; 
wenzelm@7535
    27
  have "f ([-] x) = f ((- 1r) [*] x)"; by (asm_simp add: vs_mult_minus_1);
wenzelm@7535
    28
  also; have "... = (- 1r) * (f x)"; by (rule linearform_mult_linear);
wenzelm@7535
    29
  also; have "... = - (f x)"; by asm_simp;
wenzelm@7535
    30
  finally; show ?thesis; .;
wenzelm@7535
    31
qed;
wenzelm@7535
    32
wenzelm@7535
    33
lemma linearform_diff_linear: 
wenzelm@7535
    34
  "[| is_vectorspace V; is_linearform V f; x:V; y:V |] ==> f (x [-] y) = f x - f y";  
wenzelm@7535
    35
proof -;
wenzelm@7535
    36
  assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V";
wenzelm@7535
    37
  have "f (x [-] y) = f (x [+] [-] y)"; by (simp only: diff_def);
wenzelm@7535
    38
  also; have "... = f x + f ([-] y)"; by (rule linearform_add_linear) (asm_simp+);
wenzelm@7535
    39
  also; have "f ([-] y) = - f y"; by (rule linearform_neg_linear);
wenzelm@7535
    40
  finally; show "f (x [-] y) = f x - f y"; by asm_simp;
wenzelm@7535
    41
qed;
wenzelm@7535
    42
wenzelm@7535
    43
lemma linearform_zero: "[| is_vectorspace V; is_linearform V f |] ==> f <0> = 0r"; 
wenzelm@7535
    44
proof -; 
wenzelm@7535
    45
  assume "is_vectorspace V" "is_linearform V f";
wenzelm@7535
    46
  have "f <0> = f (<0> [-] <0>)"; by asm_simp;
wenzelm@7535
    47
  also; have "... = f <0> - f <0>"; by (rule linearform_diff_linear) asm_simp+;
wenzelm@7535
    48
  also; have "... = 0r"; by simp;
wenzelm@7535
    49
  finally; show "f <0> = 0r"; .;
wenzelm@7535
    50
qed; 
wenzelm@7535
    51
wenzelm@7535
    52
end;
wenzelm@7535
    53