src/HOL/Library/Euclidean_Space.thy
 changeset 30045 b8ddd7667eed parent 30041 9becd197a40e child 30066 9223483cc927
1.1 --- a/src/HOL/Library/Euclidean_Space.thy	Sat Feb 21 21:00:50 2009 +0100
1.2 +++ b/src/HOL/Library/Euclidean_Space.thy	Sat Feb 21 15:39:59 2009 -0800
1.3 @@ -8,6 +8,7 @@
1.4  theory Euclidean_Space
1.5    imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Complex_Main
1.6    Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
1.7 +  Inner_Product
1.8    uses ("normarith.ML")
1.9  begin
1.11 @@ -547,6 +548,38 @@
1.13  end
1.15 +subsection {* Inner products *}
1.16 +
1.17 +instantiation "^" :: (real_inner, type) real_inner
1.18 +begin
1.19 +
1.20 +definition vector_inner_def:
1.21 +  "inner x y = setsum (\<lambda>i. inner (x\$i) (y\$i)) {1 .. dimindex(UNIV::'b set)}"
1.22 +
1.23 +instance proof
1.24 +  fix r :: real and x y z :: "'a ^ 'b"
1.25 +  show "inner x y = inner y x"
1.26 +    unfolding vector_inner_def
1.27 +    by (simp add: inner_commute)
1.28 +  show "inner (x + y) z = inner x z + inner y z"
1.29 +    unfolding vector_inner_def
1.30 +    by (vector inner_left_distrib)
1.31 +  show "inner (scaleR r x) y = r * inner x y"
1.32 +    unfolding vector_inner_def
1.33 +    by (vector inner_scaleR_left)
1.34 +  show "0 \<le> inner x x"
1.35 +    unfolding vector_inner_def
1.36 +    by (simp add: setsum_nonneg)
1.37 +  show "inner x x = 0 \<longleftrightarrow> x = 0"
1.38 +    unfolding vector_inner_def
1.39 +    by (simp add: Cart_eq setsum_nonneg_eq_0_iff)
1.40 +  show "norm x = sqrt (inner x x)"
1.41 +    unfolding vector_inner_def vector_norm_def setL2_def
1.42 +    by (simp add: power2_norm_eq_inner)
1.43 +qed
1.44 +
1.45 +end
1.46 +
1.47  subsection{* Properties of the dot product.  *}
1.49  lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n) \<bullet> y = y \<bullet> x"