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