src/HOL/Integ/IntDiv_setup.ML
author paulson
Sun Feb 15 10:46:37 2004 +0100 (2004-02-15)
changeset 14387 e96d5c42c4b0
parent 13517 42efec18f5b2
child 14479 0eca4aabf371
permissions -rw-r--r--
Polymorphic treatment of binary arithmetic using axclasses
     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 = 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];