src/HOL/ex/Simproc_Tests.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45224 b1d5b3820d82
child 45270 d5b5c9259afd
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
huffman@45224
     1
(*  Title:      HOL/ex/Simproc_Tests.thy
huffman@45224
     2
    Author:     Brian Huffman
huffman@45224
     3
*)
huffman@45224
     4
huffman@45224
     5
header {* Testing of arithmetic simprocs *}
huffman@45224
     6
huffman@45224
     7
theory Simproc_Tests
huffman@45224
     8
imports Rat
huffman@45224
     9
begin
huffman@45224
    10
huffman@45224
    11
text {*
huffman@45224
    12
  This theory tests the various simprocs defined in
huffman@45224
    13
  @{file "~~/src/HOL/Numeral_Simprocs.thy"}. Many of the tests
huffman@45224
    14
  are derived from commented-out code originally found in
huffman@45224
    15
  @{file "~~/src/HOL/Tools/numeral_simprocs.ML"}.
huffman@45224
    16
*}
huffman@45224
    17
huffman@45224
    18
subsection {* ML bindings *}
huffman@45224
    19
huffman@45224
    20
ML {*
huffman@45224
    21
  val semiring_assoc_fold = Numeral_Simprocs.assoc_fold_simproc
huffman@45224
    22
  val int_combine_numerals = Numeral_Simprocs.combine_numerals
huffman@45224
    23
  val field_combine_numerals = Numeral_Simprocs.field_combine_numerals
huffman@45224
    24
  val [inteq_cancel_numerals, intless_cancel_numerals, intle_cancel_numerals]
huffman@45224
    25
    = Numeral_Simprocs.cancel_numerals
huffman@45224
    26
  val [ring_eq_cancel_factor, linordered_ring_le_cancel_factor,
huffman@45224
    27
      linordered_ring_less_cancel_factor, int_div_cancel_factor,
huffman@45224
    28
      int_mod_cancel_factor, dvd_cancel_factor, divide_cancel_factor]
huffman@45224
    29
    = Numeral_Simprocs.cancel_factors
huffman@45224
    30
  val [ring_eq_cancel_numeral_factor, ring_less_cancel_numeral_factor,
huffman@45224
    31
      ring_le_cancel_numeral_factor, int_div_cancel_numeral_factors,
huffman@45224
    32
      divide_cancel_numeral_factor]
huffman@45224
    33
    = Numeral_Simprocs.cancel_numeral_factors
huffman@45224
    34
  val field_combine_numerals = Numeral_Simprocs.field_combine_numerals
huffman@45224
    35
  val [field_eq_cancel_numeral_factor, field_cancel_numeral_factor]
huffman@45224
    36
    = Numeral_Simprocs.field_cancel_numeral_factors
huffman@45224
    37
huffman@45224
    38
  fun test ps = CHANGED (asm_simp_tac (HOL_basic_ss addsimprocs ps) 1)
huffman@45224
    39
*}
huffman@45224
    40
huffman@45224
    41
huffman@45224
    42
subsection {* @{text int_combine_numerals} *}
huffman@45224
    43
huffman@45224
    44
lemma assumes "10 + (2 * l + oo) = uu"
huffman@45224
    45
  shows "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"
huffman@45224
    46
by (tactic {* test [int_combine_numerals] *}) fact
huffman@45224
    47
huffman@45224
    48
lemma assumes "-3 + (i + (j + k)) = y"
huffman@45224
    49
  shows "(i + j + 12 + (k::int)) - 15 = y"
huffman@45224
    50
by (tactic {* test [int_combine_numerals] *}) fact
huffman@45224
    51
huffman@45224
    52
lemma assumes "7 + (i + (j + k)) = y"
huffman@45224
    53
  shows "(i + j + 12 + (k::int)) - 5 = y"
huffman@45224
    54
by (tactic {* test [int_combine_numerals] *}) fact
huffman@45224
    55
huffman@45224
    56
lemma assumes "-4 * (u * v) + (2 * x + y) = w"
huffman@45224
    57
  shows "(2*x - (u*v) + y) - v*3*u = (w::int)"
huffman@45224
    58
by (tactic {* test [int_combine_numerals] *}) fact
huffman@45224
    59
huffman@45224
    60
lemma assumes "Numeral0 * (u*v) + (2 * x * u * v + y) = w"
huffman@45224
    61
  shows "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"
huffman@45224
    62
