src/HOL/Real/HahnBanach/FunctionOrder.thy
author wenzelm
Tue Sep 21 17:31:20 1999 +0200 (1999-09-21)
changeset 7566 c5a3f980a7af
parent 7535 599d3414b51d
child 7656 2f18c0ffc348
permissions -rw-r--r--
accomodate refined facts handling;
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@7535
     6
theory FunctionOrder = Subspace + Linearform:;
wenzelm@7535
     7
wenzelm@7535
     8
wenzelm@7535
     9
section {* Order on functions *};
wenzelm@7535
    10
wenzelm@7535
    11
types 'a graph = "('a * real) set";
wenzelm@7535
    12
wenzelm@7535
    13
constdefs
wenzelm@7535
    14
  graph :: "['a set, 'a => real] => 'a graph "
wenzelm@7535
    15
  "graph F f == {p. EX x. p = (x, f x) & x:F}"; (* == {(x, f x). x:F} *)
wenzelm@7535
    16
wenzelm@7535
    17
constdefs
wenzelm@7535
    18
  domain :: "'a graph => 'a set" 
wenzelm@7535
    19
  "domain g == {x. EX y. (x, y):g}";
wenzelm@7535
    20
wenzelm@7535
    21
constdefs
wenzelm@7535
    22
  funct :: "'a graph => ('a => real)"
wenzelm@7535
    23
  "funct g == %x. (@ y. (x, y):g)";
wenzelm@7535
    24
wenzelm@7566
    25
lemma graphI [intro!!]: "x:F ==> (x, f x) : graph F f";
wenzelm@7535
    26
  by (unfold graph_def, intro CollectI exI) force;
wenzelm@7535
    27
wenzelm@7566
    28
lemma graphI2 [intro!!]: "x:F ==> EX t: (graph F f). t = (x, f x)";
wenzelm@7566
    29
  by (unfold graph_def, force);
wenzelm@7566
    30
wenzelm@7566
    31
lemma graphD1 [intro!!]: "(x, y): graph F f ==> x:F";
wenzelm@7566
    32
  by (unfold graph_def, elim CollectE exE) force;
wenzelm@7566
    33
wenzelm@7566
    34
lemma graphD2 [intro!!]: "(x, y): graph H h ==> y = h x";
wenzelm@7566
    35
  by (unfold graph_def, elim CollectE exE) force; 
wenzelm@7535
    36
wenzelm@7566
    37
lemma graph_extD1 [intro!!]: "[| graph H h <= graph H' h'; x:H |] ==> h x = h' x";
wenzelm@7566
    38
  by (unfold graph_def, force);
wenzelm@7566
    39
wenzelm@7566
    40
lemma graph_extD2 [intro!!]: "[| graph H h <= graph H' h' |] ==> H <= H'";
wenzelm@7566
    41
  by (unfold graph_def, force);
wenzelm@7566
    42
wenzelm@7566
    43
lemma graph_extI: "[| !! x. x: H ==> h x = h' x; H <= H'|] ==> graph H h <= graph H' h'";
wenzelm@7566
    44
  by (unfold graph_def, force);
wenzelm@7566
    45
wenzelm@7566
    46
lemma graph_domain_funct: 
wenzelm@7566
    47
  "(!!x y z. (x, y):g ==> (x, z):g ==> z = y) ==> graph (domain g) (funct g) = g";
wenzelm@7566
    48
proof (unfold domain_def, unfold funct_def, unfold graph_def, auto);
wenzelm@7535
    49
  fix a b; assume "(a, b) : g";
wenzelm@7535
    50
  show "(a, SOME y. (a, y) : g) : g"; by (rule selectI2);
wenzelm@7535
    51
  show "EX y. (a, y) : g"; ..;
wenzelm@7535
    52
  assume uniq: "!!x y z. (x, y):g ==> (x, z):g ==> z = y";
wenzelm@7535
    53
  show "b = (SOME y. (a, y) : g)";
wenzelm@7535
    54
  proof (rule select_equality [RS sym]);
wenzelm@7535
    55
    fix y; assume "(a, y):g"; show "y = b"; by (rule uniq);
wenzelm@7535
    56
  qed;
wenzelm@7535
    57
qed;
wenzelm@7535
    58
wenzelm@7535
    59
constdefs
wenzelm@7535
    60
  norm_prev_extensions :: 
wenzelm@7535
    61
   "['a set, 'a  => real, 'a set, 'a => real] => 'a graph set"
wenzelm@7535
    62
  "norm_prev_extensions E p F f == {g. EX H h. graph H h = g 
wenzelm@7535
    63
                                             & is_linearform H h 
wenzelm@7535
    64
                                             & is_subspace H E
wenzelm@7535
    65
                                             & is_subspace F H
wenzelm@7535
    66
                                             & (graph F f <= graph H h)
wenzelm@7535
    67
                                             & (ALL x:H. h x <= p x)}";
wenzelm@7535
    68
                       
wenzelm@7535
    69
lemma norm_prev_extension_D:  
wenzelm@7535
    70
  "(g: norm_prev_extensions E p F f) ==> (EX H h. graph H h = g 
wenzelm@7535
    71
                                              & is_linearform H h 
wenzelm@7535
    72
                                              & is_subspace H E
wenzelm@7535
    73
                                              & is_subspace F H
wenzelm@7535
    74
                                              & (graph F f <= graph H h)
wenzelm@7535
    75
                                              & (ALL x:H. h x <= p x))";
wenzelm@7535
    76
 by (unfold norm_prev_extensions_def) force;
wenzelm@7535
    77
wenzelm@7566
    78
lemma norm_prev_extensionI2 [intro]:  
wenzelm@7535
    79
   "[| is_linearform H h;    
wenzelm@7535
    80
       is_subspace H E;
wenzelm@7535
    81
       is_subspace F H;
wenzelm@7535
    82
       (graph F f <= graph H h);
wenzelm@7535
    83
       (ALL x:H. h x <= p x) |]
wenzelm@7535
    84
   ==> (graph H h : norm_prev_extensions E p F f)";
wenzelm@7535
    85
 by (unfold norm_prev_extensions_def) force;
wenzelm@7535
    86
wenzelm@7566
    87
lemma norm_prev_extensionI [intro]:  
wenzelm@7535
    88
   "(EX H h. graph H h = g 
wenzelm@7535
    89
             & is_linearform H h    
wenzelm@7535
    90
             & is_subspace H E
wenzelm@7535
    91
             & is_subspace F H
wenzelm@7535
    92
             & (graph F f <= graph H h)
wenzelm@7535
    93
             & (ALL x:H. h x <= p x))
wenzelm@7535
    94
   ==> (g: norm_prev_extensions E p F f) ";
wenzelm@7535
    95
 by (unfold norm_prev_extensions_def) force;
wenzelm@7535
    96
wenzelm@7535
    97
wenzelm@7535
    98
end;
wenzelm@7535
    99