src/HOL/ex/Simproc_Tests.thy
author huffman
Wed Nov 09 15:33:24 2011 +0100 (2011-11-09)
changeset 45437 958d19d3405b
parent 45436 62bc9474d04b
child 45462 aba629d6cee5
permissions -rw-r--r--
tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
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@45435
    27
notepad begin
huffman@45435
    28
  fix a b c d oo uu i j k l u v w x y z :: "'a::number_ring"
huffman@45435
    29
  {
huffman@45435
    30
    assume "10 + (2 * l + oo) = uu"
huffman@45435
    31
    have "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = uu"
huffman@45435
    32
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
    33
  next
huffman@45435
    34
    assume "-3 + (i + (j + k)) = y"
huffman@45435
    35
    have "(i + j + 12 + k) - 15 = y"
huffman@45435
    36
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
    37
  next
huffman@45435
    38
    assume "7 + (i + (j + k)) = y"
huffman@45435
    39
    have "(i + j + 12 + k) - 5 = y"
huffman@45435
    40
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
    41
  next
huffman@45435
    42
    assume "-4 * (u * v) + (2 * x + y) = w"
huffman@45435
    43
    have "(2*x - (u*v) + y) - v*3*u = w"
huffman@45435
    44
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
    45
  next
huffman@45437
    46
    assume "2 * x * u * v + y = w"
huffman@45435
    47
    have "(2*x*u*v + (u*v)*4 + y) - v*u*4 = w"
huffman@45435
    48
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
    49
  next
huffman@45435
    50
    assume "3 * (u * v) + (2 * x * u * v + y) = w"
huffman@45435
    51
    have "(2*x*u*v + (u*v)*4 + y) - v*u = w"
huffman@45435
    52
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
    53
  next
huffman@45435
    54
    assume "-3 * (u * v) + (- (x * u * v) + - y) = w"
huffman@45435
    55
    have "u*v - (x*u*v + (u*v)*4 + y) = w"
huffman@45435
    56
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
    57
  next
huffman@45437
    58
    assume "a + - c = d"
huffman@45435
    59
    have "a + -(b+c) + b = d"
huffman@45435
    60
      apply (simp only: minus_add_distrib)
huffman@45435
    61
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
    62
  next
huffman@45435
    63
    assume "-2 * b + (a + - c) = d"
huffman@45435
    64
    have "a + -(b+c) - b = d"
huffman@45435
    65
      apply (simp only: minus_add_distrib)
huffman@45435
    66
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
    67
  next
huffman@45435
    68
    assume "-7 + (i + (j + (k + (- u + - y)))) = z"
huffman@45435
    69
    have "(i + j + -2 + k) - (u + 5 + y) = z"
huffman@45435
    70
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
    71
  next
huffman@45435
    72
    assume "-27 + (i + (j + k)) = y"
huffman@45435
    73
    have "(i + j + -12 + k) - 15 = y"
huffman@45435
    74
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
    75
  next
huffman@45435
    76
    assume "27 + (i + (j + k)) = y"
huffman@45435
    77
    have "(i + j + 12 + k) - -15 = y"
huffman@45435
    78
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
    79
  next
huffman@45435
    80
    assume "3 + (i + (j + k)) = y"
huffman@45435
    81
    have "(i + j + -12 + k) - -15 = y"
huffman@45435
    82
      by (tactic {* test [@{simproc int_combine_numerals}] *}) fact
huffman@45435
    83
  }
huffman@45435
    84
end
huffman@45224
    85
huffman@45224
    86
subsection {* @{text inteq_cancel_numerals} *}
huffman@45224
    87
huffman@45435
    88
notepad begin
huffman@45435
    89
  fix i j k u vv w y z w' y' z' :: "'a::number_ring"
