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