1structure numSyntax :> numSyntax =
2struct
3  open HolKernel Abbrev;
4
5  local open arithmeticTheory whileTheory numeralTheory in end;
6
7  val ERR = mk_HOL_ERR "numSyntax";
8
9(*---------------------------------------------------------------------------
10          Constants
11 ---------------------------------------------------------------------------*)
12
13  val num = mk_thy_type {Thy = "num", Tyop = "num", Args = []}
14
15  val suc_tm       = prim_mk_const {Name="SUC",     Thy="num"}
16  val zero_tm      = prim_mk_const {Name="0",       Thy="num"}
17  val less_tm      = prim_mk_const {Name="<",       Thy="prim_rec"}
18  val measure_tm   = prim_mk_const {Name="measure", Thy="prim_rec"}
19  val pre_tm       = prim_mk_const {Name="PRE",     Thy="prim_rec"}
20  val alt_zero_tm  = prim_mk_const {Name="ZERO",    Thy="arithmetic"}
21  val bit1_tm      = prim_mk_const {Name="BIT1",    Thy="arithmetic"}
22  val bit2_tm      = prim_mk_const {Name="BIT2",    Thy="arithmetic"}
23  val div2_tm      = prim_mk_const {Name="DIV2",    Thy="arithmetic"}
24  val div_tm       = prim_mk_const {Name="DIV",     Thy="arithmetic"}
25  val divmod_tm    = prim_mk_const {Name="DIVMOD",  Thy="arithmetic"};
26  val even_tm      = prim_mk_const {Name="EVEN",    Thy="arithmetic"}
27  val exp_tm       = prim_mk_const {Name="EXP",     Thy="arithmetic"}
28  val fact_tm      = prim_mk_const {Name="FACT",    Thy="arithmetic"}
29  val funpow_tm    = prim_mk_const {Name="FUNPOW",  Thy="arithmetic"}
30  val geq_tm       = prim_mk_const {Name=">=",      Thy="arithmetic"}
31  val greater_tm   = prim_mk_const {Name=">",       Thy="arithmetic"}
32  val leq_tm       = prim_mk_const {Name="<=",      Thy="arithmetic"}
33  val max_tm       = prim_mk_const {Name="MAX",     Thy="arithmetic"}
34  val min_tm       = prim_mk_const {Name="MIN",     Thy="arithmetic"}
35  val minus_tm     = prim_mk_const {Name="-",       Thy="arithmetic"}
36  val mod_tm       = prim_mk_const {Name="MOD",     Thy="arithmetic"}
37  val mult_tm      = prim_mk_const {Name="*",       Thy="arithmetic"}
38  val num_case_tm  = prim_mk_const {Name="num_CASE",Thy="arithmetic"}
39  val numeral_tm   = prim_mk_const {Name="NUMERAL", Thy="arithmetic"}
40  val odd_tm       = prim_mk_const {Name="ODD",     Thy="arithmetic"}
41  val plus_tm      = prim_mk_const {Name="+",       Thy="arithmetic"}
42  val least_tm     = prim_mk_const {Name="LEAST",   Thy="while"};
43  val while_tm     = prim_mk_const {Name="WHILE",   Thy="while"}
44
45
46(*---------------------------------------------------------------------------
47          Constructors
48 ---------------------------------------------------------------------------*)
49
50  fun mk_monop c tm = mk_comb(c,tm)
51  fun mk_binop c (tm1,tm2) = mk_comb(mk_comb(c,tm1),tm2);
52
53  val mk_bit1     = mk_monop bit1_tm
54  val mk_bit2     = mk_monop bit2_tm
55  val mk_div      = mk_binop div_tm
56  val mk_div2     = mk_monop div2_tm
57  val mk_even     = mk_monop even_tm
58  val mk_exp      = mk_binop exp_tm
59  val mk_fact     = mk_monop fact_tm
60  val mk_geq      = mk_binop geq_tm
61  val mk_greater  = mk_binop greater_tm
62  val mk_leq      = mk_binop leq_tm
63  val mk_less     = mk_binop less_tm
64  val mk_max      = mk_binop max_tm
65  val mk_min      = mk_binop min_tm
66  val mk_minus    = mk_binop minus_tm
67  val mk_mod      = mk_binop mod_tm
68  val mk_mult     = mk_binop mult_tm
69  val mk_odd      = mk_monop odd_tm
70  val mk_plus     = mk_binop plus_tm
71  val mk_pre      = mk_monop pre_tm
72  val mk_suc      = mk_monop suc_tm
73
74  fun mk_num_case(b,f,n) =
75      list_mk_comb(inst[alpha |-> type_of b] num_case_tm, [n,b,f]);
76
77  fun mk_funpow(f,n,x) =
78      list_mk_comb(inst [alpha |-> type_of x] funpow_tm, [f,n,x]);
79
80  fun mk_while(P,g,x) =
81      list_mk_comb(inst [alpha |-> type_of x] while_tm, [P,g,x]);
82
83  fun mk_least P =
84      mk_comb(inst [alpha |-> fst(dom_rng(type_of P))] least_tm, P);
85
86  fun mk_divmod(m,n,a) = list_mk_comb(divmod_tm, [m,n,a]);
87
88  fun mk_measure (f,x,y) =
89      list_mk_comb(inst [alpha |-> type_of x] measure_tm, [f,x,y]);
90
91  (* Partial application of measure is often more useful *)
92  fun mk_cmeasure f =
93     mk_comb(inst [alpha |-> fst(dom_rng (type_of f))] measure_tm, f);
94
95
96(*---------------------------------------------------------------------------
97          Destructors
98 ---------------------------------------------------------------------------*)
99
100  val dest_bit1     = dest_monop bit1_tm     (ERR "dest_bit1" "")
101  val dest_bit2     = dest_monop bit2_tm     (ERR "dest_bit2" "")
102  val dest_div      = dest_binop div_tm      (ERR "dest_div" "")
103  val dest_div2     = dest_monop div2_tm     (ERR "dest_div2" "")
104  val dest_even     = dest_monop even_tm     (ERR "dest_even" "")
105  val dest_exp      = dest_binop exp_tm      (ERR "dest_exp" "")
106  val dest_fact     = dest_monop fact_tm     (ERR "dest_fact" "");
107  val dest_geq      = dest_binop geq_tm      (ERR "dest_geq" "")
108  val dest_greater  = dest_binop greater_tm  (ERR "dest_greater" "")
109  val dest_least    = dest_monop least_tm    (ERR "dest_least" "");
110  val dest_leq      = dest_binop leq_tm      (ERR "dest_leq" "")
111  val dest_less     = dest_binop less_tm     (ERR "dest_less" "")
112  val dest_max      = dest_binop max_tm      (ERR "dest_max" "")
113  val dest_min      = dest_binop min_tm      (ERR "dest_min" "")
114  val dest_minus    = dest_binop minus_tm    (ERR "dest_minus" "")
115  val dest_mod      = dest_binop mod_tm      (ERR "dest_mod" "")
116  val dest_mult     = dest_binop mult_tm     (ERR "dest_mult" "")
117  val dest_odd      = dest_monop odd_tm      (ERR "dest_odd" "");
118  val dest_plus     = dest_binop plus_tm     (ERR "dest_plus" "")
119  val dest_pre      = dest_monop pre_tm      (ERR "dest_pre" "")
120  val dest_suc      = dest_monop suc_tm      (ERR "dest_suc" "")
121
122  fun dest_num_case tm =
123    case strip_comb tm
124     of (ncase,[n,b,f]) =>
125         if same_const num_case_tm ncase
126         then (b,f,n)
127         else raise ERR "dest_num_case" "not an application of \"num_CASE\""
128      | _ => raise ERR "dest_num_case" "not an application of \"num_CASE\""
129
130  fun dest_funpow tm =
131    case strip_comb tm
132     of (funpow,[f,n,x]) =>
133         if same_const funpow_tm funpow
134         then (f,n,x)
135         else raise ERR "dest_funpow" "not an application of \"FUNPOW\""
136      | _ => raise ERR "dest_funpow" "not an application of \"FUNPOW\"";
137
138
139  fun dest_while tm =
140    case strip_comb tm
141     of (whle,[P,g,x]) =>
142         if same_const while_tm whle
143         then (P,g,x)
144         else raise ERR "dest_while" "not an application of \"WHILE\""
145      | _ => raise ERR "dest_while" "not an application of \"WHILE\"";
146
147  fun dest_divmod tm =
148    case strip_comb tm
149     of (dm,[m,n,a]) =>
150         if same_const divmod_tm dm
151         then (m,n,a)
152         else raise ERR "dest_divmod" "not an application of \"divmod\""
153      | _ => raise ERR "dest_divmod" "not an application of \"divmod\"";
154
155  fun dest_measure tm =
156    case strip_comb tm
157     of (m,[f,x,y]) =>
158         if same_const measure_tm m
159         then (f,x,y)
160         else raise ERR "dest_measure" "not an application of \"measure\""
161      | _ => raise ERR "dest_measure" "not an application of \"measure\"";
162
163  fun dest_cmeasure tm =
164    case total dest_comb tm
165     of NONE => raise ERR "dest_cmeasure" "not an application of \"measure\""
166      | SOME (m,f) => if same_const measure_tm m then f
167                      else raise ERR "dest_cmeasure"
168                                     "not an application of \"measure\""
169
170(*---------------------------------------------------------------------------
171          Query operations
172 ---------------------------------------------------------------------------*)
173
174  val is_bit1     = can dest_bit1
175  val is_bit2     = can dest_bit2
176  val is_div      = can dest_div
177  val is_div2     = can dest_div2
178  val is_divmod   = can dest_divmod
179  val is_even     = can dest_even
180  val is_exp      = can dest_exp
181  val is_fact     = can dest_fact
182  val is_funpow   = can dest_funpow
183  val is_geq      = can dest_geq
184  val is_greater  = can dest_greater
185  val is_least    = can dest_least
186  val is_leq      = can dest_leq
187  val is_less     = can dest_less
188  val is_max      = can dest_max
189  val is_measure  = can dest_measure
190  val is_min      = can dest_min
191  val is_minus    = can dest_minus
192  val is_mod      = can dest_mod
193  val is_mult     = can dest_mult
194  val is_num_case = can dest_num_case
195  val is_odd      = can dest_odd
196  val is_plus     = can dest_plus
197  val is_pre      = can dest_pre
198  val is_suc      = can dest_suc
199  val is_while    = can dest_while
200
201
202(*---------------------------------------------------------------------------
203     Numerals are treated specially
204 ---------------------------------------------------------------------------*)
205
206  val mk_numeral = Literal.gen_mk_numeral {
207    mk_comb  = Term.mk_comb,
208    ALT_ZERO = alt_zero_tm,
209    ZERO     = zero_tm,
210    NUMERAL  = numeral_tm,
211    BIT1     = bit1_tm,
212    BIT2     = bit2_tm
213  };
214
215  fun dest_numeral t =
216    Literal.dest_numeral t handle HOL_ERR _ =>
217      raise ERR "dest_numeral" "term is not a numeral"
218
219  val is_numeral = can dest_numeral
220
221  val int_of_term = Arbnum.toInt o dest_numeral
222  fun term_of_int i = mk_numeral(Arbnum.fromInt i)
223
224(*---------------------------------------------------------------------------
225     Dealing with lists of things to be added or multiplied.
226 ---------------------------------------------------------------------------*)
227
228  fun list_mk_plus (h::t) = rev_itlist (C (curry mk_plus)) t h
229    | list_mk_plus [] = raise ERR "list_mk_plus" "empty list";
230
231  fun list_mk_mult (h::t) = rev_itlist (C (curry mk_mult)) t h
232    | list_mk_mult [] = raise ERR "list_mk_mult" "empty list";
233
234  val strip_plus = strip_binop (total dest_plus)
235  val strip_mult = strip_binop (total dest_mult)
236
237(*---------------------------------------------------------------------------
238     Lifting ML Arbnums to HOL nums
239 ---------------------------------------------------------------------------*)
240
241fun lift_num ty arbnum = mk_numeral arbnum
242
243end
244