diff -r d149e3cbdb39 -r deb8e1e62002 src/HOL/Real/real_arith.ML --- a/src/HOL/Real/real_arith.ML Wed Dec 10 15:59:34 2003 +0100 +++ b/src/HOL/Real/real_arith.ML Wed Dec 10 16:47:50 2003 +0100 @@ -1,22 +1,238 @@ (* Title: HOL/Real/real_arith.ML ID: $Id$ Author: Tobias Nipkow, TU Muenchen - Copyright 1999 TU Muenchen + Author: Lawrence C Paulson, Cambridge University Computer Laboratory -Augmentation of real linear arithmetic with rational coefficient handling +Simprocs: Common factor cancellation & Rational coefficient handling *) -val real_divide_1 = thm"real_divide_1"; + +(** Misc ML bindings **) + +val real_inverse_less_iff = thm"real_inverse_less_iff"; +val real_inverse_le_iff = thm"real_inverse_le_iff"; + +val pos_real_less_divide_eq = thm"pos_less_divide_eq"; +val pos_real_divide_less_eq = thm"pos_divide_less_eq"; +val pos_real_le_divide_eq = thm"pos_le_divide_eq"; +val pos_real_divide_le_eq = thm"pos_divide_le_eq"; + + +(****Common factor cancellation****) + +val real_inverse_eq_divide = thm"real_inverse_eq_divide"; +val real_mult_less_cancel2 = thm"real_mult_less_cancel2"; +val real_mult_le_cancel2 = thm"real_mult_le_cancel2"; +val real_mult_less_cancel1 = thm"real_mult_less_cancel1"; +val real_mult_le_cancel1 = thm"real_mult_le_cancel1"; +val real_mult_eq_cancel1 = thm"real_mult_eq_cancel1"; +val real_mult_eq_cancel2 = thm"real_mult_eq_cancel2"; +val real_mult_div_cancel1 = thm"real_mult_div_cancel1"; +val real_mult_div_cancel_disj = thm"real_mult_div_cancel_disj"; + local + open Real_Numeral_Simprocs +in + +val rel_real_number_of = [eq_real_number_of, less_real_number_of, + le_real_number_of_eq_not_less] + +structure CancelNumeralFactorCommon = + struct + val mk_coeff = mk_coeff + val dest_coeff = dest_coeff 1 + val trans_tac = trans_tac + val norm_tac = + ALLGOALS (simp_tac (HOL_ss addsimps real_minus_from_mult_simps @ mult_1s)) + THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@real_mult_minus_simps)) + THEN ALLGOALS (simp_tac (HOL_ss addsimps real_mult_ac)) + val numeral_simp_tac = + ALLGOALS (simp_tac (HOL_ss addsimps rel_real_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" HOLogic.realT + val cancel = real_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 =" HOLogic.realT + val cancel = real_mult_eq_cancel1 RS trans + val neg_exchanges = false +) + +structure LessCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Bin_Simprocs.prove_conv + val mk_bal = HOLogic.mk_binrel "op <" + val dest_bal = HOLogic.dest_bin "op <" HOLogic.realT + val cancel = real_mult_less_cancel1 RS trans + val neg_exchanges = true +) + +structure LeCancelNumeralFactor = CancelNumeralFactorFun + (open CancelNumeralFactorCommon + val prove_conv = Bin_Simprocs.prove_conv + val mk_bal = HOLogic.mk_binrel "op <=" + val dest_bal = HOLogic.dest_bin "op <=" HOLogic.realT + val cancel = real_mult_le_cancel1 RS trans + val neg_exchanges = true +) + +val real_cancel_numeral_factors_relations = + map prep_simproc + [("realeq_cancel_numeral_factor", + ["(l::real) * m = n", "(l::real) = m * n"], + EqCancelNumeralFactor.proc), + ("realless_cancel_numeral_factor", + ["(l::real) * m < n", "(l::real) < m * n"], + LessCancelNumeralFactor.proc), + ("realle_cancel_numeral_factor", + ["(l::real) * m <= n", "(l::real) <= m * n"], + LeCancelNumeralFactor.proc)] + +val real_cancel_numeral_factors_divide = prep_simproc + ("realdiv_cancel_numeral_factor", + ["((l::real) * m) / n", "(l::real) / (m * n)", + "((number_of v)::real) / (number_of w)"], + DivCancelNumeralFactor.proc) + +val real_cancel_numeral_factors = + real_cancel_numeral_factors_relations @ + [real_cancel_numeral_factors_divide] + +end; + +Addsimprocs real_cancel_numeral_factors; + + +(*examples: +print_depth 22; +set timing; +set trace_simp; +fun test s = (Goal s; by (Simp_tac 1)); + +test "0 <= (y::real) * -2"; +test "9*x = 12 * (y::real)"; +test "(9*x) / (12 * (y::real)) = z"; +test "9*x < 12 * (y::real)"; +test "9*x <= 12 * (y::real)"; + +test "-99*x = 132 * (y::real)"; +test "(-99*x) / (132 * (y::real)) = z"; +test "-99*x < 132 * (y::real)"; +test "-99*x <= 132 * (y::real)"; + +test "999*x = -396 * (y::real)"; +test "(999*x) / (-396 * (y::real)) = z"; +test "999*x < -396 * (y::real)"; +test "999*x <= -396 * (y::real)"; + +test "(- ((2::real) * x) <= 2 * y)"; +test "-99*x = -81 * (y::real)"; +test "(-99*x) / (-81 * (y::real)) = z"; +test "-99*x <= -81 * (y::real)"; +test "-99*x < -81 * (y::real)"; + +test "-2 * x = -1 * (y::real)"; +test "-2 * x = -(y::real)"; +test "(-2 * x) / (-1 * (y::real)) = z"; +test "-2 * x < -(y::real)"; +test "-2 * x <= -1 * (y::real)"; +test "-x < -23 * (y::real)"; +test "-x <= -23 * (y::real)"; +*) + + +(** Declarations for ExtractCommonTerm **) + +local + open Real_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 = trans_tac + val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps mult_1s@real_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 =" HOLogic.realT + val simplify_meta_eq = cancel_simplify_meta_eq real_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" HOLogic.realT + val simplify_meta_eq = cancel_simplify_meta_eq real_mult_div_cancel_disj +); + +val real_cancel_factor = + map prep_simproc + [("real_eq_cancel_factor", ["(l::real) * m = n", "(l::real) = m * n"], EqCancelFactor.proc), + ("real_divide_cancel_factor", ["((l::real) * m) / n", "(l::real) / (m * n)"], + DivideCancelFactor.proc)]; + +end; + +Addsimprocs real_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::real)"; +test "k = k*(y::real)"; +test "a*(b*c) = (b::real)"; +test "a*(b*c) = d*(b::real)*(x*a)"; + + +test "(x*k) / (k*(y::real)) = (uu::real)"; +test "(k) / (k*(y::real)) = (uu::real)"; +test "(a*(b*c)) / ((b::real)) = (uu::real)"; +test "(a*(b*c)) / (d*(b::real)*(x*a)) = (uu::real)"; + +(*FIXME: what do we do about this?*) +test "a*(b*c)/(y*z) = d*(b::real)*(x*a)/z"; +*) + +(****Augmentation of real linear arithmetic with + rational coefficient handling****) + +val divide_1 = thm"divide_1"; val times_divide_eq_left = thm"times_divide_eq_left"; val times_divide_eq_right = thm"times_divide_eq_right"; +local + (* reduce contradictory <= to False *) val simps = [True_implies_equals, inst "w" "number_of ?v" real_add_mult_distrib2, - real_divide_1,times_divide_eq_right,times_divide_eq_left]; + divide_1,times_divide_eq_right,times_divide_eq_left]; val simprocs = [real_cancel_numeral_factors_divide];