remove redundant lemma real_sum_squared_expand in favor of power2_sum
authorhuffman
Tue Sep 06 07:48:59 2011 -0700 (2011-09-06)
changeset 447495b1e1432c320
parent 44748 7f6838b3474a
child 44750 5b11f36fcacb
remove redundant lemma real_sum_squared_expand in favor of power2_sum
NEWS
src/HOL/Complex.thy
src/HOL/Library/Product_Vector.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
     1.1 --- a/NEWS	Tue Sep 06 07:45:18 2011 -0700
     1.2 +++ b/NEWS	Tue Sep 06 07:48:59 2011 -0700
     1.3 @@ -276,6 +276,7 @@
     1.4    real_squared_diff_one_factored ~> square_diff_one_factored
     1.5    realpow_two_diff ~> square_diff_square_factored
     1.6    reals_complete2 ~> complete_real
     1.7 +  real_sum_squared_expand ~> power2_sum
     1.8    exp_ln_eq ~> ln_unique
     1.9    expi_add ~> exp_add
    1.10    expi_zero ~> exp_zero
     2.1 --- a/src/HOL/Complex.thy	Tue Sep 06 07:45:18 2011 -0700
     2.2 +++ b/src/HOL/Complex.thy	Tue Sep 06 07:48:59 2011 -0700
     2.3 @@ -321,8 +321,6 @@
     2.4  lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a) - cmod b \<le> cmod a"
     2.5    by (rule ord_le_eq_trans [OF norm_triangle_ineq2], simp)
     2.6  
     2.7 -lemmas real_sum_squared_expand = power2_sum [where 'a=real]
     2.8 -
     2.9  lemma abs_Re_le_cmod: "\<bar>Re x\<bar> \<le> cmod x"
    2.10    by (cases x) simp
    2.11  
     3.1 --- a/src/HOL/Library/Product_Vector.thy	Tue Sep 06 07:45:18 2011 -0700
     3.2 +++ b/src/HOL/Library/Product_Vector.thy	Tue Sep 06 07:48:59 2011 -0700
     3.3 @@ -450,7 +450,7 @@
     3.4    assumes x: "0 \<le> x" and y: "0 \<le> y"
     3.5    shows "sqrt (x + y) \<le> sqrt x + sqrt y"
     3.6  apply (rule power2_le_imp_le)
     3.7 -apply (simp add: real_sum_squared_expand x y)
     3.8 +apply (simp add: power2_sum x y)
     3.9  apply (simp add: mult_nonneg_nonneg x y)
    3.10  apply (simp add: x y)
    3.11  done
     4.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Sep 06 07:45:18 2011 -0700
     4.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Tue Sep 06 07:48:59 2011 -0700
     4.3 @@ -420,7 +420,7 @@
     4.4    assumes x: "0 \<le> x" and y: "0 \<le> y"
     4.5    shows "sqrt (x + y) \<le> sqrt x + sqrt y"
     4.6  apply (rule power2_le_imp_le)
     4.7 -apply (simp add: real_sum_squared_expand x y)
     4.8 +apply (simp add: power2_sum x y)
     4.9  apply (simp add: mult_nonneg_nonneg x y)
    4.10  apply (simp add: x y)
    4.11  done