# HG changeset patch # User paulson # Date 1071071270 -3600 # Node ID deb8e1e62002adf0d36fc15e2e60d68ee2ed47b3 # Parent d149e3cbdb39e5dea45ddc3af0b4c3d434d22ebc combining Real/{RealArith0,real_arith}.ML diff -r d149e3cbdb39 -r deb8e1e62002 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Wed Dec 10 15:59:34 2003 +0100 +++ b/src/HOL/IsaMakefile Wed Dec 10 16:47:50 2003 +0100 @@ -141,7 +141,7 @@ Real/PRat.ML Real/PRat.thy \ Real/PReal.ML Real/PReal.thy Real/RComplete.ML Real/RComplete.thy \ Real/ROOT.ML Real/Real.thy \ - Real/RealArith0.ML Real/RealArith0.thy Real/real_arith0.ML \ + Real/RealArith0.thy Real/real_arith0.ML \ Real/RealArith.thy Real/real_arith.ML Real/RealBin.ML \ Real/RealBin.thy Real/RealDef.thy \ Real/RealInt.thy Real/RealOrd.thy \ diff -r d149e3cbdb39 -r deb8e1e62002 src/HOL/Real/RealArith0.ML --- a/src/HOL/Real/RealArith0.ML Wed Dec 10 15:59:34 2003 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,214 +0,0 @@ -(* Title: HOL/Real/RealArith.ML - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1999 University of Cambridge - -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"; -*) - -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"; 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];