huffman@45435
    90
  {
huffman@45437
    91
    assume "u = 0" have "2*u = u"
huffman@45435
    92
      by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
huffman@45224
    93
(* conclusion matches Rings.ring_1_no_zero_divisors_class.mult_cancel_right2 *)
huffman@45435
    94
  next
huffman@45435
    95
    assume "i + (j + k) = 3 + (u + y)"
huffman@45435
    96
    have "(i + j + 12 + k) = u + 15 + y"
huffman@45435
    97
      by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
huffman@45435
    98
  next
huffman@45435
    99
    assume "7 + (j + (i + k)) = y"
huffman@45435
   100
    have "(i + j*2 + 12 + k) = j + 5 + y"
huffman@45435
   101
      by (tactic {* test [@{simproc inteq_cancel_numerals}] *}) fact
huffman@45435
   102
  next
huffman@45435
   103
    assume "u + (6*z + (4*y + 6*w)) = 6*z' + (4*y' + (6*w' + vv))"
huffman@45435
   104
    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
   105
      by (tactic {* test [@{simproc int_combine_numerals}, @{simproc inteq_cancel_numerals}] *}) fact
huffman@45435
   106
  }
huffman@45435
   107
end
huffman@45224
   108
huffman@45224
   109
subsection {* @{text intless_cancel_numerals} *}
huffman@45224
   110
huffman@45435
   111
notepad begin
huffman@45435
   112
  fix b c i j k u y :: "'a::{linordered_idom,number_ring}"
huffman@45435
   113
  {
huffman@45435
   114
    assume "y < 2 * b" have "y - b < b"
huffman@45435
   115
      by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
huffman@45435
   116
  next
huffman@45435
   117
    assume "c + y < 4 * b" have "y - (3*b + c) < b - 2*c"
huffman@45435
   118
      by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
huffman@45435
   119
  next
huffman@45435
   120
    assume "i + (j + k) < 8 + (u + y)"
huffman@45435
   121
    have "(i + j + -3 + k) < u + 5 + y"
huffman@45435
   122
      by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
huffman@45435
   123
  next
huffman@45435
   124
    assume "9 + (i + (j + k)) < u + y"
huffman@45435
   125
    have "(i + j + 3 + k) < u + -6 + y"
huffman@45435
   126
      by (tactic {* test [@{simproc intless_cancel_numerals}] *}) fact
huffman@45435
   127
  }
huffman@45435
   128
end
huffman@45224
   129
huffman@45224
   130
subsection {* @{text ring_eq_cancel_numeral_factor} *}
huffman@45224
   131
huffman@45435
   132
notepad begin
huffman@45435
   133
  fix x y :: "'a::{idom,ring_char_0,number_ring}"
huffman@45435
   134
  {
huffman@45435
   135
    assume "3*x = 4*y" have "9*x = 12 * y"
huffman@45435
   136
      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
huffman@45435
   137
  next
huffman@45435
   138
    assume "-3*x = 4*y" have "-99*x = 132 * y"
huffman@45435
   139
      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
huffman@45435
   140
  next
huffman@45435
   141
    assume "111*x = -44*y" have "999*x = -396 * y"
huffman@45435
   142
      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
huffman@45435
   143
  next
huffman@45435
   144
    assume "11*x = 9*y" have "-99*x = -81 * y"
huffman@45435
   145
      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
huffman@45435
   146
  next
huffman@45437
   147
    assume "2*x = y" have "-2 * x = -1 * y"
huffman@45435
   148
      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
huffman@45435
   149
  next
huffman@45437
   150
    assume "2*x = y" have "-2 * x = -y"
huffman@45435
   151
      by (tactic {* test [@{simproc ring_eq_cancel_numeral_factor}] *}) fact
huffman@45435
   152
  }
huffman@45435
   153
end
huffman@45224
   154
huffman@45224
   155
subsection {* @{text int_div_cancel_numeral_factors} *}
huffman@45224
   156
huffman@45435
   157
notepad begin
huffman@45435
   158
  fix x y z :: "'a::{semiring_div,ring_char_0,number_ring}"