by (tactic {* test [int_combine_numerals] *}) fact
huffman@45224
    63
huffman@45224
    64
lemma assumes "3 * (u * v) + (2 * x * u * v + y) = w"
huffman@45224
    65
  shows "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"
huffman@45224
    66
by (tactic {* test [int_combine_numerals] *}) fact
huffman@45224
    67
huffman@45224
    68
lemma assumes "-3 * (u * v) + (- (x * u * v) + - y) = w"
huffman@45224
    69
  shows "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"
huffman@45224
    70
by (tactic {* test [int_combine_numerals] *}) fact
huffman@45224
    71
huffman@45224
    72
lemma assumes "Numeral0 * b + (a + - c) = d"
huffman@45224
    73
  shows "a + -(b+c) + b = (d::int)"
huffman@45224
    74
apply (simp only: minus_add_distrib)
huffman@45224
    75
by (tactic {* test [int_combine_numerals] *}) fact
huffman@45224
    76
huffman@45224
    77
lemma assumes "-2 * b + (a + - c) = d"
huffman@45224
    78
  shows "a + -(b+c) - b = (d::int)"
huffman@45224
    79
apply (simp only: minus_add_distrib)
huffman@45224
    80
by (tactic {* test [int_combine_numerals] *}) fact
huffman@45224
    81
huffman@45224
    82
lemma assumes "-7 + (i + (j + (k + (- u + - y)))) = zz"
huffman@45224
    83
  shows "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"
huffman@45224
    84
by (tactic {* test [int_combine_numerals] *}) fact
huffman@45224
    85
huffman@45224
    86
lemma assumes "-27 + (i + (j + k)) = y"
huffman@45224
    87
  shows "(i + j + -12 + (k::int)) - 15 = y"
huffman@45224
    88
by (tactic {* test [int_combine_numerals] *}) fact
huffman@45224
    89
huffman@45224
    90
lemma assumes "27 + (i + (j + k)) = y"
huffman@45224
    91
  shows "(i + j + 12 + (k::int)) - -15 = y"
huffman@45224
    92
by (tactic {* test [int_combine_numerals] *}) fact
huffman@45224
    93
huffman@45224
    94
lemma assumes "3 + (i + (j + k)) = y"
huffman@45224
    95
  shows "(i + j + -12 + (k::int)) - -15 = y"
huffman@45224
    96
by (tactic {* test [int_combine_numerals] *}) fact
huffman@45224
    97
huffman@45224
    98
huffman@45224
    99
subsection {* @{text inteq_cancel_numerals} *}
huffman@45224
   100
huffman@45224
   101
lemma assumes "u = Numeral0" shows "2*u = (u::int)"
huffman@45224
   102
by (tactic {* test [inteq_cancel_numerals] *}) fact
huffman@45224
   103
(* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *)
huffman@45224
   104
huffman@45224
   105
lemma assumes "i + (j + k) = 3 + (u + y)"
huffman@45224
   106
  shows "(i + j + 12 + (k::int)) = u + 15 + y"
huffman@45224
   107
by (tactic {* test [inteq_cancel_numerals] *}) fact
huffman@45224
   108
huffman@45224
   109
lemma assumes "7 + (j + (i + k)) = y"
huffman@45224
   110
  shows "(i + j*2 + 12 + (k::int)) = j + 5 + y"
huffman@45224
   111
by (tactic {* test [inteq_cancel_numerals] *}) fact
huffman@45224
   112
huffman@45224
   113
lemma assumes "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))"
huffman@45224
   114
  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)"
huffman@45224
   115
by (tactic {* test [int_combine_numerals, inteq_cancel_numerals] *}) fact
huffman@45224
   116
huffman@45224
   117
huffman@45224
   118
subsection {* @{text intless_cancel_numerals} *}
huffman@45224
   119
huffman@45224
   120
lemma assumes "y < 2 * b" shows "y - b < (b::int)"
huffman@45224
   121
by (tactic {* test [intless_cancel_numerals] *}) fact
huffman@45224
   122
huffman@45224
   123
lemma assumes "c + y < 4 * b" shows "y - (3*b + c) < (b::int) - 2*c"
huffman@45224
   124
by (tactic {* test [intless_cancel_numerals] *}) fact
huffman@45224
   125
huffman@45224
   126
lemma assumes "i + (j + k) < 8 + (u + y)"
huffman@45224
   127
  shows "(i + j + -3 + (k::int)) < u + 5 + y"
huffman@45224
   128
