(*  Title:      HOL/Hahn_Banach/Function_Order.thy

     Author:     Gertrud Bauer, TU Munich

 *)

 header {* An order on functions *}

 theory Function_Order

 imports Subspace Linearform

 begin

 subsection {* The graph of a function *}

 text {*

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

   domain @{text F} as the set

   \begin{center}

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

   \end{center}

   So we are modeling partial functions by specifying the domain and

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

   graph.

 *}

 types 'a graph = "('a \<times> real) set"

 definition

   graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph" where

   "graph F f = {(x, f x) | x. x \<in> F}"

 lemma graphI [intro]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f"

   unfolding graph_def by blast

 lemma graphI2 [intro?]: "x \<in> F \<Longrightarrow> \<exists>t \<in> graph F f. t = (x, f x)"

   unfolding graph_def by blast

 lemma graphE [elim?]:

     "(x, y) \<in> graph F f \<Longrightarrow> (x \<in> F \<Longrightarrow> y = f x \<Longrightarrow> C) \<Longrightarrow> C"

   unfolding graph_def by blast

 subsection {* Functions ordered by domain extension *}

 text {*

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

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

 *}

 lemma graph_extI:

   "(\<And>x. x \<in> H \<Longrightarrow> h x = h' x) \<Longrightarrow> H \<subseteq> H'

     \<Longrightarrow> graph H h \<subseteq> graph H' h'"

   unfolding graph_def by blast

 lemma graph_extD1 [dest?]:

   "graph H h \<subseteq> graph H' h' \<Longrightarrow> x \<in> H \<Longrightarrow> h x = h' x"

   unfolding graph_def by blast

 lemma graph_extD2 [dest?]:

   "graph H h \<subseteq> graph H' h' \<Longrightarrow> H \<subseteq> H'"

   unfolding graph_def by blast

 subsection {* Domain and function of a graph *}

 text {*

   The inverse functions to @{text graph} are @{text domain} and @{text

   funct}.

 *}

 definition

   "domain" :: "'a graph \<Rightarrow> 'a set" where

   "domain g = {x. \<exists>y. (x, y) \<in> g}"

 definition

   funct :: "'a graph \<Rightarrow> ('a \<Rightarrow> real)" where

   "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))"

 text {*

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

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

 *}

 lemma graph_domain_funct:

   assumes uniq: "\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y"

   shows "graph (domain g) (funct g) = g"

   unfolding domain_def funct_def graph_def

 proof auto  (* FIXME !? *)

   fix a b assume g: "(a, b) \<in> g"

   from g show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2)

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

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

   proof (rule some_equality [symmetric])

     fix y assume "(a, y) \<in> g"

     with g show "y = b" by (rule uniq)

   qed

 qed

 subsection {* Norm-preserving extensions of a function *}

 text {*

   Given a linear form @{text f} on the space @{text F} and a seminorm

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

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

   @{text p}, is defined as follows.

 *}

 definition

   norm_pres_extensions ::

     "'a::{plus, minus, uminus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)

       \<Rightarrow> 'a graph set" where

     "norm_pres_extensions E p F f

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

           \<and> linearform H h

           \<and> H \<unlhd> E

           \<and> F \<unlhd> H

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

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

 lemma norm_pres_extensionE [elim]:

   "g \<in> norm_pres_extensions E p F f

   \<Longrightarrow> (\<And>H h. g = graph H h \<Longrightarrow> linearform H h

         \<Longrightarrow> H \<unlhd> E \<Longrightarrow> F \<unlhd> H \<Longrightarrow> graph F f \<subseteq> graph H h

         \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x \<Longrightarrow> C) \<Longrightarrow> C"

   unfolding norm_pres_extensions_def by blast

 lemma norm_pres_extensionI2 [intro]:

   "linearform H h \<Longrightarrow> H \<unlhd> E \<Longrightarrow> F \<unlhd> H

     \<Longrightarrow> graph F f \<subseteq> graph H h \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x

     \<Longrightarrow> graph H h \<in> norm_pres_extensions E p F f"

   unfolding norm_pres_extensions_def by blast

 lemma norm_pres_extensionI:  (* FIXME ? *)

   "\<exists>H h. g = graph H h

     \<and> linearform H h

     \<and> H \<unlhd> E

     \<and> F \<unlhd> H

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

     \<and> (\<forall>x \<in> H. h x \<le> p x) \<Longrightarrow> g \<in> norm_pres_extensions E p F f"

   unfolding norm_pres_extensions_def by blast

 end