Casesplit-event-generation
Event generation performed by casesplit.
Some events are generated in two slightly different variants:
one that is local to the generated encapsulate, and one that is exported from the encapsulate. Proof hints are in the former but not in the latter,
thus keeping the ACL2 history ``clean'';
some proof hints may refer to events
that are generated only locally to the encapsulate.
Some events are generated only locally to the generated encapsulate. These are auxiliary events
needed to introduce the non-local (i.e. exported) events,
but whose presence in the ACL2 history is no longer needed
once the exported events have been introduced.
These only-local events have generated fresh names.
In contrast, exported events have names
that are user-controlled, directly or indirectly.
Subtopics
- Casesplit-gen-everything
- Generate the top-level event.
- Casesplit-gen-new-fn
- Generate the new function definition.
- Casesplit-gen-old-to-new-thm
- Generate the theorem that relates the old and new functions.
- Casesplit-gen-appconds-new-guard
- Generate the applicability conditions
new1-guard, ..., newp-guard, new0-guard,
in that order.
- Casesplit-gen-appconds
- Generate the applicability conditions
that are present for the current call of the transformation,
in the order given in the reference documentation.
- Casesplit-gen-appconds-thm-hyp
- Generate the applicability conditions
thm1-hyp, ..., thmp-hyp, thm0-hyp, in that order.
- Casesplit-gen-appcond-new-guard
- Generate the applicability condition newk-guard.
- Casesplit-gen-appcond-name-from-parts
- Create the name (keyword) of an applicability condition
from its parts.
- Casesplit-gen-appconds-cond-guard
- Generate the applicability conditions
cond1-guard, ..., condp-guard, in that order.
- Casesplit-gen-appcond-thm-hyp
- Generate the applicability condition thmk-hyp.
- Casesplit-gen-appcond-cond-guard
- Generate the applicability condition condk-guard.
- Casesplit-gen-appconds-new-guard-aux
- Casesplit-gen-appcond-cond-guard-name
- Name of the applicability condition :condk-guard.
- Casesplit-gen-appcond-thm-hyp-name
- Name of the applicability condition :thmk-hyp.
- Casesplit-gen-appcond-new-guard-name
- Name of the applicability condition :newk-guard.
