src/HOL/Integ/nat_simprocs.ML
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 18708 4b3dadb4fe33
parent 18442 b35d7312c64f
child 19233 77ca20b0ed77
permissions -rw-r--r--
setup: theory -> theory;
wenzelm@9436
     1
(*  Title:      HOL/nat_simprocs.ML
wenzelm@9436
     2
    ID:         $Id$
wenzelm@9436
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@9436
     4
    Copyright   2000  University of Cambridge
wenzelm@9436
     5
wenzelm@9436
     6
Simprocs for nat numerals.
wenzelm@9436
     7
*)
wenzelm@9436
     8
paulson@14430
     9
val Let_number_of = thm"Let_number_of";
paulson@14430
    10
val Let_0 = thm"Let_0";
paulson@14430
    11
val Let_1 = thm"Let_1";
paulson@14430
    12
wenzelm@9436
    13
structure Nat_Numeral_Simprocs =
wenzelm@9436
    14
struct
wenzelm@9436
    15
paulson@11868
    16
(*Maps n to #n for n = 0, 1, 2*)
paulson@11868
    17
val numeral_syms =
paulson@14387
    18
       [nat_numeral_0_eq_0 RS sym, nat_numeral_1_eq_1 RS sym, numeral_2_eq_2 RS sym];
paulson@11868
    19
val numeral_sym_ss = HOL_ss addsimps numeral_syms;
paulson@11868
    20
wenzelm@13462
    21
fun rename_numerals th =
paulson@11868
    22
    simplify numeral_sym_ss (Thm.transfer (the_context ()) th);
paulson@11868
    23
wenzelm@9436
    24
(*Utilities*)
wenzelm@9436
    25
nipkow@10693
    26
fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_bin n;
wenzelm@9436
    27
wenzelm@9436
    28
(*Decodes a unary or binary numeral to a NATURAL NUMBER*)
wenzelm@9436
    29
fun dest_numeral (Const ("0", _)) = 0
wenzelm@9436
    30
  | dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t
wenzelm@9436
    31
  | dest_numeral (Const("Numeral.number_of", _) $ w) =
paulson@15965
    32
      (IntInf.max (0, HOLogic.dest_binum w)
wenzelm@10890
    33
       handle TERM _ => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w]))
wenzelm@9436
    34
  | dest_numeral t = raise TERM("Nat_Numeral_Simprocs.dest_numeral:2", [t]);
wenzelm@9436
    35
wenzelm@9436
    36
fun find_first_numeral past (t::terms) =
wenzelm@9436
    37
        ((dest_numeral t, t, rev past @ terms)
wenzelm@9436
    38
         handle TERM _ => find_first_numeral (t::past) terms)
wenzelm@9436
    39
  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
wenzelm@9436
    40
wenzelm@9436
    41
val zero = mk_numeral 0;
wenzelm@9436
    42
val mk_plus = HOLogic.mk_binop "op +";
wenzelm@9436
    43
paulson@11868
    44
