# HG changeset patch
# User huffman
# Date 1319792547 -7200
# Node ID ae78a4ffa81dcd30154eaed5090c4df6c760a98a
# Parent  9e8616978d9956d9150cd0440b0fb2f3e47f6d8e
use simproc_setup for cancellation simprocs, to get proper name bindings

diff -r 9e8616978d99 -r ae78a4ffa81d src/HOL/Numeral_Simprocs.thy
--- a/src/HOL/Numeral_Simprocs.thy	Thu Oct 27 22:37:19 2011 +0200
+++ b/src/HOL/Numeral_Simprocs.thy	Fri Oct 28 11:02:27 2011 +0200
@@ -94,6 +94,106 @@
 
 use "Tools/numeral_simprocs.ML"
 
+simproc_setup semiring_assoc_fold
+  ("(a::'a::comm_semiring_1_cancel) * b") =
+  {* fn phi => Numeral_Simprocs.assoc_fold *}
+
+simproc_setup int_combine_numerals
+  ("(i::'a::number_ring) + j" | "(i::'a::number_ring) - j") =
+  {* fn phi => Numeral_Simprocs.combine_numerals *}
+
+simproc_setup field_combine_numerals
+  ("(i::'a::{field_inverse_zero, number_ring}) + j"
+  |"(i::'a::{field_inverse_zero, number_ring}) - j") =
+  {* fn phi => Numeral_Simprocs.field_combine_numerals *}
+
+simproc_setup inteq_cancel_numerals
+  ("(l::'a::number_ring) + m = n"
+  |"(l::'a::number_ring) = m + n"
+  |"(l::'a::number_ring) - m = n"
+  |"(l::'a::number_ring) = m - n"
+  |"(l::'a::number_ring) * m = n"
+  |"(l::'a::number_ring) = m * n") =
+  {* fn phi => Numeral_Simprocs.eq_cancel_numerals *}
+
+simproc_setup intless_cancel_numerals
+  ("(l::'a::{linordered_idom,number_ring}) + m < n"
+  |"(l::'a::{linordered_idom,number_ring}) < m + n"
+  |"(l::'a::{linordered_idom,number_ring}) - m < n"
+  |"(l::'a::{linordered_idom,number_ring}) < m - n"
+  |"(l::'a::{linordered_idom,number_ring}) * m < n"
+  |"(l::'a::{linordered_idom,number_ring}) < m * n") =
+  {* fn phi => Numeral_Simprocs.less_cancel_numerals *}
+
+simproc_setup intle_cancel_numerals
+  ("(l::'a::{linordered_idom,number_ring}) + m \<le> n"
+  |"(l::'a::{linordered_idom,number_ring}) \<le> m + n"
+  |"(l::'a::{linordered_idom,number_ring}) - m \<le> n"
+  |"(l::'a::{linordered_idom,number_ring}) \<le> m - n"
+  |"(l::'a::{linordered_idom,number_ring}) * m \<le> n"
+  |"(l::'a::{linordered_idom,number_ring}) \<le> m * n") =
+  {* fn phi => Numeral_Simprocs.le_cancel_numerals *}
+
+simproc_setup ring_eq_cancel_numeral_factor
+  ("(l::'a::{idom,number_ring}) * m = n"
+  |"(l::'a::{idom,number_ring}) = m * n") =
+  {* fn phi => Numeral_Simprocs.eq_cancel_numeral_factor *}
+
+simproc_setup ring_less_cancel_numeral_factor
+  ("(l::'a::{linordered_idom,number_ring}) * m < n"
+  |"(l::'a::{linordered_idom,number_ring}) < m * n") =
+  {* fn phi => Numeral_Simprocs.less_cancel_numeral_factor *}
+
+simproc_setup ring_le_cancel_numeral_factor
+  ("(l::'a::{linordered_idom,number_ring}) * m <= n"
+  |"(l::'a::{linordered_idom,number_ring}) <= m * n") =
+  {* fn phi => Numeral_Simprocs.le_cancel_numeral_factor *}
+
+simproc_setup int_div_cancel_numeral_factors
+  ("((l::'a::{semiring_div,number_ring}) * m) div n"
+  |"(l::'a::{semiring_div,number_ring}) div (m * n)") =
+  {* fn phi => Numeral_Simprocs.div_cancel_numeral_factor *}
+
+simproc_setup divide_cancel_numeral_factor
+  ("((l::'a::{field_inverse_zero,number_ring}) * m) / n"
+  |"(l::'a::{field_inverse_zero,number_ring}) / (m * n)"
+  |"((number_of v)::'a::{field_inverse_zero,number_ring}) / (number_of w)") =
+  {* fn phi => Numeral_Simprocs.divide_cancel_numeral_factor *}
+
+simproc_setup ring_eq_cancel_factor
+  ("(l::'a::idom) * m = n" | "(l::'a::idom) = m * n") =
+  {* fn phi => Numeral_Simprocs.eq_cancel_factor *}
+
+simproc_setup linordered_ring_le_cancel_factor
+  ("(l::'a::linordered_ring) * m <= n"
+  |"(l::'a::linordered_ring) <= m * n") =
+  {* fn phi => Numeral_Simprocs.le_cancel_factor *}
+
+simproc_setup linordered_ring_less_cancel_factor
+  ("(l::'a::linordered_ring) * m < n"
+  |"(l::'a::linordered_ring) < m * n") =
+  {* fn phi => Numeral_Simprocs.less_cancel_factor *}
+
+simproc_setup int_div_cancel_factor
+  ("((l::'a::semiring_div) * m) div n"
+  |"(l::'a::semiring_div) div (m * n)") =
+  {* fn phi => Numeral_Simprocs.div_cancel_factor *}
+
+simproc_setup int_mod_cancel_factor
+  ("((l::'a::semiring_div) * m) mod n"
+  |"(l::'a::semiring_div) mod (m * n)") =
+  {* fn phi => Numeral_Simprocs.mod_cancel_factor *}
+
+simproc_setup dvd_cancel_factor
+  ("((l::'a::idom) * m) dvd n"
+  |"(l::'a::idom) dvd (m * n)") =
+  {* fn phi => Numeral_Simprocs.dvd_cancel_factor *}
+
+simproc_setup divide_cancel_factor
+  ("((l::'a::field_inverse_zero) * m) / n"
+  |"(l::'a::field_inverse_zero) / (m * n)") =
+  {* fn phi => Numeral_Simprocs.divide_cancel_factor *}
+
 use "Tools/nat_numeral_simprocs.ML"
 
 declaration {* 
@@ -110,9 +210,12 @@
      @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
      @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},
      @{thm if_True}, @{thm if_False}])
