		Search-engine friendly clone of the ACL2 documentation.

Casesplit

APT case splitting transformation: rephrase a function definition by cases.

Introduction

Given a function, and some theorems asserting its equality to other functions under different conditions, this transformation generates an equivalent function defined to be equal to those other functions under suitable conditions.

This transformation can be used to bring together different refinements of the original function made under the different conditions, each such refinement being possibly initiated by a use of restrict with the corresponding condition.

The casesplit design notes, which use this notation, provide the mathematical concepts and template proofs upon which this transformation is based. These notes should be read alongside this reference documentation, which refers to them in some places.

General Form

(casesplit old
           conditions
           theorems
           :new-name       ; default :auto
           :new-enable     ; default :auto
           :thm-name       ; default :auto
           :thm-enable     ; default t
           :verify-guards  ; default :auto
           :hints          ; default nil
           :print          ; default :result
           :show-only      ; default nil
  )

Inputs

old

Denotes the target function to transform.
It must be the name of a function, or a numbered name with a wildcard index that resolves to the name of a function. In the rest of this documentation page, for expository convenience, it is assumed that old is the name of the denoted function.
old must be in logic mode, return a non-multiple value, and have no input or output stobjs. If the :verify-guards input is t, old must be guard-verified.
Let x1, ..., xn be the formal arguments of old
Let old-guard<x1,...,xn> be the guard term of old.
In the casesplit design notes, old is denoted by f.

conditions

Denotes the conditions that define the cases in which the definition of the new function is split.
It must be a non-empty true list (cond1 ... condp) of terms that include no free variables other than x1, ..., xn, that only call logic-mode functions, that return non-multiple values, and that have no output stobjs. If the generated function is guard-verified (which is determined by the :verify-guards input; see below), then the terms must only call guard-verified functions, except possibly in the :logic subterms of mbes and via ec-call. The terms must not include any calls to old.
In order to highlight the dependence on x1, ..., xn, in the rest of this documentation page, condk<x1,...,xn> may be used for condk.
In the casesplit design notes, condk is denoted by c_k, for 1 \leq k \leq p.

theorems

Denotes the theorems that assert the equality of old to other functions under certain conditions.
It must be a non-empty true list of symbols (thm1 ... thmp thm0) that name existing theorems, each of the form
(defthm thmk
  (implies hypk<x1,...,xn>
           (equal (old x1 ... xn)
                  newk<x1,...,xn>)))
where hypk and newk are terms that depend on (some of) x1, ..., xn (so that the theorem includes no free variables other than x1, ..., xn). As a special case, the theorem may have no hypothesis, which is equivalent to hyp<x1,...,xn> being t. The rule classes of the theorem are irrelevant, as is its enablement.
The fact that thm0 comes after thm1, ..., thmp is intentional, since each thmk corresponds to condk as explicated below.
In the casesplit design notes, thmk, hypk and newk are denoted by \mathit{ff}'_k, h_k, and f_k, for 0 \leq k \leq p.

:new-name — default :auto

Determines the name of the generated new function.
It must be one of the following:
:auto, to generate the name automatically as described in function-name-generation.
Any other symbol, to use as the name of the function.
In the rest of this documentation page, let new be the name of this function.

:new-enable — default :auto

Determines whether new is enabled.
It must be one of the following:
t, to enable it.
nil, to disable it.
:auto, to enable it iff old is enabled.

thm-name — default :auto

Determines the name of the theorem that relates old to new:
:auto, to use the paired name obtained by pairing the name of old and the name of new, putting the result into the same package as new.
Any other symbol (that is not in the main Lisp package and that is not a keyword), to use as the name of the theorem.
In the rest of this documentation page, let old-to-new be this theorem.

:thm-enable — default t

Determines whether old-to-new is enabled:
t, to enable it.
nil, to disable it.

:verify-guards — default :auto

Determines whether the guards of the generated functions are verified or not.
It must be one of the following:
t, to verify the guards.
nil, to not verify guards.
:auto, to verify the guards if and only if the guards of the target function old are verified.

:hints — default nil

Hints to prove the applicability conditions.
It must be one of the following:
A keyword-value list (appcond1 hints1 appcond2 hints2 ...), where each appcondk is a keyword that identifies one of the applicability conditions listed in the `Applicability Conditions' section and each hintsk is a list of hints of the kind that may appear just after :hints in a defthm. The hints hintsk are used to prove applicability condition appcondk. The appcond1, appcond2, ... keywords must be all distinct. An appcondk keyword is allowed only if the corresponding applicability condition is present, as specified in the `Applicability Conditions' section.
A list of hints of the kind that may appear just after :hints in a defthm. In this case, these same hints are used to prove every applicability condition,.

