# HG changeset patch # User paulson # Date 1075820311 -3600 # Node ID 61de6209676840b8657f8974e6ecc45fff37cead # Parent 67a628beb9812f52e5d9b8c5eb97caf2183d07cf further tidying of the complex numbers diff -r 67a628beb981 -r 61de62096768 src/HOL/Complex/Complex.thy --- a/src/HOL/Complex/Complex.thy Tue Feb 03 11:06:36 2004 +0100 +++ b/src/HOL/Complex/Complex.thy Tue Feb 03 15:58:31 2004 +0100 @@ -79,7 +79,7 @@ complex_diff_def: "z - w == z + - (w::complex)" - complex_mult_def: + complex_mult_def: "z * w == Complex (Re z * Re w - Im z * Im w) (Re z * Im w + Im z * Re w)" complex_divide_def: "w / (z::complex) == w * inverse z" @@ -103,83 +103,50 @@ lemma complex_equality [intro?]: "Re z = Re w ==> Im z = Im w ==> z = w" by (induct z, induct w) simp -lemma Re: "Re(Complex x y) = x" +lemma Re [simp]: "Re(Complex x y) = x" by simp -declare Re [simp] -lemma Im: "Im(Complex x y) = y" +lemma Im [simp]: "Im(Complex x y) = y" by simp -declare Im [simp] lemma complex_Re_Im_cancel_iff: "(w=z) = (Re(w) = Re(z) & Im(w) = Im(z))" by (induct w, induct z, simp) -lemma complex_Re_zero: "Re 0 = 0" +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_Im_zero: "Im 0 = 0" -by (simp add: complex_zero_def) -declare complex_Re_zero [simp] complex_Im_zero [simp] +lemma complex_Re_one [simp]: "Re 1 = 1" +by (simp add: complex_one_def) -lemma complex_Re_one: "Re 1 = 1" -by (simp add: complex_one_def) -declare complex_Re_one [simp] - -lemma complex_Im_one: "Im 1 = 0" +lemma complex_Im_one [simp]: "Im 1 = 0" by (simp add: complex_one_def) -declare complex_Im_one [simp] -lemma complex_Re_i: "Re(ii) = 0" +lemma complex_Re_i [simp]: "Re(ii) = 0" by (simp add: i_def) -declare complex_Re_i [simp] -lemma complex_Im_i: "Im(ii) = 1" +lemma complex_Im_i [simp]: "Im(ii) = 1" by (simp add: i_def) -declare complex_Im_i [simp] -lemma Re_complex_of_real_zero: "Re(complex_of_real 0) = 0" +lemma Re_complex_of_real [simp]: "Re(complex_of_real z) = z" by (simp add: complex_of_real_def) -declare Re_complex_of_real_zero [simp] -lemma Im_complex_of_real_zero: "Im(complex_of_real 0) = 0" -by (simp add: complex_of_real_def) -declare Im_complex_of_real_zero [simp] - -lemma Re_complex_of_real_one: "Re(complex_of_real 1) = 1" +lemma Im_complex_of_real [simp]: "Im(complex_of_real z) = 0" by (simp add: complex_of_real_def) -declare Re_complex_of_real_one [simp] - -lemma Im_complex_of_real_one: "Im(complex_of_real 1) = 0" -by (simp add: complex_of_real_def) -declare Im_complex_of_real_one [simp] - -lemma Re_complex_of_real: "Re(complex_of_real z) = z" -by (simp add: complex_of_real_def) -declare Re_complex_of_real [simp] - -lemma Im_complex_of_real: "Im(complex_of_real z) = 0" -by (simp add: complex_of_real_def) -declare Im_complex_of_real [simp] -subsection{*Negation*} +subsection{*Unary Minus*} lemma complex_minus: "- (Complex x y) = Complex (-x) (-y)" by (simp add: complex_minus_def) -lemma complex_Re_minus: "Re (-z) = - Re z" -by (simp add: complex_minus_def) - -lemma complex_Im_minus: "Im (-z) = - Im z" +lemma complex_Re_minus [simp]: "Re (-z) = - Re z" by (simp add: complex_minus_def) -lemma complex_minus_zero: "-(0::complex) = 0" -by (simp add: complex_minus_def complex_zero_def) -declare complex_minus_zero [simp] - -lemma complex_minus_zero_iff: "(-x = 0) = (x = (0::complex))" -by (induct x, simp add: complex_minus_def complex_zero_def) -declare complex_minus_zero_iff [simp] +lemma complex_Im_minus [simp]: "Im (-z) = - Im z" +by (simp add: complex_minus_def) subsection{*Addition*} @@ -187,10 +154,10 @@ lemma complex_add: "Complex x1 y1 + Complex x2 y2 = Complex (x1+x2) (y1+y2)" by (simp add: complex_add_def) -lemma complex_Re_add: "Re(x + y) = Re(x) + Re(y)" +lemma complex_Re_add [simp]: "Re(x + y) = Re(x) + Re(y)" by (simp add: complex_add_def) -lemma complex_Im_add: "Im(x + y) = Im(x) + Im(y)" +lemma complex_Im_add [simp]: "Im(x + y) = Im(x) + Im(y)" by (simp add: complex_add_def) lemma complex_add_commute: "(u::complex) + v = v + u" @@ -212,6 +179,13 @@ "Complex x1 y1 - Complex x2 y2 = Complex (x1-x2) (y1-y2)" by (simp add: complex_add_def complex_minus_def 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) + + subsection{*Multiplication*} lemma complex_mult: @@ -222,7 +196,7 @@ by (simp add: complex_mult_def mult_commute add_commute) lemma complex_mult_assoc: "((u::complex) * v) * w = u * (v * w)" -by (simp add: complex_mult_def mult_ac add_ac +by (simp add: complex_mult_def mult_ac add_ac right_diff_distrib right_distrib left_diff_distrib left_distrib) lemma complex_mult_one_left: "(1::complex) * z = z" @@ -239,9 +213,9 @@ by (simp add: complex_inverse_def) lemma complex_mult_inv_left: "z \ (0::complex) ==> inverse(z) * z = 1" -apply (induct z) -apply (rename_tac x y) -apply (auto simp add: complex_mult complex_inverse complex_one_def +apply (induct z) +apply (rename_tac x y) +apply (auto simp add: complex_mult complex_inverse complex_one_def complex_zero_def add_divide_distrib [symmetric] power2_eq_square mult_ac) apply (drule_tac y = y in real_sum_squares_not_zero) apply (drule_tac [2] x = x in real_sum_squares_not_zero2, auto) @@ -254,28 +228,28 @@ proof fix z u v w :: complex show "(u + v) + w = u + (v + w)" - by (rule complex_add_assoc) + by (rule complex_add_assoc) show "z + w = w + z" - by (rule complex_add_commute) + by (rule complex_add_commute) show "0 + z = z" - by (rule complex_add_zero_left) + by (rule complex_add_zero_left) show "-z + z = 0" - by (rule complex_add_minus_left) + by (rule complex_add_minus_left) show "z - w = z + -w" by (simp add: complex_diff_def) show "(u * v) * w = u * (v * w)" - by (rule complex_mult_assoc) + by (rule complex_mult_assoc) show "z * w = w * z" - by (rule complex_mult_commute) + by (rule complex_mult_commute) show "1 * z = z" - by (rule complex_mult_one_left) + by (rule complex_mult_one_left) show "0 \ (1::complex)" by (simp add: complex_zero_def complex_one_def) show "(u + v) * w = u * w + v * w" by (simp add: complex_mult_def complex_add_def left_distrib real_diff_def add_ac) show "z+u = z+v ==> u=v" proof - - assume eq: "z+u = z+v" + assume eq: "z+u = z+v" hence "(-z + z) + u = (-z + z) + v" by (simp only: eq complex_add_assoc) thus "u = v" by (simp add: complex_add_minus_left complex_add_zero_left) qed @@ -283,7 +257,7 @@ thus "z / w = z * inverse w" by (simp add: complex_divide_def) show "inverse w * w = 1" - by (simp add: neq complex_mult_inv_left) + by (simp add: neq complex_mult_inv_left) qed instance complex :: division_by_zero @@ -291,33 +265,30 @@ show inv: "inverse 0 = (0::complex)" by (simp add: complex_inverse_def complex_zero_def) fix x :: complex - show "x/0 = 0" + show "x/0 = 0" by (simp add: complex_divide_def inv) qed subsection{*Embedding Properties for @{term complex_of_real} Map*} -lemma complex_of_real_one: "complex_of_real 1 = 1" +lemma complex_of_real_one [simp]: "complex_of_real 1 = 1" by (simp add: complex_one_def complex_of_real_def) -declare complex_of_real_one [simp] -lemma complex_of_real_zero: "complex_of_real 0 = 0" +lemma complex_of_real_zero [simp]: "complex_of_real 0 = 0" by (simp add: complex_zero_def complex_of_real_def) -declare complex_of_real_zero [simp] -lemma complex_of_real_eq_iff: +lemma complex_of_real_eq_iff [iff]: "(complex_of_real x = complex_of_real y) = (x = y)" -by (simp add: complex_of_real_def) -declare complex_of_real_eq_iff [iff] +by (simp add: complex_of_real_def) lemma complex_of_real_minus: "complex_of_real(-x) = - complex_of_real x" by (simp add: complex_of_real_def complex_minus) lemma complex_of_real_inverse: - "complex_of_real(inverse x) = inverse(complex_of_real x)" + "complex_of_real(inverse x) = inverse(complex_of_real x)" apply (case_tac "x=0", simp) -apply (simp add: complex_inverse complex_of_real_def real_divide_def +apply (simp add: complex_inverse complex_of_real_def real_divide_def inverse_mult_distrib power2_eq_square) done @@ -327,7 +298,8 @@ lemma complex_of_real_diff: "complex_of_real x - complex_of_real y = complex_of_real (x - y)" -by (simp add: complex_of_real_minus [symmetric] complex_diff_def complex_of_real_add) +by (simp add: complex_of_real_minus [symmetric] complex_diff_def + complex_of_real_add) lemma complex_of_real_mult: "complex_of_real x * complex_of_real y = complex_of_real (x * y)" @@ -337,50 +309,44 @@ "complex_of_real x / complex_of_real y = complex_of_real(x/y)" apply (simp add: complex_divide_def) apply (case_tac "y=0", simp) -apply (simp add: complex_of_real_mult [symmetric] complex_of_real_inverse real_divide_def) +apply (simp add: complex_of_real_mult [symmetric] complex_of_real_inverse + real_divide_def) done lemma complex_mod: "cmod (Complex x y) = sqrt(x ^ 2 + y ^ 2)" by (simp add: cmod_def) -lemma complex_mod_zero: "cmod(0) = 0" +lemma complex_mod_zero [simp]: "cmod(0) = 0" by (simp add: cmod_def) -declare complex_mod_zero [simp] lemma complex_mod_one [simp]: "cmod(1) = 1" by (simp add: cmod_def power2_eq_square) -lemma complex_mod_complex_of_real: "cmod(complex_of_real x) = abs x" +lemma complex_mod_complex_of_real [simp]: "cmod(complex_of_real x) = abs x" by (simp add: complex_of_real_def power2_eq_square complex_mod) -declare complex_mod_complex_of_real [simp] lemma complex_of_real_abs: "complex_of_real (abs x) = complex_of_real(cmod(complex_of_real x))" by simp - subsection{*Conjugation is an Automorphism*} lemma complex_cnj: "cnj (Complex x y) = Complex x (-y)" by (simp add: cnj_def) -lemma complex_cnj_cancel_iff: "(cnj x = cnj y) = (x = y)" +lemma complex_cnj_cancel_iff [simp]: "(cnj x = cnj y) = (x = y)" by (simp add: cnj_def complex_Re_Im_cancel_iff) -declare complex_cnj_cancel_iff [simp] -lemma complex_cnj_cnj: "cnj (cnj z) = z" +lemma complex_cnj_cnj [simp]: "cnj (cnj z) = z" by (simp add: cnj_def) -declare complex_cnj_cnj [simp] -lemma complex_cnj_complex_of_real: +lemma complex_cnj_complex_of_real [simp]: "cnj (complex_of_real x) = complex_of_real x" by (simp add: complex_of_real_def complex_cnj) -declare complex_cnj_complex_of_real [simp] -lemma complex_mod_cnj: "cmod (cnj z) = cmod z" +lemma complex_mod_cnj [simp]: "cmod (cnj z) = cmod z" by (induct z, simp add: complex_cnj complex_mod power2_eq_square) -declare complex_mod_cnj [simp] lemma complex_cnj_minus: "cnj (-z) = - cnj z" by (simp add: cnj_def complex_minus complex_Re_minus complex_Im_minus) @@ -400,60 +366,43 @@ lemma complex_cnj_divide: "cnj(w / z) = (cnj w)/(cnj z)" by (simp add: complex_divide_def complex_cnj_mult complex_cnj_inverse) -lemma complex_cnj_one: "cnj 1 = 1" +lemma complex_cnj_one [simp]: "cnj 1 = 1" by (simp add: cnj_def complex_one_def) -declare complex_cnj_one [simp] lemma complex_add_cnj: "z + cnj z = complex_of_real (2 * Re(z))" by (induct z, simp add: complex_add complex_cnj complex_of_real_def) lemma complex_diff_cnj: "z - cnj z = complex_of_real (2 * Im(z)) * ii" apply (induct z) -apply (simp add: complex_add complex_cnj complex_of_real_def complex_diff_def +apply (simp add: complex_add complex_cnj complex_of_real_def complex_diff_def complex_minus i_def complex_mult) done lemma complex_cnj_zero [simp]: "cnj 0 = 0" by (simp add: cnj_def complex_zero_def) -lemma complex_cnj_zero_iff: "(cnj z = 0) = (z = 0)" +lemma complex_cnj_zero_iff [iff]: "(cnj z = 0) = (z = 0)" by (induct z, simp add: complex_zero_def complex_cnj) -declare complex_cnj_zero_iff [iff] lemma complex_mult_cnj: "z * cnj z = complex_of_real (Re(z) ^ 2 + Im(z) ^ 2)" -by (induct z, simp add: complex_cnj complex_mult complex_of_real_def power2_eq_square) - - -subsection{*Algebra*} - -lemma complex_add_left_cancel_zero: "(x + y = x) = (y = (0::complex))" -by (induct x, induct y, simp add: complex_zero_def complex_add) -declare complex_add_left_cancel_zero [simp] - -lemma complex_diff_mult_distrib: "((z1::complex) - z2) * w = (z1 * w) - (z2 * w)" -by (simp add: complex_diff_def left_distrib) - -lemma complex_diff_mult_distrib2: "(w::complex) * (z1 - z2) = (w * z1) - (w * z2)" -by (simp add: complex_diff_def right_distrib) +by (induct z, + simp add: complex_cnj complex_mult complex_of_real_def power2_eq_square) subsection{*Modulus*} -lemma complex_mod_eq_zero_cancel: "(cmod x = 0) = (x = 0)" +lemma complex_mod_eq_zero_cancel [simp]: "(cmod x = 0) = (x = 0)" apply (induct x) -apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 +apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 simp add: complex_mod complex_zero_def power2_eq_square) done -declare complex_mod_eq_zero_cancel [simp] -lemma complex_mod_complex_of_real_of_nat: +lemma complex_mod_complex_of_real_of_nat [simp]: "cmod (complex_of_real(real (n::nat))) = real n" by simp -declare complex_mod_complex_of_real_of_nat [simp] -lemma complex_mod_minus: "cmod (-x) = cmod(x)" +lemma complex_mod_minus [simp]: "cmod (-x) = cmod(x)" by (induct x, simp add: complex_mod complex_minus power2_eq_square) -declare complex_mod_minus [simp] lemma complex_mod_mult_cnj: "cmod(z * cnj(z)) = cmod(z) ^ 2" apply (induct z, simp add: complex_mod complex_cnj complex_mult) @@ -463,87 +412,84 @@ lemma complex_mod_squared: "cmod(Complex x y) ^ 2 = x ^ 2 + y ^ 2" by (simp add: cmod_def) -lemma complex_mod_ge_zero: "0 \ cmod x" +lemma complex_mod_ge_zero [simp]: "0 \ cmod x" by (simp add: cmod_def) -declare complex_mod_ge_zero [simp] -lemma abs_cmod_cancel: "abs(cmod x) = cmod x" -by (simp add: abs_if linorder_not_less) -declare abs_cmod_cancel [simp] +lemma abs_cmod_cancel [simp]: "abs(cmod x) = cmod x" +by (simp add: abs_if linorder_not_less) lemma complex_mod_mult: "cmod(x*y) = cmod(x) * cmod(y)" apply (induct x, induct y) -apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2 [symmetric] simp del: realpow_Suc) +apply (auto simp add: complex_mult complex_mod real_sqrt_mult_distrib2[symmetric] + simp del: realpow_Suc) apply (rule_tac n = 1 in power_inject_base) apply (auto simp add: power2_eq_square [symmetric] simp del: realpow_Suc) -apply (auto simp add: real_diff_def power2_eq_square right_distrib left_distrib add_ac mult_ac) +apply (auto simp add: real_diff_def power2_eq_square right_distrib left_distrib + add_ac mult_ac) done -lemma complex_mod_add_squared_eq: "cmod(x + y) ^ 2 = cmod(x) ^ 2 + cmod(y) ^ 2 + 2 * Re(x * cnj y)" +lemma complex_mod_add_squared_eq: + "cmod(x + y) ^ 2 = cmod(x) ^ 2 + cmod(y) ^ 2 + 2 * Re(x * cnj y)" apply (induct x, induct y) apply (auto simp add: complex_add complex_mod_squared complex_mult complex_cnj real_diff_def simp del: realpow_Suc) apply (auto simp add: right_distrib left_distrib power2_eq_square mult_ac add_ac) done -lemma complex_Re_mult_cnj_le_cmod: "Re(x * cnj y) \ cmod(x * cnj y)" +lemma complex_Re_mult_cnj_le_cmod [simp]: "Re(x * cnj y) \ cmod(x * cnj y)" apply (induct x, induct y) apply (auto simp add: complex_mod complex_mult complex_cnj real_diff_def simp del: realpow_Suc) done -declare complex_Re_mult_cnj_le_cmod [simp] -lemma complex_Re_mult_cnj_le_cmod2: "Re(x * cnj y) \ cmod(x * y)" +lemma complex_Re_mult_cnj_le_cmod2 [simp]: "Re(x * cnj y) \ cmod(x * y)" by (insert complex_Re_mult_cnj_le_cmod [of x y], simp add: complex_mod_mult) -declare complex_Re_mult_cnj_le_cmod2 [simp] -lemma real_sum_squared_expand: "((x::real) + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y" +lemma real_sum_squared_expand: + "((x::real) + y) ^ 2 = x ^ 2 + y ^ 2 + 2 * x * y" by (simp add: left_distrib right_distrib power2_eq_square) -lemma complex_mod_triangle_squared: "cmod (x + y) ^ 2 \ (cmod(x) + cmod(y)) ^ 2" +lemma complex_mod_triangle_squared [simp]: + "cmod (x + y) ^ 2 \ (cmod(x) + cmod(y)) ^ 2" by (simp add: real_sum_squared_expand complex_mod_add_squared_eq real_mult_assoc complex_mod_mult [symmetric]) -declare complex_mod_triangle_squared [simp] -lemma complex_mod_minus_le_complex_mod: "- cmod x \ cmod x" +lemma complex_mod_minus_le_complex_mod [simp]: "- cmod x \ cmod x" by (rule order_trans [OF _ complex_mod_ge_zero], simp) -declare complex_mod_minus_le_complex_mod [simp] -lemma complex_mod_triangle_ineq: "cmod (x + y) \ cmod(x) + cmod(y)" +lemma complex_mod_triangle_ineq [simp]: "cmod (x + y) \ cmod(x) + cmod(y)" apply (rule_tac n = 1 in realpow_increasing) apply (auto intro: order_trans [OF _ complex_mod_ge_zero] simp add: power2_eq_square [symmetric]) done -declare complex_mod_triangle_ineq [simp] -lemma complex_mod_triangle_ineq2: "cmod(b + a) - cmod b \ cmod a" +lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a) - cmod b \ cmod a" by (insert complex_mod_triangle_ineq [THEN add_right_mono, of b a"-cmod b"], simp) -declare complex_mod_triangle_ineq2 [simp] lemma complex_mod_diff_commute: "cmod (x - y) = cmod (y - x)" apply (induct x, induct y) apply (auto simp add: complex_diff complex_mod right_diff_distrib power2_eq_square left_diff_distrib add_ac mult_ac) done -lemma complex_mod_add_less: "[| cmod x < r; cmod y < s |] ==> cmod (x + y) < r + s" +lemma complex_mod_add_less: + "[| cmod x < r; cmod y < s |] ==> cmod (x + y) < r + s" by (auto intro: order_le_less_trans complex_mod_triangle_ineq) -lemma complex_mod_mult_less: "[| cmod x < r; cmod y < s |] ==> cmod (x * y) < r * s" +lemma complex_mod_mult_less: + "[| cmod x < r; cmod y < s |] ==> cmod (x * y) < r * s" by (auto intro: real_mult_less_mono' simp add: complex_mod_mult) -lemma complex_mod_diff_ineq: "cmod(a) - cmod(b) \ cmod(a + b)" +lemma complex_mod_diff_ineq [simp]: "cmod(a) - cmod(b) \ cmod(a + b)" apply (rule linorder_cases [of "cmod(a)" "cmod (b)"]) apply auto apply (rule order_trans [of _ 0], rule order_less_imp_le) -apply (simp add: compare_rls, simp) +apply (simp add: compare_rls, simp) apply (simp add: compare_rls) apply (rule complex_mod_minus [THEN subst]) apply (rule order_trans) apply (rule_tac [2] complex_mod_triangle_ineq) apply (auto simp add: add_ac) done -declare complex_mod_diff_ineq [simp] -lemma complex_Re_le_cmod: "Re z \ cmod z" +lemma complex_Re_le_cmod [simp]: "Re z \ cmod z" by (induct z, simp add: complex_mod del: realpow_Suc) -declare complex_Re_le_cmod [simp] lemma complex_mod_gt_zero: "z \ 0 ==> 0 < cmod z" apply (insert complex_mod_ge_zero [of z]) @@ -562,9 +508,8 @@ lemma complex_mod_divide: "cmod(x/y) = cmod(x)/(cmod y)" by (simp add: complex_divide_def real_divide_def, simp add: complex_mod_mult complex_mod_inverse) -lemma complex_inverse_divide: "inverse(x/y) = y/(x::complex)" +lemma complex_inverse_divide [simp]: "inverse(x/y) = y/(x::complex)" by (simp add: complex_divide_def inverse_mult_distrib mult_commute) -declare complex_inverse_divide [simp] subsection{*Exponentiation*} @@ -598,7 +543,8 @@ apply (auto simp add: complex_mod_mult) done -lemma complexpow_minus: "(-x::complex) ^ n = (if even n then (x ^ n) else -(x ^ n))" +lemma complexpow_minus: + "(-x::complex) ^ n = (if even n then (x ^ n) else -(x ^ n))" by (induct_tac "n", auto) lemma complexpow_i_squared [simp]: "ii ^ 2 = -(1::complex)" @@ -610,19 +556,16 @@ subsection{*The Function @{term sgn}*} -lemma sgn_zero: "sgn 0 = 0" +lemma sgn_zero [simp]: "sgn 0 = 0" by (simp add: sgn_def) -declare sgn_zero [simp] -lemma sgn_one: "sgn 1 = 1" +lemma sgn_one [simp]: "sgn 1 = 1" by (simp add: sgn_def) -declare sgn_one [simp] lemma sgn_minus: "sgn (-z) = - sgn(z)" by (simp add: sgn_def) -lemma sgn_eq: - "sgn z = z / complex_of_real (cmod z)" +lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)" apply (simp add: sgn_def) done @@ -631,20 +574,18 @@ apply (auto simp add: complex_of_real_def i_def complex_mult complex_add) done -lemma Re_complex_i: "Re(complex_of_real(x) + ii * complex_of_real(y)) = x" +(*????delete????*) +lemma Re_complex_i [simp]: "Re(complex_of_real(x) + ii * complex_of_real(y)) = x" by (auto simp add: complex_of_real_def i_def complex_mult complex_add) -declare Re_complex_i [simp] -lemma Im_complex_i: "Im(complex_of_real(x) + ii * complex_of_real(y)) = y" +lemma Im_complex_i [simp]: "Im(complex_of_real(x) + ii * complex_of_real(y)) = y" by (auto simp add: complex_of_real_def i_def complex_mult complex_add) -declare Im_complex_i [simp] lemma i_mult_eq: "ii * ii = complex_of_real (-1)" by (simp add: i_def complex_of_real_def complex_mult complex_add) -lemma i_mult_eq2: "ii * ii = -(1::complex)" +lemma i_mult_eq2 [simp]: "ii * ii = -(1::complex)" by (simp add: i_def complex_one_def complex_mult complex_minus) -declare i_mult_eq2 [simp] lemma cmod_i: "cmod (complex_of_real(x) + ii * complex_of_real(y)) = sqrt (x ^ 2 + y ^ 2)" @@ -662,49 +603,52 @@ ==> ya = yb" by (simp add: complex_of_real_def i_def complex_mult complex_add) -lemma complex_eq_cancel_iff: "(complex_of_real xa + ii * complex_of_real ya = +(*FIXME: tidy up this mess by fixing a canonical form for complex expressions, +e.g. x + y*ii*) + +lemma complex_eq_cancel_iff [iff]: + "(complex_of_real xa + ii * complex_of_real ya = complex_of_real xb + ii * complex_of_real yb) = ((xa = xb) & (ya = yb))" by (auto intro: complex_eq_Im_eq complex_eq_Re_eq) -declare complex_eq_cancel_iff [iff] -lemma complex_eq_cancel_iffA: "(complex_of_real xa + complex_of_real ya * ii = +lemma complex_eq_cancel_iffA [iff]: + "(complex_of_real xa + complex_of_real ya * ii = complex_of_real xb + complex_of_real yb * ii) = ((xa = xb) & (ya = yb))" by (simp add: mult_commute) -declare complex_eq_cancel_iffA [iff] -lemma complex_eq_cancel_iffB: "(complex_of_real xa + complex_of_real ya * ii = +lemma complex_eq_cancel_iffB [iff]: + "(complex_of_real xa + complex_of_real ya * ii = complex_of_real xb + ii * complex_of_real yb) = ((xa = xb) & (ya = yb))" by (auto simp add: mult_commute) -declare complex_eq_cancel_iffB [iff] -lemma complex_eq_cancel_iffC: "(complex_of_real xa + ii * complex_of_real ya = +lemma complex_eq_cancel_iffC [iff]: + "(complex_of_real xa + ii * complex_of_real ya = complex_of_real xb + complex_of_real yb * ii) = ((xa = xb) & (ya = yb))" by (auto simp add: mult_commute) -declare complex_eq_cancel_iffC [iff] -lemma complex_eq_cancel_iff2: "(complex_of_real x + ii * complex_of_real y = +lemma complex_eq_cancel_iff2 [simp]: + "(complex_of_real x + ii * complex_of_real y = complex_of_real xa) = (x = xa & y = 0)" apply (cut_tac xa = x and ya = y and xb = xa and yb = 0 in complex_eq_cancel_iff) apply (simp del: complex_eq_cancel_iff) done -declare complex_eq_cancel_iff2 [simp] -lemma complex_eq_cancel_iff2a: "(complex_of_real x + complex_of_real y * ii = +lemma complex_eq_cancel_iff2a [simp]: + "(complex_of_real x + complex_of_real y * ii = complex_of_real xa) = (x = xa & y = 0)" by (auto simp add: mult_commute) -declare complex_eq_cancel_iff2a [simp] -lemma complex_eq_cancel_iff3: "(complex_of_real x + ii * complex_of_real y = +lemma complex_eq_cancel_iff3 [simp]: + "(complex_of_real x + ii * complex_of_real y = ii * complex_of_real ya) = (x = 0 & y = ya)" apply (cut_tac xa = x and ya = y and xb = 0 and yb = ya in complex_eq_cancel_iff) apply (simp del: complex_eq_cancel_iff) done -declare complex_eq_cancel_iff3 [simp] -lemma complex_eq_cancel_iff3a: "(complex_of_real x + complex_of_real y * ii = +lemma complex_eq_cancel_iff3a [simp]: + "(complex_of_real x + complex_of_real y * ii = ii * complex_of_real ya) = (x = 0 & y = ya)" by (auto simp add: mult_commute) -declare complex_eq_cancel_iff3a [simp] lemma complex_split_Re_zero: "complex_of_real x + ii * complex_of_real y = 0 @@ -716,26 +660,23 @@ ==> y = 0" by (simp add: complex_of_real_def i_def complex_zero_def complex_mult complex_add) -lemma Re_sgn: "Re(sgn z) = Re(z)/cmod z" +lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z" apply (induct z) apply (simp add: sgn_def complex_divide_def complex_of_real_inverse [symmetric]) apply (simp add: complex_of_real_def complex_mult real_divide_def) done -declare Re_sgn [simp] -lemma Im_sgn: - "Im(sgn z) = Im(z)/cmod z" +lemma Im_sgn [simp]: "Im(sgn z) = Im(z)/cmod z" apply (induct z) apply (simp add: sgn_def complex_divide_def complex_of_real_inverse [symmetric]) apply (simp add: complex_of_real_def complex_mult real_divide_def) done -declare Im_sgn [simp] lemma complex_inverse_complex_split: "inverse(complex_of_real x + ii * complex_of_real y) = complex_of_real(x/(x ^ 2 + y ^ 2)) - ii * complex_of_real(y/(x ^ 2 + y ^ 2))" -by (simp add: complex_of_real_def i_def complex_mult complex_add +by (simp add: complex_of_real_def i_def complex_mult complex_add complex_diff_def complex_minus complex_inverse real_divide_def) (*----------------------------------------------------------------------------*) @@ -746,17 +687,14 @@ lemma complex_of_real_zero_iff [simp]: "(complex_of_real y = 0) = (y = 0)" by (auto simp add: complex_zero_def complex_of_real_def) -lemma Re_mult_i_eq: "Re (ii * complex_of_real y) = 0" -by (simp add: i_def complex_of_real_def complex_mult) -declare Re_mult_i_eq [simp] - -lemma Im_mult_i_eq: "Im (ii * complex_of_real y) = y" +lemma Re_mult_i_eq [simp]: "Re (ii * complex_of_real y) = 0" by (simp add: i_def complex_of_real_def complex_mult) -declare Im_mult_i_eq [simp] -lemma complex_mod_mult_i: "cmod (ii * complex_of_real y) = abs y" +lemma Im_mult_i_eq [simp]: "Im (ii * complex_of_real y) = y" +by (simp add: i_def complex_of_real_def complex_mult) + +lemma complex_mod_mult_i [simp]: "cmod (ii * complex_of_real y) = abs y" by (simp add: i_def complex_of_real_def complex_mult complex_mod power2_eq_square) -declare complex_mod_mult_i [simp] lemma cos_arg_i_mult_zero_pos: "0 < y ==> cos (arg(ii * complex_of_real y)) = 0" @@ -772,16 +710,17 @@ apply (rule order_trans [of _ 0], auto) done -lemma cos_arg_i_mult_zero [simp] - : "y \ 0 ==> cos (arg(ii * complex_of_real y)) = 0" -apply (insert linorder_less_linear [of y 0]) +lemma cos_arg_i_mult_zero [simp]: + "y \ 0 ==> cos (arg(ii * complex_of_real y)) = 0" +apply (insert linorder_less_linear [of y 0]) apply (auto simp add: cos_arg_i_mult_zero_pos cos_arg_i_mult_zero_neg) done subsection{*Finally! Polar Form for Complex Numbers*} -lemma complex_split_polar: "\r a. z = complex_of_real r * +lemma complex_split_polar: + "\r a. z = complex_of_real r * (complex_of_real(cos a) + ii * complex_of_real(sin a))" apply (cut_tac z = z in complex_split) apply (auto simp add: polar_Ex right_distrib complex_of_real_mult mult_ac) @@ -792,18 +731,17 @@ apply (rule complex_split_polar) done -lemma Re_complex_polar: "Re(complex_of_real r * +lemma Re_complex_polar [simp]: + "Re(complex_of_real r * (complex_of_real(cos a) + ii * complex_of_real(sin a))) = r * cos a" by (auto simp add: right_distrib complex_of_real_mult mult_ac) -declare Re_complex_polar [simp] -lemma Re_rcis: "Re(rcis r a) = r * cos a" +lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a" by (simp add: rcis_def cis_def) -declare Re_rcis [simp] lemma Im_complex_polar [simp]: - "Im(complex_of_real r * - (complex_of_real(cos a) + ii * complex_of_real(sin a))) = + "Im(complex_of_real r * + (complex_of_real(cos a) + ii * complex_of_real(sin a))) = r * sin a" by (auto simp add: right_distrib complex_of_real_mult mult_ac) @@ -811,16 +749,15 @@ by (simp add: rcis_def cis_def) lemma complex_mod_complex_polar [simp]: - "cmod (complex_of_real r * - (complex_of_real(cos a) + ii * complex_of_real(sin a))) = + "cmod (complex_of_real r * + (complex_of_real(cos a) + ii * complex_of_real(sin a))) = abs r" by (auto simp add: right_distrib cmod_i complex_of_real_mult - right_distrib [symmetric] power_mult_distrib mult_ac + right_distrib [symmetric] power_mult_distrib mult_ac simp del: realpow_Suc) -lemma complex_mod_rcis: "cmod(rcis r a) = abs r" +lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r" by (simp add: rcis_def cis_def) -declare complex_mod_rcis [simp] lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))" apply (simp add: cmod_def) @@ -828,36 +765,33 @@ apply (auto simp add: complex_mult_cnj) done -lemma complex_Re_cnj: "Re(cnj z) = Re z" -by (induct z, simp add: complex_cnj) -declare complex_Re_cnj [simp] - -lemma complex_Im_cnj: "Im(cnj z) = - Im z" +lemma complex_Re_cnj [simp]: "Re(cnj z) = Re z" by (induct z, simp add: complex_cnj) -declare complex_Im_cnj [simp] -lemma complex_In_mult_cnj_zero: "Im (z * cnj z) = 0" +lemma complex_Im_cnj [simp]: "Im(cnj z) = - Im z" +by (induct z, simp add: complex_cnj) + +lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0" by (induct z, simp add: complex_cnj complex_mult) -declare complex_In_mult_cnj_zero [simp] lemma complex_Re_mult: "[| Im w = 0; Im z = 0 |] ==> Re(w * z) = Re(w) * Re(z)" by (induct z, induct w, simp add: complex_mult) -lemma complex_Re_mult_complex_of_real: "Re (z * complex_of_real c) = Re(z) * c" +lemma complex_Re_mult_complex_of_real [simp]: + "Re (z * complex_of_real c) = Re(z) * c" by (induct z, simp add: complex_of_real_def complex_mult) -declare complex_Re_mult_complex_of_real [simp] -lemma complex_Im_mult_complex_of_real: "Im (z * complex_of_real c) = Im(z) * c" +lemma complex_Im_mult_complex_of_real [simp]: + "Im (z * complex_of_real c) = Im(z) * c" by (induct z, simp add: complex_of_real_def complex_mult) -declare complex_Im_mult_complex_of_real [simp] -lemma complex_Re_mult_complex_of_real2: "Re (complex_of_real c * z) = c * Re(z)" +lemma complex_Re_mult_complex_of_real2 [simp]: + "Re (complex_of_real c * z) = c * Re(z)" by (induct z, simp add: complex_of_real_def complex_mult) -declare complex_Re_mult_complex_of_real2 [simp] -lemma complex_Im_mult_complex_of_real2: "Im (complex_of_real c * z) = c * Im(z)" +lemma complex_Im_mult_complex_of_real2 [simp]: + "Im (complex_of_real c * z) = c * Im(z)" by (induct z, simp add: complex_of_real_def complex_mult) -declare complex_Im_mult_complex_of_real2 [simp] (*---------------------------------------------------------------------------*) (* (r1 * cis a) * (r2 * cis b) = r1 * r2 * cis (a + b) *) @@ -866,9 +800,8 @@ lemma cis_rcis_eq: "cis a = rcis 1 a" by (simp add: rcis_def) -lemma rcis_mult: - "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)" -apply (simp add: rcis_def cis_def cos_add sin_add right_distrib left_distrib +lemma rcis_mult: "rcis r1 a * rcis r2 b = rcis (r1*r2) (a + b)" +apply (simp add: rcis_def cis_def cos_add sin_add right_distrib left_distrib mult_ac add_ac) apply (auto simp add: right_distrib [symmetric] complex_mult_assoc [symmetric] complex_of_real_mult complex_of_real_add complex_add_assoc [symmetric] i_mult_eq simp del: i_mult_eq2) apply (auto simp add: add_ac) @@ -878,30 +811,25 @@ lemma cis_mult: "cis a * cis b = cis (a + b)" by (simp add: cis_rcis_eq rcis_mult) -lemma cis_zero: "cis 0 = 1" +lemma cis_zero [simp]: "cis 0 = 1" by (simp add: cis_def) -declare cis_zero [simp] -lemma cis_zero2: "cis 0 = complex_of_real 1" +lemma cis_zero2 [simp]: "cis 0 = complex_of_real 1" by (simp add: cis_def) -declare cis_zero2 [simp] -lemma rcis_zero_mod: "rcis 0 a = 0" +lemma rcis_zero_mod [simp]: "rcis 0 a = 0" by (simp add: rcis_def) -declare rcis_zero_mod [simp] -lemma rcis_zero_arg: "rcis r 0 = complex_of_real r" +lemma rcis_zero_arg [simp]: "rcis r 0 = complex_of_real r" by (simp add: rcis_def) -declare rcis_zero_arg [simp] lemma complex_of_real_minus_one: "complex_of_real (-(1::real)) = -(1::complex)" apply (simp add: complex_of_real_def complex_one_def complex_minus) done -lemma complex_i_mult_minus: "ii * (ii * x) = - x" +lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x" by (simp add: complex_mult_assoc [symmetric]) -declare complex_i_mult_minus [simp] lemma cis_real_of_nat_Suc_mult: @@ -916,20 +844,19 @@ apply (auto simp add: cis_real_of_nat_Suc_mult) done -lemma DeMoivre2: - "(rcis r a) ^ n = rcis (r ^ n) (real n * a)" -apply (simp add: rcis_def power_mult_distrib DeMoivre complex_of_real_pow) -done +lemma DeMoivre2: "(rcis r a) ^ n = rcis (r ^ n) (real n * a)" +by (simp add: rcis_def power_mult_distrib DeMoivre complex_of_real_pow) -lemma cis_inverse: "inverse(cis a) = cis (-a)" -by (simp add: cis_def complex_inverse_complex_split complex_of_real_minus complex_diff_def) -declare cis_inverse [simp] +lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)" +by (simp add: cis_def complex_inverse_complex_split complex_of_real_minus + complex_diff_def) lemma rcis_inverse: "inverse(rcis r a) = rcis (1/r) (-a)" apply (case_tac "r=0", simp) -apply (auto simp add: complex_inverse_complex_split right_distrib +apply (auto simp add: complex_inverse_complex_split right_distrib complex_of_real_mult rcis_def cis_def power2_eq_square mult_ac) -apply (auto simp add: right_distrib [symmetric] complex_of_real_minus complex_diff_def) +apply (auto simp add: right_distrib [symmetric] complex_of_real_minus + complex_diff_def) done lemma cis_divide: "cis a / cis b = cis (a - b)" @@ -941,13 +868,11 @@ apply (simp add: rcis_inverse rcis_mult real_diff_def) done -lemma Re_cis: "Re(cis a) = cos a" +lemma Re_cis [simp]: "Re(cis a) = cos a" by (simp add: cis_def) -declare Re_cis [simp] -lemma Im_cis: "Im(cis a) = sin a" +lemma Im_cis [simp]: "Im(cis a) = sin a" by (simp add: cis_def) -declare Im_cis [simp] lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)" by (auto simp add: DeMoivre) @@ -965,16 +890,16 @@ by (simp add: expi_def) lemma expi_add: "expi(a + b) = expi(a) * expi(b)" -by (simp add: expi_def complex_Re_add exp_add complex_Im_add cis_mult [symmetric] complex_of_real_mult mult_ac) +by (simp add: expi_def complex_Re_add exp_add complex_Im_add + cis_mult [symmetric] complex_of_real_mult mult_ac) lemma expi_complex_split: "expi(complex_of_real x + ii * complex_of_real y) = complex_of_real (exp(x)) * cis y" by (simp add: expi_def) -lemma expi_zero: "expi (0::complex) = 1" +lemma expi_zero [simp]: "expi (0::complex) = 1" by (simp add: expi_def) -declare expi_zero [simp] lemma complex_Re_mult_eq: "Re (w * z) = Re w * Re z - Im w * Im z" by (induct z, induct w, simp add: complex_mult) @@ -984,8 +909,7 @@ apply (induct z, induct w, simp add: complex_mult) done -lemma complex_expi_Ex: - "\a r. z = complex_of_real r * expi a" +lemma complex_expi_Ex: "\a r. z = complex_of_real r * expi a" apply (insert rcis_Ex [of z]) apply (auto simp add: expi_def rcis_def complex_mult_assoc [symmetric] complex_of_real_mult) apply (rule_tac x = "ii * complex_of_real a" in exI, auto) @@ -1023,17 +947,11 @@ val complex_Im_one = thm"complex_Im_one"; val complex_Re_i = thm"complex_Re_i"; val complex_Im_i = thm"complex_Im_i"; -val Re_complex_of_real_zero = thm"Re_complex_of_real_zero"; -val Im_complex_of_real_zero = thm"Im_complex_of_real_zero"; -val Re_complex_of_real_one = thm"Re_complex_of_real_one"; -val Im_complex_of_real_one = thm"Im_complex_of_real_one"; val Re_complex_of_real = thm"Re_complex_of_real"; val Im_complex_of_real = thm"Im_complex_of_real"; val complex_minus = thm"complex_minus"; val complex_Re_minus = thm"complex_Re_minus"; val complex_Im_minus = thm"complex_Im_minus"; -val complex_minus_zero = thm"complex_minus_zero"; -val complex_minus_zero_iff = thm"complex_minus_zero_iff"; val complex_add = thm"complex_add"; val complex_Re_add = thm"complex_Re_add"; val complex_Im_add = thm"complex_Im_add"; @@ -1079,9 +997,6 @@ val complex_cnj_zero = thm"complex_cnj_zero"; val complex_cnj_zero_iff = thm"complex_cnj_zero_iff"; val complex_mult_cnj = thm"complex_mult_cnj"; -val complex_add_left_cancel_zero = thm"complex_add_left_cancel_zero"; -val complex_diff_mult_distrib = thm"complex_diff_mult_distrib"; -val complex_diff_mult_distrib2 = thm"complex_diff_mult_distrib2"; val complex_mod_eq_zero_cancel = thm"complex_mod_eq_zero_cancel"; val complex_mod_complex_of_real_of_nat = thm"complex_mod_complex_of_real_of_nat"; val complex_mod_minus = thm"complex_mod_minus"; diff -r 67a628beb981 -r 61de62096768 src/HOL/Complex/NSCA.ML --- a/src/HOL/Complex/NSCA.ML Tue Feb 03 11:06:36 2004 +0100 +++ b/src/HOL/Complex/NSCA.ML Tue Feb 03 15:58:31 2004 +0100 @@ -493,13 +493,13 @@ Goal "[| y: CInfinitesimal; x + y = z |] ==> x @c= z"; by (rtac (bex_CInfinitesimal_iff RS iffD1) 1); by (dtac (CInfinitesimal_minus_iff RS iffD2) 1); -by (auto_tac (claset(), simpset() addsimps [hcomplex_add_assoc RS sym])); +by (asm_full_simp_tac (simpset() addsimps eq_commute::compare_rls) 1); qed "CInfinitesimal_add_capprox"; Goal "y: CInfinitesimal ==> x @c= x + y"; by (rtac (bex_CInfinitesimal_iff RS iffD1) 1); by (dtac (CInfinitesimal_minus_iff RS iffD2) 1); -by (auto_tac (claset(), simpset() addsimps [hcomplex_add_assoc RS sym])); +by (asm_full_simp_tac (simpset() addsimps eq_commute::compare_rls) 1); qed "CInfinitesimal_add_capprox_self"; Goal "y: CInfinitesimal ==> x @c= y + x"; diff -r 67a628beb981 -r 61de62096768 src/HOL/Complex/NSComplex.thy --- a/src/HOL/Complex/NSComplex.thy Tue Feb 03 11:06:36 2004 +0100 +++ b/src/HOL/Complex/NSComplex.thy Tue Feb 03 15:58:31 2004 +0100 @@ -127,38 +127,26 @@ hcomplexrel `` {%n. (X n) ^ (Y n)})" -lemma hcomplexrel_iff: - "((X,Y): hcomplexrel) = ({n. X n = Y n}: FreeUltrafilterNat)" -apply (unfold hcomplexrel_def) -apply fast -done - lemma hcomplexrel_refl: "(x,x): hcomplexrel" -apply (simp add: hcomplexrel_iff) -done +by (simp add: hcomplexrel_def) lemma hcomplexrel_sym: "(x,y): hcomplexrel ==> (y,x):hcomplexrel" -apply (auto simp add: hcomplexrel_iff eq_commute) -done +by (auto simp add: hcomplexrel_def eq_commute) lemma hcomplexrel_trans: "[|(x,y): hcomplexrel; (y,z):hcomplexrel|] ==> (x,z):hcomplexrel" -apply (simp add: hcomplexrel_iff) -apply ultra -done +by (simp add: hcomplexrel_def, ultra) lemma equiv_hcomplexrel: "equiv UNIV hcomplexrel" -apply (simp add: equiv_def refl_def sym_def trans_def hcomplexrel_refl) -apply (blast intro: hcomplexrel_sym hcomplexrel_trans) +apply (simp add: equiv_def refl_def sym_def trans_def hcomplexrel_refl) +apply (blast intro: hcomplexrel_sym hcomplexrel_trans) done lemmas equiv_hcomplexrel_iff = eq_equiv_class_iff [OF equiv_hcomplexrel UNIV_I UNIV_I, simp] lemma hcomplexrel_in_hcomplex [simp]: "hcomplexrel``{x} : hcomplex" -apply (unfold hcomplex_def hcomplexrel_def quotient_def) -apply blast -done +by (simp add: hcomplex_def hcomplexrel_def quotient_def, blast) lemma inj_on_Abs_hcomplex: "inj_on Abs_hcomplex hcomplex" apply (rule inj_on_inverseI) @@ -170,216 +158,188 @@ declare equiv_hcomplexrel [THEN eq_equiv_class_iff, simp] -declare hcomplexrel_iff [iff] lemma inj_Rep_hcomplex: "inj(Rep_hcomplex)" apply (rule inj_on_inverseI) apply (rule Rep_hcomplex_inverse) done -lemma lemma_hcomplexrel_refl: "x: hcomplexrel `` {x}" -apply (unfold hcomplexrel_def) -apply (safe) -apply auto -done -declare lemma_hcomplexrel_refl [simp] +lemma lemma_hcomplexrel_refl [simp]: "x: hcomplexrel `` {x}" +by (simp add: hcomplexrel_def) -lemma hcomplex_empty_not_mem: "{} \ hcomplex" -apply (unfold hcomplex_def) +lemma hcomplex_empty_not_mem [simp]: "{} \ hcomplex" +apply (simp add: hcomplex_def hcomplexrel_def) apply (auto elim!: quotientE) done -declare hcomplex_empty_not_mem [simp] -lemma Rep_hcomplex_nonempty: "Rep_hcomplex x \ {}" -apply (cut_tac x = "x" in Rep_hcomplex) -apply auto -done -declare Rep_hcomplex_nonempty [simp] +lemma Rep_hcomplex_nonempty [simp]: "Rep_hcomplex x \ {}" +by (cut_tac x = x in Rep_hcomplex, auto) lemma eq_Abs_hcomplex: "(!!x. z = Abs_hcomplex(hcomplexrel `` {x}) ==> P) ==> P" apply (rule_tac x1=z in Rep_hcomplex [unfolded hcomplex_def, THEN quotientE]) apply (drule_tac f = Abs_hcomplex in arg_cong) -apply (force simp add: Rep_hcomplex_inverse) +apply (force simp add: Rep_hcomplex_inverse hcomplexrel_def) done +(*??delete*) +lemma hcomplexrel_iff [iff]: + "((X,Y): hcomplexrel) = ({n. X n = Y n}: FreeUltrafilterNat)" +by (simp add: hcomplexrel_def) + subsection{*Properties of Nonstandard Real and Imaginary Parts*} lemma hRe: "hRe(Abs_hcomplex (hcomplexrel `` {X})) = Abs_hypreal(hyprel `` {%n. Re(X n)})" -apply (unfold hRe_def) -apply (rule_tac f = "Abs_hypreal" in arg_cong) -apply (auto , ultra) +apply (simp add: hRe_def) +apply (rule_tac f = Abs_hypreal in arg_cong) +apply (auto, ultra) done lemma hIm: "hIm(Abs_hcomplex (hcomplexrel `` {X})) = Abs_hypreal(hyprel `` {%n. Im(X n)})" -apply (unfold hIm_def) -apply (rule_tac f = "Abs_hypreal" in arg_cong) -apply (auto , ultra) +apply (simp add: hIm_def) +apply (rule_tac f = Abs_hypreal in arg_cong) +apply (auto, ultra) done lemma hcomplex_hRe_hIm_cancel_iff: "(w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (rule_tac z = "w" in eq_Abs_hcomplex) +apply (rule eq_Abs_hcomplex [of z]) +apply (rule eq_Abs_hcomplex [of w]) apply (auto simp add: hRe hIm complex_Re_Im_cancel_iff) apply (ultra+) done -lemma hcomplex_hRe_zero: "hRe 0 = 0" -apply (unfold hcomplex_zero_def) -apply (simp (no_asm) add: hRe hypreal_zero_num) -done -declare hcomplex_hRe_zero [simp] +lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0" +by (simp add: hcomplex_zero_def hRe hypreal_zero_num) -lemma hcomplex_hIm_zero: "hIm 0 = 0" -apply (unfold hcomplex_zero_def) -apply (simp (no_asm) add: hIm hypreal_zero_num) -done -declare hcomplex_hIm_zero [simp] +lemma hcomplex_hIm_zero [simp]: "hIm 0 = 0" +by (simp add: hcomplex_zero_def hIm hypreal_zero_num) -lemma hcomplex_hRe_one: "hRe 1 = 1" -apply (unfold hcomplex_one_def) -apply (simp (no_asm) add: hRe hypreal_one_num) -done -declare hcomplex_hRe_one [simp] +lemma hcomplex_hRe_one [simp]: "hRe 1 = 1" +by (simp add: hcomplex_one_def hRe hypreal_one_num) -lemma hcomplex_hIm_one: "hIm 1 = 0" -apply (unfold hcomplex_one_def) -apply (simp (no_asm) add: hIm hypreal_one_def hypreal_zero_num) -done -declare hcomplex_hIm_one [simp] +lemma hcomplex_hIm_one [simp]: "hIm 1 = 0" +by (simp add: hcomplex_one_def hIm hypreal_one_def hypreal_zero_num) subsection{*Addition for Nonstandard Complex Numbers*} lemma hcomplex_add_congruent2: "congruent2 hcomplexrel (%X Y. hcomplexrel `` {%n. X n + Y n})" -apply (unfold congruent2_def) -apply safe -apply (ultra+) -done +by (auto simp add: congruent2_def, ultra) lemma hcomplex_add: "Abs_hcomplex(hcomplexrel``{%n. X n}) + Abs_hcomplex(hcomplexrel``{%n. Y n}) = Abs_hcomplex(hcomplexrel``{%n. X n + Y n})" -apply (unfold hcomplex_add_def) -apply (rule_tac f = "Abs_hcomplex" in arg_cong) +apply (simp add: hcomplex_add_def) +apply (rule_tac f = Abs_hcomplex in arg_cong) apply (auto, ultra) done lemma hcomplex_add_commute: "(z::hcomplex) + w = w + z" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (rule_tac z = "w" in eq_Abs_hcomplex) +apply (rule eq_Abs_hcomplex [of z]) +apply (rule eq_Abs_hcomplex [of w]) apply (simp add: complex_add_commute hcomplex_add) done lemma hcomplex_add_assoc: "((z1::hcomplex) + z2) + z3 = z1 + (z2 + z3)" -apply (rule_tac z = "z1" in eq_Abs_hcomplex) -apply (rule_tac z = "z2" in eq_Abs_hcomplex) -apply (rule_tac z = "z3" in eq_Abs_hcomplex) +apply (rule eq_Abs_hcomplex [of z1]) +apply (rule eq_Abs_hcomplex [of z2]) +apply (rule eq_Abs_hcomplex [of z3]) apply (simp add: hcomplex_add complex_add_assoc) done lemma hcomplex_add_zero_left: "(0::hcomplex) + z = z" -apply (unfold hcomplex_zero_def) -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (simp add: hcomplex_add) +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: hcomplex_zero_def hcomplex_add) done lemma hcomplex_add_zero_right: "z + (0::hcomplex) = z" -apply (simp add: hcomplex_add_zero_left hcomplex_add_commute) -done +by (simp add: hcomplex_add_zero_left hcomplex_add_commute) lemma hRe_add: "hRe(x + y) = hRe(x) + hRe(y)" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (rule_tac z = "y" in eq_Abs_hcomplex) -apply (auto simp add: hRe hcomplex_add hypreal_add complex_Re_add) +apply (rule eq_Abs_hcomplex [of x]) +apply (rule eq_Abs_hcomplex [of y]) +apply (simp add: hRe hcomplex_add hypreal_add complex_Re_add) done lemma hIm_add: "hIm(x + y) = hIm(x) + hIm(y)" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (rule_tac z = "y" in eq_Abs_hcomplex) -apply (auto simp add: hIm hcomplex_add hypreal_add complex_Im_add) +apply (rule eq_Abs_hcomplex [of x]) +apply (rule eq_Abs_hcomplex [of y]) +apply (simp add: hIm hcomplex_add hypreal_add complex_Im_add) done subsection{*Additive Inverse on Nonstandard Complex Numbers*} lemma hcomplex_minus_congruent: - "congruent hcomplexrel (%X. hcomplexrel `` {%n. - (X n)})" -apply (unfold congruent_def) -apply safe -apply (ultra+) -done + "congruent hcomplexrel (%X. hcomplexrel `` {%n. - (X n)})" +by (simp add: congruent_def) lemma hcomplex_minus: "- (Abs_hcomplex(hcomplexrel `` {%n. X n})) = Abs_hcomplex(hcomplexrel `` {%n. -(X n)})" -apply (unfold hcomplex_minus_def) -apply (rule_tac f = "Abs_hcomplex" in arg_cong) +apply (simp add: hcomplex_minus_def) +apply (rule_tac f = Abs_hcomplex in arg_cong) apply (auto, ultra) done lemma hcomplex_add_minus_left: "-z + z = (0::hcomplex)" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hcomplex_add hcomplex_minus hcomplex_zero_def) +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: hcomplex_add hcomplex_minus hcomplex_zero_def) done subsection{*Multiplication for Nonstandard Complex Numbers*} lemma hcomplex_mult: - "Abs_hcomplex(hcomplexrel``{%n. X n}) * + "Abs_hcomplex(hcomplexrel``{%n. X n}) * Abs_hcomplex(hcomplexrel``{%n. Y n}) = - Abs_hcomplex(hcomplexrel``{%n. X n * Y n})" -apply (unfold hcomplex_mult_def) -apply (rule_tac f = "Abs_hcomplex" in arg_cong) + Abs_hcomplex(hcomplexrel``{%n. X n * Y n})" +apply (simp add: hcomplex_mult_def) +apply (rule_tac f = Abs_hcomplex in arg_cong) apply (auto, ultra) done lemma hcomplex_mult_commute: "(w::hcomplex) * z = z * w" -apply (rule_tac z = "w" in eq_Abs_hcomplex) -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hcomplex_mult complex_mult_commute) +apply (rule eq_Abs_hcomplex [of w]) +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: hcomplex_mult complex_mult_commute) done lemma hcomplex_mult_assoc: "((u::hcomplex) * v) * w = u * (v * w)" -apply (rule_tac z = "u" in eq_Abs_hcomplex) -apply (rule_tac z = "v" in eq_Abs_hcomplex) -apply (rule_tac z = "w" in eq_Abs_hcomplex) -apply (auto simp add: hcomplex_mult complex_mult_assoc) +apply (rule eq_Abs_hcomplex [of u]) +apply (rule eq_Abs_hcomplex [of v]) +apply (rule eq_Abs_hcomplex [of w]) +apply (simp add: hcomplex_mult complex_mult_assoc) done lemma hcomplex_mult_one_left: "(1::hcomplex) * z = z" -apply (unfold hcomplex_one_def) -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hcomplex_mult) +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: hcomplex_one_def hcomplex_mult) done lemma hcomplex_mult_zero_left: "(0::hcomplex) * z = 0" -apply (unfold hcomplex_zero_def) -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hcomplex_mult) +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: hcomplex_zero_def hcomplex_mult) done lemma hcomplex_add_mult_distrib: "((z1::hcomplex) + z2) * w = (z1 * w) + (z2 * w)" -apply (rule_tac z = "z1" in eq_Abs_hcomplex) -apply (rule_tac z = "z2" in eq_Abs_hcomplex) -apply (rule_tac z = "w" in eq_Abs_hcomplex) -apply (auto simp add: hcomplex_mult hcomplex_add left_distrib) +apply (rule eq_Abs_hcomplex [of z1]) +apply (rule eq_Abs_hcomplex [of z2]) +apply (rule eq_Abs_hcomplex [of w]) +apply (simp add: hcomplex_mult hcomplex_add left_distrib) done lemma hcomplex_zero_not_eq_one: "(0::hcomplex) \ (1::hcomplex)" -apply (unfold hcomplex_zero_def hcomplex_one_def) -apply auto -done -declare hcomplex_zero_not_eq_one [simp] +by (simp add: hcomplex_zero_def hcomplex_one_def) + declare hcomplex_zero_not_eq_one [THEN not_sym, simp] @@ -388,20 +348,17 @@ lemma hcomplex_inverse: "inverse (Abs_hcomplex(hcomplexrel `` {%n. X n})) = Abs_hcomplex(hcomplexrel `` {%n. inverse (X n)})" -apply (unfold hcinv_def) -apply (rule_tac f = "Abs_hcomplex" in arg_cong) +apply (simp add: hcinv_def) +apply (rule_tac f = Abs_hcomplex in arg_cong) apply (auto, ultra) done lemma hcomplex_mult_inv_left: "z \ (0::hcomplex) ==> inverse(z) * z = (1::hcomplex)" -apply (unfold hcomplex_zero_def hcomplex_one_def) -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hcomplex_inverse hcomplex_mult) -apply (ultra) +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: hcomplex_zero_def hcomplex_one_def hcomplex_inverse hcomplex_mult, ultra) apply (rule ccontr) -apply (drule left_inverse) -apply auto +apply (drule left_inverse, auto) done subsection {* The Field of Nonstandard Complex Numbers *} @@ -431,9 +388,9 @@ by (simp add: hcomplex_add_mult_distrib) show "z+u = z+v ==> u=v" proof - - assume eq: "z+u = z+v" + assume eq: "z+u = z+v" hence "(-z + z) + u = (-z + z) + v" by (simp only: eq hcomplex_add_assoc) - thus "u = v" + thus "u = v" by (simp only: hcomplex_add_minus_left hcomplex_add_zero_left) qed assume neq: "w \ 0" @@ -443,71 +400,53 @@ by (rule hcomplex_mult_inv_left) qed -lemma HCOMPLEX_INVERSE_ZERO: "inverse (0::hcomplex) = 0" -apply (simp add: hcomplex_zero_def hcomplex_inverse) -done - -lemma HCOMPLEX_DIVISION_BY_ZERO: "a / (0::hcomplex) = 0" -apply (simp add: hcomplex_divide_def HCOMPLEX_INVERSE_ZERO) -done - instance hcomplex :: division_by_zero proof + show inv: "inverse 0 = (0::hcomplex)" + by (simp add: hcomplex_inverse hcomplex_zero_def) fix x :: hcomplex - show "inverse 0 = (0::hcomplex)" by (rule HCOMPLEX_INVERSE_ZERO) - show "x/0 = 0" by (rule HCOMPLEX_DIVISION_BY_ZERO) + show "x/0 = 0" + by (simp add: hcomplex_divide_def inv) qed + subsection{*More Minus Laws*} -lemma inj_hcomplex_minus: "inj(%z::hcomplex. -z)" -apply (rule inj_onI) -apply (drule_tac f = "uminus" in arg_cong) -apply simp -done - lemma hRe_minus: "hRe(-z) = - hRe(z)" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hRe hcomplex_minus hypreal_minus complex_Re_minus) +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: hRe hcomplex_minus hypreal_minus complex_Re_minus) done lemma hIm_minus: "hIm(-z) = - hIm(z)" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hIm hcomplex_minus hypreal_minus complex_Im_minus) +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: hIm hcomplex_minus hypreal_minus complex_Im_minus) done lemma hcomplex_add_minus_eq_minus: "x + y = (0::hcomplex) ==> x = -y" -apply (drule Ring_and_Field.equals_zero_I) -apply (simp add: minus_equation_iff [of x y]) +apply (drule Ring_and_Field.equals_zero_I) +apply (simp add: minus_equation_iff [of x y]) done subsection{*More Multiplication Laws*} lemma hcomplex_mult_one_right: "z * (1::hcomplex) = z" -apply (rule Ring_and_Field.mult_1_right) -done +by (rule Ring_and_Field.mult_1_right) -lemma hcomplex_mult_minus_one: "- 1 * (z::hcomplex) = -z" -apply (simp (no_asm)) -done -declare hcomplex_mult_minus_one [simp] +lemma hcomplex_mult_minus_one [simp]: "- 1 * (z::hcomplex) = -z" +by simp -lemma hcomplex_mult_minus_one_right: "(z::hcomplex) * - 1 = -z" -apply (subst hcomplex_mult_commute) -apply (simp (no_asm)) -done -declare hcomplex_mult_minus_one_right [simp] +lemma hcomplex_mult_minus_one_right [simp]: "(z::hcomplex) * - 1 = -z" +by (subst hcomplex_mult_commute, simp) lemma hcomplex_mult_left_cancel: "(c::hcomplex) \ (0::hcomplex) ==> (c*a=c*b) = (a=b)" -by (simp add: field_mult_cancel_left) +by (simp add: field_mult_cancel_left) lemma hcomplex_mult_right_cancel: "(c::hcomplex) \ (0::hcomplex) ==> (a*c=b*c) = (a=b)" -apply (simp add: Ring_and_Field.field_mult_cancel_right); -done +by (simp add: Ring_and_Field.field_mult_cancel_right) subsection{*Subraction and Division*} @@ -515,17 +454,13 @@ lemma hcomplex_diff: "Abs_hcomplex(hcomplexrel``{%n. X n}) - Abs_hcomplex(hcomplexrel``{%n. Y n}) = Abs_hcomplex(hcomplexrel``{%n. X n - Y n})" -apply (unfold hcomplex_diff_def) -apply (auto simp add: hcomplex_minus hcomplex_add complex_diff_def) -done +by (simp add: hcomplex_diff_def hcomplex_minus hcomplex_add complex_diff_def) -lemma hcomplex_diff_eq_eq: "((x::hcomplex) - y = z) = (x = z + y)" -apply (rule Ring_and_Field.diff_eq_eq) -done +lemma hcomplex_diff_eq_eq [simp]: "((x::hcomplex) - y = z) = (x = z + y)" +by (rule Ring_and_Field.diff_eq_eq) lemma hcomplex_add_divide_distrib: "(x+y)/(z::hcomplex) = x/z + y/z" -apply (rule Ring_and_Field.add_divide_distrib) -done +by (rule Ring_and_Field.add_divide_distrib) subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*} @@ -533,98 +468,77 @@ lemma hcomplex_of_hypreal: "hcomplex_of_hypreal (Abs_hypreal(hyprel `` {%n. X n})) = Abs_hcomplex(hcomplexrel `` {%n. complex_of_real (X n)})" -apply (unfold hcomplex_of_hypreal_def) -apply (rule_tac f = "Abs_hcomplex" in arg_cong) -apply auto -apply (ultra) +apply (simp add: hcomplex_of_hypreal_def) +apply (rule_tac f = Abs_hcomplex in arg_cong, auto, ultra) done -lemma inj_hcomplex_of_hypreal: "inj hcomplex_of_hypreal" -apply (rule inj_onI) -apply (rule_tac z = "x" in eq_Abs_hypreal) -apply (rule_tac z = "y" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_of_hypreal) +lemma hcomplex_of_hypreal_cancel_iff [iff]: + "(hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)" +apply (rule eq_Abs_hypreal [of x]) +apply (rule eq_Abs_hypreal [of y]) +apply (simp add: hcomplex_of_hypreal) done -lemma hcomplex_of_hypreal_cancel_iff: - "(hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)" -apply (auto dest: inj_hcomplex_of_hypreal [THEN injD]) -done -declare hcomplex_of_hypreal_cancel_iff [iff] - lemma hcomplex_of_hypreal_minus: "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x" -apply (rule_tac z = "x" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus complex_of_real_minus) +apply (rule eq_Abs_hypreal [of x]) +apply (simp add: hcomplex_of_hypreal hcomplex_minus hypreal_minus complex_of_real_minus) done lemma hcomplex_of_hypreal_inverse: "hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)" -apply (rule_tac z = "x" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse complex_of_real_inverse) +apply (rule eq_Abs_hypreal [of x]) +apply (simp add: hcomplex_of_hypreal hypreal_inverse hcomplex_inverse complex_of_real_inverse) done lemma hcomplex_of_hypreal_add: "hcomplex_of_hypreal x + hcomplex_of_hypreal y = hcomplex_of_hypreal (x + y)" -apply (rule_tac z = "x" in eq_Abs_hypreal) -apply (rule_tac z = "y" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_of_hypreal hypreal_add hcomplex_add complex_of_real_add) +apply (rule eq_Abs_hypreal [of x]) +apply (rule eq_Abs_hypreal [of y]) +apply (simp add: hcomplex_of_hypreal hypreal_add hcomplex_add complex_of_real_add) done lemma hcomplex_of_hypreal_diff: "hcomplex_of_hypreal x - hcomplex_of_hypreal y = hcomplex_of_hypreal (x - y)" -apply (unfold hcomplex_diff_def) -apply (auto simp add: hcomplex_of_hypreal_minus [symmetric] hcomplex_of_hypreal_add hypreal_diff_def) -done +by (simp add: hcomplex_diff_def hcomplex_of_hypreal_minus [symmetric] hcomplex_of_hypreal_add hypreal_diff_def) lemma hcomplex_of_hypreal_mult: "hcomplex_of_hypreal x * hcomplex_of_hypreal y = hcomplex_of_hypreal (x * y)" -apply (rule_tac z = "x" in eq_Abs_hypreal) -apply (rule_tac z = "y" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult - complex_of_real_mult) +apply (rule eq_Abs_hypreal [of x]) +apply (rule eq_Abs_hypreal [of y]) +apply (simp add: hcomplex_of_hypreal hypreal_mult hcomplex_mult complex_of_real_mult) done lemma hcomplex_of_hypreal_divide: "hcomplex_of_hypreal x / hcomplex_of_hypreal y = hcomplex_of_hypreal(x/y)" -apply (unfold hcomplex_divide_def) -apply (case_tac "y=0") -apply (simp) +apply (simp add: hcomplex_divide_def) +apply (case_tac "y=0", simp) apply (auto simp add: hcomplex_of_hypreal_mult hcomplex_of_hypreal_inverse [symmetric]) -apply (simp (no_asm) add: hypreal_divide_def) -done - -lemma hcomplex_of_hypreal_one [simp]: - "hcomplex_of_hypreal 1 = 1" -apply (unfold hcomplex_one_def) -apply (auto simp add: hcomplex_of_hypreal hypreal_one_num) +apply (simp add: hypreal_divide_def) done -lemma hcomplex_of_hypreal_zero [simp]: - "hcomplex_of_hypreal 0 = 0" -apply (unfold hcomplex_zero_def hypreal_zero_def) -apply (auto simp add: hcomplex_of_hypreal) -done +lemma hcomplex_of_hypreal_one [simp]: "hcomplex_of_hypreal 1 = 1" +by (simp add: hcomplex_one_def hcomplex_of_hypreal hypreal_one_num) -lemma hRe_hcomplex_of_hypreal: "hRe(hcomplex_of_hypreal z) = z" -apply (rule_tac z = "z" in eq_Abs_hypreal) +lemma hcomplex_of_hypreal_zero [simp]: "hcomplex_of_hypreal 0 = 0" +by (simp add: hcomplex_zero_def hypreal_zero_def hcomplex_of_hypreal) + +lemma hRe_hcomplex_of_hypreal [simp]: "hRe(hcomplex_of_hypreal z) = z" +apply (rule eq_Abs_hypreal [of z]) apply (auto simp add: hcomplex_of_hypreal hRe) done -declare hRe_hcomplex_of_hypreal [simp] -lemma hIm_hcomplex_of_hypreal: "hIm(hcomplex_of_hypreal z) = 0" -apply (rule_tac z = "z" in eq_Abs_hypreal) +lemma hIm_hcomplex_of_hypreal [simp]: "hIm(hcomplex_of_hypreal z) = 0" +apply (rule eq_Abs_hypreal [of z]) apply (auto simp add: hcomplex_of_hypreal hIm hypreal_zero_num) done -declare hIm_hcomplex_of_hypreal [simp] -lemma hcomplex_of_hypreal_epsilon_not_zero: "hcomplex_of_hypreal epsilon \ 0" -apply (auto simp add: hcomplex_of_hypreal epsilon_def hcomplex_zero_def) -done -declare hcomplex_of_hypreal_epsilon_not_zero [simp] +lemma hcomplex_of_hypreal_epsilon_not_zero [simp]: + "hcomplex_of_hypreal epsilon \ 0" +by (auto simp add: hcomplex_of_hypreal epsilon_def hcomplex_zero_def) subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*} @@ -633,35 +547,27 @@ "hcmod (Abs_hcomplex(hcomplexrel `` {%n. X n})) = Abs_hypreal(hyprel `` {%n. cmod (X n)})" -apply (unfold hcmod_def) -apply (rule_tac f = "Abs_hypreal" in arg_cong) +apply (simp add: hcmod_def) +apply (rule_tac f = Abs_hypreal in arg_cong) apply (auto, ultra) done -lemma hcmod_zero [simp]: - "hcmod(0) = 0" -apply (unfold hcomplex_zero_def hypreal_zero_def) -apply (auto simp add: hcmod) +lemma hcmod_zero [simp]: "hcmod(0) = 0" +apply (simp add: hcomplex_zero_def hypreal_zero_def hcmod) done -lemma hcmod_one: - "hcmod(1) = 1" -apply (unfold hcomplex_one_def) -apply (auto simp add: hcmod hypreal_one_num) -done -declare hcmod_one [simp] +lemma hcmod_one [simp]: "hcmod(1) = 1" +by (simp add: hcomplex_one_def hcmod hypreal_one_num) -lemma hcmod_hcomplex_of_hypreal: "hcmod(hcomplex_of_hypreal x) = abs x" -apply (rule_tac z = "x" in eq_Abs_hypreal) +lemma hcmod_hcomplex_of_hypreal [simp]: "hcmod(hcomplex_of_hypreal x) = abs x" +apply (rule eq_Abs_hypreal [of x]) apply (auto simp add: hcmod hcomplex_of_hypreal hypreal_hrabs) done -declare hcmod_hcomplex_of_hypreal [simp] lemma hcomplex_of_hypreal_abs: "hcomplex_of_hypreal (abs x) = hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))" -apply (simp (no_asm)) -done +by simp subsection{*Conjugation*} @@ -669,232 +575,198 @@ lemma hcnj: "hcnj (Abs_hcomplex(hcomplexrel `` {%n. X n})) = Abs_hcomplex(hcomplexrel `` {%n. cnj(X n)})" -apply (unfold hcnj_def) -apply (rule_tac f = "Abs_hcomplex" in arg_cong) +apply (simp add: hcnj_def) +apply (rule_tac f = Abs_hcomplex in arg_cong) apply (auto, ultra) done -lemma inj_hcnj: "inj hcnj" -apply (rule inj_onI) -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (rule_tac z = "y" in eq_Abs_hcomplex) -apply (auto simp add: hcnj) +lemma hcomplex_hcnj_cancel_iff [iff]: "(hcnj x = hcnj y) = (x = y)" +apply (rule eq_Abs_hcomplex [of x]) +apply (rule eq_Abs_hcomplex [of y]) +apply (simp add: hcnj) +done + +lemma hcomplex_hcnj_hcnj [simp]: "hcnj (hcnj z) = z" +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: hcnj) done -lemma hcomplex_hcnj_cancel_iff: "(hcnj x = hcnj y) = (x = y)" -apply (auto dest: inj_hcnj [THEN injD]) +lemma hcomplex_hcnj_hcomplex_of_hypreal [simp]: + "hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x" +apply (rule eq_Abs_hypreal [of x]) +apply (simp add: hcnj hcomplex_of_hypreal) done -declare hcomplex_hcnj_cancel_iff [simp] - -lemma hcomplex_hcnj_hcnj: "hcnj (hcnj z) = z" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hcnj) -done -declare hcomplex_hcnj_hcnj [simp] -lemma hcomplex_hcnj_hcomplex_of_hypreal: - "hcnj (hcomplex_of_hypreal x) = hcomplex_of_hypreal x" -apply (rule_tac z = "x" in eq_Abs_hypreal) -apply (auto simp add: hcnj hcomplex_of_hypreal) +lemma hcomplex_hmod_hcnj [simp]: "hcmod (hcnj z) = hcmod z" +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: hcnj hcmod) done -declare hcomplex_hcnj_hcomplex_of_hypreal [simp] - -lemma hcomplex_hmod_hcnj: "hcmod (hcnj z) = hcmod z" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hcnj hcmod) -done -declare hcomplex_hmod_hcnj [simp] lemma hcomplex_hcnj_minus: "hcnj (-z) = - hcnj z" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hcnj hcomplex_minus complex_cnj_minus) +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: hcnj hcomplex_minus complex_cnj_minus) done lemma hcomplex_hcnj_inverse: "hcnj(inverse z) = inverse(hcnj z)" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hcnj hcomplex_inverse complex_cnj_inverse) +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: hcnj hcomplex_inverse complex_cnj_inverse) done lemma hcomplex_hcnj_add: "hcnj(w + z) = hcnj(w) + hcnj(z)" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (rule_tac z = "w" in eq_Abs_hcomplex) -apply (auto simp add: hcnj hcomplex_add complex_cnj_add) +apply (rule eq_Abs_hcomplex [of z]) +apply (rule eq_Abs_hcomplex [of w]) +apply (simp add: hcnj hcomplex_add complex_cnj_add) done lemma hcomplex_hcnj_diff: "hcnj(w - z) = hcnj(w) - hcnj(z)" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (rule_tac z = "w" in eq_Abs_hcomplex) -apply (auto simp add: hcnj hcomplex_diff complex_cnj_diff) +apply (rule eq_Abs_hcomplex [of z]) +apply (rule eq_Abs_hcomplex [of w]) +apply (simp add: hcnj hcomplex_diff complex_cnj_diff) done lemma hcomplex_hcnj_mult: "hcnj(w * z) = hcnj(w) * hcnj(z)" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (rule_tac z = "w" in eq_Abs_hcomplex) -apply (auto simp add: hcnj hcomplex_mult complex_cnj_mult) +apply (rule eq_Abs_hcomplex [of z]) +apply (rule eq_Abs_hcomplex [of w]) +apply (simp add: hcnj hcomplex_mult complex_cnj_mult) done lemma hcomplex_hcnj_divide: "hcnj(w / z) = (hcnj w)/(hcnj z)" -apply (unfold hcomplex_divide_def) -apply (simp (no_asm) add: hcomplex_hcnj_mult hcomplex_hcnj_inverse) -done +by (simp add: hcomplex_divide_def hcomplex_hcnj_mult hcomplex_hcnj_inverse) -lemma hcnj_one: "hcnj 1 = 1" -apply (unfold hcomplex_one_def) -apply (simp (no_asm) add: hcnj) -done -declare hcnj_one [simp] +lemma hcnj_one [simp]: "hcnj 1 = 1" +by (simp add: hcomplex_one_def hcnj) -lemma hcomplex_hcnj_zero: - "hcnj 0 = 0" -apply (unfold hcomplex_zero_def) -apply (auto simp add: hcnj) +lemma hcomplex_hcnj_zero [simp]: "hcnj 0 = 0" +by (simp add: hcomplex_zero_def hcnj) + +lemma hcomplex_hcnj_zero_iff [iff]: "(hcnj z = 0) = (z = 0)" +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: hcomplex_zero_def hcnj) done -declare hcomplex_hcnj_zero [simp] - -lemma hcomplex_hcnj_zero_iff: "(hcnj z = 0) = (z = 0)" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hcomplex_zero_def hcnj) -done -declare hcomplex_hcnj_zero_iff [iff] lemma hcomplex_mult_hcnj: "z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hcnj hcomplex_mult hcomplex_of_hypreal hRe hIm hypreal_add hypreal_mult complex_mult_cnj numeral_2_eq_2) +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: hcnj hcomplex_mult hcomplex_of_hypreal hRe hIm hypreal_add + hypreal_mult complex_mult_cnj numeral_2_eq_2) done subsection{*More Theorems about the Function @{term hcmod}*} -lemma hcomplex_hcmod_eq_zero_cancel: "(hcmod x = 0) = (x = 0)" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (auto simp add: hcmod hcomplex_zero_def hypreal_zero_num) +lemma hcomplex_hcmod_eq_zero_cancel [simp]: "(hcmod x = 0) = (x = 0)" +apply (rule eq_Abs_hcomplex [of x]) +apply (simp add: hcmod hcomplex_zero_def hypreal_zero_num) done -declare hcomplex_hcmod_eq_zero_cancel [simp] -lemma hcmod_hcomplex_of_hypreal_of_nat: +lemma hcmod_hcomplex_of_hypreal_of_nat [simp]: "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n" -apply (simp add: abs_if linorder_not_less) +apply (simp add: abs_if linorder_not_less) done -declare hcmod_hcomplex_of_hypreal_of_nat [simp] -lemma hcmod_hcomplex_of_hypreal_of_hypnat: +lemma hcmod_hcomplex_of_hypreal_of_hypnat [simp]: "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n" -apply (simp add: abs_if linorder_not_less) +apply (simp add: abs_if linorder_not_less) done -declare hcmod_hcomplex_of_hypreal_of_hypnat [simp] -lemma hcmod_minus: "hcmod (-x) = hcmod(x)" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (auto simp add: hcmod hcomplex_minus) +lemma hcmod_minus [simp]: "hcmod (-x) = hcmod(x)" +apply (rule eq_Abs_hcomplex [of x]) +apply (simp add: hcmod hcomplex_minus) done -declare hcmod_minus [simp] lemma hcmod_mult_hcnj: "hcmod(z * hcnj(z)) = hcmod(z) ^ 2" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hcmod hcomplex_mult hcnj hypreal_mult complex_mod_mult_cnj numeral_2_eq_2) +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: hcmod hcomplex_mult hcnj hypreal_mult complex_mod_mult_cnj numeral_2_eq_2) done -lemma hcmod_ge_zero: "(0::hypreal) \ hcmod x" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (auto simp add: hcmod hypreal_zero_num hypreal_le) +lemma hcmod_ge_zero [simp]: "(0::hypreal) \ hcmod x" +apply (rule eq_Abs_hcomplex [of x]) +apply (simp add: hcmod hypreal_zero_num hypreal_le) done -declare hcmod_ge_zero [simp] -lemma hrabs_hcmod_cancel: "abs(hcmod x) = hcmod x" -apply (simp add: abs_if linorder_not_less) -done -declare hrabs_hcmod_cancel [simp] +lemma hrabs_hcmod_cancel [simp]: "abs(hcmod x) = hcmod x" +by (simp add: abs_if linorder_not_less) lemma hcmod_mult: "hcmod(x*y) = hcmod(x) * hcmod(y)" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (rule_tac z = "y" in eq_Abs_hcomplex) -apply (auto simp add: hcmod hcomplex_mult hypreal_mult complex_mod_mult) +apply (rule eq_Abs_hcomplex [of x]) +apply (rule eq_Abs_hcomplex [of y]) +apply (simp add: hcmod hcomplex_mult hypreal_mult complex_mod_mult) done lemma hcmod_add_squared_eq: "hcmod(x + y) ^ 2 = hcmod(x) ^ 2 + hcmod(y) ^ 2 + 2 * hRe(x * hcnj y)" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (rule_tac z = "y" in eq_Abs_hcomplex) -apply (auto simp add: hcmod hcomplex_add hypreal_mult hRe hcnj hcomplex_mult - numeral_2_eq_2 realpow_two [symmetric] - simp del: realpow_Suc) -apply (auto simp add: numeral_2_eq_2 [symmetric] complex_mod_add_squared_eq - hypreal_add [symmetric] hypreal_mult [symmetric] +apply (rule eq_Abs_hcomplex [of x]) +apply (rule eq_Abs_hcomplex [of y]) +apply (simp add: hcmod hcomplex_add hypreal_mult hRe hcnj hcomplex_mult + numeral_2_eq_2 realpow_two [symmetric] + del: realpow_Suc) +apply (simp add: numeral_2_eq_2 [symmetric] complex_mod_add_squared_eq + hypreal_add [symmetric] hypreal_mult [symmetric] hypreal_of_real_def [symmetric]) done -lemma hcomplex_hRe_mult_hcnj_le_hcmod: "hRe(x * hcnj y) \ hcmod(x * hcnj y)" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (rule_tac z = "y" in eq_Abs_hcomplex) -apply (auto simp add: hcmod hcnj hcomplex_mult hRe hypreal_le) +lemma hcomplex_hRe_mult_hcnj_le_hcmod [simp]: "hRe(x * hcnj y) \ hcmod(x * hcnj y)" +apply (rule eq_Abs_hcomplex [of x]) +apply (rule eq_Abs_hcomplex [of y]) +apply (simp add: hcmod hcnj hcomplex_mult hRe hypreal_le) done -declare hcomplex_hRe_mult_hcnj_le_hcmod [simp] -lemma hcomplex_hRe_mult_hcnj_le_hcmod2: "hRe(x * hcnj y) \ hcmod(x * y)" -apply (cut_tac x = "x" and y = "y" in hcomplex_hRe_mult_hcnj_le_hcmod) +lemma hcomplex_hRe_mult_hcnj_le_hcmod2 [simp]: "hRe(x * hcnj y) \ hcmod(x * y)" +apply (cut_tac x = x and y = y in hcomplex_hRe_mult_hcnj_le_hcmod) apply (simp add: hcmod_mult) done -declare hcomplex_hRe_mult_hcnj_le_hcmod2 [simp] -lemma hcmod_triangle_squared: "hcmod (x + y) ^ 2 \ (hcmod(x) + hcmod(y)) ^ 2" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (rule_tac z = "y" in eq_Abs_hcomplex) -apply (auto simp add: hcmod hcnj hcomplex_add hypreal_mult hypreal_add +lemma hcmod_triangle_squared [simp]: "hcmod (x + y) ^ 2 \ (hcmod(x) + hcmod(y)) ^ 2" +apply (rule eq_Abs_hcomplex [of x]) +apply (rule eq_Abs_hcomplex [of y]) +apply (simp add: hcmod hcnj hcomplex_add hypreal_mult hypreal_add hypreal_le realpow_two [symmetric] numeral_2_eq_2 - simp del: realpow_Suc) -apply (simp (no_asm) add: numeral_2_eq_2 [symmetric]) + del: realpow_Suc) +apply (simp add: numeral_2_eq_2 [symmetric]) done -declare hcmod_triangle_squared [simp] -lemma hcmod_triangle_ineq: "hcmod (x + y) \ hcmod(x) + hcmod(y)" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (rule_tac z = "y" in eq_Abs_hcomplex) -apply (auto simp add: hcmod hcomplex_add hypreal_add hypreal_le) +lemma hcmod_triangle_ineq [simp]: "hcmod (x + y) \ hcmod(x) + hcmod(y)" +apply (rule eq_Abs_hcomplex [of x]) +apply (rule eq_Abs_hcomplex [of y]) +apply (simp add: hcmod hcomplex_add hypreal_add hypreal_le) done -declare hcmod_triangle_ineq [simp] -lemma hcmod_triangle_ineq2: "hcmod(b + a) - hcmod b \ hcmod a" -apply (cut_tac x1 = "b" and y1 = "a" and c = "-hcmod b" in hcmod_triangle_ineq [THEN add_right_mono]) +lemma hcmod_triangle_ineq2 [simp]: "hcmod(b + a) - hcmod b \ hcmod a" +apply (cut_tac x1 = b and y1 = a and c = "-hcmod b" in hcmod_triangle_ineq [THEN add_right_mono]) apply (simp add: add_ac) done -declare hcmod_triangle_ineq2 [simp] lemma hcmod_diff_commute: "hcmod (x - y) = hcmod (y - x)" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (rule_tac z = "y" in eq_Abs_hcomplex) -apply (auto simp add: hcmod hcomplex_diff complex_mod_diff_commute) +apply (rule eq_Abs_hcomplex [of x]) +apply (rule eq_Abs_hcomplex [of y]) +apply (simp add: hcmod hcomplex_diff complex_mod_diff_commute) done lemma hcmod_add_less: "[| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (rule_tac z = "y" in eq_Abs_hcomplex) -apply (rule_tac z = "r" in eq_Abs_hypreal) -apply (rule_tac z = "s" in eq_Abs_hypreal) -apply (auto simp add: hcmod hcomplex_add hypreal_add hypreal_less) -apply ultra +apply (rule eq_Abs_hcomplex [of x]) +apply (rule eq_Abs_hcomplex [of y]) +apply (rule eq_Abs_hypreal [of r]) +apply (rule eq_Abs_hypreal [of s]) +apply (simp add: hcmod hcomplex_add hypreal_add hypreal_less, ultra) apply (auto intro: complex_mod_add_less) done lemma hcmod_mult_less: "[| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (rule_tac z = "y" in eq_Abs_hcomplex) -apply (rule_tac z = "r" in eq_Abs_hypreal) -apply (rule_tac z = "s" in eq_Abs_hypreal) -apply (auto simp add: hcmod hypreal_mult hypreal_less hcomplex_mult) -apply ultra +apply (rule eq_Abs_hcomplex [of x]) +apply (rule eq_Abs_hcomplex [of y]) +apply (rule eq_Abs_hypreal [of r]) +apply (rule eq_Abs_hypreal [of s]) +apply (simp add: hcmod hypreal_mult hypreal_less hcomplex_mult, ultra) apply (auto intro: complex_mod_mult_less) done -lemma hcmod_diff_ineq: "hcmod(a) - hcmod(b) \ hcmod(a + b)" -apply (rule_tac z = "a" in eq_Abs_hcomplex) -apply (rule_tac z = "b" in eq_Abs_hcomplex) -apply (auto simp add: hcmod hcomplex_add hypreal_diff hypreal_le) +lemma hcmod_diff_ineq [simp]: "hcmod(a) - hcmod(b) \ hcmod(a + b)" +apply (rule eq_Abs_hcomplex [of a]) +apply (rule eq_Abs_hcomplex [of b]) +apply (simp add: hcmod hcomplex_add hypreal_diff hypreal_le) done -declare hcmod_diff_ineq [simp] - subsection{*A Few Nonlinear Theorems*} @@ -903,42 +775,32 @@ "Abs_hcomplex(hcomplexrel``{%n. X n}) hcpow Abs_hypnat(hypnatrel``{%n. Y n}) = Abs_hcomplex(hcomplexrel``{%n. X n ^ Y n})" -apply (unfold hcpow_def) -apply (rule_tac f = "Abs_hcomplex" in arg_cong) +apply (simp add: hcpow_def) +apply (rule_tac f = Abs_hcomplex in arg_cong) apply (auto, ultra) done lemma hcomplex_of_hypreal_hyperpow: "hcomplex_of_hypreal (x pow n) = (hcomplex_of_hypreal x) hcpow n" -apply (rule_tac z = "x" in eq_Abs_hypreal) -apply (rule_tac z = "n" in eq_Abs_hypnat) -apply (auto simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow) +apply (rule eq_Abs_hypreal [of x]) +apply (rule eq_Abs_hypnat [of n]) +apply (simp add: hcomplex_of_hypreal hyperpow hcpow complex_of_real_pow) done lemma hcmod_hcpow: "hcmod(x hcpow n) = hcmod(x) pow n" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (rule_tac z = "n" in eq_Abs_hypnat) -apply (auto simp add: hcpow hyperpow hcmod complex_mod_complexpow) +apply (rule eq_Abs_hcomplex [of x]) +apply (rule eq_Abs_hypnat [of n]) +apply (simp add: hcpow hyperpow hcmod complex_mod_complexpow) done lemma hcmod_hcomplex_inverse: "hcmod(inverse x) = inverse(hcmod x)" -apply (case_tac "x = 0", simp add: HCOMPLEX_INVERSE_ZERO) +apply (case_tac "x = 0", simp) apply (rule_tac c1 = "hcmod x" in hypreal_mult_left_cancel [THEN iffD1]) apply (auto simp add: hcmod_mult [symmetric]) done -lemma hcmod_divide: - "hcmod(x/y) = hcmod(x)/(hcmod y)" -apply (unfold hcomplex_divide_def hypreal_divide_def) -apply (auto simp add: hcmod_mult hcmod_hcomplex_inverse) -done - -lemma hcomplex_inverse_divide: - "inverse(x/y) = y/(x::hcomplex)" -apply (unfold hcomplex_divide_def) -apply (auto simp add: inverse_mult_distrib hcomplex_mult_commute) -done -declare hcomplex_inverse_divide [simp] +lemma hcmod_divide: "hcmod(x/y) = hcmod(x)/(hcmod y)" +by (simp add: hcomplex_divide_def hypreal_divide_def hcmod_mult hcmod_hcomplex_inverse) subsection{*Exponentiation*} @@ -974,73 +836,56 @@ lemma hcomplexpow_minus: "(-x::hcomplex) ^ n = (if even n then (x ^ n) else -(x ^ n))" -apply (induct_tac "n") -apply auto -done +by (induct_tac "n", auto) lemma hcpow_minus: "(-x::hcomplex) hcpow n = (if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (rule_tac z = "n" in eq_Abs_hypnat) -apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus) -apply ultra -apply (auto simp add: complexpow_minus) -apply ultra +apply (rule eq_Abs_hcomplex [of x]) +apply (rule eq_Abs_hypnat [of n]) +apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus, ultra) +apply (auto simp add: complexpow_minus, ultra) done lemma hcpow_mult: "((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)" -apply (rule_tac z = "r" in eq_Abs_hcomplex) -apply (rule_tac z = "s" in eq_Abs_hcomplex) -apply (rule_tac z = "n" in eq_Abs_hypnat) -apply (auto simp add: hcpow hypreal_mult hcomplex_mult power_mult_distrib) +apply (rule eq_Abs_hcomplex [of r]) +apply (rule eq_Abs_hcomplex [of s]) +apply (rule eq_Abs_hypnat [of n]) +apply (simp add: hcpow hypreal_mult hcomplex_mult power_mult_distrib) done lemma hcpow_zero [simp]: "0 hcpow (n + 1) = 0" -apply (unfold hcomplex_zero_def hypnat_one_def) -apply (rule_tac z = "n" in eq_Abs_hypnat) -apply (auto simp add: hcpow hypnat_add) +apply (simp add: hcomplex_zero_def hypnat_one_def) +apply (rule eq_Abs_hypnat [of n]) +apply (simp add: hcpow hypnat_add) done lemma hcpow_zero2 [simp]: "0 hcpow (hSuc n) = 0" -apply (unfold hSuc_def) -apply (simp (no_asm)) -done +by (simp add: hSuc_def) lemma hcpow_not_zero [simp,intro]: "r \ 0 ==> r hcpow n \ (0::hcomplex)" -apply (rule_tac z = "r" in eq_Abs_hcomplex) -apply (rule_tac z = "n" in eq_Abs_hypnat) -apply (auto simp add: hcpow hcomplex_zero_def) -apply ultra +apply (rule eq_Abs_hcomplex [of r]) +apply (rule eq_Abs_hypnat [of n]) +apply (auto simp add: hcpow hcomplex_zero_def, ultra) done lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0" -apply (blast intro: ccontr dest: hcpow_not_zero) -done +by (blast intro: ccontr dest: hcpow_not_zero) -lemma hcomplex_i_mult_eq: "iii * iii = - 1" -apply (unfold iii_def) -apply (auto simp add: hcomplex_mult hcomplex_one_def hcomplex_minus) -done -declare hcomplex_i_mult_eq [simp] +lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1" +by (simp add: iii_def hcomplex_mult hcomplex_one_def hcomplex_minus) -lemma hcomplexpow_i_squared: "iii ^ 2 = - 1" -apply (simp (no_asm) add: numeral_2_eq_2) -done -declare hcomplexpow_i_squared [simp] +lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = - 1" +by (simp add: numeral_2_eq_2) -lemma hcomplex_i_not_zero: "iii \ 0" -apply (unfold iii_def hcomplex_zero_def) -apply auto -done -declare hcomplex_i_not_zero [simp] +lemma hcomplex_i_not_zero [simp]: "iii \ 0" +by (simp add: iii_def hcomplex_zero_def) lemma hcomplex_divide: "Abs_hcomplex(hcomplexrel``{%n. X n}) / Abs_hcomplex(hcomplexrel``{%n. Y n}) = Abs_hcomplex(hcomplexrel``{%n. X n / Y n})" -apply (unfold hcomplex_divide_def complex_divide_def) -apply (auto simp add: hcomplex_inverse hcomplex_mult) -done +by (simp add: hcomplex_divide_def complex_divide_def hcomplex_inverse hcomplex_mult) + subsection{*The Function @{term hsgn}*} @@ -1048,244 +893,210 @@ lemma hsgn: "hsgn (Abs_hcomplex(hcomplexrel `` {%n. X n})) = Abs_hcomplex(hcomplexrel `` {%n. sgn (X n)})" -apply (unfold hsgn_def) -apply (rule_tac f = "Abs_hcomplex" in arg_cong) +apply (simp add: hsgn_def) +apply (rule_tac f = Abs_hcomplex in arg_cong) apply (auto, ultra) done -lemma hsgn_zero: "hsgn 0 = 0" -apply (unfold hcomplex_zero_def) -apply (simp (no_asm) add: hsgn) -done -declare hsgn_zero [simp] +lemma hsgn_zero [simp]: "hsgn 0 = 0" +by (simp add: hcomplex_zero_def hsgn) - -lemma hsgn_one: "hsgn 1 = 1" -apply (unfold hcomplex_one_def) -apply (simp (no_asm) add: hsgn) -done -declare hsgn_one [simp] +lemma hsgn_one [simp]: "hsgn 1 = 1" +by (simp add: hcomplex_one_def hsgn) lemma hsgn_minus: "hsgn (-z) = - hsgn(z)" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hsgn hcomplex_minus sgn_minus) +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: hsgn hcomplex_minus sgn_minus) done lemma hsgn_eq: "hsgn z = z / hcomplex_of_hypreal (hcmod z)" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hsgn hcomplex_divide hcomplex_of_hypreal hcmod sgn_eq) +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: hsgn hcomplex_divide hcomplex_of_hypreal hcmod sgn_eq) done lemma lemma_hypreal_P_EX2: "(\(x::hypreal) y. P x y) = (\f g. P (Abs_hypreal(hyprel `` {f})) (Abs_hypreal(hyprel `` {g})))" apply auto -apply (rule_tac z = "x" in eq_Abs_hypreal) -apply (rule_tac z = "y" in eq_Abs_hypreal) -apply auto +apply (rule_tac z = x in eq_Abs_hypreal) +apply (rule_tac z = y in eq_Abs_hypreal, auto) done lemma complex_split2: "\(n::nat). \x y. (z n) = complex_of_real(x) + ii * complex_of_real(y)" -apply (blast intro: complex_split) -done +by (blast intro: complex_split) (* Interesting proof! *) lemma hcomplex_split: "\x y. z = hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)" -apply (rule_tac z = "z" in eq_Abs_hcomplex) +apply (rule eq_Abs_hcomplex [of z]) apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult) -apply (cut_tac z = "x" in complex_split2) +apply (cut_tac z = x in complex_split2) apply (drule choice, safe)+ -apply (rule_tac x = "f" in exI) -apply (rule_tac x = "fa" in exI) -apply auto +apply (rule_tac x = f in exI) +apply (rule_tac x = fa in exI, auto) done -lemma hRe_hcomplex_i: +lemma hRe_hcomplex_i [simp]: "hRe(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = x" -apply (rule_tac z = "x" in eq_Abs_hypreal) -apply (rule_tac z = "y" in eq_Abs_hypreal) +apply (rule eq_Abs_hypreal [of x]) +apply (rule eq_Abs_hypreal [of y]) apply (auto simp add: hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal) done -declare hRe_hcomplex_i [simp] -lemma hIm_hcomplex_i: +lemma hIm_hcomplex_i [simp]: "hIm(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = y" -apply (rule_tac z = "x" in eq_Abs_hypreal) -apply (rule_tac z = "y" in eq_Abs_hypreal) -apply (auto simp add: hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal) +apply (rule eq_Abs_hypreal [of x]) +apply (rule eq_Abs_hypreal [of y]) +apply (simp add: hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal) done -declare hIm_hcomplex_i [simp] lemma hcmod_i: "hcmod (hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = ( *f* sqrt) (x ^ 2 + y ^ 2)" -apply (rule_tac z = "x" in eq_Abs_hypreal) -apply (rule_tac z = "y" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult starfun hypreal_mult hypreal_add hcmod cmod_i numeral_2_eq_2) +apply (rule eq_Abs_hypreal [of x]) +apply (rule eq_Abs_hypreal [of y]) +apply (simp add: hcomplex_of_hypreal iii_def hcomplex_add hcomplex_mult starfun hypreal_mult hypreal_add hcmod cmod_i numeral_2_eq_2) done lemma hcomplex_eq_hRe_eq: "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya = hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb ==> xa = xb" -apply (unfold iii_def) -apply (rule_tac z = "xa" in eq_Abs_hypreal) -apply (rule_tac z = "ya" in eq_Abs_hypreal) -apply (rule_tac z = "xb" in eq_Abs_hypreal) -apply (rule_tac z = "yb" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal) -apply (ultra) +apply (simp add: iii_def) +apply (rule eq_Abs_hypreal [of xa]) +apply (rule eq_Abs_hypreal [of ya]) +apply (rule eq_Abs_hypreal [of xb]) +apply (rule eq_Abs_hypreal [of yb]) +apply (simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal, ultra) done lemma hcomplex_eq_hIm_eq: "hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya = hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb ==> ya = yb" -apply (unfold iii_def) -apply (rule_tac z = "xa" in eq_Abs_hypreal) -apply (rule_tac z = "ya" in eq_Abs_hypreal) -apply (rule_tac z = "xb" in eq_Abs_hypreal) -apply (rule_tac z = "yb" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal) -apply (ultra) +apply (simp add: iii_def) +apply (rule eq_Abs_hypreal [of xa]) +apply (rule eq_Abs_hypreal [of ya]) +apply (rule eq_Abs_hypreal [of xb]) +apply (rule eq_Abs_hypreal [of yb]) +apply (simp add: hcomplex_mult hcomplex_add hcomplex_of_hypreal, ultra) done -lemma hcomplex_eq_cancel_iff: +lemma hcomplex_eq_cancel_iff [simp]: "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya = hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) = ((xa = xb) & (ya = yb))" -apply (auto intro: hcomplex_eq_hIm_eq hcomplex_eq_hRe_eq) -done -declare hcomplex_eq_cancel_iff [simp] +by (auto intro: hcomplex_eq_hIm_eq hcomplex_eq_hRe_eq) -lemma hcomplex_eq_cancel_iffA: +lemma hcomplex_eq_cancel_iffA [iff]: "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii = - hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii ) = ((xa = xb) & (ya = yb))" -apply (auto simp add: hcomplex_mult_commute) + hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii) = ((xa = xb) & (ya = yb))" +apply (simp add: hcomplex_mult_commute) done -declare hcomplex_eq_cancel_iffA [iff] -lemma hcomplex_eq_cancel_iffB: +lemma hcomplex_eq_cancel_iffB [iff]: "(hcomplex_of_hypreal xa + hcomplex_of_hypreal ya * iii = hcomplex_of_hypreal xb + iii * hcomplex_of_hypreal yb) = ((xa = xb) & (ya = yb))" -apply (auto simp add: hcomplex_mult_commute) +apply (simp add: hcomplex_mult_commute) done -declare hcomplex_eq_cancel_iffB [iff] -lemma hcomplex_eq_cancel_iffC: +lemma hcomplex_eq_cancel_iffC [iff]: "(hcomplex_of_hypreal xa + iii * hcomplex_of_hypreal ya = hcomplex_of_hypreal xb + hcomplex_of_hypreal yb * iii) = ((xa = xb) & (ya = yb))" -apply (auto simp add: hcomplex_mult_commute) +apply (simp add: hcomplex_mult_commute) done -declare hcomplex_eq_cancel_iffC [iff] -lemma hcomplex_eq_cancel_iff2: +lemma hcomplex_eq_cancel_iff2 [simp]: "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = hcomplex_of_hypreal xa) = (x = xa & y = 0)" -apply (cut_tac xa = "x" and ya = "y" and xb = "xa" and yb = "0" in hcomplex_eq_cancel_iff) +apply (cut_tac xa = x and ya = y and xb = xa and yb = 0 in hcomplex_eq_cancel_iff) apply (simp del: hcomplex_eq_cancel_iff) done -declare hcomplex_eq_cancel_iff2 [simp] -lemma hcomplex_eq_cancel_iff2a: +lemma hcomplex_eq_cancel_iff2a [simp]: "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii = hcomplex_of_hypreal xa) = (x = xa & y = 0)" -apply (auto simp add: hcomplex_mult_commute) +apply (simp add: hcomplex_mult_commute) done -declare hcomplex_eq_cancel_iff2a [simp] -lemma hcomplex_eq_cancel_iff3: +lemma hcomplex_eq_cancel_iff3 [simp]: "(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)" -apply (cut_tac xa = "x" and ya = "y" and xb = "0" and yb = "ya" in hcomplex_eq_cancel_iff) +apply (cut_tac xa = x and ya = y and xb = 0 and yb = ya in hcomplex_eq_cancel_iff) apply (simp del: hcomplex_eq_cancel_iff) done -declare hcomplex_eq_cancel_iff3 [simp] -lemma hcomplex_eq_cancel_iff3a: +lemma hcomplex_eq_cancel_iff3a [simp]: "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii = iii * hcomplex_of_hypreal ya) = (x = 0 & y = ya)" -apply (auto simp add: hcomplex_mult_commute) +apply (simp add: hcomplex_mult_commute) done -declare hcomplex_eq_cancel_iff3a [simp] lemma hcomplex_split_hRe_zero: "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0 ==> x = 0" -apply (unfold iii_def) -apply (rule_tac z = "x" in eq_Abs_hypreal) -apply (rule_tac z = "y" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num) -apply ultra -apply (auto simp add: complex_split_Re_zero) +apply (simp add: iii_def) +apply (rule eq_Abs_hypreal [of x]) +apply (rule eq_Abs_hypreal [of y]) +apply (simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num, ultra) +apply (simp add: complex_split_Re_zero) done lemma hcomplex_split_hIm_zero: "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0 ==> y = 0" -apply (unfold iii_def) -apply (rule_tac z = "x" in eq_Abs_hypreal) -apply (rule_tac z = "y" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num) -apply ultra -apply (auto simp add: complex_split_Im_zero) +apply (simp add: iii_def) +apply (rule eq_Abs_hypreal [of x]) +apply (rule eq_Abs_hypreal [of y]) +apply (simp add: hcomplex_of_hypreal hcomplex_add hcomplex_mult hcomplex_zero_def hypreal_zero_num, ultra) +apply (simp add: complex_split_Im_zero) done -lemma hRe_hsgn: "hRe(hsgn z) = hRe(z)/hcmod z" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hsgn hcmod hRe hypreal_divide) +lemma hRe_hsgn [simp]: "hRe(hsgn z) = hRe(z)/hcmod z" +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: hsgn hcmod hRe hypreal_divide) done -declare hRe_hsgn [simp] -lemma hIm_hsgn: "hIm(hsgn z) = hIm(z)/hcmod z" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hsgn hcmod hIm hypreal_divide) +lemma hIm_hsgn [simp]: "hIm(hsgn z) = hIm(z)/hcmod z" +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: hsgn hcmod hIm hypreal_divide) done -declare hIm_hsgn [simp] -lemma real_two_squares_add_zero_iff: - "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)" +lemma real_two_squares_add_zero_iff [simp]: "(x*x + y*y = 0) = ((x::real) = 0 & y = 0)" apply (auto intro: real_sum_squares_cancel) done -declare real_two_squares_add_zero_iff [simp] lemma hcomplex_inverse_complex_split: "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) = hcomplex_of_hypreal(x/(x ^ 2 + y ^ 2)) - iii * hcomplex_of_hypreal(y/(x ^ 2 + y ^ 2))" -apply (rule_tac z = "x" in eq_Abs_hypreal) -apply (rule_tac z = "y" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide hcomplex_diff complex_inverse_complex_split numeral_2_eq_2) +apply (rule eq_Abs_hypreal [of x]) +apply (rule eq_Abs_hypreal [of y]) +apply (simp add: hcomplex_of_hypreal hcomplex_mult hcomplex_add iii_def starfun hypreal_mult hypreal_add hcomplex_inverse hypreal_divide hcomplex_diff complex_inverse_complex_split numeral_2_eq_2) +done + +lemma hRe_mult_i_eq[simp]: + "hRe (iii * hcomplex_of_hypreal y) = 0" +apply (simp add: iii_def) +apply (rule eq_Abs_hypreal [of y]) +apply (simp add: hcomplex_of_hypreal hcomplex_mult hRe hypreal_zero_num) done -lemma hRe_mult_i_eq: - "hRe (iii * hcomplex_of_hypreal y) = 0" -apply (unfold iii_def) -apply (rule_tac z = "y" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hRe hypreal_zero_num) -done -declare hRe_mult_i_eq [simp] - -lemma hIm_mult_i_eq: +lemma hIm_mult_i_eq [simp]: "hIm (iii * hcomplex_of_hypreal y) = y" -apply (unfold iii_def) -apply (rule_tac z = "y" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hIm hypreal_zero_num) +apply (simp add: iii_def) +apply (rule eq_Abs_hypreal [of y]) +apply (simp add: hcomplex_of_hypreal hcomplex_mult hIm hypreal_zero_num) done -declare hIm_mult_i_eq [simp] -lemma hcmod_mult_i: "hcmod (iii * hcomplex_of_hypreal y) = abs y" -apply (rule_tac z = "y" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_of_hypreal hcmod hypreal_hrabs iii_def hcomplex_mult) +lemma hcmod_mult_i [simp]: "hcmod (iii * hcomplex_of_hypreal y) = abs y" +apply (rule eq_Abs_hypreal [of y]) +apply (simp add: hcomplex_of_hypreal hcmod hypreal_hrabs iii_def hcomplex_mult) done -declare hcmod_mult_i [simp] -lemma hcmod_mult_i2: "hcmod (hcomplex_of_hypreal y * iii) = abs y" -apply (auto simp add: hcomplex_mult_commute) -done -declare hcmod_mult_i2 [simp] +lemma hcmod_mult_i2 [simp]: "hcmod (hcomplex_of_hypreal y * iii) = abs y" +by (simp add: hcomplex_mult_commute) (*---------------------------------------------------------------------------*) (* harg *) @@ -1295,37 +1106,35 @@ "harg (Abs_hcomplex(hcomplexrel `` {%n. X n})) = Abs_hypreal(hyprel `` {%n. arg (X n)})" -apply (unfold harg_def) -apply (rule_tac f = "Abs_hypreal" in arg_cong) +apply (simp add: harg_def) +apply (rule_tac f = Abs_hypreal in arg_cong) apply (auto, ultra) done lemma cos_harg_i_mult_zero_pos: "0 < y ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0" -apply (rule_tac z = "y" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult - hypreal_zero_num hypreal_less starfun harg) -apply (ultra) +apply (rule eq_Abs_hypreal [of y]) +apply (simp add: hcomplex_of_hypreal iii_def hcomplex_mult + hypreal_zero_num hypreal_less starfun harg, ultra) done lemma cos_harg_i_mult_zero_neg: "y < 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0" -apply (rule_tac z = "y" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_of_hypreal iii_def hcomplex_mult - hypreal_zero_num hypreal_less starfun harg) -apply (ultra) +apply (rule eq_Abs_hypreal [of y]) +apply (simp add: hcomplex_of_hypreal iii_def hcomplex_mult + hypreal_zero_num hypreal_less starfun harg, ultra) done lemma cos_harg_i_mult_zero [simp]: "y \ 0 ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0" -apply (cut_tac x = "y" and y = "0" in linorder_less_linear) +apply (cut_tac x = y and y = 0 in linorder_less_linear) apply (auto simp add: cos_harg_i_mult_zero_pos cos_harg_i_mult_zero_neg) done lemma hcomplex_of_hypreal_zero_iff [simp]: "(hcomplex_of_hypreal y = 0) = (y = 0)" -apply (rule_tac z = "y" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def) +apply (rule eq_Abs_hypreal [of y]) +apply (simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def) done @@ -1340,331 +1149,259 @@ lemma hcomplex_split_polar: "\r a. z = hcomplex_of_hypreal r * (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult) -apply (cut_tac z = "x" in complex_split_polar2) +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult) +apply (cut_tac z = x in complex_split_polar2) apply (drule choice, safe)+ -apply (rule_tac x = "f" in exI) -apply (rule_tac x = "fa" in exI) -apply auto +apply (rule_tac x = f in exI) +apply (rule_tac x = fa in exI, auto) done lemma hcis: "hcis (Abs_hypreal(hyprel `` {%n. X n})) = Abs_hcomplex(hcomplexrel `` {%n. cis (X n)})" -apply (unfold hcis_def) -apply (rule_tac f = "Abs_hcomplex" in arg_cong) -apply auto -apply (ultra) +apply (simp add: hcis_def) +apply (rule_tac f = Abs_hcomplex in arg_cong, auto, ultra) done lemma hcis_eq: "hcis a = (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))" -apply (rule_tac z = "a" in eq_Abs_hypreal) -apply (auto simp add: starfun hcis hcomplex_of_hypreal iii_def hcomplex_mult hcomplex_add cis_def) +apply (rule eq_Abs_hypreal [of a]) +apply (simp add: starfun hcis hcomplex_of_hypreal iii_def hcomplex_mult hcomplex_add cis_def) done lemma hrcis: "hrcis (Abs_hypreal(hyprel `` {%n. X n})) (Abs_hypreal(hyprel `` {%n. Y n})) = Abs_hcomplex(hcomplexrel `` {%n. rcis (X n) (Y n)})" -apply (unfold hrcis_def) -apply (auto simp add: hcomplex_of_hypreal hcomplex_mult hcis rcis_def) -done +by (simp add: hrcis_def hcomplex_of_hypreal hcomplex_mult hcis rcis_def) lemma hrcis_Ex: "\r a. z = hrcis r a" -apply (simp (no_asm) add: hrcis_def hcis_eq) +apply (simp add: hrcis_def hcis_eq) apply (rule hcomplex_split_polar) done -lemma hRe_hcomplex_polar: +lemma hRe_hcomplex_polar [simp]: "hRe(hcomplex_of_hypreal r * (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* cos) a" -apply (auto simp add: right_distrib hcomplex_of_hypreal_mult mult_ac) -done -declare hRe_hcomplex_polar [simp] +by (simp add: right_distrib hcomplex_of_hypreal_mult mult_ac) -lemma hRe_hrcis: "hRe(hrcis r a) = r * ( *f* cos) a" -apply (unfold hrcis_def) -apply (auto simp add: hcis_eq) -done -declare hRe_hrcis [simp] +lemma hRe_hrcis [simp]: "hRe(hrcis r a) = r * ( *f* cos) a" +by (simp add: hrcis_def hcis_eq) -lemma hIm_hcomplex_polar: +lemma hIm_hcomplex_polar [simp]: "hIm(hcomplex_of_hypreal r * (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))) = r * ( *f* sin) a" -apply (auto simp add: right_distrib hcomplex_of_hypreal_mult mult_ac) -done -declare hIm_hcomplex_polar [simp] +by (simp add: right_distrib hcomplex_of_hypreal_mult mult_ac) -lemma hIm_hrcis: "hIm(hrcis r a) = r * ( *f* sin) a" -apply (unfold hrcis_def) -apply (auto simp add: hcis_eq) -done -declare hIm_hrcis [simp] +lemma hIm_hrcis [simp]: "hIm(hrcis r a) = r * ( *f* sin) a" +by (simp add: hrcis_def hcis_eq) -lemma hcmod_complex_polar: +lemma hcmod_complex_polar [simp]: "hcmod (hcomplex_of_hypreal r * (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))) = abs r" -apply (rule_tac z = "r" in eq_Abs_hypreal) -apply (rule_tac z = "a" in eq_Abs_hypreal) -apply (auto simp add: iii_def starfun hcomplex_of_hypreal hcomplex_mult hcmod hcomplex_add hypreal_hrabs) +apply (rule eq_Abs_hypreal [of r]) +apply (rule eq_Abs_hypreal [of a]) +apply (simp add: iii_def starfun hcomplex_of_hypreal hcomplex_mult hcmod hcomplex_add hypreal_hrabs) done -declare hcmod_complex_polar [simp] -lemma hcmod_hrcis: "hcmod(hrcis r a) = abs r" -apply (unfold hrcis_def) -apply (auto simp add: hcis_eq) -done -declare hcmod_hrcis [simp] +lemma hcmod_hrcis [simp]: "hcmod(hrcis r a) = abs r" +by (simp add: hrcis_def hcis_eq) (*---------------------------------------------------------------------------*) (* (r1 * hrcis a) * (r2 * hrcis b) = r1 * r2 * hrcis (a + b) *) (*---------------------------------------------------------------------------*) lemma hcis_hrcis_eq: "hcis a = hrcis 1 a" -apply (unfold hrcis_def) -apply (simp (no_asm)) -done +by (simp add: hrcis_def) declare hcis_hrcis_eq [symmetric, simp] lemma hrcis_mult: "hrcis r1 a * hrcis r2 b = hrcis (r1*r2) (a + b)" -apply (unfold hrcis_def) -apply (rule_tac z = "r1" in eq_Abs_hypreal) -apply (rule_tac z = "r2" in eq_Abs_hypreal) -apply (rule_tac z = "a" in eq_Abs_hypreal) -apply (rule_tac z = "b" in eq_Abs_hypreal) -apply (auto simp add: hrcis hcis hypreal_add hypreal_mult hcomplex_of_hypreal - hcomplex_mult cis_mult [symmetric] +apply (simp add: hrcis_def) +apply (rule eq_Abs_hypreal [of r1]) +apply (rule eq_Abs_hypreal [of r2]) +apply (rule eq_Abs_hypreal [of a]) +apply (rule eq_Abs_hypreal [of b]) +apply (simp add: hrcis hcis hypreal_add hypreal_mult hcomplex_of_hypreal + hcomplex_mult cis_mult [symmetric] complex_of_real_mult [symmetric]) done lemma hcis_mult: "hcis a * hcis b = hcis (a + b)" -apply (rule_tac z = "a" in eq_Abs_hypreal) -apply (rule_tac z = "b" in eq_Abs_hypreal) -apply (auto simp add: hcis hcomplex_mult hypreal_add cis_mult) +apply (rule eq_Abs_hypreal [of a]) +apply (rule eq_Abs_hypreal [of b]) +apply (simp add: hcis hcomplex_mult hypreal_add cis_mult) done -lemma hcis_zero: - "hcis 0 = 1" -apply (unfold hcomplex_one_def) -apply (auto simp add: hcis hypreal_zero_num) -done -declare hcis_zero [simp] +lemma hcis_zero [simp]: "hcis 0 = 1" +by (simp add: hcomplex_one_def hcis hypreal_zero_num) -lemma hrcis_zero_mod: - "hrcis 0 a = 0" -apply (unfold hcomplex_zero_def) -apply (rule_tac z = "a" in eq_Abs_hypreal) -apply (auto simp add: hrcis hypreal_zero_num) +lemma hrcis_zero_mod [simp]: "hrcis 0 a = 0" +apply (simp add: hcomplex_zero_def) +apply (rule eq_Abs_hypreal [of a]) +apply (simp add: hrcis hypreal_zero_num) done -declare hrcis_zero_mod [simp] -lemma hrcis_zero_arg: "hrcis r 0 = hcomplex_of_hypreal r" -apply (rule_tac z = "r" in eq_Abs_hypreal) -apply (auto simp add: hrcis hypreal_zero_num hcomplex_of_hypreal) +lemma hrcis_zero_arg [simp]: "hrcis r 0 = hcomplex_of_hypreal r" +apply (rule eq_Abs_hypreal [of r]) +apply (simp add: hrcis hypreal_zero_num hcomplex_of_hypreal) done -declare hrcis_zero_arg [simp] -lemma hcomplex_i_mult_minus: "iii * (iii * x) = - x" -apply (simp (no_asm) add: hcomplex_mult_assoc [symmetric]) -done -declare hcomplex_i_mult_minus [simp] +lemma hcomplex_i_mult_minus [simp]: "iii * (iii * x) = - x" +by (simp add: hcomplex_mult_assoc [symmetric]) -lemma hcomplex_i_mult_minus2: "iii * iii * x = - x" -apply (simp (no_asm)) -done -declare hcomplex_i_mult_minus2 [simp] +lemma hcomplex_i_mult_minus2 [simp]: "iii * iii * x = - x" +by simp lemma hcis_hypreal_of_nat_Suc_mult: "hcis (hypreal_of_nat (Suc n) * a) = hcis a * hcis (hypreal_of_nat n * a)" -apply (rule_tac z = "a" in eq_Abs_hypreal) -apply (auto simp add: hypreal_of_nat hcis hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult) +apply (rule eq_Abs_hypreal [of a]) +apply (simp add: hypreal_of_nat hcis hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult) done lemma NSDeMoivre: "(hcis a) ^ n = hcis (hypreal_of_nat n * a)" apply (induct_tac "n") -apply (auto simp add: hcis_hypreal_of_nat_Suc_mult) +apply (simp_all add: hcis_hypreal_of_nat_Suc_mult) done lemma hcis_hypreal_of_hypnat_Suc_mult: "hcis (hypreal_of_hypnat (n + 1) * a) = hcis a * hcis (hypreal_of_hypnat n * a)" -apply (rule_tac z = "a" in eq_Abs_hypreal) -apply (rule_tac z = "n" in eq_Abs_hypnat) -apply (auto simp add: hcis hypreal_of_hypnat hypnat_add hypnat_one_def hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult) +apply (rule eq_Abs_hypreal [of a]) +apply (rule eq_Abs_hypnat [of n]) +apply (simp add: hcis hypreal_of_hypnat hypnat_add hypnat_one_def hypreal_mult hcomplex_mult cis_real_of_nat_Suc_mult) done lemma NSDeMoivre_ext: "(hcis a) hcpow n = hcis (hypreal_of_hypnat n * a)" -apply (rule_tac z = "a" in eq_Abs_hypreal) -apply (rule_tac z = "n" in eq_Abs_hypnat) -apply (auto simp add: hcis hypreal_of_hypnat hypreal_mult hcpow DeMoivre) +apply (rule eq_Abs_hypreal [of a]) +apply (rule eq_Abs_hypnat [of n]) +apply (simp add: hcis hypreal_of_hypnat hypreal_mult hcpow DeMoivre) done lemma DeMoivre2: "(hrcis r a) ^ n = hrcis (r ^ n) (hypreal_of_nat n * a)" -apply (unfold hrcis_def) -apply (auto simp add: power_mult_distrib NSDeMoivre hcomplex_of_hypreal_pow) +apply (simp add: hrcis_def power_mult_distrib NSDeMoivre hcomplex_of_hypreal_pow) done lemma DeMoivre2_ext: "(hrcis r a) hcpow n = hrcis (r pow n) (hypreal_of_hypnat n * a)" -apply (unfold hrcis_def) -apply (auto simp add: hcpow_mult NSDeMoivre_ext hcomplex_of_hypreal_hyperpow) +apply (simp add: hrcis_def hcpow_mult NSDeMoivre_ext hcomplex_of_hypreal_hyperpow) +done + +lemma hcis_inverse [simp]: "inverse(hcis a) = hcis (-a)" +apply (rule eq_Abs_hypreal [of a]) +apply (simp add: hcomplex_inverse hcis hypreal_minus) done -lemma hcis_inverse: "inverse(hcis a) = hcis (-a)" -apply (rule_tac z = "a" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_inverse hcis hypreal_minus) +lemma hrcis_inverse: "inverse(hrcis r a) = hrcis (inverse r) (-a)" +apply (rule eq_Abs_hypreal [of a]) +apply (rule eq_Abs_hypreal [of r]) +apply (simp add: hcomplex_inverse hrcis hypreal_minus hypreal_inverse rcis_inverse, ultra) +apply (simp add: real_divide_def) done -declare hcis_inverse [simp] -lemma hrcis_inverse: "inverse(hrcis r a) = hrcis (inverse r) (-a)" -apply (rule_tac z = "a" in eq_Abs_hypreal) -apply (rule_tac z = "r" in eq_Abs_hypreal) -apply (auto simp add: hcomplex_inverse hrcis hypreal_minus hypreal_inverse rcis_inverse) -apply (ultra) -apply (unfold real_divide_def) -apply (auto simp add: INVERSE_ZERO) +lemma hRe_hcis [simp]: "hRe(hcis a) = ( *f* cos) a" +apply (rule eq_Abs_hypreal [of a]) +apply (simp add: hcis starfun hRe) done -lemma hRe_hcis: "hRe(hcis a) = ( *f* cos) a" -apply (rule_tac z = "a" in eq_Abs_hypreal) -apply (auto simp add: hcis starfun hRe) +lemma hIm_hcis [simp]: "hIm(hcis a) = ( *f* sin) a" +apply (rule eq_Abs_hypreal [of a]) +apply (simp add: hcis starfun hIm) done -declare hRe_hcis [simp] -lemma hIm_hcis: "hIm(hcis a) = ( *f* sin) a" -apply (rule_tac z = "a" in eq_Abs_hypreal) -apply (auto simp add: hcis starfun hIm) -done -declare hIm_hcis [simp] - -lemma cos_n_hRe_hcis_pow_n: - "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)" -apply (auto simp add: NSDeMoivre) +lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)" +apply (simp add: NSDeMoivre) done -lemma sin_n_hIm_hcis_pow_n: - "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)" -apply (auto simp add: NSDeMoivre) +lemma sin_n_hIm_hcis_pow_n: "( *f* sin) (hypreal_of_nat n * a) = hIm(hcis a ^ n)" +apply (simp add: NSDeMoivre) done -lemma cos_n_hRe_hcis_hcpow_n: - "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)" -apply (auto simp add: NSDeMoivre_ext) +lemma cos_n_hRe_hcis_hcpow_n: "( *f* cos) (hypreal_of_hypnat n * a) = hRe(hcis a hcpow n)" +apply (simp add: NSDeMoivre_ext) done -lemma sin_n_hIm_hcis_hcpow_n: - "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)" -apply (auto simp add: NSDeMoivre_ext) +lemma sin_n_hIm_hcis_hcpow_n: "( *f* sin) (hypreal_of_hypnat n * a) = hIm(hcis a hcpow n)" +apply (simp add: NSDeMoivre_ext) done lemma hexpi_add: "hexpi(a + b) = hexpi(a) * hexpi(b)" -apply (unfold hexpi_def) -apply (rule_tac z = "a" in eq_Abs_hcomplex) -apply (rule_tac z = "b" in eq_Abs_hcomplex) -apply (auto simp add: hcis hRe hIm hcomplex_add hcomplex_mult hypreal_mult starfun hcomplex_of_hypreal cis_mult [symmetric] complex_Im_add complex_Re_add exp_add complex_of_real_mult) +apply (simp add: hexpi_def) +apply (rule eq_Abs_hcomplex [of a]) +apply (rule eq_Abs_hcomplex [of b]) +apply (simp add: hcis hRe hIm hcomplex_add hcomplex_mult hypreal_mult starfun hcomplex_of_hypreal cis_mult [symmetric] complex_Im_add complex_Re_add exp_add complex_of_real_mult) done -subsection{*@{term hcomplex_of_complex}: the Injection from +subsection{*@{term hcomplex_of_complex}: the Injection from type @{typ complex} to to @{typ hcomplex}*} lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)" -apply (rule inj_onI , rule ccontr) -apply (auto simp add: hcomplex_of_complex_def) +apply (rule inj_onI, rule ccontr) +apply (simp add: hcomplex_of_complex_def) done lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii" -apply (unfold iii_def hcomplex_of_complex_def) -apply (simp (no_asm)) -done +by (simp add: iii_def hcomplex_of_complex_def) -lemma hcomplex_of_complex_add: +lemma hcomplex_of_complex_add [simp]: "hcomplex_of_complex (z1 + z2) = hcomplex_of_complex z1 + hcomplex_of_complex z2" -apply (unfold hcomplex_of_complex_def) -apply (simp (no_asm) add: hcomplex_add) -done -declare hcomplex_of_complex_add [simp] +by (simp add: hcomplex_of_complex_def hcomplex_add) -lemma hcomplex_of_complex_mult: +lemma hcomplex_of_complex_mult [simp]: "hcomplex_of_complex (z1 * z2) = hcomplex_of_complex z1 * hcomplex_of_complex z2" -apply (unfold hcomplex_of_complex_def) -apply (simp (no_asm) add: hcomplex_mult) -done -declare hcomplex_of_complex_mult [simp] +by (simp add: hcomplex_of_complex_def hcomplex_mult) -lemma hcomplex_of_complex_eq_iff: - "(hcomplex_of_complex z1 = hcomplex_of_complex z2) = (z1 = z2)" -apply (unfold hcomplex_of_complex_def) -apply auto -done -declare hcomplex_of_complex_eq_iff [simp] +lemma hcomplex_of_complex_eq_iff [simp]: + "(hcomplex_of_complex z1 = hcomplex_of_complex z2) = (z1 = z2)" +by (simp add: hcomplex_of_complex_def) -lemma hcomplex_of_complex_minus: + +lemma hcomplex_of_complex_minus [simp]: "hcomplex_of_complex (-r) = - hcomplex_of_complex r" -apply (unfold hcomplex_of_complex_def) -apply (auto simp add: hcomplex_minus) -done -declare hcomplex_of_complex_minus [simp] +by (simp add: hcomplex_of_complex_def hcomplex_minus) -lemma hcomplex_of_complex_one [simp]: - "hcomplex_of_complex 1 = 1" -apply (unfold hcomplex_of_complex_def hcomplex_one_def) -apply auto -done +lemma hcomplex_of_complex_one [simp]: "hcomplex_of_complex 1 = 1" +by (simp add: hcomplex_of_complex_def hcomplex_one_def) -lemma hcomplex_of_complex_zero [simp]: - "hcomplex_of_complex 0 = 0" -apply (unfold hcomplex_of_complex_def hcomplex_zero_def) -apply (simp (no_asm)) -done +lemma hcomplex_of_complex_zero [simp]: "hcomplex_of_complex 0 = 0" +by (simp add: hcomplex_of_complex_def hcomplex_zero_def) lemma hcomplex_of_complex_zero_iff: "(hcomplex_of_complex r = 0) = (r = 0)" -apply (auto intro: FreeUltrafilterNat_P simp add: hcomplex_of_complex_def hcomplex_zero_def) -done +by (auto intro: FreeUltrafilterNat_P simp add: hcomplex_of_complex_def hcomplex_zero_def) -lemma hcomplex_of_complex_inverse: +lemma hcomplex_of_complex_inverse [simp]: "hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)" apply (case_tac "r=0") apply (simp add: hcomplex_of_complex_zero) -apply (rule_tac c1 = "hcomplex_of_complex r" +apply (rule_tac c1 = "hcomplex_of_complex r" in hcomplex_mult_left_cancel [THEN iffD1]) apply (force simp add: hcomplex_of_complex_zero_iff) apply (subst hcomplex_of_complex_mult [symmetric]) -apply (auto simp add: hcomplex_of_complex_one hcomplex_of_complex_zero_iff) +apply (simp add: hcomplex_of_complex_one hcomplex_of_complex_zero_iff) done -declare hcomplex_of_complex_inverse [simp] -lemma hcomplex_of_complex_divide: +lemma hcomplex_of_complex_divide [simp]: "hcomplex_of_complex (z1 / z2) = hcomplex_of_complex z1 / hcomplex_of_complex z2" -apply (simp (no_asm) add: hcomplex_divide_def complex_divide_def) -done -declare hcomplex_of_complex_divide [simp] +by (simp add: hcomplex_divide_def complex_divide_def) lemma hRe_hcomplex_of_complex: "hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)" -apply (unfold hcomplex_of_complex_def hypreal_of_real_def) -apply (auto simp add: hRe) -done +by (simp add: hcomplex_of_complex_def hypreal_of_real_def hRe) lemma hIm_hcomplex_of_complex: "hIm (hcomplex_of_complex z) = hypreal_of_real (Im z)" -apply (unfold hcomplex_of_complex_def hypreal_of_real_def) -apply (auto simp add: hIm) -done +by (simp add: hcomplex_of_complex_def hypreal_of_real_def hIm) lemma hcmod_hcomplex_of_complex: "hcmod (hcomplex_of_complex x) = hypreal_of_real (cmod x)" -apply (unfold hypreal_of_real_def hcomplex_of_complex_def) -apply (auto simp add: hcmod) -done +by (simp add: hypreal_of_real_def hcomplex_of_complex_def hcmod) ML {* @@ -1710,7 +1447,6 @@ val hIm_add = thm"hIm_add"; val hcomplex_minus_congruent = thm"hcomplex_minus_congruent"; val hcomplex_minus = thm"hcomplex_minus"; -val inj_hcomplex_minus = thm"inj_hcomplex_minus"; val hcomplex_add_minus_left = thm"hcomplex_add_minus_left"; val hRe_minus = thm"hRe_minus"; val hIm_minus = thm"hIm_minus"; @@ -1728,14 +1464,11 @@ val hcomplex_add_mult_distrib = thm"hcomplex_add_mult_distrib"; val hcomplex_zero_not_eq_one = thm"hcomplex_zero_not_eq_one"; val hcomplex_inverse = thm"hcomplex_inverse"; -val HCOMPLEX_INVERSE_ZERO = thm"HCOMPLEX_INVERSE_ZERO"; -val HCOMPLEX_DIVISION_BY_ZERO = thm"HCOMPLEX_DIVISION_BY_ZERO"; val hcomplex_mult_inv_left = thm"hcomplex_mult_inv_left"; val hcomplex_mult_left_cancel = thm"hcomplex_mult_left_cancel"; val hcomplex_mult_right_cancel = thm"hcomplex_mult_right_cancel"; val hcomplex_add_divide_distrib = thm"hcomplex_add_divide_distrib"; val hcomplex_of_hypreal = thm"hcomplex_of_hypreal"; -val inj_hcomplex_of_hypreal = thm"inj_hcomplex_of_hypreal"; val hcomplex_of_hypreal_cancel_iff = thm"hcomplex_of_hypreal_cancel_iff"; val hcomplex_of_hypreal_minus = thm"hcomplex_of_hypreal_minus"; val hcomplex_of_hypreal_inverse = thm"hcomplex_of_hypreal_inverse"; @@ -1755,7 +1488,6 @@ val hcmod_hcomplex_of_hypreal = thm"hcmod_hcomplex_of_hypreal"; val hcomplex_of_hypreal_abs = thm"hcomplex_of_hypreal_abs"; val hcnj = thm"hcnj"; -val inj_hcnj = thm"inj_hcnj"; val hcomplex_hcnj_cancel_iff = thm"hcomplex_hcnj_cancel_iff"; val hcomplex_hcnj_hcnj = thm"hcomplex_hcnj_hcnj"; val hcomplex_hcnj_hcomplex_of_hypreal = thm"hcomplex_hcnj_hcomplex_of_hypreal"; @@ -1798,7 +1530,6 @@ val hcpow_minus = thm"hcpow_minus"; val hcmod_hcomplex_inverse = thm"hcmod_hcomplex_inverse"; val hcmod_divide = thm"hcmod_divide"; -val hcomplex_inverse_divide = thm"hcomplex_inverse_divide"; val hcpow_mult = thm"hcpow_mult"; val hcpow_zero = thm"hcpow_zero"; val hcpow_zero2 = thm"hcpow_zero2"; diff -r 67a628beb981 -r 61de62096768 src/HOL/Real/Complex_Numbers.thy --- a/src/HOL/Real/Complex_Numbers.thy Tue Feb 03 11:06:36 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,182 +0,0 @@ -(* Title: HOL/Real/Complex_Numbers.thy - ID: $Id$ - Author: Gertrud Bauer and Markus Wenzel, TU München - License: GPL (GNU GENERAL PUBLIC LICENSE) -*) - -header {* Complex numbers *} - -theory Complex_Numbers = RealPow + Ring_and_Field: - -subsection {* Representation of complex numbers *} - -datatype complex = Complex real real - -consts Re :: "complex => real" -primrec "Re (Complex x y) = x" - -consts Im :: "complex => real" -primrec "Im (Complex x y) = y" - -lemma complex_surj [simp]: "Complex (Re z) (Im z) = z" - by (induct z) simp - -instance complex :: zero .. -instance complex :: one .. -instance complex :: number .. -instance complex :: plus .. -instance complex :: minus .. -instance complex :: times .. -instance complex :: inverse .. - -defs (overloaded) - zero_complex_def: "0 == Complex 0 0" - one_complex_def: "1 == Complex 1 0" - number_of_complex_def: "number_of b == Complex (number_of b) 0" - add_complex_def: "z + w == Complex (Re z + Re w) (Im z + Im w)" - minus_complex_def: "z - w == Complex (Re z - Re w) (Im z - Im w)" - uminus_complex_def: "- z == Complex (- Re z) (- Im z)" - mult_complex_def: "z * w == - Complex (Re z * Re w - Im z * Im w) (Re z * Im w + Im z * Re w)" - inverse_complex_def: "(z::complex) \ 0 ==> inverse z == - Complex (Re z / ((Re z)\ + (Im z)\)) (- Im z / ((Re z)\ + (Im z)\))" - divide_complex_def: "(w::complex) \ 0 ==> z / (w::complex) == z * inverse w" - -lemma complex_equality [intro?]: "Re z = Re w ==> Im z = Im w ==> z = w" - by (induct z, induct w) simp - -lemma Re_zero [simp]: "Re 0 = 0" - and Im_zero [simp]: "Im 0 = 0" - by (simp_all add: zero_complex_def) - -lemma Re_one [simp]: "Re 1 = 1" - and Im_one [simp]: "Im 1 = 0" - by (simp_all add: one_complex_def) - -lemma Re_add [simp]: "Re (z + w) = Re z + Re w" - by (simp add: add_complex_def) - -lemma Im_add [simp]: "Im (z + w) = Im z + Im w" - by (simp add: add_complex_def) - -lemma Re_diff [simp]: "Re (z - w) = Re z - Re w" - by (simp add: minus_complex_def) - -lemma Im_diff [simp]: "Im (z - w) = Im z - Im w" - by (simp add: minus_complex_def) - -lemma Re_uminus [simp]: "Re (-z) = - Re z" - by (simp add: uminus_complex_def) - -lemma Im_uminus [simp]: "Im (-z) = - Im z" - by (simp add: uminus_complex_def) - -lemma Re_mult [simp]: "Re (z * w) = Re z * Re w - Im z * Im w" - by (simp add: mult_complex_def) - -lemma Im_mult [simp]: "Im (z * w) = Re z * Im w + Im z * Re w" - by (simp add: mult_complex_def) - -lemma zero_complex_iff: "(z = 0) = (Re z = 0 \ Im z = 0)" - and one_complex_iff: "(z = 1) = (Re z = 1 \ Im z = 0)" - by (auto simp add: complex_equality) - - -subsection {* The field of complex numbers *} - -instance complex :: field -proof - fix z u v w :: complex - show "(u + v) + w = u + (v + w)" - by (simp add: add_complex_def) - show "z + w = w + z" - by (simp add: add_complex_def) - show "0 + z = z" - by (simp add: add_complex_def zero_complex_def) - show "-z + z = 0" - by (simp add: complex_equality minus_complex_def) - show "z - w = z + -w" - by (simp add: add_complex_def minus_complex_def uminus_complex_def) - show "(u * v) * w = u * (v * w)" - by (simp add: mult_complex_def mult_ac ring_distrib real_diff_def) (* FIXME *) - show "z * w = w * z" - by (simp add: mult_complex_def) - show "1 * z = z" - by (simp add: one_complex_def mult_complex_def) - show "0 \ (1::complex)" --{*for some reason it has to be early*} - by (simp add: zero_complex_def one_complex_def) - show "(u + v) * w = u * w + v * w" - by (simp add: add_complex_def mult_complex_def ring_distrib) - show "z+u = z+v ==> u=v" - proof - - assume eq: "z+u = z+v" - hence "(-z + z) + u = (-z + z) + v" by (simp add: eq add_complex_def) - thus "u = v" by (simp add: add_complex_def) - qed - assume neq: "w \ 0" - thus "z / w = z * inverse w" - by (simp add: divide_complex_def) - show "inverse w * w = 1" - proof - have neq': "Re w * Re w + Im w * Im w \ 0" - proof - - have ge: "0 \ Re w * Re w" "0 \ Im w * Im w" by simp_all - from neq have "Re w \ 0 \ Im w \ 0" by (simp add: zero_complex_iff) - hence "Re w * Re w \ 0 \ Im w * Im w \ 0" by simp - thus ?thesis by rule (insert ge, arith+) - qed - with neq show "Re (inverse w * w) = Re 1" - by (simp add: inverse_complex_def power2_eq_square add_divide_distrib [symmetric]) - from neq show "Im (inverse w * w) = Im 1" - by (simp add: inverse_complex_def power2_eq_square - mult_ac add_divide_distrib [symmetric]) - qed -qed - - -subsection {* Basic operations *} - -instance complex :: power .. -primrec (power_complex) - "z ^ 0 = 1" - "z ^ Suc n = (z::complex) * (z ^ n)" - -lemma complex_power_two: "z\ = z * (z::complex)" - by (simp add: complex_equality numeral_2_eq_2) - - -constdefs - im_unit :: complex ("\") - "\ == Complex 0 1" - -lemma im_unit_square: "\\ = -1" - by (simp add: im_unit_def complex_power_two mult_complex_def number_of_complex_def) - - -constdefs - conjg :: "complex => complex" - "conjg z == Complex (Re z) (- Im z)" - -lemma Re_cong [simp]: "Re (conjg z) = Re z" - by (simp add: conjg_def) - -lemma Im_cong [simp]: "Im (conjg z) = - Im z" - by (simp add: conjg_def) - -lemma Re_conjg_self: "Re (z * conjg z) = (Re z)\ + (Im z)\" - by (simp add: power2_eq_square) - -lemma Im_conjg_self: "Im (z * conjg z) = 0" - by simp - - -subsection {* Embedding other number domains *} - -constdefs - complex :: "'a => complex" - "complex x == Complex (real x) 0"; - -lemma Re_complex [simp]: "Re (complex x) = real x" - by (simp add: complex_def) - -end diff -r 67a628beb981 -r 61de62096768 src/HOL/Real/Real.thy --- a/src/HOL/Real/Real.thy Tue Feb 03 11:06:36 2004 +0100 +++ b/src/HOL/Real/Real.thy Tue Feb 03 15:58:31 2004 +0100 @@ -1,2 +1,2 @@ -Real = RComplete + Complex_Numbers +Real = RComplete + RealPow