		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Combine-dirabsdeclor-into-dirabsdeclor

Combine a direct abstract declarator into another.

Signature
(combine-dirabsdeclor-into-dirabsdeclor dirabsdeclor1 dirabsdeclor2) → dirabsdeclor
Arguments: dirabsdeclor1 — Guard (dirabsdeclorp dirabsdeclor1).; dirabsdeclor2 — Guard (dirabsdeclorp dirabsdeclor2).
Returns: dirabsdeclor — Type (dirabsdeclorp dirabsdeclor).

A direct abstract declarator has, except for the base case(s), a slot declor? for another optional direct abstract declarator; this follows the structure of the grammar. The real base case is just one, a parenthesized abstract declarator; the other base case is a dummy one (see dirabsdeclor).

This function stores dirabsdeclor1 into the declor? slot of dirabsdeclor2, obtaining a new combined direct abstract declarator, provided that dirabsdeclor2 has that slot and contains nil, as required by the guard.

Definitions and Theorems

Function: combine-dirabsdeclor-into-dirabsdeclor

(defun combine-dirabsdeclor-into-dirabsdeclor
       (dirabsdeclor1 dirabsdeclor2)
 (declare (xargs :guard (and (dirabsdeclorp dirabsdeclor1)
                             (dirabsdeclorp dirabsdeclor2))))
 (declare (xargs :guard (dirabsdeclor-declor?-nil-p dirabsdeclor2)))
 (b* ((dirabsdeclor1 (dirabsdeclor-fix dirabsdeclor1)))
   (dirabsdeclor-case
        dirabsdeclor2
        :dummy-base (prog2$ (impossible) (irr-dirabsdeclor))
        :paren (prog2$ (impossible) (irr-dirabsdeclor))
        :array (change-dirabsdeclor-array dirabsdeclor2
                                          :declor? dirabsdeclor1)
        :array-static1
        (change-dirabsdeclor-array-static1 dirabsdeclor2
                                           :declor? dirabsdeclor1)
        :array-static2
        (change-dirabsdeclor-array-static2 dirabsdeclor2
                                           :declor? dirabsdeclor1)
        :array-star
        (change-dirabsdeclor-array-star dirabsdeclor2
                                        :declor? dirabsdeclor1)
        :function
        (change-dirabsdeclor-function dirabsdeclor2
                                      :declor? dirabsdeclor1))))

Theorem: dirabsdeclorp-of-combine-dirabsdeclor-into-dirabsdeclor

(defthm dirabsdeclorp-of-combine-dirabsdeclor-into-dirabsdeclor
  (b* ((dirabsdeclor (combine-dirabsdeclor-into-dirabsdeclor
                          dirabsdeclor1 dirabsdeclor2)))
    (dirabsdeclorp dirabsdeclor))
  :rule-classes :rewrite)

Theorem: combine-dirabsdeclor-into-dirabsdeclor-of-dirabsdeclor-fix-dirabsdeclor1

(defthm
 combine-dirabsdeclor-into-dirabsdeclor-of-dirabsdeclor-fix-dirabsdeclor1
 (equal (combine-dirabsdeclor-into-dirabsdeclor
             (dirabsdeclor-fix dirabsdeclor1)
             dirabsdeclor2)
        (combine-dirabsdeclor-into-dirabsdeclor
             dirabsdeclor1 dirabsdeclor2)))

Theorem: combine-dirabsdeclor-into-dirabsdeclor-dirabsdeclor-equiv-congruence-on-dirabsdeclor1

(defthm
 combine-dirabsdeclor-into-dirabsdeclor-dirabsdeclor-equiv-congruence-on-dirabsdeclor1
 (implies (dirabsdeclor-equiv dirabsdeclor1 dirabsdeclor1-equiv)
          (equal (combine-dirabsdeclor-into-dirabsdeclor
                      dirabsdeclor1 dirabsdeclor2)
                 (combine-dirabsdeclor-into-dirabsdeclor
                      dirabsdeclor1-equiv dirabsdeclor2)))
 :rule-classes :congruence)

Theorem: combine-dirabsdeclor-into-dirabsdeclor-of-dirabsdeclor-fix-dirabsdeclor2

(defthm
 combine-dirabsdeclor-into-dirabsdeclor-of-dirabsdeclor-fix-dirabsdeclor2
 (equal (combine-dirabsdeclor-into-dirabsdeclor
             dirabsdeclor1
             (dirabsdeclor-fix dirabsdeclor2))
        (combine-dirabsdeclor-into-dirabsdeclor
             dirabsdeclor1 dirabsdeclor2)))

Theorem: combine-dirabsdeclor-into-dirabsdeclor-dirabsdeclor-equiv-congruence-on-dirabsdeclor2

(defthm
 combine-dirabsdeclor-into-dirabsdeclor-dirabsdeclor-equiv-congruence-on-dirabsdeclor2
 (implies (dirabsdeclor-equiv dirabsdeclor2 dirabsdeclor2-equiv)
          (equal (combine-dirabsdeclor-into-dirabsdeclor
                      dirabsdeclor1 dirabsdeclor2)
                 (combine-dirabsdeclor-into-dirabsdeclor
                      dirabsdeclor1 dirabsdeclor2-equiv)))
 :rule-classes :congruence)