Create a flag-based ACL2::induction scheme for a mutual-recursion.

The

- a "flag function" that mimics a mutual-recursion, and
- a theorem proving that the appropriate invocations of the flag function are equivalent to the original mutually-recursive functions,
- a macro for proving properties by induction according to the flag function.

Generally speaking, writing a corresponding flag function is the first step toward proving any inductive property about mutually recursive definitions; more discussion below.

Example:

(make-flag flag-pseudo-termp ; flag function name (optional) pseudo-termp ; any member of the clique ;; optional arguments: :flag-mapping ((pseudo-termp term) (pseudo-term-listp list)) :defthm-macro-name defthm-pseudo-termp :flag-var flag :body :last ; use last body, not original :hints (("Goal" ...)) ; for the measure theorem ; (usually not necessary) :expand-with-original-defs t ; for the equivalence thm ; (usually not necessary) )

Here

The other arguments are optional:

:flag-mapping specifies short names to identify with each of the functions of the clique. By default we just use the function names themselves, but it's usually nice to pick shorter names since you'll have to mention them in the theorems you prove. The argument, if supplied and non-nil , should be a list that specifies a short name for every function in the clique. Each member of that list should be of the form(old new) where (of course)old andnew are symbols.:defthm-macro-name lets you name the new macro that will be generated for proving theorems by inducting with the flag function. By default it is nameddefthm-[flag-function-name] , i.e., for the above example, it would be calleddefthm-flag-pseudo-termp .:flag-var specifies the name of the variable to use for the flag. By default it is just calledflag , and we rarely change it. To be more precise, it ispkg::flag wherepkg is the package of the new flag function's name; usually this means you don't have to think about the package.:ruler-extenders lets you give a value for the ACL2::ruler-extenders of the new flag function.:body isnil by default, specifying that the original definition is used when extracting the body of each function. The most recent definition rule is used if:body is:last . Otherwise:body should be a list with members of the form(fn1 fn2) , indicating that the definition associated with a rule namedfn2 , if there is one, should be used as the definition for the function symbol,fn1 — and in that case, the formal parameters list specified byfn2 must equal the formal parameters list forfn1 . See the community bookbooks/tools/flag-tests.lisp for an example of using such a alist for:body , in particular for the purpose of using definitions installed with`ACL2::install-not-normalized`.:expand-with-original-defs slightly changes the hints given to the theorem proving that each invocation of the new flag function is equal to the appropriate call of one of the functions of the clique. After induction on the flag function, this theorem uses an expand hint on any call in the conclusion of one of the functions. Normally it doesn't specify what definition to expand with, but if the:expand-with-original-defs keyword is given then it says to expand with the function symbol itself (i.e., the function's original definition) in each case. This helps in cases where the proof is disrupted by some other definition rule.

To prove an inductive theorem about a mutually-recursive function, you usually have to effectively prove a single, big, ugly formula that has a different case about each function in the clique.

Normally, even with the flag function written for you, this would be a
tedious process. Here is an example of how you might prove by induction that

;; ACL2 can prove these are Booleans even without induction due to ;; type reasoning, so for illustration we'll turn these off so that ;; induction is required: (in-theory (disable (:type-prescription pseudo-termp) (:type-prescription pseudo-term-listp) (:executable-counterpart tau-system))) ;; Main part of the proof, ugly lemma with cases. Note that we ;; have to use :rule-classes nil here because this isn't a valid ;; rewrite rule. (local (defthm crux (cond ((equal flag 'term) (booleanp (pseudo-termp x))) ((equal flag 'list) (booleanp (pseudo-term-listp lst))) (t t)) :rule-classes nil :hints(("Goal" :induct (flag-pseudo-termp flag x lst))))) ;; Now we have to re-prove each part of the lemma so that we can use ;; it as a proper rule. (defthm type-of-pseudo-termp (booleanp (pseudo-termp x)) :rule-classes :type-prescription :hints(("Goal" :use ((:instance crux (flag 'term)))))) (defthm type-of-pseudo-term-listp (booleanp (pseudo-term-listp lst)) :rule-classes :type-prescription :hints(("Goal" :use ((:instance crux (flag 'list))))))

