1signature CooperSyntax = sig
2
3  include Abbrev
4  val not_tm  : term
5  val num_ty  : hol_type
6  val true_tm : term
7  val false_tm : term
8
9  val strip_exists : term -> (term list * term)
10
11  val cpis_conj : term -> bool
12  val cpis_disj : term -> bool
13
14  val cpstrip_conj : term -> term list
15  val cpstrip_disj : term -> term list
16
17  val cpEVERY_CONJ_CONV : (term -> Thm.thm) -> (term -> Thm.thm)
18  val cpEVERY_DISJ_CONV : (term -> Thm.thm) -> (term -> Thm.thm)
19
20  val has_exists : term -> bool
21  val has_forall : term -> bool
22  val has_quant : term -> bool
23
24  (* finds sub-terms satisfying given predicate that do not have any of their
25     free variables bound by binders higher in the same term *)
26  val find_free_terms : (term -> bool) -> term -> term HOLset.set
27
28  datatype qstatus = EITHER | NEITHER | qsUNIV | qsEXISTS
29  datatype term_op = CONJN | DISJN | NEGN
30  datatype reltype = rEQ | rDIV | rLT
31
32
33  val goal_qtype : term -> qstatus
34  val bop_characterise : term -> term_op option
35  val categorise_leaf : term -> reltype
36
37  val move_quants_up : term -> Thm.thm
38  val flip_forall : term -> Thm.thm
39  val flip_foralls : term -> Thm.thm
40
41  val count_vars : term -> (string * int) list
42
43  val move_conj_left : (term -> bool) -> term -> Thm.thm
44
45  val mk_constraint : term * term -> term
46  val is_constraint : term -> bool
47  val is_vconstraint : term -> term -> bool
48  val constraint_var : term -> term
49  val constraint_size : term -> Arbint.int
50  val dest_constraint : term -> (term * (term * term)) (*  (v, (lo, hi))  *)
51
52  val MK_CONSTRAINT : conv
53  val UNCONSTRAIN : conv
54  val IN_CONSTRAINT : conv -> conv
55  val quick_cst_elim : conv
56
57  val reduce_if_ground : conv
58  val fixup_newvar : conv
59
60  (* with ?x. p \/ q \/ r...          (with or's right associated)
61     expand to (?x. p) \/ (?x.q) \/ (?x.r) ...
62  *)
63  val push_one_exists_over_many_disjs : conv
64  val push_in_exists : conv
65
66  val simple_divides : term -> term -> bool
67
68  (* a "resquan" term is of the form
69     low < x /\ x <= high
70  *)
71  val resquan_remove : conv
72  val resquan_onestep : conv
73
74  (* a "vacuous" existential is a term of the form ?x. x = e *)
75  val remove_vacuous_existential : conv
76
77  val push_in_exists_and_follow : conv -> conv
78  val expand_right_and_over_or : conv
79
80  (* applies the argument conversion to all arguments of relational binary
81     operators in a standard Cooper formula (operators are =, < or
82     int_divides).  Allows for the conv argument to be a QConv, and will
83     also raise QConv.UNCHANGED itself *)
84  val ADDITIVE_TERMS_CONV : conv -> conv
85
86end
87