|
13517
|
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];
|