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