1signature intSyntax = 2sig 3 include Abbrev 4 5 (* terms and types *) 6 val int_ty : hol_type 7 val zero_tm : term 8 val one_tm : term 9 val negate_tm : term 10 val absval_tm : term 11 val plus_tm : term 12 val minus_tm : term 13 val mult_tm : term 14 val div_tm : term 15 val mod_tm : term 16 val quot_tm : term 17 val rem_tm : term 18 val exp_tm : term 19 val int_eq_tm : term 20 val less_tm : term 21 val leq_tm : term 22 val great_tm : term 23 val geq_tm : term 24 val divides_tm : term 25 val min_tm : term 26 val max_tm : term 27 val LEAST_INT_tm : term 28 val Num_tm : term (* the coercion from :int -> :num *) 29 val int_injection : term (* the injection from :num -> :int *) 30 31 (* discriminators, constructors, etc *) 32 33 val is_int_literal : term -> bool 34 val int_of_term : term -> Arbint.int 35 val term_of_int : Arbint.int -> term 36 37 val mk_injected : term -> term 38 val dest_injected : term -> term 39 val is_injected : term -> bool 40 41 val mk_Num : term -> term 42 val dest_Num : term -> term 43 val is_Num : term -> bool 44 45 val is_negated : term -> bool (* if a term is of form ~ e *) 46 val mk_negated : term -> term 47 val dest_negated : term -> term 48 49 val is_plus : term -> bool 50 val mk_plus : (term * term) -> term 51 val dest_plus : term -> (term * term) 52 val list_mk_plus : (* non-empty *) term list -> term 53 val strip_plus : term -> term list 54 55 val is_minus : term -> bool 56 val dest_minus : term -> (term * term) 57 val mk_minus : (term * term) -> term 58 59 val is_mult : term -> bool 60 val mk_mult : (term * term) -> term 61 val dest_mult : term -> (term * term) 62 val list_mk_mult : (* non-empty *) term list -> term 63 val strip_mult : term -> term list 64 65 val is_exp : term -> bool 66 val mk_exp : (term * term) -> term 67 val dest_exp : term -> (term * term) 68 69 val is_div : term -> bool 70 val dest_div : term -> (term * term) 71 val mk_div : (term * term) -> term 72 73 val is_mod : term -> bool 74 val dest_mod : term -> (term * term) 75 val mk_mod : (term * term) -> term 76 77 val is_quot : term -> bool 78 val dest_quot : term -> (term * term) 79 val mk_quot : (term * term) -> term 80 81 val is_rem : term -> bool 82 val dest_rem : term -> (term * term) 83 val mk_rem : (term * term) -> term 84 85 val is_absval : term -> bool 86 val mk_absval : term -> term 87 val dest_absval : term -> term 88 89 val is_less : term -> bool 90 val dest_less : term -> (term * term) 91 val mk_less : (term * term) -> term 92 93 val is_leq : term -> bool 94 val dest_leq : term -> (term * term) 95 val mk_leq : (term * term) -> term 96 97 val is_great : term -> bool 98 val dest_great : term -> (term * term) 99 val mk_great : (term * term) -> term 100 101 val is_geq : term -> bool 102 val dest_geq : term -> (term * term) 103 val mk_geq : (term * term) -> term 104 105 val is_divides : term -> bool 106 val dest_divides : term -> (term * term) 107 val mk_divides : (term * term) -> term 108 109 val is_min : term -> bool 110 val dest_min : term -> (term * term) 111 val mk_min : (term * term) -> term 112 113 val is_max : term -> bool 114 val dest_max : term -> (term * term) 115 val mk_max : (term * term) -> term 116 117 val is_LEAST_INT : term -> bool 118 val dest_LEAST_INT : term -> term 119 val mk_LEAST_INT : term -> term 120 121end 122