src/HOL/Complex.thy
 changeset 63040 eb4ddd18d635 parent 62620 d21dab28b3f9 child 63114 27afe7af7379
```     1.1 --- a/src/HOL/Complex.thy	Sun Apr 24 21:31:14 2016 +0200
1.2 +++ b/src/HOL/Complex.thy	Mon Apr 25 16:09:26 2016 +0200
1.3 @@ -817,7 +817,8 @@
1.4    from assms have "z \<noteq> 0" by auto
1.5    have "(SOME a. sgn z = cis a \<and> -pi < a \<and> a \<le> pi) = x"
1.6    proof
1.7 -    fix a def d \<equiv> "a - x"
1.8 +    fix a
1.9 +    define d where "d = a - x"
1.10      assume a: "sgn z = cis a \<and> - pi < a \<and> a \<le> pi"
1.11      from a assms have "- (2*pi) < d \<and> d < 2*pi"
1.12        unfolding d_def by simp
1.13 @@ -839,7 +840,7 @@
1.14  proof (simp add: arg_def assms, rule someI_ex)
1.15    obtain r a where z: "z = rcis r a" using rcis_Ex by fast
1.16    with assms have "r \<noteq> 0" by auto
1.17 -  def b \<equiv> "if 0 < r then a else a + pi"
1.18 +  define b where "b = (if 0 < r then a else a + pi)"
1.19    have b: "sgn z = cis b"
1.20      unfolding z b_def rcis_def using \<open>r \<noteq> 0\<close>
1.21      by (simp add: of_real_def sgn_scaleR sgn_if complex_eq_iff)
1.22 @@ -848,7 +849,7 @@
1.23    have cis_2pi_int: "\<And>x. cis (2 * pi * real_of_int x) = 1"
1.24      by (case_tac x rule: int_diff_cases)
1.25         (simp add: right_diff_distrib cis_divide [symmetric] cis_2pi_nat)
1.26 -  def c \<equiv> "b - 2*pi * of_int \<lceil>(b - pi) / (2*pi)\<rceil>"
1.27 +  define c where "c = b - 2 * pi * of_int \<lceil>(b - pi) / (2 * pi)\<rceil>"
1.28    have "sgn z = cis c"
1.29      unfolding b c_def
1.30      by (simp add: cis_divide [symmetric] cis_2pi_int)
```