		Search-engine friendly clone of the ACL2 documentation.

Find-base-cases

Find-a-base-case-translated-aux

Find a base-case within a translated term.

Signature
(find-a-base-case-translated-aux term fns prefer-then) → (mv erp all-base largest)
Arguments: term — Guard (pseudo-termp term).; fns — Guard (symbol-listp fns).; prefer-then — Guard (booleanp prefer-then).
Returns: erp — nil when a base-case is found.; all-base — t when term is a base-case.
Type (booleanp all-base).; largest — If (or erp all-base), then this is nil. Otherwise, it is the largest (proper) subterm which is a base-case.
Type (pseudo-termp largest), given the guard.

If none of fns appear in term, term is a base-case of itself. If term is an if call, then all base-cases of the ``then'' and ``else'' branches are base-cases of term.

A term may have many base-cases. We bias our search toward larger base-cases, and toward ``then'' branches if prefer-then, and ``else'' branches otherwise.

If term is a base-case, we return it. If either of its branches are base-cases, we return one of those, with the aforementioned biases. Otherwise, we pick the largest base-case in the biased branch.

Definitions and Theorems

Function: find-a-base-case-translated-aux

(defun find-a-base-case-translated-aux (term fns prefer-then)
 (declare (xargs :guard (and (pseudo-termp term)
                             (symbol-listp fns)
                             (booleanp prefer-then))))
 (let ((__function__ 'find-a-base-case-translated-aux))
  (declare (ignorable __function__))
  (b* (((unless (consp term)) (mv nil t nil))
       ((unless (eq 'if (car term)))
        (if (acl2::expr-calls-some-fn fns term)
            (mv t nil nil)
          (mv nil t nil)))
       ((mv erp-then all-base-then largest-then)
        (find-a-base-case-translated-aux (farg2 term)
                                         fns prefer-then))
       ((mv erp-else all-base-else largest-else)
        (find-a-base-case-translated-aux (farg3 term)
                                         fns prefer-then)))
   (cond
      (erp-then (if erp-else (mv erp-else nil nil)
                  (mv nil nil
                      (if all-base-else (farg3 term)
                        largest-else))))
      (erp-else (mv nil nil
                    (if all-base-then (farg2 term)
                      largest-then)))
      (all-base-then
           (if all-base-else
               (if (not (acl2::expr-calls-some-fn fns (farg1 term)))
                   (mv nil t nil)
                 (mv nil nil
                     (if prefer-then (farg2 term)
                       (farg3 term))))
             (mv nil nil (farg2 term))))
      (all-base-else (mv nil nil (farg3 term)))
      (prefer-then (mv nil nil largest-then))
      (t (mv nil nil largest-else))))))

Theorem: booleanp-of-find-a-base-case-translated-aux.all-base

(defthm booleanp-of-find-a-base-case-translated-aux.all-base
  (b* (((mv ?erp ?all-base ?largest)
        (find-a-base-case-translated-aux term fns prefer-then)))
    (booleanp all-base))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-find-a-base-case-translated-aux.largest

(defthm pseudo-termp-of-find-a-base-case-translated-aux.largest
 (implies
      (and (pseudo-termp term)
           (symbol-listp fns)
           (booleanp prefer-then))
      (b* (((mv ?erp ?all-base ?largest)
            (find-a-base-case-translated-aux term fns prefer-then)))
        (pseudo-termp largest)))
 :rule-classes :rewrite)