author  huffman 
Wed, 10 Aug 2011 10:13:16 0700  
changeset 44135  18b4ab6854f1 
parent 42290  b1f544c84040 
child 44136  e63ad7d5158d 
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 

16 
typedef (open Cart) 

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

17 
('a, 'b) cart = "UNIV :: (('b::finite) \<Rightarrow> 'a) set" 
33175  18 
morphisms Cart_nth Cart_lambda .. 
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 
0f17eda72e60
binder notation for default print_mode  to avoid strange output if "xsymbols" is not active;
wenzelm
parents:
35253
diff
changeset

21 
Cart_nth (infixl "$" 90) and 
0f17eda72e60
binder notation for default print_mode  to avoid strange output if "xsymbols" is not active;
wenzelm
parents:
35253
diff
changeset

22 
Cart_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 
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34290
diff
changeset

26 
the finite type class write "cart '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 

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

29 
syntax "_finite_cart" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15) 
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 
35397  33 
fun cart t u = Syntax.const @{type_syntax cart} $ t $ u; 
34290
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset

34 
fun finite_cart_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 
35397  36 
cart t (Syntax.const @{syntax_const "_ofsort"} $ u $ Syntax.const @{class_syntax finite}) 
34290
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset

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

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

39 
in 
35113  40 
[(@{syntax_const "_finite_cart"}, finite_cart_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 

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

47 
lemma Cart_eq: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

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

50 
lemma Cart_lambda_beta [simp]: "Cart_lambda g $ i = g i" 

51 
by (simp add: Cart_lambda_inverse) 

52 

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

53 
lemma Cart_lambda_unique: "(\<forall>i. f$i = g i) \<longleftrightarrow> Cart_lambda g = f" 
33175  54 
by (auto simp add: Cart_eq) 
55 

56 
lemma Cart_lambda_eta: "(\<chi> i. (g$i)) = g" 

57 
by (simp add: Cart_eq) 

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 

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

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

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

64 
definition vector_zero_def : "0 \<equiv> (\<chi> i. 0)" 
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 

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

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

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

70 
definition vector_add_def : "op + \<equiv> (\<lambda> x y. (\<chi> i. (x$i) + (y$i)))" 
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 

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

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

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

76 
definition vector_minus_def : "op  \<equiv> (\<lambda> x y. (\<chi> i. (x$i)  (y$i)))" 
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 

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

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

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

82 
definition vector_uminus_def : "uminus \<equiv> (\<lambda> x. (\<chi> i.  (x$i)))" 
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" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

87 
unfolding vector_zero_def by simp 
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" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

90 
unfolding vector_add_def by simp 
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" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

93 
unfolding vector_minus_def by simp 
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)" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

97 

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

98 
instance cart :: (semigroup_add, finite) semigroup_add 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

99 
by default (simp add: Cart_eq add_assoc) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

100 

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

101 
instance cart :: (ab_semigroup_add, finite) ab_semigroup_add 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

102 
by default (simp add: Cart_eq add_commute) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

103 

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

104 
instance cart :: (monoid_add, finite) monoid_add 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

105 
by default (simp_all add: Cart_eq) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

106 

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

107 
instance cart :: (comm_monoid_add, finite) comm_monoid_add 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

109 

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

110 
instance cart :: (cancel_semigroup_add, finite) cancel_semigroup_add 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

111 
by default (simp_all add: Cart_eq) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

112 

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

113 
instance cart :: (cancel_ab_semigroup_add, finite) cancel_ab_semigroup_add 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

115 

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

116 
instance cart :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add .. 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

117 

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

118 
instance cart :: (group_add, finite) group_add 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

120 

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

121 
instance cart :: (ab_group_add, finite) ab_group_add 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

122 
by default (simp_all add: Cart_eq) 
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 

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

127 
instantiation cart :: (real_vector, finite) real_vector 
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 

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

130 
definition vector_scaleR_def: "scaleR = (\<lambda> r x. (\<chi> i. scaleR r (x$i)))" 
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)" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

133 
unfolding vector_scaleR_def by simp 
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 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

136 
by default (simp_all add: Cart_eq scaleR_left_distrib scaleR_right_distrib) 
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 

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

143 
instantiation cart :: (topological_space, finite) topological_space 
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 

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

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

153 
unfolding open_vector_def by auto 
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)" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

167 
unfolding open_vector_def 
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}" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

180 
unfolding open_vector_def by auto 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

181 

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

182 
lemma open_vimage_Cart_nth: "open S \<Longrightarrow> open ((\<lambda>x. x $ i) ` S)" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

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

185 
apply (rule_tac x="\<lambda>k. if k = i then S else UNIV" in exI, simp) 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

187 

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

188 
lemma closed_vimage_Cart_nth: "closed S \<Longrightarrow> closed ((\<lambda>x. x $ i) ` S)" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

189 
unfolding closed_open vimage_Compl [symmetric] 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

190 
by (rule open_vimage_Cart_nth) 
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}" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

196 
by (simp add: closed_INT closed_vimage_Cart_nth) 
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 

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

199 
lemma tendsto_Cart_nth [tendsto_intros]: 
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)" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

205 
by (simp_all add: open_vimage_Cart_nth) 
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 

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

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

230 
unfolding open_vector_def by metis 
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 

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

239 
lemma tendsto_Cart_lambda [tendsto_intros]: 
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" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

242 
using assms by (simp add: tendsto_vector) 
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 

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

254 
instantiation cart :: (metric_space, finite) metric_space 
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 

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

257 
definition dist_vector_def: 
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 

38656  260 
lemma dist_nth_le_cart: "dist (x $ i) (y $ i) \<le> dist x y" 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

262 
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

263 

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

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

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

