author | huffman |
Thu, 11 Aug 2011 13:05:56 -0700 | |
changeset 44166 | d12d89a66742 |
parent 44133 | 691c52e900ca |
child 44215 | 786876687ef8 |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Multivariate_Analysis/Euclidean_Space.thy |
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
2 |
Author: Johannes Hölzl, TU München |
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
3 |
Author: Brian Huffman, Portland State University |
33175 | 4 |
*) |
5 |
||
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
6 |
header {* Finite-Dimensional Inner Product Spaces *} |
33175 | 7 |
|
8 |
theory Euclidean_Space |
|
9 |
imports |
|
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
40786
diff
changeset
|
10 |
Complex_Main |
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
40786
diff
changeset
|
11 |
"~~/src/HOL/Library/Inner_Product" |
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
12 |
"~~/src/HOL/Library/Product_Vector" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
13 |
begin |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
14 |
|
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
15 |
subsection {* Type class of Euclidean spaces *} |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
16 |
|
44129 | 17 |
class euclidean_space = real_inner + |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
18 |
fixes Basis :: "'a set" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
19 |
assumes nonempty_Basis [simp]: "Basis \<noteq> {}" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
20 |
assumes finite_Basis [simp]: "finite Basis" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
21 |
assumes inner_Basis: |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
22 |
"\<lbrakk>u \<in> Basis; v \<in> Basis\<rbrakk> \<Longrightarrow> inner u v = (if u = v then 1 else 0)" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
23 |
assumes euclidean_all_zero_iff: |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
24 |
"(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> (x = 0)" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
25 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
26 |
-- "FIXME: make this a separate definition" |
44129 | 27 |
fixes dimension :: "'a itself \<Rightarrow> nat" |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
28 |
assumes dimension_def: "dimension TYPE('a) = card Basis" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
29 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
30 |
-- "FIXME: eventually basis function can be removed" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
31 |
fixes basis :: "nat \<Rightarrow> 'a" |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
32 |
assumes image_basis: "basis ` {..<dimension TYPE('a)} = Basis" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
33 |
assumes basis_finite: "basis ` {dimension TYPE('a)..} = {0}" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
34 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
35 |
syntax "_type_dimension" :: "type => nat" ("(1DIM/(1'(_')))") |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
36 |
|
37646 | 37 |
translations "DIM('t)" == "CONST dimension (TYPE('t))" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
38 |
|
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
39 |
lemma (in euclidean_space) norm_Basis: "u \<in> Basis \<Longrightarrow> norm u = 1" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
40 |
unfolding norm_eq_sqrt_inner by (simp add: inner_Basis) |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
41 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
42 |
lemma (in euclidean_space) sgn_Basis: "u \<in> Basis \<Longrightarrow> sgn u = u" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
43 |
unfolding sgn_div_norm by (simp add: norm_Basis scaleR_one) |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
44 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
45 |
lemma (in euclidean_space) Basis_zero [simp]: "0 \<notin> Basis" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
46 |
proof |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
47 |
assume "0 \<in> Basis" thus "False" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
48 |
using inner_Basis [of 0 0] by simp |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
49 |
qed |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
50 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
51 |
lemma (in euclidean_space) nonzero_Basis: "u \<in> Basis \<Longrightarrow> u \<noteq> 0" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
52 |
by clarsimp |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
53 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
54 |
text {* Lemmas related to @{text basis} function. *} |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
55 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
56 |
lemma (in euclidean_space) euclidean_all_zero: |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
57 |
"(\<forall>i<DIM('a). inner (basis i) x = 0) \<longleftrightarrow> (x = 0)" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
58 |
using euclidean_all_zero_iff [of x, folded image_basis] |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
59 |
unfolding ball_simps by (simp add: Ball_def inner_commute) |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
60 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
61 |
lemma (in euclidean_space) basis_zero [simp]: |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
62 |
"DIM('a) \<le> i \<Longrightarrow> basis i = 0" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
63 |
using basis_finite by auto |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
64 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
65 |
lemma (in euclidean_space) DIM_positive [intro]: "0 < DIM('a)" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
66 |
unfolding dimension_def by (simp add: card_gt_0_iff) |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
67 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
68 |
lemma (in euclidean_space) basis_inj [simp, intro]: "inj_on basis {..<DIM('a)}" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
69 |
by (simp add: inj_on_iff_eq_card image_basis dimension_def [symmetric]) |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
70 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
71 |
lemma (in euclidean_space) basis_in_Basis [simp]: |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
72 |
"basis i \<in> Basis \<longleftrightarrow> i < DIM('a)" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
73 |
by (cases "i < DIM('a)", simp add: image_basis [symmetric], simp) |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
74 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
75 |
lemma (in euclidean_space) Basis_elim: |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
76 |
assumes "u \<in> Basis" obtains i where "i < DIM('a)" and "u = basis i" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
77 |
using assms unfolding image_basis [symmetric] by fast |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
78 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
79 |
lemma (in euclidean_space) basis_orthonormal: |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
80 |
"\<forall>i<DIM('a). \<forall>j<DIM('a). |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
81 |
inner (basis i) (basis j) = (if i = j then 1 else 0)" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
82 |
apply clarify |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
83 |
apply (simp add: inner_Basis) |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
84 |
apply (simp add: basis_inj [unfolded inj_on_def]) |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
85 |
done |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
86 |
|
44129 | 87 |
lemma (in euclidean_space) dot_basis: |
88 |
"inner (basis i) (basis j) = (if i = j \<and> i < DIM('a) then 1 else 0)" |
|
89 |
proof (cases "(i < DIM('a) \<and> j < DIM('a))") |
|
90 |
case False |
|
91 |
hence "inner (basis i) (basis j) = 0" by auto |
|
92 |
thus ?thesis using False by auto |
|
93 |
next |
|
94 |
case True thus ?thesis using basis_orthonormal by auto |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
95 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
96 |
|
44129 | 97 |
lemma (in euclidean_space) basis_eq_0_iff [simp]: |
98 |
"basis i = 0 \<longleftrightarrow> DIM('a) \<le> i" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
99 |
proof - |
44129 | 100 |
have "inner (basis i) (basis i) = 0 \<longleftrightarrow> DIM('a) \<le> i" |
101 |
by (simp add: dot_basis) |
|
102 |
thus ?thesis by simp |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
103 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
104 |
|
44129 | 105 |
lemma (in euclidean_space) norm_basis [simp]: |
106 |
"norm (basis i) = (if i < DIM('a) then 1 else 0)" |
|
107 |
unfolding norm_eq_sqrt_inner dot_basis by simp |
|
108 |
||
109 |
lemma (in euclidean_space) basis_neq_0 [intro]: |
|
110 |
assumes "i<DIM('a)" shows "(basis i) \<noteq> 0" |
|
111 |
using assms by simp |
|
112 |
||
113 |
subsubsection {* Projecting components *} |
|
114 |
||
115 |
definition (in euclidean_space) euclidean_component (infixl "$$" 90) |
|
116 |
where "x $$ i = inner (basis i) x" |
|
117 |
||
118 |
lemma bounded_linear_euclidean_component: |
|
119 |
"bounded_linear (\<lambda>x. euclidean_component x i)" |
|
120 |
unfolding euclidean_component_def |
|
121 |
by (rule inner.bounded_linear_right) |
|
122 |
||
123 |
interpretation euclidean_component: |
|
124 |
bounded_linear "\<lambda>x. euclidean_component x i" |
|
125 |
by (rule bounded_linear_euclidean_component) |
|
126 |
||
127 |
lemma euclidean_eqI: |
|
128 |
fixes x y :: "'a::euclidean_space" |
|
129 |
assumes "\<And>i. i < DIM('a) \<Longrightarrow> x $$ i = y $$ i" shows "x = y" |
|
130 |
proof - |
|
131 |
from assms have "\<forall>i<DIM('a). (x - y) $$ i = 0" |
|
132 |
by (simp add: euclidean_component.diff) |
|
133 |
then show "x = y" |
|
134 |
unfolding euclidean_component_def euclidean_all_zero by simp |
|
135 |
qed |
|
136 |
||
137 |
lemma euclidean_eq: |
|
138 |
fixes x y :: "'a::euclidean_space" |
|
139 |
shows "x = y \<longleftrightarrow> (\<forall>i<DIM('a). x $$ i = y $$ i)" |
|
140 |
by (auto intro: euclidean_eqI) |
|
141 |
||
142 |
lemma (in euclidean_space) basis_component [simp]: |
|
143 |
"basis i $$ j = (if i = j \<and> i < DIM('a) then 1 else 0)" |
|
144 |
unfolding euclidean_component_def dot_basis by auto |
|
145 |
||
146 |
lemma (in euclidean_space) basis_at_neq_0 [intro]: |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
147 |
"i < DIM('a) \<Longrightarrow> basis i $$ i \<noteq> 0" |
44129 | 148 |
by simp |
149 |
||
150 |
lemma (in euclidean_space) euclidean_component_ge [simp]: |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
151 |
assumes "i \<ge> DIM('a)" shows "x $$ i = 0" |
44129 | 152 |
unfolding euclidean_component_def basis_zero[OF assms] by simp |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
153 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
154 |
lemma euclidean_scaleR: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
155 |
shows "(a *\<^sub>R x) $$ i = a * (x$$i)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
156 |
unfolding euclidean_component_def by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
157 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
158 |
lemmas euclidean_simps = |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
159 |
euclidean_component.add |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
160 |
euclidean_component.diff |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
161 |
euclidean_scaleR |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
162 |
euclidean_component.minus |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
163 |
euclidean_component.setsum |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
164 |
basis_component |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
165 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
166 |
lemma euclidean_representation: |
44129 | 167 |
fixes x :: "'a::euclidean_space" |
168 |
shows "x = (\<Sum>i<DIM('a). (x$$i) *\<^sub>R basis i)" |
|
169 |
apply (rule euclidean_eqI) |
|
170 |
apply (simp add: euclidean_component.setsum euclidean_component.scaleR) |
|
171 |
apply (simp add: if_distrib setsum_delta cong: if_cong) |
|
172 |
done |
|
173 |
||
174 |
subsubsection {* Binder notation for vectors *} |
|
175 |
||
176 |
definition (in euclidean_space) Chi (binder "\<chi>\<chi> " 10) where |
|
177 |
"(\<chi>\<chi> i. f i) = (\<Sum>i<DIM('a). f i *\<^sub>R basis i)" |
|
178 |
||
179 |
lemma euclidean_lambda_beta [simp]: |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
180 |
"((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = (if j < DIM('a) then f j else 0)" |
44129 | 181 |
by (auto simp: euclidean_component.setsum euclidean_component.scaleR |
182 |
Chi_def if_distrib setsum_cases intro!: setsum_cong) |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
183 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
184 |
lemma euclidean_lambda_beta': |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
185 |
"j < DIM('a) \<Longrightarrow> ((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = f j" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
186 |
by simp |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
187 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
188 |
lemma euclidean_lambda_beta'':"(\<forall>j < DIM('a::euclidean_space). P j (((\<chi>\<chi> i. f i)::'a) $$ j)) \<longleftrightarrow> |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
189 |
(\<forall>j < DIM('a::euclidean_space). P j (f j))" by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
190 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
191 |
lemma euclidean_beta_reduce[simp]: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
192 |
"(\<chi>\<chi> i. x $$ i) = (x::'a::euclidean_space)" |
44129 | 193 |
by (simp add: euclidean_eq) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
194 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
195 |
lemma euclidean_lambda_beta_0[simp]: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
196 |
"((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ 0 = f 0" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
197 |
by (simp add: DIM_positive) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
198 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
199 |
lemma euclidean_inner: |
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
200 |
"inner x (y::'a) = (\<Sum>i<DIM('a::euclidean_space). (x $$ i) * (y $$ i))" |
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
201 |
by (subst (1 2) euclidean_representation, |
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
202 |
simp add: inner_left.setsum inner_right.setsum |
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
203 |
dot_basis if_distrib setsum_cases mult_commute) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
204 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
205 |
lemma component_le_norm: "\<bar>x$$i\<bar> \<le> norm (x::'a::euclidean_space)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
206 |
unfolding euclidean_component_def |
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
207 |
by (rule order_trans [OF Cauchy_Schwarz_ineq2]) simp |
33175 | 208 |
|
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
209 |
subsection {* Class instances *} |
33175 | 210 |
|
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
211 |
subsubsection {* Type @{typ real} *} |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
212 |
|
44129 | 213 |
instantiation real :: euclidean_space |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
214 |
begin |
44129 | 215 |
|
216 |
definition |
|
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
217 |
"Basis = {1::real}" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
218 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
219 |
definition |
44129 | 220 |
"dimension (t::real itself) = 1" |
221 |
||
222 |
definition [simp]: |
|
223 |
"basis i = (if i = 0 then 1 else (0::real))" |
|
224 |
||
225 |
lemma DIM_real [simp]: "DIM(real) = 1" |
|
226 |
by (rule dimension_real_def) |
|
227 |
||
228 |
instance |
|
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
229 |
by default (auto simp add: Basis_real_def) |
44129 | 230 |
|
231 |
end |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
232 |
|
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
233 |
subsubsection {* Type @{typ complex} *} |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
234 |
|
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
235 |
(* TODO: move these to Complex.thy/Inner_Product.thy *) |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
236 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
237 |
lemma norm_ii [simp]: "norm ii = 1" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
238 |
unfolding i_def by simp |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
239 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
240 |
lemma complex_inner_1 [simp]: "inner 1 x = Re x" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
241 |
unfolding inner_complex_def by simp |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
242 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
243 |
lemma complex_inner_1_right [simp]: "inner x 1 = Re x" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
244 |
unfolding inner_complex_def by simp |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
245 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
246 |
lemma complex_inner_ii_left [simp]: "inner ii x = Im x" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
247 |
unfolding inner_complex_def by simp |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
248 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
249 |
lemma complex_inner_ii_right [simp]: "inner x ii = Im x" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
250 |
unfolding inner_complex_def by simp |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
251 |
|
44129 | 252 |
instantiation complex :: euclidean_space |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
253 |
begin |
44129 | 254 |
|
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
255 |
definition Basis_complex_def: |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
256 |
"Basis = {1, ii}" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
257 |
|
44129 | 258 |
definition |
259 |
"dimension (t::complex itself) = 2" |
|
260 |
||
261 |
definition |
|
262 |
"basis i = (if i = 0 then 1 else if i = 1 then ii else 0)" |
|
263 |
||
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
264 |
instance |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
265 |
by default (auto simp add: Basis_complex_def dimension_complex_def |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
266 |
basis_complex_def intro: complex_eqI split: split_if_asm) |
44129 | 267 |
|
268 |
end |
|
269 |
||
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
270 |
lemma DIM_complex[simp]: "DIM(complex) = 2" |
44129 | 271 |
by (rule dimension_complex_def) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
272 |
|
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
273 |
subsubsection {* Type @{typ "'a \<times> 'b"} *} |
38656 | 274 |
|
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
275 |
lemma disjoint_iff: "A \<inter> B = {} \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<noteq> y)" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
276 |
by auto (* TODO: move elsewhere *) |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
277 |
|
44129 | 278 |
instantiation prod :: (euclidean_space, euclidean_space) euclidean_space |
38656 | 279 |
begin |
280 |
||
44129 | 281 |
definition |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
282 |
"Basis = (\<lambda>u. (u, 0)) ` Basis \<union> (\<lambda>v. (0, v)) ` Basis" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
283 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
284 |
definition |
44129 | 285 |
"dimension (t::('a \<times> 'b) itself) = DIM('a) + DIM('b)" |
286 |
||
287 |
definition |
|
288 |
"basis i = (if i < DIM('a) then (basis i, 0) else (0, basis (i - DIM('a))))" |
|
289 |
||
290 |
instance proof |
|
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
291 |
show "(Basis :: ('a \<times> 'b) set) \<noteq> {}" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
292 |
unfolding Basis_prod_def by simp |
44129 | 293 |
next |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
294 |
show "finite (Basis :: ('a \<times> 'b) set)" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
295 |
unfolding Basis_prod_def by simp |
44129 | 296 |
next |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
297 |
fix u v :: "'a \<times> 'b" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
298 |
assume "u \<in> Basis" and "v \<in> Basis" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
299 |
thus "inner u v = (if u = v then 1 else 0)" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
300 |
unfolding Basis_prod_def inner_prod_def |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
301 |
by (auto simp add: inner_Basis split: split_if_asm) |
44129 | 302 |
next |
303 |
fix x :: "'a \<times> 'b" |
|
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
304 |
show "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> x = 0" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
305 |
unfolding Basis_prod_def ball_Un ball_simps |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
306 |
by (simp add: inner_prod_def prod_eq_iff euclidean_all_zero_iff) |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
307 |
next |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
308 |
show "DIM('a \<times> 'b) = card (Basis :: ('a \<times> 'b) set)" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
309 |
unfolding dimension_prod_def Basis_prod_def |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
310 |
by (simp add: card_Un_disjoint disjoint_iff |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
311 |
card_image inj_on_def dimension_def) |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
312 |
next |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
313 |
show "basis ` {..<DIM('a \<times> 'b)} = (Basis :: ('a \<times> 'b) set)" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
314 |
by (auto simp add: Basis_prod_def dimension_prod_def basis_prod_def |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
315 |
image_def elim!: Basis_elim) |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
316 |
next |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
317 |
show "basis ` {DIM('a \<times> 'b)..} = {0::('a \<times> 'b)}" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
318 |
by (auto simp add: dimension_prod_def basis_prod_def prod_eq_iff image_def) |
38656 | 319 |
qed |
44129 | 320 |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
321 |
end |
38656 | 322 |
|
323 |
end |