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