src/HOL/Real/HahnBanach/FunctionOrder.thy
changeset 7535 599d3414b51d
child 7566 c5a3f980a7af
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Real/HahnBanach/FunctionOrder.thy	Fri Sep 10 17:28:51 1999 +0200
     1.3 @@ -0,0 +1,95 @@
     1.4 +
     1.5 +theory FunctionOrder = Subspace + Linearform:;
     1.6 +
     1.7 +
     1.8 +section {* Order on functions *};
     1.9 +
    1.10 +types 'a graph = "('a * real) set";
    1.11 +
    1.12 +constdefs
    1.13 +  graph :: "['a set, 'a => real] => 'a graph "
    1.14 +  "graph F f == {p. EX x. p = (x, f x) & x:F}"; (* == {(x, f x). x:F} *)
    1.15 +
    1.16 +constdefs
    1.17 +  domain :: "'a graph => 'a set" 
    1.18 +  "domain g == {x. EX y. (x, y):g}";
    1.19 +
    1.20 +constdefs
    1.21 +  funct :: "'a graph => ('a => real)"
    1.22 +  "funct g == %x. (@ y. (x, y):g)";
    1.23 +
    1.24 +lemma graph_I: "x:F ==> (x, f x) : graph F f";
    1.25 +  by (unfold graph_def, intro CollectI exI) force;
    1.26 +
    1.27 +lemma graphD1: "(x, y): graph F f ==> x:F";
    1.28 +  by (unfold graph_def, elim CollectD [elimify] exE) force;
    1.29 +
    1.30 +lemma graph_domain_funct: "(!!x y z. (x, y):g ==> (x, z):g ==> z = y) ==> graph (domain g) (funct g) = g";
    1.31 +proof ( unfold domain_def, unfold funct_def, unfold graph_def, auto);
    1.32 +  fix a b; assume "(a, b) : g";
    1.33 +  show "(a, SOME y. (a, y) : g) : g"; by (rule selectI2);
    1.34 +  show "EX y. (a, y) : g"; ..;
    1.35 +  assume uniq: "!!x y z. (x, y):g ==> (x, z):g ==> z = y";
    1.36 +  show "b = (SOME y. (a, y) : g)";
    1.37 +  proof (rule select_equality [RS sym]);
    1.38 +    fix y; assume "(a, y):g"; show "y = b"; by (rule uniq);
    1.39 +  qed;
    1.40 +qed;
    1.41 +
    1.42 +lemma graph_lemma1: "x:F ==> EX t: (graph F f). t = (x, f x)";
    1.43 +  by (unfold graph_def, force);
    1.44 +
    1.45 +lemma graph_lemma2: "(x, y): graph H h ==> y = h x";
    1.46 +  by (unfold graph_def, elim CollectD [elimify] exE) force; 
    1.47 +
    1.48 +lemma graph_lemma3: "[| graph H h <= graph H' h'; x:H |] ==> h x = h' x";
    1.49 +  by (unfold graph_def, force);
    1.50 +
    1.51 +lemma graph_lemma4: "[| graph H h <= graph H' h' |] ==> H <= H'";
    1.52 +  by (unfold graph_def, force);
    1.53 +
    1.54 +lemma graph_lemma5: "[| !! x. x: H ==> h x = h' x; H <= H'|] ==> graph H h <= graph H' h'";
    1.55 +  by (unfold graph_def, force);
    1.56 +
    1.57 +
    1.58 +constdefs
    1.59 +  norm_prev_extensions :: 
    1.60 +   "['a set, 'a  => real, 'a set, 'a => real] => 'a graph set"
    1.61 +  "norm_prev_extensions E p F f == {g. EX H h. graph H h = g 
    1.62 +                                             & is_linearform H h 
    1.63 +                                             & is_subspace H E
    1.64 +                                             & is_subspace F H
    1.65 +                                             & (graph F f <= graph H h)
    1.66 +                                             & (ALL x:H. h x <= p x)}";
    1.67 +                       
    1.68 +lemma norm_prev_extension_D:  
    1.69 +  "(g: norm_prev_extensions E p F f) ==> (EX H h. graph H h = g 
    1.70 +                                              & is_linearform H h 
    1.71 +                                              & is_subspace H E
    1.72 +                                              & is_subspace F H
    1.73 +                                              & (graph F f <= graph H h)
    1.74 +                                              & (ALL x:H. h x <= p x))";
    1.75 + by (unfold norm_prev_extensions_def) force;
    1.76 +
    1.77 +lemma norm_prev_extension_I2 [intro]:  
    1.78 +   "[| is_linearform H h;    
    1.79 +       is_subspace H E;
    1.80 +       is_subspace F H;
    1.81 +       (graph F f <= graph H h);
    1.82 +       (ALL x:H. h x <= p x) |]
    1.83 +   ==> (graph H h : norm_prev_extensions E p F f)";
    1.84 + by (unfold norm_prev_extensions_def) force;
    1.85 +
    1.86 +lemma norm_prev_extension_I [intro]:  
    1.87 +   "(EX H h. graph H h = g 
    1.88 +             & is_linearform H h    
    1.89 +             & is_subspace H E
    1.90 +             & is_subspace F H
    1.91 +             & (graph F f <= graph H h)
    1.92 +             & (ALL x:H. h x <= p x))
    1.93 +   ==> (g: norm_prev_extensions E p F f) ";
    1.94 + by (unfold norm_prev_extensions_def) force;
    1.95 +
    1.96 +
    1.97 +end;
    1.98 +