author | wenzelm |
Fri, 22 Oct 1999 20:14:31 +0200 | |
changeset 7917 | 5e5b9813cce7 |
parent 7808 | fd019ac3485f |
child 7927 | b50446a33c16 |
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 |
|
7917 | 6 |
header {* An Order on functions *}; |
7808 | 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 |
|
7917 | 11 |
subsection {* The graph of a function *}; |
7808 | 12 |
|
7917 | 13 |
text{* We define the \emph{graph} of a (real) function $f$ with the |
14 |
domain $F$ as the set |
|
15 |
\begin{matharray}{l} |
|
16 |
\{(x, f\ap x). \ap x:F\}. |
|
17 |
\end{matharray} |
|
18 |
So we are modelling partial functions by specifying the domain and |
|
19 |
the mapping function. We use the notion 'function' also for the graph |
|
20 |
of a function. |
|
21 |
*}; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
22 |
|
7917 | 23 |
types 'a graph = "('a::{minus, plus} * real) set"; |
7535
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 |
graph :: "['a set, 'a => real] => 'a graph " |
7917 | 27 |
"graph F f == {p. EX x. p = (x, f x) & x:F}"; (* |
28 |
== {(x, f x). x:F} *) |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
29 |
|
7566 | 30 |
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
|
31 |
by (unfold graph_def, intro CollectI exI) force; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
32 |
|
7566 | 33 |
lemma graphI2 [intro!!]: "x:F ==> EX t: (graph F f). t = (x, f x)"; |
34 |
by (unfold graph_def, force); |
|
35 |
||
36 |
lemma graphD1 [intro!!]: "(x, y): graph F f ==> x:F"; |
|
37 |
by (unfold graph_def, elim CollectE exE) force; |
|
38 |
||
39 |
lemma graphD2 [intro!!]: "(x, y): graph H h ==> y = h x"; |
|
40 |
by (unfold graph_def, elim CollectE exE) force; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
41 |
|
7917 | 42 |
subsection {* Functions ordered by domain extension *}; |
43 |
||
44 |
text{* The function $h'$ is an extension of $h$, iff the graph of |
|
45 |
$h$ is a subset of the graph of $h'$.*}; |
|
46 |
||
47 |
lemma graph_extI: |
|
48 |
"[| !! x. x: H ==> h x = h' x; H <= H'|] |
|
49 |
==> graph H h <= graph H' h'"; |
|
50 |
by (unfold graph_def, force); |
|
51 |
||
7808 | 52 |
lemma graph_extD1 [intro!!]: |
53 |
"[| graph H h <= graph H' h'; x:H |] ==> h x = h' x"; |
|
7566 | 54 |
by (unfold graph_def, force); |
55 |
||
7917 | 56 |
lemma graph_extD2 [intro!!]: |
57 |
"[| graph H h <= graph H' h' |] ==> H <= H'"; |
|
7566 | 58 |
by (unfold graph_def, force); |
59 |
||
7917 | 60 |
subsection {* Domain and function of a graph *}; |
61 |
||
62 |
text{* The inverse functions to $\idt{graph}$ are $\idt{domain}$ and |
|
63 |
$\idt{funct}$.*}; |
|
64 |
||
65 |
constdefs |
|
66 |
domain :: "'a graph => 'a set" |
|
67 |
"domain g == {x. EX y. (x, y):g}" |
|
68 |
||
69 |
funct :: "'a graph => ('a => real)" |
|
70 |
"funct g == \<lambda>x. (SOME y. (x, y):g)"; |
|
71 |
||
72 |
(*text{* The equations |
|
73 |
\begin{matharray} |
|
74 |
\idt{domain} graph F f = F {\rm and}\\ |
|
75 |
\idt{funct} graph F f = f |
|
76 |
\end{matharray} |
|
77 |
hold, but are not proved here. |
|
78 |
*};*) |
|
79 |
||
80 |
text {* The following lemma states that $g$ is the graph of a function |
|
81 |
if the relation induced by $g$ is unique. *}; |
|
7566 | 82 |
|
83 |
lemma graph_domain_funct: |
|
7808 | 84 |
"(!!x y z. (x, y):g ==> (x, z):g ==> z = y) |
85 |
==> graph (domain g) (funct g) = g"; |
|
7566 | 86 |
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
|
87 |
fix a b; assume "(a, b) : g"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
88 |
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
|
89 |
show "EX y. (a, y) : g"; ..; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
90 |
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
|
91 |
show "b = (SOME y. (a, y) : g)"; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
92 |
proof (rule select_equality [RS sym]); |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
93 |
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
|
94 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
95 |
qed; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
96 |
|
7808 | 97 |
|
98 |
||
7917 | 99 |
subsection {* Norm preserving extensions of a function *}; |
100 |
||
101 |
text {* Given a function $f$ on the space $F$ and a quasinorm $p$ on |
|
102 |
$E$. The set of all linear extensions of $f$, to superspaces $H$ of |
|
103 |
$F$, which are bounded by $p$, is defined as follows. *}; |
|
7808 | 104 |
|
105 |
||
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
106 |
constdefs |
7656 | 107 |
norm_pres_extensions :: |
7917 | 108 |
"['a::{minus, plus} set, 'a => real, 'a set, 'a => real] |
109 |
=> 'a graph set" |
|
110 |
"norm_pres_extensions E p F f |
|
111 |
== {g. EX H h. graph H h = g |
|
112 |
& is_linearform H h |
|
113 |
& is_subspace H E |
|
114 |
& is_subspace F H |
|
115 |
& graph F f <= graph H h |
|
116 |
& (ALL x:H. h x <= p x)}"; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
117 |
|
7656 | 118 |
lemma norm_pres_extension_D: |
7917 | 119 |
"g : norm_pres_extensions E p F f |
120 |
==> EX H h. graph H h = g |
|
121 |
& is_linearform H h |
|
122 |
& is_subspace H E |
|
123 |
& is_subspace F H |
|
124 |
& graph F f <= graph H h |
|
125 |
& (ALL x:H. h x <= p x)"; |
|
126 |
by (unfold norm_pres_extensions_def) force; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
127 |
|
7656 | 128 |
lemma norm_pres_extensionI2 [intro]: |
7917 | 129 |
"[| is_linearform H h; is_subspace H E; is_subspace F H; |
130 |
graph F f <= graph H h; ALL x:H. h x <= p x |] |
|
131 |
==> (graph H h : norm_pres_extensions E p F f)"; |
|
7656 | 132 |
by (unfold norm_pres_extensions_def) force; |
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
133 |
|
7656 | 134 |
lemma norm_pres_extensionI [intro]: |
7917 | 135 |
"EX H h. graph H h = g |
136 |
& is_linearform H h |
|
137 |
& is_subspace H E |
|
138 |
& is_subspace F H |
|
139 |
& graph F f <= graph H h |
|
140 |
& (ALL x:H. h x <= p x) |
|
141 |
==> g: norm_pres_extensions E p F f"; |
|
142 |
by (unfold norm_pres_extensions_def) force; |
|
7535
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
143 |
|
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
144 |
end; |
599d3414b51d
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset
|
145 |