add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
authorhuffman
Wed Nov 09 10:58:08 2011 +0100 (2011-11-09)
changeset 45435d660c4b9daa6
parent 45415 bf39b07a7a8e
child 45436 62bc9474d04b
add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type
s not in this class);
test simprocs using most general type classes instead of just int and rat.
src/HOL/Numeral_Simprocs.thy
src/HOL/ex/Simproc_Tests.thy
     1.1 --- a/src/HOL/Numeral_Simprocs.thy	Wed Nov 09 14:47:38 2011 +1100
     1.2 +++ b/src/HOL/Numeral_Simprocs.thy	Wed Nov 09 10:58:08 2011 +0100
     1.3 @@ -103,8 +103,8 @@
     1.4    {* fn phi => Numeral_Simprocs.combine_numerals *}
     1.5  
     1.6  simproc_setup field_combine_numerals
     1.7 -  ("(i::'a::{field_inverse_zero, number_ring}) + j"
     1.8 -  |"(i::'a::{field_inverse_zero, number_ring}) - j") =
     1.9 +  ("(i::'a::{field_inverse_zero,ring_char_0,number_ring}) + j"
    1.10 +  |"(i::'a::{field_inverse_zero,ring_char_0,number_ring}) - j") =
    1.11    {* fn phi => Numeral_Simprocs.field_combine_numerals *}
    1.12  
    1.13  simproc_setup inteq_cancel_numerals
    1.14 @@ -141,8 +141,8 @@
    1.15    {* fn phi => Numeral_Simprocs.le_cancel_numerals *}
    1.16  
    1.17  simproc_setup ring_eq_cancel_numeral_factor
    1.18 -  ("(l::'a::{idom,number_ring}) * m = n"
    1.19 -  |"(l::'a::{idom,number_ring}) = m * n") =
    1.20 +  ("(l::'a::{idom,ring_char_0,number_ring}) * m = n"
    1.21 +  |"(l::'a::{idom,ring_char_0,number_ring}) = m * n") =
    1.22    {* fn phi => Numeral_Simprocs.eq_cancel_numeral_factor *}
    1.23  
    1.24  simproc_setup ring_less_cancel_numeral_factor
    1.25 @@ -156,14 +156,14 @@
    1.26    {* fn phi => Numeral_Simprocs.le_cancel_numeral_factor *}
    1.27  
    1.28  simproc_setup int_div_cancel_numeral_factors
    1.29 -  ("((l::'a::{semiring_div,number_ring}) * m) div n"
    1.30 -  |"(l::'a::{semiring_div,number_ring}) div (m * n)") =
    1.31 +  ("((l::'a::{semiring_div,ring_char_0,number_ring}) * m) div n"
    1.32 +  |"(l::'a::{semiring_div,ring_char_0,number_ring}) div (m * n)") =
    1.33    {* fn phi => Numeral_Simprocs.div_cancel_numeral_factor *}
    1.34  
    1.35  simproc_setup divide_cancel_numeral_factor
    1.36 -  ("((l::'a::{field_inverse_zero,number_ring}) * m) / n"
    1.37 -  |"(l::'a::{field_inverse_zero,number_ring}) / (m * n)"
    1.38 -  |"((number_of v)::'a::{field_inverse_zero,number_ring}) / (number_of w)") =
    1.39 +  ("((l::'a::{field_inverse_zero,ring_char_0,number_ring}) * m) / n"
    1.40 +  |"(l::'a::{field_inverse_zero,ring_char_0,number_ring}) / (m * n)"
    1.41 +  |"((number_of v)::'a::{field_inverse_zero,ring_char_0,number_ring}) / (number_of w)") =
    1.42    {* fn phi => Numeral_Simprocs.divide_cancel_numeral_factor *}
    1.43  
    1.44  simproc_setup ring_eq_cancel_factor
     2.1 --- a/src/HOL/ex/Simproc_Tests.thy	Wed Nov 09 14:47:38 2011 +1100
     2.2 +++ b/src/HOL/ex/Simproc_Tests.thy	Wed Nov 09 10:58:08 2011 +0100
     2.3 @@ -24,323 +24,305 @@
     2.4  
     2.5  subsection {* @{text int_combine_numerals} *}
     2.6  
     2.7 -lemma assumes "10 + (2 * l + oo) = uu"
     2.8 -  shows "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"
     2.9 -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    2.10 -
    2.11 -lemma assumes "-3 + (i + (j + k)) = y"
    2.12 -  shows "(i + j + 12 + (k::int)) - 15 = y"
    2.13 -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    2.14 -
    2.15 -lemma assumes "7 + (i + (j + k)) = y"
    2.16 -  shows "(i + j + 12 + (k::int)) - 5 = y"
    2.17 -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    2.18 -
    2.19 -lemma assumes "-4 * (u * v) + (2 * x + y) = w"
    2.20 -  shows "(2*x - (u*v) + y) - v*3*u = (w::int)"
    2.21 -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    2.22 -
    2.23 -lemma assumes "Numeral0 * (u*v) + (2 * x * u * v + y) = w"
    2.24 -  shows "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"
    2.25 -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    2.26 -
    2.27 -lemma assumes "3 * (u * v) + (2 * x * u * v + y) = w"
    2.28 -  shows "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"
    2.29 -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    2.30 -
    2.31 -lemma assumes "-3 * (u * v) + (- (x * u * v) + - y) = w"
    2.32 -  shows "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"
    2.33 -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    2.34 -
    2.35 -lemma assumes "Numeral0 * b + (a + - c) = d"
    2.36 -  shows "a + -(b+c) + b = (d::int)"
    2.37 -apply (simp only: minus_add_distrib)
    2.38 -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    2.39 -
    2.40 -lemma assumes "-2 * b + (a + - c) = d"
    2.41 -  shows "a + -(b+c) - b = (d::int)"
    2.42 -apply (simp only: minus_add_distrib)
    2.43 -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    2.44 -
    2.45 -lemma assumes "-7 + (i + (j + (k + (- u + - y)))) = zz"
    2.46 -  shows "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"
    2.47 -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    2.48 -
    2.49 -lemma assumes "-27 + (i + (j + k)) = y"
    2.50 -  shows "(i + j + -12 + (k::int)) - 15 = y"
    2.51 -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    2.52 -
    2.53 -lemma assumes "27 + (i + (j + k)) = y"
    2.54 -  shows "(i + j + 12 + (k::int)) - -15 = y"
    2.55 -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    2.56 -
    2.57 -lemma assumes "3 + (i + (j + k)) = y"
    2.58 -  shows "(i + j + -12 + (k::int)) - -15 = y"
    2.59 -by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    2.60 -
    2.61 +notepad begin
    2.62 +  fix a b c d oo uu i j k l u v w x y z :: "'a::number_ring"
    2.63 +  {
    2.64 +    assume "10 + (2 * l + oo) = uu"
    2.65 +    have "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = uu"
    2.66 +      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    2.67 +  next
    2.68 +    assume "-3 + (i + (j + k)) = y"
    2.69 +    have "(i + j + 12 + k) - 15 = y"
    2.70 +      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    2.71 +  next
    2.72 +    assume "7 + (i + (j + k)) = y"
    2.73 +    have "(i + j + 12 + k) - 5 = y"
    2.74 +      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    2.75 +  next
    2.76 +    assume "-4 * (u * v) + (2 * x + y) = w"
    2.77 +    have "(2*x - (u*v) + y) - v*3*u = w"
    2.78 +      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    2.79 +  next
    2.80 +    assume "Numeral0 * (u*v) + (2 * x * u * v + y) = w"
    2.81 +    have "(2*x*u*v + (u*v)*4 + y) - v*u*4 = w"
    2.82 +      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    2.83 +  next
    2.84 +    assume "3 * (u * v) + (2 * x * u * v + y) = w"
    2.85 +    have "(2*x*u*v + (u*v)*4 + y) - v*u = w"
    2.86 +      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    2.87 +  next
    2.88 +    assume "-3 * (u * v) + (- (x * u * v) + - y) = w"
    2.89 +    have "u*v - (x*u*v + (u*v)*4 + y) = w"
    2.90 +      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    2.91 +  next
    2.92 +    assume "Numeral0 * b + (a + - c) = d"
    2.93 +    have "a + -(b+c) + b = d"
    2.94 +      apply (simp only: minus_add_distrib)
    2.95 +      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
    2.96 +  next
    2.97 +    assume "-2 * b + (a + - c) = d"
    2.98 +    have "a + -(b+c) - b = d"
    2.99 +      apply (simp only: minus_add_distrib)
   2.100 +      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
   2.101 +  next
   2.102 +    assume "-7 + (i + (j + (k + (- u + - y)))) = z"
   2.103 +    have "(i + j + -2 + k) - (u + 5 + y) = z"
   2.104 +      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
   2.105 +  next
   2.106 +    assume "-27 + (i + (j + k)) = y"
   2.107 +    have "(i + j + -12 + k) - 15 = y"
   2.108 +      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
   2.109 +  next
   2.110 +    assume "27 + (i + (j + k)) = y"
   2.111 +    have "(i + j + 12 + k) - -15 = y"
   2.112 +      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
   2.113 +  next
   2.114 +    assume "3 + (i + (j + k)) = y"
   2.115 +    have "(i + j + -12 + k) - -15 = y"
   2.116 +      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
   2.117 +  }
   2.118 +end
   2.119  
   2.120  subsection {* @{text inteq_cancel_numerals} *}
   2.121  
   2.122 -lemma assumes "u = Numeral0" shows "2*u = (u::int)"
   2.123 -by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
   2.124 +notepad begin
   2.125 +  fix i j k u vv w y z w' y' z' :: "'a::number_ring"
   2.126 +  {
   2.127 +    assume "u = Numeral0" have "2*u = u"
   2.128 +      by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
   2.129  (* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *)
   2.130 -
   2.131 -lemma assumes "i + (j + k) = 3 + (u + y)"
   2.132 -  shows "(i + j + 12 + (k::int)) = u + 15 + y"
   2.133 -by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
   2.134 -
   2.135 -lemma assumes "7 + (j + (i + k)) = y"
   2.136 -  shows "(i + j*2 + 12 + (k::int)) = j + 5 + y"
   2.137 -by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
   2.138 -
   2.139 -lemma assumes "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))"
   2.140 -  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)"
   2.141 -by (tactic {* test [@{simproc int_combine_numerals}, @{simproc inteq_cancel_numerals}] *}) fact
   2.142 -
   2.143 +  next
   2.144 +    assume "i + (j + k) = 3 + (u + y)"
   2.145 +    have "(i + j + 12 + k) = u + 15 + y"
   2.146 +      by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
   2.147 +  next
   2.148 +    assume "7 + (j + (i + k)) = y"
   2.149 +    have "(i + j*2 + 12 + k) = j + 5 + y"
   2.150 +      by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
   2.151 +  next
   2.152 +    assume "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))"
   2.153 +    have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + vv"
   2.154 +      by (tactic {* test [@{simproc int_combine_numerals}, @{simproc inteq_cancel_numerals}] *}) fact
   2.155 +  }
   2.156 +end
   2.157  
   2.158  subsection {* @{text intless_cancel_numerals} *}
   2.159  
   2.160 -lemma assumes "y < 2 * b" shows "y - b < (b::int)"
   2.161 -by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
   2.162 -
   2.163 -lemma assumes "c + y < 4 * b" shows "y - (3*b + c) < (b::int) - 2*c"
   2.164 -by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
   2.165 -
   2.166 -lemma assumes "i + (j + k) < 8 + (u + y)"
   2.167 -  shows "(i + j + -3 + (k::int)) < u + 5 + y"
   2.168 -by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
   2.169 -
   2.170 -lemma assumes "9 + (i + (j + k)) < u + y"
   2.171 -  shows "(i + j + 3 + (k::int)) < u + -6 + y"
   2.172 -by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
   2.173 -
   2.174 +notepad begin
   2.175 +  fix b c i j k u y :: "'a::{linordered_idom,number_ring}"
   2.176 +  {
   2.177 +    assume "y < 2 * b" have "y - b < b"
   2.178 +      by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
   2.179 +  next
   2.180 +    assume "c + y < 4 * b" have "y - (3*b + c) < b - 2*c"
   2.181 +      by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
   2.182 +  next
   2.183 +    assume "i + (j + k) < 8 + (u + y)"
   2.184 +    have "(i + j + -3 + k) < u + 5 + y"
   2.185 +      by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
   2.186 +  next
   2.187 +    assume "9 + (i + (j + k)) < u + y"
   2.188 +    have "(i + j + 3 + k) < u + -6 + y"
   2.189 +      by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
   2.190 +  }
   2.191 +end
   2.192  
   2.193  subsection {* @{text ring_eq_cancel_numeral_factor} *}
   2.194  
   2.195 -lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::int)"
   2.196 -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   2.197 -
   2.198 -lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::int)"
   2.199 -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   2.200 -
   2.201 +notepad begin
   2.202 +  fix x y :: "'a::{idom,ring_char_0,number_ring}"
   2.203 +  {
   2.204 +    assume "3*x = 4*y" have "9*x = 12 * y"
   2.205 +      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   2.206 +  next
   2.207 +    assume "-3*x = 4*y" have "-99*x = 132 * y"
   2.208 +      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   2.209 +  next
   2.210 +    assume "111*x = -44*y" have "999*x = -396 * y"
   2.211 +      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   2.212 +  next
   2.213 +    assume "11*x = 9*y" have "-99*x = -81 * y"
   2.214 +      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   2.215 +  next
   2.216 +    assume "2*x = Numeral1*y" have "-2 * x = -1 * y"
   2.217 +      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   2.218 +  next
   2.219 +    assume "2*x = Numeral1*y" have "-2 * x = -y"
   2.220 +      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   2.221 +  }
   2.222 +end
   2.223  
   2.224  subsection {* @{text int_div_cancel_numeral_factors} *}
   2.225  
   2.226 -lemma assumes "(3*x) div (4*y) = z" shows "(9*x) div (12*y) = (z::int)"
   2.227 -by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
   2.228 -
   2.229 -lemma assumes "(-3*x) div (4*y) = z" shows "(-99*x) div (132*y) = (z::int)"
   2.230 -by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
   2.231 -
   2.232 -lemma assumes "(111*x) div (-44*y) = z" shows "(999*x) div (-396*y) = (z::int)"
   2.233 -by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
   2.234 -
   2.235 -lemma assumes "(11*x) div (9*y) = z" shows "(-99*x) div (-81*y) = (z::int)"
   2.236 -by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
   2.237 -
   2.238 -lemma assumes "(2*x) div (Numeral1*y) = z"
   2.239 -  shows "(-2 * x) div (-1 * (y::int)) = z"
   2.240 -by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
   2.241 -
   2.242 +notepad begin
   2.243 +  fix x y z :: "'a::{semiring_div,ring_char_0,number_ring}"
   2.244 +  {
   2.245 +    assume "(3*x) div (4*y) = z" have "(9*x) div (12*y) = z"
   2.246 +      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
   2.247 +  next
   2.248 +    assume "(-3*x) div (4*y) = z" have "(-99*x) div (132*y) = z"
   2.249 +      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
   2.250 +  next
   2.251 +    assume "(111*x) div (-44*y) = z" have "(999*x) div (-396*y) = z"
   2.252 +      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
   2.253 +  next
   2.254 +    assume "(11*x) div (9*y) = z" have "(-99*x) div (-81*y) = z"
   2.255 +      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
   2.256 +  next
   2.257 +    assume "(2*x) div (Numeral1*y) = z"
   2.258 +    have "(-2 * x) div (-1 * y) = z"
   2.259 +      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
   2.260 +  }
   2.261 +end
   2.262  
   2.263  subsection {* @{text ring_less_cancel_numeral_factor} *}
   2.264  
   2.265 -lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::int)"
   2.266 -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   2.267 -
   2.268 -lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::int)"
   2.269 -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   2.270 -
   2.271 -lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::int)"
   2.272 -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   2.273 -
   2.274 -lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::int)"
   2.275 -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   2.276 -
   2.277 -lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::int)"
   2.278 -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   2.279 -
   2.280 -lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::int)"
   2.281 -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   2.282 -
   2.283 -lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::rat)"
   2.284 -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   2.285 -
   2.286 -lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::rat)"
   2.287 -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   2.288 -
   2.289 -lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::rat)"
   2.290 -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   2.291 -
   2.292 -lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::rat)"
   2.293 -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   2.294 -
   2.295 -lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::rat)"
   2.296 -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   2.297 -
   2.298 -lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::rat)"
   2.299 -by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   2.300 -
   2.301 +notepad begin
   2.302 +  fix x y :: "'a::{linordered_idom,number_ring}"
   2.303 +  {
   2.304 +    assume "3*x < 4*y" have "9*x < 12 * y"
   2.305 +      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   2.306 +  next
   2.307 +    assume "-3*x < 4*y" have "-99*x < 132 * y"
   2.308 +      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   2.309 +  next
   2.310 +    assume "111*x < -44*y" have "999*x < -396 * y"
   2.311 +      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   2.312 +  next
   2.313 +    assume "9*y < 11*x" have "-99*x < -81 * y"
   2.314 +      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   2.315 +  next
   2.316 +    assume "Numeral1*y < 2*x" have "-2 * x < -y"
   2.317 +      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   2.318 +  next
   2.319 +    assume "23*y < Numeral1*x" have "-x < -23 * y"
   2.320 +      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
   2.321 +  }
   2.322 +end
   2.323  
   2.324  subsection {* @{text ring_le_cancel_numeral_factor} *}
   2.325  
   2.326 -lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::int)"
   2.327 -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.328 -
   2.329 -lemma assumes "-3*x \<le> 4*y" shows "-99*x \<le> 132 * (y::int)"
   2.330 -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.331 -
   2.332 -lemma assumes "111*x \<le> -44*y" shows "999*x \<le> -396 * (y::int)"
   2.333 -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.334 -
   2.335 -lemma assumes "9*y \<le> 11*x" shows "-99*x \<le> -81 * (y::int)"
   2.336 -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.337 -
   2.338 -lemma assumes "Numeral1*y \<le> 2*x" shows "-2 * x \<le> -1 * (y::int)"
   2.339 -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.340 -
   2.341 -lemma assumes "23*y \<le> Numeral1*x" shows "-x \<le> -23 * (y::int)"
   2.342 -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.343 -
   2.344 -lemma assumes "Numeral1*y \<le> Numeral0" shows "0 \<le> (y::rat) * -2"
   2.345 -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.346 -
   2.347 -lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::rat)"
   2.348 -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.349 -
   2.350 -lemma assumes "-3*x \<le> 4*y" shows "-99*x \<le> 132 * (y::rat)"
   2.351 -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.352 -
   2.353 -lemma assumes "111*x \<le> -44*y" shows "999*x \<le> -396 * (y::rat)"
   2.354 -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.355 -
   2.356 -lemma assumes "-1*x \<le> Numeral1*y" shows "- ((2::rat) * x) \<le> 2*y"
   2.357 -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.358 -
   2.359 -lemma assumes "9*y \<le> 11*x" shows "-99*x \<le> -81 * (y::rat)"
   2.360 -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.361 -
   2.362 -lemma assumes "Numeral1*y \<le> 2*x" shows "-2 * x \<le> -1 * (y::rat)"
   2.363 -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.364 -
   2.365 -lemma assumes "23*y \<le> Numeral1*x" shows "-x \<le> -23 * (y::rat)"
   2.366 -by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.367 -
   2.368 -
   2.369 -subsection {* @{text ring_eq_cancel_numeral_factor} *}
   2.370 -
   2.371 -lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::int)"
   2.372 -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   2.373 -
   2.374 -lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::int)"
   2.375 -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   2.376 -
   2.377 -lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::int)"
   2.378 -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   2.379 -
   2.380 -lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::int)"
   2.381 -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   2.382 -
   2.383 -lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::rat)"
   2.384 -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   2.385 -
   2.386 -lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::rat)"
   2.387 -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   2.388 -
   2.389 -lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::rat)"
   2.390 -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   2.391 -
   2.392 -lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::rat)"
   2.393 -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   2.394 -
   2.395 -lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::rat)"
   2.396 -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   2.397 -
   2.398 -lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::rat)"
   2.399 -by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
   2.400 -
   2.401 +notepad begin
   2.402 +  fix x y :: "'a::{linordered_idom,number_ring}"
   2.403 +  {
   2.404 +    assume "3*x \<le> 4*y" have "9*x \<le> 12 * y"
   2.405 +      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.406 +  next
   2.407 +    assume "-3*x \<le> 4*y" have "-99*x \<le> 132 * y"
   2.408 +      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.409 +  next
   2.410 +    assume "111*x \<le> -44*y" have "999*x \<le> -396 * y"
   2.411 +      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.412 +  next
   2.413 +    assume "9*y \<le> 11*x" have "-99*x \<le> -81 * y"
   2.414 +      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.415 +  next
   2.416 +    assume "Numeral1*y \<le> 2*x" have "-2 * x \<le> -1 * y"
   2.417 +      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.418 +  next
   2.419 +    assume "23*y \<le> Numeral1*x" have "-x \<le> -23 * y"
   2.420 +      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.421 +  next
   2.422 +    assume "Numeral1*y \<le> Numeral0" have "0 \<le> y * -2"
   2.423 +      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.424 +  next
   2.425 +    assume "-1*x \<le> Numeral1*y" have "- (2 * x) \<le> 2*y"
   2.426 +      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
   2.427 +  }
   2.428 +end
   2.429  
   2.430  subsection {* @{text divide_cancel_numeral_factor} *}
   2.431  
   2.432 -lemma assumes "(3*x) / (4*y) = z" shows "(9*x) / (12 * (y::rat)) = z"
   2.433 -by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
   2.434 -
   2.435 -lemma assumes "(-3*x) / (4*y) = z" shows "(-99*x) / (132 * (y::rat)) = z"
   2.436 -by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
   2.437 -
   2.438 -lemma assumes "(111*x) / (-44*y) = z" shows "(999*x) / (-396 * (y::rat)) = z"
   2.439 -by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
   2.440 -
   2.441 -lemma assumes "(11*x) / (9*y) = z" shows "(-99*x) / (-81 * (y::rat)) = z"
   2.442 -by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
   2.443 -
   2.444 -lemma assumes "(2*x) / (Numeral1*y) = z" shows "(-2 * x) / (-1 * (y::rat)) = z"
   2.445 -by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
   2.446 -
   2.447 +notepad begin
   2.448 +  fix x y z :: "'a::{field_inverse_zero,ring_char_0,number_ring}"
   2.449 +  {
   2.450 +    assume "(3*x) / (4*y) = z" have "(9*x) / (12 * y) = z"
   2.451 +      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
   2.452 +  next
   2.453 +    assume "(-3*x) / (4*y) = z" have "(-99*x) / (132 * y) = z"
   2.454 +      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
   2.455 +  next
   2.456 +    assume "(111*x) / (-44*y) = z" have "(999*x) / (-396 * y) = z"
   2.457 +      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
   2.458 +  next
   2.459 +    assume "(11*x) / (9*y) = z" have "(-99*x) / (-81 * y) = z"
   2.460 +      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
   2.461 +  next
   2.462 +    assume "(2*x) / (Numeral1*y) = z" have "(-2 * x) / (-1 * y) = z"
   2.463 +      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
   2.464 +  }
   2.465 +end
   2.466  
   2.467  subsection {* @{text ring_eq_cancel_factor} *}
   2.468  
   2.469 -lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::int)"
   2.470 -by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   2.471 -
   2.472 -lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::int)"
   2.473 -by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   2.474 -
   2.475 -lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::int)"
   2.476 -by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   2.477 -
   2.478 -lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::int)*(x*a)"
   2.479 -by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   2.480 -
   2.481 -lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::rat)"
   2.482 -by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   2.483 -
   2.484 -lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::rat)"
   2.485 -by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   2.486 -
   2.487 -lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::rat)"
   2.488 -by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   2.489 -
   2.490 -lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::rat)*(x*a)"
   2.491 -by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   2.492 -
   2.493 +notepad begin
   2.494 +  fix a b c d k x y :: "'a::idom"
   2.495 +  {
   2.496 +    assume "k = 0 \<or> x = y" have "x*k = k*y"
   2.497 +      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   2.498 +  next
   2.499 +    assume "k = 0 \<or> 1 = y" have "k = k*y"
   2.500 +      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   2.501 +  next
   2.502 +    assume "b = 0 \<or> a*c = 1" have "a*(b*c) = b"
   2.503 +      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   2.504 +  next
   2.505 +    assume "a = 0 \<or> b = 0 \<or> c = d*x" have "a*(b*c) = d*b*(x*a)"
   2.506 +      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   2.507 +  next
   2.508 +    assume "k = 0 \<or> x = y" have "x*k = k*y"
   2.509 +      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   2.510 +  next
   2.511 +    assume "k = 0 \<or> 1 = y" have "k = k*y"
   2.512 +      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
   2.513 +  }
   2.514 +end
   2.515  
   2.516  subsection {* @{text int_div_cancel_factor} *}
   2.517  
   2.518 -lemma assumes "(if k = 0 then 0 else x div y) = uu"
   2.519 -  shows "(x*k) div (k*(y::int)) = (uu::int)"
   2.520 -by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
   2.521 -
   2.522 -lemma assumes "(if k = 0 then 0 else 1 div y) = uu"
   2.523 -  shows "(k) div (k*(y::int)) = (uu::int)"
   2.524 -by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
   2.525 -
   2.526 -lemma assumes "(if b = 0 then 0 else a * c) = uu"
   2.527 -  shows "(a*(b*c)) div ((b::int)) = (uu::int)"
   2.528 -by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
   2.529 -
   2.530 -lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
   2.531 -  shows "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)"
   2.532 -by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
   2.533 -
   2.534 +notepad begin
   2.535 +  fix a b c d k uu x y :: "'a::semiring_div"
   2.536 +  {
   2.537 +    assume "(if k = 0 then 0 else x div y) = uu"
   2.538 +    have "(x*k) div (k*y) = uu"
   2.539 +      by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
   2.540 +  next
   2.541 +    assume "(if k = 0 then 0 else 1 div y) = uu"
   2.542 +    have "(k) div (k*y) = uu"
   2.543 +      by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
   2.544 +  next
   2.545 +    assume "(if b = 0 then 0 else a * c) = uu"
   2.546 +    have "(a*(b*c)) div b = uu"
   2.547 +      by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
   2.548 +  next
   2.549 +    assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
   2.550 +    have "(a*(b*c)) div (d*b*(x*a)) = uu"
   2.551 +      by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
   2.552 +  }
   2.553 +end
   2.554  
   2.555  subsection {* @{text divide_cancel_factor} *}
   2.556  
   2.557 -lemma assumes "(if k = 0 then 0 else x / y) = uu"
   2.558 -  shows "(x*k) / (k*(y::rat)) = (uu::rat)"
   2.559 -by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
   2.560 -
   2.561 -lemma assumes "(if k = 0 then 0 else 1 / y) = uu"
   2.562 -  shows "(k) / (k*(y::rat)) = (uu::rat)"
   2.563 -by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
   2.564 -
   2.565 -lemma assumes "(if b = 0 then 0 else a * c / 1) = uu"
   2.566 -  shows "(a*(b*c)) / ((b::rat)) = (uu::rat)"
   2.567 -by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
   2.568 -
   2.569 -lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu"
   2.570 -  shows "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)"
   2.571 -by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
   2.572 +notepad begin
   2.573 +  fix a b c d k uu x y :: "'a::field_inverse_zero"
   2.574 +  {
   2.575 +    assume "(if k = 0 then 0 else x / y) = uu"
   2.576 +    have "(x*k) / (k*y) = uu"
   2.577 +      by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
   2.578 +  next
   2.579 +    assume "(if k = 0 then 0 else 1 / y) = uu"
   2.580 +    have "(k) / (k*y) = uu"
   2.581 +      by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
   2.582 +  next
   2.583 +    assume "(if b = 0 then 0 else a * c / 1) = uu"
   2.584 +    have "(a*(b*c)) / b = uu"
   2.585 +      by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
   2.586 +  next
   2.587 +    assume "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu"
   2.588 +    have "(a*(b*c)) / (d*b*(x*a)) = uu"
   2.589 +      by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
   2.590 +  }
   2.591 +end
   2.592  
   2.593  lemma shows "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z"
   2.594  oops -- "FIXME: need simproc to cover this case"
   2.595 @@ -348,38 +330,51 @@
   2.596  
   2.597  subsection {* @{text linordered_ring_less_cancel_factor} *}
   2.598  
   2.599 -lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < y*z"
   2.600 -by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
   2.601 -
   2.602 -lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < z*y"
   2.603 -by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
   2.604 -
   2.605 -lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < y*z"
   2.606 -by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
   2.607 -
   2.608 -lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < z*y"
   2.609 -by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
   2.610 -
   2.611 +notepad begin
   2.612 +  fix x y z :: "'a::linordered_idom"
   2.613 +  {
   2.614 +    assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> x*z < y*z"
   2.615 +      by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
   2.616 +  next
   2.617 +    assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> x*z < z*y"
   2.618 +      by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
   2.619 +  next
   2.620 +    assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> z*x < y*z"
   2.621 +      by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
   2.622 +  next
   2.623 +    assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> z*x < z*y"
   2.624 +      by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
   2.625 +  }
   2.626 +end
   2.627  
   2.628  subsection {* @{text linordered_ring_le_cancel_factor} *}
   2.629  
   2.630 -lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> x*z \<le> y*z"
   2.631 -by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
   2.632 -
   2.633 -lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> z*x \<le> z*y"
   2.634 -by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
   2.635 -
   2.636 +notepad begin
   2.637 +  fix x y z :: "'a::linordered_idom"
   2.638 +  {
   2.639 +    assume "0 < z \<Longrightarrow> x \<le> y" have "0 < z \<Longrightarrow> x*z \<le> y*z"
   2.640 +      by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
   2.641 +  next
   2.642 +    assume "0 < z \<Longrightarrow> x \<le> y" have "0 < z \<Longrightarrow> z*x \<le> z*y"
   2.643 +      by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
   2.644 +  }
   2.645 +end
   2.646  
   2.647  subsection {* @{text field_combine_numerals} *}
   2.648  
   2.649 -lemma assumes "5 / 6 * x = uu" shows "(x::rat) / 2 + x / 3 = uu"
   2.650 -by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
   2.651 -
   2.652 -lemma assumes "6 / 9 * x + y = uu" shows "(x::rat) / 3 + y + x / 3 = uu"
   2.653 -by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
   2.654 -
   2.655 -lemma assumes "9 / 9 * x = uu" shows "2 * (x::rat) / 3 + x / 3 = uu"
   2.656 -by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
   2.657 +notepad begin
   2.658 +  fix x uu :: "'a::{field_inverse_zero,ring_char_0,number_ring}"
   2.659 +  {
   2.660 +    assume "5 / 6 * x = uu" have "x / 2 + x / 3 = uu"
   2.661 +      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
   2.662 +  next
   2.663 +    assume "6 / 9 * x + y = uu" have "x / 3 + y + x / 3 = uu"
   2.664 +      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
   2.665 +  next
   2.666 +    assume "9 / 9 * x = uu" have "2 * x / 3 + x / 3 = uu"
   2.667 +      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
   2.668 +  }
   2.669 +end
   2.670  
   2.671  lemma "2/3 * (x::rat) + x / 3 = uu"
   2.672  apply (tactic {* test [@{simproc field_combine_numerals}] *})?