10 |
10 |
11 local |
11 local |
12 |
12 |
13 val simprocs = field_cancel_numeral_factors |
13 val simprocs = field_cancel_numeral_factors |
14 |
14 |
15 val simps = [order_less_irrefl, neg_less_iff_less, True_implies_equals, |
15 val simps = [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm True_implies_equals}, |
16 inst "a" "(number_of ?v)" right_distrib, |
16 inst "a" "(number_of ?v)" @{thm right_distrib}, |
17 divide_1, divide_zero_left, |
17 @{thm divide_1}, @{thm divide_zero_left}, |
18 times_divide_eq_right, times_divide_eq_left, |
18 @{thm times_divide_eq_right}, @{thm times_divide_eq_left}, |
19 minus_divide_left RS sym, minus_divide_right RS sym, |
19 @{thm minus_divide_left} RS sym, @{thm minus_divide_right} RS sym, |
20 of_int_0, of_int_1, of_int_add, of_int_minus, of_int_diff, |
20 of_int_0, of_int_1, of_int_add, of_int_minus, of_int_diff, |
21 of_int_mult, of_int_of_nat_eq] |
21 of_int_mult, of_int_of_nat_eq] |
22 |
22 |
23 val nat_inj_thms = [of_nat_le_iff RS iffD2, |
23 val nat_inj_thms = [of_nat_le_iff RS iffD2, |
24 of_nat_eq_iff RS iffD2] |
24 of_nat_eq_iff RS iffD2] |
30 (* not needed because x < (y::int) can be rewritten as x + 1 <= y: |
30 (* not needed because x < (y::int) can be rewritten as x + 1 <= y: |
31 of_int_less_iff RS iffD2 *) |
31 of_int_less_iff RS iffD2 *) |
32 |
32 |
33 in |
33 in |
34 |
34 |
35 val fast_rat_arith_simproc = |
35 val fast_rat_arith_simproc = Simplifier.simproc @{theory} |
36 Simplifier.simproc (the_context ()) |
|
37 "fast_rat_arith" ["(m::rat) < n","(m::rat) <= n", "(m::rat) = n"] |
36 "fast_rat_arith" ["(m::rat) < n","(m::rat) <= n", "(m::rat) = n"] |
38 Fast_Arith.lin_arith_prover |
37 Fast_Arith.lin_arith_prover |
39 |
38 |
40 val ratT = Type ("Rational.rat", []) |
39 val ratT = Type ("Rational.rat", []) |
41 |
40 |
42 val rat_arith_setup = |
41 val rat_arith_setup = |
43 Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => |
42 Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => |