Expdata-event-generation
Event generation performed by expdata.
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
- Expdata-gen-everything
- Generate the top-level event.
- Expdata-gen-thm-instances-to-terms-back
- Generate functions to generate certain kinds of lemma instances.
- Expdata-gen-new-fn-body-nonpred
- Generate the body of the new function,
when :predicate is nil.
- Expdata-gen-new-fn
- Generate the new function definition.
- Expdata-gen-new-fn-verify-guards
- Generate the event to verify the guards of the new function.
- Expdata-gen-new-fn-verify-guards-hints-nonpred-rec-1res/mres
- Generate the hints to verify the guards of the new function,
when the function is recursive,
when :predicate is nil,
and when surjmaps includes :result.
- Expdata-gen-back-of-forth-instances-to-terms-back
- Generate n lemma instances
such that the i-th instance
is of theorem backi-of-forthi
and instantiates
the formal parameter of forthi
with a given term termi in which
x1, ..., xn are replaced with
(back1 x1), ..., (backn xn).
- Expdata-gen-new-fn-verify-guards-hints-nonpred-nonrec-1res/mres
- Generate the hints to verify the guards of the new function,
when the function is not recursive,
when :predicate is nil,
and some result is being transformed.
- Expdata-gen-forth-image-instances-to-terms-back
- Generate n lemma instances
such that the i-th instance
is of theorem forthi-image
and instantiates
the formal parameter of forthi
with a given term termi in which
x1, ..., xn are replaced with
(back1 x1), ..., (backn xn).
- Expdata-gen-forth-guard-instances-to-terms-back
- Generate n lemma instances
such that the i-th instance
is of theorem forthi-guard
and instantiates
the formal parameter of forthi
with a given term termi in which
x1, ..., xn are replaced with
(back1 x1), ..., (backn xn).
- Expdata-gen-new-to-old-thm-hints-rec-1res
- Generate the hints to prove the theorem
that expresses the new function in terms of the old function,
when the functions are recursive
and the result of a single-value function is being transformed.
- Expdata-gen-defsurj
- Generate a local defsurj.
- Expdata-gen-new-to-old-thm-hints-rec-mres
- Generate the hints to prove the theorem
that expresses the new function in terms of the old function,
when the functions are recursive
and some result of a multi-value function is being transformed.
- Expdata-gen-lemma-instances-var-to-new-forth-rec-call-args-back
- Generate lemma instances where
a variable is instantiated with
a call of the new function
on forth1, ..., forthn applied to
the arguments of a recursive call of old,
with x1, ..., xn in such arguments
replaced with (back1 x1), ..., (backn xn).
- Expdata-gen-new-fn-verify-guards-hints-pred-rec
- Generate the hints to verify the guards of the new function,
when recursive and when :predicate is t.
- Expdata-gen-lemma-instances-x1...xn-to-forth-rec-call-args-back
- Generate a lemma instance
for each j-th recursive call of old,
where each formal xi of old is instantiated with
(forthi updatej-xi<(back1 x1),...,(backn xn)>),
i.e. forthi applied to
the corresponding arguments of the recursive call
in which x1, ..., xn are replaced with
(back1 x1), ..., (backn xn).
- Expdata-gen-thm-instances-to-x1...xn
- Generate a function to generate certain kinds of lemma instances.
- Expdata-gen-newp-of-new-thm-hints
- Generate the hints to prove the theorem
that says that the new function maps
values in the new representation
to values in the old representation.
- Expdata-gen-all-back-guard-instances-to-mv-nth
- Generate the concatenation of
all the n * r lemma instances generated by
expdata-gen-back-guard-instances-to-mv-nth
for all the terms, passed as the term input,
of the form
(new ... (forthi updatek-xi<...,(back xi),...>) ...),
corresponding to all the recursive calls of old.
- Expdata-gen-result-vars
- Generate variables for bounding results of old or new
when they return multiple results.
- Expdata-gen-lemma-instances-x1...xn-to-rec-call-args-back
- Generate a lemma instance
for each j-th recursive call of old,
where each formal xi of old is instantiated with
updatej-xi<(back1 x1),...,(backn xn)>,
i.e. the corresponding argument of the recursive call
in which x1, ..., xn are replaced with
(back1 x1), ..., (backn xn).
- Expdata-gen-new-to-old-thm-hints-rec-0res
- Generate the hints to prove the theorem
that expresses the new function in terms of the old function,
when the functions are recursive
and no result is being transformed.
- Expdata-gen-new-fn-verify-guards-hints-nonpred-rec-0res
- Generate the hints to verify the guards of the new function,
when the function is recursive,
when :predicate is nil,
and when surjmaps does not include :result.
- Expdata-gen-newp-of-new-thm
- Generate the theorem that says that
the new function maps values in the new representation
to values in the old representation.
- Expdata-gen-new-to-old-thm
- Generate the new-to-old theorem.
- Expdata-gen-lemma-instances-var-to-rec-calls-back
- Generate lemma instances where
a variable is instantiated with
each recursive call of old,
with x1, ..., xn in such calls
replaced with (back1 x1), ..., (backn xn).
- Expdata-gen-new-fn-body-pred
- Generate the body of the new function,
when :predicate is t.
- Expdata-gen-old-to-new-thm-hints-1res
- Generate the hints to prove the theorem
that relates the old and new function,
when the result of a single-valued function is being transformed.
- Expdata-gen-new-fn-verify-guards-hints-nonpred
- Generate the hints to verify the guards of the new function,
when :predicate is nil.
- Expdata-gen-new-fn-verify-guards-hints
- Generate the hints to verify the guards of the new function.
- Expdata-gen-all-back-of-forth-instances-to-terms-back
- Generate the concatenation of
all the n * r lemma instances generated by
expdata-gen-back-of-forth-instances-to-terms-back
for all the recursive call arguments of old
passed as the terms input.
- Expdata-gen-old-to-new-thm
- Generate the old-to-new theorem.
- Expdata-gen-new-to-old-thm-hints
- Generate the hints to prove the theorem
that expresses the new function in terms of the old function.
- Expdata-gen-new-fn-verify-guards-hints-pred-nonrec
- Generate the hints to verify the guards of the new function,
when non-recursive and when :predicate is t.
- Expdata-gen-all-forth-image-instances-to-terms-back
- Generate the concatenation of
all the n * r lemma instances generated by
expdata-gen-forth-image-instances-to-terms-back
for all the recursive call arguments of old
passed as the terms input.
- Expdata-gen-all-forth-guard-instances-to-terms-back
- Generate the concatenation of
all the n * r lemma instances generated by
expdata-gen-forth-guard-instances-to-terms-back
for all the recursive call arguments of old
passed as the terms input.
- Expdata-gen-old-to-new-thm-hints-mres
- Generate the hints to prove the theorem
that relates the old and new function,
when some result of a multi-valued function is being transformed.
- Expdata-gen-appconds
- Generate the applicability conditions.
- Expdata-xform-rec-calls
- Transform all the calls of old.
- Expdata-gen-back-of-forth-instances-to-mv-nth
- Generate m lemma instances
such that the j-th instance
is of theorem back_rj-of-forth_rj
and instantiates
the formal parameter of forth_rj
with (mv-nth j-1 ...) applied to
a given term termj.
- Expdata-gen-lemma-instance-x1...xn-to-forth-of-x1...xn
- Generate a lemma instance where
each variable xi is instantiated with
(forthi xi).
- Expdata-gen-forth-image-instances-to-mv-nth
- Generate m lemma instances
such that the j-th instance
is of theorem forth_rj-image
and instantiates
the formal parameter of forth_rj
with (mv-nth j-1 ...) applied to
a given term term.
- Expdata-gen-forth-guard-instances-to-mv-nth
- Generate m lemma instances
such that the j-th instance
is of theorem forth_rj-guard
and instantiates
the formal parameter of forth_rj
with (mv-nth j-1 ...) applied to
a given term term.
- Expdata-gen-back-guard-instances-to-mv-nth
- Generate m lemma instances
such that the j-th instance
is of theorem back_rj-guard
and instantiates
the formal parameter of back_rj
with (mv-nth j-1 ...) applied to
a given term term.
- Expdata-gen-all-back-of-forth-instances-to-mv-nth
- Generate the concatenation of
all the n * r lemma instances generated by
expdata-gen-back-of-forth-instances-to-mv-nth
for all the recursive call arguments of old
passed as the terms input.
- Expdata-gen-old-to-new-thm-formula
- Generate the formula of the theorem
that expresses the old function in terms of the new function.
- Expdata-gen-newp-guard-instances-to-x1...xn
- Generate n lemma instances
such that the i-th instance
is of theorem newpi-guard
and instantiates
the formal parameter of newp
with xi.
- Expdata-gen-new-to-old-thm-formula
- Generate the formula of the theorem
that expresses the new function in terms of the old function.
- Expdata-gen-new-fn-verify-guards-hints-nonpred-nonrec-0res
- Generate the hints to verify the guards of the new function,
when the function is not recursive,
when :predicate is nil,
and no result is being transformed.
- Expdata-gen-lemma-instance-x1...xn-to-back-of-x1...xn
- Generate a lemma instance where
each variable xi is instantiated with
(backi xi).
- Expdata-gen-forth-image-instances-to-x1...xn
- Generate n lemma instances
such that the i-th instance
is of theorem forthi-image
and instantiates
the formal parameter of forth
with xi.
- Expdata-gen-forth-image-instances-to-terms-back-aux
- Expdata-gen-forth-guard-instances-to-x1...xn
- Generate n lemma instances
such that the i-th instance
is of theorem forthi-guard
and instantiates
the formal parameter of forth
with xi.
- Expdata-gen-forth-guard-instances-to-terms-back-aux
- Expdata-gen-back-of-forth-instances-to-x1...xn
- Generate n lemma instances
such that the i-th instance
is of theorem backi-of-forthi
and instantiates
the formal parameter of forth
with xi.
- Expdata-gen-back-of-forth-instances-to-terms-back-aux
- Expdata-gen-back-image-instances-to-x1...xn
- Generate n lemma instances
such that the i-th instance
is of theorem backi-image
and instantiates
the formal parameter of back
with xi.
- Expdata-gen-back-guard-instances-to-x1...xn
- Generate n lemma instances
such that the i-th instance
is of theorem backi-guard
and instantiates
the formal parameter of back
with xi.
- Expdata-gen-newp-of-new-thm-formula
- Generate the formula of the theorem
that says that the new function maps
values in the new representation
to values in the old representation.
- Expdata-gen-fn-of-terms
- Generate a function to generate certain kinds of terms.
- Expdata-gen-oldp-of-rec-call-args-under-contexts
- Generate the conjunction of the implications,
in the :oldp-of-rec-call-args applicability condition,
that correspond to the recursive calls of old.
- Expdata-gen-new-fn-termination-hints
- Generate the hints to prove the termination of the new function,
if recursive.
- Expdata-gen-old-to-new-thm-hints
- Generate the hints to prove the theorem
that relates the old and new function.
- Expdata-gen-lemma-instance-x1...xn-to-fn-of-x1...xn
- Generate a function to generate certain kinds of lemma instances.
- Expdata-gen-old-to-new-thm-hints-0res
- Generate the hints to prove the theorem
that relates the old and new function,
when no result is being transformed.
- Expdata-gen-new-fn-verify-guards-hints-pred
- Generate the hints to verify the guards of the new function,
when :predicate is t.
- Expdata-gen-new-to-old-thm-hints-nonrec
- Generate the hints to prove the theorem
that expresses the new function in terms of the old function,
when the functions are not recursive.
- Expdata-gen-subst-x1...xn-with-back-of-x1...xn
- Substitute each formal xi of old in a term
with the term (backi xi),
where backi is the conversion associated to xi.
- Expdata-gen-oldp-of-terms
- Apply the oldpk or oldp_rk function
to the corresponding term
in a list of terms of length equal to
the number of formals or results of old.
- Expdata-gen-newp-of-terms
- Apply the newpk or newp_rk function
to the corresponding term
in a list of terms of length equal to
the number of formals or results of old.
- Expdata-gen-new-fn-body
- Generate the body of the new function.
- Expdata-gen-forth-of-terms
- Apply the forthk or forth_rk function
to the corresponding term
in a list of terms of length equal to
the number of formals or results of old.
- Expdata-gen-defsurjs
- Generate all the local defsurjs from a list.
- Expdata-gen-back-of-terms
- Apply the backk or back_rk function
to the corresponding term
in a list of terms of length equal to
the number of formals or results of old.
- Expdata-gen-new-fn-guard
- Generate the guard of the new function.
- Expdata-gen-result-vars-aux
- Expdata-gen-new-fn-measure
- Generate the measure of the function, if recursive.
- Expdata-formal-of-newp
- Formal argument of the newp predicate
of a surjective mapping.
- Expdata-formal-of-forth
- Formal argument of the forth conversion
of a surjective mapping.
- Expdata-formal-of-back
- Formal argument of the back conversion
of a surjective mapping.
- Expdata-formal-of-unary
- Formal argument of an (assumed) unary function.