-  #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc
-      :: Numeral_Simprocs.combine_numerals
-      :: Numeral_Simprocs.cancel_numerals)
+  #> Lin_Arith.add_simprocs
+      [@{simproc semiring_assoc_fold},
+       @{simproc int_combine_numerals},
+       @{simproc inteq_cancel_numerals},
+       @{simproc intless_cancel_numerals},
+       @{simproc intle_cancel_numerals}]
   #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
 *}
 
diff -r 9e8616978d99 -r ae78a4ffa81d src/HOL/Tools/numeral_simprocs.ML
--- a/src/HOL/Tools/numeral_simprocs.ML	Thu Oct 27 22:37:19 2011 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Fri Oct 28 11:02:27 2011 +0200
@@ -19,12 +19,24 @@
   val prep_simproc: theory -> string * string list * (theory -> simpset -> term -> thm option)
     -> simproc
   val trans_tac: thm option -> tactic
-  val assoc_fold_simproc: simproc
-  val combine_numerals: simproc
-  val cancel_numerals: simproc list
-  val cancel_factors: simproc list
-  val cancel_numeral_factors: simproc list
-  val field_combine_numerals: simproc
+  val assoc_fold: simpset -> cterm -> thm option
+  val combine_numerals: simpset -> cterm -> thm option
+  val eq_cancel_numerals: simpset -> cterm -> thm option
+  val less_cancel_numerals: simpset -> cterm -> thm option
+  val le_cancel_numerals: simpset -> cterm -> thm option
+  val eq_cancel_factor: simpset -> cterm -> thm option
+  val le_cancel_factor: simpset -> cterm -> thm option
+  val less_cancel_factor: simpset -> cterm -> thm option
+  val div_cancel_factor: simpset -> cterm -> thm option
+  val mod_cancel_factor: simpset -> cterm -> thm option
+  val dvd_cancel_factor: simpset -> cterm -> thm option
+  val divide_cancel_factor: 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 divide_cancel_numeral_factor: simpset -> cterm -> thm option
+  val field_combine_numerals: simpset -> cterm -> thm option
   val field_cancel_numeral_factors: simproc list
   val num_ss: simpset
   val field_comp_conv: conv
