# HG changeset patch
# User wenzelm
# Date 1488295565 -3600
# Node ID a2522ea4321606ab91c93758e2b73da3bc27a6f6
# Parent  c64d778a593a16bd6b0b7c624fc28757714bcba8# Parent  8bc9de2278c0eb02ac5dd7ba2de34eaf1c4008ee
merged;

diff -r 8bc9de2278c0 -r a2522ea43216 NEWS
--- a/NEWS	Tue Feb 28 12:42:50 2017 +0100
+++ b/NEWS	Tue Feb 28 16:26:05 2017 +0100
@@ -63,6 +63,10 @@
 * Dropped aliasses RangeP, DomainP for Rangep, Domainp respectively.
 INCOMPATIBILITY.
 
+* Renamed ii to imaginary_unit in order to free up ii as a variable name.
+The syntax \<i> remains available.
+INCOMPATIBILITY.
+
 * Dropped abbreviations transP, antisymP, single_valuedP;
 use constants transp, antisymp, single_valuedp instead.
 INCOMPATIBILITY.
diff -r 8bc9de2278c0 -r a2522ea43216 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Feb 28 12:42:50 2017 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Tue Feb 28 16:26:05 2017 +0100
@@ -76,7 +76,7 @@
 subsection\<open>Euler and de Moivre formulas.\<close>
 
 text\<open>The sine series times @{term i}\<close>
-lemma sin_ii_eq: "(\<lambda>n. (\<i> * sin_coeff n) * z^n) sums (\<i> * sin z)"
+lemma sin_i_eq: "(\<lambda>n. (\<i> * sin_coeff n) * z^n) sums (\<i> * sin z)"
 proof -
   have "(\<lambda>n. \<i> * sin_coeff n *\<^sub>R z^n) sums (\<i> * sin z)"
     using sin_converges sums_mult by blast
@@ -97,7 +97,7 @@
     by (rule exp_converges)
   finally have "(\<lambda>n. (cos_coeff n + \<i> * sin_coeff n) * z^n) sums (exp (\<i> * z))" .
   moreover have "(\<lambda>n. (cos_coeff n + \<i> * sin_coeff n) * z^n) sums (cos z + \<i> * sin z)"
-    using sums_add [OF cos_converges [of z] sin_ii_eq [of z]]
+    using sums_add [OF cos_converges [of z] sin_i_eq [of z]]
     by (simp add: field_simps scaleR_conv_of_real)
   ultimately show ?thesis
     using sums_unique2 by blast
@@ -395,7 +395,7 @@
   finally show ?thesis .
 qed
 
-lemma dist_exp_ii_1: "norm(exp(\<i> * of_real t) - 1) = 2 * \<bar>sin(t / 2)\<bar>"
+lemma dist_exp_i_1: "norm(exp(\<i> * of_real t) - 1) = 2 * \<bar>sin(t / 2)\<bar>"
   apply (simp add: exp_Euler cmod_def power2_diff sin_of_real cos_of_real algebra_simps)
   using cos_double_sin [of "t/2"]
   apply (simp add: real_sqrt_mult)
@@ -489,7 +489,7 @@
   shows "(exp z - inverse (exp z)) / 2 = -\<i> * sin(\<i> * z)"
   by (simp add: sin_exp_eq divide_simps exp_minus of_real_numeral)
 
-lemma sin_ii_times:
+lemma sin_i_times:
   fixes z :: complex
   shows "sin(\<i> * z) = \<i> * ((exp z - inverse (exp z)) / 2)"
   using sinh_complex by auto
@@ -497,7 +497,7 @@
 lemma sinh_real:
   fixes x :: real
   shows "of_real((exp x - inverse (exp x)) / 2) = -\<i> * sin(\<i> * of_real x)"
-  by (simp add: exp_of_real sin_ii_times of_real_numeral)
+  by (simp add: exp_of_real sin_i_times of_real_numeral)
 
 lemma cosh_complex:
   fixes z :: complex
@@ -509,7 +509,7 @@
   shows "of_real((exp x + inverse (exp x)) / 2) = cos(\<i> * of_real x)"
   by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real)
 
-lemmas cos_ii_times = cosh_complex [symmetric]
+lemmas cos_i_times = cosh_complex [symmetric]
 
 lemma norm_cos_squared:
     "norm(cos z) ^ 2 = cos(Re z) ^ 2 + (exp(Im z) - inverse(exp(Im z))) ^ 2 / 4"
@@ -1386,7 +1386,7 @@
                           else Ln(z) - \<i> * of_real(3 * pi/2))"
   using Im_Ln_le_pi [of z] mpi_less_Im_Ln [of z] assms
         Im_Ln_eq_pi [of z] Im_Ln_pos_lt [of z] Re_Ln_pos_le [of z]
-  by (simp add: Ln_times) auto 
+  by (simp add: Ln_times) auto
 
 lemma Ln_of_nat: "0 < n \<Longrightarrow> Ln (of_nat n) = of_real (ln (of_nat n))"
   by (subst of_real_of_nat_eq[symmetric], subst Ln_of_real[symmetric]) simp_all