(*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
wenzelm@9436
    45
fun mk_sum []        = zero
wenzelm@9436
    46
  | mk_sum [t,u]     = mk_plus (t, u)
wenzelm@9436
    47
  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
wenzelm@9436
    48
wenzelm@9436
    49
(*this version ALWAYS includes a trailing zero*)
paulson@11868
    50
fun long_mk_sum []        = HOLogic.zero
wenzelm@9436
    51
  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
wenzelm@9436
    52
wenzelm@9436
    53
val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
wenzelm@9436
    54
wenzelm@9436
    55
(*extract the outer Sucs from a term and convert them to a binary numeral*)
wenzelm@9436
    56
fun dest_Sucs (k, Const ("Suc", _) $ t) = dest_Sucs (k+1, t)
wenzelm@9436
    57
  | dest_Sucs (0, t) = t
wenzelm@9436
    58
  | dest_Sucs (k, t) = mk_plus (mk_numeral k, t);
wenzelm@9436
    59
wenzelm@9436
    60
fun dest_sum t =
wenzelm@9436
    61
      let val (t,u) = dest_plus t
wenzelm@9436
    62
      in  dest_sum t @ dest_sum u  end
wenzelm@9436
    63
      handle TERM _ => [t];
wenzelm@9436
    64
wenzelm@9436
    65
fun dest_Sucs_sum t = dest_sum (dest_Sucs (0,t));
wenzelm@9436
    66
paulson@11377
    67
paulson@11377
    68
(** Other simproc items **)
paulson@11377
    69
wenzelm@9436
    70
val trans_tac = Int_Numeral_Simprocs.trans_tac;
wenzelm@9436
    71
paulson@14430
    72
val bin_simps =
paulson@14430
    73
     [nat_numeral_0_eq_0 RS sym, nat_numeral_1_eq_1 RS sym,
paulson@14430
    74
      add_nat_number_of, nat_number_of_add_left, 
paulson@14430
    75
      diff_nat_number_of, le_number_of_eq_not_less,
paulson@14430
    76
      mult_nat_number_of, nat_number_of_mult_left, 
paulson@14430
    77
      less_nat_number_of, 
paulson@14430
    78
      Let_number_of, nat_number_of] @
paulson@14430
    79
     bin_arith_simps @ bin_rel_simps;
wenzelm@9436
    80
wenzelm@13462
    81
fun prep_simproc (name, pats, proc) =
wenzelm@13462
    82
  Simplifier.simproc (Theory.sign_of (the_context ())) name pats proc;
wenzelm@9436
    83
wenzelm@9436
    84
wenzelm@9436
    85
(*** CancelNumerals simprocs ***)
wenzelm@9436
    86
wenzelm@9436
    87
val one = mk_numeral 1;
wenzelm@9436
    88
val mk_times = HOLogic.mk_binop "op *";
wenzelm@9436
    89
wenzelm@9436
    90
fun mk_prod [] = one
wenzelm@9436
    91
  | mk_prod [t] = t
wenzelm@9436
    92
  | mk_prod (t :: ts) = if t = one then mk_prod ts
wenzelm@9436
    93
                        else mk_times (t, mk_prod ts);
wenzelm@9436
    94
wenzelm@9436
    95
val dest_times = HOLogic.dest_bin "op *" HOLogic.natT;
wenzelm@9436
    96
wenzelm@9436
    97
fun dest_prod t =
wenzelm@9436
    98
      let val (t,u) = dest_times t
wenzelm@9436
    99
      in  dest_prod t @ dest_prod u  end
wenzelm@9436
   100
      handle TERM _ => [t];
wenzelm@9436
   101
wenzelm@9436
   102
(*DON'T do the obvious simplifications; that would create special cases*)
paulson@9544
   103
fun mk_coeff (k,t) = mk_times (mk_numeral k, t);
wenzelm@9436
   104
paulson@9544
   105
(*Express t as a product of (possibly) a numeral with other factors, sorted*)
wenzelm@9436
   106
fun dest_coeff t =
wenzelm@9436
   107
    let val ts = sort Term.term_ord (dest_prod t)
wenzelm@9436
   108
        val (n, _, ts') = find_first_numeral [] ts
wenzelm@9436
   109
                          handle TERM _ => (1, one, ts)
wenzelm@9436
   110
    in (n, mk_prod ts') end;
wenzelm@9436
   111
wenzelm@9436
   112
(*Find first coefficient-term THAT MATCHES u*)
wenzelm@9436
   113
fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
wenzelm@9436
   114
  | find_first_coeff past u (t::terms) =
wenzelm@9436
   115
        let val (n,u') = dest_coeff t
wenzelm@9436
   116
        in  if u aconv u' then (n, rev past @ terms)
wenzelm@9436
   117
                          else find_first_coeff (t::past) u terms
wenzelm@9436
   118
        end
wenzelm@9436
   119
        handle TERM _ => find_first_coeff (t::past) u terms;
wenzelm@9436
   120
wenzelm@9436
   121
paulson@11868
   122
(*Simplify 1*n and n*1 to n*)
paulson@11868
   123
val add_0s  = map rename_numerals [add_0, add_0_right];
paulson@14267
   124
val mult_1s = map rename_numerals [thm"nat_mult_1", thm"nat_mult_1_right"];
wenzelm@9436
   125
wenzelm@11701
   126
(*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
paulson@12949
   127
paulson@12949
   128
(*And these help the simproc return False when appropriate, which helps
paulson@12949
   129
  the arith prover.*)
wenzelm@13462
   130
val contra_rules = [add_Suc, add_Suc_right, Zero_not_Suc, Suc_not_Zero,
paulson@12949
   131
                    le_0_eq];
paulson@12949
   132
wenzelm@9436
   133
val simplify_meta_eq =
wenzelm@9436
   134
    Int_Numeral_Simprocs.simplify_meta_eq
paulson@14387
   135
        ([nat_numeral_0_eq_0, numeral_1_eq_Suc_0, add_0, add_0_right,
paulson@12949
   136
          mult_0, mult_0_right, mult_1, mult_1_right] @ contra_rules);
wenzelm@9436
   137
paulson@10536
   138
paulson@11377
   139
(** Restricted version of dest_Sucs_sum for nat_combine_numerals:
paulson@11377
   140
    Simprocs never apply unless the original expression contains at least one
paulson@11377
   141
    numeral in a coefficient position.
paulson@11377
   142
**)
paulson@11377
   143
paulson@12196
   144
fun ignore_Sucs (Const ("Suc", _) $ t) = ignore_Sucs t
paulson@12196
   145
  | ignore_Sucs t = t;
paulson@12196
   146
paulson@11377
   147
fun is_numeral (Const("Numeral.number_of", _) $ w) = true
paulson@11377
   148
  | is_numeral _ = false;
paulson@11377
   149
paulson@11377
   150
fun prod_has_numeral t = exists is_numeral (dest_prod t);
paulson@11377
   151
wenzelm@13462
   152
fun restricted_dest_Sucs_sum t =
paulson@12196
   153
    if exists prod_has_numeral (dest_sum (ignore_Sucs t))
paulson@12196
   154
    then dest_Sucs_sum t
paulson@12196
   155
    else raise TERM("Nat_Numeral_Simprocs.restricted_dest_Sucs_sum", [t]);
paulson@11377
   156
paulson@11377
   157
paulson@14474
   158
(*Like HOL_ss but with an ordering that brings numerals to the front
paulson@14474
   159
  under AC-rewriting.*)
paulson@14474
   160
val num_ss = Int_Numeral_Simprocs.num_ss;
paulson@14474
   161
paulson@10704
   162
(*** Applying CancelNumeralsFun ***)
paulson@10536
   163
wenzelm@9436
   164
structure CancelNumeralsCommon =
wenzelm@9436
   165
  struct
paulson@14387
   166
  val mk_sum            = (fn T:typ => mk_sum)
wenzelm@9436
   167
  val dest_sum          = dest_Sucs_sum
wenzelm@9436
   168
  val mk_coeff          = mk_coeff
wenzelm@9436
   169
  val dest_coeff        = dest_coeff
wenzelm@9436
   170
  val find_first_coeff  = find_first_coeff []
wenzelm@16973
   171
  val trans_tac         = fn _ => trans_tac
wenzelm@18328
   172
wenzelm@18328
   173
  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
wenzelm@18328
   174
    [Suc_eq_add_numeral_1_left] @ add_ac
wenzelm@18328
   175
  val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
wenzelm@18328
   176
  fun norm_tac ss = 
wenzelm@18328
   177
    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
wenzelm@18328
   178
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
wenzelm@18328
   179
wenzelm@18328
   180
  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
wenzelm@18328
   181
  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss));
wenzelm@9436
   182
  val simplify_meta_eq  = simplify_meta_eq
wenzelm@9436
   183
  end;
wenzelm@9436
   184
wenzelm@9436
   185
wenzelm@9436
   186
structure EqCancelNumerals = CancelNumeralsFun
wenzelm@9436
   187
 (open CancelNumeralsCommon
wenzelm@13485
   188
  val prove_conv = Bin_Simprocs.prove_conv
wenzelm@9436
   189
  val mk_bal   = HOLogic.mk_eq
wenzelm@9436
   190
  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
wenzelm@9436
   191
  val bal_add1 = nat_eq_add_iff1 RS trans
wenzelm@9436
   192
  val bal_add2 = nat_eq_add_iff2 RS trans
wenzelm@9436
   193
);
wenzelm@9436
   194
wenzelm@9436
   195
structure LessCancelNumerals = CancelNumeralsFun
wenzelm@9436
   196
 (open CancelNumeralsCommon
wenzelm@13485
   197
  val prove_conv = Bin_Simprocs.prove_conv
wenzelm@9436
   198
  val mk_bal   = HOLogic.mk_binrel "op <"
wenzelm@9436
   199
  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
wenzelm@9436
   200
  val bal_add1 = nat_less_add_iff1 RS trans
wenzelm@9436
   201
  val bal_add2 = nat_less_add_iff2 RS trans
wenzelm@9436
   202
);
wenzelm@9436
   203
wenzelm@9436
   204
structure LeCancelNumerals = CancelNumeralsFun
wenzelm@9436
   205
 (open CancelNumeralsCommon
wenzelm@13485
   206
  val prove_conv = Bin_Simprocs.prove_conv
wenzelm@9436
   207
  val mk_bal   = HOLogic.mk_binrel "op <="
wenzelm@9436
   208
  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
wenzelm@9436
   209
  val bal_add1 = nat_le_add_iff1 RS trans
wenzelm@9436
   210
  val bal_add2 = nat_le_add_iff2 RS trans
wenzelm@9436
   211
);
wenzelm@9436
   212
wenzelm@9436
   213
structure DiffCancelNumerals = CancelNumeralsFun
wenzelm@9436
   214
 (open CancelNumeralsCommon
wenzelm@13485
   215
  val prove_conv = Bin_Simprocs.prove_conv
wenzelm@9436
   216
  val mk_bal   = HOLogic.mk_binop "op -"
wenzelm@9436
   217
  val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT
wenzelm@9436
   218
  val bal_add1 = nat_diff_add_eq1 RS trans
wenzelm@9436
   219
  val bal_add2 = nat_diff_add_eq2 RS trans
wenzelm@9436
   220
);
wenzelm@9436
   221
wenzelm@9436
   222
wenzelm@9436
   223
val cancel_numerals =
wenzelm@9436
   224
  map prep_simproc
wenzelm@9436
   225
   [("nateq_cancel_numerals",
wenzelm@13462
   226
     ["(l::nat) + m = n", "(l::nat) = m + n",
wenzelm@13462
   227
      "(l::nat) * m = n", "(l::nat) = m * n",
wenzelm@13462
   228
      "Suc m = n", "m = Suc n"],
wenzelm@9436
   229
     EqCancelNumerals.proc),
wenzelm@9436
   230
    ("natless_cancel_numerals",
wenzelm@13462
   231
     ["(l::nat) + m < n", "(l::nat) < m + n",
wenzelm@13462
   232
      "(l::nat) * m < n", "(l::nat) < m * n",
wenzelm@13462
   233
      "Suc m < n", "m < Suc n"],
wenzelm@9436
   234
     LessCancelNumerals.proc),
wenzelm@9436
   235
    ("natle_cancel_numerals",
wenzelm@13462
   236
     ["(l::nat) + m <= n", "(l::nat) <= m + n",
wenzelm@13462
   237
      "(l::nat) * m <= n", "(l::nat) <= m * n",
wenzelm@13462
   238
      "Suc m <= n", "m <= Suc n"],
wenzelm@9436
   239
     LeCancelNumerals.proc),
wenzelm@9436
   240
    ("natdiff_cancel_numerals",
wenzelm@13462
   241
     ["((l::nat) + m) - n", "(l::nat) - (m + n)",
wenzelm@13462
   242
      "(l::nat) * m - n", "(l::nat) - m * n",
wenzelm@13462
   243
      "Suc m - n", "m - Suc n"],
wenzelm@9436
   244
     DiffCancelNumerals.proc)];
wenzelm@9436
   245
wenzelm@9436
   246
paulson@10704
   247
(*** Applying CombineNumeralsFun ***)
paulson@10536
   248
wenzelm@9436
   249
structure CombineNumeralsData =
wenzelm@9436
   250
  struct
paulson@15965
   251
  val add               = IntInf.+
paulson@14387
   252
  val mk_sum            = (fn T:typ => long_mk_sum)  (*to work for 2*x + 3*x *)
paulson@11377
   253
  val dest_sum          = restricted_dest_Sucs_sum
wenzelm@9436
   254
  val mk_coeff          = mk_coeff
wenzelm@9436
   255
  val dest_coeff        = dest_coeff
wenzelm@9436
   256
  val left_distrib      = left_add_mult_distrib RS trans
wenzelm@13485
   257
  val prove_conv        = Bin_Simprocs.prove_conv_nohyps
wenzelm@16973
   258
  val trans_tac         = fn _ => trans_tac
wenzelm@18328
   259
wenzelm@18328
   260
  val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [Suc_eq_add_numeral_1] @ add_ac
wenzelm@18328
   261
  val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
wenzelm@16973
   262
  fun norm_tac ss =
wenzelm@18328
   263
    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
wenzelm@18328
   264
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
wenzelm@18328
   265
wenzelm@18328
   266
  val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
wenzelm@18328
   267
  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
wenzelm@9436
   268
  val simplify_meta_eq  = simplify_meta_eq
wenzelm@9436
   269
  end;
wenzelm@9436
   270
wenzelm@9436
   271
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
wenzelm@9436
   272
wenzelm@9436
   273
val combine_numerals =
wenzelm@13462
   274
  prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], CombineNumerals.proc);
wenzelm@9436
   275
paulson@10536
   276
paulson@10704
   277
(*** Applying CancelNumeralFactorFun ***)
paulson@10536
   278
paulson@10536
   279
structure CancelNumeralFactorCommon =
paulson@10536
   280
  struct
wenzelm@13462
   281
  val mk_coeff          = mk_coeff
wenzelm@13462
   282
  val dest_coeff        = dest_coeff
wenzelm@16973
   283
  val trans_tac         = fn _ => trans_tac
wenzelm@18328
   284
wenzelm@18328
   285
  val norm_ss1 = num_ss addsimps
wenzelm@18328
   286
    numeral_syms @ add_0s @ mult_1s @ [Suc_eq_add_numeral_1_left] @ add_ac
wenzelm@18328
   287
  val norm_ss2 = num_ss addsimps bin_simps @ add_ac @ mult_ac
wenzelm@16973
   288
  fun norm_tac ss =
wenzelm@18328
   289
    ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
wenzelm@18328
   290
    THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
wenzelm@18328
   291
wenzelm@18328
   292
  val numeral_simp_ss = HOL_ss addsimps bin_simps
wenzelm@18328
   293
  fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
paulson@10536
   294
  val simplify_meta_eq  = simplify_meta_eq
paulson@10536
   295
  end
paulson@10536
   296
paulson@10536
   297
structure DivCancelNumeralFactor = CancelNumeralFactorFun
paulson@10536
   298
 (open CancelNumeralFactorCommon
wenzelm@13485
   299
  val prove_conv = Bin_Simprocs.prove_conv
paulson@10536
   300
  val mk_bal   = HOLogic.mk_binop "Divides.op div"
paulson@10536
   301
  val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT
paulson@10536
   302
  val cancel = nat_mult_div_cancel1 RS trans
paulson@10536
   303
  val neg_exchanges = false
paulson@10536
   304
)
paulson@10536
   305
paulson@10536
   306
structure EqCancelNumeralFactor = CancelNumeralFactorFun
paulson@10536
   307
 (open CancelNumeralFactorCommon
wenzelm@13485
   308
  val prove_conv = Bin_Simprocs.prove_conv
paulson@10536
   309
  val mk_bal   = HOLogic.mk_eq
paulson@10536
   310
  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
paulson@10536
   311
  val cancel = nat_mult_eq_cancel1 RS trans
paulson@10536
   312
  val neg_exchanges = false
paulson@10536
   313
)
paulson@10536
   314
paulson@10536
   315
structure LessCancelNumeralFactor = CancelNumeralFactorFun
paulson@10536
   316
 (open CancelNumeralFactorCommon
wenzelm@13485
   317
  val prove_conv = Bin_Simprocs.prove_conv
paulson@10536
   318
  val mk_bal   = HOLogic.mk_binrel "op <"
paulson@10536
   319
  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
paulson@10536
   320
  val cancel = nat_mult_less_cancel1 RS trans
paulson@10536
   321
  val neg_exchanges = true
paulson@10536
   322
)
paulson@10536
   323
paulson@10536
   324
structure LeCancelNumeralFactor = CancelNumeralFactorFun
paulson@10536
   325
 (open CancelNumeralFactorCommon
wenzelm@13485
   326
  val prove_conv = Bin_Simprocs.prove_conv
paulson@10536
   327
  val mk_bal   = HOLogic.mk_binrel "op <="
paulson@10536
   328
  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
paulson@10536
   329
  val cancel = nat_mult_le_cancel1 RS trans
paulson@10536
   330
  val neg_exchanges = true
paulson@10536
   331
)
paulson@10536
   332
wenzelm@13462
   333
val cancel_numeral_factors =
paulson@10536
   334
  map prep_simproc
paulson@10536
   335
   [("nateq_cancel_numeral_factors",
wenzelm@13462
   336
     ["(l::nat) * m = n", "(l::nat) = m * n"],
paulson@10536
   337
     EqCancelNumeralFactor.proc),
wenzelm@13462
   338
    ("natless_cancel_numeral_factors",
wenzelm@13462
   339
     ["(l::nat) * m < n", "(l::nat) < m * n"],
paulson@10536
   340
     LessCancelNumeralFactor.proc),
wenzelm@13462
   341
    ("natle_cancel_numeral_factors",
wenzelm@13462
   342
     ["(l::nat) * m <= n", "(l::nat) <= m * n"],
paulson@10536
   343
     LeCancelNumeralFactor.proc),
wenzelm@13462
   344
    ("natdiv_cancel_numeral_factors",
wenzelm@13462
   345
     ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
paulson@10536
   346
     DivCancelNumeralFactor.proc)];
paulson@10536
   347
paulson@10704
   348
paulson@10704
   349
paulson@10704
   350
(*** Applying ExtractCommonTermFun ***)
paulson@10704
   351
paulson@10704
   352
(*this version ALWAYS includes a trailing one*)
paulson@10704
   353
fun long_mk_prod []        = one
paulson@10704
   354
  | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
paulson@10704
   355
paulson@10704
   356
(*Find first term that matches u*)
haftmann@18442
   357
fun find_first_t past u []         = raise TERM("find_first_t", [])
haftmann@18442
   358
  | find_first_t past u (t::terms) =
wenzelm@13462
   359
        if u aconv t then (rev past @ terms)
haftmann@18442
   360
        else find_first_t (t::past) u terms
haftmann@18442
   361
        handle TERM _ => find_first_t (t::past) u terms;
paulson@10704
   362
paulson@15271
   363
(** Final simplification for the CancelFactor simprocs **)
paulson@15271
   364
val simplify_one = 
paulson@15271
   365
    Int_Numeral_Simprocs.simplify_meta_eq  
paulson@15271
   366
       [mult_1_left, mult_1_right, div_1, numeral_1_eq_Suc_0];
paulson@15271
   367
wenzelm@16973
   368
fun cancel_simplify_meta_eq cancel_th ss th =
wenzelm@16973
   369
    simplify_one ss (([th, cancel_th]) MRS trans);
paulson@10704
   370
paulson@10704
   371
structure CancelFactorCommon =
paulson@10704
   372
  struct
paulson@14387
   373
  val mk_sum            = (fn T:typ => long_mk_prod)
wenzelm@13462
   374
  val dest_sum          = dest_prod
wenzelm@13462
   375
  val mk_coeff          = mk_coeff
wenzelm@13462
   376
  val dest_coeff        = dest_coeff
haftmann@18442
   377
  val find_first        = find_first_t []
wenzelm@16973
   378
  val trans_tac         = fn _ => trans_tac
wenzelm@18328
   379
  val norm_ss = HOL_ss addsimps mult_1s @ mult_ac
wenzelm@18328
   380
  fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
paulson@10704
   381
  end;
paulson@10704
   382
paulson@10704
   383
structure EqCancelFactor = ExtractCommonTermFun
paulson@10704
   384
 (open CancelFactorCommon
wenzelm@13485
   385
  val prove_conv = Bin_Simprocs.prove_conv
paulson@10704
   386
  val mk_bal   = HOLogic.mk_eq
paulson@10704
   387
  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
paulson@10704
   388
  val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_eq_cancel_disj
paulson@10704
   389
);
paulson@10704
   390
paulson@10704
   391
structure LessCancelFactor = ExtractCommonTermFun
paulson@10704
   392
 (open CancelFactorCommon
wenzelm@13485
   393
  val prove_conv = Bin_Simprocs.prove_conv
paulson@10704
   394
  val mk_bal   = HOLogic.mk_binrel "op <"
paulson@10704
   395
  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
paulson@10704
   396
  val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_less_cancel_disj
paulson@10704
   397
);
paulson@10704
   398
paulson@10704
   399
structure LeCancelFactor = ExtractCommonTermFun
paulson@10704
   400
 (open CancelFactorCommon
wenzelm@13485
   401
  val prove_conv = Bin_Simprocs.prove_conv
paulson@10704
   402
  val mk_bal   = HOLogic.mk_binrel "op <="
paulson@10704
   403
  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
paulson@10704
   404
  val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_le_cancel_disj
paulson@10704
   405
);
paulson@10704
   406
paulson@10704
   407
structure DivideCancelFactor = ExtractCommonTermFun
paulson@10704
   408
 (open CancelFactorCommon
wenzelm@13485
   409
  val prove_conv = Bin_Simprocs.prove_conv
paulson@10704
   410
  val mk_bal   = HOLogic.mk_binop "Divides.op div"
paulson@10704
   411
  val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT
paulson@10704
   412
  val simplify_meta_eq  = cancel_simplify_meta_eq nat_mult_div_cancel_disj
paulson@10704
   413
);
paulson@10704
   414
wenzelm@13462
   415
val cancel_factor =
paulson@10704
   416
  map prep_simproc
paulson@10704
   417
   [("nat_eq_cancel_factor",
wenzelm@13462
   418
     ["(l::nat) * m = n", "(l::nat) = m * n"],
paulson@10704
   419
     EqCancelFactor.proc),
paulson@10704
   420
    ("nat_less_cancel_factor",
wenzelm@13462
   421
     ["(l::nat) * m < n", "(l::nat) < m * n"],
paulson@10704
   422
     LessCancelFactor.proc),
paulson@10704
   423
    ("nat_le_cancel_factor",
wenzelm@13462
   424
     ["(l::nat) * m <= n", "(l::nat) <= m * n"],
paulson@10704
   425
     LeCancelFactor.proc),
wenzelm@13462
   426
    ("nat_divide_cancel_factor",
wenzelm@13462
   427
     ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
paulson@10704
   428
     DivideCancelFactor.proc)];
paulson@10704
   429
wenzelm@9436
   430
end;
wenzelm@9436
   431
wenzelm@9436
   432
wenzelm@9436
   433
Addsimprocs Nat_Numeral_Simprocs.cancel_numerals;
wenzelm@9436
   434
Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
paulson@10536
   435
Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors;
paulson@10704
   436
Addsimprocs Nat_Numeral_Simprocs.cancel_factor;
wenzelm@9436
   437
wenzelm@9436
   438
wenzelm@9436
   439
(*examples:
wenzelm@9436
   440
print_depth 22;
wenzelm@9436
   441
set timing;
wenzelm@9436
   442
set trace_simp;
wenzelm@9436
   443
fun test s = (Goal s; by (Simp_tac 1));
wenzelm@9436
   444
wenzelm@9436
   445
(*cancel_numerals*)
wenzelm@11704
   446
test "l +( 2) + (2) + 2 + (l + 2) + (oo  + 2) = (uu::nat)";
wenzelm@11704
   447
test "(2*length xs < 2*length xs + j)";
wenzelm@11704
   448
test "(2*length xs < length xs * 2 + j)";
wenzelm@11704
   449
test "2*u = (u::nat)";
wenzelm@11704
   450
test "2*u = Suc (u)";
wenzelm@11704
   451
test "(i + j + 12 + (k::nat)) - 15 = y";
wenzelm@11704
   452
test "(i + j + 12 + (k::nat)) - 5 = y";
wenzelm@11704
   453
test "Suc u - 2 = y";
wenzelm@11704
   454
test "Suc (Suc (Suc u)) - 2 = y";
wenzelm@11704
   455
test "(i + j + 2 + (k::nat)) - 1 = y";
paulson@11868
   456
test "(i + j + 1 + (k::nat)) - 2 = y";
wenzelm@9436
   457
wenzelm@11704
   458
test "(2*x + (u*v) + y) - v*3*u = (w::nat)";
wenzelm@11704
   459
test "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = (w::nat)";
wenzelm@11704
   460
test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::nat)";
wenzelm@11704
   461
test "Suc (Suc (2*x*u*v + u*4 + y)) - u = w";
wenzelm@11704
   462
test "Suc ((u*v)*4) - v*3*u = w";
wenzelm@11704
   463
test "Suc (Suc ((u*v)*3)) - v*3*u = w";
wenzelm@9436
   464
wenzelm@11704
   465
test "(i + j + 12 + (k::nat)) = u + 15 + y";
wenzelm@11704
   466
test "(i + j + 32 + (k::nat)) - (u + 15 + y) = zz";
wenzelm@11704
   467
test "(i + j + 12 + (k::nat)) = u + 5 + y";
wenzelm@9436
   468
(*Suc*)
wenzelm@11704
   469
test "(i + j + 12 + k) = Suc (u + y)";
wenzelm@11704
   470
test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + 41 + k)";
wenzelm@11704
   471
test "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
wenzelm@11704
   472
test "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v";
wenzelm@11704
   473
test "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
wenzelm@11704
   474
test "2*y + 3*z + 2*u = Suc (u)";
wenzelm@11704
   475
test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)";
wenzelm@11704
   476
