		Search-engine friendly clone of the ACL2 documentation.

Defretgen

Defret-mutual-generate

Generate a defret-mutual form using rules that produce hyps and conclusion conjuncts based on define formal and return specifiers.

Motivation

Suppose you have a mutual recursion with several functions and you want to prove some theorems about them. Often you need to prove something about all of them at once using mutual induction; defret-mutual and ACL2::make-flag are good tools for doing this. But sometimes there are so many functions that it becomes unwieldy to write a full defret-mutual form containing an explicit theorem for each function. This often involves a lot of repetition and isn't very DRY. Instead, one might be able to generate the theorems using rules based on the input/output signature of the functions. That is what defret-mutual-generate is intended to do.

The general idea is that for each function in the clique, we get that function's input/output signature and apply a sequence of rules, defined by the arguments to defret-mutual-generate, which result in a theorem to prove. The rules may check things like the presence or absence of a formal or return value, the name of the function, etc., and compose the resulting theorem by adding hypothesis or conclusion conjuncts, B* bindings, etc. Then we take the results from all the functions in the clique and prove them all together using defret-mutual.

Invocation Syntax

For a single set of rules generating a mutually inductive set of theorems, use the following form. The conditions and actions used by the rules entries are described below.

(defret-mutual-generate thmname-template
  :rules ((condition1 action1 ...)
          (condition2 action2 ...)
          ...)
  ;; abbreviations that generate more rules
  :formal-hyps ...
  :return-concls ...
  :function-keys ...

  ;; optional keywords
  :hints top-level-hints
  :instructions rarely-used
  :no-induction-hint nil
  :otf-flg nil
  ;; defaults to the most recent defines form:
  :mutual-recursion defines-name)

A few other keywords effectively generate additional :rules entries, as discussed below under Common Abbreviations. These may be used wherever :rules may occur.

For example:

(defret-mutual-generate term-vars-of-<fn>
   :rules ((t
            (:each-formal :type pseudo-termp :var x (:add-hyp (not (member v (term-vars x)))))
            (:each-formal :type pseudo-term-listp :var x (:add-hyp (not (member v (termlist-vars x)))))
            (:each-return :type pseudo-termp :var x (:add-concl (not (member v (term-vars x)))))
            (:each-return :type pseudo-term-listp :var x (:add-concl (not (member v (termlist-vars x))))))
           ((:has-return :type pseudo-term-listp)
            (:set-thmname termlist-vars-of-<fn>))
           ((:has-formal :name x :type pseudo-term-listp)
            (:add-keyword :hints ('(:expand ((termlist-vars x)))))))
  :mutual-recursion my-rewriter)

Sometimes it is necessary to prove more than one kind of theorem at once within a mutual induction. In this case defret-mutual-generate allows more than one set of rules to apply separately to each function in the mutual recursion, and makes a defret-mutual form containing all of the resulting defret forms. The syntax for this is as follows:

(defret-mutual-generate
  (defret-generate thmname-template1
    :rules rules1
    ...)
  (defret-generate thmname-template2
    :rules rules2
    ...)
  ...
  ;; same optional keywords as above
  :hints top-level-hints
  :mutual-recursion my-defines-name)

Theorem Generation Rules

The format of rules and rule abbreviations are described in the topic defretgen-rules.