# HG changeset patch
# User immler
# Date 1545940854 -3600
# Node ID 4cc5e4a528f8367a9dc7f6d52c90c63881bf17a1
# Parent  0f31dd2e540d1792e875a84252fd7ddc179389e7
moved dependency

diff -r 0f31dd2e540d -r 4cc5e4a528f8 src/HOL/Analysis/Euclidean_Space.thy
--- a/src/HOL/Analysis/Euclidean_Space.thy	Thu Dec 27 21:00:50 2018 +0100
+++ b/src/HOL/Analysis/Euclidean_Space.thy	Thu Dec 27 21:00:54 2018 +0100
@@ -7,7 +7,9 @@
 
 theory Euclidean_Space
 imports
-  L2_Norm Product_Vector
+  L2_Norm
+  Inner_Product
+  Product_Vector
 begin
 
 subsection \<open>Type class of Euclidean spaces\<close>
@@ -261,6 +263,44 @@
 
 subsubsection%unimportant \<open>Type @{typ "'a \<times> 'b"}\<close>
 
+instantiation prod :: (real_inner, real_inner) real_inner
+begin
+
+definition inner_prod_def:
+  "inner x y = inner (fst x) (fst y) + inner (snd x) (snd y)"
+
+lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d"
+  unfolding inner_prod_def by simp
+
+instance
+proof
+  fix r :: real
+  fix x y z :: "'a::real_inner \<times> 'b::real_inner"
+  show "inner x y = inner y x"
+    unfolding inner_prod_def
+    by (simp add: inner_commute)
+  show "inner (x + y) z = inner x z + inner y z"
+    unfolding inner_prod_def
+    by (simp add: inner_add_left)
+  show "inner (scaleR r x) y = r * inner x y"
+    unfolding inner_prod_def
+    by (simp add: distrib_left)
+  show "0 \<le> inner x x"
+    unfolding inner_prod_def
+    by (intro add_nonneg_nonneg inner_ge_zero)
+  show "inner x x = 0 \<longleftrightarrow> x = 0"
+    unfolding inner_prod_def prod_eq_iff
+    by (simp add: add_nonneg_eq_0_iff)
+  show "norm x = sqrt (inner x x)"
+    unfolding norm_prod_def inner_prod_def
+    by (simp add: power2_norm_eq_inner)
+qed
+
+end
+
+lemma inner_Pair_0: "inner x (0, b) = inner (snd x) b" "inner x (a, 0) = inner (fst x) a"
+    by (cases x, simp)+
+
 instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
 begin
 
diff -r 0f31dd2e540d -r 4cc5e4a528f8 src/HOL/Analysis/Product_Vector.thy
--- a/src/HOL/Analysis/Product_Vector.thy	Thu Dec 27 21:00:50 2018 +0100
+++ b/src/HOL/Analysis/Product_Vector.thy	Thu Dec 27 21:00:54 2018 +0100
@@ -5,9 +5,9 @@
 section \<open>Cartesian Products as Vector Spaces\<close>
 
 theory Product_Vector
-imports
-  Inner_Product
-  "HOL-Library.Product_Plus"
+  imports
+    Complex_Main
+    "HOL-Library.Product_Plus"
 begin
 
 lemma Times_eq_image_sum:
@@ -395,47 +395,6 @@
   using assms
   by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
 
-
-subsection \<open>Product is an inner product space\<close>
-
-instantiation prod :: (real_inner, real_inner) real_inner
-begin
-
-definition inner_prod_def:
-  "inner x y = inner (fst x) (fst y) + inner (snd x) (snd y)"
-
-lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d"
-  unfolding inner_prod_def by simp
-
-instance
-proof
-  fix r :: real
-  fix x y z :: "'a::real_inner \<times> 'b::real_inner"
-  show "inner x y = inner y x"
-    unfolding inner_prod_def
-    by (simp add: inner_commute)
-  show "inner (x + y) z = inner x z + inner y z"
-    unfolding inner_prod_def
-    by (simp add: inner_add_left)
-  show "inner (scaleR r x) y = r * inner x y"
-    unfolding inner_prod_def
-    by (simp add: distrib_left)
-  show "0 \<le> inner x x"
-    unfolding inner_prod_def
-    by (intro add_nonneg_nonneg inner_ge_zero)
-  show "inner x x = 0 \<longleftrightarrow> x = 0"
-    unfolding inner_prod_def prod_eq_iff
-    by (simp add: add_nonneg_eq_0_iff)
-  show "norm x = sqrt (inner x x)"
-    unfolding norm_prod_def inner_prod_def
-    by (simp add: power2_norm_eq_inner)
-qed
-
-end
-
-lemma inner_Pair_0: "inner x (0, b) = inner (snd x) b" "inner x (a, 0) = inner (fst x) a"
-    by (cases x, simp)+
-
 lemma
   fixes x :: "'a::real_normed_vector"
   shows norm_Pair1 [simp]: "norm (0,x) = norm x"