Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
authorpaulson <lp15@cam.ac.uk>
Tue Feb 28 13:51:47 2017 +0000 (2017-02-28)
changeset 65064a4abec71279a
parent 65062 dc746d43f40e
child 65065 3d7ec12f7af7
Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
NEWS
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Conformal_Mappings.thy
src/HOL/Analysis/Further_Topology.thy
src/HOL/Analysis/Great_Picard.thy
src/HOL/Analysis/Homeomorphism.thy
src/HOL/Analysis/Inner_Product.thy
src/HOL/Analysis/Jordan_Curve.thy
src/HOL/Analysis/Winding_Numbers.thy
src/HOL/Complex.thy
src/HOL/Probability/Characteristic_Functions.thy
src/HOL/Probability/Levy.thy
     1.1 --- a/NEWS	Tue Feb 28 08:18:12 2017 +0100
     1.2 +++ b/NEWS	Tue Feb 28 13:51:47 2017 +0000
     1.3 @@ -63,6 +63,10 @@
     1.4  * Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Renamed ii to imaginary_unit in order to free up ii as a variable name.
     1.8 +The syntax \<i> remains available.
     1.9 +INCOMPATIBILITY.
    1.10 +
    1.11  * Dropped abbreviations transP, antisymP, single_valuedP;
    1.12  use constants transp, antisymp, single_valuedp instead.
    1.13  INCOMPATIBILITY.
     2.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Feb 28 08:18:12 2017 +0100
     2.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Feb 28 13:51:47 2017 +0000
     2.3 @@ -76,7 +76,7 @@
     2.4  subsection\<open>Euler and de Moivre formulas.\<close>
     2.5  
     2.6  text\<open>The sine series times @{term i}\<close>
     2.7 -lemma sin_ii_eq: "(\<lambda>n. (\<i> * sin_coeff n) * z^n) sums (\<i> * sin z)"
     2.8 +lemma sin_i_eq: "(\<lambda>n. (\<i> * sin_coeff n) * z^n) sums (\<i> * sin z)"
     2.9  proof -
    2.10    have "(\<lambda>n. \<i> * sin_coeff n *\<^sub>R z^n) sums (\<i> * sin z)"
    2.11      using sin_converges sums_mult by blast
    2.12 @@ -97,7 +97,7 @@
    2.13      by (rule exp_converges)
    2.14    finally have "(\<lambda>n. (cos_coeff n + \<i> * sin_coeff n) * z^n) sums (exp (\<i> * z))" .
    2.15    moreover have "(\<lambda>n. (cos_coeff n + \<i> * sin_coeff n) * z^n) sums (cos z + \<i> * sin z)"
    2.16 -    using sums_add [OF cos_converges [of z] sin_ii_eq [of z]]
    2.17 +    using sums_add [OF cos_converges [of z] sin_i_eq [of z]]
    2.18      by (simp add: field_simps scaleR_conv_of_real)
    2.19    ultimately show ?thesis
    2.20      using sums_unique2 by blast
    2.21 @@ -395,7 +395,7 @@
    2.22    finally show ?thesis .
    2.23  qed
    2.24  
    2.25 -lemma dist_exp_ii_1: "norm(exp(\<i> * of_real t) - 1) = 2 * \<bar>sin(t / 2)\<bar>"
    2.26 +lemma dist_exp_i_1: "norm(exp(\<i> * of_real t) - 1) = 2 * \<bar>sin(t / 2)\<bar>"
    2.27    apply (simp add: exp_Euler cmod_def power2_diff sin_of_real cos_of_real algebra_simps)
    2.28    using cos_double_sin [of "t/2"]
    2.29    apply (simp add: real_sqrt_mult)
    2.30 @@ -489,7 +489,7 @@
    2.31    shows "(exp z - inverse (exp z)) / 2 = -\<i> * sin(\<i> * z)"
    2.32    by (simp add: sin_exp_eq divide_simps exp_minus of_real_numeral)
    2.33  
    2.34 -lemma sin_ii_times:
    2.35 +lemma sin_i_times:
    2.36    fixes z :: complex
    2.37    shows "sin(\<i> * z) = \<i> * ((exp z - inverse (exp z)) / 2)"
    2.38    using sinh_complex by auto
    2.39 @@ -497,7 +497,7 @@
    2.40  lemma sinh_real:
    2.41    fixes x :: real
    2.42    shows "of_real((exp x - inverse (exp x)) / 2) = -\<i> * sin(\<i> * of_real x)"
    2.43 -  by (simp add: exp_of_real sin_ii_times of_real_numeral)
    2.44 +  by (simp add: exp_of_real sin_i_times of_real_numeral)
    2.45  
    2.46  lemma cosh_complex:
    2.47    fixes z :: complex
    2.48 @@ -509,7 +509,7 @@
    2.49    shows "of_real((exp x + inverse (exp x)) / 2) = cos(\<i> * of_real x)"
    2.50    by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
    2.51  
    2.52 -lemmas cos_ii_times = cosh_complex [symmetric]
    2.53 +lemmas cos_i_times = cosh_complex [symmetric]
    2.54  
    2.55  lemma norm_cos_squared:
    2.56      "norm(cos z) ^ 2 = cos(Re z) ^ 2 + (exp(Im z) - inverse(exp(Im z))) ^ 2 / 4"
    2.57 @@ -1386,7 +1386,7 @@
    2.58                            else Ln(z) - \<i> * of_real(3 * pi/2))"
    2.59    using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
    2.60          Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
    2.61 -  by (simp add: Ln_times) auto 
    2.62 +  by (simp add: Ln_times) auto
    2.63  
    2.64  lemma Ln_of_nat: "0 < n \<Longrightarrow> Ln (of_nat n) = of_real (ln (of_nat n))"
    2.65    by (subst of_real_of_nat_eq[symmetric], subst Ln_of_real[symmetric]) simp_all
    2.66 @@ -1500,7 +1500,7 @@
    2.67  lemma Ln_series': "cmod z < 1 \<Longrightarrow> (\<lambda>n. - ((-z)^n) / of_nat n) sums ln (1 + z)"
    2.68    by (drule Ln_series) (simp add: power_minus')
    2.69  
    2.70 -lemma ln_series': 
    2.71 +lemma ln_series':
    2.72    assumes "abs (x::real) < 1"
    2.73    shows   "(\<lambda>n. - ((-x)^n) / of_nat n) sums ln (1 + x)"
    2.74  proof -
    2.75 @@ -1508,7 +1508,7 @@
    2.76      by (intro Ln_series') simp_all
    2.77    also have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) = (\<lambda>n. complex_of_real (- ((-x)^n) / of_nat n))"
    2.78      by (rule ext) simp
    2.79 -  also from assms have "ln (1 + complex_of_real x) = of_real (ln (1 + x))" 
    2.80 +  also from assms have "ln (1 + complex_of_real x) = of_real (ln (1 + x))"
    2.81      by (subst Ln_of_real [symmetric]) simp_all
    2.82    finally show ?thesis by (subst (asm) sums_of_real_iff)
    2.83  qed
    2.84 @@ -2197,7 +2197,7 @@
    2.85    show ?thesis
    2.86      using assms *
    2.87      apply (simp add: Arctan_def tan_def sin_exp_eq cos_exp_eq exp_minus divide_simps
    2.88 -                     ii_times_eq_iff power2_eq_square [symmetric])
    2.89 +                     i_times_eq_iff power2_eq_square [symmetric])
    2.90      apply (rule Ln_unique)
    2.91      apply (auto simp: divide_simps exp_minus)
    2.92      apply (simp add: algebra_simps exp_double [symmetric])
    2.93 @@ -2211,14 +2211,14 @@
    2.94  proof -
    2.95    have nz0: "1 + \<i>*z \<noteq> 0"
    2.96      using assms
    2.97 -    by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add ii.simps(1) ii.simps(2)
    2.98 +    by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add imaginary_unit.simps
    2.99                less_irrefl minus_diff_eq mult.right_neutral right_minus_eq)
   2.100    have "z \<noteq> -\<i>" using assms
   2.101      by auto
   2.102    then have zz: "1 + z * z \<noteq> 0"
   2.103 -    by (metis abs_one assms i_squared ii.simps less_irrefl minus_unique square_eq_iff)
   2.104 +    by (metis abs_one assms i_squared imaginary_unit.simps less_irrefl minus_unique square_eq_iff)
   2.105    have nz1: "1 - \<i>*z \<noteq> 0"
   2.106 -    using assms by (force simp add: ii_times_eq_iff)
   2.107 +    using assms by (force simp add: i_times_eq_iff)
   2.108    have nz2: "inverse (1 + \<i>*z) \<noteq> 0"
   2.109      using assms
   2.110      by (metis Im_complex_div_lemma Re_complex_div_lemma cmod_eq_Im divide_complex_def
   2.111 @@ -2380,7 +2380,7 @@
   2.112  
   2.113  subsection \<open>Real arctangent\<close>
   2.114  
   2.115 -lemma norm_exp_ii_times [simp]: "norm (exp(\<i> * of_real y)) = 1"
   2.116 +lemma norm_exp_i_times [simp]: "norm (exp(\<i> * of_real y)) = 1"
   2.117    by simp
   2.118  
   2.119  lemma norm_exp_imaginary: "norm(exp z) = 1 \<Longrightarrow> Re z = 0"
   2.120 @@ -2647,7 +2647,7 @@
   2.121  lemma Re_eq_pihalf_lemma:
   2.122      "\<bar>Re z\<bar> = pi/2 \<Longrightarrow> Im z = 0 \<Longrightarrow>
   2.123        Re ((exp (\<i>*z) + inverse (exp (\<i>*z))) / 2) = 0 \<and> 0 \<le> Im ((exp (\<i>*z) + inverse (exp (\<i>*z))) / 2)"
   2.124 -  apply (simp add: cos_ii_times [symmetric] Re_cos Im_cos abs_if del: eq_divide_eq_numeral1)
   2.125 +  apply (simp add: cos_i_times [symmetric] Re_cos Im_cos abs_if del: eq_divide_eq_numeral1)
   2.126    by (metis cos_minus cos_pi_half)
   2.127  
   2.128  lemma Re_less_pihalf_lemma:
   2.129 @@ -2657,7 +2657,7 @@
   2.130    have "0 < cos (Re z)" using assms
   2.131      using cos_gt_zero_pi by auto
   2.132    then show ?thesis
   2.133 -    by (simp add: cos_ii_times [symmetric] Re_cos Im_cos add_pos_pos)
   2.134 +    by (simp add: cos_i_times [symmetric] Re_cos Im_cos add_pos_pos)
   2.135  qed
   2.136  
   2.137  lemma Arcsin_sin:
   2.138 @@ -2931,9 +2931,9 @@
   2.139    also have "... \<le> (cmod w)\<^sup>2"
   2.140      by (auto simp: cmod_power2)
   2.141    finally show ?thesis
   2.142 -    using abs_le_square_iff by force 
   2.143 +    using abs_le_square_iff by force
   2.144  qed
   2.145 -  
   2.146 +
   2.147  lemma Re_Arcsin_bounds: "-pi < Re(Arcsin z) & Re(Arcsin z) \<le> pi"
   2.148    unfolding Re_Arcsin
   2.149    by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arcsin_body_lemma)
   2.150 @@ -3606,7 +3606,7 @@
   2.151         then have *: "(Arg (exp (\<i>*(2* of_real pi* of_real x))) / (2*pi)) = x"
   2.152           using that by (auto simp: Arg_exp divide_simps)
   2.153         show ?thesis
   2.154 -         by (rule_tac x="exp(ii* of_real(2*pi*x))" in bexI) (auto simp: *)
   2.155 +         by (rule_tac x="exp(\<i> * of_real(2*pi*x))" in bexI) (auto simp: *)
   2.156      qed
   2.157      ultimately show "(\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) ` sphere 0 1 = path_image \<gamma>"
   2.158        by (auto simp: path_image_def image_iff)
     3.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Tue Feb 28 08:18:12 2017 +0100
     3.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Tue Feb 28 13:51:47 2017 +0000
     3.3 @@ -2277,7 +2277,7 @@
     3.4        and e'_def:"\<forall>\<epsilon>>0. \<epsilon><e' \<longrightarrow> (f has_contour_integral c * (residue f z)) (circlepath z \<epsilon>)"
     3.5      by auto
     3.6    let ?int="\<lambda>e. contour_integral (circlepath z e) f"
     3.7 -  def \<epsilon>\<equiv>"Min {r,e'} / 2"
     3.8 +  define  \<epsilon> where "\<epsilon> \<equiv> Min {r,e'} / 2"
     3.9    have "\<epsilon>>0" "\<epsilon>\<le>r" "\<epsilon><e'" using \<open>r>0\<close> \<open>e'>0\<close> unfolding \<epsilon>_def by auto
    3.10    have "(f has_contour_integral c * (residue f z)) (circlepath z \<epsilon>)"
    3.11      using e'_def[rule_format,OF \<open>\<epsilon>>0\<close> \<open>\<epsilon><e'\<close>] .
    3.12 @@ -2341,8 +2341,8 @@
    3.13    thus ?thesis using residue_const by auto
    3.14  next
    3.15    case False
    3.16 -  def c'\<equiv>"2 * pi * \<i>"
    3.17 -  def f'\<equiv>"(\<lambda>z. c * (f z))"
    3.18 +  define c' where "c' \<equiv> 2 * pi * \<i>"
    3.19 +  define f' where "f' \<equiv> (\<lambda>z. c * (f z))"
    3.20    obtain e where "e>0" and e_cball:"cball z e \<subseteq> s" using \<open>open s\<close> \<open>z\<in>s\<close>
    3.21      using open_contains_cball_eq by blast
    3.22    have "(f' has_contour_integral c' * residue f' z) (circlepath z e)"
    3.23 @@ -2386,7 +2386,7 @@
    3.24    shows "residue (\<lambda>w. f w / (w - z)) z = f z"
    3.25  proof -
    3.26    define c where "c \<equiv> 2 * pi * \<i>"
    3.27 -  def f'\<equiv>"\<lambda>w. f w / (w - z)"
    3.28 +  define f' where "f' \<equiv> \<lambda>w. f w / (w - z)"
    3.29    obtain e where "e>0" and e_cball:"cball z e \<subseteq> s" using \<open>open s\<close> \<open>z\<in>s\<close>
    3.30      using open_contains_cball_eq by blast
    3.31    have "(f' has_contour_integral c * f z) (circlepath z e)"
    3.32 @@ -2634,7 +2634,7 @@
    3.33          unfolding cp_def using contour_integral_reversepath[OF n_circ(1)] n_circ(9)
    3.34          by auto
    3.35      qed
    3.36 -  def g'\<equiv>"g +++ pg +++ cp +++ (reversepath pg)"
    3.37 +  define g' where "g' \<equiv> g +++ pg +++ cp +++ (reversepath pg)"
    3.38    have "contour_integral g' f = (\<Sum>p\<in>pts. winding_number g' p * contour_integral (circlepath p (h p)) f)"
    3.39      proof (rule "2.hyps"(3)[of "s-{p}" "g'",OF _ _ \<open>finite pts\<close> ])
    3.40        show "connected (s - {p} - pts)" using connected by (metis Diff_insert2)
    3.41 @@ -2648,7 +2648,7 @@
    3.42          unfolding g'_def cp_def using pg(2) by simp
    3.43        show "path_image g' \<subseteq> s - {p} - pts"
    3.44          proof -
    3.45 -          def s'\<equiv>"s - {p} - pts"
    3.46 +          define s' where "s' \<equiv> s - {p} - pts"
    3.47            have s':"s' = s-insert p pts " unfolding s'_def by auto
    3.48            then show ?thesis using path_img pg(4) cp(4)
    3.49              unfolding g'_def
    3.50 @@ -2994,7 +2994,7 @@
    3.51            "\<And>w. w \<in> ball z r \<Longrightarrow> g w \<noteq> 0"
    3.52      using holomorphic_factor_zero_nonconstant[OF holo \<open>open s\<close> \<open>connected s\<close> \<open>z\<in>s\<close> \<open>f z=0\<close>]
    3.53      by (metis assms(3) assms(5) assms(6))
    3.54 -  def r'\<equiv>"r/2"
    3.55 +  define r' where "r' \<equiv> r/2"
    3.56    have "cball z r' \<subseteq> ball z r" unfolding r'_def by (simp add: \<open>0 < r\<close> cball_subset_ball_iff)
    3.57    hence "cball z r' \<subseteq> s" "g holomorphic_on cball z r'"
    3.58        "(\<forall>w\<in>cball z r'. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0)"
    3.59 @@ -3137,7 +3137,7 @@
    3.60      using h_divide by simp
    3.61    define c where "c \<equiv> 2 * pi * \<i>"
    3.62    define der_f where "der_f \<equiv> ((deriv ^^ (n - 1)) h z / fact (n-1))"
    3.63 -  def h'\<equiv>"\<lambda>u. h u / (u - z) ^ n"
    3.64 +  define h' where "h' \<equiv> \<lambda>u. h u / (u - z) ^ n"
    3.65    have "(h' has_contour_integral c / fact (n - 1) * (deriv ^^ (n - 1)) h z) (circlepath z r)"
    3.66      unfolding h'_def
    3.67      proof (rule Cauchy_has_contour_integral_higher_derivative_circlepath[of z r h z "n-1",
    3.68 @@ -3193,8 +3193,8 @@
    3.69          proof -
    3.70            define po where "po \<equiv> porder f p"
    3.71            define pp where "pp \<equiv> pol_poly f p"
    3.72 -          def f'\<equiv>"\<lambda>w. pp w / (w - p) ^ po"
    3.73 -          def ff'\<equiv>"(\<lambda>x. deriv f' x * h x / f' x)"
    3.74 +          define f' where "f' \<equiv> \<lambda>w. pp w / (w - p) ^ po"
    3.75 +          define ff' where "ff' \<equiv> (\<lambda>x. deriv f' x * h x / f' x)"
    3.76            have "f holomorphic_on ball p e1 - {p}"
    3.77              apply (intro holomorphic_on_subset[OF f_holo])
    3.78              using e1_avoid \<open>p\<in>poles\<close> unfolding avoid_def by auto
    3.79 @@ -3301,8 +3301,8 @@
    3.80          proof -
    3.81            define zo where "zo \<equiv> zorder f p"
    3.82            define zp where "zp \<equiv> zer_poly f p"
    3.83 -          def f'\<equiv>"\<lambda>w. zp w * (w - p) ^ zo"
    3.84 -          def ff'\<equiv>"(\<lambda>x. deriv f' x * h x / f' x)"
    3.85 +          define f' where "f' \<equiv> \<lambda>w. zp w * (w - p) ^ zo"
    3.86 +          define ff' where "ff' \<equiv> (\<lambda>x. deriv f' x * h x / f' x)"
    3.87            have "f holomorphic_on ball p e1"
    3.88              proof -
    3.89                have "ball p e1 \<subseteq> s - poles"
    3.90 @@ -3313,8 +3313,8 @@
    3.91              using DiffD1 mem_Collect_eq zeros_def by blast
    3.92            moreover have "\<exists>w\<in>ball p e1. f w \<noteq> 0"
    3.93              proof -
    3.94 -              def p'\<equiv>"p+e1/2"
    3.95 -              have "p'\<in>ball p e1" and "p'\<noteq>p" using \<open>e1>0\<close> unfolding p'_def by (auto simp add:dist_norm)
    3.96 +              define p' where "p' \<equiv> p+e1/2"
    3.97 +              have "p' \<in> ball p e1" and "p'\<noteq>p" using \<open>e1>0\<close> unfolding p'_def by (auto simp add:dist_norm)
    3.98                then show "\<exists>w\<in>ball p e1. f w \<noteq> 0" using e1_avoid unfolding avoid_def
    3.99                  apply (rule_tac x=p' in bexI)
   3.100                  by (auto simp add:zeros_def)
     4.1 --- a/src/HOL/Analysis/Further_Topology.thy	Tue Feb 28 08:18:12 2017 +0100
     4.2 +++ b/src/HOL/Analysis/Further_Topology.thy	Tue Feb 28 13:51:47 2017 +0000
     4.3 @@ -3131,7 +3131,7 @@
     4.4        then have "cmod (exp (\<i> * of_real (2 * pi * j / n)) - 1) < 2 * sin (pi / real n)"
     4.5          by (simp add: j field_simps)
     4.6        then have "2 * \<bar>sin((2 * pi * j / n) / 2)\<bar> < 2 * sin (pi / real n)"
     4.7 -        by (simp only: dist_exp_ii_1)
     4.8 +        by (simp only: dist_exp_i_1)
     4.9        then have sin_less: "sin((pi * j / n)) < sin (pi / real n)"
    4.10          by (simp add: field_simps)
    4.11        then have "w / z = 1"
    4.12 @@ -3179,7 +3179,7 @@
    4.13                      (\<forall>u\<in>v. Ex (homeomorphism u T (\<lambda>z. z^n))))"
    4.14             if "z \<noteq> 0" for z::complex
    4.15    proof -
    4.16 -    def d \<equiv> "min (1/2) (e/4) * norm z"
    4.17 +    define d where "d \<equiv> min (1/2) (e/4) * norm z"
    4.18      have "0 < d"
    4.19        by (simp add: d_def \<open>0 < e\<close> \<open>z \<noteq> 0\<close>)
    4.20      have iff_x_eq_y: "x^n = y^n \<longleftrightarrow> x = y"
    4.21 @@ -3502,7 +3502,7 @@
    4.22  lemma inessential_eq_continuous_logarithm_circle:
    4.23    fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
    4.24    shows "(\<exists>a. homotopic_with (\<lambda>h. True) S (sphere 0 1) f (\<lambda>t. a)) \<longleftrightarrow>
    4.25 -         (\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(ii* of_real(g x))))"
    4.26 +         (\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(\<i> * of_real(g x))))"
    4.27    (is "?lhs \<longleftrightarrow> ?rhs")
    4.28  proof
    4.29    assume L: ?lhs
    4.30 @@ -3519,9 +3519,9 @@
    4.31      done
    4.32  next
    4.33    assume ?rhs
    4.34 -  then obtain g where contg: "continuous_on S g" and g: "\<And>x. x \<in> S \<Longrightarrow> f x = exp(ii* of_real(g x))"
    4.35 +  then obtain g where contg: "continuous_on S g" and g: "\<And>x. x \<in> S \<Longrightarrow> f x = exp(\<i>* of_real(g x))"
    4.36      by metis
    4.37 -  obtain a where "homotopic_with (\<lambda>h. True) S (sphere 0 1) ((exp \<circ> (\<lambda>z. ii*z)) \<circ> (of_real \<circ> g)) (\<lambda>x. a)"
    4.38 +  obtain a where "homotopic_with (\<lambda>h. True) S (sphere 0 1) ((exp \<circ> (\<lambda>z. \<i>*z)) \<circ> (of_real \<circ> g)) (\<lambda>x. a)"
    4.39    proof (rule nullhomotopic_through_contractible)
    4.40      show "continuous_on S (complex_of_real \<circ> g)"
    4.41        by (intro conjI contg continuous_intros)
    4.42 @@ -4030,7 +4030,7 @@
    4.43    obtain g where holg: "g holomorphic_on S" and eq: "\<And>z. z \<in> S \<Longrightarrow> 1 - (f z)\<^sup>2 = (g z)\<^sup>2"
    4.44      using contractible_imp_holomorphic_sqrt [OF hol1f S]
    4.45      by (metis eq_iff_diff_eq_0 non1 power2_eq_1_iff)
    4.46 -  have holfg: "(\<lambda>z. f z + ii*g z) holomorphic_on S"
    4.47 +  have holfg: "(\<lambda>z. f z + \<i>*g z) holomorphic_on S"
    4.48      by (intro holf holg holomorphic_intros)
    4.49    have "\<And>z. z \<in> S \<Longrightarrow> f z + \<i>*g z \<noteq> 0"
    4.50      by (metis Arccos_body_lemma eq add.commute add.inverse_unique complex_i_mult_minus power2_csqrt power2_eq_iff)
    4.51 @@ -4038,13 +4038,13 @@
    4.52      using contractible_imp_holomorphic_log [OF holfg S] by metis
    4.53    show ?thesis
    4.54    proof
    4.55 -    show "(\<lambda>z. -ii*h z) holomorphic_on S"
    4.56 +    show "(\<lambda>z. -\<i>*h z) holomorphic_on S"
    4.57        by (intro holh holomorphic_intros)
    4.58      show "f z = cos (- \<i>*h z)" if "z \<in> S" for z
    4.59      proof -
    4.60 -      have "(f z + ii*g z)*(f z - ii*g z) = 1"
    4.61 +      have "(f z + \<i>*g z)*(f z - \<i>*g z) = 1"
    4.62          using that eq by (auto simp: algebra_simps power2_eq_square)
    4.63 -      then have "f z - ii*g z = inverse (f z + ii*g z)"
    4.64 +      then have "f z - \<i>*g z = inverse (f z + \<i>*g z)"
    4.65          using inverse_unique by force
    4.66        also have "... = exp (- h z)"
    4.67          by (simp add: exp_minus fgeq that)
    4.68 @@ -4214,7 +4214,7 @@
    4.69    fixes S :: "'a::real_normed_vector set"
    4.70    shows "Borsukian S \<longleftrightarrow>
    4.71           (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::complex) 1
    4.72 -              \<longrightarrow> (\<exists>g. continuous_on S (complex_of_real \<circ> g) \<and> (\<forall>x \<in> S. f x = exp(ii * of_real(g x)))))"
    4.73 +              \<longrightarrow> (\<exists>g. continuous_on S (complex_of_real \<circ> g) \<and> (\<forall>x \<in> S. f x = exp(\<i> * of_real(g x)))))"
    4.74     (is "?lhs = ?rhs")
    4.75  proof
    4.76    assume LHS: ?lhs
    4.77 @@ -4236,10 +4236,10 @@
    4.78    proof (clarsimp simp: Borsukian_continuous_logarithm_circle)
    4.79      fix f :: "'a \<Rightarrow> complex"
    4.80      assume "continuous_on S f" and f01: "f ` S \<subseteq> sphere 0 1"
    4.81 -    then obtain g where contg: "continuous_on S (complex_of_real \<circ> g)" and "\<And>x. x \<in> S \<Longrightarrow> f x =  exp(ii * of_real(g x))"
    4.82 +    then obtain g where contg: "continuous_on S (complex_of_real \<circ> g)" and "\<And>x. x \<in> S \<Longrightarrow> f x =  exp(\<i> * of_real(g x))"
    4.83        by (metis RHS)
    4.84      then show "\<exists>g. continuous_on S g \<and> (\<forall>x\<in>S. f x = exp (g x))"
    4.85 -      by (rule_tac x="\<lambda>x. ii* of_real(g x)" in exI) (auto simp: continuous_intros contg)
    4.86 +      by (rule_tac x="\<lambda>x. \<i>* of_real(g x)" in exI) (auto simp: continuous_intros contg)
    4.87    qed
    4.88  qed
    4.89  
    4.90 @@ -4503,7 +4503,7 @@
    4.91    moreover have "(g \<circ> f) ` S \<subseteq> sphere 0 1"
    4.92      using fim gim by auto
    4.93    ultimately obtain h where cont_cxh: "continuous_on S (complex_of_real \<circ> h)"
    4.94 -                       and gfh: "\<And>x. x \<in> S \<Longrightarrow> (g \<circ> f) x = exp(ii * of_real(h x))"
    4.95 +                       and gfh: "\<And>x. x \<in> S \<Longrightarrow> (g \<circ> f) x = exp(\<i> * of_real(h x))"
    4.96      using \<open>Borsukian S\<close> Borsukian_continuous_logarithm_circle_real  by metis
    4.97    then have conth: "continuous_on S h"
    4.98      by simp
     5.1 --- a/src/HOL/Analysis/Great_Picard.thy	Tue Feb 28 08:18:12 2017 +0100
     5.2 +++ b/src/HOL/Analysis/Great_Picard.thy	Tue Feb 28 13:51:47 2017 +0000
     5.3 @@ -1146,7 +1146,7 @@
     5.4    qed
     5.5    moreover
     5.6    have "contour_integral (circlepath z0 (r/2)) (\<lambda>z. m / (z - z0) + deriv h z / h z) =
     5.7 -        2 * of_real pi * ii * m + 0"
     5.8 +        2 * of_real pi * \<i> * m + 0"
     5.9    proof (rule contour_integral_unique [OF has_contour_integral_add])
    5.10      show "((\<lambda>x. m / (x - z0)) has_contour_integral 2 * of_real pi * \<i> * m) (circlepath z0 (r/2))"
    5.11        by (force simp: \<open>0 < r\<close> intro: Cauchy_integral_circlepath_simple)
     6.1 --- a/src/HOL/Analysis/Homeomorphism.thy	Tue Feb 28 08:18:12 2017 +0100
     6.2 +++ b/src/HOL/Analysis/Homeomorphism.thy	Tue Feb 28 13:51:47 2017 +0000
     6.3 @@ -1330,7 +1330,7 @@
     6.4      shows "g1 x = g2 x"
     6.5  proof -
     6.6    have "U \<subseteq> T" by (rule in_components_subset [OF u_compt])
     6.7 -  def G12 \<equiv> "{x \<in> U. g1 x - g2 x = 0}"
     6.8 +  define G12 where "G12 \<equiv> {x \<in> U. g1 x - g2 x = 0}"
     6.9    have "connected U" by (rule in_components_connected [OF u_compt])
    6.10    have contu: "continuous_on U g1" "continuous_on U g2"
    6.11         using \<open>U \<subseteq> T\<close> continuous_on_subset g1 g2 by blast+
     7.1 --- a/src/HOL/Analysis/Inner_Product.thy	Tue Feb 28 08:18:12 2017 +0100
     7.2 +++ b/src/HOL/Analysis/Inner_Product.thy	Tue Feb 28 13:51:47 2017 +0000
     7.3 @@ -298,10 +298,10 @@
     7.4  lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
     7.5    unfolding inner_complex_def by simp
     7.6  
     7.7 -lemma complex_inner_ii_left [simp]: "inner \<i> x = Im x"
     7.8 +lemma complex_inner_i_left [simp]: "inner \<i> x = Im x"
     7.9    unfolding inner_complex_def by simp
    7.10  
    7.11 -lemma complex_inner_ii_right [simp]: "inner x \<i> = Im x"
    7.12 +lemma complex_inner_i_right [simp]: "inner x \<i> = Im x"
    7.13    unfolding inner_complex_def by simp
    7.14  
    7.15  
     8.1 --- a/src/HOL/Analysis/Jordan_Curve.thy	Tue Feb 28 08:18:12 2017 +0100
     8.2 +++ b/src/HOL/Analysis/Jordan_Curve.thy	Tue Feb 28 13:51:47 2017 +0000
     8.3 @@ -90,7 +90,7 @@
     8.4      qed
     8.5      ultimately obtain z where z: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = z"
     8.6        using continuous_discrete_range_constant [OF conST contgh] by blast
     8.7 -    obtain w where "exp(ii* of_real(h w)) = exp (ii* of_real(z + h w))"
     8.8 +    obtain w where "exp(\<i> * of_real(h w)) = exp (\<i> * of_real(z + h w))"
     8.9        using disc z False
    8.10        by auto (metis diff_add_cancel g h of_real_add)
    8.11      then have [simp]: "exp (\<i>* of_real z) = 1"
     9.1 --- a/src/HOL/Analysis/Winding_Numbers.thy	Tue Feb 28 08:18:12 2017 +0100
     9.2 +++ b/src/HOL/Analysis/Winding_Numbers.thy	Tue Feb 28 13:51:47 2017 +0000
     9.3 @@ -39,7 +39,7 @@
     9.4          assume "0 \<in> interior {z. Im z * Re b \<le> Im b * Re z}"
     9.5          then obtain e where "e>0" and e: "ball 0 e \<subseteq> {z. Im z * Re b \<le> Im b * Re z}"
     9.6            by (meson mem_interior)
     9.7 -        def z \<equiv> "- sgn (Im b) * (e/3) + sgn (Re b) * (e/3) * ii"
     9.8 +        define z where "z \<equiv> - sgn (Im b) * (e/3) + sgn (Re b) * (e/3) * \<i>"
     9.9          have "z \<in> ball 0 e"
    9.10            using `e>0`
    9.11            apply (simp add: z_def dist_norm)
    10.1 --- a/src/HOL/Complex.thy	Tue Feb 28 08:18:12 2017 +0100
    10.2 +++ b/src/HOL/Complex.thy	Tue Feb 28 13:51:47 2017 +0000
    10.3 @@ -202,7 +202,7 @@
    10.4  
    10.5  subsection \<open>The Complex Number $i$\<close>
    10.6  
    10.7 -primcorec "ii" :: complex  ("\<i>")
    10.8 +primcorec imaginary_unit :: complex  ("\<i>")
    10.9    where
   10.10      "Re \<i> = 0"
   10.11    | "Im \<i> = 1"
   10.12 @@ -249,13 +249,13 @@
   10.13  lemma i_even_power [simp]: "\<i> ^ (n * 2) = (-1) ^ n"
   10.14    by (metis mult.commute power2_i power_mult)
   10.15  
   10.16 -lemma Re_ii_times [simp]: "Re (\<i> * z) = - Im z"
   10.17 +lemma Re_i_times [simp]: "Re (\<i> * z) = - Im z"
   10.18    by simp
   10.19  
   10.20 -lemma Im_ii_times [simp]: "Im (\<i> * z) = Re z"
   10.21 +lemma Im_i_times [simp]: "Im (\<i> * z) = Re z"
   10.22    by simp
   10.23  
   10.24 -lemma ii_times_eq_iff: "\<i> * w = z \<longleftrightarrow> w = - (\<i> * z)"
   10.25 +lemma i_times_eq_iff: "\<i> * w = z \<longleftrightarrow> w = - (\<i> * z)"
   10.26    by auto
   10.27  
   10.28  lemma divide_numeral_i [simp]: "z / (numeral n * \<i>) = - (\<i> * z) / numeral n"
    11.1 --- a/src/HOL/Probability/Characteristic_Functions.thy	Tue Feb 28 08:18:12 2017 +0100
    11.2 +++ b/src/HOL/Probability/Characteristic_Functions.thy	Tue Feb 28 13:51:47 2017 +0000
    11.3 @@ -69,7 +69,7 @@
    11.4    from f have "\<And>x. of_real (Re (f x)) = f x"
    11.5      by (simp add: complex_eq_iff)
    11.6    then show "AE x in M. cmod (exp (\<i> * f x)) \<le> 1"
    11.7 -    using norm_exp_ii_times[of "Re (f x)" for x] by simp
    11.8 +    using norm_exp_i_times[of "Re (f x)" for x] by simp
    11.9  qed (insert f, simp)
   11.10  
   11.11  lemma (in real_distribution) cmod_char_le_1: "norm (char M t) \<le> 1"
    12.1 --- a/src/HOL/Probability/Levy.thy	Tue Feb 28 08:18:12 2017 +0100
    12.2 +++ b/src/HOL/Probability/Levy.thy	Tue Feb 28 13:51:47 2017 +0000
    12.3 @@ -60,7 +60,7 @@
    12.4    have "?F = cmod (iexp (t * a) * (iexp (t * (b - a)) - 1) / (\<i> * t))"
    12.5      using \<open>t \<noteq> 0\<close> by (intro arg_cong[where f=norm]) (simp add: field_simps exp_diff exp_minus)
    12.6    also have "\<dots> = cmod (iexp (t * (b - a)) - 1) / abs t"
    12.7 -    unfolding norm_divide norm_mult norm_exp_ii_times using \<open>t \<noteq> 0\<close>
    12.8 +    unfolding norm_divide norm_mult norm_exp_i_times using \<open>t \<noteq> 0\<close>
    12.9      by (simp add: complex_eq_iff norm_mult)
   12.10    also have "\<dots> \<le> abs (t * (b - a)) / abs t"
   12.11      using iexp_approx1 [of "t * (b - a)" 0]