src/HOL/Integ/nat_simprocs.ML
author nipkow
Fri Dec 01 19:53:29 2000 +0100 (2000-12-01)
changeset 10574 8f98f0301d67
parent 10536 8f34ecae1446
child 10693 9e4a0e84d0d6
permissions -rw-r--r--
Linear arithmetic now copes with mixed nat/int formulae.
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
wenzelm@9436
     9
Goal "number_of v + (number_of v' + (k::nat)) = \
wenzelm@9436
    10
\        (if neg (number_of v) then number_of v' + k \
wenzelm@9436
    11
\         else if neg (number_of v') then number_of v + k \
wenzelm@9436
    12
\         else number_of (bin_add v v') + k)";
wenzelm@9436
    13
by (Simp_tac 1);
wenzelm@9436
    14
qed "nat_number_of_add_left";
wenzelm@9436
    15
wenzelm@9436
    16
wenzelm@9436
    17
(** For combine_numerals **)
wenzelm@9436
    18
wenzelm@9436
    19
Goal "i*u + (j*u + k) = (i+j)*u + (k::nat)";
wenzelm@9436
    20
by (asm_simp_tac (simpset() addsimps [add_mult_distrib]) 1);
wenzelm@9436
    21
qed "left_add_mult_distrib";
wenzelm@9436
    22
wenzelm@9436
    23
wenzelm@9436
    24
(** For cancel_numerals **)
wenzelm@9436
    25
wenzelm@9436
    26
Goal "j <= (i::nat) ==> ((i*u + m) - (j*u + n)) = (((i-j)*u + m) - n)";
wenzelm@9436
    27
by (asm_simp_tac (simpset() addsplits [nat_diff_split]
wenzelm@9436
    28
                            addsimps [add_mult_distrib]) 1);
wenzelm@9436
    29
qed "nat_diff_add_eq1";
wenzelm@9436
    30
wenzelm@9436
    31
Goal "i <= (j::nat) ==> ((i*u + m) - (j*u + n)) = (m - ((j-i)*u + n))";
wenzelm@9436
    32
by (asm_simp_tac (simpset() addsplits [nat_diff_split]
wenzelm@9436
    33
                            addsimps [add_mult_distrib]) 1);
wenzelm@9436
    34
qed "nat_diff_add_eq2";
wenzelm@9436
    35
wenzelm@9436
    36
Goal "j <= (i::nat) ==> (i*u + m = j*u + n) = ((i-j)*u + m = n)";
wenzelm@9436
    37
by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
wenzelm@9436
    38
                                  addsimps [add_mult_distrib]));
wenzelm@9436
    39
qed "nat_eq_add_iff1";
wenzelm@9436
    40
wenzelm@9436
    41
Goal "i <= (j::nat) ==> (i*u + m = j*u + n) = (m = (j-i)*u + n)";
wenzelm@9436
    42
by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
wenzelm@9436
    43
                                  addsimps [add_mult_distrib]));
wenzelm@9436
    44
qed "nat_eq_add_iff2";
wenzelm@9436
    45
wenzelm@9436
    46
Goal "j <= (i::nat) ==> (i*u + m < j*u + n) = ((i-j)*u + m < n)";
wenzelm@9436
    47
by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
wenzelm@9436
    48
                                  addsimps [add_mult_distrib]));
wenzelm@9436
    49
qed "nat_less_add_iff1";
wenzelm@9436
    50
wenzelm@9436
    51
Goal "i <= (j::nat) ==> (i*u + m < j*u + n) = (m < (j-i)*u + n)";
wenzelm@9436
    52
by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
wenzelm@9436
    53
                                  addsimps [add_mult_distrib]));
wenzelm@9436
    54
qed "nat_less_add_iff2";
wenzelm@9436
    55
wenzelm@9436
    56
Goal "j <= (i::nat) ==> (i*u + m <= j*u + n) = ((i-j)*u + m <= n)";
wenzelm@9436
    57
by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
wenzelm@9436
    58
                                  addsimps [add_mult_distrib]));
wenzelm@9436
    59
qed "nat_le_add_iff1";
wenzelm@9436
    60
wenzelm@9436
    61
