move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
authorhuffman
Mon Sep 12 09:21:01 2011 -0700 (2011-09-12)
changeset 449029ba11d41cd1f
parent 44901 ed5ddf9fcc77
child 44903 1d5079a5a0a2
move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy
src/HOL/Complex.thy
src/HOL/Library/Inner_Product.thy
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
     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.5    by (simp add: i_def)
     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.11    by (simp add: complex_eq_iff)
    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