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.10  
    1.11 @@ -547,6 +548,38 @@
    1.12  
    1.13  end
    1.14  
    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.48  
    1.49  lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n) \<bullet> y = y \<bullet> x"