@@ -251,32 +263,9 @@
   val bal_add2 = @{thm le_add_iff2} RS trans
 );
 
-val cancel_numerals =
-  map (prep_simproc @{theory})
-   [("inteq_cancel_numerals",
-     ["(l::'a::number_ring) + m = n",
-      "(l::'a::number_ring) = m + n",
-      "(l::'a::number_ring) - m = n",
-      "(l::'a::number_ring) = m - n",
-      "(l::'a::number_ring) * m = n",
-      "(l::'a::number_ring) = m * n"],
-     K EqCancelNumerals.proc),
-    ("intless_cancel_numerals",
-     ["(l::'a::{linordered_idom,number_ring}) + m < n",
-      "(l::'a::{linordered_idom,number_ring}) < m + n",
-      "(l::'a::{linordered_idom,number_ring}) - m < n",
-      "(l::'a::{linordered_idom,number_ring}) < m - n",
-      "(l::'a::{linordered_idom,number_ring}) * m < n",
-      "(l::'a::{linordered_idom,number_ring}) < m * n"],
-     K LessCancelNumerals.proc),
-    ("intle_cancel_numerals",
-     ["(l::'a::{linordered_idom,number_ring}) + m <= n",
-      "(l::'a::{linordered_idom,number_ring}) <= m + n",
-      "(l::'a::{linordered_idom,number_ring}) - m <= n",
-      "(l::'a::{linordered_idom,number_ring}) <= m - n",
-      "(l::'a::{linordered_idom,number_ring}) * m <= n",
-      "(l::'a::{linordered_idom,number_ring}) <= m * n"],
-     K LeCancelNumerals.proc)];
+fun eq_cancel_numerals ss ct = EqCancelNumerals.proc ss (term_of ct)
+fun less_cancel_numerals ss ct = LessCancelNumerals.proc ss (term_of ct)
+fun le_cancel_numerals ss ct = LeCancelNumerals.proc ss (term_of ct)
 
 structure CombineNumeralsData =
 struct
@@ -330,18 +319,9 @@
 
 structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
 
-val combine_numerals =
-  prep_simproc @{theory}
-    ("int_combine_numerals", 
-     ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], 
-     K CombineNumerals.proc);
+fun combine_numerals ss ct = CombineNumerals.proc ss (term_of ct)
 
-val field_combine_numerals =
-  prep_simproc @{theory}
-    ("field_combine_numerals", 
-     ["(i::'a::{field_inverse_zero, number_ring}) + j",
-      "(i::'a::{field_inverse_zero, number_ring}) - j"], 
-     K FieldCombineNumerals.proc);
+fun field_combine_numerals ss ct = FieldCombineNumerals.proc ss (term_of ct)
 
 (** Constant folding for multiplication in semirings **)
 
@@ -356,10 +336,7 @@
 
 structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
 
-val assoc_fold_simproc =
-  prep_simproc @{theory}
-   ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
-    K Semiring_Times_Assoc.proc);
+fun assoc_fold ss ct = Semiring_Times_Assoc.proc ss (term_of ct)
 
 structure CancelNumeralFactorCommon =
 struct
@@ -426,29 +403,11 @@
   val neg_exchanges = true
 )
 