@@ -1500,7 +1500,7 @@
 lemma Ln_series': "cmod z < 1 \<Longrightarrow> (\<lambda>n. - ((-z)^n) / of_nat n) sums ln (1 + z)"
   by (drule Ln_series) (simp add: power_minus')
 
-lemma ln_series': 
+lemma ln_series':
   assumes "abs (x::real) < 1"
   shows   "(\<lambda>n. - ((-x)^n) / of_nat n) sums ln (1 + x)"
 proof -
@@ -1508,7 +1508,7 @@
     by (intro Ln_series') simp_all
   also have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) = (\<lambda>n. complex_of_real (- ((-x)^n) / of_nat n))"
     by (rule ext) simp
-  also from assms have "ln (1 + complex_of_real x) = of_real (ln (1 + x))" 
+  also from assms have "ln (1 + complex_of_real x) = of_real (ln (1 + x))"
     by (subst Ln_of_real [symmetric]) simp_all
   finally show ?thesis by (subst (asm) sums_of_real_iff)
 qed
@@ -2197,7 +2197,7 @@
   show ?thesis
     using assms *
     apply (simp add: Arctan_def tan_def sin_exp_eq cos_exp_eq exp_minus divide_simps
-                     ii_times_eq_iff power2_eq_square [symmetric])
+                     i_times_eq_iff power2_eq_square [symmetric])
     apply (rule Ln_unique)
     apply (auto simp: divide_simps exp_minus)
     apply (simp add: algebra_simps exp_double [symmetric])
@@ -2211,14 +2211,14 @@
 proof -
   have nz0: "1 + \<i>*z \<noteq> 0"
     using assms
-    by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add ii.simps(1) ii.simps(2)
+    by (metis abs_one complex_i_mult_minus diff_0_right diff_minus_eq_add imaginary_unit.simps
               less_irrefl minus_diff_eq mult.right_neutral right_minus_eq)
   have "z \<noteq> -\<i>" using assms
     by auto
   then have zz: "1 + z * z \<noteq> 0"
-    by (metis abs_one assms i_squared ii.simps less_irrefl minus_unique square_eq_iff)
+    by (metis abs_one assms i_squared imaginary_unit.simps less_irrefl minus_unique square_eq_iff)
   have nz1: "1 - \<i>*z \<noteq> 0"
-    using assms by (force simp add: ii_times_eq_iff)
+    using assms by (force simp add: i_times_eq_iff)
   have nz2: "inverse (1 + \<i>*z) \<noteq> 0"
     using assms
     by (metis Im_complex_div_lemma Re_complex_div_lemma cmod_eq_Im divide_complex_def
@@ -2380,7 +2380,7 @@
 
 subsection \<open>Real arctangent\<close>
 
-lemma norm_exp_ii_times [simp]: "norm (exp(\<i> * of_real y)) = 1"
+lemma norm_exp_i_times [simp]: "norm (exp(\<i> * of_real y)) = 1"
   by simp
 
 lemma norm_exp_imaginary: "norm(exp z) = 1 \<Longrightarrow> Re z = 0"
@@ -2647,7 +2647,7 @@
 lemma Re_eq_pihalf_lemma:
     "\<bar>Re z\<bar> = pi/2 \<Longrightarrow> Im z = 0 \<Longrightarrow>
       Re ((exp (\<i>*z) + inverse (exp (\<i>*z))) / 2) = 0 \<and> 0 \<le> Im ((exp (\<i>*z) + inverse (exp (\<i>*z))) / 2)"
-  apply (simp add: cos_ii_times [symmetric] Re_cos Im_cos abs_if del: eq_divide_eq_numeral1)
+  apply (simp add: cos_i_times [symmetric] Re_cos Im_cos abs_if del: eq_divide_eq_numeral1)
   by (metis cos_minus cos_pi_half)
 
 lemma Re_less_pihalf_lemma:
@@ -2657,7 +2657,7 @@
   have "0 < cos (Re z)" using assms
     using cos_gt_zero_pi by auto
   then show ?thesis
-    by (simp add: cos_ii_times [symmetric] Re_cos Im_cos add_pos_pos)
+    by (simp add: cos_i_times [symmetric] Re_cos Im_cos add_pos_pos)
 qed
 
 lemma Arcsin_sin:
@@ -2931,9 +2931,9 @@
   also have "... \<le> (cmod w)\<^sup>2"
     by (auto simp: cmod_power2)
   finally show ?thesis
-    using abs_le_square_iff by force 
+    using abs_le_square_iff by force
 qed
-  
+
 lemma Re_Arcsin_bounds: "-pi < Re(Arcsin z) & Re(Arcsin z) \<le> pi"
   unfolding Re_Arcsin
   by (blast intro!: mpi_less_Im_Ln Im_Ln_le_pi Arcsin_body_lemma)
@@ -3606,7 +3606,7 @@
        then have *: "(Arg (exp (\<i>*(2* of_real pi* of_real x))) / (2*pi)) = x"
          using that by (auto simp: Arg_exp divide_simps)
        show ?thesis
-         by (rule_tac x="exp(ii* of_real(2*pi*x))" in bexI) (auto simp: *)
+         by (rule_tac x="exp(\<i> * of_real(2*pi*x))" in bexI) (auto simp: *)
     qed
     ultimately show "(\<gamma> \<circ> (\<lambda>z. Arg z / (2*pi))) ` sphere 0 1 = path_image \<gamma>"
       by (auto simp: path_image_def image_iff)
diff -r 8bc9de2278c0 -r a2522ea43216 src/HOL/Analysis/Conformal_Mappings.thy
--- a/src/HOL/Analysis/Conformal_Mappings.thy	Tue Feb 28 12:42:50 2017 +0100
+++ b/src/HOL/Analysis/Conformal_Mappings.thy	Tue Feb 28 16:26:05 2017 +0100
@@ -2277,7 +2277,7 @@
       and e'_def:"\<forall>\<epsilon>>0. \<epsilon><e' \<longrightarrow> (f has_contour_integral c * (residue f z)) (circlepath z \<epsilon>)"
     by auto
   let ?int="\<lambda>e. contour_integral (circlepath z e) f"
-  def \<epsilon>\<equiv>"Min {r,e'} / 2"
+  define  \<epsilon> where "\<epsilon> \<equiv> Min {r,e'} / 2"
   have "\<epsilon>>0" "\<epsilon>\<le>r" "\<epsilon><e'" using \<open>r>0\<close> \<open>e'>0\<close> unfolding \<epsilon>_def by auto
   have "(f has_contour_integral c * (residue f z)) (circlepath z \<epsilon>)"
     using e'_def[rule_format,OF \<open>\<epsilon>>0\<close> \<open>\<epsilon><e'\<close>] .
