src/ZF/int_arith.ML
changeset 23146 0bc590051d95
child 24630 351a308ab58d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/int_arith.ML	Thu May 31 12:06:31 2007 +0200
     1.3 @@ -0,0 +1,443 @@
     1.4 +(*  Title:      ZF/int_arith.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Larry Paulson
     1.7 +    Copyright   2000  University of Cambridge
     1.8 +
     1.9 +Simprocs for linear arithmetic.
    1.10 +*)
    1.11 +
    1.12 +
    1.13 +(** To simplify inequalities involving integer negation and literals,
    1.14 +    such as -x = #3
    1.15 +**)
    1.16 +
    1.17 +Addsimps [inst "y" "integ_of(?w)" zminus_equation,
    1.18 +          inst "x" "integ_of(?w)" equation_zminus];
    1.19 +
    1.20 +AddIffs [inst "y" "integ_of(?w)" zminus_zless,
    1.21 +         inst "x" "integ_of(?w)" zless_zminus];
    1.22 +
    1.23 +AddIffs [inst "y" "integ_of(?w)" zminus_zle,
    1.24 +         inst "x" "integ_of(?w)" zle_zminus];
    1.25 +
    1.26 +Addsimps [inst "s" "integ_of(?w)" (thm "Let_def")];
    1.27 +
    1.28 +(*** Simprocs for numeric literals ***)
    1.29 +
    1.30 +(** Combining of literal coefficients in sums of products **)
    1.31 +
    1.32 +Goal "(x $< y) <-> (x$-y $< #0)";
    1.33 +by (simp_tac (simpset() addsimps zcompare_rls) 1);
    1.34 +qed "zless_iff_zdiff_zless_0";
    1.35 +
    1.36 +Goal "[| x: int; y: int |] ==> (x = y) <-> (x$-y = #0)";
    1.37 +by (asm_simp_tac (simpset() addsimps zcompare_rls) 1);
    1.38 +qed "eq_iff_zdiff_eq_0";
    1.39 +
    1.40 +Goal "(x $<= y) <-> (x$-y $<= #0)";
    1.41 +by (asm_simp_tac (simpset() addsimps zcompare_rls) 1);
    1.42 +qed "zle_iff_zdiff_zle_0";
    1.43 +
    1.44 +
    1.45 +(** For combine_numerals **)
    1.46 +
    1.47 +Goal "i$*u $+ (j$*u $+ k) = (i$+j)$*u $+ k";
    1.48 +by (simp_tac (simpset() addsimps [zadd_zmult_distrib]@zadd_ac) 1);
    1.49 +qed "left_zadd_zmult_distrib";
    1.50 +
    1.51 +
    1.52 +(** For cancel_numerals **)
    1.53 +
    1.54 +val rel_iff_rel_0_rls = map (inst "y" "?u$+?v")
    1.55 +                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
    1.56 +                           zle_iff_zdiff_zle_0] @
    1.57 +                        map (inst "y" "n")
    1.58 +                          [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
    1.59 +                           zle_iff_zdiff_zle_0];
    1.60 +
    1.61 +Goal "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))";
    1.62 +by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
    1.63 +by (simp_tac (simpset() addsimps zcompare_rls) 1);
    1.64 +by (simp_tac (simpset() addsimps zadd_ac) 1);
    1.65 +qed "eq_add_iff1";
    1.66 +
    1.67 +Goal "(i$*u $+ m = j$*u $+ n) <-> (intify(m) = (j$-i)$*u $+ n)";
    1.68 +by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
    1.69 +by (simp_tac (simpset() addsimps zcompare_rls) 1);
    1.70 +by (simp_tac (simpset() addsimps zadd_ac) 1);
    1.71 +qed "eq_add_iff2";
    1.72 +
    1.73 +Goal "(i$*u $+ m $< j$*u $+ n) <-> ((i$-j)$*u $+ m $< n)";
    1.74 +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
    1.75 +                                     zadd_ac@rel_iff_rel_0_rls) 1);
    1.76 +qed "less_add_iff1";
    1.77 +
    1.78 +Goal "(i$*u $+ m $< j$*u $+ n) <-> (m $< (j$-i)$*u $+ n)";
    1.79 +by (asm_simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]@
    1.80 +                                     zadd_ac@rel_iff_rel_0_rls) 1);
    1.81 +qed "less_add_iff2";
    1.82 +
    1.83 +Goal "(i$*u $+ m $<= j$*u $+ n) <-> ((i$-j)$*u $+ m $<= n)";
    1.84 +by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
    1.85 +by (simp_tac (simpset() addsimps zcompare_rls) 1);
    1.86 +by (simp_tac (simpset() addsimps zadd_ac) 1);
    1.87 +qed "le_add_iff1";
    1.88 +
    1.89 +Goal "(i$*u $+ m $<= j$*u $+ n) <-> (m $<= (j$-i)$*u $+ n)";
    1.90 +by (simp_tac (simpset() addsimps [zdiff_def, zadd_zmult_distrib]) 1);
    1.91 +by (simp_tac (simpset() addsimps zcompare_rls) 1);
    1.92 +by (simp_tac (simpset() addsimps zadd_ac) 1);
    1.93 +qed "le_add_iff2";
    1.94 +
    1.95 +
    1.96 +structure Int_Numeral_Simprocs =
    1.97 +struct
    1.98 +
    1.99 +(*Utilities*)
   1.100 +
   1.101 +val integ_of_const = Const ("Bin.integ_of", iT --> iT);
   1.102 +
   1.103 +fun mk_numeral n = integ_of_const $ NumeralSyntax.mk_bin n;
   1.104 +
   1.105 +(*Decodes a binary INTEGER*)
   1.106 +fun dest_numeral (Const("Bin.integ_of", _) $ w) =
   1.107 +     (NumeralSyntax.dest_bin w
   1.108 +      handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
   1.109 +  | dest_numeral t =  raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
   1.110 +
   1.111 +fun find_first_numeral past (t::terms) =
   1.112 +        ((dest_numeral t, rev past @ terms)
   1.113 +         handle TERM _ => find_first_numeral (t::past) terms)
   1.114 +  | find_first_numeral past [] = raise TERM("find_first_numeral", []);
   1.115 +
   1.116 +val zero = mk_numeral 0;
   1.117 +val mk_plus = FOLogic.mk_binop "Int.zadd";
   1.118 +
   1.119 +val iT = Ind_Syntax.iT;
   1.120 +
   1.121 +val zminus_const = Const ("Int.zminus", iT --> iT);
   1.122 +
   1.123 +(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
   1.124 +fun mk_sum []        = zero
   1.125 +  | mk_sum [t,u]     = mk_plus (t, u)
   1.126 +  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   1.127 +
   1.128 +(*this version ALWAYS includes a trailing zero*)
   1.129 +fun long_mk_sum []        = zero
   1.130 +  | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   1.131 +
   1.132 +val dest_plus = FOLogic.dest_bin "Int.zadd" iT;
   1.133 +
   1.134 +(*decompose additions AND subtractions as a sum*)
   1.135 +fun dest_summing (pos, Const ("Int.zadd", _) $ t $ u, ts) =
   1.136 +        dest_summing (pos, t, dest_summing (pos, u, ts))
   1.137 +  | dest_summing (pos, Const ("Int.zdiff", _) $ t $ u, ts) =
   1.138 +        dest_summing (pos, t, dest_summing (not pos, u, ts))
   1.139 +  | dest_summing (pos, t, ts) =
   1.140 +        if pos then t::ts else zminus_const$t :: ts;
   1.141 +
   1.142 +fun dest_sum t = dest_summing (true, t, []);
   1.143 +
   1.144 +val mk_diff = FOLogic.mk_binop "Int.zdiff";
   1.145 +val dest_diff = FOLogic.dest_bin "Int.zdiff" iT;
   1.146 +
   1.147 +val one = mk_numeral 1;
   1.148 +val mk_times = FOLogic.mk_binop "Int.zmult";
   1.149 +
   1.150 +fun mk_prod [] = one
   1.151 +  | mk_prod [t] = t
   1.152 +  | mk_prod (t :: ts) = if t = one then mk_prod ts
   1.153 +                        else mk_times (t, mk_prod ts);
   1.154 +
   1.155 +val dest_times = FOLogic.dest_bin "Int.zmult" iT;
   1.156 +
   1.157 +fun dest_prod t =
   1.158 +      let val (t,u) = dest_times t
   1.159 +      in  dest_prod t @ dest_prod u  end
   1.160 +      handle TERM _ => [t];
   1.161 +
   1.162 +(*DON'T do the obvious simplifications; that would create special cases*)
   1.163 +fun mk_coeff (k, t) = mk_times (mk_numeral k, t);
   1.164 +
   1.165 +(*Express t as a product of (possibly) a numeral with other sorted terms*)
   1.166 +fun dest_coeff sign (Const ("Int.zminus", _) $ t) = dest_coeff (~sign) t
   1.167 +  | dest_coeff sign t =
   1.168 +    let val ts = sort Term.term_ord (dest_prod t)
   1.169 +        val (n, ts') = find_first_numeral [] ts
   1.170 +                          handle TERM _ => (1, ts)
   1.171 +    in (sign*n, mk_prod ts') end;
   1.172 +
   1.173 +(*Find first coefficient-term THAT MATCHES u*)
   1.174 +fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
   1.175 +  | find_first_coeff past u (t::terms) =
   1.176 +        let val (n,u') = dest_coeff 1 t
   1.177 +        in  if u aconv u' then (n, rev past @ terms)
   1.178 +                          else find_first_coeff (t::past) u terms
   1.179 +        end
   1.180 +        handle TERM _ => find_first_coeff (t::past) u terms;
   1.181 +
   1.182 +
   1.183 +(*Simplify #1*n and n*#1 to n*)
   1.184 +val add_0s = [zadd_0_intify, zadd_0_right_intify];
   1.185 +
   1.186 +val mult_1s = [zmult_1_intify, zmult_1_right_intify,
   1.187 +               zmult_minus1, zmult_minus1_right];
   1.188 +
   1.189 +val tc_rules = [integ_of_type, intify_in_int,
   1.190 +                int_of_type, zadd_type, zdiff_type, zmult_type] @ 
   1.191 +               thms "bin.intros";
   1.192 +val intifys = [intify_ident, zadd_intify1, zadd_intify2,
   1.193 +               zdiff_intify1, zdiff_intify2, zmult_intify1, zmult_intify2,
   1.194 +               zless_intify1, zless_intify2, zle_intify1, zle_intify2];
   1.195 +
   1.196 +(*To perform binary arithmetic*)
   1.197 +val bin_simps = [add_integ_of_left] @ bin_arith_simps @ bin_rel_simps;
   1.198 +
   1.199 +(*To evaluate binary negations of coefficients*)
   1.200 +val zminus_simps = NCons_simps @
   1.201 +                   [integ_of_minus RS sym,
   1.202 +                    bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,
   1.203 +                    bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];
   1.204 +
   1.205 +(*To let us treat subtraction as addition*)
   1.206 +val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus];
   1.207 +
   1.208 +(*push the unary minus down: - x * y = x * - y *)
   1.209 +val int_minus_mult_eq_1_to_2 =
   1.210 +    [zmult_zminus, zmult_zminus_right RS sym] MRS trans |> standard;
   1.211 +
   1.212 +(*to extract again any uncancelled minuses*)
   1.213 +val int_minus_from_mult_simps =
   1.214 +    [zminus_zminus, zmult_zminus, zmult_zminus_right];
   1.215 +
   1.216 +(*combine unary minus with numeric literals, however nested within a product*)
   1.217 +val int_mult_minus_simps =
   1.218 +    [zmult_assoc, zmult_zminus RS sym, int_minus_mult_eq_1_to_2];
   1.219 +
   1.220 +fun prep_simproc (name, pats, proc) =
   1.221 +  Simplifier.simproc (the_context ()) name pats proc;
   1.222 +
   1.223 +structure CancelNumeralsCommon =
   1.224 +  struct
   1.225 +  val mk_sum            = (fn T:typ => mk_sum)
   1.226 +  val dest_sum          = dest_sum
   1.227 +  val mk_coeff          = mk_coeff
   1.228 +  val dest_coeff        = dest_coeff 1
   1.229 +  val find_first_coeff  = find_first_coeff []
   1.230 +  fun trans_tac _       = ArithData.gen_trans_tac iff_trans
   1.231 +
   1.232 +  val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ zadd_ac
   1.233 +  val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
   1.234 +  val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ zadd_ac @ zmult_ac @ tc_rules @ intifys
   1.235 +  fun norm_tac ss =
   1.236 +    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
   1.237 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
   1.238 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3))
   1.239 +
   1.240 +  val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys
   1.241 +  fun numeral_simp_tac ss =
   1.242 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   1.243 +    THEN ALLGOALS (SIMPSET' (fn simpset => asm_simp_tac (Simplifier.inherit_context ss simpset)))
   1.244 +  val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
   1.245 +  end;
   1.246 +
   1.247 +
   1.248 +structure EqCancelNumerals = CancelNumeralsFun
   1.249 + (open CancelNumeralsCommon
   1.250 +  val prove_conv = ArithData.prove_conv "inteq_cancel_numerals"
   1.251 +  val mk_bal   = FOLogic.mk_eq
   1.252 +  val dest_bal = FOLogic.dest_eq
   1.253 +  val bal_add1 = eq_add_iff1 RS iff_trans
   1.254 +  val bal_add2 = eq_add_iff2 RS iff_trans
   1.255 +);
   1.256 +
   1.257 +structure LessCancelNumerals = CancelNumeralsFun
   1.258 + (open CancelNumeralsCommon
   1.259 +  val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
   1.260 +  val mk_bal   = FOLogic.mk_binrel "Int.zless"
   1.261 +  val dest_bal = FOLogic.dest_bin "Int.zless" iT
   1.262 +  val bal_add1 = less_add_iff1 RS iff_trans
   1.263 +  val bal_add2 = less_add_iff2 RS iff_trans
   1.264 +);
   1.265 +
   1.266 +structure LeCancelNumerals = CancelNumeralsFun
   1.267 + (open CancelNumeralsCommon
   1.268 +  val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
   1.269 +  val mk_bal   = FOLogic.mk_binrel "Int.zle"
   1.270 +  val dest_bal = FOLogic.dest_bin "Int.zle" iT
   1.271 +  val bal_add1 = le_add_iff1 RS iff_trans
   1.272 +  val bal_add2 = le_add_iff2 RS iff_trans
   1.273 +);
   1.274 +
   1.275 +val cancel_numerals =
   1.276 +  map prep_simproc
   1.277 +   [("inteq_cancel_numerals",
   1.278 +     ["l $+ m = n", "l = m $+ n",
   1.279 +      "l $- m = n", "l = m $- n",
   1.280 +      "l $* m = n", "l = m $* n"],
   1.281 +     K EqCancelNumerals.proc),
   1.282 +    ("intless_cancel_numerals",
   1.283 +     ["l $+ m $< n", "l $< m $+ n",
   1.284 +      "l $- m $< n", "l $< m $- n",
   1.285 +      "l $* m $< n", "l $< m $* n"],
   1.286 +     K LessCancelNumerals.proc),
   1.287 +    ("intle_cancel_numerals",
   1.288 +     ["l $+ m $<= n", "l $<= m $+ n",
   1.289 +      "l $- m $<= n", "l $<= m $- n",
   1.290 +      "l $* m $<= n", "l $<= m $* n"],
   1.291 +     K LeCancelNumerals.proc)];
   1.292 +
   1.293 +
   1.294 +(*version without the hyps argument*)
   1.295 +fun prove_conv_nohyps name tacs sg = ArithData.prove_conv name tacs sg [];
   1.296 +
   1.297 +structure CombineNumeralsData =
   1.298 +  struct
   1.299 +  type coeff            = IntInf.int
   1.300 +  val iszero            = (fn x : IntInf.int => x = 0)
   1.301 +  val add               = IntInf.+ 
   1.302 +  val mk_sum            = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
   1.303 +  val dest_sum          = dest_sum
   1.304 +  val mk_coeff          = mk_coeff
   1.305 +  val dest_coeff        = dest_coeff 1
   1.306 +  val left_distrib      = left_zadd_zmult_distrib RS trans
   1.307 +  val prove_conv        = prove_conv_nohyps "int_combine_numerals"
   1.308 +  fun trans_tac _       = ArithData.gen_trans_tac trans
   1.309 +
   1.310 +  val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ zadd_ac @ intifys
   1.311 +  val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
   1.312 +  val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ zadd_ac @ zmult_ac @ tc_rules @ intifys
   1.313 +  fun norm_tac ss =
   1.314 +    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
   1.315 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
   1.316 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3))
   1.317 +
   1.318 +  val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys
   1.319 +  fun numeral_simp_tac ss =
   1.320 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   1.321 +  val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
   1.322 +  end;
   1.323 +
   1.324 +structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   1.325 +
   1.326 +val combine_numerals =
   1.327 +  prep_simproc ("int_combine_numerals", ["i $+ j", "i $- j"], K CombineNumerals.proc);
   1.328 +
   1.329 +
   1.330 +
   1.331 +(** Constant folding for integer multiplication **)
   1.332 +
   1.333 +(*The trick is to regard products as sums, e.g. #3 $* x $* #4 as
   1.334 +  the "sum" of #3, x, #4; the literals are then multiplied*)
   1.335 +
   1.336 +
   1.337 +structure CombineNumeralsProdData =
   1.338 +  struct
   1.339 +  type coeff            = IntInf.int
   1.340 +  val iszero            = (fn x : IntInf.int => x = 0)
   1.341 +  val add               = IntInf.*
   1.342 +  val mk_sum            = (fn T:typ => mk_prod)
   1.343 +  val dest_sum          = dest_prod
   1.344 +  fun mk_coeff(k,t) = if t=one then mk_numeral k
   1.345 +                      else raise TERM("mk_coeff", [])
   1.346 +  fun dest_coeff t = (dest_numeral t, one)  (*We ONLY want pure numerals.*)
   1.347 +  val left_distrib      = zmult_assoc RS sym RS trans
   1.348 +  val prove_conv        = prove_conv_nohyps "int_combine_numerals_prod"
   1.349 +  fun trans_tac _       = ArithData.gen_trans_tac trans
   1.350 +
   1.351 +
   1.352 +
   1.353 +val norm_ss1 = ZF_ss addsimps mult_1s @ diff_simps @ zminus_simps
   1.354 +  val norm_ss2 = ZF_ss addsimps [zmult_zminus_right RS sym] @
   1.355 +    bin_simps @ zmult_ac @ tc_rules @ intifys
   1.356 +  fun norm_tac ss =
   1.357 +    ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
   1.358 +    THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
   1.359 +
   1.360 +  val numeral_simp_ss = ZF_ss addsimps bin_simps @ tc_rules @ intifys
   1.361 +  fun numeral_simp_tac ss =
   1.362 +    ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   1.363 +  val simplify_meta_eq  = ArithData.simplify_meta_eq (mult_1s);
   1.364 +  end;
   1.365 +
   1.366 +
   1.367 +structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData);
   1.368 +
   1.369 +val combine_numerals_prod =
   1.370 +  prep_simproc ("int_combine_numerals_prod", ["i $* j"], K CombineNumeralsProd.proc);
   1.371 +
   1.372 +end;
   1.373 +
   1.374 +
   1.375 +Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
   1.376 +Addsimprocs [Int_Numeral_Simprocs.combine_numerals,
   1.377 +             Int_Numeral_Simprocs.combine_numerals_prod];
   1.378 +
   1.379 +
   1.380 +(*examples:*)
   1.381 +(*
   1.382 +print_depth 22;
   1.383 +set timing;
   1.384 +set trace_simp;
   1.385 +fun test s = (Goal s; by (Asm_simp_tac 1));
   1.386 +val sg = #sign (rep_thm (topthm()));
   1.387 +val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1));
   1.388 +val (t,_) = FOLogic.dest_eq t;
   1.389 +
   1.390 +(*combine_numerals_prod (products of separate literals) *)
   1.391 +test "#5 $* x $* #3 = y";
   1.392 +
   1.393 +test "y2 $+ ?x42 = y $+ y2";
   1.394 +
   1.395 +test "oo : int ==> l $+ (l $+ #2) $+ oo = oo";
   1.396 +
   1.397 +test "#9$*x $+ y = x$*#23 $+ z";
   1.398 +test "y $+ x = x $+ z";
   1.399 +
   1.400 +test "x : int ==> x $+ y $+ z = x $+ z";
   1.401 +test "x : int ==> y $+ (z $+ x) = z $+ x";
   1.402 +test "z : int ==> x $+ y $+ z = (z $+ y) $+ (x $+ w)";
   1.403 +test "z : int ==> x$*y $+ z = (z $+ y) $+ (y$*x $+ w)";
   1.404 +
   1.405 +test "#-3 $* x $+ y $<= x $* #2 $+ z";
   1.406 +test "y $+ x $<= x $+ z";
   1.407 +test "x $+ y $+ z $<= x $+ z";
   1.408 +
   1.409 +test "y $+ (z $+ x) $< z $+ x";
   1.410 +test "x $+ y $+ z $< (z $+ y) $+ (x $+ w)";
   1.411 +test "x$*y $+ z $< (z $+ y) $+ (y$*x $+ w)";
   1.412 +
   1.413 +test "l $+ #2 $+ #2 $+ #2 $+ (l $+ #2) $+ (oo $+ #2) = uu";
   1.414 +test "u : int ==> #2 $* u = u";
   1.415 +test "(i $+ j $+ #12 $+ k) $- #15 = y";
   1.416 +test "(i $+ j $+ #12 $+ k) $- #5 = y";
   1.417 +
   1.418 +test "y $- b $< b";
   1.419 +test "y $- (#3 $* b $+ c) $< b $- #2 $* c";
   1.420 +
   1.421 +test "(#2 $* x $- (u $* v) $+ y) $- v $* #3 $* u = w";
   1.422 +test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u $* #4 = w";
   1.423 +test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u = w";
   1.424 +test "u $* v $- (x $* u $* v $+ (u $* v) $* #4 $+ y) = w";
   1.425 +
   1.426 +test "(i $+ j $+ #12 $+ k) = u $+ #15 $+ y";
   1.427 +test "(i $+ j $* #2 $+ #12 $+ k) = j $+ #5 $+ y";
   1.428 +
   1.429 +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";
   1.430 +
   1.431 +test "a $+ $-(b$+c) $+ b = d";
   1.432 +test "a $+ $-(b$+c) $- b = d";
   1.433 +
   1.434 +(*negative numerals*)
   1.435 +test "(i $+ j $+ #-2 $+ k) $- (u $+ #5 $+ y) = zz";
   1.436 +test "(i $+ j $+ #-3 $+ k) $< u $+ #5 $+ y";
   1.437 +test "(i $+ j $+ #3 $+ k) $< u $+ #-6 $+ y";
   1.438 +test "(i $+ j $+ #-12 $+ k) $- #15 = y";
   1.439 +test "(i $+ j $+ #12 $+ k) $- #-15 = y";
   1.440 +test "(i $+ j $+ #-12 $+ k) $- #-15 = y";
   1.441 +
   1.442 +(*Multiplying separated numerals*)
   1.443 +Goal "#6 $* ($# x $* #2) =  uu";
   1.444 +Goal "#4 $* ($# x $* $# x) $* (#2 $* $# x) =  uu";
   1.445 +*)
   1.446 +