author  huffman 
Wed, 10 Aug 2011 13:13:37 0700  
changeset 44136  e63ad7d5158d 
parent 44135  18b4ab6854f1 
child 44141  0697c01ff3ea 
permissions  rwrr 
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 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

16 
typedef (open) 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

17 
('a, 'b) vec = "UNIV :: (('b::finite) \<Rightarrow> 'a) set" 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

18 
morphisms vec_nth vec_lambda .. 
33175  19 

35254
0f17eda72e60
binder notation for default print_mode  to avoid strange output if "xsymbols" is not active;
wenzelm
parents:
35253
diff
changeset

20 
notation 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

21 
vec_nth (infixl "$" 90) and 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

22 
vec_lambda (binder "\<chi>" 10) 
33175  23 

34290
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset

24 
(* 
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34290
diff
changeset

25 
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

26 
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

27 
*) 
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset

28 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

29 
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

30 

1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset

31 
parse_translation {* 
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset

32 
let 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

33 
fun vec t u = Syntax.const @{type_syntax vec} $ t $ u; 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

34 
fun finite_vec_tr [t, u as Free (x, _)] = 
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
41413
diff
changeset

35 
if Lexicon.is_tid x then 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

36 
vec t (Syntax.const @{syntax_const "_ofsort"} $ u $ Syntax.const @{class_syntax finite}) 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

37 
else vec t u 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

38 
 finite_vec_tr [t, u] = vec t u 
34290
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset

39 
in 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

40 
[(@{syntax_const "_finite_vec"}, finite_vec_tr)] 
34290
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset

41 
end 
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset

42 
*} 
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset

43 

33175  44 
lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)" 
35253  45 
by (auto intro: ext) 
33175  46 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

47 
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

48 
by (simp add: vec_nth_inject [symmetric] fun_eq_iff) 
33175  49 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

50 
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

51 
by (simp add: vec_lambda_inverse) 
33175  52 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

53 
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

54 
by (auto simp add: vec_eq_iff) 
33175  55 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

56 
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

57 
by (simp add: vec_eq_iff) 
33175  58 

36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

59 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

60 
subsection {* Group operations and class instances *} 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

61 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

62 
instantiation vec :: (zero, finite) zero 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

63 
begin 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

64 
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

65 
instance .. 
33175  66 
end 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

67 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

68 
instantiation vec :: (plus, finite) plus 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

69 
begin 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

70 
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

71 
instance .. 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

72 
end 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

73 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

74 
instantiation vec :: (minus, finite) minus 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

75 
begin 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

76 
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

77 
instance .. 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

78 
end 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

79 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

80 
instantiation vec :: (uminus, finite) uminus 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

81 
begin 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

82 
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

83 
instance .. 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

84 
end 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

85 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

86 
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

87 
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

88 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

89 
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

90 
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

91 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

92 
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

93 
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

94 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

95 
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

96 
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

97 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

98 
instance vec :: (semigroup_add, finite) semigroup_add 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

99 
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

100 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

101 
instance vec :: (ab_semigroup_add, finite) ab_semigroup_add 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

102 
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

103 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

104 
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

105 
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

106 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

107 
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

108 
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

109 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

110 
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

111 
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

112 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

113 
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

114 
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

115 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

116 
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

117 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

118 
instance vec :: (group_add, finite) group_add 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

119 
by default (simp_all add: vec_eq_iff diff_minus) 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

120 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

121 
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

122 
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

123 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

124 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

125 
subsection {* Real vector space *} 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

126 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

127 
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

128 
begin 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

129 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

130 
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

131 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

132 
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

133 
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

134 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

135 
instance 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

136 
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

137 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

138 
end 
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 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

141 
subsection {* Topological space *} 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

142 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

143 
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

144 
begin 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

145 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

146 
definition 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

147 
"open (S :: ('a ^ 'b) set) \<longleftrightarrow> 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

