Datatypes for the translation in trusted clause-processor
Function:
(defun wordp (atom) (declare (xargs :guard t)) (let ((acl2::__function__ 'wordp)) (declare (ignorable acl2::__function__)) (if (or (acl2-numberp atom) (symbolp atom) (characterp atom) (stringp atom)) t nil)))
Theorem:
(defthm booleanp-of-wordp (b* ((word? (wordp atom))) (booleanp word?)) :rule-classes :rewrite)
Function:
(defun word-fix (atom) (declare (xargs :guard (wordp atom))) (let ((acl2::__function__ 'word-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (if (wordp atom) atom nil) :exec atom)))
Theorem:
(defthm wordp-of-word-fix (b* ((fixed (word-fix atom))) (wordp fixed)) :rule-classes :rewrite)
Theorem:
(defthm equal-word-fixed (b* ((fixed (word-fix atom))) (equal (word-fix fixed) fixed)) :rule-classes :rewrite)
Function:
(defun word-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (wordp acl2::x) (wordp acl2::y)))) (equal (word-fix acl2::x) (word-fix acl2::y)))
Theorem:
(defthm word-equiv-is-an-equivalence (and (booleanp (word-equiv x y)) (word-equiv x x) (implies (word-equiv x y) (word-equiv y x)) (implies (and (word-equiv x y) (word-equiv y z)) (word-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm word-equiv-implies-equal-word-fix-1 (implies (word-equiv acl2::x x-equiv) (equal (word-fix acl2::x) (word-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm word-fix-under-word-equiv (word-equiv (word-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm wordp-of-lisp-to-python-names (wordp (lisp-to-python-names x)))
Function:
(defun word-listp (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'word-listp)) (declare (ignorable acl2::__function__)) (if (atom x) (eq x nil) (and (wordp (car x)) (word-listp (cdr x))))))
Theorem:
(defthm word-listp-of-cons (equal (word-listp (cons acl2::a acl2::x)) (and (wordp acl2::a) (word-listp acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-cdr-when-word-listp (implies (word-listp (double-rewrite acl2::x)) (word-listp (cdr acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-when-not-consp (implies (not (consp acl2::x)) (equal (word-listp acl2::x) (not acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm wordp-of-car-when-word-listp (implies (word-listp acl2::x) (iff (wordp (car acl2::x)) (or (consp acl2::x) (wordp nil)))) :rule-classes ((:rewrite)))
Theorem:
(defthm true-listp-when-word-listp-compound-recognizer (implies (word-listp acl2::x) (true-listp acl2::x)) :rule-classes :compound-recognizer)
Theorem:
(defthm word-listp-of-list-fix (implies (word-listp acl2::x) (word-listp (acl2::list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-sfix (iff (word-listp (set::sfix acl2::x)) (or (word-listp acl2::x) (not (set::setp acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-insert (iff (word-listp (set::insert acl2::a acl2::x)) (and (word-listp (set::sfix acl2::x)) (wordp acl2::a))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-delete (implies (word-listp acl2::x) (word-listp (set::delete acl2::k acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-mergesort (iff (word-listp (set::mergesort acl2::x)) (word-listp (acl2::list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-union (iff (word-listp (set::union acl2::x acl2::y)) (and (word-listp (set::sfix acl2::x)) (word-listp (set::sfix acl2::y)))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-intersect-1 (implies (word-listp acl2::x) (word-listp (set::intersect acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-intersect-2 (implies (word-listp acl2::y) (word-listp (set::intersect acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-difference (implies (word-listp acl2::x) (word-listp (set::difference acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-duplicated-members (implies (word-listp acl2::x) (word-listp (acl2::duplicated-members acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-rev (equal (word-listp (acl2::rev acl2::x)) (word-listp (acl2::list-fix acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-append (equal (word-listp (append acl2::a acl2::b)) (and (word-listp (acl2::list-fix acl2::a)) (word-listp acl2::b))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-rcons (iff (word-listp (acl2::rcons acl2::a acl2::x)) (and (wordp acl2::a) (word-listp (acl2::list-fix acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm wordp-when-member-equal-of-word-listp (and (implies (and (member-equal acl2::a acl2::x) (word-listp acl2::x)) (wordp acl2::a)) (implies (and (word-listp acl2::x) (member-equal acl2::a acl2::x)) (wordp acl2::a))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-when-subsetp-equal (and (implies (and (subsetp-equal acl2::x acl2::y) (word-listp acl2::y)) (equal (word-listp acl2::x) (true-listp acl2::x))) (implies (and (word-listp acl2::y) (subsetp-equal acl2::x acl2::y)) (equal (word-listp acl2::x) (true-listp acl2::x)))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-set-difference-equal (implies (word-listp acl2::x) (word-listp (set-difference-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-intersection-equal-1 (implies (word-listp (double-rewrite acl2::x)) (word-listp (intersection-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-intersection-equal-2 (implies (word-listp (double-rewrite acl2::y)) (word-listp (intersection-equal acl2::x acl2::y))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-union-equal (equal (word-listp (union-equal acl2::x acl2::y)) (and (word-listp (acl2::list-fix acl2::x)) (word-listp (double-rewrite acl2::y)))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-take (implies (word-listp (double-rewrite acl2::x)) (iff (word-listp (take acl2::n acl2::x)) (or (wordp nil) (<= (nfix acl2::n) (len acl2::x))))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-repeat (iff (word-listp (acl2::repeat acl2::n acl2::x)) (or (wordp acl2::x) (zp acl2::n))) :rule-classes ((:rewrite)))
Theorem:
(defthm wordp-of-nth-when-word-listp (implies (and (word-listp acl2::x) (< (nfix acl2::n) (len acl2::x))) (wordp (nth acl2::n acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-update-nth (implies (word-listp (double-rewrite acl2::x)) (iff (word-listp (update-nth acl2::n acl2::y acl2::x)) (and (wordp acl2::y) (or (<= (nfix acl2::n) (len acl2::x)) (wordp nil))))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-butlast (implies (word-listp (double-rewrite acl2::x)) (word-listp (butlast acl2::x acl2::n))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-nthcdr (implies (word-listp (double-rewrite acl2::x)) (word-listp (nthcdr acl2::n acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-last (implies (word-listp (double-rewrite acl2::x)) (word-listp (last acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-remove (implies (word-listp acl2::x) (word-listp (remove acl2::a acl2::x))) :rule-classes ((:rewrite)))
Theorem:
(defthm word-listp-of-revappend (equal (word-listp (revappend acl2::x acl2::y)) (and (word-listp (acl2::list-fix acl2::x)) (word-listp acl2::y))) :rule-classes ((:rewrite)))
Function:
(defun word-list-fix$inline (x) (declare (xargs :guard (word-listp x))) (let ((acl2::__function__ 'word-list-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (if (atom x) nil (cons (word-fix (car x)) (word-list-fix (cdr x)))) :exec x)))
Theorem:
(defthm word-listp-of-word-list-fix (b* ((fty::newx (word-list-fix$inline x))) (word-listp fty::newx)) :rule-classes :rewrite)
Theorem:
(defthm word-list-fix-when-word-listp (implies (word-listp x) (equal (word-list-fix x) x)))
Function:
(defun word-list-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (word-listp acl2::x) (word-listp acl2::y)))) (equal (word-list-fix acl2::x) (word-list-fix acl2::y)))
Theorem:
(defthm word-list-equiv-is-an-equivalence (and (booleanp (word-list-equiv x y)) (word-list-equiv x x) (implies (word-list-equiv x y) (word-list-equiv y x)) (implies (and (word-list-equiv x y) (word-list-equiv y z)) (word-list-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm word-list-equiv-implies-equal-word-list-fix-1 (implies (word-list-equiv acl2::x x-equiv) (equal (word-list-fix acl2::x) (word-list-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm word-list-fix-under-word-list-equiv (word-list-equiv (word-list-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm equal-of-word-list-fix-1-forward-to-word-list-equiv (implies (equal (word-list-fix acl2::x) acl2::y) (word-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm equal-of-word-list-fix-2-forward-to-word-list-equiv (implies (equal acl2::x (word-list-fix acl2::y)) (word-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm word-list-equiv-of-word-list-fix-1-forward (implies (word-list-equiv (word-list-fix acl2::x) acl2::y) (word-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm word-list-equiv-of-word-list-fix-2-forward (implies (word-list-equiv acl2::x (word-list-fix acl2::y)) (word-list-equiv acl2::x acl2::y)) :rule-classes :forward-chaining)
Theorem:
(defthm car-of-word-list-fix-x-under-word-equiv (word-equiv (car (word-list-fix acl2::x)) (car acl2::x)))
Theorem:
(defthm car-word-list-equiv-congruence-on-x-under-word-equiv (implies (word-list-equiv acl2::x x-equiv) (word-equiv (car acl2::x) (car x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cdr-of-word-list-fix-x-under-word-list-equiv (word-list-equiv (cdr (word-list-fix acl2::x)) (cdr acl2::x)))
Theorem:
(defthm cdr-word-list-equiv-congruence-on-x-under-word-list-equiv (implies (word-list-equiv acl2::x x-equiv) (word-list-equiv (cdr acl2::x) (cdr x-equiv))) :rule-classes :congruence)
Theorem:
(defthm cons-of-word-fix-x-under-word-list-equiv (word-list-equiv (cons (word-fix acl2::x) acl2::y) (cons acl2::x acl2::y)))
Theorem:
(defthm cons-word-equiv-congruence-on-x-under-word-list-equiv (implies (word-equiv acl2::x x-equiv) (word-list-equiv (cons acl2::x acl2::y) (cons x-equiv acl2::y))) :rule-classes :congruence)
Theorem:
(defthm cons-of-word-list-fix-y-under-word-list-equiv (word-list-equiv (cons acl2::x (word-list-fix acl2::y)) (cons acl2::x acl2::y)))
Theorem:
(defthm cons-word-list-equiv-congruence-on-y-under-word-list-equiv (implies (word-list-equiv acl2::y y-equiv) (word-list-equiv (cons acl2::x acl2::y) (cons acl2::x y-equiv))) :rule-classes :congruence)
Theorem:
(defthm consp-of-word-list-fix (equal (consp (word-list-fix acl2::x)) (consp acl2::x)))
Theorem:
(defthm word-list-fix-under-iff (iff (word-list-fix acl2::x) (consp acl2::x)))
Theorem:
(defthm word-list-fix-of-cons (equal (word-list-fix (cons a x)) (cons (word-fix a) (word-list-fix x))))
Theorem:
(defthm len-of-word-list-fix (equal (len (word-list-fix acl2::x)) (len acl2::x)))
Theorem:
(defthm word-list-fix-of-append (equal (word-list-fix (append std::a std::b)) (append (word-list-fix std::a) (word-list-fix std::b))))
Theorem:
(defthm word-list-fix-of-repeat (equal (word-list-fix (acl2::repeat acl2::n acl2::x)) (acl2::repeat acl2::n (word-fix acl2::x))))
Theorem:
(defthm list-equiv-refines-word-list-equiv (implies (acl2::list-equiv acl2::x acl2::y) (word-list-equiv acl2::x acl2::y)) :rule-classes :refinement)
Theorem:
(defthm nth-of-word-list-fix (equal (nth acl2::n (word-list-fix acl2::x)) (if (< (nfix acl2::n) (len acl2::x)) (word-fix (nth acl2::n acl2::x)) nil)))
Theorem:
(defthm word-list-equiv-implies-word-list-equiv-append-1 (implies (word-list-equiv acl2::x fty::x-equiv) (word-list-equiv (append acl2::x acl2::y) (append fty::x-equiv acl2::y))) :rule-classes (:congruence))
Theorem:
(defthm word-list-equiv-implies-word-list-equiv-append-2 (implies (word-list-equiv acl2::y fty::y-equiv) (word-list-equiv (append acl2::x acl2::y) (append acl2::x fty::y-equiv))) :rule-classes (:congruence))
Theorem:
(defthm word-list-equiv-implies-word-list-equiv-nthcdr-2 (implies (word-list-equiv acl2::l l-equiv) (word-list-equiv (nthcdr acl2::n acl2::l) (nthcdr acl2::n l-equiv))) :rule-classes (:congruence))
Theorem:
(defthm word-list-equiv-implies-word-list-equiv-take-2 (implies (word-list-equiv acl2::l l-equiv) (word-list-equiv (take acl2::n acl2::l) (take acl2::n l-equiv))) :rule-classes (:congruence))
Function:
(defun paragraphp (par) (declare (xargs :guard t)) (let ((acl2::__function__ 'paragraphp)) (declare (ignorable acl2::__function__)) (if (atom par) (wordp par) (and (paragraphp (car par)) (paragraphp (cdr par))))))
Theorem:
(defthm booleanp-of-paragraphp (b* ((paragraph? (paragraphp par))) (booleanp paragraph?)) :rule-classes :rewrite)
Theorem:
(defthm paragraphp-corollary-1 (implies (wordp x) (paragraphp x)))
Theorem:
(defthm paragraphp-corollary-2 (implies (and (consp x) (paragraphp (car x)) (paragraphp (cdr x))) (paragraphp x)))
Theorem:
(defthm paragraphp-corollary-3 (implies (and (consp x) (paragraphp x)) (and (paragraphp (car x)) (paragraphp (cdr x)))))
Theorem:
(defthm paragraphp-corollary-4 (implies (and (paragraphp a) (paragraphp b)) (paragraphp (append a b))))
Function:
(defun paragraph-fix (x) (declare (xargs :guard (paragraphp x))) (let ((acl2::__function__ 'paragraph-fix)) (declare (ignorable acl2::__function__)) (mbe :logic (if (consp x) (cons (paragraph-fix (car x)) (paragraph-fix (cdr x))) (word-fix x)) :exec x)))
Theorem:
(defthm paragraphp-of-paragraph-fix (b* ((fixed (paragraph-fix x))) (paragraphp fixed)) :rule-classes :rewrite)
Theorem:
(defthm acl2-count-of-fixed-smaller (b* ((fixed (paragraph-fix x))) (<= (acl2-count fixed) (acl2-count x))) :rule-classes :linear)
Theorem:
(defthm acl2-count-of-car-of-fixed-smaller (b* ((fixed (paragraph-fix x))) (implies (consp fixed) (< (acl2-count (car fixed)) (acl2-count x)))) :rule-classes :linear)
Theorem:
(defthm acl2-count-of-cdr-of-fixed-smaller (b* ((fixed (paragraph-fix x))) (implies (consp fixed) (< (acl2-count (cdr fixed)) (acl2-count x)))) :rule-classes :linear)
Theorem:
(defthm equal-of-fixed-to-x (b* ((fixed (paragraph-fix x))) (implies (paragraphp x) (equal fixed x))) :rule-classes :rewrite)
Function:
(defun paragraph-equiv$inline (acl2::x acl2::y) (declare (xargs :guard (and (paragraphp acl2::x) (paragraphp acl2::y)))) (equal (paragraph-fix acl2::x) (paragraph-fix acl2::y)))
Theorem:
(defthm paragraph-equiv-is-an-equivalence (and (booleanp (paragraph-equiv x y)) (paragraph-equiv x x) (implies (paragraph-equiv x y) (paragraph-equiv y x)) (implies (and (paragraph-equiv x y) (paragraph-equiv y z)) (paragraph-equiv x z))) :rule-classes (:equivalence))
Theorem:
(defthm paragraph-equiv-implies-equal-paragraph-fix-1 (implies (paragraph-equiv acl2::x x-equiv) (equal (paragraph-fix acl2::x) (paragraph-fix x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm paragraph-fix-under-paragraph-equiv (paragraph-equiv (paragraph-fix acl2::x) acl2::x) :rule-classes (:rewrite :rewrite-quoted-constant))
Theorem:
(defthm word-listp-is-paragraphp (implies (word-listp x) (paragraphp x)))