src/HOL/Real/HahnBanach/FunctionOrder.thy
author wenzelm
Sun Jul 23 12:01:05 2000 +0200 (2000-07-23)
changeset 9408 d3d56e1d2ec1
parent 9379 21cfeae6659d
child 9503 3324cbbecef8
permissions -rw-r--r--
classical atts now intro! / intro / intro?;
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@7978
    12
text{* We define the \emph{graph} of a (real) function $f$ with
wenzelm@7917
    13
domain $F$ as the set 
wenzelm@7927
    14
\[
bauerg@9374
    15
\{(x, f\ap x). \ap x \in F\}
wenzelm@7927
    16
\]
wenzelm@7978
    17
So we are modeling partial functions by specifying the domain and 
wenzelm@7978
    18
the mapping function. We use the term ``function'' also for its graph.
wenzelm@9035
    19
*}
wenzelm@7535
    20
wenzelm@9035
    21
types 'a graph = "('a * real) set"
wenzelm@7535
    22
wenzelm@7535
    23
constdefs
wenzelm@7535
    24
  graph :: "['a set, 'a => real] => 'a graph "
bauerg@9379
    25
  "graph F f == {(x, f x) | x. x \\<in> F}" 
wenzelm@7535
    26
wenzelm@9408
    27
lemma graphI [intro?]: "x \\<in> F ==> (x, f x) \\<in> graph F f"
wenzelm@9035
    28
  by (unfold graph_def, intro CollectI exI) force
wenzelm@7535
    29
wenzelm@9408
    30
lemma graphI2 [intro?]: "x \\<in> F ==> \\<exists>t\\<in> (graph F f). t = (x, f x)"
wenzelm@9035
    31
  by (unfold graph_def, force)
wenzelm@7566
    32
wenzelm@9408
    33
lemma graphD1 [intro?]: "(x, y) \\<in> graph F f ==> x \\<in> F"
wenzelm@9035
    34
  by (unfold graph_def, elim CollectE exE) force
wenzelm@7566
    35
wenzelm@9408
    36
lemma graphD2 [intro?]: "(x, y) \\<in> graph H h ==> y = h x"
wenzelm@9035
    37
  by (unfold graph_def, elim CollectE exE) force 
wenzelm@7535
    38
wenzelm@9035
    39
subsection {* Functions ordered by domain extension *}
wenzelm@7917
    40
wenzelm@7978
    41
