1structure intReduce :> intReduce =
2struct
3
4open HolKernel boolLib integerTheory intSyntax simpLib
5
6val ERR = mk_HOL_ERR "intSimps";
7
8(*---------------------------------------------------------------------------*)
9(* Integer-specific compset                                                  *)
10(*---------------------------------------------------------------------------*)
11
12val elim_thms = [INT_ADD_REDUCE, INT_SUB_REDUCE, INT_MUL_REDUCE,
13                 INT_DIV_REDUCE, INT_MOD_REDUCE, INT_EXP_REDUCE,
14                 INT_LT_REDUCE, INT_LE_REDUCE, INT_EQ_REDUCE,
15                 INT_GT_REDUCE, INT_GE_REDUCE, INT_DIVIDES_REDUCE,
16                 INT_ABS_NUM, INT_ABS_NEG, INT_QUOT_REDUCE, INT_REM_REDUCE,
17                 INT_MAX, INT_MIN, NUM_OF_INT]
18
19fun add_int_compset cmp = computeLib.add_thms elim_thms cmp
20
21fun int_compset () =
22   let
23       val cmp = reduceLib.num_compset()
24   in
25      add_int_compset cmp; cmp
26   end
27
28(*---------------------------------------------------------------------------*)
29(* Reducer for ground integer expressions                                    *)
30(*---------------------------------------------------------------------------*)
31
32val REDUCE_CONV = computeLib.CBV_CONV (int_compset())
33
34(*---------------------------------------------------------------------------*)
35(* Add integer reductions to the global compset                              *)
36(*---------------------------------------------------------------------------*)
37
38val _ = let open computeLib in add_funs elim_thms end;
39
40(*---------------------------------------------------------------------------*)
41(* Ground reduction conversions for integers (suitable for inclusion in      *)
42(* simplifier, or as stand-alone                                             *)
43(*---------------------------------------------------------------------------*)
44
45local
46  val num_ty = numSyntax.num
47  val int_ty = intSyntax.int_ty
48  val x = mk_var("x",int_ty)
49  val y = mk_var("y",int_ty)
50  val n = mk_var("n",num_ty)
51  val basic_op_terms =
52     [plus_tm, minus_tm, mult_tm, div_tm, mod_tm, int_eq_tm,
53      less_tm, leq_tm, great_tm, geq_tm, divides_tm, rem_tm, quot_tm,
54      min_tm, max_tm]
55  val basic_op_patterns = map (fn t => list_mk_comb(t, [x,y])) basic_op_terms
56  val exp_pattern = list_mk_comb(exp_tm, [x,n])
57  val abs_patterns = [lhs (#2 (strip_forall (concl INT_ABS_NEG))),
58                      lhs (#2 (strip_forall (concl INT_ABS_NUM)))]
59  fun reducible t = is_int_literal t orelse numSyntax.is_numeral t
60  fun reducer t =
61    let val (_, args) = strip_comb t
62    in if List.all reducible args then REDUCE_CONV t else Conv.NO_CONV t
63    end
64  fun mk_conv pat =
65     {name = "Integer calculation",
66      key = SOME([], pat), trace = 2,
67      conv = K (K reducer)}
68  val rederr = ERR "RED_CONV" "Term not reducible"
69in
70val INT_REDUCE_ss = SSFRAG
71  {name=SOME"INT_REDUCE",
72   convs = map mk_conv (exp_pattern::(abs_patterns @ basic_op_patterns)),
73   rewrs = [], congs = [], filter = NONE, ac = [], dprocs = []};
74
75fun RED_CONV t =
76 let val (f, args) = strip_comb t
77     val _ = f = exp_tm orelse mem f basic_op_terms orelse raise rederr
78     val _ = List.all reducible args orelse raise rederr
79     val _ = not (Lib.can dom_rng (type_of t)) orelse raise rederr
80 in
81   REDUCE_CONV t
82 end
83
84end (* local *) ;
85
86(*---------------------------------------------------------------------------*)
87(* Add reducer to srw_ss                                                     *)
88(*---------------------------------------------------------------------------*)
89
90val _ = BasicProvers.augment_srw_ss [INT_REDUCE_ss];
91
92(* Accumulate literal additions in integer expressions
93    (doesn't do coefficient gathering - just adds up literals, and
94     reassociates along the way)
95*)
96fun collect_additive_consts tm = let
97  val summands = strip_plus tm
98in
99  case summands of
100    [] => raise Fail "strip_plus returned [] in collect_additive_consts"
101  | [_] => NO_CONV tm
102  | _ => let
103    in
104      case partition is_int_literal summands of
105        ([], _) => NO_CONV tm
106      | ([_], _) => NO_CONV tm
107      | (_, []) => REDUCE_CONV tm
108      | (numerals, non_numerals) => let
109          val reorder_t = mk_eq(tm,
110                           mk_plus(list_mk_plus non_numerals,
111                                   list_mk_plus numerals))
112          val reorder_thm =
113            EQT_ELIM(AC_CONV(INT_ADD_ASSOC, INT_ADD_COMM) reorder_t)
114        in
115          (K reorder_thm THENC REDUCE_CONV THENC
116           TRY_CONV (REWR_CONV INT_ADD_RID)) tm
117        end
118    end
119end
120
121end
122