moved dependency
authorimmler
Thu Dec 27 21:00:54 2018 +0100 (5 months ago)
changeset 695114cc5e4a528f8
parent 69510 0f31dd2e540d
child 69512 2b54f25e66c4
moved dependency
src/HOL/Analysis/Euclidean_Space.thy
src/HOL/Analysis/Product_Vector.thy
     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.36 +    by (simp add: inner_add_left)
    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.45 +    by (simp add: add_nonneg_eq_0_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.41 -    by (simp add: inner_add_left)
    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.50 -    by (simp add: add_nonneg_eq_0_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"