:print — default :result

Specifies what is printed on the screen (see screen printing).
It must be one of the following:
nil, to print nothing (not even error output).
:error, to print only error output (if any).
:result, to print, besides any error output, also the results of casesplit. This is the default value of the :print input.
:info, to print, besides any error output and the results, also some additional information about the internal operations of casesplit.
:all, to print, besides any error output, the results, and the additional information, also ACL2's output in response to all the submitted events.
If the call of casesplit is redundant, an indication to that effect is printed on the screen, unless :print is nil.

:show-only — default nil

Determines whether the event expansion of casesplit is submitted to ACL2 or just printed on the screen:
nil, to submit it.
t, to just print it. In this case: the event expansion is printed even if :print is nil (because the user has explicitly asked to show the event expansion); the resulting events are not re-printed separately (other than their appearance in the printed event expansion) even if :print is :result or :info or :all; no ACL2 output is printed for the event expansion even if :print is :all (because the event expansion is not submitted). If the call of casesplit is redundant (as defined in the `Redundancy' section), the event expansion generated by the existing call is printed.

Applicability Conditions

In order for casesplit to apply, in addition to the requirements on the inputs stated in the `Inputs' section, the following applicability conditions must be proved. The proofs are attempted when casesplit is called, using the hints optionally supplied as the :hints input described in the `Inputs' section.

:thm1-hyp
...
:thmp-hyp

condk, along with the negation of the preceding conditions, establishes the hypothesis of thmk:
(implies (and (not cond1<x1,...,xn>)
              ...
              (not condk-1<x1,...,xn>)
              condk<x1,...,xn>)
         hypk<x1,...,xn>)
There are p applicability conditions of this form.
Each of these corresponds to a H_k in the casesplit design notes, for 1 \leq k \leq p.

:thm0-hyp

The negation of all the conditions establishes the hypothesis of thm0:
(implies (and (not cond1<x1,...,xn>)
              ...
              (not condk<x1,...,xn>))
         hyp0<x1,...,xn>)
This corresponds to H_0 in the casesplit design notes.

cond1-guard
...
condp-guard

Each condk is well-defined (according to its guards) under the negation of the preceding conditions:
(implies (and 
              (not cond1<x1,...,xn>)
              ...
              (not condk-1<x1,...,xn>))
         condk-guard<x1,...,xn>)
where condk-guard consists of the guard obligations of condk.
There are p applicability conditions of this form.
Each of these corresponds to a \mathit{GC}_k in the casesplit design notes, for 1 \leq k \leq p.
These applicability conditions are present if and only if the generated function is guard-verified (which is determined by the :verify-guards input; see above).

new1-guard
...
newp-guard

Each newk is well-defined (according to its guards) under condk and the negation of the preceding conditions:
(implies (and (not cond1<x1,...,xn>)
              ...
              (not condk-1<x1,...,xn>)
              condk<x1,...,xn>)
         newk-guard<x1,...,xn>)
where newk-guard consists of the guard obligations of newk.
There are p applicability conditions of this form.
Each of these corresponds to a \mathit{Gf}_k in the casesplit design notes, for 1 \leq k \leq p.
These applicability conditions are present if and only if the generated function is guard-verified (which is determined by the :verify-guards input; see above).

new0-guard

new0 is well-defined (according to its guards) under the negation of all the conditions:
(implies (and (not cond1<x1,...,xn>)
              ...
              (not condk<x1,...,xn>))
         new0-guard<x1,...,xn>)
where new0-guard consists of the guard obligations of new0.
This corresponds to \mathit{Gf}_0 in the casesplit design notes.
This applicability condition is present if and only if the generated function is guard-verified (which is determined by the :verify-guards input; see above).

Generated Events

new

Equivalent definition of old by cases:
(defun new (x1 ... xn)
  (cond (cond1<x1,...,xn> new1<x1,...,xn>)
        ...
        (condk<x1,...,xn> newk<x1,...,xn>)
        (t new0<x1,...,xn>)))
This function is not recursive.
The guard is the same as old.
In the casesplit design notes, new is denoted by f'.

old-to-new

Theorem that relates old to new:
(defthm old-to-new
  (equal (old x1 ... xn)
         (new x1 ... xn)))
In the casesplit design notes, old-to-new is denoted by \mathit{ff}'.

Subtopics

Casesplit-implementation: Implementation of casesplit.