author  nipkow 
Thu, 07 Dec 2017 15:48:50 +0100  
changeset 67155  9e5b05d54f9d 
parent 66453  cc19f7ca2ed6 
child 67399  eab6ce8368fa 
permissions  rwrr 
63627  1 
(* Title: HOL/Analysis/Finite_Cartesian_Product.thy 
35253  2 
Author: Amine Chaieb, University of Cambridge 
33175  3 
*) 
4 

60420  5 
section \<open>Definition of finite Cartesian product types.\<close> 
33175  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 
66453
cc19f7ca2ed6
sessionqualified theory imports: isabelle imports U i d '~~/src/Benchmarks' a;
wenzelm
parents:
66281
diff
changeset

11 
"HOLLibrary.Numeral_Type" 
cc19f7ca2ed6
sessionqualified theory imports: isabelle imports U i d '~~/src/Benchmarks' a;
wenzelm
parents:
66281
diff
changeset

12 
"HOLLibrary.Countable_Set" 
cc19f7ca2ed6
sessionqualified theory imports: isabelle imports U i d '~~/src/Benchmarks' a;
wenzelm
parents:
66281
diff
changeset

13 
"HOLLibrary.FuncSet" 
33175  14 
begin 
15 

60420  16 
subsection \<open>Finite Cartesian products, with indexing and lambdas.\<close> 
33175  17 

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

19 
morphisms vec_nth vec_lambda .. 
33175  20 

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

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

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

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

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

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

26 
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

27 
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

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

29 

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

30 
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

31 

60420  32 
parse_translation \<open> 
52143  33 
let 
34 
fun vec t u = Syntax.const @{type_syntax vec} $ t $ u; 

35 
fun finite_vec_tr [t, u] = 

36 
(case Term_Position.strip_positions u of 

37 
v as Free (x, _) => 

38 
if Lexicon.is_tid x then 

39 
vec t (Syntax.const @{syntax_const "_ofsort"} $ v $ 

40 
Syntax.const @{class_syntax finite}) 

41 
else vec t u 

42 
 _ => vec t u) 

43 
in 

44 
[(@{syntax_const "_finite_vec"}, K finite_vec_tr)] 

45 
end 

60420  46 
\<close> 
34290
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset

47 

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

48 
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

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

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

51 
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

52 
by (simp add: vec_lambda_inverse) 
33175  53 

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

54 
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

55 
by (auto simp add: vec_eq_iff) 
33175  56 

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

57 
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

58 
by (simp add: vec_eq_iff) 
33175  59 

66281
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

60 
subsection \<open>Cardinality of vectors\<close> 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

61 

6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

62 
instance vec :: (finite, finite) finite 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

63 
proof 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

64 
show "finite (UNIV :: ('a, 'b) vec set)" 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

65 
proof (subst bij_betw_finite) 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

66 
show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

67 
by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff) 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

68 
have "finite (PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

69 
by (intro finite_PiE) auto 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

70 
also have "(PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set)) = Pi UNIV (\<lambda>_. UNIV)" 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

71 
by auto 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

72 
finally show "finite \<dots>" . 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

73 
qed 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

74 
qed 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

75 

6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

76 
lemma countable_PiE: 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

77 
"finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (F i)) \<Longrightarrow> countable (Pi\<^sub>E I F)" 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

78 
by (induct I arbitrary: F rule: finite_induct) (auto simp: PiE_insert_eq) 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

79 

6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

80 
instance vec :: (countable, finite) countable 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

81 
proof 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

82 
have "countable (UNIV :: ('a, 'b) vec set)" 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

83 
proof (rule countableI_bij2) 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

84 
show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

85 
by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff) 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

86 
have "countable (PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

87 
by (intro countable_PiE) auto 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

88 
also have "(PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set)) = Pi UNIV (\<lambda>_. UNIV)" 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

89 
by auto 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

90 
finally show "countable \<dots>" . 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

91 
qed 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

92 
thus "\<exists>t::('a, 'b) vec \<Rightarrow> nat. inj t" 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

93 
by (auto elim!: countableE) 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

94 
qed 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

95 

6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

96 
lemma infinite_UNIV_vec: 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

