author | blanchet |
Fri, 01 Aug 2014 14:43:57 +0200 | |
changeset 57743 | 0af2d5dfb0ac |
parent 57512 | cc97b347b301 |
child 58877 | 262572d90bc6 |
permissions | -rw-r--r-- |
35253 | 1 |
(* Title: HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy |
2 |
Author: Amine Chaieb, University of Cambridge |
|
33175 | 3 |
*) |
4 |
||
5 |
header {* Definition of finite Cartesian product types. *} |
|
6 |
||
7 |
theory Finite_Cartesian_Product |
|
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
39302
diff
changeset
|
8 |
imports |
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset
|
9 |
Euclidean_Space |
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
39302
diff
changeset
|
10 |
L2_Norm |
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
39302
diff
changeset
|
11 |
"~~/src/HOL/Library/Numeral_Type" |
33175 | 12 |
begin |
13 |
||
14 |
subsection {* Finite Cartesian products, with indexing and lambdas. *} |
|
15 |
||
49834 | 16 |
typedef ('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
17 |
morphisms vec_nth vec_lambda .. |
33175 | 18 |
|
35254
0f17eda72e60
binder notation for default print_mode -- to avoid strange output if "xsymbols" is not active;
wenzelm
parents:
35253
diff
changeset
|
19 |
notation |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
20 |
vec_nth (infixl "$" 90) and |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
21 |
vec_lambda (binder "\<chi>" 10) |
33175 | 22 |
|
34290
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
23 |
(* |
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34290
diff
changeset
|
24 |
Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
25 |
the finite type class write "vec 'b 'n" |
34290
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
26 |
*) |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
27 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
28 |
syntax "_finite_vec" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15) |
34290
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
29 |
|
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
30 |
parse_translation {* |
52143 | 31 |
let |
32 |
fun vec t u = Syntax.const @{type_syntax vec} $ t $ u; |
|
33 |
fun finite_vec_tr [t, u] = |
|
34 |
(case Term_Position.strip_positions u of |
|
35 |
v as Free (x, _) => |
|
36 |
if Lexicon.is_tid x then |
|
37 |
vec t (Syntax.const @{syntax_const "_ofsort"} $ v $ |
|
38 |
Syntax.const @{class_syntax finite}) |
|
39 |
else vec t u |
|
40 |
| _ => vec t u) |
|
41 |
in |
|
42 |
[(@{syntax_const "_finite_vec"}, K finite_vec_tr)] |
|
43 |
end |
|
34290
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
44 |
*} |
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset
|
45 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
46 |
lemma vec_eq_iff: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)" |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
47 |
by (simp add: vec_nth_inject [symmetric] fun_eq_iff) |
33175 | 48 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
49 |
lemma vec_lambda_beta [simp]: "vec_lambda g $ i = g i" |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
50 |
by (simp add: vec_lambda_inverse) |
33175 | 51 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
52 |
lemma vec_lambda_unique: "(\<forall>i. f$i = g i) \<longleftrightarrow> vec_lambda g = f" |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
53 |
by (auto simp add: vec_eq_iff) |
33175 | 54 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
55 |
lemma vec_lambda_eta: "(\<chi> i. (g$i)) = g" |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
56 |
by (simp add: vec_eq_iff) |
33175 | 57 |
|
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
58 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
59 |
subsection {* Group operations and class instances *} |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
60 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
61 |
instantiation vec :: (zero, finite) zero |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
62 |
begin |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
63 |
definition "0 \<equiv> (\<chi> i. 0)" |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
64 |
instance .. |
33175 | 65 |
end |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
66 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
67 |
instantiation vec :: (plus, finite) plus |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
68 |
begin |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
69 |
definition "op + \<equiv> (\<lambda> x y. (\<chi> i. x$i + y$i))" |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
70 |
instance .. |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
71 |
end |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
72 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
73 |
instantiation vec :: (minus, finite) minus |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
74 |
begin |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
75 |
definition "op - \<equiv> (\<lambda> x y. (\<chi> i. x$i - y$i))" |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
76 |
instance .. |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
77 |
end |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
78 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
79 |
instantiation vec :: (uminus, finite) uminus |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
80 |
begin |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
81 |
definition "uminus \<equiv> (\<lambda> x. (\<chi> i. - (x$i)))" |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
82 |
instance .. |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
83 |
end |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
84 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
85 |
lemma zero_index [simp]: "0 $ i = 0" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
86 |
unfolding zero_vec_def by simp |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
87 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
88 |
lemma vector_add_component [simp]: "(x + y)$i = x$i + y$i" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
89 |
unfolding plus_vec_def by simp |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
90 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
91 |
lemma vector_minus_component [simp]: "(x - y)$i = x$i - y$i" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
92 |
unfolding minus_vec_def by simp |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
93 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
94 |
lemma vector_uminus_component [simp]: "(- x)$i = - (x$i)" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
95 |
unfolding uminus_vec_def by simp |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
96 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
97 |
instance vec :: (semigroup_add, finite) semigroup_add |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
98 |
by default (simp add: vec_eq_iff add.assoc) |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
99 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
100 |
instance vec :: (ab_semigroup_add, finite) ab_semigroup_add |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
101 |
by default (simp add: vec_eq_iff add.commute) |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
102 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
103 |
instance vec :: (monoid_add, finite) monoid_add |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
104 |
by default (simp_all add: vec_eq_iff) |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
105 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
106 |
instance vec :: (comm_monoid_add, finite) comm_monoid_add |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
107 |
by default (simp add: vec_eq_iff) |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
108 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
109 |
instance vec :: (cancel_semigroup_add, finite) cancel_semigroup_add |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
110 |
by default (simp_all add: vec_eq_iff) |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
111 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
112 |
instance vec :: (cancel_ab_semigroup_add, finite) cancel_ab_semigroup_add |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
113 |
by default (simp add: vec_eq_iff) |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
114 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
115 |
instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add .. |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
116 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
117 |
instance vec :: (group_add, finite) group_add |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
52143
diff
changeset
|
118 |
by default (simp_all add: vec_eq_iff) |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
119 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
120 |
instance vec :: (ab_group_add, finite) ab_group_add |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
121 |
by default (simp_all add: vec_eq_iff) |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
122 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
123 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
124 |
subsection {* Real vector space *} |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
125 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
126 |
instantiation vec :: (real_vector, finite) real_vector |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
127 |
begin |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
128 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
129 |
definition "scaleR \<equiv> (\<lambda> r x. (\<chi> i. scaleR r (x$i)))" |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
130 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
131 |
lemma vector_scaleR_component [simp]: "(scaleR r x)$i = scaleR r (x$i)" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
132 |
unfolding scaleR_vec_def by simp |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
133 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
134 |
instance |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
135 |
by default (simp_all add: vec_eq_iff scaleR_left_distrib scaleR_right_distrib) |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
136 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
137 |
end |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
138 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
139 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
140 |
subsection {* Topological space *} |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
141 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
142 |
instantiation vec :: (topological_space, finite) topological_space |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
143 |
begin |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
144 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
145 |
definition |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
146 |
"open (S :: ('a ^ 'b) set) \<longleftrightarrow> |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
147 |
(\<forall>x\<in>S. \<exists>A. (\<forall>i. open (A i) \<and> x$i \<in> A i) \<and> |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
148 |
(\<forall>y. (\<forall>i. y$i \<in> A i) \<longrightarrow> y \<in> S))" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
149 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
150 |
instance proof |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
151 |
show "open (UNIV :: ('a ^ 'b) set)" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
152 |
unfolding open_vec_def by auto |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
153 |
next |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
154 |
fix S T :: "('a ^ 'b) set" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
155 |
assume "open S" "open T" thus "open (S \<inter> T)" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
156 |
unfolding open_vec_def |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
157 |
apply clarify |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
158 |
apply (drule (1) bspec)+ |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
159 |
apply (clarify, rename_tac Sa Ta) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
160 |
apply (rule_tac x="\<lambda>i. Sa i \<inter> Ta i" in exI) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
161 |
apply (simp add: open_Int) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
162 |
done |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
163 |
next |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
164 |
fix K :: "('a ^ 'b) set set" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
165 |
assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
166 |
unfolding open_vec_def |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
167 |
apply clarify |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
168 |
apply (drule (1) bspec) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
169 |
apply (drule (1) bspec) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
170 |
apply clarify |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
171 |
apply (rule_tac x=A in exI) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
172 |
apply fast |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
173 |
done |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
174 |
qed |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
175 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
176 |
end |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
177 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
178 |
lemma open_vector_box: "\<forall>i. open (S i) \<Longrightarrow> open {x. \<forall>i. x $ i \<in> S i}" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
179 |
unfolding open_vec_def by auto |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
180 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
181 |
lemma open_vimage_vec_nth: "open S \<Longrightarrow> open ((\<lambda>x. x $ i) -` S)" |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
182 |
unfolding open_vec_def |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
183 |
apply clarify |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
184 |
apply (rule_tac x="\<lambda>k. if k = i then S else UNIV" in exI, simp) |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
185 |
done |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
186 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
187 |
lemma closed_vimage_vec_nth: "closed S \<Longrightarrow> closed ((\<lambda>x. x $ i) -` S)" |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
188 |
unfolding closed_open vimage_Compl [symmetric] |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
189 |
by (rule open_vimage_vec_nth) |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
190 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
191 |
lemma closed_vector_box: "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
192 |
proof - |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
193 |
have "{x. \<forall>i. x $ i \<in> S i} = (\<Inter>i. (\<lambda>x. x $ i) -` S i)" by auto |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
194 |
thus "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
195 |
by (simp add: closed_INT closed_vimage_vec_nth) |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
196 |
qed |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
197 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
198 |
lemma tendsto_vec_nth [tendsto_intros]: |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
199 |
assumes "((\<lambda>x. f x) ---> a) net" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
200 |
shows "((\<lambda>x. f x $ i) ---> a $ i) net" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
201 |
proof (rule topological_tendstoI) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
202 |
fix S assume "open S" "a $ i \<in> S" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
203 |
then have "open ((\<lambda>y. y $ i) -` S)" "a \<in> ((\<lambda>y. y $ i) -` S)" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
204 |
by (simp_all add: open_vimage_vec_nth) |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
205 |
with assms have "eventually (\<lambda>x. f x \<in> (\<lambda>y. y $ i) -` S) net" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
206 |
by (rule topological_tendstoD) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
207 |
then show "eventually (\<lambda>x. f x $ i \<in> S) net" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
208 |
by simp |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
209 |
qed |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
210 |
|
44631 | 211 |
lemma isCont_vec_nth [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x $ i) a" |
212 |
unfolding isCont_def by (rule tendsto_vec_nth) |
|
213 |
||
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
214 |
lemma vec_tendstoI: |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
215 |
assumes "\<And>i. ((\<lambda>x. f x $ i) ---> a $ i) net" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
216 |
shows "((\<lambda>x. f x) ---> a) net" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
217 |
proof (rule topological_tendstoI) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
218 |
fix S assume "open S" and "a \<in> S" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
219 |
then obtain A where A: "\<And>i. open (A i)" "\<And>i. a $ i \<in> A i" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
220 |
and S: "\<And>y. \<forall>i. y $ i \<in> A i \<Longrightarrow> y \<in> S" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
221 |
unfolding open_vec_def by metis |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
222 |
have "\<And>i. eventually (\<lambda>x. f x $ i \<in> A i) net" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
223 |
using assms A by (rule topological_tendstoD) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
224 |
hence "eventually (\<lambda>x. \<forall>i. f x $ i \<in> A i) net" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
225 |
by (rule eventually_all_finite) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
226 |
thus "eventually (\<lambda>x. f x \<in> S) net" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
227 |
by (rule eventually_elim1, simp add: S) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
228 |
qed |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
229 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
230 |
lemma tendsto_vec_lambda [tendsto_intros]: |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
231 |
assumes "\<And>i. ((\<lambda>x. f x i) ---> a i) net" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
232 |
shows "((\<lambda>x. \<chi> i. f x i) ---> (\<chi> i. a i)) net" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
233 |
using assms by (simp add: vec_tendstoI) |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
234 |
|
44571 | 235 |
lemma open_image_vec_nth: assumes "open S" shows "open ((\<lambda>x. x $ i) ` S)" |
236 |
proof (rule openI) |
|
237 |
fix a assume "a \<in> (\<lambda>x. x $ i) ` 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" |
|
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 |
|
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, |
|
244 |
simp_all) |
|
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 |
|
247 |
then show "\<exists>T. open T \<and> a \<in> T \<and> T \<subseteq> (\<lambda>x. x $ i) ` S" by - (rule exI) |
|
248 |
qed |
|
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
249 |
|
44571 | 250 |
instance vec :: (perfect_space, finite) perfect_space |
251 |
proof |
|
252 |
fix x :: "'a ^ 'b" show "\<not> open {x}" |
|
253 |
proof |
|
254 |
assume "open {x}" |
|
255 |
hence "\<forall>i. open ((\<lambda>x. x $ i) ` {x})" by (fast intro: open_image_vec_nth) |
|
256 |
hence "\<forall>i. open {x $ i}" by simp |
|
257 |
thus "False" by (simp add: not_open_singleton) |
|
258 |
qed |
|
259 |
qed |
|
260 |
||
261 |
||
262 |
subsection {* Metric space *} |
|
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
263 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
264 |
instantiation vec :: (metric_space, finite) metric_space |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
265 |
begin |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
266 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
267 |
definition |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
268 |
"dist x y = setL2 (\<lambda>i. dist (x$i) (y$i)) UNIV" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
269 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
270 |
lemma dist_vec_nth_le: "dist (x $ i) (y $ i) \<le> dist x y" |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
271 |
unfolding dist_vec_def by (rule member_le_setL2) simp_all |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
272 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
273 |
instance proof |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
274 |
fix x y :: "'a ^ 'b" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
275 |
show "dist x y = 0 \<longleftrightarrow> x = y" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
276 |
unfolding dist_vec_def |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
277 |
by (simp add: setL2_eq_0_iff vec_eq_iff) |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
278 |
next |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
279 |
fix x y z :: "'a ^ 'b" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
280 |
show "dist x y \<le> dist x z + dist y z" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
281 |
unfolding dist_vec_def |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
282 |
apply (rule order_trans [OF _ setL2_triangle_ineq]) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
283 |
apply (simp add: setL2_mono dist_triangle2) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
284 |
done |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
285 |
next |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
286 |
fix S :: "('a ^ 'b) set" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
287 |
show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" |
44630 | 288 |
proof |
289 |
assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" |
|
290 |
proof |
|
291 |
fix x assume "x \<in> S" |
|
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" |
|
294 |
using `open S` and `x \<in> S` 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" |
|
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)" |
|
44681
49ef76b4a634
remove duplicate lemma finite_choice in favor of finite_set_choice
huffman
parents:
44631
diff
changeset
|
298 |
by (rule finite_set_choice [OF finite]) |
44630 | 299 |
then obtain r where r1: "\<forall>i. 0 < r i" |
300 |
and r2: "\<forall>i y. dist y (x $ i) < r i \<longrightarrow> y \<in> A i" by fast |
|
301 |
have "0 < Min (range r) \<and> (\<forall>y. dist y x < Min (range r) \<longrightarrow> y \<in> S)" |
|
302 |
by (simp add: r1 r2 S le_less_trans [OF dist_vec_nth_le]) |
|
303 |
thus "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" .. |
|
304 |
qed |
|
305 |
next |
|
306 |
assume *: "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" show "open S" |
|
307 |
proof (unfold open_vec_def, rule) |
|
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" |
|
310 |
using * by fast |
|
311 |
def r \<equiv> "\<lambda>i::'b. e / sqrt (of_nat CARD('b))" |
|
312 |
from `0 < e` have r: "\<forall>i. 0 < r i" |
|
56541 | 313 |
unfolding r_def by simp_all |
44630 | 314 |
from `0 < e` have e: "e = setL2 r UNIV" |
315 |
unfolding r_def by (simp add: setL2_constant) |
|
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" |
|
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" |
|
320 |
by (simp add: A_def S dist_vec_def e setL2_strict_mono dist_commute) |
|
321 |
ultimately show "\<exists>A. (\<forall>i. open (A i) \<and> x $ i \<in> A i) \<and> |
|
322 |
(\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S)" by metis |
|
323 |
qed |
|
324 |
qed |
|
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
325 |
qed |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
326 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
327 |
end |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
328 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
329 |
lemma Cauchy_vec_nth: |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
330 |
"Cauchy (\<lambda>n. X n) \<Longrightarrow> Cauchy (\<lambda>n. X n $ i)" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
331 |
unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_vec_nth_le]) |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
332 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
333 |
lemma vec_CauchyI: |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
334 |
fixes X :: "nat \<Rightarrow> 'a::metric_space ^ 'n" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
335 |
assumes X: "\<And>i. Cauchy (\<lambda>n. X n $ i)" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
336 |
shows "Cauchy (\<lambda>n. X n)" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
337 |
proof (rule metric_CauchyI) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
338 |
fix r :: real assume "0 < r" |
56541 | 339 |
hence "0 < r / of_nat CARD('n)" (is "0 < ?s") by simp |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
340 |
def N \<equiv> "\<lambda>i. LEAST N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
341 |
def M \<equiv> "Max (range N)" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
342 |
have "\<And>i. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
343 |
using X `0 < ?s` by (rule metric_CauchyD) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
344 |
hence "\<And>i. \<forall>m\<ge>N i. \<forall>n\<ge>N i. dist (X m $ i) (X n $ i) < ?s" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
345 |
unfolding N_def by (rule LeastI_ex) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
346 |
hence M: "\<And>i. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m $ i) (X n $ i) < ?s" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
347 |
unfolding M_def by simp |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
348 |
{ |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
349 |
fix m n :: nat |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
350 |
assume "M \<le> m" "M \<le> n" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
351 |
have "dist (X m) (X n) = setL2 (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
352 |
unfolding dist_vec_def .. |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
353 |
also have "\<dots> \<le> setsum (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
354 |
by (rule setL2_le_setsum [OF zero_le_dist]) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
355 |
also have "\<dots> < setsum (\<lambda>i::'n. ?s) UNIV" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
356 |
by (rule setsum_strict_mono, simp_all add: M `M \<le> m` `M \<le> n`) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
357 |
also have "\<dots> = r" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
358 |
by simp |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
359 |
finally have "dist (X m) (X n) < r" . |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
360 |
} |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
361 |
hence "\<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
362 |
by simp |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
363 |
then show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (X m) (X n) < r" .. |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
364 |
qed |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
365 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
366 |
instance vec :: (complete_space, finite) complete_space |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
367 |
proof |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
368 |
fix X :: "nat \<Rightarrow> 'a ^ 'b" assume "Cauchy X" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
369 |
have "\<And>i. (\<lambda>n. X n $ i) ----> lim (\<lambda>n. X n $ i)" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
370 |
using Cauchy_vec_nth [OF `Cauchy X`] |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
371 |
by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
372 |
hence "X ----> vec_lambda (\<lambda>i. lim (\<lambda>n. X n $ i))" |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
373 |
by (simp add: vec_tendstoI) |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
374 |
then show "convergent X" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
375 |
by (rule convergentI) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
376 |
qed |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
377 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
378 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
379 |
subsection {* Normed vector space *} |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
380 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
381 |
instantiation vec :: (real_normed_vector, finite) real_normed_vector |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
382 |
begin |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
383 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
384 |
definition "norm x = setL2 (\<lambda>i. norm (x$i)) UNIV" |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
385 |
|
44141 | 386 |
definition "sgn (x::'a^'b) = scaleR (inverse (norm x)) x" |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
387 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
388 |
instance proof |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
389 |
fix a :: real and x y :: "'a ^ 'b" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
390 |
show "norm x = 0 \<longleftrightarrow> x = 0" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
391 |
unfolding norm_vec_def |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
392 |
by (simp add: setL2_eq_0_iff vec_eq_iff) |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
393 |
show "norm (x + y) \<le> norm x + norm y" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
394 |
unfolding norm_vec_def |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
395 |
apply (rule order_trans [OF _ setL2_triangle_ineq]) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
396 |
apply (simp add: setL2_mono norm_triangle_ineq) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
397 |
done |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
398 |
show "norm (scaleR a x) = \<bar>a\<bar> * norm x" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
399 |
unfolding norm_vec_def |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
400 |
by (simp add: setL2_right_distrib) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
401 |
show "sgn x = scaleR (inverse (norm x)) x" |
44141 | 402 |
by (rule sgn_vec_def) |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
403 |
show "dist x y = norm (x - y)" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
404 |
unfolding dist_vec_def norm_vec_def |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
405 |
by (simp add: dist_norm) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
406 |
qed |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
407 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
408 |
end |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
409 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
410 |
lemma norm_nth_le: "norm (x $ i) \<le> norm x" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
411 |
unfolding norm_vec_def |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
412 |
by (rule member_le_setL2) simp_all |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
413 |
|
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset
|
414 |
lemma bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)" |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
415 |
apply default |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
416 |
apply (rule vector_add_component) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
417 |
apply (rule vector_scaleR_component) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
418 |
apply (rule_tac x="1" in exI, simp add: norm_nth_le) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
419 |
done |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
420 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
421 |
instance vec :: (banach, finite) banach .. |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
422 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
423 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
424 |
subsection {* Inner product space *} |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
425 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
426 |
instantiation vec :: (real_inner, finite) real_inner |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
427 |
begin |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
428 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
429 |
definition "inner x y = setsum (\<lambda>i. inner (x$i) (y$i)) UNIV" |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
430 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
431 |
instance proof |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
432 |
fix r :: real and x y z :: "'a ^ 'b" |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
433 |
show "inner x y = inner y x" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
434 |
unfolding inner_vec_def |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
435 |
by (simp add: inner_commute) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
436 |
show "inner (x + y) z = inner x z + inner y z" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
437 |
unfolding inner_vec_def |
57418 | 438 |
by (simp add: inner_add_left setsum.distrib) |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
439 |
show "inner (scaleR r x) y = r * inner x y" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
440 |
unfolding inner_vec_def |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
441 |
by (simp add: setsum_right_distrib) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
442 |
show "0 \<le> inner x x" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
443 |
unfolding inner_vec_def |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
444 |
by (simp add: setsum_nonneg) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
445 |
show "inner x x = 0 \<longleftrightarrow> x = 0" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
446 |
unfolding inner_vec_def |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
447 |
by (simp add: vec_eq_iff setsum_nonneg_eq_0_iff) |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
448 |
show "norm x = sqrt (inner x x)" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
449 |
unfolding inner_vec_def norm_vec_def setL2_def |
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
450 |
by (simp add: power2_norm_eq_inner) |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
451 |
qed |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
452 |
|
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
453 |
end |
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
454 |
|
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
455 |
|
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset
|
456 |
subsection {* Euclidean space *} |
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset
|
457 |
|
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
458 |
text {* Vectors pointing along a single axis. *} |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
459 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
460 |
definition "axis k x = (\<chi> i. if i = k then x else 0)" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
461 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
462 |
lemma axis_nth [simp]: "axis i x $ i = x" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
463 |
unfolding axis_def by simp |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
464 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
465 |
lemma axis_eq_axis: "axis i x = axis j y \<longleftrightarrow> x = y \<and> i = j \<or> x = 0 \<and> y = 0" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
466 |
unfolding axis_def vec_eq_iff by auto |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
467 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
468 |
lemma inner_axis_axis: |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
469 |
"inner (axis i x) (axis j y) = (if i = j then inner x y else 0)" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
470 |
unfolding inner_vec_def |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
471 |
apply (cases "i = j") |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
472 |
apply clarsimp |
57418 | 473 |
apply (subst setsum.remove [of _ j], simp_all) |
474 |
apply (rule setsum.neutral, simp add: axis_def) |
|
475 |
apply (rule setsum.neutral, simp add: axis_def) |
|
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
476 |
done |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
477 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
478 |
lemma setsum_single: |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
479 |
assumes "finite A" and "k \<in> A" and "f k = y" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
480 |
assumes "\<And>i. i \<in> A \<Longrightarrow> i \<noteq> k \<Longrightarrow> f i = 0" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
481 |
shows "(\<Sum>i\<in>A. f i) = y" |
57418 | 482 |
apply (subst setsum.remove [OF assms(1,2)]) |
483 |
apply (simp add: setsum.neutral assms(3,4)) |
|
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
484 |
done |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
485 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
486 |
lemma inner_axis: "inner x (axis i y) = inner (x $ i) y" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
487 |
unfolding inner_vec_def |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
488 |
apply (rule_tac k=i in setsum_single) |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
489 |
apply simp_all |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
490 |
apply (simp add: axis_def) |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
491 |
done |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
492 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
493 |
instantiation vec :: (euclidean_space, finite) euclidean_space |
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset
|
494 |
begin |
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset
|
495 |
|
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
496 |
definition "Basis = (\<Union>i. \<Union>u\<in>Basis. {axis i u})" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
497 |
|
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset
|
498 |
instance proof |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
499 |
show "(Basis :: ('a ^ 'b) set) \<noteq> {}" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
500 |
unfolding Basis_vec_def by simp |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
501 |
next |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
502 |
show "finite (Basis :: ('a ^ 'b) set)" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
503 |
unfolding Basis_vec_def by simp |
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset
|
504 |
next |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
505 |
fix u v :: "'a ^ 'b" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
506 |
assume "u \<in> Basis" and "v \<in> Basis" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
507 |
thus "inner u v = (if u = v then 1 else 0)" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
508 |
unfolding Basis_vec_def |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
509 |
by (auto simp add: inner_axis_axis axis_eq_axis inner_Basis) |
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset
|
510 |
next |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
511 |
fix x :: "'a ^ 'b" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
512 |
show "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> x = 0" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
513 |
unfolding Basis_vec_def |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
514 |
by (simp add: inner_axis euclidean_all_zero_iff vec_eq_iff) |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50252
diff
changeset
|
515 |
qed |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50252
diff
changeset
|
516 |
|
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50252
diff
changeset
|
517 |
lemma DIM_cart[simp]: "DIM('a^'b) = CARD('b) * DIM('a)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50252
diff
changeset
|
518 |
apply (simp add: Basis_vec_def) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50252
diff
changeset
|
519 |
apply (subst card_UN_disjoint) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50252
diff
changeset
|
520 |
apply simp |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset
|
521 |
apply simp |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50252
diff
changeset
|
522 |
apply (auto simp: axis_eq_axis) [1] |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50252
diff
changeset
|
523 |
apply (subst card_UN_disjoint) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50252
diff
changeset
|
524 |
apply (auto simp: axis_eq_axis) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50252
diff
changeset
|
525 |
done |
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset
|
526 |
|
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset
|
527 |
end |
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset
|
528 |
|
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset
|
529 |
end |