author immler Thu, 27 Dec 2018 21:00:54 +0100 changeset 69511 4cc5e4a528f8 parent 69510 0f31dd2e540d child 69512 2b54f25e66c4
moved dependency
```--- 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
+  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
+  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
```
```--- 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
-  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