src/HOL/Hahn_Banach/Function_Order.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 31795 be3e1cc5005c
child 41818 6d4c3ee8219d
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
     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 types 'a graph = "('a \<times> real) set"
    25 
    26 definition
    27   graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph" where
    28   "graph F f = {(x, f x) | x. x \<in> F}"
    29 
    30 lemma graphI [intro]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f"
    31   unfolding graph_def by blast
    32 
    33 lemma graphI2 [intro?]: "x \<in> F \<Longrightarrow> \<exists>t \<in> graph F f. t = (x, f x)"
    34   unfolding graph_def by blast
    35 
    36 lemma graphE [elim?]:
    37     "(x, y) \<in> graph F f \<Longrightarrow> (x \<in> F \<Longrightarrow> y = f x \<Longrightarrow> C) \<Longrightarrow> C"
    38   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?]:
    54   "graph H h \<subseteq> graph H' h' \<Longrightarrow> x \<in> H \<Longrightarrow> h x = h' x"
    55   unfolding graph_def by blast
    56 
    57 lemma graph_extD2 [dest?]:
    58   "graph H h \<subseteq> graph H' h' \<Longrightarrow> H \<subseteq> H'"
    59   unfolding graph_def by blast
    60 
    61 
    62 subsection {* Domain and function of a graph *}
    63 
    64 text {*
    65   The inverse functions to @{text graph} are @{text domain} and @{text
    66   funct}.
    67 *}
    68 
    69 definition
    70   "domain" :: "'a graph \<Rightarrow> 'a set" where
    71   "domain g = {x. \<exists>y. (x, y) \<in> g}"
    72 
    73 definition
    74   funct :: "'a graph \<Rightarrow> ('a \<Rightarrow> real)" where
    75   "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))"
    76 
    77 text {*
    78   The following lemma states that @{text g} is the graph of a function
    79   if the relation induced by @{text g} is unique.
    80 *}
    81 
    82 lemma graph_domain_funct:
    83   assumes uniq: "\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y"
    84   shows "graph (domain g) (funct g) = g"
    85   unfolding domain_def funct_def graph_def
    86 proof auto  (* FIXME !? *)
    87   fix a b assume g: "(a, b) \<in> g"
    88   from g show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2)
    89   from g show "\<exists>y. (a, y) \<in> g" ..
    90   from g show "b = (SOME y. (a, y) \<in> g)"
    91   proof (rule some_equality [symmetric])
    92     fix y assume "(a, y) \<in> g"
    93     with g show "y = b" by (rule uniq)
    94   qed
    95 qed
    96 
    97 
    98 subsection {* Norm-preserving extensions of a function *}
    99 
   100 text {*
   101   Given a linear form @{text f} on the space @{text F} and a seminorm
   102   @{text p} on @{text E}. The set of all linear extensions of @{text
   103   f}, to superspaces @{text H} of @{text F}, which are bounded by
   104   @{text p}, is defined as follows.
   105 *}
   106 
   107 definition
   108   norm_pres_extensions ::
   109     "'a::{plus, minus, uminus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
   110       \<Rightarrow> 'a graph set" where
   111     "norm_pres_extensions E p F f
   112       = {g. \<exists>H h. g = graph H h
   113           \<and> linearform H h
   114           \<and> H \<unlhd> E
   115           \<and> F \<unlhd> H
   116           \<and> graph F f \<subseteq> graph H h
   117           \<and> (\<forall>x \<in> H. h x \<le> p x)}"
   118 
   119 lemma norm_pres_extensionE [elim]:
   120   "g \<in> norm_pres_extensions E p F f
   121   \<Longrightarrow> (\<And>H h. g = graph H h \<Longrightarrow> linearform H h
   122         \<Longrightarrow> H \<unlhd> E \<Longrightarrow> F \<unlhd> H \<Longrightarrow> graph F f \<subseteq> graph H h
   123         \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x \<Longrightarrow> C) \<Longrightarrow> C"
   124   unfolding norm_pres_extensions_def by blast
   125 
   126 lemma norm_pres_extensionI2 [intro]:
   127   "linearform H h \<Longrightarrow> H \<unlhd> E \<Longrightarrow> F \<unlhd> H
   128     \<Longrightarrow> graph F f \<subseteq> graph H h \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x
   129     \<Longrightarrow> graph H h \<in> norm_pres_extensions E p F f"
   130   unfolding norm_pres_extensions_def by blast
   131 
   132 lemma norm_pres_extensionI:  (* FIXME ? *)
   133   "\<exists>H h. g = graph H h
   134     \<and> linearform H h
   135     \<and> H \<unlhd> E
   136     \<and> F \<unlhd> H
   137     \<and> graph F f \<subseteq> graph H h
   138     \<and> (\<forall>x \<in> H. h x \<le> p x) \<Longrightarrow> g \<in> norm_pres_extensions E p F f"
   139   unfolding norm_pres_extensions_def by blast
   140 
   141 end