bash-3.2$ acl2 Welcome to Clozure Common Lisp Version 1.6-r14468M (DarwinX8632)! ACL2 Version 4.2 built January 11, 2011 18:23:37. Copyright (C) 2011 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-4-2 for recent changes. Note: We have modified the prompt in some underlying Lisps to further distinguish it from the ACL2 prompt. ACL2 Version 4.2. Level 1. Cbd "/Users/nwetzler/". Distributed books directory "/acl2/acl2-sources/books/". Type :help for help. Type (good-bye) to quit completely out of ACL2. ACL2 !>(include-book "arithmetic-5/top" :dir :system) To turn on non-linear arithmetic, execute : (SET-DEFAULT-HINTS '((NONLINEARP-DEFAULT-HINT STABLE-UNDER-SIMPLIFICATIONP HIST PSPV))) or : (SET-DEFAULT-HINTS '((NONLINEARP-DEFAULT-HINT++ ID STABLE-UNDER-SIMPLIFICATIONP HIST NIL))) See the README for more about non-linear arithmetic and general information about using this library. Summary Form: ( INCLUDE-BOOK "arithmetic-5/top" ...) Rules: NIL Time: 0.42 seconds (prove: 0.00, print: 0.00, other: 0.42) "/acl2/acl2-sources/books/arithmetic-5/top.lisp" ACL2 !>(defmacro print-theory-since-start () `(let ((world (w state))) (set-difference-theories (current-theory :here) (theory 'start)))) Summary Form: ( DEFMACRO PRINT-THEORY-SINCE-START ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) PRINT-THEORY-SINCE-START ACL2 !>(deftheory start (current-theory :here)) Summary Form: ( DEFTHEORY START ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) 3826 ACL2 !>(defun f (x y) (+ x y)) Since F is non-recursive, its admission is trivial. We observe that the type of F is described by the theorem (ACL2-NUMBERP (F X Y)). We used primitive type reasoning. Summary Form: ( DEFUN F ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F ACL2 !>(defthm f-commutes (implies (and (integerp x) (integerp y)) (equal (f y x) (f x y)))) ACL2 Warning [Non-rec] in ( DEFTHM F-COMMUTES ...): A :REWRITE rule generated from F-COMMUTES 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. ACL2 Warning [Subsume] in ( DEFTHM F-COMMUTES ...): The previously added rule F subsumes a newly proposed :REWRITE rule generated from F-COMMUTES, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application. By the simple :definition F we reduce the conjecture to Goal' (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (+ Y X) (+ X Y))). But simplification reduces this to T, using linear arithmetic and primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM F-COMMUTES ...) Rules: ((:DEFINITION F) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: Subsume and Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F-COMMUTES ACL2 !>(print-theory-since-start) ((:REWRITE F-COMMUTES) (:TYPE-PRESCRIPTION F) (:EXECUTABLE-COUNTERPART F) (:DEFINITION F)) ACL2 !>(ubu! 'start) 3:x(DEFTHEORY START (CURRENT-THEORY :HERE)) ACL2 !>(encapsulate (((f * *) => *) ; two constrained functions of two arguments ((g * *) => *)) (local ; local witnesses for the contstrained functions (defun f (x y) (+ x y))) (local (defun g (x y) (- x y))) (defthm f-commutes ; some nice theorems about f and g (implies (and (integerp x) ; or "constraints" (integerp y)) (equal (f y x) (f x y)))) (defthm g-does-not-commute (implies (and (integerp x) (integerp y) (not (equal x y))) (not (equal (g y x) (g x y))))) ) To verify that the four 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 Y) (+ X Y))) Since F is non-recursive, its admission is trivial. We observe that the type of F is described by the theorem (ACL2-NUMBERP (F X Y)). We used primitive type reasoning. Summary Form: ( DEFUN F ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F ACL2 !>>(LOCAL (DEFUN G (X Y) (- X Y))) Since G is non-recursive, its admission is trivial. We observe that the type of G is described by the theorem (ACL2-NUMBERP (G X Y)). We used primitive type reasoning. Summary Form: ( DEFUN G ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) G ACL2 !>>(DEFTHM F-COMMUTES (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F Y X) (F X Y)))) ACL2 Warning [Non-rec] in ( DEFTHM F-COMMUTES ...): A :REWRITE rule generated from F-COMMUTES 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. ACL2 Warning [Subsume] in ( DEFTHM F-COMMUTES ...): The previously added rule F subsumes a newly proposed :REWRITE rule generated from F-COMMUTES, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application. By the simple :definition F we reduce the conjecture to Goal' (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (+ Y X) (+ X Y))). But simplification reduces this to T, using linear arithmetic and primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM F-COMMUTES ...) Rules: ((:DEFINITION F) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: Subsume and Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F-COMMUTES ACL2 !>>(DEFTHM G-DOES-NOT-COMMUTE (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G Y X) (G X Y))))) ACL2 Warning [Non-rec] in ( DEFTHM G-DOES-NOT-COMMUTE ...): A :REWRITE rule generated from G-DOES-NOT-COMMUTE will be triggered only by terms containing the non-recursive function symbol G. Unless this function is disabled, this rule is unlikely ever to be used. By the simple :definition G we reduce the conjecture to Goal' (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (+ Y (- X)) (+ X (- Y))))). But simplification reduces this to T, using linear arithmetic and primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM G-DOES-NOT-COMMUTE ...) Rules: ((:DEFINITION G) (:DEFINITION NOT) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) G-DOES-NOT-COMMUTE 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 both of the functions F and G: (AND (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F Y X) (F X Y))) (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G Y X) (G X Y))))) Summary Form: ( ENCAPSULATE (((F * ...) ...) ...) ...) Rules: NIL Warnings: Subsume and Non-rec Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) T ACL2 !>(print-theory-since-start) ((:REWRITE G-DOES-NOT-COMMUTE) (:REWRITE F-COMMUTES)) 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 !>:pe f 4:x(ENCAPSULATE (((F * *) => *) ((G * *) => *)) (LOCAL (DEFUN F (X Y) (+ X Y))) (LOCAL (DEFUN G (X Y) (- X Y))) (DEFTHM F-COMMUTES (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F Y X) (F X Y)))) (DEFTHM G-DOES-NOT-COMMUTE (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G Y X) (G X Y)))))) ACL2 !>(ubu! 'start) 3:x(DEFTHEORY START (CURRENT-THEORY :HERE)) ACL2 !>(encapsulate ; note that this time we've added guards to the constrained functions (((f * *) => * :formals (x y) :guard (and (integerp x) (integerp y))) ((g * *) => * :formals (x y) :guard (and (integerp x) (integerp y)))) ; and guards to the witnesses (local (defun f (x y) (+ x y))) (local (defun g (x y) (- x y))) (defthm f-commutes (implies (and (integerp x) (integerp y)) (equal (f y x) (f x y)))) (defthm g-does-not-commute (implies (and (integerp x) (integerp y) (not (equal x y))) (not (equal (g y x) (g x y))))) ) To verify that the four 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 Y) (+ X Y))) Since F is non-recursive, its admission is trivial. We observe that the type of F is described by the theorem (ACL2-NUMBERP (F X Y)). We used primitive type reasoning. Summary Form: ( DEFUN F ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F ACL2 !>>(LOCAL (DEFUN G (X Y) (- X Y))) Since G is non-recursive, its admission is trivial. We observe that the type of G is described by the theorem (ACL2-NUMBERP (G X Y)). We used primitive type reasoning. Summary Form: ( DEFUN G ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) G ACL2 !>>(DEFTHM F-COMMUTES (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F Y X) (F X Y)))) ACL2 Warning [Non-rec] in ( DEFTHM F-COMMUTES ...): A :REWRITE rule generated from F-COMMUTES 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. ACL2 Warning [Subsume] in ( DEFTHM F-COMMUTES ...): The previously added rule F subsumes a newly proposed :REWRITE rule generated from F-COMMUTES, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application. By the simple :definition F we reduce the conjecture to Goal' (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (+ Y X) (+ X Y))). But simplification reduces this to T, using linear arithmetic and primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM F-COMMUTES ...) Rules: ((:DEFINITION F) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: Subsume and Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F-COMMUTES ACL2 !>>(DEFTHM G-DOES-NOT-COMMUTE (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G Y X) (G X Y))))) ACL2 Warning [Non-rec] in ( DEFTHM G-DOES-NOT-COMMUTE ...): A :REWRITE rule generated from G-DOES-NOT-COMMUTE will be triggered only by terms containing the non-recursive function symbol G. Unless this function is disabled, this rule is unlikely ever to be used. By the simple :definition G we reduce the conjecture to Goal' (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (+ Y (- X)) (+ X (- Y))))). But simplification reduces this to T, using linear arithmetic and primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM G-DOES-NOT-COMMUTE ...) Rules: ((:DEFINITION G) (:DEFINITION NOT) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) G-DOES-NOT-COMMUTE 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 both of the functions F and G: (AND (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F Y X) (F X Y))) (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G Y X) (G X Y))))) Summary Form: ( ENCAPSULATE (((F * ...) ...) ...) ...) Rules: NIL Warnings: Subsume and Non-rec Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.01) T ACL2 !>(defun f-exec (x y) (declare (xargs :guard (and (rationalp x) (rationalp y)))) (* x y)) Since F-EXEC is non-recursive, its admission is trivial. We observe that the type of F-EXEC is described by the theorem (ACL2-NUMBERP (F-EXEC X Y)). We used primitive type reasoning. Computing the guard conjecture for F-EXEC.... The guard conjecture for F-EXEC is trivial to prove. F-EXEC is compliant with Common Lisp. Summary Form: ( DEFUN F-EXEC ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F-EXEC ACL2 !>(defun g-exec (x y) (declare (xargs :guard (and (rationalp x) (rationalp y)))) (< x y)) Since G-EXEC is non-recursive, its admission is trivial. We observe that the type of G-EXEC is described by the theorem (OR (EQUAL (G-EXEC X Y) T) (EQUAL (G-EXEC X Y) NIL)). Computing the guard conjecture for G-EXEC.... The guard conjecture for G-EXEC is trivial to prove. G-EXEC is compliant with Common Lisp. Summary Form: ( DEFUN G-EXEC ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) G-EXEC ACL2 !>(defattach (f f-exec) (g g-exec)) We first consider the two guard proof obligations. The first guard proof obligation is (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (AND (RATIONALP X) (RATIONALP Y))). But we reduce the conjecture to T, by case analysis. Q.E.D. The second (and last) guard proof obligation is (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (AND (RATIONALP X) (RATIONALP Y))). 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 (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F-EXEC Y X) (F-EXEC X Y))) (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G-EXEC Y X) (G-EXEC X Y))))). By the simple :definitions F-EXEC and G-EXEC we reduce the conjecture to the following two conjectures. Subgoal 2 (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (* Y X) (* X Y))). But simplification reduces this to T, using primitive type reasoning and the :rewrite rule |(* y x)|. Subgoal 1 (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (< Y X) (< X Y)))). This simplifies, using the :compound-recognizer rule BOOLEANP-COMPOUND-RECOGNIZER, the :definitions IFF and SYNP and the :rewrite rule EQUAL-OF-PREDICATES-REWRITE, to the following two conjectures. Subgoal 1.2 (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y)) (<= X Y)) (< X Y)). But simplification reduces this to T, using linear arithmetic. Subgoal 1.1 (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y)) (< Y X)) (<= Y X)). But simplification reduces this to T, using linear arithmetic. Q.E.D. Summary Form: ( DEFATTACH (F F-EXEC) ...) Rules: ((:COMPOUND-RECOGNIZER BOOLEANP-COMPOUND-RECOGNIZER) (:DEFINITION F-EXEC) (:DEFINITION G-EXEC) (:DEFINITION IFF) (:DEFINITION NOT) (:DEFINITION SYNP) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:REWRITE |(* y x)|) (:REWRITE EQUAL-OF-PREDICATES-REWRITE)) Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) :ATTACHMENTS-RECORDED ACL2 !>(f 3 4) 12 ACL2 !>(f 1/2 1/4) 1/8 ACL2 !>(defun h (x y) (declare (xargs :guard (and (integerp x) (integerp y)))) (f x y)) Since H is non-recursive, its admission is trivial. We could deduce no constraints on the type of H. Computing the guard conjecture for H.... The guard conjecture for H is trivial to prove. H is compliant with Common Lisp. Summary Form: ( DEFUN H ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) H ACL2 !>(h 1/2 1/4) ACL2 Error in TOP-LEVEL: The guard for the function call (H X Y), which is (AND (INTEGERP X) (INTEGERP Y)), is violated by the arguments in the call (H 1/2 1/4). 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 >(h 1/2 1/4) 1/8 ACL2 >(trace$ f h) ((F) (H)) ACL2 >(h 1/2 1/4) 1> (ACL2_*1*_ACL2::H 1/2 1/4) 2> (ACL2_*1*_ACL2::F 1/2 1/4) <2 (ACL2_*1*_ACL2::F 1/8) <1 (ACL2_*1*_ACL2::H 1/8) 1/8 ACL2 >(trace$ g) ((G)) ACL2 >(h 1/2 1/4) 1> (ACL2_*1*_ACL2::H 1/2 1/4) 2> (ACL2_*1*_ACL2::F 1/2 1/4) <2 (ACL2_*1*_ACL2::F 1/8) <1 (ACL2_*1*_ACL2::H 1/8) 1/8 ACL2 >(trace$ f-exec) ((F-EXEC)) ACL2 >(h 1/2 1/4) 1> (ACL2_*1*_ACL2::H 1/2 1/4) 2> (ACL2_*1*_ACL2::F 1/2 1/4) 3> (ACL2_*1*_ACL2::F-EXEC 1/2 1/4) 4> (F-EXEC 1/2 1/4) <4 (F-EXEC 1/8) <3 (ACL2_*1*_ACL2::F-EXEC 1/8) <2 (ACL2_*1*_ACL2::F 1/8) <1 (ACL2_*1*_ACL2::H 1/8) 1/8 ACL2 >:pbt 0 0 (EXIT-BOOT-STRAP-MODE) d 1 (INCLUDE-BOOK "arithmetic-5/top" :DIR ...) 2 (DEFMACRO PRINT-THEORY-SINCE-START NIL ...) 3 (DEFTHEORY START (CURRENT-THEORY :HERE)) 4 (ENCAPSULATE (((F * *) ...) ((G * *) ...)) ...) V 5 (DEFUN F-EXEC (X Y) ...) V 6 (DEFUN G-EXEC (X Y) ...) 7 (DEFATTACH (F F-EXEC) (G G-EXEC)) V 8:x(DEFUN H (X Y) ...) ACL2 >:ubt! 8 7:x(DEFATTACH (F F-EXEC) (G G-EXEC)) ACL2 >(untrace$) (F-EXEC G F) ACL2 >(thm (equal (f 3 4) 12)) Name the formula above *1. No induction schemes are suggested by *1. Consequently, the proof attempt has failed. Summary Form: ( THM ...) Rules: NIL 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: *** Goal (EQUAL (F 3 4) 12) ACL2 Error in ( THM ...): See :DOC failure. ******** FAILED ******** ACL2 >(print-theory-since-start) ((:TYPE-PRESCRIPTION G-EXEC) (:EXECUTABLE-COUNTERPART G-EXEC) (:DEFINITION G-EXEC) (:TYPE-PRESCRIPTION F-EXEC) (:EXECUTABLE-COUNTERPART F-EXEC) (:DEFINITION F-EXEC) (:REWRITE G-DOES-NOT-COMMUTE) (:REWRITE F-COMMUTES)) ACL2 >(ubu! 'start) 3:x(DEFTHEORY START (CURRENT-THEORY :HERE)) ACL2 >(encapsulate (((f * *) => * :formals (x y) :guard (and (integerp x) (integerp y))) ((g * *) => * :formals (x y) :guard (and (integerp x) (integerp y)))) (local (defun f (x y) (declare (xargs :guard (and (integerp x) (integerp y)))) (+ x y))) (local (defun g (x y) (declare (xargs :guard (and (integerp x) (integerp y)))) (- x y))) (defthm f-commutes (implies (and (integerp x) (integerp y)) (equal (f y x) (f x y)))) (defthm g-does-not-commute (implies (and (integerp x) (integerp y) (not (equal x y))) (not (equal (g y x) (g x y))))) ) To verify that the four 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 Y) (DECLARE (XARGS :GUARD (AND (INTEGERP X) (INTEGERP Y)))) (+ X Y))) Since F is non-recursive, its admission is trivial. We observe that the type of F is described by the theorem (ACL2-NUMBERP (F X Y)). We used primitive type reasoning. Computing the guard conjecture for F.... The guard conjecture for F is trivial to prove. F is compliant with Common Lisp. Summary Form: ( DEFUN F ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F ACL2 >>(LOCAL (DEFUN G (X Y) (DECLARE (XARGS :GUARD (AND (INTEGERP X) (INTEGERP Y)))) (- X Y))) Since G is non-recursive, its admission is trivial. We observe that the type of G is described by the theorem (ACL2-NUMBERP (G X Y)). We used primitive type reasoning. Computing the guard conjecture for G.... The guard conjecture for G is trivial to prove, given primitive type reasoning. G is compliant with Common Lisp. Summary Form: ( DEFUN G ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) G ACL2 >>(DEFTHM F-COMMUTES (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F Y X) (F X Y)))) ACL2 Warning [Non-rec] in ( DEFTHM F-COMMUTES ...): A :REWRITE rule generated from F-COMMUTES 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. ACL2 Warning [Subsume] in ( DEFTHM F-COMMUTES ...): The previously added rule F subsumes a newly proposed :REWRITE rule generated from F-COMMUTES, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application. By the simple :definition F we reduce the conjecture to Goal' (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (+ Y X) (+ X Y))). But simplification reduces this to T, using linear arithmetic and primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM F-COMMUTES ...) Rules: ((:DEFINITION F) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: Subsume and Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F-COMMUTES ACL2 >>(DEFTHM G-DOES-NOT-COMMUTE (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G Y X) (G X Y))))) ACL2 Warning [Non-rec] in ( DEFTHM G-DOES-NOT-COMMUTE ...): A :REWRITE rule generated from G-DOES-NOT-COMMUTE will be triggered only by terms containing the non-recursive function symbol G. Unless this function is disabled, this rule is unlikely ever to be used. By the simple :definition G we reduce the conjecture to Goal' (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (+ Y (- X)) (+ X (- Y))))). But simplification reduces this to T, using linear arithmetic and primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM G-DOES-NOT-COMMUTE ...) Rules: ((:DEFINITION G) (:DEFINITION NOT) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) G-DOES-NOT-COMMUTE 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 both of the functions F and G: (AND (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F Y X) (F X Y))) (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G Y X) (G X Y))))) Summary Form: ( ENCAPSULATE (((F * ...) ...) ...) ...) Rules: NIL Warnings: Subsume and Non-rec Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.01) T ACL2 >(defun f-exec (x y) (declare (xargs :guard (and (rationalp x) (rationalp y)))) (+ x y)) Since F-EXEC is non-recursive, its admission is trivial. We observe that the type of F-EXEC is described by the theorem (ACL2-NUMBERP (F-EXEC X Y)). We used primitive type reasoning. Computing the guard conjecture for F-EXEC.... The guard conjecture for F-EXEC is trivial to prove. F-EXEC is compliant with Common Lisp. Summary Form: ( DEFUN F-EXEC ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F-EXEC ACL2 >(defun g-exec (x y) (declare (xargs :guard (and (rationalp x) (rationalp y)))) (- x y)) Since G-EXEC is non-recursive, its admission is trivial. We observe that the type of G-EXEC is described by the theorem (ACL2-NUMBERP (G-EXEC X Y)). We used primitive type reasoning. Computing the guard conjecture for G-EXEC.... The guard conjecture for G-EXEC is trivial to prove, given primitive type reasoning. G-EXEC is compliant with Common Lisp. Summary Form: ( DEFUN G-EXEC ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) G-EXEC ACL2 >(defthm f-exec-commutes (implies (and (integerp x) (integerp y)) (equal (f-exec y x) (f-exec x y)))) ACL2 Warning [Non-rec] in ( DEFTHM F-EXEC-COMMUTES ...): A :REWRITE rule generated from F-EXEC-COMMUTES will be triggered only by terms containing the non-recursive function symbol F-EXEC. Unless this function is disabled, this rule is unlikely ever to be used. ACL2 Warning [Subsume] in ( DEFTHM F-EXEC-COMMUTES ...): The previously added rule F-EXEC subsumes a newly proposed :REWRITE rule generated from F-EXEC-COMMUTES, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application. By the simple :definition F-EXEC we reduce the conjecture to Goal' (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (+ Y X) (+ X Y))). But simplification reduces this to T, using linear arithmetic and primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM F-EXEC-COMMUTES ...) Rules: ((:DEFINITION F-EXEC) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: Subsume and Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F-EXEC-COMMUTES ACL2 >(defthm g-exec-does-not-commute (implies (and (integerp x) (integerp y) (not (equal x y))) (not (equal (g-exec y x) (g-exec x y))))) ACL2 Warning [Non-rec] in ( DEFTHM G-EXEC-DOES-NOT-COMMUTE ...): A :REWRITE rule generated from G-EXEC-DOES-NOT-COMMUTE will be triggered only by terms containing the non-recursive function symbol G-EXEC. Unless this function is disabled, this rule is unlikely ever to be used. By the simple :definition G-EXEC we reduce the conjecture to Goal' (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (+ Y (- X)) (+ X (- Y))))). But simplification reduces this to T, using linear arithmetic and primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM G-EXEC-DOES-NOT-COMMUTE ...) Rules: ((:DEFINITION G-EXEC) (:DEFINITION NOT) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) G-EXEC-DOES-NOT-COMMUTE ACL2 >(defattach (f f-exec) (g g-exec) :hints (("Goal" :use ((:instance f-exec-commutes) (:instance g-exec-does-not-commute))))) We first consider the two guard proof obligations. The first guard proof obligation is (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (AND (RATIONALP X) (RATIONALP Y))). But we reduce the conjecture to T, by case analysis. Q.E.D. The second (and last) guard proof obligation is (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (AND (RATIONALP X) (RATIONALP Y))). 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 (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F-EXEC Y X) (F-EXEC X Y))) (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G-EXEC Y X) (G-EXEC X Y))))). [Note: A hint was supplied for our processing of the goal above. Thanks!] ACL2 Warning [Use] in ( DEFATTACH (F F-EXEC) ...): It is unusual to :USE an enabled :REWRITE or :DEFINITION rule, so you may want to consider disabling (:REWRITE F-EXEC-COMMUTES) and (:REWRITE G-EXEC-DOES-NOT-COMMUTE). We augment the goal with the hypotheses provided by the :USE hint. These hypotheses can be derived from F-EXEC-COMMUTES and G-EXEC-DOES-NOT-COMMUTE via instantiation. We are left with the following subgoal. Goal' (IMPLIES (AND (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F-EXEC Y X) (F-EXEC X Y))) (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G-EXEC Y X) (G-EXEC X Y))))) (AND (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F-EXEC Y X) (F-EXEC X Y))) (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G-EXEC Y X) (G-EXEC X Y)))))). But we reduce the conjecture to T, by case analysis. Q.E.D. Summary Form: ( DEFATTACH (F F-EXEC) ...) Rules: NIL Warnings: Use Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) :ATTACHMENTS-RECORDED ACL2 >(ubu! 'start) 3:x(DEFTHEORY START (CURRENT-THEORY :HERE)) ACL2 >(defun f-exec (x y) (declare (xargs :guard (and (rationalp x) (rationalp y)))) (+ x y)) Since F-EXEC is non-recursive, its admission is trivial. We observe that the type of F-EXEC is described by the theorem (ACL2-NUMBERP (F-EXEC X Y)). We used primitive type reasoning. Computing the guard conjecture for F-EXEC.... The guard conjecture for F-EXEC is trivial to prove. F-EXEC is compliant with Common Lisp. Summary Form: ( DEFUN F-EXEC ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F-EXEC ACL2 >(defun g-exec (x y) (declare (xargs :guard (and (rationalp x) (rationalp y)))) (- x y)) Since G-EXEC is non-recursive, its admission is trivial. We observe that the type of G-EXEC is described by the theorem (ACL2-NUMBERP (G-EXEC X Y)). We used primitive type reasoning. Computing the guard conjecture for G-EXEC.... The guard conjecture for G-EXEC is trivial to prove, given primitive type reasoning. G-EXEC is compliant with Common Lisp. Summary Form: ( DEFUN G-EXEC ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) G-EXEC ACL2 >(defthm f-exec-commutes (implies (and (integerp x) (integerp y)) (equal (f-exec y x) (f-exec x y)))) ACL2 Warning [Non-rec] in ( DEFTHM F-EXEC-COMMUTES ...): A :REWRITE rule generated from F-EXEC-COMMUTES will be triggered only by terms containing the non-recursive function symbol F-EXEC. Unless this function is disabled, this rule is unlikely ever to be used. ACL2 Warning [Subsume] in ( DEFTHM F-EXEC-COMMUTES ...): The previously added rule F-EXEC subsumes a newly proposed :REWRITE rule generated from F-EXEC-COMMUTES, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application. By the simple :definition F-EXEC we reduce the conjecture to Goal' (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (+ Y X) (+ X Y))). But simplification reduces this to T, using linear arithmetic and primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM F-EXEC-COMMUTES ...) Rules: ((:DEFINITION F-EXEC) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: Subsume and Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F-EXEC-COMMUTES ACL2 >(defthm g-exec-does-not-commute (implies (and (integerp x) (integerp y) (not (equal x y))) (not (equal (g-exec y x) (g-exec x y))))) ACL2 Warning [Non-rec] in ( DEFTHM G-EXEC-DOES-NOT-COMMUTE ...): A :REWRITE rule generated from G-EXEC-DOES-NOT-COMMUTE will be triggered only by terms containing the non-recursive function symbol G-EXEC. Unless this function is disabled, this rule is unlikely ever to be used. By the simple :definition G-EXEC we reduce the conjecture to Goal' (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (+ Y (- X)) (+ X (- Y))))). But simplification reduces this to T, using linear arithmetic and primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM G-EXEC-DOES-NOT-COMMUTE ...) Rules: ((:DEFINITION G-EXEC) (:DEFINITION NOT) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) G-EXEC-DOES-NOT-COMMUTE ACL2 >(defthm defattach-proof (and (implies (and (integerp x) (integerp y)) (equal (f-exec y x) (f-exec x y))) (implies (and (integerp x) (integerp y) (not (equal x y))) (not (equal (g-exec y x) (g-exec x y))))) :hints (("Goal" :in-theory (disable f-exec g-exec)) ("Subgoal 2" :by (:instance f-exec-commutes)) ("Subgoal 1" :by (:instance g-exec-does-not-commute)))) ACL2 Warning [Non-rec] in ( DEFTHM DEFATTACH-PROOF ...): A :REWRITE rule generated from DEFATTACH-PROOF will be triggered only by terms containing the non-recursive function symbol F-EXEC. Unless this function is disabled, this rule is unlikely ever to be used. ACL2 Warning [Subsume] in ( DEFTHM DEFATTACH-PROOF ...): A newly proposed :REWRITE rule generated from DEFATTACH-PROOF probably subsumes the previously added :REWRITE rule F-EXEC-COMMUTES, in the sense that the new rule will now probably be applied whenever the old rule would have been. ACL2 Warning [Subsume] in ( DEFTHM DEFATTACH-PROOF ...): The previously added rules F-EXEC-COMMUTES and F-EXEC subsume a newly proposed :REWRITE rule generated from DEFATTACH-PROOF, in the sense that the old rules rewrite more general targets. Because the new rule will be tried first, it may nonetheless find application. ACL2 Warning [Non-rec] in ( DEFTHM DEFATTACH-PROOF ...): A :REWRITE rule generated from DEFATTACH-PROOF will be triggered only by terms containing the non-recursive function symbol G-EXEC. Unless this function is disabled, this rule is unlikely ever to be used. ACL2 Warning [Subsume] in ( DEFTHM DEFATTACH-PROOF ...): A newly proposed :REWRITE rule generated from DEFATTACH-PROOF probably subsumes the previously added :REWRITE rule G-EXEC-DOES-NOT-COMMUTE, in the sense that the new rule will now probably be applied whenever the old rule would have been. ACL2 Warning [Subsume] in ( DEFTHM DEFATTACH-PROOF ...): The previously added rule G-EXEC-DOES-NOT-COMMUTE subsumes a newly proposed :REWRITE rule generated from DEFATTACH-PROOF, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application. [Note: A hint was supplied for our processing of the goal above. Thanks!] By case analysis we reduce the conjecture to the following two conjectures. [Note: A hint was supplied for our processing of the goal below. Thanks!] Subgoal 2 (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F-EXEC Y X) (F-EXEC X Y))). But, as indicated by the hint, this goal is subsumed by (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F-EXEC Y X) (F-EXEC X Y))), which can be derived from F-EXEC-COMMUTES via instantiation. [Note: A hint was supplied for our processing of the goal below. Thanks!] Subgoal 1 (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G-EXEC Y X) (G-EXEC X Y)))). But, as indicated by the hint, this goal is subsumed by (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G-EXEC Y X) (G-EXEC X Y)))), which can be derived from G-EXEC-DOES-NOT-COMMUTE via instantiation. Q.E.D. Summary Form: ( DEFTHM DEFATTACH-PROOF ...) Rules: ((:DEFINITION NOT)) Warnings: Subsume and Non-rec Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02) DEFATTACH-PROOF ACL2 >(encapsulate (((f * *) => * :formals (x y) :guard (and (integerp x) (integerp y))) ((g * *) => * :formals (x y) :guard (and (integerp x) (integerp y)))) (local (defun f (x y) (declare (xargs :guard (and (integerp x) (integerp y)))) (f-exec x y))) (local (defun g (x y) (declare (xargs :guard (and (integerp x) (integerp y)))) (g-exec x y))) ; more changes for matt's second suggestion (defthm f-commutes (implies (and (integerp x) (integerp y)) (equal (f y x) (f x y))) :hints (("Goal" :in-theory (disable f-exec)) ("Goal'" :by (:instance f-exec-commutes)))) (defthm g-does-not-commute (implies (and (integerp x) (integerp y) (not (equal x y))) (not (equal (g y x) (g x y)))) :hints (("Goal" :in-theory (disable g-exec)) ("Goal'" :by (:instance g-exec-does-not-commute)))) ) To verify that the four 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 Y) (DECLARE (XARGS :GUARD (AND (INTEGERP X) (INTEGERP Y)))) (F-EXEC X Y))) Since F is non-recursive, its admission is trivial. We observe that the type of F is described by the theorem (ACL2-NUMBERP (F X Y)). We used the :type-prescription rule F-EXEC. Computing the guard conjecture for F.... The guard conjecture for F is trivial to prove. F is compliant with Common Lisp. Summary Form: ( DEFUN F ...) Rules: ((:TYPE-PRESCRIPTION F-EXEC)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F ACL2 >>(LOCAL (DEFUN G (X Y) (DECLARE (XARGS :GUARD (AND (INTEGERP X) (INTEGERP Y)))) (G-EXEC X Y))) Since G is non-recursive, its admission is trivial. We observe that the type of G is described by the theorem (ACL2-NUMBERP (G X Y)). We used the :type-prescription rule G-EXEC. 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: ((:TYPE-PRESCRIPTION G-EXEC)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) G ACL2 >>(DEFTHM F-COMMUTES (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F Y X) (F X Y))) :HINTS (("Goal" :IN-THEORY (DISABLE F-EXEC)) ("Goal'" :BY (:INSTANCE F-EXEC-COMMUTES)))) ACL2 Warning [Non-rec] in ( DEFTHM F-COMMUTES ...): A :REWRITE rule generated from F-COMMUTES 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. ACL2 Warning [Subsume] in ( DEFTHM F-COMMUTES ...): The previously added rule F subsumes a newly proposed :REWRITE rule generated from F-COMMUTES, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application. [Note: A hint was supplied for our processing of the goal above. Thanks!] By the simple :definition F we reduce the conjecture to [Note: A hint was supplied for our processing of the goal below. Thanks!] Goal' (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F-EXEC Y X) (F-EXEC X Y))). But, as indicated by the hint, this goal is subsumed by (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F-EXEC Y X) (F-EXEC X Y))), which can be derived from F-EXEC-COMMUTES via instantiation. Q.E.D. Summary Form: ( DEFTHM F-COMMUTES ...) Rules: ((:DEFINITION F)) Warnings: Subsume and Non-rec Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) F-COMMUTES ACL2 >>(DEFTHM G-DOES-NOT-COMMUTE (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G Y X) (G X Y)))) :HINTS (("Goal" :IN-THEORY (DISABLE G-EXEC)) ("Goal'" :BY (:INSTANCE G-EXEC-DOES-NOT-COMMUTE)))) ACL2 Warning [Non-rec] in ( DEFTHM G-DOES-NOT-COMMUTE ...): A :REWRITE rule generated from G-DOES-NOT-COMMUTE will be triggered only by terms containing the non-recursive function symbol G. Unless this function is disabled, this rule is unlikely ever to be used. [Note: A hint was supplied for our processing of the goal above. Thanks!] By the simple :definition G we reduce the conjecture to [Note: A hint was supplied for our processing of the goal below. Thanks!] Goal' (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G-EXEC Y X) (G-EXEC X Y)))). But, as indicated by the hint, this goal is subsumed by (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G-EXEC Y X) (G-EXEC X Y)))), which can be derived from G-EXEC-DOES-NOT-COMMUTE via instantiation. Q.E.D. Summary Form: ( DEFTHM G-DOES-NOT-COMMUTE ...) Rules: ((:DEFINITION G) (:DEFINITION NOT)) Warnings: Non-rec Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01) G-DOES-NOT-COMMUTE 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 both of the functions F and G: (AND (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F Y X) (F X Y))) (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G Y X) (G X Y))))) Summary Form: ( ENCAPSULATE (((F * ...) ...) ...) ...) Rules: NIL Warnings: Subsume and Non-rec Time: 0.03 seconds (prove: 0.01, print: 0.00, other: 0.02) T ACL2 >(defattach (f f-exec) (g g-exec) :hints (("Goal" :by (:instance defattach-proof)))) We first consider the two guard proof obligations. The first guard proof obligation is (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (AND (RATIONALP X) (RATIONALP Y))). But we reduce the conjecture to T, by case analysis. Q.E.D. The second (and last) guard proof obligation is (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (AND (RATIONALP X) (RATIONALP Y))). 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 (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F-EXEC Y X) (F-EXEC X Y))) (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G-EXEC Y X) (G-EXEC X Y))))). [Note: A hint was supplied for our processing of the goal above. Thanks!] But, as indicated by the hint, this goal is subsumed by (AND (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F-EXEC Y X) (F-EXEC X Y))) (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G-EXEC Y X) (G-EXEC X Y))))), which can be derived from DEFATTACH-PROOF via instantiation. Q.E.D. Summary Form: ( DEFATTACH (F F-EXEC) ...) Rules: NIL Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) :ATTACHMENTS-RECORDED ACL2 >(ubu! 'start) 3:x(DEFTHEORY START (CURRENT-THEORY :HERE)) ACL2 >(defun f-exec (x y) (declare (xargs :guard (and (rationalp x) (rationalp y)))) (+ x y)) Since F-EXEC is non-recursive, its admission is trivial. We observe that the type of F-EXEC is described by the theorem (ACL2-NUMBERP (F-EXEC X Y)). We used primitive type reasoning. Computing the guard conjecture for F-EXEC.... The guard conjecture for F-EXEC is trivial to prove. F-EXEC is compliant with Common Lisp. Summary Form: ( DEFUN F-EXEC ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F-EXEC ACL2 >(defun g-exec (x y) (declare (xargs :guard (and (rationalp x) (rationalp y)))) (- x y)) Since G-EXEC is non-recursive, its admission is trivial. We observe that the type of G-EXEC is described by the theorem (ACL2-NUMBERP (G-EXEC X Y)). We used primitive type reasoning. Computing the guard conjecture for G-EXEC.... The guard conjecture for G-EXEC is trivial to prove, given primitive type reasoning. G-EXEC is compliant with Common Lisp. Summary Form: ( DEFUN G-EXEC ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) G-EXEC ACL2 >(encapsulate (((f * *) => * :formals (x y) :guard (and (integerp x) (integerp y))) ((g * *) => * :formals (x y) :guard (and (integerp x) (integerp y)))) (local (defun f (x y) (declare (xargs :guard (and (integerp x) (integerp y)))) (+ x y))) (local (defun g (x y) (declare (xargs :guard (and (integerp x) (integerp y)))) (- x y))) (defun h (x y) (f x y)) ; need this theorem for defattach proof ;; (defthm h-exec ;; (equal (h x y) ;; (f-exec x y))) (defthm f-commutes (implies (and (integerp x) (integerp y)) (equal (f y x) (f x y)))) (defthm g-does-not-commute (implies (and (integerp x) (integerp y) (not (equal x y))) (not (equal (g y x) (g x y))))) (defthm h-commutes (implies (and (integerp x) (integerp y)) (equal (h y x) (h x y)))) ) To verify that the six 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 Y) (DECLARE (XARGS :GUARD (AND (INTEGERP X) (INTEGERP Y)))) (+ X Y))) Since F is non-recursive, its admission is trivial. We observe that the type of F is described by the theorem (ACL2-NUMBERP (F X Y)). We used primitive type reasoning. Computing the guard conjecture for F.... The guard conjecture for F is trivial to prove. F is compliant with Common Lisp. Summary Form: ( DEFUN F ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F ACL2 >>(LOCAL (DEFUN G (X Y) (DECLARE (XARGS :GUARD (AND (INTEGERP X) (INTEGERP Y)))) (- X Y))) Since G is non-recursive, its admission is trivial. We observe that the type of G is described by the theorem (ACL2-NUMBERP (G X Y)). We used primitive type reasoning. Computing the guard conjecture for G.... The guard conjecture for G is trivial to prove, given primitive type reasoning. G is compliant with Common Lisp. Summary Form: ( DEFUN G ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) G ACL2 >>(DEFUN H (X Y) (F X Y)) Since H is non-recursive, its admission is trivial. We observe that the type of H is described by the theorem (ACL2-NUMBERP (H X Y)). We used the :type-prescription rule F. Summary Form: ( DEFUN H ...) Rules: ((:TYPE-PRESCRIPTION F)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) H ACL2 >>(DEFTHM F-COMMUTES (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F Y X) (F X Y)))) ACL2 Warning [Non-rec] in ( DEFTHM F-COMMUTES ...): A :REWRITE rule generated from F-COMMUTES 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. ACL2 Warning [Subsume] in ( DEFTHM F-COMMUTES ...): The previously added rule F subsumes a newly proposed :REWRITE rule generated from F-COMMUTES, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application. By the simple :definition F we reduce the conjecture to Goal' (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (+ Y X) (+ X Y))). But simplification reduces this to T, using linear arithmetic and primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM F-COMMUTES ...) Rules: ((:DEFINITION F) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: Subsume and Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) F-COMMUTES ACL2 >>(DEFTHM G-DOES-NOT-COMMUTE (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G Y X) (G X Y))))) ACL2 Warning [Non-rec] in ( DEFTHM G-DOES-NOT-COMMUTE ...): A :REWRITE rule generated from G-DOES-NOT-COMMUTE will be triggered only by terms containing the non-recursive function symbol G. Unless this function is disabled, this rule is unlikely ever to be used. By the simple :definition G we reduce the conjecture to Goal' (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (+ Y (- X)) (+ X (- Y))))). But simplification reduces this to T, using linear arithmetic and primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM G-DOES-NOT-COMMUTE ...) Rules: ((:DEFINITION G) (:DEFINITION NOT) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) G-DOES-NOT-COMMUTE ACL2 >>(DEFTHM H-COMMUTES (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (H Y X) (H X Y)))) ACL2 Warning [Non-rec] in ( DEFTHM H-COMMUTES ...): A :REWRITE rule generated from H-COMMUTES will be triggered only by terms containing the non-recursive function symbol H. Unless this function is disabled, this rule is unlikely ever to be used. ACL2 Warning [Subsume] in ( DEFTHM H-COMMUTES ...): The previously added rule H subsumes a newly proposed :REWRITE rule generated from H-COMMUTES, in the sense that the old rule rewrites a more general target. Because the new rule will be tried first, it may nonetheless find application. By the simple :definitions F and H we reduce the conjecture to Goal' (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (+ Y X) (+ X Y))). But simplification reduces this to T, using linear arithmetic and primitive type reasoning. Q.E.D. Summary Form: ( DEFTHM H-COMMUTES ...) Rules: ((:DEFINITION F) (:DEFINITION H) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: Subsume and Non-rec Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) H-COMMUTES 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. In addition to F and G, we export H. The following constraint is associated with every one of the functions H, F and G: (AND (EQUAL (H X Y) (F X Y)) (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F Y X) (F X Y))) (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G Y X) (G X Y)))) (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (H Y X) (H X Y)))) ACL2 Warning [Infected] in ( ENCAPSULATE (((F * ...) ...) ...) ...): Note that the definitional equation for H infects the constraint of this encapsulation. That can be caused either because we are not allowed to move a defun out of nested non-trivial encapsulates or because a function ancestrally involves the constrained functions of an encapsulate and is ancestrally involved in the constraining theorems of those functions. In any case, if at all possible, you should move this definition out of the encapsulation. A constraint containing a definitional equation is often hard to use in subsequent functional instantiations. See :DOC subversive-recursions for a discussion of related issues. Summary Form: ( ENCAPSULATE (((F * ...) ...) ...) ...) Rules: NIL Warnings: Infected, Subsume and Non-rec Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.02) T ACL2 >(defattach (f f-exec) (g g-exec)) We first consider the two guard proof obligations. The first guard proof obligation is (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (AND (RATIONALP X) (RATIONALP Y))). But we reduce the conjecture to T, by case analysis. Q.E.D. The second (and last) guard proof obligation is (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (AND (RATIONALP X) (RATIONALP Y))). 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 (EQUAL (H X Y) (F-EXEC X Y)) (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F-EXEC Y X) (F-EXEC X Y))) (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G-EXEC Y X) (G-EXEC X Y)))) (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (H Y X) (H X Y)))). By the simple :definitions F-EXEC, G-EXEC and H we reduce the conjecture to the following four conjectures. Subgoal 4 (EQUAL (F X Y) (+ X Y)). This simplifies, using the :definition SYNP and the :rewrite rules |(equal (if a b c) x)|, DEFAULT-PLUS-1 and DEFAULT-PLUS-2, to the following four conjectures. Subgoal 4.4 (IMPLIES (AND (ACL2-NUMBERP Y) (ACL2-NUMBERP X)) (EQUAL (+ X Y) (F X Y))). Name the formula above *1. Subgoal 4.3 (IMPLIES (AND (NOT (ACL2-NUMBERP Y)) (ACL2-NUMBERP X)) (EQUAL X (F X Y))). Normally we would attempt to prove Subgoal 4.3 by induction. However, we prefer in this instance to focus on the original input conjecture rather than this simplified special case. We therefore abandon our previous work on this conjecture and reassign the name *1 to the original conjecture. (See :DOC otf-flg.) No induction schemes are suggested by *1. Consequently, the proof attempt has failed. Summary Form: ( DEFATTACH (F F-EXEC) ...) Rules: ((:DEFINITION F-EXEC) (:DEFINITION G-EXEC) (:DEFINITION H) (:DEFINITION NOT) (:DEFINITION SYNP) (:REWRITE |(equal (if a b c) x)|) (:REWRITE DEFAULT-PLUS-1) (:REWRITE DEFAULT-PLUS-2)) Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.00) --- The key checkpoint goals, below, may help you to debug this failure. See :DOC failure and see :DOC set-checkpoint-summary-limit. --- *** Key checkpoints before reverting to proof by induction: *** Subgoal 4.4 (IMPLIES (AND (ACL2-NUMBERP Y) (ACL2-NUMBERP X)) (EQUAL (+ X Y) (F X Y))) Subgoal 4.3 (IMPLIES (AND (NOT (ACL2-NUMBERP Y)) (ACL2-NUMBERP X)) (EQUAL X (F X Y))) ACL2 Error in ( DEFATTACH (F F-EXEC) ...): See :DOC failure. ******** FAILED ******** ACL2 >(defattach (f f-exec) (g g-exec) (h f-exec :attach nil)) We first consider the two guard proof obligations. The first guard proof obligation is (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (AND (RATIONALP X) (RATIONALP Y))). But we reduce the conjecture to T, by case analysis. Q.E.D. The second (and last) guard proof obligation is (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (AND (RATIONALP X) (RATIONALP Y))). 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 (EQUAL (F-EXEC X Y) (F-EXEC X Y)) (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F-EXEC Y X) (F-EXEC X Y))) (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (G-EXEC Y X) (G-EXEC X Y)))) (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (F-EXEC Y X) (F-EXEC X Y)))). By the simple :definitions F-EXEC and G-EXEC we reduce the conjecture to the following two conjectures. Subgoal 2 (IMPLIES (AND (INTEGERP X) (INTEGERP Y)) (EQUAL (+ Y X) (+ X Y))). But simplification reduces this to T, using linear arithmetic and primitive type reasoning. Subgoal 1 (IMPLIES (AND (INTEGERP X) (INTEGERP Y) (NOT (EQUAL X Y))) (NOT (EQUAL (+ Y (- X)) (+ X (- Y))))). But simplification reduces this to T, using linear arithmetic and primitive type reasoning. Q.E.D. Summary Form: ( DEFATTACH (F F-EXEC) ...) Rules: ((:DEFINITION F-EXEC) (:DEFINITION G-EXEC) (:DEFINITION NOT) (:FAKE-RUNE-FOR-LINEAR NIL) (:FAKE-RUNE-FOR-TYPE-SET NIL)) Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00) :ATTACHMENTS-RECORDED ACL2 >