src/HOL/Hahn_Banach/Linearform.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 31795 be3e1cc5005c
child 58744 c434e37f290e
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 29252
diff changeset
     1
(*  Title:      HOL/Hahn_Banach/Linearform.thy
7566
c5a3f980a7af accomodate refined facts handling;
wenzelm
parents: 7535
diff changeset
     2
    Author:     Gertrud Bauer, TU Munich
c5a3f980a7af accomodate refined facts handling;
wenzelm
parents: 7535
diff changeset
     3
*)
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
     4
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
     5
header {* Linearforms *}
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
     6
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
     7
theory Linearform
31795
be3e1cc5005c standard naming conventions for session and theories;
wenzelm
parents: 29252
diff changeset
     8
imports Vector_Space
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
     9
begin
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    10
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    11
text {*
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    12
  A \emph{linear form} is a function on a vector space into the reals
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    13
  that is additive and multiplicative.
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    14
*}
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    15
29234
60f7fb56f8cd More porting to new locales.
ballarin
parents: 27612
diff changeset
    16
locale linearform =
60f7fb56f8cd More porting to new locales.
ballarin
parents: 27612
diff changeset
    17
  fixes V :: "'a\<Colon>{minus, plus, zero, uminus} set" and f
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    18
  assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y"
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    19
    and mult [iff]: "x \<in> V \<Longrightarrow> f (a \<cdot> x) = a * f x"
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    20
14254
342634f38451 Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents: 13547
diff changeset
    21
declare linearform.intro [intro?]
342634f38451 Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by
ballarin
parents: 13547
diff changeset
    22
13547
wenzelm
parents: 13515
diff changeset
    23
lemma (in linearform) neg [iff]:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25762
diff changeset
    24
  assumes "vectorspace V"
13547
wenzelm
parents: 13515
diff changeset
    25
  shows "x \<in> V \<Longrightarrow> f (- x) = - f x"
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    26
proof -
29234
60f7fb56f8cd More porting to new locales.
ballarin
parents: 27612
diff changeset
    27
  interpret vectorspace V by fact
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    28
  assume x: "x \<in> V"
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
    29
  then have "f (- x) = f ((- 1) \<cdot> x)" by (simp add: negate_eq1)
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
    30
  also from x have "\<dots> = (- 1) * (f x)" by (rule mult)
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
    31
  also from x have "\<dots> = - (f x)" by simp
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    32
  finally show ?thesis .
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    33
qed
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    34
13547
wenzelm
parents: 13515
diff changeset
    35
lemma (in linearform) diff [iff]:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25762
diff changeset
    36
  assumes "vectorspace V"
13547
wenzelm
parents: 13515
diff changeset
    37
  shows "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x - y) = f x - f y"
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    38
proof -
29234
60f7fb56f8cd More porting to new locales.
ballarin
parents: 27612
diff changeset
    39
  interpret vectorspace V by fact
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    40
  assume x: "x \<in> V" and y: "y \<in> V"
27612
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
    41
  then have "x - y = x + - y" by (rule diff_eq1)
d3eb431db035 modernized specifications and proofs;
wenzelm
parents: 27611
diff changeset
    42
  also have "f \<dots> = f x + f (- y)" by (rule add) (simp_all add: x y)
23378
1d138d6bb461 tuned proofs: avoid implicit prems;
wenzelm
parents: 16417
diff changeset
    43
  also have "f (- y) = - f y" using `vectorspace V` y by (rule neg)
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    44
  finally show ?thesis by simp
9035
371f023d3dbd removed explicit terminator (";");
wenzelm
parents: 9013
diff changeset
    45
qed
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    46
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    47
text {* Every linear form yields @{text 0} for the @{text 0} vector. *}
7917
5e5b9813cce7 HahnBanach update by Gertrud Bauer;
wenzelm
parents: 7808
diff changeset
    48
13547
wenzelm
parents: 13515
diff changeset
    49
lemma (in linearform) zero [iff]:
27611
2c01c0bdb385 Removed uses of context element includes.
ballarin
parents: 25762
diff changeset
    50
  assumes "vectorspace V"
13547
wenzelm
parents: 13515
diff changeset
    51
  shows "f 0 = 0"
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    52
proof -
29234
60f7fb56f8cd More porting to new locales.
ballarin
parents: 27612
diff changeset
    53
  interpret vectorspace V by fact
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    54
  have "f 0 = f (0 - 0)" by simp
23378
1d138d6bb461 tuned proofs: avoid implicit prems;
wenzelm
parents: 16417
diff changeset
    55
  also have "\<dots> = f 0 - f 0" using `vectorspace V` by (rule diff) simp_all
13515
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    56
  also have "\<dots> = 0" by simp
a6a7025fd7e8 updated to use locales (still some rough edges);
wenzelm
parents: 12018
diff changeset
    57
  finally show ?thesis .
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    58
qed
7535
599d3414b51d The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff changeset
    59
10687
c186279eecea tuned HOL/Real/HahnBanach;
wenzelm
parents: 9408
diff changeset
    60
end