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