97 
assumes "infinite (UNIV :: 'a set)" 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

98 
shows "infinite (UNIV :: ('a, 'b :: finite) vec set)" 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

99 
proof (subst bij_betw_finite) 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

100 
show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

101 
by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff) 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

102 
have "infinite (PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" (is "infinite ?A") 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

103 
proof 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

104 
assume "finite ?A" 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

105 
hence "finite ((\<lambda>f. f undefined) ` ?A)" 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

106 
by (rule finite_imageI) 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

107 
also have "(\<lambda>f. f undefined) ` ?A = UNIV" 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

108 
by auto 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

109 
finally show False 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

110 
using \<open>infinite (UNIV :: 'a set)\<close> by contradiction 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

111 
qed 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

112 
also have "?A = Pi UNIV (\<lambda>_. UNIV)" 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

113 
by auto 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

114 
finally show "infinite (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" . 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

115 
qed 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

116 

6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

117 
lemma CARD_vec [simp]: 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

118 
"CARD(('a,'b::finite) vec) = CARD('a) ^ CARD('b)" 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

119 
proof (cases "finite (UNIV :: 'a set)") 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

120 
case True 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

121 
show ?thesis 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

122 
proof (subst bij_betw_same_card) 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

123 
show "bij_betw vec_nth UNIV (Pi (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

124 
by (intro bij_betwI[of _ _ _ vec_lambda]) (auto simp: vec_eq_iff) 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

125 
have "CARD('a) ^ CARD('b) = card (PiE (UNIV :: 'b set) (\<lambda>_. UNIV :: 'a set))" 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

126 
(is "_ = card ?A") 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

127 
by (subst card_PiE) (auto simp: prod_constant) 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

128 

6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

129 
also have "?A = Pi UNIV (\<lambda>_. UNIV)" 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

130 
by auto 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

131 
finally show "card \<dots> = CARD('a) ^ CARD('b)" .. 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

132 
qed 
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

133 
qed (simp_all add: infinite_UNIV_vec) 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

134 

60420  135 
subsection \<open>Group operations and class instances\<close> 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

136 

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

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

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

139 
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

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

142 

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

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

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

145 
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

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

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

148 

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

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

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

151 
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

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

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

154 

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

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

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

157 
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

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

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

160 

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

161 
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

162 
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

163 

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

164 
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

165 
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

166 

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

167 
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

168 
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

169 

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

170 
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

171 
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

172 

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

173 
instance vec :: (semigroup_add, finite) semigroup_add 
61169  174 
by standard (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

175 

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

176 
instance vec :: (ab_semigroup_add, finite) ab_semigroup_add 
61169  177 
by standard (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

178 

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

179 
instance vec :: (monoid_add, finite) monoid_add 
61169  180 
by standard (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

181 

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

182 
instance vec :: (comm_monoid_add, finite) comm_monoid_add 
61169  183 
by standard (simp add: vec_eq_iff) 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

184 

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

185 
instance vec :: (cancel_semigroup_add, finite) cancel_semigroup_add 
61169  186 
by standard (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

187 

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

188 
instance vec :: (cancel_ab_semigroup_add, finite) cancel_ab_semigroup_add 
61169  189 
by standard (simp_all add: vec_eq_iff diff_diff_eq) 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

190 

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

191 
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

192 

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

193 
instance vec :: (group_add, finite) group_add 
61169  194 
by standard (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

195 

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

196 
instance vec :: (ab_group_add, finite) ab_group_add 
61169  197 
by standard (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

198 

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

199 

60420  200 
subsection \<open>Real vector space\<close> 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

201 

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

202 
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

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

204 

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

205 
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

206 

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

207 
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

208 
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

209 

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

210 
instance 
61169  211 
by standard (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

212 

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

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

214 

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

215 

60420  216 
subsection \<open>Topological space\<close> 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

217 

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

218 
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

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

220 

62101  221 
definition [code del]: 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

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

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

225 

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

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

227 
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

228 
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

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

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

231 
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

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

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

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

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

236 
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

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

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

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

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

241 
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

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

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

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

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

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

247 
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

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

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

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

251 

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

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

253 

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

254 
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

255 
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

256 

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

257 
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

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

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

260 
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

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

262 

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

263 
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

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

265 
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

266 

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

267 
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

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

269 
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

270 
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

271 
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

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

273 

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

274 
lemma tendsto_vec_nth [tendsto_intros]: 
61973  275 
assumes "((\<lambda>x. f x) \<longlongrightarrow> a) net" 
276 
shows "((\<lambda>x. f x $ i) \<longlongrightarrow> a $ i) net" 

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

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

278 
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

279 
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

280 
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

281 
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

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

283 
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

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

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

286 

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

289 

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

290 
lemma vec_tendstoI: 
61973  291 
assumes "\<And>i. ((\<lambda>x. f x $ i) \<longlongrightarrow> a $ i) net" 
292 
shows "((\<lambda>x. f x) \<longlongrightarrow> a) net" 

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

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

294 
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

295 
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

296 
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

297 
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

298 
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

299 
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

300 
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

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

302 
thus "eventually (\<lambda>x. f x \<in> S) net" 
61810  303 
by (rule eventually_mono, simp add: S) 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

305 

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

306 
lemma tendsto_vec_lambda [tendsto_intros]: 
61973  307 
assumes "\<And>i. ((\<lambda>x. f x i) \<longlongrightarrow> a i) net" 
308 
shows "((\<lambda>x. \<chi> i. f x i) \<longlongrightarrow> (\<chi> i. a i)) net" 

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

309 
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

310 

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

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

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

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

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

60420  317 
using \<open>open S\<close> unfolding open_vec_def by auto 
44571  318 
hence "A i \<subseteq> (\<lambda>x. x $ i) ` S" 
319 
by (clarsimp, rule_tac x="\<chi> j. if j = i then x else z $ j" in image_eqI, 

320 
simp_all) 

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

60420  322 
using A \<open>a = z $ i\<close> by simp 
44571  323 
then show "\<exists>T. open T \<and> a \<in> T \<and> T \<subseteq> (\<lambda>x. x $ i) ` S" by  (rule exI) 
324 
qed 

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

325 

44571  326 
instance vec :: (perfect_space, finite) perfect_space 
327 
proof 

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

329 
proof 

330 
assume "open {x}" 

62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

331 
hence "\<forall>i. open ((\<lambda>x. x $ i) ` {x})" by (fast intro: open_image_vec_nth) 
44571  332 
hence "\<forall>i. open {x $ i}" by simp 
333 
thus "False" by (simp add: not_open_singleton) 

334 
qed 

335 
qed 

336 

337 

60420  338 
subsection \<open>Metric space\<close> 
62101  339 
(* TODO: Product of uniform spaces and compatibility with metric_spaces! *) 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

340 

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

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

343 

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

344 
definition 
67155  345 
"dist x y = L2_set (\<lambda>i. dist (x$i) (y$i)) UNIV" 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

346 

62101  347 
instance .. 
348 
end 

349 

350 
instantiation vec :: (metric_space, finite) uniformity_dist 

351 
begin 

352 

353 
definition [code del]: 

62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

354 
"(uniformity :: (('a, 'b) vec \<times> ('a, 'b) vec) filter) = 
62101  355 
(INF e:{0 <..}. principal {(x, y). dist x y < e})" 
356 

62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

357 
instance 
62101  358 
by standard (rule uniformity_vec_def) 
359 
end 

360 

62102
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

361 
declare uniformity_Abort[where 'a="'a :: metric_space ^ 'b :: finite", code] 
877463945ce9
fix code generation for uniformity: uniformity is a noncomputable pure data.
hoelzl
parents:
62101
diff
changeset

362 

62101  363 
instantiation vec :: (metric_space, finite) metric_space 
364 
begin 

365 

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

366 
lemma dist_vec_nth_le: "dist (x $ i) (y $ i) \<le> dist x y" 
67155  367 
unfolding dist_vec_def by (rule member_le_L2_set) simp_all 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

368 

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

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

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

371 
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

372 
unfolding dist_vec_def 
67155  373 
by (simp add: L2_set_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

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

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

376 
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

377 
unfolding dist_vec_def 
67155  378 
apply (rule order_trans [OF _ L2_set_triangle_ineq]) 
379 
apply (simp add: L2_set_mono dist_triangle2) 

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

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

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

382 
fix S :: "('a ^ 'b) set" 
62101  383 
have *: "open S \<longleftrightarrow> (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" 
44630  384 
proof 
385 
assume "open S" show "\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S" 

386 
proof 

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

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

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

60420  390 
using \<open>open S\<close> and \<open>x \<in> S\<close> unfolding open_vec_def by metis 
44630  391 
have "\<forall>i\<in>UNIV. \<exists>r>0. \<forall>y. dist y (x $ i) < r \<longrightarrow> y \<in> A i" 
392 
using A unfolding open_dist by simp 

393 
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

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

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

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

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

400 
qed 

401 
next 

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

403 
proof (unfold open_vec_def, rule) 

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

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

406 
using * by fast 

63040  407 
define r where [abs_def]: "r i = e / sqrt (of_nat CARD('b))" for i :: 'b 
60420  408 
from \<open>0 < e\<close> have r: "\<forall>i. 0 < r i" 
56541  409 
unfolding r_def by simp_all 
67155  410 
from \<open>0 < e\<close> have e: "e = L2_set r UNIV" 
411 
unfolding r_def by (simp add: L2_set_constant) 

63040  412 
define A where "A i = {y. dist (x $ i) y < r i}" for i 
44630  413 
have "\<forall>i. open (A i) \<and> x $ i \<in> A i" 
414 
unfolding A_def by (simp add: open_ball r) 

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

67155  416 
by (simp add: A_def S dist_vec_def e L2_set_strict_mono dist_commute) 
44630  417 
ultimately show "\<exists>A. (\<forall>i. open (A i) \<and> x $ i \<in> A i) \<and> 
418 
(\<forall>y. (\<forall>i. y $ i \<in> A i) \<longrightarrow> y \<in> S)" by metis 

419 
qed 

420 
qed 

62101  421 
show "open S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)" 
422 
unfolding * eventually_uniformity_metric 

423 
by (simp del: split_paired_All add: dist_vec_def dist_commute) 

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

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

425 

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

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

427 

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

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

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

430 
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

431 

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

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

433 
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

434 
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

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

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

437 
fix r :: real assume "0 < r" 
56541  438 
hence "0 < r / of_nat CARD('n)" (is "0 < ?s") by simp 
63040  439 
define N where "N i = (LEAST N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s)" for i 
440 
define M where "M = Max (range N)" 

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

441 
have "\<And>i. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s" 
60420  442 
using X \<open>0 < ?s\<close> by (rule metric_CauchyD) 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

443 
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

444 
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

445 
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

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

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

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

449 
assume "M \<le> m" "M \<le> n" 
67155  450 
have "dist (X m) (X n) = L2_set (\<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

451 
unfolding dist_vec_def .. 
64267  452 
also have "\<dots> \<le> sum (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV" 
67155  453 
by (rule L2_set_le_sum [OF zero_le_dist]) 
64267  454 
also have "\<dots> < sum (\<lambda>i::'n. ?s) UNIV" 
455 
by (rule sum_strict_mono, simp_all add: M \<open>M \<le> m\<close> \<open>M \<le> n\<close>) 

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

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

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

458 
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

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

460 
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

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

462 
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

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

464 

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

465 
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

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

467 
fix X :: "nat \<Rightarrow> 'a ^ 'b" assume "Cauchy X" 
61969  468 
have "\<And>i. (\<lambda>n. X n $ i) \<longlonglongrightarrow> lim (\<lambda>n. X n $ i)" 
60420  469 
using Cauchy_vec_nth [OF \<open>Cauchy X\<close>] 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

470 
by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) 
61969  471 
hence "X \<longlonglongrightarrow> vec_lambda (\<lambda>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

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

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

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

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

476 

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

477 

60420  478 
subsection \<open>Normed vector space\<close> 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

479 

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

480 
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

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

482 

67155  483 
definition "norm x = L2_set (\<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

484 

44141  485 
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

486 

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

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

488 
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

489 
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

490 
unfolding norm_vec_def 
67155  491 
by (simp add: L2_set_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

492 
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

493 
unfolding norm_vec_def 
67155  494 
apply (rule order_trans [OF _ L2_set_triangle_ineq]) 
495 
apply (simp add: L2_set_mono norm_triangle_ineq) 

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

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

497 
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

498 
unfolding norm_vec_def 
67155  499 
by (simp add: L2_set_right_distrib) 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

502 
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

503 
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

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

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

506 

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

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

508 

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

509 
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

510 
unfolding norm_vec_def 
67155  511 
by (rule member_le_L2_set) simp_all 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

512 

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

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

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

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

517 
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

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

519 

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

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

521 

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

522 

60420  523 
subsection \<open>Inner product space\<close> 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

524 

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

525 
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

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

527 

64267  528 
definition "inner x y = sum (\<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

529 

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

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

531 
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

532 
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

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

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

535 
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

536 
unfolding inner_vec_def 
64267  537 
by (simp add: inner_add_left sum.distrib) 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

538 
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

539 
unfolding inner_vec_def 
64267  540 
by (simp add: sum_distrib_left) 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

541 
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

542 
unfolding inner_vec_def 
64267  543 
by (simp add: sum_nonneg) 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

544 
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

545 
unfolding inner_vec_def 
64267  546 
by (simp add: vec_eq_iff sum_nonneg_eq_0_iff) 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

547 
show "norm x = sqrt (inner x x)" 
67155  548 
unfolding inner_vec_def norm_vec_def L2_set_def 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

549 
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

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

551 

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

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

553 

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

554 

60420  555 
subsection \<open>Euclidean space\<close> 
44135
18b4ab6854f1
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
42290
diff
changeset

556 

60420  557 
text \<open>Vectors pointing along a single axis.\<close> 
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

558 

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

559 
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

560 

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

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

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

563 

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

564 
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

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

566 

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

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

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

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

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

571 
apply clarsimp 
64267  572 
apply (subst sum.remove [of _ j], simp_all) 
573 
apply (rule sum.neutral, simp add: axis_def) 

574 
apply (rule sum.neutral, simp add: axis_def) 

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

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

576 

64267  577 
lemma sum_single: 
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

578 
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

579 
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

580 
shows "(\<Sum>i\<in>A. f i) = y" 
64267  581 
apply (subst sum.remove [OF assms(1,2)]) 
582 
apply (simp add: sum.neutral assms(3,4)) 

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

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

584 

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

585 
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

586 
unfolding inner_vec_def 
64267  587 
apply (rule_tac k=i in sum_single) 
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44165
diff
changeset

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

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

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

591 

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

592 
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

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

594 

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

595 
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

596 

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

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

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

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

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

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

602 
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

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

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

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

606 
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

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

608 
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

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

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

611 
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

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

613 
by (simp add: inner_axis euclidean_all_zero_iff vec_eq_iff) 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50252
diff
changeset

614 
qed 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50252
diff
changeset

615 

899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50252
diff
changeset

616 
lemma DIM_cart[simp]: "DIM('a^'b) = CARD('b) * DIM('a)" 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50252
diff
changeset

617 
apply (simp add: Basis_vec_def) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50252
diff
changeset

618 
apply (subst card_UN_disjoint) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50252
diff
changeset

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

620 
apply simp 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50252
diff
changeset

621 
apply (auto simp: axis_eq_axis) [1] 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50252
diff
changeset

622 
apply (subst card_UN_disjoint) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50252
diff
changeset

623 
apply (auto simp: axis_eq_axis) 
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
50252
diff
changeset

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

625 

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

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

627 

62397
5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
62102
diff
changeset

628 
lemma cart_eq_inner_axis: "a $ i = inner a (axis i 1)" 
5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
62102
diff
changeset

629 
by (simp add: inner_axis) 
5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
62102
diff
changeset

630 

5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
62102
diff
changeset

631 
lemma axis_in_Basis: "a \<in> Basis \<Longrightarrow> axis i a \<in> Basis" 
5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
62102
diff
changeset

632 
by (auto simp add: Basis_vec_def axis_eq_axis) 
5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
62102
diff
changeset

633 

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

634 
end 