• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
      • Term-level-reasoning
      • Glmc
      • Other-resources
      • Optimization
      • Reference
        • Def-gl-thm
        • Shape-specs
        • Symbolic-objects
        • Gl-aside
        • Def-gl-param-thm
        • Symbolic-arithmetic
        • Bfr
          • Pbfr-depends-on
          • Bfr-varname-p
          • Bfr-varname-fix
          • Bfr-to-param-space
          • Bfr-depends-on
          • Aig-var-fix
          • Bfr-reasoning
            • Bfr-cp-ev
            • Bfr-eval-cp
            • Bfr-patterns
            • Bfr-reasoning-mode
            • Bfr-eval-patterns
          • Bfr-andc2
          • Bfr-andc1
          • Bfr-unparam-env
          • Bfr-set-var
          • Bfr-nor
          • Bfr-nand
          • Bfr-mode
          • Bfr-equiv
          • Bfr-xor
          • Bfr-iff
          • Bfr-eval
          • Bfr-param-env
          • Bfr-lookup
          • Bfr-env-equiv
          • Bfr-and
          • Bfr-var
          • Bfr-or
          • Bfr-not
          • Bfr-ite
          • Bdd-mode-or-p-true
          • Aig-mode-or-p-true
          • Bfr-case
        • Def-gl-boolean-constraint
        • Gl-mbe
        • Bvec
        • Flex-bindings
        • Auto-bindings
        • Gl-interp
        • Gl-set-uninterpreted
        • Def-gl-clause-processor
        • Def-glcp-ctrex-rewrite
        • ACL2::always-equal
        • Gl-hint
        • Def-gl-rewrite
        • Def-gl-branch-merge
        • Gl-force-check
        • Gl-concretize
        • Gl-assert
        • Gl-param-thm
        • Gl-simplify-satlink-mode
        • Gl-satlink-mode
        • Gl-bdd-mode
        • Gl-aig-bddify-mode
        • Gl-fraig-satlink-mode
      • Debugging
      • Basic-tutorial
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Bfr-reasoning

Bfr-cp-ev

Basic evaluator for meta-reasoning about bfr-eval.

Definition: bfr-cp-ev

