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