acl2-books-certs 6.3-5 / usr / share / acl2-6.3 / books / misc / meta-lemmas.cert

(IN-PACKAGE "ACL2")
"ACL2 Version 6.3"
:BEGIN-PORTCULLIS-CMDS
:END-PORTCULLIS-CMDS
:EXPANSION-ALIST
((3 RECORD-EXPANSION (DEFEVALUATOR META-EV META-EV-LIST ((CAR X) (CDR X) (CONS X Y) (EQL X Y) (IF X Y Z) (MEMBER-EQUAL X Y) (NTH X Y) (TRUE-LISTP X))) (PROGN (RECORD-EXPANSION (WITH-OUTPUT :OFF ERROR :STACK :PUSH (MAKE-EVENT (ER-PROGN (WITH-OUTPUT :STACK :POP (DEFEVALUATOR-CHECK (QUOTE (DEFEVALUATOR META-EV META-EV-LIST ((CAR X) (CDR X) (CONS X Y) (EQL X Y) (IF X Y Z) (MEMBER-EQUAL X Y) (NTH X Y) (TRUE-LISTP X)))) (QUOTE META-EV) (QUOTE META-EV-LIST) (QUOTE ((CAR X) (CDR X) (CONS X Y) (EQL X Y) (IF X Y Z) (MEMBER-EQUAL X Y) (NTH X Y) (TRUE-LISTP X))) (QUOTE (DEFEVALUATOR . META-EV)) STATE)) (VALUE (QUOTE (VALUE-TRIPLE NIL)))))) (WITH-OUTPUT :OFF ERROR :STACK :PUSH (VALUE-TRIPLE NIL))) (ENCAPSULATE (((META-EV * *) => *) ((META-EV-LIST * *) => *)) (SET-INHIBIT-WARNINGS "theory") (LOCAL (IN-THEORY *DEFEVALUATOR-FORM-BASE-THEORY*)) (LOCAL (MUTUAL-RECURSION (DEFUN-NX META-EV (X A) (DECLARE (XARGS :VERIFY-GUARDS NIL :MEASURE (ACL2-COUNT X) :WELL-FOUNDED-RELATION O< :MODE :LOGIC)) (COND ((SYMBOLP X) (AND X (CDR (ASSOC-EQ X A)))) ((ATOM X) NIL) ((EQ (CAR X) (QUOTE QUOTE)) (CAR (CDR X))) ((CONSP (CAR X)) (META-EV (CAR (CDR (CDR (CAR X)))) (PAIRLIS$ (CAR (CDR (CAR X))) (META-EV-LIST (CDR X) A)))) ((EQUAL (CAR X) (QUOTE CAR)) (CAR (META-EV (CAR (CDR X)) A))) ((EQUAL (CAR X) (QUOTE CDR)) (CDR (META-EV (CAR (CDR X)) A))) ((EQUAL (CAR X) (QUOTE CONS)) (CONS (META-EV (CAR (CDR X)) A) (META-EV (CAR (CDR (CDR X))) A))) ((EQUAL (CAR X) (QUOTE EQL)) (EQL (META-EV (CAR (CDR X)) A) (META-EV (CAR (CDR (CDR X))) A))) ((EQUAL (CAR X) (QUOTE IF)) (IF (META-EV (CAR (CDR X)) A) (META-EV (CAR (CDR (CDR X))) A) (META-EV (CAR (CDR (CDR (CDR X)))) A))) ((EQUAL (CAR X) (QUOTE MEMBER-EQUAL)) (MEMBER-EQUAL (META-EV (CAR (CDR X)) A) (META-EV (CAR (CDR (CDR X))) A))) ((EQUAL (CAR X) (QUOTE NTH)) (NTH (META-EV (CAR (CDR X)) A) (META-EV (CAR (CDR (CDR X))) A))) ((EQUAL (CAR X) (QUOTE TRUE-LISTP)) (TRUE-LISTP (META-EV (CAR (CDR X)) A))) (T NIL))) (DEFUN-NX META-EV-LIST (X-LST A) (DECLARE (XARGS :MEASURE (ACL2-COUNT X-LST) :WELL-FOUNDED-RELATION O<)) (COND ((ENDP X-LST) NIL) (T (CONS (META-EV (CAR X-LST) A) (META-EV-LIST (CDR X-LST) A))))))) (LOCAL (DEFTHM EVAL-LIST-KWOTE-LST (EQUAL (META-EV-LIST (KWOTE-LST ARGS) A) (FIX-TRUE-LIST ARGS)))) (DEFTHMD META-EV-CONSTRAINT-0 (IMPLIES (AND (CONSP X) (SYNTAXP (NOT (EQUAL A (QUOTE (QUOTE NIL))))) (NOT (EQUAL (CAR X) (QUOTE QUOTE)))) (EQUAL (META-EV X A) (META-EV (CONS (CAR X) (KWOTE-LST (META-EV-LIST (CDR X) A))) NIL))) :HINTS (("Goal" :EXPAND ((:FREE (X) (HIDE X)) (META-EV X A)) :IN-THEORY (DISABLE (:EXECUTABLE-COUNTERPART META-EV))))) (DEFTHM META-EV-CONSTRAINT-1 (IMPLIES (SYMBOLP X) (EQUAL (META-EV X A) (AND X (CDR (ASSOC-EQUAL X A)))))) (DEFTHM META-EV-CONSTRAINT-2 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) (QUOTE QUOTE))) (EQUAL (META-EV X A) (CADR X)))) (DEFTHM META-EV-CONSTRAINT-3 (IMPLIES (AND (CONSP X) (CONSP (CAR X))) (EQUAL (META-EV X A) (META-EV (CADDAR X) (PAIRLIS$ (CADAR X) (META-EV-LIST (CDR X) A)))))) (DEFTHM META-EV-CONSTRAINT-4 (IMPLIES (NOT (CONSP X-LST)) (EQUAL (META-EV-LIST X-LST A) NIL))) (DEFTHM META-EV-CONSTRAINT-5 (IMPLIES (CONSP X-LST) (EQUAL (META-EV-LIST X-LST A) (CONS (META-EV (CAR X-LST) A) (META-EV-LIST (CDR X-LST) A))))) (DEFTHM META-EV-CONSTRAINT-6 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) (QUOTE CAR))) (EQUAL (META-EV X A) (CAR (META-EV (CADR X) A))))) (DEFTHM META-EV-CONSTRAINT-7 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) (QUOTE CDR))) (EQUAL (META-EV X A) (CDR (META-EV (CADR X) A))))) (DEFTHM META-EV-CONSTRAINT-8 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) (QUOTE CONS))) (EQUAL (META-EV X A) (CONS (META-EV (CADR X) A) (META-EV (CADDR X) A))))) (DEFTHM META-EV-CONSTRAINT-9 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) (QUOTE EQL))) (EQUAL (META-EV X A) (EQL (META-EV (CADR X) A) (META-EV (CADDR X) A))))) (DEFTHM META-EV-CONSTRAINT-10 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) (QUOTE IF))) (EQUAL (META-EV X A) (IF (META-EV (CADR X) A) (META-EV (CADDR X) A) (META-EV (CADDDR X) A))))) (DEFTHM META-EV-CONSTRAINT-11 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) (QUOTE MEMBER-EQUAL))) (EQUAL (META-EV X A) (MEMBER-EQUAL (META-EV (CADR X) A) (META-EV (CADDR X) A))))) (DEFTHM META-EV-CONSTRAINT-12 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) (QUOTE NTH))) (EQUAL (META-EV X A) (NTH (META-EV (CADR X) A) (META-EV (CADDR X) A))))) (DEFTHM META-EV-CONSTRAINT-13 (IMPLIES (AND (CONSP X) (EQUAL (CAR X) (QUOTE TRUE-LISTP))) (EQUAL (META-EV X A) (TRUE-LISTP (META-EV (CADR X) A)))))))))
NIL
(("/usr/share/acl2-6.3/books/misc/meta-lemmas.lisp" "meta-lemmas" "meta-lemmas" ((:SKIPPED-PROOFSP) (:AXIOMSP) (:TTAGS)) . 999152214))
1544461293