7 |
7 |
8 theory FunctionOrder = Subspace + Linearform: |
8 theory FunctionOrder = Subspace + Linearform: |
9 |
9 |
10 subsection {* The graph of a function *} |
10 subsection {* The graph of a function *} |
11 |
11 |
12 text{* We define the \emph{graph} of a (real) function $f$ with |
12 text {* |
13 domain $F$ as the set |
13 We define the \emph{graph} of a (real) function @{text f} with |
14 \[ |
14 domain @{text F} as the set |
15 \{(x, f\ap x). \ap x \in F\} |
15 \begin{center} |
16 \] |
16 @{text "{(x, f x). x \<in> F}"} |
17 So we are modeling partial functions by specifying the domain and |
17 \end{center} |
18 the mapping function. We use the term ``function'' also for its graph. |
18 So we are modeling partial functions by specifying the domain and |
|
19 the mapping function. We use the term ``function'' also for its |
|
20 graph. |
19 *} |
21 *} |
20 |
22 |
21 types 'a graph = "('a * real) set" |
23 types 'a graph = "('a * real) set" |
22 |
24 |
23 constdefs |
25 constdefs |
24 graph :: "['a set, 'a => real] => 'a graph " |
26 graph :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a graph " |
25 "graph F f == {(x, f x) | x. x \<in> F}" |
27 "graph F f \<equiv> {(x, f x) | x. x \<in> F}" |
26 |
28 |
27 lemma graphI [intro?]: "x \<in> F ==> (x, f x) \<in> graph F f" |
29 lemma graphI [intro?]: "x \<in> F \<Longrightarrow> (x, f x) \<in> graph F f" |
28 by (unfold graph_def, intro CollectI exI) force |
30 by (unfold graph_def, intro CollectI exI) blast |
29 |
31 |
30 lemma graphI2 [intro?]: "x \<in> F ==> \<exists>t\<in> (graph F f). t = (x, f x)" |
32 lemma graphI2 [intro?]: "x \<in> F \<Longrightarrow> \<exists>t\<in> (graph F f). t = (x, f x)" |
31 by (unfold graph_def, force) |
33 by (unfold graph_def) blast |
32 |
34 |
33 lemma graphD1 [intro?]: "(x, y) \<in> graph F f ==> x \<in> F" |
35 lemma graphD1 [intro?]: "(x, y) \<in> graph F f \<Longrightarrow> x \<in> F" |
34 by (unfold graph_def, elim CollectE exE) force |
36 by (unfold graph_def) blast |
35 |
37 |
36 lemma graphD2 [intro?]: "(x, y) \<in> graph H h ==> y = h x" |
38 lemma graphD2 [intro?]: "(x, y) \<in> graph H h \<Longrightarrow> y = h x" |
37 by (unfold graph_def, elim CollectE exE) force |
39 by (unfold graph_def) blast |
|
40 |
38 |
41 |
39 subsection {* Functions ordered by domain extension *} |
42 subsection {* Functions ordered by domain extension *} |
40 |
43 |
41 text{* A function $h'$ is an extension of $h$, iff the graph of |
44 text {* A function @{text h'} is an extension of @{text h}, iff the |
42 $h$ is a subset of the graph of $h'$.*} |
45 graph of @{text h} is a subset of the graph of @{text h'}. *} |
43 |
46 |
44 lemma graph_extI: |
47 lemma graph_extI: |
45 "[| !! x. x \<in> H ==> h x = h' x; H <= H'|] |
48 "(\<And>x. x \<in> H \<Longrightarrow> h x = h' x) \<Longrightarrow> H \<subseteq> H' |
46 ==> graph H h <= graph H' h'" |
49 \<Longrightarrow> graph H h \<subseteq> graph H' h'" |
47 by (unfold graph_def, force) |
50 by (unfold graph_def) blast |
48 |
51 |
49 lemma graph_extD1 [intro?]: |
52 lemma graph_extD1 [intro?]: |
50 "[| graph H h <= graph H' h'; x \<in> H |] ==> h x = h' x" |
53 "graph H h \<subseteq> graph H' h' \<Longrightarrow> x \<in> H \<Longrightarrow> h x = h' x" |
51 by (unfold graph_def, force) |
54 by (unfold graph_def) blast |
52 |
55 |
53 lemma graph_extD2 [intro?]: |
56 lemma graph_extD2 [intro?]: |
54 "[| graph H h <= graph H' h' |] ==> H <= H'" |
57 "graph H h \<subseteq> graph H' h' \<Longrightarrow> H \<subseteq> H'" |
55 by (unfold graph_def, force) |
58 by (unfold graph_def) blast |
56 |
59 |
57 subsection {* Domain and function of a graph *} |
60 subsection {* Domain and function of a graph *} |
58 |
61 |
59 text{* The inverse functions to $\idt{graph}$ are $\idt{domain}$ and |
62 text {* |
60 $\idt{funct}$.*} |
63 The inverse functions to @{text graph} are @{text domain} and |
|
64 @{text funct}. |
|
65 *} |
61 |
66 |
62 constdefs |
67 constdefs |
63 domain :: "'a graph => 'a set" |
68 domain :: "'a graph \<Rightarrow> 'a set" |
64 "domain g == {x. \<exists>y. (x, y) \<in> g}" |
69 "domain g \<equiv> {x. \<exists>y. (x, y) \<in> g}" |
65 |
70 |
66 funct :: "'a graph => ('a => real)" |
71 funct :: "'a graph \<Rightarrow> ('a \<Rightarrow> real)" |
67 "funct g == \<lambda>x. (SOME y. (x, y) \<in> g)" |
72 "funct g \<equiv> \<lambda>x. (SOME y. (x, y) \<in> g)" |
68 |
73 |
69 |
74 |
70 text {* The following lemma states that $g$ is the graph of a function |
75 text {* |
71 if the relation induced by $g$ is unique. *} |
76 The following lemma states that @{text g} is the graph of a function |
|
77 if the relation induced by @{text g} is unique. |
|
78 *} |
72 |
79 |
73 lemma graph_domain_funct: |
80 lemma graph_domain_funct: |
74 "(!!x y z. (x, y) \<in> g ==> (x, z) \<in> g ==> z = y) |
81 "(\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y) |
75 ==> graph (domain g) (funct g) = g" |
82 \<Longrightarrow> graph (domain g) (funct g) = g" |
76 proof (unfold domain_def funct_def graph_def, auto) |
83 proof (unfold domain_def funct_def graph_def, auto) |
77 fix a b assume "(a, b) \<in> g" |
84 fix a b assume "(a, b) \<in> g" |
78 show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2) |
85 show "(a, SOME y. (a, y) \<in> g) \<in> g" by (rule someI2) |
79 show "\<exists>y. (a, y) \<in> g" .. |
86 show "\<exists>y. (a, y) \<in> g" .. |
80 assume uniq: "!!x y z. (x, y) \<in> g ==> (x, z) \<in> g ==> z = y" |
87 assume uniq: "\<And>x y z. (x, y) \<in> g \<Longrightarrow> (x, z) \<in> g \<Longrightarrow> z = y" |
81 show "b = (SOME y. (a, y) \<in> g)" |
88 show "b = (SOME y. (a, y) \<in> g)" |
82 proof (rule some_equality [symmetric]) |
89 proof (rule some_equality [symmetric]) |
83 fix y assume "(a, y) \<in> g" show "y = b" by (rule uniq) |
90 fix y assume "(a, y) \<in> g" show "y = b" by (rule uniq) |
84 qed |
91 qed |
85 qed |
92 qed |
86 |
93 |
87 |
94 |
88 |
95 |
89 subsection {* Norm-preserving extensions of a function *} |
96 subsection {* Norm-preserving extensions of a function *} |
90 |
97 |
91 text {* Given a linear form $f$ on the space $F$ and a seminorm $p$ on |
98 text {* |
92 $E$. The set of all linear extensions of $f$, to superspaces $H$ of |
99 Given a linear form @{text f} on the space @{text F} and a seminorm |
93 $F$, which are bounded by $p$, is defined as follows. *} |
100 @{text p} on @{text E}. The set of all linear extensions of @{text |
94 |
101 f}, to superspaces @{text H} of @{text F}, which are bounded by |
|
102 @{text p}, is defined as follows. |
|
103 *} |
95 |
104 |
96 constdefs |
105 constdefs |
97 norm_pres_extensions :: |
106 norm_pres_extensions :: |
98 "['a::{plus, minus, zero} set, 'a => real, 'a set, 'a => real] |
107 "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) |
99 => 'a graph set" |
108 \<Rightarrow> 'a graph set" |
100 "norm_pres_extensions E p F f |
109 "norm_pres_extensions E p F f |
101 == {g. \<exists>H h. graph H h = g |
110 \<equiv> {g. \<exists>H h. graph H h = g |
102 \<and> is_linearform H h |
111 \<and> is_linearform H h |
103 \<and> is_subspace H E |
112 \<and> is_subspace H E |
104 \<and> is_subspace F H |
113 \<and> is_subspace F H |
105 \<and> graph F f <= graph H h |
114 \<and> graph F f \<subseteq> graph H h |
106 \<and> (\<forall>x \<in> H. h x <= p x)}" |
115 \<and> (\<forall>x \<in> H. h x \<le> p x)}" |
107 |
116 |
108 lemma norm_pres_extension_D: |
117 lemma norm_pres_extension_D: |
109 "g \<in> norm_pres_extensions E p F f |
118 "g \<in> norm_pres_extensions E p F f |
110 ==> \<exists>H h. graph H h = g |
119 \<Longrightarrow> \<exists>H h. graph H h = g |
111 \<and> is_linearform H h |
120 \<and> is_linearform H h |
112 \<and> is_subspace H E |
121 \<and> is_subspace H E |
113 \<and> is_subspace F H |
122 \<and> is_subspace F H |
114 \<and> graph F f <= graph H h |
123 \<and> graph F f \<subseteq> graph H h |
115 \<and> (\<forall>x \<in> H. h x <= p x)" |
124 \<and> (\<forall>x \<in> H. h x \<le> p x)" |
116 by (unfold norm_pres_extensions_def) force |
125 by (unfold norm_pres_extensions_def) blast |
117 |
126 |
118 lemma norm_pres_extensionI2 [intro]: |
127 lemma norm_pres_extensionI2 [intro]: |
119 "[| is_linearform H h; is_subspace H E; is_subspace F H; |
128 "is_linearform H h \<Longrightarrow> is_subspace H E \<Longrightarrow> is_subspace F H \<Longrightarrow> |
120 graph F f <= graph H h; \<forall>x \<in> H. h x <= p x |] |
129 graph F f \<subseteq> graph H h \<Longrightarrow> \<forall>x \<in> H. h x \<le> p x |
121 ==> (graph H h \<in> norm_pres_extensions E p F f)" |
130 \<Longrightarrow> (graph H h \<in> norm_pres_extensions E p F f)" |
122 by (unfold norm_pres_extensions_def) force |
131 by (unfold norm_pres_extensions_def) blast |
123 |
132 |
124 lemma norm_pres_extensionI [intro]: |
133 lemma norm_pres_extensionI [intro]: |
125 "\<exists>H h. graph H h = g |
134 "\<exists>H h. graph H h = g |
126 \<and> is_linearform H h |
135 \<and> is_linearform H h |
127 \<and> is_subspace H E |
136 \<and> is_subspace H E |
128 \<and> is_subspace F H |
137 \<and> is_subspace F H |
129 \<and> graph F f <= graph H h |
138 \<and> graph F f \<subseteq> graph H h |
130 \<and> (\<forall>x \<in> H. h x <= p x) |
139 \<and> (\<forall>x \<in> H. h x \<le> p x) |
131 ==> g \<in> norm_pres_extensions E p F f" |
140 \<Longrightarrow> g \<in> norm_pres_extensions E p F f" |
132 by (unfold norm_pres_extensions_def) force |
141 by (unfold norm_pres_extensions_def) blast |
133 |
142 |
134 end |
143 end |