# HG changeset patch # User huffman # Date 1315501673 25200 # Node ID e9d1fcbc7d20c4d01ee5cac40e47b4654d336e73 # Parent f74a4175a3a8bef0552bc03281711d0f76dbfe61 remove unnecessary intermediate lemmas diff -r f74a4175a3a8 -r e9d1fcbc7d20 src/HOL/Complex.thy --- a/src/HOL/Complex.thy Thu Sep 08 08:41:28 2011 -0700 +++ b/src/HOL/Complex.thy Thu Sep 08 10:07:53 2011 -0700 @@ -746,14 +746,6 @@ lemma rcis_cmod_arg: "rcis (cmod z) (arg z) = z" by (cases "z = 0", simp_all add: rcis_def cis_arg sgn_div_norm of_real_def) -lemma cos_arg_i_mult_zero_pos: (* TODO: delete *) - "0 < y ==> cos (arg(Complex 0 y)) = 0" - using cis_arg [of "Complex 0 y"] by (simp add: complex_eq_iff) - -lemma cos_arg_i_mult_zero_neg: (* TODO: delete *) - "y < 0 ==> cos (arg(Complex 0 y)) = 0" - using cis_arg [of "Complex 0 y"] by (simp add: complex_eq_iff) - lemma cos_arg_i_mult_zero [simp]: "y \ 0 ==> cos (arg(Complex 0 y)) = 0" using cis_arg [of "Complex 0 y"] by (simp add: complex_eq_iff) diff -r f74a4175a3a8 -r e9d1fcbc7d20 src/HOL/NSA/NSComplex.thy --- a/src/HOL/NSA/NSComplex.thy Thu Sep 08 08:41:28 2011 -0700 +++ b/src/HOL/NSA/NSComplex.thy Thu Sep 08 10:07:53 2011 -0700 @@ -457,14 +457,6 @@ (* harg *) (*---------------------------------------------------------------------------*) -lemma cos_harg_i_mult_zero_pos: - "!!y. 0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0" -by transfer (rule cos_arg_i_mult_zero_pos) - -lemma cos_harg_i_mult_zero_neg: - "!!y. y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0" -by transfer (rule cos_arg_i_mult_zero_neg) - lemma cos_harg_i_mult_zero [simp]: "!!y. y \ 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0" by transfer (rule cos_arg_i_mult_zero)