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