-val cancel_numeral_factors =
-  map (prep_simproc @{theory})
-   [("ring_eq_cancel_numeral_factor",
-     ["(l::'a::{idom,number_ring}) * m = n",
-      "(l::'a::{idom,number_ring}) = m * n"],
-     K EqCancelNumeralFactor.proc),
-    ("ring_less_cancel_numeral_factor",
-     ["(l::'a::{linordered_idom,number_ring}) * m < n",
-      "(l::'a::{linordered_idom,number_ring}) < m * n"],
-     K LessCancelNumeralFactor.proc),
-    ("ring_le_cancel_numeral_factor",
-     ["(l::'a::{linordered_idom,number_ring}) * m <= n",
-      "(l::'a::{linordered_idom,number_ring}) <= m * n"],
-     K LeCancelNumeralFactor.proc),
-    ("int_div_cancel_numeral_factors",
-     ["((l::'a::{semiring_div,number_ring}) * m) div n",
-      "(l::'a::{semiring_div,number_ring}) div (m * n)"],
-     K DivCancelNumeralFactor.proc),
-    ("divide_cancel_numeral_factor",
-     ["((l::'a::{field_inverse_zero,number_ring}) * m) / n",
-      "(l::'a::{field_inverse_zero,number_ring}) / (m * n)",
-      "((number_of v)::'a::{field_inverse_zero,number_ring}) / (number_of w)"],
-     K DivideCancelNumeralFactor.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 divide_cancel_numeral_factor ss ct = DivideCancelNumeralFactor.proc ss (term_of ct)
 
 val field_cancel_numeral_factors =
   map (prep_simproc @{theory})
@@ -572,33 +531,13 @@
   fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
 );
 
-val cancel_factors =
-  map (prep_simproc @{theory})
-   [("ring_eq_cancel_factor",
-     ["(l::'a::idom) * m = n",
-      "(l::'a::idom) = m * n"],
-     K EqCancelFactor.proc),
-    ("linordered_ring_le_cancel_factor",
-     ["(l::'a::linordered_ring) * m <= n",
-      "(l::'a::linordered_ring) <= m * n"],
-     K LeCancelFactor.proc),
-    ("linordered_ring_less_cancel_factor",
-     ["(l::'a::linordered_ring) * m < n",
-      "(l::'a::linordered_ring) < m * n"],
-     K LessCancelFactor.proc),
-    ("int_div_cancel_factor",
-     ["((l::'a::semiring_div) * m) div n", "(l::'a::semiring_div) div (m * n)"],
-     K DivCancelFactor.proc),
-    ("int_mod_cancel_factor",
-     ["((l::'a::semiring_div) * m) mod n", "(l::'a::semiring_div) mod (m * n)"],
-     K ModCancelFactor.proc),
-    ("dvd_cancel_factor",
-     ["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"],
-     K DvdCancelFactor.proc),
-    ("divide_cancel_factor",
-     ["((l::'a::field_inverse_zero) * m) / n",
-      "(l::'a::field_inverse_zero) / (m * n)"],
-     K DivideCancelFactor.proc)];
+fun eq_cancel_factor ss ct = EqCancelFactor.proc ss (term_of ct)
+fun le_cancel_factor ss ct = LeCancelFactor.proc ss (term_of ct)
+fun less_cancel_factor ss ct = LessCancelFactor.proc ss (term_of ct)
+fun div_cancel_factor ss ct = DivCancelFactor.proc ss (term_of ct)
+fun mod_cancel_factor ss ct = ModCancelFactor.proc ss (term_of ct)
+fun dvd_cancel_factor ss ct = DvdCancelFactor.proc ss (term_of ct)
+fun divide_cancel_factor ss ct = DivideCancelFactor.proc ss (term_of ct)
 
 local
  val zr = @{cpat "0"}
@@ -753,11 +692,6 @@
 
 end;
 
-Addsimprocs Numeral_Simprocs.cancel_numerals;
-Addsimprocs [Numeral_Simprocs.combine_numerals];
-Addsimprocs [Numeral_Simprocs.field_combine_numerals];
-Addsimprocs [Numeral_Simprocs.assoc_fold_simproc];
-
 (*examples:
 print_depth 22;
 set timing;
@@ -795,8 +729,6 @@
 test "(i + j + -12 + (k::int)) - -15 = y";
 *)
 
-Addsimprocs Numeral_Simprocs.cancel_numeral_factors;
-
 (*examples:
 print_depth 22;
 set timing;
@@ -864,9 +796,6 @@
 test "-x <= -23 * (y::rat)";
 *)
 
-Addsimprocs Numeral_Simprocs.cancel_factors;
-
-
 (*examples:
 print_depth 22;
 set timing;
diff -r 9e8616978d99 -r ae78a4ffa81d src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu Oct 27 22:37:19 2011 +0200
+++ b/src/HOL/Word/Word.thy	Fri Oct 28 11:02:27 2011 +0200
@@ -741,7 +741,7 @@
   [symmetric, folded word_number_of_def, standard]
 
 lemmas num_of_bintr = word_ubin.Abs_norm [folded word_number_of_def, standard]
-lemmas num_of_sbintr = word_sbin.Abs_norm [folded word_number_of_def, standard];
+lemmas num_of_sbintr = word_sbin.Abs_norm [folded word_number_of_def, standard]
     
 (* don't add these to simpset, since may want bintrunc n w to be simplified;
   may want these in reverse, but loop as simp rules, so use following *)
@@ -1352,7 +1352,7 @@
 
 lemmas unat_mono = word_less_nat_alt [THEN iffD1, standard]
 
-lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) \<Longrightarrow> (0 :: 'a word) ~= 1";
+lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) \<Longrightarrow> (0 :: 'a word) ~= 1"
   unfolding word_arith_wis
   by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
 
@@ -1661,7 +1661,7 @@
   apply (erule (2) udvd_decr0)
   done
 
-ML {* Delsimprocs Numeral_Simprocs.cancel_factors *}
+ML {* Delsimprocs [@{simproc linordered_ring_less_cancel_factor}] *}
 
 lemma udvd_incr2_K: 
   "p < a + s \<Longrightarrow> a <= a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a <= p \<Longrightarrow> 
@@ -1679,7 +1679,7 @@
   apply simp
   done
 
-ML {* Addsimprocs Numeral_Simprocs.cancel_factors *}
+ML {* Addsimprocs [@{simproc linordered_ring_less_cancel_factor}] *}
 
 (* links with rbl operations *)
 lemma word_succ_rbl:
diff -r 9e8616978d99 -r ae78a4ffa81d src/HOL/ex/Simproc_Tests.thy
--- a/src/HOL/ex/Simproc_Tests.thy	Thu Oct 27 22:37:19 2011 +0200
+++ b/src/HOL/ex/Simproc_Tests.thy	Fri Oct 28 11:02:27 2011 +0200
@@ -18,20 +18,6 @@
 subsection {* ML bindings *}
 
 ML {*
-  val semiring_assoc_fold = Numeral_Simprocs.assoc_fold_simproc
-  val int_combine_numerals = Numeral_Simprocs.combine_numerals
-  val field_combine_numerals = Numeral_Simprocs.field_combine_numerals
-  val [inteq_cancel_numerals, intless_cancel_numerals, intle_cancel_numerals]
-    = Numeral_Simprocs.cancel_numerals
-  val [ring_eq_cancel_factor, linordered_ring_le_cancel_factor,
-      linordered_ring_less_cancel_factor, int_div_cancel_factor,
-      int_mod_cancel_factor, dvd_cancel_factor, divide_cancel_factor]
-    = Numeral_Simprocs.cancel_factors
-  val [ring_eq_cancel_numeral_factor, ring_less_cancel_numeral_factor,
-      ring_le_cancel_numeral_factor, int_div_cancel_numeral_factors,
-      divide_cancel_numeral_factor]
-    = Numeral_Simprocs.cancel_numeral_factors
-  val field_combine_numerals = Numeral_Simprocs.field_combine_numerals
   val [field_eq_cancel_numeral_factor, field_cancel_numeral_factor]
     = Numeral_Simprocs.field_cancel_numeral_factors
 
@@ -43,238 +29,238 @@
 
 lemma assumes "10 + (2 * l + oo) = uu"
   shows "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"
-by (tactic {* test [int_combine_numerals] *}) fact
+by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
 lemma assumes "-3 + (i + (j + k)) = y"
   shows "(i + j + 12 + (k::int)) - 15 = y"
-by (tactic {* test [int_combine_numerals] *}) fact
+by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
 lemma assumes "7 + (i + (j + k)) = y"
   shows "(i + j + 12 + (k::int)) - 5 = y"
-by (tactic {* test [int_combine_numerals] *}) fact
+by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
 lemma assumes "-4 * (u * v) + (2 * x + y) = w"
   shows "(2*x - (u*v) + y) - v*3*u = (w::int)"
-by (tactic {* test [int_combine_numerals] *}) fact
+by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
 lemma assumes "Numeral0 * (u*v) + (2 * x * u * v + y) = w"
   shows "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"
-by (tactic {* test [int_combine_numerals] *}) fact
+by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
 lemma assumes "3 * (u * v) + (2 * x * u * v + y) = w"
   shows "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"
-by (tactic {* test [int_combine_numerals] *}) fact
+by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
 lemma assumes "-3 * (u * v) + (- (x * u * v) + - y) = w"
   shows "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"
-by (tactic {* test [int_combine_numerals] *}) fact
+by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
 lemma assumes "Numeral0 * b + (a + - c) = d"
   shows "a + -(b+c) + b = (d::int)"
 apply (simp only: minus_add_distrib)
-by (tactic {* test [int_combine_numerals] *}) fact
+by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
 lemma assumes "-2 * b + (a + - c) = d"
   shows "a + -(b+c) - b = (d::int)"
 apply (simp only: minus_add_distrib)
-by (tactic {* test [int_combine_numerals] *}) fact
+by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
 lemma assumes "-7 + (i + (j + (k + (- u + - y)))) = zz"
   shows "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"
-by (tactic {* test [int_combine_numerals] *}) fact
+by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
 lemma assumes "-27 + (i + (j + k)) = y"
   shows "(i + j + -12 + (k::int)) - 15 = y"
-by (tactic {* test [int_combine_numerals] *}) fact
+by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
 lemma assumes "27 + (i + (j + k)) = y"
   shows "(i + j + 12 + (k::int)) - -15 = y"
-by (tactic {* test [int_combine_numerals] *}) fact
+by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
 lemma assumes "3 + (i + (j + k)) = y"
   shows "(i + j + -12 + (k::int)) - -15 = y"
-by (tactic {* test [int_combine_numerals] *}) fact
+by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
 
 
 subsection {* @{text inteq_cancel_numerals} *}
 
 lemma assumes "u = Numeral0" shows "2*u = (u::int)"
-by (tactic {* test [inteq_cancel_numerals] *}) fact
+by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
 (* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *)
 
 lemma assumes "i + (j + k) = 3 + (u + y)"
   shows "(i + j + 12 + (k::int)) = u + 15 + y"
-by (tactic {* test [inteq_cancel_numerals] *}) fact
+by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
 
 lemma assumes "7 + (j + (i + k)) = y"
   shows "(i + j*2 + 12 + (k::int)) = j + 5 + y"
-by (tactic {* test [inteq_cancel_numerals] *}) fact
+by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
 
 lemma assumes "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))"
   shows "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)"
-by (tactic {* test [int_combine_numerals, inteq_cancel_numerals] *}) fact
+by (tactic {* test [@{simproc int_combine_numerals}, @{simproc inteq_cancel_numerals}] *}) fact
 
 
 subsection {* @{text intless_cancel_numerals} *}
 
 lemma assumes "y < 2 * b" shows "y - b < (b::int)"
-by (tactic {* test [intless_cancel_numerals] *}) fact
+by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
 
 lemma assumes "c + y < 4 * b" shows "y - (3*b + c) < (b::int) - 2*c"
-by (tactic {* test [intless_cancel_numerals] *}) fact
+by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
 
 lemma assumes "i + (j + k) < 8 + (u + y)"
   shows "(i + j + -3 + (k::int)) < u + 5 + y"
-by (tactic {* test [intless_cancel_numerals] *}) fact
+by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
 
 lemma assumes "9 + (i + (j + k)) < u + y"
   shows "(i + j + 3 + (k::int)) < u + -6 + y"
-by (tactic {* test [intless_cancel_numerals] *}) fact
+by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
 
 
 subsection {* @{text ring_eq_cancel_numeral_factor} *}
 
 lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::int)"
-by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
 lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::int)"
-by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
 
 subsection {* @{text int_div_cancel_numeral_factors} *}
 
 lemma assumes "(3*x) div (4*y) = z" shows "(9*x) div (12*y) = (z::int)"
-by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
+by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
 
 lemma assumes "(-3*x) div (4*y) = z" shows "(-99*x) div (132*y) = (z::int)"
-by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
+by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
 
 lemma assumes "(111*x) div (-44*y) = z" shows "(999*x) div (-396*y) = (z::int)"
-by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
+by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
 
 lemma assumes "(11*x) div (9*y) = z" shows "(-99*x) div (-81*y) = (z::int)"
-by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
+by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
 
 lemma assumes "(2*x) div (Numeral1*y) = z"
   shows "(-2 * x) div (-1 * (y::int)) = z"
-by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
+by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
 
 
 subsection {* @{text ring_less_cancel_numeral_factor} *}
 
 lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::int)"
