# HG changeset patch
# User huffman
# Date 1315844461 25200
# Node ID 9ba11d41cd1f28c53adc16bf92679cb75c5aea44
# Parent  ed5ddf9fcc7710f435ce18e969e705eedb93ac6b
move lemmas about complex number 'i' to Complex.thy and Library/Inner_Product.thy

diff -r ed5ddf9fcc77 -r 9ba11d41cd1f src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Mon Sep 12 09:57:33 2011 -0400
+++ b/src/HOL/Complex.thy	Mon Sep 12 09:21:01 2011 -0700
@@ -412,6 +412,9 @@
 lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 \<and> y = 1)"
   by (simp add: i_def)
 
+lemma norm_ii [simp]: "norm ii = 1"
+  by (simp add: i_def)
+
 lemma complex_i_not_zero [simp]: "ii \<noteq> 0"
   by (simp add: complex_eq_iff)
 
diff -r ed5ddf9fcc77 -r 9ba11d41cd1f src/HOL/Library/Inner_Product.thy
--- a/src/HOL/Library/Inner_Product.thy	Mon Sep 12 09:57:33 2011 -0400
+++ b/src/HOL/Library/Inner_Product.thy	Mon Sep 12 09:21:01 2011 -0700
@@ -240,6 +240,18 @@
 
 end
 
+lemma complex_inner_1 [simp]: "inner 1 x = Re x"
+  unfolding inner_complex_def by simp
+
+lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
+  unfolding inner_complex_def by simp
+
+lemma complex_inner_ii_left [simp]: "inner ii x = Im x"
+  unfolding inner_complex_def by simp
+
+lemma complex_inner_ii_right [simp]: "inner x ii = Im x"
+  unfolding inner_complex_def by simp
+
 
 subsection {* Gradient derivative *}
 
diff -r ed5ddf9fcc77 -r 9ba11d41cd1f src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Sep 12 09:57:33 2011 -0400
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Mon Sep 12 09:21:01 2011 -0700
@@ -275,23 +275,6 @@
 
 subsubsection {* Type @{typ complex} *}
 
- (* TODO: move these to Complex.thy/Inner_Product.thy *)
-
-lemma norm_ii [simp]: "norm ii = 1"
-  unfolding i_def by simp
-
-lemma complex_inner_1 [simp]: "inner 1 x = Re x"
-  unfolding inner_complex_def by simp
-
-lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
-  unfolding inner_complex_def by simp
-
-lemma complex_inner_ii_left [simp]: "inner ii x = Im x"
-  unfolding inner_complex_def by simp
-
-lemma complex_inner_ii_right [simp]: "inner x ii = Im x"
-  unfolding inner_complex_def by simp
-
 instantiation complex :: euclidean_space
 begin