		Search-engine friendly clone of the ACL2 documentation.

Jmethod

Jmethod-fix

Fixing function for jmethod structures.

Signature
(jmethod-fix x) → new-x
Arguments: x — Guard (jmethodp x).
Returns: new-x — Type (jmethodp new-x).

Definitions and Theorems

Function: jmethod-fix$inline

(defun jmethod-fix$inline (x)
 (declare (xargs :guard (jmethodp x)))
 (let ((__function__ 'jmethod-fix))
  (declare (ignorable __function__))
  (mbe :logic
       (b* ((access (jaccess-fix (cdr (std::da-nth 0 x))))
            (abstract? (acl2::bool-fix (cdr (std::da-nth 1 x))))
            (static? (acl2::bool-fix (cdr (std::da-nth 2 x))))
            (final? (acl2::bool-fix (cdr (std::da-nth 3 x))))
            (synchronized? (acl2::bool-fix (cdr (std::da-nth 4 x))))
            (native? (acl2::bool-fix (cdr (std::da-nth 5 x))))
            (strictfp? (acl2::bool-fix (cdr (std::da-nth 6 x))))
            (result (jresult-fix (cdr (std::da-nth 7 x))))
            (name (str-fix (cdr (std::da-nth 8 x))))
            (params (jparam-list-fix (cdr (std::da-nth 9 x))))
            (throws (string-list-fix (cdr (std::da-nth 10 x))))
            (body (jblock-fix (cdr (std::da-nth 11 x)))))
         (list (cons 'access access)
               (cons 'abstract? abstract?)
               (cons 'static? static?)
               (cons 'final? final?)
               (cons 'synchronized? synchronized?)
               (cons 'native? native?)
               (cons 'strictfp? strictfp?)
               (cons 'result result)
               (cons 'name name)
               (cons 'params params)
               (cons 'throws throws)
               (cons 'body body)))
       :exec x)))

Theorem: jmethodp-of-jmethod-fix

(defthm jmethodp-of-jmethod-fix
  (b* ((new-x (jmethod-fix$inline x)))
    (jmethodp new-x))
  :rule-classes :rewrite)

Theorem: jmethod-fix-when-jmethodp

(defthm jmethod-fix-when-jmethodp
  (implies (jmethodp x)
           (equal (jmethod-fix x) x)))

Function: jmethod-equiv$inline

(defun jmethod-equiv$inline (acl2::x acl2::y)
  (declare (xargs :guard (and (jmethodp acl2::x)
                              (jmethodp acl2::y))))
  (equal (jmethod-fix acl2::x)
         (jmethod-fix acl2::y)))

Theorem: jmethod-equiv-is-an-equivalence

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

Theorem: jmethod-equiv-implies-equal-jmethod-fix-1

(defthm jmethod-equiv-implies-equal-jmethod-fix-1
  (implies (jmethod-equiv acl2::x x-equiv)
           (equal (jmethod-fix acl2::x)
                  (jmethod-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: jmethod-fix-under-jmethod-equiv

(defthm jmethod-fix-under-jmethod-equiv
  (jmethod-equiv (jmethod-fix acl2::x)
                 acl2::x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: equal-of-jmethod-fix-1-forward-to-jmethod-equiv

(defthm equal-of-jmethod-fix-1-forward-to-jmethod-equiv
  (implies (equal (jmethod-fix acl2::x) acl2::y)
           (jmethod-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: equal-of-jmethod-fix-2-forward-to-jmethod-equiv

(defthm equal-of-jmethod-fix-2-forward-to-jmethod-equiv
  (implies (equal acl2::x (jmethod-fix acl2::y))
           (jmethod-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: jmethod-equiv-of-jmethod-fix-1-forward

(defthm jmethod-equiv-of-jmethod-fix-1-forward
  (implies (jmethod-equiv (jmethod-fix acl2::x)
                          acl2::y)
           (jmethod-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)

Theorem: jmethod-equiv-of-jmethod-fix-2-forward

(defthm jmethod-equiv-of-jmethod-fix-2-forward
  (implies (jmethod-equiv acl2::x (jmethod-fix acl2::y))
           (jmethod-equiv acl2::x acl2::y))
  :rule-classes :forward-chaining)