test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::nat)";
wenzelm@11704
   477
test "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)";
wenzelm@11704
   478
test "(2*n*m) < (3*(m*n)) + (u::nat)";
wenzelm@9436
   479
paulson@14474
   480
test "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0 | Suc k => k)))))) <= Suc 0)";
paulson@14474
   481
 
paulson@14474
   482
test "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) <= length l1";
paulson@14474
   483
paulson@14474
   484
test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length l3)))))) <= length (compT P E A ST mxr e))";
paulson@14474
   485
paulson@14474
   486
test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length (compT P E (A Un \<A> e) ST mxr c))))))) <= length (compT P E A ST mxr e))";
paulson@14474
   487
paulson@14474
   488
wenzelm@9436
   489
(*negative numerals: FAIL*)
wenzelm@11704
   490
test "(i + j + -23 + (k::nat)) < u + 15 + y";
wenzelm@11704
   491
test "(i + j + 3 + (k::nat)) < u + -15 + y";
wenzelm@11704
   492
test "(i + j + -12 + (k::nat)) - 15 = y";
wenzelm@11704
   493
test "(i + j + 12 + (k::nat)) - -15 = y";
wenzelm@11704
   494
test "(i + j + -12 + (k::nat)) - -15 = y";
wenzelm@9436
   495
