		Search-engine friendly clone of the ACL2 documentation.

Flattening

Simplify-flattened-if

Simplify a flattened conditional statement.

Signature
(simplify-flattened-if branches else) → stmt
Arguments: branches — Guard (branch-listp branches).; else — Guard (statement-listp else).
Returns: stmt — Type (statementp stmt).

A conditional statement is flattened in two phases. The first phase, in flatten-statement, homomorphically flattens their constituents, obtaining a list of branches with flattened tests and bodies plus a flattened list of statements for the default. In the second phase, which we do in this ACL2 function here, we simplify things as follows. We go through the branches in order, and: (i) if a branch test is false, we remove the branch and continue processing the subsequent ones; (ii) if a branch test is true, we discard all the branches that follow; (iii) otherwise, we keep the branch and continue processing the subsequent ones. The default block is discarded if a branch with true test is found; otherwise it is kept. If no branches are left (i.e. they have all been removed), we just return the default block. If there are branches left, we return those along with the default branch, packaged into a conditional statement. In any case, this ACL2 function returns a statement. This function never returns any error. The returned statement may be the same as the result from the first phase, i.e. the second phase may not simplify anything.

Definitions and Theorems

Function: simplify-flattened-if-aux

(defun simplify-flattened-if-aux (branches else)
  (declare (xargs :guard (and (branch-listp branches)
                              (statement-listp else))))
  (let ((__function__ 'simplify-flattened-if-aux))
    (declare (ignorable __function__))
    (b* (((when (endp branches))
          (mv nil (statement-list-fix else)))
         (branch (car branches))
         ((when (equal (branch->test branch)
                       (expression-literal (literal-bool t))))
          (mv nil (branch->body branch)))
         ((when (equal (branch->test branch)
                       (expression-literal (literal-bool nil))))
          (simplify-flattened-if-aux (cdr branches)
                                     else))
         ((mv new-cdr-branches new-else)
          (simplify-flattened-if-aux (cdr branches)
                                     else))
         (new-branches (cons (branch-fix branch)
                             new-cdr-branches)))
      (mv new-branches new-else))))

Theorem: branch-listp-of-simplify-flattened-if-aux.new-branches

(defthm branch-listp-of-simplify-flattened-if-aux.new-branches
  (b* (((mv ?new-branches ?new-else)
        (simplify-flattened-if-aux branches else)))
    (branch-listp new-branches))
  :rule-classes :rewrite)

Theorem: statement-listp-of-simplify-flattened-if-aux.new-else

(defthm statement-listp-of-simplify-flattened-if-aux.new-else
  (b* (((mv ?new-branches ?new-else)
        (simplify-flattened-if-aux branches else)))
    (statement-listp new-else))
  :rule-classes :rewrite)

Theorem: simplify-flattened-if-aux-of-branch-list-fix-branches

(defthm simplify-flattened-if-aux-of-branch-list-fix-branches
  (equal (simplify-flattened-if-aux (branch-list-fix branches)
                                    else)
         (simplify-flattened-if-aux branches else)))

Theorem: simplify-flattened-if-aux-branch-list-equiv-congruence-on-branches

(defthm
 simplify-flattened-if-aux-branch-list-equiv-congruence-on-branches
 (implies (branch-list-equiv branches branches-equiv)
          (equal (simplify-flattened-if-aux branches else)
                 (simplify-flattened-if-aux branches-equiv else)))
 :rule-classes :congruence)

Theorem: simplify-flattened-if-aux-of-statement-list-fix-else

(defthm simplify-flattened-if-aux-of-statement-list-fix-else
 (equal
      (simplify-flattened-if-aux branches (statement-list-fix else))
      (simplify-flattened-if-aux branches else)))

Theorem: simplify-flattened-if-aux-statement-list-equiv-congruence-on-else

(defthm
  simplify-flattened-if-aux-statement-list-equiv-congruence-on-else
  (implies (statement-list-equiv else else-equiv)
           (equal (simplify-flattened-if-aux branches else)
                  (simplify-flattened-if-aux branches else-equiv)))
  :rule-classes :congruence)

Function: simplify-flattened-if

(defun simplify-flattened-if (branches else)
  (declare (xargs :guard (and (branch-listp branches)
                              (statement-listp else))))
  (let ((__function__ 'simplify-flattened-if))
    (declare (ignorable __function__))
    (b* (((mv new-branches new-else)
          (simplify-flattened-if-aux branches else)))
      (if (consp new-branches)
          (make-statement-if :branches new-branches
                             :else new-else)
        (statement-block new-else)))))

Theorem: statementp-of-simplify-flattened-if

(defthm statementp-of-simplify-flattened-if
  (b* ((stmt (simplify-flattened-if branches else)))
    (statementp stmt))
  :rule-classes :rewrite)

Theorem: simplify-flattened-if-of-branch-list-fix-branches

(defthm simplify-flattened-if-of-branch-list-fix-branches
  (equal (simplify-flattened-if (branch-list-fix branches)
                                else)
         (simplify-flattened-if branches else)))

Theorem: simplify-flattened-if-branch-list-equiv-congruence-on-branches

(defthm
     simplify-flattened-if-branch-list-equiv-congruence-on-branches
  (implies (branch-list-equiv branches branches-equiv)
           (equal (simplify-flattened-if branches else)
                  (simplify-flattened-if branches-equiv else)))
  :rule-classes :congruence)

Theorem: simplify-flattened-if-of-statement-list-fix-else

(defthm simplify-flattened-if-of-statement-list-fix-else
  (equal (simplify-flattened-if branches (statement-list-fix else))
         (simplify-flattened-if branches else)))

Theorem: simplify-flattened-if-statement-list-equiv-congruence-on-else

(defthm
      simplify-flattened-if-statement-list-equiv-congruence-on-else
  (implies (statement-list-equiv else else-equiv)
           (equal (simplify-flattened-if branches else)
                  (simplify-flattened-if branches else-equiv)))
  :rule-classes :congruence)