@@ -2341,8 +2341,8 @@
   thus ?thesis using residue_const by auto
 next
   case False
-  def c'\<equiv>"2 * pi * \<i>"
-  def f'\<equiv>"(\<lambda>z. c * (f z))"
+  define c' where "c' \<equiv> 2 * pi * \<i>"
+  define f' where "f' \<equiv> (\<lambda>z. c * (f z))"
   obtain e where "e>0" and e_cball:"cball z e \<subseteq> s" using \<open>open s\<close> \<open>z\<in>s\<close>
     using open_contains_cball_eq by blast
   have "(f' has_contour_integral c' * residue f' z) (circlepath z e)"
@@ -2386,7 +2386,7 @@
   shows "residue (\<lambda>w. f w / (w - z)) z = f z"
 proof -
   define c where "c \<equiv> 2 * pi * \<i>"
-  def f'\<equiv>"\<lambda>w. f w / (w - z)"
+  define f' where "f' \<equiv> \<lambda>w. f w / (w - z)"
   obtain e where "e>0" and e_cball:"cball z e \<subseteq> s" using \<open>open s\<close> \<open>z\<in>s\<close>
     using open_contains_cball_eq by blast
   have "(f' has_contour_integral c * f z) (circlepath z e)"
@@ -2634,7 +2634,7 @@
         unfolding cp_def using contour_integral_reversepath[OF n_circ(1)] n_circ(9)
         by auto
     qed
-  def g'\<equiv>"g +++ pg +++ cp +++ (reversepath pg)"
+  define g' where "g' \<equiv> g +++ pg +++ cp +++ (reversepath pg)"
   have "contour_integral g' f = (\<Sum>p\<in>pts. winding_number g' p * contour_integral (circlepath p (h p)) f)"
     proof (rule "2.hyps"(3)[of "s-{p}" "g'",OF _ _ \<open>finite pts\<close> ])
       show "connected (s - {p} - pts)" using connected by (metis Diff_insert2)
@@ -2648,7 +2648,7 @@
         unfolding g'_def cp_def using pg(2) by simp
       show "path_image g' \<subseteq> s - {p} - pts"
         proof -
-          def s'\<equiv>"s - {p} - pts"
+          define s' where "s' \<equiv> s - {p} - pts"
           have s':"s' = s-insert p pts " unfolding s'_def by auto
           then show ?thesis using path_img pg(4) cp(4)
             unfolding g'_def
@@ -2994,7 +2994,7 @@
           "\<And>w. w \<in> ball z r \<Longrightarrow> g w \<noteq> 0"
     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>]
     by (metis assms(3) assms(5) assms(6))
-  def r'\<equiv>"r/2"
+  define r' where "r' \<equiv> r/2"
   have "cball z r' \<subseteq> ball z r" unfolding r'_def by (simp add: \<open>0 < r\<close> cball_subset_ball_iff)
   hence "cball z r' \<subseteq> s" "g holomorphic_on cball z r'"
       "(\<forall>w\<in>cball z r'. f w = (w - z) ^ n * g w \<and> g w \<noteq> 0)"
@@ -3137,7 +3137,7 @@
     using h_divide by simp
   define c where "c \<equiv> 2 * pi * \<i>"
   define der_f where "der_f \<equiv> ((deriv ^^ (n - 1)) h z / fact (n-1))"
