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 >