author  wenzelm 
Wed, 28 Feb 2018 16:30:25 +0100  
changeset 67732  39d80006fc29 
parent 67731  184c293f0a33 
child 67968  a5ad4c015d1c 
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 

67731  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 

67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset

21 
declare vec_lambda_inject [simplified, simp] 
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset

22 

67685
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67673
diff
changeset

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

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

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

26 
vec_lambda (binder "\<chi>" 10) 
67685
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67673
diff
changeset

27 
end 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67673
diff
changeset

28 

bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67673
diff
changeset

29 
bundle no_vec_syntax begin 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67673
diff
changeset

30 
no_notation 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67673
diff
changeset

31 
vec_nth (infixl "$" 90) and 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67673
diff
changeset

32 
vec_lambda (binder "\<chi>" 10) 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67673
diff
changeset

33 
end 
bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67673
diff
changeset

34 

bdff8bf0a75b
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations
immler
parents:
67673
diff
changeset

35 
unbundle vec_syntax 
33175  36 

67731  37 
text \<open> 
38 
Concrete syntax for \<open>('a, 'b) vec\<close>: 

39 
\<^item> \<open>'a^'b\<close> becomes \<open>('a, 'b::finite) vec\<close> 

40 
\<^item> \<open>'a^'b::_\<close> becomes \<open>('a, 'b) vec\<close> without extra sortconstraint 

41 
\<close> 

67732  42 
syntax "_vec_type" :: "type \<Rightarrow> type \<Rightarrow> type" (infixl "^" 15) 
60420  43 
parse_translation \<open> 
52143  44 
let 
45 
fun vec t u = Syntax.const @{type_syntax vec} $ t $ u; 

46 
fun finite_vec_tr [t, u] = 

47 
(case Term_Position.strip_positions u of 

48 
v as Free (x, _) => 

49 
if Lexicon.is_tid x then 

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

51 
Syntax.const @{class_syntax finite}) 

52 
else vec t u 

53 
 _ => vec t u) 

54 
in 

67732  55 
[(@{syntax_const "_vec_type"}, K finite_vec_tr)] 
52143  56 
end 
60420  57 
\<close> 
34290
1edf0f223c6e
added syntax translation to automatically add finite typeclass to index type of cartesian product type
hoelzl
parents:
34289
diff
changeset

58 

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

59 
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

60 
by (simp add: vec_nth_inject [symmetric] fun_eq_iff) 
33175  61 

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

62 
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

63 
by (simp add: vec_lambda_inverse) 
33175  64 

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

65 
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

66 
by (auto simp add: vec_eq_iff) 
33175  67 

67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset

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

69 
by (simp add: vec_eq_iff) 
33175  70 

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

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

72 

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

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

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

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

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

77 
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

78 
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

79 
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

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

81 
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

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

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

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

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

86 

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

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

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

89 
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

90 

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

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

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

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

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

95 
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

96 
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

97 
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

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

99 
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

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

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

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

103 
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

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

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

106 

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

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

108 
assumes "infinite (UNIV :: 'a set)" 
67731  109 
shows "infinite (UNIV :: ('a^'b) set)" 
66281
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

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

111 
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

112 
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

113 
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

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

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

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

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

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

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

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

121 
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

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

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

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

125 
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

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

127 

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

128 
lemma CARD_vec [simp]: 
67731  129 
"CARD('a^'b) = CARD('a) ^ CARD('b)" 
66281
6ad54b84ca5d
facts about cardinality of vector type
eberlm <eberlm@in.tum.de>
parents:
64267
diff
changeset

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

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

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

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

134 
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

135 
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

136 
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

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

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

139 

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

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

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

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

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

144 
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

145 

67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

146 
lemma countable_vector: 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

147 
fixes B:: "'n::finite \<Rightarrow> 'a set" 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

148 
assumes "\<And>i. countable (B i)" 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

149 
shows "countable {V. \<forall>i::'n::finite. V $ i \<in> B i}" 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

150 
proof  
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

151 
have "f \<in> ($) ` {V. \<forall>i. V $ i \<in> B i}" if "f \<in> Pi\<^sub>E UNIV B" for f 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

152 
proof  
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

153 
have "\<exists>W. (\<forall>i. W $ i \<in> B i) \<and> ($) W = f" 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

154 
by (metis that PiE_iff UNIV_I vec_lambda_inverse) 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

155 
then show "f \<in> ($) ` {v. \<forall>i. v $ i \<in> B i}" 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

156 
by blast 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

157 
qed 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

158 
then have "Pi\<^sub>E UNIV B = vec_nth ` {V. \<forall>i::'n. V $ i \<in> B i}" 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

