src/HOL/Integ/IntDiv_setup.ML
author nipkow
Fri Aug 23 07:41:05 2002 +0200 (2002-08-23)
changeset 13517 42efec18f5b2
child 14387 e96d5c42c4b0
permissions -rw-r--r--
Added div+mod cancelling simproc
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;
nipkow@13517
    16
val mk_sum = Int_Numeral_Simprocs.mk_sum;
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 =
nipkow@13517
    27
  let val simps = zdiff_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];