PRACTICE-FORMULATING-STRONG-RULES-4

Major Section:  INTRODUCTION-TO-THE-THEOREM-PROVER

What rules come to mind when looking at the following subterm of a Key Checkpoint? Think of strong rules (see strong-rewrite-rules).

(SUBSETP (APPEND (FOO A) (BAR B)) (MUM C))

When is (append x y) a subset of z? When everything in x is in z and everything in y is in z. We would make it a rewrite rule:

(defthm subsetp-append-1-strong
  (equal (subsetp (append x y) z)
         (and (subsetp x z)
              (subsetp y z))))

We put the ``-1-'' in the name because there is a comparable theorem for when the append is in the second argument of the subsetp; see practice-formulating-strong-rules-5.

This strong rule is better than the conditional rule;

(defthm subsetp-append-1-weak
  (implies (and (subsetp x z)
                (subsetp y z))
           (subsetp (append x y) z)))

Use your browser's Back Button now to return to practice-formulating-strong-rules.