-by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
 lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::int)"
-by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
 lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::int)"
-by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
 lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::int)"
-by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
 lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::int)"
-by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
 lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::int)"
-by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
 lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::rat)"
-by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
 lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::rat)"
-by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
 lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::rat)"
-by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
 lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::rat)"
-by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
 lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::rat)"
-by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
 lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::rat)"
-by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
 
 
 subsection {* @{text ring_le_cancel_numeral_factor} *}
 
 lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::int)"
-by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
 lemma assumes "-3*x \<le> 4*y" shows "-99*x \<le> 132 * (y::int)"
-by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
 lemma assumes "111*x \<le> -44*y" shows "999*x \<le> -396 * (y::int)"
-by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
 lemma assumes "9*y \<le> 11*x" shows "-99*x \<le> -81 * (y::int)"
-by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
 lemma assumes "Numeral1*y \<le> 2*x" shows "-2 * x \<le> -1 * (y::int)"
-by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
 lemma assumes "23*y \<le> Numeral1*x" shows "-x \<le> -23 * (y::int)"
-by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
 lemma assumes "Numeral1*y \<le> Numeral0" shows "0 \<le> (y::rat) * -2"
-by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
 lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::rat)"
-by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
 lemma assumes "-3*x \<le> 4*y" shows "-99*x \<le> 132 * (y::rat)"
