# HG changeset patch
# User huffman
# Date 1234998113 28800
# Node ID 7d0ed261b7127fc91ca0a3bd879ea77a5bc52fb9
# Parent  17ddfd0c350697fed49c0dc571fbc635849d4fed
generalize int_dvd_cancel_factor simproc to idom class

diff -r 17ddfd0c3506 -r 7d0ed261b712 src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Wed Feb 18 14:17:04 2009 -0800
+++ b/src/HOL/IntDiv.thy	Wed Feb 18 15:01:53 2009 -0800
@@ -1265,9 +1265,9 @@
   thus ?thesis by simp
 qed
 
-lemma zdvd_zmult_cancel_disj[simp]:
+lemma zdvd_zmult_cancel_disj:
   "(k*m) dvd (k*n) = (k=0 | m dvd (n::int))"
-by (auto simp: zdvd_zmult_mono dest: zdvd_mult_cancel)
+by (rule dvd_mult_cancel_left) (* already declared [simp] *)
 
 
 theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
diff -r 17ddfd0c3506 -r 7d0ed261b712 src/HOL/Ring_and_Field.thy
--- a/src/HOL/Ring_and_Field.thy	Wed Feb 18 14:17:04 2009 -0800
+++ b/src/HOL/Ring_and_Field.thy	Wed Feb 18 15:01:53 2009 -0800
@@ -384,6 +384,26 @@
   then show "a * a = b * b" by auto
 qed
 
+lemma dvd_mult_cancel_right [simp]:
+  "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
+proof -
+  have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
+    unfolding dvd_def by (simp add: mult_ac)
+  also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
+    unfolding dvd_def by simp
+  finally show ?thesis .
+qed
+
+lemma dvd_mult_cancel_left [simp]:
+  "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
+proof -
+  have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
+    unfolding dvd_def by (simp add: mult_ac)
+  also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
+    unfolding dvd_def by simp
+  finally show ?thesis .
+qed
+
 end
 
 class division_ring = ring_1 + inverse +
diff -r 17ddfd0c3506 -r 7d0ed261b712 src/HOL/Tools/int_factor_simprocs.ML
--- a/src/HOL/Tools/int_factor_simprocs.ML	Wed Feb 18 14:17:04 2009 -0800
+++ b/src/HOL/Tools/int_factor_simprocs.ML	Wed Feb 18 15:01:53 2009 -0800
@@ -263,8 +263,8 @@
  (open CancelFactorCommon
   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
-  val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.intT
-  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zdvd_zmult_cancel_disj}
+  val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT
+  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm dvd_mult_cancel_left}
 );
 
 (*Version for all fields, including unordered ones (type complex).*)
@@ -288,8 +288,8 @@
     ("int_mod_cancel_factor",
      ["((l::int) * m) mod n", "(l::int) mod (m * n)"],
      K IntModCancelFactor.proc),
-    ("int_dvd_cancel_factor",
-     ["((l::int) * m) dvd n", "(l::int) dvd (m * n)"],
+    ("dvd_cancel_factor",
+     ["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"],
      K IntDvdCancelFactor.proc),
     ("divide_cancel_factor",
      ["((l::'a::{division_by_zero,field}) * m) / n",