# HG changeset patch
# User huffman
# Date 1321007431 -3600
# Node ID 9a588a835c1e83dd0aef9228e9b972c33a7a8ffa
# Parent  aba629d6cee50b0c91386ae67f82dbe51ac4ea0a
use simproc_setup for the remaining nat_numeral simprocs

diff -r aba629d6cee5 -r 9a588a835c1e src/HOL/Numeral_Simprocs.thy
--- a/src/HOL/Numeral_Simprocs.thy	Fri Nov 11 11:11:03 2011 +0100
+++ b/src/HOL/Numeral_Simprocs.thy	Fri Nov 11 11:30:31 2011 +0100
@@ -230,6 +230,26 @@
    "Suc m - n" | "m - Suc n") =
   {* fn phi => Nat_Numeral_Simprocs.diff_cancel_numerals *}
 
+simproc_setup nat_eq_cancel_numeral_factor
+  ("(l::nat) * m = n" | "(l::nat) = m * n") =
+  {* fn phi => Nat_Numeral_Simprocs.eq_cancel_numeral_factor *}
+
+simproc_setup nat_less_cancel_numeral_factor
+  ("(l::nat) * m < n" | "(l::nat) < m * n") =
+  {* fn phi => Nat_Numeral_Simprocs.less_cancel_numeral_factor *}
+
+simproc_setup nat_le_cancel_numeral_factor
+  ("(l::nat) * m <= n" | "(l::nat) <= m * n") =
+  {* fn phi => Nat_Numeral_Simprocs.le_cancel_numeral_factor *}
+
+simproc_setup nat_div_cancel_numeral_factor
+  ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
+  {* fn phi => Nat_Numeral_Simprocs.div_cancel_numeral_factor *}
+
+simproc_setup nat_dvd_cancel_numeral_factor
+  ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
+  {* fn phi => Nat_Numeral_Simprocs.dvd_cancel_numeral_factor *}
+
 simproc_setup nat_eq_cancel_factor
   ("(l::nat) * m = n" | "(l::nat) = m * n") =
   {* fn phi => Nat_Numeral_Simprocs.eq_cancel_factor *}
@@ -242,9 +262,9 @@
   ("(l::nat) * m <= n" | "(l::nat) <= m * n") =
   {* fn phi => Nat_Numeral_Simprocs.le_cancel_factor *}
 
-simproc_setup nat_divide_cancel_factor
+simproc_setup nat_div_cancel_factor
   ("((l::nat) * m) div n" | "(l::nat) div (m * n)") =
-  {* fn phi => Nat_Numeral_Simprocs.divide_cancel_factor *}
+  {* fn phi => Nat_Numeral_Simprocs.div_cancel_factor *}
 
 simproc_setup nat_dvd_cancel_factor
   ("((l::nat) * m) dvd n" | "(l::nat) dvd (m * n)") =
diff -r aba629d6cee5 -r 9a588a835c1e src/HOL/Tools/nat_numeral_simprocs.ML
--- a/src/HOL/Tools/nat_numeral_simprocs.ML	Fri Nov 11 11:11:03 2011 +0100
+++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Fri Nov 11 11:30:31 2011 +0100
@@ -10,12 +10,16 @@
   val less_cancel_numerals: simpset -> cterm -> thm option
   val le_cancel_numerals: simpset -> cterm -> thm option
   val diff_cancel_numerals: simpset -> cterm -> thm option
+  val eq_cancel_numeral_factor: simpset -> cterm -> thm option
+  val less_cancel_numeral_factor: simpset -> cterm -> thm option
+  val le_cancel_numeral_factor: simpset -> cterm -> thm option
+  val div_cancel_numeral_factor: simpset -> cterm -> thm option
+  val dvd_cancel_numeral_factor: simpset -> cterm -> thm option
   val eq_cancel_factor: simpset -> cterm -> thm option
   val less_cancel_factor: simpset -> cterm -> thm option
   val le_cancel_factor: simpset -> cterm -> thm option
-  val divide_cancel_factor: simpset -> cterm -> thm option
+  val div_cancel_factor: simpset -> cterm -> thm option
   val dvd_cancel_factor: simpset -> cterm -> thm option
-  val cancel_numeral_factors: simproc list
 end;
 
 structure Nat_Numeral_Simprocs : NAT_NUMERAL_SIMPROCS =
@@ -300,24 +304,11 @@
   val neg_exchanges = true
 )
 
