# HG changeset patch
# User huffman
# Date 1314311754 25200
# Node ID bf8014b4f9333c7d76b02f38ce06c550608affa0
# Parent  abcf7c0743e8a6704c1c2eeb83768200bdef68dd
remove dot_lsum and dot_rsum in favor of inner_setsum_{left,right}

diff -r abcf7c0743e8 -r bf8014b4f933 NEWS
--- a/NEWS	Thu Aug 25 14:26:38 2011 -0700
+++ b/NEWS	Thu Aug 25 15:35:54 2011 -0700
@@ -218,6 +218,8 @@
   Lim_linear ~> bounded_linear.tendsto
   Lim_component ~> tendsto_euclidean_component
   Lim_component_cart ~> tendsto_vec_nth
+  dot_lsum ~> inner_setsum_left
+  dot_rsum ~> inner_setsum_right
   subset_interior ~> interior_mono
   subset_closure ~> closure_mono
   closure_univ ~> closure_UNIV
diff -r abcf7c0743e8 -r bf8014b4f933 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 25 14:26:38 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 25 15:35:54 2011 -0700
@@ -191,12 +191,6 @@
   apply (rule setsum_mono_zero_right[OF fT fST])
   by (auto intro: setsum_0')
 
-lemma dot_lsum: "finite S \<Longrightarrow> setsum f S \<bullet> y = setsum (\<lambda>x. f x \<bullet> y) S "
-  apply(induct rule: finite_induct) by(auto simp add: inner_add)
-
-lemma dot_rsum: "finite S \<Longrightarrow> y \<bullet> setsum f S = setsum (\<lambda>x. y \<bullet> f x) S "
-  apply(induct rule: finite_induct) by(auto simp add: inner_add)
-
 lemma vector_eq_ldot: "(\<forall>x. x \<bullet> y = x \<bullet> z) \<longleftrightarrow> y = z"
 proof
   assume "\<forall>x. x \<bullet> y = x \<bullet> z"
@@ -1816,7 +1810,7 @@
         apply (subst Cy)
         using C(1) fth
         apply (simp only: setsum_clauses)
-        apply (auto simp add: inner_add inner_commute[of y a] dot_lsum[OF fth])
+        apply (auto simp add: inner_add inner_commute[of y a] inner_setsum_left)
         apply (rule setsum_0')
         apply clarsimp
         apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
@@ -1833,7 +1827,7 @@
         using C(1) fth
         apply (simp only: setsum_clauses)
         apply (subst inner_commute[of x])
-        apply (auto simp add: inner_add inner_commute[of x a] dot_rsum[OF fth])
+        apply (auto simp add: inner_add inner_commute[of x a] inner_setsum_right)
         apply (rule setsum_0')
         apply clarsimp
         apply (rule C(4)[unfolded pairwise_def orthogonal_def, rule_format])
@@ -1903,7 +1897,7 @@
         apply (subst B') using fB fth
         unfolding setsum_clauses(2)[OF fth]
         apply simp unfolding inner_simps
-        apply (clarsimp simp add: inner_add dot_lsum)
+        apply (clarsimp simp add: inner_add inner_setsum_left)
         apply (rule setsum_0', rule ballI)
         unfolding inner_commute
         by (auto simp add: x field_simps intro: B(5)[unfolded pairwise_def orthogonal_def, rule_format])}