# HG changeset patch
# User nipkow
# Date 1185299933 -7200
# Node ID ef782bbf2d09f5a5d905d88f04ad94353012ef98
# Parent  091abf849a26878714aa52b84fede82f300a7fb7
Added cancel simprocs for dvd on nat and int

diff -r 091abf849a26 -r ef782bbf2d09 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Tue Jul 24 19:46:44 2007 +0200
+++ b/src/HOL/IntDiv.thy	Tue Jul 24 19:58:53 2007 +0200
@@ -1231,6 +1231,11 @@
   thus ?thesis by blast
 qed
 
+lemma zdvd_zmult_cancel_disj[simp]:
+  "(k*m) dvd (k*n) = (k=0 | m dvd (n::int))"
+by (auto simp: zdvd_zmult_mono dest: zdvd_mult_cancel)
+
+
 theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
   apply (simp split add: split_nat)
   apply (rule iffI)
diff -r 091abf849a26 -r ef782bbf2d09 src/HOL/NatBin.thy
--- a/src/HOL/NatBin.thy	Tue Jul 24 19:46:44 2007 +0200
+++ b/src/HOL/NatBin.thy	Tue Jul 24 19:58:53 2007 +0200
@@ -811,6 +811,13 @@
 lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
 by auto
 
+lemma nat_mult_dvd_cancel_disj[simp]:
+  "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
+by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])
+
+lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
+by(auto)
+
 
 subsubsection{*For @{text cancel_factor} *}
 
@@ -823,7 +830,7 @@
 lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
 by auto
 
-lemma nat_mult_div_cancel_disj:
+lemma nat_mult_div_cancel_disj[simp]:
      "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
 by (simp add: nat_mult_div_cancel1)
 
diff -r 091abf849a26 -r ef782bbf2d09 src/HOL/int_factor_simprocs.ML
--- a/src/HOL/int_factor_simprocs.ML	Tue Jul 24 19:46:44 2007 +0200
+++ b/src/HOL/int_factor_simprocs.ML	Tue Jul 24 19:58:53 2007 +0200
@@ -251,6 +251,14 @@
   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zdiv_zmult_zmult1_if}
 );
 
+structure IntDvdCancelFactor = ExtractCommonTermFun
+ (open CancelFactorCommon
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val mk_bal   = HOLogic.mk_binrel @{const_name Divides.dvd}
+  val dest_bal = HOLogic.dest_bin @{const_name Divides.dvd} HOLogic.intT
+  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zdvd_zmult_cancel_disj}
+);
+
 (*Version for all fields, including unordered ones (type complex).*)
 structure DivideCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
@@ -269,6 +277,9 @@
     ("int_div_cancel_factor",
      ["((l::int) * m) div n", "(l::int) div (m * n)"],
      K IntDivCancelFactor.proc),
+    ("int_dvd_cancel_factor",
+     ["((l::int) * m) dvd n", "(l::int) dvd (m * n)"],
+     K IntDvdCancelFactor.proc),
     ("divide_cancel_factor",
      ["((l::'a::{division_by_zero,field}) * m) / n",
       "(l::'a::{division_by_zero,field}) / (m * n)"],
diff -r 091abf849a26 -r ef782bbf2d09 src/HOL/nat_simprocs.ML
--- a/src/HOL/nat_simprocs.ML	Tue Jul 24 19:46:44 2007 +0200
+++ b/src/HOL/nat_simprocs.ML	Tue Jul 24 19:58:53 2007 +0200
@@ -291,6 +291,15 @@
   val neg_exchanges = false
 )
 
+structure DvdCancelNumeralFactor = CancelNumeralFactorFun
+ (open CancelNumeralFactorCommon
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val mk_bal   = HOLogic.mk_binrel @{const_name Divides.dvd}
+  val dest_bal = HOLogic.dest_bin @{const_name Divides.dvd} HOLogic.natT
+  val cancel = @{thm nat_mult_dvd_cancel1} RS trans
+  val neg_exchanges = false
+)
+
 structure EqCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
@@ -331,7 +340,10 @@
      K LeCancelNumeralFactor.proc),
     ("natdiv_cancel_numeral_factors",
      ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
-     K DivCancelNumeralFactor.proc)];
+     K DivCancelNumeralFactor.proc),
+    ("natdvd_cancel_numeral_factors",
+     ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
+     K DvdCancelNumeralFactor.proc)];
 
 
 
@@ -399,6 +411,14 @@
   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_div_cancel_disj}
 );
 
+structure DvdCancelFactor = ExtractCommonTermFun
+ (open CancelFactorCommon
+  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
+  val mk_bal   = HOLogic.mk_binrel @{const_name Divides.dvd}
+  val dest_bal = HOLogic.dest_bin @{const_name Divides.dvd} HOLogic.natT
+  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_dvd_cancel_disj}
+);
+
 val cancel_factor =
   map prep_simproc
    [("nat_eq_cancel_factor",
@@ -412,7 +432,10 @@
      K LeCancelFactor.proc),
     ("nat_divide_cancel_factor",
      ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
-     K DivideCancelFactor.proc)];
+     K DivideCancelFactor.proc),
+    ("nat_dvd_cancel_factor",
+     ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
+     K DvdCancelFactor.proc)];
 
 end;