1signature realSyntax = 2sig 3 include Abbrev 4 5 (* terms and types *) 6 val real_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 exp_tm : term 16 val real_eq_tm : term 17 val less_tm : term 18 val leq_tm : term 19 val great_tm : term 20 val geq_tm : term 21 val min_tm : term 22 val max_tm : term 23 val real_injection : term (* the injection from :num -> :real *) 24 25 (* discriminators, constructors, etc *) 26 27 val is_real_literal : term -> bool 28 val term_of_int : Arbint.int -> term 29 val int_of_term : term -> Arbint.int 30 31 val mk_injected : term -> term 32 val dest_injected : term -> term 33 val is_injected : term -> bool 34 35 val is_negated : term -> bool (* if a term is of form ~ e *) 36 val mk_negated : term -> term 37 val dest_negated : term -> term 38 39 val is_plus : term -> bool 40 val mk_plus : (term * term) -> term 41 val dest_plus : term -> (term * term) 42 val list_mk_plus : (* non-empty *) term list -> term 43 val strip_plus : term -> term list 44 45 val is_minus : term -> bool 46 val dest_minus : term -> (term * term) 47 val mk_minus : (term * term) -> term 48 49 val is_mult : term -> bool 50 val mk_mult : (term * term) -> term 51 val dest_mult : term -> (term * term) 52 val list_mk_mult : (* non-empty *) term list -> term 53 val strip_mult : term -> term list 54 55 val is_div : term -> bool 56 val dest_div : term -> (term * term) 57 val mk_div : (term * term) -> term 58 59 val is_absval : term -> bool 60 val mk_absval : term -> term 61 val dest_absval : term -> term 62 63 val is_less : term -> bool 64 val dest_less : term -> (term * term) 65 val mk_less : (term * term) -> term 66 67 val is_leq : term -> bool 68 val dest_leq : term -> (term * term) 69 val mk_leq : (term * term) -> term 70 71 val is_great : term -> bool 72 val dest_great : term -> (term * term) 73 val mk_great : (term * term) -> term 74 75 val is_geq : term -> bool 76 val dest_geq : term -> (term * term) 77 val mk_geq : (term * term) -> term 78 79 val is_min : term -> bool 80 val dest_min : term -> (term * term) 81 val mk_min : (term * term) -> term 82 83 val is_max : term -> bool 84 val dest_max : term -> (term * term) 85 val mk_max : (term * term) -> term 86 87end 88