src/HOL/nat_simprocs.ML
author wenzelm
Fri Mar 28 19:43:54 2008 +0100 (2008-03-28)
changeset 26462 dac4e2bce00d
parent 25919 8b1c0d434824
child 27651 16a26996c30e
permissions -rw-r--r--
avoid rebinding of existing facts;
     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 structure Nat_Numeral_Simprocs =
    10 struct
    11 
    12 (*Maps n to #n for n = 0, 1, 2*)
    13 val numeral_syms =
    14        [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm numeral_2_eq_2} RS sym];
    15 val numeral_sym_ss = HOL_ss addsimps numeral_syms;
    16 
    17 fun rename_numerals th =
    18     simplify numeral_sym_ss (Thm.transfer (the_context ()) th);
    19 
    20 (*Utilities*)
    21 
    22 fun mk_number n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_numeral n;
    23 fun dest_number t = Int.max (0, snd (HOLogic.dest_number t));
    24 
    25 fun find_first_numeral past (t::terms) =
    26         ((dest_number t, t, rev past @ terms)
    27          handle TERM _ => find_first_numeral (t::past) terms)
    28   | find_first_numeral past [] = raise TERM("find_first_numeral", []);
    29 
    30 val zero = mk_number 0;
    31 val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
    32 
    33 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
    34 fun mk_sum []        = zero
    35   | mk_sum [t,u]     = mk_plus (t, u)
    36   | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    37 
    38 (*this version ALWAYS includes a trailing zero*)
    39 fun long_mk_sum []        = HOLogic.zero
    40   | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    41 
    42 val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
    43 
    44 
    45 (** Other simproc items **)
    46 
    47 val trans_tac = Int_Numeral_Simprocs.trans_tac;
    48 
    49 val bin_simps =
    50      [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym,
    51       @{thm add_nat_number_of}, @{thm nat_number_of_add_left}, 
    52       @{thm diff_nat_number_of}, @{thm le_number_of_eq_not_less},
    53       @{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, 
    54       @{thm less_nat_number_of}, 
    55       @{thm Let_number_of}, @{thm nat_number_of}] @
    56      @{thms arith_simps} @ @{thms rel_simps};
    57 
    58 fun prep_simproc (name, pats, proc) =
    59   Simplifier.simproc (the_context ()) name pats proc;
    60 
    61 
    62 (*** CancelNumerals simprocs ***)
    63 
    64 val one = mk_number 1;
    65 val mk_times = HOLogic.mk_binop @{const_name HOL.times};
    66 
    67 fun mk_prod [] = one
    68   | mk_prod [t] = t
    69   | mk_prod (t :: ts) = if t = one then mk_prod ts
    70                         else mk_times (t, mk_prod ts);
    71 
    72 val dest_times = HOLogic.dest_bin @{const_name HOL.times} HOLogic.natT;
    73 
    74 fun dest_prod t =
    75       let val (t,u) = dest_times t
    76       in  dest_prod t @ dest_prod u  end
    77       handle TERM _ => [t];
    78 
    79 (*DON'T do the obvious simplifications; that would create special cases*)
    80 fun mk_coeff (k,t) = mk_times (mk_number k, t);
    81 
    82 (*Express t as a product of (possibly) a numeral with other factors, sorted*)
    83 fun dest_coeff t =
    84     let val ts = sort Term.term_ord (dest_prod t)
    85         val (n, _, ts') = find_first_numeral [] ts
    86                           handle TERM _ => (1, one, ts)
    87     in (n, mk_prod ts') end;
    88 
    89 (*Find first coefficient-term THAT MATCHES u*)
    90 fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
    91   | find_first_coeff past u (t::terms) =
    92         let val (n,u') = dest_coeff t
    93         in  if u aconv u' then (n, rev past @ terms)
    94                           else find_first_coeff (t::past) u terms
    95         end
    96         handle TERM _ => find_first_coeff (t::past) u terms;
    97 
    98 
    99 (*Split up a sum into the list of its constituent terms, on the way removing any
   100   Sucs and counting them.*)
   101 fun dest_Suc_sum (Const ("Suc", _) $ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts))
   102   | dest_Suc_sum (t, (k,ts)) = 
   103       let val (t1,t2) = dest_plus t
   104       in  dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts)))  end
   105       handle TERM _ => (k, t::ts);
   106 
   107 (*Code for testing whether numerals are already used in the goal*)
   108 fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true
   109   | is_numeral _ = false;
   110 
   111 fun prod_has_numeral t = exists is_numeral (dest_prod t);
   112 
   113 (*The Sucs found in the term are converted to a binary numeral. If relaxed is false,
   114   an exception is raised unless the original expression contains at least one
   115   numeral in a coefficient position.  This prevents nat_combine_numerals from 
   116   introducing numerals to goals.*)
   117 fun dest_Sucs_sum relaxed t = 
   118   let val (k,ts) = dest_Suc_sum (t,(0,[]))
   119   in
   120      if relaxed orelse exists prod_has_numeral ts then 
   121        if k=0 then ts
   122        else mk_number k :: ts
   123      else raise TERM("Nat_Numeral_Simprocs.dest_Sucs_sum", [t])
   124   end;
   125 
   126 
   127 (*Simplify 1*n and n*1 to n*)
   128 val add_0s  = map rename_numerals [@{thm add_0}, @{thm add_0_right}];
   129 val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}];
   130 
   131 (*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
   132 
   133 (*And these help the simproc return False when appropriate, which helps
   134   the arith prover.*)
   135 val contra_rules = [@{thm add_Suc}, @{thm add_Suc_right}, @{thm Zero_not_Suc},
   136   @{thm Suc_not_Zero}, @{thm le_0_eq}];
   137 
   138 val simplify_meta_eq =
   139     Int_Numeral_Simprocs.simplify_meta_eq
   140         ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm add_0}, @{thm add_0_right},
   141           @{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules);
   142 
   143 
   144 (*Like HOL_ss but with an ordering that brings numerals to the front
   145   under AC-rewriting.*)
   146 val num_ss = Int_Numeral_Simprocs.num_ss;
   147 
   148 (*** Applying CancelNumeralsFun ***)
   149 
   150 structure CancelNumeralsCommon =
   151   struct
   152   val mk_sum            = (fn T:typ => mk_sum)
   153   val dest_sum          = dest_Sucs_sum true
   154   val mk_coeff          = mk_coeff
   155   val dest_coeff        = dest_coeff
   156   val find_first_coeff  = find_first_coeff []
   157   val trans_tac         = fn _ => trans_tac
   158 
   159   val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   160     [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
   161   val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   162   fun norm_tac ss = 
   163     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   164     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   165 
   166   val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
   167   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss));
   168   val simplify_meta_eq  = simplify_meta_eq
   169   end;
   170 
   171 
   172 structure EqCancelNumerals = CancelNumeralsFun
   173  (open CancelNumeralsCommon
   174   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   175   val mk_bal   = HOLogic.mk_eq
   176   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   177   val bal_add1 = @{thm nat_eq_add_iff1} RS trans
   178   val bal_add2 = @{thm nat_eq_add_iff2} RS trans
   179 );
   180 
   181 structure LessCancelNumerals = CancelNumeralsFun
   182  (open CancelNumeralsCommon
   183   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   184   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   185   val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   186   val bal_add1 = @{thm nat_less_add_iff1} RS trans
   187   val bal_add2 = @{thm nat_less_add_iff2} RS trans
   188 );
   189 
   190 structure LeCancelNumerals = CancelNumeralsFun
   191  (open CancelNumeralsCommon
   192   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   193   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   194   val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   195   val bal_add1 = @{thm nat_le_add_iff1} RS trans
   196   val bal_add2 = @{thm nat_le_add_iff2} RS trans
   197 );
   198 
   199 structure DiffCancelNumerals = CancelNumeralsFun
   200  (open CancelNumeralsCommon
   201   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   202   val mk_bal   = HOLogic.mk_binop @{const_name HOL.minus}
   203   val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT
   204   val bal_add1 = @{thm nat_diff_add_eq1} RS trans
   205   val bal_add2 = @{thm nat_diff_add_eq2} RS trans
   206 );
   207 
   208 
   209 val cancel_numerals =
   210   map prep_simproc
   211    [("nateq_cancel_numerals",
   212      ["(l::nat) + m = n", "(l::nat) = m + n",
   213       "(l::nat) * m = n", "(l::nat) = m * n",
   214       "Suc m = n", "m = Suc n"],
   215      K EqCancelNumerals.proc),
   216     ("natless_cancel_numerals",
   217      ["(l::nat) + m < n", "(l::nat) < m + n",
   218       "(l::nat) * m < n", "(l::nat) < m * n",
   219       "Suc m < n", "m < Suc n"],
   220      K LessCancelNumerals.proc),
   221     ("natle_cancel_numerals",
   222      ["(l::nat) + m <= n", "(l::nat) <= m + n",
   223       "(l::nat) * m <= n", "(l::nat) <= m * n",
   224       "Suc m <= n", "m <= Suc n"],
   225      K LeCancelNumerals.proc),
   226     ("natdiff_cancel_numerals",
   227      ["((l::nat) + m) - n", "(l::nat) - (m + n)",
   228       "(l::nat) * m - n", "(l::nat) - m * n",
   229       "Suc m - n", "m - Suc n"],
   230      K DiffCancelNumerals.proc)];
   231 
   232 
   233 (*** Applying CombineNumeralsFun ***)
   234 
   235 structure CombineNumeralsData =
   236   struct
   237   type coeff            = int
   238   val iszero            = (fn x => x = 0)
   239   val add               = op +
   240   val mk_sum            = (fn T:typ => long_mk_sum)  (*to work for 2*x + 3*x *)
   241   val dest_sum          = dest_Sucs_sum false
   242   val mk_coeff          = mk_coeff
   243   val dest_coeff        = dest_coeff
   244   val left_distrib      = @{thm left_add_mult_distrib} RS trans
   245   val prove_conv        = Int_Numeral_Base_Simprocs.prove_conv_nohyps
   246   val trans_tac         = fn _ => trans_tac
   247 
   248   val norm_ss1 = num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
   249   val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   250   fun norm_tac ss =
   251     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   252     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   253 
   254   val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
   255   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   256   val simplify_meta_eq  = simplify_meta_eq
   257   end;
   258 
   259 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   260 
   261 val combine_numerals =
   262   prep_simproc ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
   263 
   264 
   265 (*** Applying CancelNumeralFactorFun ***)
   266 
   267 structure CancelNumeralFactorCommon =
   268   struct
   269   val mk_coeff          = mk_coeff
   270   val dest_coeff        = dest_coeff
   271   val trans_tac         = fn _ => trans_tac
   272 
   273   val norm_ss1 = num_ss addsimps
   274     numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
   275   val norm_ss2 = num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   276   fun norm_tac ss =
   277     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   278     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   279 
   280   val numeral_simp_ss = HOL_ss addsimps bin_simps
   281   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   282   val simplify_meta_eq  = simplify_meta_eq
   283   end
   284 
   285 structure DivCancelNumeralFactor = CancelNumeralFactorFun
   286  (open CancelNumeralFactorCommon
   287   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   288   val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   289   val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
   290   val cancel = @{thm nat_mult_div_cancel1} RS trans
   291   val neg_exchanges = false
   292 )
   293 
   294 structure DvdCancelNumeralFactor = CancelNumeralFactorFun
   295  (open CancelNumeralFactorCommon
   296   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   297   val mk_bal   = HOLogic.mk_binrel @{const_name Divides.dvd}
   298   val dest_bal = HOLogic.dest_bin @{const_name Divides.dvd} HOLogic.natT
   299   val cancel = @{thm nat_mult_dvd_cancel1} RS trans
   300   val neg_exchanges = false
   301 )
   302 
   303 structure EqCancelNumeralFactor = CancelNumeralFactorFun
   304  (open CancelNumeralFactorCommon
   305   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   306   val mk_bal   = HOLogic.mk_eq
   307   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   308   val cancel = @{thm nat_mult_eq_cancel1} RS trans
   309   val neg_exchanges = false
   310 )
   311 
   312 structure LessCancelNumeralFactor = CancelNumeralFactorFun
   313  (open CancelNumeralFactorCommon
   314   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   315   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   316   val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   317   val cancel = @{thm nat_mult_less_cancel1} RS trans
   318   val neg_exchanges = true
   319 )
   320 
   321 structure LeCancelNumeralFactor = CancelNumeralFactorFun
   322  (open CancelNumeralFactorCommon
   323   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   324   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   325   val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   326   val cancel = @{thm nat_mult_le_cancel1} RS trans
   327   val neg_exchanges = true
   328 )
   329 
   330 val cancel_numeral_factors =
   331   map prep_simproc
   332    [("nateq_cancel_numeral_factors",
   333      ["(l::nat) * m = n", "(l::nat) = m * n"],
   334      K EqCancelNumeralFactor.proc),
   335     ("natless_cancel_numeral_factors",
   336      ["(l::nat) * m < n", "(l::nat) < m * n"],
   337      K LessCancelNumeralFactor.proc),
   338     ("natle_cancel_numeral_factors",
   339      ["(l::nat) * m <= n", "(l::nat) <= m * n"],
   340      K LeCancelNumeralFactor.proc),
   341     ("natdiv_cancel_numeral_factors",
   342      ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
   343      K DivCancelNumeralFactor.proc),
   344     ("natdvd_cancel_numeral_factors",
   345      ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
   346      K DvdCancelNumeralFactor.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 = Int_Numeral_Simprocs.simplify_meta_eq  
   365   [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}];
   366 
   367 fun cancel_simplify_meta_eq cancel_th ss th =
   368     simplify_one ss (([th, cancel_th]) MRS trans);
   369 
   370 structure CancelFactorCommon =
   371   struct
   372   val mk_sum            = (fn T:typ => long_mk_prod)
   373   val dest_sum          = dest_prod
   374   val mk_coeff          = mk_coeff
   375   val dest_coeff        = dest_coeff
   376   val find_first        = find_first_t []
   377   val trans_tac         = fn _ => trans_tac
   378   val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   379   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   380   end;
   381 
   382 structure EqCancelFactor = ExtractCommonTermFun
   383  (open CancelFactorCommon
   384   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   385   val mk_bal   = HOLogic.mk_eq
   386   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   387   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_eq_cancel_disj}
   388 );
   389 
   390 structure LessCancelFactor = ExtractCommonTermFun
   391  (open CancelFactorCommon
   392   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   393   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less}
   394   val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT
   395   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_less_cancel_disj}
   396 );
   397 
   398 structure LeCancelFactor = ExtractCommonTermFun
   399  (open CancelFactorCommon
   400   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   401   val mk_bal   = HOLogic.mk_binrel @{const_name HOL.less_eq}
   402   val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT
   403   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_le_cancel_disj}
   404 );
   405 
   406 structure DivideCancelFactor = ExtractCommonTermFun
   407  (open CancelFactorCommon
   408   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   409   val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   410   val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
   411   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_div_cancel_disj}
   412 );
   413 
   414 structure DvdCancelFactor = ExtractCommonTermFun
   415  (open CancelFactorCommon
   416   val prove_conv = Int_Numeral_Base_Simprocs.prove_conv
   417   val mk_bal   = HOLogic.mk_binrel @{const_name Divides.dvd}
   418   val dest_bal = HOLogic.dest_bin @{const_name Divides.dvd} HOLogic.natT
   419   val simplify_meta_eq  = cancel_simplify_meta_eq @{thm nat_mult_dvd_cancel_disj}
   420 );
   421 
   422 val cancel_factor =
   423   map prep_simproc
   424    [("nat_eq_cancel_factor",
   425      ["(l::nat) * m = n", "(l::nat) = m * n"],
   426      K EqCancelFactor.proc),
   427     ("nat_less_cancel_factor",
   428      ["(l::nat) * m < n", "(l::nat) < m * n"],
   429      K LessCancelFactor.proc),
   430     ("nat_le_cancel_factor",
   431      ["(l::nat) * m <= n", "(l::nat) <= m * n"],
   432      K LeCancelFactor.proc),
   433     ("nat_divide_cancel_factor",
   434      ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
   435      K DivideCancelFactor.proc),
   436     ("nat_dvd_cancel_factor",
   437      ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
   438      K DvdCancelFactor.proc)];
   439 
   440 end;
   441 
   442 
   443 Addsimprocs Nat_Numeral_Simprocs.cancel_numerals;
   444 Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
   445 Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors;
   446 Addsimprocs Nat_Numeral_Simprocs.cancel_factor;
   447 
   448 
   449 (*examples:
   450 print_depth 22;
   451 set timing;
   452 set trace_simp;
   453 fun test s = (Goal s; by (Simp_tac 1));
   454 
   455 (*cancel_numerals*)
   456 test "l +( 2) + (2) + 2 + (l + 2) + (oo  + 2) = (uu::nat)";
   457 test "(2*length xs < 2*length xs + j)";
   458 test "(2*length xs < length xs * 2 + j)";
   459 test "2*u = (u::nat)";
   460 test "2*u = Suc (u)";
   461 test "(i + j + 12 + (k::nat)) - 15 = y";
   462 test "(i + j + 12 + (k::nat)) - 5 = y";
   463 test "Suc u - 2 = y";
   464 test "Suc (Suc (Suc u)) - 2 = y";
   465 test "(i + j + 2 + (k::nat)) - 1 = y";
   466 test "(i + j + 1 + (k::nat)) - 2 = y";
   467 
   468 test "(2*x + (u*v) + y) - v*3*u = (w::nat)";
   469 test "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = (w::nat)";
   470 test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::nat)";
   471 test "Suc (Suc (2*x*u*v + u*4 + y)) - u = w";
   472 test "Suc ((u*v)*4) - v*3*u = w";
   473 test "Suc (Suc ((u*v)*3)) - v*3*u = w";
   474 
   475 test "(i + j + 12 + (k::nat)) = u + 15 + y";
   476 test "(i + j + 32 + (k::nat)) - (u + 15 + y) = zz";
   477 test "(i + j + 12 + (k::nat)) = u + 5 + y";
   478 (*Suc*)
   479 test "(i + j + 12 + k) = Suc (u + y)";
   480 test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + 41 + k)";
   481 test "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
   482 test "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v";
   483 test "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
   484 test "2*y + 3*z + 2*u = Suc (u)";
   485 test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)";
   486 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)";
   487 test "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)";
   488 test "(2*n*m) < (3*(m*n)) + (u::nat)";
   489 
   490 test "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0 | Suc k => k)))))) <= Suc 0)";
   491  
   492 test "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) <= length l1";
   493 
   494 test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length l3)))))) <= length (compT P E A ST mxr e))";
   495 
   496 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))";
   497 
   498 
   499 (*negative numerals: FAIL*)
   500 test "(i + j + -23 + (k::nat)) < u + 15 + y";
   501 test "(i + j + 3 + (k::nat)) < u + -15 + y";
   502 test "(i + j + -12 + (k::nat)) - 15 = y";
   503 test "(i + j + 12 + (k::nat)) - -15 = y";
   504 test "(i + j + -12 + (k::nat)) - -15 = y";
   505 
   506 (*combine_numerals*)
   507 test "k + 3*k = (u::nat)";
   508 test "Suc (i + 3) = u";
   509 test "Suc (i + j + 3 + k) = u";
   510 test "k + j + 3*k + j = (u::nat)";
   511 test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)";
   512 test "(2*n*m) + (3*(m*n)) = (u::nat)";
   513 (*negative numerals: FAIL*)
   514 test "Suc (i + j + -3 + k) = u";
   515 
   516 (*cancel_numeral_factors*)
   517 test "9*x = 12 * (y::nat)";
   518 test "(9*x) div (12 * (y::nat)) = z";
   519 test "9*x < 12 * (y::nat)";
   520 test "9*x <= 12 * (y::nat)";
   521 
   522 (*cancel_factor*)
   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 < k*(y::nat)";
   529 test "k < k*(y::nat)";
   530 test "a*(b*c) < (b::nat)";
   531 test "a*(b*c) < d*(b::nat)*(x*a)";
   532 
   533 test "x*k <= k*(y::nat)";
   534 test "k <= k*(y::nat)";
   535 test "a*(b*c) <= (b::nat)";
   536 test "a*(b*c) <= d*(b::nat)*(x*a)";
   537 
   538 test "(x*k) div (k*(y::nat)) = (uu::nat)";
   539 test "(k) div (k*(y::nat)) = (uu::nat)";
   540 test "(a*(b*c)) div ((b::nat)) = (uu::nat)";
   541 test "(a*(b*c)) div (d*(b::nat)*(x*a)) = (uu::nat)";
   542 *)
   543 
   544 
   545 (*** Prepare linear arithmetic for nat numerals ***)
   546 
   547 local
   548 
   549 (* reduce contradictory <= to False *)
   550 val add_rules = @{thms ring_distribs} @
   551   [@{thm Let_number_of}, @{thm Let_0}, @{thm Let_1}, @{thm nat_0}, @{thm nat_1},
   552    @{thm add_nat_number_of}, @{thm diff_nat_number_of}, @{thm mult_nat_number_of},
   553    @{thm eq_nat_number_of}, @{thm less_nat_number_of}, @{thm le_number_of_eq_not_less},
   554    @{thm le_Suc_number_of}, @{thm le_number_of_Suc},
   555    @{thm less_Suc_number_of}, @{thm less_number_of_Suc},
   556    @{thm Suc_eq_number_of}, @{thm eq_number_of_Suc},
   557    @{thm mult_Suc}, @{thm mult_Suc_right},
   558    @{thm add_Suc}, @{thm add_Suc_right},
   559    @{thm eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
   560    @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of}, @{thm if_True}, @{thm if_False}];
   561 
   562 (* Products are multiplied out during proof (re)construction via
   563 ring_distribs. Ideally they should remain atomic. But that is
   564 currently not possible because 1 is replaced by Suc 0, and then some
   565 simprocs start to mess around with products like (n+1)*m. The rule
   566 1 == Suc 0 is necessary for early parts of HOL where numerals and
   567 simprocs are not yet available. But then it is difficult to remove
   568 that rule later on, because it may find its way back in when theories
   569 (and thus lin-arith simpsets) are merged. Otherwise one could turn the
   570 rule around (Suc n = n+1) and see if that helps products being left
   571 alone. *)
   572 
   573 val simprocs = Nat_Numeral_Simprocs.combine_numerals
   574   :: Nat_Numeral_Simprocs.cancel_numerals;
   575 
   576 in
   577 
   578 val nat_simprocs_setup =
   579   LinArith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
   580    {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
   581     inj_thms = inj_thms, lessD = lessD, neqE = neqE,
   582     simpset = simpset addsimps add_rules
   583                       addsimprocs simprocs});
   584 
   585 end;