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)