wenzelm@9436
   496
(*combine_numerals*)
wenzelm@11704
   497
test "k + 3*k = (u::nat)";
wenzelm@11704
   498
test "Suc (i + 3) = u";
wenzelm@11704
   499
test "Suc (i + j + 3 + k) = u";
wenzelm@11704
   500
test "k + j + 3*k + j = (u::nat)";
wenzelm@11704
   501
test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)";
wenzelm@11704
   502
test "(2*n*m) + (3*(m*n)) = (u::nat)";
wenzelm@9436
   503
(*negative numerals: FAIL*)
wenzelm@11704
   504
test "Suc (i + j + -3 + k) = u";
paulson@10536
   505
paulson@10704
   506
(*cancel_numeral_factors*)
wenzelm@11704
   507
test "9*x = 12 * (y::nat)";
wenzelm@11704
   508
test "(9*x) div (12 * (y::nat)) = z";
wenzelm@11704
   509
test "9*x < 12 * (y::nat)";
wenzelm@11704
   510
test "9*x <= 12 * (y::nat)";
paulson@10704
   511
paulson@10704
   512
(*cancel_factor*)
paulson@10704
   513
test "x*k = k*(y::nat)";
wenzelm@13462
   514
test "k = k*(y::nat)";
paulson@10704
   515
