src/HOL/Integ/IntDiv_setup.ML
author paulson
Wed Mar 24 10:50:29 2004 +0100 (2004-03-24)
changeset 14479 0eca4aabf371
parent 14387 e96d5c42c4b0
child 17609 5156b731ebc8
permissions -rw-r--r--
streamlined treatment of quotients for the integers
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
nipkow@13517
    28
  in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all 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
nipkow@13517
    35
      ("cancel_zdiv_zmod", ["(m::int) + n"], CancelDivMod.proc);
nipkow@13517
    36
nipkow@13517
    37
Addsimprocs[cancel_zdiv_zmod_proc];