1signature IntDP_Munge =
2sig
3
4  include Abbrev
5  val BASIC_CONV : string -> conv -> conv
6  val COND_ABS_CONV : conv
7  val NBOOL_COND_RAND_CONV : conv
8
9  val is_presburger : term -> bool
10  val non_presburger_subterms : term -> term list
11  val dealwith_nats : term -> term * (thm -> thm)
12
13  val conv_tac : conv -> tactic
14
15end
16
17(*
18   [BASIC_CONV s c t] normalises term t, and then applies conversion c
19   in an attempt to decide t.  The string s is used to generate appropriate
20   error messages, and should be the "name" of the conversion.
21
22   [COND_ABS_CONV t] takes a term of the form
23       \x. if b then L else R
24   and turns it into
25       if b then \x. L else \x. R
26   where x doesn't occur in b but may do in L and R.
27
28   [NBOOL_COND_RAND_CONV t] takes a term of the form
29       f (if b then t else e)
30   and turns it into
31       if b then f t else f e
32   as long as the type of t is not boolean (in which case the operand term
33   should be rewritten with COND_EXPAND).
34
35   [is_presburger t] returns true if term t is Presburger.
36
37   [non_presburger_subterms t] returns a list of the non-Presburger
38   sub-terms occurring in t.
39
40   [dealwith_nats t] works on terms that might contain natural number
41   formulas.  It returns a pair (t', f), where t' is an integer formula that
42   is "equivalent" to the original (but with possible extra
43   generalisations introduced).  The function f will take a theorem of the
44   form |- t' = T and produce |- t = T
45
46   [conv_tac c] creates a tactic that pulls appropriate assumptions out
47   of the assumption list, adds them to the goal (using MP_TAC), and then
48   calls the conversion c on that goal.  c is assumed to be a complete
49   arithmetic decision procedure for integers and/or natural numbers.
50   Appropriate assumptions are those whose non_presburger_subterms all
51   have type ``:int`` or ``:num``.
52*)
53