src/HOL/Nonstandard_Analysis/NSComplex.thy
changeset 65274 db2de50de28e
parent 64435 c93b0e6131c3
child 68499 d4312962161a
     1.1 --- a/src/HOL/Nonstandard_Analysis/NSComplex.thy	Thu Mar 16 13:55:29 2017 +0000
     1.2 +++ b/src/HOL/Nonstandard_Analysis/NSComplex.thy	Thu Mar 16 16:02:18 2017 +0000
     1.3 @@ -438,20 +438,17 @@
     1.4  subsubsection \<open>\<open>harg\<close>\<close>
     1.5  
     1.6  lemma cos_harg_i_mult_zero [simp]: "\<And>y. y \<noteq> 0 \<Longrightarrow> ( *f* cos) (harg (HComplex 0 y)) = 0"
     1.7 -  by transfer simp
     1.8 -
     1.9 -lemma hcomplex_of_hypreal_zero_iff [simp]: "\<And>y. hcomplex_of_hypreal y = 0 \<longleftrightarrow> y = 0"
    1.10 -  by transfer (rule of_real_eq_0_iff)
    1.11 +  by transfer (simp add: Complex_eq)
    1.12  
    1.13  
    1.14  subsection \<open>Polar Form for Nonstandard Complex Numbers\<close>
    1.15  
    1.16  lemma complex_split_polar2: "\<forall>n. \<exists>r a. (z n) = complex_of_real r * Complex (cos a) (sin a)"
    1.17 -  by (auto intro: complex_split_polar)
    1.18 +  unfolding Complex_eq by (auto intro: complex_split_polar)
    1.19  
    1.20  lemma hcomplex_split_polar:
    1.21    "\<And>z. \<exists>r a. z = hcomplex_of_hypreal r * (HComplex (( *f* cos) a) (( *f* sin) a))"
    1.22 -  by transfer (simp add: complex_split_polar)
    1.23 +  by transfer (simp add: Complex_eq complex_split_polar)
    1.24  
    1.25  lemma hcis_eq:
    1.26    "\<And>a. hcis a = hcomplex_of_hypreal (( *f* cos) a) + iii * hcomplex_of_hypreal (( *f* sin) a)"
    1.27 @@ -479,7 +476,7 @@
    1.28  
    1.29  lemma hcmod_complex_polar [simp]:
    1.30    "\<And>r a. hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = \<bar>r\<bar>"
    1.31 -  by transfer (simp add: cmod_complex_polar)
    1.32 +  by transfer (simp add: Complex_eq cmod_complex_polar)
    1.33  
    1.34  lemma hcmod_hrcis [simp]: "\<And>r a. hcmod(hrcis r a) = \<bar>r\<bar>"
    1.35    by transfer (rule complex_mod_rcis)