-by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
 lemma assumes "111*x \<le> -44*y" shows "999*x \<le> -396 * (y::rat)"
-by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
 lemma assumes "-1*x \<le> Numeral1*y" shows "- ((2::rat) * x) \<le> 2*y"
-by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
 lemma assumes "9*y \<le> 11*x" shows "-99*x \<le> -81 * (y::rat)"
-by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
 lemma assumes "Numeral1*y \<le> 2*x" shows "-2 * x \<le> -1 * (y::rat)"
-by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
 lemma assumes "23*y \<le> Numeral1*x" shows "-x \<le> -23 * (y::rat)"
-by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
 
 
 subsection {* @{text ring_eq_cancel_numeral_factor} *}
 
 lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::int)"
-by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
 lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::int)"
-by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
 lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::int)"
-by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
 lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::int)"
-by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
 lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::rat)"
-by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
 lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::rat)"
-by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
 lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::rat)"
-by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
 lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::rat)"
-by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
 lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::rat)"
-by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
 lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::rat)"
-by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
+by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
 
 
 subsection {* @{text field_cancel_numeral_factor} *}
@@ -298,66 +284,66 @@
 subsection {* @{text ring_eq_cancel_factor} *}
 
 lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::int)"
-by (tactic {* test [ring_eq_cancel_factor] *}) fact
+by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
 
 lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::int)"