Goal "i <= (j::nat) ==> (i*u + m <= j*u + n) = (m <= (j-i)*u + n)";
wenzelm@9436
    62
by (auto_tac (claset(), simpset() addsplits [nat_diff_split]
wenzelm@9436
    63
                                  addsimps [add_mult_distrib]));
wenzelm@9436
    64
qed "nat_le_add_iff2";
wenzelm@9436
    65
wenzelm@9436
    66
paulson@10536
    67
(** For cancel_numeral_factors **)
paulson@10536
    68
paulson@10536
    69
Goal "(#0::nat) < k ==> (k*m <= k*n) = (m<=n)";
paulson@10536
    70
by Auto_tac;  
paulson@10536
    71
qed "nat_mult_le_cancel1";
paulson@10536
    72
paulson@10536
    73
Goal "(#0::nat) < k ==> (k*m < k*n) = (m<n)";
paulson@10536
    74
by Auto_tac;  
paulson@10536
    75
qed "nat_mult_less_cancel1";
paulson@10536
    76
paulson@10536
    77
Goal "(#0::nat) < k ==> (k*m = k*n) = (m=n)";
paulson@10536
    78
by Auto_tac;  
paulson@10536
    79
qed "nat_mult_eq_cancel1";
paulson@10536
    80
paulson@10536
    81
Goal "(#0::nat) < k ==> (k*m) div (k*n) = (m div n)";
paulson@10536
    82
by Auto_tac;  
paulson@10536
    83
qed "nat_mult_div_cancel1";
paulson@10536
    84
paulson@10536
    85
wenzelm@9436
    86
structure Nat_Numeral_Simprocs =
wenzelm@9436
    87
struct
wenzelm@9436
    88
wenzelm@9436
    89
(*Utilities*)
wenzelm@9436
    90
wenzelm@9436
    91
fun mk_numeral n = HOLogic.number_of_const HOLogic.natT $
wenzelm@9436
    92
                   NumeralSyntax.mk_bin n;
wenzelm@9436
    93
wenzelm@9436
    94
(*Decodes a unary or binary numeral to a NATURAL NUMBER*)
wenzelm@9436
    95
fun dest_numeral (Const ("0", _)) = 0
wenzelm@9436
    96
  | dest_numeral (Const ("Suc", _) $ t) = 1 + dest_numeral t
wenzelm@9436
    97
  | dest_numeral (Const("Numeral.number_of", _) $ w) =
wenzelm@9436
    98
      (BasisLibrary.Int.max (0, NumeralSyntax.dest_bin w)
wenzelm@9436
    99
       handle Match => raise TERM("Nat_Numeral_Simprocs.dest_numeral:1", [w]))
wenzelm@9436
   100
  | dest_numeral t = raise TERM("Nat_Numeral_Simprocs.dest_numeral:2", [t]);
wenzelm@9436
   101
wenzelm@9436
   102
fun find_first_numeral past (t::terms) =
wenzelm@9436
   103
        ((dest_numeral t, t, rev past @ terms)
wenzelm@9436
   104
         handle TERM _ => find_first_numeral (t::past) terms)
wenzelm@9436
   105
  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
wenzelm@9436
   106
wenzelm@9436
   107
val zero = mk_numeral 0;
wenzelm@9436
   108
val mk_plus = HOLogic.mk_binop "op +";
wenzelm@9436
   109
wenzelm@9436
   110
