1val name_alist =
2map (fn s => (acl2_name_to_hol_name s, s))
3[
4"ACL2::IFF",
5"ACL2::BOOLEANP",
6"ACL2::IMPLIES",
7"COMMON-LISP::NOT",
8"ACL2::HIDE",
9"COMMON-LISP::EQ",
10"ACL2::TRUE-LISTP",
11"ACL2::LIST-MACRO",
12"ACL2::AND-MACRO",
13"ACL2::OR-MACRO",
14"ACL2::INTEGER-ABS",
15"ACL2::XXXJOIN",
16"ACL2::LEN",
17"COMMON-LISP::LENGTH",
18"ACL2::ACL2-COUNT",
19"ACL2::COND-CLAUSESP",
20"ACL2::COND-MACRO",
21"ACL2::EQLABLEP",
22"ACL2::EQLABLE-LISTP",
23"COMMON-LISP::ATOM",
24"ACL2::MAKE-CHARACTER-LIST",
25"ACL2::EQLABLE-ALISTP",
26"ACL2::ALISTP",
27"COMMON-LISP::ACONS",
28"COMMON-LISP::ENDP",
29"ACL2::MUST-BE-EQUAL",
30"ACL2::MEMBER-EQUAL",
31"ACL2::UNION-EQUAL",
32"ACL2::SUBSETP-EQUAL",
33"ACL2::SYMBOL-LISTP",
34"COMMON-LISP::NULL",
35"ACL2::MEMBER-EQ",
36"ACL2::SUBSETP-EQ",
37"ACL2::SYMBOL-ALISTP",
38"ACL2::ASSOC-EQ",
39"ACL2::ASSOC-EQUAL",
40"ACL2::ASSOC-EQ-EQUAL-ALISTP",
41"ACL2::ASSOC-EQ-EQUAL",
42"ACL2::NO-DUPLICATESP-EQUAL",
43"ACL2::STRIP-CARS",
44"COMMON-LISP::EQL",
45"COMMON-LISP::=",
46"COMMON-LISP::/=",
47"ACL2::ZP",
48"ACL2::ZIP",
49"COMMON-LISP::NTH",
50"COMMON-LISP::CHAR",
51"ACL2::PROPER-CONSP",
52"ACL2::IMPROPER-CONSP",
53"COMMON-LISP::CONJUGATE",
54"ACL2::PROG2$",
55"ACL2::TIME$",
56"ACL2::FIX",
57"ACL2::FORCE",
58"ACL2::IMMEDIATE-FORCE-MODEP",
59"ACL2::CASE-SPLIT",
60"ACL2::SYNP",
61"COMMON-LISP::MEMBER",
62"ACL2::NO-DUPLICATESP",
63"COMMON-LISP::ASSOC",
64"ACL2::R-EQLABLE-ALISTP",
65"COMMON-LISP::RASSOC",
66"ACL2::RASSOC-EQUAL",
67"ACL2::R-SYMBOL-ALISTP",
68"ACL2::RASSOC-EQ"];
69
70val defuns =
71[
72`(DEFUN IFF (P Q)
73       (IF P (IF Q 'T 'NIL) (IF Q 'NIL 'T)))`,
74
75
76`(DEFUN BOOLEANP (X)
77       (IF (EQUAL X 'T) 'T (EQUAL X 'NIL)))`,
78
79
80`(DEFUN IMPLIES (P Q)
81       (IF P (IF Q 'T 'NIL) 'T))`,
82
83
84`(DEFUN NOT (P) (IF P 'NIL 'T))`,
85
86
87`(DEFUN HIDE (X) X)`,
88
89
90`(DEFUN EQ (X Y) (EQUAL X Y))`,
91
92
93`(DEFUN TRUE-LISTP (X)
94       (IF (CONSP X)
95           (TRUE-LISTP (CDR X))
96           (EQ X 'NIL)))`,
97
98
99`(DEFUN LIST-MACRO (LST)
100       (IF (CONSP LST)
101           (CONS 'CONS
102                 (CONS (CAR LST)
103                       (CONS (LIST-MACRO (CDR LST)) 'NIL)))
104           'NIL))`,
105
106
107`(DEFUN AND-MACRO (LST)
108       (IF (CONSP LST)
109           (IF (CONSP (CDR LST))
110               (CONS 'IF
111                     (CONS (CAR LST)
112                           (CONS (AND-MACRO (CDR LST))
113                                 (CONS 'NIL 'NIL))))
114               (CAR LST))
115           'T))`,
116
117
118`(DEFUN OR-MACRO (LST)
119       (IF (CONSP LST)
120           (IF (CONSP (CDR LST))
121               (CONS 'IF
122                     (CONS (CAR LST)
123                           (CONS (CAR LST)
124                                 (CONS (OR-MACRO (CDR LST)) 'NIL))))
125               (CAR LST))
126           'NIL))`,
127
128
129`(DEFUN INTEGER-ABS (X)
130       (IF (INTEGERP X)
131           (IF (< X '0) (UNARY-- X) X)
132           '0))`,
133
134
135`(DEFUN XXXJOIN (FN ARGS)
136       (IF (CDR (CDR ARGS))
137           (CONS FN
138                 (CONS (CAR ARGS)
139                       (CONS (XXXJOIN FN (CDR ARGS)) 'NIL)))
140           (CONS FN ARGS)))`,
141
142
143`(DEFUN LEN (X)
144       (IF (CONSP X)
145           (BINARY-+ '1 (LEN (CDR X)))
146           '0))`,
147
148
149`(DEFUN LENGTH (X)
150       (IF (STRINGP X)
151           (LEN (COERCE X 'LIST))
152           (LEN X)))`,
153
154
155`(DEFUN ACL2-COUNT (X)
156       (IF (CONSP X)
157           (BINARY-+ '1
158                     (BINARY-+ (ACL2-COUNT (CAR X))
159                               (ACL2-COUNT (CDR X))))
160           (IF (RATIONALP X)
161               (IF (INTEGERP X)
162                   (INTEGER-ABS X)
163                   (BINARY-+ (INTEGER-ABS (NUMERATOR X))
164                             (DENOMINATOR X)))
165               (IF (COMPLEX-RATIONALP X)
166                   (BINARY-+ '1
167                             (BINARY-+ (ACL2-COUNT (REALPART X))
168                                       (ACL2-COUNT (IMAGPART X))))
169                   (IF (STRINGP X) (LENGTH X) '0)))))`,
170
171
172`(DEFUN COND-CLAUSESP (CLAUSES)
173       (IF (CONSP CLAUSES)
174           (IF (CONSP (CAR CLAUSES))
175               (IF (TRUE-LISTP (CAR CLAUSES))
176                   (IF (< (LEN (CAR CLAUSES)) '3)
177                       (IF (EQ (CAR (CAR CLAUSES)) 'T)
178                           (EQ (CDR CLAUSES) 'NIL)
179                           (COND-CLAUSESP (CDR CLAUSES)))
180                       'NIL)
181                   'NIL)
182               'NIL)
183           (EQ CLAUSES 'NIL)))`,
184
185
186`(DEFUN COND-MACRO (CLAUSES)
187       (IF (CONSP CLAUSES)
188           (IF (EQ (CAR (CAR CLAUSES)) 'T)
189               (IF (CDR (CAR CLAUSES))
190                   (CAR (CDR (CAR CLAUSES)))
191                   (CAR (CAR CLAUSES)))
192               (CONS 'IF
193                     (CONS (CAR (CAR CLAUSES))
194                           (CONS (IF (CDR (CAR CLAUSES))
195                                     (CAR (CDR (CAR CLAUSES)))
196                                     (CAR (CAR CLAUSES)))
197                                 (CONS (COND-MACRO (CDR CLAUSES))
198                                       'NIL)))))
199           'NIL))`,
200
201
202`(DEFUN EQLABLEP (X)
203       (IF (ACL2-NUMBERP X)
204           (ACL2-NUMBERP X)
205           (IF (SYMBOLP X)
206               (SYMBOLP X)
207               (CHARACTERP X))))`,
208
209
210`(DEFUN EQLABLE-LISTP (L)
211       (IF (CONSP L)
212           (IF (EQLABLEP (CAR L))
213               (EQLABLE-LISTP (CDR L))
214               'NIL)
215           (EQUAL L 'NIL)))`,
216
217
218`(DEFUN ATOM (X) (NOT (CONSP X)))`,
219
220
221`(DEFUN MAKE-CHARACTER-LIST (X)
222       (IF (ATOM X)
223           'NIL
224           (IF (CHARACTERP (CAR X))
225               (CONS (CAR X)
226                     (MAKE-CHARACTER-LIST (CDR X)))
227               (CONS (CODE-CHAR '0)
228                     (MAKE-CHARACTER-LIST (CDR X))))))`,
229
230
231`(DEFUN EQLABLE-ALISTP (X)
232       (IF (ATOM X)
233           (EQUAL X 'NIL)
234           (IF (CONSP (CAR X))
235               (IF (EQLABLEP (CAR (CAR X)))
236                   (EQLABLE-ALISTP (CDR X))
237                   'NIL)
238               'NIL)))`,
239
240
241`(DEFUN ALISTP (L)
242       (IF (ATOM L)
243           (EQ L 'NIL)
244           (IF (CONSP (CAR L))
245               (ALISTP (CDR L))
246               'NIL)))`,
247
248
249`(DEFUN ACONS (KEY DATUM ALIST)
250       (CONS (CONS KEY DATUM) ALIST))`,
251
252
253`(DEFUN ENDP (X) (ATOM X))`,
254
255
256`(DEFUN MUST-BE-EQUAL (LOGIC EXEC) LOGIC)`,
257
258
259`(DEFUN MEMBER-EQUAL (X LST)
260       (IF (ENDP LST)
261           'NIL
262           (IF (EQUAL X (CAR LST))
263               LST (MEMBER-EQUAL X (CDR LST)))))`,
264
265
266`(DEFUN UNION-EQUAL (X Y)
267       (IF (ENDP X)
268           Y
269           (IF (MEMBER-EQUAL (CAR X) Y)
270               (UNION-EQUAL (CDR X) Y)
271               (CONS (CAR X)
272                     (UNION-EQUAL (CDR X) Y)))))`,
273
274
275`(DEFUN SUBSETP-EQUAL (X Y)
276       (IF (ENDP X)
277           'T
278           (IF (MEMBER-EQUAL (CAR X) Y)
279               (SUBSETP-EQUAL (CDR X) Y)
280               'NIL)))`,
281
282
283`(DEFUN SYMBOL-LISTP (LST)
284       (IF (ATOM LST)
285           (EQ LST 'NIL)
286           (IF (SYMBOLP (CAR LST))
287               (SYMBOL-LISTP (CDR LST))
288               'NIL)))`,
289
290
291`(DEFUN NULL (X) (EQ X 'NIL))`,
292
293
294`(DEFUN MEMBER-EQ (X LST)
295       (IF (ENDP LST)
296           'NIL
297           (IF (EQ X (CAR LST))
298               LST (MEMBER-EQ X (CDR LST)))))`,
299
300
301`(DEFUN SUBSETP-EQ (X Y)
302       (IF (ENDP X)
303           'T
304           (IF (MEMBER-EQ (CAR X) Y)
305               (SUBSETP-EQ (CDR X) Y)
306               'NIL)))`,
307
308
309`(DEFUN SYMBOL-ALISTP (X)
310       (IF (ATOM X)
311           (EQ X 'NIL)
312           (IF (CONSP (CAR X))
313               (IF (SYMBOLP (CAR (CAR X)))
314                   (SYMBOL-ALISTP (CDR X))
315                   'NIL)
316               'NIL)))`,
317
318
319`(DEFUN ASSOC-EQ (X ALIST)
320       (IF (ENDP ALIST)
321           'NIL
322           (IF (EQ X (CAR (CAR ALIST)))
323               (CAR ALIST)
324               (ASSOC-EQ X (CDR ALIST)))))`,
325
326
327`(DEFUN ASSOC-EQUAL (X ALIST)
328       (IF (ENDP ALIST)
329           'NIL
330           (IF (EQUAL X (CAR (CAR ALIST)))
331               (CAR ALIST)
332               (ASSOC-EQUAL X (CDR ALIST)))))`,
333
334
335`(DEFUN ASSOC-EQ-EQUAL-ALISTP (X)
336       (IF (ATOM X)
337           (EQ X 'NIL)
338           (IF (CONSP (CAR X))
339               (IF (SYMBOLP (CAR (CAR X)))
340                   (IF (CONSP (CDR (CAR X)))
341                       (ASSOC-EQ-EQUAL-ALISTP (CDR X))
342                       'NIL)
343                   'NIL)
344               'NIL)))`,
345
346
347`(DEFUN ASSOC-EQ-EQUAL (X Y ALIST)
348       (IF (ENDP ALIST)
349           'NIL
350           (IF (IF (EQ (CAR (CAR ALIST)) X)
351                   (EQUAL (CAR (CDR (CAR ALIST))) Y)
352                   'NIL)
353               (CAR ALIST)
354               (ASSOC-EQ-EQUAL X Y (CDR ALIST)))))`,
355
356
357`(DEFUN NO-DUPLICATESP-EQUAL (L)
358       (IF (ENDP L)
359           'T
360           (IF (MEMBER-EQUAL (CAR L) (CDR L))
361               'NIL
362               (NO-DUPLICATESP-EQUAL (CDR L)))))`,
363
364
365`(DEFUN STRIP-CARS (X)
366       (IF (ENDP X)
367           'NIL
368           (CONS (CAR (CAR X))
369                 (STRIP-CARS (CDR X)))))`,
370
371
372`(DEFUN EQL (X Y) (EQUAL X Y))`,
373
374
375`(DEFUN = (X Y) (EQUAL X Y))`,
376
377
378`(DEFUN /= (X Y) (NOT (EQUAL X Y)))`,
379
380
381`(DEFUN ZP (X)
382       (IF (INTEGERP X) (NOT (< '0 X)) 'T))`,
383
384
385`(DEFUN ZIP (X)
386       (IF (INTEGERP X) (= X '0) 'T))`,
387
388
389`(DEFUN NTH (N L)
390       (IF (ENDP L)
391           'NIL
392           (IF (ZP N)
393               (CAR L)
394               (NTH (BINARY-+ '-1 N) (CDR L)))))`,
395
396
397`(DEFUN CHAR (S N)
398       (NTH N (COERCE S 'LIST)))`,
399
400
401`(DEFUN PROPER-CONSP (X)
402       (IF (CONSP X) (TRUE-LISTP X) 'NIL))`,
403
404
405`(DEFUN IMPROPER-CONSP (X)
406       (IF (CONSP X)
407           (NOT (TRUE-LISTP X))
408           'NIL))`,
409
410
411`(DEFUN CONJUGATE (X)
412       (IF (COMPLEX-RATIONALP X)
413           (COMPLEX (REALPART X)
414                    (UNARY-- (IMAGPART X)))
415           X))`,
416
417
418`(DEFUN PROG2$ (X Y) Y)`,
419
420
421`(DEFUN TIME$ (X) X)`,
422
423
424`(DEFUN FIX (X)
425       (IF (ACL2-NUMBERP X) X '0))`,
426
427
428`(DEFUN FORCE (X) X)`,
429
430
431`(DEFUN IMMEDIATE-FORCE-MODEP
432       NIL '"See :DOC immediate-force-modep.")`,
433
434
435`(DEFUN CASE-SPLIT (X) X)`,
436
437
438`(DEFUN SYNP (VARS FORM TERM) 'T)`,
439
440
441`(DEFUN MEMBER (X L)
442       (IF (ENDP L)
443           'NIL
444           (IF (EQL X (CAR L))
445               L (MEMBER X (CDR L)))))`,
446
447
448`(DEFUN NO-DUPLICATESP (L)
449       (IF (ENDP L)
450           'T
451           (IF (MEMBER (CAR L) (CDR L))
452               'NIL
453               (NO-DUPLICATESP (CDR L)))))`,
454
455
456`(DEFUN ASSOC (X ALIST)
457       (IF (ENDP ALIST)
458           'NIL
459           (IF (EQL X (CAR (CAR ALIST)))
460               (CAR ALIST)
461               (ASSOC X (CDR ALIST)))))`,
462
463
464`(DEFUN R-EQLABLE-ALISTP (X)
465       (IF (ATOM X)
466           (EQUAL X 'NIL)
467           (IF (CONSP (CAR X))
468               (IF (EQLABLEP (CDR (CAR X)))
469                   (R-EQLABLE-ALISTP (CDR X))
470                   'NIL)
471               'NIL)))`,
472
473
474`(DEFUN RASSOC (X ALIST)
475       (IF (ENDP ALIST)
476           'NIL
477           (IF (EQL X (CDR (CAR ALIST)))
478               (CAR ALIST)
479               (RASSOC X (CDR ALIST)))))`,
480
481
482`(DEFUN RASSOC-EQUAL (X ALIST)
483       (IF (ENDP ALIST)
484           'NIL
485           (IF (EQUAL X (CDR (CAR ALIST)))
486               (CAR ALIST)
487               (RASSOC-EQUAL X (CDR ALIST)))))`,
488
489
490`(DEFUN R-SYMBOL-ALISTP (X)
491       (IF (ATOM X)
492           (EQUAL X 'NIL)
493           (IF (CONSP (CAR X))
494               (IF (SYMBOLP (CDR (CAR X)))
495                   (R-SYMBOL-ALISTP (CDR X))
496                   'NIL)
497               'NIL)))`,           
498
499
500`(DEFUN RASSOC-EQ (X ALIST)
501       (IF (ENDP ALIST)
502           'NIL
503           (IF (EQ X (CDR (CAR ALIST)))
504               (CAR ALIST)
505               (RASSOC-EQ X (CDR ALIST)))))`
506];
507