by (tactic {* test [intless_cancel_numerals] *}) fact
huffman@45224
   129
huffman@45224
   130
lemma assumes "9 + (i + (j + k)) < u + y"
huffman@45224
   131
  shows "(i + j + 3 + (k::int)) < u + -6 + y"
huffman@45224
   132
by (tactic {* test [intless_cancel_numerals] *}) fact
huffman@45224
   133
huffman@45224
   134
huffman@45224
   135
subsection {* @{text ring_eq_cancel_numeral_factor} *}
huffman@45224
   136
huffman@45224
   137
lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::int)"
huffman@45224
   138
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
huffman@45224
   139
huffman@45224
   140
lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::int)"
huffman@45224
   141
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
huffman@45224
   142
huffman@45224
   143
huffman@45224
   144
subsection {* @{text int_div_cancel_numeral_factors} *}
huffman@45224
   145
huffman@45224
   146
lemma assumes "(3*x) div (4*y) = z" shows "(9*x) div (12*y) = (z::int)"
huffman@45224
   147
by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
huffman@45224
   148
huffman@45224
   149
lemma assumes "(-3*x) div (4*y) = z" shows "(-99*x) div (132*y) = (z::int)"
huffman@45224
   150
by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
huffman@45224
   151
huffman@45224
   152
lemma assumes "(111*x) div (-44*y) = z" shows "(999*x) div (-396*y) = (z::int)"
huffman@45224
   153
by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
huffman@45224
   154
huffman@45224
   155
lemma assumes "(11*x) div (9*y) = z" shows "(-99*x) div (-81*y) = (z::int)"
huffman@45224
   156
by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
huffman@45224
   157
huffman@45224
   158
lemma assumes "(2*x) div (Numeral1*y) = z"
huffman@45224
   159
  shows "(-2 * x) div (-1 * (y::int)) = z"
huffman@45224
   160
by (tactic {* test [int_div_cancel_numeral_factors] *}) fact
huffman@45224
   161
huffman@45224
   162
huffman@45224
   163
subsection {* @{text ring_less_cancel_numeral_factor} *}
huffman@45224
   164
huffman@45224
   165
lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::int)"
huffman@45224
   166
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
huffman@45224
   167
huffman@45224
   168
lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::int)"
huffman@45224
   169
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
huffman@45224
   170
huffman@45224
   171
lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::int)"
huffman@45224
   172
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
huffman@45224
   173
huffman@45224
   174
lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::int)"
huffman@45224
   175
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
huffman@45224
   176
huffman@45224
   177
lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::int)"
huffman@45224
   178
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
huffman@45224
   179
huffman@45224
   180
lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::int)"
huffman@45224
   181
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
huffman@45224
   182
huffman@45224
   183
lemma assumes "3*x < 4*y" shows "9*x < 12 * (y::rat)"
huffman@45224
   184
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
huffman@45224
   185
huffman@45224
   186
lemma assumes "-3*x < 4*y" shows "-99*x < 132 * (y::rat)"
huffman@45224
   187
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
huffman@45224
   188
huffman@45224
   189
lemma assumes "111*x < -44*y" shows "999*x < -396 * (y::rat)"
huffman@45224
   190
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
huffman@45224
   191
huffman@45224
   192
lemma assumes "9*y < 11*x" shows "-99*x < -81 * (y::rat)"
huffman@45224
   193
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
huffman@45224
   194
huffman@45224
   195
lemma assumes "Numeral1*y < 2*x" shows "-2 * x < -(y::rat)"
huffman@45224
   196
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
huffman@45224
   197
huffman@45224
   198
lemma assumes "23*y < Numeral1*x" shows "-x < -23 * (y::rat)"
huffman@45224
   199
by (tactic {* test [ring_less_cancel_numeral_factor] *}) fact
huffman@45224
   200
huffman@45224
   201
huffman@45224
   202
subsection {* @{text ring_le_cancel_numeral_factor} *}
huffman@45224
   203
huffman@45224
   204
lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::int)"
huffman@45224
   205
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
huffman@45224
   206
huffman@45224
   207
lemma assumes "-3*x \<le> 4*y" shows "-99*x \<le> 132 * (y::int)"
huffman@45224
   208
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
huffman@45224
   209
huffman@45224
   210
lemma assumes "111*x \<le> -44*y" shows "999*x \<le> -396 * (y::int)"
huffman@45224
   211
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
huffman@45224
   212
huffman@45224
   213
