acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / make-event / defrefine.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((9 RECORD-EXPANSION (DEFABSTRACTION GENERIC-FN (((F *) => *)) (LOCAL (DEFUN F (X) X)) (DEFTHM F-IS-NAT (IMPLIES (NATP X) (NATP (F X)))) (DEFTHM F-IS-CONS (IMPLIES (CONSP X) (CONSP (F X))))) (PROGN (ENCAPSULATE (((F *) => *)) (LOCAL (DEFUN F (X) X)) (DEFTHM F-IS-NAT (IMPLIES (NATP X) (NATP (F X)))) (DEFTHM F-IS-CONS (IMPLIES (CONSP X) (CONSP (F X))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((SIGNATURES (QUOTE (((F *) => *)))) (SIG (FIRST SIGNATURES)) (FARG (IF (CONSP (FIRST SIG)) (FIRST (FIRST SIG)) (FIRST SIG))) (VAL-TERM (CONSTRAINT FARG (W STATE))) (NAME (QUOTE GENERIC-FN))) (CONS (QUOTE PROGN) (CONS (CONS (QUOTE TABLE) (CONS (QUOTE ABSTRACTION-TABLE) (CONS (CONS (QUOTE QUOTE) (CONS NAME (QUOTE NIL))) (CONS (CONS (QUOTE QUOTE) (CONS VAL-TERM (QUOTE NIL))) (QUOTE NIL))))) (CONS (CONS (QUOTE DEFLABEL) (CONS NAME (QUOTE NIL))) (QUOTE NIL)))))) (PROGN (TABLE ABSTRACTION-TABLE (QUOTE GENERIC-FN) (QUOTE (IF (IMPLIES (NATP X) (NATP (F X))) (IMPLIES (CONSP X) (CONSP (F X))) (QUOTE NIL)))) (DEFLABEL GENERIC-FN))))) (10 RECORD-EXPANSION (DEFREFINE MORE-CONCRETE-FN GENERIC-FN ((((G *) => *)) (LOCAL (DEFUN G (X) X)) (DEFTHM FOO (IMPLIES (NATP X) (NATP (G X))))) :FUNCTIONAL-SUBSTITUTION ((F G))) (PROGN (ENCAPSULATE (((G *) => *)) (LOCAL (DEFUN G (X) X)) (DEFTHM FOO (IMPLIES (NATP X) (NATP (G X)))) (DEFTHM MORE-CONCRETE-FN-GENERIC-FN-ABSTRACTION-REFINEMENT (IF (IMPLIES (NATP X) (NATP (G X))) (IMPLIES (CONSP X) (CONSP (G X))) (QUOTE NIL)) :HINTS NIL :INSTRUCTIONS NIL :DOC NIL :RULE-CLASSES NIL :OTF-FLG NIL)) (RECORD-EXPANSION (MAKE-EVENT (LET* ((SIGNATURES (QUOTE (((G *) => *)))) (SIG (FIRST SIGNATURES)) (FARG (IF (CONSP (FIRST SIG)) (FIRST (FIRST SIG)) (FIRST SIG))) (VAL-TERM (CONSTRAINT FARG (W STATE))) (NAME (QUOTE MORE-CONCRETE-FN))) (CONS (QUOTE PROGN) (CONS (CONS (QUOTE TABLE) (CONS (QUOTE ABSTRACTION-TABLE) (CONS (CONS (QUOTE QUOTE) (CONS NAME (QUOTE NIL))) (CONS (CONS (QUOTE QUOTE) (CONS VAL-TERM (QUOTE NIL))) (QUOTE NIL))))) (CONS (CONS (QUOTE DEFLABEL) (CONS NAME (QUOTE NIL))) (QUOTE NIL)))))) (PROGN (TABLE ABSTRACTION-TABLE (QUOTE MORE-CONCRETE-FN) (QUOTE (IF (IMPLIES (NATP X) (NATP (G X))) (IMPLIES (CONSP X) (CONSP (G X))) (QUOTE NIL)))) (DEFLABEL MORE-CONCRETE-FN))))) (12 RECORD-EXPANSION (MUST-FAIL (DEFREFINE FLAWED-MORE-CONCRETE-FN GENERIC-FN ((((G *) => *)) (LOCAL (DEFUN G (X) (CONS 1 X))) (DEFTHM FOO (IMPLIES (NATP X) (CONSP (G X))))) :FUNCTIONAL-SUBSTITUTION ((F G)))) (VALUE-TRIPLE (QUOTE T))) (13 RECORD-EXPANSION (DEFREFINE EVEN-MORE-CONCRETE-FN MORE-CONCRETE-FN ((((C *) => *)) (LOCAL (DEFUN C (X) X)) (DEFTHM C-THM (IMPLIES (NOT (BAD-ATOM X)) (NOT (BAD-ATOM (C X)))))) :FUNCTIONAL-SUBSTITUTION ((G C))) (PROGN (ENCAPSULATE (((C *) => *)) (LOCAL (DEFUN C (X) X)) (DEFTHM C-THM (IMPLIES (NOT (BAD-ATOM X)) (NOT (BAD-ATOM (C X))))) (DEFTHM EVEN-MORE-CONCRETE-FN-MORE-CONCRETE-FN-ABSTRACTION-REFINEMENT (IF (IMPLIES (NATP X) (NATP (C X))) (IMPLIES (CONSP X) (CONSP (C X))) (QUOTE NIL)) :HINTS NIL :INSTRUCTIONS NIL :DOC NIL :RULE-CLASSES NIL :OTF-FLG NIL)) (RECORD-EXPANSION (MAKE-EVENT (LET* ((SIGNATURES (QUOTE (((C *) => *)))) (SIG (FIRST SIGNATURES)) (FARG (IF (CONSP (FIRST SIG)) (FIRST (FIRST SIG)) (FIRST SIG))) (VAL-TERM (CONSTRAINT FARG (W STATE))) (NAME (QUOTE EVEN-MORE-CONCRETE-FN))) (CONS (QUOTE PROGN) (CONS (CONS (QUOTE TABLE) (CONS (QUOTE ABSTRACTION-TABLE) (CONS (CONS (QUOTE QUOTE) (CONS NAME (QUOTE NIL))) (CONS (CONS (QUOTE QUOTE) (CONS VAL-TERM (QUOTE NIL))) (QUOTE NIL))))) (CONS (CONS (QUOTE DEFLABEL) (CONS NAME (QUOTE NIL))) (QUOTE NIL)))))) (PROGN (TABLE ABSTRACTION-TABLE (QUOTE EVEN-MORE-CONCRETE-FN) (QUOTE (IF (IMPLIES (NOT (BAD-ATOM X)) (NOT (BAD-ATOM (C X)))) (IF (IMPLIES (NATP X) (NATP (C X))) (IMPLIES (CONSP X) (CONSP (C X))) (QUOTE NIL)) (QUOTE NIL)))) (DEFLABEL EVEN-MORE-CONCRETE-FN))))) (14 RECORD-EXPANSION (DEFCONCRETIZE EVEN-MORE-CONCRETE-FN ((DEFUN D (X) X) (DEFTHM D-THM (EQUAL (D X) X))) :FUNCTIONAL-SUBSTITUTION ((C D))) (PROGN (DEFUN D (X) X) (DEFTHM D-THM (EQUAL (D X) X)) (DEFTHM EVEN-MORE-CONCRETE-FN-ABSTRACTION-CONCRETIZED (IF (IMPLIES (NOT (BAD-ATOM X)) (NOT (BAD-ATOM (D X)))) (IF (IMPLIES (NATP X) (NATP (D X))) (IMPLIES (CONSP X) (CONSP (D X))) (QUOTE NIL)) (QUOTE NIL)) :HINTS NIL :INSTRUCTIONS NIL :DOC NIL :RULE-CLASSES NIL :OTF-FLG NIL))) (15 RECORD-EXPANSION (DEFABSTRACTION FUBAR (((BAZ *) => *) ((BAR *) => *)) (LOCAL (DEFUN BAZ (X) X)) (LOCAL (DEFUN BAR (X) X)) (DEFTHM BAZ-THM (IMPLIES (NATP X) (NATP (BAZ X)))) (DEFTHM BAR-THM (IMPLIES (NATP X) (NATP (BAR X))))) (PROGN (ENCAPSULATE (((BAZ *) => *) ((BAR *) => *)) (LOCAL (DEFUN BAZ (X) X)) (LOCAL (DEFUN BAR (X) X)) (DEFTHM BAZ-THM (IMPLIES (NATP X) (NATP (BAZ X)))) (DEFTHM BAR-THM (IMPLIES (NATP X) (NATP (BAR X))))) (RECORD-EXPANSION (MAKE-EVENT (LET* ((SIGNATURES (QUOTE (((BAZ *) => *) ((BAR *) => *)))) (SIG (FIRST SIGNATURES)) (FARG (IF (CONSP (FIRST SIG)) (FIRST (FIRST SIG)) (FIRST SIG))) (VAL-TERM (CONSTRAINT FARG (W STATE))) (NAME (QUOTE FUBAR))) (CONS (QUOTE PROGN) (CONS (CONS (QUOTE TABLE) (CONS (QUOTE ABSTRACTION-TABLE) (CONS (CONS (QUOTE QUOTE) (CONS NAME (QUOTE NIL))) (CONS (CONS (QUOTE QUOTE) (CONS VAL-TERM (QUOTE NIL))) (QUOTE NIL))))) (CONS (CONS (QUOTE DEFLABEL) (CONS NAME (QUOTE NIL))) (QUOTE NIL)))))) (PROGN (TABLE ABSTRACTION-TABLE (QUOTE FUBAR) (QUOTE (IF (IMPLIES (NATP X) (NATP (BAZ X))) (IMPLIES (NATP X) (NATP (BAR X))) (QUOTE NIL)))) (DEFLABEL FUBAR))))) (16 RECORD-EXPANSION (DEFREFINE CONCRETE-BAZ-ABSTRACT-BAR FUBAR ((((C-BAZ *) => *)) (LOCAL (DEFUN C-BAZ (X) X)) (DEFTHM C-BAZ-THM (IMPLIES (INTEGERP X) (INTEGERP (C-BAZ X))))) :THM-NAME BAR-ONLY :FUNCTIONAL-SUBSTITUTION ((BAZ C-BAZ))) (PROGN (ENCAPSULATE (((C-BAZ *) => *)) (LOCAL (DEFUN C-BAZ (X) X)) (DEFTHM C-BAZ-THM (IMPLIES (INTEGERP X) (INTEGERP (C-BAZ X)))) (DEFTHM BAR-ONLY (IF (IMPLIES (NATP X) (NATP (C-BAZ X))) (IMPLIES (NATP X) (NATP (BAR X))) (QUOTE NIL)) :HINTS NIL :INSTRUCTIONS NIL :DOC NIL :RULE-CLASSES NIL :OTF-FLG NIL)) (RECORD-EXPANSION (MAKE-EVENT (LET* ((SIGNATURES (QUOTE (((C-BAZ *) => *)))) (SIG (FIRST SIGNATURES)) (FARG (IF (CONSP (FIRST SIG)) (FIRST (FIRST SIG)) (FIRST SIG))) (VAL-TERM (CONSTRAINT FARG (W STATE))) (NAME (QUOTE CONCRETE-BAZ-ABSTRACT-BAR))) (CONS (QUOTE PROGN) (CONS (CONS (QUOTE TABLE) (CONS (QUOTE ABSTRACTION-TABLE) (CONS (CONS (QUOTE QUOTE) (CONS NAME (QUOTE NIL))) (CONS (CONS (QUOTE QUOTE) (CONS VAL-TERM (QUOTE NIL))) (QUOTE NIL))))) (CONS (CONS (QUOTE DEFLABEL) (CONS NAME (QUOTE NIL))) (QUOTE NIL)))))) (PROGN (TABLE ABSTRACTION-TABLE (QUOTE CONCRETE-BAZ-ABSTRACT-BAR) (QUOTE (IF (IMPLIES (INTEGERP X) (INTEGERP (C-BAZ X))) (IF (IMPLIES (NATP X) (NATP (C-BAZ X))) (IMPLIES (NATP X) (NATP (BAR X))) (QUOTE NIL)) (QUOTE NIL)))) (DEFLABEL CONCRETE-BAZ-ABSTRACT-BAR))))) (17 RECORD-EXPANSION (DEFREFINE CONCRETE-BAZ-CONCRETE-BAR CONCRETE-BAZ-ABSTRACT-BAR ((((C-BAR *) => *)) (LOCAL (DEFUN C-BAR (X) X)) (DEFTHM C-BAR-THM (IMPLIES (INTEGERP X) (INTEGERP (C-BAR X))))) :FUNCTIONAL-SUBSTITUTION ((BAR C-BAR)) :HINTS (("Goal" :USE ((:INSTANCE BAR-ONLY))))) (PROGN (ENCAPSULATE (((C-BAR *) => *)) (LOCAL (DEFUN C-BAR (X) X)) (DEFTHM C-BAR-THM (IMPLIES (INTEGERP X) (INTEGERP (C-BAR X)))) (DEFTHM CONCRETE-BAZ-CONCRETE-BAR-CONCRETE-BAZ-ABSTRACT-BAR-ABSTRACTION-REFINEMENT (IF (IMPLIES (INTEGERP X) (INTEGERP (C-BAZ X))) (IF (IMPLIES (NATP X) (NATP (C-BAZ X))) (IMPLIES (NATP X) (NATP (C-BAR X))) (QUOTE NIL)) (QUOTE NIL)) :HINTS (("Goal" :USE ((:INSTANCE BAR-ONLY)))) :INSTRUCTIONS NIL :DOC NIL :RULE-CLASSES NIL :OTF-FLG NIL)) (RECORD-EXPANSION (MAKE-EVENT (LET* ((SIGNATURES (QUOTE (((C-BAR *) => *)))) (SIG (FIRST SIGNATURES)) (FARG (IF (CONSP (FIRST SIG)) (FIRST (FIRST SIG)) (FIRST SIG))) (VAL-TERM (CONSTRAINT FARG (W STATE))) (NAME (QUOTE CONCRETE-BAZ-CONCRETE-BAR))) (CONS (QUOTE PROGN) (CONS (CONS (QUOTE TABLE) (CONS (QUOTE ABSTRACTION-TABLE) (CONS (CONS (QUOTE QUOTE) (CONS NAME (QUOTE NIL))) (CONS (CONS (QUOTE QUOTE) (CONS VAL-TERM (QUOTE NIL))) (QUOTE NIL))))) (CONS (CONS (QUOTE DEFLABEL) (CONS NAME (QUOTE NIL))) (QUOTE NIL)))))) (PROGN (TABLE ABSTRACTION-TABLE (QUOTE CONCRETE-BAZ-CONCRETE-BAR) (QUOTE (IF (IMPLIES (INTEGERP X) (INTEGERP (C-BAR X))) (IF (IMPLIES (INTEGERP X) (INTEGERP (C-BAZ X))) (IF (IMPLIES (NATP X) (NATP (C-BAZ X))) (IMPLIES (NATP X) (NATP (C-BAR X))) (QUOTE NIL)) (QUOTE NIL)) (QUOTE NIL)))) (DEFLABEL CONCRETE-BAZ-CONCRETE-BAR))))) (18 RECORD-EXPANSION (DEFCONCRETIZE CONCRETE-BAZ-CONCRETE-BAR ((DEFUN CONCRETE-C-BAZ (X) (NFIX X)) (DEFUN CONCRETE-C-BAR (X) (IFIX X))) :FUNCTIONAL-SUBSTITUTION ((C-BAZ CONCRETE-C-BAZ) (C-BAR CONCRETE-C-BAR))) (PROGN (DEFUN CONCRETE-C-BAZ (X) (NFIX X)) (DEFUN CONCRETE-C-BAR (X) (IFIX X)) (DEFTHM CONCRETE-BAZ-CONCRETE-BAR-ABSTRACTION-CONCRETIZED (IF (IMPLIES (INTEGERP X) (INTEGERP (CONCRETE-C-BAR X))) (IF (IMPLIES (INTEGERP X) (INTEGERP (CONCRETE-C-BAZ X))) (IF (IMPLIES (NATP X) (NATP (CONCRETE-C-BAZ X))) (IMPLIES (NATP X) (NATP (CONCRETE-C-BAR X))) (QUOTE NIL)) (QUOTE NIL)) (QUOTE NIL)) :HINTS NIL :INSTRUCTIONS NIL :DOC NIL :RULE-CLASSES NIL :OTF-FLG NIL))))
NIL
(("/usr/share/acl2-6.3/books/make-event/defrefine.lisp" "defrefine" "defrefine" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1475637815) ("/usr/share/acl2-6.3/books/misc/eval.lisp" "misc/eval" "eval" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 1069973718))
2077555422