author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45694  4a8743618257 
child 49674  dbadb4d03cbc 
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 

45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
44681
diff
changeset

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

17 
morphisms vec_nth vec_lambda .. 
33175  18 

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

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

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

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

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

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

24 
Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

25 
the finite type class write "vec 'b 'n" 
34290
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset

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

27 

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

28 
syntax "_finite_vec" :: "type \<Rightarrow> type \<Rightarrow> type" ("(_ ^/ _)" [15, 16] 15) 
34290
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset

29 

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

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

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

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

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

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

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

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

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

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

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

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

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

42 

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

43 
lemma vec_eq_iff: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)" 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

44 
by (simp add: vec_nth_inject [symmetric] fun_eq_iff) 
33175  45 

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

46 
lemma vec_lambda_beta [simp]: "vec_lambda g $ i = g i" 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

47 
by (simp add: vec_lambda_inverse) 
33175  48 

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

49 
lemma vec_lambda_unique: "(\<forall>i. f$i = g i) \<longleftrightarrow> vec_lambda g = f" 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

50 
by (auto simp add: vec_eq_iff) 
33175  51 

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

52 
lemma vec_lambda_eta: "(\<chi> i. (g$i)) = g" 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

53 
by (simp add: vec_eq_iff) 
33175  54 

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

55 

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

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

57 

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

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

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

60 
definition "0 \<equiv> (\<chi> i. 0)" 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

63 

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

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

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

66 
definition "op + \<equiv> (\<lambda> x y. (\<chi> i. x$i + y$i))" 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

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

69 

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

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

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

72 
definition "op  \<equiv> (\<lambda> x y. (\<chi> i. x$i  y$i))" 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

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

75 

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

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

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

78 
definition "uminus \<equiv> (\<lambda> x. (\<chi> i.  (x$i)))" 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

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

81 

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

82 
lemma zero_index [simp]: "0 $ i = 0" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

83 
unfolding zero_vec_def by simp 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

84 

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

85 
lemma vector_add_component [simp]: "(x + y)$i = x$i + y$i" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

86 
unfolding plus_vec_def by simp 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

87 

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

88 
lemma vector_minus_component [simp]: "(x  y)$i = x$i  y$i" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

89 
unfolding minus_vec_def by simp 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

90 

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

91 
lemma vector_uminus_component [simp]: "( x)$i =  (x$i)" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

92 
unfolding uminus_vec_def by simp 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

93 

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

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

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

96 

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

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

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

99 

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

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

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

102 

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

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

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

105 

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

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

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

108 

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

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

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

111 

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

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

113 

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

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

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

116 

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

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

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

119 

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 
subsection {* Real vector space *} 
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

122 

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

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

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

125 

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

126 
definition "scaleR \<equiv> (\<lambda> r x. (\<chi> i. scaleR r (x$i)))" 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

127 

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

128 
lemma vector_scaleR_component [simp]: "(scaleR r x)$i = scaleR r (x$i)" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

129 
unfolding scaleR_vec_def by simp 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

130 

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

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

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

133 

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

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

135 

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

136 

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

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

138 

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

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

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

141 

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

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

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

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

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

146 

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

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

148 
show "open (UNIV :: ('a ^ 'b) set)" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

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

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

152 
assume "open S" "open T" thus "open (S \<inter> T)" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

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

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

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

157 
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

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

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

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

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

162 
assume "\<forall>S\<in>K. open S" thus "open (\<Union>K)" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

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

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

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

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

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

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

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

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

172 

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

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

174 

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

175 
lemma open_vector_box: "\<forall>i. open (S i) \<Longrightarrow> open {x. \<forall>i. x $ i \<in> S i}" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

177 

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

178 
lemma open_vimage_vec_nth: "open S \<Longrightarrow> open ((\<lambda>x. x $ i) ` S)" 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

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

181 
apply (rule_tac x="\<lambda>k. if k = i then S else UNIV" in exI, simp) 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

183 

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

184 
lemma closed_vimage_vec_nth: "closed S \<Longrightarrow> closed ((\<lambda>x. x $ i) ` S)" 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

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

187 

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

188 
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

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

190 
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

191 
thus "\<forall>i. closed (S i) \<Longrightarrow> closed {x. \<forall>i. x $ i \<in> S i}" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

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

194 

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

195 
lemma tendsto_vec_nth [tendsto_intros]: 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

196 
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

197 
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

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

199 
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

200 
then have "open ((\<lambda>y. y $ i) ` S)" "a \<in> ((\<lambda>y. y $ i) ` S)" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

