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