src/HOL/Real/HahnBanach/FunctionOrder.thy
 author wenzelm Sun Jul 23 12:01:05 2000 +0200 (2000-07-23) changeset 9408 d3d56e1d2ec1 parent 9379 21cfeae6659d child 9503 3324cbbecef8 permissions -rw-r--r--
classical atts now intro! / intro / intro?;
 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 "  bauerg@9379  25  "graph F f == {(x, f x) | x. x \\ F}"  wenzelm@7535  26 wenzelm@9408  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@9408  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@9408  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@9408  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:  bauerg@9379  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?]:  bauerg@9379  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"  bauerg@9379  64  "domain g == {x. \\y. (x, y) \\ g}"  wenzelm@7917  65 wenzelm@7917  66  funct :: "'a graph => ('a => real)"  bauerg@9379  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:  bauerg@9379  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)  bauerg@9379  77  fix a b assume "(a, b) \\ g"  bauerg@9379  78  show "(a, SOME y. (a, y) \\ g) \\ g" by (rule selectI2)  bauerg@9379  79  show "\\y. (a, y) \\ g" ..  bauerg@9379  80  assume uniq: "!!x y z. (x, y) \\ g ==> (x, z) \\ g ==> z = y"  bauerg@9379  81  show "b = (SOME y. (a, y) \\ g)"  wenzelm@9035  82  proof (rule select_equality [RS sym])  bauerg@9379  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  bauerg@9379  101  == {g. \\H h. graph H h = g  bauerg@9379  102  \\ is_linearform H h  bauerg@9379  103  \\ is_subspace H E  bauerg@9379  104  \\ is_subspace F H  bauerg@9379  105  \\ graph F f <= graph H h  bauerg@9379  106  \\ (\\x \\ H. h x <= p x)}"  wenzelm@7535  107   wenzelm@7656  108 lemma norm_pres_extension_D:  bauerg@9379  109  "g \\ norm_pres_extensions E p F f  bauerg@9379  110  ==> \\H h. graph H h = g  bauerg@9379  111  \\ is_linearform H h  bauerg@9379  112  \\ is_subspace H E  bauerg@9379  113  \\ is_subspace F H  bauerg@9379  114  \\ graph F f <= graph H h  bauerg@9379  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;  bauerg@9379  120  graph F f <= graph H h; \\x \\ H. h x <= p x |]  bauerg@9379  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]:  bauerg@9379  125  "\\H h. graph H h = g  bauerg@9379  126  \\ is_linearform H h  bauerg@9379  127  \\ is_subspace H E  bauerg@9379  128  \\ is_subspace F H  bauerg@9379  129  \\ graph F f <= graph H h  bauerg@9379  130  \\ (\\x \\ H. h x <= p x)  bauerg@9379  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