[acl2-books] r478 committed - Updates for recent changes in clausification/subsumption and forward-c...
acl2-...@googlecode.com
Author: kauf...@cs.utexas.edu
Date: Mon Apr 12 21:30:46 2010
Log: Updates for recent changes in clausification/subsumption and
forward-chaining.
http://code.google.com/p/acl2-books/source/detail?r=478
Modified:
/trunk/arithmetic-2/meta/common-meta.lisp
/trunk/concurrent-programs/bakery/inv-persists.lisp
/trunk/proofstyles/completeness/clock-partial.lisp
/trunk/rtl/rel7/support/lib1.delta1/round-extra2.lisp
/trunk/rtl/rel8/support/lib1.delta1/round-extra2.lisp
/trunk/workshops/1999/embedded/Proof-Of-Contribution/Proof-Of-Correctness-OneCycle.lisp
/trunk/workshops/1999/ivy/ivy-v2/ivy-sources/derive.lisp
/trunk/workshops/2002/cowles-flat/support/flat-ackermann.lisp
/trunk/workshops/2004/schmaltz-borrione/support/local_trip_book.lisp
/trunk/workshops/2007/cowles-et-al/support/cowles/while-loop.lisp
=======================================
--- /trunk/arithmetic-2/meta/common-meta.lisp Thu Dec 6 11:36:07 2007
+++ /trunk/arithmetic-2/meta/common-meta.lisp Mon Apr 12 21:30:46 2010
@@ -865,9 +865,10 @@
(equal (eva new-term a)
(eva `(,bin-op ,new-piece ,term) a)))
:hints (("Goal" :in-theory (disable pull-piece-out))
- ("Subgoal 6''" :use ((:instance pull-piece-up-correct
+;fcd/Satriani v3.7 Moore - used to be Subgoals 6'' and 5''
+ ("Subgoal 7''" :use ((:instance pull-piece-up-correct
(bin-op 'BINARY-+))))
- ("Subgoal 5''" :use ((:instance pull-piece-up-correct
+ ("Subgoal 3''" :use ((:instance pull-piece-up-correct
(bin-op 'BINARY-*)))))))
; This is the only theorem we export.
=======================================
--- /trunk/concurrent-programs/bakery/inv-persists.lisp Thu Dec 6 11:36:07
2007
+++ /trunk/concurrent-programs/bakery/inv-persists.lisp Mon Apr 12 21:30:46
2010
@@ -669,7 +669,8 @@
(lexicographic-temp (-> procs in (bake+-p (<- procs in) in procs
max))
(bake+-q (<- procs in) queue bucket max)))
- :hints (("Subgoal 17"
+; fcd/Satriani v3.7 Moore - used to be Subgoal 17
+ :hints (("Subgoal 14"
:in-theory (disable lexicographic-temp-if-something-else-set)
:use ((:instance lexicographic-temp-if-something-else-set
(p (s :loc 4 (s :status 'wait (g in procs))))
@@ -804,12 +805,15 @@
(bake+-max (<- procs in) max)))
:hints (("Goal"
:do-not-induct t)
- ("Subgoal 8"
+; fcd/Satriani v3.7 Moore - used to be Subgoal 8
+ ("Subgoal 7"
:cases ((equal in (current (<- procs in)))))
- ("Subgoal 4"
+; fcd/Satriani v3.7 Moore - used to be Subgoal 4
+ ("Subgoal 6"
:use ((:instance choosing-pos-pos-reduction
(curr (current (<- procs in))))))
- ("Subgoal 2"
+; fcd/Satriani v3.7 Moore - used to be Subgoal 2
+ ("Subgoal 4"
:use ((:instance choosing-pos-pos-reduction
(curr (current (<- procs in))))
(:instance lexicographic-pos-lex<-reduction
=======================================
--- /trunk/proofstyles/completeness/clock-partial.lisp Thu Feb 21 18:22:19
2008
+++ /trunk/proofstyles/completeness/clock-partial.lisp Mon Apr 12 21:30:46
2010
@@ -49,7 +49,9 @@
(defthm clock-fn-is-natp
(implies (exitpoint (run-fn s k))
(natp (clock-fn s)))
- :rule-classes (:rewrite :forward-chaining :type-prescription)
+ :rule-classes (:rewrite
+ ; :forward-chaining ;fcd/Satriani v3.7 Moore
+ :type-prescription)
:hints (("Goal"
:use ((:instance clock-fn-tail-inv
(steps 0))))))
=======================================
--- /trunk/rtl/rel7/support/lib1.delta1/round-extra2.lisp Thu Dec 6
11:36:07 2007
+++ /trunk/rtl/rel7/support/lib1.delta1/round-extra2.lisp Mon Apr 12
21:30:46 2010
@@ -5102,7 +5102,8 @@
(common-rounding-mode-p mode))
(>= a (drnd x mode p q)))
:hints (("Goal" :in-theory (enable sgn drnd rnd))
- ("Subgoal 5"
+;fcd/Satriani v3.7 Moore - used to be Subgoal 5
+ ("Subgoal 4"
:use ((:instance near-choice
(x x)
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))))
@@ -5202,12 +5203,13 @@
(common-rounding-mode-p mode))
(<= a (drnd x mode p q)))
:hints (("Goal" :in-theory (enable ieee-mode-p drnd rnd))
- ("Subgoal 2"
- :use ((:instance near+-choice
+; fcd/Satriani v3.7 Moore - used to be Subgoal 1
+ ("Subgoal 4"
+ :use ((:instance near-choice
(x x)
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))))
- ("Subgoal 1"
- :use ((:instance near-choice
+ ("Subgoal 2"
+ :use ((:instance near+-choice
(x x)
(n (+ P (EXPO X) (* -1 (EXPO (SPN
Q))))))))))
=======================================
--- /trunk/rtl/rel8/support/lib1.delta1/round-extra2.lisp Fri Feb 27
14:08:30 2009
+++ /trunk/rtl/rel8/support/lib1.delta1/round-extra2.lisp Mon Apr 12
21:30:46 2010
@@ -5102,7 +5102,8 @@
(common-rounding-mode-p mode))
(>= a (drnd x mode p q)))
:hints (("Goal" :in-theory (enable sgn drnd rnd))
- ("Subgoal 5"
+;fcd/Satriani v3.7 Moore - used to be Subgoal 5
+ ("Subgoal 4"
:use ((:instance near-choice
(x x)
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))))
@@ -5202,12 +5203,13 @@
(common-rounding-mode-p mode))
(<= a (drnd x mode p q)))
:hints (("Goal" :in-theory (enable ieee-mode-p drnd rnd))
- ("Subgoal 2"
- :use ((:instance near+-choice
+; fcd/Satriani v3.7 Moore - used to be Subgoal 1
+ ("Subgoal 4"
+ :use ((:instance near-choice
(x x)
(n (+ P (EXPO X) (* -1 (EXPO (SPN Q))))))))
- ("Subgoal 1"
- :use ((:instance near-choice
+ ("Subgoal 2"
+ :use ((:instance near+-choice
(x x)
(n (+ P (EXPO X) (* -1 (EXPO (SPN
Q))))))))))
=======================================
---
/trunk/workshops/1999/embedded/Proof-Of-Contribution/Proof-Of-Correctness-OneCycle.lisp
Fri Nov 14 11:53:05 2008
+++
/trunk/workshops/1999/embedded/Proof-Of-Contribution/Proof-Of-Correctness-OneCycle.lisp
Mon Apr 12 21:30:46 2010
@@ -6897,8 +6897,10 @@
(build-values-by-rns (var-value gcell2) *rns*)))
:hints (("Goal" :in-theory (enable my-or-2))
("Subgoal 5'''" :use (:instance goal15 (var-value-gcell2 (var-value
gcell2))))
- ("Subgoal 4.1" :use subgoal41)
- ("Subgoal 2.1" :use subgoal21)))
+; fcd/Satriani v3.7 Moore - used to Subgoal 4.1
+ ("Subgoal 1.1" :use subgoal41)
+; fcd/Satriani v3.7 Moore - used to Subgoal 2.1
+ ("Subgoal 3.1" :use subgoal21)))
=======================================
--- /trunk/workshops/1999/ivy/ivy-v2/ivy-sources/derive.lisp Sun Dec 16
16:23:46 2007
+++ /trunk/workshops/1999/ivy/ivy-v2/ivy-sources/derive.lisp Mon Apr 12
21:30:46 2010
@@ -371,13 +371,16 @@
; Subgoal numbers changed by Matt K. for v2-9 (probably caused by
call-stack
; change)
- ("Subgoal 20"
+; fcd/Satriani v3.7 Moore - used to be Subgoal 20
+ ("Subgoal 12"
:use ((:instance resolve-step-xsound)))
("Subgoal 16"
:use ((:instance flip-step-xsound)))
- ("Subgoal 14"
+; fcd/Satriani v3.7 Moore - used to be Subgoal 14
+ ("Subgoal 8"
:use ((:instance instantiate-step-xsound)))
- ("Subgoal 10"
+; fcd/Satriani v3.7 Moore - used to be Subgoal 10
+ ("Subgoal 20"
:use ((:instance propositional-step-xsound)))
("Subgoal 4"
:use ((:instance paramod-step-xsound)))
=======================================
--- /trunk/workshops/2002/cowles-flat/support/flat-ackermann.lisp Sun Dec
16 16:23:46 2007
+++ /trunk/workshops/2002/cowles-flat/support/flat-ackermann.lisp Mon Apr
12 21:30:46 2010
@@ -328,12 +328,14 @@
(>= i 0))
(<def= (g1-chain i x)
(ub-g1-chain x)))
- :hints (("Subgoal 8"
+; fcd/Satriani v3.7 Moore - used to be Subgoal 8
+ :hints (("Subgoal 2"
:in-theory (disable lub-f1-chain-is-upper-bound)
:use (:instance
lub-f1-chain-is-upper-bound
(x (list (- (car x) 1) 1))))
- ("Subgoal 3"
+; fcd/Satriani v3.7 Moore - used to be Subgoal 3
+ ("Subgoal 6"
:in-theory (disable lub-f1-chain-is-upper-bound)
:use ((:instance
lub-f1-chain-is-upper-bound
=======================================
--- /trunk/workshops/2004/schmaltz-borrione/support/local_trip_book.lisp
Mon Feb 8 23:04:25 2010
+++ /trunk/workshops/2004/schmaltz-borrione/support/local_trip_book.lisp
Mon Apr 12 21:30:46 2010
@@ -760,10 +760,11 @@
:do-not '(eliminate-destructors generalize fertilize))
; Subgoal hints modified by Matt K. after ACL2 Version 3.6.1 for changes in
; too-many-ifs heuristic. The first of these is just for backward
-; compatibility; the second is for the new ACL2.
+; compatibility and is irrelevant in modern proofs; the second is for the
new ACL2.
("Subgoal 25"
:expand (availablemovep route_triple n))
- ("Subgoal 2.26"
+; fcd/Satriani v3.7 Moore - used to be Subgoal 2.26
+ ("Subgoal 2.22"
:expand (all_intp route_triple))))
=======================================
--- /trunk/workshops/2007/cowles-et-al/support/cowles/while-loop.lisp Sun
Dec 16 16:23:46 2007
+++ /trunk/workshops/2007/cowles-et-al/support/cowles/while-loop.lisp Mon
Apr 12 21:30:46 2010
@@ -1404,11 +1404,15 @@
:rule-classes nil
:hints (("Goal"
:in-theory (disable (:definition nfix)))
- ("Subgoal 6"
+; fcd/Satriani v3.7 Moore - used to be Subgoal 6
+ ("Subgoal 7"
:use Subgoal-6-lemma)
- ("Subgoal 5"
- :use Subgoal-5-lemma)
+; fcd/Satriani v3.7 Moore - used to be Subgoal 5
("Subgoal 4"
- :use Subgoal-4-lemma)
+ :use Subgoal-5-lemma)
+; fcd/Satriani v3.7 Moore - used to be Subgoal 4
("Subgoal 3"
+ :use Subgoal-4-lemma)
+; fcd/Satriani v3.7 Moore - used to be Subgoal 3
+ ("Subgoal 2"
:use Subgoal-3-lemma)))