1signature CooperMath = sig 2 3 include Abbrev 4 type num = Arbnum.num 5 6 val cooper_compset : computeLib.compset 7 val REDUCE_CONV : term -> thm 8 val gcd_t : term 9 10 val gcd : Arbint.int * Arbint.int -> Arbint.int 11 val gcdl : Arbint.int list -> Arbint.int 12 val lcm : Arbint.int * Arbint.int -> Arbint.int 13 val lcml : Arbint.int list -> Arbint.int 14 val extended_gcd : num * num -> num * (Arbint.int * Arbint.int) 15 val sum_var_coeffs : term -> term -> Arbint.int 16 17 datatype dir = Left | Right 18 datatype termtype = EQ | LT 19 20 val dir_of_pair : dir -> ('a * 'a) -> 'a 21 val term_at : dir -> term -> term 22 val conv_at : dir -> (term -> thm) -> (term -> thm) 23 24 val move_terms_from: termtype -> dir -> (term -> bool) -> (term -> thm) 25 val collect_terms : term -> thm 26 val collect_in_sum : term -> term -> thm 27 28 val LINEAR_MULT : conv 29 30 (* a useful simplification conversion for division terms *) 31 (* these must be in the form 32 c | n * x + m * y + p * z ... + d 33 where all variables have coefficients and c is a positive literal. 34 There is no order required of the summands on the right however. *) 35 (* Is a "QConv"; raises QConv.UNCHANGED if a term doesn't change *) 36 val check_divides : term -> thm 37 38 39 (* for terms of form c int_divides n * x + ... , minimises the coefficients 40 and any bare numeric literals to be their old value mod c. c must be 41 positive *) 42 val minimise_divides : conv 43 44 (* replaces 45 m | a * x + b 46 with 47 d | b /\ ?t. x = ~p * (b/d) + t * (m/d) 48 where 49 d = gcd(a,m) and d = pa + qm 50 *) 51 val elim_sdivides : term -> thm 52 53 (* replaces 54 m | a * x + b /\ n | u * x + v 55 with 56 mn | d * x + v * m * p + b * n * q /\ 57 d | a * v - u * b 58 where 59 d = gcd (an, um) = pum + qan 60 *) 61 val elim_paired_divides : term -> thm 62 63 64 val simplify_constraints : term -> thm 65 66 val simplify_constrained_disjunct : conv 67 68 69 (* These two functions both factor out integers from sums 70 Both take the factor as an arbint and as a term as the first two 71 arguments (experience suggests that you usually have both of these 72 values around when programming, so it seems wasteful to force the 73 function to have to re-call either term_of_int or int_of_term). *) 74 75 (* factor_out only looks at summands of the form c * x, where c is a 76 numeral, and factor_out_lits only looks at summands that are literals 77 Both will do bogus things if given something to work on that doesn't 78 divide cleanly, e.g., factor_out_lits (Arbint.fromInt 2) ``5 + x`` *) 79 val factor_out : Arbint.int -> term -> term -> thm 80 val factor_out_lits : Arbint.int -> term -> term -> thm 81 82 val BLEAF_CONV : (conv * conv -> conv) -> conv -> conv 83 84 (* initial phases of the procedure *) 85 val phase1_CONV : conv 86 val phase2_CONV : term -> conv 87 val phase3_CONV : conv 88 89end 90