avoid duplicate rewrite warnings
authorhuffman
Tue Aug 09 10:42:07 2011 -0700 (2011-08-09)
changeset 44126ce44e70d0c47
parent 44125 230a8665c919
child 44127 7b57b9295d98
avoid duplicate rewrite warnings
src/HOL/Library/Inner_Product.thy
src/HOL/Library/Product_Vector.thy
     1.1 --- a/src/HOL/Library/Inner_Product.thy	Tue Aug 09 10:30:00 2011 -0700
     1.2 +++ b/src/HOL/Library/Inner_Product.thy	Tue Aug 09 10:42:07 2011 -0700
     1.3 @@ -123,8 +123,7 @@
     1.4          unfolding power2_sum power2_norm_eq_inner
     1.5          by (simp add: inner_add inner_commute)
     1.6        show "0 \<le> norm x + norm y"
     1.7 -        unfolding norm_eq_sqrt_inner
     1.8 -        by (simp add: add_nonneg_nonneg)
     1.9 +        unfolding norm_eq_sqrt_inner by simp
    1.10      qed
    1.11    have "sqrt (a\<twosuperior> * inner x x) = \<bar>a\<bar> * sqrt (inner x x)"
    1.12      by (simp add: real_sqrt_mult_distrib)
    1.13 @@ -217,7 +216,7 @@
    1.14    show "inner (scaleR r x) y = r * inner x y"
    1.15      unfolding inner_complex_def by (simp add: right_distrib)
    1.16    show "0 \<le> inner x x"
    1.17 -    unfolding inner_complex_def by (simp add: add_nonneg_nonneg)
    1.18 +    unfolding inner_complex_def by simp
    1.19    show "inner x x = 0 \<longleftrightarrow> x = 0"
    1.20      unfolding inner_complex_def
    1.21      by (simp add: add_nonneg_eq_0_iff complex_Re_Im_cancel_iff)
     2.1 --- a/src/HOL/Library/Product_Vector.thy	Tue Aug 09 10:30:00 2011 -0700
     2.2 +++ b/src/HOL/Library/Product_Vector.thy	Tue Aug 09 10:42:07 2011 -0700
     2.3 @@ -453,9 +453,9 @@
     2.4    assumes x: "0 \<le> x" and y: "0 \<le> y"
     2.5    shows "sqrt (x + y) \<le> sqrt x + sqrt y"
     2.6  apply (rule power2_le_imp_le)
     2.7 -apply (simp add: real_sum_squared_expand add_nonneg_nonneg x y)
     2.8 +apply (simp add: real_sum_squared_expand x y)
     2.9  apply (simp add: mult_nonneg_nonneg x y)
    2.10 -apply (simp add: add_nonneg_nonneg x y)
    2.11 +apply (simp add: x y)
    2.12  done
    2.13  
    2.14  lemma bounded_linear_Pair: