Rqe/num_calc_simp.ml

   1
   2
   3 (* PUT BASIC ARITHMETIC OF THE NATURALS INTO THE SIMPLIFIER *)
   4
   5 (* based on NUM_RED_CONV in num_calc *)
   6
   7 let arith_ss thml  = itlist (fun (x,y) ss -> ss_of_conv x y ss)
   8     [`SUC(NUMERAL n)`,NUM_SUC_CONV;
   9      `PRE(NUMERAL n)`,NUM_PRE_CONV;
  10      `FACT(NUMERAL n)`,NUM_FACT_CONV;
  11      `NUMERAL m < NUMERAL n`,NUM_REL_CONV;
  12      `NUMERAL m <= NUMERAL n`,NUM_REL_CONV;
  13      `NUMERAL m > NUMERAL n`,NUM_REL_CONV;
  14      `NUMERAL m >= NUMERAL n`,NUM_REL_CONV;
  15      `NUMERAL m = NUMERAL n`,NUM_REL_CONV;
  16      `EVEN(NUMERAL n)`,NUM_EVEN_CONV;
  17      `ODD(NUMERAL n)`,NUM_ODD_CONV;
  18      `NUMERAL m + NUMERAL n`,NUM_ADD_CONV;
  19      `NUMERAL m - NUMERAL n`,NUM_SUB_CONV;
  20      `NUMERAL m * NUMERAL n`,NUM_MULT_CONV;
  21      `(NUMERAL m) EXP (NUMERAL n)`,NUM_EXP_CONV;
  22      `(NUMERAL m) DIV (NUMERAL n)`,NUM_DIV_CONV;
  23      `(NUMERAL m) MOD (NUMERAL n)`,NUM_MOD_CONV]
  24     (basic_ss thml);;
  25
  26 let ARITH_SIMP_CONV thl = SIMPLIFY_CONV (arith_ss []) thl;;
  27
  28 let arith_net() = itlist (uncurry net_of_conv)
  29     [`SUC(NUMERAL n)`,NUM_SUC_CONV;
  30      `PRE(NUMERAL n)`,NUM_PRE_CONV;
  31      `FACT(NUMERAL n)`,NUM_FACT_CONV;
  32      `NUMERAL m < NUMERAL n`,NUM_REL_CONV;
  33      `NUMERAL m <= NUMERAL n`,NUM_REL_CONV;
  34      `NUMERAL m > NUMERAL n`,NUM_REL_CONV;
  35      `NUMERAL m >= NUMERAL n`,NUM_REL_CONV;
  36      `NUMERAL m = NUMERAL n`,NUM_REL_CONV;
  37      `EVEN(NUMERAL n)`,NUM_EVEN_CONV;
  38      `ODD(NUMERAL n)`,NUM_ODD_CONV;
  39      `NUMERAL m + NUMERAL n`,NUM_ADD_CONV;
  40      `NUMERAL m - NUMERAL n`,NUM_SUB_CONV;
  41      `NUMERAL m * NUMERAL n`,NUM_MULT_CONV;
  42      `(NUMERAL m) EXP (NUMERAL n)`,NUM_EXP_CONV;
  43      `(NUMERAL m) DIV (NUMERAL n)`,NUM_DIV_CONV;
  44      `(NUMERAL m) MOD (NUMERAL n)`,NUM_MOD_CONV]
  45     (basic_net());;
  46
  47 let ARITH_REWRITE_CONV thl =
  48   GENERAL_REWRITE_CONV true TOP_DEPTH_CONV (arith_net()) thl;;
  49
  50 let ARITH_SIMP_TAC thl = CONV_TAC (ARITH_SIMP_CONV thl);;