32 (* not needed because x < (y::int) can be rewritten as x + 1 <= y: |
32 (* not needed because x < (y::int) can be rewritten as x + 1 <= y: |
33 of_int_less_iff RS iffD2 *) |
33 of_int_less_iff RS iffD2 *) |
34 |
34 |
35 in |
35 in |
36 |
36 |
37 val ratT = Type ("Rational.rat", []) |
|
38 |
|
39 val rat_arith_setup = |
37 val rat_arith_setup = |
40 LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => |
38 LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} => |
41 {add_mono_thms = add_mono_thms, |
39 {add_mono_thms = add_mono_thms, |
42 mult_mono_thms = mult_mono_thms, |
40 mult_mono_thms = mult_mono_thms, |
43 inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms, |
41 inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms, |
44 lessD = lessD, (*Can't change lessD: the rats are dense!*) |
42 lessD = lessD, (*Can't change lessD: the rats are dense!*) |
45 neqE = neqE, |
43 neqE = neqE, |
46 simpset = simpset addsimps simps |
44 simpset = simpset addsimps simps |
47 addsimprocs simprocs}) #> |
45 addsimprocs simprocs}) #> |
48 arith_inj_const (@{const_name of_nat}, HOLogic.natT --> ratT) #> |
46 arith_inj_const (@{const_name of_nat}, @{typ "nat => rat"}) #> |
49 arith_inj_const (@{const_name of_int}, HOLogic.intT --> ratT) |
47 arith_inj_const (@{const_name of_int}, @{typ "int => rat"}) |
50 |
48 |
51 end; |
49 end; |