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