148 
(\<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

149 
(\<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

150 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

151 
instance proof 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

152 
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

153 
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

154 
next 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

155 
fix S T :: "('a ^ 'b) set" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

156 
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

157 
unfolding open_vec_def 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

158 
apply clarify 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

159 
apply (drule (1) bspec)+ 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

160 
apply (clarify, rename_tac Sa Ta) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

161 
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

162 
apply (simp add: open_Int) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

163 
done 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

164 
next 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

165 
fix K :: "('a ^ 'b) set set" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

166 
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

167 
unfolding open_vec_def 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

168 
apply clarify 
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 (drule (1) bspec) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

171 
apply clarify 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

172 
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

173 
apply fast 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

174 
done 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

175 
qed 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

176 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

177 
end 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

178 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

179 
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

180 
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

181 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

182 
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

183 
unfolding open_vec_def 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

184 
apply clarify 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

185 
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

186 
done 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

187 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

188 
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

189 
unfolding closed_open vimage_Compl [symmetric] 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

190 
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

191 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

192 
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

193 
proof  
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

194 
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

195 
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

196 
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

197 
qed 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

198 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

199 
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

200 
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

201 
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

202 
proof (rule topological_tendstoI) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

203 
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

204 
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

205 
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

206 
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

207 
by (rule topological_tendstoD) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

208 
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

209 
by simp 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

210 
qed 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

211 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

212 
lemma eventually_Ball_finite: (* TODO: move *) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

213 
assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

214 
shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

215 
using assms by (induct set: finite, simp, simp add: eventually_conj) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

216 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

217 
lemma eventually_all_finite: (* TODO: move *) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

218 
fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

219 
assumes "\<And>y. eventually (\<lambda>x. P x y) net" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

220 
shows "eventually (\<lambda>x. \<forall>y. P x y) net" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

221 
using eventually_Ball_finite [of UNIV P] assms by simp 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

222 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

223 
lemma vec_tendstoI: 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

224 
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

225 
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

226 
proof (rule topological_tendstoI) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

227 
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

228 
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

229 
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

230 
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

231 
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

232 
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

233 
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

234 
by (rule eventually_all_finite) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

235 
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

236 
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

237 
qed 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

238 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

239 
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

240 
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

241 
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

242 
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

243 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

244 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

245 
subsection {* Metric *} 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

246 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

247 
(* TODO: move somewhere else *) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

248 
lemma finite_choice: "finite A \<Longrightarrow> \<forall>x\<in>A. \<exists>y. P x y \<Longrightarrow> \<exists>f. \<forall>x\<in>A. P x (f x)" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

249 
apply (induct set: finite, simp_all) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

250 
apply (clarify, rename_tac y) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

251 
apply (rule_tac x="f(x:=y)" in exI, simp) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

252 
done 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

253 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

254 
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

255 
begin 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

256 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

257 
definition 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

258 
"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

259 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

260 
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

261 
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

262 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

263 
instance proof 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

264 
fix x y :: "'a ^ 'b" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

265 
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

266 
unfolding dist_vec_def 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

267 
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

268 
next 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

269 
fix x y z :: "'a ^ 'b" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

270 
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

271 
unfolding dist_vec_def 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

272 
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

273 
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

274 
done 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

275 
next 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

276 
(* FIXME: long proof! *) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

277 
fix S :: "('a ^ 'b) set" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

278 
show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

279 
unfolding open_vec_def open_dist 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

280 
apply safe 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

281 
apply (drule (1) bspec) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

282 
apply clarify 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

283 
apply (subgoal_tac "\<exists>e>0. \<forall>i y. dist y (x$i) < e \<longrightarrow> y \<in> A i") 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

284 
apply clarify 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

285 
apply (rule_tac x=e in exI, clarify) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

286 
apply (drule spec, erule mp, clarify) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

287 
apply (drule spec, drule spec, erule mp) 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

288 
apply (erule 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

289 
apply (subgoal_tac "\<forall>i\<in>UNIV. \<exists>e>0. \<forall>y. dist y (x$i) < e \<longrightarrow> y \<in> A i") 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

290 
apply (drule finite_choice [OF finite], clarify) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

291 
apply (rule_tac x="Min (range f)" in exI, simp) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

292 
apply clarify 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

293 
apply (drule_tac x=i in spec, clarify) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

294 
apply (erule (1) bspec) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

295 
apply (drule (1) bspec, clarify) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

296 
apply (subgoal_tac "\<exists>r. (\<forall>i::'b. 0 < r i) \<and> e = setL2 r UNIV") 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

297 
apply clarify 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

298 
apply (rule_tac x="\<lambda>i. {y. dist y (x$i) < r i}" in exI) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

299 
apply (rule conjI) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

300 
apply clarify 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

301 
apply (rule conjI) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

302 
apply (clarify, rename_tac y) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

303 
apply (rule_tac x="r i  dist y (x$i)" in exI, rule conjI, simp) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

304 
apply clarify 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

305 
apply (simp only: less_diff_eq) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

306 
apply (erule le_less_trans [OF dist_triangle]) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

307 
apply simp 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

308 
apply clarify 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

309 
apply (drule spec, erule mp) 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

310 
apply (simp add: dist_vec_def setL2_strict_mono) 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

311 
apply (rule_tac x="\<lambda>i. e / sqrt (of_nat CARD('b))" in exI) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

312 
apply (simp add: divide_pos_pos setL2_constant) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

313 
done 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

314 
qed 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

315 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

316 
end 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

317 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

318 
lemma Cauchy_vec_nth: 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

319 
"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

320 
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

321 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

322 
lemma vec_CauchyI: 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

323 
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

324 
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

325 
shows "Cauchy (\<lambda>n. X n)" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

326 
proof (rule metric_CauchyI) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

327 
fix r :: real assume "0 < r" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

328 
then have "0 < r / of_nat CARD('n)" (is "0 < ?s") 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

329 
by (simp add: divide_pos_pos) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

330 
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

331 
def M \<equiv> "Max (range N)" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

332 
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

333 
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

334 
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

335 
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

336 
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

337 
unfolding M_def by simp 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

338 
{ 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

339 
fix m n :: nat 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

340 
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

341 
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

342 
unfolding dist_vec_def .. 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

343 
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

344 
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

345 
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

346 
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

347 
also have "\<dots> = r" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

348 
by simp 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

349 
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

350 
} 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

351 
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

352 
by simp 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

353 
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

354 
qed 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

355 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

356 
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

357 
proof 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

358 
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

359 
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

360 
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

361 
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

362 
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

363 
by (simp add: vec_tendstoI) 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

364 
then show "convergent X" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

365 
by (rule convergentI) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

366 
qed 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

367 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

368 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

369 
subsection {* Normed vector space *} 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

370 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

371 
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

372 
begin 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

373 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

374 
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

375 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

376 
definition vector_sgn_def: 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

377 
"sgn (x::'a^'b) = scaleR (inverse (norm x)) x" 
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 
instance proof 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

380 
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

381 
show "0 \<le> norm x" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

382 
unfolding norm_vec_def 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

383 
by (rule setL2_nonneg) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

384 
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

385 
unfolding norm_vec_def 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

386 
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

387 
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

388 
unfolding norm_vec_def 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

389 
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

390 
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

391 
done 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

392 
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

393 
unfolding norm_vec_def 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

394 
by (simp add: setL2_right_distrib) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

395 
show "sgn x = scaleR (inverse (norm x)) x" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

396 
by (rule vector_sgn_def) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

397 
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

398 
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

399 
by (simp add: dist_norm) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

400 
qed 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

401 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

402 
end 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

403 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

404 
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

405 
unfolding norm_vec_def 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

406 
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

407 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

408 
interpretation 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

409 
apply default 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

410 
apply (rule vector_add_component) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

411 
apply (rule vector_scaleR_component) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

412 
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

413 
done 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

414 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

415 
instance vec :: (banach, finite) banach .. 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

416 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

417 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

418 
subsection {* Inner product space *} 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

419 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

420 
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

421 
begin 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

422 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

423 
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

424 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

425 
instance proof 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

426 
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

427 
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

428 
unfolding inner_vec_def 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

429 
by (simp add: inner_commute) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

430 
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

431 
unfolding inner_vec_def 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

432 
by (simp add: inner_add_left setsum_addf) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

433 
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

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: setsum_right_distrib) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

436 
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

437 
unfolding inner_vec_def 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

438 
by (simp add: setsum_nonneg) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

439 
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

440 
unfolding inner_vec_def 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

441 
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

442 
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

443 
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

444 
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

445 
qed 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

446 

df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

447 
end 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

448 

44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

449 
subsection {* Euclidean space *} 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

450 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

451 
text {* A bijection between @{text "'n::finite"} and @{text "{..<CARD('n)}"} *} 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

452 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

453 
definition vec_bij_nat :: "nat \<Rightarrow> ('n::finite)" where 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

454 
"vec_bij_nat = (SOME p. bij_betw p {..<CARD('n)} (UNIV::'n set) )" 
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

455 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

456 
abbreviation "\<pi> \<equiv> vec_bij_nat" 
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

457 
definition "\<pi>' = inv_into {..<CARD('n)} (\<pi>::nat \<Rightarrow> ('n::finite))" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

458 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

459 
lemma bij_betw_pi: 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

460 
"bij_betw \<pi> {..<CARD('n::finite)} (UNIV::('n::finite) set)" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

461 
using ex_bij_betw_nat_finite[of "UNIV::'n set"] 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

462 
by (auto simp: vec_bij_nat_def atLeast0LessThan 
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

463 
intro!: someI_ex[of "\<lambda>x. bij_betw x {..<CARD('n)} (UNIV::'n set)"]) 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

464 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

465 
lemma bij_betw_pi'[intro]: "bij_betw \<pi>' (UNIV::'n set) {..<CARD('n::finite)}" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

466 
using bij_betw_inv_into[OF bij_betw_pi] unfolding \<pi>'_def by auto 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

467 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

468 
lemma pi'_inj[intro]: "inj \<pi>'" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

469 
using bij_betw_pi' unfolding bij_betw_def by auto 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

470 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

471 
lemma pi'_range[intro]: "\<And>i::'n. \<pi>' i < CARD('n::finite)" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