-  def h'\<equiv>"\<lambda>u. h u / (u - z) ^ n"
+  define h' where "h' \<equiv> \<lambda>u. h u / (u - z) ^ n"
   have "(h' has_contour_integral c / fact (n - 1) * (deriv ^^ (n - 1)) h z) (circlepath z r)"
     unfolding h'_def
     proof (rule Cauchy_has_contour_integral_higher_derivative_circlepath[of z r h z "n-1",
@@ -3193,8 +3193,8 @@
         proof -
           define po where "po \<equiv> porder f p"
           define pp where "pp \<equiv> pol_poly f p"
-          def f'\<equiv>"\<lambda>w. pp w / (w - p) ^ po"
-          def ff'\<equiv>"(\<lambda>x. deriv f' x * h x / f' x)"
+          define f' where "f' \<equiv> \<lambda>w. pp w / (w - p) ^ po"
+          define ff' where "ff' \<equiv> (\<lambda>x. deriv f' x * h x / f' x)"
           have "f holomorphic_on ball p e1 - {p}"
             apply (intro holomorphic_on_subset[OF f_holo])
             using e1_avoid \<open>p\<in>poles\<close> unfolding avoid_def by auto
@@ -3301,8 +3301,8 @@
         proof -
           define zo where "zo \<equiv> zorder f p"
           define zp where "zp \<equiv> zer_poly f p"
-          def f'\<equiv>"\<lambda>w. zp w * (w - p) ^ zo"
-          def ff'\<equiv>"(\<lambda>x. deriv f' x * h x / f' x)"
+          define f' where "f' \<equiv> \<lambda>w. zp w * (w - p) ^ zo"
+          define ff' where "ff' \<equiv> (\<lambda>x. deriv f' x * h x / f' x)"
           have "f holomorphic_on ball p e1"
             proof -
               have "ball p e1 \<subseteq> s - poles"
@@ -3313,8 +3313,8 @@
             using DiffD1 mem_Collect_eq zeros_def by blast
           moreover have "\<exists>w\<in>ball p e1. f w \<noteq> 0"
             proof -
-              def p'\<equiv>"p+e1/2"
-              have "p'\<in>ball p e1" and "p'\<noteq>p" using \<open>e1>0\<close> unfolding p'_def by (auto simp add:dist_norm)
+              define p' where "p' \<equiv> p+e1/2"
+              have "p' \<in> ball p e1" and "p'\<noteq>p" using \<open>e1>0\<close> unfolding p'_def by (auto simp add:dist_norm)
               then show "\<exists>w\<in>ball p e1. f w \<noteq> 0" using e1_avoid unfolding avoid_def
                 apply (rule_tac x=p' in bexI)
                 by (auto simp add:zeros_def)
diff -r 8bc9de2278c0 -r a2522ea43216 src/HOL/Analysis/Further_Topology.thy
--- a/src/HOL/Analysis/Further_Topology.thy	Tue Feb 28 12:42:50 2017 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy	Tue Feb 28 16:26:05 2017 +0100
@@ -3131,7 +3131,7 @@
       then have "cmod (exp (\<i> * of_real (2 * pi * j / n)) - 1) < 2 * sin (pi / real n)"
         by (simp add: j field_simps)
       then have "2 * \<bar>sin((2 * pi * j / n) / 2)\<bar> < 2 * sin (pi / real n)"
-        by (simp only: dist_exp_ii_1)
+        by (simp only: dist_exp_i_1)
       then have sin_less: "sin((pi * j / n)) < sin (pi / real n)"
         by (simp add: field_simps)
       then have "w / z = 1"
@@ -3179,7 +3179,7 @@
                     (\<forall>u\<in>v. Ex (homeomorphism u T (\<lambda>z. z^n))))"
            if "z \<noteq> 0" for z::complex
   proof -
-    def d \<equiv> "min (1/2) (e/4) * norm z"
+    define d where "d \<equiv> min (1/2) (e/4) * norm z"
     have "0 < d"
       by (simp add: d_def \<open>0 < e\<close> \<open>z \<noteq> 0\<close>)
     have iff_x_eq_y: "x^n = y^n \<longleftrightarrow> x = y"
@@ -3502,7 +3502,7 @@
 lemma inessential_eq_continuous_logarithm_circle:
   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
   shows "(\<exists>a. homotopic_with (\<lambda>h. True) S (sphere 0 1) f (\<lambda>t. a)) \<longleftrightarrow>
-         (\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(ii* of_real(g x))))"
+         (\<exists>g. continuous_on S g \<and> (\<forall>x \<in> S. f x = exp(\<i> * of_real(g x))))"
   (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume L: ?lhs
@@ -3519,9 +3519,9 @@
     done
 next
   assume ?rhs
-  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))"
+  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))"
     by metis
-  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)"
+  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)"
   proof (rule nullhomotopic_through_contractible)
     show "continuous_on S (complex_of_real \<circ> g)"
       by (intro conjI contg continuous_intros)
@@ -4030,7 +4030,7 @@
   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"
     using contractible_imp_holomorphic_sqrt [OF hol1f S]
     by (metis eq_iff_diff_eq_0 non1 power2_eq_1_iff)
-  have holfg: "(\<lambda>z. f z + ii*g z) holomorphic_on S"
+  have holfg: "(\<lambda>z. f z + \<i>*g z) holomorphic_on S"
     by (intro holf holg holomorphic_intros)
   have "\<And>z. z \<in> S \<Longrightarrow> f z + \<i>*g z \<noteq> 0"
     by (metis Arccos_body_lemma eq add.commute add.inverse_unique complex_i_mult_minus power2_csqrt power2_eq_iff)
@@ -4038,13 +4038,13 @@
     using contractible_imp_holomorphic_log [OF holfg S] by metis
   show ?thesis
   proof
-    show "(\<lambda>z. -ii*h z) holomorphic_on S"
+    show "(\<lambda>z. -\<i>*h z) holomorphic_on S"
       by (intro holh holomorphic_intros)
     show "f z = cos (- \<i>*h z)" if "z \<in> S" for z
     proof -
-      have "(f z + ii*g z)*(f z - ii*g z) = 1"
+      have "(f z + \<i>*g z)*(f z - \<i>*g z) = 1"
         using that eq by (auto simp: algebra_simps power2_eq_square)
-      then have "f z - ii*g z = inverse (f z + ii*g z)"
+      then have "f z - \<i>*g z = inverse (f z + \<i>*g z)"
         using inverse_unique by force
       also have "... = exp (- h z)"
         by (simp add: exp_minus fgeq that)
