src/HOL/ex/Simproc_Tests.thy
author huffman
Fri Jul 20 10:53:25 2012 +0200 (2012-07-20)
changeset 48372 868dc809c8a2
parent 47108 2a1953f0d20d
child 48556 62a3fbf9d35b
permissions -rw-r--r--
make nat_cancel_sums simprocs robust in the presence of schematic variables; add regression tests
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@48372
     8
imports Main
huffman@45224
     9
begin
huffman@45224
    10
huffman@45224
    11
text {*
huffman@48372
    12
  This theory tests the various simprocs defined in @{file
huffman@48372
    13
  "~~/src/HOL/Nat.thy"} and @{file "~~/src/HOL/Numeral_Simprocs.thy"}.
huffman@48372
    14
  Many of the tests are derived from commented-out code originally
huffman@48372
    15
  found in @{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@48372
    24
subsection {* Cancellation simprocs from @{text Nat.thy} *}
huffman@48372
    25
huffman@48372
    26
notepad begin
huffman@48372
    27
  fix a b c d :: nat
huffman@48372
    28
  {
huffman@48372
    29
    assume "b = Suc c" have "a + b = Suc (c + a)"
huffman@48372
    30
      by (tactic {* test [nth Nat_Arith.nat_cancel_sums 0] *}) fact
huffman@48372
    31
  next
huffman@48372
    32
    assume "b < Suc c" have "a + b < Suc (c + a)"
huffman@48372
    33
      by (tactic {* test [nth Nat_Arith.nat_cancel_sums 1] *}) fact
huffman@48372
    34
  next
huffman@48372
    35
    assume "b \<le> Suc c" have "a + b \<le> Suc (c + a)"
huffman@48372
    36
      by (tactic {* test [nth Nat_Arith.nat_cancel_sums 2] *}) fact
huffman@48372
    37
  next
huffman@48372
    38
    assume "b - Suc c = d" have "a + b - Suc (c + a) = d"
huffman@48372
    39
      by (tactic {* test [nth Nat_Arith.nat_cancel_sums 3] *}) fact
huffman@48372
    40
  }
huffman@48372
    41
end
huffman@48372
    42
huffman@48372
    43
schematic_lemma "\<And>(y::?'b::size). size (?x::?'a::size) \<le> size y + size ?x"
huffman@48372
    44
  by (tactic {* test [nth Nat_Arith.nat_cancel_sums 2] *}) (rule le0)
huffman@48372
    45
(* TODO: test more simprocs with schematic variables *)
huffman@48372
    46
huffman@45464
    47
subsection {* Abelian group cancellation simprocs *}
huffman@45464
    48
huffman@45464
    49
notepad begin
huffman@45464
    50
  fix a b c u :: "'a::ab_group_add"
huffman@45464
    51
  {
huffman@45464
    52
    assume "(a + 0) - (b + 0) = u" have "(a + c) - (b + c) = u"
huffman@45464
    53
      by (tactic {* test [@{simproc abel_cancel_sum}] *}) fact
huffman@45464
    54
  next
huffman@45464
    55
    assume "a + 0 = b + 0" have "a + c = b + c"
huffman@45464
    56
      by (tactic {* test [@{simproc abel_cancel_relation}] *}) fact
huffman@45464
    57
  }
huffman@45464
    58
end
huffman@45464
    59
(* TODO: more tests for Groups.abel_cancel_{sum,relation} *)
huffman@45224
    60
huffman@45224
    61
subsection {* @{text int_combine_numerals} *}
huffman@45224
    62
huffman@45464
    63
(* FIXME: int_combine_numerals often unnecessarily regroups addition
huffman@45464
    64
and rewrites subtraction to negation. Ideally it should behave more
huffman@45464
    65
like Groups.abel_cancel_sum, preserving the shape of terms as much as
huffman@45464
    66
possible. *)
huffman@45464
    67
huffman@45435
    68
notepad begin
huffman@47108
    69
  fix a b c d oo uu i j k l u v w x y z :: "'a::comm_ring_1"
huffman@45435
    70
  {
huffman@45464
    71
    assume "a + - b = u" have "(a + c) - (b + c) = u"
huffman@45464
    72
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45464
    73
  next
huffman@45435
    74
    assume "10 + (2 * l + oo) = uu"
huffman@45435
    75
    have "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = uu"
huffman@45435
    76
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
    77
  next
huffman@45435
    78
    assume "-3 + (i + (j + k)) = y"
huffman@45435
    79
    have "(i + j + 12 + k) - 15 = y"
huffman@45435
    80
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
    81
  next
huffman@45435
    82
    assume "7 + (i + (j + k)) = y"
huffman@45435
    83
    have "(i + j + 12 + k) - 5 = y"
huffman@45435
    84
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
    85
  next
huffman@45435
    86
    assume "-4 * (u * v) + (2 * x + y) = w"
huffman@45435
    87
    have "(2*x - (u*v) + y) - v*3*u = w"
huffman@45435
    88
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
    89
  next
huffman@45437
    90
    assume "2 * x * u * v + y = w"
huffman@45435
    91
    have "(2*x*u*v + (u*v)*4 + y) - v*u*4 = w"
huffman@45435
    92
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
    93
  next
huffman@45435
    94
    assume "3 * (u * v) + (2 * x * u * v + y) = w"
huffman@45435
    95
    have "(2*x*u*v + (u*v)*4 + y) - v*u = w"
huffman@45435
    96
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
    97
  next
huffman@45435
    98
    assume "-3 * (u * v) + (- (x * u * v) + - y) = w"
huffman@45435
    99
    have "u*v - (x*u*v + (u*v)*4 + y) = w"
huffman@45435
   100
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
   101
  next
huffman@45437
   102
    assume "a + - c = d"
huffman@45435
   103
    have "a + -(b+c) + b = d"
huffman@45435
   104
      apply (simp only: minus_add_distrib)
huffman@45435
   105
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
   106
  next
huffman@45435
   107
    assume "-2 * b + (a + - c) = d"
huffman@45435
   108
    have "a + -(b+c) - b = d"
huffman@45435
   109
      apply (simp only: minus_add_distrib)
huffman@45435
   110
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
   111
  next
huffman@45435
   112
    assume "-7 + (i + (j + (k + (- u + - y)))) = z"
huffman@45435
   113
    have "(i + j + -2 + k) - (u + 5 + y) = z"
huffman@45435
   114
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
   115
  next
huffman@45435
   116
    assume "-27 + (i + (j + k)) = y"
huffman@45435
   117
    have "(i + j + -12 + k) - 15 = y"
huffman@45435
   118
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
   119
  next
huffman@45435
   120
    assume "27 + (i + (j + k)) = y"
huffman@45435
   121
    have "(i + j + 12 + k) - -15 = y"
huffman@45435
   122
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
   123
  next
huffman@45435
   124
    assume "3 + (i + (j + k)) = y"
huffman@45435
   125
    have "(i + j + -12 + k) - -15 = y"
huffman@45435
   126
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
   127
  }
huffman@45435
   128
end
huffman@45224
   129
huffman@45224
   130
subsection {* @{text inteq_cancel_numerals} *}
huffman@45224
   131
huffman@45435
   132
notepad begin
huffman@47108
   133
  fix i j k u vv w y z w' y' z' :: "'a::comm_ring_1"
huffman@45435
   134
  {
huffman@45437
   135
    assume "u = 0" have "2*u = u"
huffman@45435
   136
      by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
huffman@45224
   137
(* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *)
huffman@45435
   138
  next
huffman@45435
   139
    assume "i + (j + k) = 3 + (u + y)"
huffman@45435
   140
    have "(i + j + 12 + k) = u + 15 + y"
huffman@45435
   141
      by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
huffman@45435
   142
  next
huffman@45435
   143
    assume "7 + (j + (i + k)) = y"
huffman@45435
   144
    have "(i + j*2 + 12 + k) = j + 5 + y"
huffman@45435
   145
      by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
huffman@45435
   146
  next
huffman@45435
   147
    assume "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))"
huffman@45435
   148
    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"
huffman@45435
   149
      by (tactic {* test [@{simproc int_combine_numerals}, @{simproc inteq_cancel_numerals}] *}) fact
huffman@45435
   150
  }
huffman@45435
   151
end
huffman@45224
   152
huffman@45224
   153
subsection {* @{text intless_cancel_numerals} *}
huffman@45224
   154
huffman@45435
   155
notepad begin
huffman@47108
   156
  fix b c i j k u y :: "'a::linordered_idom"
huffman@45435
   157
  {
huffman@45435
   158
    assume "y < 2 * b" have "y - b < b"
huffman@45435
   159
      by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
huffman@45435
   160
  next
huffman@45435
   161
    assume "c + y < 4 * b" have "y - (3*b + c) < b - 2*c"
huffman@45435
   162
      by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
huffman@45435
   163
  next
huffman@45435
   164
    assume "i + (j + k) < 8 + (u + y)"
huffman@45435
   165
    have "(i + j + -3 + k) < u + 5 + y"
huffman@45435
   166
      by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
huffman@45435
   167
  next
huffman@45435
   168
    assume "9 + (i + (j + k)) < u + y"
huffman@45435
   169
    have "(i + j + 3 + k) < u + -6 + y"
huffman@45435
   170
      by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
huffman@45435
   171
  }
huffman@45435
   172
end
huffman@45224
   173
huffman@45224
   174
subsection {* @{text ring_eq_cancel_numeral_factor} *}
huffman@45224
   175
huffman@45435
   176
notepad begin
huffman@47108
   177
  fix x y :: "'a::{idom,ring_char_0}"
huffman@45435
   178
  {
huffman@45435
   179
    assume "3*x = 4*y" have "9*x = 12 * y"
huffman@45435
   180
      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
huffman@45435
   181
  next
huffman@45435
   182
    assume "-3*x = 4*y" have "-99*x = 132 * y"
huffman@45435
   183
      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
huffman@45435
   184
  next
huffman@45435
   185
    assume "111*x = -44*y" have "999*x = -396 * y"
huffman@45435
   186
      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
huffman@45435
   187
  next
huffman@45435
   188
    assume "11*x = 9*y" have "-99*x = -81 * y"
huffman@45435
   189
      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
huffman@45435
   190
  next
huffman@45437
   191
    assume "2*x = y" have "-2 * x = -1 * y"
huffman@45435
   192
      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
huffman@45435
   193
  next
huffman@45437
   194
    assume "2*x = y" have "-2 * x = -y"
huffman@45435
   195
      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
huffman@45435
   196
  }
huffman@45435
   197
end
huffman@45224
   198
huffman@45224
   199
subsection {* @{text int_div_cancel_numeral_factors} *}
huffman@45224
   200
huffman@45435
   201
notepad begin
huffman@47108
   202
  fix x y z :: "'a::{semiring_div,comm_ring_1,ring_char_0}"
huffman@45435
   203
  {
huffman@45435
   204
    assume "(3*x) div (4*y) = z" have "(9*x) div (12*y) = z"
huffman@45435
   205
      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
huffman@45435
   206
  next
huffman@45435
   207
    assume "(-3*x) div (4*y) = z" have "(-99*x) div (132*y) = z"
huffman@45435
   208
      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
huffman@45435
   209
  next
huffman@45435
   210
    assume "(111*x) div (-44*y) = z" have "(999*x) div (-396*y) = z"
huffman@45435
   211
      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
huffman@45435
   212
  next
huffman@45435
   213
    assume "(11*x) div (9*y) = z" have "(-99*x) div (-81*y) = z"
huffman@45435
   214
      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
huffman@45435
   215
  next
huffman@45437
   216
    assume "(2*x) div y = z"
huffman@45435
   217
    have "(-2 * x) div (-1 * y) = z"
huffman@45435
   218
      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
huffman@45435
   219
  }
huffman@45435
   220
end
huffman@45224
   221
huffman@45224
   222
subsection {* @{text ring_less_cancel_numeral_factor} *}
huffman@45224
   223
huffman@45435
   224
notepad begin
huffman@47108
   225
  fix x y :: "'a::linordered_idom"
huffman@45435
   226
  {
huffman@45435
   227
    assume "3*x < 4*y" have "9*x < 12 * y"
huffman@45435
   228
      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
huffman@45435
   229
  next
huffman@45435
   230
    assume "-3*x < 4*y" have "-99*x < 132 * y"
huffman@45435
   231
      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
huffman@45435
   232
  next
huffman@45435
   233
    assume "111*x < -44*y" have "999*x < -396 * y"
huffman@45435
   234
      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
huffman@45435
   235
  next
huffman@45435
   236
    assume "9*y < 11*x" have "-99*x < -81 * y"
huffman@45435
   237
      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
huffman@45435
   238
  next
huffman@45437
   239
    assume "y < 2*x" have "-2 * x < -y"
huffman@45435
   240
      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
huffman@45435
   241
  next
huffman@45437
   242
    assume "23*y < x" have "-x < -23 * y"
huffman@45435
   243
      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
huffman@45435
   244
  }
huffman@45435
   245
end
huffman@45224
   246
huffman@45224
   247
subsection {* @{text ring_le_cancel_numeral_factor} *}
huffman@45224
   248
huffman@45435
   249
notepad begin
huffman@47108
   250
  fix x y :: "'a::linordered_idom"
huffman@45435
   251
  {
huffman@45435
   252
    assume "3*x \<le> 4*y" have "9*x \<le> 12 * y"
huffman@45435
   253
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435
   254
  next
huffman@45435
   255
    assume "-3*x \<le> 4*y" have "-99*x \<le> 132 * y"
huffman@45435
   256
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435
   257
  next
huffman@45435
   258
    assume "111*x \<le> -44*y" have "999*x \<le> -396 * y"
huffman@45435
   259
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435
   260
  next
huffman@45435
   261
    assume "9*y \<le> 11*x" have "-99*x \<le> -81 * y"
huffman@45435
   262
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435
   263
  next
huffman@45437
   264
    assume "y \<le> 2*x" have "-2 * x \<le> -1 * y"
huffman@45435
   265
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435
   266
  next
huffman@45437
   267
    assume "23*y \<le> x" have "-x \<le> -23 * y"
huffman@45435
   268
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435
   269
  next
huffman@45437
   270
    assume "y \<le> 0" have "0 \<le> y * -2"
huffman@45435
   271
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435
   272
  next
huffman@45437
   273
    assume "- x \<le> y" have "- (2 * x) \<le> 2*y"
huffman@45435
   274
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435
   275
  }
huffman@45435
   276
end
huffman@45224
   277
huffman@45285
   278
subsection {* @{text divide_cancel_numeral_factor} *}
huffman@45224
   279
huffman@45435
   280
notepad begin
huffman@47108
   281
  fix x y z :: "'a::{field_inverse_zero,ring_char_0}"
huffman@45435
   282
  {
huffman@45435
   283
    assume "(3*x) / (4*y) = z" have "(9*x) / (12 * y) = z"
huffman@45435
   284
      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
huffman@45435
   285
  next
huffman@45435
   286
    assume "(-3*x) / (4*y) = z" have "(-99*x) / (132 * y) = z"
huffman@45435
   287
      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
huffman@45435
   288
  next
huffman@45435
   289
    assume "(111*x) / (-44*y) = z" have "(999*x) / (-396 * y) = z"
huffman@45435
   290
      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
huffman@45435
   291
  next
huffman@45435
   292
    assume "(11*x) / (9*y) = z" have "(-99*x) / (-81 * y) = z"
huffman@45435
   293
      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
huffman@45435
   294
  next
huffman@45437
   295
    assume "(2*x) / y = z" have "(-2 * x) / (-1 * y) = z"
huffman@45435
   296
      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
huffman@45435
   297
  }
huffman@45435
   298
end
huffman@45224
   299
huffman@45224
   300
subsection {* @{text ring_eq_cancel_factor} *}
huffman@45224
   301
huffman@45435
   302
notepad begin
huffman@45435
   303
  fix a b c d k x y :: "'a::idom"
huffman@45435
   304
  {
huffman@45435
   305
    assume "k = 0 \<or> x = y" have "x*k = k*y"
huffman@45435
   306
      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
huffman@45435
   307
  next
huffman@45435
   308
    assume "k = 0 \<or> 1 = y" have "k = k*y"
huffman@45435
   309
      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
huffman@45435
   310
  next
huffman@45435
   311
    assume "b = 0 \<or> a*c = 1" have "a*(b*c) = b"
huffman@45435
   312
      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
huffman@45435
   313
  next
huffman@45435
   314
    assume "a = 0 \<or> b = 0 \<or> c = d*x" have "a*(b*c) = d*b*(x*a)"
huffman@45435
   315
      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
huffman@45435
   316
  next
huffman@45435
   317
    assume "k = 0 \<or> x = y" have "x*k = k*y"
huffman@45435
   318
      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
huffman@45435
   319
  next
huffman@45435
   320
    assume "k = 0 \<or> 1 = y" have "k = k*y"
huffman@45435
   321
      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
huffman@45435
   322
  }
huffman@45435
   323
end
huffman@45224
   324
huffman@45224
   325
subsection {* @{text int_div_cancel_factor} *}
huffman@45224
   326
huffman@45435
   327
notepad begin
huffman@45435
   328
  fix a b c d k uu x y :: "'a::semiring_div"
huffman@45435
   329
  {
huffman@45435
   330
    assume "(if k = 0 then 0 else x div y) = uu"
huffman@45435
   331
    have "(x*k) div (k*y) = uu"
huffman@45435
   332
      by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
huffman@45435
   333
  next
huffman@45435
   334
    assume "(if k = 0 then 0 else 1 div y) = uu"
huffman@45435
   335
    have "(k) div (k*y) = uu"
huffman@45435
   336
      by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
huffman@45435
   337
  next
huffman@45435
   338
    assume "(if b = 0 then 0 else a * c) = uu"
huffman@45435
   339
    have "(a*(b*c)) div b = uu"
huffman@45435
   340
      by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
huffman@45435
   341
  next
huffman@45435
   342
    assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
huffman@45435
   343
    have "(a*(b*c)) div (d*b*(x*a)) = uu"
huffman@45435
   344
      by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
huffman@45435
   345
  }
huffman@45435
   346
end
huffman@45224
   347
huffman@47108
   348
lemma shows "a*(b*c)/(y*z) = d*(b::'a::linordered_field_inverse_zero)*(x*a)/z"
huffman@47108
   349
oops -- "FIXME: need simproc to cover this case"
huffman@47108
   350
huffman@45224
   351
subsection {* @{text divide_cancel_factor} *}
huffman@45224
   352
huffman@45435
   353
notepad begin
huffman@45435
   354
  fix a b c d k uu x y :: "'a::field_inverse_zero"
huffman@45435
   355
  {
huffman@45435
   356
    assume "(if k = 0 then 0 else x / y) = uu"
huffman@45435
   357
    have "(x*k) / (k*y) = uu"
huffman@45435
   358
      by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
huffman@45435
   359
  next
huffman@45435
   360
    assume "(if k = 0 then 0 else 1 / y) = uu"
huffman@45435
   361
    have "(k) / (k*y) = uu"
huffman@45435
   362
      by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
huffman@45435
   363
  next
huffman@45435
   364
    assume "(if b = 0 then 0 else a * c / 1) = uu"
huffman@45435
   365
    have "(a*(b*c)) / b = uu"
huffman@45435
   366
      by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
huffman@45435
   367
  next
huffman@45435
   368
    assume "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu"
huffman@45435
   369
    have "(a*(b*c)) / (d*b*(x*a)) = uu"
huffman@45435
   370
      by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
huffman@45435
   371
  }
huffman@45435
   372
end
huffman@45224
   373
huffman@45462
   374
lemma
huffman@45462
   375
  fixes a b c d x y z :: "'a::linordered_field_inverse_zero"
huffman@45462
   376
  shows "a*(b*c)/(y*z) = d*(b)*(x*a)/z"
huffman@45224
   377
oops -- "FIXME: need simproc to cover this case"
huffman@45224
   378
huffman@45224
   379
subsection {* @{text linordered_ring_less_cancel_factor} *}
huffman@45224
   380
huffman@45435
   381
notepad begin
huffman@45435
   382
  fix x y z :: "'a::linordered_idom"
huffman@45435
   383
  {
huffman@45435
   384
    assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> x*z < y*z"
huffman@45435
   385
      by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
huffman@45435
   386
  next
huffman@45435
   387
    assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> x*z < z*y"
huffman@45435
   388
      by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
huffman@45435
   389
  next
huffman@45435
   390
    assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> z*x < y*z"
huffman@45435
   391
      by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
huffman@45435
   392
  next
huffman@45435
   393
    assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> z*x < z*y"
huffman@45435
   394
      by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
huffman@46240
   395
  next
huffman@46240
   396
    txt "This simproc now uses the simplifier to prove that terms to
huffman@46240
   397
      be canceled are positive/negative."
huffman@46240
   398
    assume z_pos: "0 < z"
huffman@46240
   399
    assume "x < y" have "z*x < z*y"
huffman@46240
   400
      by (tactic {* CHANGED (asm_simp_tac (HOL_basic_ss
huffman@46240
   401
        addsimprocs [@{simproc linordered_ring_less_cancel_factor}]
huffman@46240
   402
        addsimps [@{thm z_pos}]) 1) *}) fact
huffman@45435
   403
  }
huffman@45435
   404
end
huffman@45224
   405
huffman@45224
   406
subsection {* @{text linordered_ring_le_cancel_factor} *}
huffman@45224
   407
huffman@45435
   408
notepad begin
huffman@45435
   409
  fix x y z :: "'a::linordered_idom"
huffman@45435
   410
  {
huffman@45435
   411
    assume "0 < z \<Longrightarrow> x \<le> y" have "0 < z \<Longrightarrow> x*z \<le> y*z"
huffman@45435
   412
      by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
huffman@45435
   413
  next
huffman@45435
   414
    assume "0 < z \<Longrightarrow> x \<le> y" have "0 < z \<Longrightarrow> z*x \<le> z*y"
huffman@45435
   415
      by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
huffman@45435
   416
  }
huffman@45435
   417
end
huffman@45224
   418
huffman@45224
   419
subsection {* @{text field_combine_numerals} *}
huffman@45224
   420
huffman@45435
   421
notepad begin
huffman@47108
   422
  fix x y z uu :: "'a::{field_inverse_zero,ring_char_0}"
huffman@45435
   423
  {
huffman@45435
   424
    assume "5 / 6 * x = uu" have "x / 2 + x / 3 = uu"
huffman@45435
   425
      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
huffman@45435
   426
  next
huffman@45435
   427
    assume "6 / 9 * x + y = uu" have "x / 3 + y + x / 3 = uu"
huffman@45435
   428
      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
huffman@45435
   429
  next
huffman@45435
   430
    assume "9 / 9 * x = uu" have "2 * x / 3 + x / 3 = uu"
huffman@45435
   431
      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
huffman@45437
   432
  next
huffman@45437
   433
    assume "y + z = uu"
huffman@45437
   434
    have "x / 2 + y - 3 * x / 6 + z = uu"
huffman@45437
   435
      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
huffman@45437
   436
  next
huffman@45437
   437
    assume "1 / 15 * x + y = uu"
huffman@45437
   438
    have "7 * x / 5 + y - 4 * x / 3 = uu"
huffman@45437
   439
      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
huffman@45435
   440
  }
huffman@45435
   441
end
huffman@45224
   442
huffman@45462
   443
lemma
huffman@47108
   444
  fixes x :: "'a::{linordered_field_inverse_zero}"
huffman@45462
   445
  shows "2/3 * x + x / 3 = uu"
huffman@45284
   446
apply (tactic {* test [@{simproc field_combine_numerals}] *})?
huffman@45224
   447
oops -- "FIXME: test fails"
huffman@45224
   448
huffman@45462
   449
subsection {* @{text nat_combine_numerals} *}
huffman@45462
   450
huffman@45462
   451
notepad begin
huffman@45462
   452
  fix i j k m n u :: nat
huffman@45462
   453
  {
huffman@45462
   454
    assume "4*k = u" have "k + 3*k = u"
huffman@45462
   455
      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
huffman@45462
   456
  next
huffman@45530
   457
    (* FIXME "Suc (i + 3) \<equiv> i + 4" *)
huffman@45462
   458
    assume "4 * Suc 0 + i = u" have "Suc (i + 3) = u"
huffman@45462
   459
      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
huffman@45462
   460
  next
huffman@45530
   461
    (* FIXME "Suc (i + j + 3 + k) \<equiv> i + j + 4 + k" *)
huffman@45462
   462
    assume "4 * Suc 0 + (i + (j + k)) = u" have "Suc (i + j + 3 + k) = u"
huffman@45462
   463
      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
huffman@45462
   464
  next
huffman@45462
   465
    assume "2 * j + 4 * k = u" have "k + j + 3*k + j = u"
huffman@45462
   466
      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
huffman@45462
   467
  next
huffman@45462
   468
    assume "6 * Suc 0 + (5 * (i * j) + (4 * k + i)) = u"
huffman@45462
   469
    have "Suc (j*i + i + k + 5 + 3*k + i*j*4) = u"
huffman@45462
   470
      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
huffman@45462
   471
  next
huffman@45462
   472
    assume "5 * (m * n) = u" have "(2*n*m) + (3*(m*n)) = u"
huffman@45462
   473
      by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
huffman@45462
   474
  }
huffman@45462
   475
end
huffman@45462
   476
huffman@45436
   477
subsection {* @{text nateq_cancel_numerals} *}
huffman@45436
   478
huffman@45436
   479
notepad begin
huffman@45436
   480
  fix i j k l oo u uu vv w y z w' y' z' :: "nat"
huffman@45436
   481
  {
huffman@47108
   482
    assume "Suc 0 * u = 0" have "2*u = (u::nat)"
huffman@45436
   483
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436
   484
  next
huffman@45436
   485
    assume "Suc 0 * u = Suc 0" have "2*u = Suc (u)"
huffman@45436
   486
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436
   487
  next
huffman@45436
   488
    assume "i + (j + k) = 3 * Suc 0 + (u + y)"
huffman@45436
   489
    have "(i + j + 12 + k) = u + 15 + y"
huffman@45436
   490
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436
   491
  next
huffman@45436
   492
    assume "7 * Suc 0 + (i + (j + k)) = u + y"
huffman@45436
   493
    have "(i + j + 12 + k) = u + 5 + y"
huffman@45436
   494
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436
   495
  next
huffman@45436
   496
    assume "11 * Suc 0 + (i + (j + k)) = u + y"
huffman@45436
   497
    have "(i + j + 12 + k) = Suc (u + y)"
huffman@45436
   498
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436
   499
  next
huffman@45436
   500
    assume "i + (j + k) = 2 * Suc 0 + (u + y)"
huffman@45436
   501
    have "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))"
huffman@45436
   502
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436
   503
  next
huffman@45436
   504
    assume "Suc 0 * u + (2 * y + 3 * z) = Suc 0"
huffman@45436
   505
    have "2*y + 3*z + 2*u = Suc (u)"
huffman@45436
   506
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436
   507
  next
huffman@45436
   508
    assume "Suc 0 * u + (2 * y + (3 * z + (6 * w + (2 * y + 3 * z)))) = Suc 0"
huffman@45436
   509
    have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)"
huffman@45436
   510
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436
   511
  next
huffman@45436
   512
    assume "Suc 0 * u + (2 * y + (3 * z + (6 * w + (2 * y + 3 * z)))) =
huffman@45436
   513
      2 * y' + (3 * z' + (6 * w' + (2 * y' + (3 * z' + vv))))"
huffman@45436
   514
    have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u =
huffman@45436
   515
      2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + vv"
huffman@45436
   516
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436
   517
  next
huffman@45436
   518
    assume "2 * u + (2 * z + (5 * Suc 0 + 2 * y)) = vv"
huffman@45436
   519
    have "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)"
huffman@45436
   520
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436
   521
  }
huffman@45224
   522
end
huffman@45436
   523
huffman@45436
   524
subsection {* @{text natless_cancel_numerals} *}
huffman@45436
   525
huffman@45436
   526
notepad begin
huffman@45436
   527
  fix length :: "'a \<Rightarrow> nat" and l1 l2 xs :: "'a" and f :: "nat \<Rightarrow> 'a"
huffman@47108
   528
  fix c i j k l m oo u uu vv w y z w' y' z' :: "nat"
huffman@45436
   529
  {
huffman@45436
   530
    assume "0 < j" have "(2*length xs < 2*length xs + j)"
huffman@45436
   531
      by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
huffman@45436
   532
  next
huffman@45436
   533
    assume "0 < j" have "(2*length xs < length xs * 2 + j)"
huffman@45436
   534
      by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
huffman@45436
   535
  next
huffman@45436
   536
    assume "i + (j + k) < u + y"
huffman@45436
   537
    have "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))"
huffman@45436
   538
      by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
huffman@45436
   539
  next
huffman@45436
   540
    assume "0 < Suc 0 * (m * n) + u" have "(2*n*m) < (3*(m*n)) + u"
huffman@45436
   541
      by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
huffman@45436
   542
  }
huffman@45436
   543
end
huffman@45436
   544
huffman@45436
   545
subsection {* @{text natle_cancel_numerals} *}
huffman@45436
   546
huffman@45436
   547
notepad begin
huffman@45436
   548
  fix length :: "'a \<Rightarrow> nat" and l2 l3 :: "'a" and f :: "nat \<Rightarrow> 'a"
huffman@45436
   549
  fix c e i j k l oo u uu vv w y z w' y' z' :: "nat"
huffman@45436
   550
  {
huffman@45436
   551
    assume "u + y \<le> 36 * Suc 0 + (i + (j + k))"
huffman@45436
   552
    have "Suc (Suc (Suc (Suc (Suc (u + y))))) \<le> ((i + j) + 41 + k)"
huffman@45436
   553
      by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
huffman@45436
   554
  next
huffman@45436
   555
    assume "5 * Suc 0 + (case length (f c) of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> k) = 0"
huffman@45436
   556
    have "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0 | Suc k => k)))))) \<le> Suc 0)"
huffman@45436
   557
      by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
huffman@45436
   558
  next
huffman@45436
   559
    assume "6 + length l2 = 0" have "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) \<le> length l1"
huffman@45436
   560
      by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
huffman@45436
   561
  next
huffman@45436
   562
    assume "5 + length l3 = 0"
huffman@45436
   563
    have "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length l3)))))) \<le> length (compT P E A ST mxr e))"
huffman@45436
   564
      by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
huffman@45436
   565
  next
huffman@45436
   566
    assume "5 + length (compT P E (A \<union> A' e) ST mxr c) = 0"
huffman@45436
   567
    have "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length (compT P E (A Un A' e) ST mxr c))))))) \<le> length (compT P E A ST mxr e))"
huffman@45436
   568
      by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
huffman@45436
   569
  }
huffman@45436
   570
end
huffman@45436
   571
huffman@45436
   572
subsection {* @{text natdiff_cancel_numerals} *}
huffman@45436
   573
huffman@45436
   574
notepad begin
huffman@45436
   575
  fix length :: "'a \<Rightarrow> nat" and l2 l3 :: "'a" and f :: "nat \<Rightarrow> 'a"
huffman@45436
   576
  fix c e i j k l oo u uu vv v w x y z zz w' y' z' :: "nat"
huffman@45436
   577
  {
huffman@45436
   578
    assume "i + (j + k) - 3 * Suc 0 = y" have "(i + j + 12 + k) - 15 = y"
huffman@45436
   579
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   580
  next
huffman@45436
   581
    assume "7 * Suc 0 + (i + (j + k)) - 0 = y" have "(i + j + 12 + k) - 5 = y"
huffman@45436
   582
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   583
  next
huffman@45436
   584
    assume "u - Suc 0 * Suc 0 = y" have "Suc u - 2 = y"
huffman@45436
   585
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   586
  next
huffman@45436
   587
    assume "Suc 0 * Suc 0 + u - 0 = y" have "Suc (Suc (Suc u)) - 2 = y"
huffman@45436
   588
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   589
  next
huffman@45436
   590
    assume "Suc 0 * Suc 0 + (i + (j + k)) - 0 = y"
huffman@45436
   591
    have "(i + j + 2 + k) - 1 = y"
huffman@45436
   592
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   593
  next
huffman@45436
   594
    assume "i + (j + k) - Suc 0 * Suc 0 = y"
huffman@45436
   595
    have "(i + j + 1 + k) - 2 = y"
huffman@45436
   596
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   597
  next
huffman@45436
   598
    assume "2 * x + y - 2 * (u * v) = w"
huffman@45436
   599
    have "(2*x + (u*v) + y) - v*3*u = w"
huffman@45436
   600
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   601
  next
huffman@45436
   602
    assume "2 * x * u * v + (5 + y) - 0 = w"
huffman@45436
   603
    have "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = w"
huffman@45436
   604
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   605
  next
huffman@45436
   606
    assume "3 * (u * v) + (2 * x * u * v + y) - 0 = w"
huffman@45436
   607
    have "(2*x*u*v + (u*v)*4 + y) - v*u = w"
huffman@45436
   608
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   609
  next
huffman@45436
   610
    assume "3 * u + (2 + (2 * x * u * v + y)) - 0 = w"
huffman@45436
   611
    have "Suc (Suc (2*x*u*v + u*4 + y)) - u = w"
huffman@45436
   612
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   613
  next
huffman@45436
   614
    assume "Suc (Suc 0 * (u * v)) - 0 = w"
huffman@45436
   615
    have "Suc ((u*v)*4) - v*3*u = w"
huffman@45436
   616
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   617
  next
huffman@45436
   618
    assume "2 - 0 = w" have "Suc (Suc ((u*v)*3)) - v*3*u = w"
huffman@45436
   619
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   620
  next
huffman@45436
   621
    assume "17 * Suc 0 + (i + (j + k)) - (u + y) = zz"
huffman@45436
   622
    have "(i + j + 32 + k) - (u + 15 + y) = zz"
huffman@45436
   623
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   624
  next
huffman@45436
   625
    assume "u + y - 0 = v" have "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v"
huffman@45436
   626
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   627
  }
huffman@45436
   628
end
huffman@45436
   629
huffman@45462
   630
subsection {* Factor-cancellation simprocs for type @{typ nat} *}
huffman@45462
   631
huffman@45462
   632
text {* @{text nat_eq_cancel_factor}, @{text nat_less_cancel_factor},
huffman@45462
   633
@{text nat_le_cancel_factor}, @{text nat_divide_cancel_factor}, and
huffman@45462
   634
@{text nat_dvd_cancel_factor}. *}
huffman@45462
   635
huffman@45462
   636
notepad begin
huffman@45462
   637
  fix a b c d k x y uu :: nat
huffman@45462
   638
  {
huffman@45462
   639
    assume "k = 0 \<or> x = y" have "x*k = k*y"
huffman@45462
   640
      by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
huffman@45462
   641
  next
huffman@45462
   642
    assume "k = 0 \<or> Suc 0 = y" have "k = k*y"
huffman@45462
   643
      by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
huffman@45462
   644
  next
huffman@45462
   645
    assume "b = 0 \<or> a * c = Suc 0" have "a*(b*c) = b"
huffman@45462
   646
      by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
huffman@45462
   647
  next
huffman@45462
   648
    assume "a = 0 \<or> b = 0 \<or> c = d * x" have "a*(b*c) = d*b*(x*a)"
huffman@45462
   649
      by (tactic {* test [@{simproc nat_eq_cancel_factor}] *}) fact
huffman@45462
   650
  next
huffman@45462
   651
    assume "0 < k \<and> x < y" have "x*k < k*y"
huffman@45462
   652
      by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
huffman@45462
   653
  next
huffman@45462
   654
    assume "0 < k \<and> Suc 0 < y" have "k < k*y"
huffman@45462
   655
      by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
huffman@45462
   656
  next
huffman@45462
   657
    assume "0 < b \<and> a * c < Suc 0" have "a*(b*c) < b"
huffman@45462
   658
      by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
huffman@45462
   659
  next
huffman@45462
   660
    assume "0 < a \<and> 0 < b \<and> c < d * x" have "a*(b*c) < d*b*(x*a)"
huffman@45462
   661
      by (tactic {* test [@{simproc nat_less_cancel_factor}] *}) fact
huffman@45462
   662
  next
huffman@45462
   663
    assume "0 < k \<longrightarrow> x \<le> y" have "x*k \<le> k*y"
huffman@45462
   664
      by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
huffman@45462
   665
  next
huffman@45462
   666
    assume "0 < k \<longrightarrow> Suc 0 \<le> y" have "k \<le> k*y"
huffman@45462
   667
      by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
huffman@45462
   668
  next
huffman@45462
   669
    assume "0 < b \<longrightarrow> a * c \<le> Suc 0" have "a*(b*c) \<le> b"
huffman@45462
   670
      by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
huffman@45462
   671
  next
huffman@45462
   672
    assume "0 < a \<longrightarrow> 0 < b \<longrightarrow> c \<le> d * x" have "a*(b*c) \<le> d*b*(x*a)"
huffman@45462
   673
      by (tactic {* test [@{simproc nat_le_cancel_factor}] *}) fact
huffman@45462
   674
  next
huffman@45462
   675
    assume "(if k = 0 then 0 else x div y) = uu" have "(x*k) div (k*y) = uu"
huffman@45463
   676
      by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
huffman@45462
   677
  next
huffman@45462
   678
    assume "(if k = 0 then 0 else Suc 0 div y) = uu" have "k div (k*y) = uu"
huffman@45463
   679
      by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
huffman@45462
   680
  next
huffman@45462
   681
    assume "(if b = 0 then 0 else a * c) = uu" have "(a*(b*c)) div (b) = uu"
huffman@45463
   682
      by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
huffman@45462
   683
  next
huffman@45462
   684
    assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
huffman@45462
   685
    have "(a*(b*c)) div (d*b*(x*a)) = uu"
huffman@45463
   686
      by (tactic {* test [@{simproc nat_div_cancel_factor}] *}) fact
huffman@45462
   687
  next
huffman@45462
   688
    assume "k = 0 \<or> x dvd y" have "(x*k) dvd (k*y)"
huffman@45462
   689
      by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
huffman@45462
   690
  next
huffman@45462
   691
    assume "k = 0 \<or> Suc 0 dvd y" have "k dvd (k*y)"
huffman@45462
   692
      by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
huffman@45462
   693
  next
huffman@45462
   694
    assume "b = 0 \<or> a * c dvd Suc 0" have "(a*(b*c)) dvd (b)"
huffman@45462
   695
      by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
huffman@45462
   696
  next
huffman@45462
   697
    assume "b = 0 \<or> Suc 0 dvd a * c" have "b dvd (a*(b*c))"
huffman@45462
   698
      by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
huffman@45462
   699
  next
huffman@45462
   700
    assume "a = 0 \<or> b = 0 \<or> c dvd d * x" have "(a*(b*c)) dvd (d*b*(x*a))"
huffman@45462
   701
      by (tactic {* test [@{simproc nat_dvd_cancel_factor}] *}) fact
huffman@45462
   702
  }
huffman@45436
   703
end
huffman@45462
   704
huffman@45463
   705
subsection {* Numeral-cancellation simprocs for type @{typ nat} *}
huffman@45463
   706
huffman@45463
   707
notepad begin
huffman@45463
   708
  fix x y z :: nat
huffman@45463
   709
  {
huffman@45463
   710
    assume "3 * x = 4 * y" have "9*x = 12 * y"
huffman@45463
   711
      by (tactic {* test [@{simproc nat_eq_cancel_numeral_factor}] *}) fact
huffman@45463
   712
  next
huffman@45463
   713
    assume "3 * x < 4 * y" have "9*x < 12 * y"
huffman@45463
   714
      by (tactic {* test [@{simproc nat_less_cancel_numeral_factor}] *}) fact
huffman@45463
   715
  next
huffman@45463
   716
    assume "3 * x \<le> 4 * y" have "9*x \<le> 12 * y"
huffman@45463
   717
      by (tactic {* test [@{simproc nat_le_cancel_numeral_factor}] *}) fact
huffman@45463
   718
  next
huffman@45463
   719
    assume "(3 * x) div (4 * y) = z" have "(9*x) div (12 * y) = z"
huffman@45463
   720
      by (tactic {* test [@{simproc nat_div_cancel_numeral_factor}] *}) fact
huffman@45463
   721
  next
huffman@45463
   722
    assume "(3 * x) dvd (4 * y)" have "(9*x) dvd (12 * y)"
huffman@45463
   723
      by (tactic {* test [@{simproc nat_dvd_cancel_numeral_factor}] *}) fact
huffman@45463
   724
  }
huffman@45462
   725
end
huffman@45463
   726
huffman@45530
   727
subsection {* Integer numeral div/mod simprocs *}
huffman@45530
   728
huffman@45530
   729
notepad begin
huffman@45530
   730
  have "(10::int) div 3 = 3"
huffman@45530
   731
    by (tactic {* test [@{simproc binary_int_div}] *})
huffman@45530
   732
  have "(10::int) mod 3 = 1"
huffman@45530
   733
    by (tactic {* test [@{simproc binary_int_mod}] *})
huffman@45530
   734
  have "(10::int) div -3 = -4"
huffman@45530
   735
    by (tactic {* test [@{simproc binary_int_div}] *})
huffman@45530
   736
  have "(10::int) mod -3 = -2"
huffman@45530
   737
    by (tactic {* test [@{simproc binary_int_mod}] *})
huffman@45530
   738
  have "(-10::int) div 3 = -4"
huffman@45530
   739
    by (tactic {* test [@{simproc binary_int_div}] *})
huffman@45530
   740
  have "(-10::int) mod 3 = 2"
huffman@45530
   741
    by (tactic {* test [@{simproc binary_int_mod}] *})
huffman@45530
   742
  have "(-10::int) div -3 = 3"
huffman@45530
   743
    by (tactic {* test [@{simproc binary_int_div}] *})
huffman@45530
   744
  have "(-10::int) mod -3 = -1"
huffman@45530
   745
    by (tactic {* test [@{simproc binary_int_mod}] *})
huffman@45530
   746
  have "(8452::int) mod 3 = 1"
huffman@45530
   747
    by (tactic {* test [@{simproc binary_int_mod}] *})
huffman@45530
   748
  have "(59485::int) div 434 = 137"
huffman@45530
   749
    by (tactic {* test [@{simproc binary_int_div}] *})
huffman@45530
   750
  have "(1000006::int) mod 10 = 6"
huffman@45530
   751
    by (tactic {* test [@{simproc binary_int_mod}] *})
huffman@45530
   752
  have "10000000 div 2 = (5000000::int)"
huffman@45530
   753
    by (tactic {* test [@{simproc binary_int_div}] *})
huffman@45530
   754
  have "10000001 mod 2 = (1::int)"
huffman@45530
   755
    by (tactic {* test [@{simproc binary_int_mod}] *})
huffman@45530
   756
  have "10000055 div 32 = (312501::int)"
huffman@45530
   757
    by (tactic {* test [@{simproc binary_int_div}] *})
huffman@45530
   758
  have "10000055 mod 32 = (23::int)"
huffman@45530
   759
    by (tactic {* test [@{simproc binary_int_mod}] *})
huffman@45530
   760
  have "100094 div 144 = (695::int)"
huffman@45530
   761
    by (tactic {* test [@{simproc binary_int_div}] *})
huffman@45530
   762
  have "100094 mod 144 = (14::int)"
huffman@45530
   763
    by (tactic {* test [@{simproc binary_int_mod}] *})
huffman@45463
   764
end
huffman@45530
   765
huffman@45530
   766
end