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