@@ -4214,7 +4214,7 @@
   fixes S :: "'a::real_normed_vector set"
   shows "Borsukian S \<longleftrightarrow>
          (\<forall>f. continuous_on S f \<and> f ` S \<subseteq> sphere (0::complex) 1
-              \<longrightarrow> (\<exists>g. continuous_on S (complex_of_real \<circ> g) \<and> (\<forall>x \<in> S. f x = exp(ii * of_real(g x)))))"
+              \<longrightarrow> (\<exists>g. continuous_on S (complex_of_real \<circ> g) \<and> (\<forall>x \<in> S. f x = exp(\<i> * of_real(g x)))))"
    (is "?lhs = ?rhs")
 proof
   assume LHS: ?lhs
@@ -4236,10 +4236,10 @@
   proof (clarsimp simp: Borsukian_continuous_logarithm_circle)
     fix f :: "'a \<Rightarrow> complex"
     assume "continuous_on S f" and f01: "f ` S \<subseteq> sphere 0 1"
-    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))"
+    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))"
       by (metis RHS)
     then show "\<exists>g. continuous_on S g \<and> (\<forall>x\<in>S. f x = exp (g x))"
-      by (rule_tac x="\<lambda>x. ii* of_real(g x)" in exI) (auto simp: continuous_intros contg)
+      by (rule_tac x="\<lambda>x. \<i>* of_real(g x)" in exI) (auto simp: continuous_intros contg)
   qed
 qed
 
@@ -4503,7 +4503,7 @@
   moreover have "(g \<circ> f) ` S \<subseteq> sphere 0 1"
     using fim gim by auto
   ultimately obtain h where cont_cxh: "continuous_on S (complex_of_real \<circ> h)"
-                       and gfh: "\<And>x. x \<in> S \<Longrightarrow> (g \<circ> f) x = exp(ii * of_real(h x))"
+                       and gfh: "\<And>x. x \<in> S \<Longrightarrow> (g \<circ> f) x = exp(\<i> * of_real(h x))"
     using \<open>Borsukian S\<close> Borsukian_continuous_logarithm_circle_real  by metis
   then have conth: "continuous_on S h"
     by simp
diff -r 8bc9de2278c0 -r a2522ea43216 src/HOL/Analysis/Great_Picard.thy
--- a/src/HOL/Analysis/Great_Picard.thy	Tue Feb 28 12:42:50 2017 +0100
+++ b/src/HOL/Analysis/Great_Picard.thy	Tue Feb 28 16:26:05 2017 +0100
@@ -1146,7 +1146,7 @@
   qed
   moreover
   have "contour_integral (circlepath z0 (r/2)) (\<lambda>z. m / (z - z0) + deriv h z / h z) =
-        2 * of_real pi * ii * m + 0"
+        2 * of_real pi * \<i> * m + 0"
   proof (rule contour_integral_unique [OF has_contour_integral_add])
     show "((\<lambda>x. m / (x - z0)) has_contour_integral 2 * of_real pi * \<i> * m) (circlepath z0 (r/2))"
       by (force simp: \<open>0 < r\<close> intro: Cauchy_integral_circlepath_simple)
diff -r 8bc9de2278c0 -r a2522ea43216 src/HOL/Analysis/Homeomorphism.thy
--- a/src/HOL/Analysis/Homeomorphism.thy	Tue Feb 28 12:42:50 2017 +0100
+++ b/src/HOL/Analysis/Homeomorphism.thy	Tue Feb 28 16:26:05 2017 +0100
@@ -1330,7 +1330,7 @@
     shows "g1 x = g2 x"
 proof -
   have "U \<subseteq> T" by (rule in_components_subset [OF u_compt])
-  def G12 \<equiv> "{x \<in> U. g1 x - g2 x = 0}"
+  define G12 where "G12 \<equiv> {x \<in> U. g1 x - g2 x = 0}"
   have "connected U" by (rule in_components_connected [OF u_compt])
   have contu: "continuous_on U g1" "continuous_on U g2"
        using \<open>U \<subseteq> T\<close> continuous_on_subset g1 g2 by blast+
diff -r 8bc9de2278c0 -r a2522ea43216 src/HOL/Analysis/Inner_Product.thy
--- a/src/HOL/Analysis/Inner_Product.thy	Tue Feb 28 12:42:50 2017 +0100
+++ b/src/HOL/Analysis/Inner_Product.thy	Tue Feb 28 16:26:05 2017 +0100
@@ -298,10 +298,10 @@
 lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
   unfolding inner_complex_def by simp
 
-lemma complex_inner_ii_left [simp]: "inner \<i> x = Im x"
+lemma complex_inner_i_left [simp]: "inner \<i> x = Im x"
   unfolding inner_complex_def by simp
 
-lemma complex_inner_ii_right [simp]: "inner x \<i> = Im x"
+lemma complex_inner_i_right [simp]: "inner x \<i> = Im x"
   unfolding inner_complex_def by simp
 
 
diff -r 8bc9de2278c0 -r a2522ea43216 src/HOL/Analysis/Jordan_Curve.thy
--- a/src/HOL/Analysis/Jordan_Curve.thy	Tue Feb 28 12:42:50 2017 +0100
+++ b/src/HOL/Analysis/Jordan_Curve.thy	Tue Feb 28 16:26:05 2017 +0100
@@ -90,7 +90,7 @@
     qed
     ultimately obtain z where z: "\<And>x. x \<in> S \<inter> T \<Longrightarrow> g x - h x = z"
       using continuous_discrete_range_constant [OF conST contgh] by blast