lemma assumes "9*y \<le> 11*x" shows "-99*x \<le> -81 * (y::int)"
huffman@45224
   214
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
huffman@45224
   215
huffman@45224
   216
lemma assumes "Numeral1*y \<le> 2*x" shows "-2 * x \<le> -1 * (y::int)"
huffman@45224
   217
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
huffman@45224
   218
huffman@45224
   219
lemma assumes "23*y \<le> Numeral1*x" shows "-x \<le> -23 * (y::int)"
huffman@45224
   220
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
huffman@45224
   221
huffman@45224
   222
lemma assumes "Numeral1*y \<le> Numeral0" shows "0 \<le> (y::rat) * -2"
huffman@45224
   223
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
huffman@45224
   224
huffman@45224
   225
lemma assumes "3*x \<le> 4*y" shows "9*x \<le> 12 * (y::rat)"
huffman@45224
   226
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
huffman@45224
   227
huffman@45224
   228
lemma assumes "-3*x \<le> 4*y" shows "-99*x \<le> 132 * (y::rat)"
huffman@45224
   229
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
huffman@45224
   230
huffman@45224
   231
lemma assumes "111*x \<le> -44*y" shows "999*x \<le> -396 * (y::rat)"
huffman@45224
   232
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
huffman@45224
   233
huffman@45224
   234
lemma assumes "-1*x \<le> Numeral1*y" shows "- ((2::rat) * x) \<le> 2*y"
huffman@45224
   235
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
huffman@45224
   236
huffman@45224
   237
lemma assumes "9*y \<le> 11*x" shows "-99*x \<le> -81 * (y::rat)"
huffman@45224
   238
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
huffman@45224
   239
huffman@45224
   240
lemma assumes "Numeral1*y \<le> 2*x" shows "-2 * x \<le> -1 * (y::rat)"
huffman@45224
   241
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
huffman@45224
   242
huffman@45224
   243
lemma assumes "23*y \<le> Numeral1*x" shows "-x \<le> -23 * (y::rat)"
huffman@45224
   244
by (tactic {* test [ring_le_cancel_numeral_factor] *}) fact
huffman@45224
   245
huffman@45224
   246
huffman@45224
   247
subsection {* @{text ring_eq_cancel_numeral_factor} *}
huffman@45224
   248
huffman@45224
   249
lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::int)"
huffman@45224
   250
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
huffman@45224
   251
huffman@45224
   252
lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::int)"
huffman@45224
   253
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
huffman@45224
   254
huffman@45224
   255
lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::int)"
huffman@45224
   256
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
huffman@45224
   257
huffman@45224
   258
lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::int)"
huffman@45224
   259
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
huffman@45224
   260
huffman@45224
   261
lemma assumes "3*x = 4*y" shows "9*x = 12 * (y::rat)"
huffman@45224
   262
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
huffman@45224
   263
huffman@45224
   264
lemma assumes "-3*x = 4*y" shows "-99*x = 132 * (y::rat)"
huffman@45224
   265
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
huffman@45224
   266
huffman@45224
   267
lemma assumes "111*x = -44*y" shows "999*x = -396 * (y::rat)"
huffman@45224
   268
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
huffman@45224
   269
huffman@45224
   270
lemma assumes "11*x = 9*y" shows "-99*x = -81 * (y::rat)"
huffman@45224
   271
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
huffman@45224
   272
huffman@45224
   273
lemma assumes "2*x = Numeral1*y" shows "-2 * x = -1 * (y::rat)"
huffman@45224
   274
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
huffman@45224
   275
huffman@45224
   276
lemma assumes "2*x = Numeral1*y" shows "-2 * x = -(y::rat)"
huffman@45224
   277
by (tactic {* test [ring_eq_cancel_numeral_factor] *}) fact
huffman@45224
   278
huffman@45224
   279
huffman@45224
   280
subsection {* @{text field_cancel_numeral_factor} *}
huffman@45224
   281
huffman@45224
   282
lemma assumes "(3*x) / (4*y) = z" shows "(9*x) / (12 * (y::rat)) = z"
huffman@45224
   283
by (tactic {* test [field_cancel_numeral_factor] *}) fact
huffman@45224
   284
huffman@45224
   285
lemma assumes "(-3*x) / (4*y) = z" shows "(-99*x) / (132 * (y::rat)) = z"
huffman@45224
   286
by (tactic {* test [field_cancel_numeral_factor] *}) fact
huffman@45224
   287
