• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
      • Fgl-rewrite-rules
      • Fgl-function-mode
      • Fgl-object
      • Fgl-solving
      • Fgl-handling-if-then-elses
      • Fgl-getting-bits-from-objects
      • Fgl-primitive-and-meta-rules
      • Fgl-counterexamples
      • Fgl-interpreter-overview
      • Fgl-correctness-of-binding-free-variables
      • Fgl-debugging
      • Fgl-testbenches
      • Def-fgl-boolean-constraint
      • Fgl-stack
        • Scratchobj
          • Scratchobj-fix
          • Scratchobj-case
          • Scratchobj-equiv
          • Scratchobj-p
          • Scratchobj-formals
          • Scratchobj-fnsym
          • Scratchobj-fgl-objlist
          • Scratchobj-fgl-obj
          • Scratchobj-cinstlist
          • Scratchobj-cinst
          • Scratchobj-bfrlist
          • Scratchobj-kind
          • Scratchobj-bfr
        • Minor-frame
        • Major-frame
        • Major-stack
        • Scratchlist
        • Minor-stack
      • Fgl-rewrite-tracing
      • Def-fgl-param-thm
      • Def-fgl-thm
      • Fgl-fast-alist-support
      • Fgl-array-support
      • Advanced-equivalence-checking-with-fgl
      • Fgl-fty-support
      • Fgl-internals
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Scratchobj

Scratchobj-fix

Fixing function for scratchobj structures.

Signature

(scratchobj-fix x) → new-x

Arguments

x — Guard (scratchobj-p x).

Returns

new-x — Type (scratchobj-p new-x).

Definitions and Theorems

Function: scratchobj-fix$inline

(defun scratchobj-fix$inline (x)
 (declare (xargs :guard (scratchobj-p x)))
 (let ((__function__ 'scratchobj-fix))
  (declare (ignorable __function__))
  (mbe
     :logic
     (case (scratchobj-kind x)
       (:fgl-obj (b* ((val (fgl-object-fix (cdr x))))
                   (cons :fgl-obj val)))
       (:fgl-objlist (b* ((val (fgl-objectlist-fix (cdr x))))
                       (cons :fgl-objlist val)))
       (:bfr (b* ((val (cdr x))) (cons :bfr val)))
       (:bfrlist (b* ((val (list-fix (cdr x))))
                   (cons :bfrlist val)))
       (:cinst (b* ((val (constraint-instance-fix (cdr x))))
                 (cons :cinst val)))
       (:cinstlist (b* ((val (constraint-instancelist-fix (cdr x))))
                     (cons :cinstlist val)))
       (:fnsym (b* ((val (pseudo-fnsym-fix (cdr x))))
                 (cons :fnsym val)))
       (:formals (b* ((val (pseudo-var-list-fix (cdr x))))
                   (cons :formals val))))
     :exec x)))

Theorem: scratchobj-p-of-scratchobj-fix

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

Theorem: scratchobj-fix-when-scratchobj-p

(defthm scratchobj-fix-when-scratchobj-p
  (implies (scratchobj-p x)
           (equal (scratchobj-fix x) x)))

Function: scratchobj-equiv$inline

(defun scratchobj-equiv$inline (x y)
  (declare (xargs :guard (and (scratchobj-p x)
                              (scratchobj-p y))))
  (equal (scratchobj-fix x)
         (scratchobj-fix y)))

Theorem: scratchobj-equiv-is-an-equivalence

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

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

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

Theorem: scratchobj-fix-under-scratchobj-equiv

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

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

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

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

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

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

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

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

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

Theorem: scratchobj-kind$inline-of-scratchobj-fix-x

(defthm scratchobj-kind$inline-of-scratchobj-fix-x
  (equal (scratchobj-kind$inline (scratchobj-fix x))
         (scratchobj-kind$inline x)))

Theorem: scratchobj-kind$inline-scratchobj-equiv-congruence-on-x

(defthm scratchobj-kind$inline-scratchobj-equiv-congruence-on-x
  (implies (scratchobj-equiv x x-equiv)
           (equal (scratchobj-kind$inline x)
                  (scratchobj-kind$inline x-equiv)))
  :rule-classes :congruence)

Theorem: consp-of-scratchobj-fix

(defthm consp-of-scratchobj-fix
  (consp (scratchobj-fix x))
  :rule-classes :type-prescription)