Renamed ii to imaginary_unit in order to free up ii as a variable name. Also replaced some legacy def commands
--- a/NEWS Tue Feb 28 08:18:12 2017 +0100
+++ b/NEWS Tue Feb 28 13:51:47 2017 +0000
@@ -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.
--- a/src/HOL/Analysis/Complex_Transcendental.thy Tue Feb 28 08:18:12 2017 +0100
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Tue Feb 28 13:51:47 2017 +0000
@@ -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)
--- a/src/HOL/Analysis/Conformal_Mappings.thy Tue Feb 28 08:18:12 2017 +0100
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Tue Feb 28 13:51:47 2017 +0000
@@ -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)
--- a/src/HOL/Analysis/Further_Topology.thy Tue Feb 28 08:18:12 2017 +0100
+++ b/src/HOL/Analysis/Further_Topology.thy Tue Feb 28 13:51:47 2017 +0000
@@ -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
--- a/src/HOL/Analysis/Great_Picard.thy Tue Feb 28 08:18:12 2017 +0100
+++ b/src/HOL/Analysis/Great_Picard.thy Tue Feb 28 13:51:47 2017 +0000
@@ -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)
--- a/src/HOL/Analysis/Homeomorphism.thy Tue Feb 28 08:18:12 2017 +0100
+++ b/src/HOL/Analysis/Homeomorphism.thy Tue Feb 28 13:51:47 2017 +0000
@@ -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+
--- a/src/HOL/Analysis/Inner_Product.thy Tue Feb 28 08:18:12 2017 +0100
+++ b/src/HOL/Analysis/Inner_Product.thy Tue Feb 28 13:51:47 2017 +0000
@@ -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
--- a/src/HOL/Analysis/Jordan_Curve.thy Tue Feb 28 08:18:12 2017 +0100
+++ b/src/HOL/Analysis/Jordan_Curve.thy Tue Feb 28 13:51:47 2017 +0000
@@ -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"
--- a/src/HOL/Analysis/Winding_Numbers.thy Tue Feb 28 08:18:12 2017 +0100
+++ b/src/HOL/Analysis/Winding_Numbers.thy Tue Feb 28 13:51:47 2017 +0000
@@ -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)
--- a/src/HOL/Complex.thy Tue Feb 28 08:18:12 2017 +0100
+++ b/src/HOL/Complex.thy Tue Feb 28 13:51:47 2017 +0000
@@ -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"
--- a/src/HOL/Probability/Characteristic_Functions.thy Tue Feb 28 08:18:12 2017 +0100
+++ b/src/HOL/Probability/Characteristic_Functions.thy Tue Feb 28 13:51:47 2017 +0000
@@ -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"
--- a/src/HOL/Probability/Levy.thy Tue Feb 28 08:18:12 2017 +0100
+++ b/src/HOL/Probability/Levy.thy Tue Feb 28 13:51:47 2017 +0000
@@ -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]