generalize int_dvd_cancel_factor simproc to idom class
authorhuffman
Wed Feb 18 15:01:53 2009 -0800 (2009-02-18)
changeset 299817d0ed261b712
parent 29980 17ddfd0c3506
child 29982 6ec97eba1ee3
generalize int_dvd_cancel_factor simproc to idom class
src/HOL/IntDiv.thy
src/HOL/Ring_and_Field.thy
src/HOL/Tools/int_factor_simprocs.ML
     1.1 --- a/src/HOL/IntDiv.thy	Wed Feb 18 14:17:04 2009 -0800
     1.2 +++ b/src/HOL/IntDiv.thy	Wed Feb 18 15:01:53 2009 -0800
     1.3 @@ -1265,9 +1265,9 @@
     1.4    thus ?thesis by simp
     1.5  qed
     1.6  
     1.7 -lemma zdvd_zmult_cancel_disj[simp]:
     1.8 +lemma zdvd_zmult_cancel_disj:
     1.9    "(k*m) dvd (k*n) = (k=0 | m dvd (n::int))"
    1.10 -by (auto simp: zdvd_zmult_mono dest: zdvd_mult_cancel)
    1.11 +by (rule dvd_mult_cancel_left) (* already declared [simp] *)
    1.12  
    1.13  
    1.14  theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
     2.1 --- a/src/HOL/Ring_and_Field.thy	Wed Feb 18 14:17:04 2009 -0800
     2.2 +++ b/src/HOL/Ring_and_Field.thy	Wed Feb 18 15:01:53 2009 -0800
     2.3 @@ -384,6 +384,26 @@
     2.4    then show "a * a = b * b" by auto
     2.5  qed
     2.6  
     2.7 +lemma dvd_mult_cancel_right [simp]:
     2.8 +  "a * c dvd b * c \<longleftrightarrow> c = 0 \<or> a dvd b"
     2.9 +proof -
    2.10 +  have "a * c dvd b * c \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
    2.11 +    unfolding dvd_def by (simp add: mult_ac)
    2.12 +  also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
    2.13 +    unfolding dvd_def by simp
    2.14 +  finally show ?thesis .
    2.15 +qed
    2.16 +
    2.17 +lemma dvd_mult_cancel_left [simp]:
    2.18 +  "c * a dvd c * b \<longleftrightarrow> c = 0 \<or> a dvd b"
    2.19 +proof -
    2.20 +  have "c * a dvd c * b \<longleftrightarrow> (\<exists>k. b * c = (a * k) * c)"
    2.21 +    unfolding dvd_def by (simp add: mult_ac)
    2.22 +  also have "(\<exists>k. b * c = (a * k) * c) \<longleftrightarrow> c = 0 \<or> a dvd b"
    2.23 +    unfolding dvd_def by simp
    2.24 +  finally show ?thesis .
    2.25 +qed
    2.26 +
    2.27  end
    2.28  
    2.29  class division_ring = ring_1 + inverse +
     3.1 --- a/src/HOL/Tools/int_factor_simprocs.ML	Wed Feb 18 14:17:04 2009 -0800
     3.2 +++ b/src/HOL/Tools/int_factor_simprocs.ML	Wed Feb 18 15:01:53 2009 -0800
     3.3 @@ -263,8 +263,8 @@
     3.4   (open CancelFactorCommon
     3.5    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
     3.6    val mk_bal   = HOLogic.mk_binrel @{const_name Ring_and_Field.dvd}
     3.7 -  val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} HOLogic.intT
     3.8 -  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zdvd_zmult_cancel_disj}
     3.9 +  val dest_bal = HOLogic.dest_bin @{const_name Ring_and_Field.dvd} Term.dummyT
    3.10 +  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm dvd_mult_cancel_left}
    3.11  );
    3.12  
    3.13  (*Version for all fields, including unordered ones (type complex).*)
    3.14 @@ -288,8 +288,8 @@
    3.15      ("int_mod_cancel_factor",
    3.16       ["((l::int) * m) mod n", "(l::int) mod (m * n)"],
    3.17       K IntModCancelFactor.proc),
    3.18 -    ("int_dvd_cancel_factor",
    3.19 -     ["((l::int) * m) dvd n", "(l::int) dvd (m * n)"],
    3.20 +    ("dvd_cancel_factor",
    3.21 +     ["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"],
    3.22       K IntDvdCancelFactor.proc),
    3.23      ("divide_cancel_factor",
    3.24       ["((l::'a::{division_by_zero,field}) * m) / n",