Welcome to Clozure Common Lisp Version 1.5-dev-r13559M-trunk (LinuxX8664)! ACL2 Version 3.6.1 built May 12, 2010 07:09:02. Copyright (C) 2009 University of Texas at Austin ACL2 comes with ABSOLUTELY NO WARRANTY. This is free software and you are welcome to redistribute it under certain conditions. For details, see the GNU General Public License. Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*). See the documentation topic note-3-6-1 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. ACL2 Version 3.6.1. Level 1. Cbd "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/defattach/". Distributed books directory "/v/filer4b/v11q001/acl2/devel/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>:q Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP). ? [RAW LISP] (f-put-global 'aok t *the-live-state*) ACL2_INVISIBLE::|The Live State Itself| ? [RAW LISP] (lp) ACL2 Version 3.6.1. Level 1. Cbd "/v/filer4b/v41q001/moore/public_html/acl2/seminar/2010.05-12-kaufmann/defattach/". Distributed books directory "/v/filer4b/v11q001/acl2/devel/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(encapsulate ((f (x) t :guard (true-listp x))) (local (defun f (x) x)) (defthm f-property (implies (consp x) (consp (f x))))) To verify that the two encapsulated events correctly extend the current theory we will evaluate them. The theory thus constructed is only ephemeral. Encapsulated Events: ACL2 !>>(LOCAL (DEFUN F (X) X)) Since F is non-recursive, its admission is trivial. We observe that the type of F is described by the theorem (EQUAL (F X) X). Summary Form: ( DEFUN F ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F ACL2 !>>(DEFTHM F-PROPERTY (IMPLIES (CONSP X) (CONSP (F X)))) ACL2 Warning [Non-rec] in ( DEFTHM F-PROPERTY ...): A :REWRITE rule generated from F-PROPERTY will be triggered only by terms containing the non-recursive function symbol F. Unless this function is disabled, this rule is unlikely ever to be used. But we reduce the conjecture to T, by the :type-prescription rule F. Q.E.D. Summary Form: ( DEFTHM F-PROPERTY ...) Rules: ((:TYPE-PRESCRIPTION F)) Warnings: Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F-PROPERTY End of Encapsulated Events. Having verified that the encapsulated events validate the signatures of the ENCAPSULATE event, we discard the ephemeral theory and extend the original theory as directed by the signatures and the non-LOCAL events. The following constraint is associated with the function F: (IMPLIES (CONSP X) (CONSP (F X))) Summary Form: ( ENCAPSULATE ((F ...) ...) ...) Rules: NIL Warnings: Non-rec Time: 0.01 seconds (prove: 0.00, print: 0.01, other: 0.00) T ACL2 !>(defun g (x) (declare (xargs :guard (or (consp x) (null x)))) (cons 17 (car x))) Since G is non-recursive, its admission is trivial. We observe that the type of G is described by the theorem (CONSP (G X)). We used primitive type reasoning. Computing the guard conjecture for G.... The guard conjecture for G is trivial to prove. G is compliant with Common Lisp. Summary Form: ( DEFUN G ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) G ACL2 !>(defattach f g) The guard proof obligation is (IMPLIES (TRUE-LISTP X) (OR (CONSP X) (NULL X))). But we reduce the conjecture to T, by case analysis. Q.E.D. This concludes the guard proof. We now prove that the attachment satisfies the required constraint. The goal to prove is (IMPLIES (CONSP X) (CONSP (G X))). But we reduce the conjecture to T, by the :type-prescription rule G. Q.E.D. Summary Form: ( DEFATTACH F G) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) :ATTACHMENTS-RECORDED ACL2 !>(f '(3 4)) (17 . 3) ACL2 !>(f 3) ACL2 Error in TOP-LEVEL: The guard for the function call (F X), which is (TRUE-LISTP X), is violated by the arguments in the call (F 3). To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users. ACL2 !>(trace$ f g) ((F) (G)) ACL2 !>(f '(3 4)) 1> (ACL2_*1*_ACL2::F (3 4)) 2> (F (3 4)) 3> (G (3 4)) <3 (G (17 . 3)) <2 (F (17 . 3)) <1 (ACL2_*1*_ACL2::F (17 . 3)) (17 . 3) ACL2 !>(f 3) 1> (ACL2_*1*_ACL2::F 3) ACL2 Error in TOP-LEVEL: The guard for the function call (F X), which is (TRUE-LISTP X), is violated by the arguments in the call (F 3). To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users. ACL2 !>(set-guard-checking nil) Masking guard violations but still checking guards except for self- recursive calls. To avoid guard checking entirely, :SET-GUARD-CHECKING :NONE. See :DOC set-guard-checking. ACL2 >(f '(3 4)) 1> (ACL2_*1*_ACL2::F (3 4)) 2> (F (3 4)) 3> (G (3 4)) <3 (G (17 . 3)) <2 (F (17 . 3)) <1 (ACL2_*1*_ACL2::F (17 . 3)) (17 . 3) ACL2 >(f 3) 1> (ACL2_*1*_ACL2::F 3) 2> (ACL2_*1*_ACL2::G 3) <2 (ACL2_*1*_ACL2::G (17)) <1 (ACL2_*1*_ACL2::F (17)) (17) ACL2 >(u) V 2:x(DEFUN G (X) ...) ACL2 >(f '(3 4)) 1> (ACL2_*1*_ACL2::F (3 4)) 2> (F (3 4)) ACL2 Error in TOP-LEVEL: ACL2 cannot ev the call of undefined function F on argument list: ((3 4)) To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 >(oops) Installing the requested world. ACL2 Observation in untracing: Untracing F. 3:x(DEFATTACH F G) ACL2 >(trace$ f) ; !! maybe shouldn't be necessary (one of the many details....) ((F)) ACL2 >(f '(3 4)) 1> (ACL2_*1*_ACL2::F (3 4)) 2> (F (3 4)) 3> (G (3 4)) <3 (G (17 . 3)) <2 (F (17 . 3)) <1 (ACL2_*1*_ACL2::F (17 . 3)) (17 . 3) ACL2 >(f 3) 1> (ACL2_*1*_ACL2::F 3) 2> (ACL2_*1*_ACL2::G 3) <2 (ACL2_*1*_ACL2::G (17)) <1 (ACL2_*1*_ACL2::F (17)) (17) ACL2 >(defattach f nil) ACL2 Observation in untracing: Untracing F. Summary Form: ( DEFATTACH F NIL) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) :ATTACHMENTS-RECORDED ACL2 >(f 3) ACL2 Error in TOP-LEVEL: ACL2 cannot ev the call of undefined function F on argument list: (3) To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 >(set-guard-checking t) Turning guard checking on, value T. ACL2 !>(f 3) ACL2 Error in TOP-LEVEL: The guard for the function call (F X), which is (TRUE-LISTP X), is violated by the arguments in the call (F 3). To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users. ACL2 !>(defattach f f) ACL2 Error in ( DEFATTACH F F): The proposed defattach event is illegal because the following is a loop in the resulting extended ancestor relation. See :DOC defattach. F is attached to F (or a sibling of it). F is an ancestor of F. Summary Form: ( DEFATTACH F F) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ACL2 Error in ( DEFATTACH F F): See :DOC failure. ******** FAILED ******** ACL2 !>(encapsulate ((h1 (x) t :guard (true-listp x))) (local (defun h1 (x) (cons x x))) (defthm h1-property (consp (h1 x)))) To verify that the two encapsulated events correctly extend the current theory we will evaluate them. The theory thus constructed is only ephemeral. Encapsulated Events: ACL2 !>>(LOCAL (DEFUN H1 (X) (CONS X X))) Since H1 is non-recursive, its admission is trivial. We observe that the type of H1 is described by the theorem (CONSP (H1 X)). We used primitive type reasoning. Summary Form: ( DEFUN H1 ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) H1 ACL2 !>>(DEFTHM H1-PROPERTY (CONSP (H1 X))) ACL2 Warning [Non-rec] in ( DEFTHM H1-PROPERTY ...): A :REWRITE rule generated from H1-PROPERTY will be triggered only by terms containing the non-recursive function symbol H1. Unless this function is disabled, this rule is unlikely ever to be used. But we reduce the conjecture to T, by the :type-prescription rule H1. Q.E.D. The storage of H1-PROPERTY depends upon the :type-prescription rule H1. Summary Form: ( DEFTHM H1-PROPERTY ...) Rules: ((:TYPE-PRESCRIPTION H1)) Warnings: Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) H1-PROPERTY End of Encapsulated Events. Having verified that the encapsulated events validate the signatures of the ENCAPSULATE event, we discard the ephemeral theory and extend the original theory as directed by the signatures and the non-LOCAL events. The following constraint is associated with the function H1: (CONSP (H1 X)) Summary Form: ( ENCAPSULATE ((H1 ...) ...) ...) Rules: NIL Warnings: Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) T ACL2 !>(defattach f h1) The guard proof obligation is (IMPLIES (TRUE-LISTP X) (TRUE-LISTP X)). But we reduce the conjecture to T, by case analysis. Q.E.D. This concludes the guard proof. We now prove that the attachment satisfies the required constraint. The goal to prove is (IMPLIES (CONSP X) (CONSP (H1 X))). But we reduce the conjecture to T, by the :executable-counterpart of IF and the simple :rewrite rule H1-PROPERTY. Q.E.D. Summary Form: ( DEFATTACH F H1) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) :ATTACHMENTS-RECORDED ACL2 !>(f '(3 4)) ACL2 Error in TOP-LEVEL: ACL2 cannot ev the call of undefined function H1 on argument list: ((3 4)) To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 !>(defun h2 (x) (list x x x)) Since H2 is non-recursive, its admission is trivial. We observe that the type of H2 is described by the theorem (AND (CONSP (H2 X)) (TRUE-LISTP (H2 X))). We used primitive type reasoning. Summary Form: ( DEFUN H2 ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) H2 ACL2 !>(defattach h1 h2) ACL2 Error in ( DEFATTACH H1 H2): Attachments must be guard-verified function symbols but H2 has not had its guard verified. See :DOC defattach. Summary Form: ( DEFATTACH H1 H2) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) ACL2 Error in ( DEFATTACH H1 H2): See :DOC failure. ******** FAILED ******** ACL2 !>(verify-guards h2) Computing the guard conjecture for H2.... The guard conjecture for H2 is trivial to prove. H2 is compliant with Common Lisp. Summary Form: ( VERIFY-GUARDS H2) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) H2 ACL2 !>(defattach h1 h2) The guard proof obligation is (IMPLIES (TRUE-LISTP X) T). But we reduce the conjecture to T, by case analysis. Q.E.D. This concludes the guard proof. We now prove that the attachment satisfies the required constraint. The goal to prove is (CONSP (H2 X)). But we reduce the conjecture to T, by the :type-prescription rule H2. Q.E.D. Summary Form: ( DEFATTACH H1 H2) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) :ATTACHMENTS-RECORDED ACL2 !>(f '(3 4)) ((3 4) (3 4) (3 4)) ACL2 !>(trace$ f h1 h2) ((F) (H1) (H2)) ACL2 !>(f '(3 4)) 1> (ACL2_*1*_ACL2::F (3 4)) 2> (F (3 4)) 3> (H1 (3 4)) 4> (H2 (3 4)) <4 (H2 ((3 4) (3 4) (3 4))) <3 (H1 ((3 4) (3 4) (3 4))) <2 (F ((3 4) (3 4) (3 4))) <1 (ACL2_*1*_ACL2::F ((3 4) (3 4) (3 4))) ((3 4) (3 4) (3 4)) ACL2 !>(f 3) 1> (ACL2_*1*_ACL2::F 3) ACL2 Error in TOP-LEVEL: The guard for the function call (F X), which is (TRUE-LISTP X), is violated by the arguments in the call (F 3). To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. See :DOC set-guard-checking for information about suppressing this check with (set-guard-checking :none), as recommended for new users. ACL2 !>(set-guard-checking nil) Masking guard violations but still checking guards except for self- recursive calls. To avoid guard checking entirely, :SET-GUARD-CHECKING :NONE. See :DOC set-guard-checking. ACL2 >(f 3) 1> (ACL2_*1*_ACL2::F 3) 2> (ACL2_*1*_ACL2::H1 3) 3> (ACL2_*1*_ACL2::H2 3) 4> (H2 3) <4 (H2 (3 3 3)) <3 (ACL2_*1*_ACL2::H2 (3 3 3)) <2 (ACL2_*1*_ACL2::H1 (3 3 3)) <1 (ACL2_*1*_ACL2::F (3 3 3)) (3 3 3) ACL2 >(defattach (f nil) (h1 nil)) ACL2 Observation in untracing: Untracing H1. ACL2 Observation in untracing: Untracing F. Summary Form: ( DEFATTACH (F NIL) ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) :ATTACHMENTS-RECORDED ACL2 >(defattach (f h1) (h1 h2)) We first consider the two guard proof obligations. The first (and last) guard proof obligation is (IMPLIES (TRUE-LISTP X) T). But we reduce the conjecture to T, by case analysis. Q.E.D. The second guard proof obligation is (IMPLIES (TRUE-LISTP X) (TRUE-LISTP X)). But we reduce the conjecture to T, by case analysis. Q.E.D. This concludes the two guard proofs. We now prove that the attachments satisfy the required constraint. The goal to prove is (AND (CONSP (H2 X)) (IMPLIES (CONSP X) (CONSP (H1 X)))). By the :executable-counterpart of IF and the simple :rewrite rule H1-PROPERTY we reduce the conjecture to Goal' (CONSP (H2 X)). But we reduce the conjecture to T, by the :type-prescription rule H2. Q.E.D. Summary Form: ( DEFATTACH (F H1) ...) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) :ATTACHMENTS-RECORDED ACL2 >(f '(3 4)) 1> (H2 (3 4)) <1 (H2 ((3 4) (3 4) (3 4))) ((3 4) (3 4) (3 4)) ACL2 >(u) 10:x(DEFATTACH (F NIL) (H1 NIL)) ACL2 >(in-theory (disable h1-property)) Summary Form: ( IN-THEORY (DISABLE ...)) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) 2122 ACL2 >(defattach (f h1) (h1 h2)) We first consider the two guard proof obligations. The first (and last) guard proof obligation is (IMPLIES (TRUE-LISTP X) T). But we reduce the conjecture to T, by case analysis. Q.E.D. The second guard proof obligation is (IMPLIES (TRUE-LISTP X) (TRUE-LISTP X)). But we reduce the conjecture to T, by case analysis. Q.E.D. This concludes the two guard proofs. We now prove that the attachments satisfy the required constraint. The goal to prove is (AND (CONSP (H2 X)) (IMPLIES (CONSP X) (CONSP (H1 X)))). By case analysis we reduce the conjecture to the following two conjectures. Subgoal 2 (CONSP (H2 X)). But we reduce the conjecture to T, by the :type-prescription rule H2. Subgoal 1 (IMPLIES (CONSP X) (CONSP (H1 X))). Name the formula above *1. No induction schemes are suggested by *1. Consequently, the proof attempt has failed. Summary Form: ( DEFATTACH (F H1) ...) Rules: ((:TYPE-PRESCRIPTION H2)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) --- The key checkpoint goal, below, may help you to debug this failure. See :DOC failure and see :DOC set-checkpoint-summary-limit. --- *** Key checkpoint at the top level: *** Subgoal 1 (IMPLIES (CONSP X) (CONSP (H1 X))) ACL2 Error in ( DEFATTACH (F H1) ...): See :DOC failure. ******** FAILED ******** ACL2 >(defattach (f h1) (h1 h2) ; succeeds because of hint: :hints (("Goal" :in-theory (enable h1-property)))) We first consider the two guard proof obligations. The first (and last) guard proof obligation is (IMPLIES (TRUE-LISTP X) T). But we reduce the conjecture to T, by case analysis. Q.E.D. The second guard proof obligation is (IMPLIES (TRUE-LISTP X) (TRUE-LISTP X)). But we reduce the conjecture to T, by case analysis. Q.E.D. This concludes the two guard proofs. We now prove that the attachments satisfy the required constraint. The goal to prove is (AND (CONSP (H2 X)) (IMPLIES (CONSP X) (CONSP (H1 X)))). [Note: A hint was supplied for our processing of the goal above. Thanks!] By the :executable-counterpart of IF and the simple :rewrite rule H1-PROPERTY we reduce the conjecture to Goal' (CONSP (H2 X)). But we reduce the conjecture to T, by the :type-prescription rule H2. Q.E.D. Summary Form: ( DEFATTACH (F H1) ...) Rules: NIL Warnings: None Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) :ATTACHMENTS-RECORDED ACL2 >:ubu! f 1:x(ENCAPSULATE ((F ...)) ...) ACL2 >(defun g (x) ; special-tail case for f (declare (xargs :guard (true-listp x))) (if (< 2 (len x)) (cons 17 (car x)) (f x))) Since G is non-recursive, its admission is trivial. We could deduce no constraints on the type of G. Computing the guard conjecture for G.... The guard conjecture for G is trivial to prove, given primitive type reasoning and the :type-prescription rule LEN. G is compliant with Common Lisp. Summary Form: ( DEFUN G ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL) (:TYPE-PRESCRIPTION LEN)) Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) G ACL2 >(defattach f g) The guard proof obligation is (IMPLIES (TRUE-LISTP X) (TRUE-LISTP X)). But we reduce the conjecture to T, by case analysis. Q.E.D. This concludes the guard proof. We now prove that the attachment satisfies the required constraint. The goal to prove is (IMPLIES (CONSP X) (CONSP (G X))). This simplifies, using the :definition G, to the following two conjectures. Subgoal 2 (IMPLIES (AND (CONSP X) (< 2 (LEN X))) (CONSP (CONS 17 (CAR X)))). But simplification reduces this to T, using primitive type reasoning. Subgoal 1 (IMPLIES (AND (CONSP X) (<= (LEN X) 2)) (CONSP (F X))). But simplification reduces this to T, using the :rewrite rule F-PROPERTY. Q.E.D. Summary Form: ( DEFATTACH F G) Rules: NIL Warnings: None Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) :ATTACHMENTS-RECORDED ACL2 >(f '(3 4 5)) (17 . 3) ACL2 >(f '(3 4)) ACL2 Error in TOP-LEVEL: ACL2 cannot ev the call of undefined function F on argument list: ((3 4)) To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 >(trace$ f g) ((F) (G)) ACL2 >(f '(3 4)) 1> (ACL2_*1*_ACL2::F (3 4)) 2> (F (3 4)) 3> (G (3 4)) 4> (F (3 4)) ACL2 Error in TOP-LEVEL: ACL2 cannot ev the call of undefined function F on argument list: ((3 4)) To debug see :DOC print-gv, see :DOC trace, and see :DOC wet. ACL2 >