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';
tuned comments;
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 \<open>An order on functions\<close>
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 \<open>The graph of a function\<close>
wenzelm@7808
    12
wenzelm@58744
    13
text \<open>
wenzelm@61879
    14
  We define the \<^emph>\<open>graph\<close> of a (real) function \<open>f\<close> with domain \<open>F\<close> as the set
wenzelm@10687
    15
  \begin{center}
wenzelm@61539
    16
  \<open>{(x, f x). x \<in> F}\<close>
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
\<close>
wenzelm@7535
    21
wenzelm@41818
    22
type_synonym 'a graph = "('a \<times> real) set"
wenzelm@7535
    23
wenzelm@44887
    24
definition graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph"
wenzelm@44887
    25
  where "graph F f = {(x, f x) | x. x \<in> F}"
wenzelm@7535
    26
wenzelm@13515
    27
lemma graphI [intro]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f"
wenzelm@27612
    28
  unfolding graph_def by blast
wenzelm@7535
    29
wenzelm@13515
    30
lemma graphI2 [intro?]: "x \<in> F \<Longrightarrow> \<exists>t \<in> 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) \<in> graph F f"
wenzelm@44887
    35
  obtains "x \<in> 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 \<open>Functions ordered by domain extension\<close>
wenzelm@7917
    40
wenzelm@58744
    41
text \<open>
wenzelm@61879
    42
  A function \<open>h'\<close> is an extension of \<open>h\<close>, iff the graph of \<open>h\<close> is a subset of
wenzelm@61879
    43
  the graph of \<open>h'\<close>.
wenzelm@58744
    44
\<close>
wenzelm@7917
    45
wenzelm@10687
    46
lemma graph_extI:
wenzelm@10687
    47
  "(\<And>x. x \<in> H \<Longrightarrow> h x = h' x) \<Longrightarrow> H \<subseteq> H'
wenzelm@13515
    48
    \<Longrightarrow> graph H h \<subseteq> graph H' h'"
wenzelm@27612
    49
  unfolding graph_def by blast
wenzelm@7917
    50
wenzelm@44887
    51
lemma graph_extD1 [dest?]: "graph H h \<subseteq> graph H' h' \<Longrightarrow> x \<in> H \<Longrightarrow> 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 \<subseteq> graph H' h' \<Longrightarrow> H \<subseteq> H'"
wenzelm@27612
    55
  unfolding graph_def by blast
wenzelm@7566
    56
wenzelm@13515
    57
wenzelm@58744
    58
subsection \<open>Domain and function of a graph\<close>
wenzelm@7917
    59
wenzelm@58744
    60
text \<open>
wenzelm@61539
    61
  The inverse functions to \<open>graph\<close> are \<open>domain\<close> and \<open>funct\<close>.
wenzelm@58744
    62
\<close>
wenzelm@7917
    63
wenzelm@44887
    64
definition domain :: "'a graph \<Rightarrow> 'a set"
wenzelm@44887
    65
  where "domain g = {x. \<exists>y. (x, y) \<in> g}"
wenzelm@7917
    66
wenzelm@44887
    67
definition funct :: "'a graph \<Rightarrow> ('a \<Rightarrow> real)"
wenzelm@44887
    68
  where "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))"
wenzelm@7917
    69
wenzelm@58744
    70
text \<open>
wenzelm@61540
    71
  The following lemma states that \<open>g\<close> is the graph of a function if the
wenzelm@61540
    72
  relation induced by \<open>g\<close> is unique.
wenzelm@58744
    73
\<close>
wenzelm@7566
    74
wenzelm@10687
    75
lemma graph_domain_funct:
wenzelm@13515
    76
  assumes uniq: "\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> 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) \<in> g"
wenzelm@23378
    81
  from g show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2)
wenzelm@23378
    82
  from g show "\<exists>y. (a, y) \<in> g" ..
wenzelm@23378
    83
  from g show "b = (SOME y. (a, y) \<in> g)"
paulson@9969
    84
  proof (rule some_equality [symmetric])
wenzelm@13515
    85
    fix y assume "(a, y) \<in> 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 \<open>Norm-preserving extensions of a function\<close>
wenzelm@7917
    92
wenzelm@58744
    93
text \<open>
wenzelm@61879
    94
  Given a linear form \<open>f\<close> on the space \<open>F\<close> and a seminorm \<open>p\<close> on \<open>E\<close>. The set
wenzelm@61879
    95
  of all linear extensions of \<open>f\<close>, to superspaces \<open>H\<close> of \<open>F\<close>, which are
wenzelm@61540
    96
  bounded by \<open>p\<close>, is defined as follows.
wenzelm@58744
    97
\<close>
wenzelm@7808
    98
wenzelm@19736
    99
definition
wenzelm@10687
   100
  norm_pres_extensions ::
wenzelm@58745
   101
    "'a::{plus,minus,uminus,zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
wenzelm@44887
   102
      \<Rightarrow> 'a graph set"
wenzelm@44887
   103
where
wenzelm@44887
   104
  "norm_pres_extensions E p F f
wenzelm@44887
   105
    = {g. \<exists>H h. g = graph H h
wenzelm@44887
   106
        \<and> linearform H h
wenzelm@44887
   107
        \<and> H \<unlhd> E
wenzelm@44887
   108
        \<and> F \<unlhd> H
wenzelm@44887
   109
        \<and> graph F f \<subseteq> graph H h
wenzelm@44887
   110
        \<and> (\<forall>x \<in> H. h x \<le> p x)}"
wenzelm@10687
   111
wenzelm@13515
   112
lemma norm_pres_extensionE [elim]:
wenzelm@44887
   113
  assumes "g \<in> 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 \<unlhd> E"
wenzelm@44887
   118
    and "F \<unlhd> H"
wenzelm@44887
   119
    and "graph F f \<subseteq> graph H h"
wenzelm@44887
   120
    and "\<forall>x \<in> H. h x \<le> 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 \<Longrightarrow> H \<unlhd> E \<Longrightarrow> F \<unlhd> H
wenzelm@13515
   125
    \<Longrightarrow> graph F f \<subseteq> graph H h \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x
wenzelm@13515
   126
    \<Longrightarrow> graph H h \<in> 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
  "\<exists>H h. g = graph H h
wenzelm@13515
   131
    \<and> linearform H h
wenzelm@13515
   132
    \<and> H \<unlhd> E
wenzelm@13515
   133
    \<and> F \<unlhd> H
wenzelm@13515
   134
    \<and> graph F f \<subseteq> graph H h
wenzelm@13515
   135
    \<and> (\<forall>x \<in> H. h x \<le> p x) \<Longrightarrow> g \<in> norm_pres_extensions E p F f"
wenzelm@27612
   136
  unfolding norm_pres_extensions_def by blast
wenzelm@7535
   137
wenzelm@10687
   138
end