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