author | wenzelm |
Sun, 04 Jun 2000 19:39:29 +0200 | |
changeset 9035 | 371f023d3dbd |
parent 9013 | 9dd0274f76af |
child 9374 | 153853af318b |
permissions | -rw-r--r-- |
7566 | 1 |
(* Title: HOL/Real/HahnBanach/Linearform.thy |
2 |
ID: $Id$ |
|
3 |
Author: Gertrud Bauer, TU Munich |
|
4 |
*) |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
5 |
|
9035 | 6 |
header {* Linearforms *} |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
7 |
|
9035 | 8 |
theory Linearform = VectorSpace: |
7917 | 9 |
|
7978 | 10 |
text{* A \emph{linear form} is a function on a vector |
9035 | 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 | 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 | 16 |
(ALL x: V. ALL y: V. f (x + y) = f x + f y) & |
9035 | 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 | 19 |
lemma is_linearformI [intro]: |
7917 | 20 |
"[| !! x y. [| x : V; y : V |] ==> f (x + y) = f x + f y; |
8703 | 21 |
!! x c. x : V ==> f (c (*) x) = c * f x |] |
9035 | 22 |
==> is_linearform V f" |
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??]: |
9035 | 26 |
"[| is_linearform V f; x:V; y:V |] ==> f (x + y) = f x + f y" |
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??]: |
9035 | 30 |
"[| is_linearform V f; x:V |] ==> f (a (*) x) = a * (f x)" |
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 | 34 |
"[| is_vectorspace V; is_linearform V f; x:V|] |
9035 | 35 |
==> f (- x) = - f x" |
36 |
proof - |
|
37 |
assume "is_linearform V f" "is_vectorspace V" "x:V" |
|
38 |
have "f (- x) = f ((- #1) (*) x)" by (simp! add: negate_eq1) |
|
39 |
also have "... = (- #1) * (f x)" by (rule linearform_mult) |
|
40 |
also have "... = - (f x)" by (simp!) |
|
41 |
finally show ?thesis . |
|
42 |
qed |
|
7535
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 | 45 |
"[| is_vectorspace V; is_linearform V f; x:V; y:V |] |
9035 | 46 |
==> f (x - y) = f x - f y" |
47 |
proof - |
|
48 |
assume "is_vectorspace V" "is_linearform V f" "x:V" "y:V" |
|
49 |
have "f (x - y) = f (x + - y)" by (simp! only: diff_eq1) |
|
50 |
also have "... = f x + f (- y)" |
|
51 |
by (rule linearform_add) (simp!)+ |
|
52 |
also have "f (- y) = - f y" by (rule linearform_neg) |
|
53 |
finally show "f (x - y) = f x - f y" by (simp!) |
|
54 |
qed |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
55 |
|
9035 | 56 |
text{* Every linear form yields $0$ for the $\zero$ vector.*} |
7917 | 57 |
|
8203
2fcc6017cb72
intro/elim/dest attributes: changed ! / !! flags to ? / ??;
wenzelm
parents:
7978
diff
changeset
|
58 |
lemma linearform_zero [intro??, simp]: |
9035 | 59 |
"[| is_vectorspace V; is_linearform V f |] ==> f 00 = #0" |
60 |
proof - |
|
61 |
assume "is_vectorspace V" "is_linearform V f" |
|
62 |
have "f 00 = f (00 - 00)" by (simp!) |
|
63 |
also have "... = f 00 - f 00" |
|
64 |
by (rule linearform_diff) (simp!)+ |
|
65 |
also have "... = #0" by simp |
|
66 |
finally show "f 00 = #0" . |
|
67 |
qed |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
68 |
|
9035 | 69 |
end |