15 val simps = [@{thm order_less_irrefl}, @{thm neg_less_iff_less}, @{thm 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)" @{thm right_distrib}, |
16 inst "a" "(number_of ?v)" @{thm right_distrib}, |
17 @{thm divide_1}, @{thm divide_zero_left}, |
17 @{thm divide_1}, @{thm divide_zero_left}, |
18 @{thm times_divide_eq_right}, @{thm times_divide_eq_left}, |
18 @{thm times_divide_eq_right}, @{thm times_divide_eq_left}, |
19 @{thm minus_divide_left} RS sym, @{thm 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, @{thm of_int_add}, @{thm of_int_minus}, @{thm of_int_diff}, |
21 of_int_mult, of_int_of_nat_eq] |
21 @{thm of_int_mult}, @{thm of_int_of_nat_eq}] |
22 |
22 |
23 val nat_inj_thms = [of_nat_le_iff RS iffD2, |
23 val nat_inj_thms = [@{thm of_nat_le_iff} RS iffD2, |
24 of_nat_eq_iff RS iffD2] |
24 @{thm of_nat_eq_iff} RS iffD2] |
25 (* not needed because x < (y::nat) can be rewritten as Suc x <= y: |
25 (* not needed because x < (y::nat) can be rewritten as Suc x <= y: |
26 of_nat_less_iff RS iffD2 *) |
26 of_nat_less_iff RS iffD2 *) |
27 |
27 |
28 val int_inj_thms = [of_int_le_iff RS iffD2, |
28 val int_inj_thms = [@{thm of_int_le_iff} RS iffD2, |
29 of_int_eq_iff RS iffD2] |
29 @{thm of_int_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 |