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