huffman@45435
   159
  {
huffman@45435
   160
    assume "(3*x) div (4*y) = z" have "(9*x) div (12*y) = z"
huffman@45435
   161
      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
huffman@45435
   162
  next
huffman@45435
   163
    assume "(-3*x) div (4*y) = z" have "(-99*x) div (132*y) = z"
huffman@45435
   164
      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
huffman@45435
   165
  next
huffman@45435
   166
    assume "(111*x) div (-44*y) = z" have "(999*x) div (-396*y) = z"
huffman@45435
   167
      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
huffman@45435
   168
  next
huffman@45435
   169
    assume "(11*x) div (9*y) = z" have "(-99*x) div (-81*y) = z"
huffman@45435
   170
      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
huffman@45435
   171
  next
huffman@45437
   172
    assume "(2*x) div y = z"
huffman@45435
   173
    have "(-2 * x) div (-1 * y) = z"
huffman@45435
   174
      by (tactic {* test [@{simproc int_div_cancel_numeral_factors}] *}) fact
huffman@45435
   175
  }
huffman@45435
   176
end
huffman@45224
   177
huffman@45224
   178
subsection {* @{text ring_less_cancel_numeral_factor} *}
huffman@45224
   179
huffman@45435
   180
notepad begin
huffman@45435
   181
  fix x y :: "'a::{linordered_idom,number_ring}"
huffman@45435
   182
  {
huffman@45435
   183
    assume "3*x < 4*y" have "9*x < 12 * y"
huffman@45435
   184
      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
huffman@45435
   185
  next
huffman@45435
   186
    assume "-3*x < 4*y" have "-99*x < 132 * y"
huffman@45435
   187
      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
huffman@45435
   188
  next
huffman@45435
   189
    assume "111*x < -44*y" have "999*x < -396 * y"
huffman@45435
   190
      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
huffman@45435
   191
  next
huffman@45435
   192
    assume "9*y < 11*x" have "-99*x < -81 * y"
huffman@45435
   193
      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
huffman@45435
   194
  next
huffman@45437
   195
    assume "y < 2*x" have "-2 * x < -y"
huffman@45435
   196
      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
huffman@45435
   197
  next
huffman@45437
   198
    assume "23*y < x" have "-x < -23 * y"
huffman@45435
   199
      by (tactic {* test [@{simproc ring_less_cancel_numeral_factor}] *}) fact
huffman@45435
   200
  }
huffman@45435
   201
end
huffman@45224
   202
huffman@45224
   203
subsection {* @{text ring_le_cancel_numeral_factor} *}
huffman@45224
   204
huffman@45435
   205
notepad begin
huffman@45435
   206
  fix x y :: "'a::{linordered_idom,number_ring}"
huffman@45435
   207
  {
huffman@45435
   208
    assume "3*x \<le> 4*y" have "9*x \<le> 12 * y"
huffman@45435
   209
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435
   210
  next
huffman@45435
   211
    assume "-3*x \<le> 4*y" have "-99*x \<le> 132 * y"
huffman@45435
   212
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435
   213
  next
huffman@45435
   214
    assume "111*x \<le> -44*y" have "999*x \<le> -396 * y"
huffman@45435
   215
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435
   216
  next
huffman@45435
   217
    assume "9*y \<le> 11*x" have "-99*x \<le> -81 * y"
huffman@45435
   218
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435
   219
  next
huffman@45437
   220
    assume "y \<le> 2*x" have "-2 * x \<le> -1 * y"
huffman@45435
   221
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435
   222
  next
huffman@45437
   223
    assume "23*y \<le> x" have "-x \<le> -23 * y"
huffman@45435
   224
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435
   225
  next
huffman@45437
   226
    assume "y \<le> 0" have "0 \<le> y * -2"
huffman@45435
   227
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435
   228
  next
huffman@45437
   229
    assume "- x \<le> y" have "- (2 * x) \<le> 2*y"
huffman@45435
   230
      by (tactic {* test [@{simproc ring_le_cancel_numeral_factor}] *}) fact
huffman@45435
   231
  }
huffman@45435
   232
end
huffman@45224
   233
huffman@45285
   234
subsection {* @{text divide_cancel_numeral_factor} *}
huffman@45224
   235
