src/HOL/Integ/IntDiv_setup.ML
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 14479 0eca4aabf371
child 17609 5156b731ebc8
permissions -rw-r--r--
Constant "If" is now local
     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 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];