# HG changeset patch
# User huffman
# Date 1315320539 25200
# Node ID 5b1e1432c3201ea332a5c4033738c1f83a73a7e2
# Parent  7f6838b3474a45638fedab1dd6c1bbc3a6ccdcd0
remove redundant lemma real_sum_squared_expand in favor of power2_sum

diff -r 7f6838b3474a -r 5b1e1432c320 NEWS
--- a/NEWS	Tue Sep 06 07:45:18 2011 -0700
+++ b/NEWS	Tue Sep 06 07:48:59 2011 -0700
@@ -276,6 +276,7 @@
   real_squared_diff_one_factored ~> square_diff_one_factored
   realpow_two_diff ~> square_diff_square_factored
   reals_complete2 ~> complete_real
+  real_sum_squared_expand ~> power2_sum
   exp_ln_eq ~> ln_unique
   expi_add ~> exp_add
   expi_zero ~> exp_zero
diff -r 7f6838b3474a -r 5b1e1432c320 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Sep 06 07:45:18 2011 -0700
+++ b/src/HOL/Complex.thy	Tue Sep 06 07:48:59 2011 -0700
@@ -321,8 +321,6 @@
 lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a) - cmod b \<le> cmod a"
   by (rule ord_le_eq_trans [OF norm_triangle_ineq2], simp)
 
-lemmas real_sum_squared_expand = power2_sum [where 'a=real]
-
 lemma abs_Re_le_cmod: "\<bar>Re x\<bar> \<le> cmod x"
   by (cases x) simp
 
diff -r 7f6838b3474a -r 5b1e1432c320 src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Tue Sep 06 07:45:18 2011 -0700
+++ b/src/HOL/Library/Product_Vector.thy	Tue Sep 06 07:48:59 2011 -0700
@@ -450,7 +450,7 @@
   assumes x: "0 \<le> x" and y: "0 \<le> y"
   shows "sqrt (x + y) \<le> sqrt x + sqrt y"
 apply (rule power2_le_imp_le)
-apply (simp add: real_sum_squared_expand x y)
+apply (simp add: power2_sum x y)
 apply (simp add: mult_nonneg_nonneg x y)
 apply (simp add: x y)
 done
diff -r 7f6838b3474a -r 5b1e1432c320 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Sep 06 07:45:18 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Sep 06 07:48:59 2011 -0700
@@ -420,7 +420,7 @@
   assumes x: "0 \<le> x" and y: "0 \<le> y"
   shows "sqrt (x + y) \<le> sqrt x + sqrt y"
 apply (rule power2_le_imp_le)
-apply (simp add: real_sum_squared_expand x y)
+apply (simp add: power2_sum x y)
 apply (simp add: mult_nonneg_nonneg x y)
 apply (simp add: x y)
 done