# HG changeset patch
# User huffman
# Date 1235259599 28800
# Node ID b8ddd7667eede528abffabd44fc7c18ea720171c
# Parent  f9182081d6c68a4c501f84947c944594ab790465
real_inner class instance for vectors

diff -r f9182081d6c6 -r b8ddd7667eed src/HOL/Library/Euclidean_Space.thy
--- a/src/HOL/Library/Euclidean_Space.thy	Sat Feb 21 21:00:50 2009 +0100
+++ b/src/HOL/Library/Euclidean_Space.thy	Sat Feb 21 15:39:59 2009 -0800
@@ -8,6 +8,7 @@
 theory Euclidean_Space
   imports "~~/src/HOL/Decision_Procs/Dense_Linear_Order" Complex_Main 
   Finite_Cartesian_Product Glbs Infinite_Set Numeral_Type
+  Inner_Product
   uses ("normarith.ML")
 begin
 
@@ -547,6 +548,38 @@
 
 end
 
+subsection {* Inner products *}
+
+instantiation "^" :: (real_inner, type) real_inner
+begin
+
+definition vector_inner_def:
+  "inner x y = setsum (\<lambda>i. inner (x$i) (y$i)) {1 .. dimindex(UNIV::'b set)}"
+
+instance proof
+  fix r :: real and x y z :: "'a ^ 'b"
+  show "inner x y = inner y x"
+    unfolding vector_inner_def
+    by (simp add: inner_commute)
+  show "inner (x + y) z = inner x z + inner y z"
+    unfolding vector_inner_def
+    by (vector inner_left_distrib)
+  show "inner (scaleR r x) y = r * inner x y"
+    unfolding vector_inner_def
+    by (vector inner_scaleR_left)
+  show "0 \<le> inner x x"
+    unfolding vector_inner_def
+    by (simp add: setsum_nonneg)
+  show "inner x x = 0 \<longleftrightarrow> x = 0"
+    unfolding vector_inner_def
+    by (simp add: Cart_eq setsum_nonneg_eq_0_iff)
+  show "norm x = sqrt (inner x x)"
+    unfolding vector_inner_def vector_norm_def setL2_def
+    by (simp add: power2_norm_eq_inner)
+qed
+
+end
+
 subsection{* Properties of the dot product.  *}
 
 lemma dot_sym: "(x::'a:: {comm_monoid_add, ab_semigroup_mult} ^ 'n) \<bullet> y = y \<bullet> x"