use simproc_setup for cancellation simprocs, to get proper name bindings
authorhuffman
Fri Oct 28 11:02:27 2011 +0200 (2011-10-28)
changeset 45284ae78a4ffa81d
parent 45283 9e8616978d99
child 45285 299abd2931d5
use simproc_setup for cancellation simprocs, to get proper name bindings
src/HOL/Numeral_Simprocs.thy
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Word/Word.thy
src/HOL/ex/Simproc_Tests.thy
     1.1 --- a/src/HOL/Numeral_Simprocs.thy	Thu Oct 27 22:37:19 2011 +0200
     1.2 +++ b/src/HOL/Numeral_Simprocs.thy	Fri Oct 28 11:02:27 2011 +0200
     1.3 @@ -94,6 +94,106 @@
     1.4  
     1.5  use "Tools/numeral_simprocs.ML"
     1.6  
     1.7 +simproc_setup semiring_assoc_fold
     1.8 +  ("(a::'a::comm_semiring_1_cancel) * b") =
     1.9 +  {* fn phi => Numeral_Simprocs.assoc_fold *}
    1.10 +
    1.11 +simproc_setup int_combine_numerals
    1.12 +  ("(i::'a::number_ring) + j" | "(i::'a::number_ring) - j") =
    1.13 +  {* fn phi => Numeral_Simprocs.combine_numerals *}
    1.14 +
    1.15 +simproc_setup field_combine_numerals
    1.16 +  ("(i::'a::{field_inverse_zero, number_ring}) + j"
    1.17 +  |"(i::'a::{field_inverse_zero, number_ring}) - j") =
    1.18 +  {* fn phi => Numeral_Simprocs.field_combine_numerals *}
    1.19 +
    1.20 +simproc_setup inteq_cancel_numerals
    1.21 +  ("(l::'a::number_ring) + m = n"
    1.22 +  |"(l::'a::number_ring) = m + n"
    1.23 +  |"(l::'a::number_ring) - m = n"
    1.24 +  |"(l::'a::number_ring) = m - n"
    1.25 +  |"(l::'a::number_ring) * m = n"
    1.26 +  |"(l::'a::number_ring) = m * n") =
    1.27 +  {* fn phi => Numeral_Simprocs.eq_cancel_numerals *}
    1.28 +
    1.29 +simproc_setup intless_cancel_numerals
    1.30 +  ("(l::'a::{linordered_idom,number_ring}) + m < n"
    1.31 +  |"(l::'a::{linordered_idom,number_ring}) < m + n"
    1.32 +  |"(l::'a::{linordered_idom,number_ring}) - m < n"
    1.33 +  |"(l::'a::{linordered_idom,number_ring}) < m - n"
    1.34 +  |"(l::'a::{linordered_idom,number_ring}) * m < n"
    1.35 +  |"(l::'a::{linordered_idom,number_ring}) < m * n") =
    1.36 +  {* fn phi => Numeral_Simprocs.less_cancel_numerals *}
    1.37 +
    1.38 +simproc_setup intle_cancel_numerals
    1.39 +  ("(l::'a::{linordered_idom,number_ring}) + m \<le> n"
    1.40 +  |"(l::'a::{linordered_idom,number_ring}) \<le> m + n"
    1.41 +  |"(l::'a::{linordered_idom,number_ring}) - m \<le> n"
    1.42 +  |"(l::'a::{linordered_idom,number_ring}) \<le> m - n"
    1.43 +  |"(l::'a::{linordered_idom,number_ring}) * m \<le> n"
    1.44 +  |"(l::'a::{linordered_idom,number_ring}) \<le> m * n") =
    1.45 +  {* fn phi => Numeral_Simprocs.le_cancel_numerals *}
    1.46 +
    1.47 +simproc_setup ring_eq_cancel_numeral_factor
    1.48 +  ("(l::'a::{idom,number_ring}) * m = n"
    1.49 +  |"(l::'a::{idom,number_ring}) = m * n") =
    1.50 +  {* fn phi => Numeral_Simprocs.eq_cancel_numeral_factor *}
    1.51 +
    1.52 +simproc_setup ring_less_cancel_numeral_factor
    1.53 +  ("(l::'a::{linordered_idom,number_ring}) * m < n"
    1.54 +  |"(l::'a::{linordered_idom,number_ring}) < m * n") =
    1.55 +  {* fn phi => Numeral_Simprocs.less_cancel_numeral_factor *}
    1.56 +
    1.57 +simproc_setup ring_le_cancel_numeral_factor
    1.58 +  ("(l::'a::{linordered_idom,number_ring}) * m <= n"
    1.59 +  |"(l::'a::{linordered_idom,number_ring}) <= m * n") =
    1.60 +  {* fn phi => Numeral_Simprocs.le_cancel_numeral_factor *}
    1.61 +
    1.62 +simproc_setup int_div_cancel_numeral_factors
    1.63 +  ("((l::'a::{semiring_div,number_ring}) * m) div n"
    1.64 +  |"(l::'a::{semiring_div,number_ring}) div (m * n)") =
    1.65 +  {* fn phi => Numeral_Simprocs.div_cancel_numeral_factor *}
    1.66 +
    1.67 +simproc_setup divide_cancel_numeral_factor
    1.68 +  ("((l::'a::{field_inverse_zero,number_ring}) * m) / n"
    1.69 +  |"(l::'a::{field_inverse_zero,number_ring}) / (m * n)"
    1.70 +  |"((number_of v)::'a::{field_inverse_zero,number_ring}) / (number_of w)") =
    1.71 +  {* fn phi => Numeral_Simprocs.divide_cancel_numeral_factor *}
    1.72 +
    1.73 +simproc_setup ring_eq_cancel_factor
    1.74 +  ("(l::'a::idom) * m = n" | "(l::'a::idom) = m * n") =
    1.75 +  {* fn phi => Numeral_Simprocs.eq_cancel_factor *}
    1.76 +
    1.77 +simproc_setup linordered_ring_le_cancel_factor
    1.78 +  ("(l::'a::linordered_ring) * m <= n"
    1.79 +  |"(l::'a::linordered_ring) <= m * n") =
    1.80 +  {* fn phi => Numeral_Simprocs.le_cancel_factor *}
    1.81 +
    1.82 +simproc_setup linordered_ring_less_cancel_factor
    1.83 +  ("(l::'a::linordered_ring) * m < n"
    1.84 +  |"(l::'a::linordered_ring) < m * n") =
    1.85 +  {* fn phi => Numeral_Simprocs.less_cancel_factor *}
    1.86 +
    1.87 +simproc_setup int_div_cancel_factor
    1.88 +  ("((l::'a::semiring_div) * m) div n"
    1.89 +  |"(l::'a::semiring_div) div (m * n)") =
    1.90 +  {* fn phi => Numeral_Simprocs.div_cancel_factor *}
    1.91 +
    1.92 +simproc_setup int_mod_cancel_factor
    1.93 +  ("((l::'a::semiring_div) * m) mod n"
    1.94 +  |"(l::'a::semiring_div) mod (m * n)") =
    1.95 +  {* fn phi => Numeral_Simprocs.mod_cancel_factor *}
    1.96 +
    1.97 +simproc_setup dvd_cancel_factor
    1.98 +  ("((l::'a::idom) * m) dvd n"
    1.99 +  |"(l::'a::idom) dvd (m * n)") =
   1.100 +  {* fn phi => Numeral_Simprocs.dvd_cancel_factor *}
   1.101 +
   1.102 +simproc_setup divide_cancel_factor
   1.103 +  ("((l::'a::field_inverse_zero) * m) / n"
   1.104 +  |"(l::'a::field_inverse_zero) / (m * n)") =
   1.105 +  {* fn phi => Numeral_Simprocs.divide_cancel_factor *}
   1.106 +
   1.107  use "Tools/nat_numeral_simprocs.ML"
   1.108  
   1.109  declaration {* 
   1.110 @@ -110,9 +210,12 @@
   1.111       @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
   1.112       @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of},
   1.113       @{thm if_True}, @{thm if_False}])
   1.114 -  #> Lin_Arith.add_simprocs (Numeral_Simprocs.assoc_fold_simproc
   1.115 -      :: Numeral_Simprocs.combine_numerals
   1.116 -      :: Numeral_Simprocs.cancel_numerals)
   1.117 +  #> Lin_Arith.add_simprocs
   1.118 +      [@{simproc semiring_assoc_fold},
   1.119 +       @{simproc int_combine_numerals},
   1.120 +       @{simproc inteq_cancel_numerals},
   1.121 +       @{simproc intless_cancel_numerals},
   1.122 +       @{simproc intle_cancel_numerals}]
   1.123    #> Lin_Arith.add_simprocs (Nat_Numeral_Simprocs.combine_numerals :: Nat_Numeral_Simprocs.cancel_numerals))
   1.124  *}
   1.125  
     2.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Thu Oct 27 22:37:19 2011 +0200
     2.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Fri Oct 28 11:02:27 2011 +0200
     2.3 @@ -19,12 +19,24 @@
     2.4    val prep_simproc: theory -> string * string list * (theory -> simpset -> term -> thm option)
     2.5      -> simproc
     2.6    val trans_tac: thm option -> tactic
     2.7 -  val assoc_fold_simproc: simproc
     2.8 -  val combine_numerals: simproc
     2.9 -  val cancel_numerals: simproc list
    2.10 -  val cancel_factors: simproc list
    2.11 -  val cancel_numeral_factors: simproc list
    2.12 -  val field_combine_numerals: simproc
    2.13 +  val assoc_fold: simpset -> cterm -> thm option
    2.14 +  val combine_numerals: simpset -> cterm -> thm option
    2.15 +  val eq_cancel_numerals: simpset -> cterm -> thm option
    2.16 +  val less_cancel_numerals: simpset -> cterm -> thm option
    2.17 +  val le_cancel_numerals: simpset -> cterm -> thm option
    2.18 +  val eq_cancel_factor: simpset -> cterm -> thm option
    2.19 +  val le_cancel_factor: simpset -> cterm -> thm option
    2.20 +  val less_cancel_factor: simpset -> cterm -> thm option
    2.21 +  val div_cancel_factor: simpset -> cterm -> thm option
    2.22 +  val mod_cancel_factor: simpset -> cterm -> thm option
    2.23 +  val dvd_cancel_factor: simpset -> cterm -> thm option
    2.24 +  val divide_cancel_factor: simpset -> cterm -> thm option
    2.25 +  val eq_cancel_numeral_factor: simpset -> cterm -> thm option
    2.26 +  val less_cancel_numeral_factor: simpset -> cterm -> thm option
    2.27 +  val le_cancel_numeral_factor: simpset -> cterm -> thm option
    2.28 +  val div_cancel_numeral_factor: simpset -> cterm -> thm option
    2.29 +  val divide_cancel_numeral_factor: simpset -> cterm -> thm option
    2.30 +  val field_combine_numerals: simpset -> cterm -> thm option
    2.31    val field_cancel_numeral_factors: simproc list
    2.32    val num_ss: simpset
    2.33    val field_comp_conv: conv
    2.34 @@ -251,32 +263,9 @@
    2.35    val bal_add2 = @{thm le_add_iff2} RS trans
    2.36  );
    2.37  
    2.38 -val cancel_numerals =
    2.39 -  map (prep_simproc @{theory})
    2.40 -   [("inteq_cancel_numerals",
    2.41 -     ["(l::'a::number_ring) + m = n",
    2.42 -      "(l::'a::number_ring) = m + n",
    2.43 -      "(l::'a::number_ring) - m = n",
    2.44 -      "(l::'a::number_ring) = m - n",
    2.45 -      "(l::'a::number_ring) * m = n",
    2.46 -      "(l::'a::number_ring) = m * n"],
    2.47 -     K EqCancelNumerals.proc),
    2.48 -    ("intless_cancel_numerals",
    2.49 -     ["(l::'a::{linordered_idom,number_ring}) + m < n",
    2.50 -      "(l::'a::{linordered_idom,number_ring}) < m + n",
    2.51 -      "(l::'a::{linordered_idom,number_ring}) - m < n",
    2.52 -      "(l::'a::{linordered_idom,number_ring}) < m - n",
    2.53 -      "(l::'a::{linordered_idom,number_ring}) * m < n",
    2.54 -      "(l::'a::{linordered_idom,number_ring}) < m * n"],
    2.55 -     K LessCancelNumerals.proc),
    2.56 -    ("intle_cancel_numerals",
    2.57 -     ["(l::'a::{linordered_idom,number_ring}) + m <= n",
    2.58 -      "(l::'a::{linordered_idom,number_ring}) <= m + n",
    2.59 -      "(l::'a::{linordered_idom,number_ring}) - m <= n",
    2.60 -      "(l::'a::{linordered_idom,number_ring}) <= m - n",
    2.61 -      "(l::'a::{linordered_idom,number_ring}) * m <= n",
    2.62 -      "(l::'a::{linordered_idom,number_ring}) <= m * n"],
    2.63 -     K LeCancelNumerals.proc)];
    2.64 +fun eq_cancel_numerals ss ct = EqCancelNumerals.proc ss (term_of ct)
    2.65 +fun less_cancel_numerals ss ct = LessCancelNumerals.proc ss (term_of ct)
    2.66 +fun le_cancel_numerals ss ct = LeCancelNumerals.proc ss (term_of ct)
    2.67  
    2.68  structure CombineNumeralsData =
    2.69  struct
    2.70 @@ -330,18 +319,9 @@
    2.71  
    2.72  structure FieldCombineNumerals = CombineNumeralsFun(FieldCombineNumeralsData);
    2.73  
    2.74 -val combine_numerals =
    2.75 -  prep_simproc @{theory}
    2.76 -    ("int_combine_numerals", 
    2.77 -     ["(i::'a::number_ring) + j", "(i::'a::number_ring) - j"], 
    2.78 -     K CombineNumerals.proc);
    2.79 +fun combine_numerals ss ct = CombineNumerals.proc ss (term_of ct)
    2.80  
    2.81 -val field_combine_numerals =
    2.82 -  prep_simproc @{theory}
    2.83 -    ("field_combine_numerals", 
    2.84 -     ["(i::'a::{field_inverse_zero, number_ring}) + j",
    2.85 -      "(i::'a::{field_inverse_zero, number_ring}) - j"], 
    2.86 -     K FieldCombineNumerals.proc);
    2.87 +fun field_combine_numerals ss ct = FieldCombineNumerals.proc ss (term_of ct)
    2.88  
    2.89  (** Constant folding for multiplication in semirings **)
    2.90  
    2.91 @@ -356,10 +336,7 @@
    2.92  
    2.93  structure Semiring_Times_Assoc = Assoc_Fold (Semiring_Times_Assoc_Data);
    2.94  
    2.95 -val assoc_fold_simproc =
    2.96 -  prep_simproc @{theory}
    2.97 -   ("semiring_assoc_fold", ["(a::'a::comm_semiring_1_cancel) * b"],
    2.98 -    K Semiring_Times_Assoc.proc);
    2.99 +fun assoc_fold ss ct = Semiring_Times_Assoc.proc ss (term_of ct)
   2.100  
   2.101  structure CancelNumeralFactorCommon =
   2.102  struct
   2.103 @@ -426,29 +403,11 @@
   2.104    val neg_exchanges = true
   2.105  )
   2.106  
   2.107 -val cancel_numeral_factors =
   2.108 -  map (prep_simproc @{theory})
   2.109 -   [("ring_eq_cancel_numeral_factor",
   2.110 -     ["(l::'a::{idom,number_ring}) * m = n",
   2.111 -      "(l::'a::{idom,number_ring}) = m * n"],
   2.112 -     K EqCancelNumeralFactor.proc),
   2.113 -    ("ring_less_cancel_numeral_factor",
   2.114 -     ["(l::'a::{linordered_idom,number_ring}) * m < n",
   2.115 -      "(l::'a::{linordered_idom,number_ring}) < m * n"],
   2.116 -     K LessCancelNumeralFactor.proc),
   2.117 -    ("ring_le_cancel_numeral_factor",
   2.118 -     ["(l::'a::{linordered_idom,number_ring}) * m <= n",
   2.119 -      "(l::'a::{linordered_idom,number_ring}) <= m * n"],
   2.120 -     K LeCancelNumeralFactor.proc),
   2.121 -    ("int_div_cancel_numeral_factors",
   2.122 -     ["((l::'a::{semiring_div,number_ring}) * m) div n",
   2.123 -      "(l::'a::{semiring_div,number_ring}) div (m * n)"],
   2.124 -     K DivCancelNumeralFactor.proc),
   2.125 -    ("divide_cancel_numeral_factor",
   2.126 -     ["((l::'a::{field_inverse_zero,number_ring}) * m) / n",
   2.127 -      "(l::'a::{field_inverse_zero,number_ring}) / (m * n)",
   2.128 -      "((number_of v)::'a::{field_inverse_zero,number_ring}) / (number_of w)"],
   2.129 -     K DivideCancelNumeralFactor.proc)];
   2.130 +fun eq_cancel_numeral_factor ss ct = EqCancelNumeralFactor.proc ss (term_of ct)
   2.131 +fun less_cancel_numeral_factor ss ct = LessCancelNumeralFactor.proc ss (term_of ct)
   2.132 +fun le_cancel_numeral_factor ss ct = LeCancelNumeralFactor.proc ss (term_of ct)
   2.133 +fun div_cancel_numeral_factor ss ct = DivCancelNumeralFactor.proc ss (term_of ct)
   2.134 +fun divide_cancel_numeral_factor ss ct = DivideCancelNumeralFactor.proc ss (term_of ct)
   2.135  
   2.136  val field_cancel_numeral_factors =
   2.137    map (prep_simproc @{theory})
   2.138 @@ -572,33 +531,13 @@
   2.139    fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
   2.140  );
   2.141  
   2.142 -val cancel_factors =
   2.143 -  map (prep_simproc @{theory})
   2.144 -   [("ring_eq_cancel_factor",
   2.145 -     ["(l::'a::idom) * m = n",
   2.146 -      "(l::'a::idom) = m * n"],
   2.147 -     K EqCancelFactor.proc),
   2.148 -    ("linordered_ring_le_cancel_factor",
   2.149 -     ["(l::'a::linordered_ring) * m <= n",
   2.150 -      "(l::'a::linordered_ring) <= m * n"],
   2.151 -     K LeCancelFactor.proc),
   2.152 -    ("linordered_ring_less_cancel_factor",
   2.153 -     ["(l::'a::linordered_ring) * m < n",
   2.154 -      "(l::'a::linordered_ring) < m * n"],
   2.155 -     K LessCancelFactor.proc),
   2.156 -    ("int_div_cancel_factor",
   2.157 -     ["((l::'a::semiring_div) * m) div n", "(l::'a::semiring_div) div (m * n)"],
   2.158 -     K DivCancelFactor.proc),
   2.159 -    ("int_mod_cancel_factor",
   2.160 -     ["((l::'a::semiring_div) * m) mod n", "(l::'a::semiring_div) mod (m * n)"],
   2.161 -     K ModCancelFactor.proc),
   2.162 -    ("dvd_cancel_factor",
   2.163 -     ["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"],
   2.164 -     K DvdCancelFactor.proc),
   2.165 -    ("divide_cancel_factor",
   2.166 -     ["((l::'a::field_inverse_zero) * m) / n",
   2.167 -      "(l::'a::field_inverse_zero) / (m * n)"],
   2.168 -     K DivideCancelFactor.proc)];
   2.169 +fun eq_cancel_factor ss ct = EqCancelFactor.proc ss (term_of ct)
   2.170 +fun le_cancel_factor ss ct = LeCancelFactor.proc ss (term_of ct)
   2.171 +fun less_cancel_factor ss ct = LessCancelFactor.proc ss (term_of ct)
   2.172 +fun div_cancel_factor ss ct = DivCancelFactor.proc ss (term_of ct)
   2.173 +fun mod_cancel_factor ss ct = ModCancelFactor.proc ss (term_of ct)
   2.174 +fun dvd_cancel_factor ss ct = DvdCancelFactor.proc ss (term_of ct)
   2.175 +fun divide_cancel_factor ss ct = DivideCancelFactor.proc ss (term_of ct)
   2.176  
   2.177  local
   2.178   val zr = @{cpat "0"}
   2.179 @@ -753,11 +692,6 @@
   2.180  
   2.181  end;
   2.182  
   2.183 -Addsimprocs Numeral_Simprocs.cancel_numerals;
   2.184 -Addsimprocs [Numeral_Simprocs.combine_numerals];
   2.185 -Addsimprocs [Numeral_Simprocs.field_combine_numerals];
   2.186 -Addsimprocs [Numeral_Simprocs.assoc_fold_simproc];
   2.187 -
   2.188  (*examples:
   2.189  print_depth 22;
   2.190  set timing;
   2.191 @@ -795,8 +729,6 @@
   2.192  test "(i + j + -12 + (k::int)) - -15 = y";
   2.193  *)
   2.194  
   2.195 -Addsimprocs Numeral_Simprocs.cancel_numeral_factors;
   2.196 -
   2.197  (*examples:
   2.198  print_depth 22;
   2.199  set timing;
   2.200 @@ -864,9 +796,6 @@
   2.201  test "-x <= -23 * (y::rat)";
   2.202  *)
   2.203  
   2.204 -Addsimprocs Numeral_Simprocs.cancel_factors;
   2.205 -
   2.206 -
   2.207  (*examples:
   2.208  print_depth 22;
   2.209  set timing;
     3.1 --- a/src/HOL/Word/Word.thy	Thu Oct 27 22:37:19 2011 +0200
     3.2 +++ b/src/HOL/Word/Word.thy	Fri Oct 28 11:02:27 2011 +0200
     3.3 @@ -741,7 +741,7 @@
     3.4    [symmetric, folded word_number_of_def, standard]
     3.5  
     3.6  lemmas num_of_bintr = word_ubin.Abs_norm [folded word_number_of_def, standard]
     3.7 -lemmas num_of_sbintr = word_sbin.Abs_norm [folded word_number_of_def, standard];
     3.8 +lemmas num_of_sbintr = word_sbin.Abs_norm [folded word_number_of_def, standard]
     3.9      
    3.10  (* don't add these to simpset, since may want bintrunc n w to be simplified;
    3.11    may want these in reverse, but loop as simp rules, so use following *)
    3.12 @@ -1352,7 +1352,7 @@
    3.13  
    3.14  lemmas unat_mono = word_less_nat_alt [THEN iffD1, standard]
    3.15  
    3.16 -lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) \<Longrightarrow> (0 :: 'a word) ~= 1";
    3.17 +lemma word_zero_neq_one: "0 < len_of TYPE ('a :: len0) \<Longrightarrow> (0 :: 'a word) ~= 1"
    3.18    unfolding word_arith_wis
    3.19    by (auto simp add: word_ubin.norm_eq_iff [symmetric] gr0_conv_Suc)
    3.20  
    3.21 @@ -1661,7 +1661,7 @@
    3.22    apply (erule (2) udvd_decr0)
    3.23    done
    3.24  
    3.25 -ML {* Delsimprocs Numeral_Simprocs.cancel_factors *}
    3.26 +ML {* Delsimprocs [@{simproc linordered_ring_less_cancel_factor}] *}
    3.27  
    3.28  lemma udvd_incr2_K: 
    3.29    "p < a + s \<Longrightarrow> a <= a + s \<Longrightarrow> K udvd s \<Longrightarrow> K udvd p - a \<Longrightarrow> a <= p \<Longrightarrow> 
    3.30 @@ -1679,7 +1679,7 @@
    3.31    apply simp
    3.32    done
    3.33  
    3.34 -ML {* Addsimprocs Numeral_Simprocs.cancel_factors *}
    3.35 +ML {* Addsimprocs [@{simproc linordered_ring_less_cancel_factor}] *}
    3.36  
    3.37  (* links with rbl operations *)
    3.38  lemma word_succ_rbl:
     4.1 --- a/src/HOL/ex/Simproc_Tests.thy	Thu Oct 27 22:37:19 2011 +0200
     4.2 +++ b/src/HOL/ex/Simproc_Tests.thy	Fri Oct 28 11:02:27 2011 +0200
     4.3 @@ -18,20 +18,6 @@
     4.4  subsection {* ML bindings *}
     4.5  
     4.6  ML {*
     4.7 -  val semiring_assoc_fold = Numeral_Simprocs.assoc_fold_simproc
     4.8 -  val int_combine_numerals = Numeral_Simprocs.combine_numerals
     4.9 -  val field_combine_numerals = Numeral_Simprocs.field_combine_numerals
    4.10 -  val [inteq_cancel_numerals, intless_cancel_numerals, intle_cancel_numerals]
    4.11 -    = Numeral_Simprocs.cancel_numerals
    4.12 -  val [ring_eq_cancel_factor, linordered_ring_le_cancel_factor,
    4.13 -      linordered_ring_less_cancel_factor, int_div_cancel_factor,
    4.14 -      int_mod_cancel_factor, dvd_cancel_factor, divide_cancel_factor]
    4.15 -    = Numeral_Simprocs.cancel_factors
    4.16 -  val [ring_eq_cancel_numeral_factor, ring_less_cancel_numeral_factor,
    4.17 -      ring_le_cancel_numeral_factor, int_div_cancel_numeral_factors,
    4.18 -      divide_cancel_numeral_factor]
    4.19 -    = Numeral_Simprocs.cancel_numeral_factors
    4.20 -  val field_combine_numerals = Numeral_Simprocs.field_combine_numerals
    4.21    val [field_eq_cancel_numeral_factor, field_cancel_numeral_factor]
    4.22      = Numeral_Simprocs.field_cancel_numeral_factors
    4.23  
    4.24 @@ -43,238 +29,238 @@
    4.25  
    4.26  lemma assumes "10 + (2 * l + oo) = uu"
    4.27    shows "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"
    4.28 -by (tactic {* test [int_combine_numerals] *}) fact
    4.29 +by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    4.30  
    4.31  lemma assumes "-3 + (i + (j + k)) = y"
    4.32    shows "(i + j + 12 + (k::int)) - 15 = y"
    4.33 -by (tactic {* test [int_combine_numerals] *}) fact
    4.34 +by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    4.35  
    4.36  lemma assumes "7 + (i + (j + k)) = y"
    4.37    shows "(i + j + 12 + (k::int)) - 5 = y"
    4.38 -by (tactic {* test [int_combine_numerals] *}) fact
    4.39 +by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    4.40  
    4.41  lemma assumes "-4 * (u * v) + (2 * x + y) = w"
    4.42    shows "(2*x - (u*v) + y) - v*3*u = (w::int)"
    4.43 -by (tactic {* test [int_combine_numerals] *}) fact
    4.44 +by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    4.45  
    4.46  lemma assumes "Numeral0 * (u*v) + (2 * x * u * v + y) = w"
    4.47    shows "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"
    4.48 -by (tactic {* test [int_combine_numerals] *}) fact
    4.49 +by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    4.50  
    4.51  lemma assumes "3 * (u * v) + (2 * x * u * v + y) = w"
    4.52    shows "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"
    4.53 -by (tactic {* test [int_combine_numerals] *}) fact
    4.54 +by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    4.55  
    4.56  lemma assumes "-3 * (u * v) + (- (x * u * v) + - y) = w"
    4.57    shows "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"
    4.58 -by (tactic {* test [int_combine_numerals] *}) fact
    4.59 +by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    4.60  
    4.61  lemma assumes "Numeral0 * b + (a + - c) = d"
    4.62    shows "a + -(b+c) + b = (d::int)"
    4.63  apply (simp only: minus_add_distrib)
    4.64 -by (tactic {* test [int_combine_numerals] *}) fact
    4.65 +by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    4.66  
    4.67  lemma assumes "-2 * b + (a + - c) = d"
    4.68    shows "a + -(b+c) - b = (d::int)"
    4.69  apply (simp only: minus_add_distrib)
    4.70 -by (tactic {* test [int_combine_numerals] *}) fact
    4.71 +by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    4.72  
    4.73  lemma assumes "-7 + (i + (j + (k + (- u + - y)))) = zz"
    4.74    shows "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"
    4.75 -by (tactic {* test [int_combine_numerals] *}) fact
    4.76 +by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    4.77  
    4.78  lemma assumes "-27 + (i + (j + k)) = y"
    4.79    shows "(i + j + -12 + (k::int)) - 15 = y"
    4.80 -by (tactic {* test [int_combine_numerals] *}) fact
    4.81 +by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    4.82  
    4.83  lemma assumes "27 + (i + (j + k)) = y"
    4.84    shows "(i + j + 12 + (k::int)) - -15 = y"
    4.85 -by (tactic {* test [int_combine_numerals] *}) fact
    4.86 +by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    4.87  
    4.88  lemma assumes "3 + (i + (j + k)) = y"
    4.89    shows "(i + j + -12 + (k::int)) - -15 = y"
    4.90 -by (tactic {* test [int_combine_numerals] *}) fact
    4.91 +by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    4.92  
    4.93  
    4.94  subsection {* @{text inteq_cancel_numerals} *}
    4.95  
    4.96  lemma assumes "u = Numeral0" shows "2*u = (u::int)"
    4.97 -by (tactic {* test [inteq_cancel_numerals] *}) fact
    4.98 +by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
    4.99  (* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *)
   4.100  
   4.101  lemma assumes "i + (j + k) = 3 + (u + y)"
   4.102    shows "(i + j + 12 + (k::int)) = u + 15 + y"
   4.103 -by (tactic {* test [inteq_cancel_numerals] *}) fact
   4.104 +by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
   4.105  
   4.106  lemma assumes "7 + (j + (i + k)) = y"
   4.107    shows "(i + j*2 + 12 + (k::int)) = j + 5 + y"
   4.108 -by (tactic {* test [inteq_cancel_numerals] *}) fact
   4.109 +by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
   4.110  
   4.111  lemma assumes "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))"
   4.112    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)"
   4.113 -by (tactic {* test [int_combine_numerals, inteq_cancel_numerals] *}) fact
   4.114 +by (tactic {* test [@{simproc int_combine_numerals}, @{simproc inteq_cancel_numerals}] *}) fact
   4.115  
   4.116  
   4.117  subsection {* @{text intless_cancel_numerals} *}
   4.118  
   4.119  lemma assumes "y < 2 * b" shows "y - b < (b::int)"
   4.120 -by (tactic {* test [intless_cancel_numerals] *}) fact
   4.121 +by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
   4.122  
   4.123  lemma assumes "c + y < 4 * b" shows "y - (3*b + c) < (b::int) - 2*c"
   4.124 -by (tactic {* test [intless_cancel_numerals] *}) fact
   4.125 +by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
   4.126  
   4.127  lemma assumes "i + (j + k) < 8 + (u + y)"
   4.128    shows "(i + j + -3 + (k::int)) < u + 5 + y"
   4.129 -by (tactic {* test [intless_cancel_numerals] *}) fact
   4.130 +by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
   4.131  
   4.132  lemma assumes "9 + (i + (j + k)) < u + y"
   4.133    shows "(i + j + 3 + (k::int)) < u + -6 + y"
   4.134 -by (tactic {* test [intless_cancel_numerals] *}) fact
   4.135 +by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
   4.136  
   4.137  
   4.138  subsection {* @{text ring_eq_cancel_numeral_factor} *}
   4.139  
   4.140  lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::int)"
   4.141 -by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
   4.142 +by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   4.143  
   4.144  lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::int)"
   4.145 -by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
   4.146 +by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   4.147  
   4.148  
   4.149  subsection {* @{text int_div_cancel_numeral_factors} *}
   4.150  
   4.151  lemma assumes "(3*x) div (4*y) = z" shows "(9*x) div (12*y) = (z::int)"
   4.152 -by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
   4.153 +by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
   4.154  
   4.155  lemma assumes "(-3*x) div (4*y) = z" shows "(-99*x) div (132*y) = (z::int)"
   4.156 -by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
   4.157 +by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
   4.158  
   4.159  lemma assumes "(111*x) div (-44*y) = z" shows "(999*x) div (-396*y) = (z::int)"
   4.160 -by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
   4.161 +by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
   4.162  
   4.163  lemma assumes "(11*x) div (9*y) = z" shows "(-99*x) div (-81*y) = (z::int)"
   4.164 -by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
   4.165 +by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
   4.166  
   4.167  lemma assumes "(2*x) div (Numeral1*y) = z"
   4.168    shows "(-2 * x) div (-1 * (y::int)) = z"
   4.169 -by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
   4.170 +by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
   4.171  
   4.172  
   4.173  subsection {* @{text ring_less_cancel_numeral_factor} *}
   4.174  
   4.175  lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::int)"
   4.176 -by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
   4.177 +by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   4.178  
   4.179  lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::int)"
   4.180 -by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
   4.181 +by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   4.182  
   4.183  lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::int)"
   4.184 -by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
   4.185 +by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   4.186  
   4.187  lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::int)"
   4.188 -by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
   4.189 +by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   4.190  
   4.191  lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::int)"
   4.192 -by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
   4.193 +by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   4.194  
   4.195  lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::int)"
   4.196 -by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
   4.197 +by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   4.198  
   4.199  lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::rat)"
   4.200 -by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
   4.201 +by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   4.202  
   4.203  lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::rat)"
   4.204 -by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
   4.205 +by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   4.206  
   4.207  lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::rat)"
   4.208 -by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
   4.209 +by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   4.210  
   4.211  lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::rat)"
   4.212 -by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
   4.213 +by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   4.214  
   4.215  lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::rat)"
   4.216 -by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
   4.217 +by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   4.218  
   4.219  lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::rat)"
   4.220 -by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
   4.221 +by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   4.222  
   4.223  
   4.224  subsection {* @{text ring_le_cancel_numeral_factor} *}
   4.225  
   4.226  lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::int)"
   4.227 -by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
   4.228 +by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   4.229  
   4.230  lemma assumes "-3*x \<le> 4*y" shows "-99*x \<le> 132 * (y::int)"
   4.231 -by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
   4.232 +by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   4.233  
   4.234  lemma assumes "111*x \<le> -44*y" shows "999*x \<le> -396 * (y::int)"
   4.235 -by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
   4.236 +by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   4.237  
   4.238  lemma assumes "9*y \<le> 11*x" shows "-99*x \<le> -81 * (y::int)"
   4.239 -by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
   4.240 +by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   4.241  
   4.242  lemma assumes "Numeral1*y \<le> 2*x" shows "-2 * x \<le> -1 * (y::int)"
   4.243 -by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
   4.244 +by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   4.245  
   4.246  lemma assumes "23*y \<le> Numeral1*x" shows "-x \<le> -23 * (y::int)"
   4.247 -by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
   4.248 +by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   4.249  
   4.250  lemma assumes "Numeral1*y \<le> Numeral0" shows "0 \<le> (y::rat) * -2"
   4.251 -by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
   4.252 +by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   4.253  
   4.254  lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::rat)"
   4.255 -by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
   4.256 +by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   4.257  
   4.258  lemma assumes "-3*x \<le> 4*y" shows "-99*x \<le> 132 * (y::rat)"
   4.259 -by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
   4.260 +by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   4.261  
   4.262  lemma assumes "111*x \<le> -44*y" shows "999*x \<le> -396 * (y::rat)"
   4.263 -by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
   4.264 +by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   4.265  
   4.266  lemma assumes "-1*x \<le> Numeral1*y" shows "- ((2::rat) * x) \<le> 2*y"
   4.267 -by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
   4.268 +by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   4.269  
   4.270  lemma assumes "9*y \<le> 11*x" shows "-99*x \<le> -81 * (y::rat)"
   4.271 -by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
   4.272 +by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   4.273  
   4.274  lemma assumes "Numeral1*y \<le> 2*x" shows "-2 * x \<le> -1 * (y::rat)"
   4.275 -by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
   4.276 +by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   4.277  
   4.278  lemma assumes "23*y \<le> Numeral1*x" shows "-x \<le> -23 * (y::rat)"
   4.279 -by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
   4.280 +by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   4.281  
   4.282  
   4.283  subsection {* @{text ring_eq_cancel_numeral_factor} *}
   4.284  
   4.285  lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::int)"
   4.286 -by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
   4.287 +by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   4.288  
   4.289  lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::int)"
   4.290 -by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
   4.291 +by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   4.292  
   4.293  lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::int)"
   4.294 -by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
   4.295 +by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   4.296  
   4.297  lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::int)"
   4.298 -by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
   4.299 +by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   4.300  
   4.301  lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::rat)"
   4.302 -by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
   4.303 +by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   4.304  
   4.305  lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::rat)"
   4.306 -by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
   4.307 +by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   4.308  
   4.309  lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::rat)"
   4.310 -by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
   4.311 +by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   4.312  
   4.313  lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::rat)"
   4.314 -by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
   4.315 +by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   4.316  
   4.317  lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::rat)"
   4.318 -by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
   4.319 +by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   4.320  
   4.321  lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::rat)"
   4.322 -by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
   4.323 +by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   4.324  
   4.325  
   4.326  subsection {* @{text field_cancel_numeral_factor} *}
   4.327 @@ -298,66 +284,66 @@
   4.328  subsection {* @{text ring_eq_cancel_factor} *}
   4.329  
   4.330  lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::int)"
   4.331 -by (tactic {* test [ring_eq_cancel_factor] *}) fact
   4.332 +by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   4.333  
   4.334  lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::int)"
   4.335 -by (tactic {* test [ring_eq_cancel_factor] *}) fact
   4.336 +by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   4.337  
   4.338  lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::int)"
   4.339 -by (tactic {* test [ring_eq_cancel_factor] *}) fact
   4.340 +by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   4.341  
   4.342  lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::int)*(x*a)"
   4.343 -by (tactic {* test [ring_eq_cancel_factor] *}) fact
   4.344 +by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   4.345  
   4.346  lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::rat)"
   4.347 -by (tactic {* test [ring_eq_cancel_factor] *}) fact
   4.348 +by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   4.349  
   4.350  lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::rat)"
   4.351 -by (tactic {* test [ring_eq_cancel_factor] *}) fact
   4.352 +by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   4.353  
   4.354  lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::rat)"
   4.355 -by (tactic {* test [ring_eq_cancel_factor] *}) fact
   4.356 +by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   4.357  
   4.358  lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::rat)*(x*a)"
   4.359 -by (tactic {* test [ring_eq_cancel_factor] *}) fact
   4.360 +by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   4.361  
   4.362  
   4.363  subsection {* @{text int_div_cancel_factor} *}
   4.364  
   4.365  lemma assumes "(if k = 0 then 0 else x div y) = uu"
   4.366    shows "(x*k) div (k*(y::int)) = (uu::int)"
   4.367 -by (tactic {* test [int_div_cancel_factor] *}) fact
   4.368 +by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
   4.369  
   4.370  lemma assumes "(if k = 0 then 0 else 1 div y) = uu"
   4.371    shows "(k) div (k*(y::int)) = (uu::int)"
   4.372 -by (tactic {* test [int_div_cancel_factor] *}) fact
   4.373 +by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
   4.374  
   4.375  lemma assumes "(if b = 0 then 0 else a * c) = uu"
   4.376    shows "(a*(b*c)) div ((b::int)) = (uu::int)"
   4.377 -by (tactic {* test [int_div_cancel_factor] *}) fact
   4.378 +by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
   4.379  
   4.380  lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
   4.381    shows "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)"
   4.382 -by (tactic {* test [int_div_cancel_factor] *}) fact
   4.383 +by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
   4.384  
   4.385  
   4.386  subsection {* @{text divide_cancel_factor} *}
   4.387  
   4.388  lemma assumes "(if k = 0 then 0 else x / y) = uu"
   4.389    shows "(x*k) / (k*(y::rat)) = (uu::rat)"
   4.390 -by (tactic {* test [divide_cancel_factor] *}) fact
   4.391 +by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
   4.392  
   4.393  lemma assumes "(if k = 0 then 0 else 1 / y) = uu"
   4.394    shows "(k) / (k*(y::rat)) = (uu::rat)"
   4.395 -by (tactic {* test [divide_cancel_factor] *}) fact
   4.396 +by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
   4.397  
   4.398  lemma assumes "(if b = 0 then 0 else a * c / 1) = uu"
   4.399    shows "(a*(b*c)) / ((b::rat)) = (uu::rat)"
   4.400 -by (tactic {* test [divide_cancel_factor] *}) fact
   4.401 +by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
   4.402  
   4.403  lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu"
   4.404    shows "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)"
   4.405 -by (tactic {* test [divide_cancel_factor] *}) fact
   4.406 +by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
   4.407  
   4.408  lemma shows "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z"
   4.409  oops -- "FIXME: need simproc to cover this case"
   4.410 @@ -366,40 +352,40 @@
   4.411  subsection {* @{text linordered_ring_less_cancel_factor} *}
   4.412  
   4.413  lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < y*z"
   4.414 -by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
   4.415 +by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
   4.416  
   4.417  lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < z*y"
   4.418 -by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
   4.419 +by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
   4.420  
   4.421  lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < y*z"
   4.422 -by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
   4.423 +by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
   4.424  
   4.425  lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < z*y"
   4.426 -by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
   4.427 +by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
   4.428  
   4.429  
   4.430  subsection {* @{text linordered_ring_le_cancel_factor} *}
   4.431  
   4.432  lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> x*z \<le> y*z"
   4.433 -by (tactic {* test [linordered_ring_le_cancel_factor] *}) fact
   4.434 +by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
   4.435  
   4.436  lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> z*x \<le> z*y"
   4.437 -by (tactic {* test [linordered_ring_le_cancel_factor] *}) fact
   4.438 +by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
   4.439  
   4.440  
   4.441  subsection {* @{text field_combine_numerals} *}
   4.442  
   4.443  lemma assumes "5 / 6 * x = uu" shows "(x::rat) / 2 + x / 3 = uu"
   4.444 -by (tactic {* test [field_combine_numerals] *}) fact
   4.445 +by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
   4.446  
   4.447  lemma assumes "6 / 9 * x + y = uu" shows "(x::rat) / 3 + y + x / 3 = uu"
   4.448 -by (tactic {* test [field_combine_numerals] *}) fact
   4.449 +by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
   4.450  
   4.451  lemma assumes "9 / 9 * x = uu" shows "2 * (x::rat) / 3 + x / 3 = uu"
   4.452 -by (tactic {* test [field_combine_numerals] *}) fact
   4.453 +by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
   4.454  
   4.455  lemma "2/3 * (x::rat) + x / 3 = uu"
   4.456 -apply (tactic {* test [field_combine_numerals] *})?
   4.457 +apply (tactic {* test [@{simproc field_combine_numerals}] *})?
   4.458  oops -- "FIXME: test fails"
   4.459  
   4.460