text{* A function $h'$ is an extension of $h$, iff the graph of 
wenzelm@9035
    42
$h$ is a subset of the graph of $h'$.*}
wenzelm@7917
    43
wenzelm@7917
    44
lemma graph_extI: 
bauerg@9379
    45
  "[| !! x. x \\<in> H ==> h x = h' x; H <= H'|]
wenzelm@9035
    46
  ==> graph H h <= graph H' h'"
wenzelm@9035
    47
  by (unfold graph_def, force)
wenzelm@7917
    48
wenzelm@9408
    49
lemma graph_extD1 [intro?]: 
bauerg@9379
    50
  "[| graph H h <= graph H' h'; x \\<in> H |] ==> h x = h' x"
wenzelm@9035
    51
  by (unfold graph_def, force)
wenzelm@7566
    52
wenzelm@9408
    53
lemma graph_extD2 [intro?]: 
wenzelm@9035
    54
  "[| graph H h <= graph H' h' |] ==> H <= H'"
wenzelm@9035
    55
  by (unfold graph_def, force)
wenzelm@7566
    56
wenzelm@9035
    57
subsection {* Domain and function of a graph *}
wenzelm@7917
    58
wenzelm@7917
    59
text{* The inverse functions to $\idt{graph}$ are $\idt{domain}$ and 
wenzelm@9035
    60
$\idt{funct}$.*}
wenzelm@7917
    61
wenzelm@7917
    62
constdefs
wenzelm@7917
    63
  domain :: "'a graph => 'a set" 
bauerg@9379
    64
  "domain g == {x. \\<exists>y. (x, y) \\<in> g}"
wenzelm@7917
    65
wenzelm@7917
    66
  funct :: "'a graph => ('a => real)"
bauerg@9379
    67
  "funct g == \\<lambda>x. (SOME y. (x, y) \\<in> g)"
wenzelm@7917
    68
wenzelm@7917
    69
wenzelm@7917
    70
text {* The following lemma states that $g$ is the graph of a function
wenzelm@9035
    71
if the relation induced by $g$ is unique. *}
wenzelm@7566
    72
wenzelm@7566
    73
lemma graph_domain_funct: 
bauerg@9379
    74
  "(!!x y z. (x, y) \\<in> g ==> (x, z) \\<in> g ==> z = y) 
wenzelm@9035
    75
  ==> graph (domain g) (funct g) = g"
wenzelm@9035
    76
proof (unfold domain_def funct_def graph_def, auto)
bauerg@9379
    77
  fix a b assume "(a, b) \\<in> g"
bauerg@9379
    78
  show "(a, SOME y. (a, y) \\<in> g) \\<in> g" by (rule selectI2)
bauerg@9379
    79
  show "\\<exists>y. (a, y) \\<in> g" ..
bauerg@9379
    80
  assume uniq: "!!x y z. (x, y) \\<in> g ==> (x, z) \\<in> g ==> z = y"
bauerg@9379
    81
  show "b = (SOME y. (a, y) \\<in> g)"
wenzelm@9035
    82
  proof (rule select_equality [RS sym])
bauerg@9379
    83
    fix y assume "(a, y) \\<in> g" show "y = b" by (rule uniq)
wenzelm@9035
    84
  qed
wenzelm@9035
    85
qed
wenzelm@7535
    86
wenzelm@7808
    87
wenzelm@7808
    88
wenzelm@9035
    89
subsection {* Norm-preserving extensions of a function *}
wenzelm@7917
    90
wenzelm@7978
    91
text {* Given a linear form $f$ on the space $F$ and a seminorm $p$ on 
wenzelm@7917
    92
$E$. The set of all linear extensions of $f$, to superspaces $H$ of 
wenzelm@9035
    93
$F$, which are bounded by $p$, is defined as follows. *}
wenzelm@7808
    94
wenzelm@7808
    95
wenzelm@7535
    96
constdefs
wenzelm@7656
    97
  norm_pres_extensions :: 
bauerg@9374
    98
    "['a::{plus, minus, zero} set, 'a  => real, 'a set, 'a => real] 
wenzelm@7917
    99
    => 'a graph set"
wenzelm@7917
   100
    "norm_pres_extensions E p F f 
bauerg@9379
   101
    == {g. \\<exists>H h. graph H h = g 
bauerg@9379
   102
                \\<and> is_linearform H h 
bauerg@9379
   103
                \\<and> is_subspace H E
bauerg@9379
   104
                \\<and> is_subspace F H
bauerg@9379
   105
                \\<and> graph F f <= graph H h
bauerg@9379
   106
                \\<and> (\\<forall>x \\<in> H. h x <= p x)}"
wenzelm@7535
   107
                       
wenzelm@7656
   108
lemma norm_pres_extension_D:  
bauerg@9379
   109
  "g \\<in> norm_pres_extensions E p F f
bauerg@9379
   110
  ==> \\<exists>H h. graph H h = g 
bauerg@9379
   111
            \\<and> is_linearform H h 
bauerg@9379
   112
            \\<and> is_subspace H E
bauerg@9379
   113
            \\<and> is_subspace F H
bauerg@9379
   114
            \\<and> graph F f <= graph H h
bauerg@9379
   115
            \\<and> (\\<forall>x \\<in> H. h x <= p x)"
wenzelm@9035
   116
  by (unfold norm_pres_extensions_def) force
wenzelm@7535
   117
wenzelm@7656
   118
lemma norm_pres_extensionI2 [intro]:  
wenzelm@7917
   119
  "[| is_linearform H h; is_subspace H E; is_subspace F H;
bauerg@9379
   120
  graph F f <= graph H h; \\<forall>x \\<in> H. h x <= p x |]
bauerg@9379
   121
  ==> (graph H h \\<in> norm_pres_extensions E p F f)"
wenzelm@9035
   122
 by (unfold norm_pres_extensions_def) force
wenzelm@7535
   123
wenzelm@7656
   124
lemma norm_pres_extensionI [intro]:  
bauerg@9379
   125
  "\\<exists>H h. graph H h = g 
bauerg@9379
   126
         \\<and> is_linearform H h    
bauerg@9379
   127
         \\<and> is_subspace H E
bauerg@9379
   128
         \\<and> is_subspace F H
bauerg@9379
   129
         \\<and> graph F f <= graph H h
bauerg@9379
   130
         \\<and> (\\<forall>x \\<in> H. h x <= p x)
bauerg@9379
   131
  ==> g \\<in> norm_pres_extensions E p F f"
wenzelm@9035
   132
  by (unfold norm_pres_extensions_def) force
wenzelm@7535
   133
wenzelm@9035
   134
end