author | wenzelm |
Fri, 08 Oct 1999 16:40:27 +0200 | |
changeset 7808 | fd019ac3485f |
parent 7656 | 2f18c0ffc348 |
child 7917 | 5e5b9813cce7 |
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 |
|
7808 | 6 |
header {* Linearforms *}; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
7 |
|
7808 | 8 |
theory Linearform = LinearSpace:; |
7535
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 |
|
7808 | 16 |
lemma is_linearformI [intro]: |
17 |
"[| !! x y. [| x : V; y : V |] ==> f (x [+] y) = f x + f y; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
18 |
!! x c. x : V ==> f (c [*] x) = c * f x |] |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
19 |
==> is_linearform V f"; |
7566 | 20 |
by (unfold is_linearform_def) force; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
21 |
|
7566 | 22 |
lemma linearform_add_linear [intro!!]: |
23 |
"[| is_linearform V f; x:V; y:V |] ==> f (x [+] y) = f x + f y"; |
|
24 |
by (unfold is_linearform_def) auto; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
25 |
|
7566 | 26 |
lemma linearform_mult_linear [intro!!]: |
27 |
"[| is_linearform V f; x:V |] ==> f (a [*] x) = a * (f x)"; |
|
28 |
by (unfold is_linearform_def) auto; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
29 |
|
7566 | 30 |
lemma linearform_neg_linear [intro!!]: |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
31 |
"[| 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
|
32 |
proof -; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
33 |
assume "is_linearform V f" "is_vectorspace V" "x:V"; |
7808 | 34 |
have "f ([-] x) = f ((- 1r) [*] x)"; by (unfold negate_def) simp; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
35 |
also; have "... = (- 1r) * (f x)"; by (rule linearform_mult_linear); |
7566 | 36 |
also; have "... = - (f x)"; by (simp!); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
37 |
finally; show ?thesis; .; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
38 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
39 |
|
7566 | 40 |
lemma linearform_diff_linear [intro!!]: |
7808 | 41 |
"[| is_vectorspace V; is_linearform V f; x:V; y:V |] |
42 |
==> f (x [-] y) = f x - f y"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
43 |
proof -; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
44 |
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
|
45 |
have "f (x [-] y) = f (x [+] [-] y)"; by (simp only: diff_def); |
7808 | 46 |
also; have "... = f x + f ([-] y)"; |
47 |
by (rule linearform_add_linear) (simp!)+; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
48 |
also; have "f ([-] y) = - f y"; by (rule linearform_neg_linear); |
7566 | 49 |
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
|
50 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
51 |
|
7808 | 52 |
lemma linearform_zero [intro!!, simp]: |
53 |
"[| 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
|
54 |
proof -; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
55 |
assume "is_vectorspace V" "is_linearform V f"; |
7566 | 56 |
have "f <0> = f (<0> [-] <0>)"; by (simp!); |
7808 | 57 |
also; have "... = f <0> - f <0>"; |
58 |
by (rule linearform_diff_linear) (simp!)+; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
59 |
also; have "... = 0r"; by simp; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
60 |
finally; show "f <0> = 0r"; .; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
61 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
62 |
|
7808 | 63 |
end; |