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