159 
by blast 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

160 
then have "countable (vec_nth ` {V. \<forall>i. V $ i \<in> B i})" 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

161 
by (metis finite_class.finite_UNIV countable_PiE assms) 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

162 
then have "countable (vec_lambda ` vec_nth ` {V. \<forall>i. V $ i \<in> B i})" 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

163 
by auto 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

164 
then show ?thesis 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

165 
by (simp add: image_comp o_def vec_nth_inverse) 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

166 
qed 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

167 

60420  168 
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

169 

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

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

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

172 
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

173 
instance .. 
33175  174 
end 
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 
instantiation vec :: (plus, finite) plus 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

177 
begin 
67399  178 
definition "(+) \<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

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

180 
end 
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 
instantiation vec :: (minus, finite) minus 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

183 
begin 
67399  184 
definition "() \<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

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

186 
end 
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 
instantiation vec :: (uminus, finite) uminus 
36591
df38e0c5c123
move class instantiations from Euclidean_Space.thy to Finite_Cartesian_Product.thy
huffman
parents:
36590
diff
changeset

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

190 
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

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

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

193 

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

194 
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

195 
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

196 

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

197 
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

198 
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

199 

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

200 
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

201 
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

202 

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

203 
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

204 
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

205 

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

206 
instance vec :: (semigroup_add, finite) semigroup_add 
61169  207 
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

208 

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

209 
instance vec :: (ab_semigroup_add, finite) ab_semigroup_add 
61169  210 
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

211 

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

212 
instance vec :: (monoid_add, finite) monoid_add 
61169  213 
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

214 

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

215 
instance vec :: (comm_monoid_add, finite) comm_monoid_add 
61169  216 
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

217 

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

218 
instance vec :: (cancel_semigroup_add, finite) cancel_semigroup_add 
61169  219 
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

220 

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

221 
instance vec :: (cancel_ab_semigroup_add, finite) cancel_ab_semigroup_add 
61169  222 
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

223 

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

224 
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

225 

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

226 
instance vec :: (group_add, finite) group_add 
61169  227 
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

228 

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

229 
instance vec :: (ab_group_add, finite) ab_group_add 
61169  230 
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

231 

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

232 

60420  233 
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

234 

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

235 
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

236 
begin 
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 
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

239 

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

240 
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

241 
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

242 

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

243 
instance 
61169  244 
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

245 

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

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

247 

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

248 

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

250 

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

251 
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

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

253 

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

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

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

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

258 

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

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

260 
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

261 
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

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

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

264 
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

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

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

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

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

269 
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

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

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

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

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

274 
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

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

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

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

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

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

280 
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

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

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

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

284 

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

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

286 

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

287 
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

288 
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

289 

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

290 
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

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

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

293 
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

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

295 

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

296 
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

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

298 
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

299 

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

300 
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

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

302 
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

303 
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

304 
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

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

306 

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

307 
lemma tendsto_vec_nth [tendsto_intros]: 
61973  308 
assumes "((\<lambda>x. f x) \<longlongrightarrow> a) net" 
309 
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

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

311 
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

312 
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

313 
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

314 
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

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

316 
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

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

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

319 

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

322 

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

323 
lemma vec_tendstoI: 
61973  324 
assumes "\<And>i. ((\<lambda>x. f x $ i) \<longlongrightarrow> a $ i) net" 
325 
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

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

327 
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

328 
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

329 
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

330 
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

331 
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

332 
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

333 
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

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

335 
thus "eventually (\<lambda>x. f x \<in> S) net" 
61810  336 
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

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

338 

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

339 
lemma tendsto_vec_lambda [tendsto_intros]: 
61973  340 
assumes "\<And>i. ((\<lambda>x. f x i) \<longlongrightarrow> a i) net" 
341 
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

342 
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

343 

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

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

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

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

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

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

353 
simp_all) 

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

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

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

358 

44571  359 
instance vec :: (perfect_space, finite) perfect_space 
360 
proof 

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

362 
proof 

363 
assume "open {x}" 

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

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

367 
qed 

368 
qed 

369 

370 

