src/HOL/Real/HahnBanach/FunctionOrder.thy
author wenzelm
Fri Sep 10 17:28:51 1999 +0200 (1999-09-10)
changeset 7535 599d3414b51d
child 7566 c5a3f980a7af
permissions -rw-r--r--
The Hahn-Banach theorem for real vectorspaces (Isabelle/Isar)
(by Gertrud Bauer, TU Munich);
     1 
     2 theory FunctionOrder = Subspace + Linearform:;
     3 
     4 
     5 section {* Order on functions *};
     6 
     7 types 'a graph = "('a * real) set";
     8 
     9 constdefs
    10   graph :: "['a set, 'a => real] => 'a graph "
    11   "graph F f == {p. EX x. p = (x, f x) & x:F}"; (* == {(x, f x). x:F} *)
    12 
    13 constdefs
    14   domain :: "'a graph => 'a set" 
    15   "domain g == {x. EX y. (x, y):g}";
    16 
    17 constdefs
    18   funct :: "'a graph => ('a => real)"
    19   "funct g == %x. (@ y. (x, y):g)";
    20 
    21 lemma graph_I: "x:F ==> (x, f x) : graph F f";
    22   by (unfold graph_def, intro CollectI exI) force;
    23 
    24 lemma graphD1: "(x, y): graph F f ==> x:F";
    25   by (unfold graph_def, elim CollectD [elimify] exE) force;
    26 
    27 lemma graph_domain_funct: "(!!x y z. (x, y):g ==> (x, z):g ==> z = y) ==> graph (domain g) (funct g) = g";
    28 proof ( unfold domain_def, unfold funct_def, unfold graph_def, auto);
    29   fix a b; assume "(a, b) : g";
    30   show "(a, SOME y. (a, y) : g) : g"; by (rule selectI2);
    31   show "EX y. (a, y) : g"; ..;
    32   assume uniq: "!!x y z. (x, y):g ==> (x, z):g ==> z = y";
    33   show "b = (SOME y. (a, y) : g)";
    34   proof (rule select_equality [RS sym]);
    35     fix y; assume "(a, y):g"; show "y = b"; by (rule uniq);
    36   qed;
    37 qed;
    38 
    39 lemma graph_lemma1: "x:F ==> EX t: (graph F f). t = (x, f x)";
    40   by (unfold graph_def, force);
    41 
    42 lemma graph_lemma2: "(x, y): graph H h ==> y = h x";
    43   by (unfold graph_def, elim CollectD [elimify] exE) force; 
    44 
    45 lemma graph_lemma3: "[| graph H h <= graph H' h'; x:H |] ==> h x = h' x";
    46   by (unfold graph_def, force);
    47 
    48 lemma graph_lemma4: "[| graph H h <= graph H' h' |] ==> H <= H'";
    49   by (unfold graph_def, force);
    50 
    51 lemma graph_lemma5: "[| !! x. x: H ==> h x = h' x; H <= H'|] ==> graph H h <= graph H' h'";
    52   by (unfold graph_def, force);
    53 
    54 
    55 constdefs
    56   norm_prev_extensions :: 
    57    "['a set, 'a  => real, 'a set, 'a => real] => 'a graph set"
    58   "norm_prev_extensions E p F f == {g. EX H h. graph H h = g 
    59                                              & is_linearform H h 
    60                                              & is_subspace H E
    61                                              & is_subspace F H
    62                                              & (graph F f <= graph H h)
    63                                              & (ALL x:H. h x <= p x)}";
    64                        
    65 lemma norm_prev_extension_D:  
    66   "(g: norm_prev_extensions E p F f) ==> (EX H h. graph H h = g 
    67                                               & is_linearform H h 
    68                                               & is_subspace H E
    69                                               & is_subspace F H
    70                                               & (graph F f <= graph H h)
    71                                               & (ALL x:H. h x <= p x))";
    72  by (unfold norm_prev_extensions_def) force;
    73 
    74 lemma norm_prev_extension_I2 [intro]:  
    75    "[| is_linearform H h;    
    76        is_subspace H E;
    77        is_subspace F H;
    78        (graph F f <= graph H h);
    79        (ALL x:H. h x <= p x) |]
    80    ==> (graph H h : norm_prev_extensions E p F f)";
    81  by (unfold norm_prev_extensions_def) force;
    82 
    83 lemma norm_prev_extension_I [intro]:  
    84    "(EX H h. graph H h = g 
    85              & is_linearform H h    
    86              & is_subspace H E
    87              & is_subspace F H
    88              & (graph F f <= graph H h)
    89              & (ALL x:H. h x <= p x))
    90    ==> (g: norm_prev_extensions E p F f) ";
    91  by (unfold norm_prev_extensions_def) force;
    92 
    93 
    94 end;
    95