src/HOL/Integ/IntDiv_setup.ML
author wenzelm
Sat Jul 08 12:54:30 2006 +0200 (2006-07-08)
changeset 20044 92cc2f4c7335
parent 17609 5156b731ebc8
child 21416 f23e4e75dfd3
permissions -rw-r--r--
simprocs: no theory argument -- use simpset context instead;
nipkow@13517
     1
(*  Title:      HOL/Integ/IntDiv_setup.ML
nipkow@13517
     2
    ID:         $Id$
nipkow@13517
     3
    Author:     Tobias Nipkow, Informatik, TU Muenchen
nipkow@13517
     4
    Copyright   2002  TU Muenchen
nipkow@13517
     5
nipkow@13517
     6
Simproc for cancelling div and mod
nipkow@13517
     7
*)
nipkow@13517
     8
nipkow@13517
     9
nipkow@13517
    10
structure CancelDivModData =
nipkow@13517
    11
struct
nipkow@13517
    12
nipkow@13517
    13
val div_name = "Divides.op div";
nipkow@13517
    14
val mod_name = "Divides.op mod";
nipkow@13517
    15
val mk_binop = HOLogic.mk_binop;
paulson@14387
    16
val mk_sum = Int_Numeral_Simprocs.mk_sum HOLogic.intT;
nipkow@13517
    17
val dest_sum = Int_Numeral_Simprocs.dest_sum;
nipkow@13517
    18
nipkow@13517
    19
(*logic*)
nipkow@13517
    20
nipkow@13517
    21
val div_mod_eqs =
nipkow@13517
    22
  map mk_meta_eq [thm"zdiv_zmod_equality",thm"zdiv_zmod_equality2"]
nipkow@13517
    23
nipkow@13517
    24
val trans = trans
nipkow@13517
    25
nipkow@13517
    26
val prove_eq_sums =
paulson@14479
    27
  let val simps = diff_int_def :: Int_Numeral_Simprocs.add_0s @ zadd_ac
wenzelm@17609
    28
  in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
nipkow@13517
    29
nipkow@13517
    30
end;
nipkow@13517
    31
nipkow@13517
    32
structure CancelDivMod = CancelDivModFun(CancelDivModData);
nipkow@13517
    33
nipkow@13517
    34
val cancel_zdiv_zmod_proc = NatArithUtils.prep_simproc
wenzelm@20044
    35
      ("cancel_zdiv_zmod", ["(m::int) + n"], K CancelDivMod.proc);
nipkow@13517
    36
nipkow@13517
    37
Addsimprocs[cancel_zdiv_zmod_proc];