-    obtain w where "exp(ii* of_real(h w)) = exp (ii* of_real(z + h w))"
+    obtain w where "exp(\<i> * of_real(h w)) = exp (\<i> * of_real(z + h w))"
       using disc z False
       by auto (metis diff_add_cancel g h of_real_add)
     then have [simp]: "exp (\<i>* of_real z) = 1"
diff -r 8bc9de2278c0 -r a2522ea43216 src/HOL/Analysis/Winding_Numbers.thy
--- a/src/HOL/Analysis/Winding_Numbers.thy	Tue Feb 28 12:42:50 2017 +0100
+++ b/src/HOL/Analysis/Winding_Numbers.thy	Tue Feb 28 16:26:05 2017 +0100
@@ -39,7 +39,7 @@
         assume "0 \<in> interior {z. Im z * Re b \<le> Im b * Re z}"
         then obtain e where "e>0" and e: "ball 0 e \<subseteq> {z. Im z * Re b \<le> Im b * Re z}"
           by (meson mem_interior)
-        def z \<equiv> "- sgn (Im b) * (e/3) + sgn (Re b) * (e/3) * ii"
+        define z where "z \<equiv> - sgn (Im b) * (e/3) + sgn (Re b) * (e/3) * \<i>"
         have "z \<in> ball 0 e"
           using `e>0`
           apply (simp add: z_def dist_norm)
diff -r 8bc9de2278c0 -r a2522ea43216 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Feb 28 12:42:50 2017 +0100
+++ b/src/HOL/Complex.thy	Tue Feb 28 16:26:05 2017 +0100
@@ -202,7 +202,7 @@
 
 subsection \<open>The Complex Number $i$\<close>
 
-primcorec "ii" :: complex  ("\<i>")
+primcorec imaginary_unit :: complex  ("\<i>")
   where
     "Re \<i> = 0"
   | "Im \<i> = 1"
@@ -249,13 +249,13 @@
 lemma i_even_power [simp]: "\<i> ^ (n * 2) = (-1) ^ n"
   by (metis mult.commute power2_i power_mult)
 
-lemma Re_ii_times [simp]: "Re (\<i> * z) = - Im z"
+lemma Re_i_times [simp]: "Re (\<i> * z) = - Im z"
   by simp
 
-lemma Im_ii_times [simp]: "Im (\<i> * z) = Re z"
+lemma Im_i_times [simp]: "Im (\<i> * z) = Re z"
   by simp
 
-lemma ii_times_eq_iff: "\<i> * w = z \<longleftrightarrow> w = - (\<i> * z)"
+lemma i_times_eq_iff: "\<i> * w = z \<longleftrightarrow> w = - (\<i> * z)"
   by auto
 
 lemma divide_numeral_i [simp]: "z / (numeral n * \<i>) = - (\<i> * z) / numeral n"
diff -r 8bc9de2278c0 -r a2522ea43216 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Tue Feb 28 12:42:50 2017 +0100
+++ b/src/HOL/Number_Theory/Residues.thy	Tue Feb 28 16:26:05 2017 +0100
@@ -37,37 +37,34 @@
 begin
 
 lemma abelian_group: "abelian_group R"
-  apply (insert m_gt_one)
-  apply (rule abelian_groupI)
-  apply (unfold R_def residue_ring_def)
-  apply (auto simp add: mod_add_right_eq ac_simps)
-  apply (case_tac "x = 0")
-  apply force
-  apply (subgoal_tac "(x + (m - x)) mod m = 0")
-  apply (erule bexI)
-  apply auto
-  done
+proof -
+  have "\<exists>y\<in>{0..m - 1}. (x + y) mod m = 0" if "0 \<le> x" "x < m" for x
+  proof (cases "x = 0")
+    case True
+    with m_gt_one show ?thesis by simp
+  next
+    case False
+    then have "(x + (m - x)) mod m = 0"
+      by simp
+    with m_gt_one that show ?thesis
+      by (metis False atLeastAtMost_iff diff_ge_0_iff_ge diff_left_mono int_one_le_iff_zero_less less_le)
+  qed
+  with m_gt_one show ?thesis
+    by (fastforce simp add: R_def residue_ring_def mod_add_right_eq ac_simps  intro!: abelian_groupI)
+qed    
 
 lemma comm_monoid: "comm_monoid R"
-  apply (insert m_gt_one)
-  apply (unfold R_def residue_ring_def)
+  unfolding R_def residue_ring_def
   apply (rule comm_monoidI)
-  apply auto
-  apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m")
-  apply (erule ssubst)
-  apply (subst mod_mult_right_eq)+
-  apply (simp_all only: ac_simps)
+    using m_gt_one  apply auto
+  apply (metis mod_mult_right_eq mult.assoc mult.commute)
+  apply (metis mult.commute)
   done
 
 lemma cring: "cring R"
-  apply (rule cringI)
-  apply (rule abelian_group)
-  apply (rule comm_monoid)
-  apply (unfold R_def residue_ring_def, auto)
-  apply (subst mod_add_eq)
-  apply (subst mult.commute)
-  apply (subst mod_mult_right_eq)
-  apply (simp add: field_simps)
+  apply (intro cringI abelian_group comm_monoid)
+  unfolding R_def residue_ring_def
+  apply (auto simp add: comm_semiring_class.distrib mod_add_eq mod_mult_left_eq)
   done
 
 end
