src/HOL/Real/HahnBanach/FunctionOrder.thy
 author paulson Fri Sep 15 12:39:57 2000 +0200 (2000-09-15) changeset 9969 4753185f1dd2 parent 9623 3ade112482af child 10687 c186279eecea permissions -rw-r--r--
renamed (most of...) the select rules
 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@9035  6 header {* An order on functions *}  wenzelm@7808  7 wenzelm@9035  8 theory FunctionOrder = Subspace + Linearform:  wenzelm@7535  9 wenzelm@9035  10 subsection {* The graph of a function *}  wenzelm@7808  11 wenzelm@7978  12 text{* We define the \emph{graph} of a (real) function $f$ with  wenzelm@7917  13 domain $F$ as the set  wenzelm@7927  14 $ bauerg@9374  15 \{(x, f\ap x). \ap x \in F\}  wenzelm@7927  16 $  wenzelm@7978  17 So we are modeling partial functions by specifying the domain and  wenzelm@7978  18 the mapping function. We use the term function'' also for its graph.  wenzelm@9035  19 *}  wenzelm@7535  20 wenzelm@9035  21 types 'a graph = "('a * real) set"  wenzelm@7535  22 wenzelm@7535  23 constdefs  wenzelm@7535  24  graph :: "['a set, 'a => real] => 'a graph "  wenzelm@9503  25  "graph F f == {(x, f x) | x. x \ F}"  wenzelm@7535  26 wenzelm@9503  27 lemma graphI [intro?]: "x \ F ==> (x, f x) \ graph F f"  wenzelm@9035  28  by (unfold graph_def, intro CollectI exI) force  wenzelm@7535  29 wenzelm@9503  30 lemma graphI2 [intro?]: "x \ F ==> \t\ (graph F f). t = (x, f x)"  wenzelm@9035  31  by (unfold graph_def, force)  wenzelm@7566  32 wenzelm@9503  33 lemma graphD1 [intro?]: "(x, y) \ graph F f ==> x \ F"  wenzelm@9035  34  by (unfold graph_def, elim CollectE exE) force  wenzelm@7566  35 wenzelm@9503  36 lemma graphD2 [intro?]: "(x, y) \ graph H h ==> y = h x"  wenzelm@9035  37  by (unfold graph_def, elim CollectE exE) force  wenzelm@7535  38 wenzelm@9035  39 subsection {* Functions ordered by domain extension *}  wenzelm@7917  40 wenzelm@7978  41 text{* A function $h'$ is an extension of $h$, iff the graph of  wenzelm@9035  42 $h$ is a subset of the graph of $h'$.*}  wenzelm@7917  43 wenzelm@7917  44 lemma graph_extI:  wenzelm@9503  45  "[| !! x. x \ H ==> h x = h' x; H <= H'|]  wenzelm@9035  46  ==> graph H h <= graph H' h'"  wenzelm@9035  47  by (unfold graph_def, force)  wenzelm@7917  48 wenzelm@9408  49 lemma graph_extD1 [intro?]:  wenzelm@9503  50  "[| graph H h <= graph H' h'; x \ H |] ==> h x = h' x"  wenzelm@9035  51  by (unfold graph_def, force)  wenzelm@7566  52 wenzelm@9408  53 lemma graph_extD2 [intro?]:  wenzelm@9035  54  "[| graph H h <= graph H' h' |] ==> H <= H'"  wenzelm@9035  55  by (unfold graph_def, force)  wenzelm@7566  56 wenzelm@9035  57 subsection {* Domain and function of a graph *}  wenzelm@7917  58 wenzelm@7917  59 text{* The inverse functions to $\idt{graph}$ are $\idt{domain}$ and  wenzelm@9035  60 $\idt{funct}$.*}  wenzelm@7917  61 wenzelm@7917  62 constdefs  wenzelm@7917  63  domain :: "'a graph => 'a set"  wenzelm@9503  64  "domain g == {x. \y. (x, y) \ g}"  wenzelm@7917  65 wenzelm@7917  66  funct :: "'a graph => ('a => real)"  wenzelm@9503  67  "funct g == \x. (SOME y. (x, y) \ g)"  wenzelm@7917  68 wenzelm@7917  69 wenzelm@7917  70 text {* The following lemma states that $g$ is the graph of a function  wenzelm@9035  71 if the relation induced by $g$ is unique. *}  wenzelm@7566  72 wenzelm@7566  73 lemma graph_domain_funct:  wenzelm@9503  74  "(!!x y z. (x, y) \ g ==> (x, z) \ g ==> z = y)  wenzelm@9035  75  ==> graph (domain g) (funct g) = g"  wenzelm@9035  76 proof (unfold domain_def funct_def graph_def, auto)  wenzelm@9503  77  fix a b assume "(a, b) \ g"  paulson@9969  78  show "(a, SOME y. (a, y) \ g) \ g" by (rule someI2)  wenzelm@9503  79  show "\y. (a, y) \ g" ..  wenzelm@9503  80  assume uniq: "!!x y z. (x, y) \ g ==> (x, z) \ g ==> z = y"  wenzelm@9503  81  show "b = (SOME y. (a, y) \ g)"  paulson@9969  82  proof (rule some_equality [symmetric])  wenzelm@9503  83  fix y assume "(a, y) \ g" show "y = b" by (rule uniq)  wenzelm@9035  84  qed  wenzelm@9035  85 qed  wenzelm@7535  86 wenzelm@7808  87 wenzelm@7808  88 wenzelm@9035  89 subsection {* Norm-preserving extensions of a function *}  wenzelm@7917  90 wenzelm@7978  91 text {* Given a linear form $f$ on the space $F$ and a seminorm $p$ on  wenzelm@7917  92 $E$. The set of all linear extensions of $f$, to superspaces $H$ of  wenzelm@9035  93 $F$, which are bounded by $p$, is defined as follows. *}  wenzelm@7808  94 wenzelm@7808  95 wenzelm@7535  96 constdefs  wenzelm@7656  97  norm_pres_extensions ::  bauerg@9374  98  "['a::{plus, minus, zero} set, 'a => real, 'a set, 'a => real]  wenzelm@7917  99  => 'a graph set"  wenzelm@7917  100  "norm_pres_extensions E p F f  wenzelm@9503  101  == {g. \H h. graph H h = g  wenzelm@9503  102  \ is_linearform H h  wenzelm@9503  103  \ is_subspace H E  wenzelm@9503  104  \ is_subspace F H  wenzelm@9503  105  \ graph F f <= graph H h  wenzelm@9503  106  \ (\x \ H. h x <= p x)}"  wenzelm@7535  107   wenzelm@7656  108 lemma norm_pres_extension_D:  wenzelm@9503  109  "g \ norm_pres_extensions E p F f  wenzelm@9503  110  ==> \H h. graph H h = g  wenzelm@9503  111  \ is_linearform H h  wenzelm@9503  112  \ is_subspace H E  wenzelm@9503  113  \ is_subspace F H  wenzelm@9503  114  \ graph F f <= graph H h  wenzelm@9503  115  \ (\x \ H. h x <= p x)"  wenzelm@9035  116  by (unfold norm_pres_extensions_def) force  wenzelm@7535  117 wenzelm@7656  118 lemma norm_pres_extensionI2 [intro]:  wenzelm@7917  119  "[| is_linearform H h; is_subspace H E; is_subspace F H;  wenzelm@9503  120  graph F f <= graph H h; \x \ H. h x <= p x |]  wenzelm@9503  121  ==> (graph H h \ norm_pres_extensions E p F f)"  wenzelm@9035  122  by (unfold norm_pres_extensions_def) force  wenzelm@7535  123 wenzelm@7656  124 lemma norm_pres_extensionI [intro]:  wenzelm@9503  125  "\H h. graph H h = g  wenzelm@9503  126  \ is_linearform H h  wenzelm@9503  127  \ is_subspace H E  wenzelm@9503  128  \ is_subspace F H  wenzelm@9503  129  \ graph F f <= graph H h  wenzelm@9503  130  \ (\x \ H. h x <= p x)  wenzelm@9503  131  ==> g \ norm_pres_extensions E p F f"  wenzelm@9035  132  by (unfold norm_pres_extensions_def) force  wenzelm@7535  133 wenzelm@9035  134 end