src/ZF/int_arith.ML
 changeset 23146 0bc590051d95 child 24630 351a308ab58d
equal inserted replaced
`       `
`     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)" zminus_equation,`
`       `
`    15           inst "x" "integ_of(?w)" equation_zminus];`
`       `
`    16 `
`       `
`    17 AddIffs [inst "y" "integ_of(?w)" zminus_zless,`
`       `
`    18          inst "x" "integ_of(?w)" zless_zminus];`
`       `
`    19 `
`       `
`    20 AddIffs [inst "y" "integ_of(?w)" zminus_zle,`
`       `
`    21          inst "x" "integ_of(?w)" 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 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 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 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 [zadd_zmult_distrib]@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 [zdiff_def, zadd_zmult_distrib]) 1);`
`       `
`    60 by (simp_tac (simpset() addsimps zcompare_rls) 1);`
`       `
`    61 by (simp_tac (simpset() addsimps 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 [zdiff_def, zadd_zmult_distrib]) 1);`
`       `
`    66 by (simp_tac (simpset() addsimps zcompare_rls) 1);`
`       `
`    67 by (simp_tac (simpset() addsimps 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 [zdiff_def, zadd_zmult_distrib]@`
`       `
`    72                                      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 [zdiff_def, zadd_zmult_distrib]@`
`       `
`    77                                      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 [zdiff_def, zadd_zmult_distrib]) 1);`
`       `
`    82 by (simp_tac (simpset() addsimps zcompare_rls) 1);`
`       `
`    83 by (simp_tac (simpset() addsimps 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 [zdiff_def, zadd_zmult_distrib]) 1);`
`       `
`    88 by (simp_tac (simpset() addsimps zcompare_rls) 1);`
`       `
`    89 by (simp_tac (simpset() addsimps 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 = [zadd_0_intify, zadd_0_right_intify];`
`       `
`   182 `
`       `
`   183 val mult_1s = [zmult_1_intify, zmult_1_right_intify,`
`       `
`   184                zmult_minus1, zmult_minus1_right];`
`       `
`   185 `
`       `
`   186 val tc_rules = [integ_of_type, intify_in_int,`
`       `
`   187                 int_of_type, zadd_type, zdiff_type, zmult_type] @ `
`       `
`   188                thms "bin.intros";`
`       `
`   189 val intifys = [intify_ident, zadd_intify1, zadd_intify2,`
`       `
`   190                zdiff_intify1, zdiff_intify2, zmult_intify1, zmult_intify2,`
`       `
`   191                zless_intify1, zless_intify2, zle_intify1, zle_intify2];`
`       `
`   192 `
`       `
`   193 (*To perform binary arithmetic*)`
`       `
`   194 val bin_simps = [add_integ_of_left] @ bin_arith_simps @ bin_rel_simps;`
`       `
`   195 `
`       `
`   196 (*To evaluate binary negations of coefficients*)`
`       `
`   197 val zminus_simps = NCons_simps @`
`       `
`   198                    [integ_of_minus RS sym,`
`       `
`   199                     bin_minus_1, bin_minus_0, bin_minus_Pls, bin_minus_Min,`
`       `
`   200                     bin_pred_1, bin_pred_0, bin_pred_Pls, bin_pred_Min];`
`       `
`   201 `
`       `
`   202 (*To let us treat subtraction as addition*)`
`       `
`   203 val diff_simps = [zdiff_def, zminus_zadd_distrib, zminus_zminus];`
`       `
`   204 `
`       `
`   205 (*push the unary minus down: - x * y = x * - y *)`
`       `
`   206 val int_minus_mult_eq_1_to_2 =`
`       `
`   207     [zmult_zminus, zmult_zminus_right RS sym] MRS trans |> standard;`
`       `
`   208 `
`       `
`   209 (*to extract again any uncancelled minuses*)`
`       `
`   210 val int_minus_from_mult_simps =`
`       `
`   211     [zminus_zminus, zmult_zminus, zmult_zminus_right];`
`       `
`   212 `
`       `
`   213 (*combine unary minus with numeric literals, however nested within a product*)`
`       `
`   214 val int_mult_minus_simps =`
`       `
`   215     [zmult_assoc, 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 @ 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 @ zadd_ac @ 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            = IntInf.int`
`       `
`   297   val iszero            = (fn x : IntInf.int => x = 0)`
`       `
`   298   val add               = IntInf.+ `
`       `
`   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 @ 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 @ zadd_ac @ 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            = IntInf.int`
`       `
`   337   val iszero            = (fn x : IntInf.int => x = 0)`
`       `
`   338   val add               = IntInf.*`
`       `
`   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      = 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 [zmult_zminus_right RS sym] @`
`       `
`   352     bin_simps @ 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 `