use simproc_setup for the remaining nat_numeral simprocs
authorhuffman
Fri Nov 11 11:30:31 2011 +0100 (2011-11-11)
changeset 454639a588a835c1e
parent 45462 aba629d6cee5
child 45464 5a5a6e6c6789
use simproc_setup for the remaining nat_numeral simprocs
src/HOL/Numeral_Simprocs.thy
src/HOL/Tools/nat_numeral_simprocs.ML
src/HOL/ex/Simproc_Tests.thy
     1.1 --- a/src/HOL/Numeral_Simprocs.thy	Fri Nov 11 11:11:03 2011 +0100
     1.2 +++ b/src/HOL/Numeral_Simprocs.thy	Fri Nov 11 11:30:31 2011 +0100
     1.3 @@ -230,6 +230,26 @@
     1.4     "Suc m - n" | "m - Suc n") =
     1.5    {* fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals *}
     1.6  
     1.7 +simproc_setup nat_eq_cancel_numeral_factor
     1.8 +  ("(l::nat) * m = n" | "(l::nat) = m * n") =
     1.9 +  {* fn phi => Nat_Numeral_Simprocs.eq_cancel_numeral_factor *}
    1.10 +
    1.11 +simproc_setup nat_less_cancel_numeral_factor
    1.12 +  ("(l::nat) * m < n" | "(l::nat) < m * n") =
    1.13 +  {* fn phi => Nat_Numeral_Simprocs.less_cancel_numeral_factor *}
    1.14 +
    1.15 +simproc_setup nat_le_cancel_numeral_factor
    1.16 +  ("(l::nat) * m <= n" | "(l::nat) <= m * n") =
    1.17 +  {* fn phi => Nat_Numeral_Simprocs.le_cancel_numeral_factor *}
    1.18 +
    1.19 +simproc_setup nat_div_cancel_numeral_factor
    1.20 +  ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
    1.21 +  {* fn phi => Nat_Numeral_Simprocs.div_cancel_numeral_factor *}
    1.22 +
    1.23 +simproc_setup nat_dvd_cancel_numeral_factor
    1.24 +  ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
    1.25 +  {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_numeral_factor *}
    1.26 +
    1.27  simproc_setup nat_eq_cancel_factor
    1.28    ("(l::nat) * m = n" | "(l::nat) = m * n") =
    1.29    {* fn phi => Nat_Numeral_Simprocs.eq_cancel_factor *}
    1.30 @@ -242,9 +262,9 @@
    1.31    ("(l::nat) * m <= n" | "(l::nat) <= m * n") =
    1.32    {* fn phi => Nat_Numeral_Simprocs.le_cancel_factor *}
    1.33  
    1.34 -simproc_setup nat_divide_cancel_factor
    1.35 +simproc_setup nat_div_cancel_factor
    1.36    ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
    1.37 -  {* fn phi => Nat_Numeral_Simprocs.divide_cancel_factor *}
    1.38 +  {* fn phi => Nat_Numeral_Simprocs.div_cancel_factor *}
    1.39  
    1.40  simproc_setup nat_dvd_cancel_factor
    1.41    ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
     2.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Fri Nov 11 11:11:03 2011 +0100
     2.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Fri Nov 11 11:30:31 2011 +0100
     2.3 @@ -10,12 +10,16 @@
     2.4    val less_cancel_numerals: simpset -> cterm -> thm option
     2.5    val le_cancel_numerals: simpset -> cterm -> thm option
     2.6    val diff_cancel_numerals: simpset -> cterm -> thm option
     2.7 +  val eq_cancel_numeral_factor: simpset -> cterm -> thm option
     2.8 +  val less_cancel_numeral_factor: simpset -> cterm -> thm option
     2.9 +  val le_cancel_numeral_factor: simpset -> cterm -> thm option
    2.10 +  val div_cancel_numeral_factor: simpset -> cterm -> thm option
    2.11 +  val dvd_cancel_numeral_factor: simpset -> cterm -> thm option
    2.12    val eq_cancel_factor: simpset -> cterm -> thm option
    2.13    val less_cancel_factor: simpset -> cterm -> thm option
    2.14    val le_cancel_factor: simpset -> cterm -> thm option
    2.15 -  val divide_cancel_factor: simpset -> cterm -> thm option
    2.16 +  val div_cancel_factor: simpset -> cterm -> thm option
    2.17    val dvd_cancel_factor: simpset -> cterm -> thm option
    2.18 -  val cancel_numeral_factors: simproc list
    2.19  end;
    2.20  
    2.21  structure Nat_Numeral_Simprocs : NAT_NUMERAL_SIMPROCS =
    2.22 @@ -300,24 +304,11 @@
    2.23    val neg_exchanges = true
    2.24  )
    2.25  
    2.26 -val cancel_numeral_factors =
    2.27 -  map (Numeral_Simprocs.prep_simproc @{theory})
    2.28 -   [("nateq_cancel_numeral_factors",
    2.29 -     ["(l::nat) * m = n", "(l::nat) = m * n"],
    2.30 -     K EqCancelNumeralFactor.proc),
    2.31 -    ("natless_cancel_numeral_factors",
    2.32 -     ["(l::nat) * m < n", "(l::nat) < m * n"],
    2.33 -     K LessCancelNumeralFactor.proc),
    2.34 -    ("natle_cancel_numeral_factors",
    2.35 -     ["(l::nat) * m <= n", "(l::nat) <= m * n"],
    2.36 -     K LeCancelNumeralFactor.proc),
    2.37 -    ("natdiv_cancel_numeral_factors",
    2.38 -     ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
    2.39 -     K DivCancelNumeralFactor.proc),
    2.40 -    ("natdvd_cancel_numeral_factors",
    2.41 -     ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
    2.42 -     K DvdCancelNumeralFactor.proc)];
    2.43 -
    2.44 +fun eq_cancel_numeral_factor ss ct = EqCancelNumeralFactor.proc ss (term_of ct)
    2.45 +fun less_cancel_numeral_factor ss ct = LessCancelNumeralFactor.proc ss (term_of ct)
    2.46 +fun le_cancel_numeral_factor ss ct = LeCancelNumeralFactor.proc ss (term_of ct)
    2.47 +fun div_cancel_numeral_factor ss ct = DivCancelNumeralFactor.proc ss (term_of ct)
    2.48 +fun dvd_cancel_numeral_factor ss ct = DvdCancelNumeralFactor.proc ss (term_of ct)
    2.49  
    2.50  
    2.51  (*** Applying ExtractCommonTermFun ***)
    2.52 @@ -392,25 +383,7 @@
    2.53  fun eq_cancel_factor ss ct = EqCancelFactor.proc ss (term_of ct)
    2.54  fun less_cancel_factor ss ct = LessCancelFactor.proc ss (term_of ct)
    2.55  fun le_cancel_factor ss ct = LeCancelFactor.proc ss (term_of ct)
    2.56 -fun divide_cancel_factor ss ct = DivideCancelFactor.proc ss (term_of ct)
    2.57 +fun div_cancel_factor ss ct = DivideCancelFactor.proc ss (term_of ct)
    2.58  fun dvd_cancel_factor ss ct = DvdCancelFactor.proc ss (term_of ct)
    2.59  
    2.60  end;
    2.61 -
    2.62 -
    2.63 -Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors;
    2.64 -
    2.65 -
    2.66 -(*examples:
    2.67 -print_depth 22;
    2.68 -set timing;
    2.69 -set simp_trace;
    2.70 -fun test s = (Goal s; by (Simp_tac 1));
    2.71 -
    2.72 -(*cancel_numeral_factors*)
    2.73 -test "9*x = 12 * (y::nat)";
    2.74 -test "(9*x) div (12 * (y::nat)) = z";
    2.75 -test "9*x < 12 * (y::nat)";
    2.76 -test "9*x <= 12 * (y::nat)";
    2.77 -
    2.78 -*)
     3.1 --- a/src/HOL/ex/Simproc_Tests.thy	Fri Nov 11 11:11:03 2011 +0100
     3.2 +++ b/src/HOL/ex/Simproc_Tests.thy	Fri Nov 11 11:30:31 2011 +0100
     3.3 @@ -640,17 +640,17 @@
     3.4        by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
     3.5    next
     3.6      assume "(if k = 0 then 0 else x div y) = uu" have "(x*k) div (k*y) = uu"
     3.7 -      by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact
     3.8 +      by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
     3.9    next
    3.10      assume "(if k = 0 then 0 else Suc 0 div y) = uu" have "k div (k*y) = uu"
    3.11 -      by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact
    3.12 +      by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
    3.13    next
    3.14      assume "(if b = 0 then 0 else a * c) = uu" have "(a*(b*c)) div (b) = uu"
    3.15 -      by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact
    3.16 +      by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
    3.17    next
    3.18      assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
    3.19      have "(a*(b*c)) div (d*b*(x*a)) = uu"
    3.20 -      by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact
    3.21 +      by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
    3.22    next
    3.23      assume "k = 0 \<or> x dvd y" have "(x*k) dvd (k*y)"
    3.24        by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
    3.25 @@ -669,4 +669,26 @@
    3.26    }
    3.27  end
    3.28  
    3.29 +subsection {* Numeral-cancellation simprocs for type @{typ nat} *}
    3.30 +
    3.31 +notepad begin
    3.32 +  fix x y z :: nat
    3.33 +  {
    3.34 +    assume "3 * x = 4 * y" have "9*x = 12 * y"
    3.35 +      by (tactic {* test [@{simproc nat_eq_cancel_numeral_factor}] *}) fact
    3.36 +  next
    3.37 +    assume "3 * x < 4 * y" have "9*x < 12 * y"
    3.38 +      by (tactic {* test [@{simproc nat_less_cancel_numeral_factor}] *}) fact
    3.39 +  next
    3.40 +    assume "3 * x \<le> 4 * y" have "9*x \<le> 12 * y"
    3.41 +      by (tactic {* test [@{simproc nat_le_cancel_numeral_factor}] *}) fact
    3.42 +  next
    3.43 +    assume "(3 * x) div (4 * y) = z" have "(9*x) div (12 * y) = z"
    3.44 +      by (tactic {* test [@{simproc nat_div_cancel_numeral_factor}] *}) fact
    3.45 +  next
    3.46 +    assume "(3 * x) dvd (4 * y)" have "(9*x) dvd (12 * y)"
    3.47 +      by (tactic {* test [@{simproc nat_dvd_cancel_numeral_factor}] *}) fact
    3.48 +  }
    3.49  end
    3.50 +
    3.51 +end