1(*****************************************************************************)
2(* FILE          : arith_cons.sml                                            *)
3(* DESCRIPTION   : Constructor, destructor and discriminator functions for   *)
4(*                 arithmetic terms.                                         *)
5(*                                                                           *)
6(* READS FILES   : <none>                                                    *)
7(* WRITES FILES  : <none>                                                    *)
8(*                                                                           *)
9(* AUTHOR        : R.J.Boulton, University of Cambridge                      *)
10(* DATE          : 4th March 1991                                            *)
11(*                                                                           *)
12(* TRANSLATOR    : R.J.Boulton, University of Cambridge                      *)
13(* DATE          : 4th February 1993                                         *)
14(*                                                                           *)
15(* LAST MODIFIED : R.J.Boulton                                               *)
16(* DATE          : 16th November 1995                                        *)
17(*****************************************************************************)
18
19structure Arith_cons :> Arith_cons =
20struct
21
22open HolKernel Arbint Abbrev;
23
24local open arithmeticTheory in end;
25
26(*===========================================================================*)
27(* Constructors, destructors and discriminators for +,-,*                    *)
28(*===========================================================================*)
29
30val num_ty = numSyntax.num
31
32(*---------------------------------------------------------------------------*)
33(* mk_plus, mk_minus, mk_mult                                                *)
34(*---------------------------------------------------------------------------*)
35
36val mk_plus  = numSyntax.mk_plus
37and mk_minus = numSyntax.mk_minus
38and mk_mult  = numSyntax.mk_mult
39
40(*---------------------------------------------------------------------------*)
41(* dest_plus, dest_minus, dest_mult                                          *)
42(*---------------------------------------------------------------------------*)
43
44val dest_plus  = numSyntax.dest_plus
45and dest_minus = numSyntax.dest_minus
46and dest_mult  = numSyntax.dest_mult
47
48(*---------------------------------------------------------------------------*)
49(* is_plus, is_minus, is_mult, is_arith_op                                   *)
50(*---------------------------------------------------------------------------*)
51
52val is_plus  = numSyntax.is_plus
53and is_minus = numSyntax.is_minus
54and is_mult  = numSyntax.is_mult
55
56(*===========================================================================*)
57(* Constructors, destructors and discriminators for <,<=,>,>=                *)
58(*===========================================================================*)
59
60(*---------------------------------------------------------------------------*)
61(* mk_less, mk_leq, mk_great, mk_geq                                         *)
62(*---------------------------------------------------------------------------*)
63
64val mk_less  = numSyntax.mk_less
65and mk_leq   = numSyntax.mk_leq
66and mk_great = numSyntax.mk_greater
67and mk_geq   = numSyntax.mk_geq
68
69(*---------------------------------------------------------------------------*)
70(* dest_less, dest_leq, dest_great, dest_geq                                 *)
71(*---------------------------------------------------------------------------*)
72
73val dest_less  = numSyntax.dest_less
74and dest_leq   = numSyntax.dest_leq
75and dest_great = numSyntax.dest_greater
76and dest_geq   = numSyntax.dest_geq
77
78(*---------------------------------------------------------------------------*)
79(* is_less, is_leq, is_great, is_geq, is_num_reln                            *)
80(*---------------------------------------------------------------------------*)
81
82val is_less  = numSyntax.is_less
83and is_leq   = numSyntax.is_leq
84and is_great = numSyntax.is_greater
85and is_geq   = numSyntax.is_geq;
86
87(*===========================================================================*)
88(* Constructor, destructor and discriminator for SUC                         *)
89(*===========================================================================*)
90
91val mk_suc   = numSyntax.mk_suc
92val dest_suc = numSyntax.dest_suc
93val is_suc   = numSyntax.is_suc;
94
95(*===========================================================================*)
96(* Constructor, destructor and discriminator for PRE                         *)
97(*===========================================================================*)
98
99val mk_pre   = numSyntax.mk_pre
100val dest_pre = numSyntax.dest_pre
101val is_pre   = numSyntax.is_pre
102
103(*===========================================================================*)
104(* Discriminators for numbers                                                *)
105(*===========================================================================*)
106
107val is_num_const = numSyntax.is_numeral
108val zero         = numSyntax.zero_tm
109fun is_zero tm   = (tm = zero)
110
111
112(*===========================================================================*)
113(* Conversions between ML integers and numeric constant terms                *)
114(*===========================================================================*)
115
116val int_of_term = fromNat o numSyntax.dest_numeral
117val term_of_int = numSyntax.mk_numeral o toNat
118
119(*===========================================================================*)
120(* Generation of a numeric variable from a name                              *)
121(*===========================================================================*)
122
123fun mk_num_var s = mk_var(s,num_ty);
124
125(*===========================================================================*)
126(* Functions to extract the arguments from an application of a binary op.    *)
127(*===========================================================================*)
128
129val arg1 = rand o rator
130and arg2 = rand;
131
132(*===========================================================================*)
133(* Is a term a full application of a numerical relation?                     *)
134(*===========================================================================*)
135
136local infixr -->
137      val num_reln_type = num_ty --> num_ty --> bool
138in
139fun is_num_reln tm =
140  (num_reln_type = type_of(rator(rator tm))) handle HOL_ERR _ => false
141end;
142
143end
144