1 (* Title: HOL/Real/HahnBanach/FunctionOrder.thy |
|
2 ID: $Id$ |
|
3 Author: Gertrud Bauer, TU Munich |
|
4 *) |
|
5 |
|
6 header {* An order on functions *} |
|
7 |
|
8 theory FunctionOrder |
|
9 imports Subspace Linearform |
|
10 begin |
|
11 |
|
12 subsection {* The graph of a function *} |
|
13 |
|
14 text {* |
|
15 We define the \emph{graph} of a (real) function @{text f} with |
|
16 domain @{text F} as the set |
|
17 \begin{center} |
|
18 @{text "{(x, f x). x \<in> F}"} |
|
19 \end{center} |
|
20 So we are modeling partial functions by specifying the domain and |
|
21 the mapping function. We use the term ``function'' also for its |
|
22 graph. |
|
23 *} |
|
24 |
|
25 types 'a graph = "('a \<times> real) set" |
|
26 |
|
27 definition |
|
28 graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph" where |
|
29 "graph F f = {(x, f x) | x. x \<in> F}" |
|
30 |
|
31 lemma graphI [intro]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f" |
|
32 unfolding graph_def by blast |
|
33 |
|
34 lemma graphI2 [intro?]: "x \<in> F \<Longrightarrow> \<exists>t \<in> graph F f. t = (x, f x)" |
|
35 unfolding graph_def by blast |
|
36 |
|
37 lemma graphE [elim?]: |
|
38 "(x, y) \<in> graph F f \<Longrightarrow> (x \<in> F \<Longrightarrow> y = f x \<Longrightarrow> C) \<Longrightarrow> C" |
|
39 unfolding graph_def by blast |
|
40 |
|
41 |
|
42 subsection {* Functions ordered by domain extension *} |
|
43 |
|
44 text {* |
|
45 A function @{text h'} is an extension of @{text h}, iff the graph of |
|
46 @{text h} is a subset of the graph of @{text h'}. |
|
47 *} |
|
48 |
|
49 lemma graph_extI: |
|
50 "(\<And>x. x \<in> H \<Longrightarrow> h x = h' x) \<Longrightarrow> H \<subseteq> H' |
|
51 \<Longrightarrow> graph H h \<subseteq> graph H' h'" |
|
52 unfolding graph_def by blast |
|
53 |
|
54 lemma graph_extD1 [dest?]: |
|
55 "graph H h \<subseteq> graph H' h' \<Longrightarrow> x \<in> H \<Longrightarrow> h x = h' x" |
|
56 unfolding graph_def by blast |
|
57 |
|
58 lemma graph_extD2 [dest?]: |
|
59 "graph H h \<subseteq> graph H' h' \<Longrightarrow> H \<subseteq> H'" |
|
60 unfolding graph_def by blast |
|
61 |
|
62 |
|
63 subsection {* Domain and function of a graph *} |
|
64 |
|
65 text {* |
|
66 The inverse functions to @{text graph} are @{text domain} and @{text |
|
67 funct}. |
|
68 *} |
|
69 |
|
70 definition |
|
71 "domain" :: "'a graph \<Rightarrow> 'a set" where |
|
72 "domain g = {x. \<exists>y. (x, y) \<in> g}" |
|
73 |
|
74 definition |
|
75 funct :: "'a graph \<Rightarrow> ('a \<Rightarrow> real)" where |
|
76 "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))" |
|
77 |
|
78 text {* |
|
79 The following lemma states that @{text g} is the graph of a function |
|
80 if the relation induced by @{text g} is unique. |
|
81 *} |
|
82 |
|
83 lemma graph_domain_funct: |
|
84 assumes uniq: "\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y" |
|
85 shows "graph (domain g) (funct g) = g" |
|
86 unfolding domain_def funct_def graph_def |
|
87 proof auto (* FIXME !? *) |
|
88 fix a b assume g: "(a, b) \<in> g" |
|
89 from g show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2) |
|
90 from g show "\<exists>y. (a, y) \<in> g" .. |
|
91 from g show "b = (SOME y. (a, y) \<in> g)" |
|
92 proof (rule some_equality [symmetric]) |
|
93 fix y assume "(a, y) \<in> g" |
|
94 with g show "y = b" by (rule uniq) |
|
95 qed |
|
96 qed |
|
97 |
|
98 |
|
99 subsection {* Norm-preserving extensions of a function *} |
|
100 |
|
101 text {* |
|
102 Given a linear form @{text f} on the space @{text F} and a seminorm |
|
103 @{text p} on @{text E}. The set of all linear extensions of @{text |
|
104 f}, to superspaces @{text H} of @{text F}, which are bounded by |
|
105 @{text p}, is defined as follows. |
|
106 *} |
|
107 |
|
108 definition |
|
109 norm_pres_extensions :: |
|
110 "'a::{plus, minus, uminus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) |
|
111 \<Rightarrow> 'a graph set" where |
|
112 "norm_pres_extensions E p F f |
|
113 = {g. \<exists>H h. g = graph H h |
|
114 \<and> linearform H h |
|
115 \<and> H \<unlhd> E |
|
116 \<and> F \<unlhd> H |
|
117 \<and> graph F f \<subseteq> graph H h |
|
118 \<and> (\<forall>x \<in> H. h x \<le> p x)}" |
|
119 |
|
120 lemma norm_pres_extensionE [elim]: |
|
121 "g \<in> norm_pres_extensions E p F f |
|
122 \<Longrightarrow> (\<And>H h. g = graph H h \<Longrightarrow> linearform H h |
|
123 \<Longrightarrow> H \<unlhd> E \<Longrightarrow> F \<unlhd> H \<Longrightarrow> graph F f \<subseteq> graph H h |
|
124 \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x \<Longrightarrow> C) \<Longrightarrow> C" |
|
125 unfolding norm_pres_extensions_def by blast |
|
126 |
|
127 lemma norm_pres_extensionI2 [intro]: |
|
128 "linearform H h \<Longrightarrow> H \<unlhd> E \<Longrightarrow> F \<unlhd> H |
|
129 \<Longrightarrow> graph F f \<subseteq> graph H h \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x |
|
130 \<Longrightarrow> graph H h \<in> norm_pres_extensions E p F f" |
|
131 unfolding norm_pres_extensions_def by blast |
|
132 |
|
133 lemma norm_pres_extensionI: (* FIXME ? *) |
|
134 "\<exists>H h. g = graph H h |
|
135 \<and> linearform H h |
|
136 \<and> H \<unlhd> E |
|
137 \<and> F \<unlhd> H |
|
138 \<and> graph F f \<subseteq> graph H h |
|
139 \<and> (\<forall>x \<in> H. h x \<le> p x) \<Longrightarrow> g \<in> norm_pres_extensions E p F f" |
|
140 unfolding norm_pres_extensions_def by blast |
|
141 |
|
142 end |
|