src/HOL/nat_simprocs.ML
changeset 23969 ef782bbf2d09
parent 23881 851c74f1bb69
child 24093 5d0ecd0c8f3c
     1.1 --- a/src/HOL/nat_simprocs.ML	Tue Jul 24 19:46:44 2007 +0200
     1.2 +++ b/src/HOL/nat_simprocs.ML	Tue Jul 24 19:58:53 2007 +0200
     1.3 @@ -291,6 +291,15 @@
     1.4    val neg_exchanges = false
     1.5  )
     1.6  
     1.7 +structure DvdCancelNumeralFactor = CancelNumeralFactorFun
     1.8 + (open CancelNumeralFactorCommon
     1.9 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    1.10 +  val mk_bal   = HOLogic.mk_binrel @{const_name Divides.dvd}
    1.11 +  val dest_bal = HOLogic.dest_bin @{const_name Divides.dvd} HOLogic.natT
    1.12 +  val cancel = @{thm nat_mult_dvd_cancel1} RS trans
    1.13 +  val neg_exchanges = false
    1.14 +)
    1.15 +
    1.16  structure EqCancelNumeralFactor = CancelNumeralFactorFun
    1.17   (open CancelNumeralFactorCommon
    1.18    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    1.19 @@ -331,7 +340,10 @@
    1.20       K LeCancelNumeralFactor.proc),
    1.21      ("natdiv_cancel_numeral_factors",
    1.22       ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
    1.23 -     K DivCancelNumeralFactor.proc)];
    1.24 +     K DivCancelNumeralFactor.proc),
    1.25 +    ("natdvd_cancel_numeral_factors",
    1.26 +     ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
    1.27 +     K DvdCancelNumeralFactor.proc)];
    1.28  
    1.29  
    1.30  
    1.31 @@ -399,6 +411,14 @@
    1.32    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_div_cancel_disj}
    1.33  );
    1.34  
    1.35 +structure DvdCancelFactor = ExtractCommonTermFun
    1.36 + (open CancelFactorCommon
    1.37 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    1.38 +  val mk_bal   = HOLogic.mk_binrel @{const_name Divides.dvd}
    1.39 +  val dest_bal = HOLogic.dest_bin @{const_name Divides.dvd} HOLogic.natT
    1.40 +  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_dvd_cancel_disj}
    1.41 +);
    1.42 +
    1.43  val cancel_factor =
    1.44    map prep_simproc
    1.45     [("nat_eq_cancel_factor",
    1.46 @@ -412,7 +432,10 @@
    1.47       K LeCancelFactor.proc),
    1.48      ("nat_divide_cancel_factor",
    1.49       ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
    1.50 -     K DivideCancelFactor.proc)];
    1.51 +     K DivideCancelFactor.proc),
    1.52 +    ("nat_dvd_cancel_factor",
    1.53 +     ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
    1.54 +     K DvdCancelFactor.proc)];
    1.55  
    1.56  end;
    1.57