huffman@45435
   236
notepad begin
huffman@45435
   237
  fix x y z :: "'a::{field_inverse_zero,ring_char_0,number_ring}"
huffman@45435
   238
  {
huffman@45435
   239
    assume "(3*x) / (4*y) = z" have "(9*x) / (12 * y) = z"
huffman@45435
   240
      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
huffman@45435
   241
  next
huffman@45435
   242
    assume "(-3*x) / (4*y) = z" have "(-99*x) / (132 * y) = z"
huffman@45435
   243
      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
huffman@45435
   244
  next
huffman@45435
   245
    assume "(111*x) / (-44*y) = z" have "(999*x) / (-396 * y) = z"
huffman@45435
   246
      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
huffman@45435
   247
  next
huffman@45435
   248
    assume "(11*x) / (9*y) = z" have "(-99*x) / (-81 * y) = z"
huffman@45435
   249
      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
huffman@45435
   250
  next
huffman@45437
   251
    assume "(2*x) / y = z" have "(-2 * x) / (-1 * y) = z"
huffman@45435
   252
      by (tactic {* test [@{simproc divide_cancel_numeral_factor}] *}) fact
huffman@45435
   253
  }
huffman@45435
   254
end
huffman@45224
   255
huffman@45224
   256
subsection {* @{text ring_eq_cancel_factor} *}
huffman@45224
   257
huffman@45435
   258
notepad begin
huffman@45435
   259
  fix a b c d k x y :: "'a::idom"
huffman@45435
   260
  {
huffman@45435
   261
    assume "k = 0 \<or> x = y" have "x*k = k*y"
huffman@45435
   262
      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
huffman@45435
   263
  next
huffman@45435
   264
    assume "k = 0 \<or> 1 = y" have "k = k*y"
huffman@45435
   265
      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
huffman@45435
   266
  next
huffman@45435
   267
    assume "b = 0 \<or> a*c = 1" have "a*(b*c) = b"
huffman@45435
   268
      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
huffman@45435
   269
  next
huffman@45435
   270
    assume "a = 0 \<or> b = 0 \<or> c = d*x" have "a*(b*c) = d*b*(x*a)"
huffman@45435
   271
      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
huffman@45435
   272
  next
huffman@45435
   273
    assume "k = 0 \<or> x = y" have "x*k = k*y"
huffman@45435
   274
      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
huffman@45435
   275
  next
huffman@45435
   276
    assume "k = 0 \<or> 1 = y" have "k = k*y"
huffman@45435
   277
      by (tactic {* test [@{simproc ring_eq_cancel_factor}] *}) fact
huffman@45435
   278
  }
huffman@45435
   279
end
huffman@45224
   280
huffman@45224
   281
subsection {* @{text int_div_cancel_factor} *}
huffman@45224
   282
huffman@45435
   283
notepad begin
huffman@45435
   284
  fix a b c d k uu x y :: "'a::semiring_div"
huffman@45435
   285
  {
huffman@45435
   286
    assume "(if k = 0 then 0 else x div y) = uu"
huffman@45435
   287
    have "(x*k) div (k*y) = uu"
huffman@45435
   288
      by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
huffman@45435
   289
  next
huffman@45435
   290
    assume "(if k = 0 then 0 else 1 div y) = uu"
huffman@45435
   291
    have "(k) div (k*y) = uu"
huffman@45435
   292
      by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
huffman@45435
   293
  next
huffman@45435
   294
    assume "(if b = 0 then 0 else a * c) = uu"
huffman@45435
   295
    have "(a*(b*c)) div b = uu"
huffman@45435
   296
      by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
huffman@45435
   297
  next
huffman@45435
   298
    assume "(if a = 0 then 0 else if b = 0 then 0 else c div (d * x)) = uu"
huffman@45435
   299
    have "(a*(b*c)) div (d*b*(x*a)) = uu"
huffman@45435
   300
      by (tactic {* test [@{simproc int_div_cancel_factor}] *}) fact
huffman@45435
   301
  }
