# HG changeset patch # User paulson # Date 1072200363 -3600 # Node ID c817dd885a3204c3eb270f9770fcef8adf360763 # Parent 94ac3895822f9b9a099c99827918115bad91e96b reorganised complex arithmetic diff -r 94ac3895822f -r c817dd885a32 src/HOL/Complex/NSComplexArith.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Complex/NSComplexArith.thy Tue Dec 23 18:26:03 2003 +0100 @@ -0,0 +1,19 @@ +(* Title: NSComplexArith + Author: Lawrence C. Paulson + Copyright: 2003 University of Cambridge + +Common factor cancellation +*) + +theory NSComplexArith = NSComplexBin +files "hcomplex_arith.ML": + +subsubsection{*Division By @{term "-1"}*} + +lemma hcomplex_divide_minus1 [simp]: "x/-1 = -(x::hcomplex)" +by simp + +lemma hcomplex_minus1_divide [simp]: "-1/(x::hcomplex) = - (1/x)" +by (simp add: hcomplex_divide_def hcomplex_minus_inverse) + +end diff -r 94ac3895822f -r c817dd885a32 src/HOL/Complex/hcomplex_arith.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Complex/hcomplex_arith.ML Tue Dec 23 18:26:03 2003 +0100 @@ -0,0 +1,164 @@ +(* Title: hcomplex_arith.ML + Author: Jacques D. Fleuriot + Copyright: 2001 University of Edinburgh + +Common factor cancellation +*) + +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 = mult_divide_cancel_left 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 = field_mult_cancel_left 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 field_mult_cancel_left +); + + +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 mult_divide_cancel_eq_if +); + +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"; +*) + +