(encapsulate (((bfr-cp-ev * *) acl2::=> *)
              ((bfr-cp-evl * *) acl2::=> *))
 (set-inhibit-warnings "theory")
 (local (value-triple :elided))
 (local (value-triple :elided))
 (local (value-triple :elided))
 (local (value-triple :elided))
 (local (value-triple :elided))
 (local (value-triple :elided))
 (local (value-triple :elided))
 (local (value-triple :elided))
 (defthmd bfr-cp-ev-constraint-0
   (implies
        (and (consp x)
             (syntaxp (not (equal a ''nil)))
             (not (equal (car x) 'quote)))
        (equal (bfr-cp-ev x a)
               (bfr-cp-ev (cons (car x)
                                (kwote-lst (bfr-cp-evl (cdr x) a)))
                          nil)))
   :hints
   (("Goal" :expand ((:free (x) (hide x))
                     (bfr-cp-ev x a)
                     (:free (args)
                            (bfr-cp-ev (cons (car x) args) nil)))
            :in-theory
            '(acl2::eval-list-kwote-lst acl2::true-list-fix-ev-lst
                                        car-cons cdr-cons))))
 (local (value-triple :elided))
 (defthm bfr-cp-ev-constraint-1
   (implies (symbolp x)
            (equal (bfr-cp-ev x a)
                   (and x (cdr (assoc-equal x a)))))
   :hints (("Goal" :expand ((bfr-cp-ev x a)))))
 (local (value-triple :elided))
 (defthm bfr-cp-ev-constraint-2
   (implies (and (consp x) (equal (car x) 'quote))
            (equal (bfr-cp-ev x a) (cadr x)))
   :hints (("Goal" :expand ((bfr-cp-ev x a)))))
 (local (value-triple :elided))
 (defthm bfr-cp-ev-constraint-3
   (implies (and (consp x) (consp (car x)))
            (equal (bfr-cp-ev x a)
                   (bfr-cp-ev (caddr (car x))
                              (pairlis$ (cadr (car x))
                                        (bfr-cp-evl (cdr x) a)))))
   :hints (("Goal" :expand ((bfr-cp-ev x a)))))
 (local (value-triple :elided))
 (defthm bfr-cp-ev-constraint-4
   (implies (not (consp acl2::x-lst))
            (equal (bfr-cp-evl acl2::x-lst a) nil))
   :hints (("Goal" :expand ((bfr-cp-evl acl2::x-lst a)))))
 (local (value-triple :elided))
 (defthm bfr-cp-ev-constraint-5
   (implies (consp acl2::x-lst)
            (equal (bfr-cp-evl acl2::x-lst a)
                   (cons (bfr-cp-ev (car acl2::x-lst) a)
                         (bfr-cp-evl (cdr acl2::x-lst) a))))
   :hints (("Goal" :expand ((bfr-cp-evl acl2::x-lst a)))))
 (local (value-triple :elided))
 (defthmd bfr-cp-ev-constraint-6
   (implies (and (not (consp x)) (not (symbolp x)))
            (equal (bfr-cp-ev x a) nil))
   :hints (("Goal" :expand ((bfr-cp-ev x a)))))
 (local (value-triple :elided))
 (defthmd bfr-cp-ev-constraint-7
   (implies (and (consp x)
                 (not (consp (car x)))
                 (not (symbolp (car x))))
            (equal (bfr-cp-ev x a) nil))
   :hints (("Goal" :expand ((bfr-cp-ev x a)))))
 (local (value-triple :elided))
 (defthm bfr-cp-ev-constraint-8
  (implies (and (consp x)
                (equal (car x) 'bfr-eval))
           (equal (bfr-cp-ev x a)
                  (bfr-eval (bfr-cp-ev (cadr x) a)
                            (bfr-cp-ev (caddr x) a))))
  :hints
  (("Goal" :expand
           ((bfr-cp-ev x a)
            (:free (x) (hide x))
            (:free (acl2::fn args)
                   (acl2::apply-for-defevaluator acl2::fn args))))))
 (local (value-triple :elided))
 (defthm bfr-cp-ev-constraint-9
  (implies (and (consp x) (equal (car x) 'equal))
           (equal (bfr-cp-ev x a)
                  (equal (bfr-cp-ev (cadr x) a)
                         (bfr-cp-ev (caddr x) a))))
  :hints
  (("Goal" :expand
           ((bfr-cp-ev x a)
            (:free (x) (hide x))
            (:free (acl2::fn args)
                   (acl2::apply-for-defevaluator acl2::fn args))))))
 (local (value-triple :elided))
 (defthm bfr-cp-ev-constraint-10
  (implies (and (consp x) (equal (car x) 'not))
           (equal (bfr-cp-ev x a)
                  (not (bfr-cp-ev (cadr x) a))))
  :hints
  (("Goal" :expand
           ((bfr-cp-ev x a)
            (:free (x) (hide x))
            (:free (acl2::fn args)
                   (acl2::apply-for-defevaluator acl2::fn args))))))
 (local (value-triple :elided))
 (defthm bfr-cp-ev-constraint-11
  (implies (and (consp x) (equal (car x) 'implies))
           (equal (bfr-cp-ev x a)
                  (implies (bfr-cp-ev (cadr x) a)
                           (bfr-cp-ev (caddr x) a))))
  :hints
  (("Goal" :expand
           ((bfr-cp-ev x a)
            (:free (x) (hide x))
            (:free (acl2::fn args)
                   (acl2::apply-for-defevaluator acl2::fn args))))))
 (local (value-triple :elided))
 (defthm bfr-cp-ev-constraint-12
  (implies (and (consp x) (equal (car x) 'if))
           (equal (bfr-cp-ev x a)
                  (if (bfr-cp-ev (cadr x) a)
                      (bfr-cp-ev (caddr x) a)
                    (bfr-cp-ev (cadddr x) a))))
  :hints
  (("Goal" :expand
           ((bfr-cp-ev x a)
            (:free (x) (hide x))
            (:free (acl2::fn args)
                   (acl2::apply-for-defevaluator acl2::fn args))))))
 (local (value-triple :elided)))

Definitions and Theorems

Theorem: bfr-cp-ev-constraint-0

(defthm bfr-cp-ev-constraint-0
  (implies
       (and (consp x)
            (syntaxp (not (equal a ''nil)))
            (not (equal (car x) 'quote)))
       (equal (bfr-cp-ev x a)
              (bfr-cp-ev (cons (car x)
                               (kwote-lst (bfr-cp-evl (cdr x) a)))
                         nil))))

Theorem: bfr-cp-ev-constraint-1

(defthm bfr-cp-ev-constraint-1
  (implies (symbolp x)
           (equal (bfr-cp-ev x a)
                  (and x (cdr (assoc-equal x a))))))

Theorem: bfr-cp-ev-constraint-2

(defthm bfr-cp-ev-constraint-2
  (implies (and (consp x) (equal (car x) 'quote))
           (equal (bfr-cp-ev x a) (cadr x))))

Theorem: bfr-cp-ev-constraint-3

(defthm bfr-cp-ev-constraint-3
  (implies (and (consp x) (consp (car x)))
           (equal (bfr-cp-ev x a)
                  (bfr-cp-ev (caddr (car x))
                             (pairlis$ (cadr (car x))
                                       (bfr-cp-evl (cdr x) a))))))

Theorem: bfr-cp-ev-constraint-4

(defthm bfr-cp-ev-constraint-4
  (implies (not (consp acl2::x-lst))
           (equal (bfr-cp-evl acl2::x-lst a) nil)))

Theorem: bfr-cp-ev-constraint-5

(defthm bfr-cp-ev-constraint-5
  (implies (consp acl2::x-lst)
           (equal (bfr-cp-evl acl2::x-lst a)
                  (cons (bfr-cp-ev (car acl2::x-lst) a)
                        (bfr-cp-evl (cdr acl2::x-lst) a)))))

Theorem: bfr-cp-ev-constraint-6

(defthm bfr-cp-ev-constraint-6
  (implies (and (not (consp x)) (not (symbolp x)))
           (equal (bfr-cp-ev x a) nil)))

Theorem: bfr-cp-ev-constraint-7

(defthm bfr-cp-ev-constraint-7
  (implies (and (consp x)
                (not (consp (car x)))
                (not (symbolp (car x))))
           (equal (bfr-cp-ev x a) nil)))

Theorem: bfr-cp-ev-constraint-8

(defthm bfr-cp-ev-constraint-8
  (implies (and (consp x)
                (equal (car x) 'bfr-eval))
           (equal (bfr-cp-ev x a)
                  (bfr-eval (bfr-cp-ev (cadr x) a)
                            (bfr-cp-ev (caddr x) a)))))

Theorem: bfr-cp-ev-constraint-9

(defthm bfr-cp-ev-constraint-9
  (implies (and (consp x) (equal (car x) 'equal))
           (equal (bfr-cp-ev x a)
                  (equal (bfr-cp-ev (cadr x) a)
                         (bfr-cp-ev (caddr x) a)))))

Theorem: bfr-cp-ev-constraint-10

(defthm bfr-cp-ev-constraint-10
  (implies (and (consp x) (equal (car x) 'not))
           (equal (bfr-cp-ev x a)
                  (not (bfr-cp-ev (cadr x) a)))))

Theorem: bfr-cp-ev-constraint-11

(defthm bfr-cp-ev-constraint-11
  (implies (and (consp x) (equal (car x) 'implies))
           (equal (bfr-cp-ev x a)
                  (implies (bfr-cp-ev (cadr x) a)
                           (bfr-cp-ev (caddr x) a)))))

Theorem: bfr-cp-ev-constraint-12

(defthm bfr-cp-ev-constraint-12
  (implies (and (consp x) (equal (car x) 'if))
           (equal (bfr-cp-ev x a)
                  (if (bfr-cp-ev (cadr x) a)
                      (bfr-cp-ev (caddr x) a)
                    (bfr-cp-ev (cadddr x) a)))))

Theorem: bfr-cp-ev-disjoin-cons

(defthm bfr-cp-ev-disjoin-cons
  (iff (bfr-cp-ev (disjoin (cons x y)) a)
       (or (bfr-cp-ev x a)
           (bfr-cp-ev (disjoin y) a))))

Theorem: bfr-cp-ev-disjoin-when-consp

(defthm bfr-cp-ev-disjoin-when-consp
  (implies (consp x)
           (iff (bfr-cp-ev (disjoin x) a)
                (or (bfr-cp-ev (car x) a)
                    (bfr-cp-ev (disjoin (cdr x)) a)))))

Theorem: bfr-cp-ev-disjoin-atom

(defthm bfr-cp-ev-disjoin-atom
  (implies (not (consp x))
           (equal (bfr-cp-ev (disjoin x) a) nil))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: bfr-cp-ev-disjoin-append

(defthm bfr-cp-ev-disjoin-append
  (iff (bfr-cp-ev (disjoin (append x y)) a)
       (or (bfr-cp-ev (disjoin x) a)
           (bfr-cp-ev (disjoin y) a))))

Theorem: bfr-cp-ev-conjoin-cons

(defthm bfr-cp-ev-conjoin-cons
  (iff (bfr-cp-ev (conjoin (cons x y)) a)
       (and (bfr-cp-ev x a)
            (bfr-cp-ev (conjoin y) a))))

Theorem: bfr-cp-ev-conjoin-when-consp

(defthm bfr-cp-ev-conjoin-when-consp
  (implies (consp x)
           (iff (bfr-cp-ev (conjoin x) a)
                (and (bfr-cp-ev (car x) a)
                     (bfr-cp-ev (conjoin (cdr x)) a)))))

Theorem: bfr-cp-ev-conjoin-atom

(defthm bfr-cp-ev-conjoin-atom
  (implies (not (consp x))
           (equal (bfr-cp-ev (conjoin x) a) t))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: bfr-cp-ev-conjoin-append

(defthm bfr-cp-ev-conjoin-append
  (iff (bfr-cp-ev (conjoin (append x y)) a)
       (and (bfr-cp-ev (conjoin x) a)
            (bfr-cp-ev (conjoin y) a))))

Theorem: bfr-cp-ev-conjoin-clauses-cons

(defthm bfr-cp-ev-conjoin-clauses-cons
  (iff (bfr-cp-ev (conjoin-clauses (cons x y))
                  a)
       (and (bfr-cp-ev (disjoin x) a)
            (bfr-cp-ev (conjoin-clauses y) a))))

Theorem: bfr-cp-ev-conjoin-clauses-when-consp

(defthm bfr-cp-ev-conjoin-clauses-when-consp
  (implies (consp x)
           (iff (bfr-cp-ev (conjoin-clauses x) a)
                (and (bfr-cp-ev (disjoin (car x)) a)
                     (bfr-cp-ev (conjoin-clauses (cdr x))
                                a)))))

Theorem: bfr-cp-ev-conjoin-clauses-atom

(defthm bfr-cp-ev-conjoin-clauses-atom
  (implies (not (consp x))
           (equal (bfr-cp-ev (conjoin-clauses x) a)
                  t))
  :rule-classes ((:rewrite :backchain-limit-lst 0)))

Theorem: bfr-cp-ev-conjoin-clauses-append

(defthm bfr-cp-ev-conjoin-clauses-append
  (iff (bfr-cp-ev (conjoin-clauses (append x y))
                  a)
       (and (bfr-cp-ev (conjoin-clauses x) a)
            (bfr-cp-ev (conjoin-clauses y) a))))