# HG changeset patch # User paulson # Date 1072187147 -3600 # Node ID fb7a114826be4ffc612b3755b1a8604d85ce05ad # Parent 255190be18c01085a1c44d8579e3b9c087368303 tidying up hcomplex arithmetic diff -r 255190be18c0 -r fb7a114826be src/HOL/Complex/CLim.ML --- a/src/HOL/Complex/CLim.ML Tue Dec 23 14:45:23 2003 +0100 +++ b/src/HOL/Complex/CLim.ML Tue Dec 23 14:45:47 2003 +0100 @@ -468,12 +468,12 @@ by Auto_tac; by (dres_inst_tac [("x","hcomplex_of_complex a + x")] spec 1); by (dres_inst_tac [("x","- hcomplex_of_complex a + x")] spec 2); -by (Step_tac 1); +by Safe_tac; by (Asm_full_simp_tac 1); by (rtac ((mem_cinfmal_iff RS iffD2) RS (CInfinitesimal_add_capprox_self RS capprox_sym)) 1); by (rtac (capprox_minus_iff2 RS iffD1) 4); -by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_commute]) 3); +by (asm_full_simp_tac (simpset() addsimps compare_rls@[hcomplex_add_commute]) 3); by (res_inst_tac [("z","x")] eq_Abs_hcomplex 2); by (res_inst_tac [("z","x")] eq_Abs_hcomplex 4); by (auto_tac (claset(), @@ -747,7 +747,8 @@ by (auto_tac (claset(),simpset() addsimps [isNSContc_NSCLIM_iff, NSCLIM_def,hcomplex_diff_def])); by (dtac (capprox_minus_iff RS iffD1) 1); -by (dtac (CLAIM "x ~= a ==> x + - a ~= (0::hcomplex)") 1); +by (subgoal_tac "xa + - (hcomplex_of_complex x) ~= 0" 1); + by (asm_full_simp_tac (simpset() addsimps compare_rls) 2); by (dres_inst_tac [("x","- hcomplex_of_complex x + xa")] bspec 1); by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_assoc RS sym]) 2); by (auto_tac (claset(),simpset() addsimps @@ -1041,12 +1042,14 @@ by (simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff]) 1); qed "NSCDERIV_pow"; -Goal "\\ CDERIV f x :> D; D = E \\ \\ CDERIV f x :> E"; +Goal "[|CDERIV f x :> D; D = E|] ==> CDERIV f x :> E"; by Auto_tac; qed "lemma_CDERIV_subst"; (*used once, in NSCDERIV_inverse*) Goal "[| h: CInfinitesimal; x ~= 0 |] ==> hcomplex_of_complex x + h ~= 0"; +by (Clarify_tac 1); +by (dtac (thm"equals_zero_I") 1); by Auto_tac; qed "CInfinitesimal_add_not_zero"; @@ -1062,7 +1065,7 @@ delsimps [hcomplex_minus_mult_eq1 RS sym, hcomplex_minus_mult_eq2 RS sym])); by (asm_simp_tac - (simpset() addsimps [hcomplex_inverse_add, + (simpset() addsimps [inverse_add, inverse_mult_distrib RS sym, hcomplex_minus_inverse RS sym] @ hcomplex_add_ac @ hcomplex_mult_ac delsimps [thm"Ring_and_Field.inverse_minus_eq", diff -r 255190be18c0 -r fb7a114826be src/HOL/Complex/NSCA.ML --- a/src/HOL/Complex/NSCA.ML Tue Dec 23 14:45:23 2003 +0100 +++ b/src/HOL/Complex/NSCA.ML Tue Dec 23 14:45:47 2003 +0100 @@ -1252,7 +1252,7 @@ by (forward_tac [CFinite_minus_iff RS iffD2] 1); by (rtac hcomplex_add_minus_eq_minus 1); by (dtac (stc_add RS sym) 1 THEN assume_tac 1); -by Auto_tac; +by (asm_simp_tac (simpset() addsimps [add_commute]) 1); qed "stc_minus"; Goalw [hcomplex_diff_def] diff -r 255190be18c0 -r fb7a114826be src/HOL/Complex/NSCA.thy --- a/src/HOL/Complex/NSCA.thy Tue Dec 23 14:45:23 2003 +0100 +++ b/src/HOL/Complex/NSCA.thy Tue Dec 23 14:45:47 2003 +0100 @@ -4,7 +4,7 @@ Description : Infinite, infinitesimal complex number etc! *) -NSCA = NSComplexArith0 + +NSCA = NSComplexArith + consts diff -r 255190be18c0 -r fb7a114826be src/HOL/Complex/NSComplex.thy --- a/src/HOL/Complex/NSComplex.thy Tue Dec 23 14:45:23 2003 +0100 +++ b/src/HOL/Complex/NSComplex.thy Tue Dec 23 14:45:47 2003 +0100 @@ -1761,13 +1761,13 @@ done declare hcomplex_of_complex_minus [simp] -lemma hcomplex_of_complex_one: +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_zero: +lemma hcomplex_of_complex_zero [simp]: "hcomplex_of_complex 0 = 0" apply (unfold hcomplex_of_complex_def hcomplex_zero_def) apply (simp (no_asm)) diff -r 255190be18c0 -r fb7a114826be src/HOL/Complex/NSComplexArith0.ML --- a/src/HOL/Complex/NSComplexArith0.ML Tue Dec 23 14:45:23 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,328 +0,0 @@ -(* Title: NSComplexArith0.ML - Author: Jacques D. Fleuriot - Copyright: 2001 University of Edinburgh - Description: Assorted facts that need binary literals - Also, common factor cancellation (see e.g. HyperArith0) -*) - -(**** -Goal "((x * y = #0) = (x = #0 | y = (#0::hcomplex)))"; -by (auto_tac (claset(),simpset() addsimps [rename_numerals hcomplex_mult_zero_iff])); -qed "hcomplex_mult_is_0"; -AddIffs [hcomplex_mult_is_0]; -****) - -(** Division and inverse **) - -Goal "0/x = (0::hcomplex)"; -by (simp_tac (simpset() addsimps [hcomplex_divide_def]) 1); -qed "hcomplex_0_divide"; -Addsimps [hcomplex_0_divide]; - -Goalw [hcomplex_divide_def] "x/(0::hcomplex) = 0"; -by (stac HCOMPLEX_INVERSE_ZERO 1); -by (Simp_tac 1); -qed "HCOMPLEX_DIVIDE_ZERO"; - -Goal "inverse (x::hcomplex) = 1/x"; -by (simp_tac (simpset() addsimps [hcomplex_divide_def]) 1); -qed "hcomplex_inverse_eq_divide"; - -Goal "(inverse(x::hcomplex) = 0) = (x = 0)"; -by (Simp_tac 1); -qed "hcomplex_inverse_zero_iff"; -Addsimps [hcomplex_inverse_zero_iff]; - -Goal "(x/y = 0) = (x=0 | y=(0::hcomplex))"; -by (auto_tac (claset(), simpset() addsimps [hcomplex_divide_def])); -qed "hcomplex_divide_eq_0_iff"; -Addsimps [hcomplex_divide_eq_0_iff]; - -Goal "h ~= (0::hcomplex) ==> h/h = 1"; -by (asm_simp_tac - (simpset() addsimps [hcomplex_divide_def]) 1); -qed "hcomplex_divide_self_eq"; -Addsimps [hcomplex_divide_self_eq]; - -bind_thm ("hcomplex_mult_minus_right", hcomplex_minus_mult_eq2 RS sym); - -Goal "!!k::hcomplex. (k*m = k*n) = (k = 0 | m=n)"; -by (case_tac "k=0" 1); -by (auto_tac (claset(), simpset() addsimps [hcomplex_mult_left_cancel])); -qed "hcomplex_mult_eq_cancel1"; - -Goal "!!k::hcomplex. (m*k = n*k) = (k = 0 | m=n)"; -by (case_tac "k=0" 1); -by (auto_tac (claset(), simpset() addsimps [hcomplex_mult_right_cancel])); -qed "hcomplex_mult_eq_cancel2"; - -Goal "!!k::hcomplex. k~=0 ==> (k*m) / (k*n) = (m/n)"; -by (asm_simp_tac - (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); -by (asm_full_simp_tac (HOL_ss addsimps hcomplex_mult_ac) 1); -qed "hcomplex_mult_div_cancel1"; - -(*For ExtractCommonTerm*) -Goal "(k*m) / (k*n) = (if k = (0::hcomplex) then 0 else m/n)"; -by (simp_tac (simpset() addsimps [hcomplex_mult_div_cancel1]) 1); -qed "hcomplex_mult_div_cancel_disj"; - - -local - open HComplex_Numeral_Simprocs -in - -val rel_hcomplex_number_of = [eq_hcomplex_number_of]; - - -structure CancelNumeralFactorCommon = - struct - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff 1 - val trans_tac = Real_Numeral_Simprocs.trans_tac - val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps hcomplex_minus_from_mult_simps @ mult_1s)) - THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@hcomplex_mult_minus_simps)) - THEN ALLGOALS (simp_tac (HOL_ss addsimps hcomplex_mult_ac)) - val numeral_simp_tac = - ALLGOALS (simp_tac (HOL_ss addsimps rel_hcomplex_number_of@bin_simps)) - val simplify_meta_eq = simplify_meta_eq - end - - -structure DivCancelNumeralFactor = CancelNumeralFactorFun - (open CancelNumeralFactorCommon - val prove_conv = Bin_Simprocs.prove_conv - val mk_bal = HOLogic.mk_binop "HOL.divide" - val dest_bal = HOLogic.dest_bin "HOL.divide" hcomplexT - val cancel = hcomplex_mult_div_cancel1 RS trans - val neg_exchanges = false -) - - -structure EqCancelNumeralFactor = CancelNumeralFactorFun - (open CancelNumeralFactorCommon - val prove_conv = Bin_Simprocs.prove_conv - val mk_bal = HOLogic.mk_eq - val dest_bal = HOLogic.dest_bin "op =" hcomplexT - val cancel = hcomplex_mult_eq_cancel1 RS trans - val neg_exchanges = false -) - - -val hcomplex_cancel_numeral_factors_relations = - map prep_simproc - [("hcomplexeq_cancel_numeral_factor", - ["(l::hcomplex) * m = n", "(l::hcomplex) = m * n"], - EqCancelNumeralFactor.proc)]; - -val hcomplex_cancel_numeral_factors_divide = prep_simproc - ("hcomplexdiv_cancel_numeral_factor", - ["((l::hcomplex) * m) / n", "(l::hcomplex) / (m * n)", - "((number_of v)::hcomplex) / (number_of w)"], - DivCancelNumeralFactor.proc); - -val hcomplex_cancel_numeral_factors = - hcomplex_cancel_numeral_factors_relations @ - [hcomplex_cancel_numeral_factors_divide]; - -end; - - -Addsimprocs hcomplex_cancel_numeral_factors; - - -(*examples: -print_depth 22; -set timing; -set trace_simp; -fun test s = (Goal s; by (Simp_tac 1)); - - -test "#9*x = #12 * (y::hcomplex)"; -test "(#9*x) / (#12 * (y::hcomplex)) = z"; - -test "#-99*x = #132 * (y::hcomplex)"; - -test "#999*x = #-396 * (y::hcomplex)"; -test "(#999*x) / (#-396 * (y::hcomplex)) = z"; - -test "#-99*x = #-81 * (y::hcomplex)"; -test "(#-99*x) / (#-81 * (y::hcomplex)) = z"; - -test "#-2 * x = #-1 * (y::hcomplex)"; -test "#-2 * x = -(y::hcomplex)"; -test "(#-2 * x) / (#-1 * (y::hcomplex)) = z"; - -*) - - -(** Declarations for ExtractCommonTerm **) - -local - open HComplex_Numeral_Simprocs -in - -structure CancelFactorCommon = - struct - val mk_sum = long_mk_prod - val dest_sum = dest_prod - val mk_coeff = mk_coeff - val dest_coeff = dest_coeff - val find_first = find_first [] - val trans_tac = Real_Numeral_Simprocs.trans_tac - val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@hcomplex_mult_ac)) - end; - - -structure EqCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Bin_Simprocs.prove_conv - val mk_bal = HOLogic.mk_eq - val dest_bal = HOLogic.dest_bin "op =" hcomplexT - val simplify_meta_eq = cancel_simplify_meta_eq hcomplex_mult_eq_cancel1 -); - - -structure DivideCancelFactor = ExtractCommonTermFun - (open CancelFactorCommon - val prove_conv = Bin_Simprocs.prove_conv - val mk_bal = HOLogic.mk_binop "HOL.divide" - val dest_bal = HOLogic.dest_bin "HOL.divide" hcomplexT - val simplify_meta_eq = cancel_simplify_meta_eq hcomplex_mult_div_cancel_disj -); - -val hcomplex_cancel_factor = - map prep_simproc - [("hcomplex_eq_cancel_factor", ["(l::hcomplex) * m = n", "(l::hcomplex) = m * n"], - EqCancelFactor.proc), - ("hcomplex_divide_cancel_factor", ["((l::hcomplex) * m) / n", "(l::hcomplex) / (m * n)"], - DivideCancelFactor.proc)]; - -end; - -Addsimprocs hcomplex_cancel_factor; - - -(*examples: -print_depth 22; -set timing; -set trace_simp; -fun test s = (Goal s; by (Asm_simp_tac 1)); - -test "x*k = k*(y::hcomplex)"; -test "k = k*(y::hcomplex)"; -test "a*(b*c) = (b::hcomplex)"; -test "a*(b*c) = d*(b::hcomplex)*(x*a)"; - - -test "(x*k) / (k*(y::hcomplex)) = (uu::hcomplex)"; -test "(k) / (k*(y::hcomplex)) = (uu::hcomplex)"; -test "(a*(b*c)) / ((b::hcomplex)) = (uu::hcomplex)"; -test "(a*(b*c)) / (d*(b::hcomplex)*(x*a)) = (uu::hcomplex)"; - -(*FIXME: what do we do about this?*) -test "a*(b*c)/(y*z) = d*(b::hcomplex)*(x*a)/z"; -*) - - -Goal "z~=0 ==> ((x::hcomplex) = y/z) = (x*z = y)"; -by (subgoal_tac "(x*z = y) = (x*z = (y/z)*z)" 1); -by (asm_simp_tac (simpset() addsimps [hcomplex_divide_def, hcomplex_mult_assoc]) 2); -by (etac ssubst 1); -by (stac hcomplex_mult_eq_cancel2 1); -by (Asm_simp_tac 1); -qed "hcomplex_eq_divide_eq"; -Addsimps [inst "z" "number_of ?w" hcomplex_eq_divide_eq]; - -Goal "z~=0 ==> (y/z = (x::hcomplex)) = (y = x*z)"; -by (subgoal_tac "(y = x*z) = ((y/z)*z = x*z)" 1); -by (asm_simp_tac (simpset() addsimps [hcomplex_divide_def, hcomplex_mult_assoc]) 2); -by (etac ssubst 1); -by (stac hcomplex_mult_eq_cancel2 1); -by (Asm_simp_tac 1); -qed "hcomplex_divide_eq_eq"; -Addsimps [inst "z" "number_of ?w" hcomplex_divide_eq_eq]; - -Goal "(m/k = n/k) = (k = 0 | m = (n::hcomplex))"; -by (case_tac "k=0" 1); -by (asm_simp_tac (simpset() addsimps [HCOMPLEX_DIVIDE_ZERO]) 1); -by (asm_simp_tac (simpset() addsimps [hcomplex_divide_eq_eq, hcomplex_eq_divide_eq, - hcomplex_mult_eq_cancel2]) 1); -qed "hcomplex_divide_eq_cancel2"; - -Goal "(k/m = k/n) = (k = 0 | m = (n::hcomplex))"; -by (case_tac "m=0 | n = 0" 1); -by (auto_tac (claset(), - simpset() addsimps [HCOMPLEX_DIVIDE_ZERO, hcomplex_divide_eq_eq, - hcomplex_eq_divide_eq, hcomplex_mult_eq_cancel1])); -qed "hcomplex_divide_eq_cancel1"; - -(** Division by 1, -1 **) - -Goal "(x::hcomplex)/1 = x"; -by (simp_tac (simpset() addsimps [hcomplex_divide_def]) 1); -qed "hcomplex_divide_1"; -Addsimps [hcomplex_divide_1]; - -Goal "x/-1 = -(x::hcomplex)"; -by (Simp_tac 1); -qed "hcomplex_divide_minus1"; -Addsimps [hcomplex_divide_minus1]; - -Goal "-1/(x::hcomplex) = - (1/x)"; -by (simp_tac (simpset() addsimps [hcomplex_divide_def, hcomplex_minus_inverse]) 1); -qed "hcomplex_minus1_divide"; -Addsimps [hcomplex_minus1_divide]; - - -Goal "(x = - y) = (y = - (x::hcomplex))"; -by Auto_tac; -qed "hcomplex_equation_minus"; - -Goal "(- x = y) = (- (y::hcomplex) = x)"; -by Auto_tac; -qed "hcomplex_minus_equation"; - -Goal "(x + - a = (0::hcomplex)) = (x=a)"; -by (simp_tac (simpset() addsimps [hcomplex_diff_eq_eq,symmetric hcomplex_diff_def]) 1); -qed "hcomplex_add_minus_iff"; -Addsimps [hcomplex_add_minus_iff]; - -Goal "(-b = -a) = (b = (a::hcomplex))"; -by Auto_tac; -qed "hcomplex_minus_eq_cancel"; -Addsimps [hcomplex_minus_eq_cancel]; - -(*Distributive laws for literals*) -Addsimps (map (inst "w" "number_of ?v") - [hcomplex_add_mult_distrib, hcomplex_add_mult_distrib2, - hcomplex_diff_mult_distrib, hcomplex_diff_mult_distrib2]); - -Addsimps [inst "x" "number_of ?v" hcomplex_equation_minus]; - -Addsimps [inst "y" "number_of ?v" hcomplex_minus_equation]; - -Goal "(x+y = (0::hcomplex)) = (y = -x)"; -by Auto_tac; -by (dtac (sym RS (hcomplex_diff_eq_eq RS iffD2)) 1); -by Auto_tac; -qed "hcomplex_add_eq_0_iff"; -AddIffs [hcomplex_add_eq_0_iff]; - -Goalw [hcomplex_diff_def]"-(x-y) = y - (x::hcomplex)"; -by (auto_tac (claset(),simpset() addsimps [hcomplex_add_commute])); -qed "hcomplex_minus_diff_eq"; -Addsimps [hcomplex_minus_diff_eq]; - -Addsimps [inst "x" "number_of ?w" hcomplex_inverse_eq_divide]; - -Goal "[|(x::hcomplex) ~= 0; y ~= 0 |] \ -\ ==> inverse(x) + inverse(y) = (x + y)*inverse(x*y)"; -by (asm_full_simp_tac (simpset() addsimps [inverse_mult_distrib, - hcomplex_add_mult_distrib,hcomplex_mult_assoc RS sym]) 1); -qed "hcomplex_inverse_add"; - -Addsimps [hcomplex_of_complex_zero,hcomplex_of_complex_one]; diff -r 255190be18c0 -r fb7a114826be src/HOL/Complex/NSComplexArith0.thy --- a/src/HOL/Complex/NSComplexArith0.thy Tue Dec 23 14:45:23 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,4 +0,0 @@ -NSComplexArith0 = NSComplexBin - - - diff -r 255190be18c0 -r fb7a114826be src/HOL/Complex/NSComplexBin.ML --- a/src/HOL/Complex/NSComplexBin.ML Tue Dec 23 14:45:23 2003 +0100 +++ b/src/HOL/Complex/NSComplexBin.ML Tue Dec 23 14:45:47 2003 +0100 @@ -24,11 +24,11 @@ qed "hcomplex_hypreal_number_of"; Goalw [hcomplex_number_of_def] "Numeral0 = (0::hcomplex)"; -by (simp_tac (simpset() addsimps [hcomplex_of_complex_zero RS sym]) 1); +by(Simp_tac 1); qed "hcomplex_numeral_0_eq_0"; Goalw [hcomplex_number_of_def] "Numeral1 = (1::hcomplex)"; -by (simp_tac (simpset() addsimps [hcomplex_of_complex_one RS sym]) 1); +by(Simp_tac 1); qed "hcomplex_numeral_1_eq_1"; (* diff -r 255190be18c0 -r fb7a114826be src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Dec 23 14:45:23 2003 +0100 +++ b/src/HOL/IsaMakefile Tue Dec 23 14:45:47 2003 +0100 @@ -174,7 +174,7 @@ Complex/ComplexBin.ML Complex/ComplexBin.thy\ Complex/NSCA.ML Complex/NSCA.thy\ Complex/NSComplex.thy\ - Complex/NSComplexArith0.ML Complex/NSComplexArith0.thy\ + Complex/hcomplex_arith.ML Complex/NSComplexArith.thy\ Complex/NSComplexBin.ML Complex/NSComplexBin.thy @cd Complex; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Complex