--- 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.
--- 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)
--- 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)
--- 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
--- 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)
--- 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+
--- 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
--- 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"
--- 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)
--- 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"
--- 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
--- 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"
--- 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]