1 2(*****************************************************************************) 3(* HOL definition of those ACL2 functions defined in defaxioms.lisp.trans *) 4(* that are used in the axioms proved in hol_defaxioms_proofsTheory. *) 5(* Unused functions are specified in comments, but not actually defined. *) 6(* Some functions are axiomatically defined using acl2AxiomDefine *) 7(*****************************************************************************) 8 9(*****************************************************************************) 10(* Ignore everything up to "END BOILERPLATE" *) 11(*****************************************************************************) 12 13(*****************************************************************************) 14(* START BOILERPLATE NEEDED FOR COMPILATION *) 15(*****************************************************************************) 16 17(****************************************************************************** 18* Load theories 19******************************************************************************) 20(* The commented out stuff below should be loaded in interactive sessions 21quietdec := true; 22map 23 load 24 ["stringLib","complex_rationalTheory","gcdTheory", 25 "sexp","sexpTheory"]; 26open stringLib complex_rationalTheory gcdTheory 27 sexp sexpTheory; 28Globals.checking_const_names := false; 29quietdec := false; 30*) 31 32(****************************************************************************** 33* Boilerplate needed for compilation: open HOL4 systems modules. 34******************************************************************************) 35open HolKernel Parse boolLib bossLib; 36 37(****************************************************************************** 38* Open theories (including ratTheory from Jens Brandt). 39******************************************************************************) 40open stringLib complex_rationalTheory gcdTheory sexp sexpTheory; 41 42(*****************************************************************************) 43(* END BOILERPLATE *) 44(*****************************************************************************) 45 46val _ = new_theory "hol_defaxioms"; 47 48(* 49 [oracles: DEFUN ACL2::IFF, DISK_THM] [axioms: ] [] 50 |- iff p q = itel [(p,andl [q; t]); (q,nil)] t, 51*) 52 53val iff_def = 54 acl2Define "ACL2::IFF" 55 `iff p q = itel [(p,andl [q; t]); (q,nil)] t`; 56 57val iff = 58 store_thm 59 ("iff_thm", 60 ``iff p q = ite p (ite q t nil) (ite q nil t)``, 61 RW_TAC std_ss [iff_def,ite_def,itel_def,andl_def]); 62 63(* 64 [oracles: DEFUN ACL2::BOOLEANP, DISK_THM] [axioms: ] [] 65 |- booleanp x = ite (equal x t) t (equal x nil), 66*) 67 68val booleanp_def = 69 acl2Define "ACL2::BOOLEANP" 70 `booleanp x = ite (equal x t) t (equal x nil)`; 71 72(* 73 [oracles: DEFUN ACL2::IMPLIES, DISK_THM] [axioms: ] [] 74 |- implies p q = ite p (andl [q; t]) t, 75*) 76 77(* Moved to sexpScript.sml 78val implies_def = 79 acl2Define "ACL2::IMPLIES" 80 `implies p q = ite p (andl [q; t]) t`; 81 82val implies_ite = 83 store_thm 84 ("implies_ite", 85 ``implies p q = ite p (ite q t nil) t``, 86 RW_TAC std_ss [implies_def,ite_def,itel_def,andl_def]); 87 88val implies = 89 store_thm 90 ("implies", 91 ``(|= implies p q) = (|= p) ==> (|= q)``, 92 ACL2_SIMP_TAC[]); 93*) 94 95(* 96 [oracles: DEFUN COMMON-LISP::NOT, DISK_THM] [axioms: ] [] 97 |- not p = ite p nil t, 98*) 99 100(* Moved to sexpScript.sml 101val not_def = 102 acl2Define "COMMON-LISP::NOT" 103 `not p = ite p nil t`; 104*) 105 106(* 107 [oracles: DEFUN ACL2::HIDE] [axioms: ] [] |- hide x = x, 108*) 109 110val hide_def = 111 acl2Define "ACL2::HIDE" 112 `hide x = x`; 113 114(* 115 [oracles: DEFUN COMMON-LISP::EQ] [axioms: ] [] |- eq x y = equal x y, 116*) 117 118val eq_def = 119 acl2Define "COMMON-LISP::EQ" 120 `eq x y = equal x y`; 121 122(* 123 [oracles: DEFUN ACL2::TRUE-LISTP, DISK_THM] [axioms: ] [] 124 |- true_listp x = ite (consp x) (true_listp (cdr x)) (eq x nil), 125*) 126 127val (true_listp_def,true_listp_ind) = 128 acl2_defn "ACL2::TRUE-LISTP" 129 (`true_listp x = ite (consp x) (true_listp (cdr x)) (eq x nil)`, 130 WF_REL_TAC `measure sexp_size` 131 THEN ACL2_SIMP_TAC []); 132 133(* 134 [oracles: DEFUN ACL2::LIST-MACRO, DISK_THM] [axioms: ] [] 135 |- list_macro lst = 136 andl [consp lst; List [csym "CONS"; car lst; list_macro (cdr lst)]], 137*) 138 139val (list_macro_def,list_macro_ind) = 140 acl2_defn "ACL2::LIST-MACRO" 141 (`list_macro lst = 142 andl [consp lst; List [csym "CONS"; car lst; list_macro (cdr lst)]]`, 143 WF_REL_TAC `measure sexp_size` 144 THEN ACL2_SIMP_TAC []); 145 146(* 147 [oracles: DEFUN ACL2::AND-MACRO, DISK_THM] [axioms: ] [] 148 |- and_macro lst = 149 ite (consp lst) 150 (ite (consp (cdr lst)) 151 (List [csym "IF"; car lst; and_macro (cdr lst); nil]) (car lst)) 152 t, 153*) 154 155val (and_macro_def,and_macro_ind) = 156 acl2_defn "ACL2::AND-MACRO" 157 (`and_macro lst = 158 ite (consp lst) 159 (ite (consp (cdr lst)) 160 (List [csym "IF"; car lst; and_macro (cdr lst); nil]) 161 (car lst)) 162 t`, 163 WF_REL_TAC `measure sexp_size` 164 THEN ACL2_SIMP_TAC []); 165 166(* 167 [oracles: DEFUN ACL2::OR-MACRO, DISK_THM] [axioms: ] [] 168 |- or_macro lst = 169 andl 170 [consp lst; 171 ite (consp (cdr lst)) 172 (List [csym "IF"; car lst; car lst; or_macro (cdr lst)]) 173 (car lst)], 174*) 175 176val (or_macro_def,or_macro_ind) = 177 acl2_defn "ACL2::OR-MACRO" 178 (`or_macro lst = 179 andl 180 [consp lst; 181 ite (consp (cdr lst)) 182 (List [csym "IF"; car lst; car lst; or_macro (cdr lst)]) 183 (car lst)]`, 184 WF_REL_TAC `measure sexp_size` 185 THEN ACL2_SIMP_TAC []); 186 187(* 188 [oracles: DEFUN ACL2::INTEGER-ABS, DISK_THM] [axioms: ] [] 189 |- integer_abs x = 190 ite (integerp x) (ite (less x (nat 0)) (unary_minus x) x) (nat 0), 191*) 192 193val integer_abs_def = 194 acl2Define "ACL2::INTEGER-ABS" 195 `integer_abs x = 196 ite (integerp x) (ite (less x (nat 0)) (unary_minus x) x) (nat 0)`; 197 198(* 199 [oracles: DEFUN ACL2::XXXJOIN, DISK_THM] [axioms: ] [] 200 |- xxxjoin fn args = 201 ite (cddr args) (List [fn; car args; xxxjoin fn (cdr args)]) 202 (cons fn args), 203*) 204 205val (xxxjoin_def,xxxjoin_ind) = 206 acl2_defn "ACL2::XXXJOIN" 207 (`xxxjoin fn args = 208 ite (cddr args) 209 (List [fn; car args; xxxjoin fn (cdr args)]) 210 (cons fn args)`, 211 WF_REL_TAC `measure (sexp_size o SND)` 212 THEN Cases_on `args` 213 THEN ACL2_SIMP_TAC []); 214 215(* 216 [oracles: DEFUN ACL2::LEN, DISK_THM] [axioms: ] [] 217 |- len x = ite (consp x) (add (nat 1) (len (cdr x))) (nat 0), 218*) 219 220val (len_def,len_ind) = 221 acl2_defn "ACL2::LEN" 222 (`len x = ite (consp x) (add (nat 1) (len (cdr x))) (nat 0)`, 223 WF_REL_TAC `measure sexp_size` 224 THEN ACL2_SIMP_TAC []); 225 226(* 227 [oracles: DEFUN COMMON-LISP::LENGTH, DISK_THM] [axioms: ] [] 228 |- length x = ite (stringp x) (len (coerce x (csym "LIST"))) (len x), 229*) 230 231val length_def = 232 acl2Define "COMMON-LISP::LENGTH" 233 `length x = ite (stringp x) (len (coerce x (csym "LIST"))) (len x)`; 234 235(* 236 [oracles: DEFUN ACL2::ACL2-COUNT, DISK_THM] [axioms: ] [] 237 |- acl2_count x = 238 itel 239 [(consp x, 240 add (nat 1) (add (acl2_count (car x)) (acl2_count (cdr x)))); 241 (rationalp x, 242 ite (integerp x) (integer_abs x) 243 (add (integer_abs (numerator x)) (denominator x))); 244 (complex_rationalp x, 245 add (nat 1) 246 (add (acl2_count (realpart x)) (acl2_count (imagpart x)))); 247 (stringp x,length x)] (nat 0), 248*) 249 250(* 251 [oracles: DEFUN ACL2::COND-CLAUSESP, DISK_THM] [axioms: ] [] 252 |- cond_clausesp clauses = 253 ite (consp clauses) 254 (andl 255 [consp (car clauses); true_listp (car clauses); 256 less (len (car clauses)) (nat 3); 257 ite (eq (caar clauses) t) (eq (cdr clauses) nil) 258 (cond_clausesp (cdr clauses))]) (eq clauses nil), 259*) 260 261val (cond_clausesp_def,cond_clausesp_ind) = 262 acl2_defn 263 "ACL2::COND-CLAUSESP" 264 (`cond_clausesp clauses = 265 ite (consp clauses) 266 (andl 267 [consp (car clauses); true_listp (car clauses); 268 less (len (car clauses)) (nat 3); 269 ite (eq (caar clauses) t) 270 (eq (cdr clauses) nil) 271 (cond_clausesp (cdr clauses))]) 272 (eq clauses nil)`, 273 WF_REL_TAC `measure sexp_size` 274 THEN ACL2_SIMP_TAC []); 275 276(* 277 [oracles: DEFUN ACL2::COND-MACRO, DISK_THM] [axioms: ] [] 278 |- cond_macro clauses = 279 andl 280 [consp clauses; 281 ite (eq (caar clauses) t) 282 (ite (cdar clauses) (cadar clauses) (caar clauses)) 283 (List 284 [csym "IF"; caar clauses; 285 ite (cdar clauses) (cadar clauses) (caar clauses); 286 cond_macro (cdr clauses)])], 287*) 288 289(* 290 [oracles: DEFUN ACL2::EQLABLEP, DISK_THM] [axioms: ] [] 291 |- eqlablep x = 292 itel [(acl2_numberp x,acl2_numberp x); (symbolp x,symbolp x)] 293 (characterp x), 294*) 295 296val eqlablep_def = 297 acl2Define "ACL2::EQLABLEP" 298 `eqlablep x = 299 itel [(acl2_numberp x,acl2_numberp x); (symbolp x,symbolp x)] 300 (characterp x)`; 301 302(* 303 [oracles: DEFUN ACL2::EQLABLE-LISTP, DISK_THM] [axioms: ] [] 304 |- eqlable_listp l = 305 ite (consp l) (andl [eqlablep (car l); eqlable_listp (cdr l)]) 306 (equal l nil), 307*) 308 309val (eqlable_listp_def,eqlable_listp_ind) = 310 acl2_defn 311 "ACL2::EQLABLE-LISTP" 312 (`eqlable_listp l = 313 ite (consp l) 314 (andl [eqlablep (car l); eqlable_listp (cdr l)]) 315 (equal l nil)`, 316 WF_REL_TAC `measure sexp_size` 317 THEN ACL2_SIMP_TAC []); 318 319val eqlable_listp = 320 store_thm 321 ("eqlable_listp", 322 ``(eqlable_listp (cons s s0) = 323 if itel 324 [(acl2_numberp s,acl2_numberp s); 325 (symbolp s,symbolp s)] (characterp s) = nil 326 then nil 327 else eqlable_listp s0) 328 /\ 329 (eqlable_listp (num n) = nil) 330 /\ 331 (eqlable_listp (chr c) = nil) 332 /\ 333 (eqlable_listp (str st) = nil) 334 /\ 335 (eqlable_listp (sym st st0) = if sym st st0 = nil then t else nil)``, 336 REPEAT CONJ_TAC 337 THEN CONV_TAC(LHS_CONV(ONCE_REWRITE_CONV[eqlable_listp_def])) 338 THEN ACL2_SIMP_TAC[]); 339 340val _ = add_acl2_simps[eqlable_listp]; 341 342(* 343 [oracles: DEFUN COMMON-LISP::ATOM] [axioms: ] [] 344 |- atom x = not (consp x), 345*) 346 347val atom_def = 348 acl2Define "COMMON-LISP::ATOM" 349 `atom x = not (consp x)`; 350 351(* 352 [oracles: DEFUN ACL2::MAKE-CHARACTER-LIST, DISK_THM] [axioms: ] [] 353 |- acl2_make_character_list x = 354 itel 355 [(atom x,nil); 356 (characterp (car x), 357 cons (car x) (acl2_make_character_list (cdr x)))] 358 (cons (code_char (nat 0)) (acl2_make_character_list (cdr x))), 359*) 360 361val (acl2_make_character_list_def,acl2_make_character_list_ind) = 362 acl2_defn 363 "ACL2::MAKE-CHARACTER-LIST" 364 (`acl2_make_character_list x = 365 itel 366 [(atom x,nil); 367 (characterp (car x), 368 cons (car x) (acl2_make_character_list (cdr x)))] 369 (cons (code_char (nat 0)) (acl2_make_character_list (cdr x)))`, 370 WF_REL_TAC `measure sexp_size` 371 THEN ACL2_SIMP_TAC []); 372 373val acl2_make_character_list = 374 store_thm 375 ("acl2_make_character_list", 376 ``(acl2_make_character_list (cons s s0) = 377 if characterp s = nil 378 then cons (code_char (nat 0)) (acl2_make_character_list s0) 379 else cons s (acl2_make_character_list s0)) 380 /\ 381 (acl2_make_character_list (num n) = nil) 382 /\ 383 (acl2_make_character_list (chr c) = nil) 384 /\ 385 (acl2_make_character_list (str st) = nil) 386 /\ 387 (acl2_make_character_list (sym st st0) = nil)``, 388 REPEAT CONJ_TAC 389 THEN CONV_TAC(LHS_CONV(ONCE_REWRITE_CONV[acl2_make_character_list_def])) 390 THEN ACL2_SIMP_TAC[itel_def]); 391 392val _ = add_acl2_simps[acl2_make_character_list]; 393 394(* 395 [oracles: DEFUN ACL2::EQLABLE-ALISTP, DISK_THM] [axioms: ] [] 396 |- eqlable_alistp x = 397 ite (atom x) (equal x nil) 398 (andl [consp (car x); eqlablep (caar x); eqlable_alistp (cdr x)]), 399*) 400 401val (eqlable_alistp_def,eqlable_alistp_ind) = 402 acl2_defn 403 "ACL2::EQLABLE-ALISTP" 404 (`eqlable_alistp x = 405 ite (atom x) 406 (equal x nil) 407 (andl [consp (car x); eqlablep (caar x); eqlable_alistp (cdr x)])`, 408 WF_REL_TAC `measure sexp_size` 409 THEN ACL2_SIMP_TAC []); 410 411(* 412 [oracles: DEFUN ACL2::ALISTP, DISK_THM] [axioms: ] [] 413 |- alistp l = 414 ite (atom l) (eq l nil) (andl [consp (car l); alistp (cdr l)]), 415*) 416 417val (alistp_def,alistp_ind) = 418 acl2_defn 419 "ACL2::ALISTP" 420 (`alistp l = 421 ite (atom l) (eq l nil) (andl [consp (car l); alistp (cdr l)])`, 422 WF_REL_TAC `measure sexp_size` 423 THEN ACL2_SIMP_TAC []); 424 425(* 426 [oracles: DEFUN COMMON-LISP::ACONS] [axioms: ] [] 427 |- acons key datum alist = cons (cons key datum) alist, 428*) 429 430val acons_def = 431 acl2Define "COMMON-LISP::ACONS" 432 `acons key datum alist = cons (cons key datum) alist`; 433 434(* 435 [oracles: DEFUN COMMON-LISP::ENDP] [axioms: ] [] |- endp x = atom x, 436*) 437 438val endp_def = 439 acl2Define "COMMON-LISP::ENDP" 440 `endp x = atom x`; 441 442(* 443 [oracles: DEFUN ACL2::MUST-BE-EQUAL] [axioms: ] [] 444 |- must_be_equal logic exec = logic, 445*) 446 447(* 448 [oracles: DEFUN ACL2::MEMBER-EQUAL, DISK_THM] [axioms: ] [] 449 |- member_equal x lst = 450 itel [(endp lst,nil); (equal x (car lst),lst)] 451 (member_equal x (cdr lst)), 452*) 453 454val (member_equal_def,member_equal_ind) = 455 acl2_defn "ACL2::MEMBER-EQUAL" 456 (`member_equal x lst = 457 itel [(endp lst,nil); (equal x (car lst),lst)] 458 (member_equal x (cdr lst))`, 459 WF_REL_TAC `measure (sexp_size o SND)` 460 THEN ACL2_SIMP_TAC []); 461 462(* 463 [oracles: DEFUN ACL2::UNION-EQUAL, DISK_THM] [axioms: ] [] 464 |- union_equal x y = 465 itel [(endp x,y); (member_equal (car x) y,union_equal (cdr x) y)] 466 (cons (car x) (union_equal (cdr x) y)), 467*) 468 469(* 470 [oracles: DEFUN ACL2::SUBSETP-EQUAL, DISK_THM] [axioms: ] [] 471 |- subsetp_equal x y = 472 ite (endp x) t 473 (andl [member_equal (car x) y; subsetp_equal (cdr x) y]), 474*) 475 476(* 477 [oracles: DEFUN ACL2::SYMBOL-LISTP, DISK_THM] [axioms: ] [] 478 |- symbol_listp lst = 479 ite (atom lst) (eq lst nil) 480 (andl [symbolp (car lst); symbol_listp (cdr lst)]), 481*) 482 483(* 484 [oracles: DEFUN COMMON-LISP::NULL] [axioms: ] [] |- null x = eq x nil, 485*) 486 487val null_def = 488 acl2Define "COMMON-LISP::NULL" 489 `null x = eq x nil`; 490 491(* 492 [oracles: DEFUN ACL2::MEMBER-EQ, DISK_THM] [axioms: ] [] 493 |- member_eq x lst = 494 itel [(endp lst,nil); (eq x (car lst),lst)] (member_eq x (cdr lst)), 495*) 496 497(* 498 [oracles: DEFUN ACL2::SUBSETP-EQ, DISK_THM] [axioms: ] [] 499 |- subsetp_eq x y = 500 ite (endp x) t (andl [member_eq (car x) y; subsetp_eq (cdr x) y]), 501*) 502 503(* 504 [oracles: DEFUN ACL2::SYMBOL-ALISTP, DISK_THM] [axioms: ] [] 505 |- symbol_alistp x = 506 ite (atom x) (eq x nil) 507 (andl [consp (car x); symbolp (caar x); symbol_alistp (cdr x)]), 508*) 509 510(* 511 [oracles: DEFUN ACL2::ASSOC-EQ, DISK_THM] [axioms: ] [] 512 |- assoc_eq x alist = 513 itel [(endp alist,nil); (eq x (caar alist),car alist)] 514 (assoc_eq x (cdr alist)), 515*) 516 517(* 518 [oracles: DEFUN ACL2::ASSOC-EQUAL, DISK_THM] [axioms: ] [] 519 |- assoc_equal x alist = 520 itel [(endp alist,nil); (equal x (caar alist),car alist)] 521 (assoc_equal x (cdr alist)), 522*) 523 524(* 525 [oracles: DEFUN ACL2::ASSOC-EQ-EQUAL-ALISTP, DISK_THM] [axioms: ] [] 526 |- assoc_eq_equal_alistp x = 527 ite (atom x) (eq x nil) 528 (andl 529 [consp (car x); symbolp (caar x); consp (cdar x); 530 assoc_eq_equal_alistp (cdr x)]), 531*) 532 533(* 534 [oracles: DEFUN ACL2::ASSOC-EQ-EQUAL, DISK_THM] [axioms: ] [] 535 |- assoc_eq_equal x y alist = 536 itel 537 [(endp alist,nil); 538 (andl [eq (caar alist) x; equal (cadar alist) y],car alist)] 539 (assoc_eq_equal x y (cdr alist)), 540*) 541 542(* 543 [oracles: DEFUN ACL2::NO-DUPLICATESP-EQUAL, DISK_THM] [axioms: ] [] 544 |- no_duplicatesp_equal l = 545 itel [(endp l,t); (member_equal (car l) (cdr l),nil)] 546 (no_duplicatesp_equal (cdr l)), 547*) 548 549(* 550 [oracles: DEFUN ACL2::STRIP-CARS, DISK_THM] [axioms: ] [] 551 |- strip_cars x = ite (endp x) nil (cons (caar x) (strip_cars (cdr x))), 552*) 553 554(* 555 [oracles: DEFUN COMMON-LISP::EQL] [axioms: ] [] |- eql x y = equal x y, 556*) 557 558val eql_def = 559 acl2Define "COMMON-LISP::EQL" 560 `eql x y = equal x y`; 561 562(* 563 [oracles: DEFUN COMMON-LISP::=] [axioms: ] [] 564 |- common_lisp_equal x y = equal x y, 565*) 566 567val common_lisp_equal_def = 568 acl2Define "COMMON-LISP::=" 569 `common_lisp_equal x y = equal x y`; 570 571(* 572 [oracles: DEFUN COMMON-LISP::/=] [axioms: ] [] 573 |- slash_equal x y = not (equal x y), 574*) 575 576(* 577 [oracles: DEFUN ACL2::ZP, DISK_THM] [axioms: ] [] 578 |- zp x = ite (integerp x) (not (less (nat 0) x)) t, 579*) 580 581val zp_def = 582 acl2Define "ACL2::ZP" 583 `zp x = ite (integerp x) (not (less (cpx 0 1 0 1) x)) t`; 584 585val zp = 586 store_thm 587 ("zp", 588 ``zp x = ite (integerp x) (not (less (nat 0) x)) t``, 589 RW_TAC std_ss [zp_def,nat_def,int_def]); 590 591(* 592 [oracles: DEFUN ACL2::ZIP, DISK_THM] [axioms: ] [] 593 |- zip x = ite (integerp x) (common_lisp_equal x (nat 0)) t, 594*) 595 596val zip_def = 597 acl2Define "ACL2::ZIP" 598 `zip x = ite (integerp x) (equal x (cpx 0 1 0 1)) t`; 599 600val zip = 601 store_thm 602 ("zip", 603 ``zip x = ite (integerp x) (common_lisp_equal x (nat 0)) t``, 604 RW_TAC std_ss [common_lisp_equal_def,zip_def,nat_def,int_def]); 605 606(* 607 [oracles: DEFUN COMMON-LISP::NTH, DISK_THM] [axioms: ] [] 608 |- nth n l = 609 itel [(endp l,nil); (zp n,car l)] (nth (add (int ~1) n) (cdr l)), 610*) 611 612(* 613 [oracles: DEFUN COMMON-LISP::CHAR, DISK_THM] [axioms: ] [] 614 |- char s n = nth n (coerce s (csym "LIST")), 615*) 616 617(* 618 [oracles: DEFUN ACL2::PROPER-CONSP, DISK_THM] [axioms: ] [] 619 |- proper_consp x = andl [consp x; true_listp x], 620*) 621 622(* 623 [oracles: DEFUN ACL2::IMPROPER-CONSP, DISK_THM] [axioms: ] [] 624 |- improper_consp x = andl [consp x; not (true_listp x)], 625*) 626 627(* 628 [oracles: DEFUN COMMON-LISP::CONJUGATE, DISK_THM] [axioms: ] [] 629 |- conjugate x = 630 ite (complex_rationalp x) 631 (complex (realpart x) (unary_minus (imagpart x))) x, 632*) 633 634(* 635 [oracles: DEFUN ACL2::PROG2$] [axioms: ] [] |- prog2_dollar x y = y, 636*) 637 638(* 639 [oracles: DEFUN ACL2::TIME$] [axioms: ] [] |- time_dollar x = x, 640*) 641 642(* 643 [oracles: DEFUN ACL2::FIX, DISK_THM] [axioms: ] [] 644 |- fix x = ite (acl2_numberp x) x (nat 0), 645*) 646 647val fix_def = 648 acl2Define "ACL2::FIX" 649 `fix x = ite (acl2_numberp x) x (cpx 0 1 0 1)`; 650 651val fix = 652 store_thm 653 ("fix", 654 ``fix x = ite (acl2_numberp x) x (nat 0)``, 655 RW_TAC std_ss [fix_def,nat_def,int_def]); 656 657(* 658 [oracles: DEFUN ACL2::FORCE] [axioms: ] [] |- force x = x, 659*) 660 661val force_def = 662 Define `force(s:sexp) = s`; 663 664(* 665 [oracles: DEFUN ACL2::IMMEDIATE-FORCE-MODEP] [axioms: ] [] 666 |- immediate_force_modep = str "See :DOC immediate-force-modep.", 667*) 668 669(* 670 [oracles: DEFUN ACL2::CASE-SPLIT] [axioms: ] [] |- case_split x = x, 671*) 672 673(* 674 [oracles: DEFUN ACL2::SYNP] [axioms: ] [] |- synp vars form term = t, 675*) 676 677(* 678 [oracles: DEFUN COMMON-LISP::MEMBER, DISK_THM] [axioms: ] [] 679 |- member x l = 680 itel [(endp l,nil); (eql x (car l),l)] (member x (cdr l)), 681*) 682 683val (member_def,member_ind) = 684 acl2_defn "COMMON-LISP::MEMBER" 685 (`member x l = 686 itel [(endp l,nil); (eql x (car l),l)] (member x (cdr l))`, 687 WF_REL_TAC `measure (sexp_size o SND)` 688 THEN ACL2_SIMP_TAC[]); 689 690(* 691 [oracles: DEFUN ACL2::NO-DUPLICATESP, DISK_THM] [axioms: ] [] 692 |- no_duplicatesp l = 693 itel [(endp l,t); (member (car l) (cdr l),nil)] 694 (no_duplicatesp (cdr l)), 695*) 696 697(* 698 [oracles: DEFUN COMMON-LISP::ASSOC, DISK_THM] [axioms: ] [] 699 |- assoc x alist = 700 itel [(endp alist,nil); (eql x (caar alist),car alist)] 701 (assoc x (cdr alist)), 702*) 703 704val (assoc_def,assoc_ind) = 705 acl2_defn "COMMON-LISP::ASSOC" 706 (`assoc x alist = 707 itel [(endp alist,nil); (eql x (caar alist),car alist)] 708 (assoc x (cdr alist))`, 709 WF_REL_TAC `measure (sexp_size o SND)` 710 THEN ACL2_SIMP_TAC[]); 711 712(* 713 [oracles: DEFUN ACL2::R-EQLABLE-ALISTP, DISK_THM] [axioms: ] [] 714 |- r_eqlable_alistp x = 715 ite (atom x) (equal x nil) 716 (andl [consp (car x); eqlablep (cdar x); r_eqlable_alistp (cdr x)]), 717*) 718 719(* 720 [oracles: DEFUN COMMON-LISP::RASSOC, DISK_THM] [axioms: ] [] 721 |- rassoc x alist = 722 itel [(endp alist,nil); (eql x (cdar alist),car alist)] 723 (rassoc x (cdr alist)), 724*) 725 726(* 727 [oracles: DEFUN ACL2::RASSOC-EQUAL, DISK_THM] [axioms: ] [] 728 |- rassoc_equal x alist = 729 itel [(endp alist,nil); (equal x (cdar alist),car alist)] 730 (rassoc_equal x (cdr alist)), 731*) 732 733(* 734 [oracles: DEFUN ACL2::R-SYMBOL-ALISTP, DISK_THM] [axioms: ] [] 735 |- r_symbol_alistp x = 736 ite (atom x) (equal x nil) 737 (andl [consp (car x); symbolp (cdar x); r_symbol_alistp (cdr x)]), 738*) 739 740(* 741 [oracles: DEFUN ACL2::RASSOC-EQ, DISK_THM] [axioms: ] [] 742 |- rassoc_eq x alist = 743 itel [(endp alist,nil); (eq x (cdar alist),car alist)] 744 (rassoc_eq x (cdr alist)), 745*) 746 747(* 748 [oracles: DEFUN COMMON-LISP::STANDARD-CHAR-P, DISK_THM] [axioms: ] [] 749 |- standard_char_p x = 750 andl 751 [member x 752 (List 753 [chr #"\n"; chr #" "; chr #"!"; chr #"\""; chr #"#"; 754 chr #"$"; chr #"%"; chr #"&"; chr #"'"; chr #"("; chr #")"; 755 chr #"*"; chr #"+"; chr #","; chr #"-"; chr #"."; chr #"/"; 756 chr #"0"; chr #"1"; chr #"2"; chr #"3"; chr #"4"; chr #"5"; 757 chr #"6"; chr #"7"; chr #"8"; chr #"9"; chr #":"; chr #";"; 758 chr #"<"; chr #"="; chr #">"; chr #"?"; chr #"@"; chr #"A"; 759 chr #"B"; chr #"C"; chr #"D"; chr #"E"; chr #"F"; chr #"G"; 760 chr #"H"; chr #"I"; chr #"J"; chr #"K"; chr #"L"; chr #"M"; 761 chr #"N"; chr #"O"; chr #"P"; chr #"Q"; chr #"R"; chr #"S"; 762 chr #"T"; chr #"U"; chr #"V"; chr #"W"; chr #"X"; chr #"Y"; 763 chr #"Z"; chr #"["; chr #"\\"; chr #"]"; chr #"^"; chr #"_"; 764 chr #"`"; chr #"a"; chr #"b"; chr #"c"; chr #"d"; chr #"e"; 765 chr #"f"; chr #"g"; chr #"h"; chr #"i"; chr #"j"; chr #"k"; 766 chr #"l"; chr #"m"; chr #"n"; chr #"o"; chr #"p"; chr #"q"; 767 chr #"r"; chr #"s"; chr #"t"; chr #"u"; chr #"v"; chr #"w"; 768 chr #"x"; chr #"y"; chr #"z"; chr #"{"; chr #"|"; chr #"}"; 769 chr #"~"]); t], 770*) 771 772val standard_char_p_def = 773 acl2Define "COMMON-LISP::STANDARD-CHAR-P" 774 `standard_char_p x = 775 andl 776 [member x 777 (List (MAP chr 778 [ #"\n"; #" "; #"!"; #"\""; #"#"; 779 #"$"; #"%"; #"&"; #"'"; #"("; #")"; 780 #"*"; #"+"; #";"; #"-"; #"."; #"/"; 781 #"0"; #"1"; #"2"; #"3"; #"4"; #"5"; 782 #"6"; #"7"; #"8"; #"9"; #":"; #";"; 783 #"<"; #"="; #">"; #"?"; #"@"; #"A"; 784 #"B"; #"C"; #"D"; #"E"; #"F"; #"G"; 785 #"H"; #"I"; #"J"; #"K"; #"L"; #"M"; 786 #"N"; #"O"; #"P"; #"Q"; #"R"; #"S"; 787 #"T"; #"U"; #"V"; #"W"; #"X"; #"Y"; 788 #"Z"; #"["; #"\\"; #"]"; #"^^"; #"_"; 789 #"^`"; #"a"; #"b"; #"c"; #"d"; #"e"; 790 #"f"; #"g"; #"h"; #"i"; #"j"; #"k"; 791 #"l"; #"m"; #"n"; #"o"; #"p"; #"q"; 792 #"r"; #"s"; #"t"; #"u"; #"v"; #"w"; 793 #"x"; #"y"; #"z"; #"{"; #"|"; #"}"; 794 #"~"])); t]`; 795 796 797 798(* 799- REWRITE_RULE [listTheory.MAP]standard_char_p_def; 800> val it = 801 |- !x. 802 standard_char_p x = 803 andl 804 [member x 805 (List 806 [chr #"\n"; chr #" "; chr #"!"; chr #"\""; chr #"#"; 807 chr #"$"; chr #"%"; chr #"&"; chr #"'"; chr #"("; 808 chr #")"; chr #"*"; chr #"+"; chr #","; chr #"-"; 809 chr #"."; chr #"/"; chr #"0"; chr #"1"; chr #"2"; 810 chr #"3"; chr #"4"; chr #"5"; chr #"6"; chr #"7"; 811 chr #"8"; chr #"9"; chr #":"; chr #";"; chr #"<"; 812 chr #"="; chr #">"; chr #"?"; chr #"@"; chr #"A"; 813 chr #"B"; chr #"C"; chr #"D"; chr #"E"; chr #"F"; 814 chr #"G"; chr #"H"; chr #"I"; chr #"J"; chr #"K"; 815 chr #"L"; chr #"M"; chr #"N"; chr #"O"; chr #"P"; 816 chr #"Q"; chr #"R"; chr #"S"; chr #"T"; chr #"U"; 817 chr #"V"; chr #"W"; chr #"X"; chr #"Y"; chr #"Z"; 818 chr #"["; chr #"\\"; chr #"]"; chr #"^"; chr #"_"; 819 chr #"`"; chr #"a"; chr #"b"; chr #"c"; chr #"d"; 820 chr #"e"; chr #"f"; chr #"g"; chr #"h"; chr #"i"; 821 chr #"j"; chr #"k"; chr #"l"; chr #"m"; chr #"n"; 822 chr #"o"; chr #"p"; chr #"q"; chr #"r"; chr #"s"; 823 chr #"t"; chr #"u"; chr #"v"; chr #"w"; chr #"x"; 824 chr #"y"; chr #"z"; chr #"{"; chr #"|"; chr #"}"; 825 chr #"~"]); t] : thm 826*) 827 828val standard_char_p = 829 save_thm 830 ("standard_char_p", 831 REWRITE_RULE [listTheory.MAP]standard_char_p_def); 832 833(* 834 [oracles: DEFUN ACL2::STANDARD-CHAR-LISTP, DISK_THM] [axioms: ] [] 835 |- standard_char_listp l = 836 ite (consp l) 837 (andl 838 [characterp (car l); standard_char_p (car l); 839 standard_char_listp (cdr l)]) (equal l nil), 840*) 841 842val (standard_char_listp_def,standard_char_listp_ind) = 843 acl2_defn "ACL2::STANDARD-CHAR-LISTP" 844 (`standard_char_listp l = 845 ite (consp l) 846 (andl 847 [characterp (car l); standard_char_p (car l); 848 standard_char_listp (cdr l)]) 849 (equal l nil)`, 850 WF_REL_TAC `measure sexp_size` 851 THEN ACL2_SIMP_TAC []); 852 853(* 854 [oracles: DEFUN ACL2::CHARACTER-LISTP, DISK_THM] [axioms: ] [] 855 |- character_listp l = 856 ite (atom l) (equal l nil) 857 (andl [characterp (car l); character_listp (cdr l)]), 858*) 859 860val (character_listp_def,character_listp_ind) = 861 acl2_defn "ACL2::CHARACTER-LISTP" 862 (`character_listp l = 863 ite (atom l) (equal l nil) 864 (andl [characterp (car l); character_listp (cdr l)])`, 865 ACL2_SIMP_TAC[] 866 THEN WF_REL_TAC `measure sexp_size` 867 THEN Cases 868 THEN ACL2_FULL_SIMP_TAC[]); 869 870val character_listp = 871 store_thm 872 ("character_listp", 873 ``(character_listp (cons s s0) = 874 if characterp s = nil then nil else character_listp s0) 875 /\ 876 (character_listp (num n) = nil) 877 /\ 878 (character_listp (chr c) = nil) 879 /\ 880 (character_listp (str st) = nil) 881 /\ 882 (character_listp (sym st st0) = if sym st st0 = nil then t else nil)``, 883 REPEAT CONJ_TAC 884 THEN CONV_TAC(LHS_CONV(ONCE_REWRITE_CONV[character_listp_def])) 885 THEN ACL2_SIMP_TAC[]); 886 887val _ = add_acl2_simps[character_listp]; 888 889(* 890 [oracles: DEFUN COMMON-LISP::STRING, DISK_THM] [axioms: ] [] 891 |- string x = 892 itel [(stringp x,x); (symbolp x,symbol_name x)] 893 (coerce (List [x]) (csym "STRING")), 894*) 895 896val string_def = 897 acl2Define "COMMON-LISP::STRING" 898 `string x = 899 itel [(stringp x,x); (symbolp x,symbol_name x)] 900 (coerce (List [x]) (csym "STRING"))`; 901 902(* 903 [oracles: DEFUN COMMON-LISP::ALPHA-CHAR-P, DISK_THM] [axioms: ] [] 904 |- alpha_char_p x = 905 andl 906 [member x 907 (List 908 [chr #"a"; chr #"b"; chr #"c"; chr #"d"; chr #"e"; chr #"f"; 909 chr #"g"; chr #"h"; chr #"i"; chr #"j"; chr #"k"; chr #"l"; 910 chr #"m"; chr #"n"; chr #"o"; chr #"p"; chr #"q"; chr #"r"; 911 chr #"s"; chr #"t"; chr #"u"; chr #"v"; chr #"w"; chr #"x"; 912 chr #"y"; chr #"z"; chr #"A"; chr #"B"; chr #"C"; chr #"D"; 913 chr #"E"; chr #"F"; chr #"G"; chr #"H"; chr #"I"; chr #"J"; 914 chr #"K"; chr #"L"; chr #"M"; chr #"N"; chr #"O"; chr #"P"; 915 chr #"Q"; chr #"R"; chr #"S"; chr #"T"; chr #"U"; chr #"V"; 916 chr #"W"; chr #"X"; chr #"Y"; chr #"Z"]); t], 917*) 918 919val alpha_char_p_def = 920 acl2Define "COMMON-LISP::ALPHA-CHAR-P" 921 `alpha_char_p x = 922 andl 923 [member x 924 (List 925 [chr #"a"; chr #"b"; chr #"c"; chr #"d"; chr #"e"; chr #"f"; 926 chr #"g"; chr #"h"; chr #"i"; chr #"j"; chr #"k"; chr #"l"; 927 chr #"m"; chr #"n"; chr #"o"; chr #"p"; chr #"q"; chr #"r"; 928 chr #"s"; chr #"t"; chr #"u"; chr #"v"; chr #"w"; chr #"x"; 929 chr #"y"; chr #"z"; chr #"A"; chr #"B"; chr #"C"; chr #"D"; 930 chr #"E"; chr #"F"; chr #"G"; chr #"H"; chr #"I"; chr #"J"; 931 chr #"K"; chr #"L"; chr #"M"; chr #"N"; chr #"O"; chr #"P"; 932 chr #"Q"; chr #"R"; chr #"S"; chr #"T"; chr #"U"; chr #"V"; 933 chr #"W"; chr #"X"; chr #"Y"; chr #"Z"]); t]`; 934 935(* 936 [oracles: DEFUN COMMON-LISP::UPPER-CASE-P, DISK_THM] [axioms: ] [] 937 |- upper_case_p x = 938 andl 939 [member x 940 (List 941 [chr #"A"; chr #"B"; chr #"C"; chr #"D"; chr #"E"; chr #"F"; 942 chr #"G"; chr #"H"; chr #"I"; chr #"J"; chr #"K"; chr #"L"; 943 chr #"M"; chr #"N"; chr #"O"; chr #"P"; chr #"Q"; chr #"R"; 944 chr #"S"; chr #"T"; chr #"U"; chr #"V"; chr #"W"; chr #"X"; 945 chr #"Y"; chr #"Z"]); t], 946*) 947 948val upper_case_p_def = 949 acl2Define "COMMON-LISP::UPPER-CASE-P" 950 `upper_case_p x = 951 andl 952 [member x 953 (List 954 [chr #"A"; chr #"B"; chr #"C"; chr #"D"; chr #"E"; chr #"F"; 955 chr #"G"; chr #"H"; chr #"I"; chr #"J"; chr #"K"; chr #"L"; 956 chr #"M"; chr #"N"; chr #"O"; chr #"P"; chr #"Q"; chr #"R"; 957 chr #"S"; chr #"T"; chr #"U"; chr #"V"; chr #"W"; chr #"X"; 958 chr #"Y"; chr #"Z"]); t]`; 959 960(* 961 [oracles: DEFUN COMMON-LISP::LOWER-CASE-P, DISK_THM] [axioms: ] [] 962 |- lower_case_p x = 963 andl 964 [member x 965 (List 966 [chr #"a"; chr #"b"; chr #"c"; chr #"d"; chr #"e"; chr #"f"; 967 chr #"g"; chr #"h"; chr #"i"; chr #"j"; chr #"k"; chr #"l"; 968 chr #"m"; chr #"n"; chr #"o"; chr #"p"; chr #"q"; chr #"r"; 969 chr #"s"; chr #"t"; chr #"u"; chr #"v"; chr #"w"; chr #"x"; 970 chr #"y"; chr #"z"]); t], 971*) 972 973val lower_case_p_def = 974 acl2Define "COMMON-LISP::LOWER-CASE-P" 975 `lower_case_p x = 976 andl 977 [member x 978 (List 979 [chr #"a"; chr #"b"; chr #"c"; chr #"d"; chr #"e"; chr #"f"; 980 chr #"g"; chr #"h"; chr #"i"; chr #"j"; chr #"k"; chr #"l"; 981 chr #"m"; chr #"n"; chr #"o"; chr #"p"; chr #"q"; chr #"r"; 982 chr #"s"; chr #"t"; chr #"u"; chr #"v"; chr #"w"; chr #"x"; 983 chr #"y"; chr #"z"]); t]`; 984 985(* 986 [oracles: DEFUN COMMON-LISP::CHAR-UPCASE, DISK_THM] [axioms: ] [] 987 |- char_upcase x = 988 (let pair = 989 assoc x 990 (List 991 [cons (chr #"a") (chr #"A"); cons (chr #"b") (chr #"B"); 992 cons (chr #"c") (chr #"C"); cons (chr #"d") (chr #"D"); 993 cons (chr #"e") (chr #"E"); cons (chr #"f") (chr #"F"); 994 cons (chr #"g") (chr #"G"); cons (chr #"h") (chr #"H"); 995 cons (chr #"i") (chr #"I"); cons (chr #"j") (chr #"J"); 996 cons (chr #"k") (chr #"K"); cons (chr #"l") (chr #"L"); 997 cons (chr #"m") (chr #"M"); cons (chr #"n") (chr #"N"); 998 cons (chr #"o") (chr #"O"); cons (chr #"p") (chr #"P"); 999 cons (chr #"q") (chr #"Q"); cons (chr #"r") (chr #"R"); 1000 cons (chr #"s") (chr #"S"); cons (chr #"t") (chr #"T"); 1001 cons (chr #"u") (chr #"U"); cons (chr #"v") (chr #"V"); 1002 cons (chr #"w") (chr #"W"); cons (chr #"x") (chr #"X"); 1003 cons (chr #"y") (chr #"Y"); cons (chr #"z") (chr #"Z")]) 1004 in 1005 itel [(pair,cdr pair); (characterp x,x)] (code_char (nat 0))), 1006*) 1007 1008val char_upcase_def = 1009 acl2Define "COMMON-LISP::CHAR-UPCASE" 1010 `char_upcase x = 1011 (let pair = 1012 assoc x 1013 (List 1014 [cons (chr #"a") (chr #"A"); cons (chr #"b") (chr #"B"); 1015 cons (chr #"c") (chr #"C"); cons (chr #"d") (chr #"D"); 1016 cons (chr #"e") (chr #"E"); cons (chr #"f") (chr #"F"); 1017 cons (chr #"g") (chr #"G"); cons (chr #"h") (chr #"H"); 1018 cons (chr #"i") (chr #"I"); cons (chr #"j") (chr #"J"); 1019 cons (chr #"k") (chr #"K"); cons (chr #"l") (chr #"L"); 1020 cons (chr #"m") (chr #"M"); cons (chr #"n") (chr #"N"); 1021 cons (chr #"o") (chr #"O"); cons (chr #"p") (chr #"P"); 1022 cons (chr #"q") (chr #"Q"); cons (chr #"r") (chr #"R"); 1023 cons (chr #"s") (chr #"S"); cons (chr #"t") (chr #"T"); 1024 cons (chr #"u") (chr #"U"); cons (chr #"v") (chr #"V"); 1025 cons (chr #"w") (chr #"W"); cons (chr #"x") (chr #"X"); 1026 cons (chr #"y") (chr #"Y"); cons (chr #"z") (chr #"Z")]) 1027 in 1028 itel [(pair,cdr pair); (characterp x,x)] (code_char (nat 0)))`; 1029 1030(* 1031 [oracles: DEFUN COMMON-LISP::CHAR-DOWNCASE, DISK_THM] [axioms: ] [] 1032 |- char_downcase x = 1033 (let pair = 1034 assoc x 1035 (List 1036 [cons (chr #"A") (chr #"a"); cons (chr #"B") (chr #"b"); 1037 cons (chr #"C") (chr #"c"); cons (chr #"D") (chr #"d"); 1038 cons (chr #"E") (chr #"e"); cons (chr #"F") (chr #"f"); 1039 cons (chr #"G") (chr #"g"); cons (chr #"H") (chr #"h"); 1040 cons (chr #"I") (chr #"i"); cons (chr #"J") (chr #"j"); 1041 cons (chr #"K") (chr #"k"); cons (chr #"L") (chr #"l"); 1042 cons (chr #"M") (chr #"m"); cons (chr #"N") (chr #"n"); 1043 cons (chr #"O") (chr #"o"); cons (chr #"P") (chr #"p"); 1044 cons (chr #"Q") (chr #"q"); cons (chr #"R") (chr #"r"); 1045 cons (chr #"S") (chr #"s"); cons (chr #"T") (chr #"t"); 1046 cons (chr #"U") (chr #"u"); cons (chr #"V") (chr #"v"); 1047 cons (chr #"W") (chr #"w"); cons (chr #"X") (chr #"x"); 1048 cons (chr #"Y") (chr #"y"); cons (chr #"Z") (chr #"z")]) 1049 in 1050 itel [(pair,cdr pair); (characterp x,x)] (code_char (nat 0))), 1051*) 1052 1053val char_downcase_def = 1054 acl2Define "COMMON-LISP::CHAR-DOWNCASE" 1055 `char_downcase x = 1056 (let pair = 1057 assoc x 1058 (List 1059 [cons (chr #"A") (chr #"a"); cons (chr #"B") (chr #"b"); 1060 cons (chr #"C") (chr #"c"); cons (chr #"D") (chr #"d"); 1061 cons (chr #"E") (chr #"e"); cons (chr #"F") (chr #"f"); 1062 cons (chr #"G") (chr #"g"); cons (chr #"H") (chr #"h"); 1063 cons (chr #"I") (chr #"i"); cons (chr #"J") (chr #"j"); 1064 cons (chr #"K") (chr #"k"); cons (chr #"L") (chr #"l"); 1065 cons (chr #"M") (chr #"m"); cons (chr #"N") (chr #"n"); 1066 cons (chr #"O") (chr #"o"); cons (chr #"P") (chr #"p"); 1067 cons (chr #"Q") (chr #"q"); cons (chr #"R") (chr #"r"); 1068 cons (chr #"S") (chr #"s"); cons (chr #"T") (chr #"t"); 1069 cons (chr #"U") (chr #"u"); cons (chr #"V") (chr #"v"); 1070 cons (chr #"W") (chr #"w"); cons (chr #"X") (chr #"x"); 1071 cons (chr #"Y") (chr #"y"); cons (chr #"Z") (chr #"z")]) 1072 in 1073 itel [(pair,cdr pair); (characterp x,x)] (code_char (nat 0)))`; 1074 1075(* 1076 [oracles: DEFUN ACL2::STRING-DOWNCASE1, DISK_THM] [axioms: ] [] 1077 |- string_downcase1 l = 1078 ite (atom l) nil 1079 (cons (char_downcase (car l)) (string_downcase1 (cdr l))), 1080*) 1081 1082val (string_downcase1_def,string_downcase1_ind) = 1083 acl2_defn "ACL2::STRING-DOWNCASE1" 1084 (`string_downcase1 l = 1085 ite (atom l) nil 1086 (cons (char_downcase (car l)) (string_downcase1 (cdr l)))`, 1087 WF_REL_TAC `measure sexp_size` 1088 THEN ACL2_SIMP_TAC []); 1089 1090(* 1091 [oracles: DEFUN COMMON-LISP::STRING-DOWNCASE, DISK_THM] [axioms: ] [] 1092 |- string_downcase x = 1093 coerce (string_downcase1 (coerce x (csym "LIST"))) (csym "STRING"), 1094*) 1095 1096val string_downcase_def = 1097 acl2Define "COMMON-LISP::STRING-DOWNCASE" 1098 `string_downcase x = 1099 coerce (string_downcase1 (coerce x (csym "LIST"))) (csym "STRING")`; 1100 1101(* 1102 [oracles: DEFUN ACL2::STRING-UPCASE1, DISK_THM] [axioms: ] [] 1103 |- string_upcase1 l = 1104 ite (atom l) nil 1105 (cons (char_upcase (car l)) (string_upcase1 (cdr l))), 1106*) 1107 1108val (string_upcase1_def,string_upcase1_ind) = 1109 acl2_defn "ACL2::STRING-UPCASE1" 1110 (`string_upcase1 l = 1111 ite (atom l) nil 1112 (cons (char_upcase (car l)) (string_upcase1 (cdr l)))`, 1113 WF_REL_TAC `measure sexp_size` 1114 THEN ACL2_SIMP_TAC []); 1115 1116(* 1117 [oracles: DEFUN COMMON-LISP::STRING-UPCASE, DISK_THM] [axioms: ] [] 1118 |- string_upcase x = 1119 coerce (string_upcase1 (coerce x (csym "LIST"))) (csym "STRING"), 1120*) 1121 1122val string_upcase_def = 1123 acl2Define "COMMON-LISP::STRING-UPCASE" 1124 `string_upcase x = 1125 coerce (string_upcase1 (coerce x (csym "LIST"))) (csym "STRING")`; 1126 1127(* 1128 [oracles: DEFUN ACL2::OUR-DIGIT-CHAR-P, DISK_THM] [axioms: ] [] 1129 |- our_digit_char_p ch radix = 1130 (let l = 1131 assoc ch 1132 (List 1133 [cons (chr #"0") (nat 0); cons (chr #"1") (nat 1); 1134 cons (chr #"2") (nat 2); cons (chr #"3") (nat 3); 1135 cons (chr #"4") (nat 4); cons (chr #"5") (nat 5); 1136 cons (chr #"6") (nat 6); cons (chr #"7") (nat 7); 1137 cons (chr #"8") (nat 8); cons (chr #"9") (nat 9); 1138 cons (chr #"a") (nat 10); cons (chr #"b") (nat 11); 1139 cons (chr #"c") (nat 12); cons (chr #"d") (nat 13); 1140 cons (chr #"e") (nat 14); cons (chr #"f") (nat 15); 1141 cons (chr #"g") (nat 16); cons (chr #"h") (nat 17); 1142 cons (chr #"i") (nat 18); cons (chr #"j") (nat 19); 1143 cons (chr #"k") (nat 20); cons (chr #"l") (nat 21); 1144 cons (chr #"m") (nat 22); cons (chr #"n") (nat 23); 1145 cons (chr #"o") (nat 24); cons (chr #"p") (nat 25); 1146 cons (chr #"q") (nat 26); cons (chr #"r") (nat 27); 1147 cons (chr #"s") (nat 28); cons (chr #"t") (nat 29); 1148 cons (chr #"u") (nat 30); cons (chr #"v") (nat 31); 1149 cons (chr #"w") (nat 32); cons (chr #"x") (nat 33); 1150 cons (chr #"y") (nat 34); cons (chr #"z") (nat 35); 1151 cons (chr #"A") (nat 10); cons (chr #"B") (nat 11); 1152 cons (chr #"C") (nat 12); cons (chr #"D") (nat 13); 1153 cons (chr #"E") (nat 14); cons (chr #"F") (nat 15); 1154 cons (chr #"G") (nat 16); cons (chr #"H") (nat 17); 1155 cons (chr #"I") (nat 18); cons (chr #"J") (nat 19); 1156 cons (chr #"K") (nat 20); cons (chr #"L") (nat 21); 1157 cons (chr #"M") (nat 22); cons (chr #"N") (nat 23); 1158 cons (chr #"O") (nat 24); cons (chr #"P") (nat 25); 1159 cons (chr #"Q") (nat 26); cons (chr #"R") (nat 27); 1160 cons (chr #"S") (nat 28); cons (chr #"T") (nat 29); 1161 cons (chr #"U") (nat 30); cons (chr #"V") (nat 31); 1162 cons (chr #"W") (nat 32); cons (chr #"X") (nat 33); 1163 cons (chr #"Y") (nat 34); cons (chr #"Z") (nat 35)]) 1164 in 1165 andl [l; less (cdr l) radix; cdr l]), 1166*) 1167 1168val our_digit_char_p_def = 1169 acl2Define "ACL2::OUR-DIGIT-CHAR-P" 1170 `our_digit_char_p ch radix = 1171 (let l = assoc ch 1172 (List 1173 [cons (chr #"0") (nat 0); cons (chr #"1") (nat 1); 1174 cons (chr #"2") (nat 2); cons (chr #"3") (nat 3); 1175 cons (chr #"4") (nat 4); cons (chr #"5") (nat 5); 1176 cons (chr #"6") (nat 6); cons (chr #"7") (nat 7); 1177 cons (chr #"8") (nat 8); cons (chr #"9") (nat 9); 1178 cons (chr #"a") (nat 10); cons (chr #"b") (nat 11); 1179 cons (chr #"c") (nat 12); cons (chr #"d") (nat 13); 1180 cons (chr #"e") (nat 14); cons (chr #"f") (nat 15); 1181 cons (chr #"g") (nat 16); cons (chr #"h") (nat 17); 1182 cons (chr #"i") (nat 18); cons (chr #"j") (nat 19); 1183 cons (chr #"k") (nat 20); cons (chr #"l") (nat 21); 1184 cons (chr #"m") (nat 22); cons (chr #"n") (nat 23); 1185 cons (chr #"o") (nat 24); cons (chr #"p") (nat 25); 1186 cons (chr #"q") (nat 26); cons (chr #"r") (nat 27); 1187 cons (chr #"s") (nat 28); cons (chr #"t") (nat 29); 1188 cons (chr #"u") (nat 30); cons (chr #"v") (nat 31); 1189 cons (chr #"w") (nat 32); cons (chr #"x") (nat 33); 1190 cons (chr #"y") (nat 34); cons (chr #"z") (nat 35); 1191 cons (chr #"A") (nat 10); cons (chr #"B") (nat 11); 1192 cons (chr #"C") (nat 12); cons (chr #"D") (nat 13); 1193 cons (chr #"E") (nat 14); cons (chr #"F") (nat 15); 1194 cons (chr #"G") (nat 16); cons (chr #"H") (nat 17); 1195 cons (chr #"I") (nat 18); cons (chr #"J") (nat 19); 1196 cons (chr #"K") (nat 20); cons (chr #"L") (nat 21); 1197 cons (chr #"M") (nat 22); cons (chr #"N") (nat 23); 1198 cons (chr #"O") (nat 24); cons (chr #"P") (nat 25); 1199 cons (chr #"Q") (nat 26); cons (chr #"R") (nat 27); 1200 cons (chr #"S") (nat 28); cons (chr #"T") (nat 29); 1201 cons (chr #"U") (nat 30); cons (chr #"V") (nat 31); 1202 cons (chr #"W") (nat 32); cons (chr #"X") (nat 33); 1203 cons (chr #"Y") (nat 34); cons (chr #"Z") (nat 35)]) 1204 in 1205 andl [l; less (cdr l) radix; cdr l])`; 1206 1207(* 1208 [oracles: DEFUN COMMON-LISP::CHAR-EQUAL] [axioms: ] [] 1209 |- char_equal x y = eql (char_downcase x) (char_downcase y), 1210*) 1211 1212val char_equal_def = 1213 acl2Define "COMMON-LISP::CHAR-EQUAL" 1214 `char_equal x y = eql (char_downcase x) (char_downcase y)`; 1215 1216(* 1217 [oracles: DEFUN ACL2::ATOM-LISTP, DISK_THM] [axioms: ] [] 1218 |- atom_listp lst = 1219 ite (atom lst) (eq lst nil) 1220 (andl [atom (car lst); atom_listp (cdr lst)]), 1221*) 1222 1223val (atom_listp_def,atom_listp_ind) = 1224 acl2_defn "ACL2::ATOM-LISTP" 1225 (`atom_listp lst = 1226 ite (atom lst) (eq lst nil) 1227 (andl [atom (car lst); atom_listp (cdr lst)])`, 1228 WF_REL_TAC `measure sexp_size` 1229 THEN ACL2_SIMP_TAC []); 1230 1231(* 1232 [oracles: DEFUN ACL2::IFIX, DISK_THM] [axioms: ] [] 1233 |- ifix x = ite (integerp x) x (nat 0), 1234*) 1235 1236val ifix_def = 1237 acl2Define "ACL2::IFIX" 1238 `ifix x = ite (integerp x) x (nat 0)`; 1239 1240(* 1241 [oracles: DEFUN ACL2::RFIX, DISK_THM] [axioms: ] [] 1242 |- rfix x = ite (rationalp x) x (nat 0), 1243*) 1244 1245val rfix_def = 1246 acl2Define "ACL2::RFIX" 1247 `rfix x = ite (rationalp x) x (nat 0)`; 1248 1249(* 1250 [oracles: DEFUN ACL2::REALFIX, DISK_THM] [axioms: ] [] 1251 |- realfix x = ite (rationalp x) x (nat 0), 1252*) 1253 1254val realfix_def = 1255 acl2Define "ACL2::REALFIX" 1256 `realfix x = ite (rationalp x) x (nat 0)`; 1257 1258(* 1259 [oracles: DEFUN ACL2::NFIX, DISK_THM] [axioms: ] [] 1260 |- nfix x = ite (andl [integerp x; not (less x (nat 0))]) x (nat 0), 1261*) 1262 1263val nfix_def = 1264 acl2Define "ACL2::NFIX" 1265 `nfix x = ite (andl [integerp x; not (less x (nat 0))]) x (nat 0)`; 1266 1267(* 1268 [oracles: DEFUN ACL2::STRING-EQUAL1, DISK_THM] [axioms: ] [] 1269 |- string_equal1 str1 str2 i maximum = 1270 (let i = nfix i in 1271 ite (not (less i (ifix maximum))) t 1272 (andl 1273 [char_equal (char str1 i) (char str2 i); 1274 string_equal1 str1 str2 (add (nat 1) i) maximum])), 1275*) 1276 1277(* 1278 1279val sexp_to_num_def = 1280 Define 1281 `sexp_to_num s = @n. s = nat n`; 1282 1283Hol_defn "FOO" 1284 `string_equal1 str1 str2 i maximum = 1285 (let i = nfix i in 1286 ite (not (less i (ifix maximum))) t 1287 (andl 1288 [char_equal (char str1 i) (char str2 i); 1289 string_equal1 str1 str2 (add (nat 1) i) maximum]))`; 1290 1291Defn.tgoal it; 1292 1293e(WF_REL_TAC 1294 `measure(\(str1,str2,i,maximum). (sexp_to_num maximum - sexp_to_num i))`); 1295 1296e(RW_TAC std_ss 1297 [DECIDE ``0 < ((m:num) - n) = n < m``]); 1298 1299DECIDE ``p <= m ==> ((m:num) < n + (m - p) = p < n)``; 1300 1301val less_nat_ref = 1302 store_thm 1303 ("less_nat_ref", 1304 ``!n. less (nat n) (nat n) = nil``, 1305 ACL2_SIMP_TAC 1306 [nat_def,int_def,cpx_def, 1307 ratTheory.RAT_LES_REF]); 1308 1309val less_int_ref = 1310 store_thm 1311 ("less_int_ref", 1312 ``!n. less (int n) (int n) = nil``, 1313 ACL2_SIMP_TAC 1314 [nat_def,int_def,cpx_def, 1315 ratTheory.RAT_LES_REF]); 1316 1317val sexp_to_num_less = 1318 store_thm 1319 ("sexp_to_num_less", 1320 ``!m n. 1321 (not (less (nfix m) (ifix n)) = nil) 1322 ==> 1323 sexp_to_num m < sexp_to_num n`` 1324 Cases THEN Cases 1325 THEN ACL2_SIMP_TAC[nat_def,REWRITE_RULE[nil_def]less_int_ref] 1326 1327*) 1328 1329(* 1330 [oracles: DEFUN COMMON-LISP::STRING-EQUAL, DISK_THM] [axioms: ] [] 1331 |- string_equal str1 str2 = 1332 (let len1 = length str1 in 1333 andl 1334 [common_lisp_equal len1 (length str2); 1335 string_equal1 str1 str2 (nat 0) len1]), 1336*) 1337 1338(* 1339 [oracles: DEFUN ACL2::STANDARD-STRING-ALISTP, DISK_THM] [axioms: ] [] 1340 |- standard_string_alistp x = 1341 ite (atom x) (eq x nil) 1342 (andl 1343 [consp (car x); stringp (caar x); 1344 standard_char_listp (coerce (caar x) (csym "LIST")); 1345 standard_string_alistp (cdr x)]), 1346*) 1347 1348(* 1349 [oracles: DEFUN ACL2::ASSOC-STRING-EQUAL, DISK_THM] [axioms: ] [] 1350 |- assoc_string_equal acl2_str alist = 1351 itel 1352 [(endp alist,nil); (string_equal acl2_str (caar alist),car alist)] 1353 (assoc_string_equal acl2_str (cdr alist)), 1354*) 1355 1356(* 1357 [oracles: DEFUN ACL2::NATP, DISK_THM] [axioms: ] [] 1358 |- natp x = andl [integerp x; not (less x (nat 0))], 1359*) 1360 1361val natp_def = 1362 acl2Define "ACL2::NATP" 1363 `natp x = andl [integerp x; not (less x (nat 0))]`; 1364 1365(* 1366 [oracles: DEFUN ACL2::POSP, DISK_THM] [axioms: ] [] 1367 |- posp x = andl [integerp x; less (nat 0) x], 1368*) 1369 1370val posp_def = 1371 acl2Define "ACL2::POSP" 1372 `posp x = andl [integerp x; less (nat 0) x]`; 1373 1374(* 1375 [oracles: DEFUN ACL2::O-FINP] [axioms: ] [] |- o_finp x = atom x, 1376*) 1377 1378val o_finp_def = 1379 acl2Define "ACL2::O-FINP" 1380 `o_finp x = atom x`; 1381 1382(* 1383 [oracles: DEFUN ACL2::O-FIRST-EXPT, DISK_THM] [axioms: ] [] 1384 |- o_first_expt x = ite (o_finp x) (nat 0) (caar x), 1385*) 1386 1387val o_first_expt_def = 1388 acl2Define "ACL2::O-FIRST-EXPT" 1389 `o_first_expt x = ite (o_finp x) (nat 0) (caar x)`; 1390 1391 1392(*****************************************************************************) 1393(* Tell system that o_first_expt decreases size *) 1394(*****************************************************************************) 1395val sexp_size_o_first_expt = 1396 store_thm 1397 ("sexp_size_o_first_expt", 1398 ``!x. ~(consp x = nil) /\ ~(consp(car x) = nil) 1399 ==> 1400 (sexp_size (o_first_expt x) < sexp_size x)``, 1401 Cases 1402 THEN ACL2_SIMP_TAC[sexp_size_def] 1403 THEN FULL_SIMP_TAC arith_ss [GSYM nil_def] 1404 THEN METIS_TAC[sexp_size_car,DECIDE``m:num < n ==> !p. m < n+p``]); 1405 1406val _ = add_acl2_simps [sexp_size_o_first_expt]; 1407 1408(* 1409 [oracles: DEFUN ACL2::O-FIRST-COEFF, DISK_THM] [axioms: ] [] 1410 |- o_first_coeff x = ite (o_finp x) x (cdar x), 1411*) 1412 1413val o_first_coeff_def = 1414 acl2Define "ACL2::O-FIRST-COEFF" 1415 `o_first_coeff x = ite (o_finp x) x (cdar x)`; 1416 1417(*****************************************************************************) 1418(* Tell system that o_first_coeff decreases size *) 1419(*****************************************************************************) 1420val sexp_size_o_first_coeff = 1421 store_thm 1422 ("sexp_size_o_first_coeff", 1423 ``!x. ~(consp x = nil) /\ ~(consp(car x) = nil) 1424 ==> 1425 (sexp_size (o_first_coeff x) < sexp_size x)``, 1426 Cases 1427 THEN ACL2_SIMP_TAC[sexp_size_def] 1428 THEN FULL_SIMP_TAC arith_ss [GSYM nil_def] 1429 THEN METIS_TAC[sexp_size_cdr,DECIDE``m:num < n ==> !p. m < n+p``]); 1430 1431val _ = add_acl2_simps [sexp_size_o_first_coeff]; 1432 1433(* 1434 [oracles: DEFUN ACL2::O-RST] [axioms: ] [] |- o_rst x = cdr x, 1435*) 1436 1437val o_rst_def = 1438 acl2Define "ACL2::O-RST" 1439 `o_rst x = cdr x`; 1440 1441(*****************************************************************************) 1442(* Tell system that o_rest decreases size *) 1443(*****************************************************************************) 1444val sexp_size_o_rst = 1445 store_thm 1446 ("sexp_size_o_rst", 1447 ``!x. ~(consp x = nil) ==> (sexp_size (o_rst x) < sexp_size x)``, 1448 ACL2_SIMP_TAC[]); 1449 1450val _ = add_acl2_simps [sexp_size_o_rst]; 1451 1452(* 1453 [oracles: DEFUN ACL2::O<G, DISK_THM] [axioms: ] [] 1454 |- o_less_g x = 1455 ite (atom x) (rationalp x) 1456 (andl 1457 [consp (car x); rationalp (o_first_coeff x); 1458 o_less_g (o_first_expt x); o_less_g (o_rst x)]), 1459*) 1460 1461(* 1462 [oracles: DEFUN ACL2::O<, DISK_THM] [axioms: ] [] 1463 |- o_less x y = 1464 itel 1465 [(o_finp x,ite (not (o_finp y)) (not (o_finp y)) (less x y)); 1466 (o_finp y,nil); 1467 (not (equal (o_first_expt x) (o_first_expt y)), 1468 o_less (o_first_expt x) (o_first_expt y)); 1469 (not (common_lisp_equal (o_first_coeff x) (o_first_coeff y)), 1470 less (o_first_coeff x) (o_first_coeff y))] 1471 (o_less (o_rst x) (o_rst y)), 1472*) 1473 1474(* 1475 [oracles: DEFUN ACL2::O-P, DISK_THM] [axioms: ] [] 1476 |- o_p x = 1477 ite (o_finp x) (natp x) 1478 (andl 1479 [consp (car x); o_p (o_first_expt x); 1480 not (eql (nat 0) (o_first_expt x)); posp (o_first_coeff x); 1481 o_p (o_rst x); 1482 o_less (o_first_expt (o_rst x)) (o_first_expt x)]), 1483*) 1484 1485(* 1486Need help from a TFL expert for this. I suspect need to add 1487something with more oomph than andl_CONG for Defn Base to exploit 1488sexp_size_o_first_expt and sexp_size_o_rst 1489 1490acl2_tgoal "ACL2::O-P" 1491 `o_p x = 1492 ite (o_finp x) (natp x) 1493 (andl 1494 [consp (car x); o_p (o_first_expt x); 1495 not (eql (nat 0) (o_first_expt x)); posp (o_first_coeff x); 1496 o_p (o_rst x); 1497 o_less (o_first_expt (o_rst x)) (o_first_expt x)])`; 1498 1499> val it = 1500 Initial goal: 1501 1502 ?R. 1503 WF R /\ (!x. (o_finp x = nil) ==> R (o_first_expt x) x) /\ 1504 !x. (o_finp x = nil) ==> R (o_rst x) x 1505 1506 : goalstack 1507 1508- e(WF_REL_TAC `measure sexp_size`); 1509OK.. 15101 subgoal: 1511> val it = 1512 (!x. (o_finp x = nil) ==> sexp_size (o_first_expt x) < sexp_size x) /\ 1513 !x. (o_finp x = nil) ==> sexp_size (o_rst x) < sexp_size x 1514 1515 : goalstack 1516 1517- sexp_size_o_first_expt; 1518> val it = 1519 |- !x. 1520 ~(consp x = nil) /\ ~(consp (car x) = nil) ==> 1521 sexp_size (o_first_expt x) < sexp_size x : thm 1522 1523- sexp_size_o_rst; 1524> val it = |- !x. ~(consp x = nil) ==> sexp_size (o_rst x) < sexp_size x : thm 1525 1526e(WF_REL_TAC `measure sexp_size`); 1527 1528val (o_p_def,o_p_ind) = 1529 acl2_defn "ACL2::O-P" 1530 (`o_p x = 1531 ite (o_finp x) (natp x) 1532 (andl 1533 [consp (car x); o_p (o_first_expt x); 1534 not (eql (nat 0) (o_first_expt x)); posp (o_first_coeff x); 1535 o_p (o_rst x); 1536 o_less (o_first_expt (o_rst x)) (o_first_expt x)])`, 1537 WF_REL_TAC `measure sexp_size` 1538 THEN ACL2_SIMP_TAC [o_finp_def] 1539 THEN FULL_SIMP_TAC std_ss [GSYM nil_def] 1540*) 1541 1542(* 1543 [oracles: DEFUN ACL2::MAKE-ORD] [axioms: ] [] 1544 |- make_ord fe fco rst = cons (cons fe fco) rst, 1545*) 1546 1547(* 1548 1549 [oracles: DEFUN ACL2::LIST*-MACRO] [axioms: ] [] 1550 |- list_star_macro lst = 1551 ite (endp (cdr lst)) (car lst) 1552 (cons (sym COMMON_LISP ACL2_STRING_ABBREV_714) 1553 (cons (car lst) (cons (list_star_macro (cdr lst)) nil))) 1554*) 1555 1556(* 1557 [oracles: DEFUN ACL2::HARD-ERROR] [axioms: ] [] 1558 |- hard_error ctx acl2_str alist = nil, 1559*) 1560 1561(* 1562 [oracles: DEFUN ACL2::ILLEGAL] [axioms: ] [] 1563 |- illegal ctx acl2_str alist = hard_error ctx acl2_str alist, 1564*) 1565 1566(* 1567 [oracles: DEFUN COMMON-LISP::KEYWORDP, DISK_THM] [axioms: ] [] 1568 |- keywordp x = 1569 andl [symbolp x; equal (symbol_package_name x) (str KEYWORD)], 1570*) 1571 1572(* 1573 [oracles: DEFUN ACL2::MEMBER-SYMBOL-NAME, DISK_THM] [axioms: ] [] 1574 |- member_symbol_name acl2_str l = 1575 itel [(endp l,nil); (equal acl2_str (symbol_name (car l)),l)] 1576 (member_symbol_name acl2_str (cdr l)), 1577*) 1578 1579val (member_symbol_name_def,member_symbol_name_ind) = 1580 acl2_defn "ACL2::MEMBER-SYMBOL-NAME" 1581 (`member_symbol_name acl2_str l = 1582 itel [(endp l,nil); (equal acl2_str (symbol_name (car l)),l)] 1583 (member_symbol_name acl2_str (cdr l))`, 1584 WF_REL_TAC `measure (sexp_size o SND)` 1585 THEN ACL2_SIMP_TAC []); 1586 1587(* 1588 [oracles: DEFUN ACL2::BINARY-APPEND, DISK_THM] [axioms: ] [] 1589 |- binary_append x y = 1590 ite (endp x) y (cons (car x) (binary_append (cdr x) y)), 1591*) 1592 1593val (binary_append_def,binary_append_ind) = 1594 acl2_defn "ACL2::BINARY-APPEND" 1595 (`binary_append x y = 1596 ite (endp x) y (cons (car x) (binary_append (cdr x) y))`, 1597 WF_REL_TAC `measure (sexp_size o FST)` 1598 THEN ACL2_SIMP_TAC []); 1599 1600(* 1601 [oracles: DEFUN ACL2::STRING-APPEND, DISK_THM] [axioms: ] [] 1602 |- string_append str1 str2 = 1603 coerce 1604 (binary_append (coerce str1 (csym "LIST")) 1605 (coerce str2 (csym "LIST"))) (csym "STRING"), 1606*) 1607 1608(* 1609 [oracles: DEFUN ACL2::STRING-LISTP, DISK_THM] [axioms: ] [] 1610 |- string_listp x = 1611 ite (atom x) (eq x nil) 1612 (andl [stringp (car x); string_listp (cdr x)]), 1613*) 1614 1615(* 1616 [oracles: DEFUN ACL2::STRING-APPEND-LST, DISK_THM] [axioms: ] [] 1617 |- string_append_lst x = 1618 ite (endp x) (str "") 1619 (string_append (car x) (string_append_lst (cdr x))), 1620*) 1621 1622(* 1623 [oracles: DEFUN COMMON-LISP::REMOVE, DISK_THM] [axioms: ] [] 1624 |- remove x l = 1625 itel [(endp l,nil); (eql x (car l),remove x (cdr l))] 1626 (cons (car l) (remove x (cdr l))), 1627*) 1628 1629(* 1630 [oracles: DEFUN ACL2::PAIRLIS$, DISK_THM] [axioms: ] [] 1631 |- pairlis_dollar x y = 1632 ite (endp x) nil 1633 (cons (cons (car x) (car y)) (pairlis_dollar (cdr x) (cdr y))), 1634*) 1635 1636(* 1637 [oracles: DEFUN ACL2::REMOVE-DUPLICATES-EQL, DISK_THM] [axioms: ] [] 1638 |- remove_duplicates_eql l = 1639 itel 1640 [(endp l,nil); 1641 (member (car l) (cdr l),remove_duplicates_eql (cdr l))] 1642 (cons (car l) (remove_duplicates_eql (cdr l))), 1643*) 1644 1645(* 1646 [oracles: DEFUN COMMON-LISP::REMOVE-DUPLICATES, DISK_THM] [axioms: ] [] 1647 |- remove_duplicates l = 1648 ite (stringp l) 1649 (coerce (remove_duplicates_eql (coerce l (csym "LIST"))) 1650 (csym "STRING")) (remove_duplicates_eql l), 1651*) 1652 1653(* 1654 [oracles: DEFUN ACL2::REMOVE-DUPLICATES-EQUAL, DISK_THM] [axioms: ] [] 1655 |- remove_duplicates_equal l = 1656 itel 1657 [(endp l,nil); 1658 (member_equal (car l) (cdr l),remove_duplicates_equal (cdr l))] 1659 (cons (car l) (remove_duplicates_equal (cdr l))), 1660*) 1661 1662(* 1663 [oracles: DEFUN COMMON-LISP::IDENTITY] [axioms: ] [] |- identity x = x, 1664*) 1665 1666(* 1667 [oracles: DEFUN COMMON-LISP::REVAPPEND, DISK_THM] [axioms: ] [] 1668 |- revappend x y = ite (endp x) y (revappend (cdr x) (cons (car x) y)), 1669*) 1670 1671(* 1672 [oracles: DEFUN COMMON-LISP::REVERSE, DISK_THM] [axioms: ] [] 1673 |- reverse x = 1674 ite (stringp x) 1675 (coerce (revappend (coerce x (csym "LIST")) nil) (csym "STRING")) 1676 (revappend x nil), 1677*) 1678 1679(* 1680 [oracles: DEFUN ACL2::SET-DIFFERENCE-EQ, DISK_THM] [axioms: ] [] 1681 |- set_difference_eq l1 l2 = 1682 itel 1683 [(endp l1,nil); 1684 (member_eq (car l1) l2,set_difference_eq (cdr l1) l2)] 1685 (cons (car l1) (set_difference_eq (cdr l1) l2)), 1686*) 1687 1688(* 1689 [oracles: DEFUN ACL2::STRIP-CDRS, DISK_THM] [axioms: ] [] 1690 |- strip_cdrs x = ite (endp x) nil (cons (cdar x) (strip_cdrs (cdr x))), 1691*) 1692 1693(* 1694 [oracles: DEFUN ACL2::MUTUAL-RECURSION-GUARDP, DISK_THM] [axioms: ] [] 1695 |- mutual_recursion_guardp rst = 1696 ite (atom rst) (equal rst nil) 1697 (andl 1698 [consp (car rst); true_listp (car rst); 1699 member_eq (caar rst) (List [csym "DEFUN"; asym "DEFUND"]); 1700 mutual_recursion_guardp (cdr rst)]), 1701*) 1702 1703(* 1704 [oracles: DEFUN ACL2::COLLECT-CADRS-WHEN-CAR-EQ, DISK_THM] [axioms: ] [] 1705 |- collect_cadrs_when_car_eq x alist = 1706 itel 1707 [(endp alist,nil); 1708 (eq x (caar alist), 1709 cons (cadar alist) (collect_cadrs_when_car_eq x (cdr alist)))] 1710 (collect_cadrs_when_car_eq x (cdr alist)), 1711*) 1712 1713(* 1714 [oracles: DEFUN ACL2::XD-NAME, DISK_THM] [axioms: ] [] 1715 |- xd_name event_type name = 1716 itel 1717 [(eq event_type (asym "DEFUND"),List [ksym "DEFUND"; name]); 1718 (eq event_type (asym "DEFTHMD"),List [ksym "DEFTHMD"; name])] 1719 (illegal (asym "XD-NAME") 1720 (str "Unexpected event-type for xd-name, %x0") 1721 (List [cons (chr #"0") event_type])), 1722*) 1723 1724(* 1725 [oracles: DEFUN ACL2::DEFUND-NAME-LIST, DISK_THM] [axioms: ] [] 1726 |- defund_name_list defuns acc = 1727 ite (endp defuns) (reverse acc) 1728 (defund_name_list (cdr defuns) 1729 (cons 1730 (ite (eq (caar defuns) (asym "DEFUND")) 1731 (xd_name (asym "DEFUND") (cadar defuns)) (cadar defuns)) 1732 acc)), 1733*) 1734 1735(* 1736 [oracles: DEFUN ACL2::PSEUDO-TERM-LISTP, DISK_THM] [axioms: ] [] 1737 |- pseudo_term_listp lst = 1738 ite (atom lst) (equal lst nil) 1739 (andl [pseudo_termp (car lst); pseudo_term_listp (cdr lst)]), 1740*) 1741 1742(* 1743 [oracles: DEFUN ACL2::PSEUDO-TERMP, DISK_THM] [axioms: ] [] 1744 |- pseudo_termp x = 1745 itel 1746 [(atom x,symbolp x); 1747 (eq (car x) (csym "QUOTE"),andl [consp (cdr x); null (cddr x)]); 1748 (not (true_listp x),nil); (not (pseudo_term_listp (cdr x)),nil); 1749 (symbolp (car x),symbolp (car x))] 1750 (andl 1751 [true_listp (car x); equal (length (car x)) (nat 3); 1752 eq (caar x) (csym "LAMBDA"); symbol_listp (cadar x); 1753 pseudo_termp (caddar x); 1754 equal (length (cadar x)) (length (cdr x))]), 1755*) 1756 1757(* 1758 [oracles: DEFUN ACL2::PSEUDO-TERM-LIST-LISTP, DISK_THM] [axioms: ] [] 1759 |- pseudo_term_list_listp l = 1760 ite (atom l) (equal l nil) 1761 (andl [pseudo_term_listp (car l); pseudo_term_list_listp (cdr l)]), 1762*) 1763 1764(* 1765 [oracles: DEFUN ACL2::ADD-TO-SET-EQ, DISK_THM] [axioms: ] [] 1766 |- add_to_set_eq x lst = ite (member_eq x lst) lst (cons x lst), 1767*) 1768 1769(* 1770 [oracles: DEFUN ACL2::ADD-TO-SET-EQL, DISK_THM] [axioms: ] [] 1771 |- add_to_set_eql x lst = ite (member x lst) lst (cons x lst), 1772*) 1773 1774(* 1775 [oracles: DEFUN ACL2::QUOTEP, DISK_THM] [axioms: ] [] 1776 |- quotep x = andl [consp x; eq (car x) (csym "QUOTE")], 1777*) 1778 1779(* 1780 [oracles: DEFUN ACL2::KWOTE, DISK_THM] [axioms: ] [] 1781 |- kwote x = List [csym "QUOTE"; x], 1782*) 1783 1784(* 1785 [oracles: DEFUN ACL2::FN-SYMB, DISK_THM] [axioms: ] [] 1786 |- fn_symb x = andl [consp x; not (eq (csym "QUOTE") (car x)); car x], 1787*) 1788 1789(* 1790 [oracles: DEFUN ACL2::ALL-VARS1-LST, DISK_THM] [axioms: ] [] 1791 |- all_vars1_lst lst ans = 1792 ite (endp lst) ans 1793 (all_vars1_lst (cdr lst) (all_vars1 (car lst) ans)), 1794*) 1795 1796(* 1797 [oracles: DEFUN ACL2::ALL-VARS1, DISK_THM] [axioms: ] [] 1798 |- all_vars1 term ans = 1799 itel 1800 [(atom term,add_to_set_eq term ans); 1801 (eq (csym "QUOTE") (car term),ans)] (all_vars1_lst (cdr term) ans), 1802*) 1803 1804(* 1805 [oracles: DEFUN ACL2::ALL-VARS] [axioms: ] [] 1806 |- all_vars term = all_vars1 term nil, 1807*) 1808 1809(* 1810 [oracles: DEFUN ACL2::INTERSECTP-EQ, DISK_THM] [axioms: ] [] 1811 |- intersectp_eq x y = 1812 itel [(endp x,nil); (member_eq (car x) y,t)] 1813 (intersectp_eq (cdr x) y), 1814*) 1815 1816(* 1817 [oracles: DEFUN ACL2::INTERSECTP-EQUAL, DISK_THM] [axioms: ] [] 1818 |- intersectp_equal x y = 1819 itel [(endp x,nil); (member_equal (car x) y,t)] 1820 (intersectp_equal (cdr x) y), 1821*) 1822 1823(* 1824 [oracles: DEFUN ACL2::MAKE-FMT-BINDINGS, DISK_THM] [axioms: ] [] 1825 |- make_fmt_bindings chars forms = 1826 ite (endp forms) nil 1827 (List 1828 [csym "CONS"; List [csym "CONS"; car chars; car forms]; 1829 make_fmt_bindings (cdr chars) (cdr forms)]), 1830*) 1831 1832(* 1833 [oracles: DEFUN ACL2::ER-PROGN-FN, DISK_THM] [axioms: ] [] 1834 |- er_progn_fn lst = 1835 itel [(endp lst,nil); (endp (cdr lst),car lst)] 1836 (List 1837 [asym "MV-LET"; 1838 List 1839 [asym "ER-PROGN-NOT-TO-BE-USED-ELSEWHERE-ERP"; 1840 asym "ER-PROGN-NOT-TO-BE-USED-ELSEWHERE-VAL"; asym "STATE"]; 1841 car lst; 1842 List 1843 [csym "IF"; asym "ER-PROGN-NOT-TO-BE-USED-ELSEWHERE-ERP"; 1844 List 1845 [asym "MV"; asym "ER-PROGN-NOT-TO-BE-USED-ELSEWHERE-ERP"; 1846 asym "ER-PROGN-NOT-TO-BE-USED-ELSEWHERE-VAL"; 1847 asym "STATE"]; 1848 List 1849 [asym "CHECK-VARS-NOT-FREE"; 1850 List 1851 [asym "ER-PROGN-NOT-TO-BE-USED-ELSEWHERE-ERP"; 1852 asym "ER-PROGN-NOT-TO-BE-USED-ELSEWHERE-VAL"]; 1853 er_progn_fn (cdr lst)]]]), 1854*) 1855 1856(* 1857 [oracles: DEFUN ACL2::LEGAL-CASE-CLAUSESP, DISK_THM] [axioms: ] [] 1858 |- legal_case_clausesp tl = 1859 ite (atom tl) (eq tl nil) 1860 (andl 1861 [consp (car tl); 1862 ite (eqlablep (caar tl)) (eqlablep (caar tl)) 1863 (eqlable_listp (caar tl)); consp (cdar tl); null (cddar tl); 1864 ite 1865 (ite (eq t (caar tl)) (eq t (caar tl)) 1866 (eq (csym "OTHERWISE") (caar tl))) (null (cdr tl)) t; 1867 legal_case_clausesp (cdr tl)]), 1868*) 1869 1870(* 1871 [oracles: DEFUN ACL2::CASE-TEST, DISK_THM] [axioms: ] [] 1872 |- case_test x pat = 1873 ite (atom pat) (List [csym "EQL"; x; List [csym "QUOTE"; pat]]) 1874 (List [csym "MEMBER"; x; List [csym "QUOTE"; pat]]), 1875*) 1876 1877(* 1878 [oracles: DEFUN ACL2::CASE-LIST, DISK_THM] [axioms: ] [] 1879 |- case_list x l = 1880 itel 1881 [(endp l,nil); 1882 (ite (eq t (caar l)) (eq t (caar l)) 1883 (eq (csym "OTHERWISE") (caar l)),List [List [t; cadar l]]); 1884 (null (caar l),case_list x (cdr l))] 1885 (cons (List [case_test x (caar l); cadar l]) (case_list x (cdr l))), 1886*) 1887 1888(* 1889 [oracles: DEFUN ACL2::CASE-LIST-CHECK, DISK_THM] [axioms: ] [] 1890 |- case_list_check l = 1891 itel 1892 [(endp l,nil); 1893 (ite (eq t (caar l)) (eq t (caar l)) 1894 (eq (csym "OTHERWISE") (caar l)), 1895 List 1896 [List 1897 [t; 1898 List 1899 [asym "CHECK-VARS-NOT-FREE"; 1900 List [asym "CASE-DO-NOT-USE-ELSEWHERE"]; cadar l]]]); 1901 (null (caar l),case_list_check (cdr l))] 1902 (cons 1903 (List 1904 [case_test (asym "CASE-DO-NOT-USE-ELSEWHERE") (caar l); 1905 List 1906 [asym "CHECK-VARS-NOT-FREE"; 1907 List [asym "CASE-DO-NOT-USE-ELSEWHERE"]; cadar l]]) 1908 (case_list_check (cdr l))), 1909*) 1910 1911(* 1912 [oracles: DEFUN ACL2::POSITION-EQUAL-AC, DISK_THM] [axioms: ] [] 1913 |- position_equal_ac item lst acc = 1914 itel [(endp lst,nil); (equal item (car lst),acc)] 1915 (position_equal_ac item (cdr lst) (add (nat 1) acc)), 1916*) 1917 1918(* 1919 [oracles: DEFUN ACL2::POSITION-AC, DISK_THM] [axioms: ] [] 1920 |- position_ac item lst acc = 1921 itel [(endp lst,nil); (eql item (car lst),acc)] 1922 (position_ac item (cdr lst) (add (nat 1) acc)), 1923*) 1924 1925(* 1926 [oracles: DEFUN ACL2::POSITION-EQUAL, DISK_THM] [axioms: ] [] 1927 |- position_equal item lst = 1928 ite (stringp lst) 1929 (position_ac item (coerce lst (csym "LIST")) (nat 0)) 1930 (position_equal_ac item lst (nat 0)), 1931*) 1932 1933(* 1934 [oracles: DEFUN ACL2::POSITION-EQ-AC, DISK_THM] [axioms: ] [] 1935 |- position_eq_ac item lst acc = 1936 itel [(endp lst,nil); (eq item (car lst),acc)] 1937 (position_eq_ac item (cdr lst) (add (nat 1) acc)), 1938*) 1939 1940(* 1941 [oracles: DEFUN ACL2::POSITION-EQ, DISK_THM] [axioms: ] [] 1942 |- position_eq item lst = position_eq_ac item lst (nat 0), 1943*) 1944 1945(* 1946 [oracles: DEFUN COMMON-LISP::POSITION, DISK_THM] [axioms: ] [] 1947 |- position item lst = 1948 ite (stringp lst) 1949 (position_ac item (coerce lst (csym "LIST")) (nat 0)) 1950 (position_ac item lst (nat 0)), 1951*) 1952 1953(* 1954 [oracles: DEFUN ACL2::NONNEGATIVE-INTEGER-QUOTIENT, DISK_THM] [axioms: ] 1955 [] 1956 |- nonnegative_integer_quotient i j = 1957 ite 1958 (ite (common_lisp_equal (nfix j) (nat 0)) 1959 (common_lisp_equal (nfix j) (nat 0)) (less (ifix i) j)) (nat 0) 1960 (add (nat 1) 1961 (nonnegative_integer_quotient (add i (unary_minus j)) j)), 1962*) 1963 1964val nonnegative_integer_quotient_def = 1965 acl2AxiomDefine "ACL2::NONNEGATIVE-INTEGER-QUOTIENT" 1966 `nonnegative_integer_quotient i j = 1967 ite 1968 (ite (common_lisp_equal (nfix j) (nat 0)) 1969 (common_lisp_equal (nfix j) (nat 0)) (less (ifix i) j)) (nat 0) 1970 (add (nat 1) 1971 (nonnegative_integer_quotient (add i (unary_minus j)) j))`; 1972 1973 1974(* 1975 [oracles: DEFUN ACL2::LEGAL-LET*-P] [axioms: ] [] 1976 |- legal_let_star_p bindings ignore_vars ignored_seen top_form = 1977 ite (endp bindings) 1978 (ite (eq ignore_vars nil) (eq ignore_vars nil) 1979 (hard_error (sym COMMON_LISP ACL2_STRING_ABBREV_453) 1980 (str 1981 "All variables declared IGNOREd in a LET* form must ~\n be bound, but ~&0 ~#0~[is~/are~] not bound in the ~\n form ~x1.") 1982 (cons (cons (chr #"0") ignore_vars) 1983 (cons (cons (chr #"1") top_form) nil)))) 1984 (ite (member_eq (car (car bindings)) ignored_seen) 1985 (hard_error (sym COMMON_LISP ACL2_STRING_ABBREV_453) 1986 (str 1987 "A variable bound twice in a LET* form may not be ~\n declared ignored. However, the variable ~x0 is bound in ~\n the form ~x1 and yet is declared ignored.") 1988 (cons (cons (chr #"0") (car (car bindings))) 1989 (cons (cons (chr #"1") top_form) nil))) 1990 (ite (member_eq (car (car bindings)) ignore_vars) 1991 (legal_let_star_p (cdr bindings) 1992 (remove (car (car bindings)) ignore_vars) 1993 (cons (car (car bindings)) ignored_seen) top_form) 1994 (legal_let_star_p (cdr bindings) ignore_vars ignored_seen 1995 top_form))) 1996*) 1997 1998(* 1999 [oracles: DEFUN ACL2::LET*-MACRO, DISK_THM] [axioms: ] [] 2000 |- let_star_macro bindings ignore_vars body = 2001 ite (ite (endp bindings) (endp bindings) (endp (cdr bindings))) 2002 (cons (sym COMMON_LISP ACL2_STRING_ABBREV_455) 2003 (cons bindings 2004 (ite ignore_vars 2005 (cons 2006 (cons (sym COMMON_LISP ACL2_STRING_ABBREV_755) 2007 (cons 2008 (cons (sym COMMON_LISP ACL2_STRING_ABBREV_555) 2009 ignore_vars) nil)) (cons body nil)) 2010 (cons body nil)))) 2011 (cons (sym COMMON_LISP ACL2_STRING_ABBREV_455) 2012 (cons (cons (car bindings) nil) 2013 (let (rest,ignore_vars,bindings) = 2014 (let_star_macro (cdr bindings) 2015 (remove (car (car bindings)) ignore_vars) body, 2016 ignore_vars,bindings) 2017 in 2018 ite (member_eq (car (car bindings)) ignore_vars) 2019 (cons 2020 (cons (sym COMMON_LISP ACL2_STRING_ABBREV_755) 2021 (cons 2022 (cons (sym COMMON_LISP ACL2_STRING_ABBREV_555) 2023 (cons (car (car bindings)) nil)) nil)) 2024 (cons rest nil)) (cons rest nil)))) 2025*) 2026 2027(* 2028 [oracles: DEFUN COMMON-LISP::FLOOR, DISK_THM] [axioms: ] [] 2029 |- floor i j = 2030 (let q = mult i (reciprocal j) in 2031 let n = numerator q in 2032 let d = denominator q in 2033 itel 2034 [(common_lisp_equal d (nat 1),n); 2035 (not (less n (nat 0)),nonnegative_integer_quotient n d)] 2036 (add 2037 (unary_minus 2038 (nonnegative_integer_quotient (unary_minus n) d)) 2039 (int ~1))), 2040*) 2041 2042val floor_def = 2043 acl2Define "COMMON-LISP::FLOOR" 2044 `floor i j = 2045 (let q = mult i (reciprocal j) in 2046 let n = numerator q in 2047 let d = denominator q in 2048 itel 2049 [(common_lisp_equal d (nat 1),n); 2050 (not (less n (nat 0)),nonnegative_integer_quotient n d)] 2051 (add 2052 (unary_minus 2053 (nonnegative_integer_quotient (unary_minus n) d)) 2054 (int ~1)))`; 2055 2056 2057(* 2058 [oracles: DEFUN COMMON-LISP::CEILING, DISK_THM] [axioms: ] [] 2059 |- ceiling i j = 2060 (let q = mult i (reciprocal j) in 2061 let n = numerator q in 2062 let d = denominator q in 2063 itel 2064 [(common_lisp_equal d (nat 1),n); 2065 (not (less n (nat 0)), 2066 add (nonnegative_integer_quotient n d) (nat 1))] 2067 (unary_minus (nonnegative_integer_quotient (unary_minus n) d))), 2068*) 2069 2070(* 2071 [oracles: DEFUN COMMON-LISP::TRUNCATE, DISK_THM] [axioms: ] [] 2072 |- truncate i j = 2073 (let q = mult i (reciprocal j) in 2074 let n = numerator q in 2075 let d = denominator q in 2076 itel 2077 [(common_lisp_equal d (nat 1),n); 2078 (not (less n (nat 0)),nonnegative_integer_quotient n d)] 2079 (unary_minus (nonnegative_integer_quotient (unary_minus n) d))), 2080*) 2081 2082(* 2083 [oracles: DEFUN COMMON-LISP::ROUND, DISK_THM] [axioms: ] [] 2084 |- round i j = 2085 (let q = mult i (reciprocal j) in 2086 itel 2087 [(integerp q,q); 2088 (not (less q (nat 0)), 2089 (let fl = floor q (nat 1) in 2090 let remainder = add q (unary_minus fl) in 2091 itel 2092 [(less (cpx 1 2 0 1) remainder,add fl (nat 1)); 2093 (less remainder (cpx 1 2 0 1),fl); 2094 (integerp (mult fl (reciprocal (nat 2))),fl)] 2095 (add fl (nat 1))))] 2096 (let cl = ceiling q (nat 1) in 2097 let remainder = add q (unary_minus cl) in 2098 itel 2099 [(less (cpx (~1) 2 0 1) remainder,cl); 2100 (less remainder (cpx (~1) 2 0 1),add cl (int ~1)); 2101 (integerp (mult cl (reciprocal (nat 2))),cl)] 2102 (add cl (int ~1)))), 2103*) 2104 2105(* 2106 [oracles: DEFUN COMMON-LISP::MOD] [axioms: ] [] 2107 |- mod x y = add x (unary_minus (mult (floor x y) y)), 2108 2109Needs FLOOR 2110 2111val mod_def = 2112 acl2Define "COMMON-LISP::MOD" 2113 `mod x y = add x (unary_minus (mult (floor x y) y))`; 2114*) 2115 2116val mod_def = 2117 acl2Define "COMMON-LISP::MOD" 2118 `mod x y = add x (unary_minus (mult (floor x y) y))`; 2119 2120(* 2121 [oracles: DEFUN COMMON-LISP::REM] [axioms: ] [] 2122 |- x rem y = add x (unary_minus (mult (truncate x y) y)), 2123*) 2124 2125(* 2126 [oracles: DEFUN COMMON-LISP::EVENP, DISK_THM] [axioms: ] [] 2127 |- evenp x = integerp (mult x (reciprocal (nat 2))), 2128*) 2129 2130(* 2131 [oracles: DEFUN COMMON-LISP::ODDP] [axioms: ] [] 2132 |- oddp x = not (evenp x), 2133*) 2134 2135(* 2136 [oracles: DEFUN COMMON-LISP::ZEROP, DISK_THM] [axioms: ] [] 2137 |- zerop x = eql x (nat 0), 2138*) 2139 2140(* 2141 [oracles: DEFUN COMMON-LISP::PLUSP, DISK_THM] [axioms: ] [] 2142 |- plusp x = less (nat 0) x, 2143*) 2144 2145(* 2146 [oracles: DEFUN COMMON-LISP::MINUSP, DISK_THM] [axioms: ] [] 2147 |- minusp x = less x (nat 0), 2148*) 2149 2150(* 2151 [oracles: DEFUN COMMON-LISP::MIN, DISK_THM] [axioms: ] [] 2152 |- min x y = ite (less x y) x y, 2153*) 2154 2155(* 2156 [oracles: DEFUN COMMON-LISP::MAX, DISK_THM] [axioms: ] [] 2157 |- max x y = ite (less y x) x y, 2158*) 2159 2160(* 2161 [oracles: DEFUN COMMON-LISP::ABS, DISK_THM] [axioms: ] [] 2162 |- abs x = ite (minusp x) (unary_minus x) x, 2163*) 2164 2165(* 2166 [oracles: DEFUN COMMON-LISP::SIGNUM, DISK_THM] [axioms: ] [] 2167 |- signum x = itel [(zerop x,nat 0); (minusp x,int ~1)] (nat 1), 2168*) 2169 2170(* 2171 [oracles: DEFUN COMMON-LISP::LOGNOT, DISK_THM] [axioms: ] [] 2172 |- lognot i = add (unary_minus (ifix i)) (int ~1), 2173*) 2174 2175(* 2176 [oracles: DEFUN COMMON-LISP::EXPT, DISK_THM] [axioms: ] [] 2177 |- expt r i = 2178 itel 2179 [(zip i,nat 1); (common_lisp_equal (fix r) (nat 0),nat 0); 2180 (less (nat 0) i,mult r (expt r (add i (int ~1))))] 2181 (mult (reciprocal r) (expt r (add i (nat 1)))), 2182 2183> Matt says: The measure for (expt r i) is (abs (ifix i)). Intuitively, we count 2184> down for positive exponents and count up for negative exponents 2185 2186val (expt_def,expt_ind) = 2187 acl2_defn "COMMON-LISP::EXPT" 2188 (`expt r i = 2189 itel 2190 [(zip i,nat 1); (common_lisp_equal (fix r) (nat 0),nat 0); 2191 (less (nat 0) i,mult r (expt r (add i (int ~1))))] 2192 (mult (reciprocal r) (expt r (add i (nat 1))))`, 2193 WF_REL_TAC `measure (sexp_size o FST)` 2194 THEN ACL2_SIMP_TAC []); 2195*) 2196 2197val expt_def = 2198 acl2AxiomDefine "COMMON-LISP::EXPT" 2199 `expt r i = 2200 itel 2201 [(zip i,nat 1); (common_lisp_equal (fix r) (nat 0),nat 0); 2202 (less (nat 0) i,mult r (expt r (add i (int ~1))))] 2203 (mult (reciprocal r) (expt r (add i (nat 1))))`; 2204 2205(* 2206 [oracles: DEFUN COMMON-LISP::LOGCOUNT, DISK_THM] [axioms: ] [] 2207 |- logcount x = 2208 itel 2209 [(zip x,nat 0); (less x (nat 0),logcount (lognot x)); 2210 (evenp x,logcount (nonnegative_integer_quotient x (nat 2)))] 2211 (add (nat 1) (logcount (nonnegative_integer_quotient x (nat 2)))), 2212*) 2213 2214(* 2215 [oracles: DEFUN COMMON-LISP::LISTP, DISK_THM] [axioms: ] [] 2216 |- listp x = ite (consp x) (consp x) (equal x nil), 2217*) 2218 2219(* 2220 [oracles: DEFUN COMMON-LISP::NTHCDR, DISK_THM] [axioms: ] [] 2221 |- nthcdr n l = ite (zp n) l (nthcdr (add n (int ~1)) (cdr l)), 2222*) 2223 2224(* 2225 [oracles: DEFUN COMMON-LISP::LAST, DISK_THM] [axioms: ] [] 2226 |- last l = ite (atom (cdr l)) l (last (cdr l)), 2227*) 2228 2229(* 2230 [oracles: DEFUN COMMON-LISP::LOGBITP, DISK_THM] [axioms: ] [] 2231 |- logbitp i j = oddp (floor (ifix j) (expt (nat 2) (nfix i))), 2232*) 2233 2234(* 2235 [oracles: DEFUN COMMON-LISP::ASH, DISK_THM] [axioms: ] [] 2236 |- ash i c = floor (mult (ifix i) (expt (nat 2) c)) (nat 1), 2237*) 2238 2239(* 2240 [oracles: DEFUN ACL2::THE-ERROR] [axioms: ] [] 2241 |- the_error x y = cdr (cons x y), 2242*) 2243 2244(* 2245 [oracles: DEFUN COMMON-LISP::CHAR<] [axioms: ] [] 2246 |- char_less x y = less (char_code x) (char_code y), 2247*) 2248 2249val char_less_def = 2250 acl2Define "COMMON-LISP::CHAR<" 2251 `char_less x y = less (char_code x) (char_code y)`; 2252 2253(* 2254 [oracles: DEFUN COMMON-LISP::CHAR>] [axioms: ] [] 2255 |- char_greater x y = less (char_code y) (char_code x), 2256*) 2257 2258(* 2259 [oracles: DEFUN COMMON-LISP::CHAR<=] [axioms: ] [] 2260 |- char_less_equal x y = not (less (char_code y) (char_code x)), 2261*) 2262 2263(* 2264 [oracles: DEFUN COMMON-LISP::CHAR>=] [axioms: ] [] 2265 |- char_greater_equal x y = not (less (char_code x) (char_code y)), 2266*) 2267 2268(* 2269 [oracles: DEFUN ACL2::STRING<-L] [axioms: ] [] 2270 |- string_less_l l1 l2 i = 2271 ite (endp l1) (ite (endp l2) nil i) 2272 (ite (endp l2) nil 2273 (ite (eql (car l1) (car l2)) 2274 (string_less_l (cdr l1) (cdr l2) (add i (cpx 1 1 0 1))) 2275 (ite (char_less (car l1) (car l2)) i nil))) 2276*) 2277 2278val (string_less_l_def,string_less_l_ind) = 2279 acl2_defn "ACL2::STRING<-L" 2280 (`string_less_l l1 l2 i = 2281 ite (endp l1) 2282 (ite (endp l2) nil i) 2283 (ite (endp l2) 2284 nil 2285 (ite (eql (car l1) (car l2)) 2286 (string_less_l (cdr l1) (cdr l2) (add i (cpx 1 1 0 1))) 2287 (ite (char_less (car l1) (car l2)) i nil)))`, 2288 WF_REL_TAC `measure (sexp_size o FST o SND)` 2289 THEN ACL2_SIMP_TAC []); 2290 2291 2292(* 2293 DEFUN COMMON-LISP::STRING< 2294 [oracles: DEFUN COMMON-LISP::STRING<] [axioms: ] [] 2295 |- string_less str1 str2 = 2296 string_less_l (coerce str1 (sym COMMON_LISP ACL2_STRING_ABBREV_521)) 2297 (coerce str2 (sym COMMON_LISP ACL2_STRING_ABBREV_521)) 2298 (cpx 0 1 0 1) 2299|- ACL2_STRING_ABBREV_521 = "LIST" 2300*) 2301 2302val string_less_def = 2303 acl2Define "COMMON-LISP::STRING<" 2304 `string_less str1 str2 = 2305 string_less_l (coerce str1 (sym COMMON_LISP "LIST")) 2306 (coerce str2 (sym COMMON_LISP "LIST")) 2307 (cpx 0 1 0 1)`; 2308 2309 2310(* 2311 [oracles: DEFUN COMMON-LISP::STRING>] [axioms: ] [] 2312 |- string_greater str1 str2 = string_less str2 str1, 2313*) 2314 2315(* 2316 [oracles: DEFUN COMMON-LISP::STRING<=, DISK_THM] [axioms: ] [] 2317 |- string_less_equal str1 str2 = 2318 ite (equal str1 str2) (length str1) (string_less str1 str2), 2319*) 2320 2321val string_less_equal_def = 2322 acl2Define "COMMON-LISP::STRING<=" 2323 `string_less_equal str1 str2 = 2324 ite (equal str1 str2) (length str1) (string_less str1 str2)`; 2325 2326(* 2327 [oracles: DEFUN COMMON-LISP::STRING>=, DISK_THM] [axioms: ] [] 2328 |- string_greater_equal str1 str2 = 2329 ite (equal str1 str2) (length str1) (string_greater str1 str2), 2330*) 2331 2332(* 2333 [oracles: DEFUN ACL2::SYMBOL-<, DISK_THM] [axioms: ] [] 2334 |- symbol_less x y = 2335 (let (x1,y1,y,x) = (symbol_name x,symbol_name y,y,x) in 2336 ite (string_less x1 y1) (string_less x1 y1) 2337 (ite (equal x1 y1) 2338 (string_less (symbol_package_name x) (symbol_package_name y)) 2339 nil)) 2340*) 2341 2342val symbol_less_def = 2343 acl2Define "ACL2::SYMBOL::-<" 2344 `symbol_less x y = 2345 (let (x1,y1,y,x) = (symbol_name x,symbol_name y,y,x) in 2346 ite (string_less x1 y1) (string_less x1 y1) 2347 (ite (equal x1 y1) 2348 (string_less (symbol_package_name x) (symbol_package_name y)) 2349 nil))`; 2350 2351 2352(* 2353 [oracles: DEFUN ACL2::SUBSTITUTE-AC, DISK_THM] [axioms: ] [] 2354 |- substitute_ac new old seq acc = 2355 itel 2356 [(endp seq,reverse acc); 2357 (eql old (car seq), 2358 substitute_ac new old (cdr seq) (cons new acc))] 2359 (substitute_ac new old (cdr seq) (cons (car seq) acc)), 2360*) 2361 2362(* 2363 [oracles: DEFUN COMMON-LISP::SUBSTITUTE, DISK_THM] [axioms: ] [] 2364 |- substitute new old seq = 2365 ite (stringp seq) 2366 (coerce (substitute_ac new old (coerce seq (csym "LIST")) nil) 2367 (csym "STRING")) (substitute_ac new old seq nil), 2368*) 2369 2370(* 2371 [oracles: DEFUN COMMON-LISP::SUBSETP, DISK_THM] [axioms: ] [] 2372 |- subsetp x y = 2373 ite (endp x) t (andl [member (car x) y; subsetp (cdr x) y]), 2374*) 2375 2376(* 2377 [oracles: DEFUN COMMON-LISP::SUBLIS, DISK_THM] [axioms: ] [] 2378 |- sublis alist tree = 2379 ite (atom tree) 2380 (let pair = assoc tree alist in ite pair (cdr pair) tree) 2381 (cons (sublis alist (car tree)) (sublis alist (cdr tree))), 2382*) 2383 2384(* 2385 [oracles: DEFUN COMMON-LISP::SUBST, DISK_THM] [axioms: ] [] 2386 |- subst new old tree = 2387 itel [(eql old tree,new); (atom tree,tree)] 2388 (cons (subst new old (car tree)) (subst new old (cdr tree))), 2389*) 2390 2391(* 2392 [oracles: DEFUN ACL2::WORLDP, DISK_THM] [axioms: ] [] 2393 |- worldp alist = 2394 ite (atom alist) (eq alist nil) 2395 (andl 2396 [consp (car alist); symbolp (caar alist); consp (cdar alist); 2397 symbolp (cadar alist); worldp (cdr alist)]), 2398*) 2399 2400(* 2401 [oracles: DEFUN ACL2::PUTPROP] [axioms: ] [] 2402 |- putprop symb key value world_alist = 2403 cons (cons symb (cons key value)) world_alist, 2404*) 2405 2406(* 2407 [oracles: DEFUN ACL2::GETPROP-DEFAULT] [axioms: ] [] 2408 |- getprop_default symb key default = default, 2409*) 2410 2411(* 2412 [oracles: DEFUN ACL2::FGETPROP, DISK_THM] [axioms: ] [] 2413 |- fgetprop symb key default world_alist = 2414 itel 2415 [(endp world_alist,default); 2416 (andl [eq symb (caar world_alist); eq key (cadar world_alist)], 2417 (let ans = cddar world_alist in 2418 ite (eq ans (ksym "ACL2-PROPERTY-UNBOUND")) default ans))] 2419 (fgetprop symb key default (cdr world_alist)), 2420*) 2421 2422(* 2423 [oracles: DEFUN ACL2::SGETPROP, DISK_THM] [axioms: ] [] 2424 |- sgetprop symb key default world_name world_alist = 2425 itel 2426 [(endp world_alist,default); 2427 (andl [eq symb (caar world_alist); eq key (cadar world_alist)], 2428 (let ans = cddar world_alist in 2429 ite (eq ans (ksym "ACL2-PROPERTY-UNBOUND")) default ans))] 2430 (sgetprop symb key default world_name (cdr world_alist)), 2431*) 2432 2433(* 2434 [oracles: DEFUN ACL2::ORDERED-SYMBOL-ALISTP] [axioms: ] [] 2435 |- ordered_symbol_alistp x = 2436 ite (atom x) (null x) 2437 (ite (atom (car x)) nil 2438 (ite (symbolp (car (car x))) 2439 (ite 2440 (ite (atom (cdr x)) (atom (cdr x)) 2441 (ite (consp (car (cdr x))) 2442 (ite (symbolp (car (car (cdr x)))) 2443 (symbol_less (car (car x)) (car (car (cdr x)))) 2444 nil) nil)) (ordered_symbol_alistp (cdr x)) nil) 2445 nil)) 2446*) 2447 2448(* 2449 [oracles: DEFUN ACL2::ADD-PAIR] [axioms: ] [] 2450 |- add_pair key value l = 2451 ite (endp l) (cons (cons key value) nil) 2452 (ite (eq key (car (car l))) (cons (cons key value) (cdr l)) 2453 (ite (symbol_less key (car (car l))) (cons (cons key value) l) 2454 (cons (car l) (add_pair key value (cdr l))))) 2455*) 2456 2457(* 2458 [oracles: DEFUN ACL2::REMOVE-FIRST-PAIR, DISK_THM] [axioms: ] [] 2459 |- remove_first_pair key l = 2460 itel [(endp l,nil); (eq key (caar l),cdr l)] 2461 (cons (car l) (remove_first_pair key (cdr l))), 2462*) 2463 2464(* 2465 [oracles: DEFUN ACL2::TRUE-LIST-LISTP, DISK_THM] [axioms: ] [] 2466 |- true_list_listp x = 2467 ite (atom x) (eq x nil) 2468 (andl [true_listp (car x); true_list_listp (cdr x)]), 2469*) 2470 2471(* 2472 [oracles: DEFUN ACL2::GETPROPS1, DISK_THM] [axioms: ] [] 2473 |- getprops1 alist = 2474 itel 2475 [(endp alist,nil); 2476 (ite (null (cdar alist)) (null (cdar alist)) 2477 (eq (cadar alist) (ksym "ACL2-PROPERTY-UNBOUND")), 2478 getprops1 (cdr alist))] 2479 (cons (cons (caar alist) (cadar alist)) (getprops1 (cdr alist))), 2480*) 2481 2482(* 2483 [oracles: DEFUN ACL2::GETPROPS, DISK_THM] [axioms: ] [] 2484 |- getprops symb world_name world_alist = 2485 itel 2486 [(endp world_alist,nil); 2487 (eq symb (caar world_alist), 2488 (let alist = getprops symb world_name (cdr world_alist) in 2489 ite (eq (cddar world_alist) (ksym "ACL2-PROPERTY-UNBOUND")) 2490 (ite (assoc_eq (cadar world_alist) alist) 2491 (remove_first_pair (cadar world_alist) alist) alist) 2492 (add_pair (cadar world_alist) (cddar world_alist) alist)))] 2493 (getprops symb world_name (cdr world_alist)), 2494*) 2495 2496(* 2497 [oracles: DEFUN ACL2::HAS-PROPSP1, DISK_THM] [axioms: ] [] 2498 |- has_propsp1 alist exceptions known_unbound = 2499 itel 2500 [(endp alist,nil); 2501 (itel 2502 [(null (cdar alist),null (cdar alist)); 2503 (eq (cadar alist) (ksym "ACL2-PROPERTY-UNBOUND"), 2504 eq (cadar alist) (ksym "ACL2-PROPERTY-UNBOUND")); 2505 (member_eq (caar alist) exceptions, 2506 member_eq (caar alist) exceptions)] 2507 (member_eq (caar alist) known_unbound), 2508 has_propsp1 (cdr alist) exceptions known_unbound)] t, 2509*) 2510 2511(* 2512 [oracles: DEFUN ACL2::HAS-PROPSP, DISK_THM] [axioms: ] [] 2513 |- has_propsp symb exceptions world_name world_alist known_unbound = 2514 itel 2515 [(endp world_alist,nil); 2516 (itel 2517 [(not (eq symb (caar world_alist)), 2518 not (eq symb (caar world_alist))); 2519 (member_eq (cadar world_alist) exceptions, 2520 member_eq (cadar world_alist) exceptions)] 2521 (member_eq (cadar world_alist) known_unbound), 2522 has_propsp symb exceptions world_name (cdr world_alist) 2523 known_unbound); 2524 (eq (cddar world_alist) (ksym "ACL2-PROPERTY-UNBOUND"), 2525 has_propsp symb exceptions world_name (cdr world_alist) 2526 (cons (cadar world_alist) known_unbound))] t, 2527*) 2528 2529(* 2530 [oracles: DEFUN ACL2::EXTEND-WORLD] [axioms: ] [] 2531 |- extend_world name wrld = wrld, 2532*) 2533 2534(* 2535 [oracles: DEFUN ACL2::RETRACT-WORLD] [axioms: ] [] 2536 |- retract_world name wrld = wrld, 2537*) 2538 2539(* 2540 [oracles: DEFUN ACL2::GLOBAL-VAL, DISK_THM] [axioms: ] [] 2541 |- global_val var wrld = 2542 fgetprop var (asym "GLOBAL-VALUE") 2543 (List 2544 [ksym "ERROR"; 2545 str 2546 "GLOBAL-VAL didn't find a value. Initialize this ~\n symbol in PRIMORDIAL-WORLD-GLOBALS."]) 2547 wrld, 2548*) 2549 2550(* 2551 [oracles: DEFUN ACL2::FUNCTION-SYMBOLP, DISK_THM] [axioms: ] [] 2552 |- function_symbolp acl2_sym wrld = 2553 not (eq (fgetprop acl2_sym (asym "FORMALS") t wrld) t), 2554*) 2555 2556(* 2557 [oracles: DEFUN ACL2::SET-DIFFERENCE-EQUAL, DISK_THM] [axioms: ] [] 2558 |- set_difference_equal l1 l2 = 2559 itel 2560 [(endp l1,nil); 2561 (member_equal (car l1) l2,set_difference_equal (cdr l1) l2)] 2562 (cons (car l1) (set_difference_equal (cdr l1) l2)), 2563*) 2564 2565(* 2566 [oracles: DEFUN ACL2::BOUNDED-INTEGER-ALISTP, DISK_THM] [axioms: ] [] 2567 |- bounded_integer_alistp l n = 2568 ite (atom l) (null l) 2569 (andl 2570 [consp (car l); 2571 (let key = caar l in 2572 andl 2573 [ite (eq key (ksym "HEADER")) (eq key (ksym "HEADER")) 2574 (andl 2575 [integerp key; integerp n; not (less key (nat 0)); 2576 less key n]); bounded_integer_alistp (cdr l) n])]), 2577*) 2578 2579(* 2580 [oracles: DEFUN ACL2::KEYWORD-VALUE-LISTP, DISK_THM] [axioms: ] [] 2581 |- keyword_value_listp l = 2582 ite (atom l) (null l) 2583 (andl 2584 [keywordp (car l); consp (cdr l); keyword_value_listp (cddr l)]), 2585*) 2586 2587(* 2588 [oracles: DEFUN ACL2::ASSOC-KEYWORD, DISK_THM] [axioms: ] [] 2589 |- assoc_keyword key l = 2590 itel [(endp l,nil); (eq key (car l),l)] (assoc_keyword key (cddr l)), 2591*) 2592 2593(* 2594 [oracles: DEFUN ACL2::ARRAY1P, DISK_THM] [axioms: ] [] 2595 |- array1p name l = 2596 andl 2597 [symbolp name; alistp l; 2598 (let header_keyword_list = cdr (assoc_eq (ksym "HEADER") l) in 2599 andl 2600 [keyword_value_listp header_keyword_list; 2601 (let dimensions = 2602 cadr 2603 (assoc_keyword (ksym "DIMENSIONS") 2604 header_keyword_list) 2605 in 2606 andl 2607 [true_listp dimensions; 2608 equal (length dimensions) (nat 1); 2609 integerp (car dimensions); 2610 integerp 2611 (cadr 2612 (assoc_keyword (ksym "MAXIMUM-LENGTH") 2613 header_keyword_list)); 2614 less (nat 0) (car dimensions); 2615 less (car dimensions) 2616 (cadr 2617 (assoc_keyword (ksym "MAXIMUM-LENGTH") 2618 header_keyword_list)); 2619 not 2620 (less (nat 2147483647) 2621 (cadr 2622 (assoc_keyword (ksym "MAXIMUM-LENGTH") 2623 header_keyword_list))); 2624 bounded_integer_alistp l (car dimensions)])])], 2625*) 2626 2627(* 2628 [oracles: DEFUN ACL2::BOUNDED-INTEGER-ALISTP2, DISK_THM] [axioms: ] [] 2629 |- bounded_integer_alistp2 l i j = 2630 ite (atom l) (null l) 2631 (andl 2632 [consp (car l); 2633 (let key = caar l in 2634 ite (eq key (ksym "HEADER")) (eq key (ksym "HEADER")) 2635 (andl 2636 [consp key; 2637 (let i1 = car key in 2638 andl 2639 [integerp i1; integerp (cdr key); integerp i; 2640 integerp j; not (less i1 (nat 0)); less i1 i; 2641 not (less (cdr key) (nat 0)); 2642 less (cdr key) j])])); 2643 bounded_integer_alistp2 (cdr l) i j]), 2644*) 2645 2646(* 2647 [oracles: DEFUN ACL2::ASSOC2, DISK_THM] [axioms: ] [] 2648 |- assoc2 i j l = 2649 itel 2650 [(atom l,nil); 2651 (andl 2652 [consp (car l); consp (caar l); eql i (caaar l); 2653 eql j (cdaar l)],car l)] (assoc2 i j (cdr l)), 2654*) 2655 2656(* 2657 [oracles: DEFUN ACL2::ARRAY2P, DISK_THM] [axioms: ] [] 2658 |- array2p name l = 2659 andl 2660 [symbolp name; alistp l; 2661 (let header_keyword_list = cdr (assoc_eq (ksym "HEADER") l) in 2662 andl 2663 [keyword_value_listp header_keyword_list; 2664 (let dimensions = 2665 cadr 2666 (assoc_keyword (ksym "DIMENSIONS") 2667 header_keyword_list) 2668 in 2669 andl 2670 [true_listp dimensions; 2671 equal (length dimensions) (nat 2); 2672 (let d1 = car dimensions in 2673 andl 2674 [integerp d1; integerp (cadr dimensions); 2675 integerp 2676 (cadr 2677 (assoc_keyword (ksym "MAXIMUM-LENGTH") 2678 header_keyword_list)); less (nat 0) d1; 2679 less (nat 0) (cadr dimensions); 2680 less (mult d1 (cadr dimensions)) 2681 (cadr 2682 (assoc_keyword (ksym "MAXIMUM-LENGTH") 2683 header_keyword_list)); 2684 not 2685 (less (nat 2147483647) 2686 (cadr 2687 (assoc_keyword (ksym "MAXIMUM-LENGTH") 2688 header_keyword_list))); 2689 bounded_integer_alistp2 l d1 2690 (cadr dimensions)])])])], 2691*) 2692 2693(* 2694 [oracles: DEFUN ACL2::HEADER, DISK_THM] [axioms: ] [] 2695 |- header name l = prog2_dollar name (assoc_eq (ksym "HEADER") l), 2696*) 2697 2698(* 2699 [oracles: DEFUN ACL2::DIMENSIONS, DISK_THM] [axioms: ] [] 2700 |- dimensions name l = 2701 cadr (assoc_keyword (ksym "DIMENSIONS") (cdr (header name l))), 2702*) 2703 2704(* 2705 [oracles: DEFUN ACL2::MAXIMUM-LENGTH, DISK_THM] [axioms: ] [] 2706 |- maximum_length name l = 2707 cadr (assoc_keyword (ksym "MAXIMUM-LENGTH") (cdr (header name l))), 2708*) 2709 2710(* 2711 [oracles: DEFUN ACL2::DEFAULT, DISK_THM] [axioms: ] [] 2712 |- default name l = 2713 cadr (assoc_keyword (ksym "DEFAULT") (cdr (header name l))), 2714*) 2715 2716(* 2717 [oracles: DEFUN ACL2::AREF1, DISK_THM] [axioms: ] [] 2718 |- aref1 name l n = 2719 (let x = andl [not (eq n (ksym "HEADER")); assoc n l] in 2720 ite (null x) (default name l) (cdr x)), 2721*) 2722 2723(* 2724 [oracles: DEFUN ACL2::COMPRESS11, DISK_THM] [axioms: ] [] 2725 |- compress11 name l i n default = 2726 ite (zp (add n (unary_minus i))) nil 2727 (let (pair,n,i,l,name,default) = (assoc i l,n,i,l,name,default) in 2728 ite (ite (null pair) (null pair) (equal (cdr pair) default)) 2729 (compress11 name l (add i (nat 1)) n default) 2730 (cons pair (compress11 name l (add i (nat 1)) n default))), 2731*) 2732 2733(* 2734 [oracles: DEFUN ACL2::COMPRESS1, DISK_THM] [axioms: ] [] 2735 |- compress1 name l = 2736 cons (header name l) 2737 (compress11 name l (nat 0) (car (dimensions name l)) 2738 (default name l)), 2739*) 2740 2741(* 2742 [oracles: DEFUN ACL2::ASET1, DISK_THM] [axioms: ] [] 2743 |- aset1 name l n val = 2744 (let l = cons (cons n val) l in 2745 ite (less (maximum_length name l) (length l)) (compress1 name l) 2746 l), 2747*) 2748 2749(* 2750 [oracles: DEFUN ACL2::AREF2, DISK_THM] [axioms: ] [] 2751 |- aref2 name l i j = 2752 (let x = assoc2 i j l in ite (null x) (default name l) (cdr x)), 2753*) 2754 2755(* 2756 [oracles: DEFUN ACL2::COMPRESS211, DISK_THM] [axioms: ] [] 2757 |- compress211 name l i x j default = 2758 ite (zp (add j (unary_minus x))) nil 2759 (let (pair,j,x,i,l,name,default) = 2760 (assoc2 i x l,j,x,i,l,name,default) 2761 in 2762 ite (ite (null pair) (null pair) (equal (cdr pair) default)) 2763 (compress211 name l i (add (nat 1) x) j default) 2764 (cons pair (compress211 name l i (add (nat 1) x) j default))), 2765*) 2766 2767(* 2768 [oracles: DEFUN ACL2::COMPRESS21, DISK_THM] [axioms: ] [] 2769 |- compress21 name l n i j default = 2770 ite (zp (add i (unary_minus n))) nil 2771 (binary_append (compress211 name l n (nat 0) j default) 2772 (compress21 name l (add n (nat 1)) i j default)), 2773*) 2774 2775(* 2776 [oracles: DEFUN ACL2::COMPRESS2, DISK_THM] [axioms: ] [] 2777 |- compress2 name l = 2778 cons (header name l) 2779 (compress21 name l (nat 0) (car (dimensions name l)) 2780 (cadr (dimensions name l)) (default name l)), 2781*) 2782 2783(* 2784 [oracles: DEFUN ACL2::ASET2, DISK_THM] [axioms: ] [] 2785 |- aset2 name l i j val = 2786 (let l = cons (cons (cons i j) val) l in 2787 ite (less (maximum_length name l) (length l)) (compress2 name l) 2788 l), 2789*) 2790 2791(* 2792 [oracles: DEFUN ACL2::FLUSH-COMPRESS] [axioms: ] [] 2793 |- flush_compress name = nil, 2794*) 2795 2796(* 2797 [oracles: DEFUN ACL2::CDRN, DISK_THM] [axioms: ] [] 2798 |- cdrn x i = 2799 ite (zp i) x (cdrn (List [csym "CDR"; x]) (add (int ~1) i)), 2800*) 2801 2802(* 2803 [oracles: DEFUN ACL2::MV-NTH, DISK_THM] [axioms: ] [] 2804 |- mv_nth n l = 2805 itel [(endp l,nil); (zp n,car l)] (mv_nth (add (int ~1) n) (cdr l)), 2806*) 2807 2808val (mv_nth_def,mv_nth_ind) = 2809 acl2_defn "ACL2::MV-NTH" 2810 (`mv_nth n l = 2811 itel [(endp l,nil); (zp n,car l)] (mv_nth (add (int ~1) n) (cdr l))`, 2812 WF_REL_TAC `measure (sexp_size o SND)` 2813 THEN ACL2_SIMP_TAC []); 2814 2815(* 2816 [oracles: DEFUN ACL2::MAKE-MV-NTHS, DISK_THM] [axioms: ] [] 2817 |- make_mv_nths args call i = 2818 ite (endp args) nil 2819 (cons (List [car args; List [asym "MV-NTH"; i; call]]) 2820 (make_mv_nths (cdr args) call (add i (nat 1)))), 2821*) 2822 2823(* 2824 [oracles: DEFUN ACL2::UPDATE-NTH, DISK_THM] [axioms: ] [] 2825 |- update_nth key val l = 2826 ite (zp key) (cons val (cdr l)) 2827 (cons (car l) (update_nth (add (int ~1) key) val (cdr l))), 2828*) 2829 2830(* 2831 [oracles: DEFUN ACL2::UPDATE-NTH-ARRAY] [axioms: ] [] 2832 |- update_nth_array j key val l = 2833 update_nth j (update_nth key val (nth j l)) l, 2834*) 2835 2836(* 2837 [oracles: DEFUN ACL2::32-BIT-INTEGERP, DISK_THM] [axioms: ] [] 2838 |- acl2_32_bit_integerp x = 2839 andl 2840 [integerp x; not (less (nat 2147483647) x); 2841 not (less x (add (unary_minus (nat 2147483647)) (int ~1)))], 2842*) 2843 2844(* 2845 [oracles: DEFUN ACL2::RATIONAL-LISTP, DISK_THM] [axioms: ] [] 2846 |- rational_listp l = 2847 ite (atom l) (eq l nil) 2848 (andl [rationalp (car l); rational_listp (cdr l)]), 2849*) 2850 2851(* 2852 [oracles: DEFUN ACL2::INTEGER-LISTP, DISK_THM] [axioms: ] [] 2853 |- integer_listp l = 2854 ite (atom l) (equal l nil) 2855 (andl [integerp (car l); integer_listp (cdr l)]), 2856*) 2857 2858(* 2859 [oracles: DEFUN ACL2::32-BIT-INTEGER-LISTP, DISK_THM] [axioms: ] [] 2860 |- acl2_32_bit_integer_listp l = 2861 ite (atom l) (equal l nil) 2862 (andl 2863 [acl2_32_bit_integerp (car l); 2864 acl2_32_bit_integer_listp (cdr l)]), 2865*) 2866 2867(* 2868 [oracles: DEFUN ACL2::OPEN-INPUT-CHANNELS, DISK_THM] [axioms: ] [] 2869 |- open_input_channels st = nth (nat 0) st, 2870*) 2871 2872(* 2873 [oracles: DEFUN ACL2::UPDATE-OPEN-INPUT-CHANNELS, DISK_THM] [axioms: ] 2874 [] |- update_open_input_channels x st = update_nth (nat 0) x st, 2875*) 2876 2877(* 2878 [oracles: DEFUN ACL2::OPEN-OUTPUT-CHANNELS, DISK_THM] [axioms: ] [] 2879 |- open_output_channels st = nth (nat 1) st, 2880*) 2881 2882(* 2883 [oracles: DEFUN ACL2::UPDATE-OPEN-OUTPUT-CHANNELS, DISK_THM] [axioms: ] 2884 [] |- update_open_output_channels x st = update_nth (nat 1) x st, 2885*) 2886 2887(* 2888 [oracles: DEFUN ACL2::GLOBAL-TABLE, DISK_THM] [axioms: ] [] 2889 |- global_table st = nth (nat 2) st, 2890*) 2891 2892(* 2893 [oracles: DEFUN ACL2::UPDATE-GLOBAL-TABLE, DISK_THM] [axioms: ] [] 2894 |- update_global_table x st = update_nth (nat 2) x st, 2895*) 2896 2897(* 2898 [oracles: DEFUN ACL2::T-STACK, DISK_THM] [axioms: ] [] 2899 |- t_stack st = nth (nat 3) st, 2900*) 2901 2902(* 2903 [oracles: DEFUN ACL2::UPDATE-T-STACK, DISK_THM] [axioms: ] [] 2904 |- update_t_stack x st = update_nth (nat 3) x st, 2905*) 2906 2907(* 2908 [oracles: DEFUN ACL2::32-BIT-INTEGER-STACK, DISK_THM] [axioms: ] [] 2909 |- acl2_32_bit_integer_stack st = nth (nat 4) st, 2910*) 2911 2912(* 2913 [oracles: DEFUN ACL2::UPDATE-32-BIT-INTEGER-STACK, DISK_THM] [axioms: ] 2914 [] |- update_32_bit_integer_stack x st = update_nth (nat 4) x st, 2915*) 2916 2917(* 2918 [oracles: DEFUN ACL2::BIG-CLOCK-ENTRY, DISK_THM] [axioms: ] [] 2919 |- big_clock_entry st = nth (nat 5) st, 2920*) 2921 2922(* 2923 [oracles: DEFUN ACL2::UPDATE-BIG-CLOCK-ENTRY, DISK_THM] [axioms: ] [] 2924 |- update_big_clock_entry x st = update_nth (nat 5) x st, 2925*) 2926 2927(* 2928 [oracles: DEFUN ACL2::IDATES, DISK_THM] [axioms: ] [] 2929 |- idates st = nth (nat 6) st, 2930*) 2931 2932(* 2933 [oracles: DEFUN ACL2::UPDATE-IDATES, DISK_THM] [axioms: ] [] 2934 |- update_idates x st = update_nth (nat 6) x st, 2935*) 2936 2937(* 2938 [oracles: DEFUN ACL2::RUN-TIMES, DISK_THM] [axioms: ] [] 2939 |- run_times st = nth (nat 7) st, 2940*) 2941 2942(* 2943 [oracles: DEFUN ACL2::UPDATE-RUN-TIMES, DISK_THM] [axioms: ] [] 2944 |- update_run_times x st = update_nth (nat 7) x st, 2945*) 2946 2947(* 2948 [oracles: DEFUN ACL2::FILE-CLOCK, DISK_THM] [axioms: ] [] 2949 |- file_clock st = nth (nat 8) st, 2950*) 2951 2952(* 2953 [oracles: DEFUN ACL2::UPDATE-FILE-CLOCK, DISK_THM] [axioms: ] [] 2954 |- update_file_clock x st = update_nth (nat 8) x st, 2955*) 2956 2957(* 2958 [oracles: DEFUN ACL2::READABLE-FILES, DISK_THM] [axioms: ] [] 2959 |- readable_files st = nth (nat 9) st, 2960*) 2961 2962(* 2963 [oracles: DEFUN ACL2::WRITTEN-FILES, DISK_THM] [axioms: ] [] 2964 |- written_files st = nth (nat 10) st, 2965*) 2966 2967(* 2968 [oracles: DEFUN ACL2::UPDATE-WRITTEN-FILES, DISK_THM] [axioms: ] [] 2969 |- update_written_files x st = update_nth (nat 10) x st, 2970*) 2971 2972(* 2973 [oracles: DEFUN ACL2::READ-FILES, DISK_THM] [axioms: ] [] 2974 |- read_files st = nth (nat 11) st, 2975*) 2976 2977(* 2978 [oracles: DEFUN ACL2::UPDATE-READ-FILES, DISK_THM] [axioms: ] [] 2979 |- update_read_files x st = update_nth (nat 11) x st, 2980*) 2981 2982(* 2983 [oracles: DEFUN ACL2::WRITEABLE-FILES, DISK_THM] [axioms: ] [] 2984 |- writeable_files st = nth (nat 12) st, 2985*) 2986 2987(* 2988 [oracles: DEFUN ACL2::LIST-ALL-PACKAGE-NAMES-LST, DISK_THM] [axioms: ] 2989 [] |- list_all_package_names_lst st = nth (nat 13) st, 2990*) 2991 2992(* 2993 [oracles: DEFUN ACL2::UPDATE-LIST-ALL-PACKAGE-NAMES-LST, DISK_THM] 2994 [axioms: ] [] 2995 |- update_list_all_package_names_lst x st = update_nth (nat 13) x st, 2996*) 2997 2998(* 2999 [oracles: DEFUN ACL2::USER-STOBJ-ALIST1, DISK_THM] [axioms: ] [] 3000 |- user_stobj_alist1 st = nth (nat 14) st, 3001*) 3002 3003(* 3004 [oracles: DEFUN ACL2::UPDATE-USER-STOBJ-ALIST1, DISK_THM] [axioms: ] [] 3005 |- update_user_stobj_alist1 x st = update_nth (nat 14) x st, 3006*) 3007 3008(* 3009 [oracles: DEFUN ACL2::ALL-BOUNDP, DISK_THM] [axioms: ] [] 3010 |- all_boundp alist1 alist2 = 3011 ite (endp alist1) t 3012 (andl [assoc (caar alist1) alist2; all_boundp (cdr alist1) alist2]), 3013*) 3014 3015(* 3016 [oracles: DEFUN ACL2::KNOWN-PACKAGE-ALISTP, DISK_THM] [axioms: ] [] 3017 |- known_package_alistp x = 3018 ite (atom x) (null x) 3019 (andl 3020 [true_listp (car x); stringp (caar x); symbol_listp (cadar x); 3021 known_package_alistp (cdr x)]), 3022*) 3023 3024(* 3025 [oracles: DEFUN ACL2::TIMER-ALISTP, DISK_THM] [axioms: ] [] 3026 |- timer_alistp x = 3027 ite (atom x) (equal x nil) 3028 (andl 3029 [consp (car x); symbolp (caar x); rational_listp (cdar x); 3030 timer_alistp (cdr x)]), 3031*) 3032 3033(* 3034 [oracles: DEFUN ACL2::TYPED-IO-LISTP, DISK_THM] [axioms: ] [] 3035 |- typed_io_listp l typ = 3036 ite (atom l) (equal l nil) 3037 (andl 3038 [itel 3039 [(eql typ (ksym "CHARACTER"),characterp (car l)); 3040 (eql typ (ksym "BYTE"), 3041 andl 3042 [integerp (car l); not (less (car l) (nat 0)); 3043 less (car l) (nat 256)])] 3044 (andl [eql typ (ksym "OBJECT"); t]); 3045 typed_io_listp (cdr l) typ]), 3046*) 3047 3048(* 3049 [oracles: DEFUN ACL2::OPEN-CHANNEL1, DISK_THM] [axioms: ] [] 3050 |- open_channel1 l = 3051 andl 3052 [true_listp l; consp l; 3053 (let header = car l in 3054 andl 3055 [true_listp header; equal (length header) (nat 4); 3056 eq (car header) (ksym "HEADER"); 3057 member_eq (cadr header) 3058 (List [ksym "CHARACTER"; ksym "BYTE"; ksym "OBJECT"]); 3059 stringp (caddr header); integerp (cadddr header); 3060 typed_io_listp (cdr l) (cadr header)])], 3061*) 3062 3063(* 3064 [oracles: DEFUN ACL2::OPEN-CHANNEL-LISTP, DISK_THM] [axioms: ] [] 3065 |- open_channel_listp l = 3066 ite (endp l) t 3067 (andl [open_channel1 (cdar l); open_channel_listp (cdr l)]), 3068*) 3069 3070(* 3071 [oracles: DEFUN ACL2::OPEN-CHANNELS-P, DISK_THM] [axioms: ] [] 3072 |- open_channels_p x = 3073 andl [ordered_symbol_alistp x; open_channel_listp x], 3074*) 3075 3076(* 3077 [oracles: DEFUN ACL2::FILE-CLOCK-P] [axioms: ] [] 3078 |- file_clock_p x = natp x, 3079*) 3080 3081(* 3082 [oracles: DEFUN ACL2::READABLE-FILE, DISK_THM] [axioms: ] [] 3083 |- readable_file x = 3084 andl 3085 [true_listp x; consp x; 3086 (let key = car x in 3087 andl 3088 [true_listp key; equal (length key) (nat 3); 3089 stringp (car key); 3090 member (cadr key) 3091 (List [ksym "CHARACTER"; ksym "BYTE"; ksym "OBJECT"]); 3092 integerp (caddr key); typed_io_listp (cdr x) (cadr key)])], 3093*) 3094 3095(* 3096 [oracles: DEFUN ACL2::READABLE-FILES-LISTP, DISK_THM] [axioms: ] [] 3097 |- readable_files_listp x = 3098 ite (atom x) (equal x nil) 3099 (andl [readable_file (car x); readable_files_listp (cdr x)]), 3100*) 3101 3102(* 3103 [oracles: DEFUN ACL2::READABLE-FILES-P] [axioms: ] [] 3104 |- readable_files_p x = readable_files_listp x, 3105*) 3106 3107(* 3108 [oracles: DEFUN ACL2::WRITTEN-FILE, DISK_THM] [axioms: ] [] 3109 |- written_file x = 3110 andl 3111 [true_listp x; consp x; 3112 (let key = car x in 3113 andl 3114 [true_listp key; equal (length key) (nat 4); 3115 stringp (car key); integerp (caddr key); 3116 integerp (cadddr key); 3117 member (cadr key) 3118 (List [ksym "CHARACTER"; ksym "BYTE"; ksym "OBJECT"]); 3119 typed_io_listp (cdr x) (cadr key)])], 3120*) 3121 3122(* 3123 [oracles: DEFUN ACL2::WRITTEN-FILE-LISTP, DISK_THM] [axioms: ] [] 3124 |- written_file_listp x = 3125 ite (atom x) (equal x nil) 3126 (andl [written_file (car x); written_file_listp (cdr x)]), 3127*) 3128 3129(* 3130 [oracles: DEFUN ACL2::WRITTEN-FILES-P] [axioms: ] [] 3131 |- written_files_p x = written_file_listp x, 3132*) 3133 3134(* 3135 [oracles: DEFUN ACL2::READ-FILE-LISTP1, DISK_THM] [axioms: ] [] 3136 |- read_file_listp1 x = 3137 andl 3138 [true_listp x; equal (length x) (nat 4); stringp (car x); 3139 member (cadr x) 3140 (List [ksym "CHARACTER"; ksym "BYTE"; ksym "OBJECT"]); 3141 integerp (caddr x); integerp (cadddr x)], 3142*) 3143 3144(* 3145 [oracles: DEFUN ACL2::READ-FILE-LISTP, DISK_THM] [axioms: ] [] 3146 |- read_file_listp x = 3147 ite (atom x) (equal x nil) 3148 (andl [read_file_listp1 (car x); read_file_listp (cdr x)]), 3149*) 3150 3151(* 3152 [oracles: DEFUN ACL2::READ-FILES-P] [axioms: ] [] 3153 |- read_files_p x = read_file_listp x, 3154*) 3155 3156(* 3157 [oracles: DEFUN ACL2::WRITABLE-FILE-LISTP1, DISK_THM] [axioms: ] [] 3158 |- writable_file_listp1 x = 3159 andl 3160 [true_listp x; equal (length x) (nat 3); stringp (car x); 3161 member (cadr x) 3162 (List [ksym "CHARACTER"; ksym "BYTE"; ksym "OBJECT"]); 3163 integerp (caddr x)], 3164*) 3165 3166(* 3167 [oracles: DEFUN ACL2::WRITABLE-FILE-LISTP, DISK_THM] [axioms: ] [] 3168 |- writable_file_listp x = 3169 ite (atom x) (equal x nil) 3170 (andl [writable_file_listp1 (car x); writable_file_listp (cdr x)]), 3171*) 3172 3173(* 3174 [oracles: DEFUN ACL2::WRITEABLE-FILES-P] [axioms: ] [] 3175 |- writeable_files_p x = writable_file_listp x, 3176*) 3177 3178(* 3179 [oracles: DEFUN ACL2::STATE-P1, DISK_THM] [axioms: ] [] 3180 |- state_p1 x = 3181 andl 3182 [true_listp x; equal (length x) (nat 15); 3183 open_channels_p (open_input_channels x); 3184 open_channels_p (open_output_channels x); 3185 ordered_symbol_alistp (global_table x); 3186 all_boundp 3187 (List 3188 [List [asym "ACCUMULATED-TTREE"]; 3189 List [asym "ACCUMULATED-WARNINGS"]; 3190 cons (asym "ACL2-VERSION") (str "ACL2 Version 2.9.3"); 3191 List [asym "AXIOMSP"]; List [asym "BDDNOTES"]; 3192 List [asym "CERTIFY-BOOK-FILE"]; 3193 List [asym "CONNECTED-BOOK-DIRECTORY"]; 3194 List [asym "CURRENT-ACL2-WORLD"]; 3195 cons (asym "CURRENT-PACKAGE") (str ACL2); 3196 cons (asym "DEFAXIOMS-OKP-CERT") t; 3197 List [asym "ERROR-TRACE-STACK"]; 3198 List [asym "EVISCERATE-HIDE-TERMS"]; 3199 cons (asym "FMT-HARD-RIGHT-MARGIN") (nat 77); 3200 cons (asym "FMT-SOFT-RIGHT-MARGIN") (nat 65); 3201 List [asym "GSTACKP"]; cons (asym "GUARD-CHECKING-ON") t; 3202 List [asym "IN-CERTIFY-BOOK-FLG"]; 3203 List [asym "IN-LOCAL-FLG"]; List [asym "IN-PROVE-FLG"]; 3204 List [asym "INCLUDE-BOOK-ALIST-STATE"]; 3205 List [asym "INFIXP"]; 3206 List [asym "INHIBIT-OUTPUT-LST"; asym "SUMMARY"]; 3207 cons (asym "LD-LEVEL") (nat 0); 3208 List [asym "LD-REDEFINITION-ACTION"]; 3209 List [asym "LD-SKIP-PROOFSP"]; 3210 List [asym "MATCH-FREE-ERROR"]; 3211 cons (asym "MORE-DOC-MAX-LINES") (nat 45); 3212 cons (asym "MORE-DOC-MIN-LINES") (nat 35); 3213 List [asym "MORE-DOC-STATE"]; 3214 List [asym "PACKAGES-CREATED-BY-DEFPKG"]; 3215 cons (asym "PRINT-BASE") (nat 10); 3216 cons (asym "PRINT-CASE") (ksym "UPCASE"); 3217 List [asym "PRINT-CLAUSE-IDS"]; 3218 cons (asym "PRINT-DOC-START-COLUMN") (nat 15); 3219 cons (asym "PROMPT-FUNCTION") (asym "DEFAULT-PRINT-PROMPT"); 3220 List [asym "PROOF-TREE-CTX"]; 3221 cons (asym "PROOFS-CO") 3222 (osym "STANDARD-CHARACTER-OUTPUT-0"); 3223 List 3224 [asym "RAW-ARITY-ALIST"; 3225 cons (asym "ER-PROGN") (csym "LAST"); 3226 cons (csym "EVAL-WHEN") (ksym "LAST"); 3227 cons (csym "LET") (ksym "LAST"); 3228 cons (csym "LET*") (ksym "LAST"); 3229 cons (asym "MV-LET") (ksym "LAST"); 3230 cons (asym "PROG2$") (ksym "LAST"); 3231 cons (csym "PROGN") (ksym "LAST"); 3232 cons (csym "THE") (ksym "LAST"); 3233 cons (csym "TIME") (ksym "LAST"); 3234 cons (csym "TRACE") (nat 1); 3235 cons (csym "UNTRACE") (nat 1)]; List [asym "SAFE-MODE"]; 3236 List [asym "SAVED-OUTPUT-REVERSED"]; 3237 List [asym "SAVED-OUTPUT-TOKEN-LST"]; 3238 List [asym "SAVED-OUTPUT-P"]; 3239 cons (asym "SKIP-PROOFS-OKP-CERT") t; 3240 List [asym "SKIPPED-PROOFSP"]; 3241 cons (asym "STANDARD-CO") 3242 (osym "STANDARD-CHARACTER-OUTPUT-0"); 3243 cons (asym "STANDARD-OI") (osym "STANDARD-OBJECT-INPUT-0"); 3244 List [asym "TAINTED-OKP"]; List [asym "TIMER-ALIST"]; 3245 cons (asym "TRACE-CO") (osym "STANDARD-CHARACTER-OUTPUT-0"); 3246 cons (asym "TRANSLATE-ERROR-DEPTH") (int ~1); 3247 cons (asym "TRIPLE-PRINT-PREFIX") (str " "); 3248 List [asym "UNDONE-WORLDS-KILL-RING"; nil; nil; nil]; 3249 List [asym "WINDOW-INTERFACEP"]; 3250 List [asym "WORMHOLE-NAME"]; List [asym "WORMHOLE-OUTPUT"]]) 3251 (global_table x); 3252 worldp (cdr (assoc (asym "CURRENT-ACL2-WORLD") (global_table x))); 3253 symbol_alistp 3254 (fgetprop (asym "ACL2-DEFAULTS-TABLE") (asym "TABLE-ALIST") nil 3255 (cdr (assoc (asym "CURRENT-ACL2-WORLD") (global_table x)))); 3256 timer_alistp (cdr (assoc (asym "TIMER-ALIST") (global_table x))); 3257 known_package_alistp 3258 (fgetprop (asym "KNOWN-PACKAGE-ALIST") (asym "GLOBAL-VALUE") nil 3259 (cdr (assoc (asym "CURRENT-ACL2-WORLD") (global_table x)))); 3260 true_listp (t_stack x); 3261 acl2_32_bit_integer_listp (acl2_32_bit_integer_stack x); 3262 integerp (big_clock_entry x); integer_listp (idates x); 3263 rational_listp (run_times x); file_clock_p (file_clock x); 3264 readable_files_p (readable_files x); 3265 written_files_p (written_files x); read_files_p (read_files x); 3266 writeable_files_p (writeable_files x); 3267 true_list_listp (list_all_package_names_lst x); 3268 symbol_alistp (user_stobj_alist1 x)], 3269*) 3270 3271(* 3272 [oracles: DEFUN ACL2::STATE-P] [axioms: ] [] 3273 |- state_p state_state = state_p1 state_state, 3274*) 3275 3276(* 3277 [oracles: DEFUN ACL2::BUILD-STATE1, DISK_THM] [axioms: ] [] 3278 |- build_state1 open_input_channels open_output_channels global_table 3279 t_stack acl2_32_bit_integer_stack big_clock idates run_times 3280 file_clock readable_files written_files read_files writeable_files 3281 list_all_package_names_lst user_stobj_alist = 3282 (let s = 3283 List 3284 [open_input_channels; open_output_channels; global_table; 3285 t_stack; acl2_32_bit_integer_stack; big_clock; idates; 3286 run_times; file_clock; readable_files; written_files; 3287 read_files; writeable_files; list_all_package_names_lst; 3288 user_stobj_alist] 3289 in 3290 ite (state_p1 s) s 3291 (List 3292 [nil; nil; 3293 List 3294 [List [asym "ACCUMULATED-TTREE"]; 3295 List [asym "ACCUMULATED-WARNINGS"]; 3296 cons (asym "ACL2-VERSION") (str "ACL2 Version 2.9.3"); 3297 List [asym "AXIOMSP"]; List [asym "BDDNOTES"]; 3298 List [asym "CERTIFY-BOOK-FILE"]; 3299 List [asym "CONNECTED-BOOK-DIRECTORY"]; 3300 List [asym "CURRENT-ACL2-WORLD"]; 3301 cons (asym "CURRENT-PACKAGE") (str ACL2); 3302 cons (asym "DEFAXIOMS-OKP-CERT") t; 3303 List [asym "ERROR-TRACE-STACK"]; 3304 List [asym "EVISCERATE-HIDE-TERMS"]; 3305 cons (asym "FMT-HARD-RIGHT-MARGIN") (nat 77); 3306 cons (asym "FMT-SOFT-RIGHT-MARGIN") (nat 65); 3307 List [asym "GSTACKP"]; cons (asym "GUARD-CHECKING-ON") t; 3308 List [asym "IN-CERTIFY-BOOK-FLG"]; 3309 List [asym "IN-LOCAL-FLG"]; List [asym "IN-PROVE-FLG"]; 3310 List [asym "INCLUDE-BOOK-ALIST-STATE"]; 3311 List [asym "INFIXP"]; 3312 List [asym "INHIBIT-OUTPUT-LST"; asym "SUMMARY"]; 3313 cons (asym "LD-LEVEL") (nat 0); 3314 List [asym "LD-REDEFINITION-ACTION"]; 3315 List [asym "LD-SKIP-PROOFSP"]; 3316 List [asym "MATCH-FREE-ERROR"]; 3317 cons (asym "MORE-DOC-MAX-LINES") (nat 45); 3318 cons (asym "MORE-DOC-MIN-LINES") (nat 35); 3319 List [asym "MORE-DOC-STATE"]; 3320 List [asym "PACKAGES-CREATED-BY-DEFPKG"]; 3321 cons (asym "PRINT-BASE") (nat 10); 3322 cons (asym "PRINT-CASE") (ksym "UPCASE"); 3323 List [asym "PRINT-CLAUSE-IDS"]; 3324 cons (asym "PRINT-DOC-START-COLUMN") (nat 15); 3325 cons (asym "PROMPT-FUNCTION") 3326 (asym "DEFAULT-PRINT-PROMPT"); 3327 List [asym "PROOF-TREE-CTX"]; 3328 cons (asym "PROOFS-CO") 3329 (osym "STANDARD-CHARACTER-OUTPUT-0"); 3330 List 3331 [asym "RAW-ARITY-ALIST"; 3332 cons (asym "ER-PROGN") (csym "LAST"); 3333 cons (csym "EVAL-WHEN") (ksym "LAST"); 3334 cons (csym "LET") (ksym "LAST"); 3335 cons (csym "LET*") (ksym "LAST"); 3336 cons (asym "MV-LET") (ksym "LAST"); 3337 cons (asym "PROG2$") (ksym "LAST"); 3338 cons (csym "PROGN") (ksym "LAST"); 3339 cons (csym "THE") (ksym "LAST"); 3340 cons (csym "TIME") (ksym "LAST"); 3341 cons (csym "TRACE") (nat 1); 3342 cons (csym "UNTRACE") (nat 1)]; 3343 List [asym "SAFE-MODE"]; 3344 List [asym "SAVED-OUTPUT-REVERSED"]; 3345 List [asym "SAVED-OUTPUT-TOKEN-LST"]; 3346 List [asym "SAVED-OUTPUT-P"]; 3347 cons (asym "SKIP-PROOFS-OKP-CERT") t; 3348 List [asym "SKIPPED-PROOFSP"]; 3349 cons (asym "STANDARD-CO") 3350 (osym "STANDARD-CHARACTER-OUTPUT-0"); 3351 cons (asym "STANDARD-OI") 3352 (osym "STANDARD-OBJECT-INPUT-0"); 3353 List [asym "TAINTED-OKP"]; List [asym "TIMER-ALIST"]; 3354 cons (asym "TRACE-CO") 3355 (osym "STANDARD-CHARACTER-OUTPUT-0"); 3356 cons (asym "TRANSLATE-ERROR-DEPTH") (int ~1); 3357 cons (asym "TRIPLE-PRINT-PREFIX") (str " "); 3358 List [asym "UNDONE-WORLDS-KILL-RING"; nil; nil; nil]; 3359 List [asym "WINDOW-INTERFACEP"]; 3360 List [asym "WORMHOLE-NAME"]; 3361 List [asym "WORMHOLE-OUTPUT"]]; nil; nil; nat 4000000; 3362 nil; nil; nat 1; nil; nil; nil; nil; nil; nil])), 3363*) 3364 3365(* 3366 [oracles: DEFUN ACL2::COERCE-STATE-TO-OBJECT] [axioms: ] [] 3367 |- coerce_state_to_object x = x, 3368*) 3369 3370(* 3371 [oracles: DEFUN ACL2::COERCE-OBJECT-TO-STATE] [axioms: ] [] 3372 |- coerce_object_to_state x = x, 3373*) 3374 3375(* 3376 [oracles: DEFUN ACL2::GLOBAL-TABLE-CARS1] [axioms: ] [] 3377 |- global_table_cars1 state_state = 3378 strip_cars (global_table state_state), 3379*) 3380 3381(* 3382 [oracles: DEFUN ACL2::GLOBAL-TABLE-CARS] [axioms: ] [] 3383 |- global_table_cars state_state = global_table_cars1 state_state, 3384*) 3385 3386(* 3387 [oracles: DEFUN ACL2::BOUNDP-GLOBAL1, DISK_THM] [axioms: ] [] 3388 |- boundp_global1 x state_state = 3389 andl [assoc x (global_table state_state); t], 3390*) 3391 3392(* 3393 [oracles: DEFUN ACL2::BOUNDP-GLOBAL] [axioms: ] [] 3394 |- boundp_global x state_state = boundp_global1 x state_state, 3395*) 3396 3397(* 3398 [oracles: DEFUN ACL2::DELETE-PAIR, DISK_THM] [axioms: ] [] 3399 |- delete_pair x l = 3400 itel [(endp l,nil); (eq x (caar l),cdr l)] 3401 (cons (car l) (delete_pair x (cdr l))), 3402*) 3403 3404(* 3405 [oracles: DEFUN ACL2::MAKUNBOUND-GLOBAL] [axioms: ] [] 3406 |- makunbound_global x state_state = 3407 update_global_table (delete_pair x (global_table state_state)) 3408 state_state, 3409*) 3410 3411(* 3412 [oracles: DEFUN ACL2::GET-GLOBAL] [axioms: ] [] 3413 |- get_global x state_state = cdr (assoc x (global_table state_state)), 3414*) 3415 3416(* 3417 [oracles: DEFUN ACL2::PUT-GLOBAL] [axioms: ] [] 3418 |- put_global key value state_state = 3419 update_global_table (add_pair key value (global_table state_state)) 3420 state_state, 3421*) 3422 3423(* 3424 [oracles: DEFUN ACL2::SET-SKIPPED-PROOFSP, DISK_THM] [axioms: ] [] 3425 |- set_skipped_proofsp state = 3426 put_global (asym "SKIPPED-PROOFSP") t state, 3427*) 3428 3429(* 3430 [oracles: DEFUN ACL2::SYMBOL-DOUBLET-LISTP, DISK_THM] [axioms: ] [] 3431 |- symbol_doublet_listp lst = 3432 ite (atom lst) (eq lst nil) 3433 (andl 3434 [consp (car lst); symbolp (caar lst); consp (cdar lst); 3435 null (cddar lst); symbol_doublet_listp (cdr lst)]), 3436*) 3437 3438(* 3439 [oracles: DEFUN ACL2::STATE-GLOBAL-LET*-GET-GLOBALS, DISK_THM] 3440 [axioms: ] [] 3441 |- state_global_let_star_get_globals bindings = 3442 ite (endp bindings) nil 3443 (cons 3444 (List 3445 [csym "IF"; 3446 List 3447 [asym "BOUNDP-GLOBAL"; List [csym "QUOTE"; caar bindings]; 3448 asym "STATE"]; 3449 List 3450 [csym "LIST"; 3451 List 3452 [asym "F-GET-GLOBAL"; 3453 List [csym "QUOTE"; caar bindings]; asym "STATE"]]; 3454 nil]) (state_global_let_star_get_globals (cdr bindings))), 3455*) 3456 3457(* 3458 [oracles: DEFUN ACL2::STATE-GLOBAL-LET*-PUT-GLOBALS, DISK_THM] 3459 [axioms: ] [] 3460 |- state_global_let_star_put_globals bindings = 3461 ite (endp bindings) nil 3462 (cons 3463 (List 3464 [asym "F-PUT-GLOBAL"; List [csym "QUOTE"; caar bindings]; 3465 List 3466 [asym "CHECK-VARS-NOT-FREE"; 3467 List [asym "STATE-GLOBAL-LET*-CLEANUP-LST"]; 3468 cadar bindings]; asym "STATE"]) 3469 (state_global_let_star_put_globals (cdr bindings))), 3470*) 3471 3472(* 3473 [oracles: DEFUN ACL2::STATE-GLOBAL-LET*-CLEANUP, DISK_THM] [axioms: ] [] 3474 |- state_global_let_star_cleanup bindings cdr_expr = 3475 ite (endp bindings) nil 3476 (cons 3477 (List 3478 [csym "IF"; List [csym "CAR"; cdr_expr]; 3479 List 3480 [asym "F-PUT-GLOBAL"; List [csym "QUOTE"; caar bindings]; 3481 List [csym "CAR"; List [csym "CAR"; cdr_expr]]; 3482 asym "STATE"]; 3483 List 3484 [asym "MAKUNBOUND-GLOBAL"; 3485 List [csym "QUOTE"; caar bindings]; asym "STATE"]]) 3486 (state_global_let_star_cleanup (cdr bindings) 3487 (List [csym "CDR"; cdr_expr]))), 3488*) 3489 3490(* 3491 [oracles: DEFUN ACL2::INTEGER-RANGE-P, DISK_THM] [axioms: ] [] 3492 |- integer_range_p lower upper x = 3493 andl [integerp x; not (less x lower); less x upper], 3494*) 3495 3496(* 3497 [oracles: DEFUN ACL2::SIGNED-BYTE-P, DISK_THM] [axioms: ] [] 3498 |- signed_byte_p bits x = 3499 andl 3500 [integerp bits; less (nat 0) bits; 3501 integer_range_p (unary_minus (expt (nat 2) (add (int ~1) bits))) 3502 (expt (nat 2) (add (int ~1) bits)) x], 3503*) 3504 3505(* 3506 [oracles: DEFUN ACL2::UNSIGNED-BYTE-P, DISK_THM] [axioms: ] [] 3507 |- unsigned_byte_p bits x = 3508 andl 3509 [integerp bits; not (less bits (nat 0)); 3510 integer_range_p (nat 0) (expt (nat 2) bits) x], 3511*) 3512 3513(* 3514 [oracles: DEFUN ACL2::ZPF, DISK_THM] [axioms: ] [] 3515 |- zpf x = ite (integerp x) (not (less (nat 0) x)) t, 3516*) 3517 3518(* 3519 [oracles: DEFUN COMMON-LISP::INTEGER-LENGTH, DISK_THM] [axioms: ] [] 3520 |- integer_length i = 3521 itel [(zip i,nat 0); (common_lisp_equal i (int ~1),nat 0)] 3522 (add (nat 1) (integer_length (floor i (nat 2)))), 3523*) 3524 3525(* 3526 [oracles: DEFUN ACL2::BINARY-LOGAND, DISK_THM] [axioms: ] [] 3527 |- binary_logand i j = 3528 itel 3529 [(zip i,nat 0); (zip j,nat 0); (eql i (int ~1),j); 3530 (eql j (int ~1),i)] 3531 (let x = 3532 mult (nat 2) 3533 (binary_logand (floor i (nat 2)) (floor j (nat 2))) 3534 in 3535 add x (itel [(evenp i,nat 0); (evenp j,nat 0)] (nat 1))), 3536*) 3537 3538(* 3539 [oracles: DEFUN COMMON-LISP::LOGNAND] [axioms: ] [] 3540 |- lognand i j = lognot (binary_logand i j), 3541*) 3542 3543(* 3544 [oracles: DEFUN ACL2::BINARY-LOGIOR] [axioms: ] [] 3545 |- binary_logior i j = lognot (binary_logand (lognot i) (lognot j)), 3546*) 3547 3548(* 3549 [oracles: DEFUN COMMON-LISP::LOGORC1] [axioms: ] [] 3550 |- logorc1 i j = binary_logior (lognot i) j, 3551*) 3552 3553(* 3554 [oracles: DEFUN COMMON-LISP::LOGORC2] [axioms: ] [] 3555 |- logorc2 i j = binary_logior i (lognot j), 3556*) 3557 3558(* 3559 [oracles: DEFUN COMMON-LISP::LOGANDC1] [axioms: ] [] 3560 |- logandc1 i j = binary_logand (lognot i) j, 3561*) 3562 3563(* 3564 [oracles: DEFUN COMMON-LISP::LOGANDC2] [axioms: ] [] 3565 |- logandc2 i j = binary_logand i (lognot j), 3566*) 3567 3568(* 3569 [oracles: DEFUN ACL2::BINARY-LOGEQV] [axioms: ] [] 3570 |- binary_logeqv i j = binary_logand (logorc1 i j) (logorc1 j i), 3571*) 3572 3573(* 3574 [oracles: DEFUN ACL2::BINARY-LOGXOR] [axioms: ] [] 3575 |- binary_logxor i j = lognot (binary_logeqv i j), 3576*) 3577 3578(* 3579 [oracles: DEFUN COMMON-LISP::LOGNOR] [axioms: ] [] 3580 |- lognor i j = lognot (binary_logior i j), 3581*) 3582 3583(* 3584 [oracles: DEFUN COMMON-LISP::LOGTEST] [axioms: ] [] 3585 |- logtest x y = not (zerop (binary_logand x y)), 3586*) 3587 3588(* 3589 [oracles: DEFUN ACL2::DIGIT-TO-CHAR, DISK_THM] [axioms: ] [] 3590 |- digit_to_char n = 3591 itel 3592 [(eql n (nat 1),chr #"1"); (eql n (nat 2),chr #"2"); 3593 (eql n (nat 3),chr #"3"); (eql n (nat 4),chr #"4"); 3594 (eql n (nat 5),chr #"5"); (eql n (nat 6),chr #"6"); 3595 (eql n (nat 7),chr #"7"); (eql n (nat 8),chr #"8"); 3596 (eql n (nat 9),chr #"9"); (eql n (nat 10),chr #"A"); 3597 (eql n (nat 11),chr #"B"); (eql n (nat 12),chr #"C"); 3598 (eql n (nat 13),chr #"D"); (eql n (nat 14),chr #"E"); 3599 (eql n (nat 15),chr #"F")] (chr #"0"), 3600*) 3601 3602(* 3603 [oracles: DEFUN ACL2::PRINT-BASE-P, DISK_THM] [axioms: ] [] 3604 |- print_base_p print_base = 3605 member print_base (List [nat 2; nat 8; nat 10; nat 16]), 3606*) 3607 3608(* 3609 [oracles: DEFUN ACL2::EXPLODE-NONNEGATIVE-INTEGER, DISK_THM] [axioms: ] 3610 [] 3611 |- explode_nonnegative_integer n print_base ans = 3612 ite (ite (zp n) (zp n) (not (print_base_p print_base))) 3613 (ite (null ans) (List [chr #"0"]) ans) 3614 (explode_nonnegative_integer (floor n print_base) print_base 3615 (cons (digit_to_char (mod n print_base)) ans)), 3616*) 3617 3618(* 3619 [oracles: DEFUN ACL2::EXPLODE-ATOM, DISK_THM] [axioms: ] [] 3620 |- explode_atom x print_base = 3621 itel 3622 [(rationalp x, 3623 ite (integerp x) 3624 (let digits = 3625 ite (less x (nat 0)) 3626 (cons (chr #"-") 3627 (explode_nonnegative_integer (unary_minus x) 3628 print_base nil)) 3629 (explode_nonnegative_integer x print_base nil) 3630 in 3631 ite 3632 (eql (nat 10) 3633 (let var = print_base in 3634 ite (integerp var) var 3635 (the_error (csym "INTEGER") var))) digits 3636 (cons (chr #"#") 3637 (cons 3638 (itel 3639 [(eql print_base (nat 2),chr #"b"); 3640 (eql print_base (nat 8),chr #"o"); 3641 (eql print_base (nat 16),chr #"x")] 3642 (illegal (asym "EXPLODE-ATOM") 3643 (str "Unexpected base, ~x0") print_base)) 3644 digits))) 3645 (binary_append (explode_atom (numerator x) print_base) 3646 (cons (chr #"/") 3647 (explode_nonnegative_integer (denominator x) print_base 3648 nil)))); 3649 (complex_rationalp x, 3650 cons (chr #"#") 3651 (cons (chr #"C") 3652 (cons (chr #"(") 3653 (binary_append (explode_atom (realpart x) print_base) 3654 (cons (chr #" ") 3655 (binary_append 3656 (explode_atom (imagpart x) print_base) 3657 (List [chr #")"]))))))); 3658 (characterp x,List [x]); (stringp x,coerce x (csym "LIST"))] 3659 (coerce (symbol_name x) (csym "LIST")), 3660*) 3661 3662(* 3663 [oracles: DEFUN ACL2::OPEN-INPUT-CHANNEL-P1, DISK_THM] [axioms: ] [] 3664 |- open_input_channel_p1 channel typ state_state = 3665 (let pair = assoc_eq channel (open_input_channels state_state) in 3666 andl [pair; eq (cadadr pair) typ]), 3667*) 3668 3669(* 3670 [oracles: DEFUN ACL2::OPEN-OUTPUT-CHANNEL-P1, DISK_THM] [axioms: ] [] 3671 |- open_output_channel_p1 channel typ state_state = 3672 (let pair = assoc_eq channel (open_output_channels state_state) in 3673 andl [pair; eq (cadadr pair) typ]), 3674*) 3675 3676(* 3677 [oracles: DEFUN ACL2::OPEN-INPUT-CHANNEL-P] [axioms: ] [] 3678 |- open_input_channel_p channel typ state_state = 3679 open_input_channel_p1 channel typ state_state, 3680*) 3681 3682(* 3683 [oracles: DEFUN ACL2::OPEN-OUTPUT-CHANNEL-P] [axioms: ] [] 3684 |- open_output_channel_p channel typ state_state = 3685 open_output_channel_p1 channel typ state_state, 3686*) 3687 3688(* 3689 [oracles: DEFUN ACL2::OPEN-OUTPUT-CHANNEL-ANY-P1, DISK_THM] [axioms: ] 3690 [] 3691 |- open_output_channel_any_p1 channel state_state = 3692 itel 3693 [(open_output_channel_p1 channel (ksym "CHARACTER") state_state, 3694 open_output_channel_p1 channel (ksym "CHARACTER") state_state); 3695 (open_output_channel_p1 channel (ksym "BYTE") state_state, 3696 open_output_channel_p1 channel (ksym "BYTE") state_state)] 3697 (open_output_channel_p1 channel (ksym "OBJECT") state_state), 3698*) 3699 3700(* 3701 [oracles: DEFUN ACL2::OPEN-OUTPUT-CHANNEL-ANY-P] [axioms: ] [] 3702 |- open_output_channel_any_p channel state_state = 3703 open_output_channel_any_p1 channel state_state, 3704*) 3705 3706(* 3707 [oracles: DEFUN ACL2::OPEN-INPUT-CHANNEL-ANY-P1, DISK_THM] [axioms: ] [] 3708 |- open_input_channel_any_p1 channel state_state = 3709 itel 3710 [(open_input_channel_p1 channel (ksym "CHARACTER") state_state, 3711 open_input_channel_p1 channel (ksym "CHARACTER") state_state); 3712 (open_input_channel_p1 channel (ksym "BYTE") state_state, 3713 open_input_channel_p1 channel (ksym "BYTE") state_state)] 3714 (open_input_channel_p1 channel (ksym "OBJECT") state_state), 3715*) 3716 3717(* 3718 [oracles: DEFUN ACL2::OPEN-INPUT-CHANNEL-ANY-P] [axioms: ] [] 3719 |- open_input_channel_any_p channel state_state = 3720 open_input_channel_any_p1 channel state_state, 3721*) 3722 3723(* 3724 [oracles: DEFUN ACL2::CHECK-HEX-UPPERCASE] [axioms: ] [] 3725 |- check_hex_uppercase print_base = nil, 3726*) 3727 3728(* 3729 [oracles: DEFUN ACL2::WRITE-BYTE$, DISK_THM] [axioms: ] [] 3730 |- write_byte_dollar x channel state_state = 3731 (let entry = 3732 cdr (assoc_eq channel (open_output_channels state_state)) 3733 in 3734 update_open_output_channels 3735 (add_pair channel (cons (car entry) (cons x (cdr entry))) 3736 (open_output_channels state_state)) state_state), 3737*) 3738 3739(* 3740 [oracles: DEFUN ACL2::PRINT-OBJECT$, DISK_THM] [axioms: ] [] 3741 |- print_object_dollar x channel state_state = 3742 (let entry = 3743 cdr (assoc_eq channel (open_output_channels state_state)) 3744 in 3745 update_open_output_channels 3746 (add_pair channel (cons (car entry) (cons x (cdr entry))) 3747 (open_output_channels state_state)) state_state), 3748*) 3749 3750(* 3751 [oracles: DEFUN ACL2::CLOSE-INPUT-CHANNEL, DISK_THM] [axioms: ] [] 3752 |- close_input_channel channel state_state = 3753 (let state_state = 3754 update_file_clock (add (nat 1) (file_clock state_state)) 3755 state_state 3756 in 3757 let header_entries = 3758 cdadr (assoc_eq channel (open_input_channels state_state)) 3759 in 3760 let state_state = 3761 update_read_files 3762 (cons 3763 (List 3764 [cadr header_entries; car header_entries; 3765 caddr header_entries; file_clock state_state]) 3766 (read_files state_state)) state_state 3767 in 3768 let state_state = 3769 update_open_input_channels 3770 (delete_pair channel (open_input_channels state_state)) 3771 state_state 3772 in 3773 state_state), 3774*) 3775 3776(* 3777 [oracles: DEFUN ACL2::CLOSE-OUTPUT-CHANNEL, DISK_THM] [axioms: ] [] 3778 |- close_output_channel channel state_state = 3779 (let state_state = 3780 update_file_clock (add (nat 1) (file_clock state_state)) 3781 state_state 3782 in 3783 let pair = assoc_eq channel (open_output_channels state_state) in 3784 let header_entries = cdadr pair in 3785 let state_state = 3786 update_written_files 3787 (cons 3788 (cons 3789 (List 3790 [cadr header_entries; car header_entries; 3791 caddr header_entries; file_clock state_state]) 3792 (cddr pair)) (written_files state_state)) state_state 3793 in 3794 let state_state = 3795 update_open_output_channels 3796 (delete_pair channel (open_output_channels state_state)) 3797 state_state 3798 in 3799 state_state), 3800*) 3801 3802(* 3803 [oracles: DEFUN ACL2::READ-CHAR$, DISK_THM] [axioms: ] [] 3804 |- read_char_dollar channel state_state = 3805 (let entry = cdr (assoc_eq channel (open_input_channels state_state)) 3806 in 3807 List 3808 [cadr entry; 3809 update_open_input_channels 3810 (add_pair channel (cons (car entry) (cddr entry)) 3811 (open_input_channels state_state)) state_state]), 3812*) 3813 3814(* 3815 [oracles: DEFUN ACL2::PEEK-CHAR$, DISK_THM] [axioms: ] [] 3816 |- peek_char_dollar channel state_state = 3817 (let entry = cdr (assoc_eq channel (open_input_channels state_state)) 3818 in 3819 cadr entry), 3820*) 3821 3822(* 3823 [oracles: DEFUN ACL2::READ-BYTE$, DISK_THM] [axioms: ] [] 3824 |- read_byte_dollar channel state_state = 3825 (let entry = cdr (assoc_eq channel (open_input_channels state_state)) 3826 in 3827 List 3828 [cadr entry; 3829 update_open_input_channels 3830 (add_pair channel (cons (car entry) (cddr entry)) 3831 (open_input_channels state_state)) state_state]), 3832*) 3833 3834(* 3835 [oracles: DEFUN ACL2::READ-OBJECT, DISK_THM] [axioms: ] [] 3836 |- read_object channel state_state = 3837 (let entry = cdr (assoc_eq channel (open_input_channels state_state)) 3838 in 3839 ite (cdr entry) 3840 (List 3841 [nil; cadr entry; 3842 update_open_input_channels 3843 (add_pair channel (cons (car entry) (cddr entry)) 3844 (open_input_channels state_state)) state_state]) 3845 (List [t; nil; state_state])), 3846*) 3847 3848(* 3849 [oracles: DEFUN ACL2::SOME-SLASHABLE, DISK_THM] [axioms: ] [] 3850 |- some_slashable l = 3851 itel 3852 [(endp l,nil); 3853 (member (car l) 3854 (List 3855 [chr #"\n"; chr #"\f"; chr #" "; chr #"\""; chr #"#"; 3856 chr #"'"; chr #"("; chr #")"; chr #","; chr #"."; chr #":"; 3857 chr #";"; chr #"\\"; chr #"`"; chr #"a"; chr #"b"; 3858 chr #"c"; chr #"d"; chr #"e"; chr #"f"; chr #"g"; chr #"h"; 3859 chr #"i"; chr #"j"; chr #"k"; chr #"l"; chr #"m"; chr #"n"; 3860 chr #"o"; chr #"p"; chr #"q"; chr #"r"; chr #"s"; chr #"t"; 3861 chr #"u"; chr #"v"; chr #"w"; chr #"x"; chr #"y"; chr #"z"; 3862 chr #"|"]),t)] (some_slashable (cdr l)), 3863*) 3864 3865(* 3866 [oracles: DEFUN ACL2::MAY-NEED-SLASHES, DISK_THM] [axioms: ] [] 3867 |- may_need_slashes x = 3868 (let l = coerce x (csym "LIST") in 3869 itel 3870 [(null l,null l); 3871 (andl 3872 [member (car l) 3873 (List 3874 [chr #"0"; chr #"1"; chr #"2"; chr #"3"; chr #"4"; 3875 chr #"5"; chr #"6"; chr #"7"; chr #"8"; chr #"9"; 3876 chr #"+"; chr #"-"; chr #"."; chr #"^"; chr #"_"]); 3877 not (member (car (last l)) (List [chr #"+"; chr #"-"]))], 3878 andl 3879 [member (car l) 3880 (List 3881 [chr #"0"; chr #"1"; chr #"2"; chr #"3"; chr #"4"; 3882 chr #"5"; chr #"6"; chr #"7"; chr #"8"; chr #"9"; 3883 chr #"+"; chr #"-"; chr #"."; chr #"^"; chr #"_"]); 3884 not (member (car (last l)) (List [chr #"+"; chr #"-"]))])] 3885 (some_slashable l)), 3886*) 3887 3888(* 3889 [oracles: DEFUN ACL2::T-STACK-LENGTH1] [axioms: ] [] 3890 |- t_stack_length1 state_state = length (t_stack state_state), 3891*) 3892 3893(* 3894 [oracles: DEFUN ACL2::T-STACK-LENGTH] [axioms: ] [] 3895 |- t_stack_length state_state = t_stack_length1 state_state, 3896*) 3897 3898(* 3899 [oracles: DEFUN ACL2::MAKE-LIST-AC, DISK_THM] [axioms: ] [] 3900 |- make_list_ac n val ac = 3901 ite (zp n) ac (make_list_ac (add (int ~1) n) val (cons val ac)), 3902*) 3903 3904(* 3905 [oracles: DEFUN ACL2::EXTEND-T-STACK] [axioms: ] [] 3906 |- extend_t_stack n val state_state = 3907 update_t_stack 3908 (binary_append (t_stack state_state) (make_list_ac n val nil)) 3909 state_state, 3910*) 3911 3912(* 3913 [oracles: DEFUN ACL2::FIRST-N-AC, DISK_THM] [axioms: ] [] 3914 |- first_n_ac i l ac = 3915 ite (zp i) (reverse ac) 3916 (first_n_ac (add (int ~1) i) (cdr l) (cons (car l) ac)), 3917*) 3918 3919(* 3920 [oracles: DEFUN ACL2::TAKE] [axioms: ] [] 3921 |- take n l = first_n_ac n l nil, 3922*) 3923 3924(* 3925 [oracles: DEFUN ACL2::SUBSEQ-LIST] [axioms: ] [] 3926 |- subseq_list lst start end = 3927 take (add end (unary_minus start)) (nthcdr start lst), 3928*) 3929 3930(* 3931 [oracles: DEFUN COMMON-LISP::SUBSEQ, DISK_THM] [axioms: ] [] 3932 |- subseq seq start end = 3933 ite (stringp seq) 3934 (coerce 3935 (subseq_list (coerce seq (csym "LIST")) start 3936 (ite end end (length seq))) (csym "STRING")) 3937 (subseq_list seq start (ite end end (length seq))), 3938*) 3939 3940(* 3941 [oracles: DEFUN COMMON-LISP::BUTLAST, DISK_THM] [axioms: ] [] 3942 |- butlast lst n = 3943 (let lng = len lst in 3944 ite (not (less n lng)) nil (take (add lng (unary_minus n)) lst)), 3945*) 3946 3947(* 3948 [oracles: DEFUN ACL2::SHRINK-T-STACK, DISK_THM] [axioms: ] [] 3949 |- shrink_t_stack n state_state = 3950 update_t_stack 3951 (first_n_ac 3952 (max (nat 0) 3953 (add (length (t_stack state_state)) (unary_minus n))) 3954 (t_stack state_state) nil) state_state, 3955*) 3956 3957(* 3958 [oracles: DEFUN ACL2::AREF-T-STACK] [axioms: ] [] 3959 |- aref_t_stack i state_state = nth i (t_stack state_state), 3960*) 3961 3962(* 3963 [oracles: DEFUN ACL2::ASET-T-STACK] [axioms: ] [] 3964 |- aset_t_stack i val state_state = 3965 update_t_stack (update_nth i val (t_stack state_state)) state_state, 3966*) 3967 3968(* 3969 [oracles: DEFUN ACL2::32-BIT-INTEGER-STACK-LENGTH1] [axioms: ] [] 3970 |- acl2_32_bit_integer_stack_length1 state_state = 3971 length (acl2_32_bit_integer_stack state_state), 3972*) 3973 3974(* 3975 [oracles: DEFUN ACL2::32-BIT-INTEGER-STACK-LENGTH] [axioms: ] [] 3976 |- acl2_32_bit_integer_stack_length state_state = 3977 acl2_32_bit_integer_stack_length1 state_state, 3978*) 3979 3980(* 3981 [oracles: DEFUN ACL2::EXTEND-32-BIT-INTEGER-STACK] [axioms: ] [] 3982 |- extend_32_bit_integer_stack n val state_state = 3983 update_32_bit_integer_stack 3984 (binary_append (acl2_32_bit_integer_stack state_state) 3985 (make_list_ac n val nil)) state_state, 3986*) 3987 3988(* 3989 [oracles: DEFUN ACL2::SHRINK-32-BIT-INTEGER-STACK, DISK_THM] [axioms: ] 3990 [] 3991 |- shrink_32_bit_integer_stack n state_state = 3992 update_32_bit_integer_stack 3993 (first_n_ac 3994 (max (nat 0) 3995 (add (length (acl2_32_bit_integer_stack state_state)) 3996 (unary_minus n))) (acl2_32_bit_integer_stack state_state) 3997 nil) state_state, 3998*) 3999 4000(* 4001 [oracles: DEFUN ACL2::AREF-32-BIT-INTEGER-STACK] [axioms: ] [] 4002 |- aref_32_bit_integer_stack i state_state = 4003 nth i (acl2_32_bit_integer_stack state_state), 4004*) 4005 4006(* 4007 [oracles: DEFUN ACL2::ASET-32-BIT-INTEGER-STACK] [axioms: ] [] 4008 |- aset_32_bit_integer_stack i val state_state = 4009 update_32_bit_integer_stack 4010 (update_nth i val (acl2_32_bit_integer_stack state_state)) 4011 state_state, 4012*) 4013 4014(* 4015 [oracles: DEFUN ACL2::BIG-CLOCK-NEGATIVE-P, DISK_THM] [axioms: ] [] 4016 |- big_clock_negative_p state_state = 4017 less (big_clock_entry state_state) (nat 0), 4018*) 4019 4020(* 4021 [oracles: DEFUN ACL2::DECREMENT-BIG-CLOCK, DISK_THM] [axioms: ] [] 4022 |- decrement_big_clock state_state = 4023 update_big_clock_entry (add (int ~1) (big_clock_entry state_state)) 4024 state_state, 4025*) 4026 4027(* 4028 [oracles: DEFUN ACL2::LIST-ALL-PACKAGE-NAMES, DISK_THM] [axioms: ] [] 4029 |- list_all_package_names state_state = 4030 List 4031 [car (list_all_package_names_lst state_state); 4032 update_list_all_package_names_lst 4033 (cdr (list_all_package_names_lst state_state)) state_state], 4034*) 4035 4036(* 4037 [oracles: DEFUN ACL2::USER-STOBJ-ALIST] [axioms: ] [] 4038 |- user_stobj_alist state_state = user_stobj_alist1 state_state, 4039*) 4040 4041(* 4042 [oracles: DEFUN ACL2::UPDATE-USER-STOBJ-ALIST] [axioms: ] [] 4043 |- update_user_stobj_alist x state_state = 4044 update_user_stobj_alist1 x state_state, 4045*) 4046 4047(* 4048 [oracles: DEFUN ACL2::POWER-EVAL, DISK_THM] [axioms: ] [] 4049 |- power_eval l b = 4050 ite (endp l) (nat 0) (add (car l) (mult b (power_eval (cdr l) b))), 4051*) 4052 4053(* 4054 [oracles: DEFUN ACL2::READ-IDATE, DISK_THM] [axioms: ] [] 4055 |- read_idate state_state = 4056 List 4057 [ite (null (idates state_state)) (nat 0) 4058 (car (idates state_state)); 4059 update_idates (cdr (idates state_state)) state_state], 4060*) 4061 4062(* 4063 [oracles: DEFUN ACL2::READ-RUN-TIME, DISK_THM] [axioms: ] [] 4064 |- read_run_time state_state = 4065 List 4066 [ite (null (run_times state_state)) (nat 0) 4067 (car (run_times state_state)); 4068 update_run_times (cdr (run_times state_state)) state_state], 4069*) 4070 4071(* 4072 [oracles: DEFUN ACL2::MAIN-TIMER, DISK_THM] [axioms: ] [] 4073 |- main_timer state = 4074 (let current_time = mv_nth (nat 0) (read_run_time state) in 4075 let old_value = 4076 ite 4077 (andl 4078 [boundp_global (asym "MAIN-TIMER") 4079 (mv_nth (nat 1) (read_run_time state)); 4080 rationalp 4081 (get_global (asym "MAIN-TIMER") 4082 (mv_nth (nat 1) (read_run_time state)))]) 4083 (get_global (asym "MAIN-TIMER") 4084 (mv_nth (nat 1) (read_run_time state))) (nat 0) 4085 in 4086 let state = 4087 put_global (asym "MAIN-TIMER") current_time 4088 (mv_nth (nat 1) (read_run_time state)) 4089 in 4090 List [add current_time (unary_minus old_value); state]), 4091*) 4092 4093(* 4094 [oracles: DEFUN ACL2::PUT-ASSOC-EQ, DISK_THM] [axioms: ] [] 4095 |- put_assoc_eq name val alist = 4096 itel 4097 [(endp alist,List [cons name val]); 4098 (eq name (caar alist),cons (cons name val) (cdr alist))] 4099 (cons (car alist) (put_assoc_eq name val (cdr alist))), 4100*) 4101 4102(* 4103 [oracles: DEFUN ACL2::PUT-ASSOC-EQL, DISK_THM] [axioms: ] [] 4104 |- put_assoc_eql name val alist = 4105 itel 4106 [(endp alist,List [cons name val]); 4107 (eql name (caar alist),cons (cons name val) (cdr alist))] 4108 (cons (car alist) (put_assoc_eql name val (cdr alist))), 4109*) 4110 4111(* 4112 [oracles: DEFUN ACL2::PUT-ASSOC-EQUAL, DISK_THM] [axioms: ] [] 4113 |- put_assoc_equal name val alist = 4114 itel 4115 [(endp alist,List [cons name val]); 4116 (equal name (caar alist),cons (cons name val) (cdr alist))] 4117 (cons (car alist) (put_assoc_equal name val (cdr alist))), 4118*) 4119 4120(* 4121 [oracles: DEFUN ACL2::SET-TIMER, DISK_THM] [axioms: ] [] 4122 |- set_timer name val state = 4123 put_global (asym "TIMER-ALIST") 4124 (put_assoc_eq name val (get_global (asym "TIMER-ALIST") state)) 4125 state, 4126*) 4127 4128(* 4129 [oracles: DEFUN ACL2::GET-TIMER, DISK_THM] [axioms: ] [] 4130 |- get_timer name state = 4131 cdr (assoc_eq name (get_global (asym "TIMER-ALIST") state)), 4132*) 4133 4134(* 4135 [oracles: DEFUN ACL2::PUSH-TIMER] [axioms: ] [] 4136 |- push_timer name val state = 4137 set_timer name (cons val (get_timer name state)) state, 4138*) 4139 4140(* 4141 [oracles: DEFUN ACL2::POP-TIMER, DISK_THM] [axioms: ] [] 4142 |- pop_timer name flg state = 4143 (let timer = get_timer name state in 4144 set_timer name 4145 (ite flg (cons (add (car timer) (cadr timer)) (cddr timer)) 4146 (cdr timer)) state), 4147*) 4148 4149(* 4150 [oracles: DEFUN ACL2::ADD-TIMERS, DISK_THM] [axioms: ] [] 4151 |- add_timers name1 name2 state = 4152 (let timer1 = get_timer name1 state in 4153 set_timer name1 4154 (cons (add (car timer1) (car (get_timer name2 state))) 4155 (cdr timer1)) state), 4156*) 4157 4158(* 4159 [oracles: DEFUN ACL2::INCREMENT-TIMER, DISK_THM] [axioms: ] [] 4160 |- increment_timer name state = 4161 (let timer = get_timer name state in 4162 let epsilon = mv_nth (nat 0) (main_timer state) in 4163 set_timer name (cons (add (car timer) epsilon) (cdr timer)) 4164 (mv_nth (nat 1) (main_timer state))), 4165*) 4166 4167(* 4168 [oracles: DEFUN ACL2::W, DISK_THM] [axioms: ] [] 4169 |- w state = get_global (asym "CURRENT-ACL2-WORLD") state, 4170*) 4171 4172(* 4173 [oracles: DEFUN ACL2::CURRENT-PACKAGE, DISK_THM] [axioms: ] [] 4174 |- current_package state = get_global (asym "CURRENT-PACKAGE") state, 4175*) 4176 4177(* 4178 [oracles: DEFUN ACL2::KNOWN-PACKAGE-ALIST, DISK_THM] [axioms: ] [] 4179 |- known_package_alist state = 4180 fgetprop (asym "KNOWN-PACKAGE-ALIST") (asym "GLOBAL-VALUE") nil 4181 (w state), 4182*) 4183 4184(* 4185 [oracles: DEFUN ACL2::SET-W, DISK_THM] [axioms: ] [] 4186 |- set_w flg wrld state = 4187 (let state = 4188 put_global (asym "CURRENT-ACL2-WORLD") (prog2_dollar flg wrld) 4189 state 4190 in 4191 ite 4192 (let entry = 4193 assoc_equal (current_package state) 4194 (known_package_alist state) 4195 in 4196 andl [not (caddr entry); entry]) state 4197 (put_global (asym "CURRENT-PACKAGE") (str ACL2) state)), 4198*) 4199 4200(* 4201 [oracles: DEFUN ACL2::UNION-EQ, DISK_THM] [axioms: ] [] 4202 |- union_eq lst1 lst2 = 4203 itel 4204 [(endp lst1,lst2); 4205 (member_eq (car lst1) lst2,union_eq (cdr lst1) lst2)] 4206 (cons (car lst1) (union_eq (cdr lst1) lst2)), 4207*) 4208 4209(* 4210 [oracles: DEFUN ACL2::LD-SKIP-PROOFSP, DISK_THM] [axioms: ] [] 4211 |- ld_skip_proofsp state = get_global (asym "LD-SKIP-PROOFSP") state, 4212*) 4213 4214(* 4215 [oracles: DEFUN ACL2::MAKE-VAR-LST1, DISK_THM] [axioms: ] [] 4216 |- make_var_lst1 root acl2_sym n acc = 4217 ite (zp n) acc 4218 (make_var_lst1 root acl2_sym (add (int ~1) n) 4219 (cons 4220 (intern_in_package_of_symbol 4221 (coerce 4222 (binary_append root 4223 (explode_nonnegative_integer (add (int ~1) n) 4224 (nat 10) nil)) (csym "STRING")) acl2_sym) acc)), 4225*) 4226 4227(* 4228 [oracles: DEFUN ACL2::MAKE-VAR-LST, DISK_THM] [axioms: ] [] 4229 |- make_var_lst acl2_sym n = 4230 make_var_lst1 (coerce (symbol_name acl2_sym) (csym "LIST")) acl2_sym 4231 n nil, 4232*) 4233 4234(* 4235 [oracles: DEFUN ACL2::NON-FREE-VAR-RUNES, DISK_THM] [axioms: ] [] 4236 |- non_free_var_runes runes free_var_runes_once free_var_runes_all acc = 4237 ite (endp runes) acc 4238 (non_free_var_runes (cdr runes) free_var_runes_once 4239 free_var_runes_all 4240 (ite 4241 (ite (member_equal (car runes) free_var_runes_once) 4242 (member_equal (car runes) free_var_runes_once) 4243 (member_equal (car runes) free_var_runes_all)) acc 4244 (cons (car runes) acc))), 4245*) 4246 4247(* 4248 [oracles: DEFUN ACL2::FREE-VAR-RUNES, DISK_THM] [axioms: ] [] 4249 |- free_var_runes flg wrld = 4250 ite (eq flg (ksym "ONCE")) 4251 (global_val (asym "FREE-VAR-RUNES-ONCE") wrld) 4252 (global_val (asym "FREE-VAR-RUNES-ALL") wrld), 4253*) 4254 4255(* 4256 [oracles: DEFUN ACL2::ABSOLUTE-PATHNAME-STRING-P, DISK_THM] [axioms: ] 4257 [] 4258 |- absolute_pathname_string_p acl2_str directoryp os = 4259 (let len = length acl2_str in 4260 andl 4261 [less (nat 0) (length acl2_str); 4262 ite (eq os (ksym "MSWINDOWS")) 4263 (let pos_colon = position (chr #":") acl2_str in 4264 andl 4265 [pos_colon; position (chr #"/") acl2_str; 4266 less pos_colon (position (chr #"/") acl2_str)]) 4267 (eql (char acl2_str (nat 0)) (chr #"/")); 4268 ite directoryp 4269 (eql (char acl2_str (add (int ~1) len)) (chr #"/")) t]), 4270*) 4271 4272(* 4273 [oracles: DEFUN ACL2::OS, DISK_THM] [axioms: ] [] 4274 |- os wrld = global_val (asym "OPERATING-SYSTEM") wrld, 4275*) 4276 4277(* 4278 [oracles: DEFUN ACL2::INCLUDE-BOOK-DIR-ALISTP, DISK_THM] [axioms: ] [] 4279 |- include_book_dir_alistp x os = 4280 ite (atom x) (null x) 4281 (andl 4282 [consp (car x); keywordp (caar x); stringp (cdar x); 4283 absolute_pathname_string_p (cdar x) t os; 4284 include_book_dir_alistp (cdr x) os]), 4285*) 4286 4287(* 4288 [oracles: DEFUN ACL2::TABLE-ALIST, DISK_THM] [axioms: ] [] 4289 |- table_alist name wrld = fgetprop name (asym "TABLE-ALIST") nil wrld, 4290*) 4291 4292(* 4293 [oracles: DEFUN ACL2::DEFAULT-VERIFY-GUARDS-EAGERNESS, DISK_THM] 4294 [axioms: ] [] 4295 |- default_verify_guards_eagerness wrld = 4296 ite 4297 (cdr 4298 (assoc_eq (ksym "VERIFY-GUARDS-EAGERNESS") 4299 (table_alist (asym "ACL2-DEFAULTS-TABLE") wrld))) 4300 (cdr 4301 (assoc_eq (ksym "VERIFY-GUARDS-EAGERNESS") 4302 (table_alist (asym "ACL2-DEFAULTS-TABLE") wrld))) (nat 1), 4303*) 4304 4305(* 4306 [oracles: DEFUN ACL2::DEFAULT-COMPILE-FNS, DISK_THM] [axioms: ] [] 4307 |- default_compile_fns wrld = 4308 cdr 4309 (assoc_eq (ksym "COMPILE-FNS") 4310 (table_alist (asym "ACL2-DEFAULTS-TABLE") wrld)), 4311*) 4312 4313(* 4314 [oracles: DEFUN ACL2::DEFAULT-MEASURE-FUNCTION, DISK_THM] [axioms: ] [] 4315 |- default_measure_function wrld = 4316 ite 4317 (cdr 4318 (assoc_eq (ksym "MEASURE-FUNCTION") 4319 (table_alist (asym "ACL2-DEFAULTS-TABLE") wrld))) 4320 (cdr 4321 (assoc_eq (ksym "MEASURE-FUNCTION") 4322 (table_alist (asym "ACL2-DEFAULTS-TABLE") wrld))) 4323 (asym "ACL2-COUNT"), 4324*) 4325 4326(* 4327 [oracles: DEFUN ACL2::DEFAULT-WELL-FOUNDED-RELATION, DISK_THM] 4328 [axioms: ] [] 4329 |- default_well_founded_relation wrld = 4330 ite 4331 (cdr 4332 (assoc_eq (ksym "WELL-FOUNDED-RELATION") 4333 (table_alist (asym "ACL2-DEFAULTS-TABLE") wrld))) 4334 (cdr 4335 (assoc_eq (ksym "WELL-FOUNDED-RELATION") 4336 (table_alist (asym "ACL2-DEFAULTS-TABLE") wrld))) (asym "O<"), 4337*) 4338 4339(* 4340 [oracles: DEFUN ACL2::GOOD-DEFUN-MODE-P, DISK_THM] [axioms: ] [] 4341 |- good_defun_mode_p p = 4342 member_eq p (List [ksym "LOGIC"; ksym "PROGRAM"]), 4343*) 4344 4345(* 4346 [oracles: DEFUN ACL2::DEFAULT-DEFUN-MODE, DISK_THM] [axioms: ] [] 4347 |- default_defun_mode wrld = 4348 (let val = 4349 cdr 4350 (assoc_eq (ksym "DEFUN-MODE") 4351 (table_alist (asym "ACL2-DEFAULTS-TABLE") wrld)) 4352 in 4353 ite (good_defun_mode_p val) val (ksym "PROGRAM")), 4354*) 4355 4356(* 4357 [oracles: DEFUN ACL2::DEFAULT-DEFUN-MODE-FROM-STATE] [axioms: ] [] 4358 |- default_defun_mode_from_state state = default_defun_mode (w state), 4359*) 4360 4361(* 4362 [oracles: DEFUN ACL2::INVISIBLE-FNS-TABLE, DISK_THM] [axioms: ] [] 4363 |- invisible_fns_table wrld = 4364 table_alist (asym "INVISIBLE-FNS-TABLE") wrld, 4365*) 4366 4367(* 4368 [oracles: DEFUN ACL2::UNARY-FUNCTION-SYMBOL-LISTP, DISK_THM] [axioms: ] 4369 [] 4370 |- unary_function_symbol_listp lst wrld = 4371 ite (atom lst) (null lst) 4372 (andl 4373 [symbolp (car lst); 4374 (let formals = fgetprop (car lst) (asym "FORMALS") nil wrld in 4375 andl [consp formals; null (cdr formals)]); 4376 unary_function_symbol_listp (cdr lst) wrld]), 4377*) 4378 4379(* 4380 [oracles: DEFUN ACL2::INVISIBLE-FNS-ENTRYP, DISK_THM] [axioms: ] [] 4381 |- invisible_fns_entryp key val wrld = 4382 andl 4383 [symbolp key; function_symbolp key wrld; 4384 unary_function_symbol_listp val wrld], 4385*) 4386 4387(* 4388 [oracles: DEFUN ACL2::DELETE-ASSOC-EQ, DISK_THM] [axioms: ] [] 4389 |- delete_assoc_eq key alist = 4390 itel [(endp alist,nil); (eq key (caar alist),cdr alist)] 4391 (cons (car alist) (delete_assoc_eq key (cdr alist))), 4392*) 4393 4394(* 4395 [oracles: DEFUN ACL2::DELETE-ASSOC-EQUAL, DISK_THM] [axioms: ] [] 4396 |- delete_assoc_equal key alist = 4397 itel [(endp alist,nil); (equal key (caar alist),cdr alist)] 4398 (cons (car alist) (delete_assoc_equal key (cdr alist))), 4399*) 4400 4401(* 4402 [oracles: DEFUN ACL2::BACKCHAIN-LIMIT, DISK_THM] [axioms: ] [] 4403 |- backchain_limit wrld = 4404 andl 4405 [cdr 4406 (assoc_eq (ksym "BACKCHAIN-LIMIT") 4407 (table_alist (asym "ACL2-DEFAULTS-TABLE") wrld)); 4408 cdr 4409 (assoc_eq (ksym "BACKCHAIN-LIMIT") 4410 (table_alist (asym "ACL2-DEFAULTS-TABLE") wrld))], 4411*) 4412 4413(* 4414 [oracles: DEFUN ACL2::DEFAULT-BACKCHAIN-LIMIT, DISK_THM] [axioms: ] [] 4415 |- default_backchain_limit wrld = 4416 andl 4417 [cdr 4418 (assoc_eq (ksym "DEFAULT-BACKCHAIN-LIMIT") 4419 (table_alist (asym "ACL2-DEFAULTS-TABLE") wrld)); 4420 cdr 4421 (assoc_eq (ksym "DEFAULT-BACKCHAIN-LIMIT") 4422 (table_alist (asym "ACL2-DEFAULTS-TABLE") wrld))], 4423*) 4424 4425(* 4426 [oracles: DEFUN ACL2::REWRITE-STACK-LIMIT, DISK_THM] [axioms: ] [] 4427 |- rewrite_stack_limit wrld = 4428 ite 4429 (cdr 4430 (assoc_eq (ksym "REWRITE-STACK-LIMIT") 4431 (table_alist (asym "ACL2-DEFAULTS-TABLE") wrld))) 4432 (cdr 4433 (assoc_eq (ksym "REWRITE-STACK-LIMIT") 4434 (table_alist (asym "ACL2-DEFAULTS-TABLE") wrld))) (nat 1000), 4435*) 4436 4437(* 4438 [oracles: DEFUN ACL2::CASE-SPLIT-LIMITATIONS, DISK_THM] [axioms: ] [] 4439 |- case_split_limitations wrld = 4440 cdr 4441 (assoc_eq (ksym "CASE-SPLIT-LIMITATIONS") 4442 (table_alist (asym "ACL2-DEFAULTS-TABLE") wrld)), 4443*) 4444 4445(* 4446 [oracles: DEFUN ACL2::BINOP-TABLE, DISK_THM] [axioms: ] [] 4447 |- binop_table wrld = table_alist (asym "BINOP-TABLE") wrld, 4448*) 4449 4450(* 4451 [oracles: DEFUN ACL2::MATCH-FREE-DEFAULT, DISK_THM] [axioms: ] [] 4452 |- match_free_default wrld = 4453 cdr 4454 (assoc_eq (ksym "MATCH-FREE-DEFAULT") 4455 (table_alist (asym "ACL2-DEFAULTS-TABLE") wrld)), 4456*) 4457 4458(* 4459 [oracles: DEFUN ACL2::MATCH-FREE-OVERRIDE, DISK_THM] [axioms: ] [] 4460 |- match_free_override wrld = 4461 (let pair = 4462 assoc_eq (ksym "MATCH-FREE-OVERRIDE") 4463 (table_alist (asym "ACL2-DEFAULTS-TABLE") wrld) 4464 in 4465 ite (ite (null pair) (null pair) (eq (cdr pair) (ksym "CLEAR"))) 4466 (ksym "CLEAR") 4467 (cons 4468 (cdr 4469 (assoc_eq (ksym "MATCH-FREE-OVERRIDE-NUME") 4470 (table_alist (asym "ACL2-DEFAULTS-TABLE") wrld))) 4471 (cdr pair))), 4472*) 4473 4474(* 4475 [oracles: DEFUN ACL2::NON-LINEARP, DISK_THM] [axioms: ] [] 4476 |- non_linearp wrld = 4477 (let temp = 4478 assoc_eq (ksym "NON-LINEARP") 4479 (table_alist (asym "ACL2-DEFAULTS-TABLE") wrld) 4480 in 4481 andl [temp; cdr temp]), 4482*) 4483 4484(* 4485 [oracles: DEFUN ACL2::MACRO-ALIASES, DISK_THM] [axioms: ] [] 4486 |- macro_aliases wrld = table_alist (asym "MACRO-ALIASES-TABLE") wrld, 4487*) 4488 4489(* 4490 [oracles: DEFUN ACL2::NTH-ALIASES, DISK_THM] [axioms: ] [] 4491 |- nth_aliases wrld = table_alist (asym "NTH-ALIASES-TABLE") wrld, 4492*) 4493 4494(* 4495 [oracles: DEFUN ACL2::DEFAULT-HINTS, DISK_THM] [axioms: ] [] 4496 |- default_hints wrld = 4497 cdr (assoc_eq t (table_alist (asym "DEFAULT-HINTS-TABLE") wrld)), 4498*) 4499 4500(* 4501 [oracles: DEFUN ACL2::FIX-TRUE-LIST, DISK_THM] [axioms: ] [] 4502 |- fix_true_list x = 4503 andl [consp x; cons (car x) (fix_true_list (cdr x))], 4504*) 4505 4506(* 4507 [oracles: DEFUN ACL2::BOOLEAN-LISTP, DISK_THM] [axioms: ] [] 4508 |- boolean_listp lst = 4509 ite (atom lst) (eq lst nil) 4510 (andl 4511 [ite (eq (car lst) t) (eq (car lst) t) (eq (car lst) nil); 4512 boolean_listp (cdr lst)]), 4513*) 4514 4515(* 4516 [oracles: DEFUN ACL2::WORMHOLE1] [axioms: ] [] 4517 |- wormhole1 name input form ld_specials = nil, 4518*) 4519 4520(* 4521 [oracles: DEFUN ACL2::ABORT!] [axioms: ] [] |- abort_exclaim = nil, 4522*) 4523 4524(* 4525 [oracles: DEFUN ACL2::FMT-TO-COMMENT-WINDOW] [axioms: ] [] 4526 |- fmt_to_comment_window acl2_str alist col evisc_tuple = nil, 4527*) 4528 4529(* 4530 [oracles: DEFUN ACL2::PAIRLIS2, DISK_THM] [axioms: ] [] 4531 |- pairlis2 x y = 4532 ite (endp y) nil 4533 (cons (cons (car x) (car y)) (pairlis2 (cdr x) (cdr y))), 4534*) 4535 4536(* 4537 [oracles: DEFUN ACL2::DUPLICATES, DISK_THM] [axioms: ] [] 4538 |- duplicates lst = 4539 itel 4540 [(endp lst,nil); 4541 (member_eq (car lst) (cdr lst), 4542 add_to_set_eq (car lst) (duplicates (cdr lst)))] 4543 (duplicates (cdr lst)), 4544*) 4545 4546(* 4547 [oracles: DEFUN ACL2::ADD-TO-SET-EQUAL, DISK_THM] [axioms: ] [] 4548 |- add_to_set_equal x l = ite (member_equal x l) l (cons x l), 4549*) 4550 4551(* 4552 [oracles: DEFUN ACL2::INTERSECTION-EQ, DISK_THM] [axioms: ] [] 4553 |- intersection_eq l1 l2 = 4554 itel 4555 [(endp l1,nil); 4556 (member_eq (car l1) l2, 4557 cons (car l1) (intersection_eq (cdr l1) l2))] 4558 (intersection_eq (cdr l1) l2), 4559*) 4560 4561(* 4562 [oracles: DEFUN ACL2::EVENS, DISK_THM] [axioms: ] [] 4563 |- evens l = ite (endp l) nil (cons (car l) (evens (cddr l))), 4564*) 4565 4566(* 4567 [oracles: DEFUN ACL2::ODDS] [axioms: ] [] |- odds l = evens (cdr l), 4568*) 4569 4570(* 4571 [oracles: DEFUN ACL2::SET-EQUALP-EQUAL, DISK_THM] [axioms: ] [] 4572 |- set_equalp_equal lst1 lst2 = 4573 andl [subsetp_equal lst1 lst2; subsetp_equal lst2 lst1], 4574*) 4575 4576(* 4577 [oracles: DEFUN ACL2::MFC-CLAUSE, DISK_THM] [axioms: ] [] 4578 |- mfc_clause mfc = 4579 andl 4580 [consp mfc; consp (cdr mfc); consp (cddr mfc); consp (cdddr mfc); 4581 consp (cddddr mfc); consp (cddddr (cdr mfc)); 4582 consp (cddddr (cddr mfc)); consp (cddddr (cdddr mfc)); 4583 consp (cddddr (cddddr mfc)); consp (car (cddddr (cddddr mfc))); 4584 consp (cdar (cddddr (cddddr mfc))); 4585 consp (cddar (cddddr (cddddr mfc))); 4586 consp (cdddar (cddddr (cddddr mfc))); 4587 consp (cddddr (car (cddddr (cddddr mfc)))); 4588 consp (car (cddddr (car (cddddr (cddddr mfc))))); 4589 pseudo_term_listp (cdar (cddddr (car (cddddr (cddddr mfc))))); 4590 cdar (cddddr (car (cddddr (cddddr mfc))))], 4591*) 4592 4593(* 4594 [oracles: DEFUN ACL2::TYPE-ALIST-ENTRYP, DISK_THM] [axioms: ] [] 4595 |- type_alist_entryp x = 4596 andl 4597 [consp x; pseudo_termp (car x); consp (cdr x); integerp (cadr x); 4598 not (less (cadr x) (int ~8192)); not (less (nat 8191) (cadr x))], 4599*) 4600 4601(* 4602 [oracles: DEFUN ACL2::TYPE-ALISTP, DISK_THM] [axioms: ] [] 4603 |- type_alistp x = 4604 ite (consp x) (andl [type_alist_entryp (car x); type_alistp (cdr x)]) 4605 (eq x nil), 4606*) 4607 4608(* 4609 [oracles: DEFUN ACL2::MFC-TYPE-ALIST, DISK_THM] [axioms: ] [] 4610 |- mfc_type_alist mfc = andl [consp mfc; type_alistp (car mfc); car mfc], 4611*) 4612 4613(* 4614 [oracles: DEFUN ACL2::MFC-ANCESTORS, DISK_THM] [axioms: ] [] 4615 |- mfc_ancestors mfc = 4616 andl 4617 [consp mfc; consp (cdr mfc); consp (cddr mfc); consp (cdddr mfc); 4618 consp (cddddr mfc); consp (cddddr (cdr mfc)); 4619 true_listp (car (cddddr (cdr mfc))); car (cddddr (cdr mfc))], 4620*) 4621 4622(* 4623 [oracles: DEFUN ACL2::BAD-ATOM, DISK_THM] [axioms: ] [] 4624 |- bad_atom x = 4625 not 4626 (itel 4627 [(consp x,consp x); (acl2_numberp x,acl2_numberp x); 4628 (symbolp x,symbolp x); (characterp x,characterp x)] 4629 (stringp x)), 4630*) 4631 4632val bad_atom_def = 4633 acl2Define "ACL2::BAD-ATOM" 4634 `bad_atom x = 4635 not 4636 (itel 4637 [(consp x,consp x); 4638 (acl2_numberp x,acl2_numberp x); 4639 (symbolp x,symbolp x); 4640 (characterp x,characterp x)] 4641 (stringp x))`; 4642 4643(* 4644 [oracles: DEFUN ACL2::ALPHORDER, DISK_THM] [axioms: ] [] 4645 |- alphorder x y = 4646 itel 4647 [(rationalp x,ite (rationalp y) (not (less y x)) t); 4648 (rationalp y,nil); 4649 (complex_rationalp x, 4650 ite (complex_rationalp y) 4651 (ite (less (realpart x) (realpart y)) 4652 (less (realpart x) (realpart y)) 4653 (andl 4654 [common_lisp_equal (realpart x) (realpart y); 4655 not (less (imagpart y) (imagpart x))])) t); 4656 (complex_rationalp y,nil); 4657 (characterp x, 4658 ite (characterp y) (not (less (char_code y) (char_code x))) t); 4659 (characterp y,nil); 4660 (stringp x,ite (stringp y) (andl [string_less_equal x y; t]) t); 4661 (stringp y,nil); 4662 (symbolp x,ite (symbolp y) (not (symbol_less y x)) t); 4663 (symbolp y,nil)] (bad_atom_less_equal x y), 4664*) 4665 4666val alphorder_def = 4667 acl2Define "ACL2::ALPHORDER" 4668 `alphorder x y = 4669 itel 4670 [(rationalp x,ite (rationalp y) (not (less y x)) t); 4671 (rationalp y,nil); 4672 (complex_rationalp x, 4673 ite (complex_rationalp y) 4674 (ite (less (realpart x) (realpart y)) 4675 (less (realpart x) (realpart y)) 4676 (andl 4677 [common_lisp_equal (realpart x) (realpart y); 4678 not (less (imagpart y) (imagpart x))])) t); 4679 (complex_rationalp y,nil); 4680 (characterp x, 4681 ite (characterp y) (not (less (char_code y) (char_code x))) t); 4682 (characterp y,nil); 4683 (stringp x,ite (stringp y) (andl [string_less_equal x y; t]) t); 4684 (stringp y,nil); 4685 (symbolp x,ite (symbolp y) (not (symbol_less y x)) t); 4686 (symbolp y,nil)] (bad_atom_less_equal x y)`; 4687 4688(* 4689 [oracles: DEFUN ACL2::LEXORDER, DISK_THM] [axioms: ] [] 4690 |- lexorder x y = 4691 itel 4692 [(atom x,ite (atom y) (alphorder x y) t); (atom y,nil); 4693 (equal (car x) (car y),lexorder (cdr x) (cdr y))] 4694 (lexorder (car x) (car y)), 4695*) 4696 4697val (lexorder_def,lexorder_ind) = 4698 acl2_defn "ACL2::LEXORDER" 4699 (`lexorder x y = 4700 itel 4701 [(atom x,ite (atom y) (alphorder x y) t); (atom y,nil); 4702 (equal (car x) (car y),lexorder (cdr x) (cdr y))] 4703 (lexorder (car x) (car y))`, 4704 WF_REL_TAC `measure (sexp_size o SND)` 4705 THEN ACL2_SIMP_TAC []); 4706 4707 4708(* 4709 [oracles: DEFUN ACL2::IF*, DISK_THM] [axioms: ] [] 4710 |- if_star x y z = ite x y z, 4711*) 4712 4713(* 4714 [oracles: DEFUN ACL2::RESIZE-LIST, DISK_THM] [axioms: ] [] 4715 |- resize_list lst n default_value = 4716 andl 4717 [integerp n; less (nat 0) n; 4718 cons (ite (atom lst) default_value (car lst)) 4719 (resize_list (ite (atom lst) lst (cdr lst)) (add (int ~1) n) 4720 default_value)], 4721*) 4722 4723(* 4724 [oracles: DEFUN ACL2::E/D-FN, DISK_THM] [axioms: ] [] 4725 |- e_slash_d_fn theory e_slash_d_list enable_p = 4726 itel 4727 [(atom e_slash_d_list,theory); 4728 (enable_p, 4729 e_slash_d_fn 4730 (List 4731 [asym "UNION-THEORIES"; theory; 4732 List [csym "QUOTE"; car e_slash_d_list]]) 4733 (cdr e_slash_d_list) nil)] 4734 (e_slash_d_fn 4735 (List 4736 [asym "SET-DIFFERENCE-THEORIES"; theory; 4737 List [csym "QUOTE"; car e_slash_d_list]]) 4738 (cdr e_slash_d_list) t), 4739*) 4740 4741val _ = export_acl2_theory(); 4742