Added cancel simprocs for dvd on nat and int
authornipkow
Tue Jul 24 19:58:53 2007 +0200 (2007-07-24)
changeset 23969ef782bbf2d09
parent 23968 091abf849a26
child 23970 a252a7da82b9
Added cancel simprocs for dvd on nat and int
src/HOL/IntDiv.thy
src/HOL/NatBin.thy
src/HOL/int_factor_simprocs.ML
src/HOL/nat_simprocs.ML
     1.1 --- a/src/HOL/IntDiv.thy	Tue Jul 24 19:46:44 2007 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Tue Jul 24 19:58:53 2007 +0200
     1.3 @@ -1231,6 +1231,11 @@
     1.4    thus ?thesis by blast
     1.5  qed
     1.6  
     1.7 +lemma zdvd_zmult_cancel_disj[simp]:
     1.8 +  "(k*m) dvd (k*n) = (k=0 | m dvd (n::int))"
     1.9 +by (auto simp: zdvd_zmult_mono dest: zdvd_mult_cancel)
    1.10 +
    1.11 +
    1.12  theorem ex_nat: "(\<exists>x::nat. P x) = (\<exists>x::int. 0 <= x \<and> P (nat x))"
    1.13    apply (simp split add: split_nat)
    1.14    apply (rule iffI)
     2.1 --- a/src/HOL/NatBin.thy	Tue Jul 24 19:46:44 2007 +0200
     2.2 +++ b/src/HOL/NatBin.thy	Tue Jul 24 19:58:53 2007 +0200
     2.3 @@ -811,6 +811,13 @@
     2.4  lemma nat_mult_div_cancel1: "(0::nat) < k ==> (k*m) div (k*n) = (m div n)"
     2.5  by auto
     2.6  
     2.7 +lemma nat_mult_dvd_cancel_disj[simp]:
     2.8 +  "(k*m) dvd (k*n) = (k=0 | m dvd (n::nat))"
     2.9 +by(auto simp: dvd_eq_mod_eq_0 mod_mult_distrib2[symmetric])
    2.10 +
    2.11 +lemma nat_mult_dvd_cancel1: "0 < k \<Longrightarrow> (k*m) dvd (k*n::nat) = (m dvd n)"
    2.12 +by(auto)
    2.13 +
    2.14  
    2.15  subsubsection{*For @{text cancel_factor} *}
    2.16  
    2.17 @@ -823,7 +830,7 @@
    2.18  lemma nat_mult_eq_cancel_disj: "(k*m = k*n) = (k = (0::nat) | m=n)"
    2.19  by auto
    2.20  
    2.21 -lemma nat_mult_div_cancel_disj:
    2.22 +lemma nat_mult_div_cancel_disj[simp]:
    2.23       "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
    2.24  by (simp add: nat_mult_div_cancel1)
    2.25  
     3.1 --- a/src/HOL/int_factor_simprocs.ML	Tue Jul 24 19:46:44 2007 +0200
     3.2 +++ b/src/HOL/int_factor_simprocs.ML	Tue Jul 24 19:58:53 2007 +0200
     3.3 @@ -251,6 +251,14 @@
     3.4    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zdiv_zmult_zmult1_if}
     3.5  );
     3.6  
     3.7 +structure IntDvdCancelFactor = ExtractCommonTermFun
     3.8 + (open CancelFactorCommon
     3.9 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    3.10 +  val mk_bal   = HOLogic.mk_binrel @{const_name Divides.dvd}
    3.11 +  val dest_bal = HOLogic.dest_bin @{const_name Divides.dvd} HOLogic.intT
    3.12 +  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm zdvd_zmult_cancel_disj}
    3.13 +);
    3.14 +
    3.15  (*Version for all fields, including unordered ones (type complex).*)
    3.16  structure DivideCancelFactor = ExtractCommonTermFun
    3.17   (open CancelFactorCommon
    3.18 @@ -269,6 +277,9 @@
    3.19      ("int_div_cancel_factor",
    3.20       ["((l::int) * m) div n", "(l::int) div (m * n)"],
    3.21       K IntDivCancelFactor.proc),
    3.22 +    ("int_dvd_cancel_factor",
    3.23 +     ["((l::int) * m) dvd n", "(l::int) dvd (m * n)"],
    3.24 +     K IntDvdCancelFactor.proc),
    3.25      ("divide_cancel_factor",
    3.26       ["((l::'a::{division_by_zero,field}) * m) / n",
    3.27        "(l::'a::{division_by_zero,field}) / (m * n)"],
     4.1 --- a/src/HOL/nat_simprocs.ML	Tue Jul 24 19:46:44 2007 +0200
     4.2 +++ b/src/HOL/nat_simprocs.ML	Tue Jul 24 19:58:53 2007 +0200
     4.3 @@ -291,6 +291,15 @@
     4.4    val neg_exchanges = false
     4.5  )
     4.6  
     4.7 +structure DvdCancelNumeralFactor = CancelNumeralFactorFun
     4.8 + (open CancelNumeralFactorCommon
     4.9 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    4.10 +  val mk_bal   = HOLogic.mk_binrel @{const_name Divides.dvd}
    4.11 +  val dest_bal = HOLogic.dest_bin @{const_name Divides.dvd} HOLogic.natT
    4.12 +  val cancel = @{thm nat_mult_dvd_cancel1} RS trans
    4.13 +  val neg_exchanges = false
    4.14 +)
    4.15 +
    4.16  structure EqCancelNumeralFactor = CancelNumeralFactorFun
    4.17   (open CancelNumeralFactorCommon
    4.18    val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    4.19 @@ -331,7 +340,10 @@
    4.20       K LeCancelNumeralFactor.proc),
    4.21      ("natdiv_cancel_numeral_factors",
    4.22       ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
    4.23 -     K DivCancelNumeralFactor.proc)];
    4.24 +     K DivCancelNumeralFactor.proc),
    4.25 +    ("natdvd_cancel_numeral_factors",
    4.26 +     ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
    4.27 +     K DvdCancelNumeralFactor.proc)];
    4.28  
    4.29  
    4.30  
    4.31 @@ -399,6 +411,14 @@
    4.32    val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_div_cancel_disj}
    4.33  );
    4.34  
    4.35 +structure DvdCancelFactor = ExtractCommonTermFun
    4.36 + (open CancelFactorCommon
    4.37 +  val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
    4.38 +  val mk_bal   = HOLogic.mk_binrel @{const_name Divides.dvd}
    4.39 +  val dest_bal = HOLogic.dest_bin @{const_name Divides.dvd} HOLogic.natT
    4.40 +  val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_dvd_cancel_disj}
    4.41 +);
    4.42 +
    4.43  val cancel_factor =
    4.44    map prep_simproc
    4.45     [("nat_eq_cancel_factor",
    4.46 @@ -412,7 +432,10 @@
    4.47       K LeCancelFactor.proc),
    4.48      ("nat_divide_cancel_factor",
    4.49       ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
    4.50 -     K DivideCancelFactor.proc)];
    4.51 +     K DivideCancelFactor.proc),
    4.52 +    ("nat_dvd_cancel_factor",
    4.53 +     ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
    4.54 +     K DvdCancelFactor.proc)];
    4.55  
    4.56  end;
    4.57