# HG changeset patch # User hoelzl # Date 1399458335 -7200 # Node ID 48a745e1bde7cf937676137a864cacfe78c731f8 # Parent 3e8cbb624cc543b5eba69a72c97c60491b881e32 avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex. diff -r 3e8cbb624cc5 -r 48a745e1bde7 NEWS --- a/NEWS Tue May 06 23:35:24 2014 +0200 +++ b/NEWS Wed May 07 12:25:35 2014 +0200 @@ -590,6 +590,48 @@ * Include more theorems in continuous_intros. Remove the continuous_on_intros, isCont_intros collections, these facts are now in continuous_intros. +* Theorems about complex numbers are now stated only using Re and Im, the Complex + constructor is not used anymore. It is possible to use primcorec to defined the + behaviour of a complex-valued function. + + Removed theorems about the Complex constructor from the simpset, they are + available as the lemma collection legacy_Complex_simps. This especially + removes + i_complex_of_real: "ii * complex_of_real r = Complex 0 r". + + Instead the reverse direction is supported with + Complex_eq: "Complex a b = a + \ * b" + + Moved csqrt from Fundamental_Algebra_Theorem to Complex. + + Renamings: + Re/Im ~> complex.sel + complex_Re/Im_zero ~> zero_complex.sel + complex_Re/Im_add ~> plus_complex.sel + complex_Re/Im_minus ~> uminus_complex.sel + complex_Re/Im_diff ~> minus_complex.sel + complex_Re/Im_one ~> one_complex.sel + complex_Re/Im_mult ~> times_complex.sel + complex_Re/Im_inverse ~> inverse_complex.sel + complex_Re/Im_scaleR ~> scaleR_complex.sel + complex_Re/Im_i ~> ii.sel + complex_Re/Im_cnj ~> cnj.sel + Re/Im_cis ~> cis.sel + + complex_divide_def ~> divide_complex_def + complex_norm_def ~> norm_complex_def + cmod_def ~> norm_complex_de + + Removed theorems: + complex_zero_def + complex_add_def + complex_minus_def + complex_diff_def + complex_one_def + complex_mult_def + complex_inverse_def + complex_scaleR_def + * Removed solvers remote_cvc3 and remote_z3. Use cvc3 and z3 instead. * Nitpick: diff -r 3e8cbb624cc5 -r 48a745e1bde7 src/HOL/Complex.thy --- a/src/HOL/Complex.thy Tue May 06 23:35:24 2014 +0200 +++ b/src/HOL/Complex.thy Wed May 07 12:25:35 2014 +0200 @@ -10,202 +10,105 @@ imports Transcendental begin -datatype complex = Complex real real +text {* -primrec Re :: "complex \ real" - where Re: "Re (Complex x y) = x" +We use the @{text codatatype}-command to define the type of complex numbers. This might look strange +at first, but allows us to use @{text primcorec} to define complex-functions by defining their +real and imaginary result separate. -primrec Im :: "complex \ real" - where Im: "Im (Complex x y) = y" +*} -lemma complex_surj [simp]: "Complex (Re z) (Im z) = z" - by (induct z) simp +codatatype complex = Complex (Re: real) (Im: real) + +lemma complex_surj: "Complex (Re z) (Im z) = z" + by (rule complex.collapse) lemma complex_eqI [intro?]: "\Re x = Re y; Im x = Im y\ \ x = y" - by (induct x, induct y) simp + by (rule complex.expand) simp lemma complex_eq_iff: "x = y \ Re x = Re y \ Im x = Im y" - by (induct x, induct y) simp - + by (auto intro: complex.expand) subsection {* Addition and Subtraction *} instantiation complex :: ab_group_add begin -definition complex_zero_def: - "0 = Complex 0 0" - -definition complex_add_def: - "x + y = Complex (Re x + Re y) (Im x + Im y)" - -definition complex_minus_def: - "- x = Complex (- Re x) (- Im x)" - -definition complex_diff_def: - "x - (y\complex) = x + - y" +primcorec zero_complex where + "Re 0 = 0" +| "Im 0 = 0" -lemma Complex_eq_0 [simp]: "Complex a b = 0 \ a = 0 \ b = 0" - by (simp add: complex_zero_def) - -lemma complex_Re_zero [simp]: "Re 0 = 0" - by (simp add: complex_zero_def) - -lemma complex_Im_zero [simp]: "Im 0 = 0" - by (simp add: complex_zero_def) - -lemma complex_add [simp]: - "Complex a b + Complex c d = Complex (a + c) (b + d)" - by (simp add: complex_add_def) +primcorec plus_complex where + "Re (x + y) = Re x + Re y" +| "Im (x + y) = Im x + Im y" -lemma complex_Re_add [simp]: "Re (x + y) = Re x + Re y" - by (simp add: complex_add_def) - -lemma complex_Im_add [simp]: "Im (x + y) = Im x + Im y" - by (simp add: complex_add_def) - -lemma complex_minus [simp]: - "- (Complex a b) = Complex (- a) (- b)" - by (simp add: complex_minus_def) - -lemma complex_Re_minus [simp]: "Re (- x) = - Re x" - by (simp add: complex_minus_def) +primcorec uminus_complex where + "Re (- x) = - Re x" +| "Im (- x) = - Im x" -lemma complex_Im_minus [simp]: "Im (- x) = - Im x" - by (simp add: complex_minus_def) - -lemma complex_diff [simp]: - "Complex a b - Complex c d = Complex (a - c) (b - d)" - by (simp add: complex_diff_def) - -lemma complex_Re_diff [simp]: "Re (x - y) = Re x - Re y" - by (simp add: complex_diff_def) - -lemma complex_Im_diff [simp]: "Im (x - y) = Im x - Im y" - by (simp add: complex_diff_def) +primcorec minus_complex where + "Re (x - y) = Re x - Re y" +| "Im (x - y) = Im x - Im y" instance - by intro_classes (simp_all add: complex_add_def complex_diff_def) + by intro_classes (simp_all add: complex_eq_iff) end - subsection {* Multiplication and Division *} instantiation complex :: field_inverse_zero begin -definition complex_one_def: - "1 = Complex 1 0" - -definition complex_mult_def: - "x * y = Complex (Re x * Re y - Im x * Im y) (Re x * Im y + Im x * Re y)" - -definition complex_inverse_def: - "inverse x = - Complex (Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)) (- Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2))" - -definition complex_divide_def: - "x / (y\complex) = x * inverse y" - -lemma Complex_eq_1 [simp]: - "Complex a b = 1 \ a = 1 \ b = 0" - by (simp add: complex_one_def) - -lemma Complex_eq_neg_1 [simp]: - "Complex a b = - 1 \ a = - 1 \ b = 0" - by (simp add: complex_one_def) - -lemma complex_Re_one [simp]: "Re 1 = 1" - by (simp add: complex_one_def) +primcorec one_complex where + "Re 1 = 1" +| "Im 1 = 0" -lemma complex_Im_one [simp]: "Im 1 = 0" - by (simp add: complex_one_def) - -lemma complex_mult [simp]: - "Complex a b * Complex c d = Complex (a * c - b * d) (a * d + b * c)" - by (simp add: complex_mult_def) - -lemma complex_Re_mult [simp]: "Re (x * y) = Re x * Re y - Im x * Im y" - by (simp add: complex_mult_def) +primcorec times_complex where + "Re (x * y) = Re x * Re y - Im x * Im y" +| "Im (x * y) = Re x * Im y + Im x * Re y" -lemma complex_Im_mult [simp]: "Im (x * y) = Re x * Im y + Im x * Re y" - by (simp add: complex_mult_def) - -lemma complex_inverse [simp]: - "inverse (Complex a b) = Complex (a / (a\<^sup>2 + b\<^sup>2)) (- b / (a\<^sup>2 + b\<^sup>2))" - by (simp add: complex_inverse_def) +primcorec inverse_complex where + "Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)" +| "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)" -lemma complex_Re_inverse: - "Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)" - by (simp add: complex_inverse_def) - -lemma complex_Im_inverse: - "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)" - by (simp add: complex_inverse_def) +definition "x / (y\complex) = x * inverse y" instance - by intro_classes (simp_all add: complex_mult_def - distrib_left distrib_right right_diff_distrib left_diff_distrib - complex_inverse_def complex_divide_def - power2_eq_square add_divide_distrib [symmetric] - complex_eq_iff) + by intro_classes + (simp_all add: complex_eq_iff divide_complex_def + distrib_left distrib_right right_diff_distrib left_diff_distrib + power2_eq_square add_divide_distrib [symmetric]) end +lemma Re_divide: "Re (x / y) = (Re x * Re y + Im x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2)" + unfolding divide_complex_def by (simp add: add_divide_distrib) -subsection {* Numerals and Arithmetic *} +lemma Im_divide: "Im (x / y) = (Im x * Re y - Re x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2)" + unfolding divide_complex_def times_complex.sel inverse_complex.sel + by (simp_all add: divide_simps) -lemma complex_Re_of_nat [simp]: "Re (of_nat n) = of_nat n" - by (induct n) simp_all +lemma Re_power2: "Re (x ^ 2) = (Re x)^2 - (Im x)^2" + by (simp add: power2_eq_square) -lemma complex_Im_of_nat [simp]: "Im (of_nat n) = 0" +lemma Im_power2: "Im (x ^ 2) = 2 * Re x * Im x" + by (simp add: power2_eq_square) + +lemma Re_power_real: "Im x = 0 \ Re (x ^ n) = Re x ^ n " by (induct n) simp_all -lemma complex_Re_of_int [simp]: "Re (of_int z) = of_int z" - by (cases z rule: int_diff_cases) simp - -lemma complex_Im_of_int [simp]: "Im (of_int z) = 0" - by (cases z rule: int_diff_cases) simp - -lemma complex_Re_numeral [simp]: "Re (numeral v) = numeral v" - using complex_Re_of_int [of "numeral v"] by simp - -lemma complex_Re_neg_numeral [simp]: "Re (- numeral v) = - numeral v" - using complex_Re_of_int [of "- numeral v"] by simp - -lemma complex_Im_numeral [simp]: "Im (numeral v) = 0" - using complex_Im_of_int [of "numeral v"] by simp - -lemma complex_Im_neg_numeral [simp]: "Im (- numeral v) = 0" - using complex_Im_of_int [of "- numeral v"] by simp - -lemma Complex_eq_numeral [simp]: - "Complex a b = numeral w \ a = numeral w \ b = 0" - by (simp add: complex_eq_iff) - -lemma Complex_eq_neg_numeral [simp]: - "Complex a b = - numeral w \ a = - numeral w \ b = 0" - by (simp add: complex_eq_iff) - +lemma Im_power_real: "Im x = 0 \ Im (x ^ n) = 0" + by (induct n) simp_all subsection {* Scalar Multiplication *} instantiation complex :: real_field begin -definition complex_scaleR_def: - "scaleR r x = Complex (r * Re x) (r * Im x)" - -lemma complex_scaleR [simp]: - "scaleR r (Complex a b) = Complex (r * a) (r * b)" - unfolding complex_scaleR_def by simp - -lemma complex_Re_scaleR [simp]: "Re (scaleR r x) = r * Re x" - unfolding complex_scaleR_def by simp - -lemma complex_Im_scaleR [simp]: "Im (scaleR r x) = r * Im x" - unfolding complex_scaleR_def by simp +primcorec scaleR_complex where + "Re (scaleR r x) = r * Re x" +| "Im (scaleR r x) = r * Im x" instance proof @@ -226,55 +129,84 @@ end - -subsection{* Properties of Embedding from Reals *} +subsection {* Numerals, Arithmetic, and Embedding from Reals *} abbreviation complex_of_real :: "real \ complex" where "complex_of_real \ of_real" declare [[coercion complex_of_real]] +declare [[coercion "of_int :: int \ complex"]] +declare [[coercion "of_nat :: nat \ complex"]] -lemma complex_of_real_def: "complex_of_real r = Complex r 0" - by (simp add: of_real_def complex_scaleR_def) +lemma complex_Re_of_nat [simp]: "Re (of_nat n) = of_nat n" + by (induct n) simp_all + +lemma complex_Im_of_nat [simp]: "Im (of_nat n) = 0" + by (induct n) simp_all + +lemma complex_Re_of_int [simp]: "Re (of_int z) = of_int z" + by (cases z rule: int_diff_cases) simp + +lemma complex_Im_of_int [simp]: "Im (of_int z) = 0" + by (cases z rule: int_diff_cases) simp + +lemma complex_Re_numeral [simp]: "Re (numeral v) = numeral v" + using complex_Re_of_int [of "numeral v"] by simp + +lemma complex_Im_numeral [simp]: "Im (numeral v) = 0" + using complex_Im_of_int [of "numeral v"] by simp lemma Re_complex_of_real [simp]: "Re (complex_of_real z) = z" - by (simp add: complex_of_real_def) + by (simp add: of_real_def) lemma Im_complex_of_real [simp]: "Im (complex_of_real z) = 0" - by (simp add: complex_of_real_def) + by (simp add: of_real_def) + +subsection {* The Complex Number $i$ *} + +primcorec "ii" :: complex ("\") where + "Re ii = 0" +| "Im ii = 1" -lemma Complex_add_complex_of_real [simp]: - shows "Complex x y + complex_of_real r = Complex (x+r) y" - by (simp add: complex_of_real_def) +lemma i_squared [simp]: "ii * ii = -1" + by (simp add: complex_eq_iff) + +lemma power2_i [simp]: "ii\<^sup>2 = -1" + by (simp add: power2_eq_square) -lemma complex_of_real_add_Complex [simp]: - shows "complex_of_real r + Complex x y = Complex (r+x) y" - by (simp add: complex_of_real_def) +lemma inverse_i [simp]: "inverse ii = - ii" + by (rule inverse_unique) simp + +lemma divide_i [simp]: "x / ii = - ii * x" + by (simp add: divide_complex_def) -lemma Complex_mult_complex_of_real: - shows "Complex x y * complex_of_real r = Complex (x*r) (y*r)" - by (simp add: complex_of_real_def) +lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x" + by (simp add: mult_assoc [symmetric]) -lemma complex_of_real_mult_Complex: - shows "complex_of_real r * Complex x y = Complex (r*x) (r*y)" - by (simp add: complex_of_real_def) +lemma Complex_eq[simp]: "Complex a b = a + \ * b" + by (simp add: complex_eq_iff) + +lemma complex_i_not_zero [simp]: "ii \ 0" + by (simp add: complex_eq_iff) -lemma complex_eq_cancel_iff2 [simp]: - shows "(Complex x y = complex_of_real xa) = (x = xa & y = 0)" - by (simp add: complex_of_real_def) +lemma complex_i_not_one [simp]: "ii \ 1" + by (simp add: complex_eq_iff) + +lemma complex_i_not_numeral [simp]: "ii \ numeral w" + by (simp add: complex_eq_iff) -lemma complex_split_polar: - "\r a. z = complex_of_real r * (Complex (cos a) (sin a))" +lemma complex_i_not_neg_numeral [simp]: "ii \ - numeral w" + by (simp add: complex_eq_iff) + +lemma complex_split_polar: "\r a. z = complex_of_real r * (cos a + \ * sin a)" by (simp add: complex_eq_iff polar_Ex) - subsection {* Vector Norm *} instantiation complex :: real_normed_field begin -definition complex_norm_def: - "norm z = sqrt ((Re z)\<^sup>2 + (Im z)\<^sup>2)" +definition "norm z = sqrt ((Re z)\<^sup>2 + (Im z)\<^sup>2)" abbreviation cmod :: "complex \ real" where "cmod \ norm" @@ -288,57 +220,60 @@ definition open_complex_def: "open (S :: complex set) \ (\x\S. \e>0. \y. dist y x < e \ y \ S)" -lemmas cmod_def = complex_norm_def - -lemma complex_norm [simp]: "cmod (Complex x y) = sqrt (x\<^sup>2 + y\<^sup>2)" - by (simp add: complex_norm_def) - instance proof fix r :: real and x y :: complex and S :: "complex set" show "(norm x = 0) = (x = 0)" - by (induct x) simp + by (simp add: norm_complex_def complex_eq_iff) show "norm (x + y) \ norm x + norm y" - by (induct x, induct y) - (simp add: real_sqrt_sum_squares_triangle_ineq) + by (simp add: norm_complex_def complex_eq_iff real_sqrt_sum_squares_triangle_ineq) show "norm (scaleR r x) = \r\ * norm x" - by (induct x) - (simp add: power_mult_distrib distrib_left [symmetric] real_sqrt_mult) + by (simp add: norm_complex_def complex_eq_iff power_mult_distrib distrib_left [symmetric] real_sqrt_mult) show "norm (x * y) = norm x * norm y" - by (induct x, induct y) - (simp add: real_sqrt_mult [symmetric] power2_eq_square algebra_simps) - show "sgn x = x /\<^sub>R cmod x" - by (rule complex_sgn_def) - show "dist x y = cmod (x - y)" - by (rule dist_complex_def) - show "open S \ (\x\S. \e>0. \y. dist y x < e \ y \ S)" - by (rule open_complex_def) -qed + by (simp add: norm_complex_def complex_eq_iff real_sqrt_mult [symmetric] power2_eq_square algebra_simps) +qed (rule complex_sgn_def dist_complex_def open_complex_def)+ end -lemma cmod_unit_one: "cmod (Complex (cos a) (sin a)) = 1" - by simp +lemma norm_ii [simp]: "norm ii = 1" + by (simp add: norm_complex_def) -lemma cmod_complex_polar: - "cmod (complex_of_real r * Complex (cos a) (sin a)) = abs r" - by (simp add: norm_mult) +lemma cmod_unit_one: "cmod (cos a + \ * sin a) = 1" + by (simp add: norm_complex_def) + +lemma cmod_complex_polar: "cmod (r * (cos a + \ * sin a)) = \r\" + by (simp add: norm_mult cmod_unit_one) lemma complex_Re_le_cmod: "Re x \ cmod x" - unfolding complex_norm_def + unfolding norm_complex_def by (rule real_sqrt_sum_squares_ge1) lemma complex_mod_minus_le_complex_mod: "- cmod x \ cmod x" - by (rule order_trans [OF _ norm_ge_zero], simp) + by (rule order_trans [OF _ norm_ge_zero]) simp -lemma complex_mod_triangle_ineq2: "cmod(b + a) - cmod b \ cmod a" - by (rule ord_le_eq_trans [OF norm_triangle_ineq2], simp) +lemma complex_mod_triangle_ineq2: "cmod (b + a) - cmod b \ cmod a" + by (rule ord_le_eq_trans [OF norm_triangle_ineq2]) simp lemma abs_Re_le_cmod: "\Re x\ \ cmod x" - by (cases x) simp + by (simp add: norm_complex_def) lemma abs_Im_le_cmod: "\Im x\ \ cmod x" - by (cases x) simp + by (simp add: norm_complex_def) + +lemma cmod_eq_Re: "Im z = 0 \ cmod z = \Re z\" + by (simp add: norm_complex_def) + +lemma cmod_eq_Im: "Re z = 0 \ cmod z = \Im z\" + by (simp add: norm_complex_def) +lemma cmod_power2: "cmod z ^ 2 = (Re z)^2 + (Im z)^2" + by (simp add: norm_complex_def) + +lemma cmod_plus_Re_le_0_iff: "cmod z + Re z \ 0 \ Re z = - cmod z" + using abs_Re_le_cmod[of z] by auto + +lemma Im_eq_0: "\Re z\ = cmod z \ Im z = 0" + by (subst (asm) power_eq_iff_eq_base[symmetric, where n=2]) + (auto simp add: norm_complex_def) lemma abs_sqrt_wlog: fixes x::"'a::linordered_idom" @@ -346,7 +281,7 @@ by (metis abs_ge_zero assms power2_abs) lemma complex_abs_le_norm: "\Re z\ + \Im z\ \ sqrt 2 * norm z" - unfolding complex_norm_def + unfolding norm_complex_def apply (rule abs_sqrt_wlog [where x="Re z"]) apply (rule abs_sqrt_wlog [where x="Im z"]) apply (rule power2_le_imp_le) @@ -369,10 +304,10 @@ subsection {* Completeness of the Complexes *} lemma bounded_linear_Re: "bounded_linear Re" - by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def) + by (rule bounded_linear_intro [where K=1], simp_all add: norm_complex_def) lemma bounded_linear_Im: "bounded_linear Im" - by (rule bounded_linear_intro [where K=1], simp_all add: complex_norm_def) + by (rule bounded_linear_intro [where K=1], simp_all add: norm_complex_def) lemmas Cauchy_Re = bounded_linear.Cauchy [OF bounded_linear_Re] lemmas Cauchy_Im = bounded_linear.Cauchy [OF bounded_linear_Im] @@ -390,127 +325,41 @@ lemmas sums_Im = bounded_linear.sums [OF bounded_linear_Im] lemma tendsto_Complex [tendsto_intros]: - assumes "(f ---> a) F" and "(g ---> b) F" - shows "((\x. Complex (f x) (g x)) ---> Complex a b) F" -proof (rule tendstoI) - fix r :: real assume "0 < r" - hence "0 < r / sqrt 2" by simp - have "eventually (\x. dist (f x) a < r / sqrt 2) F" - using `(f ---> a) F` and `0 < r / sqrt 2` by (rule tendstoD) - moreover - have "eventually (\x. dist (g x) b < r / sqrt 2) F" - using `(g ---> b) F` and `0 < r / sqrt 2` by (rule tendstoD) - ultimately - show "eventually (\x. dist (Complex (f x) (g x)) (Complex a b) < r) F" - by (rule eventually_elim2) - (simp add: dist_norm real_sqrt_sum_squares_less) -qed - + "(f ---> a) F \ (g ---> b) F \ ((\x. Complex (f x) (g x)) ---> Complex a b) F" + by (auto intro!: tendsto_intros) lemma tendsto_complex_iff: "(f ---> x) F \ (((\x. Re (f x)) ---> Re x) F \ ((\x. Im (f x)) ---> Im x) F)" -proof - - have f: "f = (\x. Complex (Re (f x)) (Im (f x)))" and x: "x = Complex (Re x) (Im x)" - by simp_all - show ?thesis - apply (subst f) - apply (subst x) - apply (intro iffI tendsto_Complex conjI) - apply (simp_all add: tendsto_Re tendsto_Im) - done -qed +proof safe + assume "((\x. Re (f x)) ---> Re x) F" "((\x. Im (f x)) ---> Im x) F" + from tendsto_Complex[OF this] show "(f ---> x) F" + unfolding complex.collapse . +qed (auto intro: tendsto_intros) instance complex :: banach proof fix X :: "nat \ complex" assume X: "Cauchy X" - from Cauchy_Re [OF X] have 1: "(\n. Re (X n)) ----> lim (\n. Re (X n))" - by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) - from Cauchy_Im [OF X] have 2: "(\n. Im (X n)) ----> lim (\n. Im (X n))" - by (simp add: Cauchy_convergent_iff convergent_LIMSEQ_iff) - have "X ----> Complex (lim (\n. Re (X n))) (lim (\n. Im (X n)))" - using tendsto_Complex [OF 1 2] by simp - thus "convergent X" - by (rule convergentI) + then have "(\n. Complex (Re (X n)) (Im (X n))) ----> Complex (lim (\n. Re (X n))) (lim (\n. Im (X n)))" + by (intro tendsto_Complex convergent_LIMSEQ_iff[THEN iffD1] Cauchy_convergent_iff[THEN iffD1] Cauchy_Re Cauchy_Im) + then show "convergent X" + unfolding complex.collapse by (rule convergentI) qed declare DERIV_power[where 'a=complex, unfolded of_nat_def[symmetric], derivative_intros] - -subsection {* The Complex Number $i$ *} - -definition "ii" :: complex ("\") - where i_def: "ii \ Complex 0 1" - -lemma complex_Re_i [simp]: "Re ii = 0" - by (simp add: i_def) - -lemma complex_Im_i [simp]: "Im ii = 1" - by (simp add: i_def) - -lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 \ y = 1)" - by (simp add: i_def) - -lemma norm_ii [simp]: "norm ii = 1" - by (simp add: i_def) - -lemma complex_i_not_zero [simp]: "ii \ 0" - by (simp add: complex_eq_iff) - -lemma complex_i_not_one [simp]: "ii \ 1" - by (simp add: complex_eq_iff) - -lemma complex_i_not_numeral [simp]: "ii \ numeral w" - by (simp add: complex_eq_iff) - -lemma complex_i_not_neg_numeral [simp]: "ii \ - numeral w" - by (simp add: complex_eq_iff) - -lemma i_mult_Complex [simp]: "ii * Complex a b = Complex (- b) a" - by (simp add: complex_eq_iff) - -lemma Complex_mult_i [simp]: "Complex a b * ii = Complex (- b) a" - by (simp add: complex_eq_iff) - -lemma i_complex_of_real [simp]: "ii * complex_of_real r = Complex 0 r" - by (simp add: i_def complex_of_real_def) - -lemma complex_of_real_i [simp]: "complex_of_real r * ii = Complex 0 r" - by (simp add: i_def complex_of_real_def) - -lemma i_squared [simp]: "ii * ii = -1" - by (simp add: i_def) - -lemma power2_i [simp]: "ii\<^sup>2 = -1" - by (simp add: power2_eq_square) - -lemma inverse_i [simp]: "inverse ii = - ii" - by (rule inverse_unique, simp) - -lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x" - by (simp add: mult_assoc [symmetric]) - - subsection {* Complex Conjugation *} -definition cnj :: "complex \ complex" where - "cnj z = Complex (Re z) (- Im z)" - -lemma complex_cnj [simp]: "cnj (Complex a b) = Complex a (- b)" - by (simp add: cnj_def) - -lemma complex_Re_cnj [simp]: "Re (cnj x) = Re x" - by (simp add: cnj_def) - -lemma complex_Im_cnj [simp]: "Im (cnj x) = - Im x" - by (simp add: cnj_def) +primcorec cnj :: "complex \ complex" where + "Re (cnj z) = Re z" +| "Im (cnj z) = - Im z" lemma complex_cnj_cancel_iff [simp]: "(cnj x = cnj y) = (x = y)" by (simp add: complex_eq_iff) lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z" - by (simp add: cnj_def) + by (simp add: complex_eq_iff) lemma complex_cnj_zero [simp]: "cnj 0 = 0" by (simp add: complex_eq_iff) @@ -518,35 +367,35 @@ lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)" by (simp add: complex_eq_iff) -lemma complex_cnj_add: "cnj (x + y) = cnj x + cnj y" +lemma complex_cnj_add [simp]: "cnj (x + y) = cnj x + cnj y" by (simp add: complex_eq_iff) -lemma cnj_setsum: "cnj (setsum f s) = (\x\s. cnj (f x))" - by (induct s rule: infinite_finite_induct) (auto simp: complex_cnj_add) +lemma cnj_setsum [simp]: "cnj (setsum f s) = (\x\s. cnj (f x))" + by (induct s rule: infinite_finite_induct) auto -lemma complex_cnj_diff: "cnj (x - y) = cnj x - cnj y" +lemma complex_cnj_diff [simp]: "cnj (x - y) = cnj x - cnj y" by (simp add: complex_eq_iff) -lemma complex_cnj_minus: "cnj (- x) = - cnj x" +lemma complex_cnj_minus [simp]: "cnj (- x) = - cnj x" by (simp add: complex_eq_iff) lemma complex_cnj_one [simp]: "cnj 1 = 1" by (simp add: complex_eq_iff) -lemma complex_cnj_mult: "cnj (x * y) = cnj x * cnj y" +lemma complex_cnj_mult [simp]: "cnj (x * y) = cnj x * cnj y" by (simp add: complex_eq_iff) -lemma cnj_setprod: "cnj (setprod f s) = (\x\s. cnj (f x))" - by (induct s rule: infinite_finite_induct) (auto simp: complex_cnj_mult) +lemma cnj_setprod [simp]: "cnj (setprod f s) = (\x\s. cnj (f x))" + by (induct s rule: infinite_finite_induct) auto -lemma complex_cnj_inverse: "cnj (inverse x) = inverse (cnj x)" - by (simp add: complex_inverse_def) +lemma complex_cnj_inverse [simp]: "cnj (inverse x) = inverse (cnj x)" + by (simp add: complex_eq_iff) -lemma complex_cnj_divide: "cnj (x / y) = cnj x / cnj y" - by (simp add: complex_divide_def complex_cnj_mult complex_cnj_inverse) +lemma complex_cnj_divide [simp]: "cnj (x / y) = cnj x / cnj y" + by (simp add: divide_complex_def) -lemma complex_cnj_power: "cnj (x ^ n) = cnj x ^ n" - by (induct n, simp_all add: complex_cnj_mult) +lemma complex_cnj_power [simp]: "cnj (x ^ n) = cnj x ^ n" + by (induct n) simp_all lemma complex_cnj_of_nat [simp]: "cnj (of_nat n) = of_nat n" by (simp add: complex_eq_iff) @@ -560,11 +409,11 @@ lemma complex_cnj_neg_numeral [simp]: "cnj (- numeral w) = - numeral w" by (simp add: complex_eq_iff) -lemma complex_cnj_scaleR: "cnj (scaleR r x) = scaleR r (cnj x)" +lemma complex_cnj_scaleR [simp]: "cnj (scaleR r x) = scaleR r (cnj x)" by (simp add: complex_eq_iff) lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z" - by (simp add: complex_norm_def) + by (simp add: norm_complex_def) lemma complex_cnj_complex_of_real [simp]: "cnj (of_real x) = of_real x" by (simp add: complex_eq_iff) @@ -585,7 +434,7 @@ by (simp add: norm_mult power2_eq_square) lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))" - by (simp add: cmod_def power2_eq_square) + by (simp add: norm_complex_def power2_eq_square) lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0" by simp @@ -601,70 +450,46 @@ lemmas has_derivative_cnj [simp, derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_cnj] lemma lim_cnj: "((\x. cnj(f x)) ---> cnj l) F \ (f ---> l) F" - by (simp add: tendsto_iff dist_complex_def Complex.complex_cnj_diff [symmetric]) + by (simp add: tendsto_iff dist_complex_def complex_cnj_diff [symmetric] del: complex_cnj_diff) lemma sums_cnj: "((\x. cnj(f x)) sums cnj l) \ (f sums l)" - by (simp add: sums_def lim_cnj cnj_setsum [symmetric]) + by (simp add: sums_def lim_cnj cnj_setsum [symmetric] del: cnj_setsum) subsection{*Basic Lemmas*} lemma complex_eq_0: "z=0 \ (Re z)\<^sup>2 + (Im z)\<^sup>2 = 0" - by (metis complex_Im_zero complex_Re_zero complex_eqI sum_power2_eq_zero_iff) + by (metis zero_complex.sel complex_eqI sum_power2_eq_zero_iff) lemma complex_neq_0: "z\0 \ (Re z)\<^sup>2 + (Im z)\<^sup>2 > 0" -by (metis complex_eq_0 less_numeral_extra(3) sum_power2_gt_zero_iff) + by (metis complex_eq_0 less_numeral_extra(3) sum_power2_gt_zero_iff) lemma complex_norm_square: "of_real ((norm z)\<^sup>2) = z * cnj z" -apply (cases z, auto) -by (metis complex_of_real_def of_real_add of_real_power power2_eq_square) +by (cases z) + (auto simp: complex_eq_iff norm_complex_def power2_eq_square[symmetric] of_real_power[symmetric] + simp del: of_real_power) -lemma complex_div_eq_0: - "(Re(a / b) = 0 \ Re(a * cnj b) = 0) & (Im(a / b) = 0 \ Im(a * cnj b) = 0)" -proof (cases "b=0") - case True then show ?thesis by auto +lemma re_complex_div_eq_0: "Re (a / b) = 0 \ Re (a * cnj b) = 0" + by (auto simp add: Re_divide) + +lemma im_complex_div_eq_0: "Im (a / b) = 0 \ Im (a * cnj b) = 0" + by (auto simp add: Im_divide) + +lemma complex_div_gt_0: + "(Re (a / b) > 0 \ Re (a * cnj b) > 0) \ (Im (a / b) > 0 \ Im (a * cnj b) > 0)" +proof cases + assume "b = 0" then show ?thesis by auto next - case False - show ?thesis - proof (cases b) - case (Complex x y) - then have "x\<^sup>2 + y\<^sup>2 > 0" - by (metis Complex_eq_0 False sum_power2_gt_zero_iff) - then have "!!u v. u / (x\<^sup>2 + y\<^sup>2) + v / (x\<^sup>2 + y\<^sup>2) = (u + v) / (x\<^sup>2 + y\<^sup>2)" - by (metis add_divide_distrib) - with Complex False show ?thesis - by (auto simp: complex_divide_def) - qed + assume "b \ 0" + then have "0 < (Re b)\<^sup>2 + (Im b)\<^sup>2" + by (simp add: complex_eq_iff sum_power2_gt_zero_iff) + then show ?thesis + by (simp add: Re_divide Im_divide zero_less_divide_iff) qed -lemma re_complex_div_eq_0: "Re(a / b) = 0 \ Re(a * cnj b) = 0" - and im_complex_div_eq_0: "Im(a / b) = 0 \ Im(a * cnj b) = 0" -using complex_div_eq_0 by auto - - -lemma complex_div_gt_0: - "(Re(a / b) > 0 \ Re(a * cnj b) > 0) & (Im(a / b) > 0 \ Im(a * cnj b) > 0)" -proof (cases "b=0") - case True then show ?thesis by auto -next - case False - show ?thesis - proof (cases b) - case (Complex x y) - then have "x\<^sup>2 + y\<^sup>2 > 0" - by (metis Complex_eq_0 False sum_power2_gt_zero_iff) - moreover have "!!u v. u / (x\<^sup>2 + y\<^sup>2) + v / (x\<^sup>2 + y\<^sup>2) = (u + v) / (x\<^sup>2 + y\<^sup>2)" - by (metis add_divide_distrib) - ultimately show ?thesis using Complex False `0 < x\<^sup>2 + y\<^sup>2` - apply (simp add: complex_divide_def zero_less_divide_iff less_divide_eq) - apply (metis less_divide_eq mult_zero_left diff_conv_add_uminus minus_divide_left) - done - qed -qed - -lemma re_complex_div_gt_0: "Re(a / b) > 0 \ Re(a * cnj b) > 0" - and im_complex_div_gt_0: "Im(a / b) > 0 \ Im(a * cnj b) > 0" -using complex_div_gt_0 by auto +lemma re_complex_div_gt_0: "Re (a / b) > 0 \ Re (a * cnj b) > 0" + and im_complex_div_gt_0: "Im (a / b) > 0 \ Im (a * cnj b) > 0" + using complex_div_gt_0 by auto lemma re_complex_div_ge_0: "Re(a / b) \ 0 \ Re(a * cnj b) \ 0" by (metis le_less re_complex_div_eq_0 re_complex_div_gt_0) @@ -684,17 +509,17 @@ lemma im_complex_div_le_0: "Im(a / b) \ 0 \ Im(a * cnj b) \ 0" by (metis im_complex_div_gt_0 not_le) -lemma Re_setsum: "Re(setsum f s) = setsum (%x. Re(f x)) s" +lemma Re_setsum[simp]: "Re (setsum f s) = (\x\s. Re (f x))" by (induct s rule: infinite_finite_induct) auto -lemma Im_setsum: "Im(setsum f s) = setsum (%x. Im(f x)) s" +lemma Im_setsum[simp]: "Im (setsum f s) = (\x\s. Im(f x))" by (induct s rule: infinite_finite_induct) auto lemma sums_complex_iff: "f sums x \ ((\x. Re (f x)) sums Re x) \ ((\x. Im (f x)) sums Im x)" unfolding sums_def tendsto_complex_iff Im_setsum Re_setsum .. lemma summable_complex_iff: "summable f \ summable (\x. Re (f x)) \ summable (\x. Im (f x))" - unfolding summable_def sums_complex_iff[abs_def] by (metis Im.simps Re.simps) + unfolding summable_def sums_complex_iff[abs_def] by (metis complex.sel) lemma summable_complex_of_real [simp]: "summable (\n. complex_of_real (f n)) \ summable f" unfolding summable_complex_iff by simp @@ -705,30 +530,14 @@ lemma summable_Im: "summable f \ summable (\x. Im (f x))" unfolding summable_complex_iff by blast -lemma Complex_setsum': "setsum (%x. Complex (f x) 0) s = Complex (setsum f s) 0" - by (induct s rule: infinite_finite_induct) auto - -lemma Complex_setsum: "Complex (setsum f s) 0 = setsum (%x. Complex (f x) 0) s" - by (metis Complex_setsum') - -lemma of_real_setsum: "of_real (setsum f s) = setsum (%x. of_real(f x)) s" - by (induct s rule: infinite_finite_induct) auto - -lemma of_real_setprod: "of_real (setprod f s) = setprod (%x. of_real(f x)) s" - by (induct s rule: infinite_finite_induct) auto +lemma complex_is_Real_iff: "z \ \ \ Im z = 0" + by (auto simp: Reals_def complex_eq_iff) lemma Reals_cnj_iff: "z \ \ \ cnj z = z" -by (metis Reals_cases Reals_of_real complex.exhaust complex.inject complex_cnj - complex_of_real_def equal_neg_zero) - -lemma Complex_in_Reals: "Complex x 0 \ \" - by (metis Reals_of_real complex_of_real_def) + by (auto simp: complex_is_Real_iff complex_eq_iff) lemma in_Reals_norm: "z \ \ \ norm(z) = abs(Re z)" - by (metis Re_complex_of_real Reals_cases norm_of_real) - -lemma complex_is_Real_iff: "z \ \ \ Im z = 0" - by (metis Complex_in_Reals Im_complex_of_real Reals_cases complex_surj) + by (simp add: complex_is_Real_iff norm_complex_def) lemma series_comparison_complex: fixes f:: "nat \ 'a::banach" @@ -753,20 +562,15 @@ subsubsection {* $\cos \theta + i \sin \theta$ *} -definition cis :: "real \ complex" where - "cis a = Complex (cos a) (sin a)" - -lemma Re_cis [simp]: "Re (cis a) = cos a" - by (simp add: cis_def) - -lemma Im_cis [simp]: "Im (cis a) = sin a" - by (simp add: cis_def) +primcorec cis :: "real \ complex" where + "Re (cis a) = cos a" +| "Im (cis a) = sin a" lemma cis_zero [simp]: "cis 0 = 1" - by (simp add: cis_def) + by (simp add: complex_eq_iff) lemma norm_cis [simp]: "norm (cis a) = 1" - by (simp add: cis_def) + by (simp add: norm_complex_def) lemma sgn_cis [simp]: "sgn (cis a) = cis a" by (simp add: sgn_div_norm) @@ -775,16 +579,16 @@ by (metis norm_cis norm_zero zero_neq_one) lemma cis_mult: "cis a * cis b = cis (a + b)" - by (simp add: cis_def cos_add sin_add) + by (simp add: complex_eq_iff cos_add sin_add) lemma DeMoivre: "(cis a) ^ n = cis (real n * a)" by (induct n, simp_all add: real_of_nat_Suc algebra_simps cis_mult) lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)" - by (simp add: cis_def) + by (simp add: complex_eq_iff) lemma cis_divide: "cis a / cis b = cis (a - b)" - by (simp add: complex_divide_def cis_mult) + by (simp add: divide_complex_def cis_mult) lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)" by (auto simp add: DeMoivre) @@ -792,9 +596,12 @@ lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)" by (auto simp add: DeMoivre) +lemma cis_pi: "cis pi = -1" + by (simp add: complex_eq_iff) + subsubsection {* $r(\cos \theta + i \sin \theta)$ *} -definition rcis :: "[real, real] \ complex" where +definition rcis :: "real \ real \ complex" where "rcis r a = complex_of_real r * cis a" lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a" @@ -838,26 +645,24 @@ abbreviation expi :: "complex \ complex" where "expi \ exp" -lemma cis_conv_exp: "cis b = exp (Complex 0 b)" -proof (rule complex_eqI) - { fix n have "Complex 0 b ^ n = - real (fact n) *\<^sub>R Complex (cos_coeff n * b ^ n) (sin_coeff n * b ^ n)" - apply (induct n) - apply (simp add: cos_coeff_def sin_coeff_def) - apply (simp add: sin_coeff_Suc cos_coeff_Suc del: mult_Suc) - done } note * = this - show "Re (cis b) = Re (exp (Complex 0 b))" - unfolding exp_def cis_def cos_def - by (subst bounded_linear.suminf[OF bounded_linear_Re summable_exp_generic], - simp add: * mult_assoc [symmetric]) - show "Im (cis b) = Im (exp (Complex 0 b))" - unfolding exp_def cis_def sin_def - by (subst bounded_linear.suminf[OF bounded_linear_Im summable_exp_generic], - simp add: * mult_assoc [symmetric]) +lemma cis_conv_exp: "cis b = exp (\ * b)" +proof - + { fix n :: nat + have "\ ^ n = fact n *\<^sub>R (cos_coeff n + \ * sin_coeff n)" + by (induct n) + (simp_all add: sin_coeff_Suc cos_coeff_Suc complex_eq_iff Re_divide Im_divide field_simps + power2_eq_square real_of_nat_Suc add_nonneg_eq_0_iff + real_of_nat_def[symmetric]) + then have "(\ * complex_of_real b) ^ n /\<^sub>R fact n = + of_real (cos_coeff n * b^n) + \ * of_real (sin_coeff n * b^n)" + by (simp add: field_simps) } + then show ?thesis + by (auto simp add: cis.ctr exp_def simp del: of_real_mult + intro!: sums_unique sums_add sums_mult sums_of_real sin_converges cos_converges) qed -lemma expi_def: "expi z = complex_of_real (exp (Re z)) * cis (Im z)" - unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp by simp +lemma expi_def: "expi z = exp (Re z) * cis (Im z)" + unfolding cis_conv_exp exp_of_real [symmetric] mult_exp_exp by (cases z) simp lemma Re_exp: "Re (exp z) = exp (Re z) * cos (Im z)" unfolding expi_def by simp @@ -872,7 +677,7 @@ done lemma expi_two_pi_i [simp]: "expi((2::complex) * complex_of_real pi * ii) = 1" - by (simp add: expi_def cis_def) + by (simp add: expi_def complex_eq_iff) subsubsection {* Complex argument *} @@ -882,15 +687,6 @@ lemma arg_zero: "arg 0 = 0" by (simp add: arg_def) -lemma of_nat_less_of_int_iff: (* TODO: move *) - "(of_nat n :: 'a::linordered_idom) < of_int x \ int n < x" - by (metis of_int_of_nat_eq of_int_less_iff) - -lemma real_of_nat_less_numeral_iff [simp]: (* TODO: move *) - "real (n::nat) < numeral w \ n < numeral w" - using of_nat_less_of_int_iff [of n "numeral w", where 'a=real] - by (simp add: real_of_nat_def zless_nat_eq_int_zless [symmetric]) - lemma arg_unique: assumes "sgn z = cis x" and "-pi < x" and "x \ pi" shows "arg z = x" @@ -923,13 +719,12 @@ def b \ "if 0 < r then a else a + pi" have b: "sgn z = cis b" unfolding z b_def rcis_def using `r \ 0` - by (simp add: of_real_def sgn_scaleR sgn_if, simp add: cis_def) + by (simp add: of_real_def sgn_scaleR sgn_if complex_eq_iff) have cis_2pi_nat: "\n. cis (2 * pi * real_of_nat n) = 1" - by (induct_tac n, simp_all add: distrib_left cis_mult [symmetric], - simp add: cis_def) + by (induct_tac n) (simp_all add: distrib_left cis_mult [symmetric] complex_eq_iff) have cis_2pi_int: "\x. cis (2 * pi * real_of_int x) = 1" - by (case_tac x rule: int_diff_cases, - simp add: right_diff_distrib cis_divide [symmetric] cis_2pi_nat) + by (case_tac x rule: int_diff_cases) + (simp add: right_diff_distrib cis_divide [symmetric] cis_2pi_nat) def c \ "b - 2*pi * of_int \(b - pi) / (2*pi)\" have "sgn z = cis c" unfolding b c_def @@ -941,22 +736,136 @@ qed lemma arg_bounded: "- pi < arg z \ arg z \ pi" - by (cases "z = 0", simp_all add: arg_zero arg_correct) + by (cases "z = 0") (simp_all add: arg_zero arg_correct) lemma cis_arg: "z \ 0 \ cis (arg z) = sgn z" by (simp add: arg_correct) lemma rcis_cmod_arg: "rcis (cmod z) (arg z) = z" - by (cases "z = 0", simp_all add: rcis_def cis_arg sgn_div_norm of_real_def) + by (cases "z = 0") (simp_all add: rcis_def cis_arg sgn_div_norm of_real_def) + +lemma cos_arg_i_mult_zero [simp]: "y \ 0 \ Re y = 0 \ cos (arg y) = 0" + using cis_arg [of y] by (simp add: complex_eq_iff) + +subsection {* Square root of complex numbers *} + +primcorec csqrt :: "complex \ complex" where + "Re (csqrt z) = sqrt ((cmod z + Re z) / 2)" +| "Im (csqrt z) = (if Im z = 0 then 1 else sgn (Im z)) * sqrt ((cmod z - Re z) / 2)" + +lemma csqrt_of_real_nonneg [simp]: "Im x = 0 \ Re x \ 0 \ csqrt x = sqrt (Re x)" + by (simp add: complex_eq_iff norm_complex_def) + +lemma csqrt_of_real_nonpos [simp]: "Im x = 0 \ Re x \ 0 \ csqrt x = \ * sqrt \Re x\" + by (simp add: complex_eq_iff norm_complex_def) + +lemma csqrt_0 [simp]: "csqrt 0 = 0" + by simp + +lemma csqrt_1 [simp]: "csqrt 1 = 1" + by simp + +lemma csqrt_ii [simp]: "csqrt \ = (1 + \) / sqrt 2" + by (simp add: complex_eq_iff Re_divide Im_divide real_sqrt_divide real_div_sqrt) -lemma cos_arg_i_mult_zero [simp]: - "y \ 0 ==> cos (arg(Complex 0 y)) = 0" - using cis_arg [of "Complex 0 y"] by (simp add: complex_eq_iff) +lemma power2_csqrt[algebra]: "(csqrt z)\<^sup>2 = z" +proof cases + assume "Im z = 0" then show ?thesis + using real_sqrt_pow2[of "Re z"] real_sqrt_pow2[of "- Re z"] + by (cases "0::real" "Re z" rule: linorder_cases) + (simp_all add: complex_eq_iff Re_power2 Im_power2 power2_eq_square cmod_eq_Re) +next + assume "Im z \ 0" + moreover + have "cmod z * cmod z - Re z * Re z = Im z * Im z" + by (simp add: norm_complex_def power2_eq_square) + moreover + have "\Re z\ \ cmod z" + by (simp add: norm_complex_def) + ultimately show ?thesis + by (simp add: Re_power2 Im_power2 complex_eq_iff real_sgn_eq + field_simps real_sqrt_mult[symmetric] real_sqrt_divide) +qed + +lemma csqrt_eq_0 [simp]: "csqrt z = 0 \ z = 0" + by auto (metis power2_csqrt power_eq_0_iff) + +lemma csqrt_eq_1 [simp]: "csqrt z = 1 \ z = 1" + by auto (metis power2_csqrt power2_eq_1_iff) + +lemma csqrt_principal: "0 < Re (csqrt z) \ Re (csqrt z) = 0 \ 0 \ Im (csqrt z)" + by (auto simp add: not_less cmod_plus_Re_le_0_iff Im_eq_0) + +lemma Re_csqrt: "0 \ Re (csqrt z)" + by (metis csqrt_principal le_less) + +lemma csqrt_square: + assumes "0 < Re b \ (Re b = 0 \ 0 \ Im b)" + shows "csqrt (b^2) = b" +proof - + have "csqrt (b^2) = b \ csqrt (b^2) = - b" + unfolding power2_eq_iff[symmetric] by (simp add: power2_csqrt) + moreover have "csqrt (b^2) \ -b \ b = 0" + using csqrt_principal[of "b ^ 2"] assms by (intro disjCI notI) (auto simp: complex_eq_iff) + ultimately show ?thesis + by auto +qed + +lemma csqrt_minus [simp]: + assumes "Im x < 0 \ (Im x = 0 \ 0 \ Re x)" + shows "csqrt (- x) = \ * csqrt x" +proof - + have "csqrt ((\ * csqrt x)^2) = \ * csqrt x" + proof (rule csqrt_square) + have "Im (csqrt x) \ 0" + using assms by (auto simp add: cmod_eq_Re mult_le_0_iff field_simps complex_Re_le_cmod) + then show "0 < Re (\ * csqrt x) \ Re (\ * csqrt x) = 0 \ 0 \ Im (\ * csqrt x)" + by (auto simp add: Re_csqrt simp del: csqrt.simps) + qed + also have "(\ * csqrt x)^2 = - x" + by (simp add: power2_csqrt power_mult_distrib) + finally show ?thesis . +qed text {* Legacy theorem names *} lemmas expand_complex_eq = complex_eq_iff lemmas complex_Re_Im_cancel_iff = complex_eq_iff lemmas complex_equality = complex_eqI +lemmas cmod_def = norm_complex_def +lemmas complex_norm_def = norm_complex_def +lemmas complex_divide_def = divide_complex_def + +lemma legacy_Complex_simps: + shows Complex_eq_0: "Complex a b = 0 \ a = 0 \ b = 0" + and complex_add: "Complex a b + Complex c d = Complex (a + c) (b + d)" + and complex_minus: "- (Complex a b) = Complex (- a) (- b)" + and complex_diff: "Complex a b - Complex c d = Complex (a - c) (b - d)" + and Complex_eq_1: "Complex a b = 1 \ a = 1 \ b = 0" + and Complex_eq_neg_1: "Complex a b = - 1 \ a = - 1 \ b = 0" + and complex_mult: "Complex a b * Complex c d = Complex (a * c - b * d) (a * d + b * c)" + and complex_inverse: "inverse (Complex a b) = Complex (a / (a\<^sup>2 + b\<^sup>2)) (- b / (a\<^sup>2 + b\<^sup>2))" + and Complex_eq_numeral: "Complex a b = numeral w \ a = numeral w \ b = 0" + and Complex_eq_neg_numeral: "Complex a b = - numeral w \ a = - numeral w \ b = 0" + and complex_scaleR: "scaleR r (Complex a b) = Complex (r * a) (r * b)" + and Complex_eq_i: "(Complex x y = ii) = (x = 0 \ y = 1)" + and i_mult_Complex: "ii * Complex a b = Complex (- b) a" + and Complex_mult_i: "Complex a b * ii = Complex (- b) a" + and i_complex_of_real: "ii * complex_of_real r = Complex 0 r" + and complex_of_real_i: "complex_of_real r * ii = Complex 0 r" + and Complex_add_complex_of_real: "Complex x y + complex_of_real r = Complex (x+r) y" + and complex_of_real_add_Complex: "complex_of_real r + Complex x y = Complex (r+x) y" + and Complex_mult_complex_of_real: "Complex x y * complex_of_real r = Complex (x*r) (y*r)" + and complex_of_real_mult_Complex: "complex_of_real r * Complex x y = Complex (r*x) (r*y)" + and complex_eq_cancel_iff2: "(Complex x y = complex_of_real xa) = (x = xa & y = 0)" + and complex_cn: "cnj (Complex a b) = Complex a (- b)" + and Complex_setsum': "setsum (%x. Complex (f x) 0) s = Complex (setsum f s) 0" + and Complex_setsum: "Complex (setsum f s) 0 = setsum (%x. Complex (f x) 0) s" + and complex_of_real_def: "complex_of_real r = Complex r 0" + and complex_norm: "cmod (Complex x y) = sqrt (x\<^sup>2 + y\<^sup>2)" + by (simp_all add: norm_complex_def field_simps complex_eq_iff Re_divide Im_divide del: Complex_eq) + +lemma Complex_in_Reals: "Complex x 0 \ \" + by (metis Reals_of_real complex_of_real_def) end diff -r 3e8cbb624cc5 -r 48a745e1bde7 src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Tue May 06 23:35:24 2014 +0200 +++ b/src/HOL/Decision_Procs/Approximation.thy Wed May 07 12:25:35 2014 +0200 @@ -235,8 +235,9 @@ from xt1(5)[OF `0 \ ?E mod 2` this] show ?thesis by auto qed - hence "sqrt (2 powr (?E mod 2)) < sqrt (2 * 2)" by auto - hence E_mod_pow: "sqrt (2 powr (?E mod 2)) < 2" unfolding real_sqrt_abs2 by auto + hence "sqrt (2 powr (?E mod 2)) < sqrt (2 * 2)" + by (auto simp del: real_sqrt_four) + hence E_mod_pow: "sqrt (2 powr (?E mod 2)) < 2" by auto have E_eq: "2 powr ?E = 2 powr (?E div 2 + ?E div 2 + ?E mod 2)" by auto have "sqrt (2 powr ?E) = sqrt (2 powr (?E div 2) * 2 powr (?E div 2) * 2 powr (?E mod 2))" diff -r 3e8cbb624cc5 -r 48a745e1bde7 src/HOL/Int.thy --- a/src/HOL/Int.thy Tue May 06 23:35:24 2014 +0200 +++ b/src/HOL/Int.thy Wed May 07 12:25:35 2014 +0200 @@ -293,6 +293,10 @@ end +lemma of_nat_less_of_int_iff: + "(of_nat n::'a::linordered_idom) < of_int x \ int n < x" + by (metis of_int_of_nat_eq of_int_less_iff) + lemma of_int_eq_id [simp]: "of_int = id" proof fix z show "of_int z = id z" diff -r 3e8cbb624cc5 -r 48a745e1bde7 src/HOL/Library/Extended_Real.thy --- a/src/HOL/Library/Extended_Real.thy Tue May 06 23:35:24 2014 +0200 +++ b/src/HOL/Library/Extended_Real.thy Wed May 07 12:25:35 2014 +0200 @@ -1894,7 +1894,7 @@ by (cases n) (auto dest: natceiling_le intro: natceiling_le_eq[THEN iffD1]) lemma numeral_less_ereal_of_enat_iff[simp]: "numeral m < ereal_of_enat n \ numeral m < n" - by (cases n) (auto simp: real_of_nat_less_iff[symmetric]) + by (cases n) auto lemma ereal_of_enat_ge_zero_cancel_iff[simp]: "0 \ ereal_of_enat n \ 0 \ n" by (cases n) (auto simp: enat_0[symmetric]) diff -r 3e8cbb624cc5 -r 48a745e1bde7 src/HOL/Library/Fundamental_Theorem_Algebra.thy --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy Tue May 06 23:35:24 2014 +0200 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy Wed May 07 12:25:35 2014 +0200 @@ -6,126 +6,12 @@ imports Polynomial Complex_Main begin -subsection {* Square root of complex numbers *} - -definition csqrt :: "complex \ complex" -where - "csqrt z = - (if Im z = 0 then - if 0 \ Re z then Complex (sqrt(Re z)) 0 - else Complex 0 (sqrt(- Re z)) - else Complex (sqrt((cmod z + Re z) /2)) ((Im z / abs(Im z)) * sqrt((cmod z - Re z) /2)))" - -lemma csqrt[algebra]: "(csqrt z)\<^sup>2 = z" -proof - - obtain x y where xy: "z = Complex x y" by (cases z) - { - assume y0: "y = 0" - { - assume x0: "x \ 0" - then have ?thesis - using y0 xy real_sqrt_pow2[OF x0] - by (simp add: csqrt_def power2_eq_square) - } - moreover - { - assume "\ x \ 0" - then have x0: "- x \ 0" by arith - then have ?thesis - using y0 xy real_sqrt_pow2[OF x0] - by (simp add: csqrt_def power2_eq_square) - } - ultimately have ?thesis by blast - } - moreover - { - assume y0: "y \ 0" - { - fix x y - let ?z = "Complex x y" - from abs_Re_le_cmod[of ?z] have tha: "abs x \ cmod ?z" - by auto - then have "cmod ?z - x \ 0" "cmod ?z + x \ 0" - by arith+ - then have "(sqrt (x * x + y * y) + x) / 2 \ 0" "(sqrt (x * x + y * y) - x) / 2 \ 0" - by (simp_all add: power2_eq_square) - } - note th = this - have sq4: "\x::real. x\<^sup>2 / 4 = (x / 2)\<^sup>2" - by (simp add: power2_eq_square) - from th[of x y] - have sq4': "sqrt (((sqrt (x * x + y * y) + x)\<^sup>2 / 4)) = (sqrt (x * x + y * y) + x) / 2" - "sqrt (((sqrt (x * x + y * y) - x)\<^sup>2 / 4)) = (sqrt (x * x + y * y) - x) / 2" - unfolding sq4 by simp_all - then have th1: "sqrt ((sqrt (x * x + y * y) + x) * (sqrt (x * x + y * y) + x) / 4) - - sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) - x) / 4) = x" - unfolding power2_eq_square by simp - have "sqrt 4 = sqrt (2\<^sup>2)" - by simp - then have sqrt4: "sqrt 4 = 2" - by (simp only: real_sqrt_abs) - have th2: "2 * (y * sqrt ((sqrt (x * x + y * y) - x) * (sqrt (x * x + y * y) + x) / 4)) / \y\ = y" - using iffD2[OF real_sqrt_pow2_iff sum_power2_ge_zero[of x y]] y0 - unfolding power2_eq_square - by (simp add: algebra_simps real_sqrt_divide sqrt4) - from y0 xy have ?thesis - apply (simp add: csqrt_def power2_eq_square) - apply (simp add: real_sqrt_sum_squares_mult_ge_zero[of x y] - real_sqrt_pow2[OF th(1)[of x y], unfolded power2_eq_square] - real_sqrt_pow2[OF th(2)[of x y], unfolded power2_eq_square] - real_sqrt_mult[symmetric]) - using th1 th2 .. - } - ultimately show ?thesis by blast -qed - -lemma csqrt_Complex: "x \ 0 \ csqrt (Complex x 0) = Complex (sqrt x) 0" - by (simp add: csqrt_def) - -lemma csqrt_0 [simp]: "csqrt 0 = 0" - by (simp add: csqrt_def) - -lemma csqrt_1 [simp]: "csqrt 1 = 1" - by (simp add: csqrt_def) - -lemma csqrt_principal: "0 < Re(csqrt(z)) | Re(csqrt(z)) = 0 & 0 \ Im(csqrt(z))" -proof (cases z) - case (Complex x y) - then show ?thesis - using real_sqrt_sum_squares_ge1 [of "x" y] - real_sqrt_sum_squares_ge1 [of "-x" y] - real_sqrt_sum_squares_eq_cancel [of x y] - apply (auto simp: csqrt_def intro!: Rings.ordered_ring_class.split_mult_pos_le) - apply (metis add_commute diff_add_cancel le_add_same_cancel1 real_sqrt_sum_squares_ge1) - apply (metis add_commute less_eq_real_def power_minus_Bit0 - real_0_less_add_iff real_sqrt_sum_squares_eq_cancel) - done -qed - -lemma Re_csqrt: "0 \ Re(csqrt z)" - by (metis csqrt_principal le_less) - -lemma csqrt_square: "0 < Re z \ Re z = 0 \ 0 \ Im z \ csqrt (z\<^sup>2) = z" - using csqrt [of "z\<^sup>2"] csqrt_principal [of "z\<^sup>2"] - by (cases z) (auto simp: power2_eq_iff) - -lemma csqrt_eq_0 [simp]: "csqrt z = 0 \ z = 0" - by auto (metis csqrt power_eq_0_iff) - -lemma csqrt_eq_1 [simp]: "csqrt z = 1 \ z = 1" - by auto (metis csqrt power2_eq_1_iff) - - subsection {* More lemmas about module of complex numbers *} -lemma complex_of_real_power: "complex_of_real x ^ n = complex_of_real (x^n)" - by (rule of_real_power [symmetric]) - text{* The triangle inequality for cmod *} lemma complex_mod_triangle_sub: "cmod w \ cmod (w + z) + norm z" using complex_mod_triangle_ineq2[of "w + z" "-z"] by auto - subsection {* Basic lemmas about polynomials *} lemma poly_bound_exists: @@ -281,7 +167,7 @@ with IH[rule_format, of m] obtain z where z: "?P z m" by blast from z have "?P (csqrt z) n" - by (simp add: m power_mult csqrt) + by (simp add: m power_mult power2_csqrt) then have "\z. ?P z n" .. } moreover @@ -319,7 +205,7 @@ let ?w = "v / complex_of_real (root n (cmod b))" from odd_real_root_pow[OF o, of "cmod b"] have th1: "?w ^ n = v^n / complex_of_real (cmod b)" - by (simp add: power_divide complex_of_real_power) + by (simp add: power_divide of_real_power[symmetric]) have th2:"cmod (complex_of_real (cmod b) / b) = 1" using b by (simp add: norm_divide) then have th3: "cmod (complex_of_real (cmod b) / b) \ 0" @@ -600,21 +486,6 @@ ultimately show ?thesis by blast qed -lemma "(rcis (sqrt (abs r)) (a/2))\<^sup>2 = rcis (abs r) a" - unfolding power2_eq_square - apply (simp add: rcis_mult) - apply (simp add: power2_eq_square[symmetric]) - done - -lemma cispi: "cis pi = -1" - by (simp add: cis_def) - -lemma "(rcis (sqrt (abs r)) ((pi + a) / 2))\<^sup>2 = rcis (- abs r) a" - unfolding power2_eq_square - apply (simp add: rcis_mult add_divide_distrib) - apply (simp add: power2_eq_square[symmetric] rcis_def cispi cis_mult[symmetric]) - done - text {* Nonzero polynomial in z goes to infinity as z does. *} lemma poly_infinity: diff -r 3e8cbb624cc5 -r 48a745e1bde7 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Tue May 06 23:35:24 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Wed May 07 12:25:35 2014 +0200 @@ -28,6 +28,7 @@ fixes c :: "'a::real_field" shows "of_nat (Suc n) * c / of_nat (fact (Suc n)) = c / of_nat (fact n)" by (simp add: of_nat_mult del: of_nat_Suc times_nat.simps) + lemma linear_times: fixes c::"'a::real_algebra" shows "linear (\x. c * x)" by (auto simp: linearI distrib_left) @@ -260,8 +261,8 @@ by (metis real_lim_sequentially setsum_in_Reals) lemma Lim_null_comparison_Re: - "eventually (\x. norm(f x) \ Re(g x)) F \ (g ---> 0) F \ (f ---> 0) F" - by (metis Lim_null_comparison complex_Re_zero tendsto_Re) + assumes "eventually (\x. norm(f x) \ Re(g x)) F" "(g ---> 0) F" shows "(f ---> 0) F" + by (rule Lim_null_comparison[OF assms(1)] tendsto_eq_intros assms(2))+ simp subsection{*Holomorphic functions*} diff -r 3e8cbb624cc5 -r 48a745e1bde7 src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Tue May 06 23:35:24 2014 +0200 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy Wed May 07 12:25:35 2014 +0200 @@ -3716,7 +3716,7 @@ where b: "\x\s. 0 < b x \ cball x (b x) \ s" using bchoice[of s "\x e. e > 0 \ cball x e \ s"] by auto have "b ` t \ {}" - unfolding i_def using obt by auto + using obt by auto def i \ "b ` t" show "\e > 0. diff -r 3e8cbb624cc5 -r 48a745e1bde7 src/HOL/NSA/CLim.thy --- a/src/HOL/NSA/CLim.thy Tue May 06 23:35:24 2014 +0200 +++ b/src/HOL/NSA/CLim.thy Wed May 07 12:25:35 2014 +0200 @@ -58,12 +58,12 @@ lemma LIM_cnj: fixes f :: "'a::real_normed_vector \ complex" shows "f -- a --> L ==> (%x. cnj (f x)) -- a --> cnj L" -by (simp add: LIM_eq complex_cnj_diff [symmetric]) +by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff) lemma LIM_cnj_iff: fixes f :: "'a::real_normed_vector \ complex" shows "((%x. cnj (f x)) -- a --> cnj L) = (f -- a --> L)" -by (simp add: LIM_eq complex_cnj_diff [symmetric]) +by (simp add: LIM_eq complex_cnj_diff [symmetric] del: complex_cnj_diff) lemma starfun_norm: "( *f* (\x. norm (f x))) = (\x. hnorm (( *f* f) x))" by transfer (rule refl) @@ -148,7 +148,7 @@ text{*Nonstandard version*} lemma NSCDERIV_pow: "NSDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))" -by (simp add: NSDERIV_DERIV_iff) +by (simp add: NSDERIV_DERIV_iff del: of_real_real_of_nat_eq) text{*Can't relax the premise @{term "x \ 0"}: it isn't continuous at zero*} lemma NSCDERIV_inverse: diff -r 3e8cbb624cc5 -r 48a745e1bde7 src/HOL/NSA/NSCA.thy --- a/src/HOL/NSA/NSCA.thy Tue May 06 23:35:24 2014 +0200 +++ b/src/HOL/NSA/NSCA.thy Wed May 07 12:25:35 2014 +0200 @@ -291,10 +291,10 @@ done lemma hRe_diff [simp]: "\x y. hRe (x - y) = hRe x - hRe y" -by transfer (rule complex_Re_diff) +by transfer simp lemma hIm_diff [simp]: "\x y. hIm (x - y) = hIm x - hIm y" -by transfer (rule complex_Im_diff) +by transfer simp lemma approx_hRe: "x \ y \ hRe x \ hRe y" unfolding approx_def by (drule Infinitesimal_hRe) simp diff -r 3e8cbb624cc5 -r 48a745e1bde7 src/HOL/NSA/NSComplex.thy --- a/src/HOL/NSA/NSComplex.thy Tue May 06 23:35:24 2014 +0200 +++ b/src/HOL/NSA/NSComplex.thy Wed May 07 12:25:35 2014 +0200 @@ -129,33 +129,33 @@ by transfer (rule complex_equality) lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0" -by transfer (rule complex_Re_zero) +by transfer simp lemma hcomplex_hIm_zero [simp]: "hIm 0 = 0" -by transfer (rule complex_Im_zero) +by transfer simp lemma hcomplex_hRe_one [simp]: "hRe 1 = 1" -by transfer (rule complex_Re_one) +by transfer simp lemma hcomplex_hIm_one [simp]: "hIm 1 = 0" -by transfer (rule complex_Im_one) +by transfer simp subsection{*Addition for Nonstandard Complex Numbers*} lemma hRe_add: "!!x y. hRe(x + y) = hRe(x) + hRe(y)" -by transfer (rule complex_Re_add) +by transfer simp lemma hIm_add: "!!x y. hIm(x + y) = hIm(x) + hIm(y)" -by transfer (rule complex_Im_add) +by transfer simp subsection{*More Minus Laws*} lemma hRe_minus: "!!z. hRe(-z) = - hRe(z)" -by transfer (rule complex_Re_minus) +by transfer (rule uminus_complex.sel) lemma hIm_minus: "!!z. hIm(-z) = - hIm(z)" -by transfer (rule complex_Im_minus) +by transfer (rule uminus_complex.sel) lemma hcomplex_add_minus_eq_minus: "x + y = (0::hcomplex) ==> x = -y" @@ -212,10 +212,10 @@ subsection{*HComplex theorems*} lemma hRe_HComplex [simp]: "!!x y. hRe (HComplex x y) = x" -by transfer (rule Re) +by transfer simp lemma hIm_HComplex [simp]: "!!x y. hIm (HComplex x y) = y" -by transfer (rule Im) +by transfer simp lemma hcomplex_surj [simp]: "!!z. HComplex (hRe z) (hIm z) = z" by transfer (rule complex_surj) @@ -423,7 +423,7 @@ by transfer (rule Complex_eq_1) lemma i_eq_HComplex_0_1: "iii = HComplex 0 1" -by transfer (rule i_def [THEN meta_eq_to_obj_eq]) +by transfer (simp add: complex_eq_iff) lemma HComplex_eq_i [simp]: "!!x y. (HComplex x y = iii) = (x = 0 & y = 1)" by transfer (rule Complex_eq_i) @@ -447,10 +447,10 @@ by transfer simp lemma hcmod_mult_i [simp]: "!!y. hcmod (iii * hcomplex_of_hypreal y) = abs y" -by transfer simp +by transfer (simp add: norm_complex_def) lemma hcmod_mult_i2 [simp]: "!!y. hcmod (hcomplex_of_hypreal y * iii) = abs y" -by transfer simp +by transfer (simp add: norm_complex_def) (*---------------------------------------------------------------------------*) (* harg *) @@ -458,7 +458,7 @@ lemma cos_harg_i_mult_zero [simp]: "!!y. y \ 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0" -by transfer (rule cos_arg_i_mult_zero) +by transfer simp lemma hcomplex_of_hypreal_zero_iff [simp]: "!!y. (hcomplex_of_hypreal y = 0) = (y = 0)" @@ -469,17 +469,17 @@ lemma complex_split_polar2: "\n. \r a. (z n) = complex_of_real r * (Complex (cos a) (sin a))" -by (blast intro: complex_split_polar) +by (auto intro: complex_split_polar) lemma hcomplex_split_polar: "!!z. \r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))" -by transfer (rule complex_split_polar) +by transfer (simp add: complex_split_polar) lemma hcis_eq: "!!a. hcis a = (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))" -by transfer (simp add: cis_def) +by transfer (simp add: complex_eq_iff) lemma hrcis_Ex: "!!z. \r a. z = hrcis r a" by transfer (rule rcis_Ex) @@ -502,12 +502,12 @@ lemma hcmod_unit_one [simp]: "!!a. hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1" -by transfer (rule cmod_unit_one) +by transfer (simp add: cmod_unit_one) lemma hcmod_complex_polar [simp]: "!!r a. hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = abs r" -by transfer (rule cmod_complex_polar) +by transfer (simp add: cmod_complex_polar) lemma hcmod_hrcis [simp]: "!!r a. hcmod(hrcis r a) = abs r" by transfer (rule complex_mod_rcis) @@ -579,10 +579,10 @@ by transfer (simp add: rcis_inverse inverse_eq_divide [symmetric]) lemma hRe_hcis [simp]: "!!a. hRe(hcis a) = ( *f* cos) a" -by transfer (rule Re_cis) +by transfer simp lemma hIm_hcis [simp]: "!!a. hIm(hcis a) = ( *f* sin) a" -by transfer (rule Im_cis) +by transfer simp lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)" by (simp add: NSDeMoivre) diff -r 3e8cbb624cc5 -r 48a745e1bde7 src/HOL/NthRoot.thy --- a/src/HOL/NthRoot.thy Tue May 06 23:35:24 2014 +0200 +++ b/src/HOL/NthRoot.thy Wed May 07 12:25:35 2014 +0200 @@ -374,12 +374,18 @@ lemma real_sqrt_one [simp]: "sqrt 1 = 1" unfolding sqrt_def by (rule real_root_one [OF pos2]) +lemma real_sqrt_four [simp]: "sqrt 4 = 2" + using real_sqrt_abs[of 2] by simp + lemma real_sqrt_minus: "sqrt (- x) = - sqrt x" unfolding sqrt_def by (rule real_root_minus) lemma real_sqrt_mult: "sqrt (x * y) = sqrt x * sqrt y" unfolding sqrt_def by (rule real_root_mult) +lemma real_sqrt_mult_self[simp]: "sqrt a * sqrt a = \a\" + using real_sqrt_abs[of a] unfolding power2_eq_square real_sqrt_mult . + lemma real_sqrt_inverse: "sqrt (inverse x) = inverse (sqrt x)" unfolding sqrt_def by (rule real_root_inverse) diff -r 3e8cbb624cc5 -r 48a745e1bde7 src/HOL/Real.thy --- a/src/HOL/Real.thy Tue May 06 23:35:24 2014 +0200 +++ b/src/HOL/Real.thy Wed May 07 12:25:35 2014 +0200 @@ -1555,6 +1555,7 @@ "real a \ (- numeral x::real) ^ n \ a \ (- numeral x::int) ^ n" unfolding real_of_int_le_iff[symmetric] by simp + subsection{*Density of the Reals*} lemma real_lbound_gt_zero: @@ -1613,6 +1614,14 @@ apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto) done +lemma real_of_nat_less_numeral_iff [simp]: + "real (n::nat) < numeral w \ n < numeral w" + using real_of_nat_less_iff[of n "numeral w"] by simp + +lemma numeral_less_real_of_nat_iff [simp]: + "numeral w < real (n::nat) \ numeral w < n" + using real_of_nat_less_iff[of "numeral w" n] by simp + lemma numeral_le_real_of_int_iff [simp]: "((numeral n) \ real (m::int)) = (numeral n \ m)" by (simp add: linorder_not_less [symmetric]) diff -r 3e8cbb624cc5 -r 48a745e1bde7 src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Tue May 06 23:35:24 2014 +0200 +++ b/src/HOL/Real_Vector_Spaces.thy Wed May 07 12:25:35 2014 +0200 @@ -257,6 +257,12 @@ lemma of_real_mult [simp]: "of_real (x * y) = of_real x * of_real y" by (simp add: of_real_def mult_commute) +lemma of_real_setsum[simp]: "of_real (setsum f s) = (\x\s. of_real (f x))" + by (induct s rule: infinite_finite_induct) auto + +lemma of_real_setprod[simp]: "of_real (setprod f s) = (\x\s. of_real (f x))" + by (induct s rule: infinite_finite_induct) auto + lemma nonzero_of_real_inverse: "x \ 0 \ of_real (inverse x) = inverse (of_real x :: 'a::real_div_algebra)" @@ -304,6 +310,12 @@ lemma of_real_of_int_eq [simp]: "of_real (of_int z) = of_int z" by (cases z rule: int_diff_cases, simp) +lemma of_real_real_of_nat_eq [simp]: "of_real (real n) = of_nat n" + by (simp add: real_of_nat_def) + +lemma of_real_real_of_int_eq [simp]: "of_real (real z) = of_int z" + by (simp add: real_of_int_def) + lemma of_real_numeral: "of_real (numeral w) = numeral w" using of_real_of_int_eq [of "numeral w"] by simp @@ -1121,6 +1133,18 @@ lemma real_sgn_neg: "(x::real) < 0 \ sgn x = -1" unfolding real_sgn_eq by simp +lemma zero_le_sgn_iff [simp]: "0 \ sgn x \ 0 \ (x::real)" + by (cases "0::real" x rule: linorder_cases) simp_all + +lemma zero_less_sgn_iff [simp]: "0 < sgn x \ 0 < (x::real)" + by (cases "0::real" x rule: linorder_cases) simp_all + +lemma sgn_le_0_iff [simp]: "sgn x \ 0 \ (x::real) \ 0" + by (cases "0::real" x rule: linorder_cases) simp_all + +lemma sgn_less_0_iff [simp]: "sgn x < 0 \ (x::real) < 0" + by (cases "0::real" x rule: linorder_cases) simp_all + lemma norm_conv_dist: "norm x = dist x 0" unfolding dist_norm by simp