Isodata-event-generation
Event generation performed by isodata.
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
- Isodata-gen-everything
- Generate the top-level event.
- Isodata-gen-thm-instances-to-terms-back
- Generate functions to generate certain kinds of lemma instances.
- Isodata-gen-new-fn-body-nonpred
- Generate the body of the new function,
when :predicate is nil.
- Isodata-gen-new-fn
- Generate the new function definition.
- Isodata-gen-new-fn-verify-guards
- Generate the event to verify the guards of the new function.
- Isodata-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 isomaps includes :result.
- Isodata-gen-new-to-list-of-mv-nth
- Generate a local theorem saying that a call of new
can be decomposed via mv-nths
and re-composed via list.
- Isodata-gen-new-to-old-lemma
- Generate the lemma use to prove new-to-old
when old is multi-valued and some result is transformed.
- Isodata-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).
- Isodata-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).
- Isodata-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).
- Isodata-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.
- Isodata-gen-defiso
- Generate a local defiso.
- Isodata-gen-new-to-old-lemma-hints
- Generate the hints to prove
the lemma use to prove new-to-old
when old is multi-valued and some result is transformed.
- Isodata-gen-old-to-new-lemma
- Generate the lemma used to prove old-to-new
when old is multi-valued and some result is transformed.
- Isodata-gen-new-to-old-thm-hints-1res
- Generate the hints to prove new-to-old,
when the result of a single-value function is being transformed.
- Isodata-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).
- Isodata-gen-new-to-old-thm
- Generate the new-to-old theorem.
- Isodata-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).
- Isodata-gen-thm-instances-to-x1...xn
- Generate a function to generate certain kinds of lemma instances.
- Isodata-gen-old-to-new-thm
- Generate the old-to-new theorem.
- Isodata-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.
- Isodata-gen-all-back-guard-instances-to-mv-nth
- Generate the concatenation of
all the m * r lemma instances generated by
isodata-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.
- Isodata-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.
- Isodata-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).
- Isodata-gen-result-vars
- Generate variables for binding results of old or new
when they return multiple results.
- Isodata-gen-old-to-new-lemma-hints
- Generate the hints to prove
the lemma used to prove old-to-new
when old is multi-valued and some result is transformed.
- Isodata-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.
- Isodata-gen-new-to-old-thm-hints-0res
- Generate the hints to prove new-to-old,
when no result is being transformed.
- Isodata-gen-new-to-old-thm-hints
- Generate the hints to prove the theorem
that expresses the new function in terms of the old function.
- Isodata-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 isomaps does not include :result.
- Isodata-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).
- Isodata-gen-new-fn-body-pred
- Generate the body of the new function,
when :predicate is t.
- Isodata-gen-all-back-of-forth-instances-to-mv-nth
- Generate the concatenation of
all the m * r lemma instances generated by
isodata-gen-back-of-forth-instances-to-mv-nth
for all the recursive call arguments of old
passed as the terms input.
- Isodata-gen-new-fn-verify-guards-hints-nonpred
- Generate the hints to verify the guards of the new function,
when :predicate is nil.
- Isodata-gen-new-fn-verify-guards-hints
- Generate the hints to verify the guards of the new function.
- Isodata-gen-all-back-of-forth-instances-to-terms-back
- Generate the concatenation of
all the n * r lemma instances generated by
isodata-gen-back-of-forth-instances-to-terms-back
for all the recursive call arguments of old
passed as the terms input.
- Isodata-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.
- Isodata-gen-all-forth-image-instances-to-terms-back
- Generate the concatenation of
all the n * r lemma instances generated by
isodata-gen-forth-image-instances-to-terms-back
for all the recursive call arguments of old
passed as the terms input.
- Isodata-gen-all-forth-guard-instances-to-terms-back
- Generate the concatenation of
all the n * r lemma instances generated by
isodata-gen-forth-guard-instances-to-terms-back
for all the recursive call arguments of old
passed as the terms input.
- Isodata-gen-old-to-new-thm-hints
- Generate the hints to prove the theorem
that relates the old and new function.
- Isodata-gen-old-to-list-of-mv-nth
- Generate a local theorem saying that a call of old
can be decomposed via mv-nths
and re-composed via list.
- Isodata-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.
- Isodata-xform-rec-calls
- Transform all the calls of old.
- Isodata-gen-appconds
- Generate the applicability conditions.
- Isodata-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.
- Isodata-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.
- Isodata-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 term.
- Isodata-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.
- Isodata-gen-old-to-new-thm-formula
- Generate the formula of the theorem
that expresses the old function in terms of the new function.
- Isodata-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.
- Isodata-gen-lemma-instance-x1...xn-to-forth-of-x1...xn
- Generate a lemma instance where
each variable xi is instantiated with
(forthi xi).
- Isodata-gen-lemma-instance-x1...xn-to-back-of-x1...xn
- Generate a lemma instance where
each variable xi is instantiated with
(backi xi).
- Isodata-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.
- Isodata-gen-forth-image-instances-to-terms-back-aux
- Isodata-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.
- Isodata-gen-forth-guard-instances-to-terms-back-aux
- Isodata-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.
- Isodata-gen-back-of-forth-instances-to-terms-back-aux
- Isodata-gen-old-to-new-lemma-formula
- Generate the formula of
the lemma used to prove old-to-new
when old is multi-valued and some result is transformed.
- Isodata-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.
- Isodata-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.
- Isodata-gen-new-to-old-lemma-formula
- Generate the formula of
the lemma use to prove new-to-old
when old is multi-valued and some result is transformed.
- Isodata-gen-fn-of-terms
- Generate a function to generate certain kinds of terms.
- Isodata-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.
- Isodata-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.
- Isodata-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.
- Isodata-gen-new-to-old-thm-formula
- Generate the formula of new-to-old.
- Isodata-gen-new-fn-termination-hints
- Generate the hints to prove the termination of the new function,
if recursive.
- Isodata-gen-new-fn-body
- Generate the body of the new function.
- Isodata-gen-lemma-instance-x1...xn-to-fn-of-x1...xn
- Generate a function to generate certain kinds of lemma instances.
- Isodata-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.
- Isodata-gen-new-fn-verify-guards-hints-pred
- Generate the hints to verify the guards of the new function,
when :predicate is t.
- Isodata-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.
- Isodata-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.
- Isodata-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.
- Isodata-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.
- Isodata-gen-defisos
- Generate all the local defisos from a list.
- Isodata-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.
- Isodata-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.
- Isodata-gen-new-fn-guard
- Generate the guard of the new function.
- Isodata-gen-new-to-old-thm-hints-mres
- Generate the hints to prove new-to-old,
when some result of a multi-value function is being transformed.
- Isodata-gen-result-vars-aux
- Isodata-gen-new-fn-measure
- Generate the measure of the function, if recursive.
- Isodata-formal-of-newp
- Formal argument of the newp predicate
of an isomorphic mapping.
- Isodata-formal-of-forth
- Formal argument of the forth conversion
of an isomorphic mapping.
- Isodata-formal-of-back
- Formal argument of the back conversion
of an isomorphic mapping.
- Isodata-formal-of-unary
- Formal argument of an (assumed) unary function.
