author immler Thu Dec 27 21:00:54 2018 +0100 (5 months ago) changeset 69511 4cc5e4a528f8 parent 69510 0f31dd2e540d child 69512 2b54f25e66c4
moved dependency
```     1.1 --- a/src/HOL/Analysis/Euclidean_Space.thy	Thu Dec 27 21:00:50 2018 +0100
1.2 +++ b/src/HOL/Analysis/Euclidean_Space.thy	Thu Dec 27 21:00:54 2018 +0100
1.3 @@ -7,7 +7,9 @@
1.4
1.5  theory Euclidean_Space
1.6  imports
1.7 -  L2_Norm Product_Vector
1.8 +  L2_Norm
1.9 +  Inner_Product
1.10 +  Product_Vector
1.11  begin
1.12
1.13  subsection \<open>Type class of Euclidean spaces\<close>
1.14 @@ -261,6 +263,44 @@
1.15
1.16  subsubsection%unimportant \<open>Type @{typ "'a \<times> 'b"}\<close>
1.17
1.18 +instantiation prod :: (real_inner, real_inner) real_inner
1.19 +begin
1.20 +
1.21 +definition inner_prod_def:
1.22 +  "inner x y = inner (fst x) (fst y) + inner (snd x) (snd y)"
1.23 +
1.24 +lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d"
1.25 +  unfolding inner_prod_def by simp
1.26 +
1.27 +instance
1.28 +proof
1.29 +  fix r :: real
1.30 +  fix x y z :: "'a::real_inner \<times> 'b::real_inner"
1.31 +  show "inner x y = inner y x"
1.32 +    unfolding inner_prod_def
1.33 +    by (simp add: inner_commute)
1.34 +  show "inner (x + y) z = inner x z + inner y z"
1.35 +    unfolding inner_prod_def
1.37 +  show "inner (scaleR r x) y = r * inner x y"
1.38 +    unfolding inner_prod_def
1.39 +    by (simp add: distrib_left)
1.40 +  show "0 \<le> inner x x"
1.41 +    unfolding inner_prod_def
1.42 +    by (intro add_nonneg_nonneg inner_ge_zero)
1.43 +  show "inner x x = 0 \<longleftrightarrow> x = 0"
1.44 +    unfolding inner_prod_def prod_eq_iff
1.46 +  show "norm x = sqrt (inner x x)"
1.47 +    unfolding norm_prod_def inner_prod_def
1.48 +    by (simp add: power2_norm_eq_inner)
1.49 +qed
1.50 +
1.51 +end
1.52 +
1.53 +lemma inner_Pair_0: "inner x (0, b) = inner (snd x) b" "inner x (a, 0) = inner (fst x) a"
1.54 +    by (cases x, simp)+
1.55 +
1.56  instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
1.57  begin
1.58
```
```     2.1 --- a/src/HOL/Analysis/Product_Vector.thy	Thu Dec 27 21:00:50 2018 +0100
2.2 +++ b/src/HOL/Analysis/Product_Vector.thy	Thu Dec 27 21:00:54 2018 +0100
2.3 @@ -5,9 +5,9 @@
2.4  section \<open>Cartesian Products as Vector Spaces\<close>
2.5
2.6  theory Product_Vector
2.7 -imports
2.8 -  Inner_Product
2.9 -  "HOL-Library.Product_Plus"
2.10 +  imports
2.11 +    Complex_Main
2.12 +    "HOL-Library.Product_Plus"
2.13  begin
2.14
2.15  lemma Times_eq_image_sum:
2.16 @@ -395,47 +395,6 @@
2.17    using assms
2.18    by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
2.19
2.20 -
2.21 -subsection \<open>Product is an inner product space\<close>
2.22 -
2.23 -instantiation prod :: (real_inner, real_inner) real_inner
2.24 -begin
2.25 -
2.26 -definition inner_prod_def:
2.27 -  "inner x y = inner (fst x) (fst y) + inner (snd x) (snd y)"
2.28 -
2.29 -lemma inner_Pair [simp]: "inner (a, b) (c, d) = inner a c + inner b d"
2.30 -  unfolding inner_prod_def by simp
2.31 -
2.32 -instance
2.33 -proof
2.34 -  fix r :: real
2.35 -  fix x y z :: "'a::real_inner \<times> 'b::real_inner"
2.36 -  show "inner x y = inner y x"
2.37 -    unfolding inner_prod_def
2.38 -    by (simp add: inner_commute)
2.39 -  show "inner (x + y) z = inner x z + inner y z"
2.40 -    unfolding inner_prod_def
2.42 -  show "inner (scaleR r x) y = r * inner x y"
2.43 -    unfolding inner_prod_def
2.44 -    by (simp add: distrib_left)
2.45 -  show "0 \<le> inner x x"
2.46 -    unfolding inner_prod_def
2.47 -    by (intro add_nonneg_nonneg inner_ge_zero)
2.48 -  show "inner x x = 0 \<longleftrightarrow> x = 0"
2.49 -    unfolding inner_prod_def prod_eq_iff
2.51 -  show "norm x = sqrt (inner x x)"
2.52 -    unfolding norm_prod_def inner_prod_def
2.53 -    by (simp add: power2_norm_eq_inner)
2.54 -qed
2.55 -
2.56 -end
2.57 -
2.58 -lemma inner_Pair_0: "inner x (0, b) = inner (snd x) b" "inner x (a, 0) = inner (fst x) a"
2.59 -    by (cases x, simp)+
2.60 -
2.61  lemma
2.62    fixes x :: "'a::real_normed_vector"
2.63    shows norm_Pair1 [simp]: "norm (0,x) = norm x"
```