# HG changeset patch # User paulson # Date 1075974328 -3600 # Node ID f454b3004f8f574d0f91dc16f21c735cb1d0c0e0 # Parent 9fe787a90a48bd88b58c3dae19b9c415294cc529 tidying up, especially the Complex numbers diff -r 9fe787a90a48 -r f454b3004f8f src/HOL/Complex/CStar.ML --- a/src/HOL/Complex/CStar.ML Thu Feb 05 04:30:38 2004 +0100 +++ b/src/HOL/Complex/CStar.ML Thu Feb 05 10:45:28 2004 +0100 @@ -194,7 +194,7 @@ Goalw [congruent_def] "congruent hcomplexrel (%X. hcomplexrel``{%n. f (X n)})"; -by (safe_tac (claset())); +by (auto_tac (clasimpset() addIffs [hcomplexrel_iff])); by (ALLGOALS(Ultra_tac)); qed "starfunC_congruent"; @@ -203,7 +203,7 @@ "( *fc* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = \ \ Abs_hcomplex(hcomplexrel `` {%n. f (X n)})"; by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1); -by Auto_tac; +by (auto_tac (clasimpset() addIffs [hcomplexrel_iff])); by (Ultra_tac 1); qed "starfunC"; @@ -219,7 +219,7 @@ "( *fcR* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = \ \ Abs_hypreal(hyprel `` {%n. f (X n)})"; by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); -by Auto_tac; +by (auto_tac (clasimpset() addIffs [hcomplexrel_iff])); by (Ultra_tac 1); qed "starfunCR"; @@ -523,7 +523,7 @@ Goalw [congruent_def] "congruent hcomplexrel (%X. hcomplexrel``{%n. f n (X n)})"; -by (safe_tac (claset())); +by (auto_tac (clasimpset() addIffs [hcomplexrel_iff])); by (ALLGOALS(Fuf_tac)); qed "starfunC_n_congruent"; @@ -531,7 +531,7 @@ "( *fcn* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = \ \ Abs_hcomplex(hcomplexrel `` {%n. f n (X n)})"; by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1); -by Auto_tac; +by (auto_tac (clasimpset() addIffs [hcomplexrel_iff])); by (Ultra_tac 1); qed "starfunC_n"; diff -r 9fe787a90a48 -r f454b3004f8f src/HOL/Complex/Complex.thy --- a/src/HOL/Complex/Complex.thy Thu Feb 05 04:30:38 2004 +0100 +++ b/src/HOL/Complex/Complex.thy Thu Feb 05 10:45:28 2004 +0100 @@ -3,12 +3,10 @@ Copyright: 2001 University of Edinburgh *) -header {* Complex numbers *} +header {* Complex Numbers: Rectangular and Polar Representations *} theory Complex = HLog: -subsection {* Representation of complex numbers *} - datatype complex = Complex real real instance complex :: zero .. @@ -89,7 +87,7 @@ (* abbreviation for (cos a + i sin a) *) cis :: "real => complex" - "cis a == complex_of_real(cos a) + ii * complex_of_real(sin a)" + "cis a == Complex (cos a) (sin a)" (* abbreviation for r*(cos a + i sin a) *) rcis :: "[real, real] => complex" @@ -139,7 +137,7 @@ subsection{*Unary Minus*} -lemma complex_minus: "- (Complex x y) = Complex (-x) (-y)" +lemma complex_minus [simp]: "- (Complex x y) = Complex (-x) (-y)" by (simp add: complex_minus_def) lemma complex_Re_minus [simp]: "Re (-z) = - Re z" @@ -151,7 +149,8 @@ subsection{*Addition*} -lemma complex_add: "Complex x1 y1 + Complex x2 y2 = Complex (x1+x2) (y1+y2)" +lemma complex_add [simp]: + "Complex x1 y1 + Complex x2 y2 = Complex (x1+x2) (y1+y2)" by (simp add: complex_add_def) lemma complex_Re_add [simp]: "Re(x + y) = Re(x) + Re(y)" @@ -188,7 +187,7 @@ subsection{*Multiplication*} -lemma complex_mult: +lemma complex_mult [simp]: "Complex x1 y1 * Complex x2 y2 = Complex (x1*x2 - y1*y2) (x1*y2 + y1*x2)" by (simp add: complex_mult_def) @@ -208,7 +207,7 @@ subsection{*Inverse*} -lemma complex_inverse: +lemma complex_inverse [simp]: "inverse (Complex x y) = Complex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))" by (simp add: complex_inverse_def) @@ -272,6 +271,28 @@ subsection{*Embedding Properties for @{term complex_of_real} Map*} +lemma Complex_add_complex_of_real [simp]: + "Complex x y + complex_of_real r = Complex (x+r) y" +by (simp add: complex_of_real_def) + +lemma complex_of_real_add_Complex [simp]: + "complex_of_real r + Complex x y = Complex (r+x) y" +by (simp add: i_def complex_of_real_def) + +lemma Complex_mult_complex_of_real: + "Complex x y * complex_of_real r = Complex (x*r) (y*r)" +by (simp add: complex_of_real_def) + +lemma complex_of_real_mult_Complex: + "complex_of_real r * Complex x y = Complex (r*x) (r*y)" +by (simp add: i_def complex_of_real_def) + +lemma i_complex_of_real [simp]: "ii * complex_of_real r = Complex 0 r" +by (simp add: i_def complex_of_real_def) + +lemma complex_of_real_i [simp]: "complex_of_real r * ii = Complex 0 r" +by (simp add: i_def complex_of_real_def) + lemma complex_of_real_one [simp]: "complex_of_real 1 = 1" by (simp add: complex_one_def complex_of_real_def) @@ -313,7 +334,7 @@ real_divide_def) done -lemma complex_mod: "cmod (Complex x y) = sqrt(x ^ 2 + y ^ 2)" +lemma complex_mod [simp]: "cmod (Complex x y) = sqrt(x ^ 2 + y ^ 2)" by (simp add: cmod_def) lemma complex_mod_zero [simp]: "cmod(0) = 0" @@ -330,6 +351,46 @@ by simp +subsection{*The Functions @{term Re} and @{term Im}*} + +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) + +lemma complex_Im_mult_eq: "Im (w * z) = Re w * Im z + Im w * Re z" +by (induct z, induct w, simp add: complex_mult) + +lemma Re_i_times [simp]: "Re(ii * z) = - Im z" +by (simp add: complex_Re_mult_eq) + +lemma Re_times_i [simp]: "Re(z * ii) = - Im z" +by (simp add: complex_Re_mult_eq) + +lemma Im_i_times [simp]: "Im(ii * z) = Re z" +by (simp add: complex_Im_mult_eq) + +lemma Im_times_i [simp]: "Im(z * ii) = Re z" +by (simp add: complex_Im_mult_eq) + +lemma complex_Re_mult: "[| Im w = 0; Im z = 0 |] ==> Re(w * z) = Re(w) * Re(z)" +by (simp add: complex_Re_mult_eq) + +lemma complex_Re_mult_complex_of_real [simp]: + "Re (z * complex_of_real c) = Re(z) * c" +by (simp add: complex_Re_mult_eq) + +lemma complex_Im_mult_complex_of_real [simp]: + "Im (z * complex_of_real c) = Im(z) * c" +by (simp add: complex_Im_mult_eq) + +lemma complex_Re_mult_complex_of_real2 [simp]: + "Re (complex_of_real c * z) = c * Re(z)" +by (simp add: complex_Re_mult_eq) + +lemma complex_Im_mult_complex_of_real2 [simp]: + "Im (complex_of_real c * z) = c * Im(z)" +by (simp add: complex_Im_mult_eq) + + subsection{*Conjugation is an Automorphism*} lemma complex_cnj: "cnj (Complex x y) = Complex x (-y)" @@ -420,14 +481,20 @@ 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]) 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) done +lemma cmod_unit_one [simp]: "cmod (Complex (cos a) (sin a)) = 1" +by (simp add: cmod_def) + +lemma cmod_complex_polar [simp]: + "cmod (complex_of_real r * Complex (cos a) (sin a)) = abs r" +by (simp only: cmod_unit_one complex_mod_mult, simp) + 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) @@ -506,10 +573,7 @@ done 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 [simp]: "inverse(x/y) = y/(x::complex)" -by (simp add: complex_divide_def inverse_mult_distrib mult_commute) +by (simp add: complex_divide_def real_divide_def complex_mod_mult complex_mod_inverse) subsection{*Exponentiation*} @@ -566,20 +630,7 @@ by (simp add: sgn_def) lemma sgn_eq: "sgn z = z / complex_of_real (cmod z)" -apply (simp add: sgn_def) -done - -lemma complex_split: "\x y. z = complex_of_real(x) + ii * complex_of_real(y)" -apply (induct z) -apply (auto simp add: complex_of_real_def i_def complex_mult complex_add) -done - -(*????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) - -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) +by (simp add: sgn_def) lemma i_mult_eq: "ii * ii = complex_of_real (-1)" by (simp add: i_def complex_of_real_def complex_mult complex_add) @@ -587,78 +638,22 @@ lemma i_mult_eq2 [simp]: "ii * ii = -(1::complex)" by (simp add: i_def complex_one_def complex_mult complex_minus) -lemma cmod_i: "cmod (complex_of_real(x) + ii * complex_of_real(y)) = - sqrt (x ^ 2 + y ^ 2)" -by (simp add: complex_mult complex_add i_def complex_of_real_def cmod_def) - -lemma complex_eq_Re_eq: - "complex_of_real xa + ii * complex_of_real ya = - complex_of_real xb + ii * complex_of_real yb - ==> xa = xb" -by (simp add: complex_of_real_def i_def complex_mult complex_add) - -lemma complex_eq_Im_eq: - "complex_of_real xa + ii * complex_of_real ya = - complex_of_real xb + ii * complex_of_real yb - ==> ya = yb" -by (simp add: complex_of_real_def i_def complex_mult complex_add) - -(*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) - -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) - -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) - -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) - 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 + "(Complex x y = complex_of_real xa) = (x = xa & y = 0)" +by (simp add: complex_of_real_def) 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) + "(Complex x y = complex_of_real xa) = (x = xa & y = 0)" +by (simp add: complex_of_real_def) -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 +lemma Complex_eq_0 [simp]: "(Complex x y = 0) = (x = 0 & y = 0)" +by (simp add: complex_zero_def) -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) +lemma Complex_eq_1 [simp]: "(Complex x y = 1) = (x = 1 & y = 0)" +by (simp add: complex_one_def) -lemma complex_split_Re_zero: - "complex_of_real x + ii * complex_of_real y = 0 - ==> x = 0" -by (simp add: complex_of_real_def i_def complex_zero_def complex_mult complex_add) - -lemma complex_split_Im_zero: - "complex_of_real x + ii * complex_of_real y = 0 - ==> y = 0" -by (simp add: complex_of_real_def i_def complex_zero_def complex_mult complex_add) +lemma Complex_eq_i [simp]: "(Complex x y = ii) = (x = 0 & y = 1)" +by (simp add: i_def) lemma Re_sgn [simp]: "Re(sgn z) = Re(z)/cmod z" apply (induct z) @@ -687,77 +682,53 @@ 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 [simp]: "Re (ii * complex_of_real y) = 0" -by (simp add: i_def complex_of_real_def complex_mult) - -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) - lemma cos_arg_i_mult_zero_pos: - "0 < y ==> cos (arg(ii * complex_of_real y)) = 0" + "0 < y ==> cos (arg(Complex 0 y)) = 0" apply (simp add: arg_def abs_if) apply (rule_tac a = "pi/2" in someI2, auto) apply (rule order_less_trans [of _ 0], auto) done lemma cos_arg_i_mult_zero_neg: - "y < 0 ==> cos (arg(ii * complex_of_real y)) = 0" + "y < 0 ==> cos (arg(Complex 0 y)) = 0" apply (simp add: arg_def abs_if) apply (rule_tac a = "- pi/2" in someI2, auto) 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]) -apply (auto simp add: cos_arg_i_mult_zero_pos cos_arg_i_mult_zero_neg) -done + "y \ 0 ==> cos (arg(Complex 0 y)) = 0" +by (auto simp add: linorder_neq_iff cos_arg_i_mult_zero_pos cos_arg_i_mult_zero_neg) subsection{*Finally! Polar Form for Complex Numbers*} 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) + "\r a. z = complex_of_real r * (Complex (cos a) (sin a))" +apply (induct z) +apply (auto simp add: polar_Ex complex_of_real_mult_Complex) done lemma rcis_Ex: "\r a. z = rcis r a" -apply (simp add: rcis_def cis_def) -apply (rule complex_split_polar) +apply (induct z) +apply (simp add: rcis_def cis_def polar_Ex complex_of_real_mult_Complex) done -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) - lemma Re_rcis [simp]: "Re(rcis r a) = r * cos a" by (simp add: rcis_def cis_def) -lemma Im_complex_polar [simp]: - "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) - lemma Im_rcis [simp]: "Im(rcis r a) = r * sin a" 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))) = - abs r" -by (auto simp add: right_distrib cmod_i complex_of_real_mult - right_distrib [symmetric] power_mult_distrib mult_ac - simp del: realpow_Suc) +lemma sin_cos_squared_add2_mult: "(r * cos a)\ + (r * sin a)\ = r\" +proof - + have "(r * cos a)\ + (r * sin a)\ = r\ * ((cos a)\ + (sin a)\)" + by (simp only: power_mult_distrib right_distrib) + thus ?thesis by simp +qed lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r" -by (simp add: rcis_def cis_def) +by (simp add: rcis_def cis_def sin_cos_squared_add2_mult) lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))" apply (simp add: cmod_def) @@ -774,24 +745,6 @@ lemma complex_In_mult_cnj_zero [simp]: "Im (z * cnj z) = 0" by (induct z, simp add: complex_cnj complex_mult) -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 [simp]: - "Re (z * complex_of_real c) = Re(z) * c" -by (induct z, simp add: complex_of_real_def complex_mult) - -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) - -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) - -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) (*---------------------------------------------------------------------------*) (* (r1 * cis a) * (r2 * cis b) = r1 * r2 * cis (a + b) *) @@ -801,21 +754,13 @@ 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 - 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) -apply (auto simp add: complex_add_assoc [symmetric] complex_of_real_add right_distrib real_diff_def mult_ac add_ac) -done +by (simp add: rcis_def cis_def complex_of_real_mult_Complex cos_add sin_add right_distrib right_diff_distrib) lemma cis_mult: "cis a * cis b = cis (a + b)" by (simp add: cis_rcis_eq rcis_mult) lemma cis_zero [simp]: "cis 0 = 1" -by (simp add: cis_def) - -lemma cis_zero2 [simp]: "cis 0 = complex_of_real 1" -by (simp add: cis_def) +by (simp add: cis_def complex_one_def) lemma rcis_zero_mod [simp]: "rcis 0 a = 0" by (simp add: rcis_def) @@ -825,8 +770,7 @@ 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 +by (simp add: complex_of_real_def complex_one_def complex_minus) lemma complex_i_mult_minus [simp]: "ii * (ii * x) = - x" by (simp add: complex_mult_assoc [symmetric]) @@ -834,10 +778,7 @@ lemma cis_real_of_nat_Suc_mult: "cis (real (Suc n) * a) = cis a * cis (real n * a)" -apply (simp add: cis_def) -apply (auto simp add: real_of_nat_Suc left_distrib cos_add sin_add left_distrib right_distrib complex_of_real_add complex_of_real_mult mult_ac add_ac) -apply (auto simp add: right_distrib [symmetric] complex_mult_assoc [symmetric] i_mult_eq complex_of_real_mult complex_of_real_add complex_add_assoc [symmetric] complex_of_real_minus [symmetric] real_diff_def mult_ac simp del: i_mult_eq2) -done +by (simp add: cis_def real_of_nat_Suc left_distrib cos_add sin_add right_distrib) lemma DeMoivre: "(cis a) ^ n = cis (real n * a)" apply (induct_tac "n") @@ -852,12 +793,7 @@ 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 - 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) -done +by (simp add: divide_inverse_zero rcis_def complex_of_real_inverse) lemma cis_divide: "cis a / cis b = cis (a - b)" by (simp add: complex_divide_def cis_mult real_diff_def) @@ -880,35 +816,13 @@ lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)" by (auto simp add: DeMoivre) -lemma expi_Im_split: - "expi (ii * complex_of_real y) = - complex_of_real (cos y) + ii * complex_of_real (sin y)" -by (simp add: expi_def cis_def) - -lemma expi_Im_cis: - "expi (ii * complex_of_real y) = cis y" -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) -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 [simp]: "expi (0::complex) = 1" by (simp add: expi_def) -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) - -lemma complex_Im_mult_eq: - "Im (w * z) = Re w * Im z + Im w * Re z" -apply (induct z, induct w, simp add: complex_mult) -done - 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) @@ -1023,46 +937,22 @@ val complexpow_minus = thm"complexpow_minus"; val complex_mod_inverse = thm"complex_mod_inverse"; val complex_mod_divide = thm"complex_mod_divide"; -val complex_inverse_divide = thm"complex_inverse_divide"; val complexpow_i_squared = thm"complexpow_i_squared"; val complex_i_not_zero = thm"complex_i_not_zero"; val sgn_zero = thm"sgn_zero"; val sgn_one = thm"sgn_one"; val sgn_minus = thm"sgn_minus"; val sgn_eq = thm"sgn_eq"; -val complex_split = thm"complex_split"; -val Re_complex_i = thm"Re_complex_i"; -val Im_complex_i = thm"Im_complex_i"; val i_mult_eq = thm"i_mult_eq"; val i_mult_eq2 = thm"i_mult_eq2"; -val cmod_i = thm"cmod_i"; -val complex_eq_Re_eq = thm"complex_eq_Re_eq"; -val complex_eq_Im_eq = thm"complex_eq_Im_eq"; -val complex_eq_cancel_iff = thm"complex_eq_cancel_iff"; -val complex_eq_cancel_iffA = thm"complex_eq_cancel_iffA"; -val complex_eq_cancel_iffB = thm"complex_eq_cancel_iffB"; -val complex_eq_cancel_iffC = thm"complex_eq_cancel_iffC"; -val complex_eq_cancel_iff2 = thm"complex_eq_cancel_iff2"; -val complex_eq_cancel_iff2a = thm"complex_eq_cancel_iff2a"; -val complex_eq_cancel_iff3 = thm"complex_eq_cancel_iff3"; -val complex_eq_cancel_iff3a = thm"complex_eq_cancel_iff3a"; -val complex_split_Re_zero = thm"complex_split_Re_zero"; -val complex_split_Im_zero = thm"complex_split_Im_zero"; val Re_sgn = thm"Re_sgn"; val Im_sgn = thm"Im_sgn"; val complex_inverse_complex_split = thm"complex_inverse_complex_split"; -val Re_mult_i_eq = thm"Re_mult_i_eq"; -val Im_mult_i_eq = thm"Im_mult_i_eq"; -val complex_mod_mult_i = thm"complex_mod_mult_i"; val cos_arg_i_mult_zero = thm"cos_arg_i_mult_zero"; val complex_of_real_zero_iff = thm"complex_of_real_zero_iff"; -val complex_split_polar = thm"complex_split_polar"; val rcis_Ex = thm"rcis_Ex"; -val Re_complex_polar = thm"Re_complex_polar"; val Re_rcis = thm"Re_rcis"; -val Im_complex_polar = thm"Im_complex_polar"; val Im_rcis = thm"Im_rcis"; -val complex_mod_complex_polar = thm"complex_mod_complex_polar"; val complex_mod_rcis = thm"complex_mod_rcis"; val complex_mod_sqrt_Re_mult_cnj = thm"complex_mod_sqrt_Re_mult_cnj"; val complex_Re_cnj = thm"complex_Re_cnj"; @@ -1077,7 +967,6 @@ val rcis_mult = thm"rcis_mult"; val cis_mult = thm"cis_mult"; val cis_zero = thm"cis_zero"; -val cis_zero2 = thm"cis_zero2"; val rcis_zero_mod = thm"rcis_zero_mod"; val rcis_zero_arg = thm"rcis_zero_arg"; val complex_of_real_minus_one = thm"complex_of_real_minus_one"; @@ -1093,10 +982,7 @@ val Im_cis = thm"Im_cis"; val cos_n_Re_cis_pow_n = thm"cos_n_Re_cis_pow_n"; val sin_n_Im_cis_pow_n = thm"sin_n_Im_cis_pow_n"; -val expi_Im_split = thm"expi_Im_split"; -val expi_Im_cis = thm"expi_Im_cis"; val expi_add = thm"expi_add"; -val expi_complex_split = thm"expi_complex_split"; val expi_zero = thm"expi_zero"; val complex_Re_mult_eq = thm"complex_Re_mult_eq"; val complex_Im_mult_eq = thm"complex_Im_mult_eq"; diff -r 9fe787a90a48 -r f454b3004f8f src/HOL/Complex/ComplexBin.ML --- a/src/HOL/Complex/ComplexBin.ML Thu Feb 05 04:30:38 2004 +0100 +++ b/src/HOL/Complex/ComplexBin.ML Thu Feb 05 10:45:28 2004 +0100 @@ -367,9 +367,9 @@ val prove_conv = Bin_Simprocs.prove_conv_nohyps_novars fun norm_tac simps = ALLGOALS (simp_tac (HOL_ss addsimps simps)) val simplify_meta_eq = Bin_Simprocs.simplify_meta_eq - end + end; -structure ComplexAbstractNumerals = AbstractNumeralsFun (ComplexAbstractNumeralsData) +structure ComplexAbstractNumerals = AbstractNumeralsFun (ComplexAbstractNumeralsData); (*For addition, we already have rules for the operand 0. Multiplication is omitted because there are already special rules for @@ -386,7 +386,7 @@ ComplexAbstractNumerals.proc diff_complex_number_of), ("complex_eq_eval_numerals", ["(m::complex) = 0", "(m::complex) = 1", "(m::complex) = number_of v"], - ComplexAbstractNumerals.proc eq_complex_number_of)] + ComplexAbstractNumerals.proc eq_complex_number_of)]; end; @@ -447,44 +447,7 @@ Addsimps [complex_of_real_zero_iff]; -(*** Real and imaginary stuff ***) - -Goalw [complex_number_of_def] - "((number_of xa :: complex) + ii * number_of ya = \ -\ number_of xb + ii * number_of yb) = \ -\ (((number_of xa :: complex) = number_of xb) & \ -\ ((number_of ya :: complex) = number_of yb))"; -by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iff])); -qed "complex_number_of_eq_cancel_iff"; -Addsimps [complex_number_of_eq_cancel_iff]; - -Goalw [complex_number_of_def] - "((number_of xa :: complex) + number_of ya * ii = \ -\ number_of xb + number_of yb * ii) = \ -\ (((number_of xa :: complex) = number_of xb) & \ -\ ((number_of ya :: complex) = number_of yb))"; -by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iffA])); -qed "complex_number_of_eq_cancel_iffA"; -Addsimps [complex_number_of_eq_cancel_iffA]; - -Goalw [complex_number_of_def] - "((number_of xa :: complex) + number_of ya * ii = \ -\ number_of xb + ii * number_of yb) = \ -\ (((number_of xa :: complex) = number_of xb) & \ -\ ((number_of ya :: complex) = number_of yb))"; -by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iffB])); -qed "complex_number_of_eq_cancel_iffB"; -Addsimps [complex_number_of_eq_cancel_iffB]; - -Goalw [complex_number_of_def] - "((number_of xa :: complex) + ii * number_of ya = \ -\ number_of xb + number_of yb * ii) = \ -\ (((number_of xa :: complex) = number_of xb) & \ -\ ((number_of ya :: complex) = number_of yb))"; -by (auto_tac (claset(), HOL_ss addsimps [complex_eq_cancel_iffC])); -qed "complex_number_of_eq_cancel_iffC"; -Addsimps [complex_number_of_eq_cancel_iffC]; - +(*Convert??? Goalw [complex_number_of_def] "((number_of xa :: complex) + ii * number_of ya = \ \ number_of xb) = \ @@ -524,6 +487,7 @@ complex_of_real_zero_iff])); qed "complex_number_of_eq_cancel_iff3a"; Addsimps [complex_number_of_eq_cancel_iff3a]; +*) Goalw [complex_number_of_def] "cnj (number_of v :: complex) = number_of v"; by (rtac complex_cnj_complex_of_real 1); diff -r 9fe787a90a48 -r f454b3004f8f src/HOL/Complex/NSCA.ML --- a/src/HOL/Complex/NSCA.ML Thu Feb 05 04:30:38 2004 +0100 +++ b/src/HOL/Complex/NSCA.ML Thu Feb 05 10:45:28 2004 +0100 @@ -943,11 +943,8 @@ \ |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) : SComplex"; by (auto_tac (claset(),simpset() addsimps [SComplex_def, hcomplex_of_complex_def,SReal_def,hypreal_of_real_def])); -by (res_inst_tac [("x","complex_of_real r + ii * complex_of_real ra")] exI 1); +by (res_inst_tac [("x","Complex r ra")] exI 1); by (Ultra_tac 1); -by (case_tac "X x" 1); -by (auto_tac (claset(),simpset() addsimps [complex_of_real_def,i_def, - complex_add,complex_mult])); qed "Reals_Re_Im_SComplex"; Goal "(Abs_hcomplex(hcomplexrel ``{%n. X n}) : SComplex) = \ @@ -987,8 +984,7 @@ by (res_inst_tac [("z","t")] eq_Abs_hypreal 1); by (res_inst_tac [("z","ta")] eq_Abs_hypreal 1); by Auto_tac; -by (res_inst_tac [("x","%n. complex_of_real (xa n) + ii * complex_of_real (xb n)")] - exI 1); +by (res_inst_tac [("x","%n. Complex (xa n) (xb n)")] exI 1); by Auto_tac; qed "stc_part_Ex"; diff -r 9fe787a90a48 -r f454b3004f8f src/HOL/Complex/NSComplex.thy --- a/src/HOL/Complex/NSComplex.thy Thu Feb 05 04:30:38 2004 +0100 +++ b/src/HOL/Complex/NSComplex.thy Thu Feb 05 10:45:28 2004 +0100 @@ -37,15 +37,15 @@ hcomplex_diff_def: "w - z == w + -(z::hcomplex)" + hcinv_def: + "inverse(P) == Abs_hcomplex(UN X: Rep_hcomplex(P). + hcomplexrel `` {%n. inverse(X n)})" + constdefs hcomplex_of_complex :: "complex => hcomplex" "hcomplex_of_complex z == Abs_hcomplex(hcomplexrel `` {%n. z})" - hcinv :: "hcomplex => hcomplex" - "inverse(P) == Abs_hcomplex(UN X: Rep_hcomplex(P). - hcomplexrel `` {%n. inverse(X n)})" - (*--- real and Imaginary parts ---*) hRe :: "hcomplex => hypreal" @@ -99,6 +99,11 @@ "hexpi z == hcomplex_of_hypreal(( *f* exp) (hRe z)) * hcis (hIm z)" +constdefs + HComplex :: "[hypreal,hypreal] => hcomplex" + "HComplex x y == hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y" + + defs (overloaded) (*----------- division ----------*) @@ -182,8 +187,7 @@ apply (force simp add: Rep_hcomplex_inverse hcomplexrel_def) done -(*??delete*) -lemma hcomplexrel_iff [iff]: +lemma hcomplexrel_iff [simp]: "((X,Y): hcomplexrel) = ({n. X n = Y n}: FreeUltrafilterNat)" by (simp add: hcomplexrel_def) @@ -195,7 +199,7 @@ Abs_hypreal(hyprel `` {%n. Re(X n)})" apply (simp add: hRe_def) apply (rule_tac f = Abs_hypreal in arg_cong) -apply (auto, ultra) +apply (auto iff: hcomplexrel_iff, ultra) done lemma hIm: @@ -203,17 +207,20 @@ Abs_hypreal(hyprel `` {%n. Im(X n)})" apply (simp add: hIm_def) apply (rule_tac f = Abs_hypreal in arg_cong) -apply (auto, ultra) +apply (auto iff: hcomplexrel_iff, ultra) done lemma hcomplex_hRe_hIm_cancel_iff: "(w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))" 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 (auto simp add: hRe hIm complex_Re_Im_cancel_iff iff: hcomplexrel_iff) apply (ultra+) done +lemma hcomplex_equality [intro?]: "hRe z = hRe w ==> hIm z = hIm w ==> z = w" +by (simp add: hcomplex_hRe_hIm_cancel_iff) + lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0" by (simp add: hcomplex_zero_def hRe hypreal_zero_num) @@ -231,14 +238,15 @@ lemma hcomplex_add_congruent2: "congruent2 hcomplexrel (%X Y. hcomplexrel `` {%n. X n + Y n})" -by (auto simp add: congruent2_def, ultra) +by (auto simp add: congruent2_def iff: hcomplexrel_iff, ultra) lemma hcomplex_add: - "Abs_hcomplex(hcomplexrel``{%n. X n}) + Abs_hcomplex(hcomplexrel``{%n. Y n}) = - Abs_hcomplex(hcomplexrel``{%n. X n + Y n})" + "Abs_hcomplex(hcomplexrel``{%n. X n}) + + Abs_hcomplex(hcomplexrel``{%n. Y n}) = + Abs_hcomplex(hcomplexrel``{%n. X n + Y n})" apply (simp add: hcomplex_add_def) apply (rule_tac f = Abs_hcomplex in arg_cong) -apply (auto, ultra) +apply (auto simp add: iff: hcomplexrel_iff, ultra) done lemma hcomplex_add_commute: "(z::hcomplex) + w = w + z" @@ -286,7 +294,7 @@ Abs_hcomplex(hcomplexrel `` {%n. -(X n)})" apply (simp add: hcomplex_minus_def) apply (rule_tac f = Abs_hcomplex in arg_cong) -apply (auto, ultra) +apply (auto iff: hcomplexrel_iff, ultra) done lemma hcomplex_add_minus_left: "-z + z = (0::hcomplex)" @@ -303,7 +311,7 @@ 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) +apply (auto iff: hcomplexrel_iff, ultra) done lemma hcomplex_mult_commute: "(w::hcomplex) * z = z * w" @@ -350,7 +358,7 @@ Abs_hcomplex(hcomplexrel `` {%n. inverse (X n)})" apply (simp add: hcinv_def) apply (rule_tac f = Abs_hcomplex in arg_cong) -apply (auto, ultra) +apply (auto iff: hcomplexrel_iff, ultra) done lemma hcomplex_mult_inv_left: @@ -428,6 +436,15 @@ apply (simp add: minus_equation_iff [of x y]) done +lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1" +by (simp add: iii_def hcomplex_mult hcomplex_one_def hcomplex_minus) + +lemma hcomplex_i_mult_left [simp]: "iii * (iii * z) = -z" +by (simp add: mult_assoc [symmetric]) + +lemma hcomplex_i_not_zero [simp]: "iii \ 0" +by (simp add: iii_def hcomplex_zero_def) + subsection{*More Multiplication Laws*} @@ -469,7 +486,7 @@ "hcomplex_of_hypreal (Abs_hypreal(hyprel `` {%n. X n})) = Abs_hcomplex(hcomplexrel `` {%n. complex_of_real (X n)})" apply (simp add: hcomplex_of_hypreal_def) -apply (rule_tac f = Abs_hcomplex in arg_cong, auto, ultra) +apply (rule_tac f = Abs_hcomplex in arg_cong, auto iff: hcomplexrel_iff, ultra) done lemma hcomplex_of_hypreal_cancel_iff [iff]: @@ -541,6 +558,34 @@ by (auto simp add: hcomplex_of_hypreal epsilon_def hcomplex_zero_def) +subsection{*HComplex theorems*} + +lemma hRe_HComplex [simp]: "hRe (HComplex x y) = x" +apply (rule eq_Abs_hypreal [of x]) +apply (rule eq_Abs_hypreal [of y]) +apply (simp add: HComplex_def hRe iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal) +done + +lemma hIm_HComplex [simp]: "hIm (HComplex x y) = y" +apply (rule eq_Abs_hypreal [of x]) +apply (rule eq_Abs_hypreal [of y]) +apply (simp add: HComplex_def hIm iii_def hcomplex_add hcomplex_mult hcomplex_of_hypreal) +done + +text{*Relates the two nonstandard constructions*} +lemma HComplex_eq_Abs_hcomplex_Complex: + "HComplex (Abs_hypreal (hyprel `` {X})) (Abs_hypreal (hyprel `` {Y})) = + Abs_hcomplex(hcomplexrel `` {%n::nat. Complex (X n) (Y n)})"; +by (simp add: hcomplex_hRe_hIm_cancel_iff hRe hIm) + +lemma hcomplex_surj [simp]: "HComplex (hRe z) (hIm z) = z" +by (simp add: hcomplex_equality) + +lemma hcomplex_induct [case_names rect, induct type: hcomplex]: + "(\x y. P (HComplex x y)) ==> P z" +by (rule hcomplex_surj [THEN subst], blast) + + subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*} lemma hcmod: @@ -549,12 +594,11 @@ apply (simp add: hcmod_def) apply (rule_tac f = Abs_hypreal in arg_cong) -apply (auto, ultra) +apply (auto iff: hcomplexrel_iff, ultra) done lemma hcmod_zero [simp]: "hcmod(0) = 0" -apply (simp add: hcomplex_zero_def hypreal_zero_def hcmod) -done +by (simp add: hcomplex_zero_def hypreal_zero_def hcmod) lemma hcmod_one [simp]: "hcmod(1) = 1" by (simp add: hcomplex_one_def hcmod hypreal_one_num) @@ -569,6 +613,64 @@ hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))" by simp +lemma HComplex_inject [simp]: "HComplex x y = HComplex x' y' = (x=x' & y=y')" +apply (rule iffI) + prefer 2 apply simp +apply (simp add: HComplex_def iii_def) +apply (rule eq_Abs_hypreal [of x]) +apply (rule eq_Abs_hypreal [of y]) +apply (rule eq_Abs_hypreal [of x']) +apply (rule eq_Abs_hypreal [of y']) +apply (auto simp add: iii_def hcomplex_mult hcomplex_add hcomplex_of_hypreal) +apply (ultra+) +done + +lemma HComplex_add [simp]: + "HComplex x1 y1 + HComplex x2 y2 = HComplex (x1+x2) (y1+y2)" +by (simp add: HComplex_def hcomplex_of_hypreal_add [symmetric] add_ac right_distrib) + +lemma HComplex_minus [simp]: "- HComplex x y = HComplex (-x) (-y)" +by (simp add: HComplex_def hcomplex_of_hypreal_minus) + +lemma HComplex_diff [simp]: + "HComplex x1 y1 - HComplex x2 y2 = HComplex (x1-x2) (y1-y2)" +by (simp add: diff_minus) + +lemma HComplex_mult [simp]: + "HComplex x1 y1 * HComplex x2 y2 = HComplex (x1*x2 - y1*y2) (x1*y2 + y1*x2)" +by (simp add: HComplex_def diff_minus hcomplex_of_hypreal_minus + hcomplex_of_hypreal_add [symmetric] hcomplex_of_hypreal_mult [symmetric] + add_ac mult_ac right_distrib) + +(*HComplex_inverse is proved below*) + +lemma hcomplex_of_hypreal_eq: "hcomplex_of_hypreal r = HComplex r 0" +by (simp add: HComplex_def) + +lemma HComplex_add_hcomplex_of_hypreal [simp]: + "HComplex x y + hcomplex_of_hypreal r = HComplex (x+r) y" +by (simp add: hcomplex_of_hypreal_eq) + +lemma hcomplex_of_hypreal_add_HComplex [simp]: + "hcomplex_of_hypreal r + HComplex x y = HComplex (r+x) y" +by (simp add: i_def hcomplex_of_hypreal_eq) + +lemma HComplex_mult_hcomplex_of_hypreal: + "HComplex x y * hcomplex_of_hypreal r = HComplex (x*r) (y*r)" +by (simp add: hcomplex_of_hypreal_eq) + +lemma hcomplex_of_hypreal_mult_HComplex: + "hcomplex_of_hypreal r * HComplex x y = HComplex (r*x) (r*y)" +by (simp add: i_def hcomplex_of_hypreal_eq) + +lemma i_hcomplex_of_hypreal [simp]: + "iii * hcomplex_of_hypreal r = HComplex 0 r" +by (simp add: HComplex_def) + +lemma hcomplex_of_hypreal_i [simp]: + "hcomplex_of_hypreal r * iii = HComplex 0 r" +by (simp add: mult_commute) + subsection{*Conjugation*} @@ -577,7 +679,7 @@ Abs_hcomplex(hcomplexrel `` {%n. cnj(X n)})" apply (simp add: hcnj_def) apply (rule_tac f = Abs_hcomplex in arg_cong) -apply (auto, ultra) +apply (auto iff: hcomplexrel_iff, ultra) done lemma hcomplex_hcnj_cancel_iff [iff]: "(hcnj x = hcnj y) = (x = y)" @@ -777,7 +879,7 @@ Abs_hcomplex(hcomplexrel``{%n. X n ^ Y n})" apply (simp add: hcpow_def) apply (rule_tac f = Abs_hcomplex in arg_cong) -apply (auto, ultra) +apply (auto iff: hcomplexrel_iff, ultra) done lemma hcomplex_of_hypreal_hyperpow: @@ -817,6 +919,9 @@ show "z^(Suc n) = z * (z^n)" by simp qed +lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = - 1" +by (simp add: power2_eq_square) + lemma hcomplex_of_hypreal_pow: "hcomplex_of_hypreal (x ^ n) = (hcomplex_of_hypreal x) ^ n" @@ -872,15 +977,6 @@ lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0" by (blast intro: ccontr dest: hcpow_not_zero) -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 [simp]: "iii ^ 2 = - 1" -by (simp add: numeral_2_eq_2) - -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})" @@ -888,6 +984,7 @@ + subsection{*The Function @{term hsgn}*} lemma hsgn: @@ -895,7 +992,7 @@ Abs_hcomplex(hcomplexrel `` {%n. sgn (X n)})" apply (simp add: hsgn_def) apply (rule_tac f = Abs_hcomplex in arg_cong) -apply (auto, ultra) +apply (auto iff: hcomplexrel_iff, ultra) done lemma hsgn_zero [simp]: "hsgn 0 = 0" @@ -914,144 +1011,33 @@ 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, auto) -done -lemma complex_split2: - "\(n::nat). \x y. (z n) = complex_of_real(x) + ii * complex_of_real(y)" -by (blast intro: complex_split) - -(* Interesting proof! *) -lemma hcomplex_split: - "\x y. z = hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)" -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 (drule choice, safe)+ -apply (rule_tac x = f in exI) -apply (rule_tac x = fa in exI, auto) -done - -lemma hRe_hcomplex_i [simp]: - "hRe(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = x" -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 - -lemma hIm_hcomplex_i [simp]: - "hIm(hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = y" +lemma hcmod_i: "hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)" 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 - -lemma hcmod_i: - "hcmod (hcomplex_of_hypreal(x) + iii * hcomplex_of_hypreal(y)) = - ( *f* sqrt) (x ^ 2 + y ^ 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 (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 (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) +apply (rule eq_Abs_hypreal [of y]) +apply (simp add: HComplex_eq_Abs_hcomplex_Complex starfun + hypreal_mult hypreal_add hcmod numeral_2_eq_2) done -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))" -by (auto intro: hcomplex_eq_hIm_eq hcomplex_eq_hRe_eq) - -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 (simp add: hcomplex_mult_commute) -done - -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 (simp add: hcomplex_mult_commute) -done - -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 (simp add: hcomplex_mult_commute) -done +lemma hcomplex_eq_cancel_iff1 [simp]: + "(hcomplex_of_hypreal xa = HComplex x y) = (xa = x & y = 0)" +by (simp add: hcomplex_of_hypreal_eq) 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 (simp del: hcomplex_eq_cancel_iff) -done + "(HComplex x y = hcomplex_of_hypreal xa) = (x = xa & y = 0)" +by (simp add: hcomplex_of_hypreal_eq) -lemma hcomplex_eq_cancel_iff2a [simp]: - "(hcomplex_of_hypreal x + hcomplex_of_hypreal y * iii = - hcomplex_of_hypreal xa) = (x = xa & y = 0)" -apply (simp add: hcomplex_mult_commute) -done - -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 (simp del: hcomplex_eq_cancel_iff) -done +lemma HComplex_eq_0 [simp]: "(HComplex x y = 0) = (x = 0 & y = 0)" +by (insert hcomplex_eq_cancel_iff2 [of _ _ 0], simp) -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 (simp add: hcomplex_mult_commute) -done +lemma HComplex_eq_1 [simp]: "(HComplex x y = 1) = (x = 1 & y = 0)" +by (insert hcomplex_eq_cancel_iff2 [of _ _ 1], simp) -lemma hcomplex_split_hRe_zero: - "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0 - ==> x = 0" -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 i_eq_HComplex_0_1: "iii = HComplex 0 1" +by (insert hcomplex_of_hypreal_i [of 1], simp) -lemma hcomplex_split_hIm_zero: - "hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y = 0 - ==> y = 0" -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 HComplex_eq_i [simp]: "(HComplex x y = iii) = (x = 0 & y = 1)" +by (simp add: i_eq_HComplex_0_1) lemma hRe_hsgn [simp]: "hRe(hsgn z) = hRe(z)/hcmod z" apply (rule eq_Abs_hcomplex [of z]) @@ -1064,8 +1050,7 @@ done 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 +by (auto intro: real_sum_squares_cancel) lemma hcomplex_inverse_complex_split: "inverse(hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y) = @@ -1074,8 +1059,16 @@ 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) +apply (simp add: diff_minus) done +lemma HComplex_inverse: + "inverse (HComplex x y) = + HComplex (x/(x ^ 2 + y ^ 2)) (-y/(x ^ 2 + y ^ 2))" +by (simp only: HComplex_def hcomplex_inverse_complex_split, simp) + + + lemma hRe_mult_i_eq[simp]: "hRe (iii * hcomplex_of_hypreal y) = 0" apply (simp add: iii_def) @@ -1096,7 +1089,7 @@ done lemma hcmod_mult_i2 [simp]: "hcmod (hcomplex_of_hypreal y * iii) = abs y" -by (simp add: hcomplex_mult_commute) +by (simp only: hcmod_mult_i hcomplex_mult_commute) (*---------------------------------------------------------------------------*) (* harg *) @@ -1105,31 +1098,29 @@ lemma harg: "harg (Abs_hcomplex(hcomplexrel `` {%n. X n})) = Abs_hypreal(hyprel `` {%n. arg (X n)})" - apply (simp add: harg_def) apply (rule_tac f = Abs_hypreal in arg_cong) -apply (auto, ultra) +apply (auto iff: hcomplexrel_iff, ultra) done lemma cos_harg_i_mult_zero_pos: - "0 < y ==> ( *f* cos) (harg(iii * hcomplex_of_hypreal y)) = 0" + "0 < y ==> ( *f* cos) (harg(HComplex 0 y)) = 0" 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) +apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult + hcomplex_add 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" + "y < 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0" 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) +apply (simp add: HComplex_def hcomplex_of_hypreal iii_def hcomplex_mult + hcomplex_add 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 (auto simp add: cos_harg_i_mult_zero_pos cos_harg_i_mult_zero_neg) -done + "y \ 0 ==> ( *f* cos) (harg(HComplex 0 y)) = 0" +by (auto simp add: linorder_neq_iff + cos_harg_i_mult_zero_pos cos_harg_i_mult_zero_neg) lemma hcomplex_of_hypreal_zero_iff [simp]: "(hcomplex_of_hypreal y = 0) = (y = 0)" @@ -1141,16 +1132,21 @@ subsection{*Polar Form for Nonstandard Complex Numbers*} lemma complex_split_polar2: - "\n. \r a. (z n) = complex_of_real r * - (complex_of_real(cos a) + ii * complex_of_real(sin a))" -apply (blast intro: complex_split_polar) + "\n. \r a. (z n) = complex_of_real r * (Complex (cos a) (sin a))" +by (blast intro: complex_split_polar) + +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, auto) done lemma hcomplex_split_polar: - "\r a. z = hcomplex_of_hypreal r * - (hcomplex_of_hypreal(( *f* cos) a) + iii * hcomplex_of_hypreal(( *f* sin) a))" + "\r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))" 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 (simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult HComplex_def) apply (cut_tac z = x in complex_split_polar2) apply (drule choice, safe)+ apply (rule_tac x = f in exI) @@ -1161,7 +1157,7 @@ "hcis (Abs_hypreal(hyprel `` {%n. X n})) = Abs_hcomplex(hcomplexrel `` {%n. cis (X n)})" apply (simp add: hcis_def) -apply (rule_tac f = Abs_hcomplex in arg_cong, auto, ultra) +apply (rule_tac f = Abs_hcomplex in arg_cong, auto iff: hcomplexrel_iff, ultra) done lemma hcis_eq: @@ -1178,35 +1174,38 @@ by (simp add: hrcis_def hcomplex_of_hypreal hcomplex_mult hcis rcis_def) lemma hrcis_Ex: "\r a. z = hrcis r a" -apply (simp add: hrcis_def hcis_eq) +apply (simp add: hrcis_def hcis_eq hcomplex_of_hypreal_mult_HComplex [symmetric]) apply (rule hcomplex_split_polar) done 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" -by (simp add: right_distrib hcomplex_of_hypreal_mult mult_ac) + "hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = + r * ( *f* cos) a" +by (simp add: hcomplex_of_hypreal_mult_HComplex) lemma hRe_hrcis [simp]: "hRe(hrcis r a) = r * ( *f* cos) a" by (simp add: hrcis_def hcis_eq) 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" -by (simp add: right_distrib hcomplex_of_hypreal_mult mult_ac) + "hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = + r * ( *f* sin) a" +by (simp add: hcomplex_of_hypreal_mult_HComplex) lemma hIm_hrcis [simp]: "hIm(hrcis r a) = r * ( *f* sin) a" by (simp add: hrcis_def hcis_eq) + +lemma hcmod_unit_one [simp]: + "hcmod (HComplex (( *f* cos) a) (( *f* sin) a)) = 1" +apply (rule eq_Abs_hypreal [of a]) +apply (simp add: HComplex_def iii_def starfun hcomplex_of_hypreal + hcomplex_mult hcmod hcomplex_add hypreal_one_def) +done + 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 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) + "hcmod (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = + abs r" +apply (simp only: hcmod_mult hcmod_unit_one, simp) done lemma hcmod_hrcis [simp]: "hcmod(hrcis r a) = abs r" @@ -1316,20 +1315,16 @@ done lemma cos_n_hRe_hcis_pow_n: "( *f* cos) (hypreal_of_nat n * a) = hRe(hcis a ^ n)" -apply (simp add: NSDeMoivre) -done +by (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 +by (simp add: NSDeMoivre) 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 +by (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 +by (simp add: NSDeMoivre_ext) lemma hexpi_add: "hexpi(a + b) = hexpi(a) * hexpi(b)" apply (simp add: hexpi_def) @@ -1545,27 +1540,11 @@ val hsgn_minus = thm"hsgn_minus"; val hsgn_eq = thm"hsgn_eq"; val lemma_hypreal_P_EX2 = thm"lemma_hypreal_P_EX2"; -val complex_split2 = thm"complex_split2"; -val hcomplex_split = thm"hcomplex_split"; -val hRe_hcomplex_i = thm"hRe_hcomplex_i"; -val hIm_hcomplex_i = thm"hIm_hcomplex_i"; val hcmod_i = thm"hcmod_i"; -val hcomplex_eq_hRe_eq = thm"hcomplex_eq_hRe_eq"; -val hcomplex_eq_hIm_eq = thm"hcomplex_eq_hIm_eq"; -val hcomplex_eq_cancel_iff = thm"hcomplex_eq_cancel_iff"; -val hcomplex_eq_cancel_iffA = thm"hcomplex_eq_cancel_iffA"; -val hcomplex_eq_cancel_iffB = thm"hcomplex_eq_cancel_iffB"; -val hcomplex_eq_cancel_iffC = thm"hcomplex_eq_cancel_iffC"; val hcomplex_eq_cancel_iff2 = thm"hcomplex_eq_cancel_iff2"; -val hcomplex_eq_cancel_iff2a = thm"hcomplex_eq_cancel_iff2a"; -val hcomplex_eq_cancel_iff3 = thm"hcomplex_eq_cancel_iff3"; -val hcomplex_eq_cancel_iff3a = thm"hcomplex_eq_cancel_iff3a"; -val hcomplex_split_hRe_zero = thm"hcomplex_split_hRe_zero"; -val hcomplex_split_hIm_zero = thm"hcomplex_split_hIm_zero"; val hRe_hsgn = thm"hRe_hsgn"; val hIm_hsgn = thm"hIm_hsgn"; val real_two_squares_add_zero_iff = thm"real_two_squares_add_zero_iff"; -val hcomplex_inverse_complex_split = thm"hcomplex_inverse_complex_split"; val hRe_mult_i_eq = thm"hRe_mult_i_eq"; val hIm_mult_i_eq = thm"hIm_mult_i_eq"; val hcmod_mult_i = thm"hcmod_mult_i"; diff -r 9fe787a90a48 -r f454b3004f8f src/HOL/Complex/NSComplexBin.ML --- a/src/HOL/Complex/NSComplexBin.ML Thu Feb 05 04:30:38 2004 +0100 +++ b/src/HOL/Complex/NSComplexBin.ML Thu Feb 05 10:45:28 2004 +0100 @@ -482,6 +482,7 @@ (*** Real and imaginary stuff ***) +(*Convert??? Goalw [hcomplex_number_of_def] "((number_of xa :: hcomplex) + iii * number_of ya = \ \ number_of xb + iii * number_of yb) = \ @@ -561,6 +562,7 @@ hcomplex_hypreal_number_of,hcomplex_of_hypreal_zero_iff])); qed "hcomplex_number_of_eq_cancel_iff3a"; Addsimps [hcomplex_number_of_eq_cancel_iff3a]; +*) Goalw [hcomplex_number_of_def] "hcnj (number_of v :: hcomplex) = number_of v"; by (rtac (hcomplex_hypreal_number_of RS ssubst) 1); diff -r 9fe787a90a48 -r f454b3004f8f src/HOL/Real/PReal.thy --- a/src/HOL/Real/PReal.thy Thu Feb 05 04:30:38 2004 +0100 +++ b/src/HOL/Real/PReal.thy Thu Feb 05 10:45:28 2004 +0100 @@ -386,17 +386,18 @@ proof (intro exI conjI) show "0 < x*y" by (simp add: mult_pos) show "x * y \ mult_set A B" - proof (auto simp add: mult_set_def) - fix u::rat and v::rat - assume "u \ A" and "v \ B" and "x*y = u*v" - moreover - with prems have "uv" - by (blast intro: preal_imp_pos [OF B] order_less_imp_le prems) - moreover - hence "u*v < x*y" by (blast intro: mult_strict_mono prems) - ultimately show False by force + proof - + { fix u::rat and v::rat + assume "u \ A" and "v \ B" and "x*y = u*v" + moreover + with prems have "uv" + by (blast intro: preal_imp_pos [OF B] order_less_imp_le prems) + moreover + hence "u*v < x*y" by (blast intro: mult_strict_mono prems) + ultimately have False by force} + thus ?thesis by (auto simp add: mult_set_def) qed qed qed @@ -646,14 +647,15 @@ proof (intro exI conjI) show "0 < inverse x" by simp show "inverse x \ inverse_set A" - proof (auto simp add: inverse_set_def) - fix y::rat - assume ygt: "inverse x < y" - have [simp]: "0 < y" by (simp add: order_less_trans [OF _ ygt]) - have iyless: "inverse y < x" - by (simp add: inverse_less_imp_less [of x] ygt) - show "inverse y \ A" - by (simp add: preal_downwards_closed [OF A x] iyless) + proof - + { fix y::rat + assume ygt: "inverse x < y" + have [simp]: "0 < y" by (simp add: order_less_trans [OF _ ygt]) + have iyless: "inverse y < x" + by (simp add: inverse_less_imp_less [of x] ygt) + have "inverse y \ A" + by (simp add: preal_downwards_closed [OF A x] iyless)} + thus ?thesis by (auto simp add: inverse_set_def) qed qed qed diff -r 9fe787a90a48 -r f454b3004f8f src/HOL/Ring_and_Field.thy --- a/src/HOL/Ring_and_Field.thy Thu Feb 05 04:30:38 2004 +0100 +++ b/src/HOL/Ring_and_Field.thy Thu Feb 05 10:45:28 2004 +0100 @@ -94,10 +94,10 @@ by (simp add: add_commute) lemma minus_minus [simp]: "- (- (a::'a::ring)) = a" - proof (rule add_left_cancel [of "-a", THEN iffD1]) - show "(-a + -(-a) = -a + a)" - by simp - qed +proof (rule add_left_cancel [of "-a", THEN iffD1]) + show "(-a + -(-a) = -a + a)" + by simp +qed lemma equals_zero_I: "a+b = 0 ==> -a = (b::'a::ring)" apply (rule right_minus_eq [THEN iffD1, symmetric]) @@ -120,15 +120,15 @@ by (simp add: diff_minus) lemma neg_equal_iff_equal [simp]: "(-a = -b) = (a = (b::'a::ring))" - proof - assume "- a = - b" - hence "- (- a) = - (- b)" - by simp - thus "a=b" by simp - next - assume "a=b" - thus "-a = -b" by simp - qed +proof + assume "- a = - b" + hence "- (- a) = - (- b)" + by simp + thus "a=b" by simp +next + assume "a=b" + thus "-a = -b" by simp +qed lemma neg_equal_0_iff_equal [simp]: "(-a = 0) = (a = (0::'a::ring))" by (subst neg_equal_iff_equal [symmetric], simp) @@ -139,16 +139,16 @@ text{*The next two equations can make the simplifier loop!*} lemma equation_minus_iff: "(a = - b) = (b = - (a::'a::ring))" - proof - +proof - have "(- (-a) = - b) = (- a = b)" by (rule neg_equal_iff_equal) thus ?thesis by (simp add: eq_commute) - qed +qed lemma minus_equation_iff: "(- a = b) = (- (b::'a::ring) = a)" - proof - +proof - have "(- a = - (-b)) = (a = -b)" by (rule neg_equal_iff_equal) thus ?thesis by (simp add: eq_commute) - qed +qed subsection {* Derived rules for multiplication *} @@ -263,13 +263,13 @@ lemma add_less_imp_less_left: assumes less: "c + a < c + b" shows "a < (b::'a::ordered_semiring)" - proof (rule ccontr) - assume "~ a < b" - hence "b \ a" by (simp add: linorder_not_less) - hence "c+b \ c+a" by (rule add_left_mono) - with this and less show False - by (simp add: linorder_not_less [symmetric]) - qed +proof (rule ccontr) + assume "~ a < b" + hence "b \ a" by (simp add: linorder_not_less) + hence "c+b \ c+a" by (rule add_left_mono) + with this and less show False + by (simp add: linorder_not_less [symmetric]) +qed lemma add_less_imp_less_right: "a + c < b + c ==> a < (b::'a::ordered_semiring)" @@ -306,7 +306,7 @@ lemma le_imp_neg_le: assumes "a \ (b::'a::ordered_ring)" shows "-b \ -a" - proof - +proof - have "-a+a \ -a+b" by (rule add_left_mono) hence "0 \ -a+b" @@ -315,18 +315,18 @@ by (rule add_right_mono) thus ?thesis by (simp add: add_assoc) - qed +qed lemma neg_le_iff_le [simp]: "(-b \ -a) = (a \ (b::'a::ordered_ring))" - proof - assume "- b \ - a" - hence "- (- a) \ - (- b)" - by (rule le_imp_neg_le) - thus "a\b" by simp - next - assume "a\b" - thus "-b \ -a" by (rule le_imp_neg_le) - qed +proof + assume "- b \ - a" + hence "- (- a) \ - (- b)" + by (rule le_imp_neg_le) + thus "a\b" by simp +next + assume "a\b" + thus "-b \ -a" by (rule le_imp_neg_le) +qed lemma neg_le_0_iff_le [simp]: "(-a \ 0) = (0 \ (a::'a::ordered_ring))" by (subst neg_le_iff_le [symmetric], simp) @@ -346,16 +346,16 @@ text{*The next several equations can make the simplifier loop!*} lemma less_minus_iff: "(a < - b) = (b < - (a::'a::ordered_ring))" - proof - +proof - have "(- (-a) < - b) = (b < - a)" by (rule neg_less_iff_less) thus ?thesis by simp - qed +qed lemma minus_less_iff: "(- a < b) = (- b < (a::'a::ordered_ring))" - proof - +proof - have "(- a < - (-b)) = (- b < a)" by (rule neg_less_iff_less) thus ?thesis by simp - qed +qed lemma le_minus_iff: "(a \ - b) = (b \ - (a::'a::ordered_ring))" apply (simp add: linorder_not_less [symmetric]) @@ -645,13 +645,13 @@ lemma mult_less_imp_less_left: assumes less: "c*a < c*b" and nonneg: "0 \ c" shows "a < (b::'a::ordered_semiring)" - proof (rule ccontr) - assume "~ a < b" - hence "b \ a" by (simp add: linorder_not_less) - hence "c*b \ c*a" by (rule mult_left_mono) - with this and less show False - by (simp add: linorder_not_less [symmetric]) - qed +proof (rule ccontr) + assume "~ a < b" + hence "b \ a" by (simp add: linorder_not_less) + hence "c*b \ c*a" by (rule mult_left_mono) + with this and less show False + by (simp add: linorder_not_less [symmetric]) +qed lemma mult_less_imp_less_right: "[|a*c < b*c; 0 \ c|] ==> a < (b::'a::ordered_semiring)" @@ -723,52 +723,50 @@ text{*Compared with @{text mult_eq_0_iff}, this version removes the requirement of an ordering.*} lemma field_mult_eq_0_iff [simp]: "(a*b = (0::'a::field)) = (a = 0 | b = 0)" - proof cases - assume "a=0" thus ?thesis by simp - next - assume anz [simp]: "a\0" - thus ?thesis - proof auto - assume "a * b = 0" - hence "inverse a * (a * b) = 0" by simp - thus "b = 0" by (simp (no_asm_use) add: mult_assoc [symmetric]) - qed - qed +proof cases + assume "a=0" thus ?thesis by simp +next + assume anz [simp]: "a\0" + { assume "a * b = 0" + hence "inverse a * (a * b) = 0" by simp + hence "b = 0" by (simp (no_asm_use) add: mult_assoc [symmetric])} + thus ?thesis by force +qed text{*Cancellation of equalities with a common factor*} lemma field_mult_cancel_right_lemma: assumes cnz: "c \ (0::'a::field)" and eq: "a*c = b*c" shows "a=b" - proof - +proof - have "(a * c) * inverse c = (b * c) * inverse c" by (simp add: eq) thus "a=b" by (simp add: mult_assoc cnz) - qed +qed lemma field_mult_cancel_right [simp]: "(a*c = b*c) = (c = (0::'a::field) | a=b)" - proof cases - assume "c=0" thus ?thesis by simp - next - assume "c\0" - thus ?thesis by (force dest: field_mult_cancel_right_lemma) - qed +proof cases + assume "c=0" thus ?thesis by simp +next + assume "c\0" + thus ?thesis by (force dest: field_mult_cancel_right_lemma) +qed lemma field_mult_cancel_left [simp]: "(c*a = c*b) = (c = (0::'a::field) | a=b)" by (simp add: mult_commute [of c] field_mult_cancel_right) lemma nonzero_imp_inverse_nonzero: "a \ 0 ==> inverse a \ (0::'a::field)" - proof +proof assume ianz: "inverse a = 0" assume "a \ 0" hence "1 = a * inverse a" by simp also have "... = 0" by (simp add: ianz) finally have "1 = (0::'a::field)" . thus False by (simp add: eq_commute) - qed +qed subsection{*Basic Properties of @{term inverse}*} @@ -790,35 +788,35 @@ lemma nonzero_inverse_minus_eq: assumes [simp]: "a\0" shows "inverse(-a) = -inverse(a::'a::field)" - proof - - have "-a * inverse (- a) = -a * - inverse a" - by simp - thus ?thesis - by (simp only: field_mult_cancel_left, simp) - qed +proof - + have "-a * inverse (- a) = -a * - inverse a" + by simp + thus ?thesis + by (simp only: field_mult_cancel_left, simp) +qed lemma inverse_minus_eq [simp]: - "inverse(-a) = -inverse(a::'a::{field,division_by_zero})"; - proof cases - assume "a=0" thus ?thesis by (simp add: inverse_zero) - next - assume "a\0" - thus ?thesis by (simp add: nonzero_inverse_minus_eq) - qed + "inverse(-a) = -inverse(a::'a::{field,division_by_zero})"; +proof cases + assume "a=0" thus ?thesis by (simp add: inverse_zero) +next + assume "a\0" + thus ?thesis by (simp add: nonzero_inverse_minus_eq) +qed lemma nonzero_inverse_eq_imp_eq: assumes inveq: "inverse a = inverse b" and anz: "a \ 0" and bnz: "b \ 0" shows "a = (b::'a::field)" - proof - +proof - have "a * inverse b = a * inverse a" by (simp add: inveq) hence "(a * inverse b) * b = (a * inverse a) * b" by simp thus "a = b" by (simp add: mult_assoc anz bnz) - qed +qed lemma inverse_eq_imp_eq: "inverse a = inverse b ==> a = (b::'a::{field,division_by_zero})"