src/HOL/Integ/IntDiv_setup.ML
author haftmann
Mon Jan 30 08:20:56 2006 +0100 (2006-01-30)
changeset 18851 9502ce541f01
parent 17609 5156b731ebc8
child 20044 92cc2f4c7335
permissions -rw-r--r--
adaptions to codegen_package
     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 HOLogic.intT;
    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 = diff_int_def :: Int_Numeral_Simprocs.add_0s @ zadd_ac
    28   in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac 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];