201 
by (simp_all add: open_vimage_vec_nth) 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

202 
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

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

204 
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

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

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

207 

44631  208 
lemma isCont_vec_nth [simp]: "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x $ i) a" 
209 
unfolding isCont_def by (rule tendsto_vec_nth) 

210 

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

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

212 
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

213 
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

214 
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

215 

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

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

217 
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

218 
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

219 
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

220 
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

221 

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

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

223 
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

224 
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

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

226 
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

227 
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

228 
and S: "\<And>y. \<forall>i. y $ i \<in> A i \<Longrightarrow> y \<in> S" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

230 
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

231 
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

232 
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

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

234 
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

235 
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

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

237 

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

238 
lemma tendsto_vec_lambda [tendsto_intros]: 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

239 
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

240 
shows "((\<lambda>x. \<chi> i. f x i) > (\<chi> i. a i)) net" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

242 

44571  243 
lemma open_image_vec_nth: assumes "open S" shows "open ((\<lambda>x. x $ i) ` S)" 
244 
proof (rule openI) 

245 
fix a assume "a \<in> (\<lambda>x. x $ i) ` S" 

246 
then obtain z where "a = z $ i" and "z \<in> S" .. 

247 
then obtain A where A: "\<forall>i. open (A i) \<and> z $ i \<in> A i" 

248 
and S: "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S" 

249 
using `open S` unfolding open_vec_def by auto 

250 
hence "A i \<subseteq> (\<lambda>x. x $ i) ` S" 

251 
by (clarsimp, rule_tac x="\<chi> j. if j = i then x else z $ j" in image_eqI, 

252 
simp_all) 

253 
hence "open (A i) \<and> a \<in> A i \<and> A i \<subseteq> (\<lambda>x. x $ i) ` S" 

254 
using A `a = z $ i` by simp 

255 
then show "\<exists>T. open T \<and> a \<in> T \<and> T \<subseteq> (\<lambda>x. x $ i) ` S" by  (rule exI) 

256 
qed 

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

257 

44571  258 
instance vec :: (perfect_space, finite) perfect_space 
259 
proof 

260 
fix x :: "'a ^ 'b" show "\<not> open {x}" 

261 
proof 

262 
assume "open {x}" 

263 
hence "\<forall>i. open ((\<lambda>x. x $ i) ` {x})" by (fast intro: open_image_vec_nth) 

264 
hence "\<forall>i. open {x $ i}" by simp 

265 
thus "False" by (simp add: not_open_singleton) 

266 
qed 

267 
qed 

268 

269 

270 
subsection {* Metric space *} 

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

271 

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

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

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

274 

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

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

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

277 

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

278 
lemma dist_vec_nth_le: "dist (x $ i) (y $ i) \<le> dist x y" 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

279 
unfolding dist_vec_def by (rule member_le_setL2) simp_all 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

280 

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

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

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

283 
show "dist x y = 0 \<longleftrightarrow> x = y" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

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

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

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

288 
show "dist x y \<le> dist x z + dist y z" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

290 
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

291 
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

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

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

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

295 
show "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" 
44630  296 
proof 
297 
assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" 

298 
proof 

299 
fix x assume "x \<in> S" 

300 
obtain A where A: "\<forall>i. open (A i)" "\<forall>i. x $ i \<in> A i" 

301 
and S: "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S" 

302 
using `open S` and `x \<in> S` unfolding open_vec_def by metis 

303 
have "\<forall>i\<in>UNIV. \<exists>r>0. \<forall>y. dist y (x $ i) < r \<longrightarrow> y \<in> A i" 

304 
using A unfolding open_dist by simp 

305 
hence "\<exists>r. \<forall>i\<in>UNIV. 0 < r i \<and> (\<forall>y. dist y (x $ i) < r i \<longrightarrow> y \<in> A i)" 

44681
49ef76b4a634
remove duplicate lemma finite_choice in favor of finite_set_choice
huffman
parents:
44631
diff
changeset

306 
by (rule finite_set_choice [OF finite]) 
44630  307 
then obtain r where r1: "\<forall>i. 0 < r i" 
308 
and r2: "\<forall>i y. dist y (x $ i) < r i \<longrightarrow> y \<in> A i" by fast 

309 
have "0 < Min (range r) \<and> (\<forall>y. dist y x < Min (range r) \<longrightarrow> y \<in> S)" 

310 
by (simp add: r1 r2 S le_less_trans [OF dist_vec_nth_le]) 

