| author | paulson |
| Wed, 24 Mar 2004 10:50:29 +0100 | |
| changeset 14479 | 0eca4aabf371 |
| parent 14387 | e96d5c42c4b0 |
| child 17609 | 5156b731ebc8 |
| permissions | -rw-r--r-- |
| 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; |
|
|
14387
e96d5c42c4b0
Polymorphic treatment of binary arithmetic using axclasses
paulson
parents:
13517
diff
changeset
|
16 |
val mk_sum = Int_Numeral_Simprocs.mk_sum HOLogic.intT; |
| 13517 | 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 = |
|
|
14479
0eca4aabf371
streamlined treatment of quotients for the integers
paulson
parents:
14387
diff
changeset
|
27 |
let val simps = diff_int_def :: Int_Numeral_Simprocs.add_0s @ zadd_ac |
| 13517 | 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]; |