472 
using bij_betw_pi' unfolding bij_betw_def by auto 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

473 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

474 
lemma \<pi>\<pi>'[simp]: "\<And>i::'n::finite. \<pi> (\<pi>' i) = i" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

475 
using bij_betw_pi by (auto intro!: f_inv_into_f simp: \<pi>'_def bij_betw_def) 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

476 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

477 
lemma \<pi>'\<pi>[simp]: "\<And>i. i\<in>{..<CARD('n::finite)} \<Longrightarrow> \<pi>' (\<pi> i::'n) = i" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

478 
using bij_betw_pi by (auto intro!: inv_into_f_eq simp: \<pi>'_def bij_betw_def) 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

479 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

480 
lemma \<pi>\<pi>'_alt[simp]: "\<And>i. i<CARD('n::finite) \<Longrightarrow> \<pi>' (\<pi> i::'n) = i" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

481 
by auto 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

482 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

483 
lemma \<pi>_inj_on: "inj_on (\<pi>::nat\<Rightarrow>'n::finite) {..<CARD('n)}" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

484 
using bij_betw_pi[where 'n='n] by (simp add: bij_betw_def) 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

485 

44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

486 
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

487 
begin 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

488 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

489 
definition "dimension (t :: ('a ^ 'b) itself) = CARD('b) * DIM('a)" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

