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

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 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 )

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 ist ,old must be guard-verified.Let

x1 , ...,xn be the formal arguments ofold Let

old-guard<x1,...,xn> be the guard term ofold .In the

casesplit design notes,old is denoted byf .

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 thanx1 , ...,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 ofmbes and viaec-call. The terms must not include any calls toold .In order to highlight the dependence on

x1 , ...,xn , in the rest of this documentation page,condk<x1,...,xn> may be used forcondk .In the

casesplit design notes,condk is denoted byc_k , for1 \leq k \leq p .

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 andnewk are terms that depend on (some of)x1 , ...,xn (so that the theorem includes no free variables other thanx1 , ...,xn ). As a special case, the theorem may have no hypothesis, which is equivalent tohyp<x1,...,xn> beingt . The rule classes of the theorem are irrelevant, as is its enablement.The fact that

thm0 comes afterthm1 , ...,thmp is intentional, since eachthmk corresponds tocondk as explicated below.In the

casesplit design notes,thmk ,hypk andnewk are denoted by\mathit{ff}'_k ,h_k , andf_k , for0 \leq k \leq p .

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.

Determines whether

new is enabled.It must be one of the following:

t , to enable it.nil , to disable it.:auto , to enable it iffold is enabled.

Determines the name of the theorem that relates

old tonew :

:auto , to use the paired name obtained by pairing the name ofold and the name ofnew , putting the result into the same package asnew .- 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.

Determines whether

old-to-new is enabled:

t , to enable it.nil , to disable it.

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 functionold are verified.

Hints to prove the applicability conditions.

It must be one of the following:

- A keyword-value list
(appcond1 hints1 appcond2 hints2 ...) , where eachappcondk is a keyword that identifies one of the applicability conditions listed in the `Applicability Conditions' section and eachhintsk is a list of hints of the kind that may appear just after:hints in adefthm. The hintshintsk are used to prove applicability conditionappcondk . Theappcond1 ,appcond2 , ... keywords must be all distinct. Anappcondk 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 adefthm. In this case, these same hints are used to prove every applicability condition,.

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 ofcasesplit . This is the default value of the:info , to print, besides any error output and the results, also some additional information about the internal operations ofcasesplit .: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, unlessnil .

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 ifnil (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:result or:info or:all ; no ACL2 output is printed for the event expansion even if:all (because the event expansion is not submitted). If the call ofcasesplit is redundant (as defined in the `Redundancy' section), the event expansion generated by the existing call is printed.

In order for

...

condk , along with the negation of the preceding conditions, establishes the hypothesis ofthmk :(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 thecasesplit design notes, for1 \leq k \leq p .

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 thecasesplit design notes.

...

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 ofcondk .There are

p applicability conditions of this form.Each of these corresponds to a

\mathit{GC}_k in thecasesplit design notes, for1 \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).

...

Each

newk is well-defined (according to its guards) undercondk 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 ofnewk .There are

p applicability conditions of this form.Each of these corresponds to a

\mathit{Gf}_k in thecasesplit design notes, for1 \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 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 ofnew0 .This corresponds to

\mathit{Gf}_0 in thecasesplit 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).

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 byf' .

Theorem that relates

old tonew :(defthm old-to-new (equal (old x1 ... xn) (new x1 ... xn)))In the

casesplit design notes,old-to-new is denoted by\mathit{ff}' .

- Casesplit-implementation
- Implementation of
`casesplit`.