# HG changeset patch # User paulson # Date 1072180485 -3600 # Node ID 7dbd3988b15b68d971904baee9525441305c1b01 # Parent 85125b18d38a5ecb196cf3eda8638ab9d46fb87e type hcomplex is now in class field diff -r 85125b18d38a -r 7dbd3988b15b src/HOL/Complex/CLim.ML --- a/src/HOL/Complex/CLim.ML Tue Dec 23 12:54:15 2003 +0100 +++ b/src/HOL/Complex/CLim.ML Tue Dec 23 12:54:45 2003 +0100 @@ -826,8 +826,8 @@ by (simp_tac (simpset() addsimps [hcomplex_add_divide_distrib]) 1); by (REPEAT(dtac (bex_CInfinitesimal_iff2 RS iffD2) 1)); by (auto_tac (claset(), - simpset() delsimps [hcomplex_times_divide1_eq] - addsimps [hcomplex_times_divide1_eq RS sym])); + simpset() delsimps [times_divide_eq_right] + addsimps [times_divide_eq_right RS sym])); by (rewtac hcomplex_diff_def); by (dres_inst_tac [("D","Db")] lemma_nscderiv2 1); by (dtac (capprox_minus_iff RS iffD2 RS (bex_CInfinitesimal_iff2 RS iffD2)) 4); @@ -1050,14 +1050,6 @@ by Auto_tac; qed "CInfinitesimal_add_not_zero"; -(*** -Goal "[|(x::hcomplex) ~= 0; y ~= 0 |] \ -\ ==> inverse(x) + inverse(y) = (x + y)*inverse(x*y)"; -by (asm_full_simp_tac (simpset() addsimps [hcomplex_inverse_distrib, - hcomplex_add_mult_distrib,hcomplex_mult_assoc RS sym]) 1); -qed "hcomplex_inverse_add"; -***) - (*Can't get rid of x ~= 0 because it isn't continuous at zero*) Goalw [nscderiv_def] @@ -1071,9 +1063,10 @@ hcomplex_minus_mult_eq2 RS sym])); by (asm_simp_tac (simpset() addsimps [hcomplex_inverse_add, - hcomplex_inverse_distrib RS sym, hcomplex_minus_inverse RS sym] + inverse_mult_distrib RS sym, hcomplex_minus_inverse RS sym] @ hcomplex_add_ac @ hcomplex_mult_ac - delsimps [hcomplex_minus_mult_eq1 RS sym, + delsimps [thm"Ring_and_Field.inverse_minus_eq", + inverse_mult_distrib, hcomplex_minus_mult_eq1 RS sym, hcomplex_minus_mult_eq2 RS sym] ) 1); by (asm_simp_tac (simpset() addsimps [hcomplex_mult_assoc RS sym, hcomplex_add_mult_distrib2] diff -r 85125b18d38a -r 7dbd3988b15b src/HOL/Complex/NSCA.ML --- a/src/HOL/Complex/NSCA.ML Tue Dec 23 12:54:15 2003 +0100 +++ b/src/HOL/Complex/NSCA.ML Tue Dec 23 12:54:45 2003 +0100 @@ -1311,7 +1311,7 @@ by (auto_tac (claset(), simpset() addsimps [stc_mult RS sym, stc_not_CInfinitesimal, CFinite_inverse])); -by (stac hcomplex_mult_inv_right 1); +by (stac right_inverse 1); by Auto_tac; qed "stc_inverse"; diff -r 85125b18d38a -r 7dbd3988b15b src/HOL/Complex/NSComplex.thy --- a/src/HOL/Complex/NSComplex.thy Tue Dec 23 12:54:15 2003 +0100 +++ b/src/HOL/Complex/NSComplex.thy Tue Dec 23 12:54:45 2003 +0100 @@ -6,6 +6,12 @@ theory NSComplex = NSInduct: +(* Move to one of the hyperreal theories *) +lemma hypreal_of_nat: "hypreal_of_nat m = Abs_hypreal(hyprel `` {%n. real m})" +apply (induct_tac "m") +apply (auto simp add: hypreal_zero_def hypreal_of_nat_Suc hypreal_zero_num hypreal_one_num hypreal_add real_of_nat_Suc) +done + constdefs hcomplexrel :: "((nat=>complex)*(nat=>complex)) set" "hcomplexrel == {p. EX X Y. p = ((X::nat=>complex),Y) & @@ -358,144 +364,12 @@ apply (auto , ultra) done -lemma hcomplex_minus_minus: "- (- z) = (z::hcomplex)" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (simp (no_asm_simp) add: hcomplex_minus) -done -declare hcomplex_minus_minus [simp] - -lemma inj_hcomplex_minus: "inj(%z::hcomplex. -z)" -apply (rule inj_onI) -apply (drule_tac f = "uminus" in arg_cong) -apply simp -done - -lemma hcomplex_minus_zero: "- 0 = (0::hcomplex)" -apply (unfold hcomplex_zero_def) -apply (simp (no_asm) add: hcomplex_minus) -done -declare hcomplex_minus_zero [simp] - -lemma hcomplex_minus_zero_iff: "(-x = 0) = (x = (0::hcomplex))" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (auto simp add: hcomplex_zero_def hcomplex_minus) -done -declare hcomplex_minus_zero_iff [simp] - -lemma hcomplex_minus_zero_iff2: "(0 = -x) = (x = (0::hcomplex))" -apply (auto dest: sym) -done -declare hcomplex_minus_zero_iff2 [simp] - -lemma hcomplex_minus_not_zero_iff: "(-x ~= 0) = (x ~= (0::hcomplex))" -apply auto -done - -lemma hcomplex_add_minus_right: "z + - z = (0::hcomplex)" -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hcomplex_add hcomplex_minus hcomplex_zero_def) -done -declare hcomplex_add_minus_right [simp] - 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) done declare hcomplex_add_minus_left [simp] -lemma hcomplex_add_minus_cancel: "z + (- z + w) = (w::hcomplex)" -apply (simp (no_asm) add: hcomplex_add_assoc [symmetric]) -done - -lemma hcomplex_minus_add_cancel: "(-z) + (z + w) = (w::hcomplex)" -apply (simp (no_asm) add: hcomplex_add_assoc [symmetric]) -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) -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) -done - -lemma hcomplex_add_minus_eq_minus: - "x + y = (0::hcomplex) ==> x = -y" -apply (unfold hcomplex_zero_def) -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (rule_tac z = "y" in eq_Abs_hcomplex) -apply (auto simp add: hcomplex_add hcomplex_minus) -apply ultra -done - -lemma hcomplex_minus_add_distrib: "-(x + y) = -x + -(y::hcomplex)" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (rule_tac z = "y" in eq_Abs_hcomplex) -apply (auto simp add: hcomplex_add hcomplex_minus) -done -declare hcomplex_minus_add_distrib [simp] - -lemma hcomplex_add_left_cancel: "((x::hcomplex) + y = x + z) = (y = z)" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (rule_tac z = "y" in eq_Abs_hcomplex) -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hcomplex_add) -done -declare hcomplex_add_left_cancel [iff] - -lemma hcomplex_add_right_cancel: "(y + (x::hcomplex)= z + x) = (y = z)" -apply (simp (no_asm) add: hcomplex_add_commute) -done -declare hcomplex_add_right_cancel [iff] - -lemma hcomplex_eq_minus_iff: "((x::hcomplex) = y) = ((0::hcomplex) = x + - y)" -apply (safe) -apply (rule_tac [2] x1 = "-y" in hcomplex_add_right_cancel [THEN iffD1]) -apply auto -done - -lemma hcomplex_eq_minus_iff2: "((x::hcomplex) = y) = (x + - y = (0::hcomplex))" -apply (safe) -apply (rule_tac [2] x1 = "-y" in hcomplex_add_right_cancel [THEN iffD1]) -apply auto -done - -subsection{*Subraction for Nonstandard Complex Numbers*} - -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 - -lemma hcomplex_diff_zero: "(z::hcomplex) - z = (0::hcomplex)" -apply (unfold hcomplex_diff_def) -apply (simp (no_asm)) -done -declare hcomplex_diff_zero [simp] - -lemma hcomplex_diff_0: "(0::hcomplex) - x = -x" -apply (simp (no_asm) add: hcomplex_diff_def) -done - -lemma hcomplex_diff_0_right: "x - (0::hcomplex) = x" -apply (simp (no_asm) add: hcomplex_diff_def) -done - -lemma hcomplex_diff_self: "x - x = (0::hcomplex)" -apply (simp (no_asm) add: hcomplex_diff_def) -done - -declare hcomplex_diff_0 [simp] hcomplex_diff_0_right [simp] hcomplex_diff_self [simp] - -lemma hcomplex_diff_eq_eq: "((x::hcomplex) - y = z) = (x = z + y)" -apply (auto simp add: hcomplex_diff_def hcomplex_add_assoc) -done - subsection{*Multiplication for Nonstandard Complex Numbers*} lemma hcomplex_mult: @@ -520,16 +394,6 @@ apply (auto simp add: hcomplex_mult complex_mult_assoc) done -lemma hcomplex_mult_left_commute: "(x::hcomplex) * (y * z) = y * (x * z)" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (rule_tac z = "y" in eq_Abs_hcomplex) -apply (rule_tac z = "z" in eq_Abs_hcomplex) -apply (auto simp add: hcomplex_mult complex_mult_left_commute) -done - -lemmas hcomplex_mult_ac = hcomplex_mult_assoc hcomplex_mult_commute - hcomplex_mult_left_commute - lemma hcomplex_mult_one_left: "(1::hcomplex) * z = z" apply (unfold hcomplex_one_def) apply (rule_tac z = "z" in eq_Abs_hcomplex) @@ -537,11 +401,6 @@ done declare hcomplex_mult_one_left [simp] -lemma hcomplex_mult_one_right: "z * (1::hcomplex) = z" -apply (simp (no_asm) add: hcomplex_mult_commute) -done -declare hcomplex_mult_one_right [simp] - lemma hcomplex_mult_zero_left: "(0::hcomplex) * z = 0" apply (unfold hcomplex_zero_def) apply (rule_tac z = "z" in eq_Abs_hcomplex) @@ -549,45 +408,6 @@ done declare hcomplex_mult_zero_left [simp] -lemma hcomplex_mult_zero_right: "z * (0::hcomplex) = 0" -apply (simp (no_asm) add: hcomplex_mult_commute) -done -declare hcomplex_mult_zero_right [simp] - -lemma hcomplex_minus_mult_eq1: "-(x * y) = -x * (y::hcomplex)" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (rule_tac z = "y" in eq_Abs_hcomplex) -apply (auto simp add: hcomplex_mult hcomplex_minus) -done - -lemma hcomplex_minus_mult_eq2: "-(x * y) = x * -(y::hcomplex)" -apply (rule_tac z = "x" in eq_Abs_hcomplex) -apply (rule_tac z = "y" in eq_Abs_hcomplex) -apply (auto simp add: hcomplex_mult hcomplex_minus) -done - -declare hcomplex_minus_mult_eq1 [symmetric, simp] hcomplex_minus_mult_eq2 [symmetric, simp] - -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_right: "(z::hcomplex) * - 1 = -z" -apply (subst hcomplex_mult_commute) -apply (simp (no_asm)) -done -declare hcomplex_mult_minus_one_right [simp] - -lemma hcomplex_minus_mult_cancel: "-x * -y = x * (y::hcomplex)" -apply auto -done -declare hcomplex_minus_mult_cancel [simp] - -lemma hcomplex_minus_mult_commute: "-x * y = x * -(y::hcomplex)" -apply auto -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) @@ -595,12 +415,6 @@ apply (auto simp add: hcomplex_mult hcomplex_add complex_add_mult_distrib) done -lemma hcomplex_add_mult_distrib2: "(w::hcomplex) * (z1 + z2) = (w * z1) + (w * z2)" -apply (rule_tac z1 = "z1 + z2" in hcomplex_mult_commute [THEN ssubst]) -apply (simp (no_asm) add: hcomplex_add_mult_distrib) -apply (simp (no_asm) add: hcomplex_mult_commute) -done - lemma hcomplex_zero_not_eq_one: "(0::hcomplex) ~= (1::hcomplex)" apply (unfold hcomplex_zero_def hcomplex_one_def) apply auto @@ -619,15 +433,6 @@ apply (auto , ultra) done -lemma HCOMPLEX_INVERSE_ZERO: "inverse (0::hcomplex) = 0" -apply (unfold hcomplex_zero_def) -apply (auto simp add: hcomplex_inverse) -done - -lemma HCOMPLEX_DIVISION_BY_ZERO: "a / (0::hcomplex) = 0" -apply (simp (no_asm) add: hcomplex_divide_def HCOMPLEX_INVERSE_ZERO) -done - lemma hcomplex_mult_inv_left: "z ~= (0::hcomplex) ==> inverse(z) * z = (1::hcomplex)" apply (unfold hcomplex_zero_def hcomplex_one_def) @@ -640,105 +445,173 @@ done declare hcomplex_mult_inv_left [simp] -lemma hcomplex_mult_inv_right: "z ~= (0::hcomplex) ==> z * inverse(z) = (1::hcomplex)" -apply (auto intro: hcomplex_mult_commute [THEN subst]) +subsection {* The Field of Nonstandard Complex Numbers *} + +instance hcomplex :: field +proof + fix z u v w :: hcomplex + show "(u + v) + w = u + (v + w)" + by (simp add: hcomplex_add_assoc) + show "z + w = w + z" + by (simp add: hcomplex_add_commute) + show "0 + z = z" + by (simp) + show "-z + z = 0" + by (simp) + show "z - w = z + -w" + by (simp add: hcomplex_diff_def) + show "(u * v) * w = u * (v * w)" + by (simp add: hcomplex_mult_assoc) + show "z * w = w * z" + by (simp add: hcomplex_mult_commute) + show "1 * z = z" + by (simp) + show "0 \ (1::hcomplex)" + by (rule hcomplex_zero_not_eq_one) + show "(u + v) * w = u * w + v * w" + by (simp add: hcomplex_add_mult_distrib) + assume neq: "w \ 0" + thus "z / w = z * inverse w" + by (simp add: hcomplex_divide_def) + show "inverse w * w = 1" + by (rule hcomplex_mult_inv_left) +qed + +lemma HCOMPLEX_INVERSE_ZERO: "inverse (0::hcomplex) = 0" +apply (unfold hcomplex_zero_def) +apply (auto simp add: hcomplex_inverse) done -declare hcomplex_mult_inv_right [simp] + +lemma HCOMPLEX_DIVISION_BY_ZERO: "a / (0::hcomplex) = 0" +apply (simp (no_asm) add: hcomplex_divide_def HCOMPLEX_INVERSE_ZERO) +done + +instance hcomplex :: division_by_zero +proof + fix x :: hcomplex + show "inverse 0 = (0::hcomplex)" by (rule HCOMPLEX_INVERSE_ZERO) + show "x/0 = 0" by (rule HCOMPLEX_DIVISION_BY_ZERO) +qed lemma hcomplex_mult_left_cancel: "(c::hcomplex) ~= (0::hcomplex) ==> (c*a=c*b) = (a=b)" -apply auto -apply (drule_tac f = "%x. x*inverse c" in arg_cong) -apply (simp add: hcomplex_mult_ac) +by (simp add: field_mult_cancel_left) + +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) +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) +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]) +done + +lemma hcomplex_minus_add_distrib: "-(x + y) = -x + -(y::hcomplex)" +apply (rule Ring_and_Field.minus_add_distrib) +done + +lemma hcomplex_add_left_cancel: "((x::hcomplex) + y = x + z) = (y = z)" +apply (rule Ring_and_Field.add_left_cancel) +done +declare hcomplex_add_left_cancel [iff] + +lemma hcomplex_add_right_cancel: "(y + (x::hcomplex)= z + x) = (y = z)" +apply (rule Ring_and_Field.add_right_cancel) +done +declare hcomplex_add_right_cancel [iff] + +subsection{*More Multiplication Laws*} + +lemma hcomplex_mult_left_commute: "(x::hcomplex) * (y * z) = y * (x * z)" +apply (rule Ring_and_Field.mult_left_commute) +done + +lemmas hcomplex_mult_ac = hcomplex_mult_assoc hcomplex_mult_commute + hcomplex_mult_left_commute + +lemma hcomplex_mult_one_right: "z * (1::hcomplex) = z" +apply (rule Ring_and_Field.mult_1_right) +done + +lemma hcomplex_mult_zero_right: "z * (0::hcomplex) = 0" +apply (rule Ring_and_Field.mult_right_zero) +done + +lemma hcomplex_minus_mult_eq1: "-(x * y) = -x * (y::hcomplex)" +apply (rule Ring_and_Field.minus_mult_left) +done + +declare hcomplex_minus_mult_eq1 [symmetric, simp] + +lemma hcomplex_minus_mult_eq2: "-(x * y) = x * -(y::hcomplex)" +apply (rule Ring_and_Field.minus_mult_right) +done + +declare hcomplex_minus_mult_eq2 [symmetric, simp] + +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_right: "(z::hcomplex) * - 1 = -z" +apply (subst hcomplex_mult_commute) +apply (simp (no_asm)) +done +declare hcomplex_mult_minus_one_right [simp] + +lemma hcomplex_add_mult_distrib2: "(w::hcomplex) * (z1 + z2) = (w * z1) + (w * z2)" +apply (rule Ring_and_Field.right_distrib) done lemma hcomplex_mult_right_cancel: "(c::hcomplex) ~= (0::hcomplex) ==> (a*c=b*c) = (a=b)" -apply (safe) -apply (drule_tac f = "%x. x*inverse c" in arg_cong) -apply (simp add: hcomplex_mult_ac) +apply (simp add: Ring_and_Field.field_mult_cancel_right); done lemma hcomplex_inverse_not_zero: "z ~= (0::hcomplex) ==> inverse(z) ~= 0" -apply (safe) -apply (frule hcomplex_mult_right_cancel [THEN iffD2]) -apply (erule_tac [2] V = "inverse z = 0" in thin_rl) -apply (assumption , auto) +apply (simp add: ); done -declare hcomplex_inverse_not_zero [simp] lemma hcomplex_mult_not_zero: "[| x ~= (0::hcomplex); y ~= 0 |] ==> x * y ~= 0" -apply (safe) -apply (drule_tac f = "%z. inverse x*z" in arg_cong) -apply (simp add: hcomplex_mult_assoc [symmetric]) +apply (simp add: Ring_and_Field.field_mult_eq_0_iff); done lemmas hcomplex_mult_not_zeroE = hcomplex_mult_not_zero [THEN notE, standard] -lemma hcomplex_inverse_inverse: "inverse(inverse x) = (x::hcomplex)" -apply (case_tac "x = 0", simp add: HCOMPLEX_INVERSE_ZERO) -apply (rule_tac c1 = "inverse x" in hcomplex_mult_right_cancel [THEN iffD1]) -apply (erule hcomplex_inverse_not_zero) -apply (auto dest: hcomplex_inverse_not_zero) -done -declare hcomplex_inverse_inverse [simp] - -lemma hcomplex_inverse_one: "inverse((1::hcomplex)) = 1" -apply (unfold hcomplex_one_def) -apply (simp (no_asm) add: hcomplex_inverse) -done -declare hcomplex_inverse_one [simp] - lemma hcomplex_minus_inverse: "inverse(-x) = -inverse(x::hcomplex)" -apply (case_tac "x = 0", simp add: HCOMPLEX_INVERSE_ZERO) -apply (rule_tac c1 = "-x" in hcomplex_mult_right_cancel [THEN iffD1]) -apply (force ); -apply (subst hcomplex_mult_inv_left) -apply auto -done - -lemma hcomplex_inverse_distrib: "inverse(x*y) = inverse x * inverse (y::hcomplex)" -apply (case_tac "x = 0", simp add: HCOMPLEX_INVERSE_ZERO) -apply (case_tac "y = 0", simp add: HCOMPLEX_INVERSE_ZERO) -apply (rule_tac c1 = "x*y" in hcomplex_mult_left_cancel [THEN iffD1]) -apply (auto simp add: hcomplex_mult_not_zero hcomplex_mult_ac) -apply (auto simp add: hcomplex_mult_not_zero hcomplex_mult_assoc [symmetric]) +apply (rule Ring_and_Field.inverse_minus_eq) done -subsection{*Division*} -lemma hcomplex_times_divide1_eq: "(x::hcomplex) * (y/z) = (x*y)/z" -apply (simp (no_asm) add: hcomplex_divide_def hcomplex_mult_assoc) -done +subsection{*Subraction and Division*} -lemma hcomplex_times_divide2_eq: "(y/z) * (x::hcomplex) = (y*x)/z" -apply (simp (no_asm) add: hcomplex_divide_def hcomplex_mult_ac) -done - -declare hcomplex_times_divide1_eq [simp] hcomplex_times_divide2_eq [simp] - -lemma hcomplex_divide_divide1_eq: "(x::hcomplex) / (y/z) = (x*z)/y" -apply (simp (no_asm) add: hcomplex_divide_def hcomplex_inverse_distrib hcomplex_mult_ac) +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 -lemma hcomplex_divide_divide2_eq: "((x::hcomplex) / y) / z = x/(y*z)" -apply (simp (no_asm) add: hcomplex_divide_def hcomplex_inverse_distrib hcomplex_mult_assoc) +lemma hcomplex_diff_eq_eq: "((x::hcomplex) - y = z) = (x = z + y)" +apply (rule Ring_and_Field.diff_eq_eq) done -declare hcomplex_divide_divide1_eq [simp] hcomplex_divide_divide2_eq [simp] - -(** As with multiplication, pull minus signs OUT of the / operator **) - -lemma hcomplex_minus_divide_eq: "(-x) / (y::hcomplex) = - (x/y)" -apply (simp (no_asm) add: hcomplex_divide_def) -done -declare hcomplex_minus_divide_eq [simp] - -lemma hcomplex_divide_minus_eq: "(x / -(y::hcomplex)) = - (x/y)" -apply (simp (no_asm) add: hcomplex_divide_def hcomplex_minus_inverse) -done -declare hcomplex_divide_minus_eq [simp] - lemma hcomplex_add_divide_distrib: "(x+y)/(z::hcomplex) = x/z + y/z" -apply (simp (no_asm) add: hcomplex_divide_def hcomplex_add_mult_distrib) +apply (rule Ring_and_Field.add_divide_distrib) done @@ -840,9 +713,8 @@ done declare hcomplex_of_hypreal_epsilon_not_zero [simp] -(*---------------------------------------------------------------------------*) -(* Modulus (absolute value) of nonstandard complex number *) -(*---------------------------------------------------------------------------*) + +subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*} lemma hcmod: "hcmod (Abs_hcomplex(hcomplexrel `` {%n. X n})) = @@ -882,8 +754,7 @@ lemma hcnj: "hcnj (Abs_hcomplex(hcomplexrel `` {%n. X n})) = - Abs_hcomplex(hcomplexrel `` {%n. cnj(X n)})" - + Abs_hcomplex(hcomplexrel `` {%n. cnj(X n)})" apply (unfold hcnj_def) apply (rule_tac f = "Abs_hcomplex" in arg_cong) apply (auto , ultra) @@ -1252,7 +1123,7 @@ lemma hcomplex_inverse_divide: "inverse(x/y) = y/(x::hcomplex)" apply (unfold hcomplex_divide_def) -apply (auto simp add: hcomplex_inverse_distrib hcomplex_mult_commute) +apply (auto simp add: inverse_mult_distrib hcomplex_mult_commute) done declare hcomplex_inverse_divide [simp] @@ -1720,7 +1591,6 @@ (*---------------------------------------------------------------------------*) lemma hcis_hrcis_eq: "hcis a = hrcis 1 a" - apply (unfold hrcis_def) apply (simp (no_asm)) done @@ -1775,12 +1645,6 @@ done declare hcomplex_i_mult_minus2 [simp] -(* Move to one of the hyperreal theories *) -lemma hypreal_of_nat: "hypreal_of_nat m = Abs_hypreal(hyprel `` {%n. real m})" -apply (induct_tac "m") -apply (auto simp add: hypreal_zero_def hypreal_of_nat_Suc hypreal_zero_num hypreal_one_num hypreal_add real_of_nat_Suc) -done - 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) @@ -1991,29 +1855,15 @@ val hIm_add = thm"hIm_add"; val hcomplex_minus_congruent = thm"hcomplex_minus_congruent"; val hcomplex_minus = thm"hcomplex_minus"; -val hcomplex_minus_minus = thm"hcomplex_minus_minus"; val inj_hcomplex_minus = thm"inj_hcomplex_minus"; -val hcomplex_minus_zero = thm"hcomplex_minus_zero"; -val hcomplex_minus_zero_iff = thm"hcomplex_minus_zero_iff"; -val hcomplex_minus_zero_iff2 = thm"hcomplex_minus_zero_iff2"; -val hcomplex_minus_not_zero_iff = thm"hcomplex_minus_not_zero_iff"; -val hcomplex_add_minus_right = thm"hcomplex_add_minus_right"; val hcomplex_add_minus_left = thm"hcomplex_add_minus_left"; -val hcomplex_add_minus_cancel = thm"hcomplex_add_minus_cancel"; -val hcomplex_minus_add_cancel = thm"hcomplex_minus_add_cancel"; val hRe_minus = thm"hRe_minus"; val hIm_minus = thm"hIm_minus"; val hcomplex_add_minus_eq_minus = thm"hcomplex_add_minus_eq_minus"; val hcomplex_minus_add_distrib = thm"hcomplex_minus_add_distrib"; val hcomplex_add_left_cancel = thm"hcomplex_add_left_cancel"; val hcomplex_add_right_cancel = thm"hcomplex_add_right_cancel"; -val hcomplex_eq_minus_iff = thm"hcomplex_eq_minus_iff"; -val hcomplex_eq_minus_iff2 = thm"hcomplex_eq_minus_iff2"; val hcomplex_diff = thm"hcomplex_diff"; -val hcomplex_diff_zero = thm"hcomplex_diff_zero"; -val hcomplex_diff_0 = thm"hcomplex_diff_0"; -val hcomplex_diff_0_right = thm"hcomplex_diff_0_right"; -val hcomplex_diff_self = thm"hcomplex_diff_self"; val hcomplex_diff_eq_eq = thm"hcomplex_diff_eq_eq"; val hcomplex_mult = thm"hcomplex_mult"; val hcomplex_mult_commute = thm"hcomplex_mult_commute"; @@ -2027,8 +1877,6 @@ val hcomplex_minus_mult_eq2 = thm"hcomplex_minus_mult_eq2"; val hcomplex_mult_minus_one = thm"hcomplex_mult_minus_one"; val hcomplex_mult_minus_one_right = thm"hcomplex_mult_minus_one_right"; -val hcomplex_minus_mult_cancel = thm"hcomplex_minus_mult_cancel"; -val hcomplex_minus_mult_commute = thm"hcomplex_minus_mult_commute"; val hcomplex_add_mult_distrib = thm"hcomplex_add_mult_distrib"; val hcomplex_add_mult_distrib2 = thm"hcomplex_add_mult_distrib2"; val hcomplex_zero_not_eq_one = thm"hcomplex_zero_not_eq_one"; @@ -2036,22 +1884,12 @@ 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_inv_right = thm"hcomplex_mult_inv_right"; val hcomplex_mult_left_cancel = thm"hcomplex_mult_left_cancel"; val hcomplex_mult_right_cancel = thm"hcomplex_mult_right_cancel"; val hcomplex_inverse_not_zero = thm"hcomplex_inverse_not_zero"; val hcomplex_mult_not_zero = thm"hcomplex_mult_not_zero"; val hcomplex_mult_not_zeroE = thm"hcomplex_mult_not_zeroE"; -val hcomplex_inverse_inverse = thm"hcomplex_inverse_inverse"; -val hcomplex_inverse_one = thm"hcomplex_inverse_one"; val hcomplex_minus_inverse = thm"hcomplex_minus_inverse"; -val hcomplex_inverse_distrib = thm"hcomplex_inverse_distrib"; -val hcomplex_times_divide1_eq = thm"hcomplex_times_divide1_eq"; -val hcomplex_times_divide2_eq = thm"hcomplex_times_divide2_eq"; -val hcomplex_divide_divide1_eq = thm"hcomplex_divide_divide1_eq"; -val hcomplex_divide_divide2_eq = thm"hcomplex_divide_divide2_eq"; -val hcomplex_minus_divide_eq = thm"hcomplex_minus_divide_eq"; -val hcomplex_divide_minus_eq = thm"hcomplex_divide_minus_eq"; 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"; diff -r 85125b18d38a -r 7dbd3988b15b src/HOL/Complex/NSComplexArith0.ML --- a/src/HOL/Complex/NSComplexArith0.ML Tue Dec 23 12:54:15 2003 +0100 +++ b/src/HOL/Complex/NSComplexArith0.ML Tue Dec 23 12:54:45 2003 +0100 @@ -29,9 +29,7 @@ qed "hcomplex_inverse_eq_divide"; Goal "(inverse(x::hcomplex) = 0) = (x = 0)"; -by (auto_tac (claset(), - simpset() addsimps [HCOMPLEX_INVERSE_ZERO])); -by (blast_tac (claset() addIs [ccontr] addDs [hcomplex_inverse_not_zero]) 1); +by (Simp_tac 1); qed "hcomplex_inverse_zero_iff"; Addsimps [hcomplex_inverse_zero_iff]; @@ -60,7 +58,7 @@ Goal "!!k::hcomplex. k~=0 ==> (k*m) / (k*n) = (m/n)"; by (asm_simp_tac - (simpset() addsimps [hcomplex_divide_def, hcomplex_inverse_distrib]) 1); + (simpset() addsimps [hcomplex_divide_def, inverse_mult_distrib]) 1); by (subgoal_tac "k * m * (inverse k * inverse n) = \ \ (k * inverse k) * (m * inverse n)" 1); by (Asm_full_simp_tac 1); @@ -295,7 +293,6 @@ Goal "(-b = -a) = (b = (a::hcomplex))"; by Auto_tac; -by (etac ( inj_hcomplex_minus RS injD) 1); qed "hcomplex_minus_eq_cancel"; Addsimps [hcomplex_minus_eq_cancel]; @@ -324,7 +321,7 @@ Goal "[|(x::hcomplex) ~= 0; y ~= 0 |] \ \ ==> inverse(x) + inverse(y) = (x + y)*inverse(x*y)"; -by (asm_full_simp_tac (simpset() addsimps [hcomplex_inverse_distrib, +by (asm_full_simp_tac (simpset() addsimps [inverse_mult_distrib, hcomplex_add_mult_distrib,hcomplex_mult_assoc RS sym]) 1); qed "hcomplex_inverse_add"; diff -r 85125b18d38a -r 7dbd3988b15b src/HOL/Complex/NSComplexBin.ML --- a/src/HOL/Complex/NSComplexBin.ML Tue Dec 23 12:54:15 2003 +0100 +++ b/src/HOL/Complex/NSComplexBin.ML Tue Dec 23 12:54:45 2003 +0100 @@ -310,7 +310,7 @@ (*To let us treat subtraction as addition*) val diff_simps = [hcomplex_diff_def, hcomplex_minus_add_distrib, - hcomplex_minus_minus]; + minus_minus]; (*push the unary minus down: - x * y = x * - y *) val hcomplex_minus_mult_eq_1_to_2 = @@ -319,7 +319,7 @@ (*to extract again any uncancelled minuses*) val hcomplex_minus_from_mult_simps = - [hcomplex_minus_minus, hcomplex_minus_mult_eq1 RS sym, + [minus_minus, hcomplex_minus_mult_eq1 RS sym, hcomplex_minus_mult_eq2 RS sym]; (*combine unary minus with numeric literals, however nested within a product*)