src/ZF/int_arith.ML
author wenzelm
Sun Oct 07 21:19:31 2007 +0200 (2007-10-07)
changeset 24893 b8ef7afe3a6b
parent 24630 351a308ab58d
child 26056 6a0801279f4c
permissions -rw-r--r--
modernized specifications;
removed legacy ML bindings;
     1 (*  Title:      ZF/int_arith.ML
     2     ID:         $Id$
     3     Author:     Larry Paulson
     4     Copyright   2000  University of Cambridge
     5 
     6 Simprocs for linear arithmetic.
     7 *)
     8 
     9 
    10 (** To simplify inequalities involving integer negation and literals,
    11     such as -x = #3
    12 **)
    13 
    14 Addsimps [inst "y" "integ_of(?w)" @{thm zminus_equation},
    15           inst "x" "integ_of(?w)" @{thm equation_zminus}];
    16 
    17 AddIffs [inst "y" "integ_of(?w)" @{thm zminus_zless},
    18          inst "x" "integ_of(?w)" @{thm zless_zminus}];
    19 
    20 AddIffs [inst "y" "integ_of(?w)" @{thm zminus_zle},
    21          inst "x" "integ_of(?w)" @{thm zle_zminus}];
    22 
    23 Addsimps [inst "s" "integ_of(?w)" @{thm Let_def}];
    24 
    25 (*** Simprocs for numeric literals ***)
    26 
    27 (** Combining of literal coefficients in sums of products **)
    28 
    29 Goal "(x $< y) <-> (x$-y $< #0)";
    30 by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
    31 qed "zless_iff_zdiff_zless_0";
    32 
    33 Goal "[| x: int; y: int |] ==> (x = y) <-> (x$-y = #0)";
    34 by (asm_simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
    35 qed "eq_iff_zdiff_eq_0";
    36 
    37 Goal "(x $<= y) <-> (x$-y $<= #0)";
    38 by (asm_simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
    39 qed "zle_iff_zdiff_zle_0";
    40 
    41 
    42 (** For combine_numerals **)
    43 
    44 Goal "i$*u $+ (j$*u $+ k) = (i$+j)$*u $+ k";
    45 by (simp_tac (simpset() addsimps [@{thm zadd_zmult_distrib}]@ @{thms zadd_ac}) 1);
    46 qed "left_zadd_zmult_distrib";
    47 
    48 
    49 (** For cancel_numerals **)
    50 
    51 val rel_iff_rel_0_rls = map (inst "y" "?u$+?v")
    52                           [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
    53                            zle_iff_zdiff_zle_0] @
    54                         map (inst "y" "n")
    55                           [zless_iff_zdiff_zless_0, eq_iff_zdiff_eq_0,
    56                            zle_iff_zdiff_zle_0];
    57 
    58 Goal "(i$*u $+ m = j$*u $+ n) <-> ((i$-j)$*u $+ m = intify(n))";
    59 by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1);
    60 by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
    61 by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1);
    62 qed "eq_add_iff1";
    63 
    64 Goal "(i$*u $+ m = j$*u $+ n) <-> (intify(m) = (j$-i)$*u $+ n)";
    65 by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1);
    66 by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
    67 by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1);
    68 qed "eq_add_iff2";
    69 
    70 Goal "(i$*u $+ m $< j$*u $+ n) <-> ((i$-j)$*u $+ m $< n)";
    71 by (asm_simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]@
    72                                      @{thms zadd_ac} @ rel_iff_rel_0_rls) 1);
    73 qed "less_add_iff1";
    74 
    75 Goal "(i$*u $+ m $< j$*u $+ n) <-> (m $< (j$-i)$*u $+ n)";
    76 by (asm_simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]@
    77                                      @{thms zadd_ac} @ rel_iff_rel_0_rls) 1);
    78 qed "less_add_iff2";
    79 
    80 Goal "(i$*u $+ m $<= j$*u $+ n) <-> ((i$-j)$*u $+ m $<= n)";
    81 by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1);
    82 by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
    83 by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1);
    84 qed "le_add_iff1";
    85 
    86 Goal "(i$*u $+ m $<= j$*u $+ n) <-> (m $<= (j$-i)$*u $+ n)";
    87 by (simp_tac (simpset() addsimps [@{thm zdiff_def}, @{thm zadd_zmult_distrib}]) 1);
    88 by (simp_tac (simpset() addsimps @{thms zcompare_rls}) 1);
    89 by (simp_tac (simpset() addsimps @{thms zadd_ac}) 1);
    90 qed "le_add_iff2";
    91 
    92 
    93 structure Int_Numeral_Simprocs =
    94 struct
    95 
    96 (*Utilities*)
    97 
    98 val integ_of_const = Const ("Bin.integ_of", iT --> iT);
    99 
   100 fun mk_numeral n = integ_of_const $ NumeralSyntax.mk_bin n;
   101 
   102 (*Decodes a binary INTEGER*)
   103 fun dest_numeral (Const("Bin.integ_of", _) $ w) =
   104      (NumeralSyntax.dest_bin w
   105       handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
   106   | dest_numeral t =  raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
   107 
   108 fun find_first_numeral past (t::terms) =
   109         ((dest_numeral t, rev past @ terms)
   110          handle TERM _ => find_first_numeral (t::past) terms)
   111   | find_first_numeral past [] = raise TERM("find_first_numeral", []);
   112 
   113 val zero = mk_numeral 0;
   114 val mk_plus = FOLogic.mk_binop "Int.zadd";
   115 
   116 val iT = Ind_Syntax.iT;
   117 
   118 val zminus_const = Const ("Int.zminus", iT --> iT);
   119 
   120 (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
   121 fun mk_sum []        = zero
   122   | mk_sum [t,u]     = mk_plus (t, u)
   123   | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   124 
   125 (*this version ALWAYS includes a trailing zero*)
   126 fun long_mk_sum []        = zero
   127   | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
   128 
   129 val dest_plus = FOLogic.dest_bin "Int.zadd" iT;
   130 
   131 (*decompose additions AND subtractions as a sum*)
   132 fun dest_summing (pos, Const ("Int.zadd", _) $ t $ u, ts) =
   133         dest_summing (pos, t, dest_summing (pos, u, ts))
   134   | dest_summing (pos, Const ("Int.zdiff", _) $ t $ u, ts) =
   135         dest_summing (pos, t, dest_summing (not pos, u, ts))
   136   | dest_summing (pos, t, ts) =
   137         if pos then t::ts else zminus_const$t :: ts;
   138 
   139 fun dest_sum t = dest_summing (true, t, []);
   140 
   141 val mk_diff = FOLogic.mk_binop "Int.zdiff";
   142 val dest_diff = FOLogic.dest_bin "Int.zdiff" iT;
   143 
   144 val one = mk_numeral 1;
   145 val mk_times = FOLogic.mk_binop "Int.zmult";
   146 
   147 fun mk_prod [] = one
   148   | mk_prod [t] = t
   149   | mk_prod (t :: ts) = if t = one then mk_prod ts
   150                         else mk_times (t, mk_prod ts);
   151 
   152 val dest_times = FOLogic.dest_bin "Int.zmult" iT;
   153 
   154 fun dest_prod t =
   155       let val (t,u) = dest_times t
   156       in  dest_prod t @ dest_prod u  end
   157       handle TERM _ => [t];
   158 
   159 (*DON'T do the obvious simplifications; that would create special cases*)
   160 fun mk_coeff (k, t) = mk_times (mk_numeral k, t);
   161 
   162 (*Express t as a product of (possibly) a numeral with other sorted terms*)
   163 fun dest_coeff sign (Const ("Int.zminus", _) $ t) = dest_coeff (~sign) t
   164   | dest_coeff sign t =
   165     let val ts = sort Term.term_ord (dest_prod t)
   166         val (n, ts') = find_first_numeral [] ts
   167                           handle TERM _ => (1, ts)
   168     in (sign*n, mk_prod ts') end;
   169 
   170 (*Find first coefficient-term THAT MATCHES u*)
   171 fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
   172   | find_first_coeff past u (t::terms) =
   173         let val (n,u') = dest_coeff 1 t
   174         in  if u aconv u' then (n, rev past @ terms)
   175                           else find_first_coeff (t::past) u terms
   176         end
   177         handle TERM _ => find_first_coeff (t::past) u terms;
   178 
   179 
   180 (*Simplify #1*n and n*#1 to n*)
   181 val add_0s = [@{thm zadd_0_intify}, @{thm zadd_0_right_intify}];
   182 
   183 val mult_1s = [@{thm zmult_1_intify}, @{thm zmult_1_right_intify},
   184                @{thm zmult_minus1}, @{thm zmult_minus1_right}];
   185 
   186 val tc_rules = [@{thm integ_of_type}, @{thm intify_in_int},
   187                 @{thm int_of_type}, @{thm zadd_type}, @{thm zdiff_type}, @{thm zmult_type}] @ 
   188                @{thms bin.intros};
   189 val intifys = [@{thm intify_ident}, @{thm zadd_intify1}, @{thm zadd_intify2},
   190                @{thm zdiff_intify1}, @{thm zdiff_intify2}, @{thm zmult_intify1}, @{thm zmult_intify2},
   191                @{thm zless_intify1}, @{thm zless_intify2}, @{thm zle_intify1}, @{thm zle_intify2}];
   192 
   193 (*To perform binary arithmetic*)
   194 val bin_simps = [@{thm add_integ_of_left}] @ @{thms bin_arith_simps} @ @{thms bin_rel_simps};
   195 
   196 (*To evaluate binary negations of coefficients*)
   197 val zminus_simps = @{thms NCons_simps} @
   198                    [@{thm integ_of_minus} RS sym,
   199                     @{thm bin_minus_1}, @{thm bin_minus_0}, @{thm bin_minus_Pls}, @{thm bin_minus_Min},
   200                     @{thm bin_pred_1}, @{thm bin_pred_0}, @{thm bin_pred_Pls}, @{thm bin_pred_Min}];
   201 
   202 (*To let us treat subtraction as addition*)
   203 val diff_simps = [@{thm zdiff_def}, @{thm zminus_zadd_distrib}, @{thm zminus_zminus}];
   204 
   205 (*push the unary minus down: - x * y = x * - y *)
   206 val int_minus_mult_eq_1_to_2 =
   207     [@{thm zmult_zminus}, @{thm zmult_zminus_right} RS sym] MRS trans |> standard;
   208 
   209 (*to extract again any uncancelled minuses*)
   210 val int_minus_from_mult_simps =
   211     [@{thm zminus_zminus}, @{thm zmult_zminus}, @{thm zmult_zminus_right}];
   212 
   213 (*combine unary minus with numeric literals, however nested within a product*)
   214 val int_mult_minus_simps =
   215     [@{thm zmult_assoc}, @{thm zmult_zminus} RS sym, int_minus_mult_eq_1_to_2];
   216 
   217 fun prep_simproc (name, pats, proc) =
   218   Simplifier.simproc (the_context ()) name pats proc;
   219 
   220 structure CancelNumeralsCommon =
   221   struct
   222   val mk_sum            = (fn T:typ => mk_sum)
   223   val dest_sum          = dest_sum
   224   val mk_coeff          = mk_coeff
   225   val dest_coeff        = dest_coeff 1
   226   val find_first_coeff  = find_first_coeff []
   227   fun trans_tac _       = ArithData.gen_trans_tac iff_trans
   228 
   229   val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac}
   230   val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
   231   val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys
   232   fun norm_tac ss =
   233     ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
   234     THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
   235     THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3))
   236 
   237   val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys
   238   fun numeral_simp_tac ss =
   239     ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   240     THEN ALLGOALS (SIMPSET' (fn simpset => asm_simp_tac (Simplifier.inherit_context ss simpset)))
   241   val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
   242   end;
   243 
   244 
   245 structure EqCancelNumerals = CancelNumeralsFun
   246  (open CancelNumeralsCommon
   247   val prove_conv = ArithData.prove_conv "inteq_cancel_numerals"
   248   val mk_bal   = FOLogic.mk_eq
   249   val dest_bal = FOLogic.dest_eq
   250   val bal_add1 = eq_add_iff1 RS iff_trans
   251   val bal_add2 = eq_add_iff2 RS iff_trans
   252 );
   253 
   254 structure LessCancelNumerals = CancelNumeralsFun
   255  (open CancelNumeralsCommon
   256   val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
   257   val mk_bal   = FOLogic.mk_binrel "Int.zless"
   258   val dest_bal = FOLogic.dest_bin "Int.zless" iT
   259   val bal_add1 = less_add_iff1 RS iff_trans
   260   val bal_add2 = less_add_iff2 RS iff_trans
   261 );
   262 
   263 structure LeCancelNumerals = CancelNumeralsFun
   264  (open CancelNumeralsCommon
   265   val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
   266   val mk_bal   = FOLogic.mk_binrel "Int.zle"
   267   val dest_bal = FOLogic.dest_bin "Int.zle" iT
   268   val bal_add1 = le_add_iff1 RS iff_trans
   269   val bal_add2 = le_add_iff2 RS iff_trans
   270 );
   271 
   272 val cancel_numerals =
   273   map prep_simproc
   274    [("inteq_cancel_numerals",
   275      ["l $+ m = n", "l = m $+ n",
   276       "l $- m = n", "l = m $- n",
   277       "l $* m = n", "l = m $* n"],
   278      K EqCancelNumerals.proc),
   279     ("intless_cancel_numerals",
   280      ["l $+ m $< n", "l $< m $+ n",
   281       "l $- m $< n", "l $< m $- n",
   282       "l $* m $< n", "l $< m $* n"],
   283      K LessCancelNumerals.proc),
   284     ("intle_cancel_numerals",
   285      ["l $+ m $<= n", "l $<= m $+ n",
   286       "l $- m $<= n", "l $<= m $- n",
   287       "l $* m $<= n", "l $<= m $* n"],
   288      K LeCancelNumerals.proc)];
   289 
   290 
   291 (*version without the hyps argument*)
   292 fun prove_conv_nohyps name tacs sg = ArithData.prove_conv name tacs sg [];
   293 
   294 structure CombineNumeralsData =
   295   struct
   296   type coeff            = int
   297   val iszero            = (fn x => x = 0)
   298   val add               = op + 
   299   val mk_sum            = (fn T:typ => long_mk_sum) (*to work for #2*x $+ #3*x *)
   300   val dest_sum          = dest_sum
   301   val mk_coeff          = mk_coeff
   302   val dest_coeff        = dest_coeff 1
   303   val left_distrib      = left_zadd_zmult_distrib RS trans
   304   val prove_conv        = prove_conv_nohyps "int_combine_numerals"
   305   fun trans_tac _       = ArithData.gen_trans_tac trans
   306 
   307   val norm_ss1 = ZF_ss addsimps add_0s @ mult_1s @ diff_simps @ zminus_simps @ @{thms zadd_ac} @ intifys
   308   val norm_ss2 = ZF_ss addsimps bin_simps @ int_mult_minus_simps @ intifys
   309   val norm_ss3 = ZF_ss addsimps int_minus_from_mult_simps @ @{thms zadd_ac} @ @{thms zmult_ac} @ tc_rules @ intifys
   310   fun norm_tac ss =
   311     ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
   312     THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
   313     THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss3))
   314 
   315   val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys
   316   fun numeral_simp_tac ss =
   317     ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   318   val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
   319   end;
   320 
   321 structure CombineNumerals = CombineNumeralsFun(CombineNumeralsData);
   322 
   323 val combine_numerals =
   324   prep_simproc ("int_combine_numerals", ["i $+ j", "i $- j"], K CombineNumerals.proc);
   325 
   326 
   327 
   328 (** Constant folding for integer multiplication **)
   329 
   330 (*The trick is to regard products as sums, e.g. #3 $* x $* #4 as
   331   the "sum" of #3, x, #4; the literals are then multiplied*)
   332 
   333 
   334 structure CombineNumeralsProdData =
   335   struct
   336   type coeff            = int
   337   val iszero            = (fn x => x = 0)
   338   val add               = op *
   339   val mk_sum            = (fn T:typ => mk_prod)
   340   val dest_sum          = dest_prod
   341   fun mk_coeff(k,t) = if t=one then mk_numeral k
   342                       else raise TERM("mk_coeff", [])
   343   fun dest_coeff t = (dest_numeral t, one)  (*We ONLY want pure numerals.*)
   344   val left_distrib      = @{thm zmult_assoc} RS sym RS trans
   345   val prove_conv        = prove_conv_nohyps "int_combine_numerals_prod"
   346   fun trans_tac _       = ArithData.gen_trans_tac trans
   347 
   348 
   349 
   350 val norm_ss1 = ZF_ss addsimps mult_1s @ diff_simps @ zminus_simps
   351   val norm_ss2 = ZF_ss addsimps [@{thm zmult_zminus_right} RS sym] @
   352     bin_simps @ @{thms zmult_ac} @ tc_rules @ intifys
   353   fun norm_tac ss =
   354     ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss1))
   355     THEN ALLGOALS (asm_simp_tac (Simplifier.inherit_context ss norm_ss2))
   356 
   357   val numeral_simp_ss = ZF_ss addsimps bin_simps @ tc_rules @ intifys
   358   fun numeral_simp_tac ss =
   359     ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
   360   val simplify_meta_eq  = ArithData.simplify_meta_eq (mult_1s);
   361   end;
   362 
   363 
   364 structure CombineNumeralsProd = CombineNumeralsFun(CombineNumeralsProdData);
   365 
   366 val combine_numerals_prod =
   367   prep_simproc ("int_combine_numerals_prod", ["i $* j"], K CombineNumeralsProd.proc);
   368 
   369 end;
   370 
   371 
   372 Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
   373 Addsimprocs [Int_Numeral_Simprocs.combine_numerals,
   374              Int_Numeral_Simprocs.combine_numerals_prod];
   375 
   376 
   377 (*examples:*)
   378 (*
   379 print_depth 22;
   380 set timing;
   381 set trace_simp;
   382 fun test s = (Goal s; by (Asm_simp_tac 1));
   383 val sg = #sign (rep_thm (topthm()));
   384 val t = FOLogic.dest_Trueprop (Logic.strip_assums_concl(getgoal 1));
   385 val (t,_) = FOLogic.dest_eq t;
   386 
   387 (*combine_numerals_prod (products of separate literals) *)
   388 test "#5 $* x $* #3 = y";
   389 
   390 test "y2 $+ ?x42 = y $+ y2";
   391 
   392 test "oo : int ==> l $+ (l $+ #2) $+ oo = oo";
   393 
   394 test "#9$*x $+ y = x$*#23 $+ z";
   395 test "y $+ x = x $+ z";
   396 
   397 test "x : int ==> x $+ y $+ z = x $+ z";
   398 test "x : int ==> y $+ (z $+ x) = z $+ x";
   399 test "z : int ==> x $+ y $+ z = (z $+ y) $+ (x $+ w)";
   400 test "z : int ==> x$*y $+ z = (z $+ y) $+ (y$*x $+ w)";
   401 
   402 test "#-3 $* x $+ y $<= x $* #2 $+ z";
   403 test "y $+ x $<= x $+ z";
   404 test "x $+ y $+ z $<= x $+ z";
   405 
   406 test "y $+ (z $+ x) $< z $+ x";
   407 test "x $+ y $+ z $< (z $+ y) $+ (x $+ w)";
   408 test "x$*y $+ z $< (z $+ y) $+ (y$*x $+ w)";
   409 
   410 test "l $+ #2 $+ #2 $+ #2 $+ (l $+ #2) $+ (oo $+ #2) = uu";
   411 test "u : int ==> #2 $* u = u";
   412 test "(i $+ j $+ #12 $+ k) $- #15 = y";
   413 test "(i $+ j $+ #12 $+ k) $- #5 = y";
   414 
   415 test "y $- b $< b";
   416 test "y $- (#3 $* b $+ c) $< b $- #2 $* c";
   417 
   418 test "(#2 $* x $- (u $* v) $+ y) $- v $* #3 $* u = w";
   419 test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u $* #4 = w";
   420 test "(#2 $* x $* u $* v $+ (u $* v) $* #4 $+ y) $- v $* u = w";
   421 test "u $* v $- (x $* u $* v $+ (u $* v) $* #4 $+ y) = w";
   422 
   423 test "(i $+ j $+ #12 $+ k) = u $+ #15 $+ y";
   424 test "(i $+ j $* #2 $+ #12 $+ k) = j $+ #5 $+ y";
   425 
   426 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";
   427 
   428 test "a $+ $-(b$+c) $+ b = d";
   429 test "a $+ $-(b$+c) $- b = d";
   430 
   431 (*negative numerals*)
   432 test "(i $+ j $+ #-2 $+ k) $- (u $+ #5 $+ y) = zz";
   433 test "(i $+ j $+ #-3 $+ k) $< u $+ #5 $+ y";
   434 test "(i $+ j $+ #3 $+ k) $< u $+ #-6 $+ y";
   435 test "(i $+ j $+ #-12 $+ k) $- #15 = y";
   436 test "(i $+ j $+ #12 $+ k) $- #-15 = y";
   437 test "(i $+ j $+ #-12 $+ k) $- #-15 = y";
   438 
   439 (*Multiplying separated numerals*)
   440 Goal "#6 $* ($# x $* #2) =  uu";
   441 Goal "#4 $* ($# x $* $# x) $* (#2 $* $# x) =  uu";
   442 *)
   443