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/FunctionOrder.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 {* An Order on Functions *}; |
7 |
||
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
8 |
theory FunctionOrder = Subspace + Linearform:; |
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 |
|
7808 | 11 |
|
12 |
subsection {* The graph of a function *} |
|
13 |
||
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
14 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
15 |
types 'a graph = "('a * real) set"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
16 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
17 |
constdefs |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
18 |
graph :: "['a set, 'a => real] => 'a graph " |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
19 |
"graph F f == {p. EX x. p = (x, f x) & x:F}"; (* == {(x, f x). x:F} *) |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
20 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
21 |
constdefs |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
22 |
domain :: "'a graph => 'a set" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
23 |
"domain g == {x. EX y. (x, y):g}"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
24 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
25 |
constdefs |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
26 |
funct :: "'a graph => ('a => real)" |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
27 |
"funct g == %x. (@ y. (x, y):g)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
28 |
|
7566 | 29 |
lemma graphI [intro!!]: "x:F ==> (x, f x) : graph F f"; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
30 |
by (unfold graph_def, intro CollectI exI) force; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
31 |
|
7566 | 32 |
lemma graphI2 [intro!!]: "x:F ==> EX t: (graph F f). t = (x, f x)"; |
33 |
by (unfold graph_def, force); |
|
34 |
||
35 |
lemma graphD1 [intro!!]: "(x, y): graph F f ==> x:F"; |
|
36 |
by (unfold graph_def, elim CollectE exE) force; |
|
37 |
||
38 |
lemma graphD2 [intro!!]: "(x, y): graph H h ==> y = h x"; |
|
39 |
by (unfold graph_def, elim CollectE exE) force; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
40 |
|
7808 | 41 |
lemma graph_extD1 [intro!!]: |
42 |
"[| graph H h <= graph H' h'; x:H |] ==> h x = h' x"; |
|
7566 | 43 |
by (unfold graph_def, force); |
44 |
||
45 |
lemma graph_extD2 [intro!!]: "[| graph H h <= graph H' h' |] ==> H <= H'"; |
|
46 |
by (unfold graph_def, force); |
|
47 |
||
7808 | 48 |
lemma graph_extI: |
49 |
"[| !! x. x: H ==> h x = h' x; H <= H'|] ==> graph H h <= graph H' h'"; |
|
7566 | 50 |
by (unfold graph_def, force); |
51 |
||
52 |
lemma graph_domain_funct: |
|
7808 | 53 |
"(!!x y z. (x, y):g ==> (x, z):g ==> z = y) |
54 |
==> graph (domain g) (funct g) = g"; |
|
7566 | 55 |
proof (unfold domain_def, unfold funct_def, unfold graph_def, auto); |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
56 |
fix a b; assume "(a, b) : g"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
57 |
show "(a, SOME y. (a, y) : g) : g"; by (rule selectI2); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
58 |
show "EX y. (a, y) : g"; ..; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
59 |
assume uniq: "!!x y z. (x, y):g ==> (x, z):g ==> z = y"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
60 |
show "b = (SOME y. (a, y) : g)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
61 |
proof (rule select_equality [RS sym]); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
62 |
fix y; assume "(a, y):g"; show "y = b"; by (rule uniq); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
63 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
64 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
65 |
|
7808 | 66 |
|
67 |
||
68 |
subsection {* The set of norm preserving extensions of a function *} |
|
69 |
||
70 |
||
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
71 |
constdefs |
7656 | 72 |
norm_pres_extensions :: |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
73 |
"['a set, 'a => real, 'a set, 'a => real] => 'a graph set" |
7656 | 74 |
"norm_pres_extensions E p F f == {g. EX H h. graph H h = g |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
75 |
& is_linearform H h |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
76 |
& is_subspace H E |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
77 |
& is_subspace F H |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
78 |
& (graph F f <= graph H h) |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
79 |
& (ALL x:H. h x <= p x)}"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
80 |
|
7656 | 81 |
lemma norm_pres_extension_D: |
82 |
"(g: norm_pres_extensions E p F f) ==> (EX H h. graph H h = g |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
83 |
& is_linearform H h |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
84 |
& is_subspace H E |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
85 |
& is_subspace F H |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
86 |
& (graph F f <= graph H h) |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
87 |
& (ALL x:H. h x <= p x))"; |
7656 | 88 |
by (unfold norm_pres_extensions_def) force; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
89 |
|
7656 | 90 |
lemma norm_pres_extensionI2 [intro]: |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
91 |
"[| is_linearform H h; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
92 |
is_subspace H E; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
93 |
is_subspace F H; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
94 |
(graph F f <= graph H h); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
95 |
(ALL x:H. h x <= p x) |] |
7656 | 96 |
==> (graph H h : norm_pres_extensions E p F f)"; |
97 |
by (unfold norm_pres_extensions_def) force; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
98 |
|
7656 | 99 |
lemma norm_pres_extensionI [intro]: |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
100 |
"(EX H h. graph H h = g |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
101 |
& is_linearform H h |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
102 |
& is_subspace H E |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
103 |
& is_subspace F H |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
104 |
& (graph F f <= graph H h) |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
105 |
& (ALL x:H. h x <= p x)) |
7656 | 106 |
==> (g: norm_pres_extensions E p F f) "; |
107 |
by (unfold norm_pres_extensions_def) force; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
108 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
109 |
end; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
110 |