author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 44887  7ca82df6e951 
child 58744  c434e37f290e 
permissions  rwrr 
31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29197
diff
changeset

1 
(* Title: HOL/Hahn_Banach/Function_Order.thy 
7566  2 
Author: Gertrud Bauer, TU Munich 
3 
*) 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

4 

9035  5 
header {* An order on functions *} 
7808  6 

31795
be3e1cc5005c
standard naming conventions for session and theories;
wenzelm
parents:
29197
diff
changeset

7 
theory Function_Order 
27612  8 
imports Subspace Linearform 
9 
begin 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

10 

9035  11 
subsection {* The graph of a function *} 
7808  12 

10687  13 
text {* 
14 
We define the \emph{graph} of a (real) function @{text f} with 

15 
domain @{text F} as the set 

16 
\begin{center} 

17 
@{text "{(x, f x). x \<in> F}"} 

18 
\end{center} 

19 
So we are modeling partial functions by specifying the domain and 

20 
the mapping function. We use the term ``function'' also for its 

21 
graph. 

9035  22 
*} 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

23 

41818  24 
type_synonym 'a graph = "('a \<times> real) set" 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

25 

44887  26 
definition graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph" 
27 
where "graph F f = {(x, f x)  x. x \<in> F}" 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

28 

13515  29 
lemma graphI [intro]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f" 
27612  30 
unfolding graph_def by blast 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

31 

13515  32 
lemma graphI2 [intro?]: "x \<in> F \<Longrightarrow> \<exists>t \<in> graph F f. t = (x, f x)" 
27612  33 
unfolding graph_def by blast 
7566  34 

13515  35 
lemma graphE [elim?]: 
44887  36 
assumes "(x, y) \<in> graph F f" 
37 
obtains "x \<in> F" and "y = f x" 

38 
using assms unfolding graph_def by blast 

10687  39 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

40 

9035  41 
subsection {* Functions ordered by domain extension *} 
7917  42 

13515  43 
text {* 
44 
A function @{text h'} is an extension of @{text h}, iff the graph of 

45 
@{text h} is a subset of the graph of @{text h'}. 

46 
*} 

7917  47 

10687  48 
lemma graph_extI: 
49 
"(\<And>x. x \<in> H \<Longrightarrow> h x = h' x) \<Longrightarrow> H \<subseteq> H' 

13515  50 
\<Longrightarrow> graph H h \<subseteq> graph H' h'" 
27612  51 
unfolding graph_def by blast 
7917  52 

44887  53 
lemma graph_extD1 [dest?]: "graph H h \<subseteq> graph H' h' \<Longrightarrow> x \<in> H \<Longrightarrow> h x = h' x" 
27612  54 
unfolding graph_def by blast 
7566  55 

44887  56 
lemma graph_extD2 [dest?]: "graph H h \<subseteq> graph H' h' \<Longrightarrow> H \<subseteq> H'" 
27612  57 
unfolding graph_def by blast 
7566  58 

13515  59 

9035  60 
subsection {* Domain and function of a graph *} 
7917  61 

10687  62 
text {* 
13515  63 
The inverse functions to @{text graph} are @{text domain} and @{text 
64 
funct}. 

10687  65 
*} 
7917  66 

44887  67 
definition domain :: "'a graph \<Rightarrow> 'a set" 
68 
where "domain g = {x. \<exists>y. (x, y) \<in> g}" 

7917  69 

44887  70 
definition funct :: "'a graph \<Rightarrow> ('a \<Rightarrow> real)" 
71 
where "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))" 

7917  72 

10687  73 
text {* 
74 
The following lemma states that @{text g} is the graph of a function 

75 
if the relation induced by @{text g} is unique. 

76 
*} 

7566  77 

10687  78 
lemma graph_domain_funct: 
13515  79 
assumes uniq: "\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y" 
80 
shows "graph (domain g) (funct g) = g" 

27612  81 
unfolding domain_def funct_def graph_def 
82 
proof auto (* FIXME !? *) 

23378  83 
fix a b assume g: "(a, b) \<in> g" 
84 
from g show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2) 

85 
from g show "\<exists>y. (a, y) \<in> g" .. 

86 
from g show "b = (SOME y. (a, y) \<in> g)" 

9969  87 
proof (rule some_equality [symmetric]) 
13515  88 
fix y assume "(a, y) \<in> g" 
23378  89 
with g show "y = b" by (rule uniq) 
9035  90 
qed 
91 
qed 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

92 

7808  93 

9035  94 
subsection {* Normpreserving extensions of a function *} 
7917  95 

10687  96 
text {* 
97 
Given a linear form @{text f} on the space @{text F} and a seminorm 

98 
@{text p} on @{text E}. The set of all linear extensions of @{text 

99 
f}, to superspaces @{text H} of @{text F}, which are bounded by 

100 
@{text p}, is defined as follows. 

101 
*} 

7808  102 

19736  103 
definition 
10687  104 
norm_pres_extensions :: 
25762  105 
"'a::{plus, minus, uminus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) 
44887  106 
\<Rightarrow> 'a graph set" 
107 
where 

108 
"norm_pres_extensions E p F f 

109 
= {g. \<exists>H h. g = graph H h 

110 
\<and> linearform H h 

111 
\<and> H \<unlhd> E 

112 
\<and> F \<unlhd> H 

113 
\<and> graph F f \<subseteq> graph H h 

114 
\<and> (\<forall>x \<in> H. h x \<le> p x)}" 

10687  115 

13515  116 
lemma norm_pres_extensionE [elim]: 
44887  117 
assumes "g \<in> norm_pres_extensions E p F f" 
118 
obtains H h 

119 
where "g = graph H h" 

120 
and "linearform H h" 

121 
and "H \<unlhd> E" 

122 
and "F \<unlhd> H" 

123 
and "graph F f \<subseteq> graph H h" 

124 
and "\<forall>x \<in> H. h x \<le> p x" 

125 
using assms unfolding norm_pres_extensions_def by blast 

7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

126 

10687  127 
lemma norm_pres_extensionI2 [intro]: 
13515  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" 

27612  131 
unfolding norm_pres_extensions_def by blast 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

132 

13515  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" 

27612  140 
unfolding norm_pres_extensions_def by blast 
7535
599d3414b51d
The HahnBanach theorem for real vectorspaces (Isabelle/Isar)
wenzelm
parents:
diff
changeset

141 

10687  142 
end 