-by (tactic {* test [ring_eq_cancel_factor] *}) fact
+by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
 
 lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::int)"
-by (tactic {* test [ring_eq_cancel_factor] *}) fact
+by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
 
 lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::int)*(x*a)"
-by (tactic {* test [ring_eq_cancel_factor] *}) fact
+by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
 
 lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::rat)"
-by (tactic {* test [ring_eq_cancel_factor] *}) fact
+by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
 
 lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::rat)"
-by (tactic {* test [ring_eq_cancel_factor] *}) fact
+by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
 
 lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::rat)"
-by (tactic {* test [ring_eq_cancel_factor] *}) fact
+by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
 
 lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::rat)*(x*a)"
-by (tactic {* test [ring_eq_cancel_factor] *}) fact
+by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
 
 
 subsection {* @{text int_div_cancel_factor} *}
 
 lemma assumes "(if k = 0 then 0 else x div y) = uu"
   shows "(x*k) div (k*(y::int)) = (uu::int)"
-by (tactic {* test [int_div_cancel_factor] *}) fact
+by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
 
 lemma assumes "(if k = 0 then 0 else 1 div y) = uu"
   shows "(k) div (k*(y::int)) = (uu::int)"
-by (tactic {* test [int_div_cancel_factor] *}) fact
+by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
 
 lemma assumes "(if b = 0 then 0 else a * c) = uu"
   shows "(a*(b*c)) div ((b::int)) = (uu::int)"
