author huffman Mon Sep 12 09:21:01 2011 -0700 (2011-09-12) changeset 44902 9ba11d41cd1f parent 44901 ed5ddf9fcc77 child 44903 1d5079a5a0a2
move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
 src/HOL/Complex.thy file | annotate | diff | revisions src/HOL/Library/Inner_Product.thy file | annotate | diff | revisions src/HOL/Multivariate_Analysis/Euclidean_Space.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Complex.thy	Mon Sep 12 09:57:33 2011 -0400
1.2 +++ b/src/HOL/Complex.thy	Mon Sep 12 09:21:01 2011 -0700
1.3 @@ -412,6 +412,9 @@
1.4  lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 \<and> y = 1)"
1.6
1.7 +lemma norm_ii [simp]: "norm ii = 1"
1.8 +  by (simp add: i_def)
1.9 +
1.10  lemma complex_i_not_zero [simp]: "ii \<noteq> 0"
1.12
```
```     2.1 --- a/src/HOL/Library/Inner_Product.thy	Mon Sep 12 09:57:33 2011 -0400
2.2 +++ b/src/HOL/Library/Inner_Product.thy	Mon Sep 12 09:21:01 2011 -0700
2.3 @@ -240,6 +240,18 @@
2.4
2.5  end
2.6
2.7 +lemma complex_inner_1 [simp]: "inner 1 x = Re x"
2.8 +  unfolding inner_complex_def by simp
2.9 +
2.10 +lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
2.11 +  unfolding inner_complex_def by simp
2.12 +
2.13 +lemma complex_inner_ii_left [simp]: "inner ii x = Im x"
2.14 +  unfolding inner_complex_def by simp
2.15 +
2.16 +lemma complex_inner_ii_right [simp]: "inner x ii = Im x"
2.17 +  unfolding inner_complex_def by simp
2.18 +
2.19
2.20  subsection {* Gradient derivative *}
2.21
```
```     3.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Sep 12 09:57:33 2011 -0400
3.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Sep 12 09:21:01 2011 -0700
3.3 @@ -275,23 +275,6 @@
3.4
3.5  subsubsection {* Type @{typ complex} *}
3.6
3.7 - (* TODO: move these to Complex.thy/Inner_Product.thy *)
3.8 -
3.9 -lemma norm_ii [simp]: "norm ii = 1"
3.10 -  unfolding i_def by simp
3.11 -
3.12 -lemma complex_inner_1 [simp]: "inner 1 x = Re x"
3.13 -  unfolding inner_complex_def by simp
3.14 -
3.15 -lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
3.16 -  unfolding inner_complex_def by simp
3.17 -
3.18 -lemma complex_inner_ii_left [simp]: "inner ii x = Im x"
3.19 -  unfolding inner_complex_def by simp
3.20 -
3.21 -lemma complex_inner_ii_right [simp]: "inner x ii = Im x"
3.22 -  unfolding inner_complex_def by simp
3.23 -
3.24  instantiation complex :: euclidean_space
3.25  begin
3.26
```