@@ -100,8 +97,8 @@
   unfolding R_def residue_ring_def units_of_def by auto
 
 lemma res_units_eq: "Units R = {x. 0 < x \<and> x < m \<and> coprime x m}"
-  apply (insert m_gt_one)
-  apply (unfold Units_def R_def residue_ring_def)
+  using m_gt_one
+  unfolding Units_def R_def residue_ring_def
   apply auto
   apply (subgoal_tac "x \<noteq> 0")
   apply auto
@@ -111,18 +108,12 @@
   done
 
 lemma res_neg_eq: "\<ominus> x = (- x) mod m"
-  apply (insert m_gt_one)
-  apply (unfold R_def a_inv_def m_inv_def residue_ring_def)
-  apply auto
+  using m_gt_one unfolding R_def a_inv_def m_inv_def residue_ring_def
+  apply simp
   apply (rule the_equality)
-  apply auto
-  apply (subst mod_add_right_eq)
-  apply auto
-  apply (subst mod_add_left_eq)
-  apply auto
-  apply (subgoal_tac "y mod m = - x mod m")
-  apply simp
-  apply (metis minus_add_cancel mod_mult_self1 mult.commute)
+  apply (simp add: mod_add_right_eq)
+  apply (simp add: add.commute mod_add_right_eq)
+  apply (metis add.right_neutral minus_add_cancel mod_add_right_eq mod_pos_pos_trivial)
   done
 
 lemma finite [iff]: "finite (carrier R)"
@@ -157,7 +148,7 @@
 
 (* FIXME revise algebra library to use 1? *)
 lemma pow_cong: "(x mod m) (^) n = x^n mod m"
-  apply (insert m_gt_one)
+  using m_gt_one
   apply (induct n)
   apply (auto simp add: nat_pow_def one_cong)
   apply (metis mult.commute mult_cong)
@@ -213,7 +204,7 @@
   defines "R \<equiv> residue_ring (int p)"
 
 sublocale residues_prime < residues p
-  apply (unfold R_def residues_def)
+  unfolding R_def residues_def
   using p_prime apply auto
   apply (metis (full_types) of_nat_1 of_nat_less_iff prime_gt_1_nat)
   done
@@ -222,18 +213,14 @@
 begin
 
 lemma is_field: "field R"
-  apply (rule cring.field_intro2)
-  apply (rule cring)
+proof -
+  have "\<And>x. \<lbrakk>gcd x (int p) \<noteq> 1; 0 \<le> x; x < int p\<rbrakk> \<Longrightarrow> x = 0"
+    by (metis dual_order.order_iff_strict gcd.commute less_le_not_le p_prime prime_imp_coprime prime_nat_int_transfer zdvd_imp_le)
+  then show ?thesis
+  apply (intro cring.field_intro2 cring)
   apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq)
-  apply (rule classical)
-  apply (erule notE)
-  apply (subst gcd.commute)
-  apply (rule prime_imp_coprime_int)
-  apply (simp add: p_prime)
-  apply (rule notI)
-  apply (frule zdvd_imp_le)
-  apply auto
-  done
+    done
+qed
 
 lemma res_prime_units_eq: "Units R = {1..p - 1}"
   apply (subst res_units_eq)
@@ -252,20 +239,22 @@
 
 subsection \<open>Euler's theorem\<close>
 
-text \<open>The definition of the phi function.\<close>
+text \<open>The definition of the totient function.\<close>
 
 definition phi :: "int \<Rightarrow> nat"
-  where "phi m = card {x. 0 < x \<and> x < m \<and> gcd x m = 1}"
+  where "phi m = card {x. 0 < x \<and> x < m \<and> coprime x m}"
 
-lemma phi_def_nat: "phi m = card {x. 0 < x \<and> x < nat m \<and> gcd x (nat m) = 1}"
-  apply (simp add: phi_def)
-  apply (rule bij_betw_same_card [of nat])
-  apply (auto simp add: inj_on_def bij_betw_def image_def)
-  apply (metis dual_order.irrefl dual_order.strict_trans leI nat_1 transfer_nat_int_gcd(1))
-  apply (metis One_nat_def of_nat_0 of_nat_1 of_nat_less_0_iff int_nat_eq nat_int
-    transfer_int_nat_gcd(1) of_nat_less_iff)
-  done
-
+lemma phi_def_nat: "phi m = card {x. 0 < x \<and> x < nat m \<and> coprime x (nat m)}"
+  unfolding phi_def
+proof (rule bij_betw_same_card [of nat])
+  show "bij_betw nat {x. 0 < x \<and> x < m \<and> coprime x m} {x. 0 < x \<and> x < nat m \<and> coprime x (nat m)}"
+    apply (auto simp add: inj_on_def bij_betw_def image_def)
+     apply (metis dual_order.irrefl dual_order.strict_trans leI nat_1 transfer_nat_int_gcd(1))
+    apply (metis One_nat_def of_nat_0 of_nat_1 of_nat_less_0_iff int_nat_eq nat_int
+        transfer_int_nat_gcd(1) of_nat_less_iff)
+    done
+qed
+  
 lemma prime_phi:
   assumes "2 \<le> p" "phi p = p - 1"
   shows "prime p"
@@ -292,12 +281,7 @@
 qed
 
 lemma phi_zero [simp]: "phi 0 = 0"
