--- 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
--- 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"