		Search-engine friendly clone of the ACL2 documentation.

Syntax-abstraction

Abstract-bit

A BIT parse tree is abstracted to its bit.

Signature
(abstract-bit tree) → bit
Arguments: tree — Guard (treep tree).
Returns: bit — Type (integer-range-p 0 2 bit).

Definitions and Theorems

Function: abstract-bit

(defun abstract-bit (tree)
  (declare (xargs :guard (treep tree)))
  (b* (((fun (fail))
        (prog2$ (abstract-fail) 0))
       ((unless (tree-case tree :nonleaf))
        (fail))
       (treess (tree-nonleaf->branches tree))
       ((unless (consp treess)) (fail))
       (trees (car treess))
       ((unless (consp trees)) (fail))
       (subtree (car trees))
       (nat (abstract-terminal subtree)))
    (if (eql nat (char-code #\0)) 0 1)))

Theorem: return-type-of-abstract-bit

(defthm return-type-of-abstract-bit
  (b* ((bit (abstract-bit tree)))
    (integer-range-p 0 2 bit))
  :rule-classes :rewrite)

Theorem: natp-of-abstract-bit

(defthm natp-of-abstract-bit
  (b* ((bit (abstract-bit tree)))
    (natp bit))
  :rule-classes :type-prescription)

Theorem: abstract-bit-linear

(defthm abstract-bit-linear
  (b* ((bit (abstract-bit tree)))
    (< bit 2))
  :rule-classes :linear)