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