src/HOL/Real/HahnBanach/FunctionOrder.thy
author wenzelm
Sat Dec 16 21:41:51 2000 +0100 (2000-12-16)
changeset 10687 c186279eecea
parent 9969 4753185f1dd2
child 11472 d08d4e17a5f6
permissions -rw-r--r--
tuned HOL/Real/HahnBanach;
     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 = Subspace + Linearform:
     9 
    10 subsection {* The graph of a function *}
    11 
    12 text {*
    13   We define the \emph{graph} of a (real) function @{text f} with
    14   domain @{text F} as the set
    15   \begin{center}
    16   @{text "{(x, f x). x \<in> F}"}
    17   \end{center}
    18   So we are modeling partial functions by specifying the domain and
    19   the mapping function. We use the term ``function'' also for its
    20   graph.
    21 *}
    22 
    23 types 'a graph = "('a * real) set"
    24 
    25 constdefs
    26   graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph "
    27   "graph F f \<equiv> {(x, f x) | x. x \<in> F}"
    28 
    29 lemma graphI [intro?]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f"
    30   by (unfold graph_def, intro CollectI exI) blast
    31 
    32 lemma graphI2 [intro?]: "x \<in> F \<Longrightarrow> \<exists>t\<in> (graph F f). t = (x, f x)"
    33   by (unfold graph_def) blast
    34 
    35 lemma graphD1 [intro?]: "(x, y) \<in> graph F f \<Longrightarrow> x \<in> F"
    36   by (unfold graph_def) blast
    37 
    38 lemma graphD2 [intro?]: "(x, y) \<in> graph H h \<Longrightarrow> y = h x"
    39   by (unfold graph_def) blast
    40 
    41 
    42 subsection {* Functions ordered by domain extension *}
    43 
    44 text {* A function @{text h'} is an extension of @{text h}, iff the
    45   graph of @{text h} is a subset of the graph of @{text h'}. *}
    46 
    47 lemma graph_extI:
    48   "(\<And>x. x \<in> H \<Longrightarrow> h x = h' x) \<Longrightarrow> H \<subseteq> H'
    49   \<Longrightarrow> graph H h \<subseteq> graph H' h'"
    50   by (unfold graph_def) blast
    51 
    52 lemma graph_extD1 [intro?]:
    53   "graph H h \<subseteq> graph H' h' \<Longrightarrow> x \<in> H \<Longrightarrow> h x = h' x"
    54   by (unfold graph_def) blast
    55 
    56 lemma graph_extD2 [intro?]:
    57   "graph H h \<subseteq> graph H' h' \<Longrightarrow> H \<subseteq> H'"
    58   by (unfold graph_def) blast
    59 
    60 subsection {* Domain and function of a graph *}
    61 
    62 text {*
    63   The inverse functions to @{text graph} are @{text domain} and
    64   @{text funct}.
    65 *}
    66 
    67 constdefs
    68   domain :: "'a graph \<Rightarrow> 'a set"
    69   "domain g \<equiv> {x. \<exists>y. (x, y) \<in> g}"
    70 
    71   funct :: "'a graph \<Rightarrow> ('a \<Rightarrow> real)"
    72   "funct g \<equiv> \<lambda>x. (SOME y. (x, y) \<in> g)"
    73 
    74 
    75 text {*
    76   The following lemma states that @{text g} is the graph of a function
    77   if the relation induced by @{text g} is unique.
    78 *}
    79 
    80 lemma graph_domain_funct:
    81   "(\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y)
    82   \<Longrightarrow> graph (domain g) (funct g) = g"
    83 proof (unfold domain_def funct_def graph_def, auto)
    84   fix a b assume "(a, b) \<in> g"
    85   show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2)
    86   show "\<exists>y. (a, y) \<in> g" ..
    87   assume uniq: "\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y"
    88   show "b = (SOME y. (a, y) \<in> g)"
    89   proof (rule some_equality [symmetric])
    90     fix y assume "(a, y) \<in> g" show "y = b" by (rule uniq)
    91   qed
    92 qed
    93 
    94 
    95 
    96 subsection {* Norm-preserving extensions of a function *}
    97 
    98 text {*
    99   Given a linear form @{text f} on the space @{text F} and a seminorm
   100   @{text p} on @{text E}. The set of all linear extensions of @{text
   101   f}, to superspaces @{text H} of @{text F}, which are bounded by
   102   @{text p}, is defined as follows.
   103 *}
   104 
   105 constdefs
   106   norm_pres_extensions ::
   107     "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
   108     \<Rightarrow> 'a graph set"
   109     "norm_pres_extensions E p F f
   110     \<equiv> {g. \<exists>H h. graph H h = g
   111                 \<and> is_linearform H h
   112                 \<and> is_subspace H E
   113                 \<and> is_subspace F H
   114                 \<and> graph F f \<subseteq> graph H h
   115                 \<and> (\<forall>x \<in> H. h x \<le> p x)}"
   116 
   117 lemma norm_pres_extension_D:
   118   "g \<in> norm_pres_extensions E p F f
   119   \<Longrightarrow> \<exists>H h. graph H h = g
   120             \<and> is_linearform H h
   121             \<and> is_subspace H E
   122             \<and> is_subspace F H
   123             \<and> graph F f \<subseteq> graph H h
   124             \<and> (\<forall>x \<in> H. h x \<le> p x)"
   125   by (unfold norm_pres_extensions_def) blast
   126 
   127 lemma norm_pres_extensionI2 [intro]:
   128   "is_linearform H h \<Longrightarrow> is_subspace H E \<Longrightarrow> is_subspace F H \<Longrightarrow>
   129   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  by (unfold norm_pres_extensions_def) blast
   132 
   133 lemma norm_pres_extensionI [intro]:
   134   "\<exists>H h. graph H h = g
   135          \<and> is_linearform H h
   136          \<and> is_subspace H E
   137          \<and> is_subspace F H
   138          \<and> graph F f \<subseteq> graph H h
   139          \<and> (\<forall>x \<in> H. h x \<le> p x)
   140   \<Longrightarrow> g \<in> norm_pres_extensions E p F f"
   141   by (unfold norm_pres_extensions_def) blast
   142 
   143 end