3 Simprocs for nat numerals. |
3 Simprocs for nat numerals. |
4 *) |
4 *) |
5 |
5 |
6 signature NAT_NUMERAL_SIMPROCS = |
6 signature NAT_NUMERAL_SIMPROCS = |
7 sig |
7 sig |
8 val combine_numerals: Proof.context -> cterm -> thm option |
8 val combine_numerals: Simplifier.proc |
9 val eq_cancel_numerals: Proof.context -> cterm -> thm option |
9 val eq_cancel_numerals: Simplifier.proc |
10 val less_cancel_numerals: Proof.context -> cterm -> thm option |
10 val less_cancel_numerals: Simplifier.proc |
11 val le_cancel_numerals: Proof.context -> cterm -> thm option |
11 val le_cancel_numerals: Simplifier.proc |
12 val diff_cancel_numerals: Proof.context -> cterm -> thm option |
12 val diff_cancel_numerals: Simplifier.proc |
13 val eq_cancel_numeral_factor: Proof.context -> cterm -> thm option |
13 val eq_cancel_numeral_factor: Simplifier.proc |
14 val less_cancel_numeral_factor: Proof.context -> cterm -> thm option |
14 val less_cancel_numeral_factor: Simplifier.proc |
15 val le_cancel_numeral_factor: Proof.context -> cterm -> thm option |
15 val le_cancel_numeral_factor: Simplifier.proc |
16 val div_cancel_numeral_factor: Proof.context -> cterm -> thm option |
16 val div_cancel_numeral_factor: Simplifier.proc |
17 val dvd_cancel_numeral_factor: Proof.context -> cterm -> thm option |
17 val dvd_cancel_numeral_factor: Simplifier.proc |
18 val eq_cancel_factor: Proof.context -> cterm -> thm option |
18 val eq_cancel_factor: Simplifier.proc |
19 val less_cancel_factor: Proof.context -> cterm -> thm option |
19 val less_cancel_factor: Simplifier.proc |
20 val le_cancel_factor: Proof.context -> cterm -> thm option |
20 val le_cancel_factor: Simplifier.proc |
21 val div_cancel_factor: Proof.context -> cterm -> thm option |
21 val div_cancel_factor: Simplifier.proc |
22 val dvd_cancel_factor: Proof.context -> cterm -> thm option |
22 val dvd_cancel_factor: Simplifier.proc |
23 end; |
23 end; |
24 |
24 |
25 structure Nat_Numeral_Simprocs : NAT_NUMERAL_SIMPROCS = |
25 structure Nat_Numeral_Simprocs : NAT_NUMERAL_SIMPROCS = |
26 struct |
26 struct |
27 |
27 |