equal
deleted
inserted
replaced
|
1 (* Title: HOL/Integ/IntDiv_setup.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow, Informatik, TU Muenchen |
|
4 Copyright 2002 TU Muenchen |
|
5 |
|
6 Simproc for cancelling div and mod |
|
7 *) |
|
8 |
|
9 |
|
10 structure CancelDivModData = |
|
11 struct |
|
12 |
|
13 val div_name = "Divides.op div"; |
|
14 val mod_name = "Divides.op mod"; |
|
15 val mk_binop = HOLogic.mk_binop; |
|
16 val mk_sum = Int_Numeral_Simprocs.mk_sum; |
|
17 val dest_sum = Int_Numeral_Simprocs.dest_sum; |
|
18 |
|
19 (*logic*) |
|
20 |
|
21 val div_mod_eqs = |
|
22 map mk_meta_eq [thm"zdiv_zmod_equality",thm"zdiv_zmod_equality2"] |
|
23 |
|
24 val trans = trans |
|
25 |
|
26 val prove_eq_sums = |
|
27 let val simps = zdiff_def :: Int_Numeral_Simprocs.add_0s @ zadd_ac |
|
28 in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all simps) end |
|
29 |
|
30 end; |
|
31 |
|
32 structure CancelDivMod = CancelDivModFun(CancelDivModData); |
|
33 |
|
34 val cancel_zdiv_zmod_proc = NatArithUtils.prep_simproc |
|
35 ("cancel_zdiv_zmod", ["(m::int) + n"], CancelDivMod.proc); |
|
36 |
|
37 Addsimprocs[cancel_zdiv_zmod_proc]; |