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