Obviously this is tedious and makes you say everything twice. Since the
steps are so standard,

(defthm-pseudo-termp (defthm type-of-pseudo-termp (booleanp (pseudo-termp x)) :rule-classes :type-prescription :flag term) (defthm type-of-pseudo-term-listp (booleanp (pseudo-term-listp lst)) :rule-classes :type-prescription :flag list))

It's worth understanding some of the details of what's going on here.

The macro automatically tries to induct using the induction scheme. But

(mutual-recursion (defun pseudo-termp (x) ...) (defun pseudo-term-listp (lst) ...))

So the theorem above only works without hints because we happened to choose

(defthm-pseudo-termp (defthm type-of-pseudo-termp (booleanp (pseudo-termp term)) :rule-classes :type-prescription :flag term) (defthm type-of-pseudo-term-listp (booleanp (pseudo-term-listp termlist)) :rule-classes :type-prescription :flag list) :hints(("Goal" :induct (flag-pseudo-termp flag term termlist))))

**Proof Templates**. You can submit,
e.g.,

**Localizing Theorems**. Sometimes you may only want to export one of
the theorems. For instance, if we only want to add a rule about the term case,
but no the list case, we could do this:

(defthm-pseudo-termp (defthm type-of-pseudo-termp (booleanp (pseudo-termp x)) :rule-classes :type-prescription :flag term) (defthm type-of-pseudo-term-listp (booleanp (pseudo-term-listp lst)) :flag list :skip t))

**Irrelevant Cases**. Sometimes the theorem you want is inductive in such
a way that some functions are irrelevant; nothing needs to be proved about them
in order to prove the desired theorem about the others. The :skip keyword can
be used with a theorem of T to do this:

(defthm-pseudo-termp (defthm type-of-pseudo-termp (booleanp (pseudo-termp x)) :rule-classes :type-prescription :flag term) (defthm type-of-pseudo-term-listp t :flag list :skip t))

Alternatively, you can provide the :skip-others keyword to the top-level macro and simply leave out the trivial parts:

(defthm-pseudo-termp (defthm type-of-pseudo-termp (booleanp (pseudo-termp x)) :rule-classes :type-prescription :flag term) :skip-others t)

**Multiple Theorems**. You may have more than one defthm form for a given
flag. For the main inductive proof, these are all simply conjoined
together (and their hints are simply appended together), but they are exported
as separate theorems and may have different

**Legacy Syntax**. There is an older, alternate syntax for

For advanced users, note that each individual "theorem" can have its own computed hints. For instance we can write:

(defthm-pseudo-termp (defthm type-of-pseudo-termp (booleanp (pseudo-termp term)) :rule-classes :type-prescription :flag term :hints ('(:expand ((pseudo-termp x))))) (defthm type-of-pseudo-term-listp (booleanp (pseudo-term-listp termlist)) :rule-classes :type-prescription :flag list :hints ('(:expand ((pseudo-term-listp lst))))) :hints(("Goal" :induct (flag-pseudo-termp flag term termlist))))

These hints are used **during the mutually inductive proof**. Under the
top-level induction, we check the clause for the current subgoal to determine
the hypothesized setting of the flag variable, and provide the computed hints
for the appropriate case.

If you provide both a top-level hints form and hints on some or all of the
separate theorems, both sets of hints have an effect; try

You may use subgoal hints as well as computed hints, but they will not have any effect if the particular subgoal does not occur when those hints are in effect. We simply translate subgoal hints to computed hints:

("Subgoal *1/5.2" :in-theory (theory 'foo)) ---> (and (equal id (parse-clause-id "Subgoal *1/5.2")) '(:in-theory (theory 'foo)))

As mentioned above, if there is more than one defthm form for a given flag, the hints for all such forms are simply appended together; the hints given to one such form may affect what you might think of as the proof of another.