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