huffman@45224
   288
lemma assumes "(111*x) / (-44*y) = z" shows "(999*x) / (-396 * (y::rat)) = z"
huffman@45224
   289
by (tactic {* test [field_cancel_numeral_factor] *}) fact
huffman@45224
   290
huffman@45224
   291
lemma assumes "(11*x) / (9*y) = z" shows "(-99*x) / (-81 * (y::rat)) = z"
huffman@45224
   292
by (tactic {* test [field_cancel_numeral_factor] *}) fact
huffman@45224
   293
huffman@45224
   294
lemma assumes "(2*x) / (Numeral1*y) = z" shows "(-2 * x) / (-1 * (y::rat)) = z"
huffman@45224
   295
by (tactic {* test [field_cancel_numeral_factor] *}) fact
huffman@45224
   296
huffman@45224
   297
huffman@45224
   298
subsection {* @{text ring_eq_cancel_factor} *}
huffman@45224
   299
huffman@45224
   300
lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::int)"
huffman@45224
   301
by (tactic {* test [ring_eq_cancel_factor] *}) fact
huffman@45224
   302
huffman@45224
   303
lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::int)"
huffman@45224
   304
by (tactic {* test [ring_eq_cancel_factor] *}) fact
huffman@45224
   305
huffman@45224
   306
lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::int)"
huffman@45224
   307
by (tactic {* test [ring_eq_cancel_factor] *}) fact
huffman@45224
   308
huffman@45224
   309
lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::int)*(x*a)"
huffman@45224
   310
by (tactic {* test [ring_eq_cancel_factor] *}) fact
huffman@45224
   311
huffman@45224
   312
lemma assumes "k = 0 \<or> x = y" shows "x*k = k*(y::rat)"
huffman@45224
   313
by (tactic {* test [ring_eq_cancel_factor] *}) fact
huffman@45224
   314
huffman@45224
   315
lemma assumes "k = 0 \<or> 1 = y" shows "k = k*(y::rat)"
huffman@45224
   316
by (tactic {* test [ring_eq_cancel_factor] *}) fact
huffman@45224
   317
huffman@45224
   318
lemma assumes "b = 0 \<or> a*c = 1" shows "a*(b*c) = (b::rat)"
huffman@45224
   319
by (tactic {* test [ring_eq_cancel_factor] *}) fact
huffman@45224
   320
huffman@45224
   321
lemma assumes "a = 0 \<or> b = 0 \<or> c = d*x" shows "a*(b*c) = d*(b::rat)*(x*a)"
huffman@45224
   322
by (tactic {* test [ring_eq_cancel_factor] *}) fact
huffman@45224
   323
huffman@45224
   324
huffman@45224
   325
subsection {* @{text int_div_cancel_factor} *}
huffman@45224
   326
huffman@45224
   327
lemma assumes "(if k = 0 then 0 else x div y) = uu"
huffman@45224
   328
  shows "(x*k) div (k*(y::int)) = (uu::int)"
huffman@45224
   329
by (tactic {* test [int_div_cancel_factor] *}) fact
huffman@45224
   330
huffman@45224
   331
lemma assumes "(if k = 0 then 0 else 1 div y) = uu"
huffman@45224
   332
  shows "(k) div (k*(y::int)) = (uu::int)"
huffman@45224
   333
by (tactic {* test [int_div_cancel_factor] *}) fact
huffman@45224
   334
huffman@45224
   335
lemma assumes "(if b = 0 then 0 else a * c) = uu"
huffman@45224
   336
  shows "(a*(b*c)) div ((b::int)) = (uu::int)"
huffman@45224
   337
by (tactic {* test [int_div_cancel_factor] *}) fact
huffman@45224
   338
huffman@45224
   339
lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
huffman@45224
   340
  shows "(a*(b*c)) div (d*(b::int)*(x*a)) = (uu::int)"
huffman@45224
   341
by (tactic {* test [int_div_cancel_factor] *}) fact
huffman@45224
   342
huffman@45224
   343
huffman@45224
   344
subsection {* @{text divide_cancel_factor} *}
huffman@45224
   345
huffman@45224
   346
lemma assumes "(if k = 0 then 0 else x / y) = uu"
huffman@45224
   347
  shows "(x*k) / (k*(y::rat)) = (uu::rat)"
huffman@45224
   348
by (tactic {* test [divide_cancel_factor] *}) fact
huffman@45224
   349
