; Portcullis commands:
; (add-include-book-dir :cbooks "/Users/kaufmann/fh/e/current/e/cbooks")
; (include-book "g-logic/portcullis" :dir :cbooks)
(in-package "ACL2")
(include-book "g-logic/bfr-proof-check" :dir :cbooks)
(set-inhibit-warnings "theory") ; avoid some annoying warnings
(set-zzchk-debug-level 2) ; optional
;;;;;;;;;; First example ;;;;;;;;;;
(gl::with-recorded-proofs ; supports two-pass approach
(def-gl-thm bool-distrib ; prove theorem with SAT solver
:hyp (and (booleanp a)
(booleanp b)
(booleanp c))
:concl (iff (or (and a b) c)
(and (or a c) (or b c)))
:rule-classes nil
:g-bindings `((a ,(gl::g-boolean 0))
(b ,(gl::g-boolean 1))
(c ,(gl::g-boolean 2))))
; Add optional argument of t here, if you want proofs to be checked when
; running interactively.
)
(encapsulate
()
(set-enforce-redundancy t) ; local to encapsulate
(defthm bool-distrib ; redundant
(implies (and (booleanp a) (booleanp b) (booleanp c))
(iff (or (and a b) c) (and (or a c) (or b c))))
:rule-classes nil))
;;;;;;;;;; Second example ;;;;;;;;;;
; From e/cbooks/g-logic/examples/mostek-6502-def.lisp:
(local
(defun mk-number-list (start skip n)
(declare (xargs :guard (and (natp n)
(acl2-numberp start)
(acl2-numberp skip))))
(if (zp (nfix n))
nil
(cons start (mk-number-list (+ start skip) skip (1- n))))))
(gl::with-recorded-proofs
(def-gl-thm add-test-32
:hyp (let* ((nbits 32) (ubound (expt 2 (1- nbits))) (lbound (- ubound)))
(and (integerp a) (< lbound a) (< a ubound)
(integerp b) (< lbound b) (< b ubound)))
:concl (equal (+ a b) (+ b a))
:rule-classes nil
:g-bindings `((a (:G-NUMBER ,(mk-number-list 0 2 32)))
(b (:G-NUMBER ,(mk-number-list 1 2 32)))))
; Add optional argument of t here, if you want proofs to be checked when
; running interactively.
)
(encapsulate
()
(set-enforce-redundancy t) ; local to encapsulate
(defthm add-test-32 ; redundant
(implies (let* ((nbits 32) (ubound (expt 2 (1- nbits))) (lbound (- ubound)))
(and (integerp a) (< lbound a) (< a ubound)
(integerp b) (< lbound b) (< b ubound)))
(equal (+ a b) (+ b a)))
:rule-classes nil))
; For more examples, see (relative to cbooks/ directorY) the book
; ../e4/regression/bfr-proof-check-test.lisp.