# HG changeset patch # User wenzelm # Date 1470166230 -7200 # Node ID 58aab4745e85d9e1105bf3424ef8853bef43c8fe # Parent d0e2bad67bd467ca67929d7f5170f9478e091d20 more symbols; diff -r d0e2bad67bd4 -r 58aab4745e85 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Tue Aug 02 21:05:34 2016 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Tue Aug 02 21:30:30 2016 +0200 @@ -4457,7 +4457,7 @@ text \Connection to E c over the complex numbers --- Euler and de Moivre.\ -lemma Eii_sin_cos: "E (ii * c) = fps_cos c + fps_const ii * fps_sin c" +lemma Eii_sin_cos: "E (\ * c) = fps_cos c + fps_const \ * fps_sin c" (is "?l = ?r") proof - have "?l $ n = ?r $ n" for n @@ -4477,7 +4477,7 @@ by (simp add: fps_eq_iff) qed -lemma E_minus_ii_sin_cos: "E (- (ii * c)) = fps_cos c - fps_const ii * fps_sin c" +lemma E_minus_ii_sin_cos: "E (- (\ * c)) = fps_cos c - fps_const \ * fps_sin c" unfolding minus_mult_right Eii_sin_cos by (simp add: fps_sin_even fps_cos_odd) lemma fps_const_minus: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)" @@ -4490,7 +4490,7 @@ lemma fps_numeral_fps_const: "numeral i = fps_const (numeral i :: 'a::comm_ring_1)" by (fact numeral_fps_const) (* FIXME: duplicate *) -lemma fps_cos_Eii: "fps_cos c = (E (ii * c) + E (- ii * c)) / fps_const 2" +lemma fps_cos_Eii: "fps_cos c = (E (\ * c) + E (- \ * c)) / fps_const 2" proof - have th: "fps_cos c + fps_cos c = fps_cos c * fps_const 2" by (simp add: numeral_fps_const) @@ -4499,9 +4499,9 @@ by (simp add: fps_sin_even fps_cos_odd numeral_fps_const fps_divide_unit fps_const_inverse th) qed -lemma fps_sin_Eii: "fps_sin c = (E (ii * c) - E (- ii * c)) / fps_const (2*ii)" +lemma fps_sin_Eii: "fps_sin c = (E (\ * c) - E (- \ * c)) / fps_const (2*\)" proof - - have th: "fps_const \ * fps_sin c + fps_const \ * fps_sin c = fps_sin c * fps_const (2 * ii)" + have th: "fps_const \ * fps_sin c + fps_const \ * fps_sin c = fps_sin c * fps_const (2 * \)" by (simp add: fps_eq_iff numeral_fps_const) show ?thesis unfolding Eii_sin_cos minus_mult_commute @@ -4509,15 +4509,15 @@ qed lemma fps_tan_Eii: - "fps_tan c = (E (ii * c) - E (- ii * c)) / (fps_const ii * (E (ii * c) + E (- ii * c)))" + "fps_tan c = (E (\ * c) - E (- \ * c)) / (fps_const \ * (E (\ * c) + E (- \ * c)))" unfolding fps_tan_def fps_sin_Eii fps_cos_Eii mult_minus_left E_neg apply (simp add: fps_divide_unit fps_inverse_mult fps_const_mult[symmetric] fps_const_inverse del: fps_const_mult) apply simp done lemma fps_demoivre: - "(fps_cos a + fps_const ii * fps_sin a)^n = - fps_cos (of_nat n * a) + fps_const ii * fps_sin (of_nat n * a)" + "(fps_cos a + fps_const \ * fps_sin a)^n = + fps_cos (of_nat n * a) + fps_const \ * fps_sin (of_nat n * a)" unfolding Eii_sin_cos[symmetric] E_power_mult by (simp add: ac_simps) diff -r d0e2bad67bd4 -r 58aab4745e85 src/HOL/Library/Fundamental_Theorem_Algebra.thy --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Aug 02 21:05:34 2016 +0200 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue Aug 02 21:30:30 2016 +0200 @@ -126,13 +126,13 @@ lemma unimodular_reduce_norm: assumes md: "cmod z = 1" - shows "cmod (z + 1) < 1 \ cmod (z - 1) < 1 \ cmod (z + ii) < 1 \ cmod (z - ii) < 1" + shows "cmod (z + 1) < 1 \ cmod (z - 1) < 1 \ cmod (z + \) < 1 \ cmod (z - \) < 1" proof - obtain x y where z: "z = Complex x y " by (cases z) auto from md z have xy: "x\<^sup>2 + y\<^sup>2 = 1" by (simp add: cmod_def) - have False if "cmod (z + 1) \ 1" "cmod (z - 1) \ 1" "cmod (z + ii) \ 1" "cmod (z - ii) \ 1" + have False if "cmod (z + 1) \ 1" "cmod (z - 1) \ 1" "cmod (z + \) \ 1" "cmod (z - \) \ 1" proof - from that z xy have "2 * x \ 1" "2 * x \ -1" "2 * y \ 1" "2 * y \ -1" by (simp_all add: cmod_def power2_eq_square algebra_simps) @@ -190,17 +190,17 @@ apply (cases "cmod (complex_of_real (cmod b) / b - 1) < 1") apply (rule_tac x="-1" in exI) apply simp - apply (cases "cmod (complex_of_real (cmod b) / b + ii) < 1") + apply (cases "cmod (complex_of_real (cmod b) / b + \) < 1") apply (cases "even m") - apply (rule_tac x="ii" in exI) + apply (rule_tac x="\" in exI) apply (simp add: m power_mult) - apply (rule_tac x="- ii" in exI) + apply (rule_tac x="- \" in exI) apply (simp add: m power_mult) apply (cases "even m") - apply (rule_tac x="- ii" in exI) + apply (rule_tac x="- \" in exI) apply (simp add: m power_mult) apply (auto simp add: m power_mult) - apply (rule_tac x="ii" in exI) + apply (rule_tac x="\" in exI) apply (auto simp add: m power_mult) done then obtain v where v: "cmod (complex_of_real (cmod b) / b + v^n) < 1" diff -r d0e2bad67bd4 -r 58aab4745e85 src/HOL/Library/Inner_Product.thy --- a/src/HOL/Library/Inner_Product.thy Tue Aug 02 21:05:34 2016 +0200 +++ b/src/HOL/Library/Inner_Product.thy Tue Aug 02 21:30:30 2016 +0200 @@ -293,10 +293,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 ii x = Im x" +lemma complex_inner_ii_left [simp]: "inner \ x = Im x" unfolding inner_complex_def by simp -lemma complex_inner_ii_right [simp]: "inner x ii = Im x" +lemma complex_inner_ii_right [simp]: "inner x \ = Im x" unfolding inner_complex_def by simp diff -r d0e2bad67bd4 -r 58aab4745e85 src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy --- a/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Tue Aug 02 21:05:34 2016 +0200 +++ b/src/HOL/Multivariate_Analysis/Cauchy_Integral_Thm.thy Tue Aug 02 21:30:30 2016 +0200 @@ -3453,7 +3453,7 @@ pathstart p = pathstart \ \ pathfinish p = pathfinish \ \ (\t \ {0..1}. norm(\ t - p t) < e) \ - contour_integral p (\w. 1/(w - z)) = 2 * pi * ii * n" + contour_integral p (\w. 1/(w - z)) = 2 * pi * \ * n" lemma winding_number: assumes "path \" "z \ path_image \" "0 < e" @@ -3461,7 +3461,7 @@ pathstart p = pathstart \ \ pathfinish p = pathfinish \ \ (\t \ {0..1}. norm (\ t - p t) < e) \ - contour_integral p (\w. 1/(w - z)) = 2 * pi * ii * winding_number \ z" + contour_integral p (\w. 1/(w - z)) = 2 * pi * \ * winding_number \ z" proof - have "path_image \ \ UNIV - {z}" using assms by blast @@ -3476,11 +3476,11 @@ then obtain h where h: "polynomial_function h \ pathstart h = pathstart \ \ pathfinish h = pathfinish \ \ (\t \ {0..1}. norm(h t - \ t) < d/2)" using path_approx_polynomial_function [OF \path \\, of "d/2"] d by auto - define nn where "nn = 1/(2* pi*ii) * contour_integral h (\w. 1/(w - z))" + define nn where "nn = 1/(2* pi*\) * contour_integral h (\w. 1/(w - z))" have "\n. \e > 0. \p. valid_path p \ z \ path_image p \ pathstart p = pathstart \ \ pathfinish p = pathfinish \ \ (\t \ {0..1}. norm(\ t - p t) < e) \ - contour_integral p (\w. 1/(w - z)) = 2 * pi * ii * n" + contour_integral p (\w. 1/(w - z)) = 2 * pi * \ * n" (is "\n. \e > 0. ?PP e n") proof (rule_tac x=nn in exI, clarify) fix e::real @@ -3509,7 +3509,7 @@ "\e. e>0 \ \p. valid_path p \ z \ path_image p \ pathstart p = pathstart \ \ pathfinish p = pathfinish \ \ (\t \ {0..1}. norm (\ t - p t) < e) \ - contour_integral p (\w. 1/(w - z)) = 2 * pi * ii * n" + contour_integral p (\w. 1/(w - z)) = 2 * pi * \ * n" shows "winding_number \ z = n" proof - have "path_image \ \ UNIV - {z}" @@ -3525,7 +3525,7 @@ "valid_path p \ z \ path_image p \ pathstart p = pathstart \ \ pathfinish p = pathfinish \ \ (\t \ {0..1}. norm (\ t - p t) < e) \ - contour_integral p (\w. 1/(w - z)) = 2 * pi * ii * n" + contour_integral p (\w. 1/(w - z)) = 2 * pi * \ * n" using pi [OF e] by blast obtain q where q: "valid_path q \ z \ path_image q \ @@ -3552,7 +3552,7 @@ "\e. e>0 \ \p. valid_path p \ z \ path_image p \ pathfinish p = pathstart p \ (\t \ {0..1}. norm (\ t - p t) < e) \ - contour_integral p (\w. 1/(w - z)) = 2 * pi * ii * n" + contour_integral p (\w. 1/(w - z)) = 2 * pi * \ * n" shows "winding_number \ z = n" proof - have "path_image \ \ UNIV - {z}" @@ -3568,7 +3568,7 @@ "valid_path p \ z \ path_image p \ pathfinish p = pathstart p \ (\t \ {0..1}. norm (\ t - p t) < e) \ - contour_integral p (\w. 1/(w - z)) = 2 * pi * ii * n" + contour_integral p (\w. 1/(w - z)) = 2 * pi * \ * n" using pi [OF e] by blast obtain q where q: "valid_path q \ z \ path_image q \ @@ -3590,12 +3590,12 @@ lemma winding_number_valid_path: assumes "valid_path \" "z \ path_image \" - shows "winding_number \ z = 1/(2*pi*ii) * contour_integral \ (\w. 1/(w - z))" + shows "winding_number \ z = 1/(2*pi*\) * contour_integral \ (\w. 1/(w - z))" using assms by (auto simp: valid_path_imp_path intro!: winding_number_unique) lemma has_contour_integral_winding_number: assumes \: "valid_path \" "z \ path_image \" - shows "((\w. 1/(w - z)) has_contour_integral (2*pi*ii*winding_number \ z)) \" + shows "((\w. 1/(w - z)) has_contour_integral (2*pi*\*winding_number \ z)) \" by (simp add: winding_number_valid_path has_contour_integral_integral contour_integrable_inversediff assms) lemma winding_number_trivial [simp]: "z \ a \ winding_number(linepath a a) z = 0" @@ -3697,7 +3697,7 @@ show ?thesis apply (simp add: Re_winding_number [OF \] field_simps) apply (rule has_integral_component_nonneg - [of ii "\x. if x \ {0<..<1} + [of \ "\x. if x \ {0<..<1} then 1/(\ x - z) * vector_derivative \ (at x) else 0", simplified]) prefer 3 apply (force simp: *) apply (simp add: Basis_complex_def) @@ -3718,8 +3718,8 @@ proof - have "e \ Im (contour_integral \ (\w. 1 / (w - z)))" apply (rule has_integral_component_le - [of ii "\x. ii*e" "ii*e" "{0..1}" - "\x. if x \ {0<..<1} then 1/(\ x - z) * vector_derivative \ (at x) else ii*e" + [of \ "\x. \*e" "\*e" "{0..1}" + "\x. if x \ {0<..<1} then 1/(\ x - z) * vector_derivative \ (at x) else \*e" "contour_integral \ (\w. 1/(w - z))", simplified]) using e apply (simp_all add: Basis_complex_def) @@ -3874,7 +3874,7 @@ corollary winding_number_exp_2pi: "\path p; z \ path_image p\ - \ pathfinish p - z = exp (2 * pi * ii * winding_number p z) * (pathstart p - z)" + \ pathfinish p - z = exp (2 * pi * \ * winding_number p z) * (pathstart p - z)" using winding_number [of p z 1] unfolding valid_path_def path_image_def pathstart_def pathfinish_def by (force dest: winding_number_exp_integral(2) [of _ 0 1 z] simp: field_simps contour_integral_integral exp_minus) @@ -4330,7 +4330,7 @@ if x: "0 \ x" "x \ 1" for x proof - have "integral {0..x} (\t. vector_derivative \ (at t) / (\ t - z)) / (2 * of_real pi * \) = - 1 / (2*pi*ii) * contour_integral (subpath 0 x \) (\w. 1/(w - z))" + 1 / (2*pi*\) * contour_integral (subpath 0 x \) (\w. 1/(w - z))" using assms x apply (simp add: contour_integral_subcontour_integral [OF contour_integrable_inversediff]) done @@ -4343,7 +4343,7 @@ qed show ?thesis apply (rule continuous_on_eq - [where f = "\x. 1 / (2*pi*ii) * + [where f = "\x. 1 / (2*pi*\) * integral {0..x} (\t. 1/(\ t - z) * vector_derivative \ (at t))"]) apply (rule continuous_intros)+ apply (rule indefinite_integral_continuous) @@ -4491,7 +4491,7 @@ and fcd: "(\x. x \ interior s - k \ f field_differentiable at x)" and z: "z \ interior s - k" and vpg: "valid_path \" and pasz: "path_image \ \ s - {z}" and loop: "pathfinish \ = pathstart \" - shows "((\w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \ z * f z)) \" + shows "((\w. f w / (w - z)) has_contour_integral (2*pi * \ * winding_number \ z * f z)) \" proof - obtain f' where f': "(f has_field_derivative f') (at z)" using fcd [OF z] by (auto simp: field_differentiable_def) @@ -4536,7 +4536,7 @@ theorem Cauchy_integral_formula_convex_simple: "\convex s; f holomorphic_on s; z \ interior s; valid_path \; path_image \ \ s - {z}; pathfinish \ = pathstart \\ - \ ((\w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \ z * f z)) \" + \ ((\w. f w / (w - z)) has_contour_integral (2*pi * \ * winding_number \ z * f z)) \" apply (rule Cauchy_integral_formula_weak [where k = "{}"]) using holomorphic_on_imp_continuous_on by auto (metis at_within_interior holomorphic_on_def interiorE subsetCE) @@ -4856,19 +4856,19 @@ subsection\Partial circle path\ definition part_circlepath :: "[complex, real, real, real, real] \ complex" - where "part_circlepath z r s t \ \x. z + of_real r * exp (ii * of_real (linepath s t x))" + where "part_circlepath z r s t \ \x. z + of_real r * exp (\ * of_real (linepath s t x))" lemma pathstart_part_circlepath [simp]: - "pathstart(part_circlepath z r s t) = z + r*exp(ii * s)" + "pathstart(part_circlepath z r s t) = z + r*exp(\ * s)" by (metis part_circlepath_def pathstart_def pathstart_linepath) lemma pathfinish_part_circlepath [simp]: - "pathfinish(part_circlepath z r s t) = z + r*exp(ii*t)" + "pathfinish(part_circlepath z r s t) = z + r*exp(\*t)" by (metis part_circlepath_def pathfinish_def pathfinish_linepath) proposition has_vector_derivative_part_circlepath [derivative_intros]: "((part_circlepath z r s t) has_vector_derivative - (ii * r * (of_real t - of_real s) * exp(ii * linepath s t x))) + (\ * r * (of_real t - of_real s) * exp(\ * linepath s t x))) (at x within X)" apply (simp add: part_circlepath_def linepath_def scaleR_conv_of_real) apply (rule has_vector_derivative_real_complex) @@ -4877,13 +4877,13 @@ corollary vector_derivative_part_circlepath: "vector_derivative (part_circlepath z r s t) (at x) = - ii * r * (of_real t - of_real s) * exp(ii * linepath s t x)" + \ * r * (of_real t - of_real s) * exp(\ * linepath s t x)" using has_vector_derivative_part_circlepath vector_derivative_at by blast corollary vector_derivative_part_circlepath01: "\0 \ x; x \ 1\ \ vector_derivative (part_circlepath z r s t) (at x within {0..1}) = - ii * r * (of_real t - of_real s) * exp(ii * linepath s t x)" + \ * r * (of_real t - of_real s) * exp(\ * linepath s t x)" using has_vector_derivative_part_circlepath by (auto simp: vector_derivative_at_within_ivl) @@ -4899,7 +4899,7 @@ proposition path_image_part_circlepath: assumes "s \ t" - shows "path_image (part_circlepath z r s t) = {z + r * exp(ii * of_real x) | x. s \ x \ x \ t}" + shows "path_image (part_circlepath z r s t) = {z + r * exp(\ * of_real x) | x. s \ x \ x \ t}" proof - { fix z::real assume "0 \ z" "z \ 1" @@ -4986,7 +4986,7 @@ by (metis "2" abs_of_pos diff_gt_0_iff_gt norm_of_real of_real_diff) have "finite (part_circlepath z r s t -` {y} \ {0..1})" if "y \ k" for y proof - - define w where "w = (y - z)/of_real r / exp(ii * of_real s)" + define w where "w = (y - z)/of_real r / exp(\ * of_real s)" have fin: "finite (of_real -` {z. cmod z \ 1 \ exp (\ * complex_of_real (t - s) * z) = w})" apply (rule finite_vimageI [OF finite_bounded_log2]) using \s < t\ apply (auto simp: inj_of_real) @@ -5063,7 +5063,7 @@ done next case False then have "r \ 0" "s \ t" by auto - have *: "\x y z s t. ii*((1 - x) * s + x * t) = ii*(((1 - y) * s + y * t)) + z \ ii*(x - y) * (t - s) = z" + have *: "\x y z s t. \*((1 - x) * s + x * t) = \*(((1 - y) * s + y * t)) + z \ \*(x - y) * (t - s) = z" by (simp add: algebra_simps) have abs01: "\x y::real. 0 \ x \ x \ 1 \ 0 \ y \ y \ 1 \ (x = y \ x = 0 \ y = 1 \ x = 1 \ y = 0 \ \x - y\ \ {0,1})" @@ -5134,7 +5134,7 @@ definition circlepath :: "[complex, real, real] \ complex" where "circlepath z r \ part_circlepath z r 0 (2*pi)" -lemma circlepath: "circlepath z r = (\x. z + r * exp(2 * of_real pi * ii * of_real x))" +lemma circlepath: "circlepath z r = (\x. z + r * exp(2 * of_real pi * \ * of_real x))" by (simp add: circlepath_def part_circlepath_def linepath_def algebra_simps) lemma pathstart_circlepath [simp]: "pathstart (circlepath z r) = z + r" @@ -5173,7 +5173,7 @@ using path_image_circlepath_minus_subset by fastforce proposition has_vector_derivative_circlepath [derivative_intros]: - "((circlepath z r) has_vector_derivative (2 * pi * ii * r * exp (2 * of_real pi * ii * of_real x))) + "((circlepath z r) has_vector_derivative (2 * pi * \ * r * exp (2 * of_real pi * \ * of_real x))) (at x within X)" apply (simp add: circlepath_def scaleR_conv_of_real) apply (rule derivative_eq_intros) @@ -5182,13 +5182,13 @@ corollary vector_derivative_circlepath: "vector_derivative (circlepath z r) (at x) = - 2 * pi * ii * r * exp(2 * of_real pi * ii * x)" + 2 * pi * \ * r * exp(2 * of_real pi * \ * x)" using has_vector_derivative_circlepath vector_derivative_at by blast corollary vector_derivative_circlepath01: "\0 \ x; x \ 1\ \ vector_derivative (circlepath z r) (at x within {0..1}) = - 2 * pi * ii * r * exp(2 * of_real pi * ii * x)" + 2 * pi * \ * r * exp(2 * of_real pi * \ * x)" using has_vector_derivative_circlepath by (auto simp: vector_derivative_at_within_ivl) @@ -5300,7 +5300,7 @@ theorem Cauchy_integral_circlepath: assumes "continuous_on (cball z r) f" "f holomorphic_on (ball z r)" "norm(w - z) < r" - shows "((\u. f u/(u - w)) has_contour_integral (2 * of_real pi * ii * f w)) + shows "((\u. f u/(u - w)) has_contour_integral (2 * of_real pi * \ * f w)) (circlepath z r)" proof - have "r > 0" @@ -5320,7 +5320,7 @@ corollary Cauchy_integral_circlepath_simple: assumes "f holomorphic_on cball z r" "norm(w - z) < r" - shows "((\u. f u/(u - w)) has_contour_integral (2 * of_real pi * ii * f w)) + shows "((\u. f u/(u - w)) has_contour_integral (2 * of_real pi * \ * f w)) (circlepath z r)" using assms by (force simp: holomorphic_on_imp_continuous_on holomorphic_on_subset Cauchy_integral_circlepath) @@ -5634,7 +5634,7 @@ and w: "w \ ball z r" shows "(\u. f u/(u - w)^2) contour_integrable_on (circlepath z r)" (is "?thes1") - and "(f has_field_derivative (1 / (2 * of_real pi * ii) * contour_integral(circlepath z r) (\u. f u / (u - w)^2))) (at w)" + and "(f has_field_derivative (1 / (2 * of_real pi * \) * contour_integral(circlepath z r) (\u. f u / (u - w)^2))) (at w)" (is "?thes2") proof - have [simp]: "r \ 0" using w @@ -5642,7 +5642,7 @@ have f: "continuous_on (path_image (circlepath z r)) f" by (rule continuous_on_subset [OF contf]) (force simp add: cball_def sphere_def) have int: "\w. dist z w < r \ - ((\u. f u / (u - w)) has_contour_integral (\x. 2 * of_real pi * ii * f x) w) (circlepath z r)" + ((\u. f u / (u - w)) has_contour_integral (\x. 2 * of_real pi * \ * f x) w) (circlepath z r)" by (rule Cauchy_integral_circlepath [OF contf holf]) (simp add: dist_norm norm_minus_commute) show ?thes1 apply (simp add: power2_eq_square) @@ -5651,7 +5651,7 @@ done have "((\x. 2 * of_real pi * \ * f x) has_field_derivative contour_integral (circlepath z r) (\u. f u / (u - w)^2)) (at w)" apply (simp add: power2_eq_square) - apply (rule Cauchy_next_derivative_circlepath [OF f _ _ w, where k=1 and g = "\x. 2 * of_real pi * ii * f x", simplified]) + apply (rule Cauchy_next_derivative_circlepath [OF f _ _ w, where k=1 and g = "\x. 2 * of_real pi * \ * f x", simplified]) apply (blast intro: int) done then have fder: "(f has_field_derivative contour_integral (circlepath z r) (\u. f u / (u - w)^2) / (2 * of_real pi * \)) (at w)" @@ -5676,7 +5676,7 @@ using field_differentiable_at_within field_differentiable_def fder by blast then have "continuous_on (path_image (circlepath z r)) f" using \r > 0\ by (force elim: holomorphic_on_subset [THEN holomorphic_on_imp_continuous_on]) - then have contfpi: "continuous_on (path_image (circlepath z r)) (\x. 1/(2 * of_real pi*ii) * f x)" + then have contfpi: "continuous_on (path_image (circlepath z r)) (\x. 1/(2 * of_real pi*\) * f x)" by (auto intro: continuous_intros)+ have contf_cball: "continuous_on (cball z r) f" using holf_cball by (simp add: holomorphic_on_imp_continuous_on holomorphic_on_subset) @@ -6079,7 +6079,7 @@ and fcd: "(\x. x \ interior s - k \ f field_differentiable at x)" and z: "z \ interior s" and vpg: "valid_path \" and pasz: "path_image \ \ s - {z}" and loop: "pathfinish \ = pathstart \" - shows "((\w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \ z * f z)) \" + shows "((\w. f w / (w - z)) has_contour_integral (2*pi * \ * winding_number \ z * f z)) \" apply (rule Cauchy_integral_formula_weak [OF s finite.emptyI contf]) apply (simp add: holomorphic_on_open [symmetric] field_differentiable_def) using no_isolated_singularity [where s = "interior s"] @@ -6096,7 +6096,7 @@ assumes contf: "continuous_on (cball z r) f" and holf: "f holomorphic_on ball z r" and w: "w \ ball z r" - shows "((\u. f u / (u - w) ^ (Suc k)) has_contour_integral ((2 * pi * ii) / (fact k) * (deriv ^^ k) f w)) + shows "((\u. f u / (u - w) ^ (Suc k)) has_contour_integral ((2 * pi * \) / (fact k) * (deriv ^^ k) f w)) (circlepath z r)" using w proof (induction k arbitrary: w) @@ -6137,7 +6137,7 @@ and w: "w \ ball z r" shows "(\u. f u / (u - w)^(Suc k)) contour_integrable_on (circlepath z r)" (is "?thes1") - and "(deriv ^^ k) f w = (fact k) / (2 * pi * ii) * contour_integral(circlepath z r) (\u. f u/(u - w)^(Suc k))" + and "(deriv ^^ k) f w = (fact k) / (2 * pi * \) * contour_integral(circlepath z r) (\u. f u/(u - w)^(Suc k))" (is "?thes2") proof - have *: "((\u. f u / (u - w) ^ Suc k) has_contour_integral (2 * pi) * \ / (fact k) * (deriv ^^ k) f w) @@ -6152,12 +6152,12 @@ corollary Cauchy_contour_integral_circlepath: assumes "continuous_on (cball z r) f" "f holomorphic_on ball z r" "w \ ball z r" - shows "contour_integral(circlepath z r) (\u. f u/(u - w)^(Suc k)) = (2 * pi * ii) * (deriv ^^ k) f w / (fact k)" + shows "contour_integral(circlepath z r) (\u. f u/(u - w)^(Suc k)) = (2 * pi * \) * (deriv ^^ k) f w / (fact k)" by (simp add: Cauchy_higher_derivative_integral_circlepath [OF assms]) corollary Cauchy_contour_integral_circlepath_2: assumes "continuous_on (cball z r) f" "f holomorphic_on ball z r" "w \ ball z r" - shows "contour_integral(circlepath z r) (\u. f u/(u - w)^2) = (2 * pi * ii) * deriv f w" + shows "contour_integral(circlepath z r) (\u. f u/(u - w)^2) = (2 * pi * \) * deriv f w" using Cauchy_contour_integral_circlepath [OF assms, of 1] by (simp add: power2_eq_square) @@ -6263,10 +6263,10 @@ apply auto done then have "(\k. contour_integral (circlepath z r) (\u. f u/(u - z)^(Suc k)) * (w - z)^k) - sums (2 * of_real pi * ii * f w)" + sums (2 * of_real pi * \ * f w)" using w by (auto simp: dist_commute dist_norm contour_integral_unique [OF Cauchy_integral_circlepath_simple [OF holfc]]) then have "(\k. contour_integral (circlepath z r) (\u. f u / (u - z) ^ Suc k) * (w - z)^k / (\ * (of_real pi * 2))) - sums ((2 * of_real pi * ii * f w) / (\ * (complex_of_real pi * 2)))" + sums ((2 * of_real pi * \ * f w) / (\ * (complex_of_real pi * 2)))" by (rule sums_divide) then have "(\n. (w - z) ^ n * contour_integral (circlepath z r) (\u. f u / (u - z) ^ Suc n) / (\ * (of_real pi * 2))) sums f w" @@ -6407,7 +6407,7 @@ by (rule contour_integral_uniform_limit_circlepath [OF ev_int ev_less F \0 < r\]) have cif_tends_cig: "((\n. contour_integral(circlepath z r) (\u. f n u / (u - w))) \ contour_integral(circlepath z r) (\u. g u/(u - w))) F" by (rule contour_integral_uniform_limit_circlepath [OF ev_int ev_less F \0 < r\]) - have f_tends_cig: "((\n. 2 * of_real pi * ii * f n w) \ contour_integral (circlepath z r) (\u. g u / (u - w))) F" + have f_tends_cig: "((\n. 2 * of_real pi * \ * f n w) \ contour_integral (circlepath z r) (\u. g u / (u - w))) F" apply (rule Lim_transform_eventually [where f = "\n. contour_integral (circlepath z r) (\u. f n u/(u - w))"]) apply (rule eventually_mono [OF cont]) apply (rule contour_integral_unique [OF Cauchy_integral_circlepath]) @@ -7077,7 +7077,7 @@ and z: "z \ u" and \: "polynomial_function \" and pasz: "path_image \ \ u - {z}" and loop: "pathfinish \ = pathstart \" and zero: "\w. w \ u \ winding_number \ w = 0" - shows "((\w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \ z * f z)) \" + shows "((\w. f w / (w - z)) has_contour_integral (2*pi * \ * winding_number \ z * f z)) \" proof - obtain \' where pf\': "polynomial_function \'" and \': "\x. (\ has_vector_derivative (\' x)) (at x)" using has_vector_derivative_polynomial_function [OF \] by blast @@ -7468,7 +7468,7 @@ and z: "z \ s" and vpg: "valid_path \" and pasz: "path_image \ \ s - {z}" and loop: "pathfinish \ = pathstart \" and zero: "\w. w \ s \ winding_number \ w = 0" - shows "((\w. f w / (w - z)) has_contour_integral (2*pi * ii * winding_number \ z * f z)) \" + shows "((\w. f w / (w - z)) has_contour_integral (2*pi * \ * winding_number \ z * f z)) \" proof - have "path \" using vpg by (blast intro: valid_path_imp_path) have hols: "(\w. f w / (w - z)) holomorphic_on s - {z}" "(\w. 1 / (w - z)) holomorphic_on s - {z}" diff -r d0e2bad67bd4 -r 58aab4745e85 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Tue Aug 02 21:05:34 2016 +0200 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Tue Aug 02 21:30:30 2016 +0200 @@ -75,44 +75,44 @@ subsection\Euler and de Moivre formulas.\ text\The sine series times @{term i}\ -lemma sin_ii_eq: "(\n. (ii * sin_coeff n) * z^n) sums (ii * sin z)" +lemma sin_ii_eq: "(\n. (\ * sin_coeff n) * z^n) sums (\ * sin z)" proof - - have "(\n. ii * sin_coeff n *\<^sub>R z^n) sums (ii * sin z)" + have "(\n. \ * sin_coeff n *\<^sub>R z^n) sums (\ * sin z)" using sin_converges sums_mult by blast then show ?thesis by (simp add: scaleR_conv_of_real field_simps) qed -theorem exp_Euler: "exp(ii * z) = cos(z) + ii * sin(z)" +theorem exp_Euler: "exp(\ * z) = cos(z) + \ * sin(z)" proof - - have "(\n. (cos_coeff n + ii * sin_coeff n) * z^n) - = (\n. (ii * z) ^ n /\<^sub>R (fact n))" + have "(\n. (cos_coeff n + \ * sin_coeff n) * z^n) + = (\n. (\ * z) ^ n /\<^sub>R (fact n))" proof fix n - show "(cos_coeff n + ii * sin_coeff n) * z^n = (ii * z) ^ n /\<^sub>R (fact n)" + show "(cos_coeff n + \ * sin_coeff n) * z^n = (\ * z) ^ n /\<^sub>R (fact n)" by (auto simp: cos_coeff_def sin_coeff_def scaleR_conv_of_real field_simps elim!: evenE oddE) qed - also have "... sums (exp (ii * z))" + also have "... sums (exp (\ * z))" by (rule exp_converges) - finally have "(\n. (cos_coeff n + ii * sin_coeff n) * z^n) sums (exp (ii * z))" . - moreover have "(\n. (cos_coeff n + ii * sin_coeff n) * z^n) sums (cos z + ii * sin z)" + finally have "(\n. (cos_coeff n + \ * sin_coeff n) * z^n) sums (exp (\ * z))" . + moreover have "(\n. (cos_coeff n + \ * sin_coeff n) * z^n) sums (cos z + \ * sin z)" using sums_add [OF cos_converges [of z] sin_ii_eq [of z]] by (simp add: field_simps scaleR_conv_of_real) ultimately show ?thesis using sums_unique2 by blast qed -corollary exp_minus_Euler: "exp(-(ii * z)) = cos(z) - ii * sin(z)" +corollary exp_minus_Euler: "exp(-(\ * z)) = cos(z) - \ * sin(z)" using exp_Euler [of "-z"] by simp -lemma sin_exp_eq: "sin z = (exp(ii * z) - exp(-(ii * z))) / (2*ii)" +lemma sin_exp_eq: "sin z = (exp(\ * z) - exp(-(\ * z))) / (2*\)" by (simp add: exp_Euler exp_minus_Euler) -lemma sin_exp_eq': "sin z = ii * (exp(-(ii * z)) - exp(ii * z)) / 2" +lemma sin_exp_eq': "sin z = \ * (exp(-(\ * z)) - exp(\ * z)) / 2" by (simp add: exp_Euler exp_minus_Euler) -lemma cos_exp_eq: "cos z = (exp(ii * z) + exp(-(ii * z))) / 2" +lemma cos_exp_eq: "cos z = (exp(\ * z) + exp(-(\ * z))) / 2" by (simp add: exp_Euler exp_minus_Euler) subsection\Relationships between real and complex trig functions\ @@ -127,7 +127,7 @@ shows "Re(cos(of_real x)) = cos x" by (simp add: cos_of_real) -lemma DeMoivre: "(cos z + ii * sin z) ^ n = cos(n * z) + ii * sin(n * z)" +lemma DeMoivre: "(cos z + \ * sin z) ^ n = cos(n * z) + \ * sin(n * z)" apply (simp add: exp_Euler [symmetric]) by (metis exp_of_nat_mult mult.left_commute) @@ -174,7 +174,7 @@ subsection\Get a nice real/imaginary separation in Euler's formula.\ lemma Euler: "exp(z) = of_real(exp(Re z)) * - (of_real(cos(Im z)) + ii * of_real(sin(Im z)))" + (of_real(cos(Im z)) + \ * of_real(sin(Im z)))" by (cases z) (simp add: exp_add exp_Euler cos_of_real exp_of_real sin_of_real) lemma Re_sin: "Re(sin z) = sin(Re z) * (exp(Im z) + exp(-(Im z))) / 2" @@ -209,7 +209,7 @@ apply (metis Re_exp cos_one_2pi_int mult.commute mult.left_neutral norm_exp_eq_Re norm_one one_complex.simps(1)) by (metis Im_exp Re_exp complex_Re_Im_cancel_iff cos_one_2pi_int sin_double Re_complex_of_real complex_Re_numeral exp_zero mult.assoc mult.left_commute mult_eq_0_iff mult_numeral_1 numeral_One of_real_0 sin_zero_iff_int2) -lemma exp_eq: "exp w = exp z \ (\n::int. w = z + (of_int (2 * n) * pi) * ii)" +lemma exp_eq: "exp w = exp z \ (\n::int. w = z + (of_int (2 * n) * pi) * \)" (is "?lhs = ?rhs") proof - have "exp w = exp z \ exp (w-z) = 1" @@ -226,9 +226,9 @@ lemma exp_integer_2pi: assumes "n \ \" - shows "exp((2 * n * pi) * ii) = 1" + shows "exp((2 * n * pi) * \) = 1" proof - - have "exp((2 * n * pi) * ii) = exp 0" + have "exp((2 * n * pi) * \) = exp 0" using assms by (simp only: Ints_def exp_eq) auto also have "... = 1" @@ -377,7 +377,7 @@ finally show ?thesis . qed -lemma dist_exp_ii_1: "norm(exp(ii * of_real t) - 1) = 2 * \sin(t / 2)\" +lemma dist_exp_ii_1: "norm(exp(\ * of_real t) - 1) = 2 * \sin(t / 2)\" 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) @@ -385,27 +385,27 @@ lemma sinh_complex: fixes z :: complex - shows "(exp z - inverse (exp z)) / 2 = -ii * sin(ii * z)" + shows "(exp z - inverse (exp z)) / 2 = -\ * sin(\ * z)" by (simp add: sin_exp_eq divide_simps exp_minus of_real_numeral) lemma sin_ii_times: fixes z :: complex - shows "sin(ii * z) = ii * ((exp z - inverse (exp z)) / 2)" + shows "sin(\ * z) = \ * ((exp z - inverse (exp z)) / 2)" using sinh_complex by auto lemma sinh_real: fixes x :: real - shows "of_real((exp x - inverse (exp x)) / 2) = -ii * sin(ii * of_real x)" + shows "of_real((exp x - inverse (exp x)) / 2) = -\ * sin(\ * of_real x)" by (simp add: exp_of_real sin_ii_times of_real_numeral) lemma cosh_complex: fixes z :: complex - shows "(exp z + inverse (exp z)) / 2 = cos(ii * z)" + shows "(exp z + inverse (exp z)) / 2 = cos(\ * z)" by (simp add: cos_exp_eq divide_simps exp_minus of_real_numeral exp_of_real) lemma cosh_real: fixes x :: real - shows "of_real((exp x + inverse (exp x)) / 2) = cos(ii * of_real x)" + shows "of_real((exp x + inverse (exp x)) / 2) = cos(\ * 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] @@ -614,14 +614,14 @@ definition Arg :: "complex \ real" where "Arg z \ if z = 0 then 0 else THE t. 0 \ t \ t < 2*pi \ - z = of_real(norm z) * exp(ii * of_real t)" + z = of_real(norm z) * exp(\ * of_real t)" lemma Arg_0 [simp]: "Arg(0) = 0" by (simp add: Arg_def) lemma Arg_unique_lemma: - assumes z: "z = of_real(norm z) * exp(ii * of_real t)" - and z': "z = of_real(norm z) * exp(ii * of_real t')" + assumes z: "z = of_real(norm z) * exp(\ * of_real t)" + and z': "z = of_real(norm z) * exp(\ * of_real t')" and t: "0 \ t" "t < 2*pi" and t': "0 \ t'" "t' < 2*pi" and nz: "z \ 0" @@ -647,7 +647,7 @@ by (simp add: n) qed -lemma Arg: "0 \ Arg z & Arg z < 2*pi & z = of_real(norm z) * exp(ii * of_real(Arg z))" +lemma Arg: "0 \ Arg z & Arg z < 2*pi & z = of_real(norm z) * exp(\ * of_real(Arg z))" proof (cases "z=0") case True then show ?thesis by (simp add: Arg_def) @@ -657,7 +657,7 @@ and ReIm: "Re z / cmod z = cos t" "Im z / cmod z = sin t" using sincos_total_2pi [OF complex_unit_circle [OF False]] by blast - have z: "z = of_real(norm z) * exp(ii * of_real t)" + have z: "z = of_real(norm z) * exp(\ * of_real t)" apply (rule complex_eqI) using t False ReIm apply (auto simp: exp_Euler sin_of_real cos_of_real divide_simps) @@ -673,13 +673,13 @@ corollary shows Arg_ge_0: "0 \ Arg z" and Arg_lt_2pi: "Arg z < 2*pi" - and Arg_eq: "z = of_real(norm z) * exp(ii * of_real(Arg z))" + and Arg_eq: "z = of_real(norm z) * exp(\ * of_real(Arg z))" using Arg by auto -lemma complex_norm_eq_1_exp: "norm z = 1 \ (\t. z = exp(ii * of_real t))" +lemma complex_norm_eq_1_exp: "norm z = 1 \ (\t. z = exp(\ * of_real t))" using Arg [of z] by auto -lemma Arg_unique: "\of_real r * exp(ii * of_real a) = z; 0 < r; 0 \ a; a < 2*pi\ \ Arg z = a" +lemma Arg_unique: "\of_real r * exp(\ * of_real a) = z; 0 < r; 0 \ a; a < 2*pi\ \ Arg z = a" apply (rule Arg_unique_lemma [OF _ Arg_eq]) using Arg [of z] apply (auto simp: norm_mult) @@ -1012,13 +1012,13 @@ text\Note that in this special case the unwinding number is -1, 0 or 1.\ definition unwinding :: "complex \ complex" where - "unwinding(z) = (z - Ln(exp z)) / (of_real(2*pi) * ii)" - -lemma unwinding_2pi: "(2*pi) * ii * unwinding(z) = z - Ln(exp z)" + "unwinding(z) = (z - Ln(exp z)) / (of_real(2*pi) * \)" + +lemma unwinding_2pi: "(2*pi) * \ * unwinding(z) = z - Ln(exp z)" by (simp add: unwinding_def) lemma Ln_times_unwinding: - "w \ 0 \ z \ 0 \ Ln(w * z) = Ln(w) + Ln(z) - (2*pi) * ii * unwinding(Ln w + Ln z)" + "w \ 0 \ z \ 0 \ Ln(w * z) = Ln(w) + Ln(z) - (2*pi) * \ * unwinding(Ln w + Ln z)" using unwinding_2pi by (simp add: exp_add) @@ -1192,22 +1192,22 @@ apply (metis Im_Ln_less_pi Im_Ln_le_pi add.commute add_mono_thms_linordered_field(3) inverse_nonzero_iff_nonzero mult_2) done -lemma Ln_minus1 [simp]: "Ln(-1) = ii * pi" +lemma Ln_minus1 [simp]: "Ln(-1) = \ * pi" apply (rule exp_complex_eqI) using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi apply (auto simp: abs_if) done -lemma Ln_ii [simp]: "Ln ii = ii * of_real pi/2" - using Ln_exp [of "ii * (of_real pi/2)"] +lemma Ln_ii [simp]: "Ln \ = \ * of_real pi/2" + using Ln_exp [of "\ * (of_real pi/2)"] unfolding exp_Euler by simp -lemma Ln_minus_ii [simp]: "Ln(-ii) = - (ii * pi/2)" +lemma Ln_minus_ii [simp]: "Ln(-\) = - (\ * pi/2)" proof - - have "Ln(-ii) = Ln(inverse ii)" by simp - also have "... = - (Ln ii)" using Ln_inverse by blast - also have "... = - (ii * pi/2)" by simp + have "Ln(-\) = Ln(inverse \)" by simp + also have "... = - (Ln \)" using Ln_inverse by blast + also have "... = - (\ * pi/2)" by simp finally show ?thesis . qed @@ -1215,9 +1215,9 @@ assumes "w \ 0" "z \ 0" shows "Ln(w * z) = (if Im(Ln w + Ln z) \ -pi then - (Ln(w) + Ln(z)) + ii * of_real(2*pi) + (Ln(w) + Ln(z)) + \ * of_real(2*pi) else if Im(Ln w + Ln z) > pi then - (Ln(w) + Ln(z)) - ii * of_real(2*pi) + (Ln(w) + Ln(z)) - \ * of_real(2*pi) else Ln(w) + Ln(z))" using pi_ge_zero Im_Ln_le_pi [of w] Im_Ln_le_pi [of z] using assms mpi_less_Im_Ln [of w] mpi_less_Im_Ln [of z] @@ -1242,8 +1242,8 @@ lemma Ln_minus: assumes "z \ 0" shows "Ln(-z) = (if Im(z) \ 0 \ ~(Re(z) < 0 \ Im(z) = 0) - then Ln(z) + ii * pi - else Ln(z) - ii * pi)" (is "_ = ?rhs") + then Ln(z) + \ * pi + else Ln(z) - \ * pi)" (is "_ = ?rhs") 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] by (fastforce simp: exp_add exp_diff exp_Euler intro!: Ln_unique) @@ -1280,9 +1280,9 @@ lemma Ln_times_ii: assumes "z \ 0" - shows "Ln(ii * z) = (if 0 \ Re(z) | Im(z) < 0 - then Ln(z) + ii * of_real pi/2 - else Ln(z) - ii * of_real(3 * pi/2))" + shows "Ln(\ * z) = (if 0 \ Re(z) | Im(z) < 0 + then Ln(z) + \ * of_real pi/2 + else Ln(z) - \ * 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 (auto simp: Ln_times) @@ -1313,7 +1313,7 @@ by simp next case False - then have "z / of_real(norm z) = exp(ii * of_real(Arg z))" + then have "z / of_real(norm z) = exp(\ * of_real(Arg z))" using Arg [of z] by (metis abs_norm_cancel nonzero_mult_divide_cancel_left norm_of_real zero_less_norm_iff) then have "- z / of_real(norm z) = exp (\ * (of_real (Arg z) - pi))" diff -r d0e2bad67bd4 -r 58aab4745e85 src/HOL/Multivariate_Analysis/Conformal_Mappings.thy --- a/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy Tue Aug 02 21:05:34 2016 +0200 +++ b/src/HOL/Multivariate_Analysis/Conformal_Mappings.thy Tue Aug 02 21:30:30 2016 +0200 @@ -42,7 +42,7 @@ have der_dif: "(deriv ^^ n) (\w. f w - y) z = (deriv ^^ n) f z" using \0 < r\ \0 < n\ by (auto simp: higher_deriv_diff [OF holf holomorphic_on_const]) - have "norm ((2 * of_real pi * ii)/(fact n) * (deriv ^^ n) (\w. f w - y) z) + have "norm ((2 * of_real pi * \)/(fact n) * (deriv ^^ n) (\w. f w - y) z) \ (B0/r^(Suc n)) * (2 * pi * r)" apply (rule has_contour_integral_bound_circlepath [of "(\u. (f u - y)/(u - z)^(Suc n))" _ z]) using Cauchy_has_contour_integral_higher_derivative_circlepath [OF contf' holf'] @@ -70,7 +70,7 @@ (circlepath \ r)" apply (rule Cauchy_has_contour_integral_higher_derivative_circlepath [OF contf holf]) using \0 < r\ by simp - then have "norm ((2 * pi * ii)/(fact n) * (deriv ^^ n) f \) \ (B / r^(Suc n)) * (2 * pi * r)" + then have "norm ((2 * pi * \)/(fact n) * (deriv ^^ n) f \) \ (B / r^(Suc n)) * (2 * pi * r)" apply (rule has_contour_integral_bound_circlepath) using \0 \ B\ \0 < r\ apply (simp_all add: norm_divide norm_power nof frac_le norm_minus_commute del: power_Suc) @@ -1229,13 +1229,13 @@ done then obtain \ where "\>0" and \: "cball 0 \ \ U" using \open U\ open_contains_cball by blast - then have "\ * exp(2 * of_real pi * ii * (0/n)) \ cball 0 \" - "\ * exp(2 * of_real pi * ii * (1/n)) \ cball 0 \" + then have "\ * exp(2 * of_real pi * \ * (0/n)) \ cball 0 \" + "\ * exp(2 * of_real pi * \ * (1/n)) \ cball 0 \" by (auto simp: norm_mult) - with \ have "\ * exp(2 * of_real pi * ii * (0/n)) \ U" - "\ * exp(2 * of_real pi * ii * (1/n)) \ U" by blast+ - then obtain y0 y1 where "y0 \ T" and y0: "(y0 - \) * g y0 = \ * exp(2 * of_real pi * ii * (0/n))" - and "y1 \ T" and y1: "(y1 - \) * g y1 = \ * exp(2 * of_real pi * ii * (1/n))" + with \ have "\ * exp(2 * of_real pi * \ * (0/n)) \ U" + "\ * exp(2 * of_real pi * \ * (1/n)) \ U" by blast+ + then obtain y0 y1 where "y0 \ T" and y0: "(y0 - \) * g y0 = \ * exp(2 * of_real pi * \ * (0/n))" + and "y1 \ T" and y1: "(y1 - \) * g y1 = \ * exp(2 * of_real pi * \ * (1/n))" by (auto simp: U_def) then have "y0 \ ball \ \" "y1 \ ball \ \" using Tsb by auto moreover have "y0 \ y1" @@ -1720,7 +1720,7 @@ then have 3: "continuous_on S (\z. if 0 \ Im z then f z else cnj (f (cnj z)))" by force show ?thesis - apply (rule holomorphic_on_paste_across_line [OF \open S\, of "-ii" _ 0]) + apply (rule holomorphic_on_paste_across_line [OF \open S\, of "- \" _ 0]) using 1 2 3 apply auto done @@ -2141,7 +2141,7 @@ definition residue :: "(complex \ complex) \ complex \ complex" where "residue f z = (SOME int. \e>0. \\>0. \ (f has_contour_integral 2*pi* ii *int) (circlepath z \))" + \ (f has_contour_integral 2*pi* \ *int) (circlepath z \))" lemma contour_integral_circlepath_eq: assumes "open s" and f_holo:"f holomorphic_on (s-{z})" and "0e2" @@ -2253,11 +2253,11 @@ lemma base_residue: assumes "open s" "z\s" "r>0" and f_holo:"f holomorphic_on (s - {z})" and r_cball:"cball z r \ s" - shows "(f has_contour_integral 2*pi*ii* (residue f z)) (circlepath z r)" + shows "(f has_contour_integral 2 * pi * \ * (residue f z)) (circlepath z r)" proof - obtain e where "e>0" and e_cball:"cball z e \ s" using open_contains_cball[of s] \open s\ \z\s\ by auto - define c where "c \ 2*pi*ii" + define c where "c \ 2 * pi * \" define i where "i \ contour_integral (circlepath z e) f / c" have "(f has_contour_integral c*i) (circlepath z \)" when "\>0" "\ proof - diff -r d0e2bad67bd4 -r 58aab4745e85 src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Aug 02 21:05:34 2016 +0200 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Aug 02 21:30:30 2016 +0200 @@ -167,8 +167,7 @@ instantiation complex :: euclidean_space begin -definition Basis_complex_def: - "Basis = {1, ii}" +definition Basis_complex_def: "Basis = {1, \}" instance by standard (auto simp add: Basis_complex_def intro: complex_eqI split: if_split_asm) diff -r d0e2bad67bd4 -r 58aab4745e85 src/HOL/Nonstandard_Analysis/NSComplex.thy --- a/src/HOL/Nonstandard_Analysis/NSComplex.thy Tue Aug 02 21:05:34 2016 +0200 +++ b/src/HOL/Nonstandard_Analysis/NSComplex.thy Tue Aug 02 21:30:30 2016 +0200 @@ -35,7 +35,7 @@ definition iii :: hcomplex where - "iii = star_of ii" + "iii = star_of \" (*------- complex conjugate ------*) @@ -602,7 +602,7 @@ subsection\@{term hcomplex_of_complex}: the Injection from type @{typ complex} to to @{typ hcomplex}\ -lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii" +lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex \" by (rule iii_def) lemma hRe_hcomplex_of_complex: diff -r d0e2bad67bd4 -r 58aab4745e85 src/HOL/Probability/Characteristic_Functions.thy --- a/src/HOL/Probability/Characteristic_Functions.thy Tue Aug 02 21:05:34 2016 +0200 +++ b/src/HOL/Probability/Characteristic_Functions.thy Tue Aug 02 21:30:30 2016 +0200 @@ -48,8 +48,8 @@ lemma interval_integral_iexp: fixes a b :: real - shows "(CLBINT x=a..b. iexp x) = ii * iexp a - ii * iexp b" - by (subst interval_integral_FTC_finite [where F = "\x. -ii * iexp x"]) + shows "(CLBINT x=a..b. iexp x) = \ * iexp a - \ * iexp b" + by (subst interval_integral_FTC_finite [where F = "\x. -\ * iexp x"]) (auto intro!: derivative_eq_intros continuous_intros) subsection \The Characteristic Function of a Real Measure.\ @@ -64,7 +64,7 @@ lemma (in prob_space) integrable_iexp: assumes f: "f \ borel_measurable M" "\x. Im (f x) = 0" - shows "integrable M (\x. exp (ii * (f x)))" + shows "integrable M (\x. exp (\ * (f x)))" proof (intro integrable_const_bound [of _ 1]) from f have "\x. of_real (Re (f x)) = f x" by (simp add: complex_eq_iff) @@ -133,18 +133,18 @@ fixes x :: real and n :: nat defines "f s m \ complex_of_real ((x - s) ^ m)" shows "(CLBINT s=0..x. f s n * iexp s) = - x^Suc n / Suc n + (ii / Suc n) * (CLBINT s=0..x. f s (Suc n) * iexp s)" + x^Suc n / Suc n + (\ / Suc n) * (CLBINT s=0..x. f s (Suc n) * iexp s)" proof - have 1: "((\s. complex_of_real(-((x - s) ^ (Suc n) / (Suc n))) * iexp s) - has_vector_derivative complex_of_real((x - s)^n) * iexp s + (ii * iexp s) * complex_of_real(-((x - s) ^ (Suc n) / (Suc n)))) + has_vector_derivative complex_of_real((x - s)^n) * iexp s + (\ * iexp s) * complex_of_real(-((x - s) ^ (Suc n) / (Suc n)))) (at s within A)" for s A by (intro derivative_eq_intros) auto let ?F = "\s. complex_of_real(-((x - s) ^ (Suc n) / (Suc n))) * iexp s" - have "x^(Suc n) / (Suc n) = (CLBINT s=0..x. (f s n * iexp s + (ii * iexp s) * -(f s (Suc n) / (Suc n))))" (is "?LHS = ?RHS") + have "x^(Suc n) / (Suc n) = (CLBINT s=0..x. (f s n * iexp s + (\ * iexp s) * -(f s (Suc n) / (Suc n))))" (is "?LHS = ?RHS") proof - - have "?RHS = (CLBINT s=0..x. (f s n * iexp s + (ii * iexp s) * + have "?RHS = (CLBINT s=0..x. (f s n * iexp s + (\ * iexp s) * complex_of_real(-((x - s) ^ (Suc n) / (Suc n)))))" by (cases "0 \ x") (auto intro!: simp: f_def[abs_def]) also have "... = ?F x - ?F 0" @@ -165,7 +165,7 @@ fixes x :: real defines "f s m \ complex_of_real ((x - s) ^ m)" shows "iexp x = - (\k \ n. (ii * x)^k / (fact k)) + ((ii ^ (Suc n)) / (fact n)) * (CLBINT s=0..x. (f s n) * (iexp s))" (is "?P n") + (\k \ n. (\ * x)^k / (fact k)) + ((\ ^ (Suc n)) / (fact n)) * (CLBINT s=0..x. (f s n) * (iexp s))" (is "?P n") proof (induction n) show "?P 0" by (auto simp add: field_simps interval_integral_iexp f_def zero_ereal_def) @@ -184,7 +184,7 @@ lemma iexp_eq2: fixes x :: real defines "f s m \ complex_of_real ((x - s) ^ m)" - shows "iexp x = (\k\Suc n. (ii*x)^k/fact k) + ii^Suc n/fact n * (CLBINT s=0..x. f s n*(iexp s - 1))" + shows "iexp x = (\k\Suc n. (\*x)^k/fact k) + \^Suc n/fact n * (CLBINT s=0..x. f s n*(iexp s - 1))" proof - have isCont_f: "isCont (\s. f s n) x" for n x by (auto simp: f_def) @@ -204,7 +204,7 @@ (auto intro!: derivative_eq_intros simp del: power_Suc simp add: add_nonneg_eq_0_iff) qed (auto intro: continuous_at_imp_continuous_on isCont_f) - have calc3: "ii ^ (Suc (Suc n)) / (fact (Suc n)) = (ii ^ (Suc n) / (fact n)) * (ii / (Suc n))" + have calc3: "\ ^ (Suc (Suc n)) / (fact (Suc n)) = (\ ^ (Suc n) / (fact n)) * (\ / (Suc n))" by (simp add: field_simps) show ?thesis @@ -246,10 +246,10 @@ finally show ?thesis . qed -lemma iexp_approx1: "cmod (iexp x - (\k \ n. (ii * x)^k / fact k)) \ \x\^(Suc n) / fact (Suc n)" +lemma iexp_approx1: "cmod (iexp x - (\k \ n. (\ * x)^k / fact k)) \ \x\^(Suc n) / fact (Suc n)" proof - - have "iexp x - (\k \ n. (ii * x)^k / fact k) = - ((ii ^ (Suc n)) / (fact n)) * (CLBINT s=0..x. (x - s)^n * (iexp s))" (is "?t1 = ?t2") + have "iexp x - (\k \ n. (\ * x)^k / fact k) = + ((\ ^ (Suc n)) / (fact n)) * (CLBINT s=0..x. (x - s)^n * (iexp s))" (is "?t1 = ?t2") by (subst iexp_eq1 [of _ n], simp add: field_simps) then have "cmod (?t1) = cmod (?t2)" by simp @@ -268,7 +268,7 @@ finally show ?thesis . qed -lemma iexp_approx2: "cmod (iexp x - (\k \ n. (ii * x)^k / fact k)) \ 2 * \x\^n / fact n" +lemma iexp_approx2: "cmod (iexp x - (\k \ n. (\ * x)^k / fact k)) \ 2 * \x\^n / fact n" proof (induction n) \ \really cases\ case (Suc n) have *: "\a b. interval_lebesgue_integrable lborel a b f \ interval_lebesgue_integrable lborel a b g \ @@ -277,8 +277,8 @@ using order_trans[OF f g] f g unfolding interval_lebesgue_integral_def interval_lebesgue_integrable_def by (auto simp: integral_nonneg_AE[OF AE_I2] intro!: integral_mono mult_mono) - have "iexp x - (\k \ Suc n. (ii * x)^k / fact k) = - ((ii ^ (Suc n)) / (fact n)) * (CLBINT s=0..x. (x - s)^n * (iexp s - 1))" (is "?t1 = ?t2") + have "iexp x - (\k \ Suc n. (\ * x)^k / fact k) = + ((\ ^ (Suc n)) / (fact n)) * (CLBINT s=0..x. (x - s)^n * (iexp s - 1))" (is "?t1 = ?t2") unfolding iexp_eq2 [of x n] by (simp add: field_simps) then have "cmod (?t1) = cmod (?t2)" by simp @@ -301,13 +301,13 @@ lemma (in real_distribution) char_approx1: assumes integrable_moments: "\k. k \ n \ integrable M (\x. x^k)" - shows "cmod (char M t - (\k \ n. ((ii * t)^k / fact k) * expectation (\x. x^k))) \ + shows "cmod (char M t - (\k \ n. ((\ * t)^k / fact k) * expectation (\x. x^k))) \ (2*\t\^n / fact n) * expectation (\x. \x\^n)" (is "cmod (char M t - ?t1) \ _") proof - have integ_iexp: "integrable M (\x. iexp (t * x))" by (intro integrable_const_bound) auto - define c where [abs_def]: "c k x = (ii * t)^k / fact k * complex_of_real (x^k)" for k x + define c where [abs_def]: "c k x = (\ * t)^k / fact k * complex_of_real (x^k)" for k x have integ_c: "\k. k \ n \ integrable M (\x. c k x)" unfolding c_def by (intro integrable_mult_right integrable_of_real integrable_moments) @@ -335,14 +335,14 @@ lemma (in real_distribution) char_approx2: assumes integrable_moments: "\k. k \ n \ integrable M (\x. x ^ k)" - shows "cmod (char M t - (\k \ n. ((ii * t)^k / fact k) * expectation (\x. x^k))) \ + shows "cmod (char M t - (\k \ n. ((\ * t)^k / fact k) * expectation (\x. x^k))) \ (\t\^n / fact (Suc n)) * expectation (\x. min (2 * \x\^n * Suc n) (\t\ * \x\^Suc n))" (is "cmod (char M t - ?t1) \ _") proof - have integ_iexp: "integrable M (\x. iexp (t * x))" by (intro integrable_const_bound) auto - define c where [abs_def]: "c k x = (ii * t)^k / fact k * complex_of_real (x^k)" for k x + define c where [abs_def]: "c k x = (\ * t)^k / fact k * complex_of_real (x^k)" for k x have integ_c: "\k. k \ n \ integrable M (\x. c k x)" unfolding c_def by (intro integrable_mult_right integrable_of_real integrable_moments) @@ -445,7 +445,7 @@ assumes integrable_moments : "\k. k \ n \ integrable M (\x. X x ^ k)" and rv_X[measurable]: "random_variable borel X" and \_distr : "distr M borel X = \" - shows "cmod (char \ t - (\k \ n. ((ii * t)^k / fact k) * expectation (\x. (X x)^k))) \ + shows "cmod (char \ t - (\k \ n. ((\ * t)^k / fact k) * expectation (\x. (X x)^k))) \ (2 * \t\^n / fact n) * expectation (\x. \X x\^n)" unfolding \_distr[symmetric] apply (subst (1 2) integral_distr [symmetric, OF rv_X], simp, simp) @@ -495,7 +495,7 @@ "char std_normal_distribution = (\t. complex_of_real (exp (- (t^2) / 2)))" proof (intro ext LIMSEQ_unique) fix t :: real - let ?f' = "\k. (ii * t)^k / fact k * (LINT x | std_normal_distribution. x^k)" + let ?f' = "\k. (\ * t)^k / fact k * (LINT x | std_normal_distribution. x^k)" let ?f = "\n. (\k \ n. ?f' k)" show "?f \ exp (-(t^2) / 2)" proof (rule limseq_even_odd) diff -r d0e2bad67bd4 -r 58aab4745e85 src/HOL/Probability/Levy.thy --- a/src/HOL/Probability/Levy.thy Tue Aug 02 21:05:34 2016 +0200 +++ b/src/HOL/Probability/Levy.thy Tue Aug 02 21:30:30 2016 +0200 @@ -19,21 +19,21 @@ lemma Levy_Inversion_aux1: fixes a b :: real assumes "a \ b" - shows "((\t. (iexp (-(t * a)) - iexp (-(t * b))) / (ii * t)) \ b - a) (at 0)" + shows "((\t. (iexp (-(t * a)) - iexp (-(t * b))) / (\ * t)) \ b - a) (at 0)" (is "(?F \ _) (at _)") proof - have 1: "cmod (?F t - (b - a)) \ a^2 / 2 * abs t + b^2 / 2 * abs t" if "t \ 0" for t proof - have "cmod (?F t - (b - a)) = cmod ( - (iexp (-(t * a)) - (1 + ii * -(t * a))) / (ii * t) - - (iexp (-(t * b)) - (1 + ii * -(t * b))) / (ii * t))" - (is "_ = cmod (?one / (ii * t) - ?two / (ii * t))") + (iexp (-(t * a)) - (1 + \ * -(t * a))) / (\ * t) - + (iexp (-(t * b)) - (1 + \ * -(t * b))) / (\ * t))" + (is "_ = cmod (?one / (\ * t) - ?two / (\ * t))") using \t \ 0\ by (intro arg_cong[where f=norm]) (simp add: field_simps) - also have "\ \ cmod (?one / (ii * t)) + cmod (?two / (ii * t))" + also have "\ \ cmod (?one / (\ * t)) + cmod (?two / (\ * t))" by (rule norm_triangle_ineq4) - also have "cmod (?one / (ii * t)) = cmod ?one / abs t" + also have "cmod (?one / (\ * t)) = cmod ?one / abs t" by (simp add: norm_divide norm_mult) - also have "cmod (?two / (ii * t)) = cmod ?two / abs t" + also have "cmod (?two / (\ * t)) = cmod ?two / abs t" by (simp add: norm_divide norm_mult) also have "cmod ?one / abs t + cmod ?two / abs t \ ((- (a * t))^2 / 2) / abs t + ((- (b * t))^2 / 2) / abs t" @@ -60,9 +60,9 @@ lemma Levy_Inversion_aux2: fixes a b t :: real assumes "a \ b" and "t \ 0" - shows "cmod ((iexp (t * b) - iexp (t * a)) / (ii * t)) \ b - a" (is "?F \ _") + shows "cmod ((iexp (t * b) - iexp (t * a)) / (\ * t)) \ b - a" (is "?F \ _") proof - - have "?F = cmod (iexp (t * a) * (iexp (t * (b - a)) - 1) / (ii * t))" + have "?F = cmod (iexp (t * a) * (iexp (t * (b - a)) - 1) / (\ * t))" using \t \ 0\ by (intro arg_cong[where f=norm]) (simp add: field_simps exp_diff exp_minus) also have "\ = cmod (iexp (t * (b - a)) - 1) / abs t" unfolding norm_divide norm_mult norm_exp_ii_times using \t \ 0\ @@ -81,14 +81,14 @@ assumes "a \ b" defines "\ \ measure M" and "\ \ char M" assumes "\ {a} = 0" and "\ {b} = 0" - shows "(\T. 1 / (2 * pi) * (CLBINT t=-T..T. (iexp (-(t * a)) - iexp (-(t * b))) / (ii * t) * \ t)) + shows "(\T. 1 / (2 * pi) * (CLBINT t=-T..T. (iexp (-(t * a)) - iexp (-(t * b))) / (\ * t) * \ t)) \ \ {a<..b}" (is "(\T. 1 / (2 * pi) * (CLBINT t=-T..T. ?F t * \ t)) \ of_real (\ {a<..b})") proof - interpret P: pair_sigma_finite lborel M .. from bounded_Si obtain B where Bprop: "\T. abs (Si T) \ B" by auto from Bprop [of 0] have [simp]: "B \ 0" by auto - let ?f = "\t x :: real. (iexp (t * (x - a)) - iexp(t * (x - b))) / (ii * t)" + let ?f = "\t x :: real. (iexp (t * (x - a)) - iexp(t * (x - b))) / (\ * t)" { fix T :: real assume "T \ 0" let ?f' = "$t, x). indicator {-T<..R ?f t x" @@ -110,7 +110,7 @@ using 1 by (intro interval_lebesgue_integral_add(2) [symmetric] interval_integrable_mirror[THEN iffD2]) simp_all also have "\ = (CLBINT t=(0::real)..T. ((iexp(t * (x - a)) - iexp (-(t * (x - a)))) - - (iexp(t * (x - b)) - iexp (-(t * (x - b))))) / (ii * t))" + (iexp(t * (x - b)) - iexp (-(t * (x - b))))) / (\ * t))" using \T \ 0\ by (intro interval_integral_cong) (auto simp add: divide_simps) also have "\ = (CLBINT t=(0::real)..T. complex_of_real( 2 * (sin (t * (x - a)) / t) - 2 * (sin (t * (x - b)) / t)))" diff -r d0e2bad67bd4 -r 58aab4745e85 src/HOL/ex/BinEx.thy --- a/src/HOL/ex/BinEx.thy Tue Aug 02 21:05:34 2016 +0200 +++ b/src/HOL/ex/BinEx.thy Tue Aug 02 21:30:30 2016 +0200 @@ -750,22 +750,22 @@ subsection\Complex Arithmetic\ -lemma "(1359 + 93746*ii) - (2468 + 46375*ii) = -1109 + 47371*ii" +lemma "(1359 + 93746*$ - (2468 + 46375*\) = -1109 + 47371*\" by simp -lemma "- (65745 + -47371*ii) = -65745 + 47371*ii" +lemma "- (65745 + -47371*\) = -65745 + 47371*\" by simp text\Multiplication requires distributive laws. Perhaps versions instantiated to literal constants should be added to the simpset.\ -lemma "(1 + ii) * (1 - ii) = 2" +lemma "(1 + \) * (1 - \) = 2" by (simp add: ring_distribs) -lemma "(1 + 2*ii) * (1 + 3*ii) = -5 + 5*ii" +lemma "(1 + 2*\) * (1 + 3*\) = -5 + 5*\" by (simp add: ring_distribs) -lemma "(-84 + 255*ii) + (51 * 255*ii) = -84 + 13260 * ii" +lemma "(-84 + 255*\) + (51 * 255*\) = -84 + 13260 * \" by (simp add: ring_distribs) text\No inequalities or linear arithmetic: the complex numbers are unordered!\ diff -r d0e2bad67bd4 -r 58aab4745e85 src/HOL/ex/Cubic_Quartic.thy --- a/src/HOL/ex/Cubic_Quartic.thy Tue Aug 02 21:05:34 2016 +0200 +++ b/src/HOL/ex/Cubic_Quartic.thy Tue Aug 02 21:30:30 2016 +0200 @@ -93,8 +93,8 @@ q = (9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3); s = csqrt(q^2 + p^3); s1 = (if p = 0 then ccbrt(2 * q) else ccbrt(q + s)); - s2 = -s1 * (1 + ii * csqrt 3) / 2; - s3 = -s1 * (1 - ii * csqrt 3) / 2 + s2 = -s1 * (1 + \ * csqrt 3) / 2; + s3 = -s1 * (1 - \ * csqrt 3) / 2 in if p = 0 then a * x^3 + b * x^2 + c * x + d = 0 \ @@ -112,8 +112,8 @@ let ?q = "(9 * a * b * c - 2 * b^3 - 27 * a^2 * d) / (54 * a^3)" let ?s = "csqrt (?q^2 + ?p^3)" let ?s1 = "if ?p = 0 then ccbrt(2 * ?q) else ccbrt(?q + ?s)" - let ?s2 = "- ?s1 * (1 + ii * csqrt 3) / 2" - let ?s3 = "- ?s1 * (1 - ii * csqrt 3) / 2" + let ?s2 = "- ?s1 * (1 + \ * csqrt 3) / 2" + let ?s3 = "- ?s1 * (1 - \ * csqrt 3) / 2" let ?y = "x + b / (3 * a)" from a0 have zero: "9 * a^2 \ 0" "a^3 * 54 \ 0" "(a * 3) \ 0" by auto @@ -122,9 +122,9 @@ have "csqrt 3^2 = 3" by (rule power2_csqrt) then have th0: "?s^2 = ?q^2 + ?p ^ 3 \ ?s1^ 3 = (if ?p = 0 then 2 * ?q else ?q + ?s) \ - ?s2 = - ?s1 * (1 + ii * csqrt 3) / 2 \ - ?s3 = - ?s1 * (1 - ii * csqrt 3) / 2 \ - ii^2 + 1 = 0 \ csqrt 3^2 = 3" + ?s2 = - ?s1 * (1 + \ * csqrt 3) / 2 \ + ?s3 = - ?s1 * (1 - \ * csqrt 3) / 2 \ + \^2 + 1 = 0 \ csqrt 3^2 = 3" using zero by (simp add: field_simps ccbrt) from cubic_basic[OF th0, of ?y] show ?thesis