266 
show "dist x y = 0 \<longleftrightarrow> x = y" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

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

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

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

271 
show "dist x y \<le> dist x z + dist y z" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

273 
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

274 
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

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

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

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

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

279 
show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

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

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

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

284 
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

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

286 
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

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

288 
apply (drule spec, drule spec, erule mp) 
38656  289 
apply (erule le_less_trans [OF dist_nth_le_cart]) 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

290 
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

291 
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

292 
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

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

294 
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

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

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

297 
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

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

299 
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

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

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

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

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

304 
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

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

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

307 
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

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

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

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

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

312 
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

313 
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

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

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

316 

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

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

318 

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

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

320 
"Cauchy (\<lambda>n. X n) \<Longrightarrow> Cauchy (\<lambda>n. X n $ i)" 
38656  321 
unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_nth_le_cart]) 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

322 

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

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

324 
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

325 
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

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

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

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

329 
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

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

331 
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

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

333 
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

334 
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

335 
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

336 
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

337 
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

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

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

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

341 
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

342 
have "dist (X m) (X n) = setL2 (\<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

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

344 
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

345 
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

346 
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

347 
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

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

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

350 
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

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

352 
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

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

354 
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

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

356 

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

357 
instance cart :: (complete_space, finite) complete_space 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

359 
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

360 
have "\<And>i. (\<lambda>n. X n $ i) > lim (\<lambda>n. X n $ i)" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

361 
using Cauchy_Cart_nth [OF `Cauchy X`] 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

363 
hence "X > Cart_lambda (\<lambda>i. lim (\<lambda>n. X n $ i))" 
36660
1cc4ab4b7ff7
make (X > L) an abbreviation for (X > L) sequentially
huffman
parents:
36591
diff
changeset

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

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

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

367 
qed 
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 

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

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

371 

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

372 
instantiation cart :: (real_normed_vector, finite) real_normed_vector 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

374 

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

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

376 
"norm x = setL2 (\<lambda>i. norm (x$i)) UNIV" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

377 

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

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

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

380 

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

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

382 
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

383 
show "0 \<le> norm x" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

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

386 
show "norm x = 0 \<longleftrightarrow> x = 0" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

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

389 
show "norm (x + y) \<le> norm x + norm y" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

391 
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

392 
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

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

394 
show "norm (scaleR a x) = \<bar>a\<bar> * norm x" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

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

397 
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

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

399 
show "dist x y = norm (x  y)" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

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

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

405 

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

406 
lemma norm_nth_le: "norm (x $ i) \<le> norm x" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

408 
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

409 

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

410 
interpretation Cart_nth: bounded_linear "\<lambda>x. x $ i" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

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

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

414 
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

415 
done 
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 
instance cart :: (banach, finite) banach .. 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

418 

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

419 

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

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

421 

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

422 
instantiation cart :: (real_inner, finite) real_inner 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

426 
"inner x y = setsum (\<lambda>i. inner (x$i) (y$i)) UNIV" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

427 

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

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

429 
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

430 
show "inner x y = inner y x" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

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

433 
show "inner (x + y) z = inner x z + inner y z" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

435 
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

436 
show "inner (scaleR r x) y = r * inner x y" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

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

439 
show "0 \<le> inner x x" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

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

442 
show "inner x x = 0 \<longleftrightarrow> x = 0" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

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

445 
show "norm x = sqrt (inner x x)" 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

446 
unfolding inner_vector_def norm_vector_def setL2_def 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

447 
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

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

449 

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

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

451 

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

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

453 

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

454 
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

455 

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

456 
definition cart_bij_nat :: "nat \<Rightarrow> ('n::finite)" where 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

457 
"cart_bij_nat = (SOME p. bij_betw p {..<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

458 

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

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

460 
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

461 

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

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

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

464 
using ex_bij_betw_nat_finite[of "UNIV::'n set"] 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

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

466 
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

467 

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

468 
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

469 
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

470 

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

471 
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

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'_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

475 
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

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::'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

478 
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

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>[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

481 
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

482 

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

483 
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

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

485 

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

486 
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

487 
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

488 

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

489 
instantiation cart :: (euclidean_space, finite) euclidean_space 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

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

491 

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

492 
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

493 

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

494 
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

495 
(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

496 
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

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

498 

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

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

500 
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

501 
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

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

503 
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

504 
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

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

506 
unfolding basis_cart_def using assms by (auto simp: Cart_eq not_less field_simps) 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

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

508 

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

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

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

511 
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

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

513 
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

514 

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

515 
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

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

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

518 
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

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

520 
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

521 
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

522 
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

523 
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

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

525 
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

526 
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

527 
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

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

529 

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

530 
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

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

532 
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

533 
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

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

535 
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

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

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

538 
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

539 
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

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

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

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

543 

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

544 
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

545 
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

546 
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

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

548 
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

549 
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

550 
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

551 
qed 
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 DIM_cart[simp]: "DIM('a^'b) = CARD('b) * DIM('a)" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

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

555 

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

556 
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

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

558 
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

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

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

561 
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

562 
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

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

564 

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

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

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

567 
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

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

569 

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

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

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

572 
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

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

574 
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

575 
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

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

577 

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

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

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

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

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

582 

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

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

584 
show "0 < DIM('a ^ 'b)" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

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

586 
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

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

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

589 
assume "DIM('a ^ 'b) \<le> i" thus "basis i = (0::'a^'b)" 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

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

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

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

593 
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

594 
inner (basis i :: 'a ^ 'b) (basis j) = (if i = j then 1 else 0)" 
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_vector_def) 
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

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

597 
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

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

601 
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

602 
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

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

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

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

606 
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

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

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

609 
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

610 
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

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

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

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

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

615 

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

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

617 

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

618 
end 