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