1.1 --- a/src/HOL/IsaMakefile Thu Oct 20 22:02:49 2011 +0200
1.2 +++ b/src/HOL/IsaMakefile Fri Oct 21 08:42:11 2011 +0200
1.3 @@ -1058,10 +1058,10 @@
1.4 ex/Quickcheck_Narrowing_Examples.thy ex/Quicksort.thy ex/ROOT.ML \
1.5 ex/Records.thy ex/ReflectionEx.thy ex/Refute_Examples.thy \
1.6 ex/SAT_Examples.thy ex/Serbian.thy ex/Set_Theory.thy \
1.7 - ex/Set_Algebras.thy ex/SVC_Oracle.thy ex/sledgehammer_tactics.ML \
1.8 - ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy \
1.9 - ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy \
1.10 - ex/Unification.thy ex/While_Combinator_Example.thy \
1.11 + ex/Set_Algebras.thy ex/Simproc_Tests.thy ex/SVC_Oracle.thy \
1.12 + ex/sledgehammer_tactics.ML ex/Seq.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
1.13 + ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy \
1.14 + ex/Tree23.thy ex/Unification.thy ex/While_Combinator_Example.thy \
1.15 ex/document/root.bib ex/document/root.tex ex/svc_funcs.ML \
1.16 ex/svc_test.thy ../Tools/interpretation_with_defs.ML
1.17 @$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
2.1 --- a/src/HOL/ex/ROOT.ML Thu Oct 20 22:02:49 2011 +0200
2.2 +++ b/src/HOL/ex/ROOT.ML Fri Oct 21 08:42:11 2011 +0200
2.3 @@ -71,7 +71,8 @@
2.4 "Birthday_Paradox",
2.5 "List_to_Set_Comprehension_Examples",
2.6 "Set_Algebras",
2.7 - "Seq"
2.8 + "Seq",
2.9 + "Simproc_Tests"
2.10 ];
2.11
2.12 if getenv "ISABELLE_GHC" = "" then ()
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/ex/Simproc_Tests.thy Fri Oct 21 08:42:11 2011 +0200
3.3 @@ -0,0 +1,417 @@
3.4 +(* Title: HOL/ex/Simproc_Tests.thy
3.5 + Author: Brian Huffman
3.6 +*)
3.7 +
3.8 +header {* Testing of arithmetic simprocs *}
3.9 +
3.10 +theory Simproc_Tests
3.11 +imports Rat
3.12 +begin
3.13 +
3.14 +text {*
3.15 + This theory tests the various simprocs defined in
3.16 + @{file "~~/src/HOL/Numeral_Simprocs.thy"}. Many of the tests
3.17 + are derived from commented-out code originally found in
3.18 + @{file "~~/src/HOL/Tools/numeral_simprocs.ML"}.
3.19 +*}
3.20 +
3.21 +subsection {* ML bindings *}
3.22 +
3.23 +ML {*
3.24 + val semiring_assoc_fold = Numeral_Simprocs.assoc_fold_simproc
3.25 + val int_combine_numerals = Numeral_Simprocs.combine_numerals
3.26 + val field_combine_numerals = Numeral_Simprocs.field_combine_numerals
3.27 + val [inteq_cancel_numerals, intless_cancel_numerals, intle_cancel_numerals]
3.28 + = Numeral_Simprocs.cancel_numerals
3.29 + val [ring_eq_cancel_factor, linordered_ring_le_cancel_factor,
3.30 + linordered_ring_less_cancel_factor, int_div_cancel_factor,
3.31 + int_mod_cancel_factor, dvd_cancel_factor, divide_cancel_factor]
3.32 + = Numeral_Simprocs.cancel_factors
3.33 + val [ring_eq_cancel_numeral_factor, ring_less_cancel_numeral_factor,
3.34 + ring_le_cancel_numeral_factor, int_div_cancel_numeral_factors,
3.35 + divide_cancel_numeral_factor]
3.36 + = Numeral_Simprocs.cancel_numeral_factors
3.37 + val field_combine_numerals = Numeral_Simprocs.field_combine_numerals
3.38 + val [field_eq_cancel_numeral_factor, field_cancel_numeral_factor]
3.39 + = Numeral_Simprocs.field_cancel_numeral_factors
3.40 +
3.41 + fun test ps = CHANGED (asm_simp_tac (HOL_basic_ss addsimprocs ps) 1)
3.42 +*}
3.43 +
3.44 +
3.45 +subsection {* @{text int_combine_numerals} *}
3.46 +
3.47 +lemma assumes "10 + (2 * l + oo) = uu"
3.48 + shows "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"
3.49 +by (tactic {* test [int_combine_numerals] *}) fact
3.50 +
3.51 +lemma assumes "-3 + (i + (j + k)) = y"
3.52 + shows "(i + j + 12 + (k::int)) - 15 = y"
3.53 +by (tactic {* test [int_combine_numerals] *}) fact
3.54 +
3.55 +lemma assumes "7 + (i + (j + k)) = y"
3.56 + shows "(i + j + 12 + (k::int)) - 5 = y"
3.57 +by (tactic {* test [int_combine_numerals] *}) fact
3.58 +
3.59 +lemma assumes "-4 * (u * v) + (2 * x + y) = w"
3.60 + shows "(2*x - (u*v) + y) - v*3*u = (w::int)"
3.61 +by (tactic {* test [int_combine_numerals] *}) fact
3.62 +
3.63 +lemma assumes "Numeral0 * (u*v) + (2 * x * u * v + y) = w"
3.64 + shows "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"
3.65 +by (tactic {* test [int_combine_numerals] *}) fact
3.66 +
3.67 +lemma assumes "3 * (u * v) + (2 * x * u * v + y) = w"
3.68 + shows "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"
3.69 +by (tactic {* test [int_combine_numerals] *}) fact
3.70 +
3.71 +lemma assumes "-3 * (u * v) + (- (x * u * v) + - y) = w"
3.72 + shows "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"
3.73 +by (tactic {* test [int_combine_numerals] *}) fact
3.74 +
3.75 +lemma assumes "Numeral0 * b + (a + - c) = d"
3.76 + shows "a + -(b+c) + b = (d::int)"
3.77 +apply (simp only: minus_add_distrib)
3.78 +by (tactic {* test [int_combine_numerals] *}) fact
3.79 +
3.80 +lemma assumes "-2 * b + (a + - c) = d"
3.81 + shows "a + -(b+c) - b = (d::int)"
3.82 +apply (simp only: minus_add_distrib)
3.83 +by (tactic {* test [int_combine_numerals] *}) fact
3.84 +
3.85 +lemma assumes "-7 + (i + (j + (k + (- u + - y)))) = zz"
3.86 + shows "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"
3.87 +by (tactic {* test [int_combine_numerals] *}) fact
3.88 +
3.89 +lemma assumes "-27 + (i + (j + k)) = y"
3.90 + shows "(i + j + -12 + (k::int)) - 15 = y"
3.91 +by (tactic {* test [int_combine_numerals] *}) fact
3.92 +
3.93 +lemma assumes "27 + (i + (j + k)) = y"
3.94 + shows "(i + j + 12 + (k::int)) - -15 = y"
3.95 +by (tactic {* test [int_combine_numerals] *}) fact
3.96 +
3.97 +lemma assumes "3 + (i + (j + k)) = y"
3.98 + shows "(i + j + -12 + (k::int)) - -15 = y"
3.99 +by (tactic {* test [int_combine_numerals] *}) fact
3.100 +
3.101 +
3.102 +subsection {* @{text inteq_cancel_numerals} *}
3.103 +
3.104 +lemma assumes "u = Numeral0" shows "2*u = (u::int)"
3.105 +by (tactic {* test [inteq_cancel_numerals] *}) fact
3.106 +(* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *)
3.107 +
3.108 +lemma assumes "i + (j + k) = 3 + (u + y)"
3.109 + shows "(i + j + 12 + (k::int)) = u + 15 + y"
3.110 +by (tactic {* test [inteq_cancel_numerals] *}) fact
3.111 +
3.112 +lemma assumes "7 + (j + (i + k)) = y"
3.113 + shows "(i + j*2 + 12 + (k::int)) = j + 5 + y"
3.114 +by (tactic {* test [inteq_cancel_numerals] *}) fact
3.115 +
3.116 +lemma assumes "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))"
3.117 + 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)"
3.118 +by (tactic {* test [int_combine_numerals, inteq_cancel_numerals] *}) fact
3.119 +
3.120 +
3.121 +subsection {* @{text intless_cancel_numerals} *}
3.122 +
3.123 +lemma assumes "y < 2 * b" shows "y - b < (b::int)"
3.124 +by (tactic {* test [intless_cancel_numerals] *}) fact
3.125 +
3.126 +lemma assumes "c + y < 4 * b" shows "y - (3*b + c) < (b::int) - 2*c"
3.127 +by (tactic {* test [intless_cancel_numerals] *}) fact
3.128 +
3.129 +lemma assumes "i + (j + k) < 8 + (u + y)"
3.130 + shows "(i + j + -3 + (k::int)) < u + 5 + y"
3.131 +by (tactic {* test [intless_cancel_numerals] *}) fact
3.132 +
3.133 +lemma assumes "9 + (i + (j + k)) < u + y"
3.134 + shows "(i + j + 3 + (k::int)) < u + -6 + y"
3.135 +by (tactic {* test [intless_cancel_numerals] *}) fact
3.136 +
3.137 +
3.138 +subsection {* @{text ring_eq_cancel_numeral_factor} *}
3.139 +
3.140 +lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::int)"
3.141 +by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
3.142 +
3.143 +lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::int)"
3.144 +by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
3.145 +
3.146 +
3.147 +subsection {* @{text int_div_cancel_numeral_factors} *}
3.148 +
3.149 +lemma assumes "(3*x) div (4*y) = z" shows "(9*x) div (12*y) = (z::int)"
3.150 +by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
3.151 +
3.152 +lemma assumes "(-3*x) div (4*y) = z" shows "(-99*x) div (132*y) = (z::int)"
3.153 +by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
3.154 +
3.155 +lemma assumes "(111*x) div (-44*y) = z" shows "(999*x) div (-396*y) = (z::int)"
3.156 +by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
3.157 +
3.158 +lemma assumes "(11*x) div (9*y) = z" shows "(-99*x) div (-81*y) = (z::int)"
3.159 +by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
3.160 +
3.161 +lemma assumes "(2*x) div (Numeral1*y) = z"
3.162 + shows "(-2 * x) div (-1 * (y::int)) = z"
3.163 +by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
3.164 +
3.165 +
3.166 +subsection {* @{text ring_less_cancel_numeral_factor} *}
3.167 +
3.168 +lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::int)"
3.169 +by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
3.170 +
3.171 +lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::int)"
3.172 +by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
3.173 +
3.174 +lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::int)"
3.175 +by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
3.176 +
3.177 +lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::int)"
3.178 +by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
3.179 +
3.180 +lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::int)"
3.181 +by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
3.182 +
3.183 +lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::int)"
3.184 +by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
3.185 +
3.186 +lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::rat)"
3.187 +by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
3.188 +
3.189 +lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::rat)"
3.190 +by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
3.191 +
3.192 +lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::rat)"
3.193 +by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
3.194 +
3.195 +lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::rat)"
3.196 +by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
3.197 +
3.198 +lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::rat)"
3.199 +by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
3.200 +
3.201 +lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::rat)"
3.202 +by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
3.203 +
3.204 +
3.205 +subsection {* @{text ring_le_cancel_numeral_factor} *}
3.206 +
3.207 +lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::int)"
3.208 +by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
3.209 +
3.210 +lemma assumes "-3*x \<le> 4*y" shows "-99*x \<le> 132 * (y::int)"
3.211 +by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
3.212 +
3.213 +lemma assumes "111*x \<le> -44*y" shows "999*x \<le> -396 * (y::int)"
3.214 +by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
3.215 +
3.216 +lemma assumes "9*y \<le> 11*x" shows "-99*x \<le> -81 * (y::int)"
3.217 +by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
3.218 +
3.219 +lemma assumes "Numeral1*y \<le> 2*x" shows "-2 * x \<le> -1 * (y::int)"
3.220 +by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
3.221 +
3.222 +lemma assumes "23*y \<le> Numeral1*x" shows "-x \<le> -23 * (y::int)"
3.223 +by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
3.224 +
3.225 +lemma assumes "Numeral1*y \<le> Numeral0" shows "0 \<le> (y::rat) * -2"
3.226 +by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
3.227 +
3.228 +lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::rat)"
3.229 +by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
3.230 +
3.231 +lemma assumes "-3*x \<le> 4*y" shows "-99*x \<le> 132 * (y::rat)"
3.232 +by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
3.233 +
3.234 +lemma assumes "111*x \<le> -44*y" shows "999*x \<le> -396 * (y::rat)"
3.235 +by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
3.236 +
3.237 +lemma assumes "-1*x \<le> Numeral1*y" shows "- ((2::rat) * x) \<le> 2*y"
3.238 +by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
3.239 +
3.240 +lemma assumes "9*y \<le> 11*x" shows "-99*x \<le> -81 * (y::rat)"
3.241 +by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
3.242 +
3.243 +lemma assumes "Numeral1*y \<le> 2*x" shows "-2 * x \<le> -1 * (y::rat)"
3.244 +by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
3.245 +
3.246 +lemma assumes "23*y \<le> Numeral1*x" shows "-x \<le> -23 * (y::rat)"
3.247 +by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
3.248 +
3.249 +
3.250 +subsection {* @{text ring_eq_cancel_numeral_factor} *}
3.251 +
3.252 +lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::int)"
3.253 +by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
3.254 +
3.255 +lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::int)"
3.256 +by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
3.257 +
3.258 +lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::int)"
3.259 +by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
3.260 +
3.261 +lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::int)"
3.262 +by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
3.263 +
3.264 +lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::rat)"
3.265 +by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
3.266 +
3.267 +lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::rat)"
3.268 +by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
3.269 +
3.270 +lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::rat)"
3.271 +by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
3.272 +
3.273 +lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::rat)"
3.274 +by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
3.275 +
3.276 +lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::rat)"
3.277 +by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
3.278 +
3.279 +lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::rat)"
3.280 +by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
3.281 +
3.282 +
3.283 +subsection {* @{text field_cancel_numeral_factor} *}
3.284 +
3.285 +lemma assumes "(3*x) / (4*y) = z" shows "(9*x) / (12 * (y::rat)) = z"
3.286 +by (tactic {* test [field_cancel_numeral_factor] *}) fact
3.287 +
3.288 +lemma assumes "(-3*x) / (4*y) = z" shows "(-99*x) / (132 * (y::rat)) = z"
3.289 +by (tactic {* test [field_cancel_numeral_factor] *}) fact
3.290 +
3.291 +lemma assumes "(111*x) / (-44*y) = z" shows "(999*x) / (-396 * (y::rat)) = z"
3.292 +by (tactic {* test [field_cancel_numeral_factor] *}) fact
3.293 +
3.294 +lemma assumes "(11*x) / (9*y) = z" shows "(-99*x) / (-81 * (y::rat)) = z"
3.295 +by (tactic {* test [field_cancel_numeral_factor] *}) fact
3.296 +
3.297 +lemma assumes "(2*x) / (Numeral1*y) = z" shows "(-2 * x) / (-1 * (y::rat)) = z"
3.298 +by (tactic {* test [field_cancel_numeral_factor] *}) fact
3.299 +
3.300 +
3.301 +subsection {* @{text ring_eq_cancel_factor} *}
3.302 +
3.303 +lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::int)"
3.304 +by (tactic {* test [ring_eq_cancel_factor] *}) fact
3.305 +
3.306 +lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::int)"
3.307 +by (tactic {* test [ring_eq_cancel_factor] *}) fact
3.308 +
3.309 +lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::int)"
3.310 +by (tactic {* test [ring_eq_cancel_factor] *}) fact
3.311 +
3.312 +lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::int)*(x*a)"
3.313 +by (tactic {* test [ring_eq_cancel_factor] *}) fact
3.314 +
3.315 +lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::rat)"
3.316 +by (tactic {* test [ring_eq_cancel_factor] *}) fact
3.317 +
3.318 +lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::rat)"
3.319 +by (tactic {* test [ring_eq_cancel_factor] *}) fact
3.320 +
3.321 +lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::rat)"
3.322 +by (tactic {* test [ring_eq_cancel_factor] *}) fact
3.323 +
3.324 +lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::rat)*(x*a)"
3.325 +by (tactic {* test [ring_eq_cancel_factor] *}) fact
3.326 +
3.327 +
3.328 +subsection {* @{text int_div_cancel_factor} *}
3.329 +
3.330 +lemma assumes "(if k = 0 then 0 else x div y) = uu"
3.331 + shows "(x*k) div (k*(y::int)) = (uu::int)"
3.332 +by (tactic {* test [int_div_cancel_factor] *}) fact
3.333 +
3.334 +lemma assumes "(if k = 0 then 0 else 1 div y) = uu"
3.335 + shows "(k) div (k*(y::int)) = (uu::int)"
3.336 +by (tactic {* test [int_div_cancel_factor] *}) fact
3.337 +
3.338 +lemma assumes "(if b = 0 then 0 else a * c) = uu"
3.339 + shows "(a*(b*c)) div ((b::int)) = (uu::int)"
3.340 +by (tactic {* test [int_div_cancel_factor] *}) fact
3.341 +
3.342 +lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
3.343 + shows "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)"
3.344 +by (tactic {* test [int_div_cancel_factor] *}) fact
3.345 +
3.346 +
3.347 +subsection {* @{text divide_cancel_factor} *}
3.348 +
3.349 +lemma assumes "(if k = 0 then 0 else x / y) = uu"
3.350 + shows "(x*k) / (k*(y::rat)) = (uu::rat)"
3.351 +by (tactic {* test [divide_cancel_factor] *}) fact
3.352 +
3.353 +lemma assumes "(if k = 0 then 0 else 1 / y) = uu"
3.354 + shows "(k) / (k*(y::rat)) = (uu::rat)"
3.355 +by (tactic {* test [divide_cancel_factor] *}) fact
3.356 +
3.357 +lemma assumes "(if b = 0 then 0 else a * c / 1) = uu"
3.358 + shows "(a*(b*c)) / ((b::rat)) = (uu::rat)"
3.359 +by (tactic {* test [divide_cancel_factor] *}) fact
3.360 +
3.361 +lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu"
3.362 + shows "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)"
3.363 +by (tactic {* test [divide_cancel_factor] *}) fact
3.364 +
3.365 +lemma shows "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z"
3.366 +oops -- "FIXME: need simproc to cover this case"
3.367 +
3.368 +
3.369 +subsection {* @{text linordered_ring_less_cancel_factor} *}
3.370 +
3.371 +lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < y*z"
3.372 +by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
3.373 +
3.374 +lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < z*y"
3.375 +by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
3.376 +
3.377 +lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < y*z"
3.378 +by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
3.379 +
3.380 +lemma "(0::rat) < z \<Longrightarrow> z*x < z*y"
3.381 +apply (tactic {* test [linordered_ring_less_cancel_factor] *})?
3.382 +oops -- "FIXME: test fails"
3.383 +
3.384 +
3.385 +subsection {* @{text linordered_ring_le_cancel_factor} *}
3.386 +
3.387 +lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> x*z \<le> y*z"
3.388 +by (tactic {* test [linordered_ring_le_cancel_factor] *}) fact
3.389 +
3.390 +lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> z*x \<le> z*y"
3.391 +apply (tactic {* test [linordered_ring_le_cancel_factor] *})?
3.392 +oops -- "FIXME: test fails"
3.393 +
3.394 +
3.395 +subsection {* @{text field_combine_numerals} *}
3.396 +
3.397 +lemma assumes "5 / 6 * x = uu" shows "(x::rat) / 2 + x / 3 = uu"
3.398 +by (tactic {* test [field_combine_numerals] *}) fact
3.399 +
3.400 +lemma assumes "6 / 9 * x + y = uu" shows "(x::rat) / 3 + y + x / 3 = uu"
3.401 +by (tactic {* test [field_combine_numerals] *}) fact
3.402 +
3.403 +lemma assumes "9 / 9 * x = uu" shows "2 * (x::rat) / 3 + x / 3 = uu"
3.404 +by (tactic {* test [field_combine_numerals] *}) fact
3.405 +
3.406 +lemma "2/3 * (x::rat) + x / 3 = uu"
3.407 +apply (tactic {* test [field_combine_numerals] *})?
3.408 +oops -- "FIXME: test fails"
3.409 +
3.410 +
3.411 +subsection {* @{text field_eq_cancel_numeral_factor} *}
3.412 +
3.413 +text {* TODO: tests for @{text field_eq_cancel_numeral_factor} simproc *}
3.414 +
3.415 +
3.416 +subsection {* @{text field_cancel_numeral_factor} *}
3.417 +
3.418 +text {* TODO: tests for @{text field_cancel_numeral_factor} simproc *}
3.419 +
3.420 +end