remove unnecessary intermediate lemmas
authorhuffman
Thu Sep 08 10:07:53 2011 -0700 (2011-09-08)
changeset 44846e9d1fcbc7d20
parent 44844 f74a4175a3a8
child 44847 b93d17a52217
remove unnecessary intermediate lemmas
src/HOL/Complex.thy
src/HOL/NSA/NSComplex.thy
     1.1 --- a/src/HOL/Complex.thy	Thu Sep 08 08:41:28 2011 -0700
     1.2 +++ b/src/HOL/Complex.thy	Thu Sep 08 10:07:53 2011 -0700
     1.3 @@ -746,14 +746,6 @@
     1.4  lemma rcis_cmod_arg: "rcis (cmod z) (arg z) = z"
     1.5    by (cases "z = 0", simp_all add: rcis_def cis_arg sgn_div_norm of_real_def)
     1.6  
     1.7 -lemma cos_arg_i_mult_zero_pos: (* TODO: delete *)
     1.8 -   "0 < y ==> cos (arg(Complex 0 y)) = 0"
     1.9 -  using cis_arg [of "Complex 0 y"] by (simp add: complex_eq_iff)
    1.10 -
    1.11 -lemma cos_arg_i_mult_zero_neg: (* TODO: delete *)
    1.12 -   "y < 0 ==> cos (arg(Complex 0 y)) = 0"
    1.13 -  using cis_arg [of "Complex 0 y"] by (simp add: complex_eq_iff)
    1.14 -
    1.15  lemma cos_arg_i_mult_zero [simp]:
    1.16       "y \<noteq> 0 ==> cos (arg(Complex 0 y)) = 0"
    1.17    using cis_arg [of "Complex 0 y"] by (simp add: complex_eq_iff)
     2.1 --- a/src/HOL/NSA/NSComplex.thy	Thu Sep 08 08:41:28 2011 -0700
     2.2 +++ b/src/HOL/NSA/NSComplex.thy	Thu Sep 08 10:07:53 2011 -0700
     2.3 @@ -457,14 +457,6 @@
     2.4  (*  harg                                                                     *)
     2.5  (*---------------------------------------------------------------------------*)
     2.6  
     2.7 -lemma cos_harg_i_mult_zero_pos:
     2.8 -     "!!y. 0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
     2.9 -by transfer (rule cos_arg_i_mult_zero_pos)
    2.10 -
    2.11 -lemma cos_harg_i_mult_zero_neg:
    2.12 -     "!!y. y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
    2.13 -by transfer (rule cos_arg_i_mult_zero_neg)
    2.14 -
    2.15  lemma cos_harg_i_mult_zero [simp]:
    2.16       "!!y. y \<noteq> 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0"
    2.17  by transfer (rule cos_arg_i_mult_zero)