(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
wenzelm@9436
   111
fun mk_sum []        = zero
wenzelm@9436
   112
  | mk_sum [t,u]     = mk_plus (t, u)
wenzelm@9436
   113
  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
wenzelm@9436
   114
wenzelm@9436
   115
(*this version ALWAYS includes a trailing zero*)
wenzelm@9436
   116
fun long_mk_sum []        = zero
wenzelm@9436
   117
  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
wenzelm@9436
   118
wenzelm@9436
   119
val dest_plus = HOLogic.dest_bin "op +" HOLogic.natT;
wenzelm@9436
   120
wenzelm@9436
   121
(*extract the outer Sucs from a term and convert them to a binary numeral*)
wenzelm@9436
   122
fun dest_Sucs (k, Const ("Suc", _) $ t) = dest_Sucs (k+1, t)
wenzelm@9436
   123
  | dest_Sucs (0, t) = t
wenzelm@9436
   124
  | dest_Sucs (k, t) = mk_plus (mk_numeral k, t);
wenzelm@9436
   125
wenzelm@9436
   126
fun dest_sum t =
wenzelm@9436
   127
      let val (t,u) = dest_plus t
wenzelm@9436
   128
      in  dest_sum t @ dest_sum u  end
wenzelm@9436
   129
      handle TERM _ => [t];
wenzelm@9436
   130
wenzelm@9436
   131
fun dest_Sucs_sum t = dest_sum (dest_Sucs (0,t));
wenzelm@9436
   132
wenzelm@9436
   133
val trans_tac = Int_Numeral_Simprocs.trans_tac;
wenzelm@9436
   134
wenzelm@9436
   135
val prove_conv = Int_Numeral_Simprocs.prove_conv;
wenzelm@9436
   136
wenzelm@9436
   137
val bin_simps = [add_nat_number_of, nat_number_of_add_left,
wenzelm@9436
   138
                 diff_nat_number_of, le_nat_number_of_eq_not_less,
paulson@10536
   139
                 less_nat_number_of, mult_nat_number_of, 
paulson@10536
   140
                 Let_number_of, nat_number_of] @
wenzelm@9436
   141
                bin_arith_simps @ bin_rel_simps;
wenzelm@9436
   142
wenzelm@9436
   143
fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
wenzelm@9436
   144
fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ())) (s, HOLogic.termT);
wenzelm@9436
   145
val prep_pats = map prep_pat;
wenzelm@9436
   146
wenzelm@9436
   147
wenzelm@9436
   148
(*** CancelNumerals simprocs ***)
wenzelm@9436
   149
wenzelm@9436
   150
val one = mk_numeral 1;
wenzelm@9436
   151
val mk_times = HOLogic.mk_binop "op *";
wenzelm@9436
   152
wenzelm@9436
   153
fun mk_prod [] = one
wenzelm@9436
   154
  | mk_prod [t] = t
wenzelm@9436
   155
  | mk_prod (t :: ts) = if t = one then mk_prod ts
wenzelm@9436
   156
                        else mk_times (t, mk_prod ts);
wenzelm@9436
   157
wenzelm@9436
   158
val dest_times = HOLogic.dest_bin "op *" HOLogic.natT;
wenzelm@9436
   159
wenzelm@9436
   160
fun dest_prod t =
wenzelm@9436
   161
      let val (t,u) = dest_times t
wenzelm@9436
   162
      in  dest_prod t @ dest_prod u  end
wenzelm@9436
   163
      handle TERM _ => [t];
wenzelm@9436
   164
wenzelm@9436
   165
