src/HOL/Real/HahnBanach/Linearform.thy
author nipkow
Thu, 13 Apr 2000 15:01:50 +0200
changeset 8703 816d8f6513be
parent 8203 2fcc6017cb72
child 9013 9dd0274f76af
permissions -rw-r--r--
Times -> <*> ** -> <*lex*>
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
7808
fd019ac3485f update from Gertrud;
wenzelm
parents: 7656
diff changeset
     6
header {* Linearforms *};
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
     7
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
     8
theory Linearform = VectorSpace:;
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
     9
7978
1b99ee57d131 final update by Gertrud Bauer;
wenzelm
parents: 7917
diff changeset
    10
text{* A \emph{linear form} is a function on a vector
1b99ee57d131 final update by Gertrud Bauer;
wenzelm
parents: 7917
diff changeset
    11
space into the reals that is additive and multiplicative. *};
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    12
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    13
constdefs
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    14
  is_linearform :: "['a::{minus, plus} set, 'a => real] => bool" 
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    15
  "is_linearform V f == 
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    16
      (ALL x: V. ALL y: V. f (x + y) = f x + f y) &
8703
816d8f6513be Times -> <*>
nipkow
parents: 8203
diff changeset
    17
      (ALL x: V. ALL a. f (a (*) x) = a * (f x))"; 
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    18
7808
fd019ac3485f update from Gertrud;
wenzelm
parents: 7656
diff changeset
    19
lemma is_linearformI [intro]: 
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    20
  "[| !! x y. [| x : V; y : V |] ==> f (x + y) = f x + f y;
8703
816d8f6513be Times -> <*>
nipkow
parents: 8203
diff changeset
    21
    !! x c. x : V ==> f (c (*) x) = c * f x |]
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    22
 ==> is_linearform V f";
7566
c5a3f980a7af accomodate refined facts handling;
wenzelm
parents: 7535
diff changeset
    23
 by (unfold is_linearform_def) force;
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    24
8203
2fcc6017cb72 intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents: 7978
diff changeset
    25
lemma linearform_add [intro??]: 
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    26
  "[| is_linearform V f; x:V; y:V |] ==> f (x + y) = f x + f y";
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    27
  by (unfold is_linearform_def) fast;
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    28
8203
2fcc6017cb72 intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents: 7978
diff changeset
    29
lemma linearform_mult [intro??]: 
8703
816d8f6513be Times -> <*>
nipkow
parents: 8203
diff changeset
    30
  "[| is_linearform V f; x:V |] ==>  f (a (*) x) = a * (f x)"; 
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    31
  by (unfold is_linearform_def) fast;
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    32
8203
2fcc6017cb72 intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents: 7978
diff changeset
    33
lemma linearform_neg [intro??]:
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    34
  "[|  is_vectorspace V; is_linearform V f; x:V|] 
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    35
  ==> f (- x) = - f x";
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    36
proof -; 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    37
  assume "is_linearform V f" "is_vectorspace V" "x:V"; 
8703
816d8f6513be Times -> <*>
nipkow
parents: 8203
diff changeset
    38
  have "f (- x) = f ((- 1r) (*) x)"; by (simp! add: negate_eq1);
7978
1b99ee57d131 final update by Gertrud Bauer;
wenzelm
parents: 7917
diff changeset
    39
  also; have "... = (- 1r) * (f x)"; by (rule linearform_mult);
7566
c5a3f980a7af accomodate refined facts handling;
wenzelm
parents: 7535
diff changeset
    40
  also; have "... = - (f x)"; by (simp!);
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    41
  finally; show ?thesis; .;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    42
qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    43
8203
2fcc6017cb72 intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents: 7978
diff changeset
    44
lemma linearform_diff [intro??]: 
7808
fd019ac3485f update from Gertrud;
wenzelm
parents: 7656
diff changeset
    45
  "[| is_vectorspace V; is_linearform V f; x:V; y:V |] 
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    46
  ==> f (x - y) = f x - f y";  
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    47
proof -;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    48
  assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V";
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    49
  have "f (x - y) = f (x + - y)"; by (simp! only: diff_eq1);
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    50
  also; have "... = f x + f (- y)"; 
7978
1b99ee57d131 final update by Gertrud Bauer;
wenzelm
parents: 7917
diff changeset
    51
    by (rule linearform_add) (simp!)+;
1b99ee57d131 final update by Gertrud Bauer;
wenzelm
parents: 7917
diff changeset
    52
  also; have "f (- y) = - f y"; by (rule linearform_neg);
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    53
  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
    54
qed;
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    55
7978
1b99ee57d131 final update by Gertrud Bauer;
wenzelm
parents: 7917
diff changeset
    56
text{* Every linear form yields $0$ for the $\zero$ vector.*};
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    57
8203
2fcc6017cb72 intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents: 7978
diff changeset
    58
lemma linearform_zero [intro??, simp]: 
8703
816d8f6513be Times -> <*>
nipkow
parents: 8203
diff changeset
    59
  "[| is_vectorspace V; is_linearform V f |] ==> f 00 = 0r"; 
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    60
proof -; 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    61
  assume "is_vectorspace V" "is_linearform V f";
8703
816d8f6513be Times -> <*>
nipkow
parents: 8203
diff changeset
    62
  have "f 00 = f (00 - 00)"; by (simp!);
816d8f6513be Times -> <*>
nipkow
parents: 8203
diff changeset
    63
  also; have "... = f 00 - f 00"; 
7978
1b99ee57d131 final update by Gertrud Bauer;
wenzelm
parents: 7917
diff changeset
    64
    by (rule linearform_diff) (simp!)+;
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    65
  also; have "... = 0r"; by simp;
8703
816d8f6513be Times -> <*>
nipkow
parents: 8203
diff changeset
    66
  finally; show "f 00 = 0r"; .;
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    67
qed; 
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    68
7808
fd019ac3485f update from Gertrud;
wenzelm
parents: 7656
diff changeset
    69
end;