src/HOL/Real/HahnBanach/FunctionOrder.thy
author wenzelm
Fri Oct 08 16:40:27 1999 +0200 (1999-10-08)
changeset 7808 fd019ac3485f
parent 7656 2f18c0ffc348
child 7917 5e5b9813cce7
permissions -rw-r--r--
update from Gertrud;
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@7808
     6
header {* An Order on Functions *};
wenzelm@7808
     7
wenzelm@7535
     8
theory FunctionOrder = Subspace + Linearform:;
wenzelm@7535
     9
wenzelm@7535
    10
wenzelm@7808
    11
wenzelm@7808
    12
subsection {* The graph of a function *}
wenzelm@7808
    13
wenzelm@7535
    14
wenzelm@7535
    15
types 'a graph = "('a * real) set";
wenzelm@7535
    16
wenzelm@7535
    17
constdefs
wenzelm@7535
    18
  graph :: "['a set, 'a => real] => 'a graph "
wenzelm@7535
    19
  "graph F f == {p. EX x. p = (x, f x) & x:F}"; (* == {(x, f x). x:F} *)
wenzelm@7535
    20
wenzelm@7535
    21
constdefs
wenzelm@7535
    22
  domain :: "'a graph => 'a set" 
wenzelm@7535
    23
  "domain g == {x. EX y. (x, y):g}";
wenzelm@7535
    24
wenzelm@7535
    25
constdefs
wenzelm@7535
    26
  funct :: "'a graph => ('a => real)"
wenzelm@7535
    27
  "funct g == %x. (@ y. (x, y):g)";
wenzelm@7535
    28
wenzelm@7566
    29
lemma graphI [intro!!]: "x:F ==> (x, f x) : graph F f";
wenzelm@7535
    30
  by (unfold graph_def, intro CollectI exI) force;
wenzelm@7535
    31
wenzelm@7566
    32
lemma graphI2 [intro!!]: "x:F ==> EX t: (graph F f). t = (x, f x)";
wenzelm@7566
    33
  by (unfold graph_def, force);
wenzelm@7566
    34
wenzelm@7566
    35
lemma graphD1 [intro!!]: "(x, y): graph F f ==> x:F";
wenzelm@7566
    36
  by (unfold graph_def, elim CollectE exE) force;
wenzelm@7566
    37
wenzelm@7566
    38
lemma graphD2 [intro!!]: "(x, y): graph H h ==> y = h x";
wenzelm@7566
    39
  by (unfold graph_def, elim CollectE exE) force; 
wenzelm@7535
    40
wenzelm@7808
    41
lemma graph_extD1 [intro!!]: 
wenzelm@7808
    42
  "[| graph H h <= graph H' h'; x:H |] ==> h x = h' x";
wenzelm@7566
    43
  by (unfold graph_def, force);
wenzelm@7566
    44
wenzelm@7566
    45
lemma graph_extD2 [intro!!]: "[| graph H h <= graph H' h' |] ==> H <= H'";
wenzelm@7566
    46
  by (unfold graph_def, force);
wenzelm@7566
    47
wenzelm@7808
    48
lemma graph_extI: 
wenzelm@7808
    49
  "[| !! x. x: H ==> h x = h' x; H <= H'|] ==> graph H h <= graph H' h'";
wenzelm@7566
    50
  by (unfold graph_def, force);
wenzelm@7566
    51
wenzelm@7566
    52
lemma graph_domain_funct: 
wenzelm@7808
    53
  "(!!x y z. (x, y):g ==> (x, z):g ==> z = y) 
wenzelm@7808
    54
  ==> graph (domain g) (funct g) = g";
wenzelm@7566
    55
proof (unfold domain_def, unfold funct_def, unfold graph_def, auto);
wenzelm@7535
    56
  fix a b; assume "(a, b) : g";
wenzelm@7535
    57
  show "(a, SOME y. (a, y) : g) : g"; by (rule selectI2);
wenzelm@7535
    58
  show "EX y. (a, y) : g"; ..;
wenzelm@7535
    59
  assume uniq: "!!x y z. (x, y):g ==> (x, z):g ==> z = y";
wenzelm@7535
    60
  show "b = (SOME y. (a, y) : g)";
wenzelm@7535
    61
  proof (rule select_equality [RS sym]);
wenzelm@7535
    62
    fix y; assume "(a, y):g"; show "y = b"; by (rule uniq);
wenzelm@7535
    63
  qed;
wenzelm@7535
    64
qed;
wenzelm@7535
    65
wenzelm@7808
    66
wenzelm@7808
    67
wenzelm@7808
    68
subsection {* The set of norm preserving extensions of a function *}
wenzelm@7808
    69
wenzelm@7808
    70
wenzelm@7535
    71
constdefs
wenzelm@7656
    72
  norm_pres_extensions :: 
wenzelm@7535
    73
   "['a set, 'a  => real, 'a set, 'a => real] => 'a graph set"
wenzelm@7656
    74
  "norm_pres_extensions E p F f == {g. EX H h. graph H h = g 
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
                       
wenzelm@7656
    81
lemma norm_pres_extension_D:  
wenzelm@7656
    82
  "(g: norm_pres_extensions E p F f) ==> (EX H h. graph H h = g 
wenzelm@7535
    83
                                              & is_linearform H h 
wenzelm@7535
    84
                                              & is_subspace H E
wenzelm@7535
    85
                                              & is_subspace F H
wenzelm@7535
    86
                                              & (graph F f <= graph H h)
wenzelm@7535
    87
                                              & (ALL x:H. h x <= p x))";
wenzelm@7656
    88
 by (unfold norm_pres_extensions_def) force;
wenzelm@7535
    89
wenzelm@7656
    90
lemma norm_pres_extensionI2 [intro]:  
wenzelm@7535
    91
   "[| is_linearform H h;    
wenzelm@7535
    92
       is_subspace H E;
wenzelm@7535
    93
       is_subspace F H;
wenzelm@7535
    94
       (graph F f <= graph H h);
wenzelm@7535
    95
       (ALL x:H. h x <= p x) |]
wenzelm@7656
    96
   ==> (graph H h : norm_pres_extensions E p F f)";
wenzelm@7656
    97
 by (unfold norm_pres_extensions_def) force;
wenzelm@7535
    98
wenzelm@7656
    99
lemma norm_pres_extensionI [intro]:  
wenzelm@7535
   100
   "(EX H h. graph H h = g 
wenzelm@7535
   101
             & is_linearform H h    
wenzelm@7535
   102
             & is_subspace H E
wenzelm@7535
   103
             & is_subspace F H
wenzelm@7535
   104
             & (graph F f <= graph H h)
wenzelm@7535
   105
             & (ALL x:H. h x <= p x))
wenzelm@7656
   106
   ==> (g: norm_pres_extensions E p F f) ";
wenzelm@7656
   107
 by (unfold norm_pres_extensions_def) force;
wenzelm@7535
   108
wenzelm@7535
   109
end;
wenzelm@7535
   110