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 +
```