src/HOL/nat_simprocs.ML
author nipkow
Tue Jul 24 19:58:53 2007 +0200 (2007-07-24)
changeset 23969 ef782bbf2d09
parent 23881 851c74f1bb69
child 24093 5d0ecd0c8f3c
permissions -rw-r--r--
Added cancel simprocs for dvd on nat and int
     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 = IntInf.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      arith_simps @ 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 Numeral.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 (IntInf.fromInt 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            = IntInf.int
   238   val iszero            = (fn x : IntInf.int => x = 0)
   239   val add               = IntInf.+
   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 =
   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 eq_number_of_0}, @{thm eq_0_number_of}, @{thm less_0_number_of},
   559    @{thm of_int_number_of_eq}, @{thm of_nat_number_of_eq}, @{thm nat_number_of}, @{thm if_True}, @{thm if_False}];
   560 
   561 val simprocs = Nat_Numeral_Simprocs.combine_numerals
   562   :: Nat_Numeral_Simprocs.cancel_numerals;
   563 
   564 in
   565 
   566 val nat_simprocs_setup =
   567   Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
   568    {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
   569     inj_thms = inj_thms, lessD = lessD, neqE = neqE,
   570     simpset = simpset addsimps add_rules
   571                       addsimprocs simprocs});
   572 
   573 end;