src/HOL/Real/HahnBanach/FunctionOrder.thy
author wenzelm
Tue Jul 15 19:39:37 2008 +0200 (2008-07-15)
changeset 27612 d3eb431db035
parent 25762 c03e9d04b3e4
permissions -rw-r--r--
modernized specifications and proofs;
tuned document;
     1 (*  Title:      HOL/Real/HahnBanach/FunctionOrder.thy
     2     ID:         $Id$
     3     Author:     Gertrud Bauer, TU Munich
     4 *)
     5 
     6 header {* An order on functions *}
     7 
     8 theory FunctionOrder
     9 imports Subspace Linearform
    10 begin
    11 
    12 subsection {* The graph of a function *}
    13 
    14 text {*
    15   We define the \emph{graph} of a (real) function @{text f} with
    16   domain @{text F} as the set
    17   \begin{center}
    18   @{text "{(x, f x). x \<in> F}"}
    19   \end{center}
    20   So we are modeling partial functions by specifying the domain and
    21   the mapping function. We use the term ``function'' also for its
    22   graph.
    23 *}
    24 
    25 types 'a graph = "('a \<times> real) set"
    26 
    27 definition
    28   graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph" where
    29   "graph F f = {(x, f x) | x. x \<in> F}"
    30 
    31 lemma graphI [intro]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f"
    32   unfolding graph_def by blast
    33 
    34 lemma graphI2 [intro?]: "x \<in> F \<Longrightarrow> \<exists>t \<in> graph F f. t = (x, f x)"
    35   unfolding graph_def by blast
    36 
    37 lemma graphE [elim?]:
    38     "(x, y) \<in> graph F f \<Longrightarrow> (x \<in> F \<Longrightarrow> y = f x \<Longrightarrow> C) \<Longrightarrow> C"
    39   unfolding graph_def by blast
    40 
    41 
    42 subsection {* Functions ordered by domain extension *}
    43 
    44 text {*
    45   A function @{text h'} is an extension of @{text h}, iff the graph of
    46   @{text h} is a subset of the graph of @{text h'}.
    47 *}
    48 
    49 lemma graph_extI:
    50   "(\<And>x. x \<in> H \<Longrightarrow> h x = h' x) \<Longrightarrow> H \<subseteq> H'
    51     \<Longrightarrow> graph H h \<subseteq> graph H' h'"
    52   unfolding graph_def by blast
    53 
    54 lemma graph_extD1 [dest?]:
    55   "graph H h \<subseteq> graph H' h' \<Longrightarrow> x \<in> H \<Longrightarrow> h x = h' x"
    56   unfolding graph_def by blast
    57 
    58 lemma graph_extD2 [dest?]:
    59   "graph H h \<subseteq> graph H' h' \<Longrightarrow> H \<subseteq> H'"
    60   unfolding graph_def by blast
    61 
    62 
    63 subsection {* Domain and function of a graph *}
    64 
    65 text {*
    66   The inverse functions to @{text graph} are @{text domain} and @{text
    67   funct}.
    68 *}
    69 
    70 definition
    71   "domain" :: "'a graph \<Rightarrow> 'a set" where
    72   "domain g = {x. \<exists>y. (x, y) \<in> g}"
    73 
    74 definition
    75   funct :: "'a graph \<Rightarrow> ('a \<Rightarrow> real)" where
    76   "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))"
    77 
    78 text {*
    79   The following lemma states that @{text g} is the graph of a function
    80   if the relation induced by @{text g} is unique.
    81 *}
    82 
    83 lemma graph_domain_funct:
    84   assumes uniq: "\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y"
    85   shows "graph (domain g) (funct g) = g"
    86   unfolding domain_def funct_def graph_def
    87 proof auto  (* FIXME !? *)
    88   fix a b assume g: "(a, b) \<in> g"
    89   from g show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2)
    90   from g show "\<exists>y. (a, y) \<in> g" ..
    91   from g show "b = (SOME y. (a, y) \<in> g)"
    92   proof (rule some_equality [symmetric])
    93     fix y assume "(a, y) \<in> g"
    94     with g show "y = b" by (rule uniq)
    95   qed
    96 qed
    97 
    98 
    99 subsection {* Norm-preserving extensions of a function *}
   100 
   101 text {*
   102   Given a linear form @{text f} on the space @{text F} and a seminorm
   103   @{text p} on @{text E}. The set of all linear extensions of @{text
   104   f}, to superspaces @{text H} of @{text F}, which are bounded by
   105   @{text p}, is defined as follows.
   106 *}
   107 
   108 definition
   109   norm_pres_extensions ::
   110     "'a::{plus, minus, uminus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
   111       \<Rightarrow> 'a graph set" where
   112     "norm_pres_extensions E p F f
   113       = {g. \<exists>H h. g = graph H h
   114           \<and> linearform H h
   115           \<and> H \<unlhd> E
   116           \<and> F \<unlhd> H
   117           \<and> graph F f \<subseteq> graph H h
   118           \<and> (\<forall>x \<in> H. h x \<le> p x)}"
   119 
   120 lemma norm_pres_extensionE [elim]:
   121   "g \<in> norm_pres_extensions E p F f
   122   \<Longrightarrow> (\<And>H h. g = graph H h \<Longrightarrow> linearform H h
   123         \<Longrightarrow> H \<unlhd> E \<Longrightarrow> F \<unlhd> H \<Longrightarrow> graph F f \<subseteq> graph H h
   124         \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x \<Longrightarrow> C) \<Longrightarrow> C"
   125   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