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)
```