-val cancel_numeral_factors =
-  map (Numeral_Simprocs.prep_simproc @{theory})
-   [("nateq_cancel_numeral_factors",
-     ["(l::nat) * m = n", "(l::nat) = m * n"],
-     K EqCancelNumeralFactor.proc),
-    ("natless_cancel_numeral_factors",
-     ["(l::nat) * m < n", "(l::nat) < m * n"],
-     K LessCancelNumeralFactor.proc),
-    ("natle_cancel_numeral_factors",
-     ["(l::nat) * m <= n", "(l::nat) <= m * n"],
-     K LeCancelNumeralFactor.proc),
-    ("natdiv_cancel_numeral_factors",
-     ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
-     K DivCancelNumeralFactor.proc),
-    ("natdvd_cancel_numeral_factors",
-     ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
-     K DvdCancelNumeralFactor.proc)];
-
+fun eq_cancel_numeral_factor ss ct = EqCancelNumeralFactor.proc ss (term_of ct)
+fun less_cancel_numeral_factor ss ct = LessCancelNumeralFactor.proc ss (term_of ct)
+fun le_cancel_numeral_factor ss ct = LeCancelNumeralFactor.proc ss (term_of ct)
+fun div_cancel_numeral_factor ss ct = DivCancelNumeralFactor.proc ss (term_of ct)
+fun dvd_cancel_numeral_factor ss ct = DvdCancelNumeralFactor.proc ss (term_of ct)
 
 
 (*** Applying ExtractCommonTermFun ***)
@@ -392,25 +383,7 @@
 fun eq_cancel_factor ss ct = EqCancelFactor.proc ss (term_of ct)
 fun less_cancel_factor ss ct = LessCancelFactor.proc ss (term_of ct)
 fun le_cancel_factor ss ct = LeCancelFactor.proc ss (term_of ct)
-fun divide_cancel_factor ss ct = DivideCancelFactor.proc ss (term_of ct)
+fun div_cancel_factor ss ct = DivideCancelFactor.proc ss (term_of ct)
 fun dvd_cancel_factor ss ct = DvdCancelFactor.proc ss (term_of ct)
 
 end;
-
-
-Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors;
-
-
-(*examples:
-print_depth 22;
-set timing;
-set simp_trace;
-fun test s = (Goal s; by (Simp_tac 1));
-
-(*cancel_numeral_factors*)
-test "9*x = 12 * (y::nat)";
-test "(9*x) div (12 * (y::nat)) = z";
-test "9*x < 12 * (y::nat)";
-test "9*x <= 12 * (y::nat)";
-
-*)
diff -r aba629d6cee5 -r 9a588a835c1e src/HOL/ex/Simproc_Tests.thy
--- a/src/HOL/ex/Simproc_Tests.thy	Fri Nov 11 11:11:03 2011 +0100
+++ b/src/HOL/ex/Simproc_Tests.thy	Fri Nov 11 11:30:31 2011 +0100
@@ -640,17 +640,17 @@
       by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
   next
     assume "(if k = 0 then 0 else x div y) = uu" have "(x*k) div (k*y) = uu"
-      by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact
+      by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
   next
     assume "(if k = 0 then 0 else Suc 0 div y) = uu" have "k div (k*y) = uu"
-      by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact
+      by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
   next
     assume "(if b = 0 then 0 else a * c) = uu" have "(a*(b*c)) div (b) = uu"
-      by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact
+      by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
   next
     assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
     have "(a*(b*c)) div (d*b*(x*a)) = uu"
-      by (tactic {* test [@{simproc nat_divide_cancel_factor}] *}) fact
+      by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
   next
     assume "k = 0 \<or> x dvd y" have "(x*k) dvd (k*y)"
       by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
@@ -669,4 +669,26 @@
   }
 end
 
+subsection {* Numeral-cancellation simprocs for type @{typ nat} *}
+
+notepad begin
+  fix x y z :: nat
+  {
+    assume "3 * x = 4 * y" have "9*x = 12 * y"
+      by (tactic {* test [@{simproc nat_eq_cancel_numeral_factor}] *}) fact
+  next
+    assume "3 * x < 4 * y" have "9*x < 12 * y"
+      by (tactic {* test [@{simproc nat_less_cancel_numeral_factor}] *}) fact
+  next
+    assume "3 * x \<le> 4 * y" have "9*x \<le> 12 * y"
+      by (tactic {* test [@{simproc nat_le_cancel_numeral_factor}] *}) fact
+  next
+    assume "(3 * x) div (4 * y) = z" have "(9*x) div (12 * y) = z"
+      by (tactic {* test [@{simproc nat_div_cancel_numeral_factor}] *}) fact
+  next
+    assume "(3 * x) dvd (4 * y)" have "(9*x) dvd (12 * y)"
+      by (tactic {* test [@{simproc nat_dvd_cancel_numeral_factor}] *}) fact
+  }
 end
+
+end