60420  371 
subsection \<open>Metric space\<close> 
62101  372 
(* 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

373 

62101  374 
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

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

376 

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

377 
definition 
67155  378 
"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

379 

62101  380 
instance .. 
381 
end 

382 

383 
instantiation vec :: (metric_space, finite) uniformity_dist 

384 
begin 

385 

386 
definition [code del]: 

67731  387 
"(uniformity :: (('a^'b::_) \<times> ('a^'b::_)) filter) = 
62101  388 
(INF e:{0 <..}. principal {(x, y). dist x y < e})" 
389 

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

390 
instance 
62101  391 
by standard (rule uniformity_vec_def) 
392 
end 

393 

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

394 
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

395 

62101  396 
instantiation vec :: (metric_space, finite) metric_space 
397 
begin 

398 

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

399 
lemma dist_vec_nth_le: "dist (x $ i) (y $ i) \<le> dist x y" 
67155  400 
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

401 

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

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

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

404 
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

405 
unfolding dist_vec_def 
67155  406 
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

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

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

409 
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

410 
unfolding dist_vec_def 
67155  411 
apply (rule order_trans [OF _ L2_set_triangle_ineq]) 
412 
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

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

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

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

419 
proof 

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

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

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

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

426 
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

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

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

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

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

433 
qed 

434 
next 

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

436 
proof (unfold open_vec_def, rule) 

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

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

439 
using * by fast 

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

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

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

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

452 
qed 

453 
qed 

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

456 
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

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

458 

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

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

460 

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

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

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

463 
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

464 

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

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

466 
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

467 
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

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

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

470 
fix r :: real assume "0 < r" 
56541  471 
hence "0 < r / of_nat CARD('n)" (is "0 < ?s") by simp 
63040  472 
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 
473 
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

474 
have "\<And>i. \<exists>N. \<forall>m\<ge>N. \<forall>n\<ge>N. dist (X m $ i) (X n $ i) < ?s" 
60420  475 
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

476 
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

477 
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

478 
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

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

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

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

482 
assume "M \<le> m" "M \<le> n" 
67155  483 
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

484 
unfolding dist_vec_def .. 
64267  485 
also have "\<dots> \<le> sum (\<lambda>i. dist (X m $ i) (X n $ i)) UNIV" 
67155  486 
by (rule L2_set_le_sum [OF zero_le_dist]) 
64267  487 
also have "\<dots> < sum (\<lambda>i::'n. ?s) UNIV" 
488 
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

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

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

491 
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

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

493 
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

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

495 
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

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

497 

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

498 
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

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

500 
fix X :: "nat \<Rightarrow> 'a ^ 'b" assume "Cauchy X" 
61969  501 
have "\<And>i. (\<lambda>n. X n $ i) \<longlonglongrightarrow> lim (\<lambda>n. X n $ i)" 
60420  502 
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

503 
by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) 
61969  504 
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

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

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

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

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

509 

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

510 

60420  511 
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

512 

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

513 
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

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

515 

67155  516 
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

517 

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

519 

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

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

521 
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

522 
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

523 
unfolding norm_vec_def 
67155  524 
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

525 
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

526 
unfolding norm_vec_def 
67155  527 
apply (rule order_trans [OF _ L2_set_triangle_ineq]) 
528 
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

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

530 
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

531 
unfolding norm_vec_def 
67155  532 
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

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

535 
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

536 
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

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

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

539 

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

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

541 

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

542 
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

543 
unfolding norm_vec_def 
67155  544 
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

545 

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

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

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

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

550 
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

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

552 

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

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

554 

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

555 

60420  556 
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

557 

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

558 
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

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

560 

64267  561 
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

562 

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

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

564 
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

565 
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

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

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

568 
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

569 
unfolding inner_vec_def 
64267  570 
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

571 
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

572 
unfolding inner_vec_def 
64267  573 
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

574 
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

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

577 
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

578 
unfolding inner_vec_def 
64267  579 
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

580 
show "norm x = sqrt (inner x x)" 
67155  581 
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

582 
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

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

584 

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

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

586 

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

587 

60420  588 
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

589 

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

591 

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

592 
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

593 

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

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

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

596 

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

597 
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

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

599 

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

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

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

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

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

604 
apply clarsimp 
64267  605 
apply (subst sum.remove [of _ j], simp_all) 
606 
apply (rule sum.neutral, simp add: axis_def) 

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

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

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

609 

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

611 
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

612 
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

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

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

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

617 

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

618 
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

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

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

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

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

624 

67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

625 
lemma inner_axis': "inner(axis i y) x = inner y (x $ i)" 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

626 
by (simp add: inner_axis inner_commute) 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

627 

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

628 
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

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

630 

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

631 
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

632 

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

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

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

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

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

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

638 
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

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

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

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

642 
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

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

644 
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

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

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

647 
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

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

649 
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

650 
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

651 

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

652 
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

653 
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

654 
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

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

656 
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

657 
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

658 
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

659 
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

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

661 

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

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

663 

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

664 
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

665 
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

666 

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

667 
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

668 
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

669 

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

670 
end 