huffman@45435
   302
end
huffman@45224
   303
huffman@45224
   304
subsection {* @{text divide_cancel_factor} *}
huffman@45224
   305
huffman@45435
   306
notepad begin
huffman@45435
   307
  fix a b c d k uu x y :: "'a::field_inverse_zero"
huffman@45435
   308
  {
huffman@45435
   309
    assume "(if k = 0 then 0 else x / y) = uu"
huffman@45435
   310
    have "(x*k) / (k*y) = uu"
huffman@45435
   311
      by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
huffman@45435
   312
  next
huffman@45435
   313
    assume "(if k = 0 then 0 else 1 / y) = uu"
huffman@45435
   314
    have "(k) / (k*y) = uu"
huffman@45435
   315
      by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
huffman@45435
   316
  next
huffman@45435
   317
    assume "(if b = 0 then 0 else a * c / 1) = uu"
huffman@45435
   318
    have "(a*(b*c)) / b = uu"
huffman@45435
   319
      by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
huffman@45435
   320
  next
huffman@45435
   321
    assume "(if a = 0 then 0 else if b = 0 then 0 else c / (d * x)) = uu"
huffman@45435
   322
    have "(a*(b*c)) / (d*b*(x*a)) = uu"
huffman@45435
   323
      by (tactic {* test [@{simproc divide_cancel_factor}] *}) fact
huffman@45435
   324
  }
huffman@45435
   325
end
huffman@45224
   326
huffman@45224
   327
lemma shows "a*(b*c)/(y*z) = d*(b::rat)*(x*a)/z"
huffman@45224
   328
oops -- "FIXME: need simproc to cover this case"
huffman@45224
   329
huffman@45224
   330
huffman@45224
   331
subsection {* @{text linordered_ring_less_cancel_factor} *}
huffman@45224
   332
huffman@45435
   333
notepad begin
huffman@45435
   334
  fix x y z :: "'a::linordered_idom"
huffman@45435
   335
  {
huffman@45435
   336
    assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> x*z < y*z"
huffman@45435
   337
      by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
huffman@45435
   338
  next
huffman@45435
   339
    assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> x*z < z*y"
huffman@45435
   340
      by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
huffman@45435
   341
  next
huffman@45435
   342
    assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> z*x < y*z"
huffman@45435
   343
      by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
huffman@45435
   344
  next
huffman@45435
   345
    assume "0 < z \<Longrightarrow> x < y" have "0 < z \<Longrightarrow> z*x < z*y"
huffman@45435
   346
      by (tactic {* test [@{simproc linordered_ring_less_cancel_factor}] *}) fact
huffman@45435
   347
  }
huffman@45435
   348
end
huffman@45224
   349
huffman@45224
   350
subsection {* @{text linordered_ring_le_cancel_factor} *}
huffman@45224
   351
huffman@45435
   352
notepad begin
huffman@45435
   353
  fix x y z :: "'a::linordered_idom"
huffman@45435
   354
  {
huffman@45435
   355
    assume "0 < z \<Longrightarrow> x \<le> y" have "0 < z \<Longrightarrow> x*z \<le> y*z"
huffman@45435
   356
      by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
huffman@45435
   357
  next
huffman@45435
   358
    assume "0 < z \<Longrightarrow> x \<le> y" have "0 < z \<Longrightarrow> z*x \<le> z*y"
huffman@45435
   359
      by (tactic {* test [@{simproc linordered_ring_le_cancel_factor}] *}) fact
huffman@45435
   360
  }
huffman@45435
   361
end
huffman@45224
   362
huffman@45224
   363
subsection {* @{text field_combine_numerals} *}
huffman@45224
   364
huffman@45435
   365
notepad begin
huffman@45437
   366
  fix x y z uu :: "'a::{field_inverse_zero,ring_char_0,number_ring}"