(*DON'T do the obvious simplifications; that would create special cases*)
paulson@9544
   166
fun mk_coeff (k,t) = mk_times (mk_numeral k, t);
wenzelm@9436
   167
paulson@9544
   168
(*Express t as a product of (possibly) a numeral with other factors, sorted*)
wenzelm@9436
   169
fun dest_coeff t =
wenzelm@9436
   170
    let val ts = sort Term.term_ord (dest_prod t)
wenzelm@9436
   171
        val (n, _, ts') = find_first_numeral [] ts
wenzelm@9436
   172
                          handle TERM _ => (1, one, ts)
wenzelm@9436
   173
    in (n, mk_prod ts') end;
wenzelm@9436
   174
wenzelm@9436
   175
(*Find first coefficient-term THAT MATCHES u*)
wenzelm@9436
   176
fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
wenzelm@9436
   177
  | find_first_coeff past u (t::terms) =
wenzelm@9436
   178
        let val (n,u') = dest_coeff t
wenzelm@9436
   179
        in  if u aconv u' then (n, rev past @ terms)
wenzelm@9436
   180
                          else find_first_coeff (t::past) u terms
wenzelm@9436
   181
        end
wenzelm@9436
   182
        handle TERM _ => find_first_coeff (t::past) u terms;
wenzelm@9436
   183
wenzelm@9436
   184
wenzelm@9436
   185
(*Simplify #1*n and n*#1 to n*)
wenzelm@9436
   186
val add_0s = map rename_numerals [add_0, add_0_right];
wenzelm@9436
   187
val mult_1s = map rename_numerals [mult_1, mult_1_right];
wenzelm@9436
   188
wenzelm@9436
   189
(*Final simplification: cancel + and *; replace #0 by 0 and #1 by 1*)
wenzelm@9436
   190
val simplify_meta_eq =
wenzelm@9436
   191
    Int_Numeral_Simprocs.simplify_meta_eq
wenzelm@9436
   192
         [numeral_0_eq_0, numeral_1_eq_1, add_0, add_0_right,
wenzelm@9436
   193
         mult_0, mult_0_right, mult_1, mult_1_right];
wenzelm@9436
   194
paulson@10536
   195
paulson@10536
   196
(*** Instantiating CancelNumeralsFun ***)
paulson@10536
   197
wenzelm@9436
   198
structure CancelNumeralsCommon =
wenzelm@9436
   199
  struct
wenzelm@9436
   200
  val mk_sum            = mk_sum
wenzelm@9436
   201
  val dest_sum          = dest_Sucs_sum
wenzelm@9436
   202
  val mk_coeff          = mk_coeff
wenzelm@9436
   203
  val dest_coeff        = dest_coeff
wenzelm@9436
   204
  val find_first_coeff  = find_first_coeff []
wenzelm@9436
   205
  val trans_tac          = trans_tac
wenzelm@9436
   206
  val norm_tac = ALLGOALS
wenzelm@9436
   207
                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@
wenzelm@9436
   208
                                       [add_0, Suc_eq_add_numeral_1]@add_ac))
wenzelm@9436
   209
                 THEN ALLGOALS (simp_tac
wenzelm@9436
   210
                                (HOL_ss addsimps bin_simps@add_ac@mult_ac))
wenzelm@9436
   211
  val numeral_simp_tac  = ALLGOALS
wenzelm@9436
   212
                (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
wenzelm@9436
   213
  val simplify_meta_eq  = simplify_meta_eq
wenzelm@9436
   214
  end;
wenzelm@9436
   215
wenzelm@9436
   216
wenzelm@9436
   217
structure EqCancelNumerals = CancelNumeralsFun
wenzelm@9436
   218
 (open CancelNumeralsCommon
wenzelm@9436
   219
  val prove_conv = prove_conv "nateq_cancel_numerals"
wenzelm@9436
   220
  val mk_bal   = HOLogic.mk_eq
wenzelm@9436
   221
  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
wenzelm@9436
   222
  val bal_add1 = nat_eq_add_iff1 RS trans
wenzelm@9436
   223
  val bal_add2 = nat_eq_add_iff2 RS trans
wenzelm@9436
   224
);
wenzelm@9436
   225
wenzelm@9436
   226
structure LessCancelNumerals = CancelNumeralsFun
wenzelm@9436
   227
 (open CancelNumeralsCommon
wenzelm@9436
   228
  val prove_conv = prove_conv "natless_cancel_numerals"
wenzelm@9436
   229
  val mk_bal   = HOLogic.mk_binrel "op <"
wenzelm@9436
   230
  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
wenzelm@9436
   231
  val bal_add1 = nat_less_add_iff1 RS trans
wenzelm@9436
   232
  val bal_add2 = nat_less_add_iff2 RS trans
wenzelm@9436
   233
);
wenzelm@9436
   234
wenzelm@9436
   235
structure LeCancelNumerals = CancelNumeralsFun
wenzelm@9436
   236
 (open CancelNumeralsCommon
wenzelm@9436
   237
  val prove_conv = prove_conv "natle_cancel_numerals"
wenzelm@9436
   238
  val mk_bal   = HOLogic.mk_binrel "op <="
wenzelm@9436
   239
  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
wenzelm@9436
   240
  val bal_add1 = nat_le_add_iff1 RS trans
wenzelm@9436
   241
  val bal_add2 = nat_le_add_iff2 RS trans
wenzelm@9436
   242
);
wenzelm@9436
   243
wenzelm@9436
   244
structure DiffCancelNumerals = CancelNumeralsFun
wenzelm@9436
   245
 (open CancelNumeralsCommon
wenzelm@9436
   246
  val prove_conv = prove_conv "natdiff_cancel_numerals"
wenzelm@9436
   247
  val mk_bal   = HOLogic.mk_binop "op -"
wenzelm@9436
   248
  val dest_bal = HOLogic.dest_bin "op -" HOLogic.natT
wenzelm@9436
   249
  val bal_add1 = nat_diff_add_eq1 RS trans
wenzelm@9436
   250
  val bal_add2 = nat_diff_add_eq2 RS trans
wenzelm@9436
   251
);
wenzelm@9436
   252
wenzelm@9436
   253
wenzelm@9436
   254
val cancel_numerals =
wenzelm@9436
   255
  map prep_simproc
wenzelm@9436
   256
   [("nateq_cancel_numerals",
wenzelm@9436
   257
     prep_pats ["(l::nat) + m = n", "(l::nat) = m + n",
wenzelm@9436
   258
                "(l::nat) * m = n", "(l::nat) = m * n",
wenzelm@9436
   259
                "Suc m = n", "m = Suc n"],
wenzelm@9436
   260
     EqCancelNumerals.proc),
wenzelm@9436
   261
    ("natless_cancel_numerals",
wenzelm@9436
   262
     prep_pats ["(l::nat) + m < n", "(l::nat) < m + n",
wenzelm@9436
   263
                "(l::nat) * m < n", "(l::nat) < m * n",
wenzelm@9436
   264
                "Suc m < n", "m < Suc n"],
wenzelm@9436
   265
     LessCancelNumerals.proc),
wenzelm@9436
   266
    ("natle_cancel_numerals",
wenzelm@9436
   267
     prep_pats ["(l::nat) + m <= n", "(l::nat) <= m + n",
wenzelm@9436
   268
                "(l::nat) * m <= n", "(l::nat) <= m * n",
wenzelm@9436
   269
                "Suc m <= n", "m <= Suc n"],
wenzelm@9436
   270
     LeCancelNumerals.proc),
wenzelm@9436
   271
    ("natdiff_cancel_numerals",
wenzelm@9436
   272
     prep_pats ["((l::nat) + m) - n", "(l::nat) - (m + n)",
wenzelm@9436
   273
                "(l::nat) * m - n", "(l::nat) - m * n",
wenzelm@9436
   274
                "Suc m - n", "m - Suc n"],
wenzelm@9436
   275
     DiffCancelNumerals.proc)];
wenzelm@9436
   276
wenzelm@9436
   277
paulson@10536
   278
(*** Instantiating CombineNumeralsFun ***)
paulson@10536
   279
wenzelm@9436
   280
structure CombineNumeralsData =
wenzelm@9436
   281
  struct
paulson@9571
   282
  val add		= op + : int*int -> int 
wenzelm@9436
   283
  val mk_sum            = long_mk_sum    (*to work for e.g. #2*x + #3*x *)
wenzelm@9436
   284
  val dest_sum          = dest_Sucs_sum
wenzelm@9436
   285
  val mk_coeff          = mk_coeff
wenzelm@9436
   286
  val dest_coeff        = dest_coeff
wenzelm@9436
   287
  val left_distrib      = left_add_mult_distrib RS trans
paulson@9544
   288
  val prove_conv = 
paulson@9544
   289
       Int_Numeral_Simprocs.prove_conv_nohyps "nat_combine_numerals"
wenzelm@9436
   290
  val trans_tac          = trans_tac
wenzelm@9436
   291
  val norm_tac = ALLGOALS
wenzelm@9436
   292
                   (simp_tac (HOL_ss addsimps add_0s@mult_1s@
wenzelm@9436
   293
                                       [add_0, Suc_eq_add_numeral_1]@add_ac))
wenzelm@9436
   294
                 THEN ALLGOALS (simp_tac
wenzelm@9436
   295
                                (HOL_ss addsimps bin_simps@add_ac@mult_ac))
wenzelm@9436
   296
  val numeral_simp_tac  = ALLGOALS
wenzelm@9436
   297
                (simp_tac (HOL_ss addsimps [numeral_0_eq_0 RS sym]@add_0s@bin_simps))
wenzelm@9436
   298
  val simplify_meta_eq  = simplify_meta_eq
wenzelm@9436
   299
  end;
wenzelm@9436
   300
wenzelm@9436
   301
structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
wenzelm@9436
   302
wenzelm@9436
   303
val combine_numerals =
wenzelm@9436
   304
    prep_simproc ("nat_combine_numerals",
wenzelm@9436
   305
                  prep_pats ["(i::nat) + j", "Suc (i + j)"],
wenzelm@9436
   306
                  CombineNumerals.proc);
wenzelm@9436
   307
paulson@10536
   308
paulson@10536
   309
(*** Instantiating CancelNumeralFactorFun ***)
paulson@10536
   310
paulson@10536
   311
structure CancelNumeralFactorCommon =
paulson@10536
   312
  struct
paulson@10536
   313
  val mk_coeff		= mk_coeff
paulson@10536
   314
  val dest_coeff	= dest_coeff
paulson@10536
   315
  val trans_tac         = trans_tac
paulson@10536
   316
  val norm_tac = ALLGOALS (simp_tac (HOL_ss addsimps 
paulson@10536
   317
                                             [Suc_eq_add_numeral_1]@mult_1s))
paulson@10536
   318
                 THEN ALLGOALS (simp_tac (HOL_ss addsimps bin_simps@mult_ac))
paulson@10536
   319
  val numeral_simp_tac	= ALLGOALS (simp_tac (HOL_ss addsimps bin_simps))
paulson@10536
   320
  val simplify_meta_eq  = simplify_meta_eq
paulson@10536
   321
  end
paulson@10536
   322
paulson@10536
   323
structure DivCancelNumeralFactor = CancelNumeralFactorFun
paulson@10536
   324
 (open CancelNumeralFactorCommon
paulson@10536
   325
  val prove_conv = prove_conv "natdiv_cancel_numeral_factor"
paulson@10536
   326
  val mk_bal   = HOLogic.mk_binop "Divides.op div"
paulson@10536
   327
  val dest_bal = HOLogic.dest_bin "Divides.op div" HOLogic.natT
paulson@10536
   328
  val cancel = nat_mult_div_cancel1 RS trans
paulson@10536
   329
  val neg_exchanges = false
paulson@10536
   330
)
paulson@10536
   331
paulson@10536
   332
structure EqCancelNumeralFactor = CancelNumeralFactorFun
paulson@10536
   333
 (open CancelNumeralFactorCommon
paulson@10536
   334
  val prove_conv = prove_conv "nateq_cancel_numeral_factor"
paulson@10536
   335
  val mk_bal   = HOLogic.mk_eq
paulson@10536
   336
  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
paulson@10536
   337
  val cancel = nat_mult_eq_cancel1 RS trans
paulson@10536
   338
  val neg_exchanges = false
paulson@10536
   339
)
paulson@10536
   340
paulson@10536
   341
structure LessCancelNumeralFactor = CancelNumeralFactorFun
paulson@10536
   342
 (open CancelNumeralFactorCommon
paulson@10536
   343
  val prove_conv = prove_conv "natless_cancel_numeral_factor"
paulson@10536
   344
  val mk_bal   = HOLogic.mk_binrel "op <"
paulson@10536
   345
  val dest_bal = HOLogic.dest_bin "op <" HOLogic.natT
paulson@10536
   346
  val cancel = nat_mult_less_cancel1 RS trans
paulson@10536
   347
  val neg_exchanges = true
paulson@10536
   348
)
paulson@10536
   349
paulson@10536
   350
structure LeCancelNumeralFactor = CancelNumeralFactorFun
paulson@10536
   351
 (open CancelNumeralFactorCommon
paulson@10536
   352
  val prove_conv = prove_conv "natle_cancel_numeral_factor"
paulson@10536
   353
  val mk_bal   = HOLogic.mk_binrel "op <="
paulson@10536
   354
  val dest_bal = HOLogic.dest_bin "op <=" HOLogic.natT
paulson@10536
   355
  val cancel = nat_mult_le_cancel1 RS trans
paulson@10536
   356
  val neg_exchanges = true
paulson@10536
   357
)
paulson@10536
   358
paulson@10536
   359
val cancel_numeral_factors = 
paulson@10536
   360
  map prep_simproc
paulson@10536
   361
   [("nateq_cancel_numeral_factors",
paulson@10536
   362
     prep_pats ["(l::nat) * m = n", "(l::nat) = m * n"], 
paulson@10536
   363
     EqCancelNumeralFactor.proc),
paulson@10536
   364
    ("natless_cancel_numeral_factors", 
paulson@10536
   365
     prep_pats ["(l::nat) * m < n", "(l::nat) < m * n"], 
paulson@10536
   366
     LessCancelNumeralFactor.proc),
paulson@10536
   367
    ("natle_cancel_numeral_factors", 
paulson@10536
   368
     prep_pats ["(l::nat) * m <= n", "(l::nat) <= m * n"], 
paulson@10536
   369
     LeCancelNumeralFactor.proc),
paulson@10536
   370
    ("natdiv_cancel_numeral_factors", 
paulson@10536
   371
     prep_pats ["((l::nat) * m) div n", "(l::nat) div (m * n)"], 
paulson@10536
   372
     DivCancelNumeralFactor.proc)];
paulson@10536
   373
wenzelm@9436
   374
end;
wenzelm@9436
   375
wenzelm@9436
   376
wenzelm@9436
   377
Addsimprocs Nat_Numeral_Simprocs.cancel_numerals;
wenzelm@9436
   378
Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
paulson@10536
   379
Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors;
wenzelm@9436
   380
wenzelm@9436
   381
wenzelm@9436
   382
(*examples:
wenzelm@9436
   383
print_depth 22;
wenzelm@9436
   384
set timing;
wenzelm@9436
   385
set trace_simp;
wenzelm@9436
   386
fun test s = (Goal s; by (Simp_tac 1));
wenzelm@9436
   387
wenzelm@9436
   388
(*cancel_numerals*)
wenzelm@9436
   389
test "l +( #2) + (#2) + #2 + (l + #2) + (oo  + #2) = (uu::nat)";
wenzelm@9436
   390
test "(#2*length xs < #2*length xs + j)";
wenzelm@9436
   391
test "(#2*length xs < length xs * #2 + j)";
wenzelm@9436
   392
test "#2*u = (u::nat)";
wenzelm@9436
   393
test "#2*u = Suc (u)";
wenzelm@9436
   394
test "(i + j + #12 + (k::nat)) - #15 = y";
wenzelm@9436
   395
test "(i + j + #12 + (k::nat)) - #5 = y";
wenzelm@9436
   396
test "Suc u - #2 = y";
wenzelm@9436
   397
test "Suc (Suc (Suc u)) - #2 = y";
wenzelm@9436
   398
test "(i + j + #2 + (k::nat)) - 1 = y";
wenzelm@9436
   399
test "(i + j + #1 + (k::nat)) - 2 = y";
wenzelm@9436
   400
wenzelm@9436
   401
test "(#2*x + (u*v) + y) - v*#3*u = (w::nat)";
wenzelm@9436
   402
test "(#2*x*u*v + #5 + (u*v)*#4 + y) - v*u*#4 = (w::nat)";
wenzelm@9436
   403
test "(#2*x*u*v + (u*v)*#4 + y) - v*u = (w::nat)";
wenzelm@9436
   404
test "Suc (Suc (#2*x*u*v + u*#4 + y)) - u = w";
wenzelm@9436
   405
test "Suc ((u*v)*#4) - v*#3*u = w";
wenzelm@9436
   406
test "Suc (Suc ((u*v)*#3)) - v*#3*u = w";
wenzelm@9436
   407
wenzelm@9436
   408
test "(i + j + #12 + (k::nat)) = u + #15 + y";
wenzelm@9436
   409
test "(i + j + #32 + (k::nat)) - (u + #15 + y) = zz";
wenzelm@9436
   410
test "(i + j + #12 + (k::nat)) = u + #5 + y";
wenzelm@9436
   411
(*Suc*)
wenzelm@9436
   412
test "(i + j + #12 + k) = Suc (u + y)";
wenzelm@9436
   413
test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + #41 + k)";
wenzelm@9436
   414
test "(i + j + #5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
wenzelm@9436
   415
test "Suc (Suc (Suc (Suc (Suc (u + y))))) - #5 = v";
wenzelm@9436
   416
test "(i + j + #5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
wenzelm@9436
   417
test "#2*y + #3*z + #2*u = Suc (u)";
wenzelm@9436
   418
test "#2*y + #3*z + #6*w + #2*y + #3*z + #2*u = Suc (u)";
wenzelm@9436
   419
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@9436
   420
test "#6 + #2*y + #3*z + #4*u = Suc (vv + #2*u + z)";
wenzelm@9436
   421
test "(#2*n*m) < (#3*(m*n)) + (u::nat)";
wenzelm@9436
   422
wenzelm@9436
   423
(*negative numerals: FAIL*)
wenzelm@9436
   424
test "(i + j + #-23 + (k::nat)) < u + #15 + y";
wenzelm@9436
   425
test "(i + j + #3 + (k::nat)) < u + #-15 + y";
wenzelm@9436
   426
test "(i + j + #-12 + (k::nat)) - #15 = y";
wenzelm@9436
   427
test "(i + j + #12 + (k::nat)) - #-15 = y";
wenzelm@9436
   428
test "(i + j + #-12 + (k::nat)) - #-15 = y";
wenzelm@9436
   429
wenzelm@9436
   430
(*combine_numerals*)
wenzelm@9436
   431
test "k + #3*k = (u::nat)";
wenzelm@9436
   432
test "Suc (i + #3) = u";
wenzelm@9436
   433
test "Suc (i + j + #3 + k) = u";
wenzelm@9436
   434
test "k + j + #3*k + j = (u::nat)";
wenzelm@9436
   435
test "Suc (j*i + i + k + #5 + #3*k + i*j*#4) = (u::nat)";
wenzelm@9436
   436
test "(#2*n*m) + (#3*(m*n)) = (u::nat)";
wenzelm@9436
   437
(*negative numerals: FAIL*)
wenzelm@9436
   438
test "Suc (i + j + #-3 + k) = u";
paulson@10536
   439
paulson@10536
   440
(*cancel_numeral_factor*)
paulson@10536
   441
test "#9*x = #12 * (y::nat)";
paulson@10536
   442
test "(#9*x) div (#12 * (y::nat)) = z";
paulson@10536
   443
test "#9*x < #12 * (y::nat)";
paulson@10536
   444
test "#9*x <= #12 * (y::nat)";
wenzelm@9436
   445
*)
wenzelm@9436
   446
wenzelm@9436
   447
wenzelm@9436
   448
(*** Prepare linear arithmetic for nat numerals ***)
wenzelm@9436
   449
wenzelm@9436
   450
local
wenzelm@9436
   451
wenzelm@9436
   452
(* reduce contradictory <= to False *)
wenzelm@9436
   453
val add_rules =
wenzelm@9436
   454
  [add_nat_number_of, diff_nat_number_of, mult_nat_number_of,
wenzelm@9436
   455
   eq_nat_number_of, less_nat_number_of, le_nat_number_of_eq_not_less,
wenzelm@9436
   456
   le_Suc_number_of,le_number_of_Suc,
wenzelm@9436
   457
   less_Suc_number_of,less_number_of_Suc,
wenzelm@9436
   458
   Suc_eq_number_of,eq_number_of_Suc,
wenzelm@9436
   459
   eq_number_of_0, eq_0_number_of, less_0_number_of,
wenzelm@9436
   460
   nat_number_of, Let_number_of, if_True, if_False];
wenzelm@9436
   461
wenzelm@9436
   462
val simprocs = [Nat_Times_Assoc.conv,
wenzelm@9436
   463
                Nat_Numeral_Simprocs.combine_numerals]@
wenzelm@9436
   464
                Nat_Numeral_Simprocs.cancel_numerals;
wenzelm@9436
   465
wenzelm@9436
   466
in
wenzelm@9436
   467
wenzelm@9436
   468
val nat_simprocs_setup =
nipkow@10574
   469
 [Fast_Arith.map_data (fn {add_mono_thms, inj_thms, lessD, simpset} =>
nipkow@10574
   470
   {add_mono_thms = add_mono_thms, inj_thms = inj_thms, lessD = lessD,
wenzelm@9436
   471
    simpset = simpset addsimps add_rules
wenzelm@9436
   472
                      addsimps basic_renamed_arith_simps
wenzelm@9436
   473
                      addsimprocs simprocs})];
wenzelm@9436
   474
wenzelm@9436
   475
end;