removed unused lemma sin_cos_squared_add2_mult
authorhuffman
Wed Sep 07 10:04:07 2011 -0700 (2011-09-07)
changeset 448236ce95c8c0ba8
parent 44822 2690b6de5021
child 44824 34b83d981380
removed unused lemma sin_cos_squared_add2_mult
src/HOL/Complex.thy
     1.1 --- a/src/HOL/Complex.thy	Wed Sep 07 09:45:39 2011 -0700
     1.2 +++ b/src/HOL/Complex.thy	Wed Sep 07 10:04:07 2011 -0700
     1.3 @@ -621,13 +621,6 @@
     1.4  lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a"
     1.5    by (simp add: rcis_def cis_def)
     1.6  
     1.7 -lemma sin_cos_squared_add2_mult: "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior>"
     1.8 -proof -
     1.9 -  have "(r * cos a)\<twosuperior> + (r * sin a)\<twosuperior> = r\<twosuperior> * ((cos a)\<twosuperior> + (sin a)\<twosuperior>)"
    1.10 -    by (simp only: power_mult_distrib right_distrib)
    1.11 -  thus ?thesis by simp
    1.12 -qed
    1.13 -
    1.14  lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
    1.15    by (simp add: rcis_def cis_def norm_mult)
    1.16