huffman@45435
   367
  {
huffman@45435
   368
    assume "5 / 6 * x = uu" have "x / 2 + x / 3 = uu"
huffman@45435
   369
      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
huffman@45435
   370
  next
huffman@45435
   371
    assume "6 / 9 * x + y = uu" have "x / 3 + y + x / 3 = uu"
huffman@45435
   372
      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
huffman@45435
   373
  next
huffman@45435
   374
    assume "9 / 9 * x = uu" have "2 * x / 3 + x / 3 = uu"
huffman@45435
   375
      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
huffman@45437
   376
  next
huffman@45437
   377
    assume "y + z = uu"
huffman@45437
   378
    have "x / 2 + y - 3 * x / 6 + z = uu"
huffman@45437
   379
      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
huffman@45437
   380
  next
huffman@45437
   381
    assume "1 / 15 * x + y = uu"
huffman@45437
   382
    have "7 * x / 5 + y - 4 * x / 3 = uu"
huffman@45437
   383
      by (tactic {* test [@{simproc field_combine_numerals}] *}) fact
huffman@45435
   384
  }
huffman@45435
   385
end
huffman@45224
   386
huffman@45224
   387
lemma "2/3 * (x::rat) + x / 3 = uu"
huffman@45284
   388
apply (tactic {* test [@{simproc field_combine_numerals}] *})?
huffman@45224
   389
oops -- "FIXME: test fails"
huffman@45224
   390
huffman@45436
   391
subsection {* @{text nateq_cancel_numerals} *}
huffman@45436
   392
huffman@45436
   393
notepad begin
huffman@45436
   394
  fix i j k l oo u uu vv w y z w' y' z' :: "nat"
huffman@45436
   395
  {
huffman@45436
   396
    assume "Suc 0 * u = 0" have "2*u = (u::nat)"
huffman@45436
   397
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436
   398
  next
huffman@45436
   399
    assume "Suc 0 * u = Suc 0" have "2*u = Suc (u)"
huffman@45436
   400
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436
   401
  next
huffman@45436
   402
    assume "i + (j + k) = 3 * Suc 0 + (u + y)"
huffman@45436
   403
    have "(i + j + 12 + k) = u + 15 + y"
huffman@45436
   404
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436
   405
  next
huffman@45436
   406
    assume "7 * Suc 0 + (i + (j + k)) = u + y"
huffman@45436
   407
    have "(i + j + 12 + k) = u + 5 + y"
huffman@45436
   408
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436
   409
  next
huffman@45436
   410
    assume "11 * Suc 0 + (i + (j + k)) = u + y"
huffman@45436
   411
    have "(i + j + 12 + k) = Suc (u + y)"
huffman@45436
   412
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436
   413
  next
huffman@45436
   414
    assume "i + (j + k) = 2 * Suc 0 + (u + y)"
huffman@45436
   415
    have "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))"
huffman@45436
   416
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436
   417
  next
huffman@45436
   418
    assume "Suc 0 * u + (2 * y + 3 * z) = Suc 0"
huffman@45436
   419
    have "2*y + 3*z + 2*u = Suc (u)"
huffman@45436
   420
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436
   421
  next
huffman@45436
   422
    assume "Suc 0 * u + (2 * y + (3 * z + (6 * w + (2 * y + 3 * z)))) = Suc 0"
huffman@45436
   423
    have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)"
huffman@45436
   424
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436
   425
  next
huffman@45436
   426
    assume "Suc 0 * u + (2 * y + (3 * z + (6 * w + (2 * y + 3 * z)))) =
