remove some unnecessary simp rules from simpset
authorhuffman
Tue Sep 06 13:16:46 2011 -0700 (2011-09-06)
changeset 447610694fc3248fd
parent 44760 19e1c6e922b6
child 44762 8f9d09241a68
child 44764 264436dd9491
remove some unnecessary simp rules from simpset
src/HOL/Complex.thy
     1.1 --- a/src/HOL/Complex.thy	Tue Sep 06 21:56:11 2011 +0200
     1.2 +++ b/src/HOL/Complex.thy	Tue Sep 06 13:16:46 2011 -0700
     1.3 @@ -304,10 +304,10 @@
     1.4  
     1.5  end
     1.6  
     1.7 -lemma cmod_unit_one [simp]: "cmod (Complex (cos a) (sin a)) = 1"
     1.8 +lemma cmod_unit_one: "cmod (Complex (cos a) (sin a)) = 1"
     1.9    by simp
    1.10  
    1.11 -lemma cmod_complex_polar [simp]:
    1.12 +lemma cmod_complex_polar:
    1.13    "cmod (complex_of_real r * Complex (cos a) (sin a)) = abs r"
    1.14    by (simp add: norm_mult)
    1.15  
    1.16 @@ -315,10 +315,10 @@
    1.17    unfolding complex_norm_def
    1.18    by (rule real_sqrt_sum_squares_ge1)
    1.19  
    1.20 -lemma complex_mod_minus_le_complex_mod [simp]: "- cmod x \<le> cmod x"
    1.21 +lemma complex_mod_minus_le_complex_mod: "- cmod x \<le> cmod x"
    1.22    by (rule order_trans [OF _ norm_ge_zero], simp)
    1.23  
    1.24 -lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a) - cmod b \<le> cmod a"
    1.25 +lemma complex_mod_triangle_ineq2: "cmod(b + a) - cmod b \<le> cmod a"
    1.26    by (rule ord_le_eq_trans [OF norm_triangle_ineq2], simp)
    1.27  
    1.28  lemma abs_Re_le_cmod: "\<bar>Re x\<bar> \<le> cmod x"
    1.29 @@ -635,7 +635,7 @@
    1.30  qed
    1.31  
    1.32  lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
    1.33 -  by (simp add: rcis_def cis_def sin_cos_squared_add2_mult)
    1.34 +  by (simp add: rcis_def cis_def norm_mult)
    1.35  
    1.36  lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
    1.37    by (simp add: cmod_def power2_eq_square)