src/HOL/Hahn_Banach/Function_Order.thy
author blanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58306 117ba6cbe414
parent 44887 7ca82df6e951
child 58744 c434e37f290e
permissions -rw-r--r--
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
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@9035
     5
header {* An order on functions *}
wenzelm@7808
     6
wenzelm@31795
     7
theory Function_Order
wenzelm@27612
     8
imports Subspace Linearform
wenzelm@27612
     9
begin
wenzelm@7535
    10
wenzelm@9035
    11
subsection {* The graph of a function *}
wenzelm@7808
    12
wenzelm@10687
    13
text {*
wenzelm@10687
    14
  We define the \emph{graph} of a (real) function @{text f} with
wenzelm@10687
    15
  domain @{text F} as the set
wenzelm@10687
    16
  \begin{center}
wenzelm@10687
    17
  @{text "{(x, f x). x \<in> F}"}
wenzelm@10687
    18
  \end{center}
wenzelm@10687
    19
  So we are modeling partial functions by specifying the domain and
wenzelm@10687
    20
  the mapping function. We use the term ``function'' also for its
wenzelm@10687
    21
  graph.
wenzelm@9035
    22
*}
wenzelm@7535
    23
wenzelm@41818
    24
type_synonym 'a graph = "('a \<times> real) set"
wenzelm@7535
    25
wenzelm@44887
    26
definition graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph"
wenzelm@44887
    27
  where "graph F f = {(x, f x) | x. x \<in> F}"
wenzelm@7535
    28
wenzelm@13515
    29
lemma graphI [intro]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f"
wenzelm@27612
    30
  unfolding graph_def by blast
wenzelm@7535
    31
wenzelm@13515
    32
lemma graphI2 [intro?]: "x \<in> F \<Longrightarrow> \<exists>t \<in> graph F f. t = (x, f x)"
wenzelm@27612
    33
  unfolding graph_def by blast
wenzelm@7566
    34
wenzelm@13515
    35
lemma graphE [elim?]:
wenzelm@44887
    36
  assumes "(x, y) \<in> graph F f"
wenzelm@44887
    37
  obtains "x \<in> F" and "y = f x"
wenzelm@44887
    38
  using assms unfolding graph_def by blast
wenzelm@10687
    39
wenzelm@7535
    40
wenzelm@9035
    41
subsection {* Functions ordered by domain extension *}
wenzelm@7917
    42
wenzelm@13515
    43
text {*
wenzelm@13515
    44
  A function @{text h'} is an extension of @{text h}, iff the graph of
wenzelm@13515
    45
  @{text h} is a subset of the graph of @{text h'}.
wenzelm@13515
    46
*}
wenzelm@7917
    47
wenzelm@10687
    48
lemma graph_extI:
wenzelm@10687
    49
  "(\<And>x. x \<in> H \<Longrightarrow> h x = h' x) \<Longrightarrow> H \<subseteq> H'
wenzelm@13515
    50
    \<Longrightarrow> graph H h \<subseteq> graph H' h'"
wenzelm@27612
    51
  unfolding graph_def by blast
wenzelm@7917
    52
wenzelm@44887
    53
lemma graph_extD1 [dest?]: "graph H h \<subseteq> graph H' h' \<Longrightarrow> x \<in> H \<Longrightarrow> h x = h' x"
wenzelm@27612
    54
  unfolding graph_def by blast
wenzelm@7566
    55
wenzelm@44887
    56
lemma graph_extD2 [dest?]: "graph H h \<subseteq> graph H' h' \<Longrightarrow> H \<subseteq> H'"
wenzelm@27612
    57
  unfolding graph_def by blast
wenzelm@7566
    58
wenzelm@13515
    59
wenzelm@9035
    60
subsection {* Domain and function of a graph *}
wenzelm@7917
    61
wenzelm@10687
    62
text {*
wenzelm@13515
    63
  The inverse functions to @{text graph} are @{text domain} and @{text
wenzelm@13515
    64
  funct}.
wenzelm@10687
    65
*}
wenzelm@7917
    66
wenzelm@44887
    67
definition domain :: "'a graph \<Rightarrow> 'a set"
wenzelm@44887
    68
  where "domain g = {x. \<exists>y. (x, y) \<in> g}"
wenzelm@7917
    69
wenzelm@44887
    70
definition funct :: "'a graph \<Rightarrow> ('a \<Rightarrow> real)"
wenzelm@44887
    71
  where "funct g = (\<lambda>x. (SOME y. (x, y) \<in> g))"
wenzelm@7917
    72
wenzelm@10687
    73
text {*
wenzelm@10687
    74
  The following lemma states that @{text g} is the graph of a function
wenzelm@10687
    75
  if the relation induced by @{text g} is unique.
wenzelm@10687
    76
*}
wenzelm@7566
    77
wenzelm@10687
    78
lemma graph_domain_funct:
wenzelm@13515
    79
  assumes uniq: "\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y"
wenzelm@13515
    80
  shows "graph (domain g) (funct g) = g"
wenzelm@27612
    81
  unfolding domain_def funct_def graph_def
wenzelm@27612
    82
proof auto  (* FIXME !? *)
wenzelm@23378
    83
  fix a b assume g: "(a, b) \<in> g"
wenzelm@23378
    84
  from g show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2)
wenzelm@23378
    85
  from g show "\<exists>y. (a, y) \<in> g" ..
wenzelm@23378
    86
  from g show "b = (SOME y. (a, y) \<in> g)"
paulson@9969
    87
  proof (rule some_equality [symmetric])
wenzelm@13515
    88
    fix y assume "(a, y) \<in> g"
wenzelm@23378
    89
    with g show "y = b" by (rule uniq)
wenzelm@9035
    90
  qed
wenzelm@9035
    91
qed
wenzelm@7535
    92
wenzelm@7808
    93
wenzelm@9035
    94
subsection {* Norm-preserving extensions of a function *}
wenzelm@7917
    95
wenzelm@10687
    96
text {*
wenzelm@10687
    97
  Given a linear form @{text f} on the space @{text F} and a seminorm
wenzelm@10687
    98
  @{text p} on @{text E}. The set of all linear extensions of @{text
wenzelm@10687
    99
  f}, to superspaces @{text H} of @{text F}, which are bounded by
wenzelm@10687
   100
  @{text p}, is defined as follows.
wenzelm@10687
   101
*}
wenzelm@7808
   102
wenzelm@19736
   103
definition
wenzelm@10687
   104
  norm_pres_extensions ::
haftmann@25762
   105
    "'a::{plus, minus, uminus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real)
wenzelm@44887
   106
      \<Rightarrow> 'a graph set"
wenzelm@44887
   107
where
wenzelm@44887
   108
  "norm_pres_extensions E p F f
wenzelm@44887
   109
    = {g. \<exists>H h. g = graph H h
wenzelm@44887
   110
        \<and> linearform H h
wenzelm@44887
   111
        \<and> H \<unlhd> E
wenzelm@44887
   112
        \<and> F \<unlhd> H
wenzelm@44887
   113
        \<and> graph F f \<subseteq> graph H h
wenzelm@44887
   114
        \<and> (\<forall>x \<in> H. h x \<le> p x)}"
wenzelm@10687
   115
wenzelm@13515
   116
lemma norm_pres_extensionE [elim]:
wenzelm@44887
   117
  assumes "g \<in> norm_pres_extensions E p F f"
wenzelm@44887
   118
  obtains H h
wenzelm@44887
   119
    where "g = graph H h"
wenzelm@44887
   120
    and "linearform H h"
wenzelm@44887
   121
    and "H \<unlhd> E"
wenzelm@44887
   122
    and "F \<unlhd> H"
wenzelm@44887
   123
    and "graph F f \<subseteq> graph H h"
wenzelm@44887
   124
    and "\<forall>x \<in> H. h x \<le> p x"
wenzelm@44887
   125
  using assms unfolding norm_pres_extensions_def by blast
wenzelm@7535
   126
wenzelm@10687
   127
lemma norm_pres_extensionI2 [intro]:
wenzelm@13515
   128
  "linearform H h \<Longrightarrow> H \<unlhd> E \<Longrightarrow> F \<unlhd> H
wenzelm@13515
   129
    \<Longrightarrow> graph F f \<subseteq> graph H h \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x
wenzelm@13515
   130
    \<Longrightarrow> graph H h \<in> norm_pres_extensions E p F f"
wenzelm@27612
   131
  unfolding norm_pres_extensions_def by blast
wenzelm@7535
   132
wenzelm@13515
   133
lemma norm_pres_extensionI:  (* FIXME ? *)
wenzelm@13515
   134
  "\<exists>H h. g = graph H h
wenzelm@13515
   135
    \<and> linearform H h
wenzelm@13515
   136
    \<and> H \<unlhd> E
wenzelm@13515
   137
    \<and> F \<unlhd> H
wenzelm@13515
   138
    \<and> graph F f \<subseteq> graph H h
wenzelm@13515
   139
    \<and> (\<forall>x \<in> H. h x \<le> p x) \<Longrightarrow> g \<in> norm_pres_extensions E p F f"
wenzelm@27612
   140
  unfolding norm_pres_extensions_def by blast
wenzelm@7535
   141
wenzelm@10687
   142
end