3 (* PUT BASIC ARITHMETIC OF THE NATURALS INTO THE SIMPLIFIER *)
5 (* based on NUM_RED_CONV in num_calc *)
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]
26 let ARITH_SIMP_CONV thl = SIMPLIFY_CONV (arith_ss []) thl;;
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]
47 let ARITH_REWRITE_CONV thl =
48 GENERAL_REWRITE_CONV true TOP_DEPTH_CONV (arith_net()) thl;;
50 let ARITH_SIMP_TAC thl = CONV_TAC (ARITH_SIMP_CONV thl);;