huffman@45224
   350
lemma assumes "(if k = 0 then 0 else 1 / y) = uu"
huffman@45224
   351
  shows "(k) / (k*(y::rat)) = (uu::rat)"
huffman@45224
   352
by (tactic {* test [divide_cancel_factor] *}) fact
huffman@45224
   353
huffman@45224
   354
lemma assumes "(if b = 0 then 0 else a * c / 1) = uu"
huffman@45224
   355
  shows "(a*(b*c)) / ((b::rat)) = (uu::rat)"
huffman@45224
   356
by (tactic {* test [divide_cancel_factor] *}) fact
huffman@45224
   357
huffman@45224
   358
lemma assumes "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu"
huffman@45224
   359
  shows "(a*(b*c)) / (d*(b::rat)*(x*a)) = (uu::rat)"
huffman@45224
   360
by (tactic {* test [divide_cancel_factor] *}) fact
huffman@45224
   361
huffman@45224
   362
lemma shows "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z"
huffman@45224
   363
oops -- "FIXME: need simproc to cover this case"
huffman@45224
   364
huffman@45224
   365
huffman@45224
   366
subsection {* @{text linordered_ring_less_cancel_factor} *}
huffman@45224
   367
huffman@45224
   368
lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < y*z"
huffman@45224
   369
by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
huffman@45224
   370
huffman@45224
   371
lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> x*z < z*y"
huffman@45224
   372
by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
huffman@45224
   373
huffman@45224
   374
lemma assumes "0 < z \<Longrightarrow> x < y" shows "(0::rat) < z \<Longrightarrow> z*x < y*z"
huffman@45224
   375
by (tactic {* test [linordered_ring_less_cancel_factor] *}) fact
huffman@45224
   376
huffman@45224
   377
lemma "(0::rat) < z \<Longrightarrow> z*x < z*y"
huffman@45224
   378
apply (tactic {* test [linordered_ring_less_cancel_factor] *})?
huffman@45224
   379
oops -- "FIXME: test fails"
huffman@45224
   380
huffman@45224
   381
huffman@45224
   382
subsection {* @{text linordered_ring_le_cancel_factor} *}
huffman@45224
   383
huffman@45224
   384
lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> x*z \<le> y*z"
huffman@45224
   385
by (tactic {* test [linordered_ring_le_cancel_factor] *}) fact
huffman@45224
   386
huffman@45224
   387
lemma assumes "0 < z \<Longrightarrow> x \<le> y" shows "(0::rat) < z \<Longrightarrow> z*x \<le> z*y"
huffman@45224
   388
apply (tactic {* test [linordered_ring_le_cancel_factor] *})?
huffman@45224
   389
oops -- "FIXME: test fails"
huffman@45224
   390
huffman@45224
   391
huffman@45224
   392
subsection {* @{text field_combine_numerals} *}
huffman@45224
   393
huffman@45224
   394
lemma assumes "5 / 6 * x = uu" shows "(x::rat) / 2 + x / 3 = uu"
huffman@45224
   395
by (tactic {* test [field_combine_numerals] *}) fact
huffman@45224
   396
huffman@45224
   397
lemma assumes "6 / 9 * x + y = uu" shows "(x::rat) / 3 + y + x / 3 = uu"
huffman@45224
   398
by (tactic {* test [field_combine_numerals] *}) fact
huffman@45224
   399
huffman@45224
   400
lemma assumes "9 / 9 * x = uu" shows "2 * (x::rat) / 3 + x / 3 = uu"
huffman@45224
   401
by (tactic {* test [field_combine_numerals] *}) fact
huffman@45224
   402
huffman@45224
   403
lemma "2/3 * (x::rat) + x / 3 = uu"
huffman@45224
   404
apply (tactic {* test [field_combine_numerals] *})?
huffman@45224
   405
oops -- "FIXME: test fails"
huffman@45224
   406
huffman@45224
   407
huffman@45224
   408
subsection {* @{text field_eq_cancel_numeral_factor} *}
huffman@45224
   409
huffman@45224
   410
text {* TODO: tests for @{text field_eq_cancel_numeral_factor} simproc *}
huffman@45224
   411
huffman@45224
   412
huffman@45224
   413
subsection {* @{text field_cancel_numeral_factor} *}
huffman@45224
   414
huffman@45224
   415
text {* TODO: tests for @{text field_cancel_numeral_factor} simproc *}
huffman@45224
   416
huffman@45224
   417
end