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