Filtering...

remove-guard-holders1

books/system/remove-guard-holders1

Included Books

subcor-var flag pseudo-termp-lemmas
other
(in-package "ACL2")
include-book
(include-book "subcor-var")
local
(local (include-book "tools/flag" :dir :system))
local
(local (include-book "pseudo-termp-lemmas"))
other
(verify-termination apply$-badge-p)
other
(verify-termination badge-userfn-structure-alistp)
other
(verify-termination apply$-badge-alistp-ilks-t)
other
(verify-termination weak-badge-userfn-structure-alistp)
local
(local (defthm weak-badge-userfn-structure-alistp-forward-to-alistp
    (implies (weak-badge-userfn-structure-alistp x) (alistp x))
    :rule-classes :forward-chaining))
local
(local (defthm weak-badge-userfn-structure-alistp-gives-access
    (implies (and (weak-badge-userfn-structure-alistp x)
        (assoc-equal fn x))
      (and (weak-badge-userfn-structure-tuplep (assoc-equal fn x))
        (weak-apply$-badge-p (access-badge-userfn-structure-tuple-badge (assoc-equal fn x)))))
    :rule-classes nil))
badge-userfn-structure-alistp-forward-to-weak-badge-userfn-structure-alistptheorem
(defthm badge-userfn-structure-alistp-forward-to-weak-badge-userfn-structure-alistp
  (implies (badge-userfn-structure-alistp x)
    (weak-badge-userfn-structure-alistp x))
  :rule-classes :forward-chaining)
other
(verify-termination ilks-per-argument-slot
  (declare (xargs :guard-hints (("Goal" :use (:instance weak-badge-userfn-structure-alistp-gives-access
           (x (cdr (assoc-equal :badge-userfn-structure (fgetprop 'badge-table 'table-alist nil wrld))))))))))
local
(local (defthm acl2-count-car-last
    (< (acl2-count (car (last args))) (+ 1 (acl2-count args)))
    :rule-classes :linear))
other
(verify-termination (remove-guard-holders1 (declare (xargs :verify-guards nil))))
local
(local (with-output :off :all :on summary
    (make-flag remove-guard-holders1)))
local
(local (defthm equal-len-0-rewrite
    (equal (equal 0 (len x)) (not (consp x)))))
local
(local (defun my-double-cdr-induction
    (lst ilks)
    (if (atom lst)
      (list lst ilks)
      (my-double-cdr-induction (cdr lst) (cdr ilks)))))
len-mv-nth-1-remove-guard-holders1-lsttheorem
(defthm len-mv-nth-1-remove-guard-holders1-lst
  (equal (len (mv-nth 1 (remove-guard-holders1-lst lst lamp)))
    (len lst))
  :hints (("Goal" :induct (my-double-cdr-induction lst ilks))))
local
(local (defthm pseudo-termp-car-last
    (implies (pseudo-term-listp term)
      (pseudo-termp (car (last term))))))
local
(local (defthm pseudo-termp-listp-append
    (implies (and (pseudo-term-listp terms1) (pseudo-term-listp terms2))
      (pseudo-term-listp (append terms1 terms2)))))
local
(local (defthm pseudo-termp-listp-take
    (implies (pseudo-term-listp terms)
      (pseudo-term-listp (take n terms)))))
local
(local (with-output :off :all :on summary
    (defthm-flag-remove-guard-holders1 (defthm pseudo-termp-remove-guard-holders1
        (implies (pseudo-termp term)
          (pseudo-termp (mv-nth 1 (remove-guard-holders1 changedp0 term lamp))))
        :flag remove-guard-holders1)
      (defthm pseudo-term-listp-remove-guard-holders1-lst
        (implies (pseudo-term-listp lst)
          (pseudo-term-listp (mv-nth 1 (remove-guard-holders1-lst lst lamp))))
        :flag remove-guard-holders1-lst)
      :hints (("Goal" :in-theory (disable member-equal
           pseudo-termp-lambda-lemma
           take
           quote-listp))))))
pseudo-termp-remove-guard-holders1theorem
(defthm pseudo-termp-remove-guard-holders1
  (implies (pseudo-termp term)
    (pseudo-termp (mv-nth 1 (remove-guard-holders1 changedp0 term lamp)))))
pseudo-term-listp-remove-guard-holders1-lsttheorem
(defthm pseudo-term-listp-remove-guard-holders1-lst
  (implies (pseudo-term-listp lst)
    (pseudo-term-listp (mv-nth 1 (remove-guard-holders1-lst lst lamp)))))
local
(local (defthm pseudo-term-listp-remove-guard-holders1-lst-forward
    (implies (pseudo-term-listp lst)
      (pseudo-term-listp (mv-nth 1 (remove-guard-holders1-lst lst lamp))))
    :rule-classes ((:forward-chaining :trigger-terms ((mv-nth 1 (remove-guard-holders1-lst lst lamp)))))))
other
(verify-guards remove-guard-holders1)