490 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

491 
definition "(basis i::'a^'b) = 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

492 
(if i < (CARD('b) * DIM('a)) 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

493 
then (\<chi> j::'b. if j = \<pi>(i div DIM('a)) then basis (i mod DIM('a)) else 0) 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

494 
else 0)" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

495 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

496 
lemma basis_eq: 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

497 
assumes "i < CARD('b)" and "j < DIM('a)" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

498 
shows "basis (j + i * DIM('a)) = (\<chi> k. if k = \<pi> i then basis j else 0)" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

499 
proof  
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

500 
have "j + i * DIM('a) < DIM('a) * (i + 1)" using assms by (auto simp: field_simps) 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

501 
also have "\<dots> \<le> DIM('a) * CARD('b)" using assms unfolding mult_le_cancel1 by auto 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

502 
finally show ?thesis 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

503 
unfolding basis_vec_def using assms by (auto simp: vec_eq_iff not_less field_simps) 
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

504 
qed 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

505 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

506 
lemma basis_eq_pi': 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

507 
assumes "j < DIM('a)" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

508 
shows "basis (j + \<pi>' i * DIM('a)) $ k = (if k = i then basis j else 0)" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

509 
apply (subst basis_eq) 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

510 
using pi'_range assms by simp_all 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

511 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

512 
lemma split_times_into_modulo[consumes 1]: 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

513 
fixes k :: nat 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

514 
assumes "k < A * B" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

515 
obtains i j where "i < A" and "j < B" and "k = j + i * B" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

516 
proof 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

517 
have "A * B \<noteq> 0" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

518 
proof assume "A * B = 0" with assms show False by simp qed 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

519 
hence "0 < B" by auto 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

520 
thus "k mod B < B" using `0 < B` by auto 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

521 
next 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

522 
have "k div B * B \<le> k div B * B + k mod B" by (rule le_add1) 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

523 
also have "... < A * B" using assms by simp 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

524 
finally show "k div B < A" by auto 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

525 
qed simp 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

526 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

527 
lemma split_CARD_DIM[consumes 1]: 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

528 
fixes k :: nat 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

529 
assumes k: "k < CARD('b) * DIM('a)" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

530 
obtains i and j::'b where "i < DIM('a)" "k = i + \<pi>' j * DIM('a)" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

