		Search-engine friendly clone of the ACL2 documentation.

Nat-set

Nat-sfix

(nat-sfix x) is a usual fty set fixing function.

Signature
(nat-sfix x) → *
Arguments: x — Guard (nat-setp x).

In the logic, we apply nfix to each member of the x. In the execution, none of that is actually necessary and this is just an inlined identity function.

Definitions and Theorems

Function: nat-sfix

(defun nat-sfix (x)
  (declare (xargs :guard (nat-setp x)))
  (mbe :logic (if (nat-setp x) x nil)
       :exec x))

Theorem: nat-setp-of-nat-sfix

(defthm nat-setp-of-nat-sfix
  (nat-setp (nat-sfix x)))

Theorem: nat-sfix-when-nat-setp

(defthm nat-sfix-when-nat-setp
  (implies (nat-setp x)
           (equal (nat-sfix x) x)))

Theorem: emptyp-nat-sfix

(defthm emptyp-nat-sfix
  (implies (or (set::emptyp x) (not (nat-setp x)))
           (set::emptyp (nat-sfix x))))

Theorem: emptyp-of-nat-sfix

(defthm emptyp-of-nat-sfix
  (equal (set::emptyp (nat-sfix x))
         (or (not (nat-setp x))
             (set::emptyp x))))

Function: nat-sequiv$inline

(defun nat-sequiv$inline (x y)
  (declare (xargs :guard (and (nat-setp x) (nat-setp y))))
  (equal (nat-sfix x) (nat-sfix y)))

Theorem: nat-sequiv-is-an-equivalence

(defthm nat-sequiv-is-an-equivalence
  (and (booleanp (nat-sequiv x y))
       (nat-sequiv x x)
       (implies (nat-sequiv x y)
                (nat-sequiv y x))
       (implies (and (nat-sequiv x y) (nat-sequiv y z))
                (nat-sequiv x z)))
  :rule-classes (:equivalence))

Theorem: nat-sequiv-implies-equal-nat-sfix-1

(defthm nat-sequiv-implies-equal-nat-sfix-1
  (implies (nat-sequiv x x-equiv)
           (equal (nat-sfix x) (nat-sfix x-equiv)))
  :rule-classes (:congruence))

Theorem: nat-sfix-under-nat-sequiv

(defthm nat-sfix-under-nat-sequiv
  (nat-sequiv (nat-sfix x) x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-nat-sfix-1-forward-to-nat-sequiv

(defthm equal-of-nat-sfix-1-forward-to-nat-sequiv
  (implies (equal (nat-sfix x) y)
           (nat-sequiv x y))
  :rule-classes :forward-chaining)

Theorem: equal-of-nat-sfix-2-forward-to-nat-sequiv

(defthm equal-of-nat-sfix-2-forward-to-nat-sequiv
  (implies (equal x (nat-sfix y))
           (nat-sequiv x y))
  :rule-classes :forward-chaining)

Theorem: nat-sequiv-of-nat-sfix-1-forward

(defthm nat-sequiv-of-nat-sfix-1-forward
  (implies (nat-sequiv (nat-sfix x) y)
           (nat-sequiv x y))
  :rule-classes :forward-chaining)

Theorem: nat-sequiv-of-nat-sfix-2-forward

(defthm nat-sequiv-of-nat-sfix-2-forward
  (implies (nat-sequiv x (nat-sfix y))
           (nat-sequiv x y))
  :rule-classes :forward-chaining)