11 "~~/src/HOL/Library/Numeral_Type" |
11 "~~/src/HOL/Library/Numeral_Type" |
12 begin |
12 begin |
13 |
13 |
14 subsection {* Finite Cartesian products, with indexing and lambdas. *} |
14 subsection {* Finite Cartesian products, with indexing and lambdas. *} |
15 |
15 |
16 typedef (open Cart) |
16 typedef (open) |
17 ('a, 'b) cart = "UNIV :: (('b::finite) \<Rightarrow> 'a) set" |
17 ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set" |
18 morphisms Cart_nth Cart_lambda .. |
18 morphisms vec_nth vec_lambda .. |
19 |
19 |
20 notation |
20 notation |
21 Cart_nth (infixl "$" 90) and |
21 vec_nth (infixl "$" 90) and |
22 Cart_lambda (binder "\<chi>" 10) |
22 vec_lambda (binder "\<chi>" 10) |
23 |
23 |
24 (* |
24 (* |
25 Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than |
25 Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than |
26 the finite type class write "cart 'b 'n" |
26 the finite type class write "vec 'b 'n" |
27 *) |
27 *) |
28 |
28 |
29 syntax "_finite_cart" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15) |
29 syntax "_finite_vec" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15) |
30 |
30 |
31 parse_translation {* |
31 parse_translation {* |
32 let |
32 let |
33 fun cart t u = Syntax.const @{type_syntax cart} $ t $ u; |
33 fun vec t u = Syntax.const @{type_syntax vec} $ t $ u; |
34 fun finite_cart_tr [t, u as Free (x, _)] = |
34 fun finite_vec_tr [t, u as Free (x, _)] = |
35 if Lexicon.is_tid x then |
35 if Lexicon.is_tid x then |
36 cart t (Syntax.const @{syntax_const "_ofsort"} $ u $ Syntax.const @{class_syntax finite}) |
36 vec t (Syntax.const @{syntax_const "_ofsort"} $ u $ Syntax.const @{class_syntax finite}) |
37 else cart t u |
37 else vec t u |
38 | finite_cart_tr [t, u] = cart t u |
38 | finite_vec_tr [t, u] = vec t u |
39 in |
39 in |
40 [(@{syntax_const "_finite_cart"}, finite_cart_tr)] |
40 [(@{syntax_const "_finite_vec"}, finite_vec_tr)] |
41 end |
41 end |
42 *} |
42 *} |
43 |
43 |
44 lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)" |
44 lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)" |
45 by (auto intro: ext) |
45 by (auto intro: ext) |
46 |
46 |
47 lemma Cart_eq: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)" |
47 lemma vec_eq_iff: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)" |
48 by (simp add: Cart_nth_inject [symmetric] fun_eq_iff) |
48 by (simp add: vec_nth_inject [symmetric] fun_eq_iff) |
49 |
49 |
50 lemma Cart_lambda_beta [simp]: "Cart_lambda g $ i = g i" |
50 lemma vec_lambda_beta [simp]: "vec_lambda g $ i = g i" |
51 by (simp add: Cart_lambda_inverse) |
51 by (simp add: vec_lambda_inverse) |
52 |
52 |
53 lemma Cart_lambda_unique: "(\<forall>i. f$i = g i) \<longleftrightarrow> Cart_lambda g = f" |
53 lemma vec_lambda_unique: "(\<forall>i. f$i = g i) \<longleftrightarrow> vec_lambda g = f" |
54 by (auto simp add: Cart_eq) |
54 by (auto simp add: vec_eq_iff) |
55 |
55 |
56 lemma Cart_lambda_eta: "(\<chi> i. (g$i)) = g" |
56 lemma vec_lambda_eta: "(\<chi> i. (g$i)) = g" |
57 by (simp add: Cart_eq) |
57 by (simp add: vec_eq_iff) |
58 |
58 |
59 |
59 |
60 subsection {* Group operations and class instances *} |
60 subsection {* Group operations and class instances *} |
61 |
61 |
62 instantiation cart :: (zero,finite) zero |
62 instantiation vec :: (zero, finite) zero |
63 begin |
63 begin |
64 definition vector_zero_def : "0 \<equiv> (\<chi> i. 0)" |
64 definition "0 \<equiv> (\<chi> i. 0)" |
65 instance .. |
65 instance .. |
66 end |
66 end |
67 |
67 |
68 instantiation cart :: (plus,finite) plus |
68 instantiation vec :: (plus, finite) plus |
69 begin |
69 begin |
70 definition vector_add_def : "op + \<equiv> (\<lambda> x y. (\<chi> i. (x$i) + (y$i)))" |
70 definition "op + \<equiv> (\<lambda> x y. (\<chi> i. x$i + y$i))" |
71 instance .. |
71 instance .. |
72 end |
72 end |
73 |
73 |
74 instantiation cart :: (minus,finite) minus |
74 instantiation vec :: (minus, finite) minus |
75 begin |
75 begin |
76 definition vector_minus_def : "op - \<equiv> (\<lambda> x y. (\<chi> i. (x$i) - (y$i)))" |
76 definition "op - \<equiv> (\<lambda> x y. (\<chi> i. x$i - y$i))" |
77 instance .. |
77 instance .. |
78 end |
78 end |
79 |
79 |
80 instantiation cart :: (uminus,finite) uminus |
80 instantiation vec :: (uminus, finite) uminus |
81 begin |
81 begin |
82 definition vector_uminus_def : "uminus \<equiv> (\<lambda> x. (\<chi> i. - (x$i)))" |
82 definition "uminus \<equiv> (\<lambda> x. (\<chi> i. - (x$i)))" |
83 instance .. |
83 instance .. |
84 end |
84 end |
85 |
85 |
86 lemma zero_index [simp]: "0 $ i = 0" |
86 lemma zero_index [simp]: "0 $ i = 0" |
87 unfolding vector_zero_def by simp |
87 unfolding zero_vec_def by simp |
88 |
88 |
89 lemma vector_add_component [simp]: "(x + y)$i = x$i + y$i" |
89 lemma vector_add_component [simp]: "(x + y)$i = x$i + y$i" |
90 unfolding vector_add_def by simp |
90 unfolding plus_vec_def by simp |
91 |
91 |
92 lemma vector_minus_component [simp]: "(x - y)$i = x$i - y$i" |
92 lemma vector_minus_component [simp]: "(x - y)$i = x$i - y$i" |
93 unfolding vector_minus_def by simp |
93 unfolding minus_vec_def by simp |
94 |
94 |
95 lemma vector_uminus_component [simp]: "(- x)$i = - (x$i)" |
95 lemma vector_uminus_component [simp]: "(- x)$i = - (x$i)" |
96 unfolding vector_uminus_def by simp |
96 unfolding uminus_vec_def by simp |
97 |
97 |
98 instance cart :: (semigroup_add, finite) semigroup_add |
98 instance vec :: (semigroup_add, finite) semigroup_add |
99 by default (simp add: Cart_eq add_assoc) |
99 by default (simp add: vec_eq_iff add_assoc) |
100 |
100 |
101 instance cart :: (ab_semigroup_add, finite) ab_semigroup_add |
101 instance vec :: (ab_semigroup_add, finite) ab_semigroup_add |
102 by default (simp add: Cart_eq add_commute) |
102 by default (simp add: vec_eq_iff add_commute) |
103 |
103 |
104 instance cart :: (monoid_add, finite) monoid_add |
104 instance vec :: (monoid_add, finite) monoid_add |
105 by default (simp_all add: Cart_eq) |
105 by default (simp_all add: vec_eq_iff) |
106 |
106 |
107 instance cart :: (comm_monoid_add, finite) comm_monoid_add |
107 instance vec :: (comm_monoid_add, finite) comm_monoid_add |
108 by default (simp add: Cart_eq) |
108 by default (simp add: vec_eq_iff) |
109 |
109 |
110 instance cart :: (cancel_semigroup_add, finite) cancel_semigroup_add |
110 instance vec :: (cancel_semigroup_add, finite) cancel_semigroup_add |
111 by default (simp_all add: Cart_eq) |
111 by default (simp_all add: vec_eq_iff) |
112 |
112 |
113 instance cart :: (cancel_ab_semigroup_add, finite) cancel_ab_semigroup_add |
113 instance vec :: (cancel_ab_semigroup_add, finite) cancel_ab_semigroup_add |
114 by default (simp add: Cart_eq) |
114 by default (simp add: vec_eq_iff) |
115 |
115 |
116 instance cart :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add .. |
116 instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add .. |
117 |
117 |
118 instance cart :: (group_add, finite) group_add |
118 instance vec :: (group_add, finite) group_add |
119 by default (simp_all add: Cart_eq diff_minus) |
119 by default (simp_all add: vec_eq_iff diff_minus) |
120 |
120 |
121 instance cart :: (ab_group_add, finite) ab_group_add |
121 instance vec :: (ab_group_add, finite) ab_group_add |
122 by default (simp_all add: Cart_eq) |
122 by default (simp_all add: vec_eq_iff) |
123 |
123 |
124 |
124 |
125 subsection {* Real vector space *} |
125 subsection {* Real vector space *} |
126 |
126 |
127 instantiation cart :: (real_vector, finite) real_vector |
127 instantiation vec :: (real_vector, finite) real_vector |
128 begin |
128 begin |
129 |
129 |
130 definition vector_scaleR_def: "scaleR = (\<lambda> r x. (\<chi> i. scaleR r (x$i)))" |
130 definition "scaleR \<equiv> (\<lambda> r x. (\<chi> i. scaleR r (x$i)))" |
131 |
131 |
132 lemma vector_scaleR_component [simp]: "(scaleR r x)$i = scaleR r (x$i)" |
132 lemma vector_scaleR_component [simp]: "(scaleR r x)$i = scaleR r (x$i)" |
133 unfolding vector_scaleR_def by simp |
133 unfolding scaleR_vec_def by simp |
134 |
134 |
135 instance |
135 instance |
136 by default (simp_all add: Cart_eq scaleR_left_distrib scaleR_right_distrib) |
136 by default (simp_all add: vec_eq_iff scaleR_left_distrib scaleR_right_distrib) |
137 |
137 |
138 end |
138 end |
139 |
139 |
140 |
140 |
141 subsection {* Topological space *} |
141 subsection {* Topological space *} |
142 |
142 |
143 instantiation cart :: (topological_space, finite) topological_space |
143 instantiation vec :: (topological_space, finite) topological_space |
144 begin |
144 begin |
145 |
145 |
146 definition open_vector_def: |
146 definition |
147 "open (S :: ('a ^ 'b) set) \<longleftrightarrow> |
147 "open (S :: ('a ^ 'b) set) \<longleftrightarrow> |
148 (\<forall>x\<in>S. \<exists>A. (\<forall>i. open (A i) \<and> x$i \<in> A i) \<and> |
148 (\<forall>x\<in>S. \<exists>A. (\<forall>i. open (A i) \<and> x$i \<in> A i) \<and> |
149 (\<forall>y. (\<forall>i. y$i \<in> A i) \<longrightarrow> y \<in> S))" |
149 (\<forall>y. (\<forall>i. y$i \<in> A i) \<longrightarrow> y \<in> S))" |
150 |
150 |
151 instance proof |
151 instance proof |
152 show "open (UNIV :: ('a ^ 'b) set)" |
152 show "open (UNIV :: ('a ^ 'b) set)" |
153 unfolding open_vector_def by auto |
153 unfolding open_vec_def by auto |
154 next |
154 next |
155 fix S T :: "('a ^ 'b) set" |
155 fix S T :: "('a ^ 'b) set" |
156 assume "open S" "open T" thus "open (S \<inter> T)" |
156 assume "open S" "open T" thus "open (S \<inter> T)" |
157 unfolding open_vector_def |
157 unfolding open_vec_def |
158 apply clarify |
158 apply clarify |
159 apply (drule (1) bspec)+ |
159 apply (drule (1) bspec)+ |
160 apply (clarify, rename_tac Sa Ta) |
160 apply (clarify, rename_tac Sa Ta) |
161 apply (rule_tac x="\<lambda>i. Sa i \<inter> Ta i" in exI) |
161 apply (rule_tac x="\<lambda>i. Sa i \<inter> Ta i" in exI) |
162 apply (simp add: open_Int) |
162 apply (simp add: open_Int) |
163 done |
163 done |
164 next |
164 next |
165 fix K :: "('a ^ 'b) set set" |
165 fix K :: "('a ^ 'b) set set" |
166 assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)" |
166 assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)" |
167 unfolding open_vector_def |
167 unfolding open_vec_def |
168 apply clarify |
168 apply clarify |
169 apply (drule (1) bspec) |
169 apply (drule (1) bspec) |
170 apply (drule (1) bspec) |
170 apply (drule (1) bspec) |
171 apply clarify |
171 apply clarify |
172 apply (rule_tac x=A in exI) |
172 apply (rule_tac x=A in exI) |
175 qed |
175 qed |
176 |
176 |
177 end |
177 end |
178 |
178 |
179 lemma open_vector_box: "\<forall>i. open (S i) \<Longrightarrow> open {x. \<forall>i. x $ i \<in> S i}" |
179 lemma open_vector_box: "\<forall>i. open (S i) \<Longrightarrow> open {x. \<forall>i. x $ i \<in> S i}" |
180 unfolding open_vector_def by auto |
180 unfolding open_vec_def by auto |
181 |
181 |
182 lemma open_vimage_Cart_nth: "open S \<Longrightarrow> open ((\<lambda>x. x $ i) -` S)" |
182 lemma open_vimage_vec_nth: "open S \<Longrightarrow> open ((\<lambda>x. x $ i) -` S)" |
183 unfolding open_vector_def |
183 unfolding open_vec_def |
184 apply clarify |
184 apply clarify |
185 apply (rule_tac x="\<lambda>k. if k = i then S else UNIV" in exI, simp) |
185 apply (rule_tac x="\<lambda>k. if k = i then S else UNIV" in exI, simp) |
186 done |
186 done |
187 |
187 |
188 lemma closed_vimage_Cart_nth: "closed S \<Longrightarrow> closed ((\<lambda>x. x $ i) -` S)" |
188 lemma closed_vimage_vec_nth: "closed S \<Longrightarrow> closed ((\<lambda>x. x $ i) -` S)" |
189 unfolding closed_open vimage_Compl [symmetric] |
189 unfolding closed_open vimage_Compl [symmetric] |
190 by (rule open_vimage_Cart_nth) |
190 by (rule open_vimage_vec_nth) |
191 |
191 |
192 lemma closed_vector_box: "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}" |
192 lemma closed_vector_box: "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}" |
193 proof - |
193 proof - |
194 have "{x. \<forall>i. x $ i \<in> S i} = (\<Inter>i. (\<lambda>x. x $ i) -` S i)" by auto |
194 have "{x. \<forall>i. x $ i \<in> S i} = (\<Inter>i. (\<lambda>x. x $ i) -` S i)" by auto |
195 thus "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}" |
195 thus "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}" |
196 by (simp add: closed_INT closed_vimage_Cart_nth) |
196 by (simp add: closed_INT closed_vimage_vec_nth) |
197 qed |
197 qed |
198 |
198 |
199 lemma tendsto_Cart_nth [tendsto_intros]: |
199 lemma tendsto_vec_nth [tendsto_intros]: |
200 assumes "((\<lambda>x. f x) ---> a) net" |
200 assumes "((\<lambda>x. f x) ---> a) net" |
201 shows "((\<lambda>x. f x $ i) ---> a $ i) net" |
201 shows "((\<lambda>x. f x $ i) ---> a $ i) net" |
202 proof (rule topological_tendstoI) |
202 proof (rule topological_tendstoI) |
203 fix S assume "open S" "a $ i \<in> S" |
203 fix S assume "open S" "a $ i \<in> S" |
204 then have "open ((\<lambda>y. y $ i) -` S)" "a \<in> ((\<lambda>y. y $ i) -` S)" |
204 then have "open ((\<lambda>y. y $ i) -` S)" "a \<in> ((\<lambda>y. y $ i) -` S)" |
205 by (simp_all add: open_vimage_Cart_nth) |
205 by (simp_all add: open_vimage_vec_nth) |
206 with assms have "eventually (\<lambda>x. f x \<in> (\<lambda>y. y $ i) -` S) net" |
206 with assms have "eventually (\<lambda>x. f x \<in> (\<lambda>y. y $ i) -` S) net" |
207 by (rule topological_tendstoD) |
207 by (rule topological_tendstoD) |
208 then show "eventually (\<lambda>x. f x $ i \<in> S) net" |
208 then show "eventually (\<lambda>x. f x $ i \<in> S) net" |
209 by simp |
209 by simp |
210 qed |
210 qed |
218 fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool" |
218 fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool" |
219 assumes "\<And>y. eventually (\<lambda>x. P x y) net" |
219 assumes "\<And>y. eventually (\<lambda>x. P x y) net" |
220 shows "eventually (\<lambda>x. \<forall>y. P x y) net" |
220 shows "eventually (\<lambda>x. \<forall>y. P x y) net" |
221 using eventually_Ball_finite [of UNIV P] assms by simp |
221 using eventually_Ball_finite [of UNIV P] assms by simp |
222 |
222 |
223 lemma tendsto_vector: |
223 lemma vec_tendstoI: |
224 assumes "\<And>i. ((\<lambda>x. f x $ i) ---> a $ i) net" |
224 assumes "\<And>i. ((\<lambda>x. f x $ i) ---> a $ i) net" |
225 shows "((\<lambda>x. f x) ---> a) net" |
225 shows "((\<lambda>x. f x) ---> a) net" |
226 proof (rule topological_tendstoI) |
226 proof (rule topological_tendstoI) |
227 fix S assume "open S" and "a \<in> S" |
227 fix S assume "open S" and "a \<in> S" |
228 then obtain A where A: "\<And>i. open (A i)" "\<And>i. a $ i \<in> A i" |
228 then obtain A where A: "\<And>i. open (A i)" "\<And>i. a $ i \<in> A i" |
229 and S: "\<And>y. \<forall>i. y $ i \<in> A i \<Longrightarrow> y \<in> S" |
229 and S: "\<And>y. \<forall>i. y $ i \<in> A i \<Longrightarrow> y \<in> S" |
230 unfolding open_vector_def by metis |
230 unfolding open_vec_def by metis |
231 have "\<And>i. eventually (\<lambda>x. f x $ i \<in> A i) net" |
231 have "\<And>i. eventually (\<lambda>x. f x $ i \<in> A i) net" |
232 using assms A by (rule topological_tendstoD) |
232 using assms A by (rule topological_tendstoD) |
233 hence "eventually (\<lambda>x. \<forall>i. f x $ i \<in> A i) net" |
233 hence "eventually (\<lambda>x. \<forall>i. f x $ i \<in> A i) net" |
234 by (rule eventually_all_finite) |
234 by (rule eventually_all_finite) |
235 thus "eventually (\<lambda>x. f x \<in> S) net" |
235 thus "eventually (\<lambda>x. f x \<in> S) net" |
236 by (rule eventually_elim1, simp add: S) |
236 by (rule eventually_elim1, simp add: S) |
237 qed |
237 qed |
238 |
238 |
239 lemma tendsto_Cart_lambda [tendsto_intros]: |
239 lemma tendsto_vec_lambda [tendsto_intros]: |
240 assumes "\<And>i. ((\<lambda>x. f x i) ---> a i) net" |
240 assumes "\<And>i. ((\<lambda>x. f x i) ---> a i) net" |
241 shows "((\<lambda>x. \<chi> i. f x i) ---> (\<chi> i. a i)) net" |
241 shows "((\<lambda>x. \<chi> i. f x i) ---> (\<chi> i. a i)) net" |
242 using assms by (simp add: tendsto_vector) |
242 using assms by (simp add: vec_tendstoI) |
243 |
243 |
244 |
244 |
245 subsection {* Metric *} |
245 subsection {* Metric *} |
246 |
246 |
247 (* TODO: move somewhere else *) |
247 (* TODO: move somewhere else *) |
249 apply (induct set: finite, simp_all) |
249 apply (induct set: finite, simp_all) |
250 apply (clarify, rename_tac y) |
250 apply (clarify, rename_tac y) |
251 apply (rule_tac x="f(x:=y)" in exI, simp) |
251 apply (rule_tac x="f(x:=y)" in exI, simp) |
252 done |
252 done |
253 |
253 |
254 instantiation cart :: (metric_space, finite) metric_space |
254 instantiation vec :: (metric_space, finite) metric_space |
255 begin |
255 begin |
256 |
256 |
257 definition dist_vector_def: |
257 definition |
258 "dist x y = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV" |
258 "dist x y = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV" |
259 |
259 |
260 lemma dist_nth_le_cart: "dist (x $ i) (y $ i) \<le> dist x y" |
260 lemma dist_vec_nth_le: "dist (x $ i) (y $ i) \<le> dist x y" |
261 unfolding dist_vector_def |
261 unfolding dist_vec_def by (rule member_le_setL2) simp_all |
262 by (rule member_le_setL2) simp_all |
|
263 |
262 |
264 instance proof |
263 instance proof |
265 fix x y :: "'a ^ 'b" |
264 fix x y :: "'a ^ 'b" |
266 show "dist x y = 0 \<longleftrightarrow> x = y" |
265 show "dist x y = 0 \<longleftrightarrow> x = y" |
267 unfolding dist_vector_def |
266 unfolding dist_vec_def |
268 by (simp add: setL2_eq_0_iff Cart_eq) |
267 by (simp add: setL2_eq_0_iff vec_eq_iff) |
269 next |
268 next |
270 fix x y z :: "'a ^ 'b" |
269 fix x y z :: "'a ^ 'b" |
271 show "dist x y \<le> dist x z + dist y z" |
270 show "dist x y \<le> dist x z + dist y z" |
272 unfolding dist_vector_def |
271 unfolding dist_vec_def |
273 apply (rule order_trans [OF _ setL2_triangle_ineq]) |
272 apply (rule order_trans [OF _ setL2_triangle_ineq]) |
274 apply (simp add: setL2_mono dist_triangle2) |
273 apply (simp add: setL2_mono dist_triangle2) |
275 done |
274 done |
276 next |
275 next |
277 (* FIXME: long proof! *) |
276 (* FIXME: long proof! *) |
278 fix S :: "('a ^ 'b) set" |
277 fix S :: "('a ^ 'b) set" |
279 show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" |
278 show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" |
280 unfolding open_vector_def open_dist |
279 unfolding open_vec_def open_dist |
281 apply safe |
280 apply safe |
282 apply (drule (1) bspec) |
281 apply (drule (1) bspec) |
283 apply clarify |
282 apply clarify |
284 apply (subgoal_tac "\<exists>e>0. \<forall>i y. dist y (x$i) < e \<longrightarrow> y \<in> A i") |
283 apply (subgoal_tac "\<exists>e>0. \<forall>i y. dist y (x$i) < e \<longrightarrow> y \<in> A i") |
285 apply clarify |
284 apply clarify |
286 apply (rule_tac x=e in exI, clarify) |
285 apply (rule_tac x=e in exI, clarify) |
287 apply (drule spec, erule mp, clarify) |
286 apply (drule spec, erule mp, clarify) |
288 apply (drule spec, drule spec, erule mp) |
287 apply (drule spec, drule spec, erule mp) |
289 apply (erule le_less_trans [OF dist_nth_le_cart]) |
288 apply (erule le_less_trans [OF dist_vec_nth_le]) |
290 apply (subgoal_tac "\<forall>i\<in>UNIV. \<exists>e>0. \<forall>y. dist y (x$i) < e \<longrightarrow> y \<in> A i") |
289 apply (subgoal_tac "\<forall>i\<in>UNIV. \<exists>e>0. \<forall>y. dist y (x$i) < e \<longrightarrow> y \<in> A i") |
291 apply (drule finite_choice [OF finite], clarify) |
290 apply (drule finite_choice [OF finite], clarify) |
292 apply (rule_tac x="Min (range f)" in exI, simp) |
291 apply (rule_tac x="Min (range f)" in exI, simp) |
293 apply clarify |
292 apply clarify |
294 apply (drule_tac x=i in spec, clarify) |
293 apply (drule_tac x=i in spec, clarify) |
352 hence "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r" |
351 hence "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r" |
353 by simp |
352 by simp |
354 then show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r" .. |
353 then show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r" .. |
355 qed |
354 qed |
356 |
355 |
357 instance cart :: (complete_space, finite) complete_space |
356 instance vec :: (complete_space, finite) complete_space |
358 proof |
357 proof |
359 fix X :: "nat \<Rightarrow> 'a ^ 'b" assume "Cauchy X" |
358 fix X :: "nat \<Rightarrow> 'a ^ 'b" assume "Cauchy X" |
360 have "\<And>i. (\<lambda>n. X n $ i) ----> lim (\<lambda>n. X n $ i)" |
359 have "\<And>i. (\<lambda>n. X n $ i) ----> lim (\<lambda>n. X n $ i)" |
361 using Cauchy_Cart_nth [OF `Cauchy X`] |
360 using Cauchy_vec_nth [OF `Cauchy X`] |
362 by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) |
361 by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) |
363 hence "X ----> Cart_lambda (\<lambda>i. lim (\<lambda>n. X n $ i))" |
362 hence "X ----> vec_lambda (\<lambda>i. lim (\<lambda>n. X n $ i))" |
364 by (simp add: tendsto_vector) |
363 by (simp add: vec_tendstoI) |
365 then show "convergent X" |
364 then show "convergent X" |
366 by (rule convergentI) |
365 by (rule convergentI) |
367 qed |
366 qed |
368 |
367 |
369 |
368 |
370 subsection {* Normed vector space *} |
369 subsection {* Normed vector space *} |
371 |
370 |
372 instantiation cart :: (real_normed_vector, finite) real_normed_vector |
371 instantiation vec :: (real_normed_vector, finite) real_normed_vector |
373 begin |
372 begin |
374 |
373 |
375 definition norm_vector_def: |
374 definition "norm x = setL2 (\<lambda>i. norm (x$i)) UNIV" |
376 "norm x = setL2 (\<lambda>i. norm (x$i)) UNIV" |
|
377 |
375 |
378 definition vector_sgn_def: |
376 definition vector_sgn_def: |
379 "sgn (x::'a^'b) = scaleR (inverse (norm x)) x" |
377 "sgn (x::'a^'b) = scaleR (inverse (norm x)) x" |
380 |
378 |
381 instance proof |
379 instance proof |
382 fix a :: real and x y :: "'a ^ 'b" |
380 fix a :: real and x y :: "'a ^ 'b" |
383 show "0 \<le> norm x" |
381 show "0 \<le> norm x" |
384 unfolding norm_vector_def |
382 unfolding norm_vec_def |
385 by (rule setL2_nonneg) |
383 by (rule setL2_nonneg) |
386 show "norm x = 0 \<longleftrightarrow> x = 0" |
384 show "norm x = 0 \<longleftrightarrow> x = 0" |
387 unfolding norm_vector_def |
385 unfolding norm_vec_def |
388 by (simp add: setL2_eq_0_iff Cart_eq) |
386 by (simp add: setL2_eq_0_iff vec_eq_iff) |
389 show "norm (x + y) \<le> norm x + norm y" |
387 show "norm (x + y) \<le> norm x + norm y" |
390 unfolding norm_vector_def |
388 unfolding norm_vec_def |
391 apply (rule order_trans [OF _ setL2_triangle_ineq]) |
389 apply (rule order_trans [OF _ setL2_triangle_ineq]) |
392 apply (simp add: setL2_mono norm_triangle_ineq) |
390 apply (simp add: setL2_mono norm_triangle_ineq) |
393 done |
391 done |
394 show "norm (scaleR a x) = \<bar>a\<bar> * norm x" |
392 show "norm (scaleR a x) = \<bar>a\<bar> * norm x" |
395 unfolding norm_vector_def |
393 unfolding norm_vec_def |
396 by (simp add: setL2_right_distrib) |
394 by (simp add: setL2_right_distrib) |
397 show "sgn x = scaleR (inverse (norm x)) x" |
395 show "sgn x = scaleR (inverse (norm x)) x" |
398 by (rule vector_sgn_def) |
396 by (rule vector_sgn_def) |
399 show "dist x y = norm (x - y)" |
397 show "dist x y = norm (x - y)" |
400 unfolding dist_vector_def norm_vector_def |
398 unfolding dist_vec_def norm_vec_def |
401 by (simp add: dist_norm) |
399 by (simp add: dist_norm) |
402 qed |
400 qed |
403 |
401 |
404 end |
402 end |
405 |
403 |
406 lemma norm_nth_le: "norm (x $ i) \<le> norm x" |
404 lemma norm_nth_le: "norm (x $ i) \<le> norm x" |
407 unfolding norm_vector_def |
405 unfolding norm_vec_def |
408 by (rule member_le_setL2) simp_all |
406 by (rule member_le_setL2) simp_all |
409 |
407 |
410 interpretation Cart_nth: bounded_linear "\<lambda>x. x $ i" |
408 interpretation vec_nth: bounded_linear "\<lambda>x. x $ i" |
411 apply default |
409 apply default |
412 apply (rule vector_add_component) |
410 apply (rule vector_add_component) |
413 apply (rule vector_scaleR_component) |
411 apply (rule vector_scaleR_component) |
414 apply (rule_tac x="1" in exI, simp add: norm_nth_le) |
412 apply (rule_tac x="1" in exI, simp add: norm_nth_le) |
415 done |
413 done |
416 |
414 |
417 instance cart :: (banach, finite) banach .. |
415 instance vec :: (banach, finite) banach .. |
418 |
416 |
419 |
417 |
420 subsection {* Inner product space *} |
418 subsection {* Inner product space *} |
421 |
419 |
422 instantiation cart :: (real_inner, finite) real_inner |
420 instantiation vec :: (real_inner, finite) real_inner |
423 begin |
421 begin |
424 |
422 |
425 definition inner_vector_def: |
423 definition "inner x y = setsum (\<lambda>i. inner (x$i) (y$i)) UNIV" |
426 "inner x y = setsum (\<lambda>i. inner (x$i) (y$i)) UNIV" |
|
427 |
424 |
428 instance proof |
425 instance proof |
429 fix r :: real and x y z :: "'a ^ 'b" |
426 fix r :: real and x y z :: "'a ^ 'b" |
430 show "inner x y = inner y x" |
427 show "inner x y = inner y x" |
431 unfolding inner_vector_def |
428 unfolding inner_vec_def |
432 by (simp add: inner_commute) |
429 by (simp add: inner_commute) |
433 show "inner (x + y) z = inner x z + inner y z" |
430 show "inner (x + y) z = inner x z + inner y z" |
434 unfolding inner_vector_def |
431 unfolding inner_vec_def |
435 by (simp add: inner_add_left setsum_addf) |
432 by (simp add: inner_add_left setsum_addf) |
436 show "inner (scaleR r x) y = r * inner x y" |
433 show "inner (scaleR r x) y = r * inner x y" |
437 unfolding inner_vector_def |
434 unfolding inner_vec_def |
438 by (simp add: setsum_right_distrib) |
435 by (simp add: setsum_right_distrib) |
439 show "0 \<le> inner x x" |
436 show "0 \<le> inner x x" |
440 unfolding inner_vector_def |
437 unfolding inner_vec_def |
441 by (simp add: setsum_nonneg) |
438 by (simp add: setsum_nonneg) |
442 show "inner x x = 0 \<longleftrightarrow> x = 0" |
439 show "inner x x = 0 \<longleftrightarrow> x = 0" |
443 unfolding inner_vector_def |
440 unfolding inner_vec_def |
444 by (simp add: Cart_eq setsum_nonneg_eq_0_iff) |
441 by (simp add: vec_eq_iff setsum_nonneg_eq_0_iff) |
445 show "norm x = sqrt (inner x x)" |
442 show "norm x = sqrt (inner x x)" |
446 unfolding inner_vector_def norm_vector_def setL2_def |
443 unfolding inner_vec_def norm_vec_def setL2_def |
447 by (simp add: power2_norm_eq_inner) |
444 by (simp add: power2_norm_eq_inner) |
448 qed |
445 qed |
449 |
446 |
450 end |
447 end |
451 |
448 |
452 subsection {* Euclidean space *} |
449 subsection {* Euclidean space *} |
453 |
450 |
454 text {* A bijection between @{text "'n::finite"} and @{text "{..<CARD('n)}"} *} |
451 text {* A bijection between @{text "'n::finite"} and @{text "{..<CARD('n)}"} *} |
455 |
452 |
456 definition cart_bij_nat :: "nat \<Rightarrow> ('n::finite)" where |
453 definition vec_bij_nat :: "nat \<Rightarrow> ('n::finite)" where |
457 "cart_bij_nat = (SOME p. bij_betw p {..<CARD('n)} (UNIV::'n set) )" |
454 "vec_bij_nat = (SOME p. bij_betw p {..<CARD('n)} (UNIV::'n set) )" |
458 |
455 |
459 abbreviation "\<pi> \<equiv> cart_bij_nat" |
456 abbreviation "\<pi> \<equiv> vec_bij_nat" |
460 definition "\<pi>' = inv_into {..<CARD('n)} (\<pi>::nat \<Rightarrow> ('n::finite))" |
457 definition "\<pi>' = inv_into {..<CARD('n)} (\<pi>::nat \<Rightarrow> ('n::finite))" |
461 |
458 |
462 lemma bij_betw_pi: |
459 lemma bij_betw_pi: |
463 "bij_betw \<pi> {..<CARD('n::finite)} (UNIV::('n::finite) set)" |
460 "bij_betw \<pi> {..<CARD('n::finite)} (UNIV::('n::finite) set)" |
464 using ex_bij_betw_nat_finite[of "UNIV::'n set"] |
461 using ex_bij_betw_nat_finite[of "UNIV::'n set"] |
465 by (auto simp: cart_bij_nat_def atLeast0LessThan |
462 by (auto simp: vec_bij_nat_def atLeast0LessThan |
466 intro!: someI_ex[of "\<lambda>x. bij_betw x {..<CARD('n)} (UNIV::'n set)"]) |
463 intro!: someI_ex[of "\<lambda>x. bij_betw x {..<CARD('n)} (UNIV::'n set)"]) |
467 |
464 |
468 lemma bij_betw_pi'[intro]: "bij_betw \<pi>' (UNIV::'n set) {..<CARD('n::finite)}" |
465 lemma bij_betw_pi'[intro]: "bij_betw \<pi>' (UNIV::'n set) {..<CARD('n::finite)}" |
469 using bij_betw_inv_into[OF bij_betw_pi] unfolding \<pi>'_def by auto |
466 using bij_betw_inv_into[OF bij_betw_pi] unfolding \<pi>'_def by auto |
470 |
467 |