-  unfolding phi_def
-(* Auto hangs here. Once again, where is the simplification rule
-   1 \<equiv> Suc 0 coming from? *)
-  apply (auto simp add: card_eq_0_iff)
-(* Add card_eq_0_iff as a simp rule? delete card_empty_imp? *)
-  done
+  unfolding phi_def by (auto simp add: card_eq_0_iff)
 
 lemma phi_one [simp]: "phi 1 = 0"
   by (auto simp add: phi_def card_eq_0_iff)
@@ -309,30 +293,12 @@
   assumes a: "gcd a m = 1"
   shows "[a^phi m = 1] (mod m)"
 proof -
-  from a m_gt_one have [simp]: "a mod m \<in> Units R"
-    by (intro mod_in_res_units)
-  from phi_eq have "(a mod m) (^) (phi m) = (a mod m) (^) (card (Units R))"
-    by simp
-  also have "\<dots> = \<one>"
-    by (intro units_power_order_eq_one) auto
-  finally show ?thesis
-    by (simp add: res_to_cong_simps)
+  have "a ^ phi m mod m = 1 mod m"
+    by (metis assms finite_Units m_gt_one mod_in_res_units one_cong phi_eq pow_cong units_power_order_eq_one)
+  then show ?thesis
+    using res_eq_to_cong by blast
 qed
 
-(* In fact, there is a two line proof!
-
-lemma (in residues) euler_theorem1:
-  assumes a: "gcd a m = 1"
-  shows "[a^phi m = 1] (mod m)"
-proof -
-  have "(a mod m) (^) (phi m) = \<one>"
-    by (simp add: phi_eq units_power_order_eq_one a m_gt_one)
-  then show ?thesis
-    by (simp add: res_to_cong_simps)
-qed
-
-*)
-
 text \<open>Outside the locale, we can relax the restriction \<open>m > 1\<close>.\<close>
 lemma euler_theorem:
   assumes "m \<ge> 0"
@@ -348,16 +314,10 @@
 qed
 
 lemma (in residues_prime) phi_prime: "phi p = nat p - 1"
-  apply (subst phi_eq)
-  apply (subst res_prime_units_eq)
-  apply auto
-  done
+  by (simp add: residues.phi_eq residues_axioms residues_prime.res_prime_units_eq residues_prime_axioms)
 
 lemma phi_prime: "prime (int p) \<Longrightarrow> phi p = nat p - 1"
-  apply (rule residues_prime.phi_prime)
-  apply simp
-  apply (erule residues_prime.intro)
-  done
+  by (simp add: residues_prime.intro residues_prime.phi_prime)
 
 lemma fermat_theorem:
   fixes a :: int
@@ -424,18 +384,12 @@
   finally have "(\<Otimes>i\<in>Units R. i) = \<ominus> \<one>"
     by simp
   also have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>Units R. i mod p)"
-    apply (rule finprod_cong')
-    apply auto
-    apply (subst (asm) res_prime_units_eq)
-    apply auto
-    done
+    by (rule finprod_cong') (auto simp: res_units_eq)
   also have "\<dots> = (\<Prod>i\<in>Units R. i) mod p"
-    apply (rule prod_cong)
-    apply auto
-    done
+    by (rule prod_cong) auto
   also have "\<dots> = fact (p - 1) mod p"
     apply (simp add: fact_prod)
-    apply (insert assms)
+    using assms
     apply (subst res_prime_units_eq)
     apply (simp add: int_prod zmod_int prod_int_eq)
     done
diff -r 8bc9de2278c0 -r a2522ea43216 src/HOL/Probability/Characteristic_Functions.thy
--- a/src/HOL/Probability/Characteristic_Functions.thy	Tue Feb 28 12:42:50 2017 +0100
+++ b/src/HOL/Probability/Characteristic_Functions.thy	Tue Feb 28 16:26:05 2017 +0100
@@ -69,7 +69,7 @@
   from f have "\<And>x. of_real (Re (f x)) = f x"
     by (simp add: complex_eq_iff)
   then show "AE x in M. cmod (exp (\<i> * f x)) \<le> 1"
-    using norm_exp_ii_times[of "Re (f x)" for x] by simp
+    using norm_exp_i_times[of "Re (f x)" for x] by simp
 qed (insert f, simp)
 
 lemma (in real_distribution) cmod_char_le_1: "norm (char M t) \<le> 1"
diff -r 8bc9de2278c0 -r a2522ea43216 src/HOL/Probability/Levy.thy
--- a/src/HOL/Probability/Levy.thy	Tue Feb 28 12:42:50 2017 +0100
+++ b/src/HOL/Probability/Levy.thy	Tue Feb 28 16:26:05 2017 +0100
@@ -60,7 +60,7 @@
   have "?F = cmod (iexp (t * a) * (iexp (t * (b - a)) - 1) / (\<i> * t))"
     using \<open>t \<noteq> 0\<close> by (intro arg_cong[where f=norm]) (simp add: field_simps exp_diff exp_minus)
   also have "\<dots> = cmod (iexp (t * (b - a)) - 1) / abs t"
-    unfolding norm_divide norm_mult norm_exp_ii_times using \<open>t \<noteq> 0\<close>
+    unfolding norm_divide norm_mult norm_exp_i_times using \<open>t \<noteq> 0\<close>
     by (simp add: complex_eq_iff norm_mult)
   also have "\<dots> \<le> abs (t * (b - a)) / abs t"
     using iexp_approx1 [of "t * (b - a)" 0]