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