diff options
Diffstat (limited to 'books/workshops/1999/ste/fundamental.lisp')
| -rw-r--r-- | books/workshops/1999/ste/fundamental.lisp | 259 |
1 files changed, 259 insertions, 0 deletions
diff --git a/books/workshops/1999/ste/fundamental.lisp b/books/workshops/1999/ste/fundamental.lisp new file mode 100644 index 0000000..971b7d2 --- /dev/null +++ b/books/workshops/1999/ste/fundamental.lisp @@ -0,0 +1,259 @@ +(in-package "ACL2") + +(include-book "lemma-4") + +(defun-sk ste-thm (ckt a c) + (forall r (implies (and (r-p r) + (t-p r ckt) + (r-nmp r (l-depth a) (l-maxn a)) + + (equal (l-depth a) (l-depth c)) + (equal (l-maxn a) (l-maxn c)) + + (equal (len ckt) (l-maxn a)) + + (l-eval a r) + ) + (l-eval c r)))) + +(defthm ste-thm-backward + (implies (and (l-p a) + (l-p c) + (c-p ckt) + + (r-lte (l-defseq c (l-depth c) (l-maxn c)) + (l-deftraj a ckt)) + ) + (ste-thm ckt a c)) + :hints (("Goal'" + :use ((:instance lemma-2-pre + (l c) + (r (STE-THM-WITNESS CKT A C)) + (n (L-DEPTH A)) + (m (L-MAXN A)) + ) + (:instance r-lte-transitive + (a (L-DEFSEQ C (L-DEPTH A) (L-MAXN A))) + (b (R-DEFTRAJ (L-DEFSEQ A (L-DEPTH A) (L-MAXN A)) + CKT (S-MAKE (L-MAXN A) 'X))) + (c (STE-THM-WITNESS CKT A C)) + )) ) ) ) + + +(defthm r-nmp-l-defseq + (IMPLIES (AND (L-P A) + ;(C-P CKT) + ) + (R-NMP (L-DEFSEQ A (l-depth a) (l-maxn a)) + (l-depth a) + (l-maxn a))) + ) + +(defthm r-nmp-l-defseq-nils + (implies (and (l-p a) + (equal (l-maxn a) 0) + ) + (R-NMP (L-DEFSEQ A (L-DEPTH A) 0) + (L-DEPTH A) + 0)) + :hints (("Goal" + :use ((:instance r-nmp-l-defseq)))) + ) + +(defthm r-nmp-r-deftraj + (IMPLIES (AND (L-P A) + (C-P CKT) + (equal (len ckt) m) + + (r-p r) + (r-nmp r n m) + (positivep n) + (naturalp m) + (s-p s) + (equal (len s) m) + ) + (R-NMP (R-DEFTRAJ r CKT s) + n + m) ) ) + + +(defthm r-nmp-r-deftraj-nils + (implies (and + (l-p a) + (equal (l-maxn a) 0) + ;(equal ckt nil) + ;(equal s nil) + ;(equal m 0) + ) + (R-NMP (R-DEFTRAJ (L-DEFSEQ A (L-DEPTH A) 0) + NIL NIL) + (L-DEPTH A) + 0)) + :hints (("Goal" + :do-not-induct t + :in-theory (disable r-nmp-r-deftraj) + :use ((:instance r-nmp-r-deftraj + (a a) + (ckt nil) + (m 0) + (r (L-DEFSEQ A (L-DEPTH A) 0)) + (n (l-depth a)) + (s nil) + )))) + ) + + +(defthm r-nmp-r-deftraj-ldefseq + (implies (and + (l-p a) + (c-p ckt) + (equal (len ckt) (l-maxn a)) + ) + (R-NMP (R-DEFTRAJ (L-DEFSEQ A (L-DEPTH A) (L-MAXN A)) + CKT (S-MAKE (L-MAXN A) 'X)) + (L-DEPTH A) + (L-MAXN A)) + ) + :hints (("Goal" + :use ((:instance r-nmp-r-deftraj + (r (L-DEFSEQ A (L-DEPTH A) (L-MAXN A))) + (n (L-DEPTH A)) + (m (L-MAXN A)) + (ckt ckt) + (s (S-MAKE (L-MAXN A) 'X)) + )) + )) + ) + + + + + + + +(defthm ste-thm-forward + (implies (and (l-p a) + (l-p c) + (c-p ckt) + + (equal (l-depth a) (l-depth c)) + (equal (l-maxn a) (l-maxn c)) + + (equal (len ckt) (l-maxn a)) + + (ste-thm ckt a c) + ) + (r-lte (l-defseq c (l-depth c) (l-maxn c)) + (l-deftraj a ckt))) + :hints (("Goal" + :do-not '(generalize fertilize) + :in-theory (disable ste-thm lemma-2-pre + lemma-4-1 + lemma-4-2 + lemma-4-3 lemma-4-3-backward lemma-4-3-forward + l-evalp-when-n-l-depth-and-l-maxn) + :use ( + (:instance ste-thm-necc + (r (R-DEFTRAJ (L-DEFSEQ A (L-DEPTH A) (L-MAXN A)) + CKT (S-MAKE (L-MAXN A) 'X)))) + (:instance lemma-4-1 + (l a) + (c ckt)) + (:instance lemma-4-2 + (l a) + (c ckt)) + ) + ) + ("Subgoal 5" + :use ((:instance l-evalp-when-n-l-depth-and-l-maxn + (l c) + ) + (:instance lemma-2-pre + (l c) + (n (l-depth a)) + (m 0) + (r (R-DEFTRAJ (L-DEFSEQ A (L-DEPTH A) 0) + NIL NIL))))) + ("Subgoal 2" + :use ( + (:instance l-evalp-when-n-l-depth-and-l-maxn + (l c) + ) + (:instance lemma-2-pre + (l c) + (r (R-DEFTRAJ (L-DEFSEQ A (L-DEPTH A) (L-MAXN A)) + CKT (S-MAKE (L-MAXN A) 'X))) + (n (L-DEPTH a)) + (m (L-MAXN a)) + ) + ) + ) + ) + :otf-flg t + ) + + +(defthm fundamental-theorem-of-ste-pre + (implies (and (l-p a) + (l-p c) + (c-p ckt) + + (equal (l-depth a) (l-depth c)) + (equal (l-maxn a) (l-maxn c)) + + (equal (len ckt) (l-maxn a)) + ) + (iff (ste-thm ckt a c) + (r-lte (l-defseq c (l-depth c) (l-maxn c)) + (l-deftraj a ckt)))) + :hints (("Goal" + :use ((:instance ste-thm-forward) + (:instance ste-thm-backward)))) + ) + +(defun ste-wf-maxn (ckt thms) + (if (consp thms) + (cons `(equal (l-maxn ,(first (first thms))) (len ,ckt)) + (cons `(equal (l-maxn ,(second (first thms))) (len ,ckt)) + (ste-wf-maxn ckt (cdr thms)))) + nil)) + +(defun ste-wf-depth (deep thms) + (if (consp thms) + (cons `(l-p ,(first (first thms))) + (cons `(l-p ,(second (first thms))) + (cons `(equal (l-depth ,(first (first thms))) + (l-depth ,deep)) + (cons `(equal (l-depth ,(second (first thms))) + (l-depth ,deep)) + (ste-wf-depth deep (cdr thms)))))) + nil)) + +(defmacro ste-wf (ckt &rest thms) + `(and + (c-p ,ckt) + ,@(ste-wf-maxn ckt thms) + ,@(ste-wf-depth (first (first thms)) thms) + ) + ) + +(defthm fundamental-theorem-of-ste + (implies (and (l-p a) + (l-p c) + (c-p ckt) + + (ste-wf ckt (a c)) + + ;(equal (l-depth a) (l-depth c)) + ;(equal (l-maxn a) (l-maxn c)) + + ;(equal (len ckt) (l-maxn a)) + ) + (iff (ste-thm ckt a c) + (r-lte (defseq c) + (deftraj a ckt)))) + + :hints (("Goal" + :use ((:instance fundamental-theorem-of-ste-pre ) + ))) + )
\ No newline at end of file |