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