src/HOL/Hahn_Banach/Function_Order.thy
 author haftmann Fri Nov 01 18:51:14 2013 +0100 (2013-11-01) changeset 54230 b1d955791529 parent 44887 7ca82df6e951 child 58744 c434e37f290e permissions -rw-r--r--
more simplification rules on unary and binary minus
     1 (*  Title:      HOL/Hahn_Banach/Function_Order.thy

     2     Author:     Gertrud Bauer, TU Munich

     3 *)

     4

     5 header {* An order on functions *}

     6

     7 theory Function_Order

     8 imports Subspace Linearform

     9 begin

    10

    11 subsection {* The graph of a function *}

    12

    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.

    22 *}

    23

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

    25

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

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

    28

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

    30   unfolding graph_def by blast

    31

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

    33   unfolding graph_def by blast

    34

    35 lemma graphE [elim?]:

    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

    39

    40

    41 subsection {* Functions ordered by domain extension *}

    42

    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 *}

    47

    48 lemma graph_extI:

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

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

    51   unfolding graph_def by blast

    52

    53 lemma graph_extD1 [dest?]: "graph H h \<subseteq> graph H' h' \<Longrightarrow> x \<in> H \<Longrightarrow> h x = h' x"

    54   unfolding graph_def by blast

    55

    56 lemma graph_extD2 [dest?]: "graph H h \<subseteq> graph H' h' \<Longrightarrow> H \<subseteq> H'"

    57   unfolding graph_def by blast

    58

    59

    60 subsection {* Domain and function of a graph *}

    61

    62 text {*

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

    64   funct}.

    65 *}

    66

    67 definition domain :: "'a graph \<Rightarrow> 'a set"

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

    69

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

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

    72

    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 *}

    77

    78 lemma graph_domain_funct:

    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"

    81   unfolding domain_def funct_def graph_def

    82 proof auto  (* FIXME !? *)

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

    87   proof (rule some_equality [symmetric])

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

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

    90   qed

    91 qed

    92

    93

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

    95

    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 *}

   102

   103 definition

   104   norm_pres_extensions ::

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

   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)}"

   115

   116 lemma norm_pres_extensionE [elim]:

   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

   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