Filtering...

nth-equiv

books/centaur/misc/nth-equiv

Included Books

universal-equiv equiv
other
(in-package "ACL2")
include-book
(include-book "universal-equiv")
include-book
(include-book "std/lists/equiv" :dir :system)
other
(def-universal-equiv nth-equiv
  :qvars n
  :equiv-terms ((equal (nth n x))))
other
(defcong nth-equiv
  equal
  (nth n x)
  2
  :hints (("Goal" :in-theory (enable nth-equiv-necc))))
other
(defcong nth-equiv
  nth-equiv
  (update-nth n v x)
  3
  :hints (("Goal" :in-theory (enable nth-equiv-necc)
     :expand ((:free (n v x y) (nth-equiv (update-nth n v x) y))))))
update-nth-of-same-under-nth-equivtheorem
(defthm update-nth-of-same-under-nth-equiv
  (nth-equiv (update-nth n (nth n x) x) x)
  :hints (("Goal" :in-theory (enable nth-equiv))))
local
(local (defthm +-cancel-consts
    (implies (syntaxp (and (quotep x) (quotep y)))
      (equal (+ x y z) (+ (+ x y) z)))))
other
(defcong nth-equiv
  equal
  (car x)
  1
  :hints (("goal" :use ((:instance nth-equiv-necc (n 0) (y x-equiv)))
     :in-theory (e/d (nth) (nth-equiv-implies-equal-nth-2)))))
other
(defcong nth-equiv
  nth-equiv
  (cdr x)
  1
  :hints (("goal" :use ((:instance nth-equiv-necc
        (n (+ 1 (nfix (nth-equiv-witness (cdr x) (cdr x-equiv)))))
        (y x-equiv)))
     :expand ((nth-equiv (cdr x) (cdr x-equiv)) (nth-equiv (cdr x) nil)
       (nth-equiv nil (cdr x-equiv)))
     :in-theory (disable nth-equiv-implies-equal-nth-2))))
nth-equiv-recursivetheorem
(defthmd nth-equiv-recursive
  (equal (nth-equiv x y)
    (or (and (atom x) (atom y))
      (and (equal (car x) (car y)) (nth-equiv (cdr x) (cdr y)))))
  :hints ((and stable-under-simplificationp
     '(:cases ((nth-equiv x y)))) (and stable-under-simplificationp
      (cond ((equal (car clause) '(nth-equiv x y)) '(:expand ((nth-equiv x y) (:free (n) (nth n x))
              (:free (n) (nth n y))))))))
  :rule-classes ((:definition :install-body nil
     :clique (nth-equiv)
     :controller-alist ((nth-equiv t t)))))
cdr2-indfunction
(defun cdr2-ind
  (x y)
  (declare (xargs :measure (+ (acl2-count x) (acl2-count y))))
  (if (and (atom x) (atom y))
    nil
    (cdr2-ind (cdr x) (cdr y))))
nth-equiv-indtheorem
(defthmd nth-equiv-ind
  t
  :rule-classes ((:induction :pattern (nth-equiv x y) :scheme (cdr2-ind x y))))
other
(defrefinement list-equiv
  nth-equiv
  :hints (("goal" :in-theory (enable nth-equiv-recursive
       nth-equiv-ind
       list-equiv
       true-list-fix))))
true-list-fix-under-nth-equivtheorem
(defthm true-list-fix-under-nth-equiv
  (nth-equiv (true-list-fix x) x))
other
(defcong list-equiv equal (nth-equiv x y) 1)
other
(defcong list-equiv equal (nth-equiv x y) 2)
other
(defcong nth-equiv
  nth-equiv
  (cons x y)
  2
  :hints (("Goal" :in-theory (enable nth-equiv-recursive))))
other
(defcong nth-equiv
  nth-equiv
  (cdr x)
  1
  :hints (("Goal" :in-theory (enable nth-equiv-recursive))))
other
(defcong nth-equiv
  nth-equiv
  (nthcdr n x)
  2
  :hints (("Goal" :in-theory (enable nth-equiv-recursive))))
other
(defcong nth-equiv
  nth-equiv
  (update-nth n v x)
  3
  :hints (("Goal" :in-theory (enable nth-equiv-recursive))))
true-list-fix-under-nth-equivtheorem
(defthm true-list-fix-under-nth-equiv
  (nth-equiv (true-list-fix x) x))
nth-equiv-execfunction
(defun nth-equiv-exec
  (x y)
  (declare (xargs :guard (and (true-listp x) (true-listp y))
      :guard-hints (("goal" :in-theory (enable nth-equiv-recursive nth-equiv-exec)))))
  (mbe :logic (nth-equiv x y)
    :exec (or (and (atom x) (atom y))
      (and (equal (car x) (car y))
        (nth-equiv-exec (cdr x) (cdr y))))))
other
(defsection nth-equiv-fix
  (defund nth-equiv-fix
    (x)
    (declare (xargs :guard (true-listp x)))
    (if (atom (remove nil x))
      nil
      (cons (car x) (nth-equiv-fix (cdr x)))))
  (local (in-theory (enable nth-equiv-fix)))
  (local (defthm nth-when-remove-nil
      (implies (not (consp (remove nil x))) (not (nth n x)))))
  (defthm nth-of-nth-equiv-fix
    (equal (nth n (nth-equiv-fix x)) (nth n x)))
  (defthm nth-equiv-fix-under-nth-equiv
    (nth-equiv (nth-equiv-fix x) x)
    :hints (("Goal" :in-theory (enable nth-equiv))))
  (defthm nth-equiv-fix-self
    (equal (nth-equiv-fix (nth-equiv-fix x)) (nth-equiv-fix x)))
  (local (defthm consp-remove-equal-of-true-list-fix
      (equal (consp (remove-equal k (true-list-fix x)))
        (consp (remove-equal k x)))))
  (defcong nth-equiv
    equal
    (nth-equiv-fix x)
    1
    :hints (("goal" :in-theory (enable nth-equiv-recursive nth-equiv-ind)
       :induct (nth-equiv x x-equiv))))
  (defthmd nth-equiv-is-equal-of-fixes
    (equal (nth-equiv x y)
      (equal (nth-equiv-fix x) (nth-equiv-fix y)))
    :hints (("goal" :use ((:instance nth-equiv-fix-under-nth-equiv) (:instance nth-equiv-fix-under-nth-equiv (x y)))
       :in-theory (disable nth-equiv-fix-under-nth-equiv nth-equiv-fix)))))