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