311 
thus "\<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" .. 

312 
qed 

313 
next 

314 
assume *: "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" show "open S" 

315 
proof (unfold open_vec_def, rule) 

316 
fix x assume "x \<in> S" 

317 
then obtain e where "0 < e" and S: "\<forall>y. dist y x < e \<longrightarrow> y \<in> S" 

318 
using * by fast 

319 
def r \<equiv> "\<lambda>i::'b. e / sqrt (of_nat CARD('b))" 

320 
from `0 < e` have r: "\<forall>i. 0 < r i" 

321 
unfolding r_def by (simp_all add: divide_pos_pos) 

322 
from `0 < e` have e: "e = setL2 r UNIV" 

323 
unfolding r_def by (simp add: setL2_constant) 

324 
def A \<equiv> "\<lambda>i. {y. dist (x $ i) y < r i}" 

325 
have "\<forall>i. open (A i) \<and> x $ i \<in> A i" 

326 
unfolding A_def by (simp add: open_ball r) 

327 
moreover have "\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S" 

328 
by (simp add: A_def S dist_vec_def e setL2_strict_mono dist_commute) 

329 
ultimately show "\<exists>A. (\<forall>i. open (A i) \<and> x $ i \<in> A i) \<and> 

330 
(\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S)" by metis 

331 
qed 

332 
qed 

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

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

334 

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

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

336 

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

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

338 
"Cauchy (\<lambda>n. X n) \<Longrightarrow> Cauchy (\<lambda>n. X n $ i)" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

339 
unfolding Cauchy_def by (fast intro: le_less_trans [OF dist_vec_nth_le]) 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

340 

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

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

342 
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

343 
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

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

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

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

347 
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

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

349 
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

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

351 
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

352 
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

353 
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

354 
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

355 
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

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

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

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

359 
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

360 
have "dist (X m) (X n) = setL2 (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

362 
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

363 
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

364 
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

365 
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

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

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

368 
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

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

370 
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

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

372 
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

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

374 

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

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

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

377 
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

378 
have "\<And>i. (\<lambda>n. X n $ i) > lim (\<lambda>n. X n $ i)" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

380 
by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

381 
hence "X > vec_lambda (\<lambda>i. lim (\<lambda>n. X n $ i))" 
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

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

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

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

386 

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

387 

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

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

389 

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

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

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

392 

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

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

394 

44141  395 
definition "sgn (x::'a^'b) = scaleR (inverse (norm x)) x" 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

396 

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

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

398 
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

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

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

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

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

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

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

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

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

407 
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

408 
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

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

410 
show "norm (scaleR a x) = \<bar>a\<bar> * norm x" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

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

413 
show "sgn x = scaleR (inverse (norm x)) x" 
44141  414 
by (rule sgn_vec_def) 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

415 
show "dist x y = norm (x  y)" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

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

418 
qed 
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 
end 
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 
lemma norm_nth_le: "norm (x $ i) \<le> norm x" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

424 
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

425 

44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
44233
diff
changeset

426 
lemma bounded_linear_vec_nth: "bounded_linear (\<lambda>x. x $ i)" 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

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

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

430 
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

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

432 

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

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

434 

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

435 

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

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

437 

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

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

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

440 

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

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

442 

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

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

444 
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

445 
show "inner x y = inner y x" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

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

448 
show "inner (x + y) z = inner x z + inner y z" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

450 
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

451 
show "inner (scaleR r x) y = r * inner x y" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

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

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

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

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

457 
show "inner x x = 0 \<longleftrightarrow> x = 0" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

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

460 
show "norm x = sqrt (inner x x)" 
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset

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

462 
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

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

464 

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

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

466 

44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

467 

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

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

469 

44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

470 
text {* Vectors pointing along a single axis. *} 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

471 

d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

472 
definition "axis k x = (\<chi> i. if i = k then x else 0)" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

473 

d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

474 
lemma axis_nth [simp]: "axis i x $ i = x" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

475 
unfolding axis_def by simp 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

476 

d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

477 
lemma axis_eq_axis: "axis i x = axis j y \<longleftrightarrow> x = y \<and> i = j \<or> x = 0 \<and> y = 0" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

478 
unfolding axis_def vec_eq_iff by auto 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

479 

d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

480 
lemma inner_axis_axis: 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

481 
"inner (axis i x) (axis j y) = (if i = j then inner x y else 0)" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

482 
unfolding inner_vec_def 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

483 
apply (cases "i = j") 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

484 
apply clarsimp 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