531 
proof  
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

532 
from split_times_into_modulo[OF k] guess i j . note ij = this 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

533 
show thesis 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

534 
proof 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

535 
show "j < DIM('a)" using ij by simp 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

536 
show "k = j + \<pi>' (\<pi> i :: 'b) * DIM('a)" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

537 
using ij by simp 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

538 
qed 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

539 
qed 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

540 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

541 
lemma linear_less_than_times: 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

542 
fixes i j A B :: nat assumes "i < B" "j < A" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

543 
shows "j + i * A < B * A" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

544 
proof  
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

545 
have "i * A + j < (Suc i)*A" using `j < A` by simp 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

546 
also have "\<dots> \<le> B * A" using `i < B` unfolding mult_le_cancel2 by simp 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

547 
finally show ?thesis by simp 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

548 
qed 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

549 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

550 
lemma DIM_cart[simp]: "DIM('a^'b) = CARD('b) * DIM('a)" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

551 
by (rule dimension_vec_def) 
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

552 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

553 
lemma all_less_DIM_cart: 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

554 
fixes m n :: nat 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

555 
shows "(\<forall>i<DIM('a^'b). P i) \<longleftrightarrow> (\<forall>x::'b. \<forall>i<DIM('a). P (i + \<pi>' x * DIM('a)))" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

556 
unfolding DIM_cart 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

557 
apply safe 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

558 
apply (drule spec, erule mp, erule linear_less_than_times [OF pi'_range]) 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

559 
apply (erule split_CARD_DIM, simp) 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

560 
done 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

561 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

562 
lemma eq_pi_iff: 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

563 
fixes x :: "'c::finite" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

564 
shows "i < CARD('c::finite) \<Longrightarrow> x = \<pi> i \<longleftrightarrow> \<pi>' x = i" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

565 
by auto 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

566 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

567 
lemma all_less_mult: 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

568 
fixes m n :: nat 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

569 
shows "(\<forall>i<(m * n). P i) \<longleftrightarrow> (\<forall>i<m. \<forall>j<n. P (j + i * n))" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

570 
apply safe 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

571 
apply (drule spec, erule mp, erule (1) linear_less_than_times) 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

572 
apply (erule split_times_into_modulo, simp) 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

573 
done 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

574 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

575 
lemma inner_if: 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

576 
"inner (if a then x else y) z = (if a then inner x z else inner y z)" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

577 
"inner x (if a then y else z) = (if a then inner x y else inner x z)" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

578 
by simp_all 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

579 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

580 
instance proof 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

581 
show "0 < DIM('a ^ 'b)" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

582 
unfolding dimension_vec_def 
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

583 
by (intro mult_pos_pos zero_less_card_finite DIM_positive) 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

584 
next 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

585 
fix i :: nat 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

586 
assume "DIM('a ^ 'b) \<le> i" thus "basis i = (0::'a^'b)" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

587 
unfolding dimension_vec_def basis_vec_def 
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

588 
by simp 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

589 
next 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

590 
show "\<forall>i<DIM('a ^ 'b). \<forall>j<DIM('a ^ 'b). 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

591 
inner (basis i :: 'a ^ 'b) (basis j) = (if i = j then 1 else 0)" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

592 
apply (simp add: inner_vec_def) 
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

593 
apply safe 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

594 
apply (erule split_CARD_DIM, simp add: basis_eq_pi') 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

595 
apply (simp add: inner_if setsum_delta cong: if_cong) 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

596 
apply (simp add: basis_orthonormal) 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

597 
apply (elim split_CARD_DIM, simp add: basis_eq_pi') 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

598 
apply (simp add: inner_if setsum_delta cong: if_cong) 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

599 
apply (clarsimp simp add: basis_orthonormal) 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

600 
done 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

601 
next 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

602 
fix x :: "'a ^ 'b" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

603 
show "(\<forall>i<DIM('a ^ 'b). inner (basis i) x = 0) \<longleftrightarrow> x = 0" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

604 
unfolding all_less_DIM_cart 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

605 
unfolding inner_vec_def 
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

606 
apply (simp add: basis_eq_pi') 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

607 
apply (simp add: inner_if setsum_delta cong: if_cong) 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

608 
apply (simp add: euclidean_all_zero) 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

609 
apply (simp add: vec_eq_iff) 
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

610 
done 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

611 
qed 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

612 

36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

613 
end 
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

614 

18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

615 
end 