Tailrec-event-generation
Event generation performed by tailrec.
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
- Tailrec-gen-new-to-old-thm
- Generate the theorem equating the new function
to a combination of the old function with a
(f'{}f in the design notes).
- Tailrec-gen-new-fn
- Generate the new function definition.
- Tailrec-gen-everything
- Generate the top-level event.
- Tailrec-gen-old-to-new-thm
- Generate the theorem that relates
the old function to the new function
(f{}f' and f{}f'_0 in the design notes).
- Tailrec-gen-wrapper-fn
- Generate the wrapper function definition.
- Tailrec-gen-domain-of-old-thm
- Generate the theorem asserting that
the old function always yields values in the domain
(D{}f in the design notes).
- Tailrec-gen-combine-left-identity-ground-thm
- Generate the theorem asserting that
the base value of the recursion
is left identity of the combination operator
(L{}I_0 in the design notes).
- Tailrec-gen-appconds
- Generate the applicability conditions.
- Tailrec-gen-wrapper-to-old-thm
- Generate the theorem
that relates the old function to the wrapper function
(f{}\tilde{f} in the design notes).
- Tailrec-gen-old-to-wrapper-thm
- Generate the theorem
that relates the old function to the wrapper function
(f{}\tilde{f} in the design notes).
- Tailrec-gen-old-guard-of-alpha-thm
- Generate the theorem asserting that
the guard of the old function is preserved by \alpha
(\gamma_f\alpha in the design notes).
- Tailrec-gen-alpha-fn
- Generate the definition of
the \alpha function of the design notes.
- Tailrec-gen-domain-of-ground-base-thm
- Generate the theorem asserting that
the base value of the recursion is in the domain
(D{}b_0 in the design notes).
- Tailrec-gen-test-of-alpha-thm
- Generate the theorem asserting that
the recursion exit test succeeds on the result of \alpha
(a\alpha in the design notes).
- Tailrec-gen-old-as-new-term
- Generate the term that
rephrases (a generic call to) the old function
in terms of the new function.
- Tailrec-gen-base-guard-thm
- Generate the theorem asserting that
the guard of the base term is satisfied
if the guard of the target function is
(G{}b in the design notes).
- Tailrec-gen-alpha-component-terms
- Generate the terms of the components of the result of \alpha.
- Tailrec-gen-combine-op
- Generate the combination operator.
- Tailrec-gen-id-var-u
- Generate the variable u to use in the
:combine-left-identity and
:combine-right-identity
applicability conditions.
- Tailrec-gen-alpha-component-terms-aux
- Tailrec-gen-var-v
- Generate the variable u to use in the
:domain-of-combine,
:domain-of-combine-uncond,
:combine-associativity, and
:combine-associativity-uncond
applicability conditions.
- Tailrec-gen-var-u
- Generate the variable u to use in the
:domain-of-combine,
:domain-of-combine-uncond,
:combine-associativity, and
:combine-associativity-uncond
applicability conditions.
- Tailrec-gen-var-w
- Generate the variable u to use in the
:combine-associativity and
:combine-associativity-uncond
applicability conditions.