huffman@45436
   427
      2 * y' + (3 * z' + (6 * w' + (2 * y' + (3 * z' + vv))))"
huffman@45436
   428
    have "2*y + 3*z + 6*w + 2*y + 3*z + 2*u =
huffman@45436
   429
      2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + vv"
huffman@45436
   430
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436
   431
  next
huffman@45436
   432
    assume "2 * u + (2 * z + (5 * Suc 0 + 2 * y)) = vv"
huffman@45436
   433
    have "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)"
huffman@45436
   434
      by (tactic {* test [@{simproc nateq_cancel_numerals}] *}) fact
huffman@45436
   435
  }
huffman@45224
   436
end
huffman@45436
   437
huffman@45436
   438
subsection {* @{text natless_cancel_numerals} *}
huffman@45436
   439
huffman@45436
   440
notepad begin
huffman@45436
   441
  fix length :: "'a \<Rightarrow> nat" and l1 l2 xs :: "'a" and f :: "nat \<Rightarrow> 'a"
huffman@45436
   442
  fix c i j k l oo u uu vv w y z w' y' z' :: "nat"
huffman@45436
   443
  {
huffman@45436
   444
    assume "0 < j" have "(2*length xs < 2*length xs + j)"
huffman@45436
   445
      by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
huffman@45436
   446
  next
huffman@45436
   447
    assume "0 < j" have "(2*length xs < length xs * 2 + j)"
huffman@45436
   448
      by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
huffman@45436
   449
  next
huffman@45436
   450
    assume "i + (j + k) < u + y"
huffman@45436
   451
    have "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))"
huffman@45436
   452
      by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
huffman@45436
   453
  next
huffman@45436
   454
    assume "0 < Suc 0 * (m * n) + u" have "(2*n*m) < (3*(m*n)) + u"
huffman@45436
   455
      by (tactic {* test [@{simproc natless_cancel_numerals}] *}) fact
huffman@45436
   456
  next
huffman@45436
   457
    (* FIXME: negative numerals fail
huffman@45436
   458
    have "(i + j + -23 + (k::nat)) < u + 15 + y"
huffman@45436
   459
      apply (tactic {* test [@{simproc natless_cancel_numerals}] *})?
huffman@45436
   460
      sorry
huffman@45436
   461
    have "(i + j + 3 + (k::nat)) < u + -15 + y"
huffman@45436
   462
      apply (tactic {* test [@{simproc natless_cancel_numerals}] *})?
huffman@45436
   463
      sorry*)
huffman@45436
   464
  }
huffman@45436
   465
end
huffman@45436
   466
huffman@45436
   467
subsection {* @{text natle_cancel_numerals} *}
huffman@45436
   468
huffman@45436
   469
notepad begin
huffman@45436
   470
  fix length :: "'a \<Rightarrow> nat" and l2 l3 :: "'a" and f :: "nat \<Rightarrow> 'a"
huffman@45436
   471
  fix c e i j k l oo u uu vv w y z w' y' z' :: "nat"
huffman@45436
   472
  {
huffman@45436
   473
    assume "u + y \<le> 36 * Suc 0 + (i + (j + k))"
huffman@45436
   474
    have "Suc (Suc (Suc (Suc (Suc (u + y))))) \<le> ((i + j) + 41 + k)"
huffman@45436
   475
      by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
huffman@45436
   476
  next
huffman@45436
   477
    assume "5 * Suc 0 + (case length (f c) of 0 \<Rightarrow> 0 | Suc k \<Rightarrow> k) = 0"
huffman@45436
   478
    have "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0 | Suc k => k)))))) \<le> Suc 0)"
huffman@45436
   479
      by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
huffman@45436
   480
  next
huffman@45436
   481
    assume "6 + length l2 = 0" have "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) \<le> length l1"
huffman@45436
   482
      by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
huffman@45436
   483
  next
huffman@45436
   484
    assume "5 + length l3 = 0"
huffman@45436
   485
    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
   486
      by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
huffman@45436
   487
  next
huffman@45436
   488
    assume "5 + length (compT P E (A \<union> A' e) ST mxr c) = 0"
huffman@45436
   489
    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
   490
      by (tactic {* test [@{simproc natle_cancel_numerals}] *}) fact
huffman@45436
   491
  }
huffman@45436
   492
end
huffman@45436
   493
huffman@45436
   494
subsection {* @{text natdiff_cancel_numerals} *}
huffman@45436
   495
huffman@45436
   496
notepad begin
huffman@45436
   497
  fix length :: "'a \<Rightarrow> nat" and l2 l3 :: "'a" and f :: "nat \<Rightarrow> 'a"
huffman@45436
   498
  fix c e i j k l oo u uu vv v w x y z zz w' y' z' :: "nat"
huffman@45436
   499
  {
huffman@45436
   500
    assume "i + (j + k) - 3 * Suc 0 = y" have "(i + j + 12 + k) - 15 = y"
huffman@45436
   501
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   502
  next
huffman@45436
   503
    assume "7 * Suc 0 + (i + (j + k)) - 0 = y" have "(i + j + 12 + k) - 5 = y"
huffman@45436
   504
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   505
  next
huffman@45436
   506
    assume "u - Suc 0 * Suc 0 = y" have "Suc u - 2 = y"
huffman@45436
   507
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   508
  next
huffman@45436
   509
    assume "Suc 0 * Suc 0 + u - 0 = y" have "Suc (Suc (Suc u)) - 2 = y"
huffman@45436
   510
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   511
  next
huffman@45436
   512
    assume "Suc 0 * Suc 0 + (i + (j + k)) - 0 = y"
huffman@45436
   513
    have "(i + j + 2 + k) - 1 = y"
huffman@45436
   514
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   515
  next
huffman@45436
   516
    assume "i + (j + k) - Suc 0 * Suc 0 = y"
huffman@45436
   517
    have "(i + j + 1 + k) - 2 = y"
huffman@45436
   518
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   519
  next
huffman@45436
   520
    assume "2 * x + y - 2 * (u * v) = w"
huffman@45436
   521
    have "(2*x + (u*v) + y) - v*3*u = w"
huffman@45436
   522
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   523
  next
huffman@45436
   524
    assume "2 * x * u * v + (5 + y) - 0 = w"
huffman@45436
   525
    have "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = w"
huffman@45436
   526
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   527
  next
huffman@45436
   528
    assume "3 * (u * v) + (2 * x * u * v + y) - 0 = w"
huffman@45436
   529
    have "(2*x*u*v + (u*v)*4 + y) - v*u = w"
huffman@45436
   530
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   531
  next
huffman@45436
   532
    assume "3 * u + (2 + (2 * x * u * v + y)) - 0 = w"
huffman@45436
   533
    have "Suc (Suc (2*x*u*v + u*4 + y)) - u = w"
huffman@45436
   534
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   535
  next
huffman@45436
   536
    assume "Suc (Suc 0 * (u * v)) - 0 = w"
huffman@45436
   537
    have "Suc ((u*v)*4) - v*3*u = w"
huffman@45436
   538
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   539
  next
huffman@45436
   540
    assume "2 - 0 = w" have "Suc (Suc ((u*v)*3)) - v*3*u = w"
huffman@45436
   541
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   542
  next
huffman@45436
   543
    assume "17 * Suc 0 + (i + (j + k)) - (u + y) = zz"
huffman@45436
   544
    have "(i + j + 32 + k) - (u + 15 + y) = zz"
huffman@45436
   545
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   546
  next
huffman@45436
   547
    assume "u + y - 0 = v" have "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v"
huffman@45436
   548
      by (tactic {* test [@{simproc natdiff_cancel_numerals}] *}) fact
huffman@45436
   549
  next
huffman@45436
   550
    (* FIXME: negative numerals fail
huffman@45436
   551
    have "(i + j + -12 + k) - 15 = y"
huffman@45436
   552
      apply (tactic {* test [@{simproc natdiff_cancel_numerals}] *})?
huffman@45436
   553
      sorry
huffman@45436
   554
    have "(i + j + 12 + k) - -15 = y"
huffman@45436
   555
      apply (tactic {* test [@{simproc natdiff_cancel_numerals}] *})?
huffman@45436
   556
      sorry
huffman@45436
   557
    have "(i + j + -12 + k) - -15 = y"
huffman@45436
   558
      apply (tactic {* test [@{simproc natdiff_cancel_numerals}] *})?
huffman@45436
   559
      sorry*)
huffman@45436
   560
  }
huffman@45436
   561
end
huffman@45436
   562
huffman@45436
   563
end