test "a*(b*c) = (b::nat)";
paulson@10704
   516
test "a*(b*c) = d*(b::nat)*(x*a)";
paulson@10704
   517
paulson@10704
   518
test "x*k < k*(y::nat)";
wenzelm@13462
   519
test "k < k*(y::nat)";
paulson@10704
   520
test "a*(b*c) < (b::nat)";
paulson@10704
   521
test "a*(b*c) < d*(b::nat)*(x*a)";
paulson@10704
   522
paulson@10704
   523
test "x*k <= k*(y::nat)";
wenzelm@13462
   524
test "k <= k*(y::nat)";
paulson@10704
   525
test "a*(b*c) <= (b::nat)";
paulson@10704
   526
test "a*(b*c) <= d*(b::nat)*(x*a)";
paulson@10704
   527
paulson@10704
   528
test "(x*k) div (k*(y::nat)) = (uu::nat)";
wenzelm@13462
   529
test "(k) div (k*(y::nat)) = (uu::nat)";
paulson@10704
   530
test "(a*(b*c)) div ((b::nat)) = (uu::nat)";
paulson@10704
   531
test "(a*(b*c)) div (d*(b::nat)*(x*a)) = (uu::nat)";
wenzelm@9436
   532
*)
wenzelm@9436
   533
wenzelm@9436
   534