485 
apply (subst setsum_diff1' [where a=j], simp_all) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

486 
apply (rule setsum_0', simp add: axis_def) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

487 
apply (rule setsum_0', simp add: axis_def) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

488 
done 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

489 

d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

490 
lemma setsum_single: 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

491 
assumes "finite A" and "k \<in> A" and "f k = y" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

492 
assumes "\<And>i. i \<in> A \<Longrightarrow> i \<noteq> k \<Longrightarrow> f i = 0" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

493 
shows "(\<Sum>i\<in>A. f i) = y" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

494 
apply (subst setsum_diff1' [OF assms(1,2)]) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

495 
apply (simp add: setsum_0' assms(3,4)) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

496 
done 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

497 

d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

498 
lemma inner_axis: "inner x (axis i y) = inner (x $ i) y" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

499 
unfolding inner_vec_def 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

500 
apply (rule_tac k=i in setsum_single) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

501 
apply simp_all 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

502 
apply (simp add: axis_def) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

503 
done 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

504 

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

505 
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

506 

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

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

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

509 

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

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

511 
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

512 

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

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

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

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

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

517 
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

518 

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

519 
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

520 
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

521 

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

522 
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

523 
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

524 

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

525 
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

526 
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

527 

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

528 
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

529 
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

530 

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

531 
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

532 
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

533 

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

534 
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

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

536 

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

537 
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

538 
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

539 

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

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

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

542 

44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

543 
definition "Basis = (\<Union>i. \<Union>u\<in>Basis. {axis i u})" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

544 

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

545 
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

546 

44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

547 
definition "basis i = 
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

548 
(if i < (CARD('b) * DIM('a)) 
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

549 
then axis (\<pi>(i div DIM('a))) (basis (i mod DIM('a))) 
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

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

551 

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

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

553 
assumes "i < CARD('b)" and "j < DIM('a)" 
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

554 
shows "basis (j + i * DIM('a)) = axis (\<pi> i) (basis j)" 
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

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

556 
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

557 
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

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

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

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

561 

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

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

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

564 
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

565 
apply (subst basis_eq) 
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

566 
using pi'_range assms by (simp_all add: axis_def) 
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

567 

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

568 
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

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

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

571 
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

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

573 
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

574 
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

575 
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

576 
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

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

578 
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

579 
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

580 
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

581 
qed simp 
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 
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

584 
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

585 
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

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

587 
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

588 
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

589 
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

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

591 

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

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

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

594 

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

595 
instance proof 
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

596 
show "(Basis :: ('a ^ 'b) set) \<noteq> {}" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

597 
unfolding Basis_vec_def by simp 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

598 
next 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

599 
show "finite (Basis :: ('a ^ 'b) set)" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

600 
unfolding Basis_vec_def by simp 
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

601 
next 
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

602 
fix u v :: "'a ^ 'b" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

603 
assume "u \<in> Basis" and "v \<in> Basis" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

604 
thus "inner u v = (if u = v then 1 else 0)" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

605 
unfolding Basis_vec_def 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

606 
by (auto simp add: inner_axis_axis axis_eq_axis inner_Basis) 
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

607 
next 
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

608 
fix x :: "'a ^ 'b" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

609 
show "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> x = 0" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

610 
unfolding Basis_vec_def 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

611 
by (simp add: inner_axis euclidean_all_zero_iff vec_eq_iff) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

612 
next 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

613 
show "DIM('a ^ 'b) = card (Basis :: ('a ^ 'b) set)" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

614 
unfolding Basis_vec_def dimension_vec_def dimension_def 
44215  615 
by (simp add: card_UN_disjoint [unfolded disjoint_iff_not_equal] 
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

616 
axis_eq_axis nonzero_Basis) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

617 
next 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

618 
show "basis ` {..<DIM('a ^ 'b)} = (Basis :: ('a ^ 'b) set)" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

619 
unfolding Basis_vec_def 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

620 
apply auto 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

621 
apply (erule split_times_into_modulo) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

622 
apply (simp add: basis_eq axis_eq_axis) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

623 
apply (erule Basis_elim) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

624 
apply (simp add: image_def basis_vec_def axis_eq_axis) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

625 
apply (rule rev_bexI, simp) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

626 
apply (erule linear_less_than_times [OF pi'_range]) 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

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

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

629 
next 
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

630 
show "basis ` {DIM('a ^ 'b)..} = {0::'a ^ 'b}" 
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

631 
by (auto simp add: image_def basis_vec_def) 
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

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

633 

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

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

635 

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

636 
end 