-by (tactic {* test [int_div_cancel_factor] *}) fact
+by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
 
 lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
   shows "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)"
-by (tactic {* test [int_div_cancel_factor] *}) fact
+by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
 
 
 subsection {* @{text divide_cancel_factor} *}
 
 lemma assumes "(if k = 0 then 0 else x / y) = uu"
   shows "(x*k) / (k*(y::rat)) = (uu::rat)"
-by (tactic {* test [divide_cancel_factor] *}) fact
+by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
 
 lemma assumes "(if k = 0 then 0 else 1 / y) = uu"
   shows "(k) / (k*(y::rat)) = (uu::rat)"
-by (tactic {* test [divide_cancel_factor] *}) fact
+by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
 
 lemma assumes "(if b = 0 then 0 else a * c / 1) = uu"
   shows "(a*(b*c)) / ((b::rat)) = (uu::rat)"
-by (tactic {* test [divide_cancel_factor] *}) fact
+by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
 
 lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu"
   shows "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)"
-by (tactic {* test [divide_cancel_factor] *}) fact
+by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
 
 lemma shows "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z"
 oops -- "FIXME: need simproc to cover this case"
@@ -366,40 +352,40 @@
 subsection {* @{text linordered_ring_less_cancel_factor} *}
 
 lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < y*z"
-by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
+by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
 
 lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < z*y"
-by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
+by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
 
 lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < y*z"
-by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
+by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
 
 lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < z*y"
-by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
+by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
 
 
 subsection {* @{text linordered_ring_le_cancel_factor} *}
 
 lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> x*z \<le> y*z"
-by (tactic {* test [linordered_ring_le_cancel_factor] *}) fact
+by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
 
 lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> z*x \<le> z*y"
-by (tactic {* test [linordered_ring_le_cancel_factor] *}) fact
+by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
 
 
 subsection {* @{text field_combine_numerals} *}
 
 lemma assumes "5 / 6 * x = uu" shows "(x::rat) / 2 + x / 3 = uu"
-by (tactic {* test [field_combine_numerals] *}) fact
+by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
 
 lemma assumes "6 / 9 * x + y = uu" shows "(x::rat) / 3 + y + x / 3 = uu"
-by (tactic {* test [field_combine_numerals] *}) fact
+by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
 
 lemma assumes "9 / 9 * x = uu" shows "2 * (x::rat) / 3 + x / 3 = uu"
-by (tactic {* test [field_combine_numerals] *}) fact
+by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
 
 lemma "2/3 * (x::rat) + x / 3 = uu"
-apply (tactic {* test [field_combine_numerals] *})?
+apply (tactic {* test [@{simproc field_combine_numerals}] *})?
 oops -- "FIXME: test fails"