author | hoelzl |
Fri, 14 Dec 2012 15:46:01 +0100 | |
changeset 50526 | 899c9c4e4a4c |
parent 44902 | 9ba11d41cd1f |
child 53939 | eb25bddf6a22 |
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 |
|
44628
bd17b7543af1
move lemmas from Topology_Euclidean_Space to Euclidean_Space
huffman
parents:
44571
diff
changeset
|
10 |
L2_Norm |
41413
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 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
26 |
abbreviation dimension :: "('a::euclidean_space) itself \<Rightarrow> nat" where |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
27 |
"dimension TYPE('a) \<equiv> card (Basis :: 'a set)" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
28 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
29 |
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
|
30 |
|
37646 | 31 |
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
|
32 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
33 |
lemma (in euclidean_space) norm_Basis[simp]: "u \<in> Basis \<Longrightarrow> norm u = 1" |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
34 |
unfolding norm_eq_sqrt_inner by (simp add: inner_Basis) |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
35 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
36 |
lemma (in euclidean_space) inner_same_Basis[simp]: "u \<in> Basis \<Longrightarrow> inner u u = 1" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
37 |
by (simp add: inner_Basis) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
38 |
|
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
39 |
lemma (in euclidean_space) inner_not_same_Basis: "u \<in> Basis \<Longrightarrow> v \<in> Basis \<Longrightarrow> u \<noteq> v \<Longrightarrow> inner u v = 0" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
40 |
by (simp add: inner_Basis) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
41 |
|
44166
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" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
43 |
unfolding sgn_div_norm by (simp add: scaleR_one) |
44166
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 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
54 |
lemma (in euclidean_space) SOME_Basis: "(SOME i. i \<in> Basis) \<in> Basis" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
55 |
by (metis ex_in_conv nonempty_Basis someI_ex) |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
56 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
57 |
lemma (in euclidean_space) inner_setsum_left_Basis[simp]: |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
58 |
"b \<in> Basis \<Longrightarrow> inner (\<Sum>i\<in>Basis. f i *\<^sub>R i) b = f b" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
59 |
by (simp add: inner_setsum_left inner_Basis if_distrib setsum_cases) |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
60 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
61 |
lemma (in euclidean_space) euclidean_eqI: |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
62 |
assumes b: "\<And>b. b \<in> Basis \<Longrightarrow> inner x b = inner y b" shows "x = y" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
63 |
proof - |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
64 |
from b have "\<forall>b\<in>Basis. inner (x - y) b = 0" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
65 |
by (simp add: inner_diff_left) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
66 |
then show "x = y" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
67 |
by (simp add: euclidean_all_zero_iff) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
68 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
69 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
70 |
lemma (in euclidean_space) euclidean_eq_iff: |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
71 |
"x = y \<longleftrightarrow> (\<forall>b\<in>Basis. inner x b = inner y b)" |
44129 | 72 |
by (auto intro: euclidean_eqI) |
73 |
||
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
74 |
lemma (in euclidean_space) euclidean_representation_setsum: |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
75 |
"(\<Sum>i\<in>Basis. f i *\<^sub>R i) = b \<longleftrightarrow> (\<forall>i\<in>Basis. f i = inner b i)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
76 |
by (subst euclidean_eq_iff) 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
|
77 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
78 |
lemma (in euclidean_space) euclidean_representation: "(\<Sum>b\<in>Basis. inner x b *\<^sub>R b) = x" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
79 |
unfolding euclidean_representation_setsum by simp |
44129 | 80 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
81 |
lemma (in euclidean_space) choice_Basis_iff: |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
82 |
fixes P :: "'a \<Rightarrow> real \<Rightarrow> bool" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
83 |
shows "(\<forall>i\<in>Basis. \<exists>x. P i x) \<longleftrightarrow> (\<exists>x. \<forall>i\<in>Basis. P i (inner x i))" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
84 |
unfolding bchoice_iff |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
85 |
proof safe |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
86 |
fix f assume "\<forall>i\<in>Basis. P i (f i)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
87 |
then show "\<exists>x. \<forall>i\<in>Basis. P i (inner x i)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
88 |
by (auto intro!: exI[of _ "\<Sum>i\<in>Basis. f i *\<^sub>R i"]) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
89 |
qed 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
|
90 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
91 |
lemma DIM_positive: "0 < DIM('a::euclidean_space)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
92 |
by (simp add: card_gt_0_iff) |
44628
bd17b7543af1
move lemmas from Topology_Euclidean_Space to Euclidean_Space
huffman
parents:
44571
diff
changeset
|
93 |
|
44571 | 94 |
subsection {* Subclass relationships *} |
95 |
||
96 |
instance euclidean_space \<subseteq> perfect_space |
|
97 |
proof |
|
98 |
fix x :: 'a show "\<not> open {x}" |
|
99 |
proof |
|
100 |
assume "open {x}" |
|
101 |
then obtain e where "0 < e" and e: "\<forall>y. dist y x < e \<longrightarrow> y = x" |
|
102 |
unfolding open_dist by fast |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
103 |
def y \<equiv> "x + scaleR (e/2) (SOME b. b \<in> Basis)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
104 |
have [simp]: "(SOME b. b \<in> Basis) \<in> Basis" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
105 |
by (rule someI_ex) (auto simp: ex_in_conv) |
44571 | 106 |
from `0 < e` have "y \<noteq> x" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
107 |
unfolding y_def by (auto intro!: nonzero_Basis) |
44571 | 108 |
from `0 < e` have "dist y x < e" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
109 |
unfolding y_def by (simp add: dist_norm norm_Basis) |
44571 | 110 |
from `y \<noteq> x` and `dist y x < e` show "False" |
111 |
using e by simp |
|
112 |
qed |
|
113 |
qed |
|
114 |
||
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
115 |
subsection {* Class instances *} |
33175 | 116 |
|
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
117 |
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
|
118 |
|
44129 | 119 |
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
|
120 |
begin |
44129 | 121 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
122 |
definition |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
123 |
[simp]: "Basis = {1::real}" |
44129 | 124 |
|
125 |
instance |
|
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
126 |
by default (auto simp add: Basis_real_def) |
44129 | 127 |
|
128 |
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
|
129 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
130 |
lemma DIM_real[simp]: "DIM(real) = 1" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
131 |
by simp |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
132 |
|
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
133 |
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
|
134 |
|
44129 | 135 |
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
|
136 |
begin |
44129 | 137 |
|
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
138 |
definition Basis_complex_def: |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
139 |
"Basis = {1, ii}" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
140 |
|
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
141 |
instance |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
142 |
by default (auto simp add: Basis_complex_def intro: complex_eqI split: split_if_asm) |
44129 | 143 |
|
144 |
end |
|
145 |
||
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
36778
diff
changeset
|
146 |
lemma DIM_complex[simp]: "DIM(complex) = 2" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
147 |
unfolding Basis_complex_def 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
|
148 |
|
44133
691c52e900ca
split Linear_Algebra.thy from Euclidean_Space.thy
huffman
parents:
44129
diff
changeset
|
149 |
subsubsection {* Type @{typ "'a \<times> 'b"} *} |
38656 | 150 |
|
44129 | 151 |
instantiation prod :: (euclidean_space, euclidean_space) euclidean_space |
38656 | 152 |
begin |
153 |
||
44129 | 154 |
definition |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
155 |
"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
|
156 |
|
44129 | 157 |
instance proof |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
158 |
show "(Basis :: ('a \<times> 'b) set) \<noteq> {}" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
159 |
unfolding Basis_prod_def by simp |
44129 | 160 |
next |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
161 |
show "finite (Basis :: ('a \<times> 'b) set)" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
162 |
unfolding Basis_prod_def by simp |
44129 | 163 |
next |
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
164 |
fix u v :: "'a \<times> 'b" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
165 |
assume "u \<in> Basis" and "v \<in> Basis" |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
166 |
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
|
167 |
unfolding Basis_prod_def inner_prod_def |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
168 |
by (auto simp add: inner_Basis split: split_if_asm) |
44129 | 169 |
next |
170 |
fix x :: "'a \<times> 'b" |
|
44166
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
171 |
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
|
172 |
unfolding Basis_prod_def ball_Un ball_simps |
d12d89a66742
modify euclidean_space class to include basis set
huffman
parents:
44133
diff
changeset
|
173 |
by (simp add: inner_prod_def prod_eq_iff euclidean_all_zero_iff) |
38656 | 174 |
qed |
44129 | 175 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
176 |
lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('a) + DIM('b)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
177 |
unfolding Basis_prod_def |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
178 |
by (subst card_Un_disjoint) (auto intro!: card_image arg_cong2[where f="op +"] inj_onI) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
44902
diff
changeset
|
179 |
|
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 |
end |
38656 | 181 |
|
182 |
end |