wenzelm@9436
   535
(*** Prepare linear arithmetic for nat numerals ***)
wenzelm@9436
   536
wenzelm@9436
   537
local
wenzelm@9436
   538
wenzelm@9436
   539
(* reduce contradictory <= to False *)
wenzelm@9436
   540
val add_rules =
paulson@14430
   541
  [thm "Let_number_of", Let_0, Let_1, nat_0, nat_1,
paulson@11868
   542
   add_nat_number_of, diff_nat_number_of, mult_nat_number_of,
paulson@14365
   543
   eq_nat_number_of, less_nat_number_of, le_number_of_eq_not_less,
nipkow@11296
   544
   le_Suc_number_of,le_number_of_Suc,
wenzelm@9436
   545
   less_Suc_number_of,less_number_of_Suc,
nipkow@11296
   546
   Suc_eq_number_of,eq_number_of_Suc,
paulson@14369
   547
   mult_Suc, mult_Suc_right,
wenzelm@9436
   548
   eq_number_of_0, eq_0_number_of, less_0_number_of,
paulson@14390
   549
   of_int_number_of_eq, of_nat_number_of_eq, nat_number_of, if_True, if_False];
wenzelm@9436
   550
paulson@14387
   551
val simprocs = [Nat_Numeral_Simprocs.combine_numerals]@
wenzelm@9436
   552
                Nat_Numeral_Simprocs.cancel_numerals;
wenzelm@9436
   553
wenzelm@9436
   554
in
wenzelm@9436
   555
wenzelm@9436
   556
val nat_simprocs_setup =
wenzelm@18708
   557
  Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
nipkow@10693
   558
   {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
nipkow@15921
   559
    inj_thms = inj_thms, lessD = lessD, neqE = neqE,
wenzelm@9436
   560
    simpset = simpset addsimps add_rules
wenzelm@18708
   561
                      addsimprocs simprocs});
wenzelm@9436
   562
wenzelm@9436
   563
end;