--- a/src/HOL/Real/rat_arith.ML Mon Feb 16 15:24:03 2004 +0100
+++ b/src/HOL/Real/rat_arith.ML Tue Feb 17 10:41:59 2004 +0100
@@ -8,236 +8,20 @@
Instantiation of the generic linear arithmetic package for type rat.
*)
-(*FIXME DELETE*)
+(*FIXME: these monomorphic versions are necessary because of a bug in the arith
+ procedure*)
val rat_mult_strict_left_mono =
read_instantiate_sg(sign_of (the_context())) [("a","?a::rat")] mult_strict_left_mono;
val rat_mult_left_mono =
read_instantiate_sg(sign_of (the_context())) [("a","?a::rat")] mult_left_mono;
- val le_number_of_eq = thm"le_number_of_eq";
-
-
-(****Common factor cancellation****)
-
-(*To quote from Provers/Arith/cancel_numeral_factor.ML:
-
-This simproc Cancels common coefficients in balanced expressions:
-
- u*#m ~~ u'*#m' == #n*u ~~ #n'*u'
-
-where ~~ is an appropriate balancing operation (e.g. =, <=, <, div, /)
-and d = gcd(m,m') and n=m/d and n'=m'/d.
-*)
-
-val rel_number_of = [eq_number_of_eq, less_number_of_eq_neg, le_number_of_eq]
-
-local open Int_Numeral_Simprocs
-in
-
-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 minus_from_mult_simps @ mult_1s))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_minus_simps))
- THEN ALLGOALS (simp_tac (HOL_ss addsimps mult_ac))
- val numeral_simp_tac =
- ALLGOALS (simp_tac (HOL_ss addsimps rel_number_of@bin_simps))
- val simplify_meta_eq =
- Int_Numeral_Simprocs.simplify_meta_eq
- [add_0, add_0_right,
- mult_zero_left, mult_zero_right, mult_1, mult_1_right];
- 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" Term.dummyT
- 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 =" Term.dummyT
- val cancel = field_mult_cancel_left 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 <" Term.dummyT
- val cancel = mult_less_cancel_left 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 <=" Term.dummyT
- val cancel = mult_le_cancel_left RS trans
- val neg_exchanges = true
-)
-
-val field_cancel_numeral_factors_relations =
- map Bin_Simprocs.prep_simproc
- [("field_eq_cancel_numeral_factor",
- ["(l::'a::{field,number_ring}) * m = n",
- "(l::'a::{field,number_ring}) = m * n"],
- EqCancelNumeralFactor.proc),
- ("field_less_cancel_numeral_factor",
- ["(l::'a::{ordered_field,number_ring}) * m < n",
- "(l::'a::{ordered_field,number_ring}) < m * n"],
- LessCancelNumeralFactor.proc),
- ("field_le_cancel_numeral_factor",
- ["(l::'a::{ordered_field,number_ring}) * m <= n",
- "(l::'a::{ordered_field,number_ring}) <= m * n"],
- LeCancelNumeralFactor.proc)]
-
-val field_cancel_numeral_factors_divide =
- Bin_Simprocs.prep_simproc
- ("field_cancel_numeral_factor",
- ["((l::'a::{field,number_ring}) * m) / n",
- "(l::'a::{field,number_ring}) / (m * n)",
- "((number_of v)::'a::{field,number_ring}) / (number_of w)"],
- DivCancelNumeralFactor.proc)
-
-val field_cancel_numeral_factors =
- field_cancel_numeral_factors_relations @
- [field_cancel_numeral_factors_divide]
-
-end;
-
-Addsimprocs field_cancel_numeral_factors;
-
-
-(*examples:
-print_depth 22;
-set timing;
-set trace_simp;
-fun test s = (Goal s; by (Simp_tac 1));
-
-test "0 <= (y::rat) * -2";
-test "9*x = 12 * (y::rat)";
-test "(9*x) / (12 * (y::rat)) = z";
-test "9*x < 12 * (y::rat)";
-test "9*x <= 12 * (y::rat)";
-
-test "-99*x = 132 * (y::rat)";
-test "(-99*x) / (132 * (y::rat)) = z";
-test "-99*x < 132 * (y::rat)";
-test "-99*x <= 132 * (y::rat)";
-
-test "999*x = -396 * (y::rat)";
-test "(999*x) / (-396 * (y::rat)) = z";
-test "999*x < -396 * (y::rat)";
-test "999*x <= -396 * (y::rat)";
-
-test "(- ((2::rat) * x) <= 2 * y)";
-test "-99*x = -81 * (y::rat)";
-test "(-99*x) / (-81 * (y::rat)) = z";
-test "-99*x <= -81 * (y::rat)";
-test "-99*x < -81 * (y::rat)";
-
-test "-2 * x = -1 * (y::rat)";
-test "-2 * x = -(y::rat)";
-test "(-2 * x) / (-1 * (y::rat)) = z";
-test "-2 * x < -(y::rat)";
-test "-2 * x <= -1 * (y::rat)";
-test "-x < -23 * (y::rat)";
-test "-x <= -23 * (y::rat)";
-*)
-
-
-(** Declarations for ExtractCommonTerm **)
-
-local open Int_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@mult_ac))
- end;
-
-(*This version works for all fields, including unordered ones (complex).
- The version declared in int_factor_simprocs.ML is for integers.*)
-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 =" Term.dummyT
- val simplify_meta_eq = cancel_simplify_meta_eq field_mult_cancel_left
-);
-
-
-(*This version works for fields, with the generic divides operator (/).
- The version declared in int_factor_simprocs.ML for integers with div.*)
-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" Term.dummyT
- val simplify_meta_eq = cancel_simplify_meta_eq mult_divide_cancel_eq_if
-);
-
-val field_cancel_factor =
- map Bin_Simprocs.prep_simproc
- [("field_eq_cancel_factor",
- ["(l::'a::field) * m = n", "(l::'a::field) = m * n"],
- EqCancelFactor.proc),
- ("field_divide_cancel_factor",
- ["((l::'a::field) * m) / n", "(l::'a::field) / (m * n)"],
- DivideCancelFactor.proc)];
-
-end;
-
-Addsimprocs field_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::rat)";
-test "k = k*(y::rat)";
-test "a*(b*c) = (b::rat)";
-test "a*(b*c) = d*(b::rat)*(x*a)";
-
-
-test "(x*k) / (k*(y::rat)) = (uu::rat)";
-test "(k) / (k*(y::rat)) = (uu::rat)";
-test "(a*(b*c)) / ((b::rat)) = (uu::rat)";
-test "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)";
-
-(*FIXME: what do we do about this?*)
-test "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z";
-*)
-
-
(****Instantiation of the generic linear arithmetic package for fields****)
-
local
-val simprocs = [field_cancel_numeral_factors_divide]
+val simprocs = field_cancel_numeral_factors
val mono_ss = simpset() addsimps
[add_mono,add_strict_mono,add_less_le_mono,add_le_less_mono];
@@ -259,10 +43,11 @@
(rat_mult_left_mono,
cvar(rat_mult_left_mono, hd(tl(prems_of rat_mult_left_mono))))]
-val simps = [order_less_irrefl, True_implies_equals,
+val simps = [order_less_irrefl, neg_less_iff_less, True_implies_equals,
inst "a" "(number_of ?v)" right_distrib,
divide_1, divide_zero_left,
times_divide_eq_right, times_divide_eq_left,
+ minus_divide_left RS sym, minus_divide_right RS sym,
of_int_0, of_int_1, of_int_add, of_int_minus, of_int_diff,
of_int_mult, of_int_of_nat_eq];