1 (* Title: HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy |
1 (* Title: HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy |
2 Author: Amine Chaieb, University of Cambridge |
2 Author: Amine Chaieb, University of Cambridge |
3 *) |
3 *) |
4 |
4 |
5 section {* Definition of finite Cartesian product types. *} |
5 section \<open>Definition of finite Cartesian product types.\<close> |
6 |
6 |
7 theory Finite_Cartesian_Product |
7 theory Finite_Cartesian_Product |
8 imports |
8 imports |
9 Euclidean_Space |
9 Euclidean_Space |
10 L2_Norm |
10 L2_Norm |
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 \<open>Finite Cartesian products, with indexing and lambdas.\<close> |
15 |
15 |
16 typedef ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set" |
16 typedef ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set" |
17 morphisms vec_nth vec_lambda .. |
17 morphisms vec_nth vec_lambda .. |
18 |
18 |
19 notation |
19 notation |
25 the finite type class write "vec 'b 'n" |
25 the finite type class write "vec 'b 'n" |
26 *) |
26 *) |
27 |
27 |
28 syntax "_finite_vec" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15) |
28 syntax "_finite_vec" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15) |
29 |
29 |
30 parse_translation {* |
30 parse_translation \<open> |
31 let |
31 let |
32 fun vec t u = Syntax.const @{type_syntax vec} $ t $ u; |
32 fun vec t u = Syntax.const @{type_syntax vec} $ t $ u; |
33 fun finite_vec_tr [t, u] = |
33 fun finite_vec_tr [t, u] = |
34 (case Term_Position.strip_positions u of |
34 (case Term_Position.strip_positions u of |
35 v as Free (x, _) => |
35 v as Free (x, _) => |
39 else vec t u |
39 else vec t u |
40 | _ => vec t u) |
40 | _ => vec t u) |
41 in |
41 in |
42 [(@{syntax_const "_finite_vec"}, K finite_vec_tr)] |
42 [(@{syntax_const "_finite_vec"}, K finite_vec_tr)] |
43 end |
43 end |
44 *} |
44 \<close> |
45 |
45 |
46 lemma vec_eq_iff: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)" |
46 lemma vec_eq_iff: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)" |
47 by (simp add: vec_nth_inject [symmetric] fun_eq_iff) |
47 by (simp add: vec_nth_inject [symmetric] fun_eq_iff) |
48 |
48 |
49 lemma vec_lambda_beta [simp]: "vec_lambda g $ i = g i" |
49 lemma vec_lambda_beta [simp]: "vec_lambda g $ i = g i" |
54 |
54 |
55 lemma vec_lambda_eta: "(\<chi> i. (g$i)) = g" |
55 lemma vec_lambda_eta: "(\<chi> i. (g$i)) = g" |
56 by (simp add: vec_eq_iff) |
56 by (simp add: vec_eq_iff) |
57 |
57 |
58 |
58 |
59 subsection {* Group operations and class instances *} |
59 subsection \<open>Group operations and class instances\<close> |
60 |
60 |
61 instantiation vec :: (zero, finite) zero |
61 instantiation vec :: (zero, finite) zero |
62 begin |
62 begin |
63 definition "0 \<equiv> (\<chi> i. 0)" |
63 definition "0 \<equiv> (\<chi> i. 0)" |
64 instance .. |
64 instance .. |
119 |
119 |
120 instance vec :: (ab_group_add, finite) ab_group_add |
120 instance vec :: (ab_group_add, finite) ab_group_add |
121 by default (simp_all add: vec_eq_iff) |
121 by default (simp_all add: vec_eq_iff) |
122 |
122 |
123 |
123 |
124 subsection {* Real vector space *} |
124 subsection \<open>Real vector space\<close> |
125 |
125 |
126 instantiation vec :: (real_vector, finite) real_vector |
126 instantiation vec :: (real_vector, finite) real_vector |
127 begin |
127 begin |
128 |
128 |
129 definition "scaleR \<equiv> (\<lambda> r x. (\<chi> i. scaleR r (x$i)))" |
129 definition "scaleR \<equiv> (\<lambda> r x. (\<chi> i. scaleR r (x$i)))" |
236 proof (rule openI) |
236 proof (rule openI) |
237 fix a assume "a \<in> (\<lambda>x. x $ i) ` S" |
237 fix a assume "a \<in> (\<lambda>x. x $ i) ` S" |
238 then obtain z where "a = z $ i" and "z \<in> S" .. |
238 then obtain z where "a = z $ i" and "z \<in> S" .. |
239 then obtain A where A: "\<forall>i. open (A i) \<and> z $ i \<in> A i" |
239 then obtain A where A: "\<forall>i. open (A i) \<and> z $ i \<in> A i" |
240 and S: "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S" |
240 and S: "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S" |
241 using `open S` unfolding open_vec_def by auto |
241 using \<open>open S\<close> unfolding open_vec_def by auto |
242 hence "A i \<subseteq> (\<lambda>x. x $ i) ` S" |
242 hence "A i \<subseteq> (\<lambda>x. x $ i) ` S" |
243 by (clarsimp, rule_tac x="\<chi> j. if j = i then x else z $ j" in image_eqI, |
243 by (clarsimp, rule_tac x="\<chi> j. if j = i then x else z $ j" in image_eqI, |
244 simp_all) |
244 simp_all) |
245 hence "open (A i) \<and> a \<in> A i \<and> A i \<subseteq> (\<lambda>x. x $ i) ` S" |
245 hence "open (A i) \<and> a \<in> A i \<and> A i \<subseteq> (\<lambda>x. x $ i) ` S" |
246 using A `a = z $ i` by simp |
246 using A \<open>a = z $ i\<close> by simp |
247 then show "\<exists>T. open T \<and> a \<in> T \<and> T \<subseteq> (\<lambda>x. x $ i) ` S" by - (rule exI) |
247 then show "\<exists>T. open T \<and> a \<in> T \<and> T \<subseteq> (\<lambda>x. x $ i) ` S" by - (rule exI) |
248 qed |
248 qed |
249 |
249 |
250 instance vec :: (perfect_space, finite) perfect_space |
250 instance vec :: (perfect_space, finite) perfect_space |
251 proof |
251 proof |
289 assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" |
289 assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" |
290 proof |
290 proof |
291 fix x assume "x \<in> S" |
291 fix x assume "x \<in> S" |
292 obtain A where A: "\<forall>i. open (A i)" "\<forall>i. x $ i \<in> A i" |
292 obtain A where A: "\<forall>i. open (A i)" "\<forall>i. x $ i \<in> A i" |
293 and S: "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S" |
293 and S: "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S" |
294 using `open S` and `x \<in> S` unfolding open_vec_def by metis |
294 using \<open>open S\<close> and \<open>x \<in> S\<close> unfolding open_vec_def by metis |
295 have "\<forall>i\<in>UNIV. \<exists>r>0. \<forall>y. dist y (x $ i) < r \<longrightarrow> y \<in> A i" |
295 have "\<forall>i\<in>UNIV. \<exists>r>0. \<forall>y. dist y (x $ i) < r \<longrightarrow> y \<in> A i" |
296 using A unfolding open_dist by simp |
296 using A unfolding open_dist by simp |
297 hence "\<exists>r. \<forall>i\<in>UNIV. 0 < r i \<and> (\<forall>y. dist y (x $ i) < r i \<longrightarrow> y \<in> A i)" |
297 hence "\<exists>r. \<forall>i\<in>UNIV. 0 < r i \<and> (\<forall>y. dist y (x $ i) < r i \<longrightarrow> y \<in> A i)" |
298 by (rule finite_set_choice [OF finite]) |
298 by (rule finite_set_choice [OF finite]) |
299 then obtain r where r1: "\<forall>i. 0 < r i" |
299 then obtain r where r1: "\<forall>i. 0 < r i" |
307 proof (unfold open_vec_def, rule) |
307 proof (unfold open_vec_def, rule) |
308 fix x assume "x \<in> S" |
308 fix x assume "x \<in> S" |
309 then obtain e where "0 < e" and S: "\<forall>y. dist y x < e \<longrightarrow> y \<in> S" |
309 then obtain e where "0 < e" and S: "\<forall>y. dist y x < e \<longrightarrow> y \<in> S" |
310 using * by fast |
310 using * by fast |
311 def r \<equiv> "\<lambda>i::'b. e / sqrt (of_nat CARD('b))" |
311 def r \<equiv> "\<lambda>i::'b. e / sqrt (of_nat CARD('b))" |
312 from `0 < e` have r: "\<forall>i. 0 < r i" |
312 from \<open>0 < e\<close> have r: "\<forall>i. 0 < r i" |
313 unfolding r_def by simp_all |
313 unfolding r_def by simp_all |
314 from `0 < e` have e: "e = setL2 r UNIV" |
314 from \<open>0 < e\<close> have e: "e = setL2 r UNIV" |
315 unfolding r_def by (simp add: setL2_constant) |
315 unfolding r_def by (simp add: setL2_constant) |
316 def A \<equiv> "\<lambda>i. {y. dist (x $ i) y < r i}" |
316 def A \<equiv> "\<lambda>i. {y. dist (x $ i) y < r i}" |
317 have "\<forall>i. open (A i) \<and> x $ i \<in> A i" |
317 have "\<forall>i. open (A i) \<and> x $ i \<in> A i" |
318 unfolding A_def by (simp add: open_ball r) |
318 unfolding A_def by (simp add: open_ball r) |
319 moreover have "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S" |
319 moreover have "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S" |
338 fix r :: real assume "0 < r" |
338 fix r :: real assume "0 < r" |
339 hence "0 < r / of_nat CARD('n)" (is "0 < ?s") by simp |
339 hence "0 < r / of_nat CARD('n)" (is "0 < ?s") by simp |
340 def N \<equiv> "\<lambda>i. LEAST N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s" |
340 def N \<equiv> "\<lambda>i. LEAST N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s" |
341 def M \<equiv> "Max (range N)" |
341 def M \<equiv> "Max (range N)" |
342 have "\<And>i. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s" |
342 have "\<And>i. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s" |
343 using X `0 < ?s` by (rule metric_CauchyD) |
343 using X \<open>0 < ?s\<close> by (rule metric_CauchyD) |
344 hence "\<And>i. \<forall>m\<ge>N i. \<forall>n\<ge>N i. dist (X m $ i) (X n $ i) < ?s" |
344 hence "\<And>i. \<forall>m\<ge>N i. \<forall>n\<ge>N i. dist (X m $ i) (X n $ i) < ?s" |
345 unfolding N_def by (rule LeastI_ex) |
345 unfolding N_def by (rule LeastI_ex) |
346 hence M: "\<And>i. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m $ i) (X n $ i) < ?s" |
346 hence M: "\<And>i. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m $ i) (X n $ i) < ?s" |
347 unfolding M_def by simp |
347 unfolding M_def by simp |
348 { |
348 { |
351 have "dist (X m) (X n) = setL2 (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV" |
351 have "dist (X m) (X n) = setL2 (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV" |
352 unfolding dist_vec_def .. |
352 unfolding dist_vec_def .. |
353 also have "\<dots> \<le> setsum (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV" |
353 also have "\<dots> \<le> setsum (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV" |
354 by (rule setL2_le_setsum [OF zero_le_dist]) |
354 by (rule setL2_le_setsum [OF zero_le_dist]) |
355 also have "\<dots> < setsum (\<lambda>i::'n. ?s) UNIV" |
355 also have "\<dots> < setsum (\<lambda>i::'n. ?s) UNIV" |
356 by (rule setsum_strict_mono, simp_all add: M `M \<le> m` `M \<le> n`) |
356 by (rule setsum_strict_mono, simp_all add: M \<open>M \<le> m\<close> \<open>M \<le> n\<close>) |
357 also have "\<dots> = r" |
357 also have "\<dots> = r" |
358 by simp |
358 by simp |
359 finally have "dist (X m) (X n) < r" . |
359 finally have "dist (X m) (X n) < r" . |
360 } |
360 } |
361 hence "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r" |
361 hence "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r" |
365 |
365 |
366 instance vec :: (complete_space, finite) complete_space |
366 instance vec :: (complete_space, finite) complete_space |
367 proof |
367 proof |
368 fix X :: "nat \<Rightarrow> 'a ^ 'b" assume "Cauchy X" |
368 fix X :: "nat \<Rightarrow> 'a ^ 'b" assume "Cauchy X" |
369 have "\<And>i. (\<lambda>n. X n $ i) ----> lim (\<lambda>n. X n $ i)" |
369 have "\<And>i. (\<lambda>n. X n $ i) ----> lim (\<lambda>n. X n $ i)" |
370 using Cauchy_vec_nth [OF `Cauchy X`] |
370 using Cauchy_vec_nth [OF \<open>Cauchy X\<close>] |
371 by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) |
371 by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) |
372 hence "X ----> vec_lambda (\<lambda>i. lim (\<lambda>n. X n $ i))" |
372 hence "X ----> vec_lambda (\<lambda>i. lim (\<lambda>n. X n $ i))" |
373 by (simp add: vec_tendstoI) |
373 by (simp add: vec_tendstoI) |
374 then show "convergent X" |
374 then show "convergent X" |
375 by (rule convergentI) |
375 by (rule convergentI) |
376 qed |
376 qed |
377 |
377 |
378 |
378 |
379 subsection {* Normed vector space *} |
379 subsection \<open>Normed vector space\<close> |
380 |
380 |
381 instantiation vec :: (real_normed_vector, finite) real_normed_vector |
381 instantiation vec :: (real_normed_vector, finite) real_normed_vector |
382 begin |
382 begin |
383 |
383 |
384 definition "norm x = setL2 (\<lambda>i. norm (x$i)) UNIV" |
384 definition "norm x = setL2 (\<lambda>i. norm (x$i)) UNIV" |
419 done |
419 done |
420 |
420 |
421 instance vec :: (banach, finite) banach .. |
421 instance vec :: (banach, finite) banach .. |
422 |
422 |
423 |
423 |
424 subsection {* Inner product space *} |
424 subsection \<open>Inner product space\<close> |
425 |
425 |
426 instantiation vec :: (real_inner, finite) real_inner |
426 instantiation vec :: (real_inner, finite) real_inner |
427 begin |
427 begin |
428 |
428 |
429 definition "inner x y = setsum (\<lambda>i. inner (x$i) (y$i)) UNIV" |
429 definition "inner x y = setsum (\<lambda>i. inner (x$i) (y$i)) UNIV" |
451 qed |
451 qed |
452 |
452 |
453 end |
453 end |
454 |
454 |
455 |
455 |
456 subsection {* Euclidean space *} |
456 subsection \<open>Euclidean space\<close> |
457 |
457 |
458 text {* Vectors pointing along a single axis. *} |
458 text \<open>Vectors pointing along a single axis.\<close> |
459 |
459 |
460 definition "axis k x = (\<chi> i. if i = k then x else 0)" |
460 definition "axis k x = (\<chi> i. if i = k then x else 0)" |
461 |
461 |
462 lemma axis_nth [simp]: "axis i x $ i = x" |
462 lemma axis_nth [simp]: "axis i x $ i = x" |
463 unfolding axis_def by simp |
463 unfolding axis_def by simp |