src/HOL/Tools/nat_numeral_simprocs.ML
author haftmann
Fri Feb 19 14:47:01 2010 +0100 (2010-02-19)
changeset 35267 8dfd816713c6
parent 35092 cfe605c54e50
child 35408 b48ab741683b
permissions -rw-r--r--
moved remaning class operations from Algebras.thy to Groups.thy
     1 (* Author: Lawrence C Paulson, Cambridge University Computer Laboratory
     2 
     3 Simprocs for nat numerals.
     4 *)
     5 
     6 signature NAT_NUMERAL_SIMPROCS =
     7 sig
     8   val combine_numerals: simproc
     9   val cancel_numerals: simproc list
    10   val cancel_factors: simproc list
    11   val cancel_numeral_factors: simproc list
    12 end;
    13 
    14 structure Nat_Numeral_Simprocs =
    15 struct
    16 
    17 (*Maps n to #n for n = 0, 1, 2*)
    18 val numeral_syms = [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym, @{thm 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 @{theory} th);
    23 
    24 (*Utilities*)
    25 
    26 fun mk_number n = HOLogic.number_of_const HOLogic.natT $ HOLogic.mk_numeral n;
    27 fun dest_number t = Int.max (0, snd (HOLogic.dest_number t));
    28 
    29 fun find_first_numeral past (t::terms) =
    30         ((dest_number t, t, rev past @ terms)
    31          handle TERM _ => find_first_numeral (t::past) terms)
    32   | find_first_numeral past [] = raise TERM("find_first_numeral", []);
    33 
    34 val zero = mk_number 0;
    35 val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
    36 
    37 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
    38 fun mk_sum []        = zero
    39   | mk_sum [t,u]     = mk_plus (t, u)
    40   | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    41 
    42 (*this version ALWAYS includes a trailing zero*)
    43 fun long_mk_sum []        = HOLogic.zero
    44   | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    45 
    46 val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
    47 
    48 
    49 (** Other simproc items **)
    50 
    51 val bin_simps =
    52      [@{thm nat_numeral_0_eq_0} RS sym, @{thm nat_numeral_1_eq_1} RS sym,
    53       @{thm add_nat_number_of}, @{thm nat_number_of_add_left}, 
    54       @{thm diff_nat_number_of}, @{thm le_number_of_eq_not_less},
    55       @{thm mult_nat_number_of}, @{thm nat_number_of_mult_left}, 
    56       @{thm less_nat_number_of}, 
    57       @{thm Let_number_of}, @{thm nat_number_of}] @
    58      @{thms arith_simps} @ @{thms rel_simps} @ @{thms neg_simps};
    59 
    60 
    61 (*** CancelNumerals simprocs ***)
    62 
    63 val one = mk_number 1;
    64 val mk_times = HOLogic.mk_binop @{const_name Groups.times};
    65 
    66 fun mk_prod [] = one
    67   | mk_prod [t] = t
    68   | mk_prod (t :: ts) = if t = one then mk_prod ts
    69                         else mk_times (t, mk_prod ts);
    70 
    71 val dest_times = HOLogic.dest_bin @{const_name Groups.times} HOLogic.natT;
    72 
    73 fun dest_prod t =
    74       let val (t,u) = dest_times t
    75       in  dest_prod t @ dest_prod u  end
    76       handle TERM _ => [t];
    77 
    78 (*DON'T do the obvious simplifications; that would create special cases*)
    79 fun mk_coeff (k,t) = mk_times (mk_number k, t);
    80 
    81 (*Express t as a product of (possibly) a numeral with other factors, sorted*)
    82 fun dest_coeff t =
    83     let val ts = sort TermOrd.term_ord (dest_prod t)
    84         val (n, _, ts') = find_first_numeral [] ts
    85                           handle TERM _ => (1, one, ts)
    86     in (n, mk_prod ts') end;
    87 
    88 (*Find first coefficient-term THAT MATCHES u*)
    89 fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
    90   | find_first_coeff past u (t::terms) =
    91         let val (n,u') = dest_coeff t
    92         in  if u aconv u' then (n, rev past @ terms)
    93                           else find_first_coeff (t::past) u terms
    94         end
    95         handle TERM _ => find_first_coeff (t::past) u terms;
    96 
    97 
    98 (*Split up a sum into the list of its constituent terms, on the way removing any
    99   Sucs and counting them.*)
   100 fun dest_Suc_sum (Const ("Suc", _) $ t, (k,ts)) = dest_Suc_sum (t, (k+1,ts))
   101   | dest_Suc_sum (t, (k,ts)) = 
   102       let val (t1,t2) = dest_plus t
   103       in  dest_Suc_sum (t1, dest_Suc_sum (t2, (k,ts)))  end
   104       handle TERM _ => (k, t::ts);
   105 
   106 (*Code for testing whether numerals are already used in the goal*)
   107 fun is_numeral (Const(@{const_name Int.number_of}, _) $ w) = true
   108   | is_numeral _ = false;
   109 
   110 fun prod_has_numeral t = exists is_numeral (dest_prod t);
   111 
   112 (*The Sucs found in the term are converted to a binary numeral. If relaxed is false,
   113   an exception is raised unless the original expression contains at least one
   114   numeral in a coefficient position.  This prevents nat_combine_numerals from 
   115   introducing numerals to goals.*)
   116 fun dest_Sucs_sum relaxed t = 
   117   let val (k,ts) = dest_Suc_sum (t,(0,[]))
   118   in
   119      if relaxed orelse exists prod_has_numeral ts then 
   120        if k=0 then ts
   121        else mk_number k :: ts
   122      else raise TERM("Nat_Numeral_Simprocs.dest_Sucs_sum", [t])
   123   end;
   124 
   125 
   126 (*Simplify 1*n and n*1 to n*)
   127 val add_0s  = map rename_numerals [@{thm Nat.add_0}, @{thm Nat.add_0_right}];
   128 val mult_1s = map rename_numerals [@{thm nat_mult_1}, @{thm nat_mult_1_right}];
   129 
   130 (*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
   131 
   132 (*And these help the simproc return False when appropriate, which helps
   133   the arith prover.*)
   134 val contra_rules = [@{thm add_Suc}, @{thm add_Suc_right}, @{thm Zero_not_Suc},
   135   @{thm Suc_not_Zero}, @{thm le_0_eq}];
   136 
   137 val simplify_meta_eq =
   138     Arith_Data.simplify_meta_eq
   139         ([@{thm nat_numeral_0_eq_0}, @{thm numeral_1_eq_Suc_0}, @{thm Nat.add_0}, @{thm Nat.add_0_right},
   140           @{thm mult_0}, @{thm mult_0_right}, @{thm mult_1}, @{thm mult_1_right}] @ contra_rules);
   141 
   142 
   143 (*** Applying CancelNumeralsFun ***)
   144 
   145 structure CancelNumeralsCommon =
   146   struct
   147   val mk_sum            = (fn T:typ => mk_sum)
   148   val dest_sum          = dest_Sucs_sum true
   149   val mk_coeff          = mk_coeff
   150   val dest_coeff        = dest_coeff
   151   val find_first_coeff  = find_first_coeff []
   152   fun trans_tac _       = Arith_Data.trans_tac
   153 
   154   val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @
   155     [@{thm Suc_eq_plus1_left}] @ @{thms add_ac}
   156   val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   157   fun norm_tac ss = 
   158     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   159     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   160 
   161   val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
   162   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss));
   163   val simplify_meta_eq  = simplify_meta_eq
   164   end;
   165 
   166 
   167 structure EqCancelNumerals = CancelNumeralsFun
   168  (open CancelNumeralsCommon
   169   val prove_conv = Arith_Data.prove_conv
   170   val mk_bal   = HOLogic.mk_eq
   171   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   172   val bal_add1 = @{thm nat_eq_add_iff1} RS trans
   173   val bal_add2 = @{thm nat_eq_add_iff2} RS trans
   174 );
   175 
   176 structure LessCancelNumerals = CancelNumeralsFun
   177  (open CancelNumeralsCommon
   178   val prove_conv = Arith_Data.prove_conv
   179   val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   180   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
   181   val bal_add1 = @{thm nat_less_add_iff1} RS trans
   182   val bal_add2 = @{thm nat_less_add_iff2} RS trans
   183 );
   184 
   185 structure LeCancelNumerals = CancelNumeralsFun
   186  (open CancelNumeralsCommon
   187   val prove_conv = Arith_Data.prove_conv
   188   val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   189   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   190   val bal_add1 = @{thm nat_le_add_iff1} RS trans
   191   val bal_add2 = @{thm nat_le_add_iff2} RS trans
   192 );
   193 
   194 structure DiffCancelNumerals = CancelNumeralsFun
   195  (open CancelNumeralsCommon
   196   val prove_conv = Arith_Data.prove_conv
   197   val mk_bal   = HOLogic.mk_binop @{const_name Groups.minus}
   198   val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT
   199   val bal_add1 = @{thm nat_diff_add_eq1} RS trans
   200   val bal_add2 = @{thm nat_diff_add_eq2} RS trans
   201 );
   202 
   203 
   204 val cancel_numerals =
   205   map (Arith_Data.prep_simproc @{theory})
   206    [("nateq_cancel_numerals",
   207      ["(l::nat) + m = n", "(l::nat) = m + n",
   208       "(l::nat) * m = n", "(l::nat) = m * n",
   209       "Suc m = n", "m = Suc n"],
   210      K EqCancelNumerals.proc),
   211     ("natless_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 LessCancelNumerals.proc),
   216     ("natle_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 LeCancelNumerals.proc),
   221     ("natdiff_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 DiffCancelNumerals.proc)];
   226 
   227 
   228 (*** Applying CombineNumeralsFun ***)
   229 
   230 structure CombineNumeralsData =
   231   struct
   232   type coeff            = int
   233   val iszero            = (fn x => x = 0)
   234   val add               = op +
   235   val mk_sum            = (fn T:typ => long_mk_sum)  (*to work for 2*x + 3*x *)
   236   val dest_sum          = dest_Sucs_sum false
   237   val mk_coeff          = mk_coeff
   238   val dest_coeff        = dest_coeff
   239   val left_distrib      = @{thm left_add_mult_distrib} RS trans
   240   val prove_conv        = Arith_Data.prove_conv_nohyps
   241   fun trans_tac _       = Arith_Data.trans_tac
   242 
   243   val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1}] @ @{thms add_ac}
   244   val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   245   fun norm_tac ss =
   246     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   247     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   248 
   249   val numeral_simp_ss = HOL_ss addsimps add_0s @ bin_simps;
   250   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   251   val simplify_meta_eq  = simplify_meta_eq
   252   end;
   253 
   254 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   255 
   256 val combine_numerals =
   257   Arith_Data.prep_simproc @{theory}
   258     ("nat_combine_numerals", ["(i::nat) + j", "Suc (i + j)"], K CombineNumerals.proc);
   259 
   260 
   261 (*** Applying CancelNumeralFactorFun ***)
   262 
   263 structure CancelNumeralFactorCommon =
   264   struct
   265   val mk_coeff          = mk_coeff
   266   val dest_coeff        = dest_coeff
   267   fun trans_tac _       = Arith_Data.trans_tac
   268 
   269   val norm_ss1 = Numeral_Simprocs.num_ss addsimps
   270     numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms add_ac}
   271   val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   272   fun norm_tac ss =
   273     ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   274     THEN ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss2))
   275 
   276   val numeral_simp_ss = HOL_ss addsimps bin_simps
   277   fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   278   val simplify_meta_eq  = simplify_meta_eq
   279   end
   280 
   281 structure DivCancelNumeralFactor = CancelNumeralFactorFun
   282  (open CancelNumeralFactorCommon
   283   val prove_conv = Arith_Data.prove_conv
   284   val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   285   val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
   286   val cancel = @{thm nat_mult_div_cancel1} RS trans
   287   val neg_exchanges = false
   288 )
   289 
   290 structure DvdCancelNumeralFactor = CancelNumeralFactorFun
   291  (open CancelNumeralFactorCommon
   292   val prove_conv = Arith_Data.prove_conv
   293   val mk_bal   = HOLogic.mk_binrel @{const_name Rings.dvd}
   294   val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} HOLogic.natT
   295   val cancel = @{thm nat_mult_dvd_cancel1} RS trans
   296   val neg_exchanges = false
   297 )
   298 
   299 structure EqCancelNumeralFactor = CancelNumeralFactorFun
   300  (open CancelNumeralFactorCommon
   301   val prove_conv = Arith_Data.prove_conv
   302   val mk_bal   = HOLogic.mk_eq
   303   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   304   val cancel = @{thm nat_mult_eq_cancel1} RS trans
   305   val neg_exchanges = false
   306 )
   307 
   308 structure LessCancelNumeralFactor = CancelNumeralFactorFun
   309  (open CancelNumeralFactorCommon
   310   val prove_conv = Arith_Data.prove_conv
   311   val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   312   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
   313   val cancel = @{thm nat_mult_less_cancel1} RS trans
   314   val neg_exchanges = true
   315 )
   316 
   317 structure LeCancelNumeralFactor = CancelNumeralFactorFun
   318  (open CancelNumeralFactorCommon
   319   val prove_conv = Arith_Data.prove_conv
   320   val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   321   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   322   val cancel = @{thm nat_mult_le_cancel1} RS trans
   323   val neg_exchanges = true
   324 )
   325 
   326 val cancel_numeral_factors =
   327   map (Arith_Data.prep_simproc @{theory})
   328    [("nateq_cancel_numeral_factors",
   329      ["(l::nat) * m = n", "(l::nat) = m * n"],
   330      K EqCancelNumeralFactor.proc),
   331     ("natless_cancel_numeral_factors",
   332      ["(l::nat) * m < n", "(l::nat) < m * n"],
   333      K LessCancelNumeralFactor.proc),
   334     ("natle_cancel_numeral_factors",
   335      ["(l::nat) * m <= n", "(l::nat) <= m * n"],
   336      K LeCancelNumeralFactor.proc),
   337     ("natdiv_cancel_numeral_factors",
   338      ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
   339      K DivCancelNumeralFactor.proc),
   340     ("natdvd_cancel_numeral_factors",
   341      ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
   342      K DvdCancelNumeralFactor.proc)];
   343 
   344 
   345 
   346 (*** Applying ExtractCommonTermFun ***)
   347 
   348 (*this version ALWAYS includes a trailing one*)
   349 fun long_mk_prod []        = one
   350   | long_mk_prod (t :: ts) = mk_times (t, mk_prod ts);
   351 
   352 (*Find first term that matches u*)
   353 fun find_first_t past u []         = raise TERM("find_first_t", [])
   354   | find_first_t past u (t::terms) =
   355         if u aconv t then (rev past @ terms)
   356         else find_first_t (t::past) u terms
   357         handle TERM _ => find_first_t (t::past) u terms;
   358 
   359 (** Final simplification for the CancelFactor simprocs **)
   360 val simplify_one = Arith_Data.simplify_meta_eq  
   361   [@{thm mult_1_left}, @{thm mult_1_right}, @{thm div_1}, @{thm numeral_1_eq_Suc_0}];
   362 
   363 fun cancel_simplify_meta_eq ss cancel_th th =
   364     simplify_one ss (([th, cancel_th]) MRS trans);
   365 
   366 structure CancelFactorCommon =
   367   struct
   368   val mk_sum            = (fn T:typ => long_mk_prod)
   369   val dest_sum          = dest_prod
   370   val mk_coeff          = mk_coeff
   371   val dest_coeff        = dest_coeff
   372   val find_first        = find_first_t []
   373   fun trans_tac _       = Arith_Data.trans_tac
   374   val norm_ss = HOL_ss addsimps mult_1s @ @{thms mult_ac}
   375   fun norm_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss))
   376   val simplify_meta_eq  = cancel_simplify_meta_eq
   377   end;
   378 
   379 structure EqCancelFactor = ExtractCommonTermFun
   380  (open CancelFactorCommon
   381   val prove_conv = Arith_Data.prove_conv
   382   val mk_bal   = HOLogic.mk_eq
   383   val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT
   384   fun simp_conv _ _ = SOME @{thm nat_mult_eq_cancel_disj}
   385 );
   386 
   387 structure LessCancelFactor = ExtractCommonTermFun
   388  (open CancelFactorCommon
   389   val prove_conv = Arith_Data.prove_conv
   390   val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
   391   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT
   392   fun simp_conv _ _ = SOME @{thm nat_mult_less_cancel_disj}
   393 );
   394 
   395 structure LeCancelFactor = ExtractCommonTermFun
   396  (open CancelFactorCommon
   397   val prove_conv = Arith_Data.prove_conv
   398   val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
   399   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT
   400   fun simp_conv _ _ = SOME @{thm nat_mult_le_cancel_disj}
   401 );
   402 
   403 structure DivideCancelFactor = ExtractCommonTermFun
   404  (open CancelFactorCommon
   405   val prove_conv = Arith_Data.prove_conv
   406   val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
   407   val dest_bal = HOLogic.dest_bin @{const_name Divides.div} HOLogic.natT
   408   fun simp_conv _ _ = SOME @{thm nat_mult_div_cancel_disj}
   409 );
   410 
   411 structure DvdCancelFactor = ExtractCommonTermFun
   412  (open CancelFactorCommon
   413   val prove_conv = Arith_Data.prove_conv
   414   val mk_bal   = HOLogic.mk_binrel @{const_name Rings.dvd}
   415   val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} HOLogic.natT
   416   fun simp_conv _ _ = SOME @{thm nat_mult_dvd_cancel_disj}
   417 );
   418 
   419 val cancel_factor =
   420   map (Arith_Data.prep_simproc @{theory})
   421    [("nat_eq_cancel_factor",
   422      ["(l::nat) * m = n", "(l::nat) = m * n"],
   423      K EqCancelFactor.proc),
   424     ("nat_less_cancel_factor",
   425      ["(l::nat) * m < n", "(l::nat) < m * n"],
   426      K LessCancelFactor.proc),
   427     ("nat_le_cancel_factor",
   428      ["(l::nat) * m <= n", "(l::nat) <= m * n"],
   429      K LeCancelFactor.proc),
   430     ("nat_divide_cancel_factor",
   431      ["((l::nat) * m) div n", "(l::nat) div (m * n)"],
   432      K DivideCancelFactor.proc),
   433     ("nat_dvd_cancel_factor",
   434      ["((l::nat) * m) dvd n", "(l::nat) dvd (m * n)"],
   435      K DvdCancelFactor.proc)];
   436 
   437 end;
   438 
   439 
   440 Addsimprocs Nat_Numeral_Simprocs.cancel_numerals;
   441 Addsimprocs [Nat_Numeral_Simprocs.combine_numerals];
   442 Addsimprocs Nat_Numeral_Simprocs.cancel_numeral_factors;
   443 Addsimprocs Nat_Numeral_Simprocs.cancel_factor;
   444 
   445 
   446 (*examples:
   447 print_depth 22;
   448 set timing;
   449 set trace_simp;
   450 fun test s = (Goal s; by (Simp_tac 1));
   451 
   452 (*cancel_numerals*)
   453 test "l +( 2) + (2) + 2 + (l + 2) + (oo  + 2) = (uu::nat)";
   454 test "(2*length xs < 2*length xs + j)";
   455 test "(2*length xs < length xs * 2 + j)";
   456 test "2*u = (u::nat)";
   457 test "2*u = Suc (u)";
   458 test "(i + j + 12 + (k::nat)) - 15 = y";
   459 test "(i + j + 12 + (k::nat)) - 5 = y";
   460 test "Suc u - 2 = y";
   461 test "Suc (Suc (Suc u)) - 2 = y";
   462 test "(i + j + 2 + (k::nat)) - 1 = y";
   463 test "(i + j + 1 + (k::nat)) - 2 = y";
   464 
   465 test "(2*x + (u*v) + y) - v*3*u = (w::nat)";
   466 test "(2*x*u*v + 5 + (u*v)*4 + y) - v*u*4 = (w::nat)";
   467 test "(2*x*u*v + (u*v)*4 + y) - v*u = (w::nat)";
   468 test "Suc (Suc (2*x*u*v + u*4 + y)) - u = w";
   469 test "Suc ((u*v)*4) - v*3*u = w";
   470 test "Suc (Suc ((u*v)*3)) - v*3*u = w";
   471 
   472 test "(i + j + 12 + (k::nat)) = u + 15 + y";
   473 test "(i + j + 32 + (k::nat)) - (u + 15 + y) = zz";
   474 test "(i + j + 12 + (k::nat)) = u + 5 + y";
   475 (*Suc*)
   476 test "(i + j + 12 + k) = Suc (u + y)";
   477 test "Suc (Suc (Suc (Suc (Suc (u + y))))) <= ((i + j) + 41 + k)";
   478 test "(i + j + 5 + k) < Suc (Suc (Suc (Suc (Suc (u + y)))))";
   479 test "Suc (Suc (Suc (Suc (Suc (u + y))))) - 5 = v";
   480 test "(i + j + 5 + k) = Suc (Suc (Suc (Suc (Suc (Suc (Suc (u + y)))))))";
   481 test "2*y + 3*z + 2*u = Suc (u)";
   482 test "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = Suc (u)";
   483 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)";
   484 test "6 + 2*y + 3*z + 4*u = Suc (vv + 2*u + z)";
   485 test "(2*n*m) < (3*(m*n)) + (u::nat)";
   486 
   487 test "(Suc (Suc (Suc (Suc (Suc (Suc (case length (f c) of 0 => 0 | Suc k => k)))))) <= Suc 0)";
   488  
   489 test "Suc (Suc (Suc (Suc (Suc (Suc (length l1 + length l2)))))) <= length l1";
   490 
   491 test "( (Suc (Suc (Suc (Suc (Suc (length (compT P E A ST mxr e) + length l3)))))) <= length (compT P E A ST mxr e))";
   492 
   493 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))";
   494 
   495 
   496 (*negative numerals: FAIL*)
   497 test "(i + j + -23 + (k::nat)) < u + 15 + y";
   498 test "(i + j + 3 + (k::nat)) < u + -15 + y";
   499 test "(i + j + -12 + (k::nat)) - 15 = y";
   500 test "(i + j + 12 + (k::nat)) - -15 = y";
   501 test "(i + j + -12 + (k::nat)) - -15 = y";
   502 
   503 (*combine_numerals*)
   504 test "k + 3*k = (u::nat)";
   505 test "Suc (i + 3) = u";
   506 test "Suc (i + j + 3 + k) = u";
   507 test "k + j + 3*k + j = (u::nat)";
   508 test "Suc (j*i + i + k + 5 + 3*k + i*j*4) = (u::nat)";
   509 test "(2*n*m) + (3*(m*n)) = (u::nat)";
   510 (*negative numerals: FAIL*)
   511 test "Suc (i + j + -3 + k) = u";
   512 
   513 (*cancel_numeral_factors*)
   514 test "9*x = 12 * (y::nat)";
   515 test "(9*x) div (12 * (y::nat)) = z";
   516 test "9*x < 12 * (y::nat)";
   517 test "9*x <= 12 * (y::nat)";
   518 
   519 (*cancel_factor*)
   520 test "x*k = k*(y::nat)";
   521 test "k = k*(y::nat)";
   522 test "a*(b*c) = (b::nat)";
   523 test "a*(b*c) = d*(b::nat)*(x*a)";
   524 
   525 test "x*k < k*(y::nat)";
   526 test "k < k*(y::nat)";
   527 test "a*(b*c) < (b::nat)";
   528 test "a*(b*c) < d*(b::nat)*(x*a)";
   529 
   530 test "x*k <= k*(y::nat)";
   531 test "k <= k*(y::nat)";
   532 test "a*(b*c) <= (b::nat)";
   533 test "a*(b*c) <= d*(b::nat)*(x*a)";
   534 
   535 test "(x*k) div (k*(y::nat)) = (uu::nat)";
   536 test "(k) div (k*(y::nat)) = (uu::nat)";
   537 test "(a*(b*c)) div ((b::nat)) = (uu::nat)";
   538 test "(a*(b*c)) div (d*(b::nat)*(x*a)) = (uu::nat)";
   539 *)